\input utility.tdf
\input logic.tdf
\lineb
\vskip 1in 

\centerline{\bigrm Rules }
\vskip 1in 
{\bigrm

		This is a file of rules of inference used by ProofCheck.
Each rule occupies one line.  Any lines in this 
(source) file without {\TeX} dollar
signs are comment lines.  Ordinary variables
should be unadorned single letters.  

 } 

All inference rules in this file should be
derivable from standard sentence logic and 
the predicate logic in {\it A Predicate Logic Based on 
Indefinite Description and Two Notions of Identity} 
and some existence presumptions of ordinary logic
as applied to mathematical but not logical terms
and formulas.  (As an example of such an existence
presumption, it will be taken as a semantic axiom
that if x belongs to y then both x and y must exist.
On the other hand if x is identical to y then no
such presumption obtains.)
The current version of this file contains existence presumptions
regarding only elementhood, set inclusion  and tuples.

The variables in this file taken from the beginning of the alphabet
are to be taken as fixed in relation to unification. 
Thus the rule that `for all x, px' may be inferred from pa
is valid even though the inference of `for all x, px' from py
is not valid.   When pa is unified with a formula, the letter
a must be matched with a variable which is free in that formula. 

The rules in this file have not been checked.   
\lineb



$\qvar$ <= $\qvar$ 

$(\pvar \Iff \pvar)$ <=

$(\pvar \c \qvar)$ <= $\qvar$

$(\pvar \c \pvar \And \pvar )$ <= 

$(\qvar \c (\pvar \c \qvar))$ <=

$(\pvar \Or \qvar)$ <= $\qvar$

$(\pvar \Or \pvar \c \pvar)$ <=

$((\pvar \c \qvar) \And \pvar \c \qvar)$<=

$\qvar$ <= $(\pvar \And \qvar)$

$(\pvar \c (\qvar\c \rvar))$ <= $(\pvar \And \qvar \c \rvar)$

$(\pvar \And \qvar \c \rvar)$ <= $(\pvar \c (\qvar\c \rvar))$

$(\pvar \And \qvar \c \rvar)$ <= $(\pvar \And \qvar \And \svar \c \rvar)$,$(\pvar \c \svar)$

$(\pvar \And \qvar \c \rvar)$ <= $(\pvar \c \svar)$,$(\pvar \And \qvar \And \svar \c \rvar)$

$(\pvar \c \pvar \And \qvar)$ <= $(\pvar \Iff \qvar \And \rvar)$

$(\pvar \c \pvar \And \qvar)$ <= $(\qvar \And \rvar\Iff \pvar)$

$(\pvar \And \qvar \c \rvar)$ <= $(\pvar \c \qvar \Iff \rvar \And \svar)$

$(\pvar \And \qvar \c \rvar)$ <= $(\pvar \c \rvar \And \svar\Iff \qvar)$

\lineb


Modus Ponens Style Rules
\lineb

$\qvar$ <=  $(\pvar \c \qvar)$;$\pvar$

$\qvar$ <= $(\pvar \c \qvar\And \rvar)$; $\pvar$

$\rvar$ <=  $(\pvar \And \qvar\c \rvar)$;$\pvar$,$\qvar$

$\rvar$ <=  $(\pvar \And \qvar\c \rvar \And \pqvar)$;$\pvar$,$\qvar$

$\svar$ <=  $(\pvar \And \qvar\And \rvar\c \svar)$;$\pvar$,$\qvar$,$\rvar$

$\svar$ <=  $(\pvar \And \qvar\And \rvar\c \svar \And \pqvar)$;$\pvar$,$\qvar$,$\rvar$

$\svar$ <=  $(\pvar \And \qvar\And \rvar \And \pqvar\c \svar)$;$\pvar$,$\qvar$,$\rvar$,$\pqvar$

$\svar$ <=  $(\pvar \And \qvar\And \rvar \And \pqvar\And \prvar\c \svar)$;$\pvar$,$\qvar$,$\rvar$,$\pqvar$,$\prvar$

$\svar$ <=  $(\pvar \And \qvar\And \rvar \And \pqvar\And \prvar \And \psvar\c \svar)$;$\pvar$,$\qvar$,$\rvar$,$\pqvar$,$\prvar$,$\psvar$

$\svar$ <= $(\ppvar \And \pqvar \And \prvar \And \psvar \And \ptvar \And \qpvar \And \qqvar \c \svar)$;$\ppvar $,$\pqvar $,$\prvar $,$\psvar $,$\ptvar $,$\qpvar $,$\qqvar$

$\svar$ <= $(\ppvar \And \pqvar \And \prvar \And \psvar \And \ptvar \And \qpvar \And \qqvar\And \qrvar \c \svar)$;$\ppvar $,$\pqvar $,$\prvar $,$\psvar $,$\ptvar $,$\qpvar $,$\qqvar$,$\qrvar$

$\svar$ <= $(\ppvar \And \pqvar \And \prvar \And \psvar \And \ptvar \And \qpvar \And \qqvar \And \qrvar \And \qsvar \c \svar)$;$\ppvar $,$\pqvar $,$\prvar $,$\psvar $,$\ptvar $,$\qpvar $,$\qqvar$,$\qrvar$,$\qsvar$

$\rvar$ <= $(\ppvar \And \pqvar \And \prvar \And \psvar \And \qpvar \And \qqvar \And \qrvar \And \qsvar \And \rpvar \And \rqvar \c \rvar)$ ;  $\ppvar $,$  \pqvar $,$  \prvar $,$  \psvar $,$  \qpvar $,$  \qqvar $,$  \qrvar $,$  \qsvar $,$  \rpvar $ ,$ \rqvar$

$\qvar$ <=  $(\pvar \Iff \qvar)$;$\pvar$

$\qvar$ <=  $(\qvar \Iff \pvar)$;$\pvar$

$\qvar$ <= $(\pvar \And \qvar \Iff \rvar)$;$\rvar$

$\qvar$ <= $(\rvar \Iff \pvar \And \qvar )$;$\rvar$

$\qvar$ <= $(\pvar \Iff \qvar )$ ; $(\pvar \And \rvar)$

$\qvar$ <= $(\qvar \Iff\pvar)$ ; $(\pvar \And \rvar)$

$\qvar$ <= $(\pqvar \And \prvar \Iff \qvar \And \rvar)$ ; $\pqvar$,$\prvar$

$\qvar$ <= $( \qvar \And \rvar\Iff \pqvar \And \prvar )$ ; $\pqvar$,$\prvar$

$\rvar$ <=  $(\pvar \Iff \qvar \And \rvar)$;$\pvar$

$\rvar$ <=  $(\pvar \And \qvar\Iff \rvar)$;$\pvar$,$\qvar$

$\svar$ <=  $(\pvar \And \qvar\And \rvar\Iff \svar)$;$\pvar$,$\qvar$,$\rvar$

$\rvar$ <= $(\pvar \c \qvar \Iff \rvar \And \svar)$ ; $\pvar$,$\qvar$

$\rvar$ <= $(\pvar \c \qvar \Iff \rvar \And \svar)$ ; $\qvar$,$\pvar$

$\rvar$ <= $(\pvar \c \rvar \And \svar \Iff \qvar)$ ; $\pvar$,$\qvar$

$\rvar$ <= $(\pvar \c \rvar \And \svar \Iff \qvar)$ ; $\qvar$,$\pvar$

$\svar$ <=  $(\pvar \c \qvar\And \rvar\Iff \svar)$;$\pvar$,$\qvar$,$\rvar$

$\svar$ <=  $(\pvar \c \qvar\And \rvar\Iff \svar)$;$\qvar$,$\pvar$,$\rvar$

$\svar$ <=  $(\pvar \c \qvar\And \rvar\Iff \svar)$;$\rvar$,$\qvar$,$\pvar$

$\qvar$ <=  $(\pvar \Iff \qvar)$;$\pvar$

$\rvar$ <=  $(\rvar\Iff\pvar \And \qvar)$;$\pvar$,$\qvar$

$(\pvar \c \rvar)$ <= $(\qvar \c \pvar \Iff \rvar \And \svar)$ ; $\qvar$

$(\pvar \c \rvar)$ <= $(\qvar \c  \rvar \And \svar \Iff \pvar)$ ; $\qvar$

$(\pvar \c \rvar)$ <= $(\qvar \c \rvar \Iff \pvar \And \svar)$ ; $\svar$,$\qvar$

$(\pvar \c \rvar)$ <= $(\qvar \c  \pvar \And \svar \Iff \rvar)$ ; $\svar$,$\qvar$

$(\pvar \c \rvar)$ <= $(\qvar \c \rvar \Iff \pvar \And \svar)$ ; $\qvar$,$\svar$

$(\pvar \c \rvar)$ <= $(\qvar \c  \pvar \And \svar \Iff \rvar)$ ; $\qvar$,$\svar$

$(\pvar \Iff \qvar)$<= $(\pvar \Iff \qvar \And \rvar \And \svar)$;$\rvar$,$\svar$

$(\qvar \Iff \pvar)$<= $(\pvar \Iff \qvar \And \rvar \And \svar)$;$\rvar$,$\svar$

$(\pvar \Iff \qvar)$<= $(\qvar \And \rvar \And \svar\Iff\pvar)$;$\rvar$,$\svar$

$(\qvar \Iff \pvar)$<= $(\qvar \And \rvar \And \svar\Iff\pvar)$;$\rvar$,$\svar$

$\rvar$ <= $(\rvar \Iff \ppvar \And \pqvar \And \prvar )$; $\ppvar$,$\pqvar$,$\prvar$

$\rvar$ <= $(\rvar \Iff \ppvar \And \pqvar \And \prvar \And \psvar )$; $\ppvar$,$\pqvar$,$\prvar$,$\psvar$

$\rvar$ <= $(\rvar \Iff \ppvar \And \pqvar \And \prvar \And \psvar \And \qpvar)$; $\ppvar$,$\pqvar$,$\prvar$,$\psvar$,$\qpvar$

$\pqvar$ <=  $(\pvar \And \qvar\And \rvar\And \svar\c\pqvar)$;$\pvar$,$\qvar$,$\rvar$,$\svar$

$\svar$ <= $(\pvar \And \qvar \c \rvar \Iff \svar)$;$\pvar$,$\qvar$,$\rvar$

$\svar$ <= $(\pvar \And \qvar \c \svar \Iff \rvar)$;$\pvar$,$\qvar$,$\rvar$

$\svar$ <= $(\pvar \And \qvar \And \pqvar \c \rvar \Iff \svar)$;$\pvar$,$\qvar$,$\pqvar$,$\rvar$

$\svar$ <= $(\pvar \And \qvar \And \pqvar \c \svar \Iff \rvar)$;$\pvar$,$\qvar$,$\pqvar$,$\rvar$

$\svar$ <= $(\pvar \And \qvar \And \pqvar\And \prvar \c \rvar \Iff \svar)$;$\pvar$,$\qvar$,$\pqvar$,$\prvar$,$\rvar$

$\svar$ <= $(\pvar \And \qvar \And \pqvar \And\prvar\c \svar \Iff \rvar)$;$\pvar$,$\qvar$,$\pqvar$,$\prvar$,$\rvar$

$\qvar$ <=$(\qvar \And \svar \Iff \pqvar \And \prvar \And \psvar)$;$\pqvar$,$\prvar$,$\psvar$

$\qvar$ <=  $(\pvar \Iff \qvar)$;$\pvar$

$\pvar$ <=  $(\pvar \Iff \qvar)$;$\qvar$

$\rvar$ <=  $(\pvar \c \qvar \Iff \rvar)$;$\pvar$,$\qvar$

$\qvar$ <=  $(\pvar \c \qvar \Iff \rvar)$;$\pvar$,$\rvar$

$(\pvar \c \qvar )$ <= $(\pvar \And\rvar \And \svar\Iff \qvar)$;$\rvar$,$\svar$ 

$(\pvar \c \qvar )$ <= $(\pvar \And\rvar \And \svar\Iff \qvar)$;$\svar$,$\rvar$ 

$(\pvar \c \qvar )$ <= $(\qvar \Iff \pvar \And\rvar \And \svar)$;$\rvar$,$\svar$ 

$(\pvar \c \qvar )$ <= $(\qvar \Iff \pvar \And\rvar \And \svar)$;$\svar$,$\rvar$ 

$(\pvar  \c \rvar)$ <= $(\pvar \Iff \qvar \And \rvar)$; $\qvar$

$(\pvar \And \rvar\c \svar)$<=$(\pvar \And \qvar \c \rvar \Iff \svar)$;$\qvar$

$(\pvar \And \rvar\c \svar)$<=$(\pvar \And \qvar \c \svar \Iff \rvar)$;$\qvar$

$(\pvar \c \qvar)$ <= $(\pqvar \And \prvar \And \psvar \c \pvar \Iff \qvar)$;$\pqvar$,$\prvar$,$\psvar$

$(\pvar \c \qvar)$ <= $(\pqvar \And \prvar \And \psvar \c \qvar \Iff \pvar)$;$\pqvar$,$\prvar$,$\psvar$

$(\pvar \c \qvar)$ <= $(\pvar \And \rvar \c \qvar \And \svar)$ ; $\rvar$

$(\Not\pvar \c \Not\qvar)$ <= $(\pqvar \And \prvar \And \psvar \c \pvar \Iff \qvar)$;$\pqvar$,$\prvar$,$\psvar$ 

$(\Not\qvar \c \Not\pvar)$ <= $(\pqvar \And \prvar \And \psvar \c \pvar \Iff \qvar)$;$\pqvar$,$\prvar$,$\psvar$ 

$\qvar$ <= $(\qvar \Iff \pvar \Or \rvar)$;$\pvar$

$\qvar$ <= $(\qvar \Iff \rvar \Or \pvar)$;$\pvar$

$\Not \pvar$ <= $(\pvar \c \qvar)$ ; $\Not \qvar$

$(\rvar \c \pvar) $ <= $(\pvar \Iff \qvar)$ ; $\qvar$

$(\rvar \c \pvar) $ <= $(\qvar \Iff \pvar)$ ; $\qvar$

$(\pvar \c \qvar) $ <= $(\rvar \And \svar \c \qvar)$ ; $\rvar$,$\svar$

$(\pvar \And \rvar \c \qvar \And \rvar)$ <=  $(\svar \c \qvar\Iff \pvar)$;$\svar$

$(\rvar \c \rvar \And \svar)$ <=  $(\pvar \And \qvar\And \rvar\c \svar)$;$\pvar$,$\qvar$

$\svar$ <=  $(\pvar \c \svar\Iff \qvar\And \rvar)$;$\pvar$,$\qvar$,$\rvar$

$\svar$ <=  $(\pvar \c \svar\Iff \qvar\And \rvar)$;$\qvar$,$\pvar$,$\rvar$

$\svar$ <=  $(\pvar \c \svar\Iff \qvar\And \rvar)$;$\rvar$,$\qvar$,$\pvar$

$\qvar$<=$(\pqvar \And \prvar \c \pvar \Iff \qvar)$;$\pvar$,$\pqvar$,$\prvar$

$\qvar$<=$(\pqvar \And \prvar \c \pvar \Iff \qvar)$;$\pqvar$,$\pvar$,$\prvar$

$\qvar$<=$(\pqvar \And \prvar \c \pvar \Iff \qvar)$;$\prvar$,$\pqvar$,$\pvar$

$\qvar$<=$(\pqvar \And \prvar \c \qvar \Iff \pvar)$;$\pvar$,$\pqvar$,$\prvar$

$\qvar$<=$(\pqvar \And \prvar \c \qvar \Iff \pvar)$;$\pqvar$,$\pvar$,$\prvar$

$\qvar$<=$(\pqvar \And \prvar \c \pvar \Iff \pvar)$;$\prvar$,$\pqvar$,$\pvar$

$\Not \qvar$ <= $(\pvar \And \qvar \Iff \rvar)$;$\pvar$,$\Not\rvar$

$\Not \qvar$ <= $(\rvar \Iff \pvar \And \qvar)$;$\pvar$,$\Not\rvar$

$\Not \qvar$ <= $(\pvar \And \qvar \Iff \rvar)$;$\Not\rvar$,$\pvar$

$\Not \qvar$ <= $(\rvar \Iff \pvar \And \qvar)$;$\Not\rvar$,$\pvar$

$(\pvar \c \qvar)$ <= $(\pqvar \And \prvar \And \psvar \And \ppvar \c \pvar \Iff \qvar)$;$\pqvar$,$\prvar$,$\psvar$,$\ppvar$

$(\pvar \c \qvar)$ <= $(\pqvar \And \prvar \And \psvar \And \ppvar \c \qvar \Iff \pvar)$;$\pqvar$,$\prvar$,$\psvar$,$\ppvar$

$(\pvar \c \pvar \And\qvar)$ <= $(\pvar \c \qvar \Iff \rvar)$;  $\rvar$

$(\pvar \c \pvar \And\qvar)$ <= $(\pvar \c \rvar \Iff \qvar)$;  $\rvar$

$(\svar \c \rvar)$ <= $(\ppvar \And \pqvar \And \prvar \c \rvar)$ ; $\ppvar$,$\pqvar$,$\prvar$

$(\svar \c \rvar)$ <= $(\ppvar \And \pqvar \And \prvar \And \psvar \c \rvar)$ ; $\ppvar$,$\pqvar$,$\prvar$,$\psvar$

$(\pvar \And \prvar \And \rvar \c \pvar \And \qvar \And \rvar)$ <= $(\pvar \And \pqvar \And \prvar\c \qvar)$;$\pqvar$

$(\pvar \c \qvar)$ <= $(\pvar \And \rvar \c \svar \Iff \qvar)$;$\rvar$,$\svar$

$(\pvar \c \qvar)$ <= $(\pvar \And \rvar \c \svar \Iff \qvar)$;$\svar$,$\rvar$

$(\pvar \c \qvar)$ <= $(\pvar \And \rvar \c \qvar \Iff \svar)$;$\rvar$,$\svar$

$(\pvar \c \qvar)$ <= $(\pvar \And \rvar \c \qvar \Iff \svar)$;$\svar$,$\rvar$

$(\pvar  \c \pvar \And \qvar)$ <= $(\ppvar \And \pqvar \And \prvar\c\qvar)$;$\ppvar$,$\pqvar$,$\prvar$

$(\pqvar \c \rvar )$ <= $(\pvar  \c \rvar \Iff \pqvar \Or \prvar )$;$\pvar$

$(\prvar \c \rvar )$ <= $(\pvar  \c \rvar \Iff \pqvar \Or \prvar )$;$\pvar$

$\rvar $ <= $(\pvar \c \qvar \Iff \rvar)$ ; $\pvar$,$\qvar$

$\rvar $ <= $(\pvar \c \qvar \Iff \rvar)$ ; $\qvar$,$\pvar$

$\rvar $ <= $(\pvar \c \rvar \Iff \qvar)$ ; $\pvar$,$\qvar$

$\rvar $ <= $(\pvar \c \rvar \Iff \qvar)$ ; $\qvar$,$\pvar$

$\qvar$<=$(\pqvar \And \prvar \And \psvar \c \qvar)$;($(\pvar \Iff \pqvar \And \svar)$;$\pvar$),$\prvar$,$\psvar$

$\qvar$<=$(\pqvar \And \prvar \And \psvar \c \qvar)$;$\prvar$,($(\pvar \Iff \pqvar \And \svar)$;$\pvar$),$\psvar$

$\qvar$<=$(\pqvar \And \prvar \And \psvar \c \qvar)$;$\prvar$,$\psvar$,($(\pvar \Iff \pqvar \And \svar)$;$\pvar$)

\lineb

Case Eliminations

$(\qvar \Or \rvar)$ <= $(\pvar \Or \qvar \Or\rvar)$;$\Not \pvar$

$(\qvar \Or \rvar)$ <= $(\qvar \Or \pvar \Or\rvar)$;$\Not \pvar$

$(\qvar \Or \rvar)$ <= $(\qvar \Or \rvar \Or\pvar)$;$\Not \pvar$

$\rvar$ <= $(\pvar \Or \qvar \Or\rvar)$;$\Not \pvar$,$\Not \qvar$

$\rvar$ <= $(\pvar \Or \qvar \Or\rvar)$;$\Not \qvar$,$\Not \pvar$

$\rvar$ <= $(\pvar \Or \rvar \Or\qvar)$;$\Not \pvar$,$\Not \qvar$

$\rvar$ <= $(\pvar \Or \rvar \Or\qvar)$;$\Not \qvar$,$\Not \pvar$

$\rvar$ <= $(\rvar \Or \pvar \Or\qvar)$;$\Not \pvar$,$\Not \qvar$

$\rvar$ <= $(\rvar \Or \pvar \Or\qvar)$;$\Not \qvar$,$\Not \pvar$

$\qvar$ <= $( \pvar \Or \qvar)$; $\Not \pvar$

$\qvar$ <= $( \qvar \Or \pvar)$; $\Not \pvar$

$(\rvar \And \qvar)$ <= $(\rvar \And ( \pvar \Or \qvar))$; $\Not \pvar$

$(\rvar \And \qvar)$ <= $(\rvar \And ( \qvar \Or \pvar))$; $\Not \pvar$

$(\rvar \And \qvar)$ <= $(\rvar \And ( \pvar \Or \qvar) \And \Not\pvar )$

$(\rvar \And \qvar)$ <= $(\rvar \And ( \qvar \Or \pvar))$; $\Not \pvar$

$(\rvar \And ( \pvar \Or \qvar) \And \Not\pvar  \c \rvar \And \qvar)$ <=

$(\rvar \And ( \qvar \Or \pvar) \And \Not\pvar  \c \rvar \And \qvar)$ <=

$(\Not \pvar \c \qvar)$ <= $(\pvar \Or \qvar)$

$(\Not \pvar \c \qvar)$ <= $(\qvar \Or \pvar)$

$(\Not \pvar \c \qvar \Or \rvar)$ <= $(\pvar\Or\qvar\Or\rvar)$

$(\Not \pvar \c \qvar \Or \rvar)$ <= $(\qvar\Or\pvar\Or\rvar)$

$(\Not \pvar \c \qvar \Or \rvar)$ <= $(\rvar\Or\qvar\Or\pvar)$

$\rvar$ <= $(\pvar\c\rvar)$,$(\qvar\c\rvar)$;$(\pvar\Or\qvar)$

$((\pvar \Or \qvar \Or \rvar) \And \Not \pvar \c \qvar \Or \rvar)$ <=

$((\pvar \Or \qvar \Or \rvar) \And \Not \qvar \c \pvar \Or \rvar)$ <=

$((\pvar \Or \qvar \Or \rvar) \And \Not \rvar \c \pvar \Or \qvar)$ <=

$(\qvar \Iff \qvar \Or \rvar)$ <= $\Not\rvar$

$(\qvar \Iff \rvar \Or \qvar)$ <= $\Not\rvar$

$(\qvar \Or \rvar\Iff \qvar)$ <= $\Not\rvar$

$(\rvar \Or \qvar\Iff \qvar)$ <= $\Not\rvar$

$((\pvar \Or \qvar \Or \rvar) \And \Not \pvar \Iff \qvar \Or \rvar)$ <= 

$((\pvar \Or \qvar \Or \rvar) \And \Not \qvar \Iff \pvar \Or \rvar)$ <= 

$((\pvar \Or \qvar \Or \rvar) \And \Not \rvar \Iff \pvar \Or \qvar)$ <= 

$(\qvar \Or \rvar \Iff (\pvar \Or \qvar \Or \rvar) \And \Not \pvar)$ <= 

$(\pvar \Or \rvar \Iff (\pvar \Or \qvar \Or \rvar) \And \Not \qvar)$ <= 

$(\pvar \Or \qvar \Iff (\pvar \Or \qvar \Or \rvar) \And \Not \rvar)$ <= 

$\rvar$ <= $(\pqvar\c\rvar)$,$(\prvar\c\rvar)$,$(\psvar\c\rvar)$;$(\pqvar\Or\prvar\Or\psvar)$

$(\pvar \c \qvar)$ <= $(\pqvar \c \qvar)$,$(\prvar \c \qvar)$,$(\psvar \c \qvar)$;$(\pvar \c \pqvar \Or \prvar \Or \psvar )$ 

$\pvar$ <= $(x = y \Or \pvar)$; $(x \ne y)$

$\pvar$ <= $(\pvar \Or x = y)$; $(x \ne y)$

$\pvar$ <= $(x \ne y \Or \pvar)$; $(x = y)$

$\pvar$ <= $(\pvar \Or x \ne y)$; $(x = y)$

$(x = y \Or \pvar \c \pvar)$<= $(x \ne y)$

$(\pvar \Or x = y \c \pvar)$<= $(x \ne y)$

$(x \ne y \Or \pvar \c \pvar)$<= $(x = y)$

$(\pvar \Or x \ne y \c \pvar)$<=  $(x = y)$

$(\pvar \And \Not\qvar \c \rvar)$ <= $(\pvar \c \qvar \Or \rvar)$

$(\pvar \And \Not\rvar \c \qvar)$ <= $(\pvar \c \qvar \Or \rvar)$

\lineb


Justifying Implications
\lineb

$(\pvar \And \qvar \c \qvar)$ <=

$(\qvar \c \qvar)$ <=

$(\pvar \c \qvar)$ <= $(\pvar \c \qvar \And \rvar)$

$(\pvar \And \qvar \c \pvar \And \qvar \And \qvar)$<=

$(\pvar \c \qvar)$ <= $(\pvar \Iff \qvar \And \rvar)$

$(\pvar \c \qvar)$ <= $(\qvar \And \rvar\Iff \pvar)$

$(\pvar \And \rvar \c \qvar \And \rvar)$<=$(\svar \And \qvar \Iff \pvar)$

$(\pvar \And \rvar \c \qvar \And \rvar)$<=$(\pvar \Iff \svar \And \qvar)$

$(\pvar \c \qvar)$ <= $(\pvar \And \rvar \Iff \qvar)$;$\rvar$

$(\pvar \c \qvar)$ <= $(\qvar \Iff \pvar\And\rvar)$;$\rvar$

$(\pvar \c \rvar)$ <=  $(\pvar \c \qvar\Iff \rvar)$;$\qvar$

$(\pvar \c \rvar)$ <=  $(\qvar \c \pvar\Iff \rvar)$;$\qvar$

