---

Step * 1 1 1 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||
20. v1 : copath(a.B[a];coW-item(w;t))
21. v2 : copath(a.B[a];coW-item(w';b))
22. v3 : copath(a.B[a];coW-item(w;t))
23. v4 : copath(a.B[a];coW-item(w';b))
⊢ Legal1(<v1, v2>;<v3, v4>)
⇒ Legal1(let u,v = <v1, v2> 
          in <copath-cons(t;u), copath-cons(b;v)>;let u,v = <v3, v4> 
                                                  in <copath-cons(t;u), copath-cons(b;v)>)
BY
{ ((RepUR ``sg-legal1 coW-game`` 0 THEN (D 0 THENA Auto))
   THEN ParallelLast
   THEN RWO "length-copath-cons" 0
   THEN Auto
   THEN BLemma `copathAgree-cons`
   THEN Auto) }

---

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||
20.  v1  :  copath(a.B[a];coW-item(w;t))
21.  v2  :  copath(a.B[a];coW-item(w';b))
22.  v3  :  copath(a.B[a];coW-item(w;t))
23.  v4  :  copath(a.B[a];coW-item(w';b))
\mvdash{}  Legal1(<v1,  v2><v3,  v4>)
{}\mRightarrow{}  Legal1(let  u,v  =  <v1,  v2> 
                    in  <copath-cons(t;u),  copath-cons(b;v)>let  u,v  =  <v3,  v4> 
                                                                                                    in  <copath-cons(t;u),  copath-cons(b;v)>)


By

---

Latex:
((RepUR  ``sg-legal1  coW-game``  0  THEN  (D  0  THENA  Auto))
  THEN  ParallelLast
  THEN  RWO  "length-copath-cons"  0
  THEN  Auto
  THEN  BLemma  `copathAgree-cons`
  THEN  Auto)

---

Home Index