DEFINITION weight_le()
TYPE =
∀t:T
.∀f:nat→nat
.∀g:nat→nat
.∀n:nat.(le (f n) (g n))
→le (weight_map f t) (weight_map g t)
BODY =
assume t: T
we proceed by induction on t to prove
∀f:nat→nat
.∀g:nat→nat
.∀n:nat.(le (f n) (g n))
→le (weight_map f t) (weight_map g t)
case TSort : n:nat ⇒
the thesis becomes
∀f:nat→nat
.∀g:nat→nat
.∀n0:nat.(le (f n0) (g n0))
→le (weight_map g (TSort n)) (weight_map g (TSort n))
assume f: nat→nat
assume g: nat→nat
suppose : ∀n0:nat.(le (f n0) (g n0))
by (le_n .)
we proved le (weight_map g (TSort n)) (weight_map g (TSort n))
that is equivalent to le (weight_map f (TSort n)) (weight_map g (TSort n))
∀f:nat→nat
.∀g:nat→nat
.∀n0:nat.(le (f n0) (g n0))
→le (weight_map g (TSort n)) (weight_map g (TSort n))
case TLRef : n:nat ⇒
the thesis becomes
∀f:nat→nat
.∀g:nat→nat.∀H:∀n0:nat.(le (f n0) (g n0)).(le (f n) (g n))
assume f: nat→nat
assume g: nat→nat
suppose H: ∀n0:nat.(le (f n0) (g n0))
by (H .)
we proved le (f n) (g n)
that is equivalent to le (weight_map f (TLRef n)) (weight_map g (TLRef n))
∀f:nat→nat
.∀g:nat→nat.∀H:∀n0:nat.(le (f n0) (g n0)).(le (f n) (g n))
case THead ⇒
we need to prove
∀k:K
.∀t0:T
.∀f:nat→nat
.∀g:nat→nat
.∀n:nat.(le (f n) (g n))
→le (weight_map f t0) (weight_map g t0)
→∀t1:T
.∀f:nat→nat
.∀g:nat→nat
.∀n:nat.(le (f n) (g n))
→le (weight_map f t1) (weight_map g t1)
→∀f:nat→nat
.∀g:nat→nat
.∀n:nat.(le (f n) (g n))
→le (weight_map f (THead k t0 t1)) (weight_map g (THead k t0 t1))
assume k: K
we proceed by induction on k to prove
∀t0:T
.∀f:nat→nat
.∀g:nat→nat
.∀n:nat.(le (f n) (g n))
→le (weight_map f t0) (weight_map g t0)
→∀t1:T
.∀f:nat→nat
.∀g:nat→nat
.∀n:nat.(le (f n) (g n))
→le (weight_map f t1) (weight_map g t1)
→∀f:nat→nat
.∀g:nat→nat
.∀n:nat.(le (f n) (g n))
→le (weight_map f (THead k t0 t1)) (weight_map g (THead k t0 t1))
case Bind : b:B ⇒
the thesis becomes
∀t0:T
.∀f:nat→nat
.∀g:nat→nat
.∀n:nat.(le (f n) (g n))
→le (weight_map f t0) (weight_map g t0)
→∀t1:T
.∀f:nat→nat
.∀g:nat→nat
.∀n:nat.(le (f n) (g n))
→le (weight_map f t1) (weight_map g t1)
→∀f:nat→nat
.∀g:nat→nat
.∀n:nat.(le (f n) (g n))
→(le
weight_map f (THead (Bind b) t0 t1)
weight_map g (THead (Bind b) t0 t1))
we proceed by induction on b to prove
∀t0:T
.∀f:nat→nat
.∀g:nat→nat
.∀n:nat.(le (f n) (g n))
→le (weight_map f t0) (weight_map g t0)
→∀t1:T
.∀f:nat→nat
.∀g:nat→nat
.∀n:nat.(le (f n) (g n))
→le (weight_map f t1) (weight_map g t1)
→∀f:nat→nat
.∀g:nat→nat
.∀n:nat.(le (f n) (g n))
→(le
<λ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))
<λb1:B.nat>
CASE b OF
Abbr⇒
S
plus
weight_map g t0
weight_map (wadd g (S (weight_map g t0))) t1
| Abst⇒S (plus (weight_map g t0) (weight_map (wadd g O) t1))
| Void⇒S (plus (weight_map g t0) (weight_map (wadd g O) t1)))
case Abbr : ⇒
the thesis becomes
∀t0:T
.∀f:nat→nat
.∀g:nat→nat
.∀n:nat.(le (f n) (g n))
→le (weight_map f t0) (weight_map g t0)
→∀t1:T
.∀f:nat→nat
.∀g:nat→nat
.∀n:nat.(le (f n) (g n))
→le (weight_map f t1) (weight_map g t1)
→∀f:nat→nat
.∀g:nat→nat
.∀n:nat.(le (f n) (g n))
→(le
<λ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))
<λb1:B.nat>
CASE Abbr OF
Abbr⇒
S
plus
weight_map g t0
weight_map (wadd g (S (weight_map g t0))) t1
| Abst⇒S (plus (weight_map g t0) (weight_map (wadd g O) t1))
| Void⇒S (plus (weight_map g t0) (weight_map (wadd g O) t1)))
assume t0: T
suppose H:
∀f:nat→nat
.∀g:nat→nat
.∀n:nat.(le (f n) (g n))
→le (weight_map f t0) (weight_map g t0)
assume t1: T
suppose H0:
∀f:nat→nat
.∀g:nat→nat
.∀n:nat.(le (f n) (g n))
→le (weight_map f t1) (weight_map g t1)
assume f: nat→nat
assume g: nat→nat
suppose H1: ∀n:nat.(le (f n) (g n))
(h1)
by (H . . H1)
le (weight_map f t0) (weight_map g t0)
end of h1
(h2)
assume n: nat
by (H . . H1)
we proved le (weight_map f t0) (weight_map g t0)
by (le_n_S . . previous)
we proved le (S (weight_map f t0)) (S (weight_map g t0))
by (wadd_le . . H1 . . previous .)
we proved
le
wadd f (S (weight_map f t0)) n
wadd g (S (weight_map g t0)) n
we proved
∀n:nat
.le
wadd f (S (weight_map f t0)) n
wadd g (S (weight_map g t0)) n
by (H0 . . previous)
le
weight_map (wadd f (S (weight_map f t0))) t1
weight_map (wadd g (S (weight_map g t0))) t1
end of h2
by (le_plus_plus . . . . h1 h2)
we proved
le
plus
weight_map f t0
weight_map (wadd f (S (weight_map f t0))) t1
plus
weight_map g t0
weight_map (wadd g (S (weight_map g t0))) t1
by (le_n_S . . previous)
we proved
le
S
plus
weight_map f t0
weight_map (wadd f (S (weight_map f t0))) t1
S
plus
weight_map g t0
weight_map (wadd g (S (weight_map g t0))) t1
that is equivalent to
le
<λ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))
<λb1:B.nat>
CASE Abbr OF
Abbr⇒
S
plus
weight_map g t0
weight_map (wadd g (S (weight_map g t0))) t1
| Abst⇒S (plus (weight_map g t0) (weight_map (wadd g O) t1))
| Void⇒S (plus (weight_map g t0) (weight_map (wadd g O) t1))
∀t0:T
.∀f:nat→nat
.∀g:nat→nat
.∀n:nat.(le (f n) (g n))
→le (weight_map f t0) (weight_map g t0)
→∀t1:T
.∀f:nat→nat
.∀g:nat→nat
.∀n:nat.(le (f n) (g n))
→le (weight_map f t1) (weight_map g t1)
→∀f:nat→nat
.∀g:nat→nat
.∀n:nat.(le (f n) (g n))
→(le
<λ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))
<λb1:B.nat>
CASE Abbr OF
Abbr⇒
S
plus
weight_map g t0
weight_map (wadd g (S (weight_map g t0))) t1
| Abst⇒S (plus (weight_map g t0) (weight_map (wadd g O) t1))
| Void⇒S (plus (weight_map g t0) (weight_map (wadd g O) t1)))
case Abst : ⇒
the thesis becomes
∀t0:T
.∀f:nat→nat
.∀g:nat→nat
.∀n:nat.(le (f n) (g n))
→le (weight_map f t0) (weight_map g t0)
→∀t1:T
.∀f:nat→nat
.∀g:nat→nat
.∀n:nat.(le (f n) (g n))
→le (weight_map f t1) (weight_map g t1)
→∀f:nat→nat
.∀g:nat→nat
.∀n:nat.(le (f n) (g n))
→(le
<λ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))
<λb1:B.nat>
CASE Abst OF
Abbr⇒
S
plus
weight_map g t0
weight_map (wadd g (S (weight_map g t0))) t1
| Abst⇒S (plus (weight_map g t0) (weight_map (wadd g O) t1))
| Void⇒S (plus (weight_map g t0) (weight_map (wadd g O) t1)))
assume t0: T
suppose H:
∀f:nat→nat
.∀g:nat→nat
.∀n:nat.(le (f n) (g n))
→le (weight_map f t0) (weight_map g t0)
assume t1: T
suppose H0:
∀f:nat→nat
.∀g:nat→nat
.∀n:nat.(le (f n) (g n))
→le (weight_map f t1) (weight_map g t1)
assume f: nat→nat
assume g: nat→nat
suppose H1: ∀n:nat.(le (f n) (g n))
(h1)
by (H . . H1)
le (weight_map f t0) (weight_map g t0)
end of h1
(h2)
assume n: nat
by (le_n .)
we proved le O O
by (wadd_le . . H1 . . previous .)
we proved le (wadd f O n) (wadd g O n)
we proved ∀n:nat.(le (wadd f O n) (wadd g O n))
by (H0 . . previous)
le (weight_map (wadd f O) t1) (weight_map (wadd g O) t1)
end of h2
by (le_plus_plus . . . . h1 h2)
we proved
le
plus (weight_map f t0) (weight_map (wadd f O) t1)
plus (weight_map g t0) (weight_map (wadd g O) t1)
by (le_n_S . . previous)
we proved
le
S (plus (weight_map f t0) (weight_map (wadd f O) t1))
S (plus (weight_map g t0) (weight_map (wadd g O) t1))
that is equivalent to
le
<λ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))
<λb1:B.nat>
CASE Abst OF
Abbr⇒
S
plus
weight_map g t0
weight_map (wadd g (S (weight_map g t0))) t1
| Abst⇒S (plus (weight_map g t0) (weight_map (wadd g O) t1))
| Void⇒S (plus (weight_map g t0) (weight_map (wadd g O) t1))
∀t0:T
.∀f:nat→nat
.∀g:nat→nat
.∀n:nat.(le (f n) (g n))
→le (weight_map f t0) (weight_map g t0)
→∀t1:T
.∀f:nat→nat
.∀g:nat→nat
.∀n:nat.(le (f n) (g n))
→le (weight_map f t1) (weight_map g t1)
→∀f:nat→nat
.∀g:nat→nat
.∀n:nat.(le (f n) (g n))
→(le
<λ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))
<λb1:B.nat>
CASE Abst OF
Abbr⇒
S
plus
weight_map g t0
weight_map (wadd g (S (weight_map g t0))) t1
| Abst⇒S (plus (weight_map g t0) (weight_map (wadd g O) t1))
| Void⇒S (plus (weight_map g t0) (weight_map (wadd g O) t1)))
case Void : ⇒
the thesis becomes
∀t0:T
.∀f:nat→nat
.∀g:nat→nat
.∀n:nat.(le (f n) (g n))
→le (weight_map f t0) (weight_map g t0)
→∀t1:T
.∀f:nat→nat
.∀g:nat→nat
.∀n:nat.(le (f n) (g n))
→le (weight_map f t1) (weight_map g t1)
→∀f:nat→nat
.∀g:nat→nat
.∀n:nat.(le (f n) (g n))
→(le
<λ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))
<λb1:B.nat>
CASE Void OF
Abbr⇒
S
plus
weight_map g t0
weight_map (wadd g (S (weight_map g t0))) t1
| Abst⇒S (plus (weight_map g t0) (weight_map (wadd g O) t1))
| Void⇒S (plus (weight_map g t0) (weight_map (wadd g O) t1)))
assume t0: T
suppose H:
∀f:nat→nat
.∀g:nat→nat
.∀n:nat.(le (f n) (g n))
→le (weight_map f t0) (weight_map g t0)
assume t1: T
suppose H0:
∀f:nat→nat
.∀g:nat→nat
.∀n:nat.(le (f n) (g n))
→le (weight_map f t1) (weight_map g t1)
assume f: nat→nat
assume g: nat→nat
suppose H1: ∀n:nat.(le (f n) (g n))
(h1)
by (H . . H1)
le (weight_map f t0) (weight_map g t0)
end of h1
(h2)
assume n: nat
by (le_n .)
we proved le O O
by (wadd_le . . H1 . . previous .)
we proved le (wadd f O n) (wadd g O n)
we proved ∀n:nat.(le (wadd f O n) (wadd g O n))
by (H0 . . previous)
le (weight_map (wadd f O) t1) (weight_map (wadd g O) t1)
end of h2
by (le_plus_plus . . . . h1 h2)
we proved
le
plus (weight_map f t0) (weight_map (wadd f O) t1)
plus (weight_map g t0) (weight_map (wadd g O) t1)
by (le_n_S . . previous)
we proved
le
S (plus (weight_map f t0) (weight_map (wadd f O) t1))
S (plus (weight_map g t0) (weight_map (wadd g O) t1))
that is equivalent to
le
<λ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))
<λb1:B.nat>
CASE Void OF
Abbr⇒
S
plus
weight_map g t0
weight_map (wadd g (S (weight_map g t0))) t1
| Abst⇒S (plus (weight_map g t0) (weight_map (wadd g O) t1))
| Void⇒S (plus (weight_map g t0) (weight_map (wadd g O) t1))
∀t0:T
.∀f:nat→nat
.∀g:nat→nat
.∀n:nat.(le (f n) (g n))
→le (weight_map f t0) (weight_map g t0)
→∀t1:T
.∀f:nat→nat
.∀g:nat→nat
.∀n:nat.(le (f n) (g n))
→le (weight_map f t1) (weight_map g t1)
→∀f:nat→nat
.∀g:nat→nat
.∀n:nat.(le (f n) (g n))
→(le
<λ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))
<λb1:B.nat>
CASE Void OF
Abbr⇒
S
plus
weight_map g t0
weight_map (wadd g (S (weight_map g t0))) t1
| Abst⇒S (plus (weight_map g t0) (weight_map (wadd g O) t1))
| Void⇒S (plus (weight_map g t0) (weight_map (wadd g O) t1)))
we proved
∀t0:T
.∀f:nat→nat
.∀g:nat→nat
.∀n:nat.(le (f n) (g n))
→le (weight_map f t0) (weight_map g t0)
→∀t1:T
.∀f:nat→nat
.∀g:nat→nat
.∀n:nat.(le (f n) (g n))
→le (weight_map f t1) (weight_map g t1)
→∀f:nat→nat
.∀g:nat→nat
.∀n:nat.(le (f n) (g n))
→(le
<λ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))
<λb1:B.nat>
CASE b OF
Abbr⇒
S
plus
weight_map g t0
weight_map (wadd g (S (weight_map g t0))) t1
| Abst⇒S (plus (weight_map g t0) (weight_map (wadd g O) t1))
| Void⇒S (plus (weight_map g t0) (weight_map (wadd g O) t1)))
∀t0:T
.∀f:nat→nat
.∀g:nat→nat
.∀n:nat.(le (f n) (g n))
→le (weight_map f t0) (weight_map g t0)
→∀t1:T
.∀f:nat→nat
.∀g:nat→nat
.∀n:nat.(le (f n) (g n))
→le (weight_map f t1) (weight_map g t1)
→∀f:nat→nat
.∀g:nat→nat
.∀n:nat.(le (f n) (g n))
→(le
weight_map f (THead (Bind b) t0 t1)
weight_map g (THead (Bind b) t0 t1))
case Flat : :F ⇒
the thesis becomes
∀t0:T
.∀H:∀f0:nat→nat
.∀g:nat→nat
.(∀n:nat.(le (f0 n) (g n)))→(le (weight_map f0 t0) (weight_map g t0))
.∀t1:T
.∀H0:∀f0:nat→nat
.∀g:nat→nat
.(∀n:nat.(le (f0 n) (g n)))→(le (weight_map f0 t1) (weight_map g t1))
.∀f0:nat→nat
.∀g:nat→nat
.∀H1:∀n:nat.(le (f0 n) (g n))
.le
S (plus (weight_map f0 t0) (weight_map f0 t1))
S (plus (weight_map g t0) (weight_map g t1))
assume t0: T
suppose H:
∀f0:nat→nat
.∀g:nat→nat
.(∀n:nat.(le (f0 n) (g n)))→(le (weight_map f0 t0) (weight_map g t0))
assume t1: T
suppose H0:
∀f0:nat→nat
.∀g:nat→nat
.(∀n:nat.(le (f0 n) (g n)))→(le (weight_map f0 t1) (weight_map g t1))
assume f0: nat→nat
assume g: nat→nat
suppose H1: ∀n:nat.(le (f0 n) (g n))
(h1)
by (H . . H1)
le (weight_map f0 t0) (weight_map g t0)
end of h1
(h2)
by (H0 . . H1)
le (weight_map f0 t1) (weight_map g t1)
end of h2
by (le_plus_plus . . . . h1 h2)
we proved
le
plus (weight_map f0 t0) (weight_map f0 t1)
plus (weight_map g t0) (weight_map g t1)
by (le_n_S . . previous)
we proved
le
S (plus (weight_map f0 t0) (weight_map f0 t1))
S (plus (weight_map g t0) (weight_map g t1))
that is equivalent to
le
weight_map f0 (THead (Flat __8) t0 t1)
weight_map g (THead (Flat __8) t0 t1)
∀t0:T
.∀H:∀f0:nat→nat
.∀g:nat→nat
.(∀n:nat.(le (f0 n) (g n)))→(le (weight_map f0 t0) (weight_map g t0))
.∀t1:T
.∀H0:∀f0:nat→nat
.∀g:nat→nat
.(∀n:nat.(le (f0 n) (g n)))→(le (weight_map f0 t1) (weight_map g t1))
.∀f0:nat→nat
.∀g:nat→nat
.∀H1:∀n:nat.(le (f0 n) (g n))
.le
S (plus (weight_map f0 t0) (weight_map f0 t1))
S (plus (weight_map g t0) (weight_map g t1))
we proved
∀t0:T
.∀f:nat→nat
.∀g:nat→nat
.∀n:nat.(le (f n) (g n))
→le (weight_map f t0) (weight_map g t0)
→∀t1:T
.∀f:nat→nat
.∀g:nat→nat
.∀n:nat.(le (f n) (g n))
→le (weight_map f t1) (weight_map g t1)
→∀f:nat→nat
.∀g:nat→nat
.∀n:nat.(le (f n) (g n))
→le (weight_map f (THead k t0 t1)) (weight_map g (THead k t0 t1))
∀k:K
.∀t0:T
.∀f:nat→nat
.∀g:nat→nat
.∀n:nat.(le (f n) (g n))
→le (weight_map f t0) (weight_map g t0)
→∀t1:T
.∀f:nat→nat
.∀g:nat→nat
.∀n:nat.(le (f n) (g n))
→le (weight_map f t1) (weight_map g t1)
→∀f:nat→nat
.∀g:nat→nat
.∀n:nat.(le (f n) (g n))
→le (weight_map f (THead k t0 t1)) (weight_map g (THead k t0 t1))
we proved
∀f:nat→nat
.∀g:nat→nat
.∀n:nat.(le (f n) (g n))
→le (weight_map f t) (weight_map g t)
we proved
∀t:T
.∀f:nat→nat
.∀g:nat→nat
.∀n:nat.(le (f n) (g n))
→le (weight_map f t) (weight_map g t)