Nuprl Definition : isom-games
g1 ≅ g2 ==
∃f:Pos(g1) ⟶ Pos(g2)
∃g:Pos(g2) ⟶ Pos(g1)
((∀x,y:Pos(g1). (Legal1(x;y) ⇒ Legal1(f x;f y)))
∧ (∀x,y:Pos(g1). (Legal2(x;y) ⇒ Legal2(f x;f y)))
∧ (∀x,y:Pos(g2). (Legal1(x;y) ⇒ Legal1(g x;g y)))
∧ (∀x,y:Pos(g2). (Legal2(x;y) ⇒ Legal2(g x;g y)))
∧ (∀x:Pos(g2). ((f (g x)) = x ∈ Pos(g2)))
∧ (∀x:Pos(g1). ((g (f x)) = x ∈ Pos(g1)))
∧ ((f InitialPos(g1)) = InitialPos(g2) ∈ Pos(g2))
∧ ((g InitialPos(g2)) = InitialPos(g1) ∈ Pos(g1)))
Definitions occuring in Statement :
sg-legal2: Legal2(x;y),
sg-legal1: Legal1(x;y),
sg-init: InitialPos(g),
sg-pos: Pos(g),
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
apply: f a,
function: x:A ⟶ B[x],
equal: s = t ∈ T
Definitions occuring in definition :
exists: ∃x:A. B[x],
function: x:A ⟶ B[x],
sg-legal1: Legal1(x;y),
implies: P ⇒ Q,
sg-legal2: Legal2(x;y),
all: ∀x:A. B[x],
and: P ∧ Q,
equal: s = t ∈ T,
sg-pos: Pos(g),
apply: f a,
sg-init: InitialPos(g)
FDL editor aliases :
isom-games
Latex:
g1 \mcong{} g2 ==
\mexists{}f:Pos(g1) {}\mrightarrow{} Pos(g2)
\mexists{}g:Pos(g2) {}\mrightarrow{} Pos(g1)
((\mforall{}x,y:Pos(g1). (Legal1(x;y) {}\mRightarrow{} Legal1(f x;f y)))
\mwedge{} (\mforall{}x,y:Pos(g1). (Legal2(x;y) {}\mRightarrow{} Legal2(f x;f y)))
\mwedge{} (\mforall{}x,y:Pos(g2). (Legal1(x;y) {}\mRightarrow{} Legal1(g x;g y)))
\mwedge{} (\mforall{}x,y:Pos(g2). (Legal2(x;y) {}\mRightarrow{} Legal2(g x;g y)))
\mwedge{} (\mforall{}x:Pos(g2). ((f (g x)) = x))
\mwedge{} (\mforall{}x:Pos(g1). ((g (f x)) = x))
\mwedge{} ((f InitialPos(g1)) = InitialPos(g2))
\mwedge{} ((g InitialPos(g2)) = InitialPos(g1)))
Date html generated:
2019_06_20-PM-00_52_54
Last ObjectModification:
2019_01_02-PM-01_32_15
Theory : co-recursion-2
Home
Index