---

Step * of Lemma coW-trans_wf

∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w1,w2,w3:coW(A;a.B[a])]. ∀[n:ℕ]. ∀[X:win2strat(coW-game(a.B[a];w1;w2);n)].
∀[Y:win2strat(coW-game(a.B[a];w2;w3);n)].
  (coW-trans(X; Y) ∈ win2strat(coW-game(a.B[a];w1;w3);n))
BY
{ (InductionOnNat
   THEN Auto
   THEN Try (((Unfold `win2strat` 0 THEN Reduce 0) THEN Trivial))
   THEN (Unfold `win2strat` 0 THEN (SplitOnConclITE THENA Auto) THEN Try (Trivial))
   THEN ((Assert ∀k:ℕ. ((k ≤ n) ⇒ (X ∈ win2strat(coW-game(a.B[a];w1;w2);k))) BY
                Auto)
         THEN (Assert ∀k:ℕ. ((k ≤ n) ⇒ (Y ∈ win2strat(coW-game(a.B[a];w2;w3);k))) BY
                     Auto)
         )
   THEN RepeatFor 2 ((Unfold `win2strat` -5 THEN (SplitOnHypITE -5  THENA Auto) THEN Try (Trivial)))
   THEN RepeatFor 2 (Thin (-1))
   THEN Thin (-3)
   THEN DepIsectHD (-4)
   THEN DepIsectHD (-3)
   THEN DepIsectCD
   THEN Try (BackThruSomeHyp)
   THEN (FunExt THENA 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. n : ℤ
7. 0 < n
8. ∀[X:win2strat(coW-game(a.B[a];w1;w2);n - 1)]. ∀[Y:win2strat(coW-game(a.B[a];w2;w3);n - 1)].
     (coW-trans(X; Y) ∈ win2strat(coW-game(a.B[a];w1;w3);n - 1))
9. X : s:win2strat(coW-game(a.B[a];w1;w2);n - 1) ⋂ moves:{f:strat2play(coW-game(a.B[a];w1;w2);n - 1;s)| 
                                                          ||f|| = (2 * n) ∈ ℤ}  ⟶ {p:Pos(coW-game(a.B[a];w1;w2))| Legal\000C2(moves[(2 * n) - 1];p)} 
10. X ∈ win2strat(coW-game(a.B[a];w1;w2);n - 1)
11. X ∈ moves:{f:strat2play(coW-game(a.B[a];w1;w2);n - 1;X)| ||f|| = (2 * n) ∈ ℤ}  ⟶ {p:Pos(coW-game(a.B[a];w1;w2))| 
                                                                            Legal2(moves[(2 * n) - 1];p)} 
12. Y : s:win2strat(coW-game(a.B[a];w2;w3);n - 1) ⋂ moves:{f:strat2play(coW-game(a.B[a];w2;w3);n - 1;s)| 
                                                           ||f|| = (2 * n) ∈ ℤ}  ⟶ {p:Pos(coW-game(a.B[a];w2;w3))| Lega\000Cl2(moves[(2 * n) - 1];p)} 
13. Y ∈ win2strat(coW-game(a.B[a];w2;w3);n - 1)
14. Y ∈ moves:{f:strat2play(coW-game(a.B[a];w2;w3);n - 1;Y)| ||f|| = (2 * n) ∈ ℤ}  ⟶ {p:Pos(coW-game(a.B[a];w2;w3))| 
                                                                            Legal2(moves[(2 * n) - 1];p)} 
15. ∀k:ℕ. ((k ≤ n) ⇒ (X ∈ win2strat(coW-game(a.B[a];w1;w2);k)))
16. ∀k:ℕ. ((k ≤ n) ⇒ (Y ∈ win2strat(coW-game(a.B[a];w2;w3);k)))
17. moves : {f:strat2play(coW-game(a.B[a];w1;w3);n - 1;coW-trans(X; Y))| ||f|| = (2 * n) ∈ ℤ} 
⊢ coW-trans(X; Y) moves ∈ {p:Pos(coW-game(a.B[a];w1;w3))| Legal2(moves[(2 * n) - 1];p)} 

---

Latex:

---

Latex:
\mforall{}[A:\mBbbU{}'].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[w1,w2,w3:coW(A;a.B[a])].  \mforall{}[n:\mBbbN{}].
\mforall{}[X:win2strat(coW-game(a.B[a];w1;w2);n)].  \mforall{}[Y:win2strat(coW-game(a.B[a];w2;w3);n)].
    (coW-trans(X;  Y)  \mmember{}  win2strat(coW-game(a.B[a];w1;w3);n))


By

---

Latex:
(InductionOnNat
  THEN  Auto
  THEN  Try  (((Unfold  `win2strat`  0  THEN  Reduce  0)  THEN  Trivial))
  THEN  (Unfold  `win2strat`  0  THEN  (SplitOnConclITE  THENA  Auto)  THEN  Try  (Trivial))
  THEN  ((Assert  \mforall{}k:\mBbbN{}.  ((k  \mleq{}  n)  {}\mRightarrow{}  (X  \mmember{}  win2strat(coW-game(a.B[a];w1;w2);k)))  BY
                            Auto)
              THEN  (Assert  \mforall{}k:\mBbbN{}.  ((k  \mleq{}  n)  {}\mRightarrow{}  (Y  \mmember{}  win2strat(coW-game(a.B[a];w2;w3);k)))  BY
                                      Auto)
              )
  THEN  RepeatFor  2  ((Unfold  `win2strat`  -5  THEN  (SplitOnHypITE  -5    THENA  Auto)  THEN  Try  (Trivial)))
  THEN  RepeatFor  2  (Thin  (-1))
  THEN  Thin  (-3)
  THEN  DepIsectHD  (-4)
  THEN  DepIsectHD  (-3)
  THEN  DepIsectCD
  THEN  Try  (BackThruSomeHyp)
  THEN  (FunExt  THENA  Auto))

---

Home Index