---

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


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

---

Latex:

---

Latex:

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


By

---

Latex:
(D  0  With  \mkleeneopen{}[]\mkleeneclose{}    THEN  Auto)

---

Home Index