DEFINITION cimp_getl_conf()
TYPE =
∀c1:C
.∀c2:C
.cimp c1 c2
→∀b:B
.∀d1:C
.∀w:T
.∀i:nat
.getl i c1 (CHead d1 (Bind b) w)
→ex2 C λd2:C.cimp d1 d2 λd2:C.getl i c2 (CHead d2 (Bind b) w)
BODY =
assume c1: C
assume c2: C
we must prove
cimp c1 c2
→∀b:B
.∀d1:C
.∀w:T
.∀i:nat
.getl i c1 (CHead d1 (Bind b) w)
→ex2 C λd2:C.cimp d1 d2 λd2:C.getl i c2 (CHead d2 (Bind b) w)
or equivalently
∀b:B
.∀d1:C
.∀w:T
.∀h:nat
.getl h c1 (CHead d1 (Bind b) w)
→ex C λd2:C.getl h c2 (CHead d2 (Bind b) w)
→∀b:B
.∀d1:C
.∀w:T
.∀i:nat
.getl i c1 (CHead d1 (Bind b) w)
→ex2 C λd2:C.cimp d1 d2 λd2:C.getl i c2 (CHead d2 (Bind b) w)
suppose H:
∀b:B
.∀d1:C
.∀w:T
.∀h:nat
.getl h c1 (CHead d1 (Bind b) w)
→ex C λd2:C.getl h c2 (CHead d2 (Bind b) w)
assume b: B
assume d1: C
assume w: T
assume i: nat
suppose H0: getl i c1 (CHead d1 (Bind b) w)
(H_x)
by (H . . . . H0)
ex C λd2:C.getl i c2 (CHead d2 (Bind b) w)
end of H_x
(H1) consider H_x
we proceed by induction on H1 to prove
ex2
C
λd2:C
.∀b0:B
.∀d3:C
.∀w0:T
.∀h:nat
.getl h d1 (CHead d3 (Bind b0) w0)
→ex C λd4:C.getl h d2 (CHead d4 (Bind b0) w0)
λd2:C.getl i c2 (CHead d2 (Bind b) w)
case ex_intro : x:C H2:getl i c2 (CHead x (Bind b) w) ⇒
the thesis becomes
ex2
C
λd2:C
.∀b0:B
.∀d3:C
.∀w0:T
.∀h:nat
.getl h d1 (CHead d3 (Bind b0) w0)
→ex C λd4:C.getl h d2 (CHead d4 (Bind b0) w0)
λd2:C.getl i c2 (CHead d2 (Bind b) w)
assume b0: B
assume d0: C
assume w0: T
assume h: nat
suppose H3: getl h d1 (CHead d0 (Bind b0) w0)
(H_y)
by (getl_trans . . . . H0)
∀e2:C.(getl (S h) (CHead d1 (Bind b) w) e2)→(getl (plus (S h) i) c1 e2)
end of H_y
(H_x0)
consider H3
we proved getl h d1 (CHead d0 (Bind b0) w0)
that is equivalent to getl (r (Bind b) h) d1 (CHead d0 (Bind b0) w0)
by (getl_head . . . . previous .)
we proved getl (S h) (CHead d1 (Bind b) w) (CHead d0 (Bind b0) w0)
by (H_y . previous)
we proved getl (plus (S h) i) c1 (CHead d0 (Bind b0) w0)
by (H . . . . previous)
ex C λd2:C.getl (plus (S h) i) c2 (CHead d2 (Bind b0) w0)
end of H_x0
(H4) consider H_x0
consider H4
we proved ex C λd2:C.getl (plus (S h) i) c2 (CHead d2 (Bind b0) w0)
that is equivalent to ex C λd2:C.getl (S (plus h i)) c2 (CHead d2 (Bind b0) w0)
we proceed by induction on the previous result to prove ex C λd2:C.getl h x (CHead d2 (Bind b0) w0)
case ex_intro : x0:C H5:getl (S (plus h i)) c2 (CHead x0 (Bind b0) w0) ⇒
the thesis becomes ex C λd2:C.getl h x (CHead d2 (Bind b0) w0)
(H_y0)
by (getl_conf_le . . . H5 . . H2)
le i (S (plus h i))
→(getl
minus (S (plus h i)) i
CHead x (Bind b) w
CHead x0 (Bind b0) w0)
end of H_y0
(H6)
by (refl_equal . .)
eq nat (plus (S h) i) (plus (S h) i)
end of H6
(H7)
consider H6
we proved eq nat (plus (S h) i) (plus (S h) i)
that is equivalent to eq nat (S (plus h i)) (plus (S h) i)
we proceed by induction on the previous result to prove
getl
minus (plus (S h) i) i
CHead x (Bind b) w
CHead x0 (Bind b0) w0
case refl_equal : ⇒
the thesis becomes
getl
minus (S (plus h i)) i
CHead x (Bind b) w
CHead x0 (Bind b0) w0
by (le_plus_r . .)
we proved le i (plus h i)
by (le_S . . previous)
we proved le i (S (plus h i))
by (H_y0 previous)
getl
minus (S (plus h i)) i
CHead x (Bind b) w
CHead x0 (Bind b0) w0
getl
minus (plus (S h) i) i
CHead x (Bind b) w
CHead x0 (Bind b0) w0
end of H7
(H8)
by (minus_plus_r . .)
we proved eq nat (minus (plus (S h) i) i) (S h)
we proceed by induction on the previous result to prove getl (S h) (CHead x (Bind b) w) (CHead x0 (Bind b0) w0)
case refl_equal : ⇒
the thesis becomes the hypothesis H7
getl (S h) (CHead x (Bind b) w) (CHead x0 (Bind b0) w0)
end of H8
by (getl_gen_S . . . . . H8)
we proved getl (r (Bind b) h) x (CHead x0 (Bind b0) w0)
that is equivalent to getl h x (CHead x0 (Bind b0) w0)
by (ex_intro . . . previous)
ex C λd2:C.getl h x (CHead d2 (Bind b0) w0)
we proved ex C λd2:C.getl h x (CHead d2 (Bind b0) w0)
we proved
∀b0:B
.∀d0:C
.∀w0:T
.∀h:nat
.getl h d1 (CHead d0 (Bind b0) w0)
→ex C λd2:C.getl h x (CHead d2 (Bind b0) w0)
by (ex_intro2 . . . . previous H2)
ex2
C
λd2:C
.∀b0:B
.∀d3:C
.∀w0:T
.∀h:nat
.getl h d1 (CHead d3 (Bind b0) w0)
→ex C λd4:C.getl h d2 (CHead d4 (Bind b0) w0)
λd2:C.getl i c2 (CHead d2 (Bind b) w)
we proved
ex2
C
λd2:C
.∀b0:B
.∀d3:C
.∀w0:T
.∀h:nat
.getl h d1 (CHead d3 (Bind b0) w0)
→ex C λd4:C.getl h d2 (CHead d4 (Bind b0) w0)
λd2:C.getl i c2 (CHead d2 (Bind b) w)
that is equivalent to ex2 C λd2:C.cimp d1 d2 λd2:C.getl i c2 (CHead d2 (Bind b) w)
we proved
∀b:B
.∀d1:C
.∀w:T
.∀h:nat
.getl h c1 (CHead d1 (Bind b) w)
→ex C λd2:C.getl h c2 (CHead d2 (Bind b) w)
→∀b:B
.∀d1:C
.∀w:T
.∀i:nat
.getl i c1 (CHead d1 (Bind b) w)
→ex2 C λd2:C.cimp d1 d2 λd2:C.getl i c2 (CHead d2 (Bind b) w)
that is equivalent to
cimp c1 c2
→∀b:B
.∀d1:C
.∀w:T
.∀i:nat
.getl i c1 (CHead d1 (Bind b) w)
→ex2 C λd2:C.cimp d1 d2 λd2:C.getl i c2 (CHead d2 (Bind b) w)
we proved
∀c1:C
.∀c2:C
.cimp c1 c2
→∀b:B
.∀d1:C
.∀w:T
.∀i:nat
.getl i c1 (CHead d1 (Bind b) w)
→ex2 C λd2:C.cimp d1 d2 λd2:C.getl i c2 (CHead d2 (Bind b) w)