---

Step * 2 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)
8. (∀f∈rev(map(λf.f^-1;L)).P[f])
⊢ g^-1 ≡ reduce(λx,y. (x y);1;rev(map(λf.f^-1;L)))
BY
{ Assert ⌜∀a:Point. (a^-1 reduce(λx,y. (x y);1;L))^-1 ≡ reduce(λx,y. (x y);a;rev(map(λf.f^-1;L)))⌝⋅ }

1
.....assertion..... 
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])
⊢ ∀a:Point. (a^-1 reduce(λx,y. (x y);1;L))^-1 ≡ reduce(λx,y. (x y);a;rev(map(λf.f^-1;L)))

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])
9. ∀a:Point. (a^-1 reduce(λx,y. (x y);1;L))^-1 ≡ reduce(λx,y. (x y);a;rev(map(λf.f^-1;L)))
⊢ 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)
8.  (\mforall{}f\mmember{}rev(map(\mlambda{}f.f\^{}-1;L)).P[f])
\mvdash{}  g\^{}-1  \mequiv{}  reduce(\mlambda{}x,y.  (x  y);1;rev(map(\mlambda{}f.f\^{}-1;L)))


By

---

Latex:
Assert  \mkleeneopen{}\mforall{}a:Point.  (a\^{}-1  reduce(\mlambda{}x,y.  (x  y);1;L))\^{}-1  \mequiv{}  reduce(\mlambda{}x,y.  (x  y);a;rev(map(\mlambda{}f.f\^{}-1;L)))\mkleeneclose{}\mcdot{}

---

Home Index