DEFINITION drop1_getl_trans()
TYPE =
∀hds:PList
.∀c1:C
.∀c2:C
.drop1 hds c2 c1
→∀b:B
.∀e1:C
.∀v:T
.∀i:nat
.getl i c1 (CHead e1 (Bind b) v)
→(ex2
C
λe2:C.drop1 (ptrans hds i) e2 e1
λe2:C.getl (trans hds i) c2 (CHead e2 (Bind b) (lift1 (ptrans hds i) v)))
BODY =
assume hds: PList
we proceed by induction on hds to prove
∀c1:C
.∀c2:C
.drop1 hds c2 c1
→∀b:B
.∀e1:C
.∀v:T
.∀i:nat
.getl i c1 (CHead e1 (Bind b) v)
→(ex2
C
λe2:C.drop1 (ptrans hds i) e2 e1
λe2:C.getl (trans hds i) c2 (CHead e2 (Bind b) (lift1 (ptrans hds i) v)))
case PNil : ⇒
the thesis becomes
∀c1:C
.∀c2:C
.drop1 PNil c2 c1
→∀b:B
.∀e1:C
.∀v:T
.∀i:nat
.getl i c1 (CHead e1 (Bind b) v)
→(ex2
C
λe2:C.drop1 (ptrans PNil i) e2 e1
λe2:C.getl (trans PNil i) c2 (CHead e2 (Bind b) (lift1 (ptrans PNil i) v)))
assume c1: C
assume c2: C
suppose H: drop1 PNil c2 c1
assume b: B
assume e1: C
assume v: T
assume i: nat
suppose H0: getl i c1 (CHead e1 (Bind b) v)
(H_y)
by (drop1_gen_pnil . . H)
eq C c2 c1
end of H_y
by (drop1_nil .)
we proved drop1 PNil e1 e1
by (ex_intro2 . . . . previous H0)
we proved ex2 C λe2:C.drop1 PNil e2 e1 λe2:C.getl i c1 (CHead e2 (Bind b) v)
by (eq_ind_r . . . previous . H_y)
we proved ex2 C λe2:C.drop1 PNil e2 e1 λe2:C.getl i c2 (CHead e2 (Bind b) v)
that is equivalent to
ex2
C
λe2:C.drop1 (ptrans PNil i) e2 e1
λe2:C.getl (trans PNil i) c2 (CHead e2 (Bind b) (lift1 (ptrans PNil i) v))
∀c1:C
.∀c2:C
.drop1 PNil c2 c1
→∀b:B
.∀e1:C
.∀v:T
.∀i:nat
.getl i c1 (CHead e1 (Bind b) v)
→(ex2
C
λe2:C.drop1 (ptrans PNil i) e2 e1
λe2:C.getl (trans PNil i) c2 (CHead e2 (Bind b) (lift1 (ptrans PNil i) v)))
case PCons : h:nat d:nat hds0:PList ⇒
the thesis becomes
∀c1:C
.∀c2:C
.∀H0:drop1 (PCons h d hds0) c2 c1
.∀b:B
.∀e1:C
.∀v:T
.∀i:nat
.∀H1:getl i c1 (CHead e1 (Bind b) v)
.ex2
C
λe2:C
.drop1
<λb1:bool.PList>
CASE blt (trans hds0 i) d OF
true⇒PCons h (minus d (S (trans hds0 i))) (ptrans hds0 i)
| false⇒ptrans hds0 i
e2
e1
λe2:C
.getl
<λb1:bool.nat>
CASE blt (trans hds0 i) d OF
true⇒trans hds0 i
| false⇒plus (trans hds0 i) h
c2
CHead
e2
Bind b
lift1
<λb1:bool.PList>
CASE blt (trans hds0 i) d OF
true⇒PCons h (minus d (S (trans hds0 i))) (ptrans hds0 i)
| false⇒ptrans hds0 i
v
(H) by induction hypothesis we know
∀c1:C
.∀c2:C
.drop1 hds0 c2 c1
→∀b:B
.∀e1:C
.∀v:T
.∀i:nat
.getl i c1 (CHead e1 (Bind b) v)
→(ex2
C
λe2:C.drop1 (ptrans hds0 i) e2 e1
λe2:C.getl (trans hds0 i) c2 (CHead e2 (Bind b) (lift1 (ptrans hds0 i) v)))
assume c1: C
assume c2: C
suppose H0: drop1 (PCons h d hds0) c2 c1
assume b: B
assume e1: C
assume v: T
assume i: nat
suppose H1: getl i c1 (CHead e1 (Bind b) v)
(H_x)
by (drop1_gen_pcons . . . . . H0)
ex2 C λc2:C.drop h d c2 c2 λc2:C.drop1 hds0 c2 c1
end of H_x
(H2) consider H_x
we proceed by induction on H2 to prove
ex2
C
λe2:C
.drop1
<λb1:bool.PList>
CASE blt (trans hds0 i) d OF
true⇒PCons h (minus d (S (trans hds0 i))) (ptrans hds0 i)
| false⇒ptrans hds0 i
e2
e1
λe2:C
.getl
<λb1:bool.nat>
CASE blt (trans hds0 i) d OF
true⇒trans hds0 i
| false⇒plus (trans hds0 i) h
c2
CHead
e2
Bind b
lift1
<λb1:bool.PList>
CASE blt (trans hds0 i) d OF
true⇒PCons h (minus d (S (trans hds0 i))) (ptrans hds0 i)
| false⇒ptrans hds0 i
v
case ex_intro2 : x:C H3:drop h d c2 x H4:drop1 hds0 x c1 ⇒
the thesis becomes
ex2
C
λe2:C
.drop1
<λb1:bool.PList>
CASE blt (trans hds0 i) d OF
true⇒PCons h (minus d (S (trans hds0 i))) (ptrans hds0 i)
| false⇒ptrans hds0 i
e2
e1
λe2:C
.getl
<λb1:bool.nat>
CASE blt (trans hds0 i) d OF
true⇒trans hds0 i
| false⇒plus (trans hds0 i) h
c2
CHead
e2
Bind b
lift1
<λb1:bool.PList>
CASE blt (trans hds0 i) d OF
true⇒PCons h (minus d (S (trans hds0 i))) (ptrans hds0 i)
| false⇒ptrans hds0 i
v
assume x_x: bool
we proceed by induction on x_x to prove
eq bool (blt (trans hds0 i) d) x_x
→(ex2
C
λe2:C
.drop1
<λb1:bool.PList>
CASE x_x OF
true⇒PCons h (minus d (S (trans hds0 i))) (ptrans hds0 i)
| false⇒ptrans hds0 i
e2
e1
λe2:C
.getl
<λb1:bool.nat> CASE x_x OF true⇒trans hds0 i | false⇒plus (trans hds0 i) h
c2
CHead
e2
Bind b
lift1
<λb1:bool.PList>
CASE x_x OF
true⇒PCons h (minus d (S (trans hds0 i))) (ptrans hds0 i)
| false⇒ptrans hds0 i
v)
case true : ⇒
the thesis becomes
eq bool (blt (trans hds0 i) d) true
→(ex2
C
λe2:C
.drop1
<λb1:bool.PList>
CASE true OF
true⇒PCons h (minus d (S (trans hds0 i))) (ptrans hds0 i)
| false⇒ptrans hds0 i
e2
e1
λe2:C
.getl
<λb1:bool.nat> CASE true OF true⇒trans hds0 i | false⇒plus (trans hds0 i) h
c2
CHead
e2
Bind b
lift1
<λb1:bool.PList>
CASE true OF
true⇒PCons h (minus d (S (trans hds0 i))) (ptrans hds0 i)
| false⇒ptrans hds0 i
v)
suppose H5: eq bool (blt (trans hds0 i) d) true
(H_x0)
by (H . . H4 . . . . H1)
ex2
C
λe2:C.drop1 (ptrans hds0 i) e2 e1
λe2:C.getl (trans hds0 i) x (CHead e2 (Bind b) (lift1 (ptrans hds0 i) v))
end of H_x0
(H6) consider H_x0
we proceed by induction on H6 to prove
ex2
C
λe2:C.drop1 (PCons h (minus d (S (trans hds0 i))) (ptrans hds0 i)) e2 e1
λe2:C
.getl
trans hds0 i
c2
CHead
e2
Bind b
lift1 (PCons h (minus d (S (trans hds0 i))) (ptrans hds0 i)) v
case ex_intro2 : x0:C H7:drop1 (ptrans hds0 i) x0 e1 H8:getl (trans hds0 i) x (CHead x0 (Bind b) (lift1 (ptrans hds0 i) v)) ⇒
the thesis becomes
ex2
C
λe2:C.drop1 (PCons h (minus d (S (trans hds0 i))) (ptrans hds0 i)) e2 e1
λe2:C
.getl
trans hds0 i
c2
CHead
e2
Bind b
lift1 (PCons h (minus d (S (trans hds0 i))) (ptrans hds0 i)) v
(H_x1)
by (blt_lt . . H5)
we proved lt (trans hds0 i) d
by (drop_getl_trans_lt . . previous . . . H3 . . . H8)
ex2
C
λe1:C
.getl
trans hds0 i
c2
CHead
e1
Bind b
lift h (minus d (S (trans hds0 i))) (lift1 (ptrans hds0 i) v)
λe1:C.drop h (minus d (S (trans hds0 i))) e1 x0
end of H_x1
(H9) consider H_x1
we proceed by induction on H9 to prove
ex2
C
λe2:C.drop1 (PCons h (minus d (S (trans hds0 i))) (ptrans hds0 i)) e2 e1
λe2:C
.getl
trans hds0 i
c2
CHead
e2
Bind b
lift1 (PCons h (minus d (S (trans hds0 i))) (ptrans hds0 i)) v
case ex_intro2 : x1:C H10:getl (trans hds0 i) c2 (CHead x1 (Bind b) (lift h (minus d (S (trans hds0 i))) (lift1 (ptrans hds0 i) v))) H11:drop h (minus d (S (trans hds0 i))) x1 x0 ⇒
the thesis becomes
ex2
C
λe2:C.drop1 (PCons h (minus d (S (trans hds0 i))) (ptrans hds0 i)) e2 e1
λe2:C
.getl
trans hds0 i
c2
CHead
e2
Bind b
lift1 (PCons h (minus d (S (trans hds0 i))) (ptrans hds0 i)) v
(h1)
by (drop1_cons . . . . H11 . . H7)
drop1 (PCons h (minus d (S (trans hds0 i))) (ptrans hds0 i)) x1 e1
end of h1
(h2)
consider H10
we proved
getl
trans hds0 i
c2
CHead
x1
Bind b
lift h (minus d (S (trans hds0 i))) (lift1 (ptrans hds0 i) v)
getl
trans hds0 i
c2
CHead
x1
Bind b
lift1 (PCons h (minus d (S (trans hds0 i))) (ptrans hds0 i)) v
end of h2
by (ex_intro2 . . . . h1 h2)
ex2
C
λe2:C.drop1 (PCons h (minus d (S (trans hds0 i))) (ptrans hds0 i)) e2 e1
λe2:C
.getl
trans hds0 i
c2
CHead
e2
Bind b
lift1 (PCons h (minus d (S (trans hds0 i))) (ptrans hds0 i)) v
ex2
C
λe2:C.drop1 (PCons h (minus d (S (trans hds0 i))) (ptrans hds0 i)) e2 e1
λe2:C
.getl
trans hds0 i
c2
CHead
e2
Bind b
lift1 (PCons h (minus d (S (trans hds0 i))) (ptrans hds0 i)) v
we proved
ex2
C
λe2:C.drop1 (PCons h (minus d (S (trans hds0 i))) (ptrans hds0 i)) e2 e1
λe2:C
.getl
trans hds0 i
c2
CHead
e2
Bind b
lift1 (PCons h (minus d (S (trans hds0 i))) (ptrans hds0 i)) v
that is equivalent to
ex2
C
λe2:C
.drop1
<λb1:bool.PList>
CASE true OF
true⇒PCons h (minus d (S (trans hds0 i))) (ptrans hds0 i)
| false⇒ptrans hds0 i
e2
e1
λe2:C
.getl
<λb1:bool.nat> CASE true OF true⇒trans hds0 i | false⇒plus (trans hds0 i) h
c2
CHead
e2
Bind b
lift1
<λb1:bool.PList>
CASE true OF
true⇒PCons h (minus d (S (trans hds0 i))) (ptrans hds0 i)
| false⇒ptrans hds0 i
v
eq bool (blt (trans hds0 i) d) true
→(ex2
C
λe2:C
.drop1
<λb1:bool.PList>
CASE true OF
true⇒PCons h (minus d (S (trans hds0 i))) (ptrans hds0 i)
| false⇒ptrans hds0 i
e2
e1
λe2:C
.getl
<λb1:bool.nat> CASE true OF true⇒trans hds0 i | false⇒plus (trans hds0 i) h
c2
CHead
e2
Bind b
lift1
<λb1:bool.PList>
CASE true OF
true⇒PCons h (minus d (S (trans hds0 i))) (ptrans hds0 i)
| false⇒ptrans hds0 i
v)
case false : ⇒
the thesis becomes
eq bool (blt (trans hds0 i) d) false
→(ex2
C
λe2:C
.drop1
<λb1:bool.PList>
CASE false OF
true⇒PCons h (minus d (S (trans hds0 i))) (ptrans hds0 i)
| false⇒ptrans hds0 i
e2
e1
λe2:C
.getl
<λb1:bool.nat> CASE false OF true⇒trans hds0 i | false⇒plus (trans hds0 i) h
c2
CHead
e2
Bind b
lift1
<λb1:bool.PList>
CASE false OF
true⇒PCons h (minus d (S (trans hds0 i))) (ptrans hds0 i)
| false⇒ptrans hds0 i
v)
suppose H5: eq bool (blt (trans hds0 i) d) false
(H_x0)
by (H . . H4 . . . . H1)
ex2
C
λe2:C.drop1 (ptrans hds0 i) e2 e1
λe2:C.getl (trans hds0 i) x (CHead e2 (Bind b) (lift1 (ptrans hds0 i) v))
end of H_x0
(H6) consider H_x0
we proceed by induction on H6 to prove
ex2
C
λe2:C.drop1 (ptrans hds0 i) e2 e1
λe2:C.getl (plus (trans hds0 i) h) c2 (CHead e2 (Bind b) (lift1 (ptrans hds0 i) v))
case ex_intro2 : x0:C H7:drop1 (ptrans hds0 i) x0 e1 H8:getl (trans hds0 i) x (CHead x0 (Bind b) (lift1 (ptrans hds0 i) v)) ⇒
the thesis becomes
ex2
C
λe2:C.drop1 (ptrans hds0 i) e2 e1
λe2:C.getl (plus (trans hds0 i) h) c2 (CHead e2 (Bind b) (lift1 (ptrans hds0 i) v))
(H9)
by (drop_getl_trans_ge . . . . . H3 . H8)
le d (trans hds0 i)
→getl (plus (trans hds0 i) h) c2 (CHead x0 (Bind b) (lift1 (ptrans hds0 i) v))
end of H9
by (bge_le . . H5)
we proved le d (trans hds0 i)
by (H9 previous)
we proved getl (plus (trans hds0 i) h) c2 (CHead x0 (Bind b) (lift1 (ptrans hds0 i) v))
by (ex_intro2 . . . . H7 previous)
ex2
C
λe2:C.drop1 (ptrans hds0 i) e2 e1
λe2:C.getl (plus (trans hds0 i) h) c2 (CHead e2 (Bind b) (lift1 (ptrans hds0 i) v))
we proved
ex2
C
λe2:C.drop1 (ptrans hds0 i) e2 e1
λe2:C.getl (plus (trans hds0 i) h) c2 (CHead e2 (Bind b) (lift1 (ptrans hds0 i) v))
that is equivalent to
ex2
C
λe2:C
.drop1
<λb1:bool.PList>
CASE false OF
true⇒PCons h (minus d (S (trans hds0 i))) (ptrans hds0 i)
| false⇒ptrans hds0 i
e2
e1
λe2:C
.getl
<λb1:bool.nat> CASE false OF true⇒trans hds0 i | false⇒plus (trans hds0 i) h
c2
CHead
e2
Bind b
lift1
<λb1:bool.PList>
CASE false OF
true⇒PCons h (minus d (S (trans hds0 i))) (ptrans hds0 i)
| false⇒ptrans hds0 i
v
eq bool (blt (trans hds0 i) d) false
→(ex2
C
λe2:C
.drop1
<λb1:bool.PList>
CASE false OF
true⇒PCons h (minus d (S (trans hds0 i))) (ptrans hds0 i)
| false⇒ptrans hds0 i
e2
e1
λe2:C
.getl
<λb1:bool.nat> CASE false OF true⇒trans hds0 i | false⇒plus (trans hds0 i) h
c2
CHead
e2
Bind b
lift1
<λb1:bool.PList>
CASE false OF
true⇒PCons h (minus d (S (trans hds0 i))) (ptrans hds0 i)
| false⇒ptrans hds0 i
v)
we proved
eq bool (blt (trans hds0 i) d) x_x
→(ex2
C
λe2:C
.drop1
<λb1:bool.PList>
CASE x_x OF
true⇒PCons h (minus d (S (trans hds0 i))) (ptrans hds0 i)
| false⇒ptrans hds0 i
e2
e1
λe2:C
.getl
<λb1:bool.nat> CASE x_x OF true⇒trans hds0 i | false⇒plus (trans hds0 i) h
c2
CHead
e2
Bind b
lift1
<λb1:bool.PList>
CASE x_x OF
true⇒PCons h (minus d (S (trans hds0 i))) (ptrans hds0 i)
| false⇒ptrans hds0 i
v)
we proved
∀x_x:bool
.eq bool (blt (trans hds0 i) d) x_x
→(ex2
C
λe2:C
.drop1
<λb1:bool.PList>
CASE x_x OF
true⇒PCons h (minus d (S (trans hds0 i))) (ptrans hds0 i)
| false⇒ptrans hds0 i
e2
e1
λe2:C
.getl
<λb1:bool.nat> CASE x_x OF true⇒trans hds0 i | false⇒plus (trans hds0 i) h
c2
CHead
e2
Bind b
lift1
<λb1:bool.PList>
CASE x_x OF
true⇒PCons h (minus d (S (trans hds0 i))) (ptrans hds0 i)
| false⇒ptrans hds0 i
v)
by (xinduction . . . previous)
ex2
C
λe2:C
.drop1
<λb1:bool.PList>
CASE blt (trans hds0 i) d OF
true⇒PCons h (minus d (S (trans hds0 i))) (ptrans hds0 i)
| false⇒ptrans hds0 i
e2
e1
λe2:C
.getl
<λb1:bool.nat>
CASE blt (trans hds0 i) d OF
true⇒trans hds0 i
| false⇒plus (trans hds0 i) h
c2
CHead
e2
Bind b
lift1
<λb1:bool.PList>
CASE blt (trans hds0 i) d OF
true⇒PCons h (minus d (S (trans hds0 i))) (ptrans hds0 i)
| false⇒ptrans hds0 i
v
we proved
ex2
C
λe2:C
.drop1
<λb1:bool.PList>
CASE blt (trans hds0 i) d OF
true⇒PCons h (minus d (S (trans hds0 i))) (ptrans hds0 i)
| false⇒ptrans hds0 i
e2
e1
λe2:C
.getl
<λb1:bool.nat>
CASE blt (trans hds0 i) d OF
true⇒trans hds0 i
| false⇒plus (trans hds0 i) h
c2
CHead
e2
Bind b
lift1
<λb1:bool.PList>
CASE blt (trans hds0 i) d OF
true⇒PCons h (minus d (S (trans hds0 i))) (ptrans hds0 i)
| false⇒ptrans hds0 i
v
that is equivalent to
ex2
C
λe2:C.drop1 (ptrans (PCons h d hds0) i) e2 e1
λe2:C
.getl
trans (PCons h d hds0) i
c2
CHead e2 (Bind b) (lift1 (ptrans (PCons h d hds0) i) v)
∀c1:C
.∀c2:C
.∀H0:drop1 (PCons h d hds0) c2 c1
.∀b:B
.∀e1:C
.∀v:T
.∀i:nat
.∀H1:getl i c1 (CHead e1 (Bind b) v)
.ex2
C
λe2:C
.drop1
<λb1:bool.PList>
CASE blt (trans hds0 i) d OF
true⇒PCons h (minus d (S (trans hds0 i))) (ptrans hds0 i)
| false⇒ptrans hds0 i
e2
e1
λe2:C
.getl
<λb1:bool.nat>
CASE blt (trans hds0 i) d OF
true⇒trans hds0 i
| false⇒plus (trans hds0 i) h
c2
CHead
e2
Bind b
lift1
<λb1:bool.PList>
CASE blt (trans hds0 i) d OF
true⇒PCons h (minus d (S (trans hds0 i))) (ptrans hds0 i)
| false⇒ptrans hds0 i
v
we proved
∀c1:C
.∀c2:C
.drop1 hds c2 c1
→∀b:B
.∀e1:C
.∀v:T
.∀i:nat
.getl i c1 (CHead e1 (Bind b) v)
→(ex2
C
λe2:C.drop1 (ptrans hds i) e2 e1
λe2:C.getl (trans hds i) c2 (CHead e2 (Bind b) (lift1 (ptrans hds i) v)))
we proved
∀hds:PList
.∀c1:C
.∀c2:C
.drop1 hds c2 c1
→∀b:B
.∀e1:C
.∀v:T
.∀i:nat
.getl i c1 (CHead e1 (Bind b) v)
→(ex2
C
λe2:C.drop1 (ptrans hds i) e2 e1
λe2:C.getl (trans hds i) c2 (CHead e2 (Bind b) (lift1 (ptrans hds i) v)))