DEFINITION nf2_appls_lref()
TYPE =
∀c:C
.∀i:nat
.nf2 c (TLRef i)
→∀vs:TList.(nfs2 c vs)→(nf2 c (THeads (Flat Appl) vs (TLRef i)))
BODY =
assume c: C
assume i: nat
suppose H: nf2 c (TLRef i)
assume vs: TList
we proceed by induction on vs to prove (nfs2 c vs)→(nf2 c (THeads (Flat Appl) vs (TLRef i)))
case TNil : ⇒
the thesis becomes (nfs2 c TNil)→(nf2 c (THeads (Flat Appl) TNil (TLRef i)))
we must prove (nfs2 c TNil)→(nf2 c (THeads (Flat Appl) TNil (TLRef i)))
or equivalently True→(nf2 c (THeads (Flat Appl) TNil (TLRef i)))
suppose : True
consider H
we proved nf2 c (TLRef i)
that is equivalent to nf2 c (THeads (Flat Appl) TNil (TLRef i))
we proved True→(nf2 c (THeads (Flat Appl) TNil (TLRef i)))
(nfs2 c TNil)→(nf2 c (THeads (Flat Appl) TNil (TLRef i)))
case TCons : t:T t0:TList ⇒
the thesis becomes
nfs2 c (TCons t t0)
→nf2 c (THeads (Flat Appl) (TCons t t0) (TLRef i))
(H0) by induction hypothesis we know (nfs2 c t0)→(nf2 c (THeads (Flat Appl) t0 (TLRef i)))
we must prove
nfs2 c (TCons t t0)
→nf2 c (THeads (Flat Appl) (TCons t t0) (TLRef i))
or equivalently
land (nf2 c t) (nfs2 c t0)
→nf2 c (THeads (Flat Appl) (TCons t t0) (TLRef i))
suppose H1: land (nf2 c t) (nfs2 c t0)
(H2) consider H1
we proceed by induction on H2 to prove nf2 c (THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i)))
case conj : H3:nf2 c t H4:nfs2 c t0 ⇒
the thesis becomes nf2 c (THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i)))
(H_y)
by (H0 H4)
nf2 c (THeads (Flat Appl) t0 (TLRef i))
end of H_y
assume t2: T
suppose H5: pr2 c (THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))) t2
(H6)
by (pr2_gen_appl . . . . H5)
or3
ex3_2
T
T
λu2:T.λt2:T.eq T t2 (THead (Flat Appl) u2 t2)
λu2:T.λ:T.pr2 c t u2
λ:T.λt2:T.pr2 c (THeads (Flat Appl) t0 (TLRef i)) t2
ex4_4
T
T
T
T
λy1:T
.λz1:T
.λ:T
.λ:T.eq T (THeads (Flat Appl) t0 (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 t 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 (THeads (Flat Appl) t0 (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 t 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 H6
we proceed by induction on H6 to prove
eq T (THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))) t2
case or3_intro0 : H7:ex3_2 T T λu2:T.λt3:T.eq T t2 (THead (Flat Appl) u2 t3) λu2:T.λ:T.pr2 c t u2 λ:T.λt3:T.pr2 c (THeads (Flat Appl) t0 (TLRef i)) t3 ⇒
the thesis becomes
eq T (THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))) t2
we proceed by induction on H7 to prove
eq T (THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))) t2
case ex3_2_intro : x0:T x1:T H8:eq T t2 (THead (Flat Appl) x0 x1) H9:pr2 c t x0 H10:pr2 c (THeads (Flat Appl) t0 (TLRef i)) x1 ⇒
the thesis becomes
eq T (THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))) t2
by (H_y . H10)
we proved eq T (THeads (Flat Appl) t0 (TLRef i)) x1
we proceed by induction on the previous result to prove
eq
T
THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))
THead (Flat Appl) x0 x1
case refl_equal : ⇒
the thesis becomes
eq
T
THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))
THead (Flat Appl) x0 (THeads (Flat Appl) t0 (TLRef i))
by (H3 . H9)
we proved eq T t x0
we proceed by induction on the previous result to prove
eq
T
THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))
THead (Flat Appl) x0 (THeads (Flat Appl) t0 (TLRef i))
case refl_equal : ⇒
the thesis becomes
eq
T
THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))
THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))
by (refl_equal . .)
eq
T
THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))
THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))
eq
T
THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))
THead (Flat Appl) x0 (THeads (Flat Appl) t0 (TLRef i))
we proved
eq
T
THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))
THead (Flat Appl) x0 x1
by (eq_ind_r . . . previous . H8)
eq T (THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))) t2
eq T (THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))) t2
case or3_intro1 : H7:ex4_4 T T T T λy1:T.λz1:T.λ:T.λ:T.eq T (THeads (Flat Appl) t0 (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 t u2 λ:T.λz1:T.λ:T.λt3:T.∀b:B.∀u:T.(pr2 (CHead c (Bind b) u) z1 t3) ⇒
the thesis becomes
eq T (THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))) t2
we proceed by induction on H7 to prove
eq T (THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))) t2
case ex4_4_intro : x0:T x1:T x2:T x3:T H8:eq T (THeads (Flat Appl) t0 (TLRef i)) (THead (Bind Abst) x0 x1) H9:eq T t2 (THead (Bind Abbr) x2 x3) :pr2 c t x2 :∀b:B.∀u:T.(pr2 (CHead c (Bind b) u) x1 x3) ⇒
the thesis becomes
eq T (THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))) t2
suppose : nf2 c (THeads (Flat Appl) TNil (TLRef i))
suppose H13:
eq
T
THeads (Flat Appl) TNil (TLRef i)
THead (Bind Abst) x0 x1
(H14)
consider H13
we proved
eq
T
THeads (Flat Appl) TNil (TLRef i)
THead (Bind Abst) x0 x1
that is equivalent to eq T (TLRef i) (THead (Bind Abst) x0 x1)
we proceed by induction on the previous result 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 H14
consider H14
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
eq
T
THead (Flat Appl) t (THeads (Flat Appl) TNil (TLRef i))
THead (Bind Abbr) x2 x3
we proved
eq
T
THead (Flat Appl) t (THeads (Flat Appl) TNil (TLRef i))
THead (Bind Abbr) x2 x3
nf2 c (THeads (Flat Appl) TNil (TLRef i))
→((eq
T
THeads (Flat Appl) TNil (TLRef i)
THead (Bind Abst) x0 x1)
→(eq
T
THead (Flat Appl) t (THeads (Flat Appl) TNil (TLRef i))
THead (Bind Abbr) x2 x3))
assume t1: T
assume t3: TList
suppose :
nf2 c (THeads (Flat Appl) t3 (TLRef i))
→(eq T (THeads (Flat Appl) t3 (TLRef i)) (THead (Bind Abst) x0 x1)
→(eq
T
THead (Flat Appl) t (THeads (Flat Appl) t3 (TLRef i))
THead (Bind Abbr) x2 x3))
suppose : nf2 c (THeads (Flat Appl) (TCons t1 t3) (TLRef i))
suppose H13:
eq
T
THeads (Flat Appl) (TCons t1 t3) (TLRef i)
THead (Bind Abst) x0 x1
(H14)
consider H13
we proved
eq
T
THeads (Flat Appl) (TCons t1 t3) (TLRef i)
THead (Bind Abst) x0 x1
that is equivalent to
eq
T
THead (Flat Appl) t1 (THeads (Flat Appl) t3 (TLRef i))
THead (Bind Abst) x0 x1
we proceed by induction on the previous result to prove
<λ:T.Prop>
CASE THead (Bind Abst) x0 x1 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒False | Flat ⇒True
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE THead (Flat Appl) t1 (THeads (Flat Appl) t3 (TLRef i)) OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒False | Flat ⇒True
consider I
we proved True
<λ:T.Prop>
CASE THead (Flat Appl) t1 (THeads (Flat Appl) t3 (TLRef i)) OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒False | Flat ⇒True
<λ:T.Prop>
CASE THead (Bind Abst) x0 x1 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒False | Flat ⇒True
end of H14
consider H14
we proved
<λ:T.Prop>
CASE THead (Bind Abst) x0 x1 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒False | Flat ⇒True
that is equivalent to False
we proceed by induction on the previous result to prove
eq
T
THead
Flat Appl
t
THeads (Flat Appl) (TCons t1 t3) (TLRef i)
THead (Bind Abbr) x2 x3
we proved
eq
T
THead
Flat Appl
t
THeads (Flat Appl) (TCons t1 t3) (TLRef i)
THead (Bind Abbr) x2 x3
nf2 c (THeads (Flat Appl) (TCons t1 t3) (TLRef i))
→∀H13:eq
T
THeads (Flat Appl) (TCons t1 t3) (TLRef i)
THead (Bind Abst) x0 x1
.eq
T
THead
Flat Appl
t
THeads (Flat Appl) (TCons t1 t3) (TLRef i)
THead (Bind Abbr) x2 x3
by (previous . H_y H8)
we proved
eq
T
THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))
THead (Bind Abbr) x2 x3
by (eq_ind_r . . . previous . H9)
eq T (THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))) t2
eq T (THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))) t2
case or3_intro2 : H7: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 (THeads (Flat Appl) t0 (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 t 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
eq T (THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))) t2
we proceed by induction on H7 to prove
eq T (THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))) t2
case ex6_6_intro : x0:B x1:T x2:T x3:T x4:T x5:T :not (eq B x0 Abst) H9:eq T (THeads (Flat Appl) t0 (TLRef i)) (THead (Bind x0) x1 x2) H10:eq T t2 (THead (Bind x0) x5 (THead (Flat Appl) (lift (S O) O x4) x3)) :pr2 c t x4 :pr2 c x1 x5 :pr2 (CHead c (Bind x0) x5) x2 x3 ⇒
the thesis becomes
eq T (THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))) t2
suppose : nf2 c (THeads (Flat Appl) TNil (TLRef i))
suppose H15: eq T (THeads (Flat Appl) TNil (TLRef i)) (THead (Bind x0) x1 x2)
(H16)
consider H15
we proved eq T (THeads (Flat Appl) TNil (TLRef i)) (THead (Bind x0) x1 x2)
that is equivalent to eq T (TLRef i) (THead (Bind x0) x1 x2)
we proceed by induction on the previous result 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 H16
consider H16
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
eq
T
THead (Flat Appl) t (THeads (Flat Appl) TNil (TLRef i))
THead (Bind x0) x5 (THead (Flat Appl) (lift (S O) O x4) x3)
we proved
eq
T
THead (Flat Appl) t (THeads (Flat Appl) TNil (TLRef i))
THead (Bind x0) x5 (THead (Flat Appl) (lift (S O) O x4) x3)
nf2 c (THeads (Flat Appl) TNil (TLRef i))
→(eq T (THeads (Flat Appl) TNil (TLRef i)) (THead (Bind x0) x1 x2)
→(eq
T
THead (Flat Appl) t (THeads (Flat Appl) TNil (TLRef i))
THead (Bind x0) x5 (THead (Flat Appl) (lift (S O) O x4) x3)))
assume t1: T
assume t3: TList
suppose :
nf2 c (THeads (Flat Appl) t3 (TLRef i))
→(eq T (THeads (Flat Appl) t3 (TLRef i)) (THead (Bind x0) x1 x2)
→(eq
T
THead (Flat Appl) t (THeads (Flat Appl) t3 (TLRef i))
THead (Bind x0) x5 (THead (Flat Appl) (lift (S O) O x4) x3)))
suppose : nf2 c (THeads (Flat Appl) (TCons t1 t3) (TLRef i))
suppose H15:
eq
T
THeads (Flat Appl) (TCons t1 t3) (TLRef i)
THead (Bind x0) x1 x2
(H16)
consider H15
we proved
eq
T
THeads (Flat Appl) (TCons t1 t3) (TLRef i)
THead (Bind x0) x1 x2
that is equivalent to
eq
T
THead (Flat Appl) t1 (THeads (Flat Appl) t3 (TLRef i))
THead (Bind x0) x1 x2
we proceed by induction on the previous result to prove
<λ:T.Prop>
CASE THead (Bind x0) x1 x2 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒False | Flat ⇒True
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE THead (Flat Appl) t1 (THeads (Flat Appl) t3 (TLRef i)) OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒False | Flat ⇒True
consider I
we proved True
<λ:T.Prop>
CASE THead (Flat Appl) t1 (THeads (Flat Appl) t3 (TLRef i)) OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒False | Flat ⇒True
<λ:T.Prop>
CASE THead (Bind x0) x1 x2 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒False | Flat ⇒True
end of H16
consider H16
we proved
<λ:T.Prop>
CASE THead (Bind x0) x1 x2 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒False | Flat ⇒True
that is equivalent to False
we proceed by induction on the previous result to prove
eq
T
THead
Flat Appl
t
THeads (Flat Appl) (TCons t1 t3) (TLRef i)
THead (Bind x0) x5 (THead (Flat Appl) (lift (S O) O x4) x3)
we proved
eq
T
THead
Flat Appl
t
THeads (Flat Appl) (TCons t1 t3) (TLRef i)
THead (Bind x0) x5 (THead (Flat Appl) (lift (S O) O x4) x3)
nf2 c (THeads (Flat Appl) (TCons t1 t3) (TLRef i))
→∀H15:eq
T
THeads (Flat Appl) (TCons t1 t3) (TLRef i)
THead (Bind x0) x1 x2
.eq
T
THead
Flat Appl
t
THeads (Flat Appl) (TCons t1 t3) (TLRef i)
THead (Bind x0) x5 (THead (Flat Appl) (lift (S O) O x4) x3)
by (previous . H_y H9)
we proved
eq
T
THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))
THead (Bind x0) x5 (THead (Flat Appl) (lift (S O) O x4) x3)
by (eq_ind_r . . . previous . H10)
eq T (THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))) t2
eq T (THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))) t2
we proved
eq T (THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))) t2
we proved
∀t2:T
.pr2 c (THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))) t2
→eq T (THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))) t2
nf2 c (THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i)))
we proved nf2 c (THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i)))
that is equivalent to nf2 c (THeads (Flat Appl) (TCons t t0) (TLRef i))
we proved
land (nf2 c t) (nfs2 c t0)
→nf2 c (THeads (Flat Appl) (TCons t t0) (TLRef i))
nfs2 c (TCons t t0)
→nf2 c (THeads (Flat Appl) (TCons t t0) (TLRef i))
we proved (nfs2 c vs)→(nf2 c (THeads (Flat Appl) vs (TLRef i)))
we proved
∀c:C
.∀i:nat
.nf2 c (TLRef i)
→∀vs:TList.(nfs2 c vs)→(nf2 c (THeads (Flat Appl) vs (TLRef i)))