Nuprl Definition : simple-game
SimpleGame == Pos:Type × Pos × Pos ⟶ Pos ⟶ ℙ × (Pos ⟶ Pos ⟶ ℙ)
Definitions occuring in Statement :
prop: ℙ,
function: x:A ⟶ B[x],
product: x:A × B[x],
universe: Type
Definitions occuring in definition :
universe: Type,
product: x:A × B[x],
function: x:A ⟶ B[x],
prop: ℙ
FDL editor aliases :
simple-game
Latex:
SimpleGame == Pos:Type \mtimes{} Pos \mtimes{} Pos {}\mrightarrow{} Pos {}\mrightarrow{} \mBbbP{} \mtimes{} (Pos {}\mrightarrow{} Pos {}\mrightarrow{} \mBbbP{})
Date html generated:
2019_06_20-PM-00_51_54
Last ObjectModification:
2019_01_02-PM-01_31_14
Theory : co-recursion-2
Home
Index