---

Step * of Lemma coWtransInvariant_wf

∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w1,w2,w3:coW(A;a.B[a])]. ∀[k:ℕ]. ∀[X:win2strat(coW-game(a.B[a];w1;w2);k + 1)].
∀[Y:win2strat(coW-game(a.B[a];w2;w3);k + 1)]. ∀[a:strat2play(coW-game(a.B[a];w1;w2);k;X)].
∀[b:strat2play(coW-game(a.B[a];w2;w3);k;Y)]. ∀[m1:sequence(Pos(coW-game(a.B[a];w1;w3)))].
  coWtransInvariant(a.B[a];w1;w2;w3;k;X;Y;a;b;m1) ∈ ℙ supposing ((2 * k) + 2) ≤ ||m1||
BY
{ (Auto
   THEN Unfold `coWtransInvariant` 0
   THEN (GenConclTerm ⌜a[(2 * k) + 1]⌝⋅ THENA Auto)
   THEN RepUR ``sg-pos coW-game`` -2
   THEN D -2
   THEN (GenConclTerm ⌜b[(2 * k) + 1]⌝⋅ THENA Auto)
   THEN (RepUR ``sg-pos coW-game`` -2 THEN D -2)
   THEN RepUR ``sg-pos coW-game`` 0
   THEN Reduce 0
   THEN Auto) }

1
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))
⊢ snd((X a)) ∈ copath(a.B[a];w2)

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

---

Latex:

---

Latex:
\mforall{}[A:\mBbbU{}'].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[w1,w2,w3:coW(A;a.B[a])].  \mforall{}[k:\mBbbN{}].  \mforall{}[X:win2strat(coW-game(a.B[a];w1;w2);k
                                                                                                                                +  1)].
\mforall{}[Y:win2strat(coW-game(a.B[a];w2;w3);k  +  1)].  \mforall{}[a:strat2play(coW-game(a.B[a];w1;w2);k;X)].
\mforall{}[b:strat2play(coW-game(a.B[a];w2;w3);k;Y)].  \mforall{}[m1:sequence(Pos(coW-game(a.B[a];w1;w3)))].
    coWtransInvariant(a.B[a];w1;w2;w3;k;X;Y;a;b;m1)  \mmember{}  \mBbbP{}  supposing  ((2  *  k)  +  2)  \mleq{}  ||m1||


By

---

Latex:
(Auto
  THEN  Unfold  `coWtransInvariant`  0
  THEN  (GenConclTerm  \mkleeneopen{}a[(2  *  k)  +  1]\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  RepUR  ``sg-pos  coW-game``  -2
  THEN  D  -2
  THEN  (GenConclTerm  \mkleeneopen{}b[(2  *  k)  +  1]\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (RepUR  ``sg-pos  coW-game``  -2  THEN  D  -2)
  THEN  RepUR  ``sg-pos  coW-game``  0
  THEN  Reduce  0
  THEN  Auto)

---

Home Index