Proof of Nuprl Lemma : coW-trans

Step * 1 1 2 2 1 of Lemma coW-trans_wf

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) ∈ ℤ}
18. k : ℤ
19. 0 < k
20. k ≤ (n - 1)
21. m1 : strat2play(coW-game(a.B[a];w1;w3);k;coW-trans(X; Y))
22. ||m1|| = ((2 * k) + 2) ∈ ℤ
23. 1 ≤ k
24. (2 * 1) ≤ (2 * k)
25. ¬(||m1|| = 0 ∈ ℤ)
26. transMoves(X;Y;seq-truncate(m1;||m1|| - 2)) ∈ {p:strat2play(coW-game(a.B[a];w1;w2);k - 1;X)

                                                   × strat2play(coW-game(a.B[a];w2;w3);k - 1;Y)|

let a,b = p

                                                   in coWtransInvariant(a.B[a];w1;w2;w3;k

                                                      - 1;X;Y;a;b;seq-truncate(m1;||m1|| - 2))}

27. m1 ∈ sequence(Pos(coW-game(a.B[a];w1;w3)))
28. ((2 * k) + 2) ≤ ||m1||
29. {p:strat2play(coW-game(a.B[a];w1;w2);k - 1;X) × strat2play(coW-game(a.B[a];w2;w3);k - 1;Y)|
     let a,b = p
     in coWtransInvariant(a.B[a];w1;w2;w3;k - 1;X;Y;a;b;seq-truncate(m1;||m1|| - 2))}  ∈ Type
⊢ let a,b = transMoves(X;Y;seq-truncate(m1;||m1|| - 2))
  in let x,z1 = if (||m1|| =_z 2) then <(), ()> else X a fi
     in let z2,y = if (||m1|| =_z 2) then <(), ()> else Y b fi
        in let u,v = m1[||m1|| - 1]
           in if copath-length(x) <z copath-length(u)
              then let M1 = seq-add(seq-add(a;<x, z1>);<u, z1>) in
                    let M2 = seq-add(seq-add(b;<z2, y>);<snd((X M1)), y>) in
                    <M1, M2>
              else let M2 = seq-add(seq-add(b;<z2, y>);<z2, v>) in
                    let M1 = seq-add(seq-add(a;<x, z1>);<x, fst((Y M2))>) in
                    <M1, M2>

              fi  ∈ {p:strat2play(coW-game(a.B[a];w1;w2);k;X) × strat2play(coW-game(a.B[a];w2;w3);k;Y)|

                     let a,b = p
                     in coWtransInvariant(a.B[a];w1;w2;w3;k;X;Y;a;b;m1)}
