Nuprl Lemma : sg-init_wf
∀[g:SimpleGame]. (InitialPos(g) ∈ Pos(g))
Proof
Definitions occuring in Statement : 
sg-init: InitialPos(g)
, 
sg-pos: Pos(g)
, 
simple-game: SimpleGame
, 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
Definitions unfolded in proof : 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
, 
sg-init: InitialPos(g)
, 
simple-game: SimpleGame
, 
pi1: fst(t)
, 
pi2: snd(t)
, 
sg-pos: Pos(g)
Lemmas referenced : 
simple-game_wf
Rules used in proof : 
sqequalSubstitution, 
sqequalTransitivity, 
computationStep, 
sqequalReflexivity, 
isect_memberFormation, 
introduction, 
cut, 
sqequalRule, 
sqequalHypSubstitution, 
productElimination, 
thin, 
hypothesisEquality, 
hypothesis, 
axiomEquality, 
equalityTransitivity, 
equalitySymmetry, 
extract_by_obid
Latex:
\mforall{}[g:SimpleGame].  (InitialPos(g)  \mmember{}  Pos(g))
Date html generated:
2018_07_25-PM-01_31_05
Last ObjectModification:
2018_06_06-AM-10_44_01
Theory : co-recursion
Home
Index