Nuprl Definition : strat2play

A play of game g of length at least 2*n that follows strategy s
on the first n moves by player two.⋅

strat2play(g;n;s) ==
if (n =_z 0)

  then {moves:sequence(Pos(g))| (2 ≤ ||moves||) ∧ (moves[0] = InitialPos(g) ∈ Pos(g)) ∧ Legal1(moves[0];moves[1])}

  else f:strat2play(g;n - 1;s) ⋂ {moves:sequence(Pos(g))|
                                  (((2 * n) + 2) ≤ ||moves||)
                                  ∧ Legal1(moves[2 * n];moves[(2 * n) + 1])

                                  ∧ (moves[2 * n] = (s play-truncate(f;2 * n)) ∈ Pos(g))}

fi

Definitions occuring in Statement : play-truncate: play-truncate(f;m), play-item: moves[i], sg-legal1: Legal1(x;y), sg-init: InitialPos(g), sg-pos: Pos(g), dep-isect: x:A ⋂ B[x], seq-item: s[i], seq-len: ||s||, sequence: sequence(T), ifthenelse: if b then t else f fi , eq_int: (i =_z j), le: A ≤ B, and: P ∧ Q, set: {x:A| B[x]} , apply: f a, multiply: n * m, subtract: n - m, add: n + m, natural_number: $n, equal: s = t ∈ T
Definitions occuring in definition : ifthenelse: if b then t else f fi , eq_int: (i =_z j), seq-item: s[i], sg-init: InitialPos(g), dep-isect: x:A ⋂ B[x], subtract: n - m, set: {x:A| B[x]} , sequence: sequence(T), le: A ≤ B, seq-len: ||s||, and: P ∧ Q, sg-legal1: Legal1(x;y), add: n + m, equal: s = t ∈ T, sg-pos: Pos(g), play-item: moves[i], apply: f a, play-truncate: play-truncate(f;m), multiply: n * m, natural_number: $n
FDL editor aliases : strat2play

Latex:
strat2play(g;n;s) == if (n =\msubz{} 0) then \{moves:sequence(Pos(g))| (2 \mleq{} ||moves||) \mwedge{} (moves[0] = InitialPos(g)) \mwedge{} Legal1(moves[0];moves[1])\} else f:strat2play(g;n - 1;s) \mcap{} \{moves:sequence(Pos(g))| (((2 * n) + 2) \mleq{} ||moves||) \mwedge{} Legal1(moves[2 * n];moves[(2 * n) + 1]) \mwedge{} (moves[2 * n] = (s play-truncate(f;2 * n)))\} fi Date html generated: 2019_06_20-PM-00_52_05 Last ObjectModification: 2019_01_02-PM-01_31_54 Theory : co-recursion-2 Home Index