Nuprl Lemma : win2strat-properties
∀g:SimpleGame. ∀n:ℕ+. ∀s:win2strat(g;n).
((s ∈ win2strat(g;n - 1))
∧ (s ∈ moves:{f:strat2play(g;n - 1;s)| ||f|| = (2 * n) ∈ ℤ} ⟶ {p:Pos(g)| Legal2(moves[(2 * n) - 1];p)} ))
Proof
Definitions occuring in Statement :
strat2play: strat2play(g;n;s),
win2strat: win2strat(g;n),
play-len: ||moves||,
play-item: moves[i],
sg-legal2: Legal2(x;y),
sg-pos: Pos(g),
simple-game: SimpleGame,
nat_plus: ℕ+,
all: ∀x:A. B[x],
and: P ∧ Q,
member: t ∈ T,
set: {x:A| B[x]} ,
function: x:A ⟶ B[x],
multiply: n * m,
subtract: n - m,
natural_number: $n,
int: ℤ,
equal: s = t ∈ T
Definitions unfolded in proof :
all: ∀x:A. B[x],
win2strat: win2strat(g;n),
member: t ∈ T,
uall: ∀[x:A]. B[x],
subtype_rel: A ⊆r B,
nat_plus: ℕ+,
and: P ∧ Q,
cand: A c∧ B,
false: False,
guard: {T},
uimplies: b supposing a,
implies: P ⇒ Q,
prop: ℙ,
or: P ∨ Q,
sq_type: SQType(T),
uiff: uiff(P;Q),
ifthenelse: if b then t else f fi ,
btrue: tt,
iff: P ⇐⇒ Q,
not: ¬A,
rev_implies: P ⇐ Q,
bfalse: ff
Lemmas referenced :
win2strat_wf,
nat_plus_subtype_nat,
nat_plus_wf,
simple-game_wf,
eq_int_wf,
less_than_transitivity1,
le_weakening,
less_than_irreflexivity,
assert_wf,
bnot_wf,
not_wf,
equal-wf-T-base,
bool_cases,
subtype_base_sq,
bool_wf,
bool_subtype_base,
eqtt_to_assert,
assert_of_eq_int,
eqff_to_assert,
iff_transitivity,
iff_weakening_uiff,
assert_of_bnot
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
sqequalHypSubstitution,
cut,
introduction,
extract_by_obid,
isectElimination,
thin,
hypothesisEquality,
applyEquality,
hypothesis,
sqequalRule,
setElimination,
rename,
natural_numberEquality,
because_Cache,
equalityTransitivity,
equalitySymmetry,
independent_isectElimination,
dependent_functionElimination,
independent_functionElimination,
voidElimination,
independent_pairFormation,
intEquality,
baseClosed,
dependentIntersectionElimination,
unionElimination,
instantiate,
cumulativity,
productElimination,
impliesFunctionality
Latex:
\mforall{}g:SimpleGame. \mforall{}n:\mBbbN{}\msupplus{}. \mforall{}s:win2strat(g;n).
((s \mmember{} win2strat(g;n - 1))
\mwedge{} (s \mmember{} moves:\{f:strat2play(g;n - 1;s)| ||f|| = (2 * n)\} {}\mrightarrow{} \{p:Pos(g)| Legal2(moves[(2 * n) - 1];p\000C)\} ))
Date html generated:
2018_07_25-PM-01_32_17
Last ObjectModification:
2018_07_11-PM-00_23_50
Theory : co-recursion
Home
Index