%% LyX 2.3.6.1 created this file.  For more info, see http://www.lyx.org/.
%% Do not edit unless you really know what you are doing.
\documentclass[english]{beamer}
\usepackage{mathptmx}
\usepackage[T1]{fontenc}
\usepackage[latin9]{inputenc}
\setcounter{secnumdepth}{3}
\usepackage{verbatim}
\usepackage{mathtools}
\usepackage{amsbsy}
\usepackage{amstext}
\usepackage{amsthm}
\usepackage{amssymb}
\usepackage{setspace}
\usepackage{xargs}[2008/03/08]
\PassOptionsToPackage{normalem}{ulem}
\usepackage{ulem}
\setstretch{0.7}

\makeatletter
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Textclass specific LaTeX commands.
% this default might be overridden by plain title style
\newcommand\makebeamertitle{\frame{\maketitle}}%
% (ERT) argument for the TOC
\AtBeginDocument{%
  \let\origtableofcontents=\tableofcontents
  \def\tableofcontents{\@ifnextchar[{\origtableofcontents}{\gobbletableofcontents}}
  \def\gobbletableofcontents#1{\origtableofcontents}
}
\theoremstyle{plain}
\newtheorem{thm}{\protect\theoremname}
\theoremstyle{definition}
\newtheorem{defn}[thm]{\protect\definitionname}

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

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

\usepackage{graphicx}
\usepackage{xcolor}
\usepackage{hyperref}
\usepackage[mathcal]{euscript}
%Dioihin
\usepackage{setspace}
\usepackage{sansmathfonts}
\let\hbar\undefined
\usepackage{arev}
\beamertemplatenavigationsymbolsempty
\setbeamertemplate{footline}[frame number]

\makeatother

\usepackage{babel}
\providecommand{\definitionname}{Definition}
\providecommand{\theoremname}{Theorem}

\begin{document}
\noindent\begin{minipage}[t]{1\columnwidth}%
\global\let \oldquad\quad
\global\let \oldqquad\qquad

\global\long\def\quad{\oldqquad}%
\global\long\def\qquad{\oldqquad}%
\global\long\def\skip{}%
\global\long\def\s{\ }%

\global\long\def\sulut#1{\left(#1\right)}%

\global\long\def\veny#1#2#3{\text{{\scalebox{#3}[#2]{\ensuremath{#1}}}}}%

\global\long\def\nouse#1#2{\raisebox{#2ex}{\ensuremath{#1}}}%

\global\long\def\makeop#1{\operatorname{#1}}%

\global\long\def\makelim#1#2{\operatorname*{#1}\limits _{#2}}%

\global\long\def\back#1{\hspace{-#1em}}%

\newcommandx\integ[2][usedefault, addprefix=\global, 1=\skip]{\int_{#2}^{#1}\negthickspace}%

\global\long\def\set#1#2{\left\{  #1\,\vphantom{\overset{o}{O}}\middle|\,#2\right\}  }%

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

\global\long\def\seq#1{\vec{#1}}%
\global\long\def\tuple#1{\vec{#1}}%

\global\long\def\holdsIn{\mathrel{\veny{\models}1{-1}}}%
%
\end{minipage}

\global\long\def\cst#1{\textsf{#1}}%
\global\long\def\namedsimp#1#2#3{\frac{#2}{#3}\text{\textsc{#1}}}%

\linespread{1.3}\selectfont{}\let\overrightarrow\vec

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

\global\long\def\DenseTable{\setlength\arraycolsep{0pt}}%

\global\long\def\underline#1{\text{\leavevmode\vtop{\hbox{\ensuremath{#1}}\kern0.4ex  \hrule height.4pt}}}%

\newcommandx\Sum[2][usedefault, addprefix=\global, 1=n\text{=}0, 2=m]{\mathchoice{{\textstyle \sum\limits _{#1}^{#2}}\skip}{\sum\limits _{#1}^{#2}}{{\textstyle \mathop{\overset{#2}{\underset{#1}{\Sigma}}}}\skip}{{\scriptstyle \mathop{\overset{#2}{\underset{#1}{\Sigma}}}}\skip}}%

\global\long\def\operatorEquality#1{\mop{\back{.05}\veny{#1}{.9}{.9}\back{.05}}}%

\global\long\def\bigred#1{\mathclap{\smash{\nouse{\veny{{\color{red}#1}}{1.5}2}{-.5}}}}%

\global\long\def\vaihda#1#2#3{{\alt<#2->{#3}{\mathrlap{#1}\phantom{#3}}}}%
%pitenee

\global\long\def\vaihdaa#1#2#3{{\alt<#2->{\mathrlap{#3}\phantom{#1}}{#1}}}%
%lyhenee

\global\long\def\vaihdax#1#2#3{{\alt<#2->{#3}{\phantom{#3}\mathllap{#1}}}}%
%vasen pitenee

\global\long\def\Vaihda#1#2#3{{\alt<#2->{#3}{\mathrlap{#1}\phantom{#3}}}}%
%suurenee

\global\long\def\erotuA#1#2{{\alt<#2>{\color{red}#1}{#1}}}%
\begin{comment}
\textcolor{red}{Punakorostus}
\end{comment}

\global\long\def\erotuB#1#2{{\alt<#2>{\color{blue}#1}{#1}}}%
\begin{comment}
\textcolor{blue}{Sinikorostus}
\end{comment}

\global\long\def\tableOper#1{\s#1\back{0.6}}%

\global\long\def\GeneralizeTransitions#1#2#3{\vaihdaa{#1}4{\vaihda{\:\phantom{#3}#2}5{\vaihda{#1}6{\phantom{#3}\vaihda{\#f}7{\s s}}}}}%

$\mathrlap{}$
\title{{\Large{}Recurrence-Driven Summations}\\
{\Large{}in Automated Deduction}}
\author{$\begin{array}{l}
\text{Visa Nummelin}\\
{\scriptstyle \text{Joint work with Jasmin Blanchette and Sander R. Dahmen}}
\end{array}$}
\date{2\textsuperscript{nd} June 2023}
\makebeamertitle

\frametitle{Questions of interest}
\begin{itemize}[<+->]
\item Prove equations between summation expressions
\item $\Sum f_{m-n}=\Sum f_{n}\quad\Sum\Sum[k=0][n]f_{n,k}=\Sum[k=0]\Sum[n=k]f_{n,k}$
\item $\Sum6n^{2}=m\sulut{m+1}\sulut{2m+1}\quad\Sum n^{3}=\sulut{\Sum n}^{2}$
\item $\sulut{x+y}^{m}=\Sum\binom{m}{n}x^{n}y^{m-n}\quad\binom{x+y}{m}=\Sum\binom{x}{n}\binom{y}{m-n}$
\item $\sulut{x+y}^{m}=\Sum\binom{m}{n}x\sulut{x-n}^{n-1}\sulut{y+n}^{m-n}$
\item<2-> $\Vaihda{\text{Arbitrary sequences (reverse, triangle swap)}}3{\Vaihda{\text{Elementary arithmetic (power sums)}}4{\Vaihda{\text{Holonomic formulas (binomial, Wandermonde's)}}5{\Vaihda{\text{Beyond holonomic (Abel's binomial formula)}}6{\text{Integrate to an existing base prover (in theory)}}}}}$
\end{itemize}

\frametitle{Source of recurrences}

Summation ${\scriptstyle \Sum}a_{n}=:g_{m}$ can be defined by
\begin{itemize}
\item the base case $g_{0}=a_{0}$; and
\item the recurrence equation $g_{m+1}=g_{m}+a_{m+1}$
\end{itemize}
Recurrences are useful to define other sequences too
\begin{itemize}[<+(1)->]
\item exponential: $b^{n+1}=b\cdot b^{n}$ \alt<2>{with base case $b^{0}=1$}~
\item Fibonacci: $F_{n+2}=F_{n+1}+F_{n}$ \alt<3>{with base cases $F_{0}=0$, $F_{1}=1$}~
\item factorial: $\sulut{n+1}!=\sulut{n+1}\cdot n!$ \alt<4>{with base case $0!=1$}~
\item binomial coefficient: for $\binom{m}{n}=\frac{m!}{n!\sulut{m-n}!}$ holds\\
 $\binom{m+1}{n}=\frac{m+1}{m-n+1}\binom{m}{n}\quad\text{and}\quad\binom{m}{n+1}=\frac{m-n}{n+1}\binom{m}{n}$
\item polynomial $P$: if $d=\makeop{deg}P$ then for all $n$\\
 $P\sulut{n+d}+...+\sulut{-1}^{d-j}\binom{d}{j}P\sulut{n+j}+...+\sulut{-1}^{d}P\sulut n=0$
\end{itemize}

\frametitle{Application of recurrences}
\begin{itemize}
\item Recurrences are linear, with polynomial coefficients, and finite in length
\item<2-> To prove equation $f_{n}=0$ for $n\in\mathbb{N}$, it suffices to find\\
- recurrence $c_{n,}{}_{d}f_{n+d}=c_{n,}{}_{d-1}f_{n+d-1}+...+c_{n,}{}_{0}f_{n}$; and\\
- prove base cases $f_{0}=...=f_{d-1}=0$ and $\exists c_{n,d}^{-1}$
\item<3-> 
\global\long\def\plusplus{+\negthickspace...\negthickspace+}%
$\Vaihda{f_{\vaihda d4{d+1}}=c_{\vaihda 041,d}^{-1}\sulut{c_{\vaihda 041,d-1}f_{\vaihdaa{d-1}4d}\plusplus c_{\vaihda 041,0}f_{\vaihdaa 041}}=c_{\vaihda 041,d}^{-1}\sulut{0\plusplus0}=0}5{+,\cdot,\sum\text{ and substitutions build expressions}}$
\item<6-> Example decomposition: $\vaihda{\erotuA{\binom{x+y}{m}}8}9{A_{x,y,m}}\s\vaihda =7{\vaihda{\erotuB -8}9+}\s\vaihdaa{\erotuB{\Sum\binom{x}{n}\binom{y}{m-n}}8}9{B_{x,y,m}}\vaihda{}7{{}=0}$\\
$\vaihda{}9{A_{x,y,m}=\vaihda{\binom{\erotuA{x+y}{10}}{m}}{11}{\left\{ u\mapsto x+y\right\} C_{u,m}\quad C_{u,m}=\binom{u}{m}}}$\\
$\vaihda{}9{B_{x,y,m}=\vaihdaa{\erotuA -{12}\erotuB{{\scriptstyle \Sum}\binom{x}{n}\binom{y}{m-n}}{12}}{13}{\sulut{-1}\cdot D_{x,y,m}}}$\\
$\vaihda{}{13}{D_{x,y,m}={\scriptstyle \Sum}\vaihda{\erotuA{\binom{x}{n}\binom{y}{m-n}}{14}}{15}{E_{x,y,m,n}}}$\\
$\vaihda{}{15}{E_{x,y,m,n}=\vaihda{\erotuA{\binom{x}{n}}{16}}{17}{C_{x,n}}\cdot\vaihdaa{\erotuB{\binom{y}{m-n}}{16}}{17}{F_{y,m,n}}}$\\
$\vaihda{}{17}{F_{y,m,n}=\vaihda{\binom{y}{\erotuA{m-n}{18}}}{19}{\left\{ u\mapsto m-n\right\} C_{y,u}}}$
\end{itemize}

\frametitle{Informal example}
\begin{itemize}
\item Principle of propagation:\\
From recurrences of sequences $f_{n}$, $g_{n}$, $h_{n,m,k}$\\
derive recurrences to $f_{n}+g_{n}$, $f_{n}g_{n}$, ${\scriptstyle \Sum}h_{n,m,k}$, $f_{\text{matrix}\cdot n}$
\item Let $g_{0}=a_{0}$, $g_{1}=a_{0}+a_{1}$, $g_{m+2}=g_{m}+a_{m+1}+a_{m+2}$
\item Claim $g_{m}=\Sum a_{n}$ for $m\geq0$
\item<2-> Recurrence of $A_{m}:=\Sum a_{n}$ is $A_{m+1}=A_{m}+a_{m+1}$
\item<3-> Recurrence of $B_{m}:=g_{m}-A_{m}$ is found by deriving consequences w.r.t. term ordering s.t. $B\prec g,A$
\end{itemize}

\frametitle{Informal example (recurrence of $B_{m}:=g_{m}-A_{m}$)}

$\begin{aligned}\text{Known: }A_{m+1} & =A_{m}+a_{m+1} & \hspace{5em}\sulut{\alpha_{m}}\\
g_{m} & =A_{m}+B_{m} & \sulut{\beta_{m}}
\end{aligned}
$

$\back 2\Vaihda{\begin{array}{lll}
 & g_{m+2}=g_{m}+a_{m+2}+a_{m+1} & \sulut{\gamma_{m}}\\
\phantom{-\quad} & \vaihda{}2{g_{m+2}=A_{m+2}+B_{m+2}} & \vaihda{}2{\sulut{\beta_{m+2}}}\\
 & \phantom{A_{m+2}=g_{m}+a_{m+2}+a_{m+1}-B_{m+2}}\\
\\
\\
\\
\\
\\
\\
\end{array}}3{\Vaihda{\begin{array}{lll}
 & g_{m+2}=\erotuA{g_{m}+a_{m+2}+a_{m+1}}3 & \sulut{\gamma_{m}}\\
-\quad & g_{m+2}=\erotuB{A_{m+2}+B_{m+2}}3 & \sulut{\beta_{m+2}}\\
\hline  & \erotuB{A_{m+2}}3=\erotuA{g_{m}+a_{m+2}+a_{m+1}}3-\erotuB{B_{m+2}}3\\
 & \vaihda{}4{A_{m+2}=A_{m+1}+a_{m+2}} & \vaihda{}4{\sulut{\alpha_{m+1}}}\\
\\
\\
\\
\\
\\
\end{array}}5{\Vaihda{\begin{array}{lll}
 & g_{m+2}=g_{m}+a_{m+2}+a_{m+1} & \sulut{\gamma_{m}}\\
-\quad & g_{m+2}=A_{m+2}+B_{m+2} & \sulut{\beta_{m+2}}\\
\hline  & A_{m+2}=\erotuA{g_{m}}5+a_{m+2}+\erotuA{a_{m+1}-B_{m+2}}5\\
- & A_{m+2}=\erotuB{A_{m+1}}5+a_{m+2} & \sulut{\alpha_{m+1}}\\
\hline  & \erotuB{A_{m+1}}5=\erotuA{g_{m}+a_{m+1}-B_{m+2}}5\\
 & \vaihda{}6{A_{m+1}=A_{m}+a_{m+1}} & \vaihda{}6{\sulut{\alpha_{m}}}\\
\\
\\
\\
\end{array}}7{\Vaihda{\begin{array}{lll}
 & g_{m+2}=g_{m}+a_{m+2}+a_{m+1} & \sulut{\gamma_{m}}\\
-\quad & g_{m+2}=A_{m+2}+B_{m+2} & \sulut{\beta_{m+2}}\\
\hline  & A_{m+2}=g_{m}+a_{m+2}+a_{m+1}-B_{m+2}\\
- & A_{m+2}=A_{m+1}+a_{m+2} & \sulut{\alpha_{m+1}}\\
\hline  & A_{m+1}=\erotuA{g_{m}}7+a_{m+1}\erotuA{{}-B_{m+2}}7\\
- & A_{m+1}=\erotuB{A_{m}}7+a_{m+1} & \sulut{\alpha_{m}}\\
\hline  & \erotuA{g_{m}}7=\erotuB{A_{m}}7+\erotuA{B_{m+2}}7\\
 & \vaihda{}8{g_{m}=A_{m}+B_{m}} & \vaihda{}8{\sulut{\beta_{m}}}\\
\\
\end{array}}9{\begin{array}{lll}
 & g_{m+2}=g_{m}+a_{m+2}+a_{m+1} & \sulut{\gamma_{m}}\\
-\quad & g_{m+2}=A_{m+2}+B_{m+2} & \sulut{\beta_{m+2}}\\
\hline  & A_{m+2}=g_{m}+a_{m+2}+a_{m+1}-B_{m+2}\\
- & A_{m+2}=A_{m+1}+a_{m+2} & \sulut{\alpha_{m+1}}\\
\hline  & A_{m+1}=g_{m}+a_{m+1}-B_{m+2}\\
- & A_{m+1}=A_{m}+a_{m+1} & \sulut{\alpha_{m}}\\
\hline  & g_{m}=A_{m}+B_{m+2}\\
- & g_{m}=A_{m}+B_{m} & \sulut{\beta_{m}}\\
\hline  & B_{m+2}=B_{m}
\end{array}}}}}$

\frametitle{Informal example (induction)}
\begin{itemize}
\item $B_{m+2}=B_{m}$ means if $g_{m}=\Sum a_{n}$ then $g_{m+2}=\Sum[][m+2]a_{n}$
\begin{itemize}
\item Verifies the induction step
\end{itemize}
\item Induction base cases $g_{0}=\Sum[][0]a_{n}$ and $g_{1}=\Sum[][1]a_{n}$
\begin{itemize}
\item Summations can be expanded, e.g., $\Sum[][1]a_{n}=a_{0}+a_{1}$
\item Leave for the base theorem prover
\end{itemize}
\end{itemize}

\frametitle{Operator polynomial notation}
\begin{defn}
Operator polynomials are noncommutative $\mathbb{Z}$-algebra\\
(so closed under addition and composition as product)\\
spanned by two types of indeterminates:
\begin{itemize}
\item Shifts $N,M,...$ operating $\sulut{Mf}_{n,m,...}=f_{n,m+1,...}$
\item Multipliers $n,m,...$ operating $\sulut{mf}_{n,m,...}=m\cdot f_{n,m,...}$
\end{itemize}
\end{defn}
\begin{itemize}
\item<2-> \smash{\parbox[t]{\linewidth}{~\\
\textcolor{white}{\textemdash \textemdash }Noncommutation: $Nn=\sulut{n+1}N$\alt<2>{ because
\[
\sulut{Nnf}_{n}=\sulut{nf}_{n+1}=\sulut{n+1}\cdot f_{n+1}=\sulut{n+1}\cdot\sulut{Nf}_{n}=\sulut{\sulut{n+1}Nf}_{n}
\]
}{}}}
\item<3-> \smash{\parbox[t]{\linewidth}{~\\
\textcolor{white}{\textemdash \textemdash }Example: $\vaihda{}5(\vaihdaa{mM-nM+{}}4{\sulut{m-n+1}}M-m-1\vaihda{}5{)\binom{m}{n}=\vaihda{}60}$\alt<5>{\\
\textcolor{white}{\textemdash \textemdash Example}$=\sulut{m-n+1}\binom{m+1}{n}-\sulut{m+1}\binom{m}{n}=0$}{}}}
\item<6-> Example: $\vaihda{g_{n+2}}7{N^{2}\vaihdaa{g_{n}}8g}\s\vaihda =8-\s\vaihdaa{g_{n}}8g\s\vaihda +8-\s\vaihda{a_{n+2}}7{N^{2}\vaihdaa{a_{n}}8a}\s\vaihda +8-\s\vaihda{a_{n+1}}7{N\vaihdaa{a_{n}}8{a=0}}$
\end{itemize}

\frametitle{Elimination of sequences and operators}
\begin{itemize}
\item Recurrences have form $P_{1}f^{1}+...+P_{k}f^{k}=0$ where\\
$P_{j}$'s are operator polynomials and $f^{j}$'s sequences
\item<2-> Terms have form $yn_{1}^{x_{1}}...n_{d}^{x_{d}}N_{1}^{z_{1}}...N_{d}^{z_{d}}f=:y\overrightarrow{n}^{x}\overrightarrow{N}^{z}f$\\
where $n_{j}$'s are variables, $f$ is sequence, $\pm$$y,x_{j},z_{j}\in\mathbb{N}$
\item<3-> \smash{\parbox[t]{\linewidth}{~\\
\textcolor{white}{\textemdash \textemdash }Linearly order terms by weighting $x_{j}$'{\small{}s}, $z_{j}$'{\small{}s} {\small{}and}~$f$\visible<4-8>{\\
\textcolor{white}{\textemdash{}} $\begin{array}{llllll}
\text{Example:} & \vaihdaa{A_{m+2}}5{M^{2}A}\tableOper = & \vaihdaa{g_{m}}5g\tableOper + & \vaihdaa{a_{m+2}}5{M^{2}a}\tableOper + & \vaihdaa{a_{m+1}}5{Ma}\tableOper - & \vaihdaa{B_{m+2}}5{M^{2}B}\\
\vaihda{\mathrlap{\text{Lexicographically: }1^{st}\text{ total degree on }g,A}}6{1^{st}} & \vaihda{}62 & \vaihda{}60 & \vaihda{}6{-\infty} & \vaihda{}6{-\infty} & \vaihda{}6{-\infty}\\
\vaihda{\mathrlap{\hphantom{\text{Lexicographically: }}2^{nd}\text{ total degree on }a,B}}7{2^{nd}} & \vaihda{}7{-\infty} & \vaihda{}7{-\infty} & \vaihda{}72 & \vaihda{}71 & \vaihda{}72\\
\vaihda{\mathrlap{\hphantom{\text{Lexicographically: }}3^{rd}\text{ }\sulut{g,A,a,B}\mapsto\sulut{3,2,1,0}}}8{3^{rd}} & \vaihda{}82 & \vaihda{}83 & \vaihda{}81 & \vaihda{}81 & \vaihda{}80
\end{array}$}{}}}
\item<9-> To eliminate $n_{j}$, $N_{j}$ or $f$, make its weight dominant
\item<10-> To superpose two recurrences, left-multiply them by (the least number of) indeterminates s.t. maximal terms become equal, and subtract
\item<11-> Eliminating $h$: $\Vaihda{\begin{array}{r}
\vaihda{}{13}{{\color{red}M}(}\vaihdax{\sulut{\sulut{h+1}H-m+h}}{12}{{\color{blue}hH\binom{m}{h}}+H\binom{m}{h}-m\binom{m}{h}+h}\binom{m}{h}\vaihda{}{13})=0\\
\vaihdax{\vaihda{}{13}{{\color{blue}H}}\sulut{\sulut{m-\erotuA h{12-}+1}\erotuA M{12-}-m-1}}{14}{\sulut{\sulut{m-{\color{red}h}}{\color{red}M}-m-1}{\color{blue}H}}\erotuA{\binom{m}{h}}{12-}\hphantom{)}=0\\
\hphantom{\sulut{hM+\sulut{m+1}\sulut{HM-M-H}}\binom{m}{h})=0}
\end{array}}{15}{\Vaihda{\begin{array}{r}
M(hH\binom{m}{h}+H\binom{m}{h}-m\binom{m}{h}+h\binom{m}{h})=0\\
+\hfill\sulut{\sulut{m-h}M-m-1}H\binom{m}{h}\hphantom{)}=0\\
\hline \sulut{hM+\sulut{m+1}\sulut{HM-M-H}}\binom{m}{h}\hphantom{)}=0
\end{array}}{16}{\Vaihda{\begin{array}{r}
\sulut{\erotuB{hM}{17}+\sulut{m+1}\sulut{HM-M-H}}\erotuB{\binom{m}{h}}{17}=0\\
\vaihda{}{17}{\sulut{\sulut{m-{\color{red}h}+1}{\color{red}M}-m-1}{\color{red}\binom{m}{h}}=0}\\
\\
\end{array}}{18}{\begin{array}{r}
\sulut{hM+\sulut{m+1}\sulut{HM-M-H}}\binom{m}{h}=0\\
+\hfill\sulut{\sulut{m-h+1}M-m-1}\binom{m}{h}=0\\
\hline \sulut{m+1}\sulut{HM-H-1}\binom{m}{h}=0
\end{array}}}}$
\end{itemize}

\frametitle{Propagation 1/4: addition}
\begin{itemize}
\item Let sequence $f^{j}$ have set of recurrences $F_{j}$ ($j=1,2$)
\item To find recurrences of $f^{+}:=\vaihda{}2{P_{1}}f^{1}+\vaihda{}2{P_{2}}f^{2}$\\
eliminate $f^{1},f^{2}$ from $F_{1}\cup F_{2}\cup\left\{ \vaihda{}2{P_{1}}f^{1}+\vaihda{}2{P_{2}}f^{2}-f^{+}=0\right\} $
\item<3-> In the earlier example $B_{m}:=g_{m}-A_{m}$
\begin{align*}
 & f^{1}=g &  & F_{1}=\left\{ 0=M^{2}g-g-M^{2}a-Ma\right\}  &  & P_{1}=1\\
 & f^{2}=A &  & F_{2}=\left\{ 0=MA-A-Ma\right\}  &  & P_{2}=-1\\
 & f^{+}=B
\end{align*}
\end{itemize}

\frametitle{Propagation 2/4: summation}
\begin{itemize}
\item Let sequence $f$ have set of recurrences $F$
\item To find recurrences of ${\scriptstyle \Sum}f_{n,m,...}$\\
first eliminate multiplier $n$ from $F$, then \textquotedblleft commute\textquotedblright :\\
${\scriptstyle \Sum}P\sulut{N,M,m}f=P\sulut{1,M,m}{\scriptstyle \Sum}f+\text{boundary terms}$
\item<2-> ${\scriptstyle \Sum}X=X{\scriptstyle \Sum}$ for indeterminate $X\not\in\left\{ n,N,M\right\} $
\item<2-> ${\scriptstyle \Sum}M\vaihdaa{g_{n,m}}3g=M{\scriptstyle \Sum}\vaihdaa{g_{n,m}}3g-\vaihda{g_{m+1,m+1}}3{M\left\{ n\mapsto m\right\} g}$
\item<2-> ${\scriptstyle \Sum}N\vaihdaa{g_{n,m}}3g={\scriptstyle \Sum}\vaihdaa{g_{n,m}}3g+\vaihda{g_{m+1,m}}3{\left\{ n\mapsto m\right\} Ng}-\vaihda{g_{0,m}}3{\left\{ n\mapsto0\right\} g}$
\end{itemize}

\frametitle{Propagation 2/4: summation example}
\begin{itemize}[<+->]
\item Claim: $\Sum\binom{m}{n}=2^{m}$
\item Recurrences $0=\sulut{\sulut{m-n+1}M-m-1}\binom{m}{n}$ and $0=\sulut{\sulut{n+1}N-m+n}\binom{m}{n}$
\item First, $n$ eliminated: $0=\sulut{\sulut{m+1}\sulut{NM-N-1}}\binom{m}{n}$
\item Then $0=\smash{\Sum}\sulut{\sulut{m+1}\sulut{NM-N-1}}\binom{m}{n}=$
\[
\back 4\begin{array}{l}
=\sulut{m{+}1}\Sum[][\smash{m}]\sulut{N\sulut{M-1}\binom{m}{n}-\binom{m}{n}}\vaihda{}5{{}=}\\
\vaihda{}5{=\sulut{m{+}1}\Bigg(\Sum\sulut{M{-}2}\binom{m}{n}+\vaihdaa{\vaihdaa{\left\{ n{\mapsto}m\right\} N\sulut{M{-}1}\binom{m}{n}}6{\binom{m+1}{m+1}-\binom{m}{m+1}}-\vaihdaa{\left\{ n{\mapsto}0\right\} \sulut{M{-}1}\binom{m}{n}\Bigg)}6{\binom{m+1}{0}+\binom{m}{0}\Bigg)}}7{1\Bigg)\vaihda{}8{{}=}}}\\
\vaihda{}8{=\sulut{m{+}1}\vaihdaa{\Bigg(\sulut{M-2}\Sum[\smash{n=0}]\binom{m}{n}+1-\vaihdaa{M\left\{ n{\mapsto}m\right\} \binom{m}{n}\Bigg)}9{\binom{m+1}{m+1}\Bigg)}}{10}{\sulut{M-2}\Sum\binom{m}{n}}}
\end{array}
\]
\item<11-> $\sulut{m+1}\sulut{M-2}\sulut{\smash{\Sum}\binom{m}{n}-2^{m}}=0$ since $\sulut{M-2}2^{m}=0$
\end{itemize}

