Nuprl Definition : class-pred
class-pred(X;es;e) == last(λe'.0 <z #(X es e')) e
Definitions occuring in Statement :
es-local-pred: last(P),
lt_int: i <z j,
apply: f a,
lambda: λx.A[x],
natural_number: $n,
bag-size: #(bs)
FDL editor aliases :
class-pred
Latex:
class-pred(X;es;e) == last(\mlambda{}e'.0 <z \#(X es e')) e
Date html generated:
2016_05_16-PM-11_18_48
Last ObjectModification:
2012_02_25-PM-01_59_20
Theory : event-ordering
Home
Index