#LyX 2.3 created this file. For more info see http://www.lyx.org/
\lyxformat 544
\begin_document
\begin_header
\save_transient_properties true
\origin unavailable
\textclass article
\begin_preamble
\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}
\end_preamble
\use_default_options true
\begin_modules
theorems-vu
enumitem
\end_modules
\maintain_unincluded_children false
\language english
\language_package default
\inputencoding auto
\fontencoding global
\font_roman "default" "default"
\font_sans "default" "default"
\font_typewriter "default" "default"
\font_math "auto" "auto"
\font_default_family default
\use_non_tex_fonts false
\font_sc false
\font_osf false
\font_sf_scale 100 100
\font_tt_scale 100 100
\use_microtype false
\use_dash_ligatures false
\graphics default
\default_output_format default
\output_sync 0
\bibtex_command default
\index_command default
\paperfontsize default
\spacing other 0.8
\use_hyperref false
\papersize default
\use_geometry false
\use_package amsmath 1
\use_package amssymb 1
\use_package cancel 1
\use_package esint 1
\use_package mathdots 1
\use_package mathtools 1
\use_package mhchem 1
\use_package stackrel 1
\use_package stmaryrd 1
\use_package undertilde 1
\cite_engine basic
\cite_engine_type default
\biblio_style plain
\use_bibtopic false
\use_indices false
\paperorientation portrait
\suppress_date false
\justification false
\use_refstyle 1
\use_minted 0
\index Index
\shortcut idx
\color #004000
\end_index
\leftmargin 2cm
\topmargin 1cm
\rightmargin 2cm
\bottommargin 3cm
\secnumdepth 3
\tocdepth 2
\paragraph_separation indent
\paragraph_indentation default
\is_math_indent 0
\math_numbering_side default
\quotes_style english
\dynamic_quotes 0
\papercolumns 1
\papersides 1
\paperpagestyle default
\tracking_changes false
\output_changes false
\html_math_output 0
\html_css_as_file 0
\html_be_strict false
\end_header

\begin_body

\begin_layout Standard
\begin_inset Box Frameless
position "t"
hor_pos "c"
has_inner_box 1
inner_pos "t"
use_parbox 0
use_makebox 0
width "100col%"
special "none"
height "1in"
height_special "totalheight"
thickness "0.4pt"
separation "3pt"
shadowsize "4pt"
framecolor "black"
backgroundcolor "none"
status collapsed

\begin_layout Plain Layout
\begin_inset ERT
status open

\begin_layout Plain Layout


\backslash
global
\backslash
let 
\backslash
oldquad
\backslash
quad
\end_layout

\begin_layout Plain Layout


\backslash
global
\backslash
let 
\backslash
oldqquad
\backslash
qquad
\end_layout

\end_inset


\end_layout

\begin_layout Plain Layout
\begin_inset FormulaMacro
\newcommand{\skip}{}
{​}
\end_inset


\begin_inset FormulaMacro
\newcommand{\s}{\ }
{ }
\end_inset


\begin_inset FormulaMacro
\newcommand{\quad}{\oldquad}
{     }
\end_inset


\begin_inset FormulaMacro
\newcommand{\qquad}{\oldqquad}
{          }
\end_inset


\end_layout

