---

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


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)
BY
{ Assert ⌜x2 a # y2 a⌝⋅ }

1
.....assertion..... 
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)
⊢ x2 a # y2 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)
20. x2 a # 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:

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
6.  x1  :  Point  {}\mrightarrow{}  Point
7.  x2  :  Point  {}\mrightarrow{}  Point
8.  (\mforall{}x:Point.  x1  (x2  x)  \mequiv{}  x)
\mwedge{}  (\mforall{}x:Point.  x2  (x1  x)  \mequiv{}  x)
\mwedge{}  (\mforall{}x,y:Point.    (x1  x  \#  x1  y  {}\mRightarrow{}  x  \#  y))
\mwedge{}  (\mforall{}x,y:Point.    (x2  x  \#  x2  y  {}\mRightarrow{}  x  \#  y))
9.  y1  :  Point  {}\mrightarrow{}  Point
10.  y2  :  Point  {}\mrightarrow{}  Point
11.  (\mforall{}x:Point.  y1  (y2  x)  \mequiv{}  x)
\mwedge{}  (\mforall{}x:Point.  y2  (y1  x)  \mequiv{}  x)
\mwedge{}  (\mforall{}x,y:Point.    (y1  x  \#  y1  y  {}\mRightarrow{}  x  \#  y))
\mwedge{}  (\mforall{}x,y:Point.    (y2  x  \#  y2  y  {}\mRightarrow{}  x  \#  y))
12.  z1  :  Point  {}\mrightarrow{}  Point
13.  z2  :  Point  {}\mrightarrow{}  Point
14.  (\mforall{}x:Point.  z1  (z2  x)  \mequiv{}  x)
\mwedge{}  (\mforall{}x:Point.  z2  (z1  x)  \mequiv{}  x)
\mwedge{}  (\mforall{}x,y:Point.    (z1  x  \#  z1  y  {}\mRightarrow{}  x  \#  y))
\mwedge{}  (\mforall{}x,y:Point.    (z2  x  \#  z2  y  {}\mRightarrow{}  x  \#  y))
15.  w1  :  Point  {}\mrightarrow{}  Point
16.  w2  :  Point  {}\mrightarrow{}  Point
17.  (\mforall{}x:Point.  w1  (w2  x)  \mequiv{}  x)
\mwedge{}  (\mforall{}x:Point.  w2  (w1  x)  \mequiv{}  x)
\mwedge{}  (\mforall{}x,y:Point.    (w1  x  \#  w1  y  {}\mRightarrow{}  x  \#  y))
\mwedge{}  (\mforall{}x,y:Point.    (w2  x  \#  w2  y  {}\mRightarrow{}  x  \#  y))
18.  a  :  Point
19.  y3  :  z2  (x2  a)  \#  z2  (y2  a)
\mvdash{}  inl  (inr  <a,  sepw  (x2  a)  (y2  a)>  )  \mmember{}  ((\mexists{}a:Point.  x1  a  \#  y1  a)  \mvee{}  (\mexists{}a:Point.  x2  a  \#  y2  a))
    \mvee{}  (\mexists{}a:Point.  z1  a  \#  w1  a)
    \mvee{}  (\mexists{}a:Point.  z2  a  \#  w2  a)


By

---

Latex:
Assert  \mkleeneopen{}x2  a  \#  y2  a\mkleeneclose{}\mcdot{}

---

Home Index