DEFINITION csuba_arity()
TYPE =
∀g:G.∀c1:C.∀t:T.∀a:A.(arity g c1 t a)→∀c2:C.(csuba g 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.(csuba g c1 c2)→(arity g c2 t a)
case arity_sort : c:C n:nat ⇒
the thesis becomes ∀c2:C.(csuba g c c2)→(arity g c2 (TSort n) (ASort O n))
assume c2: C
suppose : csuba g c c2
by (arity_sort . . .)
we proved arity g c2 (TSort n) (ASort O n)
∀c2:C.(csuba g 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:(csuba g c c2).(arity g c2 (TLRef i) a0)
(H2) by induction hypothesis we know ∀c2:C.(csuba g d c2)→(arity g c2 u a0)
assume c2: C
suppose H3: csuba g c c2
(H4)
by (csuba_getl_abbr . . . . . H0 . H3)
ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abbr) u) λd2:C.csuba g d d2
end of H4
we proceed by induction on H4 to prove arity g c2 (TLRef i) a0
case ex_intro2 : x:C H5:getl i c2 (CHead x (Bind Abbr) u) H6:csuba g d x ⇒
the thesis becomes arity g c2 (TLRef i) a0
by (H2 . H6)
we proved arity g x u a0
by (arity_abbr . . . . . H5 . previous)
arity g c2 (TLRef i) a0
we proved arity g c2 (TLRef i) a0
∀c2:C.∀H3:(csuba g 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 H1:arity g d u (asucc g a0) ⇒
the thesis becomes ∀c2:C.∀H3:(csuba g c c2).(arity g c2 (TLRef i) a0)
(H2) by induction hypothesis we know ∀c2:C.(csuba g d c2)→(arity g c2 u (asucc g a0))
assume c2: C
suppose H3: csuba g c c2
(H4)
by (csuba_getl_abst . . . . . H0 . H3)
or
ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d d2
ex4_3
C
T
A
λd2:C.λu2:T.λ:A.getl i c2 (CHead d2 (Bind Abbr) u2)
λd2:C.λ:T.λ:A.csuba g d d2
λ:C.λ:T.λa:A.arity g d u (asucc g a)
λd2:C.λu2:T.λa:A.arity g d2 u2 a
end of H4
we proceed by induction on H4 to prove arity g c2 (TLRef i) a0
case or_introl : H5:ex2 C λd2:C.getl i c2 (CHead d2 (Bind Abst) u) λd2:C.csuba g d d2 ⇒
the thesis becomes arity g c2 (TLRef i) a0
we proceed by induction on H5 to prove arity g c2 (TLRef i) a0
case ex_intro2 : x:C H6:getl i c2 (CHead x (Bind Abst) u) H7:csuba g d x ⇒
the thesis becomes arity g c2 (TLRef i) a0
by (H2 . H7)
we proved arity g x u (asucc g a0)
by (arity_abst . . . . . H6 . previous)
arity g c2 (TLRef i) a0
arity g c2 (TLRef i) a0
case or_intror : H5:ex4_3 C T A λd2:C.λu2:T.λ:A.getl i c2 (CHead d2 (Bind Abbr) u2) λd2:C.λ:T.λ:A.csuba g d d2 λ:C.λ:T.λa1:A.arity g d u (asucc g a1) λd2:C.λu2:T.λa1:A.arity g d2 u2 a1 ⇒
the thesis becomes arity g c2 (TLRef i) a0
we proceed by induction on H5 to prove arity g c2 (TLRef i) a0
case ex4_3_intro : x0:C x1:T x2:A H6:getl i c2 (CHead x0 (Bind Abbr) x1) :csuba g d x0 H8:arity g d u (asucc g x2) H9:arity g x0 x1 x2 ⇒
the thesis becomes arity g c2 (TLRef i) a0
(h1)
by (arity_abbr . . . . . H6 . H9)
arity g c2 (TLRef i) x2
end of h1
(h2)
by (arity_mono . . . . H8 . H1)
we proved leq g (asucc g x2) (asucc g a0)
by (asucc_inj . . . previous)
leq g x2 a0
end of h2
by (arity_repl . . . . h1 . h2)
arity g c2 (TLRef i) a0
arity g c2 (TLRef i) a0
we proved arity g c2 (TLRef i) a0
∀c2:C.∀H3:(csuba g 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:(csuba g c c2).(arity g c2 (THead (Bind b) u t0) a2)
(H2) by induction hypothesis we know ∀c2:C.(csuba g c c2)→(arity g c2 u a1)
(H4) by induction hypothesis we know ∀c2:C.(csuba g (CHead c (Bind b) u) c2)→(arity g c2 t0 a2)
assume c2: C
suppose H5: csuba g c c2
(h1) by (H2 . H5) we proved arity g c2 u a1
(h2)
by (csuba_head . . . H5 . .)
we proved csuba g (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:(csuba g 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:(csuba g c c2).(arity g c2 (THead (Bind Abst) u t0) (AHead a1 a2))
(H1) by induction hypothesis we know ∀c2:C.(csuba g c c2)→(arity g c2 u (asucc g a1))
(H3) by induction hypothesis we know ∀c2:C.(csuba g (CHead c (Bind Abst) u) c2)→(arity g c2 t0 a2)
assume c2: C
suppose H4: csuba g c c2
(h1)
by (H1 . H4)
arity g c2 u (asucc g a1)
end of h1
(h2)
by (csuba_head . . . H4 . .)
we proved csuba g (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:(csuba g 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:(csuba g c c2).(arity g c2 (THead (Flat Appl) u t0) a2)
(H1) by induction hypothesis we know ∀c2:C.(csuba g c c2)→(arity g c2 u a1)
(H3) by induction hypothesis we know ∀c2:C.(csuba g c c2)→(arity g c2 t0 (AHead a1 a2))
assume c2: C
suppose H4: csuba g 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:(csuba g 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:(csuba g c c2).(arity g c2 (THead (Flat Cast) u t0) a0)
(H1) by induction hypothesis we know ∀c2:C.(csuba g c c2)→(arity g c2 u (asucc g a0))
(H3) by induction hypothesis we know ∀c2:C.(csuba g c c2)→(arity g c2 t0 a0)
assume c2: C
suppose H4: csuba g 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:(csuba g 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:(csuba g c c2).(arity g c2 t0 a2)
(H1) by induction hypothesis we know ∀c2:C.(csuba g c c2)→(arity g c2 t0 a1)
assume c2: C
suppose H3: csuba g 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:(csuba g c c2).(arity g c2 t0 a2)
we proved ∀c2:C.(csuba g c1 c2)→(arity g c2 t a)
we proved ∀g:G.∀c1:C.∀t:T.∀a:A.(arity g c1 t a)→∀c2:C.(csuba g c1 c2)→(arity g c2 t a)