---

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

.....set predicate..... 
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. sg-reachable(coW-game(a.B[a];coW-item(w;t);coW-item(w';b));InitialPos(coW-game(a.B[a];coW-item(w;t);...));<p1, p2>)
⊢ sg-reachable(coW-game(a.B[a];w;w');<copath-cons(t;()), copath-cons(b;())>;<copath-cons(t;p1), copath-cons(b;p2)>)
BY
{ (((Subst' InitialPos(coW-game(a.B[a];coW-item(w;t);coW-item(w';b))) ~ <(), ()> -1 THENA Computation) THEN ParallelLast\000C THEN ExRepD)
   THEN (D 0 With ⌜λp.let u,v = p in <copath-cons(t;u), copath-cons(b;v)> o f⌝  THENW Auto)
   THEN (RWW  "seq-comp-len seq-comp-item" 0 THENA Auto)
   THEN Reduce 0
   THEN Auto
   THEN Try (((RWO  "-5" 0 THENA Auto) THEN RepUR ``sg-pos coW-game`` 0 THEN EqCD THEN 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||
⊢ ↓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)>)

2
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)>)

---

Latex:

---

Latex:
.....set  predicate..... 
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.  sg-reachable(coW-game(a.B[a];coW-item(w;t);coW-item(w';b));InitialPos(...);<p1,  p2>)
\mvdash{}  sg-reachable(coW-game(a.B[a];w;w');<copath-cons(t;()),  copath-cons(b;())><copath-cons(t;p1),  copa\000Cth-cons(b;p2)>)


By

---

Latex:
(((Subst'  InitialPos(coW-game(a.B[a];coW-item(w;t);coW-item(w';b)))  \msim{}  <(),  ()>  -1  THENA  Computation)\000C  THEN  ParallelLast  THEN  ExRepD)
  THEN  (D  0  With  \mkleeneopen{}\mlambda{}p.let  u,v  =  p  in  <copath-cons(t;u),  copath-cons(b;v)>  o  f\mkleeneclose{}    THENW  Auto)
  THEN  (RWW    "seq-comp-len  seq-comp-item"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  Auto
  THEN  Try  (((RWO    "-5"  0  THENA  Auto)  THEN  RepUR  ``sg-pos  coW-game``  0  THEN  EqCD  THEN  Auto)))

---

Home Index