#LyX 2.2 created this file. For more info see http://www.lyx.org/
\lyxformat 508
\begin_document
\begin_header
\save_transient_properties true
\origin unavailable
\textclass beamer
\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}}

\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}
\let\hbar\undefined
\beamertemplatenavigationsymbolsempty
\setbeamertemplate{footline}[frame number]
\end_preamble
\use_default_options true
\begin_modules
my-theorems
\end_modules
\maintain_unincluded_children false
\language english
\language_package default
\inputencoding auto
\fontencoding global
\font_roman "times" "default"
\font_sans "default" "default"
\font_typewriter "default" "default"
\font_math "auto" "auto"
\font_default_family default
\use_non_tex_fonts false
\font_sc false
\font_osf false
\font_sf_scale 100 100
\font_tt_scale 100 100
\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
\index Index
\shortcut idx
\color #004000
\end_index
\leftmargin 2cm
\topmargin 1cm
\rightmargin 2cm
\bottommargin 3cm
\secnumdepth 3
\tocdepth 2
\paragraph_separation indent
\paragraph_indentation default
\quotes_language english
\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{\veny}[3]{\text{{\scalebox{#3}[#2]{\ensuremath{#1}}}}}
{\overset{#2}{↕}\overset{↔#3}{#1}}
\end_inset


\end_layout

\begin_layout Plain Layout
\begin_inset FormulaMacro
\newcommand{\nouse}[2]{\raisebox{#2ex}{\ensuremath{#1}}}
{#1\overset{#2}{\uparrow}}
\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{\integ}[2][\skip]{\int_{#2}^{#1}\negthickspace}
{\int\limits _{#2}^{\s#1}}
\end_inset


\end_layout

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


\end_layout

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


\end_layout

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


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


\end_layout

\begin_layout Plain Layout
\begin_inset FormulaMacro
\newcommand{\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


\begin_inset FormulaMacro
\newcommand{\holdsIn}{\mathrel{\veny{\models}1{-1}}}
{\s⫤\s}
\end_inset


\end_layout

\begin_layout Plain Layout
\begin_inset FormulaMacro
\newcommand{\tihkutaulu}{\setlength\arraycolsep{0pt}}
{{\color{gray}\underset{{\scriptstyle u}}{\underset{{\scriptstyle k}}{\overset{{\scriptstyle t}}{\overset{{\scriptstyle i}}{{\scriptstyle h}}}}}}}
\end_inset


\end_layout

\begin_layout Plain Layout
\begin_inset FormulaMacro
\newcommand{\vaihda}[3]{{\alt<#2->{#3}{\mathrlap{#1}\phantom{#3}}}}
{#1{\color{gray}\overset{{\scriptstyle \s#2}}{/}}#3}
\end_inset


\begin_inset ERT
status collapsed

\begin_layout Plain Layout

%pitenee
\end_layout

\end_inset


\end_layout

\begin_layout Plain Layout
\begin_inset FormulaMacro
\newcommand{\vaihdaa}[3]{{\alt<#2->{\mathrlap{#3}\phantom{#1}}{#1}}}
{#1{\color{gray}\overset{{\scriptstyle \s#2}}{/}}#3}
\end_inset


\begin_inset ERT
status collapsed

\begin_layout Plain Layout

%lyhenee
\end_layout

\end_inset


\end_layout

\begin_layout Plain Layout
\begin_inset FormulaMacro
\newcommand{\vaihdax}[3]{{\alt<#2->{#3}{\phantom{#3}\mathllap{#1}}}}
{#1{\color{gray}\overset{{\scriptstyle \s#2}}{|}}#3}
\end_inset


\begin_inset ERT
status collapsed

\begin_layout Plain Layout

%vasen pitenee
\end_layout

\end_inset


\end_layout

\begin_layout Plain Layout
\begin_inset FormulaMacro
\newcommand{\Vaihda}[3]{{\alt<#2->{#3}{\mathrlap{#1}\phantom{#3}}}}
{\begin{array}{l}
{\displaystyle #1}{\color{gray}\overset{{\scriptstyle \s#2}}{/}}\\
{\displaystyle #3}
\end{array}}
\end_inset


\begin_inset ERT
status collapsed

\begin_layout Plain Layout

%suurenee
\end_layout

\end_inset


\end_layout

\begin_layout Plain Layout
\begin_inset FormulaMacro
\newcommand{\erotuA}[2]{{\alt<#2>{\color{red}#1}{#1}}}
{#1^{{\color{red}\boldsymbol{#2}}}}
\end_inset


\begin_inset Note Comment
status open

\begin_layout Plain Layout

\color red
Punakorostus
\end_layout

\end_inset


\end_layout

\begin_layout Plain Layout
\begin_inset FormulaMacro
\newcommand{\erotuB}[2]{{\alt<#2>{\color{blue}#1}{#1}}}
{#1^{{\color{blue}\boldsymbol{#2}}}}
\end_inset


\begin_inset Note Comment
status open

\begin_layout Plain Layout

\color blue
Sinikorostus
\end_layout

\end_inset


\end_layout

\end_inset


\end_layout

\begin_layout Standard
\begin_inset ERT
status open

\begin_layout Plain Layout


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

\end_inset


\end_layout

\begin_layout Standard
\begin_inset FormulaMacro
\newcommand{\sulut}[1]{\left(#1\right)}
{（#1）}
\end_inset


\end_layout

\begin_layout Standard
\begin_inset FormulaMacro
\newcommand{\Sum}[2][n\text{=}0][m]{\mathchoice{{\textstyle \sum\limits _{#1}^{#2}}\skip}{{\textstyle \mathop{\overset{#2}{\underset{#1}{\Sigma}}}}\skip}{{\textstyle \mathop{\overset{#2}{\underset{#1}{\Sigma}}}}\skip}{{\scriptstyle \mathop{\overset{#2}{\underset{#1}{\Sigma}}}}\skip}}
{\overset{#2}{\underset{#1}{∑}}}
\end_inset


\end_layout

\begin_layout Standard
\begin_inset FormulaMacro
\newcommand{\GeneralizeTransitions}[3]{\vaihdaa{#1}4{\vaihda{\:\phantom{#3}#2}5{\vaihda{#1}6{\phantom{#3}\vaihda{\#f}7{\s s}}}}}
{#1{\color{gray}\overset{4}{/}}{\color{gray}{\scriptscriptstyle #3}}#2{\color{gray}/\cdots}}
\end_inset


\end_layout

\begin_layout Standard
\begin_inset Formula $\mathrlap{}$
\end_inset


\end_layout

\begin_layout Title

\size larger
Recurrence-Driven Summations
\begin_inset Newline newline
\end_inset

in Automated Deduction
\end_layout

\begin_layout Author
\begin_inset Formula $\begin{array}{l}
\text{Visa Nummelin}\\
{\scriptstyle \text{Joint work with Jasmin Blanchette and Sander R. Dahmen}}
\end{array}$
\end_inset


\end_layout

\begin_layout Date
FroCoS 2023
\begin_inset Newline newline
\end_inset

21
\begin_inset script superscript

\begin_layout Plain Layout
st
\end_layout

\end_inset

 September
\end_layout

\begin_layout Frame
\begin_inset Argument 4
status open

\begin_layout Plain Layout
Questions of interest
\end_layout

\end_inset


\end_layout

\begin_deeper
\begin_layout Itemize
\begin_inset Argument 1
status open

\begin_layout Plain Layout
+-
\end_layout

\end_inset

Prove equations between summation expressions
\end_layout

\begin_layout Itemize
Integrate the heuristic to an automatic base prover (in theory)
\end_layout

\begin_layout Itemize
\begin_inset Formula $\Sum n2^{n}=\left(m-1\right)2^{m}+1\qquad\qquad\Sum n^{3}=\sulut{\Sum n}^{2}$
\end_inset


\begin_inset ERT
status collapsed

\begin_layout Plain Layout


\backslash
alt<3>{
\end_layout

\end_inset


\begin_inset Newline newline
\end_inset

Arithmetic and induction are in the heart of the tasks
\begin_inset ERT
status collapsed

\begin_layout Plain Layout

}
\end_layout

\end_inset

 
\end_layout

\begin_layout Itemize
\begin_inset Formula $\sulut{x+y}^{m}=\Sum\binom{m}{n}x^{n}y^{m-n}\qquad\qquad\binom{x+y}{m}=\Sum\binom{x}{n}\binom{y}{m-n}$
\end_inset


\begin_inset ERT
status collapsed

\begin_layout Plain Layout


\backslash
alt<4>{
\end_layout

\end_inset


\begin_inset Newline newline
\end_inset

Theory of holonomic formulas provides ground work
\begin_inset ERT
status collapsed

\begin_layout Plain Layout

}
\end_layout

\end_inset

 
\end_layout

\begin_layout Itemize
\begin_inset Formula $\sulut{x+y}^{m}=\Sum\binom{m}{n}x\sulut{x-n}^{n-1}\sulut{y+n}^{m-n}$
\end_inset


\begin_inset ERT
status collapsed

\begin_layout Plain Layout


\backslash
alt<5>{
\end_layout

\end_inset


\begin_inset Newline newline
\end_inset

Beyond holonomic: demand less recurrences
\begin_inset ERT
status collapsed

\begin_layout Plain Layout

}
\end_layout

\end_inset

 
\end_layout

\begin_layout Itemize
\begin_inset Formula $\Sum f_{m-n}=\Sum f_{n}\qquad\qquad\Sum\Sum[k=0][n]f_{n,k}=\Sum[k=0]\Sum[n=k]f_{n,k}$
\end_inset


\begin_inset ERT
status collapsed

\begin_layout Plain Layout


\backslash
alt<6>{
\end_layout

\end_inset


\begin_inset Newline newline
\end_inset

Beyond holonomic: allow heterogeneous recurrences
\begin_inset ERT
status collapsed

\begin_layout Plain Layout

}
\end_layout

\end_inset

 
\end_layout

\end_deeper
\begin_layout Standard
\begin_inset Separator plain
\end_inset


\end_layout

\begin_layout Frame
\begin_inset Argument 4
status open

\begin_layout Plain Layout
Source of recurrences
\end_layout

\end_inset


\end_layout

\begin_deeper
\begin_layout Standard
Summation 
\begin_inset Formula $\Sum a_{n}=:g_{m}$
\end_inset

 can be defined by
\end_layout

\begin_layout Itemize
the base case 
\begin_inset Formula $g_{0}=a_{0}$
\end_inset

; and
\end_layout

\begin_layout Itemize
the recurrence equation 
\begin_inset Formula $g_{m+1}=g_{m}+a_{m+1}$
\end_inset


\end_layout

\begin_layout Standard
Recurrences are useful to define other sequences too
\end_layout

\begin_layout Itemize
\begin_inset Argument 1
status open

\begin_layout Plain Layout
+(1)-
\end_layout

\end_inset

exponential: 
\begin_inset Formula $b^{n+1}=b\cdot b^{n}$
\end_inset

 
\begin_inset ERT
status collapsed

\begin_layout Plain Layout


\backslash
alt<2>{
\end_layout

\end_inset

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


\begin_inset ERT
status collapsed

\begin_layout Plain Layout

}
\end_layout

\end_inset


\begin_inset space ~
\end_inset


\end_layout

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

 
\begin_inset ERT
status collapsed

\begin_layout Plain Layout


\backslash
alt<3>{
\end_layout

\end_inset

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

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


\begin_inset ERT
status collapsed

\begin_layout Plain Layout

}
\end_layout

\end_inset


\begin_inset space ~
\end_inset


\end_layout

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

 
\begin_inset ERT
status collapsed

\begin_layout Plain Layout


\backslash
alt<4>{
\end_layout

\end_inset

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


\begin_inset ERT
status collapsed

\begin_layout Plain Layout

}
\end_layout

\end_inset


\begin_inset space ~
\end_inset


\end_layout

\begin_layout Itemize
binomial coefficient: for 
\begin_inset Formula $\binom{m}{n}=\frac{m!}{n!\sulut{m-n}!}$
\end_inset

 holds
\begin_inset Newline newline
\end_inset

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


\end_layout

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

: if 
\begin_inset Formula $d=\makeop{deg}P+1$
\end_inset

 then for all 
\begin_inset Formula $n$
\end_inset


\begin_inset Newline newline
\end_inset

 
\begin_inset Formula $P\sulut{n+d}+...+\sulut{-1}^{d-j}\binom{d}{j}P\sulut{n+j}+...+\sulut{-1}^{d}P\sulut n=0$
\end_inset


\end_layout

\end_deeper
\begin_layout Standard
\begin_inset Separator plain
\end_inset


\end_layout

\begin_layout Frame
\begin_inset Argument 4
status open

\begin_layout Plain Layout
Application of recurrences
\end_layout

\end_inset


\end_layout

\begin_deeper
\begin_layout Itemize
Our recurrences are linear, finite in length and
\begin_inset Newline newline
\end_inset

have polynomial coefficients
\end_layout

\begin_layout Itemize
\begin_inset Argument item:2
status open

\begin_layout Plain Layout
2-
\end_layout

\end_inset

To prove equation 
\begin_inset Formula $f_{n}=0$
\end_inset

 for 
\begin_inset Formula $n\in\mathbb{N}$
\end_inset

, it suffices to find
\begin_inset Newline newline
\end_inset

- recurrence 
\begin_inset Formula $c_{n,}{}_{d}f_{n+d}=c_{n,}{}_{d-1}f_{n+d-1}+...+c_{n,}{}_{0}f_{n}$
\end_inset

; and
\begin_inset Newline newline
\end_inset

- prove base cases 
\begin_inset Formula $f_{0}=...=f_{d-1}=0$
\end_inset

 and 
\begin_inset Formula $\exists c_{n,d}^{-1}$
\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Argument item:2
status open

\begin_layout Plain Layout
3-
\end_layout

\end_inset


\begin_inset FormulaMacro
\newcommand{\plusplus}{+\negthickspace...\negthickspace+}
{+...+}
\end_inset


\begin_inset Formula $\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,\Sigma\text{ and substitutions build expressions}}$
\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Argument item:2
status open

\begin_layout Plain Layout
6-
\end_layout

\end_inset

Example decomposition: 
\begin_inset Formula $\vaihdaa{\erotuA{\Sum a_{m-n}}8}9{\qquad C_{m}}\s\vaihda =7{\vaihda{\erotuB -8}9+}\s\vaihda{\erotuB{g_{m}}8}9{G_{m}}\vaihda{}7{{}=0}$
\end_inset


\begin_inset Newline newline
\end_inset


\begin_inset Formula $\vaihda{}9{G_{m}=\vaihdaa{\erotuA -{10}\erotuB{g_{m}}{10}}{11}{\sulut{-1}\cdot g_{m}}}$
\end_inset


\begin_inset Newline newline
\end_inset


\begin_inset Formula $\vaihda{}9{C_{m}=\Sum\vaihda{\erotuA{a_{m-n}}{12}}{13}{B_{m}^{n}}}$
\end_inset


\begin_inset Newline newline
\end_inset


\begin_inset Formula $\vaihda{}{13}{B_{m}^{n}=\vaihda{a_{\erotuA{m-n}{14}}}{15}{\left\{ k\mapsto m-n\right\} a_{k}}}$
\end_inset


\end_layout

\end_deeper
\begin_layout Standard
\begin_inset Separator plain
\end_inset


\end_layout

\begin_layout Frame
\begin_inset Argument 4
status open

\begin_layout Plain Layout
Example (recurrence derivation)
\end_layout

\end_inset


\end_layout

\begin_deeper
\begin_layout Itemize
Key idea: From recurrences of sequences 
\begin_inset Formula $f_{m}^{n}$
\end_inset

 and 
\begin_inset Formula $h_{m}^{n}$
\end_inset


\begin_inset Newline newline
\end_inset

derive recurrences for 
\begin_inset Formula $f_{m}^{n}+h_{m}^{n}$
\end_inset

 , 
\begin_inset Formula $f_{m}^{n}h_{m}^{n}$
\end_inset

 , 
\begin_inset Formula $\Sum f_{m}^{n}$
\end_inset

 , 
\begin_inset Formula $f_{\gamma n+\delta m}^{\alpha n+\beta m}$
\end_inset


\begin_inset Newline newline
\end_inset

 
\end_layout

\begin_layout Itemize
Let 
\begin_inset Formula $g_{0}=a_{0}$
\end_inset

, 
\begin_inset Formula $g_{1}=a_{0}+a_{1}$
\end_inset

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


\end_layout

\begin_layout Itemize
Claim 
\begin_inset Formula $\Sum a_{m-n}=g_{m}$
\end_inset

 for 
\begin_inset Formula $m\geq0$
\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Argument item:2
status open

\begin_layout Plain Layout
2-
\end_layout

\end_inset

Take 
\begin_inset Formula $\erotuA{\text{one}}2$
\end_inset

 recurrence for 
\begin_inset Formula $g$
\end_inset

 and none for 
\begin_inset Formula $a$
\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Argument item:2
status open

\begin_layout Plain Layout
3-
\end_layout

\end_inset

Recurrence of 
\begin_inset Formula $B_{m}^{n}:=a_{m-n}$
\end_inset

 is 
\begin_inset Formula $B_{m+1}^{n+1}=B_{m}^{n}$
\end_inset


\begin_inset Newline newline
\end_inset

because 
\begin_inset Formula $\left(m+1\right)-\left(n+1\right)=m-n$
\end_inset


\end_layout

\end_deeper
\begin_layout Standard
\begin_inset Separator plain
\end_inset


\end_layout

\begin_layout Frame
\begin_inset Argument 4
status open

\begin_layout Plain Layout
Example (recurrence of 
\begin_inset Formula $C_{m}:=\Sum B_{m}^{n}$
\end_inset

)
\end_layout

\end_inset


\end_layout

\begin_deeper
\begin_layout Itemize
Next consider the sequence 
\begin_inset Formula $C_{m}:=\Sum B_{m}^{n}=\Sum a_{m-n}$
\end_inset


\end_layout

\begin_layout Itemize
To normalize indices, for any sequence 
\begin_inset Formula $f$
\end_inset

 we have 
\begin_inset Formula 
\begin{align*}
{\textstyle \Sum}f_{j}^{n+1} & ={\textstyle \Sum}f_{j}^{n}+f_{j}^{m+1}-f_{j}^{0}\\
{\textstyle \Sum}f_{m+1}^{n} & =\left\{ m\mapsto m+1\right\} \left({\textstyle \Sum}f_{m}^{n}-f_{m}^{m}\right)
\end{align*}

\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Argument item:2
status open

\begin_layout Plain Layout
2-
\end_layout

\end_inset

Apply these to 
\begin_inset Formula $0=\Sum\left(B_{m+1}^{n+1}-B_{m}^{n}\right)=\Sum B_{m+1}^{n+1}-C_{m}\vaihda{}3=$
\end_inset


\begin_inset Formula 
\[
\tihkutaulu\smash{\begin{array}{lll}
 & \phantom{\Sum}\\
\vaihda{}3{{}=\Sum B_{m+1}^{n}} & \vaihda{}3{{}+B_{m+1}^{m+1}-B_{m+1}^{0}} & \vaihda{}3{{}-C_{m}}\vaihda{}4{{}=}\\
\vaihda{}4{{}=\Sum[][m+1]B_{m+1}^{n}-B_{m+1}^{m+1}} & \vaihda{}4{{}+B_{m+1}^{m+1}-a_{m+1-0}} & \vaihda{}4{{}-C_{m}}\vaihda{}5{{}=}\\
\vaihda{}5{\mathrlap{{}=C_{m+1}-a_{m+1}-C_{m}}}
\end{array}}
\]

\end_inset


\end_layout

\end_deeper
\begin_layout Standard
\begin_inset Separator plain
\end_inset


\end_layout

\begin_layout Frame
\begin_inset Argument 4
status open

\begin_layout Plain Layout
Example (recurrence of 
\begin_inset Formula $D_{m}:=C_{m}-g_{m}$
\end_inset

)
\end_layout

\end_inset


\end_layout

\begin_deeper
\begin_layout Standard
To find recurrences of 
\begin_inset Formula $D_{m}:=C_{m}-g_{m}$
\end_inset

, use term ordering s.t.
 
\begin_inset Formula $D\prec C,g$
\end_inset

 and derive consequences from known recurrences:
\end_layout

\begin_layout Standard
\begin_inset Formula $\hspace{3em}\begin{aligned}C_{m+1} & =C_{m}+a_{m+1} & \hspace{4.5em}\sulut{\alpha_{m}}\\
g_{m} & =C_{m}-D_{m} & \sulut{\beta_{m}}
\end{aligned}
$
\end_inset


\end_layout

\begin_layout Standard
\begin_inset Formula $\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}=C_{m+2}-D_{m+2}} & \vaihda{}2{\sulut{\beta_{m+2}}}\\
 & \phantom{C_{m+2}=g_{m}+a_{m+2}+a_{m+1}+D_{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{C_{m+2}-D_{m+2}}3 & \sulut{\beta_{m+2}}\\
\hline  & \erotuB{C_{m+2}}3=\erotuA{g_{m}+a_{m+2}+a_{m+1}}3+\erotuB{D_{m+2}}3\\
 & \vaihda{}4{C_{m+2}=C_{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}=C_{m+2}-D_{m+2} & \sulut{\beta_{m+2}}\\
\hline  & C_{m+2}=\erotuA{g_{m}}5+a_{m+2}+\erotuA{a_{m+1}+D_{m+2}}5\\
- & C_{m+2}=\erotuB{C_{m+1}}5+a_{m+2} & \sulut{\alpha_{m+1}}\\
\hline  & \erotuB{C_{m+1}}5=\erotuA{g_{m}+a_{m+1}+D_{m+2}}5\\
 & \vaihda{}6{C_{m+1}=C_{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}=C_{m+2}-D_{m+2} & \sulut{\beta_{m+2}}\\
\hline  & C_{m+2}=g_{m}+a_{m+2}+a_{m+1}+D_{m+2}\\
- & C_{m+2}=C_{m+1}+a_{m+2} & \sulut{\alpha_{m+1}}\\
\hline  & C_{m+1}=\erotuA{g_{m}}7+a_{m+1}+\erotuA{D_{m+2}}7\\
- & C_{m+1}=\erotuB{C_{m}}7+a_{m+1} & \sulut{\alpha_{m}}\\
\hline  & \erotuA{g_{m}}7=\erotuB{C_{m}}7-\erotuA{D_{m+2}}7\\
 & \vaihda{}8{g_{m}=C_{m}-D_{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}=C_{m+2}-D_{m+2} & \sulut{\beta_{m+2}}\\
\hline  & C_{m+2}=g_{m}+a_{m+2}+a_{m+1}+D_{m+2}\\
- & C_{m+2}=C_{m+1}+a_{m+2} & \sulut{\alpha_{m+1}}\\
\hline  & C_{m+1}=g_{m}+a_{m+1}+D_{m+2}\\
- & C_{m+1}=C_{m}+a_{m+1} & \sulut{\alpha_{m}}\\
\hline  & g_{m}=C_{m}-D_{m+2}\\
- & g_{m}=C_{m}-D_{m} & \sulut{\beta_{m}}\\
\hline  & D_{m+2}=D_{m}
\end{array}}}}}$
\end_inset


\end_layout

\end_deeper
\begin_layout Standard
\begin_inset Note Comment
status open

\begin_layout Plain Layout
\begin_inset Separator plain
\end_inset


\end_layout

\begin_layout Frame
\begin_inset Argument 4
status open

\begin_layout Plain Layout
Elimination as key derivation step
\end_layout

\end_inset


\end_layout

\begin_deeper
\begin_layout Itemize
In the derivation of 
\begin_inset Formula $D_{m+2}=D_{m}$
\end_inset

, we 
\emph on
eliminated
\emph default
 terms containing 
\begin_inset Formula $C$
\end_inset

 or 
\begin_inset Formula $g$
\end_inset

 by ordering 
\begin_inset Formula $D\prec C,g$
\end_inset


\end_layout

\begin_layout Plain Layout
Generally:
\end_layout

\begin_layout Itemize
Before applying 
\begin_inset Formula $\Sum$
\end_inset

 to recurrences,
\begin_inset Newline newline
\end_inset

eliminate terms with 
\begin_inset Formula $n$
\end_inset

-dependent coefficients
\end_layout

\begin_layout Itemize
\begin_inset Argument item:2
status open

\begin_layout Plain Layout
2-
\end_layout

\end_inset

Before applying 
\begin_inset Formula $\left\{ n\mapsto0\right\} $
\end_inset

 to recurrences,
\begin_inset Newline newline
\end_inset

eliminate terms with shifted 
\begin_inset Formula $n$
\end_inset

-index
\end_layout

\begin_layout Itemize
\begin_inset Argument item:2
status open

\begin_layout Plain Layout
2-
\end_layout

\end_inset

All linear substitutions are handled by “eliminating shifts”
\end_layout

\begin_layout Itemize
\begin_inset Argument item:2
status open

\begin_layout Plain Layout
3-
\end_layout

\end_inset

Product 
\begin_inset Formula $f_{n}g_{n}=\left\{ m\mapsto n\right\} \left(f_{n}g_{m}\right)$
\end_inset

 is written variable disjoint
\end_layout

\begin_layout Itemize
\begin_inset Argument item:2
status open

\begin_layout Plain Layout
3-
\end_layout

\end_inset

By linearity, recurrences of 
\begin_inset Formula $f_{n}g_{m}$
\end_inset

 are union of
\begin_inset Newline newline
\end_inset

recurrences of 
\begin_inset Formula $f_{n}$
\end_inset

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

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

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


\end_layout

\end_deeper
\end_inset


\begin_inset Separator plain
\end_inset


\end_layout

\begin_layout Frame
\begin_inset Argument 4
status open

\begin_layout Plain Layout
Normalization of sequences
\end_layout

\end_inset


\end_layout

\begin_deeper
\begin_layout Itemize
Homogeneous 
\begin_inset Formula $D_{m+2}{=}D_{m}$
\end_inset

 does induction 
\begin_inset Formula $D_{m}{=}0\Rightarrow D_{m+2}{=}0$
\end_inset


\end_layout

\begin_layout Itemize
Heterogeneous recurrence (e.g.
 
\begin_inset Formula $D_{m+2}-D_{m}=\makeop{bad}_{m}$
\end_inset

) wouldn't
\end_layout

\begin_layout Itemize
\begin_inset Argument item:2
status open

\begin_layout Plain Layout
2-
\end_layout

\end_inset

Fix such by rewriting (
\begin_inset Formula $\to$
\end_inset

) between propagation steps
\end_layout

\begin_layout Itemize
\begin_inset Argument item:2
status open

\begin_layout Plain Layout
2-
\end_layout

\end_inset

E.g.
 
\begin_inset Formula $-B_{m+1}^{m+1}+B_{m+1}^{m+1}-B_{m+1}^{0}\to-a_{m+1}$
\end_inset

 where 
\begin_inset Formula $B_{m}^{n}=a_{m-n}$
\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Argument item:2
status open

\begin_layout Plain Layout
3-
\end_layout

\end_inset

Sort, cancel and distribute in + and 
\begin_inset Formula $\cdot$
\end_inset

 expressions
\end_layout

\begin_layout Itemize
\begin_inset Argument item:2
status open

\begin_layout Plain Layout
3-
\end_layout

\end_inset

Rewrite (
\begin_inset Formula $f,g$
\end_inset

 sequences; 
\begin_inset Formula $\sigma,\widehat{\sigma}$
\end_inset

 substitutions; 
\begin_inset Formula $c\in\mathbb{N}$
\end_inset

)
\begin_inset Formula 
\begin{align*}
{\textstyle \Sum[][c]}f_{\overrightarrow{m}}^{n} & \to f_{\overrightarrow{m}}^{0}+...+f_{\overrightarrow{m}}^{c} & \left\{ \overrightarrow{m}\mapsto\overrightarrow{x}\right\} m_{j} & \to x_{j}\\
g_{\overrightarrow{m}}\cdot{\textstyle \Sum[][x]}f_{\overrightarrow{m}}^{n} & \to{\textstyle \Sum[][x]}g_{\overrightarrow{m}}f_{\overrightarrow{m}}^{n} & \sigma\sulut{f_{\overrightarrow{m}}g_{\overrightarrow{m}}} & \to\sigma f_{\overrightarrow{m}}\cdot\sigma g_{\overrightarrow{m}}\\
\sigma{\textstyle \Sum[][x]}f_{\overrightarrow{m}}^{n} & \to{\textstyle \Sum[][\sigma x]}\sigma f_{\overrightarrow{m}}^{n} & \widehat{\sigma}\sigma f_{\overrightarrow{m}} & \to\sulut{\widehat{\sigma}\circ\sigma}f_{\overrightarrow{m}}
\end{align*}

\end_inset


\end_layout

\end_deeper
\begin_layout Standard
\begin_inset Separator plain
\end_inset


\end_layout

\begin_layout Frame
\begin_inset Argument 4
status open

\begin_layout Plain Layout
Integration to superposition calculus
\end_layout

\end_inset


\end_layout

\begin_deeper
\begin_layout Itemize
The base prover could use higher-order superposition
\end_layout

\begin_layout Itemize
\begin_inset Argument item:2
status open

\begin_layout Plain Layout
2-
\end_layout

\end_inset

During proving detect clauses 
\begin_inset Formula $g\left[\vaihda s3{\overrightarrow{s}}\right]\neq0$
\end_inset

 containing 
\begin_inset Formula $\sum$
\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Argument item:2
status open

\begin_layout Plain Layout
2-
\end_layout

\end_inset

To them apply new inference rule 
\begin_inset Formula 
\[
\frac{g\left[\vaihda s3{\overrightarrow{s}}\right]\neq\vaihda 03{0\vee C}\quad\text{initial recurrences}}{\smash{\bigvee\limits _{\vaihda b3{\overrightarrow{b}}\in B}}g\left[\vaihda b3{\overrightarrow{b}}\right]\neq\vaihda 03{0\vee C\vee L}}\s,\quad\text{where}
\]

\end_inset


\end_layout

\begin_deeper
\begin_layout Itemize
\begin_inset Argument item:2
status open

\begin_layout Plain Layout
2-
\end_layout

\end_inset

choose subterm
\begin_inset Formula $\vaihdax s3{\text{s }\overrightarrow{s}}$
\end_inset

 to be generalized
\end_layout

\begin_layout Itemize
\begin_inset Argument item:2
status open

\begin_layout Plain Layout
2-
\end_layout

\end_inset

get base cases 
\begin_inset Formula $B$
\end_inset

 from recurrences derived to 
\begin_inset Formula $g$
\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Argument item:2
status open

\begin_layout Plain Layout
3-
\end_layout

\end_inset


\begin_inset Formula $L=$
\end_inset

 leading coefficients have inverses
\end_layout

\end_deeper
\end_deeper
\begin_layout Standard
\begin_inset Separator plain
\end_inset


\end_layout

\begin_layout Frame
\begin_inset Argument 4
status open

\begin_layout Plain Layout
Base cases of induction
\end_layout

\end_inset


\end_layout

\begin_deeper
\begin_layout Itemize
To refute 
\begin_inset Formula $g\left[\overrightarrow{s}\right]\neq0$
\end_inset

, prove generally 
\begin_inset Formula $\forall\overrightarrow{n}{\in}\mathbb{N}^{{\scriptscriptstyle \#}\overrightarrow{s}}\negthickspace:g\left[\overrightarrow{n}\right]=0$
\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Argument item:2
status open

\begin_layout Plain Layout
2-
\end_layout

\end_inset

Largest shift in recurrence of 
\begin_inset Formula $g$
\end_inset

 determines base cases
\end_layout

\begin_layout Itemize
\begin_inset Argument item:2
status open

\begin_layout Plain Layout
2-
\end_layout

\end_inset

Base cases of 
\begin_inset Formula $c_{n,b}^{\vaihda{}3{m,a}}g\left[n+b\vaihda{}3{,m+a}\right]+...+c_{n,0}^{\vaihda{}3{m,0}}g\left[n\vaihda{}3{,m}\right]=0$
\end_inset

 are 
\begin_inset Formula $g\left[0\vaihda{}3{,i}\right]=...=g\left[b-1\vaihda{}3{,i}\right]=\vaihda 03{0=g\left[i,0\right]=...=g\left[i,a-1\right]\s\forall i}$
\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Argument item:2
status open

\begin_layout Plain Layout
4-
\end_layout

\end_inset

Compare shifts (e.g.
 
\begin_inset Formula $n,m{+}3$
\end_inset

 vs 
\begin_inset Formula $n{+}3,m$
\end_inset

) lexicographically
\end_layout

\begin_layout Itemize
\begin_inset Argument item:2
status open

\begin_layout Plain Layout
4-
\end_layout

\end_inset

With many recurrences, intersect base case sets
\end_layout

\end_deeper
\begin_layout Standard
\begin_inset Separator plain
\end_inset


\end_layout

\begin_layout Frame
\begin_inset Argument 4
status open

\begin_layout Plain Layout
Conclusion
\end_layout

\end_inset


\end_layout

\begin_deeper
\begin_layout Itemize
Recurrences prove an induction step for an equation
\end_layout

\begin_layout Itemize
Recurrences of a sum can be derived from
\begin_inset Newline newline
\end_inset

recurrences of the summand
\end_layout

\begin_layout Itemize
This way holonomic sequences can be integrated to
\begin_inset Newline newline
\end_inset

superposition and other proof calculi
\end_layout

\end_deeper
\end_body
\end_document
