DEFINITION lift_d()
TYPE =
∀t:T
.∀h:nat
.∀k:nat
.∀d:nat
.∀e:nat
.le e d
→eq T (lift h (plus k d) (lift k e t)) (lift k e (lift h d t))
BODY =
assume t: T
we proceed by induction on t to prove
∀h:nat
.∀k:nat
.∀d:nat
.∀e:nat
.le e d
→eq T (lift h (plus k d) (lift k e t)) (lift k e (lift h d t))
case TSort : n:nat ⇒
the thesis becomes
∀h:nat
.∀k:nat
.∀d:nat
.∀e:nat
.le e d
→(eq
T
lift h (plus k d) (lift k e (TSort n))
lift k e (lift h d (TSort n)))
assume h: nat
assume k: nat
assume d: nat
assume e: nat
suppose : le e d
(h1)
(h1)
(h1)
(h1)
by (refl_equal . .)
eq T (TSort n) (TSort n)
end of h1
(h2)
by (lift_sort . . .)
eq T (lift k e (TSort n)) (TSort n)
end of h2
by (eq_ind_r . . . h1 . h2)
eq T (TSort n) (lift k e (TSort n))
end of h1
(h2)
by (lift_sort . . .)
eq T (lift h d (TSort n)) (TSort n)
end of h2
by (eq_ind_r . . . h1 . h2)
eq T (TSort n) (lift k e (lift h d (TSort n)))
end of h1
(h2)
by (lift_sort . . .)
eq T (lift h (plus k d) (TSort n)) (TSort n)
end of h2
by (eq_ind_r . . . h1 . h2)
eq
T
lift h (plus k d) (TSort n)
lift k e (lift h d (TSort n))
end of h1
(h2)
by (lift_sort . . .)
eq T (lift k e (TSort n)) (TSort n)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
eq
T
lift h (plus k d) (lift k e (TSort n))
lift k e (lift h d (TSort n))
∀h:nat
.∀k:nat
.∀d:nat
.∀e:nat
.le e d
→(eq
T
lift h (plus k d) (lift k e (TSort n))
lift k e (lift h d (TSort n)))
case TLRef : n:nat ⇒
the thesis becomes
∀h:nat
.∀k:nat
.∀d:nat
.∀e:nat
.∀H:le e d
.eq
T
lift h (plus k d) (lift k e (TLRef n))
lift k e (lift h d (TLRef n))
assume h: nat
assume k: nat
assume d: nat
assume e: nat
suppose H: le e d
(h1)
suppose H0: lt n e
(H1)
by (lt_le_trans . . . H0 H)
lt n d
end of H1
(h1)
(h1)
(h1)
(h1)
by (refl_equal . .)
eq T (TLRef n) (TLRef n)
end of h1
(h2)
by (lift_lref_lt . . . H0)
eq T (lift k e (TLRef n)) (TLRef n)
end of h2
by (eq_ind_r . . . h1 . h2)
eq T (TLRef n) (lift k e (TLRef n))
end of h1
(h2)
by (lift_lref_lt . . . H1)
eq T (lift h d (TLRef n)) (TLRef n)
end of h2
by (eq_ind_r . . . h1 . h2)
eq T (TLRef n) (lift k e (lift h d (TLRef n)))
end of h1
(h2)
by (le_plus_r . .)
we proved le d (plus k d)
by (lt_le_trans . . . H1 previous)
we proved lt n (plus k d)
by (lift_lref_lt . . . previous)
eq T (lift h (plus k d) (TLRef n)) (TLRef n)
end of h2
by (eq_ind_r . . . h1 . h2)
eq
T
lift h (plus k d) (TLRef n)
lift k e (lift h d (TLRef n))
end of h1
(h2)
by (lift_lref_lt . . . H0)
eq T (lift k e (TLRef n)) (TLRef n)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
eq
T
lift h (plus k d) (lift k e (TLRef n))
lift k e (lift h d (TLRef n))
lt n e
→(eq
T
lift h (plus k d) (lift k e (TLRef n))
lift k e (lift h d (TLRef n)))
end of h1
(h2)
suppose H0: le e n
(h1)
(h1)
(h1)
suppose H1: lt n d
(h1)
(h1)
(h1)
by (refl_equal . .)
eq T (TLRef (plus n k)) (TLRef (plus n k))
end of h1
(h2)
by (lift_lref_ge . . . H0)
eq T (lift k e (TLRef n)) (TLRef (plus n k))
end of h2
by (eq_ind_r . . . h1 . h2)
eq T (TLRef (plus n k)) (lift k e (TLRef n))
end of h1
(h2)
by (lift_lref_lt . . . H1)
eq T (lift h d (TLRef n)) (TLRef n)
end of h2
by (eq_ind_r . . . h1 . h2)
eq T (TLRef (plus n k)) (lift k e (lift h d (TLRef n)))
end of h1
(h2)
by (lt_reg_r . . . H1)
we proved lt (plus n k) (plus d k)
by (lift_lref_lt . . . previous)
eq
T
lift h (plus d k) (TLRef (plus n k))
TLRef (plus n k)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
eq
T
lift h (plus d k) (TLRef (plus n k))
lift k e (lift h d (TLRef n))
lt n d
→(eq
T
lift h (plus d k) (TLRef (plus n k))
lift k e (lift h d (TLRef n)))
end of h1
(h2)
suppose H1: le d n
(h1)
(h1)
(h1)
by (plus_permute_2_in_3 . . .)
we proved eq nat (plus (plus n h) k) (plus (plus n k) h)
by (sym_eq . . . previous)
we proved eq nat (plus (plus n k) h) (plus (plus n h) k)
by (f_equal . . . . . previous)
eq
T
TLRef (plus (plus n k) h)
TLRef (plus (plus n h) k)
end of h1
(h2)
by (le_plus_trans . . . H0)
we proved le e (plus n h)
by (lift_lref_ge . . . previous)
eq
T
lift k e (TLRef (plus n h))
TLRef (plus (plus n h) k)
end of h2
by (eq_ind_r . . . h1 . h2)
eq
T
TLRef (plus (plus n k) h)
lift k e (TLRef (plus n h))
end of h1
(h2)
by (lift_lref_ge . . . H1)
eq T (lift h d (TLRef n)) (TLRef (plus n h))
end of h2
by (eq_ind_r . . . h1 . h2)
eq
T
TLRef (plus (plus n k) h)
lift k e (lift h d (TLRef n))
end of h1
(h2)
by (le_n .)
we proved le k k
by (le_plus_plus . . . . H1 previous)
we proved le (plus d k) (plus n k)
by (lift_lref_ge . . . previous)
eq
T
lift h (plus d k) (TLRef (plus n k))
TLRef (plus (plus n k) h)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
eq
T
lift h (plus d k) (TLRef (plus n k))
lift k e (lift h d (TLRef n))
le d n
→(eq
T
lift h (plus d k) (TLRef (plus n k))
lift k e (lift h d (TLRef n)))
end of h2
by (lt_le_e . . . h1 h2)
eq
T
lift h (plus d k) (TLRef (plus n k))
lift k e (lift h d (TLRef n))
end of h1
(h2)
by (plus_sym . .)
eq nat (plus k d) (plus d k)
end of h2
by (eq_ind_r . . . h1 . h2)
eq
T
lift h (plus k d) (TLRef (plus n k))
lift k e (lift h d (TLRef n))
end of h1
(h2)
by (lift_lref_ge . . . H0)
eq T (lift k e (TLRef n)) (TLRef (plus n k))
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
eq
T
lift h (plus k d) (lift k e (TLRef n))
lift k e (lift h d (TLRef n))
le e n
→(eq
T
lift h (plus k d) (lift k e (TLRef n))
lift k e (lift h d (TLRef n)))
end of h2
by (lt_le_e . . . h1 h2)
we proved
eq
T
lift h (plus k d) (lift k e (TLRef n))
lift k e (lift h d (TLRef n))
∀h:nat
.∀k:nat
.∀d:nat
.∀e:nat
.∀H:le e d
.eq
T
lift h (plus k d) (lift k e (TLRef n))
lift k e (lift h d (TLRef n))
case THead : k:K t0:T t1:T ⇒
the thesis becomes
∀h:nat
.∀k0:nat
.∀d:nat
.∀e:nat
.∀H1:le e d
.eq
T
lift h (plus k0 d) (lift k0 e (THead k t0 t1))
lift k0 e (lift h d (THead k t0 t1))
(H) by induction hypothesis we know
∀h:nat
.∀k0:nat
.∀d:nat
.∀e:nat
.le e d
→eq T (lift h (plus k0 d) (lift k0 e t0)) (lift k0 e (lift h d t0))
(H0) by induction hypothesis we know
∀h:nat
.∀k0:nat
.∀d:nat
.∀e:nat
.le e d
→eq T (lift h (plus k0 d) (lift k0 e t1)) (lift k0 e (lift h d t1))
assume h: nat
assume k0: nat
assume d: nat
assume e: nat
suppose H1: le e d
(h1)
(h1)
(h1)
(h1)
(h1)
(h1)
by (refl_equal . .)
eq K k k
end of h1
(h2)
by (H . . . . H1)
eq T (lift h (plus k0 d) (lift k0 e t0)) (lift k0 e (lift h d t0))
end of h2
(h3)
by (s_le . . . H1)
we proved le (s k e) (s k d)
by (H0 . . . . previous)
eq
T
lift h (plus k0 (s k d)) (lift k0 (s k e) t1)
lift k0 (s k e) (lift h (s k d) t1)
end of h3
by (f_equal3 . . . . . . . . . . . h1 h2 h3)
eq
T
THead
k
lift h (plus k0 d) (lift k0 e t0)
lift h (plus k0 (s k d)) (lift k0 (s k e) t1)
THead k (lift k0 e (lift h d t0)) (lift k0 (s k e) (lift h (s k d) t1))
end of h1
(h2)
by (s_plus_sym . . .)
eq nat (s k (plus k0 d)) (plus k0 (s k d))
end of h2
by (eq_ind_r . . . h1 . h2)
eq
T
THead
k
lift h (plus k0 d) (lift k0 e t0)
lift h (s k (plus k0 d)) (lift k0 (s k e) t1)
THead k (lift k0 e (lift h d t0)) (lift k0 (s k e) (lift h (s k d) t1))
end of h1
(h2)
by (lift_head . . . . .)
eq
T
lift k0 e (THead k (lift h d t0) (lift h (s k d) t1))
THead k (lift k0 e (lift h d t0)) (lift k0 (s k e) (lift h (s k d) t1))
end of h2
by (eq_ind_r . . . h1 . h2)
eq
T
THead
k
lift h (plus k0 d) (lift k0 e t0)
lift h (s k (plus k0 d)) (lift k0 (s k e) t1)
lift k0 e (THead k (lift h d t0) (lift h (s k d) t1))
end of h1
(h2)
by (lift_head . . . . .)
eq
T
lift h d (THead k t0 t1)
THead k (lift h d t0) (lift h (s k d) t1)
end of h2
by (eq_ind_r . . . h1 . h2)
eq
T
THead
k
lift h (plus k0 d) (lift k0 e t0)
lift h (s k (plus k0 d)) (lift k0 (s k e) t1)
lift k0 e (lift h d (THead k t0 t1))
end of h1
(h2)
by (lift_head . . . . .)
eq
T
lift h (plus k0 d) (THead k (lift k0 e t0) (lift k0 (s k e) t1))
THead
k
lift h (plus k0 d) (lift k0 e t0)
lift h (s k (plus k0 d)) (lift k0 (s k e) t1)
end of h2
by (eq_ind_r . . . h1 . h2)
eq
T
lift h (plus k0 d) (THead k (lift k0 e t0) (lift k0 (s k e) t1))
lift k0 e (lift h d (THead k t0 t1))
end of h1
(h2)
by (lift_head . . . . .)
eq T (lift k0 e (THead k t0 t1)) (THead k (lift k0 e t0) (lift k0 (s k e) t1))
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
eq
T
lift h (plus k0 d) (lift k0 e (THead k t0 t1))
lift k0 e (lift h d (THead k t0 t1))
∀h:nat
.∀k0:nat
.∀d:nat
.∀e:nat
.∀H1:le e d
.eq
T
lift h (plus k0 d) (lift k0 e (THead k t0 t1))
lift k0 e (lift h d (THead k t0 t1))
we proved
∀h:nat
.∀k:nat
.∀d:nat
.∀e:nat
.le e d
→eq T (lift h (plus k d) (lift k e t)) (lift k e (lift h d t))
we proved
∀t:T
.∀h:nat
.∀k:nat
.∀d:nat
.∀e:nat
.le e d
→eq T (lift h (plus k d) (lift k e t)) (lift k e (lift h d t))