Step * of Lemma mfact_exists

g:IAbMonoid
  (Cancel(|g|;|g|;*)
   WellFnd{i}(|g|;x,y.x p| y)
   (∀c:|g|. Dec(Reducible(c)))
   (∀b:|g|. ((¬(g-unit(b)))  (∃as:Atom{g} List. (b (Π as) ∈ |g|)))))
BY
((UnivCD) THENA Auto) }

1
1. IAbMonoid
2. Cancel(|g|;|g|;*)
3. WellFnd{i}(|g|;x,y.x p| y)
4. ∀c:|g|. Dec(Reducible(c))
5. |g|
6. ¬(g-unit(b))
⊢ ∃as:Atom{g} List. (b (Π as) ∈ |g|)


Latex:


Latex:
\mforall{}g:IAbMonoid
    (Cancel(|g|;|g|;*)
    {}\mRightarrow{}  WellFnd\{i\}(|g|;x,y.x  p|  y)
    {}\mRightarrow{}  (\mforall{}c:|g|.  Dec(Reducible(c)))
    {}\mRightarrow{}  (\mforall{}b:|g|.  ((\mneg{}(g-unit(b)))  {}\mRightarrow{}  (\mexists{}as:Atom\{g\}  List.  (b  =  (\mPi{}  as))))))


By


Latex:
((UnivCD)  THENA  Auto)




Home Index