---

Step * 2 1 1 1 of Lemma coW-equiv-iff


1. [A] : 𝕌'
2. B : A ⟶ Type
3. w : coW(A;a.B[a])
4. w' : coW(A;a.B[a])
5. ∀z:coW(A;a.B[a]). (coWmem(a.B[a];z;w) ⇐⇒ coWmem(a.B[a];z;w'))
6. n : ℕ
7. p3 : coPath(a.B[a];w;n)
8. n1 : ℕ
9. p4 : coPath(a.B[a];w';n1)
10. ((n = 1 ∈ ℤ) ∧ (<n1, p4> = <0, ⋅> ∈ (n:ℕ × coPath(a.B[a];w';n))))
∨ ((n1 = 1 ∈ ℤ) ∧ (<n, p3> = <0, ⋅> ∈ (n:ℕ × coPath(a.B[a];w;n))))
⊢ ∃q:{q:Pos(coW-game(a.B[a];w;w'))| Legal2(<<n, p3>, n1, p4>;q)} . win2(coW-game(a.B[a];w;w')@q)
BY
{ (RepeatFor 2 (D -1)
   THEN ((EqHD (-1) THENA Auto) THEN All Reduce)
   THEN Eliminate ⌜n⌝⋅
   THEN Eliminate ⌜n1⌝⋅
   THEN ThinVar `n1'
   THEN ThinVar `n'
   THEN Thin (-1)
   THEN ∀h:hyp. (Unfold `coPath` h THEN Reduce h) 
   THEN DProds) }

1
1. [A] : 𝕌'
2. B : A ⟶ Type
3. w : coW(A;a.B[a])
4. w' : coW(A;a.B[a])
5. ∀z:coW(A;a.B[a]). (coWmem(a.B[a];z;w) ⇐⇒ coWmem(a.B[a];z;w'))
6. t : coW-dom(a.B[a];w)
7. p5 : coPath(a.B[a];coW-item(w;t);0)
8. p4 : Top
⊢ ∃q:{q:Pos(coW-game(a.B[a];w;w'))| Legal2(<<1, t, p5>, 0, p4>;q)} . win2(coW-game(a.B[a];w;w')@q)

2
1. [A] : 𝕌'
2. B : A ⟶ Type
3. w : coW(A;a.B[a])
4. w' : coW(A;a.B[a])
5. ∀z:coW(A;a.B[a]). (coWmem(a.B[a];z;w) ⇐⇒ coWmem(a.B[a];z;w'))
6. p3 : Top
7. t : coW-dom(a.B[a];w')
8. p5 : coPath(a.B[a];coW-item(w';t);0)
⊢ ∃q:{q:Pos(coW-game(a.B[a];w;w'))| Legal2(<<0, p3>, 1, t, p5>;q)} . win2(coW-game(a.B[a];w;w')@q)

---

Latex:

---

Latex:

1.  [A]  :  \mBbbU{}'
2.  B  :  A  {}\mrightarrow{}  Type
3.  w  :  coW(A;a.B[a])
4.  w'  :  coW(A;a.B[a])
5.  \mforall{}z:coW(A;a.B[a]).  (coWmem(a.B[a];z;w)  \mLeftarrow{}{}\mRightarrow{}  coWmem(a.B[a];z;w'))
6.  n  :  \mBbbN{}
7.  p3  :  coPath(a.B[a];w;n)
8.  n1  :  \mBbbN{}
9.  p4  :  coPath(a.B[a];w';n1)
10.  ((n  =  1)  \mwedge{}  (<n1,  p4>  =  ɘ,  \mcdot{}>))  \mvee{}  ((n1  =  1)  \mwedge{}  (<n,  p3>  =  ɘ,  \mcdot{}>))
\mvdash{}  \mexists{}q:\{q:Pos(coW-game(a.B[a];w;w'))|  Legal2(<<n,  p3>,  n1,  p4>q)\}  .  win2(coW-game(a.B[a];w;w')@q)


By

---

Latex:
(RepeatFor  2  (D  -1)
  THEN  ((EqHD  (-1)  THENA  Auto)  THEN  All  Reduce)
  THEN  Eliminate  \mkleeneopen{}n\mkleeneclose{}\mcdot{}
  THEN  Eliminate  \mkleeneopen{}n1\mkleeneclose{}\mcdot{}
  THEN  ThinVar  `n1'
  THEN  ThinVar  `n'
  THEN  Thin  (-1)
  THEN  \mforall{}h:hyp.  (Unfold  `coPath`  h  THEN  Reduce  h) 
  THEN  DProds)

---

Home Index