---

Step * 1 of Lemma ws-monotone


∀p:ℚ List. ∀F,G:ℕ||p|| ⟶ ℚ.
  ((∀q:ℚ. ((q ∈ p) ⇒ (0 ≤ q))) ⇒ (∀x:ℕ||p||. ((F x) ≤ (G x))) ⇒ (weighted-sum(p;F) ≤ weighted-sum(p;G)))
BY
{ xxxInductionOn ⌜||p||⌝ NatInd⋅xxx }

1
.....basecase..... 
1. d : ℤ
⊢ ∀p:ℚ List
    ((||p|| ≤ 0)
    ⇒ (∀F,G:ℕ||p|| ⟶ ℚ.
          ((∀q:ℚ. ((q ∈ p) ⇒ (0 ≤ q))) ⇒ (∀x:ℕ||p||. ((F x) ≤ (G x))) ⇒ (weighted-sum(p;F) ≤ weighted-sum(p;G)))))

2
.....upcase..... 
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)))))
⊢ ∀p:ℚ List
    ((||p|| ≤ d)
    ⇒ (∀F,G:ℕ||p|| ⟶ ℚ.
          ((∀q:ℚ. ((q ∈ p) ⇒ (0 ≤ q))) ⇒ (∀x:ℕ||p||. ((F x) ≤ (G x))) ⇒ (weighted-sum(p;F) ≤ weighted-sum(p;G)))))

3
1. ∀d:ℕ. ∀p:ℚ List.
     ((||p|| ≤ d)
     ⇒ (∀F,G:ℕ||p|| ⟶ ℚ.
           ((∀q:ℚ. ((q ∈ p) ⇒ (0 ≤ q))) ⇒ (∀x:ℕ||p||. ((F x) ≤ (G x))) ⇒ (weighted-sum(p;F) ≤ weighted-sum(p;G)))))
2. p : ℚ List
3. F : ℕ||p|| ⟶ ℚ
4. G : ℕ||p|| ⟶ ℚ
5. ∀q:ℚ. ((q ∈ p) ⇒ (0 ≤ q))
6. ∀x:ℕ||p||. ((F x) ≤ (G x))
7. ∀F,G:ℕ||p|| ⟶ ℚ.
     ((∀q:ℚ. ((q ∈ p) ⇒ (0 ≤ q))) ⇒ (∀x:ℕ||p||. ((F x) ≤ (G x))) ⇒ (weighted-sum(p;F) ≤ weighted-sum(p;G)))
⊢ weighted-sum(p;F) ≤ weighted-sum(p;G)

---

Latex:

---

Latex:

\mforall{}p:\mBbbQ{}  List.  \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)))


By

---

Latex:
xxxInductionOn  \mkleeneopen{}||p||\mkleeneclose{}  NatInd\mcdot{}xxx

---

Home Index