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