$(\pvar \c \rvar)$ <=  $(\pvar \c \rvar\Iff \qvar)$;$\qvar$

$(\pvar \c \rvar)$ <=  $(\qvar \c \rvar\Iff \pvar)$;$\qvar$

$(\pvar \And \rvar \c \qvar \And \rvar)$ <= $(\pvar \And \svar \Iff \qvar)$ ; $\svar$

$(\pvar \And \rvar \c \qvar \And \rvar)$ <= $(\qvar \Iff \pvar \And \svar)$ ; $\svar$

$(\pvar \And \rvar \c \qvar \And \rvar)$ <= $(\qvar \Iff \pvar \And \svar \And \psvar)$ ; $\svar$,$\psvar$

$(\pvar \And \rvar \c \qvar \And \rvar)$ <= $(\pvar \And \svar \And \psvar \Iff \qvar)$ ; $\svar$,$\psvar$

$(\qvar \c \rvar)$ <=  $(\ppvar \And \pqvar\c \qvar\Iff \rvar)$;$\ppvar$,$\pqvar$

$(\qvar \c \rvar)$ <=  $(\ppvar \And \pqvar \c \rvar\Iff \qvar)$;$\ppvar$,$\pqvar$

$(\pvar \c \qvar)$ <= $(\qvar \Iff \pvar \Or \rvar)$

$(\pvar \c \qvar)$ <= $(\qvar \Iff \rvar \Or \pvar)$

$(\pvar \c \qvar)$ <= $(\pvar \Or \rvar\Iff \qvar)$

$(\pvar \c \qvar)$ <= $(\pvar \Or \rvar\Iff \qvar)$

$(\svar \c \rvar \And \svar)$ <= $(\pvar \And \qvar \c \rvar)$; $\pvar$,$\qvar$

$(\pvar \And \qvar \c \rvar \And \qvar)$ <= $(\pvar \And \qvar \c \rvar)$

$(\pvar \And \qvar \c \rvar \And \qvar)$ <= $(\pvar \c  \qvar \Iff \rvar)$

$(\pvar \And \qvar \c \rvar \And \qvar)$ <= $(\qvar \c  \pvar \Iff \rvar)$

$(\pvar \And \qvar \c \pvar \And \rvar)$ <= $( \rvar \Iff \pvar \And \qvar) $

$(\pvar \c \rvar)$ <= $(\pvar \c \qvar)$, $(\qvar \Iff \rvar)$

$(\pvar \c \rvar)$ <= $(\pvar \c \qvar)$, $(\rvar \Iff \qvar)$

$(\pvar \c \rvar)$ <= $(\pvar \And \qvar \c \rvar)$; $\qvar$

$(\pvar \c \pvar \And \rvar)$ <= $(\pvar \And \qvar \c \rvar)$; $\qvar$

$(\pvar \c \rvar)$ <= $(\pvar \And \qpvar \And \qqvar\c \rvar)$; $\qpvar$,$\qqvar$

$(\pvar \c \rvar)$ <= $(\pvar \And \qpvar \And \qqvar\And \qrvar \c \rvar)$; $\qpvar$,$\qqvar$,$\qrvar$

$(\pvar \c \rvar)$ <= $(\pvar \And \qpvar \And \qqvar\And \qrvar\And \qsvar \c \rvar)$; $\qpvar$,$\qqvar$,$\qrvar$,$\qsvar$

$(\pvar \c \rvar)$ <= $(\pvar \And \qpvar \And \qqvar\And \qrvar\And \qsvar \And \spvar \c \rvar)$; $\qpvar$,$\qqvar$,$\qrvar$,$\qsvar$,$\spvar$

$(\pvar \c \rvar)$ <= $(\pvar \And \qpvar \And \qqvar\And \qrvar\And \qsvar \And \spvar \And \sqvar\c \rvar)$; $\qpvar$,$\qqvar$,$\qrvar$,$\qsvar$,$\spvar$,$\sqvar$

$(\qvar \c \qvar \And \rvar)$ <= $(\pvar \c \rvar)$; $\pvar$

$(\pvar \c \qvar)$ <= $(\pvar \Iff \qvar \And \rvar)$

$(\pvar \c \qvar)$ <= $(\pvar \And \rvar\Iff \qvar )$;$\rvar$

$(\pvar \c \qvar)$ <= $(\qvar \Iff \pvar \And \rvar)$;$\rvar$

$(\pvar \c \rvar)$ <= $(\pvar \And \qvar \c \rvar)$; $\qvar$

$(\pvar \c \svar)$ <= $(\pvar \And \qvar \And \rvar \c \svar)$; $\qvar$, $\rvar$

$(\pvar \c \rvar)$ <= $(\pvar \And \qvar \And \pqvar \And \prvar \c \rvar)$; $\qvar$, $\pqvar$,$\prvar$

$(\pvar \And \rvar\c \pvar \And \svar)$ <=  $(\pvar \And \qvar \And \rvar \c \svar)$;$\qvar$

$(\pvar \And \rvar \c \pvar \And \qvar \And \rvar)$ <= $(\pvar \Iff \pvar \And \qvar)$

$(\pvar \And \rvar \c \qvar \And \rvar)$ <= $(\pvar \Iff \qvar \And \pqvar)$

$(\pvar  \c \pvar \And \qvar)$ <= $(\qvar \Iff \rvar )$; $\rvar$

$(\pvar \c \pvar \And \qvar)$ <= $(\qvar \And \rvar)$
\lineb

Justifying Conjunctions

$(\pvar \And \qvar \And \rvar \And \svar\And \ppvar\And \pqvar \And \prvar \And \psvar)$ <= $\pvar$,$\qvar$,$\rvar$,$\svar$,$\ppvar$,$\pqvar$,$\prvar$,$\psvar$

$(\pvar \And \qvar \And \rvar \And \svar\And \ppvar\And \pqvar \And \prvar)$ <= $\pvar$,$\qvar$,$\rvar$,$\svar$,$\ppvar$,$\pqvar$,$\prvar$

$(\pvar \And \qvar \And \rvar \And \svar\And \ppvar\And \pqvar )$ <= $\pvar$,$\qvar$,$\rvar$,$\svar$,$\ppvar$,$\pqvar$

$(\pvar \And \qvar \And \rvar \And \svar\And \ppvar)$ <= $\pvar$,$\qvar$,$\rvar$,$\svar$,$\ppvar$

$(\pvar \And \qvar \And \rvar \And \svar)$ <= $\pvar$,$\qvar$,$\rvar$,$\svar$

$(\pvar \And \rvar)$ <= $(\pvar \c \qvar \Iff \rvar)$; $(\pvar \And\qvar)$

$(\pvar \And \rvar)$ <= $(\pvar \c \rvar \Iff \qvar)$; $(\pvar\And \qvar)$

$(\pvar \And \rvar \c \qvar \And \rvar)$<=$(\pvar \And \pqvar \And \prvar \And \psvar \c \qvar)$; $\pqvar$,$\prvar$,$\psvar$

$(\rvar \c \qvar \And \rvar)$<=$(\pvar \And \pqvar \And \prvar \And \psvar \c \qvar)$; $\pvar$,$\pqvar$,$\prvar$,$\psvar$

\lineb

Replacing a Conjunct

$(\pvar \And \qvar \c \pvar \And \rvar)$ <= $(\pvar \And \svar \c \qvar \Iff \rvar)$;$\svar$

$(\pvar \And \qvar \c \pvar \And \rvar)$ <= $(\pvar \And \svar \c \rvar \Iff \qvar)$;$\svar$

$(\Not \pvar \And \rvar \c \Not \qvar\And \rvar )$ <= $(\pqvar \c \pvar \Iff\qvar)$;$\pqvar$

$(\Not \pvar \And \rvar \c \Not \qvar\And \rvar )$ <= $(\pqvar \c \qvar \Iff\pvar)$;$\pqvar$

$(\rvar \And \pvar \c \rvar \And \qvar)$<= $(\pvar \And \pqvar \And \prvar \c \qvar)$;$\pqvar$,$\prvar$

Strengthening a Conjunct

$((\pvar \Or \rvar)\And \qvar \c \pvar \And \qvar)$ <= $\Not \rvar$

$((\rvar \Or \pvar)\And \qvar \c \pvar \And \qvar)$ <= $\Not \rvar$

$((\pvar \Or \rvar)\And \qvar \c \pvar \And \qvar)$ <= $(\svar \c \Not \rvar)$;$\svar$

$((\rvar \Or \pvar)\And \qvar \c \pvar \And \qvar)$ <= $(\svar \c \Not \rvar)$;$\svar$

$((\pvar \Or \rvar)\And \qvar \c \pvar \And \qvar)$ <= $(\rvar \c  \svar)$;$\Not\svar$

$((\rvar \Or \pvar)\And \qvar \c \pvar \And \qvar)$ <= $(\rvar \c  \svar)$;$\Not\svar$

\lineb

Adding a Conjunct

$(\pvar \c \qvar \And \pvar)$ <= $(\ppvar \And \pqvar \And \prvar \c \qvar \Iff \psvar)$ ; $\ppvar$,$\pqvar$,$\prvar$,$\psvar$

$(\pvar \c \qvar \And \pvar)$ <= $(\ppvar \And \pqvar \And \prvar \c \qvar \Iff \psvar)$ ; $\ppvar$,$\pqvar$,$\psvar$,$\prvar$

$(\pvar \c \qvar \And \pvar)$ <= $(\ppvar \And \pqvar \And \prvar \c \qvar \Iff \psvar)$ ; $\ppvar$,$\psvar$,$\prvar$,$\pqvar$

$(\pvar \c \qvar \And \pvar)$ <= $(\ppvar \And \pqvar \And \prvar \c \qvar \Iff \psvar)$ ; $\psvar$,$\pqvar$,$\prvar$,$\ppvar$

$(\pvar \c \qvar \And \pvar)$ <= $(\ppvar \And \pqvar \And \prvar \c \psvar \Iff \qvar)$ ; $\ppvar$,$\pqvar$,$\prvar$,$\psvar$

$(\pvar \c \qvar \And \pvar)$ <= $(\ppvar \And \pqvar \And \prvar \c \psvar \Iff \qvar)$ ; $\ppvar$,$\pqvar$,$\psvar$,$\prvar$

$(\pvar \c \qvar \And \pvar)$ <= $(\ppvar \And \pqvar \And \prvar \c \psvar \Iff \qvar)$ ; $\ppvar$,$\psvar$,$\prvar$,$\pqvar$

$(\pvar \c \qvar \And \pvar)$ <= $(\ppvar \And \pqvar \And \prvar \c \psvar \Iff \qvar)$ ; $\psvar$,$\pqvar$,$\prvar$,$\ppvar$
\lineb

Justifying Implications of Disjunctions 
\lineb

$(\pvar \c \pvar \Or \qvar)$ <=

$(\qvar \c \pvar \Or \qvar)$ <=

$(\pvar \Or \qvar)$ <= $\pvar$

$(\pvar \Or \qvar)$ <= $\qvar$

$(\pvar \Or \qvar \c \qvar \Or \pvar)$ <=

$(\pvar \Or (\pvar \Or \qvar)\c \pvar \Or \qvar)$ <=

$((\pvar \Or \qvar) \Or \qvar \c \pvar \Or \qvar)$ <=

$( \pvar \Or \qvar \c \qvar)$<= $\Not \pvar$

$( \pvar \Or \qvar \c \pvar)$<= $\Not \qvar$

$( \pvar \Or \qvar \Or \rvar \c \qvar \Or \rvar)$<= $\Not \pvar$

$( \pvar \Or \qvar \Or \rvar \c \pvar \Or \rvar)$<= $\Not \qvar$

$( \pvar \Or \qvar \Or \rvar \c \pvar \Or \qvar)$<= $\Not \rvar$

$( \rvar \Or \pvar \c \rvar \Or \qvar)$<= $(\pvar\c \qvar)$

$(\pvar \Or \rvar \c \qvar \Or \rvar )$<= $(\pvar\c \qvar)$

$(\pvar \Or \rvar \c \qvar \Or \rvar)$<= $(\pvar \And \pqvar \c \qvar)$;$\pqvar$

$(\rvar \Or \pvar \c \rvar \Or \qvar)$<= $(\pvar \And \pqvar \c \qvar)$;$\pqvar$

$(\rvar \Or \pvar \c \rvar \Or \qvar)$ <= $(\pvar \Iff \qvar)$

$(\pvar \Or \rvar \c \qvar \Or \rvar)$ <= $(\pvar \Iff \qvar)$

$(\pvar \Or \qvar \c\pvar )$<=$(\qvar \And \rvar \c \pvar )$;$\rvar$

$(\qvar \Or \pvar \c\pvar )$<=$(\qvar \And \rvar \c \pvar )$;$\rvar$

$(\pvar  \Or \rvar \c \qvar \Or \rvar )$ <= $(\pqvar \c \qvar \Iff \pvar )$;$\prvar$

$(\pvar  \Or \rvar \c \qvar \Or \rvar )$ <= $(\pqvar \c \pvar \Iff \qvar )$;$\prvar$

$(\rvar  \Or \pvar \c \rvar \Or \qvar )$ <= $(\pqvar \c \qvar \Iff \pvar )$;$\prvar$

$(\rvar  \Or \pvar \c \rvar \Or \qvar )$ <= $(\pqvar \c \pvar \Iff \qvar )$;$\prvar$

$(\pvar \Or (\qvar \And \rvar) \c \pvar \Or \qvar)$ <=

$((\pvar \And \rvar) \Or \qvar \c \pvar \Or \qvar)$ <=

$(\pvar \Or (\rvar \Or \qvar) \c \pvar \Or \qvar)$ <= $(\rvar \c \qvar)$

$((\rvar \Or \qvar) \Or \pvar \c \qvar \Or \pvar)$ <= $(\rvar \c \qvar)$

$(\pvar \Or (\qvar \Or \rvar) \c \pvar \Or \qvar)$ <= $(\rvar \c \qvar)$

$((\qvar \Or \rvar) \Or \pvar \c \qvar \Or \pvar)$ <= $(\rvar \c \qvar)$

$(\pvar \c \qvar)$ <= $(\pvar \c \rvar \And \svar)$; $(\rvar \c \qvar)$, $(\svar \c \qvar)$

$(\pvar \c \qvar)$ <= $(\pvar \c \rvar \And \svar)$; $(\svar \c \qvar)$, $(\rvar \c \qvar)$

$((\Not \qvar \And \rvar) \Or  \svar\c (\Not \pvar \And \rvar)\Or\svar)$ <= $(\pvar \c \qvar)$

$(\svar \Or (\Not \qvar \And \rvar) \c \svar \Or (\Not \pvar \And \rvar))$ <= $(\pvar \c \qvar)$

$((\pvar \And \rvar) \Or  \svar\c (\qvar \And \rvar)\Or\svar)$ <= $(\qvar\Iff \pvar \And \pqvar)$;$\pqvar$

$((\pvar \And \rvar) \Or  \svar\c (\qvar \And \rvar)\Or\svar)$ <= $(\pvar \And \pqvar\Iff \qvar )$;$\pqvar$

$(\svar \Or  (\pvar \And \rvar) \c \svar\Or(\qvar \And \rvar) )$ <= $(\qvar\Iff \pvar \And \pqvar)$;$\pqvar$

$(\svar \Or  (\pvar \And \rvar) \c \svar\Or(\qvar \And \rvar) )$ <= $( \pvar \And \pqvar\Iff \qvar )$;$\pqvar$

$(\pvar \Or \qvar \c \pvar)$ <= $(\qvar \c \pvar)$

$(\pvar \Or \qvar \c \qvar)$ <= $(\pvar \c \qvar)$

$(\pvar \Or (\qvar \Or \rvar)\c (\pvar \Or \qvar) \Or \rvar)$ <=

$((\pvar \Or \qvar )\Or \rvar\c \pvar \Or (\qvar \Or \rvar))$ <=

$(\pvar \Or \rvar \c \qvar \Or \rvar)$ <= $(\pvar \Iff \qvar)$

$(\pvar \Or \rvar \c \qvar \Or \rvar)$ <= $(\qvar \Iff \pvar)$

$(\rvar \Or \pvar \c \rvar \Or \qvar)$ <= $(\pvar \Iff \qvar)$

$(\rvar \Or \pvar \c \rvar \Or \qvar)$ <= $(\qvar \Iff \pvar)$

$(\pvar \Or \rvar \c \qvar \Or \rvar)$ <= $(\pvar \Iff \qvar \And \svar)$;$\svar$

$(\pvar \Or \rvar \c \qvar \Or \rvar)$ <= $(\qvar \Iff \pvar \And \svar)$;$\svar$

$(\pvar \Or \rvar \c \qvar \Or \rvar)$ <= $(\qvar \And \svar\Iff \pvar)$;$\svar$

$(\pvar \Or \rvar \c \qvar \Or \rvar)$ <= $(\pvar \And \svar\Iff \qvar)$;$\svar$

$(\rvar \Or \pvar   \c \rvar \Or \qvar  )$ <= $(\pvar \Iff \qvar \And \svar)$;$\svar$

$(\rvar \Or \pvar   \c \rvar \Or \qvar  )$ <= $(\qvar \Iff \pvar \And \svar)$;$\svar$

$(\rvar \Or \pvar   \c \rvar \Or \qvar  )$ <= $(\qvar \And \svar\Iff \pvar)$;$\svar$

$(\rvar \Or \pvar   \c \rvar \Or \qvar  )$ <= $(\pvar \And \svar\Iff \qvar)$;$\svar$

$(\pvar \Or \rvar \c \qvar \Or \rvar)$ <= $(\pqvar \And \prvar \c\pvar \Iff \qvar)$;$\pqvar$,$\prvar$

$(\pvar \Or \rvar \c \qvar \Or \rvar)$ <= $(\pqvar\And\prvar\c\qvar \Iff\pvar)$;$\pqvar$,$\prvar$

$(\rvar \Or \pvar \c \rvar \Or \qvar)$ <= $(\pqvar\And\prvar\c\pvar \Iff\qvar)$;$\pqvar$,$\prvar$

$(\rvar \Or \pvar \c \rvar \Or \qvar)$ <= $(\pqvar\And\prvar\c\qvar \Iff\pvar)$;$\pqvar$,$\prvar$

$(\Some x \pbar x \Or \pvar \c \Some x \qbar x \Or \pvar)$ <= $(\pbar a\c\qbar a)$ U 

$(\Some x (\pbar x \And \rbar x) \Or \pvar \c \Some x (\qbar x \And \rbar x)\Or \pvar)$<= $(\pbar a \c \qbar a)$ U

$(\pvar \Or \Some x (\pbar x \And \rbar x) \c \pvar \Or \Some x (\qbar x \And \rbar x))$<= $(\pbar a \c \qbar a)$ U

$(y \in A \Or \rvar \c \qbar y \Or \rvar)$<= $\Each x \in A \qbar x$

$(\rvar \Or y \in A \c \rvar \Or \qbar y )$<= $\Each x \in A \qbar x$

$(\pvar \Or \rvar \c \qvar \Or \rvar)$<= $(\pvar \And \pqvar \And \prvar \c \qvar)$;$\pqvar$,$\prvar$

$(\rvar \Or \pvar \c \rvar \Or \qvar)$<= $(\pvar \And \pqvar \And \prvar \c \qvar)$;$\pqvar$,$\prvar$

$(\pvar \Or \rvar \c \qvar \Or \rvar)$<= $(\pvar \And \pqvar \And \prvar \Iff \qvar)$;$\pqvar$,$\prvar$

$(\rvar \Or \pvar \c \rvar \Or \qvar)$<= $(\pvar \And \pqvar \And \prvar \Iff \qvar)$;$\pqvar$,$\prvar$

$(\pvar \Or \rvar \c \qvar \Or \rvar)$<= $(\qvar \Iff \pvar \And \pqvar \And \prvar )$;$\pqvar$,$\prvar$

$(\rvar \Or \pvar \c \rvar \Or \qvar)$<= $(\qvar \Iff \pvar \And \pqvar \And \prvar )$;$\pqvar$,$\prvar$
\lineb

Interrupted Implication of Disjunctions
\lineb

$(\rvar \Or \qvar)$<=$(\pvar \c \qvar)$;$(\rvar \Or \pvar)$

$(\qvar \Or \rvar)$<=$(\pvar \c \qvar)$;$(\pvar \Or \rvar)$

\lineb

Cases Rules
\lineb


$\rvar$ <= $(\pvar\c\rvar)$,$(\qvar \c \rvar)$;$(\pvar\Or\qvar)$
 
$\rvar$ <= $(\pvar\c\rvar)$,$(\qvar \c \rvar)$;$(\qvar\Or\pvar)$ 

$\rvar$ <= $(\pvar \c \rvar)$, $(\Not \pvar \c \rvar)$

$\rvar$ <= $(\Not\pvar \c \rvar)$, $(\pvar \c \rvar)$

$(\qvar \c \rvar)$ <= $(\qvar \And \Not\pvar \c \rvar)$, $(\qvar \And \pvar \c \rvar)$

$(\qvar \c \rvar)$ <= $(\qvar \And \pvar \c \rvar)$, $(\qvar \And \Not\pvar \c \rvar)$


\lineb



Justifying Implication with And
\lineb

$(\pvar \c \qvar \And \rvar)$ <= $(\pvar \c \qvar)$,$(\pvar \c \rvar)$

$(\pvar \c \qvar \And \rvar \And \svar)$ <= $(\pvar \c \qvar)$,$(\pvar \c \rvar)$,$(\pvar \c \svar)$

$(\pvar \c \pvar \And \qvar)$ <= $(\qvar \And \rvar)$

$(\pvar \And \rvar \c \pvar \And \qvar \And \rvar)$ <= $(\pvar \c \qvar \And \pqvar)$

$(\pvar  \c \pvar \And \qvar )$ <= $(\pvar \c \qvar \And \pqvar)$

$(\pvar  \c \pvar \And \qvar )$ <= $(\pqvar\c \prvar \Iff \qvar )$;$\pqvar$,$\prvar$

$(\pvar  \c \pvar \And \qvar )$ <= $(\pqvar\c \prvar \Iff \qvar )$;$\prvar$,$\pqvar$

$(\pvar  \c \pvar \And \qvar )$ <= $(\pqvar\c \qvar \Iff \prvar )$;$\pqvar$,$\prvar$

$(\pvar  \c \pvar \And \qvar )$ <= $(\pqvar\c \qvar \Iff \prvar )$;$\prvar$,$\pqvar$

$(\Not \pvar \c \Not \qvar)$ <= $(\pvar \Iff \pqvar \And \prvar \And \qvar)$;$\pqvar$,$\prvar$

$(\Not \qvar \c \Not \pvar)$ <= $(\pvar \Iff \pqvar \And \prvar \And \qvar)$;$\pqvar$,$\prvar$

$(\pvar \c \qvar \And \rvar \And \svar)$ <= $(\pvar \c \qvar)$,$(\pvar \c \rvar)$,$(\pvar \c \svar)$

\lineb

Establishing a Biconditional
\lineb

$(\pvar \Iff \qvar)$ <= $(\pvar \c \qvar)$,$(\Not\pqvar \c \Not\qvar)$

$(\pvar \Iff \qvar)$ <= $(\Not\pqvar \c \Not\qvar)$,$(\pvar \c \qvar)$

$(\qvar \Iff \pvar)$ <= $(\pvar \c \qvar)$,$(\Not\pqvar \c \Not\qvar)$

$(\qvar \Iff \pvar)$ <= $(\Not\pqvar \c \Not\qvar)$,$(\pvar \c \qvar)$

$(\pqvar \Iff \prvar)$<=$(\pvar \And \qvar \c \pqvar \Iff \prvar)$;$\pvar$,$\qvar$

\lineb



Justifying If and Only if Steps:
\lineb

$(\pvar \c \qvar \Iff \rvar)$ <= $(\pvar \And \qvar \c \rvar)$,$(\rvar \c \qvar)$

$(\pvar \c \qvar \Iff \rvar)$ <= $(\rvar \c \qvar)$,$(\pvar \And \qvar \c \rvar)$

$(\pvar \c \rvar \Iff \qvar)$ <= $(\pvar \And \qvar \c \rvar)$,$(\rvar \c \qvar)$

$(\pvar \c \rvar \Iff \qvar)$ <= $(\rvar \c \qvar)$,$(\pvar \And \qvar \c \rvar)$

$(\rvar \Or \pvar \Iff \rvar \Or \qvar)$ <= $(\pvar\Iff \qvar)$

$(\pvar \Or \rvar\Iff  \qvar\Or \rvar)$ <= $(\pvar\Iff \qvar)$

$(\pvar \Iff \pvar \And \qvar)$ <= $\qvar$

$(\prvar \Iff \prvar \And \qvar \And \rvar)$ <= $\qvar$,$\rvar$

$(\prvar \And \qvar\Iff \prvar)$ <= $\qvar$

$(\prvar \And \qvar \And \rvar\Iff\prvar)$ <= $\qvar$,$\rvar$

$(\pvar \Iff \qvar)$ <= $(\pvar \c \qvar)$,$(\qvar \c \pvar)$

$(\pvar \Iff \qvar)$ <= $(\qvar \c \pvar)$,$(\pvar \c \qvar)$

$(\pvar \Iff \qvar)$ <= $(\pvar \Iff \qvar \And\rvar)$;$\rvar$

$(\pvar \Iff \qvar)$ <= $(\pvar\And\rvar\Iff \qvar)$;$\rvar$

$(\qvar \Iff \pvar)$ <= $(\pvar \Iff \qvar \And\rvar)$;$\rvar$

$(\qvar \Iff \pvar)$ <= $(\pvar\And\rvar\Iff \qvar)$;$\rvar$

$(\pvar \Iff \pvar \And \qvar)$ <= $(\pvar \And \rvar \c \qvar)$; $\rvar$

$(\pvar \And \rvar \Iff \pvar \And \qvar \And \rvar)$ <= $(\pvar\And \svar\c \qvar)$; $\svar$
$(\pvar \And \rvar \Iff \qvar \And \rvar)$ <= $(\pvar\Iff\qvar)$

$(\pvar \And \rvar \Iff \qvar \And \rvar)$ <= $(\qvar\Iff\pvar)$

