%% LyX 2.3.6.1 created this file.  For more info, see http://www.lyx.org/.
%% Do not edit unless you really know what you are doing.
\documentclass[english]{article}
\usepackage[T1]{fontenc}
\usepackage[latin9]{inputenc}
\setcounter{tocdepth}{2}
\usepackage{xcolor}
\usepackage{mathtools}
\usepackage{enumitem}
\usepackage{amsmath}
\usepackage{amsthm}
\usepackage{amssymb}
\usepackage{setspace}
\usepackage{xargs}[2008/03/08]
\setstretch{0.8}

\makeatletter
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Textclass specific LaTeX commands.
\newlength{\lyxlabelwidth}      % auxiliary length 
\def\Layout#1 #2.{\theoremstyle{#1}\newtheorem{#2}[theoremx]{\expandafter\protect\csname#2name\endcsname}}
\theoremstyle{plain}
\newtheorem{theoremx}{\protect\theoremname}[section]
\Layout definition example.
\Layout definition definition.
\Layout remark remark.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% User specified LaTeX commands.
\def\unq@#1=00#2#3#4#5#6&#7&#8&{\csname#4#5\endcsname#6&#7#1&#8&}
\def\def@#1#2#3{\expandafter\def\csname#1#2\endcsname#3}
\def\?#1#2#3{\def@#1#2{##1&##2&##3&{\unq@##1&#3&}}}
\?10{#2\text{-}&#3}
\?23{#2\#&#3}
\?25{#2\%&#3}
\?3D{#2=&#3}
\?5B{#2[&#3}
\?5D{#2]&#3}
\?7B{&#2&#3}
\?7D{#3{#2}}
\?C4{#2\"A&#3}
\?D6{#2\"O&#3}
\?E4{#2\"a&#3}
\?F6{#2\"o&#3}
\def@00{&#1&&{#1}}
\def@24{#1 #2&#3&{\expandafter\rec@\csname#1\endcsname#2&#3&}}
\def\rec@#1#2&#3&{\unq@#2&#3#1&}
\def\label@in@display#1{\tag*{{\large$\scriptstyle(\unq@#1 =000000&&&)$}}\gdef\df@label{#1}}

\setlength{\emergencystretch}{1.5em}
\onehalfspacing
\delimiterfactor=547
\delimitershortfall=99pt
\let\oldleft\left
\let\oldright\right 
\def\left{\mathopen{}\mathclose\bgroup\oldleft}
\def\right{\aftergroup\egroup\oldright}

%\usepackage{newtxmath}
\usepackage{graphicx}
\usepackage{xcolor}
\usepackage{hyperref}
\usepackage[mathcal]{euscript}
\usepackage{prftree}

\makeatother

\usepackage{babel}
\providecommand{\definitionname}{Definition}
\providecommand{\examplename}{Example}
\providecommand{\remarkname}{Remark}
\providecommand{\theoremname}{Theorem}

\begin{document}
\noindent\begin{minipage}[t]{1\columnwidth}%
\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\,\vphantom{\overset{o}{O}}\middle|\,#2\right\}  }%

\global\long\def\url#1{\text{\href{#1}{#1}}}%

\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}}}%
%
\end{minipage}

\let\disjunction\vee \def\vee{\mathrel{\disjunction}}

\global\long\def\link#1#2{\hyperref[#2]{#1}}%

\global\long\def\simprule#1#2{\begin{array}{c}
\negthickspace#1\negthickspace\\
\hline\hline \negthickspace#2\negthickspace
\end{array}}%

\global\long\def\mgux{\makeop{mgu}^{\times}}%
\global\long\def\csu{\makeop{CSU}^{\times}}%


\section{Motivation}

Equations involving indexed summations are an ubiquitous topic in mathematics. Our goal here is to automate proofs involving these summations. Support of such automation is relatively scarce because summation cannot be directly expressed in first-order logic. A major exception is the case of hypergeometric summation (binomial coefficient type summation) and further the theory of holonomic sequences.

Gosper first presented a method to find closed hypergeometric form of an indefinite sum $\sum_{n=0}^{m}f_{n}$ of a hypergeometric sequence $f_{n}$ \cite{Gosper}. That is an exploration tool while the resulting equation is simple to verify. Wilf and Zeilberger then used this in their WZ pairs method \cite{WZcert} to certify definite hypergeometric summations such as the binomial theorem $\sum_{n\in\mathbb{Z}}\binom{m}{n}a^{n}b^{m-n}=\sulut{a+b}^{m}$. Here the gain is now in automating even difficult proofs. Sacrificing some efficiency a theoretically more widely applicable alternative comes from the theory of multivariate holonomic sequences \cite{basicholo}. These are functions defined by linear recurrences with polynomial coefficients and finitely many initial values.

Due to its power and simplicity I took the holonomic approach as the basis of my work. The arithmetic it requires generalizes immediately to commutative groups and rings. This is a reasonable setting for the sort of general automation I try to create. Whereas holonomic sequences provide a decision procedure for equality, I work in the context of incomplete definitions (like \cite{close}). Consequently there's no simple description of the problems my method solves on its own but as an add-on to superposition calculus it trivially preserves completeness.

The core reasoning could be cast in terms of generalized Gröbner-bases but I prefer superposition calculus and its terminology (terms, inferences, saturation,...) Moreover I implement the method in Zipperposition \cite{Zip} which is a higher-order superposition prover \cite{HOsup}. In this context terms with summations, such as $\sum_{n=a}^{b}n$, need no special introduction. Right now things of section \ref{Propagations} are implemented while only minimal demo functionality from section \ref{Integration} is working. Proof reconstruction in Isabelle is uncharted territory.

\section{Preliminaries}
\begin{itemize}
\item Here polynomials are non-commutative by default. Though we still ask commutation relations for indeterminates, e.g. $XY-YX=X$ in a ring $\mathbb{Z}\left[X,Y\right]$. Theoretical basis is that of Ore-polynomials \cite{Ore}.
\item The procedure works with symbolic equations. I write them using $\approx$ to distinguish them from meta reasoning (=). So $P\approx0$ is something to save for later, except that if $P=0$, it is a triviality.
\item Monomial order $\preccurlyeq$ in the sense of Gröbner-bases is a well-founded order on standard commutative monomials s.t. multiplication is increasing meaning $M\preccurlyeq M'\Rightarrow NM\preccurlyeq NM'$ for all monomials $M,M',N$.
\item Monomial order for generalized Gröbner-bases is the same except that non-commutative monomials are not closed under multiplication (when normalized). Hence \textquotedblleft multiplication is increasing\textquotedblright{} only upto leading (largest) monomials.
\end{itemize}

\section{Reasoning with recurrences \label{Propagations}}

We consider sequences and functions defined by linear finite-step recurrence equations, and we try to automate proofs about their indexed sums. Examples of such sequences:
\begin{itemize}
\item Fibonacci numbers $F_{n+2}-F_{n+1}-F_{n}=0$ for $n\geq0$ with $F_{0}=0$ and $F_{1}=1$.
\item Polynomials $P$ because for $d=\makeop{deg}P+1$ and every $n$ holds
\[
P\sulut n-\binom{d}{1}P\sulut{n-1}+\binom{d}{2}P\sulut{n-2}\pm...+\sulut{-1}^{d}P\sulut{n-d}=0.
\]
\item Sums $S_{m}=\sum_{n=0}^{m}f_{n}$ upto fresh variable because $S_{m+1}-S_{m}=f_{m+1}$ for $m\geq0$.
\item Exponentials: $b^{n+1}=b\cdot b^{n}$ for $n\geq0$ with $b^{0}=1$.
\item Factorial: $\sulut{n+1}!=\sulut{n+1}\cdot n!$ for $n\geq0$ with $0!=1$.
\end{itemize}
In fancier words the definitional facts we can use are multivariate inhomogeneous linear finite-step equations with polynomial coefficients. A prototypical example is $\sulut{n^{2}+1}f_{m+2}^{n+1}+mf_{m+1}^{n}-nmf_{m}^{n+1}=h_{m}^{n}$ where $f$ and $h$ are symbolic sequences and $n,m$ integer variables. Such equations make sense with values in any ring or commutative group which is our assumed setting.

We use the techniques of the theory of holonomic sequences to work with the recurrences. That is for every \emph{composite} term\textemdash addition, product or indexed sum of simpler terms\textemdash we try to find a linear recurrence from the recurrences of its parts. This works upwards from non-composite, \emph{atomic}, terms whose recurrences need to be given.
\begin{example}
\label{indefinite sum ex.}Consider task of proving $\sum_{n=0}^{m}f_{n}=g_{m}+f_{0}$ given $g_{0}=0$ and $g_{m+1}=g_{m}+f_{m+1}$.

We write this canonically as an equation to zero: $g_{m}+f_{0}-\sum_{n=0}^{m}f_{n}=0$. Atomic terms are $f$ and $g$. One way of piecing up the composite expression is to give names $h_{m}=g_{m}+f_{0}$, $F_{m}=\sum_{n=0}^{m}f_{n}$, and $E_{m}=h_{m}-F_{m}$. We then proceed to find recurrences for $h$, $F$ and $E$ from the given recurrence $g_{m+1}-g_{m}-f_{m+1}=0$ of $g$.

Recurrence of $h$: We defined $h$ in terms of $g$ (and constant $f_{0}$). Hence we want to eliminate $g$ from the equations. We use superposition-style reasoning with $g$ being largest symbol.
\[
\begin{array}{cll}
 & g_{m+1}-g_{m}-f_{m+1} & {\color{gray}=0}\\
-\quad & g_{m\phantom{{}+1}}+f_{0}-h_{m} & {\color{gray}=0}\mathrlap{\s\left[m\mapsto m+1\right]}\\
\hline  & -g_{m}-f_{m+1}-f_{0}+h_{m+1} & {\color{gray}=0}\\
+\quad & \phantom{-}g_{m}+f_{0}-h_{m} & {\color{gray}=0}\\
\hline  & h_{m+1}-h_{m}-f_{m+1} & {\color{gray}=0}
\end{array}
\]

Recurrence of $F$: Obviously $F_{m+1}-F_{m}=f_{m+1}$. Formally we derive this by considering how the index set $\left[0,m\right]$ changes when $m$ changes. When $m\geq0$ we get $\left[0,m\right]\setminus\left[0,m+1\right]=\varnothing$ and $\left[0,m+1\right]\setminus\left[0,m\right]=\left\{ m+1\right\} $ so
\[
F_{m+1}-F_{m}=\sum_{n\in\left\{ m+1\right\} }f_{n}-\sum_{n\in\varnothing}f_{n}=f_{m+1}.
\]

Recurrence of $E$: Since $E_{m}=h_{m}-F_{m}$ is defined by $h$ and $F$, we eliminate $h$ and $F$ with the help of their recurrences.
\begin{align*}
0 & =h_{m}-F_{m}-E_{m} & \sulut 1 & \text{ by definition}\\
0 & =h_{m+1}-h_{m}-f_{m+1} & \sulut 2 & \text{ recurrence of }h\\
0 & =F_{m+1}-F_{m}-f_{m+1} & \sulut 3 & \text{ recurrence of }F\\
0 & =-F_{m+1}-E_{m+1}+h_{m}+f_{m+1} & \sulut 4 & \text{ as }\sulut 1\left[m\mapsto m+1\right]-\sulut 2\\
0 & =h_{m}-E_{m+1}-F_{m} & \sulut 5 & \text{ as }\sulut 4+\sulut 3\\
0 & =-E_{m+1}+E_{m} & \sulut 6 & \text{ as }\sulut 5-\sulut 1
\end{align*}
Hence $E_{m+1}=E_{m}$ and by induction, to prove the claim $E_{m}=0$ for $m\geq0$, it now suffices to prove the trivial base case $E_{0}=0$.
\end{example}

\subsection{Propagation to addition \label{Plus}}

We introduce formal notation for the equations we make use of to better communicate possibilities and limits. A basic recurrence has the form $R_{1}f_{1}+...+R_{k}f_{k}\approx0$. Here each $f_{j}$ is a sequence (or like) term whose fine structure is ignored in calculations making $f_{j}$ like an atomic constant. Instead the operator polynomials $R_{j}$ carry a rich fine structure that is defined below. Finally the $\approx$ hints that this is data in the algorithm instead of an explanation or a calculation step.
\begin{definition}
Operator polynomials are non-commutative polynomials over $\mathbb{Z}$ spanned by indeterminates of two types: multiplication and shift. Operator polynomials operate on sequences and the like functions with values in a commutative group by mapping them to other such functions. This operation is naturally extended from the operation of the indeterminates:

The $j$\textsuperscript{th} multiplication indeterminate, say $n_{j}$, operates to a function $f$ by multiplication by the $j$\textsuperscript{th} coordinate: $\sulut{n_{j}f}\sulut{...,\makeop n_{j},...}=\makeop n_{j}\cdot f\sulut{...,\makeop n_{j},...}$.

The $j$\textsuperscript{th} shift indeterminate, say $N_{j}$, operates to a function $f$ by shifting it in the direction of the $j$\textsuperscript{th} coordinate: $\sulut{N_{j}f}\sulut{...,\makeop n_{j},...}=f\sulut{...,\makeop n_{j}+1,...}$.

Compatibly with the operation action the indeterminates commute except that
\[
N_{j}n_{j}=\sulut{n_{j}+1}N_{j}=n_{j}N_{j}+N_{j}.
\]
\end{definition}
Conventionally I use the same lower case letter for a variable and its multiplier, and the corresponding upper case letter for the shift indeterminate. For example I expand the (non-)commutation relation as 
\[
\sulut{Mmf}_{m}=\sulut{mf}_{m+1}=\sulut{m+1}f_{m+1}=\sulut{m+1}\sulut{Mf}_{m}=\sulut{\sulut{m+1}Mf}_{m}.
\]

An equation is a sum of monomials equal to zero. A monomial has the form $c\cdot n_{1}^{a_{1}}...n_{k}^{a_{k}}\cdot N_{1}^{b_{1}}...N_{k}^{b_{k}}f$ where $c\in\mathbb{Z}$, $a_{j},b_{j}\in\mathbb{N}$, and $f$ is a sequence term. An equation set can be saturated\textemdash ignoring the fine structure of the sequence terms\textemdash by a (generalized) Gröbner-basis computation. Saturation with eager simplification terminates by the standard argument: The ideal spanned by reducible monomials in the plain commutative polynomial ring $\mathbb{Z}\left[n_{1},...,n_{k},N_{1},...,N_{k}\right]$ increases as new recurrences are found but the ring is Noetherian \cite{wiki:stop}. To each sequence term $f$ corresponds a different ideal but there is only a finite number of them.

Assume that in a formula that we try to prove occurs sequence-like sub-expressions $f_{n}$, $g_{n}$ and $f_{n}+g_{n}$. We then introduce a convenience name $h\approx f+g$ and propagate recurrences of $f$ and $g$ to $h$.
\begin{definition}
Propagation to addition is accomplished as follows. Let $f$ and $g$ be the relevant terms and let $h$ be the formal name of their addition $f+g$. Let $F$ be the set of recurrences involving $f$, and $G$ be those involving $g$. Eliminate $f$ and $g$ from the recurrences $F\cup G\cup\left\{ h\approx f+g\right\} $ by saturating them w.r.t. an order making $f$- and $g$-monomials larger than others. The recurrences of $h$ are then those which contain $h$ but no $f$ nor $g$. Propagation to repeated and weighted addition (e.g. $2f-g+1$) is achieved similarly.
\end{definition}
In the previous example \ref{indefinite sum ex.} it seemed obvious to do simple induction, and so the presented solution seems cumbersome. However if we had assumed $g_{n+2}=g_{n}+f_{n+1}+f_{n+2}$ with $g_{0}=0$ and $g_{1}=f_{1}$, a less simple induction with step size of 2 would have been needed. With recurrences the step size is a by-product of the computation, that can be read off from the final recurrence. You can see that in this adapted propagation to addition step:
\begin{example}
Let $N^{2}g-g-N^{2}f-Nf\approx0$, $NF-F-Nf\approx0$ and $E\approx g+f_{0}-F$ where $N$ is the shift indeterminate. We find recurrence of $E$ by eliminating $g$ and $F$. Maximal terms\textemdash which we cancel on each inference\textemdash are in bold.
\[
\begin{array}{lll}
 &  & \boldsymbol{N^{2}g}-g-N^{2}f-Nf\\
-N^{2} &  & \boldsymbol{g}-F-E+f_{0}\\
\hline  &  & -g-N^{2}f-Nf+\boldsymbol{N^{2}F}+N^{2}E-f_{0}\\
-N &  & \boldsymbol{NF}-F-Nf\\
\hline  &  & -g-Nf+N^{2}E-f_{0}+\boldsymbol{NF}\\
- &  & \boldsymbol{NF}-F-Nf\\
\hline  &  & -\boldsymbol{g}+N^{2}E-f_{0}+F\\
+ &  & \boldsymbol{g}-F-E+f_{0}\\
\hline  &  & \boldsymbol{N^{2}E}-E
\end{array}
\]
So $E_{n+2}=E_{n}$ which immediately tells that the induction needs a step size of 2. Especially 2 base cases $n=0$ and $n=1$ remain to be checked.
\end{example}

\subsection{Propagation to summation \label{Sum}}

A summation is a term of the form $\Sigma_{D}f$ where $\Sigma$ is an interpreted function symbol, $D$ is a term representing the domain of summation, and the summand $f$ is a sequence term. We mostly write this in different notations, for example $\sum_{j\in D_{n}}f_{n,j}$ to make the variables explicit.
\begin{definition}
Propagation of recurrences to summation $\Sigma_{D}f$ of a sequence term $f$ proceeds in three steps. First we determine \emph{bad} indeterminates that cannot be pulled out of the sum. Multiplication by the summation variable is always one of them whereas other variables always commute with $\Sigma_{D}$. Badness of shifts depends on $D$ and involves computing error terms. Next we eliminate the bad indeterminates from recurrences of $f$ by saturation. Then recurrences of $\Sigma_{D}f$ can be computed from those of $f$ and error terms of shifts.

For the shift indeterminate $S$ corresponding to the summation variable we have
\[
\sum_{D}\sulut{S-1}g=\sum_{\sulut{D+1}\setminus D}g-\sum_{D\setminus\sulut{D+1}}g=:Eg
\]
where $D+1=\set{d+1}{d\in D}$. If the sets $\sulut{D+1}\setminus D$ and $D\setminus\sulut{D+1}$ can be enumerated (see section \ref{Enumerate}), then the error $E$ becomes an evaluation of $g$ on an explicit set of terms to be substituted to the summation variable. In such case $S$ is \emph{nearly $D$-bijective.}

For any other shift indeterminate $N$ with corresponding variable $n$ we have 
\[
\sum_{D_{n}}Ng_{n}-N\sum_{D_{n}}g_{n}=\sum_{D_{n}}g_{n+1}-\sum_{D_{n+1}}g_{n+1}=\sum_{\mathclap{D_{n}\setminus D_{n+1}}}g_{n+1}-\sum_{\mathclap{D_{n+1}\setminus D_{n}}}g_{n+1}=:\widetilde{N}g_{n}.
\]
If the sets $D_{n}\setminus D_{n+1}$ and $D_{n+1}\setminus D_{n}$ can be enumerated, then also this error $\widetilde{N}$ becomes an explicit evaluation as above. In such case $N$ is \emph{nearly} \emph{$D_{n}$-commutable. }This can be iterated to calculate commutation errors $\widetilde{P}g:=\sum_{D}Pg-P\sum_{D}g$ for polynomials $P$ of $N$.

A shift indeterminate is bad if it is not nearly bijective or commutable. Let $P\sulut S$ be a polynomial missing bad indeterminates, viewed as a function of (possibly bad and missing) shift $S$ w.r.t. the summation variable. Since multiplication by the summation variable is bad, $S$ commutes with indeterminates in $P\sulut S$. Hence we can uniquely write $P\sulut S=\sulut{S-1}Q\sulut S+P\sulut 1$ by polynomial long division. Now a recurrence $P\sulut Sf\approx0$ of $f$ can be pulled over $\sum_{D}$ as follows:
\begin{align}
{\textstyle \sum_{D}}P\sulut Sf & ={\textstyle \sum_{D}}\sulut{\sulut{S-1}Q\sulut S+P\sulut 1}f &  & \text{polynomial division}\nonumber \\
 & =EQ\sulut Sf+{\textstyle \sum_{D}}P\sulut 1f &  & \text{near bijectivity}\label{=000024varSigma =000024! P=000024! =000024! =000024to =000024! P=000024! =000024varSigma}\\
 & =EQ\sulut Sf+\widetilde{\smash{P\sulut 1}}f+P\sulut 1{\textstyle \sum_{D}}f &  & \text{near commutation repeated}\quad\quad\nonumber 
\end{align}
\end{definition}
\begin{remark}
If the sum ranges over all integers, then both bijectivity and commutation errors vanish. For an infinite sum to make sense its summand must have a finite support. For example $\binom{m}{n}=0$ unless $0\leq n\leq m$ which implies an extensibility $\sum_{n=0}^{m}\binom{m}{n}f_{n,m}=\sum_{n\in\mathbb{Z}}\binom{m}{n}f_{n,m}$ assuming $f$ is extensible. Justifying such extension is often easier than cancelling the error terms (see example \ref{Fibonacci}).
\end{remark}
\begin{example}
\[
\sum_{m=0}^{k}\sum_{n=0}^{m}f_{m,n}=\sum_{n=0}^{k}\sum_{m=n}^{k}f_{m,n}
\]
\label{swap nested}First consider the left hand side $\mathcal{L}_{k}=\sum_{m=0}^{k}l_{m}=\sum_{m=0}^{k}\sum_{n=0}^{m}f_{m,n}$ where we have named summand as $l_{m}$. Obviously $\sulut{K-1}l_{m}\approx0$ with $K$ denoting a shift w.r.t. $k$. This recurrence has no multiplication by $m$ so we directly proceed to pull it over $\sum_{m=0}^{k}$ to get a recurrence for $\mathcal{L}_{k}$. No shift w.r.t. $m$ is present either so we skip near bijectivity. Near commutation error for $K$ is (when $k\geq0$)
\[
\sulut{\sum_{m=0}^{k}K-K\sum_{m=0}^{k}}l_{m}=\sum_{m\in\left[0,k\right]\setminus\left[0,k+1\right]}l_{m}-\sum_{m\in\left[0,k+1\right]\setminus\left[0,k\right]}l_{m}=-l_{k+1}.
\]
Hence $\sulut{K-1}\mathcal{L}_{k}-Kl_{k}\approx0$, which is a conclusion of the following specialization of the generic derivation \ref{=000024varSigma =000024! P=000024! =000024! =000024to =000024! P=000024! =000024varSigma}
\[
0=\sum_{m=0}^{k}0\approx\sum_{m=0}^{k}\sulut{Kl_{m}-l_{m}}=K\sum_{m=0}^{k}l_{m}-l_{k+1}-\sum_{m=0}^{k}l_{m}=\sulut{K-1}\mathcal{L}_{k}-Kl_{k}.
\]

Next consider the right hand side $\mathcal{R}_{k}=\sum_{n=0}^{k}r_{k,n}=\sum_{n=0}^{k}\sum_{m=n}^{k}f_{m,n}$. Obviously $\sulut{K-1}f_{m,n}\approx0$ and like above this propagates to $\sulut{K-1}r_{k,n}-Kf_{k,n}\approx0$. The second propagation from $r_{k,n}$ to $\mathcal{R}_{k}$ is also very similar but here we can observe how near commutation error duplicates a parameter:
\[
\sulut{\sum_{n=0}^{k}K-K\sum_{n=0}^{k}}a_{k,n}=\sum_{n\in\left[0,k\right]\setminus\left[0,k+1\right]}a_{k+1,n}-\sum_{n\in\left[0,k+1\right]\setminus\left[0,k\right]}a_{k+1,n}=-Ka_{k,k}
\]
where $a$ is $r$ or $f$. With that $\sulut{K-1}r_{k,n}\approx Kf_{k,n}$ implies $\sulut{K-1}\mathcal{R}_{k}-Kr_{k,k}\approx Kl_{k}-Kf_{k,k}$ where name $l_{k}=\sum_{n=0}^{k}f_{k,n}$ is reused.

Finally we combine recurrences of $\mathcal{L}$ and $\mathcal{R}$ to get $\sulut{K-1}\sulut{\mathcal{L}_{k}-\mathcal{R}_{k}}\approx Kr_{k,k}-Kf_{k,k}$. The right hand side evaluates to 0 which is sufficient and necessary to using this recurrence to prove the induction step of $\mathcal{L}_{k}-\mathcal{R}_{k}=0\s\forall k\geq0$. The remaining base case $\mathcal{L}_{0}-\mathcal{R}_{0}=0$ is again easy as all the summations range over $\left\{ 0\right\} $.
\end{example}
The input problems, or at least the near commutation/bijectivity error terms, can introduce copies of the same sequence evaluated at different points. We focus on simple cases in which recurrences can be propagated. Consider replacing a sequence term $f_{m}$ by $g_{m,n}:=f_{m+an+b}$ where $n$ is a fresh variable and $a,b\in\mathbb{Z}$ are explicit constants. Every recurrence of $f$ translates to a recurrence of $g$ by substituting $m$ by $m+an+b$. Indeed $\sulut{m+1}+an+b=\sulut{m+an+b}+1$ implies that substitution $\left\{ m\mapsto m+an+b\right\} $ does not affect shifts in recurrences of $f_{m}$. Corresponding to an added variable $n$ we also find an additional equation $\sulut{N-M^{a}}g_{m,n}\approx0$ if $a>0$, or $\sulut{NM^{-a}-1}g_{m,n}\approx0$ if $a<0$. Here and below $M$ shifts $m$ and $N$ shifts $n$. General affine substitutions are treated in section \ref{Substitute}.
\begin{example}
\[
\sum_{n=0}^{m}f_{n}=\sum_{n=0}^{m}f_{m-n}
\]
Write $F^{m}$ for the left hand side, $G^{m}$ for right, and $g_{n}^{m}=f_{m-n}$. We have the trivial $\sulut{M-1}f_{n}\approx0$ that propagates to $\sulut{M-1}F^{m}-Mf_{m}\approx0$ as in previous example \ref{swap nested}. Next $g_{n}^{m}=f_{m+\sulut{-1}n+0}$ and as discussed above we find $\sulut{NM-1}g_{n}^{m}\approx0$. To propagate this we compute the relevant bijectivity and commutation errors:
\begin{align*}
\sum_{n=0}^{m}\sulut{N-1}a_{n}^{m} & =\sum_{n\in\left[1,m+1\right]\setminus\left[0,m\right]}a_{n}^{m}-\sum_{n\in\left[0,m\right]\setminus\left[1,m+1\right]}a_{n}^{m}=a_{m+1}^{m}-a_{0}^{m}\\
\sulut{\sum_{n=0}^{m}M-M\sum_{n=0}^{m}}a_{n}^{m} & =\sum_{n\in\left[0,m\right]\setminus\left[0,m+1\right]}a_{n}^{m+1}-\sum_{n\in\left[0,m+1\right]\setminus\left[0,m\right]}a_{n}^{m+1}=-Ma_{m}^{m}
\end{align*}
The first equation is used with $a_{n}^{m}=Mg_{n}^{m}$ and the second with $a_{n}^{m}=g_{n}^{m}$ in the calculation specialized from \ref{=000024varSigma =000024! P=000024! =000024! =000024to =000024! P=000024! =000024varSigma}
\begin{align*}
0 & \approx\sum_{n=0}^{m}\sulut{NMg_{n}^{m}-g_{n}^{m}}=g_{m+1}^{m+1}-g_{0}^{m+1}+\sum_{n=0}^{m}\sulut{Mg_{n}^{m}-g_{n}^{m}}\\
 & =g_{m+1}^{m+1}-g_{0}^{m+1}-Mg_{m}^{m}+\sulut{M-1}\sum_{n=0}^{m}g_{n}^{m}=\\
 & =-Mg_{0}^{m}+\sulut{M-1}G^{m}
\end{align*}
Hence $\sulut{M-1}G^{m}-Mg_{0}^{m}\approx0$. The final propagation gives $\sulut{M-1}\sulut{F^{m}-G^{m}}\approx M\sulut{f_{m}-g_{0}^{m}}$ where of course $f_{m}-g_{0}^{m}=0$. The proof finishes as in earlier examples.
\end{example}

\subsection{Propagation to operator polynomial \label{Poly}}
\begin{definition}
Given an operator polynomial $P$ and sequence term $f$ we propagate recurrences $F$ of $f$ to those of $Pf$ by giving it a formal name $h$ and eliminating $f$ from $F\cup\left\{ h\approx Pf\right\} $.
\end{definition}
This simple propagation step plays mostly a role of an optimization. It produces simpler recurrences than repeated propagations to addition and multiplication. Moreover we can already see how the proof method handles nontrivial computation before we dive into comparatively difficult case of multiplication.
\begin{example}
\begin{flalign*}
 &  & \sum_{y\in\mathbb{Z}}y^{2}\binom{x}{y} & =2^{x-2}x\sulut{x+1} & \text{(note: \ensuremath{{\textstyle y^{2}\binom{x}{y}=0}} unless \ensuremath{1\leq y\leq x})}
\end{flalign*}
\global\long\def\aidspace{\hspace{-10em}}%
 
\global\long\def\yless#1{-x^{2}#1X^{2}-2x#1X^{2}+2x^{2}#1X-#1X^{2}+5x#1X+x^{2}X-x^{2}#1+2#1X+4xX-3x#1-x^{2}+4X-2#1-3x-2}%
\begin{align*}
0 & \approx\sulut{X-2}2^{x} & \sulut 1 & \text{ by definition}\\
0 & \approx\sulut{{\color{blue}\sulut{x-y+1}X-x-1}}{\textstyle \binom{x}{y}} & \sulut 2 & \text{ standard property of }{\textstyle \binom{x}{y}}\\
0 & \approx\sulut{\sulut{y+1}Y-x+y}{\textstyle \binom{x}{y}} & \sulut 3 & \text{ standard property of }{\textstyle \binom{x}{y}}\\
 & \quad\quad\quad\textsl{Propagation}\\
0 & \approx g_{x}-{\textstyle \frac{1}{4}}\sulut{x^{2}+x}2^{x} & \sulut 4 & \text{ rename }2^{x-2}x\sulut{x+1}=:g_{x}\\
0 & \approx4Xg_{x}-\sulut{3xX+2X+2x^{2}}2^{x} & \sulut 5 & =x^{2}\sulut 1+4X\sulut 4\\
0 & \approx\sulut{xX-2x-4}g_{x} & \sulut 6 & \text{ by 1,4,5,... (multistep)}\\
\\
0 & \approx f_{y}^{x}-y^{2}{\textstyle \binom{x}{y}} & \sulut 7 & \text{ rename }y^{2}{\textstyle \binom{x}{y}}=:f_{y}^{x}\\
0 & \approx\sulut{{\color{blue}\sulut{x-y+1}X-x-1}}f_{y}^{x} & \sulut 8 & \text{ by 2,{\color{gray}3,}7 (multistep)}\\
0 & \approx\sulut{y^{2}Y-yx+y^{2}-x+y}f_{y}^{x} & \sulut 9 & \text{ by {\color{gray}2,}3,7 (multistep)}\\
\\
 & \aidspace\mathrlap{0\approx\sulut{\yless Y}f_{y}^{x}}\\
 &  & \sulut{10} & \text{ by 8,9 (eliminated \ensuremath{y})}\\
 & \aidspace\mathrlap{0\approx\sulut{\yless{\phantom{Y}\mathllap{{\color{red}\cdot\!1}}}}{\color{red}\Sigma_{y}}f_{y}^{x}}\\
 &  & \sulut{11} & \text{ since }\smash{{\textstyle \sum\limits _{y\in\mathbb{Z}}}}\circ\sulut{Y-1}=0\\
\\
0 & \approx h_{x}-\Sigma_{y}f_{y}^{x}+g_{x} & \sulut{12} & \text{ rename }\Sigma_{y}f_{y}^{x}-g_{x}=:h_{x}\\
0 & \approx\mathrlap{\sulut{-\sulut{x+1}{}^{2}X^{2}+3\sulut{x+1}\sulut{x+2}X-2\sulut{x+1}\sulut{x+2}}h_{x}}\\
 &  & \sulut{13} & \text{ by 6,11,12}
\end{align*}
Since the leading factor $-\sulut{x+1}^{2}\neq0$ for $x\geq0$, double step induction proves the claim upto the base cases $h_{0}=0$ and $h_{1}=0$.
\end{example}

\subsection{Propagation to product \label{Times}}

Consider sequence terms $f_{n}$ and $g_{m}$ with disjoint variable tuples $n$ and $m$. The recurrences of their pointwise product $f_{n}g_{m}$ are essentially a union of recurrences of $f_{n}$ and $g_{m}$. Namely if $Pf_{n}+E\approx0$ for an operator polynomial $P$ and some error terms $E$, then $P\sulut{f_{n}g_{m}}+E\cdot g_{m}\approx0$ (w.l.o.g. there's no $m$ in $P$ nor $E$). Similarly for $g_{m}$. Now propagation to product can be reduced to propagation to substitution.
\begin{definition}
Let $f_{n}$ and $g_{n}$ be sequence terms. Their recurrences are propagated to their pointwise product $f_{n}g_{n}$ by propagating to the substitution $\left\{ m\mapsto n\right\} f_{n}g_{m}=f_{n}g_{n}$ according to the next definition \ref{subs. prop. def.}. Here $m$ are a fresh copy of variables $n$. Recurrences of $f_{n}g_{m}$ are those of $f_{n}$ and $g_{m}$ multiplied by $g_{m}$ or $f_{n}$ respectively.
\end{definition}
Before considering general substitutions let's see what should be done in the special case of multiplication.
\begin{example}
Let $f_{n}=n_{1}^{n_{2}}$ and $g_{n}=\binom{n_{1}}{n_{2}}$. We will derive a recurrence of $f_{n}g_{n}$ from the standard recurrences 
\begin{align*}
0 & \approx\sulut{N_{2}-n_{1}}f_{n} & \sulut F\\
0 & \approx\sulut{M_{1}M_{2}-M_{2}-1}g_{m} & \sulut{\Delta} & \text{ Pascal's triangle}\\
0 & \approx\sulut{\sulut{m_{2}+1}M_{1}M_{2}-m_{1}-1}g_{m} & \sulut G & \text{ from }{\textstyle \binom{m_{1}}{m_{2}}=\frac{m_{1}}{m_{2}}\binom{m_{1}-1}{m_{2}-1}}
\end{align*}
(Unlike the purely stylistic factoring of $f_{n}$, $g_{m}$ etc., I will abuse the factoring of $m_{2}+1$ to shorten the derivation a bit.) Observe that any single shift in the final recurrence of $f_{n}g_{n}$ can be written 
\[
N_{j}\sulut{f_{n}g_{n}}=\sulut{N_{j}f_{n}}\sulut{N_{j}g_{n}}=\left\{ m\mapsto n\right\} \sulut{N_{j}f_{n}}\sulut{M_{j}g_{m}}=\left\{ m\mapsto n\right\} N_{j}M_{j}\sulut{f_{n}g_{m}}.
\]
Hence we can pull over $\left\{ m\mapsto n\right\} $ only and all the shift pairs $N_{j}M_{j}$ whereas other $N_{j}$'s and $M_{j}$'s we must eliminate. To this end we add name definitions 
\begin{align*}
0 & \approx\sulut{N_{1}M_{1}-\widetilde{N}_{1}}\sulut{f_{n}g_{m}} & \sulut 1\\
0 & \approx\sulut{N_{2}M_{2}-\widetilde{N}_{2}}\sulut{f_{n}g_{m}} & \sulut 2
\end{align*}
The new shift indeterminate $\widetilde{N}_{j}$ gets nontrivial commutation relations with both $n_{j}$ and $m_{j}$, namely $\widetilde{N}_{j}n_{j}=\sulut{n_{j}+1}\widetilde{N}_{j}$ and $\widetilde{N}_{j}m_{j}=\sulut{m_{j}+1}\widetilde{N}_{j}$. Let's shorten $h:=f_{n}g_{m}$ in the saturation eliminating $N_{j}$ and $M_{j}$:
\begin{align*}
0 & \approx\sulut{\sulut{m_{2}+1}M_{2}+m_{2}-m_{1}}h & \sulut 3 & =\sulut G-\sulut{m_{2}+1}\sulut{\Delta}\text{, simplification}\\
0 & \approx\sulut{n_{1}M_{2}-\widetilde{N}_{2}}h & \sulut 4 & =\sulut 2-n_{1}\sulut F\text{, simplification}\\
0 & \approx\sulut{\sulut{m_{2}+1}\widetilde{N}_{2}+n_{1}m_{2}-n_{1}m_{1}}h & \sulut 5 & =n_{1}\sulut 3-\sulut{m_{2}+1}\sulut 4
\end{align*}
Saturation must still consider all superpositions between (\emph{F}),($\Delta$),(1),(3),(4),(5), except the taken one of (3) and (4), but (5) will remain as the only equation without any $N_{j}$ or $M_{j}$. Applying the substitution $\left\{ m\mapsto n\right\} $ to it gives
\[
\sulut{\sulut{n_{2}+1}N_{2}+n_{1}n_{2}-n_{1}^{2}}\sulut{n_{1}^{n_{2}}\binom{n_{1}}{n_{2}}}\approx0.
\]
\end{example}

\subsection{Propagation to substitution \label{Substitute}}

\begin{definition}
\label{subs. prop. def.} Let $f_{m}$ be a sequence term with $m\in\mathbb{Z}^{d}$ and let $\sigma$ be an affine substitution sending $m_{k}$ to $\sum_{j=1}^{r}s_{kj}n_{j}+a_{k}$ where all $s_{kj},a_{k}\in\mathbb{Z}$ are explicit constants and $n_{j}$ are variables of the range of $\sigma$. Then for each shift $N_{j}$ in the range we have $N_{j}\sigma=\sigma M_{1}^{s_{1j}}...M_{d}^{s_{dj}}$. We propagate recurrences of $f_{m}$ to those of $\sigma f_{m}$ as follows.

We name $M_{1}^{s_{1j}}...M_{d}^{s_{dj}}$ as $\widetilde{N}_{j}$ by introducing the recurrences that make the exponents $s_{kj}$ non-negative: 
\[
\widetilde{N}_{j}\prod_{k:\s s_{kj}<0}M_{k}^{-s_{kj}}f_{m}\approx\prod_{k:\s s_{kj}\geq0}M_{k}^{s_{kj}}f_{m}\quad\text{for }j\in\left\{ 1,...,d\right\} .
\]
The new shift indeterminates $\widetilde{N}_{j}$ satisfy the commutation relations $\widetilde{N}_{j}m_{k}=\sulut{m_{k}+s_{kj}}\widetilde{N}_{j}$. With these we eliminate $M_{j}$'s in favor of $\widetilde{N}_{j}$'s from recurrences of $f_{m}$. All resulting equations that lack every $M_{j}$ give recurrences of $\sigma f_{m}$ under the operation of $\sigma$ due to the commutation relations $\sigma\widetilde{N}_{j}=N_{j}\sigma$ and $\sigma m_{k}=\sulut{\sum_{j=1}^{r}s_{kj}n_{j}+a_{k}}\sigma$.
\end{definition}
\begin{example}
\[
\sum_{n=0}^{m-1}\binom{n}{m-1-n}=F_{m}:=m^{\text{th}}\text{ Fibonacci number}
\]
\label{Fibonacci}For binomial coefficient we have recurrences $\sulut{NM-M-1}\binom{n}{m}\approx0$ and $\binom{n}{m}=\frac{n}{m}\binom{n-1}{m-1}$ or equivalently $\sulut{\sulut{m+1}NM-n-1}\binom{n}{m}\approx0$. We want to propagate these over the substitution $\sigma=\left\{ \sulut{n,m}\mapsto\sulut{n,m-1-n}\right\} $. We have $N\sigma=\sigma NM^{-1}$ and $M\sigma=\sigma M$. So we introduce the definitions
\begin{align*}
\sulut{\widetilde{N}M-N}{\textstyle \binom{n}{m}} & \approx0 & \sulut 1\\
\sulut{\widetilde{M}-M}{\textstyle \binom{n}{m}} & \approx0 & \sulut 2
\end{align*}
Next we eliminate $N,M$ in favor of $\widetilde{N},\widetilde{M}$. Here (2) immediately rewrites every $M$ to $\widetilde{M}$ and then (1) becomes $\sulut{-N+\widetilde{N}\widetilde{M}}\binom{n}{m}\approx0$ that rewrites every $N$. Consequently we end up with equations
\begin{align*}
\sulut{-M+\widetilde{M}}{\textstyle \binom{n}{m}} & \approx0 &  &  & f_{m}^{n}:={\textstyle \binom{n}{m-1-n}}\\
\sulut{-N+\widetilde{N}\widetilde{M}}{\textstyle \binom{n}{m}} & \approx0\\
\sulut{\widetilde{N}\widetilde{M}^{2}-\widetilde{M}-1}{\textstyle \binom{n}{m}} & \approx0 &  & \overset{\sigma}{\mapsto} & \sulut{NM^{2}-M-1}f_{m}^{n} & \approx0\\
\sulut{\sulut{m+1}\widetilde{N}\widetilde{M}^{2}-n-1}{\textstyle \binom{n}{m}} & \approx0 &  & \overset{\sigma}{\mapsto} & \sulut{\sulut{m-n}NM^{2}-n-1}f_{m}^{n} & \approx0
\end{align*}

Next we propagate the recurrence $\sulut{NM^{2}-M-1}f_{m}^{n}\approx0$\textemdash that readily lacks multiplier $n$\textemdash to summation $\sum_{n=0}^{m-1}$. Let's compute near bijectivity and commutation errors. Since the sum has natural boundaries (summand vanishes outside them), these will eventually reduce to 0. 
\begin{align*}
\sum_{n=0}^{m-1}\sulut{N-1}{\color{blue}a_{m}^{n}} & ={\color{blue}a_{m}^{m}-a_{m}^{0}}\\
\sulut{\sum_{n=0}^{m-1}M-M\sum_{n=0}^{m-1}}{\color{purple}a_{m}^{n}} & ={\color{purple}-a_{m+1}^{m}}
\end{align*}
\begin{align*}
0 & \approx\sum_{n=0}^{m-1}\sulut{NM^{2}f_{m}^{n}-Mf_{m}^{n}-f_{m}^{n}}\\
 & =\sum_{n=0}^{m-1}\sulut{N-1}{\color{blue}M^{2}f_{m}^{n}}+\sum_{n=0}^{m-1}\sulut{{\color{purple}M}^{2}{\color{purple}f_{m}^{n}}-M{\color{purple}f_{m}^{n}}-f_{m}^{n}}\\
 & ={\color{blue}f_{m+2}^{m}-f_{m+2}^{0}}+\sulut{{\color{purple}-f_{m+2}^{m}-f_{m+2}^{m+1}}}-\sulut{{\color{purple}-f_{m+1}^{m}}}+\sulut{M^{2}-M-1}\sum_{n=0}^{m-1}f_{m}^{n}\\
 & =-\binom{0}{m+1}-\binom{m+1}{0}+\binom{m}{0}+\sulut{M^{2}-M-1}\sum_{n=0}^{m-1}f_{m}^{n}
\end{align*}
Here $\binom{0}{m+1}=0$ and $\binom{m}{0}=1=\binom{m+1}{0}$ when $m\geq0$. The final propagation to difference hence gives $\sulut{M^{2}-M-1}\sulut{\sum_{n=0}^{m-1}f_{m}^{n}-F_{m}}\approx0$ and the claimed equality follows after checking two initial values.
\end{example}


\section{As part of superposition \label{Integration}}

\global\long\def\myrule{\textsc{Recurse}}%
The recurrence propagation method can be used in refutation of an inequation such as $\Sigma_{D}f\eri t$ (where $\Sigma$ is a predefined summation symbol and $D,f,t$ are terms). A straightforward black-box integration into superposition calculus is to try the method to every eligible inequation $\Sigma_{D}f\eri t$ in every clause. This can be formulated as an inference rule:
\[
\frac{\hfill C\vee\Sigma_{D}f\eri t\hphantom{)\left[n:=i\right]}}{B\vee C\vee\bigvee\limits _{i\in I}\sulut{\Sigma_{D}f\eri t}\left[n:=i\right]}\quad\myrule
\]
The inference finds suitable subterms $n$ to generalize, propagates recurrences w.r.t. those $n$ and replaces them with sufficient initial values $I$ according to the final recurrences. Term $\Sigma_{D}f-t$ determines only the propagation steps whereas the propagated recurrences come from any number of side premises which are not shown here. In some cases it might be useful to allow also conditional equations as side premises which $B$ reminds about.

Remarks: $I$ is a finite set of terms. We can only hope that they make the clause simpler in place of $n$. Inductionless derivation has $I=\varnothing$. Elements of $I$ and $n$ can be tuples (optimization over repeating a single assignment form). Often terms also outside $n$ are generalized. It is sound that $n$ appears in $C$ but chances are that generalization then loses important information. Side premises may also tell something about $n$, most usefully bounds. The trigger $\Sigma_{D}f\eri t$ can be generalized to $a\cdot\Sigma_{D}f+b\eri t$ with $\cdot$,+ interpreted.
\begin{example}
(Fulfillment of \ref{swap nested}.) Consider the clauses $0\leq\kappa$ and 
\[
\Sigma_{\left[0,\kappa\right]}\lambda m.\Sigma_{\left[0,\kappa\right]}\lambda n.fmn\eri\Sigma_{\left[0,\kappa\right]}\lambda n.\Sigma_{\left[n,\kappa\right]}\lambda m.fmn
\]
where $0,\kappa,f,\left[\cdot,\cdot\right],\leq,\Sigma$ are function symbols and $\lambda\cdot.\cdot$ forms an anonymous function. We assume presence of also other clauses that define $\leq$ (integer arithmetic) and $\Sigma$ (commutative groups). The inequality clause here has a syntactic form that triggers the $\myrule$ rule.

In the propagation part we'll want to consider recurrences w.r.t. $\kappa$ but $\kappa$ is a constant. Hence we generalize $\kappa$ to a variable $k$ and try to prove the stronger claim 
\[
\forall k\s(\underset{\mathclap{\begin{subarray}{c}
\text{background clauses}\\
\text{with }\kappa\mapsto k
\end{subarray}}}{\underbrace{0\leq k}}\implies\underset{\begin{subarray}{c}
\text{negated trigger clause normalized as }\approx0\\
\text{with }\kappa\mapsto k
\end{subarray}}{\underbrace{\Sigma_{\left[0,k\right]}\lambda m.\Sigma_{\left[0,k\right]}\lambda n.fmn-\Sigma_{\left[0,k\right]}\lambda n.\Sigma_{\left[n,k\right]}\lambda m.fmn\approx0}}).
\]
Its instance with $k=\kappa$ will contradict the given clauses but the propagation method will only prove it upto initial values of $k$. Of course we need a better reason to choose precisesly $\kappa$ to be generalized. Only integer subterms in the trigger need to be considered. They are $0,\kappa,m,n,fmn$. Last three contain bound variables $m,n$ and hence cannot be generalized. There's little point generalizing the interpreted 0. So $\kappa$ was the only option.

Finding recurrences is done in the example \ref{swap nested}. But before that we enumerate the necessary sets to compute bijectivity and commutation errors (these do not depend dynamically on the propagation). Let's consider $\left[0,\kappa+1\right]\setminus\left[0,\kappa\right]$ that should be simplified to $\left\{ \kappa+1\right\} $. The simplification machinery of superposition can be reused as follows. Add to the proof state the formula $a\in\left[0,\kappa+1\right]\wedge a\not\in\left[0,\kappa\right]\Leftrightarrow b$ where constant $a$ represents an arbitrary test point and role of constant $b$ is to guarantee soundness. Then wait for $a\approx\kappa+1\Leftrightarrow b$ to appear (in its clausified form; see subsection \ref{Enumerate}).

In the end one recurrence is found and it is $T_{k+1}-T_{k}\approx0$ while $\forall k\s\sulut{0\leq k\Rightarrow T_{k}\approx0}$ is the generalization to prove. By induction $0\approx T_{0}\Rightarrow\forall k\s\sulut{0\leq k\Rightarrow T_{k}\approx0}$ where the recurrence told the number (1) of initial values $\left\{ 0\right\} $ and the constraint of $k$ $\sulut{0\leq k}$ told their offset. But the generalized goal was contradictory so $\myrule$ concludes
\[
\Sigma_{\left[0,0\right]}\lambda m.\Sigma_{\left[0,0\right]}\lambda n.fmn\eri\Sigma_{\left[0,0\right]}\lambda n.\Sigma_{\left[n,0\right]}\lambda m.fmn.
\]

Now simplification should take over and rewrite $\Sigma_{\left[0,0\right]}F\to\Sigma_{\left\{ 0\right\} }F\to F0$. This reduces the just obtained inequation clause to $f00\eri f00$ that shows the clause set to be contradictory.
\end{example}
I proceed to give heuristics to solve issues that must be considered in this kind of integration. We must address how to choose subterms $n$ to generalize and how to initially find recurrence equations. Moreover we will specify how we try to enumerate set expressions\textemdash a detail we skipped about propagation to sums in \ref{Sum}. But first, let us not forget the obvious prerequisite of detecting a theory of commutative groups or rings.

\subsection{Theory detection}

To find e.g. a binary function I'm going to consider as candidates all function symbols with parameters\textemdash form $f\sulut{\tuple p,\cdot,\tuple r,\cdot,\tuple t}$ with constant term tuples $\tuple p,\tuple r,\tuple t$\textemdash that appear in the input clauses. These forms are motivated by encoding of types as parameters (like $+\sulut{\makeop{type},\cdot,\cdot}$) and lifting of group operations to, say, quotient (like $\makeop{lift}\sulut{+_{\makeop{base}},\cdot,\cdot}$).

When I ask to test or check an expression (clause) $C$, I mean to first look for it syntactically. If that is unsuccessful, $\neg C$ is then attempted to be refuted by running another instance of the prover on it a short while.
\begin{itemize}
\item I assume a syntactic criterion to detect summation symbols $\Sigma$. The internal form is then normalized, e.g. term $\makeop{sum}\sulut{f,a,b}$ could become $\Sigma_{\left[a,b\right[}f$. (I need a hard coded criterion because I feel that defining properties of $\Sigma$ are easily stated in unforeseenable ways.)
\item I assume access to defining properties of $\Sigma$ and as by-product to constants +,0 as well as to their commutative monoid axioms. Needed properties are:
\begin{enumerate}
\item \label{sum 0}$\Sigma_{A}f=0\Leftarrow\forall a\in A.\s fa=0$
\item \label{sum 1}$\Sigma_{\left\{ a\right\} }f=fa$
\item \label{sum A=000394B}$\Sigma_{A}f+\Sigma_{B\setminus A}f=\Sigma_{B}f+\Sigma_{A\setminus B}f$ when $\set{a\in A\cup B}{fa\neq0}$ is finite
\item \label{sum f+g}$\Sigma_{A}\sulut{f+g}=\Sigma_{A}f+\Sigma_{A}g$ when $\set{a\in A}{fa\neq0\text{ or }ga\neq0}$ is finite
\item \label{sum other}Definition in terms of this normal form, e.g. $\makeop{sum}\sulut{f,a,b}=\Sigma_{\left[a,b\right[}f$.
\end{enumerate}
\item Find unary $-$ s.t. $\forall a.\s{-}a+a=0$, or binary $-$ s.t. $\forall a,b.\s a-b+b=a$, or verify cancellation $\forall a,b,c\s\sulut{a+c=b+c\Rightarrow a=b}$ and complete into group.
\item Optionally find distributive binary function: the multiplication. Other properties are also useful (I programmed under assumptions of unit and commutativity).
\item Detect integers and their operations for induction (already in Zipperposition).
\end{itemize}

\subsection{Choosing terms to generalize}

Generalizing subterms $n$ in an inequality $\neg E_{n}$ means that we ignore fine structure of these $n$ and look the task of refuting $\neg E_{n}$ as a task of proving $\forall n\s E_{n}$. These $n$ become the variables in the propagation steps.

My generalization heuristic is this. First, explicit integer constants ($0,\pm1,\pm2,...$) are never generalized. All other atomic constants (in the trigger $\Sigma_{D}f\eri t$) of type $X$ are generalized where the group $X$ is range of a $\Sigma$. Extending, $g\sulut{t_{1},...,t_{n}}\in X$ is generalized if $t_{j}\in\mathbb{Z}$ is explicit or $t_{j}\not\in X$ for every $j$. This is explained by considering a situation in which we do not want to generalize: if $g:X\to X$, then $g$ can admit recurrences useful with e.g. $g\sulut{a+b}$ with $a,b$ generalized. However recurrences are useless with $g1$, as 1 is not generalized, and hence $g1$ may be turned into a variable.

\subsection{Choosing initial recurrences}

The general principle is to choose recurrences $s_{1}\approx s_{2}$ from clauses $s_{1}\approx s_{2}\vee C$ when $s_{1}\approx s_{2}$ shares function symbols with the trigger $\Sigma_{D}f\eri t$ or another chosen recurrence. (The next heuristic will likely need tuning once I get to realize it.) Starting from both sides $s_{1},s_{2}$ of an equation $s_{1}\approx s_{2}$ let the \emph{scope of interpretation} cover all terms recursively within additions and products as well as summands. That is, any term that can participate to propagation. I start with all (uninterpreted) head function symbols of terms within the scope of interpretation in $\Sigma_{D}f\approx t$. For each such $g$ I look for clauses $Pg\sulut{x,a}+s\approx0\vee C$ (when normalized) where the polynomial $P$ operates at (the positions of) free variables $x$, and parameters $a$ match the corresponding parameters in some earlier occurrence of $g$. The term sequences $x$ and $a$ may be interleaved, and $x$ is nonempty. The $s$ is any term and clause $C$ has no eligible literals. I then repeat with top-level function symbols from $s$.

The goal is to find symbols used to define each $g$ above but unfortunately this naïve search also picks symbols defined by any $g$. To mitigate this let's consider an auxiliary property \textquotedblleft needs definition\textquotedblright{} of function symbols. All the starting symbols need definition by default. Let then $g$ need definition and consider a clause $Pg\sulut{x,a}+s\approx0\vee C$ as before. If it does not represent a proper recurrence\textemdash all shifts in $P$ are equal\textemdash then the symbols from $s$ may need definition. A symbol needs definition in no other situation. Moreover say that $Pg\sulut{x,a}+s\approx0\vee C$ provides a definition for $g$. Now we filter the naïvely found symbols based on these two properties. If a symbol needs definition but is not provided one, then recursively remove that symbol and clauses that contain it.
\begin{example}
In our very first example \ref{indefinite sum ex.} we'd see a trigger $\sum_{n=0}^{m}f_{n}\eri g_{m}+f_{0}$ and two candidate initial recurrences $g_{0}\approx0$ and $g_{n+1}\approx g_{n}+f_{n+1}$. Here $n$ is variable, and constant $m$ gets abstracted. Function symbols from scope of interpretation are $f$ and $g$ that need definition for now. Clause $g_{0}\approx0$ lacks variables and so does not give a recurrence. Normalized clause $\sulut{N-1}g_{n}-f_{n+1}\approx0$ provides a proper recurrence for $g$, and as $f$ occurs in this clause, $f$ no longer needs definition.
\end{example}

\subsection{Near bijectivity and commutation \label{Enumerate}}

To preserve some generality I suggest in section \ref{Sum} to compute bijectivity and commutation errors by enumerating sets given as terms. This can be done as follows. Let $A$ be a term of set type to enumerate. I let the superposition calculus to simplify proposition $s\in A$ into form $\bigvee_{j=1}^{m}s\approx a_{j}$ where $s$ is a large Skolem symbol and $a_{j}$ are any terms. To avoid contradiction I put $b\Leftrightarrow s\in A$ instead of $s\in A$ into proof state with $b$ being a fresh small unselectable constant. Then I wait for 
\[
\makeop{cnf}\sulut{b\Leftrightarrow\bigvee_{j=1}^{m}s\approx a_{j}}=\left\{ b\vee s\eri a_{1},\s...,\s b\vee s\eri a_{m},\s\neg b\vee\bigvee_{j=1}^{m}s\approx a_{j}\right\} 
\]
to appear. (Cnf stands for clause normal form.) Finally I check $a_{i}\eri a_{j}$ for $i\neq j$ by refuting each $a_{i}\approx a_{j}$ in turn. Afterwards $a_{1},...,a_{m}$ enumerates $A$.

\subsection{Initial values to induction}

A common case is that variables are natural numbers and we have a final recurrence with maximal shift $S_{1}^{a_{1}}...S_{k}^{a_{k}}$. Then initial values $\bigcup_{j=1}^{k}\set{n\in\mathbb{N}^{k}}{0\leq n_{j}<a_{j}}$ suffice. As a union of stacked hyperplanes that is infinite (unless $k\leq1$) but it corresponds to just $\sum_{j=1}^{k}a_{j}$ substitutions $\left\{ n_{j}\mapsto i\right\} $ for $1\leq j\leq k$ and $0\leq i<a_{j}$.

General case with multiple recurrences and boundaries would be complex. To be useful the final recurrences must have the form $Rs\approx0$ with $R$ an operator polynomial and $s=\Sigma_{D}f-t$ the term we want to vanish. On the shift indeterminates fix any monomial order in the sense of commutative Gröbner-bases. For each recurrence consider the exponents $a=\sulut{a_{1},...,a_{k}}$ of its maximal monomial $S_{1}^{a_{1}}...S_{k}^{a_{k}}$. Let $\sqsubseteq$ be the least translation invariant order on $\mathbb{Z}^{k}$ s.t. $0\sqsubseteq a$ for each of these exponent tuples $a$. Since $a\geq0$ componentwise, $\sqsubseteq$ extends naturally to $\sulut{\left\{ -\infty\right\} \cup\mathbb{Z}}^{k}$. Now if $X\subseteq\mathbb{Z}^{k}$ is a convex set on which $s\approx0$ is to be proven, then the needed initial values are $\sqsubseteq$-minimal elements of closure of $X$ in $\sulut{\left\{ -\infty\right\} \cup\mathbb{Z}}^{k}$. Except that $-\infty$ of course cannot be used and the corresponding coordinate must be split with artificial bounds (like $n\leq0$ and $n\geq0$; in 1D this is to say that two inductions to opposite directions are needed to prove something for all integers). In this case as well as generally the recurrences may have to be applied backwards. Moreover one must check that the multiplier in the leading term does not vanish on $X$. Note that the leading term is different for backward recurrence. In theory more initial values could be used to overcome a problem of vanishing multiplier in the leading term but that would require finding the zeros explicitly.

\section{Related work}
\begin{itemize}
\item Zeilberger popularized holonomic sequences and recurrences in proving equations of summations \cite{basicholo}.
\item Paule and Schorn implemented WZ algorithm in Mathematica \cite{MathematicaWZ}. Koutschan added holonomic systems \cite{MathematicaHolo}. (Univariate work of Mallinger \cite{inductPhD} preceded this.)
\item Mahboubi and Sibut-Pinote formalize holonomic computations from Mathematica in Coq as part of formalizing $\zeta\sulut 3\not\in\mathbb{Q}$ \cite{Coq}.
\item Harrison implemented WZ certification in HOL Light with Maxima as a backend \cite{HOL:WZ}. Due to division (by 0) in WZ method the proof reconstruction (by analytic continuation) is difficult compared to using recurrences here.
\item Chyzak, Kauers and Salvy study meta-theory of a homogeneous version of the method here with many more options as monomials \cite{close}. Their results apply to the presented method.
\item Koornwinder implemented WZ algorithm and its $q$-analogue in Maple \cite{MapleWZ}.
\item 
\end{itemize}
\bibliographystyle{plain}
\bibliography{bib}

\end{document}