\begin_layout Plain Layout
\begin_inset FormulaMacro
\newcommand{\underline}[1]{\text{\leavevmode\vtop{\hbox{\ensuremath{#1}}\kern0.4ex  \hrule height.4pt}}}
{\underline{#1}}
\end_inset


\end_layout

\begin_layout Plain Layout
\begin_inset FormulaMacro
\newcommand{\sulut}[1]{\left(#1\right)}
{{\scriptscriptstyle \texttt{(}\lyxlock}#1{\scriptscriptstyle \texttt{)}}}
\end_inset


\end_layout

\begin_layout Plain Layout
\begin_inset FormulaMacro
\newcommand{\makeop}[1]{\operatorname{#1}}
{\text{ #1 }}
\end_inset


\end_layout

\begin_layout Plain Layout
\begin_inset FormulaMacro
\newcommand{\makelim}[2]{\operatorname*{#1}\limits _{#2}}
{\text{ #1}\limits _{#2}}
\end_inset


\end_layout

\begin_layout Plain Layout
\begin_inset FormulaMacro
\newcommand{\back}[1]{\hspace{-#1em}}
{^{\overleftarrow{#1}}}
\end_inset


\end_layout

\begin_layout Plain Layout
\begin_inset FormulaMacro
\newcommand{\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}} }
{\Big|_{#1}}
\end_inset


\end_layout

\begin_layout Plain Layout
\begin_inset FormulaMacro
\newcommand{\eri}{\not\approx}
\end_inset


\begin_inset FormulaMacro
\newcommand{\integ}[2][\skip]{\int_{#2}^{#1}\negthickspace}
{\int\limits _{#2}^{\s#1}}
\end_inset


\end_layout

\begin_layout Plain Layout
\begin_inset FormulaMacro
\newcommand{\set}[2]{\left\{  #1\,\vphantom{\overset{o}{O}}\middle|\,#2\right\}  }
{\left\{ #1\Big|#2\right\} }
\end_inset


\end_layout

\begin_layout Plain Layout
\begin_inset FormulaMacro
\newcommand{\url}[1]{\text{\href{#1}{#1}}}
{{\color{blue}#1}}
\end_inset


\end_layout

\begin_layout Plain Layout
\begin_inset FormulaMacro
\newcommand{\seq}[1]{\vec{#1}}
{\overset{{\scriptstyle →}}{#1}}
\end_inset


\begin_inset FormulaMacro
\newcommand{\tuple}[1]{\vec{#1}}
{\overset{{\scriptstyle →}}{#1}}
\end_inset


\end_layout

\begin_layout Plain Layout
\begin_inset FormulaMacro
\newcommand{\holdsIn}{\mathrel{\veny\models1{-1}}}
{\s⫤\s}
\end_inset


\end_layout

\begin_layout Plain Layout
\begin_inset FormulaMacro
\newcommand{\rule}[3]{{\scriptstyle #2}{\displaystyle \frac{#3}{#1}}}
\end_inset


\end_layout

\end_inset


\end_layout

\begin_layout Standard
\begin_inset ERT
status open

\begin_layout Plain Layout


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

\end_inset


\end_layout

\begin_layout Standard
\begin_inset FormulaMacro
\newcommand{\link}[2]{\hyperref[#2]{#1}}
{^{{\scriptscriptstyle #2}}#1}
\end_inset


\end_layout

\begin_layout Standard
\begin_inset FormulaMacro
\newcommand{\simprule}[2]{\begin{array}{c}
\negthickspace#1\negthickspace\\
\hline\hline \negthickspace#2\negthickspace
\end{array}}
{\begin{array}{c}
#1\\
\hline\hline #2
\end{array}}
\end_inset


\end_layout

\begin_layout Standard
\begin_inset FormulaMacro
\newcommand{\mgux}{\makeop{mgu}^{\times}}
\end_inset


\begin_inset FormulaMacro
\newcommand{\csu}{\makeop{CSU}^{\times}}
\end_inset


\end_layout

\begin_layout Section
Motivation
\end_layout

\begin_layout Standard
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.
\end_layout

\begin_layout Standard
Gosper first presented a method to find closed hypergeometric form of an
 indefinite sum 
\begin_inset Formula $\sum_{n=0}^{m}f_{n}$
\end_inset

 of a hypergeometric sequence 
\begin_inset Formula $f_{n}$
\end_inset

 
\begin_inset CommandInset citation
LatexCommand cite
key "Gosper"
literal "false"

\end_inset

.
 That is an exploration tool while the resulting equation is simple to verify.
 Wilf and Zeilberger then used this in their WZ pairs method 
\begin_inset CommandInset citation
LatexCommand cite
key "WZcert"
literal "false"

\end_inset

 to certify definite hypergeometric summations such as the binomial theorem
 
\begin_inset Formula $\sum_{n\in\mathbb{Z}}\binom{m}{n}a^{n}b^{m-n}=\sulut{a+b}^{m}$
\end_inset

.
 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 
\begin_inset CommandInset citation
LatexCommand cite
key "basicholo"
literal "false"

\end_inset

.
 These are functions defined by linear recurrences with polynomial coefficients
 and finitely many initial values.
\end_layout

\begin_layout Standard
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 
\begin_inset CommandInset citation
LatexCommand cite
key "close"
literal "false"

\end_inset

).
 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.
\end_layout

\begin_layout Standard
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 
\begin_inset CommandInset citation
LatexCommand cite
key "Zip"
literal "false"

\end_inset

 which is a higher-order superposition prover 
\begin_inset CommandInset citation
LatexCommand cite
key "HOsup"
literal "false"

\end_inset

.
 In this context terms with summations, such as 
\begin_inset Formula $\sum_{n=a}^{b}n$
\end_inset

, need no special introduction.
 Right now things of section 
\begin_inset CommandInset ref
LatexCommand ref
reference "Propagations"
plural "false"
caps "false"
noprefix "false"

\end_inset

 are implemented while only minimal demo functionality from section 
\begin_inset CommandInset ref
LatexCommand ref
reference "Integration"
plural "false"
caps "false"
noprefix "false"

\end_inset

 is working.
 Proof reconstruction in Isabelle is uncharted territory.
\end_layout

\begin_layout Section
Preliminaries
\end_layout

\begin_layout Itemize
Here polynomials are non-commutative by default.
 Though we still ask commutation relations for indeterminates, e.g.
 
\begin_inset Formula $XY-YX=X$
\end_inset

 in a ring 
\begin_inset Formula $\mathbb{Z}\left[X,Y\right]$
\end_inset

.
 Theoretical basis is that of Ore-polynomials 
\begin_inset CommandInset citation
LatexCommand cite
key "Ore"
literal "false"

\end_inset

.
\end_layout

\begin_layout Itemize
The procedure works with symbolic equations.
 I write them using 
\begin_inset Formula $\approx$
\end_inset

 to distinguish them from meta reasoning (=).
 So 
\begin_inset Formula $P\approx0$
\end_inset

 is something to save for later, except that if 
\begin_inset Formula $P=0$
\end_inset

, it is a triviality.
\end_layout

\begin_layout Itemize
Monomial order 
\begin_inset Formula $\preccurlyeq$
\end_inset

 in the sense of Gröbner-bases is a well-founded order on standard commutative
 monomials s.t.
 multiplication is increasing meaning 
\begin_inset Formula $M\preccurlyeq M'\Rightarrow NM\preccurlyeq NM'$
\end_inset

 for all monomials 
\begin_inset Formula $M,M',N$
\end_inset

.
\end_layout

\begin_layout Itemize
Monomial order for generalized Gröbner-bases is the same except that non-commuta
tive monomials are not closed under multiplication (when normalized).
 Hence “multiplication is increasing” only upto leading (largest) monomials.
\end_layout

\begin_layout Section
Reasoning with recurrences 
\begin_inset CommandInset label
LatexCommand label
name "Propagations"

\end_inset


\end_layout

\begin_layout Standard
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:
\end_layout

\begin_layout Itemize
Fibonacci numbers 
\begin_inset Formula $F_{n+2}-F_{n+1}-F_{n}=0$
\end_inset

 for 
\begin_inset Formula $n\geq0$
\end_inset

 with 
\begin_inset Formula $F_{0}=0$
\end_inset

 and 
\begin_inset Formula $F_{1}=1$
\end_inset

.
\end_layout

\begin_layout Itemize
Polynomials 
\begin_inset Formula $P$
\end_inset

 because for 
\begin_inset Formula $d=\makeop{deg}P+1$
\end_inset

 and every 
\begin_inset Formula $n$
\end_inset

 holds
\begin_inset Formula 
\[
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.
\]

\end_inset


\end_layout

\begin_layout Itemize
Sums 
\begin_inset Formula $S_{m}=\sum_{n=0}^{m}f_{n}$
\end_inset

 upto fresh variable because 
\begin_inset Formula $S_{m+1}-S_{m}=f_{m+1}$
\end_inset

 for 
\begin_inset Formula $m\geq0$
\end_inset

.
\end_layout

\begin_layout Itemize
Exponentials: 
\begin_inset Formula $b^{n+1}=b\cdot b^{n}$
\end_inset

 for 
\begin_inset Formula $n\geq0$
\end_inset

 with 
\begin_inset Formula $b^{0}=1$
\end_inset

.
\end_layout

\begin_layout Itemize
Factorial: 
\begin_inset Formula $\sulut{n+1}!=\sulut{n+1}\cdot n!$
\end_inset

 for 
\begin_inset Formula $n\geq0$
\end_inset

 with 
\begin_inset Formula $0!=1$
\end_inset

.
\end_layout

\begin_layout Standard
In fancier words the definitional facts we can use are multivariate inhomogeneou
s linear finite-step equations with polynomial coefficients.
 A prototypical example is 
\begin_inset Formula $\sulut{n^{2}+1}f_{m+2}^{n+1}+mf_{m+1}^{n}-nmf_{m}^{n+1}=h_{m}^{n}$
\end_inset

 where 
\begin_inset Formula $f$
\end_inset

 and 
\begin_inset Formula $h$
\end_inset

 are symbolic sequences and 
\begin_inset Formula $n,m$
\end_inset

 integer variables.
 Such equations make sense with values in any ring or commutative group
 which is our assumed setting.
\end_layout

\begin_layout Standard
We use the techniques of the theory of holonomic sequences to work with
 the recurrences.
 That is for every 
\emph on
composite
\emph default
 term—addition, product or indexed sum of simpler terms—we try to find a
 linear recurrence from the recurrences of its parts.
 This works upwards from non-composite, 
\emph on
atomic
\emph default
, terms whose recurrences need to be given.
\end_layout

\begin_layout Example
\begin_inset CommandInset label
LatexCommand label
name "indefinite sum ex."

\end_inset

Consider task of proving 
\begin_inset Formula $\sum_{n=0}^{m}f_{n}=g_{m}+f_{0}$
\end_inset

 given 
\begin_inset Formula $g_{0}=0$
\end_inset

 and 
\begin_inset Formula $g_{m+1}=g_{m}+f_{m+1}$
\end_inset

.
\end_layout

\begin_layout Example
We write this canonically as an equation to zero: 
\begin_inset Formula $g_{m}+f_{0}-\sum_{n=0}^{m}f_{n}=0$
\end_inset

.
 Atomic terms are 
\begin_inset Formula $f$
\end_inset

 and 
\begin_inset Formula $g$
\end_inset

.
 One way of piecing up the composite expression is to give names 
\begin_inset Formula $h_{m}=g_{m}+f_{0}$
\end_inset

, 
\begin_inset Formula $F_{m}=\sum_{n=0}^{m}f_{n}$
\end_inset

, and 
\begin_inset Formula $E_{m}=h_{m}-F_{m}$
\end_inset

.
 We then proceed to find recurrences for 
\begin_inset Formula $h$
\end_inset

, 
\begin_inset Formula $F$
\end_inset

 and 
\begin_inset Formula $E$
\end_inset

 from the given recurrence 
\begin_inset Formula $g_{m+1}-g_{m}-f_{m+1}=0$
\end_inset

 of 
\begin_inset Formula $g$
\end_inset

.
\end_layout

\begin_layout Example
Recurrence of 
\begin_inset Formula $h$
\end_inset

: We defined 
\begin_inset Formula $h$
\end_inset

 in terms of 
\begin_inset Formula $g$
\end_inset

 (and constant 
\begin_inset Formula $f_{0}$
\end_inset

).
 Hence we want to eliminate 
\begin_inset Formula $g$
\end_inset

 from the equations.
 We use superposition-style reasoning with 
\begin_inset Formula $g$
\end_inset

 being largest symbol.
\begin_inset Formula 
\[
\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}
\]

\end_inset


\end_layout

\begin_layout Example
Recurrence of 
\begin_inset Formula $F$
\end_inset

: Obviously 
\begin_inset Formula $F_{m+1}-F_{m}=f_{m+1}$
\end_inset

.
 Formally we derive this by considering how the index set 
\begin_inset Formula $\left[0,m\right]$
\end_inset

 changes when 
\begin_inset Formula $m$
\end_inset

 changes.
 When 
\begin_inset Formula $m\geq0$
\end_inset

 we get 
\begin_inset Formula $\left[0,m\right]\setminus\left[0,m+1\right]=\varnothing$
\end_inset

 and 
\begin_inset Formula $\left[0,m+1\right]\setminus\left[0,m\right]=\left\{ m+1\right\} $
\end_inset

 so
\begin_inset Formula 
\[
F_{m+1}-F_{m}=\sum_{n\in\left\{ m+1\right\} }f_{n}-\sum_{n\in\varnothing}f_{n}=f_{m+1}.
\]

\end_inset


\end_layout

\begin_layout Example
Recurrence of 
\begin_inset Formula $E$
\end_inset

: Since 
\begin_inset Formula $E_{m}=h_{m}-F_{m}$
\end_inset

 is defined by 
\begin_inset Formula $h$
\end_inset

 and 
\begin_inset Formula $F$
\end_inset

, we eliminate 
\begin_inset Formula $h$
\end_inset

 and 
\begin_inset Formula $F$
\end_inset

 with the help of their recurrences.
\begin_inset Formula 
\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*}

\end_inset

Hence 
\begin_inset Formula $E_{m+1}=E_{m}$
\end_inset

 and by induction, to prove the claim 
\begin_inset Formula $E_{m}=0$
\end_inset

 for 
\begin_inset Formula $m\geq0$
\end_inset

, it now suffices to prove the trivial base case 
\begin_inset Formula $E_{0}=0$
\end_inset

.
\end_layout

\begin_layout Subsection
Propagation to addition 
\begin_inset CommandInset label
LatexCommand label
name "Plus"

\end_inset


\end_layout

\begin_layout Standard
We introduce formal notation for the equations we make use of to better
 communicate possibilities and limits.
 A basic recurrence has the form 
\begin_inset Formula $R_{1}f_{1}+...+R_{k}f_{k}\approx0$
\end_inset

.
 Here each 
\begin_inset Formula $f_{j}$
\end_inset

 is a sequence (or like) term whose fine structure is ignored in calculations
 making 
\begin_inset Formula $f_{j}$
\end_inset

 like an atomic constant.
 Instead the operator polynomials 
\begin_inset Formula $R_{j}$
\end_inset

 carry a rich fine structure that is defined below.
 Finally the 
\begin_inset Formula $\approx$
\end_inset

 hints that this is data in the algorithm instead of an explanation or a
 calculation step.
\end_layout

\begin_layout Definition
Operator polynomials are non-commutative polynomials over 
\begin_inset Formula $\mathbb{Z}$
\end_inset

 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:
\end_layout

\begin_layout Definition
The 
\begin_inset Formula $j$
\end_inset


\begin_inset script superscript

\begin_layout Plain Layout
th
\end_layout

\end_inset

 multiplication indeterminate, say 
\begin_inset Formula $n_{j}$
\end_inset

, operates to a function 
\begin_inset Formula $f$
\end_inset

 by multiplication by the 
\begin_inset Formula $j$
\end_inset


\begin_inset script superscript

\begin_layout Plain Layout
th
\end_layout

\end_inset

 coordinate: 
\begin_inset Formula $\sulut{n_{j}f}\sulut{...,\makeop n_{j},...}=\makeop n_{j}\cdot f\sulut{...,\makeop n_{j},...}$
\end_inset

.
\end_layout

\begin_layout Definition
The 
\begin_inset Formula $j$
\end_inset


\begin_inset script superscript

\begin_layout Plain Layout
th
\end_layout

\end_inset

 shift indeterminate, say 
\begin_inset Formula $N_{j}$
\end_inset

, operates to a function 
\begin_inset Formula $f$
\end_inset

 by shifting it in the direction of the 
\begin_inset Formula $j$
\end_inset


\begin_inset script superscript

\begin_layout Plain Layout
th
\end_layout

\end_inset

 coordinate: 
\begin_inset Formula $\sulut{N_{j}f}\sulut{...,\makeop n_{j},...}=f\sulut{...,\makeop n_{j}+1,...}$
\end_inset

.
\end_layout

\begin_layout Definition
Compatibly with the operation action the indeterminates commute except that
\begin_inset Formula 
\[
N_{j}n_{j}=\sulut{n_{j}+1}N_{j}=n_{j}N_{j}+N_{j}.
\]

\end_inset


\end_layout

\begin_layout Standard
Conventionally I use the same lower case letter for a variable and its multiplie
r, and the corresponding upper case letter for the shift indeterminate.
 For example I expand the (non-)commutation relation as 
\begin_inset Formula 
\[
\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}.
\]

\end_inset


\end_layout

\begin_layout Standard
An equation is a sum of monomials equal to zero.
 A monomial has the form 
\begin_inset Formula $c\cdot n_{1}^{a_{1}}...n_{k}^{a_{k}}\cdot N_{1}^{b_{1}}...N_{k}^{b_{k}}f$
\end_inset

 where 
\begin_inset Formula $c\in\mathbb{Z}$
\end_inset

, 
\begin_inset Formula $a_{j},b_{j}\in\mathbb{N}$
\end_inset

, and 
\begin_inset Formula $f$
\end_inset

 is a sequence term.
 An equation set can be saturated—ignoring the fine structure of the sequence
 terms—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 
\begin_inset Formula $\mathbb{Z}\left[n_{1},...,n_{k},N_{1},...,N_{k}\right]$
\end_inset

 increases as new recurrences are found but the ring is Noetherian 
\begin_inset CommandInset citation
LatexCommand cite
key "wiki:stop"
literal "false"

\end_inset

.
 To each sequence term 
\begin_inset Formula $f$
\end_inset

 corresponds a different ideal but there is only a finite number of them.
\end_layout

\begin_layout Standard
Assume that in a formula that we try to prove occurs sequence-like sub-expressio
ns 
\begin_inset Formula $f_{n}$
\end_inset

, 
\begin_inset Formula $g_{n}$
\end_inset

 and 
\begin_inset Formula $f_{n}+g_{n}$
\end_inset

.
 We then introduce a convenience name 
\begin_inset Formula $h\approx f+g$
\end_inset

 and propagate recurrences of 
\begin_inset Formula $f$
\end_inset

 and 
\begin_inset Formula $g$
\end_inset

 to 
\begin_inset Formula $h$
\end_inset

.
\end_layout

\begin_layout Definition
Propagation to addition is accomplished as follows.
 Let 
\begin_inset Formula $f$
\end_inset

 and 
\begin_inset Formula $g$
\end_inset

 be the relevant terms and let 
\begin_inset Formula $h$
\end_inset

 be the formal name of their addition 
\begin_inset Formula $f+g$
\end_inset

.
 Let 
\begin_inset Formula $F$
\end_inset

 be the set of recurrences involving 
\begin_inset Formula $f$
\end_inset

, and 
\begin_inset Formula $G$
\end_inset

 be those involving 
\begin_inset Formula $g$
\end_inset

.
 Eliminate 
\begin_inset Formula $f$
\end_inset

 and 
\begin_inset Formula $g$
\end_inset

 from the recurrences 
\begin_inset Formula $F\cup G\cup\left\{ h\approx f+g\right\} $
\end_inset

 by saturating them w.r.t.
 an order making 
\begin_inset Formula $f$
\end_inset

- and 
\begin_inset Formula $g$
\end_inset

-monomials larger than others.
 The recurrences of 
\begin_inset Formula $h$
\end_inset

 are then those which contain 
\begin_inset Formula $h$
\end_inset

 but no 
\begin_inset Formula $f$
\end_inset

 nor 
\begin_inset Formula $g$
\end_inset

.
 Propagation to repeated and weighted addition (e.g.
 
\begin_inset Formula $2f-g+1$
\end_inset

) is achieved similarly.
\end_layout

\begin_layout Standard
In the previous example 
\begin_inset CommandInset ref
LatexCommand ref
reference "indefinite sum ex."

\end_inset

 it seemed obvious to do simple induction, and so the presented solution
 seems cumbersome.
 However if we had assumed 
\begin_inset Formula $g_{n+2}=g_{n}+f_{n+1}+f_{n+2}$
\end_inset

 with 
\begin_inset Formula $g_{0}=0$
\end_inset

 and 
\begin_inset Formula $g_{1}=f_{1}$
\end_inset

, 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:
\end_layout

\begin_layout Example
Let 
\begin_inset Formula $N^{2}g-g-N^{2}f-Nf\approx0$
\end_inset

, 
\begin_inset Formula $NF-F-Nf\approx0$
\end_inset

 and 
\begin_inset Formula $E\approx g+f_{0}-F$
\end_inset

 where 
\begin_inset Formula $N$
\end_inset

 is the shift indeterminate.
 We find recurrence of 
\begin_inset Formula $E$
\end_inset

 by eliminating 
\begin_inset Formula $g$
\end_inset

 and 
\begin_inset Formula $F$
\end_inset

.
 Maximal terms—which we cancel on each inference—are in bold.
\begin_inset Formula 
\[
\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}
\]

\end_inset

So 
\begin_inset Formula $E_{n+2}=E_{n}$
\end_inset

 which immediately tells that the induction needs a step size of 2.
 Especially 2 base cases 
\begin_inset Formula $n=0$
\end_inset

 and 
\begin_inset Formula $n=1$
\end_inset

 remain to be checked.
\end_layout

\begin_layout Subsection
Propagation to summation 
\begin_inset CommandInset label
LatexCommand label
name "Sum"

\end_inset


\end_layout

\begin_layout Standard
A summation is a term of the form 
\begin_inset Formula $\Sigma_{D}f$
\end_inset

 where 
\begin_inset Formula $\Sigma$
\end_inset

 is an interpreted function symbol, 
\begin_inset Formula $D$
\end_inset

 is a term representing the domain of summation, and the summand 
\begin_inset Formula $f$
\end_inset

 is a sequence term.
 We mostly write this in different notations, for example 
\begin_inset Formula $\sum_{j\in D_{n}}f_{n,j}$
\end_inset

 to make the variables explicit.
\end_layout

\begin_layout Definition
Propagation of recurrences to summation 
\begin_inset Formula $\Sigma_{D}f$
\end_inset

 of a sequence term 
\begin_inset Formula $f$
\end_inset

 proceeds in three steps.
 First we determine 
\emph on
bad
\emph default
 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 
\begin_inset Formula $\Sigma_{D}$
\end_inset

.
 Badness of shifts depends on 
\begin_inset Formula $D$
\end_inset

 and involves computing error terms.
 Next we eliminate the bad indeterminates from recurrences of 
\begin_inset Formula $f$
\end_inset

 by saturation.
 Then recurrences of 
\begin_inset Formula $\Sigma_{D}f$
\end_inset

 can be computed from those of 
\begin_inset Formula $f$
\end_inset

 and error terms of shifts.
\end_layout

\begin_layout Definition
For the shift indeterminate 
\begin_inset Formula $S$
\end_inset

 corresponding to the summation variable we have
\begin_inset Formula 
\[
\sum_{D}\sulut{S-1}g=\sum_{\sulut{D+1}\setminus D}g-\sum_{D\setminus\sulut{D+1}}g=:Eg
\]

\end_inset

where 
\begin_inset Formula $D+1=\set{d+1}{d\in D}$
\end_inset

.
 If the sets 
\begin_inset Formula $\sulut{D+1}\setminus D$
\end_inset

 and 
\begin_inset Formula $D\setminus\sulut{D+1}$
\end_inset

 can be enumerated (see section 
\begin_inset CommandInset ref
LatexCommand ref
reference "Enumerate"
plural "false"
caps "false"
noprefix "false"

\end_inset

), then the error 
\begin_inset Formula $E$
\end_inset

 becomes an evaluation of 
\begin_inset Formula $g$
\end_inset

 on an explicit set of terms to be substituted to the summation variable.
 In such case 
\begin_inset Formula $S$
\end_inset

 is 
\emph on
nearly 
\begin_inset Formula $D$
\end_inset

-bijective.
\end_layout

\begin_layout Definition
For any other shift indeterminate 
\begin_inset Formula $N$
\end_inset

 with corresponding variable 
\begin_inset Formula $n$
\end_inset

 we have 
\begin_inset Formula 
\[
\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}.
\]

\end_inset

If the sets 
\begin_inset Formula $D_{n}\setminus D_{n+1}$
\end_inset

 and 
\begin_inset Formula $D_{n+1}\setminus D_{n}$
\end_inset

 can be enumerated, then also this error 
\begin_inset Formula $\widetilde{N}$
\end_inset

 becomes an explicit evaluation as above.
 In such case 
\begin_inset Formula $N$
\end_inset

 is 
\emph on
nearly
\emph default
 
\emph on

\begin_inset Formula $D_{n}$
\end_inset

-commutable.
 
\emph default
This can be iterated to calculate commutation errors 
\begin_inset Formula $\widetilde{P}g:=\sum_{D}Pg-P\sum_{D}g$
\end_inset

 for polynomials 
\begin_inset Formula $P$
\end_inset

 of 
\begin_inset Formula $N$
\end_inset

.
\end_layout

\begin_layout Definition
A shift indeterminate is bad if it is not nearly bijective or commutable.
 Let 
\begin_inset Formula $P\sulut S$
\end_inset

 be a polynomial missing bad indeterminates, viewed as a function of (possibly
 bad and missing) shift 
\begin_inset Formula $S$
\end_inset

 w.r.t.
 the summation variable.
 Since multiplication by the summation variable is bad, 
\begin_inset Formula $S$
\end_inset

 commutes with indeterminates in 
\begin_inset Formula $P\sulut S$
\end_inset

.
 Hence we can uniquely write 
\begin_inset Formula $P\sulut S=\sulut{S-1}Q\sulut S+P\sulut 1$
\end_inset

 by polynomial long division.
 Now a recurrence 
\begin_inset Formula $P\sulut Sf\approx0$
\end_inset

 of 
\begin_inset Formula $f$
\end_inset

 can be pulled over 
\begin_inset Formula $\sum_{D}$
\end_inset

 as follows:
\begin_inset Formula 
\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{$varSigma $! P$! $! $to $! P$! $varSigma}\\
 & =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_inset


\begin_inset Note Note
status collapsed

\begin_layout Plain Layout
\begin_inset Formula 
\begin{equation}
\begin{array}{l}
\sum_{D}P\sulut Sf=\sum_{D}\sulut{\sulut{S-1}Q\sulut S+P\sulut 1}f\hfill\text{polynomial division}\\
\quad\quad=EQ\sulut Sf+\sum_{D}P\sulut 1f\hfill\text{near bijectivity}\\
\quad\quad=EQ\sulut Sf+\widetilde{\smash{P\sulut 1}}f+P\sulut 1\sum_{D}f\quad\quad\text{repeat near commutation}
\end{array}\label{OLD$varSigma P$to P$varSigma}
\end{equation}

\end_inset


\end_layout

\end_inset


\end_layout

\begin_layout 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 
\begin_inset Formula $\binom{m}{n}=0$
\end_inset

 unless 
\begin_inset Formula $0\leq n\leq m$
\end_inset

 which implies an extensibility 
\begin_inset Formula $\sum_{n=0}^{m}\binom{m}{n}f_{n,m}=\sum_{n\in\mathbb{Z}}\binom{m}{n}f_{n,m}$
\end_inset

 assuming 
\begin_inset Formula $f$
\end_inset

 is extensible.
 Justifying such extension is often easier than cancelling the error terms
 (see example 
\begin_inset CommandInset ref
LatexCommand ref
reference "Fibonacci"
plural "false"
caps "false"
noprefix "false"

\end_inset

).
\end_layout

\begin_layout Example
\begin_inset Formula 
\[
\sum_{m=0}^{k}\sum_{n=0}^{m}f_{m,n}=\sum_{n=0}^{k}\sum_{m=n}^{k}f_{m,n}
\]

\end_inset


\begin_inset CommandInset label
LatexCommand label
name "swap nested"

\end_inset

First consider the left hand side 
\begin_inset Formula $\mathcal{L}_{k}=\sum_{m=0}^{k}l_{m}=\sum_{m=0}^{k}\sum_{n=0}^{m}f_{m,n}$
\end_inset

 where we have named summand as 
\begin_inset Formula $l_{m}$
\end_inset

.
 Obviously 
\begin_inset Formula $\sulut{K-1}l_{m}\approx0$
\end_inset

 with 
\begin_inset Formula $K$
\end_inset

 denoting a shift w.r.t.
 
\begin_inset Formula $k$
\end_inset

.
 This recurrence has no multiplication by 
\begin_inset Formula $m$
\end_inset

 so we directly proceed to pull it over 
\begin_inset Formula $\sum_{m=0}^{k}$
\end_inset

 to get a recurrence for 
\begin_inset Formula $\mathcal{L}_{k}$
\end_inset

.
 No shift w.r.t.
 
\begin_inset Formula $m$
\end_inset

 is present either so we skip near bijectivity.
 Near commutation error for 
\begin_inset Formula $K$
\end_inset

 is (when 
\begin_inset Formula $k\geq0$
\end_inset

)
\begin_inset Formula 
\[
\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}.
\]

\end_inset

Hence 
\begin_inset Formula $\sulut{K-1}\mathcal{L}_{k}-Kl_{k}\approx0$
\end_inset

, which is a conclusion of the following specialization of the generic derivatio
n 
\begin_inset CommandInset ref
LatexCommand ref
reference "$varSigma $! P$! $! $to $! P$! $varSigma"
plural "false"
caps "false"
noprefix "false"

\end_inset


\begin_inset Formula 
\[
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}.
\]

\end_inset


\end_layout

\begin_layout Example
Next consider the right hand side 
\begin_inset Formula $\mathcal{R}_{k}=\sum_{n=0}^{k}r_{k,n}=\sum_{n=0}^{k}\sum_{m=n}^{k}f_{m,n}$
\end_inset

.
 Obviously 
\begin_inset Formula $\sulut{K-1}f_{m,n}\approx0$
\end_inset

 and like above this propagates to 
\begin_inset Formula $\sulut{K-1}r_{k,n}-Kf_{k,n}\approx0$
\end_inset

.
 The second propagation from 
\begin_inset Formula $r_{k,n}$
\end_inset

 to 
\begin_inset Formula $\mathcal{R}_{k}$
\end_inset

 is also very similar but here we can observe how near commutation error
 duplicates a parameter:
\begin_inset Formula 
\[
\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}
\]

\end_inset

where 
\begin_inset Formula $a$
\end_inset

 is 
\begin_inset Formula $r$
\end_inset

 or 
\begin_inset Formula $f$
\end_inset

.
 With that 
\begin_inset Formula $\sulut{K-1}r_{k,n}\approx Kf_{k,n}$
\end_inset

 implies 
\begin_inset Formula $\sulut{K-1}\mathcal{R}_{k}-Kr_{k,k}\approx Kl_{k}-Kf_{k,k}$
\end_inset

 where name 
\begin_inset Formula $l_{k}=\sum_{n=0}^{k}f_{k,n}$
\end_inset

 is reused.
\end_layout

\begin_layout Example
Finally we combine recurrences of 
\begin_inset Formula $\mathcal{L}$
\end_inset

 and 
\begin_inset Formula $\mathcal{R}$
\end_inset

 to get 
\begin_inset Formula $\sulut{K-1}\sulut{\mathcal{L}_{k}-\mathcal{R}_{k}}\approx Kr_{k,k}-Kf_{k,k}$
\end_inset

.
 The right hand side evaluates to 0 which is sufficient and necessary to
 using this recurrence to prove the induction step of 
\begin_inset Formula $\mathcal{L}_{k}-\mathcal{R}_{k}=0\s\forall k\geq0$
\end_inset

.
 The remaining base case 
\begin_inset Formula $\mathcal{L}_{0}-\mathcal{R}_{0}=0$
\end_inset

 is again easy as all the summations range over 
\begin_inset Formula $\left\{ 0\right\} $
\end_inset

.
\end_layout

\begin_layout Standard
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 
\begin_inset Formula $f_{m}$
\end_inset

 by 
\begin_inset Formula $g_{m,n}:=f_{m+an+b}$
\end_inset

 where 
\begin_inset Formula $n$
\end_inset

 is a fresh variable and 
\begin_inset Formula $a,b\in\mathbb{Z}$
\end_inset

 are explicit constants.
 Every recurrence of 
\begin_inset Formula $f$
\end_inset

 translates to a recurrence of 
\begin_inset Formula $g$
\end_inset

 by substituting 
\begin_inset Formula $m$
\end_inset

 by 
\begin_inset Formula $m+an+b$
\end_inset

.
 Indeed 
\begin_inset Formula $\sulut{m+1}+an+b=\sulut{m+an+b}+1$
\end_inset

 implies that substitution 
\begin_inset Formula $\left\{ m\mapsto m+an+b\right\} $
\end_inset

 does not affect shifts in recurrences of 
\begin_inset Formula $f_{m}$
\end_inset

.
 Corresponding to an added variable 
\begin_inset Formula $n$
\end_inset

 we also find an additional equation 
\begin_inset Formula $\sulut{N-M^{a}}g_{m,n}\approx0$
\end_inset

 if 
\begin_inset Formula $a>0$
\end_inset

, or 
\begin_inset Formula $\sulut{NM^{-a}-1}g_{m,n}\approx0$
\end_inset

 if 
\begin_inset Formula $a<0$
\end_inset

.
 Here and below 
\begin_inset Formula $M$
\end_inset

 shifts 
\begin_inset Formula $m$
\end_inset

 and 
\begin_inset Formula $N$
\end_inset

 shifts 
\begin_inset Formula $n$
\end_inset

.
 General affine substitutions are treated in section 
\begin_inset CommandInset ref
LatexCommand ref
reference "Substitute"
plural "false"
caps "false"
noprefix "false"

\end_inset

.
\end_layout

\begin_layout Example
\begin_inset Formula 
\[
\sum_{n=0}^{m}f_{n}=\sum_{n=0}^{m}f_{m-n}
\]

\end_inset

Write 
\begin_inset Formula $F^{m}$
\end_inset

 for the left hand side, 
\begin_inset Formula $G^{m}$
\end_inset

 for right, and 
\begin_inset Formula $g_{n}^{m}=f_{m-n}$
\end_inset

.
 We have the trivial 
\begin_inset Formula $\sulut{M-1}f_{n}\approx0$
\end_inset

 that propagates to 
\begin_inset Formula $\sulut{M-1}F^{m}-Mf_{m}\approx0$
\end_inset

 as in previous example 
\begin_inset CommandInset ref
LatexCommand ref
reference "swap nested"
plural "false"
caps "false"
noprefix "false"

\end_inset

.
 Next 
\begin_inset Formula $g_{n}^{m}=f_{m+\sulut{-1}n+0}$
\end_inset

 and as discussed above we find 
\begin_inset Formula $\sulut{NM-1}g_{n}^{m}\approx0$
\end_inset

.
 To propagate this we compute the relevant bijectivity and commutation errors:
\begin_inset Formula 
\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*}

\end_inset

The first equation is used with 
\begin_inset Formula $a_{n}^{m}=Mg_{n}^{m}$
\end_inset

 and the second with 
\begin_inset Formula $a_{n}^{m}=g_{n}^{m}$
\end_inset

 in the calculation specialized from 
\begin_inset CommandInset ref
LatexCommand ref
reference "$varSigma $! P$! $! $to $! P$! $varSigma"
plural "false"
caps "false"
noprefix "false"

\end_inset


\begin_inset Formula 
\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*}

\end_inset

Hence 
\begin_inset Formula $\sulut{M-1}G^{m}-Mg_{0}^{m}\approx0$
\end_inset

.
 The final propagation gives 
\begin_inset Formula $\sulut{M-1}\sulut{F^{m}-G^{m}}\approx M\sulut{f_{m}-g_{0}^{m}}$
\end_inset

 where of course 
\begin_inset Formula $f_{m}-g_{0}^{m}=0$
\end_inset

.
 The proof finishes as in earlier examples.
\end_layout

\begin_layout Subsection
Propagation to operator polynomial 
\begin_inset CommandInset label
LatexCommand label
name "Poly"

\end_inset


\end_layout

\begin_layout Definition
Given an operator polynomial 
\begin_inset Formula $P$
\end_inset

 and sequence term 
\begin_inset Formula $f$
\end_inset

 we propagate recurrences 
\begin_inset Formula $F$
\end_inset

 of 
\begin_inset Formula $f$
\end_inset

 to those of 
\begin_inset Formula $Pf$
\end_inset

 by giving it a formal name 
\begin_inset Formula $h$
\end_inset

 and eliminating 
\begin_inset Formula $f$
\end_inset

 from 
\begin_inset Formula $F\cup\left\{ h\approx Pf\right\} $
\end_inset

.
\end_layout

\begin_layout Standard
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.
\end_layout

\begin_layout Example
\begin_inset Formula 
\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*}

\end_inset


\begin_inset FormulaMacro
\newcommand{\aidspace}{\hspace{-10em}}
{\s}
\end_inset

 
\begin_inset FormulaMacro
\newcommand{\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}
{\left[x,X,#1\right]}
\end_inset


\begin_inset Formula 
\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*}

\end_inset

Since the leading factor 
\begin_inset Formula $-\sulut{x+1}^{2}\neq0$
\end_inset

 for 
\begin_inset Formula $x\geq0$
\end_inset

, double step induction proves the claim upto the base cases 
\begin_inset Formula $h_{0}=0$
\end_inset

 and 
\begin_inset Formula $h_{1}=0$
\end_inset

.
\end_layout

\begin_layout Subsection
Propagation to product 
\begin_inset CommandInset label
LatexCommand label
name "Times"

\end_inset


\end_layout

\begin_layout Standard
Consider sequence terms 
\begin_inset Formula $f_{n}$
\end_inset

 and 
\begin_inset Formula $g_{m}$
\end_inset

 with disjoint variable tuples 
\begin_inset Formula $n$
\end_inset

 and 
\begin_inset Formula $m$
\end_inset

.
 The recurrences of their pointwise product 
\begin_inset Formula $f_{n}g_{m}$
\end_inset

 are essentially a union of recurrences of 
\begin_inset Formula $f_{n}$
\end_inset

 and 
\begin_inset Formula $g_{m}$
\end_inset

.
 Namely if 
\begin_inset Formula $Pf_{n}+E\approx0$
\end_inset

 for an operator polynomial 
\begin_inset Formula $P$
\end_inset

 and some error terms 
\begin_inset Formula $E$
\end_inset

, then 
\begin_inset Formula $P\sulut{f_{n}g_{m}}+E\cdot g_{m}\approx0$
\end_inset

 (w.l.o.g.
 there's no 
\begin_inset Formula $m$
\end_inset

 in 
\begin_inset Formula $P$
\end_inset

 nor 
\begin_inset Formula $E$
\end_inset

).
 Similarly for 
\begin_inset Formula $g_{m}$
\end_inset

.
 Now propagation to product can be reduced to propagation to substitution.
\end_layout

\begin_layout Definition
Let 
\begin_inset Formula $f_{n}$
\end_inset

 and 
\begin_inset Formula $g_{n}$
\end_inset

 be sequence terms.
 Their recurrences are propagated to their pointwise product 
\begin_inset Formula $f_{n}g_{n}$
\end_inset

 by propagating to the substitution 
\begin_inset Formula $\left\{ m\mapsto n\right\} f_{n}g_{m}=f_{n}g_{n}$
\end_inset

 according to the next definition 
\begin_inset CommandInset ref
LatexCommand ref
reference "subs. prop. def."
plural "false"
caps "false"
noprefix "false"

\end_inset

.
 Here 
\begin_inset Formula $m$
\end_inset

 are a fresh copy of variables 
\begin_inset Formula $n$
\end_inset

.
 Recurrences of 
\begin_inset Formula $f_{n}g_{m}$
\end_inset

 are those of 
\begin_inset Formula $f_{n}$
\end_inset

 and 
\begin_inset Formula $g_{m}$
\end_inset

 multiplied by 
\begin_inset Formula $g_{m}$
\end_inset

 or 
\begin_inset Formula $f_{n}$
\end_inset

 respectively.
\end_layout

\begin_layout Standard
Before considering general substitutions let's see what should be done in
 the special case of multiplication.
\end_layout

\begin_layout Example
Let 
\begin_inset Formula $f_{n}=n_{1}^{n_{2}}$
\end_inset

 and 
\begin_inset Formula $g_{n}=\binom{n_{1}}{n_{2}}$
\end_inset

.
 We will derive a recurrence of 
\begin_inset Formula $f_{n}g_{n}$
\end_inset

 from the standard recurrences 
\begin_inset Formula 
\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*}

\end_inset

(Unlike the purely stylistic factoring of 
\begin_inset Formula $f_{n}$
\end_inset

, 
\begin_inset Formula $g_{m}$
\end_inset

 etc., I will abuse the factoring of 
\begin_inset Formula $m_{2}+1$
\end_inset

 to shorten the derivation a bit.) Observe that any single shift in the final
 recurrence of 
\begin_inset Formula $f_{n}g_{n}$
\end_inset

 can be written 
\begin_inset Formula 
\[
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}}.
\]

\end_inset

Hence we can pull over 
\begin_inset Formula $\left\{ m\mapsto n\right\} $
\end_inset

 only and all the shift pairs 
\begin_inset Formula $N_{j}M_{j}$
\end_inset

 whereas other 
\begin_inset Formula $N_{j}$
\end_inset

's and 
\begin_inset Formula $M_{j}$
\end_inset

's we must eliminate.
 To this end we add name definitions 
\begin_inset Formula 
\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*}

\end_inset

The new shift indeterminate 
\begin_inset Formula $\widetilde{N}_{j}$
\end_inset

 gets nontrivial commutation relations with both 
\begin_inset Formula $n_{j}$
\end_inset

 and 
\begin_inset Formula $m_{j}$
\end_inset

, namely 
\begin_inset Formula $\widetilde{N}_{j}n_{j}=\sulut{n_{j}+1}\widetilde{N}_{j}$
\end_inset

 and 
\begin_inset Formula $\widetilde{N}_{j}m_{j}=\sulut{m_{j}+1}\widetilde{N}_{j}$
\end_inset

.
 Let's shorten 
\begin_inset Formula $h:=f_{n}g_{m}$
\end_inset

 in the saturation eliminating 
\begin_inset Formula $N_{j}$
\end_inset

 and 
\begin_inset Formula $M_{j}$
\end_inset

:
\begin_inset Formula 
\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*}

\end_inset

Saturation must still consider all superpositions between (
\emph on
F
\emph default
),(
\begin_inset Formula $\Delta$
\end_inset

),(1),(3),(4),(5), except the taken one of (3) and (4), but (5) will remain
 as the only equation without any 
\begin_inset Formula $N_{j}$
\end_inset

 or 
\begin_inset Formula $M_{j}$
\end_inset

.
 Applying the substitution 
\begin_inset Formula $\left\{ m\mapsto n\right\} $
\end_inset

 to it gives
\begin_inset Formula 
\[
\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_inset


\end_layout

\begin_layout Subsection
Propagation to substitution 
\begin_inset CommandInset label
LatexCommand label
name "Substitute"

\end_inset


\end_layout

\begin_layout Standard
\begin_inset Note Note
status collapsed

\begin_layout Example
\begin_inset FormulaMacro
\newcommand{\stirling}[2]{\left\{  \begin{subarray}{c}
#1\\
#2
\end{subarray}\right\}  }
{\{{}_{#2}^{#1}\}}
\end_inset

 Stirling numbers of the first kind 
\begin_inset Formula $\stirling mn=:s$
\end_inset

 are defined by recurrence 
\begin_inset Formula $MNs=\sulut{n+1}Ns+s$
\end_inset

 (and initial values 
\begin_inset Formula $\stirling 00=1$
\end_inset

, 
\begin_inset Formula $\stirling n0=\stirling 0n=0$
\end_inset

 for 
\begin_inset Formula $n>0$
\end_inset

; capitals are shifts).
 But often some linear expressions are substituted to 
\begin_inset Formula $m$
\end_inset

 and 
\begin_inset Formula $n$
\end_inset

, for example 
\begin_inset Formula $\stirling{3a-2b}{a+b-c}$
\end_inset

, and then our method needs recurrences w.r.t.
 
\begin_inset Formula $a,b,c$
\end_inset

.
 Let's see how to derive them.
 Let 
\begin_inset Formula $\sigma=\left\{ \sulut{m,n}\mapsto\sulut{3a-2b,a+b-c}\right\} $
\end_inset

 be the relevant substitution.
 Naïvely applying 
\begin_inset Formula $\sigma$
\end_inset

 to 
\begin_inset Formula $MNs=\sulut{n+1}Ns+s$
\end_inset

 gives 
\begin_inset Formula $\sigma MNs=\sulut{a+b-c+1}\sigma Ns+\sigma s$
\end_inset

 which is not a recurrence of 
\begin_inset Formula $\sigma s$
\end_inset

 due to the presence of 
\begin_inset Formula $\sigma MNs$
\end_inset

 and 
\begin_inset Formula $\sigma Ns$
\end_inset

.
 Instead we shall derive good recurrences of 
\begin_inset Formula $s$
\end_inset

 that transform to recurrences of 
\begin_inset Formula $\sigma s$
\end_inset

 under the application of 
\begin_inset Formula $\sigma$
\end_inset

.
\end_layout

\begin_layout Example
We immediately read off 
\begin_inset Formula $A\sigma=\sigma M^{3}N$
\end_inset

 and 
\begin_inset Formula $B\sigma=\sigma M^{-2}N$
\end_inset

 and 
\begin_inset Formula $C\sigma=\sigma N^{-1}$
\end_inset

.
 So 
\begin_inset Formula $M^{3}N$
\end_inset

, 
\begin_inset Formula $M^{-2}N$
\end_inset

 and 
\begin_inset Formula $N^{-1}$
\end_inset

 can be pulled out of 
\begin_inset Formula $\sigma$
\end_inset

.
 Let's call them 
\begin_inset Formula $\widetilde{A}$
\end_inset

, 
\begin_inset Formula $\widetilde{B}$
\end_inset

 and 
\begin_inset Formula $\widetilde{C}$
\end_inset

 respectively, which we formally express by the equations:
\begin_inset Formula 
\begin{align*}
0 & \approx M^{3}Ns-\widetilde{A}s & \sulut A\\
0 & \approx\widetilde{B}M^{2}s-Ns & \sulut B\\
0 & \approx\widetilde{C}Ns-s & \sulut C
\end{align*}

\end_inset

Now we find the good recurrences of 
\begin_inset Formula $s$
\end_inset

 by eliminating 
\begin_inset Formula $M,N$
\end_inset

 in favor of 
\begin_inset Formula $\widetilde{A},\widetilde{B},\widetilde{C}$
\end_inset

 and multiplier indeterminates.
 In this example we also keep track of simplification to see when 
\begin_inset Formula $M$
\end_inset

 and 
\begin_inset Formula $N$
\end_inset

 are fully eliminated.
 
\begin_inset Formula 
\begin{align*}
0 & \approx MNs-\sulut{n+1}Ns-s & \sulut 0 & \text{ by definition of }s\\
0 & \approx Ms-ns-\widetilde{C}s & \sulut 1 & =\widetilde{C}\sulut 0-M\sulut C;\s\widetilde{C}\sulut{n+1}=n\widetilde{C}\text{ since }\widetilde{C}\text{ is }N^{-1}
\end{align*}

\end_inset

Now (0) and (1) can be superposed to derive “
\begin_inset Formula $\sulut 0-N\sulut 1$
\end_inset

”.
 In that we do not have to multiply/shift (0) and hence it can be replaced
 by the conclusion that is actually a duplicate of 
\begin_inset Formula $\sulut C$
\end_inset

.
 Consequently (0) won't participate in future inferences.
\begin_inset Formula 
\begin{align*}
0 & \approx M^{3}s-\widetilde{A}\widetilde{C}s & \sulut 2 & =\widetilde{C}\sulut A-M^{3}\sulut C;\s\sulut 2\&\sulut C\text{ simplify \ensuremath{\sulut A} to triviality}\\
0 & \approx M^{2}\sulut{\widetilde{C}+n}s-\widetilde{A}\widetilde{C}s & \sulut{2'} & =\sulut 2-M^{2}\sulut 1\\
0 & \approx M\sulut{\widetilde{C}+n}^{2}s-\widetilde{A}\widetilde{C}s & \sulut{2''} & =\sulut{2'}-M\sulut{\widetilde{C}+n}\sulut 1\text{; note: }M\sulut{\widetilde{C}+n}=\sulut{\widetilde{C}+n}M\\
0 & \approx\sulut{\widetilde{C}+n}^{3}s-\widetilde{A}\widetilde{C}s & \sulut{2'''} & =\sulut{2''}-\sulut{\widetilde{C}+n}^{2}\sulut 1
\end{align*}

\end_inset

I factor 
\begin_inset Formula $\widetilde{C}+n$
\end_inset

 for presentation reasons: e.g.
 as 
\begin_inset Formula $\sulut{\widetilde{C}+n}^{2}=\widetilde{C}^{2}+2n\widetilde{C}-\widetilde{C}+n^{2}$
\end_inset

 the step 
\begin_inset Formula $\sulut{2''}\to\sulut{2'''}$
\end_inset

 would expand to 4.
 Anyhow all the steps are simplifications and eventually we are left with
 
\begin_inset Formula $\sulut B$
\end_inset

, 
\begin_inset Formula $\sulut C$
\end_inset

, 
\begin_inset Formula $\sulut 1$
\end_inset

 and 
\begin_inset Formula $\sulut{2'''}$
\end_inset

.
 Here 
\begin_inset Formula $\sulut{2'''}$
\end_inset

 is already free of 
\begin_inset Formula $M$
\end_inset

 and 
\begin_inset Formula $N$
\end_inset

 but we are about to find another recurrence too.
\begin_inset Formula 
\begin{align*}
0 & \approx-Ns+\widetilde{B}\sulut{\widetilde{C}+n}^{2}s & \sulut 3 & \text{ from simplifying \ensuremath{\sulut B} by \ensuremath{\sulut 1}}\\
0 & \approx\widetilde{C}\widetilde{B}\sulut{\widetilde{C}+n}^{2}s-s & \sulut 4 & =\sulut C+\widetilde{C}\sulut 3
\end{align*}

\end_inset

Now left are (1), 
\begin_inset Formula $\sulut{2'''}$
\end_inset

, (3) and (4).
 We still need to consider superpositions between (1),(3) (that contain
 
\begin_inset Formula $N$
\end_inset

 or 
\begin_inset Formula $M$
\end_inset

) and 
\begin_inset Formula $\sulut{2'''}$
\end_inset

,(4) (that do not)—only commutative case can require shared indeterminate
 as a precondition of superposition.
 All the resulting recurrences can be simplified to triviality as well as
 the one from superposing (1) and (3).
\end_layout

\begin_layout Example
Can we stop with result 
\begin_inset Formula $\sulut{2'''}$
\end_inset

,(4)? That is, after 
\begin_inset Formula $\sulut{2'''}$
\end_inset

 and (4) alone derive nothing with (1) and (3), do their consequences inherit
 this? If not, the computation becomes too long for presentation.
\end_layout

\end_inset


\end_layout

\begin_layout Definition
\begin_inset CommandInset label
LatexCommand label
name "subs. prop. def."

\end_inset

 Let 
\begin_inset Formula $f_{m}$
\end_inset

 be a sequence term with 
\begin_inset Formula $m\in\mathbb{Z}^{d}$
\end_inset

 and let 
\begin_inset Formula $\sigma$
\end_inset

 be an affine substitution sending 
\begin_inset Formula $m_{k}$
\end_inset

 to 
\begin_inset Formula $\sum_{j=1}^{r}s_{kj}n_{j}+a_{k}$
\end_inset

 where all 
\begin_inset Formula $s_{kj},a_{k}\in\mathbb{Z}$
\end_inset

 are explicit constants and 
\begin_inset Formula $n_{j}$
\end_inset

 are variables of the range of 
\begin_inset Formula $\sigma$
\end_inset

.
 Then for each shift 
\begin_inset Formula $N_{j}$
\end_inset

 in the range we have 
\begin_inset Formula $N_{j}\sigma=\sigma M_{1}^{s_{1j}}...M_{d}^{s_{dj}}$
\end_inset

.
 We propagate recurrences of 
\begin_inset Formula $f_{m}$
\end_inset

 to those of 
\begin_inset Formula $\sigma f_{m}$
\end_inset

 as follows.
\end_layout

\begin_layout Definition
We name 
\begin_inset Formula $M_{1}^{s_{1j}}...M_{d}^{s_{dj}}$
\end_inset

 as 
\begin_inset Formula $\widetilde{N}_{j}$
\end_inset

 by introducing the recurrences that make the exponents 
\begin_inset Formula $s_{kj}$
\end_inset

 non-negative: 
\begin_inset Formula 
\[
\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\} .
\]

\end_inset

The new shift indeterminates 
\begin_inset Formula $\widetilde{N}_{j}$
\end_inset

 satisfy the commutation relations 
\begin_inset Formula $\widetilde{N}_{j}m_{k}=\sulut{m_{k}+s_{kj}}\widetilde{N}_{j}$
\end_inset

.
 With these we eliminate 
\begin_inset Formula $M_{j}$
\end_inset

's in favor of 
\begin_inset Formula $\widetilde{N}_{j}$
\end_inset

's from recurrences of 
\begin_inset Formula $f_{m}$
\end_inset

.
 All resulting equations that lack every 
\begin_inset Formula $M_{j}$
\end_inset

 give recurrences of 
\begin_inset Formula $\sigma f_{m}$
\end_inset

 under the operation of 
\begin_inset Formula $\sigma$
\end_inset

 due to the commutation relations 
\begin_inset Formula $\sigma\widetilde{N}_{j}=N_{j}\sigma$
\end_inset

 and 
\begin_inset Formula $\sigma m_{k}=\sulut{\sum_{j=1}^{r}s_{kj}n_{j}+a_{k}}\sigma$
\end_inset

.
\end_layout

\begin_layout Example
\begin_inset Formula 
\[
\sum_{n=0}^{m-1}\binom{n}{m-1-n}=F_{m}:=m^{\text{th}}\text{ Fibonacci number}
\]

\end_inset


\begin_inset CommandInset label
LatexCommand label
name "Fibonacci"

\end_inset

For binomial coefficient we have recurrences 
\begin_inset Formula $\sulut{NM-M-1}\binom{n}{m}\approx0$
\end_inset

 and 
\begin_inset Formula $\binom{n}{m}=\frac{n}{m}\binom{n-1}{m-1}$
\end_inset

 or equivalently 
\begin_inset Formula $\sulut{\sulut{m+1}NM-n-1}\binom{n}{m}\approx0$
\end_inset

.
 We want to propagate these over the substitution 
\begin_inset Formula $\sigma=\left\{ \sulut{n,m}\mapsto\sulut{n,m-1-n}\right\} $
\end_inset

.
 We have 
\begin_inset Formula $N\sigma=\sigma NM^{-1}$
\end_inset

 and 
\begin_inset Formula $M\sigma=\sigma M$
\end_inset

.
 So we introduce the definitions
\begin_inset Formula 
\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*}

\end_inset

Next we eliminate 
\begin_inset Formula $N,M$
\end_inset

 in favor of 
\begin_inset Formula $\widetilde{N},\widetilde{M}$
\end_inset

.
 Here (2) immediately rewrites every 
\begin_inset Formula $M$
\end_inset

 to 
\begin_inset Formula $\widetilde{M}$
\end_inset

 and then (1) becomes 
\begin_inset Formula $\sulut{-N+\widetilde{N}\widetilde{M}}\binom{n}{m}\approx0$
\end_inset

 that rewrites every 
\begin_inset Formula $N$
\end_inset

.
 Consequently we end up with equations
\begin_inset Formula 
\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*}

\end_inset


\end_layout

\begin_layout Example
Next we propagate the recurrence 
\begin_inset Formula $\sulut{NM^{2}-M-1}f_{m}^{n}\approx0$
\end_inset

—that readily lacks multiplier 
\begin_inset Formula $n$
\end_inset

—to summation 
\begin_inset Formula $\sum_{n=0}^{m-1}$
\end_inset

.
 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_inset Formula 
\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*}

\end_inset


\begin_inset Formula 
\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*}

\end_inset

Here 
\begin_inset Formula $\binom{0}{m+1}=0$
\end_inset

 and 
\begin_inset Formula $\binom{m}{0}=1=\binom{m+1}{0}$
\end_inset

 when 
\begin_inset Formula $m\geq0$
\end_inset

.
 The final propagation to difference hence gives 
\begin_inset Formula $\sulut{M^{2}-M-1}\sulut{\sum_{n=0}^{m-1}f_{m}^{n}-F_{m}}\approx0$
\end_inset

 and the claimed equality follows after checking two initial values.
\end_layout

\begin_layout Standard
\begin_inset Note Note
status open

\begin_layout Plain Layout
Holonomic sequence identities like the binomial formula, geometric series,
\begin_inset Formula 
\begin{align*}
 & \sum_{n=1}^{m}n^{2}\binom{m}{n}=2^{m-2}m\sulut{m+1} &  & \sum_{n=0}^{m}\binom{x}{n}\binom{y}{m-n}=\binom{x+y}{m}\\
 & \sum_{n=0}^{m}\sulut{-1}^{m-n}\binom{2m}{n}^{2}=\binom{2m}{m} &  & \sum_{n=0}^{m}\binom{n}{m-1-n}=m^{\text{th}}\text{ Fibonacci number}
\end{align*}

\end_inset

and generalizations by relaxation, e.g.
 Abel's binomial theorem 
\begin_inset Formula 
\[
x^{-1}\sulut{x+y}^{n}=\sum_{k=0}^{n}\binom{n}{k}\sulut{x-ak}^{k-1}\sulut{y+ak}^{n-k}.
\]

\end_inset


\end_layout

\end_inset


\end_layout

\begin_layout Standard
\begin_inset Note Note
status collapsed

\begin_layout Example
Consider 
\begin_inset Formula $\sum_{n=1}^{m}\delta_{j}^{n}f_{n}=f_{j}$
\end_inset

 for 
\begin_inset Formula $1\leq j\leq m$
\end_inset

.
 This looks like it should be in the scope of the method but unfortunately
 it 
\series bold
fails
\series default
: The Dirac 
\begin_inset Formula $\delta$
\end_inset

 is characterized by the relations 
\begin_inset Formula $\sulut{NJ-1}\delta_{j}^{n}=0$
\end_inset

, 
\begin_inset Formula $\sulut{n-j}\delta_{j}^{n}=0$
\end_inset

, and the single initial value 
\begin_inset Formula $\delta_{0}^{0}=1$
\end_inset

.
 To the product 
\begin_inset Formula $\delta_{j}^{n}f_{n}$
\end_inset

 we derive only 
\begin_inset Formula $\sulut{n-j}\delta_{j}^{n}f_{n}=0$
\end_inset

 where the summation variable 
\begin_inset Formula $n$
\end_inset

 cannot be get rid of.
 Testing the near commutation of 
\begin_inset Formula $m$
\end_inset

-shift still gives 
\begin_inset Formula $\sulut{M-1}\sum_{n=1}^{m}\delta_{j}^{n}f_{n}=\delta_{j}^{m+1}f_{m+1}$
\end_inset

 that leads to the final recurrence 
\begin_inset Formula $\sulut{m+1-j}\sulut{M-1}\sulut{\sum_{n=1}^{m}\delta_{j}^{n}f_{n}-f_{j}}=0$
\end_inset

.
 This allows induction over 
\begin_inset Formula $m$
\end_inset

.
 Taking into account that 
\begin_inset Formula $j\leq m$
\end_inset

 and consequently 
\begin_inset Formula $m+1-j\neq0$
\end_inset

, we must consider exactly the initial value 
\begin_inset Formula $m=j$
\end_inset

.
 For the specialized problem 
\begin_inset Formula $\sum_{n=1}^{j}\delta_{j}^{n}f_{n}=f_{j}$
\end_inset

 we are however unable to propagate any recurrence.
\end_layout

\begin_layout Example
A direct induction proof is nevertheless possible:
\begin_inset Formula 
\begin{align*}
f_{j+1} & =:Sf_{j}\quad\text{by definition here, and}\\
\sum_{n=1}^{j+1}\delta_{j+1}^{n}f_{n} & =\delta_{j+1}^{1}f_{1}+\sum_{n=1}^{j}\delta_{j+1}^{n+1}f_{n+1}=\sum_{n=1}^{j}\delta_{j}^{n}Sf_{n}
\end{align*}

\end_inset

So 
\begin_inset Formula $\makeop{claim}\sulut{j,Sf}\Rightarrow\makeop{claim}\sulut{j+1,f}$
\end_inset

.
 We see that the induction step needs a different sequence to apply the
 induction hypothesis on.
 Since 
\begin_inset Formula $f$
\end_inset

 is generic, that is perfectly good, but the recurrence method only deals
 with generic indices, not sequences.
\end_layout

\end_inset


\end_layout

\begin_layout Section
As part of superposition 
\begin_inset CommandInset label
LatexCommand label
name "Integration"

\end_inset


\end_layout

\begin_layout Standard
\begin_inset FormulaMacro
\newcommand{\myrule}{\textsc{Recurse}}
\end_inset

The recurrence propagation method can be used in refutation of an inequation
 such as 
\begin_inset Formula $\Sigma_{D}f\eri t$
\end_inset

 (where 
\begin_inset Formula $\Sigma$
\end_inset

 is a predefined summation symbol and 
\begin_inset Formula $D,f,t$
\end_inset

 are terms).
 A straightforward black-box integration into superposition calculus is
 to try the method to every eligible inequation 
\begin_inset Formula $\Sigma_{D}f\eri t$
\end_inset

 in every clause.
 This can be formulated as an inference rule:
\begin_inset Formula 
\[
\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
\]

\end_inset

The inference finds suitable subterms 
\begin_inset Formula $n$
\end_inset

 to generalize, propagates recurrences w.r.t.
 those 
\begin_inset Formula $n$
\end_inset

 and replaces them with sufficient initial values 
\begin_inset Formula $I$
\end_inset

 according to the final recurrences.
 Term 
\begin_inset Formula $\Sigma_{D}f-t$
\end_inset

 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 
\begin_inset Formula $B$
\end_inset

 reminds about.
\end_layout

\begin_layout Standard
Remarks: 
\begin_inset Formula $I$
\end_inset

 is a finite set of terms.
 We can only hope that they make the clause simpler in place of 
\begin_inset Formula $n$
\end_inset

.
 Inductionless derivation has 
\begin_inset Formula $I=\varnothing$
\end_inset

.
 Elements of 
\begin_inset Formula $I$
\end_inset

 and 
\begin_inset Formula $n$
\end_inset

 can be tuples (optimization over repeating a single assignment form).
 Often terms also outside 
\begin_inset Formula $n$
\end_inset

 are generalized.
 It is sound that 
\begin_inset Formula $n$
\end_inset

 appears in 
\begin_inset Formula $C$
\end_inset

 but chances are that generalization then loses important information.
 Side premises may also tell something about 
\begin_inset Formula $n$
\end_inset

, most usefully bounds.
 The trigger 
\begin_inset Formula $\Sigma_{D}f\eri t$
\end_inset

 can be generalized to 
\begin_inset Formula $a\cdot\Sigma_{D}f+b\eri t$
\end_inset

 with 
\begin_inset Formula $\cdot$
\end_inset

,+ interpreted.
\end_layout

\begin_layout Example
(Fulfillment of 
\begin_inset CommandInset ref
LatexCommand ref
reference "swap nested"
plural "false"
caps "false"
noprefix "false"

\end_inset

.) Consider the clauses 
\begin_inset Formula $0\leq\kappa$
\end_inset

 and 
\begin_inset Formula 
\[
\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
\]

\end_inset

where 
\begin_inset Formula $0,\kappa,f,\left[\cdot,\cdot\right],\leq,\Sigma$
\end_inset

 are function symbols and 
\begin_inset Formula $\lambda\cdot.\cdot$
\end_inset

 forms an anonymous function.
 We assume presence of also other clauses that define 
\begin_inset Formula $\leq$
\end_inset

 (integer arithmetic) and 
\begin_inset Formula $\Sigma$
\end_inset

 (commutative groups).
 The inequality clause here has a syntactic form that triggers the 
\begin_inset Formula $\myrule$
\end_inset

 rule.
\end_layout

\begin_layout Example
In the propagation part we'll want to consider recurrences w.r.t.
 
\begin_inset Formula $\kappa$
\end_inset

 but 
\begin_inset Formula $\kappa$
\end_inset

 is a constant.
 Hence we generalize 
\begin_inset Formula $\kappa$
\end_inset

 to a variable 
\begin_inset Formula $k$
\end_inset

 and try to prove the stronger claim 
\begin_inset Formula 
\[
\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}}).
\]

\end_inset

Its instance with 
\begin_inset Formula $k=\kappa$
\end_inset

 will contradict the given clauses but the propagation method will only
 prove it upto initial values of 
\begin_inset Formula $k$
\end_inset

.
 Of course we need a better reason to choose precisesly 
\begin_inset Formula $\kappa$
\end_inset

 to be generalized.
 Only integer subterms in the trigger need to be considered.
 They are 
\begin_inset Formula $0,\kappa,m,n,fmn$
\end_inset

.
 Last three contain bound variables 
\begin_inset Formula $m,n$
\end_inset

 and hence cannot be generalized.
 There's little point generalizing the interpreted 0.
 So 
\begin_inset Formula $\kappa$
\end_inset

 was the only option.
\end_layout

\begin_layout Example
Finding recurrences is done in the example 
\begin_inset CommandInset ref
LatexCommand ref
reference "swap nested"
plural "false"
caps "false"
noprefix "false"

\end_inset

.
 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 
\begin_inset Formula $\left[0,\kappa+1\right]\setminus\left[0,\kappa\right]$
\end_inset

 that should be simplified to 
\begin_inset Formula $\left\{ \kappa+1\right\} $
\end_inset

.
 The simplification machinery of superposition can be reused as follows.
 Add to the proof state the formula 
\begin_inset Formula $a\in\left[0,\kappa+1\right]\wedge a\not\in\left[0,\kappa\right]\Leftrightarrow b$
\end_inset

 where constant 
\begin_inset Formula $a$
\end_inset

 represents an arbitrary test point and role of constant 
\begin_inset Formula $b$
\end_inset

 is to guarantee soundness.
 Then wait for 
\begin_inset Formula $a\approx\kappa+1\Leftrightarrow b$
\end_inset

 to appear (in its clausified form; see subsection 
\begin_inset CommandInset ref
LatexCommand ref
reference "Enumerate"
plural "false"
caps "false"
noprefix "false"

\end_inset

).
\end_layout

\begin_layout Example
In the end one recurrence is found and it is 
\begin_inset Formula $T_{k+1}-T_{k}\approx0$
\end_inset

 while 
\begin_inset Formula $\forall k\s\sulut{0\leq k\Rightarrow T_{k}\approx0}$
\end_inset

 is the generalization to prove.
 By induction 
\begin_inset Formula $0\approx T_{0}\Rightarrow\forall k\s\sulut{0\leq k\Rightarrow T_{k}\approx0}$
\end_inset

 where the recurrence told the number (1) of initial values 
\begin_inset Formula $\left\{ 0\right\} $
\end_inset

 and the constraint of 
\begin_inset Formula $k$
\end_inset

 
\begin_inset Formula $\sulut{0\leq k}$
\end_inset

 told their offset.
 But the generalized goal was contradictory so 
\begin_inset Formula $\myrule$
\end_inset

 concludes
\begin_inset Formula 
\[
\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.
\]

\end_inset


\end_layout

\begin_layout Example
Now simplification should take over and rewrite 
\begin_inset Formula $\Sigma_{\left[0,0\right]}F\to\Sigma_{\left\{ 0\right\} }F\to F0$
\end_inset

.
 This reduces the just obtained inequation clause to 
\begin_inset Formula $f00\eri f00$
\end_inset

 that shows the clause set to be contradictory.
\end_layout

\begin_layout Standard
I proceed to give heuristics to solve issues that must be considered in
 this kind of integration.
 We must address how to choose subterms 
\begin_inset Formula $n$
\end_inset

 to generalize and how to initially find recurrence equations.
 Moreover we will specify how we try to enumerate set expressions—a detail
 we skipped about propagation to sums in 
\begin_inset CommandInset ref
LatexCommand ref
reference "Sum"
plural "false"
caps "false"
noprefix "false"

\end_inset

.
 But first, let us not forget the obvious prerequisite of detecting a theory
 of commutative groups or rings.
\end_layout

\begin_layout Subsection
Theory detection
\end_layout

\begin_layout Standard
To find e.g.
 a binary function I'm going to consider as candidates all function symbols
 with parameters—form 
\begin_inset Formula $f\sulut{\tuple p,\cdot,\tuple r,\cdot,\tuple t}$
\end_inset

 with constant term tuples 
\begin_inset Formula $\tuple p,\tuple r,\tuple t$
\end_inset

—that appear in the input clauses.
 These forms are motivated by encoding of types as parameters (like 
\begin_inset Formula $+\sulut{\makeop{type},\cdot,\cdot}$
\end_inset

) and lifting of group operations to, say, quotient (like 
\begin_inset Formula $\makeop{lift}\sulut{+_{\makeop{base}},\cdot,\cdot}$
\end_inset

).
\end_layout

\begin_layout Standard
When I ask to test or check an expression (clause) 
\begin_inset Formula $C$
\end_inset

, I mean to first look for it syntactically.
 If that is unsuccessful, 
\begin_inset Formula $\neg C$
\end_inset

 is then attempted to be refuted by running another instance of the prover
 on it a short while.
\end_layout

\begin_layout Itemize
I assume a syntactic criterion to detect summation symbols 
\begin_inset Formula $\Sigma$
\end_inset

.
 The internal form is then normalized, e.g.
 term 
\begin_inset Formula $\makeop{sum}\sulut{f,a,b}$
\end_inset

 could become 
\begin_inset Formula $\Sigma_{\left[a,b\right[}f$
\end_inset

.
 (I need a hard coded criterion because I feel that defining properties
 of 
\begin_inset Formula $\Sigma$
\end_inset

 are easily stated in unforeseenable ways.)
\end_layout

\begin_layout Itemize
I assume access to defining properties of 
\begin_inset Formula $\Sigma$
\end_inset

 and as by-product to constants +,0 as well as to their commutative monoid
 axioms.
 Needed properties are:
\end_layout

\begin_deeper
\begin_layout Enumerate
\begin_inset CommandInset label
LatexCommand label
name "sum 0"

\end_inset


\begin_inset Formula $\Sigma_{A}f=0\Leftarrow\forall a\in A.\s fa=0$
\end_inset


\end_layout

\begin_layout Enumerate
\begin_inset CommandInset label
LatexCommand label
name "sum 1"

\end_inset


\begin_inset Formula $\Sigma_{\left\{ a\right\} }f=fa$
\end_inset


\end_layout

\begin_layout Enumerate
\begin_inset CommandInset label
LatexCommand label
name "sum AΔB"

\end_inset


\begin_inset Formula $\Sigma_{A}f+\Sigma_{B\setminus A}f=\Sigma_{B}f+\Sigma_{A\setminus B}f$
\end_inset

 when 
\begin_inset Formula $\set{a\in A\cup B}{fa\neq0}$
\end_inset

 is finite
\end_layout

\begin_layout Enumerate
\begin_inset CommandInset label
LatexCommand label
name "sum f+g"

\end_inset


\begin_inset Formula $\Sigma_{A}\sulut{f+g}=\Sigma_{A}f+\Sigma_{A}g$
\end_inset

 when 
\begin_inset Formula $\set{a\in A}{fa\neq0\text{ or }ga\neq0}$
\end_inset

 is finite
\end_layout

\begin_layout Enumerate
\begin_inset CommandInset label
LatexCommand label
name "sum other"

\end_inset

Definition in terms of this normal form, e.g.
 
\begin_inset Formula $\makeop{sum}\sulut{f,a,b}=\Sigma_{\left[a,b\right[}f$
\end_inset

.
\end_layout

\end_deeper
\begin_layout Itemize
Find unary 
\begin_inset Formula $-$
\end_inset

 s.t.
 
\begin_inset Formula $\forall a.\s{-}a+a=0$
\end_inset

, or binary 
\begin_inset Formula $-$
\end_inset

 s.t.
 
\begin_inset Formula $\forall a,b.\s a-b+b=a$
\end_inset

, or verify cancellation 
\begin_inset Formula $\forall a,b,c\s\sulut{a+c=b+c\Rightarrow a=b}$
\end_inset

 and complete into group.
\end_layout

\begin_layout Itemize
Optionally find distributive binary function: the multiplication.
 Other properties are also useful (I programmed under assumptions of unit
 and commutativity).
\end_layout

\begin_layout Itemize
Detect integers and their operations for induction (already in Zipperposition).
\end_layout

\begin_layout Subsection
Choosing terms to generalize
\end_layout

\begin_layout Standard
Generalizing subterms 
\begin_inset Formula $n$
\end_inset

 in an inequality 
\begin_inset Formula $\neg E_{n}$
\end_inset

 means that we ignore fine structure of these 
\begin_inset Formula $n$
\end_inset

 and look the task of refuting 
\begin_inset Formula $\neg E_{n}$
\end_inset

 as a task of proving 
\begin_inset Formula $\forall n\s E_{n}$
\end_inset

.
 These 
\begin_inset Formula $n$
\end_inset

 become the variables in the propagation steps.
\end_layout

\begin_layout Standard
My generalization heuristic is this.
 First, explicit integer constants (
\begin_inset Formula $0,\pm1,\pm2,...$
\end_inset

) are never generalized.
 All other atomic constants (in the trigger 
\begin_inset Formula $\Sigma_{D}f\eri t$
\end_inset

) of type 
\begin_inset Formula $X$
\end_inset

 are generalized where the group 
\begin_inset Formula $X$
\end_inset

 is range of a 
\begin_inset Formula $\Sigma$
\end_inset

.
 Extending, 
\begin_inset Formula $g\sulut{t_{1},...,t_{n}}\in X$
\end_inset

 is generalized if 
\begin_inset Formula $t_{j}\in\mathbb{Z}$
\end_inset

 is explicit or 
\begin_inset Formula $t_{j}\not\in X$
\end_inset

 for every 
\begin_inset Formula $j$
\end_inset

.
 This is explained by considering a situation in which we do not want to
 generalize: if 
\begin_inset Formula $g:X\to X$
\end_inset

, then 
\begin_inset Formula $g$
\end_inset

 can admit recurrences useful with e.g.
 
\begin_inset Formula $g\sulut{a+b}$
\end_inset

 with 
\begin_inset Formula $a,b$
\end_inset

 generalized.
 However recurrences are useless with 
\begin_inset Formula $g1$
\end_inset

, as 1 is not generalized, and hence 
\begin_inset Formula $g1$
\end_inset

 may be turned into a variable.
\end_layout

\begin_layout Subsection
Choosing initial recurrences
\end_layout

\begin_layout Standard
The general principle is to choose recurrences 
\begin_inset Formula $s_{1}\approx s_{2}$
\end_inset

 from clauses 
\begin_inset Formula $s_{1}\approx s_{2}\vee C$
\end_inset

 when 
\begin_inset Formula $s_{1}\approx s_{2}$
\end_inset

 shares function symbols with the trigger 
\begin_inset Formula $\Sigma_{D}f\eri t$
\end_inset

 or another chosen recurrence.
 (The next heuristic will likely need tuning once I get to realize it.) Starting
 from both sides 
\begin_inset Formula $s_{1},s_{2}$
\end_inset

 of an equation 
\begin_inset Formula $s_{1}\approx s_{2}$
\end_inset

 let the 
\emph on
scope of interpretation
\emph default
 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 
\begin_inset Formula $\Sigma_{D}f\approx t$
\end_inset

.
 For each such 
\begin_inset Formula $g$
\end_inset

 I look for clauses 
\begin_inset Formula $Pg\sulut{x,a}+s\approx0\vee C$
\end_inset

 (when normalized) where the polynomial 
\begin_inset Formula $P$
\end_inset

 operates at (the positions of) free variables 
\begin_inset Formula $x$
\end_inset

, and parameters 
\begin_inset Formula $a$
\end_inset

 match the corresponding parameters in some earlier occurrence of 
\begin_inset Formula $g$
\end_inset

.
 The term sequences 
\begin_inset Formula $x$
\end_inset

 and 
\begin_inset Formula $a$
\end_inset

 may be interleaved, and 
\begin_inset Formula $x$
\end_inset

 is nonempty.
 The 
\begin_inset Formula $s$
\end_inset

 is any term and clause 
\begin_inset Formula $C$
\end_inset

 has no eligible literals.
 I then repeat with top-level function symbols from 
\begin_inset Formula $s$
\end_inset

.
\end_layout

\begin_layout Standard
The goal is to find symbols used to define each 
\begin_inset Formula $g$
\end_inset

 above but unfortunately this naïve search also picks symbols defined by
 any 
\begin_inset Formula $g$
\end_inset

.
 To mitigate this let's consider an auxiliary property “needs definition”
 of function symbols.
 All the starting symbols need definition by default.
 Let then 
\begin_inset Formula $g$
\end_inset

 need definition and consider a clause 
\begin_inset Formula $Pg\sulut{x,a}+s\approx0\vee C$
\end_inset

 as before.
 If it does not represent a proper recurrence—all shifts in 
\begin_inset Formula $P$
\end_inset

 are equal—then the symbols from 
\begin_inset Formula $s$
\end_inset

 may need definition.
 A symbol needs definition in no other situation.
 Moreover say that 
\begin_inset Formula $Pg\sulut{x,a}+s\approx0\vee C$
\end_inset

 provides a definition for 
\begin_inset Formula $g$
\end_inset

.
 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.
\end_layout

\begin_layout Example
In our very first example 
\begin_inset CommandInset ref
LatexCommand ref
reference "indefinite sum ex."
plural "false"
caps "false"
noprefix "false"

\end_inset

 we'd see a trigger 
\begin_inset Formula $\sum_{n=0}^{m}f_{n}\eri g_{m}+f_{0}$
\end_inset

 and two candidate initial recurrences 
\begin_inset Formula $g_{0}\approx0$
\end_inset

 and 
\begin_inset Formula $g_{n+1}\approx g_{n}+f_{n+1}$
\end_inset

.
 Here 
\begin_inset Formula $n$
\end_inset

 is variable, and constant 
\begin_inset Formula $m$
\end_inset

 gets abstracted.
 Function symbols from scope of interpretation are 
\begin_inset Formula $f$
\end_inset

 and 
\begin_inset Formula $g$
\end_inset

 that need definition for now.
 Clause 
\begin_inset Formula $g_{0}\approx0$
\end_inset

 lacks variables and so does not give a recurrence.
 Normalized clause 
\begin_inset Formula $\sulut{N-1}g_{n}-f_{n+1}\approx0$
\end_inset

 provides a proper recurrence for 
\begin_inset Formula $g$
\end_inset

, and as 
\begin_inset Formula $f$
\end_inset

 occurs in this clause, 
\begin_inset Formula $f$
\end_inset

 no longer needs definition.
\end_layout

\begin_layout Subsection
Near bijectivity and commutation 
\begin_inset CommandInset label
LatexCommand label
name "Enumerate"

\end_inset


\end_layout

\begin_layout Standard
To preserve some generality I suggest in section 
\begin_inset CommandInset ref
LatexCommand ref
reference "Sum"
plural "false"
caps "false"
noprefix "false"

\end_inset

 to compute bijectivity and commutation errors by enumerating sets given
 as terms.
 This can be done as follows.
 Let 
\begin_inset Formula $A$
\end_inset

 be a term of set type to enumerate.
 I let the superposition calculus to simplify proposition 
\begin_inset Formula $s\in A$
\end_inset

 into form 
\begin_inset Formula $\bigvee_{j=1}^{m}s\approx a_{j}$
\end_inset

 where 
\begin_inset Formula $s$
\end_inset

 is a large Skolem symbol and 
\begin_inset Formula $a_{j}$
\end_inset

 are any terms.
 To avoid contradiction I put 
\begin_inset Formula $b\Leftrightarrow s\in A$
\end_inset

 instead of 
\begin_inset Formula $s\in A$
\end_inset

 into proof state with 
\begin_inset Formula $b$
\end_inset

 being a fresh small unselectable constant.
 Then I wait for 
\begin_inset Formula 
\[
\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\} 
\]

\end_inset

to appear.
 (Cnf stands for clause normal form.) Finally I check 
\begin_inset Formula $a_{i}\eri a_{j}$
\end_inset

 for 
\begin_inset Formula $i\neq j$
\end_inset

 by refuting each 
\begin_inset Formula $a_{i}\approx a_{j}$
\end_inset

 in turn.
 Afterwards 
\begin_inset Formula $a_{1},...,a_{m}$
\end_inset

 enumerates 
\begin_inset Formula $A$
\end_inset

.
\end_layout

\begin_layout Subsection
Initial values to induction
\end_layout

\begin_layout Standard
A common case is that variables are natural numbers and we have a final
 recurrence with maximal shift 
\begin_inset Formula $S_{1}^{a_{1}}...S_{k}^{a_{k}}$
\end_inset

.
 Then initial values 
\begin_inset Formula $\bigcup_{j=1}^{k}\set{n\in\mathbb{N}^{k}}{0\leq n_{j}<a_{j}}$
\end_inset

 suffice.
 As a union of stacked hyperplanes that is infinite (unless 
\begin_inset Formula $k\leq1$
\end_inset

) but it corresponds to just 
\begin_inset Formula $\sum_{j=1}^{k}a_{j}$
\end_inset

 substitutions 
\begin_inset Formula $\left\{ n_{j}\mapsto i\right\} $
\end_inset

 for 
\begin_inset Formula $1\leq j\leq k$
\end_inset

 and 
\begin_inset Formula $0\leq i<a_{j}$
\end_inset

.
\end_layout

\begin_layout Standard
General case with multiple recurrences and boundaries would be complex.
 To be useful the final recurrences must have the form 
\begin_inset Formula $Rs\approx0$
\end_inset

 with 
\begin_inset Formula $R$
\end_inset

 an operator polynomial and 
\begin_inset Formula $s=\Sigma_{D}f-t$
\end_inset

 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 
\begin_inset Formula $a=\sulut{a_{1},...,a_{k}}$
\end_inset

 of its maximal monomial 
\begin_inset Formula $S_{1}^{a_{1}}...S_{k}^{a_{k}}$
\end_inset

.
 Let 
\begin_inset Formula $\sqsubseteq$
\end_inset

 be the least translation invariant order on 
\begin_inset Formula $\mathbb{Z}^{k}$
\end_inset

 s.t.
 
\begin_inset Formula $0\sqsubseteq a$
\end_inset

 for each of these exponent tuples 
\begin_inset Formula $a$
\end_inset

.
 Since 
\begin_inset Formula $a\geq0$
\end_inset

 componentwise, 
\begin_inset Formula $\sqsubseteq$
\end_inset

 extends naturally to 
\begin_inset Formula $\sulut{\left\{ -\infty\right\} \cup\mathbb{Z}}^{k}$
\end_inset

.
 Now if 
\begin_inset Formula $X\subseteq\mathbb{Z}^{k}$
\end_inset

 is a convex set on which 
\begin_inset Formula $s\approx0$
\end_inset

 is to be proven, then the needed initial values are 
\begin_inset Formula $\sqsubseteq$
\end_inset

-minimal elements of closure of 
\begin_inset Formula $X$
\end_inset

 in 
\begin_inset Formula $\sulut{\left\{ -\infty\right\} \cup\mathbb{Z}}^{k}$
\end_inset

.
 Except that 
\begin_inset Formula $-\infty$
\end_inset

 of course cannot be used and the corresponding coordinate must be split
 with artificial bounds (like 
\begin_inset Formula $n\leq0$
\end_inset

 and 
\begin_inset Formula $n\geq0$
\end_inset

; 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 
\begin_inset Formula $X$
\end_inset

.
 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.
\end_layout

\begin_layout Section
Related work
\end_layout

\begin_layout Itemize
Zeilberger popularized holonomic sequences and recurrences in proving equations
 of summations 
\begin_inset CommandInset citation
LatexCommand cite
key "basicholo"
literal "false"

\end_inset

.
\end_layout

\begin_layout Itemize
Paule and Schorn implemented WZ algorithm in Mathematica 
\begin_inset CommandInset citation
LatexCommand cite
key "MathematicaWZ"
literal "true"

\end_inset

.
 Koutschan added holonomic systems 
\begin_inset CommandInset citation
LatexCommand cite
key "MathematicaHolo"
literal "false"

\end_inset

.
 (Univariate work of Mallinger 
\begin_inset CommandInset citation
LatexCommand cite
key "inductPhD"
literal "false"

\end_inset

 preceded this.)
\end_layout

\begin_layout Itemize
Mahboubi and Sibut-Pinote formalize holonomic computations from Mathematica
 in Coq as part of formalizing 
\begin_inset Formula $\zeta\sulut 3\not\in\mathbb{Q}$
\end_inset

 
\begin_inset CommandInset citation
LatexCommand cite
key "Coq"
literal "true"

\end_inset

.
\end_layout

\begin_layout Itemize
Harrison implemented WZ certification in HOL Light with Maxima as a backend
 
\begin_inset CommandInset citation
LatexCommand cite
key "HOL:WZ"
literal "true"

\end_inset

.
 Due to division (by 0) in WZ method the proof reconstruction (by analytic
 continuation) is difficult compared to using recurrences here.
\end_layout

\begin_layout Itemize
Chyzak, Kauers and Salvy study meta-theory of a homogeneous version of the
 method here with many more options as monomials 
\begin_inset CommandInset citation
LatexCommand cite
key "close"
literal "true"

\end_inset

.
 Their results apply to the presented method.
\end_layout

\begin_layout Itemize
Koornwinder implemented WZ algorithm and its 
\begin_inset Formula $q$
\end_inset

-analogue in Maple 
\begin_inset CommandInset citation
LatexCommand cite
key "MapleWZ"
literal "false"

\end_inset

.
\end_layout

\begin_layout Itemize
\begin_inset Note Note
status open

\begin_layout Plain Layout
TODO Abel, Ore, Gosper,...
\end_layout

\end_inset


\end_layout

\begin_layout Standard
\begin_inset CommandInset bibtex
LatexCommand bibtex
btprint "btPrintCited"
bibfiles "../bib"
options "plain"

\end_inset


\end_layout

\end_body
\end_document
