% \documentclass{article}
% \title{UML2CD+Z Prelude}
% \author{Laurent Henocque\\LSIS Marseille\\laurent.henocque@lsis.org}

% \usepackage{fuzz}
% \usepackage{amssymb}

% \begin{document}

%% \begin{zed}
%%   [UNIVERSE]
%% \end{zed}

%%\begin{zed}
%%   CLASS == \power UNIVERSE
%%\end{zed}

\newcommand{\quotes}[1]{``#1"}

\newcommand{\udr}{.}
\newcommand{\udf}{.}
\newcommand{\sdr}{\rightarrow}
\newcommand{\sdf}{\rightarrow}
\newcommand{\sbr}{\leadsto}
\newcommand{\sbf}{\leadsto}
\newcommand{\saf}{\rightarrow}

%%inop \udr 6
%%inop \udf 6
%%inop \sdr 6
%%inop \sdf 6
%%inop \sbr 6
%%inop \sbf 6
%%inop \saf 6

%%\begin{gendef}[U,X]
%%   \_ \udr \_:(U \cross (U \rel X)) \fun \power X\\
%%   \_ \udf \_:(U \cross (U \fun X)) \fun X\\
%%   \_ \sdr \_:(\power U \cross (U \rel X)) \fun \power X\\
%%   \_ \sdf \_:(\power U \cross (U \fun X)) \fun \power X\\
%%   \_ \sbr \_:(\power U \cross (U \rel X)) \fun \bag X\\
%%   \_ \sbf \_:(\power U \cross (U \fun X)) \fun \bag X\\
%%   \_ \saf \_:(\power U  \cross (\power U  \fun X)) \fun X\\
%%\where
%%   \forall e1:U;e2:(U \fun X) @ e1 \udf e2 = e2(e1)\\
%%   \forall e1:U;e2:(U \rel X) @ e1 \udr e2 = e2\limg \{e1\} \rimg\\
%%   \forall e1:\power U;e2:(U \fun X) @ e1 \sdf e2 = \\
%%   \t1 \{x:U|x\in e1@e2(x)\}\\
%%   \forall e1:\power U;e2:(U \rel X) @ e1 \sdf e2 = e2\limg e1 \rimg\\
%%   \forall e1:\power U ;e2:(\power U  \fun X) @ e1 \saf e2 = e2(e1)\\
%%   \forall f:U \fun X @ \emptyset \sbf f=\lbag \rbag\\
%%   \forall f:U \fun X ; s:\power_1 U @ \forall u:s @ s \sbf f = (s \setminus \{u\}) \sbf f \uplus \lbag f(u) \rbag\\
%%   \forall f:U \rel X @ \emptyset \sbf f=\lbag \rbag\\
%%   \forall f:U \rel X ; s:\power_1 U @ \forall u:s @ s \sbr f = (s \setminus \{u\}) \sbr f \uplus \{x:X|(u,x)\in f@x\mapsto 1\}
%%\end{gendef}
%
%% \begin{axdef}
%%     bagsum:(\nat \fun \nat)\fun \nat
%% \where
%%     bagsum (\emptyset)=0\\
%%     \forall b:\nat \fun \nat@ \forall x:\dom b @ bagsum(b)=x * b(x) + bagsum(b \uminus \{x \mapsto b(x)\} )
%% \end{axdef}
%
%%\begin{gendef}[U]
%%size:\power U \fun \nat\\
%%\where
%%\forall s:\power U@ size(s)=\# s
%%\end{gendef}


% \end{document}