---

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

.....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
BY
{ ((Assert ∀x,y:Point.  (z2 x # z2 y ⇒ x # y) BY (SplitAndHyps THEN Trivial)) THEN BHyp -1  THEN Auto) }

---

Latex:

---

Latex:
.....assertion..... 
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{}  x2  a  \#  y2  a


By

---

Latex:
((Assert  \mforall{}x,y:Point.    (z2  x  \#  z2  y  {}\mRightarrow{}  x  \#  y)  BY
                (SplitAndHyps  THEN  Trivial))
  THEN  BHyp  -1 
  THEN  Auto)

---

Home Index