DEFINITION dnf_dec2()
TYPE =
∀t:T
.∀d:nat
.or
∀w:T.(ex T λv:T.subst0 d w t (lift (S O) d v))
ex T λv:T.eq T t (lift (S O) d v)
BODY =
assume t: T
we proceed by induction on t to prove
∀d:nat
.or
∀w:T.(ex T λv:T.subst0 d w t (lift (S O) d v))
ex T λv:T.eq T t (lift (S O) d v)
case TSort : n:nat ⇒
the thesis becomes
∀d:nat
.or
∀w:T.(ex T λv:T.subst0 d w (TSort n) (lift (S O) d v))
ex T λv:T.eq T (TSort n) (lift (S O) d v)
assume d: nat
(h1)
by (refl_equal . .)
eq T (TSort n) (TSort n)
end of h1
(h2)
by (lift_sort . . .)
eq T (lift (S O) d (TSort n)) (TSort n)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved eq T (TSort n) (lift (S O) d (TSort n))
by (ex_intro . . . previous)
we proved ex T λv:T.eq T (TSort n) (lift (S O) d v)
by (or_intror . . previous)
we proved
or
∀w:T.(ex T λv:T.subst0 d w (TSort n) (lift (S O) d v))
ex T λv:T.eq T (TSort n) (lift (S O) d v)
∀d:nat
.or
∀w:T.(ex T λv:T.subst0 d w (TSort n) (lift (S O) d v))
ex T λv:T.eq T (TSort n) (lift (S O) d v)
case TLRef : n:nat ⇒
the thesis becomes
∀d:nat
.or
∀w:T.(ex T λv:T.subst0 d w (TLRef n) (lift (S O) d v))
ex T λv:T.eq T (TLRef n) (lift (S O) d v)
assume d: nat
(h1)
suppose H: lt n d
(h1)
by (refl_equal . .)
eq T (TLRef n) (TLRef n)
end of h1
(h2)
by (lift_lref_lt . . . H)
eq T (lift (S O) d (TLRef n)) (TLRef n)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved eq T (TLRef n) (lift (S O) d (TLRef n))
by (ex_intro . . . previous)
we proved ex T λv:T.eq T (TLRef n) (lift (S O) d v)
by (or_intror . . previous)
we proved
or
∀w:T.(ex T λv:T.subst0 d w (TLRef n) (lift (S O) d v))
ex T λv:T.eq T (TLRef n) (lift (S O) d v)
lt n d
→(or
∀w:T.(ex T λv:T.subst0 d w (TLRef n) (lift (S O) d v))
ex T λv:T.eq T (TLRef n) (lift (S O) d v))
end of h1
(h2)
suppose H: eq nat n d
we proceed by induction on H to prove
or
∀w:T.(ex T λv:T.subst0 d w (TLRef n) (lift (S O) d v))
ex T λv:T.eq T (TLRef n) (lift (S O) d v)
case refl_equal : ⇒
the thesis becomes
or
∀w:T.(ex T λv:T.subst0 n w (TLRef n) (lift (S O) n v))
ex T λv:T.eq T (TLRef n) (lift (S O) n v)
assume w: T
(h1)
by (subst0_lref . .)
we proved subst0 n w (TLRef n) (lift (S n) O w)
subst0 n w (TLRef n) (lift (plus (S O) n) O w)
end of h1
(h2)
(h1)
by (le_n .)
we proved le (plus O n) (plus O n)
le n (plus O n)
end of h1
(h2) by (le_O_n .) we proved le O n
by (lift_free . . . . . h1 h2)
eq T (lift (S O) n (lift n O w)) (lift (plus (S O) n) O w)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved subst0 n w (TLRef n) (lift (S O) n (lift n O w))
by (ex_intro . . . previous)
we proved ex T λv:T.subst0 n w (TLRef n) (lift (S O) n v)
we proved ∀w:T.(ex T λv:T.subst0 n w (TLRef n) (lift (S O) n v))
by (or_introl . . previous)
or
∀w:T.(ex T λv:T.subst0 n w (TLRef n) (lift (S O) n v))
ex T λv:T.eq T (TLRef n) (lift (S O) n v)
we proved
or
∀w:T.(ex T λv:T.subst0 d w (TLRef n) (lift (S O) d v))
ex T λv:T.eq T (TLRef n) (lift (S O) d v)
eq nat n d
→(or
∀w:T.(ex T λv:T.subst0 d w (TLRef n) (lift (S O) d v))
ex T λv:T.eq T (TLRef n) (lift (S O) d v))
end of h2
(h3)
suppose H: lt d n
(h1)
by (refl_equal . .)
eq T (TLRef n) (TLRef n)
end of h1
(h2)
by (lift_lref_gt . . H)
eq T (lift (S O) d (TLRef (pred n))) (TLRef n)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved eq T (TLRef n) (lift (S O) d (TLRef (pred n)))
by (ex_intro . . . previous)
we proved ex T λv:T.eq T (TLRef n) (lift (S O) d v)
by (or_intror . . previous)
we proved
or
∀w:T.(ex T λv:T.subst0 d w (TLRef n) (lift (S O) d v))
ex T λv:T.eq T (TLRef n) (lift (S O) d v)
lt d n
→(or
∀w:T.(ex T λv:T.subst0 d w (TLRef n) (lift (S O) d v))
ex T λv:T.eq T (TLRef n) (lift (S O) d v))
end of h3
by (lt_eq_gt_e . . . h1 h2 h3)
we proved
or
∀w:T.(ex T λv:T.subst0 d w (TLRef n) (lift (S O) d v))
ex T λv:T.eq T (TLRef n) (lift (S O) d v)
∀d:nat
.or
∀w:T.(ex T λv:T.subst0 d w (TLRef n) (lift (S O) d v))
ex T λv:T.eq T (TLRef n) (lift (S O) d v)
case THead : k:K t0:T t1:T ⇒
the thesis becomes
∀d:nat
.or
∀w:T.(ex T λv:T.subst0 d w (THead k t0 t1) (lift (S O) d v))
ex T λv:T.eq T (THead k t0 t1) (lift (S O) d v)
(H) by induction hypothesis we know
∀d:nat
.or
∀w:T.(ex T λv:T.subst0 d w t0 (lift (S O) d v))
ex T λv:T.eq T t0 (lift (S O) d v)
(H0) by induction hypothesis we know
∀d:nat
.or
∀w:T.(ex T λv:T.subst0 d w t1 (lift (S O) d v))
ex T λv:T.eq T t1 (lift (S O) d v)
assume d: nat
(H_x)
by (H .)
or
∀w:T.(ex T λv:T.subst0 d w t0 (lift (S O) d v))
ex T λv:T.eq T t0 (lift (S O) d v)
end of H_x
(H1) consider H_x
we proceed by induction on H1 to prove
or
∀w:T.(ex T λv:T.subst0 d w (THead k t0 t1) (lift (S O) d v))
ex T λv:T.eq T (THead k t0 t1) (lift (S O) d v)
case or_introl : H2:∀w:T.(ex T λv:T.subst0 d w t0 (lift (S O) d v)) ⇒
the thesis becomes
or
∀w:T.(ex T λv:T.subst0 d w (THead k t0 t1) (lift (S O) d v))
ex T λv:T.eq T (THead k t0 t1) (lift (S O) d v)
(H_x0)
by (H0 .)
or
∀w:T.(ex T λv:T.subst0 (s k d) w t1 (lift (S O) (s k d) v))
ex T λv:T.eq T t1 (lift (S O) (s k d) v)
end of H_x0
(H3) consider H_x0
we proceed by induction on H3 to prove
or
∀w:T.(ex T λv:T.subst0 d w (THead k t0 t1) (lift (S O) d v))
ex T λv:T.eq T (THead k t0 t1) (lift (S O) d v)
case or_introl : H4:∀w:T.(ex T λv:T.subst0 (s k d) w t1 (lift (S O) (s k d) v)) ⇒
the thesis becomes
or
∀w:T.(ex T λv:T.subst0 d w (THead k t0 t1) (lift (S O) d v))
ex T λv:T.eq T (THead k t0 t1) (lift (S O) d v)
assume w: T
(H_x1)
by (H4 .)
ex T λv:T.subst0 (s k d) w t1 (lift (S O) (s k d) v)
end of H_x1
(H5) consider H_x1
we proceed by induction on H5 to prove ex T λv:T.subst0 d w (THead k t0 t1) (lift (S O) d v)
case ex_intro : x:T H6:subst0 (s k d) w t1 (lift (S O) (s k d) x) ⇒
the thesis becomes ex T λv:T.subst0 d w (THead k t0 t1) (lift (S O) d v)
(H_x2)
by (H2 .)
ex T λv:T.subst0 d w t0 (lift (S O) d v)
end of H_x2
(H7) consider H_x2
we proceed by induction on H7 to prove ex T λv:T.subst0 d w (THead k t0 t1) (lift (S O) d v)
case ex_intro : x0:T H8:subst0 d w t0 (lift (S O) d x0) ⇒
the thesis becomes ex T λv:T.subst0 d w (THead k t0 t1) (lift (S O) d v)
(h1)
by (subst0_both . . . . H8 . . . H6)
subst0 d w (THead k t0 t1) (THead k (lift (S O) d x0) (lift (S O) (s k d) x))
end of h1
(h2)
by (lift_head . . . . .)
eq
T
lift (S O) d (THead k x0 x)
THead k (lift (S O) d x0) (lift (S O) (s k d) x)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved subst0 d w (THead k t0 t1) (lift (S O) d (THead k x0 x))
by (ex_intro . . . previous)
ex T λv:T.subst0 d w (THead k t0 t1) (lift (S O) d v)
ex T λv:T.subst0 d w (THead k t0 t1) (lift (S O) d v)
we proved ex T λv:T.subst0 d w (THead k t0 t1) (lift (S O) d v)
we proved ∀w:T.(ex T λv:T.subst0 d w (THead k t0 t1) (lift (S O) d v))
by (or_introl . . previous)
or
∀w:T.(ex T λv:T.subst0 d w (THead k t0 t1) (lift (S O) d v))
ex T λv:T.eq T (THead k t0 t1) (lift (S O) d v)
case or_intror : H4:ex T λv:T.eq T t1 (lift (S O) (s k d) v) ⇒
the thesis becomes
or
∀w:T.(ex T λv:T.subst0 d w (THead k t0 t1) (lift (S O) d v))
ex T λv:T.eq T (THead k t0 t1) (lift (S O) d v)
we proceed by induction on H4 to prove
or
∀w:T.(ex T λv:T.subst0 d w (THead k t0 t1) (lift (S O) d v))
ex T λv:T.eq T (THead k t0 t1) (lift (S O) d v)
case ex_intro : x:T H5:eq T t1 (lift (S O) (s k d) x) ⇒
the thesis becomes
or
∀w:T.(ex T λv:T.subst0 d w (THead k t0 t1) (lift (S O) d v))
ex T λv:T.eq T (THead k t0 t1) (lift (S O) d v)
assume w: T
(H_x1)
by (H2 .)
ex T λv:T.subst0 d w t0 (lift (S O) d v)
end of H_x1
(H6) consider H_x1
we proceed by induction on H6 to prove
ex T λv:T.subst0 d w (THead k t0 (lift (S O) (s k d) x)) (lift (S O) d v)
case ex_intro : x0:T H7:subst0 d w t0 (lift (S O) d x0) ⇒
the thesis becomes
ex T λv:T.subst0 d w (THead k t0 (lift (S O) (s k d) x)) (lift (S O) d v)
(h1)
by (subst0_fst . . . . H7 . .)
subst0
d
w
THead k t0 (lift (S O) (s k d) x)
THead k (lift (S O) d x0) (lift (S O) (s k d) x)
end of h1
(h2)
by (lift_head . . . . .)
eq
T
lift (S O) d (THead k x0 x)
THead k (lift (S O) d x0) (lift (S O) (s k d) x)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
subst0
d
w
THead k t0 (lift (S O) (s k d) x)
lift (S O) d (THead k x0 x)
by (ex_intro . . . previous)
ex T λv:T.subst0 d w (THead k t0 (lift (S O) (s k d) x)) (lift (S O) d v)
we proved
ex T λv:T.subst0 d w (THead k t0 (lift (S O) (s k d) x)) (lift (S O) d v)
we proved
∀w:T
.ex T λv:T.subst0 d w (THead k t0 (lift (S O) (s k d) x)) (lift (S O) d v)
by (or_introl . . previous)
we proved
or
∀w:T
.ex T λv:T.subst0 d w (THead k t0 (lift (S O) (s k d) x)) (lift (S O) d v)
ex
T
λv:T.eq T (THead k t0 (lift (S O) (s k d) x)) (lift (S O) d v)
by (eq_ind_r . . . previous . H5)
or
∀w:T.(ex T λv:T.subst0 d w (THead k t0 t1) (lift (S O) d v))
ex T λv:T.eq T (THead k t0 t1) (lift (S O) d v)
or
∀w:T.(ex T λv:T.subst0 d w (THead k t0 t1) (lift (S O) d v))
ex T λv:T.eq T (THead k t0 t1) (lift (S O) d v)
or
∀w:T.(ex T λv:T.subst0 d w (THead k t0 t1) (lift (S O) d v))
ex T λv:T.eq T (THead k t0 t1) (lift (S O) d v)
case or_intror : H2:ex T λv:T.eq T t0 (lift (S O) d v) ⇒
the thesis becomes
or
∀w:T.(ex T λv:T.subst0 d w (THead k t0 t1) (lift (S O) d v))
ex T λv:T.eq T (THead k t0 t1) (lift (S O) d v)
we proceed by induction on H2 to prove
or
∀w:T.(ex T λv:T.subst0 d w (THead k t0 t1) (lift (S O) d v))
ex T λv:T.eq T (THead k t0 t1) (lift (S O) d v)
case ex_intro : x:T H3:eq T t0 (lift (S O) d x) ⇒
the thesis becomes
or
∀w:T.(ex T λv:T.subst0 d w (THead k t0 t1) (lift (S O) d v))
ex T λv:T.eq T (THead k t0 t1) (lift (S O) d v)
(H_x0)
by (H0 .)
or
∀w:T.(ex T λv:T.subst0 (s k d) w t1 (lift (S O) (s k d) v))
ex T λv:T.eq T t1 (lift (S O) (s k d) v)
end of H_x0
(H4) consider H_x0
we proceed by induction on H4 to prove
or
∀w:T.(ex T λv:T.subst0 d w (THead k t0 t1) (lift (S O) d v))
ex T λv:T.eq T (THead k t0 t1) (lift (S O) d v)
case or_introl : H5:∀w:T.(ex T λv:T.subst0 (s k d) w t1 (lift (S O) (s k d) v)) ⇒
the thesis becomes
or
∀w:T.(ex T λv:T.subst0 d w (THead k t0 t1) (lift (S O) d v))
ex T λv:T.eq T (THead k t0 t1) (lift (S O) d v)
assume w: T
(H_x1)
by (H5 .)
ex T λv:T.subst0 (s k d) w t1 (lift (S O) (s k d) v)
end of H_x1
(H6) consider H_x1
we proceed by induction on H6 to prove ex T λv:T.subst0 d w (THead k (lift (S O) d x) t1) (lift (S O) d v)
case ex_intro : x0:T H7:subst0 (s k d) w t1 (lift (S O) (s k d) x0) ⇒
the thesis becomes ex T λv:T.subst0 d w (THead k (lift (S O) d x) t1) (lift (S O) d v)
(h1)
by (subst0_snd . . . . . H7 .)
subst0
d
w
THead k (lift (S O) d x) t1
THead k (lift (S O) d x) (lift (S O) (s k d) x0)
end of h1
(h2)
by (lift_head . . . . .)
eq
T
lift (S O) d (THead k x x0)
THead k (lift (S O) d x) (lift (S O) (s k d) x0)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved subst0 d w (THead k (lift (S O) d x) t1) (lift (S O) d (THead k x x0))
by (ex_intro . . . previous)
ex T λv:T.subst0 d w (THead k (lift (S O) d x) t1) (lift (S O) d v)
we proved ex T λv:T.subst0 d w (THead k (lift (S O) d x) t1) (lift (S O) d v)
we proved ∀w:T.(ex T λv:T.subst0 d w (THead k (lift (S O) d x) t1) (lift (S O) d v))
by (or_introl . . previous)
we proved
or
∀w:T.(ex T λv:T.subst0 d w (THead k (lift (S O) d x) t1) (lift (S O) d v))
ex T λv:T.eq T (THead k (lift (S O) d x) t1) (lift (S O) d v)
by (eq_ind_r . . . previous . H3)
or
∀w:T.(ex T λv:T.subst0 d w (THead k t0 t1) (lift (S O) d v))
ex T λv:T.eq T (THead k t0 t1) (lift (S O) d v)
case or_intror : H5:ex T λv:T.eq T t1 (lift (S O) (s k d) v) ⇒
the thesis becomes
or
∀w:T.(ex T λv:T.subst0 d w (THead k t0 t1) (lift (S O) d v))
ex T λv:T.eq T (THead k t0 t1) (lift (S O) d v)
we proceed by induction on H5 to prove
or
∀w:T.(ex T λv:T.subst0 d w (THead k t0 t1) (lift (S O) d v))
ex T λv:T.eq T (THead k t0 t1) (lift (S O) d v)
case ex_intro : x0:T H6:eq T t1 (lift (S O) (s k d) x0) ⇒
the thesis becomes
or
∀w:T.(ex T λv:T.subst0 d w (THead k t0 t1) (lift (S O) d v))
ex T λv:T.eq T (THead k t0 t1) (lift (S O) d v)
(h1)
by (refl_equal . .)
eq
T
THead k (lift (S O) d x) (lift (S O) (s k d) x0)
THead k (lift (S O) d x) (lift (S O) (s k d) x0)
end of h1
(h2)
by (lift_head . . . . .)
eq
T
lift (S O) d (THead k x x0)
THead k (lift (S O) d x) (lift (S O) (s k d) x0)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
eq
T
THead k (lift (S O) d x) (lift (S O) (s k d) x0)
lift (S O) d (THead k x x0)
by (ex_intro . . . previous)
we proved
ex
T
λv:T
.eq
T
THead k (lift (S O) d x) (lift (S O) (s k d) x0)
lift (S O) d v
by (or_intror . . previous)
we proved
or
∀w:T
.ex
T
λv:T
.subst0
d
w
THead k (lift (S O) d x) (lift (S O) (s k d) x0)
lift (S O) d v
ex
T
λv:T
.eq
T
THead k (lift (S O) d x) (lift (S O) (s k d) x0)
lift (S O) d v
by (eq_ind_r . . . previous . H3)
we proved
or
∀w:T
.ex T λv:T.subst0 d w (THead k t0 (lift (S O) (s k d) x0)) (lift (S O) d v)
ex T λv:T.eq T (THead k t0 (lift (S O) (s k d) x0)) (lift (S O) d v)
by (eq_ind_r . . . previous . H6)
or
∀w:T.(ex T λv:T.subst0 d w (THead k t0 t1) (lift (S O) d v))
ex T λv:T.eq T (THead k t0 t1) (lift (S O) d v)
or
∀w:T.(ex T λv:T.subst0 d w (THead k t0 t1) (lift (S O) d v))
ex T λv:T.eq T (THead k t0 t1) (lift (S O) d v)
or
∀w:T.(ex T λv:T.subst0 d w (THead k t0 t1) (lift (S O) d v))
ex T λv:T.eq T (THead k t0 t1) (lift (S O) d v)
or
∀w:T.(ex T λv:T.subst0 d w (THead k t0 t1) (lift (S O) d v))
ex T λv:T.eq T (THead k t0 t1) (lift (S O) d v)
we proved
or
∀w:T.(ex T λv:T.subst0 d w (THead k t0 t1) (lift (S O) d v))
ex T λv:T.eq T (THead k t0 t1) (lift (S O) d v)
∀d:nat
.or
∀w:T.(ex T λv:T.subst0 d w (THead k t0 t1) (lift (S O) d v))
ex T λv:T.eq T (THead k t0 t1) (lift (S O) d v)
we proved
∀d:nat
.or
∀w:T.(ex T λv:T.subst0 d w t (lift (S O) d v))
ex T λv:T.eq T t (lift (S O) d v)
we proved
∀t:T
.∀d:nat
.or
∀w:T.(ex T λv:T.subst0 d w t (lift (S O) d v))
ex T λv:T.eq T t (lift (S O) d v)