---

Step * 1 1 of Lemma permutation-s-group_wf

.....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
BY
{ ((Assert ∀x,y:Point(rv).  (x ≡ y ⇒ f1 x ≡ f1 y) BY
          (ParallelOp 8 THEN ParallelLast THEN RepeatFor 2 ((D 0 THENA Auto)) THEN D -2 THEN BHyp -2 THEN Auto))
   THEN (Assert f1 (f2 x) ≡ x BY
               Auto)
   THEN InstHyp [⌜f3 (f4 (f2 x))⌝;⌜f2 x⌝] (-2)⋅
   THEN Auto) }

---

Latex:

---

Latex:
.....aux..... 
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))
4.  f1  :  Point(rv)  {}\mrightarrow{}  Point(rv)
5.  f2  :  Point(rv)  {}\mrightarrow{}  Point(rv)
6.  \mforall{}x:Point(rv).  f1  (f2  x)  \mequiv{}  x
7.  \mforall{}x:Point(rv).  f2  (f1  x)  \mequiv{}  x
8.  \mforall{}x,y:Point(rv).    (f1  x  \#  f1  y  {}\mRightarrow{}  x  \#  y)
9.  \mforall{}x,y:Point(rv).    (f2  x  \#  f2  y  {}\mRightarrow{}  x  \#  y)
10.  f3  :  Point(rv)  {}\mrightarrow{}  Point(rv)
11.  f4  :  Point(rv)  {}\mrightarrow{}  Point(rv)
12.  \mforall{}x:Point(rv).  f3  (f4  x)  \mequiv{}  x
13.  \mforall{}x:Point(rv).  f4  (f3  x)  \mequiv{}  x
14.  \mforall{}x,y:Point(rv).    (f3  x  \#  f3  y  {}\mRightarrow{}  x  \#  y)
15.  \mforall{}x,y:Point(rv).    (f4  x  \#  f4  y  {}\mRightarrow{}  x  \#  y)
16.  x  :  Point(rv)
\mvdash{}  f1  (f3  (f4  (f2  x)))  \mequiv{}  x


By

---

Latex:
((Assert  \mforall{}x,y:Point(rv).    (x  \mequiv{}  y  {}\mRightarrow{}  f1  x  \mequiv{}  f1  y)  BY
                (ParallelOp  8
                  THEN  ParallelLast
                  THEN  RepeatFor  2  ((D  0  THENA  Auto))
                  THEN  D  -2
                  THEN  BHyp  -2
                  THEN  Auto))
  THEN  (Assert  f1  (f2  x)  \mequiv{}  x  BY
                          Auto)
  THEN  InstHyp  [\mkleeneopen{}f3  (f4  (f2  x))\mkleeneclose{};\mkleeneopen{}f2  x\mkleeneclose{}]  (-2)\mcdot{}
  THEN  Auto)

---

Home Index