---

Step * 1 3 3 2 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))
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))
5. sepw : x:Point(rv) ⟶ y:{y:Point(rv)| x # y}  ⟶ x # y
⊢ TERMOF{permutation-s-group-sep-or:o, 1:l, i:l} rv sepw ∈ ∀x,x',y,y':Point(permutation-ss(rv)).
                                                             (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
{ ((Assert ∀r1:SeparationSpace. ∀s1:x:Point(r1) ⟶ y:{y:Point(r1)| x # y}  ⟶ x # y.
             (∀x,x',y,y':Point(permutation-ss(r1)).
                (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 RepeatFor 4 (((MemCD THENW Auto)
                              THENL [Auto
                                    ; ((RWO  "permutation-ss-point" (-1) THENA Auto)
                                       THEN D -1
                                       THEN D -2
                                       THEN All Reduce)]
                             ))
           THEN RWO "permutation-ss-sep" 0
           THEN Auto))
   THEN GenConclTerm ⌜TERMOF{permutation-s-group-sep-or:o, 1:l, i:l}⌝⋅
   ) }

1
.....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))
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))
5. sepw : x:Point(rv) ⟶ y:{y:Point(rv)| x # y}  ⟶ x # y
6. ∀r1:SeparationSpace. ∀s1:x:Point(r1) ⟶ y:{y:Point(r1)| x # y}  ⟶ x # y.
     (∀x,x',y,y':Point(permutation-ss(r1)).
        (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')) ∈ ℙ)
⊢ TERMOF{permutation-s-group-sep-or:o, 1:l, i:l} ∈ ∀rv:SeparationSpace. ∀sepw:x:Point(rv)
                                                                              ⟶ y:{y:Point(rv)| x # y} 
                                                                              ⟶ x # y.
                                                   ∀x,x',y,y':Point(permutation-ss(rv)).
                                                     (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'))

2
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))
5. sepw : x:Point(rv) ⟶ y:{y:Point(rv)| x # y}  ⟶ x # y
6. ∀r1:SeparationSpace. ∀s1:x:Point(r1) ⟶ y:{y:Point(r1)| x # y}  ⟶ x # y.
     (∀x,x',y,y':Point(permutation-ss(r1)).
        (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')) ∈ ℙ)
7. v : ∀rv:SeparationSpace. ∀sepw:x:Point(rv) ⟶ y:{y:Point(rv)| x # y}  ⟶ x # y. ∀x,x',y,y':Point(permutation-ss(rv)).
         (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'))
8. TERMOF{permutation-s-group-sep-or:o, 1:l, i:l}
= v
∈ (∀rv:SeparationSpace. ∀sepw:x:Point(rv) ⟶ y:{y:Point(rv)| x # y}  ⟶ x # y. ∀x,x',y,y':Point(permutation-ss(rv)).
     (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')))
⊢ v rv sepw ∈ ∀x,x',y,y':Point(permutation-ss(rv)).
                (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'))

---

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))
4.  \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))
5.  sepw  :  x:Point(rv)  {}\mrightarrow{}  y:\{y:Point(rv)|  x  \#  y\}    {}\mrightarrow{}  x  \#  y
\mvdash{}  TERMOF\{permutation-s-group-sep-or:o,  1:l,  i:l\}  rv  sepw
    \mmember{}  \mforall{}x,x',y,y':Point(permutation-ss(rv)).
            (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:
((Assert  \mforall{}r1:SeparationSpace.  \mforall{}s1:x:Point(r1)  {}\mrightarrow{}  y:\{y:Point(r1)|  x  \#  y\}    {}\mrightarrow{}  x  \#  y.
                      (\mforall{}x,x',y,y':Point(permutation-ss(r1)).
                            (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'))  \mmember{}  \mBbbP{})  BY
                (RepeatFor  2  ((D  0  THENA  Auto))
                  THEN  RepeatFor  4  (((MemCD  THENW  Auto)
                                                        THENL  [Auto
                                                                    ;  ((RWO    "permutation-ss-point"  (-1)  THENA  Auto)
                                                                          THEN  D  -1
                                                                          THEN  D  -2
                                                                          THEN  All  Reduce)]
                                                      ))
                  THEN  RWO  "permutation-ss-sep"  0
                  THEN  Auto))
  THEN  GenConclTerm  \mkleeneopen{}TERMOF\{permutation-s-group-sep-or:o,  1:l,  i:l\}\mkleeneclose{}\mcdot{}
  )

---

Home Index