DEFINITION lift_weight_add()
TYPE =
∀w:nat
.∀t:T
.∀h:nat
.∀d:nat
.∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(lt m d)→(eq nat (g m) (f m))
→(eq nat (g d) w
→(∀m:nat.(le d m)→(eq nat (g (S m)) (f m))
→(eq
nat
weight_map f (lift h d t)
weight_map g (lift (S h) d t))))
BODY =
assume w: nat
assume t: T
we proceed by induction on t to prove
∀h:nat
.∀d:nat
.∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(lt m d)→(eq nat (g m) (f m))
→(eq nat (g d) w
→(∀m:nat.(le d m)→(eq nat (g (S m)) (f m))
→(eq
nat
weight_map f (lift h d t)
weight_map g (lift (S h) d t))))
case TSort : n:nat ⇒
the thesis becomes
∀h:nat
.∀d:nat
.∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(lt m d)→(eq nat (g m) (f m))
→(eq nat (g d) w
→(∀m:nat.(le d m)→(eq nat (g (S m)) (f m))
→(eq
nat
weight_map g (lift (S h) d (TSort n))
weight_map g (lift (S h) d (TSort n)))))
assume h: nat
assume d: nat
assume f: nat→nat
assume g: nat→nat
suppose : ∀m:nat.(lt m d)→(eq nat (g m) (f m))
suppose : eq nat (g d) w
suppose : ∀m:nat.(le d m)→(eq nat (g (S m)) (f m))
by (refl_equal . .)
we proved
eq
nat
weight_map g (lift (S h) d (TSort n))
weight_map g (lift (S h) d (TSort n))
that is equivalent to
eq
nat
weight_map f (lift h d (TSort n))
weight_map g (lift (S h) d (TSort n))
∀h:nat
.∀d:nat
.∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(lt m d)→(eq nat (g m) (f m))
→(eq nat (g d) w
→(∀m:nat.(le d m)→(eq nat (g (S m)) (f m))
→(eq
nat
weight_map g (lift (S h) d (TSort n))
weight_map g (lift (S h) d (TSort n)))))
case TLRef : n:nat ⇒
the thesis becomes
∀h:nat
.∀d:nat
.∀f:nat→nat
.∀g:nat→nat
.∀H:∀m:nat.(lt m d)→(eq nat (g m) (f m))
.eq nat (g d) w
→∀H1:∀m:nat.(le d m)→(eq nat (g (S m)) (f m))
.eq
nat
weight_map f (lift h d (TLRef n))
weight_map g (lift (S h) d (TLRef n))
assume h: nat
assume d: nat
assume f: nat→nat
assume g: nat→nat
suppose H: ∀m:nat.(lt m d)→(eq nat (g m) (f m))
suppose : eq nat (g d) w
suppose H1: ∀m:nat.(le d m)→(eq nat (g (S m)) (f m))
(h1)
suppose H2: lt n d
(h1)
(h1)
by (H . H2)
we proved eq nat (g n) (f n)
by (sym_eq . . . previous)
we proved eq nat (f n) (g n)
eq nat (weight_map f (TLRef n)) (weight_map g (TLRef n))
end of h1
(h2)
by (lift_lref_lt . . . H2)
eq T (lift (S h) d (TLRef n)) (TLRef n)
end of h2
by (eq_ind_r . . . h1 . h2)
eq
nat
weight_map f (TLRef n)
weight_map g (lift (S h) d (TLRef n))
end of h1
(h2)
by (lift_lref_lt . . . H2)
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 g (lift (S h) d (TLRef n))
lt n d
→(eq
nat
weight_map f (lift h d (TLRef n))
weight_map g (lift (S h) d (TLRef n)))
end of h1
(h2)
suppose H2: le d n
(h1)
(h1)
by (plus_n_Sm . .)
we proved eq nat (S (plus n h)) (plus n (S h))
we proceed by induction on the previous result to prove eq nat (f (plus n h)) (g (plus n (S h)))
case refl_equal : ⇒
the thesis becomes eq nat (f (plus n h)) (g (S (plus n h)))
by (le_plus_trans . . . H2)
we proved le d (plus n h)
by (H1 . previous)
we proved eq nat (g (S (plus n h))) (f (plus n h))
by (sym_eq . . . previous)
eq nat (f (plus n h)) (g (S (plus n h)))
we proved eq nat (f (plus n h)) (g (plus n (S h)))
eq
nat
weight_map f (TLRef (plus n h))
weight_map g (TLRef (plus n (S h)))
end of h1
(h2)
by (lift_lref_ge . . . H2)
eq T (lift (S h) d (TLRef n)) (TLRef (plus n (S h)))
end of h2
by (eq_ind_r . . . h1 . h2)
eq
nat
weight_map f (TLRef (plus n h))
weight_map g (lift (S h) d (TLRef n))
end of h1
(h2)
by (lift_lref_ge . . . H2)
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 g (lift (S h) d (TLRef n))
le d n
→(eq
nat
weight_map f (lift h d (TLRef n))
weight_map g (lift (S h) d (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 g (lift (S h) d (TLRef n))
∀h:nat
.∀d:nat
.∀f:nat→nat
.∀g:nat→nat
.∀H:∀m:nat.(lt m d)→(eq nat (g m) (f m))
.eq nat (g d) w
→∀H1:∀m:nat.(le d m)→(eq nat (g (S m)) (f m))
.eq
nat
weight_map f (lift h d (TLRef n))
weight_map g (lift (S h) d (TLRef n))
case THead : k:K t0:T t1:T ⇒
the thesis becomes
∀h:nat
.∀d:nat
.∀f:nat→nat
.∀g:nat→nat
.∀H1:∀m:nat.(lt m d)→(eq nat (g m) (f m))
.∀H2:eq nat (g d) w
.∀H3:∀m:nat.(le d m)→(eq nat (g (S m)) (f m))
.eq
nat
weight_map f (lift h d (THead k t0 t1))
weight_map g (lift (S h) d (THead k t0 t1))
(H) by induction hypothesis we know
∀h:nat
.∀d:nat
.∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(lt m d)→(eq nat (g m) (f m))
→(eq nat (g d) w
→(∀m:nat.(le d m)→(eq nat (g (S m)) (f m))
→(eq
nat
weight_map f (lift h d t0)
weight_map g (lift (S h) d t0))))
(H0) by induction hypothesis we know
∀h:nat
.∀d:nat
.∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(lt m d)→(eq nat (g m) (f m))
→(eq nat (g d) w
→(∀m:nat.(le d m)→(eq nat (g (S m)) (f m))
→(eq
nat
weight_map f (lift h d t1)
weight_map g (lift (S h) d t1))))
assume h: nat
assume d: nat
assume f: nat→nat
assume g: nat→nat
suppose H1: ∀m:nat.(lt m d)→(eq nat (g m) (f m))
suppose H2: eq nat (g d) w
suppose H3: ∀m:nat.(le d m)→(eq nat (g (S m)) (f m))
we proceed by induction on k to prove
eq
nat
weight_map f (lift h d (THead k t0 t1))
weight_map g (lift (S h) d (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 g (lift (S h) d (THead (Bind b) t0 t1))
(h1)
(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 g (lift (S h) d t0)
weight_map
wadd g (S (weight_map g (lift (S h) d t0)))
lift (S h) (S d) t1
| Abst⇒
S
plus
weight_map g (lift (S h) d t0)
weight_map (wadd g O) (lift (S h) (S d) t1)
| Void⇒
S
plus
weight_map g (lift (S h) d t0)
weight_map (wadd g O) (lift (S h) (S d) 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 g (lift (S h) d t0)
weight_map
wadd g (S (weight_map g (lift (S h) d t0)))
lift (S h) (S d) t1
| Abst⇒
S
plus
weight_map g (lift (S h) d t0)
weight_map (wadd g O) (lift (S h) (S d) t1)
| Void⇒
S
plus
weight_map g (lift (S h) d t0)
weight_map (wadd g O) (lift (S h) (S d) t1)
(h1)
by (H . . . . H1 H2 H3)
eq
nat
weight_map f (lift h d t0)
weight_map g (lift (S h) d t0)
end of h1
(h2)
(h1)
assume m: nat
suppose H4: lt m (S d)
by (lt_gen_xS . . H4)
we proved or (eq nat m O) (ex2 nat λm:nat.eq nat m (S m) λm:nat.lt m d)
we proceed by induction on the previous result to prove
eq
nat
wadd g (S (weight_map g (lift (S h) d t0))) m
wadd f (S (weight_map f (lift h d t0))) m
case or_introl : H5:eq nat m O ⇒
the thesis becomes
eq
nat
wadd g (S (weight_map g (lift (S h) d t0))) m
wadd f (S (weight_map f (lift h d t0))) m
by (H . . . . H1 H2 H3)
we proved
eq
nat
weight_map f (lift h d t0)
weight_map g (lift (S h) d t0)
by (sym_eq . . . previous)
we proved
eq
nat
weight_map g (lift (S h) d t0)
weight_map f (lift h d t0)
by (f_equal . . . . . previous)
we proved
eq
nat
S (weight_map g (lift (S h) d t0))
S (weight_map f (lift h d t0))
that is equivalent to
eq
nat
wadd g (S (weight_map g (lift (S h) d t0))) O
wadd f (S (weight_map f (lift h d t0))) O
by (eq_ind_r . . . previous . H5)
eq
nat
wadd g (S (weight_map g (lift (S h) d t0))) m
wadd f (S (weight_map f (lift h d t0))) m
case or_intror : H5:ex2 nat λm0:nat.eq nat m (S m0) λm0:nat.lt m0 d ⇒
the thesis becomes
eq
nat
wadd g (S (weight_map g (lift (S h) d t0))) m
wadd f (S (weight_map f (lift h d t0))) m
we proceed by induction on H5 to prove
eq
nat
wadd g (S (weight_map g (lift (S h) d t0))) m
wadd f (S (weight_map f (lift h d t0))) m
case ex_intro2 : x:nat H6:eq nat m (S x) H7:lt x d ⇒
the thesis becomes
eq
nat
wadd g (S (weight_map g (lift (S h) d t0))) m
wadd f (S (weight_map f (lift h d t0))) m
by (H1 . H7)
we proved eq nat (g x) (f x)
that is equivalent to
eq
nat
wadd g (S (weight_map g (lift (S h) d t0))) (S x)
wadd f (S (weight_map f (lift h d t0))) (S x)
by (eq_ind_r . . . previous . H6)
eq
nat
wadd g (S (weight_map g (lift (S h) d t0))) m
wadd f (S (weight_map f (lift h d t0))) m
eq
nat
wadd g (S (weight_map g (lift (S h) d t0))) m
wadd f (S (weight_map f (lift h d t0))) m
we proved
eq
nat
wadd g (S (weight_map g (lift (S h) d t0))) m
wadd f (S (weight_map f (lift h d t0))) m
∀m:nat
.lt m (S d)
→(eq
nat
wadd g (S (weight_map g (lift (S h) d t0))) m
wadd f (S (weight_map f (lift h d t0))) m)
end of h1
(h2)
consider H2
we proved eq nat (g d) w
eq nat (wadd g (S (weight_map g (lift (S h) d t0))) (S d)) w
end of h2
(h3)
assume m: nat
suppose H4: le (S d) m
by (le_gen_S . . H4)
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 (g m) (wadd f (S (weight_map f (lift h d t0))) m)
case ex_intro2 : x:nat H5:eq nat m (S x) H6:le d x ⇒
the thesis becomes eq nat (g m) (wadd f (S (weight_map f (lift h d t0))) m)
by (H3 . H6)
we proved eq nat (g (S x)) (f x)
that is equivalent to
eq
nat
g (S x)
wadd f (S (weight_map f (lift h d t0))) (S x)
by (eq_ind_r . . . previous . H5)
eq nat (g m) (wadd f (S (weight_map f (lift h d t0))) m)
we proved eq nat (g m) (wadd f (S (weight_map f (lift h d t0))) m)
that is equivalent to
eq
nat
wadd g (S (weight_map g (lift (S h) d t0))) (S m)
wadd f (S (weight_map f (lift h d t0))) m
∀m:nat
.le (S d) m
→(eq
nat
wadd g (S (weight_map g (lift (S h) d t0))) (S m)
wadd f (S (weight_map f (lift h d t0))) m)
end of h3
by (H0 . . . . h1 h2 h3)
eq
nat
weight_map
wadd f (S (weight_map f (lift h d t0)))
lift h (S d) t1
weight_map
wadd g (S (weight_map g (lift (S h) d t0)))
lift (S h) (S d) 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 (S (weight_map f (lift h d t0)))
lift h (S d) t1
plus
weight_map g (lift (S h) d t0)
weight_map
wadd g (S (weight_map g (lift (S h) d t0)))
lift (S h) (S d) t1
by (f_equal . . . . . previous)
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 g (lift (S h) d t0)
weight_map
wadd g (S (weight_map g (lift (S h) d t0)))
lift (S h) (S d) 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 g (lift (S h) d t0)
weight_map
wadd g (S (weight_map g (lift (S h) d t0)))
lift (S h) (S d) t1
| Abst⇒
S
plus
weight_map g (lift (S h) d t0)
weight_map (wadd g O) (lift (S h) (S d) t1)
| Void⇒
S
plus
weight_map g (lift (S h) d t0)
weight_map (wadd g O) (lift (S h) (S d) 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 g (lift (S h) d t0)
weight_map
wadd g (S (weight_map g (lift (S h) d t0)))
lift (S h) (S d) t1
| Abst⇒
S
plus
weight_map g (lift (S h) d t0)
weight_map (wadd g O) (lift (S h) (S d) t1)
| Void⇒
S
plus
weight_map g (lift (S h) d t0)
weight_map (wadd g O) (lift (S h) (S d) t1)
(h1)
by (H . . . . H1 H2 H3)
eq
nat
weight_map f (lift h d t0)
weight_map g (lift (S h) d t0)
end of h1
(h2)
(h1)
assume m: nat
suppose H4: lt m (S d)
by (lt_gen_xS . . H4)
we proved or (eq nat m O) (ex2 nat λm:nat.eq nat m (S m) λm:nat.lt m d)
we proceed by induction on the previous result to prove eq nat (wadd g O m) (wadd f O m)
case or_introl : H5:eq nat m O ⇒
the thesis becomes eq nat (wadd g O m) (wadd f O m)
by (refl_equal . .)
we proved eq nat O O
that is equivalent to eq nat (wadd g O O) (wadd f O O)
by (eq_ind_r . . . previous . H5)
eq nat (wadd g O m) (wadd f O m)
case or_intror : H5:ex2 nat λm0:nat.eq nat m (S m0) λm0:nat.lt m0 d ⇒
the thesis becomes eq nat (wadd g O m) (wadd f O m)
we proceed by induction on H5 to prove eq nat (wadd g O m) (wadd f O m)
case ex_intro2 : x:nat H6:eq nat m (S x) H7:lt x d ⇒
the thesis becomes eq nat (wadd g O m) (wadd f O m)
by (H1 . H7)
we proved eq nat (g x) (f x)
that is equivalent to eq nat (wadd g O (S x)) (wadd f O (S x))
by (eq_ind_r . . . previous . H6)
eq nat (wadd g O m) (wadd f O m)
eq nat (wadd g O m) (wadd f O m)
we proved eq nat (wadd g O m) (wadd f O m)
∀m:nat.(lt m (S d))→(eq nat (wadd g O m) (wadd f O m))
end of h1
(h2)
consider H2
we proved eq nat (g d) w
eq nat (wadd g O (S d)) w
end of h2
(h3)
assume m: nat
suppose H4: le (S d) m
by (le_gen_S . . H4)
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 (g m) (wadd f O m)
case ex_intro2 : x:nat H5:eq nat m (S x) H6:le d x ⇒
the thesis becomes eq nat (g m) (wadd f O m)
by (H3 . H6)
we proved eq nat (g (S x)) (f x)
that is equivalent to eq nat (g (S x)) (wadd f O (S x))
by (eq_ind_r . . . previous . H5)
eq nat (g m) (wadd f O m)
we proved eq nat (g m) (wadd f O m)
that is equivalent to eq nat (wadd g O (S m)) (wadd f O m)
∀m:nat.(le (S d) m)→(eq nat (wadd g O (S m)) (wadd f O m))
end of h3
by (H0 . . . . h1 h2 h3)
eq
nat
weight_map (wadd f O) (lift h (S d) t1)
weight_map (wadd g O) (lift (S h) (S d) 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) (lift h (S d) t1)
plus
weight_map g (lift (S h) d t0)
weight_map (wadd g O) (lift (S h) (S d) t1)
by (f_equal . . . . . previous)
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 g (lift (S h) d t0)
weight_map (wadd g O) (lift (S h) (S d) 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 g (lift (S h) d t0)
weight_map
wadd g (S (weight_map g (lift (S h) d t0)))
lift (S h) (S d) t1
| Abst⇒
S
plus
weight_map g (lift (S h) d t0)
weight_map (wadd g O) (lift (S h) (S d) t1)
| Void⇒
S
plus
weight_map g (lift (S h) d t0)
weight_map (wadd g O) (lift (S h) (S d) 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 g (lift (S h) d t0)
weight_map
wadd g (S (weight_map g (lift (S h) d t0)))
lift (S h) (S d) t1
| Abst⇒
S
plus
weight_map g (lift (S h) d t0)
weight_map (wadd g O) (lift (S h) (S d) t1)
| Void⇒
S
plus
weight_map g (lift (S h) d t0)
weight_map (wadd g O) (lift (S h) (S d) t1)
(h1)
by (H . . . . H1 H2 H3)
eq
nat
weight_map f (lift h d t0)
weight_map g (lift (S h) d t0)
end of h1
(h2)
(h1)
assume m: nat
suppose H4: lt m (S d)
by (lt_gen_xS . . H4)
we proved or (eq nat m O) (ex2 nat λm:nat.eq nat m (S m) λm:nat.lt m d)
we proceed by induction on the previous result to prove eq nat (wadd g O m) (wadd f O m)
case or_introl : H5:eq nat m O ⇒
the thesis becomes eq nat (wadd g O m) (wadd f O m)
by (refl_equal . .)
we proved eq nat O O
that is equivalent to eq nat (wadd g O O) (wadd f O O)
by (eq_ind_r . . . previous . H5)
eq nat (wadd g O m) (wadd f O m)
case or_intror : H5:ex2 nat λm0:nat.eq nat m (S m0) λm0:nat.lt m0 d ⇒
the thesis becomes eq nat (wadd g O m) (wadd f O m)
we proceed by induction on H5 to prove eq nat (wadd g O m) (wadd f O m)
case ex_intro2 : x:nat H6:eq nat m (S x) H7:lt x d ⇒
the thesis becomes eq nat (wadd g O m) (wadd f O m)
by (H1 . H7)
we proved eq nat (g x) (f x)
that is equivalent to eq nat (wadd g O (S x)) (wadd f O (S x))
by (eq_ind_r . . . previous . H6)
eq nat (wadd g O m) (wadd f O m)
eq nat (wadd g O m) (wadd f O m)
we proved eq nat (wadd g O m) (wadd f O m)
∀m:nat.(lt m (S d))→(eq nat (wadd g O m) (wadd f O m))
end of h1
(h2)
consider H2
we proved eq nat (g d) w
eq nat (wadd g O (S d)) w
end of h2
(h3)
assume m: nat
suppose H4: le (S d) m
by (le_gen_S . . H4)
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 (g m) (wadd f O m)
case ex_intro2 : x:nat H5:eq nat m (S x) H6:le d x ⇒
the thesis becomes eq nat (g m) (wadd f O m)
by (H3 . H6)
we proved eq nat (g (S x)) (f x)
that is equivalent to eq nat (g (S x)) (wadd f O (S x))
by (eq_ind_r . . . previous . H5)
eq nat (g m) (wadd f O m)
we proved eq nat (g m) (wadd f O m)
that is equivalent to eq nat (wadd g O (S m)) (wadd f O m)
∀m:nat.(le (S d) m)→(eq nat (wadd g O (S m)) (wadd f O m))
end of h3
by (H0 . . . . h1 h2 h3)
eq
nat
weight_map (wadd f O) (lift h (S d) t1)
weight_map (wadd g O) (lift (S h) (S d) 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) (lift h (S d) t1)
plus
weight_map g (lift (S h) d t0)
weight_map (wadd g O) (lift (S h) (S d) t1)
by (f_equal . . . . . previous)
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 g (lift (S h) d t0)
weight_map (wadd g O) (lift (S h) (S d) 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 g (lift (S h) d t0)
weight_map
wadd g (S (weight_map g (lift (S h) d t0)))
lift (S h) (S d) t1
| Abst⇒
S
plus
weight_map g (lift (S h) d t0)
weight_map (wadd g O) (lift (S h) (S d) t1)
| Void⇒
S
plus
weight_map g (lift (S h) d t0)
weight_map (wadd g O) (lift (S h) (S d) 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 g (lift (S h) d t0)
weight_map
wadd g (S (weight_map g (lift (S h) d t0)))
lift (S h) (S d) t1
| Abst⇒
S
plus
weight_map g (lift (S h) d t0)
weight_map (wadd g O) (lift (S h) (S d) t1)
| Void⇒
S
plus
weight_map g (lift (S h) d t0)
weight_map (wadd g O) (lift (S h) (S d) t1)
eq
nat
weight_map
f
THead (Bind b) (lift h d t0) (lift h (s (Bind b) d) t1)
weight_map
g
THead (Bind b) (lift (S h) d t0) (lift (S h) (s (Bind b) d) t1)
end of h1
(h2)
by (lift_head . . . . .)
eq
T
lift (S h) d (THead (Bind b) t0 t1)
THead (Bind b) (lift (S h) d t0) (lift (S h) (s (Bind b) d) t1)
end of h2
by (eq_ind_r . . . h1 . h2)
eq
nat
weight_map
f
THead (Bind b) (lift h d t0) (lift h (s (Bind b) d) t1)
weight_map g (lift (S h) d (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 g (lift (S h) d (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 g (lift (S h) d (THead (Flat f0) t0 t1))
(h1)
(h1)
(h1)
by (H . . . . H1 H2 H3)
eq
nat
weight_map f (lift h d t0)
weight_map g (lift (S h) d t0)
end of h1
(h2)
by (H0 . . . . H1 H2 H3)
eq
nat
weight_map f (lift h d t1)
weight_map g (lift (S h) d 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 g (lift (S h) d t0)
weight_map g (lift (S h) d 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 g (lift (S h) d t0)
weight_map g (lift (S h) d t1)
eq
nat
weight_map
f
THead (Flat f0) (lift h d t0) (lift h (s (Flat f0) d) t1)
weight_map
g
THead (Flat f0) (lift (S h) d t0) (lift (S h) (s (Flat f0) d) t1)
end of h1
(h2)
by (lift_head . . . . .)
eq
T
lift (S h) d (THead (Flat f0) t0 t1)
THead (Flat f0) (lift (S h) d t0) (lift (S h) (s (Flat f0) d) t1)
end of h2
by (eq_ind_r . . . h1 . h2)
eq
nat
weight_map
f
THead (Flat f0) (lift h d t0) (lift h (s (Flat f0) d) t1)
weight_map g (lift (S h) d (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 g (lift (S h) d (THead (Flat f0) t0 t1))
we proved
eq
nat
weight_map f (lift h d (THead k t0 t1))
weight_map g (lift (S h) d (THead k t0 t1))
∀h:nat
.∀d:nat
.∀f:nat→nat
.∀g:nat→nat
.∀H1:∀m:nat.(lt m d)→(eq nat (g m) (f m))
.∀H2:eq nat (g d) w
.∀H3:∀m:nat.(le d m)→(eq nat (g (S m)) (f m))
.eq
nat
weight_map f (lift h d (THead k t0 t1))
weight_map g (lift (S h) d (THead k t0 t1))
we proved
∀h:nat
.∀d:nat
.∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(lt m d)→(eq nat (g m) (f m))
→(eq nat (g d) w
→(∀m:nat.(le d m)→(eq nat (g (S m)) (f m))
→(eq
nat
weight_map f (lift h d t)
weight_map g (lift (S h) d t))))
we proved
∀w:nat
.∀t:T
.∀h:nat
.∀d:nat
.∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(lt m d)→(eq nat (g m) (f m))
→(eq nat (g d) w
→(∀m:nat.(le d m)→(eq nat (g (S m)) (f m))
→(eq
nat
weight_map f (lift h d t)
weight_map g (lift (S h) d t))))