Nuprl Lemma : Game0_wf
0 ∈ Game
Proof
Definitions occuring in Statement :
Game0: 0,
Game: Game,
member: t ∈ T
Definitions unfolded in proof :
Game0: 0,
member: t ∈ T,
uall: ∀[x:A]. B[x]
Lemmas referenced :
mk-Game_wf,
nil_wf,
Game_wf
Rules used in proof :
sqequalSubstitution,
sqequalRule,
sqequalReflexivity,
sqequalTransitivity,
computationStep,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
instantiate,
hypothesis
Latex:
0 \mmember{} Game
Date html generated:
2018_05_22-PM-09_52_50
Last ObjectModification:
2018_05_20-PM-10_37_19
Theory : Numbers!and!Games
Home
Index