---

Step * of Lemma list-ss_wf

∀[ss:SeparationSpace]. (list(ss) ∈ SeparationSpace)
BY
{ (Auto
   THEN Unfold `list-ss` 0
   THEN MemCD
   THEN Try ((MemTypeCD
              THEN Auto
              THEN Reduce 0
              THEN Auto
              THEN (D 0 THENA Auto)
              THEN D -1
              THEN MoveToConcl (-1)
              THEN Fold `not` 0
              THEN Auto))
   THEN Reduce 0
   THEN RepeatFor 3 ((MemCD THENA Auto))
   THEN Auto
   THEN All Reduce
   THEN ExRepD
   THEN Reduce 0
   THEN Auto
   THEN (Assert ss ∈ SeparationSpace BY
               Auto)
   THEN (D 1 THENA Auto)
   THEN All (Folds ``ss-sep ss-point``)
   THEN Try ((GenConclAtAddr [2;1] THEN (D -2 THEN Reduce 0) THEN MemCD THEN Auto))
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[ss:SeparationSpace].  (list(ss)  \mmember{}  SeparationSpace)


By

---

Latex:
(Auto
  THEN  Unfold  `list-ss`  0
  THEN  MemCD
  THEN  Try  ((MemTypeCD
                        THEN  Auto
                        THEN  Reduce  0
                        THEN  Auto
                        THEN  (D  0  THENA  Auto)
                        THEN  D  -1
                        THEN  MoveToConcl  (-1)
                        THEN  Fold  `not`  0
                        THEN  Auto))
  THEN  Reduce  0
  THEN  RepeatFor  3  ((MemCD  THENA  Auto))
  THEN  Auto
  THEN  All  Reduce
  THEN  ExRepD
  THEN  Reduce  0
  THEN  Auto
  THEN  (Assert  ss  \mmember{}  SeparationSpace  BY
                          Auto)
  THEN  (D  1  THENA  Auto)
  THEN  All  (Folds  ``ss-sep  ss-point``)
  THEN  Try  ((GenConclAtAddr  [2;1]  THEN  (D  -2  THEN  Reduce  0)  THEN  MemCD  THEN  Auto))
  THEN  Auto)

---

Home Index