$(\pvar \And \qvar \And \rvar \Iff \pvar \And \rvar)$ <= $(\pvar\Iff\qvar)$

$(\pvar \And \qvar \And \rvar \Iff \pvar \And \rvar)$ <= $(\qvar\Iff\pvar)$

$(\pvar \And \rvar \Iff \pvar \And \qvar \And \rvar)$ <= $(\pvar\Iff\qvar)$

$(\pvar \And \rvar \Iff \pvar \And \qvar \And \rvar)$ <= $(\qvar\Iff\pvar)$

$(\pvar \And \qvar \And \rvar \Iff \pvar \And \qvar)$ <= $(\qvar \c \rvar)$

$(\pvar \And \qvar \Iff \pvar \And \qvar\And \rvar)$ <= $(\qvar \c \rvar)$

$(\pvar \Iff \qvar)$<=$(\pvar \Iff \rvar)$,$(\qvar \Iff \rvar)$

$(\pvar \Iff \qvar)$<=$(\pvar \Iff \rvar)$,$(\rvar \Iff \qvar)$

$(\qvar \Iff \pvar)$<=$(\rvar \Iff \pvar)$,$(\qvar \Iff \rvar)$

$(\qvar \Iff \pvar)$<=$(\rvar \Iff \pvar)$,$(\rvar \Iff \qvar)$


$(\pvar \Or \qvar \c\rvar)$ <= $(\pvar\c\rvar)$,$(\qvar\c\rvar)$

$(\pvar \c \rvar)$ <= $(\pvar \Or \qvar \c \rvar)$

$(\pvar \c \rvar)$ <= $(\qvar \Or \pvar \c \rvar)$

$(\rvar \Iff \qvar \And \rvar)$ <= $(\pvar \c \qvar)$ ; $\pvar$ 

$(\qvar \And \rvar \Iff \rvar)$ <= $(\pvar \c \qvar)$ ; $\pvar$ 

$(\rvar \Iff \qvar \And \rvar)$ <= $(\qvar \Iff \pvar)$;$\pvar$ 

$(\qvar \And \rvar \Iff \rvar)$ <= $(\qvar \Iff \pvar)$;$\pvar$ 

$(\rvar \Iff \qvar \And \rvar)$ <= $(\pvar \Iff \qvar)$;$\pvar$ 

$(\qvar \And \rvar \Iff \rvar)$ <= $(\pvar \Iff \qvar)$;$\pvar$ 

$(\pvar \Or \qvar \c \rvar)$<=$(\pvar\c\rvar)$,$(\qvar\c\rvar)$

$(\pvar \Iff \pvar \And \qvar)$ <= $(\pvar \And \rvar \c \qvar)$;$\rvar$

$(\Some x \pbar x \Iff \Some x \qbar x)$ <= $(\pbar a \Iff \qbar a \And \pvar)$ U $\pvar$

$(\Some x \pbar x \Iff \Some x \qbar x)$ <= $(\qbar a \And \pvar \Iff \pbar a)$ U $\pvar$

$(\pvar \And \Some x \qbar x \Iff \Some x (\pvar \And \qbar x))$ <= 

$( \Some x (\pvar \And \qbar x)\Iff\pvar \And \Some x \qbar x ) $ <= 

$(\pqvar \c \pvar \And \rvar \Iff\qvar\And \rvar)$ <= $(\qvar\Iff \pvar)$

$(\pqvar \c \pvar \And \rvar \Iff\qvar\And \rvar)$ <= $(\pvar\Iff \qvar)$

$(\pqvar \c \pvar \And \qvar \Iff\pvar)$ <= $(\pvar\c \qvar)$

$(\pqvar \c \pvar \Iff\qvar\And \pvar)$ <= $(\pvar\c \qvar)$

$(\pqvar \c \pvar \And \qvar \And \rvar\Iff\pvar\And \rvar)$ <= $(\pvar\c \qvar)$

$(\pqvar \c \pvar\And \rvar \Iff\qvar\And \pvar\And \rvar)$ <= $(\pvar\c \qvar)$

$(\pvar \And \qvar \Iff \pvar)$ <= $(\pvar \Iff \qvar)$

$(\pvar \And \qvar \Iff \pvar)$ <= $(\qvar \Iff \pvar)$

$(\pvar \And \rvar\Iff \pvar \And \qvar)$ <= $(\pvar \c \qvar \Iff \rvar)$

$(\pvar \And \rvar\Iff \pvar \And \qvar)$ <= $(\pvar \c \rvar \Iff \qvar)$

$(\pvar \And \rvar\Iff \qvar \And \rvar)$ <= $(\pvar \Iff \qvar \And \svar)$;$\svar$

$(\pvar \And \rvar\Iff \qvar \And \rvar)$ <= $(\qvar \And \svar\Iff \pvar)$;$\svar$

$(\qvar \And \rvar\Iff \pvar \And \rvar)$ <= $(\pvar \Iff \qvar \And \svar)$;$\svar$

$(\qvar \And \rvar\Iff \pvar \And \rvar)$ <= $(\qvar \And \svar\Iff \pvar)$;$\svar$

$(\pvar \And \qvar \And \rvar \Iff \pvar \And \qvar \And \svar)$ <= $(\pvar \c \rvar\Iff\svar)$

$(\pvar \And \qvar \And \rvar \Iff \pvar \And \qvar \And \svar)$ <= $(\pvar \c \svar\Iff\rvar)$
\lineb

Weakening a Biconditional

$(\pvar \c \qvar \Iff \rvar)$ <= $(\qvar \Iff \pvar \And \rvar)$

$(\pvar \c \qvar \Iff \rvar)$ <= $(\pvar \And \qvar \Iff \rvar)$

\lineb

Distributive Law

$((\ppvar \Or \pqvar )\And \pvar \Iff (\ppvar \And \pvar)\Or (\pqvar \And \pvar))$ <=

$((\ppvar \And \pvar)\Or (\pqvar \And \pvar)\Iff (\ppvar \Or \pqvar )\And \pvar )$ <=

$((\ppvar \Or \pqvar \Or \prvar)\And \pvar \Iff (\ppvar \And \pvar)\Or (\pqvar \And \pvar)\Or (\prvar \And \pvar))$ <=

$((\ppvar \And \pvar)\Or (\pqvar \And \pvar)\Or (\prvar \And \pvar)\Iff (\ppvar \Or \pqvar\Or \prvar )\And \pvar )$ <=

\lineb



Justifying Implications with And
\lineb

$(\pvar \c \pvar \And \qvar)$ <= $(\pvar \c \qvar)$

$(\pvar \c \pvar \And \qvar)$ <= $(\pvar \Iff \qvar)$

$(\pvar \c \pvar \And \qvar)$ <= $(\qvar \Iff \pvar)$

$(\pvar \And \qvar \c \rvar)$ <= $(\pvar \c \qvar \Iff \rvar)$

$(\pvar \And \qvar \c \rvar)$ <= $(\pvar \c \rvar \Iff \qvar)$

$(\pvar \And \rvar \c \qvar \And \rvar)$ <= $(\pvar\Iff \qvar)$

$(\pvar \And \rvar \c \pvar \And \qvar \And \rvar)$ <= $(\pvar\And \svar\c \qvar)$; $\svar$

$(\pvar \And \qvar \And \svar \c \pvar \And \rvar \And \svar)$ <= $(\pvar \And \qvar \c \rvar)$

$(\pvar \And \svar\c \rvar\And \svar)$ <= $(\pvar \And \qvar \c \rvar)$; $\qvar$

$(\pvar \And \qvar \c \pvar \And \qvar \And \rvar)$ <= $(\qvar \c \rvar)$

$(\pvar \And \qvar\c \pvar \And \qvar \And \rvar)$ <= $(\qvar \c \rvar)$ 

$(\pvar \c \pvar \And \qvar)$ <= $(\qvar \Iff \pqvar)$;$\pqvar$

$(\pvar \c \pvar \And \qvar)$ <= $(\pqvar \Iff \qvar)$;$\pqvar$

$(\pvar \c \pvar \And \qvar)$ <= $(\qvar \Iff \pqvar\And\prvar)$;$\pqvar$,$\prvar$

$(\pvar \c \pvar \And \qvar)$ <= $(\pqvar \And \prvar\Iff \qvar)$;$\pqvar$

$(\pvar \c \pvar \And \qvar)$ <= $(\qvar \Iff \pqvar\And\prvar \And\psvar  )$;$\pqvar$,$\prvar$,$\psvar$

$(\pvar \c \pvar \And \qvar)$ <= $(\pqvar \And \prvar \And \psvar \Iff \qvar)$;$\pqvar$,$\psvar$

$(\pvar \And \qvar \And \rvar)$ <= $\pvar$,$\qvar$,$\rvar$

$(\pvar \And \qvar \c \pvar \And (\qvar \Or \rvar))$ <=

$(\pvar \And \rvar \c \pvar \And (\qvar \Or \rvar))$ <=

$(\qvar \And \rvar \And \svar  \c \pvar \And \qvar \And \svar)$ <= $(\pvar \Iff \qvar \And \rvar)$

$(\qvar \And \rvar \And \svar  \c \pvar \And \qvar \And \svar)$ <= $(\qvar \And \rvar\Iff\pvar)$

\lineb

Justifying If and Only If steps containing Or

$(\pvar \Or \rvar \Iff \qvar \Or \rvar)$ <= $(\pvar \Iff \qvar)$

$(\pvar \Or \rvar \Iff \qvar \Or \rvar)$ <= $(\qvar \Iff \pvar)$

$(\rvar \Or \pvar \Iff \rvar \Or \qvar)$ <= $(\pvar \Iff \qvar)$

$(\rvar \Or \pvar \Iff \rvar \Or \qvar)$ <= $(\qvar \Iff \pvar)$

$(\pvar \Or \rvar \Iff \qvar \Or \rvar)$ <= $(\svar \c \pvar \Iff \qvar)$ ; $\svar$

$(\pvar \Or \rvar \Iff \qvar \Or \rvar)$ <= $(\svar \c \qvar \Iff \pvar)$ ; $\svar$

$(\rvar \Or \pvar \Iff \rvar \Or \qvar)$ <= $(\svar \c \pvar \Iff \qvar)$ ; $\svar$

$(\rvar \Or \pvar \Iff \rvar \Or \qvar)$ <= $(\svar \c \qvar \Iff \pvar)$ ; $\svar$


$(\pvar \Or \pqvar  \Iff \qvar \Or \pqvar)$ <= $(\pvar \Iff \qvar \And \rvar)$;$\rvar$

$(\qvar \Or \pqvar  \Iff \pvar \Or \pqvar)$ <= $(\pvar \Iff \qvar \And \rvar)$;$\rvar$

$(\pqvar \Or \pvar  \Iff \pqvar \Or \qvar)$ <= $(\pvar \Iff \qvar \And \rvar)$;$\rvar$

$(\pqvar \Or \qvar  \Iff \pqvar \Or \pvar)$ <= $(\pvar \Iff \qvar \And \rvar)$;$\rvar$
\lineb

Disjunctions
\lineb

$(\pvar \Or \qvar)$ <= $(\qvar \Or \pvar)$

$(\qvar \Or \rvar)$<= $(\pvar \c \qvar)$;$(\pvar \Or \rvar)$

$(\qvar \Or \rvar)$<= $(\pvar \c \qvar)$,$(\Not\pvar \c \rvar)$

$(\qvar \Or \rvar)$<= $(\Not\pvar \c \qvar)$,$(\pvar \c \rvar)$

$(\Not \pvar \Or \qvar \c \qvar)$<= $\pvar$

$(\pvar \Or \qvar \c \qvar)$<= $\Not \pvar$

$(\qvar \Or \Not \pvar \c \qvar)$<= $\pvar$

$(\qvar \Or \pvar \c \qvar)$<= $\Not \pvar$

\lineb

Ternary Disjunction
\lineb

$(\pvar \Or (\qvar \Or \rvar) \c \pvar \Or \qvar \Or \rvar)$<=
\lineb

Existential Quantifier Dropping using Equality
\lineb

$(\Some x (x = y \And \pbar x) \c \pbar y)$<=

$(\Some x (y = x \And \pbar x) \c \pbar y)$<=

Existential Quantifier Dropping inside a Disjunction with Equality
\lineb

$(\pvar \Or \Some x (x = y \And \pbar x) \c \pvar \Or \pbar y)$<=

$(\Some x (x = y \And \pbar x)\Or \pvar \c \pbar y \Or \pvar)$<=

$(\pvar \Or \Some x (y = x \And \pbar x) \c \pvar \Or \pbar y)$<=

$(\Some x (y = x \And \pbar x)\Or \pvar \c \pbar y \Or \pvar)$<=

Disjunctive Hypotheses
\lineb

$(\pvar \c \qvar)$ <= $(\pvar \And (\pqvar \Or \prvar) \c \qvar)$; $\pqvar$

$(\pvar \c \qvar)$ <= $(\pvar \And (\pqvar \Or \prvar) \c \qvar)$; $\prvar$

$(\pqvar \c \qvar)$ <= $(\pvar \And (\pqvar \Or \prvar) \c \qvar)$; $\pvar$

$(\prvar \c \qvar)$ <= $(\pvar \And (\pqvar \Or \prvar) \c \qvar)$; $\pvar$
\lineb


Negation
\lineb

$\pvar$<= $(\Not\pvar \c \pvar)$

$\Not \pvar $ <= $(\pvar \c \false)$

$\pvar $ <= $(\Not \pvar \c \false)$

$\Not\pvar$<= $(\pvar \c \Not\pvar)$

$(\pvar \c \false)$ <= $\Not \pvar$

$(\pvar \c \false)$ <= $(\qvar \c \Not \pvar)$;$\qvar$

$(\pvar \c \pvar \And \Not \qvar )$ <= $( \qvar \c \false)$

$(\Not \qvar \And \rvar \c \Not \pvar \And \rvar)$ <= $(\pvar \c \qvar)$

$(\Not \pvar \c \false)$ <= $\pvar$

$(\Not \pvar \c \false)$ <= $(\qvar \c \pvar)$;$\qvar$

$(\pvar \c \qvar)$ <= $(\Not \qvar \c \Not \pvar)$

$(\Not \pvar \c \Not \qvar)$ <= $(\qvar \c \pvar)$

$(\rvar \And \pvar \c \qvar)$ <= $(\rvar \And \Not \qvar \c \Not \pvar)$

$(\Not \rvar \c \Not \qvar)$ <= $(\pvar\And\qvar\c\rvar)$;$\pvar$

$(\Not \pvar \c \Not \qvar)$<= $(\pvar \Iff \qvar \And \rvar)$; $\rvar$

$(\Not \qvar \c \Not \pvar)$<= $(\pvar \Iff \qvar \And \rvar)$; $\rvar$

$(\false \c \pvar)$ <=

$(\Not \Not \pvar \c \pvar)$ <=

$(\Not \pvar \And (\pvar \Or \qvar) \c \qvar)$ <=

$(\Not \pvar \And (\qvar \Or \pvar) \c \qvar)$ <=

$\qvar$ <=  $(\pvar \And \ppvar\c \qvar)$;$\pvar$,$\ppvar$

$\qvar$ <=  $(\pvar \And \ppvar \And \pqvar\c \qvar)$;$\pvar$,$\ppvar$,$\pqvar$

$(\pvar \c \qvar)$ <= $(\pvar \Iff \qvar)$

$(\qvar \c \pvar)$ <= $(\pvar \Iff \qvar)$

$(\pvar \And \rvar\c \qvar\And \rvar)$ <= $(\pvar \Iff \qvar)$

$(\qvar \And \rvar\c \pvar\And \rvar)$ <= $(\pvar \Iff \qvar)$

$(\pvar \c \qvar)$ <= $(\pvar \Iff \qvar \And \rvar)$

$(\pvar \c \qvar)$ <= $(\qvar \And \rvar\Iff \pvar)$

$(\ppvar \And \qvar)$ <=  $\ppvar$,$\qvar$ 

$\ppvar $ <= $(\ppvar \And \qvar)$ 

$(\Not \pvar \And \rvar \c \Not \qvar \And \rvar)$ <= $(\pvar \Iff \qvar)$

$(\Not \pvar \And \rvar \c \Not \qvar \And \rvar)$ <= $(\qvar \Iff \pvar)$

$(\Not \pvar \And \rvar \Iff \Not \qvar \And \rvar)$ <= $(\pvar \Iff \qvar)$

$(\Not \pvar \And \rvar \Iff \Not \qvar \And \rvar)$ <= $(\qvar \Iff \pvar)$

$(\pvar \And \Not \pvar \c \false)$ <=

$(\pvar \And \qvar \c \pvar \And \Not\rvar)$ <= $(\rvar \c \Not \qvar)$

$\false$ <= $\pvar $,$\Not\pvar$

$\false$ <= $\Not\pvar $,$\pvar$

$\Not\pvar $<= $(\pvar \Iff \qvar)$;$\Not\qvar$

$\Not\pvar $<= $(\qvar \Iff \pvar)$;$\Not\qvar$

$(\Not\pvar \c\qvar )$<=$(\pvar \Iff \Not\qvar \And \rvar)$;$\rvar$

$\pvar$ <= $\Not \Not \pvar$

$\Not \Not \pvar$ <= $\pvar$

$(\pvar \And \qvar)$ <= $(\Not \Not \pvar \And \qvar)$

$(\Not \Not \pvar \And \qvar)$ <= $(\pvar \And \qvar)$

$(\pvar \And \qvar \c \Not \Not \pvar \And \qvar)$ <= 

$(\Not \Not \pvar \And \qvar \c \pvar \And \qvar)$ <= 

$(\Not (\pvar \And \qvar) \c \Not \pvar \Or \Not \qvar)$ <=

$(\Not (\pvar \And \qvar \And \rvar) \c \Not \pvar \Or \Not \qvar \Or \Not \rvar)$ <=

\lineb

Justifying Implications of Biconditionals
\lineb

$(\pvar \Iff \qvar \c \pvar \Iff \rvar)$ <= $(\qvar \Iff \rvar)$

$(\pvar \Iff \qvar \c \pvar \Iff \rvar)$ <= $(\rvar \Iff \qvar)$

$(\qvar \Iff \pvar \c \rvar \Iff \pvar)$ <= $(\qvar \Iff \rvar)$

$(\qvar \Iff \pvar \c \rvar \Iff \pvar)$ <= $(\rvar \Iff \qvar)$

$(\pvar \Iff \qvar)$ <= $(\qvar \Iff \pvar)$

$(\pvar \Iff \rvar \c \qvar \Iff \rvar)$ <= $(\pvar \Iff \qvar)$

$(\pvar \Iff \rvar \c \qvar \Iff \rvar)$ <= $(\qvar \Iff \pvar)$

$(\rvar \Iff \pvar \c\rvar \Iff \qvar)$ <= $(\pvar \Iff \qvar)$

$(\rvar \Iff \pvar \c\rvar \Iff  \qvar )$ <= $(\qvar \Iff \pvar)$

$(\pvar \Iff \rvar \c \qvar \Iff \rvar)$ <= $(\pqvar \c\pvar \Iff \qvar)$ ; $\pqvar$

$(\pvar \Iff \rvar \c \qvar \Iff \rvar)$ <= $(\pqvar \c\qvar \Iff \pvar)$ ; $\pqvar$

$(\rvar \Iff \pvar \c\rvar \Iff \qvar)$ <= $(\pqvar \c\pvar \Iff \qvar)$ ; $\pqvar$

$(\rvar \Iff \pvar \c\rvar \Iff  \qvar )$ <= $(\pqvar \c\qvar \Iff \pvar)$ ; $\pqvar$

$(\pvar \And \qvar \Iff \prvar)$ <= $(\pvar \c \qvar)$

$(\pvar \Iff \pvar\And \qvar)$ <= $(\pvar \c \qvar)$

$(\pvar \And \qvar \And \rvar\Iff \prvar\And \rvar)$ <= $(\pvar \c \qvar)$

$(\pvar\And \rvar \Iff \pvar\And \qvar\And \rvar )$ <= $(\pvar \c \qvar)$

$(\true \c \ppvar)$ <= $(\qpvar \And \rvar\Iff \ppvar)$; $\qpvar$,$\rvar$

$(\true \c \ppvar)$ <= $(\ppvar \Iff \qpvar\And\rvar)$; $\qpvar$,$\rvar$

$(\true \c \ppvar)$ <= $(\qpvar \Iff \ppvar)$; $\qpvar$

$(\true \c \ppvar)$ <= $(\ppvar \Iff \qpvar)$; $\qpvar$

$(\true \c \ppvar )$ <=  $\ppvar$

$(\true \c \qvar) $ <=  $(\ppvar \c \qvar)$; $\ppvar$ 

$(\true \c \qvar) $ <=  $(\ppvar \And \prvar \c \qvar)$; $\ppvar$ , $\prvar$

$(\true \c \qpvar) $ <=  $(\ppvar \And \pqvar \And \prvar\c\qpvar)$; $\ppvar$ , $\pqvar$, $\prvar$

$(\true \c \qvar) $ <=  $(\ppvar \And \pqvar \And \prvar\And \psvar \c \qvar)$; $\ppvar$ , $\pqvar$, $\prvar$, $\psvar$

$(\true \c \ppvar \And \qvar)$ <=  $\ppvar$,$\qvar$ 

$(\ppvar \c \qvar \And \rvar)$ <= $(\ppvar\c\qvar)$, $\rvar$

$(\ppvar \c \ppvar \And \qvar)$ <=  $\qvar$

$(\ppvar \c \ppvar \And \qvar\And\rvar)$ <=  $\qvar$,$\rvar$

$(\ppvar \c \ppvar \And \qvar\And\rvar \And \svar)$ <=  $\qvar$,$\rvar$,$\svar$

$(\rvar \And \svar \And \pvar \c \qvar \And \rvar)$ <= $(\pvar \c \qvar)$

$(\rvar \And \svar \And \pvar \c \qvar \And \rvar)$ <= $(\pvar \And \ppvar \c \qvar)$ ; $\ppvar$

$(\rvar \And \svar \And \pvar \c \qvar \And \rvar)$ <= $(\pvar \And \ppvar \And \pqvar \c \qvar)$ ; $\ppvar$ , $\pqvar$

$(\rvar \And \svar \And \pvar \c \qvar \And \rvar)$ <= $(\pvar \And \ppvar \And \pqvar \And \prvar \c \qvar)$ ; $\ppvar$ , $\pqvar$ , $\prvar$

$(\rvar \And \svar \And \pvar \c \qvar \And \rvar)$ <= $(\pvar \And \ppvar \And \pqvar \And \prvar \And \psvar \c \qvar)$ ; $\ppvar$ , $\pqvar$ , $\prvar$ ,$\psvar$

$(\prvar \And \qvar \c \rvar)$ <= $(\prvar \c \rvar)$

$(\prvar \And \qvar \c \rvar)$ <= $(\prvar \c \qvar \Iff \rvar)$

$(\prvar \And \qvar \And \svar \c \rvar \And \svar )$ <= $(\pvar \c \qvar \Iff \rvar)$

$(\prvar \And \qvar \c \rvar)$ <= $(\pvar \c \qvar \Iff \rvar)$

$(\pqvar \And \qvar \And \svar \c \rvar \And \svar )$ <= $(\pvar \c \qvar \Iff \rvar)$ ; $\pvar$

$(\pvar \And \rvar \c \qvar \And \rvar)$ <= $(\pvar \c \qvar)$

$(\pvar \And \rvar \Iff \qvar \And \rvar)$ <= $(\svar\c\pvar\Iff\qvar)$; $\svar$

$(\pvar \And \rvar \c \qvar \And \rvar)$ <= $(\svar\c\pvar\Iff\qvar)$; $\svar$

$(\pvar \c \qvar \And \rvar)$ <= $(\pvar \c \qvar)$ + $(\pvar \c \rvar)$

$(\pqvar \And \prvar\c \qvar \And \rvar)$ <= $(\pqvar \c \qvar)$ + $(\prvar \c \rvar)$

$(\pvar \c \qvar \And \rvar \And \pvar)$ <= $(\pvar \c \qvar)$ + $(\pvar \c \rvar)$

The following three lines have two conclusions:

$(\prvar \And \qrvar\c\rvar \And \svar)$  $(\psvar \And \qsvar\c \rvar \And \svar)$ <= $(\prvar\c \rvar)$ + $(\qrvar \c \svar)$

$(\prvar \And \qrvar\c\rvar \And \svar)$  $(\psvar \And \qsvar\c \rvar \And \svar)$ <= $(\prvar\Iff\rvar)$ + $(\psvar\Iff\svar)$

$(\prvar \And \qrvar\c\rvar \And \svar)$  $(\psvar \And \qsvar\c \rvar \And \svar)$ <= $(\rvar\Iff\prvar)$ + $(\svar\Iff\psvar)$
\lineb 

Transitive Implications

$(\pvar \c \svar)$ <= $(\pvar \c \qvar)$ - $(\pvar \c \rvar)$ ;$(\qvar \And \rvar \c \svar)$

$\rvar$ <= $\pvar$ - $\qvar$ ; $(\pvar \And \qvar \c \rvar)$

$(x \ident z)$ <= $(x \ident y)$ - $(y \ident z)$

$(x = z)$ <= $(x \ident y)$ - $(y = z)$

$(x = z)$ <= $(x = y)$ - $(y \ident z)$

$(\pvar \c \rvar)$ <= $(\pvar\c\qvar)$ - $(\qvar\c\rvar)$

$(\pvar \c \rvar)$ <= $(\pvar\Iff\qvar)$ - $(\qvar\c\rvar)$

$(\pvar \c \rvar)$ <= $(\qvar\Iff\pvar)$ - $(\qvar\c\rvar)$

$(\pvar \c \rvar)$ <= $(\pvar\c\qvar)$ - $(\qvar\Iff\rvar)$

$(\pvar \c \rvar)$ <= $(\pvar\c\qvar)$ - $(\rvar\Iff\qvar)$

$(\pvar \c \rvar)$ <= $(\pvar\Iff\qvar)$ - $(\qvar\Iff\rvar)$

$(\pvar \c \rvar)$ <= $(\pvar\Iff\qvar)$ - $(\rvar\Iff\qvar)$

