Nuprl Definition : transition-system
transition-system{i:l} == T:Type × init:T × R:T ⟶ T ⟶ ℙ × ({s:T| init (R^*) s} ⟶ ℙ)
Definitions occuring in Statement :
rel_star: R^*,
prop: ℙ,
infix_ap: x f y,
set: {x:A| B[x]} ,
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],
set: {x:A| B[x]} ,
infix_ap: x f y,
rel_star: R^*,
prop: ℙ
Latex:
transition-system\{i:l\} == T:Type \mtimes{} init:T \mtimes{} R:T {}\mrightarrow{} T {}\mrightarrow{} \mBbbP{} \mtimes{} (\{s:T| init rel\_star(T; R) s\} {}\mrightarrow{} \mBbbP{})
Date html generated:
2016_05_15-PM-05_37_41
Last ObjectModification:
2015_09_23-AM-07_57_11
Theory : general
Home
Index