\documentclass[twoside]{article}
% This file was generated from SGML source --- DO NOT EDIT
\usepackage{oratr,z-eves}
\title{The Z/EVES 2.0 Mathematical Toolkit}
\author{Mark Saaltink}
\trproject{Z/EVES Project}
\trnumber{TR-99-5493-05b}
\date{October 1999}
\begin{document}
\maketitle
\pagenumbering{roman}
\thispagestyle{empty} %% make TOC start on an odd page!
\mbox{} %% something to put on the page
\setcounter{page}{0}
\cleardoublepage
\tableofcontents
\cleardoublepage
\pagenumbering{arabic}
\section{Introduction }

The Z/EVES Mathematical Toolkit\footnote{This work was funded by the
United States Department of Defense under contract MDA904-95-C-2031.}
includes the declaration of all the
constants of the Standard Mathematical Toolkit as described by
Spivey~\cite{Spivey-ZRM}
or the proposed ISO Standard for Z~\cite{Z-Std-CD},
and presents useful theorems about these constants.
The theorems are divided into two groups.  The first group contains theorems
meant for
human consumption, which are presented in the most natural way.  The second
group contains theorems meant for the prover to use automatically,
which are presented in
whatever way will work best.  Often, however, many theorems in the human
consumption group are also suitable for automatic use, and are marked as
rewrite rules.


This report is the specification of the standard ``toolkit'' section
distributed with Z/EVES, Version 2.0~\cite{Z-EVES-RM}.


The toolkit defines operations in several categories, which we summarize here.
For each operation, we show its {\LaTeX} markup command (needed for users of
the command line interface to Z/EVES, but not by users of the graphical
interface), give the page of this report containing its definition (or the
main theorems about it), and a brief description of its meaning.



