DEFINITION drop_conf_ge()
TYPE =
∀i:nat
.∀a:C
.∀c:C
.drop i O c a
→∀e:C
.∀h:nat
.∀d:nat
.drop h d c e
→(le (plus d h) i)→(drop (minus i h) O e a)
BODY =
assume i: nat
we proceed by induction on i to prove
∀a:C
.∀c:C
.drop i O c a
→∀e:C
.∀h:nat
.∀d:nat
.drop h d c e
→(le (plus d h) i)→(drop (minus i h) O e a)
case O : ⇒
the thesis becomes
∀a:C
.∀c:C
.drop O O c a
→∀e:C
.∀h:nat
.∀d:nat
.drop h d c e
→(le (plus d h) O)→(drop (minus O h) O e a)
assume a: C
assume c: C
suppose H: drop O O c a
assume e: C
assume h: nat
assume d: nat
suppose H0: drop h d c e
suppose H1: le (plus d h) O
(H2)
by (drop_gen_refl . . H)
we proved eq C c a
we proceed by induction on the previous result to prove drop h d a e
case refl_equal : ⇒
the thesis becomes the hypothesis H0
drop h d a e
end of H2
(H_y)
by (le_n_O_eq . H1)
eq nat O (plus d h)
end of H_y
by (sym_eq . . . H_y)
we proved eq nat (plus d h) O
by (plus_O . . previous)
we proved land (eq nat d O) (eq nat h O)
we proceed by induction on the previous result to prove drop (minus O h) O e a
case conj : H3:eq nat d O H4:eq nat h O ⇒
the thesis becomes drop (minus O h) O e a
(H5)
we proceed by induction on H3 to prove drop h O a e
case refl_equal : ⇒
the thesis becomes the hypothesis H2
drop h O a e
end of H5
(H6)
we proceed by induction on H4 to prove drop O O a e
case refl_equal : ⇒
the thesis becomes the hypothesis H5
drop O O a e
end of H6
by (drop_gen_refl . . H6)
we proved eq C a e
we proceed by induction on the previous result to prove drop (minus O O) O e a
case refl_equal : ⇒
the thesis becomes drop (minus O O) O a a
by (drop_refl .)
we proved drop O O a a
drop (minus O O) O a a
we proved drop (minus O O) O e a
by (eq_ind_r . . . previous . H4)
drop (minus O h) O e a
we proved drop (minus O h) O e a
∀a:C
.∀c:C
.drop O O c a
→∀e:C
.∀h:nat
.∀d:nat
.drop h d c e
→(le (plus d h) O)→(drop (minus O h) O e a)
case S : i0:nat ⇒
the thesis becomes
∀a:C
.∀c:C
.drop (S i0) O c a
→∀e:C
.∀h:nat
.∀d:nat
.drop h d c e
→(le (plus d h) (S i0))→(drop (minus (S i0) h) O e a)
(H) by induction hypothesis we know
∀a:C
.∀c:C
.drop i0 O c a
→∀e:C
.∀h:nat
.∀d:nat
.(drop h d c e)→(le (plus d h) i0)→(drop (minus i0 h) O e a)
assume a: C
assume c: C
we proceed by induction on c to prove
drop (S i0) O c a
→∀e:C
.∀h:nat
.∀d:nat
.drop h d c e
→(le (plus d h) (S i0))→(drop (minus (S i0) h) O e a)
case CSort : n:nat ⇒
the thesis becomes
∀H0:drop (S i0) O (CSort n) a
.∀e:C
.∀h:nat
.∀d:nat
.∀H1:drop h d (CSort n) e
.∀H2:(le (plus d h) (S i0)).(drop (minus (S i0) h) O e a)
suppose H0: drop (S i0) O (CSort n) a
assume e: C
assume h: nat
assume d: nat
suppose H1: drop h d (CSort n) e
suppose H2: le (plus d h) (S i0)
by (drop_gen_sort . . . . H1)
we proved and3 (eq C e (CSort n)) (eq nat h O) (eq nat d O)
we proceed by induction on the previous result to prove drop (minus (S i0) h) O e a
case and3_intro : H3:eq C e (CSort n) H4:eq nat h O H5:eq nat d O ⇒
the thesis becomes drop (minus (S i0) h) O e a
by (drop_gen_sort . . . . H0)
we proved and3 (eq C a (CSort n)) (eq nat (S i0) O) (eq nat O O)
we proceed by induction on the previous result to prove drop (minus (S i0) h) O e a
case and3_intro : H6:eq C a (CSort n) H7:eq nat (S i0) O :eq nat O O ⇒
the thesis becomes drop (minus (S i0) h) O e a
(H9)
we proceed by induction on H5 to prove le (plus O h) (S i0)
case refl_equal : ⇒
the thesis becomes the hypothesis H2
le (plus O h) (S i0)
end of H9
(H11)
we proceed by induction on H7 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 H11
consider H11
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 (minus (S i0) O) O (CSort n) (CSort n)
we proved drop (minus (S i0) O) O (CSort n) (CSort n)
by (eq_ind_r . . . previous . H6)
we proved drop (minus (S i0) O) O (CSort n) a
by (eq_ind_r . . . previous . H3)
we proved drop (minus (S i0) O) O e a
by (eq_ind_r . . . previous . H4)
drop (minus (S i0) h) O e a
drop (minus (S i0) h) O e a
we proved drop (minus (S i0) h) O e a
∀H0:drop (S i0) O (CSort n) a
.∀e:C
.∀h:nat
.∀d:nat
.∀H1:drop h d (CSort n) e
.∀H2:(le (plus d h) (S i0)).(drop (minus (S i0) h) O e a)
case CHead ⇒
we need to prove
∀c0:C
.drop (S i0) O c0 a
→∀e:C
.∀h:nat
.∀d:nat
.drop h d c0 e
→(le (plus d h) (S i0))→(drop (minus (S i0) h) O e a)
→∀k:K
.∀t:T
.drop (S i0) O (CHead c0 k t) a
→∀e:C
.∀h:nat
.∀d:nat
.drop h d (CHead c0 k t) e
→(le (plus d h) (S i0))→(drop (minus (S i0) h) O e a)
assume c0: C
suppose H0:
drop (S i0) O c0 a
→∀e:C
.∀h:nat
.∀d:nat
.drop h d c0 e
→(le (plus d h) (S i0))→(drop (minus (S i0) h) O e a)
assume k: K
we proceed by induction on k to prove
∀t:T
.drop (S i0) O (CHead c0 k t) a
→∀e:C
.∀h:nat
.∀d:nat
.drop h d (CHead c0 k t) e
→(le (plus d h) (S i0))→(drop (minus (S i0) h) O e a)
case Bind : b:B ⇒
the thesis becomes
∀t:T
.∀H1:drop (S i0) O (CHead c0 (Bind b) t) a
.∀e:C
.∀h:nat
.∀d:nat
.∀H2:drop h d (CHead c0 (Bind b) t) e
.∀H3:(le (plus d h) (S i0)).(drop (minus (S i0) h) O e a)
assume t: T
suppose H1: drop (S i0) O (CHead c0 (Bind b) t) a
assume e: C
assume h: nat
assume d: nat
suppose H2: drop h d (CHead c0 (Bind b) t) e
suppose H3: le (plus d h) (S i0)
suppose H4: drop h O (CHead c0 (Bind b) t) e
suppose H5: le (plus O h) (S i0)
suppose H6: drop O O (CHead c0 (Bind b) t) e
suppose : le (plus O O) (S i0)
by (drop_gen_refl . . H6)
we proved eq C (CHead c0 (Bind b) t) e
we proceed by induction on the previous result to prove drop (minus (S i0) O) O e a
case refl_equal : ⇒
the thesis becomes drop (minus (S i0) O) O (CHead c0 (Bind b) t) a
by (drop_gen_drop . . . . . H1)
we proved drop (r (Bind b) i0) O c0 a
by (drop_drop . . . . previous .)
we proved drop (S i0) O (CHead c0 (Bind b) t) a
drop (minus (S i0) O) O (CHead c0 (Bind b) t) a
we proved drop (minus (S i0) O) O e a
drop O O (CHead c0 (Bind b) t) e
→(le (plus O O) (S i0))→(drop (minus (S i0) O) O e a)
assume h0: nat
suppose :
drop h0 O (CHead c0 (Bind b) t) e
→(le (plus O h0) (S i0))→(drop (minus (S i0) h0) O e a)
suppose H6: drop (S h0) O (CHead c0 (Bind b) t) e
suppose H7: le (plus O (S h0)) (S i0)
(h1)
by (drop_gen_drop . . . . . H1)
we proved drop (r (Bind b) i0) O c0 a
drop i0 O c0 a
end of h1
(h2)
by (drop_gen_drop . . . . . H6)
we proved drop (r (Bind b) h0) O c0 e
drop h0 O c0 e
end of h2
(h3)
consider H7
we proved le (plus O (S h0)) (S i0)
that is equivalent to le (S (plus O h0)) (S i0)
by (le_S_n . . previous)
le (plus O h0) i0
end of h3
by (H . . h1 . . . h2 h3)
we proved drop (minus i0 h0) O e a
that is equivalent to drop (minus (S i0) (S h0)) O e a
∀H6:drop (S h0) O (CHead c0 (Bind b) t) e
.∀H7:(le (plus O (S h0)) (S i0)).(drop (minus i0 h0) O e a)
by (previous . H4 H5)
we proved drop (minus (S i0) h) O e a
drop h O (CHead c0 (Bind b) t) e
→(le (plus O h) (S i0))→(drop (minus (S i0) h) O e a)
assume d0: nat
suppose :
drop h d0 (CHead c0 (Bind b) t) e
→(le (plus d0 h) (S i0))→(drop (minus (S i0) h) O e a)
suppose H4: drop h (S d0) (CHead c0 (Bind b) t) e
suppose H5: le (plus (S d0) h) (S i0)
by (drop_gen_skip_l . . . . . . H4)
we proved
ex3_2
C
T
λe:C.λv:T.eq C e (CHead e (Bind b) v)
λ:C.λv:T.eq T t (lift h (r (Bind b) d0) v)
λe:C.λ:T.drop h (r (Bind b) d0) c0 e
we proceed by induction on the previous result to prove drop (minus (S i0) h) O e a
case ex3_2_intro : x0:C x1:T H6:eq C e (CHead x0 (Bind b) x1) :eq T t (lift h (r (Bind b) d0) x1) H8:drop h (r (Bind b) d0) c0 x0 ⇒
the thesis becomes drop (minus (S i0) h) O e a
consider H5
we proved le (plus (S d0) h) (S i0)
that is equivalent to le (S (plus d0 h)) (S i0)
by (le_S_n . . previous)
we proved le (plus d0 h) i0
by (le_trans_plus_r . . . previous)
we proved le h i0
by (minus_Sn_m . . previous)
we proved eq nat (S (minus i0 h)) (minus (S i0) h)
we proceed by induction on the previous result to prove drop (minus (S i0) h) O (CHead x0 (Bind b) x1) a
case refl_equal : ⇒
the thesis becomes drop (S (minus i0 h)) O (CHead x0 (Bind b) x1) a
(h1)
by (drop_gen_drop . . . . . H1)
we proved drop (r (Bind b) i0) O c0 a
drop i0 O c0 a
end of h1
(h2)
consider H8
we proved drop h (r (Bind b) d0) c0 x0
drop h d0 c0 x0
end of h2
(h3)
consider H5
we proved le (plus (S d0) h) (S i0)
that is equivalent to le (S (plus d0 h)) (S i0)
by (le_S_n . . previous)
le (plus d0 h) i0
end of h3
by (H . . h1 . . . h2 h3)
we proved drop (minus i0 h) O x0 a
that is equivalent to drop (r (Bind b) (minus i0 h)) O x0 a
by (drop_drop . . . . previous .)
drop (S (minus i0 h)) O (CHead x0 (Bind b) x1) a
we proved drop (minus (S i0) h) O (CHead x0 (Bind b) x1) a
by (eq_ind_r . . . previous . H6)
drop (minus (S i0) h) O e a
we proved drop (minus (S i0) h) O e a
∀H4:drop h (S d0) (CHead c0 (Bind b) t) e
.∀H5:(le (plus (S d0) h) (S i0)).(drop (minus (S i0) h) O e a)
by (previous . H2 H3)
we proved drop (minus (S i0) h) O e a
∀t:T
.∀H1:drop (S i0) O (CHead c0 (Bind b) t) a
.∀e:C
.∀h:nat
.∀d:nat
.∀H2:drop h d (CHead c0 (Bind b) t) e
.∀H3:(le (plus d h) (S i0)).(drop (minus (S i0) h) O e a)
case Flat : f:F ⇒
the thesis becomes
∀t:T
.∀H1:drop (S i0) O (CHead c0 (Flat f) t) a
.∀e:C
.∀h:nat
.∀d:nat
.∀H2:drop h d (CHead c0 (Flat f) t) e
.∀H3:(le (plus d h) (S i0)).(drop (minus (S i0) h) O e a)
assume t: T
suppose H1: drop (S i0) O (CHead c0 (Flat f) t) a
assume e: C
assume h: nat
assume d: nat
suppose H2: drop h d (CHead c0 (Flat f) t) e
suppose H3: le (plus d h) (S i0)
suppose H4: drop h O (CHead c0 (Flat f) t) e
suppose H5: le (plus O h) (S i0)
suppose H6: drop O O (CHead c0 (Flat f) t) e
suppose : le (plus O O) (S i0)
by (drop_gen_refl . . H6)
we proved eq C (CHead c0 (Flat f) t) e
we proceed by induction on the previous result to prove drop (minus (S i0) O) O e a
case refl_equal : ⇒
the thesis becomes drop (minus (S i0) O) O (CHead c0 (Flat f) t) a
by (drop_gen_drop . . . . . H1)
we proved drop (r (Flat f) i0) O c0 a
by (drop_drop . . . . previous .)
we proved drop (S i0) O (CHead c0 (Flat f) t) a
drop (minus (S i0) O) O (CHead c0 (Flat f) t) a
we proved drop (minus (S i0) O) O e a
drop O O (CHead c0 (Flat f) t) e
→(le (plus O O) (S i0))→(drop (minus (S i0) O) O e a)
assume h0: nat
suppose :
drop h0 O (CHead c0 (Flat f) t) e
→(le (plus O h0) (S i0))→(drop (minus (S i0) h0) O e a)
suppose H6: drop (S h0) O (CHead c0 (Flat f) t) e
suppose H7: le (plus O (S h0)) (S i0)
(h1)
by (drop_gen_drop . . . . . H1)
we proved drop (r (Flat f) i0) O c0 a
drop (S i0) O c0 a
end of h1
(h2)
by (drop_gen_drop . . . . . H6)
we proved drop (r (Flat f) h0) O c0 e
drop (S h0) O c0 e
end of h2
by (H0 h1 . . . h2 H7)
we proved drop (minus (S i0) (S h0)) O e a
∀H6:drop (S h0) O (CHead c0 (Flat f) t) e
.∀H7:(le (plus O (S h0)) (S i0)).(drop (minus (S i0) (S h0)) O e a)
by (previous . H4 H5)
we proved drop (minus (S i0) h) O e a
drop h O (CHead c0 (Flat f) t) e
→(le (plus O h) (S i0))→(drop (minus (S i0) h) O e a)
assume d0: nat
suppose :
drop h d0 (CHead c0 (Flat f) t) e
→(le (plus d0 h) (S i0))→(drop (minus (S i0) h) O e a)
suppose H4: drop h (S d0) (CHead c0 (Flat f) t) e
suppose H5: le (plus (S d0) h) (S i0)
by (drop_gen_skip_l . . . . . . H4)
we proved
ex3_2
C
T
λe:C.λv:T.eq C e (CHead e (Flat f) v)
λ:C.λv:T.eq T t (lift h (r (Flat f) d0) v)
λe:C.λ:T.drop h (r (Flat f) d0) c0 e
we proceed by induction on the previous result to prove drop (minus (S i0) h) O e a
case ex3_2_intro : x0:C x1:T H6:eq C e (CHead x0 (Flat f) x1) :eq T t (lift h (r (Flat f) d0) x1) H8:drop h (r (Flat f) d0) c0 x0 ⇒
the thesis becomes drop (minus (S i0) h) O e a
(H9)
(h1)
(h1)
by (drop_gen_drop . . . . . H1)
we proved drop (r (Flat f) i0) O c0 a
drop (S i0) O c0 a
end of h1
(h2)
consider H8
we proved drop h (r (Flat f) d0) c0 x0
drop h (S d0) c0 x0
end of h2
by (H0 h1 . . . h2 H5)
drop (minus (S i0) h) O x0 a
end of h1
(h2)
consider H5
we proved le (plus (S d0) h) (S i0)
that is equivalent to le (S (plus d0 h)) (S i0)
by (le_S_n . . previous)
we proved le (plus d0 h) i0
by (le_trans_plus_r . . . previous)
we proved le h i0
by (minus_Sn_m . . previous)
eq nat (S (minus i0 h)) (minus (S i0) h)
end of h2
by (eq_ind_r . . . h1 . h2)
drop (S (minus i0 h)) O x0 a
end of H9
consider H5
we proved le (plus (S d0) h) (S i0)
that is equivalent to le (S (plus d0 h)) (S i0)
by (le_S_n . . previous)
we proved le (plus d0 h) i0
by (le_trans_plus_r . . . previous)
we proved le h i0
by (minus_Sn_m . . previous)
we proved eq nat (S (minus i0 h)) (minus (S i0) h)
we proceed by induction on the previous result to prove drop (minus (S i0) h) O (CHead x0 (Flat f) x1) a
case refl_equal : ⇒
the thesis becomes drop (S (minus i0 h)) O (CHead x0 (Flat f) x1) a
consider H9
we proved drop (S (minus i0 h)) O x0 a
that is equivalent to drop (r (Flat f) (minus i0 h)) O x0 a
by (drop_drop . . . . previous .)
drop (S (minus i0 h)) O (CHead x0 (Flat f) x1) a
we proved drop (minus (S i0) h) O (CHead x0 (Flat f) x1) a
by (eq_ind_r . . . previous . H6)
drop (minus (S i0) h) O e a
we proved drop (minus (S i0) h) O e a
∀H4:drop h (S d0) (CHead c0 (Flat f) t) e
.∀H5:(le (plus (S d0) h) (S i0)).(drop (minus (S i0) h) O e a)
by (previous . H2 H3)
we proved drop (minus (S i0) h) O e a
∀t:T
.∀H1:drop (S i0) O (CHead c0 (Flat f) t) a
.∀e:C
.∀h:nat
.∀d:nat
.∀H2:drop h d (CHead c0 (Flat f) t) e
.∀H3:(le (plus d h) (S i0)).(drop (minus (S i0) h) O e a)
we proved
∀t:T
.drop (S i0) O (CHead c0 k t) a
→∀e:C
.∀h:nat
.∀d:nat
.drop h d (CHead c0 k t) e
→(le (plus d h) (S i0))→(drop (minus (S i0) h) O e a)
∀c0:C
.drop (S i0) O c0 a
→∀e:C
.∀h:nat
.∀d:nat
.drop h d c0 e
→(le (plus d h) (S i0))→(drop (minus (S i0) h) O e a)
→∀k:K
.∀t:T
.drop (S i0) O (CHead c0 k t) a
→∀e:C
.∀h:nat
.∀d:nat
.drop h d (CHead c0 k t) e
→(le (plus d h) (S i0))→(drop (minus (S i0) h) O e a)
we proved
drop (S i0) O c a
→∀e:C
.∀h:nat
.∀d:nat
.drop h d c e
→(le (plus d h) (S i0))→(drop (minus (S i0) h) O e a)
∀a:C
.∀c:C
.drop (S i0) O c a
→∀e:C
.∀h:nat
.∀d:nat
.drop h d c e
→(le (plus d h) (S i0))→(drop (minus (S i0) h) O e a)
we proved
∀a:C
.∀c:C
.drop i O c a
→∀e:C
.∀h:nat
.∀d:nat
.drop h d c e
→(le (plus d h) i)→(drop (minus i h) O e a)
we proved
∀i:nat
.∀a:C
.∀c:C
.drop i O c a
→∀e:C
.∀h:nat
.∀d:nat
.drop h d c e
→(le (plus d h) i)→(drop (minus i h) O e a)