DEFINITION lift_weight_map()
TYPE =
∀t:T
.∀h:nat
.∀d:nat
.∀f:nat→nat
.∀m:nat.(le d m)→(eq nat (f m) O)
→eq nat (weight_map f (lift h d t)) (weight_map f t)
BODY =
assume t: T
we proceed by induction on t to prove
∀h:nat
.∀d:nat
.∀f:nat→nat
.∀m:nat.(le d m)→(eq nat (f m) O)
→eq nat (weight_map f (lift h d t)) (weight_map f t)
case TSort : n:nat ⇒
the thesis becomes
nat
→∀d:nat
.∀f:nat→nat
.∀m:nat.(le d m)→(eq nat (f m) O)
→eq nat (weight_map f (TSort n)) (weight_map f (TSort n))
assume : nat
assume d: nat
assume f: nat→nat
suppose : ∀m:nat.(le d m)→(eq nat (f m) O)
by (refl_equal . .)
we proved eq nat (weight_map f (TSort n)) (weight_map f (TSort n))
that is equivalent to
eq
nat
weight_map f (lift __4 d (TSort n))
weight_map f (TSort n)
nat
→∀d:nat
.∀f:nat→nat
.∀m:nat.(le d m)→(eq nat (f m) O)
→eq nat (weight_map f (TSort n)) (weight_map f (TSort n))
case TLRef : n:nat ⇒
the thesis becomes
∀h:nat
.∀d:nat
.∀f:nat→nat
.∀H:∀m:nat.(le d m)→(eq nat (f m) O)
.eq
nat
weight_map f (lift h d (TLRef n))
weight_map f (TLRef n)
assume h: nat
assume d: nat
assume f: nat→nat
suppose H: ∀m:nat.(le d m)→(eq nat (f m) O)
(h1)
suppose H0: lt n d
(h1)
by (refl_equal . .)
eq nat (weight_map f (TLRef n)) (weight_map f (TLRef n))
end of h1
(h2)
by (lift_lref_lt . . . H0)
eq T (lift h d (TLRef n)) (TLRef n)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
eq
nat
weight_map f (lift h d (TLRef n))
weight_map f (TLRef n)
lt n d
→(eq
nat
weight_map f (lift h d (TLRef n))
weight_map f (TLRef n))
end of h1
(h2)
suppose H0: le d n
(h1)
(h1)
by (le_plus_trans . . . H0)
we proved le d (plus n h)
by (H . previous)
eq nat (f (plus n h)) O
end of h1
(h2)
by (H . H0)
eq nat (f n) O
end of h2
by (eq_ind_r . . . h1 . h2)
we proved eq nat (f (plus n h)) (f n)
eq
nat
weight_map f (TLRef (plus n h))
weight_map f (TLRef n)
end of h1
(h2)
by (lift_lref_ge . . . H0)
eq T (lift h d (TLRef n)) (TLRef (plus n h))
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
eq
nat
weight_map f (lift h d (TLRef n))
weight_map f (TLRef n)
le d n
→(eq
nat
weight_map f (lift h d (TLRef n))
weight_map f (TLRef n))
end of h2
by (lt_le_e . . . h1 h2)
we proved
eq
nat
weight_map f (lift h d (TLRef n))
weight_map f (TLRef n)
∀h:nat
.∀d:nat
.∀f:nat→nat
.∀H:∀m:nat.(le d m)→(eq nat (f m) O)
.eq
nat
weight_map f (lift h d (TLRef n))
weight_map f (TLRef n)
case THead : k:K t0:T t1:T ⇒
the thesis becomes
∀h:nat
.∀d:nat
.∀f:nat→nat
.∀H1:∀m:nat.(le d m)→(eq nat (f m) O)
.eq
nat
weight_map f (lift h d (THead k t0 t1))
weight_map f (THead k t0 t1)
(H) by induction hypothesis we know
∀h:nat
.∀d:nat
.∀f:nat→nat
.∀m:nat.(le d m)→(eq nat (f m) O)
→eq nat (weight_map f (lift h d t0)) (weight_map f t0)
(H0) by induction hypothesis we know
∀h:nat
.∀d:nat
.∀f:nat→nat
.∀m:nat.(le d m)→(eq nat (f m) O)
→eq nat (weight_map f (lift h d t1)) (weight_map f t1)
assume h: nat
assume d: nat
assume f: nat→nat
suppose H1: ∀m:nat.(le d m)→(eq nat (f m) O)
we proceed by induction on k to prove
eq
nat
weight_map f (lift h d (THead k t0 t1))
weight_map f (THead k t0 t1)
case Bind : b:B ⇒
the thesis becomes
eq
nat
weight_map f (lift h d (THead (Bind b) t0 t1))
weight_map f (THead (Bind b) t0 t1)
(h1)
we proceed by induction on b to prove
eq
nat
<λb1:B.nat>
CASE b OF
Abbr⇒
S
plus
weight_map f (lift h d t0)
weight_map
wadd f (S (weight_map f (lift h d t0)))
lift h (S d) t1
| Abst⇒
S
plus
weight_map f (lift h d t0)
weight_map (wadd f O) (lift h (S d) t1)
| Void⇒
S
plus
weight_map f (lift h d t0)
weight_map (wadd f O) (lift h (S d) t1)
<λb1:B.nat>
CASE b OF
Abbr⇒
S
plus
weight_map f t0
weight_map (wadd f (S (weight_map f t0))) t1
| Abst⇒S (plus (weight_map f t0) (weight_map (wadd f O) t1))
| Void⇒S (plus (weight_map f t0) (weight_map (wadd f O) t1))
case Abbr : ⇒
the thesis becomes
eq
nat
<λb1:B.nat>
CASE Abbr OF
Abbr⇒
S
plus
weight_map f (lift h d t0)
weight_map
wadd f (S (weight_map f (lift h d t0)))
lift h (S d) t1
| Abst⇒
S
plus
weight_map f (lift h d t0)
weight_map (wadd f O) (lift h (S d) t1)
| Void⇒
S
plus
weight_map f (lift h d t0)
weight_map (wadd f O) (lift h (S d) t1)
<λb1:B.nat>
CASE Abbr OF
Abbr⇒
S
plus
weight_map f t0
weight_map (wadd f (S (weight_map f t0))) t1
| Abst⇒S (plus (weight_map f t0) (weight_map (wadd f O) t1))
| Void⇒S (plus (weight_map f t0) (weight_map (wadd f O) t1))
(h1)
(h1)
by (refl_equal . .)
eq
nat
S
plus
weight_map f t0
weight_map (wadd f (S (weight_map f t0))) t1
S
plus
weight_map f t0
weight_map (wadd f (S (weight_map f t0))) t1
end of h1
(h2)
assume m: nat
suppose H2: le (S d) m
by (le_gen_S . . H2)
we proved ex2 nat λn:nat.eq nat m (S n) λn:nat.le d n
we proceed by induction on the previous result to prove eq nat (wadd f (S (weight_map f t0)) m) O
case ex_intro2 : x:nat H3:eq nat m (S x) H4:le d x ⇒
the thesis becomes eq nat (wadd f (S (weight_map f t0)) m) O
by (H1 . H4)
we proved eq nat (f x) O
that is equivalent to eq nat (wadd f (S (weight_map f t0)) (S x)) O
by (eq_ind_r . . . previous . H3)
eq nat (wadd f (S (weight_map f t0)) m) O
we proved eq nat (wadd f (S (weight_map f t0)) m) O
we proved
∀m:nat
.(le (S d) m)→(eq nat (wadd f (S (weight_map f t0)) m) O)
by (H0 . . . previous)
eq
nat
weight_map (wadd f (S (weight_map f t0))) (lift h (S d) t1)
weight_map (wadd f (S (weight_map f t0))) t1
end of h2
by (eq_ind_r . . . h1 . h2)
eq
nat
S
plus
weight_map f t0
weight_map (wadd f (S (weight_map f t0))) (lift h (S d) t1)
S
plus
weight_map f t0
weight_map (wadd f (S (weight_map f t0))) t1
end of h1
(h2)
by (H . . . H1)
eq nat (weight_map f (lift h d t0)) (weight_map f t0)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
eq
nat
S
plus
weight_map f (lift h d t0)
weight_map
wadd f (S (weight_map f (lift h d t0)))
lift h (S d) t1
S
plus
weight_map f t0
weight_map (wadd f (S (weight_map f t0))) t1
eq
nat
<λb1:B.nat>
CASE Abbr OF
Abbr⇒
S
plus
weight_map f (lift h d t0)
weight_map
wadd f (S (weight_map f (lift h d t0)))
lift h (S d) t1
| Abst⇒
S
plus
weight_map f (lift h d t0)
weight_map (wadd f O) (lift h (S d) t1)
| Void⇒
S
plus
weight_map f (lift h d t0)
weight_map (wadd f O) (lift h (S d) t1)
<λb1:B.nat>
CASE Abbr OF
Abbr⇒
S
plus
weight_map f t0
weight_map (wadd f (S (weight_map f t0))) t1
| Abst⇒S (plus (weight_map f t0) (weight_map (wadd f O) t1))
| Void⇒S (plus (weight_map f t0) (weight_map (wadd f O) t1))
case Abst : ⇒
the thesis becomes
eq
nat
<λb1:B.nat>
CASE Abst OF
Abbr⇒
S
plus
weight_map f (lift h d t0)
weight_map
wadd f (S (weight_map f (lift h d t0)))
lift h (S d) t1
| Abst⇒
S
plus
weight_map f (lift h d t0)
weight_map (wadd f O) (lift h (S d) t1)
| Void⇒
S
plus
weight_map f (lift h d t0)
weight_map (wadd f O) (lift h (S d) t1)
<λb1:B.nat>
CASE Abst OF
Abbr⇒
S
plus
weight_map f t0
weight_map (wadd f (S (weight_map f t0))) t1
| Abst⇒S (plus (weight_map f t0) (weight_map (wadd f O) t1))
| Void⇒S (plus (weight_map f t0) (weight_map (wadd f O) t1))
(h1)
(h1)
by (H . . . H1)
eq nat (weight_map f (lift h d t0)) (weight_map f t0)
end of h1
(h2)
by (refl_equal . .)
eq nat (weight_map (wadd f O) t1) (weight_map (wadd f O) t1)
end of h2
by (f_equal2 . . . . . . . . h1 h2)
we proved
eq
nat
plus (weight_map f (lift h d t0)) (weight_map (wadd f O) t1)
plus (weight_map f t0) (weight_map (wadd f O) t1)
by (f_equal . . . . . previous)
eq
nat
S
plus (weight_map f (lift h d t0)) (weight_map (wadd f O) t1)
S (plus (weight_map f t0) (weight_map (wadd f O) t1))
end of h1
(h2)
assume m: nat
suppose H2: le (S d) m
by (le_gen_S . . H2)
we proved ex2 nat λn:nat.eq nat m (S n) λn:nat.le d n
we proceed by induction on the previous result to prove eq nat (wadd f O m) O
case ex_intro2 : x:nat H3:eq nat m (S x) H4:le d x ⇒
the thesis becomes eq nat (wadd f O m) O
by (H1 . H4)
we proved eq nat (f x) O
that is equivalent to eq nat (wadd f O (S x)) O
by (eq_ind_r . . . previous . H3)
eq nat (wadd f O m) O
we proved eq nat (wadd f O m) O
we proved ∀m:nat.(le (S d) m)→(eq nat (wadd f O m) O)
by (H0 . . . previous)
eq
nat
weight_map (wadd f O) (lift h (S d) t1)
weight_map (wadd f O) t1
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
eq
nat
S
plus
weight_map f (lift h d t0)
weight_map (wadd f O) (lift h (S d) t1)
S (plus (weight_map f t0) (weight_map (wadd f O) t1))
eq
nat
<λb1:B.nat>
CASE Abst OF
Abbr⇒
S
plus
weight_map f (lift h d t0)
weight_map
wadd f (S (weight_map f (lift h d t0)))
lift h (S d) t1
| Abst⇒
S
plus
weight_map f (lift h d t0)
weight_map (wadd f O) (lift h (S d) t1)
| Void⇒
S
plus
weight_map f (lift h d t0)
weight_map (wadd f O) (lift h (S d) t1)
<λb1:B.nat>
CASE Abst OF
Abbr⇒
S
plus
weight_map f t0
weight_map (wadd f (S (weight_map f t0))) t1
| Abst⇒S (plus (weight_map f t0) (weight_map (wadd f O) t1))
| Void⇒S (plus (weight_map f t0) (weight_map (wadd f O) t1))
case Void : ⇒
the thesis becomes
eq
nat
<λb1:B.nat>
CASE Void OF
Abbr⇒
S
plus
weight_map f (lift h d t0)
weight_map
wadd f (S (weight_map f (lift h d t0)))
lift h (S d) t1
| Abst⇒
S
plus
weight_map f (lift h d t0)
weight_map (wadd f O) (lift h (S d) t1)
| Void⇒
S
plus
weight_map f (lift h d t0)
weight_map (wadd f O) (lift h (S d) t1)
<λb1:B.nat>
CASE Void OF
Abbr⇒
S
plus
weight_map f t0
weight_map (wadd f (S (weight_map f t0))) t1
| Abst⇒S (plus (weight_map f t0) (weight_map (wadd f O) t1))
| Void⇒S (plus (weight_map f t0) (weight_map (wadd f O) t1))
(h1)
(h1)
by (H . . . H1)
eq nat (weight_map f (lift h d t0)) (weight_map f t0)
end of h1
(h2)
by (refl_equal . .)
eq nat (weight_map (wadd f O) t1) (weight_map (wadd f O) t1)
end of h2
by (f_equal2 . . . . . . . . h1 h2)
we proved
eq
nat
plus (weight_map f (lift h d t0)) (weight_map (wadd f O) t1)
plus (weight_map f t0) (weight_map (wadd f O) t1)
by (f_equal . . . . . previous)
eq
nat
S
plus (weight_map f (lift h d t0)) (weight_map (wadd f O) t1)
S (plus (weight_map f t0) (weight_map (wadd f O) t1))
end of h1
(h2)
assume m: nat
suppose H2: le (S d) m
by (le_gen_S . . H2)
we proved ex2 nat λn:nat.eq nat m (S n) λn:nat.le d n
we proceed by induction on the previous result to prove eq nat (wadd f O m) O
case ex_intro2 : x:nat H3:eq nat m (S x) H4:le d x ⇒
the thesis becomes eq nat (wadd f O m) O
by (H1 . H4)
we proved eq nat (f x) O
that is equivalent to eq nat (wadd f O (S x)) O
by (eq_ind_r . . . previous . H3)
eq nat (wadd f O m) O
we proved eq nat (wadd f O m) O
we proved ∀m:nat.(le (S d) m)→(eq nat (wadd f O m) O)
by (H0 . . . previous)
eq
nat
weight_map (wadd f O) (lift h (S d) t1)
weight_map (wadd f O) t1
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
eq
nat
S
plus
weight_map f (lift h d t0)
weight_map (wadd f O) (lift h (S d) t1)
S (plus (weight_map f t0) (weight_map (wadd f O) t1))
eq
nat
<λb1:B.nat>
CASE Void OF
Abbr⇒
S
plus
weight_map f (lift h d t0)
weight_map
wadd f (S (weight_map f (lift h d t0)))
lift h (S d) t1
| Abst⇒
S
plus
weight_map f (lift h d t0)
weight_map (wadd f O) (lift h (S d) t1)
| Void⇒
S
plus
weight_map f (lift h d t0)
weight_map (wadd f O) (lift h (S d) t1)
<λb1:B.nat>
CASE Void OF
Abbr⇒
S
plus
weight_map f t0
weight_map (wadd f (S (weight_map f t0))) t1
| Abst⇒S (plus (weight_map f t0) (weight_map (wadd f O) t1))
| Void⇒S (plus (weight_map f t0) (weight_map (wadd f O) t1))
we proved
eq
nat
<λb1:B.nat>
CASE b OF
Abbr⇒
S
plus
weight_map f (lift h d t0)
weight_map
wadd f (S (weight_map f (lift h d t0)))
lift h (S d) t1
| Abst⇒
S
plus
weight_map f (lift h d t0)
weight_map (wadd f O) (lift h (S d) t1)
| Void⇒
S
plus
weight_map f (lift h d t0)
weight_map (wadd f O) (lift h (S d) t1)
<λb1:B.nat>
CASE b OF
Abbr⇒
S
plus
weight_map f t0
weight_map (wadd f (S (weight_map f t0))) t1
| Abst⇒S (plus (weight_map f t0) (weight_map (wadd f O) t1))
| Void⇒S (plus (weight_map f t0) (weight_map (wadd f O) t1))
eq
nat
weight_map
f
THead (Bind b) (lift h d t0) (lift h (s (Bind b) d) t1)
weight_map f (THead (Bind b) t0 t1)
end of h1
(h2)
by (lift_head . . . . .)
eq
T
lift h d (THead (Bind b) t0 t1)
THead (Bind b) (lift h d t0) (lift h (s (Bind b) d) t1)
end of h2
by (eq_ind_r . . . h1 . h2)
eq
nat
weight_map f (lift h d (THead (Bind b) t0 t1))
weight_map f (THead (Bind b) t0 t1)
case Flat : f0:F ⇒
the thesis becomes
eq
nat
weight_map f (lift h d (THead (Flat f0) t0 t1))
weight_map f (THead (Flat f0) t0 t1)
(h1)
(h1)
by (H . . . H1)
eq nat (weight_map f (lift h d t0)) (weight_map f t0)
end of h1
(h2)
by (H0 . . . H1)
eq nat (weight_map f (lift h d t1)) (weight_map f t1)
end of h2
by (f_equal2 . . . . . . . . h1 h2)
we proved
eq
nat
plus (weight_map f (lift h d t0)) (weight_map f (lift h d t1))
plus (weight_map f t0) (weight_map f t1)
by (f_equal . . . . . previous)
we proved
eq
nat
S
plus (weight_map f (lift h d t0)) (weight_map f (lift h d t1))
S (plus (weight_map f t0) (weight_map f t1))
eq
nat
weight_map
f
THead (Flat f0) (lift h d t0) (lift h (s (Flat f0) d) t1)
weight_map f (THead (Flat f0) t0 t1)
end of h1
(h2)
by (lift_head . . . . .)
eq
T
lift h d (THead (Flat f0) t0 t1)
THead (Flat f0) (lift h d t0) (lift h (s (Flat f0) d) t1)
end of h2
by (eq_ind_r . . . h1 . h2)
eq
nat
weight_map f (lift h d (THead (Flat f0) t0 t1))
weight_map f (THead (Flat f0) t0 t1)
we proved
eq
nat
weight_map f (lift h d (THead k t0 t1))
weight_map f (THead k t0 t1)
∀h:nat
.∀d:nat
.∀f:nat→nat
.∀H1:∀m:nat.(le d m)→(eq nat (f m) O)
.eq
nat
weight_map f (lift h d (THead k t0 t1))
weight_map f (THead k t0 t1)
we proved
∀h:nat
.∀d:nat
.∀f:nat→nat
.∀m:nat.(le d m)→(eq nat (f m) O)
→eq nat (weight_map f (lift h d t)) (weight_map f t)
we proved
∀t:T
.∀h:nat
.∀d:nat
.∀f:nat→nat
.∀m:nat.(le d m)→(eq nat (f m) O)
→eq nat (weight_map f (lift h d t)) (weight_map f t)