---

Step * 1 3 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))
⊢ ∀[sepw:∀x:Point(rv). ∀y:{y:Point(rv)| x # y} .  x # y]. (Perm(rv) ∈ s-Group)
BY
{ ((D 0 THENA Auto) THEN Unfold `all` -1 THEN Unfold `permutation-s-group` 0 THEN MemCD THEN Try (Trivial)) }

1
.....subterm..... T:t
1: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
⊢ permutation-ss(rv) ∈ SeparationSpace

2
.....subterm..... T:t
4: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
⊢ λfg,fg'. let f,g = fg in let f',g' = fg' in <f o f', g' o g> ∈ {f:Point(permutation-ss(rv))
                                                           ⟶ Point(permutation-ss(rv))
                                                           ⟶ Point(permutation-ss(rv))| 
                                                           (∀x,y,z:Point(permutation-ss(rv)).
                                                              f x (f y z) ≡ f (f x y) z)
                                                           ∧ (∀x:Point(permutation-ss(rv)). f x <λx.x, λx.x> ≡ x)
                                                           ∧ (∀x:Point(permutation-ss(rv))
                                                                f x ((λfg.let f,g = fg in <g, f>) x) ≡ <λx.x, λx.x>)} 

3
.....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'))

4
.....subterm..... T:t
6: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
⊢ λx,y,d. case d of inl(asep) => inr asep  | inr(asep) => inl asep ∈ ∀x,y:Point(permutation-ss(rv)).
                                                                 ((λfg.let f,g = fg in <g, f>) x # (λfg.let f,g = fg 
                                                                                                        in <g, f>) 
                                                                                                   y
                                                                 ⇒ x # 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))
\mvdash{}  \mforall{}[sepw:\mforall{}x:Point(rv).  \mforall{}y:\{y:Point(rv)|  x  \#  y\}  .    x  \#  y].  (Perm(rv)  \mmember{}  s-Group)


By

---

Latex:
((D  0  THENA  Auto)
  THEN  Unfold  `all`  -1
  THEN  Unfold  `permutation-s-group`  0
  THEN  MemCD
  THEN  Try  (Trivial))

---

Home Index