Step
*
1
2
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)
⊢ mul-monomials(<m1, u><m1, u>) = mul-monomials(<m1, m2><m1, []>) ∈ iMonomial()
BY
{ (RepUR ``mul-monomials`` 0 THEN (GenConcl ⌜(m1 * m1) = d ∈ ℤ-o⌝⋅ THENA Auto)) }
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 = merge-int-accum(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)
\mvdash{}  mul-monomials(<m1,  u><m1,  u>)  =  mul-monomials(<m1,  m2><m1,  []>)
By
Latex:
(RepUR  ``mul-monomials``  0  THEN  (GenConcl  \mkleeneopen{}(m1  *  m1)  =  d\mkleeneclose{}\mcdot{}  THENA  Auto))
Home
Index