Nuprl Definition : prior_iterated_classrel
s ∈ prior(X*(f,init,e)) ==
((↑first(e)) ∧ s ↓∈ init loc(e)) ∨ ((¬↑first(e)) ∧ iterated_classrel(es;S;A;f;init;X;pred(e);s))
Definitions occuring in Statement :
iterated_classrel: iterated_classrel(es;S;A;f;init;X;e;v),
es-first: first(e),
es-pred: pred(e),
es-loc: loc(e),
assert: ↑b,
not: ¬A,
or: P ∨ Q,
and: P ∧ Q,
apply: f a,
bag-member: x ↓∈ bs
FDL editor aliases :
prior_iterated_classrel
s \mmember{} prior(X*(f,init,e)) ==
((\muparrow{}first(e)) \mwedge{} s \mdownarrow{}\mmember{} init loc(e)) \mvee{} ((\mneg{}\muparrow{}first(e)) \mwedge{} iterated\_classrel(es;S;A;f;init;X;pred(e);s))
Date html generated:
2015_07_17-PM-00_25_24
Last ObjectModification:
2012_02_25-PM-01_15_36
Home
Index