---

Step * 2 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. p : {p:Pos(coW-game(a.B[a];w;w'))| Legal1(InitialPos(coW-game(a.B[a];w;w'));p)} 
⊢ ∃q:{q:Pos(coW-game(a.B[a];w;w'))| Legal2(p;q)} . win2(coW-game(a.B[a];w;w')@q)
BY
{ (D -1
   THEN (RepUR ``sg-pos coW-game`` -2 THEN D -2)
   THEN (Assert ((copath-length(p1) = 1 ∈ ℤ) ∧ (p2 = () ∈ copath(a.B[a];w')))
               ∨ ((copath-length(p2) = 1 ∈ ℤ) ∧ (p1 = () ∈ copath(a.B[a];w))) BY
               ((RepUR ``sg-legal1 coW-game`` -1 THEN (Subst' copath-length(()) ~ 0 -1 THENA Computation))
                THEN Reduce -1
                THEN ((Decide ⌜copath-length(p1) = 1 ∈ ℤ⌝⋅ THENA Auto) THENL [OrLeft; OrRight])
                THEN Auto
                THEN SplitOrHyps
                THEN Auto
                THEN (RWO "-5<" (-1) THENA Auto)
                THEN (Subst' copath-length(()) ~ 0 -1 THENA Computation)
                THEN Auto))
   THEN Thin (-2)) }

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. p1 : copath(a.B[a];w)
7. p2 : copath(a.B[a];w')
8. ((copath-length(p1) = 1 ∈ ℤ) ∧ (p2 = () ∈ copath(a.B[a];w')))
∨ ((copath-length(p2) = 1 ∈ ℤ) ∧ (p1 = () ∈ copath(a.B[a];w)))
⊢ ∃q:{q:Pos(coW-game(a.B[a];w;w'))| Legal2(<p1, p2>;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.  p  :  \{p:Pos(coW-game(a.B[a];w;w'))|  Legal1(InitialPos(coW-game(a.B[a];w;w'));p)\} 
\mvdash{}  \mexists{}q:\{q:Pos(coW-game(a.B[a];w;w'))|  Legal2(p;q)\}  .  win2(coW-game(a.B[a];w;w')@q)


By

---

Latex:
(D  -1
  THEN  (RepUR  ``sg-pos  coW-game``  -2  THEN  D  -2)
  THEN  (Assert  ((copath-length(p1)  =  1)  \mwedge{}  (p2  =  ()))  \mvee{}  ((copath-length(p2)  =  1)  \mwedge{}  (p1  =  ()))  BY
                          ((RepUR  ``sg-legal1  coW-game``  -1
                              THEN  (Subst'  copath-length(())  \msim{}  0  -1  THENA  Computation)
                              )
                            THEN  Reduce  -1
                            THEN  ((Decide  \mkleeneopen{}copath-length(p1)  =  1\mkleeneclose{}\mcdot{}  THENA  Auto)  THENL  [OrLeft;  OrRight])
                            THEN  Auto
                            THEN  SplitOrHyps
                            THEN  Auto
                            THEN  (RWO  "-5<"  (-1)  THENA  Auto)
                            THEN  (Subst'  copath-length(())  \msim{}  0  -1  THENA  Computation)
                            THEN  Auto))
  THEN  Thin  (-2))

---

Home Index