Nuprl Lemma : strat2play-longer

[g:SimpleGame]. ∀[n:ℕ]. ∀[s:win2strat(g;n)]. ∀[moves:strat2play(g;n;s)]. ∀[x:sequence(Pos(g))].
  ((x ∈ strat2play(g;n;s)) ∧ (seq-truncate(x;||moves||) moves ∈ strat2play(g;n;s))) supposing 
     ((seq-truncate(x;||moves||) moves ∈ sequence(Pos(g))) and 
     (||moves|| ≤ ||x||))


Proof




Definitions occuring in Statement :  strat2play: strat2play(g;n;s) win2strat: win2strat(g;n) sg-pos: Pos(g) simple-game: SimpleGame seq-truncate: seq-truncate(s;n) seq-len: ||s|| sequence: sequence(T) nat: uimplies: supposing a uall: [x:A]. B[x] le: A ≤ B and: P ∧ Q member: t ∈ T equal: t ∈ T
Definitions unfolded in proof :  label: ...$L... t less_than: a < b nat_plus: + so_apply: x[s] so_lambda: λ2x.t[x] exists: x:A. B[x] win2strat: win2strat(g;n) play-truncate: play-truncate(f;m) play-len: ||moves|| it: unit: Unit bool: 𝔹 bfalse: ff sq_type: SQType(T) sq_stable: SqStable(P) squash: T play-item: moves[i] btrue: tt ifthenelse: if then else fi  eq_int: (i =z j) strat2play: strat2play(g;n;s) true: True subtract: m uiff: uiff(P;Q) rev_implies:  Q iff: ⇐⇒ Q or: P ∨ Q decidable: Dec(P) not: ¬A less_than': less_than'(a;b) le: A ≤ B top: Top lelt: i ≤ j < k int_seg: {i..j-} cand: c∧ B all: x:A. B[x] subtype_rel: A ⊆B and: P ∧ Q prop: uimplies: supposing a guard: {T} ge: i ≥  false: False implies:  Q nat: member: t ∈ T uall: [x:A]. B[x]
Lemmas referenced :  omega-shadow minus-zero two-mul one-mul not-equal-implies-less le-add-cancel-alt mul-commutes mul-distributes mul-distributes-right set_subtype_base play-item_wf sg-legal2_wf seq-truncate-truncate le_reflexive seq-len-truncate play-len_wf equal-wf-T-base play-truncate_wf uiff_transitivity assert_of_bnot iff_weakening_uiff iff_transitivity eqff_to_assert assert_of_eq_int eqtt_to_assert bool_subtype_base subtype_base_sq bool_cases sq_stable__le multiply_nat_wf add_nat_wf mul-associates mul_bounds_1a add-is-int-iff zero-mul add-mul-special not-le-2 win2strat_subtype bool_wf int_subtype_base equal-wf-base not_wf bnot_wf assert_wf le_weakening eq_int_wf le-add-cancel2 sg-legal1_wf iff_weakening_equal subtype_rel_self not-lt-2 decidable__lt true_wf squash_wf le_transitivity simple-game_wf le_weakening2 le-add-cancel add-zero add_functionality_wrt_le add-commutes add-swap add-associates minus-minus minus-add minus-one-mul-top zero-add minus-one-mul condition-implies-le less-iff-le not-ge-2 subtract_wf decidable__le false_wf win2strat_wf strat2play_wf le_wf seq-truncate_wf int_seg_wf seq-truncate-item lelt_wf nat_wf seq-len_wf sg-pos_wf sequence_wf and_wf seq-item_wf equal_wf strat2play_subtype less_than_wf ge_wf less_than_irreflexivity less_than_transitivity1 nat_properties
Rules used in proof :  sqequalIntensionalEquality dependent_pairFormation equalityElimination impliesFunctionality cumulativity dependentIntersection_memberEquality closedConclusion baseApply dependentIntersectionElimination promote_hyp instantiate baseClosed imageMemberEquality universeEquality imageElimination minusEquality intEquality unionElimination multiplyEquality addEquality setEquality independent_pairEquality voidEquality levelHypothesis hyp_replacement addLevel productElimination applyLambdaEquality productEquality independent_pairFormation equalitySymmetry equalityTransitivity dependent_set_memberEquality applyEquality because_Cache isect_memberEquality axiomEquality dependent_functionElimination lambdaEquality voidElimination independent_functionElimination independent_isectElimination natural_numberEquality lambdaFormation intWeakElimination sqequalRule rename setElimination hypothesis hypothesisEquality thin isectElimination sqequalHypSubstitution extract_by_obid cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[g:SimpleGame].  \mforall{}[n:\mBbbN{}].  \mforall{}[s:win2strat(g;n)].  \mforall{}[moves:strat2play(g;n;s)].  \mforall{}[x:sequence(Pos(g))].
    ((x  \mmember{}  strat2play(g;n;s))  \mwedge{}  (seq-truncate(x;||moves||)  =  moves))  supposing 
          ((seq-truncate(x;||moves||)  =  moves)  and 
          (||moves||  \mleq{}  ||x||))



Date html generated: 2018_07_25-PM-01_33_23
Last ObjectModification: 2018_06_25-AM-10_43_52

Theory : co-recursion


Home Index