DEFINITION sn3_appls_cast()
TYPE =
∀c:C
.∀vs:TList
.∀u:T
.sn3 c (THeads (Flat Appl) vs u)
→∀t:T
.sn3 c (THeads (Flat Appl) vs t)
→sn3 c (THeads (Flat Appl) vs (THead (Flat Cast) u t))
BODY =
assume c: C
assume vs: TList
we proceed by induction on vs to prove
∀u:T
.sn3 c (THeads (Flat Appl) vs u)
→∀t0:T
.sn3 c (THeads (Flat Appl) vs t0)
→sn3 c (THeads (Flat Appl) vs (THead (Flat Cast) u t0))
case TNil : ⇒
the thesis becomes
∀u:T
.sn3 c (THeads (Flat Appl) TNil u)
→∀t0:T
.sn3 c (THeads (Flat Appl) TNil t0)
→sn3 c (THeads (Flat Appl) TNil (THead (Flat Cast) u t0))
assume u: T
we must prove
sn3 c (THeads (Flat Appl) TNil u)
→∀t0:T
.sn3 c (THeads (Flat Appl) TNil t0)
→sn3 c (THeads (Flat Appl) TNil (THead (Flat Cast) u t0))
or equivalently
sn3 c u
→∀t:T
.sn3 c (THeads (Flat Appl) TNil t)
→sn3 c (THeads (Flat Appl) TNil (THead (Flat Cast) u t))
suppose H: sn3 c u
assume t: T
we must prove
sn3 c (THeads (Flat Appl) TNil t)
→sn3 c (THeads (Flat Appl) TNil (THead (Flat Cast) u t))
or equivalently
sn3 c t
→sn3 c (THeads (Flat Appl) TNil (THead (Flat Cast) u t))
suppose H0: sn3 c t
by (sn3_cast . . H . H0)
we proved sn3 c (THead (Flat Cast) u t)
that is equivalent to sn3 c (THeads (Flat Appl) TNil (THead (Flat Cast) u t))
we proved
sn3 c t
→sn3 c (THeads (Flat Appl) TNil (THead (Flat Cast) u t))
that is equivalent to
sn3 c (THeads (Flat Appl) TNil t)
→sn3 c (THeads (Flat Appl) TNil (THead (Flat Cast) u t))
we proved
sn3 c u
→∀t:T
.sn3 c (THeads (Flat Appl) TNil t)
→sn3 c (THeads (Flat Appl) TNil (THead (Flat Cast) u t))
that is equivalent to
sn3 c (THeads (Flat Appl) TNil u)
→∀t0:T
.sn3 c (THeads (Flat Appl) TNil t0)
→sn3 c (THeads (Flat Appl) TNil (THead (Flat Cast) u t0))
∀u:T
.sn3 c (THeads (Flat Appl) TNil u)
→∀t0:T
.sn3 c (THeads (Flat Appl) TNil t0)
→sn3 c (THeads (Flat Appl) TNil (THead (Flat Cast) u t0))
case TCons ⇒
we need to prove
∀t:T
.∀t0:TList
.∀u:T
.sn3 c (THeads (Flat Appl) t0 u)
→∀t0:T
.sn3 c (THeads (Flat Appl) t0 t0)
→sn3 c (THeads (Flat Appl) t0 (THead (Flat Cast) u t0))
→∀u:T
.sn3 c (THeads (Flat Appl) (TCons t t0) u)
→∀t0:T
.sn3 c (THeads (Flat Appl) (TCons t t0) t0)
→sn3 c (THeads (Flat Appl) (TCons t t0) (THead (Flat Cast) u t0))
assume t: T
assume t0: TList
we proceed by induction on t0 to prove
∀u:T
.sn3 c (THeads (Flat Appl) t0 u)
→∀t2:T
.sn3 c (THeads (Flat Appl) t0 t2)
→sn3 c (THeads (Flat Appl) t0 (THead (Flat Cast) u t2))
→∀u:T
.sn3 c (THead (Flat Appl) t (THeads (Flat Appl) t0 u))
→∀t2:T
.sn3 c (THead (Flat Appl) t (THeads (Flat Appl) t0 t2))
→(sn3
c
THead
Flat Appl
t
THeads (Flat Appl) t0 (THead (Flat Cast) u t2))
case TNil : ⇒
the thesis becomes
∀u:T
.sn3 c (THeads (Flat Appl) TNil u)
→∀t1:T
.sn3 c (THeads (Flat Appl) TNil t1)
→sn3 c (THeads (Flat Appl) TNil (THead (Flat Cast) u t1))
→∀u:T
.sn3 c (THead (Flat Appl) t (THeads (Flat Appl) TNil u))
→∀t1:T
.sn3 c (THead (Flat Appl) t (THeads (Flat Appl) TNil t1))
→(sn3
c
THead
Flat Appl
t
THeads (Flat Appl) TNil (THead (Flat Cast) u t1))
suppose :
∀u:T
.sn3 c (THeads (Flat Appl) TNil u)
→∀t1:T
.sn3 c (THeads (Flat Appl) TNil t1)
→sn3 c (THeads (Flat Appl) TNil (THead (Flat Cast) u t1))
assume u: T
suppose H0: sn3 c (THead (Flat Appl) t (THeads (Flat Appl) TNil u))
assume t1: T
suppose H1: sn3 c (THead (Flat Appl) t (THeads (Flat Appl) TNil t1))
(h1)
consider H0
we proved sn3 c (THead (Flat Appl) t (THeads (Flat Appl) TNil u))
sn3 c (THead (Flat Appl) t u)
end of h1
(h2)
consider H1
we proved sn3 c (THead (Flat Appl) t (THeads (Flat Appl) TNil t1))
sn3 c (THead (Flat Appl) t t1)
end of h2
by (sn3_appl_cast . . . h1 . h2)
we proved sn3 c (THead (Flat Appl) t (THead (Flat Cast) u t1))
that is equivalent to
sn3
c
THead
Flat Appl
t
THeads (Flat Appl) TNil (THead (Flat Cast) u t1)
∀u:T
.sn3 c (THeads (Flat Appl) TNil u)
→∀t1:T
.sn3 c (THeads (Flat Appl) TNil t1)
→sn3 c (THeads (Flat Appl) TNil (THead (Flat Cast) u t1))
→∀u:T
.sn3 c (THead (Flat Appl) t (THeads (Flat Appl) TNil u))
→∀t1:T
.sn3 c (THead (Flat Appl) t (THeads (Flat Appl) TNil t1))
→(sn3
c
THead
Flat Appl
t
THeads (Flat Appl) TNil (THead (Flat Cast) u t1))
case TCons : t1:T t2:TList ⇒
the thesis becomes
∀H0:∀u:T
.sn3 c (THeads (Flat Appl) (TCons t1 t2) u)
→∀t3:T
.sn3 c (THeads (Flat Appl) (TCons t1 t2) t3)
→sn3 c (THeads (Flat Appl) (TCons t1 t2) (THead (Flat Cast) u t3))
.∀u:T
.∀H1:sn3 c (THead (Flat Appl) t (THeads (Flat Appl) (TCons t1 t2) u))
.∀t3:T
.∀H2:sn3 c (THead (Flat Appl) t (THeads (Flat Appl) (TCons t1 t2) t3))
.sn3
c
THead
Flat Appl
t
THeads (Flat Appl) (TCons t1 t2) (THead (Flat Cast) u t3)
() by induction hypothesis we know
∀u:T
.sn3 c (THeads (Flat Appl) t2 u)
→∀t3:T
.sn3 c (THeads (Flat Appl) t2 t3)
→sn3 c (THeads (Flat Appl) t2 (THead (Flat Cast) u t3))
→∀u:T
.sn3 c (THead (Flat Appl) t (THeads (Flat Appl) t2 u))
→∀t3:T
.sn3 c (THead (Flat Appl) t (THeads (Flat Appl) t2 t3))
→(sn3
c
THead
Flat Appl
t
THeads (Flat Appl) t2 (THead (Flat Cast) u t3))
suppose H0:
∀u:T
.sn3 c (THeads (Flat Appl) (TCons t1 t2) u)
→∀t3:T
.sn3 c (THeads (Flat Appl) (TCons t1 t2) t3)
→sn3 c (THeads (Flat Appl) (TCons t1 t2) (THead (Flat Cast) u t3))
assume u: T
suppose H1: sn3 c (THead (Flat Appl) t (THeads (Flat Appl) (TCons t1 t2) u))
assume t3: T
suppose H2: sn3 c (THead (Flat Appl) t (THeads (Flat Appl) (TCons t1 t2) t3))
(H_x)
by (sn3_gen_flat . . . . H2)
land (sn3 c t) (sn3 c (THeads (Flat Appl) (TCons t1 t2) t3))
end of H_x
(H3) consider H_x
consider H3
we proved land (sn3 c t) (sn3 c (THeads (Flat Appl) (TCons t1 t2) t3))
that is equivalent to
land (sn3 c t) (sn3 c (THead (Flat Appl) t1 (THeads (Flat Appl) t2 t3)))
we proceed by induction on the previous result to prove
sn3
c
THead
Flat Appl
t
THeads (Flat Appl) (TCons t1 t2) (THead (Flat Cast) u t3)
case conj : :sn3 c t H5:sn3 c (THead (Flat Appl) t1 (THeads (Flat Appl) t2 t3)) ⇒
the thesis becomes
sn3
c
THead
Flat Appl
t
THeads (Flat Appl) (TCons t1 t2) (THead (Flat Cast) u t3)
(H6) consider H5
(H_x0)
by (sn3_gen_flat . . . . H1)
land (sn3 c t) (sn3 c (THeads (Flat Appl) (TCons t1 t2) u))
end of H_x0
(H7) consider H_x0
consider H7
we proved land (sn3 c t) (sn3 c (THeads (Flat Appl) (TCons t1 t2) u))
that is equivalent to
land
sn3 c t
sn3 c (THead (Flat Appl) t1 (THeads (Flat Appl) t2 u))
we proceed by induction on the previous result to prove
sn3
c
THead
Flat Appl
t
THeads (Flat Appl) (TCons t1 t2) (THead (Flat Cast) u t3)
case conj : H8:sn3 c t H9:sn3 c (THead (Flat Appl) t1 (THeads (Flat Appl) t2 u)) ⇒
the thesis becomes
sn3
c
THead
Flat Appl
t
THeads (Flat Appl) (TCons t1 t2) (THead (Flat Cast) u t3)
(H10) consider H9
(h1)
(h1)
consider H10
we proved sn3 c (THead (Flat Appl) t1 (THeads (Flat Appl) t2 u))
sn3 c (THeads (Flat Appl) (TCons t1 t2) u)
end of h1
(h2)
consider H6
we proved sn3 c (THead (Flat Appl) t1 (THeads (Flat Appl) t2 t3))
sn3 c (THeads (Flat Appl) (TCons t1 t2) t3)
end of h2
by (H0 . h1 . h2)
sn3 c (THeads (Flat Appl) (TCons t1 t2) (THead (Flat Cast) u t3))
end of h1
(h2)
assume u2: T
suppose H11: pr3 c (THeads (Flat Appl) (TCons t1 t2) (THead (Flat Cast) u t3)) u2
suppose H12:
iso (THeads (Flat Appl) (TCons t1 t2) (THead (Flat Cast) u t3)) u2
→∀P:Prop.P
by (pr3_iso_appls_cast . . . . . H11 H12)
we proved pr3 c (THeads (Flat Appl) (TCons t1 t2) t3) u2
by (pr3_thin_dx . . . previous . .)
we proved
pr3
c
THead (Flat Appl) t (THeads (Flat Appl) (TCons t1 t2) t3)
THead (Flat Appl) t u2
by (sn3_pr3_trans . . H2 . previous)
we proved sn3 c (THead (Flat Appl) t u2)
∀u2:T
.pr3 c (THeads (Flat Appl) (TCons t1 t2) (THead (Flat Cast) u t3)) u2
→(iso (THeads (Flat Appl) (TCons t1 t2) (THead (Flat Cast) u t3)) u2
→∀P:Prop.P
→sn3 c (THead (Flat Appl) t u2))
end of h2
by (sn3_appl_appls . . . . h1 . H8 h2)
sn3
c
THead
Flat Appl
t
THeads (Flat Appl) (TCons t1 t2) (THead (Flat Cast) u t3)
sn3
c
THead
Flat Appl
t
THeads (Flat Appl) (TCons t1 t2) (THead (Flat Cast) u t3)
we proved
sn3
c
THead
Flat Appl
t
THeads (Flat Appl) (TCons t1 t2) (THead (Flat Cast) u t3)
∀H0:∀u:T
.sn3 c (THeads (Flat Appl) (TCons t1 t2) u)
→∀t3:T
.sn3 c (THeads (Flat Appl) (TCons t1 t2) t3)
→sn3 c (THeads (Flat Appl) (TCons t1 t2) (THead (Flat Cast) u t3))
.∀u:T
.∀H1:sn3 c (THead (Flat Appl) t (THeads (Flat Appl) (TCons t1 t2) u))
.∀t3:T
.∀H2:sn3 c (THead (Flat Appl) t (THeads (Flat Appl) (TCons t1 t2) t3))
.sn3
c
THead
Flat Appl
t
THeads (Flat Appl) (TCons t1 t2) (THead (Flat Cast) u t3)
we proved
∀u:T
.sn3 c (THeads (Flat Appl) t0 u)
→∀t2:T
.sn3 c (THeads (Flat Appl) t0 t2)
→sn3 c (THeads (Flat Appl) t0 (THead (Flat Cast) u t2))
→∀u:T
.sn3 c (THead (Flat Appl) t (THeads (Flat Appl) t0 u))
→∀t2:T
.sn3 c (THead (Flat Appl) t (THeads (Flat Appl) t0 t2))
→(sn3
c
THead
Flat Appl
t
THeads (Flat Appl) t0 (THead (Flat Cast) u t2))
that is equivalent to
∀u:T
.sn3 c (THeads (Flat Appl) t0 u)
→∀t0:T
.sn3 c (THeads (Flat Appl) t0 t0)
→sn3 c (THeads (Flat Appl) t0 (THead (Flat Cast) u t0))
→∀u:T
.sn3 c (THeads (Flat Appl) (TCons t t0) u)
→∀t0:T
.sn3 c (THeads (Flat Appl) (TCons t t0) t0)
→sn3 c (THeads (Flat Appl) (TCons t t0) (THead (Flat Cast) u t0))
∀t:T
.∀t0:TList
.∀u:T
.sn3 c (THeads (Flat Appl) t0 u)
→∀t0:T
.sn3 c (THeads (Flat Appl) t0 t0)
→sn3 c (THeads (Flat Appl) t0 (THead (Flat Cast) u t0))
→∀u:T
.sn3 c (THeads (Flat Appl) (TCons t t0) u)
→∀t0:T
.sn3 c (THeads (Flat Appl) (TCons t t0) t0)
→sn3 c (THeads (Flat Appl) (TCons t t0) (THead (Flat Cast) u t0))
we proved
∀u:T
.sn3 c (THeads (Flat Appl) vs u)
→∀t0:T
.sn3 c (THeads (Flat Appl) vs t0)
→sn3 c (THeads (Flat Appl) vs (THead (Flat Cast) u t0))
we proved
∀c:C
.∀vs:TList
.∀u:T
.sn3 c (THeads (Flat Appl) vs u)
→∀t0:T
.sn3 c (THeads (Flat Appl) vs t0)
→sn3 c (THeads (Flat Appl) vs (THead (Flat Cast) u t0))