BY
{ ((Assert m1[||m1|| - 2]
          = let a,b = transMoves(X;Y;seq-truncate(m1;||m1|| - 2))
            in let u,x = X a
               in let x,v = Y b
                  in <u, v>
          ∈ Pos(coW-game(a.B[a];w1;w3)) BY
          ((OnVar `m1' Strat2PlayInvariant THENA Auto)
           THEN D -1
           THEN (D -1 With ⌜k - 1⌝  THENA Auto)
           THEN (RepeatFor 2 (D -1) THENA Auto)
           THEN D -1
           THEN (Subst' (k - 1) + 1 ~ k -1 THENA Auto)
           THEN (Subst' 2 * k ~ ||m1|| - 2 -1 THENA Auto)
           THEN Unfold `play-truncate` -1
           THEN Unfold `coW-trans` -1
           THEN Reduce -1
           THEN Auto))
   THEN MoveToConcl (-1)
   THEN (GenConclTerm ⌜transMoves(X;Y;seq-truncate(m1;||m1|| - 2))⌝⋅ 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)}

                                                   × strat2play(coW-game(a.B[a];w2;w3);k - 1;Y)|

let a,b = p

                                                   in coWtransInvariant(a.B[a];w1;w2;w3;k

                                                      - 1;X;Y;a;b;seq-truncate(m1;||m1|| - 2))}

27. m1 ∈ sequence(Pos(coW-game(a.B[a];w1;w3)))
28. ((2 * k) + 2) ≤ ||m1||
29. {p:strat2play(coW-game(a.B[a];w1;w2);k - 1;X) × strat2play(coW-game(a.B[a];w2;w3);k - 1;Y)|
     let a,b = p
     in coWtransInvariant(a.B[a];w1;w2;w3;k - 1;X;Y;a;b;seq-truncate(m1;||m1|| - 2))}  ∈ Type
30. v : {p:strat2play(coW-game(a.B[a];w1;w2);k - 1;X) × strat2play(coW-game(a.B[a];w2;w3);k - 1;Y)|
         let a,b = p
         in coWtransInvariant(a.B[a];w1;w2;w3;k - 1;X;Y;a;b;seq-truncate(m1;||m1|| - 2))}
31. transMoves(X;Y;seq-truncate(m1;||m1|| - 2))
= v
∈ {p:strat2play(coW-game(a.B[a];w1;w2);k - 1;X) × strat2play(coW-game(a.B[a];w2;w3);k - 1;Y)|
   let a,b = p
   in coWtransInvariant(a.B[a];w1;w2;w3;k - 1;X;Y;a;b;seq-truncate(m1;||m1|| - 2))}

⊢ (m1[||m1|| - 2] = let a,b = v in let u,x = X a in let x,v = Y b in <u, v> ∈ Pos(coW-game(a.B[a];w1;w3)))

⇒ (let a,b = v
    in let x,z1 = if (||m1|| =_z 2) then <(), ()> else X a fi
       in let z2,y = if (||m1|| =_z 2) then <(), ()> else Y b fi
          in let u,v = m1[||m1|| - 1]
             in if copath-length(x) <z copath-length(u)
                then let M1 = seq-add(seq-add(a;<x, z1>);<u, z1>) in
                      let M2 = seq-add(seq-add(b;<z2, y>);<snd((X M1)), y>) in
                      <M1, M2>
                else let M2 = seq-add(seq-add(b;<z2, y>);<z2, v>) in
                      let M1 = seq-add(seq-add(a;<x, z1>);<x, fst((Y M2))>) in
                      <M1, M2>

                fi  ∈ {p:strat2play(coW-game(a.B[a];w1;w2);k;X) × strat2play(coW-game(a.B[a];w2;w3);k;Y)|

let a,b = p
in coWtransInvariant(a.B[a];w1;w2;w3;k;X;Y;a;b;m1)} )

Latex:

Latex:
1. A : \mBbbU{}' 2. B : A {}\mrightarrow{} Type 3. w1 : coW(A;a.B[a]) 4. w2 : coW(A;a.B[a]) 5. w3 : coW(A;a.B[a]) 6. n : \mBbbZ{} 7. 0 < n 8. \mforall{}[X:win2strat(coW-game(a.B[a];w1;w2);n - 1)]. \mforall{}[Y:win2strat(coW-game(a.B[a];w2;w3);n - 1)]. (coW-trans(X; Y) \mmember{} win2strat(coW-game(a.B[a];w1;w3);n - 1)) 9. X : s:win2strat(coW-game(a.B[a];w1;w2);n - 1) \mcap{} moves:\{f:strat2play(coW-game(a.B[a];w1;w2);n - 1;s)| ||f|| = (2 * n)\} {}\mrightarrow{} \{p:Pos(coW-game(a.B[a];w1;w2))| Legal2(moves[(2 * n) - 1];p)\} 10. X \mmember{} win2strat(coW-game(a.B[a];w1;w2);n - 1) 11. X \mmember{} moves:\{f:strat2play(coW-game(a.B[a];w1;w2);n - 1;X)| ||f|| = (2 * n)\} {}\mrightarrow{} \{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) \mcap{} moves:\{f:strat2play(coW-game(a.B[a];w2;w3);n - 1;s)| ||f|| = (2 * n)\} {}\mrightarrow{} \{p:Pos(coW-game(a.B[a];w2;w3))| Legal2(moves[(2 * n) - 1];p)\} 13. Y \mmember{} win2strat(coW-game(a.B[a];w2;w3);n - 1) 14. Y \mmember{} moves:\{f:strat2play(coW-game(a.B[a];w2;w3);n - 1;Y)| ||f|| = (2 * n)\} {}\mrightarrow{} \{p:Pos(coW-game(a.B[a];w2;w3))| Legal2(moves[(2 * n) - 1];p)\} 15. \mforall{}k:\mBbbN{}. ((k \mleq{} n) {}\mRightarrow{} (X \mmember{} win2strat(coW-game(a.B[a];w1;w2);k))) 16. \mforall{}k:\mBbbN{}. ((k \mleq{} n) {}\mRightarrow{} (Y \mmember{} 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)\} 18. k : \mBbbZ{} 19. 0 < k 20. k \mleq{} (n - 1) 21. m1 : strat2play(coW-game(a.B[a];w1;w3);k;coW-trans(X; Y)) 22. ||m1|| = ((2 * k) + 2) 23. 1 \mleq{} k 24. (2 * 1) \mleq{} (2 * k) 25. \mneg{}(||m1|| = 0) 26. transMoves(X;Y;seq-truncate(m1;||m1|| - 2)) \mmember{} \{p:strat2play(coW-game(a.B[a];w1;w2);k - 1;X) \mtimes{} strat2play(coW-game(a.B[a];w2;w3);k - 1;Y)| let a,b = p in coWtransInvariant(a.B[a];w1;w2;w3;k - 1;X;Y;a;b;seq-truncate(m1;||m1|| - 2))\} 27. m1 \mmember{} sequence(Pos(coW-game(a.B[a];w1;w3))) 28. ((2 * k) + 2) \mleq{} ||m1|| 29. \{p:strat2play(coW-game(a.B[a];w1;w2);k - 1;X) \mtimes{} strat2play(coW-game(a.B[a];w2;w3);k - 1;Y)| let a,b = p in coWtransInvariant(a.B[a];w1;w2;w3;k - 1;X;Y;a;b;seq-truncate(m1;||m1|| - 2))\} \mmember{} Type \mvdash{} let a,b = transMoves(X;Y;seq-truncate(m1;||m1|| - 2)) in let x,z1 = if (||m1|| =\msubz{} 2) then <(), ()> else X a fi in let z2,y = if (||m1|| =\msubz{} 2) then <(), ()> else Y b fi in let u,v = m1[||m1|| - 1] in if copath-length(x) <z copath-length(u) then let M1 = seq-add(seq-add(a;<x, z1>);<u, z1>) in let M2 = seq-add(seq-add(b;<z2, y>);<snd((X M1)), y>) in <M1, M2> else let M2 = seq-add(seq-add(b;<z2, y>);<z2, v>) in let M1 = seq-add(seq-add(a;<x, z1>);<x, fst((Y M2))>) in <M1, M2> fi \mmember{} \{p:strat2play(coW-game(a.B[a];w1;w2);k;X) \mtimes{} strat2play(coW-game(a.B[a];w2;w3);k;Y)| let a,b = p in coWtransInvariant(a.B[a];w1;w2;w3;k;X;Y;a;b;m1)\} By Latex: ((Assert m1[||m1|| - 2] = let a,b = transMoves(X;Y;seq-truncate(m1;||m1|| - 2)) in let u,x = X a in let x,v = Y b in <u, v> BY ((OnVar `m1' Strat2PlayInvariant THENA Auto) THEN D -1 THEN (D -1 With \mkleeneopen{}k - 1\mkleeneclose{} THENA Auto) THEN (RepeatFor 2 (D -1) THENA Auto) THEN D -1 THEN (Subst' (k - 1) + 1 \msim{} k -1 THENA Auto) THEN (Subst' 2 * k \msim{} ||m1|| - 2 -1 THENA Auto) THEN Unfold `play-truncate` -1 THEN Unfold `coW-trans` -1 THEN Reduce -1 THEN Auto)) THEN MoveToConcl (-1) THEN (GenConclTerm \mkleeneopen{}transMoves(X;Y;seq-truncate(m1;||m1|| - 2))\mkleeneclose{}\mcdot{} THENA Auto)) Home Index