DEFINITION sn3_appls_lref()
TYPE =
∀c:C
.∀i:nat
.nf2 c (TLRef i)
→∀us:TList.(sns3 c us)→(sn3 c (THeads (Flat Appl) us (TLRef i)))
BODY =
assume c: C
assume i: nat
suppose H: nf2 c (TLRef i)
assume us: TList
we proceed by induction on us to prove (sns3 c us)→(sn3 c (THeads (Flat Appl) us (TLRef i)))
case TNil : ⇒
the thesis becomes (sns3 c TNil)→(sn3 c (THeads (Flat Appl) TNil (TLRef i)))
we must prove (sns3 c TNil)→(sn3 c (THeads (Flat Appl) TNil (TLRef i)))
or equivalently True→(sn3 c (THeads (Flat Appl) TNil (TLRef i)))
suppose : True
by (sn3_nf2 . . H)
we proved sn3 c (TLRef i)
that is equivalent to sn3 c (THeads (Flat Appl) TNil (TLRef i))
we proved True→(sn3 c (THeads (Flat Appl) TNil (TLRef i)))
(sns3 c TNil)→(sn3 c (THeads (Flat Appl) TNil (TLRef i)))
case TCons ⇒
we need to prove
∀t:T
.∀t0:TList
.(sns3 c t0)→(sn3 c (THeads (Flat Appl) t0 (TLRef i)))
→(sns3 c (TCons t t0)
→sn3 c (THeads (Flat Appl) (TCons t t0) (TLRef i)))
assume t: T
assume t0: TList
we proceed by induction on t0 to prove
(sns3 c t0)→(sn3 c (THeads (Flat Appl) t0 (TLRef i)))
→(land (sn3 c t) (sns3 c t0)
→sn3 c (THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))))
case TNil : ⇒
the thesis becomes
(sns3 c TNil)→(sn3 c (THeads (Flat Appl) TNil (TLRef i)))
→(land (sn3 c t) (sns3 c TNil)
→(sn3
c
THead (Flat Appl) t (THeads (Flat Appl) TNil (TLRef i))))
suppose : (sns3 c TNil)→(sn3 c (THeads (Flat Appl) TNil (TLRef i)))
suppose H1: land (sn3 c t) (sns3 c TNil)
(H2) consider H1
consider H2
we proved land (sn3 c t) (sns3 c TNil)
that is equivalent to land (sn3 c t) True
we proceed by induction on the previous result to prove
sn3
c
THead (Flat Appl) t (THeads (Flat Appl) TNil (TLRef i))
case conj : H3:sn3 c t :True ⇒
the thesis becomes
sn3
c
THead (Flat Appl) t (THeads (Flat Appl) TNil (TLRef i))
by (sn3_appl_lref . . H . H3)
we proved sn3 c (THead (Flat Appl) t (TLRef i))
sn3
c
THead (Flat Appl) t (THeads (Flat Appl) TNil (TLRef i))
we proved
sn3
c
THead (Flat Appl) t (THeads (Flat Appl) TNil (TLRef i))
(sns3 c TNil)→(sn3 c (THeads (Flat Appl) TNil (TLRef i)))
→(land (sn3 c t) (sns3 c TNil)
→(sn3
c
THead (Flat Appl) t (THeads (Flat Appl) TNil (TLRef i))))
case TCons : t1:T t2:TList ⇒
the thesis becomes
∀H1:sns3 c (TCons t1 t2)
→sn3 c (THeads (Flat Appl) (TCons t1 t2) (TLRef i))
.∀H2:land (sn3 c t) (sns3 c (TCons t1 t2))
.sn3
c
THead
Flat Appl
t
THeads (Flat Appl) (TCons t1 t2) (TLRef i)
() by induction hypothesis we know
(sns3 c t2)→(sn3 c (THeads (Flat Appl) t2 (TLRef i)))
→(land (sn3 c t) (sns3 c t2)
→sn3 c (THead (Flat Appl) t (THeads (Flat Appl) t2 (TLRef i))))
suppose H1:
sns3 c (TCons t1 t2)
→sn3 c (THeads (Flat Appl) (TCons t1 t2) (TLRef i))
suppose H2: land (sn3 c t) (sns3 c (TCons t1 t2))
(H3) consider H2
consider H3
we proved land (sn3 c t) (sns3 c (TCons t1 t2))
that is equivalent to land (sn3 c t) (land (sn3 c t1) (sns3 c t2))
we proceed by induction on the previous result to prove
sn3
c
THead
Flat Appl
t
THeads (Flat Appl) (TCons t1 t2) (TLRef i)
case conj : H4:sn3 c t H5:land (sn3 c t1) (sns3 c t2) ⇒
the thesis becomes
sn3
c
THead
Flat Appl
t
THeads (Flat Appl) (TCons t1 t2) (TLRef i)
we proceed by induction on H5 to prove
sn3
c
THead
Flat Appl
t
THeads (Flat Appl) (TCons t1 t2) (TLRef i)
case conj : H6:sn3 c t1 H7:sns3 c t2 ⇒
the thesis becomes
sn3
c
THead
Flat Appl
t
THeads (Flat Appl) (TCons t1 t2) (TLRef i)
(h1)
by (conj . . H6 H7)
we proved land (sn3 c t1) (sns3 c t2)
that is equivalent to sns3 c (TCons t1 t2)
by (H1 previous)
sn3 c (THeads (Flat Appl) (TCons t1 t2) (TLRef i))
end of h1
(h2)
assume u2: T
suppose H8: pr3 c (THeads (Flat Appl) (TCons t1 t2) (TLRef i)) u2
suppose H9: (iso (THeads (Flat Appl) (TCons t1 t2) (TLRef i)) u2)→∀P:Prop.P
by (nf2_iso_appls_lref . . H . . H8)
we proved iso (THeads (Flat Appl) (TCons t1 t2) (TLRef i)) u2
by (H9 previous .)
we proved sn3 c (THead (Flat Appl) t u2)
∀u2:T
.pr3 c (THeads (Flat Appl) (TCons t1 t2) (TLRef i)) u2
→((iso (THeads (Flat Appl) (TCons t1 t2) (TLRef i)) u2)→∀P:Prop.P
→sn3 c (THead (Flat Appl) t u2))
end of h2
by (sn3_appl_appls . . . . h1 . H4 h2)
sn3
c
THead
Flat Appl
t
THeads (Flat Appl) (TCons t1 t2) (TLRef i)
sn3
c
THead
Flat Appl
t
THeads (Flat Appl) (TCons t1 t2) (TLRef i)
we proved
sn3
c
THead
Flat Appl
t
THeads (Flat Appl) (TCons t1 t2) (TLRef i)
∀H1:sns3 c (TCons t1 t2)
→sn3 c (THeads (Flat Appl) (TCons t1 t2) (TLRef i))
.∀H2:land (sn3 c t) (sns3 c (TCons t1 t2))
.sn3
c
THead
Flat Appl
t
THeads (Flat Appl) (TCons t1 t2) (TLRef i)
we proved
(sns3 c t0)→(sn3 c (THeads (Flat Appl) t0 (TLRef i)))
→(land (sn3 c t) (sns3 c t0)
→sn3 c (THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))))
that is equivalent to
(sns3 c t0)→(sn3 c (THeads (Flat Appl) t0 (TLRef i)))
→(sns3 c (TCons t t0)
→sn3 c (THeads (Flat Appl) (TCons t t0) (TLRef i)))
∀t:T
.∀t0:TList
.(sns3 c t0)→(sn3 c (THeads (Flat Appl) t0 (TLRef i)))
→(sns3 c (TCons t t0)
→sn3 c (THeads (Flat Appl) (TCons t t0) (TLRef i)))
we proved (sns3 c us)→(sn3 c (THeads (Flat Appl) us (TLRef i)))
we proved
∀c:C
.∀i:nat
.nf2 c (TLRef i)
→∀us:TList.(sns3 c us)→(sn3 c (THeads (Flat Appl) us (TLRef i)))