Nuprl Lemma : strat2play_subtype

[g:SimpleGame]. ∀[n:ℕ]. ∀[s:win2strat(g;n)].
  (strat2play(g;n;s) ⊆{moves:sequence(Pos(g))| ((2 n) 2) ≤ ||moves||} )


Proof




Definitions occuring in Statement :  strat2play: strat2play(g;n;s) win2strat: win2strat(g;n) sg-pos: Pos(g) simple-game: SimpleGame seq-len: ||s|| sequence: sequence(T) nat: subtype_rel: A ⊆B uall: [x:A]. B[x] le: A ≤ B set: {x:A| B[x]}  multiply: m add: m natural_number: $n
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T subtype_rel: A ⊆B strat2play: strat2play(g;n;s) nat: and: P ∧ Q all: x:A. B[x] implies:  Q exists: x:A. B[x] so_lambda: λ2x.t[x] so_apply: x[s] uimplies: supposing a prop: le: A ≤ B top: Top subtract: m sq_type: SQType(T) guard: {T} ge: i ≥  squash: T or: P ∨ Q uiff: uiff(P;Q) ifthenelse: if then else fi  btrue: tt iff: ⇐⇒ Q not: ¬A rev_implies:  Q bfalse: ff
Lemmas referenced :  strat2play_wf win2strat_wf nat_wf simple-game_wf eq_int_wf seq-len_wf sg-pos_wf set_subtype_base le_wf int_subtype_base equal_wf add-commutes subtract_wf minus-zero zero-add add-zero subtype_base_sq mul-commutes assert_wf bnot_wf not_wf equal-wf-T-base bool_cases bool_wf bool_subtype_base eqtt_to_assert assert_of_eq_int eqff_to_assert iff_transitivity iff_weakening_uiff assert_of_bnot nat_properties
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaEquality sqequalHypSubstitution extract_by_obid isectElimination thin hypothesisEquality hypothesis sqequalRule axiomEquality isect_memberEquality because_Cache setElimination rename natural_numberEquality equalityTransitivity equalitySymmetry productElimination lambdaFormation dependent_pairFormation sqequalIntensionalEquality applyEquality intEquality independent_isectElimination dependent_functionElimination independent_functionElimination promote_hyp dependent_set_memberEquality addEquality multiplyEquality voidElimination voidEquality instantiate cumulativity baseClosed dependentIntersectionElimination applyLambdaEquality imageMemberEquality imageElimination unionElimination independent_pairFormation impliesFunctionality

Latex:
\mforall{}[g:SimpleGame].  \mforall{}[n:\mBbbN{}].  \mforall{}[s:win2strat(g;n)].
    (strat2play(g;n;s)  \msubseteq{}r  \{moves:sequence(Pos(g))|  ((2  *  n)  +  2)  \mleq{}  ||moves||\}  )



Date html generated: 2018_07_25-PM-01_32_25
Last ObjectModification: 2018_06_12-PM-01_15_15

Theory : co-recursion


Home Index