DEFINITION sc3_props__sc3_sn3_abst()
TYPE =
∀g:G
.∀a:A
.land
∀c:C.∀t:T.(sc3 g a c t)→(sn3 c t)
∀vs:TList
.∀i:nat
.let t := THeads (Flat Appl) vs (TLRef i)
in ∀c:C.(arity g c t a)→(nf2 c (TLRef i))→(sns3 c vs)→(sc3 g a c t)
BODY =
assume g: G
assume a: A
we proceed by induction on a to prove
land
∀c:C.∀t:T.(sc3 g a c t)→(sn3 c t)
∀vs:TList
.∀i:nat
.let t := THeads (Flat Appl) vs (TLRef i)
in ∀c:C.(arity g c t a)→(nf2 c (TLRef i))→(sns3 c vs)→(sc3 g a c t)
case ASort : n:nat n0:nat ⇒
the thesis becomes
land
∀c:C.∀t:T.(sc3 g (ASort n n0) c t)→(sn3 c t)
∀vs:TList
.∀i:nat
.let t := THeads (Flat Appl) vs (TLRef i)
in ∀c:C
.arity g c t (ASort n n0)
→(nf2 c (TLRef i))→(sns3 c vs)→(sc3 g (ASort n n0) c t)
(h1)
assume c: C
assume t: T
suppose H: land (arity g c t (ASort n n0)) (sn3 c t)
(H0) consider H
we proceed by induction on H0 to prove sn3 c t
case conj : :arity g c t (ASort n n0) H2:sn3 c t ⇒
the thesis becomes the hypothesis H2
we proved sn3 c t
∀c:C.∀t:T.(land (arity g c t (ASort n n0)) (sn3 c t))→(sn3 c t)
end of h1
(h2)
assume vs: TList
assume i: nat
assume c: C
suppose H: arity g c (THeads (Flat Appl) vs (TLRef i)) (ASort n n0)
suppose H0: nf2 c (TLRef i)
suppose H1: sns3 c vs
by (sn3_appls_lref . . H0 . H1)
we proved sn3 c (THeads (Flat Appl) vs (TLRef i))
by (conj . . H previous)
we proved
land
arity g c (THeads (Flat Appl) vs (TLRef i)) (ASort n n0)
sn3 c (THeads (Flat Appl) vs (TLRef i))
∀vs:TList
.∀i:nat
.∀c:C
.arity g c (THeads (Flat Appl) vs (TLRef i)) (ASort n n0)
→(nf2 c (TLRef i)
→(sns3 c vs
→(land
arity g c (THeads (Flat Appl) vs (TLRef i)) (ASort n n0)
sn3 c (THeads (Flat Appl) vs (TLRef i)))))
end of h2
by (conj . . h1 h2)
we proved
land
∀c:C.∀t:T.(land (arity g c t (ASort n n0)) (sn3 c t))→(sn3 c t)
∀vs:TList
.∀i:nat
.∀c:C
.arity g c (THeads (Flat Appl) vs (TLRef i)) (ASort n n0)
→(nf2 c (TLRef i)
→(sns3 c vs
→(land
arity g c (THeads (Flat Appl) vs (TLRef i)) (ASort n n0)
sn3 c (THeads (Flat Appl) vs (TLRef i)))))
land
∀c:C.∀t:T.(sc3 g (ASort n n0) c t)→(sn3 c t)
∀vs:TList
.∀i:nat
.let t := THeads (Flat Appl) vs (TLRef i)
in ∀c:C
.arity g c t (ASort n n0)
→(nf2 c (TLRef i))→(sns3 c vs)→(sc3 g (ASort n n0) c t)
case AHead : a0:A a1:A ⇒
the thesis becomes
land
∀c:C.∀t:T.(sc3 g (AHead a0 a1) c t)→(sn3 c t)
∀vs:TList
.∀i:nat
.let t := THeads (Flat Appl) vs (TLRef i)
in ∀c:C
.arity g c t (AHead a0 a1)
→(nf2 c (TLRef i))→(sns3 c vs)→(sc3 g (AHead a0 a1) c t)
(H) by induction hypothesis we know
land
∀c:C.∀t:T.(sc3 g a0 c t)→(sn3 c t)
∀vs:TList
.∀i:nat
.∀c:C
.arity g c (THeads (Flat Appl) vs (TLRef i)) a0
→(nf2 c (TLRef i)
→(sns3 c vs)→(sc3 g a0 c (THeads (Flat Appl) vs (TLRef i))))
(H0) by induction hypothesis we know
land
∀c:C.∀t:T.(sc3 g a1 c t)→(sn3 c t)
∀vs:TList
.∀i:nat
.∀c:C
.arity g c (THeads (Flat Appl) vs (TLRef i)) a1
→(nf2 c (TLRef i)
→(sns3 c vs)→(sc3 g a1 c (THeads (Flat Appl) vs (TLRef i))))
(h1)
assume c: C
assume t: T
suppose H1:
land
arity g c t (AHead a0 a1)
∀d:C
.∀w:T
.sc3 g a0 d w
→∀is:PList.(drop1 is d c)→(sc3 g a1 d (THead (Flat Appl) w (lift1 is t)))
(H2) consider H
we proceed by induction on H2 to prove sn3 c t
case conj : :∀c0:C.∀t0:T.(sc3 g a0 c0 t0)→(sn3 c0 t0) H4:∀vs:TList.∀i:nat.∀c0:C.(arity g c0 (THeads (Flat Appl) vs (TLRef i)) a0)→(nf2 c0 (TLRef i))→(sns3 c0 vs)→(sc3 g a0 c0 (THeads (Flat Appl) vs (TLRef i))) ⇒
the thesis becomes sn3 c t
(H5) consider H0
we proceed by induction on H5 to prove sn3 c t
case conj : H6:∀c0:C.∀t0:T.(sc3 g a1 c0 t0)→(sn3 c0 t0) :∀vs:TList.∀i:nat.∀c0:C.(arity g c0 (THeads (Flat Appl) vs (TLRef i)) a1)→(nf2 c0 (TLRef i))→(sns3 c0 vs)→(sc3 g a1 c0 (THeads (Flat Appl) vs (TLRef i))) ⇒
the thesis becomes sn3 c t
(H8) consider H1
we proceed by induction on H8 to prove sn3 c t
case conj : H9:arity g c t (AHead a0 a1) H10:∀d:C.∀w:T.(sc3 g a0 d w)→∀is:PList.(drop1 is d c)→(sc3 g a1 d (THead (Flat Appl) w (lift1 is t))) ⇒
the thesis becomes sn3 c t
(H_y)
by (arity_aprem . . . . H9 . .)
aprem O (AHead a0 a1) a0
→(ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (plus O j) O d c
λd:C.λu:T.λ:nat.arity g d u (asucc g a0))
end of H_y
(H11)
by (aprem_zero . .)
we proved aprem O (AHead a0 a1) a0
by (H_y previous)
ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (plus O j) O d c
λd:C.λu:T.λ:nat.arity g d u (asucc g a0)
end of H11
consider H11
we proved
ex2_3
C
T
nat
λd:C.λ:T.λj:nat.drop (plus O j) O d c
λd:C.λu:T.λ:nat.arity g d u (asucc g a0)
that is equivalent to ex2_3 C T nat λd:C.λ:T.λj:nat.drop j O d c λd:C.λu:T.λ:nat.arity g d u (asucc g a0)
we proceed by induction on the previous result to prove sn3 c t
case ex2_3_intro : x0:C x1:T x2:nat H12:drop x2 O x0 c H13:arity g x0 x1 (asucc g a0) ⇒
the thesis becomes sn3 c t
(H_y0)
(h1)
by (getl_refl . . .)
we proved getl O (CHead x0 (Bind Abst) x1) (CHead x0 (Bind Abst) x1)
by (arity_abst . . . . . previous . H13)
we proved arity g (CHead x0 (Bind Abst) x1) (TLRef O) a0
arity
g
CHead x0 (Bind Abst) x1
THeads (Flat Appl) TNil (TLRef O)
a0
end of h1
(h2)
by (getl_refl . . .)
we proved getl O (CHead x0 (Bind Abst) x1) (CHead x0 (Bind Abst) x1)
by (nf2_lref_abst . . . . previous)
nf2 (CHead x0 (Bind Abst) x1) (TLRef O)
end of h2
(h3)
consider I
we proved True
sns3 (CHead x0 (Bind Abst) x1) TNil
end of h3
by (H4 . . . h1 h2 h3)
we proved
sc3
g
a0
CHead x0 (Bind Abst) x1
THeads (Flat Appl) TNil (TLRef O)
that is equivalent to sc3 g a0 (CHead x0 (Bind Abst) x1) (TLRef O)
by (H10 . . previous .)
drop1 (PCons (S x2) O PNil) (CHead x0 (Bind Abst) x1) c
→(sc3
g
a1
CHead x0 (Bind Abst) x1
THead (Flat Appl) (TLRef O) (lift1 (PCons (S x2) O PNil) t))
end of H_y0
(H_y1)
(h1)
consider H12
we proved drop x2 O x0 c
that is equivalent to drop (r (Bind Abst) x2) O x0 c
by (drop_drop . . . . previous .)
drop (S x2) O (CHead x0 (Bind Abst) x1) c
end of h1
(h2)
by (drop1_nil .)
drop1 PNil c c
end of h2
by (drop1_cons . . . . h1 . . h2)
we proved drop1 (PCons (S x2) O PNil) (CHead x0 (Bind Abst) x1) c
by (H_y0 previous)
we proved
sc3
g
a1
CHead x0 (Bind Abst) x1
THead (Flat Appl) (TLRef O) (lift1 (PCons (S x2) O PNil) t)
that is equivalent to
sc3
g
a1
CHead x0 (Bind Abst) x1
THead (Flat Appl) (TLRef O) (lift (S x2) O t)
by (H6 . . previous)
sn3
CHead x0 (Bind Abst) x1
THead (Flat Appl) (TLRef O) (lift (S x2) O t)
end of H_y1
(H_x)
by (sn3_gen_flat . . . . H_y1)
land
sn3 (CHead x0 (Bind Abst) x1) (TLRef O)
sn3 (CHead x0 (Bind Abst) x1) (lift (S x2) O t)
end of H_x
(H14) consider H_x
we proceed by induction on H14 to prove sn3 c t
case conj : :sn3 (CHead x0 (Bind Abst) x1) (TLRef O) H16:sn3 (CHead x0 (Bind Abst) x1) (lift (S x2) O t) ⇒
the thesis becomes sn3 c t
consider H12
we proved drop x2 O x0 c
that is equivalent to drop (r (Bind Abst) x2) O x0 c
by (drop_drop . . . . previous .)
we proved drop (S x2) O (CHead x0 (Bind Abst) x1) c
by (sn3_gen_lift . . . . H16 . previous)
sn3 c t
sn3 c t
sn3 c t
sn3 c t
sn3 c t
we proved sn3 c t
∀c:C
.∀t:T
.(land
arity g c t (AHead a0 a1)
∀d:C
.∀w:T
.sc3 g a0 d w
→∀is:PList.(drop1 is d c)→(sc3 g a1 d (THead (Flat Appl) w (lift1 is t))))
→sn3 c t
end of h1
(h2)
assume vs: TList
assume i: nat
assume c: C
suppose H1: arity g c (THeads (Flat Appl) vs (TLRef i)) (AHead a0 a1)
suppose H2: nf2 c (TLRef i)
suppose H3: sns3 c vs
assume d: C
assume w: T
suppose H4: sc3 g a0 d w
assume is: PList
suppose H5: drop1 is d c
(H6) consider H
we proceed by induction on H6 to prove
sc3
g
a1
d
THead
Flat Appl
w
lift1 is (THeads (Flat Appl) vs (TLRef i))
case conj : H7:∀c0:C.∀t:T.(sc3 g a0 c0 t)→(sn3 c0 t) :∀vs0:TList.∀i0:nat.∀c0:C.(arity g c0 (THeads (Flat Appl) vs0 (TLRef i0)) a0)→(nf2 c0 (TLRef i0))→(sns3 c0 vs0)→(sc3 g a0 c0 (THeads (Flat Appl) vs0 (TLRef i0))) ⇒
the thesis becomes
sc3
g
a1
d
THead
Flat Appl
w
lift1 is (THeads (Flat Appl) vs (TLRef i))
(H9) consider H0
we proceed by induction on H9 to prove
sc3
g
a1
d
THead
Flat Appl
w
lift1 is (THeads (Flat Appl) vs (TLRef i))
case conj : :∀c0:C.∀t:T.(sc3 g a1 c0 t)→(sn3 c0 t) H11:∀vs0:TList.∀i0:nat.∀c0:C.(arity g c0 (THeads (Flat Appl) vs0 (TLRef i0)) a1)→(nf2 c0 (TLRef i0))→(sns3 c0 vs0)→(sc3 g a1 c0 (THeads (Flat Appl) vs0 (TLRef i0))) ⇒
the thesis becomes
sc3
g
a1
d
THead
Flat Appl
w
lift1 is (THeads (Flat Appl) vs (TLRef i))
(H_y)
by (H11 .)
∀i0:nat
.∀c0:C
.arity g c0 (THeads (Flat Appl) (TCons w (lifts1 is vs)) (TLRef i0)) a1
→(nf2 c0 (TLRef i0)
→(sns3 c0 (TCons w (lifts1 is vs))
→sc3 g a1 c0 (THeads (Flat Appl) (TCons w (lifts1 is vs)) (TLRef i0))))
end of H_y
(h1)
(h1)
(h1)
by (lift1_lref . .)
we proved eq T (lift1 is (TLRef i)) (TLRef (trans is i))
we proceed by induction on the previous result to prove
arity
g
d
THead
Flat Appl
w
THeads (Flat Appl) (lifts1 is vs) (TLRef (trans is i))
a1
case refl_equal : ⇒
the thesis becomes
arity
g
d
THead
Flat Appl
w
THeads (Flat Appl) (lifts1 is vs) (lift1 is (TLRef i))
a1
by (lifts1_flat . . . .)
we proved
eq
T
lift1 is (THeads (Flat Appl) vs (TLRef i))
THeads (Flat Appl) (lifts1 is vs) (lift1 is (TLRef i))
we proceed by induction on the previous result to prove
arity
g
d
THead
Flat Appl
w
THeads (Flat Appl) (lifts1 is vs) (lift1 is (TLRef i))
a1
case refl_equal : ⇒
the thesis becomes
arity
g
d
THead
Flat Appl
w
lift1 is (THeads (Flat Appl) vs (TLRef i))
a1
(h1)
by (sc3_arity_gen . . . . H4)
arity g d w a0
end of h1
(h2)
by (arity_lift1 . . . . . . H5 H1)
arity g d (lift1 is (THeads (Flat Appl) vs (TLRef i))) (AHead a0 a1)
end of h2
by (arity_appl . . . . h1 . . h2)
arity
g
d
THead
Flat Appl
w
lift1 is (THeads (Flat Appl) vs (TLRef i))
a1
arity
g
d
THead
Flat Appl
w
THeads (Flat Appl) (lifts1 is vs) (lift1 is (TLRef i))
a1
we proved
arity
g
d
THead
Flat Appl
w
THeads (Flat Appl) (lifts1 is vs) (TLRef (trans is i))
a1
arity
g
d
THeads (Flat Appl) (TCons w (lifts1 is vs)) (TLRef (trans is i))
a1
end of h1
(h2)
by (lift1_lref . .)
we proved eq T (lift1 is (TLRef i)) (TLRef (trans is i))
we proceed by induction on the previous result to prove nf2 d (TLRef (trans is i))
case refl_equal : ⇒
the thesis becomes nf2 d (lift1 is (TLRef i))
by (nf2_lift1 . . . . H5 H2)
nf2 d (lift1 is (TLRef i))
nf2 d (TLRef (trans is i))
end of h2
(h3)
(h1) by (H7 . . H4) we proved sn3 d w
(h2)
by (sns3_lifts1 . . . H5 . H3)
sns3 d (lifts1 is vs)
end of h2
by (conj . . h1 h2)
we proved land (sn3 d w) (sns3 d (lifts1 is vs))
sns3 d (TCons w (lifts1 is vs))
end of h3
by (H_y . . h1 h2 h3)
we proved
sc3
g
a1
d
THeads (Flat Appl) (TCons w (lifts1 is vs)) (TLRef (trans is i))
sc3
g
a1
d
THead
Flat Appl
w
THeads (Flat Appl) (lifts1 is vs) (TLRef (trans is i))
end of h1
(h2)
by (lift1_lref . .)
eq T (lift1 is (TLRef i)) (TLRef (trans is i))
end of h2
by (eq_ind_r . . . h1 . h2)
sc3
g
a1
d
THead
Flat Appl
w
THeads (Flat Appl) (lifts1 is vs) (lift1 is (TLRef i))
end of h1
(h2)
by (lifts1_flat . . . .)
eq
T
lift1 is (THeads (Flat Appl) vs (TLRef i))
THeads (Flat Appl) (lifts1 is vs) (lift1 is (TLRef i))
end of h2
by (eq_ind_r . . . h1 . h2)
sc3
g
a1
d
THead
Flat Appl
w
lift1 is (THeads (Flat Appl) vs (TLRef i))
sc3
g
a1
d
THead
Flat Appl
w
lift1 is (THeads (Flat Appl) vs (TLRef i))
we proved
sc3
g
a1
d
THead
Flat Appl
w
lift1 is (THeads (Flat Appl) vs (TLRef i))
we proved
∀d:C
.∀w:T
.sc3 g a0 d w
→∀is:PList
.drop1 is d c
→(sc3
g
a1
d
THead
Flat Appl
w
lift1 is (THeads (Flat Appl) vs (TLRef i)))
by (conj . . H1 previous)
we proved
land
arity g c (THeads (Flat Appl) vs (TLRef i)) (AHead a0 a1)
∀d:C
.∀w:T
.sc3 g a0 d w
→∀is:PList
.drop1 is d c
→(sc3
g
a1
d
THead
Flat Appl
w
lift1 is (THeads (Flat Appl) vs (TLRef i)))
∀vs:TList
.∀i:nat
.∀c:C
.arity g c (THeads (Flat Appl) vs (TLRef i)) (AHead a0 a1)
→(nf2 c (TLRef i)
→(sns3 c vs
→(land
arity g c (THeads (Flat Appl) vs (TLRef i)) (AHead a0 a1)
∀d:C
.∀w:T
.sc3 g a0 d w
→∀is:PList
.drop1 is d c
→(sc3
g
a1
d
THead
Flat Appl
w
lift1 is (THeads (Flat Appl) vs (TLRef i))))))
end of h2
by (conj . . h1 h2)
we proved
land
∀c:C
.∀t:T
.(land
arity g c t (AHead a0 a1)
∀d:C
.∀w:T
.sc3 g a0 d w
→∀is:PList.(drop1 is d c)→(sc3 g a1 d (THead (Flat Appl) w (lift1 is t))))
→sn3 c t
∀vs:TList
.∀i:nat
.∀c:C
.arity g c (THeads (Flat Appl) vs (TLRef i)) (AHead a0 a1)
→(nf2 c (TLRef i)
→(sns3 c vs
→(land
arity g c (THeads (Flat Appl) vs (TLRef i)) (AHead a0 a1)
∀d:C
.∀w:T
.sc3 g a0 d w
→∀is:PList
.drop1 is d c
→(sc3
g
a1
d
THead
Flat Appl
w
lift1 is (THeads (Flat Appl) vs (TLRef i))))))
land
∀c:C.∀t:T.(sc3 g (AHead a0 a1) c t)→(sn3 c t)
∀vs:TList
.∀i:nat
.let t := THeads (Flat Appl) vs (TLRef i)
in ∀c:C
.arity g c t (AHead a0 a1)
→(nf2 c (TLRef i))→(sns3 c vs)→(sc3 g (AHead a0 a1) c t)
we proved
land
∀c:C.∀t:T.(sc3 g a c t)→(sn3 c t)
∀vs:TList
.∀i:nat
.let t := THeads (Flat Appl) vs (TLRef i)
in ∀c:C.(arity g c t a)→(nf2 c (TLRef i))→(sns3 c vs)→(sc3 g a c t)
we proved
∀g:G
.∀a:A
.land
∀c:C.∀t:T.(sc3 g a c t)→(sn3 c t)
∀vs:TList
.∀i:nat
.let t := THeads (Flat Appl) vs (TLRef i)
in ∀c:C.(arity g c t a)→(nf2 c (TLRef i))→(sns3 c vs)→(sc3 g a c t)