---

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
{ (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) }

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
⊢ ((0 + ((F 0) * u)) + weighted-sum(v;λi.(F (i + 1)))) ≤ ((0 + ((G 0) * u)) + weighted-sum(v;λi.(G (i + 1))))

---

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

(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)

---

Home Index