Nuprl Lemma : coW-trans

Nuprl Lemma : coW-trans_wf

∀[A:𝕌']. ∀[B:A ⟶ Type]. ∀[w1,w2,w3:coW(A;a.B[a])]. ∀[n:ℕ]. ∀[X:win2strat(coW-game(a.B[a];w1;w2);n)].

∀[Y:win2strat(coW-game(a.B[a];w2;w3);n)].
(coW-trans(X; Y) ∈ win2strat(coW-game(a.B[a];w1;w3);n))

Proof

Definitions occuring in Statement : coW-trans: coW-trans(X; Y), coW-game: coW-game(a.B[a];w;w'), coW: coW(A;a.B[a]), win2strat: win2strat(g;n), nat: ℕ, uall: ∀[x:A]. B[x], so_apply: x[s], member: t ∈ T, function: x:A ⟶ B[x], universe: Type
Definitions unfolded in proof : uall: ∀[x:A]. B[x], member: t ∈ T, nat: ℕ, implies: P ⇒ Q, false: False, ge: i ≥ j , uimplies: b supposing a, not: ¬A, satisfiable_int_formula: satisfiable_int_formula(fmla), exists: ∃x:A. B[x], all: ∀x:A. B[x], top: Top, and: P ∧ Q, prop: ℙ, win2strat: win2strat(g;n), eq_int: (i =_z j), subtract: n - m, ifthenelse: if b then t else f fi , btrue: tt, so_lambda: λ₂x.t[x], so_apply: x[s], decidable: Dec(P), or: P ∨ Q, subtype_rel: A ⊆r B, guard: {T}, bool: 𝔹, unit: Unit, it: ⋅, uiff: uiff(P;Q), bfalse: ff, iff: P ⇐⇒ Q, rev_implies: P ⇐ Q, sq_type: SQType(T), transMoves: transMoves(X;Y;moves), play-len: ||moves||, seq-len: ||s||, pi1: fst(t), seq-truncate: seq-truncate(s;n), strat2play: strat2play(g;n;s), sequence: sequence(T), play-item: moves[i], int_seg: {i..j^-}, lelt: i ≤ j < k, coW-game: coW-game(a.B[a];w;w'), sg-pos: Pos(g), squash: ↓T, true: True, sg-init: InitialPos(g), sg-legal1: Legal1(x;y), pi2: snd(t), lt_int: i <z j, le: A ≤ B, less_than': less_than'(a;b), copath-length: copath-length(p), copath-nil: (), let: let, seq-add: seq-add(s;x), seq-nil: seq-nil(), bnot: ¬_bb, assert: ↑b, seq-item: s[i], cand: A c∧ B, sg-legal2: Legal2(x;y), coWtransInvariant: coWtransInvariant(x.B[x];w1;w2;w3;k;X;Y;a;b;moves), label: ...$L... t, copath: copath(a.B[a];w), copathAgree: copathAgree(a.B[a];w;x;y), play-truncate: play-truncate(f;m), coW-trans: coW-trans(X; Y), rev_uimplies: rev_uimplies(P;Q), nequal: a ≠ b ∈ T , nat_plus: ℕ⁺, coW-pos-lens: coW-pos-lens(p;i;j)
Lemmas referenced : nat_properties, full-omega-unsat, intformand_wf, intformle_wf, itermConstant_wf, itermVar_wf, intformless_wf, istype-int, int_formula_prop_and_lemma, istype-void, int_formula_prop_le_lemma, int_term_value_constant_lemma, int_term_value_var_lemma, int_formula_prop_less_lemma, int_formula_prop_wf, ge_wf, istype-less_than, win2strat_wf, coW-game_wf, decidable__le, intformnot_wf, int_formula_prop_not_lemma, istype-le, subtract-1-ge-0, istype-nat, coW_wf, istype-universe, eq_int_wf, equal-wf-base, bool_wf, int_subtype_base, assert_wf, bnot_wf, not_wf, istype-assert, intformeq_wf, int_formula_prop_eq_lemma, win2strat_subtype, strat2play_wf, subtract_wf, itermSubtract_wf, int_term_value_subtract_lemma, play-len_wf, uiff_transitivity, eqtt_to_assert, assert_of_eq_int, iff_transitivity, iff_weakening_uiff, eqff_to_assert, assert_of_bnot, bool_cases, subtype_base_sq, bool_subtype_base, mul-distributes, add-associates, mul-commutes, add-swap, add-commutes, zero-add, decidable__equal_int, itermAdd_wf, itermMultiply_wf, int_term_value_add_lemma, int_term_value_mul_lemma, copath_length_nil_lemma, play-item_wf, decidable__lt, strat2play-invariant-1, sg-legal1_wf, squash_wf, true_wf, sg-pos_wf, simple-game_wf, subtype_rel_self, iff_weakening_equal, equal_wf, nat_wf, set_subtype_base, le_wf, istype-false, copath-length_wf, lt_int_wf, assert_of_lt_int, int_seg_properties, bool_cases_sqequal, assert-bnot, less_than_wf, copath-nil_wf, int_seg_wf, seq-len_wf, seq-item_wf, sg-init_wf, copathAgree-nil, sg-legal2_wf, copath_wf, coWtransInvariant_wf, pi1_wf, pi2_wf, subtype_rel_wf, add_functionality_wrt_eq, strat2play_subtype, le-add-cancel, le_antisymmetry_iff, mul-associates, equal-wf-T-base, mul_preserves_le, le-add-cancel2, add-zero, less-iff-le, le-add-cancel-alt, add_functionality_wrt_le, minus-one-mul-top, minus-minus, minus-add, minus-one-mul, condition-implies-le, not-le-2, false_wf, play-truncate_wf, less_than_transitivity1, le_weakening2, strat2play_subtype_le, not-lt-2, add-mul-special, zero-mul, lelt_wf, seq-len-truncate, sequence_wf, seq-truncate_wf, add-is-int-iff, subtract-add-cancel, bfalse_wf, not-equal-2, eq_int_eq_false, win2strat-properties, seq-truncate-item, le_reflexive, coW-play-invariant, mod2-2n, mod2-2n-plus-1, strat2play-invariant, and_wf, or_wf, less_than_irreflexivity, le_int_wf, assert_functionality_wrt_uiff, bnot_of_lt_int, assert_of_le_int, copathAgree_wf, strat2play-add, add-subtract-cancel, mul-distributes-right, copathAgree_refl, istype_wf, subtype_rel_set, seq-add_wf, seq-add-len, strat2play-longer, le_weakening, coW-pos-lens_wf, intformor_wf, int_formula_prop_or_lemma
Rules used in proof : sqequalSubstitution, sqequalTransitivity, computationStep, sqequalReflexivity, Error :isect_memberFormation_alt, introduction, cut, extract_by_obid, sqequalHypSubstitution, isectElimination, thin, hypothesisEquality, hypothesis, setElimination, rename, sqequalRule, intWeakElimination, Error :lambdaFormation_alt, natural_numberEquality, independent_isectElimination, approximateComputation, independent_functionElimination, Error :dependent_pairFormation_alt, Error :lambdaEquality_alt, int_eqEquality, dependent_functionElimination, Error :isect_memberEquality_alt, voidElimination, independent_pairFormation, Error :universeIsType, axiomEquality, equalityTransitivity, equalitySymmetry, Error :isectIsTypeImplies, Error :inhabitedIsType, Error :functionIsTypeImplies, applyEquality, Error :dependent_set_memberEquality_alt, unionElimination, because_Cache, instantiate, cumulativity, Error :functionIsType, universeEquality, baseApply, closedConclusion, baseClosed, intEquality, Error :equalityIstype, sqequalBase, dependentIntersectionElimination, dependentIntersection_memberEquality, functionExtensionality, setEquality, equalityElimination, productElimination, multiplyEquality, Error :setIsType, Error :productIsType, addEquality, imageElimination, imageMemberEquality, hyp_replacement, applyLambdaEquality, independent_pairEquality, Error :dependent_pairEquality_alt, promote_hyp, Error :inlFormation_alt, dependentIntersectionEqElimination, voidEquality, Error :inrFormation_alt, Error :equalityIsType4, minusEquality, Error :equalityIsType1, dependent_set_memberEquality, lambdaFormation, lambdaEquality, isect_memberEquality, productEquality, Error :unionIsType, Error :equalityIsType2, unionEquality, Error :equalityIsType3, pointwiseFunctionality

Latex:
\mforall{}[A:\mBbbU{}']. \mforall{}[B:A {}\mrightarrow{} Type]. \mforall{}[w1,w2,w3:coW(A;a.B[a])]. \mforall{}[n:\mBbbN{}]. \mforall{}[X:win2strat(coW-game(a.B[a];w1;w2);n)]. \mforall{}[Y:win2strat(coW-game(a.B[a];w2;w3);n)]. (coW-trans(X; Y) \mmember{} win2strat(coW-game(a.B[a];w1;w3);n)) Date html generated: 2019_06_20-PM-01_10_53 Last ObjectModification: 2019_01_02-PM-04_22_25 Theory : co-recursion-2 Home Index