---

Step * 1 1 1 1 1 2 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))
7. p : Pos(coW-game(T.T;f b;regextfun(f;regextW(G;b))))@i
8. q : {q:Pos(coW-game(T.T;f b;regextfun(f;regextW(G;b))))| Legal1(p;q)} @i
9. 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')))))@i
⊢ ∃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'))))))
BY
{ (D -2
   THEN (((Assert Legal1(p;q) BY (Unhide THEN Auto)) THEN Thin (-3)) THEN ExRepD)
   THEN All (RepUR ``sg-pos coW-game sg-legal1 sg-legal2``)
   THEN DProds
   THEN All Reduce
   THEN D -1
   THEN ExRepD) }

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))
7. p1 : copath(T.T;f b)@i
8. p2 : copath(T.T;regextfun(f;regextW(G;b)))@i
9. q1 : copath(T.T;f b)@i
10. q2 : copath(T.T;regextfun(f;regextW(G;b)))@i
11. g1 : copath-length(p1) = copath-length(p2) ∈ ℤ@i
12. b' : T@i
13. g4 : seteq(copath-at(f b;p1);f b')@i
14. g5 : seteq(copath-at(regextfun(f;regextW(G;b));p2);regextfun(f;regextW(G;b')))@i
15. copath-length(q1) = (copath-length(p1) + 1) ∈ ℤ
16. copathAgree(T.T;f b;p1;q1)
17. p2 = q2 ∈ copath(T.T;regextfun(f;regextW(G;b)))
⊢ ∃r:{r:copath(T.T;f b) × copath(T.T;regextfun(f;regextW(G;b)))| 
      let u',v' = r 
      in (((copath-length(u') = (copath-length(q1) + 1) ∈ ℤ)
         ∧ copathAgree(T.T;f b;q1;u')
         ∧ (q2 = v' ∈ copath(T.T;regextfun(f;regextW(G;b)))))
         ∨ ((q1 = u' ∈ copath(T.T;f b))
           ∧ (copath-length(v') = (copath-length(q2) + 1) ∈ ℤ)
           ∧ copathAgree(T.T;regextfun(f;regextW(G;b));q2;v')))
         ∧ (copath-length(u') = copath-length(v') ∈ ℤ)} 
   ((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'))))))

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))
7. p1 : copath(T.T;f b)@i
8. p2 : copath(T.T;regextfun(f;regextW(G;b)))@i
9. q1 : copath(T.T;f b)@i
10. q2 : copath(T.T;regextfun(f;regextW(G;b)))@i
11. g1 : copath-length(p1) = copath-length(p2) ∈ ℤ@i
12. b' : T@i
13. g4 : seteq(copath-at(f b;p1);f b')@i
14. g5 : seteq(copath-at(regextfun(f;regextW(G;b));p2);regextfun(f;regextW(G;b')))@i
15. p1 = q1 ∈ copath(T.T;f b)
16. copath-length(q2) = (copath-length(p2) + 1) ∈ ℤ
17. copathAgree(T.T;regextfun(f;regextW(G;b));p2;q2)
⊢ ∃r:{r:copath(T.T;f b) × copath(T.T;regextfun(f;regextW(G;b)))| 
      let u',v' = r 
      in (((copath-length(u') = (copath-length(q1) + 1) ∈ ℤ)
         ∧ copathAgree(T.T;f b;q1;u')
         ∧ (q2 = v' ∈ copath(T.T;regextfun(f;regextW(G;b)))))
         ∨ ((q1 = u' ∈ copath(T.T;f b))
           ∧ (copath-length(v') = (copath-length(q2) + 1) ∈ ℤ)
           ∧ copathAgree(T.T;regextfun(f;regextW(G;b));q2;v')))
         ∧ (copath-length(u') = copath-length(v') ∈ ℤ)} 
   ((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))
7.  p  :  Pos(coW-game(T.T;f  b;regextfun(f;regextW(G;b))))@i
8.  q  :  \{q:Pos(coW-game(T.T;f  b;regextfun(f;regextW(G;b))))|  Legal1(p;q)\}  @i
9.  gd  :  (copath-length(fst(p))  =  copath-length(snd(p)))
\mwedge{}  (\mexists{}b':T
        (seteq(copath-at(f  b;fst(p));f  b')
        \mwedge{}  seteq(copath-at(regextfun(f;regextW(G;b));snd(p));regextfun(f;regextW(G;b')))))@i
\mvdash{}  \mexists{}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)))
      \mwedge{}  (\mexists{}b':T
              (seteq(copath-at(f  b;fst(r));f  b')
              \mwedge{}  seteq(copath-at(regextfun(f;regextW(G;b));snd(r));regextfun(f;regextW(G;b'))))))


By

---

Latex:
(D  -2
  THEN  (((Assert  Legal1(p;q)  BY  (Unhide  THEN  Auto))  THEN  Thin  (-3))  THEN  ExRepD)
  THEN  All  (RepUR  ``sg-pos  coW-game  sg-legal1  sg-legal2``)
  THEN  DProds
  THEN  All  Reduce
  THEN  D  -1
  THEN  ExRepD)

---

Home Index