---

Step * 2 2 1 2 1 1 of Lemma generated-s-subgroup_wf


1. sg : s-Group
2. u : Point
3. v : Point List
4. ∀a:Point. (a^-1 reduce(λx,y. (x y);1;v))^-1 ≡ reduce(λx,y. (x y);a;rev(map(λf.f^-1;v)))
5. a : Point
6. v1 : Point
7. reduce(λx,y. (x y);1;v) = v1 ∈ Point
⊢ ((v1^-1 u^-1) a) ≡ (v1^-1 (u^-1 a))
BY
{ (RWO "sg-assoc" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  sg  :  s-Group
2.  u  :  Point
3.  v  :  Point  List
4.  \mforall{}a:Point.  (a\^{}-1  reduce(\mlambda{}x,y.  (x  y);1;v))\^{}-1  \mequiv{}  reduce(\mlambda{}x,y.  (x  y);a;rev(map(\mlambda{}f.f\^{}-1;v)))
5.  a  :  Point
6.  v1  :  Point
7.  reduce(\mlambda{}x,y.  (x  y);1;v)  =  v1
\mvdash{}  ((v1\^{}-1  u\^{}-1)  a)  \mequiv{}  (v1\^{}-1  (u\^{}-1  a))


By

---

Latex:
(RWO  "sg-assoc"  0  THEN  Auto)

---

Home Index