a,e such that R[e; a]
e
X with value F[e; a] ==
(e:E. (
e 
X 
a:A. R[e; a]))
(e:E. a:A. (R[e; a] (X(e) = F[e; a])))
Definitions :
and: P Q,
iff: P Q,
assert: b,
in-eclass: e X,
exists: x:A. B[x],
es-E: E,
all: x:A. B[x],
implies: P Q,
equal: s = t,
eclass-val: X(e)
FDL editor aliases :
es-class-def
\mforall{}a,e such that R[e; a]
e\mmember{}X with value F[e; a] ==
(\mforall{}e:E. (\muparrow{}e \mmember{}\msubb{} X \mLeftarrow{}{}\mRightarrow{} \mexists{}a:A. R[e; a])) \mwedge{} (\mforall{}e:E. \mforall{}a:A. (R[e; a] {}\mRightarrow{} (X(e) = F[e; a])))
Date html generated:
2010_08_27-PM-02_36_36
Last ObjectModification:
2010_03_23-PM-01_37_27
Home
Index