Nuprl Lemma : isom-games_inversion
∀[g1,g2:SimpleGame]. (g1 ≅ g2 ⇒ g2 ≅ g1)
Proof
Definitions occuring in Statement :
isom-games: g1 ≅ g2,
simple-game: SimpleGame,
uall: ∀[x:A]. B[x],
implies: P ⇒ Q
Definitions unfolded in proof :
all: ∀x:A. B[x],
so_apply: x[s],
so_lambda: λ2x.t[x],
prop: ℙ,
cand: A c∧ B,
and: P ∧ Q,
member: t ∈ T,
exists: ∃x:A. B[x],
isom-games: g1 ≅ g2,
implies: P ⇒ Q,
uall: ∀[x:A]. B[x]
Lemmas referenced :
simple-game_wf,
isom-games_wf,
exists_wf,
sg-init_wf,
equal_wf,
sg-legal2_wf,
sg-legal1_wf,
sg-pos_wf,
all_wf
Rules used in proof :
applyEquality,
functionEquality,
lambdaEquality,
sqequalRule,
isectElimination,
extract_by_obid,
introduction,
productEquality,
independent_pairFormation,
hypothesis,
cut,
hypothesisEquality,
dependent_pairFormation,
thin,
productElimination,
sqequalHypSubstitution,
lambdaFormation,
isect_memberFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
\mforall{}[g1,g2:SimpleGame]. (g1 \mcong{} g2 {}\mRightarrow{} g2 \mcong{} g1)
Date html generated:
2018_07_25-PM-01_34_08
Last ObjectModification:
2018_07_11-PM-00_26_43
Theory : co-recursion
Home
Index