---

Step * 1 1 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. j : |g|
6. ∀k:|g|. ((k p| j) ⇒ (¬(g-unit(k))) ⇒ (∃as:Atom{g} List. (k = (Π as) ∈ |g|)))
7. ¬(g-unit(j))
8. Reducible(j)
⊢ ∃as:Atom{g} List. (j = (Π as) ∈ |g|)
BY
{ UnfoldTopAb 8 THEN ExistHD 8 }

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))
8. b : |g|
9. c : |g|
10. ¬(g-unit(b))
11. ¬(g-unit(c))
12. j = (b * c) ∈ |g|
⊢ ∃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.  j  :  |g|
6.  \mforall{}k:|g|.  ((k  p|  j)  {}\mRightarrow{}  (\mneg{}(g-unit(k)))  {}\mRightarrow{}  (\mexists{}as:Atom\{g\}  List.  (k  =  (\mPi{}  as))))
7.  \mneg{}(g-unit(j))
8.  Reducible(j)
\mvdash{}  \mexists{}as:Atom\{g\}  List.  (j  =  (\mPi{}  as))


By

---

Latex:
UnfoldTopAb  8  THEN  ExistHD  8

---

Home Index