---

Step * 1 1 1 1 1 2 2 1 1 of Lemma assert-nonneg-monomial

.....antecedent..... 
1. n : ℕ
2. u : ℤ
3. u1 : ℤ
4. v : ℤ List
5. ∀L1:ℤ List
     (||L1|| < ||[u; [u1 / v]]||
     ⇒ sorted(L1)
     ⇒ (↑even-int-list(L1))
     ⇒ (∃u:{vs:ℤ List| sorted(vs)} . (L1 = merge-int-accum(u;u) ∈ (ℤ List))))
6. sorted([u; [u1 / v]])
7. u = u1 ∈ ℤ
8. ↑even-int-list(v)
⊢ sorted(v)
BY
{ ((RWO "sorted-cons" (-3) THENA Auto) THEN D -3 THEN RWO "sorted-cons" (-4) THEN Auto) }

---

Latex:

---

Latex:
.....antecedent..... 
1.  n  :  \mBbbN{}
2.  u  :  \mBbbZ{}
3.  u1  :  \mBbbZ{}
4.  v  :  \mBbbZ{}  List
5.  \mforall{}L1:\mBbbZ{}  List
          (||L1||  <  ||[u;  [u1  /  v]]||
          {}\mRightarrow{}  sorted(L1)
          {}\mRightarrow{}  (\muparrow{}even-int-list(L1))
          {}\mRightarrow{}  (\mexists{}u:\{vs:\mBbbZ{}  List|  sorted(vs)\}  .  (L1  =  merge-int-accum(u;u))))
6.  sorted([u;  [u1  /  v]])
7.  u  =  u1
8.  \muparrow{}even-int-list(v)
\mvdash{}  sorted(v)


By

---

Latex:
((RWO  "sorted-cons"  (-3)  THENA  Auto)  THEN  D  -3  THEN  RWO  "sorted-cons"  (-4)  THEN  Auto)

---

Home Index