Nuprl Lemma : good-sg-win2

g:SimpleGame
  ((∃Good:Pos(g) ⟶ ℙ'
     (Good[InitialPos(g)] ∧ (∀p:Pos(g). ∀q:{q:Pos(g)| Legal1(p;q)} . ∀gd:Good[p].  ∃r:{r:Pos(g)| Legal2(q;r)} Good[r])\000C))
   win2(g))


Proof




Definitions occuring in Statement :  win2: win2(g) sg-legal2: Legal2(x;y) sg-legal1: Legal1(x;y) sg-init: InitialPos(g) sg-pos: Pos(g) simple-game: SimpleGame prop: so_apply: x[s] all: x:A. B[x] exists: x:A. B[x] implies:  Q and: P ∧ Q set: {x:A| B[x]}  function: x:A ⟶ B[x]
Definitions unfolded in proof :  all: x:A. B[x] implies:  Q exists: x:A. B[x] and: P ∧ Q win2: win2(g) uall: [x:A]. B[x] member: t ∈ T nat: false: False ge: i ≥  uimplies: supposing a not: ¬A satisfiable_int_formula: satisfiable_int_formula(fmla) top: Top prop: win2strat: win2strat(g;n) so_apply: x[s] subtype_rel: A ⊆B sq_type: SQType(T) guard: {T} decidable: Dec(P) or: P ∨ Q pi1: fst(t) bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) ifthenelse: if then else fi  bfalse: ff iff: ⇐⇒ Q rev_implies:  Q squash: T int_seg: {i..j-} lelt: i ≤ j < k subtract: m goodAux: goodAux(g0;G;moves) eq_int: (i =z j) play-len: ||moves|| play-truncate: play-truncate(f;m) true: True less_than': less_than'(a;b) le: A ≤ B less_than: a < b nat_plus: + play-item: moves[i] pi2: snd(t) seq-item: s[i] nequal: a ≠ b ∈  let: let sq_stable: SqStable(P) seq-len: ||s|| seq-truncate: seq-truncate(s;n) sequence: sequence(T)
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 subtract-1-ge-0 istype-nat sg-pos_wf sg-init_wf subtype_rel_self sg-legal1_wf sg-legal2_wf simple-game_wf eq_int_wf equal-wf-base bool_wf assert_wf bnot_wf not_wf istype-assert intformnot_wf intformeq_wf int_formula_prop_not_lemma int_formula_prop_eq_lemma int_subtype_base subtype_base_sq strat2play_wf subtract_wf decidable__le itermSubtract_wf int_term_value_subtract_lemma istype-le play-len_wf subtype_rel_function uiff_transitivity eqtt_to_assert assert_of_eq_int iff_transitivity iff_weakening_uiff eqff_to_assert assert_of_bnot play-item_wf itermMultiply_wf int_term_value_mul_lemma decidable__lt itermAdd_wf int_term_value_add_lemma strat2play-invariant-1 seq-len-truncate 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 istype-false strat2play_subtype mul_bounds_1b mul-commutes mul-distributes subtract-add-cancel bool_subtype_base equal_wf squash_wf true_wf istype-universe eq_int_eq_false bfalse_wf iff_weakening_equal seq-truncate-truncate seq-truncate-item mul-swap mul-associates not-lt-2 omega-shadow minus-zero zero-mul mul-distributes-right two-mul add-mul-special one-mul le_reflexive not-equal-implies-less istype-sqequal sq_stable__le subtract_nat_wf subtype_rel-equal le-add-cancel-alt
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :lambdaFormation_alt,  sqequalHypSubstitution productElimination thin rename cut hypothesis promote_hyp Error :isect_memberFormation_alt,  introduction extract_by_obid isectElimination hypothesisEquality setElimination intWeakElimination natural_numberEquality independent_isectElimination approximateComputation independent_functionElimination Error :dependent_pairFormation_alt,  Error :lambdaEquality_alt,  int_eqEquality dependent_functionElimination Error :isect_memberEquality_alt,  voidElimination sqequalRule independent_pairFormation Error :universeIsType,  axiomEquality equalityTransitivity equalitySymmetry Error :functionIsTypeImplies,  Error :inhabitedIsType,  Error :productIsType,  Error :functionIsType,  universeEquality applyEquality instantiate because_Cache Error :setIsType,  baseClosed intEquality Error :equalityIstype,  sqequalBase baseApply closedConclusion dependentIntersection_memberEquality cumulativity Error :dependent_set_memberEquality_alt,  unionElimination functionExtensionality functionEquality setEquality productEquality equalityElimination imageElimination multiplyEquality addEquality applyLambdaEquality minusEquality hyp_replacement imageMemberEquality

Latex:
\mforall{}g:SimpleGame
    ((\mexists{}Good:Pos(g)  {}\mrightarrow{}  \mBbbP{}'
          (Good[InitialPos(g)]
          \mwedge{}  (\mforall{}p:Pos(g).  \mforall{}q:\{q:Pos(g)|  Legal1(p;q)\}  .  \mforall{}gd:Good[p].    \mexists{}r:\{r:Pos(g)|  Legal2(q;r)\}  .  Good[r]))\000C)
    {}\mRightarrow{}  win2(g))



Date html generated: 2019_06_20-PM-00_53_46
Last ObjectModification: 2019_01_02-PM-03_35_18

Theory : co-recursion-2


Home Index