apxproof.dtx

% \iffalse meta-comment
%
% Copyright (C) 2016-2022 by Pierre Senellart
%
% This work may be distributed and/or modified under the
% conditions of the LaTeX Project Public License, either version 1.3
% of this license or (at your option) any later version.
% The latest version of this license is in
%   http://www.latex-project.org/lppl.txt
% and version 1.3 or later is part of all distributions of LaTeX
% version 2005/12/01 or later.
%
% This work has the LPPL maintenance status `maintained'.
%
% The Current Maintainer of this work is Pierre Senellart
% <pierre@senellart.com> and a version control system for this work
% is available at http://github.com/PierreSenellart/apxproof
%
% This work consists of the files apxproof.dtx and apxproof.ins
% and the derived file apxproof.sty.
%
% \fi
%
% \iffalse
%<package>\NeedsTeXFormat{LaTeX2e}[2005/12/01]
%<package>\ProvidesPackage{apxproof}
%<package>  [2022/10/14 v1.2.4 Automatic proofs in appendix]
%
%<*driver>
\documentclass{ltxdoc}
\usepackage{apxproof}
\usepackage{hypdoc}
\usepackage{textcomp}
\usepackage[TS1,T1]{fontenc}
\usepackage{lmodern}
\usepackage{microtype}
\newtheorem{example}{Example}
\newtheoremrep{foobar}{Foobar}
\EnableCrossrefs
\CodelineIndex
\RecordChanges
\begin{document}
  \DocInput{apxproof.dtx}
\end{document}
%</driver>
% \fi
%
% \CheckSum{974}
%
% \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{v1.0.4}{2017/03/02}{Show options commented on in margin and index}
%\iffalse
% Taken from xkeyval.dtx
%\fi
%\makeatletter
%\def\DescribeOption#1{\leavevmode\@bsphack
%              \marginpar{\raggedleft\PrintDescribeOption{#1}}%
%              \SpecialOptionIndex{#1}\@esphack\ignorespaces}
%\def\PrintDescribeOption#1{\strut\emph{option}\\\MacroFont #1\ }
%\def\SpecialOptionIndex#1{\@bsphack
%    \index{#1\actualchar{\protect\ttfamily#1}
%           (option)\encapchar usage}%
%    \index{options:\levelchar#1\actualchar{\protect\ttfamily#1}\encapchar
%           usage}\@esphack}
%\def\DescribeOptions#1{\leavevmode\@bsphack
%  \marginpar{\raggedleft\strut\emph{options}%
%  \@for\@tempa:=#1\do{%
%    \\\strut\MacroFont\@tempa\SpecialOptionIndex\@tempa
%  }}\@esphack\ignorespaces}
%\makeatother
%
% \changes{v1.0.0}{2016/10/31}{Initial released version}
% \changes{v1.0.1}{2016/11/07}{Prevent empty bibliography environment;
% fix typos}
%
% \GetFileInfo{apxproof.sty}
%
% \makeatletter\c@IndexColumns=2\makeatother
% \DoNotIndex{
%  \newcommand,\newenvironment,\end,\begin,\edef,\if,\else,\fi,\def,
%  \begingroup,\endgroup,\csname,\let,\noexpand,\protect,\expandafter,
%  \ifthenelse,\equal,\endcsname,\@empty,\@ifnotempty,\immediate,
%  \addtocounter,\newcounter,\newtoggle,\global,\ifdefined,\iftoggle,
%  \ifx,\jobname,\makeatletter,\makeatother,\newwrite,\NewEnviron,
%  \patchcmd,\relax,\renewcommand,\renewenvironment,\RequirePackage,
%  \roman,\space,\undefined,\unexpanded
% }
%
% \title{The \textsf{apxproof} package}
%
% \author{Pierre Senellart \\ \texttt{pierre@senellart.com} \\
% \url{http://github.com/PierreSenellart/apxproof}}
% \date{\filedate \quad \fileversion}
%
% \maketitle
%
% \begin{abstract}
% This package makes it easier to write articles where proofs and other material
% are deferred to the appendix. The appendix material is written in the \LaTeX{}
% code along with the main text which it naturally complements, and it is
% automatically deferred. The package can automatically send proofs to the
% appendix, can repeat in the appendix the theorem environments stated in the
% main text, can section the appendix automatically based on the sectioning of
% the main text, and supports a separate bibliography for the appendix material.
% \end{abstract}
%
% \section{Usage}
% The \textsf{apxproof} package is intended to simplify the writing of articles where some of
% the content needs to be deferred to an appendix. This is in particular
% useful for the submission of scientific articles to conferences or
% journals that limit the number of pages in the main text but allow an
% extra appendix, where proofs of theorems and other material can be added.
%
% \subsection{Basics}
% To use \textsf{apxproof}, first load it in the header of your document:
% \begin{quote}|\usepackage{apxproof}|\end{quote}
% On its own, this does not do anything and should not change the
% appearance of your document. To add an appendix with some material from
% your document, use the |toappendix| environment:
% \begin{quote}
% |\begin{toappendix}|\DescribeEnv{toappendix}\\
% \hspace*{1em}\dots\\
% |\end{toappendix}|
% \end{quote}
% The content will appear at the end of your document, in an
% automatically generated section that refers to the current section in the main
% text.
% \begin{example}
% Throughout this documentation, all examples produce content
% deferred to the appendix, at the very end of this document.
% \begin{verbatim}
% \begin{toappendix}
% This content is in the appendix.
% \end{toappendix}
% \end{verbatim}
% \begin{toappendix}
% This content is in the appendix.
% \end{toappendix}
% \end{example}
% \changes{v1.0.3}{2017/01/10}{Note on entire sections in appendix}
% When the content to put in appendix is an entire section, make sure
% that \verb|\section| is the very first command that appears within the
% \verb|toappendix| environment. It will disable the automatic production
% of a section heading.
% \subsection{Repeated Theorems and Proofs}
% In some scientific papers that include proofs, it is common to defer
% proofs to the appendix. This can easily be achieved using the
% |appendixproof| environment:
% \begin{quote}
% |\begin{appendixproof}|\DescribeEnv{appendixproof}\\
% \hspace*{1em}\dots\\
% |\end{appendixproof}|
% \end{quote}
% This behaves like the |toappendix| environment, except that
% a proof environment is generated.
% \begin{example}We now send a proof to the appendix:
% \begin{verbatim}
% \begin{appendixproof}
% This proof is in the appendix.
% \end{appendixproof}
% \end{verbatim}
% \begin{appendixproof}
% This proof is in the appendix.
% \end{appendixproof}
% \end{example}
%
% When deferring proofs to the appendix, an annoying problem is that the
% statement of the theorem remains in the main text; it is hard to read a
% proof that is far away from the statement it proves. \textsf{apxproof}
% solves this issue by allowing statements of theorems to be \emph{repeated}:
% once in the main text, and once in the appendix before the proof of
% the statement. To use this feature, you can define a new
% \emph{repeated theorem} environment using the |\newtheoremrep| command:
% \changes{v1.0.5}{2017/05/31}{Ability to specify a sectioning counter in newtheoremrep}
% \begin{quote}
% |\newtheoremrep|\marg{name}\oarg{counter}\marg{title}\oarg{countersec}\DescribeMacro{\newtheoremrep}
% \end{quote}
% Usage is exactly the same as that of AMS \LaTeX{}'s |\newtheorem|
% macro:
% \begin{itemize}
% \item \meta{name} (e.g., |theorem|) is the name of an environment that is created for this kind of
% theorem;
% \item \meta{counter} (e.g., |definition|) is an optional counter describing
% from which kind of environment the numbering of these environments should be
% inherited;
% \item \meta{title}
% (e.g., |Theorem|) is
% the title that will be used to display this theorem environment;
% \item \meta{countersec} (e.g., |section|) is an optional counter of a
% sectioning command indicating that counters for this theorem should
% be prefixed by this counter (and reset at each occurrence of the
% sectioning command).
% \end{itemize}
% \meta{counter} and \meta{countersec} should not be used together.
% What
% differs from |\newtheorem| is that, when the following is written:
% \begin{quote}
% |\newtheoremrep{foobar}{Foobar}|
% \end{quote}
% then \emph{two} environments are defined: the \verb|foobar|
% environment, which behaves as if |\newtheorem| had been used, and the
% |foobarrep| environment, which results in the statement of this
% environment being repeated in the appendix.
%
% One interesting feature of \textsf{apxproof} is that in most
% situations, there is no need to use the |appendixproof| environment.
% Indeed, the |proof| \DescribeEnv{proof} environment is redefined by \textsf{apxproof} to
% automatically put the proof either in the main text (if it follows a
% regular theorem) or in the appendix (if it follows a repeated
% theorem).
% \begin{example}
% Assume we have first defined a repeated theorem environment |foobar| as
% above.
% We can now use this theorem environment, first for a regular theorem in
% the main text, then for a theorem repeated in the main text and in the
% appendix:
% \begin{quote}
% \begin{verbatim}
% \begin{foobar}
% This foobar is a regular one, in the main text.
% \end{foobar}
% \begin{proof}
% This is the proof of the regular foobar.
% \end{proof}
% \end{verbatim}
% \end{quote}
% We obtain:
% \begin{foobar}
% This foobar is a regular one, in the main text.
% \end{foobar}
% \begin{proof}
% This is the proof of the regular foobar.
% \end{proof}
% Now, if we use a repeated theorem:
% \begin{quote}
% \begin{verbatim}
% \begin{foobarrep}
% This foobar is repeated in the appendix.
% \end{foobarrep}
% \begin{proof}
% This is the proof of the repeated foobar.
% \end{proof}
% \end{verbatim}
% \end{quote}
% We now obtain:
% \begin{foobarrep}
% This foobar is repeated in the appendix.
% \end{foobarrep}
% \begin{proof}
% This is the proof of the repeated foobar.
% \end{proof}
% Note that, since |hyperref| is loaded, there are hyperlinks
% created between the statements of the theorems in the main text and in
% the appendix.
% \end{example}
%
% When the proof is deferred to the appendix, it is common practice to
% add a proof sketch in the main text. \textsf{apxproof} defines a simple
% |proofsketch| environment for this purpose:
% \changes{v1.0.5}{2017/05/31}{Fix compilation of proofsketch environment in inline mode}
% \begin{quote}
% |\begin{proofsketch}|\DescribeEnv{proofsketch}\\
% \hspace*{1em}\dots\\
% |\end{proofsketch}|
% \end{quote}
% The proof sketch is typeset similarly to a proof, but is always in the
% main text. Similarly, an |inlineproof| \DescribeEnv{inlineproof}
% environment is provided so as to
% be able to have both a proof in the appendix (using the regular |proof|
% environment, or alternatively the |appendixproof| environment) and a
% different proof in the main text (using the |inlineproof| environment).
% \begin{example} Here are simple examples of proof sketches and inline
% proofs:
% \begin{verbatim}
% \begin{proofsketch}
% This is a proof sketch.
% \end{proofsketch}
% \end{verbatim}
% \begin{proofsketch}
% This is a proof sketch.
% \end{proofsketch}
% \begin{verbatim}
% \begin{inlineproof}
% This is an inline proof.
% \end{inlineproof}
% \end{verbatim}
% \begin{inlineproof}
% This is an inline proof.
% \end{inlineproof}
% \end{example}
%
% \subsection{Bibliography}
% By default, \textsf{apxproof} automatically adds a bibliography in the appendix
% with only the references cited in the appendix material. This allows for a
% clean separation of references used solely in the main text, and those
% used in the appendix.
% \begin{example}
% Assume we have citations both in the main text and in the appendix.
% \begin{verbatim}
% This is a citation in the main text~\cite{lamport86}.
% \begin{toappendix}
% This is a citation in the appendix~\cite{proofsAreHard}.
% \end{toappendix}
% \end{verbatim}
% This is a citation in the main text~\cite{lamport86}.
% \begin{toappendix}
% This is a citation in the appendix~\cite{proofsAreHard}.
% \end{toappendix}
% \end{example}
% The bibliography in the appendix can use
% a different style and heading than the bibliography in the main text (and, by
% default, it does). See
% Section~\ref{sec:customization} for how to configure the appearance of
% that bibliography.
%
% \DescribeOption{bibliography}
% In order to use a single appendix for the main text and the
% bibliography, one can specify the
% value |common| to the |bibliography| option when loading the package.
% (By default this option is set to |separate|.)
% \subsection{Mode}
% \DescribeOption{appendix}
% An optional \meta{mode} can be specified when loading the package:
% \begin{quote}|\usepackage[appendix=|\meta{mode}|]{apxproof}|\end{quote}
% \meta{mode} can take one of the following three values:
% \begin{description}
% \item[|append|] This is the default.
% Appendix material gathered by \textsf{apxproof} is appended to
% the main text.
% \item[|inline|] In this mode, \textsf{apxproof} simply inlines the
% content along with the main text.
% \item[|strip|] This mode functions similarly to |append| except that
% the appendix is not appended at the end of the document. All appendix
% material is therefore removed.
% \end{description}
%
% \subsection{Customization}
% \label{sec:customization}
% \textsf{apxproof} provides a few macros that can be redefined (using
% |\renewcommand|) to customize the appearance of the appendix:
% \begin{description}
% \item[\textbackslash|mainbodyrepeatedtheorem|]\DescribeMacro{\mainbodyrepeatedtheorem}
% is a macro that is executed at the beginning of the body of every
% repeated theorem. This can be used to notify the reader that the
% theorem is repeated in appendix in some way, e.g., with a margin note.
% \item[\textbackslash|appendixsectionformat|\marg{number}\marg{title}]\DescribeMacro{\appendixsectionformat} is a macro
% that indicates how to format the section titles in the Appendix, given
% the number and title of the section in the main text. By
% default, they appear as ``Proofs for Section~\meta{number}
% (\meta{title})''.
% \item[\textbackslash|appendixrefname|]\DescribeMacro{\appendixrefname} contains the heading that is displayed before
% the bibliography. By default, this is ``References for the
% Appendix''. (Note that this command is also defined and used by the
% |memoir| document class.)
% \item[\textbackslash|appendixbibliographystyle|]\DescribeMacro{\appendixbibliographystyle} contains the |.bst| bibliography
% style that is used in the bibliography in appendix. By default, this is
% |alpha|.
% \item[\textbackslash|appendixbibliographyprelim|]\DescribeMacro{\appendixbibliographyprelim} contains arbitrary code that is executed
% just before the production of the bibliography in appendix, which can
% be used to configure the way it is displayed.
% \item[\textbackslash|appendixprelim|]\DescribeMacro{\appendixprelim} contains arbitrary code that is executed
% just before the production of the appendix, which can
% be used to configure the way it is displayed. By default, this command
% contains |\clearpage\onecolumn| (the appendix is typeset on a new page
% in single-column mode) but redefining this option allows changing this
% behavior.
% \end{description}
% \DescribeOption{repeqn}
% Another customization capability concerns \emph{numbered equations} that are present
% within repeated theorems. An optional |repeqn| option can be specified
% when loading the package, which controls whether
% equation numbers should be as in the main text (by setting this option
% to |same|, the default) or independently
% numbered (by setting this option to |independent|). In the latter case,
% whenever a referenceable counter is set with |\label{|\meta{counter}|}|,
% |\ref{|\meta{counter}|}| references the counter in the main text, while
% |\ref{|\meta{counter}|-apx}| references the counter in the appendix
% (except in |inline| mode, where both have the same effect).
%
% \DescribeOption{forwardlinking}
% Another customization option concerns hyperlinking.
% Usually, when \textsf{hyperref} is loaded, |foobarrep|
% environments in the main text have their number link to their repetition in the
% appendix. To suppress this behavior and have |foobarrep| environments
% treated as if \textsf{hyperref} were not loaded, one can specify the
% value |no| to the |forwardlinking| option when loading the package. (By
% default this option is set to |yes|.)
%
% \subsection{Advanced Features}
% We now describe a few advanced macros and environments, the usage of
% which is limited to special cases:
% \begin{description}
% \item[|nestedproof|]\DescribeEnv{nestedproof} is an environment that
% can be used within a |proof| environment deferred in the appendix; this
% is required because, for technical reasons, no |proof| environment can
% be nested within a deferred |proof| environment.
% \item[\textbackslash|noproofinappendix|]\DescribeMacro{\noproofinappendix}
% can be used inside repeated theorems that are not followed by a
% |proof| or |appendixproof| environment; the point is to ensure that a further
% |proof| environment cannot be mistakenly understood as a proof of the repeated
% theorem. It should not be needed in most situations as
% \textsf{apxproof} tries figuring out when a proof follows a repeated
% theorem automatically, but may occasionally be needed in complex
% scenarios.
% \item[\textbackslash|nosectionappendix|]\DescribeMacro{\nosectionappendix}
% is to be used inside a section that \emph{does} contain appendix material, but
% for which a section in the appendix should not be created. This should
% be rarely needed. When this command is present, appendix material is
% appended to the end of the previously created section.
% \end{description}
% \section{Supported Document Classes}
% Because \textsf{apxproof} modifies sectioning commands, bibliographies,
% and proofs, it may not work straight away with arbitrary document classes.
% It has currently been tested with and is supported for the following
% document classes:
% \begin{itemize}
% \item \LaTeX{} standard document classes (e.g., |article.cls|)
% \item \href{https://www.ctan.org/pkg/koma-script}{KOMA-Script}
% (e.g., |scrartcl.cls|, |scrbook.cls|)
% \item \href{https://ctan.org/pkg/memoir}{|memoir.cls|}
% \item \href{https://www.acm.org/publications/proceedings-template}{ACM
% SIG Proceedings} (e.g., |sig-alternate.cls|, |acmart.cls|)
% \item \href{https://www.springer.com/computer/lncs/lncs+authors}{
% Springer's Lecture Notes in Computer Science} (e.g.,
% |llncs.cls|)
% \item
% \href{https://www.dagstuhl.de/en/publications/lipics}{Schlo\ss{}
% Dagstuhl's Leibniz International Proceedings in Informatics} (e.g.,
% |lipics.cls|, |lipcs-v2016.cls|)
% \end{itemize}
% Other classes may work out of the box. Adding support for specific
% classes is possible and can be requested from the
% author of this package.
% \section{Known Issues and Limitations}
% We report here some issues we are currently aware of:
% \begin{itemize}
% \item When using \textsf{hyperref}, the appendix in the bibliography is
% not hyperlinked. This is to avoid possible issues with multiply defined
% bibliography entries.
% \item |appendixproof|, |proof|, |toappendix| environments cannot be nested. This is a limitation of
% the \textsf{fancyvrb} package that \textsf{apxproof} relies on. Note
% the existence of the |nestedproof| environment for nested proofs.
% \item \textsf{apxproof} poorly interacts with Sync\TeX: identifying
% which source line has produced which box does not work for appendix
% content managed by \textsf{apxproof} or repeated theorems. No obvious
% fix is known, though this issue will be investigated in the long term.
% \item Unless the |bibliography| option is set to |common|, the
% \textsf{bibunits} package
% is used to generate a second bibliography. This means any package, such
% as \textsf{biblatex}, that is incompatible with \textsf{bibunits} will not be
% compatible with \textsf{apxproof} unless |bibliography| is set to |common|.
% \end{itemize}
%
% Issues not listed here should be reported to the author.
%
% \section{License}
% Copyright \textcopyright{} 2016--2022 by Pierre Senellart.
%
% This work may be distributed and/or modified under the conditions of the
% \LaTeX{} Project Public License, either version 1.3 of this license or (at
% your option) any later version. The latest version of this license is in
% \url{http://www.latex-project.org/lppl.txt} and version 1.3 or later is part of
% all distributions of \LaTeX{} version 2005/12/01 or later.
%
% \section{Contact}
% \begin{itemize}
% \item \url{https://github.com/PierreSenellart/apxproof}
% \item
% Pierre Senellart
% \href{mailto:pierre@senellart.com}{<pierre@senellart.com>}
% \end{itemize}
% Bug reports and feature requests should
% preferably be submitted through the \emph{Issues} feature of GitHub.
%
% \section{Acknowledgments}
% Thanks to Antoine Amarilli for feedback and proofreading. Thanks to K.~D.
% Bauer for the implementation of the forward-linking mechanism, and
% for various bugfixes. Thanks to  Leonid Kostrykin for an initial
% implementation of the |forwardlinking| option.
%
% \StopEventually{
%   \PrintChanges
%   \PrintIndex
% }
%
% \section{Implementation}
% We now describe the entire code of the package, in a literate programming
% fashion. Throughout the package, we use the |axp@| prefix to identify
% local macros and environment names, which are not meant to be used by the final
% user.
% \subsection{Dependencies}
% We first load a few package dependencies:
% \begin{itemize}
% \item \textsf{environ} to easily define the repeated theorem
% environments.
%    \begin{macrocode}
\RequirePackage{environ}
%    \end{macrocode}
% \item \textsf{etoolbox} to define simple toggles.
%    \begin{macrocode}
\RequirePackage{etoolbox}
%    \end{macrocode}
% \item \textsf{fancyvrb} for the bulk of the work of exporting appendix
% material in an auxiliary file.
%    \begin{macrocode}
\RequirePackage{fancyvrb}
%    \end{macrocode}
% \item \textsf{ifthen} for easier comparison of character strings.
%    \begin{macrocode}
\RequirePackage{ifthen}
%    \end{macrocode}
% \item \textsf{kvoptions} to manage options passed to the package.
%    \begin{macrocode}
\RequirePackage{kvoptions}
%    \end{macrocode}
% \item \textsf{catchfile} to be able to check the content of files
% |\input| within appendix content.
%    \begin{macrocode}
\RequirePackage{catchfile}
%    \end{macrocode}
% \item \textsf{amsthm} for its |\newteorem| macro.
% Some document classes (e.g., \textsf{lipics})
% preload \textsf{amsthm}: this is fine, |\RequirePackage{amsthm}|
% will simply have no effect. On the other hand, some other document
% classes (e.g., \textsf{llncs} or \textsf{sig-alternate}) define a
% |proof| environment that conflicts with \textsf{amsthm}, so we have to
% undefine this environment before loading \textsf{amsthm}. In that case,
% we reestablish the existing proof environments, in case they had been
% customized (e.g., \textsf{sig-alternate})
% \changes{v1.0.4}{2017/03/08}{Re-establish custom proof environments}
%    \begin{macrocode}
\@ifpackageloaded{amsthm}{
  }{
    \let\apx@oldamsthmproof\proof
    \let\apx@oldamsthmendproof\endproof
    \let\proof\undefined
    \let\endproof\undefined
  }
\RequirePackage{amsthm}
\ifdefined\apx@oldamsthmproof
  \let\proof\apx@oldamsthmproof
  \let\endproof\apx@oldamsthmendproof
\fi
%    \end{macrocode}
% \end{itemize}
% \subsection{Option Processing}
% Many names throughout the package use an arobase (|@|) to avoid name
% conflict with user-defined names. To simplify the compilation of the
% documentation, we simply make it a regular character in all the rest.
%    \begin{macrocode}
\makeatletter
%    \end{macrocode}
% We setup the processing of options using \textsf{keyval} facilities.
%    \begin{macrocode}
\SetupKeyvalOptions{
  family=axp,
  prefix=axp@
}
%    \end{macrocode}
% We declare the following options:
% \begin{itemize}
%   \item |appendix|, with a default value of |append| (other possible
%     values: |strip|, |inline|);
%   \item |bibliography|, with a default value of |separate| (other
%     possible value: |common|);
%   \item |repeqn|, with a default value of |same| (other possible value:
%   |independent|).
% \end{itemize}
% \begin{macro}{\axp@appendix}
%    \begin{macrocode}
\DeclareStringOption[append]{appendix}
%    \end{macrocode}
% \end{macro}
% \begin{macro}{\axp@bibliography}
% \changes{v1.0.4}{2017/03/02}{\texttt{bibliography} option}
%    \begin{macrocode}
\DeclareStringOption[separate]{bibliography}
%    \end{macrocode}
% \end{macro}
% \begin{macro}{\axp@repeqn}
% \changes{v1.1.0}{2018/07/20}{\texttt{repeqn} option}
%    \begin{macrocode}
\DeclareStringOption[same]{repeqn}
%    \end{macrocode}
% \end{macro}
% \begin{macro}{\axp@forwardlinking}
% \changes{v1.2.3}{2021/07/12}{\texttt{forwardlinking} option}
%    \begin{macrocode}
\DeclareStringOption[yes]{forwardlinking}
%    \end{macrocode}
% \end{macro}
%    \begin{macrocode}
\ProcessLocalKeyvalOptions*
%    \end{macrocode}
% We check that the value of the options are valid, and add a
% message to the compilation log.
%    \begin{macrocode}
\ifthenelse{\equal{\axp@appendix}{append}}{
  \message{apxproof: Appendix material appended to the document}
}{\ifthenelse{\equal{\axp@appendix}{strip}}{
  \message{apxproof: Appendix material stripped}
}{\ifthenelse{\equal{\axp@appendix}{inline}}{
  \message{apxproof: Appendix material inlined within the document}
}{
  \errmessage{Error: unsupported option appendix=\axp@appendix\ for
  package apxproof}
}}}
\ifthenelse{\equal{\axp@bibliography}{separate}}{
%    \end{macrocode}
% The external \textsf{bibunits} package
% is used to add a second bibliography for the appendix material.
% \changes{v1.2.0}{2019/04/17}{Do not load \textsf{bibunits} if
% \texttt{bibliography} is set to \texttt{common}}
%    \begin{macrocode}
  \RequirePackage{bibunits}
  \message{apxproof: Separate bibliography for appendix material}
}{\ifthenelse{\equal{\axp@bibliography}{common}}{
  \message{apxproof: Common bibliography for appendix and main text}
}{
  \errmessage{Error: unsupported option bibliography=\axp@bibliography\ for
  package apxproof}
}}
\ifthenelse{\equal{\axp@repeqn}{same}}{
  \message{apxproof: Repeated equations keep the same numbering}
}{\ifthenelse{\equal{\axp@repeqn}{independent}}{
  \message{apxproof: Repeated equations are independently numbered}
}{
  \errmessage{Error: unsupported option repeqn=\axp@repeqn\ for
  package apxproof}
}}
%    \end{macrocode}
% \begin{macro}{\axp@forward@suppress}
%    \begin{macrocode}
\newbool{axp@forward@suppress}
\ifthenelse{\equal{\axp@forwardlinking}{yes}}{
}{\ifthenelse{\equal{\axp@forwardlinking}{no}}{
  \message{apxproof: Disable forward linking}
  \global\booltrue{axp@forward@suppress}%
}{
  \errmessage{Error: unsupported option forwardlinking=\axp@repeqn\ for
  package apxproof}
}}
%    \end{macrocode}
% \end{macro}
% \subsection{Macros Common to All Compilation Modes}
% \begin{macro}{\axp@newtheoremrep@definetheorem}
% \changes{v1.2.0}{2019/10/01}{Restore predefined theorem counters}
% Common to all compilation modes, we define
% |\axp@newtheoremrep@definetheorem|.
% When called with first argument |foobar|, we first undefine the existing
% |foobar| environment (and its counter) if it has already been defined (e.g., by the
% document class), then invoke |\axp@newtheorem| for the regular version
% of the theorem |foobar|, saving and restoring any existing theorem counter unless the
% |\newtheoremdep| redefines the base counter.
%    \begin{macrocode}
\def\axp@newtheoremrep@definetheorem#1#2#3#4{%
  \expandafter\let\csname #1\endcsname\undefined
  \ifcsname c@#1\endcsname
    \expandafter\expandafter\expandafter\let\expandafter\expandafter
      \csname c@axp@#1\endcsname\csname c@#1\endcsname
    \expandafter\let\csname c@#1\endcsname\undefined
  \fi
  \axp@newtheorem{#1}{#2}{#3}{#4}%
  \ifcsname c@axp@#1\endcsname
    \ifx\relax#2\relax
      \expandafter\expandafter\expandafter\let\expandafter\expandafter
        \csname c@#1\endcsname\csname c@axp@#1\endcsname
    \else
    \fi
  \fi
}
%    \end{macrocode}
% \end{macro}
% \begin{macro}{\axp@newtheorem}
% \changes{v1.0.6}{2018/05/10}{Introduce intermediary command for theorem
% macro}
% \begin{macro}{\@axp@newtheorem}
% \begin{macro}{\@@axp@newtheorem}
% We introduce an intermediate |\axp@newtheorem| command to define a new
% theorem, differently depending on whether there is a section counter or
% not. This will be useful, in particular to allow changing this
% definition depending on the document class. This command uses two
% intermediary commands, |\@axp@newtheorem| and |\@@axp@newtheorem|, for
% the non-starred and starred versions.
%    \begin{macrocode}
\def\axp@newtheorem{\@ifstar\@@axp@newtheorem\@axp@newtheorem}
\def\@axp@newtheorem#1#2#3#4{%
  \ifx\relax#4\relax
    \newtheorem{#1}[#2]{#3}%
  \else
    \newtheorem{#1}{#3}[#4]%
  \fi
}
\def\@@axp@newtheorem#1#2{%
  \newtheorem*{#1}{#2}%
}
%    \end{macrocode}
% \end{macro}
% \end{macro}
% \end{macro}
% \begin{macro}{\newtheoremrep}
% \begin{macro}{\axp@newtheoremreptmp}
% We define the high-level |\newtheoremrep| to have the same syntax as
% \textsf{amsthm}'s |\newtheorem|. For this purpose, we need a little
% trick to deal with the second and fourth optional arguments, which is what
% |\@oparg| and |\axp@newtheoremreptmp| are
% used for. |\axp@newtheoremrep| is defined differently
% depending on the compilation mode.
%    \begin{macrocode}
\newcommand\newtheoremrep[1]{%
  \@oparg{\axp@newtheoremreptmp{#1}}[]%
}
\def\axp@newtheoremreptmp#1[#2]#3{%
  \@oparg{\axp@newtheoremrep{#1}[#2]{#3}}[]%
}
%    \end{macrocode}
% \end{macro}
% \end{macro}
% \begin{environment}{proofsketch}
% Simple |proofsketch| environment.
% \changes{v1.0.3}{2016/12/16}{Ignore spaces after beginning of Proof sketch}
%    \begin{macrocode}
  \newenvironment{proofsketch}{\begin{axp@oldproof}[Proof sketch]}{\end{axp@oldproof}}
%    \end{macrocode}
% \end{environment}
% \begin{macro}{\mainbodyrepeatedtheorem}
% \changes{v1.2.0}{2019/09/21}{Configurable repeated theorem command}
% \begin{macro}{\appendixrefname}
% \changes{v1.2.1}{2020/10/09}{Fix compatibility with
% \texttt{memoir} document class}
% \begin{macro}{\appendixbibliographystyle}
% \begin{macro}{\appendixbibliographyprelim}
% \begin{macro}{\appendixprelim}
% \changes{v1.0.4}{2017/03/03}{Configurable appendix style}
% \begin{macro}{\appendixsectionformat}
% \changes{v1.1.0}{2018/07/17}{Fix missing space in default
% \cs{appendixsectionformat}}
% We provide sensible defaults for these user-customizable macros.
% Even though they are not all useful in all modes, we define them for
% all modes so that a |\renewcommand| works in all cases.
%    \begin{macrocode}
\newcommand{\mainbodyrepeatedtheorem}{}
\providecommand{\appendixrefname}{References for the Appendix}
\newcommand{\appendixbibliographystyle}{alpha}
\newcommand{\appendixbibliographyprelim}{}
\newcommand{\appendixprelim}{\clearpage\onecolumn}
\newcommand{\appendixsectionformat}[2]{Proofs for Section~#1\ (#2)}
%    \end{macrocode}
% \end{macro}
% \end{macro}
% \end{macro}
% \end{macro}
% \end{macro}
% \end{macro}
% \begin{environment}{axp@oldproof}
%   We save the definition of the existing |proof| environment (and of
%   the |claimproof| environment that the \textsf{lipics} document class
%   defines).
%    \begin{macrocode}
  \let\axp@oldproof\proof
  \let\endaxp@oldproof\endproof
  \let\axp@oldclaimproof\claimproof
  \let\endaxp@oldclaimproof\endclaimproof
%    \end{macrocode}
% \end{environment}
% We define a utility macro that will be used to properly set the
% |\label| command (and its \textsf{amsmath} counterpart,
% |\label@in@display|) for equations within repeated theorems, depending on the
% compilation mode.
% \begin{macro}{\axp@redefinelabels}
% \changes{v1.1.0}{2018/07/04}{Fix \cs{label} not being disabled
% in \textsf{amsmath} environments, where \cs{label@in@display} is
% used instead (K. D. Bauer)}
% \changes{v1.2.0}{2019/02/15}{Fix extra spacing erroneously
% introduced within the \texttt{\textbackslash axp@redefinelabels}
% macro}
%    \begin{macrocode}
  \newcommand{\axp@redefinelabels}{%
    \providecommand\label@in@display{}%
    \ifthenelse{\equal{\axp@appendix}{inline}}{%
      \let\axp@oldlabel\label
      \let\axp@oldlabel@in@display\label@in@display
      \renewcommand\label[1]{%
        \axp@oldlabel{##1}%
        \axp@oldlabel{##1-apx}%
      }%
      \renewcommand\label@in@display[1]{%
        \axp@oldlabel@in@display{##1}%
        \axp@oldlabel{##1-apx}%
      }%
    }{%
      \let\axp@oldlabel\label
      \let\axp@oldlabel@in@display\label@in@display
      \renewcommand\label[1]{\axp@oldlabel{##1-apx}}%
      \renewcommand\label@in@display[1]{\axp@oldlabel@in@display{##1-apx}}%
    }%
  }
%    \end{macrocode}
% \end{macro}
% \subsubsection{Class-Specific Behavior}
% Finally, some class-specific behavior common to all compilation modes.
% \paragraph{\textsf{llncs} and other Springer document classes}
% \changes{v1.0.6}{2018/05/10}{Better support of Springer document
% classes}
%     \begin{macrocode}
   \ifdefined\spnewtheorem
%    \end{macrocode}
% \begin{macro}{\@axp@newtheorem}
% \begin{macro}{\@@axp@newtheorem}
% It is necessary to use |\spnewtheorem| instead of |\newtheorem| in
% Springer document classes to obtain standard formatting.
%    \begin{macrocode}
\def\@axp@newtheorem#1#2#3#4{%
  \ifx\relax#4\relax
    \ifx\relax#2\relax
      \spnewtheorem{#1}{#3}{\bfseries}{\itshape}%
    \else
      \spnewtheorem{#1}[#2]{#3}{\bfseries}{\itshape}%
    \fi
  \else
    \spnewtheorem{#1}{#3}[#4]{\bfseries}{\itshape}%
  \fi
}
\def\@@axp@newtheorem#1#2{%
  \spnewtheorem*{#1}{#2}{\upshape\bfseries}{\itshape}%
}
%    \end{macrocode}
% \end{macro}
% \end{macro}
% \begin{macro}{proofsketch}
% \changes{v1.2.0}{2019/02/15}{Fix proof sketches in inline
% compilation mode for Springer document classes}
% We redefine the |proofsketch| environment, which is used
% differently in the base class.
%    \begin{macrocode}
\renewenvironment{proofsketch}{\begin{axp@oldproof}[sketch]}{\end{axp@oldproof}}
%    \end{macrocode}
% \end{macro}
% We have to redefine the macro |\@thmcountersep| for proper sectioned
% counters.
%    \begin{macrocode}
\def\@thmcountersep{.}
  \fi
%    \end{macrocode}
% \subsection{Inline Compilation Mode}
%    \begin{macrocode}
\ifthenelse{\equal{\axp@appendix}{inline}}{
%    \end{macrocode}
% \begin{macro}{\axp@newtheoremrep}
% In inline mode, |\axp@newtheoremrep| uses
% |\axp@newtheoremrep@definetheorem| to define the regular theorem
% environment and creates a repeated theorem
% environment that behaves exactly as the regular theorem environment,
% while calling |\axp@redefinelabels| to make sure that |-axp| variants
% of equation counters are defined.
% \changes{v1.2.0}{2019/02/15}{Fix formatting of theorems without
% notes in some document classes in inline mode}
%    \begin{macrocode}
  \def\axp@newtheoremrep#1[#2]#3[#4]{%
    \axp@newtheoremrep@definetheorem{#1}{#2}{#3}{#4}%
    \NewEnviron{#1rep}[1][]{%
      \ifx\relax##1\relax
        \begin{#1}\axp@redefinelabels\BODY\end{#1}%
      \else
        \begin{#1}[##1]\axp@redefinelabels\BODY\end{#1}%
      \fi
    }
  }
%    \end{macrocode}
% \end{macro}
% \begin{environment}{inlineproof}
% \begin{environment}{nestedproof}
% \begin{environment}{appendixproof}
% In inline mode, these environments behave like the regular |proof|
% environment.
%    \begin{macrocode}
  \let\inlineproof\proof
  \let\endinlineproof\endproof
  \let\nestedproof\proof
  \let\endnestedproof\endproof
  \let\appendixproof\proof
  \let\endappendixproof\endproof
%    \end{macrocode}
% \end{environment}
% \end{environment}
% \end{environment}
% \begin{environment}{toappendix}
% \begin{macro}{\noproofinappendix}
% \begin{macro}{\nosectionappendix}
% In inline mode, this environment and these macros are no-ops.
%    \begin{macrocode}
  \newenvironment{toappendix}{}{}
  \let\noproofinappendix\relax
  \let\nosectionappendix\relax
%    \end{macrocode}
% \end{macro}
% \end{macro}
% \end{environment}
%    \begin{macrocode}
}
%    \end{macrocode}
% \subsection{Append or Strip Compilation Modes}
%    \begin{macrocode}
{
%    \end{macrocode}
% We now deal with the case where \textsf{apxproof} really does something
% useful: either append the appendix material to the document, or strip
% it entirely.
% \bigskip
%    \subsubsection{Auxiliary File for the Appendix}
% \begin{macro}{\axp@proofsfile}
% We open a new auxiliary file, with extension |.axp|, where the appendix
% material will be dumped.
% \changes{v1.1.0}{2018/07/11}{Initialization deferred to \cs{AtBeginDocument}
% for compatibility with \cs{dump}ed precompiled preambles (K. D.
% Bauer)}
%    \begin{macrocode}
  \AtBeginDocument{
    \newwrite\axp@proofsfile
    \immediate\openout\axp@proofsfile=\jobname.axp
  }
%    \end{macrocode}
% \end{macro}
% \begin{environment}{proof}
% \begin{macro}{\section}
% At the beginning of this file, we make |@| a regular character (since
% it will be used in several places for internal names) and reestablish the original definition of
% the |proof| environment and the |\section| macro.
%    \begin{macrocode}
  \AtBeginDocument{
    \immediate\write\axp@proofsfile{%
      \noexpand\makeatletter
      \noexpand\let\noexpand\proof\noexpand\axp@oldproof
      \noexpand\let\noexpand\endproof\noexpand\endaxp@oldproof
      \noexpand\let\noexpand\claimproof\noexpand\axp@oldclaimproof
      \noexpand\let\noexpand\endclaimproof\noexpand\endaxp@oldclaimproof
      \noexpand\let\noexpand\section\noexpand\axp@oldsection
    }
  }
%    \end{macrocode}
% \end{macro}
% \end{environment}
% \begin{macro}{\axp@unactivateeightbit}
% \changes{v1.1.0}{2019/01/28}{Fix compilation of non-ASCII
% characters with \texttt{\textbackslash usepackage[utf8]\{inputenc\}}}
% We need an auxiliary macro to disable active characters that have the
% high bit set when writing to the |.axp| file. See
% \url{https://tex.stackexchange.com/a/145361/166858}
%    \begin{macrocode}
  \def\axp@unactivateeightbit{%
    \count@=128%
    \loop
      \catcode\count@=12%
      \ifnum\count@<255%
      \advance\count@\@ne
    \repeat}
%    \end{macrocode}
% \end{macro}
% \begin{environment}{axp@VerbatimOut}
% \begin{macro}{\FVB@axp@VerbatimOut}
% \begin{macro}{\FVE@axp@VerbatimOut}
% \changes{v1.1.0}{2018/10/02}{Make \textsf{apxproof} compatible with
% independent use of \textsf{fancyvrb}}
% Using the functionalities of the \textsf{fancyvrb} package, we define a
% custom verbatim environment |axp@VerbatimOut| that writes every line
% to the |\axp@proofsfile|. We also use the previous macro to disable active
% characters with the eighth bit set, and we make sure the catcode of |@|
% is reset for every verbatim environment, in case it is used by the user (e.g.,
% as in the \textsf{xypic} package). Finally, as an additional
% precaution, we reset |\FV@CatCodesHook| that is for example set by the
% |commandchars| or |commentchar| option of |\fvset|.
% \changes{v1.2.1}{2020/01/01}{Fix compatibility with
% \textsf{xypic} package}
% \changes{v1.2.1}{2020/10/15}{Fix compatibility with other uses of \textsf{fancyvrb} that set
% \texttt{\textbackslash FV@CatCodesHook}}
%    \begin{macrocode}
  \DefineVerbatimEnvironment{axp@VerbatimOut}{axp@VerbatimOut}{}
  \def\FVB@axp@VerbatimOut{%
    \@bsphack
    \begingroup
      \axp@unactivateeightbit
      \FV@DefineWhiteSpace
      \def\FV@Space{\space}%
      \FV@DefineTabOut
      \def\FV@ProcessLine{\immediate\write\axp@proofsfile}%
      \let\FV@FontScanPrep\relax
      \let\@noligs\relax
      \def\FV@CatCodesHook{}%
      \FV@Scan}
  \def\FVE@axp@VerbatimOut{%
      \immediate\write\axp@proofsfile{\noexpand\makeatletter}%
      \endgroup\@esphack}
%    \end{macrocode}
% \end{macro}
% \end{macro}
% \end{environment}
% \begin{environment}{toappendix}
% The entire content of this environment is put in appendix,
% starting a new appendix section beforehand if needed.
%    \begin{macrocode}
  \newenvironment{toappendix}
    {\axp@writesection\axp@VerbatimOut}
    {\endaxp@VerbatimOut}
%    \end{macrocode}
% \end{environment}
%    \subsubsection{Definition of New Theorems}
% \begin{macro}{axp@seenreptheorem}
% Used to indicate whether a repeated theorem was just typeset, without
% its proof.
%    \begin{macrocode}
  \newtoggle{axp@seenreptheorem}
%    \end{macrocode}
% \end{macro}
% \begin{macro}{axp@rpcounter}
% Sequentially incremented for every repeated theorem, used to create labels.
%    \begin{macrocode}
  \newcounter{axp@rpcounter}
%    \end{macrocode}
% \end{macro}
% \begin{macro}{axp@equation}
% \begin{macro}{axp@equationx}
% Used to save the value of the |equation| counter, when |repeqn| is set
% to |same|.
%    \begin{macrocode}
  \newcounter{axp@equation}
  \newcounter{axp@equationx}
%    \end{macrocode}
% \end{macro}
% \end{macro}
% \begin{macro}{axp@newtheoremrep}
% With first argument |foobar|, we use
% |\axp@newtheoremrep@definetheorem| to define the regular version of the
% theorem |foobar|. We then patch |\begin{foobar}| so as not to
% expect a proof in the appendix and define an internal theorem |axp@foobarrp| that
% will be used in the appendix to restate the existing theorem.
%    \begin{macrocode}
  \def\axp@newtheoremrep#1[#2]#3[#4]{%
    \axp@newtheoremrep@definetheorem{#1}{#2}{#3}{#4}%
    \expandafter\pretocmd\csname #1\endcsname{\noproofinappendix}{}{}%
    \axp@newtheorem*{axp@#1rp}{#3}%
    \axp@forward@setup{#1}{#2}{#3}{#4}%
%    \end{macrocode}
% We then define a |foobarrep| environment that increments the
% |axp@rpcounter| and typeset the regular |foobar| theorem with a label
% derived from the counter, along with a possible custom command to
% identify repeated theorems. We distinguish the case when the theorem
% argument has a note and when it does not.
% \changes{v1.0.6}{2018/05/10}{Better handling of note-free theorems in
% document classes that treat theorems differently when they have an
% empty note}
% We save the equation counter
% before typesetting the theorem environment, to reset it to the same
% value in the repeated environment when |repeqn| is set to |same|.
% \changes{v1.2.2}{2020/11/25}{Fix handling of optional arguments of
% repeated theorems containing optional arguments}
%    \begin{macrocode}
    \NewEnviron{#1rep}[1][]{%
      \ifthenelse{\equal{\axp@repeqn}{same}}{%
        \setcounter{axp@equation}{\value{equation}}%
      }{}%
      \addtocounter{axp@rpcounter}{1}%
      \ifx\relax##1\relax
        \axp@with@forward{#1}{\begin{#1}}\label{axp@r\roman{axp@rpcounter}}%
      \else
        \axp@with@forward{#1}{\begin{#1}[{##1}]}\label{axp@r\roman{axp@rpcounter}}%
      \fi
      \mainbodyrepeatedtheorem
      \BODY\end{#1}%
%    \end{macrocode}
% We set the |axp@seenreptheorem| toggle to indicate that we are looking
% for the proof of the theorem, then store in a macro the content of the
% theorem's body.
%    \begin{macrocode}
      \global\toggletrue{axp@seenreptheorem}%
      \global\expandafter\let\csname rplet\roman{axp@rpcounter}%
                             \endcsname
      \BODY
%    \end{macrocode}
% Possibly after starting a new appendix section if needed, we typeset a
% repeated version of the theorem using the |axp@foobarrp| environment
% and a reference to the previously defined label.
% We use |\axp@redefinelabels| in this environment to avoid multiply
% defined labels. We have to deal in a careful way with theorem notes: we
% want to use a theorem note to display the number of the repeated
% theorem, but theorem notes are usually typeset in a much
% different way (different font, parentheses) than theorem
% headings. In the case of the Springer document
% classes, we use the  |\theopargself| macro to disable parentheses. For
% other document classes, we need to manually patch the |\thmhead|
% command at the right time. We also specially cover the case of
% the ACM document class where |\@acmplainnotefont| is used instead
% of |\thm@notefont|.
% \changes{v1.0.2}{2016/12/13}{Fix missing space between repeated theorem
% counter and theorem note}
% \changes{v1.0.2}{2016/12/13}{Fix display of repeated theorem counter in
% some document classes}
% \changes{v1.0.6}{2018/05/10}{Fix incorrect use of \texttt{\textbackslash noexpand}
% in optional argument of macro environment}
% \changes{v1.2.0}{2019/10/07}{Fix display of theorem notes}
%    \begin{macrocode}
      \axp@writesection%
      \immediate\write\axp@proofsfile{\noexpand\makeatletter}%
      \ifthenelse{\equal{\axp@repeqn}{same}}{%
        \immediate\write\axp@proofsfile{%
          \noexpand\setcounter{axp@equationx}{\value{equation}}%
          \noexpand\setcounter{equation}{\theaxp@equation}%
        }%
      }{}%
      \ifbool{axp@forward@suppress}{%
        \global\def\axp@refstar{\ref*}
      }{%
        \global\def\axp@refstar{\ref}
      }
      \immediate\write\axp@proofsfile{{%
        \ifdefined\theopargself
          \noexpand\theopargself
        \else
          \noexpand\pretocmd{\noexpand\@begintheorem}{%
            \noexpand\patchcmd{\noexpand\thmhead}{\noexpand\@acmplainnotefont}{}{}{}%
            \noexpand\patchcmd{\noexpand\thmhead}{\noexpand\the\noexpand\thm@notefont}{}{}{}%
            \noexpand\patchcmd{\noexpand\thmhead}{(}{}{}{}%
            \noexpand\patchcmd{\noexpand\thmhead}{)}{}{}{}%
          }{}{}
        \fi
        \noexpand\begin{axp@#1rp}
          [%
            \noexpand\axp@refstar{axp@r\roman{axp@rpcounter}}%
            \@ifnotempty{##1}{%
              \ifdefined\theopargself
              \else
                \ifdefined\@acmplainnotefont
                  \noexpand\@acmplainnotefont
                \else
                  \noexpand\ifdefined\noexpand\thm@notefont
                    \noexpand\the\noexpand\thm@notefont
                  \noexpand\fi
                \fi
              \fi
              {} (\unexpanded{{##1}})%
            }%
          ]%
          \noexpand\axp@forward@target{axp@fw@r\roman{axp@rpcounter}}{}%
          \noexpand\axp@redefinelabels
          \expandafter\noexpand\csname rplet\roman{axp@rpcounter}%
                               \endcsname
        \noexpand\end{axp@#1rp}
      }}%
      \ifthenelse{\equal{\axp@repeqn}{same}}{%
        \immediate\write\axp@proofsfile{%
          \noexpand\setcounter{equation}{\value{axp@equationx}}%
        }%
      }{}%
    }%
  }
%    \end{macrocode}
% \end{macro}
%
%    \subsubsection{Forward-Linking Mechanism}
% \changes{v1.1.0}{2018/07/02}{Added forward-link mechanism (K. D. Bauer)}
%
% When hyperref is loaded, |foobarrep| environments
% in the main text have their number link to their
% repetition in the appendix.
%
%

%
% \begin{macro}{\axp@with@forward}
% In order to make the number of the |foobarrep| theorem a link
% to its repeated version, we temporarily redefine the
% |\thefoobar| command, or, if we inherited the counter
% from a |bazbar| environment, the |\thebazbar| command.
% This seems to be the only robust way, to make the number
% a |\hyperlink|, without adding extensive dependence
% on internals of |amsthm|, the builtin |\newtheorem|
% and possibly document-class specific definitions.
%
% In order to allow users to redefine |\thefoobar| without
% breaking this feature, we redefine |\thefoobar| only
% for the duration of the |\begin{foobar}| form,
% resetting it to the old value as soon as possible.
%
% Redefining |\thefoobar| has the side effect of changing |\newlabel| entries
% in the |.aux| file, so we need to to be able to disable
% addition of the hyperlink, which is why we use an
% intermediate |\axp@forward@link|\marg{target}\marg{text} macro,
% We also redefine |\theHfoobar| which is used by |hyperref| but not
% defined if |hyperref| was loaded after |\newtheoremrep| was used.
% and |\protect| it to output it verbatim into the |.aux| file.
%
% These hyperlinks are of course disabled in the |strip| compilation
% mode.
%    \begin{macrocode}
   \newcommand{\axp@with@forward}[2]{%
     \ifthenelse{\equal{\axp@appendix}{strip}}{#2}{
       \global\booltrue{axp@forward}%
       \ifcsundef{axp@old@the\csname axp@cn@#1\endcsname}{%
         \csletcs{axp@old@the\csname axp@cn@#1\endcsname}{the\csname axp@cn@#1\endcsname}%
         \csletcs{theH\csname axp@cn@#1\endcsname}{the\csname axp@cn@#1\endcsname}%
         \csdef{the\csname axp@cn@#1\endcsname}{%
           \protect\axp@forward@link{axp@fw@r\roman{axp@rpcounter}}%
             {\csname axp@old@the\csname axp@cn@#1\endcsname\endcsname}%
         }%
       }{}%
       #2%
       \ifcsdef{axp@old@the\csname axp@cn@#1\endcsname}{%
         \csletcs{the\csname axp@cn@#1\endcsname}{axp@old@the\csname axp@cn@#1\endcsname}%
       }{}%
       \global\boolfalse{axp@forward}
     }}%
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\axp@forward@link}
% \begin{macro}{axp@forward}
% Dummy macro, for handling the unwanted change of
% the |\newlabel| entry in the |.aux| file caused by
% changing the definition of |\thefoobar|.
%
%    \begin{macrocode}
  \newbool{axp@forward}
  \newcommand{\axp@forward@link}[2]{%
    \ifboolexpr{ bool {axp@forward} and not bool {axp@forward@suppress} }{%
      \ifcsdef{hyperlink}{%
        \hyperlink{#1}{#2}%
      }{%
        #2%
      }%
    }{%
      #2%
    }%
  }%
%    \end{macrocode}
% \end{macro}
% \end{macro}
%
% \begin{macro}{\axp@forward@target}
% Provides the needed |\hypertarget|.
% Intended to be written to the |.axp| file.
%    \begin{macrocode}
  \newcommand{\axp@forward@target}[2]{%
    \ifcsname hypertarget\endcsname
      \hypertarget{#1}{#2}%
    \else
      #2%
    \fi
  }
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\axp@forward@setup}
% In order to support counter inheritance with the first
% optional argument of |\newtheoremrep|,
% we need access to the name of the counter.
% For compliance with the behavior of |\@axp@newtheorem|,
% the first optional argument (|#2|) is ignored
% if the second optional argument (|#4|) is given.
%    \begin{macrocode}
  \newcommand{\axp@forward@setup}[4]{%
    \csedef{axp@cn@#1}{\ifblank{#4}{\ifblank{#2}{#1}{#2}}{#1}}%
  }
%    \end{macrocode}
% \end{macro}
%
%
%    \subsubsection{Proof Environments}
% \begin{macro}{\noproofinappendix}
%   Utility macro that toggles |axp@seenreptheorem| to false.
%    \begin{macrocode}
  \newcommand\noproofinappendix{%
    \global\togglefalse{axp@seenreptheorem}%
  }
%    \end{macrocode}
% \end{macro}
% \begin{environment}{appendixproof}
% \changes{v1.2.4}{2021/11/03}{Support optional arguments in proofs}
% We dump the content of this in appendix, within an original |proof|
% environment, possibly after creating a new appendix section.
% We support
% optional arguments in proofs, but we need to be careful not to gobble
% any newline character, that would make it impossible to process the
% first line with \textsf{fancyvrb}.
%    \begin{macrocode}
  \def\appendixproof{\catcode`\^^M=\active\@ifnextchar[{\catcode`\^^M=5\@@appendixproof}{\catcode`\^^M=5\@appendixproof}}
  \def\@appendixproof
    {%
      \axp@writesection
      \immediate\write\axp@proofsfile{%
        \noexpand\makeatletter\noexpand\begin{axp@oldproof}\noexpand\makeatother%
      }%
      \axp@VerbatimOut
    }
  \def\@@appendixproof[#1]%
    {%
      \axp@writesection
      \immediate\write\axp@proofsfile{%
        \noexpand\makeatletter\noexpand\begin{axp@oldproof}[\unexpanded{#1}]\noexpand\makeatother%
      }%
      \axp@VerbatimOut
    }
  \def\endappendixproof
    {%
      \endaxp@VerbatimOut
      \immediate\write\axp@proofsfile{%
        \noexpand\end{axp@oldproof}%
      }%
      \noproofinappendix
    }
%    \end{macrocode}
% \end{environment}
% \begin{environment}{proof}
% This environment either puts the proof in appendix, if we are after a repeated
% theorem without its proof, or inlines it otherwise. We support
% optional arguments in proofs, but we need to be careful not to gobble
% any newline character, that would make it impossible to process the
% first line with \textsf{fancyvrb}.
%    \begin{macrocode}
  \def\proof{\catcode`\^^M=\active\ltx@ifnextchar@nospace[{\catcode`\^^M=5\axp@@proof}{\catcode`\^^M=5\axp@proof}}
  \def\axp@proof
    {%
      \iftoggle{axp@seenreptheorem}{%
        \appendixproof
      }{%
        \axp@oldproof
      }%
    }
  \def\axp@@proof[#1]%
    {%
      \iftoggle{axp@seenreptheorem}{%
        \appendixproof[#1]
      }{%
        \axp@oldproof[#1]
      }%
    }
  \def\endproof
    {%
      \iftoggle{axp@seenreptheorem}{%
        \endappendixproof
      }{%
        \endaxp@oldproof
      }%
    }
%    \end{macrocode}
% \end{environment}
% \begin{environment}{claimproof}
% \changes{v1.2.4}{2021/11/03}{Support for \texttt{claimproof} environment
% from \textsf{lipics}}
% If the |claimproof| environment exists (\textsf{lipics} document
% class), we also redefine it, in the same way.
%    \begin{macrocode}
  \ifdefined\claimproof
  \def\claimproof{\catcode`\^^M=\active\ltx@ifnextchar@nospace[{\catcode`\^^M=5\axp@@claimproof}{\catcode`\^^M=5\axp@claimproof}}
  \def\axp@claimproof
    {%
      \iftoggle{axp@seenreptheorem}{%
        \appendixproof
      }{%
        \axp@oldclaimproof
      }%
    }
  \def\axp@@claimproof[#1]%
    {%
      \iftoggle{axp@seenreptheorem}{%
        \appendixproof[#1]
      }{%
        \axp@oldclaimproof[#1]
      }%
    }
  \def\endclaimproof
    {%
      \iftoggle{axp@seenreptheorem}{%
        \immediate\write\axp@proofsfile{%
          \noexpand\makeatletter
          \noexpand\let\noexpand\endaxp@oldproof\noexpand\endaxp@oldclaimproof
          \noexpand\makeatother
        }%
        \endappendixproof
      }{%
        \endaxp@oldclaimproof
      }%
    }
  \fi
%    \end{macrocode}
% \end{environment}

% \begin{environment}{inlineproof}
% \begin{environment}{nestedproof}
% These two environments are synonyms for the original |proof|
% environment.
%    \begin{macrocode}
  \let\inlineproof\axp@oldproof
  \let\endinlineproof\endaxp@oldproof
  \let\nestedproof\axp@oldproof
  \let\endnestedproof\endaxp@oldproof
%    \end{macrocode}
% \end{environment}
% \end{environment}
%    \subsubsection{Section Management}
% \begin{macro}{axp@seccounter}
% Sequentially incremented for every section, used to create labels.
%    \begin{macrocode}
  \newcounter{axp@seccounter}
%    \end{macrocode}
% \end{macro}
% \begin{macro}{\axp@sectitle}
% Saves the title of the last encountered section.
%    \begin{macrocode}
  \def\axp@sectitle{}
%    \end{macrocode}
% \end{macro}
% \begin{macro}{\axp@section}
% \changes{v1.2.2}{2021/06/23}{Detect a section within an included
% file to avoid produced useless sections}
% \begin{macro}{\axp@@sectiontestinput}
% \begin{macro}{\axp@@sectiontestsection}
% This command |\axp@section| behaves similarly to |\axp@oldsection|,
% except that it first tests whether a |\section| follows, and if so,
% does not produce anything. This is useful to avoid producing empty
% sections in the appendix. Using the \textsf{catchfile} package, we
% also check whether a |\section| is within an |\input| that immediately
% follows.
%    \begin{macrocode}
  \def\axp@section#1{%
    \@ifnextchar\input
      {\axp@@sectiontestinput{#1}}%
      {\axp@@sectiontestsection{#1}}%
  }
  \def\axp@@sectiontestinput#1\input#2{%
    \CatchFileDef{\axp@tmp}{#2}{}%
    \def\axp@tmptmp{\axp@@sectiontestsection{#1}}%
    \expandafter\axp@tmptmp\axp@tmp%
  }
  \def\axp@@sectiontestsection#1{\@ifnextchar\section{\makeatother}{\axp@oldsection{#1}\makeatother}}
%    \end{macrocode}
% \end{macro}
% \end{macro}
% \end{macro}
% \begin{macro}{\axp@oldsection}
% \begin{macro}{\section}
% \changes{v1.1.0}{2018/07/25}{Rewrote definition of \cs{section}
% to enable optional argument. See \#23. (K. D. Bauer)}
% \changes{v1.1.0}{2018/07/25}{Fix handling of fragile macros within
% section headings. See \#22.}
% \begin{macro}{\@section}
% \begin{macro}{\@@section}
% We redefine the |\section| command to create a label based on
% |axp@seccounter| and to store its title in |\axp@sectitle|.
% In order to support starred and unstarred versions, as well
% as the optional short-title argument, the intermediate macros
% \cs{@section} and \cs{@@section} are needed.
%    \begin{macrocode}
  \let\axp@oldsection\section
  \def\section{\@ifstar\@section\@@section}
  \newcommand{\@section}[2][\relax]{\axp@@@section{*}{#1}{#2}}%
  \newcommand{\@@section}[2][\relax]{\axp@@@section{}{#1}{#2}}%
  \newcommand{\axp@@@section}[3]{%
    \global\def\axp@sectitle{#3}%
    \ifx\relax#2\relax
      \axp@oldsection#1{#3}%
    \else
      \axp@oldsection#1[{#2}]{#3}%
    \fi
    \addtocounter{axp@seccounter}{1}%
    \label{axp@s\roman{axp@seccounter}}%
  }
%    \end{macrocode}
% \end{macro}
% \end{macro}
% \end{macro}
% \end{macro}
% \begin{macro}{\nosectionappendix}
% We remove the current section title, to indicate no section should be
% created in the appendix.
%    \begin{macrocode}
  \newcommand{\nosectionappendix}{
    \global\def\axp@sectitle{}%
  }
%    \end{macrocode}
% \end{macro}
% \begin{macro}{\axp@writesection}
% If |\axp@sectitle| is not empty, we create
% a new section in the appendix, referring to the main text section.
%
% Here, we wrap |\ref{axp@si}| into |\axp@protectref@i|, in order
% to protect the label name from wrongly being converted to uppercase,
% e.g., in \textsf{fancyhdr} with |\pagestyle{fancy}|.
%
% This macro is defined both in the |.aux| file (in order to ensure availability
% when typesetting the |\tableofcontents|), and immediately before typesetting
% the appendix section (to ensure availability in the |\section| command).
%
% \changes{v1.0.6}{2018/05/10}{Fix extraneous space after section number
% in appendix titles}
% \changes{v1.1.0}{2018/07/09}{Make \cs{axp@tmp} wrapper more robust.
% Resolves issues from use of section title in \textsf{fancyhdr},
% and in \cs{tableofcontents} (K. D. Bauer).}
%    \begin{macrocode}
  \newcommand\axp@writesection{%
    \ifx\axp@sectitle\@empty
    \else
      \edef\axp@tmp{%
        \noexpand\global\noexpand\def
        \expandonce{\csname axp@protectref@\roman{axp@seccounter}\endcsname}{%
          \noexpand\ref{axp@s\roman{axp@seccounter}}%
        }%
      }%
      \immediate\write\@auxout{\expandonce\axp@tmp}
      \immediate\write\axp@proofsfile{%
        \expandonce\axp@tmp^^J%
        \noexpand\axp@section{%
          \noexpand\appendixsectionformat{%
            \protect
            \expandonce{\csname axp@protectref@\roman{axp@seccounter}\endcsname}%
          }{\expandonce\axp@sectitle}%
        }%
      }%
      \nosectionappendix
    \fi
  }
%    \end{macrocode}
% \end{macro}
% Finally, in a somewhat ad hoc manner, we disable the whole section management
% for \cs{tableofcontents}, which may be typeset using a section heading,
% but for which automatic section management does not make sense.
%
% \begin{macro}{\axp@oldtableofcontents}
% \begin{macro}{\tableofcontents}
% \changes{v1.1.0}{2018/07/09}{Disable section management for table
% of contents}
%    \begin{macrocode}
  \let\axp@oldtableofcontents\tableofcontents
  \def\tableofcontents{{\let\section\axp@oldsection\axp@oldtableofcontents}}
%    \end{macrocode}
% \end{macro}
% \end{macro}
%    \subsubsection{Append Compilation Mode}
%    \begin{macrocode}
  \ifthenelse{\equal{\axp@appendix}{append}}{
%    \end{macrocode}
% \begin{macro}{\axp@oldbibliography}
% \begin{macro}{\bibliography}
% Unless the |bibliography| option is set to |common|, we need to set the
% appendix bibliography source to be the same as that of the main
% text, thanks to \textsf{bibunits}'s |\defaultbibliography| macro.
%    \begin{macrocode}
    \ifthenelse{\equal{\axp@bibliography}{separate}}{
      \let\axp@oldbibliography\bibliography
      \renewcommand\bibliography[1]{%
        \defaultbibliography{#1}%
        \axp@oldbibliography{#1}%
      }
    }{}
%    \end{macrocode}
% \end{macro}
% \end{macro}
% After the end of the main text, we add the appendix (after the command
% |\appendixprelim| is issued)
% within a |bibunit| environment so as to typeset
% a separate bibliography for the appendix (unless the |bibliography|
% option is set to |common|). This is done using |\pretocmd| on
% |\@enddocumenthook| instead of |\AtEndDocument| because we want the
% code to be run before any code in the |\@enddocumenthook| that has
% been set in the document class, as in the \textsf{amsart} document
% class.
% \changes{v1.2.2}{2021/03/23}{Compatibility with AMS document classes: do not
% use \texttt{\textbackslash AtEndDocument}}
% There is an extra test to
% ensure an empty bibliography environment is not produced.
% The name of the bibliography is changed to |\appendixrefname|; in most
% document classes, it is called |\refname| but it is occasionally
% (|scrartcl|, |scrreprt|) called |\bibname|. An ad-hoc test is added
% to fix a conflict with the \textsf{natbib} package which redefines
% |bibcite| at the end of the document.
% \changes{v1.0.6}{2018/05/10}{Deal with document classes where the
% bibliography is called \texttt{\textbackslash bibname}}
% \changes{v1.2.1}{2020/02/27}{Ad hoc fix for \textsf{natbib}
% package conflict}
% \changes{v1.2.3}{2021/08/03}{More robust redefinition of
% \texttt{thebibliography} environment, for compatibility with
% \textsf{tocbibind}}
%    \begin{macrocode}
    \pretocmd{\@enddocumenthook}{%
      \ifdefined\NAT@testdef
        \renewcommand\bibcite[2]{%
          \global\@namedef{b@#1\@extra@binfo}{#2}%
        }
      \fi
      \appendixprelim
      \appendix
      \ifthenelse{\equal{\axp@bibliography}{separate}}{
      \begin{bibunit}[\appendixbibliographystyle]
      }{}
        \immediate\closeout\axp@proofsfile
        \input{\jobname.axp}
      \ifthenelse{\equal{\axp@bibliography}{separate}}{
        \ifdefined\refname
          \renewcommand{\refname}{\appendixrefname}
        \else\ifdefined\bibname
          \renewcommand{\bibname}{\appendixrefname}
        \fi\fi
        \let\axp@oldthebibliography\thebibliography
        \let\endaxp@oldthebibliography\endthebibliography
        \renewenvironment{thebibliography}[1]{%
          \def\axp@tmp{#1}%
          \ifx\axp@tmp\empty
            \gdef\axp@noappendixbibliography1\relax
          \else
            \begin{axp@oldthebibliography}{#1}%
          \fi
        }{%
          \ifdefined\axp@noappendixbibliography\relax\else\end{axp@oldthebibliography}%
        \fi}
        \appendixbibliographyprelim
        \putbib
      \end{bibunit}
      \ifdefined\NAT@testdef
        \let\bibcite\NAT@testdef
      \fi
      }{}
    }{}{}
%    \end{macrocode}
%    \begin{macrocode}
  }{}
%    \end{macrocode}
% \subsubsection{Class-Specific Behavior}
% We conclude with some class-specific behavior.
% \paragraph{ACM Document Classes (old versions, till 2017)}
% \changes{v1.0.4}{2017/03/08}{More faithful theorem style for ACM templates}
% \changes{v1.0.4}{2017/03/08}{More robust coherent styling of proof sketches}
%    \begin{macrocode}
  \ifdefined\@acmtitlebox
%    \end{macrocode}
% We first redefine the |proofsketch| environment, which is used
% differently in the base class.
%    \begin{macrocode}
  \renewenvironment{proofsketch}{\begin{axp@oldproof}[sketch]}{\end{axp@oldproof}}
%    \end{macrocode}
% We adjust the styling of theorems for the needs of \textsf{apxproof}.
%    \begin{macrocode}
  \newtheoremstyle{mystyle}
    {6pt}
    {6pt}
    {\itshape}
    {10pt}
    {\scshape}
    {.}
    {.5em}
    {}
  \theoremstyle{mystyle}
%    \end{macrocode}
% \begin{macro}{\thebibliography}
% \begin{macro}{\refname}
% \begin{macro}{\appendixrefname}
% The section title of the bibliography is in uppercase in these document
% classes. In addition, the |\thebibliography| macro hard-codes twice
% the section title, so we un-hardcode it so that it can be modified
% in the appendix.
%    \begin{macrocode}
    \patchcmd{\thebibliography}{References}{\protect\refname}{}{}
    \patchcmd{\thebibliography}{References}{\protect\refname}{}{}
    \newcommand{\refname}{REFERENCES}
    \renewcommand{\appendixrefname}{REFERENCES FOR THE APPENDIX}
%    \end{macrocode}
% \end{macro}
% \end{macro}
% \end{macro}
%
%    \begin{macrocode}
  \fi
%    \end{macrocode}
% \changes{v1.0.6}{2018/05/10}{Support of new ACM document class
% (\texttt{acmart.cls})}
% \paragraph{\textsf{lipcs}}
%    \begin{macrocode}
   \ifdefined\lipics@opterrshort
%    \end{macrocode}
% \begin{macro}{\appendixbibliographyprelim}
% \changes{v1.0.3}{2017/02/06}{Support for lipics-v2016}
% The default bibliography in the \textsf{lipics} document class
% formatting is not compatible with the
% \textsf{alpha} bibliography style. We fix this here.
%    \begin{macrocode}
    \renewcommand{\appendixbibliographyprelim}{%
      \global\let\@oldbiblabel\@biblabel
      \def\@biblabel{\hspace*{-2em}\small\@oldbiblabel}%
    }
%    \end{macrocode}
% \end{macro}
%    \begin{macrocode}
  \fi
}
%    \end{macrocode}
% \Finale
% \bibliographystyle{plain}
% \bibliography{apxproof}