---

Step * of Lemma permutation-s-group-sep-or

∀rv:SeparationSpace. ∀sepw:x:Point ⟶ y:{y:Point| x # y}  ⟶ x # y. ∀x,x',y,y':Point.
  (let f,g = x 
   in let f',g' = y 
      in <f o f', g' o g> # let f,g = x' 
                            in let f',g' = y' 
                               in <f o f', g' o g>
  ⇒ (x # x' ∨ y # y'))
BY
{ (RepeatFor 2 ((D 0 THENA Auto))
   THEN (Assert ∀a,b:Point.  SqStable(a # b) BY
               (Auto THEN (D 0 THENA Auto) THEN UseWitness ⌜sepw a b⌝⋅ THEN Auto))
   THEN RepeatFor 4 (((D 0 THENA Auto)
                      THEN (RWO  "permutation-ss-point" (-1) THENA Auto)
                      THEN D -1
                      THEN D -2
                      THEN All Reduce))
   THEN (RWO "permutation-ss-sep" 0 THENA Auto)
   THEN RepUR ``fun-sep`` 0
   THEN (D 0 THENA Auto)
   THEN D -1
   THEN ExRepD) }

1
1. rv : SeparationSpace
2. sepw : x:Point ⟶ y:{y:Point| x # y}  ⟶ x # y
3. ∀a,b:Point.  SqStable(a # b)
4. x1 : Point ⟶ Point
5. x2 : Point ⟶ Point
6. [%2] : (∀x:Point. x1 (x2 x) ≡ x)
∧ (∀x:Point. x2 (x1 x) ≡ x)
∧ (∀x,y:Point.  (x1 x # x1 y ⇒ x # y))
∧ (∀x,y:Point.  (x2 x # x2 y ⇒ x # y))
7. x3 : Point ⟶ Point
8. x4 : Point ⟶ Point
9. [%3] : (∀x:Point. x3 (x4 x) ≡ x)
∧ (∀x:Point. x4 (x3 x) ≡ x)
∧ (∀x,y:Point.  (x3 x # x3 y ⇒ x # y))
∧ (∀x,y:Point.  (x4 x # x4 y ⇒ x # y))
10. y1 : Point ⟶ Point
11. y2 : Point ⟶ Point
12. [%4] : (∀x:Point. y1 (y2 x) ≡ x)
∧ (∀x:Point. y2 (y1 x) ≡ x)
∧ (∀x,y:Point.  (y1 x # y1 y ⇒ x # y))
∧ (∀x,y:Point.  (y2 x # y2 y ⇒ x # y))
13. y3 : Point ⟶ Point
14. y4 : Point ⟶ Point
15. [%5] : (∀x:Point. y3 (y4 x) ≡ x)
∧ (∀x:Point. y4 (y3 x) ≡ x)
∧ (∀x,y:Point.  (y3 x # y3 y ⇒ x # y))
∧ (∀x,y:Point.  (y4 x # y4 y ⇒ x # y))
16. a : Point
17. x1 (y1 a) # x3 (y3 a)
⊢ ((∃a:Point. x1 a # x3 a) ∨ (∃a:Point. x2 a # x4 a)) ∨ (∃a:Point. y1 a # y3 a) ∨ (∃a:Point. y2 a # y4 a)

2
1. rv : SeparationSpace
2. sepw : x:Point ⟶ y:{y:Point| x # y}  ⟶ x # y
3. ∀a,b:Point.  SqStable(a # b)
4. x1 : Point ⟶ Point
5. x2 : Point ⟶ Point
6. [%2] : (∀x:Point. x1 (x2 x) ≡ x)
∧ (∀x:Point. x2 (x1 x) ≡ x)
∧ (∀x,y:Point.  (x1 x # x1 y ⇒ x # y))
∧ (∀x,y:Point.  (x2 x # x2 y ⇒ x # y))
7. x3 : Point ⟶ Point
8. x4 : Point ⟶ Point
9. [%3] : (∀x:Point. x3 (x4 x) ≡ x)
∧ (∀x:Point. x4 (x3 x) ≡ x)
∧ (∀x,y:Point.  (x3 x # x3 y ⇒ x # y))
∧ (∀x,y:Point.  (x4 x # x4 y ⇒ x # y))
10. y1 : Point ⟶ Point
11. y2 : Point ⟶ Point
12. [%4] : (∀x:Point. y1 (y2 x) ≡ x)
∧ (∀x:Point. y2 (y1 x) ≡ x)
∧ (∀x,y:Point.  (y1 x # y1 y ⇒ x # y))
∧ (∀x,y:Point.  (y2 x # y2 y ⇒ x # y))
13. y3 : Point ⟶ Point
14. y4 : Point ⟶ Point
15. [%5] : (∀x:Point. y3 (y4 x) ≡ x)
∧ (∀x:Point. y4 (y3 x) ≡ x)
∧ (∀x,y:Point.  (y3 x # y3 y ⇒ x # y))
∧ (∀x,y:Point.  (y4 x # y4 y ⇒ x # y))
16. a : Point
17. y2 (x2 a) # y4 (x4 a)
⊢ ((∃a:Point. x1 a # x3 a) ∨ (∃a:Point. x2 a # x4 a)) ∨ (∃a:Point. y1 a # y3 a) ∨ (∃a:Point. y2 a # y4 a)

---

Latex:

---

Latex:
\mforall{}rv:SeparationSpace.  \mforall{}sepw:x:Point  {}\mrightarrow{}  y:\{y:Point|  x  \#  y\}    {}\mrightarrow{}  x  \#  y.  \mforall{}x,x',y,y':Point.
    (let  f,g  =  x 
      in  let  f',g'  =  y 
            in  <f  o  f',  g'  o  g>  \#  let  f,g  =  x' 
                                                        in  let  f',g'  =  y' 
                                                              in  <f  o  f',  g'  o  g>
    {}\mRightarrow{}  (x  \#  x'  \mvee{}  y  \#  y'))


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))
  THEN  (Assert  \mforall{}a,b:Point.    SqStable(a  \#  b)  BY
                          (Auto  THEN  (D  0  THENA  Auto)  THEN  UseWitness  \mkleeneopen{}sepw  a  b\mkleeneclose{}\mcdot{}  THEN  Auto))
  THEN  RepeatFor  4  (((D  0  THENA  Auto)
                                        THEN  (RWO    "permutation-ss-point"  (-1)  THENA  Auto)
                                        THEN  D  -1
                                        THEN  D  -2
                                        THEN  All  Reduce))
  THEN  (RWO  "permutation-ss-sep"  0  THENA  Auto)
  THEN  RepUR  ``fun-sep``  0
  THEN  (D  0  THENA  Auto)
  THEN  D  -1
  THEN  ExRepD)

---

Home Index