---

Step * of Lemma mk-ss_wf

∀[P:Type]. ∀[Sep:{s:P ⟶ P ⟶ ℙ| ∀x:P. (¬(s x x))} ]. ∀[C:∀x,y,z:P.  ((Sep x y) ⇒ ((Sep x z) ∨ (Sep y z)))].
  (Point=P #=Sep cotrans=C ∈ SeparationSpace)
BY
{ (Auto
   THEN RepUR ``mk-ss separation-space`` 0
   THEN RepeatFor 3 ((RecordPlusTypeCD THENL [ Id; (Reduce 0 THEN Try (Trivial))]))
   THEN RepUR ``record record-update`` 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[P:Type].  \mforall{}[Sep:\{s:P  {}\mrightarrow{}  P  {}\mrightarrow{}  \mBbbP{}|  \mforall{}x:P.  (\mneg{}(s  x  x))\}  ].  \mforall{}[C:\mforall{}x,y,z:P.
                                                                                                                      ((Sep  x  y)  {}\mRightarrow{}  ((Sep  x  z)  \mvee{}  (Sep  y  z)))].
    (Point=P  \#=Sep  cotrans=C  \mmember{}  SeparationSpace)


By

---

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

---

Home Index