---

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


1. m1 : ℤ-o
2. m2 : {vs:ℤ List| sorted(vs)} 
3. 0 ≤ m1
4. ↑even-int-list(m2)
5. u : {vs:ℤ List| sorted(vs)} 
6. m2 = merge-int-accum(u;u) ∈ (ℤ List)
7. d : ℤ-o
8. (m1 * m1) = d ∈ ℤ-o
⊢ eval c = d in eval u = merge-int-accum(u;u) in   <c, u> = eval c = d in eval u = m2 in   <c, u> ∈ iMonomial()
BY
{ (HypSubst' (-3) 0 THEN Auto) }

---

Latex:

---

Latex:

1.  m1  :  \mBbbZ{}\msupminus{}\msupzero{}
2.  m2  :  \{vs:\mBbbZ{}  List|  sorted(vs)\} 
3.  0  \mleq{}  m1
4.  \muparrow{}even-int-list(m2)
5.  u  :  \{vs:\mBbbZ{}  List|  sorted(vs)\} 
6.  m2  =  merge-int-accum(u;u)
7.  d  :  \mBbbZ{}\msupminus{}\msupzero{}
8.  (m1  *  m1)  =  d
\mvdash{}  eval  c  =  d  in  eval  u  =  merge-int-accum(u;u)  in      <c,  u>  =  eval  c  =  d  in  eval  u  =  m2  in      <c,  u>


By

---

Latex:
(HypSubst'  (-3)  0  THEN  Auto)

---

Home Index