% \iffalse meta-comment
%
% Copyright (C) 2005 by Paul van Tilburg <paul@luon.net>
% ------------------------------------------------------
%
% This package is free software; you can redistribute it and/or modify
% it under the terms of the GNU General Public License as published by
% the Free Software Foundation; either version 2 of the License, or
% (at your option) any later version.
%
% This package is distributed in the hope that it will be useful,
% but WITHOUT ANY WARRANTY; without even the implied warranty of
% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
% GNU General Public License for more details.
%
% You should have received a copy of the GNU General Public License
% along with this package; if not, write to the Free Software
% Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.%
%
% \fi
%
% \iffalse
%<*driver>
\ProvidesFile{flagderiv.dtx}
%</driver>
%<flagderiv>\NeedsTeXFormat{LaTeX2e}[1999/12/01]
%<flagderiv>\ProvidesPackage{flagderiv}
%<*flagderiv>
[2005/08/26 v0.10 Flag style derivation package]
%</flagderiv>
%
%<*driver>
\documentclass{ltxdoc}
\usepackage{amsmath, amssymb}
\usepackage{calc}
\usepackage{flagderiv}
\usepackage{fvrb-ex}
\usepackage{theorem}
\usepackage{url}
\setlength{\parindent}{0pt}
\setlength{\parskip}{\medskipamount}
\setcounter{tocdepth}{2}
\theoremstyle{plain}
\newtheorem{lemma}{Lemma}
\newcommand{\false}{\textit{False}}
\newcommand{\flags}{\texttt{flagderiv}}
\newcommand{\IHbase}{\underline{\textit{Base}}:~}
\newcommand{\IHhyp}{\underline{\textit{Induction-hypothesis}}:~}
\newcommand{\IHstep}{\underline{\textit{Step}}:~}
\newcommand{\Nat}{\ensuremath{\mathbb{N}}}
\newcommand{\All}{\ensuremath{\mathbb{Z}}}
\newcommand{\Powerset}{\ensuremath{\mathcal{P}}}
\renewcommand{\implies}{\Rightarrow}
\newcommand{\biimplies}{\Leftrightarrow}
\newcommand{\OHA}{\rightarrow}
\newcommand{\THA}{\twoheadrightarrow}
\newcommand{\NHA}[1]{\stackrel{#1}{\rightarrow}}
\newcommand{\CRtext}{\ensuremath{\mathit{CR}}}
\newcommand{\CR}{\ensuremath{(\forall a, b, c\in A: a\THA b\land a\THA c:%
(\exists d\in A:: b\THA d\land c\THA d))}}
\newcommand{\MCtext}{\ensuremath{\mathit{mixed~confluent}}}
\newcommand{\MC}{\ensuremath{(\forall a, b, c\in A: a\OHA b\land a\THA c:%
(\exists d\in A:: b\THA d\land c\THA d))}}
\EnableCrossrefs
\CodelineIndex
\RecordChanges
\begin{document}
\DocInput{flagderiv.dtx}
\end{document}
%</driver>
% \fi
%
% \CheckSum{0}
%
% \CharacterTable
% {Upper-case \A\B\C\D\E\F\G\H\I\J\K\L\M\N\O\P\Q\R\S\T\U\V\W\X\Y\Z
% Lower-case \a\b\c\d\e\f\g\h\i\j\k\l\m\n\o\p\q\r\s\t\u\v\w\x\y\z
% Digits \0\1\2\3\4\5\6\7\8\9
% Exclamation \! Double quote \" Hash (number) \#
% Dollar \$ Percent \% Ampersand \&
% Acute accent \' Left paren \( Right paren \)
% Asterisk \* Plus \+ Comma \,
% Minus \- Point \. Solidus \/
% Colon \: Semicolon \; Less than \<
% Equals \= Greater than \> Question mark \?
% Commercial at \@ Left bracket \[ Backslash \\
% Right bracket \] Circumflex \^ Underscore \_
% Grave accent \` Left brace \{ Vertical bar \|
% Right brace \} Tilde \~}
%
%
% \changes{v0.9f}{2005/02/04}{Initial version.}
% \changes{v0.9g}{2005/05/16}{Added example and usage documentation.}
% \changes{v0.9h}{2005/06/06}{Added the flagderiv* environment.}
% \changes{v0.9i}{2005/06/10}{Fixed minor issues in the documentation
% and resolved a ref-format bug.}
% \changes{v0.10}{2005/08/26}{Drop dependancy on farray, include fix.}
%
% \GetFileInfo{flagderiv.dtx}
%
% \DoNotIndex{\newcommand,\newenvironment}
%
% \title{The \textsf{flagderiv} package\thanks{This document
% corresponds to \textsf{flagderiv}~\fileversion, dated \filedate.}}
% \author{Paul van Tilburg \\ \url{paul@luon.net}}
%
% \maketitle
%
% \tableofcontents
%
% \section{Introduction}
%
% This document describes how to use \flags~to make flag-style proofs in
% \LaTeX.
%
% It can handle taking steps, making assumptions, introducing variables and
% conclusions. The package allows the style to be configured. For
% example, the variable introduction symbol can be redefined. Other
% features include multiple page flag-style proofs.
%
% The documentation and all examples are based upon version \fileversion\
% of \flags.
%
% \begin{center}
% \scriptsize
% \renewcommand{\introsymb}{\text{Let}}
% \begin{flagderiv}
% \assume{i:assume:no-package}{\text{There is no nice package to do flag-style proofs}}{}
% \introduce{i:intro:feature}{x\text{, such that } x\text{ is a flag-style feature}}{}
% \skipsteps{5}{\vdots}{}
% \step{i:feature-met}{\flags~\text{can do it}}{}
% \conclude{i:conclusion}{\flags~\text{fulfils my every flag-style proof need}}
% {$\forall$-introduction on \ref{i:intro:feature} and \ref{i:feature-met}}
% \step{i:false}{\false}{\false-introduction on \ref{i:assume:no-package} and \ref{i:conclusion}}
% \conclude{i:conclude:not-no-package}{\lnot (\text{There is no nice package to do flag-style proofs})}
% {$\lnot$-introduction on \ref{i:assume:no-package} and \ref{i:false}}
% \step{i:step:nice-package}{\text{So, there exists a nice package to do flag-style proofs}}
% {$\lnot\lnot$-elimination on \ref{i:conclude:not-no-package}}
% \end{flagderiv}
% \end{center}
%
% \section{Acknowledgements}
%
% I want to thank Jan Zwanenburg and Erik Poll for the first versions of
% this package, professor R.P.\ Nederpelt for his ever-persisting package
% reviews, feedback and suggestions and last but not least Mark van Eijk,
% who has written parts of section~\ref{sec:usage} and all examples in
% section~\ref{sec:ex}.
%
% \section{Usage\label{sec:usage}}
%
% This section explains how the \flags\ package works by means of examples
% and how the commands should be used. I try to cover all possibilities and
% features of this package. For bigger examples, please refer to
% section~\ref{sec:ex}; for more detailed documentation on the commands
% and inner workings, refer to the \flags\ package itself.
%
% \subsection{Basic derivations}
% \DescribeEnv{flagderiv}
% Basic derivations are written using an intuitive command sequence
% placed in the |flagderiv| environment\index{usage}. The example below
% uses auto-numbering of the lines. Variable introductions, assumptions,
% steps and conclusions can be done using the following commands
% respectively:
%
% \begin{itemize}
% \item \DescribeMacro{\introduce}\index{usage}
% |\introduce|\marg{label}\marg{formula}\marg{comment},
% \item \DescribeMacro{\assume}\index{usage}
% |\assume|\marg{label}\marg{formula}\marg{comment},
% \item \DescribeMacro{\step}\index{usage}
% |\step|\marg{label}\marg{formula}\marg{comment}, and
% \item \DescribeMacro{\conclude}\index{usage}
% |\conclude|\oarg{number}\marg{label}\marg{formula}\marg{comment}.
% \end{itemize}
%
% Lines can be referred to using the {\em label} that is provided as the
% first argument to each of the commands. {\em Formulas} are placed in
% the second argument and a {\em comment} in the third.
% See subsection~\ref{sec:usage:multi} for the explanation of the optional
% argument {\em number} of |\conclude|.
%
% \begin{Example}[gobble=7,frame=single,label=Auto-numbering]
% \begin{flagderiv}
% \introduce{in-x}{x: \Nat}{Introduction of $x$}
% \assume{as-x}{x > 5}{Assumption}
% \step{big-x}{x > 1}{Arithmetic on \ref{in-x} and \ref{as-x}}
% \conclude{conc}{x > 5 \implies x > 1}
% {$\implies$-intro on \ref{as-x} and \ref{big-x}}
% \conclude{}{\forall x \in \Nat: x > 5 \implies x > 1}
% {$\forall$-intro on \ref{in-x} and \ref{conc}}
% \end{flagderiv}
% \end{Example}
%
% The following example uses manual numbering. This is done by using the
% \DescribeMacro{\introduce*}
% starred versions of the previous given commands (|\introduce*|,
% \DescribeMacro{\assume*}
% \DescribeMacro{\step*}
% \DescribeMacro{\conclude*}
% |\assume*|, |\step*| and |\conclude*|) and using a
% {\em custom number} instead of a {\ em label} as the first argument.
% Note that because of this, derivation line references are not possible
% and should be done manually as well.
%
% \begin{Example}[gobble=7,frame=single,label=Manual numbering]
% \begin{flagderiv}
% \introduce*{$(1)$}{x: \Nat}{Introduction of $x$}
% \assume*{$(2)$}{P(x)}{Assumption}
% \skipsteps*{\dots}{}
% \step*{$(n - 2)$}{Q(x)}{}
% \conclude*{$(n - 1)$}{P(x) \implies Q(x)}
% {$\implies$-intro on $(2)$ and $(n - 2)$}
% \conclude*{$(n)$}{\forall x \in \Nat: P(x) \implies Q(x)}
% {$\forall$-intro on $(1)$ and $(n - 1)$}
% \end{flagderiv}
% \end{Example}
%
% Note that the |\skipsteps*| used in the previous example is
% explained in section~\ref{sec:usage:skipsteps}.
%
% \subsection{Concluding multiple assumptions/introductions\label{sec:usage:multi}}
% Sometimes it is useful to make a conclusion from multiple open
% assumptions and/or introductions at once. This can be done by supplying
% an optional {\em number} to the |\conclude| command. Usage is
% illustrated in the example below.
%
% \begin{Example}[gobble=7,frame=single,label=Multiple conclusion]
% \begin{flagderiv}
% \introduce{}{x: \Nat}{}
% \assume{}{P(x)}{}
% \step{}{Q(x)}{}
% \conclude[2]{}{\forall x \in \Nat: (P(x) \implies Q(x))}{}
% \end{flagderiv}
% \end{Example}
%
% \subsection{Skipping steps\label{sec:usage:skipsteps}}
% When writing example derivations or abbreviating those where
% obvious/trivial steps may be skipped, one can use the
% \DescribeMacro{\skipsteps}
% |\skipsteps|\marg{number}\marg{formula}\marg{comment} command for
% auto-numbered derivations. This commands takes the {\em number} of
% steps to skip as the first argument, a {\em formula} as the second and
% a {\em comment} as the third, like a normal step.
% \vspace{3em}
%
% \begin{Example}[gobble=7,frame=single,label=Skipping 5 steps]
% \begin{flagderiv}
% \assume{as}{P \implies Q}{}
% \step{lem-p}{P \lor \neg P}{LEM}
% \skipsteps{5}{\dots}
% {Prove $\neg P \lor Q$ for $P$ and $\neg P$}
% \step{or-elm}{\neg P \lor Q}{$\lor$-elim on \ref{lem-p}}
% \end{flagderiv}
% \end{Example}
%
% For skipping an unknown number of steps in a manual numbered
% \DescribeMacro{\skipsteps*}
% derivation, the command |\skipsteps*|\marg{formula}\marg{comment} can
% be used. Here the number of steps to skip must be omitted, since there
% is no counting involved. See for example the $\implies$-intro rule:
%
% \begin{Example}[gobble=7,frame=single,label=Skipping steps]
% \begin{flagderiv}
% \assume*{$(1)$}{P}{Assumption}
% \skipsteps*{\dots}{Derive $Q$}
% \step*{$(n - 1)$}{Q}{}
% \conclude*{$(n)$}{P \implies Q}
% {$\implies$-intro on $(1)$ to $(n - 1)$}
% \end{flagderiv}
% \end{Example}
%
% \subsection{Closing assumptions/introductions}
% Assumptions and introductions (contexts) are not always closed by a
% conclusion, it is sometimes useful to keep proven propositions within
% \DescribeMacro{\done}
% its context. The |\done| command (|\done|\oarg{number}) can be used to
% close a assumption and/or introduction without mentioning why. It takes
% an optional argument {\em number} to close multiple open assumptions
% and/or introductions. An example from the WTT (Weak Type Theory):
%
% \begin{Example}[gobble=7,frame=single,label=Closing assumptions/introductions]
% \begin{flagderiv}
% \introduce{}{n: \Nat}{}
% \introduce{}{d: \Nat}{}
% \step{}{\text{$d$ is a divisor of $n$} :=
% \exists_{k: \Nat} (n = d \cdot k)}{}
% \done
% \introduce{}{m: \Nat}{}
% \step{}{\text{$m$ is a multiple of $n$} :=
% \exists_{k: \Nat} (m = k \cdot n)}{}
% \done[2]
% \end{flagderiv}
% \end{Example}
%
% \vspace{-1em}
% The last |\done[2]| can be omitted since closing the \flags\ environment
% implicitly closes all open introductions and assumptions.
%
%
% \subsection{Spacing between lines}
% The spacing between derivation lines defaults to {\tt 8pt} but can be
% changed
% \DescribeMacro{derivskip}\index{setting}
% by adjusting the length (using |\setlength| on {\tt derivskip})
% before starting or during a \flags\ environment. See for example the
% more condensed proof:
%
% \begin{Example}[gobble=7,frame=single,label=Condensing a derivation]
% \setlength{\derivskip}{4pt}
% \begin{flagderiv}
% \assume{}{P}{}
% \assume{}{Q}{}
% \step{}{P}{}
% \conclude{}{Q \implies P}{}
% \conclude{}{P \implies Q \implies P}{}
% \end{flagderiv}
% \end{Example}
%
% Note that flag derivations will automatically be split across pages if
% it is too long and the |flagderiv| environment is used. See also the
% {\tt longtable} package. This does not happen for |flagderiv*|, which
% is a normal |tabular|.
%
% \subsection{The introduction symbol}
% \DescribeMacro{\introsymb}\index{changing}
% The way an introduction flag differs from an assumption flag is that it
% is prefixed with an {\em introduction symbol}. This symbol is by
% default set to $\mathbf{var}$ (|\mathbf{var}|) but can be changed
% to a different symbol, for example to $\leadsto$ (|\leadsto|) or
% just `Let'. This can be changed by redefining the |\introsymb|
% command before opening the \flags\ environment.
%
% \begin{Example}[gobble=7,frame=single,label=Changing the introduction symbol]
% \renewcommand{\introsymb}{\textbf{Let}}
% \begin{flagderiv}
% \introduce{intro-x}{x: \Nat}{Introduction}
% \introduce{intro-y}{y: \Nat}{Introduction}
% \skipsteps*{\ddots}{}
% \end{flagderiv}
% \end{Example}
%
% \subsection{Numbering and format}
% When the derivation lines are automatically numbered the numbers are
% formatted as ``({\em number})'' and so are the references. This format
% \DescribeMacro{fd@stepcount}
% \DescribeMacro{\thestepcount}\index{changing}
% can be changed by overriding the |\thestepcount| command using the
% {\tt fd@stepcount} counter before opening the \flags\ environment.
%
% \begin{Example}[gobble=7,frame=single,label=Changing the numbering format]
% \renewcommand{\thestepcount}{[\Roman{fd@stepcount}]}
% \begin{flagderiv}
% \step{ass}{P \implies Q}{}
% \step{lem}{P \lor \neg P}{LEM}
% \assume{ass-nP}{\neg P}{Assumption}
% \step{s0}{\neg P \lor \neg Q}{$\lor$-intro on \ref{ass-nP}}
% \done
% \assume{ass-nnP}{P}{Assumption}
% \step{s1}{Q}{$\implies$-elim on \ref{ass-nnP} and \ref{ass}}
% \step{s2}{\neg P \lor \neg Q}{$\lor$-intro on \ref{s1}}
% \done
% \step{or-el}{\neg P \lor Q}
% {$\lor$-elim on \ref{lem}, \ref{s0} and \ref{s2}}
% \end{flagderiv}
% \end{Example}
%
% \DescribeMacro{\thesteplabel}\index{changing}
% Since the manual numbered derivations use no counter, the format can be
% changed by overriding the |\thesteplabel| command which will take
% one argument, the {\em custom number}.
%
% \begin{Example}[gobble=7,frame=single,label=Changing the numbering format]
% \renewcommand{\thesteplabel}[1]{#1.}
% \begin{flagderiv}
% \assume*{1}{P}{Assumption}
% \skipsteps*{\dots}{Derive $Q$}
% \step*{n - 1}{Q}{}
% \conclude*{n}{P \implies Q}{$\implies$-intro on 1 to n - 1}
% \end{flagderiv}
% \end{Example}
%
% Note that since references are also manually done, the same format
% should be used there by the writer him/herself.
%
% \subsection{Inline comments}
% In general there are two ways to place the comments with respect to
% the formulas in derivations. The first is behind the formula (the
% default). The second way is to place them inline, that is, on a separate
% line before the formula.
%
% All \flags\ environments can be set globally to display the comments
% inline by passing the global option {\tt inlcmnts} to the \flags\
% package (e.g.\\|\usepackage[inlcmnts]{flagsderiv}|).
%
% \DescribeMacro{\inlcmnts}\index{usage}
% Giving the |\inlcmnts| command makes the environments after this
% command explicitly switch into inline-comment-mode (the default or
% \DescribeMacro{\noinlcmnts}\index{usage}
% global option is forgotten) after which giving |\noinlcmnts| will set
% it back to normal mode.
%
% \begin{Example}[gobble=7,frame=single,label=Inline comments]
% \inlcmnts
% \begin{flagderiv}
% \assume{as-P}{P}{Assume:}
% \assume{as-Q}{Q}{Assume:}
% \step{re-P}{P}{Rei \ref{as-P}:}
% \conclude{imp1}{Q \implies P}
% {$\implies$-intro on \ref{as-Q} and \ref{re-P}:}
% \conclude{imp2}{P \implies Q \implies P}
% {$\implies$-intro on \ref{as-P} and \ref{imp1}:}
% \end{flagderiv}
% \end{Example}
%
% When the comments are inserted inline, a certain format is used, namely
% to enclose the comment with braces. This is the default, but can be
% \DescribeMacro{\theinlcmnt}
% overridden by redefining the |\theinlcmnt| command.\index{override}
% \vspace{1em}
%
% \begin{Example}[gobble=7,frame=single,label=Changing inline comments format]
% \inlcmnts
% \renewcommand{\theinlcmnt}[1]{--#1--}
% \begin{flagderiv}
% \assume{ass-P}{P}{Assumption}
% \assume{ass-Q}{Q}{Assumption}
% \step{rei-P}{P}{Rei \ref{ass-P}}
% \end{flagderiv}
% \end{Example}
%
% \subsection{Namespaces for labels}
% In a document with a lot of auto-numbered derivations it is easy to lose
% overview of labels already used or it may be hard to keep thinking of
% new ones. To solve this a \flags\ environment can take a {\em namespace}
% as optional argument\index{namespacing}. This makes the lines referable
% as normal within the same derivation but also globally when the namespace
% and a colon is added outside the derivation. For example a derivation for
% Modus Tollens (MT):
%
% \begin{Example}[gobble=7,frame=single,label=Derivation label namespace]
% \begin{flagderiv}[mt]
% \step{s0}{P \implies Q}{}
% \assume{as-nQ}{\neg Q}{Assumption}
% \assume{as-P}{P}{Assumption}
% \step{s1}{Q}{$\implies$-elim on \ref{s0} and \ref{as-P}}
% \step{s2}{\bot}{$\bot$-intro on \ref{as-nQ} and \ref{s1}}
% \conclude{nP}{\neg P}{$\neg$-intro on \ref{as-P} and \ref{s2}}
% \conclude{nQ-nP}{\neg Q \implies \neg P}
% {$\implies$-intro on \ref{as-nQ} and \ref{nP}}
% \end{flagderiv}
%
% Note that step~\ref{mt:as-P} is not an intuitive step but necessary
% to get $\neg P$ under the assumption $\neg Q$.
% \end{Example}
%
% \subsection{Other options}
% \DescribeMacro{\caption}\index{usage}
% \DescribeMacro{\tablehead}\DescribeMacro{\tablefirsthead}
% A \flags\ environment actually wraps a {\tt longtable}. This means
% that at the start of an environment all {\tt longtable} options are
% available. This means the use of |\caption|, and setting heads
% (|\tablehead| and |\tablefirsthead|) and feet (|\endfoot|
% \DescribeMacro{\endfoot}\DescribeMacro{\endlastfoot}
% and |\endlastfoot|) but also changing the lengths, etc.
%
% \DescribeEnv{flagderiv*}
% Note that this does not hold for the slightly different |flagderiv*|
% environment, which acts exactly the same but is wrapped in a normal
% {\tt tabular} and thus can not be split across pages.
%
% \begin{Example}[gobble=7,frame=single,label=Captioned]
% \inlcmnts
% \begin{flagderiv}[reflex]
% \caption{The reflexivity of $\equiv_n$} \\
% \introduce*{(1)}{x \in \All}{Assume:}
% \skipsteps*{\dots \\ \dots}{}
% \step*{(n - 1)}{x \equiv_n x}{}
% \conclude*{(n)}{\forall x \in \All: x \equiv_n x}
% {$\forall$-intro on (1) and (n - 1):}
% \end{flagderiv}
% \end{Example}
%
% \DescribeMacro{\\}
% Additional it is possible to add custom newlines (|\\|) in all
% step formulas\footnote{This is not possible in introductions or
% assumptions, but they can often be split into multiple introductions or
% assumptions.} when the formula gets too long as demonstrated in the
% above example.
%
%
% \section{Examples\label{sec:ex}}
% The following are just a few real-life examples of flag-style proofs,
% where \flags\ provides an elegant means to include these proofs in
% \LaTeX-documents.
%
% \subsection{Examples from \flags}
% \subsection*{A derivation with auto-numbering and labels/references}
% \begin{flagderiv}
% \introduce{intro-xy}{x,y \in \mathbb{N}}{Introduction}
% \assume{assum:1}{x > 0}{Assumption}
% \assume{assum:2}{x < y}{Assumption}
% \step{y-pos}{y > 0}{Transitivity on \ref{assum:1} and \ref{assum:2}}
% \step{y3-pos}{y^3 > 0}{Arithmetic on \ref{y-pos}}
% \conclude{imp:1}{x < y \implies y^3 > 0}
% {$\implies$-intro on \ref{assum:2} and \ref{y3-pos}}
% \conclude{imp:2}{x > 0 \implies x < y \implies y^3 > 0}
% {$\implies$-intro on \ref{assum:1} and \ref{imp:1}}
% \conclude{}{\forall x, y \in \Nat: x > 0 \land x < y \implies y^3 > 0}
% {$\forall$-intro on \ref{intro-xy} and \ref{imp:2}}
% \end{flagderiv}
%
% \subsection*{A derivation with manual numbering}
% \begin{flagderiv}
% \assume*{(m)}{\neg P}{}
% \skipsteps{1}{\dots}{}
% \step*{(n - 2)}{False}{}
% \conclude*{(n - 1)}{\neg\neg P}
% {$\implies$-intro on (m) and (n - 2), and Negation}
% \step*{(n)}{P}{Double negation on (n - 1)}
% \end{flagderiv}
%
%
% \subsection{Predicate Calculus}
% \subsubsection*{Idempotence}
% \begin{flagderiv}[pc-idempotence]
% \assume{intro:PP}{P \land P}{}
% \step{and-elim:P}{P}{$\land$-elim on \ref{intro:PP}}
% \conclude{impl-intro:PP-P}{P \land P \implies P}
% {$\implies$-intro on \ref{intro:PP}
% and \ref{and-elim:P}}
% \assume{intro:P}{P}{}
% \step{and-intro:P}{P \land P}{$\land$-intro on \ref{intro:P}
% and \ref{intro:P}}
% \conclude{impl-intro:P-PP}{P \implies P \land P}
% {$\implies$-intro on \ref{intro:P}
% and \ref{and-intro:P}}
% \step{and-intro:result}{(P \land P \implies P) \land
% (P \implies P \land P)}
% {$\land$-intro on \ref{impl-intro:PP-P}
% and \ref{impl-intro:P-PP}}
% \step{idempotence}{P \land P \equiv P}
% {$\equiv$-intro on \ref{and-intro:result}}
% \end{flagderiv}
%
% \subsubsection*{De Morgan}
% \begin{flagderiv}[pc-demorgan]
% \assume{intro:NPQ}{\lnot (P \land Q)}{}
% \assume{intro:NNP}{\lnot\lnot P}{}
% \assume{intro:Q}{Q}{}
% \step{notnot-elim:P}{P}{$\lnot\lnot$-elim on \ref{intro:NNP}}
% \step{and-intro:PQ}{P \land Q}{$\land$-intro on \ref{intro:Q}
% and \ref{notnot-elim:P}}
% \step{false-intro:2}{\false}
% {$\false$-intro on \ref{and-intro:PQ}
% and \ref{intro:NPQ}}
% \conclude{not-intro:Q}{\lnot Q}{$\lnot$-intro on \ref{intro:Q}
% and \ref{false-intro:2}}
% \conclude{impl-intro:NNP-NQ}{\lnot\lnot P \implies \lnot Q}
% {$\implies$-intro on \ref{intro:NNP}
% and \ref{not-intro:Q}}
% \step{or-intro:NP-NQ}{\lnot P \lor \lnot Q}
% {$\lor$-intro on \ref{impl-intro:NNP-NQ}}
% \conclude{impl-intro:NPQ-NPNQ}{\lnot (P \land Q) \implies
% \lnot P \lor \lnot Q}
% {$\implies$-intro on \ref{intro:NPQ}
% and \ref{or-intro:NP-NQ}}
% \assume{intro:NPNQ}{\lnot P \land \lnot Q}{}
% \assume{intro:PQ}{P \lor Q}{}
% \step{or-elim:NP-Q}{\lnot P \implies Q}
% {$\lor$-elim on \ref{intro:PQ}}
% \step{and-elim:NP}{\lnot P}{$\land$-elim on \ref{intro:NPNQ}}
% \step{impl-elim:Q}{Q}{$\implies$-elim on \ref{or-elim:NP-Q}
% and \ref{and-elim:NP}}
% \step{and-elim:NQ}{\lnot Q}{$\land$-elim on \ref{intro:NPNQ}}
% \step{false-intro:1}{\false}{$\false$-intro on \ref{impl-elim:Q}
% and \ref{and-elim:NQ}}
% \conclude{impl-intro:PQ}{P \lor Q \implies \false}
% {$\implies$-intro on \ref{intro:PQ}
% and \ref{false-intro:1}}
% \step{not-intro:PQ}{\lnot (P \lor Q)}
% {$\lnot$-intro on \ref{impl-intro:PQ}}
% \conclude{impl-intro:NPNQ-NPQ}{\lnot P \land \lnot Q \implies
% \lnot (P \lor Q)}
% {$\implies$-intro on \ref{intro:NPNQ}
% and \ref{not-intro:PQ}}
% \step{and-intro:result}{(\lnot (P \land Q) \implies
% \lnot P \lor \lnot Q)
% \land\\
% (\lnot P \land \lnot Q \implies
% \lnot (P \lor Q))}
% {$\land$-intro on \ref{impl-intro:NPQ-NPNQ}
% and \ref{impl-intro:NPNQ-NPQ}}
% \step{demorgan}{\lnot (P \land Q) \equiv \lnot P \lor \lnot Q}
% {$\equiv$-intro on \ref{and-intro:result}}
% \end{flagderiv}
%
% \subsubsection*{Transitivity}
% \begin{flagderiv}[pc-transitivity]
% \introduce{intro:PQR}{P, Q, R}{}
% \assume{intro:PQQR}{(P \implies Q) \land (Q \implies R)}{}
% \assume{intro:P}{P}{}
% \step{and-elim:PQ}{P \implies Q}
% {$\land$-elim on \ref{intro:PQQR}}
% \step{impl-elim:Q}{Q}{$\implies$-elim on \ref{and-elim:PQ}
% and \ref{intro:P}}
% \step{and-elim:QR}{Q \implies R}
% {$\land$-elim on \ref{intro:PQQR}}
% \step{impl-elim:R}{R}{$\implies$-elim on \ref{and-elim:QR}
% and \ref{impl-elim:Q}}
% \conclude{impl-intro:PR}{P \implies R}
% {$\implies$-intro on \ref{intro:P}
% and \ref{impl-elim:R}}
% \conclude{impl-intro:PQQR-PR}{(P \implies Q) \land (Q \implies R)
% \implies (P \implies R)}
% {$\implies$-intro on \ref{intro:PQQR}
% and \ref{impl-intro:PR}}
% \conclude{transitivity}{(\forall P, Q, R::
% (P \implies Q) \land (Q \implies R)
% \implies (P \implies R)
% )}
% {$\forall$-intro on \ref{intro:PQR}
% and \ref{impl-intro:PQQR-PR}}
% \end{flagderiv}
%
% \subsection{Rewrite Systems}
% \subsubsection*{Mixed confluent $\biimplies$ Church-Rosser}
% {
% \renewcommand{\introsymb}{\text{Let}}
% \begin{flagderiv}
% \assume*{1}{\CRtext}{hyp}
% \introduce*{2}{a, b, c\in A, \text{such that}~a\OHA b\land a\THA c}{}
% \step*{3}{a\OHA b\land a\THA c}{rei (2)}
% \step*{4}{a\THA b\land a\THA c}{$\forall$-elimination on lemma~\ref{transclosure} and (3)}
% \step*{5}{(\exists d\in A:: b\THA d\land c\THA d)}{$\forall$-elimination on (1) and (4)}
% \conclude*{6}{\MCtext}{$\forall$-introduction on (2) and (5)}
% \conclude*{7}{\CRtext\implies\MCtext}{$\implies$-introduction on (1) and (6)}
% \assume*{8}{\MCtext}{}
% \assume*{9}{\text{Induction on the length of}~a\THA b}{}
% \skipsteps*{\IHbase}{}
% \introduce*{11}{a, b, c\in A, \text{such that}~a\NHA{0} b\land a\THA c}{}
% \step*{12}{a=b}{def $\NHA{0}$, (11)}
% \step*{13}{a\THA c}{$\land$-elimination on (11)}
% \step*{14}{b\THA c}{(12) applied on (13)}
% \step*{15}{c\THA c \land b\THA c}{}
% \step*{16}{(\exists d\in A:: b\THA d\land c\THA d)}{}
% \renewcommand{\thesteplabel}[1]{#1}
% \conclude*{}{\IHhyp}{}
% \step*{18}{\ensuremath{(\forall a, b, c\in A: a\NHA{n} b\land a\THA c:\\ \quad
% (\exists d\in A:: b\THA d\land c\THA d))}}{}
% \skipsteps*{\IHstep}{}
% \introduce*{20}{a, b, c\in A, \text{such that}~a\NHA{n+1} b\land a\THA c}{}
% \step*{21}{a\NHA{n+1} b}{$\land$-elimination on (20)}
% \step*{22}{a\NHA{n} b'\OHA b}{}
% \step*{23}{a\THA c}{$\land$-elimination on (20)}
% \step*{24}{a\NHA{n} b' \land a\THA c}{$\land$-introduction on (22) and (23)}
% \step*{25}{(\exists d'\in A:: b'\THA d'\land c\THA d')}{$\forall$-elimination on (18) and (24)}
% \step*{26}{d', \text{such that}~b'\THA d'\land c\THA d'}{$\exists$-elimination on (25)}
% \step*{27}{b'\OHA b \land b'\THA d'}{}
% \step*{28}{(\exists d\in A:: b\THA d\land d'\THA d)}{$\forall$-elimination on (8) and (27)}
% \step*{29}{d, \text{such that}~b\THA d\land d'\THA d}{$\exists$-elimination on (28)}
% \step*{30}{a\NHA{n} b'\OHA b\THA d \land a\THA c\THA d'\THA d}{}
% \step*{31}{b\THA d \land c\THA d}{}
% \step*{32}{(\exists d\in A:: b\THA d\land c\THA d)}{}
% \conclude*[2]{33}{\CRtext}{}
% \conclude*{34}{\MCtext\implies\CRtext}{$\implies$-introduction on (8) and (33)}
% \step*{35}{\MCtext\biimplies\CRtext}{$\biimplies$-introduction on (7) and (34)}
% \end{flagderiv}
% }
%
% \begin{lemma}
% \label{transclosure}
% \mbox{\ensuremath{(\forall a, b\in A: a\OHA b: a\THA b)}}
% \end{lemma}
%
% \StopEventually{}
%
% \newpage
% \section{Implementation}
%
% First some initial code is needed for processing of the options.
% Note that {\tt ifthen} is used throughout the package.
% \begin{macrocode}
\RequirePackage{ifthen}
\newboolean{@inlcmnts}
% \end{macrocode}
%
% Processing of the option ({\tt inlcmnts}) for enabling inline comments.
% \begin{macrocode}
\DeclareOption{inlcmnts}{\setboolean{@inlcmnts}{true}}
\ProcessOptions
% \end{macrocode}
%
% Loading of the required packages.
% Note that \flags\ needs to require a fix/override for the array package,
% until the fixed version is available in most distributions.
% \begin{macrocode}
\RequirePackage{array}
\RequirePackage{longtable}
\long\@namedef{NC@rewrite@*}#1#2{%
\count@#1\relax
\loop
\ifnum\count@>\z@
\advance\count@\m@ne
\@temptokena\expandafter{\the\@temptokena#2}%
\repeat
\NC@find}
% \end{macrocode}
%
% \subsection{Generic settings, counters and commands}
%
% \begin{macro}{fd@flagcount}
% \begin{macro}{fd@stepcount}
% The counters keeping the number of opened/nested flags and the number of
% derivation steps.
% \begin{macrocode}
\newcounter{fd@flagcount}
\newcounter{fd@stepcount}
% \end{macrocode}
% \end{macro}
% \end{macro}
%
% \begin{macro}{\derivskip}
% The default space ({\tt 8pt}) between lines in a derivation. This is
% overridable to define a different default length.
% \begin{macrocode}
\newlength{\derivskip}
\setlength{\derivskip}{8pt}
% \end{macrocode}
% \end{macro}
%
% \begin{macro}{\introsymb}
% The symbol used as variable introduction prefix. Overridable with
% |\renewcommand| to insert a different symbol, defaults to:
% |\textbf{var}|.
%
% Ex. |\renewcommand{\introsymb}{\textbf{Let}}|
% \begin{macrocode}
\newcommand{\introsymb}{\textbf{var}}
% \end{macrocode}
% \end{macro}
%
% \begin{macro}{\thestepcount}
% This is the command used to generate a step number label (used by
% auto-numbering). |\thestepcount| can be overridden to display labels
% differently, defaults to: ({\it number}). This exposes the internal
% |\thefd@stepcount| command.
%
% Ex. |\renewcommand{\thestepcount}{[\arabic{stepcount}]}|
% \begin{macrocode}
\newcommand{\thestepcount}{(\arabic{fd@stepcount})}
\renewcommand{\thefd@stepcount}{\thestepcount}
% \end{macrocode}
% \end{macro}
%
% \begin{macro}{\thesteplabel}
% Command used to generate a customized step label (used by manual numbering).
% |\thesteplabel| can be overridden to display manual numbers differently,
% this command has one argument: \marg{label}.
% The command does nothing by default (i.e\@. just returns the argument).
%
% Ex. |\renewcommand{\thesteplabel}[1]{[##1]}|
% \begin{macrocode}
\newcommand{\thesteplabel}[1]{#1}
% \end{macrocode}
% \end{macro}
%
% \begin{macro}{\theinlcmnt}
% The command used to format inline comments (if enabled). |\theinlcmnt|
% can be overridden to display it differently and has one argument:
% \marg{comment}. Defaults to: \{ {\em comment text} \}.
%
% Ex. |\renewcommand{\theinlcmnt}[1]{--#1--}|
% \begin{macrocode}
\newcommand{\theinlcmnt}[1]{\{ #1 \}}
% \end{macrocode}
% \end{macro}
%
% \begin{macro}{\inlcmnts}
% Command to switch inline comments explicitly on (and by that, overriding
% and forgetting the default determined by the absence or presence of the
% {\tt inlcmnts} package option).
%
% \begin{macrocode}
\newcommand{\inlcmnts}{\setboolean{@inlcmnts}{true}}
% \end{macrocode}
% \end{macro}
%
% \begin{macro}{\noinlcmnts}
% Command to switch inline comments explicitly off (and by that, overriding
% and forgetting the default determined by the absence or presence of the
% {\tt inlcmnts} package option).
%
% \begin{macrocode}
\newcommand{\noinlcmnts}{\setboolean{@inlcmnts}{false}}
% \end{macrocode}
% \end{macro}
%
% \subsection{The derivation environment}
%
% The following three sections describe the internal commands and constructs
% of the {\tt flagderiv} environment, after which the last section will
% explain how the environment works and how it is put together using the
% internal constructs.
%
% Note that for almost all commands there exists two versions, one used
% for manual numbered derivations and one for automatic numbered/labelled
% derivations (both forms can be mixed within the environment).
%
% \subsubsection{Labels}
%
% Derivation lines are labelled and can be referred to. This can be done
% with automatically numbered lines where the first argument is a normal
% \LaTeX\ label. However, to avoid clashing, the labels can be automatically
% prefixed with a namespace. The following two commands handle this prefixing.
%
% \begin{macro}{\@labelprefix}
% Command that specifies the label namespace prefix.
%
% \begin{macrocode}
\newcommand{\@labelprefix}{\relax}
% \end{macrocode}
% \end{macro}
% \begin{macro}{\@derlabel}
% Internal command to define a label using the prefix (if a label
% is defined, otherwise do nothing).
%
% \begin{macrocode}
\newcommand{\@derlabel}[1]{%
\ifthenelse{\equal{#1}{}}{}{\label{\@labelprefix#1}}%
}
% \end{macrocode}
% \end{macro}
%
% \subsubsection{Steps}
%
% A line of a derivation can be one of five types:
% \begin{enumerate}
% \item A simple and bare line, only internally accessible,
% \item a comment line,
% \item a derivation step (both automatically and manual numbered),
% \item a line to indicate skipping of steps,
% \item a flag (handled in the next section).
% \end{enumerate}
%
% This section deals with the first four types.
%
% \begin{macro}{\@derline}
% A simple derivation line that uses {\tt fd@flagcount} to remember
% the number of open flags. This command is used as:
% |\@derline|\marg{label}\marg{formula}\marg{comment}, with:
% \begin{description}
% \item[\marg{label}] a label which can be left empty, to refer back to in
% comments of other derivation lines,
% \item[\marg{formula}] the formula, and
% \item[\marg{comment}] a comment.
% \end{description}
%
% \begin{macrocode}
\newcommand{\@derline}[3]{%
\mbox{#1} &
\setlength{\extrarowheight}{\derivskip}%
% \end{macrocode}
% If the flag counter is still zero\dots
% \begin{macrocode}
\ifthenelse{\value{fd@flagcount}=0}%
% \end{macrocode}
% then this line is outside any flag,
% \begin{macrocode}
{\begin{array}[t]{@{}l}}%
% \end{macrocode}
% otherwise this is inside one or more flag contexts and the amount of
% open flagpoles equal to the number of open contexts should be inserted.
%
% \begin{macrocode}
{\begin{array}[t]{*{\value{fd@flagcount}}{|@{\hspace{2\arraycolsep}}}l}}
\ensuremath{#2}
\end{array} &
\mbox{#3} \\
}
% \end{macrocode}
% \end{macro}
%
% \begin{macro}{\@CMNTderline}
% Command to fold the comment on a separate line before the
% actual derivation line if the {\tt inlcmnts} option is set for this
% package, see also |\@derline| for the argument handling.
%
% \begin{macrocode}
\newcommand{\@CMNTderline}[3]{%
\ifthenelse{\boolean{@inlcmnts}}{%
% \end{macrocode}
% If the inline comments option is enabled, fold the comment before the
% actual line.
% \begin{macrocode}
\ifthenelse{\equal{#3}{}}{}{%
% \end{macrocode}
% There is comment, insert it inline.
% \begin{macrocode}
\@derline{}{\mbox{\theinlcmnt{#3}}}{}%
}
\@derline{#1}{#2}{}%
}{%
% \end{macrocode}
% If inline comments are not enabled, pass everything to |\@derline| directly.
% \begin{macrocode}
\@derline{#1}{#2}{#3}%
}%
}
% \end{macrocode}
% \end{macro}
%
% \begin{macro}{\@MANstep}
% \begin{macro}{\@AUTOstep}
% Command for the manual ({\tt MAN}) and automatically ({\tt AUTO})
% numbered version of a derivation step. See also |\@derline|.
%
% \begin{macrocode}
\newcommand{\@MANstep}[3]{\@CMNTderline{\thesteplabel{#1}}{#2}{#3}}
% \end{macrocode}
%
% \begin{macrocode}
\newcommand{\@AUTOstep}[3]{%
\refstepcounter{fd@stepcount}%
\@derlabel{#1}\@CMNTderline{\thestepcount}{#2}{#3}%
}
% \end{macrocode}
% \end{macro}
% \end{macro}
%
% \begin{macro}{\@MANskipsteps}
% \begin{macro}{\@AUTOskipsteps}
% Command for the manual ({\tt MAN}) and automatically ({\tt AUTO})
% numbered version of skipping derivation steps. See also |\@derline|.
%
% \begin{macrocode}
\newcommand{\@MANskipsteps}[2]{\@CMNTderline{}{#1}{#2}}
% \end{macrocode}
%
% \begin{macrocode}
\newcommand{\@AUTOskipsteps}[3]{%
\addtocounter{fd@stepcount}{#1}%
\@CMNTderline{}{#2}{#3}%
}
% \end{macrocode}
% \end{macro}
% \end{macro}
%
% \subsubsection{Flags}
%
% Flags are actually simple derivation lines with two extras: the formula
% is put into a flag box and the flag counter {\tt fd@flagcount} is incremented
% when one is opened. Next to flag commands there are also commands to
% to close (and by that decrementing the counter) flags.
%
% There exist three types of flags:
% \begin{enumerate}
% \item the simple and bare flag,
% \item the assumption flag (both manual and automatically numbered),
% \item the variable introduction flag (also manual and automatically numbered).
% \end{enumerate}
%
% \begin{macro}{\@flagbox}
% Creates a flag for (a box around) the given text/formula, takes
% \marg{formula} as an argument.
% \begin{macrocode}
\newcommand{\@flagbox}[1]{%
\setlength{\fboxsep}{0.75ex}%
\fbox{#1}%
}
% \end{macrocode}
% \end{macro}
%
% \begin{macro}{\@startflag}
% Starts a flag context by opening a flag and incrementing the counter.
% The command is used as:
% |\@startflag|\marg{label}\marg{formula}\marg{comment},
% see also |\@derline| for the meaning of these arguments.
%
% \begin{macrocode}
\newcommand{\@startflag}[3]{%
\@CMNTderline{#1}{\@flagbox{\ensuremath{#2}}}{#3}%
\addtocounter{fd@flagcount}{1}%
}
% \end{macrocode}
% \end{macro}
%
% \begin{macro}{\@endflag}
% Ends a flag by closing it and decrementing the counter. Takes the
% number of flags to close \marg{number} as an argument.
%
% \begin{macrocode}
\newcommand{\@endflag}[1]{\addtocounter{fd@flagcount}{-#1}}
% \end{macrocode}
% \end{macro}
%
% \begin{macro}{\@flagclose}
% Wrapper command for closing a number of flags simultaneously taking \oarg{number}
% as an optional argument, defaulting to 1. See also |\@endflag|.
%
% \begin{macrocode}
\newcommand{\@flagclose}[1][1]{\@endflag{#1}}
% \end{macrocode}
% \end{macro}
%
% \begin{macro}{\@MANassume}
% \begin{macro}{\@AUTOassume}
% Command for the manual ({\tt MAN}) and automatic ({\tt AUTO})
% numbered version of an assumption flag, see also |\@startflag|.
%
% \begin{macrocode}
\newcommand{\@MANassume}[3]{\@startflag{\thesteplabel{#1}}{#2}{#3}}
% \end{macrocode}
%
% \begin{macrocode}
\newcommand{\@AUTOassume}[3]{
\refstepcounter{fd@stepcount}%
\@derlabel{#1}\@startflag{\thestepcount}{#2}{#3}%
}
% \end{macrocode}
% \end{macro}
% \end{macro}
%
% \begin{macro}{\@MANintroduction}
% \begin{macro}{\@AUTOintroduction}
% Command for the manual ({\tt MAN}) and automatically ({\tt AUTO})
% numbered version of an introduction flag, see also |\@startflag|.
%
% \begin{macrocode}
\newcommand{\@MANintroduction}[3]{%
\@startflag{\thesteplabel{#1}}{\introsymb~#2}{#3}%
}
% \end{macrocode}
%
% \begin{macrocode}
\newcommand{\@AUTOintroduction}[3]{
\refstepcounter{fd@stepcount}%
\@derlabel{#1}\@startflag{\thestepcount}{\introsymb~#2}{#3}%
}
% \end{macrocode}
% \end{macro}
% \end{macro}
%
% \begin{macro}{\@MANconclude}
% \begin{macro}{\@AUTOconclude}
% Command to conclude from one or more open flags in the manual ({\tt MAN})
% and automatically ({\tt AUTO}) numbered version, see also |\@endflag|.
% The command is used as:
% |\@MANconclude|\oarg{number}\marg{label}\marg{formula}\marg{comment},
% where the \oarg{number} indicates the number of flags to close,
% defaulting to 1.
%
% \begin{macrocode}
\newcommand{\@MANconclude}[4][1]{\@endflag{#1}\step*{#2}{#3}{#4}}
% \end{macrocode}
%
% \begin{macrocode}
\newcommand{\@AUTOconclude}[4][1]{\@endflag{#1}\step{#2}{#3}{#4}}
% \end{macrocode}
% \end{macro}
% \end{macro}
%
% \subsubsection{The environment itself}
%
% \begin{environment}{flagderiv}
% This section explains the main environment for flag style
% derivations/proofs: {\tt flagderiv}. The command has an optional
% argument \oarg{prefix}, used as label prefix so that labels can be
% ``scoped'' with a namespace local to the derivation but still
% accessible from the outside.
%
% Examples:\\
% |\begin{flagderiv} ... \end{flagderiv}|\\
% |\begin{flagderiv}[abs] ... \end{flagderiv}|
%
% \begin{macrocode}
\newenvironment{flagderiv}[1][]{%
% \end{macrocode}
%
% First, set the optional label prefix (if given) and reset the counters.
%
% \begin{macrocode}
\ifthenelse{\equal{#1}{}}{%
\renewcommand{\@labelprefix}{}%
}{%
\renewcommand{\@labelprefix}{#1:}%
}%
\setcounter{fd@flagcount}{0}%
\setcounter{fd@stepcount}{0}%
% \end{macrocode}
%
% Note: {\em All} of the following five commands have a star version which
% allows manual numbering, instead of having auto-numbering, \LaTeX\ labels
% and references.
%
% \begin{macro}{\assume}
% \begin{macro}{\assume*}
% Opens an assumption flag; command usage:\\[1em]
% |\assume|\marg{label}\marg{formula}\marg{comment}\\
% |\assume*|\marg{custom-number}\marg{formula}\marg{comment}
%
% Examples: \\
% |\assume{assum:1}{x > 0}{Assumption}|\\
% |\assume*{l}{\neg P}{}|
%
% \begin{macrocode}
\newcommand{\assume}{\@ifstar{\@MANassume}{\@AUTOassume}}
% \end{macrocode}
% \end{macro}
% \end{macro}
%
% \begin{macro}{\introduce}
% \begin{macro}{\introduce*}
% Opens an introduction flag. Command usage: \\[1em]
% |\introduce|\marg{label}\marg{formula}\marg{comment} \\
% |\introduce*|\marg{custom-number}\marg{formula}\marg{comment}
%
% Examples:\\
% |\introduce{intro-x}{x \in \mathbb{N}}{Introduction}| \\
% |\introduce*{l - 1}{P \in s_P}{}|
%
% \begin{macrocode}
\newcommand{\introduce}{\@ifstar{\@MANintroduction}{\@AUTOintroduction}}
% \end{macrocode}
% \end{macro}
% \end{macro}
%
% \begin{macro}{\conclude}
% \begin{macro}{\conclude*}
% Performs a conclusion/multiple conclusion from one or more
% introductions and/or assumptions. The command usage:\\[1em]
% |\conclude|\oarg{number}\marg{label}\marg{formula}\marg{comment}\\
% |\conclude*|\oarg{number}\marg{custon-number}\marg{formula}\marg{comment}
%
% The optional argument \oarg{number} indicates how much flags should be
% closed with this conclusion, this defaults to 1.
%
% Examples;\\
% |\conclude[2]{concl:2}{x > 0 \implies ...}{$\implies$-intro on ...}|\\
% |\conclude*{n - 1}{\neg\neg P}{$\implies$-intro on (l) ...}|
%
% \begin{macrocode}
\newcommand{\conclude}{\@ifstar{\@MANconclude}{\@AUTOconclude}}
% \end{macrocode}
% \end{macro}
% \end{macro}
%
% \begin{macro}{\step}
% \begin{macro}{\step*}
% Performs a derivation step, command usage:\\[1em]
% |\step|\marg{label}\marg{formula}\marg{comment}\\
% |\step*|\marg{custom-number}\marg{formula}\marg{comment}
%
% Examples:\\
% |\step{x-elim}{x > 0}{$\forall$-elem on \ref{assum:1}}|\\
% |\step*{n - 1}{x > 0}{$\forall$-elem on (n - 3)}|
%
% Note: |\\| (line breaks) may be inserted for splitting
% large formulas.
%
% \begin{macrocode}
\newcommand{\step}{\@ifstar{\@MANstep}{\@AUTOstep}}
% \end{macrocode}
% \end{macro}
% \end{macro}
%
% \begin{macro}{\skipsteps}
% \begin{macro}{\skipsteps*}
% Skips a number of steps (for usage in examples), usage:\\[1em]
% |\skipsteps|\marg{number}\marg{formula}\marg{comments}\\
% |\skipsteps*|\marg{formula}\marg{comments}.
%
% Examples:\\
% |\skipsteps{3}{\vdots}{Etcetera, etcetera}|\\
% |\skipsteps*{\vdots}{Etcetera, etcetera}|
%
% \begin{macrocode}
\newcommand{\skipsteps}{\@ifstar{\@MANskipsteps}{\@AUTOskipsteps}}
% \end{macrocode}
% \end{macro}
% \end{macro}
%
% \begin{macro}{\done}
% Closes a number of flags because contexts have been opened and
% should be closed without conclusions. Command usage: \\[1em]
% |\done|\oarg{number}
%
% This command takes a number of introductions/assumptions, \oarg{number},
% to close as an optional argument, which defaults to 1.
%
% Examples:\\
% |\done|\\
% |\done[3]|
%
% \begin{macrocode}
\newcommand{\done}{\@flagclose}
% \end{macrocode}
% \end{macro}
%
% Silently override |\ref| to work with the defined namespace.
% \begin{macrocode}
\let\origref\ref%
\renewcommand{\ref}[1]{\origref{\@labelprefix##1}}%
% \end{macrocode}
%
% The actual flagderiv environment is just a longtable (called
% ``derivation'').
%
% \begin{macrocode}
\renewcommand{\tablename}{Derivation}%
\begin{longtable}[l]{rll}
}{%
\end{longtable}
}
% \end{macrocode}
% \end{environment}
%
% \begin{environment}{flagderiv*}
% The |flagderiv*| environment is almost the same as |flagderiv|
% with the only difference that the resulting derivation will and
% can not be split across pages.
%
% Example:\\
% |\begin{flagderiv*} ... \end{flagderiv*}|\\
%
% \begin{macrocode}
\newenvironment{flagderiv*}[1][]{%
\ifthenelse{\equal{#1}{}}{%
\renewcommand{\@labelprefix}{}%
}{%
\renewcommand{\@labelprefix}{#1:}%
}%
\setcounter{fd@flagcount}{0}%
\setcounter{fd@stepcount}{0}%
\newcommand{\assume}{\@ifstar{\@MANassume}{\@AUTOassume}}
\newcommand{\introduce}{\@ifstar{\@MANintroduction}{\@AUTOintroduction}}
\newcommand{\conclude}{\@ifstar{\@MANconclude}{\@AUTOconclude}}
\newcommand{\step}{\@ifstar{\@MANstep}{\@AUTOstep}}
\newcommand{\skipsteps}{\@ifstar{\@MANskipsteps}{\@AUTOskipsteps}}
\newcommand{\done}{\@flagclose}
\let\origref\ref%
\renewcommand{\ref}[1]{\origref{\@labelprefix##1}}%
\renewcommand{\tablename}{Derivation}
\begin{tabular}{rll}
}{%
\end{tabular}
}
% \end{macrocode}
% \end{environment}
%
% \PrintIndex
% \PrintChanges
%
% \Finale
\endinput