Q 
f P == 
e:{e:E| P e} . ((f e < e) 
(Q (f e)))
Definitions :
all: x:A. B[x],
set: {x:A| B[x]} ,
es-E: E,
and: P Q,
es-causl: (e < e'),
apply: f a
FDL editor aliases :
antecedent-function
Q \mleftarrow{}{}{}f{}{} P == \mforall{}e:\{e:E| P e\} . ((f e < e) \mwedge{} (Q (f e)))
Date html generated:
2010_08_27-AM-09_41_45
Last ObjectModification:
2009_12_17-PM-10_45_29
Home
Index