$(\pvar \c \rvar)$ <= $(\qvar\Iff\pvar)$ - $(\qvar\Iff\rvar)$

$(\pvar \c \rvar)$ <= $(\qvar\Iff\pvar)$ - $(\rvar\Iff\qvar)$

$(x = z)$ <= $(x =  y)$ - $(y \ident z)$

$(x = z)$ <= $(x \ident y)$ - $(y = z)$

$(x \ident z)$ <= $(x \ident y)$ - $(y \ident z)$

$(\pvar \c \rvar)$<= $(\pvar \c \qvar)$ - $(\qvar \Iff \rvar \And \prvar)$

$(\pvar \c \rvar)$<= $(\pvar \Iff \qvar \And \pqvar)$ - $(\qvar \c \rvar)$

$(\pvar \c\rvar )$<=$(\qvar \And \pqvar\Iff \pvar)$-$(\qvar \c \rvar)$

$(\rvar \And \pvar \c \rvar \And \qvar)$<=$(\pvar \c \pqvar)$-$(\pqvar\Iff \qvar)$

$(\rvar \And \pvar \c \rvar \And \qvar)$<=$(\pvar \c \pqvar)$-$(\qvar\Iff \pqvar)$

$(\rvar \And \pvar \c \rvar \And \qvar)$<=$(\pvar \Iff \pqvar \And \prvar)$-$(\pqvar\Iff \qrvar \And \qvar)$

$(\rvar \And \pvar \c \rvar \And \qvar)$<=$(\pvar \c \pqvar)$-$(\pqvar\Iff \qrvar \And \qvar)$

$(\rvar \And \pvar \c \rvar \And \qvar)$<=$(\pvar \Iff \pqvar \And \prvar)$-$(\pqvar\c\qvar)$

$(\pvar \Iff \rvar)$ <= $(\pvar\Iff\qvar)$ - $(\qvar\Iff\rvar)$

$(\pvar \Iff \rvar)$ <= $(\pvar\Iff\qvar)$ - $(\rvar\Iff\qvar)$

$(\pvar \c \pvar\And \rvar)$<= $(\pvar \c \qvar)$-$(\qvar \c \rvar)$

$(\pvar \c \rvar)$ <= $(\pvar \c \pqvar \Or\prvar)$-$(\pqvar \c \rvar)$,$(\prvar \c \rvar)$
\lineb

$(\pvar \c \pbar x)$ <= $(\pvar \c x \ident y)$ - $(\pvar \c \pbar y)$

$(\pvar \c \pbar x)$ <= $(\pvar \c x = y)$ -  $(\pvar \c \pbar y)$

$(\pvar \c \pbar z)$ <= $(\pvar \c \pbar y)$ - $(\pvar \c y = z)$

$(\pvar \c \pbar z)$ <= $(\pvar \c \pbar y)$ - $(\pvar \c y \ident z)$

$\pbar x$ <= $(x \ident y)$ - $\pbar y$

$\pbar x$ <= $(x = y)$ -  $\pbar y$

$\pbar z$ <= $\pbar y$ - $(y = z)$

$\pbar z$ <= $\pbar y$ - $(y \ident z)$


Double Transitive Implications
\lineb


$(\pvar \c \qvar)$<= $(\pvar \c \pqvar)$ - $(\pqvar \c \prvar)$ - $(\prvar \c \qvar)$

$(\pvar \c \qvar)$<= $(\pvar \Iff \pqvar)$ - $(\pqvar \c \prvar)$ - $(\prvar \c \qvar)$

$(\pvar \c \qvar)$<= $(\pvar \c \pqvar)$ - $(\pqvar \Iff \prvar)$ - $(\prvar \c \qvar)$

$(\pvar \c \qvar)$<= $(\pvar \c \pqvar)$ - $(\pqvar \c \prvar)$ - $(\prvar \Iff \qvar)$

$(\pvar \c \qvar)$<= $(\pqvar \Iff \pvar)$ - $(\pqvar \c \prvar)$ - $(\prvar \c \qvar)$

$(\pvar \c \qvar)$<= $(\pvar \c \pqvar)$ - $(\prvar \Iff \pqvar)$ - $(\prvar \c \qvar)$

$(\pvar \c \qvar)$<= $(\pvar \c \pqvar)$ - $(\pqvar \c \prvar)$ - $(\qvar \Iff \prvar)$

$(\pvar \c \qvar)$<= $(\pvar \Iff \pqvar)$ - $(\pqvar \Iff \prvar)$ - $(\prvar \Iff \qvar)$

$(\pvar \c \qvar)$<= $(\pqvar \Iff \pvar)$ - $(\pqvar \Iff \prvar)$ - $(\prvar \c \qvar)$

$(\pvar \c \qvar)$<= $(\pqvar \Iff \pvar)$ - $(\prvar \Iff \pqvar)$ - $(\prvar \c \qvar)$

$(\pvar \c \qvar)$<= $(\pvar \Iff \pqvar)$ - $(\pqvar \Iff \prvar)$ - $(\prvar \c \qvar)$

$(\pvar \c \qvar)$<= $(\pvar \Iff \pqvar)$ - $(\prvar \Iff \pqvar)$ - $(\prvar \c \qvar)$

$(\pvar \c \qvar)$<= $(\pqvar \Iff \pvar)$ - $(\pqvar \c \prvar)$ - $(\prvar \Iff \qvar)$

$(\pvar \c \qvar)$<= $(\pqvar \Iff \pvar)$ - $(\pqvar \c \prvar)$ - $(\qvar \Iff \prvar)$

$(\pvar \c \qvar)$<= $(\pvar \Iff \pqvar)$ - $(\pqvar \c \prvar)$ - $(\prvar \Iff \qvar)$

$(\pvar \c \qvar)$<= $(\pvar \Iff \pqvar)$ - $(\pqvar \c \prvar)$ - $(\qvar \Iff \prvar)$

$(\pvar \c \qvar)$<= $(\pvar \c \pqvar)$ - $(\prvar \Iff \pqvar)$ - $(\prvar \Iff \qvar)$

$(\pvar \c \qvar)$<= $(\pvar \c \pqvar)$ - $(\prvar \Iff \pqvar)$ - $(\qvar \Iff \prvar)$

$(\pvar \c \qvar)$<= $(\pvar \c \pqvar)$ - $(\pqvar \Iff \prvar)$ - $(\prvar \Iff \qvar)$

$(\pvar \c \qvar)$<= $(\pvar \c \pqvar)$ - $(\pqvar \Iff \prvar)$ - $(\qvar \Iff \prvar)$

\lineb

Context Shedding
\lineb

$(\pvar \Iff \qvar)$ <= $(\rvar \c \pvar \Iff \qvar)$ ! $(\pvar\c\rvar)$,$(\qvar \c \rvar)$ 

$(\pvar \Iff \qvar)$ <= $(\rvar \c \pvar \Iff \qvar)$ ! $(\qvar\c\rvar)$,$(\pvar \c \rvar)$ 

$(\pvar \Iff \qvar \And \rvar)$ <= $(\rvar \c \pvar\Iff\qvar)$ ! $(\pvar \c \rvar)$

$(\qvar \And \rvar\Iff \pvar)$ <= $(\rvar \c \qvar\Iff\pvar)$ ! $(\pvar \c \rvar)$ 

$(\pvar \Iff \qvar \And \rvar)$ <= $(\rvar \c \qvar\Iff\pvar)$ ! $(\pvar \c \rvar)$ 

$(\pvar \Iff \qvar \And \rvar)$ <= $(\rvar \c \pvar\Iff\qvar)$ ! $(\pvar \c \rvar)$ 

$(x \ident y)$ <=  $(\pvar \c x \ident y)$ ! $(\ex x \c \pvar)$, $(\ex y \c \pvar)$ 

$(x \ident y)$ <=  $(\pvar \c x  = y)$ ! $(\ex x \c \pvar)$, $(\ex y \c \pvar)$ 

$(\pvar \c \qvar)$ <= $(\rvar \And\pvar\c\qvar)$ ! $(\pvar \c \rvar)$ 

$(x \ident y)$ <= $(\ex x \c x \ident y)$,$(\ex y \c x \ident y)$

$(x \ident y)$ <= $(\ex y \c x \ident y)$,$(\ex x \c x \ident y)$
\lineb

Identity and Equality Substitutions
\lineb

$(x \ident y \c \ubar x \ident \ubar y)$ <= 

$(y \ident x \c \ubar x \ident \ubar y)$ <= 

$(y = x \c \ubar x \ident \ubar y)$ <=

$(x = y \c \ubar x \ident \ubar y)$ <=

$\pbar t$ <= $(t = u)$, $\pbar u$ 

$\pbar t$ <= $(u = t)$, $\pbar u$ 

$\pbar t$ <=  $\pbar u$, $(t = u)$

$\pbar t$ <=  $\pbar u$, $(u = t)$

$(t = u \c \pbar t)$ <= $\pbar u$ 

$(u = t \c \pbar t)$ <= $\pbar u$ 

$\pbar t$ <=  $(\pbar u \And t = u)$

$\pbar t$ <=  $(\pbar u \And u = t)$

$(y = x \And \pbar x \c \pbar y)$ <=

$(y = x \And \pbar x \c y = x \And \pbar y)$ <=

$(x = y \And \pbar x \c \pbar y)$ <=

$(\pbar v \And u = v \c \pbar u)$ <=

$(x = y \And \pbar x \c x = y \And \pbar y)$ <=

$(\pvar \And y = x \And \pbar x \c \pvar \And y = x \And \pbar y)$ <=

$(\pvar \c \pvar \And \pbar t)$ <= $(t = u)$, $\pbar u$ 

$(\pvar \c \pvar \And \pbar t)$ <= $\pbar u$, $(t = u)$

$(\pbar y \c \pbar x)$ <= $(\pvar \And \qvar \c x = y)$; $\pvar$,$\qvar$

$(\pbar x \c \pbar y)$ <= $(\pvar \And \qvar \c x = y)$; $\pvar$,$\qvar$

$(\pbar u \c \pbar t)$ <= $(\pvar\And\qvar \c t \ident u)$ ; $\pvar$,$\qvar$

$(\pbar u \c \pbar t)$ <= $(\pvar\And\qvar \c u \ident t)$ ; $\pvar$,$\qvar$

$(x = y \c \pbar y)$ <= $(\pvar \And \qvar \c \pbar x)$; $\pvar$,$\qvar$

$(y = x \c \pbar y)$ <= $(\pvar \And \qvar \c \pbar x)$; $\pvar$,$\qvar$

$(\pbar u \c \pbar t)$ <= $(\pvar\And\qvar \And \rvar \c t \ident u)$ ; $\pvar$,$\qvar$,$\rvar$

$(\pbar u \c \pbar t)$ <= $(\pvar\And\qvar \And \rvar \c u \ident t)$ ; $\pvar$,$\qvar$,$\rvar$

$(\ubar x \ident \ubar y)$ <= $(\pvar \And \qvar \And \rvar \And \svar \c x=y)$;$\pvar$,$\qvar$,$\rvar$,$\svar$

$(\ubar x \ident \ubar y)$ <= $(\pvar \And \qvar \And \rvar \And \svar \c y=x)$;$\pvar$,$\qvar$,$\rvar$,$\svar$

$(\pvar \And \pbar u \c \pvar \And \pbar t)$ <= $(\pvar\And\qvar \c t \ident u)$ ; $\qvar$

$(\pvar \And \pbar u \c \pvar \And \pbar t)$ <= $(\pvar\And\qvar \c u \ident t)$ ; $\qvar$

$(\pbar u \c \pbar t)$ <= $(\pvar \c t \ident u)$ ; $\pvar$

$(\pbar u \c \pbar t)$ <= $(\pvar \c u \ident t)$ ; $\pvar$

$(\pbar u \c \pbar t)$ <= $(\pvar \c t = u)$ ; $\pvar$

$(\pbar u \c \pbar t)$ <= $(\pvar \c u = t)$ ; $\pvar$

$(\pbar u \c \pbar t)$ <= $(\pvar \Iff t \ident u)$ ; $\pvar$

$(\pbar u \c \pbar t)$ <= $(\pvar \Iff u \ident t)$ ; $\pvar$

$(\pbar u \c \pbar t)$ <= $(\pvar \Iff t = u)$ ; $\pvar$

$(\pbar u \c \pbar t)$ <= $(\pvar \Iff u = t)$ ; $\pvar$

$\pbar t$ <= $(\pvar \c t = u)$; $\pvar$,$\pbar u$

$\pbar t$ <= $(\pvar \c u = t)$; $\pvar$,$\pbar u$

$\pbar t$ <= $(\pvar \c t = u)$; $\pbar u$,$\pvar$

$\pbar t$ <= $(\pvar \c u = t)$; $\pbar u$,$\pvar$

$(\pvar \c \ubar u \ident \ubar t)$ <= $(t = u)$ 

$(\pvar \c \ubar u \ident \ubar t)$ <= $(u =  t)$ 

$(\pvar \c \ubar u \ident \ubar t)$ <= $(t \ident u)$ 

$(\pvar \c \ubar u \ident \ubar t)$ <= $(u \ident t)$ 

$(\ubar u \ident \ubar t)$ <= $(\pvar \c t \ident u)$ ;$\pvar$

$(\ubar u \ident \ubar t)$ <= $(\pvar \c u \ident t)$ ;$\pvar$

$(\qvar \c \ubar x \ident \ubar y)$ <= $(\pvar \c x = y)$;$\pvar$

$(\qvar \c \ubar x \ident \ubar y)$ <= $(\pvar \Iff x = y)$; $\pvar$

$(\qvar \c \ubar x \ident \ubar y)$ <= $(\pvar \Iff y = x)$; $\pvar$

$(\qvar \c \ubar x \ident \ubar y)$ <= $( y = x\Iff \pvar)$; $\pvar$

$(\qvar \c \ubar x \ident \ubar y)$ <= $( x = y\Iff \pvar)$; $\pvar$

$(\ubar u \ident \ubar t)$ <= $(\pvar \And \qvar \c t \ident u)$ ;$\pvar$, $\qvar$

$(\ubar u \ident \ubar t)$ <= $(\pvar \And \qvar \c u \ident t)$ ;$\pvar$, $\qvar$

$(\ubar u \ident \ubar t)$ <= $(\pvar \And \qvar\And \rvar \c t \ident u)$ ;$\pvar$, $\qvar$,$\rvar$

$(\ubar u \ident \ubar t)$ <= $(\pvar \And \qvar\And \rvar \c u \ident t)$ ;$\pvar$, $\qvar$,$\rvar$

$(t \ident u \c \pbar t \Iff \pbar u)$ <=

$(u \ident t \c \pbar t \Iff \pbar u)$ <=

$(\ubar u \ident \ubar t)$ <= $(t \ident u)$

$(\ubar u \ident \ubar t)$ <= $(u \ident t)$

$(\ubar u \ident \ubar t)$ <= $(\pvar \c t = u)$ ;$\pvar$

$(\ubar u \ident \ubar t)$ <= $(\pvar \c u = t)$ ;$\pvar$

$(\ubar x \ident \ubar y)$ <= $(\pvar \Iff x = y)$;$\pvar$

$(\ubar x \ident \ubar y)$ <= $(\pvar \Iff y = x)$;$\pvar$

$(\ubar x \ident \ubar y)$ <= $(x = y\Iff \pvar)$;$\pvar$

$(\ubar x \ident \ubar y)$ <= $(y = x\Iff \pvar)$;$\pvar$

$(\ubar u \ident \ubar t)$ <= $(\pvar\And\qvar \c t = u)$ ;$\pvar$,$\qvar$

$(\ubar u \ident \ubar t)$ <= $(\pvar \And \qvar\c u = t)$ ;$\pvar$,$\qvar$

$(\pbar u \Iff \pbar t)$ <= $(\pvar\And\qvar \c t \ident u)$ ;$\pvar$,$\qvar$

$(\pbar u \Iff \pbar t)$ <= $(\pvar \And \qvar\c u \ident t)$ ;$\pvar$,$\qvar$

$(\pbar u \Iff \pbar t)$ <= $(\pvar\c t \ident u)$ ;$\pvar$

$(\pbar u \Iff \pbar t)$ <= $(\pvar \c u \ident t)$ ;$\pvar$

$(\pbar u \Iff \pbar t)$ <= $(\pvar\And\qvar \c t = u)$ ;$\pvar$,$\qvar$

$(\pbar u \Iff \pbar t)$ <= $(\pvar \And \qvar\c u = t)$ ;$\pvar$,$\qvar$

$(\pbar u \Iff \pbar t)$ <= $(\pvar\c t = u)$ ;$\pvar$

$(\pbar u \Iff \pbar t)$ <= $(\pvar \c u = t)$ ;$\pvar$

$(\pbar x \c \pbar y)$ <= $(\pvar \c x = y)$;$\pvar$

$(\pbar x \c \pbar y)$ <= $(\pvar \c y = x)$;$\pvar$

$(\pbar x \c \pbar y)$ <= $(\pvar \c x = y \Iff \qvar)$;$\pvar$, $\qvar$

$(\pbar x \c \pbar y)$ <= $(\pvar \c y = x \Iff \qvar)$;$\pvar$, $\qvar$

$(\pbar x \c \pbar y)$ <= $(\pvar \c x = y \Iff \qvar)$;$\qvar$, $\pvar$

$(\pbar x \c \pbar y)$ <= $(\pvar \c y = x \Iff \qvar)$;$\qvar$, $\pvar$

$(\qvar \And \pbar x \c \qvar \And \pbar y)$<= $(\qvar \c x = y)$

$(\qvar \And \pbar x \c \qvar \And \pbar y)$<= $(\qvar \c y = x)$

$(\ubar u \ident \ubar t)$ <= $(\pvar\And\qvar\And\rvar \c t = u)$ ;$\pvar$,$\qvar$,$\rvar$

$(\ubar u \ident \ubar t)$ <= $(\pvar \And \qvar\And\rvar\c u = t)$ ;$\pvar$,$\qvar$,$\rvar$

$(\ubar u \ident \ubar t)$ <= $(t = u)$

$(\ubar u \ident \ubar t)$ <= $(u = t)$

$(\pbar u \c \pbar t)$ <= $(t \ident u)$ 

$(\pbar u \c \pbar t)$ <= $(u \ident t)$ 

$(\pbar u \c \pbar t)$ <= $(t = u)$ 

$(\pbar u \c \pbar t)$ <= $(u = t)$ 

$(\vbar x \ident \vbar y)$ <= $(x = y)$

$(\vbar x \ident \vbar y)$ <= $(y = x)$

$(x = y \c \pbar x \Iff \pbar y)$<= 

$(y = x \c \pbar x \Iff \pbar y)$<= 

$(\pbar t \Iff \pbar u)$ <= $(t \ident u)$

$(\pbar t \Iff \pbar u)$ <= $(u \ident t)$

$(\pbar t \Iff \pbar u)$ <= $(t = u)$

$(\pbar t \Iff \pbar u)$ <= $(u = t)$

$\pbar t$ <= $\pbar u$,  $(t \ident u)$

$\pbar t$ <= $\pbar u$, $(u \ident t)$

$\pbar t$ <= $(t \ident u)$, $\pbar u$ 

$\pbar t$ <= $(u \ident t)$, $\pbar u$ 

$(t \ident u \c \pbar t)$ <= $\pbar u$ 

$(u \ident t \c \pbar t)$ <= $\pbar u$ 

$\pbar x$ <= $(x \ident \an s \pbar s)$, $\Some s \pbar s$

$\pbar x$ <=  $\Some s \pbar s$,$(x \ident \an s \pbar s)$

$\pbar x$ <= $(x \ident \The s \pbar s)$, $\One s \pbar s$

$\pbar x$ <=  $\One s \pbar s$,$(x \ident \The s \pbar s)$

$(\One s \pbar s \c \pbar x)$ <= $(x \ident \The s \pbar s)$

$\pbar y$ <= $(y  =  \The x\pbar x)$

$(y = \The x \pbar x \c \pbar y)$ <=

$(\pvar\And\pbar x\And\Not \pbar y \c \pvar \And \Not (x = y))$ <=

$(\pvar\And\pbar x\And\Not \pbar y \c \pvar \And \Not (y = x))$ <=

$(x = y \c \pbar x )$ <= $(\pvar \c \pbar y)$; $\pvar$

$(y = x \c \pbar x )$ <= $(\pvar \c \pbar y)$; $\pvar$

$(x = y \And \pvar \c \pbar y \And \pvar)$ <= $\pbar x$

$(y = x \And \pvar \c \pbar y \And \pvar)$ <= $\pbar x$

$(\pvar \And \qbar x \c \qbar y)$ <= $(\pvar \c x = y)$

$(\pvar \And \qbar x \c \qbar y)$ <= $(\pvar \c y = x)$

$(y = x \Or \qvar \c \pbar x \Or \qvar)$ <= $\pbar y$

$(\qvar \Or y = x \c\qvar \Or  \pbar x )$ <= $\pbar y$

$(x = y \Or \qvar \c \pbar x \Or \qvar)$ <= $\pbar y$

$(\qvar \Or x = y \c\qvar \Or  \pbar x )$ <= $\pbar y$

$(\rvar \c \ubar x \ident \ubar y)$ <= $(\pvar \And \qvar \c x = y)$;$\pvar$,$\qvar$

$(\qvar \c \ubar x \ident \ubar y) $<= $(\pvar \c x = y)$; $\pvar$

$(\qvar \c \ubar x \ident \ubar y) $<= $(\pvar \c y = x)$; $\pvar$

\lineb


Equality Substitutions Inside Quantifiers
\lineb

$(\Some x (\pbar x \And \Some y (\pbarp xy \And z = y))\Iff \Some x(\pbar x \And \Some y (\pbarp xz \And z = y)))$ <= 

$(\Some y \One x(\pbarpp xy\ubar x\And \ubar x = s) \Iff \Some y \One x (\pbarpp x y s \And \ubar x = s))$ <= 

$(\Some x (\pbar x \And x = y)\Iff \Some x (\pbar y \And x=y))$ <=

$(\Some x(\pbar x \And x = y) \c \pbar y)$<=

\lineb

Biconditional Substitutions

\lineb

$(\Not \pvar \Iff \Not \qvar)$ <= $(\pvar \Iff \qvar)$

$(\Not \pvar \c \Not \qvar)$ <= $(\pvar \Iff \qvar)$

$(\Not \qvar \c \Not \pvar)$ <= $(\pvar \Iff \qvar)$

\lineb

The Existence Quantifier
\lineb

$\Some x \pbar x$ <= $\ex y$,$\pbar y$

$\Some x \pbar x$ <= $\pbar y$,$\ex y$

$\Some x \pbar x$ <= $\One x \pbar x$

$(\pbar y \And \ex y \c \Some x \pbar x)$ <= 

$(\Some x \pbar x \c \ex y)$<= $(y \ident \an x \pbar x)$

$(\pbar y\c\Some x (\pbar x \And \qbar x))$ <= $\qbar y$,$\ex y$

$(\pbar y\c\Some x (\pbar x \And \qbar x))$ <= $\ex y$, $\qbar y$

$(\pvar \And \Some x \pbar x \c \pvar \And \pbar y)$ <= $(y \ident \an x \pbar x)$

$(\Some s \pvar \c \pvar)$<=

$(\Some x \Some y ; \pbarp xy \qvar \c \qvar)$<=

$(\pvar \And \Some x  \qvar\c \pvar \And \qvar)$ <= 

$(\pbar y \c \Some x \pbar x)$<=  $\ex y$

$(\Some s,t \pvar \c \pvar)$<=

$(\pbarp xy \And \ex x \And \ex y\c \Some x,y \pbarp xy)$ <= 

$(\Some x (\qbar x \And \pvar) \And \qvar \c \pvar \And \qvar)$ <=

$(\Some x (\qbar x \And \pvar) \c \pvar)$<=

$(\Some x (\pbar x \And \qbar x) \c \Some x \pbar x )$<=

$(\Some x \qbar x \And \pvar\c \Some x (\qbar x \And \pvar))$<=

$(\Some x(\qbar x \And \pvar)\c \Some x \qbar x \And \pvar )$<=

$(\Some x\pbar x \c\Some x(\pbar x \And\pvar))$<= $\pvar$

$(\Some x;\pbar x \qbar x \c \Some x ;\pbar x \rbar x)$<= $\Each x ; \pbar x (\qbar x \c \rbar x)$ 

$(x \in y \And \pbar x)$ <= $(x \ident \an s \in y \pbar s)$, $\Some s \in y \pbar s$

$(\Some s \pbar s \c \pbar x)$ <= $(x \ident \an s \pbar s)$

$(\Some s \in y \pbar s \c x \in y\And \pbar x)$ <= $(x \ident \an s \in y\pbar s)$

$(\Some s \in y \pbar s \c \pbar x)$ <= $(x \ident \an s \in y \pbar s)$

$(\Some x(\pbar \ubar x \And \ubar x = y)\c\Some x(\pbar y \And \ubar x = y))$ <= 

$(\Some x(\pbar \ubar x \And y = \ubar x)\c\Some x(\pbar y \And  y = \ubar x ))$ <= 

$(\pvar \And \pbar y \And \ex y \Iff\pvar \And \Some x\pbar x\And \pbar y \And \ex y)$ <=

$( \pvar \And \Some x\pbar x\And \pbar y \And \ex y \Iff \pvar \And \pbar y \And \ex y )$ <=

$(\pbar y \And \ex y \Iff \Some x\pbar x\And \pbar y \And \ex y)$ <=

$(\Some x\pbar x\And \pbar y \And \ex y \Iff  \pbar y \And \ex y )$ <=

$\Some x \Some y \pbarp xy$ <= $ \pbarp uv$,$\ex u$,$\ex v$

$\Some x \Some y \pbarp xy$ <= $ \pbarp uv$,$\ex v$,$\ex u$

$\Some x \Some y \pbarp xy$ <= $ \Some y \Some x \pbarp xy$

$\Some x;\pbar x \Some y \pbarp xy$<=$\Some y \Some x;\pbar x\pbarp xy$ 

$\Some x \Some y; \qbar y \pbarp xy$ <= $\Some y; \qbar y\pbarp xy$ 

$\Some x; \pbar x \Some y; \qbar y \pbarp xy$<=$\Some y;\qbar y\pbarp xy$

