DEFINITION ty3_arity()
TYPE =
∀g:G.∀c:C.∀t1:T.∀t2:T.(ty3 g c t1 t2)→(ex2 A λa1:A.arity g c t1 a1 λa1:A.arity g c t2 (asucc g a1))
BODY =
assume g: G
assume c: C
assume t1: T
assume t2: T
suppose H: ty3 g c t1 t2
we proceed by induction on H to prove ex2 A λa1:A.arity g c t1 a1 λa1:A.arity g c t2 (asucc g a1)
case ty3_conv : c0:C t3:T t:T :ty3 g c0 t3 t u:T t4:T :ty3 g c0 u t4 H4:pc3 c0 t4 t3 ⇒
the thesis becomes ex2 A λa1:A.arity g c0 u a1 λa1:A.arity g c0 t3 (asucc g a1)
(H1) by induction hypothesis we know ex2 A λa1:A.arity g c0 t3 a1 λa1:A.arity g c0 t (asucc g a1)
(H3) by induction hypothesis we know ex2 A λa1:A.arity g c0 u a1 λa1:A.arity g c0 t4 (asucc g a1)
(H5) consider H1
we proceed by induction on H5 to prove ex2 A λa1:A.arity g c0 u a1 λa1:A.arity g c0 t3 (asucc g a1)
case ex_intro2 : x:A H6:arity g c0 t3 x :arity g c0 t (asucc g x) ⇒
the thesis becomes ex2 A λa1:A.arity g c0 u a1 λa1:A.arity g c0 t3 (asucc g a1)
(H8) consider H3
we proceed by induction on H8 to prove ex2 A λa1:A.arity g c0 u a1 λa1:A.arity g c0 t3 (asucc g a1)
case ex_intro2 : x0:A H9:arity g c0 u x0 H10:arity g c0 t4 (asucc g x0) ⇒
the thesis becomes ex2 A λa1:A.arity g c0 u a1 λa1:A.arity g c0 t3 (asucc g a1)
(H11) consider H4
consider H11
we proved pc3 c0 t4 t3
that is equivalent to ex2 T λt0:T.pr3 c0 t4 t0 λt0:T.pr3 c0 t3 t0
we proceed by induction on the previous result to prove ex2 A λa1:A.arity g c0 u a1 λa1:A.arity g c0 t3 (asucc g a1)
case ex_intro2 : x1:T H12:pr3 c0 t4 x1 H13:pr3 c0 t3 x1 ⇒
the thesis becomes ex2 A λa1:A.arity g c0 u a1 λa1:A.arity g c0 t3 (asucc g a1)
(h1)
by (arity_sred_pr3 . . . H12 . . H10)
arity g c0 x1 (asucc g x0)
end of h1
(h2)
by (arity_sred_pr3 . . . H13 . . H6)
arity g c0 x1 x
end of h2
by (arity_mono . . . . h1 . h2)
we proved leq g (asucc g x0) x
by (leq_sym . . . previous)
we proved leq g x (asucc g x0)
by (arity_repl . . . . H6 . previous)
we proved arity g c0 t3 (asucc g x0)
by (ex_intro2 . . . . H9 previous)
ex2 A λa1:A.arity g c0 u a1 λa1:A.arity g c0 t3 (asucc g a1)
ex2 A λa1:A.arity g c0 u a1 λa1:A.arity g c0 t3 (asucc g a1)
ex2 A λa1:A.arity g c0 u a1 λa1:A.arity g c0 t3 (asucc g a1)
ex2 A λa1:A.arity g c0 u a1 λa1:A.arity g c0 t3 (asucc g a1)
case ty3_sort : c0:C m:nat ⇒
the thesis becomes
ex2
A
λa1:A.arity g c0 (TSort m) a1
λa1:A.arity g c0 (TSort (next g m)) (asucc g a1)
(h1)
by (arity_sort . . .)
arity g c0 (TSort m) (ASort O m)
end of h1
(h2)
by (arity_sort . . .)
we proved arity g c0 (TSort (next g m)) (ASort O (next g m))
arity g c0 (TSort (next g m)) (asucc g (ASort O m))
end of h2
by (ex_intro2 . . . . h1 h2)
ex2
A
λa1:A.arity g c0 (TSort m) a1
λa1:A.arity g c0 (TSort (next g m)) (asucc g a1)
case ty3_abbr : n:nat c0:C d:C u:T H0:getl n c0 (CHead d (Bind Abbr) u) t:T :ty3 g d u t ⇒
the thesis becomes
ex2
A
λa1:A.arity g c0 (TLRef n) a1
λa1:A.arity g c0 (lift (S n) O t) (asucc g a1)
(H2) by induction hypothesis we know ex2 A λa1:A.arity g d u a1 λa1:A.arity g d t (asucc g a1)
(H3) consider H2
we proceed by induction on H3 to prove
ex2
A
λa1:A.arity g c0 (TLRef n) a1
λa1:A.arity g c0 (lift (S n) O t) (asucc g a1)
case ex_intro2 : x:A H4:arity g d u x H5:arity g d t (asucc g x) ⇒
the thesis becomes
ex2
A
λa1:A.arity g c0 (TLRef n) a1
λa1:A.arity g c0 (lift (S n) O t) (asucc g a1)
(h1)
by (arity_abbr . . . . . H0 . H4)
arity g c0 (TLRef n) x
end of h1
(h2)
by (getl_drop . . . . . H0)
we proved drop (S n) O c0 d
by (arity_lift . . . . H5 . . . previous)
arity g c0 (lift (S n) O t) (asucc g x)
end of h2
by (ex_intro2 . . . . h1 h2)
ex2
A
λa1:A.arity g c0 (TLRef n) a1
λa1:A.arity g c0 (lift (S n) O t) (asucc g a1)
ex2
A
λa1:A.arity g c0 (TLRef n) a1
λa1:A.arity g c0 (lift (S n) O t) (asucc g a1)
case ty3_abst : n:nat c0:C d:C u:T H0:getl n c0 (CHead d (Bind Abst) u) t:T :ty3 g d u t ⇒
the thesis becomes
ex2
A
λa1:A.arity g c0 (TLRef n) a1
λa1:A.arity g c0 (lift (S n) O u) (asucc g a1)
(H2) by induction hypothesis we know ex2 A λa1:A.arity g d u a1 λa1:A.arity g d t (asucc g a1)
(H3) consider H2
we proceed by induction on H3 to prove
ex2
A
λa1:A.arity g c0 (TLRef n) a1
λa1:A.arity g c0 (lift (S n) O u) (asucc g a1)
case ex_intro2 : x:A H4:arity g d u x :arity g d t (asucc g x) ⇒
the thesis becomes
ex2
A
λa1:A.arity g c0 (TLRef n) a1
λa1:A.arity g c0 (lift (S n) O u) (asucc g a1)
(H_x)
by (leq_asucc . .)
ex A λa0:A.leq g x (asucc g a0)
end of H_x
(H6) consider H_x
we proceed by induction on H6 to prove
ex2
A
λa1:A.arity g c0 (TLRef n) a1
λa1:A.arity g c0 (lift (S n) O u) (asucc g a1)
case ex_intro : x0:A H7:leq g x (asucc g x0) ⇒
the thesis becomes
ex2
A
λa1:A.arity g c0 (TLRef n) a1
λa1:A.arity g c0 (lift (S n) O u) (asucc g a1)
(h1)
by (arity_repl . . . . H4 . H7)
we proved arity g d u (asucc g x0)
by (arity_abst . . . . . H0 . previous)
arity g c0 (TLRef n) x0
end of h1
(h2)
by (getl_drop . . . . . H0)
we proved drop (S n) O c0 d
by (arity_lift . . . . H4 . . . previous)
we proved arity g c0 (lift (S n) O u) x
by (arity_repl . . . . previous . H7)
arity g c0 (lift (S n) O u) (asucc g x0)
end of h2
by (ex_intro2 . . . . h1 h2)
ex2
A
λa1:A.arity g c0 (TLRef n) a1
λa1:A.arity g c0 (lift (S n) O u) (asucc g a1)
ex2
A
λa1:A.arity g c0 (TLRef n) a1
λa1:A.arity g c0 (lift (S n) O u) (asucc g a1)
ex2
A
λa1:A.arity g c0 (TLRef n) a1
λa1:A.arity g c0 (lift (S n) O u) (asucc g a1)
case ty3_bind : c0:C u:T t:T :ty3 g c0 u t b:B t3:T t4:T :ty3 g (CHead c0 (Bind b) u) t3 t4 ⇒
the thesis becomes
ex2
A
λa1:A.arity g c0 (THead (Bind b) u t3) a1
λa1:A.arity g c0 (THead (Bind b) u t4) (asucc g a1)
(H1) by induction hypothesis we know ex2 A λa1:A.arity g c0 u a1 λa1:A.arity g c0 t (asucc g a1)
(H3) by induction hypothesis we know
ex2
A
λa1:A.arity g (CHead c0 (Bind b) u) t3 a1
λa1:A.arity g (CHead c0 (Bind b) u) t4 (asucc g a1)
(H4) consider H1
we proceed by induction on H4 to prove
ex2
A
λa1:A.arity g c0 (THead (Bind b) u t3) a1
λa1:A.arity g c0 (THead (Bind b) u t4) (asucc g a1)
case ex_intro2 : x:A H5:arity g c0 u x :arity g c0 t (asucc g x) ⇒
the thesis becomes
ex2
A
λa1:A.arity g c0 (THead (Bind b) u t3) a1
λa1:A.arity g c0 (THead (Bind b) u t4) (asucc g a1)
(H7) consider H3
we proceed by induction on H7 to prove
ex2
A
λa1:A.arity g c0 (THead (Bind b) u t3) a1
λa1:A.arity g c0 (THead (Bind b) u t4) (asucc g a1)
case ex_intro2 : x0:A H8:arity g (CHead c0 (Bind b) u) t3 x0 H9:arity g (CHead c0 (Bind b) u) t4 (asucc g x0) ⇒
the thesis becomes
ex2
A
λa1:A.arity g c0 (THead (Bind b) u t3) a1
λa1:A.arity g c0 (THead (Bind b) u t4) (asucc g a1)
(H_x)
by (leq_asucc . .)
ex A λa0:A.leq g x (asucc g a0)
end of H_x
(H10) consider H_x
we proceed by induction on H10 to prove
ex2
A
λa1:A.arity g c0 (THead (Bind b) u t3) a1
λa1:A.arity g c0 (THead (Bind b) u t4) (asucc g a1)
case ex_intro : x1:A H11:leq g x (asucc g x1) ⇒
the thesis becomes
ex2
A
λa1:A.arity g c0 (THead (Bind b) u t3) a1
λa1:A.arity g c0 (THead (Bind b) u t4) (asucc g a1)
suppose H12: arity g (CHead c0 (Bind Abbr) u) t3 x0
suppose H13: arity g (CHead c0 (Bind Abbr) u) t4 (asucc g x0)
(h1)
by (arity_bind . . not_abbr_abst . . . H5 . . H12)
arity g c0 (THead (Bind Abbr) u t3) x0
end of h1
(h2)
by (arity_bind . . not_abbr_abst . . . H5 . . H13)
arity g c0 (THead (Bind Abbr) u t4) (asucc g x0)
end of h2
by (ex_intro2 . . . . h1 h2)
we proved
ex2
A
λa1:A.arity g c0 (THead (Bind Abbr) u t3) a1
λa1:A.arity g c0 (THead (Bind Abbr) u t4) (asucc g a1)
arity g (CHead c0 (Bind Abbr) u) t3 x0
→(arity g (CHead c0 (Bind Abbr) u) t4 (asucc g x0)
→(ex2
A
λa1:A.arity g c0 (THead (Bind Abbr) u t3) a1
λa1:A.arity g c0 (THead (Bind Abbr) u t4) (asucc g a1)))
suppose H12: arity g (CHead c0 (Bind Abst) u) t3 x0
suppose H13: arity g (CHead c0 (Bind Abst) u) t4 (asucc g x0)
(h1)
by (arity_repl . . . . H5 . H11)
we proved arity g c0 u (asucc g x1)
by (arity_head . . . . previous . . H12)
arity g c0 (THead (Bind Abst) u t3) (AHead x1 x0)
end of h1
(h2)
(h1)
by (arity_repl . . . . H5 . H11)
we proved arity g c0 u (asucc g x1)
by (arity_head . . . . previous . . H13)
arity g c0 (THead (Bind Abst) u t4) (AHead x1 (asucc g x0))
end of h1
(h2)
by (leq_refl . .)
we proved leq g (asucc g (AHead x1 x0)) (asucc g (AHead x1 x0))
leq g (AHead x1 (asucc g x0)) (asucc g (AHead x1 x0))
end of h2
by (arity_repl . . . . h1 . h2)
arity g c0 (THead (Bind Abst) u t4) (asucc g (AHead x1 x0))
end of h2
by (ex_intro2 . . . . h1 h2)
we proved
ex2
A
λa1:A.arity g c0 (THead (Bind Abst) u t3) a1
λa1:A.arity g c0 (THead (Bind Abst) u t4) (asucc g a1)
arity g (CHead c0 (Bind Abst) u) t3 x0
→(arity g (CHead c0 (Bind Abst) u) t4 (asucc g x0)
→(ex2
A
λa1:A.arity g c0 (THead (Bind Abst) u t3) a1
λa1:A.arity g c0 (THead (Bind Abst) u t4) (asucc g a1)))
suppose H12: arity g (CHead c0 (Bind Void) u) t3 x0
suppose H13: arity g (CHead c0 (Bind Void) u) t4 (asucc g x0)
(h1)
by (sym_not_eq . . . not_abst_void)
we proved not (eq B Void Abst)
by (arity_bind . . previous . . . H5 . . H12)
arity g c0 (THead (Bind Void) u t3) x0
end of h1
(h2)
by (sym_not_eq . . . not_abst_void)
we proved not (eq B Void Abst)
by (arity_bind . . previous . . . H5 . . H13)
arity g c0 (THead (Bind Void) u t4) (asucc g x0)
end of h2
by (ex_intro2 . . . . h1 h2)
we proved
ex2
A
λa1:A.arity g c0 (THead (Bind Void) u t3) a1
λa1:A.arity g c0 (THead (Bind Void) u t4) (asucc g a1)
arity g (CHead c0 (Bind Void) u) t3 x0
→(arity g (CHead c0 (Bind Void) u) t4 (asucc g x0)
→(ex2
A
λa1:A.arity g c0 (THead (Bind Void) u t3) a1
λa1:A.arity g c0 (THead (Bind Void) u t4) (asucc g a1)))
by (previous . H8 H9)
ex2
A
λa1:A.arity g c0 (THead (Bind b) u t3) a1
λa1:A.arity g c0 (THead (Bind b) u t4) (asucc g a1)
ex2
A
λa1:A.arity g c0 (THead (Bind b) u t3) a1
λa1:A.arity g c0 (THead (Bind b) u t4) (asucc g a1)
ex2
A
λa1:A.arity g c0 (THead (Bind b) u t3) a1
λa1:A.arity g c0 (THead (Bind b) u t4) (asucc g a1)
ex2
A
λa1:A.arity g c0 (THead (Bind b) u t3) a1
λa1:A.arity g c0 (THead (Bind b) u t4) (asucc g a1)
case ty3_appl : c0:C w:T u:T :ty3 g c0 w u v:T t:T :ty3 g c0 v (THead (Bind Abst) u t) ⇒
the thesis becomes
ex2
A
λa1:A.arity g c0 (THead (Flat Appl) w v) a1
λa1:A
.arity
g
c0
THead (Flat Appl) w (THead (Bind Abst) u t)
asucc g a1
(H1) by induction hypothesis we know ex2 A λa1:A.arity g c0 w a1 λa1:A.arity g c0 u (asucc g a1)
(H3) by induction hypothesis we know
ex2 A λa1:A.arity g c0 v a1 λa1:A.arity g c0 (THead (Bind Abst) u t) (asucc g a1)
(H4) consider H1
we proceed by induction on H4 to prove
ex2
A
λa1:A.arity g c0 (THead (Flat Appl) w v) a1
λa1:A
.arity
g
c0
THead (Flat Appl) w (THead (Bind Abst) u t)
asucc g a1
case ex_intro2 : x:A H5:arity g c0 w x H6:arity g c0 u (asucc g x) ⇒
the thesis becomes
ex2
A
λa1:A.arity g c0 (THead (Flat Appl) w v) a1
λa1:A
.arity
g
c0
THead (Flat Appl) w (THead (Bind Abst) u t)
asucc g a1
(H7) consider H3
we proceed by induction on H7 to prove
ex2
A
λa1:A.arity g c0 (THead (Flat Appl) w v) a1
λa1:A
.arity
g
c0
THead (Flat Appl) w (THead (Bind Abst) u t)
asucc g a1
case ex_intro2 : x0:A H8:arity g c0 v x0 H9:arity g c0 (THead (Bind Abst) u t) (asucc g x0) ⇒
the thesis becomes
ex2
A
λa1:A.arity g c0 (THead (Flat Appl) w v) a1
λa1:A
.arity
g
c0
THead (Flat Appl) w (THead (Bind Abst) u t)
asucc g a1
(H10)
by (arity_gen_abst . . . . . H9)
ex3_2
A
A
λa1:A.λa2:A.eq A (asucc g x0) (AHead a1 a2)
λa1:A.λ:A.arity g c0 u (asucc g a1)
λ:A.λa2:A.arity g (CHead c0 (Bind Abst) u) t a2
end of H10
we proceed by induction on H10 to prove
ex2
A
λa1:A.arity g c0 (THead (Flat Appl) w v) a1
λa1:A
.arity
g
c0
THead (Flat Appl) w (THead (Bind Abst) u t)
asucc g a1
case ex3_2_intro : x1:A x2:A H11:eq A (asucc g x0) (AHead x1 x2) H12:arity g c0 u (asucc g x1) H13:arity g (CHead c0 (Bind Abst) u) t x2 ⇒
the thesis becomes
ex2
A
λa1:A.arity g c0 (THead (Flat Appl) w v) a1
λa1:A
.arity
g
c0
THead (Flat Appl) w (THead (Bind Abst) u t)
asucc g a1
(H14)
by (sym_eq . . . H11)
eq A (AHead x1 x2) (asucc g x0)
end of H14
(H15)
by (asucc_gen_head . . . . H14)
ex2 A λa0:A.eq A x0 (AHead x1 a0) λa0:A.eq A x2 (asucc g a0)
end of H15
we proceed by induction on H15 to prove
ex2
A
λa1:A.arity g c0 (THead (Flat Appl) w v) a1
λa1:A
.arity
g
c0
THead (Flat Appl) w (THead (Bind Abst) u t)
asucc g a1
case ex_intro2 : x3:A H16:eq A x0 (AHead x1 x3) H17:eq A x2 (asucc g x3) ⇒
the thesis becomes
ex2
A
λa1:A.arity g c0 (THead (Flat Appl) w v) a1
λa1:A
.arity
g
c0
THead (Flat Appl) w (THead (Bind Abst) u t)
asucc g a1
(H18)
we proceed by induction on H17 to prove arity g (CHead c0 (Bind Abst) u) t (asucc g x3)
case refl_equal : ⇒
the thesis becomes the hypothesis H13
arity g (CHead c0 (Bind Abst) u) t (asucc g x3)
end of H18
(H19)
we proceed by induction on H16 to prove arity g c0 v (AHead x1 x3)
case refl_equal : ⇒
the thesis becomes the hypothesis H8
arity g c0 v (AHead x1 x3)
end of H19
(h1)
by (arity_mono . . . . H12 . H6)
we proved leq g (asucc g x1) (asucc g x)
by (asucc_inj . . . previous)
we proved leq g x1 x
by (leq_sym . . . previous)
we proved leq g x x1
by (arity_repl . . . . H5 . previous)
we proved arity g c0 w x1
by (arity_appl . . . . previous . . H19)
arity g c0 (THead (Flat Appl) w v) x3
end of h1
(h2)
by (arity_head . . . . H6 . . H18)
we proved arity g c0 (THead (Bind Abst) u t) (AHead x (asucc g x3))
by (arity_appl . . . . H5 . . previous)
arity
g
c0
THead (Flat Appl) w (THead (Bind Abst) u t)
asucc g x3
end of h2
by (ex_intro2 . . . . h1 h2)
ex2
A
λa1:A.arity g c0 (THead (Flat Appl) w v) a1
λa1:A
.arity
g
c0
THead (Flat Appl) w (THead (Bind Abst) u t)
asucc g a1
ex2
A
λa1:A.arity g c0 (THead (Flat Appl) w v) a1
λa1:A
.arity
g
c0
THead (Flat Appl) w (THead (Bind Abst) u t)
asucc g a1
ex2
A
λa1:A.arity g c0 (THead (Flat Appl) w v) a1
λa1:A
.arity
g
c0
THead (Flat Appl) w (THead (Bind Abst) u t)
asucc g a1
ex2
A
λa1:A.arity g c0 (THead (Flat Appl) w v) a1
λa1:A
.arity
g
c0
THead (Flat Appl) w (THead (Bind Abst) u t)
asucc g a1
ex2
A
λa1:A.arity g c0 (THead (Flat Appl) w v) a1
λa1:A
.arity
g
c0
THead (Flat Appl) w (THead (Bind Abst) u t)
asucc g a1
case ty3_cast : c0:C t3:T t4:T :ty3 g c0 t3 t4 t0:T :ty3 g c0 t4 t0 ⇒
the thesis becomes
ex2
A
λa1:A.arity g c0 (THead (Flat Cast) t4 t3) a1
λa1:A.arity g c0 (THead (Flat Cast) t0 t4) (asucc g a1)
(H1) by induction hypothesis we know ex2 A λa1:A.arity g c0 t3 a1 λa1:A.arity g c0 t4 (asucc g a1)
(H3) by induction hypothesis we know ex2 A λa1:A.arity g c0 t4 a1 λa1:A.arity g c0 t0 (asucc g a1)
(H4) consider H1
we proceed by induction on H4 to prove
ex2
A
λa1:A.arity g c0 (THead (Flat Cast) t4 t3) a1
λa1:A.arity g c0 (THead (Flat Cast) t0 t4) (asucc g a1)
case ex_intro2 : x:A H5:arity g c0 t3 x H6:arity g c0 t4 (asucc g x) ⇒
the thesis becomes
ex2
A
λa1:A.arity g c0 (THead (Flat Cast) t4 t3) a1
λa1:A.arity g c0 (THead (Flat Cast) t0 t4) (asucc g a1)
(H7) consider H3
we proceed by induction on H7 to prove
ex2
A
λa1:A.arity g c0 (THead (Flat Cast) t4 t3) a1
λa1:A.arity g c0 (THead (Flat Cast) t0 t4) (asucc g a1)
case ex_intro2 : x0:A H8:arity g c0 t4 x0 H9:arity g c0 t0 (asucc g x0) ⇒
the thesis becomes
ex2
A
λa1:A.arity g c0 (THead (Flat Cast) t4 t3) a1
λa1:A.arity g c0 (THead (Flat Cast) t0 t4) (asucc g a1)
(h1)
by (arity_cast . . . . H6 . H5)
arity g c0 (THead (Flat Cast) t4 t3) x
end of h1
(h2)
by (arity_mono . . . . H8 . H6)
we proved leq g x0 (asucc g x)
by (asucc_repl . . . previous)
we proved leq g (asucc g x0) (asucc g (asucc g x))
by (arity_repl . . . . H9 . previous)
we proved arity g c0 t0 (asucc g (asucc g x))
by (arity_cast . . . . previous . H6)
arity g c0 (THead (Flat Cast) t0 t4) (asucc g x)
end of h2
by (ex_intro2 . . . . h1 h2)
ex2
A
λa1:A.arity g c0 (THead (Flat Cast) t4 t3) a1
λa1:A.arity g c0 (THead (Flat Cast) t0 t4) (asucc g a1)
ex2
A
λa1:A.arity g c0 (THead (Flat Cast) t4 t3) a1
λa1:A.arity g c0 (THead (Flat Cast) t0 t4) (asucc g a1)
ex2
A
λa1:A.arity g c0 (THead (Flat Cast) t4 t3) a1
λa1:A.arity g c0 (THead (Flat Cast) t0 t4) (asucc g a1)
we proved ex2 A λa1:A.arity g c t1 a1 λa1:A.arity g c t2 (asucc g a1)
we proved ∀g:G.∀c:C.∀t1:T.∀t2:T.(ty3 g c t1 t2)→(ex2 A λa1:A.arity g c t1 a1 λa1:A.arity g c t2 (asucc g a1))