DEFINITION sc3_appl()
TYPE =
∀g:G
.∀a1:A
.∀a2:A
.∀vs:TList
.∀c:C
.∀v:T
.∀t:T
.sc3 g a2 c (THeads (Flat Appl) vs (THead (Bind Abbr) v t))
→(sc3 g a1 c v
→∀w:T
.sc3 g (asucc g a1) c w
→(sc3
g
a2
c
THeads
Flat Appl
vs
THead (Flat Appl) v (THead (Bind Abst) w t)))
BODY =
assume g: G
assume a1: A
assume a2: A
we proceed by induction on a2 to prove
∀vs:TList
.∀c:C
.∀v:T
.∀t:T
.sc3 g a2 c (THeads (Flat Appl) vs (THead (Bind Abbr) v t))
→(sc3 g a1 c v
→∀w:T
.sc3 g (asucc g a1) c w
→(sc3
g
a2
c
THeads
Flat Appl
vs
THead (Flat Appl) v (THead (Bind Abst) w t)))
case ASort : n:nat n0:nat ⇒
the thesis becomes
∀vs:TList
.∀c:C
.∀v:T
.∀t:T
.(sc3
g
ASort n n0
c
THeads (Flat Appl) vs (THead (Bind Abbr) v t))
→(sc3 g a1 c v
→∀w:T
.sc3 g (asucc g a1) c w
→(sc3
g
ASort n n0
c
THeads
Flat Appl
vs
THead (Flat Appl) v (THead (Bind Abst) w t)))
assume vs: TList
assume c: C
assume v: T
assume t: T
we must prove
(sc3
g
ASort n n0
c
THeads (Flat Appl) vs (THead (Bind Abbr) v t))
→(sc3 g a1 c v
→∀w:T
.sc3 g (asucc g a1) c w
→(sc3
g
ASort n n0
c
THeads
Flat Appl
vs
THead (Flat Appl) v (THead (Bind Abst) w t)))
or equivalently
(land
arity
g
c
THeads (Flat Appl) vs (THead (Bind Abbr) v t)
ASort n n0
sn3 c (THeads (Flat Appl) vs (THead (Bind Abbr) v t)))
→(sc3 g a1 c v
→∀w:T
.sc3 g (asucc g a1) c w
→(sc3
g
ASort n n0
c
THeads
Flat Appl
vs
THead (Flat Appl) v (THead (Bind Abst) w t)))
suppose H:
land
arity
g
c
THeads (Flat Appl) vs (THead (Bind Abbr) v t)
ASort n n0
sn3 c (THeads (Flat Appl) vs (THead (Bind Abbr) v t))
suppose H0: sc3 g a1 c v
assume w: T
suppose H1: sc3 g (asucc g a1) c w
(H2) consider H
we proceed by induction on H2 to prove
land
arity
g
c
THeads
Flat Appl
vs
THead (Flat Appl) v (THead (Bind Abst) w t)
ASort n n0
sn3
c
THeads
Flat Appl
vs
THead (Flat Appl) v (THead (Bind Abst) w t)
case conj : H3:arity g c (THeads (Flat Appl) vs (THead (Bind Abbr) v t)) (ASort n n0) H4:sn3 c (THeads (Flat Appl) vs (THead (Bind Abbr) v t)) ⇒
the thesis becomes
land
arity
g
c
THeads
Flat Appl
vs
THead (Flat Appl) v (THead (Bind Abst) w t)
ASort n n0
sn3
c
THeads
Flat Appl
vs
THead (Flat Appl) v (THead (Bind Abst) w t)
(h1)
(h1)
by (sc3_arity_gen . . . . H0)
arity g c v a1
end of h1
(h2)
by (sc3_arity_gen . . . . H1)
arity g c w (asucc g a1)
end of h2
by (arity_appls_appl . . . . h1 . h2 . . . H3)
arity
g
c
THeads
Flat Appl
vs
THead (Flat Appl) v (THead (Bind Abst) w t)
ASort n n0
end of h1
(h2)
by (sc3_sn3 . . . . H1)
we proved sn3 c w
by (sn3_appls_beta . . . . H4 . previous)
sn3
c
THeads
Flat Appl
vs
THead (Flat Appl) v (THead (Bind Abst) w t)
end of h2
by (conj . . h1 h2)
land
arity
g
c
THeads
Flat Appl
vs
THead (Flat Appl) v (THead (Bind Abst) w t)
ASort n n0
sn3
c
THeads
Flat Appl
vs
THead (Flat Appl) v (THead (Bind Abst) w t)
we proved
land
arity
g
c
THeads
Flat Appl
vs
THead (Flat Appl) v (THead (Bind Abst) w t)
ASort n n0
sn3
c
THeads
Flat Appl
vs
THead (Flat Appl) v (THead (Bind Abst) w t)
that is equivalent to
sc3
g
ASort n n0
c
THeads
Flat Appl
vs
THead (Flat Appl) v (THead (Bind Abst) w t)
we proved
(land
arity
g
c
THeads (Flat Appl) vs (THead (Bind Abbr) v t)
ASort n n0
sn3 c (THeads (Flat Appl) vs (THead (Bind Abbr) v t)))
→(sc3 g a1 c v
→∀w:T
.sc3 g (asucc g a1) c w
→(sc3
g
ASort n n0
c
THeads
Flat Appl
vs
THead (Flat Appl) v (THead (Bind Abst) w t)))
that is equivalent to
(sc3
g
ASort n n0
c
THeads (Flat Appl) vs (THead (Bind Abbr) v t))
→(sc3 g a1 c v
→∀w:T
.sc3 g (asucc g a1) c w
→(sc3
g
ASort n n0
c
THeads
Flat Appl
vs
THead (Flat Appl) v (THead (Bind Abst) w t)))
∀vs:TList
.∀c:C
.∀v:T
.∀t:T
.(sc3
g
ASort n n0
c
THeads (Flat Appl) vs (THead (Bind Abbr) v t))
→(sc3 g a1 c v
→∀w:T
.sc3 g (asucc g a1) c w
→(sc3
g
ASort n n0
c
THeads
Flat Appl
vs
THead (Flat Appl) v (THead (Bind Abst) w t)))
case AHead : a:A a0:A ⇒
the thesis becomes
∀vs:TList
.∀c:C
.∀v:T
.∀t:T
.(sc3
g
AHead a a0
c
THeads (Flat Appl) vs (THead (Bind Abbr) v t))
→(sc3 g a1 c v
→∀w:T
.sc3 g (asucc g a1) c w
→(sc3
g
AHead a a0
c
THeads
Flat Appl
vs
THead (Flat Appl) v (THead (Bind Abst) w t)))
() by induction hypothesis we know
∀vs:TList
.∀c:C
.∀v:T
.∀t:T
.sc3 g a c (THeads (Flat Appl) vs (THead (Bind Abbr) v t))
→(sc3 g a1 c v
→∀w:T
.sc3 g (asucc g a1) c w
→(sc3
g
a
c
THeads
Flat Appl
vs
THead (Flat Appl) v (THead (Bind Abst) w t)))
(H0) by induction hypothesis we know
∀vs:TList
.∀c:C
.∀v:T
.∀t:T
.sc3 g a0 c (THeads (Flat Appl) vs (THead (Bind Abbr) v t))
→(sc3 g a1 c v
→∀w:T
.sc3 g (asucc g a1) c w
→(sc3
g
a0
c
THeads
Flat Appl
vs
THead (Flat Appl) v (THead (Bind Abst) w t)))
assume vs: TList
assume c: C
assume v: T
assume t: T
we must prove
(sc3
g
AHead a a0
c
THeads (Flat Appl) vs (THead (Bind Abbr) v t))
→(sc3 g a1 c v
→∀w:T
.sc3 g (asucc g a1) c w
→(sc3
g
AHead a a0
c
THeads
Flat Appl
vs
THead (Flat Appl) v (THead (Bind Abst) w t)))
or equivalently
(land
arity
g
c
THeads (Flat Appl) vs (THead (Bind Abbr) v t)
AHead a a0
∀d:C
.∀w:T
.sc3 g a d w
→∀is:PList
.drop1 is d c
→(sc3
g
a0
d
THead
Flat Appl
w
lift1 is (THeads (Flat Appl) vs (THead (Bind Abbr) v t))))
→(sc3 g a1 c v
→∀w:T
.sc3 g (asucc g a1) c w
→(sc3
g
AHead a a0
c
THeads
Flat Appl
vs
THead (Flat Appl) v (THead (Bind Abst) w t)))
suppose H1:
land
arity
g
c
THeads (Flat Appl) vs (THead (Bind Abbr) v t)
AHead a a0
∀d:C
.∀w:T
.sc3 g a d w
→∀is:PList
.drop1 is d c
→(sc3
g
a0
d
THead
Flat Appl
w
lift1 is (THeads (Flat Appl) vs (THead (Bind Abbr) v t)))
suppose H2: sc3 g a1 c v
assume w: T
suppose H3: sc3 g (asucc g a1) c w
(H4) consider H1
we proceed by induction on H4 to prove
land
arity
g
c
THeads
Flat Appl
vs
THead (Flat Appl) v (THead (Bind Abst) w t)
AHead a a0
∀d:C
.∀w0:T
.sc3 g a d w0
→∀is:PList
.drop1 is d c
→(sc3
g
a0
d
THead
Flat Appl
w0
lift1
is
THeads
Flat Appl
vs
THead (Flat Appl) v (THead (Bind Abst) w t))
case conj : H5:arity g c (THeads (Flat Appl) vs (THead (Bind Abbr) v t)) (AHead a a0) H6:∀d:C.∀w0:T.(sc3 g a d w0)→∀is:PList.(drop1 is d c)→(sc3 g a0 d (THead (Flat Appl) w0 (lift1 is (THeads (Flat Appl) vs (THead (Bind Abbr) v t))))) ⇒
the thesis becomes
land
arity
g
c
THeads
Flat Appl
vs
THead (Flat Appl) v (THead (Bind Abst) w t)
AHead a a0
∀d:C
.∀w0:T
.sc3 g a d w0
→∀is:PList
.drop1 is d c
→(sc3
g
a0
d
THead
Flat Appl
w0
lift1
is
THeads
Flat Appl
vs
THead (Flat Appl) v (THead (Bind Abst) w t))
(h1)
(h1)
by (sc3_arity_gen . . . . H2)
arity g c v a1
end of h1
(h2)
by (sc3_arity_gen . . . . H3)
arity g c w (asucc g a1)
end of h2
by (arity_appls_appl . . . . h1 . h2 . . . H5)
arity
g
c
THeads
Flat Appl
vs
THead (Flat Appl) v (THead (Bind Abst) w t)
AHead a a0
end of h1
(h2)
assume d: C
assume w0: T
suppose H7: sc3 g a d w0
assume is: PList
suppose H8: drop1 is d c
(h1)
(h1)
(h1)
(H_y)
by (H0 .)
∀c:C
.∀v:T
.∀t:T
.(sc3
g
a0
c
THeads
Flat Appl
TCons w0 (lifts1 is vs)
THead (Bind Abbr) v t)
→(sc3 g a1 c v
→∀w:T
.sc3 g (asucc g a1) c w
→(sc3
g
a0
c
THeads
Flat Appl
TCons w0 (lifts1 is vs)
THead (Flat Appl) v (THead (Bind Abst) w t)))
end of H_y
(h1)
by (lift1_bind . . . .)
we proved
eq
T
lift1 is (THead (Bind Abbr) v t)
THead (Bind Abbr) (lift1 is v) (lift1 (Ss is) t)
we proceed by induction on the previous result to prove
sc3
g
a0
d
THead
Flat Appl
w0
THeads
Flat Appl
lifts1 is vs
THead (Bind Abbr) (lift1 is v) (lift1 (Ss is) t)
case refl_equal : ⇒
the thesis becomes
sc3
g
a0
d
THead
Flat Appl
w0
THeads (Flat Appl) (lifts1 is vs) (lift1 is (THead (Bind Abbr) v t))
by (lifts1_flat . . . .)
we proved
eq
T
lift1 is (THeads (Flat Appl) vs (THead (Bind Abbr) v t))
THeads (Flat Appl) (lifts1 is vs) (lift1 is (THead (Bind Abbr) v t))
we proceed by induction on the previous result to prove
sc3
g
a0
d
THead
Flat Appl
w0
THeads (Flat Appl) (lifts1 is vs) (lift1 is (THead (Bind Abbr) v t))
case refl_equal : ⇒
the thesis becomes
sc3
g
a0
d
THead
Flat Appl
w0
lift1 is (THeads (Flat Appl) vs (THead (Bind Abbr) v t))
by (H6 . . H7 . H8)
sc3
g
a0
d
THead
Flat Appl
w0
lift1 is (THeads (Flat Appl) vs (THead (Bind Abbr) v t))
sc3
g
a0
d
THead
Flat Appl
w0
THeads (Flat Appl) (lifts1 is vs) (lift1 is (THead (Bind Abbr) v t))
we proved
sc3
g
a0
d
THead
Flat Appl
w0
THeads
Flat Appl
lifts1 is vs
THead (Bind Abbr) (lift1 is v) (lift1 (Ss is) t)
sc3
g
a0
d
THeads
Flat Appl
TCons w0 (lifts1 is vs)
THead (Bind Abbr) (lift1 is v) (lift1 (Ss is) t)
end of h1
(h2)
by (sc3_lift1 . . . . . . H2 H8)
sc3 g a1 d (lift1 is v)
end of h2
(h3)
by (sc3_lift1 . . . . . . H3 H8)
sc3 g (asucc g a1) d (lift1 is w)
end of h3
by (H_y . . . h1 h2 . h3)
we proved
sc3
g
a0
d
THeads
Flat Appl
TCons w0 (lifts1 is vs)
THead
Flat Appl
lift1 is v
THead (Bind Abst) (lift1 is w) (lift1 (Ss is) t)
sc3
g
a0
d
THead
Flat Appl
w0
THeads
Flat Appl
lifts1 is vs
THead
Flat Appl
lift1 is v
THead (Bind Abst) (lift1 is w) (lift1 (Ss is) t)
end of h1
(h2)
by (lift1_bind . . . .)
eq
T
lift1 is (THead (Bind Abst) w t)
THead (Bind Abst) (lift1 is w) (lift1 (Ss is) t)
end of h2
by (eq_ind_r . . . h1 . h2)
sc3
g
a0
d
THead
Flat Appl
w0
THeads
Flat Appl
lifts1 is vs
THead (Flat Appl) (lift1 is v) (lift1 is (THead (Bind Abst) w t))
end of h1
(h2)
by (lift1_flat . . . .)
eq
T
lift1 is (THead (Flat Appl) v (THead (Bind Abst) w t))
THead (Flat Appl) (lift1 is v) (lift1 is (THead (Bind Abst) w t))
end of h2
by (eq_ind_r . . . h1 . h2)
sc3
g
a0
d
THead
Flat Appl
w0
THeads
Flat Appl
lifts1 is vs
lift1 is (THead (Flat Appl) v (THead (Bind Abst) w t))
end of h1
(h2)
by (lifts1_flat . . . .)
eq
T
lift1
is
THeads
Flat Appl
vs
THead (Flat Appl) v (THead (Bind Abst) w t)
THeads
Flat Appl
lifts1 is vs
lift1 is (THead (Flat Appl) v (THead (Bind Abst) w t))
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
sc3
g
a0
d
THead
Flat Appl
w0
lift1
is
THeads
Flat Appl
vs
THead (Flat Appl) v (THead (Bind Abst) w t)
∀d:C
.∀w0:T
.sc3 g a d w0
→∀is:PList
.drop1 is d c
→(sc3
g
a0
d
THead
Flat Appl
w0
lift1
is
THeads
Flat Appl
vs
THead (Flat Appl) v (THead (Bind Abst) w t))
end of h2
by (conj . . h1 h2)
land
arity
g
c
THeads
Flat Appl
vs
THead (Flat Appl) v (THead (Bind Abst) w t)
AHead a a0
∀d:C
.∀w0:T
.sc3 g a d w0
→∀is:PList
.drop1 is d c
→(sc3
g
a0
d
THead
Flat Appl
w0
lift1
is
THeads
Flat Appl
vs
THead (Flat Appl) v (THead (Bind Abst) w t))
we proved
land
arity
g
c
THeads
Flat Appl
vs
THead (Flat Appl) v (THead (Bind Abst) w t)
AHead a a0
∀d:C
.∀w0:T
.sc3 g a d w0
→∀is:PList
.drop1 is d c
→(sc3
g
a0
d
THead
Flat Appl
w0
lift1
is
THeads
Flat Appl
vs
THead (Flat Appl) v (THead (Bind Abst) w t))
that is equivalent to
sc3
g
AHead a a0
c
THeads
Flat Appl
vs
THead (Flat Appl) v (THead (Bind Abst) w t)
we proved
(land
arity
g
c
THeads (Flat Appl) vs (THead (Bind Abbr) v t)
AHead a a0
∀d:C
.∀w:T
.sc3 g a d w
→∀is:PList
.drop1 is d c
→(sc3
g
a0
d
THead
Flat Appl
w
lift1 is (THeads (Flat Appl) vs (THead (Bind Abbr) v t))))
→(sc3 g a1 c v
→∀w:T
.sc3 g (asucc g a1) c w
→(sc3
g
AHead a a0
c
THeads
Flat Appl
vs
THead (Flat Appl) v (THead (Bind Abst) w t)))
that is equivalent to
(sc3
g
AHead a a0
c
THeads (Flat Appl) vs (THead (Bind Abbr) v t))
→(sc3 g a1 c v
→∀w:T
.sc3 g (asucc g a1) c w
→(sc3
g
AHead a a0
c
THeads
Flat Appl
vs
THead (Flat Appl) v (THead (Bind Abst) w t)))
∀vs:TList
.∀c:C
.∀v:T
.∀t:T
.(sc3
g
AHead a a0
c
THeads (Flat Appl) vs (THead (Bind Abbr) v t))
→(sc3 g a1 c v
→∀w:T
.sc3 g (asucc g a1) c w
→(sc3
g
AHead a a0
c
THeads
Flat Appl
vs
THead (Flat Appl) v (THead (Bind Abst) w t)))
we proved
∀vs:TList
.∀c:C
.∀v:T
.∀t:T
.sc3 g a2 c (THeads (Flat Appl) vs (THead (Bind Abbr) v t))
→(sc3 g a1 c v
→∀w:T
.sc3 g (asucc g a1) c w
→(sc3
g
a2
c
THeads
Flat Appl
vs
THead (Flat Appl) v (THead (Bind Abst) w t)))
we proved
∀g:G
.∀a1:A
.∀a2:A
.∀vs:TList
.∀c:C
.∀v:T
.∀t:T
.sc3 g a2 c (THeads (Flat Appl) vs (THead (Bind Abbr) v t))
→(sc3 g a1 c v
→∀w:T
.sc3 g (asucc g a1) c w
→(sc3
g
a2
c
THeads
Flat Appl
vs
THead (Flat Appl) v (THead (Bind Abst) w t)))