---

Step * of Lemma coW-game-reachable

∀[A:𝕌']
  ∀B:A ⟶ Type. ∀w,w':coW(A;a.B[a]). ∀p,q:Pos(coW-game(a.B[a];w;w')).
    (sg-reachable(coW-game(a.B[a];w;w');p;q) ⇒ coW-pos-agree(a.B[a];w;w';p;q))
BY
{ ((Auto THEN D -1)
   THEN ExRepD
   THEN (RWO "-4<" 0 THENA Auto)
   THEN (RWO "-3<" 0 THENA Auto)
   THEN ThinVar `p'
   THEN ThinVar `q') }

1
1. [A] : 𝕌'
2. B : A ⟶ Type
3. w : coW(A;a.B[a])
4. w' : coW(A;a.B[a])
5. f : sequence(Pos(coW-game(a.B[a];w;w')))
6. 0 < ||f||
7. ∀i:ℕ. ((2 * i) + 1 < ||f|| ⇒ (↓Legal1(f[2 * i];f[(2 * i) + 1])))
8. ∀i:ℕ+. (2 * i < ||f|| ⇒ (↓Legal2(f[(2 * i) - 1];f[2 * i])))
⊢ coW-pos-agree(a.B[a];w;w';f[0];f[||f|| - 1])

---

Latex:

---

Latex:
\mforall{}[A:\mBbbU{}']
    \mforall{}B:A  {}\mrightarrow{}  Type.  \mforall{}w,w':coW(A;a.B[a]).  \mforall{}p,q:Pos(coW-game(a.B[a];w;w')).
        (sg-reachable(coW-game(a.B[a];w;w');p;q)  {}\mRightarrow{}  coW-pos-agree(a.B[a];w;w';p;q))


By

---

Latex:
((Auto  THEN  D  -1)
  THEN  ExRepD
  THEN  (RWO  "-4<"  0  THENA  Auto)
  THEN  (RWO  "-3<"  0  THENA  Auto)
  THEN  ThinVar  `p'
  THEN  ThinVar  `q')

---

Home Index