---

Step * 1 2 of Lemma coW-game-step-isom


1. A : 𝕌'
2. B : A ⟶ Type
3. w : coW(A;a.B[a])
4. w' : coW(A;a.B[a])
5. t : coW-dom(a.B[a];w)
6. b : coW-dom(a.B[a];w')
7. p1 : copath(a.B[a];coW-item(w;t))
8. p2 : copath(a.B[a];coW-item(w';b))
9. f : sequence(Pos(coW-game(a.B[a];coW-item(w;t);coW-item(w';b))))
10. 0 < ||f||
11. f[0] = <(), ()> ∈ Pos(coW-game(a.B[a];coW-item(w;t);coW-item(w';b)))
12. f[||f|| - 1] = <p1, p2> ∈ Pos(coW-game(a.B[a];coW-item(w;t);coW-item(w';b)))
13. ∀i:ℕ. ((2 * i) + 1 < ||f|| ⇒ (↓Legal1(f[2 * i];f[(2 * i) + 1])))
14. ∀i:ℕ+. (2 * i < ||f|| ⇒ (↓Legal2(f[(2 * i) - 1];f[2 * i])))
15. 0 < ||f||
16. let u,v = f[0] 
    in <copath-cons(t;u), copath-cons(b;v)>
= <copath-cons(t;()), copath-cons(b;())>
∈ Pos(coW-game(a.B[a];w;w'))
17. let u,v = f[||f|| - 1] 
    in <copath-cons(t;u), copath-cons(b;v)>
= <copath-cons(t;p1), copath-cons(b;p2)>
∈ Pos(coW-game(a.B[a];w;w'))
18. ∀i:ℕ
      ((2 * i) + 1 < ||f||
      ⇒ (↓Legal1(let u,v = f[2 * i] 
                  in <copath-cons(t;u), copath-cons(b;v)>;let u,v = f[(2 * i) + 1] 
                                                          in <copath-cons(t;u), copath-cons(b;v)>)))
19. i : ℕ+
20. 2 * i < ||f||
⊢ ↓Legal2(let u,v = f[(2 * i) - 1] 
          in <copath-cons(t;u), copath-cons(b;v)>;let u,v = f[2 * i] 
                                                  in <copath-cons(t;u), copath-cons(b;v)>)
BY
{ ((FHyp (-7) [-1] THENA Auto)
   THEN ParallelLast
   THEN MoveToConcl (-1)
   THEN ((GenConclTerm ⌜f[2 * i]⌝⋅ THENA Auto) THEN Thin (-1) THEN RepUR ``sg-pos coW-game`` -1 THEN D -1)
   THEN (GenConclTerm ⌜f[(2 * i) - 1]⌝⋅ THENA Auto)
   THEN Thin (-1)
   THEN RepUR ``sg-pos coW-game`` -1
   THEN D -1) }

1
1. A : 𝕌'
2. B : A ⟶ Type
3. w : coW(A;a.B[a])
4. w' : coW(A;a.B[a])
5. t : coW-dom(a.B[a];w)
6. b : coW-dom(a.B[a];w')
7. p1 : copath(a.B[a];coW-item(w;t))
8. p2 : copath(a.B[a];coW-item(w';b))
9. f : sequence(Pos(coW-game(a.B[a];coW-item(w;t);coW-item(w';b))))
10. 0 < ||f||
11. f[0] = <(), ()> ∈ Pos(coW-game(a.B[a];coW-item(w;t);coW-item(w';b)))
12. f[||f|| - 1] = <p1, p2> ∈ Pos(coW-game(a.B[a];coW-item(w;t);coW-item(w';b)))
13. ∀i:ℕ. ((2 * i) + 1 < ||f|| ⇒ (↓Legal1(f[2 * i];f[(2 * i) + 1])))
14. ∀i:ℕ+. (2 * i < ||f|| ⇒ (↓Legal2(f[(2 * i) - 1];f[2 * i])))
15. 0 < ||f||
16. let u,v = f[0] 
    in <copath-cons(t;u), copath-cons(b;v)>
= <copath-cons(t;()), copath-cons(b;())>
∈ Pos(coW-game(a.B[a];w;w'))
17. let u,v = f[||f|| - 1] 
    in <copath-cons(t;u), copath-cons(b;v)>
= <copath-cons(t;p1), copath-cons(b;p2)>
∈ Pos(coW-game(a.B[a];w;w'))
18. ∀i:ℕ
      ((2 * i) + 1 < ||f||
      ⇒ (↓Legal1(let u,v = f[2 * i] 
                  in <copath-cons(t;u), copath-cons(b;v)>;let u,v = f[(2 * i) + 1] 
                                                          in <copath-cons(t;u), copath-cons(b;v)>)))
19. i : ℕ+
20. 2 * i < ||f||
21. v1 : copath(a.B[a];coW-item(w;t))
22. v2 : copath(a.B[a];coW-item(w';b))
23. v3 : copath(a.B[a];coW-item(w;t))
24. v4 : copath(a.B[a];coW-item(w';b))
⊢ Legal2(<v3, v4>;<v1, v2>) ⇒ Legal2(let u,v = <v3, v4> in <copath-cons(t;u), copath-cons(b;v)>;let u,v = <v1, v2> in <\000Ccopath-cons(t;u), copath-cons(b;v)>)

---

Latex:

---

Latex:

1.  A  :  \mBbbU{}'
2.  B  :  A  {}\mrightarrow{}  Type
3.  w  :  coW(A;a.B[a])
4.  w'  :  coW(A;a.B[a])
5.  t  :  coW-dom(a.B[a];w)
6.  b  :  coW-dom(a.B[a];w')
7.  p1  :  copath(a.B[a];coW-item(w;t))
8.  p2  :  copath(a.B[a];coW-item(w';b))
9.  f  :  sequence(Pos(coW-game(a.B[a];coW-item(w;t);coW-item(w';b))))
10.  0  <  ||f||
11.  f[0]  =  <(),  ()>
12.  f[||f||  -  1]  =  <p1,  p2>
13.  \mforall{}i:\mBbbN{}.  ((2  *  i)  +  1  <  ||f||  {}\mRightarrow{}  (\mdownarrow{}Legal1(f[2  *  i];f[(2  *  i)  +  1])))
14.  \mforall{}i:\mBbbN{}\msupplus{}.  (2  *  i  <  ||f||  {}\mRightarrow{}  (\mdownarrow{}Legal2(f[(2  *  i)  -  1];f[2  *  i])))
15.  0  <  ||f||
16.  let  u,v  =  f[0]  in  <copath-cons(t;u),  copath-cons(b;v)>  =  <copath-cons(t;()),  copath-cons(b;())>
17.  let  u,v  =  f[||f||  -  1] 
        in  <copath-cons(t;u),  copath-cons(b;v)>
=  <copath-cons(t;p1),  copath-cons(b;p2)>
18.  \mforall{}i:\mBbbN{}
            ((2  *  i)  +  1  <  ||f||
            {}\mRightarrow{}  (\mdownarrow{}Legal1(let  u,v  =  f[2  *  i] 
                                    in  <copath-cons(t;u),  copath-cons(b;v)>let  u,v  =  f[(2  *  i)  +  1] 
                                                                                                                    in  <copath-cons(t;u),  copath-cons(b;v)>)))
19.  i  :  \mBbbN{}\msupplus{}
20.  2  *  i  <  ||f||
\mvdash{}  \mdownarrow{}Legal2(let  u,v  =  f[(2  *  i)  -  1] 
                    in  <copath-cons(t;u),  copath-cons(b;v)>let  u,v  =  f[2  *  i] 
                                                                                                    in  <copath-cons(t;u),  copath-cons(b;v)>)


By

---

Latex:
((FHyp  (-7)  [-1]  THENA  Auto)
  THEN  ParallelLast
  THEN  MoveToConcl  (-1)
  THEN  ((GenConclTerm  \mkleeneopen{}f[2  *  i]\mkleeneclose{}\mcdot{}  THENA  Auto)
              THEN  Thin  (-1)
              THEN  RepUR  ``sg-pos  coW-game``  -1
              THEN  D  -1)
  THEN  (GenConclTerm  \mkleeneopen{}f[(2  *  i)  -  1]\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Thin  (-1)
  THEN  RepUR  ``sg-pos  coW-game``  -1
  THEN  D  -1)

---

Home Index