DEFINITION sn3_appls_abbr()
TYPE =
∀c:C
.∀d:C
.∀w:T
.∀i:nat
.getl i c (CHead d (Bind Abbr) w)
→∀vs:TList
.sn3 c (THeads (Flat Appl) vs (lift (S i) O w))
→sn3 c (THeads (Flat Appl) vs (TLRef i))
BODY =
assume c: C
assume d: C
assume w: T
assume i: nat
suppose H: getl i c (CHead d (Bind Abbr) w)
assume vs: TList
we proceed by induction on vs to prove
sn3 c (THeads (Flat Appl) vs (lift (S i) O w))
→sn3 c (THeads (Flat Appl) vs (TLRef i))
case TNil : ⇒
the thesis becomes
sn3 c (THeads (Flat Appl) TNil (lift (S i) O w))
→sn3 c (THeads (Flat Appl) TNil (TLRef i))
we must prove
sn3 c (THeads (Flat Appl) TNil (lift (S i) O w))
→sn3 c (THeads (Flat Appl) TNil (TLRef i))
or equivalently
sn3 c (lift (S i) O w)
→sn3 c (THeads (Flat Appl) TNil (TLRef i))
suppose H0: sn3 c (lift (S i) O w)
(H_y)
by (getl_drop . . . . . H)
we proved drop (S i) O c d
by (sn3_gen_lift . . . . H0 . previous)
sn3 d w
end of H_y
by (sn3_abbr . . . . H H_y)
we proved sn3 c (TLRef i)
that is equivalent to sn3 c (THeads (Flat Appl) TNil (TLRef i))
we proved
sn3 c (lift (S i) O w)
→sn3 c (THeads (Flat Appl) TNil (TLRef i))
sn3 c (THeads (Flat Appl) TNil (lift (S i) O w))
→sn3 c (THeads (Flat Appl) TNil (TLRef i))
case TCons ⇒
we need to prove
∀v:T
.∀vs0:TList
.sn3 c (THeads (Flat Appl) vs0 (lift (S i) O w))
→sn3 c (THeads (Flat Appl) vs0 (TLRef i))
→(sn3 c (THeads (Flat Appl) (TCons v vs0) (lift (S i) O w))
→sn3 c (THeads (Flat Appl) (TCons v vs0) (TLRef i)))
assume v: T
assume vs0: TList
we proceed by induction on vs0 to prove
sn3 c (THeads (Flat Appl) vs0 (lift (S i) O w))
→sn3 c (THeads (Flat Appl) vs0 (TLRef i))
→((sn3
c
THead (Flat Appl) v (THeads (Flat Appl) vs0 (lift (S i) O w)))
→sn3 c (THead (Flat Appl) v (THeads (Flat Appl) vs0 (TLRef i))))
case TNil : ⇒
the thesis becomes
sn3 c (THeads (Flat Appl) TNil (lift (S i) O w))
→sn3 c (THeads (Flat Appl) TNil (TLRef i))
→((sn3
c
THead
Flat Appl
v
THeads (Flat Appl) TNil (lift (S i) O w))
→(sn3
c
THead (Flat Appl) v (THeads (Flat Appl) TNil (TLRef i))))
suppose :
sn3 c (THeads (Flat Appl) TNil (lift (S i) O w))
→sn3 c (THeads (Flat Appl) TNil (TLRef i))
suppose H1:
sn3
c
THead
Flat Appl
v
THeads (Flat Appl) TNil (lift (S i) O w)
consider H1
we proved
sn3
c
THead
Flat Appl
v
THeads (Flat Appl) TNil (lift (S i) O w)
that is equivalent to sn3 c (THead (Flat Appl) v (lift (S i) O w))
by (sn3_appl_abbr . . . . H . previous)
we proved sn3 c (THead (Flat Appl) v (TLRef i))
that is equivalent to
sn3
c
THead (Flat Appl) v (THeads (Flat Appl) TNil (TLRef i))
sn3 c (THeads (Flat Appl) TNil (lift (S i) O w))
→sn3 c (THeads (Flat Appl) TNil (TLRef i))
→((sn3
c
THead
Flat Appl
v
THeads (Flat Appl) TNil (lift (S i) O w))
→(sn3
c
THead (Flat Appl) v (THeads (Flat Appl) TNil (TLRef i))))
case TCons : t:T t0:TList ⇒
the thesis becomes
∀H1:sn3 c (THeads (Flat Appl) (TCons t t0) (lift (S i) O w))
→sn3 c (THeads (Flat Appl) (TCons t t0) (TLRef i))
.∀H2:sn3
c
THead
Flat Appl
v
THeads (Flat Appl) (TCons t t0) (lift (S i) O w)
.sn3
c
THead
Flat Appl
v
THeads (Flat Appl) (TCons t t0) (TLRef i)
() by induction hypothesis we know
sn3 c (THeads (Flat Appl) t0 (lift (S i) O w))
→sn3 c (THeads (Flat Appl) t0 (TLRef i))
→((sn3
c
THead (Flat Appl) v (THeads (Flat Appl) t0 (lift (S i) O w)))
→sn3 c (THead (Flat Appl) v (THeads (Flat Appl) t0 (TLRef i))))
suppose H1:
sn3 c (THeads (Flat Appl) (TCons t t0) (lift (S i) O w))
→sn3 c (THeads (Flat Appl) (TCons t t0) (TLRef i))
suppose H2:
sn3
c
THead
Flat Appl
v
THeads (Flat Appl) (TCons t t0) (lift (S i) O w)
(H_x)
by (sn3_gen_flat . . . . H2)
land
sn3 c v
sn3 c (THeads (Flat Appl) (TCons t t0) (lift (S i) O w))
end of H_x
(H3) consider H_x
consider H3
we proved
land
sn3 c v
sn3 c (THeads (Flat Appl) (TCons t t0) (lift (S i) O w))
that is equivalent to
land
sn3 c v
sn3
c
THead (Flat Appl) t (THeads (Flat Appl) t0 (lift (S i) O w))
we proceed by induction on the previous result to prove
sn3
c
THead
Flat Appl
v
THeads (Flat Appl) (TCons t t0) (TLRef i)
case conj : H4:sn3 c v H5:sn3 c (THead (Flat Appl) t (THeads (Flat Appl) t0 (lift (S i) O w))) ⇒
the thesis becomes
sn3
c
THead
Flat Appl
v
THeads (Flat Appl) (TCons t t0) (TLRef i)
(h1)
consider H5
we proved
sn3
c
THead (Flat Appl) t (THeads (Flat Appl) t0 (lift (S i) O w))
that is equivalent to sn3 c (THeads (Flat Appl) (TCons t t0) (lift (S i) O w))
by (H1 previous)
sn3 c (THeads (Flat Appl) (TCons t t0) (TLRef i))
end of h1
(h2)
assume u2: T
suppose H6: pr3 c (THeads (Flat Appl) (TCons t t0) (TLRef i)) u2
suppose H7:
(iso (THeads (Flat Appl) (TCons t t0) (TLRef i)) u2)→∀P:Prop.P
by (pr3_iso_appls_abbr . . . . H . . H6 H7)
we proved pr3 c (THeads (Flat Appl) (TCons t t0) (lift (S i) O w)) u2
by (pr3_thin_dx . . . previous . .)
we proved
pr3
c
THead
Flat Appl
v
THeads (Flat Appl) (TCons t t0) (lift (S i) O w)
THead (Flat Appl) v u2
by (sn3_pr3_trans . . H2 . previous)
we proved sn3 c (THead (Flat Appl) v u2)
∀u2:T
.pr3 c (THeads (Flat Appl) (TCons t t0) (TLRef i)) u2
→((iso (THeads (Flat Appl) (TCons t t0) (TLRef i)) u2)→∀P:Prop.P
→sn3 c (THead (Flat Appl) v u2))
end of h2
by (sn3_appl_appls . . . . h1 . H4 h2)
sn3
c
THead
Flat Appl
v
THeads (Flat Appl) (TCons t t0) (TLRef i)
we proved
sn3
c
THead
Flat Appl
v
THeads (Flat Appl) (TCons t t0) (TLRef i)
∀H1:sn3 c (THeads (Flat Appl) (TCons t t0) (lift (S i) O w))
→sn3 c (THeads (Flat Appl) (TCons t t0) (TLRef i))
.∀H2:sn3
c
THead
Flat Appl
v
THeads (Flat Appl) (TCons t t0) (lift (S i) O w)
.sn3
c
THead
Flat Appl
v
THeads (Flat Appl) (TCons t t0) (TLRef i)
we proved
sn3 c (THeads (Flat Appl) vs0 (lift (S i) O w))
→sn3 c (THeads (Flat Appl) vs0 (TLRef i))
→((sn3
c
THead (Flat Appl) v (THeads (Flat Appl) vs0 (lift (S i) O w)))
→sn3 c (THead (Flat Appl) v (THeads (Flat Appl) vs0 (TLRef i))))
that is equivalent to
sn3 c (THeads (Flat Appl) vs0 (lift (S i) O w))
→sn3 c (THeads (Flat Appl) vs0 (TLRef i))
→(sn3 c (THeads (Flat Appl) (TCons v vs0) (lift (S i) O w))
→sn3 c (THeads (Flat Appl) (TCons v vs0) (TLRef i)))
∀v:T
.∀vs0:TList
.sn3 c (THeads (Flat Appl) vs0 (lift (S i) O w))
→sn3 c (THeads (Flat Appl) vs0 (TLRef i))
→(sn3 c (THeads (Flat Appl) (TCons v vs0) (lift (S i) O w))
→sn3 c (THeads (Flat Appl) (TCons v vs0) (TLRef i)))
we proved
sn3 c (THeads (Flat Appl) vs (lift (S i) O w))
→sn3 c (THeads (Flat Appl) vs (TLRef i))
we proved
∀c:C
.∀d:C
.∀w:T
.∀i:nat
.getl i c (CHead d (Bind Abbr) w)
→∀vs:TList
.sn3 c (THeads (Flat Appl) vs (lift (S i) O w))
→sn3 c (THeads (Flat Appl) vs (TLRef i))