DEFINITION drop_trans_ge()
TYPE =
∀i:nat
.∀c1:C
.∀c2:C
.∀d:nat
.∀h:nat
.drop h d c1 c2
→∀e2:C.(drop i O c2 e2)→(le d i)→(drop (plus i h) O c1 e2)
BODY =
assume i: nat
we proceed by induction on i to prove
∀c1:C
.∀c2:C
.∀d:nat
.∀h:nat
.drop h d c1 c2
→∀e2:C.(drop i O c2 e2)→(le d i)→(drop (plus i h) O c1 e2)
case O : ⇒
the thesis becomes
∀c1:C
.∀c2:C
.∀d:nat
.∀h:nat
.drop h d c1 c2
→∀e2:C.(drop O O c2 e2)→(le d O)→(drop (plus O h) O c1 e2)
assume c1: C
assume c2: C
assume d: nat
assume h: nat
suppose H: drop h d c1 c2
assume e2: C
suppose H0: drop O O c2 e2
suppose H1: le d O
by (drop_gen_refl . . H0)
we proved eq C c2 e2
we proceed by induction on the previous result to prove drop (plus O h) O c1 e2
case refl_equal : ⇒
the thesis becomes drop (plus O h) O c1 c2
(H_y)
by (le_n_O_eq . H1)
eq nat O d
end of H_y
(H2)
by (eq_ind_r . . . H . H_y)
drop h O c1 c2
end of H2
consider H2
we proved drop h O c1 c2
drop (plus O h) O c1 c2
we proved drop (plus O h) O c1 e2
∀c1:C
.∀c2:C
.∀d:nat
.∀h:nat
.drop h d c1 c2
→∀e2:C.(drop O O c2 e2)→(le d O)→(drop (plus O h) O c1 e2)
case S : i0:nat ⇒
the thesis becomes
∀c1:C
.∀c2:C
.∀d:nat
.∀h:nat
.drop h d c1 c2
→∀e2:C.(drop (S i0) O c2 e2)→(le d (S i0))→(drop (plus (S i0) h) O c1 e2)
(IHi) by induction hypothesis we know
∀c1:C
.∀c2:C
.∀d:nat
.∀h:nat
.(drop h d c1 c2)→∀e2:C.(drop i0 O c2 e2)→(le d i0)→(drop (plus i0 h) O c1 e2)
assume c1: C
we proceed by induction on c1 to prove
∀c2:C
.∀d:nat
.∀h:nat
.drop h d c1 c2
→∀e2:C.(drop (S i0) O c2 e2)→(le d (S i0))→(drop (plus (S i0) h) O c1 e2)
case CSort : n:nat ⇒
the thesis becomes
∀c2:C
.∀d:nat
.∀h:nat
.∀H:drop h d (CSort n) c2
.∀e2:C.∀H0:(drop (S i0) O c2 e2).∀H1:(le d (S i0)).(drop (S (plus i0 h)) O (CSort n) e2)
assume c2: C
assume d: nat
assume h: nat
suppose H: drop h d (CSort n) c2
assume e2: C
suppose H0: drop (S i0) O c2 e2
suppose H1: le d (S i0)
by (drop_gen_sort . . . . H)
we proved and3 (eq C c2 (CSort n)) (eq nat h O) (eq nat d O)
we proceed by induction on the previous result to prove drop (S (plus i0 h)) O (CSort n) e2
case and3_intro : H2:eq C c2 (CSort n) H3:eq nat h O H4:eq nat d O ⇒
the thesis becomes drop (S (plus i0 h)) O (CSort n) e2
(H6)
we proceed by induction on H2 to prove drop (S i0) O (CSort n) e2
case refl_equal : ⇒
the thesis becomes the hypothesis H0
drop (S i0) O (CSort n) e2
end of H6
by (drop_gen_sort . . . . H6)
we proved and3 (eq C e2 (CSort n)) (eq nat (S i0) O) (eq nat O O)
we proceed by induction on the previous result to prove drop (S (plus i0 O)) O (CSort n) e2
case and3_intro : H7:eq C e2 (CSort n) H8:eq nat (S i0) O :eq nat O O ⇒
the thesis becomes drop (S (plus i0 O)) O (CSort n) e2
(H10)
we proceed by induction on H8 to prove <λ:nat.Prop> CASE O OF O⇒False | S ⇒True
case refl_equal : ⇒
the thesis becomes <λ:nat.Prop> CASE S i0 OF O⇒False | S ⇒True
consider I
we proved True
<λ:nat.Prop> CASE S i0 OF O⇒False | S ⇒True
<λ:nat.Prop> CASE O OF O⇒False | S ⇒True
end of H10
consider H10
we proved <λ:nat.Prop> CASE O OF O⇒False | S ⇒True
that is equivalent to False
we proceed by induction on the previous result to prove drop (S (plus i0 O)) O (CSort n) (CSort n)
we proved drop (S (plus i0 O)) O (CSort n) (CSort n)
by (eq_ind_r . . . previous . H7)
drop (S (plus i0 O)) O (CSort n) e2
we proved drop (S (plus i0 O)) O (CSort n) e2
by (eq_ind_r . . . previous . H3)
drop (S (plus i0 h)) O (CSort n) e2
we proved drop (S (plus i0 h)) O (CSort n) e2
that is equivalent to drop (plus (S i0) h) O (CSort n) e2
∀c2:C
.∀d:nat
.∀h:nat
.∀H:drop h d (CSort n) c2
.∀e2:C.∀H0:(drop (S i0) O c2 e2).∀H1:(le d (S i0)).(drop (S (plus i0 h)) O (CSort n) e2)
case CHead : c2:C k:K t:T ⇒
the thesis becomes
∀c3:C
.∀d:nat
.∀h:nat
.drop h d (CHead c2 k t) c3
→∀e2:C
.drop (S i0) O c3 e2
→(le d (S i0))→(drop (S (plus i0 h)) O (CHead c2 k t) e2)
(IHc) by induction hypothesis we know
∀c3:C
.∀d:nat
.∀h:nat
.drop h d c2 c3
→∀e2:C.(drop (S i0) O c3 e2)→(le d (S i0))→(drop (S (plus i0 h)) O c2 e2)
assume c3: C
assume d: nat
we proceed by induction on d to prove
∀h:nat
.drop h d (CHead c2 k t) c3
→∀e2:C
.drop (S i0) O c3 e2
→(le d (S i0))→(drop (S (plus i0 h)) O (CHead c2 k t) e2)
case O : ⇒
the thesis becomes
∀h:nat
.drop h O (CHead c2 k t) c3
→∀e2:C
.drop (S i0) O c3 e2
→(le O (S i0))→(drop (S (plus i0 h)) O (CHead c2 k t) e2)
assume h: nat
we proceed by induction on h to prove
drop h O (CHead c2 k t) c3
→∀e2:C
.drop (S i0) O c3 e2
→(le O (S i0))→(drop (S (plus i0 h)) O (CHead c2 k t) e2)
case O : ⇒
the thesis becomes
drop O O (CHead c2 k t) c3
→∀e2:C
.drop (S i0) O c3 e2
→(le O (S i0))→(drop (S (plus i0 O)) O (CHead c2 k t) e2)
suppose H: drop O O (CHead c2 k t) c3
assume e2: C
suppose H0: drop (S i0) O c3 e2
suppose : le O (S i0)
(H2)
by (drop_gen_refl . . H)
we proved eq C (CHead c2 k t) c3
by (eq_ind_r . . . H0 . previous)
drop (S i0) O (CHead c2 k t) e2
end of H2
by (plus_n_O .)
we proved eq nat i0 (plus i0 O)
we proceed by induction on the previous result to prove drop (S (plus i0 O)) O (CHead c2 k t) e2
case refl_equal : ⇒
the thesis becomes drop (S i0) O (CHead c2 k t) e2
by (drop_gen_drop . . . . . H2)
we proved drop (r k i0) O c2 e2
by (drop_drop . . . . previous .)
drop (S i0) O (CHead c2 k t) e2
we proved drop (S (plus i0 O)) O (CHead c2 k t) e2
drop O O (CHead c2 k t) c3
→∀e2:C
.drop (S i0) O c3 e2
→(le O (S i0))→(drop (S (plus i0 O)) O (CHead c2 k t) e2)
case S : n:nat ⇒
the thesis becomes
∀H0:drop (S n) O (CHead c2 k t) c3
.∀e2:C
.∀H1:drop (S i0) O c3 e2
.∀H2:(le O (S i0)).(drop (S (plus i0 (S n))) O (CHead c2 k t) e2)
() by induction hypothesis we know
drop n O (CHead c2 k t) c3
→∀e2:C
.drop (S i0) O c3 e2
→(le O (S i0))→(drop (S (plus i0 n)) O (CHead c2 k t) e2)
suppose H0: drop (S n) O (CHead c2 k t) c3
assume e2: C
suppose H1: drop (S i0) O c3 e2
suppose H2: le O (S i0)
by (plus_n_Sm . .)
we proved eq nat (S (plus i0 n)) (plus i0 (S n))
we proceed by induction on the previous result to prove drop (S (plus i0 (S n))) O (CHead c2 k t) e2
case refl_equal : ⇒
the thesis becomes drop (S (S (plus i0 n))) O (CHead c2 k t) e2
(h1)
(h1)
by (drop_gen_drop . . . . . H0)
we proved drop (r k n) O c2 c3
by (IHc . . . previous . H1 H2)
drop (S (plus i0 (r k n))) O c2 e2
end of h1
(h2)
by (r_plus_sym . . .)
eq nat (r k (plus i0 n)) (plus i0 (r k n))
end of h2
by (eq_ind_r . . . h1 . h2)
drop (S (r k (plus i0 n))) O c2 e2
end of h1
(h2)
by (r_S . .)
eq nat (r k (S (plus i0 n))) (S (r k (plus i0 n)))
end of h2
by (eq_ind_r . . . h1 . h2)
we proved drop (r k (S (plus i0 n))) O c2 e2
by (drop_drop . . . . previous .)
drop (S (S (plus i0 n))) O (CHead c2 k t) e2
we proved drop (S (plus i0 (S n))) O (CHead c2 k t) e2
∀H0:drop (S n) O (CHead c2 k t) c3
.∀e2:C
.∀H1:drop (S i0) O c3 e2
.∀H2:(le O (S i0)).(drop (S (plus i0 (S n))) O (CHead c2 k t) e2)
we proved
drop h O (CHead c2 k t) c3
→∀e2:C
.drop (S i0) O c3 e2
→(le O (S i0))→(drop (S (plus i0 h)) O (CHead c2 k t) e2)
∀h:nat
.drop h O (CHead c2 k t) c3
→∀e2:C
.drop (S i0) O c3 e2
→(le O (S i0))→(drop (S (plus i0 h)) O (CHead c2 k t) e2)
case S : d0:nat ⇒
the thesis becomes
∀h:nat
.∀H:drop h (S d0) (CHead c2 k t) c3
.∀e2:C
.∀H0:(drop (S i0) O c3 e2).∀H1:(le (S d0) (S i0)).(drop (S (plus i0 h)) O (CHead c2 k t) e2)
(IHd) by induction hypothesis we know
∀h:nat
.drop h d0 (CHead c2 k t) c3
→∀e2:C
.drop (S i0) O c3 e2
→(le d0 (S i0))→(drop (S (plus i0 h)) O (CHead c2 k t) e2)
assume h: nat
suppose H: drop h (S d0) (CHead c2 k t) c3
assume e2: C
suppose H0: drop (S i0) O c3 e2
suppose H1: le (S d0) (S i0)
by (drop_gen_skip_l . . . . . . H)
we proved
ex3_2
C
T
λe:C.λv:T.eq C c3 (CHead e k v)
λ:C.λv:T.eq T t (lift h (r k d0) v)
λe:C.λ:T.drop h (r k d0) c2 e
we proceed by induction on the previous result to prove drop (S (plus i0 h)) O (CHead c2 k t) e2
case ex3_2_intro : x0:C x1:T H2:eq C c3 (CHead x0 k x1) H3:eq T t (lift h (r k d0) x1) H4:drop h (r k d0) c2 x0 ⇒
the thesis becomes drop (S (plus i0 h)) O (CHead c2 k t) e2
(H5)
we proceed by induction on H2 to prove
∀h0:nat
.drop h0 d0 (CHead c2 k t) (CHead x0 k x1)
→∀e3:C
.drop (S i0) O (CHead x0 k x1) e3
→(le d0 (S i0))→(drop (S (plus i0 h0)) O (CHead c2 k t) e3)
case refl_equal : ⇒
the thesis becomes the hypothesis IHd
∀h0:nat
.drop h0 d0 (CHead c2 k t) (CHead x0 k x1)
→∀e3:C
.drop (S i0) O (CHead x0 k x1) e3
→(le d0 (S i0))→(drop (S (plus i0 h0)) O (CHead c2 k t) e3)
end of H5
(H6)
we proceed by induction on H2 to prove drop (S i0) O (CHead x0 k x1) e2
case refl_equal : ⇒
the thesis becomes the hypothesis H0
drop (S i0) O (CHead x0 k x1) e2
end of H6
by (drop_gen_drop . . . . . H6)
we proved drop (r k i0) O x0 e2
assume b: B
suppose H8: drop h (r (Bind b) d0) c2 x0
suppose H9: drop (r (Bind b) i0) O x0 e2
(h1)
consider H9
we proved drop (r (Bind b) i0) O x0 e2
drop i0 O x0 e2
end of h1
(h2)
consider H1
we proved le (S d0) (S i0)
that is equivalent to le (S (r (Bind b) d0)) (S i0)
by (le_S_n . . previous)
le (r (Bind b) d0) i0
end of h2
by (IHi . . . . H8 . h1 h2)
we proved drop (plus i0 h) O c2 e2
that is equivalent to drop (r (Bind b) (plus i0 h)) O c2 e2
∀H8:drop h (r (Bind b) d0) c2 x0
.∀H9:(drop (r (Bind b) i0) O x0 e2).(drop (plus i0 h) O c2 e2)
assume f: F
suppose H8: drop h (r (Flat f) d0) c2 x0
suppose H9: drop (r (Flat f) i0) O x0 e2
(h1)
consider H9
we proved drop (r (Flat f) i0) O x0 e2
drop (S i0) O x0 e2
end of h1
(h2)
consider H1
we proved le (S d0) (S i0)
le (r (Flat f) d0) (S i0)
end of h2
by (IHc . . . H8 . h1 h2)
we proved drop (S (plus i0 h)) O c2 e2
that is equivalent to drop (r (Flat f) (plus i0 h)) O c2 e2
∀H8:drop h (r (Flat f) d0) c2 x0
.∀H9:(drop (r (Flat f) i0) O x0 e2).(drop (S (plus i0 h)) O c2 e2)
by (previous . H4 previous)
we proved drop (r k (plus i0 h)) O c2 e2
by (drop_drop . . . . previous .)
we proved drop (S (plus i0 h)) O (CHead c2 k (lift h (r k d0) x1)) e2
by (eq_ind_r . . . previous . H3)
drop (S (plus i0 h)) O (CHead c2 k t) e2
we proved drop (S (plus i0 h)) O (CHead c2 k t) e2
∀h:nat
.∀H:drop h (S d0) (CHead c2 k t) c3
.∀e2:C
.∀H0:(drop (S i0) O c3 e2).∀H1:(le (S d0) (S i0)).(drop (S (plus i0 h)) O (CHead c2 k t) e2)
we proved
∀h:nat
.drop h d (CHead c2 k t) c3
→∀e2:C
.drop (S i0) O c3 e2
→(le d (S i0))→(drop (S (plus i0 h)) O (CHead c2 k t) e2)
that is equivalent to
∀h:nat
.drop h d (CHead c2 k t) c3
→∀e2:C
.drop (S i0) O c3 e2
→(le d (S i0))→(drop (plus (S i0) h) O (CHead c2 k t) e2)
∀c3:C
.∀d:nat
.∀h:nat
.drop h d (CHead c2 k t) c3
→∀e2:C
.drop (S i0) O c3 e2
→(le d (S i0))→(drop (S (plus i0 h)) O (CHead c2 k t) e2)
we proved
∀c2:C
.∀d:nat
.∀h:nat
.drop h d c1 c2
→∀e2:C.(drop (S i0) O c2 e2)→(le d (S i0))→(drop (plus (S i0) h) O c1 e2)
∀c1:C
.∀c2:C
.∀d:nat
.∀h:nat
.drop h d c1 c2
→∀e2:C.(drop (S i0) O c2 e2)→(le d (S i0))→(drop (plus (S i0) h) O c1 e2)
we proved
∀c1:C
.∀c2:C
.∀d:nat
.∀h:nat
.drop h d c1 c2
→∀e2:C.(drop i O c2 e2)→(le d i)→(drop (plus i h) O c1 e2)
we proved
∀i:nat
.∀c1:C
.∀c2:C
.∀d:nat
.∀h:nat
.drop h d c1 c2
→∀e2:C.(drop i O c2 e2)→(le d i)→(drop (plus i h) O c1 e2)