---

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

.....assertion..... 
1. m2 : {vs:ℤ List| sorted(vs)} 
2. ↑even-int-list(m2)
⊢ ∀L:ℤ List. (sorted(L) ⇒ (↑even-int-list(L)) ⇒ (∃u:{vs:ℤ List| sorted(vs)} . (L = merge-int-accum(u;u) ∈ (ℤ List))))
BY
{ (All Thin THEN InductionOnLength) }

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

---

Latex:

---

Latex:
.....assertion..... 
1.  m2  :  \{vs:\mBbbZ{}  List|  sorted(vs)\} 
2.  \muparrow{}even-int-list(m2)
\mvdash{}  \mforall{}L:\mBbbZ{}  List
        (sorted(L)  {}\mRightarrow{}  (\muparrow{}even-int-list(L))  {}\mRightarrow{}  (\mexists{}u:\{vs:\mBbbZ{}  List|  sorted(vs)\}  .  (L  =  merge-int-accum(u;u))))


By

---

Latex:
(All  Thin  THEN  InductionOnLength)

---

Home Index