---

Step * of Lemma coW-play-invariant

∀[A:𝕌']
  ∀B:A ⟶ Type. ∀w,w':coW(A;a.B[a]). ∀n:ℕ. ∀s:win2strat(coW-game(a.B[a];w;w');n).
  ∀moves:strat2play(coW-game(a.B[a];w;w');n;s). ∀i:ℕ.
    (((i ≤ n)
    ⇒ (coW-pos-lens(moves[2 * i];i;i)
       ∧ (coW-pos-lens(moves[(2 * i) + 1];i;i + 1) ∨ coW-pos-lens(moves[(2 * i) + 1];i + 1;i))))
    ∧ ((i ≤ ((2 * n) + 1)) ⇒ (∀j:ℕi + 1. coW-pos-agree(a.B[a];w;w';moves[j];moves[i]))))
BY
{ (RepeatFor 7 ((D 0 THENA Auto))
   THEN (Strat2PlayInvariant (-1) THENA Auto)
   THEN D -1
   THEN (D 0 THENA Auto)
   THEN NatInd (-1)) }

1
.....basecase..... 
1. [A] : 𝕌'
2. B : A ⟶ Type
3. w : coW(A;a.B[a])
4. w' : coW(A;a.B[a])
5. n : ℕ
6. s : win2strat(coW-game(a.B[a];w;w');n)
7. moves : strat2play(coW-game(a.B[a];w;w');n;s)
8. moves[0] = InitialPos(coW-game(a.B[a];w;w')) ∈ Pos(coW-game(a.B[a];w;w'))
9. ∀i:ℕn + 1
     ((↓Legal1(moves[2 * i];moves[(2 * i) + 1]))
     ∧ (i < n
       ⇒ ((↓Legal2(moves[(2 * i) + 1];moves[2 * (i + 1)]))
          ∧ (moves[2 * (i + 1)] = (s play-truncate(moves;2 * (i + 1))) ∈ Pos(coW-game(a.B[a];w;w'))))))
⊢ ((0 ≤ n)
⇒ (coW-pos-lens(moves[2 * 0];0;0)
   ∧ (coW-pos-lens(moves[(2 * 0) + 1];0;0 + 1) ∨ coW-pos-lens(moves[(2 * 0) + 1];0 + 1;0))))
∧ ((0 ≤ ((2 * n) + 1)) ⇒ (∀j:ℕ0 + 1. coW-pos-agree(a.B[a];w;w';moves[j];moves[0])))

2
.....upcase..... 
1. [A] : 𝕌'
2. B : A ⟶ Type
3. w : coW(A;a.B[a])
4. w' : coW(A;a.B[a])
5. n : ℕ
6. s : win2strat(coW-game(a.B[a];w;w');n)
7. moves : strat2play(coW-game(a.B[a];w;w');n;s)
8. moves[0] = InitialPos(coW-game(a.B[a];w;w')) ∈ Pos(coW-game(a.B[a];w;w'))
9. ∀i:ℕn + 1
     ((↓Legal1(moves[2 * i];moves[(2 * i) + 1]))
     ∧ (i < n
       ⇒ ((↓Legal2(moves[(2 * i) + 1];moves[2 * (i + 1)]))
          ∧ (moves[2 * (i + 1)] = (s play-truncate(moves;2 * (i + 1))) ∈ Pos(coW-game(a.B[a];w;w'))))))
10. i : ℤ
11. [%4] : 0 < i
12. (((i - 1) ≤ n)
⇒ (coW-pos-lens(moves[2 * (i - 1)];i - 1;i - 1)
   ∧ (coW-pos-lens(moves[(2 * (i - 1)) + 1];i - 1;(i - 1) + 1)
     ∨ coW-pos-lens(moves[(2 * (i - 1)) + 1];(i - 1) + 1;i - 1))))
∧ (((i - 1) ≤ ((2 * n) + 1)) ⇒ (∀j:ℕ(i - 1) + 1. coW-pos-agree(a.B[a];w;w';moves[j];moves[i - 1])))
⊢ ((i ≤ n)
⇒ (coW-pos-lens(moves[2 * i];i;i)
   ∧ (coW-pos-lens(moves[(2 * i) + 1];i;i + 1) ∨ coW-pos-lens(moves[(2 * i) + 1];i + 1;i))))
∧ ((i ≤ ((2 * n) + 1)) ⇒ (∀j:ℕi + 1. coW-pos-agree(a.B[a];w;w';moves[j];moves[i])))

---

Latex:

---

Latex:
\mforall{}[A:\mBbbU{}']
    \mforall{}B:A  {}\mrightarrow{}  Type.  \mforall{}w,w':coW(A;a.B[a]).  \mforall{}n:\mBbbN{}.  \mforall{}s:win2strat(coW-game(a.B[a];w;w');n).
    \mforall{}moves:strat2play(coW-game(a.B[a];w;w');n;s).  \mforall{}i:\mBbbN{}.
        (((i  \mleq{}  n)
        {}\mRightarrow{}  (coW-pos-lens(moves[2  *  i];i;i)
              \mwedge{}  (coW-pos-lens(moves[(2  *  i)  +  1];i;i  +  1)  \mvee{}  coW-pos-lens(moves[(2  *  i)  +  1];i  +  1;i))))
        \mwedge{}  ((i  \mleq{}  ((2  *  n)  +  1))  {}\mRightarrow{}  (\mforall{}j:\mBbbN{}i  +  1.  coW-pos-agree(a.B[a];w;w';moves[j];moves[i]))))


By

---

Latex:
(RepeatFor  7  ((D  0  THENA  Auto))
  THEN  (Strat2PlayInvariant  (-1)  THENA  Auto)
  THEN  D  -1
  THEN  (D  0  THENA  Auto)
  THEN  NatInd  (-1))

---

Home Index