$(\Some x \Some y \pbarp xy \c \Some y \Some x \pbarp xy)$<=

$(\Some x;\pbar x \Some y \pbarp xy\c\Some y \Some x;\pbar x\pbarp xy)$ <=

$(\Some x \Some y; \qbar y \pbarp xy \c \Some y; \qbar y\pbarp xy)$ <=

$(\Some x; \pbar x \Some y; \qbar y \pbarp xy\c\Some y;\qbar y\pbarp xy)$ <=

$(\Some x \Some y \pbarp xy \Iff \Some y \Some x \pbarp xy)$<=

$(\Some x;\pbar x \Some y \pbarp xy\Iff\Some y \Some x;\pbar x\pbarp xy)$ <=

$(\Some x \Some y; \qbar y \pbarp xy \Iff \Some y; \qbar y\pbarp xy)$ <=

$(\Some x; \pbar x \Some y; \qbar y \pbarp xy\Iff\Some y;\qbar y\pbarp xy)$ <=

$(\Some x (\pbar x \And \rbar x)\Iff \Some x (\qbar x\And\rbar x))$ <= $(\qbar a \Iff \pbar a)$ U 

$(\Some x \Some y (\pbarp xy \And \qbar x)\Iff\Some x(\Some y \pbarp xy \And \qbar x))$ <=

$(\Some x,y (\pbarp xy \And \qbarp xy) \c \Some x,y\pbarp xy )$<=

$(\pvar \And \ex x \And \ex y \And \pbarp xy \c \pvar \And\Some x \Some y \pbarp xy)$ <=

$(\Some x (\pbar x \And \Some y (x = y))\Iff \Some x \pbar x)$ <=

$(\Some x \pbar x \Iff \Some x (\pbar x\And \Some y (x = y)))$ <=

$(\Some x (\pbar x \And \Some y (y = x))\Iff \Some x \pbar x)$ <=

$(\Some x \pbar x \Iff \Some x (\pbar x\And \Some y (y = x)))$ <=

$(\Some x (\pbar x \And y = x) \Iff  \Some x (\pbar y \And y = x))$ <=

$(\Some x (\pbar x \And y = x) \Iff  \pbar y \And \Some x (y = x))$ <=

$(\Some x (\qbar x \And \Some y (\pbar x  \And \pbarp x y)) \Iff \Some x (\qbar x \And \pbar x \And \Some y \pbarp x y))$ <=

$( \Some x (\qbar x \And \pbar x \And \Some y \pbarp x y) \Iff \Some x (\qbar x \And \Some y (\pbar x  \And \pbarp x y)) )$ <=

$(\Some x (\pbar x \And \qvar \And \rvar) \Iff \Some x (\pbar x \And \qvar))$ <= $(\qvar \c \rvar )$ 

$(\Each x(\pbar x \Iff \qbar x) \c \Some x\pbar x \Iff \Some x\qbar x)$<=

$(\Some x (\rbar x \And \pbar x)\Iff \Some x (\rbar x \And \qbar x))$ <=$\Each x(\rbar x \c \pbar x \Iff \qbar x)$

$(\Some x (\rbar x \And \pbar x) \And \qvar \c \Some x (\rbar x \And \qbar x) \And \qvar)$ <= $\Each x(\rbar x \And \pbar x \c \qbar x)$

$(\Some x (\pbar x \And \Not \pbar x \And \qbar x) \c \false)$<=

$\Some x,y, \in A (\pbarp xy \And \qbarp xy)$<= $\pbarp uv$,$\qbarp uv$,$(u,v,\in A)$

$\Some x,y, \in A (\pbarp xy \And \qbarp xy)$<= $\pbarp uv$,$(u,v,\in A)$,$\qbarp uv$

$\Some x,y, \in A (\pbarp xy \And \qbarp xy)$<= $(u,v,\in A)$,$\pbarp uv$,$\qbarp uv$

$(\Some x (\pbar x \And \qbar x) \Or \pvar \c \Some x \pbar x \Or \pvar)$ <=

$(\pvar \Or \Some x (\pbar x \And \qbar x) \c \pvar \Or \Some x \pbar x )$ <=

$(\pvar \Or \Some x \qvar \c \pvar \Or \qvar)$ <=

$(\Some x \pvar \Or \qvar \c \pvar \Or \qvar)$<=

$(\Some x ; \pbar x (\qbar x \Or \rbar x)\c \Some x;\pbar x \qbar x \Or \Some x ;\pbar x \rbar x)$<=

$(\Some x \pbar x \Iff \Some x\qbar x)$ <= $\Each x (\pbar x \Iff \qbar x)$  
\lineb

The Universal Quantifier
\lineb

$(\Each x \pbar x \And \ex y \c \pbar y)$ <=

$(\Each x \pbar x \c \pbar y)$ <= $\ex y$

$(\ex y \c \pbar y)$ <= $\Each x \pbar x$

$(\ex y \And \pbar y \c \qbar y)$<= $\Each x (\pbar x \c \qbar x)$

$\pbar y$ <= $\Each x \pbar x$,$\ex y$

$\pbar y$ <= $\ex y$,$\Each x \pbar x$

$(\Each x (\pbar x \c \qbar x) \c \qbar y)$<=$\pbar y$,$\ex y$

$(\Each x (\pbar x \c \qbar x) \c \qbar y)$ <= $\ex y$,$\pbar y$

$(\ex x \And \pbar x \And \Each y(\pbar y \c \qbar y) \c \qbar x)$<=

$(\Each x (\pbar x \c \qbar x) \c \Each x (\pbar x \c \rbar x))$ <= $\Each x(\qbar x \c \rbar x)$

$(\Each x; \pbar x \qbar x \c\Each x;\pbar x \rbar x)$<=$\Each x;\pbar x(\qbar x\c\rbar x))$

$(\Each x (\rbar x \c \pbar x \And \qbar x)\c \Each x (\rbar x \c \pbar x))$ <=

$\Each x (\pbar x \And \qbar x \c \qbar x)$<=

$\Each x (\rbar x \c \pbar x)$ <= $\Each x \pbar x $

$\Each x (\rbar x \c \pbar x)$ <= $\Each x(\rbar x \c \pbar x \And \qbar x)$

$(\Each x (\pbar x \Or \qbar x) \c \Each x \qbar x )$ <= $\Each x \Not\pbar x $

$(\Each x (\rbar x \c \pbar x \Or \qbar x) \c \Each x (\rbar x \c \qbar x)) $ <= $\Each x (\rbar x \c \Not\pbar x )$

$(\Each u,v (\pbarp uv \c \qbarp uv) \c \qbarp xy)$<=$\pbarp xy$,$\ex x$,$\ex y$

$(\Each u,v (\pbarp uv \c \qbarp uv) \c \qbarp xy)$<=$\ex x$,$\pbarp xy$,$\ex y$

$(\Each u,v (\pbarp uv \c \qbarp uv) \c \qbarp xy)$<=$\ex x$,$\ex y$,$\pbarp xy$

$(\Each u,v (\pbarp uv \c \qbarp uv) \c \qbarp xy)$<=$\pbarp xy$,$\ex y$,$\ex x$

$(\Each u,v (\pbarp uv \c \qbarp uv) \c \qbarp xy)$<=$\ex y$,$\pbarp xy$,$\ex x$

$(\Each u,v (\pbarp uv \c \qbarp uv) \c \qbarp xy)$<=$\ex y$,$\ex x$,$\pbarp xy$

$(\pbarp xy \c \qbarp xy)$<= $\Each u,v (\pbarp uv \And \rbarp uv\c \qbarp uv)$; $\ex x$,$\ex y$,$\rbarp xy$ 

$(\pbarp xy \c \qbarp xy)$<= $\Each u,v (\pbarp uv \And \rbarp uv\c \qbarp uv)$; $\ex x$,$\rbarp xy$,$\ex y$ 

$(\pbarp xy \c \qbarp xy)$<= $\Each u,v (\pbarp uv \And \rbarp uv\c \qbarp uv)$; $\rbarp xy$,$\ex x$,$\ex y$ 

$(\pbarp xy \c \qbarp xy)$<= $\Each u,v (\pbarp uv \And \rbarp uv\c \qbarp uv)$; $\ex y$,$\ex x$,$\rbarp xy$ 

$(\pbarp xy \c \qbarp xy)$<= $\Each u,v (\pbarp uv \And \rbarp uv\c \qbarp uv)$; $\ex y$,$\rbarp xy$,$\ex x$ 

$(\pbarp xy \c \qbarp xy)$<= $\Each u,v (\pbarp uv \And \rbarp uv\c \qbarp uv)$; $\rbarp xy$,$\ex y$,$\ex x$ 

$(\pbarp xy\And\ex x\And\ex y \c \qbarp xy)$<= $\Each u,v (\pbarp uv \c \qbarp uv)$ 

$(\pbarp xy\And \rbarp xy \And\ex x\And\ex y \c \rbarp xy \And \qbarp xy)$<= $\Each u,v (\pbarp uv \And \rbarp uv\c \qbarp uv)$ 

$(\pvar\And\Each x \qbar x \Iff \Each x(\pvar \And \qbar x))$<=

$(\Each x(\pvar \And \qbar x)\Iff \pvar\And\Each x \qbar x )$<=

$(\Each x (\pbar x \c \pvar \And \qbar x) \Iff \pvar \And \Each x (\pbar x \c \qbar x))$ <= $\Some x \pbar x$

$(\pvar \And \Each x (\pbar x \c \pbar x)\Iff \pvar)$<=

$(\pvar \Iff \pvar \And \Each x (\pbar x \c \pbar x))$<=

$(\Each x \qbar x \c \Each x (\rbar x \c \qbar x)) $ <= 

$\qbar x$ <= $\Each y \in A(\pbar y \c \qbar y)$;$(x \in A\And\pbar x)$

$\qbar x$<=$\Each y\in A(\pbar y \c \qbar y)$;$(x \in A)$,$\pbar x$

$\qbar x$<=$\Each y\in A(\pbar y \c \qbar y)$; $\pbar x$,$(x \in A)$

$\qbar x$<=$\Each y\in A(\pbar y \And \rbar y\c \qbar y)$;$(x \in A)$,$\pbar x$,$\rbar x$

$\qbar x$<=$\Each y\in A(\pbar y \And \rbar y\c \qbar y)$; $\pbar x$,$(x \in A)$,$\rbar x$

$\qbar x$<=$\Each y\in A(\pbar y \And \rbar y\c \qbar y)$; $\pbar x$,$\rbar x$,$(x \in A)$

$\qbarp xy$ <= $\Each u,v,\in A(\pbarp uv \c \qbarp uv)$;$(x,y,\in A \And \pbarp xy)$

$\pbar y$ <= $(\pvar \c \Each x \in A \pbar x)$; $\pvar$,$(y \in A)$

$\pbar y$ <= $(\pvar \c \Each x \in A \pbar x)$; $(y \in A)$,$\pvar$

$(\Some x; \pbar x \rbar x \c \Some x;\qbar x \rbar x)$<=$\Each x(\pbar x \c \qbar x)$

$(\Some x,y; \pbarp xy \rbarp xy \c \Some x,y;\qbarp xy \rbarp xy)$<=$\Each x,y(\pbarp xy \c \qbarp xy)$

$\Each x ; \pbar x(\qbar x \c \rbar x)$ <= $\Each x ; \pbar x (\qbar x \Iff \rbar x)$

$\Each x ; \pbar x(\qbar x \c \rbar x)$ <= $\Each x ; \pbar x (\rbar x \Iff \qbar x)$

$(\pvar \c\qbar x )$<=$(\pvar \Iff \Each y(\pbar y \c \qbar y))$;$\pbar x$

$(\pvar \c\qbar x )$<=$(\pvar \Iff \Each y(\pbar y \c \qbar y))$;$(\rvar \And \pbar x)$

$(\pvar \And \rvar \And \pbar x\c\qbar x \And \rvar)$<=$(\pvar \Iff \Each y(\pbar y \c \qbar y))$

$(\pvar \And \rvar \c \qbar x \And \rvar)$<=$(\pvar \Iff \Each y(\pbar y \c \qbar y))$;$\pbar x$

$\Each x \qbar x$<= ($(\pbar a \c \qbar a)$ U); $\Each x\pbar x$
\lineb

Universally Quantified Disjunctions

$(\Each x (\pbar x \c \q^{1}_{01}x \Or (\q^{1}_{02}x \Or \q^{1}_{03}x))\c \Each x (\pbar x \c \q^{1}_{01}x \Or \q^{1}_{02}x \Or \q^{1}_{03}x))$ <=

$(\Each x (\pbar x \c (\q^{1}_{01}x \Or \q^{1}_{02}x) \Or \q^{1}_{03}x)\c \Each x (\pbar x \c \q^{1}_{01}x \Or \q^{1}_{02}x \Or \q^{1}_{03}x))$ <=

$(\Each x (\pbar x \c (\q^{1}_{01}x \Or \q^{1}_{02}x) \Or \q^{1}_{03}x)\c \Each x (\pbar x \c \q^{1}_{01}x \Or (\q^{1}_{02}x \Or \q^{1}_{03}x)))$ <=

$(\Each x (\pbar x \c \q^{1}_{01}x \Or \rbar x)\c \Each x (\pbar x \c \q^{1}_{02}x \Or \rbar x))$ <= $(\pbar a \c (\q^{1}_{01}a \c \q^{1}_{02}a))$ U

$(\Each x (\pbar x \c \rbar x \Or \q^{1}_{01}x )\c \Each x (\pbar x \c \rbar x \Or \q^{1}_{02}x))$ <= $(\q^{1}_{01}a \c \q^{1}_{02}a)$ U

$(\Each x (\pbar x \c  \q^{1}_{01}x \Or \rbar x)\c \Each x (\pbar x \c \q^{1}_{02}x \Or \rbar x))$ <= $(\q^{1}_{01}a \c \q^{1}_{02}a)$ U

$(\Each x (\pbar x \c \q^{1}_{01}x \Or \rbar x)\c \Each x (\pbar x \c \q^{1}_{02}x \Or \rbar x))$ <= $(\pbar a \And \q^{1}_{01}a \c \q^{1}_{02}a)$ U

$(\Each x (\pbar x \c \rbar x\Or \q^{1}_{01}x )\c \Each x (\pbar x \c \rbar x \Or \q^{1}_{02}x ))$ <= $(\pbar a \And \q^{1}_{01}a \c \q^{1}_{02}a)$ U

$(\Each x(\pbar x \c \qbar x \Or \rbar x) \c \Each x (\pbar x \c \rbar x \Or \qbar x))$<=

$(\Each x (\pbar x \c \q^{1}_{01} x \Or \q^{1}_{02} x \Or \q^{1}_{03} x) \c\Each x (\pbar x \c \q^{1}_{01} x  \Or \q^{1}_{03} x ))$<= $(\q^{1}_{02} a\c \q^{1}_{03} a)$ U
\lineb

The  Uniqueness Quantifier
\lineb

$(\Unq x \pbar x \c \Unq x \qbar x)$<= $(\qbar a \c \pbar a)$ U


The Existence and Uniqueness Quantifier
\lineb

$\One x \pbar x$ <= $\Some x \pbar x$, $\Unq x \pbar x$

$\ex \The x \pbar x$ <= $\One x \pbar x$

$(\ex \The x \pbar x \c\One x \pbar x )$<=

$(y = \The x \pbar x)$ <= $\Unq x \pbar x$, $\ex y $,$\pbar y$

$(y = \The x \pbar x)$ <= $\Unq x \pbar x$, $\ex y $,$\pbar y$

$(y = \The x \pbar x)$ <= $\ex y$, $\Unq x \pbar x$, $\ex y $

$(y = \The x \pbar x)$ <= $\ex y$, $\pbar y$, $\Unq x \pbar x$

$(y = \The x \pbar x)$ <= $\pbar y$, $\ex y$, $\Unq x \pbar x$

$(y = \The x \pbar x)$ <= $\pbar y$, $\Unq x \pbar x$, $\ex y $

$(\Unq x \pbar x \c y = \The x \pbar x)$ <= $\ex y$,$\pbar y$

$(\Unq x \pbar x \c y = \The x \pbar x)$ <= $\pbar y$, $\ex y$

$(\pbar y \c y = \The x \pbar x)$ <= $\Unq x \pbar x$, $\ex y$

$(\pbar y \c y = \The x \pbar x)$ <= $\ex y$, $\Unq x \pbar x$

$(\One x \pbar x\c y = \The x \pbar x)$ <= $(y \ident \The x\pbar x)$

$\One x \pbar x $<= $\ex \The x \pbar x$

$(\ex \The x \pbar x \Iff \One x \pbar x)$ <=

$(\One x \pbar x \Iff \ex \The x \pbar x)$ <=

$\One x (x = y \And \pbar x)$ <= $\Some x (x = y \And \pbar x)$

$(\One x (x = y \And \pbar x)\Iff\Some x(x = y \And \pbar x))$<=

$(\Some x (x = y \And \pbar x)\Iff\One x(x = y \And \pbar x))$<=

$\Some x\pbar x$ <= $\One x \pbar x$ 

$(\One x \pbar x\c\Some x \pbar x)$ <= 

$(\One x\pbar x \And y = \The x \pbar x\Iff\One x\pbar x\And \pbar y \And \ex y)$ <=

$( \One x\pbar x\And \pbar y \And \ex y\Iff \One x\pbar x \And y = \The x \pbar x)$ <=

$\pbar y$ <= $\One x\pbar x $, $ (y \ident \The x \pbar x)$ 

$\pbar y$ <=  $ (y \ident \The x \pbar x)$, $\One x\pbar x $

$(y = \The x \pbar x)$ <= $ (y \ident \The x \pbar x)$ , $\One x\pbar x $

$(y = \The x \pbar x)$ <=  $\One x\pbar x $,$(y \ident \The x \pbar x)$ 

$(\pvar \And \One x\pbar x \And y = \The x \pbar x\Iff\pvar \And \One x\pbar x\And \pbar y \And \ex y)$ <=

$(\pvar \And  \One x\pbar x\And \pbar y \And \ex y\Iff \pvar \And \One x\pbar x \And y = \The x \pbar x)$ <=

$(\pbar x \And \ex x \c x = y)$<= $(y = \The x \pbar x)$

$(\Some x \One y(\pbarp xy \And \pbar x)\Iff \Some x(\One y\pbarp xy \And \pbar x))$ <=
\lineb


Hence rules
\lineb

$(\ppvar \c \qvar)$ <= $\qvar$ H $\ppvar$

$(\pvar \c \qvar \And \rvar)$ <= $\qvar$,$\rvar$ H $\pvar$

$(\ppvar \And \pqvar\c \qvar)$ <= $\qvar$ H $\ppvar$,$\pqvar$

$(\ppvar \And \pqvar \And \prvar \c \qvar)$ <= $\qvar$ H $\ppvar$ , $\pqvar$ , $\prvar$ 

$(\ppvar \And \pqvar \And \prvar \And \psvar\c \qvar)$ <= $\qvar$ H $\ppvar$ , $\pqvar$ , $\prvar$ ,$\psvar$

$(\ppvar \And \pqvar \And \prvar \And \psvar\And \qpvar\c \qvar)$ <= $\qvar$ H $\ppvar$,$\pqvar$ , $\prvar$ ,$\psvar$,$\qpvar$

$(\ppvar \And \pqvar \And \prvar \And \psvar\And \qpvar \And \qqvar \c \qvar)$ <= $\qvar$ H $\ppvar$,$\pqvar$ , $\prvar$ ,$\psvar$,$\qpvar$,$\qqvar$

$(\ppvar \And \pqvar \And \prvar \And \psvar\And \qpvar \And \qqvar \And \qrvar \c \qvar)$ <= $\qvar$ H $\ppvar$,$\pqvar$ , $\prvar$ ,$\psvar$,$\qpvar$,$\qqvar$,$\qrvar$

$(\ppvar \And \pqvar \And \prvar \And \psvar\And \qpvar \And \qqvar \And \qrvar \And \qsvar\c \qvar)$ <= $\qvar$ H $\ppvar$,$\pqvar$ , $\prvar$ ,$\psvar$,$\qpvar$,$\qqvar$,$\qrvar$,$\qsvar$

$(\ppvar \And \pqvar \And \prvar \And \psvar\And \qpvar \And \qqvar \And \qrvar \And \qsvar \And \rpvar\c \qvar)$ <= $\qvar$ H $\ppvar$,$\pqvar$ , $\prvar$ ,$\psvar$,$\qpvar$,$\qqvar$,$\qrvar$,$\qsvar$,$\rpvar$

$(\ppvar \And \pqvar \And \prvar \And \psvar\And \qpvar \And \qqvar \And \qrvar \And \qsvar \And \rpvar\And\rqvar\c \qvar)$ <= $\qvar$ H $\ppvar$,$\pqvar$ , $\prvar$ ,$\psvar$,$\qpvar$,$\qqvar$,$\qrvar$,$\qsvar$,$\rpvar$,$\rqvar$

$(\ppvar \And \pqvar \And \prvar \And \psvar\And \qpvar \And \qqvar \And \qrvar \And \qsvar \And \rpvar\And \rqvar\And \rrvar\c \qvar)$ <= $\qvar$ H $\ppvar$,$\pqvar$ , $\prvar$ ,$\psvar$,$\qpvar$,$\qqvar$,$\qrvar$,$\qsvar$,$\rpvar$,$\rqvar$,$\rrvar$

$(\ppvar \And \rvar\c \qvar)$ <= $(\rvar \c \qvar)$ H $\ppvar$

$(\ppvar \And \pqvar \And \rvar \c \qvar)$ <= $(\rvar\c\qvar)$ H $\ppvar$, $\pqvar$ 

$(\ppvar \And \prvar \And \psvar\And \pqvar \c \qvar)$ <=$(\pqvar \c \qvar)$ H $\ppvar$,$\prvar$,$\psvar$

$(\ppvar \And \prvar \And\psvar\And \qpvar \And \pqvar \c \qvar)$ <=$(\pqvar \c \qvar)$ H $\ppvar$,$\prvar$,$\psvar$,$\qpvar$

$(\ppvar \And \prvar \And \psvar\And \pqvar \And \qpvar \And \qqvar \c \qvar)$ <=$(\pqvar \c \qvar)$ H $\ppvar$,$\prvar$,$\psvar$,$\qpvar$,$\qqvar$

$(\ppvar \And \prvar \And \psvar\And \pqvar \And \qpvar \And \qqvar \And \qrvar \c \qvar)$ <=$(\pqvar \c \qvar)$ H $\ppvar$,$\prvar$,$\psvar$,$\qpvar$,$\qqvar$,$\qrvar$

$(\ppvar \And \prvar \And \psvar\And \pqvar \And \qpvar \And \qqvar \And \qrvar \And \qsvar \c \qvar)$ <=$(\pqvar \c \qvar)$ H $\ppvar$,$\prvar$,$\psvar$,$\qpvar$,$\qqvar$,$\qrvar$,$\qsvar$

$(\ppvar \And \prvar \And \psvar\And \pqvar \And \qpvar \And \qqvar \And \qrvar \And \qsvar \And \rpvar \c \qvar)$ <=$(\pqvar \c \qvar)$ H $\ppvar$,$\prvar$,$\psvar$,$\qpvar$,$\qqvar$,$\qrvar$,$\qsvar$,$\rpvar$

$(\ppvar \And \prvar \And \psvar\And \pqvar \And \qpvar \And \qqvar \And \qrvar \And \qsvar \And \rpvar \And \rqvar\c \qvar)$ <=$(\pqvar \c \qvar)$ H $\ppvar$,$\prvar$,$\psvar$,$\qpvar$,$\qqvar$,$\qrvar$,$\qsvar$,$\rpvar$,$\rqvar$

$(\ppvar \And \prvar \And \psvar\And \pqvar \And \qpvar \And \qqvar \And \qrvar \And \qsvar \And \rpvar \And\rqvar\And\rrvar\c \qvar)$ <=$(\pqvar \c \qvar)$ H $\ppvar$,$\prvar$,$\psvar$,$\qpvar$,$\qqvar$,$\qrvar$,$\qsvar$,$\rpvar$,$\rqvar$,$\rrvar$

$(\ppvar \And \prvar \And \psvar\And \pqvar \And \qpvar \And \qqvar \And \qrvar \And \qsvar \And \rpvar \And \rqvar\And\rrvar\And\rsvar\c \qvar)$ <=$(\pqvar \c \qvar)$ H $\ppvar$,$\prvar$,$\psvar$,$\qpvar$,$\qqvar$,$\qrvar$,$\qsvar$,$\rpvar$,$\rqvar$,$\rrvar$,$\rsvar$

$(\ppvar \And \prvar \And \psvar\And \pqvar \And \qpvar \And \qqvar \And \qrvar \And \qsvar \And \rpvar \c \qvar)$ <=$(\pqvar \c \qvar)$ H $\ppvar$,$\prvar$,$\psvar$,$\qpvar$,$\qqvar$,$\qrvar$,$\qsvar$,$\rpvar$

$\pvar$ <= $\false$ H $\Not \pvar$ 

$\Not \pvar$ <= $\false$ H $\pvar$ 

$\Not \pvar$ <= $\Not\pvar$ H $\pvar$

$\pvar$ <= $\pvar$ H $\Not\pvar$

$(\pvar \Or \qvar)$ <= $\qvar$ H $\Not\pvar$

$(\qvar \Or \pvar)$ <= $\qvar$ H $\Not\pvar$

$(\svar \c \pvar \Or \qvar)$ <= $(\svar \c \qvar)$ H $\Not\pvar$

$(\svar \c \qvar \Or \pvar)$ <= $(\svar \c \qvar)$ H $\Not\pvar$

$(\pvar \And \qvar \Iff \pvar \And \rvar)$ <= $(\qvar \Iff \rvar)$ H $\pvar$

$(\pvar \c \qpvar \And \qqvar)$ <= $\qpvar$,$\qqvar$ H $\pvar$

$(\pvar \c \qpvar \And \qqvar \And \qrvar)$ <= $\qpvar$,$\qqvar$,$\qrvar$ H $\pvar$

$(\pvar \c \qpvar \And \qqvar \And \qrvar\And \qsvar)$ <= $\qpvar$,$\qqvar$,$\qrvar$ $\qsvar$ H $\pvar$
\lineb