\frametitle{Propagation 3/4: linear substitution}
\begin{itemize}
\item Let $g_{\vaihda n{15}{\overrightarrow{n}}}=\left\{ \vaihda m{15}{\overrightarrow{m}}\mapsto\vaihda 2{15}A\vaihda n{15}{\overrightarrow{n}}\right\} f_{\vaihda m{15}{\overrightarrow{m}}}=f_{\vaihda 2{15}A\vaihda n{15}{\overrightarrow{n}}}$ and $F=f_{\vaihda m{15}{\overrightarrow{m}}}$'s recurrences
\item $\left\{ \vaihda m{16}{\overrightarrow{m}}\mapsto\vaihda 2{16}A\vaihda n{16}{\overrightarrow{n}}\right\} P(\vaihda m2{\vaihda m{16}{\overrightarrow{m}},\vaihda M4{\vaihda{M^{2}}{16}{\overrightarrow{M}^{A\delta_{j}}}}}\vaihda ){16}{)_{j=1}^{\#n}}f_{\vaihda m{16}{\overrightarrow{m}}}=P(\vaihda{2n}2{\vaihda 2{16}A\vaihda n{16}{\overrightarrow{n}},\vaihda ?4{\vaihda N{16}{N_{j}}}}\vaihda ){16}{)_{j=1}^{\#n}}g_{\vaihda n{16}{\overrightarrow{n}}}$
\item<3-> \alt<5->{Overload $\vaihda N{17}{\overrightarrow{N}^{x}}:=\vaihda{M^{2}}{17}{\overrightarrow{M}^{Ax}}$. Eliminate $\vaihda M{17}{\overrightarrow{M}}$ from $F\cup\{\vaihda{M^{2}}{17}{\overrightarrow{M}^{A\delta_{j}}}=\vaihda N{17}{N_{j}}\vaihda{\}}{17}{\mathrlap{\}_{j=1}^{\#n}}}$}{$N\left\{ m\mapsto2n\right\} =\left\{ m\mapsto2n\right\} M^{2}$ because $f_{2\sulut{n+1}}=f_{2n+2}$}
\item<6-> $\smash{\begin{array}{l}
\phantom{\prod\limits _{k=1}^{\#m}}\\
\vaihda N{18}{\overrightarrow{N}^{x}}\vaihda m{18}{m_{k}}=\sulut{m+\vaihda 2{18}{Ax}}\vaihda{}{18}{_{k}}\vaihda N{18}{\overrightarrow{N}^{x}}\quad\vaihda N{18}{N_{j}}\vaihda M{18}{M_{k}}=\vaihda M{18}{M_{k}}\vaihda N{18}{N_{j}}\\
\vaihda{}{18}{N_{j}\vaihda{\s=\overrightarrow{M}^{A\delta_{j}}}{19}{\prod\limits _{k:\s A_{kj}<0}M_{k}^{\left|A_{kj}\right|}}=\prod\limits _{\vaihda{\s\s\s k=1}{19}{k:\s A_{kj}>0}}^{\vaihdaa{\#m}{19}{}}M_{k}^{A_{kj}}}
\end{array}}$
\item<7-14> Example: for $\sulut{2n}!=$$\left\{ m\mapsto2n\right\} m!$ omitting \textquotedblleft =0\textquotedblright{} 
\begin{gather*}
\sulut{\erotuA M{8,10,12}-m-1}\erotuA{m!}{8,10,12},\quad\erotuA{M^{2}}8-N\vaihda{}9{,\quad\Vaihda{\sulut{\sulut{\erotuA m{10}+2}\erotuA M{10}+N}\erotuA{m!}{10}}{11}{\Vaihda{\sulut{\erotuA{2M}{12}+N+m\sulut{m+1}}\erotuA{m!}{12}}{13}{\sulut{N+\sulut{m+2}\sulut{m+1}}m!}}}\\
\back 4\Vaihda{\vaihda{}8{M\sulut{M-m-1}m!-\sulut{M^{2}-N}m!=\sulut{\sulut{m+2}M+N}m!}}9{\Vaihda{\vaihda{}{10}{\sulut{\sulut{m+2}M+N}m!-m\sulut{M-m-1}m!=\sulut{2M+N+m\sulut{m+1}}m!}}{11}{\vaihda{}{12}{\vaihdaa{\sulut{2M+N+m\sulut{m+1}}m!-2\sulut{M-m-1}m!=\sulut{N+\sulut{m+2}\sulut{m+1}}m!}{13}{}}}}
\end{gather*}
\item<14> Hence $\sulut{N+\sulut{2n+2}\sulut{2n+1}}\s\sulut{2n}!=0$
\end{itemize}

\frametitle{Propagation 4/4: product}
\begin{itemize}
\item Let sequences $f,g$ have sets of recurrences $F,G$
\item $f_{n}g_{n}=\left\{ m\mapsto n\right\} f_{n}g_{m}$
\item<2-> For disjoint indices, using linearity,\\
$\DenseTable\begin{array}{rlcrl}
P\sulut{n,N}f_{n}={} & \vaihda 03{e_{n}} & \implies & P\sulut{n,N} & \sulut{f_{n}g_{m}}=\vaihda 03{e_{n}g_{m}}\\
\widetilde{P}\sulut{m,M}g_{m}={} & \vaihda 03{\widetilde{e}_{m}} & \implies & \widetilde{P}\sulut{m,M} & \sulut{f_{n}g_{m}}=\vaihda 03{f_{n}\widetilde{e}_{m}}
\end{array}$
\item<4-> So recurrences of $f_{n}g_{m}$ are $F\cdot g_{m}\cup f_{n}\cdot\left\{ n\mapsto m\right\} G$
\item<4-> Then propagate to substitution (block matrix $\bigg[{\scriptstyle \begin{subarray}{c}
\mathcal{I}\\
\mathcal{I}
\end{subarray}}\bigg]$) %TODO Wandermonde example?
\end{itemize}

\frametitle{Homogenization by iteration}
\begin{itemize}
\item To prove $f=0$ we search homogeneous $Pf=0$
\item Propagation can give heterogeneous $Pf=f'$
\item<2-> New goal: $f'=0$
\item<2-> Suffices to iterate propagation on $f'$ because\\
if $P_{2}f'=\vaihda 03{f''}$ then $P_{2}Pf=\vaihda 03{f''\text{ etc. on }f''}$
\item<3-> Termination is provable by term order on sequences
\end{itemize}

\frametitle{Normalization of sequences}
\begin{itemize}
\item To simplify sequences between propagation steps
\item Normal writing order of operations:\\
\textcolor{gray}{out/root $\gets$} +, $\sum$, $\cdot$, substitutions \textcolor{gray}{$\to$ in/leaves}
\item<2-> $\Vaihda{\left\{ m{\mapsto}2k\right\} m!\Sum\sulut{n^{m}+\binom{m+k}{n+k}}=\Sum[][2k]\sulut{2k}!n^{2k}+\Sum[][2k]\sulut{2k}!\binom{3k}{n+k}}3{\text{Distribute \ensuremath{\sum},\ensuremath{\cdot},substitutions over +}}$
\item<3-> Sort associativity, commutativity, inverse
\item<3-> Rewrite ($f,g$ sequences; $\sigma,\sigma'$ substitutions; $c\in\mathbb{N}$)
\begin{align*}
1f,f1,\left\{ \right\} f & \to f & \left\{ \overrightarrow{n}\mapsto\overrightarrow{x}\right\} n_{j} & \to x_{j}\\
g\cdot{\scriptstyle \Sum[][x]}f & \to{\scriptstyle \Sum[][x]}gf & \sigma\sulut{fg} & \to\sigma f\cdot\sigma g\\
\sigma{\scriptstyle \Sum[][x]}f & \to{\scriptstyle \Sum[][\sigma x]}\sigma f & \sigma'\sigma f & \to\sulut{\sigma'\circ\sigma}f\\
{\textstyle {\scriptstyle \Sum[][c]}f} & \to\left\{ n\mapsto0\right\} f+...+\left\{ n\mapsto c\right\} f\kern-200mm 
\end{align*}
\end{itemize}

\frametitle{Integration to superposition calculus}
\begin{itemize}
\item Input task must use our built-in $\sum$\alt<2->{, hence}{}
\begin{itemize}
\item<2-> its domain (integers)\alt<3->{; and}{}
\item<3-> its range (commutative \alt<4->{\sout{monoid} group)}{monoid)}
\end{itemize}
\item<5-> Ring as range is optional $\Rightarrow$ search $\cdot$ on demand
\item<6-> During proving detect clauses $g\left[s\right]{\neq}0$ containing $\sum$
\item<6-> To them apply inference rule 
\[
\frac{g\left[s\right]\neq\vaihda 07{0\vee C}\quad\text{initial recurrences}}{\smash{\bigvee\limits _{b\in B}}g\left[b\right]\neq\vaihda 07{0\vee C\vee L}}\quad\text{where}
\]

\begin{itemize}
\item<6-> choose subterms $s$ to be generalized
\item<6-> get base cases $B$ from final recurrences
\item<7-> $L=$ leading coefficients have inverses
\end{itemize}
\end{itemize}

\frametitle{Subterm generalization}
\begin{itemize}
\item To refute $g\left[s\right]\neq0$, prove generally $\forall n{\in}\mathbb{Z}^{\#s}\negthickspace:g\left[n\right]{=}0$
\item We must choose subterms $s$
\item<2-> Example: \#=length and average axiom $\mu f=\Sum[n=1][\#f]{\displaystyle \frac{f_{n}}{\#f}}$
\item<2-> Claim $\mu\sulut{f-\mu f}^{2}=\mu\:f^{2}-\sulut{\mu f}^{2}$ \alt<3->{negated expands}{}
\[
\vaihda{}3{\Sum[n=1][\GeneralizeTransitions{\#\sulut{f-...}^{2}}{s_{1}}{\#(f}]\frac{\sulut{f_{n}-{\scriptstyle \Sum[n=1][\GeneralizeTransitions{\#f}{s_{3}}{}]}f_{n}/\GeneralizeTransitions{\#f}{s_{3}}{}}\overset{{\scriptstyle 2}}{\phantom{I}}}{\GeneralizeTransitions{\#\sulut{f-{\scriptstyle \Sum[n=1][\#f]}f_{n}/\#f}\overset{{\scriptstyle 2}}{\phantom{I}}}{s_{1}}{mmm}}-\Sum[n=1][\GeneralizeTransitions{\#\,f^{2}}{s_{2}}{\s}]\frac{f_{n}^{2}}{\GeneralizeTransitions{\#\,f^{2}}{s_{2}}{\s}}+\sulut{\Sum[n=1][\GeneralizeTransitions{\#f}{s_{3}}{}]\frac{f_{n}}{\GeneralizeTransitions{\#f}{s_{3}}{}}}^{2}\neq0}
\]
\item<4-> $\smash{\vaihdaa{s_{1}=\#\sulut{f-{\scriptstyle \Sum[n=1][\#f]}f_{n}/\#f}^{2},\s s_{2}=\#\,f^{2},\s s_{3}=\#f\implies\text{False!}}5{\vaihda{\text{Base prover must apply }\#\circ\makeop{lift}\sulut{...}=\#}7{s=\#f\implies\text{Correct generalization}}}}$
\item<8-> E.g., generalize nonnumeral $\mathbb{Z}$-constants bottom-up
\item<9->  $\mathrlap{\text{Afterwards identify sequences, last their recurrences}}$
\end{itemize}

\frametitle{Induction}
\begin{itemize}
\item Let $Pf=0$ be found to prove $f=0$
\item Apply induction on $\mathbb{N}^{k}$ (upto $2^{k}$ times on $\mathbb{Z}^{k}$)
\item If $P\sulut{\vaihda n3{\overrightarrow{n}},\vaihda N3{\overrightarrow{N}}}=\vaihda{N^{d}}3{\vaihdaa{N_{1}^{d_{1}}\vaihda{N_{2}^{d_{2}}}5{...N_{k}^{d_{k}}}}6{c\sulut{\overrightarrow{n}}\overrightarrow{N}^{d}}}$ + lower $\erotuA{\text{order}}4$ terms, then\\
base cases are $\vaihda{f_{d-1}=...=f_{0}=0}2{B=\vaihda{\left[0,d_{\phantom{1}}\right[}3{\vaihda{\left[0,d_{1}\right[\negthickspace\negthickspace\times\negthickspace\negthickspace\left\{ x_{2}\right\} \cup\left\{ x_{1}\right\} \negthickspace\negmedspace\times\negthickspace\!\left[0,d_{2}\right[}5{\bigcup_{j=1}^{k}\set{\left\{ x_{j}\mapsto a\right\} \overrightarrow{x}}{a\in\left[0,d_{j}\right[}}}}$ \\
\alt<3->{where $x_{j}$'s are free variables of the base prover}{~}
\item<4-> Induction w.r.t. any monomial $\erotuA{\text{order}}4$
\item<6-> Extra side conditions $L$ encode $\forall\overrightarrow{n}\in\mathbb{N}^{k}\!\setminus\!B\s\exists c\sulut{\overrightarrow{n}}^{-1}$
\item<7-> Multiple recurrences $\Rightarrow$ intersect base case sets
\item<8-> $A\cap B$ is kinda $\set{\alpha\circ\beta}{\alpha\in A,\beta\in B}$ as substitutions
\end{itemize}

\frametitle{Limitations}
\begin{itemize}
\item It is only heuristic with unjustified complexity
\item<2-> Domain of sequences is $\mathbb{Z}^{d}$ (not $\mathbb{N}^{d}$)
\item<3-> Generalization: ${\scriptstyle \Sum}\delta_{nj}f_{n\vaihda{}4{{\color{red}+k}}}=f_{j\vaihda{}4{{\color{red}+k}}}$ if $0\leq j\leq m\vaihda{\text{ FAILS}}4{\text{, OK}}$
\item<5-> Interval sum: $\Vaihda{\smash{\makeop{det}A=\Sum[\mathclap{{\color{red}\sigma\in\text{permutation}}}][\hphantom{\text{ermuta}}]\makeop{parity}\sigma\cdot\prod\limits _{j}A_{j,\sigma j}}}6{\Vaihda{{\scriptstyle \Sum[{\color{red}g\in G}][\skip]}g=0\text{ or }a\text{ if }\set{g\neq0}{2g=0}=\left\{ a\right\} }7{\sulut{x+y+z}^{m}={\scriptstyle \Sum[{\color{red}\mathllap{i+}j+n=\mathrlap{m}}][\skip]}m!\frac{{\textstyle x^{i}}}{{\textstyle i!}}\frac{{\textstyle y^{j}}}{{\textstyle j!}}\frac{{\textstyle z^{n}}}{{\textstyle n!}}}}$
\item<8-> Linear indices: ${\scriptstyle \Sum[][{\color{red}km}-1]}f_{n}={\scriptstyle \Sum[][m-1]\s\Sum[j=0][k-1]}f_{{\color{red}kn}+j}$
\item<9-> Division: ${\scriptstyle \Sum\s\Sum[k=1][n]}\binom{m}{n}\binom{n}{k}{\color{red}\frac{{\normalcolor {\textstyle \sulut{-1}^{m-n}2^{n}-2^{-m}}}}{{\textstyle 2^{k}-2^{-k}}}}=2^{m}-1$
\item<10-> No summations in assumptions, hence no:\\
triangle matrix inversion, Bernoulli numbers
\item<11-> Black box integration, hence weak handling of:\\
leading coefficients, side conditions of recurrences
\item<12-> Polynomial coefficients in recurrences (not rational)
\end{itemize}
\end{frame}
\end{document}
