#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{stmaryrd}
\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 "palatino" "default"
\font_sans "default" "default"
\font_typewriter "default" "default"
\font_math "libertine-ntxm" "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 true
\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 true
\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 3cm
\topmargin 0cm
\rightmargin 3cm
\bottommargin 0cm
\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\,\boldsymbol{\left|\vphantom{#1#2}\right.}\mathopen{}\,#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 \to}}{#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 Section
Initialization –VN+JB 
\begin_inset CommandInset label
LatexCommand label
name "sec:initialization"

\end_inset


\end_layout

\begin_layout Standard
We assume that the base calculus works with generic logical formulas and
 hence we must first recognize the special structure of the recurrences.
 Interpreted symbols (
\begin_inset Formula $\sum,+,$
\end_inset

numerals) we assume as built in.
 To-be induction variables appear as constants in the negated goal—part
 of the negation procedure Skolemized them—so some integer constant terms
 need to be generalized (internally).
 Finally we must decide which terms represent (multivariate) sequences and
 which clauses represent their recurrences.
\end_layout

\begin_layout Subsection
Theory Detection 
\begin_inset CommandInset label
LatexCommand label
name "Backtheory"

\end_inset


\end_layout

\begin_layout Standard
We require the necessary theory of summation to be predefined (tagged in
 input task or hard coded).
 It would be too fragile to try to recognize this in general.
 Specifically this means inductive theory of integers, axioms for commutative
 group (including multiplication by integers), and definition of summation
 from 0 by 
\begin_inset Formula $\sum_{n=0}^{-1}f_{n}=0$
\end_inset

 and 
\begin_inset Formula $\sum_{n=0}^{m+1}f_{n}=\sum_{n=0}^{m}f_{n}+f_{m+1}$
\end_inset

 even for negative 
\begin_inset Formula $m\in\mathbb{Z}$
\end_inset

.
 Other bounded intervals are then expressed as differences 
\begin_inset Formula $\sum_{n=k}^{m}f_{n}=\sum_{n=0}^{m}f_{n}-\sum_{n=0}^{k-1}f_{n}$
\end_inset

.
\end_layout

\begin_layout Standard
Multiplication (distributive binary operator) may or may not be present.
 We search candidates to it from the negated goal inequation to refute.
 They could be taken to be of the form 
\begin_inset Formula $f\sulut{\tuple p,\cdot,\tuple r,\cdot,\tuple t}$
\end_inset

 with function symbol 
\begin_inset Formula $f$
\end_inset

 and ground (variableless) term tuples 
\begin_inset Formula $\tuple p,\tuple r,\tuple t$
\end_inset

.
 These forms are motivated by encoding of types as parameters (like 
\begin_inset Formula $\times\sulut{\makeop{type},\cdot,\cdot}$
\end_inset

) and lifting of operations (like 
\begin_inset Formula $\makeop{lift}\sulut{\times_{\makeop{base}},\cdot,\cdot}$
\end_inset

) to quotients, products etc.
 For each candidate we try to prove left and right distributivity by syntactical
ly looking for that axiom or running another instance of the prover on it.
 Similarly finding commutativity and unit can also be useful.
\end_layout

\begin_layout Subsection
Term Generalization 
\begin_inset CommandInset label
LatexCommand label
name "sec:term-generalization"

\end_inset


\end_layout

\begin_layout Standard
A straightforward generalization heuristic is this: each non-numeral subterm
 
\begin_inset Formula $s\in\mathbb{Z}$
\end_inset

 of the negated goal is generalized if 
\begin_inset Formula $s$
\end_inset

 is variableless aka ground even after an attempt to generalize its subterms.
 For example in the following integer terms that initially lack variables
 the underlined subterm(s) would be generalized:
\begin_inset Formula 
\[
\underline a\quad123\quad\underline{f\sulut{0,2}}\quad2f\sulut{\underline{g\sulut{-1}},-3\underline a}\quad f\sulut{1,g\sulut{\underline a+1}}
\]

\end_inset


\end_layout

\begin_layout Standard
Now let the subterms 
\begin_inset Formula $\tuple s$
\end_inset

 be chosen to generalization.
 Then the negated goal 
\begin_inset Formula $C\vee t\neq u$
\end_inset

 (as in the 
\noun on
Summation
\noun default
 inference) is transformed to the unnegated generalized goal 
\begin_inset Formula 
\[
\neg C\implies\forall\tuple n\in Z\negthickspace:\sulut{t-u}\left[\tuple s\mapsto\tuple n\right]=0\quad\text{where \ensuremath{Z\subseteq\mathbb{Z}^{k}} collects bounds of \ensuremath{\tuple s}.}
\]

\end_inset

The generalization makes it possible to use induction to prove that the
 goal sequence term 
\begin_inset Formula $\sulut{t-u}\left[\tuple s\mapsto\tuple n\right]$
\end_inset

—a function of 
\begin_inset Formula $\tuple n$
\end_inset

—vanishes on 
\begin_inset Formula $Z$
\end_inset

.
 Instantiating the generalized goal with 
\begin_inset Formula $\tuple n:=\tuple s$
\end_inset

 will refute 
\begin_inset Formula $t\neq u$
\end_inset

 and so conclude 
\begin_inset Formula $C$
\end_inset

.
 Note that conditions 
\begin_inset Formula $C$
\end_inset

 are not transformed and instead literals of 
\begin_inset Formula $\neg C$
\end_inset

 act like all other currently established clauses.
 The set 
\begin_inset Formula $Z$
\end_inset

 represents facts about 
\begin_inset Formula $\tuple s$
\end_inset

 that we find among known clauses including 
\begin_inset Formula $\neg C$
\end_inset

.
 For example in order to get a recurrence for a factorial 
\begin_inset Formula $n_{1}!$
\end_inset

 out of a clause 
\begin_inset Formula $\sulut{m+1}!=\sulut{m+1}m!\vee0\not\leq m$
\end_inset

 we had to find a bounding clause 
\begin_inset Formula $s_{1}\geq0$
\end_inset

 or its generalization.
 The more we know about 
\begin_inset Formula $\tuple s$
\end_inset

 the more recurrences we get.
 On the other hand 
\begin_inset Formula $Z$
\end_inset

 must allow induction so we keep it convex by only considering (some) affine
 bounds of
\begin_inset space ~
\end_inset


\begin_inset Formula $\tuple s$
\end_inset

.
\end_layout

\begin_layout Subsection
Choice of Initial Recurrences 
\begin_inset CommandInset label
LatexCommand label
name "sec:choice-of-initial-recurrences"

\end_inset


\end_layout

\begin_layout Standard
\begin_inset FormulaMacro
\newcommand{\redOp}[1]{{\color{red}{}#1{}}}
{{\color{red}#1}}
\end_inset

 From semantic point of view the recurrences we search are 
\color teal
multivariate
\color inherit
 
\color red
affine
\color inherit
 (or inhomogeneous linear) 
\color blue
finite fixed step
\color inherit
 equations with 
\color purple
polynomial coefficients
\color inherit
.
 A prototypical example is
\end_layout

\begin_layout Standard
\begin_inset Formula 
\[
\sulut{{\color{purple}n^{2}+1}}{\color{red}f}_{{\color{teal}n}{\color{blue}+2}}^{{\color{teal}m}{\color{blue}+1}}\redOp +{\color{purple}m}{\color{red}f}_{{\color{teal}n}{\color{blue}+1}}^{{\color{teal}m}}\redOp -{\color{purple}nm}{\color{red}f}_{{\color{teal}n}}^{{\color{teal}m}{\color{blue}+1}}={\color{red}g}_{{\color{teal}n}}^{{\color{teal}m}}\redOp -{\color{purple}2}{\color{red}h}_{{\color{teal}n}}^{{\color{teal}m}}\redOp +\sulut{{\color{purple}m-n}}{\color{red}h}_{{\color{teal}n}}^{{\color{teal}m}{\color{blue}-1}}.
\]

\end_inset


\end_layout

\begin_layout Standard
Let there be an edge between two equation clauses if they share a sequence
 term with an occurrence on top-level meaning not nested inside an uninterpreted
 function symbol.
 The currently established clauses then form a graph.
 We take as initial recurrences the connected component of the goal (viewed
 after generalization and unnegation).
\end_layout

\begin_layout Standard
A sequence term means here a term of the form 
\begin_inset Formula $f\sulut{\tuple a,\tuple n}$
\end_inset

 where 
\begin_inset Formula $f$
\end_inset

 is an uninterpreted function symbol, 
\begin_inset Formula $\tuple a$
\end_inset

 is tuple of ground terms (variableless parameters to 
\begin_inset Formula $f$
\end_inset

), and 
\begin_inset Formula $\tuple n$
\end_inset

 is tuple of integer variables or affine combinations of them.
 The tuples 
\begin_inset Formula $\tuple a$
\end_inset

 and 
\begin_inset Formula $\tuple n$
\end_inset

 may be interleaved, but 
\begin_inset Formula $\tuple n$
\end_inset

 must be nonempty.
 When it comes to sharing, the 
\begin_inset Formula $f$
\end_inset

 and 
\begin_inset Formula $\tuple a$
\end_inset

 identify the sequence whereas 
\begin_inset Formula $\tuple n$
\end_inset

 may vary.
 If an equation is conditional, say 
\begin_inset Formula $f\sulut{\tuple a,\tuple n}=t\vee C$
\end_inset

, then we only consider sequences in the equation part 
\begin_inset Formula $f\sulut{\tuple a,\tuple n}=t$
\end_inset

.
\end_layout

\begin_layout Standard
In other contexts an analogous step is known as lemma filtering or fact
 selection.
 Optimistically bloat from irrelevant facts is less of an issue here because
 we can only use linear recurrences.
 The just given heuristic does nothing to avoid it.
\end_layout

\begin_layout Standard
Without an implementation it is hard to say how flexibly one must treat
 conditions.
 I can think of three possibilities (+ combinations):
\end_layout

\begin_layout Enumerate
only equations
\end_layout

\begin_layout Enumerate
conditions of equations are collected to 
\begin_inset Formula $D$
\end_inset

 in the final output clause
\end_layout

\begin_layout Enumerate
conditions of equations must be proved during selection (instantiation OK)
\end_layout

\begin_layout Section
Propagation –VN+SD 
\begin_inset CommandInset label
LatexCommand label
name "sec:propagation"

\end_inset


\end_layout

\begin_layout Standard
From linear recurrences of sequence terms 
\begin_inset Formula $f_{n,m}$
\end_inset

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

, we can derive recurrences for 
\begin_inset Formula $f_{n,m}\pm g_{n,m}$
\end_inset

, 
\begin_inset Formula $f_{n,m}\cdot g_{n,m}$
\end_inset

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

 and 
\begin_inset Formula $f_{an+bm,cn+dm}$
\end_inset

 where 
\begin_inset Formula $a,b,c,d$
\end_inset

 are numerals and 
\begin_inset Formula $n,m$
\end_inset

 are variables (there could be more of them).
 This will be achieved by algorithms corresponding to the closure properties
 of holonomic sequences.
 We refer to this as propagation of the recurrences.
\end_layout

\begin_layout Standard
Given a negated goal 
\begin_inset Formula $C\vee t\neq u$
\end_inset

 to refute, we want to find linear recurrences for 
\begin_inset Formula $t-u$
\end_inset

 (after generalizing it to a sequence) that can then be used to inductively
 prove 
\begin_inset Formula $t-u=0$
\end_inset

.
 Starting from the recurrences found in initialization we propagate them
 bottom up along the tree structure of the term 
\begin_inset Formula $t-u$
\end_inset

.
 In each propagation the syntactic fine structure of the terms is ignored
 and deduction is only based on non-commutative Gröbner basis completion,
 of which we will present a quick overview in the specific setting that
 we will use.
 
\end_layout

\begin_layout Subsection
Basic setup of Gröbner Bases
\end_layout

\begin_layout Standard
A (generalized) Gröbner basis is a certain nice generating set of a left-ideal
 of (possibly non-commutative) polynomials.
 Equivalently, we shall view it as a system of polynomial equations which
 is complete for rewriting.
 Given a polynomial equation 
\begin_inset Formula $P=0$
\end_inset

, then for every monomial 
\begin_inset Formula $M$
\end_inset

 we get a rewrite rule as follows.
 Decompose 
\begin_inset Formula $MP=L+R$
\end_inset

 where 
\begin_inset Formula $L$
\end_inset

 is the leading monomial of 
\begin_inset Formula $MP$
\end_inset

 (w.r.t.
 to the chosen monomial ordering) times its coefficient.
 Then 
\begin_inset Formula $L=-R$
\end_inset

 gives rise to a rewrite rule 
\begin_inset Formula $L\to-R$
\end_inset

.
 A system of equations is completed for rewriting once its every consequence
 can be proven by rewriting by these rules.
\end_layout

\begin_layout Standard
For example the system 
\begin_inset Formula $\left\{ ab^{2}=a+b,a^{2}b=a+1\right\} $
\end_inset

 does not prove its consequence 
\begin_inset Formula $a^{2}=b$
\end_inset

 by rewriting (instead one must subtract the equations multiplied by 
\begin_inset Formula $a$
\end_inset

 or 
\begin_inset Formula $b$
\end_inset

).
 Conversely, the system's Gröbner basis 
\begin_inset Formula $\left\{ a^{2}=b,b^{2}=a+1\right\} $
\end_inset

 gives rewrite proofs 
\begin_inset Formula $\smash{ab^{2}\xrightarrow[b^{2}=a+1]{\s}a^{2}+a\xrightarrow[a^{2}=b]{\s}b+a}$
\end_inset

 and 
\begin_inset Formula $\smash{a^{2}b\xrightarrow[a^{2}=b]{\s}b^{2}\xrightarrow[b^{2}=a+1]{\s}a+1}$
\end_inset

.
\end_layout

\begin_layout Definition
We work with non-commutative polynomials over 
\begin_inset Formula $\mathbb{Z}$
\end_inset

 spanned by indeterminates of two types: multiplier and shift.
 We call them operator polynomials because they have the semantics of operating
 to group-valued multivariate sequences, naturally extended from the indetermina
tes:
\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

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

, operates to a sequence 
\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 shift indeterminate with numeral parameters 
\begin_inset Formula $s_{j}\in\mathbb{Z}$
\end_inset

, say 
\begin_inset Formula $S$
\end_inset

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

 by shifting it 
\begin_inset Formula $s_{j}$
\end_inset

 steps 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 for all
\begin_inset space ~
\end_inset


\begin_inset Formula $j$
\end_inset

: 
\begin_inset Formula $\sulut{Sf}\sulut{\makeop n_{1},...,\makeop n_{k}}=f\sulut{\makeop n_{1}+s_{1},...,\makeop n_{k}+s_{k}}$
\end_inset

.
\end_layout

\begin_layout Standard
By declaring that an indeterminate 
\begin_inset Formula $M$
\end_inset

 shifts a variable 
\begin_inset Formula $m$
\end_inset

 we mean that 
\begin_inset Formula $M$
\end_inset

 is a shift indeterminate with single nonzero parameter 1 s.t.
 
\begin_inset Formula $\sulut{Mf}\sulut{...,m,...}=f\sulut{...,m+1,...}$
\end_inset

.
 The operator semantics require the following non-commutation relation between
 
\begin_inset Formula $n_{j}$
\end_inset

 and 
\begin_inset Formula $S$
\end_inset

 of the previous definition:
\begin_inset Formula 
\begin{align*}
\sulut{Sn_{j}f}\sulut{\tuple{\makeop n}} & =\sulut{n_{j}f}\sulut{\tuple{\makeop n}+\tuple s}=\sulut{\makeop n_{j}+s_{j}}f\sulut{\tuple{\makeop n}+\tuple s}=\\
 & =\sulut{\makeop n_{j}+s_{j}}\sulut{Sf}\sulut{\tuple{\makeop n}}=\sulut{\sulut{n_{j}S+s_{j}S}f}\sulut{\tuple{\makeop n}}
\end{align*}

\end_inset

Especially 
\begin_inset Formula $n_{j}$
\end_inset

 and 
\begin_inset Formula $S$
\end_inset

 commute if and only if 
\begin_inset Formula $s_{j}=0$
\end_inset

.
 Obviously multipliers commute with each others and so do shifts too.
 These (non-)commutation relations are part of the symbolic polynomial algebra
 unlike other semantic relations between shift indeterminates.
 For example if 
\begin_inset Formula $N_{j}$
\end_inset

 shifts 
\begin_inset Formula $n_{j}$
\end_inset

, then the product 
\begin_inset Formula $N_{1}N_{2}$
\end_inset

 is different from a shift indeterminate with parameters (1,1,0,...,0) even
 though the semantic operations are the same.
 We need this distinction only with propagation to substitution, and elsewhere
 shifts with single nonzero parameter 1 suffice.
\end_layout

\begin_layout Definition
By monomials we refer only to polynomials 
\begin_inset Formula $n_{1}^{a_{1}}...n_{k}^{a_{k}}S_{1}^{b_{1}}...S_{l}^{b_{l}}$
\end_inset

 where 
\begin_inset Formula $n_{j}$
\end_inset

 are multiplier indeterminates, 
\begin_inset Formula $S_{j}$
\end_inset

 are shift indeterminates, and 
\begin_inset Formula $a_{j},b_{j}\in\mathbb{N}$
\end_inset

 are numerals.
\end_layout

\begin_layout Standard
Due to the (non-)commutation relations polynomials can be written as sums
 of monomials times their integer coefficients.
 This makes working with these non-commutative polynomials quite similar
 to normal commutative ones.
 Though a major difference is that monomials are not closed under multiplication
: 
\begin_inset Formula $N\cdot n^{2}=\sulut{n+1}^{2}\cdot N=n^{2}N+2nN+N$
\end_inset

 is a trinomial with indeterminate 
\begin_inset Formula $N$
\end_inset

 shifting variable 
\begin_inset Formula $n$
\end_inset

.
 This complicates the following definition of monomial order and leading
 monomial that in turn define how to interpret a polynomial equation as
 a rewrite rule.
\end_layout

\begin_layout Definition
A monomial order 
\begin_inset Formula $\preccurlyeq$
\end_inset

 is a well-founded order on monomials s.t.
 multiplication is increasing in largest monomials called leading.
 This means for monomials 
\begin_inset Formula $A,B,C$
\end_inset

 that if 
\begin_inset Formula $A\preccurlyeq B$
\end_inset

, then monomials of 
\begin_inset Formula $CA$
\end_inset

 
\begin_inset Formula $\preccurlyeq$
\end_inset

 leading monomial of 
\begin_inset Formula $CB$
\end_inset

.
 (Cf.
 the term order in superposition which is well-founded and compatible with
 contexts.)
\end_layout

\begin_layout Standard
Buchberger's algorithm to compute Gröbner bases (also in non-commutative
 context) fits to framework of saturating proof calculi.
 It repeatedly derives from polynomial equations 
\begin_inset Formula $P=0$
\end_inset

 and 
\begin_inset Formula $R=0$
\end_inset

 a new one 
\begin_inset Formula $AP-BR=0$
\end_inset

 where coefficient-monomials-products 
\begin_inset Formula $A,B$
\end_inset

 are most general ones (lowest degree) that unify the leading terms of 
\begin_inset Formula $AP$
\end_inset

 and 
\begin_inset Formula $BR$
\end_inset

.
 Unlike many saturation procedures the completion into Gröbner basis always
 terminates with eager simplification.
 The standard short algebraic termination argument 
\begin_inset CommandInset citation
LatexCommand cite
key "wiki:stop"
literal "false"

\end_inset

 from commutative case applies almost verbatim.
\end_layout

\begin_layout Standard
The similarity with superposition eases implementation of Gröbner bases
 in such provers.
 Hence we'll present propagations as applications of elimination by Gröbner
 bases.
 Though alternative methods can be an order of magnitude cheaper on each
 propagation step 
\begin_inset CommandInset citation
LatexCommand cite
key "MathematicaHolo"
literal "false"

\end_inset

.
\end_layout

\begin_layout Definition
\begin_inset CommandInset label
LatexCommand label
name "elimination"

\end_inset

Eliminating indeterminates 
\begin_inset Formula $X_{1},...,X_{k}$
\end_inset

 (among all 
\begin_inset Formula $X_{1},...,X_{m}$
\end_inset

, both multipliers and shifts) from equations 
\begin_inset Formula $E$
\end_inset

 means computing a Gröbner basis of 
\begin_inset Formula $E$
\end_inset

 w.r.t.
 any 
\begin_inset Formula $X_{1},...,X_{k}$
\end_inset

-elimination order.
 Such monomial order must satisfy 
\begin_inset Formula $X_{j}\succ X_{k+1}^{a_{k+1}}...X_{m}^{a_{m}}$
\end_inset

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

.
 A possible choice is to first compare total degree over 
\begin_inset Formula $X_{1},...,X_{k}$
\end_inset

, then over 
\begin_inset Formula $X_{k+1},...,X_{m}$
\end_inset

, and then break ties (reverse) lexicographically.
 The elimination order favors equations without 
\begin_inset Formula $X_{1},...,X_{k}$
\end_inset

, and others we discard.
 
\begin_inset Note Note
status open

\begin_layout Plain Layout
- second last sentence could be out of definition
\end_layout

\begin_layout Plain Layout
- last should be in: only eq.s without 
\begin_inset Formula $X_{1},...,X_{k}$
\end_inset

 interest
\end_layout

\begin_layout Plain Layout
- I failed to find to-the-point (elimination) reference
\end_layout

\begin_layout Plain Layout
- fixing the order does not even make sense as 
\begin_inset Formula $X_{j}$
\end_inset

's vary
\end_layout

\end_inset


\end_layout

\begin_layout Standard
A single operator polynomial 
\begin_inset Formula $P$
\end_inset

 perfectly encodes a linear homogeneous recurrence 
\begin_inset Formula $Pf=0$
\end_inset

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

.
 However we allow heterogeneous recurrences of the form 
\begin_inset Formula $P_{1}f^{1}+...+P_{k}f^{k}=0$
\end_inset

 where 
\begin_inset Formula $f^{1},...,f^{k}$
\end_inset

 are arbitrary different sequence terms.
 We can encode these on demand by single operator polynomials.
 W.l.o.g.
 
\begin_inset Formula $f^{1},...,f^{k}$
\end_inset

 are all the sequence terms needed to express the current recurrences with
 the help of operator polynomials.
 For each 
\begin_inset Formula $f^{j}$
\end_inset

 let 
\begin_inset Formula $n_{j}$
\end_inset

 be a fresh variable (not a parameter of any 
\begin_inset Formula $f^{i}$
\end_inset

).
 Then the polynomial 
\begin_inset Formula $P_{1}n_{1}+...+P_{k}n_{k}$
\end_inset

 encodes 
\begin_inset Formula $P_{1}f^{1}+...+P_{k}f^{k}=0$
\end_inset

 for the purposes of elimination.
\end_layout

\begin_layout Standard
This encoding obviously lacks the operation semantics and e.g.
 
\begin_inset Formula $n_{1}^{2}$
\end_inset

 makes no sense at all (
\begin_inset Formula $f^{1}$
\end_inset

 is group valued).
 However it is easy to see that the standard Gröbner basis computation only
 derives polynomials of the original form 
\begin_inset Formula $P_{1}n_{1}+...+P_{k}n_{k}$
\end_inset

 where no 
\begin_inset Formula $P_{i}$
\end_inset

 contains any 
\begin_inset Formula $n_{j}$
\end_inset

.
 Indeed the encoding polynomial behaves like a vector 
\begin_inset Formula $\sulut{P_{1},...,P_{k}}$
\end_inset

 with uniform componentwise operations.
 The semantics are recovered by first substituting 
\begin_inset Formula $\set{n_{j}\mapsto f^{j}}{1\leq j\leq k}$
\end_inset

.
 Moreover we can conveniently talk about ordering and elimination of sequence
 terms 
\begin_inset Formula $f^{j}$
\end_inset

 by understanding them as references to the corresponding indeterminates
 
\begin_inset Formula $n_{j}$
\end_inset

 that usually remain implicit.
\end_layout

\begin_layout Standard
\begin_inset Note Note
status collapsed

\begin_layout Plain Layout
In all propagation steps a central part is to eliminate certain indeterminates.
 We work with recurrences of the form 
\begin_inset Formula $P_{1}f^{1}+...+P_{k}f^{k}=0$
\end_inset

 where 
\begin_inset Formula $P_{j}$
\end_inset

 are operator polynomials.
 The sequence terms 
\begin_inset Formula $f^{j}$
\end_inset

 behave in calculations formally just like commutative indeterminates (say
 shifts w.r.t.
 fresh variables—there's no semantics involved).
 So general Gröbner bases suffice for us and asking elimination of sequence
 terms makes sense.
\end_layout

\end_inset


\end_layout

\begin_layout Subsection
Addition
\end_layout

\begin_layout Definition
Let 
\begin_inset Formula $f$
\end_inset

 and 
\begin_inset Formula $g$
\end_inset

 be sequence terms and let 
\begin_inset Formula $h$
\end_inset

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

.
 The recurrences 
\begin_inset Formula $F$
\end_inset

 of 
\begin_inset Formula $f$
\end_inset

 and 
\begin_inset Formula $G$
\end_inset

 of 
\begin_inset Formula $g$
\end_inset

 are propagated to those for 
\begin_inset Formula $h$
\end_inset

 by eliminating 
\begin_inset Formula $f$
\end_inset

 and 
\begin_inset Formula $g$
\end_inset

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

.
 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 Example
\begin_inset CommandInset label
LatexCommand label
name "indefinite sum ex."

\end_inset

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

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

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

, for all 
\begin_inset Formula $m\in\mathbb{N}$
\end_inset

.
 The defining recurrence of 
\begin_inset Formula $g$
\end_inset

 can be written index-free as 
\begin_inset Formula $M^{2}g=g+Ma+M^{2}a$
\end_inset

 where the operator indeterminate 
\begin_inset Formula $M$
\end_inset

 shifts 
\begin_inset Formula $m$
\end_inset

.
 Let's also make explicit the defining recurrence of the sum 
\begin_inset Formula $f_{m}:=\sum_{n=0}^{m}a_{n}$
\end_inset

 namely 
\begin_inset Formula $Mf=f+Ma$
\end_inset

.
 Our goal is to prove that 
\begin_inset Formula $h_{m}:=f_{m}-g_{m}-a_{0}$
\end_inset

 is 0.
 To this end we propagate recurrences to 
\begin_inset Formula $h$
\end_inset

 using a total degree driven order suggested in elimination definition 
\begin_inset CommandInset ref
LatexCommand ref
reference "elimination"
plural "false"
caps "false"
noprefix "false"

\end_inset

 with 
\begin_inset Formula $f\prec g$
\end_inset

 (leading terms are bold): 
\begin_inset FormulaMacro
\newcommand{\isZero}{{\color{gray}0={}}}
{{\color{gray}{\scriptstyle 0}\s}}
\end_inset


\begin_inset Formula 
\[
\back 6\begin{array}{lll}
 & \isZero\boldsymbol{M^{2}g}-g-Ma-M^{2}a & \mathrlap{\quad\text{recurrence of }g}\\
-M^{2}\quad\s\s & \isZero\boldsymbol{g}+a_{0}-f+h & \mathrlap{\quad\text{definition of }h}\\
\hline  & \isZero-g-Ma-M^{2}a-a_{0}+\boldsymbol{M^{2}f}+M^{2}h\\
-M & \isZero\boldsymbol{Mf}-f-Ma & \mathrlap{\quad\text{recurrence of }f}\\
\hline  & \isZero-g-Ma-a_{0}+M^{2}h+\boldsymbol{Mf}\\
- & \isZero\boldsymbol{Mf}-f-Ma & \mathrlap{\quad\text{recurrence of }f}\\
\hline  & \isZero-\boldsymbol{g}-a_{0}+M^{2}h+f\\
+ & \isZero\boldsymbol{g}+a_{0}-f+h & \mathrlap{\quad\text{definition of }h}\\
\hline  & \isZero\boldsymbol{M^{2}h}-h
\end{array}
\]

\end_inset

It happens in this example that 
\begin_inset Formula $h_{m+2}-h_{m}=0$
\end_inset

 is the only recurrence lacking 
\begin_inset Formula $f$
\end_inset

 and 
\begin_inset Formula $g$
\end_inset

 so we cut off the rest of the Gröbner basis calculation.
 Since 
\begin_inset Formula $h_{m+2}-h_{m}=0$
\end_inset

 contains only the sequence 
\begin_inset Formula $h$
\end_inset

, we can use it to prove inductive step (of size 2) of 
\begin_inset Formula $\forall m.\s h_{m}=0$
\end_inset

.
 We are then left with the two base cases 
\begin_inset Formula $h_{0}=0$
\end_inset

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

 that the 
\noun on
Summation
\noun default
 inference would postpone to its conclusion without auxiliary symbols as
 
\begin_inset Formula $\sum_{n=0}^{0}a_{n}\neq g_{0}+a_{0}\vee\sum_{n=0}^{1}a_{n}\neq g_{1}+a_{0}$
\end_inset

.
\end_layout

\begin_layout Subsection
Substitution
\end_layout

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

\end_inset

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

 be a sequence term with 
\begin_inset Formula $\tuple 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}^{d'}s_{kj}n_{j}+a_{k}$
\end_inset

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

 are numerals 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

 where 
\begin_inset Formula $M_{k}$
\end_inset

 are shifts in the domain.
 We propagate recurrences of 
\begin_inset Formula $f_{\tuple m}$
\end_inset

 to those of 
\begin_inset Formula $\sigma f_{\tuple 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 recurrences that make the exponents 
\begin_inset Formula $s_{kj}$
\end_inset

 positive: 
\begin_inset Formula 
\[
\widetilde{N}_{j}\prod_{k:\:s_{kj}<0}M_{k}^{-s_{kj}}=\prod_{k:\:s_{kj}>0}M_{k}^{s_{kj}}\quad\text{for }j\in\left\{ 1,...,d'\right\} .
\]

\end_inset

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

 with parameters 
\begin_inset Formula $\sulut{s_{1j},...,s_{dj}}$
\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_{\tuple m}$
\end_inset

.
 The resulting 
\begin_inset Formula $M_{j}$
\end_inset

-free equations give recurrences of 
\begin_inset Formula $\sigma f_{\tuple m}$
\end_inset

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

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

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

.
\end_layout

\begin_layout Subsection
Product
\end_layout

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

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

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

 and 
\begin_inset Formula $\tuple m$
\end_inset

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

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

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

.
 Namely if 
\begin_inset Formula $Pf_{\tuple n}+e=0$
\end_inset

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

 and some excess terms 
\begin_inset Formula $e$
\end_inset

, then 
\begin_inset Formula $P\sulut{f_{\tuple n}g_{\tuple m}}+e\cdot g_{\tuple m}=0$
\end_inset

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

 in 
\begin_inset Formula $P$
\end_inset

 nor 
\begin_inset Formula $e$
\end_inset

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

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

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

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

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

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

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

\end_inset

.
 Here 
\begin_inset Formula $\tuple m$
\end_inset

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

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

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

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

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

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

 respectively.
\end_layout

\begin_layout Subsection
Summation
\end_layout

\begin_layout Definition
\begin_inset CommandInset label
LatexCommand label
name "sum prop."

\end_inset

Consider sequence term 
\begin_inset Formula $f_{m,n}$
\end_inset

 where 
\begin_inset Formula $n$
\end_inset

 and 
\begin_inset Formula $m$
\end_inset

 are single variables while any number of other implicit variables are also
 allowed.
 We propagate recurrences of 
\begin_inset Formula $f_{m,n}$
\end_inset

 to its sum 
\begin_inset Formula $\sum_{n=0}^{m}f_{m,n}$
\end_inset

 as follows.
 Any recurrence 
\begin_inset Formula $Pf_{m,n}+e=0$
\end_inset

 trivially implies 
\begin_inset Formula $\sum_{n=0}^{m}Pf_{m,n}+\sum_{n=0}^{m}e=0$
\end_inset

.
 Here 
\begin_inset Formula $P$
\end_inset

 is any operator polynomial and excess terms 
\begin_inset Formula $e$
\end_inset

 contain sequences other than 
\begin_inset Formula $f_{m,n}$
\end_inset

.
 We then pull 
\begin_inset Formula $P$
\end_inset

 out of 
\begin_inset Formula $\sum_{n=0}^{m}$
\end_inset

 indeterminate by indeterminate.
 All pointwise multiplication commutes with 
\begin_inset Formula $\sum_{n=0}^{m}$
\end_inset

 except multiplication by 
\begin_inset Formula $n$
\end_inset

 that must be eliminated from the recurrences of 
\begin_inset Formula $f_{m,n}$
\end_inset

 to start with.
 Shift 
\begin_inset Formula $N$
\end_inset

 w.r.t.
 
\begin_inset Formula $n$
\end_inset

 is pulled out (and changed to 1) using the telescoping identity
\begin_inset Formula 
\[
\sum_{n=0}^{m}\sulut{N-1}g_{m,n}=g_{m,m+1}-g_{m,0}.
\]

\end_inset

Shift 
\begin_inset Formula $M$
\end_inset

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

 is pulled out using the identity
\begin_inset Formula 
\[
\sum_{n=0}^{m}Mg_{m,n}=M\sum_{n=0}^{m}g_{m,n}-Mg_{m,m}.
\]

\end_inset

Shifts w.r.t.
 variables other than 
\begin_inset Formula $n$
\end_inset

 and 
\begin_inset Formula $m$
\end_inset

 commute with 
\begin_inset Formula $\sum_{n=0}^{m}$
\end_inset

.
\end_layout

\begin_layout Remark
Summation 
\begin_inset Formula $\sum_{n=0}^{m}f_{m,n}$
\end_inset

 is defined given that 
\begin_inset Formula $f_{m,n}$
\end_inset

 is defined when 
\begin_inset Formula $0\leq n\leq m$
\end_inset

.
 This does not imply that 
\begin_inset Formula $\sum_{n=0}^{m}Pf_{m,n}$
\end_inset

 is defined because 
\begin_inset Formula $P$
\end_inset

 could shift 
\begin_inset Formula $n$
\end_inset

 more than 
\begin_inset Formula $m$
\end_inset

.
 Consequently one might have to consider e.g.
 
\begin_inset Formula $\sum_{n=0}^{m-2}Pf_{m,n}$
\end_inset

 instead and add 
\begin_inset Formula $f_{m,m-1}+f_{m,m}$
\end_inset

 retroactive.
 This is awkward and we assume instead that sequence terms are globally
 defined.
 Similar issue plagues propagation to substitution.
\end_layout

\begin_layout Example
This example demonstrates propagations to substitutions and summations.
\end_layout

\begin_layout Example
\begin_inset Formula 
\[
\sum_{n=0}^{m}\binom{n}{m-n}=F_{m+1}\text{ (Fibonacci numbers)}
\]

\end_inset


\begin_inset CommandInset label
LatexCommand label
name "Fibonacci"

\end_inset

Fibonacci numbers are defined by 
\begin_inset Formula $F_{1}=F_{2}=1$
\end_inset

 and 
\begin_inset Formula $\sulut{N^{2}-N-1}F_{n}=0$
\end_inset

 where 
\begin_inset Formula $N$
\end_inset

 shifts variable 
\begin_inset Formula $n$
\end_inset

.
 For binomial coefficient we have recurrences 
\begin_inset Formula $\sulut{NM-M-1}\binom{n}{m}=0$
\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}=0$
\end_inset

.
 Their Gröbner basis (w.r.t.
 total degree order) is 
\begin_inset Formula 
\[
\left\{ NM-M-1,\sulut{m+1}M-n+m,\sulut{n-m+1}N-n-1\right\} .
\]

\end_inset

We want to propagate these over the substitution 
\begin_inset Formula $\sigma=\left\{ \sulut{n,m}\mapsto\sulut{n,m-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}} & =0\label{1}\\
\sulut{\widetilde{M}-M}{\textstyle \binom{n}{m}} & =0\label{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 (
\begin_inset CommandInset ref
LatexCommand ref
reference "2"
plural "false"
caps "false"
noprefix "false"

\end_inset

) immediately rewrites every 
\begin_inset Formula $M$
\end_inset

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

 and then (
\begin_inset CommandInset ref
LatexCommand ref
reference "1"
plural "false"
caps "false"
noprefix "false"

\end_inset

) becomes 
\begin_inset Formula $\sulut{-N+\widetilde{N}\widetilde{M}}\binom{n}{m}=0$
\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}} & =0 &  &  & f_{m,n}:={\textstyle \binom{n}{m-n}}\\
\sulut{-N+\widetilde{N}\widetilde{M}}{\textstyle \binom{n}{m}} & =0\\
\sulut{\widetilde{N}\widetilde{M}^{2}-\widetilde{M}-1}{\textstyle \binom{n}{m}} & =0 &  & \overset{\sigma}{\mapsto} & \sulut{NM^{2}-M-1}f_{m,n} & =0\\
\sulut{\sulut{m+1}\widetilde{N}\widetilde{M}^{2}-n-1}{\textstyle \binom{n}{m}} & =0 &  & \overset{\sigma}{\mapsto} & \sulut{\sulut{m-n+1}NM^{2}-n-1}f_{m,n} & =0\\
\sulut{\sulut{m+1}\widetilde{M}-n+m}{\textstyle \binom{n}{m}} & =0 &  & \overset{\sigma}{\mapsto} & \sulut{\sulut{m-n+1}M+m-2n}f_{m,n} & =0\\
\sulut{\sulut{n-m+1}\widetilde{N}\widetilde{M}-n-1}{\textstyle \binom{n}{m}} & =0
\end{align*}

\end_inset


\end_layout

\begin_layout Example
Next we must eliminate multiplication by 
\begin_inset Formula $n$
\end_inset

 in order to propagate recurrences to 
\begin_inset Formula $\sum_{n=0}^{m}f_{m,n}$
\end_inset

.
 The only recurrence we find is the one we already have: 
\begin_inset Formula $\sulut{NM^{2}-M-1}f_{m,n}=0$
\end_inset

.
 Next we pull out the shift 
\begin_inset Formula $N$
\end_inset

 from 
\begin_inset Formula $\sum_{n=0}^{m}$
\end_inset


\begin_inset Formula 
\[
\sum_{n=0}^{m}NM^{2}f_{m,n}=\sum_{n=0}^{m}M^{2}f_{m,n}+\left\{ n\mapsto m\right\} NM^{2}f_{m,n}-M^{2}f_{m,0}.
\]

\end_inset

Then we pull out the shifts 
\begin_inset Formula $M$
\end_inset


\begin_inset Formula 
\[
\sum_{n=0}^{m}\sulut{M^{2}-M-1}f_{m,n}=
\]

\end_inset


\end_layout

\begin_layout Example
we get
\begin_inset Formula 
\begin{gather*}
\sulut{M^{2}-M-1}\sum_{n=0}^{m}f_{m,n}+\left\{ n\mapsto m\right\} \frac{NM^{2}-M-N^{2}M^{2}+NM}{N-1}Nf_{m,n}-\left\{ n\mapsto0\right\} M^{2}f_{m,n}\\
=\sulut{M^{2}-M-1}\sum_{n=0}^{m}f_{m,n}-\underset{=1}{\underbrace{f_{m+2,m+2}}}+\underset{=1}{\underbrace{f_{m+1,m+1}}}-\underset{=0}{\underbrace{f_{m+2,0}}}
\end{gather*}

\end_inset

which is exactly the same recurrence that defines the (shifted) Fibonacci
 numbers 
\begin_inset Formula $F_{m+1}$
\end_inset

 and consequently also the difference 
\begin_inset Formula $\sum_{n=0}^{m}f_{m,n}-F_{m+1}$
\end_inset

.
\end_layout

\begin_layout Standard
We can derive closed formulas for the propagation result after elimination
 of multiplication by 
\begin_inset Formula $n$
\end_inset

.
 This can help to understand the form of the result while the above simple
 recursive formulas remain a viable way to compute it.
 The telescoping formula amounts to Euclidean division of polynomials by
 
\begin_inset Formula $N-1$
\end_inset

 (and as 
\begin_inset Formula $n$
\end_inset

 is eliminated, 
\begin_inset Formula $N$
\end_inset

 commutes with remaining indeterminates).
 Namely if 
\begin_inset Formula $P\sulut N=\sulut{N-1}Q\sulut N+P\sulut 1$
\end_inset

 then 
\begin_inset Formula $P\sulut Nf_{m,n}+e=0$
\end_inset

 implies
\begin_inset Formula 
\begin{align*}
-\sum_{n=0}^{m}e & =\sum_{n=0}^{m}P\sulut Nf_{m,n}=\sum_{n=0}^{m}\sulut{\sulut{N-1}Q\sulut Nf_{m,n}+P\sulut 1f_{m,n}}=\\
 & =\left\{ n\mapsto m+1\right\} Q\sulut Nf_{m,n}-\left\{ n\mapsto0\right\} Q\sulut Nf_{m,n}+\sum_{n=0}^{m}P\sulut 1f_{m,n}.
\end{align*}

\end_inset

Here all terms except the last summation can be considered as excess to
 be eliminated later.
 The operator polynomial 
\begin_inset Formula $P\sulut 1$
\end_inset

 now contains neither 
\begin_inset Formula $n$
\end_inset

 nor 
\begin_inset Formula $N$
\end_inset

.
 
\end_layout

\begin_layout Standard
Concerning the second identity let 
\begin_inset Formula $\sigma=\left\{ n\mapsto m\right\} $
\end_inset

.
 Then for example 
\begin_inset Formula 
\begin{align*}
\sum_{n=0}^{m}M^{3}f_{m,n} & =M\sum_{n=0}^{m}M^{2}f_{m,n}-M\sigma M^{2}f_{m,n}\\
 & =M^{2}\sum_{n=0}^{m}Mf_{m,n}-M^{2}\sigma Mf_{m,n}-M\sigma M^{2}f_{m,n}\\
 & =M^{3}\sum_{n=0}^{m}f_{m,n}-M\sulut{M^{2}\sigma+M\sigma M+\sigma M^{2}}f_{m,n}
\end{align*}

\end_inset

and in general 
\begin_inset Formula $\sum_{n=0}^{m}M^{a}f_{m,n}-M^{a}\sum_{n=0}^{m}f_{m,n}=-M\sum_{j=0}^{a-1}M^{j}\sigma M^{a-1-j}f_{m,n}$
\end_inset

.
 Since 
\begin_inset Formula $M\sigma=\sigma NM$
\end_inset

 we can rewrite this as
\begin_inset Formula 
\[
M\sum_{j=0}^{a-1}M^{j}\sigma M^{a-1-j}=\sum_{j=0}^{a-1}\sigma N^{j+1}M^{a}=\sigma\frac{N^{a}-1}{N-1}NM^{a}=\sigma\frac{\sulut{NM}^{a}-M^{a}}{N-1}N.
\]

\end_inset

So by linearity, for 
\begin_inset Formula $P\sulut M$
\end_inset

 containing neither 
\begin_inset Formula $n$
\end_inset

 nor 
\begin_inset Formula $N$
\end_inset

 holds
\begin_inset Formula 
\[
\sum_{n=0}^{m}P\sulut Mf_{m,n}-P\sulut M\sum_{n=0}^{m}f_{m,n}=-\sigma\frac{P\sulut{NM}-P\sulut M}{N-1}Nf_{m,n}.
\]

\end_inset


\end_layout

\begin_layout Standard
Combining the previous formulas we can write propagation of a recurrence
 
\begin_inset Formula $0=P\sulut{N,M}f_{m,n}+e$
\end_inset

 in the form
\begin_inset Formula 
\begin{align*}
0=P\sulut{1,M}\sum_{n=0}^{m}f_{m,n} & +\left\{ n\mapsto m\right\} \frac{P\sulut{N,M}-P\sulut{1,M}}{N-1}Nf_{m,n}-{}\\
 & -\left\{ n\mapsto\mathrlap{0}\hphantom{m}\right\} \frac{P\sulut{N,M}-P\sulut{1,M}}{N-1}f_{m,n}-{}\\
 & -\left\{ n\mapsto m\right\} \frac{P\sulut{1,NM}-P\sulut{1,M}}{N-1}Nf_{m,n}+{}\\
 & +\sum_{n=0}^{m}e=\\
=P\sulut{1,M}\sum_{n=0}^{m}f_{m,n} & +\left\{ n\mapsto m\right\} \frac{P\sulut{N,M}-P\sulut{1,NM}}{N-1}Nf_{m,n}-{}\\
 & -\left\{ n\mapsto\mathrlap{0}\hphantom{m}\right\} \frac{P\sulut{N,M}-P\sulut{1,M}}{N-1}f_{m,n}+\sum_{n=0}^{m}e.
\end{align*}

\end_inset


\end_layout

\begin_layout Standard
\begin_inset Note Note
status open

\begin_layout Subsection
Summation via substitution
\end_layout

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

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

.
 Let 
\begin_inset Formula $N$
\end_inset

 shift 
\begin_inset Formula $n$
\end_inset

 and 
\begin_inset Formula $M$
\end_inset

 shift 
\begin_inset Formula $m$
\end_inset

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

 are propagated to 
\begin_inset Formula $F_{m}$
\end_inset

 by first eliminating multiplication by 
\begin_inset Formula $n$
\end_inset

 from them.
 Then using polynomial division a recurrence 
\begin_inset Formula $P\sulut Nf_{n}+e=0$
\end_inset

 implies 
\begin_inset Formula 
\begin{align*}
-\sum_{n=0}^{m}e=\sum_{n=0}^{m}P\sulut Nf_{n} & =\sum_{n=0}^{m}\sulut{\sulut{N-1}Q\sulut N+P\sulut 1}f_{n}=\\
 & =MQ\sulut Mf_{m}-\left\{ n\mapsto0\right\} Q\sulut Nf_{n}+P\sulut 1F_{m}
\end{align*}

\end_inset

where the operator polynomial 
\begin_inset Formula $Q\sulut N$
\end_inset

 is defined by Euclidean division 
\begin_inset Formula $P\sulut N=\sulut{N-1}Q\sulut N+P\sulut 1$
\end_inset

.
 Here we view 
\begin_inset Formula $P$
\end_inset

 and 
\begin_inset Formula $Q$
\end_inset

 as functions of the shift 
\begin_inset Formula $N$
\end_inset

 that commutes with every present indeterminate as the multiplier 
\begin_inset Formula $n$
\end_inset

 is eliminated.
 Telescoping 
\begin_inset Formula $\sum_{n=0}^{m}\sulut{N-1}g_{n}=g_{m+1}-g_{0}$
\end_inset

 explains the last step of the derivation.
 The excess terms 
\begin_inset Formula $e$
\end_inset

, that contain other sequences than 
\begin_inset Formula $f_{n}$
\end_inset

, remain inside the summation waiting a lucky cancellation or a future summation
 propagation step.
\end_layout

\begin_layout Definition
\noindent
Additionally the recurrence 
\begin_inset Formula $\sulut{M-1}F_{m}-Mf_{m}=0$
\end_inset

 is always valid.
 Other variables than 
\begin_inset Formula $m$
\end_inset

 and 
\begin_inset Formula $n$
\end_inset

 can be present.
 General summations 
\begin_inset Formula $\sum_{n=0}^{m}f_{n,m}=\left\{ k\mapsto m\right\} \sum_{n=0}^{k}f_{n,m}$
\end_inset

 are reduced to the above using substitutions like with products.
\end_layout

\end_inset


\end_layout

\begin_layout Subsection
Iteration on Excess Terms
\end_layout

\begin_layout Standard
Let 
\begin_inset Formula $g$
\end_inset

 be the term from the negated goal to be proven 0.
 After propagating along the structure of 
\begin_inset Formula $g$
\end_inset

 we end up with recurrences of the form 
\begin_inset Formula $Pg+e=0$
\end_inset

 where 
\begin_inset Formula $P$
\end_inset

 is an operator polynomial and excess terms 
\begin_inset Formula $e$
\end_inset

 contain sequences other than 
\begin_inset Formula $g$
\end_inset

.
 If 
\begin_inset Formula $e\neq0$
\end_inset

 syntactically—rare in practice—then 
\begin_inset Formula $Pg+e=0$
\end_inset

 is no good for induction.
 A solution is to iterate a full series of propagations on 
\begin_inset Formula $e$
\end_inset

 to find 
\begin_inset Formula $P_{2}e+e_{2}=0$
\end_inset

 and conclude 
\begin_inset Formula $P_{2}Pg-e_{2}=0$
\end_inset

 etc.
 until the excess 
\begin_inset Formula $e,e_{2},...$
\end_inset

 becomes 0.
\end_layout

\begin_layout Standard
We'll impose an order on the sequence terms to accomplish three things.
 First we get a clean definition of which terms in a recurrence are excess.
 Secondly well-foundedness of the order will guarantee termination of the
 iteration of full propagations on excess.
 Moreover the iterations can be interleaved with basic normalizations such
 as 
\begin_inset Formula $\left\{ n\mapsto2m\right\} n\left\{ k\mapsto3n\right\} f_{k}\to2m\left\{ k\mapsto6m\right\} f_{k}$
\end_inset

.
\end_layout

\begin_layout Standard
The sequence terms can be viewed as terms over the first-order alphabet
 with binary function symbol 
\begin_inset Formula $\cdot$
\end_inset

, unary 
\begin_inset Formula $\sum_{n=0}^{a}$
\end_inset

 and 
\begin_inset Formula $\sigma$
\end_inset

 for each affine variable sum 
\begin_inset Formula $a$
\end_inset

 and substitution 
\begin_inset Formula $\sigma$
\end_inset

, and nullary symbol for each variable and each sequence term with uninterpreted
 head.
 Addition + is excluded because as all 
\begin_inset Formula $\cdot,\sum_{n=0}^{a},\sigma$
\end_inset

 are distributive, we normalize recurrences to the form 
\begin_inset Formula $c_{1}t_{1}+....+c_{k}t_{k}=0$
\end_inset

 where 
\begin_inset Formula $c_{j}\in\mathbb{Z}\setminus\left\{ 0\right\} $
\end_inset

 are numeric coefficients and 
\begin_inset Formula $t_{j}$
\end_inset

 are distinct sequence terms in the above additionless alphabet.
\end_layout

\begin_layout Definition
Spine of a sequence term is the sequence term obtained by erasing operator
 polynomial indeterminates from it.
 Precisely this means fully reducing the sequence term by the rewrite rules
\begin_inset Formula 
\begin{align*}
nt,tn & \to t &  & n\text{ is nullary symbol of variable}\\
\sigma t & \to\sigma't &  & \sigma'\text{ is linear part of substitution }\sigma\\
{\textstyle \sum_{n=0}^{a}}t & \to{\textstyle \sum_{n=0}^{a'}}t &  & a'\text{ is linear part of }a
\end{align*}

\end_inset

Here linear part of e.g.
 
\begin_inset Formula $\left\{ n\mapsto2k+1,m\mapsto-3\right\} $
\end_inset

 is 
\begin_inset Formula $\left\{ n\mapsto2k,m\mapsto0\right\} $
\end_inset

.
\end_layout

\begin_layout Standard
It is easy to describe how each propagation step can change the spines of
 the involved sequence terms.
 Let 
\begin_inset Formula $e_{h}$
\end_inset

 denote (the spine of) a term from a recurrence of (term with spine) 
\begin_inset Formula $h\in\left\{ f,g\right\} $
\end_inset

.
 Then propagation to addition 
\begin_inset Formula $f+g$
\end_inset

 has only spines 
\begin_inset Formula $e_{f}$
\end_inset

 and 
\begin_inset Formula $e_{g}$
\end_inset

 in the resulting recurrences.
 Propagation to product 
\begin_inset Formula $fg$
\end_inset

 has 
\begin_inset Formula $fe_{g}$
\end_inset

 and 
\begin_inset Formula $e_{f}g$
\end_inset

.
 Propagation to substitution 
\begin_inset Formula $\sigma f$
\end_inset

 has 
\begin_inset Formula $\sigma e_{f}$
\end_inset

.
 Finally propagation to summation 
\begin_inset Formula $\sum_{n=0}^{m}f$
\end_inset

 has 
\begin_inset Formula $\left\{ n\mapsto0\right\} f$
\end_inset

, 
\begin_inset Formula $\left\{ n\mapsto m\right\} f$
\end_inset

 and 
\begin_inset Formula $\sum_{n=0}^{m}e_{f}$
\end_inset

.
\end_layout

\begin_layout Standard
Since term orders are compatible with contexts, comparing spines by one
 will almost automatically keep excess terms smaller than the main ones
 over propagation steps.
 As per the above consideration, it suffices to additionally demand a term
 order 
\begin_inset Formula $>$
\end_inset

 to satisfy 
\begin_inset Formula $\sum_{n=0}^{m}t>\sigma t$
\end_inset

 for substitutions 
\begin_inset Formula $\sigma$
\end_inset

 and sequence terms 
\begin_inset Formula $t$
\end_inset

.
 Though we'll consider more specific term order which is to later orient
 simplification rules too.
 (Note that the innocent simplifications {
\begin_inset Formula $\sigma\sulut{ts}\to\sigma t\cdot\sigma s$
\end_inset

, 
\begin_inset Formula $\sigma\sigma't\to\sulut{\sigma\circ\sigma'}t$
\end_inset

} cannot be oriented by KBO nor LPO 
\begin_inset CommandInset citation
LatexCommand cite
key "RPO-82,LPO<RPO-83,KBO-03,KBO-09"
literal "false"

\end_inset

.)
\end_layout

\begin_layout Definition
Fix any TKBO 
\begin_inset CommandInset citation
LatexCommand cite
key "TKBO-07"
literal "false"

\end_inset

 with exactly three different weights 
\begin_inset Formula $W\sum_{n=0}^{a}>W\sulut{\cdot}>3W\sigma>0$
\end_inset

 and all argument coefficients 2 (or WPO(max)
\begin_inset space ~
\end_inset


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

\end_inset

 with precedence 
\begin_inset Formula $\sum_{n=0}^{a}\prec\cdot\prec\sigma$
\end_inset

 and positive equal penalties).
 Moreover nullary symbols of variables must have equal weights.
\end_layout

\begin_layout Definition
The excess (partial) order on the sequence terms is obtained by comparing
 the spines of terms using this fixed TKBO.
\end_layout

\begin_layout Definition
Excess terms of a recurrence are all the non-maximal sequence terms of it
 w.r.t.
 the excess order.
\end_layout

\begin_layout Standard
The weights for the excess order are arranged to be compatible with normalizatio
n that pushes substitutions to leafs and pulls summations towards root in
 term tree.
 The resulting normal form is nothing but the typical way of writing sequence
 terms without operator notation.
 It is also the normal form of the rewrite system consisting of the applicable
 associativity and/or commutativity rules of 
\begin_inset Formula $\cdot$
\end_inset

 as well as the following where 
\begin_inset Formula $t,s$
\end_inset

 are sequence terms, 
\begin_inset Formula $a$
\end_inset

 is affine variable sum and 
\begin_inset Formula $\sigma,\sigma'$
\end_inset

 are affine substitutions.
\begin_inset Formula 
\begin{align*}
1t,t1,\left\{ \right\} t & \to t\\
\sulut{\sigma\cup\left\{ n\mapsto a\right\} }t & \to\sigma t &  & \back 3t\text{ lacks variable }n\\
\sulut{\sigma\cup\left\{ n\mapsto a\right\} }n & \to a &  & \back 3n\text{ is variable / its nullary symbol}\\
\sigma\sigma't & \to\sulut{\sigma\circ\sigma'}t\\
\sigma\sulut{ts} & \to\sigma t\cdot\sigma s\\
{\textstyle \sigma\sum_{n=0}^{a}t} & \to{\textstyle \sum_{n=0}^{\sigma a}\sigma t}\\
{\textstyle s\cdot\sum_{n=0}^{a}t} & \to{\textstyle \sum_{n=0}^{a}st} &  & \text{also with \ensuremath{\cdot} flipped}\\
{\textstyle \sum_{n=0}^{c}t} & \to\left\{ n\mapsto0\right\} t+...+\left\{ n\mapsto c\right\} t &  & c\text{ is numeral (adapt if \ensuremath{c<0})}
\end{align*}

\end_inset

These rules (third and last) produce additions which must be interpreted
 as follows.
 Sequence term rule 
\begin_inset Formula $t_{0}\to c_{1}t_{1}+...+c_{k}t_{k}$
\end_inset

 implies rules 
\begin_inset Formula $f\left[t_{0}\right]+R=0\longrightarrow c_{1}f\left[t_{1}\right]+...+c_{k}f\left[t_{k}\right]+R=0$
\end_inset

 on the recurrences where 
\begin_inset Formula $c_{j}$
\end_inset

 are numeral coefficients, 
\begin_inset Formula $f\left[t_{j}\right]$
\end_inset

 is a sequence term with a distinguished subterm 
\begin_inset Formula $t_{j}$
\end_inset

, and 
\begin_inset Formula $R$
\end_inset

 is the sum of the rest of the terms in the recurrence.
 This is analogous to how monomial reductions lift to polynomials in Gröbner
 basis theory.
 It suffices to prove that 
\begin_inset Formula $t_{0}$
\end_inset

 dominates each of 
\begin_inset Formula $t_{1},...,t_{k}$
\end_inset

 individually to conclude termination.
 The reader may then check local confluence to conclude normalizability.
\end_layout

\begin_layout Standard
First rule trio is trivial.
 In the second rule we assumed that removing a binding form substitution
 
\begin_inset Formula $\sigma\cup\left\{ n\mapsto a\right\} $
\end_inset

 lowers its precedence (otherwise the rule must just map to minimizing 
\begin_inset Formula $a$
\end_inset

 instead).
 Third rule needs only 
\begin_inset Formula $\sulut{\sigma\cup\left\{ n\mapsto a\right\} }n>m$
\end_inset

 for variables 
\begin_inset Formula $m$
\end_inset

 in 
\begin_inset Formula $a$
\end_inset

 which holds because 
\begin_inset Formula $n$
\end_inset

 and 
\begin_inset Formula $m$
\end_inset

 have the same weight.
 Combining substitutions 
\begin_inset Formula $\sigma$
\end_inset

 and 
\begin_inset Formula $\sigma'$
\end_inset

 into one 
\begin_inset Formula $\sigma\circ\sigma'$
\end_inset

 decreases weight.
 The only duplicating rule 
\begin_inset Formula $\sigma\sulut{ts}\to\sigma t\cdot\sigma s$
\end_inset

 requires 
\begin_inset Formula $W\sigma+2\sulut{W\sulut{\cdot}+2\sulut{Wt+Ws}}>W\sulut{\cdot}+4W\sigma+4Wt+4Ws$
\end_inset

 that is the assumption 
\begin_inset Formula $W\sulut{\cdot}>3W\sigma$
\end_inset

.
 The three last rules are similarly ordered due to the assumed weight order.
 While comparing spines first, these orientations remain, though possibly
 as non-strict.
 
\begin_inset Note Note
status open

\begin_layout Plain Layout
- We only propagate for maximal excess terms on each round.
\end_layout

\begin_layout Plain Layout
- Usability or its lack for 
\begin_inset Formula $f_{2n+1}-f_{2n}=e_{n}$
\end_inset

.
\end_layout

\begin_layout Plain Layout
- It is important that goal and its subterms are chosen large.
\end_layout

\begin_layout Plain Layout
- Why variables do not clash.
\end_layout

\begin_layout Plain Layout
- 
\begin_inset Formula $\sum_{n=0}^{a}\sum_{m=0}^{b}=\sum_{m=0}^{b}\sum_{n=0}^{a}$
\end_inset


\end_layout

\end_inset


\end_layout

\begin_layout Section
Induction –VN+SD 
\begin_inset CommandInset label
LatexCommand label
name "sec:induction"

\end_inset


\end_layout

\begin_layout Standard
After propagation we consider all recurrences 
\begin_inset Formula $Pg=0$
\end_inset

 of the goal sequence term 
\begin_inset Formula $g$
\end_inset

 to be proven 0.
 In exceptionally lucky cases 
\begin_inset Formula $P=\pm1$
\end_inset

 and we are unconditionally done.
 This naturally happens when the goal is to prove a recurrence that this
 method is about to derive anyway.
 Otherwise we apply induction and leave as conditions the base cases as
 well as invertibility of the leading coefficients.
\end_layout

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

 w.r.t.
 any monomial order.
 Then the values 
\begin_inset Formula $\bigcup_{j=1}^{k}\set{\tuple n\in\mathbb{N}^{k}}{n_{j}<b_{j}}$
\end_inset

 suffice to base cases.
 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}b_{j}$
\end_inset

 one-variable substitutions 
\begin_inset Formula $\left\{ n_{j}\mapsto a\right\} $
\end_inset

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

 and 
\begin_inset Formula $0\leq a<b_{j}$
\end_inset

.
 If our generous generalization produced variables that do not participate
 in induction (their 
\begin_inset Formula $b_{j}=0$
\end_inset

), they are substituted back to their original values.
\end_layout

\begin_layout Standard
If there is more than one applicable final recurrence, we take the intersection
 of their base value sets w.r.t.
 the same arbitrary monomial order.
 This works because induction step w.r.t.
 that order can be taken by recurrence 
\begin_inset Formula $R$
\end_inset

 on nonbase point w.r.t.
 
\begin_inset Formula $R$
\end_inset

 with any final recurrence 
\begin_inset Formula $R$
\end_inset

.
 (If recurrences have different side conditions, then there might not be
 an optimal base-cases+conditions combination but rather many incomparable
 options to choose from.)
\end_layout

\begin_layout Standard
To represent the intersection as substitutions we distribute it over the
 hyperplane stack unions.
 This results in a union of hyperline stacks of the form 
\begin_inset Formula $\set{\tuple n\in\mathbb{N}^{k}}{n_{j}<b_{j}\text{ when }j\in J}$
\end_inset

 where 
\begin_inset Formula $b$
\end_inset

 and 
\begin_inset Formula $J\subseteq\left\{ 1,...,k\right\} $
\end_inset

 vary.
 One such hyperline stack is represented by 
\begin_inset Formula $\prod_{j\in J}b_{j}$
\end_inset

 substitutions 
\begin_inset Formula $\set{n_{j}\mapsto a_{j}}{j\in J}$
\end_inset

 enumerating choices 
\begin_inset Formula $0\leq a_{j}<b_{j}$
\end_inset

.
 Unfortunately distribution duplicates some base cases.
 To compensate, if 
\begin_inset Formula $I\subseteq J$
\end_inset

 and 
\begin_inset Formula $\tuple b\geq\tuple c$
\end_inset

 pointwise, then 
\begin_inset Formula $\left\{ \tuple n<\tuple b\text{ on }I\right\} \supseteq\left\{ \tuple n<\tuple c\text{ on }J\right\} $
\end_inset

 so that the latter hyperline stack can be removed in favor of the former.
\end_layout

\begin_layout Standard
If a variable 
\begin_inset Formula $n\in\mathbb{Z}$
\end_inset

 is unbound, we do twice inductions on the rays, say 
\begin_inset Formula $0\leq n$
\end_inset

 and 
\begin_inset Formula $n<b$
\end_inset

 if 
\begin_inset Formula $b$
\end_inset

 base cases will be needed.
 The latter backwards induction can be transformed to the prior format by
 the change of variables 
\begin_inset Formula $n\mapsto b-1-n$
\end_inset

.
\end_layout

\begin_layout Section
Examples –SD+VN 
\begin_inset CommandInset label
LatexCommand label
name "sec:examples"

\end_inset


\end_layout

\begin_layout Standard

\color gray
Regarding choice of examples, in the scope of the method are:
\end_layout

\begin_layout Description

\color gray
WZ
\begin_inset space ~
\end_inset

examples such as Apéry's recurrence, binomial theorem, Vandermonde's convolution
: 
\begin_inset Formula 
\[
\sulut{\sulut{m+2}^{3}M^{2}-\sulut{17m^{2}+51m+39}\sulut{2m+3}M+\sulut{m+1}^{3}}\sum_{n=0}^{m}\binom{m}{n}^{2}\binom{m+n}{n}^{2}=0
\]

\end_inset


\begin_inset Formula 
\[
\sulut{x+y}^{m}=\sum_{n=0}^{m}\binom{m}{n}x^{n}y^{m-n},\quad\sum_{n=0}^{m}\binom{x}{n}\binom{y}{m-n}=\binom{x+y}{m},\quad\sum_{n=0}^{m}\binom{n}{m-n}=\makeop{fib}_{m+1}
\]

\end_inset


\end_layout

\begin_layout Description

\color gray
Non-holonomic discrete identities à la 
\begin_inset CommandInset citation
LatexCommand cite
key "close"
literal "false"

\end_inset

 such as Abel's binomial formula, Stirling number identities:
\begin_inset Formula 
\[
\sulut{x+y}^{m}=\sum_{n=0}^{m}\binom{m}{n}x\sulut{x-n}^{n-1}\sulut{y+n}^{m-n},\quad\sum_{k=n}^{m}\sulut{-1}^{k-n}\left[\begin{array}{c}
m\\
k
\end{array}\right]\left\{ \begin{array}{c}
k\\
n
\end{array}\right\} =\delta_{n}^{m}
\]

\end_inset


\end_layout

\begin_layout Description

\color gray
Elementary general summation formulas such as sum-by-parts, reverse, swap:
\begin_inset Formula 
\[
\sum_{n=0}^{m}f_{m-n}=\sum_{n=0}^{m}f_{n},\quad\sum_{m=0}^{k}\sum_{n=0}^{m}f_{m,n}=\sum_{n=0}^{k}\sum_{m=n}^{k}f_{m,n},\quad\sum_{n=1}^{m}\sulut{f_{2n-1}+f_{2n}}=\sum_{n=1}^{2m}f_{n}
\]

\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 we have no recurrence for 
\begin_inset Formula $f_{m,n}$
\end_inset

 and moreover we can propagate nothing useful for 
\begin_inset Formula $l_{m}$
\end_inset

 either.
 Nevertheless when it is the turn of 
\begin_inset Formula $\mathcal{L}_{k}$
\end_inset

, we get the immediate recurrence 
\begin_inset Formula $\sulut{K-1}\mathcal{L}_{k}-Kl_{k}=0$
\end_inset

 where 
\begin_inset Formula $K$
\end_inset

 is a shift w.r.t.
 
\begin_inset Formula $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}\sulut{S_{k,n}-s_{n}}=\sum_{n=0}^{k}\sulut{\sum_{m=0}^{k}f_{m,n}-\sum_{m=0}^{n-1}f_{m,n}}$
\end_inset

 where 
\begin_inset Formula $r_{k,n}$
\end_inset

, 
\begin_inset Formula $S_{k,n}$
\end_inset

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

 are auxiliary names.
 Propagation to summation 
\begin_inset Formula $S_{k,n}$
\end_inset

 gives 
\begin_inset Formula $\sulut{K-1}S_{k,n}-Kf_{k,n}=0$
\end_inset

.
 Obviously 
\begin_inset Formula $\sulut{K-1}s_{n}=0$
\end_inset

 and combining these with 
\begin_inset Formula $r_{k,n}=S_{k,n}-s_{n}$
\end_inset

 gives 
\begin_inset Formula $\sulut{K-1}r_{k,n}-Kf_{k,n}=0$
\end_inset

 as the recurrence of 
\begin_inset Formula $r_{k,n}$
\end_inset

.
\end_layout

\begin_layout Example
Propagation to summation 
\begin_inset Formula $\mathcal{R}_{k}$
\end_inset

 gives 
\begin_inset Formula $\sulut{K-1}\mathcal{R}_{k}-Kr_{k,k}-\sum_{n=0}^{k}Kf_{k,n}=0$
\end_inset

.
 Final propagation to difference gives the recurrence 
\begin_inset Formula $\sulut{K-1}\sulut{\mathcal{L}_{k}-\mathcal{R}_{k}}-Kl_{k}+Kr_{k,k}+\sum_{n=0}^{k}Kf_{k,n}=0$
\end_inset

.
 We can simplify the excess terms as follows
\begin_inset Formula 
\[
Kr_{k,k}=\sum_{m=0}^{k+1}f_{m,k+1}-\sum_{m=0}^{k}f_{m,k+1}=f_{k+1,k+1}
\]

\end_inset


\begin_inset Formula 
\[
-Kl_{k}+\sum_{n=0}^{k}Kf_{k,n}=-\sum_{n=0}^{k+1}f_{k+1,n}+\sum_{n=0}^{k}f_{k+1,n}=-f_{k+1,k+1}
\]

\end_inset

Consequently we end up with the recurrence 
\begin_inset Formula $\sulut{K-1}\sulut{\mathcal{L}_{k}-\mathcal{R}_{k}}=0$
\end_inset

 that allows a simple induction to prove the claim from its base case 
\begin_inset Formula $\mathcal{L}_{0}=\mathcal{R}_{0}$
\end_inset

.
\end_layout

\begin_layout Standard
\begin_inset Separator plain
\end_inset


\end_layout

\begin_layout Example
\begin_inset Formula 
\[
\sum_{n=0}^{m}\binom{n}{m-n}=F_{m+1}\text{ (Fibonacci numbers)}
\]

\end_inset


\begin_inset CommandInset label
LatexCommand label
name "Fibonacci1"

\end_inset

Fibonacci numbers are defined by 
\begin_inset Formula $F_{1}=F_{2}=1$
\end_inset

 and 
\begin_inset Formula $\sulut{N^{2}-N-1}F_{n}=0$
\end_inset

 where 
\begin_inset Formula $N$
\end_inset

 is a shift w.r.t.
 
\begin_inset Formula $n$
\end_inset

.
 For binomial coefficient we have recurrences 
\begin_inset Formula $\sulut{NM-M-1}\binom{n}{m}=0$
\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}=0$
\end_inset

.
 We want to propagate these over the substitution 
\begin_inset Formula $\sigma=\left\{ \sulut{n,m}\mapsto\sulut{n,m-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}} & =0\label{1F}\\
\sulut{\widetilde{M}-M}{\textstyle \binom{n}{m}} & =0\label{2F}
\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 (
\begin_inset CommandInset ref
LatexCommand ref
reference "2F"
plural "false"
caps "false"
noprefix "false"

\end_inset

) immediately rewrites every 
\begin_inset Formula $M$
\end_inset

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

 and then (
\begin_inset CommandInset ref
LatexCommand ref
reference "1F"
plural "false"
caps "false"
noprefix "false"

\end_inset

) becomes 
\begin_inset Formula $\sulut{-N+\widetilde{N}\widetilde{M}}\binom{n}{m}=0$
\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}} & =0 &  &  & f_{m,n}:={\textstyle \binom{n}{m-n}}\\
\sulut{-N+\widetilde{N}\widetilde{M}}{\textstyle \binom{n}{m}} & =0\\
\sulut{\widetilde{N}\widetilde{M}^{2}-\widetilde{M}-1}{\textstyle \binom{n}{m}} & =0 &  & \overset{\sigma}{\mapsto} & \sulut{NM^{2}-M-1}f_{m,n} & =0\\
\sulut{\sulut{m+1}\widetilde{N}\widetilde{M}^{2}-n-1}{\textstyle \binom{n}{m}} & =0 &  & \overset{\sigma}{\mapsto} & \sulut{\sulut{m-n+1}NM^{2}-n-1}f_{m,n} & =0
\end{align*}

\end_inset


\end_layout

\begin_layout Example
Next we must eliminate multiplication by 
\begin_inset Formula $n$
\end_inset

 in order to propagate recurrences to 
\begin_inset Formula $\sum_{n=0}^{m}f_{m,n}$
\end_inset

.
 So from 
\begin_inset Formula $\sulut{NM^{2}-M-1}f_{m,n}=0$
\end_inset

 we get
\begin_inset Formula 
\begin{gather*}
\sulut{M^{2}-M-1}\sum_{n=0}^{m}f_{m,n}+\left\{ n\mapsto m\right\} \frac{NM^{2}-M-N^{2}M^{2}+NM}{N-1}Nf_{m,n}-\left\{ n\mapsto0\right\} M^{2}f_{m,n}\\
=\sulut{M^{2}-M-1}\sum_{n=0}^{m}f_{m,n}-\underset{=1}{\underbrace{f_{m+2,m+2}}}+\underset{=1}{\underbrace{f_{m+1,m+1}}}-\underset{=0}{\underbrace{f_{m+2,0}}}
\end{gather*}

\end_inset

which is exactly the same recurrence that defines the (shifted) Fibonacci
 numbers 
\begin_inset Formula $F_{m+1}$
\end_inset

 and consequently also the difference 
\begin_inset Formula $\sum_{n=0}^{m}f_{m,n}-F_{m+1}$
\end_inset

.
\end_layout

\begin_layout Example
We do induction using the recurrence 
\begin_inset Formula $M^{2}-M-1$
\end_inset

.
 Its leading term is uniquely 
\begin_inset Formula $M^{2}$
\end_inset

 implying base cases 
\begin_inset Formula $\set i{0\leq i<2}=\left\{ 0,1\right\} $
\end_inset

 (assuming 
\begin_inset Formula $m\in\mathbb{N}$
\end_inset

).
 The coefficient of 
\begin_inset Formula $M^{2}$
\end_inset

 is 1 and especially always invertible so there's no side condition coming
 from that.
 
\noun on
Summation
\noun default
 inference hence produces a conclusion
\begin_inset Formula 
\[
\sum_{n=0}^{0}\binom{n}{0-n}\neq F_{1}\vee\sum_{n=0}^{1}\binom{n}{1-n}\neq F_{2}
\]

\end_inset

which is readily refuted by evaluating all four terms.
\end_layout

\begin_layout Section
Related Work
\end_layout

\begin_layout Standard
Holonomic sequences are ones definable by recurrences with polynomial coefficien
ts and finitely many base case values.
 They are closed w.r.t.
 
\begin_inset Formula $+,\cdot,\sum$
\end_inset

 and affine substitutions which especially makes their equality decidable
 
\begin_inset CommandInset citation
LatexCommand cite
key "basicholo"
literal "false"

\end_inset

.
 Dropping requirement of finitely many base cases gives homogeneous version
 of the presented propagation procedure whose theory Chyzak, Kauers and
 Salvy laid out 
\begin_inset CommandInset citation
LatexCommand cite
key "close"
literal "false"

\end_inset

.
 Heterogeneity is regularly discussed with Gröbner bases under the technical
 name of module bases 
\begin_inset CommandInset citation
LatexCommand cite
key "moduleGB-03,moduleGB-18,moduleGB-20"
literal "false"

\end_inset

.
 Its integration into propagations made elementary identities about general
 sequences provable which may interest general purpose theorem provers.
\end_layout

\begin_layout Standard
Hypergeometric sums are practically common holonomic sequences that have
 much faster algorithms available.
 Gosper's indefinite summation 
\begin_inset CommandInset citation
LatexCommand cite
key "Gosper"
literal "false"

\end_inset

 can be applied to compute Wilf-Zeilberger-pairs 
\begin_inset CommandInset citation
LatexCommand cite
key "WZcert"
literal "false"

\end_inset

 that come with compact proof certificates for definite sum identities.
 These fast methods admit generalizations to the full holonomic setting
 (see Koutschan's thesis 
\begin_inset CommandInset citation
LatexCommand cite
key "MathematicaHolo"
literal "false"

\end_inset

 for an overview).
\end_layout

\begin_layout Standard
Holonomic functions have a nearly dual theory where differential equations
 with polynomial coefficients play the rôle of recurrences.
 Above references present the discrete and continuous holonomic theories
 together, some times unified and generalized by the language of Ore-polynomials
 
\begin_inset CommandInset citation
LatexCommand cite
key "Ore"
literal "false"

\end_inset

.
 We presented only the discrete case because currently axiomatic provers
 tend to lack theoretical groundwork to bootstrap useable differential algebra.
 
\color gray
Should this paragraph be removed as too unrelated?
\end_layout

\begin_layout Standard
Software:
\end_layout

\begin_layout Itemize
HOL Light – Maxima bridge by Harrison 
\begin_inset CommandInset citation
LatexCommand cite
key "HOL:WZ"
literal "false"

\end_inset


\end_layout

\begin_layout Itemize
Coq – Mathematica by Mahboubi and Sibut-Pinote 
\begin_inset CommandInset citation
LatexCommand cite
key "Coq"
literal "false"

\end_inset


\end_layout

\begin_layout Itemize
CASes e.g.
 Mathematica 
\begin_inset CommandInset citation
LatexCommand cite
key "MathematicaHolo,inductPhD,MathematicaWZ"
literal "false"

\end_inset

, Maple 
\begin_inset CommandInset citation
LatexCommand cite
key "MapleWZ"
literal "false"

\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
