DEFINITION subst0_weight_le()
TYPE =
∀u:T
.∀t:T
.∀z:T
.∀d:nat
.subst0 d u t z
→∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S d) O u)) (g d)
→le (weight_map f z) (weight_map g t))
BODY =
assume u: T
assume t: T
assume z: T
assume d: nat
suppose H: subst0 d u t z
we proceed by induction on H to prove
∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S d) O u)) (g d)
→le (weight_map f z) (weight_map g t))
case subst0_lref : v:T i:nat ⇒
the thesis becomes
∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→∀H1:lt (weight_map f (lift (S i) O v)) (g i)
.le
weight_map f (lift (S i) O v)
weight_map g (TLRef i)
assume f: nat→nat
assume g: nat→nat
suppose : ∀m:nat.(le (f m) (g m))
suppose H1: lt (weight_map f (lift (S i) O v)) (g i)
consider H1
we proved lt (weight_map f (lift (S i) O v)) (g i)
that is equivalent to
le
S (weight_map f (lift (S i) O v))
weight_map g (TLRef i)
by (le_S . . previous)
we proved
le
S (weight_map f (lift (S i) O v))
S (weight_map g (TLRef i))
by (le_S_n . . previous)
we proved
le
weight_map f (lift (S i) O v)
weight_map g (TLRef i)
∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→∀H1:lt (weight_map f (lift (S i) O v)) (g i)
.le
weight_map f (lift (S i) O v)
weight_map g (TLRef i)
case subst0_fst : v:T u2:T u1:T i:nat :subst0 i v u1 u2 t0:T k:K ⇒
the thesis becomes
∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→le (weight_map f (THead k u2 t0)) (weight_map g (THead k u1 t0)))
(H1) by induction hypothesis we know
∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→le (weight_map f u2) (weight_map g u1))
we proceed by induction on k to prove
∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→le (weight_map f (THead k u2 t0)) (weight_map g (THead k u1 t0)))
case Bind : b:B ⇒
the thesis becomes
∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind b) u2 t0)
weight_map g (THead (Bind b) u1 t0)))
we proceed by induction on b to prove
∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind b) u2 t0)
weight_map g (THead (Bind b) u1 t0)))
case Abbr : ⇒
the thesis becomes
∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind Abbr) u2 t0)
weight_map g (THead (Bind Abbr) u1 t0)))
assume f: nat→nat
assume g: nat→nat
suppose H2: ∀m:nat.(le (f m) (g m))
suppose H3: lt (weight_map f (lift (S i) O v)) (g i)
(h1)
by (H1 . . H2 H3)
le (weight_map f u2) (weight_map g u1)
end of h1
(h2)
assume n: nat
by (H1 . . H2 H3)
we proved le (weight_map f u2) (weight_map g u1)
by (le_n_S . . previous)
we proved le (S (weight_map f u2)) (S (weight_map g u1))
by (wadd_le . . H2 . . previous .)
we proved
le
wadd f (S (weight_map f u2)) n
wadd g (S (weight_map g u1)) n
we proved
∀n:nat
.le
wadd f (S (weight_map f u2)) n
wadd g (S (weight_map g u1)) n
by (weight_le . . . previous)
le
weight_map (wadd f (S (weight_map f u2))) t0
weight_map (wadd g (S (weight_map g u1))) t0
end of h2
by (le_plus_plus . . . . h1 h2)
we proved
le
plus
weight_map f u2
weight_map (wadd f (S (weight_map f u2))) t0
plus
weight_map g u1
weight_map (wadd g (S (weight_map g u1))) t0
by (le_n_S . . previous)
we proved
le
S
plus
weight_map f u2
weight_map (wadd f (S (weight_map f u2))) t0
S
plus
weight_map g u1
weight_map (wadd g (S (weight_map g u1))) t0
that is equivalent to
le
weight_map f (THead (Bind Abbr) u2 t0)
weight_map g (THead (Bind Abbr) u1 t0)
∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind Abbr) u2 t0)
weight_map g (THead (Bind Abbr) u1 t0)))
case Abst : ⇒
the thesis becomes
∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind Abst) u2 t0)
weight_map g (THead (Bind Abst) u1 t0)))
assume f: nat→nat
assume g: nat→nat
suppose H2: ∀m:nat.(le (f m) (g m))
suppose H3: lt (weight_map f (lift (S i) O v)) (g i)
(h1)
by (H1 . . H2 H3)
le (weight_map f u2) (weight_map g u1)
end of h1
(h2)
assume n: nat
by (le_n .)
we proved le O O
by (wadd_le . . H2 . . 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 (weight_le . . . previous)
le (weight_map (wadd f O) t0) (weight_map (wadd g O) t0)
end of h2
by (le_plus_plus . . . . h1 h2)
we proved
le
plus (weight_map f u2) (weight_map (wadd f O) t0)
plus (weight_map g u1) (weight_map (wadd g O) t0)
by (le_n_S . . previous)
we proved
le
S (plus (weight_map f u2) (weight_map (wadd f O) t0))
S (plus (weight_map g u1) (weight_map (wadd g O) t0))
that is equivalent to
le
weight_map f (THead (Bind Abst) u2 t0)
weight_map g (THead (Bind Abst) u1 t0)
∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind Abst) u2 t0)
weight_map g (THead (Bind Abst) u1 t0)))
case Void : ⇒
the thesis becomes
∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind Void) u2 t0)
weight_map g (THead (Bind Void) u1 t0)))
assume f: nat→nat
assume g: nat→nat
suppose H2: ∀m:nat.(le (f m) (g m))
suppose H3: lt (weight_map f (lift (S i) O v)) (g i)
(h1)
by (H1 . . H2 H3)
le (weight_map f u2) (weight_map g u1)
end of h1
(h2)
assume n: nat
by (le_n .)
we proved le O O
by (wadd_le . . H2 . . 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 (weight_le . . . previous)
le (weight_map (wadd f O) t0) (weight_map (wadd g O) t0)
end of h2
by (le_plus_plus . . . . h1 h2)
we proved
le
plus (weight_map f u2) (weight_map (wadd f O) t0)
plus (weight_map g u1) (weight_map (wadd g O) t0)
by (le_n_S . . previous)
we proved
le
S (plus (weight_map f u2) (weight_map (wadd f O) t0))
S (plus (weight_map g u1) (weight_map (wadd g O) t0))
that is equivalent to
le
weight_map f (THead (Bind Void) u2 t0)
weight_map g (THead (Bind Void) u1 t0)
∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind Void) u2 t0)
weight_map g (THead (Bind Void) u1 t0)))
∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind b) u2 t0)
weight_map g (THead (Bind b) u1 t0)))
case Flat : :F ⇒
the thesis becomes
∀f0:nat→nat
.∀g:nat→nat
.∀H2:∀m:nat.(le (f0 m) (g m))
.∀H3:lt (weight_map f0 (lift (S i) O v)) (g i)
.le
S (plus (weight_map f0 u2) (weight_map f0 t0))
S (plus (weight_map g u1) (weight_map g t0))
assume f0: nat→nat
assume g: nat→nat
suppose H2: ∀m:nat.(le (f0 m) (g m))
suppose H3: lt (weight_map f0 (lift (S i) O v)) (g i)
(h1)
by (H1 . . H2 H3)
le (weight_map f0 u2) (weight_map g u1)
end of h1
(h2)
by (weight_le . . . H2)
le (weight_map f0 t0) (weight_map g t0)
end of h2
by (le_plus_plus . . . . h1 h2)
we proved
le
plus (weight_map f0 u2) (weight_map f0 t0)
plus (weight_map g u1) (weight_map g t0)
by (le_n_S . . previous)
we proved
le
S (plus (weight_map f0 u2) (weight_map f0 t0))
S (plus (weight_map g u1) (weight_map g t0))
that is equivalent to
le
weight_map f0 (THead (Flat __5) u2 t0)
weight_map g (THead (Flat __5) u1 t0)
∀f0:nat→nat
.∀g:nat→nat
.∀H2:∀m:nat.(le (f0 m) (g m))
.∀H3:lt (weight_map f0 (lift (S i) O v)) (g i)
.le
S (plus (weight_map f0 u2) (weight_map f0 t0))
S (plus (weight_map g u1) (weight_map g t0))
∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→le (weight_map f (THead k u2 t0)) (weight_map g (THead k u1 t0)))
case subst0_snd ⇒
we need to prove
∀k:K
.∀v:T
.∀t2:T
.∀t1:T
.∀i:nat
.subst0 (s k i) v t1 t2
→(∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S (s k i)) O v)) (g (s k i))
→le (weight_map f t2) (weight_map g t1))
→∀u0:T
.∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→le (weight_map f (THead k u0 t2)) (weight_map g (THead k u0 t1))))
assume k: K
we proceed by induction on k to prove
∀v:T
.∀t2:T
.∀t1:T
.∀i:nat
.subst0 (s k i) v t1 t2
→(∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S (s k i)) O v)) (g (s k i))
→le (weight_map f t2) (weight_map g t1))
→∀u0:T
.∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→le (weight_map f (THead k u0 t2)) (weight_map g (THead k u0 t1))))
case Bind : b:B ⇒
the thesis becomes
∀v:T
.∀t2:T
.∀t1:T
.∀i:nat
.subst0 (s (Bind b) i) v t1 t2
→(∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→((lt
weight_map f (lift (S (s (Bind b) i)) O v)
g (s (Bind b) i))
→le (weight_map f t2) (weight_map g t1))
→∀u0:T
.∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind b) u0 t2)
weight_map g (THead (Bind b) u0 t1))))
we proceed by induction on b to prove
∀v:T
.∀t2:T
.∀t1:T
.∀i:nat
.subst0 (s (Bind b) i) v t1 t2
→(∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→((lt
weight_map f (lift (S (s (Bind b) i)) O v)
g (s (Bind b) i))
→le (weight_map f t2) (weight_map g t1))
→∀u0:T
.∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind b) u0 t2)
weight_map g (THead (Bind b) u0 t1))))
case Abbr : ⇒
the thesis becomes
∀v:T
.∀t2:T
.∀t1:T
.∀i:nat
.subst0 (s (Bind Abbr) i) v t1 t2
→(∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→((lt
weight_map f (lift (S (s (Bind Abbr) i)) O v)
g (s (Bind Abbr) i))
→le (weight_map f t2) (weight_map g t1))
→∀u0:T
.∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind Abbr) u0 t2)
weight_map g (THead (Bind Abbr) u0 t1))))
assume v: T
assume t2: T
assume t1: T
assume i: nat
we must prove
subst0 (s (Bind Abbr) i) v t1 t2
→(∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→((lt
weight_map f (lift (S (s (Bind Abbr) i)) O v)
g (s (Bind Abbr) i))
→le (weight_map f t2) (weight_map g t1))
→∀u0:T
.∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind Abbr) u0 t2)
weight_map g (THead (Bind Abbr) u0 t1))))
or equivalently
subst0 (S i) v t1 t2
→(∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→((lt
weight_map f (lift (S (s (Bind Abbr) i)) O v)
g (s (Bind Abbr) i))
→le (weight_map f t2) (weight_map g t1))
→∀u0:T
.∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind Abbr) u0 t2)
weight_map g (THead (Bind Abbr) u0 t1))))
suppose : subst0 (S i) v t1 t2
we must prove
∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→((lt
weight_map f (lift (S (s (Bind Abbr) i)) O v)
g (s (Bind Abbr) i))
→le (weight_map f t2) (weight_map g t1))
→∀u0:T
.∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind Abbr) u0 t2)
weight_map g (THead (Bind Abbr) u0 t1)))
or equivalently
∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S (S i)) O v)) (g (S i))
→le (weight_map f t2) (weight_map g t1))
→∀u0:T
.∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind Abbr) u0 t2)
weight_map g (THead (Bind Abbr) u0 t1)))
suppose H1:
∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S (S i)) O v)) (g (S i))
→le (weight_map f t2) (weight_map g t1))
assume u0: T
assume f: nat→nat
assume g: nat→nat
suppose H2: ∀m:nat.(le (f m) (g m))
suppose H3: lt (weight_map f (lift (S i) O v)) (g i)
(h1)
by (weight_le . . . H2)
le (weight_map f u0) (weight_map g u0)
end of h1
(h2)
(h1)
assume m: nat
by (weight_le . . . H2)
we proved le (weight_map f u0) (weight_map g u0)
by (le_n_S . . previous)
we proved le (S (weight_map f u0)) (S (weight_map g u0))
by (wadd_le . . H2 . . previous .)
we proved
le
wadd f (S (weight_map f u0)) m
wadd g (S (weight_map g u0)) m
∀m:nat
.le
wadd f (S (weight_map f u0)) m
wadd g (S (weight_map g u0)) m
end of h1
(h2)
by (lift_weight_add_O . . . .)
we proved
eq
nat
weight_map f (lift (S i) O v)
weight_map
wadd f (S (weight_map f u0))
lift (S (S i)) O v
we proceed by induction on the previous result to prove
lt
weight_map
wadd f (S (weight_map f u0))
lift (S (S i)) O v
g i
case refl_equal : ⇒
the thesis becomes the hypothesis H3
we proved
lt
weight_map
wadd f (S (weight_map f u0))
lift (S (S i)) O v
g i
lt
weight_map
wadd f (S (weight_map f u0))
lift (S (S i)) O v
wadd g (S (weight_map g u0)) (S i)
end of h2
by (H1 . . h1 h2)
le
weight_map (wadd f (S (weight_map f u0))) t2
weight_map (wadd g (S (weight_map g u0))) t1
end of h2
by (le_plus_plus . . . . h1 h2)
we proved
le
plus
weight_map f u0
weight_map (wadd f (S (weight_map f u0))) t2
plus
weight_map g u0
weight_map (wadd g (S (weight_map g u0))) t1
by (le_n_S . . previous)
we proved
le
S
plus
weight_map f u0
weight_map (wadd f (S (weight_map f u0))) t2
S
plus
weight_map g u0
weight_map (wadd g (S (weight_map g u0))) t1
that is equivalent to
le
weight_map f (THead (Bind Abbr) u0 t2)
weight_map g (THead (Bind Abbr) u0 t1)
we proved
∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S (S i)) O v)) (g (S i))
→le (weight_map f t2) (weight_map g t1))
→∀u0:T
.∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind Abbr) u0 t2)
weight_map g (THead (Bind Abbr) u0 t1)))
that is equivalent to
∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→((lt
weight_map f (lift (S (s (Bind Abbr) i)) O v)
g (s (Bind Abbr) i))
→le (weight_map f t2) (weight_map g t1))
→∀u0:T
.∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind Abbr) u0 t2)
weight_map g (THead (Bind Abbr) u0 t1)))
we proved
subst0 (S i) v t1 t2
→(∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→((lt
weight_map f (lift (S (s (Bind Abbr) i)) O v)
g (s (Bind Abbr) i))
→le (weight_map f t2) (weight_map g t1))
→∀u0:T
.∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind Abbr) u0 t2)
weight_map g (THead (Bind Abbr) u0 t1))))
that is equivalent to
subst0 (s (Bind Abbr) i) v t1 t2
→(∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→((lt
weight_map f (lift (S (s (Bind Abbr) i)) O v)
g (s (Bind Abbr) i))
→le (weight_map f t2) (weight_map g t1))
→∀u0:T
.∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind Abbr) u0 t2)
weight_map g (THead (Bind Abbr) u0 t1))))
∀v:T
.∀t2:T
.∀t1:T
.∀i:nat
.subst0 (s (Bind Abbr) i) v t1 t2
→(∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→((lt
weight_map f (lift (S (s (Bind Abbr) i)) O v)
g (s (Bind Abbr) i))
→le (weight_map f t2) (weight_map g t1))
→∀u0:T
.∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind Abbr) u0 t2)
weight_map g (THead (Bind Abbr) u0 t1))))
case Abst : ⇒
the thesis becomes
∀v:T
.∀t2:T
.∀t1:T
.∀i:nat
.subst0 (s (Bind Abst) i) v t1 t2
→(∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→((lt
weight_map f (lift (S (s (Bind Abst) i)) O v)
g (s (Bind Abst) i))
→le (weight_map f t2) (weight_map g t1))
→∀u0:T
.∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind Abst) u0 t2)
weight_map g (THead (Bind Abst) u0 t1))))
assume v: T
assume t2: T
assume t1: T
assume i: nat
we must prove
subst0 (s (Bind Abst) i) v t1 t2
→(∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→((lt
weight_map f (lift (S (s (Bind Abst) i)) O v)
g (s (Bind Abst) i))
→le (weight_map f t2) (weight_map g t1))
→∀u0:T
.∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind Abst) u0 t2)
weight_map g (THead (Bind Abst) u0 t1))))
or equivalently
subst0 (S i) v t1 t2
→(∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→((lt
weight_map f (lift (S (s (Bind Abst) i)) O v)
g (s (Bind Abst) i))
→le (weight_map f t2) (weight_map g t1))
→∀u0:T
.∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind Abst) u0 t2)
weight_map g (THead (Bind Abst) u0 t1))))
suppose : subst0 (S i) v t1 t2
we must prove
∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→((lt
weight_map f (lift (S (s (Bind Abst) i)) O v)
g (s (Bind Abst) i))
→le (weight_map f t2) (weight_map g t1))
→∀u0:T
.∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind Abst) u0 t2)
weight_map g (THead (Bind Abst) u0 t1)))
or equivalently
∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S (S i)) O v)) (g (S i))
→le (weight_map f t2) (weight_map g t1))
→∀u0:T
.∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind Abst) u0 t2)
weight_map g (THead (Bind Abst) u0 t1)))
suppose H1:
∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S (S i)) O v)) (g (S i))
→le (weight_map f t2) (weight_map g t1))
assume u0: T
assume f: nat→nat
assume g: nat→nat
suppose H2: ∀m:nat.(le (f m) (g m))
suppose H3: lt (weight_map f (lift (S i) O v)) (g i)
(h1)
by (weight_le . . . H2)
le (weight_map f u0) (weight_map g u0)
end of h1
(h2)
(h1)
assume m: nat
by (le_n .)
we proved le O O
by (wadd_le . . H2 . . previous .)
we proved le (wadd f O m) (wadd g O m)
∀m:nat.(le (wadd f O m) (wadd g O m))
end of h1
(h2)
by (lift_weight_add_O . . . .)
we proved
eq
nat
weight_map f (lift (S i) O v)
weight_map (wadd f O) (lift (S (S i)) O v)
we proceed by induction on the previous result to prove lt (weight_map (wadd f O) (lift (S (S i)) O v)) (g i)
case refl_equal : ⇒
the thesis becomes the hypothesis H3
we proved lt (weight_map (wadd f O) (lift (S (S i)) O v)) (g i)
lt
weight_map (wadd f O) (lift (S (S i)) O v)
wadd g O (S i)
end of h2
by (H1 . . h1 h2)
le (weight_map (wadd f O) t2) (weight_map (wadd g O) t1)
end of h2
by (le_plus_plus . . . . h1 h2)
we proved
le
plus (weight_map f u0) (weight_map (wadd f O) t2)
plus (weight_map g u0) (weight_map (wadd g O) t1)
by (le_n_S . . previous)
we proved
le
S (plus (weight_map f u0) (weight_map (wadd f O) t2))
S (plus (weight_map g u0) (weight_map (wadd g O) t1))
that is equivalent to
le
weight_map f (THead (Bind Abst) u0 t2)
weight_map g (THead (Bind Abst) u0 t1)
we proved
∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S (S i)) O v)) (g (S i))
→le (weight_map f t2) (weight_map g t1))
→∀u0:T
.∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind Abst) u0 t2)
weight_map g (THead (Bind Abst) u0 t1)))
that is equivalent to
∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→((lt
weight_map f (lift (S (s (Bind Abst) i)) O v)
g (s (Bind Abst) i))
→le (weight_map f t2) (weight_map g t1))
→∀u0:T
.∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind Abst) u0 t2)
weight_map g (THead (Bind Abst) u0 t1)))
we proved
subst0 (S i) v t1 t2
→(∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→((lt
weight_map f (lift (S (s (Bind Abst) i)) O v)
g (s (Bind Abst) i))
→le (weight_map f t2) (weight_map g t1))
→∀u0:T
.∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind Abst) u0 t2)
weight_map g (THead (Bind Abst) u0 t1))))
that is equivalent to
subst0 (s (Bind Abst) i) v t1 t2
→(∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→((lt
weight_map f (lift (S (s (Bind Abst) i)) O v)
g (s (Bind Abst) i))
→le (weight_map f t2) (weight_map g t1))
→∀u0:T
.∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind Abst) u0 t2)
weight_map g (THead (Bind Abst) u0 t1))))
∀v:T
.∀t2:T
.∀t1:T
.∀i:nat
.subst0 (s (Bind Abst) i) v t1 t2
→(∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→((lt
weight_map f (lift (S (s (Bind Abst) i)) O v)
g (s (Bind Abst) i))
→le (weight_map f t2) (weight_map g t1))
→∀u0:T
.∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind Abst) u0 t2)
weight_map g (THead (Bind Abst) u0 t1))))
case Void : ⇒
the thesis becomes
∀v:T
.∀t2:T
.∀t1:T
.∀i:nat
.subst0 (s (Bind Void) i) v t1 t2
→(∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→((lt
weight_map f (lift (S (s (Bind Void) i)) O v)
g (s (Bind Void) i))
→le (weight_map f t2) (weight_map g t1))
→∀u0:T
.∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind Void) u0 t2)
weight_map g (THead (Bind Void) u0 t1))))
assume v: T
assume t2: T
assume t1: T
assume i: nat
we must prove
subst0 (s (Bind Void) i) v t1 t2
→(∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→((lt
weight_map f (lift (S (s (Bind Void) i)) O v)
g (s (Bind Void) i))
→le (weight_map f t2) (weight_map g t1))
→∀u0:T
.∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind Void) u0 t2)
weight_map g (THead (Bind Void) u0 t1))))
or equivalently
subst0 (S i) v t1 t2
→(∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→((lt
weight_map f (lift (S (s (Bind Void) i)) O v)
g (s (Bind Void) i))
→le (weight_map f t2) (weight_map g t1))
→∀u0:T
.∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind Void) u0 t2)
weight_map g (THead (Bind Void) u0 t1))))
suppose : subst0 (S i) v t1 t2
we must prove
∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→((lt
weight_map f (lift (S (s (Bind Void) i)) O v)
g (s (Bind Void) i))
→le (weight_map f t2) (weight_map g t1))
→∀u0:T
.∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind Void) u0 t2)
weight_map g (THead (Bind Void) u0 t1)))
or equivalently
∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S (S i)) O v)) (g (S i))
→le (weight_map f t2) (weight_map g t1))
→∀u0:T
.∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind Void) u0 t2)
weight_map g (THead (Bind Void) u0 t1)))
suppose H1:
∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S (S i)) O v)) (g (S i))
→le (weight_map f t2) (weight_map g t1))
assume u0: T
assume f: nat→nat
assume g: nat→nat
suppose H2: ∀m:nat.(le (f m) (g m))
suppose H3: lt (weight_map f (lift (S i) O v)) (g i)
(h1)
by (weight_le . . . H2)
le (weight_map f u0) (weight_map g u0)
end of h1
(h2)
(h1)
assume m: nat
by (le_n .)
we proved le O O
by (wadd_le . . H2 . . previous .)
we proved le (wadd f O m) (wadd g O m)
∀m:nat.(le (wadd f O m) (wadd g O m))
end of h1
(h2)
by (lift_weight_add_O . . . .)
we proved
eq
nat
weight_map f (lift (S i) O v)
weight_map (wadd f O) (lift (S (S i)) O v)
we proceed by induction on the previous result to prove lt (weight_map (wadd f O) (lift (S (S i)) O v)) (g i)
case refl_equal : ⇒
the thesis becomes the hypothesis H3
we proved lt (weight_map (wadd f O) (lift (S (S i)) O v)) (g i)
lt
weight_map (wadd f O) (lift (S (S i)) O v)
wadd g O (S i)
end of h2
by (H1 . . h1 h2)
le (weight_map (wadd f O) t2) (weight_map (wadd g O) t1)
end of h2
by (le_plus_plus . . . . h1 h2)
we proved
le
plus (weight_map f u0) (weight_map (wadd f O) t2)
plus (weight_map g u0) (weight_map (wadd g O) t1)
by (le_n_S . . previous)
we proved
le
S (plus (weight_map f u0) (weight_map (wadd f O) t2))
S (plus (weight_map g u0) (weight_map (wadd g O) t1))
that is equivalent to
le
weight_map f (THead (Bind Void) u0 t2)
weight_map g (THead (Bind Void) u0 t1)
we proved
∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S (S i)) O v)) (g (S i))
→le (weight_map f t2) (weight_map g t1))
→∀u0:T
.∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind Void) u0 t2)
weight_map g (THead (Bind Void) u0 t1)))
that is equivalent to
∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→((lt
weight_map f (lift (S (s (Bind Void) i)) O v)
g (s (Bind Void) i))
→le (weight_map f t2) (weight_map g t1))
→∀u0:T
.∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind Void) u0 t2)
weight_map g (THead (Bind Void) u0 t1)))
we proved
subst0 (S i) v t1 t2
→(∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→((lt
weight_map f (lift (S (s (Bind Void) i)) O v)
g (s (Bind Void) i))
→le (weight_map f t2) (weight_map g t1))
→∀u0:T
.∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind Void) u0 t2)
weight_map g (THead (Bind Void) u0 t1))))
that is equivalent to
subst0 (s (Bind Void) i) v t1 t2
→(∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→((lt
weight_map f (lift (S (s (Bind Void) i)) O v)
g (s (Bind Void) i))
→le (weight_map f t2) (weight_map g t1))
→∀u0:T
.∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind Void) u0 t2)
weight_map g (THead (Bind Void) u0 t1))))
∀v:T
.∀t2:T
.∀t1:T
.∀i:nat
.subst0 (s (Bind Void) i) v t1 t2
→(∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→((lt
weight_map f (lift (S (s (Bind Void) i)) O v)
g (s (Bind Void) i))
→le (weight_map f t2) (weight_map g t1))
→∀u0:T
.∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind Void) u0 t2)
weight_map g (THead (Bind Void) u0 t1))))
∀v:T
.∀t2:T
.∀t1:T
.∀i:nat
.subst0 (s (Bind b) i) v t1 t2
→(∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→((lt
weight_map f (lift (S (s (Bind b) i)) O v)
g (s (Bind b) i))
→le (weight_map f t2) (weight_map g t1))
→∀u0:T
.∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind b) u0 t2)
weight_map g (THead (Bind b) u0 t1))))
case Flat : :F ⇒
the thesis becomes
∀v:T
.∀t2:T
.∀t1:T
.∀i:nat
.subst0 (s (Flat __5) i) v t1 t2
→(∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→((lt
weight_map f (lift (S (s (Flat __9) i)) O v)
g (s (Flat __9) i))
→le (weight_map f t2) (weight_map g t1))
→∀u0:T
.∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Flat __12) u0 t2)
weight_map g (THead (Flat __12) u0 t1))))
assume v: T
assume t2: T
assume t1: T
assume i: nat
we must prove
subst0 (s (Flat __5) i) v t1 t2
→(∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→((lt
weight_map f (lift (S (s (Flat __9) i)) O v)
g (s (Flat __9) i))
→le (weight_map f t2) (weight_map g t1))
→∀u0:T
.∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Flat __12) u0 t2)
weight_map g (THead (Flat __12) u0 t1))))
or equivalently
subst0 i v t1 t2
→(∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→((lt
weight_map f (lift (S (s (Flat __9) i)) O v)
g (s (Flat __9) i))
→le (weight_map f t2) (weight_map g t1))
→∀u0:T
.∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Flat __12) u0 t2)
weight_map g (THead (Flat __12) u0 t1))))
suppose : subst0 i v t1 t2
we must prove
∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→((lt
weight_map f (lift (S (s (Flat __9) i)) O v)
g (s (Flat __9) i))
→le (weight_map f t2) (weight_map g t1))
→∀u0:T
.∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Flat __12) u0 t2)
weight_map g (THead (Flat __12) u0 t1)))
or equivalently
∀f0:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f0 m) (g m))
→(lt (weight_map f0 (lift (S i) O v)) (g i)
→le (weight_map f0 t2) (weight_map g t1))
→∀u0:T
.∀f0:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f0 m) (g m))
→(lt (weight_map f0 (lift (S i) O v)) (g i)
→(le
weight_map f0 (THead (Flat __12) u0 t2)
weight_map g (THead (Flat __12) u0 t1)))
suppose H1:
∀f0:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f0 m) (g m))
→(lt (weight_map f0 (lift (S i) O v)) (g i)
→le (weight_map f0 t2) (weight_map g t1))
assume u0: T
assume f0: nat→nat
assume g: nat→nat
suppose H2: ∀m:nat.(le (f0 m) (g m))
suppose H3: lt (weight_map f0 (lift (S i) O v)) (g i)
(h1)
by (weight_le . . . H2)
le (weight_map f0 u0) (weight_map g u0)
end of h1
(h2)
by (H1 . . H2 H3)
le (weight_map f0 t2) (weight_map g t1)
end of h2
by (le_plus_plus . . . . h1 h2)
we proved
le
plus (weight_map f0 u0) (weight_map f0 t2)
plus (weight_map g u0) (weight_map g t1)
by (le_n_S . . previous)
we proved
le
S (plus (weight_map f0 u0) (weight_map f0 t2))
S (plus (weight_map g u0) (weight_map g t1))
that is equivalent to
le
weight_map f0 (THead (Flat __12) u0 t2)
weight_map g (THead (Flat __12) u0 t1)
we proved
∀f0:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f0 m) (g m))
→(lt (weight_map f0 (lift (S i) O v)) (g i)
→le (weight_map f0 t2) (weight_map g t1))
→∀u0:T
.∀f0:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f0 m) (g m))
→(lt (weight_map f0 (lift (S i) O v)) (g i)
→(le
weight_map f0 (THead (Flat __12) u0 t2)
weight_map g (THead (Flat __12) u0 t1)))
that is equivalent to
∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→((lt
weight_map f (lift (S (s (Flat __9) i)) O v)
g (s (Flat __9) i))
→le (weight_map f t2) (weight_map g t1))
→∀u0:T
.∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Flat __12) u0 t2)
weight_map g (THead (Flat __12) u0 t1)))
we proved
subst0 i v t1 t2
→(∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→((lt
weight_map f (lift (S (s (Flat __9) i)) O v)
g (s (Flat __9) i))
→le (weight_map f t2) (weight_map g t1))
→∀u0:T
.∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Flat __12) u0 t2)
weight_map g (THead (Flat __12) u0 t1))))
that is equivalent to
subst0 (s (Flat __5) i) v t1 t2
→(∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→((lt
weight_map f (lift (S (s (Flat __9) i)) O v)
g (s (Flat __9) i))
→le (weight_map f t2) (weight_map g t1))
→∀u0:T
.∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Flat __12) u0 t2)
weight_map g (THead (Flat __12) u0 t1))))
∀v:T
.∀t2:T
.∀t1:T
.∀i:nat
.subst0 (s (Flat __5) i) v t1 t2
→(∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→((lt
weight_map f (lift (S (s (Flat __9) i)) O v)
g (s (Flat __9) i))
→le (weight_map f t2) (weight_map g t1))
→∀u0:T
.∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Flat __12) u0 t2)
weight_map g (THead (Flat __12) u0 t1))))
we proved
∀v:T
.∀t2:T
.∀t1:T
.∀i:nat
.subst0 (s k i) v t1 t2
→(∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S (s k i)) O v)) (g (s k i))
→le (weight_map f t2) (weight_map g t1))
→∀u0:T
.∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→le (weight_map f (THead k u0 t2)) (weight_map g (THead k u0 t1))))
∀k:K
.∀v:T
.∀t2:T
.∀t1:T
.∀i:nat
.subst0 (s k i) v t1 t2
→(∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S (s k i)) O v)) (g (s k i))
→le (weight_map f t2) (weight_map g t1))
→∀u0:T
.∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→le (weight_map f (THead k u0 t2)) (weight_map g (THead k u0 t1))))
case subst0_both ⇒
we need to prove
∀v:T
.∀u1:T
.∀u2:T
.∀i:nat
.subst0 i v u1 u2
→(∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→le (weight_map f u2) (weight_map g u1))
→∀k:K
.∀t1:T
.∀t2:T
.subst0 (s k i) v t1 t2
→(∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S (s k i)) O v)) (g (s k i))
→le (weight_map f t2) (weight_map g t1))
→∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→le (weight_map f (THead k u2 t2)) (weight_map g (THead k u1 t1)))))
assume v: T
assume u1: T
assume u2: T
assume i: nat
suppose : subst0 i v u1 u2
suppose H1:
∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→le (weight_map f u2) (weight_map g u1))
assume k: K
we proceed by induction on k to prove
∀t1:T
.∀t2:T
.subst0 (s k i) v t1 t2
→(∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S (s k i)) O v)) (g (s k i))
→le (weight_map f t2) (weight_map g t1))
→∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→le (weight_map f (THead k u2 t2)) (weight_map g (THead k u1 t1))))
case Bind : b:B ⇒
the thesis becomes
∀t1:T
.∀t2:T
.subst0 (s (Bind b) i) v t1 t2
→(∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→((lt
weight_map f (lift (S (s (Bind b) i)) O v)
g (s (Bind b) i))
→le (weight_map f t2) (weight_map g t1))
→∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind b) u2 t2)
weight_map g (THead (Bind b) u1 t1))))
we proceed by induction on b to prove
∀t1:T
.∀t2:T
.subst0 (s (Bind b) i) v t1 t2
→(∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→((lt
weight_map f (lift (S (s (Bind b) i)) O v)
g (s (Bind b) i))
→le (weight_map f t2) (weight_map g t1))
→∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind b) u2 t2)
weight_map g (THead (Bind b) u1 t1))))
case Abbr : ⇒
the thesis becomes
∀t1:T
.∀t2:T
.subst0 (s (Bind Abbr) i) v t1 t2
→(∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→((lt
weight_map f (lift (S (s (Bind Abbr) i)) O v)
g (s (Bind Abbr) i))
→le (weight_map f t2) (weight_map g t1))
→∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind Abbr) u2 t2)
weight_map g (THead (Bind Abbr) u1 t1))))
assume t1: T
assume t2: T
we must prove
subst0 (s (Bind Abbr) i) v t1 t2
→(∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→((lt
weight_map f (lift (S (s (Bind Abbr) i)) O v)
g (s (Bind Abbr) i))
→le (weight_map f t2) (weight_map g t1))
→∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind Abbr) u2 t2)
weight_map g (THead (Bind Abbr) u1 t1))))
or equivalently
subst0 (S i) v t1 t2
→(∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→((lt
weight_map f (lift (S (s (Bind Abbr) i)) O v)
g (s (Bind Abbr) i))
→le (weight_map f t2) (weight_map g t1))
→∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind Abbr) u2 t2)
weight_map g (THead (Bind Abbr) u1 t1))))
suppose : subst0 (S i) v t1 t2
we must prove
∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→((lt
weight_map f (lift (S (s (Bind Abbr) i)) O v)
g (s (Bind Abbr) i))
→le (weight_map f t2) (weight_map g t1))
→∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind Abbr) u2 t2)
weight_map g (THead (Bind Abbr) u1 t1)))
or equivalently
∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S (S i)) O v)) (g (S i))
→le (weight_map f t2) (weight_map g t1))
→∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind Abbr) u2 t2)
weight_map g (THead (Bind Abbr) u1 t1)))
suppose H3:
∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S (S i)) O v)) (g (S i))
→le (weight_map f t2) (weight_map g t1))
assume f: nat→nat
assume g: nat→nat
suppose H4: ∀m:nat.(le (f m) (g m))
suppose H5: lt (weight_map f (lift (S i) O v)) (g i)
(h1)
by (H1 . . H4 H5)
le (weight_map f u2) (weight_map g u1)
end of h1
(h2)
(h1)
assume m: nat
by (H1 . . H4 H5)
we proved le (weight_map f u2) (weight_map g u1)
by (le_n_S . . previous)
we proved le (S (weight_map f u2)) (S (weight_map g u1))
by (wadd_le . . H4 . . previous .)
we proved
le
wadd f (S (weight_map f u2)) m
wadd g (S (weight_map g u1)) m
∀m:nat
.le
wadd f (S (weight_map f u2)) m
wadd g (S (weight_map g u1)) m
end of h1
(h2)
by (lift_weight_add_O . . . .)
we proved
eq
nat
weight_map f (lift (S i) O v)
weight_map
wadd f (S (weight_map f u2))
lift (S (S i)) O v
we proceed by induction on the previous result to prove
lt
weight_map
wadd f (S (weight_map f u2))
lift (S (S i)) O v
g i
case refl_equal : ⇒
the thesis becomes the hypothesis H5
we proved
lt
weight_map
wadd f (S (weight_map f u2))
lift (S (S i)) O v
g i
lt
weight_map
wadd f (S (weight_map f u2))
lift (S (S i)) O v
wadd g (S (weight_map g u1)) (S i)
end of h2
by (H3 . . h1 h2)
le
weight_map (wadd f (S (weight_map f u2))) t2
weight_map (wadd g (S (weight_map g u1))) t1
end of h2
by (le_plus_plus . . . . h1 h2)
we proved
le
plus
weight_map f u2
weight_map (wadd f (S (weight_map f u2))) t2
plus
weight_map g u1
weight_map (wadd g (S (weight_map g u1))) t1
by (le_n_S . . previous)
we proved
le
S
plus
weight_map f u2
weight_map (wadd f (S (weight_map f u2))) t2
S
plus
weight_map g u1
weight_map (wadd g (S (weight_map g u1))) t1
that is equivalent to
le
weight_map f (THead (Bind Abbr) u2 t2)
weight_map g (THead (Bind Abbr) u1 t1)
we proved
∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S (S i)) O v)) (g (S i))
→le (weight_map f t2) (weight_map g t1))
→∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind Abbr) u2 t2)
weight_map g (THead (Bind Abbr) u1 t1)))
that is equivalent to
∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→((lt
weight_map f (lift (S (s (Bind Abbr) i)) O v)
g (s (Bind Abbr) i))
→le (weight_map f t2) (weight_map g t1))
→∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind Abbr) u2 t2)
weight_map g (THead (Bind Abbr) u1 t1)))
we proved
subst0 (S i) v t1 t2
→(∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→((lt
weight_map f (lift (S (s (Bind Abbr) i)) O v)
g (s (Bind Abbr) i))
→le (weight_map f t2) (weight_map g t1))
→∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind Abbr) u2 t2)
weight_map g (THead (Bind Abbr) u1 t1))))
that is equivalent to
subst0 (s (Bind Abbr) i) v t1 t2
→(∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→((lt
weight_map f (lift (S (s (Bind Abbr) i)) O v)
g (s (Bind Abbr) i))
→le (weight_map f t2) (weight_map g t1))
→∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind Abbr) u2 t2)
weight_map g (THead (Bind Abbr) u1 t1))))
∀t1:T
.∀t2:T
.subst0 (s (Bind Abbr) i) v t1 t2
→(∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→((lt
weight_map f (lift (S (s (Bind Abbr) i)) O v)
g (s (Bind Abbr) i))
→le (weight_map f t2) (weight_map g t1))
→∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind Abbr) u2 t2)
weight_map g (THead (Bind Abbr) u1 t1))))
case Abst : ⇒
the thesis becomes
∀t1:T
.∀t2:T
.subst0 (s (Bind Abst) i) v t1 t2
→(∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→((lt
weight_map f (lift (S (s (Bind Abst) i)) O v)
g (s (Bind Abst) i))
→le (weight_map f t2) (weight_map g t1))
→∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind Abst) u2 t2)
weight_map g (THead (Bind Abst) u1 t1))))
assume t1: T
assume t2: T
we must prove
subst0 (s (Bind Abst) i) v t1 t2
→(∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→((lt
weight_map f (lift (S (s (Bind Abst) i)) O v)
g (s (Bind Abst) i))
→le (weight_map f t2) (weight_map g t1))
→∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind Abst) u2 t2)
weight_map g (THead (Bind Abst) u1 t1))))
or equivalently
subst0 (S i) v t1 t2
→(∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→((lt
weight_map f (lift (S (s (Bind Abst) i)) O v)
g (s (Bind Abst) i))
→le (weight_map f t2) (weight_map g t1))
→∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind Abst) u2 t2)
weight_map g (THead (Bind Abst) u1 t1))))
suppose : subst0 (S i) v t1 t2
we must prove
∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→((lt
weight_map f (lift (S (s (Bind Abst) i)) O v)
g (s (Bind Abst) i))
→le (weight_map f t2) (weight_map g t1))
→∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind Abst) u2 t2)
weight_map g (THead (Bind Abst) u1 t1)))
or equivalently
∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S (S i)) O v)) (g (S i))
→le (weight_map f t2) (weight_map g t1))
→∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind Abst) u2 t2)
weight_map g (THead (Bind Abst) u1 t1)))
suppose H3:
∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S (S i)) O v)) (g (S i))
→le (weight_map f t2) (weight_map g t1))
assume f: nat→nat
assume g: nat→nat
suppose H4: ∀m:nat.(le (f m) (g m))
suppose H5: lt (weight_map f (lift (S i) O v)) (g i)
(h1)
by (H1 . . H4 H5)
le (weight_map f u2) (weight_map g u1)
end of h1
(h2)
(h1)
assume m: nat
by (le_n .)
we proved le O O
by (wadd_le . . H4 . . previous .)
we proved le (wadd f O m) (wadd g O m)
∀m:nat.(le (wadd f O m) (wadd g O m))
end of h1
(h2)
by (lift_weight_add_O . . . .)
we proved
eq
nat
weight_map f (lift (S i) O v)
weight_map (wadd f O) (lift (S (S i)) O v)
we proceed by induction on the previous result to prove lt (weight_map (wadd f O) (lift (S (S i)) O v)) (g i)
case refl_equal : ⇒
the thesis becomes the hypothesis H5
we proved lt (weight_map (wadd f O) (lift (S (S i)) O v)) (g i)
lt
weight_map (wadd f O) (lift (S (S i)) O v)
wadd g O (S i)
end of h2
by (H3 . . h1 h2)
le (weight_map (wadd f O) t2) (weight_map (wadd g O) t1)
end of h2
by (le_plus_plus . . . . h1 h2)
we proved
le
plus (weight_map f u2) (weight_map (wadd f O) t2)
plus (weight_map g u1) (weight_map (wadd g O) t1)
by (le_n_S . . previous)
we proved
le
S (plus (weight_map f u2) (weight_map (wadd f O) t2))
S (plus (weight_map g u1) (weight_map (wadd g O) t1))
that is equivalent to
le
weight_map f (THead (Bind Abst) u2 t2)
weight_map g (THead (Bind Abst) u1 t1)
we proved
∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S (S i)) O v)) (g (S i))
→le (weight_map f t2) (weight_map g t1))
→∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind Abst) u2 t2)
weight_map g (THead (Bind Abst) u1 t1)))
that is equivalent to
∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→((lt
weight_map f (lift (S (s (Bind Abst) i)) O v)
g (s (Bind Abst) i))
→le (weight_map f t2) (weight_map g t1))
→∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind Abst) u2 t2)
weight_map g (THead (Bind Abst) u1 t1)))
we proved
subst0 (S i) v t1 t2
→(∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→((lt
weight_map f (lift (S (s (Bind Abst) i)) O v)
g (s (Bind Abst) i))
→le (weight_map f t2) (weight_map g t1))
→∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind Abst) u2 t2)
weight_map g (THead (Bind Abst) u1 t1))))
that is equivalent to
subst0 (s (Bind Abst) i) v t1 t2
→(∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→((lt
weight_map f (lift (S (s (Bind Abst) i)) O v)
g (s (Bind Abst) i))
→le (weight_map f t2) (weight_map g t1))
→∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind Abst) u2 t2)
weight_map g (THead (Bind Abst) u1 t1))))
∀t1:T
.∀t2:T
.subst0 (s (Bind Abst) i) v t1 t2
→(∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→((lt
weight_map f (lift (S (s (Bind Abst) i)) O v)
g (s (Bind Abst) i))
→le (weight_map f t2) (weight_map g t1))
→∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind Abst) u2 t2)
weight_map g (THead (Bind Abst) u1 t1))))
case Void : ⇒
the thesis becomes
∀t1:T
.∀t2:T
.subst0 (s (Bind Void) i) v t1 t2
→(∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→((lt
weight_map f (lift (S (s (Bind Void) i)) O v)
g (s (Bind Void) i))
→le (weight_map f t2) (weight_map g t1))
→∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind Void) u2 t2)
weight_map g (THead (Bind Void) u1 t1))))
assume t1: T
assume t2: T
we must prove
subst0 (s (Bind Void) i) v t1 t2
→(∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→((lt
weight_map f (lift (S (s (Bind Void) i)) O v)
g (s (Bind Void) i))
→le (weight_map f t2) (weight_map g t1))
→∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind Void) u2 t2)
weight_map g (THead (Bind Void) u1 t1))))
or equivalently
subst0 (S i) v t1 t2
→(∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→((lt
weight_map f (lift (S (s (Bind Void) i)) O v)
g (s (Bind Void) i))
→le (weight_map f t2) (weight_map g t1))
→∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind Void) u2 t2)
weight_map g (THead (Bind Void) u1 t1))))
suppose : subst0 (S i) v t1 t2
we must prove
∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→((lt
weight_map f (lift (S (s (Bind Void) i)) O v)
g (s (Bind Void) i))
→le (weight_map f t2) (weight_map g t1))
→∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind Void) u2 t2)
weight_map g (THead (Bind Void) u1 t1)))
or equivalently
∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S (S i)) O v)) (g (S i))
→le (weight_map f t2) (weight_map g t1))
→∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind Void) u2 t2)
weight_map g (THead (Bind Void) u1 t1)))
suppose H3:
∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S (S i)) O v)) (g (S i))
→le (weight_map f t2) (weight_map g t1))
assume f: nat→nat
assume g: nat→nat
suppose H4: ∀m:nat.(le (f m) (g m))
suppose H5: lt (weight_map f (lift (S i) O v)) (g i)
(h1)
by (H1 . . H4 H5)
le (weight_map f u2) (weight_map g u1)
end of h1
(h2)
(h1)
assume m: nat
by (le_n .)
we proved le O O
by (wadd_le . . H4 . . previous .)
we proved le (wadd f O m) (wadd g O m)
∀m:nat.(le (wadd f O m) (wadd g O m))
end of h1
(h2)
by (lift_weight_add_O . . . .)
we proved
eq
nat
weight_map f (lift (S i) O v)
weight_map (wadd f O) (lift (S (S i)) O v)
we proceed by induction on the previous result to prove lt (weight_map (wadd f O) (lift (S (S i)) O v)) (g i)
case refl_equal : ⇒
the thesis becomes the hypothesis H5
we proved lt (weight_map (wadd f O) (lift (S (S i)) O v)) (g i)
lt
weight_map (wadd f O) (lift (S (S i)) O v)
wadd g O (S i)
end of h2
by (H3 . . h1 h2)
le (weight_map (wadd f O) t2) (weight_map (wadd g O) t1)
end of h2
by (le_plus_plus . . . . h1 h2)
we proved
le
plus (weight_map f u2) (weight_map (wadd f O) t2)
plus (weight_map g u1) (weight_map (wadd g O) t1)
by (le_n_S . . previous)
we proved
le
S (plus (weight_map f u2) (weight_map (wadd f O) t2))
S (plus (weight_map g u1) (weight_map (wadd g O) t1))
that is equivalent to
le
weight_map f (THead (Bind Void) u2 t2)
weight_map g (THead (Bind Void) u1 t1)
we proved
∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S (S i)) O v)) (g (S i))
→le (weight_map f t2) (weight_map g t1))
→∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind Void) u2 t2)
weight_map g (THead (Bind Void) u1 t1)))
that is equivalent to
∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→((lt
weight_map f (lift (S (s (Bind Void) i)) O v)
g (s (Bind Void) i))
→le (weight_map f t2) (weight_map g t1))
→∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind Void) u2 t2)
weight_map g (THead (Bind Void) u1 t1)))
we proved
subst0 (S i) v t1 t2
→(∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→((lt
weight_map f (lift (S (s (Bind Void) i)) O v)
g (s (Bind Void) i))
→le (weight_map f t2) (weight_map g t1))
→∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind Void) u2 t2)
weight_map g (THead (Bind Void) u1 t1))))
that is equivalent to
subst0 (s (Bind Void) i) v t1 t2
→(∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→((lt
weight_map f (lift (S (s (Bind Void) i)) O v)
g (s (Bind Void) i))
→le (weight_map f t2) (weight_map g t1))
→∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind Void) u2 t2)
weight_map g (THead (Bind Void) u1 t1))))
∀t1:T
.∀t2:T
.subst0 (s (Bind Void) i) v t1 t2
→(∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→((lt
weight_map f (lift (S (s (Bind Void) i)) O v)
g (s (Bind Void) i))
→le (weight_map f t2) (weight_map g t1))
→∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind Void) u2 t2)
weight_map g (THead (Bind Void) u1 t1))))
∀t1:T
.∀t2:T
.subst0 (s (Bind b) i) v t1 t2
→(∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→((lt
weight_map f (lift (S (s (Bind b) i)) O v)
g (s (Bind b) i))
→le (weight_map f t2) (weight_map g t1))
→∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Bind b) u2 t2)
weight_map g (THead (Bind b) u1 t1))))
case Flat : :F ⇒
the thesis becomes
∀t1:T
.∀t2:T
.subst0 (s (Flat __3) i) v t1 t2
→(∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→((lt
weight_map f (lift (S (s (Flat __7) i)) O v)
g (s (Flat __7) i))
→le (weight_map f t2) (weight_map g t1))
→∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Flat __9) u2 t2)
weight_map g (THead (Flat __9) u1 t1))))
assume t1: T
assume t2: T
we must prove
subst0 (s (Flat __3) i) v t1 t2
→(∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→((lt
weight_map f (lift (S (s (Flat __7) i)) O v)
g (s (Flat __7) i))
→le (weight_map f t2) (weight_map g t1))
→∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Flat __9) u2 t2)
weight_map g (THead (Flat __9) u1 t1))))
or equivalently
subst0 i v t1 t2
→(∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→((lt
weight_map f (lift (S (s (Flat __7) i)) O v)
g (s (Flat __7) i))
→le (weight_map f t2) (weight_map g t1))
→∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Flat __9) u2 t2)
weight_map g (THead (Flat __9) u1 t1))))
suppose : subst0 i v t1 t2
we must prove
∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→((lt
weight_map f (lift (S (s (Flat __7) i)) O v)
g (s (Flat __7) i))
→le (weight_map f t2) (weight_map g t1))
→∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Flat __9) u2 t2)
weight_map g (THead (Flat __9) u1 t1)))
or equivalently
∀f0:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f0 m) (g m))
→(lt (weight_map f0 (lift (S i) O v)) (g i)
→le (weight_map f0 t2) (weight_map g t1))
→∀f0:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f0 m) (g m))
→(lt (weight_map f0 (lift (S i) O v)) (g i)
→(le
weight_map f0 (THead (Flat __9) u2 t2)
weight_map g (THead (Flat __9) u1 t1)))
suppose H3:
∀f0:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f0 m) (g m))
→(lt (weight_map f0 (lift (S i) O v)) (g i)
→le (weight_map f0 t2) (weight_map g t1))
assume f0: nat→nat
assume g: nat→nat
suppose H4: ∀m:nat.(le (f0 m) (g m))
suppose H5: lt (weight_map f0 (lift (S i) O v)) (g i)
(h1)
by (H1 . . H4 H5)
le (weight_map f0 u2) (weight_map g u1)
end of h1
(h2)
by (H3 . . H4 H5)
le (weight_map f0 t2) (weight_map g t1)
end of h2
by (le_plus_plus . . . . h1 h2)
we proved
le
plus (weight_map f0 u2) (weight_map f0 t2)
plus (weight_map g u1) (weight_map g t1)
by (le_n_S . . previous)
we proved
le
S (plus (weight_map f0 u2) (weight_map f0 t2))
S (plus (weight_map g u1) (weight_map g t1))
that is equivalent to
le
weight_map f0 (THead (Flat __9) u2 t2)
weight_map g (THead (Flat __9) u1 t1)
we proved
∀f0:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f0 m) (g m))
→(lt (weight_map f0 (lift (S i) O v)) (g i)
→le (weight_map f0 t2) (weight_map g t1))
→∀f0:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f0 m) (g m))
→(lt (weight_map f0 (lift (S i) O v)) (g i)
→(le
weight_map f0 (THead (Flat __9) u2 t2)
weight_map g (THead (Flat __9) u1 t1)))
that is equivalent to
∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→((lt
weight_map f (lift (S (s (Flat __7) i)) O v)
g (s (Flat __7) i))
→le (weight_map f t2) (weight_map g t1))
→∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Flat __9) u2 t2)
weight_map g (THead (Flat __9) u1 t1)))
we proved
subst0 i v t1 t2
→(∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→((lt
weight_map f (lift (S (s (Flat __7) i)) O v)
g (s (Flat __7) i))
→le (weight_map f t2) (weight_map g t1))
→∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Flat __9) u2 t2)
weight_map g (THead (Flat __9) u1 t1))))
that is equivalent to
subst0 (s (Flat __3) i) v t1 t2
→(∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→((lt
weight_map f (lift (S (s (Flat __7) i)) O v)
g (s (Flat __7) i))
→le (weight_map f t2) (weight_map g t1))
→∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Flat __9) u2 t2)
weight_map g (THead (Flat __9) u1 t1))))
∀t1:T
.∀t2:T
.subst0 (s (Flat __3) i) v t1 t2
→(∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→((lt
weight_map f (lift (S (s (Flat __7) i)) O v)
g (s (Flat __7) i))
→le (weight_map f t2) (weight_map g t1))
→∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→(le
weight_map f (THead (Flat __9) u2 t2)
weight_map g (THead (Flat __9) u1 t1))))
we proved
∀t1:T
.∀t2:T
.subst0 (s k i) v t1 t2
→(∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S (s k i)) O v)) (g (s k i))
→le (weight_map f t2) (weight_map g t1))
→∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→le (weight_map f (THead k u2 t2)) (weight_map g (THead k u1 t1))))
∀v:T
.∀u1:T
.∀u2:T
.∀i:nat
.subst0 i v u1 u2
→(∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→le (weight_map f u2) (weight_map g u1))
→∀k:K
.∀t1:T
.∀t2:T
.subst0 (s k i) v t1 t2
→(∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S (s k i)) O v)) (g (s k i))
→le (weight_map f t2) (weight_map g t1))
→∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S i) O v)) (g i)
→le (weight_map f (THead k u2 t2)) (weight_map g (THead k u1 t1)))))
we proved
∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S d) O u)) (g d)
→le (weight_map f z) (weight_map g t))
we proved
∀u:T
.∀t:T
.∀z:T
.∀d:nat
.subst0 d u t z
→∀f:nat→nat
.∀g:nat→nat
.∀m:nat.(le (f m) (g m))
→(lt (weight_map f (lift (S d) O u)) (g d)
→le (weight_map f z) (weight_map g t))