Nuprl Lemma : sg-legal1-change-init

[g:SimpleGame]. ∀[x,y,j:Top].  (Legal1(x;y) Legal1(x;y))


Proof




Definitions occuring in Statement :  sg-change-init: g@j sg-legal1: Legal1(x;y) simple-game: SimpleGame uall: [x:A]. B[x] top: Top sqequal: t
Definitions unfolded in proof :  pi1: fst(t) pi2: snd(t) spreadn: spread4 sg-change-init: g@j sg-legal1: Legal1(x;y) simple-game: SimpleGame member: t ∈ T uall: [x:A]. B[x]
Lemmas referenced :  simple-game_wf top_wf
Rules used in proof :  hypothesis extract_by_obid cut because_Cache sqequalAxiom sqequalRule thin productElimination sqequalHypSubstitution introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[g:SimpleGame].  \mforall{}[x,y,j:Top].    (Legal1(x;y)  \msim{}  Legal1(x;y))



Date html generated: 2018_07_25-PM-01_35_17
Last ObjectModification: 2018_06_20-PM-03_49_03

Theory : co-recursion


Home Index