---

Step * 1 1 1 1 of Lemma subset-co-regext


1. T : Type
2. f : T ⟶ coSet{i:l}
3. ∀i:T. ∀i@0:set-dom(f i).  ∃b:T. seteq(set-item(f i;i@0);f b)
4. b : T@i
5. G : i:T ⟶ i@0:set-dom(f i) ⟶ T
6. ∀i:T. ∀i@0:set-dom(f i).  seteq(set-item(f i;i@0);f (G i i@0))
⊢ seteq(f b;regextfun(f;regextW(G;b)))
BY
{ (Unfold `seteq` 0 THEN Unfold `coW-equiv` 0 THEN (BLemma `good-sg-win2` THENW Auto)) }

1
1. T : Type
2. f : T ⟶ coSet{i:l}
3. ∀i:T. ∀i@0:set-dom(f i).  ∃b:T. seteq(set-item(f i;i@0);f b)
4. b : T@i
5. G : i:T ⟶ i@0:set-dom(f i) ⟶ T
6. ∀i:T. ∀i@0:set-dom(f i).  seteq(set-item(f i;i@0);f (G i i@0))
⊢ ∃Good:Pos(coW-game(T.T;f b;regextfun(f;regextW(G;b)))) ⟶ ℙ'
   (Good[InitialPos(coW-game(T.T;f b;regextfun(f;regextW(G;b))))]
   ∧ (∀p:Pos(coW-game(T.T;f b;regextfun(f;regextW(G;b)))). ∀q:{q:Pos(coW-game(T.T;f b;regextfun(f;regextW(G;b))))| 
                                                               Legal1(p;q)} . ∀gd:Good[p].
        ∃r:{r:Pos(coW-game(T.T;f b;regextfun(f;regextW(G;b))))| Legal2(q;r)} . Good[r]))

---

Latex:

---

Latex:

1.  T  :  Type
2.  f  :  T  {}\mrightarrow{}  coSet\{i:l\}
3.  \mforall{}i:T.  \mforall{}i@0:set-dom(f  i).    \mexists{}b:T.  seteq(set-item(f  i;i@0);f  b)
4.  b  :  T@i
5.  G  :  i:T  {}\mrightarrow{}  i@0:set-dom(f  i)  {}\mrightarrow{}  T
6.  \mforall{}i:T.  \mforall{}i@0:set-dom(f  i).    seteq(set-item(f  i;i@0);f  (G  i  i@0))
\mvdash{}  seteq(f  b;regextfun(f;regextW(G;b)))


By

---

Latex:
(Unfold  `seteq`  0  THEN  Unfold  `coW-equiv`  0  THEN  (BLemma  `good-sg-win2`  THENW  Auto))

---

Home Index