---

Step * 1 1 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 : ℕ
19. (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)>)
BY
{ (FHyp (-7) [-1] THENA Auto) }

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 : ℕ
19. (2 * i) + 1 < ||f||
20. ↓Legal1(f[2 * i];f[(2 * i) + 1])
⊢ ↓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)>)

---

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.  i  :  \mBbbN{}
19.  (2  *  i)  +  1  <  ||f||
\mvdash{}  \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)>)


By

---

Latex:
(FHyp  (-7)  [-1]  THENA  Auto)

---

Home Index