---

Step * 1 2 1 of Lemma mfact_exists_a


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
7. ¬(g-unit(b))
8. ∃as:Atom{g} List. (b = (Π as) ∈ |g|)
⊢ ∃as:Atom{g} List. (b ~ (Π as))
BY
{ D (-1) THEN With as (D 0) 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
7. ¬(g-unit(b))
8. as : Atom{g} List
9. b = (Π as) ∈ |g|
⊢ b ~ (Π
        as)

---

Latex:

---

Latex:

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


By

---

Latex:
D  (-1)  THEN  With  as  (D  0)  THENA  Auto

---

Home Index