DEFINITION arity_cimp_conf()
TYPE =
∀g:G.∀c1:C.∀t:T.∀a:A.(arity g c1 t a)→∀c2:C.(cimp c1 c2)→(arity g c2 t a)
BODY =
assume g: G
assume c1: C
assume t: T
assume a: A
suppose H: arity g c1 t a
we proceed by induction on H to prove ∀c2:C.(cimp c1 c2)→(arity g c2 t a)
case arity_sort : c:C n:nat ⇒
the thesis becomes ∀c2:C.(cimp c c2)→(arity g c2 (TSort n) (ASort O n))
assume c2: C
suppose : cimp c c2
by (arity_sort . . .)
we proved arity g c2 (TSort n) (ASort O n)
∀c2:C.(cimp c c2)→(arity g c2 (TSort n) (ASort O n))
case arity_abbr : c:C d:C u:T i:nat H0:getl i c (CHead d (Bind Abbr) u) a0:A :arity g d u a0 ⇒
the thesis becomes ∀c2:C.∀H3:(cimp c c2).(arity g c2 (TLRef i) a0)
(H2) by induction hypothesis we know ∀c2:C.(cimp d c2)→(arity g c2 u a0)
assume c2: C
suppose H3: cimp c c2
(H_x)
by (H3 . . . . H0)
ex C λd2:C.getl i c2 (CHead d2 (Bind Abbr) u)
end of H_x
(H4) consider H_x
we proceed by induction on H4 to prove arity g c2 (TLRef i) a0
case ex_intro : x:C H5:getl i c2 (CHead x (Bind Abbr) u) ⇒
the thesis becomes arity g c2 (TLRef i) a0
(H_x0)
by (cimp_getl_conf . . H3 . . . . H0)
ex2 C λd2:C.cimp d d2 λd2:C.getl i c2 (CHead d2 (Bind Abbr) u)
end of H_x0
(H6) consider H_x0
we proceed by induction on H6 to prove arity g c2 (TLRef i) a0
case ex_intro2 : x0:C H7:cimp d x0 H8:getl i c2 (CHead x0 (Bind Abbr) u) ⇒
the thesis becomes arity g c2 (TLRef i) a0
(H9)
by (getl_mono . . . H5 . H8)
we proved eq C (CHead x (Bind Abbr) u) (CHead x0 (Bind Abbr) u)
we proceed by induction on the previous result to prove getl i c2 (CHead x0 (Bind Abbr) u)
case refl_equal : ⇒
the thesis becomes the hypothesis H5
getl i c2 (CHead x0 (Bind Abbr) u)
end of H9
(H10)
by (getl_mono . . . H5 . H8)
we proved eq C (CHead x (Bind Abbr) u) (CHead x0 (Bind Abbr) u)
by (f_equal . . . . . previous)
we proved
eq
C
<λ:C.C> CASE CHead x (Bind Abbr) u OF CSort ⇒x | CHead c0 ⇒c0
<λ:C.C> CASE CHead x0 (Bind Abbr) u OF CSort ⇒x | CHead c0 ⇒c0
eq
C
λe:C.<λ:C.C> CASE e OF CSort ⇒x | CHead c0 ⇒c0 (CHead x (Bind Abbr) u)
λe:C.<λ:C.C> CASE e OF CSort ⇒x | CHead c0 ⇒c0 (CHead x0 (Bind Abbr) u)
end of H10
(H11)
consider H10
we proved
eq
C
<λ:C.C> CASE CHead x (Bind Abbr) u OF CSort ⇒x | CHead c0 ⇒c0
<λ:C.C> CASE CHead x0 (Bind Abbr) u OF CSort ⇒x | CHead c0 ⇒c0
that is equivalent to eq C x x0
by (eq_ind_r . . . H9 . previous)
getl i c2 (CHead x (Bind Abbr) u)
end of H11
(H12)
consider H10
we proved
eq
C
<λ:C.C> CASE CHead x (Bind Abbr) u OF CSort ⇒x | CHead c0 ⇒c0
<λ:C.C> CASE CHead x0 (Bind Abbr) u OF CSort ⇒x | CHead c0 ⇒c0
that is equivalent to eq C x x0
by (eq_ind_r . . . H7 . previous)
cimp d x
end of H12
by (H2 . H12)
we proved arity g x u a0
by (arity_abbr . . . . . H11 . previous)
arity g c2 (TLRef i) a0
arity g c2 (TLRef i) a0
we proved arity g c2 (TLRef i) a0
∀c2:C.∀H3:(cimp c c2).(arity g c2 (TLRef i) a0)
case arity_abst : c:C d:C u:T i:nat H0:getl i c (CHead d (Bind Abst) u) a0:A :arity g d u (asucc g a0) ⇒
the thesis becomes ∀c2:C.∀H3:(cimp c c2).(arity g c2 (TLRef i) a0)
(H2) by induction hypothesis we know ∀c2:C.(cimp d c2)→(arity g c2 u (asucc g a0))
assume c2: C
suppose H3: cimp c c2
(H_x)
by (H3 . . . . H0)
ex C λd2:C.getl i c2 (CHead d2 (Bind Abst) u)
end of H_x
(H4) consider H_x
we proceed by induction on H4 to prove arity g c2 (TLRef i) a0
case ex_intro : x:C H5:getl i c2 (CHead x (Bind Abst) u) ⇒
the thesis becomes arity g c2 (TLRef i) a0
(H_x0)
by (cimp_getl_conf . . H3 . . . . H0)
ex2 C λd2:C.cimp d d2 λd2:C.getl i c2 (CHead d2 (Bind Abst) u)
end of H_x0
(H6) consider H_x0
we proceed by induction on H6 to prove arity g c2 (TLRef i) a0
case ex_intro2 : x0:C H7:cimp d x0 H8:getl i c2 (CHead x0 (Bind Abst) u) ⇒
the thesis becomes arity g c2 (TLRef i) a0
(H9)
by (getl_mono . . . H5 . H8)
we proved eq C (CHead x (Bind Abst) u) (CHead x0 (Bind Abst) u)
we proceed by induction on the previous result to prove getl i c2 (CHead x0 (Bind Abst) u)
case refl_equal : ⇒
the thesis becomes the hypothesis H5
getl i c2 (CHead x0 (Bind Abst) u)
end of H9
(H10)
by (getl_mono . . . H5 . H8)
we proved eq C (CHead x (Bind Abst) u) (CHead x0 (Bind Abst) u)
by (f_equal . . . . . previous)
we proved
eq
C
<λ:C.C> CASE CHead x (Bind Abst) u OF CSort ⇒x | CHead c0 ⇒c0
<λ:C.C> CASE CHead x0 (Bind Abst) u OF CSort ⇒x | CHead c0 ⇒c0
eq
C
λe:C.<λ:C.C> CASE e OF CSort ⇒x | CHead c0 ⇒c0 (CHead x (Bind Abst) u)
λe:C.<λ:C.C> CASE e OF CSort ⇒x | CHead c0 ⇒c0 (CHead x0 (Bind Abst) u)
end of H10
(H11)
consider H10
we proved
eq
C
<λ:C.C> CASE CHead x (Bind Abst) u OF CSort ⇒x | CHead c0 ⇒c0
<λ:C.C> CASE CHead x0 (Bind Abst) u OF CSort ⇒x | CHead c0 ⇒c0
that is equivalent to eq C x x0
by (eq_ind_r . . . H9 . previous)
getl i c2 (CHead x (Bind Abst) u)
end of H11
(H12)
consider H10
we proved
eq
C
<λ:C.C> CASE CHead x (Bind Abst) u OF CSort ⇒x | CHead c0 ⇒c0
<λ:C.C> CASE CHead x0 (Bind Abst) u OF CSort ⇒x | CHead c0 ⇒c0
that is equivalent to eq C x x0
by (eq_ind_r . . . H7 . previous)
cimp d x
end of H12
by (H2 . H12)
we proved arity g x u (asucc g a0)
by (arity_abst . . . . . H11 . previous)
arity g c2 (TLRef i) a0
arity g c2 (TLRef i) a0
we proved arity g c2 (TLRef i) a0
∀c2:C.∀H3:(cimp c c2).(arity g c2 (TLRef i) a0)
case arity_bind : b:B H0:not (eq B b Abst) c:C u:T a1:A :arity g c u a1 t0:T a2:A :arity g (CHead c (Bind b) u) t0 a2 ⇒
the thesis becomes ∀c2:C.∀H5:(cimp c c2).(arity g c2 (THead (Bind b) u t0) a2)
(H2) by induction hypothesis we know ∀c2:C.(cimp c c2)→(arity g c2 u a1)
(H4) by induction hypothesis we know ∀c2:C.(cimp (CHead c (Bind b) u) c2)→(arity g c2 t0 a2)
assume c2: C
suppose H5: cimp c c2
(h1) by (H2 . H5) we proved arity g c2 u a1
(h2)
by (cimp_bind . . H5 . .)
we proved cimp (CHead c (Bind b) u) (CHead c2 (Bind b) u)
by (H4 . previous)
arity g (CHead c2 (Bind b) u) t0 a2
end of h2
by (arity_bind . . H0 . . . h1 . . h2)
we proved arity g c2 (THead (Bind b) u t0) a2
∀c2:C.∀H5:(cimp c c2).(arity g c2 (THead (Bind b) u t0) a2)
case arity_head : c:C u:T a1:A :arity g c u (asucc g a1) t0:T a2:A :arity g (CHead c (Bind Abst) u) t0 a2 ⇒
the thesis becomes ∀c2:C.∀H4:(cimp c c2).(arity g c2 (THead (Bind Abst) u t0) (AHead a1 a2))
(H1) by induction hypothesis we know ∀c2:C.(cimp c c2)→(arity g c2 u (asucc g a1))
(H3) by induction hypothesis we know ∀c2:C.(cimp (CHead c (Bind Abst) u) c2)→(arity g c2 t0 a2)
assume c2: C
suppose H4: cimp c c2
(h1)
by (H1 . H4)
arity g c2 u (asucc g a1)
end of h1
(h2)
by (cimp_bind . . H4 . .)
we proved cimp (CHead c (Bind Abst) u) (CHead c2 (Bind Abst) u)
by (H3 . previous)
arity g (CHead c2 (Bind Abst) u) t0 a2
end of h2
by (arity_head . . . . h1 . . h2)
we proved arity g c2 (THead (Bind Abst) u t0) (AHead a1 a2)
∀c2:C.∀H4:(cimp c c2).(arity g c2 (THead (Bind Abst) u t0) (AHead a1 a2))
case arity_appl : c:C u:T a1:A :arity g c u a1 t0:T a2:A :arity g c t0 (AHead a1 a2) ⇒
the thesis becomes ∀c2:C.∀H4:(cimp c c2).(arity g c2 (THead (Flat Appl) u t0) a2)
(H1) by induction hypothesis we know ∀c2:C.(cimp c c2)→(arity g c2 u a1)
(H3) by induction hypothesis we know ∀c2:C.(cimp c c2)→(arity g c2 t0 (AHead a1 a2))
assume c2: C
suppose H4: cimp c c2
(h1) by (H1 . H4) we proved arity g c2 u a1
(h2)
by (H3 . H4)
arity g c2 t0 (AHead a1 a2)
end of h2
by (arity_appl . . . . h1 . . h2)
we proved arity g c2 (THead (Flat Appl) u t0) a2
∀c2:C.∀H4:(cimp c c2).(arity g c2 (THead (Flat Appl) u t0) a2)
case arity_cast : c:C u:T a0:A :arity g c u (asucc g a0) t0:T :arity g c t0 a0 ⇒
the thesis becomes ∀c2:C.∀H4:(cimp c c2).(arity g c2 (THead (Flat Cast) u t0) a0)
(H1) by induction hypothesis we know ∀c2:C.(cimp c c2)→(arity g c2 u (asucc g a0))
(H3) by induction hypothesis we know ∀c2:C.(cimp c c2)→(arity g c2 t0 a0)
assume c2: C
suppose H4: cimp c c2
(h1)
by (H1 . H4)
arity g c2 u (asucc g a0)
end of h1
(h2) by (H3 . H4) we proved arity g c2 t0 a0
by (arity_cast . . . . h1 . h2)
we proved arity g c2 (THead (Flat Cast) u t0) a0
∀c2:C.∀H4:(cimp c c2).(arity g c2 (THead (Flat Cast) u t0) a0)
case arity_repl : c:C t0:T a1:A :arity g c t0 a1 a2:A H2:leq g a1 a2 ⇒
the thesis becomes ∀c2:C.∀H3:(cimp c c2).(arity g c2 t0 a2)
(H1) by induction hypothesis we know ∀c2:C.(cimp c c2)→(arity g c2 t0 a1)
assume c2: C
suppose H3: cimp c c2
by (H1 . H3)
we proved arity g c2 t0 a1
by (arity_repl . . . . previous . H2)
we proved arity g c2 t0 a2
∀c2:C.∀H3:(cimp c c2).(arity g c2 t0 a2)
we proved ∀c2:C.(cimp c1 c2)→(arity g c2 t a)
we proved ∀g:G.∀c1:C.∀t:T.∀a:A.(arity g c1 t a)→∀c2:C.(cimp c1 c2)→(arity g c2 t a)