Step * 1 1 of Lemma sg-id-op


1. sg s-Group
2. Point
3. (x x^-1) ≡ 1
4. (x^-1 x^-1^-1) ≡ 1
⊢ (((x x^-1) x) (x^-1 x^-1^-1)) ≡ x
BY
(RWO "sg-assoc<THENA Auto) }

1
1. sg s-Group
2. Point
3. (x x^-1) ≡ 1
4. (x^-1 x^-1^-1) ≡ 1
⊢ ((x x^-1) (x (x^-1 x^-1^-1))) ≡ x


Latex:


Latex:

1.  sg  :  s-Group
2.  x  :  Point
3.  (x  x\^{}-1)  \mequiv{}  1
4.  (x\^{}-1  x\^{}-1\^{}-1)  \mequiv{}  1
\mvdash{}  (((x  x\^{}-1)  x)  (x\^{}-1  x\^{}-1\^{}-1))  \mequiv{}  x


By


Latex:
(RWO  "sg-assoc<"  0  THENA  Auto)




Home Index