Universalizations
\lineb

$\Each x \pbar x$ <= $\pbar a$ U

$\Each x \pbar x$ <= $(\ex a \c \pbar a)$ U

$\Each x( \pbar x \c \qbar x)$ <= $(\pbar a \Iff \qbar a)$ U

$\Each x( \pbar x \c \qbar x)$ <= $(\qbar a \Iff \pbar a)$ U

$\Each x(\pbar x \Iff \qbar x)$ <= $(\qbar a \Iff \pbar a)$ U

$\Each x( \pbar x \c \qbar x)$ <= $\qbar a$ U

$\Each x (\pbar x \And \qbar x \c \rbar x)$ <= $(\qbar a \c \rbar a)$ U

$\Each t,u \pbarp tu$ <= $\pbarp ab$ U

$(\Some x (\pbar x \And \rbar x)\c \Some x (\qbar x\And \rbar x))$ <= $(\pbar a \c \qbar a)$ U

$(\Some x \pbar x \c \Some x \qbar x)$<=$(\pbar a \c \qbar a)$ U

$(\Some x \pbar x \Iff \Some x (\pbar x \And \qbar x))$<=$(\pbar a \c \qbar a)$ U

$(\Some x (\pbar x\And \qbar x) \Iff \Some x \pbar x)$<=$(\pbar a \c \qbar a)$ U

$(\Some x (\pbar x \And \rbar x)\c \Some x (\qbar x\And \rbar x))$ <= $(\pbar a \Iff \qbar a)$ U

$(\pvar \And \Some x (\pbar x \And \rbar x) \c \pvar \And \Some x (\qbar x \And \rbar x))$<= $(\pbar a \c \qbar a)$ U

$(\Some x \pbar x \Iff \Some x\qbar x)$<=$(\ex a \c \pbar a \Iff\qbar a)$ U

$(\Some x \pbar x \Iff \Some x\qbar x)$<=$(\ex a \c \qbar a \Iff\pbar a)$ U

$(\Some x \pbar x \c \Some x\qbar x)$<=$(\pbar a \Iff\qbar a)$ U

$(\Some x \pbar x \c \Some x\qbar x)$<=$(\qbar a \Iff\pbar a)$ U

$(\Some x(\pbar x \And \rbar x) \c \Some x(\qbar x \And \rbar x))$<=$(\pvar \And \pbar a\c\qbar a)$ U $\pvar$

$(\Some x (\pbar x \And \rbar x)\Iff \Some x(\qbar x\And\rbar x))$ <= $(\pbar a \Iff \qbar a)$ U

$(\Some x(\pbar x \And \rbar x) \c \Some x(\qbar x \And \rbar x))$<=$(\qbar a\Iff\pbar a)$ U

$(\Some x(\pbar x \And \rbar x) \c \Some x(\qbar x \And \rbar x))$<=$(\pbar a\Iff\qbar a)$ U

$(\Some x \pbar x \c \Some x (\pbar x \And \qbar x))$<=$(\pbar a \c \qbar a)$ U

$(\Some x (\pbar x \And \rbar x) \c \Some x (\pbar x \And \qbar x \And \rbar x))$<= $(\pbar a \c \qbar a)$ U

$(\Some x \pbar x \And \pvar\c \Some x \qbar x\And \pvar)$<=$(\pbar a \c \qbar a)$ U

$(\Some x \in y \pbar x \c \Some x\in y  \qbar x)$<=$(\pbar a \c \qbar a)$ U

$(\Some x \pbar x \And \pvar\c \Some x \qbar x\And \pvar)$<=$(\pbar a \Iff \qbar a)$ U

$(\Some x  \qbar x \Iff \Some x  \rbar x)$ <= $(\qbar a \Iff \rbar a)$ U

$(\Some x(\pbar x \And \rbar x) \c \Some x(\qbar x \And \rbar x))$<= $(\pbar a \And \rbar a \c \qbar a)$ U

$(\Some x(\pbar x\And\qbar x)\c\Some x(\pbar x\And\qbar x\And\qvar))$ <=  $(\pbar a \c \qvar)$ U

$(\Some x (\pbar x \And \qbar x)\c  \qvar)$ <=  $(\pbar a \c \qvar)$ U

$\Unq t \pbar t$ <= $(\pbar a \And \pbar b \c a = b)$ U

$\Unq t \pbar t$<= $\Each x(\pbar x \c x = y)$

$\Each s\Unq t \pbarp ts$ <= $(\pbarp ac \And \pbarp bc \c a = b)$ U

$(\Each x (\pbar x \c x = y)\c \Unq t \pbar t )$<= 

$\Not \pbar\Nul$ <= $(\pbar a \c \ex a)$ U

$(\Each x  \qbar x \Iff \Each x  \rbar x)$ <= $(\qbar a \Iff \rbar a)$ U

$(\Each x (\pbar x \c \qbar x) \Iff \Each x (\pbar x \c \rbar x))$ <= $(\qbar a \Iff \rbar a)$ U

$(\Each x (\pbar x \c \qbar x) \c \Each x (\pbar x \c \rbar x))$ <= $(\qbar a \c \rbar a)$ U

$(\Each x (\pbar x \c \qbar x) \c \Each x (\pbar x \c \rbar x))$ <= $(\rbar a \Iff \qbar a)$ U

$(\Each x (\pbar x \c \qbar x) \c \Each x (\pbar x \c \rbar x))$ <= $(\qbar a \Iff \rbar a)$ U

$\Each x \qbar x$ <= $(\pbar a \c \qbar a)$ U $\Each x\pbar x$

$\Each x \qbar x$ <= $(\pbar a \Iff\qbar a)$ U $\Each x\pbar x$

$\Each x \qbar x$ <= $(\qbar a \Iff\pbar a)$ U $\Each x\pbar x$

$\Each x(\rbar x \c  \qbar x)$ <= $(\pbar a \Iff\qbar a)$ U $\Each x(\rbar x \c \pbar x)$

$\Each x(\rbar x \c  \qbar x)$ <= $(\qbar a \Iff\pbar a)$ U $\Each x(\rbar x \c \pbar x)$

$(\Each x \pbar x \c \Each x \qbar x)$ <= $(\pbar a \c \qbar a)$ U

$(\Some x (\pbar x \And \qbar x) \c \Some x (\pbar x \And \rbar x))$ <= $(\pvar \And \qbar a \Iff \rbar a)$ U $\pvar$

$(\Some x (\pbar x \And \rbar x) \Iff \Some x(\qbar x \And \rbar x))$ <= $(\pvar \c \pbar a \Iff \qbar a)$ U $\pvar$

$(\Some x (\qbar x \And \rbar x) \Iff \Some x(\pbar x \And \rbar x))$ <= $(\pvar \c \pbar a \Iff \qbar a)$ U $\pvar$

$(\One x (\pbar x \And \qbar x) \c \One x (\pbar x \And \rbar x))$ <= $(\pvar \And \qbar a \Iff \rbar a)$ U $\pvar$

$(\One x (\pbar x \And \rbar x) \Iff \One x(\qbar x \And \rbar x))$ <= $(\pvar \c \pbar a \Iff \qbar a)$ U $\pvar$

$(\One x (\qbar x \And \rbar x) \Iff \One x(\pbar x \And \rbar x))$ <= $(\pvar \c \pbar a \Iff \qbar a)$ U $\pvar$

$(\One x\pbar x \Iff\One x\qbar x)$ <= $(\pbar a\Iff\qbar a)$ U

$(\One x\qbar x \Iff\One x\pbar x)$ <= $(\pbar a\Iff\qbar a)$ U

$(\pvar \And \Some x \qbar x \Iff \pvar \And \Some x \rbar x)$ <= $(\qbar a \Iff \rbar a)$ U

$(\pvar \And \Some x \qbar x \Iff \pvar \And \Some x \rbar x)$ <= $(\rbar a \Iff \qbar a)$ U

$(\Each x ; \pbar x \qbar x \c \false)$ <= $(\qbar a \And \rbar a \c \false)$ U $\Some x; \pbar x \rbar x$ , $\Some x \pbar x$

$(\Each x ; \pbar x \qbar x \c \false)$ <= $(\qbar a \And \rbar a \c \false)$ U  $\Some x \pbar x $ , $\Some x; \pbar x \rbar x$

$(\Some x ; \pbar x \qbar x \c \false)$ <= $(\qbar a \And \rbar a \c \false)$ U $\Each x; \pbar x \rbar x$ , $\Some x \pbar x$

$(\Some x ; \pbar x \qbar x \c \false)$ <= $(\qbar a \And \rbar a \c \false)$ U $\Some x \pbar x$ , $\Each x; \pbar x \rbar x$ 

$(\Each x(\pbar x \c \qbar x) \Iff \Each x (\pbar x \c \rbar x))$ <= $(\pbar a \c \qbar a \Iff \rbar a)$ U

$(\Each x (\pbar x \c \qbar x) \c \Each x (\pbar x \c \rbar x))$<= $(\qbar a \Iff \rbar a \And \pbar a)$ U

$(\Each x; \pbar x \qbar x \c\Each x;\pbar x \rbar x)$<= $(\pbar a \And \qbar a\c\rbar a)$ U

$(\pvar \And \Each x \in A\pbar x \c \pvar \And \Each x \in A \qbar x)$ <= $(\pvar \And \qvar \And \rvar \And \svar \And \pbar a \c \qbar a)$ U $\qvar$,$\rvar$,$\svar$

$(\Each x \pbar x \And \qvar)$ <= ($\pbar a$ U), $\qvar$

$(\Each x \pbar x \And \qvar)$ <= $\qvar$, ($\pbar a$ U)

\lineb

Double Universalizations
\lineb

$\Each u \Each v \pbarp uv $ <= $\pbarp ab $ U

$(\Some x(\pbar x \And \Some y (\pbarp xy \And \qbarp xy))\Iff\Some x(\pbar x \And \Some y (\pbarp xy \And \rbarp xy)))$ <= $(\qbarp ab \Iff \rbarp ab)$ U

$(\Some x\One y (\pbarp xy \And \rbarp xy)\Iff\Some x\One y(\qbarp xy \And \rbarp xy))$ <= $(\pbarp ab\Iff\qbarp ab)$ U

$(\Some x\One y (\pbarp xy \And \rbarp xy)\Iff\Some x\One y(\qbarp xy \And \rbarp xy))$ <= $(\qbarp ab\Iff\pbarp ab)$ U

$\Each x,y (\pbarp xy \c \qbarp xy)$ <= $\qbarp ab$ U

$\Each x ;\pbar x \Each y ;\qbar y \rbarp xy$<= $(\pbar a \And \qbar b \c \rbarp ab)$ U

$(\Some x,y \pbarp xy \c \Some x,y \qbarp xy)$ <= $(\pvar \And \pbarp ab \c \qbarp ab)$ U $\pvar$

$(\Some x,y \pbarp xy \c \Some x,y \qbarp xy)$ <= $(\pbarp ab \c \qbarp ab)$ U

$(\Some x (\pbar x \And \rbar x)\c\Some x \qbar x)$ <= $(\pbar a\c\qbar a)$ U

$(\Some x,y,\in A(\pbarp xy \And \rbarp xy)\c\Some x,y,\in A(\qbarp xy \And \rbarp xy))$<=    $(\pvar \And \pbarp ab \c \qbarp ab)$ U $\pvar$

$(\Some x \Some y ; \pbarp xy \rbarp xy \Iff \Some x \Some y ;\pbarp xy \qbarp xy)$<=$(\rbarp ab \Iff \qbarp ab)$ U

$(\Some x \Some y ; \pbarp xy \qbarp xy \Iff \Some x \Some y ;\pbarp xy \rbarp xy)$<=$(\rbarp ab \Iff \qbarp ab)$ U

$(\Some x \Some y ; \pbarp xy \rbarp xy \c \Some x \Some y ;\pbarp xy \qbarp xy)$<=$(\rbarp ab \Iff \qbarp ab)$ U

$(\Some x \Some y ; \pbarp xy \qbarp xy \c \Some x \Some y ;\pbarp xy \rbarp xy)$<=$(\rbarp ab \Iff \qbarp ab)$ U

$(\Some x \Some y ; \pbarp xy \qbarp xy \c \Some x \Some y ;\pbarp xy \rbarp xy)$<=$(\qbarp ab \c \rbarp ab)$ U

$(\Some x \Some y ; \pbarp xy \qbarp xy \Iff \Some x \Some y ; \pbarp xy \rbarp xy)$<= $(\q^{2}_{01}ab \c \qbarp ab \Iff \rbarp ab)$ U $\Each x \Each y ; \pbarp xy \q^{2}_{01}xy$

$(\Some x \Some y ; \pbarp xy \qbarp xy \Iff \Some x \Some y ; \pbarp xy \rbarp xy)$<= $(\q^{2}_{01}ab \c \rbarp ab \Iff \qbarp ab)$ U $\Each x \Each y ; \pbarp xy \q^{2}_{01}xy$

\lineb

Super Universalization Rules
\lineb

$(\Each x (\pbar x \c \qbar x) \And \Not\pbar \Nul)$<= $((\pbar a \c \qbar a)\And(\qbar a \c \ex a))$ U

$(\Each x (\pbar x \c \qbar x) \And \Not\pbar \Nul)$<= $(\pbar a \c \qbar a)$,$(\qbar a \c \ex a)$ U

$(\Each x (\pbar x \c \qbar x) \And \Not\pbar \Nul)$<= $(\qbar a \c \ex a)$, $(\pbar a \c \qbar a)$ U

Implied Existence Rules

$(\pbar x \c \Some x \pbar x)$<= $(\pbar a \c \ex a) $ U 

$\Some x \pbar x$<= $(\pbar a \c \ex a) $ U $\pbar x$

$(\pbar x \c \qbar x)$ <= $\Each x (\pbar x \c \qbar x)$; ($(\pbar a \c \ex a)$ U)

$(\pbar x \c \qbar x)$ <= $\Each x (\pbar x \And \rbar x\c \qbar x)$;$\rbar x$, ($(\pbar a \c \ex a)$ U)

$(\pbar x \c \qbar x)$ <= $\Each x (\pbar x \And \rbar x\c \qbar x)$; ($(\pbar a \c \ex a)$ U),$\rbar x$

$(\pbar x \c \qbar x)$ <= $\Each x (\pbar x \c \qbar x\Iff \rbar x)$; ($(\pbar a \c \ex a)$ U),$\rbar x$

$(\pbar x \c \qbar x)$ <= $\Each x (\pbar x \c \qbar x\Iff \rbar x)$;$\rbar x$, ($(\pbar a \c \ex a)$ U)

$(\pbar x \c \qbar x)$ <= $\Each x (\pbar x \c \rbar x\Iff \qbar x)$; ($(\pbar a \c \ex a)$ U),$\rbar x$

$(\pbar x \c \qbar x)$ <= $\Each x (\pbar x \c \rbar x\Iff \qbar x)$;$\rbar x$, ($(\pbar a \c \ex a)$ U)

$\qbar x$ <= $\Each x (\pbar x \c \rbar x\Iff \qbar x)$;($(\pbar a \c \ex a)$ U),$\pbar x$,$\rbar x$

$\qbar x$ <= $\Each x (\pbar x \c \rbar x\Iff \qbar x)$;($(\pbar a \c \ex a)$ U),$\rbar x$,$\pbar x$

$\qbar x$ <= $\Each x (\pbar x \c \rbar x\Iff \qbar x)$;$\rbar x$, ($(\pbar a \c \ex a)$ U),$\pbar x$

$\qbar x$ <= $\Each x (\pbar x \c \rbar x\Iff \qbar x)$;$\pbar x$, ($(\pbar a \c \ex a)$ U),$\rbar x$

$\qbar x$ <= $\Each x (\pbar x \c \rbar x\Iff \qbar x)$;$\rbar x$,$\pbar x$,($(\pbar a \c \ex a)$ U)

$\qbar x$ <= $\Each x (\pbar x \c \rbar x\Iff \qbar x)$;$\pbar x$,$\rbar x$,($(\pbar a \c \ex a)$ U)

$\qvar$<= $(\qvar \Iff \Each x(\pbar x \c \ex \ubar x))$;($(\pbar a \c \ex\ubar a)$ U)

$\qvar$<= $(\Each x(\pbar x \c \ex \ubar x)\Iff \qvar)$;($(\pbar a \c \ex\ubar a)$ U)

$\qvar$<= $(\Each x(\pbar x \c \ex \ubar x)\c \qvar)$;($(\pbar a \c \ex\ubar a)$ U)

$(\pbar x \And \qbar x \c \rbar x)$<= $(\qbar a \c \ex a )$ U $\Each x (\pbar x \And \qbar x \c \rbar x)$

$(\pbarp xy \And \qbarp xy \c \rbarp xy)$<= $(\qbarp ab \c \ex a \And \ex b)$ U $\Each x \Each y (\pbarp xy \And \qbarp xy \c \rbarp xy)$

Rules Assuming Existent Operand Requirement
\lineb

$\pbar y$ <= $\Each x \in z \pbar x$; $(y \in z)$ 

$\pbar y$ <= $\Each x \i z \pbar x$; $(y \i z)$ 

$\pbar y$ <= $\Each x \in z (\qbar x \c \pbar x)$; $(y \in z)$, $\qbar y$

$\pbar y$ <= $\Each x \in z (\qbar x \c \pbar x)$; $\qbar y$, $(y \in z)$ 

$\pbar y$ <= $\Each x \i z (\qbar x \c \pbar x)$; $(y \i z)$, $\qbar y$

$\pbar y$ <= $\Each x \i z (\qbar x \c \pbar x)$; $\qbar y$, $(y \i z)$ 

$\qbar y$ <= $\Each x \in z (\pbar x \c \qbar x)$; $(y \in z \And \pbar y)$ 

$(y \in z \And \pbar y \c \qbar y)$ <= $\Each x \in z (\pbar x \c \qbar x)$

$(x \in A \c x \in A \And \pbar x)$ <= $\Each x \in A \pbar x$

$(x \in A \And \rvar \c \pbar x \And \rvar)$ <= $\Each x \in A \pbar x$

$(\pvar \c \pbar y)$ <= $\Each x \in z \pbar x$; $(y \in z)$ 

$(\Each y \in A (\pbar y \c \qbar y) \c  \qbar x)$ <= $(x \in A)$,$\pbar x$

$(\Each y \in A (\pbar y \c \qbar y) \c  \qbar x)$ <= $\pbar x$,$(x \in A)$

$\pbarp xy$ <= $\Each x,y, \in z \pbarp  xy$; $(x,y, \in z)$ 

$\pbarp xy$ <= $\Each x,y, \in z \pbarp  xy$; $(x \in z)$ ,$(y\in z)$

$\pbarp xy$ <= $\Each x,y, \in z \pbarp  xy$; $(y \in z)$ ,$(x\in z)$

$(y \in z \c \pbar y)$ <= $\Each x \in z \pbar x$

$(x\in z \And y \in z \c \pbarp xy)$ <= $\Each x,y, \in z \pbarp xy$

$(x\in z \c \pbarp xy)$ <= $\Each x,y, \in z \pbarp xy$; $(y \in z)$

$(y\in z \c \pbarp xy)$ <= $\Each x,y, \in z \pbarp xy$; $(x \in z)$

$(\Each x \in z \pbar x \c \pbar y)$ <= $(y \in z)$

$(y \in z \And \Each x \in z \pbar x \c \pbar y)$ <=

$\Some x \in z \pbar x$ <= $\pbar y$, $(y \in z)$

$\Some x \in z \pbar x$ <=  $(y \in z)$,$\pbar y$

$\Some x \in z (\pbar x \And \qbar x)$ <=  $(y \in z)$,$\pbar y$,$\qbar y$

$\Some x \in z (\pbar x \And \qbar x)$ <=  $\pbar y$,$(y \in z)$,$\qbar y$

$\Some x \in z (\pbar x \And \qbar x)$ <=  $\pbar y$,$\qbar y$,$(y \in z)$

$\Some x \in z \pbar x$ <=  $(y \in z\And \pbar y)$

$\Some x,y \in z \pbarp xy$ <= $\pbarp uv$, $(u,v, \in z)$

$\Some x,y \in z \pbarp xy$ <=  $(u,v, \in z)$,$\pbarp uv$

$\Some x,y \in z \pbarp xy$ <=  $(u,v, \in z\And \pbarp uv)$

$\Some x \in z (\pbar x \And \qbar x)$ <=  $(y \in z\And \pbar y)$,$\qbar y$

$\Some x \in z (\pbar x \And \qbar x)$ <=  $\qbar y$, $(y \in z\And \pbar y)$

$(\pbar y \c \Some x \in z \pbar x)$ <=  $(y \in z)$

$(y \in z \And \pbar y \c \Some x \in z \pbar x)$ <= 

$(y \in z \c \Some x \in z \pbar x)$ <=  $\pbar y$

$\Some x \in z (\pbar x \And \qbar x)$ <=  $(u \in z\And \pbar u)$,$\qbar u$

$\Some x \in z (\pbar x \And \qbar x)$ <=  $\qbar u$, $(u \in z\And \pbar u)$

$\pbar y$<=$(\qvar \Iff \Each x \in A \pbar x)$;$\qvar$,$(y \in A)$

$\pbar y$<=$(\qvar \Iff \Each x \in A \pbar x)$;$(y \in A)$,$\qvar$

$(\pvar \c \pbar y)$<=$(\pvar \Iff \prvar \And \Each x \in A \pbar x )$;$(y \in A)$

$\pbar y$<= $(\pvar \Iff \qvar \And \Each t \in A  \pbar t)$;$\pvar$,$(y \in A)$

$\pbar y$<= $(\pvar \Iff \qvar \And \Each t \in A  \pbar t)$;$(y \in A)$,$\pvar$

$(x \in A \c \pbarp xy)$ <= $\Each t \in A \Each u \in B \pbarp tu$;$(y \in B)$

$(y \in B \c \pbarp xy)$ <= $\Each t \in A \Each u \in B \pbarp tu$;$(x \in A)$

$(y \i z \c \pbar y)$ <= $\Each x \i z \pbar x$

$(x \i A \And \rvar \c \pbar x \And \rvar)$ <= $\Each x \i A \pbar x$
\lineb

Elementary Properties of Identity and Equality
\lineb

$(x = y \c y = x)$ <=

$(z \ident y \c y \ident x)$ <=

$(x = y)$ <= $(y = x)$

$(x \ident y)$ <= $(y \ident x)$

$(x \ident y)$ <= $(y = x)$

$(\pvar \And x = y \And y = z \c \pvar \And x = y \And y = z \And x = z)$ <=

$(x = y)$ <= $(x = z)$, $(y = z)$

$(x = y)$ <= $(y = z)$, $(x = z)$

$(x \ident z \And y \ident z \c x \ident y)$ <=

$(x = y \c \ex x \And \ex y)$ <=

$(x = y)$ <= $\ex x$, $(x \ident y)$

$(x = y)$ <= $\ex y$, $(x \ident y)$

$(x = y)$ <=  $(x \ident y)$,$\ex x$

$(x = y)$ <=  $(x \ident y)$,$\ex y$

$(y\ident z \c x =z)$ <= $(y = x)$

$(x = y\Or \pvar \Iff y = x \Or \pvar)$ <=

$(\pvar \Or x = y \Iff \pvar \Or y = x)$ <=

\lineb


Negation
\lineb

$(\pvar \Or \qvar)$ <= $(\Not \pvar \c \qvar)$
\lineb

Negated Equality
\lineb

$(x \ne y)$ <= $\ex x$, $\ex y$, $\Not (x = y)$

$(x \ne y)$ <= $\ex x$, $\Not(x = y)$, $\ex y$

$(x \ne y)$ <=  $\Not(x = y)$,$\ex x$, $\ex y$

$\ex x$ <= $(x \ne y)$

$\ex y$ <= $(x \ne y)$

$\Not (x = y)$ <= $(x \ne y)$

$\false$ <= $(x = y)$, $(x \ne y)$

$\false$ <= $(x \ne y)$, $(x = y)$

$(x = y \c \false)$ <=  $(\pvar \c x \ne y)$;$\pvar$

$(x \ne y \c \false)$ <=  $(\pvar \c x = y)$;$\pvar$

$(x = y \c \false)$ <=  $(x \ne y)$

$(x \ne y \c \false)$ <=  $(x = y)$

$(x \ne y \c \ex x \And \Not(x = y))$ <=

$(x \ne y \c \ex y \And \Not(x = y))$ <=

$(x \ne y \And \pvar \c y \ne x \And \pvar)$ <=

$(x \ne y \And \pvar \Iff y \ne x \And \pvar)$ <=

$(x \ne y \c \ex x \And \ex y )$ <=

$(x \ne y \c \ex x \And \ex y \And x \ne y)$ <=

$(x \ne y \c \ex x \And x \ne y)$ <=

$(x \ne y \c \ex y \And x \ne y)$ <=

$(x \ne y \c \ex x \And \ex y \And \Not(x = y))$ <=

$(\ex x \And \ex y \And \Not(x = y))$ <= $(x \ne y)$

$(\ex x \And \Not(x = y))$ <= $(x \ne y)$

$(\ex y \And \Not(x = y))$ <= $(x \ne y)$

$(\ex x \And \ex y )$ <= $(x \ne y)$

$(\pvar \And \ex x \And \ex y \And \Not(x = y))$ <= $(\pvar \And x \ne y)$

$(\pvar \And \ex x \And \Not(x = y))$ <= $(\pvar \And x \ne y)$

$(\pvar \And \ex y \And \Not(x = y))$ <= $(\pvar \And x \ne y)$

$(\pvar \And \ex x \And \ex y )$ <= $(\pvar \And x \ne y)$
\lineb

Exactly Once Sentential Connector
\lineb

$(\pvar \And \Not\qvar \c \pvar \Onr \qvar)$ <=

$(\Not\pvar \And \qvar \c \pvar \Onr \qvar)$ <=

$(\pvar \Onr \qvar)$ <= $(\pvar \And \Not\qvar)$

$(\pvar \Onr \qvar)$ <= $(\Not\pvar \And \qvar)$ 

$(\pvar \Onr \qvar)$ <= $\pvar $,$\Not\qvar$

$(\pvar \Onr \qvar)$ <= $\Not\pvar$,$\qvar$ 

