---

Step * 1 2 1 1 of Lemma ws-monotone


1. d : ℤ
2. 0 < d
3. ∀p:ℚ List
     ((||p|| ≤ (d - 1))
     ⇒ (∀F,G:ℕ||p|| ─→ ℚ.
           ((∀q:ℚ. ((q ∈ p) ⇒ (0 ≤ q))) ⇒ (∀x:ℕ||p||. ((F x) ≤ (G x))) ⇒ (weighted-sum(p;F) ≤ weighted-sum(p;G)))))
4. u : ℚ
5. v : ℚ List
6. (||v|| + 1) ≤ d@i
7. F : ℕ||v|| + 1 ─→ ℚ@i
8. G : ℕ||v|| + 1 ─→ ℚ@i
9. ∀q:ℚ. ((q ∈ [u / v]) ⇒ (0 ≤ q))@i
10. ∀x:ℕ||v|| + 1. ((F x) ≤ (G x))@i
11. weighted-sum(v;λi.(F (i + 1))) ≤ weighted-sum(v;λi.(G (i + 1)))
⊢ ((0 + ((F 0) * u)) + weighted-sum(v;λi.(F (i + 1)))) ≤ ((0 + ((G 0) * u)) + weighted-sum(v;λi.(G (i + 1))))
BY
{ (Assert ((F 0) * u) ≤ ((G 0) * u) BY
         ((Subst' ((F 0) * u) = (u * (F 0)) ∈ ℚ 0 THENA Auto')⋅
          THEN (Subst' ((G 0) * u) = (u * (G 0)) ∈ ℚ 0 THENA Auto')⋅
          )) }

1
1. d : ℤ
2. 0 < d
3. ∀p:ℚ List
     ((||p|| ≤ (d - 1))
     ⇒ (∀F,G:ℕ||p|| ─→ ℚ.
           ((∀q:ℚ. ((q ∈ p) ⇒ (0 ≤ q))) ⇒ (∀x:ℕ||p||. ((F x) ≤ (G x))) ⇒ (weighted-sum(p;F) ≤ weighted-sum(p;G)))))
4. u : ℚ
5. v : ℚ List
6. (||v|| + 1) ≤ d@i
7. F : ℕ||v|| + 1 ─→ ℚ@i
8. G : ℕ||v|| + 1 ─→ ℚ@i
9. ∀q:ℚ. ((q ∈ [u / v]) ⇒ (0 ≤ q))@i
10. ∀x:ℕ||v|| + 1. ((F x) ≤ (G x))@i
11. weighted-sum(v;λi.(F (i + 1))) ≤ weighted-sum(v;λi.(G (i + 1)))
⊢ (u * (F 0)) ≤ (u * (G 0))

2
1. d : ℤ
2. 0 < d
3. ∀p:ℚ List
     ((||p|| ≤ (d - 1))
     ⇒ (∀F,G:ℕ||p|| ─→ ℚ.
           ((∀q:ℚ. ((q ∈ p) ⇒ (0 ≤ q))) ⇒ (∀x:ℕ||p||. ((F x) ≤ (G x))) ⇒ (weighted-sum(p;F) ≤ weighted-sum(p;G)))))
4. u : ℚ
5. v : ℚ List
6. (||v|| + 1) ≤ d@i
7. F : ℕ||v|| + 1 ─→ ℚ@i
8. G : ℕ||v|| + 1 ─→ ℚ@i
9. ∀q:ℚ. ((q ∈ [u / v]) ⇒ (0 ≤ q))@i
10. ∀x:ℕ||v|| + 1. ((F x) ≤ (G x))@i
11. weighted-sum(v;λi.(F (i + 1))) ≤ weighted-sum(v;λi.(G (i + 1)))
12. ((F 0) * u) ≤ ((G 0) * u)
⊢ ((0 + ((F 0) * u)) + weighted-sum(v;λi.(F (i + 1)))) ≤ ((0 + ((G 0) * u)) + weighted-sum(v;λi.(G (i + 1))))

---

Latex:



1.  d  :  \mBbbZ{}
2.  0  <  d
3.  \mforall{}p:\mBbbQ{}  List
          ((||p||  \mleq{}  (d  -  1))
          {}\mRightarrow{}  (\mforall{}F,G:\mBbbN{}||p||  {}\mrightarrow{}  \mBbbQ{}.
                      ((\mforall{}q:\mBbbQ{}.  ((q  \mmember{}  p)  {}\mRightarrow{}  (0  \mleq{}  q)))
                      {}\mRightarrow{}  (\mforall{}x:\mBbbN{}||p||.  ((F  x)  \mleq{}  (G  x)))
                      {}\mRightarrow{}  (weighted-sum(p;F)  \mleq{}  weighted-sum(p;G)))))
4.  u  :  \mBbbQ{}
5.  v  :  \mBbbQ{}  List
6.  (||v||  +  1)  \mleq{}  d@i
7.  F  :  \mBbbN{}||v||  +  1  {}\mrightarrow{}  \mBbbQ{}@i
8.  G  :  \mBbbN{}||v||  +  1  {}\mrightarrow{}  \mBbbQ{}@i
9.  \mforall{}q:\mBbbQ{}.  ((q  \mmember{}  [u  /  v])  {}\mRightarrow{}  (0  \mleq{}  q))@i
10.  \mforall{}x:\mBbbN{}||v||  +  1.  ((F  x)  \mleq{}  (G  x))@i
11.  weighted-sum(v;\mlambda{}i.(F  (i  +  1)))  \mleq{}  weighted-sum(v;\mlambda{}i.(G  (i  +  1)))
\mvdash{}  ((0  +  ((F  0)  *  u))  +  weighted-sum(v;\mlambda{}i.(F  (i  +  1))))  \mleq{}  ((0  +  ((G  0)  *  u))
+  weighted-sum(v;\mlambda{}i.(G  (i  +  1))))


By

(Assert  ((F  0)  *  u)  \mleq{}  ((G  0)  *  u)  BY
              ((Subst'  ((F  0)  *  u)  =  (u  *  (F  0))  0  THENA  Auto')\mcdot{}
                THEN  (Subst'  ((G  0)  *  u)  =  (u  *  (G  0))  0  THENA  Auto')\mcdot{}
                ))

---

Home Index