Nuprl Lemma : Game-induction
∀[P:Game ⟶ ℙ']
((∀g:Game. ((∀m:Game. ((left-option{i:l}(g;m) ∨ right-option{i:l}(g;m)) ⇒ P[m])) ⇒ P[g])) ⇒ {∀g:Game. P[g]})
Proof
Definitions occuring in Statement :
right-option: right-option{i:l}(g;m),
left-option: left-option{i:l}(g;m),
Game: Game,
uall: ∀[x:A]. B[x],
prop: ℙ,
guard: {T},
so_apply: x[s],
all: ∀x:A. B[x],
implies: P ⇒ Q,
or: P ∨ Q,
function: x:A ⟶ B[x]
Definitions unfolded in proof :
guard: {T},
uall: ∀[x:A]. B[x],
implies: P ⇒ Q,
all: ∀x:A. B[x],
member: t ∈ T,
so_lambda: λ2x.t[x],
so_apply: x[s],
Game: Game,
prop: ℙ,
subtype_rel: A ⊆r B,
or: P ∨ Q,
Wsup: Wsup(a;b),
left-option: left-option{i:l}(g;m),
left-move: left-move(g;x),
left-indices: left-indices(g),
pi1: fst(t),
pi2: snd(t),
exists: ∃x:A. B[x],
right-option: right-option{i:l}(g;m),
right-move: right-move(g;x),
right-indices: right-indices(g),
GameB: GameB(p),
GameA: GameA{i:l}(),
uimplies: b supposing a,
iff: P ⇐⇒ Q,
and: P ∧ Q,
rev_implies: P ⇐ Q
Lemmas referenced :
W-induction,
GameA_wf,
GameB_wf,
Game_wf,
all_wf,
or_wf,
left-option_wf,
right-option_wf,
Wsup_wf,
subtype_rel_self,
W_wf,
subtype_rel_union,
iff_weakening_equal
Rules used in proof :
sqequalSubstitution,
sqequalRule,
sqequalReflexivity,
sqequalTransitivity,
computationStep,
isect_memberFormation,
lambdaFormation,
cut,
thin,
instantiate,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
hypothesis,
lambdaEquality,
cumulativity,
hypothesisEquality,
independent_functionElimination,
dependent_functionElimination,
functionEquality,
applyEquality,
universeEquality,
because_Cache,
functionExtensionality,
equalityTransitivity,
equalitySymmetry,
unionElimination,
productElimination,
inlEquality,
voidEquality,
independent_isectElimination,
voidElimination,
inrEquality
Latex:
\mforall{}[P:Game {}\mrightarrow{} \mBbbP{}']
((\mforall{}g:Game. ((\mforall{}m:Game. ((left-option\{i:l\}(g;m) \mvee{} right-option\{i:l\}(g;m)) {}\mRightarrow{} P[m])) {}\mRightarrow{} P[g]))
{}\mRightarrow{} \{\mforall{}g:Game. P[g]\})
Date html generated:
2018_05_22-PM-09_52_41
Last ObjectModification:
2018_05_20-PM-10_37_08
Theory : Numbers!and!Games
Home
Index