summaryrefslogtreecommitdiff
path: root/macros/latex/contrib/flagderiv
diff options
context:
space:
mode:
authorNorbert Preining <norbert@preining.info>2019-09-02 13:46:59 +0900
committerNorbert Preining <norbert@preining.info>2019-09-02 13:46:59 +0900
commite0c6872cf40896c7be36b11dcc744620f10adf1d (patch)
tree60335e10d2f4354b0674ec22d7b53f0f8abee672 /macros/latex/contrib/flagderiv
Initial commit
Diffstat (limited to 'macros/latex/contrib/flagderiv')
-rw-r--r--macros/latex/contrib/flagderiv/README2
-rw-r--r--macros/latex/contrib/flagderiv/flagderiv.dtx1261
-rw-r--r--macros/latex/contrib/flagderiv/flagderiv.ins63
-rw-r--r--macros/latex/contrib/flagderiv/flagderiv.pdfbin0 -> 211314 bytes
4 files changed, 1326 insertions, 0 deletions
diff --git a/macros/latex/contrib/flagderiv/README b/macros/latex/contrib/flagderiv/README
new file mode 100644
index 0000000000..1f676cdb40
--- /dev/null
+++ b/macros/latex/contrib/flagderiv/README
@@ -0,0 +1,2 @@
+The flagderiv package used to create mathematical derivations using
+the flag/flagpole notation.
diff --git a/macros/latex/contrib/flagderiv/flagderiv.dtx b/macros/latex/contrib/flagderiv/flagderiv.dtx
new file mode 100644
index 0000000000..c9025c73e2
--- /dev/null
+++ b/macros/latex/contrib/flagderiv/flagderiv.dtx
@@ -0,0 +1,1261 @@
+% \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
diff --git a/macros/latex/contrib/flagderiv/flagderiv.ins b/macros/latex/contrib/flagderiv/flagderiv.ins
new file mode 100644
index 0000000000..2dfc581c97
--- /dev/null
+++ b/macros/latex/contrib/flagderiv/flagderiv.ins
@@ -0,0 +1,63 @@
+%%
+%% 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.
+
+\input docstrip.tex
+\keepsilent
+
+\usedir{tex/latex/flagderiv}
+
+\preamble
+
+This is a generated file.
+
+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.
+
+\endpreamble
+
+\generate{\file{flagderiv.sty}{\from{flagderiv.dtx}{flagderiv}}}
+%\generate{\file{farray.sty}{\from{farray.dtx}{farry}}}
+
+\obeyspaces
+\Msg{*************************************************************}
+\Msg{* *}
+\Msg{* To finish the installation you have to move the following *}
+\Msg{* file into a directory searched by TeX: *}
+\Msg{* *}
+\Msg{* flagderiv.sty *}
+\Msg{* *}
+\Msg{* To produce the documentation run the file flagderiv.dtx *}
+\Msg{* through LaTeX. *}
+\Msg{* *}
+\Msg{* Happy TeXing! *}
+\Msg{* *}
+\Msg{*************************************************************}
+
+\endbatchfile
diff --git a/macros/latex/contrib/flagderiv/flagderiv.pdf b/macros/latex/contrib/flagderiv/flagderiv.pdf
new file mode 100644
index 0000000000..b3a4f91291
--- /dev/null
+++ b/macros/latex/contrib/flagderiv/flagderiv.pdf
Binary files differ