DEFINITION arity_appls_cast()
TYPE =
∀g:G
.∀c:C
.∀u:T
.∀t:T
.∀vs:TList
.∀a:A
.arity g c (THeads (Flat Appl) vs u) (asucc g a)
→(arity g c (THeads (Flat Appl) vs t) a
→arity g c (THeads (Flat Appl) vs (THead (Flat Cast) u t)) a)
BODY =
assume g: G
assume c: C
assume u: T
assume t: T
assume vs: TList
we proceed by induction on vs to prove
∀a:A
.arity g c (THeads (Flat Appl) vs u) (asucc g a)
→(arity g c (THeads (Flat Appl) vs t) a
→arity g c (THeads (Flat Appl) vs (THead (Flat Cast) u t)) a)
case TNil : ⇒
the thesis becomes
∀a:A
.arity g c (THeads (Flat Appl) TNil u) (asucc g a)
→(arity g c (THeads (Flat Appl) TNil t) a
→(arity
g
c
THeads (Flat Appl) TNil (THead (Flat Cast) u t)
a))
assume a: A
we must prove
arity g c (THeads (Flat Appl) TNil u) (asucc g a)
→(arity g c (THeads (Flat Appl) TNil t) a
→(arity
g
c
THeads (Flat Appl) TNil (THead (Flat Cast) u t)
a))
or equivalently
arity g c u (asucc g a)
→(arity g c (THeads (Flat Appl) TNil t) a
→(arity
g
c
THeads (Flat Appl) TNil (THead (Flat Cast) u t)
a))
suppose H: arity g c u (asucc g a)
we must prove
arity g c (THeads (Flat Appl) TNil t) a
→(arity
g
c
THeads (Flat Appl) TNil (THead (Flat Cast) u t)
a)
or equivalently
arity g c t a
→(arity
g
c
THeads (Flat Appl) TNil (THead (Flat Cast) u t)
a)
suppose H0: arity g c t a
by (arity_cast . . . . H . H0)
we proved arity g c (THead (Flat Cast) u t) a
that is equivalent to
arity
g
c
THeads (Flat Appl) TNil (THead (Flat Cast) u t)
a
we proved
arity g c t a
→(arity
g
c
THeads (Flat Appl) TNil (THead (Flat Cast) u t)
a)
that is equivalent to
arity g c (THeads (Flat Appl) TNil t) a
→(arity
g
c
THeads (Flat Appl) TNil (THead (Flat Cast) u t)
a)
we proved
arity g c u (asucc g a)
→(arity g c (THeads (Flat Appl) TNil t) a
→(arity
g
c
THeads (Flat Appl) TNil (THead (Flat Cast) u t)
a))
that is equivalent to
arity g c (THeads (Flat Appl) TNil u) (asucc g a)
→(arity g c (THeads (Flat Appl) TNil t) a
→(arity
g
c
THeads (Flat Appl) TNil (THead (Flat Cast) u t)
a))
∀a:A
.arity g c (THeads (Flat Appl) TNil u) (asucc g a)
→(arity g c (THeads (Flat Appl) TNil t) a
→(arity
g
c
THeads (Flat Appl) TNil (THead (Flat Cast) u t)
a))
case TCons : t0:T t1:TList ⇒
the thesis becomes
∀a:A
.arity g c (THeads (Flat Appl) (TCons t0 t1) u) (asucc g a)
→(arity g c (THeads (Flat Appl) (TCons t0 t1) t) a
→(arity
g
c
THeads (Flat Appl) (TCons t0 t1) (THead (Flat Cast) u t)
a))
(H) by induction hypothesis we know
∀a:A
.arity g c (THeads (Flat Appl) t1 u) (asucc g a)
→(arity g c (THeads (Flat Appl) t1 t) a
→arity g c (THeads (Flat Appl) t1 (THead (Flat Cast) u t)) a)
assume a: A
we must prove
arity g c (THeads (Flat Appl) (TCons t0 t1) u) (asucc g a)
→(arity g c (THeads (Flat Appl) (TCons t0 t1) t) a
→(arity
g
c
THeads (Flat Appl) (TCons t0 t1) (THead (Flat Cast) u t)
a))
or equivalently
(arity
g
c
THead (Flat Appl) t0 (THeads (Flat Appl) t1 u)
asucc g a)
→(arity g c (THeads (Flat Appl) (TCons t0 t1) t) a
→(arity
g
c
THeads (Flat Appl) (TCons t0 t1) (THead (Flat Cast) u t)
a))
suppose H0:
arity
g
c
THead (Flat Appl) t0 (THeads (Flat Appl) t1 u)
asucc g a
we must prove
arity g c (THeads (Flat Appl) (TCons t0 t1) t) a
→(arity
g
c
THeads (Flat Appl) (TCons t0 t1) (THead (Flat Cast) u t)
a)
or equivalently
arity g c (THead (Flat Appl) t0 (THeads (Flat Appl) t1 t)) a
→(arity
g
c
THeads (Flat Appl) (TCons t0 t1) (THead (Flat Cast) u t)
a)
suppose H1: arity g c (THead (Flat Appl) t0 (THeads (Flat Appl) t1 t)) a
(H2)
by (arity_gen_appl . . . . . H1)
ex2
A
λa1:A.arity g c t0 a1
λa1:A.arity g c (THeads (Flat Appl) t1 t) (AHead a1 a)
end of H2
we proceed by induction on H2 to prove
arity
g
c
THead
Flat Appl
t0
THeads (Flat Appl) t1 (THead (Flat Cast) u t)
a
case ex_intro2 : x:A H3:arity g c t0 x H4:arity g c (THeads (Flat Appl) t1 t) (AHead x a) ⇒
the thesis becomes
arity
g
c
THead
Flat Appl
t0
THeads (Flat Appl) t1 (THead (Flat Cast) u t)
a
(H5)
by (arity_gen_appl . . . . . H0)
ex2
A
λa1:A.arity g c t0 a1
λa1:A.arity g c (THeads (Flat Appl) t1 u) (AHead a1 (asucc g a))
end of H5
we proceed by induction on H5 to prove
arity
g
c
THead
Flat Appl
t0
THeads (Flat Appl) t1 (THead (Flat Cast) u t)
a
case ex_intro2 : x0:A H6:arity g c t0 x0 H7:arity g c (THeads (Flat Appl) t1 u) (AHead x0 (asucc g a)) ⇒
the thesis becomes
arity
g
c
THead
Flat Appl
t0
THeads (Flat Appl) t1 (THead (Flat Cast) u t)
a
(h1)
(h1)
by (arity_mono . . . . H6 . H3)
leq g x0 x
end of h1
(h2)
by (leq_refl . .)
leq g (asucc g a) (asucc g a)
end of h2
by (leq_head . . . h1 . . h2)
we proved leq g (AHead x0 (asucc g a)) (AHead x (asucc g a))
by (arity_repl . . . . H7 . previous)
arity g c (THeads (Flat Appl) t1 u) (AHead x (asucc g a))
end of h1
(h2)
by (leq_refl . .)
we proved leq g (asucc g (AHead x a)) (asucc g (AHead x a))
leq g (AHead x (asucc g a)) (asucc g (AHead x a))
end of h2
by (arity_repl . . . . h1 . h2)
we proved arity g c (THeads (Flat Appl) t1 u) (asucc g (AHead x a))
by (H . previous H4)
we proved
arity
g
c
THeads (Flat Appl) t1 (THead (Flat Cast) u t)
AHead x a
by (arity_appl . . . . H3 . . previous)
arity
g
c
THead
Flat Appl
t0
THeads (Flat Appl) t1 (THead (Flat Cast) u t)
a
arity
g
c
THead
Flat Appl
t0
THeads (Flat Appl) t1 (THead (Flat Cast) u t)
a
we proved
arity
g
c
THead
Flat Appl
t0
THeads (Flat Appl) t1 (THead (Flat Cast) u t)
a
that is equivalent to
arity
g
c
THeads (Flat Appl) (TCons t0 t1) (THead (Flat Cast) u t)
a
we proved
arity g c (THead (Flat Appl) t0 (THeads (Flat Appl) t1 t)) a
→(arity
g
c
THeads (Flat Appl) (TCons t0 t1) (THead (Flat Cast) u t)
a)
that is equivalent to
arity g c (THeads (Flat Appl) (TCons t0 t1) t) a
→(arity
g
c
THeads (Flat Appl) (TCons t0 t1) (THead (Flat Cast) u t)
a)
we proved
(arity
g
c
THead (Flat Appl) t0 (THeads (Flat Appl) t1 u)
asucc g a)
→(arity g c (THeads (Flat Appl) (TCons t0 t1) t) a
→(arity
g
c
THeads (Flat Appl) (TCons t0 t1) (THead (Flat Cast) u t)
a))
that is equivalent to
arity g c (THeads (Flat Appl) (TCons t0 t1) u) (asucc g a)
→(arity g c (THeads (Flat Appl) (TCons t0 t1) t) a
→(arity
g
c
THeads (Flat Appl) (TCons t0 t1) (THead (Flat Cast) u t)
a))
∀a:A
.arity g c (THeads (Flat Appl) (TCons t0 t1) u) (asucc g a)
→(arity g c (THeads (Flat Appl) (TCons t0 t1) t) a
→(arity
g
c
THeads (Flat Appl) (TCons t0 t1) (THead (Flat Cast) u t)
a))
we proved
∀a:A
.arity g c (THeads (Flat Appl) vs u) (asucc g a)
→(arity g c (THeads (Flat Appl) vs t) a
→arity g c (THeads (Flat Appl) vs (THead (Flat Cast) u t)) a)
we proved
∀g:G
.∀c:C
.∀u:T
.∀t:T
.∀vs:TList
.∀a:A
.arity g c (THeads (Flat Appl) vs u) (asucc g a)
→(arity g c (THeads (Flat Appl) vs t) a
→arity g c (THeads (Flat Appl) vs (THead (Flat Cast) u t)) a)