#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 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}
\usepackage{sansmathfonts}
\let\hbar\undefined
\usepackage{arev}
\beamertemplatenavigationsymbolsempty
\setbeamertemplate{footline}[frame number]
\end_preamble
\use_default_options true
\begin_modules
theorems-std
\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
\use_microtype false
\use_dash_ligatures false
\graphics default
\default_output_format default
\output_sync 0
\bibtex_command default
\index_command default
\paperfontsize default
\spacing other 0.7
\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 2cm
\topmargin 1cm
\rightmargin 2cm
\bottommargin 3cm
\secnumdepth 3
\tocdepth 2
\paragraph_separation indent
\paragraph_indentation default
\is_math_indent 0
\math_numbering_side default
\quotes_style english
\dynamic_quotes 0
\papercolumns 1
\papersides 1
\paperpagestyle default
\tracking_changes false
\output_changes false
\html_math_output 0
\html_css_as_file 0
\html_be_strict false
\end_header

\begin_body

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

\begin_layout Plain Layout
\begin_inset ERT
status open

\begin_layout Plain Layout


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

\begin_layout Plain Layout


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

\end_inset


\end_layout

\begin_layout Plain Layout
\begin_inset FormulaMacro
\newcommand{\quad}{\oldqquad}
{     }
\end_inset


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


\begin_inset FormulaMacro
\newcommand{\skip}{}
{​}
\end_inset


