Nuprl Lemma : sg-normalize_wf
∀[g:SimpleGame]. (sg-normalize(g) ∈ SimpleGame)
Proof
Definitions occuring in Statement :
sg-normalize: sg-normalize(g),
simple-game: SimpleGame,
uall: ∀[x:A]. B[x],
member: t ∈ T
Definitions unfolded in proof :
sg-normalize: sg-normalize(g),
member: t ∈ T,
uall: ∀[x:A]. B[x]
Lemmas referenced :
simple-game_wf,
sg-init_wf,
sg-change-init_wf
Rules used in proof :
equalitySymmetry,
equalityTransitivity,
axiomEquality,
hypothesis,
hypothesisEquality,
thin,
isectElimination,
sqequalHypSubstitution,
extract_by_obid,
sqequalRule,
cut,
introduction,
isect_memberFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
\mforall{}[g:SimpleGame]. (sg-normalize(g) \mmember{} SimpleGame)
Date html generated:
2018_07_25-PM-01_35_07
Last ObjectModification:
2018_06_19-PM-01_34_26
Theory : co-recursion
Home
Index