---

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


1. n : ℕ
2. u : ℤ
3. v : ℤ List
4. ∀L1:ℤ List
     (||L1|| < ||[u / v]||
     ⇒ sorted(L1)
     ⇒ (↑even-int-list(L1))
     ⇒ (∃u:{vs:ℤ List| sorted(vs)} . (L1 = merge-int-accum(u;u) ∈ (ℤ List))))
5. sorted([u / v])
6. ↑even-int-list([u / v])
⊢ ∃u@0:{vs:ℤ List| sorted(vs)} . ([u / v] = merge-int-accum(u@0;u@0) ∈ (ℤ List))
BY
{ DVar `v' }

1
1. n : ℕ
2. u : ℤ
3. ∀L1:ℤ List
     (||L1|| < ||[u]||
     ⇒ sorted(L1)
     ⇒ (↑even-int-list(L1))
     ⇒ (∃u:{vs:ℤ List| sorted(vs)} . (L1 = merge-int-accum(u;u) ∈ (ℤ List))))
4. sorted([u])
5. ↑even-int-list([u])
⊢ ∃u@0:{vs:ℤ List| sorted(vs)} . ([u] = merge-int-accum(u@0;u@0) ∈ (ℤ List))

2
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. ↑even-int-list([u; [u1 / v]])
⊢ ∃u@0:{vs:ℤ List| sorted(vs)} . ([u; [u1 / v]] = merge-int-accum(u@0;u@0) ∈ (ℤ List))

---

Latex:

---

Latex:

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


By

---

Latex:
DVar  `v'

---

Home Index