---

Step * 2 2 1 2 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
⊢ (a^-1 (u reduce(λx,y. (x y);1;v)))^-1 ≡ reduce(λx,y. (x y);a;rev(map(λf.f^-1;v)) @ [u^-1])
BY
{ ((RWW "reduce-append sg-inv-id sg-id-op" 0 THEN Auto)
   THEN Reduce 0
   THEN (RWO "-2<" 0 THENA Auto)
   THEN (GenConclTerm ⌜reduce(λx,y. (x y);1;v)⌝⋅ THENA Auto)) }

1
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
⊢ (a^-1 (u v1))^-1 ≡ ((u^-1 a)^-1 v1)^-1

---

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
\mvdash{}  (a\^{}-1  (u  reduce(\mlambda{}x,y.  (x  y);1;v)))\^{}-1  \mequiv{}  reduce(\mlambda{}x,y.  (x  y);a;rev(map(\mlambda{}f.f\^{}-1;v))  @  [u\^{}-1])


By

---

Latex:
((RWW  "reduce-append  sg-inv-id  sg-id-op"  0  THEN  Auto)
  THEN  Reduce  0
  THEN  (RWO  "-2<"  0  THENA  Auto)
  THEN  (GenConclTerm  \mkleeneopen{}reduce(\mlambda{}x,y.  (x  y);1;v)\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index