---

Step * 3 1 1 1 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
     ((∃L:Point List. ((∀f∈L.P[f]) ∧ g ≡ reduce(λx,y. (x y);1;L)))
     ⇒ (∃L:Point List. ((∀f∈L.P[f]) ∧ g^-1 ≡ reduce(λx,y. (x y);1;L))))
5. u : Point
6. v : Point List
7. ∀y,v@0:Point.  (y ≡ v@0 ⇒ (reduce(λx,y. (x y);1;v) y) ≡ reduce(λx,y. (x y);v@0;v))
⊢ ∀y,v@0:Point.  (y ≡ v@0 ⇒ ((u reduce(λx,y. (x y);1;v)) y) ≡ (u reduce(λx,y. (x y);v@0;v)))
BY
{ (RepeatFor 3 (ParallelLast) THEN (RWO "-1<" 0 THENA Auto) THEN GenConclTerm ⌜reduce(λx,y. (x y);1;v)⌝⋅ THEN Auto) }

1
1. sg : s-Group
2. P : Point ⟶ ℙ
3. ∀f:Point. (P[f] ⇒ P[f^-1])
4. ∀g:Point
     ((∃L:Point List. ((∀f∈L.P[f]) ∧ g ≡ reduce(λx,y. (x y);1;L)))
     ⇒ (∃L:Point List. ((∀f∈L.P[f]) ∧ g^-1 ≡ reduce(λx,y. (x y);1;L))))
5. u : Point
6. v : Point List
7. ∀y,v@0:Point.  (y ≡ v@0 ⇒ (reduce(λx,y. (x y);1;v) y) ≡ reduce(λx,y. (x y);v@0;v))
8. y : Point
9. ∀v@0:Point. (y ≡ v@0 ⇒ (reduce(λx,y. (x y);1;v) y) ≡ reduce(λx,y. (x y);v@0;v))
10. v@0 : Point
11. y ≡ v@0
12. (reduce(λx,y. (x y);1;v) y) ≡ reduce(λx,y. (x y);v@0;v)
13. v1 : Point
14. reduce(λx,y. (x y);1;v) = v1 ∈ Point
⊢ ((u v1) y) ≡ (u (v1 y))

---

Latex:

---

Latex:

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


By

---

Latex:
(RepeatFor  3  (ParallelLast)
  THEN  (RWO  "-1<"  0  THENA  Auto)
  THEN  GenConclTerm  \mkleeneopen{}reduce(\mlambda{}x,y.  (x  y);1;v)\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index