---

Step * 5 of Lemma mk-s-subgroup_wf


1. sg : s-Group
2. P : Point ⟶ ℙ
3. P[1]
4. ∀x:Point. (P[x] ⇒ P[x^-1])
5. ∀x,y:Point.  (P[x] ⇒ P[y] ⇒ P[(x y)])
⊢ sg."opsep" ∈ ∀x,x',y,y':{x:Point| P[x]} .  ((λx,y. (x y)) x y # (λx,y. (x y)) x' y ⇒ (x # x' ∨ y # y'))
BY
{ (Reduce 0
   THEN (Assert sg ∈ s-Group BY
               Auto)
   THEN (D 1 THENA Auto)
   THEN DoSubsume
   THEN Try (Trivial)
   THEN Folds ``sg-op`` 0
   THEN Unfold `all` 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  sg  :  s-Group
2.  P  :  Point  {}\mrightarrow{}  \mBbbP{}
3.  P[1]
4.  \mforall{}x:Point.  (P[x]  {}\mRightarrow{}  P[x\^{}-1])
5.  \mforall{}x,y:Point.    (P[x]  {}\mRightarrow{}  P[y]  {}\mRightarrow{}  P[(x  y)])
\mvdash{}  sg."opsep"  \mmember{}  \mforall{}x,x',y,y':\{x:Point|  P[x]\}  .    ((\mlambda{}x,y.  (x  y))  x  y  \#  (\mlambda{}x,y.  (x  y))  x'  y  {}\mRightarrow{}  (x  \#  x'  \mvee{}  y  \000C\#  y'))


By

---

Latex:
(Reduce  0
  THEN  (Assert  sg  \mmember{}  s-Group  BY
                          Auto)
  THEN  (D  1  THENA  Auto)
  THEN  DoSubsume
  THEN  Try  (Trivial)
  THEN  Folds  ``sg-op``  0
  THEN  Unfold  `all`  0
  THEN  Auto)

---

Home Index