---

Step * 2 of Lemma coWtransInvariant_wf


1. A : 𝕌'
2. B : A ⟶ Type
3. w1 : coW(A;a.B[a])
4. w2 : coW(A;a.B[a])
5. w3 : coW(A;a.B[a])
6. k : ℕ
7. X : win2strat(coW-game(a.B[a];w1;w2);k + 1)
8. Y : win2strat(coW-game(a.B[a];w2;w3);k + 1)
9. a : strat2play(coW-game(a.B[a];w1;w2);k;X)
10. b : strat2play(coW-game(a.B[a];w2;w3);k;Y)
11. m1 : sequence(Pos(coW-game(a.B[a];w1;w3)))
12. ((2 * k) + 2) ≤ ||m1||
13. v1 : copath(a.B[a];w1)
14. v2 : copath(a.B[a];w2)
15. a[(2 * k) + 1] = <v1, v2> ∈ Pos(coW-game(a.B[a];w1;w2))
16. v3 : copath(a.B[a];w2)
17. v4 : copath(a.B[a];w3)
18. b[(2 * k) + 1] = <v3, v4> ∈ Pos(coW-game(a.B[a];w2;w3))
19. ||a|| = ((2 * k) + 2) ∈ ℤ
20. ||b|| = ((2 * k) + 2) ∈ ℤ
21. m1[(2 * k) + 1] = <v1, v4> ∈ (copath(a.B[a];w1) × copath(a.B[a];w3))
⊢ fst((Y b)) ∈ copath(a.B[a];w2)
BY
{ ((InstLemma `win2strat-properties` [⌜coW-game(a.B[a];w2;w3)⌝;⌜k + 1⌝;⌜Y⌝]⋅ THENA Auto)
   THEN D -1
   THEN (GenConclTerm ⌜Y b⌝⋅ THENA Auto)
   THEN D -2
   THEN RepUR ``sg-pao coW-game`` -3
   THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  \mBbbU{}'
2.  B  :  A  {}\mrightarrow{}  Type
3.  w1  :  coW(A;a.B[a])
4.  w2  :  coW(A;a.B[a])
5.  w3  :  coW(A;a.B[a])
6.  k  :  \mBbbN{}
7.  X  :  win2strat(coW-game(a.B[a];w1;w2);k  +  1)
8.  Y  :  win2strat(coW-game(a.B[a];w2;w3);k  +  1)
9.  a  :  strat2play(coW-game(a.B[a];w1;w2);k;X)
10.  b  :  strat2play(coW-game(a.B[a];w2;w3);k;Y)
11.  m1  :  sequence(Pos(coW-game(a.B[a];w1;w3)))
12.  ((2  *  k)  +  2)  \mleq{}  ||m1||
13.  v1  :  copath(a.B[a];w1)
14.  v2  :  copath(a.B[a];w2)
15.  a[(2  *  k)  +  1]  =  <v1,  v2>
16.  v3  :  copath(a.B[a];w2)
17.  v4  :  copath(a.B[a];w3)
18.  b[(2  *  k)  +  1]  =  <v3,  v4>
19.  ||a||  =  ((2  *  k)  +  2)
20.  ||b||  =  ((2  *  k)  +  2)
21.  m1[(2  *  k)  +  1]  =  <v1,  v4>
\mvdash{}  fst((Y  b))  \mmember{}  copath(a.B[a];w2)


By

---

Latex:
((InstLemma  `win2strat-properties`  [\mkleeneopen{}coW-game(a.B[a];w2;w3)\mkleeneclose{};\mkleeneopen{}k  +  1\mkleeneclose{};\mkleeneopen{}Y\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  (GenConclTerm  \mkleeneopen{}Y  b\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  D  -2
  THEN  RepUR  ``sg-pao  coW-game``  -3
  THEN  Auto)

---

Home Index