\newcommand\xpageref[1]{p.~\pageref{#1}}

\newenvironment{ops}%
{\begin{tabular}{p{2.7cm}p{3.9cm}p{.9cm}p{5.5cm}}}%
{\end{tabular}}


\begin{ops}
{\bf General} \\
\\
$KnownMember$ & \verb$KnownMember$ &
	\xpageref{weakening} & membership (for ``weakening'' rules) \\
$\mu x: S$ & \verb'\mu x: S' &
	\xpageref{rules-mu} & definite description terms \\
$x \neq y$ & \verb$x \neq y$ &
	\xpageref{def-neq} & not equal \\
$x \notin y$ & \verb$x \notin y$ &
	\xpageref{def-neq} & not a member \\
\\
\end{ops}




\begin{ops}
{\bf Sets}\\
\\
$\power X$ & \verb$\power X$ &
	\xpageref{rules-power} &  powerset \\
$X \cross Y$ & \verb$X \cross Y$ &
	\xpageref{rules-cross} & cross product \\
$\emptyset$ & \verb$\emptyset$ &
	\xpageref{def-emptyset} & empty set \\
$\power_1 X$ & \verb$\power_1 X$ &
	\xpageref{def-power1} & non-empty powerset \\
$S \subseteq T$ & \verb$S \subseteq T$ &
	\xpageref{def-subseteq} & subset relation \\
$S \subset T$ & \verb$S \subset T$ &
	\xpageref{def-subseteq} & proper subset relation \\
$S \cup T$ & \verb$S \cup T$ &
	\xpageref{def-cup} & set union \\ 
$S \cap T$ & \verb$S \cap T$ &
	\xpageref{def-cap} & set intersection \\
$S \setminus T$ & \verb$S \setminus T$ &
	\xpageref{def-setminus} & set difference (relative complement)\\
$\bigcup S, \bigcap S$ & \verb$\bigcup S, \bigcap S$ &
	\xpageref{def-bigcup} & generalized union or intersection \\
\\
\end{ops}




\begin{ops}
\multicolumn{2}{l}{{\bf Ordered Pairs}}\\
\\
$first$ & \verb$first$ &
	\xpageref{def-first} & first component of a pair\\
$second$ & \verb$second$ &
	\xpageref{def-first} & second component of a pair\\
$x \mapsto y$ & \verb$x \mapsto y$ &
	\xpageref{def-maplet} & maplets \\
\\
\end{ops}



\begin{ops}
\multicolumn{2}{l}{{\bf Relations}}\\
\\
$X \rel Y$ & \verb$X \rel Y$ &
	\xpageref{rules-rel} & relation space \\
$\dom R, \ran R$ & \verb$\dom R, \ran R$ &
	\xpageref{def-dom} & domain, range of a relation \\
$\id S$ & \verb$\id S$ &
	\xpageref{def-id} & identity relation \\
$Q \comp R, R \circ Q$ & \verb$Q \comp R, R \circ Q$ &
	\xpageref{def-comp} & composition \\
$S \dres R$ & \verb$S \dres R$ &
	\xpageref{def-dres} & domain restriction \\
$R \rres S$ & \verb$R \rres S$ &
	\xpageref{def-dres} & range restriction \\
$S \ndres R$ & \verb$S \ndres R$ &
	\xpageref{def-ndres} & domain anti-restriction \\
$R \nrres S$ & \verb$R \nrres S$ &
	\xpageref{def-ndres} & range anti-restriction \\
$R \inv$ & \verb$R \inv$ &
	\xpageref{def-inv} & inverse relation\\
$R \limg S \rimg$ & \verb$R \limg S \rimg$ &
	\xpageref{def-image} & relational image \\
$Q \oplus R$ & \verb$Q \oplus R$ &
	\xpageref{def-oplus} & overriding \\
$R\plus, R\star$ & \verb$R\plus, R\star$ &
	\xpageref{def-tclosure} & transitive closure\\
$R \bsup k \esup$ & \verb$R \bsup k \esup$ &
	\xpageref{def-iter} & iterate of a relation \\
\\
\end{ops}




\begin{ops}
\multicolumn{2}{l}{{\bf Functions}}\\
\\
$X \pfun Y, X \fun Y$ & \verb$X \pfun Y, X \fun Y$ &
	\xpageref{def-pfun} & function spaces \\
$X \pinj Y, X \inj Y$ & \verb$X \pinj Y, X \inj Y$ &
	\xpageref{def-pinj} & injective (1-1) function spaces \\
$X \psurj Y, X \surj Y$ & \verb$X \psurj Y, X \surj Y$ &
	\xpageref{def-psurj} & surjective (onto) function spaces \\
$X \bij Y$ & \verb$X \bij Y$ &
	\xpageref{def-bij} & bijections \\
$X \ffun Y, X \finj Y$ & \verb$X \ffun Y, X \finj Y$ &
	\xpageref{def-ffun} & finite functions \\
$g \circ f$ & \verb$g \circ f$ &
	\xpageref{def-comp} & composition \\
$f \limg S \rimg$ & \verb$f \limg S \rimg$ &
	\xpageref{def-image} & image \\
$f \oplus g$ & \verb$f \oplus g$ &
	\xpageref{def-oplus} & overriding \\
$f \bsup n \esup$ & \verb$f \bsup n \esup$ &
	\xpageref{def-iter} & iterate of a function \\
$f~ applies\$to~ x$ & \verb'f~applies\$to~x' & 
	\xpageref{rules-appliesTo} & applicability \\
\\
\end{ops}




\begin{ops}
\multicolumn{2}{l}{{\bf Numbers and finiteness}}\\
\\
$\nat, \nat_1$ & \verb$\nat, \nat_1$ &
	\xpageref{def-nat} & natural numbers \\
$succ(n)$ & \verb$succ(n)$ & 
	\xpageref{def-nat} & successor ($n + 1$) \\
$k \upto n$ & \verb$k \upto n$ &
	\xpageref{def-upto} & ranges \\
$min~S, max~S$ & \verb$min~S, max~S$ &
	\xpageref{def-min} & minimum and maximum \\
$\finset X$ & \verb$\finset X$ &
	\xpageref{def-finset} & finite subsets \\
$\finset_1 X$ & \verb$\finset_1 X$ &
	\xpageref{def-finset} & non-empty finite subsets \\
$\# S$ & \verb$\# S$ &
	\xpageref{def-size} & cardinality \\
\\
\end{ops}




\begin{ops}
\multicolumn{2}{l}{{\bf Sequences}}\\
\\
$\seq X, \seq_1 X$ & \verb$\seq X, \seq_1 X$ &
	\xpageref{def-seq} & sequences \\
$\iseq X$ & \verb$\iseq X$ &
	\xpageref{def-seq} & injective sequences \\
$s \cat t$ & \verb$s \cat t$ &
	\xpageref{def-cat} & concatenation \\
$\dcat s$ & \verb$\dcat s$ &
	\xpageref{def-dcat} & distributed concatenation \\
$head~s, last~s$ & \verb$head~s, last~s$ &
	\xpageref{def-head} & first (last) element \\
$tail~s, front~s$ & \verb$tail~s, front~s$ &
	\xpageref{def-head} & parts of a sequence \\
$rev~s$ & \verb$rev~s$ &
	\xpageref{def-rev} & reversal \\
$S \extract s$ & \verb$S \extract s$ &
	\xpageref{def-filter} & selection of a subsequence\\
$s \filter S$ & \verb$s \filter S$ &
	\xpageref{def-filter} & selection of a subsequence\\
$squash(f)$ & \verb$squash(f)$ &
	\xpageref{def-filter} & creation of a sequence \\
$s \prefix t$ &
	\verb$s \prefix t$ &
	\xpageref{def-prefix} & subsequence relations \\
$s \suffix t$ &
	\verb$s \suffix t$ &
	\xpageref{def-prefix} & subsequence relations \\
$s \inseq t$ &
	\verb$s \inseq t$ &
	\xpageref{def-prefix} & subsequence relations \\
$\disjoint s$ & \verb$\disjoint s$ &
	\xpageref{def-disjoint} & disjointness \\
$\partition s$ & \verb$\partition s$ &
	\xpageref{def-disjoint} & partitions \\
\\
\end{ops}




\begin{ops}
{\bf Bags}\\
\\
$\bag X$ & \verb$\bag X$ &
	\xpageref{def-bag} & bags (multisets)\\
$count~B, B \bcount x$ & \verb$count~B, B \bcount x$ &
	\xpageref{def-inbag} & multiplicity in a bag \\
$x \inbag B$ & \verb$x \inbag B$ &
	\xpageref{def-inbag} & membership in a bag \\
$A \subbageq B$ & \verb$A \subbageq B$ &
	\xpageref{def-subbageq} & subbag relationship \\
$n \otimes B$ & \verb$n \otimes B$ &
	\xpageref{def-otimes} & bag scaling \\
$A \uplus B$ & \verb$A \uplus B$ &
	\xpageref{def-uplus} & bag union \\
$A \uminus B$ & \verb$A \uminus B$ &
	\xpageref{def-uminus} & bag difference \\
$items(s)$ & \verb$items(s)$ &
	\xpageref{def-items} & bag of elements from a sequence \\
\end{ops}



\subsection{Changes since Version 2.2 }

There have been several changes from Version 2.2 of the Toolkit:
\begin{enumerate}
\item{}  A number of rewriting rules have been disabled, as they were in general
quite inefficient.  These rules were capable of causing the prover to do
lots of work on subgoals that usually failed.  Where possible, simple cases
of these rules, that recognize special cases syntactically, have been added.
\item{}  The induction theorems have been rewritten to use $\_ \subseteq \_$
in their conclusions, and have been made disabled rewrite rules.  This makes
them slightly easier to use, since they can be applied, with the rewriter
working out the instantiation.
\item{}  A few theorems were generalized to be applicable in cases where
non-maximal generic actuals are used.
\item{}  Several new theorems were added.
\item{}  Five errors were corrected.
\end{enumerate}


\newpage

\section{Automation strategies }

Before presenting the specification of the Toolkit, we will discuss some
of the technical issues that influence the form of its theorems.
This section is rather technical and should be skipped on first reading.


\subsection{Weakening }\label{describe-weakening}

There is a basic rewriting strategy that colours much of the Toolkit
theory.  It is a bit tricky to automate ``weakening'' proofs, where
membership in a large set is inferred from membership in a small set.
For example,
$x \in \nat \cross \nat_1$ implies
$x \in \num \cross \nat$.
These sorts of goals arise all the time, and should be trivial to prove.


We adopt the following approach:
\begin{itemize}
\item{} Given a global constant declared as
$c: T$, a  grule
$c \in T$ is automatically generated.
(Such theorems must be added by hand for constants declared as
abbreviations.  We give these theorems names of the form
$x\_type$.)
\item{} A special ``known membership'' function is defined, and we
add a forward rule
$x \in S \implies x~knownIn~S$ and another
$ \lnot x \in S \implies \lnot x ~knownIn~S$.  (Unfortunately, a
$knownIn$
relation is unsuitable here, as it would need a generic parameter.  Therefore,
we use a generic schema
$KnownMember$, with the set as the generic actual and
component
$element$ as the member.)
\item{} We add the rewrite rule
$x~knownIn~T \land T \in\power S \implies x \in S$.
We similarly add
$\lnot x~knownIn~T \land S \in\power T \implies \lnot x \in S$.
\end{itemize}

Most weakening proofs give rise to subgoals of the form
$S \in \power T$.  If
$S$ is itself a global constant, the weakening rule
can apply again.
We also give rules for such subgoals for interesting
cases of $S$ and $T$ below.  For example,
$A \pfun B \in\power (A' \pfun B')
\iff A \in \power A' \land B \in \power B'$.  These theorems have names
ending with ``$\_sub$''.  Generally, these rules express the monotonicity
of set constructors such as $\_ \pfun \_$, $\finset \_$ and
$\seq \_$.


\subsection{Ideal rules }

Theorems expressing properties inherited by subsets
are also worth automating. 
For example, any subset of a relation
is a relation, any subset of a partial function is a partial function, and
any subset of a finite set is a finite set.


This sort of reasoning plays out as follows: the fact that
$X$ is a subset of  $Y$ is recorded as
$X \in\power Y$.  Thus, if we are trying to show  $X \in I$,
the weakening rule will give a subgoal of the form
$\power Y \in \power I$.
If $I$ is one of
the sets mentioned above (e.g., $I = A \rel B$ or \ldots, or
$I = \finset A$), then
$\power Y \in \power I \iff Y \in I$.  Thus, adding this
$\_ideal$ rule for each different set
$I$ is enough to allow the automation of these proofs.


\subsection{Facts about function results }

A general rule gives the fact $f(x) \in R$ if
$f \in D \pfun R$ and
$x \in \dom f$---that is, function applications have values in the range of
the function.


In cases where a tighter containing set is available for a function
application, it may be useful to give an additional weakening rule.
For example, the domain restriction ($S \dres R$) is a subset of
$R$, whereas from the declaration of
$\_ \dres \_$ we can conclude only that it is a subset of
$X \rel Y$ (where $X \rel Y$ is the type of $R$).
This fact about domain restriction could be expressed by the predicate
$$\forall S: \power X; R: X \rel Y @ S \dres R \subseteq R.$$


It is possible to express this fact in a form that can be used more
automatically by EVES, by writing instead the rule
$$\forall S: \power X; R X \rel Y | \power R \in \power Z @
     S \dres R \in Z.$$
This form interacts particularly well with the ``ideal'' rules.  For example,
if $Z$ is an ideal set, then the subgoal
$\power R \in \power Z$ will be rewritten to
$R \in Z$---so, for example, if $R$ is an injection, Z/EVES can
conclude that $S \dres R$ is also an injection.


These theorems are given names ending in  $\_result$.


\subsection{Computation rules }

It is useful to be able to use Z/EVES to calculate the value of a Z expression,
such as
$\dom \{ 1 \mapsto 1, 2 \mapsto 4, 3 \mapsto 9\}$.


Set constructions, sequence constructions, and bag constructions are in
fact formed from three primitives: a constant for the empty value (e.g., 
$\{\}$,
$\langle \rangle$, or
$\lbag \rbag$); a constructor for singletons;
and a ``join'' operation ($\_ \cup \_$ for sets,
$\_ \cat \_$ for sequences,
and
$\_ \uplus \_$ for bags).  For example,
$\{1, 2, 3\}$ is really just
an abbreviation for
$\{ 1 \} \cup \{ 2 \} \cup \{ 3 \}$).


In writing enough rewrite rules to allow for computations of functions
applied to constructions, it is therefore necessary to cover the three cases
(empty, unit, join).  Wherever possible in this Toolkit, we have included
enough such rules to allow these computations to be performed.
For example, the three rules
$domEmpty$,
$domSingleton$, and
$domCup$ are enough to allow domains of explicitly given relations to be
computed by rewriting.

\newpage

\section{Weakening }\label{weakening}

Here is the definition of the ``known membership'' relation.  As
explained in Section~\ref{describe-weakening}, it is necessary to use
a schema rather than a relation.



\subsection*{Definitions}


\begin[disabled]{schema}{KnownMember[X]}
  element: X
\end{schema}


\subsection*{Theorems}


\begin{theorem}{frule knownMember}[X]
  element \in X \implies KnownMember[X]
\end{theorem}



\begin{theorem}{rule weakening}
  KnownMember[X] \land X \in \power Y
\implies
  element \in Y
\end{theorem}


\newpage

\section{Tuples }

Tuples are part of the Z notation.  We present the main theorems
used in proofs.


\subsection{Two-element tuples }


\begin{theorem}{grule select\_2\_1}
  (x,y).1 = x
\end{theorem}


\begin{theorem}{grule select\_2\_2}
  (x,y).2 = y
\end{theorem}


\begin{theorem}{rule eqTuple2}
  (x,y) = (x',y')
\iff
  x = x' \land y = y'
\end{theorem}


\begin{theorem}{rule select\_1\_member}
  x \in X \cross Y
\implies x.1 \in X
\end{theorem}


\begin{theorem}{rule select\_2\_member}
  x \in X \cross Y
\implies x.2 \in Y
\end{theorem}


\begin{theorem}{grule tupleComposition2}
  x \in X \cross Y
\implies x = (x.1, x.2)
\end{theorem}


\subsection{Three-element tuples }


\begin{theorem}{grule select\_3\_1}
  (x,y,z).1 = x
\end{theorem}


\begin{theorem}{grule select\_3\_2}
  (x,y,z).2 = y
\end{theorem}


\begin{theorem}{grule select\_3\_3}
  (x,y,z).3 = z
\end{theorem}


\begin{theorem}{rule eqTuple3}
  (x,y,z) = (x',y',z')
\iff
  x = x' \land y = y' \land z = z'
\end{theorem}

\newpage

\section{Mu terms }\label{rules-mu}

Mu terms are treated specially by Z/EVES; a term of the form
$\mu ST @ e$ is converted into
$\mu m: \{ ST @ e\}$ (unless it already
has this form
$\mu x: S$ for some set
$S$).  This latter form is treated as
a function of
$S$.



\subsection*{Theorems}

We present here some of the theorems needed for dealing with mu terms.



\begin{theorem}{muInSet}[S]
  (\exists a: S @ \forall b: S @ b = a)
\implies
  (\mu x: S) \in S
\end{theorem}


\begin{theorem}{muValue}[S]
                s \in S
         \land (\forall s': S @ s' = s)
\implies (\mu x: S) = s
\end{theorem}


\subsection*{Automation}

We generally do not provide much automation for mu terms.  When a mu term
appears in an equality, we can do a bit better, since we then have a candidate
value for the expression.



\begin{theorem}{rule muValue1}[S]
  \forall s: S | (\forall s': S @ s' = s)
    @ (\mu x: S) = s \iff true
\end{theorem}


\begin{theorem}{rule muValue2}[S]
  \forall s: S | (\forall s': S @ s' = s)
    @ s = (\mu x: S) \iff true
\end{theorem}


\begin{theorem}{rule muSingleton}
  (\mu x: \{ y \}) = y
\end{theorem}


\newpage

\section{Applicability }\label{rules-appliesTo}

Relation $\_ applies\$to \_$ is used in domain checking conditions.
It is declared as
$$\_applies\$to\_[X,Y]: (X \rel Y) \rel X.$$



%%inrel applies\$to

Most of the rules about
$\_ applies\$to \_$ appear later in the Toolkit, after
``$\dom$'' has been introduced.



\subsection*{Theorems}


\begin[disabled]{theorem}{rule appliesToDef}[X,Y]
  \forall R: X \rel Y; x: X @
           R ~ applies\$to ~ x
     \iff (\exists y: Y | (x,y) \in R @ \forall y': Y | (x,y') \in R @ y = y')
\end{theorem}

\newpage

\section{Negations }\label{def-neq}


\subsection*{Definitions}


\syndef{\neq}{inrel}{"&neq"} \quad\verb'\neq'


\syndef{\notin}{inrel}{"&notin"} \quad\verb'\notin'


\begin{gendef}[X]
  \_\neq\_: X \rel X
\also
  \_\notin\_: X \rel \power X
\where
 \Label{notEqDef}
    \forall x, y: X
      @      x \neq y
        \iff \lnot x = y
\also
 \Label{notinDef}
    \forall x: X; S: \power X
      @      x \notin S
        \iff \lnot x \in S
\end{gendef}


\subsection*{Automation}


\begin{theorem}{rule notEqRule}[X]
     x \neq y
\iff
     (x \in X \land y \in X \land \lnot x = y)
\end{theorem}


\begin{theorem}{rule notInRule}[X]
  x \notin S
\iff
  (x \in X \land S \in \power X \land \lnot x \in S)
\end{theorem}

\newpage


\section{Sets }


\subsection{Extensionality }

The extensionality property is disabled, and needs to be enabled or applied
manually in those proofs where it is needed.


Additional extensionality properties are defined for relations
(theorem
$relationExtensionality$), functions (theorems
$pfunExtensionality$
and
$funExtensionality$),
and bags (theorem
$bagExtensionality$).



\subsubsection*{Theorems}


\begin[disabled]{theorem}{rule extensionality}
  X = Y \iff (\forall x: X @ x \in Y) \land (\forall y: Y @ y \in X)
\end{theorem}


\begin[disabled]{theorem}{rule extensionality2}
  X = Y \iff X \in \power Y \land Y \in \power X
\end{theorem}

Theorem $extensionality3$ cannot be a rule, because $X$ is not bound in the
pattern $S = T$.


\begin{theorem}{extensionality3}[X]
  \forall S, T: \power X @
    S = T \iff
           (\forall x: X | x \in S @ x \in T)
     \land (\forall x': X | x' \in T @ x' \in S)
\end{theorem}


\newpage

\subsection{Powersets }\label{rules-power}

The powerset notation is a predefined part of the Z notation.
Here are some basic theorems.



\subsubsection*{Theorems}


\begin[disabled]{theorem}{rule inPower}
  X \in \power Y \iff (\forall e: X @ e \in Y)
\end{theorem}


\begin{theorem}{rule inPowerSelf}
  X \in \power X
\end{theorem}


\begin{theorem}{rule power\_sub}
 \power X \in \power (\power Y) \iff X \in \power Y
\end{theorem}

The following two facts are automated by the ``weakening'' rules
in Section~\ref{weakening}.



\begin{theorem}{inPowerTransitive}
  X \in \power Y \land Y \in \power Z
\implies X \in \power Z
\end{theorem}


\begin{theorem}{inSubset}
  x \in Y \land Y \in \power Z
\implies x \in Z
\end{theorem}

\newpage

\subsection{Cross products }\label{rules-cross}

Cross products are part of the Z notation.  Here are some
basic theorems about two and three-element cross products.



\begin[disabled]{theorem}{rule inCross2}
  p \in X \cross Y
\iff (\exists x: X; y: Y @ p = (x,y))
\end{theorem}


\begin{theorem}{rule tupleInCross2}
  (x,y) \in X \cross Y
\iff
  x \in X \land y \in Y
\end{theorem}


\begin{theorem}{rule CrossSubsetCross2}
  A \in \power X \land B \in \power Y
\implies
  A \cross B \in \power (X \cross Y)
\end{theorem}


\begin{theorem}{rule crossNull\_2\_1}
  \{ \} \cross Y = \{ \}
\end{theorem}


\begin{theorem}{rule crossNull\_2\_2}
  X \cross \{ \} = \{ \}
\end{theorem}


\begin{theorem}{rule crossEqualNull2}
  X \cross Y = \{\}
\iff
  X = \{\} \lor Y = \{\}
\end{theorem}


\begin[disabled]{theorem}{rule inCross3}
  p \in X \cross Y \cross Z
\iff (\exists x: X; y: Y; z: Z @ p = (x,y,z))
\end{theorem}


\begin{theorem}{rule tupleInCross3}
  (x,y,z) \in X \cross Y \cross Z
\iff
  x \in X \land y \in Y \land z \in Z
\end{theorem}


\begin{theorem}{rule CrossSubsetCross3}
  A \in \power X \land B \in \power Y \land C \in \power Z
\implies
  A \cross B \cross C \in \power (X \cross Y \cross Z)
\end{theorem}


\begin{theorem}{rule crossNull\_3\_1}
  \{ \} \cross Y \cross Z = \{ \}
\end{theorem}


\begin{theorem}{rule crossNull\_3\_2}
  X \cross \{ \} \cross Z = \{ \}
\end{theorem}


\begin{theorem}{rule crossNull\_3\_3}
  X \cross Y \cross \{ \} = \{ \}
\end{theorem}


\begin{theorem}{rule crossEqualNull3}
  X \cross Y \cross Z = \{\}
\iff
  X = \{\} \lor Y = \{\} \lor Z = \{\}
\end{theorem}

\newpage

\subsection{Empty set }\label{def-emptyset}


\subsubsection*{Definition}


\syndef{\empty}{word}{"&empty"} \quad\verb'\empty'
\syndef{\emptyset}{word}{"&empty"} \quad\verb'\emptyset'

The name \protect\verb&\empty& is a synonym for \protect\verb&\emptyset& for backward
compatibility with some early versions of {\LaTeX} markup for Z.  The
name \protect\verb&\emptyset& is preferred, especially for printing, as newer versions
of {\LaTeX} markup will not display \protect\verb&\empty& correctly.


\begin[disabled]{zed}
  \emptyset[X] == \{~x: X | false~\}
\end{zed}


\subsubsection*{Theorems}

It is convenient in proofs to use the empty set extension instead of
the empty set, as the extension is simpler (since it does not use
a generic actual).



\begin{theorem}{rule emptyDefinition}[X]
  \emptyset[X] = \{ \}
\end{theorem}


\begin{theorem}{rule inNull}
  \lnot x \in \{ \}
\end{theorem}


\begin{theorem}{rule nullSubset}
  \{ \} \in \power X
\end{theorem}


\begin{theorem}{rule powerNull}
  \power \{ \} = \{ \{ \} \}
\end{theorem}


\begin{theorem}{nonEmptySetHasMember}
  S = \{\} \lor (\exists x: S @ true)
\end{theorem}

\newpage

\subsection{Unit sets }

Unit sets can be denoted by set displays.



\subsubsection*{Theorems}


\begin{theorem}{rule inUnit}
  x \in \{ y \}
\iff x = y
\end{theorem}


\begin{theorem}{rule unitSubset}
  \{ x \} \in \power X
\iff
  x \in X
\end{theorem}



\begin{theorem}{rule unitEqualUnit}
  \{ x \} = \{ y \}
\iff
  x = y
\end{theorem}


\begin{theorem}{rule nullEqualUnit}
  \lnot (\{ \} = \{ x \})
\end{theorem}


\begin{theorem}{rule unitEqualNull}
  \lnot (\{ x \} = \{ \})
\end{theorem}


\begin{theorem}{rule inPowerUnit}
  x \in \power \{ y \}
\iff
  x = \{ y \} \lor x = \{ \}
\end{theorem}

\newpage

\subsection{Non-empty powerset }\label{def-power1}


\subsubsection*{Definition}


\begin[disabled]{zed}
  \power_1 X == \{~S: \power X | S \neq \emptyset~\}
\end{zed}


\subsubsection*{Theorems}


\begin{theorem}{grule power1\_type}[X]
  \power_1 X \in \power (\power X)
\end{theorem}


\begin{theorem}{rule inPower1}
  x \in \power_1 X
\iff
  x \in \power X \land \lnot x = \{ \}
\end{theorem}


\begin{theorem}{rule power1Empty}
  \power_1 \{ \} = \{ \}
\end{theorem}


\begin{theorem}{rule power1Unit}
  \power_1 \{ x \} = \{ \{ x \} \}
\end{theorem}


\subsubsection*{Automation}


\begin{theorem}{rule power1\_strong\_type}
  \power_1 X \in \power (\power Y)
\iff
   X \in \power Y
\end{theorem}


\begin{theorem}{rule power1\_sub}
  \power_1 X \in \power (\power_1 Y)
\iff
  X \in \power Y
\end{theorem}


\newpage

\subsection{Subsets }\label{def-subseteq}


\subsubsection*{Definition}


\syndef{\subseteq}{inrel}{"&sube"} \quad\verb'\subseteq'


\syndef{\subset}{inrel}{"&sub"} \quad\verb'\subset'


\begin{gendef}[X]
  \_\subseteq\_, \_\subset\_: \power X \rel \power X
\where
\Label{disabled rule subDef}
    \forall A, B: \power X
      @      A \subseteq B
        \iff (\forall x: A @ x \in B)
\also
\Label{disabled rule psubDef}
    \forall A, B: \power X
      @      A \subset B
        \iff       A \subseteq B
             \land A \neq B
\end{gendef}


\subsubsection*{Theorems}


\begin[disabled]{theorem}{rule subsetSelf}[X]
  \forall S: \power X @ S \subseteq S
\end{theorem}


\begin[disabled]{theorem}{rule nullsetSubset}[X]
  \forall S: \power X @ \{\} \subseteq S
\end{theorem}


\begin[disabled]{theorem}{rule subsetTransitive}[X]
  \forall A, B, C: \power X | A \subseteq B \subseteq C @ A \subseteq C
\end{theorem}


\begin{theorem}{rule psubsetSelf}[X]
  \forall S: \power X @ \lnot S \subset S
\end{theorem}


\begin{theorem}{rule nullsetPsubset}[X]
  \forall S: \power X @
      \{\} \subset S \iff \lnot S = \{\}
\end{theorem}


\subsubsection*{Automation}

The subset notation is convenient, but is awkward in expressing
theorems because of the generic actual.  We cannot express the simple
fact that
$A$ is a subset of
$B$ without at the same time constraining
them to be subsets of something else (the generic actual).  A different
notation,
$A \in \power B$, expresses exactly what we mean, although it is
uglier than the subset notation.



\begin{theorem}{rule subsetDef}[X]
  A \subseteq B
\iff
  A \in \power B \land B \in \power X
\end{theorem}


\begin{theorem}{rule psubsetDef}[X]
  A \subset B
\iff
  A \in \power B \land B \in \power X \land \lnot A = B
\end{theorem}

\newpage

\subsection{Union }\label{def-cup}


\subsubsection*{Definitions}

Function
$\_ \cup \_$ is predefined, as it is needed in the expansion of
set extensions.



\subsubsection*{Theorems}


\begin{theorem}{rule inCup}[X]
  \forall A, B: \power X @
      x \in A \cup B \iff x \in A \lor x \in B
\end{theorem}


\begin[disabled]{theorem}{rule cupSubsetLeft}[X]
  S \subseteq[X] T
\implies
  S \cup T = T
\end{theorem}


\begin[disabled]{theorem}{rule cupSubsetRight}[X]
  T \subseteq[X] S
\implies
  S \cup T = S
\end{theorem}


\begin{theorem}{rule cupNullLeft}[X]
  \forall S: \power X @
     \{\} \cup S = S
\end{theorem}


\begin{theorem}{rule cupNullRight}[X]
  \forall S: \power X @
    S \cup \{\} = S
\end{theorem}


\begin{theorem}{rule cupCommutes}[X]
  \forall S, T: \power X @ S \cup T = T \cup S
\end{theorem}


\begin{theorem}{rule cupAssociates}[X]
  \forall S, T, V: \power X @
	(S \cup T) \cup V = S \cup (T \cup V)
\end{theorem}


\begin{theorem}{rule cupSubset}[X]
  \forall S, T: \power X @
      (S \cup T) \in \power U
    \iff
      S \in \power U \land T \in \power U
\end{theorem}


\subsubsection*{Automation}

The following two rules are needed to compute
equalities between set extensions,
for example, $\{ 1, 2 \} = \{ \}$.  However, they are not enough,
we would need additional rules to show
$\lnot \{ 1, 2 \} = \{ 2, 3 \}$.  These additional facts do not appear to
make good rewrite rules.


\begin{theorem}{rule cupEqualNullLeft}[X]
  \forall S, T: \power X @
     S \cup T = \{\} \iff S = \{\} \land T = \{\}
\end{theorem}


\begin{theorem}{rule cupEqualNullRight}[X]
  \forall S, T: \power X @
     \{\} = S \cup T  \iff S = \{\} \land T = \{\}
\end{theorem}

Rule
$cupPermutes$ is needed to complement the associative and commutative
laws.



\begin{theorem}{rule cupPermutes}[X]
  \forall S, T, V: \power X @
	S \cup (T \cup V) = T \cup (S \cup V)
\end{theorem}


\begin{theorem}{rule subsetCup}[X]
  \forall T, U: \power X @
     (S \in \power T \lor S \in \power U)
   \implies
      S \in \power (T \cup U)
\end{theorem}

\newpage

\subsection{Intersection }\label{def-cap}


\subsubsection*{Definitions}


\syndef{\cap}{infun4}{"&cap"} \quad\verb'\cap'


\begin{gendef}[X]
  \_\cap\_: \power X \cross \power X \fun \power X
\where
\Label{capDefinition}
    \forall x: X; A, B: \power X
      @ x \in A \cap B \iff x \in A \land x \in B
\end{gendef}


\subsubsection*{Theorems}


\begin{theorem}{rule inCap}[X]
  \forall A, B: \power X @
    x \in A \cap B \iff x \in A \land x \in B
\end{theorem}


\begin[disabled]{theorem}{rule capSubsetLeft}[X]
  S \subseteq[X] T
\implies
  S \cap T = S
\end{theorem}


\begin[disabled]{theorem}{rule capSubsetRight}[X]
  T \subseteq[X] S
\implies
  S \cap T = T
\end{theorem}


\begin{theorem}{rule capNullLeft}[X]
  \forall S: \power X @  \{\} \cap  S = \{\}
\end{theorem}


\begin{theorem}{rule capNullRight}[X]
  \forall S: \power X @ S \cap \{\} = \{\}
\end{theorem}


\begin{theorem}{rule unitCap}[X]
  \forall x: X; S: \power X @
    \{ x \} \cap S = \IF x \in S \THEN \{ x \} \ELSE \{ \}
\end{theorem}


\begin{theorem}{rule capUnit}[X]
  \forall x: X; S: \power X @
    S \cap \{ x \} = \IF x \in S \THEN \{ x \} \ELSE \{ \}
\end{theorem}


\begin{theorem}{rule capCommutes}[X]
  \forall S, T: \power X @ S \cap T = T \cap S
\end{theorem}


\begin{theorem}{rule capAssociates}[X]
  \forall S, T, V: \power X @
	(S \cap T) \cap V = S \cap (T \cap V)
\end{theorem}


\begin[disabled]{theorem}{rule capSubset}[X]
  \forall S, T, U: \power X @
     (S \subseteq U \lor T \subseteq U)
   \implies
      S \cap T \subseteq U
\end{theorem}


\begin{theorem}{rule subsetCap}[X]
  \forall T, U: \power X @
     S \in \power (T \cap U) \iff S \in \power T \land S \in \power U
\end{theorem}


\subsubsection*{Automation}

Rule
$capPermutes$ is needed to complement the associative and commutative
laws.


\begin{theorem}{rule capPermutes}[X]
  \forall S, T, V: \power X @
	S \cap (T \cap V) = T \cap (S \cap V)
\end{theorem}



\begin{theorem}{rule cap\_result}[X]
  \forall S, T: \power X |
      \power S \in \power Z \lor \power T \in \power Z
    @ S \cap T \in Z
\end{theorem}


In order to compute intersections of literals, we need the following
two rules. 


\begin{theorem}{rule computeCap1}[X]
  \forall x: X; S, T: \power X | x \in T @
    (\{ x \} \cup S) \cap T
  =  \{x \} \cup (S \cap T)
\end{theorem}


\begin{theorem}{rule computeCap2}[X]
  \forall x: X; S, T: \power X | \lnot x \in T @
    (\{ x \} \cup S) \cap T
=  S \cap T
\end{theorem}

\newpage

\subsection{Set difference }\label{def-setminus}


\subsubsection*{Definitions}


\syndef{\setminus}{infun3}{"&setminus"} \quad\verb'\setminus'



\begin{gendef}[X]
 \_ \setminus \_: \power X \cross \power X \fun \power X
\where
\Label{diffDefinition}
    \forall x: X; A, B: \power X
      @ x \in A \setminus B \iff x \in A \land \lnot x \in B
\end{gendef}


\subsubsection*{Theorems}


\begin{theorem}{rule inDiff}[X]
  \forall S, T: \power X @
       x \in S \setminus T
    \iff
      x \in S \land \lnot x \in T
\end{theorem}


\begin{theorem}{rule diffDiff}[X]
  \forall S, T, U: \power X @
     (S \setminus T) \setminus U = S \setminus (T \cup U)
\end{theorem}


\begin{theorem}{rule diffSubset}[X]
  \forall S,T,U: \power X @
    S \setminus T \subseteq U
  \iff S \subseteq U \cup T
\end{theorem}


\begin[disabled]{theorem}{rule diffSuperset}[X]
  \forall S, T: \power X | S \in \power T @ S \setminus T = \{\}
\end{theorem}


\begin{theorem}{rule diffEmptyLeft}[X]
  \forall S: \power X @ \{\} \setminus S = \{\}
\end{theorem}


\begin{theorem}{rule diffEmptyRight}[X]
  \forall S: \power X @ S \setminus \{ \} = S
\end{theorem}


\begin{theorem}{rule unitDiff}[X]
  \forall x: X; S: \power X @
    \{ x \} \setminus S = \IF x \in S \THEN \{ \} \ELSE \{ x \}
\end{theorem}


\subsubsection*{Automation}

The following is derived from the fact $S \setminus T \subseteq S$.


\begin{theorem}{rule diff\_result}[X]
  \forall S, T: \power X | \power S \in \power Z @
    S \setminus T \in Z
\end{theorem}

In order to compute differences of literals, we need the following
two rules.


\begin{theorem}{rule computeDiff1}[X]
  \forall x: X; S, T: \power X | x \in T @
    (\{ x \} \cup S) \setminus T
=  S \setminus T
\end{theorem}


\begin{theorem}{rule computeDiff2}[X]
  \forall x: X; S, T: \power X | \lnot x \in T @
    (\{ x \} \cup S) \setminus T
= \{x \} \cup (S \setminus T)
\end{theorem}

\newpage

\subsection{Distribution laws }


\subsubsection*{Theorems}


\begin[disabled]{theorem}{rule distributeCupOverCapRight}[X]
  \forall A, B, C: \power X @
     A \cup (B \cap C) = (A \cup B) \cap (A \cup C)
\end{theorem}


\begin[disabled]{theorem}{rule distributeCupOverCapLeft}[X]
  \forall A, B, C: \power X @
     (A \cap B) \cup C = (A \cup C) \cap (B \cup C)
\end{theorem}


\begin[disabled]{theorem}{rule distributeCapOverCupRight}[X]
  \forall A, B, C: \power X @
     A \cap (B \cup C) = (A \cap B) \cup (A \cap C)
\end{theorem}


\begin[disabled]{theorem}{rule distributeCapOverCupLeft}[X]
  \forall A, B, C: \power X @
     (A \cup B) \cap C = (A \cap C) \cup (B \cap C)
\end{theorem}


\begin[disabled]{theorem}{rule distributeDiffOverCupRight}[X]
  \forall A, B, C: \power X @
     A \setminus (B \cup C) = (A \setminus B) \cap (A \setminus C)
\end{theorem}


\begin[disabled]{theorem}{rule distributeDiffOverCupLeft}[X]
  \forall A, B, C: \power X @
     (A \cup B) \setminus C = (A \setminus C) \cup (B \setminus C)
\end{theorem}


\begin[disabled]{theorem}{rule distributeDiffOverCapRight}[X]
  \forall A, B, C: \power X @
     A \setminus (B \cap C) = (A \setminus B) \cup (A \setminus C)
\end{theorem}


\begin[disabled]{theorem}{rule distributeDiffOverCapLeft}[X]
  \forall A, B, C: \power X @
     (A \cap B) \setminus C = (A \setminus C) \cap (B \setminus C)
\end{theorem}


\newpage

\subsection{Generalized union and intersection }\label{def-bigcup}


\subsubsection*{Definitions}


\begin{gendef}[X]
  \bigcup, \bigcap: \power (\power X) \fun \power X
\where
\Label{rule inBigcup}
    \forall x: X; A: \power (\power X)
      @ x \in \bigcup A \iff ( \exists B: A @ x \in B )
\also
\Label{rule inBigcap}
    \forall x: X; A: \power (\power X)
      @ x \in \bigcap A \iff ( \forall B: A @ x \in B )
\end{gendef}


\subsubsection*{Theorems}


\begin{theorem}{rule bigcupEmpty}[X]
  \bigcup[X] \{\} = \{\}
\end{theorem}


\begin{theorem}{rule bigcupUnit}[X]
  S \in \power X  
\implies
  \bigcup \{ S \} = S
\end{theorem}


\begin{theorem}{rule bigcupUnion}[X]
\forall S,T: \power (\power X) @
  \bigcup (S \cup T) = (\bigcup S) \cup (\bigcup T)
\end{theorem}


\begin{theorem}{rule inPowerBigcup}[X]
  \forall S: \power (\power X) @
     x \in S \implies x \in \power (\bigcup S)
\end{theorem}


\begin{theorem}{rule bigcupInPower}[X]
  \forall S: \power (\power X) @
           \bigcup S \in \power T
      \iff
           S \in \power (\power T)
\end{theorem}


\begin[disabled]{theorem}{rule bigcupSubsetBigcup}[X]
  \forall S, T: \power (\power X)
     | S \subseteq T
     @ \bigcup S \subseteq \bigcup T
\end{theorem}


\begin{theorem}{rule bigcapEmpty}[X]
  \bigcap[X] \{\} = X
\end{theorem}


\begin{theorem}{rule bigcapUnit}[X]
  S \in \power X  
\implies
  \bigcap \{ S \} = S
\end{theorem}


\begin{theorem}{rule bigcapUnion}[X]
\forall S,T: \power (\power X) @
  \bigcap (S \cup T) = (\bigcap S) \cap (\bigcap T)
\end{theorem}


\begin{theorem}{rule bigcapInPower}[X]
  \forall S: \power (\power X) @
      x \in S \implies \bigcap S \in \power x
\end{theorem}


\begin[disabled]{theorem}{rule inPowerBigcap}[X]
  \forall T: \power (\power X) @
         S \in \power (\bigcap T)
    \iff (\forall U: T @ S \in \power U)
\end{theorem}


\begin[disabled]{theorem}{rule bigcapSubsetBigcap}[X]
  \forall S, T: \power (\power X)
     | T \subseteq S
     @ \bigcap S \subseteq \bigcap T
\end{theorem}

\newpage

\section{Ordered pairs }\label{def-first}

The definitions of
$first$ and
$second$ are here for compatibility
with the original toolkit.  It is usually more convenient to use
the numeric projection functions (i.e., write
$p.1$ instead of
$first ~ p$).  This is better in proofs because there are no generic actuals
needed.



\subsection*{Definitions}


\begin{gendef}[X,Y]
  first: X \cross Y \fun X \\
  second: X \cross Y \fun Y
\where
\Label{rule firstDefinition}
  \forall x: X; y: Y @ first(x,y) = x
\also
\Label{rule secondDefinition}
  \forall x: X; y: Y @ second(x,y) = y
\also
\Label{pairComposition}
  \forall p: X \cross Y @ p = (first~ p, second~ p)
\end{gendef}


\subsection*{Theorems}


\begin{theorem}{rule firstIsDot1}[X,Y]
  \forall p: X \cross Y @ first[X,Y] p = p.1
\end{theorem}


\begin{theorem}{rule secondIsDot2}[X,Y]
  \forall p: X \cross Y @ second[X,Y] p = p.2
\end{theorem}

\newpage

\section{Relations }


\subsection{Relation space }\label{rules-rel}

The function
$\_\rel\_$ is predefined by the equation
$X \rel Y = \power (X \cross Y)$.



\subsubsection*{Theorems}


\begin{theorem}{grule relDefinition}[X,Y]
  X \rel Y = \power (X \cross Y)
\end{theorem}


\begin{theorem}{rule nullInRel}
  \{\} \in X \rel Y
\end{theorem}


\begin{theorem}{rule unitInRel}
  \{ p \} \in X \rel Y
\iff
  p \in X \cross Y
\end{theorem}


\begin{theorem}{rule cupInRel}[X, Y]
  \forall Q, R: \power (X \cross Y) @ \\
\t1      Q \cup R \in A \rel B
    \iff Q \in A \rel B \land R \in A \rel B
\end{theorem}


\begin{theorem}{subsetOfRelIsRel}[X,Y]
  R \in X \rel Y \land S \subseteq R
\implies
  S \in X \rel Y
\end{theorem}


\begin{theorem}{rule crossIsRel}[X,Y]
  \forall A: \power X; B: \power Y @
    A \cross B \in X \rel Y
\end{theorem}


\begin{theorem}{rule relEqualNull}
  \lnot X \rel Y = \{\}
\end{theorem}


\begin{theorem}{relationExtensionality}[X,Y]
  \forall Q, R: X \rel Y @
     Q = R \iff (\forall x: X; y: Y @ x \inrel{R} y \iff x \inrel{Q} y)
\end{theorem}



\subsubsection*{Automation}


\begin{theorem}{rule rel\_type}[X,Y]
  \power (X \cross Y) \in Z \implies X \rel Y \in Z
\end{theorem}


\begin{theorem}{rule rel\_ideal}[X,Y]
  \power S \in \power (X \rel Y)
\iff
  S \in X \rel Y
\end{theorem}


\begin{theorem}{rule rel\_sub}[X,Y]
  \forall A: \power X; B: \power Y @
    A \rel B \in \power (X \rel Y)
\end{theorem}

\newpage

\subsection{Maplets }\label{def-maplet}

Maplets provide an alternative notation for ordered pairs.  They are usually
used in defining functions or relations.  The defining axiom is phrased as
a rewrite rule to eliminate maplets in favour of pairs.



\subsubsection*{Definitions}


\syndef{\mapsto}{infun1}{"&map"} \quad\verb'\mapsto'


\begin{gendef}[X,Y]
  \_ \mapsto \_: X \cross Y \fun X \cross Y
\where
\Label{rule mapDef}
  \forall x: X; y: Y @ x \mapsto y = (x, y)
\end{gendef}

\newpage

\subsection{Domain and range }\label{def-dom}


\syndef{\dom}{word}{"&dom"} \quad\verb'\dom'


\syndef{\ran}{word}{"&ran"} \quad\verb'\ran'


\subsubsection*{Definitions}


\begin{gendef}[X, Y]
  \dom: (X \rel Y) \fun \power X \\
  \ran: (X \rel Y) \fun \power Y
\where
\Label{disabled rule domDefinition}
  \forall R: X \rel Y @ \dom R = \{ x: X; y: Y | (x, y) \in R @ x \}
\also
\Label{disabled rule ranDefinition}
  \forall R: X \rel Y @ \ran R = \{ x: X; y: Y | (x, y) \in R @ y \}
\end{gendef}


\subsubsection*{Theorems}


\begin[disabled]{theorem}{rule inDom}[X, Y]
\forall  R: X \rel Y @
   x \in \dom ~ R
 \iff
   (\exists y: Y @ (x, y) \in R)
\end{theorem}


\begin{theorem}{memberFirstInDom}[X,Y]
  \forall R: X \rel Y | (x, y) \in R @ x \in \dom R
\end{theorem}


\begin{theorem}{rule domEmpty}[X,Y]
  \dom[X,Y] \{ \} = \{ \}
\end{theorem}


\begin{theorem}{rule domSingleton}[X,Y]
  \forall p: X \cross Y @ \dom \{ p \} = \{ p.1 \}
\end{theorem}


\begin{theorem}{rule domCup} [X, Y]
   \forall Q, R: X \rel Y @ \dom (Q \cup R) = (\dom Q) \cup (\dom R)
\end{theorem}


\begin{theorem}{rule domCross}[X,Y]
  \forall A: \power X; B: \power Y
     | \lnot B = \{ \}
     @ \dom (A \cross B) = A
\end{theorem}


\begin[disabled]{theorem}{rule domSubset}[X,Y]
  \forall S: X \rel Y @ \forall R: \power S  @ \dom R \in \power (\dom S)
\end{theorem}


\begin[disabled]{theorem}{rule inRan}[X, Y]
\forall R: X \rel Y @
     y \in \ran ~ R
  \iff
     (\exists x: X @ (x, y) \in R)
\end{theorem}


\begin{theorem}{memberSecondInRan}[X,Y]
  \forall R: X \rel Y | (x, y) \in R @ y \in \ran R
\end{theorem}


\begin[disabled]{theorem}{rule inRanFunction}[X, Y]
\forall f: X \pfun Y @
     y \in \ran ~ f
  \iff
     (\exists x: \dom f @ y = f(x))
\end{theorem}


\begin{theorem}{rule ranEmpty}[X,Y]
  \ran[X,Y] \{ \} = \{ \}
\end{theorem}


\begin{theorem}{rule ranSingleton}[X,Y]
  \forall p: X \cross Y @ \ran \{ p \} = \{ p.2 \}
\end{theorem}


\begin{theorem}{rule ranCup} [X, Y]
   \forall Q, R: X \rel Y @ \ran (Q \cup R) = (\ran Q) \cup (\ran R)
\end{theorem}


\begin{theorem}{rule ranCross}[X,Y]
  \forall A: \power X; B: \power Y
     | \lnot A = \{ \}
     @ \ran (A \cross B) = B
\end{theorem}


\begin[disabled]{theorem}{rule ranSubset}[X,Y]
  \forall S: X \rel Y @ \forall R: \power S  @ \ran R \in \power (\ran S)
\end{theorem}


\subsubsection*{Automation}


\begin{theorem}{rule domInPower}[X,Y]
  S \in \power X \land R \in S \rel Y
\implies
  \dom[X,Y] R \in \power S
\end{theorem}


\begin{theorem}{rule ranInPower}[X,Y]
  S \in \power Y \land R \in X \rel S
\implies
  \ran[X,Y] R \in \power S
\end{theorem}

\newpage

\subsection{Identity relation }\label{def-id}


\subsubsection*{Definitions}


\syndef{\id}{pregen}{"&id"} \quad\verb'\id'


\begin[disabled]{zed}
  \id X == \{~ x: X @ x \mapsto x ~\}
\end{zed}


\subsubsection*{Theorems}


\begin[disabled]{theorem}{rule inId}[X]
  p \in \id X
\iff
  p \in X \cross X \land p.1 = p.2
\end{theorem}


\begin{theorem}{rule pairInId}[X]
  (x,y) \in \id X \iff x = y \land x \in X
\end{theorem}


\begin{theorem}{rule applyId}[X]
  \forall x: X @ (\id X)(x) = x
\end{theorem}


\begin{theorem}{rule domId}[X]
  \forall S: \power X @ \dom (\id S) = S
\end{theorem}


\begin{theorem}{rule ranId}[X]
  \forall S: \power X @ \ran (\id S) = S
\end{theorem}


\begin{theorem}{rule idNull}
  \id \{\} = \{\}
\end{theorem}


\begin{theorem}{rule idUnit}
  \id \{ x \} = \{ (x,x) \}
\end{theorem}


\begin{theorem}{rule idCup}[X]
  \forall A,B: \power X @ \id (A \cup B) = \id A \cup \id B
\end{theorem}


\begin{theorem}{rule idSubsetId}
  \id X \in \power (\id Y)
\iff
  X \in \power Y
\end{theorem}


\subsubsection*{Automation}

The next four rules could be replaced by a
$\_type$ rule.  Better, though,
would be to use
$X \bij X$ as the declared set, if bijections were
declared yet.


\begin{theorem}{rule idType}[X]
   \id X \in \power (A \cross B)
\iff
    X \in \power A \land X \in \power B
\end{theorem}


\begin{theorem}{rule idInRel}[X]
   \id X \in A \rel B
\iff
    X \in \power A \land X \in \power B
\end{theorem}


\begin{theorem}{rule idInPfun}[X]
   \id X \in (A \pfun B)
\iff
    X \in\power A \land X \in \power B
\end{theorem}


\begin{theorem}{rule idInFun}[X]
   \id X \in (A \fun B)
\iff
    X = A \land X \in \power B
\end{theorem}

\newpage

\subsection{Composition }\label{def-comp}

Two composition operators are defined; they are identical except for the
order of their arguments.  Rather than have two sets of rules, one for each
composition operator, we use rule
$circDef$ to replace
$g \circ f$
by
$f \comp g$.



\subsubsection*{Definitions}


\syndef{\comp}{infun4}{"&relcomp"} \quad\verb'\comp'


\syndef{\circ}{infun4}{"&fncomp"} \quad\verb'\circ'


\begin{gendef}[X,Y,Z]
  \_ \comp \_: (X \rel Y) \cross (Y \rel Z) \fun (X \rel Z) \\
  \_ \circ \_: (Y \rel Z) \cross (X \rel Y) \fun (X \rel Z)
\where
\Label{disabled rule compDef}
  \forall Q: X \rel Y; R: Y \rel Z @ \\
\t1 Q \comp R = \{~ x: X; y: Y; z: Z | x \inrel{Q} y \inrel{R} z @ (x,z) ~\}
\also
\Label{rule circDef}
  \forall Q: X \rel Y; R: Y \rel Z @ \\
\t1 R \circ Q = Q \comp R
\end{gendef}


\subsubsection*{Theorems}


\begin{theorem}{rule pairInComp}[X,Y,Z]
  \forall  Q: X \rel Y; R: Y \rel Z @
     (x,z) \in Q \comp R
   \iff
     (\exists y: Y @ x \inrel{Q} y \inrel{R} z)
\end{theorem}


\begin{theorem}{rule compAssociates}[W,X,Y,Z]
  \forall  P: W \rel X; Q: X \rel Y; R: Y \rel Z @
     (P \comp Q) \comp R = P \comp (Q \comp R)
\end{theorem}

The domain of a composition $Q \comp R$ is
$Q\inv \limg \dom R \rimg$, but
this fact cannot be legally stated this early in the Toolkit.  A similar
fact (and problem) applies to the range of a composition.
See Section~\ref{def-image}, where these theorems appear.


\begin{theorem}{domCompSmaller}[X,Y,Z]
  \forall  Q: X \rel Y; R: Y \rel Z @
     	\dom (Q \comp R) \subseteq  \dom Q
\end{theorem}


\begin[disabled]{theorem}{rule easyDomComp}[X,Y,Z]
  \forall  Q: X \rel Y; R: Y \rel Z | \ran Q \in \power (\dom R) @
	\dom (Q \comp R) = \dom Q
\end{theorem}


\begin{theorem}{ranCompSmaller}[X,Y,Z]
  \forall  Q: X \rel Y; R: Y \rel Z @
     	\ran (Q \comp R) \subseteq  \ran R
\end{theorem}


\begin[disabled]{theorem}{rule easyRanComp}[X,Y,Z]
  \forall  Q: X \rel Y; R: Y \rel Z | \dom R \in \power (\ran Q) @
	\ran (Q \comp R) = \ran R
\end{theorem}


\begin{theorem}{rule applyComp}[X,Y,Z]
	       f \in X \pfun Y
	 \land g \in Y \pfun Z
	 \land x \in \dom f
	 \land f(x) \in \dom g
\implies (f \comp g)(x) = g(f(x))
\end{theorem}

It is hard to make a stronger rule than the following, because a composition
may apply to a value in cases where its first member does not.
For example, if
$f = \num \cross \num$ and
$g = \{0 \mapsto 0\}$, then
$f$ does
not apply to anything, while
$f \comp g$ is a function with domain
$\num$.


\begin{theorem}{rule compAppliesTo}[X,Y,Z]
 \forall f: X \rel Y; g: Y \rel Z @
        f ~ applies\$to ~x
\implies ((f \comp g) ~ applies\$to ~ x
	  \iff g ~ applies\$to ~ f(x))
\end{theorem}


\begin[disabled]{theorem}{rule compMonotone}[X,Y,Z]
 \forall Q, Q': X \rel Y; R,R': Y \rel Z |
     Q' \subseteq Q \land R' \subseteq R @
	Q' \comp R' \subseteq (Q \comp R)
\end{theorem}


\begin{theorem}{rule compInRel}[X,Y,Z]
  \forall A: \power X; B: \power Z
     | Q \in A \rel Y \land R \in Y \rel B
     @ Q \comp R \in A \rel B
\end{theorem}


\begin{theorem}{rule compInPfun}[X,Y,Z]
  \forall A: \power X; B: \power Z
     | f \in A \pfun Y \land g \in Y \pfun B
     @ f \comp g \in A \pfun B
\end{theorem}


\begin{theorem}{rule compInFun}[X,Y,Z]
  \forall A: \power X; B: \power Z
     | f \in X \pfun Y \land g \in Y \pfun Z
     @ \\ \t1
       f \comp g \in A \fun B
       \iff (\dom (f \comp g) = A \land \ran (f \comp g) \subseteq B)
\end{theorem}


\subsubsection*{Automation}


\begin{theorem}{rule applyCompKnownFunctions}[X,Y,Z]
	       KnownMember[A \fun B][f/element]
	 \land KnownMember[C \fun D][g/element] \\
	 \land x \in A 
	 \land A \in \power X
	 \land B \in \power C
	 \land C \in \power Y
	 \land D \in \power Z \\
\implies (f \comp g)(x) = g(f(x))
\end{theorem}

We could add $domCompResult$ and $RanCompResult$ here.


\newpage

\subsection{Domain and range restriction }\label{def-dres}


\subsubsection*{Definitions}


\syndef{\dres}{infun6}{"&dres"} \quad\verb'\dres'


\syndef{\rres}{infun6}{"&rres"} \quad\verb'\rres'


\begin{gendef}[X,Y]
  \_ \dres \_: \power X \cross (X \rel Y) \fun (X \rel Y) \\
  \_ \rres \_: (X \rel Y) \cross \power Y \fun (X \rel Y)
\where
\Label{disabled rule dresDef}
  \forall S: \power X; R: X \rel Y @
    S \dres R = \{~ p: R | p.1 \in S ~\}
\also
\Label{disabled rule rresDef}
  \forall R: X \rel Y; S: \power Y @ 
    R \rres S = \{~ p: R | p.2 \in S ~\}
\end{gendef}


\subsubsection*{Theorems}


\begin{theorem}{rule inDres}[X,Y]
  \forall S: \power X; R: X \rel Y @
     x \in S \dres R \iff x \in R \land x.1 \in S
\end{theorem}


\begin{theorem}{rule inRres}[X,Y]
  \forall R: X \rel Y; S: \power Y @
     x \in R \rres S \iff x \in R \land x.2 \in S
\end{theorem}


\begin{theorem}{rule domDres}[X,Y]
  \forall R: X \rel Y; S: \power X @
     \dom (S \dres R) = S \cap \dom R
\end{theorem}


\begin{theorem}{rule ranRres}[X,Y]
  \forall R: X \rel Y; S: \power Y @
    \ran (R \rres S) = (\ran R) \cap S
\end{theorem}


\begin{theorem}{dresIsSubset}[X,Y]
  \forall R: X \rel Y; S: \power X @
      S \dres R \subseteq R
\end{theorem}


\begin{theorem}{rresIsSubset}[X,Y]
  \forall R: X \rel Y; S: \power Y @
      R \rres S \subseteq R
\end{theorem}


\begin{theorem}{rule compIdLeft}[X,Y]
  \forall S: \power X; R: X \rel Y @
     (\id S) \comp R = S \dres R
\end{theorem}


\begin{theorem}{rule compIdRight}[X,Y]
  \forall R: X \rel Y; S: \power Y @
     R \comp (\id S) = R \rres S
\end{theorem}


\begin{theorem}{rule dresId}[X]
  \forall S, T: \power X @
    S \dres (\id T) = \id (S \cap T)
\end{theorem}


\begin{theorem}{rule rresId}[X]
  \forall S, T: \power X @
    (\id S) \rres T = \id (S \cap T)
\end{theorem}


\begin{theorem}{rule dresDres}[X,Y]
  \forall S, T: \power X; R: X \rel Y @
    S \dres (T \dres R) = (S \cap T) \dres R
\end{theorem}


\begin{theorem}{rule rresRres}[X,Y]
  \forall S, T: \power Y; R: X \rel Y @
    (R \rres S) \rres T = R \rres (S \cap T)
\end{theorem}

We should normalize
$S \dres R \rres T$, as the order of association
does not matter.


\begin[disabled]{theorem}{rule dresEverything}[X,Y]
  \forall R: X \rel Y; S: \power X @
      S \cap \dom R = \{ \} \implies S \dres R = \{ \}
\end{theorem}


\begin[disabled]{theorem}{rule rresEverything}[X,Y]
  \forall R: X \rel Y; S: \power Y @
      S \cap \ran R = \{ \} \implies R \rres S = \{ \}
\end{theorem}


\begin{theorem}{rule nullDres}[X,Y]
  \forall R: X \rel Y @ \{\} \dres R = \{\}
\end{theorem}


\begin{theorem}{rule rresNull}[X,Y]
  \forall R: X \rel Y @ R \rres \{\} = \{\}
\end{theorem}


\begin{theorem}{rule dresNull}[X,Y]
 \forall S: \power X @  S \dres[X,Y] \{\} = \{\}
\end{theorem}


\begin{theorem}{rule nullRres}[X,Y]
 \forall S: \power Y @  \{\} \rres[X,Y] S = \{\}
\end{theorem}


\begin[disabled]{theorem}{rule dresElimination}[X,Y]
  \forall R: X \rel Y; S: \power X @
  \dom R \in \power S \implies S \dres R = R
\end{theorem}


\begin[disabled]{theorem}{rule rresElimination}[X,Y]
  \forall R: X \rel Y; S: \power Y @
  \ran R \in \power S \implies R \rres S = R
\end{theorem}


\begin{theorem}{rule dresUnit}[X,Y]
  \forall x: X; y: Y; S: \power X @
  S \dres \{ (x,y) \} = 
  \IF x \in S \THEN \{ (x,y) \} \ELSE \{ \}
\end{theorem}


\begin{theorem}{rule unitRres}[X,Y]
  \forall x: X; y: Y; S: \power Y @
  \{ (x,y) \} \rres S = 
  \IF y \in S \THEN \{ (x,y) \} \ELSE \{ \}
\end{theorem}


\begin{theorem}{rule unitDres}[X,Y]
  \forall R: X \rel Y; x: X @
    (\lnot x \in \dom R) \implies \{ x \} \dres R = \{ \}
\end{theorem}


\begin{theorem}{rule rresUnit}[X,Y]
  \forall R: X \rel Y; y: Y @
    (\lnot y \in \ran R) \implies R \rres \{ y \} = \{ \}
\end{theorem}


\begin{theorem}{rule dresCup}[X,Y]
  \forall S: \power X; Q, R: X \rel Y @
    S \dres (Q \cup R) = (S \dres Q) \cup (S \dres R)
\end{theorem}


\begin{theorem}{rule rresCup}[X,Y]
  \forall Q, R: X \rel Y; S: \power Y @
     (Q \cup R) \rres S = (Q \rres S) \cup (R \rres S)
\end{theorem}

There should be theorems about restricting compositions.


\begin{theorem}{rule applyDres}[X,Y]
  \forall f: X \pfun Y; S: \power X @
    x \in S \land x \in \dom f
   \implies (S \dres f)(x) = f(x)
\end{theorem}


\begin{theorem}{rule applyRres}[X,Y]
  \forall f: X \pfun Y; S: \power Y @
    x \in \dom f \land f(x) \in S
   \implies (f \rres S)(x) = f(x)
\end{theorem}


\subsubsection*{Automation}


\begin{theorem}{rule dres\_result}[X,Y]
\forall S: \power X; R: X \rel Y @
  \power R \in \power Z
\implies
  S \dres R \in Z
\end{theorem}


\begin{theorem}{rule rres\_result}[X,Y]
  \forall S: \power Y; R: X \rel Y @
    \power R \in \power Z
  \implies
    R \rres S \in Z
\end{theorem}

\newpage

\subsection{Domain and range anti-restriction }\label{def-ndres}


\subsubsection*{Definitions}


\syndef{\ndres}{infun6}{"&dsub"} \quad\verb'\ndres'


\syndef{\nrres}{infun6}{"&rsub"} \quad\verb'\nrres'


\begin{gendef}[X,Y]
  \_ \ndres \_: \power X \cross (X \rel Y) \fun (X \rel Y) \\
  \_ \nrres \_: (X \rel Y) \cross \power Y \fun (X \rel Y)
\where
\Label{disabled rule ndresDef}
  \forall S: \power X; R: X \rel Y @
    S \ndres R = \{~ p: R | \lnot p.1 \in S ~\}
\also
\Label{disabled rule nrresDef}
  \forall R: X \rel Y; S: \power Y @ 
    R \nrres S = \{~ p: R | \lnot p.2 \in S ~\}
\end{gendef}


\subsubsection*{Theorems}


\begin{theorem}{rule inNdres}[X,Y]
  \forall S: \power X; R: X \rel Y @
     x \in S \ndres R \iff x \in R \land \lnot x.1 \in S
\end{theorem}


\begin{theorem}{rule inNrres}[X,Y]
  \forall R: X \rel Y; S: \power Y @
     x \in R \nrres S \iff x \in R \land \lnot x.2 \in S
\end{theorem}


\begin{theorem}{rule domNdres}[X,Y]
  \forall R: X \rel Y; S: \power X @
     \dom (S \ndres R) = (\dom R) \setminus S
\end{theorem}


\begin{theorem}{rule ranNrres}[X,Y]
  \forall R: X \rel Y; S: \power Y @
    \ran (R \nrres S) = (\ran R) \setminus S
\end{theorem}


\begin{theorem}{ndresIsSubset}[X,Y]
  \forall R: X \rel Y; S: \power X @
      S \ndres R \subseteq R
\end{theorem}


\begin{theorem}{nrresIsSubset}[X,Y]
  \forall R: X \rel Y; S: \power Y @
      R \nrres S \subseteq R
\end{theorem}


\begin{theorem}{rule ndresId}[X]
  \forall S, T: \power X @
    S \ndres (\id T) = \id (T \setminus S)
\end{theorem}


\begin{theorem}{rule nrresId}[X]
  \forall S, T: \power X @
    (\id S) \nrres T = \id (S \setminus T)
\end{theorem}


\begin{theorem}{rule ndresNdres}[X,Y]
  \forall S, T: \power X; R: X \rel Y @
    S \ndres (T \ndres R) = (S \cup T) \ndres R
\end{theorem}


\begin{theorem}{rule nrresNrres}[X,Y]
  \forall S, T: \power Y; R: X \rel Y @
    (R \nrres S) \nrres T = R \nrres (S \cup T)
\end{theorem}

More similar rules are possible, for various combinations of
$\dres$, $\ndres$, $\rres$, and $\nrres$.


\begin[disabled]{theorem}{rule ndresNothing}[X,Y]
  \forall R: X \rel Y; S: \power X @
      S \cap \dom R = \{ \} \implies S \ndres R = R
\end{theorem}


\begin[disabled]{theorem}{rule nrresNothing}[X,Y]
  \forall R: X \rel Y; S: \power Y @
      S \cap \ran R = \{ \} \implies R \nrres S = R
\end{theorem}


\begin{theorem}{rule nullNdres}[X,Y]
  \forall R: X \rel Y @ \{\} \ndres R = R
\end{theorem}


\begin{theorem}{rule nrresNull}[X,Y]
  \forall R: X \rel Y @ R \nrres \{\} = R
\end{theorem}


\begin[disabled]{theorem}{rule ndresEverything}[X,Y]
  \forall R: X \rel Y; S: \power X @
  \dom R \in \power S \implies S \ndres R = \{\}
\end{theorem}


\begin[disabled]{theorem}{rule nrresEverything}[X,Y]
  \forall R: X \rel Y; S: \power Y @
  \ran R \in \power S \implies R \nrres S = \{\}
\end{theorem}


\begin{theorem}{rule ndresNull}[X,Y]
  \forall  S: \power X @ S \ndres[X,Y] \{\} = \{\}
\end{theorem}


\begin{theorem}{rule nullNrres}[X,Y]
  \forall  S: \power Y @ \{\} \nrres[X,Y] S = \{\}
\end{theorem}



\begin{theorem}{rule ndresUnit}[X,Y]
  \forall x: X; y: Y; S: \power X @
    S \ndres \{ (x,y) \} = 
      \IF x \in S \THEN \{\} \ELSE \{ (x,y) \}
\end{theorem}


\begin{theorem}{rule nrresUnit}[X,Y]
  \forall x: X; y: Y; S: \power Y @
    \{ (x,y) \} \nrres S = 
      \IF y \in S \THEN \{\} \ELSE \{ (x,y) \}
\end{theorem}


\begin{theorem}{rule ndresCup}[X,Y]
  \forall S: \power X; Q, R: X \rel Y @
    S \ndres (Q \cup R) = (S \ndres Q) \cup (S \ndres R)
\end{theorem}


\begin{theorem}{rule nrresCup}[X,Y]
  \forall Q, R: X \rel Y; S: \power Y @
     (Q \cup R) \nrres S = (Q \nrres S) \cup (R \nrres S)
\end{theorem}

There should be theorems about anti-restricting compositions.


\begin{theorem}{rule applyNdres}[X,Y]
  \forall f: X \pfun Y; S: \power X @
    \lnot x \in S \land x \in \dom f
   \implies (S \ndres f)(x) = f(x)
\end{theorem}


\begin{theorem}{rule applyNrres}[X,Y]
  \forall f: X \pfun Y; S: \power Y @
    x \in \dom f \land \lnot f(x) \in S
   \implies (f \nrres S)(x) = f(x)
\end{theorem}




\subsubsection*{Automation}


\begin{theorem}{rule ndres\_result}[X,Y]
\forall S: \power X; R: X \rel Y @
  \power R \in \power Z
\implies
  S \ndres R \in Z
\end{theorem}


\begin{theorem}{rule nrres\_result}[X,Y]
  \forall S: \power Y; R: X \rel Y @
    \power R \in \power Z
  \implies
    R \nrres S \in Z
\end{theorem}

\newpage

\subsection{Relational inversion }\label{def-inv}


\subsubsection*{Definitions}


\syndef{\inv}{postfun}{"&inverse"} \quad\verb'\inv'


\begin{gendef}[X,Y]
  \_ \inv: (X \rel Y) \fun (Y \rel X)
\where
\Label{disabled rule invDef}
  \forall R: X \rel Y @
    R \inv = \{ p: R @ (p.2, p.1) \}
\end{gendef}


\subsubsection*{Theorems}


\begin{theorem}{rule invInPowerCross}[X,Y]
  \forall A: \power Y; B: \power X; R: X \rel Y @
    R \inv \in \power (A \cross B) \iff R \in \power (B \cross A)
\end{theorem}


\begin{theorem}{rule invInRel}[X,Y]
  \forall A: \power Y; B: \power X; R: X \rel Y @
      R \inv \in A \rel B \iff R \in B \rel A
\end{theorem}


\begin{theorem}{rule pairInInv}[X,Y]
  \forall R: X \rel Y @
    (x,y) \in R \inv \iff (y,x) \in R
\end{theorem}


\begin[disabled]{theorem}{rule inversesEqual}[X,Y]
  \forall Q, R: X \rel Y @
     Q\inv = R\inv \iff Q = R
\end{theorem}


\begin[disabled]{theorem}{rule inversesSubseteq}[X,Y]
  \forall Q, R: X \rel Y @
     Q\inv \subseteq R\inv \iff Q \subseteq R
\end{theorem}


\begin{theorem}{rule invCross}[X,Y]
  \forall A: \power X; B: \power Y @
    (A \cross B) \inv = B \cross A
\end{theorem}


\begin{theorem}{rule invEmpty}[X,Y]
  (\_ \inv)[X,Y] \{\} = \{\}
\end{theorem}


\begin{theorem}{rule invUnit}[X,Y]
  \forall x: X; y: Y @ \{ (x, y) \} \inv = \{ (y,x) \}
\end{theorem}


\begin{theorem}{rule invCup}[X,Y]
  \forall Q,R: X \rel Y @ (Q \cup R)\inv = (Q\inv) \cup (R \inv)
\end{theorem}


\begin{theorem}{rule invCap}[X,Y]
  \forall Q,R: X \rel Y @ (Q \cap R)\inv = (Q\inv) \cap (R \inv)
\end{theorem}


\begin{theorem}{rule invSetminus}[X,Y]
  \forall Q,R: X \rel Y @ (Q \setminus R)\inv = (Q\inv) \setminus (R \inv)
\end{theorem}


\begin{theorem}{rule invInv}[X,Y]
  \forall R: X \rel Y @ (R \inv) \inv = R
\end{theorem}


\begin{theorem}{rule invComp}[X,Y,Z]
  \forall Q: X \rel Y; R: Y \rel Z @
    (Q \comp R) \inv = (R \inv) \comp (Q \inv)
\end{theorem}


\begin{theorem}{rule invId}[X]
  \forall S: \power X @  (\id S) \inv = \id S
\end{theorem}


\begin{theorem}{rule invDres}[X,Y]
  \forall S: \power X; R: X \rel Y @
    (S \dres R) \inv = (R \inv) \rres S
\end{theorem}


\begin{theorem}{rule invRres}[X,Y]
  \forall S: \power Y; R: X \rel Y @
    (R \rres S) \inv = S \dres (R \inv)
\end{theorem}


\begin{theorem}{rule invNdres}[X,Y]
  \forall S: \power X; R: X \rel Y @
    (S \ndres R) \inv = (R \inv) \nrres S
\end{theorem}


\begin{theorem}{rule invNrres}[X,Y]
  \forall S: \power Y; R: X \rel Y @
    (R \nrres S) \inv = S \ndres (R \inv)
\end{theorem}



\begin{theorem}{rule domInv}[X,Y]
  \forall R: X \rel Y @  \dom (R \inv) = \ran R
\end{theorem}


\begin{theorem}{rule ranInv}[X,Y]
  \forall R: X \rel Y @ \ran (R \inv) = \dom R
\end{theorem}


Rules about applying inverses appear in Section~\ref{def-pinj}.

\newpage

\subsection{Relational image }\label{def-image}


\subsubsection*{Definitions}


\begin{gendef}[X,Y]
  \_ \limg \_ \rimg: (X \rel Y) \cross \power X \fun \power Y
\where
 \Label{disabled rule imageDef}
  \forall R: X \rel Y; S: \power X @
    R \limg S \rimg = \ran (S \dres R)
\end{gendef}


\subsubsection*{Theorems}


\begin[disabled]{theorem}{rule inImage}[X,Y]
  \forall R: X \rel Y; S: \power X @
    y \in R \limg S \rimg \iff (\exists x: S @ x \inrel{R} y)
\end{theorem}


\begin{theorem}{imageSubsetRange}[X, Y]
  \forall R: X \rel Y; S: \power X @
    R \limg S \rimg \subseteq \ran R
\end{theorem}


\begin[disabled]{theorem}{rule imageMonotonic}[X,Y]
  \forall Q, R: X \rel Y; S, T: \power X | S \subseteq T \land  Q \subseteq R @
    Q \limg S \rimg \in \power (R \limg T \rimg)
\end{theorem}


\begin{theorem}{imageMonotonic1}[X,Y]
  \forall R: X \rel Y; S, T: \power X | S \subseteq T @
    R \limg S \rimg \subseteq R \limg T \rimg
\end{theorem}


\begin{theorem}{imageMonotonic2}[X,Y]
  \forall Q, R: X \rel Y; S: \power X | Q \subseteq R @
   Q \limg S \rimg \subseteq R \limg S \rimg
\end{theorem}


\begin{theorem}{rule imageNull}[X,Y]
  \forall R: X \rel Y @ R \limg \{\} \rimg = \{\}
\end{theorem}


\begin{theorem}{rule nullImage}[X,Y]
  \forall S: \power X @
    (\_ \limg \_ \rimg)[X,Y](\{ \}, S) = \{ \}
\end{theorem}

The following rule should perhaps be disabled, as it can lead to ugly formulas
(e.g., $R \limg \{ 1, 2 \} \rimg$ will be greatly expanded).
On the other hand, it is needed for calculating functional images (e.g.,
$succ \limg \{ 1, 2 \} \rimg$).


\begin{theorem}{rule imageCup}[X,Y]
  \forall R: X \rel Y; S, T: \power X @
    R \limg S \cup T \rimg = 
    R \limg S \rimg \cup R \limg T \rimg
\end{theorem}


\begin[disabled]{theorem}{rule fullImage}[X,Y]
  \forall R: X \rel Y | \dom R \in \power S @ R \limg S \rimg = \ran R
\end{theorem}


\begin{theorem}{rule firstImage}[X,Y]
  \forall S: X \rel Y @
    first \limg S \rimg = \dom S
\end{theorem}


\begin{theorem}{rule secondImage}[X,Y]
  \forall S: X \rel Y @
    second \limg S \rimg = \ran S
\end{theorem}


\begin{theorem}{rule idImage}[X]
  \forall S, T: \power X @ (\id S) \limg T \rimg = S \cap T
\end{theorem}


\begin{theorem}{rule imageDres}[X,Y]
  \forall R: X \rel Y; S, T: \power X @
     (S \dres R) \limg T \rimg = R \limg S \cap T \rimg
\end{theorem}


\begin{theorem}{rule imageRres}[X,Y]
  \forall R: X \rel Y; S: \power Y; T: \power T @
    (R \rres S) \limg T \rimg = R \limg T \rimg \cap S
\end{theorem}


\begin{theorem}{rule imageNdres}[X,Y]
  \forall R: X \rel Y; S, T: \power X @
     (S \ndres R) \limg T \rimg = R \limg T \setminus S \rimg
\end{theorem}


\begin{theorem}{rule imageNrres}[X,Y]
  \forall R: X \rel Y; S: \power Y; T: \power T @
    (R \nrres S) \limg T \rimg = R \limg T \rimg \setminus S
\end{theorem}


\begin{theorem}{rule imageComp}[X,Y,Z]
  \forall Q: X \rel Y; R: Y \rel Z; S: \power X @
    (Q \comp R)\limg S \rimg = R \limg Q \limg S \rimg \rimg
\end{theorem}


\begin{theorem}{rule inImageInv}[X,Y]
  \forall f: Y \pfun X; S: \power X @
        x \in f\inv \limg S \rimg
   \iff x \in \dom f \land f(x) \in S
\end{theorem}


\begin[disabled]{theorem}{rule domComp}[X,Y,Z]
  \forall Q: X \rel Y; R: Y \rel Z @
     \dom (Q \comp R) = Q\inv \limg \dom R \rimg
\end{theorem}


\begin[disabled]{theorem}{rule ranComp}[X,Y,Z]
  \forall Q: X \rel Y; R: Y \rel Z @
     \ran (Q \comp R) = R \limg \ran Q \rimg
\end{theorem}


\begin{theorem}{rule applicationInImage}[X,Y]
  \forall f: X \pfun Y; S: \power X @
    \forall x: S | x \in \dom f @
      f(x) \in f \limg S \rimg
\end{theorem}


\subsubsection*{Automation}

The following rules allow simple relational images to be
calculated, e.g.,
$succ \limg \{ 1, 2, 3 \} \rimg$.  The first rule is
disabled because of the if-form it introduces.


\begin[disabled]{theorem}{rule functionImageUnit}[X,Y]
  \forall f: X \pfun Y
     @ f \limg \{ x \} \rimg =
	\IF x \in \dom f
        \THEN \{ f(x) \}
        \ELSE \{\}
\end{theorem}


\begin{theorem}{rule functionImageUnitOnDom}[X,Y]
  \forall f: X \pfun Y
     | x \in \dom f
     @ f \limg \{ x \} \rimg = \{ f(x) \}
\end{theorem}


\begin{theorem}{rule functionImageUnitOffDom}[X,Y]
  \forall f: X \pfun Y
     | \lnot x \in \dom f
     @ f \limg \{ x \} \rimg = \{  \}
\end{theorem}



\begin{theorem}{rule image\_result}[X,Y]
  \forall R: X \rel Y; S: \power X @
    \power (\ran R) \in \power Z
  \implies
    R \limg S \rimg \in Z
\end{theorem}

\newpage

\subsection{Overriding }\label{def-oplus}


\subsubsection*{Definitions}


\syndef{\oplus}{infun5}{"&oplus"} \quad\verb'\oplus'


\begin{gendef}[X,Y]
  \_ \oplus \_: (X \rel Y) \cross (X \rel Y) \fun (X \rel Y)
\where
\Label{disabled rule oplusDef}
  \forall Q, R: X \rel Y @
    Q \oplus R = ((\dom R) \ndres Q) \cup R
\end{gendef}


\subsubsection*{Theorems}


\begin{theorem}{rule overrideInPowerCross}[X,Y]
  \forall A: \power X; B: \power Y @
     \forall Q,R: A \rel B @ Q \oplus R \in \power (A \cross B)
\end{theorem}


\begin{theorem}{rule overrideInRel}[X,Y]
  \forall A: \power X; B: \power Y @
     \forall Q,R: A \rel B @ Q \oplus R \in A \rel B
\end{theorem}


\begin{theorem}{rule overrideInPfun}[X,Y]
  \forall A: \power X; B: \power Y @
     \forall f, g: A \pfun B @ f \oplus g \in A \pfun B
\end{theorem}


\begin{theorem}{rule overrideInFun}[X,Y]
  \forall A: \power X; B: \power Y @
     \forall f: A \fun B; g: A \pfun B @ f \oplus g \in A \fun B
\end{theorem}


\begin{theorem}{rule overrideAssociates}[X,Y]
  \forall Q, R, S: X \rel Y @
     (Q \oplus R) \oplus S = Q \oplus (R \oplus S)
\end{theorem}


\begin{theorem}{rule overrideWithNull}[X,Y]
  \forall R: X \rel Y @ R \oplus \{\} = R
\end{theorem}

The following theorem has as a special case $\{\} \oplus R = R$.


\begin[disabled]{theorem}{rule overrideEverything}[X,Y]
  \forall Q, R: X \rel Y | \dom Q \subseteq \dom R @ Q \oplus R = R
\end{theorem}


\begin{theorem}{rule overrideNull}[X,Y]
  \forall R: X \rel Y @ \{\} \oplus R = R
\end{theorem}


\begin{theorem}{rule domOverride}[X,Y]
 \forall Q,R: X \rel Y @
    \dom (Q \oplus R) = (\dom Q) \cup (\dom R)
\end{theorem}


\begin{theorem}{rule overrideAppliesTo}[X,Y]
  \forall f, g: X \rel Y @
    (f \oplus g) ~ applies\$to ~ x
\iff g ~ applies\$to ~ x \lor (\lnot x \in \dom g \land f ~ applies\$to ~ x)
\end{theorem}


\begin[disabled]{theorem}{rule applyOverride}[X,Y]
  \forall f, g: X \rel Y; x: X | (f \oplus g) ~ applies\$to ~ x @
    (f \oplus g)(x) = \IF g ~ applies\$to ~ x  \THEN g(x) \ELSE f(x)
\end{theorem}



\begin{theorem}{rule applyOverride1}[X,Y]
  \forall f, g: X \rel Y; x: X | g ~ applies\$to ~ x @
    (f \oplus g)(x) = g(x)
\end{theorem}


\begin{theorem}{rule applyOverride2}[X,Y]
  \forall f, g: X \rel Y; x: X
    | \lnot x \in \dom g \land  f ~ applies\$to ~ x
    @ (f \oplus g)(x) = f(x)
\end{theorem}

\newpage

\subsection{Transitive closure }\label{def-tclosure}


\subsubsection*{Definitions}


\syndef{\plus}{postfun}{"&tclosure"} \quad\verb'\plus'


\syndef{\star}{postfun}{"&rtclosure"} \quad\verb'\star'


\begin{gendef}[X]
  \_ \plus, \_ \star: (X \rel X) \fun (X \rel X)
\where
\Label{disabled rule plusDef}
  \forall R: X \rel X @ R \plus =
    \bigcap \{~Q: X \rel X | R \subseteq Q \land Q \comp Q \subseteq Q~\}
\also
\Label{disabled rule starDef}
  \forall R: X \rel X @ R \plus =
    \bigcap \{~Q: X \rel X | \id X \subseteq Q \land 
                             R \subseteq Q \land
                             Q \comp Q \subseteq Q~\}
\end{gendef}


\subsubsection*{Theorems}


\begin{theorem}{rule domPlus}[X]
  \forall R: X \rel X @
    \dom (R \plus) = \dom R
\end{theorem}


\begin{theorem}{rule ranPlus}[X]
  \forall R: X \rel X @
    \ran (R \plus) = \ran R
\end{theorem}


\begin{theorem}{rule plusInRel}[X]
  \forall A,B: \power X; R: X \rel X @
      R \plus \in A \rel B
    \iff 
      R \in A \rel B
\end{theorem}


\begin{theorem}{rule domStar}[X]
  \forall R: X \rel X @
    \dom (R \star) = X
\end{theorem}


\begin{theorem}{rule ranStar}[X]
  \forall R: X \rel X @
    \ran (R \star) = X
\end{theorem}


\begin{theorem}{rule starInRel}[X]
  \forall R: X \rel X @
      R \star \in A \rel B
    \iff 
      X \in \power A \land X \in \power B
\end{theorem}


\begin{theorem}{rule nullPlus}[X]
  \{ \} \plus [X] = \{\}
\end{theorem}


\begin{theorem}{rule nullStar}[X]
  \{ \} \star = \id X
\end{theorem}


\begin{theorem}{plusMonotonic}[X]
  \forall Q, R: X \rel X
    | Q \subseteq R
    @ Q \plus \subseteq R \plus
\end{theorem}


\begin{theorem}{starMonotonic}[X]
  \forall Q, R: X \rel X
    | Q \subseteq R
    @ Q \star \subseteq R \star
\end{theorem}


Many more theorems should be added!

\newpage

\section{Functions }


\subsection{Function spaces }\label{def-pfun}


\subsubsection*{Definitions}

Partial and total function spaces are predefined; the definitions
are
$$X \pfun Y == \{~ f: X \rel Y | \forall x: X; y,y': Y |
	(x,y) \in f \land (x, y') \in f @ y = y' ~\}$$
and
$$X \fun Y ==
  \{~ f: X \pfun Y | \forall x: X @ \exists y: Y @ (x,y) \in f ~\}.$$




\subsubsection*{Theorems}


\begin[disabled]{theorem}{rule pfunDef}[X, Y]
\forall R: X \rel Y @
  R \in X \pfun Y \iff R\inv \comp R \subseteq \id Y
\end{theorem}


\begin{theorem}{rule nullInPfun}
  \{ \} \in A \pfun B
\end{theorem}


\begin{theorem}{rule nullInFun}
  \{\} \in A \fun B
\iff
  A = \{\}
\end{theorem}


\begin{theorem}{rule unitInPfun}
  \{ p \} \in A \pfun B
\iff
  p \in A \cross B
\end{theorem}


\begin{theorem}{rule cupInPfun}[X,Y]
\forall f, g: \power (X \cross Y); A: \power X; B: \power Y @\\
\t2  (f \cup g) \in A \pfun B\\
\t1 \iff\\
\t2     f \in A \pfun B \\
\t2 \land g \in A \pfun B\\
\t2 \land (\forall x: A | x \in \dom f \land x \in \dom g @ f(x) = g(x))
\end{theorem}


\begin[disabled]{theorem}{rule cupInFun}[X,Y]
\forall f, g: \power (X \cross Y); A: \power X; B: \power Y @\\
\t2  (f \cup g) \in A \fun B\\
\t1 \iff\\
\t2     f \in A \pfun B \\
\t2 \land g \in A \pfun B\\
\t2 \land (\forall x: A | x \in \dom f \land x \in \dom g @ f(x) = g(x)) \\
\t2 \land (\dom f) \cup (\dom g) = A
\end{theorem}


\begin{theorem}{subsetOfPfun}
  f \in A \pfun B \land g \in \power f
\implies
  g \in A \pfun B
\end{theorem}


\begin{theorem}{pfunExtensionality}[X,Y]
  \forall f, g: X \pfun Y @
    f = g \iff
    \dom f = \dom g \land (\forall x: \dom f @ f(x) = g(x))
\end{theorem}


\begin{theorem}{funExtensionality}[X,Y]
  \forall f, g: X \fun Y @
    f = g \iff (\forall x: X @ f(x) = g(x))
\end{theorem}



\subsubsection*{Automation}


\begin{theorem}{grule pfun\_type}[X,Y]
  X \pfun Y \in \power (X \rel Y)
\end{theorem}


\begin{theorem}{rule pfun\_sub}[X,Y]
  \forall A: \power X; B: \power Y @
    A \pfun B \in \power (X \pfun Y)
\end{theorem}


\begin{theorem}{rule pfun\_ideal}[X,Y]
  \power Z \in \power (X \pfun Y)
\iff
  Z \in X \pfun Y
\end{theorem}


\begin{theorem}{grule fun\_type}[X,Y]
  X \fun Y \in \power (X \pfun Y)
\end{theorem}


\begin{theorem}{rule fun\_sub}[X,Y]
  \forall B: \power Y @
    X \fun B \in \power (X \fun Y)
\end{theorem}


\begin{theorem}{rule domFunction}
               KnownMember[A \fun B]
         \land A \in \power X
         \land B \in \power Y
\implies \dom[X,Y] element = A
\end{theorem}

The following theorem might lead to non-maximal generic actuals in
$dom[A,B]$.


\begin{theorem}{rule applicationInDeclaredRangePfun}[A,B]
        KnownMember[A \pfun B]
  \land x \in \dom element
  \land B \in \power X
\implies
   element(x) \in X
\end{theorem}


\begin{theorem}{rule applicationInDeclaredRangeFun}[A,B]
        KnownMember[A \fun B]
  \land x \in A
  \land B \in \power X
\implies
   element(x) \in X
\end{theorem}

\newpage

\subsection{Application }

Function application is part of the Z syntax, so no definitions are needed.



\subsubsection*{Theorems}



\begin{theorem}{rule pfunAppliesTo}[X,Y]
  \forall f: X \pfun Y @
    f~applies\$to~x \iff x \in \dom f
\end{theorem}



\begin{theorem}{applyInRanPfun}[X,Y]
  \forall A: \power X; B: \power Y @
    \forall f: A \pfun B @
      \forall a: \dom f @
        f(a) \in \ran f \land f(a) \in B
\end{theorem}


\begin{theorem}{applyInRanFun}[X,Y]
  \forall f: X \fun Y; a: X @ f(a) \in Y
\end{theorem}


\begin{theorem}{pairInFunction}[X,Y]
  \forall f: X \pfun Y @
    (x, y) \in f \implies y = f(x)
\end{theorem}


\begin{theorem}{rule applyUnit}
   z = x
\implies
  \{ (x,y) \} (z) =  y
\end{theorem}


\begin{theorem}{rule applyCupLeft}[X,Y]
\forall f, g: X \rel Y @
        (f \cup g) \in X \pfun Y
  \land x \in \dom f
\implies
  (f \cup g)(x) = f(x)
\end{theorem}


\begin{theorem}{rule applyCupRight}[X,Y]
\forall f, g: X \rel Y @
       (f \cup g) \in X \pfun Y
  \land x \in \dom g
\implies
  (f \cup g)(x) = g(x)
\end{theorem}


\begin{theorem}{applySubset}[X,Y]
  \forall f, g: X \pfun Y; x: X | f \subseteq g \land x \in \dom f @
    f(x) = g(x)
\end{theorem}

\newpage

\subsection{Injections }\label{def-pinj}


\subsubsection*{Definitions}


\syndef{\pinj}{ingen}{"&pinj"} \quad\verb'\pinj'


\syndef{\inj}{ingen}{"&inj"} \quad\verb'\inj'


\begin[disabled]{zed}
  X \pinj Y == \{~ f: X \pfun Y | f \inv \in Y \pfun X ~\}
\end{zed}


\begin[disabled]{zed}
  X \inj Y == (X \pinj Y) \cap (X \fun Y)
\end{zed}


\subsubsection*{Theorems}


\begin{theorem}{rule nullInPinj}
  \{\} \in A \pinj B
\end{theorem}


\begin{theorem}{rule unitInPinj}
  \{ p \} \in A \pinj B
\iff
  p \in A \cross B
\end{theorem}


\begin{theorem}{rule nullInInj}
  \{\} \in A \inj B
\iff
  A = \{\}
\end{theorem}


\begin[disabled]{theorem}{rule cupInPinj}[X,Y]
\forall f, g: \power (X \cross Y); A: \power X; B: \power Y @\\
\t2  (f \cup g) \in A \pinj B\\
\t1 \iff\\
\t2     f \in A \pfun B \\
\t2 \land g \in A \pfun B\\
\t2 \land (\forall x: A | x \in \dom f \land x \in \dom g @ f(x) = g(x))\\
\t2 \land (\forall y: B | y \in \ran f \land y \in \ran g @ f\inv(y) = g\inv(y))
\end{theorem}



\begin{theorem}{pinjApplicationsEqual}[X,Y]
  \forall A: \power X; B: \power Y @
   \forall f: A \pinj B @
    \forall x, y: \dom f @ f(x) = f(y) \implies x = y
\end{theorem}


\begin{theorem}{subsetOfPinjIsPinj}[X,Y]
    \forall f: X \pinj Y @
      \forall g: \power f @
         g \in X \pinj Y
\end{theorem}



\begin{theorem}{applyInverse}[X,Y]
  \forall A: \power X; B: \power Y | f \in A \pinj B \land x \in \dom f @
     f\inv(f(x)) = x
\end{theorem}


\subsubsection*{Automation}


\begin{theorem}{grule pinj\_type}
  X \pinj Y \in \power (X \pfun Y)
\end{theorem}


\begin{theorem}{rule inj\_type}
  (X \pinj Y \in \power Z \lor X \fun Y \in \power Z)
\implies
  X \inj Y \in \power Z
\end{theorem}


\begin{theorem}{rule pinj\_sub}[X,Y]
  \forall A: \power X; B: \power Y @
    A \pinj B \in \power (X \pinj Y)
\end{theorem}


\begin{theorem}{rule inj\_sub}[X,Y]
  \forall B: \power Y @
    X \inj B \in \power (X \inj Y)
\end{theorem}


\begin{theorem}{rule pinj\_ideal}
  \power R \in \power (A \pinj B)
\iff
  R \in A \pinj B
\end{theorem}


\begin{theorem}{rule applicationInDeclaredRangePinj}[A,B]
        KnownMember[A \pinj B]
  \land x \in \dom element
  \land B \in \power X
\implies
   element(x) \in X
\end{theorem}


\begin{theorem}{rule domInjection}
               KnownMember[A \inj B]
         \land A \in \power X
         \land B \in \power Y
\implies \dom[X,Y] element = A
\end{theorem}


\begin{theorem}{rule applicationInDeclaredRangeInj}[A,B]
        KnownMember[A \inj B]
  \land x \in A
  \land B \in \power X
\implies
   element(x) \in X
\end{theorem}

We do not have enough rules to ``compute'' membership of a set construction
in
$A \inj B$.

\newpage

\subsection{Surjections }\label{def-psurj}


\subsubsection*{Definitions}


\syndef{\psurj}{ingen}{"&psurj"} \quad\verb'\psurj'


\syndef{\surj}{ingen}{"&surj"} \quad\verb'\surj'


\begin[disabled]{zed}
  X \psurj Y == \{~ f: X \pfun Y | \ran f = Y ~\}
\end{zed}


\begin[disabled]{zed}
  X \surj Y == (X \psurj Y) \cap (X \fun Y)
\end{zed}


\subsubsection*{Theorems}



\begin{theorem}{nullInPsurj}
  \{\} \in A \psurj B \iff B = \{\}
\end{theorem}


\begin{theorem}{unitInPsurj}
  \{ p \} \in A \psurj B \iff (p \in A \cross B \land B = \{ p.2 \})
\end{theorem}


\begin{theorem}{rule cupInPsurj}[X,Y]
\forall f, g: \power (X \cross Y); A: \power X; B: \power Y @\\
\t2  (f \cup g) \in A \psurj B\\
\t1 \iff\\
\t2     f \in A \pfun B \\
\t2 \land g \in A \pfun B\\
\t2 \land (\forall x: A | x \in \dom f \land x \in \dom g @ f(x) = g(x))\\
\t2 \land (\ran f) \cup (\ran g) = B
\end{theorem}



\subsubsection*{Automation}


\begin{theorem}{grule psurj\_type}
  X \psurj Y \in \power (X \pfun Y)
\end{theorem}


\begin{theorem}{rule psurj\_sub}[X,Y]
  \forall A: \power X @
    A \psurj Y \in \power (X \psurj Y)
\end{theorem}


\begin{theorem}{rule surj\_type}
  (X \psurj Y \in \power Z \lor X \fun Y \in \power Z)
\implies
  X \surj Y \in \power Z
\end{theorem}


\begin{theorem}{rule ranPsurj}[X,Y]
               KnownMember[A \psurj B]
         \land A \in \power X
         \land B \in \power Y
\implies \ran[X,Y] element = B
\end{theorem}


\begin{theorem}{rule applicationInDeclaredRangePsurj}[A,B]
        KnownMember[A \psurj B]
  \land x \in \dom element
  \land B \in \power X
\implies
   element(x) \in X
\end{theorem}


\begin{theorem}{rule domSurjection}[X,Y]
               KnownMember[A \surj B]
         \land A \in \power X
         \land B \in \power Y
\implies \dom[X,Y] element = A
\end{theorem}


\begin{theorem}{rule ranSurjection}[X,Y]
               KnownMember[A \surj B]
         \land A \in \power X
         \land B \in \power Y
\implies \ran[X,Y] element = B
\end{theorem}


\begin{theorem}{rule applicationInDeclaredRangeSurj}[A,B]
        KnownMember[A \surj B]
  \land x \in A
  \land B \in \power X
\implies
   element(x) \in X
\end{theorem}

We do not have enough rules to ``compute'' membership of a set construction
in
$A \surj B$.

\newpage

\subsection{Bijections }\label{def-bij}


\subsubsection*{Definitions}


\syndef{\bij}{ingen}{"&bij"} \quad\verb'\bij'


\begin[disabled]{zed}
  X \bij Y == (X \surj Y) \cap (X \inj Y)
\end{zed}


\subsubsection*{Theorems}


\begin{theorem}{rule nullInBij}
  \{ \} \in A \bij B \iff (A = \{\}\land B = \{\})
\end{theorem}


\begin{theorem}{rule unitInBij}
  \{ p \} \in A \bij B \iff (A = \{p.1\}\land B = \{p.2\})
\end{theorem}



\subsubsection*{Automation}


\begin{theorem}{rule bij\_type}
  (X \inj Y \in \power Z \lor X \surj Y \in \power Z)
\implies
  X \bij Y \in \power Z
\end{theorem}


\begin{theorem}{grule id\_type}
  \id X \in X \bij X
\end{theorem}


\begin{theorem}{rule domBijection}[X,Y]
               KnownMember[A \bij B]
         \land A \in \power X
         \land B \in \power Y
\implies \dom[X,Y] element = A
\end{theorem}


\begin{theorem}{rule ranBijection}[X,Y]
               KnownMember[A \bij B]
         \land A \in \power X
         \land B \in \power Y
\implies \ran[X,Y] element = B
\end{theorem}


\begin{theorem}{rule applicationInDeclaredRangeBij}[A,B]
        KnownMember[A \bij B]
  \land x \in A
  \land B \in \power X
\implies
   element(x) \in X
\end{theorem}

We do not have enough rules to ``compute'' membership of a set construction
in
$A \bij B$.

\newpage

\subsection{Inversion and function spaces }


\subsubsection*{Theorems }


\begin{theorem}{rule inverseInPfun}[X,Y]
  \forall A: \power X; B: \power Y @ 
     \forall f: B \pinj A @
       f\inv \in A \pfun B
\end{theorem}


\begin{theorem}{rule inverseInFun}[X,Y]
  \forall A: \power X; B: \power Y @ \forall f: B \pinj A @
     f\inv \in A \fun B \iff \ran f = A
\end{theorem}


\begin{theorem}{rule inverseInPinj}[X,Y]
  \forall A: \power X; B: \power Y; f: Y \rel X @
     f\inv \in A \pinj B \iff  f \in B \pinj A
\end{theorem}


\begin{theorem}{rule inverseInInj}[X,Y]
  \forall A: \power X; B: \power Y; f: Y \rel X @
     f\inv \in A \inj B \iff  f \in B \pinj A \land \ran f = A
\end{theorem}


\begin{theorem}{rule inverseInPsurj}[X,Y]
  \forall A: \power X; B: \power Y | f \in B \inj A @
     f\inv \in A \psurj B
\end{theorem}


\begin{theorem}{rule inverseInSurj}[X,Y]
  \forall A: \power X; B: \power Y | f \in B \bij A @
     f\inv \in A \surj B
\end{theorem}


\begin{theorem}{rule inverseBij}[X,Y]
  \forall A: \power Y; B: \power X; f: X \rel Y @
      f\inv \in A \bij B \iff f \in B \bij A
\end{theorem}

\newpage

\section{Numbers }


\begin{theorem}{integersExist}
  \lnot (\num = \{\})
\end{theorem}

Function
$the\$integer$ can be generated by a proof step; it is applied
to some expression whose value could not be determined to be integer.


\begin{theorem}{rule theIntegerElimination}
  \forall i: \num @ the\$integer(i) = i
\end{theorem}


\subsection{Arithmetic functions }

The arithmetic functions
$\_ + \_$,
$\_ - \_$,
$(-)$,
$\_ * \_$,
$\_ \div \_$ and
$\_ \mod \_$ are predefined.



\subsubsection*{Theorems}


\begin{theorem}{rule domDiv}
  \dom (\_ \div \_) = \num \cross (\num \setminus \{ 0 \})
\end{theorem}


\begin{theorem}{rule domMod}
  \dom (\_ \mod \_) = \num \cross (\num \setminus \{ 0 \})
\end{theorem}


\begin{theorem}{grule divModRelation}
  \forall x, y: \num | \lnot y = 0 @
    x = (x \div y) * y + (x \mod y)
\end{theorem}


\begin{theorem}{modRange1}
  \forall x,y: \num | y > 0 @ 0 \leq x \mod y < y
\end{theorem}


\begin{theorem}{modRange2}
  \forall x,y: \num | y < 0 @ y < x \mod y \leq 0
\end{theorem}

\newpage

\subsection{Arithmetic relations }

The relations
$\_ < \_$,
$\_ \leq \_$,
$\_ \geq \_$, and
$\_ > \_$ are
predefined.



\subsubsection*{Theorems}


\begin{theorem}{rule lessthanInv}
  (\_ < \_)\inv = (\_ > \_)
\end{theorem}


\begin{theorem}{rule leqInv}
  (\_ \leq \_)\inv = (\_ \geq \_)
\end{theorem}


\begin{theorem}{rule greaterthanInv}
  (\_ > \_)\inv = (\_ < \_)
\end{theorem}


\begin{theorem}{rule geqInv}
  (\_ \geq \_)\inv = (\_ \leq \_)
\end{theorem}

We could also have a number of theorems about composition of the
arithmetic relations.

\newpage

\subsection{Naturals }\label{def-nat}


\subsubsection*{Definitions}


\begin[disabled]{zed}
  \nat == \{~ n: \num | n \geq 0 ~\}
\end{zed}


\begin[disabled]{zed}
  \nat_1 == \{~ n: \nat | n \geq 1 ~\}
\end{zed}


\begin{axdef}
   succ: \nat \bij \nat_1
\where
\Label{rule succDef}
   \forall n: \nat @ succ(n) = n + 1
\end{axdef}


\subsubsection*{Theorems}


\begin{theorem}{rule inNat}
  x \in \nat \iff x \in \num \land x \geq 0
\end{theorem}


\begin{theorem}{rule inNat1}
  x \in \nat_1 \iff x \in \num \land x \geq 1
\end{theorem}


\begin{theorem}{natsExist}
  \lnot \nat = \{\}
\end{theorem}


\begin{theorem}{nat1sExist}
  \lnot \nat_1 = \{\}
\end{theorem}

The following theorem shows that functions on the naturals can be defined
inductively.

\begin{theorem}{primitiveRecursion}[X]
  \forall base: X; step: X \cross \nat \fun X @ \\ \t1
    \exists f: \nat \fun X @ \\ \t2
	    f(0) = base \land
	    (\forall n: \nat @ f(n+1) = step(f(n),n))
\end{theorem}

Here is another version of the primitive recursion theorem, where we allow the
defined function to have additional parameters.

\begin{theorem}{generalPrimitiveRecursion}[Result,Parameter]
  \forall base: Parameter \fun Result;
	step: Result \cross \nat \cross Parameter \fun Result @ \\ \t1
    \exists f: \nat \cross Parameter \fun Result @ \\ \t2
         \forall p: Parameter @ \\ \t3
	    f(0,p) = base(p) \land
	    ( \forall n: \nat @ f(n+1, p) = step(f(n, p),n,p))
\end{theorem}


\subsubsection*{Automation}


\begin{theorem}{grule natType}
  \nat \in \power \num
\end{theorem}


\begin{theorem}{grule nat1\_type}
  \nat_1 \in \power \nat
\end{theorem}

\newpage

\subsection{Relational iteration }\label{def-iter}


\subsubsection*{Definitions}


\begin{gendef}[X]
  iter: \num \fun (X \rel X) \fun (X \rel X)
\where
\Label{rule iter0}
  \forall R: X \rel X @ iter~0~R = \id X
\also
\Label{iterNegative}
  \forall R: X \rel X; n: \num | n < 0 @ iter~n~R = iter~(- n)~(R \inv)
\also
\Label{iterPositive}
  \forall R: X \rel X; n: \nat @
      iter~(n+1)~R =R \comp (iter~n~R)
\end{gendef}


\subsubsection*{Theorems}


\begin{theorem}{rule iterateId}[X]
  \forall n: \num; S: \power X @ (\id S) \bsup n \esup =
	\IF n = 0 \THEN \id X \ELSE \id S
\end{theorem}


\begin{theorem}{rule iterateEmpty}[X]
  \forall n: \num | \lnot n = 0 @
    iter[X]~n ~ \{ \} = \{ \}
\end{theorem}


\begin{theorem}{rule oneIteration}[X]
  \forall R: X \rel X @ R \bsup 1 \esup = R
\end{theorem}


\begin{theorem}{rule minusOneIteration}[X]
  \forall R: X \rel X @ R \bsup -1 \esup = R\inv
\end{theorem}


\begin[disabled]{theorem}{rule composePositiveIterates}[X]
  \forall n, k: \nat; R: X \rel Y @
     R \bsup n + k \esup = R \bsup n \esup \comp R \bsup k \esup
\end{theorem}


\begin{theorem}{inverseOfIteration}[X]
  \forall R: X \rel X; n: \num @ (R \bsup n \esup)\inv = R \bsup - n \esup
\end{theorem}


\begin{theorem}{iterInPlus}[X]
  \forall n: \nat_1; R: X \rel X @ R \bsup n \esup \subseteq R\plus
\end{theorem}


\begin{theorem}{iterInStar}[X]
  \forall n: \nat; R: X \rel X @ R \bsup n \esup \subseteq R\star
\end{theorem}

Many more theorems should be added.

\newpage

\subsection{Ranges }\label{def-upto}


\subsubsection*{Definitions}


\syndef{\upto}{infun2}{"&upto"} \quad\verb'\upto'


\begin{axdef}
  \_ \upto \_: \num \cross \num \fun \power \num
\where
\Label{disabled rule rangeDef}
  \forall a, b: \num @ a \upto b = \{~ k: \num | a \leq k \leq b ~\}
\end{axdef}


\subsubsection*{Theorems}


\begin{theorem}{rule inRange}
  \forall a, b: \num @
     x \in a \upto b \iff a \leq x \leq b
\end{theorem}


\begin{theorem}{rule rangeNull}
  a > b \implies a \upto b = \{\}
\end{theorem}


\begin{theorem}{rule rangeUnit}
  \forall a: \num @ a \upto a = \{ a \}
\end{theorem}



\begin{theorem}{rule rangeSubsetNat}
  \forall a, b: \num @
     a \upto b \in \power \nat \iff a \in \nat \lor b < a
\end{theorem}


\begin{theorem}{rule rangeSubsetNat1}
  \forall a, b: \num @
     a \upto b \in \power \nat_1 \iff a \in \nat_1 \lor b < a
\end{theorem}


\begin{theorem}{rule rangeSubsetRange}
  \forall a, b, c, d: \num @
     a \upto b \in \power (c \upto d) \iff
     b < a \lor (c \leq a \land b \leq d)
\end{theorem}


\begin{theorem}{rule rangeEqualRange}
  \forall a,b,c,d: \num @
     a \upto b = c \upto d \iff
       (a = c \land b = d) \lor (b < a \land d < c)
\end{theorem}

There should be theorems for unions, intersections, and differences of ranges.

\newpage

\subsection{Finiteness }\label{def-finset}


\subsubsection*{Definitions}


\syndef{\finset}{pregen}{"&fset"} \quad\verb'\finset'


\begin[disabled]{zed}
  \finset X == \{~S: \power X | \exists n: \nat @
			\exists f: 1 \upto n \fun S @ \ran f = S~\}
\end{zed}


\begin[disabled]{zed}
  \finset_1 X == (\finset X) \setminus \{ \{\} \}
\end{zed}


\subsubsection*{Theorems}


\begin{theorem}{rule inFinset1}[X]
  x \in \finset_1 X \iff x \in \finset X \land \lnot x = \{ \}
\end{theorem}


\begin{theorem}{rule nullFinite}[X]
  \{\} \in \finset X
\end{theorem}


\begin{theorem}{rule unitFinite}[X]
  \{ x \} \in \finset X \iff x \in X
\end{theorem}


\begin{theorem}{rule cupFinite}[X]
  \forall A,B: \power X @
    A \cup B \in \finset Y \iff (A \in \finset Y \land B \in \finset Y)
\end{theorem}


\begin{theorem}{rule numIsInfinite}
  \lnot (\num \in \finset \num)
\end{theorem}


\begin{theorem}{rule natIsInfinite}
  \lnot (\nat \in \finset \num)
\end{theorem}


\begin{theorem}{rule nat1IsInfinite}
  \lnot (\nat_1 \in \finset \num)
\end{theorem}


\begin{theorem}{rule powersetInFinset}[X]
    \power X \in \finset (\power Y)
\iff X \in \finset Y
\end{theorem}


\begin{theorem}{rule rangeInFinset}
  \forall a, b: \num @
    a \upto b \in \finset X \iff a \upto b \in \power X
\end{theorem}



\begin{theorem}{rule crossIsFinite2}[X,Y]
    \lnot (A \cross B = \{ \})
\implies
    ( A \cross B \in \finset (X \cross Y)
      \iff A \in \finset X \land B \in \finset Y)
\end{theorem}


\begin[disabled]{theorem}{rule finiteInduction}[X]
  \forall S: \power (\power X)
     | \{ \} \in S
       \land (\forall x: X; Y: S @ \{ x \} \cup Y \in S)
     @ \finset X \subseteq S
\end{theorem}


\begin[disabled]{theorem}{rule finite1Induction}[X]
  \forall S: \power (\power X)
     | (\forall x: X @ \{ x \} \in S)
       \land (\forall A, B: S @ A \cup B \in S)
     @ \finset_1 X \subseteq S
\end{theorem}


\subsubsection*{Automation}


\begin{theorem}{grule finset\_type}[X]
  \finset X \in \power (\power X)
\end{theorem}


\begin{theorem}{rule finset\_sub}
  \finset X \in \power (\finset Y)
\iff
  X \in \power Y
\end{theorem}


\begin{theorem}{rule finset\_ideal}
  \power X \in \power (\finset Y)
\iff
  X \in \finset Y
\end{theorem}



\begin{theorem}{grule finset1\_type}[X]
  \finset_1 X \in \power (\finset X)
\end{theorem}


\begin{theorem}{rule finset1\_sub}
  \finset_1 X \in \power (\finset_1 Y)
\iff
  X \in \power Y
\end{theorem}

\newpage

\subsection{Cardinality }\label{def-size}



\subsubsection*{Definitions}


\syndef{\#}{word}{"&cardinality"} \quad\verb'\#'


\begin{gendef}[X]
  \#: \finset X \fun \nat
\where
\Label{sizeDef}
  \forall S: \finset X @
    \exists f: 1 \upto (\# S) \bij S @ true
\end{gendef}


\subsubsection*{Theorems}



\begin[disabled]{theorem}{rule ranCard}[X]
  \ran (\#[X]) = \IF X \in \finset X \THEN 0 \upto \# X \ELSE \nat
\end{theorem}


\begin{theorem}{rule sizeNull}[X]
  \#[X] \{\} = 0
\end{theorem}


\begin{theorem}{rule sizeUnit}[X]
  \forall x: X @ \# \{ x \} = 1
\end{theorem}


\begin{theorem}{rule sizeRange}
  \forall a, b: \num @
    \# (a \upto b) = \IF a \leq b \THEN 1 + b - a \ELSE 0
\end{theorem}


\begin{theorem}{sizeOfSubset}[X]
  \forall T: \finset X | S \in \power T @
     0 \leq \# S \leq \# T
\end{theorem}


\begin{theorem}{rule cardAddElement}[X]
  \forall x: X; S: \finset X | \lnot x \in S @
    \# (\{ x \} \cup S) = 1 + \# S
\end{theorem}


\begin{theorem}{cardCup}[X]
  \forall S, T: \finset X @
    \# S + \# T = \# (S \cup T) + \# (S \cap T)
\end{theorem}


\begin{theorem}{cardDiff}[X]
  \forall S: \finset X; T: \power X @
    \# (S \setminus T) = \#S - \#(S \cap T)
\end{theorem}


\begin{theorem}{rule card0}[X]
  \forall S: \finset X @ \#S = 0 \iff S = \{ \}
\end{theorem}


\begin{theorem}{cardIsNonNegqative}[X]
  \forall S: \finset X @ \#S \geq 0 
\end{theorem}


\newpage

\subsection{Finite function spaces }\label{def-ffun}


\subsubsection*{Definitions}


\syndef{\ffun}{ingen}{"&fpfun"} \quad\verb'\ffun'


\syndef{\finj}{ingen}{"&fpinj"} \quad\verb'\finj'


\begin[disabled]{zed}
  X \ffun Y == (X \pfun Y) \cap \finset (X \cross Y)
\also
  X \finj Y == (X \ffun Y) \cap (X \pinj Y)
\end{zed}


\subsubsection*{Theorems}


\begin{theorem}{rule nullInFFun}
  \{\} \in A \ffun B
\end{theorem}


\begin{theorem}{rule unitInFFun}
  \{p\} \in A \ffun B \iff p \in A \cross B
\end{theorem}


\begin{theorem}{rule cupInFfun}[X,Y]
\forall f, g: \power (X \cross Y); A: \power X; B: \power Y @\\
\t2  (f \cup g) \in A \ffun B\\
\t1 \iff\\
\t2     f \in A \ffun B \\
\t2 \land g \in A \ffun B\\
\t2 \land (\forall x: A | x \in \dom f \land x \in \dom g @ f(x) = g(x))
\end{theorem}


\begin{theorem}{rule nullInFinj}
  \{\} \in A \finj B
\end{theorem}


\begin{theorem}{rule unitInFinj}
  \{p\} \in A \finj B \iff p \in A \cross B
\end{theorem}


\begin[disabled]{theorem}{rule cupInFinj}[X,Y]
\forall f, g: \power (X \cross Y); A: \power X; B: \power Y @\\
\t2  (f \cup g) \in A \finj B\\
\t1 \iff\\
\t2     f \in A \finj B \\
\t2 \land g \in A \finj B\\
\t2 \land (\forall x: A | x \in \dom f \land x \in \dom g @ f(x) = g(x))\\
\t2 \land (\forall y: \dom f; z: \dom g | f(y) = g(z) @ y = z)
\end{theorem}


\begin{theorem}{functionFinite}[X,Y]
  \forall A: \power X; B: \power Y @
     f \in A \ffun B \iff (f \in A \pfun B \land \dom f \in \finset X)
\end{theorem}


\begin{theorem}{finiteFunction}[X,Y]
  \forall f: X \ffun Y @
          \dom f \in \finset X
    \land \ran f \in \finset Y
    \land \# (\ran f) \leq \# (\dom f) = \# f
\end{theorem}


\subsubsection*{Automation}


\begin{theorem}{rule ffun\_type}
  (X \pfun Y \in \power Z \lor \finset (X \cross Y) \in \power Z)
\implies
  X \ffun Y \in \power Z
\end{theorem}


\begin{theorem}{rule finj\_type}
  (X \ffun Y \in \power Z \lor X \pinj Y \in \power Z)
\implies
  X \finj Y \in \power Z
\end{theorem}


\begin{theorem}{rule ffun\_ideal}
  \power R \in \power (X \ffun Y)
\iff
  R \in X \ffun Y
\end{theorem}


\begin{theorem}{rule finj\_ideal}
  \power R \in \power (X \finj Y)
\iff
  R \in X \finj Y
\end{theorem}


\begin{theorem}{rule ffun\_sub}[X,Y]
  \forall A: \power X; B: \power Y @
    A \ffun B \in \power (X \ffun Y)
\end{theorem}


\begin{theorem}{rule finj\_sub}[X,Y]
  \forall A: \power X; B: \power Y @
    A \finj B \in \power (X \finj Y)
\end{theorem}


\begin{theorem}{rule applicationInDeclaredRangeFfun}[A,B]
        KnownMember[A \ffun B]
  \land x \in \dom element
  \land B \in \power X
\implies
   element(x) \in X
\end{theorem}


\begin{theorem}{rule applicationInDeclaredRangeFinj}[A,B]
        KnownMember[A \finj B]
  \land x \in \dom element
  \land B \in \power X
\implies
   element(x) \in X
\end{theorem}


\newpage

\subsection{Min and max }\label{def-min}


\subsubsection*{Definitions}


\begin{axdef}
  min, max: \power_1 \num \pfun \num
\where
\Label{minDef}
  min = \{~S: \power \num; m: \num
	   | m \in S \land (\forall n: S @ m \leq n)~\}
\also
\Label{maxDef}
  max = \{~S: \power \num; m: \num
	   | m \in S \land (\forall n: S @ n \leq m)~\}
\end{axdef}


\subsubsection*{Theorems}


\begin{theorem}{maxProperty}
         S \in \dom max
\implies       max~S \in S
         \land (\forall n: S @ n \leq max~S)
\end{theorem}


\begin{theorem}{minProperty}
         S \in \dom min
\implies       min~S \in S
         \land (\forall n: S @ min~S \leq n)
\end{theorem}


\begin{theorem}{minBound}
  \forall S: \power \num; x: \num | (\forall n: S @ x \leq n) @
    S \in \dom min \land x \leq min~S 
\end{theorem}


\begin{theorem}{maxBound}
  \forall S: \power \num; x: \num | (\forall n: S @ n \leq x) @
    S \in \dom max \land  max~S \leq x
\end{theorem}


\begin{theorem}{explicitMin}
  \forall S: \power \num | x \in S \land (\forall n: S @ x \leq n) @
    S \in \dom min \land min~S = x
\end{theorem}


\begin{theorem}{explicitMax}
  \forall S: \power \num | x \in S \land (\forall n: S @ n \leq x) @
    S \in \dom max \land max~S = x
\end{theorem}



\begin{theorem}{rule natIsWellFounded}
   \forall S: \power \nat @
	S \in \dom min \iff \lnot S  = \{ \}
\end{theorem}


\begin{theorem}{rule finiteSetHasMin}
  S \in \finset_1 \num \implies S \in \dom min
\end{theorem}


\begin{theorem}{rule finiteSetHasMax}
  S \in \finset_1 \num \implies S \in \dom max
\end{theorem}


\begin{theorem}{rule minUnit}
  \forall x: \num @ min \{ x \} = x
\end{theorem}


\begin{theorem}{rule minRange}
  \forall a, b: \num | a \leq b @ min (a \upto b) = a
\end{theorem}


\begin{theorem}{rule maxUnit}
  \forall x: \num @ max \{ x \} = x
\end{theorem}


\begin{theorem}{rule maxRange}
  \forall a, b: \num | a \leq b @ max (a \upto b) = b
\end{theorem}


\begin{theorem}{rule cupInDomMin}
  S \neq \{ \} \land T \neq \{ \}
\implies
  (S \cup T \in \dom min \iff (S \in \dom min \land T \in \dom min))
\end{theorem}


\begin{theorem}{rule minCup}
  S \in \dom min \land T \in \dom min
\implies min (S \cup T) =
  \IF min~S < min~T
  \THEN min~S
  \ELSE min~T
\end{theorem}


\begin{theorem}{rule cupInDomMax}
  S \neq \{ \} \land T \neq \{ \}
\implies
  (S \cup T \in \dom max \iff (S \in \dom max \land T \in \dom max))
\end{theorem}


\begin{theorem}{rule maxCup}
  S \in \dom max \land T \in \dom max
\implies max (S \cup T) =
  \IF max~S < max~T
  \THEN max~T
  \ELSE max~S
\end{theorem}

\newpage

\subsection{Induction }

We express the induction schemes using set variables.  In order to use
induction to show
$\forall n: \nat @ P(n)$ for some property
$P$, one
first forms the set
$P\_values == \{~n: \nat | P(n)~\}$, then uses one
of the induction theorems to show
$\nat \subseteq P\_values$.  Rewriting
this (using $subDef$ and $inPower$) gives the original goal.



\subsubsection*{Theorems}


\begin[disabled]{theorem}{rule natInduction}
  \forall S: \power \num
     |       0 \in S
       \land (\forall x: S @ x + 1 \in S)
     @ \nat \subseteq S
\end{theorem}


\begin[disabled]{theorem}{rule nat1Induction}
  \forall S: \power \num
     |       1 \in S
       \land (\forall x: S @ x + 1 \in S)
     @ \nat_1 \subseteq S
\end{theorem}


\begin[disabled]{theorem}{rule natStrongInduction}
  \forall S: \power \num
     | (\forall x: \nat | (\forall y: \nat | y < x @ y \in S) @ x \in S)
     @ \nat \subseteq S
\end{theorem}


\begin[disabled]{theorem}{rule nat1StrongInduction}
  \forall S: \power \num
     | (\forall x: \nat_1 | (\forall y: \nat_1 | y < x @ y \in S) @ x \in S)
     @ \nat_1 \subseteq S
\end{theorem}

\newpage

\section{Sequences }\label{def-seq}


\subsection*{Definitions}


\syndef{\seq}{pregen}{"&seq"} \quad\verb'\seq'


\syndef{\iseq}{pregen}{"&iseq"} \quad\verb'\iseq'


\begin[disabled]{zed}
  \seq X == \{ f: \nat \pfun X | \exists n: \nat @ \dom f = 1 \upto n~\}
\also
  \seq_1 X == \{ f: \seq X | \# f > 0 \}
\also
  \iseq X == (\seq X) \cap (\nat \pinj X)
\end{zed}


\subsection*{Theorems}

It is sometimes useful to be able to convert sequence extensions to set
extensions.


\begin[disabled]{theorem}{rule nullSeqDef}
  \langle \rangle = \{ \}
\end{theorem}


\begin[disabled]{theorem}{rule unitSeqDef}
    \langle x \rangle = \{ (1, x) \}
\end{theorem}


\begin{theorem}{rule unitInSeq}[X]
  \langle x \rangle \in \seq X \iff x \in X
\end{theorem}


\begin{theorem}{rule unitInIseq}[X]
  \langle x \rangle \in \iseq X \iff x \in X
\end{theorem}


\begin{theorem}{rule inSeq1}[X]
  s \in \seq_1 X \iff s \in \seq X \land \lnot s = \langle \rangle
\end{theorem}


\begin{theorem}{rule applyUnitSeq}
  \langle x \rangle (1) = x
\end{theorem}


\begin{theorem}{rule sizeNullSeq}[X]
  \#[\num \cross X] \langle \rangle = 0
\end{theorem}


\begin{theorem}{rule sizeUnitSeq}[X]
  \forall x: X @
    \# \langle x \rangle = 1
\end{theorem}


\begin{theorem}{domSeq}[X]
  \forall s: \seq X @ \dom s = 1 \upto \# s
\end{theorem}


\begin{theorem}{rule unitIsNullSeq1}
  \lnot \langle x \rangle = \langle \rangle
\end{theorem}


\begin{theorem}{rule unitIsNullSeq2}
  \lnot \langle \rangle = \langle x \rangle
\end{theorem}


\begin{theorem}{rule unitsEqual}
  \langle x \rangle = \langle y \rangle \iff x = y
\end{theorem}


\begin{theorem}{rule ranNullSeq}[X]
  \ran[\num, X] \langle \rangle = \{ \}
\end{theorem}


\begin{theorem}{rule ranUnitSeq}[X]
  \forall x: X @ \ran \langle x \rangle = \{ x \}
\end{theorem}


\begin{theorem}{ranSeqInPower}[X]
  \forall s: \seq X @ \ran s \in \power Y \iff s \in \seq Y
\end{theorem}


\begin{theorem}{rule dresSeqInSeq}[X]
  \forall S: \power X @
    \forall a,b: \num; s: \seq S @
       (a \upto b) \dres s \in \seq S
       \iff ( a \leq 1 \lor b < a \lor a > \# s )
\end{theorem}



\begin{theorem}{rule seqSize0}[X]
  \forall s: \seq X @ \# s = 0 \iff s = \langle \rangle
\end{theorem}


\subsection*{Automation}


\begin{theorem}{grule seq\_type}[X]
  \seq X \in \power (\nat_1 \ffun X)
\end{theorem}


\begin{theorem}{grule seq1\_type}[X]
  \seq_1 X \in \power (\seq X)
\end{theorem}


\begin{theorem}{rule iseq\_type}[X]
  (\seq X \in \power Z \lor \nat_1 \finj X \in \power Z)
\implies
  \iseq X \in \power Z
\end{theorem}


\begin{theorem}{grule nullSeqType}
  \langle \rangle \in \iseq \{\}
\end{theorem}


\begin{theorem}{grule unitSeqType}
  \langle x \rangle \in \iseq \{ x \}
\end{theorem}


\begin{theorem}{rule seq\_sub}[Y]
  \seq X \in \power (\seq Y) \iff X \in \power Y
\end{theorem}


\begin{theorem}{rule seq1\_sub}[Y]
  \seq_1 X \in \power (\seq_1 Y) \iff X \in \power Y
\end{theorem}


\begin{theorem}{rule iseq\_sub}[Y]
  \iseq X \in \power (\iseq Y) \iff X \in \power Y
\end{theorem}


\begin{theorem}{rule domSeqRule}[X]
               KnownMember[\seq A]
         \land A \in \power X
\implies \dom element = 1 \upto \# element
\end{theorem}


\begin{theorem}{rule applicationInDeclaredRangeSeq}[A,B]
        KnownMember[\seq A]
  \land 1 \leq x \leq \# element
  \land A \in \power X
\implies
   element(x) \in X
\end{theorem}


\begin{theorem}{rule domIseqRule}[X]
               KnownMember[\iseq A]
         \land A \in \power X
\implies \dom element = 1 \upto \# element
\end{theorem}


\begin{theorem}{rule applicationInDeclaredRangeIseq}[A,B]
        KnownMember[\iseq A]
  \land 1 \leq x \leq \# element
  \land A \in \power X
\implies
   element(x) \in X
\end{theorem}


\newpage

\subsection{Concatenation }\label{def-cat}


\subsubsection*{Definitions}


\syndef{\cat}{infun3}{"&seqcat"} \quad\verb'\cat'


\begin{gendef}[X]
  \_ \cat \_: \seq X \cross \seq X \fun \seq X
\end{gendef}


\subsubsection*{Theorems}


\begin{theorem}{rule domCat}
  \seq X \cross \seq X \in \power A \land \seq X \in \power B
\implies
  \dom[A,B] (\_ \cat \_)[X] = \seq X \cross \seq X
\end{theorem}



\begin{theorem}{rule catInSeq}[X]
  \forall s, t: \seq X @
	 (s \cat t) \in \seq Y
    \iff (s \in \seq Y \land t \in \seq Y)
\end{theorem}



\begin{theorem}{rule sizeCat}[X]
  \forall s, t: \seq X @ \# (s \cat t) = (\# s) + (\# t)
\end{theorem}



\begin{theorem}{rule applyCat}[X]
  \forall s, t: \seq X @
    \forall n: 1 \upto \# s + \# t @
       (s \cat t)(n) = \IF n \leq \# s \THEN s(n) \ELSE t(n - \# s)
\end{theorem}


\begin{theorem}{rule ranCat}[X]
  \forall s, t: \seq X @
     \ran (s \cat t) = \ran s \cup \ran t
\end{theorem}


\begin{theorem}{rule nullCat}[X]
  \forall s: \seq X @ \langle \rangle \cat s = s
\end{theorem}


\begin{theorem}{rule catNull}[X]
  \forall s: \seq X @ s \cat \langle \rangle = s
\end{theorem}


\begin[disabled]{theorem}{rule catRightCancellation}[X]
  \forall s, t, u: \seq X @
         (s \cat u = t \cat u)
    \iff s = t
\end{theorem}


\begin[disabled]{theorem}{rule catLeftCancellation}[X]
  \forall s, t, u: \seq X @
         (s \cat t = s \cat u)
    \iff t = u
\end{theorem}


\begin{theorem}{rule catsEqual}[X]
  \forall x, y: X; s, t: \seq X @
    \langle x \rangle \cat s = \langle y \rangle \cat t
    \iff x = y \land s = t
\end{theorem}


\begin{theorem}{rule catAssociates}[X]
  \forall s, t, u: \seq X @
    (s \cat t) \cat u = s \cat (t \cat u)
\end{theorem}


\begin{theorem}{rule catYieldsNullseq}[X]
  \forall s, t: \seq X @
         ((s \cat t) = \langle \rangle)
    \iff s = \langle \rangle \land t = \langle \rangle
\end{theorem}

\newpage

\subsection{Sequence decomposition }\label{def-head}


\subsubsection*{Definitions}


\begin{gendef}[X]
  head, last: \seq_1 X \fun X \\
  tail, front: \seq_1 X \fun \seq X
\where
\Label{disabled rule headDef}
  \forall s: \seq_1 X @ head~s = s(1)
\also
\Label{disabled rule lastDef}
  \forall s: \seq_1 X @ last~s = s(\# s)
\also
\Label{disabled rule tailDef}
  \forall s: \seq_1 X @ tail~s = (\lambda n: 1 \upto \# s - 1 @ s(n+1))
\also
\Label{disabled rule frontDef}
  \forall s: \seq_1 X @ front~s = (\lambda n: 1 \upto \# s - 1 @ s(n))
\end{gendef}


\subsubsection*{Theorems}


\begin{theorem}{rule headInSet}[X]
  \forall Y: \power X @ \forall s: \seq_1 Y @ head~s \in Y
\end{theorem}


\begin{theorem}{rule lastInSet}[X]
  \forall Y: \power X @ \forall s: \seq_1 Y @ last~s \in Y
\end{theorem}


\begin{theorem}{rule tailInSeq}[X]
  \forall Y: \power X @ \forall s: \seq_1 Y @ tail~s \in \seq Y
\end{theorem}


\begin{theorem}{rule frontInSeq}[X]
  \forall Y: \power X @ \forall s: \seq_1 Y @ front~s \in \seq Y
\end{theorem}


\begin{theorem}{headTailComposition}[X]
  \forall s: \seq_1 X @ s = \langle head~s \rangle \cat (tail~s)
\end{theorem}


\begin{theorem}{frontLastComposition}[X]
  \forall s: \seq_1 X @ s = (front~s) \cat \langle last~s \rangle
\end{theorem}


\begin{theorem}{rule cardTail}[X]
  \forall s: \seq_1 X @ \# (tail~s) = (\# s) - 1
\end{theorem}


\begin{theorem}{rule applyTail}[X]
  \forall s: \seq_1 X
     | 1 \leq n < \# s
     @ (tail~s)(n) = s(n+1)
\end{theorem}


\begin{theorem}{rule cardFront}[X]
  \forall s: \seq_1 X @ \# (front~s) = (\# s) - 1
\end{theorem}


\begin{theorem}{rule applyFront}[X]
  \forall s: \seq_1 X
     | 1 \leq n < \# s
     @ (front~s)(n) = s(n)
\end{theorem}


\begin{theorem}{rule headUnit}[X]
  \forall x: X @ head~\langle x \rangle = x
\end{theorem}


\begin{theorem}{rule headCat}[X]
  \forall s, t: \seq X | \lnot s = \langle \rangle @
	head~(s \cat t) = head~s
\end{theorem}


\begin{theorem}{rule tailUnit}[X]
  \forall x: X @ tail~\langle x \rangle = \langle \rangle
\end{theorem}


\begin{theorem}{rule tailCat}[X]
  \forall s, t: \seq X | \lnot s = \langle \rangle @
	tail~(s \cat t) = (tail~s) \cat t
\end{theorem}


\begin{theorem}{rule lastUnit}[X]
  \forall x: X @ last~\langle x \rangle = x
\end{theorem}


\begin{theorem}{rule lastCat}[X]
  \forall s, t: \seq X | \lnot t = \langle \rangle @
	last~(s \cat t) = last ~ t
\end{theorem}


\begin{theorem}{rule frontUnit}[X]
  \forall x: X @ front~\langle x \rangle = \langle \rangle
\end{theorem}


\begin{theorem}{rule frontCat}[X]
  \forall s, t: \seq X | \lnot t = \langle \rangle @
	front~(s \cat t) = s \cat (front~t)
\end{theorem}


\subsubsection*{Automation}


\begin{theorem}{rule tail\_result}[X]
  \forall s: \seq_1 X | \seq (\ran s) \in \power Z @ tail~s \in Z
\end{theorem}


\begin{theorem}{rule front\_result}[X]
  \forall s: \seq_1 X | \power s \in \power Z  @ front~s \in Z
\end{theorem}


\begin{theorem}{rule head\_result}[X]
  \forall s: \seq_1 X | \ran s \in \power Z @ head~s \in Z
\end{theorem}


\begin{theorem}{rule last\_result}[X]
  \forall s: \seq_1 X | \ran s \in \power Z @ last~s \in Z
\end{theorem}

\newpage

\subsection{Reversal }\label{def-rev}


\subsubsection*{Definitions}


\begin{gendef}[X]
  rev: \seq X \fun \seq X
\where
\Label{rule revNull}
  rev~\langle \rangle = \langle \rangle
\also
\Label{rule revUnit}
  \forall x: X @ rev \langle x \rangle = \langle x \rangle
\also
\Label{rule revCat}
  \forall s, t: \seq X @
    rev (s \cat t) = (rev ~ t) \cat (rev ~ s)
\end{gendef}


\subsubsection*{Theorems}


\begin{theorem}{rule revInSeq}[X]
  \forall s: \seq X @
     rev~s \in \seq Y \iff s \in \seq Y
\end{theorem}


\begin{theorem}{rule revInIseq}[X]
  \forall s: \seq X @
     rev~s \in \iseq Y \iff s \in \iseq Y
\end{theorem}


\begin{theorem}{rule revRev}[X]
  \forall s: \seq X @ rev (rev ~ s) = s
\end{theorem}


\begin{theorem}{rule domRev}[X]
  \forall s: \seq X @ \dom (rev ~ s) = \dom s
\end{theorem}


\begin{theorem}{rule ranRev}[X]
  \forall s: \seq X @ \ran (rev ~ s) = \ran s
\end{theorem}


\begin{theorem}{rule cardRev}[X]
  \forall s: \seq X @ \# (rev ~ s) = \# s
\end{theorem}



\begin{theorem}{rule tailRev}[X]
  \forall s: \seq_1 X @ tail (rev~s) = rev~(front ~ s)
\end{theorem}


\begin{theorem}{rule frontRev}[X]
  \forall s: \seq_1 X @ front (rev~s) = rev~(tail ~ s)
\end{theorem}


\begin{theorem}{rule headRev}[X]
  \forall s: \seq_1 X @ head (rev~s) = last~s
\end{theorem}


\begin{theorem}{rule lastRev}[X]
  \forall s: \seq_1 X @ last (rev~s) = head~s
\end{theorem}



\begin{theorem}{rule applyRev}[X]
  \forall s: \seq X | 1 \leq n \leq \# s @ (rev~s)(n) = s(1 + (\# s) - n)
\end{theorem}

\newpage

\subsection{Filtering }\label{def-filter}


\subsubsection*{Definitions}


\syndef{\filter}{infun4}{"&filter"} \quad\verb'\filter'


\syndef{\extract}{infun4}{"&extract"} \quad\verb'\extract'


\begin{gendef}[X]
  \_ \extract \_: \power \num \cross \seq X  \fun \seq X\\
  \_ \filter \_: \seq X \cross \power X  \fun \seq X \\
  squash: (\nat_1 \ffun X) \fun \seq X
\where
\Label{extractDef}
  \forall E: \power \num; s: \seq X @
      E \extract s = squash (E \dres s)
\also
\Label{filterDef}
  \forall s: \seq X; F: \power X @
     s \filter F = squash (s \rres F)
\also
\Label{squashDef}
  \forall f: \nat_1 \ffun X @ \\ \t1
      \exists g: 1 \upto \# f \finj (\dom f) \\ \t2
          | (\forall i, j: \dom g | i < j @ g(i) < g(j)) \\ \t2
          @ squash(f) = g \comp f
\end{gendef}
      

Spivey specifies
$\_ \extract \_: \power \nat_1 \cross \ldots$; there seemed to
be no obvious reason why that domain could not be enlarged.



\subsubsection*{Theorems}


\begin{theorem}{rule extractNull}[X]
  \forall E: \power \num @
    E \extract[X] \langle \rangle = \langle \rangle
\end{theorem}


\begin[disabled]{theorem}{rule extractUnit}[X]
  \forall E: \power \num; x: X @
    E \extract \langle x \rangle =
	\IF 1 \in E \THEN \langle x \rangle \ELSE \langle \rangle
\end{theorem}


\begin{theorem}{rule extractUnit1}[X]
  \forall E: \power \num; x: X | 1 \in E @
    E \extract \langle x \rangle = \langle x \rangle
\end{theorem}


\begin{theorem}{rule extractUnit2}[X]
  \forall E: \power \num; x: X | 1 \notin E @
    E \extract \langle x \rangle = \langle \rangle
\end{theorem}


\begin[disabled]{theorem}{rule extractAll}[X]
  \forall E: \power \num; s: \seq X | \dom s \in \power E @
    E \extract s = s
\end{theorem}


\begin[disabled]{theorem}{rule extractNone}[X]
  \forall E: \power \num; s: \seq X | (\dom s) \cap E = \{\} @
    E \extract s = \langle \rangle
\end{theorem}


\begin{theorem}{rule nullExtract}[X]
  \forall s: \seq X @ \{\} \extract s = \langle \rangle
\end{theorem}


\begin{theorem}{rule extractIsSeq}[X]
    \forall E: \power \num; Y: \power X @ \forall s: \seq Y @
       E \extract s \in \seq Y
\end{theorem}


\begin{theorem}{rule extractIsIseq}[X]
    \forall E: \power \num; Y: \power X @ \forall s: \iseq Y @
       E \extract s \in \iseq Y
\end{theorem}


\begin[disabled]{theorem}{rule sizeExtract}[X]
  \forall E: \power \num; s: \seq X @
    \# (E \extract s) = \# (E \cap (1 \upto \# s))
\end{theorem}


\begin{theorem}{rule nullFilter}[X]
  \forall F: \power X @ \langle \rangle \filter F = \langle \rangle
\end{theorem}


\begin[disabled]{theorem}{rule filterUnit}[X]
  \forall F: \power X; x: X @
    \langle x \rangle \filter F =
	\IF x \in F \THEN \langle x \rangle \ELSE \langle \rangle
\end{theorem}


\begin{theorem}{rule filterUnit1}[X]
  \forall F: \power X @ \forall x: F @
    \langle x \rangle \filter F = \langle x \rangle
\end{theorem}


\begin{theorem}{rule filterUnit2}[X]
  \forall F: \power X; x: X
    | \lnot x \in F
    @ \langle x \rangle \filter F = \langle \rangle
\end{theorem}


\begin{theorem}{rule filterCat}[X]
  \forall F: \power X; s, t: \seq X @
    (s \cat t) \filter F = (s \filter F) \cat (t \filter F)
\end{theorem}


\begin[disabled]{theorem}{rule filterAll}[X]
  \forall F: \power X; s: \seq X
     | F \cap \ran s = \{ \}
     @ s \filter F = \langle \rangle
\end{theorem}


\begin[disabled]{theorem}{rule filterNone}[X]
  \forall F: \power X; s: \seq X
     | \ran s \subseteq F
     @ s \filter F = s
\end{theorem}


\begin{theorem}{rule filterNull}[X]
  \forall s: \seq X @ s \filter \{\} = \langle \rangle
\end{theorem}


\begin{theorem}{rule filterInSeq1}[X]
  \forall s: \seq X; F: \power Z @
    (s \filter F) \in \seq Z
\end{theorem}


\begin{theorem}{rule filterInSeq2}[X]
  \forall s: \seq Z; F: \power X @
    (s \filter F) \in \seq Z
\end{theorem}


\begin{theorem}{rule filterInIseq1}[X]
  \forall s: \iseq X; F: \power Z @
    (s \filter F) \in \iseq Z
\end{theorem}


\begin{theorem}{rule filterInIseq2}[X]
  \forall s: \iseq Z; F: \power X @
    (s \filter F) \in \iseq Z
\end{theorem}


\begin{theorem}{rule ranFilter}[X]
  \forall s: \seq X; F: \power X @
     \ran (s \filter F) = (\ran s) \cap F
\end{theorem}


\begin{theorem}{rule revFilter}[X]
  \forall s: \seq X; F: \power X @
    rev (s \filter F) = (rev ~ s) \filter F
\end{theorem}


\begin{theorem}{rule sizeFilter}[X]
  \forall s: \seq X; F: \power X @ \# (s \filter F) \leq \# s
\end{theorem}



\begin{theorem}{rule squashInSeq}[X]
  \forall Y: \power X @
    \forall f: \nat_1 \ffun Y @
      squash(f) \in \seq Y
\end{theorem}


\begin{theorem}{rule squashInIseq}[X]
  \forall Y: \power X @
    \forall f: \nat_1 \finj Y @
      squash(f) \in \iseq Y
\end{theorem}


\begin{theorem}{rule squashNull}[X]
  squash[X] (\{\}) = \langle \rangle
\end{theorem}


\begin{theorem}{rule squashUnit}[X]
  \forall p: \nat_1 \cross X @ squash \{ p \} = \langle p.2 \rangle
\end{theorem}

There should be other rules about squash.



\subsubsection*{Automation}

We should perhaps offer $filterResult$, $extractResult$, and
$squashResult$.

\newpage

\subsection{Mapping over a sequence }

Mapping a function $f$ over a sequence
$s = \langle x_1, x_2, \ldots\rangle$
results in the sequence $\langle f(x_1), f(x_2), \ldots\rangle$.
There is no special function for this in Z; since sequences are functions,
composition can be used instead.  The above result can be expressed as
$ f \circ s $ or $ s \comp f $.


\subsubsection*{Theorems}

The following three theorems allow for the computation of
mapping of a function over a literal sequence.


\begin{theorem}{rule mapSeqNull}[X,Y]
  \forall f: X \rel Y @ \langle \rangle \comp f = \langle \rangle
\end{theorem}


\begin{theorem}{rule mapSeqUnit}[X,Y]
  \forall f: X \pfun Y; x: X 
    | x \in \dom f
    @ \langle x \rangle \comp f = \langle f(x)\rangle
\end{theorem}



\begin{theorem}{rule mapSeqCat}[X,Y]
  \forall f: X \pfun Y; s, t: \seq X
    | \ran s \subseteq \dom f \land \ran t \subseteq \dom f
    @ (s \cat t) \comp f = (s \comp f) \cat (t \comp f)
\end{theorem}


\newpage

\subsection{Relations between sequences }\label{def-prefix}


\subsubsection*{Definitions}


\syndef{\prefix}{inrel}{"&prefix"} \quad\verb'\prefix'


\syndef{\suffix}{inrel}{"&suffix"} \quad\verb'\suffix'


\syndef{\inseq}{inrel}{"&inseq"} \quad\verb'\inseq'


\begin{gendef}[X]
  \_ \prefix \_, \_ \suffix \_, \_ \inseq \_: \seq X \rel \seq X 
\where
  \forall s, t: \seq X @
      s \prefix t \iff (\exists u: \seq X @ s \cat u = t)
\also
  \forall s, t: \seq X @
      s \suffix t \iff (\exists u: \seq X @ u \cat s = t)
\also
  \forall s, t: \seq X @
      s \inseq t \iff (\exists u,v: \seq X @ u \cat s \cat v = t)
\end{gendef}


\subsubsection*{Theorems}


\begin{theorem}{rule nullPrefix}[X]
  \forall t: \seq X @  \langle \rangle \prefix t
\end{theorem}


\begin{theorem}{rule prefixNull}[X]
  \forall s: \seq X @ s \prefix \langle \rangle \iff s = \langle \rangle
\end{theorem}


\begin{theorem}{rule nullSuffix}[X]
  \forall t: \seq X @ \langle \rangle \suffix t
\end{theorem}


\begin{theorem}{rule suffixNull}[X]
  \forall s: \seq X @ s \suffix \langle \rangle \iff s = \langle \rangle
\end{theorem}


\begin{theorem}{rule nullInseq}[X]
  \forall t: \seq X @ \langle \rangle \inseq t
\end{theorem}


\begin{theorem}{rule inseqNull}[X]
  \forall s: \seq X @ s \inseq \langle \rangle \iff s = \langle \rangle
\end{theorem}


\begin{theorem}{prefixRev}[X]
  \forall s, t: \seq X @ s \prefix t \iff rev(s) \suffix rev(t)
\end{theorem}


\begin{theorem}{inSeqRev}[X]
  \forall s, t: \seq X @ rev(s) \inseq rev(t) \implies s \inseq t
\end{theorem}

The partial order laws should be added.

\newpage

\subsection{Distributed concatenation }\label{def-dcat}


\subsubsection*{Definitions}


\begin{gendef}[X]
  \dcat: \seq (\seq X) \fun \seq X
\where
\Label{rule dcatNull}
  \dcat \langle \rangle = \langle \rangle
\also
\Label{rule dcatUnit}
  \forall s: \seq X @ \dcat \langle s \rangle = s
\also
\Label{rule dcatCat}
  \forall s, t: \seq (\seq X) @
     \dcat (s \cat t) = (\dcat s) \cat (\dcat t)
\end{gendef}


\subsubsection*{Theorems}


\begin{theorem}{rule dcatInSeq}[X]
  \forall s: \seq (\seq X); Y: \power X @
    \dcat s \in \seq Y \iff s \in \seq(\seq Y)
\end{theorem}

\newpage

\subsection{Disjointness and partitioning }\label{def-disjoint}


\subsubsection*{Definitions}


\syndef{\disjoint}{prerel}{"&disjoint"} \quad\verb'\disjoint'


\syndef{\partition}{inrel}{"&partition"} \quad\verb'\partition'


\begin{gendef}[I,X]
  \disjoint \_: \power (I \pfun \power X) \\
  \_ \partition \_: (I \pfun \power X) \rel \power X
\where
\Label{disabled rule disjointDef}
  \forall S: I \pfun \power X @
    \disjoint S \iff
    (\forall i, j: \dom S | \lnot i = j @ S(i) \cap S(j) = \{ \})
\also
\Label{rule partitionDef}
  \forall S: I \pfun \power X; T: \power X @
    S \partition T \iff \disjoint S \land \bigcup (\ran S) = T
\end{gendef}


\subsubsection*{Theorems}


\begin{theorem}{rule disjointEmpty}[I,X]
  \disjoint[I,X]~\{ \}
\end{theorem}


\begin{theorem}{rule disjointNull}[X]
  \disjoint[\num, X]~\langle \rangle
\end{theorem}


\begin{theorem}{rule disjointUnit}[I,X]
  \forall x: I \cross \power X @ \disjoint \{ x \}
\end{theorem}


\begin{theorem}{rule disjointUnitSeq}[X]
  \forall x: \power X @ \disjoint \langle x \rangle
\end{theorem}


\begin[disabled]{theorem}{rule disjointCat}[X]
  \forall s, t: \seq (\power X) @
        \disjoint (s \cat t)
   \iff       \disjoint s
        \land \disjoint t
        \land (\bigcup (\ran s)) \cap (\bigcup (\ran t)) = \{ \}
\end{theorem}

\newpage

\subsection{Induction }
The comments on integer induction apply equally well here.


\begin[disabled]{theorem}{rule seqInduction}[X]
  \forall A: \power X @
   \forall S: \power (\seq A) |
          \langle \rangle \in S
     \land (\forall x: A @ \langle x \rangle \in S)
     \land (\forall s, t: S @ s \cat t \in S)
  @ \seq A \subseteq S
\end{theorem}


\begin[disabled]{theorem}{rule seqLeftInduction}[X]
  \forall A: \power X; S: \power (\seq X) |
          \langle \rangle \in S
     \land (\forall x: A; s: S @ \langle x \rangle \cat s \in S)
  @ \seq A \subseteq S
\end{theorem}


\begin[disabled]{theorem}{rule seqRightInduction}[X]
  \forall A: \power X; S: \power (\seq X) |
          \langle \rangle \in S
     \land (\forall x: A; s: S @ s \cat \langle x \rangle \in S)
  @ \seq A \subseteq S
\end{theorem}


\begin[disabled]{theorem}{rule seq1Induction}[X]
  \forall A: \power X @
    \forall S: \power (\seq A) |
          (\forall x: A @ \langle x \rangle \in S)
    \land (\forall s, t: S @ s \cat t \in S)
  @ \seq_1 A \subseteq S
\end{theorem}

\newpage

\section{Bags }\label{def-bag}


\subsection*{Definitions}


\syndef{\bag}{pregen}{"&bag"} \quad\verb'\bag'

We define $ \bag X$ as $X \pfun \nat_1$ rather than
$X \fun \nat$ so that $A \subseteq B$ implies 
$ \bag A \subseteq \bag B$.


\begin[disabled]{zed}
  \bag X == X \pfun \nat_1
\end{zed}


\subsection*{Theorems}

It is sometimes useful to turn bag extensions into set extensions.


\begin[disabled]{theorem}{rule nullBagDef}
  \lbag \rbag = \{ \}
\end{theorem}


\begin[disabled]{theorem}{rule unitBagDef}
    \lbag x \rbag = \{ (x, 1) \}
\end{theorem}


\begin{theorem}{grule unitBagType}
  \lbag x \rbag \in \bag \{ x \}
\end{theorem}


\begin{theorem}{rule unitInBag}
  \lbag x \rbag \in \bag X \iff x \in X
\end{theorem}

Some specifiers use set constructions as bags; the following three
rules account for that:


\begin{theorem}{rule nullsetInBag}[X]
  \{ \} \in \bag X
\end{theorem}


\begin{theorem}{rule unitsetInBag}[X]
  \{ x \} \in \bag X \iff x \in X \cross \nat_1
\end{theorem}


\begin{theorem}{rule cupInBag}[X]
  \forall S, T: \power (X \cross \num); Y: \power X
      | (\dom S) \cap \dom T= \{\} \\ \t1
      @      S \cup T \in \bag Y
        \iff S \in \bag Y \land T \in \bag Y
\end{theorem}


\begin{theorem}{rule sizeNullBag}[X]
  \#[X \cross \num] \lbag \rbag = 0
\end{theorem}


\begin{theorem}{rule sizeUnitBag}[X]
  \forall x: X @
    \# \lbag x \rbag = 1
\end{theorem}


\begin{theorem}{rule unitIsNullBag1}
  \lnot \lbag x \rbag = \lbag \rbag
\end{theorem}


\begin{theorem}{rule unitIsNullBag2}
  \lnot \lbag \rbag = \lbag x \rbag
\end{theorem}


\begin{theorem}{rule unitBagsEqual}
  \lbag x \rbag = \lbag y \rbag\iff x = y
\end{theorem}

If $B$ is a bag, $\dom B$ gives the set of elements of the bag.


\begin{theorem}{rule domNullBag}[X]
  \dom[X, \num] \lbag \rbag = \{ \}
\end{theorem}


\begin{theorem}{rule domUnitBag}[X]
  \forall x: X @ \dom \lbag x \rbag = \{ x \}
\end{theorem}


\subsection*{Automation}


\begin{theorem}{grule bag\_type}
  \bag X \in \power (X \pfun \nat_1)
\end{theorem}


\begin{theorem}{rule bag\_sub}
  \bag X \in \power (\bag Y)
\iff
  X \in \power Y
\end{theorem}


\begin{theorem}{rule bag\_ideal}
  \power R \in \power (\bag X)
\iff
  R \in \bag X
\end{theorem}


\begin{theorem}{grule nullBagType}
  \lbag \rbag \in \bag \{\}
\end{theorem}

\newpage

\subsection{Bag count }\label{def-inbag}


\subsubsection*{Definitions}


\syndef{\inbag}{inrel}{"&inbag"} \quad\verb'\inbag'


\syndef{\bcount}{infun5}{"&bagcount"} \quad\verb'\bcount'


\begin{gendef}[X]
  \_ \inbag \_: X \rel \bag X \\
  count: \bag X \fun (X \fun \nat) \\
  \_ \bcount \_: \bag X \cross X \fun \nat
\where
\Label{disabled rule inbagDef}
  \forall x: X; B: \bag X @ x \inbag B \iff x \in \dom B
\also
\Label{rule countDef}
  \forall x: X; B: \bag X @ (count ~ B)x = B \bcount x
\also
\Label{disabled rule bcountDef}
  \forall x: X; B: \bag X @ B \bcount x =
    \IF x \inbag B \THEN B(x) \ELSE 0
\end{gendef}


\subsubsection*{Theorems}


\begin{theorem}{rule domCount}[X]
  \forall B: \bag X @ \dom (count~B) = X
\end{theorem}


\begin{theorem}{rule inNullBag}[X]
  \lnot x \inbag[X] \lbag \rbag
\end{theorem}


\begin{theorem}{rule inUnitBag}[X]
  x \inbag \lbag y \rbag \iff x \in X \land x = y
\end{theorem}


\begin{theorem}{rule bcountNullBag}[X]
  \forall x: X @ \lbag \rbag \bcount x = 0
\end{theorem}


\begin{theorem}{rule bcountUnitBag}[X]
  \forall x, y: X @
	\lbag x \rbag \bcount y = \IF x = y \THEN 1 \ELSE 0
\end{theorem}


\begin{theorem}{bagExtensionality}[X]
  \forall A, B: \bag X @
    A = B \iff (\forall x: X @ A \bcount x = B \bcount x)
\end{theorem}


\newpage

\subsection{Subbags }\label{def-subbageq}


\subsubsection*{Definitions}


\syndef{\subbageq}{inrel}{"&subbageq"} \quad\verb'\subbageq'


\begin{gendef}[X]
  \_ \subbageq \_: \bag X \rel \bag X \\
\where
\Label{disabled rule subbagDef}
  \forall A, B: \bag X @ A \subbageq B \iff
	(\forall x: X @ A \bcount x \leq B \bcount x)
\end{gendef}


\subsubsection*{Theorems}


\begin{theorem}{rule nullBagSubbag}[X]
  \forall B: \bag X @ \lbag \rbag \subbageq B
\end{theorem}


\begin{theorem}{rule unitBagSubbag}[X]
  \forall x: X; B: \bag X @
    \lbag x \rbag \subbageq B \iff x \inbag B
\end{theorem}


\begin{theorem}{rule subbagSelf}[X]
  \forall B: \bag X @ B \subbageq B
\end{theorem}

We need more rules about subbags, e.g., transitivity.

\newpage

\subsection{Bag scaling }\label{def-otimes}


\subsubsection*{Definitions}


\syndef{\otimes}{infun5}{"&bagscale"} \quad\verb'\otimes'


\begin{gendef}[X]
  \_ \otimes \_: \nat \cross \bag X \fun \bag X
\where
\Label{rule bcountBagScale}
  \forall n: \nat; B: \bag X; x: X @
     (n \otimes B) \bcount x = n * (B \bcount x)
\end{gendef}


\subsubsection*{Theorems}


\begin{theorem}{rule bagscaleBy0}[X]
  \forall B: \bag X @ 0 \otimes B = \lbag \rbag
\end{theorem}


\begin{theorem}{rule bagscaleBy1}[X]
  \forall B: \bag X @ 1 \otimes B = B
\end{theorem}


\begin{theorem}{rule bagscaleNull}[X]
  \forall n: \nat @ n \otimes[X] \lbag \rbag = \lbag \rbag
\end{theorem}


\begin{theorem}{rule bagscalebagscale}[X]
  \forall n, k: \nat; B: \bag X @
     n \otimes (k \otimes B) = (n * k) \otimes B
\end{theorem}


\begin{theorem}{rule domBagscale}[X]
  \forall n: \nat_1; B: \bag X @
    \dom (n \otimes B) = \dom B
\end{theorem}


\begin{theorem}{rule ranBagscale}[X]
  \forall n: \nat_1; B: \bag X @
    \ran (n \otimes B) = \ran B
\end{theorem}


\begin{theorem}{rule inbagscale}[X]
  \forall x: X; n: \nat; B: \bag X @
     x \inbag n \otimes B \iff x \inbag B \land \lnot n = 0
\end{theorem}


\begin{theorem}{rule bagscaleInBag}[X]
  \forall n: \nat; B: \bag X; Y: \power X @
     (n \otimes B) \in \bag Y \iff n = 0 \lor B \in \bag Y
\end{theorem}


\subsubsection*{Automation}

The following rules allow the computation of scaling of bags expressed by
set comprehensions.


\begin{theorem}{rule bagScaleNullset}[X]
  \forall n: \nat @ n \otimes[X] \{ \} = \{ \}
\end{theorem}


\begin{theorem}{rule bagScaleUnitSet}[X]
  \forall n, k: \nat; x: X @ n \otimes \{ (x,k)\} = \{ (x, n*k) \}
\end{theorem}


\begin{theorem}{rule bagScaleUnion}[X]
  \forall S, T: \power (X \cross \num) | (S \cup T) \in \bag X @
    n \otimes (S \cup T) = (n \otimes S) \cup (n \otimes T)
\end{theorem}

\newpage

\subsection{Bag union }\label{def-uplus}


\syndef{\uplus}{infun3}{"&bagUnion"} \quad\verb'\uplus'

Function
$\_ \uplus \_$ is predefined.



\subsubsection*{Theorems}


\begin{theorem}{rule domBagUnionFunction}[X]
  \bag X \cross \bag X \in \power A \land \bag X \in \power B
\implies 
  \dom[A,B] (\_ \uplus \_)[X] = \bag X \cross \bag X
\end{theorem}


\begin{theorem}{rule ranBagUnionFunction}[X]
  \bag X \cross \bag X \in \power A \land \bag X \in \power B
\implies   \ran[A,B] (\_ \uplus \_)[X] = \bag X
\end{theorem}


\begin{theorem}{rule domBagUnion}[X]
  \forall A, B: \bag X @ \dom (A \uplus B) = (\dom A) \cup (\dom B)
\end{theorem}


\begin{theorem}{rule inBagUnion}[X]
  \forall A, B: \bag X @
    x \inbag (A \uplus B) \iff (x \inbag A) \lor (x \inbag B)
\end{theorem}


\begin{theorem}{rule countBagUnion}[X]
  \forall A, B: \bag X; x: X @
    (A \uplus B) \bcount x = A \bcount x + B \bcount x
\end{theorem}


\begin{theorem}{rule bagUnionInBag}[X]
  \forall Y: \power X; A, B: \bag X @
    A \uplus B \in \bag Y \iff A \in \bag Y \land B \in \bag Y
\end{theorem}


\begin{theorem}{rule bagUnionNullLeft}[X]
  \forall B: \bag X @  \lbag \rbag \uplus B = B
\end{theorem}


\begin{theorem}{rule bagUnionNullRight}[X]
  \forall B: \bag X @  B \uplus \lbag \rbag = B
\end{theorem}


\begin{theorem}{rule bagUnionCommutes}[X]
  \forall A, B: \bag X @ A \uplus B = B \uplus A
\end{theorem}


\begin{theorem}{rule bagUnionAssociates}[X]
  \forall A, B, C: \bag X @ (A \uplus B) \uplus C = A \uplus (B \uplus C)
\end{theorem}


\begin{theorem}{rule bagUnionPermutes}[X]
  \forall A, B, C: \bag X @ A \uplus (B \uplus C) = B \uplus (A \uplus C)
\end{theorem}

\newpage

\subsection{Bag difference }\label{def-uminus}


\subsubsection*{Definitions}


\syndef{\uminus}{infun3}{"&bagDifference"} \quad\verb'\uminus'


\begin{gendef}[X]
  \_ \uminus \_: \bag X \cross \bag X \fun \bag X
\where
\Label{rule bcountUminus}
  \forall A, B: \bag X; x: X @
     (A \uminus B) \bcount x =max \{ 0, (A \bcount x) - (B \bcount x) \}
\end{gendef}


\subsubsection*{Theorems}


\begin{theorem}{rule inBagDifference}[X]
  \forall A, B: \bag X; x: X @
    x \inbag (A \uminus B) \iff A \bcount x > B \bcount x
\end{theorem}


\begin{theorem}{rule bagDifferenceNullLeft}[X]
  \forall B: \bag X @  \lbag \rbag \uminus B = \lbag \rbag
\end{theorem}


\begin{theorem}{rule bagDifferenceNullRight}[X]
  \forall B: \bag X @  B \uminus \lbag \rbag = B
\end{theorem}


\begin{theorem}{rule bagDifferenceSubbag}[X]
  \forall A, B, C: \bag X @
    (A \uminus B) \subbageq C \iff A \subbageq B \uplus C
\end{theorem}

\newpage

\subsection{Items }\label{def-items}


\subsubsection*{Definition}


\begin{gendef}[X]
  items: \seq X \fun \bag X
\end{gendef}


\subsubsection*{Theorems}


\begin{theorem}{rule itemsNullSeq}[X]
  items[X] \langle \rangle = \lbag \rbag
\end{theorem}


\begin{theorem}{rule itemsUnitSeq}[X]
  \forall x: X @
    items[X] \langle x \rangle = \lbag x \rbag
\end{theorem}


\begin{theorem}{rule itemsCat}[X]
  \forall s, t: \seq X @
    items (s \cat t) = (items~s) \uplus (items~t)
\end{theorem}


\begin{theorem}{rule inItems}[X]
  \forall s: \seq X @
     x \inbag (items~s) \iff x \in \ran s
\end{theorem}


\begin{theorem}{rule itemsInBag}[X]
  \forall s: \seq X; Y: \power X @
    items~s \in \bag Y \iff s \in \seq Y
\end{theorem}


\begin{theorem}{rule domItems}[X]
  \forall s: \seq X @ \dom (items~s) = \ran s
\end{theorem}


\begin[disabled]{theorem}{rule countItems}[X]
  \forall s: \seq X; x: X @ (items~s) \bcount x = \# (s \rres \{ x \})
\end{theorem}

\newpage


\bibliographystyle{plain}
\begin{thebibliography}{99}
\bibitem{Z-Std-CD}ISO SC22 Working Group 19. Z notation.
Technical report, ISO/IEC JTC1/SC22 N1970, 1995.
ISO CD 13568; Committee Draft of the proposed Z Standard.
\bibitem{Z-EVES-RM}Irwin Meisels and Mark Saaltink.
The Z/EVES 2.0 Reference Manual.
Technical Report TR-99-5493-03e, ORA Canada, October 1999.
\bibitem{Spivey-ZRM}J. M. Spivey.
{\it The Z Notation: A Reference Manual\/}.
Prentice Hall International Series in Computer Science,
2nd edition, 1992.
\end{thebibliography}
\end{document}