---

Step * 2 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)
⊢ ∃L:Point List. ((∀f∈L.P[f]) ∧ g^-1 ≡ reduce(λx,y. (x y);1;L))
BY
{ (D 0 With ⌜rev(map(λf.f^-1;L))⌝  THEN Auto) }

1
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])

2
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)
8. (∀f∈rev(map(λf.f^-1;L)).P[f])
⊢ g^-1 ≡ reduce(λx,y. (x y);1;rev(map(λf.f^-1;L)))

---

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{}  \mexists{}L:Point  List.  ((\mforall{}f\mmember{}L.P[f])  \mwedge{}  g\^{}-1  \mequiv{}  reduce(\mlambda{}x,y.  (x  y);1;L))


By

---

Latex:
(D  0  With  \mkleeneopen{}rev(map(\mlambda{}f.f\^{}-1;L))\mkleeneclose{}    THEN  Auto)

---

Home Index