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. {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`` 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. {vs:ℤ List| sorted(vs)} 
6. m2 merge-int-accum(u;u) ∈ (ℤ List)
7. : ℤ-o
8. (m1 m1) d ∈ ℤ-o
⊢ eval in
  eval merge-int-accum(u;u) in
    <c, u>
eval in
  eval 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