---

Step * 1 of Lemma matom_ty_properties


1. g : GrpSig@i'
2. a : Atom{g}@i
⊢ (¬(g-unit(a))) ∧ (¬Reducible(a))
BY
{ ((Unfold `matom_ty` 2 THENM D 2 
THEN CUnhide THENM D 3) THEN Auto) }

---

Latex:

---

Latex:

1.  g  :  GrpSig@i'
2.  a  :  Atom\{g\}@i
\mvdash{}  (\mneg{}(g-unit(a)))  \mwedge{}  (\mneg{}Reducible(a))


By

---

Latex:
((Unfold  `matom\_ty`  2  THENM  D  2 
THEN  CUnhide  THENM  D  3)  THEN  Auto)

---

Home Index