---

Step * 1 of Lemma mk-s-group_wf


1. ss : self:"Point":Type
        "#":{s:self."Point" ⟶ self."Point" ⟶ ℙ| ∀x:self."Point". (¬(s x x))} 
        "#symm":∀x,y:self."Point".  ((self."#" x y) ⇒ (self."#" y x)) ⋂ x:Atom ⟶ if x =a "#or"
                                                                                   then ∀x,y,z:self."Point".
                                                                                          ((self."#" x y)
                                                                                          ⇒ ((self."#" x z)
                                                                                             ∨ (self."#" y z)))
                                                                                   else Top
                                                                                   fi 
2. ss ∈ record(x.Top)
3. e : Point
4. i : Point ⟶ Point
5. o : {f:Point ⟶ Point ⟶ Point| 
        (∀x,y,z:Point.  f x (f y z) ≡ f (f x y) z) ∧ (∀x:Point. f x e ≡ x) ∧ (∀x:Point. f x (i x) ≡ e)} 
6. sep : ∀x,x',y,y':Point.  (o x y # o x' y ⇒ (x # x' ∨ y # y'))
7. invsep : ∀x,y:Point.  (i x # i y ⇒ x # y)
8. ss ∈ SeparationSpace
9. ss."Point" ∈ Type
10. ss."#" ∈ {s:ss."Point" ⟶ ss."Point" ⟶ ℙ| ∀x:ss."Point". (¬(s x x))} 
11. ss."#symm" ∈ ∀x,y:ss."Point".  ((ss."#" x y) ⇒ (ss."#" y x))
12. ss."#or" ∈ ∀x,y,z:ss."Point".  ((ss."#" x y) ⇒ ((ss."#" x z) ∨ (ss."#" y z)))
⊢ ss["id" := e]["inv" := i]["op" := o]["opsep" := sep]["invsep" := invsep] ∈ SeparationSpace
BY
{ (RepUR ``separation-space`` 0
   THEN RepeatFor 4 ((RecordPlusTypeCD THENL [ Id; (Reduce 0 THEN Trivial)]))
   THEN RepUR ``record record-update`` 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  ss  :  self:"Point":Type
                "\#":\{s:self."Point"  {}\mrightarrow{}  self."Point"  {}\mrightarrow{}  \mBbbP{}|  \mforall{}x:self."Point".  (\mneg{}(s  x  x))\} 
                "\#symm":\mforall{}x,y:self."Point".    ((self."\#"  x  y)  {}\mRightarrow{}  (self."\#"  y  x))  \mcap{}  x:Atom
                {}\mrightarrow{}  if  x  =a  "\#or"
                      then  \mforall{}x,y,z:self."Point".    ((self."\#"  x  y)  {}\mRightarrow{}  ((self."\#"  x  z)  \mvee{}  (self."\#"  y  z)))
                      else  Top
                      fi 
2.  ss  \mmember{}  record(x.Top)
3.  e  :  Point
4.  i  :  Point  {}\mrightarrow{}  Point
5.  o  :  \{f:Point  {}\mrightarrow{}  Point  {}\mrightarrow{}  Point| 
                (\mforall{}x,y,z:Point.    f  x  (f  y  z)  \mequiv{}  f  (f  x  y)  z)
                \mwedge{}  (\mforall{}x:Point.  f  x  e  \mequiv{}  x)
                \mwedge{}  (\mforall{}x:Point.  f  x  (i  x)  \mequiv{}  e)\} 
6.  sep  :  \mforall{}x,x',y,y':Point.    (o  x  y  \#  o  x'  y  {}\mRightarrow{}  (x  \#  x'  \mvee{}  y  \#  y'))
7.  invsep  :  \mforall{}x,y:Point.    (i  x  \#  i  y  {}\mRightarrow{}  x  \#  y)
8.  ss  \mmember{}  SeparationSpace
9.  ss."Point"  \mmember{}  Type
10.  ss."\#"  \mmember{}  \{s:ss."Point"  {}\mrightarrow{}  ss."Point"  {}\mrightarrow{}  \mBbbP{}|  \mforall{}x:ss."Point".  (\mneg{}(s  x  x))\} 
11.  ss."\#symm"  \mmember{}  \mforall{}x,y:ss."Point".    ((ss."\#"  x  y)  {}\mRightarrow{}  (ss."\#"  y  x))
12.  ss."\#or"  \mmember{}  \mforall{}x,y,z:ss."Point".    ((ss."\#"  x  y)  {}\mRightarrow{}  ((ss."\#"  x  z)  \mvee{}  (ss."\#"  y  z)))
\mvdash{}  ss["id"  :=  e]["inv"  :=  i]["op"  :=  o]["opsep"  :=  sep]["invsep"  :=  invsep]  \mmember{}  SeparationSpace


By

---

Latex:
(RepUR  ``separation-space``  0
  THEN  RepeatFor  4  ((RecordPlusTypeCD  THENL  [  Id;  (Reduce  0  THEN  Trivial)]))
  THEN  RepUR  ``record  record-update``  0
  THEN  Auto)

---

Home Index