DEFINITION lift1_free()
TYPE =
∀hds:PList
.∀i:nat
.∀t:T
.eq
T
lift1 hds (lift (S i) O t)
lift (S (trans hds i)) O (lift1 (ptrans hds i) t)
BODY =
assume hds: PList
we proceed by induction on hds to prove
∀i:nat
.∀t:T
.eq
T
lift1 hds (lift (S i) O t)
lift (S (trans hds i)) O (lift1 (ptrans hds i) t)
case PNil : ⇒
the thesis becomes
∀i:nat
.∀t:T
.eq
T
lift1 PNil (lift (S i) O t)
lift (S (trans PNil i)) O (lift1 (ptrans PNil i) t)
assume i: nat
assume t: T
by (refl_equal . .)
we proved eq T (lift (S i) O t) (lift (S i) O t)
that is equivalent to
eq
T
lift1 PNil (lift (S i) O t)
lift (S (trans PNil i)) O (lift1 (ptrans PNil i) t)
∀i:nat
.∀t:T
.eq
T
lift1 PNil (lift (S i) O t)
lift (S (trans PNil i)) O (lift1 (ptrans PNil i) t)
case PCons : h:nat d:nat hds0:PList ⇒
the thesis becomes
∀i:nat
.∀t:T
.eq
T
lift h d (lift1 hds0 (lift (S i) O t))
lift
S
<λb:bool.nat>
CASE blt (trans hds0 i) d OF
true⇒trans hds0 i
| false⇒plus (trans hds0 i) h
O
lift1
<λb: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
t
(H) by induction hypothesis we know
∀i:nat
.∀t:T
.eq
T
lift1 hds0 (lift (S i) O t)
lift (S (trans hds0 i)) O (lift1 (ptrans hds0 i) t)
assume i: nat
assume t: T
(h1)
assume x_x: bool
we proceed by induction on x_x to prove
eq bool (blt (trans hds0 i) d) x_x
→(eq
T
lift h d (lift (S (trans hds0 i)) O (lift1 (ptrans hds0 i) t))
lift
S
<λb1:bool.nat> CASE x_x OF true⇒trans hds0 i | false⇒plus (trans hds0 i) h
O
lift1
<λb1:bool.PList>
CASE x_x OF
true⇒PCons h (minus d (S (trans hds0 i))) (ptrans hds0 i)
| false⇒ptrans hds0 i
t)
case true : ⇒
the thesis becomes
eq bool (blt (trans hds0 i) d) true
→(eq
T
lift h d (lift (S (trans hds0 i)) O (lift1 (ptrans hds0 i) t))
lift
S
<λb1:bool.nat> CASE true OF true⇒trans hds0 i | false⇒plus (trans hds0 i) h
O
lift1
<λb1:bool.PList>
CASE true OF
true⇒PCons h (minus d (S (trans hds0 i))) (ptrans hds0 i)
| false⇒ptrans hds0 i
t)
suppose H0: eq bool (blt (trans hds0 i) d) true
(h1)
(h1)
by (refl_equal . .)
we proved
eq
T
lift
S (trans hds0 i)
O
lift1 (PCons h (minus d (S (trans hds0 i))) (ptrans hds0 i)) t
lift
S (trans hds0 i)
O
lift1 (PCons h (minus d (S (trans hds0 i))) (ptrans hds0 i)) t
eq
T
lift
S (trans hds0 i)
O
lift h (minus d (S (trans hds0 i))) (lift1 (ptrans hds0 i) t)
lift
S (trans hds0 i)
O
lift1 (PCons h (minus d (S (trans hds0 i))) (ptrans hds0 i)) t
end of h1
(h2)
by (le_O_n .)
we proved le O (minus d (S (trans hds0 i)))
by (lift_d . . . . . previous)
eq
T
lift
h
plus (S (trans hds0 i)) (minus d (S (trans hds0 i)))
lift (S (trans hds0 i)) O (lift1 (ptrans hds0 i) t)
lift
S (trans hds0 i)
O
lift h (minus d (S (trans hds0 i))) (lift1 (ptrans hds0 i) t)
end of h2
by (eq_ind_r . . . h1 . h2)
eq
T
lift
h
plus (S (trans hds0 i)) (minus d (S (trans hds0 i)))
lift (S (trans hds0 i)) O (lift1 (ptrans hds0 i) t)
lift
S (trans hds0 i)
O
lift1 (PCons h (minus d (S (trans hds0 i))) (ptrans hds0 i)) t
end of h1
(h2)
by (blt_lt . . H0)
we proved lt (trans hds0 i) d
by (lt_le_S . . previous)
we proved le (S (trans hds0 i)) d
by (le_bge . . previous)
we proved eq bool (blt d (S (trans hds0 i))) false
by (bge_le . . previous)
we proved le (S (trans hds0 i)) d
by (le_plus_minus . . previous)
eq nat d (plus (S (trans hds0 i)) (minus d (S (trans hds0 i))))
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
eq
T
lift h d (lift (S (trans hds0 i)) O (lift1 (ptrans hds0 i) t))
lift
S (trans hds0 i)
O
lift1 (PCons h (minus d (S (trans hds0 i))) (ptrans hds0 i)) t
that is equivalent to
eq
T
lift h d (lift (S (trans hds0 i)) O (lift1 (ptrans hds0 i) t))
lift
S
<λb1:bool.nat> CASE true OF true⇒trans hds0 i | false⇒plus (trans hds0 i) h
O
lift1
<λb1:bool.PList>
CASE true OF
true⇒PCons h (minus d (S (trans hds0 i))) (ptrans hds0 i)
| false⇒ptrans hds0 i
t
eq bool (blt (trans hds0 i) d) true
→(eq
T
lift h d (lift (S (trans hds0 i)) O (lift1 (ptrans hds0 i) t))
lift
S
<λb1:bool.nat> CASE true OF true⇒trans hds0 i | false⇒plus (trans hds0 i) h
O
lift1
<λb1:bool.PList>
CASE true OF
true⇒PCons h (minus d (S (trans hds0 i))) (ptrans hds0 i)
| false⇒ptrans hds0 i
t)
case false : ⇒
the thesis becomes
eq bool (blt (trans hds0 i) d) false
→(eq
T
lift h d (lift (S (trans hds0 i)) O (lift1 (ptrans hds0 i) t))
lift
S
<λb1:bool.nat> CASE false OF true⇒trans hds0 i | false⇒plus (trans hds0 i) h
O
lift1
<λb1:bool.PList>
CASE false OF
true⇒PCons h (minus d (S (trans hds0 i))) (ptrans hds0 i)
| false⇒ptrans hds0 i
t)
suppose H0: eq bool (blt (trans hds0 i) d) false
(h1)
by (plus_n_Sm . .)
we proved eq nat (S (plus h (trans hds0 i))) (plus h (S (trans hds0 i)))
we proceed by induction on the previous result to prove
eq
T
lift (plus h (S (trans hds0 i))) O (lift1 (ptrans hds0 i) t)
lift (S (plus (trans hds0 i) h)) O (lift1 (ptrans hds0 i) t)
case refl_equal : ⇒
the thesis becomes
eq
T
lift (S (plus h (trans hds0 i))) O (lift1 (ptrans hds0 i) t)
lift (S (plus (trans hds0 i) h)) O (lift1 (ptrans hds0 i) t)
(h1)
by (refl_equal . .)
eq
T
lift (S (plus (trans hds0 i) h)) O (lift1 (ptrans hds0 i) t)
lift (S (plus (trans hds0 i) h)) O (lift1 (ptrans hds0 i) t)
end of h1
(h2)
by (plus_sym . .)
eq nat (plus h (trans hds0 i)) (plus (trans hds0 i) h)
end of h2
by (eq_ind_r . . . h1 . h2)
eq
T
lift (S (plus h (trans hds0 i))) O (lift1 (ptrans hds0 i) t)
lift (S (plus (trans hds0 i) h)) O (lift1 (ptrans hds0 i) t)
eq
T
lift (plus h (S (trans hds0 i))) O (lift1 (ptrans hds0 i) t)
lift (S (plus (trans hds0 i) h)) O (lift1 (ptrans hds0 i) t)
end of h1
(h2)
(h1)
by (plus_n_Sm . .)
we proved eq nat (S (plus O (trans hds0 i))) (plus O (S (trans hds0 i)))
we proceed by induction on the previous result to prove le d (plus O (S (trans hds0 i)))
case refl_equal : ⇒
the thesis becomes le d (S (plus O (trans hds0 i)))
(h1)
by (bge_le . . H0)
we proved le d (trans hds0 i)
by (le_plus_trans . . . previous)
we proved le d (plus (trans hds0 i) O)
by (le_S . . previous)
le d (S (plus (trans hds0 i) O))
end of h1
(h2)
by (plus_sym . .)
eq nat (plus O (trans hds0 i)) (plus (trans hds0 i) O)
end of h2
by (eq_ind_r . . . h1 . h2)
le d (S (plus O (trans hds0 i)))
le d (plus O (S (trans hds0 i)))
end of h1
(h2) by (le_O_n .) we proved le O d
by (lift_free . . . . . h1 h2)
eq
T
lift h d (lift (S (trans hds0 i)) O (lift1 (ptrans hds0 i) t))
lift (plus h (S (trans hds0 i))) O (lift1 (ptrans hds0 i) t)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
eq
T
lift h d (lift (S (trans hds0 i)) O (lift1 (ptrans hds0 i) t))
lift (S (plus (trans hds0 i) h)) O (lift1 (ptrans hds0 i) t)
that is equivalent to
eq
T
lift h d (lift (S (trans hds0 i)) O (lift1 (ptrans hds0 i) t))
lift
S
<λb1:bool.nat> CASE false OF true⇒trans hds0 i | false⇒plus (trans hds0 i) h
O
lift1
<λb1:bool.PList>
CASE false OF
true⇒PCons h (minus d (S (trans hds0 i))) (ptrans hds0 i)
| false⇒ptrans hds0 i
t
eq bool (blt (trans hds0 i) d) false
→(eq
T
lift h d (lift (S (trans hds0 i)) O (lift1 (ptrans hds0 i) t))
lift
S
<λb1:bool.nat> CASE false OF true⇒trans hds0 i | false⇒plus (trans hds0 i) h
O
lift1
<λb1:bool.PList>
CASE false OF
true⇒PCons h (minus d (S (trans hds0 i))) (ptrans hds0 i)
| false⇒ptrans hds0 i
t)
we proved
eq bool (blt (trans hds0 i) d) x_x
→(eq
T
lift h d (lift (S (trans hds0 i)) O (lift1 (ptrans hds0 i) t))
lift
S
<λb1:bool.nat> CASE x_x OF true⇒trans hds0 i | false⇒plus (trans hds0 i) h
O
lift1
<λb1:bool.PList>
CASE x_x OF
true⇒PCons h (minus d (S (trans hds0 i))) (ptrans hds0 i)
| false⇒ptrans hds0 i
t)
we proved
∀x_x:bool
.eq bool (blt (trans hds0 i) d) x_x
→(eq
T
lift h d (lift (S (trans hds0 i)) O (lift1 (ptrans hds0 i) t))
lift
S
<λb1:bool.nat> CASE x_x OF true⇒trans hds0 i | false⇒plus (trans hds0 i) h
O
lift1
<λb1:bool.PList>
CASE x_x OF
true⇒PCons h (minus d (S (trans hds0 i))) (ptrans hds0 i)
| false⇒ptrans hds0 i
t)
by (xinduction . . . previous)
eq
T
lift h d (lift (S (trans hds0 i)) O (lift1 (ptrans hds0 i) t))
lift
S
<λb1:bool.nat>
CASE blt (trans hds0 i) d OF
true⇒trans hds0 i
| false⇒plus (trans hds0 i) h
O
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
t
end of h1
(h2)
by (H . .)
eq
T
lift1 hds0 (lift (S i) O t)
lift (S (trans hds0 i)) O (lift1 (ptrans hds0 i) t)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
eq
T
lift h d (lift1 hds0 (lift (S i) O t))
lift
S
<λb:bool.nat>
CASE blt (trans hds0 i) d OF
true⇒trans hds0 i
| false⇒plus (trans hds0 i) h
O
lift1
<λb: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
t
that is equivalent to
eq
T
lift1 (PCons h d hds0) (lift (S i) O t)
lift (S (trans (PCons h d hds0) i)) O (lift1 (ptrans (PCons h d hds0) i) t)
∀i:nat
.∀t:T
.eq
T
lift h d (lift1 hds0 (lift (S i) O t))
lift
S
<λb:bool.nat>
CASE blt (trans hds0 i) d OF
true⇒trans hds0 i
| false⇒plus (trans hds0 i) h
O
lift1
<λb: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
t
we proved
∀i:nat
.∀t:T
.eq
T
lift1 hds (lift (S i) O t)
lift (S (trans hds i)) O (lift1 (ptrans hds i) t)
we proved
∀hds:PList
.∀i:nat
.∀t:T
.eq
T
lift1 hds (lift (S i) O t)
lift (S (trans hds i)) O (lift1 (ptrans hds i) t)