% Stan Warford
% Pepperdine University
% File: 220.Equations.tex
% The equation handout for Gries & Schneider, A Logical Approach to Discrete Math
% with modifications

\documentclass{amsart}
\usepackage{fontspec}
\usepackage[slantedGreek]{mathptmx}
\usepackage{amssymb,latexsym,graphics}

\setmainfont{Times}[ItalicFont    ={* Italic},
                    BoldFont      ={* Bold},
                    BoldItalicFont={* Bold Italic}]
\setsansfont{Helvetica}

\newcommand{\lgap}{2pt}                             % Line gap
\newcommand{\llgap}{6pt}                            % Larger line gap
\newcommand{\lllgap}{12pt}                          % Larger yet line gap
\newcommand{\equivs}{\ensuremath{\;\equiv\;}}       % Equivales with space
\newcommand{\equivss}{\ensuremath{\;\;\equiv\;\;}}  % Equivales with double space
\newcommand{\nequiv}{\ensuremath{\not\equiv}}       % Inequivalent
\newcommand{\impl}{\ensuremath{\Rightarrow}}        % Implies
\newcommand{\impls}{\ensuremath{\;\Rightarrow\;}}   % Implies with space
\newcommand{\nimpl}{\ensuremath{\not\Rightarrow}}   % Does not imply
\newcommand{\foll}{\ensuremath{\Leftarrow}}         % Follows from
\newcommand{\nfoll}{\ensuremath{\not\Leftarrow}}    % Does not follow from
\newcommand{\mymod}{\;\textbf{mod}\;}
\newcommand{\mygcd}{\;\textbf{gcd}\;}
\newcommand{\mylcm}{\;\textbf{lcm}\;}
\newcommand{\lbag}{\lbrace\hspace{-.2em}|\;}        % Left bag delimiter
\newcommand{\rbag}{\;|\hspace{-.2em}\rbrace}        % Right bag delimiter

% These macros are used for quantifications. Thanks to David Gries for sharing
\newcommand{\thedr}{\rule[-.25ex]{.32mm}{1.75ex}}   % Symbol that separates dummy from range in quantification
\newcommand{\dr}{\;\,\thedr\,\;}                    % Symbol that separates dummy from range, with spacing
\newcommand{\rb}{:}                                 % Symbol that separates range from body in quantification
\newcommand{\drrb}{\;\thedr\,{:}\;}                 % Symbol that separates dummy from body when range is missing
\newcommand{\all}{\forall}                          % Universal quantification
\newcommand{\ext}{\exists}                          % Existential quantification
\newcommand{\guard}{[\negthinspace ]}               % Rectangle for guard

