Nuprl Lemma : respond-implies-win2

∀g:SimpleGame. ((∀p:{p:Pos(g)| Legal1(InitialPos(g);p)} . ∃q:{q:Pos(g)| Legal2(p;q)} . win2(g@q)) ⇒ win2(g))

Proof

Definitions occuring in Statement : sg-change-init: g@j, win2: win2(g), sg-legal2: Legal2(x;y), sg-legal1: Legal1(x;y), sg-init: InitialPos(g), sg-pos: Pos(g), simple-game: SimpleGame, all: ∀x:A. B[x], exists: ∃x:A. B[x], implies: P ⇒ Q, set: {x:A| B[x]}
Definitions unfolded in proof : sg-legal2: Legal2(x;y), int_nzero: ℤ^-^o, nequal: a ≠ b ∈ T , sg-init: InitialPos(g), strat2play: strat2play(g;n;s), seq-tl: seq-tl(s), cand: A c∧ B, sg-reachable: sg-reachable(g;x;y), sq_stable: SqStable(P), eq_int: (i =_z j), pi2: snd(t), seq-len: ||s||, seq-truncate: seq-truncate(s;n), seq-item: s[i], play-len: ||moves||, play-truncate: play-truncate(f;m), sequence: sequence(T), spreadn: spread4, sg-change-init: g@j, sg-pos: Pos(g), simple-game: SimpleGame, less_than: a < b, nat_plus: ℕ⁺, play-item: moves[i], sq_type: SQType(T), squash: ↓T, lelt: i ≤ j < k, int_seg: {i..j^-}, bfalse: ff, ifthenelse: if b then t else f fi , btrue: tt, it: ⋅, unit: Unit, bool: 𝔹, true: True, less_than': less_than'(a;b), le: A ≤ B, top: Top, subtract: n - m, uiff: uiff(P;Q), rev_implies: P ⇐ Q, not: ¬A, and: P ∧ Q, iff: P ⇐⇒ Q, or: P ∨ Q, decidable: Dec(P), win2strat: win2strat(g;n), uimplies: b supposing a, guard: {T}, ge: i ≥ j , false: False, nat: ℕ, win2: win2(g), subtype_rel: A ⊆r B, pi1: fst(t), so_apply: x[s], so_lambda: λ₂x.t[x], prop: ℙ, uall: ∀[x:A]. B[x], member: t ∈ T, exists: ∃x:A. B[x], implies: P ⇒ Q, all: ∀x:A. B[x]
Lemmas referenced : play-truncate_wf, add_nat_plus, le_transitivity, nequal_wf, trivial-cancel, bfalse_wf, multiply-is-int-iff, eq_int_eq_false, bool_subtype_base, mul-swap, sg-reachable_self, sg-legal1-change-init, add-is-int-iff, add-member-int_seg2, seq-settype, mod2-2n-plus-1, mod2-2n, seq-tl-item, seq-truncate-item, seq-len-truncate, int_seg_properties, nat_plus_properties, nat_plus_subtype_nat, set_subtype_base, le_weakening2, nat_plus_wf, multiply_nat_wf, add_nat_wf, mul_bounds_1a, seq-truncate_wf, strat2play-invariant, int_seg_wf, le-add-cancel-alt, sq_stable__le, seq-tl_wf, seq-tl-len, le_weakening, seq-item_wf, sg-reachable_wf, seq-len_wf, sequence_wf, strat2play_subtype, win2strat_wf, win2strat-properties, le_antisymmetry_iff, mul_preserves_le, le-add-cancel2, minus-zero, not-equal-2, decidable__int_equal, decidable__lt, omega-shadow, not-lt-2, two-mul, add-mul-special, one-mul, le_reflexive, iff_weakening_equal, true_wf, squash_wf, subtype_rel_self, not-equal-implies-less, subtype_base_sq, zero-mul, mul-distributes-right, mul-associates, mul-commutes, mul-distributes, play-item_wf, lelt_wf, strat2play-invariant-1, assert_of_bnot, eqff_to_assert, iff_weakening_uiff, iff_transitivity, assert_of_eq_int, eqtt_to_assert, uiff_transitivity, play-len_wf, equal-wf-T-base, le_wf, not-le-2, strat2play_wf, int_subtype_base, not_wf, bnot_wf, assert_wf, equal-wf-base, bool_wf, eq_int_wf, simple-game_wf, nat_wf, 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, false_wf, subtract_wf, decidable__le, less_than_wf, ge_wf, less_than_irreflexivity, less_than_transitivity1, nat_properties, all_wf, set_wf, equal_wf, sg-change-init_wf, win2_wf, sg-legal2_wf, exists_wf, sg-init_wf, sg-legal1_wf, sg-pos_wf
Rules used in proof : applyLambdaEquality, addLevel, functionEquality, productEquality, isectEquality, universeEquality, imageMemberEquality, cumulativity, instantiate, multiplyEquality, sqequalIntensionalEquality, imageElimination, impliesFunctionality, equalityElimination, dependent_set_memberEquality, dependentIntersection_memberEquality, closedConclusion, baseApply, baseClosed, minusEquality, intEquality, voidEquality, isect_memberEquality, addEquality, independent_pairFormation, unionElimination, axiomEquality, voidElimination, independent_isectElimination, natural_numberEquality, intWeakElimination, isect_memberFormation, independent_functionElimination, dependent_functionElimination, equalitySymmetry, equalityTransitivity, productElimination, because_Cache, sqequalRule, setElimination, isectElimination, extract_by_obid, introduction, setEquality, hypothesisEquality, sqequalHypSubstitution, functionExtensionality, applyEquality, lambdaEquality, dependent_pairFormation, rename, thin, promote_hyp, hypothesis, cut, lambdaFormation, sqequalReflexivity, computationStep, sqequalTransitivity, sqequalSubstitution

Latex:
\mforall{}g:SimpleGame ((\mforall{}p:\{p:Pos(g)| Legal1(InitialPos(g);p)\} . \mexists{}q:\{q:Pos(g)| Legal2(p;q)\} . win2(g@q)) {}\mRightarrow{} win2(g)) Date html generated: 2018_07_25-PM-01_36_33 Last ObjectModification: 2018_06_20-PM-09_31_37 Theory : co-recursion Home Index