---

Step * 1 1 2 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
{ ((With [j] (D 0) THENM AbReduce 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))
8. ¬Reducible(j)
⊢ j ∈ Atom{g}

2
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)
⊢ j = (j * e) ∈ |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.  \mneg{}Reducible(j)
\mvdash{}  \mexists{}as:Atom\{g\}  List.  (j  =  (\mPi{}  as))


By

---

Latex:
((With  [j]  (D  0)  THENM  AbReduce  0)  THENA  Auto)

---

Home Index