Q 
==f== P ==  
e:{e:E| P e} . (f e c
 e 
 (Q (f e)))
Definitions : 
all:
x:A. B[x], 
set: {x:A| B[x]} , 
es-E: E, 
and: P 
 Q, 
es-causle: e c
 e', 
apply: f a
FDL editor aliases : 
weak-antecedent-function
Q  \mleftarrow{}==f==  P  ==    \mforall{}e:\{e:E|  P  e\}  .  (f  e  c\mleq{}  e  \mwedge{}  (Q  (f  e)))
Date html generated:
2010_08_27-AM-09_39_04
Last ObjectModification:
2009_12_16-AM-08_53_02
Home
Index