---

Step * of Lemma mfact_exists_a

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

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

---

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{}c:|g|.  Dec(g-unit(c)))
    {}\mRightarrow{}  (\mforall{}b:|g|.  \mexists{}as:Atom\{g\}  List.  (b  \msim{}  (\mPi{}  as))))


By

---

Latex:
((RepD)  THENA  Auto)

---

Home Index