%	proofeg.tex	(Examples for proof.sty)
%
%		on Oct 13, 1990
%		by Makoto Tatsuta
%
%	I hope you can learn how to use proof figure macros easily
%	by these examples.

\def\imp{\to}
\def\land{\mathbin\&}

\documentstyle[proof]{article}

\begin{document}
\section*{Examples of proof.sty}

\verb|\infer| draws beautiful proof figures easily:

\noindent (1)
$$
\infer{A}{
	\infer{B}{
		B11\land B12\land B13
		&
		B21\land B22\land B23
	}
	&
	C
}
$$

\noindent (2)
$$
\infer{A1\land A2\land A3\land A4\land A5\land A6}{
	\infer{B}{
		B11\land B12\land B13
		&
		B21\land B22\land B23
	}
	&
	C
}
$$

\noindent (3)
$$
\infer{A1\land A2\land A3\land A4\land A5\land A6}{
	C
	&
	\infer{B}{
		B11\land B12\land B13
		&
		B21\land B22\land B23
	}
}
$$

You can use also some variations:

\noindent (4)
$$
\infer[(1)]{A}{
	\infer*{B}{
		B11\land B12\land B13
		&
		B21\land B22\land B23
	}
	&
	C
}
$$

\noindent (5)
$$
\infer*[(1)]{A1\land A2\land A3\land A4\land A5\land A6}{
	\deduce[{\displaystyle \sum}]{B}{
		B11\land B12\land B13
		&
		B21\land B22\land B23
	}
	&
	\deduce{C}{(2)}
}
$$

Here are more practical examples:

\noindent (6)
$$
\infer[(\land I)]{A \land B}{A & B}
\qquad
\infer[(\land E_l)]A{A\land B}
\qquad
\infer[(\land E_r)]B{A\land B}
$$

$$
\infer[(\imp I)]{A \imp B}{
	\infer*{B}{[A]}
}
\qquad
\infer[(\imp E)]{B}{
	A \imp B
	&
	A
}
$$

Some techniques:
Use \verb|\vcenter| for an equation of proofs.

\noindent (7)
$$
\pi = \vcenter{
\infer{E}{
	A
	&
	\infer{D}{B & C}
}
}
$$

Use \verb|\kern| to adjust the form of a proof.

\noindent (8)
$$
\infer{E}{
	A
	&
	\infer{D}{B & C} \kern 0.5cm
}
$$

\end{document}
