---

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

.....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>)} 
BY
{ ((MemTypeCD THENW Auto)
   THEN Try (Trivial)
   THEN Reduce 0
   THEN SplitAndConcl
   THEN Repeat ((Intro THEN (RWO  "permutation-ss-point" (-1) THENA Auto) THEN D -1 THEN D -2 THEN All Reduce))
   THEN BLemma `permutation-ss-eq-iff`
   THEN Auto
   THEN RepUR ``compose`` 0
   THEN Auto) }

---

Latex:

---

Latex:
.....subterm.....  T:t
4: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{}  \mlambda{}fg,fg'.  let  f,g  =  fg  in  let  f',g'  =  fg'  in  <f  o  f',  g'  o  g>  \mmember{}  \{f:Point(permutation-ss(rv))
                                                                                                                      {}\mrightarrow{}  Point(permutation-ss(rv))
                                                                                                                      {}\mrightarrow{}  Point(permutation-ss(rv))| 
                                                                                                                      (\mforall{}x,y,z:Point(permutation-ss(rv)).
                                                                                                                            f  x  (f  y  z)  \mequiv{}  f  (f  x  y)  z)
                                                                                                                      \mwedge{}  (\mforall{}x:Point(permutation-ss(rv))
                                                                                                                                f  x  <\mlambda{}x.x,  \mlambda{}x.x>  \mequiv{}  x)
                                                                                                                      \mwedge{}  (\mforall{}x:Point(permutation-ss(rv))
                                                                                                                                f  x 
                                                                                                                                ((\mlambda{}fg.let  f,g  =  fg 
                                                                                                                                            in  <g,  f>) 
                                                                                                                                  x)  \mequiv{}  <\mlambda{}x.x,  \mlambda{}x.x>)\} 


By

---

Latex:
((MemTypeCD  THENW  Auto)
  THEN  Try  (Trivial)
  THEN  Reduce  0
  THEN  SplitAndConcl
  THEN  Repeat  ((Intro
                              THEN  (RWO    "permutation-ss-point"  (-1)  THENA  Auto)
                              THEN  D  -1
                              THEN  D  -2
                              THEN  All  Reduce))
  THEN  BLemma  `permutation-ss-eq-iff`
  THEN  Auto
  THEN  RepUR  ``compose``  0
  THEN  Auto)

---

Home Index