---

Step * of Lemma permutation-s-group_wf

∀[rv:SeparationSpace]. ∀[sepw:∀x:Point. ∀y:{y:Point| x # y} .  x # y].  (Perm(rv) ∈ s-Group)
BY
{ (Intro
   THEN (Assert <λx.x, λx.x> ∈ Point BY
               ((RWO  "permutation-ss-point" 0 THENA Auto) THEN MemTypeCD THEN Reduce 0 THEN Auto))
   THEN (Assert λfg.let f,g = fg 
                    in <g, f> ∈ Point ⟶ Point BY
               ((MemCD THENA Auto)
                THEN (RWO  "permutation-ss-point" (-1) THENA Auto)
                THEN D -1
                THEN D -2
                THEN All Reduce
                THEN (RWO  "permutation-ss-point" 0 THENA Auto)
                THEN MemTypeCD
                THEN Reduce 0
                THEN Auto))) }

1
1. [rv] : SeparationSpace
2. <λx.x, λx.x> ∈ Point
3. λfg.let f,g = fg 
       in <g, f> ∈ Point ⟶ Point
⊢ ∀[sepw:∀x:Point. ∀y:{y:Point| x # y} .  x # y]. (Perm(rv) ∈ s-Group)

---

Latex:

---

Latex:
\mforall{}[rv:SeparationSpace].  \mforall{}[sepw:\mforall{}x:Point.  \mforall{}y:\{y:Point|  x  \#  y\}  .    x  \#  y].    (Perm(rv)  \mmember{}  s-Group)


By

---

Latex:
(Intro
  THEN  (Assert  <\mlambda{}x.x,  \mlambda{}x.x>  \mmember{}  Point  BY
                          ((RWO    "permutation-ss-point"  0  THENA  Auto)  THEN  MemTypeCD  THEN  Reduce  0  THEN  Auto))
  THEN  (Assert  \mlambda{}fg.let  f,g  =  fg 
                                    in  <g,  f>  \mmember{}  Point  {}\mrightarrow{}  Point  BY
                          ((MemCD  THENA  Auto)
                            THEN  (RWO    "permutation-ss-point"  (-1)  THENA  Auto)
                            THEN  D  -1
                            THEN  D  -2
                            THEN  All  Reduce
                            THEN  (RWO    "permutation-ss-point"  0  THENA  Auto)
                            THEN  MemTypeCD
                            THEN  Reduce  0
                            THEN  Auto)))

---

Home Index