$(\pvar \Onr \qvar)$ <= $\pvar$,$\Not\qvar$

$(\pvar \Onr \qvar)$ <= $\Not\pvar $,$ \qvar$ 

$((\pvar \And \Not\qvar) \Or (\Not\pvar \And \qvar))$ <= $(\pvar \Onr \qvar)$

$((\Not\pvar \And \qvar) \Or (\pvar \And \Not\qvar))$ <= $(\pvar \Onr \qvar)$

$((\pvar \Onr \qvar)\c (\pvar \And \Not\qvar) \Or (\Not\pvar \And \qvar))$ <= 

$((\pvar \Onr \qvar)\c (\Not\pvar \And \qvar) \Or (\pvar \And \Not\qvar))$ <= 

\lineb

Miscellaneous
\lineb

$(\pvar \c \qvar \Iff \rvar)$ <= $(\pvar \And \qvar \c \rvar)$,$(\pvar \And \rvar \c \qvar)$

$(\pvar \c \rvar)$ <= $(\pqvar \And \prvar \c \rvar \Iff \pvar \Or \qvar)$;$\pqvar$,$\prvar$

$(\qvar \c \rvar)$ <= $(\pqvar \And \prvar \c \rvar \Iff \pvar \Or \qvar)$;$\pqvar$,$\prvar$

$(\pvar \And \qvar \c \rvar)$<= $(\pvar \And \pqvar \c (\qvar \c \rvar))$;$\pqvar$

$(\Not \Some x (\pbar x \And \qbar x) \c \Each x (\pbar x \c \Not \qbar x))$<= 

$(\Not \Each x (\pbar x \c \qbar x) \c \Some x (\pbar x \And \Not \qbar x))$<= 

%\noindent{\bf{10. Logic Facts}}

$(\pvar \And x = y \c \pvar \And y = x)$ <=

$(x \ident y) $<= $(\pvar \c x = y)$; $\pvar$

$(x \ident y)$ <= $(\pvar \c y = x)$; $\pvar$

$(x \ident y) $<= $(\pvar \Iff x = y)$; $\pvar$

$(x \ident y)$ <= $(\pvar \Iff y = x)$; $\pvar$

$(\pvar \c x \ident y)$ <= $(y \ident x)$

$(\vbar x \ident \vbar y) $<= $(\pvar \c x \ident y)$; $\pvar$

$(\vbar x \ident \vbar y)$ <= $(\pvar \c y \ident x)$; $\pvar$

$\Some x,y(\pbar x \And \pbar y \And x\ne y)$ <= $\Not\Unq t \pbar t$ 

$(\Each x (\rbar x \c \pbar x \Or \qbar x) \c \Some x(\rbar x \And \pbar x) \Or \Each x(\rbar x \c \qbar x))$<=

$(\Each x (\rbar x \c \pbar x \Or \qbar x) \c \Each x(\rbar x \c \qbar x)\Or \Some x(\rbar x \And \pbar x) )$<=

$(\Each x (\rbar x \c \qbar x \Or \pbar x) \c \Some x(\rbar x \And \pbar x) \Or \Each x(\rbar x \c \qbar x))$<=

$(\Each x (\rbar x \c \qbar x \Or \pbar x) \c \Each x(\rbar x \c \qbar x)\Or \Some x(\rbar x \And \pbar x) )$<=

$(\Some x(\rbar x \And \pbar x) \Or \Each x(\rbar x \c \qbar x))$<= $\Each x (\rbar x \c \pbar x \Or \qbar x)$

$(\Each x(\rbar x \c \qbar x)\Or \Some x(\rbar x \And \pbar x) )$<= $\Each x (\rbar x \c \pbar x \Or \qbar x)$

$(\Some x(\rbar x \And \pbar x) \Or \Each x(\rbar x \c \qbar x))$<= $\Each x (\rbar x \c \qbar x \Or \pbar x)$ 

$(\Each x(\rbar x \c \qbar x)\Or \Some x(\rbar x \And \pbar x) )$<= $\Each x (\rbar x \c \qbar x \Or \pbar x)$

$\ex x$ <= $(x = y)$

$\ex y$ <= $(x = y)$

$(x = y \c \ex x)$ <=

$(x = y \c \ex y)$ <=

$(x = x)$ <= $\ex x$

$(x = y)$ <= $(y = x)$

$(y = x\And y = z \c z = x)$ <=

$(x = y\And z = y \c x = z)$ <=

$(x = y \And y = z \c z = x)$ <=

$(y \ident z \And x = z \c x = y)$ <=

$(\pvar \c x = y)$ <= $(y = x)$

$(x = y \Iff  y = x)$ <=

$(x = y \c  y = x)$ <=

$(x = y \c  x \ident y)$ <=

$(x \ident y)$ <= $(x = y)$

$\Some x (x = u \And  \pbar x)$ <= $(\pbar a \c \ex a)$ U $\pbar u$

$(\pbar y \Iff \Some x (x = y \And  \pbar x))$ <= $(\pbar a \c \ex a)$ U 
\lineb

Exclusive Or Rules

$(\pvar \Onr \rvar \Iff \qvar \Onr \rvar)$ <= $(\pvar \Iff \qvar)$

$(\rvar \Onr \pvar \Iff \rvar \Onr \qvar)$ <= $(\pvar \Iff \qvar)$

$(\pvar \Onr \rvar \Iff \qvar \Onr \rvar)$ <= $(\qvar \Iff \pvar)$

$(\rvar \Onr \pvar \Iff \rvar \Onr \qvar)$ <= $(\qvar \Iff \pvar)$
\lineb

Deep Context Rules

$(\rvar \c \Each x (\pbar x \c \qvar))$ <= $\qvar$
\lineb

Compound Rules 
\lineb

$\qvar$ <= $(\pqvar \c \qvar)$;($(\prvar \c \pqvar)$;$\prvar$)

$\pvar$ <=  $(\qvar \c \pvar)$;($(\qvar \Iff \rvar)$; $\rvar$)

$\qvar$ <= $(\pvar \And \pqvar \c \qvar)$;($(\prvar \c \pqvar)$;$\prvar$),$\pvar$

$\qvar$ <= $(\pvar \And \pqvar \c \qvar)$;$\pvar$,($(\prvar \c \pqvar)$;$\prvar$)

$(\pvar \c \qvar )$ <= $(\qvar \Iff \pvar \And\Each x \qbar x \And \svar)$;($\qbar a$ U),$\svar$ 

$(\pvar \c \qvar )$ <= $(\qvar \Iff \pvar \And\Each x \qbar x \And \svar)$;$\svar$,($\qbar a$ U)

$(\pvar \c \qvar )$ <= $(\qvar \Iff \pvar \And\Each x \qbar x \And \svar)$;($(\rvar \c \svar)$; $\rvar$ ),($\qbar a$ U)

$(\pvar \c \qvar )$ <= $(\qvar \Iff \pvar \And\Each x \qbar x \And \svar)$;($\qbar a$ U),($(\rvar \c \svar)$; $\rvar$ )

$(\pvar \c \qvar)$<=$(\pvar \And \rvar \c \qvar)$;($(\pqvar \And\prvar \And \psvar\c \rvar)$;$\pqvar$,$\prvar$,$\psvar$)

$\qvar$<=$(\qvar \Iff \rvar \And \Each x \pbar x)$;($\pbar a$ U),($(\pqvar \And \prvar \c\rvar)$;$\pqvar$,$\prvar$)

$\qvar$<=$(\qvar \Iff \rvar \And \Each x \pbar x)$;($(\pqvar \And \prvar \c\rvar)$;$\pqvar$,$\prvar$),($\pbar a$ U)

$\rvar$<=$(\pvar \And \qvar \c \rvar)$;$\pvar$,($(\pqvar \And \prvar \c \qvar)$;$\pqvar$,$\prvar$)

$\rvar$<=$(\pvar \And \qvar \c \rvar)$;($(\pqvar \And \prvar \c \qvar)$;$\pqvar$,$\prvar$),$\pvar$

$\qvar$ <= $(\pvar \And \pqvar \And \psvar\c \qvar)$;($(\prvar \c \pqvar)$;$\prvar$),$\pvar$,$\psvar$

$\qvar$ <= $(\pvar \And \pqvar \And \psvar\c \qvar)$;$\psvar$,($(\prvar \c \pqvar)$;$\prvar$),$\pvar$

$\qvar$ <= $(\pvar \And \pqvar \And \psvar\c \qvar)$;$\pvar$,$\psvar$,($(\prvar \c \pqvar)$;$\prvar$)

$\qvar$ <= $(\pvar \And \pqvar \And \psvar\c \qvar)$;($(\prvar \Iff \pqvar)$;$\prvar$),$\pvar$,$\psvar$

$\qvar$ <= $(\pvar \And \pqvar \And \psvar\c \qvar)$;$\psvar$,($(\prvar \Iff \pqvar)$;$\prvar$),$\pvar$

$\qvar$ <= $(\pvar \And \pqvar \And \psvar\c \qvar)$;$\pvar$,$\psvar$,($(\prvar \Iff \pqvar)$;$\prvar$)

$\qvar$ <= $(\pvar \And \pqvar \And \psvar \And \rvar \c \qvar)$;$\rvar$,$\pvar$,$\psvar$,($(\prvar \c \pqvar)$;$\prvar$)

$\qvar$ <= $(\pvar \And \pqvar \And \psvar \And \rvar \c \qvar)$;$\rvar$,$\psvar$,($(\prvar \c \pqvar)$;$\prvar$),$\pvar$

$\qvar$ <= $(\pvar \And \pqvar \And \psvar \And \rvar \c \qvar)$;$\rvar$,($(\prvar \c \pqvar)$;$\prvar$),$\pvar$,$\psvar$

$\qvar$ <= $(\pvar \And \pqvar \And \psvar \And \rvar \c \qvar)$;($(\prvar \c \pqvar)$;$\prvar$),$\pvar$,$\psvar$,$\rvar$

$\pvar$<= $(\pvar \Iff \qvar \And \rvar)$;$\qvar$,($(\pqvar \Iff \rvar)$; $\pqvar$)

$\pvar$<= $(\pvar \Iff \qvar \And \rvar)$;($(\pqvar \Iff \rvar)$; $\pqvar$),$\qvar$

$\pvar$<= $(\pvar \Iff \qvar \And \rvar)$;$\qvar$,($(\rvar \Iff \pqvar)$; $\pqvar$)

$\pvar$<= $(\pvar \Iff \qvar \And \rvar)$;($(\rvar \Iff \pqvar)$; $\pqvar$),$\qvar$

$\qvar$ <= $(\pvar \Iff \qvar)$;($(\rvar \c \pvar)$;$\rvar$)

$\qvar$ <= $(\qvar \Iff \pvar)$;($(\rvar \c \pvar)$;$\rvar$)

$\qvar$ <= $(\pvar \Iff \qvar)$;($(\rvar \Iff \pvar)$;$\rvar$)

$\qvar$ <= $(\pvar \Iff \qvar)$;($(\pvar \Iff \rvar)$;$\rvar$)

$\qvar$ <= $(\qvar \Iff \pvar)$;($(\rvar \Iff \pvar)$;$\rvar$)

$\qvar$ <= $(\qvar \Iff \pvar)$;($(\pvar \Iff \rvar)$;$\rvar$)

$\rvar $ <=$(\rvar\Iff \pvar \And \qvar)$;($(\pvar \Iff \pqvar \And \prvar)$;$\pqvar$,$\prvar$),$\qvar$

$\rvar $ <=$(\rvar\Iff \pvar \And \qvar)$;$\qvar$,($(\pvar \Iff \pqvar \And \prvar)$;$\pqvar$,$\prvar$)

$\rvar$ <= ($(\pvar \c \qvar)$ - $(\qvar \c \rvar)$) ; $\pvar$

$\rvar$ <= $(\qvar \c \rvar)$; ($(\pqvar \And \prvar \c \qvar)$;$\pvar$,$\pqvar$)

$\qvar$ <= $(\pvar \c \qvar)$;($(\rvar \Iff \pvar \And \svar)$; $\rvar$)

$\qvar$ <= $(\pvar \c \qvar)$;($(\pvar \And \svar\Iff \rvar)$; $\rvar$)

$\rvar$ <= $(\rvar \Iff \pvar \And \qvar)$; $\pvar$,($(\pqvar \And \prvar \c \qvar)$;$\pqvar$,$\prvar$)

$\rvar$ <= $(\pvar \And \qvar\Iff \rvar)$; $\pvar$,($(\pqvar \And \prvar \c \qvar)$;$\pqvar$,$\prvar$)

$\rvar$ <= $(\rvar \Iff \pvar \And \qvar)$; ($(\pqvar \And \prvar \c \qvar)$;$\pqvar$,$\prvar$),$\pvar$

$\rvar$ <= $(\pvar \And \qvar\Iff\rvar)$; ($(\pqvar \And \prvar \c \qvar)$;$\pqvar$,$\prvar$),$\pvar$

$(\qvar \c \pvar)$<= $(\pvar \Iff \qvar \And \rvar)$;($(\pqvar \Iff \rvar)$;$\pqvar$)

$(\qvar \c \pvar)$<= $(\pvar \Iff \qvar \And \rvar)$;($(\rvar \Iff \pqvar)$;$\pqvar$)

$(\pvar \c \qvar)$<= $(\ppvar \And \pqvar \c \qvar \Iff \pvar)$;$\ppvar$,($(\svar\c\pqvar)$;$\svar$)

$(\pvar \c \qvar)$<= $(\ppvar \And \pqvar \c \qvar \Iff \pvar)$;($(\svar\c\pqvar)$;$\svar$),$\ppvar$

$(\pvar \c \qvar)$<= $(\ppvar \And \pqvar \c \pvar \Iff \qvar)$;$\ppvar$,($(\svar\c\pqvar)$;$\svar$)

$(\pvar \c \qvar)$<= $(\ppvar \And \pqvar \c \pvar \Iff \qvar)$;($(\svar\c\pqvar)$;$\svar$),$\ppvar$

$(\qvar \c \pvar)$ <= $(\pvar \Iff \qvar \And \rvar \And \svar)$;$\rvar$,($(\tvar \c \svar)$; $\tvar$)

$(\qvar \c \pvar)$ <= $(\pvar \Iff \qvar \And \rvar \And \svar)$;($(\tvar \c \svar)$; $\tvar$),$\rvar$

$(\pvar \c \qvar)$<=$(\pqvar \And \prvar \c \pvar \Iff \qvar)$;($(\qpvar \c \pqvar)$;$\qpvar$),($(\rpvar \c \prvar)$;$\rpvar$)

$(\pvar \c \qvar)$<=$(\pqvar \And \prvar \c \qvar \Iff \pvar)$;($(\qpvar \c \pqvar)$;$\qpvar$),($(\rpvar \c \prvar)$;$\rpvar$)

$(\rvar \Or \pvar \c \rvar \Or \qvar)$ <= $(\pqvar\And\prvar\c\qvar \Iff\pvar)$;$\pqvar$,($(\psvar \c \prvar)$;$\psvar$)

$(\rvar \Or \pvar \c \rvar \Or \qvar)$ <= $(\pqvar\And\prvar\c\qvar \Iff\pvar)$;($(\psvar \c \prvar)$;$\psvar$),$\pqvar$

$(\qvar \c \pvar)$ <= $(\qvar \And \rvar \And \svar\Iff\pvar)$;$\rvar$,($(\tvar \c \svar)$; $\tvar$)

$(\qvar \c \pvar)$ <= $(\qvar \And \rvar \And \svar\Iff\pvar)$;($(\tvar \c \svar)$; $\tvar$),$\rvar$

$(\pvar \c \qvar)$ <= $(\pvar \And \pqvar \c \qvar)$;($(\prvar \c \pqvar)$;$\prvar$)

$(\pvar \c \qvar)$ <= $(\pvar \And \pqvar \c \qvar)$;($(\prvar \And \psvar \c \pqvar)$;$\prvar$,$\psvar$)

$(\pvar \c \svar)$ <= $(\pvar \And \qvar \And \rvar \c \svar)$;($(\pqvar \c \qvar)$;$\pqvar$),$\rvar$

$(\pvar \c \svar)$ <= $(\pvar \And \qvar \And \rvar \c \svar)$;$\rvar$,($(\pqvar \c \qvar)$;$\pqvar$)

$(\pvar \c \qvar)$ <= $(\rvar \c \pvar \Iff \qvar)$ ; ( $(\svar \c \rvar)$; $\svar$ )

$(\pvar \c \qvar)$ <= $(\rvar \c \qvar \Iff \pvar)$ ; ( $(\svar \c \rvar)$; $\svar$ )

$(\pvar \c \qvar)$ <= $(\pvar \And \rvar \c \qvar)$;($(\svar \Iff \rvar)$;$\svar$)

$(\pvar \c \qvar)$ <= $(\pvar \And \tvar\Iff \qvar)$;($(\svar \c \tvar)$;$\svar$)

$(\pvar \c \qvar)$ <= $(\qvar \Iff \pvar \And \tvar)$;($(\svar \c \tvar)$;$\svar$)

$(\svar \c \rvar)$ <= $(\qvar \c \rvar)$;($(\pvar \c \qvar)$;$\pvar$)

$(\pvar \c \qvar)$ <= $(\pvar \And \rvar \c \qvar)$;($(\rvar \Iff \svar)$;$\svar$)

$(\pvar \c \qvar)$ <= $(\pvar \And \rvar \c \qvar)$;($(\svar \Iff \rvar)$;$\svar$)

$(\pvar \c \pvar \And \qvar)$<= $(\pqvar \Iff \qvar)$;($(\rvar \c \pqvar)$;$\rvar$)

$(\pvar \c \pvar \And \qvar)$<= $(\qvar \Iff \pqvar)$;($(\rvar \c \pqvar)$;$\rvar$)

$(\pvar \c \pvar \And \qvar)$<= $(\rvar \c \qvar)$;($(\pqvar \And \prvar \c \rvar)$;$\pqvar$,$\prvar$)

$(\pvar \And \rvar \c \qvar \And \rvar)$ <= $(\pvar \And \svar \c \qvar)$; ($(\tvar \c \svar)$; $\tvar$)

$(\pvar \c \pvar \And \rvar)$ <= $(\pvar \And \qvar \c \rvar)$ ;($(\svar \c \qvar)$; $\svar$)

$(\pvar \Or \rvar\c \qvar\Or \rvar)$ <= $(\pvar \And \pqvar \c \qvar)$;($(\prvar \Iff \pqvar)$;$\prvar$)

$(\rvar \Or \pvar \c\rvar \Or  \qvar)$ <= $(\pvar \And \pqvar \c \qvar)$;($(\prvar \Iff \pqvar)$;$\prvar$)

$(\pvar \Or \rvar\c \qvar\Or \rvar)$ <= $(\pvar \And \pqvar \c \qvar)$;($(\pqvar \Iff \prvar)$;$\prvar$)

$(\rvar \Or \pvar \c\rvar \Or  \qvar)$ <= $(\pvar \And \pqvar \c \qvar)$;($(\pqvar \Iff \prvar)$;$\prvar$)

$(\pvar \c \qvar)$<=$(\pvar \And \rvar \c \qvar)$;($(\svar \Iff  \rvar \And \tvar)$;$\svar$)

$(\pvar \c \qvar)$<=$(\pvar \And \rvar \c \qvar)$;($(\rvar \And \tvar\Iff \svar)$;$\svar$)

$(\pvar \c \rvar)$ <= $(\pvar \And \qpvar \And \qqvar\And \qrvar \c \rvar)$; $\qpvar$,$\qqvar$,($(\pqvar \c \qrvar)$;$\pqvar$)

$(\pvar \c \rvar)$ <= $(\pvar \And \qpvar \And \qqvar\And \qrvar \c \rvar)$; ($(\pqvar \c \qrvar)$;$\pqvar$),$\qpvar$,$\qqvar$

$(\pvar \c \rvar)$ <= $(\pvar \And \qpvar \And \qqvar\And \qrvar \c \rvar)$; $\qpvar$,($(\pqvar \c \qrvar)$;$\pqvar$),$\qqvar$

$(\pvar \Or \rvar\c \qvar \Or \rvar)$ <= $(\pvar \And \svar \c \qvar)$;($(\ppvar \And \pqvar \c \svar)$;$\ppvar$,$\pqvar$)

$(\rvar \Or \pvar\c \rvar \Or \qvar)$ <= $(\pvar \And \svar \c \qvar)$;($(\ppvar \And \pqvar \c \svar)$;$\ppvar$,$\pqvar$)

$\pvar$<=$(\qvar \And \rvar \c \pvar)$;$\rvar$,($(\pqvar \c \prvar)$-$(\qvar \Iff \prvar)$)

$\pvar$<=$(\qvar \And \rvar \c \pvar)$;$\rvar$,($(\pqvar \c \prvar)$-$(\prvar \Iff \qvar)$)

$\pvar$<=$(\qvar \And \rvar \c \pvar)$;($(\pqvar \c \prvar)$-$(\qvar \Iff \prvar)$),$\rvar$

$\pvar$<=$(\qvar \And \rvar \c \pvar)$;($(\pqvar \c \prvar)$-$(\prvar \Iff \qvar)$),$\rvar$

$(\pvar \c \rvar)$<=$(\rvar \Iff \pvar\And \qvar)$;($(\qvar \Iff \pqvar \And \prvar)$;$\pqvar$,$\prvar$)

$(\pvar \c \rvar)$<=$(\pvar\And \qvar\Iff \rvar)$;($(\qvar \Iff \pqvar \And \prvar)$;$\pqvar$,$\prvar$)

$(\pvar \c \rvar)$<=$(\rvar \Iff \pvar\And \qvar)$;($(\pqvar \And \prvar\Iff \qvar)$;$\pqvar$,$\prvar$)

$(\pvar \c \rvar)$<=$(\pvar\And \qvar\Iff \rvar)$;($(\pqvar \And \prvar\Iff \qvar)$;$\pqvar$,$\prvar$)

$\rvar$<=$(\pvar \And \qvar \c \rvar)$;$\pvar$,($(\pqvar \Iff \qvar)$;$\pqvar$)

$\rvar$<=$(\pvar \And \qvar \c \rvar)$;$\pvar$,($(\qvar \Iff \pqvar)$;$\pqvar$)

$\rvar$<=$(\pvar \And \qvar \c \rvar)$;($(\pqvar \Iff \qvar)$;$\pqvar$),$\pvar$

$\rvar$<=$(\pvar \And \qvar \c \rvar)$;($(\qvar \Iff \pqvar)$;$\pqvar$),$\pvar$

$\qvar$<=$(\qvar \Iff \pqvar \And \prvar)$;($(\qpvar \And \qqvar \And \qrvar \c \pqvar)$;$\qpvar$ ,$\qqvar$ ,$\qrvar$ ),$\prvar$

$\qvar$<=$(\qvar \Iff \pqvar \And \prvar)$;$\prvar$,($(\qpvar \And \qqvar \And \qrvar \c \pqvar)$;$\qpvar$ ,$\qqvar$ ,$\qrvar$ )

$\rvar $ <=$(\pvar \And \qvar \c \rvar)$;($(\pqvar \c \pvar)$;$\pqvar$),($(\prvar\c\qvar)$;$\prvar$)

$\Not \pvar $ <= $(\pvar \And \qvar \c \false)$; $\qvar$

$\Not \pvar $ <= $(\pvar \And \qvar \c \false)$; ($(\svar \c \qvar)$; $\svar$)

$(\Not\pvar \c\qvar )$<=$(\pvar \Iff \Not\qvar \And \rvar)$;($(\pqvar \c \rvar)$;$\pqvar$)
\lineb

Compound Case Elimination 
\lineb
$( \pvar \Or \qvar \c \pvar)$<= $(\rvar \c \Not\qvar)$; $\rvar$

$( \qvar \Or \pvar \c \pvar)$<= $(\rvar \c \Not\qvar)$; $\rvar$
\lineb

Compound Nesting of Hypothesis
\lineb

$(\pvar \c\rvar )$<=$(\qvar \c \rvar)$;($(\pvar \And \prvar \c \qvar)$; $\prvar$)

Compound Replacing a Disjunct
\lineb


$(\pvar \Or \rvar \c \qvar \Or \rvar)$<=$(\pvar \And \pqvar \And \prvar \c \qvar)$;$\pqvar$,($(\qpvar \c \prvar)$;$\qpvar$)

$(\pvar \Or \rvar \c \qvar \Or \rvar)$<=$(\pvar \And \pqvar \And \prvar \c \qvar)$;($(\qpvar \c \prvar)$;$\qpvar$),$\pqvar$

$(\rvar \Or \pvar \c \rvar \Or \qvar)$<=$(\pvar \And \pqvar \And \prvar \c \qvar)$;$\pqvar$,($(\qpvar \c \prvar)$;$\qpvar$)

$(\rvar \Or \pvar \Or \c \rvar \Or \qvar)$<=$(\pvar \And \pqvar \And \prvar \c \qvar)$;($(\qpvar \c \prvar)$;$\qpvar$),$\pqvar$

$(\rvar \Or \pvar \c \rvar \Or \qvar)$ <= $(\pqvar\And\prvar\c\qvar \Iff\pvar)$;($(\qpvar \c \pqvar)$;$\qpvar$),($(\psvar \c \prvar)$;$\psvar$)

\lineb

Compound Pick Minor Premise from a Conjunction
\lineb

$(\tvar \c \tvar \And \rvar)$<=$(\pvar \And \qvar \c \rvar)$ ;$(\qvar \And \svar)$,($(\pqvar \c \pvar)$;$\pqvar$)

$(\tvar \c \tvar \And \rvar)$<=$(\pvar \And \qvar \c \rvar)$ ;($(\pqvar \c \pvar)$;$\pqvar$),$(\qvar \And \svar)$

$(x \in A \c \pbarp xy)$ <= $\Each t \in A \Each u \in B \pbarp tu$;$(\pvar \And y \in B)$

$(y \in B \c \pbarp xy)$ <= $\Each t \in A \Each u \in B \pbarp tu$;$(\pvar \And x \in A)$

\lineb

Compound Pick Conclusion from a Conjunction
\lineb

$(\rvar \c \pvar)$ <=  $(\pvar \And \qvar)$

