---

Step * 3 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. g : Point
6. y : Point
7. L1 : Point List
8. (∀f∈L1.P[f])
9. g ≡ reduce(λx,y. (x y);1;L1)
10. L : Point List
11. (∀f∈L.P[f])
12. y ≡ reduce(λx,y. (x y);1;L)
⊢ ∃L:Point List. ((∀f∈L.P[f]) ∧ (g y) ≡ reduce(λx,y. (x y);1;L))
BY
{ ((D 0 With ⌜L1 @ L⌝  THEN Auto) THEN RWW "reduce-append l_all_append" 0 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. g : Point
6. y : Point
7. L1 : Point List
8. (∀f∈L1.P[f])
9. g ≡ reduce(λx,y. (x y);1;L1)
10. L : Point List
11. (∀f∈L.P[f])
12. y ≡ reduce(λx,y. (x y);1;L)
13. (∀f∈L1 @ L.P[f])
⊢ (g y) ≡ reduce(λx,y. (x y);reduce(λx,y. (x y);1;L);L1)

---

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.  g  :  Point
6.  y  :  Point
7.  L1  :  Point  List
8.  (\mforall{}f\mmember{}L1.P[f])
9.  g  \mequiv{}  reduce(\mlambda{}x,y.  (x  y);1;L1)
10.  L  :  Point  List
11.  (\mforall{}f\mmember{}L.P[f])
12.  y  \mequiv{}  reduce(\mlambda{}x,y.  (x  y);1;L)
\mvdash{}  \mexists{}L:Point  List.  ((\mforall{}f\mmember{}L.P[f])  \mwedge{}  (g  y)  \mequiv{}  reduce(\mlambda{}x,y.  (x  y);1;L))


By

---

Latex:
((D  0  With  \mkleeneopen{}L1  @  L\mkleeneclose{}    THEN  Auto)  THEN  RWW  "reduce-append  l\_all\_append"  0  THEN  Auto)

---

Home Index