---

Step * 2 1 of Lemma generated-s-subgroup_wf


1. sg : s-Group
2. P : Point ⟶ ℙ
3. ∀f:Point. (P[f] ⇒ P[f^-1])
4. g : Point
5. L : Point List
6. (∀f∈L.P[f])
7. g ≡ reduce(λx,y. (x y);1;L)
⊢ (∀f∈rev(map(λf.f^-1;L)).P[f])
BY
{ (((RWW "l_all_reverse l_all_map" 0 THENA Auto) THEN Reduce 0)
   THEN (All (RWO "l_all_iff")  THEN Auto)
   THEN (RWO "member-map" (-1) THENA Auto)
   THEN (Reduce -1 THEN ExRepD)
   THEN RWO "-1" 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  sg  :  s-Group
2.  P  :  Point  {}\mrightarrow{}  \mBbbP{}
3.  \mforall{}f:Point.  (P[f]  {}\mRightarrow{}  P[f\^{}-1])
4.  g  :  Point
5.  L  :  Point  List
6.  (\mforall{}f\mmember{}L.P[f])
7.  g  \mequiv{}  reduce(\mlambda{}x,y.  (x  y);1;L)
\mvdash{}  (\mforall{}f\mmember{}rev(map(\mlambda{}f.f\^{}-1;L)).P[f])


By

---

Latex:
(((RWW  "l\_all\_reverse  l\_all\_map"  0  THENA  Auto)  THEN  Reduce  0)
  THEN  (All  (RWO  "l\_all\_iff")    THEN  Auto)
  THEN  (RWO  "member-map"  (-1)  THENA  Auto)
  THEN  (Reduce  -1  THEN  ExRepD)
  THEN  RWO  "-1"  0
  THEN  Auto)

---

Home Index