$\pqvar$<= $(\pqvar \And \prvar \Iff \qvar)$;($(\pvar \c \qvar)$;$\pvar$)

$\pqvar$<= $(\qvar \Iff \pqvar \And \prvar )$;($(\pvar \c \qvar)$;$\pvar$)
\lineb

Compound Equality Substitution
\lineb

$(\pbar x \c \pbar y)$<= $(\pvar \And\qvar\c x = y)$; $\pvar$,($(\pqvar \c\qvar)$;$\pqvar$)

$(\pbar x \c \pbar y)$<= $(\pvar \And\qvar\c x = y)$; ($(\pqvar \c\qvar)$;$\pqvar$),$\pvar$
 
\lineb

Compound Indefinite Description
\lineb

$\pbar x$<=$(x \ident \an s \pbar s)$,($(\pvar \c \Some s \pbar s)$;$\pvar$)

$\pbar x$<= ($(\pvar \c \Some s \pbar s)$;$\pvar$),$(x \ident \an s \pbar s)$

$\pbar x$<=$(x \ident \an s \pbar s)$,($(\pvar \Iff \Some s \pbar s)$;$\pvar$)

$\pbar x$<= ($(\pvar \Iff \Some s \pbar s)$;$\pvar$),$(x \ident \an s \pbar s)$

$\pbar x$<=$(x \ident \an s \pbar s)$,($(\Some s \pbar s\Iff\pvar)$;$\pvar$)

$\pbar x$<= ($(\Some s \pbar s\Iff \pvar)$;$\pvar$),$(x \ident \an s \pbar s)$
\lineb

Nested Compounding
\lineb

$(\pvar \c \qvar)$ <= $(\pvar \And \rvar \c \qvar)$;($(\svar \c \rvar)$;($(\svar \Iff \pqvar)$;$\pqvar$))

$(\pvar \c \qvar)$ <= $(\pvar \And \rvar \c \qvar)$;($(\svar \c \rvar)$;($(\pqvar \Iff \svar)$;$\pqvar$))

$(\pvar \c \qvar)$ <= $(\pvar \And \rvar \c \qvar)$;($(\svar \c \rvar)$;($(\pqvar \c \svar)$;$\pqvar$))

$(\pvar \c \qvar)$ <= $(\pvar \And \rvar \c \qvar)$;($(\rvar \Iff \svar)$;($(\pqvar \c \svar)$;$\pqvar$))

$(\pvar \c \qvar)$ <= $(\pvar \And \rvar \c \qvar)$;($(\svar \Iff \rvar)$;($(\pqvar \c \svar)$;$\pqvar$))

$(\qvar \c \rvar)$ <=$(\rvar\Iff \pvar \And \qvar)$;($(\pvar \Iff \pqvar \And \prvar)$;$\pqvar$,($(\qpvar \c \prvar)$;$\qpvar$))

$\rvar $ <=$(\rvar\Iff \pvar \And \qvar)$;($(\pvar \Iff \pqvar \And \prvar)$;$\pqvar$,($(\qpvar \c \prvar)$;$\qpvar$)),$\qvar$

$\rvar $ <=$(\rvar\Iff \pvar \And \qvar)$;$\qvar$,($(\pvar \Iff \pqvar \And \prvar)$;$\pqvar$,($(\qpvar \c \prvar)$;$\qpvar$))

$(\qvar \c \pvar)$<= $(\pvar \Iff \qvar \And \rvar)$;($(\rvar \Iff \pqvar)$;($(\prvar \c \pqvar)$;$\prvar$))

$(\qvar \c \pvar)$<= $(\pvar \Iff \qvar \And \rvar)$;($(\pqvar \Iff \rvar)$;($(\prvar \c \pqvar)$;$\prvar$))

$(\qvar \c \pvar)$<= $(\qvar \And \rvar \Iff \pvar)$;($(\rvar \Iff \pqvar)$;($(\prvar \c \pqvar)$;$\prvar$))

$(\qvar \c \pvar)$<= $(\qvar \And \rvar \Iff \pvar)$;($(\pqvar \Iff \rvar)$;($(\prvar \c \pqvar)$;$\prvar$))

$(\ubar x \ident \ubar y)$ <= $(\pvar \c y = x)$;($(\prvar\Iff\pvar)$;($(\pqvar\c\prvar)$;$\pqvar$))

$(\ubar x \ident \ubar y)$ <= $(\pvar \c y = x)$;($(\pvar\Iff\prvar)$;($(\pqvar\c\prvar)$;$\pqvar$))

$(\ubar x \ident \ubar y)$ <= $(\pvar \c x = y)$;($(\prvar\Iff\pvar)$;($(\pqvar\c\prvar)$;$\pqvar$))

$(\ubar x \ident \ubar y)$ <= $(\pvar \c x = y)$;($(\pvar\Iff\prvar)$;($(\pqvar\c\prvar)$;$\pqvar$))

$(\pvar \c\qvar )$<=$(\prvar \c \qvar )$;($(\pqvar \And \pvar \c \prvar)$;($(\ptvar \c \pqvar)$;$\ptvar$))

\lineb

Pick Minor Premise from Conjunction
\lineb

$(\rvar \c \qvar\And \rvar)$ <= $(\pvar \c \qvar )$;$(\pvar\And \svar)$

$\qvar$ <=  $(\pvar \c \qvar)$; $(\pvar \And \rvar)$

$(\pvar \c \false)$ <= $(\qvar \And \Not \pvar)$

$\rvar$<= $(\pvar \And \qvar \c \rvar)$ ; $\pvar$, $(\qvar \And \svar)$

$\rvar$<= $(\pvar \And \qvar \c \rvar)$ ; $(\qvar \And \svar)$,$\pvar$

$\svar$ <=  $(\pvar \And \qvar\And \rvar\c \svar)$;$\pvar$,$\qvar$,$(\pqvar \And \rvar)$

$\svar$ <=  $(\pvar \And \qvar\And \rvar\c \svar)$;$\qvar$,$(\pqvar \And \rvar)$,$\pvar$

$\svar$ <=  $(\pvar \And \qvar\And \rvar\c \svar)$;$(\pqvar \And \rvar)$,$\pvar$,$\qvar$

$(\tvar \c \tvar \And \rvar)$<=$(\pvar \And \qvar \c \rvar)$ ; $\pvar$, $(\qvar \And \svar)$

$(\tvar \c \tvar \And \rvar)$<=$(\pvar \And \qvar \c \rvar)$ ; $(\qvar \And \svar)$,$\pvar$

$(\pvar \c \qvar)$<=$(\pvar \And \rvar \c \qvar)$ ;  $(\rvar \And \svar)$

$(\tvar \c \tvar \And \svar)$<=  $(\pvar \And \qvar\And \rvar\c \svar)$;$\pvar$,$\qvar$,$(\pqvar \And \rvar)$

$(\tvar \c \tvar \And \svar)$<=  $(\pvar \And \qvar\And \rvar\c \svar)$;$\qvar$,$(\pqvar \And \rvar)$,$\pvar$

$(\tvar \c \tvar \And \svar)$<=  $(\pvar \And \qvar\And \rvar\c \svar)$;$(\pqvar \And \rvar)$,$\pvar$,$\qvar$
\lineb

Pick a Premise from a conjunction and pass the other conjunct

\lineb
$(\qvar \And \svar)$<=$(\pqvar \And \prvar \And\psvar \c \qvar)$;$\pqvar$,$\prvar$,$(\psvar \And \svar)$

$(\qvar \And \svar)$<=$(\pqvar \And \prvar \And\psvar \c \qvar)$;$\prvar$,$(\psvar \And \svar)$,$\pqvar$

$(\qvar \And \svar)$<=$(\pqvar \And \prvar \And\psvar \c \qvar)$;$(\psvar \And \svar)$,$\pqvar$,$\prvar$


Compound Universalized Premise
\lineb

$\qvar$<=$(\Each x \pbar x\c \qvar)$;($\pbar a$ U)

$\qvar$<=$(\Each x \pbar x\Iff \qvar)$;($\pbar a$ U)

$\qvar$<=$(\qvar \Iff \Each x \pbar x)$;($\pbar a$ U)

$(\pvar \c \qvar)$<=$(\Each x \pbar x\c \qvar)$;($\pbar a$ U)

$\qvar$<=$(\Each x \Each y \pbarp xy \c \qvar)$;($\pbarp ab$ U)

$\qvar$<=$(\Each x \Each y \pbarp xy \Iff \qvar)$;($\pbarp ab$ U)

$\qvar$<=$(\qvar \Iff \Each x \Each y \pbarp xy)$;($\pbarp ab$ U)

$\qvar$<=$(\pqvar \And \Each x \pbar x\c \qvar)$;($\pbar a$ U),$\pqvar$

$\qvar$<=$(\pqvar \And \Each x \pbar x\c \qvar)$;$\pqvar$,($\pbar a$ U)

$\qvar$<=$(\pqvar \And \Each x \pbar x\c \qvar)$;($\pbar a$ U),($(\prvar\c\pqvar)$;$\prvar$)

$\qvar$<=$(\pqvar \And \Each x \pbar x\c \qvar)$;($(\prvar\c\pqvar)$;$\prvar$),($\pbar a$ U)

$(\pqvar \c \qvar)$<=$(\pqvar \And \Each x \pbar x\c \qvar)$;($\pbar a$ U)

$(\pqvar \c\qvar)$<=$(\pqvar \And \prvar \And \Each x \pbar x\c \qvar)$;$\prvar$,($\pbar a$ U)

$(\pqvar \c \qvar)$<=$(\pqvar \And \prvar \And \Each x \pbar x\c \qvar)$;($\pbar a$ U),$\prvar$

$\qvar$<=$(\pqvar \And \prvar \And \Each x \pbar x\c \qvar)$;$\pqvar$,$\prvar$,($\pbar a$ U)

$\qvar$<=$(\pqvar \And \prvar \And \Each x \pbar x\c \qvar)$;$\pqvar$,($\pbar a$ U),$\prvar$

$\qvar$<=$(\pqvar \And \prvar \And \Each x \pbar x\c \qvar)$;($\pbar a$ U),$\prvar$,$\pqvar$

$\qvar$<=$(\pqvar \And \Each x \pbar x\Iff \qvar)$;$\pqvar$,($\pbar a$ U)

$\qvar$<=$(\qvar \Iff \pqvar \And \Each x \pbar x)$;$\pqvar$,($\pbar a$ U)

$\qvar$<=$(\pqvar \And \Each x \pbar x\Iff \qvar)$;($\pbar a$ U),$\pqvar$

$\qvar$<=$(\qvar \Iff \pqvar \And \Each x \pbar x)$;($\pbar a$ U),$\pqvar$

$\qvar$<=$(\pvar \And \Each x (\pbar x \c \qbar x) \c \qvar)$; ($(\pbar a \Iff \qbar a)$ U),$\pvar$

$\qvar$<=$(\pvar \And \Each x (\pbar x \c \qbar x) \c \qvar)$; ($(\qbar a \Iff \pbar a)$ U),$\pvar$

$\qvar$<=$(\pvar \And \Each x (\pbar x \c \qbar x) \c \qvar)$;$\pvar$,($(\pbar a \Iff \qbar a)$ U)

$\qvar$<=$(\pvar \And \Each x (\pbar x \c \qbar x) \c \qvar)$;$\pvar$,($(\qbar a \Iff \pbar a)$ U)

$\qvar$<=$(\qvar \Iff\pqvar \And \prvar\And \Each x\pbar x)$;$\pqvar$,$\prvar$,($\pbar a$ U)

$\qvar$<=$(\qvar \Iff\pqvar \And \prvar\And \Each x\pbar x)$;$\pqvar$,($\pbar a$ U),$\prvar$

$\qvar$<=$(\qvar \Iff\pqvar \And \prvar\And \Each x\pbar x)$;($\pbar a$ U),$\pqvar$,$\prvar$

$\qvar$<=$(\pqvar \And \prvar \And \Each x\pbar x\Iff\qvar)$;$\pqvar$,$\prvar$,($\pbar a$ U)

$\qvar$<=$(\pqvar \And \prvar \And \Each x\pbar x\Iff\qvar)$;$\pqvar$,($\pbar a$ U),$\prvar$

$\qvar$<=$(\qvar \Iff\pvar \And \prvar\And \Each x\pbar x)$;($\pbar a$ U),$\prvar$,($(\pqvar \c \pvar)$;$\pqvar$)

$\qvar$<=$(\qvar \Iff\pvar \And \prvar\And \Each x\pbar x)$;($\pbar a$ U),($(\pqvar \c \pvar)$;$\pqvar$),$\prvar$

$\qvar$<=$(\qvar \Iff\pvar \And \prvar\And \Each x\pbar x)$;$\prvar$,($\pbar a$ U),($(\pqvar \c \pvar)$;$\pqvar$)

$\qvar$<=$(\qvar \Iff\pvar \And \prvar\And \Each x\pbar x)$;$\prvar$,($(\pqvar \c \pvar)$;$\pqvar$),($\pbar a$ U)

$\qvar$<=$(\qvar \Iff\pvar \And \prvar\And \Each x\pbar x)$;($(\pqvar \c \pvar)$;$\pqvar$),($\pbar a$ U),$\prvar$

$\qvar$<=$(\qvar \Iff\pvar \And \prvar\And \Each x\pbar x)$;($(\pqvar \c \pvar)$;$\pqvar$),$\prvar$,($\pbar a$ U)

$\qvar$<=$(\pqvar \And \prvar \And \Each x\pbar x\Iff\qvar)$;($\pbar a$ U),$\pqvar$,$\prvar$

$\qvar$<=$(\pqvar \And \prvar \c \Each x \pbar x\Iff \qvar)$;$\pqvar$,$\prvar$,($\pbar a$ U)

$\qvar$<=$(\pqvar \And \prvar \c \Each x \pbar x\Iff \qvar)$;$\prvar$,($\pbar a$ U),$\prvar$

$\qvar$<=$(\pqvar \And \prvar \c \Each x \pbar x\Iff \qvar)$;($\pbar a$ U),$\prvar$,$\pqvar$

$\qvar$<=$(\pqvar \And \prvar \c \qvar \Iff\Each x \pbar x)$;$\pqvar$,$\prvar$,($\pbar a$ U)

$\qvar$<=$(\pqvar \And \prvar \c \qvar \Iff\Each x \pbar x)$;$\prvar$,($\pbar a$ U),$\prvar$

$\qvar$<=$(\pqvar \And \prvar \c \qvar \Iff\Each x \pbar x)$;($\pbar a$ U),$\prvar$,$\pqvar$

$\svar$ <=  $(\pvar \And \qvar\And \Each x;\pbar x \Each y;\qbarp xy \rbarp xy \c \svar)$; $\pvar$,$\qvar$,($(\pbar a \And \qbarp ab \c \rbarp ab)$ U )

$\svar$ <=  $(\pvar \And \qvar\And \Each x;\pbar x \Each y;\qbarp xy \rbarp xy \c \svar)$; $\pvar$,($(\pbar a \And \qbarp ab \c \rbarp ab)$ U ),$\qvar$

$\svar$ <=  $(\pvar \And \qvar\And \Each x;\pbar x \Each y;\qbarp xy \rbarp xy \c \svar)$; ($(\pbar a \And \qbarp ab \c \rbarp ab)$ U ),$\qvar$,$\pvar$

$\svar$ <=  $(\pvar \And \qvar\And \Each x,y ;\pbarp xy \Each z;\qbarpp xyz \rbarpp xyz \c \svar)$; ($(\pbarp ab \And \qbarpp abc \c \rbarpp abc)$ U ),$\qvar$,$\pvar$

$\svar$ <=  $(\pvar \And \qvar\And \Each x,y ;\pbarp xy \Each z;\qbarpp xyz \rbarpp xyz \c \svar)$;$\pvar$,($(\pbarp ab \And \qbarpp abc \c \rbarpp abc)$ U ),$\qvar$

$\svar$ <=  $(\pvar \And \qvar\And \Each x,y ;\pbarp xy \Each z;\qbarpp xyz \rbarpp xyz \c \svar)$;$\pvar$,$\qvar$,($(\pbarp ab \And \qbarpp abc \c \rbarpp abc)$ U )

$\svar$ <=  $(\pvar \And \Each x,y ;\pbarp xy \Each z;\qbarpp xyz \rbarpp xyz \c \svar)$; ($(\pbarp ab \And \qbarpp abc \c \rbarpp abc)$ U ),$\pvar$

$\svar$ <=  $(\pvar \And \Each x,y ;\pbarp xy \Each z;\qbarpp xyz \rbarpp xyz \c \svar)$;$\pvar$,($(\pbarp ab \And \qbarpp abc \c \rbarpp abc)$ U )

$\qvar$<=$(\qvar \Iff \pvar \And \Each s\Unq t \pbarp ts)$;($(\pbarp ac \And \pbarp bc \c a = b)$ U),$\pvar$

$\qvar$<=$(\qvar \Iff \pvar \And \Each s\Unq t \pbarp ts)$;$\pvar$,($(\pbarp ac \And \pbarp bc \c a = b)$ U)

$\qvar $<= $(\pvar \c \qvar \Iff \Each x,y \pbarp xy)$; $\pvar$,($\pbarp ab$ U)

$\qvar $<= $(\pvar \c \qvar \Iff \Each x,y \pbarp xy)$; ($\pbarp ab$ U),$\pvar$

\lineb

Ignore Overhanging Premise

$(\rvar \c \qvar)$ <=  $(\pvar \c \qvar)$;$\pvar$
\lineb

Double Compound Universalized Premise
\lineb

$\qvar$<=$(\pvar \And \Each x ;\pbar x \Each y ;\qbar y \rbarp xy\c \qvar)$; $\pvar$,($(\pbar a \And \qbar b \c \rbarp ab)$ U)

$\qvar$<=$(\pvar \And \Each x ;\pbar x \Each y ;\qbar y \rbarp xy\c \qvar)$;($(\pbar a \And \qbar b \c \rbarp ab)$ U),$\pvar$

$\qvar$<=$(\pvar \And \Each x \pbar x \And \Each x \qbar x \c \qvar)$;$\pvar$,($\pbar a$ U),($\qbar b$ U)

$\qvar$<=$(\pvar \And \Each x \pbar x \And \Each x \qbar x \c \qvar)$;($\pbar a$ U),$\pvar$,($\qbar b$ U)

$\qvar$<=$(\pvar \And \Each x \pbar x \And \Each x \qbar x \c \qvar)$;($\pbar a$ U),($\qbar b$ U),$\pvar$

$\qvar$<=$(\pqvar \And \prvar \And \Each x,y \pbarp xy\c \qvar)$;($\pbarp ab$ U),$\pqvar$,$\prvar$

$\qvar$<=$(\pqvar \And \prvar \And \Each x,y \pbarp xy\c \qvar)$;$\prvar$,($\pbarp ab$ U),$\pqvar$

$\qvar$<=$(\pqvar \And \prvar \And \Each x,y \pbarp xy\c \qvar)$;$\pqvar$,$\prvar$,($\pbarp ab$ U)
\lineb

Mixed Compound Premises
\lineb

$\rvar$<=$(\pvar \And \qvar \And \Each x \pbar x \c \rvar)$;($\pbar a$ U),($(\pqvar \c \qvar)$;$\pqvar$),$\pvar$

$\rvar$<=$(\pvar \And \qvar \And \Each x \pbar x \c \rvar)$;($\pbar a$ U),$\pvar$,($(\pqvar \c \qvar)$;$\pqvar$)

$\rvar$<=$(\pvar \And \qvar \And \Each x \pbar x \c \rvar)$;$\pvar$,($\pbar a$ U),($(\pqvar \c \qvar)$;$\pqvar$)

$\rvar$<=$(\pvar \And \qvar \And \Each x \pbar x \c \rvar)$;($(\pqvar \c \qvar)$;$\pqvar$),($\pbar a$ U),$\pvar$

$\rvar$<=$(\pvar \And \qvar \And \Each x \pbar x \c \rvar)$;($(\pqvar \c \qvar)$;$\pqvar$),$\pvar$,($\pbar a$ U)

$\rvar$<=$(\pvar \And \qvar \And \Each x \pbar x \c \rvar)$;$\pvar$,($(\pqvar \c \qvar)$;$\pqvar$),($\pbar a$ U)

$\rvar$<=$(\pvar \And \qvar \And \Each x \pbar x \c \rvar)$;($(\pqvar \c \qvar)$;$\pqvar$),($(\prvar \c \pvar)$; $\prvar)$,($\pbar a$ U)

$\rvar$<=$(\pvar \And \qvar \And \Each x \pbar x \c \rvar)$;($\pbar a$ U),($(\pqvar \c \qvar)$;$\pqvar$),($(\prvar \c \pvar)$; $\prvar)$

$\rvar$<=$(\pvar \And \qvar \And \Each x \pbar x \c \rvar)$;($(\pqvar \c \qvar)$;$\pqvar$),($\pbar a$ U),($(\prvar \c \pvar)$; $\prvar)$

$\qvar$<=$(\qvar \Iff \pvar \And \Each x \pbar x)$;($(\pvar \Iff \rvar)$;$\rvar$),($\pbar a$ U)

$\qvar$<=$(\qvar \Iff \pvar \And \Each x \pbar x)$;($(\rvar \Iff \pvar)$;$\rvar$),($\pbar a$ U)

$\qvar$<=$(\qvar \Iff \pvar \And \Each x \pbar x)$;($(\rvar \c \pvar)$;$\rvar$),($\pbar a$ U)

$\qvar$<=$(\qvar \Iff \pvar \And \Each x \pbar x)$;($\pbar a$ U),($(\rvar \c \pvar)$;$\rvar$)

$\qvar$<=$(\qvar \Iff \pvar \And \Each x \pbar x)$;($\pbar a$ U),($(\rvar \Iff \pvar)$;$\rvar$)

$\qvar$<=$(\qvar \Iff \pvar \And \Each x \pbar x)$;($\pbar a$ U),($(\pvar \Iff \rvar)$;$\rvar$)

$\qvar$<=$(\pvar \And \Each x \pbar x\Iff \qvar)$;($(\pvar \Iff \rvar)$;$\rvar$),($\pbar a$ U)

$\qvar$<=$(\pvar \And \Each x \pbar x\Iff \qvar)$;($(\rvar \Iff \pvar)$;$\rvar$),($\pbar a$ U)

$\qvar$<=$(\pvar \And \Each x \pbar x\Iff \qvar)$;($(\rvar \c \pvar)$;$\rvar$),($\pbar a$ U)

$\qvar$<=$(\pvar \And \Each x \pbar x\Iff \qvar)$;($\pbar a$ U),($(\rvar \c \pvar)$;$\rvar$)

$\qvar$<=$(\pvar \And \Each x \pbar x\Iff \qvar)$;($\pbar a$ U),($(\rvar \Iff \pvar)$;$\rvar$)

$\qvar$<=$(\pvar \And \Each x \pbar x\Iff \qvar)$;($\pbar a$ U),($(\pvar \Iff \rvar)$;$\rvar$)

$\rvar$<=$(\pvar \And \qvar \And \Each x \pbar x \c \rvar)$;$\pvar$,($(\pqvar \Iff \qvar)$;$\pqvar$),($\pbar a$ U)

$\rvar$<=$(\pvar \And \qvar \And \Each x \pbar x \c \rvar)$;($(\pqvar \Iff \qvar)$;$\pqvar$),$\pvar$,($\pbar a$ U)

$\rvar$<=$(\pvar \And \qvar \And \Each x \pbar x \c \rvar)$;($(\pqvar \Iff \qvar)$;$\pqvar$),($\pbar a$ U),$\pvar$

$\rvar$<=$(\pvar \And \qvar \And \Each x \pbar x \c \rvar)$;($\pbar a$ U),$\pvar$,($(\pqvar \Iff \qvar)$;$\pqvar$)

$\rvar$<=$(\pvar \And \qvar \And \Each x \pbar x \c \rvar)$;($\pbar a$ U),($(\pqvar \Iff \qvar)$;$\pqvar$),$\pvar$

$\rvar$<=$(\pvar \And \qvar \And \Each x \pbar x \c \rvar)$;$\pvar$,($\pbar a$ U),($(\pqvar \Iff \qvar)$;$\pqvar$)

\lineb
Complex Transitive Rules

$(\pvar \Iff \Some x \Some y ;\pbarp xy \rbarp xy)$ <= ($(\pqvar \And \Each x,y ;\pbarp xy \q^{2}_{01}xy \c \pvar \Iff \Some x \Some y ; \pbarp xy \qbarp xy)$;($(\pbarp cd \c \q^{2}_{01}cd)$ U),$\pqvar$)-($(\q^{2}_{01}ab \c \qbarp ab \Iff \rbarp ab)$ U)

$(\pvar \Iff \Some x \Some y ;\pbarp xy \rbarp xy)$ <= ($(\pqvar \And \Each x,y ;\pbarp xy \q^{2}_{01}xy \c \pvar \Iff \Some x \Some y ; \pbarp xy \qbarp xy)$;$\pqvar$,($(\pbarp cd \c \q^{2}_{01}cd)$ U))-($(\q^{2}_{01}ab \c \qbarp ab \Iff \rbarp ab)$ U)


\lineb
Ordered Pair Rules (These are Implied Existence Rules ONLY)

$((u,v)\in A \c (u,v) \in A \And \pbarp uv)$<=$\Each x,y \in A\pbarp xy$

$((u,v)\in A \c \pbarp uv)$<=$\Each x,y \in A\pbarp xy$

$((u,v) \in A \And \pbarp uv)$<=$\Each x,y \in A\pbarp xy$,$((u,v) \in A)$

$((u,v) \in A \And \pbarp uv)$<=$((u,v) \in A)$,$\Each x,y \in A\pbarp xy$

$((u,v) \in A \And \pbarp uv \c \pvar)$<=$(\pvar \Iff \Some x,y \in A \pbarp xy)$

$((u,v) \in A \And \pbarp uv \c \pvar)$<=$(\Some x,y \in A \pbarp xy\Iff \pvar)$

$((u,v) \in A \And \pbarp uv \c \pvar)$<=$(\pqvar \And\prvar \c \pvar \Iff \Some x,y \in A \pbarp xy)$;$\pqvar$,$\prvar$
\end
