---

Step * of Lemma mk-s-group_wf

∀[ss:SeparationSpace]. ∀[e:Point(ss)]. ∀[i:Point(ss) ⟶ Point(ss)]. ∀[o:{f:Point(ss) ⟶ Point(ss) ⟶ Point(ss)| 
                                                                         (∀x,y,z:Point(ss).  f x (f y z) ≡ f (f x y) z)
                                                                         ∧ (∀x:Point(ss). f x e ≡ x)
                                                                         ∧ (∀x:Point(ss). f x (i x) ≡ e)} ].
∀[sep:∀x,x',y,y':Point(ss).  (o x y # o x' y' ⇒ (x # x' ∨ y # y'))]. ∀[invsep:∀x,y:Point(ss).  (i x # i y ⇒ x # y)].
  (mk-s-group(ss; e; i; o; sep; invsep) ∈ s-Group)
BY
{ (Auto
   THEN (Assert ss ∈ SeparationSpace BY
               Auto)
   THEN (D 1 THENA Auto)
   THEN Unfolds ``mk-s-group s-group`` 0
   THEN RepUR ``ss-point ss-sep`` 0
   THEN ((MemTypeCD THENA Auto)
         THENL [(Unfold `s-group-structure` 0
                 THEN RepeatFor 5 ((RecordPlusTypeCD
                                    THENL [ Id
                                          ; (Reduce 0
                                             THEN Try ((RepUR ``ss-eq ss-sep ss-point`` 0
                                                        THEN Folds ``ss-point ss-sep`` 0
                                                        THEN Try (Fold `ss-eq` 0)
                                                        THEN (Trivial ORELSE Complete (MemCD))))
                                             )]
                                   ))
                 THEN RepUR ``separation-space`` 0
                 THEN RepeatFor 3 ((RecordPlusTypeCD THENL [ Id; (Reduce 0 THEN Trivial)]))
                 THEN RepUR ``record record-update`` 0
                 THEN Auto)
               ; (D 0
                  THEN RepUR ``ss-eq ss-sep ss-point sg-op sg-id sg-inv`` 0
                  THEN Folds ``ss-point ss-sep`` 0
                  THEN Try (Fold `ss-eq` 0)
                  THEN DSetVars
                  THEN Unhide
                  THEN Auto)]
   )) }

---

Latex:

---

Latex:
\mforall{}[ss:SeparationSpace].  \mforall{}[e:Point(ss)].  \mforall{}[i:Point(ss)  {}\mrightarrow{}  Point(ss)].  \mforall{}[o:\{f:Point(ss)
                                                                                                                                                  {}\mrightarrow{}  Point(ss)
                                                                                                                                                  {}\mrightarrow{}  Point(ss)| 
                                                                                                                                                  (\mforall{}x,y,z:Point(ss).
                                                                                                                                                        f  x  (f  y  z)  \mequiv{}  f  (f  x  y) 
                                                                                                                                                                                    z)
                                                                                                                                                  \mwedge{}  (\mforall{}x:Point(ss).  f  x  e  \mequiv{}  x)
                                                                                                                                                  \mwedge{}  (\mforall{}x:Point(ss)
                                                                                                                                                            f  x  (i  x)  \mequiv{}  e)\}  ].
\mforall{}[sep:\mforall{}x,x',y,y':Point(ss).    (o  x  y  \#  o  x'  y'  {}\mRightarrow{}  (x  \#  x'  \mvee{}  y  \#  y'))].  \mforall{}[invsep:\mforall{}x,y:Point(ss).
                                                                                                                                                                  (i  x  \#  i  y
                                                                                                                                                                  {}\mRightarrow{}  x  \#  y)].
    (mk-s-group(ss;  e;  i;  o;  sep;  invsep)  \mmember{}  s-Group)


By

---

Latex:
(Auto
  THEN  (Assert  ss  \mmember{}  SeparationSpace  BY
                          Auto)
  THEN  (D  1  THENA  Auto)
  THEN  Unfolds  ``mk-s-group  s-group``  0
  THEN  RepUR  ``ss-point  ss-sep``  0
  THEN  ((MemTypeCD  THENA  Auto)
              THENL  [(Unfold  `s-group-structure`  0
                              THEN  RepeatFor  5  ((RecordPlusTypeCD
                                                                    THENL  [  Id
                                                                                ;  (Reduce  0
                                                                                      THEN  Try  ((RepUR  ``ss-eq  ss-sep  ss-point``  0
                                                                                                            THEN  Folds  ``ss-point  ss-sep``  0
                                                                                                            THEN  Try  (Fold  `ss-eq`  0)
                                                                                                            THEN  (Trivial  ORELSE  Complete  (MemCD))))
                                                                                      )]
                                                                  ))
                              THEN  RepUR  ``separation-space``  0
                              THEN  RepeatFor  3  ((RecordPlusTypeCD  THENL  [  Id;  (Reduce  0  THEN  Trivial)]))
                              THEN  RepUR  ``record  record-update``  0
                              THEN  Auto)
                          ;  (D  0
                                THEN  RepUR  ``ss-eq  ss-sep  ss-point  sg-op  sg-id  sg-inv``  0
                                THEN  Folds  ``ss-point  ss-sep``  0
                                THEN  Try  (Fold  `ss-eq`  0)
                                THEN  DSetVars
                                THEN  Unhide
                                THEN  Auto)]
  ))

---

Home Index