---

Step * 1 2 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 = merge-int-accum(m2;[]) in
    <c, u>
∈ iMonomial()
BY
{ (Subst' merge-int-accum(m2;[]) ~ m2 0 THENA Computation) }

1
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()

---

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  =  merge-int-accum(m2;[])  in
        <c,  u>


By

---

Latex:
(Subst'  merge-int-accum(m2;[])  \msim{}  m2  0  THENA  Computation)

---

Home Index