---

Step * 1 of Lemma permutation-s-group_wf


1. [rv] : SeparationSpace
2. <λx.x, λx.x> ∈ Point(permutation-ss(rv))
3. λfg.let f,g = fg 
       in <g, f> ∈ Point(permutation-ss(rv)) ⟶ Point(permutation-ss(rv))
⊢ ∀[sepw:∀x:Point(rv). ∀y:{y:Point(rv)| x # y} .  x # y]. (Perm(rv) ∈ s-Group)
BY
{ (Assert λfg,fg'. let f,g = fg in let f',g' = fg' in <f o f', g' o g> ∈ Point(permutation-ss(rv))
          ⟶ Point(permutation-ss(rv))
          ⟶ Point(permutation-ss(rv)) BY
         (RepeatFor 2 (((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
          THEN EAuto 1)) }

1
.....aux..... 
1. rv : SeparationSpace
2. <λx.x, λx.x> ∈ Point(permutation-ss(rv))
3. λfg.let f,g = fg 
       in <g, f> ∈ Point(permutation-ss(rv)) ⟶ Point(permutation-ss(rv))
4. f1 : Point(rv) ⟶ Point(rv)
5. f2 : Point(rv) ⟶ Point(rv)
6. ∀x:Point(rv). f1 (f2 x) ≡ x
7. ∀x:Point(rv). f2 (f1 x) ≡ x
8. ∀x,y:Point(rv).  (f1 x # f1 y ⇒ x # y)
9. ∀x,y:Point(rv).  (f2 x # f2 y ⇒ x # y)
10. f3 : Point(rv) ⟶ Point(rv)
11. f4 : Point(rv) ⟶ Point(rv)
12. ∀x:Point(rv). f3 (f4 x) ≡ x
13. ∀x:Point(rv). f4 (f3 x) ≡ x
14. ∀x,y:Point(rv).  (f3 x # f3 y ⇒ x # y)
15. ∀x,y:Point(rv).  (f4 x # f4 y ⇒ x # y)
16. x : Point(rv)
⊢ f1 (f3 (f4 (f2 x))) ≡ x

2
.....aux..... 
1. rv : SeparationSpace
2. <λx.x, λx.x> ∈ Point(permutation-ss(rv))
3. λfg.let f,g = fg 
       in <g, f> ∈ Point(permutation-ss(rv)) ⟶ Point(permutation-ss(rv))
4. f1 : Point(rv) ⟶ Point(rv)
5. f2 : Point(rv) ⟶ Point(rv)
6. ∀x:Point(rv). f1 (f2 x) ≡ x
7. ∀x:Point(rv). f2 (f1 x) ≡ x
8. ∀x,y:Point(rv).  (f1 x # f1 y ⇒ x # y)
9. ∀x,y:Point(rv).  (f2 x # f2 y ⇒ x # y)
10. f3 : Point(rv) ⟶ Point(rv)
11. f4 : Point(rv) ⟶ Point(rv)
12. ∀x:Point(rv). f3 (f4 x) ≡ x
13. ∀x:Point(rv). f4 (f3 x) ≡ x
14. ∀x,y:Point(rv).  (f3 x # f3 y ⇒ x # y)
15. ∀x,y:Point(rv).  (f4 x # f4 y ⇒ x # y)
16. ∀x:Point(rv). f1 (f3 (f4 (f2 x))) ≡ x
17. x : Point(rv)
⊢ f4 (f2 (f1 (f3 x))) ≡ x

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

---

Latex:

---

Latex:

1.  [rv]  :  SeparationSpace
2.  <\mlambda{}x.x,  \mlambda{}x.x>  \mmember{}  Point(permutation-ss(rv))
3.  \mlambda{}fg.let  f,g  =  fg 
              in  <g,  f>  \mmember{}  Point(permutation-ss(rv))  {}\mrightarrow{}  Point(permutation-ss(rv))
\mvdash{}  \mforall{}[sepw:\mforall{}x:Point(rv).  \mforall{}y:\{y:Point(rv)|  x  \#  y\}  .    x  \#  y].  (Perm(rv)  \mmember{}  s-Group)


By

---

Latex:
(Assert  \mlambda{}fg,fg'.  let  f,g  =  fg  in  let  f',g'  =  fg'  in  <f  o  f',  g'  o  g>  \mmember{}  Point(permutation-ss(rv))
                {}\mrightarrow{}  Point(permutation-ss(rv))
                {}\mrightarrow{}  Point(permutation-ss(rv))  BY
              (RepeatFor  2  (((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
                THEN  EAuto  1))

---

Home Index