---

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

.....subterm..... T:t
5:n
1. rv : SeparationSpace
2. <λx.x, λx.x> ∈ Point
3. λfg.let f,g = fg 
       in <g, f> ∈ Point ⟶ Point
4. λfg,fg'. let f,g = fg in let f',g' = fg' in <f o f', g' o g> ∈ Point ⟶ Point ⟶ Point
5. sepw : x:Point ⟶ y:{y:Point| x # y}  ⟶ x # y
⊢ λx,y,z,w,d. case d
              of inl(asep) =>
              let a,sep = asep 
              in inl inl <(fst(z)) a, sep>
              | inr(asep) =>
              let a,sep = asep 
              in inl (inr <a, sepw ((snd(x)) a) ((snd(y)) a)> ) ∈ ∀x,x',y,y':Point.
                                                 ((λ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' \000Cy
                                                 ⇒ (x # x' ∨ y # y'))
BY
{ (Reduce 0
   THEN RepeatFor 4 (((MemCD 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 (MemCD THENA Auto)
   THEN RepeatFor 2 (D -1)
   THEN Reduce 0) }

1
1. rv : SeparationSpace
2. <λx.x, λx.x> ∈ Point
3. λfg.let f,g = fg 
       in <g, f> ∈ Point ⟶ Point
4. λfg,fg'. let f,g = fg in let f',g' = fg' in <f o f', g' o g> ∈ Point ⟶ Point ⟶ Point
5. sepw : x:Point ⟶ y:{y:Point| x # y}  ⟶ x # y
6. x1 : Point ⟶ Point
7. x2 : Point ⟶ Point
8. (∀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))
9. y1 : Point ⟶ Point
10. y2 : Point ⟶ Point
11. (∀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))
12. z1 : Point ⟶ Point
13. z2 : Point ⟶ Point
14. (∀x:Point. z1 (z2 x) ≡ x)
∧ (∀x:Point. z2 (z1 x) ≡ x)
∧ (∀x,y:Point.  (z1 x # z1 y ⇒ x # y))
∧ (∀x,y:Point.  (z2 x # z2 y ⇒ x # y))
15. w1 : Point ⟶ Point
16. w2 : Point ⟶ Point
17. (∀x:Point. w1 (w2 x) ≡ x)
∧ (∀x:Point. w2 (w1 x) ≡ x)
∧ (∀x,y:Point.  (w1 x # w1 y ⇒ x # y))
∧ (∀x,y:Point.  (w2 x # w2 y ⇒ x # y))
18. a : Point
19. x3 : x1 (z1 a) # y1 (z1 a)
⊢ inl inl <z1 a, x3> ∈ ((∃a:Point. x1 a # y1 a) ∨ (∃a:Point. x2 a # y2 a)) ∨ (∃a:Point. z1 a # w1 a) ∨ (∃a:Point. z2 a #\000C w2 a)

2
1. rv : SeparationSpace
2. <λx.x, λx.x> ∈ Point
3. λfg.let f,g = fg 
       in <g, f> ∈ Point ⟶ Point
4. λfg,fg'. let f,g = fg in let f',g' = fg' in <f o f', g' o g> ∈ Point ⟶ Point ⟶ Point
5. sepw : x:Point ⟶ y:{y:Point| x # y}  ⟶ x # y
6. x1 : Point ⟶ Point
7. x2 : Point ⟶ Point
8. (∀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))
9. y1 : Point ⟶ Point
10. y2 : Point ⟶ Point
11. (∀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))
12. z1 : Point ⟶ Point
13. z2 : Point ⟶ Point
14. (∀x:Point. z1 (z2 x) ≡ x)
∧ (∀x:Point. z2 (z1 x) ≡ x)
∧ (∀x,y:Point.  (z1 x # z1 y ⇒ x # y))
∧ (∀x,y:Point.  (z2 x # z2 y ⇒ x # y))
15. w1 : Point ⟶ Point
16. w2 : Point ⟶ Point
17. (∀x:Point. w1 (w2 x) ≡ x)
∧ (∀x:Point. w2 (w1 x) ≡ x)
∧ (∀x,y:Point.  (w1 x # w1 y ⇒ x # y))
∧ (∀x,y:Point.  (w2 x # w2 y ⇒ x # y))
18. a : Point
19. y3 : z2 (x2 a) # z2 (y2 a)
⊢ inl (inr <a, sepw (x2 a) (y2 a)> ) ∈ ((∃a:Point. x1 a # y1 a) ∨ (∃a:Point. x2 a # y2 a))
  ∨ (∃a:Point. z1 a # w1 a)
  ∨ (∃a:Point. z2 a # w2 a)

---

Latex:

---

Latex:
.....subterm.....  T:t
5:n
1.  rv  :  SeparationSpace
2.  <\mlambda{}x.x,  \mlambda{}x.x>  \mmember{}  Point
3.  \mlambda{}fg.let  f,g  =  fg 
              in  <g,  f>  \mmember{}  Point  {}\mrightarrow{}  Point
4.  \mlambda{}fg,fg'.  let  f,g  =  fg  in  let  f',g'  =  fg'  in  <f  o  f',  g'  o  g>  \mmember{}  Point  {}\mrightarrow{}  Point  {}\mrightarrow{}  Point
5.  sepw  :  x:Point  {}\mrightarrow{}  y:\{y:Point|  x  \#  y\}    {}\mrightarrow{}  x  \#  y
\mvdash{}  \mlambda{}x,y,z,w,d.  case  d
                            of  inl(asep)  =>
                            let  a,sep  =  asep 
                            in  inl  inl  <(fst(z))  a,  sep>
                            |  inr(asep)  =>
                            let  a,sep  =  asep 
                            in  inl  (inr  <a,  sepw  ((snd(x))  a)  ((snd(y))  a)>  )  \mmember{}  \mforall{}x,x',y,y':Point.
                                                                                                  ((\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:
(Reduce  0
  THEN  RepeatFor  4  (((MemCD  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  (MemCD  THENA  Auto)
  THEN  RepeatFor  2  (D  -1)
  THEN  Reduce  0)

---

Home Index