DEFINITION arity_appls_appl()
TYPE =
∀g:G
.∀c:C
.∀v:T
.∀a1:A
.arity g c v a1
→∀u:T
.arity g c u (asucc g a1)
→∀t:T
.∀vs:TList
.∀a2:A
.arity g c (THeads (Flat Appl) vs (THead (Bind Abbr) v t)) a2
→(arity
g
c
THeads
Flat Appl
vs
THead (Flat Appl) v (THead (Bind Abst) u t)
a2)
BODY =
assume g: G
assume c: C
assume v: T
assume a1: A
suppose H: arity g c v a1
assume u: T
suppose H0: arity g c u (asucc g a1)
assume t: T
assume vs: TList
we proceed by induction on vs to prove
∀a2:A
.arity g c (THeads (Flat Appl) vs (THead (Bind Abbr) v t)) a2
→(arity
g
c
THeads
Flat Appl
vs
THead (Flat Appl) v (THead (Bind Abst) u t)
a2)
case TNil : ⇒
the thesis becomes
∀a2:A
.arity g c (THeads (Flat Appl) TNil (THead (Bind Abbr) v t)) a2
→(arity
g
c
THeads
Flat Appl
TNil
THead (Flat Appl) v (THead (Bind Abst) u t)
a2)
assume a2: A
we must prove
arity g c (THeads (Flat Appl) TNil (THead (Bind Abbr) v t)) a2
→(arity
g
c
THeads
Flat Appl
TNil
THead (Flat Appl) v (THead (Bind Abst) u t)
a2)
or equivalently
arity g c (THead (Bind Abbr) v t) a2
→(arity
g
c
THeads
Flat Appl
TNil
THead (Flat Appl) v (THead (Bind Abst) u t)
a2)
suppose H1: arity g c (THead (Bind Abbr) v t) a2
(H_x)
we must prove not (eq B Abbr Abst)
or equivalently (eq B Abbr Abst)→False
suppose H2: eq B Abbr Abst
by (not_abbr_abst H2)
we proved False
we proved (eq B Abbr Abst)→False
that is equivalent to not (eq B Abbr Abst)
by (arity_gen_bind . previous . . . . . H1)
ex2 A λa1:A.arity g c v a1 λ:A.arity g (CHead c (Bind Abbr) v) t a2
end of H_x
(H2) consider H_x
we proceed by induction on H2 to prove arity g c (THead (Flat Appl) v (THead (Bind Abst) u t)) a2
case ex_intro2 : x:A :arity g c v x H4:arity g (CHead c (Bind Abbr) v) t a2 ⇒
the thesis becomes arity g c (THead (Flat Appl) v (THead (Bind Abst) u t)) a2
(h1)
by (csuba_refl . .)
we proved csuba g c c
by (csuba_abst . . . previous . . H0 . H)
csuba g (CHead c (Bind Abst) u) (CHead c (Bind Abbr) v)
end of h1
(h2)
(h1)
by (csubv_refl .)
csubv c c
end of h1
(h2)
by (sym_not_eq . . . not_void_abst)
not (eq B Abst Void)
end of h2
by (csubv_bind . . h1 . h2 . . .)
csubv (CHead c (Bind Abst) u) (CHead c (Bind Abbr) v)
end of h2
by (csuba_arity_rev . . . . H4 . h1 h2)
we proved arity g (CHead c (Bind Abst) u) t a2
by (arity_head . . . . H0 . . previous)
we proved arity g c (THead (Bind Abst) u t) (AHead a1 a2)
by (arity_appl . . . . H . . previous)
arity g c (THead (Flat Appl) v (THead (Bind Abst) u t)) a2
we proved arity g c (THead (Flat Appl) v (THead (Bind Abst) u t)) a2
that is equivalent to
arity
g
c
THeads
Flat Appl
TNil
THead (Flat Appl) v (THead (Bind Abst) u t)
a2
we proved
arity g c (THead (Bind Abbr) v t) a2
→(arity
g
c
THeads
Flat Appl
TNil
THead (Flat Appl) v (THead (Bind Abst) u t)
a2)
that is equivalent to
arity g c (THeads (Flat Appl) TNil (THead (Bind Abbr) v t)) a2
→(arity
g
c
THeads
Flat Appl
TNil
THead (Flat Appl) v (THead (Bind Abst) u t)
a2)
∀a2:A
.arity g c (THeads (Flat Appl) TNil (THead (Bind Abbr) v t)) a2
→(arity
g
c
THeads
Flat Appl
TNil
THead (Flat Appl) v (THead (Bind Abst) u t)
a2)
case TCons : t0:T t1:TList ⇒
the thesis becomes
∀a2:A
.(arity
g
c
THeads (Flat Appl) (TCons t0 t1) (THead (Bind Abbr) v t)
a2)
→(arity
g
c
THeads
Flat Appl
TCons t0 t1
THead (Flat Appl) v (THead (Bind Abst) u t)
a2)
(H1) by induction hypothesis we know
∀a2:A
.arity g c (THeads (Flat Appl) t1 (THead (Bind Abbr) v t)) a2
→(arity
g
c
THeads
Flat Appl
t1
THead (Flat Appl) v (THead (Bind Abst) u t)
a2)
assume a2: A
we must prove
(arity
g
c
THeads (Flat Appl) (TCons t0 t1) (THead (Bind Abbr) v t)
a2)
→(arity
g
c
THeads
Flat Appl
TCons t0 t1
THead (Flat Appl) v (THead (Bind Abst) u t)
a2)
or equivalently
(arity
g
c
THead
Flat Appl
t0
THeads (Flat Appl) t1 (THead (Bind Abbr) v t)
a2)
→(arity
g
c
THeads
Flat Appl
TCons t0 t1
THead (Flat Appl) v (THead (Bind Abst) u t)
a2)
suppose H2:
arity
g
c
THead
Flat Appl
t0
THeads (Flat Appl) t1 (THead (Bind Abbr) v t)
a2
(H3)
by (arity_gen_appl . . . . . H2)
ex2
A
λa1:A.arity g c t0 a1
λa1:A
.arity
g
c
THeads (Flat Appl) t1 (THead (Bind Abbr) v t)
AHead a1 a2
end of H3
we proceed by induction on H3 to prove
arity
g
c
THead
Flat Appl
t0
THeads
Flat Appl
t1
THead (Flat Appl) v (THead (Bind Abst) u t)
a2
case ex_intro2 : x:A H4:arity g c t0 x H5:arity g c (THeads (Flat Appl) t1 (THead (Bind Abbr) v t)) (AHead x a2) ⇒
the thesis becomes
arity
g
c
THead
Flat Appl
t0
THeads
Flat Appl
t1
THead (Flat Appl) v (THead (Bind Abst) u t)
a2
by (H1 . H5)
we proved
arity
g
c
THeads
Flat Appl
t1
THead (Flat Appl) v (THead (Bind Abst) u t)
AHead x a2
by (arity_appl . . . . H4 . . previous)
arity
g
c
THead
Flat Appl
t0
THeads
Flat Appl
t1
THead (Flat Appl) v (THead (Bind Abst) u t)
a2
we proved
arity
g
c
THead
Flat Appl
t0
THeads
Flat Appl
t1
THead (Flat Appl) v (THead (Bind Abst) u t)
a2
that is equivalent to
arity
g
c
THeads
Flat Appl
TCons t0 t1
THead (Flat Appl) v (THead (Bind Abst) u t)
a2
we proved
(arity
g
c
THead
Flat Appl
t0
THeads (Flat Appl) t1 (THead (Bind Abbr) v t)
a2)
→(arity
g
c
THeads
Flat Appl
TCons t0 t1
THead (Flat Appl) v (THead (Bind Abst) u t)
a2)
that is equivalent to
(arity
g
c
THeads (Flat Appl) (TCons t0 t1) (THead (Bind Abbr) v t)
a2)
→(arity
g
c
THeads
Flat Appl
TCons t0 t1
THead (Flat Appl) v (THead (Bind Abst) u t)
a2)
∀a2:A
.(arity
g
c
THeads (Flat Appl) (TCons t0 t1) (THead (Bind Abbr) v t)
a2)
→(arity
g
c
THeads
Flat Appl
TCons t0 t1
THead (Flat Appl) v (THead (Bind Abst) u t)
a2)
we proved
∀a2:A
.arity g c (THeads (Flat Appl) vs (THead (Bind Abbr) v t)) a2
→(arity
g
c
THeads
Flat Appl
vs
THead (Flat Appl) v (THead (Bind Abst) u t)
a2)
we proved
∀g:G
.∀c:C
.∀v:T
.∀a1:A
.arity g c v a1
→∀u:T
.arity g c u (asucc g a1)
→∀t:T
.∀vs:TList
.∀a2:A
.arity g c (THeads (Flat Appl) vs (THead (Bind Abbr) v t)) a2
→(arity
g
c
THeads
Flat Appl
vs
THead (Flat Appl) v (THead (Bind Abst) u t)
a2)