Nuprl Definition : prior_iterated_classrel
s 
prior(X*(f,init,e)) == ((
first(e)) 
s 
init loc(e)) 
((
first(e)) s X*(f,init,pred(e)))
Definitions occuring in Statement :
iterated_classrel: v X*(f,init,e),
es-pred: pred(e),
es-first: first(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{} s \mmember{} X*(f,init,pred(e)))
Date html generated:
2012_01_23-PM-12_21_36
Last ObjectModification:
2012_01_20-AM-02_47_44
Home
Index