Nuprl Lemma : coW-play-invariant

∀[A:𝕌']
  ∀B:A ⟶ Type. ∀w,w':coW(A;a.B[a]). ∀n:ℕ. ∀s:win2strat(coW-game(a.B[a];w;w');n).
  ∀moves:strat2play(coW-game(a.B[a];w;w');n;s). ∀i:ℕ.
    (((i ≤ n)
    ⇒ (coW-pos-lens(moves[2 * i];i;i)

       ∧ (coW-pos-lens(moves[(2 * i) + 1];i;i + 1) ∨ coW-pos-lens(moves[(2 * i) + 1];i + 1;i))))

∧ ((i ≤ ((2 * n) + 1)) ⇒ (∀j:ℕi + 1. coW-pos-agree(a.B[a];w;w';moves[j];moves[i]))))

Proof

Definitions occuring in Statement : coW-pos-agree: coW-pos-agree(a.B[a];w;w';p;q), coW-pos-lens: coW-pos-lens(p;i;j), coW-game: coW-game(a.B[a];w;w'), coW: coW(A;a.B[a]), strat2play: strat2play(g;n;s), win2strat: win2strat(g;n), play-item: moves[i], int_seg: {i..j^-}, nat: ℕ, uall: ∀[x:A]. B[x], so_apply: x[s], le: A ≤ B, all: ∀x:A. B[x], implies: P ⇒ Q, or: P ∨ Q, and: P ∧ Q, function: x:A ⟶ B[x], multiply: n * m, add: n + m, natural_number: $n, universe: Type
Definitions unfolded in proof : exists: ∃x:A. B[x], nequal: a ≠ b ∈ T , int_nzero: ℤ^-^o, sg-legal2: Legal2(x;y), coW-pos-agree: coW-pos-agree(a.B[a];w;w';p;q), sq_type: SQType(T), sg-legal1: Legal1(x;y), sg-pos: Pos(g), copath-length: copath-length(p), copath-nil: (), pi2: snd(t), pi1: fst(t), coW-pos-lens: coW-pos-lens(p;i;j), sg-init: InitialPos(g), coW-game: coW-game(a.B[a];w;w'), play-item: moves[i], cand: A c∧ B, less_than: a < b, nat_plus: ℕ⁺, squash: ↓T, sq_stable: SqStable(P), guard: {T}, true: True, top: Top, subtract: n - m, uimplies: b supposing a, uiff: uiff(P;Q), rev_implies: P ⇐ Q, iff: P ⇐⇒ Q, or: P ∨ Q, decidable: Dec(P), not: ¬A, false: False, less_than': less_than'(a;b), le: A ≤ B, lelt: i ≤ j < k, int_seg: {i..j^-}, subtype_rel: A ⊆r B, nat: ℕ, prop: ℙ, implies: P ⇒ Q, and: P ∧ Q, so_apply: x[s], so_lambda: λ₂x.t[x], member: t ∈ T, all: ∀x:A. B[x], uall: ∀[x:A]. B[x]
Lemmas referenced : coW-pos-agree_transitivity, not-equal-implies-less, not-equal-2, sq_stable__copathAgree, and_wf, rem_bounds_1, div_bounds_1, nequal_wf, equal-wf-base, div_rem_sum, le_weakening2, subtract-add-cancel, less_than_irreflexivity, less_than_transitivity1, int_seg_cases, int_seg_subtype, copathAgree_refl, minus-zero, int_seg_properties, equal-wf-base-T, copath-nil_wf, copathAgree_wf, copath_wf, equal-wf-T-base, le_antisymmetry_iff, copath-length_wf, decidable__int_equal, subtype_base_sq, simple-game_wf, sg-legal1_wf, iff_weakening_equal, subtype_rel_self, sg-pos_wf, true_wf, squash_wf, nat_properties, le-add-cancel-alt, mul-swap, omega-shadow, zero-mul, mul-distributes-right, two-mul, add-mul-special, one-mul, le_reflexive, mul-commutes, mul-distributes, coW_wf, win2strat_wf, strat2play_wf, primrec-wf2, less_than_wf, set_wf, le-add-cancel2, mul-associates, not-lt-2, decidable__lt, multiply-is-int-iff, int_subtype_base, set_subtype_base, add-is-int-iff, coW-pos-agree_wf, int_seg_wf, all_wf, equal_wf, sq_stable__le, nat_wf, multiply_nat_wf, add_nat_wf, or_wf, lelt_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-le-2, decidable__le, false_wf, mul_bounds_1a, play-item_wf, coW-pos-lens_wf, subtract_wf, le_wf, coW-game_wf, strat2play-invariant-1
Rules used in proof : applyLambdaEquality, hyp_replacement, remainderEquality, sqequalIntensionalEquality, dependent_pairFormation, divideEquality, andLevelFunctionality, orFunctionality, equalityUniverse, promote_hyp, axiomEquality, independent_pairEquality, hypothesis_subsumption, inrFormation, inlFormation, levelHypothesis, addLevel, closedConclusion, baseApply, equalitySymmetry, equalityTransitivity, imageElimination, baseClosed, imageMemberEquality, minusEquality, intEquality, voidEquality, isect_memberEquality, addEquality, independent_isectElimination, independent_functionElimination, voidElimination, unionElimination, independent_pairFormation, multiplyEquality, dependent_set_memberEquality, functionExtensionality, instantiate, universeEquality, cumulativity, because_Cache, natural_numberEquality, functionEquality, productEquality, setElimination, rename, productElimination, hypothesis, applyEquality, lambdaEquality, sqequalRule, hypothesisEquality, isectElimination, thin, dependent_functionElimination, sqequalHypSubstitution, extract_by_obid, introduction, cut, lambdaFormation, isect_memberFormation, sqequalReflexivity, computationStep, sqequalTransitivity, sqequalSubstitution

Latex:
\mforall{}[A:\mBbbU{}'] \mforall{}B:A {}\mrightarrow{} Type. \mforall{}w,w':coW(A;a.B[a]). \mforall{}n:\mBbbN{}. \mforall{}s:win2strat(coW-game(a.B[a];w;w');n). \mforall{}moves:strat2play(coW-game(a.B[a];w;w');n;s). \mforall{}i:\mBbbN{}. (((i \mleq{} n) {}\mRightarrow{} (coW-pos-lens(moves[2 * i];i;i) \mwedge{} (coW-pos-lens(moves[(2 * i) + 1];i;i + 1) \mvee{} coW-pos-lens(moves[(2 * i) + 1];i + 1;i)))) \mwedge{} ((i \mleq{} ((2 * n) + 1)) {}\mRightarrow{} (\mforall{}j:\mBbbN{}i + 1. coW-pos-agree(a.B[a];w;w';moves[j];moves[i])))) Date html generated: 2018_07_25-PM-01_43_44 Last ObjectModification: 2018_06_16-PM-00_20_17 Theory : co-recursion Home Index