% Macros for proof hints
\newcommand{\Gll} {\langle}                         % Open hint
\newcommand{\Ggg} {\rangle}                         % Close hint
\newlength{\Glllength}                              % Length of open hint symbol
\settowidth{\Glllength}{$.\Gll$}
\newcommand{\Hint}[1]     {\ \ \ $\Gll              \mbox{#1} \Ggg$ }   % Single line hint
\newcommand{\Hintfirst}[1]{\ \ \ $\Gll              \mbox{#1}$ }        % First line of multiline hint
\newcommand{\Hintmid}[1]  {\ \ $\hspace{\Glllength} \mbox{#1}$ }        % Middle line of multiline hint
\newcommand{\Hintlast}[1] {\ \ $\hspace{\Glllength} \mbox{#1} \Ggg$ }   % Last line of multiline hint

% Single and double quotes
\newcommand{\Lq}{\mbox{`}}
\newcommand{\Rq}{\mbox{'}}
\newcommand{\Lqq}{\mbox{``}}
\newcommand{\Rqq}{\mbox{''}}

\begin{document}
\title[Theorems from LADM]{Theorems from Gries and Schneider's LADM}
\author{J.~Stanley Warford}
\address{Natural Science Division\\
         Pepperdine University\\
         Malibu, CA 90265}
\email{Stan.Warford@pepperdine.edu}
\urladdr{https://www.cslab.pepperdine.edu/warford/}
\date{\today}
\begin{abstract}
This is a collection of the axioms and theorems in Gries and Schneider's
book \textit{A Logical Approach to Discrete Math} (LADM), Springer-Verlag, 1993.
The numbering is consistent with that text.
Additional theorems not included or numbered in LADM are indicated by a three-part
number.
This document serves as a reference for homework exercises and taking exams.
\end{abstract}

\maketitle

\section*{Table of Precedences}
\begin{tabbing}
(m)\;\=\hspace{14pc}\=\kill
(a)\>$[x := e]$ (textual substitution) \>(highest precedence)\\
(b)\>. (function application)\\
(c)\>unary prefix operators: $+$\quad $-$\quad $\neg$\quad $\#$\quad $\thicksim$\quad $\mathcal{P}$\\
(d)\>$**$\\
(e)\>$\cdot$\quad $/$\quad $\div$\quad \textbf{mod}\quad \textbf{gcd}\\
(f)\>$+$\quad $-$\quad $\cup$\quad $\cap$\quad $\times$\quad $\circ$\quad $\bullet$\\
(g)\>$\downarrow$\quad $\uparrow$\\
(h)\>$\#$\\
(i)\>$\triangleleft$\quad $\triangleright$\quad \textasciicircum\\
(j)\>$=$\quad $<$\quad $>$\quad $\in$\quad $\subset$\quad $\subseteq$\quad $\supset$\quad $\supseteq$\quad $\mid$ \>(conjunctional)\\
(k)\>$\lor$\quad $\land$\\
(l)\>$\impl$\quad $\foll$\\
(m)\>$\equiv$ \>(lowest precedence)\\
\end{tabbing}
\par
All nonassociative binary infix operators associate from left to right except $**$, $\triangleleft$, and $\impl$,
which associate from right to left.

\textbf{Definition of} $/$: The operators on lines (j), (l), and (m) may have a slash $/$ through them to denote negation---e.g.
$x\notin T$ is an abbreviation for $\neg(x \in T)$.

\section*{Some Basic Types}
\begin{tabbing}
$positive reals$\quad\quad\= Symbol\quad\quad\=\kill
Name                \>Symbol           \> Type (set of values)\\[-8pt]
\rule{5in}{0.5pt}\\
$integer$           \>$\mathbb{Z}$     \> integers: $\ldots , -3, -2, -1, 0, 1, 2, 3, \ldots$\\[\lgap]
$nat$               \>$\mathbb{N}$     \> natural numbers: $0, 1, 2, \ldots$\\[\lgap]
$positive$          \>$\mathbb{Z}^{+}$ \> positive integers: $1, 2, 3, \ldots$\\[\lgap]
$negative$          \>$\mathbb{Z}^{-}$ \> negative integers: $-1, -2, -3, \ldots$\\[\lgap]
$rational$          \>$\mathbb{Q}$     \> rational numbers: $i/j$ for $i,j$ integers, $j\ne 0$\\[\lgap]
$reals$             \>$\mathbb{R}$     \> real numbers\\[\lgap]
$positive$ $reals$  \>$\mathbb{R}^{+}$ \> positive real numbers\\[\lgap]
$bool$              \>$\mathbb{B}$     \> booleans: $true, false$
\end{tabbing}

\section*{Theorems of the Propositional Calculus}

\subsection*{Equivalence and $true$}
\begin{tabbing}
(99.99.9)\;\=\kill
(3.1)\>\textbf{Axiom, Associativity of $\equiv$ :}\quad $((p\equiv q) \equiv r)\equivs (p\equiv (q\equiv r))$\\[\lgap]
(3.2)\>\textbf{Axiom, Symmetry of $\equiv$ :}\quad $p\equiv q \equiv q\equiv p$\\[\lgap]
(3.3)\>\textbf{Axiom, Identity of $\equiv$ :}\quad $true\equiv q \equiv q$\\[\lgap]
(3.4)\>$true$\\[\lgap]
(3.5)\>\textbf{Reflexivity of $\equiv$ :}\quad $p\equiv p$\\
\end{tabbing}

\subsection*{Negation, inequivalence, and $false$}
\begin{tabbing}
(99.99.9)\;\=\kill
(3.8)\>\textbf{Definition of $false$ :}\quad $false\equiv \neg true$\\[\lgap]
(3.9)\>\textbf{Axiom, Distributivity of $\neg$ over $\equiv$ :}\quad $\neg (p\equiv q) \equivs \neg p \equiv q$\\[\lgap]
(3.10)\>\textbf{Definition of $\nequiv$ :}\quad $(p\nequiv q)\equivs\neg(p\equiv q)$\\[\lgap]
(3.11)\>$\neg p \equiv q \equiv p \equiv \neg q$\\[\lgap]
(3.12)\>\textbf{Double negation:}\quad $\neg\neg p\equiv p$\\[\lgap]
(3.13)\>\textbf{Negation of $false$:}\quad $\neg false\equiv true$\\[\lgap]
(3.14)\>$(p\nequiv q)\equivs\neg p\equiv q$\\[\lgap]
(3.15)\>$\neg p\equiv p\equiv false$\\[\lgap]
(3.16)\>\textbf{Symmetry of $\nequiv$ :}\quad $(p\nequiv q) \equivs (q\nequiv p)$\\[\lgap]
(3.17)\>\textbf{Associativity of $\nequiv$ :}\quad $((p\nequiv q) \nequiv r)\equivs (p\nequiv (q\nequiv r))$\\[\lgap]
(3.18)\>\textbf{Mutual associativity:}\quad $((p\nequiv q) \equiv r)\equivs (p\nequiv (q\equiv r))$\\[\lgap]
(3.19)\>\textbf{Mutual interchangeability:}\quad $p\nequiv q \equiv r\equivss p\equiv q\nequiv r$\\
(3.19.1)\>$p\nequiv p \nequiv q\equivs q$\\
\end{tabbing}

\subsection*{Disjunction}
\begin{tabbing}
(99.99.9)\;\=\kill
(3.24)\>\textbf{Axiom, Symmetry of $\lor$ :}\quad $p\lor q \equiv q\lor p$\\[\lgap]
(3.25)\>\textbf{Axiom, Associativity of $\lor$ :}\quad $(p\lor q) \lor r\equiv p\lor (q\lor r)$\\[\lgap]
(3.26)\>\textbf{Axiom, Idempotency of $\lor$ :}\quad $p\lor p \equiv p$\\[\lgap]
(3.27)\>\textbf{Axiom, Distributivity of $\lor$ over $\equiv$ :}\quad $p\lor (q\equiv r)\equiv p\lor q\equiv p\lor r$\\[\lgap]
(3.28)\>\textbf{Axiom, Excluded middle:}\quad $p\lor\neg p$\\[\lgap]
(3.29)\>\textbf{Zero of $\lor$ :}\quad $p\lor true\equiv true$\\[\lgap]
(3.30)\>\textbf{Identity of $\lor$ :}\quad $p\lor false\equiv p$\\[\lgap]
(3.31)\>\textbf{Distributivity of $\lor$ over $\lor$ :}\quad $p\lor (q\lor r)\equiv (p\lor q)\lor (p\lor r)$\\[\lgap]
(3.32)\>$p\lor q\equiv p\lor\neg q\equiv p$\\
\end{tabbing}

%\newpage

\subsection*{Conjunction}
\begin{tabbing}
(99.99.9)\;\=(m)\;\=\kill
(3.35)\>\textbf{Axiom, Golden rule:}\quad $p\land q\equivs p\equivs q\equivs p\lor q$\\[\lgap]
(3.36)\>\textbf{Symmetry of $\land$ :}\quad $p\land q \equiv q\land p$\\[\lgap]
(3.37)\>\textbf{Associativity of $\land$ :}\quad $(p\land q) \land r\equiv p\land (q\land r)$\\[\lgap]
(3.38)\>\textbf{Idempotency of $\land$ :}\quad  $p\land p \equiv p$\\[\lgap]
(3.39)\>\textbf{Identity of $\land$ :}\quad $p\land true\equiv p$\\[\lgap]
(3.40)\>\textbf{Zero of $\land$ :}\quad $p\land false\equiv false$\\[\lgap]
(3.41)\>\textbf{Distributivity of $\land$ over $\land$ :}\quad $p\land (q\land r)\equiv (p\land q)\land (p\land r)$\\[\lgap]
(3.42)\>\textbf{Contradiction:}\quad $p \land \neg p \equiv false$\\[\lgap]
(3.43)\>\textbf{Absorption:}\\
      \> (a)\> $p \land (p \lor q) \equiv p$\\[\lgap]
      \> (b)\> $p \lor (p \land q) \equiv p$\\[\lgap]
(3.44)\>\textbf{Absorption:}\\
      \> (a)\> $p \land (\neg p \lor q) \equiv p \land q$\\[\lgap]
      \> (b)\> $p \lor (\neg p \land q) \equiv p \lor q$\\[\lgap]
(3.45)\>\textbf{Distributivity of $\lor$ over $\land$ :}\quad $p\lor (q\land r)\equiv (p\lor q)\land (p\lor r)$\\[\lgap]
(3.46)\>\textbf{Distributivity of $\land$ over $\lor$ :}\quad $p\land (q\lor r)\equiv (p\land q)\lor (p\land r)$\\[\lgap]
(3.46.1)\>\textbf{Consensus:}\quad $(p \land q) \lor (\neg p \land r) \lor (q \land r) \equiv (p \land q) \lor (\neg p \land r)$\\[\lgap]
(3.47)\>\textbf{De Morgan:}\\
      \> (a)\> $\neg (p \land q) \equiv \neg p \lor \neg q$\\[\lgap]
      \> (b)\> $\neg (p \lor q) \equiv \neg p \land \neg q$\\[\lgap]
(3.48)\>$p\land q\equivs p\land \neg q\equivs \neg p$\\[\lgap]
(3.49)\>$p\land (q\equiv r)\equivs p\land q\equivs p\land r \equivs p$\\[\lgap]
(3.50)\>$p\land (q\equiv p)\equivs p\land q$\\[\lgap]
(3.51)\>\textbf{Replacement:}\quad $(p \equiv q) \land (r \equiv p) \equivss (p \equiv q) \land (r \equiv q)$\\[\lgap]
(3.52)\>\textbf{Equivalence:}\quad $p \equiv q \equivs (p \land q) \lor (\neg p \land \neg q)$\\[\lgap]
(3.53)\>\textbf{Exclusive or:}\quad $p \nequiv q \equivs (\neg p \land q) \lor (p \land \neg q)$\\[\lgap]
(3.55)\>$(p\land q)\land r \equivs p \equivs q \equivs r \equivs p\lor q \equivs q\lor r \equivs r\lor p \equivs p \lor q\lor r$\\
\end{tabbing}

%\newpage

\subsection*{Implication}
\begin{tabbing}
(99.99.9)\;\=(m)\;\=\kill
(3.57)\>\textbf{Definition of Implication:}\quad $p\impl q \equivs p\lor q \equivs q$\\[\lgap]
(3.58)\>\textbf{Axiom, Consequence:}\quad $p\foll q \equivs q\impl p$\\[\lgap]
(3.59)\>\textbf{Implication:}\quad $p\impl q \equivs \neg p \lor q$\\[\lgap]
(3.60)\>\textbf{Implication:}\quad $p\impl q \equivs p\land q \equivs p$\\[\lgap]
(3.61)\>\textbf{Contrapositive:}\quad $p\impl q \equivs \neg q\impl \neg p$\\[\lgap]
(3.62)\>$p\impl (q\equiv r) \equivs p\land q\equivs p\land r$\\[\lgap]
(3.63)\>\textbf{Distributivity of $\impl$ over $\equiv$ :}\quad $p\impl (q\equiv r)\equivs (p\impl q)\equivs (p\impl r)$\\[\lgap]
(3.63.1)\>\textbf{Distributivity of $\impl$ over $\land$ :}\quad $p\impl q\land r\equivs (p\impl q)\land (p\impl r)$\\[\lgap]
(3.63.2)\>\textbf{Distributivity of $\impl$ over $\lor$ :}\quad $p\impl q\lor r\equivs (p\impl q)\lor (p\impl r)$\\[\lgap]
(3.64)\>$p\impl (q\impl r) \equivs (p\impl q)\impl (p\impl r)$\\[\lgap]
(3.65)\>\textbf{Shunting:}\quad $p\land q\impl r\equivs p\impl (q\impl r)$\\[\lgap]
(3.66)\>$p\land (p\impl q) \equivs p\land q$\\[\lgap]
(3.67)\>$p\land (q\impl p) \equivs p$\\[\lgap]
(3.68)\>$p\lor (p\impl q) \equivs true$\\[\lgap]
(3.69)\>$p\lor (q\impl p) \equivs q\impl p$\\[\lgap]
(3.70)\>$p\lor q \impl p\land q \equivs p \equivs q$\\[\lgap]
(3.71)\>\textbf{Reflexivity of $\impl$ :}\quad $p\impl p$\\[\lgap]
(3.72)\>\textbf{Right zero of $\impl$ :}\quad $p\impl true \equivs true$\\[\lgap]
(3.73)\>\textbf{Left identity of $\impl$ :}\quad $true\impl p \equivs p$\\[\lgap]
(3.74)\>$p\impl false \equivs \neg p$\\[\lgap]
(3.74.1)\>$\neg p\impl false \equivs p$\\[\lgap]
(3.74.2)\>$p\impl \neg p \equivs \neg p$\\[\lgap]
(3.75)\>$false\impl p \equivs true$\\[\lgap]
(3.76)\>\textbf{Weakening/strengthening:}\\
      \> (a)\> $p\impl p\lor q$\quad \quad \quad (Weakening the consequent)\\[\lgap]
      \> (b)\> $p\land q \impl p$\quad \quad \quad (Strengthening the antecedent)\\[\lgap]
      \> (c)\> $p\land q \impl p\lor q$\quad \quad \quad (Weakening/strengthening)\\[\lgap]
      \> (d)\> $p\lor (q\land r) \impl p\lor q$\\[\lgap]
      \> (e)\> $p\land q \impl p\land (q \lor r)$\\[\lgap]
(3.76.1)\>$p\land q \impl p\lor r$\quad \quad \quad (Weakening/strengthening)\\[\lgap]
(3.76.2)\>$(p\impl q) \impl ((q\impl r)\impl (p\impl r))$\\[\lgap]
(3.77)\>\textbf{Modus ponens:}\quad $p\land (p\impl q)\impl q$\\[\lgap]
(3.77.1)\>\textbf{Modus tollens:}\quad $(p\impl q)\land \neg q \impl \neg p$\\[\lgap]
(3.78)\>$(p\impl r) \land (q\impl r) \equivs p\lor q\impl r$\\[\lgap]
(3.78.1)\>$(p\impl r)\lor (q\impl r) \equivs p\land q\impl r$\\[\lgap]
(3.79)\>$(p\impl r) \land (\neg p\impl r) \equivs r$\\[\lgap]
(3.80)\>\textbf{Mutual implication:}\quad $(p\impl q) \land (q\impl p) \equivs (p\equiv q)$\\[\lgap]
(3.81)\>\textbf{Antisymmetry:}\quad $(p\impl q) \land (q\impl p) \impl (p\equiv q)$\\[\lgap]
(3.82)\>\textbf{Transitivity:}\\
      \> (a)\> $(p\impl q) \land (q\impl r) \impl (p\impl r)$\\[\lgap]
      \> (b)\> $(p\equiv q) \land (q\impl r) \impl (p\impl r)$\\[\lgap]
      \> (c)\> $(p\impl q) \land (q\equiv r) \impl (p\impl r)$\\[\lgap]
(3.82.1)\>\textbf{Transitivity of $\equiv$ :}\quad $(p\equiv q)\land (q\equiv r)\impl (p\equiv r)$\\[\lgap]
(3.82.2)\>$(p\equiv q)\impl (p\impl q)$
\end{tabbing}

\subsection*{Leibniz as an axiom}
\begin{tabbing}
(99.99.9)\;\=(m)\;\=\kill
This section uses the following notation: $E^{z}_{X}$ means $E[z := X]$.\\[\lgap]
(3.83)\>\textbf{Axiom, Leibniz:}\quad $e=f\impl E^{z}_{e} = E^{z}_{f}$\\[\lgap]
(3.84)\>\textbf{Substitution:}\\
      \> (a)\> $(e=f) \land E^{z}_{e} \equivs (e=f)\land E^{z}_{f}$\\[\lgap]
      \> (b)\> $(e=f) \impl E^{z}_{e} \equivs (e=f)\impl E^{z}_{f}$\\[\lgap]
      \> (c)\> $q\land (e=f) \impl E^{z}_{e} \equivs q\land (e=f)\impl E^{z}_{f}$\\[\lgap]
(3.85)\>\textbf{Replace by $true$:}\\
      \> (a)\> $p \impl E^{z}_{p} \equivs p\impl E^{z}_{true}$\\[\lgap]
      \> (b)\> $q\land p \impl E^{z}_{p} \equivs q\land p\impl E^{z}_{true}$\\[\lgap]
(3.86)\>\textbf{Replace by $false$:}\\
      \> (a)\> $E^{z}_{p} \impl p \equivs E^{z}_{false}\impl p$\\[\lgap]
      \> (b)\> $E^{z}_{p} \impl p\lor q \equivs E^{z}_{false}\impl p\lor q$\\[\lgap]
(3.87)\>\textbf{Replace by $true$:}\quad $p\land E^{z}_{p} \equivs p\land E^{z}_{true}$\\
(3.88)\>\textbf{Replace by $false$:}\quad $p\lor E^{z}_{p} \equivs p\lor E^{z}_{false}$\\
(3.89)\>\textbf{Shannon:}\quad $E^{z}_{p}\equivs (p\land E^{z}_{true}) \lor (\neg p\land E^{z}_{false})$\\
(3.89.1)\>$E^{z}_{true}\land E^{z}_{false} \impl E^{z}_{p}$
\end{tabbing}

\subsection*{Additional theorems concerning implication}
\begin{tabbing}
(99.99.9)\;\=(m)\;\=\kill
(4.1)\>$p\impl (q\impl p)$\\[\lgap]
(4.2)\>\textbf{Monotonicity of $\lor$ :}\quad $(p\impl q) \impl (p\lor r \impl q\lor r)$\\[\lgap]
(4.3)\>\textbf{Monotonicity of $\land$ :}\quad $(p\impl q) \impl (p\land r \impl q\land r)$\\[\lgap]
\end{tabbing}

\subsection*{Proof technique metatheorems.}
\begin{tabbing}
(99.99.9)\;\=(m)\;\=\kill
(4.4)\>\textbf{Deduction (assume conjuncts of antecedent):}\\[\lgap]
      \>To prove $P_{1}\land P_{2}\impl Q$, assume $P_{1}$ and $P_{2}$, and prove $Q$.\\[\lgap]
      \>You cannot use textual substitution in $P_{1}$ or $P_{2}$.\\[\lgap]
(4.5)\>\textbf{Case analysis:}\quad If $E^{z}_{true}$ and $E^{z}_{false}$ are theorems, then so is $E^{z}_{P}$.\\[\lgap]
(4.6)\>\textbf{Case analysis:}\quad $(p\lor q\lor r)\land (p\impl s)\land (q\impl s)\land (r\impl s)\impl s$\\[\lgap]
(4.7)\>\textbf{Mutual implication:}\quad To prove $P\equiv Q$, prove $P\impl Q$ and $Q\impl P$.\\[\lgap]
(4.7.1)\>\textbf{Truth implication:}\quad To prove $P$, prove $true\impl P$.\\[\lgap]
(4.9)\>\textbf{Proof by contradiction:}\quad To prove $P$, prove $\neg P\impl false$.\\[\lgap]
(4.9.1)\>\textbf{Proof by contradiction:}\quad To prove $P$, prove $\neg P\equiv false$.\\[\lgap]
(4.12)\>\textbf{Proof by contrapositive:}\quad To prove $P\impl Q$, prove $\neg Q\impl \neg P$.\\[\lgap]
\end{tabbing}

\section*{General Laws of Quantification}
\begin{tabbing}
(99.99.9)\;\=(m)\;\=\kill
For symmetric and associative binary operator $\star$ with identity $u$.\\[\lgap]
(8.13)\>\textbf{Axiom, Empty range:}\quad $(\star x \dr false \rb P) =u$\\[\lgap]
(8.14)\>\textbf{Axiom, One-point rule:}\quad Provided $\neg occurs(\Lq x\Rq ,\Lq E\Rq)$,\\[\lgap]
      \>$(\star x\dr x=E\rb P) = P[x:=E]$\\[\lgap]
(8.15)\>\textbf{Axiom, Distributivity:}\quad Provided $P,Q:\mathbb{B}$ or $R$ is finite,\\[\lgap]
      \>$(\star x\dr R\rb P)\star (\star x\dr R\rb Q) = (\star x\dr R\rb P\star Q)$\\[\lgap]
(8.16)\>\textbf{Axiom, Range split:}\quad Provided $R\land S\equiv false$ and $P:\mathbb{B}$ or $R$ and $S$ are finite,\\[\lgap]
      \>$(\star x\dr R\lor S\rb P) = (\star x\dr R\rb P)\star (\star x\dr S\rb P)$\\[\lgap]
(8.17)\>\textbf{Axiom, Range split:}\quad Provided $P:\mathbb{B}$ or $R$ and $S$ are finite,\\[\lgap]
      \>$(\star x\dr R\lor S\rb P)\star (\star x\dr R\land S\rb P) = (\star x\dr R\rb P)\star (\star x\dr S\rb P)$\\[\lgap]
(8.18)\>\textbf{Axiom, Range split for idempotent $\star$ :}\quad Provided $P:\mathbb {B}$ or $R$ and $S$ are finite,\\[\lgap]
      \>$(\star x\dr R\lor S\rb P) = (\star x\dr R\rb P)\star (\star x\dr S\rb P)$\\[\lgap]
(8.19)\>\textbf{Axiom, Interchange of dummies:}\quad Provided $\star$ is idempotent or $R$ and $Q$ are finite,\\[\lgap]
      \>$\neg occurs(\Lq y\Rq ,\Lq R\Rq)$, $\neg occurs(\Lq x\Rq ,\Lq Q\Rq)$,\\[\lgap]
      \>$(\star x\dr R\rb (\star y\dr Q\rb P)) = (\star y\dr Q\rb (\star x\dr R\rb P))$\\[\lgap]
(8.20)\>\textbf{Axiom, nesting:}\quad Provided $\neg occurs(\Lq y\Rq ,\Lq R\Rq)$,\\[\lgap]
      \>$(\star x,y\dr R\land Q\rb P) = (\star x\dr R\rb (\star y\dr Q\rb P))$\\[\lgap]
(8.21)\>\textbf{Axiom, Dummy renaming:}\quad Provided $\neg occurs(\Lq y\Rq ,\Lq R, P\Rq)$,\\[\lgap]
      \>$(\star x\dr R\rb P) = (\star y\dr R[x:=y]\rb P[x:=y])$\\[\lgap]
(8.22)\>\textbf{Change of dummy:}\quad Provided $\neg occurs(\Lq y\Rq ,\Lq R, P\Rq)$, and $f$ has an inverse,\\[\lgap]
      \>$(\star x\dr R\rb P) = (\star y\dr R[x:=f.y]\rb P[x:=f.y])$\\[\lgap]
\end{tabbing}

\newpage

\begin{tabbing}
(99.99.9)\;\=(m)\;\=\kill
(8.23)\>\textbf{Split off term:}\quad For $n$: $\mathbb{N}$,\\[\lgap]
      \> (a)\> $(\star i\dr 0\le i < n+1\rb P) = (\star i\dr 0\le i < n\rb P)\star P[i:=n]$\\[\lgap]
      \> (b)\> $(\star i\dr 0\le i < n+1\rb P) = P[i:=0]\star (\star i\dr 0< i < n+1\rb P)$\\[\lgap]
\end{tabbing}

\section*{Theorems of the Predicate Calculus}

\subsection*{Universal quantification}
\begin{tabbing}
(99.99.9)\;\=(m)\;\=\kill
Notation: $(\star x\drrb P)$ means $(\star x\dr true\rb P)$.\\[\lgap]
(9.2)\>\textbf{Axiom, Trading:}\quad $(\all x\dr R\rb P)\equiv (\all x\drrb R\impl P)$\\[\lgap]
(9.3)\>\textbf{Trading:}\\[\lgap]
      \> (a)\> $(\all x\dr R\rb P)\equiv (\all x\drrb \neg R\lor P)$\\[\lgap]
      \> (b)\> $(\all x\dr R\rb P)\equiv (\all x\drrb R\land P\equiv R)$\\[\lgap]
      \> (c)\> $(\all x\dr R\rb P)\equiv (\all x\drrb R\lor P\equiv P)$\\[\lgap]
(9.4)\>\textbf{Trading:}\\[\lgap]
      \> (a)\> $(\all x\dr Q\land R\rb P)\equiv (\all x\dr Q\rb R\impl P)$\\[\lgap]
      \> (b)\> $(\all x\dr Q\land R\rb P)\equiv (\all x\dr Q\rb \neg R\lor P)$\\[\lgap]
      \> (c)\> $(\all x\dr Q\land R\rb P)\equiv (\all x\dr Q\rb R\land P\equiv R)$\\[\lgap]
      \> (d)\> $(\all x\dr Q\land R\rb P)\equiv (\all x\dr Q\rb R\lor P\equiv P)$\\[\lgap]
(9.4.1)\>\textbf{Universal double trading:} \quad $(\all x\dr R\rb P)\equiv (\all x\dr \neg P \rb \neg R)$\\[\lgap]
(9.5)\>\textbf{Axiom, Distributivity of $\lor$ over $\all$ :}\quad Provided $\neg occurs(\Lq x\Rq ,\Lq P\Rq)$,\\[\lgap]
      \>$P\lor (\all x\dr R\rb Q)\equiv (\all x\dr R\rb P\lor Q)$\\[\lgap]
(9.6)\>Provided $\neg occurs(\Lq x\Rq ,\Lq P\Rq)$, \quad $(\all x\dr R\rb P)\equiv P\lor (\all x\drrb \neg R)$\\[\lgap]
(9.7)\>\textbf{Distributivity of $\land$ over $\all$ :}\quad Provided $\neg occurs(\Lq x\Rq ,\Lq P\Rq)$,\\[\lgap]
      \>$\neg (\all x\drrb \neg R)\impl ((\all x\dr R\rb P\land Q)\equiv P\land (\all x\dr R\rb Q))$\\[\lgap]
(9.8)\>$(\all x\dr R\rb true)\equiv true$\\[\lgap]
(9.9)\>$(\all x\dr R\rb P\equiv Q)\impl ((\all x\dr R\rb P)\equiv (\all x\dr R\rb Q))$\\[\lgap]
(9.10)\>\textbf{Range weakening/strengthening:}\quad $(\all x\dr Q\lor R\rb P)\impl (\all x\dr Q\rb P)$\\[\lgap]
(9.11)\>\textbf{Body weakening/strengthening:}\quad $(\all x\dr R\rb P\land Q)\impl (\all x\dr R\rb P)$\\[\lgap]
(9.12)\>\textbf{Monotonicity of $\all$ :}\quad $(\all x\dr R\rb Q\impl P)\impl ((\all x\dr R\rb Q)\impl (\all x\dr R\rb P))$\\[\lgap]
(9.13)\>\textbf{Instantiation:}\quad $(\all x\drrb P)\impl P[x:=E]$\\[\lgap]
(9.16)\>\textbf{Metatheorem:}\quad $P$ is a theorem iff $(\all x\drrb P)$ is a theorem.\\[\lgap]
\end{tabbing}

\subsection*{Existential quantification}
\begin{tabbing}
(99.99.9)\;\=(m)\;\=\kill
(9.17)\>\textbf{Axiom, Generalized De Morgan:}\quad $(\ext x\dr R\rb P)\equiv \neg (\all x\dr R\rb \neg P)$\\[\lgap]
(9.18)\>\textbf{Generalized De Morgan:}\\[\lgap]
      \> (a)\> $\neg (\ext x\dr R\rb \neg P)\equiv (\all x\dr R\rb P)$\\[\lgap]
      \> (b)\> $\neg (\ext x\dr R\rb P)\equiv (\all x\dr R\rb \neg P)$\\[\lgap]
      \> (c)\> $(\ext x\dr R\rb \neg P)\equiv \neg (\all x\dr R\rb P)$\\[\lgap]
(9.19)\>\textbf{Trading:}\quad $(\ext x\dr R\rb P)\equiv (\ext x\drrb R\land P)$\\[\lgap]
(9.20)\>\textbf{Trading:}\quad $(\ext x\dr Q\land R\rb P)\equiv (\ext x\dr Q\rb R\land P)$\\[\lgap]
(9.20.1)\>\textbf{Existential double trading:} \quad $(\ext x\dr R\rb P)\equiv (\ext x\dr P \rb R)$\\[\lgap]
(9.20.2)\>$(\ext x \drrb R) \impl ((\all x\dr R\rb P)\impl (\ext x\dr R \rb P))$\\[\lgap]
(9.21)\>\textbf{Distributivity of $\land$ over $\ext$ :}\quad Provided $\neg occurs(\Lq x\Rq ,\Lq P\Rq)$,\\[\lgap]
      \>$P\land (\ext x\dr R\rb Q)\equiv (\ext x\dr R\rb P\land Q)$\\[\lgap]
(9.22)\>Provided $\neg occurs(\Lq x\Rq ,\Lq P\Rq)$, \quad $(\ext x\dr R\rb P)\equiv P\land (\ext x\drrb R)$\\[\lgap]
(9.23)\>\textbf{Distributivity of $\lor$ over $\ext$ :}\quad Provided $\neg occurs(\Lq x\Rq ,\Lq P\Rq)$,\\[\lgap]
      \>$(\ext x\drrb R)\impl ((\ext x\dr R\rb P\lor Q)\equiv P\lor (\ext x\dr R\rb Q))$\\[\lgap]
(9.24)\>$(\ext x\dr R\rb false)\equiv false$\\[\lgap]
(9.25)\>\textbf{Range weakening/strengthening:}\quad $(\ext x\dr R\rb P)\impl (\ext x\dr Q\lor R\rb P)$\\[\lgap]
(9.26)\>\textbf{Body weakening/strengthening:}\quad $(\ext x\dr R\rb P)\impl (\ext x\dr R\rb P\lor Q)$\\[\lgap]
(9.26.1)\>\textbf{Body weakening/strengthening:}\quad $(\ext x\dr R\rb P\land Q)\impl (\ext x\dr R\rb P)$\\[\lgap]
(9.27)\>\textbf{Monotonicity of $\ext$ :}\quad $(\all x\dr R\rb Q\impl P)\impl ((\ext x\dr R\rb Q)\impl (\ext x\dr R\rb P))$\\[\lgap]
(9.28)\>\textbf{$\ext$-Introduction:}\quad $P[x:=E]\impl (\ext x\drrb P)$\\[\lgap]
(9.29)\>\textbf{Interchange of quantification:}\quad Provided $\neg occurs(\Lq y\Rq ,\Lq R\Rq)$ and $\neg occurs(\Lq x\Rq ,\Lq Q\Rq)$,\\[\lgap]
      \>$(\ext x\dr R\rb (\all y\dr Q\rb P))\impl (\all y\dr Q\rb (\ext x\dr R\rb P))$\\[\lgap]
(9.30)\>Provided $\neg occurs(\Lq \hat{x}\Rq ,\Lq Q\Rq)$,\\[\lgap]
      \>$(\ext x\dr R\rb P)\impl Q$ is a theorem iff $(R\land P)[x:=\hat{x}]\impl Q$ is a theorem.\\[\lgap]
\end{tabbing}

\section*{A Theory of Sets}
\begin{tabbing}
(99.99.9)\;\=(m)\;\=\kill
(11.2)\>\textbf{Axiom, Enumeration:}\quad $\{e_{0}, e_{1},\ldots ,e_{n-1}\} = \{ x\dr x=e_{0}\lor x=e_{1}\lor \cdots \lor x=e_{n-1}\rb x \}$\\[\lgap]
(11.3)\>\textbf{Axiom, Set membership:}\quad Provided $\neg occurs(\Lq x\Rq ,\Lq F\Rq)$,\\[\lgap]
      \>$F\in \{x\dr R\rb E\}\equiv (\ext x\dr R\rb F=E)$\\[\lgap]
(11.4)\>\textbf{Axiom, Extensionality:}\quad $S=T\equivss (\all x\drrb x\in S\equivs x\in T)$\\[\lgap]
(11.4.1)\>\textbf{Axiom, Empty set:}\quad $\emptyset = \{x\dr false\rb E\}$\\
(11.4.2)\>$e\in \emptyset\equivs false$\\
(11.4.3)\>\textbf{Axiom, Universe:}\quad $\mathbf{U}=\{x\drrb x\},\quad \mathbf{U}$: $set(t) =\{x$: $t\drrb x\}$\\
(11.4.4)\>$e\in \mathbf{U}\equivs true$,\quad for $e$: $t$ and $\mathbf{U}$: $set(t)$\\
(11.5)\>$S=\{x\dr x\in S\rb x\}$\\[\lgap]
(11.5.1)\>\textbf{Axiom, Abbreviation:}\quad For $x$ a single variable, $\{x\dr R\} = \{x\dr R\rb x\}$\\
(11.6)\>Provided $\neg occurs(\Lq y\Rq ,\Lq R\Rq)$ and $\neg occurs(\Lq y\Rq ,\Lq E\Rq)$,\\[\lgap]
      \>$\{x\dr R\rb E\} = \{y\dr (\ext x\dr R\rb y=E)\}$\\[\lgap]
(11.7)\>$x\in \{x\dr R\} \equivs R$\\[\lgap]
      \>$R$ is the characteristic predicate of the set.\\[\lgap]
(11.7.1)\>$y\in \{x\dr R\} \equivs R[x:=y]$ for any expression $y$\\[\lgap]
(11.9)\>$\{x\dr Q\} = \{x\dr R\} \equivs (\all x\drrb Q\equiv R)$\\[\lgap]
(11.10)\>$\{x\dr Q\} = \{x\dr R\}$ is valid iff $Q\equiv R$ is valid.\\[\lgap]
(11.11)\>\textbf{Methods for proving set equality } $S=T$ \textbf{:}\\[\lgap]
       \> (a)\> Use Leibniz directly.\\[\lgap]
       \> (b)\> Use axiom Extensionality (11.4) and prove the (9.8) Lemma\\
       \>    \> $v\in S\equivs v\in T$ for an arbitrary value $v$.\\[\lgap]
       \> (c)\> Prove $Q\equiv R$ and conclude $\{x\dr Q\} = \{x\dr R\}$.\\[\lgap]
\end{tabbing}

\newpage

\subsection*{Operations on sets}
\begin{tabbing}
(99.99.9)\;\=(m)\;\=\kill
(11.12)\>\textbf{Axiom, Size:}\quad $\#S = (\upSigma x\dr x\in S\rb 1)$\\[\lgap]
(11.13)\>\textbf{Axiom, Subset:}\quad $S\subseteq T \equiv (\all x\dr x\in S\rb x\in T)$\\[\lgap]
(11.14)\>\textbf{Axiom, Proper subset:}\quad $S\subset T \equivs S\subseteq T\land S\ne T$\\[\lgap]
(11.15)\>\textbf{Axiom, Superset:}\quad $T\supseteq S \equivs S\subseteq T$\\[\lgap]
(11.16)\>\textbf{Axiom, Proper superset:}\quad $T\supset S \equivs S\subset T$\\[\lgap]
(11.17)\>\textbf{Axiom, Complement:}\quad $v\in \sim S \equivs v\in \mathbf{U} \land v\notin S$\\[\lgap]
(11.18)\>$v\in \sim S \equivs v\notin S$,\quad for $v$ in $\mathbf{U}$\\[\lgap]
(11.19)\>$\sim \sim S = S$\\[\lgap]
(11.20)\>\textbf{Axiom, Union:}\quad $v\in S \cup T\equivs v\in S\lor v\in T$\\[\lgap]
(11.21)\>\textbf{Axiom, Intersection:}\quad $v\in S \cap T\equivs v\in S\land v\in T$\\[\lgap]
(11.22)\>\textbf{Axiom, Difference:}\quad $v\in S - T\equivs v\in S\land v\notin T$\\[\lgap]
(11.23)\>\textbf{Axiom, Power set:}\quad $v\in \mathcal{P}S\equivs v\subseteq S$\\[\lgap]
(11.24)\>\textbf{Definition. } Let $E_{s}$ be a set expression constructed from set variables, $\emptyset$, $\mathbf{U}$, $\sim$, $\cup$, and $\cap$.\\[\lgap]
       \>Then $E_{p}$ is the expression constructed from $E_{s}$ by replacing:\\[\lgap]
       \>$\emptyset$ with $false$, \quad $\mathbf{U}$ with $true$, \quad $\cup$ with $\lor$, \quad $\cap$ with $\land$, \quad $\sim$ with $\neg$.\\[\lgap]
       \>The construction is reversible: $E_{s}$ can be constructed from $E_{p}$.\\[\lgap]
(11.25)\>\textbf{Metatheorem. } For any set expressions $E_{s}$ and $F_{s}$:\\[\lgap]
       \>(a)\> $E_{s} = F_{s}$ is valid iff $E_{p} \equiv F_{p}$ is valid,\\[\lgap]
       \>(b)\> $E_{s} \subseteq F_{s}$ is valid iff $E_{p} \impl F_{p}$ is valid,\\[\lgap]
       \>(c)\> $E_{s} = \mathbf{U}$ is valid iff $E_{p}$ is valid.\\[\lgap]
\end{tabbing}

\subsection*{Basic properties of $\cup$}
\begin{tabbing}
(99.99.9)\;\=(m)\;\=\kill
(11.26)\>\textbf{Symmetry of $\cup$ :}\quad $S\cup T = T\cup S$\\[\lgap]
(11.27)\>\textbf{Associativity of $\cup$ :}\quad $(S\cup T)\cup U = S\cup (T\cup U)$\\[\lgap]
(11.28)\>\textbf{Idempotency of $\cup$ :}\quad $S\cup S = S$\\[\lgap]
(11.29)\>\textbf{Zero of $\cup$ :}\quad $S\cup \mathbf{U} = \mathbf{U}$\\[\lgap]
(11.30)\>\textbf{Identity of $\cup$ :}\quad $S\cup \emptyset = S$\\[\lgap]
(11.31)\>\textbf{Weakening:}\quad $S\subseteq S\cup T$\\[\lgap]
(11.32)\>\textbf{Excluded middle:}\quad $S \cup \sim S = \mathbf{U}$\\[\lgap]
\end{tabbing}

\subsection*{Basic properties of $\cap$}
\begin{tabbing}
(99.99.9)\;\=(m)\;\=\kill
(11.33)\>\textbf{Symmetry of $\cap$ :}\quad $S\cap T = T\cap S$\\[\lgap]
(11.34)\>\textbf{Associativity of $\cap$ :}\quad $(S\cap T)\cap U = S\cap (T\cap U)$\\[\lgap]
(11.35)\>\textbf{Idempotency of $\cap$ :}\quad $S\cap S = S$\\[\lgap]
(11.36)\>\textbf{Zero of $\cap$ :}\quad $S\cap \emptyset = \emptyset$\\[\lgap]
(11.37)\>\textbf{Identity of $\cap$ :}\quad $S\cap \mathbf{U} = S$\\[\lgap]
(11.38)\>\textbf{Strengthening:}\quad $S\cap T\subseteq S$\\[\lgap]
(11.39)\>\textbf{Contradiction:}\quad $S\: \cap \sim S = \emptyset$\\[\lgap]
\end{tabbing}

\subsection*{Basic properties of combinations of $\cup$ and $\cap$}
\begin{tabbing}
(99.99.9)\;\=(m)\;\=\kill
(11.40)\>\textbf{Distributivity of $\cup$ over $\cap$ :}\quad $S\cup (T\cap U) = (S\cup T)\cap (S\cup U)$\\[\lgap]
(11.41)\>\textbf{Distributivity of $\cap$ over $\cup$ :}\quad $S\cap (T\cup U) = (S\cap T)\cup (S\cap U)$\\[\lgap]
(11.42)\>\textbf{De Morgan:}\\[\lgap]
       \>(a)\> $\sim (S\cup T) =\; \sim S\:\cap \sim T$\\[\lgap]
       \>(b)\> $\sim (S\cap T) =\; \sim S\:\cup \sim T$\\[\lgap]
\end{tabbing}

\subsection*{Additional properties of $\cup$ and $\cap$}
\begin{tabbing}
(99.99.9)\;\=(m)\;\=\kill
(11.43)\>$S\subseteq T \land U\subseteq V \impl (S\cup U)\subseteq (T\cup V)$\\[\lgap]
(11.44)\>$S\subseteq T \land U\subseteq V \impl (S\cap U)\subseteq (T\cap V)$\\[\lgap]
(11.45)\>$S\subseteq T \equiv S\cup T = T$\\[\lgap]
(11.46)\>$S\subseteq T \equiv S\cap T = S$\\[\lgap]
(11.47)\>$S\cup T = \mathbf{U} \equivs (\all x\dr x\in \mathbf{U}\rb x\notin S\impl x\in T)$\\[\lgap]
(11.48)\>$S\cap T = \emptyset \equivs (\all x\drrb x\in S\impl x\notin T)$\\[\lgap]
\end{tabbing}

\subsection*{Properties of set difference}
\begin{tabbing}
(99.99.9)\;\=(m)\;\=\kill
(11.49)\>$S - T = S\:\cap \sim T$\\[\lgap]
(11.50)\>$S - T \subseteq S$\\[\lgap]
(11.51)\>$S - \emptyset = S$\\[\lgap]
(11.52)\>$S\cap (T - S) = \emptyset$\\[\lgap]
(11.53)\>$S\cup (T - S) = S\cup T$\\[\lgap]
(11.54)\>$S - (T\cup U) = (S - T)\cap (S - U)$\\[\lgap]
(11.55)\>$S - (T\cap U) = (S - T)\cup (S - U)$\\[\lgap]
\end{tabbing}

\subsection*{Implication versus subset}
\begin{tabbing}
(99.99.9)\;\=(m)\;\=\kill
(11.56)\>$(\all x\drrb P\impl Q) \equivs \{x\dr P\} \subseteq \{x\dr Q\}$\\[\lgap]
\end{tabbing}

\subsection*{Properties of subset}
\begin{tabbing}
(99.99.9)\;\=(m)\;\=\kill
(11.57)\>\textbf{Antisymmetry:}\quad $S\subseteq T\land T\subseteq S \equivs S = T$\\[\lgap]
(11.58)\>\textbf{Reflexivity:}\quad $S\subseteq S$\\[\lgap]
(11.59)\>\textbf{Transitivity:}\quad $S\subseteq T\land T\subseteq U\impl S\subseteq U$\\[\lgap]
(11.60)\>$\emptyset \subseteq S$\\[\lgap]
(11.61)\>$S\subset T \equivs S\subseteq T\land \neg (T\subseteq S)$\\[\lgap]
(11.62)\>$S\subset T \equivs S\subseteq T\land (\ext x\dr x\in T\rb x\notin S)$\\[\lgap]
(11.63)\>$S\subseteq T \equivs S\subset T\lor S = T$\\[\lgap]
(11.64)\>$S\not\subset S$\\[\lgap]
(11.65)\>$S\subset T\impl S\subseteq T$\\[\lgap]
(11.66)\>$S\subset T\impl T\nsubseteq S$\\[\lgap]
(11.67)\>$S\subseteq T\impl T\not\subset S$\\[\lgap]
(11.68)\>$S\subseteq T\land \neg(U\subseteq T)\impl \neg (U\subseteq S)$\\[\lgap]
(11.69)\>$(\ext x\dr x\in S\rb x\notin T)\impl S\ne T$\\[\lgap]
(11.70)\>\textbf{Transitivity:}\\[\lgap]
           \>(a)\>$S\subseteq T\land T\subset U\impl S\subset U$\\[\lgap]
           \>(b)\>$S\subset T\land T\subseteq U\impl S\subset U$\\[\lgap]
           \>(c)\>$S\subset T\land T\subset U\impl S\subset U$\\[\lgap]
\end{tabbing}

\subsection*{Theorems concerning power set $\mathcal{P}$}
\begin{tabbing}
(99.99.9)\;\=(m)\;\=\kill
(11.71)\>$\mathcal{P}\emptyset = \{\emptyset\}$\\[\lgap]
(11.72)\>$S\in \mathcal{P}S$\\[\lgap]
(11.73)\>$\# (\mathcal{P}S) = 2^{\# S}\quad ($for finite set $S)$\\[\lgap]
\end{tabbing}

\subsection*{Union and intersection of families of sets}
\begin{tabbing}
(99.99.9)\;\=(m)\;\=\kill
(11.74.1)\>\textbf{Definition:}\quad $v\in (\cup x\dr R\rb E) \equivs (\ext x\dr R\rb v\in E)$\\[\lgap]
(11.75.1)\>\textbf{Definition:}\quad $v\in (\cap x\dr R\rb E) \equivs (\all x\dr R\rb v\in E)$\\[\lgap]
(11.76)\>\textbf{Axiom, Partition:}\quad Set $S$ partitions $T$ if\\[\lgap]
           \>(i)\> the sets in $S$ are pairwise disjoint and\\[\lgap]
           \>(ii)\> the union of the sets in $S$ is $T$, that is, if\\[\lgap]
           \>$(\all u, v\dr u\in S\land v\in S\land u\ne v\rb u\cap v = \emptyset)\land (\cup u\dr u\in S\rb u) = T$\\[\lgap]
\end{tabbing}

\subsection*{Bags}
\begin{tabbing}
(99.99.9)\;\=(m)\;\=\kill
(11.79)\>\textbf{Axiom, Membership:}\quad $v\in \lbag x\dr R\rb E\rbag\equivss (\ext x\dr R\rb v=E)$\\[\lgap]
(11.80)\>\textbf{Axiom, Size:}\quad $\# \lbag x\dr R\rb E\rbag = (\upSigma x\dr R\rb 1)$\\[\lgap]
(11.81)\>\textbf{Axiom, Number of occurrences:}\quad $v\# \lbag x\dr R\rb E\rbag = (\upSigma x\dr R\land v=E\rb 1)$\\[\lgap]
(11.82)\>\textbf{Axiom, Bag equality:}\quad $B=C\equivss (\all v\drrb v\# B=v\# C)$\\[\lgap]
(11.83)\>\textbf{Axiom, Subbag:}\quad $B\subseteq C \equiv (\all v\drrb v\#B\le v\# C)$\\[\lgap]
(11.84)\>\textbf{Axiom, Proper subbag:}\quad $B\subset C \equiv B\subseteq C\land B\ne C$\\[\lgap]
(11.85)\>\textbf{Axiom, Union:}\quad $B\cup C = \lbag v,i\dr 0\le i<v\# B+v\# C\rb v\rbag$\\[\lgap]
(11.86)\>\textbf{Axiom, Intersection:}\quad $B\cap C = \lbag v,i\dr 0\le i<v\# B\downarrow v\# C\rb v\rbag$\\[\lgap]
(11.87)\>\textbf{Axiom, Difference:}\quad $B-C = \lbag v,i\dr 0\le i<v\# B-v\# C\rb v\rbag$\\[\lgap]
\end{tabbing}

\section*{Mathematical Induction}
\begin{tabbing}
(99.99.9)\;\=(m)\;\=\kill
(12.3)\>\textbf{Axiom, Mathematical Induction over $\mathbb{N}$:}\\[\lgap]
          \>$(\all n$: $\mathbb{N}\drrb (\all i\dr 0\le i < n\rb P.i)\impl P.n) \; \impl \; (\all n$: $\mathbb{N}\drrb P.n)$\\[\lgap]
(12.4)\>\textbf{Mathematical Induction over $\mathbb{N}$:}\\[\lgap]
          \>$(\all n$: $\mathbb{N}\drrb (\all i\dr 0\le i < n\rb P.i)\impl P.n) \equivss (\all n$: $\mathbb{N}\drrb P.n)$\\[\lgap]
(12.5)\>\textbf{Mathematical Induction over $\mathbb{N}$:}\\[\lgap]
          \>$P.0\land (\all n$: $\mathbb{N}\drrb (\all i\dr 0\le i \le n\rb P.i)\impl P(n+1)) \equivss (\all n$: $\mathbb{N}\drrb P.n)$\\[\lgap]
(12.11)\>\textbf{Definition, $b$ to the power $n$:}\\[\lgap]
           \>$b^{0} = 1$\\[\lgap]
           \>$b^{n+1} = b\cdot b^{n}\quad$ for $ n\ge 0$\\[\lgap]
(12.12)\>\textbf{$b$ to the power $n$:}\\[\lgap]
           \>$b^{0} = 1$\\[\lgap]
           \>$b^{n} = b\cdot b^{n-1}\quad$ for $ n\ge 1$\\[\lgap]
(12.13)\>\textbf{Definition, factorial:}\\[\lgap]
           \>$0! = 1$\\[\lgap]
           \>$n! = n\cdot (n-1)!\quad $ for $n > 0$\\[\lgap]
(12.14)\>\textbf{Definition, Fibonacci:}\\[\lgap]
           \>$F_{0} = 0,\quad F_{1}=1$\\[\lgap]
           \>$F_{n} = F_{n-1} + F_{n-2}\quad$ for $n > 1$\\[\lgap]
(12.14.1)\>\textbf{Definition, Golden Ratio:}\quad $\phi = (1 + \sqrt{5})/2 \approx 1.618\quad \quad \hat{\phi} = (1 - \sqrt{5})/2 \approx -0.618$\\[\lgap]
(12.15)\>$\phi^{2} = \phi + 1\quad$ and $\quad \hat{\phi}^{2} = \hat{\phi} + 1$\\[\lgap]
(12.16)\>$F_{n}\le \phi^{n-1}$\quad for $n\ge 1$\\[\lgap]
(12.16.1)\>$\phi^{n-2}\le F_{n}$\quad for $n\ge 1$\\[\lgap]
(12.17)\>$F_{n+m} = F_{m}\cdot F_{n+1} + F_{m-1}\cdot F_{n}\quad \quad$ for $n\ge 0$ and $m\ge 1$\\[\lgap]
\end{tabbing}

\end{document}
