DEFINITION sn3_appl_lref()
TYPE =
∀c:C
.∀i:nat
.nf2 c (TLRef i)
→∀v:T.(sn3 c v)→(sn3 c (THead (Flat Appl) v (TLRef i)))
BODY =
assume c: C
assume i: nat
suppose H: nf2 c (TLRef i)
assume v: T
suppose H0: sn3 c v
we proceed by induction on H0 to prove sn3 c (THead (Flat Appl) v (TLRef i))
case sn3_sing : t1:T :∀t2:T.((eq T t1 t2)→∀P:Prop.P)→(pr3 c t1 t2)→(sn3 c t2) ⇒
the thesis becomes sn3 c (THead (Flat Appl) t1 (TLRef i))
(H2) by induction hypothesis we know
∀t2:T
.(eq T t1 t2)→∀P:Prop.P
→(pr3 c t1 t2)→(sn3 c (THead (Flat Appl) t2 (TLRef i)))
assume t2: T
suppose H3: (eq T (THead (Flat Appl) t1 (TLRef i)) t2)→∀P:Prop.P
suppose H4: pr2 c (THead (Flat Appl) t1 (TLRef i)) t2
(H5)
by (pr2_gen_appl . . . . H4)
or3
ex3_2 T T λu2:T.λt2:T.eq T t2 (THead (Flat Appl) u2 t2) λu2:T.λ:T.pr2 c t1 u2 λ:T.λt2:T.pr2 c (TLRef i) t2
ex4_4
T
T
T
T
λy1:T.λz1:T.λ:T.λ:T.eq T (TLRef i) (THead (Bind Abst) y1 z1)
λ:T.λ:T.λu2:T.λt2:T.eq T t2 (THead (Bind Abbr) u2 t2)
λ:T.λ:T.λu2:T.λ:T.pr2 c t1 u2
λ:T.λz1:T.λ:T.λt2:T.∀b:B.∀u:T.(pr2 (CHead c (Bind b) u) z1 t2)
ex6_6
B
T
T
T
T
T
λb:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b Abst)
λb:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.eq T (TLRef i) (THead (Bind b) y1 z1)
λb:B
.λ:T
.λ:T
.λz2:T
.λu2:T
.λy2:T.eq T t2 (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2))
λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr2 c t1 u2
λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr2 c y1 y2
λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr2 (CHead c (Bind b) y2) z1 z2
end of H5
we proceed by induction on H5 to prove sn3 c t2
case or3_intro0 : H6:ex3_2 T T λu2:T.λt3:T.eq T t2 (THead (Flat Appl) u2 t3) λu2:T.λ:T.pr2 c t1 u2 λ:T.λt3:T.pr2 c (TLRef i) t3 ⇒
the thesis becomes sn3 c t2
we proceed by induction on H6 to prove sn3 c t2
case ex3_2_intro : x0:T x1:T H7:eq T t2 (THead (Flat Appl) x0 x1) H8:pr2 c t1 x0 H9:pr2 c (TLRef i) x1 ⇒
the thesis becomes sn3 c t2
(H10)
we proceed by induction on H7 to prove
eq T (THead (Flat Appl) t1 (TLRef i)) (THead (Flat Appl) x0 x1)
→∀P:Prop.P
case refl_equal : ⇒
the thesis becomes the hypothesis H3
eq T (THead (Flat Appl) t1 (TLRef i)) (THead (Flat Appl) x0 x1)
→∀P:Prop.P
end of H10
(H11)
by (H . H9)
we proved eq T (TLRef i) x1
by (eq_ind_r . . . H10 . previous)
(eq
T
THead (Flat Appl) t1 (TLRef i)
THead (Flat Appl) x0 (TLRef i))
→∀P:Prop.P
end of H11
by (H . H9)
we proved eq T (TLRef i) x1
we proceed by induction on the previous result to prove sn3 c (THead (Flat Appl) x0 x1)
case refl_equal : ⇒
the thesis becomes sn3 c (THead (Flat Appl) x0 (TLRef i))
(H_x)
by (term_dec . .)
or (eq T t1 x0) (eq T t1 x0)→∀P:Prop.P
end of H_x
(H13) consider H_x
we proceed by induction on H13 to prove sn3 c (THead (Flat Appl) x0 (TLRef i))
case or_introl : H14:eq T t1 x0 ⇒
the thesis becomes sn3 c (THead (Flat Appl) x0 (TLRef i))
(H15)
by (eq_ind_r . . . H11 . H14)
(eq
T
THead (Flat Appl) t1 (TLRef i)
THead (Flat Appl) t1 (TLRef i))
→∀P:Prop.P
end of H15
we proceed by induction on H14 to prove sn3 c (THead (Flat Appl) x0 (TLRef i))
case refl_equal : ⇒
the thesis becomes sn3 c (THead (Flat Appl) t1 (TLRef i))
by (refl_equal . .)
we proved
eq
T
THead (Flat Appl) t1 (TLRef i)
THead (Flat Appl) t1 (TLRef i)
by (H15 previous .)
sn3 c (THead (Flat Appl) t1 (TLRef i))
sn3 c (THead (Flat Appl) x0 (TLRef i))
case or_intror : H14:(eq T t1 x0)→∀P:Prop.P ⇒
the thesis becomes sn3 c (THead (Flat Appl) x0 (TLRef i))
by (pr3_pr2 . . . H8)
we proved pr3 c t1 x0
by (H2 . H14 previous)
sn3 c (THead (Flat Appl) x0 (TLRef i))
sn3 c (THead (Flat Appl) x0 (TLRef i))
we proved sn3 c (THead (Flat Appl) x0 x1)
by (eq_ind_r . . . previous . H7)
sn3 c t2
sn3 c t2
case or3_intro1 : H6:ex4_4 T T T T λy1:T.λz1:T.λ:T.λ:T.eq T (TLRef i) (THead (Bind Abst) y1 z1) λ:T.λ:T.λu2:T.λt3:T.eq T t2 (THead (Bind Abbr) u2 t3) λ:T.λ:T.λu2:T.λ:T.pr2 c t1 u2 λ:T.λz1:T.λ:T.λt3:T.∀b:B.∀u:T.(pr2 (CHead c (Bind b) u) z1 t3) ⇒
the thesis becomes sn3 c t2
we proceed by induction on H6 to prove sn3 c t2
case ex4_4_intro : x0:T x1:T x2:T x3:T H7:eq T (TLRef i) (THead (Bind Abst) x0 x1) H8:eq T t2 (THead (Bind Abbr) x2 x3) :pr2 c t1 x2 :∀b:B.∀u:T.(pr2 (CHead c (Bind b) u) x1 x3) ⇒
the thesis becomes sn3 c t2
(H12)
we proceed by induction on H7 to prove
<λ:T.Prop>
CASE THead (Bind Abst) x0 x1 OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE TLRef i OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
consider I
we proved True
<λ:T.Prop>
CASE TLRef i OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
<λ:T.Prop>
CASE THead (Bind Abst) x0 x1 OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
end of H12
consider H12
we proved
<λ:T.Prop>
CASE THead (Bind Abst) x0 x1 OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove sn3 c (THead (Bind Abbr) x2 x3)
we proved sn3 c (THead (Bind Abbr) x2 x3)
by (eq_ind_r . . . previous . H8)
sn3 c t2
sn3 c t2
case or3_intro2 : H6:ex6_6 B T T T T T λb:B.λ:T.λ:T.λ:T.λ:T.λ:T.not (eq B b Abst) λb:B.λy1:T.λz1:T.λ:T.λ:T.λ:T.eq T (TLRef i) (THead (Bind b) y1 z1) λb:B.λ:T.λ:T.λz2:T.λu2:T.λy2:T.eq T t2 (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) λ:B.λ:T.λ:T.λ:T.λu2:T.λ:T.pr2 c t1 u2 λ:B.λy1:T.λ:T.λ:T.λ:T.λy2:T.pr2 c y1 y2 λb:B.λ:T.λz1:T.λz2:T.λ:T.λy2:T.pr2 (CHead c (Bind b) y2) z1 z2 ⇒
the thesis becomes sn3 c t2
we proceed by induction on H6 to prove sn3 c t2
case ex6_6_intro : x0:B x1:T x2:T x3:T x4:T x5:T :not (eq B x0 Abst) H8:eq T (TLRef i) (THead (Bind x0) x1 x2) H9:eq T t2 (THead (Bind x0) x5 (THead (Flat Appl) (lift (S O) O x4) x3)) :pr2 c t1 x4 :pr2 c x1 x5 :pr2 (CHead c (Bind x0) x5) x2 x3 ⇒
the thesis becomes sn3 c t2
(H14)
we proceed by induction on H8 to prove
<λ:T.Prop>
CASE THead (Bind x0) x1 x2 OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE TLRef i OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
consider I
we proved True
<λ:T.Prop>
CASE TLRef i OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
<λ:T.Prop>
CASE THead (Bind x0) x1 x2 OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
end of H14
consider H14
we proved
<λ:T.Prop>
CASE THead (Bind x0) x1 x2 OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove sn3 c (THead (Bind x0) x5 (THead (Flat Appl) (lift (S O) O x4) x3))
we proved sn3 c (THead (Bind x0) x5 (THead (Flat Appl) (lift (S O) O x4) x3))
by (eq_ind_r . . . previous . H9)
sn3 c t2
sn3 c t2
we proved sn3 c t2
we proved
∀t2:T
.(eq T (THead (Flat Appl) t1 (TLRef i)) t2)→∀P:Prop.P
→(pr2 c (THead (Flat Appl) t1 (TLRef i)) t2)→(sn3 c t2)
by (sn3_pr2_intro . . previous)
sn3 c (THead (Flat Appl) t1 (TLRef i))
we proved sn3 c (THead (Flat Appl) v (TLRef i))
we proved
∀c:C
.∀i:nat
.nf2 c (TLRef i)
→∀v:T.(sn3 c v)→(sn3 c (THead (Flat Appl) v (TLRef i)))