---

Step * 1 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))
⊢ (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))))));...)))
BY
{ (RepUR ``sg-init coW-game`` 0
   THEN D 0
   THEN ((Fold `member` 0 THEN Auto)
   ORELSE (D 0 With ⌜b⌝  THEN Auto THEN Try ((BLemma `seteq_weakening` THEN Auto)) THEN Unfold `coSet` 0 THEN Auto)
   )) }

---

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{}  (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)))))))
\mwedge{}  (\mexists{}b':T
        (seteq(copath-at(f  b;fst(InitialPos(coW-game(T.T;f  b;regextfun(f;regextW(G;b))))));f  b')
        \mwedge{}  seteq(copath-at(regextfun(f;regextW(G;b));snd(InitialPos(coW-game(T.T;f 
                                                                                                                                                        b;...))));...)))


By

---

Latex:
(RepUR  ``sg-init  coW-game``  0
  THEN  D  0
  THEN  ((Fold  `member`  0  THEN  Auto)
  ORELSE  (D  0  With  \mkleeneopen{}b\mkleeneclose{} 
                  THEN  Auto
                  THEN  Try  ((BLemma  `seteq\_weakening`  THEN  Auto))
                  THEN  Unfold  `coSet`  0
                  THEN  Auto)
  ))

---

Home Index