\begin_inset FormulaMacro
\newcommand{\s}{\ }
{ }
\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{\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{\holdsIn}{\mathrel{\veny{\models}1{-1}}}
{\s⫤\s}
\end_inset


\end_layout

\end_inset


\end_layout

\begin_layout Standard
\begin_inset FormulaMacro
\newcommand{\cst}[1]{\textsf{#1}}
\end_inset


\begin_inset FormulaMacro
\newcommand{\namedsimp}[3]{\frac{#2}{#3}\text{\textsc{#1}}}
\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{\simprule}[2]{\begin{array}{c}
\negthickspace#1\negthickspace\\
\hline\hline \negthickspace#2\negthickspace
\end{array}}
{\begin{array}{c}
#1\\
\hline\hline #2
\end{array}}
\end_inset


\end_layout

\begin_layout Standard
\begin_inset FormulaMacro
\newcommand{\DenseTable}{\setlength\arraycolsep{0pt}}
{{\color{gray}\underset{e}{\underset{s}{\overset{d}{\overset{e}{{\scriptstyle n}}}}}}}
\end_inset


\end_layout

\begin_layout Standard
\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 Standard
\begin_inset FormulaMacro
\newcommand{\Sum}[2][n\text{=}0][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}}
{\mathop{\overset{#2}{\underset{#1}{\sum}}}}
\end_inset


\end_layout

\begin_layout Standard
\begin_inset FormulaMacro
\newcommand{\operatorEquality}[1]{\mop{\back{.05}\veny{#1}{.9}{.9}\back{.05}}}
{#1}
\end_inset


\end_layout

\begin_layout Standard
\begin_inset FormulaMacro
\newcommand{\bigred}[1]{\mathclap{\smash{\nouse{\veny{{\color{red}#1}}{1.5}2}{-.5}}}}
{{\color{red}#1}}
\end_inset


\end_layout

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

\begin_layout Standard

\color none
\begin_inset FormulaMacro
\newcommand{\tableOper}[1]{\s#1\back{0.6}}
{#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
2
\begin_inset script superscript

\begin_layout Plain Layout
nd
\end_layout

\end_inset

 June 2023
\end_layout

\begin_layout FrameTitle
Questions of interest
\end_layout

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


\end_layout

\begin_layout Itemize
\begin_inset Formula $\Sum6n^{2}=m\sulut{m+1}\sulut{2m+1}\quad\Sum n^{3}=\sulut{\Sum n}^{2}$
\end_inset


\end_layout

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


\end_layout

\begin_layout Itemize
\begin_inset Argument item:2
status open

\begin_layout Plain Layout

2-
\end_layout

\end_inset


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


\end_layout

\begin_layout FrameTitle
Source of recurrences
\end_layout

\begin_layout Standard
Summation 
\begin_inset Formula ${\scriptstyle \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$
\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

\begin_layout FrameTitle
Application of recurrences
\end_layout

\begin_layout Itemize
Recurrences are linear, with polynomial coefficients, and finite in length
\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,\sum\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 $\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}$
\end_inset


\begin_inset Newline newline
\end_inset


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


\begin_inset Newline newline
\end_inset


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


\begin_inset Newline newline
\end_inset


\begin_inset Formula $\vaihda{}{13}{D_{x,y,m}={\scriptstyle \Sum}\vaihda{\erotuA{\binom{x}{n}\binom{y}{m-n}}{14}}{15}{E_{x,y,m,n}}}$
\end_inset


\begin_inset Newline newline
\end_inset


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


\begin_inset Newline newline
\end_inset


\begin_inset Formula $\vaihda{}{17}{F_{y,m,n}=\vaihda{\binom{y}{\erotuA{m-n}{18}}}{19}{\left\{ u\mapsto m-n\right\} C_{y,u}}}$
\end_inset


\end_layout

\begin_layout FrameTitle
Informal example
\end_layout

\begin_layout Itemize
Principle of propagation:
\begin_inset Newline newline
\end_inset

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

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

, 
\begin_inset Formula $h_{n,m,k}$
\end_inset


\begin_inset Newline newline
\end_inset

derive recurrences to 
\begin_inset Formula $f_{n}+g_{n}$
\end_inset

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

, 
\begin_inset Formula ${\scriptstyle \Sum}h_{n,m,k}$
\end_inset

, 
\begin_inset Formula $f_{\text{matrix}\cdot n}$
\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 $g_{m+2}=g_{m}+a_{m+1}+a_{m+2}$
\end_inset


\end_layout

\begin_layout Itemize
Claim 
\begin_inset Formula $g_{m}=\Sum a_{n}$
\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

Recurrence of 
\begin_inset Formula $A_{m}:=\Sum a_{n}$
\end_inset

 is 
\begin_inset Formula $A_{m+1}=A_{m}+a_{m+1}$
\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}:=g_{m}-A_{m}$
\end_inset

 is found by deriving consequences w.r.t.
 term ordering s.t.
 
\begin_inset Formula $B\prec g,A$
\end_inset


\end_layout

\begin_layout FrameTitle
Informal example (recurrence of 
\begin_inset Formula $B_{m}:=g_{m}-A_{m}$
\end_inset

)
\end_layout

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


\end_layout

\begin_layout FrameTitle
Informal example (induction)
\end_layout

\begin_layout Itemize
\begin_inset Formula $B_{m+2}=B_{m}$
\end_inset

 means if 
\begin_inset Formula $g_{m}=\Sum a_{n}$
\end_inset

 then 
\begin_inset Formula $g_{m+2}=\Sum[][m+2]a_{n}$
\end_inset


\end_layout

\begin_deeper
\begin_layout Itemize
Verifies the induction step
\end_layout

\end_deeper
\begin_layout Itemize
Induction base cases 
\begin_inset Formula $g_{0}=\Sum[][0]a_{n}$
\end_inset

 and 
\begin_inset Formula $g_{1}=\Sum[][1]a_{n}$
\end_inset


\end_layout

\begin_deeper
\begin_layout Itemize
Summations can be expanded, e.g., 
\begin_inset Formula $\Sum[][1]a_{n}=a_{0}+a_{1}$
\end_inset


\end_layout

\begin_layout Itemize
Leave for the base theorem prover
\end_layout

\end_deeper
\begin_layout FrameTitle
Operator polynomial notation
\end_layout

\begin_layout Definition
Operator polynomials are noncommutative 
\begin_inset Formula $\mathbb{Z}$
\end_inset

-algebra
\begin_inset Newline newline
\end_inset

(so closed under addition and composition as product)
\begin_inset Newline newline
\end_inset

spanned by two types of indeterminates:
\end_layout

\begin_deeper
\begin_layout Itemize
Shifts 
\begin_inset Formula $N,M,...$
\end_inset

 operating 
\begin_inset Formula $\sulut{Mf}_{n,m,...}=f_{n,m+1,...}$
\end_inset


\end_layout

\begin_layout Itemize
Multipliers 
\begin_inset Formula $n,m,...$
\end_inset

 operating 
\begin_inset Formula $\sulut{mf}_{n,m,...}=m\cdot f_{n,m,...}$
\end_inset


\end_layout

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

\begin_layout Plain Layout

2-
\end_layout

\end_inset


\begin_inset ERT
status collapsed

\begin_layout Plain Layout


\backslash
smash{
\backslash
parbox[t]{
\backslash
linewidth}{
\end_layout

\end_inset


\begin_inset space ~
\end_inset


\begin_inset Newline newline
\end_inset


\color white
——
\color inherit
Noncommutation: 
\begin_inset Formula $Nn=\sulut{n+1}N$
\end_inset


\begin_inset ERT
status collapsed

\begin_layout Plain Layout


\backslash
alt<2>{
\end_layout

\end_inset

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

\end_inset


\color none

\begin_inset ERT
status collapsed

\begin_layout Plain Layout

}{}}}
\end_layout

\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 ERT
status collapsed

\begin_layout Plain Layout


\backslash
smash{
\backslash
parbox[t]{
\backslash
linewidth}{
\end_layout

\end_inset


\begin_inset space ~
\end_inset


\begin_inset Newline newline
\end_inset


\color white
——
\color inherit
Example: 
\begin_inset Formula $\vaihda{}5(\vaihdaa{mM-nM+{}}4{\sulut{m-n+1}}M-m-1\vaihda{}5{)\binom{m}{n}=\vaihda{}60}$
\end_inset


\begin_inset ERT
status collapsed

\begin_layout Plain Layout


\backslash
alt<5>{
\end_layout

\end_inset


\begin_inset Newline newline
\end_inset


\color white
——Example
\color inherit

\begin_inset Formula $=\sulut{m-n+1}\binom{m+1}{n}-\sulut{m+1}\binom{m}{n}=0$
\end_inset


\color none

\begin_inset ERT
status collapsed

\begin_layout Plain Layout

}{}}}
\end_layout

\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Argument item:2
status open

\begin_layout Plain Layout

6-
\end_layout

\end_inset

Example: 
\begin_inset Formula $\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_inset


\end_layout

\begin_layout FrameTitle
Elimination of sequences and operators
\end_layout

\begin_layout Itemize
Recurrences have form 
\begin_inset Formula $P_{1}f^{1}+...+P_{k}f^{k}=0$
\end_inset

 where
\begin_inset Newline newline
\end_inset


\begin_inset Formula $P_{j}$
\end_inset

's are operator polynomials and 
\begin_inset Formula $f^{j}$
\end_inset

's sequences
\end_layout

\begin_layout Itemize
\begin_inset Argument item:2
status open

\begin_layout Plain Layout

2-
\end_layout

\end_inset

Terms have form 
\begin_inset Formula $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$
\end_inset


\begin_inset Newline newline
\end_inset

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

's are variables, 
\begin_inset Formula $f$
\end_inset

 is sequence, 
\begin_inset Formula $\pm$
\end_inset


\begin_inset Formula $y,x_{j},z_{j}\in\mathbb{N}$
\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 ERT
status collapsed

\begin_layout Plain Layout


\backslash
smash{
\backslash
parbox[t]{
\backslash
linewidth}{
\end_layout

\end_inset


\begin_inset space ~
\end_inset


\begin_inset Newline newline
\end_inset


\color white
——
\color inherit
Linearly order terms by weighting 
\begin_inset Formula $x_{j}$
\end_inset

'
\size small
s
\size default
, 
\begin_inset Formula $z_{j}$
\end_inset

'
\size small
s
\size default
 
\size small
and
\size default

\begin_inset space ~
\end_inset


\begin_inset Formula $f$
\end_inset


\color none

\begin_inset ERT
status collapsed

\begin_layout Plain Layout


\backslash
visible<4-8>{
\end_layout

\end_inset


\begin_inset Newline newline
\end_inset


\color white
—
\color none
 
\begin_inset Formula $\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}$
\end_inset


\begin_inset ERT
status collapsed

\begin_layout Plain Layout

}{}}}
\end_layout

\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Argument item:2
status open

\begin_layout Plain Layout

9-
\end_layout

\end_inset

To eliminate 
\begin_inset Formula $n_{j}$
\end_inset

, 
\begin_inset Formula $N_{j}$
\end_inset

 or 
\begin_inset Formula $f$
\end_inset

, make its weight dominant
\end_layout

\begin_layout Itemize
\begin_inset Argument item:2
status open

\begin_layout Plain Layout

10-
\end_layout

\end_inset

To superpose two recurrences, left-multiply them by (the least number of)
 indeterminates s.t.
 maximal terms become equal, and subtract
\end_layout

\begin_layout Itemize
\begin_inset Argument item:2
status open

\begin_layout Plain Layout

11-
\end_layout

\end_inset

Eliminating 
\begin_inset Formula $h$
\end_inset

: 
\begin_inset Formula $\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_inset


\end_layout

\begin_layout FrameTitle
Propagation 1/4: addition
\end_layout

\begin_layout Itemize
Let sequence 
\begin_inset Formula $f^{j}$
\end_inset

 have set of recurrences 
\begin_inset Formula $F_{j}$
\end_inset

 (
\begin_inset Formula $j=1,2$
\end_inset

)
\end_layout

\begin_layout Itemize
To find recurrences of 
\begin_inset Formula $f^{+}:=\vaihda{}2{P_{1}}f^{1}+\vaihda{}2{P_{2}}f^{2}$
\end_inset


\begin_inset Newline newline
\end_inset

eliminate 
\begin_inset Formula $f^{1},f^{2}$
\end_inset

 from 
\begin_inset Formula $F_{1}\cup F_{2}\cup\left\{ \vaihda{}2{P_{1}}f^{1}+\vaihda{}2{P_{2}}f^{2}-f^{+}=0\right\} $
\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Argument item:2
status open

\begin_layout Plain Layout

3-
\end_layout

\end_inset

In the earlier example 
\begin_inset Formula $B_{m}:=g_{m}-A_{m}$
\end_inset


\begin_inset Formula 
\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_inset


\end_layout

\begin_layout FrameTitle
Propagation 2/4: summation
\end_layout

\begin_layout Itemize
Let sequence 
\begin_inset Formula $f$
\end_inset

 have set of recurrences 
\begin_inset Formula $F$
\end_inset


\end_layout

\begin_layout Itemize
To find recurrences of 
\begin_inset Formula ${\scriptstyle \Sum}f_{n,m,...}$
\end_inset


\begin_inset Newline newline
\end_inset

first eliminate multiplier 
\begin_inset Formula $n$
\end_inset

 from 
\begin_inset Formula $F$
\end_inset

, then “commute”:
\begin_inset Newline newline
\end_inset


\begin_inset Formula ${\scriptstyle \Sum}P\sulut{N,M,m}f=P\sulut{1,M,m}{\scriptstyle \Sum}f+\text{boundary terms}$
\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Argument item:2
status open

\begin_layout Plain Layout

2-
\end_layout

\end_inset


\begin_inset Formula ${\scriptstyle \Sum}X=X{\scriptstyle \Sum}$
\end_inset

 for indeterminate 
\begin_inset Formula $X\not\in\left\{ n,N,M\right\} $
\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Argument item:2
status open

\begin_layout Plain Layout

2-
\end_layout

\end_inset


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


\end_layout

\begin_layout Itemize
\begin_inset Argument item:2
status open

\begin_layout Plain Layout

2-
\end_layout

\end_inset


\begin_inset Formula ${\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_inset


\end_layout

\begin_layout FrameTitle
Propagation 2/4: summation example
\end_layout

\begin_layout Itemize
\begin_inset Argument 1
status open

\begin_layout Plain Layout

+-
\end_layout

\end_inset

Claim: 
\begin_inset Formula $\Sum\binom{m}{n}=2^{m}$
\end_inset


\end_layout

\begin_layout Itemize
Recurrences 
\begin_inset Formula $0=\sulut{\sulut{m-n+1}M-m-1}\binom{m}{n}$
\end_inset

 and 
\begin_inset Formula $0=\sulut{\sulut{n+1}N-m+n}\binom{m}{n}$
\end_inset


\end_layout

\begin_layout Itemize
First, 
\begin_inset Formula $n$
\end_inset

 eliminated: 
\begin_inset Formula $0=\sulut{\sulut{m+1}\sulut{NM-N-1}}\binom{m}{n}$
\end_inset


\end_layout

\begin_layout Itemize
Then 
\begin_inset Formula $0=\smash{\Sum}\sulut{\sulut{m+1}\sulut{NM-N-1}}\binom{m}{n}=$
\end_inset


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

\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Argument item:2
status open

\begin_layout Plain Layout

11-
\end_layout

\end_inset


\begin_inset Formula $\sulut{m+1}\sulut{M-2}\sulut{\smash{\Sum}\binom{m}{n}-2^{m}}=0$
\end_inset

 since 
\begin_inset Formula $\sulut{M-2}2^{m}=0$
\end_inset


\end_layout

\begin_layout FrameTitle
Propagation 3/4: linear substitution
\end_layout

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

 and 
\begin_inset Formula $F=f_{\vaihda m{15}{\overrightarrow{m}}}$
\end_inset

's recurrences
\end_layout

\begin_layout Itemize
\begin_inset Formula $\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}}}$
\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 ERT
status collapsed

\begin_layout Plain Layout


\backslash
alt<5->{
\end_layout

\end_inset

Overload 
\begin_inset Formula $\vaihda N{17}{\overrightarrow{N}^{x}}:=\vaihda{M^{2}}{17}{\overrightarrow{M}^{Ax}}$
\end_inset

.
 Eliminate 
\begin_inset Formula $\vaihda M{17}{\overrightarrow{M}}$
\end_inset

 from 
\begin_inset Formula $F\cup\{\vaihda{M^{2}}{17}{\overrightarrow{M}^{A\delta_{j}}}=\vaihda N{17}{N_{j}}\vaihda{\}}{17}{\mathrlap{\}_{j=1}^{\#n}}}$
\end_inset


\begin_inset ERT
status collapsed

\begin_layout Plain Layout

}{
\end_layout

\end_inset


\begin_inset Formula $N\left\{ m\mapsto2n\right\} =\left\{ m\mapsto2n\right\} M^{2}$
\end_inset

 because 
\begin_inset Formula $f_{2\sulut{n+1}}=f_{2n+2}$
\end_inset


\begin_inset ERT
status collapsed

\begin_layout Plain Layout

}
\end_layout

\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Argument item:2
status open

\begin_layout Plain Layout

6-
\end_layout

\end_inset


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


\end_layout

\begin_layout Itemize
\begin_inset Argument item:2
status open

\begin_layout Plain Layout

7-14
\end_layout

\end_inset

Example: for 
\begin_inset Formula $\sulut{2n}!=$
\end_inset


\begin_inset Formula $\left\{ m\mapsto2n\right\} m!$
\end_inset

 omitting “=0” 
\begin_inset Formula 
\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*}

\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Argument item:2
status open

\begin_layout Plain Layout

14
\end_layout

\end_inset

Hence 
\begin_inset Formula $\sulut{N+\sulut{2n+2}\sulut{2n+1}}\s\sulut{2n}!=0$
\end_inset


\end_layout

\begin_layout FrameTitle
Propagation 4/4: product
\end_layout

\begin_layout Itemize
Let sequences 
\begin_inset Formula $f,g$
\end_inset

 have sets of recurrences 
\begin_inset Formula $F,G$
\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Formula $f_{n}g_{n}=\left\{ m\mapsto n\right\} f_{n}g_{m}$
\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Argument item:2
status open

\begin_layout Plain Layout

2-
\end_layout

\end_inset

For disjoint indices, using linearity,
\begin_inset Newline newline
\end_inset


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


\end_layout

\begin_layout Itemize
\begin_inset Argument item:2
status open

\begin_layout Plain Layout

4-
\end_layout

\end_inset

So recurrences of 
\begin_inset Formula $f_{n}g_{m}$
\end_inset

 are 
\begin_inset Formula $F\cdot g_{m}\cup f_{n}\cdot\left\{ n\mapsto m\right\} G$
\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Argument item:2
status open

\begin_layout Plain Layout

4-
\end_layout

\end_inset

Then propagate to substitution (block matrix 
\begin_inset Formula $\bigg[{\scriptstyle \begin{subarray}{c}
\mathcal{I}\\
\mathcal{I}
\end{subarray}}\bigg]$
\end_inset

) 
\begin_inset ERT
status open

\begin_layout Plain Layout

%TODO Wandermonde example?
\end_layout

\end_inset


\end_layout

\begin_layout FrameTitle
Homogenization by iteration
\end_layout

\begin_layout Itemize
To prove 
\begin_inset Formula $f=0$
\end_inset

 we search homogeneous 
\begin_inset Formula $Pf=0$
\end_inset


\end_layout

\begin_layout Itemize
Propagation can give heterogeneous 
\begin_inset Formula $Pf=f'$
\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Argument item:2
status open

\begin_layout Plain Layout

2-
\end_layout

\end_inset

New goal: 
\begin_inset Formula $f'=0$
\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Argument item:2
status open

\begin_layout Plain Layout

2-
\end_layout

\end_inset

Suffices to iterate propagation on 
\begin_inset Formula $f'$
\end_inset

 because
\begin_inset Newline newline
\end_inset

if 
\begin_inset Formula $P_{2}f'=\vaihda 03{f''}$
\end_inset

 then 
\begin_inset Formula $P_{2}Pf=\vaihda 03{f''\text{ etc. on }f''}$
\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Argument item:2
status open

\begin_layout Plain Layout

3-
\end_layout

\end_inset

Termination is provable by term order on sequences
\end_layout

\begin_layout FrameTitle
Normalization of sequences
\end_layout

\begin_layout Itemize
To simplify sequences between propagation steps
\end_layout

\begin_layout Itemize
Normal writing order of operations:
\begin_inset Newline newline
\end_inset


\color gray
out/root 
\begin_inset Formula $\gets$
\end_inset


\color inherit
 +, 
\begin_inset Formula $\sum$
\end_inset

, 
\begin_inset Formula $\cdot$
\end_inset

, substitutions 
\color gray

\begin_inset Formula $\to$
\end_inset

 in/leaves
\end_layout

\begin_layout Itemize
\begin_inset Argument item:2
status open

\begin_layout Plain Layout

2-
\end_layout

\end_inset


\begin_inset Formula $\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 \sum,\cdot,substitutions over +}}$
\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Argument item:2
status open

\begin_layout Plain Layout

3-
\end_layout

\end_inset

Sort associativity, commutativity, inverse
\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,\sigma'$
\end_inset

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

)
\begin_inset Formula 
\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_inset


\end_layout

\begin_layout FrameTitle
Integration to superposition calculus
\end_layout

\begin_layout Itemize
Input task must use our built-in 
\begin_inset Formula $\sum$
\end_inset


\begin_inset ERT
status collapsed

\begin_layout Plain Layout


\backslash
alt<2->{, hence}{}
\end_layout

\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

its domain (integers)
\begin_inset ERT
status collapsed

\begin_layout Plain Layout


\backslash
alt<3->{; and}{}
\end_layout

\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Argument item:2
status open

\begin_layout Plain Layout

3-
\end_layout

\end_inset

its range (commutative 
\begin_inset ERT
status collapsed

\begin_layout Plain Layout


\backslash
alt<4->{
\end_layout

\end_inset


\strikeout on
monoid
\strikeout default
 group)
\begin_inset ERT
status collapsed

\begin_layout Plain Layout

}{monoid)}
\end_layout

\end_inset


\end_layout

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

\begin_layout Plain Layout

5-
\end_layout

\end_inset

Ring as range is optional 
\begin_inset Formula $\Rightarrow$
\end_inset

 search 
\begin_inset Formula $\cdot$
\end_inset

 on demand
\end_layout

\begin_layout Itemize
\begin_inset Argument item:2
status open

\begin_layout Plain Layout

6-
\end_layout

\end_inset

During proving detect clauses 
\begin_inset Formula $g\left[s\right]{\neq}0$
\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

6-
\end_layout

\end_inset

To them apply inference rule 
\begin_inset Formula 
\[
\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}
\]

\end_inset


\end_layout

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

\begin_layout Plain Layout

6-
\end_layout

\end_inset

choose subterms 
\begin_inset Formula $s$
\end_inset

 to be generalized
\end_layout

\begin_layout Itemize
\begin_inset Argument item:2
status open

\begin_layout Plain Layout

6-
\end_layout

\end_inset

get base cases 
\begin_inset Formula $B$
\end_inset

 from final recurrences
\end_layout

\begin_layout Itemize
\begin_inset Argument item:2
status open

\begin_layout Plain Layout

7-
\end_layout

\end_inset


\begin_inset Formula $L=$
\end_inset

 leading coefficients have inverses
\end_layout

\end_deeper
\begin_layout FrameTitle
Subterm generalization
\end_layout

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

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


\end_layout

\begin_layout Itemize
We must choose subterms 
\begin_inset Formula $s$
\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Argument item:2
status open

\begin_layout Plain Layout

2-
\end_layout

\end_inset

Example: #=length and average axiom 
\begin_inset Formula $\mu f=\Sum[n=1][\#f]{\displaystyle \frac{f_{n}}{\#f}}$
\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Argument item:2
status open

\begin_layout Plain Layout

2-
\end_layout

\end_inset

Claim 
\begin_inset Formula $\mu\sulut{f-\mu f}^{2}=\mu\:f^{2}-\sulut{\mu f}^{2}$
\end_inset

 
\begin_inset ERT
status collapsed

\begin_layout Plain Layout


\backslash
alt<3->{
\end_layout

\end_inset

negated expands
\begin_inset ERT
status collapsed

\begin_layout Plain Layout

}{}
\end_layout

\end_inset


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

\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Argument item:2
status open

\begin_layout Plain Layout

4-
\end_layout

\end_inset


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


\end_layout

\begin_layout Itemize
\begin_inset Argument item:2
status open

\begin_layout Plain Layout

8-
\end_layout

\end_inset

E.g., generalize nonnumeral 
\begin_inset Formula $\mathbb{Z}$
\end_inset

-constants bottom-up
\end_layout

\begin_layout Itemize
\begin_inset Argument item:2
status open

\begin_layout Plain Layout

9-
\end_layout

\end_inset

 
\begin_inset Formula $\mathrlap{\text{Afterwards identify sequences, last their recurrences}}$
\end_inset


\end_layout

\begin_layout FrameTitle
Induction
\end_layout

\begin_layout Itemize
Let 
\begin_inset Formula $Pf=0$
\end_inset

 be found to prove 
\begin_inset Formula $f=0$
\end_inset


\end_layout

\begin_layout Itemize
Apply induction on 
\begin_inset Formula $\mathbb{N}^{k}$
\end_inset

 (upto 
\begin_inset Formula $2^{k}$
\end_inset

 times on 
\begin_inset Formula $\mathbb{Z}^{k}$
\end_inset

)
\end_layout

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

 + lower 
\begin_inset Formula $\erotuA{\text{order}}4$
\end_inset

 terms, then
\begin_inset Newline newline
\end_inset

base cases are 
\begin_inset Formula $\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[}}}}$
\end_inset

 
\begin_inset Newline newline
\end_inset


\begin_inset ERT
status collapsed

\begin_layout Plain Layout


\backslash
alt<3->{
\end_layout

\end_inset

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

's are free variables of the base prover
\begin_inset ERT
status collapsed

\begin_layout Plain Layout

}{~}
\end_layout

\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Argument item:2
status open

\begin_layout Plain Layout

4-
\end_layout

\end_inset

Induction w.r.t.
 any monomial 
\begin_inset Formula $\erotuA{\text{order}}4$
\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Argument item:2
status open

\begin_layout Plain Layout

6-
\end_layout

\end_inset

Extra side conditions 
\begin_inset Formula $L$
\end_inset

 encode 
\begin_inset Formula $\forall\overrightarrow{n}\in\mathbb{N}^{k}\!\setminus\!B\s\exists c\sulut{\overrightarrow{n}}^{-1}$
\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Argument item:2
status open

\begin_layout Plain Layout

7-
\end_layout

\end_inset

Multiple recurrences 
\begin_inset Formula $\Rightarrow$
\end_inset

 intersect base case sets
\end_layout

\begin_layout Itemize
\begin_inset Argument item:2
status open

\begin_layout Plain Layout

8-
\end_layout

\end_inset


\begin_inset Formula $A\cap B$
\end_inset

 is kinda 
\begin_inset Formula $\set{\alpha\circ\beta}{\alpha\in A,\beta\in B}$
\end_inset

 as substitutions
\end_layout

\begin_layout FrameTitle
Limitations
\end_layout

\begin_layout Itemize
It is only heuristic with unjustified complexity
\end_layout

\begin_layout Itemize
\begin_inset Argument item:2
status open

\begin_layout Plain Layout

2-
\end_layout

\end_inset

Domain of sequences is 
\begin_inset Formula $\mathbb{Z}^{d}$
\end_inset

 (not 
\begin_inset Formula $\mathbb{N}^{d}$
\end_inset

)
\end_layout

\begin_layout Itemize
\begin_inset Argument item:2
status open

\begin_layout Plain Layout

3-
\end_layout

\end_inset

Generalization: 
\begin_inset Formula ${\scriptstyle \Sum}\delta_{nj}f_{n\vaihda{}4{{\color{red}+k}}}=f_{j\vaihda{}4{{\color{red}+k}}}$
\end_inset

 if 
\begin_inset Formula $0\leq j\leq m\vaihda{\text{ FAILS}}4{\text{, OK}}$
\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Argument item:2
status open

\begin_layout Plain Layout

5-
\end_layout

\end_inset

Interval sum: 
\begin_inset Formula $\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!}}}}$
\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Argument item:2
status open

\begin_layout Plain Layout

8-
\end_layout

\end_inset

Linear indices: 
\begin_inset Formula ${\scriptstyle \Sum[][{\color{red}km}-1]}f_{n}={\scriptstyle \Sum[][m-1]\s\Sum[j=0][k-1]}f_{{\color{red}kn}+j}$
\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Argument item:2
status open

\begin_layout Plain Layout

9-
\end_layout

\end_inset

Division: 
\begin_inset Formula ${\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$
\end_inset


\end_layout

\begin_layout Itemize
\begin_inset Argument item:2
status open

\begin_layout Plain Layout

10-
\end_layout

\end_inset

No summations in assumptions, hence no:
\begin_inset Newline newline
\end_inset

triangle matrix inversion, Bernoulli numbers
\end_layout

\begin_layout Itemize
\begin_inset Argument item:2
status open

\begin_layout Plain Layout

11-
\end_layout

\end_inset

Black box integration, hence weak handling of:
\begin_inset Newline newline
\end_inset

leading coefficients, side conditions of recurrences
\end_layout

\begin_layout Itemize
\begin_inset Argument item:2
status open

\begin_layout Plain Layout

12-
\end_layout

\end_inset

Polynomial coefficients in recurrences (not rational)
\end_layout

\begin_layout Standard
\begin_inset Note Note
status collapsed

\begin_layout Frame
\begin_inset Argument 4
status open

\begin_layout Plain Layout
Representing polynomials in Lean
\end_layout

\end_inset


\end_layout

\begin_deeper
\begin_layout Itemize
Operations of polynomials needed to compute Gröbner-bases:
\end_layout

\begin_deeper
\begin_layout Itemize
addition
\end_layout

\begin_layout Itemize
multiplication 
\color gray
(by monomial)
\end_layout

\begin_layout Itemize
determine leading (least simple) monomial
\end_layout

\begin_layout Itemize
test for 0
\end_layout

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

\begin_layout Plain Layout

2-
\end_layout

\end_inset


\begin_inset Flex Alternative
status open

\begin_layout Plain Layout
\begin_inset Argument 1
status open

\begin_layout Plain Layout

4-
\end_layout

\end_inset


\begin_inset Argument 2
status open

\begin_layout Plain Layout

\strikeout on
\color magenta
\begin_inset Formula ${\color{black}\text{Tensor / nD-matrix of coefficients}}$
\end_inset


\end_layout

\end_inset


\begin_inset Flex Structure
status collapsed

\begin_layout Plain Layout

\color black
Tensor / nD-matrix of coefficients
\end_layout

\end_inset


\end_layout

\end_inset


\begin_inset Newline newline
\end_inset


\begin_inset Flex Visible
status open

\begin_layout Plain Layout

\color none
\begin_inset Argument 1
status open

\begin_layout Plain Layout

3-
\end_layout

\end_inset

wastes space: 
\begin_inset Formula $\sum_{j=1}^{n}X_{j}^{2}$
\end_inset

 needs exponential 
\begin_inset Formula $\mathcal{O}\left(2^{n}\right)$
\end_inset

 memory
\end_layout

\end_inset


\begin_inset Newline newline
\end_inset

 
\end_layout

\begin_layout Itemize
\begin_inset Argument item:2
status open

\begin_layout Plain Layout

2-
\end_layout

\end_inset

List of (monomial, coefficient)-pairs
\begin_inset Flex Visible
status open

\begin_layout Plain Layout
\begin_inset Argument 1
status open

\begin_layout Plain Layout

4-
\end_layout

\end_inset

—
\color magenta
state of art
\end_layout

\end_inset


\begin_inset Newline newline
\end_inset


\begin_inset Flex Visible
status open

\begin_layout Plain Layout

\color none
\begin_inset Argument 1
status open

\begin_layout Plain Layout

3-
\end_layout

\end_inset

efficient multiplication demands extra temporary structures
\end_layout

\end_inset


\begin_inset Newline newline
\end_inset

 
\end_layout

\begin_layout Itemize
\begin_inset Argument item:2
status open

\begin_layout Plain Layout

2-
\end_layout

\end_inset

Tree of (monomial, coefficient)-pairs
\begin_inset Flex Visible
status open

\begin_layout Plain Layout
\begin_inset Argument 1
status open

\begin_layout Plain Layout

4-
\end_layout

\end_inset

—
\color magenta
my choice
\end_layout

\end_inset


\begin_inset Newline newline
\end_inset


\begin_inset Flex Visible
status open

\begin_layout Plain Layout

\color none
\begin_inset Argument 1
status open

\begin_layout Plain Layout

3-
\end_layout

\end_inset

most constant overhead
\end_layout

\end_inset


\begin_inset Newline newline
\end_inset

 
\end_layout

\begin_layout Itemize
\begin_inset Argument item:2
status open

\begin_layout Plain Layout

2-
\end_layout

\end_inset

Hash map from monomials to coefficients
\begin_inset Newline newline
\end_inset


\begin_inset Flex Visible
status open

\begin_layout Plain Layout

\color none
\begin_inset Argument 1
status open

\begin_layout Plain Layout

3-
\end_layout

\end_inset

leading term is expensive to find
\end_layout

\end_inset


\begin_inset Newline newline
\end_inset

 
\end_layout

\begin_layout Itemize
\begin_inset Argument item:2
status open

\begin_layout Plain Layout

2-
\end_layout

\end_inset

Single variate recursive via 
\begin_inset Formula $K\left[\seq X,Y\right]\cong K\left[\seq X\right]\left[Y\right]$
\end_inset


\begin_inset Newline newline
\end_inset


\begin_inset Flex Visible
status open

\begin_layout Plain Layout

\color none
\begin_inset Argument 1
status open

\begin_layout Plain Layout

3-
\end_layout

\end_inset

tricky in typed setting
\end_layout

\end_inset


\end_layout

\end_deeper
\end_inset


\begin_inset ERT
status collapsed

\begin_layout Plain Layout


\backslash
end{frame}
\end_layout

\end_inset


\end_layout

\end_body
\end_document
