---

Step * 1 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))
⊢ ∃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]))
BY
{ ((D 0 With ⌜λp.((copath-length(fst(p)) = copath-length(snd(p)) ∈ ℤ)
                 ∧ (∃b':T
                     (seteq(copath-at(f b;fst(p));f b')
                     ∧ seteq(copath-at(regextfun(f;regextW(G;b));snd(p));regextfun(f;regextW(G;b'))))))⌝ 
    THENW (Auto
           THEN OnVar `p' \h. RepUR ``sg-pos coW-game`` h THEN D h
           THEN Reduce 0
           THEN Try (Unfold `coSet` 0)
           THEN Auto)
    )
   THEN RepUR ``so_apply`` 0
   THEN D 0) }

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))
⊢ (copath-length(fst(InitialPos(coW-game(T.T;f b;regextfun(f;regextW(G;b))))))
= copath-length(snd(InitialPos(coW-game(T.T;f b;regextfun(f;regextW(G;b))))))
∈ ℤ)
∧ (∃b':T
    (seteq(copath-at(f b;fst(InitialPos(coW-game(T.T;f b;regextfun(f;regextW(G;b))))));f b')
    ∧ seteq(copath-at(regextfun(f;regextW(G;b));snd(InitialPos(coW-game(T.T;f 
                                                                            b;regextfun(f;regextW(G;b))))));...)))

2
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))
⊢ ∀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:(copath-length(fst(p)) = copath-length(snd(p)) ∈ ℤ)
      ∧ (∃b':T
          (seteq(copath-at(f b;fst(p));f b')
          ∧ seteq(copath-at(regextfun(f;regextW(G;b));snd(p));regextfun(f;regextW(G;b'))))).
    ∃r:{r:Pos(coW-game(T.T;f b;regextfun(f;regextW(G;b))))| Legal2(q;r)} 
     ((copath-length(fst(r)) = copath-length(snd(r)) ∈ ℤ)
     ∧ (∃b':T
         (seteq(copath-at(f b;fst(r));f b')
         ∧ seteq(copath-at(regextfun(f;regextW(G;b));snd(r));regextfun(f;regextW(G;b'))))))

---

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{}  \mexists{}Good:Pos(coW-game(T.T;f  b;regextfun(f;regextW(G;b))))  {}\mrightarrow{}  \mBbbP{}'
      (Good[InitialPos(coW-game(T.T;f  b;regextfun(f;regextW(G;b))))]
      \mwedge{}  (\mforall{}p:Pos(coW-game(T.T;f  b;regextfun(f;regextW(G;b)))).
            \mforall{}q:\{q:Pos(coW-game(T.T;f  b;regextfun(f;regextW(G;b))))|  Legal1(p;q)\}  .  \mforall{}gd:Good[p].
                \mexists{}r:\{r:Pos(coW-game(T.T;f  b;regextfun(f;regextW(G;b))))|  Legal2(q;r)\}  .  Good[r]))


By

---

Latex:
((D  0  With  \mkleeneopen{}\mlambda{}p....\mkleeneclose{} 
    THENW  (Auto
                  THEN  OnVar  `p'  \mbackslash{}h.  RepUR  ``sg-pos  coW-game``  h  THEN  D  h
                  THEN  Reduce  0
                  THEN  Try  (Unfold  `coSet`  0)
                  THEN  Auto)
    )
  THEN  RepUR  ``so\_apply``  0
  THEN  D  0)

---

Home Index