Nuprl Definition : iterated_classrel
v 
X*(f,init,e) ==
Y
(
iterated_classrel,e,v.
(
z:S
(if first(e) then z init loc(e) else iterated_classrel pred(e) z fi
((a:A. (a X(e) (v = (f a z)))) 
((
a:A. (
a X(e))) (v = z))))))
e
v
Definitions occuring in Statement :
classrel: v X(e),
es-pred: pred(e),
es-first: first(e),
es-loc: loc(e),
ifthenelse: if b then t else f fi ,
ycomb: Y,
all: x:A. B[x],
exists: x:A. B[x],
not: A,
squash: T,
or: P Q,
and: P Q,
apply: f a,
lambda: x.A[x],
equal: s = t,
bag-member: x bs
FDL editor aliases :
iterated_classrel
iterated_classrel
iterated_classrel
iterated_classrel
v \mmember{} X*(f,init,e) ==
Y
(\mlambda{}iterated$_{classrel}$,e,v.
(\mdownarrow{}\mexists{}z:S
(if first(e) then z \mdownarrow{}\mmember{} init loc(e) else iterated$_{classrel}$ pred(e) z f\000Ci
\mwedge{} ((\mexists{}a:A. (a \mmember{} X(e) \mwedge{} (v = (f a z)))) \mvee{} ((\mforall{}a:A. (\mneg{}a \mmember{} X(e))) \mwedge{} (v = z))))))
e
v
Date html generated:
2012_01_23-PM-12_19_09
Last ObjectModification:
2012_01_09-PM-03_19_44
Home
Index