---

Step * 1 of Lemma mfact_exists


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

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

---

Latex:

---

Latex:

1.  g  :  IAbMonoid
2.  Cancel(|g|;|g|;*)
3.  WellFnd\{i\}(|g|;x,y.x  p|  y)
4.  \mforall{}c:|g|.  Dec(Reducible(c))
5.  b  :  |g|
6.  \mneg{}(g-unit(b))
\mvdash{}  \mexists{}as:Atom\{g\}  List.  (b  =  (\mPi{}  as))


By

---

Latex:
((WFndHypInd  3  5  THENM  D  0)  THENA  Auto)

---

Home Index