---

Step * 1 2 of Lemma ws-monotone

.....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)))))
BY
{ xxx(Auto
      THEN DVar `p'
      THEN All Reduce
      THEN Auto'
      THEN Subst' [u / v] ~ [u] @ v 0
      THEN Try (Complete ((Reduce 0 THEN Trivial)))
      THEN (RWO "weighted-sum-split" 0 THENA (Auto' THEN All Reduce THEN Auto'))
      THEN Reduce 0)xxx }

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
7. F : ℕ||v|| + 1 ⟶ ℚ
8. G : ℕ||v|| + 1 ⟶ ℚ
9. ∀q:ℚ. ((q ∈ [u / v]) ⇒ (0 ≤ q))
10. ∀x:ℕ||v|| + 1. ((F x) ≤ (G x))
⊢ ((0 + ((F 0) * u)) + weighted-sum(v;λi.(F (i + 1)))) ≤ ((0 + ((G 0) * u)) + weighted-sum(v;λi.(G (i + 1))))

---

Latex:

---

Latex:
.....upcase..... 
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)))))
\mvdash{}  \mforall{}p:\mBbbQ{}  List
        ((||p||  \mleq{}  d)
        {}\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

---

Latex:
xxx(Auto
        THEN  DVar  `p'
        THEN  All  Reduce
        THEN  Auto'
        THEN  Subst'  [u  /  v]  \msim{}  [u]  @  v  0
        THEN  Try  (Complete  ((Reduce  0  THEN  Trivial)))
        THEN  (RWO  "weighted-sum-split"  0  THENA  (Auto'  THEN  All  Reduce  THEN  Auto'))
        THEN  Reduce  0)xxx

---

Home Index