DEFINITION drop_gen_drop()
TYPE =
∀k:K
.∀c:C
.∀x:C.∀u:T.∀h:nat.(drop (S h) O (CHead c k u) x)→(drop (r k h) O c x)
BODY =
assume k: K
assume c: C
assume x: C
assume u: T
assume h: nat
suppose H: drop (S h) O (CHead c k u) x
assume y: C
suppose H0: drop (S h) O y x
assume y0: nat
suppose H1: drop (S h) y0 y x
assume y1: nat
suppose H2: drop y1 y0 y x
we proceed by induction on H2 to prove
eq nat y1 (S h)
→(eq nat y0 O)→(eq C y (CHead c k u))→(drop (r k h) y0 c x)
case drop_refl : c0:C ⇒
the thesis becomes
∀H3:eq nat O (S h)
.(eq nat O O)→∀H5:(eq C c0 (CHead c k u)).(drop (r k h) O c c0)
suppose H3: eq nat O (S h)
suppose : eq nat O O
suppose H5: eq C c0 (CHead c k u)
(H6)
we proceed by induction on H3 to prove <λ:nat.Prop> CASE S h OF O⇒True | S ⇒False
case refl_equal : ⇒
the thesis becomes <λ:nat.Prop> CASE O OF O⇒True | S ⇒False
consider I
we proved True
<λ:nat.Prop> CASE O OF O⇒True | S ⇒False
<λ:nat.Prop> CASE S h OF O⇒True | S ⇒False
end of H6
consider H6
we proved <λ:nat.Prop> CASE S h OF O⇒True | S ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove drop (r k h) O c (CHead c k u)
we proved drop (r k h) O c (CHead c k u)
by (eq_ind_r . . . previous . H5)
we proved drop (r k h) O c c0
∀H3:eq nat O (S h)
.(eq nat O O)→∀H5:(eq C c0 (CHead c k u)).(drop (r k h) O c c0)
case drop_drop : k0:K h0:nat c0:C e:C H3:drop (r k0 h0) O c0 e u0:T ⇒
the thesis becomes
∀H5:eq nat (S h0) (S h)
.eq nat O O
→∀H7:(eq C (CHead c0 k0 u0) (CHead c k u)).(drop (r k h) O c e)
(H4) by induction hypothesis we know
eq nat (r k0 h0) (S h)
→(eq nat O O)→(eq C c0 (CHead c k u))→(drop (r k h) O c e)
suppose H5: eq nat (S h0) (S h)
suppose : eq nat O O
suppose H7: eq C (CHead c0 k0 u0) (CHead c k u)
(H8)
by (f_equal . . . . . H7)
we proved
eq
C
<λ:C.C> CASE CHead c0 k0 u0 OF CSort ⇒c0 | CHead c1 ⇒c1
<λ:C.C> CASE CHead c k u OF CSort ⇒c0 | CHead c1 ⇒c1
eq
C
λe0:C.<λ:C.C> CASE e0 OF CSort ⇒c0 | CHead c1 ⇒c1 (CHead c0 k0 u0)
λe0:C.<λ:C.C> CASE e0 OF CSort ⇒c0 | CHead c1 ⇒c1 (CHead c k u)
end of H8
(h1)
(H9)
by (f_equal . . . . . H7)
we proved
eq
K
<λ:C.K> CASE CHead c0 k0 u0 OF CSort ⇒k0 | CHead k1 ⇒k1
<λ:C.K> CASE CHead c k u OF CSort ⇒k0 | CHead k1 ⇒k1
eq
K
λe0:C.<λ:C.K> CASE e0 OF CSort ⇒k0 | CHead k1 ⇒k1 (CHead c0 k0 u0)
λe0:C.<λ:C.K> CASE e0 OF CSort ⇒k0 | CHead k1 ⇒k1 (CHead c k u)
end of H9
(H11)
consider H9
we proved
eq
K
<λ:C.K> CASE CHead c0 k0 u0 OF CSort ⇒k0 | CHead k1 ⇒k1
<λ:C.K> CASE CHead c k u OF CSort ⇒k0 | CHead k1 ⇒k1
eq K k0 k
end of H11
suppose H12: eq C c0 c
(H13)
we proceed by induction on H12 to prove
eq nat (r k0 h0) (S h)
→(eq nat O O)→(eq C c (CHead c k u))→(drop (r k h) O c e)
case refl_equal : ⇒
the thesis becomes the hypothesis H4
eq nat (r k0 h0) (S h)
→(eq nat O O)→(eq C c (CHead c k u))→(drop (r k h) O c e)
end of H13
(H14)
we proceed by induction on H12 to prove drop (r k0 h0) O c e
case refl_equal : ⇒
the thesis becomes the hypothesis H3
drop (r k0 h0) O c e
end of H14
(H15)
we proceed by induction on H11 to prove
eq nat (r k h0) (S h)
→(eq nat O O)→(eq C c (CHead c k u))→(drop (r k h) O c e)
case refl_equal : ⇒
the thesis becomes the hypothesis H13
eq nat (r k h0) (S h)
→(eq nat O O)→(eq C c (CHead c k u))→(drop (r k h) O c e)
end of H15
(H16)
we proceed by induction on H11 to prove drop (r k h0) O c e
case refl_equal : ⇒
the thesis becomes the hypothesis H14
drop (r k h0) O c e
end of H16
(H17)
by (f_equal . . . . . H5)
we proved
eq
nat
<λ:nat.nat> CASE S h0 OF O⇒h0 | S n⇒n
<λ:nat.nat> CASE S h OF O⇒h0 | S n⇒n
eq
nat
λe0:nat.<λ:nat.nat> CASE e0 OF O⇒h0 | S n⇒n (S h0)
λe0:nat.<λ:nat.nat> CASE e0 OF O⇒h0 | S n⇒n (S h)
end of H17
(H19)
consider H17
we proved
eq
nat
<λ:nat.nat> CASE S h0 OF O⇒h0 | S n⇒n
<λ:nat.nat> CASE S h OF O⇒h0 | S n⇒n
that is equivalent to eq nat h0 h
we proceed by induction on the previous result to prove drop (r k h) O c e
case refl_equal : ⇒
the thesis becomes the hypothesis H16
drop (r k h) O c e
end of H19
consider H19
we proved drop (r k h) O c e
(eq C c0 c)→(drop (r k h) O c e)
end of h1
(h2)
consider H8
we proved
eq
C
<λ:C.C> CASE CHead c0 k0 u0 OF CSort ⇒c0 | CHead c1 ⇒c1
<λ:C.C> CASE CHead c k u OF CSort ⇒c0 | CHead c1 ⇒c1
eq C c0 c
end of h2
by (h1 h2)
we proved drop (r k h) O c e
∀H5:eq nat (S h0) (S h)
.eq nat O O
→∀H7:(eq C (CHead c0 k0 u0) (CHead c k u)).(drop (r k h) O c e)
case drop_skip : k0:K h0:nat d:nat c0:C e:C H3:drop h0 (r k0 d) c0 e u0:T ⇒
the thesis becomes
∀H5:eq nat h0 (S h)
.∀H6:eq nat (S d) O
.∀H7:eq C (CHead c0 k0 (lift h0 (r k0 d) u0)) (CHead c k u)
.drop (r k h) (S d) c (CHead e k0 u0)
(H4) by induction hypothesis we know
eq nat h0 (S h)
→(eq nat (r k0 d) O
→(eq C c0 (CHead c k u))→(drop (r k h) (r k0 d) c e))
suppose H5: eq nat h0 (S h)
suppose H6: eq nat (S d) O
suppose H7: eq C (CHead c0 k0 (lift h0 (r k0 d) u0)) (CHead c k u)
(H8)
we proceed by induction on H5 to prove eq C (CHead c0 k0 (lift (S h) (r k0 d) u0)) (CHead c k u)
case refl_equal : ⇒
the thesis becomes the hypothesis H7
eq C (CHead c0 k0 (lift (S h) (r k0 d) u0)) (CHead c k u)
end of H8
(H9)
we proceed by induction on H5 to prove
eq nat (S h) (S h)
→(eq nat (r k0 d) O
→(eq C c0 (CHead c k u))→(drop (r k h) (r k0 d) c e))
case refl_equal : ⇒
the thesis becomes the hypothesis H4
eq nat (S h) (S h)
→(eq nat (r k0 d) O
→(eq C c0 (CHead c k u))→(drop (r k h) (r k0 d) c e))
end of H9
(H10)
we proceed by induction on H5 to prove drop (S h) (r k0 d) c0 e
case refl_equal : ⇒
the thesis becomes the hypothesis H3
drop (S h) (r k0 d) c0 e
end of H10
(H11)
by (f_equal . . . . . H8)
we proved
eq
C
<λ:C.C> CASE CHead c0 k0 (lift (S h) (r k0 d) u0) OF CSort ⇒c0 | CHead c1 ⇒c1
<λ:C.C> CASE CHead c k u OF CSort ⇒c0 | CHead c1 ⇒c1
eq
C
λe0:C.<λ:C.C> CASE e0 OF CSort ⇒c0 | CHead c1 ⇒c1 (CHead c0 k0 (lift (S h) (r k0 d) u0))
λe0:C.<λ:C.C> CASE e0 OF CSort ⇒c0 | CHead c1 ⇒c1 (CHead c k u)
end of H11
(h1)
(H12)
by (f_equal . . . . . H8)
we proved
eq
K
<λ:C.K> CASE CHead c0 k0 (lift (S h) (r k0 d) u0) OF CSort ⇒k0 | CHead k1 ⇒k1
<λ:C.K> CASE CHead c k u OF CSort ⇒k0 | CHead k1 ⇒k1
eq
K
λe0:C.<λ:C.K> CASE e0 OF CSort ⇒k0 | CHead k1 ⇒k1 (CHead c0 k0 (lift (S h) (r k0 d) u0))
λe0:C.<λ:C.K> CASE e0 OF CSort ⇒k0 | CHead k1 ⇒k1 (CHead c k u)
end of H12
(h1)
(H13)
by (f_equal . . . . . H8)
we proved
eq
T
<λ:C.T>
CASE CHead c0 k0 (lift (S h) (r k0 d) u0) OF
CSort ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd0:nat
.λt:T
.<λt1:T.T>
CASE t OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb:bool.nat> CASE blt i d0 OF true⇒i | false⇒f i
| THead k1 u1 t0⇒THead k1 (lref_map f d0 u1) (lref_map f (s k1 d0) t0)
}
λx0:nat.plus x0 (S h)
r k0 d
u0
| CHead t⇒t
<λ:C.T>
CASE CHead c k u OF
CSort ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd0:nat
.λt:T
.<λt1:T.T>
CASE t OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb:bool.nat> CASE blt i d0 OF true⇒i | false⇒f i
| THead k1 u1 t0⇒THead k1 (lref_map f d0 u1) (lref_map f (s k1 d0) t0)
}
λx0:nat.plus x0 (S h)
r k0 d
u0
| CHead t⇒t
eq
T
λe0:C
.<λ:C.T>
CASE e0 OF
CSort ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd0:nat
.λt:T
.<λt1:T.T>
CASE t OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb:bool.nat> CASE blt i d0 OF true⇒i | false⇒f i
| THead k1 u1 t0⇒THead k1 (lref_map f d0 u1) (lref_map f (s k1 d0) t0)
}
λx0:nat.plus x0 (S h)
r k0 d
u0
| CHead t⇒t
CHead c0 k0 (lift (S h) (r k0 d) u0)
λe0:C
.<λ:C.T>
CASE e0 OF
CSort ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd0:nat
.λt:T
.<λt1:T.T>
CASE t OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb:bool.nat> CASE blt i d0 OF true⇒i | false⇒f i
| THead k1 u1 t0⇒THead k1 (lref_map f d0 u1) (lref_map f (s k1 d0) t0)
}
λx0:nat.plus x0 (S h)
r k0 d
u0
| CHead t⇒t
CHead c k u
end of H13
suppose H14: eq K k0 k
suppose H15: eq C c0 c
(H16)
we proceed by induction on H15 to prove
eq nat (S h) (S h)
→(eq nat (r k0 d) O
→(eq C c (CHead c k u))→(drop (r k h) (r k0 d) c e))
case refl_equal : ⇒
the thesis becomes the hypothesis H9
eq nat (S h) (S h)
→(eq nat (r k0 d) O
→(eq C c (CHead c k u))→(drop (r k h) (r k0 d) c e))
end of H16
(H17)
we proceed by induction on H15 to prove drop (S h) (r k0 d) c e
case refl_equal : ⇒
the thesis becomes the hypothesis H10
drop (S h) (r k0 d) c e
end of H17
(H18)
we proceed by induction on H14 to prove eq T (lift (S h) (r k d) u0) u
case refl_equal : ⇒
the thesis becomes eq T (lift (S h) (r k0 d) u0) u
consider H13
we proved
eq
T
<λ:C.T>
CASE CHead c0 k0 (lift (S h) (r k0 d) u0) OF
CSort ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd0:nat
.λt:T
.<λt1:T.T>
CASE t OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb:bool.nat> CASE blt i d0 OF true⇒i | false⇒f i
| THead k1 u1 t0⇒THead k1 (lref_map f d0 u1) (lref_map f (s k1 d0) t0)
}
λx0:nat.plus x0 (S h)
r k0 d
u0
| CHead t⇒t
<λ:C.T>
CASE CHead c k u OF
CSort ⇒
FIXlref_map{
lref_map:(nat→nat)→nat→T→T
:=λf:nat→nat
.λd0:nat
.λt:T
.<λt1:T.T>
CASE t OF
TSort n⇒TSort n
| TLRef i⇒TLRef <λb:bool.nat> CASE blt i d0 OF true⇒i | false⇒f i
| THead k1 u1 t0⇒THead k1 (lref_map f d0 u1) (lref_map f (s k1 d0) t0)
}
λx0:nat.plus x0 (S h)
r k0 d
u0
| CHead t⇒t
eq T (lift (S h) (r k0 d) u0) u
eq T (lift (S h) (r k d) u0) u
end of H18
(H19)
we proceed by induction on H14 to prove
eq nat (S h) (S h)
→(eq nat (r k d) O
→(eq C c (CHead c k u))→(drop (r k h) (r k d) c e))
case refl_equal : ⇒
the thesis becomes the hypothesis H16
eq nat (S h) (S h)
→(eq nat (r k d) O
→(eq C c (CHead c k u))→(drop (r k h) (r k d) c e))
end of H19
(H22)
we proceed by induction on H6 to prove <λ:nat.Prop> CASE O OF O⇒False | S ⇒True
case refl_equal : ⇒
the thesis becomes <λ:nat.Prop> CASE S d OF O⇒False | S ⇒True
consider I
we proved True
<λ:nat.Prop> CASE S d OF O⇒False | S ⇒True
<λ:nat.Prop> CASE O OF O⇒False | S ⇒True
end of H22
consider H22
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 (r k h) (S d) c (CHead e k u0)
we proved drop (r k h) (S d) c (CHead e k u0)
by (eq_ind_r . . . previous . H14)
we proved drop (r k h) (S d) c (CHead e k0 u0)
(eq K k0 k)→(eq C c0 c)→(drop (r k h) (S d) c (CHead e k0 u0))
end of h1
(h2)
consider H12
we proved
eq
K
<λ:C.K> CASE CHead c0 k0 (lift (S h) (r k0 d) u0) OF CSort ⇒k0 | CHead k1 ⇒k1
<λ:C.K> CASE CHead c k u OF CSort ⇒k0 | CHead k1 ⇒k1
eq K k0 k
end of h2
by (h1 h2)
(eq C c0 c)→(drop (r k h) (S d) c (CHead e k0 u0))
end of h1
(h2)
consider H11
we proved
eq
C
<λ:C.C> CASE CHead c0 k0 (lift (S h) (r k0 d) u0) OF CSort ⇒c0 | CHead c1 ⇒c1
<λ:C.C> CASE CHead c k u OF CSort ⇒c0 | CHead c1 ⇒c1
eq C c0 c
end of h2
by (h1 h2)
we proved drop (r k h) (S d) c (CHead e k0 u0)
∀H5:eq nat h0 (S h)
.∀H6:eq nat (S d) O
.∀H7:eq C (CHead c0 k0 (lift h0 (r k0 d) u0)) (CHead c k u)
.drop (r k h) (S d) c (CHead e k0 u0)
we proved
eq nat y1 (S h)
→(eq nat y0 O)→(eq C y (CHead c k u))→(drop (r k h) y0 c x)
we proved
∀y1:nat
.drop y1 y0 y x
→(eq nat y1 (S h)
→(eq nat y0 O)→(eq C y (CHead c k u))→(drop (r k h) y0 c x))
by (insert_eq . . . . previous H1)
we proved (eq nat y0 O)→(eq C y (CHead c k u))→(drop (r k h) y0 c x)
we proved
∀y0:nat
.drop (S h) y0 y x
→(eq nat y0 O)→(eq C y (CHead c k u))→(drop (r k h) y0 c x)
by (insert_eq . . . . previous H0)
we proved (eq C y (CHead c k u))→(drop (r k h) O c x)
we proved
∀y:C
.drop (S h) O y x
→(eq C y (CHead c k u))→(drop (r k h) O c x)
by (insert_eq . . . . previous H)
we proved drop (r k h) O c x
we proved
∀k:K
.∀c:C
.∀x:C.∀u:T.∀h:nat.(drop (S h) O (CHead c k u) x)→(drop (r k h) O c x)