---

Step * 1 1 of Lemma ws-monotone

.....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)))))
BY
{ ((Auto THEN DVar `p') THEN All Reduce THEN Auto') }

---

Latex:


.....basecase..... 
1.  d  :  \mBbbZ{}
\mvdash{}  \mforall{}p:\mBbbQ{}  List
        ((||p||  \mleq{}  0)
        {}\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)))))


By

((Auto  THEN  DVar  `p')  THEN  All  Reduce  THEN  Auto')

---

Home Index