\def\orcid#1{{\href{http://orcid.org/#1}{\protect\raisebox{-1.25pt}{\protect\includegraphics{orcid.pdf}}}}}
\def\orcid#1{\orcidID{#1}}

\bibliographystyle{splncs04}
% \usepackage{amsthm}
\usepackage{cite}
\usepackage{etoolbox}
\usepackage{dcolumn}
\usepackage{algorithmicx}
\usepackage{regexpatch}
\usepackage{algorithm}% http://ctan.org/pkg/algorithms
\usepackage[noend]{algpseudocode}% http://ctan.org/pkg/algorithmicx
\usepackage{prftree}
\usepackage[utf8]{inputenc}
% \usepackage[T1]{fontenc}
% \usepackage[english]{babel}
\usepackage{enumerate}
\usepackage[final]{graphicx}
\usepackage{tikz}
\usepackage{pgfplots}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{mathtools}
%\usepackage{subcaption}
%\usepackage{caption}
\usepackage{booktabs}
\usepackage{stmaryrd}
\usepackage[nomessages]{fp}
\usepackage{setspace}
\usepackage{xargs}[2008/03/08]
\usepackage{xr}
\usepackage{xcolor}
\usepackage{stackengine}
\usepackage{calc}
\usepackage{cancel}
\usepackage[mathscr]{eucal}
%%% or a
\usepackage[f]{esvect}
\usepackage{bussproofs}
\usepackage{ocgbase}
\usepackage{tcolorbox}
\usepackage{tikzpagenodes}
\usepackage{linegoal}
\usepackage{units}
\usepackage{url}
%\captionsetup{justification=raggedright,singlelinecheck=false}
\xpatchcmd{\algorithmic}{\labelsep 0.5em}{\labelsep 3em}{\typeout{Success!}}{\typeout{Oh dear!}}

\hyphenation{hyper-plane hyper-planes hyper-line hyper-lines super-posi-tion
  non-commut-a-tion Fibo-nacci Zip-per-posi-tion}

% Used for displaying a sample figure. If possible, figure files should be
% included in EPS format.

