DEFINITION sn3_appls_beta()
TYPE =
∀c:C
.∀v:T
.∀t:T
.∀us:TList
.sn3 c (THeads (Flat Appl) us (THead (Bind Abbr) v t))
→∀w:T
.sn3 c w
→(sn3
c
THeads
Flat Appl
us
THead (Flat Appl) v (THead (Bind Abst) w t))
BODY =
assume c: C
assume v: T
assume t: T
assume us: TList
we proceed by induction on us to prove
sn3 c (THeads (Flat Appl) us (THead (Bind Abbr) v t))
→∀w:T
.sn3 c w
→(sn3
c
THeads
Flat Appl
us
THead (Flat Appl) v (THead (Bind Abst) w t))
case TNil : ⇒
the thesis becomes
sn3 c (THeads (Flat Appl) TNil (THead (Bind Abbr) v t))
→∀w:T
.sn3 c w
→(sn3
c
THeads
Flat Appl
TNil
THead (Flat Appl) v (THead (Bind Abst) w t))
we must prove
sn3 c (THeads (Flat Appl) TNil (THead (Bind Abbr) v t))
→∀w:T
.sn3 c w
→(sn3
c
THeads
Flat Appl
TNil
THead (Flat Appl) v (THead (Bind Abst) w t))
or equivalently
sn3 c (THead (Bind Abbr) v t)
→∀w:T
.sn3 c w
→(sn3
c
THeads
Flat Appl
TNil
THead (Flat Appl) v (THead (Bind Abst) w t))
suppose H: sn3 c (THead (Bind Abbr) v t)
assume w: T
suppose H0: sn3 c w
by (sn3_beta . . . H . H0)
we proved sn3 c (THead (Flat Appl) v (THead (Bind Abst) w t))
that is equivalent to
sn3
c
THeads
Flat Appl
TNil
THead (Flat Appl) v (THead (Bind Abst) w t)
we proved
sn3 c (THead (Bind Abbr) v t)
→∀w:T
.sn3 c w
→(sn3
c
THeads
Flat Appl
TNil
THead (Flat Appl) v (THead (Bind Abst) w t))
sn3 c (THeads (Flat Appl) TNil (THead (Bind Abbr) v t))
→∀w:T
.sn3 c w
→(sn3
c
THeads
Flat Appl
TNil
THead (Flat Appl) v (THead (Bind Abst) w t))
case TCons ⇒
we need to prove
∀u:T
.∀us0:TList
.sn3 c (THeads (Flat Appl) us0 (THead (Bind Abbr) v t))
→∀w:T
.sn3 c w
→(sn3
c
THeads
Flat Appl
us0
THead (Flat Appl) v (THead (Bind Abst) w t))
→(sn3 c (THeads (Flat Appl) (TCons u us0) (THead (Bind Abbr) v t))
→∀w:T
.sn3 c w
→(sn3
c
THeads
Flat Appl
TCons u us0
THead (Flat Appl) v (THead (Bind Abst) w t)))
assume u: T
assume us0: TList
we proceed by induction on us0 to prove
sn3 c (THeads (Flat Appl) us0 (THead (Bind Abbr) v t))
→∀w:T
.sn3 c w
→(sn3
c
THeads
Flat Appl
us0
THead (Flat Appl) v (THead (Bind Abst) w t))
→((sn3
c
THead
Flat Appl
u
THeads (Flat Appl) us0 (THead (Bind Abbr) v t))
→∀w:T
.sn3 c w
→(sn3
c
THead
Flat Appl
u
THeads
Flat Appl
us0
THead (Flat Appl) v (THead (Bind Abst) w t)))
case TNil : ⇒
the thesis becomes
sn3 c (THeads (Flat Appl) TNil (THead (Bind Abbr) v t))
→∀w:T
.sn3 c w
→(sn3
c
THeads
Flat Appl
TNil
THead (Flat Appl) v (THead (Bind Abst) w t))
→((sn3
c
THead
Flat Appl
u
THeads (Flat Appl) TNil (THead (Bind Abbr) v t))
→∀w:T
.sn3 c w
→(sn3
c
THead
Flat Appl
u
THeads
Flat Appl
TNil
THead (Flat Appl) v (THead (Bind Abst) w t)))
suppose :
sn3 c (THeads (Flat Appl) TNil (THead (Bind Abbr) v t))
→∀w:T
.sn3 c w
→(sn3
c
THeads
Flat Appl
TNil
THead (Flat Appl) v (THead (Bind Abst) w t))
suppose H0:
sn3
c
THead
Flat Appl
u
THeads (Flat Appl) TNil (THead (Bind Abbr) v t)
assume w: T
suppose H1: sn3 c w
consider H0
we proved
sn3
c
THead
Flat Appl
u
THeads (Flat Appl) TNil (THead (Bind Abbr) v t)
that is equivalent to sn3 c (THead (Flat Appl) u (THead (Bind Abbr) v t))
by (sn3_appl_beta . . . . previous . H1)
we proved
sn3
c
THead
Flat Appl
u
THead (Flat Appl) v (THead (Bind Abst) w t)
that is equivalent to
sn3
c
THead
Flat Appl
u
THeads
Flat Appl
TNil
THead (Flat Appl) v (THead (Bind Abst) w t)
sn3 c (THeads (Flat Appl) TNil (THead (Bind Abbr) v t))
→∀w:T
.sn3 c w
→(sn3
c
THeads
Flat Appl
TNil
THead (Flat Appl) v (THead (Bind Abst) w t))
→((sn3
c
THead
Flat Appl
u
THeads (Flat Appl) TNil (THead (Bind Abbr) v t))
→∀w:T
.sn3 c w
→(sn3
c
THead
Flat Appl
u
THeads
Flat Appl
TNil
THead (Flat Appl) v (THead (Bind Abst) w t)))
case TCons : t0:T t1:TList ⇒
the thesis becomes
∀H0:sn3 c (THeads (Flat Appl) (TCons t0 t1) (THead (Bind Abbr) v t))
→∀w:T
.sn3 c w
→(sn3
c
THeads
Flat Appl
TCons t0 t1
THead (Flat Appl) v (THead (Bind Abst) w t))
.∀H1:sn3
c
THead
Flat Appl
u
THeads (Flat Appl) (TCons t0 t1) (THead (Bind Abbr) v t)
.∀w:T
.∀H2:sn3 c w
.sn3
c
THead
Flat Appl
u
THeads
Flat Appl
TCons t0 t1
THead (Flat Appl) v (THead (Bind Abst) w t)
() by induction hypothesis we know
sn3 c (THeads (Flat Appl) t1 (THead (Bind Abbr) v t))
→∀w:T
.sn3 c w
→(sn3
c
THeads
Flat Appl
t1
THead (Flat Appl) v (THead (Bind Abst) w t))
→((sn3
c
THead
Flat Appl
u
THeads (Flat Appl) t1 (THead (Bind Abbr) v t))
→∀w:T
.sn3 c w
→(sn3
c
THead
Flat Appl
u
THeads
Flat Appl
t1
THead (Flat Appl) v (THead (Bind Abst) w t)))
suppose H0:
sn3 c (THeads (Flat Appl) (TCons t0 t1) (THead (Bind Abbr) v t))
→∀w:T
.sn3 c w
→(sn3
c
THeads
Flat Appl
TCons t0 t1
THead (Flat Appl) v (THead (Bind Abst) w t))
suppose H1:
sn3
c
THead
Flat Appl
u
THeads (Flat Appl) (TCons t0 t1) (THead (Bind Abbr) v t)
assume w: T
suppose H2: sn3 c w
(H_x)
by (sn3_gen_flat . . . . H1)
land
sn3 c u
sn3 c (THeads (Flat Appl) (TCons t0 t1) (THead (Bind Abbr) v t))
end of H_x
(H3) consider H_x
consider H3
we proved
land
sn3 c u
sn3 c (THeads (Flat Appl) (TCons t0 t1) (THead (Bind Abbr) v t))
that is equivalent to
land
sn3 c u
sn3
c
THead
Flat Appl
t0
THeads (Flat Appl) t1 (THead (Bind Abbr) v t)
we proceed by induction on the previous result to prove
sn3
c
THead
Flat Appl
u
THeads
Flat Appl
TCons t0 t1
THead (Flat Appl) v (THead (Bind Abst) w t)
case conj : H4:sn3 c u H5:sn3 c (THead (Flat Appl) t0 (THeads (Flat Appl) t1 (THead (Bind Abbr) v t))) ⇒
the thesis becomes
sn3
c
THead
Flat Appl
u
THeads
Flat Appl
TCons t0 t1
THead (Flat Appl) v (THead (Bind Abst) w t)
(h1)
consider H5
we proved
sn3
c
THead
Flat Appl
t0
THeads (Flat Appl) t1 (THead (Bind Abbr) v t)
that is equivalent to sn3 c (THeads (Flat Appl) (TCons t0 t1) (THead (Bind Abbr) v t))
by (H0 previous . H2)
sn3
c
THeads
Flat Appl
TCons t0 t1
THead (Flat Appl) v (THead (Bind Abst) w t)
end of h1
(h2)
assume u2: T
suppose H6:
pr3
c
THeads
Flat Appl
TCons t0 t1
THead (Flat Appl) v (THead (Bind Abst) w t)
u2
suppose H7:
(iso
THeads
Flat Appl
TCons t0 t1
THead (Flat Appl) v (THead (Bind Abst) w t)
u2)
→∀P:Prop.P
(H8)
by (pr3_iso_appls_beta . . . . . . H6 H7)
pr3 c (THeads (Flat Appl) (TCons t0 t1) (THead (Bind Abbr) v t)) u2
end of H8
by (pr3_thin_dx . . . H8 . .)
we proved
pr3
c
THead
Flat Appl
u
THeads (Flat Appl) (TCons t0 t1) (THead (Bind Abbr) v t)
THead (Flat Appl) u u2
by (sn3_pr3_trans . . H1 . previous)
we proved sn3 c (THead (Flat Appl) u u2)
∀u2:T
.(pr3
c
THeads
Flat Appl
TCons t0 t1
THead (Flat Appl) v (THead (Bind Abst) w t)
u2)
→((iso
THeads
Flat Appl
TCons t0 t1
THead (Flat Appl) v (THead (Bind Abst) w t)
u2)
→∀P:Prop.P
→sn3 c (THead (Flat Appl) u u2))
end of h2
by (sn3_appl_appls . . . . h1 . H4 h2)
sn3
c
THead
Flat Appl
u
THeads
Flat Appl
TCons t0 t1
THead (Flat Appl) v (THead (Bind Abst) w t)
we proved
sn3
c
THead
Flat Appl
u
THeads
Flat Appl
TCons t0 t1
THead (Flat Appl) v (THead (Bind Abst) w t)
∀H0:sn3 c (THeads (Flat Appl) (TCons t0 t1) (THead (Bind Abbr) v t))
→∀w:T
.sn3 c w
→(sn3
c
THeads
Flat Appl
TCons t0 t1
THead (Flat Appl) v (THead (Bind Abst) w t))
.∀H1:sn3
c
THead
Flat Appl
u
THeads (Flat Appl) (TCons t0 t1) (THead (Bind Abbr) v t)
.∀w:T
.∀H2:sn3 c w
.sn3
c
THead
Flat Appl
u
THeads
Flat Appl
TCons t0 t1
THead (Flat Appl) v (THead (Bind Abst) w t)
we proved
sn3 c (THeads (Flat Appl) us0 (THead (Bind Abbr) v t))
→∀w:T
.sn3 c w
→(sn3
c
THeads
Flat Appl
us0
THead (Flat Appl) v (THead (Bind Abst) w t))
→((sn3
c
THead
Flat Appl
u
THeads (Flat Appl) us0 (THead (Bind Abbr) v t))
→∀w:T
.sn3 c w
→(sn3
c
THead
Flat Appl
u
THeads
Flat Appl
us0
THead (Flat Appl) v (THead (Bind Abst) w t)))
that is equivalent to
sn3 c (THeads (Flat Appl) us0 (THead (Bind Abbr) v t))
→∀w:T
.sn3 c w
→(sn3
c
THeads
Flat Appl
us0
THead (Flat Appl) v (THead (Bind Abst) w t))
→(sn3 c (THeads (Flat Appl) (TCons u us0) (THead (Bind Abbr) v t))
→∀w:T
.sn3 c w
→(sn3
c
THeads
Flat Appl
TCons u us0
THead (Flat Appl) v (THead (Bind Abst) w t)))
∀u:T
.∀us0:TList
.sn3 c (THeads (Flat Appl) us0 (THead (Bind Abbr) v t))
→∀w:T
.sn3 c w
→(sn3
c
THeads
Flat Appl
us0
THead (Flat Appl) v (THead (Bind Abst) w t))
→(sn3 c (THeads (Flat Appl) (TCons u us0) (THead (Bind Abbr) v t))
→∀w:T
.sn3 c w
→(sn3
c
THeads
Flat Appl
TCons u us0
THead (Flat Appl) v (THead (Bind Abst) w t)))
we proved
sn3 c (THeads (Flat Appl) us (THead (Bind Abbr) v t))
→∀w:T
.sn3 c w
→(sn3
c
THeads
Flat Appl
us
THead (Flat Appl) v (THead (Bind Abst) w t))
we proved
∀c:C
.∀v:T
.∀t:T
.∀us:TList
.sn3 c (THeads (Flat Appl) us (THead (Bind Abbr) v t))
→∀w:T
.sn3 c w
→(sn3
c
THeads
Flat Appl
us
THead (Flat Appl) v (THead (Bind Abst) w t))