Nuprl Lemma : isom-win2
∀g1,g2:SimpleGame. (g1 ≅ g2 ⇒ {win2(g1) ⇐⇒ win2(g2)})
Proof
Definitions occuring in Statement :
isom-games: g1 ≅ g2,
win2: win2(g),
simple-game: SimpleGame,
guard: {T},
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
implies: P ⇒ Q
Definitions unfolded in proof :
rev_implies: P ⇐ Q,
prop: ℙ,
and: P ∧ Q,
iff: P ⇐⇒ Q,
guard: {T},
member: t ∈ T,
uall: ∀[x:A]. B[x],
implies: P ⇒ Q,
all: ∀x:A. B[x]
Lemmas referenced :
simple-game_wf,
isom-games_wf,
win2_wf,
isom-preserves-win2,
isom-games_inversion
Rules used in proof :
because_Cache,
dependent_functionElimination,
independent_pairFormation,
hypothesis,
independent_functionElimination,
hypothesisEquality,
thin,
isectElimination,
sqequalHypSubstitution,
extract_by_obid,
introduction,
cut,
lambdaFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
\mforall{}g1,g2:SimpleGame. (g1 \mcong{} g2 {}\mRightarrow{} \{win2(g1) \mLeftarrow{}{}\mRightarrow{} win2(g2)\})
Date html generated:
2018_07_25-PM-01_34_40
Last ObjectModification:
2018_07_11-PM-00_26_19
Theory : co-recursion
Home
Index