---

Step * 1 3 3 of Lemma permutation-s-group_wf

.....subterm..... T:t
5:n
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, 1:l} rv sepw ∈ ∀x,x',y,y':Point(permutation-ss(rv)).
                                                             ((λfg,fg'. let f,g = fg 
                                                                        in let f',g' = fg' 
                                                                           in <f o f', g' o g>) 
                                                              x 
                                                              y # (λfg,fg'. let f,g = fg 
                                                                            in let f',g' = fg' 
                                                                               in <f o f', g' o g>) 
                                                                  x' 
                                                                  y'
                                                             ⇒ (x # x' ∨ y # y'))
BY
{ Subst' TERMOF{permutation-s-group-sep-or:o, 1:l, 1:l} rv sepw ~ TERMOF{permutation-s-group-sep-or:o, 1:l, i:l} rv 
                                                                  sepw 0 }

1
.....equality..... 
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, 1:l} rv sepw ~ TERMOF{permutation-s-group-sep-or:o, 1:l, i:l} rv sepw

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
⊢ TERMOF{permutation-s-group-sep-or:o, 1:l, i:l} rv sepw ∈ ∀x,x',y,y':Point(permutation-ss(rv)).
                                                             ((λfg,fg'. let f,g = fg 
                                                                        in let f',g' = fg' 
                                                                           in <f o f', g' o g>) 
                                                              x 
                                                              y # (λfg,fg'. let f,g = fg 
                                                                            in let f',g' = fg' 
                                                                               in <f o f', g' o g>) 
                                                                  x' 
                                                                  y'
                                                             ⇒ (x # x' ∨ y # y'))

---

Latex:

---

Latex:
.....subterm.....  T:t
5:n
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,  1:l\}  rv  sepw  \mmember{}  \mforall{}x,x',y,y':Point(permutation-ss(rv)).
                                                                                                                          ((\mlambda{}fg,fg'.  let  f,g  =  fg 
                                                                                                                                                in  let  f',g'  =  fg' 
                                                                                                                                                      in  <f  o  f',  g'  o  g>) 
                                                                                                                            x 
                                                                                                                            y  \#  (\mlambda{}fg,fg'.  let  f,g  =  fg 
                                                                                                                                                        in  let  f',g'  =  fg' 
                                                                                                                                                              in  <f  o  f',  g'  o  g>) 
                                                                                                                                    x' 
                                                                                                                                    y'
                                                                                                                          {}\mRightarrow{}  (x  \#  x'  \mvee{}  y  \#  y'))


By

---

Latex:
Subst'  TERMOF\{permutation-s-group-sep-or:o,  1:l,  1:l\}  rv  sepw  \msim{}  TERMOF\{permutation-s-group-sep-or:o,
                                                                                                                                              1:l,
                                                                                                                                              i:l\} 
                                                                                                                                rv 
                                                                                                                                sepw  0

---

Home Index