Nuprl Definition : prior-iterated-classrel
prior-iterated-classrel(es;A;S;s;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
prior-iterated-classrel(es;A;S;s;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_26_18
Last ObjectModification:
2012_03_26-PM-11_52_01
Home
Index