Nuprl Definition : ts-reachable
ts-reachable(ts) == {s:ts-type(ts)| ts-init(ts) (ts-rel(ts)^*) s}
Definitions occuring in Statement :
ts-rel: ts-rel(ts),
ts-init: ts-init(ts),
ts-type: ts-type(ts),
rel_star: R^*,
infix_ap: x f y,
set: {x:A| B[x]}
Definitions occuring in definition :
set: {x:A| B[x]} ,
infix_ap: x f y,
rel_star: R^*,
ts-type: ts-type(ts),
ts-rel: ts-rel(ts),
ts-init: ts-init(ts)
FDL editor aliases :
ts-reachable
Latex:
ts-reachable(ts) == \{s:ts-type(ts)| ts-init(ts) rel\_star(ts-type(ts); ts-rel(ts)) s\}
Date html generated:
2016_05_15-PM-05_39_10
Last ObjectModification:
2015_09_23-AM-07_57_41
Theory : general
Home
Index