Nuprl Lemma : win2-iff

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

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

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