\usepackage[
   a4paper,
   pdftex,
%   pdftitle={SAT-Inspired Higher-Order Eliminations},
%   pdfauthor={Jasmin Blanchette and Petar Vukmirovi\'c},
   pdfkeywords={},
   pdfborder={0 0 0},
   draft=false,
   colorlinks,linkcolor=blue,citecolor=blue,urlcolor=blue,
   bookmarksnumbered,
   bookmarks,
   bookmarksdepth=2,
   bookmarksopenlevel=2,
   bookmarksopen]{hyperref}
% If you use the hyperref package, please uncomment the following line to
% display URLs in blue roman font according to Springer's eBook style:
\renewcommand\UrlFont{\color{blue}\rmfamily}

%\usepackage[mathlines]{lineno}
%\linenumbersep=100pt
%\linenumbers
%
%\newcommand*\patchAmsMathEnvironmentForLineno[1]{%
%  \expandafter\let\csname old#1\expandafter\endcsname\csname #1\endcsname
%  \expandafter\let\csname oldend#1\expandafter\endcsname\csname end#1\endcsname
%  \renewenvironment{#1}%
%     {\linenomath\csname old#1\endcsname}%
%     {\csname oldend#1\endcsname\endlinenomath}}% 
%\newcommand*\patchBothAmsMathEnvironmentsForLineno[1]{%
%  \patchAmsMathEnvironmentForLineno{#1}%
%  \patchAmsMathEnvironmentForLineno{#1*}}%
%\AtBeginDocument{%
%\patchBothAmsMathEnvironmentsForLineno{equation}%
%\patchBothAmsMathEnvironmentsForLineno{align}%
%\patchBothAmsMathEnvironmentsForLineno{flalign}%
%\patchBothAmsMathEnvironmentsForLineno{alignat}%
%\patchBothAmsMathEnvironmentsForLineno{gather}%
%\patchBothAmsMathEnvironmentsForLineno{multline}%
%}
%
%\usepackage{etoolbox} %% <- for \cspreto, \csappto, \patchcmd, \pretocmd, \apptocmd
%
%% Patch 'normal' math environments:
%\newcommand*\linenomathpatch[1]{%
%  \cspreto{#1}{\linenomath}%
%  \cspreto{#1*}{\linenomath}%
%  \cspreto{end#1}{\endlinenomath}%
%  \cspreto{end#1*}{\endlinenomath}%
%}
%%% Patch AMS math environments:
%\newcommand*\linenomathpatchAMS[1]{%
%  \cspreto{#1}{\linenomathAMS}%
%  \cspreto{#1*}{\linenomathAMS}%
%  \csappto{end#1}{\endlinenomath}%
%  \csappto{end#1*}{\endlinenomath}%
%}
%
%%% Definition of \linenomathAMS depends on whether the mathlines option is provided
%\expandafter\ifx\linenomath\linenomathWithnumbers
%  \let\linenomathAMS\linenomathWithnumbers
%  %% The following line gets rid of an extra line numbers at the bottom:
%  \patchcmd\linenomathAMS{\advance\postdisplaypenalty\linenopenalty}{}{}{}
%\else
%  \let\linenomathAMS\linenomathNonumbers
%\fi
%
%\linenomathpatch{equation}
%\linenomathpatchAMS{gather}
%\linenomathpatchAMS{multline}
%\linenomathpatchAMS{align}
%\linenomathpatchAMS{alignat}
%\linenomathpatchAMS{flalign}

%from LyX
\makeatletter
\global\let \oldquad\quad
\global\let \oldqquad\qquad
\global\long\def\skip{}%
\global\long\def\s{\ }%
\global\long\def\quad{\oldquad}%
\global\long\def\qquad{\oldqquad}%
\global\long\def\underline#1{\text{\leavevmode\vtop{\hbox{\ensuremath{#1}}\kern0.4ex  \hrule height.4pt}}}%
\global\long\def\sulut#1{\left(#1\right)}%
\global\long\def\makeop#1{\operatorname{#1}}%
\global\long\def\makelim#1#2{\operatorname*{#1}\limits _{#2}}%
\global\long\def\back#1{\hspace{-#1em}}%
\global\long\def\on#1{\mathchoice{\raisebox{-4.5pt}{$\scalebox{1}[1.5]{|}$}\raisebox{-3pt}{\ensuremath{_{#1}}}}{\raisebox{-3pt}{\ensuremath{\scalebox{1}[1.5]{|}}}\raisebox{-1.5pt}{\ensuremath{_{#1}}}}{\raisebox{-1pt}{\ensuremath{{\scriptstyle |}}}\raisebox{-1pt}{\ensuremath{_{{\scriptscriptstyle #1}}}}}{\raisebox{-0.5pt}{${\scriptscriptstyle |}$}_{#1}} }%
\global\long\def\eri{\not\approx}%
\newcommandx\integ[2][usedefault, addprefix=\global, 1=\skip]{\int_{#2}^{#1}\negthickspace}%
\global\long\def\set#1#2{\left\{  #1\boldsymbol\mid#2\right\}  }%
%\global\long\def\url#1{\text{\href{#1}{#1}}}%  %%% Commented out by Jasmin Blanchette -- cause trouble with _
\global\long\def\seq#1{\vec{#1}}%
\global\long\def\tuple#1{\vec{#1}}%
\global\long\def\holdsIn{\mathrel{\veny\models1{-1}}}%
\global\long\def\rule#1#2#3{{\scriptstyle #2}{\displaystyle \frac{#3}{#1}}}%
\global\long\def\link#1#2{\hyperref[#2]{{\color{black}#1}}}%
\global\long\def\hdim#1{\makeop{dim}_{#1}}%
\global\long\def\vdim{\makeop{dim}^{\text{vec}}}%
\newcommandx\ofdeg[2][usedefault, addprefix=\global, 1=, 2=d]{#1^{\makeop{deg}\leq#2}}%
\let\disjunction\vee \def\vee{\mathrel{\disjunction}}
\delimiterfactor=547
\delimitershortfall=99pt
\let\oldleft\left
\let\oldright\right 
\def\left{\mathopen{}\mathclose\bgroup\oldleft}
\def\right{\aftergroup\egroup\oldright}
\newcommand{\noun}[1]{\textsc{#1}}
\makeatother

\newcommand\cst[1]{\mathsf{#1}}

%% TYPESETTING: hacks
\newcommand\medrightarrow{\mathrel{{{\color{black}\relbar}\kern-0.9ex\rlap{\color{white}\ensuremath{\blacksquare}}\kern-0.9ex}\joinrel{\color{black}\rightarrow}}}
\newcommand\medleftarrow{\mathrel{{\color{black}\leftarrow}\kern-0.9ex\rlap{\color{white}\ensuremath{\blacksquare}}\kern-0.9ex\joinrel{{\color{black}\relbar}}}}
\newcommand\medleftrightarrow{\mathrel{\leftarrow\kern-1.685ex\rightarrow}}
\newcommand\Medrightarrow{\mathrel{{{\color{black}\Relbar}\kern-0.9ex\rlap{\color{white}\ensuremath{\blacksquare}}\kern-0.9ex}\joinrel{\color{black}\Rightarrow}}}
\newcommand\Medleftrightarrow{\mathrel{\Leftarrow\kern-1.685ex\Rightarrow}}

% Usage: \tooltip [color!transparency (default yellow!10)] {link text} {tip text}
% The link and tip texts can be formated and colored freely. The tooltip shows and hides by clicking the link text. Required packages are {ocgbase, tcolorbox, tikzpagenodes, linegoal, calc}. See https://tex.stackexchange.com/questions/155518/tooltip-that-works-with-all-pdf-readers
\makeatletter\catcode`_=11\catcode`:=11
\newcommand\tooltip[3][yellow!10]{{%
\leavevmode%
% put tip box on a PDF layer (OCG)
\ocgbase@new@ocg{tipOCG.\thetcnt}{/Print<</PrintState/OFF>>/Export<</ExportState/OFF>>}{false}%
\xdef\tipOCG{\ocgbase@last@ocg}%
\ocgbase@add@ocg@to@radiobtn@grp{tool@tips}{\tipOCG}% show max 1 tip
\pbs_pdflink:nn{%
	/Subtype/Link/Border[0 0 0]/A <</S/SetOCGState/State [/Toggle \tipOCG]>>
}{#2}%
\sbox\tiptext{%
	\ocgbase@oc@bdc{\tipOCG}\ocgbase@open@stack@push{\tipOCG}%
	\tcbox[colframe=black,colback=#1,size=fbox,arc=1ex,sharp corners=southwest]{#3}%
	\ocgbase@oc@emc\ocgbase@open@stack@pop\tpNull}%
\clist_set:Nn\tpOffsets{0pt,0pt}%
\tipshift=0pt%
\setlength\whatsleft{\linegoal}%
\edef\twd{\the\wd\tiptext}%
\ifdim\whatsleft<\dimexpr\twd+\clist_item:Nn\tpOffsets{1}\relax%
	\setlength\tipshift{\whatsleft-\twd-\clist_item:Nn\tpOffsets{1}}\fi%
\raisebox{\heightof{#1}+\the\dp\tiptext+\clist_item:Nn\tpOffsets{2}}[0pt][0pt]{%
	\makebox[0pt][l]{\hspace{\dimexpr\tipshift+\clist_item:Nn\tpOffsets{1}\relax}\usebox{\tiptext}}}%
\stepcounter{tcnt}%
}}% end of \tooltip
\makeatother\catcode`_=8\catcode`:=12
\newsavebox\tiptext\newcounter{tcnt}
\newlength{\whatsleft}\newlength{\tipshift}

\newcommand{\confrep}[2]{\begin{conf}#1\end{conf}\begin{rep}#2\end{rep}}

%\newcommand\CDOT{\cdot}
\newcommand\CDOT{}

\let\sumBig\sum
\begin{conf}
\global\long\def\sum{{\textstyle\sumBig}}% Makes every \sum ∑ small in conference version. Use \sumBig for the original behavior.
\end{conf}
\confrep{\global\long\def\blink#1#2{#1}}{\global\long\def\blink#1#2{\link{#1}{#2}}}

\def\pretitle{Recurrence-Driven~Summations in~Automated~Deduction}
\confrep%Do not put \confrep inside \title because of random errors.
{\title{\pretitle}}
{\title{\pretitle\\(Technical Report)}}


\author{
  Visa Nummelin\inst{1}\orcid{0000-0001-7049-6847}
  \and\\
  Jasmin Blanchette\inst{1,2}\orcid{0000-0002-8367-0936}
  \and\\
  Sander R. Dahmen\inst{1}\orcid{0000-0002-0014-0789}%
}
\institute{
    Vrije Universiteit Amsterdam, Amsterdam, the Netherlands \\
    \email{\{visa.nummelin,j.c.blanchette,s.r.dahmen\}@vu.nl}
  \and
    Ludwig-Maximilians-Universit\"at M\"unchen, Munich,~Germany \\
    \email{jasmin.blanchette@lmu.de}
%  \and
%    Max-Planck-Institut f\"ur Informatik, Saarland Informatics Campus, Saarbr\"ucken,~Germany \\
%    \email{jasmin.blanchette@mpi-inf.mpg.de}
}
\authorrunning{V. Nummelin, J. Blanchette, and S. R. Dahmen}

\spnewtheorem{examplex}[theorem]{Example}{\bfseries}{\rmfamily}
\spnewtheorem{remarkx}[theorem]{Remark}{\bfseries}{\rmfamily}
\spnewtheorem{conventionx}[theorem]{Convention}{\bfseries}{\rmfamily}
\spnewtheorem{definitionx}[theorem]{Definition}{\bfseries}{\rmfamily}
\spnewtheorem{procedurex}[theorem]{Procedure}{\bfseries}{\rmfamily}
\spnewtheorem{lemmax}[theorem]{Lemma}{\bfseries}{\slshape}
\spnewtheorem{theoremx}[theorem]{Theorem}{\bfseries}{\slshape}
\spnewtheorem{corollaryx}[theorem]{Corollary}{\bfseries}{\slshape}
\spnewtheorem*{proofx}{Proof}{\slshape}{\rmfamily}

\DeclareMathOperator{\mgu}{mgu}

\let\oldlabelitemi=\labelitemi
\let\labelitemi=\labelitemii %% CHEAT!
\let\labelitemii=\oldlabelitemi %% CHEAT!

\def\negvthinspace{\kern-0.083333em}
\def\vthinspace{\kern+0.083333em}
\def\vvthinspace{\kern+0.0416667em}
\def\negvvthinspace{\kern-0.0416667em}

% for "bussproofs" package
\EnableBpAbbreviations
\def\ScoreOverhang{1.5pt}
\def\proofSkipAmount{\vskip 0pt}
\def\defaultHypSeparation{\hskip0.75em}

\begin{document}

% Broken on too many PDF viewers.
%\def\SumInf.{\tooltip{\textsc{Summation}}%
%{$\displaystyle\frac{C_{1}\enskip\cdots\enskip C_{l}\quad C\mathrel{\lor}t\not=u}{D\mathrel{\lor}C\mathrel{\lor}\bigvee_{\vec{b}\in B}\{\vec{s}\mapsto\vec{b}\}(t\not=u)}\quad$(page \pageref{sum rule})}%
%}

\def\SumInf.{\textsc{Summation}}

\maketitle
\setcounter{footnote}{0}

\begin{sloppypar}
\begin{abstract}
Many problems in mathematics and computer science involve summations. We present
a procedure that automatically proves equations involving finite summations,
inspired by the theory of holonomic sequences. The procedure is designed to be
interleaved with the activities of a higher-order automatic theorem prover. It
performs an induction and automatically solves the induction step, leaving the
base cases to the theorem prover.\confrep{}{ We show how to integrate the
procedure with superposition, satisfiability modulo theories, and tableaux.}
\end{abstract}
\end{sloppypar}

\section{Introduction}
\label{sec:introduction}

Finite summations---that is, summations $\sum_{i=m}^{n} t_i$ over finitely many
terms $t_i$---are ubiquitous in mathematics and computer science, but
they are poorly supported by automatic theorem provers. One reason is that
summations are higher-order, whereas most theorem provers are first-order.
%In addition, higher-order provers are generally weak at induction, which is vital
%for reasoning about summations.

In recent years, we have seen the rise of higher-order provers%
\confrep{
\cite{barbosa-et-al-2019,sb-21-leo3,br-20-vampire-ho-combs,vukmirovic-et-al-2022-hot,vukmirovic-et-al-2023}%
}{, such as cvc5
\cite{barbosa-et-al-2019},
E \cite{vukmirovic-et-al-2023},
Leo-III \cite{sb-21-leo3}, Vampire \cite{br-20-vampire-ho-combs}, veriT
\cite{barbosa-et-al-2019}, and Zipperposition \cite{vukmirovic-et-al-2022-hot}%
}. With these provers,
\confrep{}{a summation }$\sum_{i=m}^n t_i$ can be represented as %the $\lambda$-term
$\cst{sum}\; m\; n\; (\lambda i.\> t_i)$; the traditional $\sum$ syntax can be seen as
syntactic sugar\confrep{}{ for a $\lambda$-term}. But despite the use of heuristics
\cite[Sect.~4]{vukmirovic-et-al-2022-hot}, higher-order provers are ill-equipped
to reason inductively. A simple problem such as % proving the equation
$\sum_{i=0}^\cst{n} i = \cst{n} \CDOT (\cst{n} + 1)/2$ is a formidable challenge for them, even if
we include axioms for $+$, $\cdot\kern.04ex$, $/$, and $\sum$ together
with an induction principle.

In this \paper, we introduce a procedure for proving such equations in a
higher-order prover. The procedure is triggered by a proof goal of the form $k
\CDOT \sum s + t = u$, possibly with some conditions
(Sect.~\ref{sec:inference-rules}). In a refutational prover, the equation would
be negated, as $k \CDOT \sum s + t \not= u$, and would correspond to the negated
conjecture, a problem axiom, or some clause derived by the prover.

Our procedure translates facts about summations to linear recurrences. These
recurrences have almost the same form as multivariate holonomic sequences
\cite{basicholo}, which, while not being a prerequisite for reading this paper, strongly inspired our work. Each recurrence is
associated with a multivariate sequence---a sequence with one or more indices.
In this \paper, the word ``sequence'' generally means ``multivariate sequence.''

The procedure has three steps.

\begin{enumerate}
\item \emph{Initialization} (Sect.~\ref{sec:initialization}):
Heuristically choose terms in the goal to generalize and perform induction on.
Among the problem axioms, select those of a suitable form as initial recurrences
for the procedure.

\smallskip

\item \emph{Propagation} (Sect.~\ref{sec:propagation}):
From the initial recurrences, compute recurrences corresponding to the goal. For
$+$, $\cdot\kern.04ex$, and $\sum$ expressions occurring in the goal, recurrences are
computed from the recurrences of their direct subexpressions.

\smallskip

\item \emph{Induction} (Sect.~\ref{sec:induction}):
If the final recurrences for the goal involve only the goal and no other
sequences, use them for induction. If they make the difference of successive values of $k \CDOT \sum s +
t - u$ constantly 0, this establishes the induction step. Then reduce the goal
to a set of base cases and give these to the prover.
\end{enumerate}
%
Propagation and induction apply holonomic-style techniques almost as a black box.
Initialization connects them to the overall proof search.

For example, to prove $\sum_{i=0}^\cst{n} i = \cst{n} \CDOT (\cst{n} + 1)/2$, the procedure would transform the
equation into recurrences and find out that the difference $\sum_{i=0}^\cst{n} i - \cst{n}
\CDOT (\cst{n} + 1)/2$ remains constant as $\cst{n}$ increases, thereby establishing the
induction step. If that difference is constantly 0, we get
$\sum_{i=0}^\cst{n} i = \cst{n} \CDOT (\cst{n} + 1)/2$; in general, it suffices to prove a number of base
cases, which are left to the prover.
This example is very simple, but the procedure scales up to more sophisticated
problems (Sect.~\ref{sec:examples}). An implementation is under way in the
Zipperposition prover \cite{vukmirovic-et-al-2022-hot}.

The procedure treats $\sum$ as an interpreted (built-in) symbol. The summation
expression evaluates to a value in a commutative group, or a ring if
ring multiplication is present. The commutative group or ring gives us $+$, $\cdot\kern.04ex$, %% TYPESETTING: hack
and $-$.
%, and $0$; a ring also gives us $1$.
These are also interpreted, as are numerals.
%A key property is that integers can multiply elements of a commutative group, which is one reason why indices must be integers.
Integers, including indices, can multiply group elements.
Based on the interpretation, we use the forms $t=u$ and $t-u=0$ interchangeably.

\looseness=-1
Compared with Wilf--Zeilberger pairs \cite{WZcert} and other methods
(Sect.~\ref{sec:related-work}), the main benefit of our procedure is that it
goes beyond holonomic sequences and supports both uninterpreted functions and
an infinite number of base cases. Our procedure is widely applicable and may
help prove
not only difficult summations in a restrictive form but also
easier summations in a more general form, which is useful in a general-purpose theorem prover.
At the heart of our work is the novel combination of techniques from superposition and
holonomic sequences, which is visible both in the prover integration
(Sect.~\ref{sec:inference-rule}) and in the computation of so-called
excess terms (Sect.~\ref{sec:propagation}).
\begin{conf}%
We refer to our technical report~\cite{our-report} for more details.
%including proofs of our claims.
\end{conf}%

\begin{conf}
\section{Inference Rule}
\label{sec:inference-rule}
\label{sec:inference-rules}

% SMT and tableaux

Our procedure can be integrated into a theorem prover, where it takes the form
of an inference rule that complements the prover's existing rules. Our technical
report discusses an integration with satisfiability modulo theories (SMT) and
tableaux; here, we present a rule for superposition:
%
\[\label{sum rule}
\AXC{$C_1$\enskip$\cdots$\enskip$C_l$}
  \AXC{\strut $C' \mathrel\lor t[\vec s\,] \not= 0$}
\RL{\textsc{Summation}}
\BIC{\strut $D \mathrel\lor C' \mathrel\lor
  \bigvee_{\vec b \in B} t[\vec b\,] \not= 0$}
\DP
\]
%
These side conditions apply:
%
\begin{itemize}
\item $t[\vec s\,]$ is an expression that can be brought into the general form
  $k \CDOT \sum_{i=m}^n t' + t''$;

\item the procedure selects, generalizes, and performs an induction on the subterms $\vec s$ of $t$
  (Sect.\ \ref{sec:term-generalization});

\pagebreak[2]

\item the procedure succeeds at proving the induction step based on
  initial recurrences derived from $C_1,\dots,C_l$
  (Sect.~\ref{sec:choice-of-initial-recurrences}) and their propagation
  (Sect.~\ref{sec:propagation});

\item the procedure identifies $B$ as the finite set of base cases of the
  induction, where each case is a vector $\vec b$ of terms\confrep{}{ (not necessarily
  numerals)} of the same length as $\vec s$ (Sect.~\ref{sec:induction});
  and

\item the subclause $D$ captures potential conditions determined by the
  procedure.
\end{itemize}
The intuition behind the rule is that the conclusion
should be easier to refute than the rightmost premise.
As for the premises $C_1,\dots,C_l$, they can
contain useful information about $\vec s$, often about bounds.

\end{conf}
\begin{rep}%
\section{Inference Rules}
\label{sec:inference-rule}
\label{sec:inference-rules}

Our procedure can be integrated into \confrep{a theorem prover}{various types of theorem provers}, where it takes the
form of an inference rule that complements the prover's existing rules. We
present such a rule for provers based on the superposition calculus and briefly
discuss a similar integration with two other proof calculi:\
satisfiability modulo theories (SMT) and tableaux.

\maybesubsection{Superposition}
  
Superposition
%%% TODO future: Update the CASC citation "sutcliffe-desharnais-2022-casc".
%
is a calculus for classical first-order logic. It reasons
about formulas in conjunctive normal form, or clauses, that contain the
equality predicate. It
\confrep{}{can be viewed as a generalization of the Knuth--Bendix
completion procedure \cite{knuth-bendix-1970} to clausal first-order logic.\par
Superposition is highly successful; the first-order
division of the CADE ATP Systems Competition (CASC)
\cite{sutcliffe-desharnais-2022-casc} has been dominated
by a superposition prover since 2002. The calculus }%
has been
extended to higher-order logic, as combinatory superposition
\cite{bhayat-reger-2020-combsup} and $\lambda$-super\-position
\cite{vukmirovic-et-al-2022-hot}. Zipperposition, based on
$\lambda$-super\-position, has won in the higher-order division of CASC in 2020,
2021, and 2022.

Superposition is a refutational calculus: Starting from the negation of the
conjecture taken as an axiom, it tries to derive a contradiction---the empty,
false clause $\bot$. This is achieved by saturation:\
systematically deriving consequences of existing clauses, aiming to eventually
derive $\bot$.

The calculus consists of inference rules that generate new clauses based on the
presence of suitable premises in the clause set. The premises of a rule are
shown above a horizontal bar; the derived conclusion is shown below the bar. We
extend superposition with a rule that interfaces with our summation procedure:
%
\[\label{sum rule}
\AXC{$C_1$\enskip$\cdots$\enskip$C_l$}
  \AXC{\strut $C' \mathrel\lor t[\vec s\,] \not= 0$}
\RL{\textsc{Summation}}
\BIC{\strut $D \mathrel\lor C' \mathrel\lor
  \bigvee_{\vec b \in B} t[\vec b\,] \not= 0$}
\DP
\]
%
\confrep{}{(By commutativity of $\lor$ and $=$, the rule also applies to a rightmost
premise of the form $t'[\vec s\,] \not= t[\vec s\,] \mathrel\lor C'$, for example.)}
The following side conditions apply:
%
\begin{itemize}
\item $t[\vec s\,]$ is an expression that can be brought into the general form
  $k \CDOT \sum_{i=m}^n t' + t''$ using the group properties
  (e.g., $t[\vec s\,]$ could be $3 - \smash{\sum_{i=0}^n n^i}$), or using the ring properties if $t[\vec s\,]$ is known to be in a ring;

\item the procedure selects, generalizes and performs an induction on the subterms $\vec s$ of $t[\vec s\,]$
  (Sect.\ \ref{sec:term-generalization});

\item the procedure succeeds at proving the induction step based on
  initial recurrences derived from the premises $C_1,\dots,C_l$
  (Sect.~\ref{sec:choice-of-initial-recurrences}) and propagation of these recurrences
  (Sect.~\ref{sec:propagation});

\item the procedure identifies $B$ as the finite set of base cases of the
  induction, where each case is a vector $\vec b$ of terms\confrep{}{ (not necessarily
  numerals)} of the same length as $\vec s$ (Sect.~\ref{sec:induction});
  and

\item the subclause $D$ captures potential conditions
  determined by the procedure.
\end{itemize}
%
\confrep{}{It can also be useful to make the rule less prolific by requiring
that $t[\vec s\,] \not= 0$ is eligible for superposition inferences, a notion that is
defined in the standard superposition calculus.}
In the rule's conclusion, the notation $t[\vec b\,]$
stands for the term $t[\vec s\,]$
in which the distinguished occurrence of each subterm $s_i$, where $s_i$ is among the
components of $\vec s$, is replaced by the corresponding term
$b_i$ from $\vec b$.
%
For example,
if $t[u_1, u_2] = \cst{g}\;u_1\;u_2$,
$\vec s = (\cst{f}\;\cst{a}{,}\; \cst{a})$,
and $\vec b = (0, 1)$,
then
generalization would transform
$t[\cst{f}\;\cst{a}, \cst{a}] = \cst{g}\;(\cst{f}\;\cst{a})\;\cst{a}$
into
$t[0, 1] = \cst{g}\;0\;1$.

The intuition behind the rule is that the conclusion, which is only about a
finite set of base cases, should be easier to refute than the rightmost premise.
Sometimes the set $B$ of base cases might even be empty, \confrep{if}{meaning that} the
procedure needed no induction. As for the premises $C_1,\dots,C_l$, they can
contain useful information about $\vec s$, often about bounds.

\begin{examplex}
Consider the goal $\forall n.\; n \ge 0 \medrightarrow \sum_{i=0}^n i = n \CDOT
(n + 1)/2$. Clausification produces two clauses:\ $\cst{n} \ge 0$ and
$\sum_{i=0}^\cst{n} i \not= \cst{n} \CDOT (\cst{n} + 1)/2$ where
$\cst{n}$ is a Skolem constant. The following inference applies our procedure to
solve the induction step of the second premise:
\[
\AXC{$\cst{n} \ge 0$}
  \AXC{\strut $\sum_{i=0}^\cst{n} i \not= \cst{n} \CDOT (\cst{n} + 1)/2$}
\RL{\sc{Summation}}
\BIC{$\sum_{i=0}^0 i \not= 0(0+1)/2 \vee \sum_{i=0}^1 i \not= 1(1+1)/2 \vee \sum_{i=0}^2 i \not= 2(2+1)/2$}
\DP
\]
%
The induction is on the subterm $\cst{n}$, which is generalized to a variable.
The procedure generates three base
cases, for $\cst{n} \in \{0, 1, 2\}$. These are easy to reduce to falsity using
superposition's simplification machinery and basic equations that expand
finite sums. Built-in arithmetic procedures%
\confrep{ \cite{dragan-et-al-2013,cruanes-2015}}{, as found for example in Vampire
\cite{dragan-et-al-2013} and Zipperposition \cite{cruanes-2015},}
can easily reason about the arithmetic expressions. At the end, the prover
derives the empty clause~$\bot$.
\end{examplex}

\oursubsection{Other Proof Calculi}

Besides superposition, our procedure can be integrated into other proof calculi.
We briefly sketch integrations into higher-order versions of SMT and tableaux.

SMT solvers \cite{barbosa-et-al-2019} combine a SAT solver, which decides
propositional logic, and theory solvers. One theory solver is the congruence
closure, which decides the theory of equality over uninterpreted functions;
for example, from $\cst{a} = \cst{b}$, it infers that
$\cst{f}\;\cst{a} = \cst{f}\;\cst{b}$.
The congruence closure maintains a partition of terms in equivalence classes. In
addition, it keeps track of disequations.

When the congruence closure becomes aware of a disequation $t[\vec s\,] \not= 0$
where $t[\vec s\,]$ can be brought into the general form $k \CDOT \sum_{i=m}^n
t'+t''$, the envisioned integration would invoke
our procedure and, on success, add the implication
\[
t[\vec s\,] \not= 0 \medrightarrow D \mathrel\lor
\bigvee_{\vec b \in B} t[\vec b\,] \not= 0
\]
to the set of clauses to refute, where $D$, $B$, and $\vec s$ are as for
superposition. This implication can safely be added regardless of the current
SAT model, because it is a tautology in the theory of summations. Even though it
is not a decision procedure, in this respect the integration would behave like a
theory solver. The procedure could use any initial recurrences derived
from clauses $C_1, \dots, C_l$ found in the current set of clauses.

As for tableaux \cite{brown-smolka-2010-tableaux}, an integration would work
as follows. Whenever a clause $C' \mathrel\lor t[\vec s\,] \not= 0$ emerges in
a leaf node of the proof tree, where $t[\vec s\,]$ can be
brought into the form $k \CDOT \sum_{i=m}^n t' + t''$,
the integration would invoke our procedure and, on success, add the clause
$D \mathrel\lor C' \mathrel\lor
  \bigvee_{\vec b \in B} t[\vec b\,] \not= 0$
next to $C' \mathrel\lor t[\vec s\,] \not= 0$ in the current leaf, where $D$, $B$, and
$\vec s$ are as above. The procedure could use any initial recurrences derived
from clauses $C_1, \dots, C_l$ found in the branch containing the current leaf.
\end{rep}%

{

\section{Initialization}\label{sec:initialization}

% We assume that the base calculus works with generic logical clauses.
The first
step of our procedure is to
recognize the %special
structure of recurrences.
Variables on which we can perform induction
appear as Skolem constants in the negated goal.
Further opportunities for induction can be created by generalizing complex terms.
Also as part of this step, we must choose which terms represent
(multivariate) 
sequences and which clauses represent their recurrences.

\oursubsection{Theory Detection}
\label{Backtheory}

We require the necessary theory of summation to be predefined\confrep{}{, either as a
specially tagged subset of the input or as a theory that is hard-coded in the
prover}.
Specifically, this refers to the inductive theory of integers,
axioms for commutative groups (including multiplication by integers),
and the definition of summation from 0 by
$\sum_{n=0}^{-1}f_{n}=0$ and
$\sum_{n=0}^{m+1}f_{n}=\sum_{n=0}^{m}f_{n}+f_{m+1}$
even for negative $m\in\mathbb{Z}$.
Other finite intervals than $[0,m]$ %CADE review addition
are expressible as differences\confrep{}{:
$\sum_{n=k}^{m}f_{n}=\sum_{n=0}^{m}f_{n}-\sum_{n=0}^{k-1}f_{n}$}.

Ring multiplication may be absent, so we do not take it as predefined.
Instead, we search candidate binary operators
from the negated goal.\confrep{}{ Often multiplication candidates would have the
form $\cst{f}\;l\;r$ where $l$ and $r$ are left and right operands, respectively,
but we generally allow the form $\cst{f}\;\tuple a\;l\;\smash{\tuple b}\;r\;\tuple c$
with a function symbol $\cst{f}$ and variable-free term tuples
$\tuple a,\smash{\tuple b},\tuple c$.
This form is motivated by the encoding of types as parameters (e.g.,
$\cst{mul}\;\cst{real}\;l\;r$) and lifting of operations (e.g.,
$\makeop{lift}\;\cst{mul}_{\cst{real}}\;l\;r$) to quotients,
products, etc.} For each candidate, we can try to prove left and right distributivity
by syntactically looking for that axiom or by running another instance of the
prover. Distributivity is the only necessary property to apply the procedure, but associativity, commutativity, and the unit element can also be used in simplifications.

\oursubsection{Term Generalization}
\label{sec:term-generalization}

Term generalization transforms Skolem constants or complex terms into
variables and then performs an induction on the variables.
We propose a straightforward heuristic: For each nonnumeral subterm $s$ of type $\mathbb{Z}$ occurring in the negated goal, generalize $s$ if $s$ stays variable-free even after recursively
applying this heuristic on the proper subterms of $s$ itself.
For example,
in the following variable-free integer terms, the underlined
subterms would be generalized:
\confrep{%
$\underline{\vphantom{()}\cst{a}}$,
$123$,
$\underline{\vphantom{()}\cst{f}\;0\;2}$,
$2\cst{f}\;(\underline{\cst{g}\;(-1)})\;(-3\underline{\vphantom{()}\cst{a}})$,
$\cst{f}\;1\;(\cst{g}\;(\underline{\vphantom{()}\cst{a}}+1))$,
$\cst{f}\;(\cst{g}\;\underline{\vphantom{()}\cst{a}})\;7\underline{\vphantom{()}\cst{a}}$.
\vphantom{$_{{}_{()_{()}}}$} %% TYPESETTING: hack
\par
}{%
\begin{align*}
 &\underline{\vphantom{()}\cst{a}}
&&123
&&\underline{\vphantom{()}\cst{f}\;0\;2}
&&2\cst{f}\;(\underline{\cst{g}\;(-1)})\;(-3\underline{\vphantom{()}\cst{a}})
&&\cst{f}\;1\;(\cst{g}\;(\underline{\vphantom{()}\cst{a}}+1))
&&\cst{f}\;(\cst{g}\;\underline{\vphantom{()}\cst{a}})\;7\underline{\vphantom{()}\cst{a}}
\end{align*}
}
\noindent\hbox{}\kern\parindent
Let $\tuple s = (s_1,\dots,s_d)$ be the subterms chosen for generalization. Then, based on the negated goal $C'\vee t[\vec s\,]\neq 0$ (as in the \SumInf. rule), generalization sets up the goal 
$\forall\tuple n\in N.\;t[\vec n]=0$
where $N\subseteq\mathbb{Z}^{d}$ collects the bounds of $\tuple s$ (often $N=\mathbb{N}^{d}$).
%We accept conditional proofs of this goal.
We try to prove this goal up to base cases and other mild conditions.

The generalization makes it possible to use induction to prove that the goal sequence term $t[\vec n]$---a function of $\tuple n$---equals zero on $N$. We try
to prove the generalized goal assuming $\neg C'$ and some extra conditions $E$ such as the base cases of the induction. Then, instantiating $\tuple n:=\tuple s$, we conclude $C'\vee\neg E\vee t[\vec s\,]=0$. This, together with the negated goal $C'\vee t[\vec s\,]\neq 0$, implies a conclusion of the form $C'\vee\neg E$ for the \SumInf. rule. Note that $C'$ is not generalized.

\pagebreak[2]

\looseness=-1
The set $N$ embodies knowledge about $\tuple s$ that we find among existing clauses $C_1, \dots, C_l$
and the condition $\neg C'$. The free variables of $\neg C'$ are interpreted as constants, and they can also occur in $\tuple s$.
For example, assume that $\tuple s=\cst f\;s'$ and $\tuple n=n$\confrep{}{ are singletons} and that the generalized goal contains the factorial $n!$. Its recurrence must be in a conditional clause---e.g., $\sulut{m+1}!=\sulut{m+1}m!\vee0\not\leq m$. To use this recurrence for $n!$, we need $n\geq0$, which we can ensure using $N$ if we find a bounding clause $\cst f\;s'\geq0$ or its generalization such as $\cst f\;m\geq0$ where $m$ is a free variable. The more we know about $\tuple s$, the more recurrences we can get. At the same time, $N$ must allow induction, so we keep it convex by considering only coordinatewise bounds of~$\tuple s$.

{\oursubsection{Form of sequence terms}

Sequence terms are terms of the underlying higher-order logic that our procedure can work with. From their structure, we distinguish (pointwise) addition and multiplication, summation, and affine substitution. This gives a first-order grammar to express the sequence terms.
\begin{definitionx}
\label{def:sequence-terms}
%\looseness=-1
\emph{Sequence terms} on a ring $A$ are inductively defined as follows. The logic's terms of type $A$ with distinguished integer variables $\tuple n$ are sequence terms. If $f_{\tuple n}$ and $g_{\tuple n}$ are sequence terms with $d$ variables $\tuple n$, then so are $f_{\tuple n}+g_{\tuple n}$, $f_{\tuple n}\cdot g_{\tuple n}$, $\sum_{i=0}^{\tuple c\bullet\tuple n+a}f_{\{n_j \mapsto i\}\tuple n}$, and $\sigma f_{\tuple n} = f_{\sigma \tuple n}$ where $\tuple c$ is a vector, $a$ is an integer, $\tuple c\bullet \tuple n = c_1n_1 + \cdots + c_dn_d$,
and $\sigma$ is an affine substitution (meaning $\sigma\tuple m=q\tuple m+\smash{\tuple b}$ for a matrix $q$ and a vector $\smash{\tuple b}$);
$a$, the entries of $\tuple c$, and the entries of $\sigma$ (meaning the entries of $q$ and $\tuple b$) must be numerals.
\end{definitionx}

\begin{remarkx}
In Definition~\ref{def:sequence-terms} and in the sequel, a commutative group can be used instead of a ring if ring multiplication is absent. In this case,
all formulas involving ring multiplication (e.g., $f_{\tuple n}\cdot g_{\tuple n}$) should be ignored.
\end{remarkx}

We view sequence terms as functions $\smash{\mathbb{Z}^{d}}\to A$\confrep{}{, so in particular natural number indices must be extended. For example, the factorial $n!$ for $n\in\mathbb{N}$ can be extended as 0 onto the negative integers by replacing its
recurrence $n!-n\sulut{n{-}1}!=0$ with $n\cdot n!-n^{2}\sulut{n{-}1}!=0$ and adding the initial value $(-1)!=0$.
This multiplication by $n$ is necessary to make a cut at 0 and avoid the contradiction $1=0!=0\cdot\sulut{-1}!=0$}. We then write the sequence terms from the definition compactly as $f+g$, $f\cdot g$, $\sum_{j}^{a}f$, and $\sigma f$, and call $a=\tuple c\bullet\tuple n+d$ an affine variable sum. Moreover, since $\cdot\kern.04ex$, $\sum_{j}^{a}$, and $\sigma$ all distribute over $+$, we can write any sequence term as $c_{1}f^{1}+\cdots+c_{k}f^{k}$ where the coefficients $c_{j}$ are numerals and the sequence terms $f^{j}$ are distinct and
do not contain $+$.
 Finally, we forbid variable shadowing: $\sum_{n_{j}=0}^{a}$ binds $n_{j}$, and while $\sum_{j}^{a}\sum_{j}^{b}g$ and $\sum_{j}^{n_{j}}g$ and other references to $n_{j}$ outside $\sum_{j}^{a}$ are syntactically valid, we avoid such forms by renaming them during encoding and never reintroducing them.
}

\oursubsection{Choice of Initial Recurrences}
\label{sec:choice-of-initial-recurrences}

Semantically, the recurrences we look for are
{multivariate} heterogeneous linear
{finite-fixed-step} equations with {polynomial coefficients}. An archetypical example is
\begin{equation}\label{eqn:archetypical}
\sulut{n^{2}+1}f_{n+2,m+1}+mf_{n+1,m}=nmf_{n,m+1}-2h_{n,m}+\sulut{m-n}h_{n,m+1}+1 %.
\pagebreak[2]
\end{equation}
Here, the sequences $f,h,1$ are bivariate, and the sequence indices
are all of the form $n+k$ or $m+k$ for numerals $k \in \mathbb{Z}$, amounting to
finite fixed steps.

The general form is $0=P_{1}g^{1}+\cdots+P_{k}g^{k}=\tuple P\bullet\tuple g$ where $\tuple g=\sulut{g^{1},...,g^{k}}$ is a tuple of sequence terms and $\tuple P$ is a tuple of operator polynomials as defined below. If $k=1$, we have a homogeneous recurrence of $g^{1}$; otherwise, it is heterogeneous.

\begin{definitionx}
\emph{\label{polynomials}Operator polynomials} are a $\mathbb{Z}$-algebra with composition as product (meaning closed under addition, composition, and integer multiplication) spanned by the multiplier and shift operators:
\begin{itemize}
\item The \emph{multiplier} operator $M_{j}$ of index $j$ multiplies a
%(ring- or group-valued)
multivariate sequence $f$ by the variable $n_{j}$ of index $j$:
%%% Ring-valued is also group-valued because rings are groups. So we do not mention ring here.
$\sulut{M_{j}f}_{\tuple n}=n_{j}f_{\tuple n}$.

\item The \emph{shift} operator $S_{j}=\{n_{j}\mapsto n_{j}+1\}$ of index $j$ increments the variable $n_{j}$ of index $j$ of a multivariate sequence $f$ by one: $\sulut{S_{j}f}_{\tuple n}=f_{\{n_{j}\mapsto n_{j}+1\}\tuple n}$.
\end{itemize}
\end{definitionx}

With $d$ index variables, the operator polynomials look like ordinary polynomials $\mathbb Z[M_1,...,M_d,S_1,...,S_d]$, but the composition product is noncommutative since $S_i M_i = M_i S_i + S_i$ for all $i=1, \ldots, d$ (a derivation of which is given in the next section directly above equation~\eqref{eqn:commutation_relations}).
As an example of expressing recurrences in terms of operator polynomials, consider the previous archetypical recurrence~\eqref{eqn:archetypical}.
Taking $n$ as the first and $m$ as the second variable, the recurrence reads
$$((M_1^2+1) S_1^2 S_2 + M_2 S_1 - M_1 M_2 S_2)\cdot f + (2 - (M_2-M_1)S_2)\cdot h + (-1)\cdot1 = 0$$

\begin{remarkx}\label{recurrence as term}
The expression $\tuple P\bullet\tuple g$ identifying a recurrence is itself a sequence term. It suffices to observe that if $f$ is a sequence term, then so are the substitution $S_{j}f$ and the product $M_{j}f=\sulut{\tuple n\mapsto n_{j}}\cdot f$ with the projection sequence term $\tuple n\mapsto n_{j}$.
\begin{rep}%
If we are not in a ring setting, the integer-group product is still a bihomomorphism, which is all that we need in the sequel.
\end{rep}
\end{remarkx}


As sketched in Sect.~\ref{sec:introduction}, we must select some of the problem
axioms as initial recurrences for the procedure. This is accomplished as
follows.
%
Let there be an edge between two axioms
of the form $C \lor s = t$ (where $C$ may be empty)
if they both contain a top-level occurrence of the same sequence $g$, i.e., an occurrence of $g$ that is not nested inside an uninterpreted function symbol.
The axioms then form a
graph. We take as initial recurrences the connected component of the generalized
goal.

By a sequence $g$, we mean the $\cst{f}\;\tuple a$ part of a term of the form
$\cst{f}\;\tuple a\;\tuple n$ where
$\cst{f}$ is an uninterpreted function symbol,
$\tuple a$ is a tuple of variable-free
terms, and $\tuple n$ is a nonempty tuple of integer variables or
affine (i.e., linear term + constant term) combinations of them.
The tuples $\tuple a$ and $\tuple n$ may in general be
interleaved.

In other contexts, an analogous step is known as lemma filtering or premise
selection \cite[Sect.~2]{blanchette-et-al-2016-qed}. Clutter from irrelevant facts
is less of an issue in the context of our procedure because it can use only
linear recurrences. Beyond this, our simple heuristic does nothing to
avoid clutter.

What should we do about conditions such as $C$ in $C\vee\cst{f}\;\tuple a\;\tuple n = t$?
\confrep{}{In an implementation, there would be at least three ways to cope with them: }%
%
\confrep{%
We could forbid them and work only with unit equations such as
  $\cst{f}\;\tuple a\;\tuple n = t$.
We could collect them and put them in the $D$ component of the
  \SumInf. rule's conclusion.
Or we could attempt to prove them when the initial recurrences are selected.
In our ongoing implementation, we chose the first option, but what the best option is remains an open question.
}{
\begin{itemize}
\item We could forbid them and work only with unit equations such as
  $\cst{f}\;\tuple a\;\tuple n = t$.

\smallskip

\item We could collect them and put them in the $D$ component of the
  \SumInf. rule's conclusion.

\smallskip

\item We could attempt to prove them when the initial recurrences are selected.
\end{itemize}
In our ongoing implementation, we chose the first option, but what the best option is remains an open question.
}
}
% 
{


\section{Propagation}\label{sec:propagation}
\emph{Holonomic sequences} can be defined by homogeneous recurrences
with polynomial coefficients
and finitely many base cases. They are closed under the four operations that build sequence terms ($+,\cdot\kern.04ex,\sum_{j}^{a},\sigma$), which especially
makes their equality decidable \cite{basicholo}.
The closure is realized by four procedures to derive recurrences of a sequence term from the recurrences of its immediate subterms, which we call \emph{propagation}. We can propagate independently of the base cases and hence work on nonholonomic sequence terms \cite{close}.
Although we expect the holonomic subcase to be decidable in our setting,
in general 
decidable equality
is lost.
Additionally, unlike in the holonomic setting, we allow heterogeneous recurrences. We will build this into our noncommutative Gröbner basis setup that is used in the propagation procedures.

\oursubsection{Gröbner Bases of Recurrence Operators}

A (generalized) Gröbner basis is a certain well-behaved generating set of a left-ideal of (possibly noncommutative) polynomials. Equivalently, we will view it as a system of polynomial equations\pagebreak[2] that is complete for rewriting.
Given a polynomial equation $P=0$, for every monomial $M$ we get a rewrite rule as follows. Decompose $MP$ as $MP=L+R$ where $L$ is the leading monomial of $MP$
 w.r.t.\ a fixed monomial ordering times its coefficient.
Then $L=-R$ gives rise to a rewrite rule $L\to-R$.
A system of equations is complete for rewriting if every one of its consequences can be proved via rewriting by these rules.

\begin{examplex}
The system $\left\{ ab^{2}=a+b{,}\; a^{2}b=a+1\right\} $ does not prove its consequence $a^{2}=b$ by rewriting.
(We can see that $a^{2}=b$ is a consequence by multiplying the first equation
by $a$ and the second equation by $b$ and then by subtracting the two equations.)
In the other direction, the system's Gröbner basis $\left\{ a^{2}=b{,}\; b^{2}=a+1\right\} $ does give rewrite proofs $\smash{ab^{2}\xrightarrow[\smash{b^{2}=a+1}]{\s}a^{2}+a\xrightarrow[\smash{a^{2}=b}]{\s}b+a}$ and $\smash{a^{2}b\xrightarrow[\smash{a^{2}=b}]{\s}b^{2}\xrightarrow[\smash{b^{2}=a+1}]{\s}a+1}$.
\vphantom{$_{{}_{()_{()}}}$} %% TYPESETTING: hack
\end{examplex}

%\looseness=-1
A theory of Gröbner bases exists for various polynomial algebras \cite{noncommutativeGB}. In our setting, a 
\confrep{}{simple }sufficient requirement is that all indeterminates $X,Y$ commute up to lower-order terms: $XY-YX\in\mathbb{Z}X+\mathbb{Z}Y+\mathbb{Z}$.
The operator polynomials of Definition~\ref{polynomials} fall into this category with
the natural choice of taking all multiplier and
shift operators as indeterminates. Indeed, for any sequence term $f$, we have the noncommutation relations
\[
\sulut{S_{j}M_{j}f}_{\tuple n} = \sulut{S_{j}\sulut{\tuple n\mapsto n_{j}f_{\tuple n}}}_{\tuple n}= \sulut{n_{j}+1}\sulut{S_{j}f}_{\tuple n}=\sulut{\sulut{M_{j}S_{j}+S_{j}}f}_{\tuple n}
\]
and all other pairs of multipliers and shifts commute exactly. That is:}
\begin{equation}\label{eqn:commutation_relations}
S_i M_j = M_j S_i + \delta_{i,j} S_i
\qquad S_i S_j = S_ jS_i
\qquad \quad M_i M_j = M_j M_i
\end{equation}
for all $i$ and~$j$,
where $\delta_{i,j}$ \confrep{}{denotes the Kronecker delta, which }equals $1$ if $i=j$ and $0$ otherwise.
When we consider a formal polynomial algebra (necessary to perform Gröbner basis computations), we will usually mean polynomials with integer coefficients and indeterminates $M_1,M_2,\dotsc,S_1,S_2,\dotsc$ satisfying \eqref{eqn:commutation_relations}.
Exceptionally, when we use propagation to substitution, we will consider compositions of shifts formally as further individual indeterminates, as explained \confrep{above Procedure~\ref{subs. prop.}}{in Sect.~\ref{sec:propagation-to-substitution}}.
Apart from this exceptional setting, we fix a choice of monomials as follows.

\begin{definitionx}\label{def:monomials}
In our setting, a \emph{monomial} is a polynomial of the form $M_{1}^{x_{1}}
\cdots\allowbreak M_{d}^{x_{d}}\allowbreak S_{1}^{y_{1}}\cdots S_{d}^{y_{d}}$ where the exponents $x_{j},y_{j}\in\mathbb{N}$ are numerals.
\end{definitionx}

Due to the (non)commutation relations \eqref{eqn:commutation_relations}, polynomials can be written as sums of
monomials times their integer coefficients.
This makes working with these noncommutative polynomials similar to working with commutative ones.
A major
difference is that monomials are not closed under product,
as illustrated by
$S_1{\cdot}M_1 = M_1 S_1 + S_1$.
This complicates the definition of monomial order below, which in turn defines how to interpret a polynomial equation as a rewrite rule.

\begin{definitionx}
A \emph{monomial order} $\preccurlyeq$ is a well-founded total order on monomials such that for all monomials $A,B,C$, if $A\preccurlyeq B$, then the leading monomial of $CA$ is $\preccurlyeq$-smaller than the leading monomial of $CB$;
here, the \emph{leading monomial} of a nonzero polynomial $P$ means the $\preccurlyeq$-largest
monomial occurring in $P$.
\confrep{}{(Compare this with the term order in superposition, which is well founded and compatible with contexts.)}
\end{definitionx}

Buchberger's algorithm to compute Gröbner bases (also in a noncommutative context) is similar to saturation-based theorem proving.
It repeatedly derives from polynomial equations $P=0$ and $R=0$ new equations $AP-BR=0$ where coefficient--monomial products $A,B$ make the leading monomials of $AP$ and $BR$ cancel.
It suffices to take $A, B$ with smallest total degree and coprime coefficient.
$A$ and $B$ play a similar role to
the most general unifier in superposition.
Since $S_j$ is semantically bijective, we can and always do cancel it, replacing $S_jR=0$ by $R=0$.
\confrep{T}{Unlike many saturation procedures, t}his modified completion into a Gröbner basis always terminates.
The standard termination proof reduces to applying noetherianity of commutative
polynomials
over $\mathbb{Z}$ or Dickson's lemma \cite{noncommutativeGB}.
\begin{rep}
 
The similarity with superposition eases presentation and implementation of Gröbner bases in the context of superposition provers. Hence, we will present propagations as applications of elimination by Gröbner bases. Other methods can be an order of magnitude faster on complicated propagations \cite{MathematicaHolo}; however, we do not know what would work best in practice on average cases in a theorem prover.

\end{rep}

%\looseness=-1
A single operator polynomial $P_{1}$ perfectly encodes a linear homogeneous recurrence $0=P_{1}g$ of a sequence term $g$.
However, we allow any heterogeneous recurrence of the form $0=\tuple P\bullet\tuple f=P_{1}f^{1}+\cdots+P_{k}f^{k}$ where $\tuple f=\sulut{f^{1},\dotsc,f^{k}}$ is an arbitrary tuple of different sequence terms.
We can encode this by a single operator polynomial for the duration of one Gröbner basis computation as follows.
\confrep{L}{Without loss of generality, l}et $\tuple f$ enumerate exactly once all the sequence terms needed to express the current recurrences with the help of operator polynomials.
Let $\tuple f$ depend on $d$ variables.
For each $f^{j}$, we consider a shift $F_{j} := S_{d+j}$ w.r.t.\ a so far unused variable.
Then the operator polynomial $\tuple P\bullet\tuple F$ encodes $0=\tuple P\bullet\tuple f$.

This encoding does not respect the semantics of operator polynomials; to recover
it, we must apply the substitution $\left\{ \tuple F\mapsto\tuple f\right\} $. However, products such as $F_{1}F_{2}$ remain uninterpretable even with ring-valued sequences because the operator product---function composition---is different from multiplication of $f^{j}$'s. Hence, we will simply discard uninterpretable polynomials after the Gröbner basis computation.
Moreover, from now on, we will freely write $f^{j}$ for $F_{j}$.

\begin{definitionx}
Let $X_{1},\dotsc,X_{n}$ be an enumeration of all multiplier and shift indeterminates.
An ($X_{1},\dotsc,X_{k}$)\emph{-elimination order }is a monomial order such that $X_{j}\succ X_{k+1}^{a_{k+1}}\allowbreak{\cdots}\allowbreak X_{n}^{a_{n}}$ for all indices $j\leq k$ and all exponents $a_{k+1},\allowbreak\dotsc,\allowbreak a_n \in \mathbb{N}$.
\end{definitionx}

\confrep{
Our default choice for the order is to compare total degree in $X_1,\allowbreak...,\allowbreak X_k$ and break ties using the total degree reverse
lexicographical order~\cite[Chapter~2~§2]{CoxLittleOShea-15}.
}{
Our default choice for the elimination order is to first compare the total degree over $X_{1},\dotsc,X_{k}$, then compare the total degree over $X_{k+1},\dotsc,X_{n}$, and then break ties by comparing the $n$-tuples of exponents lexicographically,
considering smaller exponents as larger~\cite[Chapter~2~§2]{CoxLittleOShea-15}.
}

\begin{procedurex}\label{elimination}\looseness=-1
\emph{Eliminating} indeterminates $X_{1},\dotsc,X_{k}$ from a finite system of equations $E$ means computing a Gröbner basis $G$ of $E$ w.r.t.\ an ($X_{1},\dotsc,X_{k}$)-elimination order and then discarding all polynomials from $G$ that contain any of $X_{1},\dotsc,X_{k}$ or that are not linear in the indeterminates encoding sequence terms.
(As mentioned above, during the Gröbner basis computation, whenever we derive a
polynomial $S_jR$, we replace it by $R$.)
\end{procedurex}

While in principle any Gröbner basis would suffice for elimination, our
default choice is to compute the reduced Gröbner basis (i.e., the fully simplified one). The nonlinear polynomials can be discarded as soon as they are derived during the Gröbner basis computation instead of only at the end.
\confrep{%
Recurrence equations produced by elimination are logical consequences of the input equations, as we explain in our technical report.}{
\par
Recurrence equations produced by elimination are logical consequences of the input equations.
To see this, observe that $0=\tuple P\bullet\tuple f$ implies $0=A\tuple P\bullet\tuple f$ for every operator monomial $A$ before the encoding. Hence, multiplication by monomials that do not contain $F_{j}$'s has the correct semantics. The monomials of any encoded polynomial $\tuple P\bullet\tuple F$ have the same total degree in the $F_{j}$'s, i.e., $\tuple P\bullet\tuple F$ is homogeneous in the $F_j$'s. Now homogeneity in the $F_{j}$'s is preserved by monomial multiplication and monomial canceling addition. Moreover, these operations never lower the degree of homogeneity (i.e., the total degree in the $F_j$'s). Consequently, Buchberger's algorithm derives only polynomials homogeneous in the $F_{j}$'s, and linear interpretable ones are never derived from the nonlinear uninterpretable ones. This proves that a Gröbner basis $G$ computed by Buchberger's algorithm has the desired property that polynomials linear in the $F_j$'s, when interpreted as equations, are logical consequences of the input equations. Then every other Gröbner basis has this desired property as well because $G$ rewrites their elements to 0 and rewriting preserves homogeneity in the $F_{j}$'s.}

Despite the formally equivalent roles of all sequence terms $f^{i}$ in
the recurrence $0=\tuple P\bullet\tuple f$, we associate with every recurrence a sequence term $f^{j}$.
It is often convenient to write such a recurrence of $f^{j}$ as $P_{j}f^{j}+e=0$ where the \emph{excess terms} $e=\tuple P\bullet\tuple f-P_{j}f^{j}$ contain all sequence terms $f^{i}$ except $f^{j}$.
The choice of $f^{j}$ among $\tuple f$ will be determined by the definition of excess terms (Definition~\ref{excess}). However, this choice remains irrelevant for the individual propagation steps, described below. We adapt these steps from the four closure properties of holonomic sequences by carrying excess terms along.

\oursubsection{Propagation to Addition} \confrep{Let us start with addition
of sequence terms.}{}

\begin{procedurex}
Let $f$ and $g$ be sequence terms, and let $h$ be the formal name of their addition $f+g$. The associated recurrences $F$ of $f$ and $G$ of $g$ are propagated to those of $h$ by eliminating $f$ and $g$ from $F\cup G\cup\left\{ h=f+g\right\} $.
(By Procedure~\ref{elimination}, this involves computing a Gröbner basis for these equations and then discarding the equations containing $f$ or $g$
as well as the corresponding nonlinear terms.)
\end{procedurex}

Actually, the same propagation technique works if $f+g$ is replaced by any expression in the general recurrence format $\tuple P\bullet\tuple l$ (a dot product of operator polynomials $\tuple P$ and sequence terms $\tuple l$).
The key is that the defining equation $h=\tuple P\bullet\tuple l$ is again a linear recurrence. Such propagations could also be done by iterating more primitive propagations.

\begin{examplex}
\label{indefinite sum ex.}\looseness=-1 Consider the goal $\sum_{j=0}^{n}a_{j}=g_{n}+a_{0}$ given $g_{0}=0$ and $g_{n+2}=g_{n}+a_{n+1}+a_{n+2}$ for all $n\in\mathbb{N}$. The defining recurrence of $g$ can be written using the operator polynomials as $S_{1}^{2}g=g+S_{1}a+S_{1}^{2}a$. The defining recurrence of the sum $f_{n}:=\sum_{j=0}^{n}a_{j}$ is $S_{1}f=f+S_{1}a$. We must prove that $h_{n}:=g_{n}+a_{0}-f_{n}$ is 0. To achieve this, we propagate recurrences to $h$ using the elimination procedure described above
(Procedure~\ref{elimination}) and the total-degree-based $(f, g)$-elimination order with
$f\prec g$. Leading monomials are shown in bold:

\global\long\def\isZero{{\color{gray}\vphantom{\frac{\int}{1}}0={}}}%
\[
\back 6\begin{array}{lll}
 & \isZero\boldsymbol{S_{1}^{2}g}-g-S_{1}a-S_{1}^{2}a & \mathrlap{\quad\text{recurrence of }g}\\
-S_{1}^{2}\quad\s\s & \isZero\boldsymbol{g}+a_{0}-f-h & \mathrlap{\quad\text{definition of }h}\\
\hline  & \isZero{-}g-S_{1}a-S_{1}^{2}a-a_{0}+\boldsymbol{S_{1}^{2}f}+S_{1}^{2}h\\
-S_{1} & \isZero\boldsymbol{S_{1}f}-f-S_{1}a & \mathrlap{\quad\text{recurrence of }f}\\
\hline  & \isZero{-}g-S_{1}a-a_{0}+S_{1}^{2}h+\boldsymbol{S_{1}f}\\
- & \isZero\boldsymbol{S_{1}f}-f-S_{1}a & \mathrlap{\quad\text{recurrence of }f}\\
\hline  & \isZero{-}\boldsymbol{g}-a_{0}+S_{1}^{2}h+f\\
+ & \isZero\boldsymbol{g}+a_{0}-f-h & \mathrlap{\quad\text{definition of }h}\\
\hline  & \isZero\boldsymbol{S_{1}^{2}h}-h
\end{array}
\]
In this example, $h_{n+2}-h_{n}=0$ is the only recurrence that does not contain $f$ and $g$, so we discard the rest of the Gröbner basis calculation. Since $h_{n+2}-h_{n}=0$ contains only the sequence $h$, we can use it to prove the induction step (of size 2) of a proof of $\forall n.\s h_{n}=0$. We are then left with the two base cases $h_{0}=0$ and $h_{1}=0$, which the \SumInf. inference would include in its conclusion without auxiliary symbols ($f$ and $h$) as
$\sum_{j=0}^{0}a_{j}\neq g_{0}+a_{0}\vee\sum_{j=0}^{1}a_{j}\neq g_{1}+a_{0}$.
\end{examplex}

\oursubsection{Propagation to Substitution}
\label{sec:propagation-to-substitution}

\global\long\def\compShift{\mathbb{S}}%
 Consider a numeral matrix $a=\left[a_{kj}\right]_{kj}\in\mathbb{Z}^{d\times \smash{D}}$ and a vector $\smash{\tuple b}\in\mathbb{Z}^{d}$.
They characterize an affine substitution $\sigma=\left\{ \tuple n\mapsto a\tuple n+\smash{\tuple b}\right\} \allowbreak =\{n_{k}\mapsto\sum_{j=1}^{\smash{D}}a_{kj}n_{j}+b_{k}$ $|$ $1\leq k\leq d\}$.
As an operator on sequences, $\sigma$ performs an affine change of variables: $\sulut{\sigma f}_{\tuple n}=f_{a\tuple n+\smash{\tuple b}}$.\confrep{}{ We
restrict our substitutions to affine ones to remain within the propagation
framework.}

Clearly, any recurrence $Pf=0$ of $f$ implies $\sigma Pf=0$.
Moreover, if $\sigma P=P'\sigma$, then $P'\sigma f=0$ gives a recurrence of $\sigma f$.
Finding such \confrep{a}{an operator polynomial} $P'$ for a general $P$ can be reduced to
finding an operator polynomial $P'_X$ satisfying $\sigma X=P'_X\sigma$ for every
indeterminant~$X$.
This amounts to pushing all indeterminates $X$ leftwards.
\confrep{}{The relevant formula is \[
P=\sum_{k=1}^{T}c_{k}\sulut{\prod_{j=1}^{t_{k}}X_{kj}}f_{k}\implies P'=\sum_{k=1}^{T}c_{k}\sulut{\prod_{j=1}^{t_{k}}P'_{X_{kj}}}f_{k}
\]}%
For multipliers, we have $\sigma (M_1,\dotsc,M_d)=\sulut{a(M_1,\allowbreak\dotsc,\allowbreak M_D)+\smash{\tuple b}}\sigma$.
In contrast, shifts are easily pushed only rightwards---namely,
$S_{j}\sigma=\sigma S_{1}^{a_{1j}}\cdots S_{d}^{a_{dj}}$.
\confrep{}{This holds because, using the notation $g|\tuple m=g_{\tuple m}$, we have
\begin{align*}
S_{j}\sigma f|\tuple n&=\sigma f|\left\{ n_{j}\mapsto n_{j}+1\right\} \tuple n=f|\sulut{a\left\{ n_{j}\mapsto n_{j}+1\right\} \tuple n+\tuple b}=\\&=f|\sulut{\sulut{a\tuple n}_{k}+a_{kj}+\tuple b_{k}}_{k=1}^{d}=f|\sulut{\sulut{a\tuple n+\tuple b}_{k}+a_{kj}}_{k=1}^{d}=\\&=S_{1}^{a_{1j}}\cdots S_{d}^{a_{dj}}f|\sulut{a\tuple n+\tuple b}=\sigma S_{1}^{a_{1j}}\cdots S_{d}^{a_{dj}}f|\tuple n
\end{align*}%
}%
Consequently, the recurrences of $f$ must be first expressed in terms of the composite shifts $\compShift_{j}:=S_{1}^{a_{1j}}\cdots S_{d}^{a_{dj}}$.
As operators, these satisfy the (non)commuta\-tion relations
%
\begin{equation}\label{eqn:comp_shift_relations}
\compShift_{j}M_{k}=\sulut{M_{k}+a_{kj}}\compShift_{j} \qquad \compShift_i \compShift_j = \compShift_j \compShift_i \qquad \compShift_i S_j=S_j \compShift_i
\end{equation}
This makes the $\compShift_{j}$'s suitable as indeterminates in Gröbner basis computations.

Accordingly, for propagation to substitution, we enlarge our formal polynomial algebra to also contain the indeterminates $\compShift_1,\compShift_2,\ldots$ satisfying the relations~\eqref{eqn:comp_shift_relations}, while also keeping~\eqref{eqn:commutation_relations}.
We note that, \relax{as operators}, the indeterminates further satisfy (essentially by definition) the relations
\begin{equation}
\label{eqn:defining_relation_comp_shift}\confrep{\textstyle}{}
\compShift_{j}\prod_{k:\:a_{kj}<0}S_{k}^{\left|a_{kj}\right|}=\prod_{k:\:a_{kj}>0}S_{k}^{a_{kj}}\quad\text{for }j\in\left\{ 1,\dotsc,D\right\}
\end{equation}
\confrep{We add these new relations}{While we could have defined our polynomial algebra to incorporate these relations as well, we chose to \emph{not} do this, thereby creating a distinction between the semantic operators and the syntactic polynomial algebra. Instead, we add these relations}
to the system of recurrence equations of which we compute the Gröbner basis.
Finally, we extend our notion of \emph{monomial} from Definition~\ref{def:monomials} to mean any polynomial of the form $M_{1}^{x_{1}}\cdots M_{d}^{x_{d}}S_{1}^{y_{1}}\cdots S_{d}^{y_{d}}\compShift_1^{z_1}\cdots \compShift_{D}^{z_{D}}$ where the exponents $x_{j},y_{j},z_j \in \mathbb{N}$ are numerals.

\begin{procedurex}
\label{subs. prop.}Recurrences of a sequence term $f$ are propagated to its affine substitution $\sulut{\sigma f}_{\tuple n}=f_{a\tuple n+\smash{\tuple b}}$ as follows\confrep{}{, using the extended polynomial algebra described above}.
Eliminate each $S_{k}$ from the system of polynomial equations containing both the recurrences of $f$ and the relations~\eqref{eqn:defining_relation_comp_shift}.
Every resulting recurrence $P\sulut{\tuple M,\tuple{\compShift}}f+e=0$ implies a recurrence $P\sulut{a\tuple M+\smash{\tuple b},\tuple S}\sigma f+\sigma e=0$ of $\sigma f$ where we have collected the indeterminates into vectors and where $e$ are excess terms that do not contain $f$.
\end{procedurex}

\begin{rep}
All shifts in $\sigma e$, including composite ones, are interpreted as substitutions.
%The simplification $\sigma P\sulut{\tuple M,\tuple{\compShift}}=P\sulut{a\tuple M+\smash{\tuple b},\tuple S}\sigma$ is applied when possible also in $\sigma e$ by the rewrite rules in Sect.~\ref{Iteration on excess}.
\end{rep}

\begin{examplex}
\looseness=-1
\label{Fibonacci1}Consider \confrep{}{the formula }${%\displaystyle
\sum_{n_1=0}^{n_2}\binom{n_1}{n_2{-}n_1}=F_{n_2+1}}$ where the Fibonacci numbers are defined by $F_{1}=F_{2}=1$ and $\sulut{S_{1}^{2}-S_{1}-1}F=0$.
For the binomial coefficient $
\binom{\cdot}{\cdot}_{n_1,n_2} =
\binom{n_{1}}{n_{2}}=\frac{n_{1}!}{n_{2}!\sulut{n_{1}-n_{2}}!}$, the recurrence from Pascal's triangle reads \confrep{}{in variable-free notation }as $\sulut{S_{1}S_{2}-S_{2}-1}{\textstyle \binom{\cdot}{\cdot}}=0$ and extends $\binom{n_{1}}{n_{2}}$ from $0\leq n_{2}\leq n_{1}$ to all
\confrep{$n_2 \in \mathbb{Z}$ and $n_1 \in \mathbb{N}$}{integers $n_{2}$ and natural numbers $n_1$}.
Moreover, we have $\binom{n_{1}}{n_{2}}=\frac{n_{1}}{n_{2}}\binom{n_{1}-1}{n_{2}-1}$\confrep{---i.e.,}{ or equivalently} $\sulut{\sulut{M_{2}+1}S_{1}S_{2}-M_{1}-1}{\textstyle \binom{\cdot}{\cdot}}=0$.
\confrep{}{(These recurrences could be propagated from the recurrence of the factorial, except that our procedure cannot handle the domain extension.) }%
We want to propagate these recurrences to the substitution $\sigma=\{ n_{1}\mapsto n_{1}{,}\allowbreak\; n_{2}\mapsto n_{2}-n_{1}\} $.
We have $S_{1}\sigma=\sigma S_{1}S_{2}^{-1}$ and $S_{2}\sigma=\sigma S_{2}$.
So we introduce for $S_{1}S_{2}^{-1}$ and $S_{2}$ the \confrep{}{new }indeterminates $\compShift_{1}$ and $\compShift_{2}$ whose characterizing recurrences~\eqref{eqn:defining_relation_comp_shift} read
\begin{align*}
\sulut{\compShift_{1}S_{2}-S_{1}}{\textstyle \binom{\cdot}{\cdot}}&=0\quad\text{(i)}
&
\sulut{\compShift_{2}-S_{2}}{\textstyle \binom{\cdot}{\cdot}}&=0\quad\text{(ii)}
\end{align*}
Next, we eliminate $S_{1},S_{2}$ in favor of $\compShift_{1},\compShift_{2}$. Here, (ii) immediately rewrites every $S_{2}$ to $\compShift_{2}$ and then (i) becomes $\sulut{-S_{1}+\compShift_{1}\compShift_{2}}{\textstyle \binom{\cdot}{\cdot}}=0$, which rewrites every $S_{1}$. The remaining steps to complete a Gröbner basis w.r.t.\ some total-degree order are irrelevant for
what we want to illustrate. We factor the result for readability:
\begin{align*}
\sulut{-S_{1}+\compShift_{1}\compShift_{2}}{\textstyle \binom{\cdot}{\cdot}}&=0&\sulut{-S_{2}+\compShift_{2}}{\textstyle \binom{\cdot}{\cdot}}&=0\\\sulut{\compShift_{1}\compShift_{2}^{2}-\compShift_{2}-1}{\textstyle \binom{\cdot}{\cdot}}&=0\hspace{8em}&\sulut{\sulut{M_{2}+1}\compShift_{2}-M_{1}+M_{2}}{\textstyle \binom{\cdot}{\cdot}}&=0\\
&&\mathllap{\sulut{\sulut{M_{1}+1}\compShift_{1}\compShift_{2}-\sulut{M_{1}-M_{2}+2}\compShift_{1}-M_{1}-1}}{\textstyle \binom{\cdot}{\cdot}}&=0\\
&&\mathllap{\sulut{\sulut{M_{1}-M_{2}+1}\sulut{M_{1}-M_{2}+2}\compShift_{1}-M_{1}M_{2}-M_{2}}}{\textstyle \binom{\cdot}{\cdot}}&=0
\end{align*}
Now $\sigma$ maps the lowest four recurrences to recurrences of $f_{n_{1},n_{2}}=\binom{n_{1}}{n_{2}-n_{1}}$ below:
\begin{align*}
\sulut{S_{1}S_{2}^{2}-S_{2}-1}f&=0\hspace{6em}&\sulut{\sulut{M_{2}-M_{1}+1}S_{2}-2M_{1}+M_{2}}f&=0\\
&&\mathllap{\sulut{\sulut{M_{1}+1}S_{1}S_{2}-\sulut{2M_{1}-M_{2}+2}S_{1}-M_{1}-1}}f&=0\\
&&\mathllap{\sulut{\sulut{2M_{1}-M_{2}+1}\sulut{2M_{1}-M_{2}+2}S_{1}-\sulut{M_{1}+1}\sulut{M_{2}-M_{1}}}}f&=0
\end{align*}
The next step is to propagate to the summation. We postpone it to Example~\ref{Fibonacci2}\confrep{}{, after we have presented the required theory}.
\end{examplex}

\oursubsection{Propagation to Product}

Let $\cdot$ be ring multiplication or more generally a group bihomomorphism.
If the sequence terms $f$ and $g$ depend on disjoint sets of variables, recurrences of $fg = f\cdot g$ are essentially a union of recurrences of $f$ and $g$. Namely, let $Pf+e=0$ be any recurrence of $f$ where $P$ is an operator polynomial on the variables of $f$ and the excess terms $e$ do not contain $f$. Then $P\sulut{fg}+eg=0$ because $g$ is effectively a constant to $P$, and similarly for recurrences of $g$. With the help of this special case, propagation to product
can be reduced to propagation to substitution, as explained below.

\begin{procedurex}
Let $f$ and $g$ be sequence terms parameterized by the variables $\tuple n=\sulut{n_{j}}_{j=1}^{d}$. Let $\tuple m=\sulut{n_{j+d}}_{j=1}^{d}$ be a tuple of fresh variables. The recurrences of $f$ and $g$ are propagated to their pointwise product $fg$ in two steps. First, the recurrences of the variable-disjoint product $f_{\tuple n}g_{\tuple m}$ are the union of the recurrences of $f_{\tuple n}$
multiplied on the right by $g_{\tuple m}$ and of those of $g_{\tuple m}$ multiplied on the left by $f_{\tuple n}$. Then the recurrences of $f_{\tuple n}g_{\tuple n}=\left\{ \tuple m\mapsto\tuple n\right\} \sulut{f_{\tuple n}g_{\tuple m}}$ are found by propagating to substitution using Procedure~\ref{subs. prop.}.
\end{procedurex}

\oursubsection{Propagation to Summation}

We finally consider \confrep{}{as the last type of propagation }%
the summations $\sum_{n_{1}=0}^{n_{2}}f_{\tuple n}$.
\confrep{We can}{Without loss of generality, we} assume that the variables are numbered so that the sum acts on the first two.
Similarly to above, we consider the consequence $\sum_{n_{1}=0}^{n_{2}}Pf_{\tuple n}+\sum_{n_{1}=0}^{n_{2}}e_{\tuple n}=0$ of a recurrence $Pf+e=0$ of the sequence term $f$ where $P$ is an operator polynomial and $e$ are excess terms.
We want to find an operator polynomial $P'$ such that $\sum_{n_{1}=0}^{n_{2}}P$ becomes $P'\sum_{n_{1}=0}^{n_{2}}$ up to excess terms.
%Like for substitutions, it suffices to find $P'$ whenever $P$ is an %indeterminate.
%
Like for substitutions, finding such a $P'$ for $P$ can be reduced to finding an
operator polynomial $P'_X$ satisfying $\sum_{n_{1}=0}^{n_{2}}X =
P'_X\sum_{n_{1}=0}^{n_{2}}$ up to excess terms
for every indeterminant~$X$.
The result will be a recurrence $P'\sum_{n_{1}=0}^{n_{2}}f_{\tuple n}+e'=0$ of $\sum_{n_{1}=0}^{n_{2}}f_{\tuple n}$.

\begin{procedurex}
\looseness=-1
\label{sum prop.}Recurrences of a sequence term $f$ are propagated to its sum $\sum_{n_{1}=0}^{n_{2}}f_{\tuple n}$ as follows.
First, eliminate multipliers $M_{1}$ from all recurrences of $f$.
Every resulting recurrence $Pf+e=0$ implies $\sum_{n_{1}=0}^{n_{2}}Pf_{\tuple n}+\sum_{n_{1}=0}^{n_{2}}e_{\tuple n}=0$. Here, $P$ is an operator polynomial that does not contain $M_{1}$, and the excess terms $e$ do not contain $f$.
Next, each of these recurrences is rewritten into the form $P'\sum_{n_{1}=0}^{n_{2}}f_{\tuple n}+E_{0}+E_{n_{2}}+\sum_{n_{1}=0}^{n_{2}}e_{\tuple n}=0$ where $P'$ is an operator polynomial and the $E_{m}$'s are part of excess terms built by applying some operator polynomials and the substitution $\left\{ n_{1}\mapsto m\right\}$ to $f$.
This is achieved by commuting $\sum_{n_{1}=0}^{n_{2}}$ with indeterminates other than $S_{1}$ and $S_{2}$. These two indeterminates are instead handled by
\confrep{}{the formulas}
\begin{align*}
\sum_{n_{1}=0}^{n_{2}}S_{1}g_{\tuple n} & =\sum_{n_{1}=0}^{n_{2}}g_{\tuple n}+\left\{ n_{1}\mapsto n_{2}+1\right\} g_{\tuple n}-\left\{ n_{1}\mapsto0\right\} g_{\tuple n}\\
\sum_{n_{1}=0}^{n_{2}}S_{2}g_{\tuple n} & =S_{2}\sum_{n_{1}=0}^{n_{2}}g_{\tuple n}-S_{2}\left\{ n_{1}\mapsto n_{2}\right\} g_{\tuple n}
\end{align*}
\end{procedurex}
\begin{rep}
 
\begin{remarkx}
The summation $\sum_{n_{1}=0}^{n_{2}}f_{\tuple n}$ is defined if $f_{\tuple n}$ is defined when $0\leq n_{1}\leq n_{2}$.
This does not imply that $\sum_{n_{1}=0}^{n_{2}}Pf_{\tuple n}$ is defined because $P$ could shift $n_{1}$ more than $n_{2}$. Consequently, one might have to consider for example $\sum_{n_{1}=0}^{n_{2}-2}Pf_{\tuple n}$ instead and add $f\sulut{n_{2},n_{2}-1,\ldots}\allowbreak+f\sulut{n_{2},n_{2},\ldots}$ retroactively. This is awkward; we assume instead that sequence terms are globally defined. A similar issue affects propagation to substitution.
\end{remarkx}
\end{rep}

\begin{examplex}
\looseness=-1
\label{Fibonacci2}Let us continue the proof of ${%\displaystyle
\sum_{n_1=0}^{n_2}\binom{n_1}{n_2-n_1}=F_{n_2+1}}$ from Example~\ref{Fibonacci1}. There we found for the summand $f_{n_{1},n_{2}}=\binom{n_{1}}{n_{2}-n_{1}}$ a recurrence $(S_{1}S_{2}^{2}-S_{2}-1)f=0$. It is actually the only recurrence after eliminating $M_{1}$ as a first step of propagation to summation. Next, we set $S_{1}$ to 1 using a telescoping identity:
\begin{align*}
\sum_{n_{1}=0}^{n_{2}}S_{1}S_{2}^{2}f & =\sum_{n_{1}=0}^{n_{2}}S_{2}^{2}f+\left\{ n_{1}\mapsto n_{2}\right\} S_{1}S_{2}^{2}f-\left\{ n_{1}\mapsto0\right\} S_{2}^{2}f
\end{align*}
Then we push the remaining shifts $S_{2}$ leftwards:
\confrep{\[
\begin{array}{r}
\sum{}_{n_{1}=0}^{n_{2}}\sulut{S_{2}^{2}-S_{2}}f=S_{2}\sum{}_{n_{1}=0}^{n_{2}}\sulut{S_{2}-1}f-S_{2}\left\{ n_{1}\mapsto n_{2}\right\} \sulut{S_{2}-1}f\\
\vphantom{frac{\frac\int1}1}
=\sulut{S_{2}^{2}-S_{2}}\sum{}_{n_{1}=0}^{n_{2}}f-S_{2}^{2}\left\{ n_{1}\mapsto n_{2}\right\} f-S_{2}\left\{ n_{1}\mapsto n_{2}\right\} \sulut{S_{2}-1}f
\end{array}
\]
}{
\begin{align*}
\sum_{n_{1}=0}^{n_{2}}\sulut{S_{2}^{2}-S_{2}}f & =S_{2}\sum_{n_{1}=0}^{n_{2}}\sulut{S_{2}-1}f-S_{2}\left\{ n_{1}\mapsto n_{2}\right\} \sulut{S_{2}-1}f\\
 & =\sulut{S_{2}^{2}-S_{2}}\sum_{n_{1}=0}^{n_{2}}f-S_{2}^{2}\left\{ n_{1}\mapsto n_{2}\right\} f-S_{2}\left\{ n_{1}\mapsto n_{2}\right\} \sulut{S_{2}-1}f
\end{align*}
}Hence, in total we have 
\global\long\def\midminus{\negthickspace{}-}%
\begin{align*}
 & \sum_{n_{1}=0}^{n_{2}}\sulut{S_{1}S_{2}^{2}-S_{2}-1}f-\sulut{S_{2}^{2}-S_{2}-1}\sum_{n_{1}=0}^{n_{2}}f\\
 & \begin{array}{llll}
=\left\{ n_{1}\mapsto n_{2}\right\} S_{1}S_{2}^{2}f & \midminus\left\{ n_{1}\mapsto0\right\} S_{2}^{2}f & \midminus S_{2}^{2}\left\{ n_{1}\mapsto n_{2}\right\} f & \midminus S_{2}\left\{ n_{1}\mapsto n_{2}\right\} \sulut{S_{2}-1}f\\
=\binom{n_{2}+1}{1} & \midminus\binom{0}{n_{2}+2} & \midminus\binom{n_{2}+2}{0} & \midminus\binom{n_{2}+1}{1}+\binom{n_{2}+1}{0}\\
=\cancel{\binom{n_{2}+1}{1}} & \midminus0 & \midminus1 & \midminus\cancel{\binom{n_{2}+1}{1}}+1\hfill=0
\end{array}
\end{align*}
Since $(S_{1}S_{2}^{2}-S_{2}-1)f=0$, we have
$\sulut{S_{2}^{2}-S_{2}-1}\sum_{n_{1}=0}^{n_{2}}f=0$. Now this
 is the same recurrence that \confrep{}{the shifted Fibonacci numbers }%
 $F_{n_2+1}$ satisf\confrep{ies}{y} and hence
  the final propagation to difference gives $\sulut{S_{2}^{2}-S_{2}-1}\allowbreak(\sum_{n_{1}=0}^{n_{2}}f - F_{n_2+1})=0$.
   This proves an induction step of size 2 and leaves two base cases that can be
discharged by a theorem prover.
\end{examplex}

\begin{rep}
We can derive closed formulas for the summation propagation result after elimination of multiplication $M_{1}$ by the sum's index variable. This can help understand the form of the result while the recursive formulas of Procedure~\ref{sum prop.} remain a viable way to compute it. The telescoping formula amounts to Euclidean division of polynomials by $S_{1}-1$ (where $S_{1}$ commutes with remaining indeterminates because $M_{1}$ is eliminated). Namely, if $P\sulut{S_{1}}=\sulut{S_{1}-1}Q\sulut{S_{1}}+P\sulut 1$, then $P\sulut{S_{1}}f_{\tuple n}+e_{\tuple n}=0$ implies
%
\begin{align*}
-\sum_{n_{1}=0}^{n_{2}}e_{\tuple n} & =\sum_{n_{1}=0}^{n_{2}}P\sulut{S_{1}}f_{\tuple n}=\sum_{n_{1}=0}^{n_{2}}\sulut{\sulut{S_{1}-1}Q\sulut{S_{1}}f_{\tuple n}+P\sulut 1f_{\tuple n}} %=
\\
 & =\left\{ n_{1}\mapsto n_{2}+1\right\} Q\sulut{S_{1}}f_{\tuple n}-\left\{ n_{1}\mapsto0\right\} Q\sulut{S_{1}}f_{\tuple n}+\sum_{n_{1}=0}^{n_{2}}P\sulut 1f_{\tuple n}.
\end{align*}
Here, all terms except the last summation can be considered as excess to be eliminated later. The operator polynomial $P\sulut 1$ now contains neither $M_{1}$ nor~$S_{1}$. 

Concerning the second identity, let $\sigma=\left\{ n_{1}\mapsto n_{2}\right\} $. Then, for example
\begin{align*}
\sum_{n_{1}=0}^{n_{2}}S_{2}^{3}f_{\tuple n} & =S_{2}\sum_{n_{1}=0}^{n_{2}}S_{2}^{2}f_{\tuple n}-S_{2}\sigma S_{2}^{2}f_{\tuple n}\\
 & =S_{2}^{2}\sum_{n_{1}=0}^{n_{2}}S_{2}f_{\tuple n}-S_{2}^{2}\sigma S_{2}f_{\tuple n}-S_{2}\sigma S_{2}^{2}f_{\tuple n}\\
 & =S_{2}^{3}\sum_{n_{1}=0}^{n_{2}}f_{\tuple n}-S_{2}\sulut{S_{2}^{2}\sigma+S_{2}\sigma S_{2}+\sigma S_{2}^{2}}f_{\tuple n}
\end{align*}
and in general $\sum_{n_{1}=0}^{n_{2}}S_{2}^{a}f_{\tuple n}-S_{2}^{a}\sum_{n_{1}=0}^{n_{2}}f_{\tuple n}=-S_{2}\sum_{j=0}^{a-1}S_{2}^{j}\sigma S_{2}^{a-1-j}f_{\tuple n}$. Since $S_{2}\sigma=\sigma S_{1}S_{2}$, we can rewrite this as
\[
S_{2}\sum_{j=0}^{a-1}S_{2}^{j}\sigma S_{2}^{a-1-j}=\sum_{j=0}^{a-1}\sigma S_{1}^{j+1}S_{2}^{a}=\sigma\frac{S_{1}^{a}-1}{S_{1}-1}S_{1}S_{2}^{a}=\sigma\frac{\sulut{S_{1}S_{2}}^{a}-S_{2}^{a}}{S_{1}-1}S_{1}.
\]
So by linearity, for $P\sulut{S_{2}}$ containing neither $M_{1}$ nor $S_{1}$ we have
\[
\sum_{n_{1}=0}^{n_{2}}P\sulut{S_{2}}f_{\tuple n}-P\sulut{S_{2}}\sum_{n_{1}=0}^{n_{2}}f_{\tuple n}=-\sigma\frac{P\sulut{S_{1}S_{2}}-P\sulut{S_{2}}}{S_{1}-1}S_{1}f_{\tuple n}.
\]

Combining the previous formulas, we can write propagation of a recurrence $0=P\sulut{S_{1},S_{2}}f_{\tuple n}+e_{\tuple n}$ in the form
%
\begin{align*}
0=P\sulut{1,S_{2}}\sum_{n_{1}=0}^{n_{2}}f_{\tuple n} & +\left\{ n_{1}\mapsto n_{2}\right\} \frac{P\sulut{S_{1},S_{2}}-P\sulut{1,S_{2}}}{S_{1}-1}S_{1}f_{\tuple n} %-{}
\\
 & -\left\{ n_{1}\mapsto\mathrlap{0}\hphantom{n_{2}}\right\} \frac{P\sulut{S_{1},S_{2}}-P\sulut{1,S_{2}}}{S_{1}-1}f_{\tuple n} %-{}
 \\
 & -\left\{ n_{1}\mapsto n_{2}\right\} \frac{P\sulut{1,S_{1}S_{2}}-P\sulut{1,S_{2}}}{S_{1}-1}S_{1}f_{\tuple n} %+{}
 \\
 & +\sum_{n_{1}=0}^{n_{2}}e_{\tuple n} %=
\displaybreak[1]\\
=P\sulut{1,S_{2}}\sum_{n_{1}=0}^{n_{2}}f_{\tuple n} & +\left\{ n_{1}\mapsto n_{2}\right\} \frac{P\sulut{S_{1},S_{2}}-P\sulut{1,S_{1}S_{2}}}{S_{1}-1}S_{1}f_{\tuple n} %-{}
\\
 & -\left\{ n_{1}\mapsto\mathrlap{0}\hphantom{n_{2}}\right\} \frac{P\sulut{S_{1},S_{2}}-P\sulut{1,S_{2}}}{S_{1}-1}f_{\tuple n}+\sum_{n_{1}=0}^{n_{2}}e_{\tuple n} %.
\end{align*}
\end{rep}


\oursubsection{Iteration on Excess Terms}
\label{Iteration on excess}

Let $g$ be the term from the negated goal to be proved to be 0. After propagating along the structure of $g$, we end up with recurrences of the form $Pg=e$ where $P$ is an operator polynomial and the excess terms $e$ do not contain $g$. In the holonomic case, $e$ will be syntactically $0$.
We have also observed that $e$ is often $0$ in the nonholonomic case as well.
But if $e$ is not syntactically $0$, then $Pg=e$ cannot immediately be used for a proof by induction. A solution is to iterate a full series of propagations with $e$ in place of $g$ to find $P_{2}e=e_{2}$ and conclude $P_{2}Pg=P_{2}e=e_{2}$, then repeat as long as necessary. This process will always terminate, although it might fail to find recurrences.
\begin{rep}%
So in general, we propagate to $e_{j-1}$ to find $P_{j}e_{j-1}=e_{j}$, conclude $P_{j}\cdots P_{2}Pg=e_{j}$, and repeat until we encounter an $e_{k}=0$.
\end{rep}

We will impose an order on the sequence terms to accomplish three things. First, we get a proper %clean
definition of which terms in a recurrence are excess. Second, well-foundedness of the order will guarantee termination of the iteration of full propagations to excess terms. Third, the iterations can be interleaved with basic normalizations such as $\left\{ n_{1}\mapsto2n_{1}\right\} M_{1}\left\{ n_{1}\mapsto3n_{1}{+}1\right\} f\to2M_{1}\left\{ n_{1}\mapsto6n_{1}{+}2\right\} f$.

\begin{definitionx}
The \emph{spine} of a sequence term $f$ without addition, denoted by $\makeop{spine}f$, is the sequence term obtained intuitively by erasing operator polynomials from $f$. Precisely, this means fully reducing $f$ by the rewrite
rules \confrep{$at\to t$, $M_{j}t\to t$, $\{\vec{n}\mapsto b\vec{n}+\vec{c}\}t\to\{\vec{n}\mapsto b\vec{n}\}t$, and ${\textstyle \sum_{j}^{\vec{c}\bullet\vec{n}+a}}t\to{\textstyle \sum_{j}^{\vec{c}\bullet\vec{n}}}t$ }{
\begin{align*}
at & \to t & M_{j}t & \to t & \{\vec{n}\mapsto b\vec{n}+\vec{c}\}t & \to\{\vec{n}\mapsto b\vec{n}\}t & {\textstyle \sum_{j}^{\vec{c}\bullet\vec{n}+a}}t & \to{\textstyle \sum_{j}^{\vec{c}\bullet\vec{n}}}t
\end{align*}
}where $a$, $\vec c$, and the matrix %Keep “matrix” as that cannot be inferred over being integer.
$b$ are all numeric.
\end{definitionx}
\begin{sloppypar}
\confrep{S}{As substitutions, s}hift indeterminates mix with other
substitutions, which explains the last two rules. For example, $\makeop{spine}\,\left\{ n_{1}\mapsto2n_{1}\right\} M_{1}\left\{ n_{1}\mapsto3n_{1}+1\right\} f=\left\{ n_{1}\mapsto2n_{1}\right\}\allowbreak \left\{ n_{1}\mapsto3n_{1}\right\} f$. If we have a sequence term $c_{1}g^{1}+\cdots+c_{k}g^{k}$ with addition, it contains multiple spines, one for each $g^{j}$. The significance of spines is that when\pagebreak[2] we derive a more
complex consequence from a recurrence (during elimination by applying an operator polynomial to it), its spines do not become more complex.
\end{sloppypar}

We can easily describe how each propagation step changes the spines of the involved sequence terms. Propagation to the addition $f+g$ produces only spines $e_{f}$ and $e_{g}$ in the resulting recurrences, where $e_{f}$ denotes a spine of a term from a recurrence of $f$ and analogously for $e_{g}$. Moreover, propagation to the substitution $\sigma f$ produces $\sigma e_{f}$, propagation to the product $fg$ produces $(\makeop{spine}f)e_{g}$ and $e_{f}(\makeop{spine}g)$, and propagation to the summation $\sum_{n_{1}=0}^{n_{2}}f$ produces $\left\{ n_{1}\mapsto0\right\} \allowbreak(\makeop{spine}f)$, $\left\{ n_{1}\mapsto n_{2}\right\} \allowbreak(\makeop{spine}f)$, and $\sum_{n_{1}=0}^{n_{2}}e_{f}$, where $e_{f}$ and $e_{g}$ are as above.

\confrep{We want propagations to preserve the invariant that excess terms are small. Given how spines change under propagation, a term order on spines
offers a way to define smallness. We choose an order that also orients simplifications.}{Since term orders are compatible with contexts, comparing spines using a term order will almost automatically keep excess terms smaller than the main terms over propagation steps. This is an invariant we want to impose. Given how spines change under propagation, it suffices to additionally require that the term order satisfies $\sum_{j}^{a}t>\sigma t$ for substitutions $\sigma$ and sequence terms $t$. Below we consider a more specific term order, which will be able to orient simplification rules as well.
%Below sentence was a justification for the introduction of relatively strange TKBO. However, now that the argument coefficients are an optional feature of KBO, the sentence is redundant.
%(Note that the terminating simplifications \{$\sigma\sulut{ts}\to\sigma t\cdot\sigma s$, $\sigma\sigma't\to\sulut{\sigma\circ\sigma'}t$\} can be oriented neither by the Knuth--Bendix order without argument coefficients \cite{KBO-03,KBO-09} nor by the lexicographic path order \cite{RPO-82,LPO<RPO-83}.)
}
\begin{definitionx}
\label{excess}\looseness=-1 Fix a Knuth--Bendix order with argument coefficients \cite{TKBO-07} with
exactly three weights $W\sum_{n=0}^{a}>W\sulut{\cdot}>3W\sigma>0$ and all argument coefficients set to 2. Moreover, projection sequence terms corresponding to $M_{j}$'s (Remark~\ref{recurrence as term}) must have equal weights, and substitutions with fewer bindings must have lower precedence\confrep{}{ than those with more bindings}. The \emph{excess} (\emph{partial}) \emph{order} on addition-free sequence terms is obtained by comparing the spines of terms using this fixed order. \emph{Excess terms} of a recurrence are all its nonmaximal sequence terms w.r.t.\ the excess order.
\end{definitionx}

The weights for the excess order are arranged to be compatible with normalization, which pushes substitutions to the leaf nodes of the term tree and pulls summations towards the root. The resulting normal form is simply the typical way of writing terms without explicit substitutions. It is also the normal form of the rewrite system consisting of the applicable associativity and/or commutativity rules of $\cdot$ as well as the following rules:
\begin{align*}
{\textstyle s\cdot\sum_{j}^{a}t}&\to{\textstyle \sum_{j}^{a}st}&\mathllap{1t,t1,\left\{ \right\} t}&\to t\\{\textstyle \left(\sum_{j}^{a}s\right)\cdot t}&\to{\textstyle \sum_{j}^{a}st}&\mathllap{\sulut{\sigma\cup\left\{ n_{j}\mapsto a\right\} }u}&\to\sigma u\\{\textstyle \sigma\sum_{j}^{a}t}&\to{\textstyle \sum_{j}^{\sigma a}\sigma t}&\mathllap{\sulut{\sigma\cup\left\{ n_{j}\mapsto a\right\} }M_{j}}&\to a\\{\textstyle \sum_{j}^{c}t}&\to\left\{ n_{j}\mapsto0\right\} t+\cdots+\left\{ n_{j}\mapsto c\right\} t&\sigma\sulut{ts}&\to\sigma t\cdot\sigma s\\{\textstyle \sum_{j}^{-c}t}&\to-\left\{ n_{j}\mapsto-1\right\} t-\cdots-\left\{ n_{j}\mapsto1-c\right\} t&\sigma\sigma't&\to\sulut{\sigma\circ\sigma'}t
\end{align*}
where $s,t,u$ are sequence terms, $u$ does not contain the variable $n_{j}$, $a$ is an affine variable sum, $M_{j}=\tuple n \mapsto n_{j}$ is a projection sequence term, $\sigma,\sigma'$ are affine substitutions, and the numeral $c$ is nonnegative.

\looseness=-1
These rules produce additions, which must be interpreted as follows. For any rule above of the general form $t_{0}\to c_{1}t_{1}+\cdots+c_{k}t_{k}$, the actual rewrite on the level of entire recurrences is $f\left[t_{0}\right]+R=0\,\to\,c_{1}f\left[t_{1}\right]+\cdots+c_{k}f\left[t_{k}\right]+R=0$ where $c_{j}$ are numerals, the sequence terms $f\left[t_{j}\right]$ are equal except for the distinguished subterm $t_{j}$, and $R$ is the sum of the remaining terms in the recurrence.
\begin{rep}
This is analogous to how monomial reductions lift to polynomials in Gröbner basis theory.
\end{rep}

To conclude termination, it suffices to prove that $t_{0}$ dominates each of $t_{1},\dots,\allowbreak t_{k}$ individually. \confrep{The proof is in our technical report. It makes apparent our choices of weights and argument coefficients for the transfinite Knuth--Bendix order.}{Let us proceed down the right column. The first rule triple ($1t,\allowbreak t1,\allowbreak \left\{ \right\} t\to t$) is trivial. In the second rule, by assumption removing a binding from a substitution $\sigma\cup\left\{ n_{j}\mapsto a\right\} $ lowers its precedence. The third rule needs only $\sulut{\sigma\cup\left\{ n_{j}\mapsto a\right\} }M_{j}>M_{k}$ for all $j,k$, which holds because $M_{j}$ and $M_{k}$ have the same weight. For the fourth rule, the only duplicating rule $\sigma\sulut{ts}\to\sigma t\cdot\sigma s$ requires $W\sigma+2\sulut{W\sulut{\cdot}+2\sulut{Wt+Ws}}>W\sulut{\cdot}+4W\sigma+4Wt+4Ws$, which is equivalent to the assumption $W\sulut{\cdot}>3W\sigma$.
For the last rule, combining substitutions $\sigma$ and $\sigma'$ into one $\sigma\circ\sigma'$ decreases the weight.
The rules on the left column are similarly oriented by the assumed weight order. While comparing spines first, these orientations remain, although they might be
nonstrict.

\subsection{The Question of Completeness in the Holonomic Case}

We do not know if our procedure is complete in the holonomic case\,---\,that is, if it propagates enough recurrences to reduce deciding equality to a finite number of base cases for any holonomic atomic sequence terms.
Since our method is closely related to the holonomic decision procedure, one could have expected that proving completeness in our setting would be easy to achieve.
However, there are several issues that prevented us from proving completeness.

The main issue arises in connection with propagation to substitution.
It is not related to the unusual algebra of the compound shifts, but rather to the change---especially the reduction---of the number of variables.
Indeed, we do not even know if propagation to $\left\{ n_{1}\mapsto0\right\} $ is complete. For $\left\{ n_{1}\mapsto0\right\} $, the compound shifts are simply all $S_{j}$ for $j\geq2$ and the propagation procedure can be reformulated as follows: Eliminate $S_{1}$ and replace $M_{1}$ by 0 in the remaining recurrences.
\begin{examplex}\sloppypar
Consider the operator polynomials $\{ M_{1}\sulut{S_{1}-1},$ $M_{1}\sulut{S_{2}-1},$ $S_{1}\sulut{S_{2}-1}\}$, which form a Gröbner basis (w.r.t.\ any monomial order).
If a sequence $f$ satisfies the corresponding recurrences, $f$ is holonomic.
Namely, using first $M_{1}\sulut{S_{1}-1}$ and then $S_{1}\sulut{S_{2}-1}$, we get $f_{1,0}=f_{1+n_{1},0}=f_{1+n_{1},n_{2}}$ and similarly $f_{0,0}=f_{-n_{1},0}=f_{-n_{1},n_{2}}$ for $n_{1}\in\mathbb{N}$ and $n_{2}\in\mathbb{Z}$.
Hence $f$ is determined by only two base cases (namely, $f_{1,0}$ and $f_{0,0}$) and is therefore holonomic.

Now consider propagation to $\left\{ n_{1}\mapsto0\right\} f_{\tuple{n}}$.
If we discard recurrences containing $S_{1}$, we are left with $M_{1}\sulut{S_{2}-1}f=0$. But replacing $M_{1}$ by 0 here gives the triviality $0=0$, leading to no recurrences for $\left\{ n_{1}\mapsto0\right\} f_{\tuple{n}}$.
In general, the replacement is the issue that this entire subsection is about.
In this example, we recover thanks to the requirement that shifts are canceled during elimination, because then $S_{1}\sulut{S_{2}-1}$ yields $S_{2}-1$, and this operator polynomial gives us a useful recurrence for $\left\{ n_{1}\mapsto0\right\} f_{\tuple{n}}$.
\end{examplex}
In the same way that propagation to $\left\{ n_{1}\mapsto0\right\} $ eliminates $S_{1}$ and replaces $M_{1}$ by 0, propagation to $\sum_{n_{1}}$ eliminates $M_{1}$ and replaces $S_{1}$ by 1 (and adds excess terms).
However, with $\sum_{n_{1}}$, if replacement would map a recurrence to $0$, we can avoid the problem thanks to the identity $M_{1}\sulut{S_{1}-1}-\sulut{S_{1}-1}\sulut{M_{1}-1}=-1$.
Using this, we see that an ill-behaved recurrence $\sulut{S_{1}-1}R=0$ implies 
\[
0=M_{1}\sulut{S_{1}-1}R=\sulut{S_{1}-1}\sulut{M_{1}-1}R-R
\]
where $\sulut{S_{1}-1}\sulut{M_{1}-1}R$ will map to 0, leaving $R=0$. Higher powers of $S_{1}-1$ are canceled by iterating this. For $\left\{ n_{1}\mapsto0\right\} $, there is no similar identity $PM_{1}-M_{1}P'=-1$;
this can be seen by applying it to $\delta_{n_{1},0}$ and evaluating at $n_{1}=0$.

The above standard argument works even better in the differential setting \cite{close,MathematicaHolo,basicholo}.
There differentiation $\partial_{j}$ w.r.t.\ variable $n_{j}$ of index $j$ takes the place of the shift $S_{j}$.
Propagation to integration $\int dn_{1}$ is secured by $M_{1}\partial_{1}-\partial_{1}M_{1}=-1$, and to substitution $\left\{ n_{1}\mapsto0\right\} $ by $-\partial_{1}M_{1}-M_{1}\sulut{-\partial_{1}}=-1$.
In fact, the proper theory of holonomicity exists in the differential setting and merely translates to the discrete in the coefficients of the power series of functions.
Then the discrete substitution $\left\{ n_{1}\mapsto-1\right\} $ corresponds to contour integration around 0.
However, only $\partial_{1}$ cancels when integrating, whereas the discrete $M_{1}+1$ corresponds to the differential product $\partial_{1}M_{1}$ (because $\frac{\partial}{\partial z}z\sulut{f_{k}z^{k}}=\sulut{k+1}\sulut{f_{k}z^{k}}$). In other words, a Gröbner basis of our shifty operator polynomials contains different, possibly worse, information than a Gröbner basis of differential polynomials that actually define the holonomicity.

We still expect that our procedure is complete.
To support this, fix a transcendental constant $q$ and consider the $\mathbb{Z}$-algebra spanned by shifts and exponential multipliers $q^{n_{j}}$ (instead of $n_{j}$, also known as $M_{j}$).
For the substitution $\left\{ n_{1}\mapsto0\right\} $, we observe the same issue that $q^{n_{1}}-1$ is replaced by 0 and uncancellable.
However, using homological algebra, Sabbah proved that substitution---with a compound shift indeterminate based method---preserves holonomicity in this algebra \cite{qholo}.
In the analytic limit $q\to1$, we also have $\sulut{q^{n_{j}}-1}/\sulut{q-1}\to n_{j}$, and we obtain our operator polynomial algebra.
Unfortunately, this observation tells us nothing about the computational behavior of operator polynomials and their Gröbner bases.
}
\section{Induction}
\label{sec:induction}

After propagation, we consider all recurrences $Pg=0$ of the goal sequence term $g$ to be proved to be 0.
In exceptionally fortunate cases, the operator polynomial $P$ is $\pm1$ and we are unconditionally done because, for any group, the multiplication-by-$\pm1$ map is invertible.
This happens when the objective is to prove a recurrence that this method derives as a substep anyway.
Otherwise, we apply induction and leave as conditions the base cases as well as invertibility of the multiplication maps associated with the leading monomials' coefficients.

A common case is that variables range over natural numbers and we have a final recurrence with leading shift $S_{1}^{b_{1}}\cdots S_{d}^{b_{d}}$ w.r.t.\ any monomial order.
Then the values $\smash{\bigcup_{j=1}^{d}\set{\tuple n\in\mathbb{N}^{d}}{n_{j}<b_{j}}}$ suffice for the base cases,
as a union of stacked\pagebreak[2] hyperplanes that is infinite unless $d\leq1$, but it corresponds to only $\sum_{j=1}^{d}b_{j}$ one-variable substitutions $\left\{ n_{j}\mapsto a\right\} $ for $1\leq j\leq d$ and $0\leq a<b_{j}$.
If our eager
generalization produced variables that do not participate in their induction (i.e., their $b_{j}$'s are $0$), they are replaced back to their original values.

If there is more than one applicable final recurrence, we take the intersection of their base value sets w.r.t.\ the same monomial order.
To see that it works, consider any point outside the intersection.
It is a nonbase point w.r.t.\ some final recurrence and hence
the induction step can be taken by the recurrence.
\confrep{}{If recurrences have different side conditions, then there might not be an optimal combination of base cases and conditions but rather many incomparable options to choose from.}

To represent the intersection as substitutions, we distribute it over the hyperplane stack unions.
This results in a union of hyperline stacks of the form $N(J,\vec b) := \set{\tuple n\in\mathbb{N}^{d}}{n_{j}<b_{j}\text{ for all }j\in J}$ where $J\subseteq\left\{ 1,\dotsc,d\right\} $ and $\vec b$ vary.
One such stack is represented by $\prod_{j\in J}b_{j}$ substitutions $\set{n_{j}\mapsto a_{j}}{j\in J}$ where the $a_{j}$'s are chosen arbitrarily
such that $0 \le a_{j} < b_j$.
Unfortunately, distribution duplicates some base cases. To compensate, if $I\subseteq J$ and $\smash{\tuple b}\geq\tuple c$ pointwise, then $N(I,\vec b) \supseteq N(J,\vec c)$, so that $N(J,\vec c)$ can be removed in favor of $N(I,\vec b)$.

If a variable $n\in\mathbb{Z}$ is unbounded, we perform two inductions on the
rays: $0\leq n$ and $n<b$ if $b$ base cases are needed. The backward induction on $n<b$ can be transformed into \confrep{an}{a forward} induction on \confrep{$\mathbb{N}$}{natural numbers starting from 0} by the change of variables $n\mapsto b-1-n$.

\section{Examples}
\label{sec:examples}

\newcommandx\Stirling[2][usedefault, addprefix=\global, 1=k, 2=n]{\left\{  \begin{subarray}{c}
#1\\
#2\vphantom{()}
\end{subarray}\right\}  }%
Our procedure can prove the induction step of holonomic sequence formulas such as
Example \ref{Fibonacci1}, the binomial formula:
\[\blink{\sulut{a+b}^{h}=\sum_{n=0}^{h}{\textstyle\binom{h}{n}}a^{n}b^{h-n}}{binomial}\qquad\qquad\blink{{\textstyle\binom{a+b}{h}}=\sum_{n=0}^{h}{\textstyle\binom{a}{n}}{\textstyle\binom{b}{h-n}}}{Vandermonde}\]%
%
Heterogeneous recurrences, which are beyond the holonomic fragment, enable
proving elementary general sequence formulas such as Example \ref{indefinite
sum ex.}
and the following:
\[\blink{\sum_{n=0}^{h}f_{h-n}=\sum_{n=0}^{h}f_{n}}{reverse}\qquad\qquad\blink{\sum_{h=0}^{k}\sum_{n=0}^{h}f_{h,n}=\sum_{n=0}^{k}\sum_{h=n}^{k}f_{h,n}}{swapsum}\]
If we ignore the holonomic base case requirements, we can for example prove the induction steps of Abel's binomial formula and of some Stirling number identities:
\begin{align*}
\confrep{\textstyle}{}
\blink{\sulut{a+b}^{h}=\sum_{n=0}^{h}{\textstyle\binom{h}{n}}a\sulut{a-n}^{n-1}\sulut{b+n}^{h-n}}{Abel}
&& \confrep{\textstyle}{}
{h^{k}}/{h!} & \confrep{\textstyle}{}
=\sum_{n=0}^{h}\Stirling/\sulut{h-n}!
\end{align*}
Here, the Stirling numbers of the second kind \smash{$\Stirling$} are one of many special nonholonomic sequences that frequently arise in combinatorics.
They count the number of partitions of a $k$-element set into $n$ subsets.

\def\StirlingExample{
As further demonstration, we apply our procedure to the last equation.
For convenience, we will use the name of a variable also to denote its
multiplier operator. Moreover, we will use the uppercase version of the name of
a variable to denote its shift operator.
%Thus $\sulut{nf}_{n}=n\cdot f_{n}$ and $\sulut{Nf}_{n}=f_{n+1}$ for a sequence %term $f$ with variable named $n$.
The defining recurrence of the Stirling numbers then reads $\sulut{KN-\sulut{n+1}N-1}\Stirling=0$
for $k,n\geq0$, where $K$ and $N$ denote
the shift operators for the variables $k$ and $n$, the first $n$ denotes
the multiplier for the variable~$n$, and the second $n$ is the variable itself.
This recurrence is complemented
by the initial values $\smash{\Stirling[0][0]=1}$ and $\smash{\Stirling[n][0]=\Stirling[0][n]=0}$ if $n \not= 0$.

Starting from the right, the inverse $m!^{-1}$ of the factorial satisfies the recurrence $\sulut{mM+M-1}m!^{-1}=0$ that holds for all $m\in\mathbb{Z}$ by extension. This must be found in the initialization step because there is no propagation to division. Propagation to the substitution $\left\{ m\mapsto h-n\right\} $ then gives the following recurrences, factored for clarity:
\begin{align*}
\sulut{\sulut{h-n+1}H-1}\sulut{h-n}!^{-1}& =0
& \sulut{N-h+n}\sulut{h-n}!^{-1} & =0
\end{align*}

To propagate to product,
we consider $\Stirling[k_{1}][n_{1}]$ and $\sulut{h_{2}-n_{2}}!^{-1}$ with variables renamed apart. We must propagate to the substitution $\{n_{j} \mapsto n${,}\; $h_{j} \mapsto h${,}\; $k_{j} \mapsto k \mid\allowbreak j\in\left\{ 1,2\right\} \}$ the recurrences of $\Stirling[k_{1}][n_{1}]\sulut{h_{2}-n_{2}}!^{-1}$ given by the following five operator polynomials:
\begin{align*}
K_{1}N_{1}-\sulut{n_{1}+1}N_{1}-1 \s\text{~and~}\s H_{1}-1 & \quad\text{ from \ensuremath{\Stirling[k_{1}][n_{1}]}}\\
\sulut{h_{2}-n_{2}+1}H_{2}-1,\s N_{2}-h_{2}+n_{2}{,} \s\text{~and~}\s K_{2}-1 & \quad\text{ from }\sulut{h_{2}-n_{2}}!^{-1}
\end{align*}
We added here the trivial recurrences given by $H_{1}-1$ and $K_{2}-1$ implied by the independence from $h_{1}$ and $k_{2}$. Among the defining recurrences~\eqref{eqn:defining_relation_comp_shift} of the compound shift indeterminates $N,H,K$, the recurrence $H_{1}H_{2}-H$ simplifies to $H_{2}-H$
by $H_1 - 1$
and $K_{1}K_{2}-K$ to $K_{1}-K$
by $K_2 - 1$.
(In other words, the factorwise renaming of already disjoint variables $h$ and $k$ amounts to renaming in the entire product.)
The third compound shift recurrence, $N_{1}N_{2}-N$, simplifies to $\sulut{h_{2}-n_{2}}N_{1}-N$ by $N_{2}-h_{2}+n_{2}$. The part of the Gröbner basis with only compound shifts is then straightforwardly finished with the result $\left\{ KN-\sulut{n_{1}+1}N-h_{2}+n_{2},\s\sulut{h_{2}-n_{2}+1}H-1\right\}$. Hence this propagation step yields

%%% TYPESETTING: hack
\vskip\abovedisplayshortskip
\vskip-\abovedisplayskip
\vskip-\baselineskip

\begin{align*}
\sulut{KN-\sulut{n+1}N-h+n}\frac{\Stirling}{\sulut{h-n}!}&=0&\sulut{\sulut{h-n+1}H-1}\frac{\Stirling}{\sulut{h-n}!}&=0
\end{align*}

To sum over $n$, we first eliminate $n$ from the previous two recurrences and conclude $\sulut{H\sulut{K-h}+\sulut{N-1}\sulut{KH-\sulut{h+1}H+1}}\sulut{\Stirling/\sulut{h-n}!}=0$. The sum has natural boundaries, meaning that the summand vanishes outside them. This guarantees that there will be no excess terms, which we also tediously discover when pulling out the indeterminates:
\[\begin{array}{l}
{\displaystyle {\textstyle \sumBig\limits_{n=0}^{h}}\sulut{N-1}\smash{\overset{P}{\overbrace{\sulut{KH-\sulut{h+1}H+1}}}}\frac{\Stirling}{\sulut{h-n}!}=P\sulut{\frac{\Stirling[][h+1]}{\sulut{-1}!}-\frac{\Stirling[][0]}{h!}}}\\ % =
\hfill{\displaystyle =-\Stirling[k+1][0]/\sulut{h+1}!+\Stirling[][0]\sulut{\sulut{h+1}H-1}h!^{-1}=0}\\
{\displaystyle {\textstyle \sumBig\limits _{n=0}^{h}}H\sulut{K-h}\frac{\Stirling}{\sulut{h-n}!}-H\sulut{K-h}{\textstyle \sumBig\limits _{n=0}^{h}}\frac{\Stirling}{\sulut{h-n}!}=-\sulut{K-h}\frac{\Stirling[][h+1]}{\sulut{-1}!}=0}
\end{array}\]
Here, by the recurrence of the inverse of the factorial, we get $\sulut{-1}!^{-1}=0$. So we obtain a recurrence $H\sulut{K-h}\sum_{n=0}^{h}\Stirling/\sulut{h-n}!=0$ for the left-hand side of our goal. For the right-hand side, we unproblematically obtain $\sulut{K-h}$\allowbreak$\sulut{h^{k}/h!}=0$. Hence $H\sulut{K-h}$ zeros out the difference
$h^k/h!-\sum_{n=0}^{h}\Stirling/\sulut{h-n}!$.
\confrep{}{\par}
The largest shift $HK$ of the operator $H\sulut{K-h}$ determines that the two sets of base cases $h=0$ and $k=0$ are sufficient for induction.\confrep{}{ Unlike in the holonomic setting, the base cases are not necessarily easier than the original formula. Hence, we leave the base cases to the prover. Here, the first case $h=0$ is easy because the sum becomes a single term. On the other hand, when $k=0$ the sum retains its variable length of $h+1$, but the nonholonomic factor $\Stirling$ simplifies to its initial value $\Stirling[0]$.
With these initial values, only the term with $n=0$ remains, while generally we might have to repeat \SumInf..}
}
\confrep{\StirlingExample}{\begin{examplex}\StirlingExample\end{examplex}}

\begin{rep}

\begin{examplex}
Let $a,b\in\mathbb{R}$ be reals and $h\in\mathbb{N}$ be a natural number. We prove 
\[
\sulut{a+b}^{h}=\sum_{n=0}^{h}\binom{h}{n}a^{n}b^{h-n}
\]
\label{binomial}For the sake of conciseness, let us use only the recurrence of $\binom{h}{n}$ that already lacks multiplication by $n$---namely, $\sulut{HN-N-1}\binom{h}{n}=0$ from Pascal's triangle. To propagate to the product $\binom{h}{n}a^{n}$ we rename variables $n$ apart as $n_{1}$ and $n_{2}$, and proceed to eliminate their shifts $N_{1}$ and $N_{2}$ from 
\[
HN_{1}-N_{1}-1\qquad N_{2}-a\qquad N_{1}N_{2}-N
\]
Here $N_{1}N_{2}-N$ is the defining relation~(\ref{eqn:defining_relation_comp_shift}) for the compound shift $N$. Immediately, $N_{2}-a$ rewrites $N_{1}N_{2}-N$ to $aN_{1}-N$. A superposition $a\sulut{HN_{1}-N_{1}-1}-H\sulut{aN_{1}-N}=HN-aN_{1}-a$ leaves a conclusion that is rewritten to $HN-N-a$ by $aN_{1}-N$, completing the propagation.

We find the obvious recurrences $\sulut{bN-1}b^{h-n}=0$ and $\sulut{H-b}b^{h-n}=0$ by propagation to substitution. To propagate to the final product $\binom{h}{n}a^{n}\cdot b^{h-n}$ we rename like above and eliminate $N_{1},N_{2},H_{1},H_{2}$ from the operator polynomials 
\[
H_{1}N_{1}-N_{1}-a\qquad\begin{array}{c}
bN_{2}-1\\
H_{2}-b
\end{array}\qquad\begin{array}{c}
N_{1}N_{2}-N\\
H_{1}H_{2}-H
\end{array}
\]
The top-row polynomials give $N_{1}-bN$, which rewrites $H_{1}N_{1}-N_{1}-a$ to $bH_{1}N-bN-a$. The bottom-row polynomials give $bH_{1}-H$, and one rewrite later we conclude $\sulut{HN-bN-a}\sulut{\binom{h}{n}a^{n}b^{h-n}}=0$.

The propagation to summation $\sum_{n=0}^{h}$ will map $N\mapsto1$ in the recurrence of the main term, giving $H-b-a$, which also annihilates the left-hand side $\sulut{a+b}^{h}$. Finally, we check that the excess terms become 0:
%
\begin{align*}
0 & =\sum_{n=0}^{h}\sulut{HN-bN}\sulut{\binom{h}{n}a^{n}b^{h-n}}=\sum_{n=0}^{h}\sulut{H-b}\sulut{\binom{h}{n}a^{n}b^{h-n}}+\\
 & \quad+\left\{ n\mapsto h+1\right\} \sulut{H-b}\sulut{\binom{h}{n}a^{n}b^{h-n}}-\left\{ n\mapsto0\right\} \sulut{H-b}\sulut{\binom{h}{n}a^{n}b^{h-n}}=\\
 \displaybreak[1]\\
 & =\sum_{n=0}^{h}\sulut{H-b}\sulut{\binom{h}{n}a^{n}b^{h-n}}+\binom{h+1}{h+1}a^{h+1}-0-\binom{h+1}{0}b^{h+1}+b\binom{h}{0}b^{h}=\\
 & =\sulut{H-b}\sum_{n=0}^{h}\binom{h}{n}a^{n}b^{h-n}-\binom{h+1}{h+1}a^{h+1}+a^{h+1}=\sulut{H-b}\sum_{n=0}^{h}\binom{h}{n}a^{n}b^{h-n}
\end{align*}

Hence the operator polynomial $H-b-a$ annihilates (meaning maps to 0) the entire difference $\sulut{a+b}^{h}-\sum_{n=0}^{h}\binom{h}{n}a^{n}b^{h-n}$. For induction, the leading shift monomial of $H-b-a$ is $H$. Hence an induction step of size 1 w.r.t.\ $h$ is guaranteed to succeed. The base cases are obtained by substituting $\left\{ h\mapsto0\right\} $, and a theorem prover can check them by direct simplification.
\end{examplex}
%
\begin{examplex}
We prove Vandermonde's convolution formula
\[
\binom{a+b}{h}=\sum_{n=0}^{h}\binom{a}{n}\binom{b}{h-n}
\]
\label{Vandermonde}The textbook proof is to expand the three binomial powers in $\sulut{x+1}^{a+b}=\sulut{x+1}^{a}\sulut{x+1}^{b}$ and then match the like powers of $x$. Since both sides of the summation formula are polynomials in $a$ and $b$, it must hold for $a$ and $b$ taken from any commutative ring. Our recurrence propagation procedure can directly work in this full generality by only considering recurrences in $n$ and $h$.

We start from $\sulut{\sulut{n{+}1}N+n-a}\binom{a}{n}=0$. This propagates to $\binom{b}{h-n}=\{a\mapsto b$, $n\mapsto h-n\} \binom{a}{n}$ as $\sulut{\sulut{h-n+1}H+h-n-b}\binom{b}{h-n}=0$ and $\sulut{HN-1}\binom{b}{h-n}=0$ with monomial order such that $H<N$. Next, to propagate to product we rename $n$ as $n_{1}$ and $n_{2}$, and proceed to eliminate $N_{1}$ and $N_{2}$ from 
\[
\sulut{n_{1}+1}N_{1}+n_{1}-a\qquad\begin{array}{c}
\sulut{h-n_{2}+1}H+h-n_{2}-b\\
HN_{2}-1
\end{array}\qquad N_{1}N_{2}-N
\]
From $HN_{2}-1$ and $N_{1}N_{2}-N$ we derive $N_{1}-HN$ that rewrites the leftmost operator polynomial leading to the result 
\[
\sulut{n_{1}+1}HN+n_{1}-a\qquad\sulut{h-n_{2}+1}H+h-n_{2}-b
\]
where we then identify $n_{1}$ and $n_{2}$. After this identification, if $nH$ is the leading monomial of the right polynomial, it could rewrite the leading monomial $nHN$ of the left polynomial. This shows that the final result of propagation steps need not be a Gröbner basis, which is unproblematic. Instead, we start with that rewrite when propagating to summation $\sum_{n=0}^{h}$ next. The result of the rewrite is $n-a+\sulut{h+1}H+N\sulut{h-n-b}$. Its leading monomial $nN$ superposes with $nH$ of $\sulut{h-n+1}H+h-n-b$ because we must eliminate $n$. After simplifying the result, we get 
\[
\sulut{H+1}\sulut{\sulut{h+1}H+h-a-b}-bH\sulut{N-1}
\]
which does not contain $n$. In the first term, $\sulut{h+1}H+h-a-b$ annihilates the left-hand side $\binom{a+b}{h}$ of the goal equation, while the second term $-bH\sulut{N-1}$ maps to 0 when $N$ maps to 1. This implies that the final operator polynomial we get is $\sulut{H+1}\sulut{\sulut{h+1}H+h-a-b}$, but we must also check that the excess terms become 0.

The excess term computation is routine but lengthy. We omit it because we know that it succeeds by the following argument. The sum $\sum_{n=0}^{h}\binom{a}{n}\binom{b}{h-n}$ has so-called natural boundaries, meaning that the summand is 0 outside the interval $\left[0,h\right]$. Hence the summation range $\left[0,h\right]$ can be extended without changing the value of the sum or the value of the excess terms that depends on the sum. However, excess terms are found by evaluation at the end points of the summation range. When the range is extended enough (by about the degree of the operator polynomial), it becomes obvious that the excess terms equal 0.
\end{examplex}

\begin{examplex}Let $f$ be group-valued and $h$ be a natural number. We prove
\[
\mathcal{L}_{h}:=\sum_{n=0}^{h}f_{h-n}=\sum_{n=0}^{h}f_{n}=:\mathcal{R}_{h}
\]
\label{reverse}Let us start with the substitution on the left-hand side.
If $h-n=k$, then $\sulut{h+1}-n=k+1$ and $h-\sulut{n+1}=k-1$, so $H=K$ and $N=K^{-1}$ define the relevant compound shifts. The latter equation, $N=K^{-1}$, translates to the polynomial $NK-1$, which simplifies to $NH-1$ when $K$ is eliminated by the equation $H=K$. So we conclude $\sulut{NH-1}f_{h-n}=0$.

Next, we push the indeterminates leftwards to propagate to the summation $\mathcal{L}_{h}=\sum_{n=0}^{h}f_{h-n}$ and simplify the excess terms as we proceed: 
\begin{align*}
0 & =\sum_{n=0}^{h}\sulut{NHf_{h-n}-f_{h-n}}=\left\{ n{\mapsto}h{+}1\right\} Hf_{h-n}-Hf_{h-0}+\sum_{n=0}^{h}\sulut{Hf_{h-n}-f_{h-n}}\\
 & =f_{0}-Hf_{h}-Hf_{h-h}+\sulut{H-1}\sum_{n=0}^{h}f_{h-n}=-Hf_{h}+\sulut{H-1}\mathcal{L}_{h}
\end{align*}
Hence $\sulut{H-1}\mathcal{L}_{h}-Hf_{h}=0$. Since we also have $\sulut{H-1}\mathcal{R}_{h}=Hf_{h}$, the final propagation to difference gives $\sulut{H-1}\sulut{\mathcal{R}_{h}-\mathcal{L}_{h}}=0$. The rest of the proof is routine.
\end{examplex}

\begin{examplex}Let $f$ be group-valued and $k$ be a natural number. We prove
\[
\mathcal{L}_{k}:=\sum_{h=0}^{k}\overset{l_{h}}{\overbrace{\sum_{n=0}^{h}f_{h,n}}}=\sum_{n=0}^{k}\overset{r_{k,n}}{\overbrace{\sum_{h=n}^{k}f_{h,n}}}=:\mathcal{R}_{k}
\]
\label{swapsum}First consider the left-hand side $\mathcal{L}_{k}$. Trivially, $\sulut{K-1}l_{h}=0$ with $K$ denoting a shift w.r.t.~$k$. This recurrence has no multiplication by $h$, so we directly proceed to pull it over $\sum_{h=0}^{k}$ to get a recurrence for $\mathcal{L}_{k}$: 
\[
0=\sum_{h=0}^{k}\sulut{Kl_{h}-l_{h}}=-K\left\{ h\mapsto k\right\} l_{h}+\sulut{K-1}\sum_{h=0}^{k}l_{h}=-Kl_{k}+\sulut{K-1}\mathcal{L}_{k}
\]

Next, consider the right-hand side $\mathcal{R}_{k}$. Recall that $r_{k,n}$ can be expressed in terms of summations from 0 as $\sum_{h=0}^{k}f_{h,n}-\sum_{h=0}^{n-1}f_{h,n}$. Nevertheless, the constancy recurrence $\sulut{K-1}f_{h,n}=0$ propagates as above, yielding $\sulut{K-1}r_{k,n}-Kf_{k,n}=0$. To propagate from $r_{k,n}$ to $\mathcal{R}_{k}$, we pull the shift $K$ over $\sum_{n=0}^{k}$ as follows:
\begin{align*}
0 & =\sum_{n=0}^{k}\sulut{Kr_{k,n}-r_{k,n}-Kf_{k,n}}\\
 & =-Kr_{k,k}+\sulut{K-1}\sum_{n=0}^{\smash{k}}r_{k,n}+Kf_{k,k}-K\sum_{n=0}^{\smash{k}}f_{k,n}\\
 & =-Kr_{k,k}+\sulut{K-1}\mathcal{R}_{k}+Kf_{k,k}-Kl_{k}
\end{align*}
Here the excess term $-Kr_{k,k}$ simplifies and cancels $Kf_{k,k}$: 
\begin{align*}
-Kr_{k,k} & =-\sum_{h=0}^{k+1}f_{h,k+1}+\sum_{h=0}^{k+1-1}f_{h,k+1}=\\
 & =-f_{k+1,k+1}-\sum_{h=0}^{k}f_{h,k+1}+\sum_{h=0}^{k}f_{h,k+1}=-Kf_{k,k}
\end{align*}
Hence, we conclude $\sulut{K{-}1}\mathcal{R}_{k}-Kl_{k}=0$. Now the final propagation to difference gives $\sulut{K-1}\sulut{\mathcal{R}_{k}-\mathcal{L}_{k}}=0$. The proof finishes routinely.
\end{examplex}

\begin{examplex}
Abel generalized the binomial formula on the limit $\frac{a}{h},\frac{b}{h}\to\infty$ as
\[
\sulut{a+b}^{h}={\displaystyle \sum_{n=0}^{h}}\binom{h}{n}a\sulut{a-n}^{n-1}\sulut{b+n}^{h-n}
\]
\label{Abel}We must propagate the recurrence $\sulut{K-c}c^{k}=0$ of the powers $c^{k}$ to their three substitution instances $\sulut{a+b}^{h}$, $\sulut{a-n}^{n-1}$, and $\sulut{b+n}^{h-n}$. We will go through the last
instance in detail and just state the results of the first two easier ones:
\[
\left.\begin{array}{r}
H-a-b\\
A-B
\end{array}\right\} \sulut{a+b}^{h}=0 \qquad \sulut{AN-a+n}\sulut{a-n}^{n-1}=0
\]
For the substitution $\left\{ c\mapsto b+n,k\mapsto h-n\right\} $, we put together the defining relations~(\ref{eqn:defining_relation_comp_shift}) of the composite shifts $B,N,H$ and the initial recurrence $\sulut{K-c}c^{k}=0$:
\[
B-C\qquad NK-C\qquad H-K\qquad K-c
\]
We must eliminate $C$ and $K$, which is readily achieved by rewriting by $B-C$ and $K-c$. Since
$N$ is $K^{-1}C$, we have $Nc=\sulut{c+1}N$. Hence we derive from $\sulut{c+1}N-B$ and $H-c$ that the substitution transforms to 
\[
\left.\begin{array}{r}
\sulut{b+n+1}N-B\\
H-b-n
\end{array}\right\} \sulut{b+n}^{h-n}=0
\]

\begin{sloppypar}
Now consider $a\sulut{a-n}^{n-1}$. Without the factor $a$, the interpretation of $\sulut{a-n}^{n-1}$ for $a=n=0$ is undefined, but with it we can define $0\sulut{0-0}^{0-1}=0^{0}=1$ so that it is compatible with the recurrence below. Let $f_{a,n}=\sulut{a-n}^{n-1}$ and $g_{a,n}=a\sulut{a-n}^{n-1}$. Eliminating $f_{a,n}$ from $\{ \sulut{AN-a+n}f_{a,n}=0{,}\allowbreak\; af_{a,n}=g_{a,n}\} $ gives 
\[
\sulut{aAN-\sulut{a+1}\sulut{a-n}}g_{a,n}=0
\]
\end{sloppypar}

Next, let us consider the product $a\sulut{a-n_{1}}^{n_{1}-1}\cdot\sulut{b+n_{2}}^{h-n_{2}}$ where we have renamed the variables $n$ apart. After introducing the compound shift $N=N_{1}N_{2}$, we proceed to eliminate $N_{1}$ and $N_{2}$ from 
\[
aAN_{1}-\sulut{a+1}\sulut{a-n_{1}}\quad\begin{array}{c}
\sulut{b+n_{2}+1}N_{2}-B\\
H-b-n_{2}
\end{array}\quad N_{1}N_{2}-N
\]
The operator $H-b-n_{2}$ is good as is and does not interfere with the rest of the computation if $H>b,n_{2}$ w.r.t.\ the monomial order. From $\sulut{b+n_{2}+1}N_{2}-B$ and $N_{1}N_{2}-N$ we derive $BN_{1}-\sulut{b+n_{2}+1}N$, whose superposition with $aAN_{1}-\sulut{a+1}\sulut{a-n}$ eliminates $N_{1}$. We conclude 
\[
\left.\begin{array}{r}
H-b-n\\
a\sulut{b+n+1}AN-\sulut{a+1}\sulut{a-n}B
\end{array}\right\} a\sulut{a-n}^{n-1}\sulut{b+n}^{h-n}=0
\]

Unlike before, in this example we do need to use the plurality of the recurrences of the binomial coefficient $\binom{h_{1}}{n_{1}}$. A Gröbner basis of its annihilators is given by 
\[
\sulut{h_{1}+1-n_{1}}H_{1}-h_{1}-1\qquad\sulut{n_{1}+1}N_{1}-h_{1}+n_{1}\quad N_{1}H_{1}-N_{1}-1
\]
To these we add recurrences of $a\sulut{a-n_{2}}^{n_{2}-1}\sulut{b+n_{2}}^{h_{2}-n_{2}}$ and composite shifts:
\[
H_{2}-b-n_{2}\qquad a\sulut{b+n_{2}+1}AN_{2}-\sulut{a+1}\sulut{a-n_{2}}B\qquad N_{1}N_{2}-N\qquad H_{1}H_{2}-H
\]
We must eliminate $N_{1},N_{2},H_{1},H_{2}$. From the leftmost \textquotedblleft $H$ polynomials\textquotedblright{} and $H_{1}H_{2}-H$ we get $\sulut{h_{1}+1-n_{1}}H-\sulut{h_{1}+1}\sulut{b+n_{2}}$. Similarly, from the middle \textquotedblleft $N$ polynomials\textquotedblright{}, we get $a\sulut{b{+}n_{2}{+}1}\sulut{n_{1}{+}1}AN-\sulut{h_{1}{-}n_{1}}\sulut{a{+}1}\sulut{a{-}n_{2}}B$. Finally, from $N_{1}H_{1}-N_{1}-1$ and all the four polynomials on the second line, we get $a\sulut{H-b-n_{2}-1}AN-\sulut{a+1}\sulut{a-n_{2}}B$. So 
\[
\begin{array}{@{}c@{}}
\\
\\
\\
\end{array}\smash{\left.\begin{array}{@{}c@{}}
\\
\sulut{h+1-n}H-\sulut{h+1}\sulut{b+n}\\
a\sulut{b+n+1}\sulut{n+1}AN-\sulut{h-n}\sulut{a+1}\sulut{a-n}B\\
a\sulut{H-b-n-1}AN-\sulut{a+1}\sulut{a-n}B\\
\\
\end{array}\right\}\textstyle\binom{h}{n}a\sulut{a{-}n}^{n-1}\sulut{b{+}n}^{h-n}\;{=}\;0}
\]

Next, to propagate to summation, we must eliminate $n$. The first operator can be written $-\sulut{H+h+1}\boldsymbol{n}+\sulut{h+1}\sulut{H-b}$. The last operator can be written $\sulut{\sulut{a+1}B-aAN}\boldsymbol{n}+aAN\sulut{H-b}-a\sulut{a+1}B$. Since $H+h+1$ and $\sulut{a+1}B-aAN$ commute, eliminating $n$ yields at least 
\begin{gather*}
\sulut{\sulut{a+1}B-aAN}\sulut{h+1}\sulut{H-b}+\sulut{H+h+1}\sulut{aAN\sulut{H-b}-a\sulut{a+1}B}=\\
=aANH\sulut{H-b}-a\sulut{a+1}BH+\sulut{a+1}B\sulut{h+1}\sulut{H-a-b}=\\
=\sulut{N-1}{\color{gray}aAH\sulut{H{-}b}}+{\color{gray}a\sulut{a{+}1}H}\sulut{A-B}+{\color{gray}\sulut{aAH{+}\sulut{a{+}1}B\sulut{h{+}1}}}\sulut{H-a-b}
\end{gather*}
Here $N-1$ vanishes in propagation, and $A-B$ and $H-a-b$ are annihilators of $\sulut{a+b}^{h}$, while irrelevant factors are shown in gray. We omit the excess term computation because bounds are natural as for
Vandermonde's convolution formula (Example~\ref{Vandermonde}).

So the leading monomial from one recurrence of the entire difference can be chosen to be $aAH^{2}$. This leaves as base cases the three specializations $a=0$, $h=0$, and $h=1$. The first case also takes care of the invertibility of $a$ in $aAH^{2}$. The cases $h=0$ and $h=1$ can be easily symbolically evaluated. When $a=0$, we must detect that $a\sulut{a-n}^{n-1}=\delta_{0,n}$ (maybe by its recurrence), which again makes the sum finite. Alternatively, we could treat $a$ as a rational expression indeterminate and hence make $aA$ unconditionally invertible. Both of these tricks are beyond the scope of our procedure.
\end{examplex}

\end{rep}

\section{Related Work}
\label{sec:related-work}

\looseness=-1
Holonomic sequences \cite{basicholo} are closely related to our work.
Unlike our approach, which allows infinitely many
base cases as long as they are finitely representable 
(Sect.~\ref{sec:induction}), they are
limited to a finite number of base cases. Relaxing this limitation
yields approximately the homogeneous version of our propagation procedure
(i.e., without excess terms), whose theory Chyzak, Kauers, and Salvy laid out \cite{close}. Heterogeneity amounts to module Gröbner bases \cite{moduleGB-03,moduleGB-18,moduleGB-20}.
Its integration into propagations makes elementary identities about general sequences automatically provable, which may be of interest for general-purpose theorem provers.

In practice, hypergeometric sums are common holonomic sequences that have much faster algorithms available. Gosper's indefinite summation \cite{Gosper} can be applied to compute Wilf--Zeilberger pairs \cite{WZcert}, which offer compact proof certificates for definite sum identities. These fast methods admit generalizations to the full holonomic setting. See Koutschan's thesis \cite{MathematicaHolo} for an overview.

\begin{rep}
Holonomic functions have a nearly dual theory where differential equations with polynomial coefficients play the role of recurrences. The above references present the discrete and continuous holonomic theories together, sometimes unified and generalized by the language of Ore polynomials \cite{Ore,holoOre}. We presented only the discrete case because current higher-order provers lack the theoretical groundwork needed to bootstrap usable differential algebra.

%Leave this for the implementation paper.
%Software:
%\begin{itemize}
%\item HOL Light -- Maxima bridge by Harrison \cite{HOL:WZ}
%\item Coq -- Mathematica by Mahboubi and Sibut-Pinote \cite{Coq}
%\item CASes e.g. Mathematica \cite{MathematicaHolo,inductPhD,MathematicaWZ}, Maple \cite{MapleWZ}
%\end{itemize}
\end{rep}

Finding a closed form instead of only checking it for a summation is a different but related task. A common approach is to perform a recurrence solving phase after recurrence computation, as in the Mathematica package Sigma~\cite{Sigma06,Sigma21}.

\section{Conclusion}
\label{sec:conclusion}

We presented a procedure for proving equations involving summations within an
automatic higher-order theorem prover. The procedure is inspired by
holonomic sequences and partly generalizes them. It expresses the problem as recurrences and \confrep{}{systematically }%
derives new recurrences from existing ones. In case of success, it shows
the induction step of a proof by induction, leaving the base cases to the
\confrep{}{theorem }prover.

As future work, we want to continue implementing the procedure in Zipperposition \cite{vukmirovic-et-al-2022-hot}.
We hope that the subsequent practical experiments help us to settle how side conditions of initial recurrences ought to be handled.

\let\Acksize=\small

\def\ackname{\Acksize Acknowledgment}
\paragraph{\textbf{\upshape\ackname.}}
{\Acksize

We thank Pascal Fontaine for his ideas on how to integrate our procedure into
SMT and tableaux.
We also thank Anne Baanen, Pascal Fontaine, Mark Summerfield, and the anonymous
reviewers for suggesting improvements.

Nummelin and Blanchette's research has
received funding from the Netherlands Organization for Scientific Research (NWO)
under the Vidi program (proj\-ect No.\ 016.Vidi.189.037, Lean Forward).
%
Dahmen's research has
received funding from the NWO
under the Vidi program (proj\-ect No.\ 639.032.613, New Diophantine Directions).

}

\bibstyle{splncs04}
\bibliography{bib}

\end{document}
