DEFINITION lift_gen_lref()
TYPE =
∀t:T
.∀d:nat
.∀h:nat
.∀i:nat
.eq T (TLRef i) (lift h d t)
→(or
land (lt i d) (eq T t (TLRef i))
land (le (plus d h) i) (eq T t (TLRef (minus i h))))
BODY =
assume t: T
we proceed by induction on t to prove
∀d:nat
.∀h:nat
.∀i:nat
.eq T (TLRef i) (lift h d t)
→(or
land (lt i d) (eq T t (TLRef i))
land (le (plus d h) i) (eq T t (TLRef (minus i h))))
case TSort : n:nat ⇒
the thesis becomes
∀d:nat
.∀h:nat
.∀i:nat
.∀H:eq T (TLRef i) (lift h d (TSort n))
.or
land (lt i d) (eq T (TSort n) (TLRef i))
land (le (plus d h) i) (eq T (TSort n) (TLRef (minus i h)))
assume d: nat
assume h: nat
assume i: nat
suppose H: eq T (TLRef i) (lift h d (TSort n))
(H0)
by (lift_sort . . .)
we proved eq T (lift h d (TSort n)) (TSort n)
we proceed by induction on the previous result to prove eq T (TLRef i) (TSort n)
case refl_equal : ⇒
the thesis becomes the hypothesis H
eq T (TLRef i) (TSort n)
end of H0
(H1)
we proceed by induction on H0 to prove
<λ:T.Prop>
CASE TSort n OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE TLRef i OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
consider I
we proved True
<λ:T.Prop>
CASE TLRef i OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
<λ:T.Prop>
CASE TSort n OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
end of H1
consider H1
we proved
<λ:T.Prop>
CASE TSort n OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove
or
land (lt i d) (eq T (TSort n) (TLRef i))
land (le (plus d h) i) (eq T (TSort n) (TLRef (minus i h)))
we proved
or
land (lt i d) (eq T (TSort n) (TLRef i))
land (le (plus d h) i) (eq T (TSort n) (TLRef (minus i h)))
∀d:nat
.∀h:nat
.∀i:nat
.∀H:eq T (TLRef i) (lift h d (TSort n))
.or
land (lt i d) (eq T (TSort n) (TLRef i))
land (le (plus d h) i) (eq T (TSort n) (TLRef (minus i h)))
case TLRef : n:nat ⇒
the thesis becomes
∀d:nat
.∀h:nat
.∀i:nat
.∀H:eq T (TLRef i) (lift h d (TLRef n))
.or
land (lt i d) (eq T (TLRef n) (TLRef i))
land (le (plus d h) i) (eq T (TLRef n) (TLRef (minus i h)))
assume d: nat
assume h: nat
assume i: nat
suppose H: eq T (TLRef i) (lift h d (TLRef n))
(h1)
suppose H0: lt n d
(H1)
by (lift_lref_lt . . . H0)
we proved eq T (lift h d (TLRef n)) (TLRef n)
we proceed by induction on the previous result to prove eq T (TLRef i) (TLRef n)
case refl_equal : ⇒
the thesis becomes the hypothesis H
eq T (TLRef i) (TLRef n)
end of H1
(H2)
by (f_equal . . . . . H1)
we proved
eq
nat
<λ:T.nat> CASE TLRef i OF TSort ⇒i | TLRef n0⇒n0 | THead ⇒i
<λ:T.nat> CASE TLRef n OF TSort ⇒i | TLRef n0⇒n0 | THead ⇒i
eq
nat
λe:T.<λ:T.nat> CASE e OF TSort ⇒i | TLRef n0⇒n0 | THead ⇒i (TLRef i)
λe:T.<λ:T.nat> CASE e OF TSort ⇒i | TLRef n0⇒n0 | THead ⇒i (TLRef n)
end of H2
(h1)
by (refl_equal . .)
we proved eq T (TLRef n) (TLRef n)
by (conj . . H0 previous)
we proved land (lt n d) (eq T (TLRef n) (TLRef n))
by (or_introl . . previous)
or
land (lt n d) (eq T (TLRef n) (TLRef n))
land (le (plus d h) n) (eq T (TLRef n) (TLRef (minus n h)))
end of h1
(h2)
consider H2
we proved
eq
nat
<λ:T.nat> CASE TLRef i OF TSort ⇒i | TLRef n0⇒n0 | THead ⇒i
<λ:T.nat> CASE TLRef n OF TSort ⇒i | TLRef n0⇒n0 | THead ⇒i
eq nat i n
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
or
land (lt i d) (eq T (TLRef n) (TLRef i))
land (le (plus d h) i) (eq T (TLRef n) (TLRef (minus i h)))
lt n d
→(or
land (lt i d) (eq T (TLRef n) (TLRef i))
land (le (plus d h) i) (eq T (TLRef n) (TLRef (minus i h))))
end of h1
(h2)
suppose H0: le d n
(H1)
by (lift_lref_ge . . . H0)
we proved eq T (lift h d (TLRef n)) (TLRef (plus n h))
we proceed by induction on the previous result to prove eq T (TLRef i) (TLRef (plus n h))
case refl_equal : ⇒
the thesis becomes the hypothesis H
eq T (TLRef i) (TLRef (plus n h))
end of H1
(H2)
by (f_equal . . . . . H1)
we proved
eq
nat
<λ:T.nat> CASE TLRef i OF TSort ⇒i | TLRef n0⇒n0 | THead ⇒i
<λ:T.nat> CASE TLRef (plus n h) OF TSort ⇒i | TLRef n0⇒n0 | THead ⇒i
eq
nat
λe:T.<λ:T.nat> CASE e OF TSort ⇒i | TLRef n0⇒n0 | THead ⇒i (TLRef i)
λe:T.<λ:T.nat> CASE e OF TSort ⇒i | TLRef n0⇒n0 | THead ⇒i
TLRef (plus n h)
end of H2
(h1)
(h1)
(h1)
by (le_n .)
we proved le h h
by (le_plus_plus . . . . H0 previous)
le (plus d h) (plus n h)
end of h1
(h2)
by (refl_equal . .)
eq T (TLRef n) (TLRef n)
end of h2
by (conj . . h1 h2)
we proved land (le (plus d h) (plus n h)) (eq T (TLRef n) (TLRef n))
by (or_intror . . previous)
or
land (lt (plus n h) d) (eq T (TLRef n) (TLRef (plus n h)))
land (le (plus d h) (plus n h)) (eq T (TLRef n) (TLRef n))
end of h1
(h2)
by (minus_plus_r . .)
eq nat (minus (plus n h) h) n
end of h2
by (eq_ind_r . . . h1 . h2)
or
land (lt (plus n h) d) (eq T (TLRef n) (TLRef (plus n h)))
land
le (plus d h) (plus n h)
eq T (TLRef n) (TLRef (minus (plus n h) h))
end of h1
(h2)
consider H2
we proved
eq
nat
<λ:T.nat> CASE TLRef i OF TSort ⇒i | TLRef n0⇒n0 | THead ⇒i
<λ:T.nat> CASE TLRef (plus n h) OF TSort ⇒i | TLRef n0⇒n0 | THead ⇒i
eq nat i (plus n h)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
or
land (lt i d) (eq T (TLRef n) (TLRef i))
land (le (plus d h) i) (eq T (TLRef n) (TLRef (minus i h)))
le d n
→(or
land (lt i d) (eq T (TLRef n) (TLRef i))
land (le (plus d h) i) (eq T (TLRef n) (TLRef (minus i h))))
end of h2
by (lt_le_e . . . h1 h2)
we proved
or
land (lt i d) (eq T (TLRef n) (TLRef i))
land (le (plus d h) i) (eq T (TLRef n) (TLRef (minus i h)))
∀d:nat
.∀h:nat
.∀i:nat
.∀H:eq T (TLRef i) (lift h d (TLRef n))
.or
land (lt i d) (eq T (TLRef n) (TLRef i))
land (le (plus d h) i) (eq T (TLRef n) (TLRef (minus i h)))
case THead : k:K t0:T t1:T ⇒
the thesis becomes
∀d:nat
.∀h:nat
.∀i:nat
.∀H1:eq T (TLRef i) (lift h d (THead k t0 t1))
.or
land (lt i d) (eq T (THead k t0 t1) (TLRef i))
land (le (plus d h) i) (eq T (THead k t0 t1) (TLRef (minus i h)))
() by induction hypothesis we know
∀d:nat
.∀h:nat
.∀i:nat
.eq T (TLRef i) (lift h d t0)
→(or
land (lt i d) (eq T t0 (TLRef i))
land (le (plus d h) i) (eq T t0 (TLRef (minus i h))))
() by induction hypothesis we know
∀d:nat
.∀h:nat
.∀i:nat
.eq T (TLRef i) (lift h d t1)
→(or
land (lt i d) (eq T t1 (TLRef i))
land (le (plus d h) i) (eq T t1 (TLRef (minus i h))))
assume d: nat
assume h: nat
assume i: nat
suppose H1: eq T (TLRef i) (lift h d (THead k t0 t1))
(H2)
by (lift_head . . . . .)
we proved
eq
T
lift h d (THead k t0 t1)
THead k (lift h d t0) (lift h (s k d) t1)
we proceed by induction on the previous result to prove eq T (TLRef i) (THead k (lift h d t0) (lift h (s k d) t1))
case refl_equal : ⇒
the thesis becomes the hypothesis H1
eq T (TLRef i) (THead k (lift h d t0) (lift h (s k d) t1))
end of H2
(H3)
we proceed by induction on H2 to prove
<λ:T.Prop>
CASE THead k (lift h d t0) (lift h (s k d) t1) OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE TLRef i OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
consider I
we proved True
<λ:T.Prop>
CASE TLRef i OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
<λ:T.Prop>
CASE THead k (lift h d t0) (lift h (s k d) t1) OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
end of H3
consider H3
we proved
<λ:T.Prop>
CASE THead k (lift h d t0) (lift h (s k d) t1) OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove
or
land (lt i d) (eq T (THead k t0 t1) (TLRef i))
land (le (plus d h) i) (eq T (THead k t0 t1) (TLRef (minus i h)))
we proved
or
land (lt i d) (eq T (THead k t0 t1) (TLRef i))
land (le (plus d h) i) (eq T (THead k t0 t1) (TLRef (minus i h)))
∀d:nat
.∀h:nat
.∀i:nat
.∀H1:eq T (TLRef i) (lift h d (THead k t0 t1))
.or
land (lt i d) (eq T (THead k t0 t1) (TLRef i))
land (le (plus d h) i) (eq T (THead k t0 t1) (TLRef (minus i h)))
we proved
∀d:nat
.∀h:nat
.∀i:nat
.eq T (TLRef i) (lift h d t)
→(or
land (lt i d) (eq T t (TLRef i))
land (le (plus d h) i) (eq T t (TLRef (minus i h))))
we proved
∀t:T
.∀d:nat
.∀h:nat
.∀i:nat
.eq T (TLRef i) (lift h d t)
→(or
land (lt i d) (eq T t (TLRef i))
land (le (plus d h) i) (eq T t (TLRef (minus i h))))