Maximum sensitivity to update schedules of elementary cellular automata over periodic configurations

Perrot, Kévin; Montalva-Medel, Marco; de Oliveira, Pedro P. B.; Ruivo, Eurico L. P.

doi:10.1007/s11047-019-09743-9

Maximum sensitivity to update schedules of elementary cellular automata over periodic configurations

Published: 10 July 2019

Volume 19, pages 51–90, (2020)
Cite this article

Download PDF

Natural Computing Aims and scope Submit manuscript

Maximum sensitivity to update schedules of elementary cellular automata over periodic configurations

Download PDF

Kévin Perrot¹,
Marco Montalva-Medel²,
Pedro P. B. de Oliveira³ &
…
Eurico L. P. Ruivo³

187 Accesses
3 Citations
Explore all metrics

Abstract

This work is a thoughtful extension of the ideas sketched in Montalva et al. (AUTOMATA 2017 exploratory papers proceedings, 2017), aiming at classifying elementary cellular automata (ECA) according to their maximal one-step sensitivity to changes in the schedule of cells update. It provides a complete classification of the ECA rule space for all period sizes $n > 9$ and, together with the classification for all period sizes $n \le 9$ presented in Montalva et al. (Chaos Solitons Fractals 113:209–220, 2018), closes this problem and opens further questionings. Most of the 256 ECA rule’s sensitivity is proved or disproved to be maximum thanks to an automatic application of basic methods. We formalize meticulous case disjunctions that lead to the results, and patch failing cases for some rules with simple arguments. This gives new insights on the dynamics of ECA rules depending on the proof method employed, as for the last rules 45 and 105 requiring $({\texttt{0011}})^*$ induction patterns.

Non-maximal Sensitivity to Synchronism in Periodic Elementary Cellular Automata: Exact Asymptotic Measures

The impact of alphabet size on pattern complexity of maxmin- $$\omega$$ cellular automata

Article Open access 14 April 2020

Ebrahim L. Patel

A survey of cellular automata: types, dynamics, non-uniformity and applications

Article 23 July 2018

Kamalika Bhattacharjee, Nazma Naskar, … Sukanta Das

1 Introduction

Cellular automata (CAs) are discrete dynamical systems (both in time and space) where each cell of a lattice is given a state from a finite set. States evolve according to local interaction rules among neighbors. The neighborhood and rule are uniform, they can be described as a set of relative positions and a function giving a new state for a cell from states on that set of relative positions. Even with basic local rules, cellular automata may display very complex global behavior: well-known binary cellular automata rules such as the game of life (Gardner 1970) and rule 110 (Cook 2004) are known to be capable of simulating Turing machines.

Classically, CA cells are updated synchronously at every time step: the state of a cell at time $t+1$ is a function of its neighbors’ at time t (Kari 2005). However, the introduction of variations in the schedule (order) according to which cells are updated has been gaining attention in recent years, unveiling richer behaviors. This has been observed both on the dynamics and problem-solving ability, and regarding the simulation of real-world phenomena; see Fatès (2014) for a comprehensive review. The present work focuses on deterministic evolution, i.e. introduction of variations in a deterministically followed update schedule, and not a stochastic one. In this context a basic question to answer is: given a CA, how much do changes in the schedule of cells update carry changes in its dynamical behavior? We approach this qualitatively by the notion of maximum update schedule sensitivity and the classification that follows.

In the more general framework of automata networks, Aracena et al. (2011, 2009, 2013) gave a relevant notion of equivalence classes of update schedule, with a constructive characterization of the equivalence relation. We base our work on an application of this characterization to elementary cellular automata (ECA), and measure the sensitivity to update schedules as the number of different dynamics obtained over the set of update schedule equivalence classes. Given two non-equivalent update schedules ${\varDelta }\not \equiv {\varDelta }'$, the two obtained dynamics differ if and only if they differ on at least one configuration x, that is if there exists a cell i such that the update of x according to ${\varDelta }$ and ${\varDelta }'$ lead to different states for cell i. This notion of difference in dynamics may be called one-step sensitivity, as we look at the direct successor of a configuration. This is of course a key step towards the more general understanding of k-steps sensitivity for any $k \in {\mathbb {N}}$, and even for the limit behavior $k=\omega$.

This paper considers deterministic update schedules over periodic configurations (of given size n). We believe that the notion of update schedule sensitivity is ground stone to the possibilities to study classical problems in the CA litterature under new perspectives. For instance, in the standard setting of fully synchronous updates, it has been shown that no single CA rule is able to solve the density classification task (de Oliveira 2014). It is still an open question to know whether there exist a solution under another deterministic update schedule (though it is possible in the stochastic setting Fatès 2011). One may agree to the intuition that a CA rule presenting many different dynamics due to distinct update schedules offers more possibilities to tackle the problem.

The paper is organized as follows: in Sect. 2 we define the notion of sensitivity to update schedules on ECA, and in Sect. 3 we present a serie of results in order to classify the whole rule space of ECA for any size $n \ge 9$ according to the sensitivity definition proposed in the above section. A precise table of content for Sect. 3 is provided. It first contains general considerations, such as a count of the number of different update schedules of size n and the introduction of a notation for sequences of updates, second is a study of non-max-sensitive rules, and finally a step by step classification of every ECA. Basic ideas are meticulously formalized and generalized until all remaining rules are proven to be max-sensitive to update schedule changes. Section 3 ends with a summary of the results. Finally, in Sect. 4, we present the paper conclusions and perspectives.

2 Definitions

Cellular automata are discrete (both in space and time) and deterministic dynamical systems. We will consider the family of elementary cellular automata (two states and radius one neighborhood in dimension one) on periodic configurations. Let us introduce the classical definitions where the evolution is considered under the parallel update schedule, and then introduce other update schedules for the purpose of studying the sensitivity to synchronism.

2.1 Cellular automata

Given a dimension d and a finite set of states S, we consider the set of configurations ${{\mathbb {Z}}^d}^S$ which associates a state to each cell of a d-dimensional lattice. For convenience, the state of cell i in the configuration x will also be denoted $x_i$ (instead of x(i)).

A cellular automata dynamics is described by the parallel application of a local rule. The nieghborhood N is a finite tuple of d-dimensional vectors (elements of ${\mathbb {Z}}^d$), and the cellular automata local rule is a total function from $S^N$ to S which gives the new state of a cell according to the states of its neighboors. The rule is then applied in parallel at every lattice position, during discrete time steps.

Definition 1

A cellular automaton (CA) is a 4-tuple (d, S, N, f) with

$d \in {\mathbb {N}}$ the dimension,
$S \subset {\mathbb {N}}$ the finite set of states,
$N \subset {\mathbb {Z}}^d$ the finite tuple of neighbors,
$f:S^N \rightarrow S$ the local rule.

The parallel dynamics F of a CA on the configuration space $S^{{\mathbb {Z}}^d}$ is given by

$$\begin{aligned} F(x)_i=f(x_{i+N[1]},x_{i+N[2]},\ldots ,x_{i+N[k]}) \end{aligned}$$

with $k=|N|$ and N[j] the jth element of the tuple.

2.2 Elementary cellular automata

Elementary cellular automata are the family of cellular automata in dimension one, with Boolean states and von Neumann neighborhood of radius one.

Definition 2

Elementary cellular automata (ECA) are the cellular automata with $d=1$, $S=\{{\texttt{0}},{\texttt{1}}\}$ and $N=(-1,0,+1)$. An ECA will therefore be identified by its local rule f.

The 256 local rules of ECAs may also be described by their Wolfram number (Wolfram 2002) given by

$$\begin{aligned} W(f)=\sum _{(x_1,x_2,x_3)\in \{{\texttt{0}},{\texttt{1}}\}^3 } f(x_1,x_2,x_3)2^{2^2x_1+2^1x_2+2^0x_3}. \end{aligned}$$

2.3 Finite periodic configurations

A one-dimensional ECA configuration x is periodic when there exists a period $n \in {\mathbb {N}}$ such that $x_i = x_{i + n}$ for all $i \in {\mathbb {Z}}$. An ECA evolving from a periodic configuration can be described as elements of $S^n$, and the parallel dynamics F is given by

$$\begin{aligned} F(x)_i=f(x_{i-1 \mod n},x_i,x_{i+1 \mod n}) \text { for all } i \in {\llbracket} 0;n-1 {\rrbracket } \end{aligned}$$

where ${\llbracket} a;b {\rrbracket }\equiv \{i\in {\mathbb {Z}}:\, a\le i\le b\}$, for any integers a and b with $a\le b$.

In the rest of this paper we restrict our study to ECAs on periodic configurations identified with elements of $\{{\texttt{0}},{\texttt{1}}\}^n$, and call n the size of the configuration.

2.4 ECA interaction digraph

It captures the general interactions given by the neighborhood $(-1,0,+1)$. For an illustration see Fig. 1 (left).

Definition 3

The ECA interaction digraph of size n is $G_{n}=(V_{n},A_{n})$ such that $V_{n}={\llbracket} 0;n-1 {\rrbracket }$ is the set of cells and

$$\begin{aligned} A_{n}=\bigcup _{i \in {\llbracket} 0;n-1 {\rrbracket }} \{ (i,i-1 \mod n), (i,i), (i,i+1 \mod n) \}. \end{aligned}$$

Note that it does not depend on the local rule. In Sect. 2.7 we will motivate the removal of loops in this ECA interaction digraph, regarding synchronism sensitivity.

2.5 Update schedule

In the previous subsections we defined ECAs under the standard parallel update schedule. Let us now introduce some variations on the order according to which cells are updated during one time step.

Definition 4

A fair and periodicupdate schedule of period n for ECAs (update schedule for short) is simply defined as an ordered partition of ${\llbracket} 0;n-1 {\rrbracket }$, denoted ${\varDelta }=({\varDelta }_1,\ldots ,{\varDelta }_p)$.

The image of a configuration $x \in \{{\texttt{0}},{\texttt{1}}\}^n$ under update schedule ${\varDelta }=({\varDelta }_1,\ldots ,{\varDelta }_p)$ is then defined recursively, as

$$\begin{aligned} F_{({\varDelta }_j,{\varDelta }_{j+1},\ldots ,{\varDelta }_p)}(x)=F_{({\varDelta }_{j+1},\ldots , {\varDelta }_p)}(F_{{\varDelta }_j}(x)) \end{aligned}$$

and $F_{(\,)}(x)=x$, with a substep defined as

$$\begin{aligned}&\forall i \in {\llbracket} 0;n-1 {\rrbracket }, \\&F_{{\varDelta }_j}(x)_i = \left\{ \begin{array}{ll} f(x_{i-1} \mod n, x_i, x_{i+1} \mod n) &\quad \text {if} \, i \in {\varDelta }_j \\ x_i &\quad \text {otherwise} \end{array} \right. \end{aligned}$$

The image is also denoted $F_{\varDelta }(x)$ for simplicity. In this context, the parallel update schedule is ${\varDelta }^\text {par}=({\llbracket} 0;n-1 {\rrbracket })$, and an ordered partition made of n singletons (which can also be seen as a permutation of ${\llbracket} 0;n-1 {\rrbracket }$) is a sequential update schedule.

2.6 Transition digraph and dynamics

Definition 5

Given an ECA rule f of size n and an update schedule ${\varDelta }$, we define the transition digraph${\mathcal {G}}_{f,n,{\varDelta }}=({\mathcal {V}}_{n},{\mathcal {A}}_{n})$ as the digraph where ${\mathcal {V}}_{n}=\{{\texttt{0}},{\texttt{1}}\}^n$ is the set of configurations, and there is an arc $(x,x') \in {\mathcal {A}}_{n}$ if and only if $F_{\varDelta }(x)=x'$.

The digraph ${\mathcal {G}}_{f,n,{\varDelta }}$ is thought as an object catching the dynamic of rule f under ${\varDelta }$.

Definition 6

We define the fair periodic dynamics (dynamics for short) of a rule f as

$$\begin{aligned} {\mathcal {D}}(f,n)=\{ {\mathcal {G}}_{f,n,{\varDelta }} \mid {\varDelta }\, \text {fair periodic update schedule} \}. \end{aligned}$$

The dynamics is the set of every dynamic (as captured by the transition graph) that we can obtain by varying the update schedule, for an ECA rule f of size n.

2.7 Update digraph and equivalent update schedules

There are natural equivalence classes of fair periodic update schedules for ECAs of a given size n. In fact, it only matters to know the order of update among neighbors automata. This subsection is inspired by the developments introduced in Aracena et al. (2009) on the notion of update digraphs build upon the interaction digraph of automata networks, and applies them to the ECA interaction digraph. In Aracena et al. (2009) a fair periodic update schedule ${\varDelta }=({\varDelta }_1,\ldots ,{\varDelta }_p)$ is defined as a function such as $t_{\varDelta }: {\llbracket} 0;n-1 {\rrbracket } \rightarrow {\llbracket} 1;p {\rrbracket }$ with $t_{\varDelta }(i)=j$ if and only if $i \in {\varDelta }_j$, i.e. $t_{\varDelta }(i)=\arg _{j \in {\llbracket} 1;p {\rrbracket }}(i \in {\varDelta }_j)$ tells the time step j at which cell i is updated (note that $t_{\varDelta }$ is well defined since $({\varDelta }_1,\ldots ,{\varDelta }_p)$ is a partition of ${\llbracket} 0;n-1 {\rrbracket }$). In the rest of the paper we will use both ${\varDelta }$ and $t_{\varDelta }$.

Given an update schedule ${\varDelta }$, we define the label function$lab_{n,{\varDelta }} : \hat{A_{n}} \rightarrow \{ \oplus ,\ominus \}$, with $\hat{A_{n}}$ the loopless subset of $A_{n}$, i.e. $\hat{A_{n}}=\{ (i,i') \in A_{n} \mid i \ne i' \}$, as follows:

$$\begin{aligned} \forall (i,i') \in \hat{A_{n}},\quad lab_{n,{\varDelta }}((i,i'))= \left\{ \begin{array}{ll} \oplus &{} \text {if } \, t_{\varDelta }(i) \ge t_{\varDelta }(i')\\ \ominus &{} \text {if } \, t_{\varDelta }(i) < t_{\varDelta }(i'). \end{array}\right. \end{aligned}$$

A $\ominus$ label on the arc from i to $i'$ means that i is updated strictly prior to $i'$ during every time step. In other words, during the computation of $F_{\varDelta }(x)$, at the substep when we apply the local function at position $i'$, the state of i may not be $x_i$ anymore.

Definition 7

The update digraph of ${\varDelta }$ is the labeled digraph $G_{n,{\varDelta }}=(V_{n},\hat{A_{n}},lab_{n,{\varDelta }})$.

Definition 8

We denote by ${\mathcal {U}}(n)$ the set of update digraphs for ECAs of size n:

$$\begin{aligned} {\mathcal {U}}(n)=\{ G_{n,{\varDelta }} \mid {\varDelta }\, \text {fair periodic update schedule} \}. \end{aligned}$$

Let us now remark that loops would always be labeled $\oplus$, hence they would have add no information to update digraphs. Also note that some label functions on ${\hat{A}}$ do not correspond to any update schedule ( for example if two arcs $(s,s')$ and $(s',s)$ are both labeled $\ominus$), and that different update schedules may lead to the same label function. We say that a label function $lab_n:\hat{A_{n}} \rightarrow \{\ominus ,\oplus \}$ is valid when there is an update schedule ${\varDelta }$ such that $lab_n=lab_{{\varDelta },n}$. Aracena et al. gave an exact characterization of the valid label functions.

Theorem 1

(Aracena et al. 2011) A label function $lab_n: \hat{A_{n}} \rightarrow \{ \oplus ,\ominus \}$ is valid if and only if there is no cycle $(i_0,i_1,\ldots ,i_k)$, with $i_0=i_k$, of length $k>0$ such that:

for all $1 \le j < k$, $((i_j,i_{j+1}) \in \hat{A_{n}} \wedge lab((i_j,i_{j+1}))=\oplus )$
or $((i_{j+1},i_j) \in \hat{A_{n}} \wedge lab((i_{j+1},i_j))=\ominus )$,
exists $1 \le j < k, lab((i_{j+1},i_j))=\ominus$.

In words, the multi-digraph where the labeling is unchanged but the orientation of negative arcs is reversed, does not contain a cycle with at least one negative arc (forbidden cycle).

Update digraphs can be seen as equivalence classes of update schedules (${\varDelta }\equiv {\varDelta }'$ if and only if $lab_{n,{\varDelta }}=lab_{n,{\varDelta }'}$): those always giving the same transition digraph (dynamic), whatever be the ECA local rule.

Theorem 2

(Aracena et al. 2009) For all f, n, ${\varDelta }$, ${\varDelta }'$, if $lab_{n,{\varDelta }}=lab_{n,{\varDelta }'}$ then ${\mathcal {G}}_{f,n,{\varDelta }}={\mathcal {G}}_{f,n,{\varDelta }'}$.

Thus $|{\mathcal {U}}(n)|$ is the number of non-equivalent update schedules on the ECA interaction digraph. For an illustration see Fig. 1 (right).

2.8 Update schedule sensitivity

The number $|{\mathcal {U}}(n)|$ can be thought as an upper bound on the number of different dynamics of an ECA of size n (note that it does not depend on the rule). In contrast, $|{\mathcal {D}}(f,n)|$ depends also on the local rule, and is the actual number of different dynamics of ECA f.

Definition 9

We are interested in the sensitivity to synchronism of ECAs, as measured by the quantity

$$\begin{aligned} sensitivity(f,n)=\frac{|{\mathcal {D}}(f,n)|}{|{\mathcal {U}}(n)|}. \end{aligned}$$

The sensitivity to synchronism is the proportion of different dynamics relative to the number of equivalent classes of fair periodic update schedules, for a given size n.

We obviously have $\frac{1}{|{\mathcal {U}}(n)|} \le sensitivity(f,n) \le 1$, and an ECA is as much sensible to synchronism as it has different dynamics as the update schedule varies. The extreme cases are, an ECA f with $sensitivity(f,n)=\frac{1}{|{\mathcal {U}}(n)|}$ has always the same dynamic ${\mathcal {G}}_{f,n,{\varDelta }}$ for all update schedule ${\varDelta }$, and an ECA f with $sensitivity(n,f)=1$ has a different dynamic for each non-equivalent update schedule ${\varDelta }$ (for all ${\varDelta }\not \equiv {\varDelta }'$ it has ${\mathcal {G}}_{f,n,{\varDelta }} \ne {\mathcal {G}}_{f,n,{\varDelta }'}$).

Definition 10

An ECA f such that

$$\begin{aligned} \exists n_0 \in {\mathbb {N}}: \forall n \ge n_0 : sensitivity(f,n)=1 \end{aligned}$$

is called (ultimately) max-sensitive to synchronism.

Note that a rule f is max-sensitive for a given size n if and only if

$$\begin{aligned} \forall {\varDelta }\not \equiv {\varDelta }' : \exists x \in \{{\texttt{0}},{\texttt{1}}\}^n : \exists i \in {\llbracket} 0;n-1 {\rrbracket } : F_{\varDelta }(x)_i \ne F_{{\varDelta }'}(x)_i. \end{aligned}$$

(1)

2.9 Symmetries among ECAs

Instead of studying the whole ECA rule space, one may consider only a representative of each dynamical equivalence class. Two rules are dynamically equivalent if they have the same dynamics up to conjugation (swapping ${\texttt{0}}$s and ${\texttt{1}}$s), reflection (swapping left and right) or conjugated-reflection (reflection and conjugation). More formally, two local ECA rules f and g are dynamically equivalent if one of the following holds:

$$\begin{aligned} \begin{array}{lrl} f(a,b,c)=1-g(1-a,1-b,1-c) &{} \quad \hbox {for all} \, (a,b,c)\in \{{\texttt{0}},{\texttt{1}}\}^3 &{} \quad \hbox {(conjugation)}\\ f(a,b,c)=g(c,b,a) &{} \quad \hbox {for all} \, (a,b,c)\in \{{\texttt{0}},{\texttt{1}}\}^3 &{} \quad \hbox {(reflection)} \\ f(a,b,c)=1-g(1-c,1-b,1-a) &{} \quad \hbox {for all} \, (a,b,c)\in \{{\texttt{0}},{\texttt{1}}\}^3 &{} \quad \hbox {(reflected-conjugation)} \end{array} \end{aligned}$$

The ECA rule space is partitioned into 88 classes of dynamically equivalent rules:

$$\begin{aligned} 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 18, 19, 22, 23, 24, 25, 26, 27, 28, 29, 30, 32, 33, 34, 35, 36, 37, 38, 40, 41, 42, 43, 44, 45, 46, 50, 51, 54, 56, 57, 58, 60, 62, 72, 73, 74, 76, 77, 78, 90, 94, 104, 105, 106, 108, 110, 122, 126, 128, 130, 132, 134, 136, 138, 140, 142, 146, 150, 152, 154, 156, 160, 162, 164, 168, 170, 172, 178, 184, 200, 204, 232. \end{aligned}$$

An ECA, its conjugation, reflection and conjugated-reflection, all have the same interaction digraph, and their respective transition digraphs for a given update schedule are isomorphic, hence they are equally sensitive to synchronism.

2.10 Previous results on ECAs

In Montalva et al. (2018) we gave a classification of the ECA rule space according to their maximal sensitivity to synchronism for n equals 3 to 9, and noticed that for n from 7 to 9 the classification is stable. The present work completes the characterization for all $n \ge 9$. It starts as a continuation of the idea sketched in Montalva et al. (2017), and eventually greatly extends them.

3 Characterization of max-sensitive ECAs

As mentioned in the previous section, in the rest of the paper we concentrate on the sensitivity to synchronism of

ECAs designated by their Wolfram rule number,
up to conjugation, reflection and conjugated-reflection,
on periodic configurations of size $n \ge 3$
under fair periodic update schedules.

This will only be fully recalled in the sum-up Sect. 3.10. We may omit to mention moduli n for clarity, and will also assume that ECA interaction digraphs are loopless.

3.1 Counting update schedules for ECAs

We can count the number of equivalence classes of update schedules for ECAs, that is the number of valid labelings of the ECA interaction digraph presented on Fig. 1.

Lemma 1

For any ECA of size n, we have $|{\mathcal {U}}(n)| = 3^n-2^{n+1}+2$.

Note that this result is also present in Montalva et al. (2017) with a different proof.

Proof

There are at most $4^n$ labellings (2n arcs, see Fig. 1), out of which we will remove the invalid ones. First remark that we can only have forbidden cycles of length 2 or n. Let $A_2$ denote the set of labellings with at least one forbidden cycle of length 2, and $A_{2,i}$ denote the set of labellings with exactly i forbidden cycles of length 2. Similarly, let $A_n$ denote the set of labellings with at least one forbidden cycle of length n, $A_{n,c,j}$ denote the set of labellings where a clockwise forbidden cycle of length n has a maximum of j negative arcs, and $A_{n,{\bar{c}},j'}$ denote the set of labellings where a counterclockwise forbidden cycle of length n has a maximum of $j'$ negative arcs. There are $4^n-|A_2 \cup A_n|$ valid labellings. With $\uplus$ the disjoint union, counting gives:

$$\begin{aligned} |A_2|= & {} \left| \biguplus \limits _{i=1}^n A_{2,i}\right| = \sum \limits _{i=1}^n {n \atopwithdelims ()i} 3^{n-i} = 4^n-3^n \\ |A_n|= & {} \left| \biguplus \limits _{j=1}^n A_{n,c,j} \cup \biguplus \limits _{j'=1}^n A_{n,{\bar{c}},j'} \right| \\= & {} 2 \sum \limits _{j=1}^n {n \atopwithdelims ()j} 2^j - \sum \limits _{j=1}^n \sum \limits _{j'=1}^n {n \atopwithdelims ()j} (\text {iff}\,j=j') \\= & {} 2(3^n-1)-(2^n-1) \\ |A_2 \cap A_n|= & {} \left| \biguplus \limits _{i=1}^n \left( A_{2,i} \cap \left( \biguplus \limits _{j=1}^n A_{n,c,j} \cup \biguplus \limits _{j'=1}^n A_{n,{\bar{c}},j'} \right) \right) \right| \\= & {} \sum \limits _{i=1}^n \left( 2 \left| A_{2,i} \cap \biguplus \limits _{j=1}^n A_{n,c,j} \right| \right. \\&\quad \qquad \left. - \left| A_{2,i} \cap \biguplus \limits _{j=1}^n A_{n,c,j} \cap \biguplus \limits _{j'=1}^n A_{n,{\bar{c}},j'} \right| \right) \\= & {} \sum \limits _{i=1}^n \left( 2 \sum \limits _{j=1}^n {n \atopwithdelims ()i}{n-i \atopwithdelims ()j-i} - {n \atopwithdelims ()i} \right) \\= & {} 2 (3^n-2^n) - (2^n-1) \end{aligned}$$

so that $|A_2 \cup A_n|=|A_2|+|A_n|-|A_2 \cap A_n|=4^n-3^n+2^{n+1}-2$. $\square$

Lemma 1 counts the number of equivalence classes of updates schedules for ECAs. This number equals the number of dynamics for (and only for) max-sensitive ECAs, it is at the bases of numerical simulations conducted in Montalva et al. (2018) for small values of n

3.2 Rules with non-effective interactions (10 rules)

The ECA interaction digraph is the same for all ECA rule, and we compute the number of equivalence classes of update schedules from it. However one can easily notice that for some rules such as rule 0, arcs of the ECA interaction digraph do not correspond to “effective interactions”. This is a classical notion in the framework of automata networks, where the interaction digraph of rule 0 would have no arc (Noual 2012). Changing the order of updates of cells not effectively linked ($\oplus$ or $\ominus$) has no consequence on the dynamic, therefore rule 0 cannot admit $3^n-2^{n+1}+2$ different dynamics, and is not max-sensitive. In this subsection we formalize this intuitive observation.

Given a configuration $x \in \{{\texttt{0}},{\texttt{1}}\}^n$ and a cell $i \in {\llbracket} 0;n-1 {\rrbracket }$, we denote $\overline{x}^{i}$ the configuration where only the state of cell i is flipped, i.e. $\overline{x}^{i}_i=1-x_i$ and $\overline{x}^{i}_{i'}=x_{i'}$ for $i' \ne i$.

Definition 11

An interaction $(i,i')$ is f-effective if and only if there exists a configuration x such that $f(\overline{x}^{i})_{i'} \ne f(x)_{i'}$.

The idea is that cell i effectively influences cell $i'$ when there is at least one case (a configuration x) such that the state of cell i may change the state of cell $i'$.

Given an ECA rule, some arcs of the ECA interaction digraph (Fig. 1) may be non-effective. In this case the ECA cannot be max-sensitive, as stated in the following lemma.

Lemma 2

If there exists a non-f-effective arc $(i,i') \in A_{n}$ then rule f is not max-sensitive.

Note that Lemma 2 also directly follows from Proposition 5 of Aracena et al. (2013).

Proof

It is straightforward to notice that in this case for any size n there exist two non-equivalent update schedules giving the same dynamics, hence contradicting Formula (1). Without loss of generality let us suppose that $i'=i+1$ and $i<n-1$. Consider ${\varDelta }$ an update schedule such that $lab_{n,{\varDelta }}(a)=\oplus$ for all arc a, and ${\varDelta }'$ such that $lab_{n,{\varDelta }'}$ equals $lab_{n,{\varDelta }}$ everywhere but on arc $(i,i')$, for which $lab_{n,{\varDelta }'}((i,i'))=\ominus$. For simplicity we take ${\varDelta }=({\llbracket} 0;n-1 {\rrbracket })$ and ${\varDelta }'=({\llbracket} 0;i {\rrbracket },{\llbracket} i+1;n-1 {\rrbracket })$. Then for any configuration x we have:

1.
$\forall j \ne i+1: \quad F_{{\varDelta }'}(x)_j = f(x_{j-1},x_j,x_{j+1}) = F_{{\varDelta }}(x)_j$,
2.
$F_{{\varDelta }'}(x)_{i+1} = f(f(x_{i-1},x_{i},x_{i+1}),x_{i+1},x_{i+2}) = f(x_{i},x_{i+1},x_{i+2}) = F_{{\varDelta }}(x)_{i+1}$ where the central equality follows from the fact that arc $(i,i+1)$ is non-effective.

That is, the negation of Formula (1) holds. $\square$

Indeed, A simple exhaustive search in constant time for each rule gives the first classification.

Theorem 3

Rules 0, 3, 12, 15, 34, 51, 60, 136, 170, 204 are not max-sensitive for any n.

Proof

By application of Lemma 2 according to the following observations:

for all i the arc $(i+1,i)$ is non-r-effective, $r\in \{3,12,15,60\}$,
for all i the arc $(i,i+1)$ is non-r-effective, $r\in \{34,136,170\}$,
for all i the arcs $(i+1,i)$ and $(i-1,i)$ are non-r-effective, $r\in \{51,204\}$.

$\square$

There are 78 ECA rules with 2n effective interactions (all arcs of the ECA interaction digraph): 1, 2, 4, 5, 6, 7, 8, 9, 10, 11, 13, 14, 18, 19, 22, 23, 24, 25, 26, 27, 28, 29, 30, 32, 33, 35, 36, 37, 38, 40, 41, 42, 43, 44, 45, 46, 50, 54, 56, 57, 58, 62, 72, 73, 74, 76, 77, 78, 90, 94, 104, 105, 106, 108, 110, 122, 126, 128, 130, 132, 134, 138, 140, 142, 146, 150, 152, 154, 156, 160, 162, 164, 168, 172, 178, 184, 200, 232.

3.3 Properties of non-equivalent update schedules

In this case, for any two non-equivalent update schedules ${\varDelta }\not \equiv {\varDelta }'$, we have by definition that

$$\begin{aligned} \exists i_0:&\quad lab_{n,{\varDelta }}((i_0,i_0+1))=\oplus \wedge lab_{n,{\varDelta }'}((i_0,i_0+1))=\ominus \\&\text {or } lab_{n,{\varDelta }}((i_0+1,i_0))=\oplus \wedge lab_{n,{\varDelta }'}((i_0+1,i_0))=\ominus \end{aligned}$$

Let us consider in more details some properties of the second case,

$$\begin{aligned} \exists i_0: lab_{n,{\varDelta }}((i_0+1,i_0))=\oplus \wedge lab_{n,{\varDelta }'}((i_0+1,i_0))=\ominus \end{aligned}$$

(2)

(the first case is symmetric). Please keep in mind that when we want to prove a formula $\forall {\varDelta }\not \equiv {\varDelta }'$ (such as max-sensitivity) then we have to consider the two symmetric cases, and when we want to prove that $\exists {\varDelta }\not \equiv {\varDelta }'$ for a formula (such as non-max-sensitivity) then we only have to exhibit such update schedules in one of the two cases. This will be recalled in the statements of Lemmas and Theorems when we say “a rule and/or its reflection”.

Definition 12

We say that $i_0$ is $\ell$-right-bounded in ${\varDelta }$ when

$$\begin{aligned}&lab_{n,{\varDelta }}((i_0+1,i_0)) \\&\quad =\ominus \wedge \dots \wedge lab_{n,{\varDelta }}((i_0+\ell ,i_0+\ell -1))=\ominus \\&lab_{n,{\varDelta }}((i_0+\ell +1,i_0+\ell )) =\oplus \end{aligned}$$

and symmetrically $i_0$ is $(-m)$-left-bounded in ${\varDelta }$ when

$$\begin{aligned}&lab_{n,{\varDelta }}((i_0-m-1,i_0-m)) =\oplus \\&lab_{n,{\varDelta }}((i_0-m,i_0-m+1)) \\&\quad =\ominus \wedge \dots \wedge lab_{n,{\varDelta }}((i_0-1,i_0))=\ominus . \end{aligned}$$

We also say that $i_0$ is $(-m,\ell )$-bounded in ${\varDelta }$.

Property 1

For all ${\varDelta }\not \equiv {\varDelta }'$: there exist $i_0, m, m', \ell ':$

$$\begin{aligned} \begin{aligned} (0 \le m< n)&\wedge (0 \le m'< n) \wedge (1 \le \ell ' < n) \\&\wedge (\ell '+m' \le n) \wedge (\ell '+m \le n) \end{aligned} \end{aligned}$$

and such that $i_0$ is $(-m,0)$-bounded in ${\varDelta }$, and $i_0$ is $(-m',\ell ')$-bounded in ${\varDelta }'$.

Graphically, for ${\varDelta }$ (above) and ${\varDelta }'$ (below), Property 1 states

Proof

If one of the three first inequalities is not fulfilled then there is a forbidden cycle of length n in ${\varDelta }$ or ${\varDelta }'$ (with n$\ominus$ labels). If the penultimate inequality ($\ell '+m' < n$) is not fulfilled then there is a forbidden cycle of length 2 in ${\varDelta }'$ (where the left and right boundings of $i_0$ overlap).

For the last inequality, suppose it does not hold, i.e. $\ell '+m > n$, it means that the left bounding of $i_0$ in ${\varDelta }$ strictly overlaps the right bounding of $i_0$ in ${\varDelta }'$. We can deduce that the update digraphs of ${\varDelta }$ and ${\varDelta }'$ differ on the label of the arc $(i_0-m+1,i_0-m)$: we have $lab_{n,{\varDelta }}((i_0-m+1,i_0-m))=\oplus$ (because $lab_{n,{\varDelta }}((i_0-m,i_0-m+1))=\ominus$) and $lab_{n,{\varDelta }'}((i_0-m+1,i_0-m))=\ominus$ (because $\ell '+m > n$ so $\ell '+m-n > 0$). As a consequence there exist $i_0-m,0,0,\ell '+m-n$ verifying the property: $i_0-m$ is (0, 0)-bounded in ${\varDelta }'$ and $(0,\ell '+m-n)$-bounded in ${\varDelta }'$. $\square$

Property 1 will be useful to prove max-sensitivity using the $i_0,m,m',\ell '$ given for each pair of non-equivalent update schedule. The next property will be useful to prove non-max-sensitivity using the ${\varDelta },{\varDelta }'$ given for each $i_0,m,\ell$.

Property 2

For all $i_0, m,\ell : (0 \le m< n-1) \wedge (1 \le \ell< n-1) \wedge (1 \le \ell +m <n)$, there exist ${\varDelta }\not \equiv {\varDelta }'$ such that $i_0$ is $(-m,0)$-bounded in ${\varDelta }$, and $i_0$ is $(-m,\ell )$-bounded in ${\varDelta }'$. Moreover, we can choose ${\varDelta },{\varDelta }'$ such that their update digraphs differ only on the labelling of arc $(i_0+1,i_0)$ ($lab_{n,{\varDelta }}((i_0+1,i_0))=\oplus$ and $lab_{n,{\varDelta }'}((i_0+1,i_0))=\ominus$).

Proof

If one simply chooses all other labels (not yet fixed by boundings or the last condition) to be $\oplus$, then both update digraphs are valid. $\square$

Also note that for each arc $(i,i+1)$ labeled $\ominus$, the arc $(i+1,i)$ is necessarily labeled $\oplus$, otherwise there is a forbidden cycle of length 2.

3.4 A useful notation

To prove or disprove the equality of $F_{{\varDelta }}(x)$ and $F_{{\varDelta }'}(x)$, we will often compute the images on one cell $i_0$ of configuration x updated under two update schedules ${\varDelta },{\varDelta }'$. If $i_0$ is $(-m,\ell )$-bounded in ${\varDelta }$ then the value of $F_{{\varDelta }}(x)_{i_0}$ depends only on

$$\begin{aligned} (x_{i_0-m-1},x_{i_0-m},\ldots ,x_{i_0},\ldots ,x_{i_0+\ell },x_{i_0+\ell +1}), \end{aligned}$$

as will be proved in Lemma 3 by using the following notation.

For $m \ge 0, \ell \ge 0$,

$$\begin{aligned} f^{{-m}\rightarrow {i_0}\leftarrow {\ell }}((x_{i_0-m-1},x_{i_0-m},\ldots , x_{i_0},\ldots ,x_{i_0+\ell },x_{i_0+\ell +1})) \end{aligned}$$

is defined as

$$\begin{aligned}&f\left( \;f^{{-m+1}\rightarrow {i_0-1}}((x_{i_0-m-1},x_{i_0-m}, \dots ,x_{i_0-1},x_{i_0}))\;,\;x_{i_0}\;, \right. \\&\qquad \left. f^{{i_0+1}\leftarrow {\ell -1}} ((x_{i_0},x_{i_0+1},\ldots ,x_{i_0+\ell },x_{i_0+\ell +1}))\;\right) \end{aligned}$$

themselves defined inductively as

$$\begin{aligned}&f^{{-b}\rightarrow {a}}((x_{a-b-1},\ldots ,x_{a+1})) \\&\quad =f^{{-b+1}\rightarrow {a}}((f(x_{a-b-1}, x_{a-b},x_{a-b+1}),x_{a-b+1},\ldots ,x_{a+1})) \\&\qquad \hbox {for} \, a \le 0\\&f^{{a}\leftarrow {b}}((x_{a-1},\ldots ,x_{a+b+1})) \\&\quad =f^{{a}\leftarrow {b-1}}((x_{a-1},\ldots , x_{a+b-1},f(x_{a+b-1},x_{a+b},x_{a+b+1}))) \\&\qquad \hbox {for} \, a \ge 0 \end{aligned}$$

with base cases

$$\begin{aligned} f^{{1}\rightarrow {a}}((x_a,x_{a+1}))=x_a \, \hbox {and} \, f^{{a}\leftarrow {-1}}((x_{a-1},x_a))=x_a \end{aligned}$$

corresponding in particular to

$$\begin{aligned}&f^{X}((x_{a-1},x_a,x_{a+1}))=f(x_{a-1},x_a,x_{a+1}) \\&\quad \hbox {for} \, X \in \{{0}\rightarrow {a}\leftarrow {0},{0}\rightarrow {a},{a}\leftarrow {0}\}. \end{aligned}$$

This notation corresponds intuitively to an update schedule of the form

$$\begin{aligned} (\dots ,\{i_0-3,i_0+3\},\{i_0-2,i_0+2\},\{i_0-1,i_0+1\},\{i_0\}). \end{aligned}$$

Lemma 3

If $i_0$ is $(-m,\ell )$-bounded in ${\varDelta }$ then for $x=(x_0,\ldots ,x_n) \in \{{\texttt{0}},{\texttt{1}}\}^n$ we have

$$\begin{aligned} F_{{\varDelta }}(x)_{i_0}= & {} f^{{-m}\rightarrow {i_0}\leftarrow {\ell }} \\&((x_{i_0-m-1}, x_{i_0-m},\ldots ,x_{i_0},\ldots ,x_{i_0+\ell },x_{i_0+\ell +1})). \end{aligned}$$

Proof

Let ${\varDelta }=({\varDelta }_1,\ldots ,{\varDelta }_p)$. Since $i_0$ is $(-m,\ell )$-bounded in ${\varDelta }$, we have two sequences of substeps $j_{-m}<j_{-m+1}<\dots<j_{-1}<j_0$ and $j_0>j_1>\dots>j_{\ell -1}>j_{\ell }$ such that for all i between $-m$ and $\ell$ the cell $i_0+i$ is updated during substep $j_i$, that is $i_0+i \in {\varDelta }_{j_i}$.

It just remains to unfold the notation on both sides. Let us present the left side, the right side being symmetric. By induction on m we can get

$$\begin{aligned} f^{{-m+1}\rightarrow {i_0-1}}((x_{i_0-m-1},\ldots ,x_{i_0}))=F_{{\varGamma }}(x)_{i_0-1} \end{aligned}$$

with ${\varGamma }=({\varDelta }_1,\ldots ,{\varDelta }_{j_{-1}})$ and so even ${\varGamma }=({\varDelta }_1,\ldots ,{\varDelta }_{j_0-1})$, from the base case

$$\begin{aligned}&f^{{-m+1}\rightarrow {i_0-1}}((x_{i_0-m-1},\ldots ,x_{i_0})) \\&\quad = f^{{-m+2}\rightarrow {i_0-1}}((f(x_{i_0-m-1},x_{i_0-m},x_{i_0-m+1}), x_{i_0-m+1},\ldots ,x_{i_0}))\\&\quad = f^{{-m+2}\rightarrow {i_0-1}}((F_{{\varGamma }}(x)_{i_0-m}, F_{{\varGamma }}(x)_{i_0-m+1},\ldots ,F_{{\varGamma }}(x)_{i_0})) \end{aligned}$$

with ${\varGamma }=({\varDelta }_1,\ldots ,{\varDelta }_{j_{-m}})$, and induction for $m' < m$ as

$$\begin{aligned}&f^{{-m'+1}\rightarrow {i_0-1}}((F_{{\varGamma }}(x)_{i_0-m'-1},\ldots , F_{{\varGamma }}(x)_{i_0}))\\&\quad = f^{{-m'+2}\rightarrow {i_0-1}} \\&\qquad ((f(F_{{\varGamma }}(x)_{i_0-m'-1}, F_{{\varGamma }}(x)_{i_0-m'},F_{{\varGamma }}(x)_{i_0-m'+1}), \\&\qquad \quad F_{{\varGamma }}(x)_{i_0-m'+1},\ldots ,F_{{\varGamma }}(x)_{i_0}))\\&\quad = f^{{-m'+2}\rightarrow {i_0-1}} \\&\qquad ((F_{{\varGamma }'}(x)_{i_0-m'}, F_{{\varGamma }'}(x)_{i_0-m'+1},\ldots ,F_{{\varGamma }'}(x)_{i_0})) \end{aligned}$$

with ${\varGamma }=({\varDelta }_1,\ldots ,{\varDelta }_{j_{-m'+1}})$ and ${\varGamma }'=({\varDelta }_1,\ldots ,{\varDelta }_{j_{-m'}})$. The proof is finished by combining both sides and applying substep ${\varDelta }_{j_0}$ as follows,

$$\begin{aligned}&f^{{-m}\rightarrow {i_0}\leftarrow {\ell }}((x_{i_0-m-1},\ldots ,x_{i_0},\ldots ,x_{i_0+\ell +1})) \\&\quad = f(F_{{\varGamma }}(x)_{i_0-1},F_{{\varGamma }}(x)_{i_0},F_{{\varGamma }}(x)_{i_0+1})\\&\quad = F_{{\varGamma }'}(x)_{i_0} \end{aligned}$$

with ${\varGamma }=({\varDelta }_1,\ldots ,{\varDelta }_{j_0-1})$ and ${\varGamma }'=({\varDelta }_1,\ldots ,{\varDelta }_{j_0-1},{\varDelta }_{j_0})$ so even ${\varGamma }'={\varDelta }$. $\square$

3.5 Finite counter-example to max-sensitivity (6 rules)

According to Formula (1), given a rule if there exist two update schedules ${\varDelta }\not \equiv {\varDelta }'$ having identical dynamic (i.e. identical transition digraph: for all configuration x we have $F_{{\varDelta }}(x)=F_{{\varDelta }'}(x)$), then the rule is not max-sensitive. This is our strategy in this section, using two update schedules given by Property 2.

Lemma 4

Given a rule f or its reflection, if there exist $m \ge 0, \ell \ge 1$: $\forall (x_{-m-1},\ldots ,x_0,\ldots ,x_{\ell +1}) \in \{{\texttt{0}},{\texttt{1}}\}^{m+\ell +3}$ we have

$$\begin{aligned}&f^{{-m}\rightarrow {0}\leftarrow {0}}((x_{-m-1},x_{-m},\ldots ,x_0,x_1)) \\&\quad = f^{{-m}\rightarrow {0}\leftarrow {\ell }}((x_{-m-1},x_{-m},\ldots ,x_0, \dots ,x_{\ell },y_{\ell +1})) \end{aligned}$$

then rule f is not max-sensitive for any $n \ge m+\ell$.

Proof

Let ${\varDelta },{\varDelta }'$ be given by Property 2 (with all other labels $\oplus$) for cell 0 and the $m,\ell$ existing above, i.e. ${\varDelta }$ and ${\varDelta }'$ differ only in the labeling of arc (1, 0). Then for all $y \in \{{\texttt{0}},{\texttt{1}}\}^n$ we will prove that $F_{{\varDelta }}(y)_i=F_{{\varDelta }'}(y)_i$ for all i.

For all $i \ne 0$ we directly have that i is (a, b)-bounded with the same a and b in both ${\varDelta }$ and ${\varDelta }'$. As a consequence of Lemma 3, for all $i \ne 0$ we have $F_{{\varDelta }}(y)_{i}=F_{{\varDelta }'}(y)_{i}$. We have that 0 is (m, 0)-bounded in ${\varDelta }$, and $(m,\ell )$-bounded in ${\varDelta }'$, so Lemma 3 gives

$$\begin{aligned} F_{{\varDelta }}(y)_{0}&= f^{{-m}\rightarrow {0}\leftarrow {0}}((y_{-m-1},y_{-m},\ldots ,y_0,y_1))\\&= f^{{-m}\rightarrow {0}\leftarrow {\ell }}((y_{-m-1},y_{-m},\ldots ,y_0,\ldots , y_{\ell },y_{\ell +1})) \\&= F_{{\varDelta }'}(y)_{0} \end{aligned}$$

where the middle equality comes from our hypothesis. We can conclude that ${\varDelta },{\varDelta }'$ witness non-max-sensitivity according to Formula (1), and such ${\varDelta },{\varDelta }'$ must be defined on a state set of size $n \ge m+\ell$ to prevent forbidden cycles of length 2. $\square$

Note that the hypothesis of Lemma 4 takes a time $O(m \ell \, 2^{m+\ell })$ to check, for a countably infinite number of m and $\ell$. Some unintensive computer tests give the next theorem.

Theorem 4

Rules 8, 28, 32, 44, 140, 200 are not max-sensitive for any n.

Proof

The hypothesis of Lemma 4 have been tested for all pair of $0 \le m \le 5$ and $1 \le \ell \le 5$, and for the two symmetric cases of Formula (2) (equivalently, the hypothesis of Lemma 4 have been tested for a rule and its reflection). Lemma 4 can be applied as follows.

Rule 64 (reflection of 8) for $m= 1$ and $\ell = 1$.
Rule 28 (reflection of 70) for $m= 0$ and $\ell = 1$.
Rule 32 (reflection of 32) for $m= 1$ and $\ell = 1$.
Rule 44 (reflection of 100) for $m= 0$ and $\ell = 1$.
Rule 196 (reflection of 140) for $m= 0$ and $\ell = 1$.
Rule 200 (reflection of 200) for $m= 0$ and $\ell = 1$.

$\square$

3.6 Inductive counter-example to max-sensitivity (3 rules)

Note that when $n=m+\ell$ then we have the additional constraint $-m=\ell$ (with appropriate modulo). As a consequence the $\forall (x_{-m-1},\ldots ,x_{\ell +1})$ of Lemma 4 becomes $\forall (x_{-m-1},\ldots ,x_{\ell -2})$ and we have $x_{\ell -1}=x_{-m-1}$, $x_{\ell }=x_{-m}$, $x_{\ell +1}=x_{-m+1}$. However this test is valid only for the given $n=m+\ell$, and in order to have a result valid for any n we need an induction step. In this section we close this gap for rules 128, 160, 162 [the rules to consider were guessed from exhaustive tests for small values of n in Montalva et al. (2018)].

Theorem 5

Rules 128, 160, 162 are not max-sensitive for any n.

Proof

Instead of rule 162 we will consider its reflection, rule 176, so that the three rules all have the same “orientation”. We recall the definition of their local function, with column $abc \in \{{\texttt{0}},{\texttt{1}}\}^3$ representing the value of f(a, b, c).

We consider the same update schedules as in the previous section: let ${\varDelta },{\varDelta }'$ be given by Property 2 (with all other labels $\oplus$) for 0 and the $m,\ell$ existing above, i.e. ${\varDelta }$ and ${\varDelta }'$ differ only in the labeling of arc (1, 0). Then for all $x \in \{{\texttt{0}},{\texttt{1}}\}^n$ we will prove that $F_{{\varDelta }}(x)_i=F_{{\varDelta }'}(x)_i$ for all i.

For all $i \ne 0$ we still directly have that i is (a, b)-bounded with the same a and b in both ${\varDelta }$ and ${\varDelta }'$. As a consequence of Lemma 3, for all $i \ne 0$ we have $F_{{\varDelta }}(x)_{i}=F_{{\varDelta }'}(x)_{i}$. Now let us consider cell 0. For any $m \ge 0$, a straightforward induction gives the following:

$$\begin{aligned} \text {if} \, \exists k: (-m-1 \le k \le 1) \wedge (x_k={\texttt{0}}) \, \text {then} \, F_{{\varDelta }}(x)_0=F_{{\varDelta }'}(x)_0={\texttt{0}}. \end{aligned}$$

Consequently, for ${\varDelta },{\varDelta }'$ given by $\ell =1$ and $m=n-1$, this means that for all $x \in \{{\texttt{0}},{\texttt{1}}\}^n$ such that $x \ne ({\texttt{1}},\ldots ,{\texttt{1}})$ we have $F_{{\varDelta }}(x)_0=F_{{\varDelta }'}(x)_0={\texttt{0}}$. Since furthermore another straightforward induction gives $F_{{\varDelta }}(({\texttt{1}},\ldots ,{\texttt{1}}))_0=F_{{\varDelta }'}(({\texttt{1}},\ldots ,{\texttt{1}}))_0={\texttt{1}}$, we have the same transition digraph (dynamic) for rules 128, 160, 176 (reflection of 162) under update schedules ${\varDelta }\not \equiv {\varDelta }'$. $\square$

3.7 Finite proof of max-sensitivity (55 rules)

According to Formula (1), given a rule, if for all ${\varDelta }\not \equiv {\varDelta }'$ we can prove that there exist a configuration x and a cell $i_0$ such that $F_{{\varDelta }}(x)_{i_0} \ne F_{{\varDelta }'}(x)_{i_0}$, then the rule is max-sensitive. This is our strategy in this section, using Property 1 for each pair of non-equivalent update schedules. We recall that we present the reasoning in the case of Formula (2) (as it is presented in Property 1), but we will have to consider the two symmetric cases to prove max-sensitivity.

The following lemma is kind of brute force: it looks for some finite upper bounds to the bounding of $i_0$ in ${\varDelta }$ and ${\varDelta }'$, so that whatever the $m,m',\ell '$ given by Property 1 we can always ensure that there exist a configuration x and a cell $i_0$ such that $F_{{\varDelta }}(x)_{i_0} \ne F_{{\varDelta }'}(x)_{i_0}$. Depending on the values of $m, m', \ell '$ given by Property 1 compared to the ${\hat{m}},{\hat{\ell }}$ of the following lemma, we will fall in one of the eight cases, and the formula for each case ensures that it is possible to construct one such x in this case. Such a proof has been sketched in Montalva et al. (2017) for rule 1.

Lemma 5

Given a rule f and its reflection, if there exist ${\hat{m}} \ge 0, {\hat{\ell }} \ge 1$ satisfying the 8 formulas

1.
$\forall m< {\hat{m}}, m'< {\hat{m}}, 1 \le \ell ' < {\hat{\ell }} : \exists (x^1_{-\max \{m,m'\}-1},\ldots ,x^1_0,\ldots ,x^1_{\ell '+1})$:
$$\begin{aligned}&f^{{-m}\rightarrow {0}\leftarrow {0}}((x^1_{-m-1},\ldots ,x^1_0,x^1_1)) \\&\quad = {\texttt {1}}-f^{{-m'}\rightarrow {0}\leftarrow {\ell '}}((x^1_{-m'-1},\ldots , x^1_0,\ldots ,x^1_{\ell '+1})) \end{aligned}$$
2.
$\forall m< {\hat{m}}, m' < {\hat{m}} : \exists (x^2_{-\max \{m,m'\}-1},\ldots ,x^2_0,\ldots ,x^2_{{\hat{\ell }}}):$
$$\begin{aligned}&f^{{-m}\rightarrow {0}\leftarrow {0}}((x^2_{-m-1},\ldots ,x^2_0,x^2_1)) \\&\quad = {\texttt{1}}-f^{{-m'}\rightarrow {0}\leftarrow {{\hat{\ell }}}}((x^2_{-m'-1},\ldots ,x^2_0, \dots ,x^2_{{\hat{\ell }}},{\texttt{0}}))\\&\quad = {\texttt{1}}-f^{{-m'}\rightarrow {0}\leftarrow {{\hat{\ell }}}}((x^2_{-m'-1},\ldots ,x^2_0, \dots ,x^2_{{\hat{\ell }}},{\texttt{1}})) \end{aligned}$$
3.
$\forall m< {\hat{m}}, 1 \le \ell ' < {\hat{\ell }} : \exists (x^3_{-{\hat{m}}},\ldots ,x^3_0,\ldots ,x^3_{\ell '+1}):$
$$\begin{aligned}&f^{{-m}\rightarrow {0}\leftarrow {0}}((x^3_{-m-1},\ldots ,x^3_0,x^3_1)) \\&\quad = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {\ell '}}(({\texttt{0}},x^3_{-{\hat{m}}},\ldots , x^3_0,\ldots ,x^3_{\ell '+1}))\\&\quad = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {\ell '}}(({\texttt{1}},x^3_{-{\hat{m}}}, \dots ,x^3_0,\ldots ,x^3_{\ell '+1})) \end{aligned}$$
4.
$\forall m < {\hat{m}} : \exists (x^4_{-{\hat{m}}},\ldots ,x^4_0,\ldots ,x^4_{{\hat{\ell }}}):$
$$\begin{aligned}&f^{{-m}\rightarrow {0}\leftarrow {0}}((x^4_{-m-1},\ldots ,x^4_0,x^4_1)) \\&\quad = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {{\hat{\ell }}}}(({\texttt{0}},x^4_{-{\hat{m}}}, \dots ,x^4_0,\ldots ,x^4_{{\hat{\ell }}},{\texttt{0}}))\\&\quad = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {{\hat{\ell }}}}(({\texttt{1}},x^4_{-{\hat{m}}}, \dots ,x^4_0,\ldots ,x^4_{{\hat{\ell }}},{\texttt{0}}))\\&\quad = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {{\hat{\ell }}}}(({\texttt{0}},x^4_{-{\hat{m}}}, \dots ,x^4_0,\ldots ,x^4_{{\hat{\ell }}},{\texttt{1}}))\\&\quad = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {{\hat{\ell }}}}(({\texttt{1}},x^4_{-{\hat{m}}}, \dots ,x^4_0,\ldots ,x^4_{{\hat{\ell }}},{\texttt{1}})) \end{aligned}$$
5.
$\forall m'< {\hat{m}}, 1 \le \ell ' < {\hat{\ell }} : \exists (x^5_{-{\hat{m}}},\ldots ,x^5_0,\ldots ,x^5_{\ell '+1}):$
$$\begin{aligned}&f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {0}}(({\texttt{0}},x^5_{-{\hat{m}}},\ldots ,x^5_0,x^5_1)) \\&\quad =f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {0}}(({\texttt{1}},x^5_{-{\hat{m}}},\ldots ,x^5_0,x^5_1))\\&\quad = {\texttt{1}}-f^{{-m'}\rightarrow {0}\leftarrow {\ell '}}((x^5_{-m'-1},\ldots ,x^5_0,\ldots ,x^5_{\ell '+1})) \end{aligned}$$
6.
$\forall m' < {\hat{m}} : \exists (x^6_{-{\hat{m}}},\ldots ,x^6_0,\ldots ,x^6_{{\hat{\ell }}}):$
$$\begin{aligned}&f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {0}}(({\texttt{0}},x^6_{-{\hat{m}}},\ldots ,x^6_0,x^6_1)) \\&\quad =f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {0}}(({\texttt{1}},x^6_{-{\hat{m}}},\ldots ,x^6_0,x^6_1)) \\&\quad = {\texttt{1}}-f^{{-m'}\rightarrow {0}\leftarrow {{\hat{\ell }}}}((x^6_{-m'-1},\ldots ,x^6_0,\ldots , x^6_{{\hat{\ell }}},{\texttt{0}}))\\&\quad = {\texttt{1}}-f^{{-m'}\rightarrow {0}\leftarrow {{\hat{\ell }}}}((x^6_{-m'-1}, \dots ,x^6_0,\ldots ,x^6_{{\hat{\ell }}},{\texttt{1}})) \end{aligned}$$
7.
$\forall 1 \le \ell ' < {\hat{\ell }} : \exists (x^7_{-{\hat{m}}},\ldots ,x^7_0,\ldots ,x^7_{\ell '+1})$:
$$\begin{aligned}&f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {0}}(({\texttt{0}},x^7_{-{\hat{m}}},\ldots ,x^7_0,x^7_1)) \\&\quad =f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {0}}(({\texttt{1}},x^7_{-{\hat{m}}},\ldots ,x^7_0,x^7_1)) \\&\quad = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {\ell '}}(({\texttt{0}},x^7_{-{\hat{m}}},\ldots ,x^7_0, \dots ,x^7_{\ell '+1}))\\&\quad = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {\ell '}}(({\texttt{1}},x^7_{-{\hat{m}}}, \dots ,x^7_0,\ldots ,x^7_{\ell '+1})) \end{aligned}$$
8.
$\exists (x^8_{-{\hat{m}}},\ldots ,x^8_0,\ldots ,x^8_{{\hat{\ell }}}):$
$$\begin{aligned}&f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {0}}(({\texttt{0}},x^8_{-{\hat{m}}},\ldots ,x^8_0,x^8_1)) \\&\quad =f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {0}}(({\texttt{1}},x^8_{-{\hat{m}}},\ldots ,x^8_0,x^8_1)) \\&\quad = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {{\hat{\ell }}}}(({\texttt{0}},x^8_{-{\hat{m}}}, \dots ,x^8_0,\ldots ,x^8_{{\hat{\ell }}},{\texttt{0}}))\\&\quad = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {{\hat{\ell }}}}(({\texttt{1}},x^8_{-{\hat{m}}}, \dots ,x^8_0,\ldots ,x^8_{{\hat{\ell }}},{\texttt{0}}))\\&\quad = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {{\hat{\ell }}}}(({\texttt{0}},x^8_{-{\hat{m}}}, \dots ,x^8_0,\ldots ,x^8_{{\hat{\ell }}},{\texttt{1}}))\\&\quad = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {{\hat{\ell }}}}(({\texttt{1}},x^8_{-{\hat{m}}}, \dots ,x^8_0,\ldots ,x^8_{{\hat{\ell }}},{\texttt{1}})) \end{aligned}$$

then $\forall {\varDelta }\not \equiv {\varDelta }': \exists x \in \{{\texttt{0}},{\texttt{1}}\}^n: \exists i_0: F_{{\varDelta }}(x)_{i_0} \ne F_{{\varDelta }'}(x)_{i_0}$, for any $n \ge {\hat{m}}+{\hat{\ell }}+1$.

Proof

Let ${\varDelta }\not \equiv {\varDelta }'$ according to the case of Formula (2). Then, according to Property 1 there exist some $i_0,m,m',\ell '$. Depending on the order of m (resp.$m', \ell '$) compared to ${\hat{m}}$ (resp.${\hat{m}}, {\hat{\ell }}$), we fall in one of the 8 cases above (for example if $m \ge {\hat{m}}, m'<{\hat{m}}, \ell ' \ge {\hat{\ell }}$ then we are in case 6), let us denote it $c \in {\llbracket} 1;8 {\rrbracket }$. We use the fact that cellular automata are shift invariant: what is claimed at cell 0 in the hypothesis can be applied to cell $i_0$. Lemma 3 can be used (the left (resp. right) side of equalities corresponds to ${\varDelta }$ (resp. ${\varDelta }'$)) to conclude:

$$\begin{aligned} \exists x \in \{{\texttt{0}},{\texttt{1}}\}^n \quad \text { (with }\, x_i=x^c_i \,\text { where }\, x^c \text { is defined)} : F_{{\varDelta }}(x)_{i_0} \ne F_{{\varDelta }'}(x)_{i_0}. \end{aligned}$$

Indeed, when m (resp. $m', \ell '$) is strictly smaller than ${\hat{m}}$ (resp. ${\hat{m}}, {\hat{\ell }}$) then there is no special consideration, and when m (resp. $m', \ell '$) is larger than ${\hat{m}}$ (resp. ${\hat{m}}, {\hat{\ell }}$) then whatever the result $x'_{i_0-{\hat{m}}-1}$ (resp. $x'_{i_0-{\hat{m}}-1}, x'_{i_0{\hat{\ell }}+1}$) of substeps updating the state of cells $i_0-m$ to $i_0-{\hat{m}}-1$ (resp. $i_0-m'$ to $i_0-{\hat{m}}-1$, $i_0+\ell '$ to $i_0+{\hat{\ell }}+1$) we have

$$\begin{aligned} F_{{\varDelta }}(x)_{i_0}&= f^{{-m}\rightarrow {i_0}\leftarrow {0}}((x_{-i_0-m-1}, \dots ,x_{i_0},x_{i_0+1}))\\&= f^{{-{\hat{m}}}\rightarrow {i_0}\leftarrow {0}}((x'_{i_0-{\hat{m}}-1},x_{i_0- {\hat{m}}},\ldots ,x_{i_0},x_{i_0+1}))\\ \text {(resp. } F_{{\varDelta }'}(x)_{i_0}&= f^{{-{\hat{m}}}\rightarrow {i_0}\leftarrow {a}} \\&\quad ((x'_{i_0-{\hat{m}}-1},x_{i_0-{\hat{m}}},\ldots ,x_{i_0},\ldots ,x_{i_0+a+1})) \\&\qquad \text { for}\,\text { any }\,a,\\ F_{{\varDelta }'}(x)_{i_0}&= f^{{-a}\rightarrow {i_0}\leftarrow {{\hat{\ell }}}} \\&\quad ((x_{i_0-a-1}, \dots ,x_{i_0},\ldots ,x_{i_0+{\hat{\ell }}},x'_{i_0+{\hat{\ell }}+1})) \\&\qquad \text { for}\,\text { any }\,a {\text {)}} \end{aligned}$$

and the Lemma claims that whether $x'_{i_0-{\hat{m}}-1}={\texttt{0}}$ or $x'_{i_0-{\hat{m}}-1}={\texttt{1}}$ (resp. $x'_{i_0-{\hat{m}}-1}={\texttt{0}}$ or $x'_{i_0-{\hat{m}}-1}={\texttt{1}}$, $x'_{i_0+{\hat{\ell }}+1}={\texttt{0}}$ or $x'_{i_0+{\hat{\ell }}+1}={\texttt{1}}$) do not matter to have different images at $i_0$.

In order to be always able to use $x^c$ to construct x, we require $n \ge {\hat{m}}+{\hat{l}}+1$. $\square$

Note that the hypothesis of Lemma 5 takes a time ${\mathcal {O}}({\hat{m}}^2{\hat{\ell }}\,2^{{\hat{m}}+{\hat{\ell }}})$ to check, for a countably infinite number of ${\hat{m}}$ and ${\hat{\ell }}$. Also note that taking different ${\hat{m}}$ and ${\hat{m}}'$ for ${\varDelta }$ and ${\varDelta }'$ would also work with accordingly detailed considerations, and would give qualitatively similar results when tested on the family of ECAs. Some unintensive computer tests give the next theorem.

Theorem 6

Max-sensitivity is achieved by rules 1, 4, 5, 6, 19, 22, 23, 24, 27, 36, 37, 46, 50, 54, 126, 152, 178, 184 for any$n \ge 3$, rules 9, 14, 18, 29, 35, 38, 43, 56, 57, 58, 74, 94, 110, 132, 142, 146, 156, 172 for any given explicit names which are $n \ge 4$, rules 7, 11, 26, 62, 72, 73, 78, 108, 122, 134 for any$n \ge 5$, rules 33, 41, 76, 77, 164, 232 for any$n \ge 6$, rules 13, 25, 104 for any$n \ge 7$.

Proof

The hypothesis of Lemma 5 have been tested for all pair of $0\le {\hat{m}} \le 5$ and $1 \le {\hat{\ell }} \le 5$, and for the two symmetric cases of Formula (2) (equivalently, the hypothesis of Lemma 5 have been tested for a rule and its reflection). As an additional witness to the values of ${\hat{m}}$ and ${\hat{\ell }}$ for a rule and its reflection, we also give an $x \in \{{\texttt{0}},{\texttt{1}}\}^{{\hat{m}}+{\hat{\ell }}+1}$ satisfying the 8th and last formula (this case represents asymptotically a hundred percents of update schedules).

Rule 1 (reflection 1) passed all 8 tests for ${\hat{m}}= 1 , {\hat{\ell }}= 1$, with $x^8= ({\texttt{1}}, {\texttt{0}}, {\texttt{1}})$.
Rule 4 (reflection 4) passed all 8 tests for ${\hat{m}}= 1 , {\hat{\ell }}= 1$, with $x^8= ({\texttt{0}}, {\texttt{1}}, {\texttt{1}})$.
Rule 5 (reflection 5) passed all 8 tests for ${\hat{m}}= 1 , {\hat{\ell }}= 1$, with $x^8= ({\texttt{0}}, {\texttt{1}}, {\texttt{1}})$.
Rule 6 (reflection 20) passed all 8 tests for ${\hat{m}}= 1 , {\hat{\ell }}= 1$, with $x^8= ({\texttt{1}}, {\texttt{1}}, {\texttt{1}})$.
Rule 20 (reflection 6) passed all 8 tests for ${\hat{m}}= 1 , {\hat{\ell }}= 1$, with $x^8= ({\texttt{0}}, {\texttt{1}}, {\texttt{1}})$.
Rule 7 (reflection 21) passed all 8 tests for ${\hat{m}}= 1 , {\hat{\ell }}= 1$, with $x^8= ({\texttt{1}}, {\texttt{1}}, {\texttt{1}})$.
Rule 21 (reflection 7) passed all 8 tests for ${\hat{m}}= 0 , {\hat{\ell }}= 4$, with $x^8= ({\texttt{0}}, {\texttt{0}}, {\texttt{0}}, {\texttt{1}}, {\texttt{1}})$.
Rule 9 (reflection 65) passed all 8 tests for ${\hat{m}}= 1 , {\hat{\ell }}= 1$, with $x^8= ({\texttt{0}}, {\texttt{1}}, {\texttt{1}})$.
Rule 65 (reflection 9) passed all 8 tests for ${\hat{m}}= 2 , {\hat{\ell }}= 1$, with $x^8= ({\texttt{0}}, {\texttt{1}}, {\texttt{0}}, {\texttt{1}})$.
Rule 11 (reflection 81) passed all 8 tests for ${\hat{m}}= 3 , {\hat{\ell }}= 1$, with $x^8= ({\texttt{1}}, {\texttt{0}}, {\texttt{0}}, {\texttt{1}}, {\texttt{1}})$.
Rule 81 (reflection 11) passed all 8 tests for ${\hat{m}}= 0 , {\hat{\ell }}= 1$, with $x^8= ({\texttt{0}}, {\texttt{1}})$.
Rule 13 (reflection 69) passed all 8 tests for ${\hat{m}}= 3 , {\hat{\ell }}= 3$, with $x^8= ({\texttt{0}}, {\texttt{1}}, {\texttt{0}}, {\texttt{0}}, {\texttt{0}}, {\texttt{0}}, {\texttt{1}})$.
Rule 69 (reflection 13) passed all 8 tests for ${\hat{m}}= 0 , {\hat{\ell }}= 3$, with $x^8= ({\texttt{1}}, {\texttt{1}}, {\texttt{1}}, {\texttt{0}})$.
Rule 14 (reflection 84) passed all 8 tests for ${\hat{m}}= 1 , {\hat{\ell }}= 2$, with $x^8= ({\texttt{0}}, {\texttt{0}}, {\texttt{0}}, {\texttt{1}})$.
Rule 84 (reflection 14) passed all 8 tests for ${\hat{m}}= 0 , {\hat{\ell }}= 2$, with $x^8= ({\texttt{1}}, {\texttt{0}}, {\texttt{0}})$.
Rule 18 (reflection 18) passed all 8 tests for ${\hat{m}}= 1 , {\hat{\ell }}= 2$, with $x^8= ({\texttt{1}}, {\texttt{0}}, {\texttt{1}}, {\texttt{0}})$.
Rule 19 (reflection 19) passed all 8 tests for ${\hat{m}}= 1 , {\hat{\ell }}= 1$, with $x^8= ({\texttt{0}}, {\texttt{0}}, {\texttt{0}})$.
Rule 22 (reflection 22) passed all 8 tests for ${\hat{m}}= 1 , {\hat{\ell }}= 1$, with $x^8= ({\texttt{1}}, {\texttt{1}}, {\texttt{1}})$.
Rule 23 (reflection 23) passed all 8 tests for ${\hat{m}}= 1 , {\hat{\ell }}= 1$, with $x^8= ({\texttt{0}}, {\texttt{0}}, {\texttt{0}})$.
Rule 24 (reflection 66) passed all 8 tests for ${\hat{m}}= 1 , {\hat{\ell }}= 1$, with $x^8= ({\texttt{0}}, {\texttt{1}}, {\texttt{1}})$.
Rule 66 (reflection 24) passed all 8 tests for ${\hat{m}}= 1 , {\hat{\ell }}= 1$, with $x^8= ({\texttt{0}}, {\texttt{0}}, {\texttt{1}})$.
Rule 25 (reflection 67) passed all 8 tests for ${\hat{m}}= 0 , {\hat{\ell }}= 2$, with $x^8= ({\texttt{0}}, {\texttt{1}}, {\texttt{1}})$.
Rule 67 (reflection 25) passed all 8 tests for ${\hat{m}}= 3 , {\hat{\ell }}= 3$, with $x^8= ({\texttt{1}}, {\texttt{1}}, {\texttt{0}}, {\texttt{1}}, {\texttt{1}}, {\texttt{1}}, {\texttt{0}})$.
Rule 26 (reflection 82) passed all 8 tests for ${\hat{m}}= 1 , {\hat{\ell }}= 2$, with $x^8= ({\texttt{1}}, {\texttt{0}}, {\texttt{1}}, {\texttt{1}})$.
Rule 82 (reflection 26) passed all 8 tests for ${\hat{m}}= 2 , {\hat{\ell }}= 2$, with $x^8= ({\texttt{1}}, {\texttt{1}}, {\texttt{0}}, {\texttt{1}}, {\texttt{0}})$.
Rule 27 (reflection 83) passed all 8 tests for ${\hat{m}}= 1 , {\hat{\ell }}= 1$, with $x^8= ({\texttt{0}}, {\texttt{0}}, {\texttt{0}})$.
Rule 83 (reflection 27) passed all 8 tests for ${\hat{m}}= 1 , {\hat{\ell }}= 1$, with $x^8= ({\texttt{0}}, {\texttt{0}}, {\texttt{0}})$.
Rule 29 (reflection 71) passed all 8 tests for ${\hat{m}}= 0 , {\hat{\ell }}= 3$, with $x^8= ({\texttt{0}}, {\texttt{0}}, {\texttt{0}}, {\texttt{1}})$.
Rule 71 (reflection 29) passed all 8 tests for ${\hat{m}}= 0 , {\hat{\ell }}= 3$, with $x^8= ({\texttt{1}}, {\texttt{1}}, {\texttt{1}}, {\texttt{0}})$.
Rule 33 (reflection 33) passed all 8 tests for ${\hat{m}}= 1 , {\hat{\ell }}= 4$, with $x^8= ({\texttt{1}}, {\texttt{0}}, {\texttt{0}}, {\texttt{0}}, {\texttt{0}}, {\texttt{1}})$.
Rule 35 (reflection 49) passed all 8 tests for ${\hat{m}}= 2 , {\hat{\ell }}= 1$, with $x^8= ({\texttt{1}}, {\texttt{0}}, {\texttt{0}}, {\texttt{0}})$.
Rule 49 (reflection 35) passed all 8 tests for ${\hat{m}}= 1 , {\hat{\ell }}= 1$, with $x^8= ({\texttt{1}}, {\texttt{0}}, {\texttt{1}})$.
Rule 36 (reflection 36) passed all 8 tests for ${\hat{m}}= 1 , {\hat{\ell }}= 1$, with $x^8= ({\texttt{1}}, {\texttt{1}}, {\texttt{1}})$.
Rule 37 (reflection 37) passed all 8 tests for ${\hat{m}}= 1 , {\hat{\ell }}= 1$, with $x^8= ({\texttt{1}}, {\texttt{1}}, {\texttt{1}})$.
Rule 38 (reflection 52) passed all 8 tests for ${\hat{m}}= 0 , {\hat{\ell }}= 3$, with $x^8= ({\texttt{0}}, {\texttt{0}}, {\texttt{1}}, {\texttt{1}})$.
Rule 52 (reflection 38) passed all 8 tests for ${\hat{m}}= 1 , {\hat{\ell }}= 1$, with $x^8= ({\texttt{1}}, {\texttt{1}}, {\texttt{0}})$.
Rule 41 (reflection 97) passed all 8 tests for ${\hat{m}}= 1 , {\hat{\ell }}= 2$, with $x^8= ({\texttt{1}}, {\texttt{0}}, {\texttt{1}}, {\texttt{1}})$.
Rule 97 (reflection 41) passed all 8 tests for ${\hat{m}}= 2 , {\hat{\ell }}= 3$, with $x^8= ({\texttt{1}}, {\texttt{1}}, {\texttt{0}}, {\texttt{0}}, {\texttt{1}}, {\texttt{0}})$.
Rule 43 (reflection 113) passed all 8 tests for ${\hat{m}}= 2 , {\hat{\ell }}= 1$, with $x^8= ({\texttt{0}}, {\texttt{1}}, {\texttt{1}}, {\texttt{1}})$.
Rule 113 (reflection 43) passed all 8 tests for ${\hat{m}}= 2 , {\hat{\ell }}= 1$, with $x^8= ({\texttt{0}}, {\texttt{0}}, {\texttt{1}}, {\texttt{0}})$.
Rule 46 (reflection 116) passed all 8 tests for ${\hat{m}}= 0 , {\hat{\ell }}= 2$, with $x^8= ({\texttt{0}}, {\texttt{0}}, {\texttt{1}})$.
Rule 116 (reflection 46) passed all 8 tests for ${\hat{m}}= 0 , {\hat{\ell }}= 1$, with $x^8= ({\texttt{1}}, {\texttt{0}})$.
Rule 50 (reflection 50) passed all 8 tests for ${\hat{m}}= 1 , {\hat{\ell }}= 1$, with $x^8= ({\texttt{1}}, {\texttt{0}}, {\texttt{1}})$.
Rule 54 (reflection 54) passed all 8 tests for ${\hat{m}}= 1 , {\hat{\ell }}= 1$, with $x^8= ({\texttt{1}}, {\texttt{1}}, {\texttt{0}})$.
Rule 56 (reflection 98) passed all 8 tests for ${\hat{m}}= 2 , {\hat{\ell }}= 1$, with $x^8= ({\texttt{1}}, {\texttt{0}}, {\texttt{1}}, {\texttt{0}})$.
Rule 98 (reflection 56) passed all 8 tests for ${\hat{m}}= 0 , {\hat{\ell }}= 1$, with $x^8= ({\texttt{0}}, {\texttt{1}})$.
Rule 57 (reflection 99) passed all 8 tests for ${\hat{m}}= 1 , {\hat{\ell }}= 2$, with $x^8= ({\texttt{1}}, {\texttt{0}}, {\texttt{1}}, {\texttt{1}})$.
Rule 99 (reflection 57) passed all 8 tests for ${\hat{m}}= 1 , {\hat{\ell }}= 2$, with $x^8= ({\texttt{0}}, {\texttt{1}}, {\texttt{0}}, {\texttt{0}})$.
Rule 58 (reflection 114) passed all 8 tests for ${\hat{m}}= 1 , {\hat{\ell }}= 2$, with $x^8= ({\texttt{1}}, {\texttt{0}}, {\texttt{1}}, {\texttt{1}})$.
Rule 114 (reflection 58) passed all 8 tests for ${\hat{m}}= 1 , {\hat{\ell }}= 1$, with $x^8= ({\texttt{0}}, {\texttt{1}}, {\texttt{0}})$.
Rule 62 (reflection 118) passed all 8 tests for ${\hat{m}}= 2 , {\hat{\ell }}= 2$, with $x^8= ({\texttt{0}}, {\texttt{1}}, {\texttt{0}}, {\texttt{0}}, {\texttt{1}})$.
Rule 118 (reflection 62) passed all 8 tests for ${\hat{m}}= 0 , {\hat{\ell }}= 1$, with $x^8= ({\texttt{1}}, {\texttt{0}})$.
Rule 72 (reflection 72) passed all 8 tests for ${\hat{m}}= 1 , {\hat{\ell }}= 3$, with $x^8= ({\texttt{0}}, {\texttt{1}}, {\texttt{1}}, {\texttt{1}}, {\texttt{0}})$.
Rule 73 (reflection 73) passed all 8 tests for ${\hat{m}}= 1 , {\hat{\ell }}= 3$, with $x^8= ({\texttt{0}}, {\texttt{1}}, {\texttt{1}}, {\texttt{1}}, {\texttt{0}})$.
Rule 74 (reflection 88) passed all 8 tests for ${\hat{m}}= 1 , {\hat{\ell }}= 2$, with $x^8= ({\texttt{0}}, {\texttt{0}}, {\texttt{1}}, {\texttt{0}})$.
Rule 88 (reflection 74) passed all 8 tests for ${\hat{m}}= 1 , {\hat{\ell }}= 2$, with $x^8= ({\texttt{0}}, {\texttt{1}}, {\texttt{0}}, {\texttt{0}})$.
Rule 76 (reflection 76) passed all 8 tests for ${\hat{m}}= 2 , {\hat{\ell }}= 3$, with $x^8= ({\texttt{0}}, {\texttt{1}}, {\texttt{1}}, {\texttt{1}}, {\texttt{1}}, {\texttt{0}})$.
Rule 77 (reflection 77) passed all 8 tests for ${\hat{m}}= 2 , {\hat{\ell }}= 3$, with $x^8= ({\texttt{0}}, {\texttt{1}}, {\texttt{1}}, {\texttt{1}}, {\texttt{1}}, {\texttt{0}})$.
Rule 78 (reflection 92) passed all 8 tests for ${\hat{m}}= 1 , {\hat{\ell }}= 2$, with $x^8= ({\texttt{0}}, {\texttt{0}}, {\texttt{0}}, {\texttt{1}})$.
Rule 92 (reflection 78) passed all 8 tests for ${\hat{m}}= 2 , {\hat{\ell }}= 2$, with $x^8= ({\texttt{0}}, {\texttt{1}}, {\texttt{1}}, {\texttt{0}}, {\texttt{0}})$.
Rule 94 (reflection 94) passed all 8 tests for ${\hat{m}}= 1 , {\hat{\ell }}= 2$, with $x^8= ({\texttt{1}}, {\texttt{0}}, {\texttt{0}}, {\texttt{1}})$.
Rule 104 (reflection 104) passed all 8 tests for ${\hat{m}}= 2 , {\hat{\ell }}= 4$, with $x^8= ({\texttt{0}}, {\texttt{0}}, {\texttt{1}}, {\texttt{1}}, {\texttt{1}}, {\texttt{0}}, {\texttt{0}})$.
Rule 108 (reflection 108) passed all 8 tests for ${\hat{m}}= 2 , {\hat{\ell }}= 2$, with $x^8= ({\texttt{1}}, {\texttt{0}}, {\texttt{1}}, {\texttt{0}}, {\texttt{1}})$.
Rule 110 (reflection 124) passed all 8 tests for ${\hat{m}}= 0 , {\hat{\ell }}= 2$, with $x^8= ({\texttt{0}}, {\texttt{0}}, {\texttt{1}})$.
Rule 124 (reflection 110 ) passed all 8 tests for ${\hat{m}}= 2 , {\hat{\ell }}= 1$, with $x^8= ({\texttt{1}}, {\texttt{0}}, {\texttt{1}}, {\texttt{0}})$.
Rule 122 (reflection 122) passed all 8 tests for ${\hat{m}}= 1 , {\hat{\ell }}= 3$, with $x^8= ({\texttt{0}}, {\texttt{1}}, {\texttt{0}}, {\texttt{0}}, {\texttt{0}})$.
Rule 126 (reflection 126) passed all 8 tests for ${\hat{m}}= 1 , {\hat{\ell }}= 1$, with $x^8= ({\texttt{0}}, {\texttt{1}}, {\texttt{0}})$.
Rule 132 (reflection 132) passed all 8 tests for ${\hat{m}}= 1 , {\hat{\ell }}= 2$, with $x^8= ({\texttt{0}}, {\texttt{1}}, {\texttt{1}}, {\texttt{0}})$.
Rule 134 (reflection 148) passed all 8 tests for ${\hat{m}}= 1 , {\hat{\ell }}= 3$, with $x^8= ({\texttt{0}}, {\texttt{0}}, {\texttt{0}}, {\texttt{1}}, {\texttt{0}})$.
Rule 148 (reflection 134) passed all 8 tests for ${\hat{m}}= 1 , {\hat{\ell }}= 2$, with $x^8= ({\texttt{0}}, {\texttt{1}}, {\texttt{0}}, {\texttt{0}})$.
Rule 142 (reflection 212) passed all 8 tests for ${\hat{m}}= 1 , {\hat{\ell }}= 2$, with $x^8= ({\texttt{0}}, {\texttt{0}}, {\texttt{0}}, {\texttt{1}})$.
Rule 212 (reflection 142) passed all 8 tests for ${\hat{m}}= 1 , {\hat{\ell }}= 2$, with $x^8= ({\texttt{0}}, {\texttt{1}}, {\texttt{0}}, {\texttt{0}})$.
Rule 146 (reflection 146) passed all 8 tests for ${\hat{m}}= 1 , {\hat{\ell }}= 2$, with $x^8= ({\texttt{1}}, {\texttt{0}}, {\texttt{1}}, {\texttt{0}})$.
Rule 152 (reflection 194) passed all 8 tests for ${\hat{m}}= 0 , {\hat{\ell }}= 2$, with $x^8= ({\texttt{1}}, {\texttt{0}}, {\texttt{0}})$.
Rule 194 (reflection 152) passed all 8 tests for ${\hat{m}}= 1 , {\hat{\ell }}= 1$, with $x^8= ({\texttt{0}}, {\texttt{0}}, {\texttt{1}})$.
Rule 156 (reflection 198) passed all 8 tests for ${\hat{m}}= 1 , {\hat{\ell }}= 2$, with $x^8= ({\texttt{1}}, {\texttt{1}}, {\texttt{0}}, {\texttt{0}})$.
Rule 198 (reflection 156) passed all 8 tests for ${\hat{m}}= 1 , {\hat{\ell }}= 2$, with $x^8= ({\texttt{0}}, {\texttt{0}}, {\texttt{1}}, {\texttt{1}})$.
Rule 164 (reflection 164) passed all 8 tests for ${\hat{m}}= 2 , {\hat{\ell }}= 3$, with $x^8= ({\texttt{0}}, {\texttt{0}}, {\texttt{1}}, {\texttt{1}}, {\texttt{0}}, {\texttt{0}})$.
Rule 172 (reflection 228) passed all 8 tests for ${\hat{m}}= 1 , {\hat{\ell }}= 2$, with $x^8= ({\texttt{1}}, {\texttt{1}}, {\texttt{0}}, {\texttt{1}})$.
Rule 228 (reflection 172) passed all 8 tests for ${\hat{m}}= 1 , {\hat{\ell }}= 2$, with $x^8= ({\texttt{1}}, {\texttt{0}}, {\texttt{1}}, {\texttt{1}})$.
Rule 178 (reflection 178) passed all 8 tests for ${\hat{m}}= 1 , {\hat{\ell }}= 1$, with $x^8= ({\texttt{0}}, {\texttt{1}}, {\texttt{0}})$.
Rule 184 (reflection 226) passed all 8 tests for ${\hat{m}}= 0 , {\hat{\ell }}= 1$, with $x^8= ({\texttt{1}}, {\texttt{0}})$.
Rule 226 (reflection 184) passed all 8 tests for ${\hat{m}}= 0 , {\hat{\ell }}= 1$, with $x^8= ({\texttt{0}}, {\texttt{1}})$.
Rule 232 (reflection 232) passed all 8 tests for ${\hat{m}}= 2 , {\hat{\ell }}= 3$, with $x^8= ({\texttt{0}}, {\texttt{0}}, {\texttt{1}}, {\texttt{0}}, {\texttt{1}}, {\texttt{1}})$.

$\square$

3.8 Inductive proof of max-sensitivity (12 rules)

In this subsection we follow the same idea as in the previous subsection, but we refine the condition on $x^c$ in each case $c \in {\llbracket} 1;8 {\rrbracket }$, so that it also allows inductions with x of the forms

$$\begin{aligned} ({\texttt{0}}&,{\texttt{0}},\ldots ,{\texttt{0}},x_{-{\hat{m}}},\ldots ,x_{i_0},\dots )\\ ({\texttt{1}}&,{\texttt{0}},\ldots ,{\texttt{0}},x_{-{\hat{m}}},\ldots ,x_{i_0},\dots )\\ ({\texttt{0}}&,{\texttt{1}},\ldots ,{\texttt{1}},x_{-{\hat{m}}},\ldots ,x_{i_0},\dots )\\ ({\texttt{1}}&,{\texttt{1}},\ldots ,{\texttt{1}},x_{-{\hat{m}}},\ldots ,x_{i_0},\dots )\\ \uparrow \\ i_0-m-1 \end{aligned}$$

(until $lab((i_0-m-1,i_0-m))=\oplus$ on the left side), and similarly for the right side. The idea of such proofs has been sketched in Montalva et al. (2017) for rule 2 (with some missing considerations related to overlaps of the left and right boundings, as configurations are periodic).

In the case we want to consider inductions on one or both sides of x, it requires a more careful consideration of how the two sequences of labels $\ominus$ (left and right) meet and overlap (if they do). To give an idea, let us consider two update schedules ${\varDelta }\not \equiv {\varDelta }'$ and the $i_0,m,m',\ell '$ given by Property 1. In the case that we want to prove the existence of

$$\begin{aligned} (x_{i_0-m-1},\ldots ,x_{i_0},\ldots ,x_{i_0+\ell '+1}) \end{aligned}$$

then we have to consider the two last inequalities of Property 1, telling that it may be possible with ${\varDelta },{\varDelta }'$ that cells are identified as in one of the four following cases

$$\begin{aligned} \begin{array}{lrrcrcr} &{} x_{i_0-m-1}=x_{i_0+\ell '-1} &{}\wedge &{} x_{i_0-m}=x_{i_0+\ell '} &{}\wedge &{} x_{i_0-m+1}=x_{i_0+\ell '+1}\\ \text {or } &{} x_{i_0-m-1}=x_{i_0+\ell '} &{}\wedge &{} x_{i_0-m}=x_{i_0+\ell '+1} &{}&{}\\ \text {or } &{} x_{i_0-m-1}=x_{i_0+\ell '+1} &{}&{}&{}&{} \end{array} \end{aligned}$$

or no identification of cells. This depends on the ${\varDelta }, {\varDelta }'$, and we have to prove that in any case there exist an x and $i_0$ such that $F_{{\varDelta }}(x)_{i_0} \ne F_{{\varDelta }'}(x)_{i_0}$. It is clear that only configurations of the form

$$\begin{aligned} \begin{array}{rc} &{}({\texttt{0}},{\texttt{0}},\ldots ,{\texttt{0}},x_{-{\hat{m}}},\ldots ,x_{i_0},\ldots ,\dots , x_{{\hat{\ell }}},{\texttt{0}},\ldots ,{\texttt{0}},{\texttt{0}})\\ \text {or } &{}({\texttt{1}},{\texttt{1}},\ldots ,{\texttt{1}},x_{-{\hat{m}}},\ldots ,x_{i_0},\ldots , \dots ,x_{{\hat{\ell }}},{\texttt{1}},\ldots ,{\texttt{1}},{\texttt{1}}) \end{array} \end{aligned}$$

can satisfy the first case (and consequently, all four cases).

The following lemma includes Lemma 5, as for each case we consider (if applicable) inductions on both sides, one side only, and no induction. It is again a kind of brute force analysis of rules, but this time it requires a more careful consideration of the case disjunction. Though the number of cases is important (71 in a naive decomposition, reduced to 48 with basic analysis), the way it is decomposed is easy to validate, and each case is thereafter straightforward to investigate.

Though it simply formalizes the above reasoning, the next statement is long. It is basically a tedious but well structured case disjunction, as argued in the proof (which may guide the reader through predicates). It is marked with an emphasized color and formatting in order to ease the reading.

Lemma 6

Given a rule f and its reflection, if there exist ${\hat{m}} \ge 0, {\hat{\ell }} \ge 1$ satisfying the 8 predicates below (for clarity predicates are given explicit names which are only syntactic), then $\forall {\varDelta }\not \equiv {\varDelta }': \exists x \in \{{\texttt{0}},{\texttt{1}}\}^n: \exists i_0: F_{{\varDelta }}(x)_{i_0} \ne F_{{\varDelta }'}(x)_{i_0}$, for any $n \ge {\hat{m}}+{\hat{\ell }}+1$.

1.
$\underline{Predicate \, {\mathcal {I}}(m<{\hat{m}},m'<{\hat{m}},\ell '<{\hat{\ell }})}$, defined as $\forall m< {\hat{m}}, m'< {\hat{m}}, 1 \le \ell ' < {\hat{\ell }} : \exists (x^1_{-\max \{m,m'\}-1},\ldots ,x^1_0,\ldots ,x^1_{\ell '+1})$:
$$\begin{aligned}&f^{{-m}\rightarrow {0}\leftarrow {0}}((x^1_{-m-1},\ldots ,x^1_1)) \\&\quad = {\texttt {1}}-f^{{-m'}\rightarrow {0}\leftarrow {\ell '}}((x^1_{-m'-1},\ldots ,\dots ,x^1_{\ell '+1})) \end{aligned}$$
2.
$\underline{Predicate\, {\mathcal {I}}(m<{\hat{m}},m'<{\hat{m}},\ell '\ge {\hat{\ell }})}$, defined as
$$\begin{aligned} &{\mathcal {I}}(m<{\hat{m}},m'<{\hat{m}},\ell '\ge {\hat{\ell }}, \text {right}\,\text {finite})\\ & \vee {\mathcal {I}}(m<{\hat{m}},m'<{\hat{m}},\ell '\ge {\hat{\ell }}, \text {right}\,\text {induction}) \end{aligned}$$

with ${\mathcal {I}}(m<{\hat{m}},m'<{\hat{m}},\ell '\ge {\hat{\ell }}, \text {right}\,\text {finite})$ defined as

$\forall m< {\hat{m}}, m' < {\hat{m}} : \exists (x^2_{-\max \{m,m'\}-1},\ldots ,x^2_0,\ldots ,x^2_{{\hat{\ell }}})$:

$$\begin{aligned}&f^{{-m}\rightarrow {0}\leftarrow {0}}((x^2_{-m-1},\ldots ,x^2_1)) \\&\quad = {\texttt{1}}-f^{{-m'}\rightarrow {0}\leftarrow {{\hat{\ell }}}}((x^2_{-m'-1},\ldots ,x^2_{{\hat{\ell }}},{\texttt{0}}))\\&\quad = {\texttt{1}}-f^{{-m'}\rightarrow {0}\leftarrow {{\hat{\ell }}}}((x^2_{-m'-1},\ldots ,x^2_{{\hat{\ell }}},{\texttt{1}})) \end{aligned}$$

and ${\mathcal {I}}(m<{\hat{m}},m'<{\hat{m}},\ell '\ge {\hat{\ell }},\text {right}\,\text {induction})$ defined as

$$\begin{aligned}&{\mathcal {I}}(m<{\hat{m}},m'<{\hat{m}},\ell '\ge {\hat{\ell }}, \text {right}\,\text {induction}, {\textcircled {3}})\\&\quad \wedge {\mathcal {I}}(m<{\hat{m}},m'<{\hat{m}},\ell '\ge {\hat{\ell }}, \text {right}\,\text {induction}, {\textcircled {2}})\\&\quad \wedge {\mathcal {I}}(m<{\hat{m}},m'<{\hat{m}},\ell '\ge {\hat{\ell }}, \text{right}\,\text {induction}, {\textcircled {1}}) \end{aligned}$$

where

$$\begin{aligned} {\textcircled {3}}\,&\,\text { is } \max \{m,m'\}+\ell '=n\\ {\textcircled {2}}\,&\,\text { is } \max \{m,m'\}+\ell '=n-1\\ {\textcircled {1}}\,&\,\text { is } \max \{m,m'\}+\ell '=n-2 \end{aligned}$$

with ${\mathcal {I}}(m<{\hat{m}},m'<{\hat{m}},\ell '\ge {\hat{\ell }}, \text {right}\,\text {induction},{\textcircled {3}})$ defined as (where ${\textcircled {3}}$ is $\max \{m,m'\}+\ell '=n$) $\forall m< {\hat{m}}, m' < {\hat{m}} : \exists (x^2_{-\max \{m,m'\}-1},\ldots ,x^2_0,\ldots ,x^2_{{\hat{\ell }}-1}) : \exists a,b \in \{{\texttt{0}},{\texttt{1}}\}: f(a,a,b) = b$

$$\begin{aligned}&f^{{-m}\rightarrow {0}\leftarrow {0}}((x^2_{-m-1},\ldots ,x^2_1)) \\&\quad = {\texttt{1}}-f^{{-m'}\rightarrow {0}\leftarrow {{\hat{\ell }}}}((x^2_{-m'-1},\ldots ,x^2_{{\hat{\ell }}-1},a,b))\\&x^2_{-\max \{m,m'\}-1} = a\\&x^2_{-\max \{m,m'\}} = a\\&x^2_{-\max \{m,m'\}+1} = b \end{aligned}$$

and ${\mathcal {I}}(m<{\hat{m}},m'<{\hat{m}},\ell '\ge {\hat{\ell }}, \text {right}\,\text {induction}, {\textcircled {2}})$ defined as (where ${\textcircled {2}}$ is $\max \{m,m'\}+\ell '=n-1$) $\forall m< {\hat{m}}, m' < {\hat{m}} : \exists (x^2_{-\max \{m,m'\}-1},\ldots ,x^2_0,\ldots ,x^2_{{\hat{\ell }}-1}) : \exists a,b \in \{{\texttt{0}},{\texttt{1}}\}: f(a,a,b) = b$

$$\begin{aligned}&f^{{-m}\rightarrow {0}\leftarrow {0}}((x^2_{-m-1},\ldots ,x^2_1)) \\ &\quad = {\texttt{1}}-f^{{-m'}\rightarrow {0}\leftarrow {{\hat{\ell }}}}((x^2_{-m'-1}, \dots ,x^2_{{\hat{\ell }}-1},a,b))\\ &x^2_{-\max \{m,m'\}-1} = a\\ &x^2_{-\max \{m,m'\}} = b \end{aligned}$$

and ${\mathcal {I}}(m<{\hat{m}},m'<{\hat{m}},\ell '\ge {\hat{\ell }}, \text {right}\,\text {induction},{\textcircled {1}})$ defined as (where ${\textcircled {1}}$ is $\max \{m,m'\}+\ell '=n-2$) $\forall m< {\hat{m}}, m' < {\hat{m}} : \exists (x^2_{-\max \{m,m'\}-1},\ldots ,x^2_0,\ldots ,x^2_{{\hat{\ell }}-1}) : \exists a,b \in \{{\texttt{0}},{\texttt{1}}\}: f(a,a,b) = b$

$$\begin{aligned}&f^{{-m}\rightarrow {0}\leftarrow {0}}((x^2_{-m-1},\ldots ,x^2_1)) \\&\quad = {\texttt{1}}-f^{{-m'}\rightarrow {0}\leftarrow {{\hat{\ell }}}}((x^2_{-m'-1}, \dots ,x^2_{{\hat{\ell }}-1},a,b))\\&x^2_{-\max \{m,m'\}-1} = b \end{aligned}$$

3.
$\underline{Predicate \,{\mathcal {I}}(m<{\hat{m}},m'\ge {\hat{m}},\ell '<{\hat{\ell }})}$, defined as
$$\begin{aligned}&{\mathcal {I}}(m<{\hat{m}},m'\ge {\hat{m}},\ell '<{\hat{\ell }},\text {left finite})\\&\quad \vee {\mathcal {I}}(m<{\hat{m}},m'\ge {\hat{m}},\ell '<{\hat{\ell }},\text {left}\,\text {induction}) \end{aligned}$$

with ${\mathcal {I}}(m<{\hat{m}},m'\ge {\hat{m}},\ell '<{\hat{\ell }},\text {left finite})$ defined as

$\forall m< {\hat{m}}, 1 \le \ell ' < {\hat{\ell }} : \exists (x^3_{-{\hat{m}}},\ldots ,x^3_0,\ldots ,x^3_{\ell '+1}):$

$$\begin{aligned}&f^{{-m}\rightarrow {0}\leftarrow {0}}((x^3_{-m-1},\ldots ,x^3_1)) \\&\quad = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {\ell '}}(({\texttt{0}},x^3_{-{\hat{m}}},\ldots ,x^3_{\ell '+1}))\\&\quad = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {\ell '}}(({\texttt{1}},x^3_{-{\hat{m}}},\ldots ,x^3_{\ell '+1})) \end{aligned}$$

and ${\mathcal {I}}(m<{\hat{m}},m'\ge {\hat{m}},\ell '<{\hat{\ell }},\text {left}\,\text {induction})$defined as

$$\begin{aligned}&{\mathcal {I}}(m<{\hat{m}},m'\ge {\hat{m}},\ell '<{\hat{\ell }}, \text {left}\,\text {induction}, {\textcircled {3}})\\&\quad \wedge {\mathcal {I}}(m<{\hat{m}},m'\ge {\hat{m}},\ell '<{\hat{\ell }}, \text {left}\,\text {induction}, {\textcircled {2}})\\&\quad \wedge {\mathcal {I}}(m<{\hat{m}},m'\ge {\hat{m}},\ell '<{\hat{\ell }}, \text {left}\,\text {induction}, {\textcircled {1}}) \end{aligned}$$

where

$$\begin{aligned} {\textcircled {3}}&\,\text { is } m'+\ell '=n\\ {\textcircled {2}}&\,\text { is } m'+\ell '=n-1\\ {\textcircled {1}}&\,\text { is } m'+\ell '=n-2 \end{aligned}$$

with ${\mathcal {I}}(m<{\hat{m}},m'\ge {\hat{m}},\ell '<{\hat{\ell }}, \text {left}\,\text {induction}, {\textcircled {3}})$defined as (where ${\textcircled {3}}$ is $m'+\ell '=n$) $\forall m< {\hat{m}}, 1 \le \ell ' < {\hat{\ell }} : \exists (x^3_{-{\hat{m}}+1},\ldots ,x^3_0,\ldots ,x^3_{\ell '+1}) : \exists a,b \in \{{\texttt{0}},{\texttt{1}}\}: f(b,a,a) = a$

$$\begin{aligned}&f^{{-m}\rightarrow {0}\leftarrow {0}}((x^3_{-m-1},\ldots ,x^3_1)) \\&\quad = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {\ell '}}((b,a,x^3_{-{\hat{m}}+1},\ldots ,x^3_{\ell '+1}))\\&\qquad (\text {if } m={\hat{m}}-1 \text { then } x^3_{-m-1}=x^3_{-{\hat{m}}}=a)\\&x^3_{\ell '+1} = a\\&x^3_{\ell '} = a\\&x^3_{\ell '-1} = b \end{aligned}$$

and ${\mathcal {I}}(m<{\hat{m}},m'\ge {\hat{m}},\ell '<{\hat{\ell }}, \text {left}\,\text {induction}, {\textcircled {2}})$ defined as (where ${\textcircled {2}}$ is $m'+\ell '=n-1$) $\forall m< {\hat{m}}, 1 \le \ell ' < {\hat{\ell }}: \exists (x^3_{-{\hat{m}}+1},\ldots ,x^3_0,\ldots ,x^3_{\ell '+1}) : \exists a,b \in \{{\texttt{0}},{\texttt{1}}\}: f(b,a,a) = a$

$$\begin{aligned}&&f^{{-m}\rightarrow {0}\leftarrow {0}}((x^3_{-m-1},\ldots ,x^3_1)) \\&\quad = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {\ell '}}((b,a,x^3_{-{\hat{m}}+1}, \dots ,x^3_{\ell '+1}))\\&\qquad (\text {if } m={\hat{m}}-1 \text { then } x^3_{-m-1}=x^3_{-{\hat{m}}}=a)\\&x^3_{\ell '+1} = a\\&x^3_{\ell '} = b \end{aligned}$$

and ${\mathcal {I}}(m<{\hat{m}},m'\ge {\hat{m}},\ell '<{\hat{\ell }}, \text {left}\,\text {induction}, {\textcircled {1}})$ defined as (where ${\textcircled {1}}$ is $m'+\ell '=n-2$) $\forall m< {\hat{m}}, 1 \le \ell ' < {\hat{\ell }} : \exists (x^3_{-{\hat{m}}+1},\ldots ,x^3_0,\ldots ,x^3_{\ell '+1}) : \exists a,b \in \{{\texttt{0}},{\texttt{1}}\}:$

$$\begin{aligned}&f(b,a,a) = a\\&f^{{-m}\rightarrow {0}\leftarrow {0}}((x^3_{-m-1},\ldots ,x^3_1)) \\&\quad = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {\ell '}}((b,a,x^3_{-{\hat{m}}+1},\ldots ,x^3_{\ell '+1}))\\&\qquad (\text {if } m={\hat{m}}-1 \text { then } x^3_{-m-1}=x^3_{-{\hat{m}}}=a)\\&x^3_{\ell '+1} = b \end{aligned}$$

4.
$\underline{Predicate \, {\mathcal {I}}(m<{\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }})}$, defined as
$$\begin{aligned}&{\mathcal {I}}(m<{\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }},\text {left finite}, \text {right}\,\text {finite})\\&\quad \vee {\mathcal {I}}(m<{\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }},\text {left finite}, \text {right}\,\text {induction})\\&\quad \vee {\mathcal {I}}(m<{\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right finite})\\&\quad \vee {\mathcal {I}}(m<{\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right}\,\text {induction}) \end{aligned}$$

with ${\mathcal {I}}(m<{\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }},\text {left finite}, \text {right}\,\text {finite})$ defined as

$\forall m < {\hat{m}} : \exists (x^4_{-{\hat{m}}},\ldots ,x^4_0,\ldots ,x^4_{{\hat{\ell }}}):$

$$\begin{aligned}&f^{{-m}\rightarrow {0}\leftarrow {0}}((x^4_{-m-1},\ldots ,x^4_1)) \\&\quad = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {{\hat{\ell }}}}(({\texttt{0}},x^4_{-{\hat{m}}}, \dots ,x^4_{{\hat{\ell }}},{\texttt{0}}))\\&\quad = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {{\hat{\ell }}}}(({\texttt{1}},x^4_{-{\hat{m}}}, \dots ,x^4_{{\hat{\ell }}},{\texttt{0}}))\\&\quad = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {{\hat{\ell }}}}(({\texttt{0}},x^4_{-{\hat{m}}}, \dots ,x^4_{{\hat{\ell }}},{\texttt{1}}))\\&\quad = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {{\hat{\ell }}}}(({\texttt{1}},x^4_{-{\hat{m}}}, \dots ,x^4_{{\hat{\ell }}},{\texttt{1}})) \end{aligned}$$

and${\mathcal {I}}(m<{\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }},\text {left finite}, \text {right}\,\text {induction})$defined as

$$\begin{aligned}&{\mathcal {I}}(m<{\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }},\text {left finite}, \text {right}\,\text {induction},{\textcircled {2}})\\&\quad \wedge {\mathcal {I}}(m<{\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }},\text {left finite}, \text{right}\,\text {induction}, {\textcircled {1}}) \end{aligned}$$

where

$$\begin{aligned}&{\textcircled {2}}\text { is } m'+\ell '=n \wedge m'={\hat{m}}\\&{\textcircled {1}}\text { is } (m'+\ell '=n-1 \wedge m'={\hat{m}}) \\&\quad \vee (m'+\ell '=n \wedge m'={\hat{m}}+1) \end{aligned}$$

with ${\mathcal {I}}(m<{\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }},\text {left finite}, \text {right}\,\text {induction}, {\textcircled {2}})$ defined as (where ${\textcircled {2}}$ is $m'+\ell '=n \wedge m'={\hat{m}}$) $\forall m < {\hat{m}} : \exists (x^4_{-{\hat{m}}},\ldots ,x^4_0,\ldots ,x^4_{{\hat{\ell }}-1}) : \exists a,b \in \{{\texttt{0}},{\texttt{1}}\}: f(a,a,b) = b$

$$\begin{aligned}&f^{{-m}\rightarrow {0}\leftarrow {0}}((x^4_{-m-1},\ldots ,x^4_1)) \\&\quad = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {{\hat{\ell }}}}(({\texttt{0}},x^4_{-{\hat{m}}}, \dots ,x^4_{{\hat{\ell }}-1},a,b))\\&\quad = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {{\hat{\ell }}}}(({\texttt{1}},x^4_{-{\hat{m}}}, \dots ,x^4_{{\hat{\ell }}-1},a,b))\\&x^4_{-{\hat{m}}} = a\\&x^4_{-{\hat{m}}+1} = b \end{aligned}$$

and ${\mathcal {I}}(m<{\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }},\text {left finite}, \text {right}\,\text {induction},{\textcircled {1}})$ defined as (where ${\textcircled {1}}$ is $(m'+\ell '=n-1 \wedge m'={\hat{m}}) \vee (m'+\ell '=n \wedge m'={\hat{m}}+1)$) $\forall m < {\hat{m}} : \exists (x^4_{-{\hat{m}}},\ldots ,x^4_0,\ldots ,x^4_{{\hat{\ell }}-1}) : \exists a,b \in \{{\texttt{0}},{\texttt{1}}\}: f(a,a,b) = b$

$$\begin{aligned}&f^{{-m}\rightarrow {0}\leftarrow {0}}((x^4_{-m-1},\ldots ,x^4_1)) \\&\quad = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {{\hat{\ell }}}}(({\texttt{0}},x^4_{-{\hat{m}}}, \dots ,x^4_{{\hat{\ell }}-1},a,b))\\&\quad = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {{\hat{\ell }}}}(({\texttt{1}},x^4_{-{\hat{m}}}, \dots ,x^4_{{\hat{\ell }}-1},a,b))\\&x^4_{-{\hat{m}}} = b \end{aligned}$$

and${\mathcal {I}}(m<{\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right finite})$defined as

$$\begin{aligned}&{\mathcal {I}}(m<{\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right finite},{\textcircled {2}})\\&\quad \wedge {\mathcal {I}}(m<{\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right finite},{\textcircled {1}}) \end{aligned}$$

where

$$\begin{aligned} {\textcircled {2}}&\,\text { is } m'+\ell '=n \wedge \ell '={\hat{\ell }}\\ {\textcircled {1}}&\,\text { is } (m'+\ell '=n-1 \wedge \ell '={\hat{\ell }}) \vee (m'+\ell '=n \wedge \ell '={\hat{\ell }}+1) \end{aligned}$$

with ${\mathcal {I}}(m<{\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right finite},{\textcircled {2}})$ defined as (where ${\textcircled {2}}$ is $m'+\ell '=n \wedge \ell '={\hat{\ell }}$)

$\forall m < {\hat{m}} : \exists (x^4_{-{\hat{m}}+1},\ldots ,x^4_0,\ldots ,x^4_{{\hat{\ell }}}) : \exists a,b \in \{{\texttt{0}},{\texttt{1}}\}:$

$$\begin{aligned}&f(b,a,a) = b\\&f^{{-m}\rightarrow {0}\leftarrow {0}}((x^4_{-m-1},\ldots ,x^4_1)) \\&\quad = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {{\hat{\ell }}}}((b,a,x^4_{-{\hat{m}}+1}, \dots ,x^4_{{\hat{\ell }}},{\texttt{0}}))\\&\quad = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {{\hat{\ell }}}}((b,a,x^4_{-{\hat{m}}+1}, \dots ,x^4_{{\hat{\ell }}},{\texttt{1}}))\\&\qquad (\text {if } m={\hat{m}}-1 \text { then } x^4_{-m-1}=x^4_{-{\hat{m}}}=a)\\&x^4_{{\hat{\ell }}} = a\\&x^4_{{\hat{\ell }}-1} = b \end{aligned}$$

and ${\mathcal {I}}(m<{\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right finite},{\textcircled {1}})$ defined as (where ${\textcircled {1}}$ is $(m'+\ell '=n-1 \wedge \ell '={\hat{\ell }}) \vee (m'+\ell '=n \wedge \ell '={\hat{\ell }}+1)$)

$\forall m < {\hat{m}} : \exists (x^4_{-{\hat{m}}+1},\ldots ,x^4_0,\ldots ,x^4_{{\hat{\ell }}}) : \exists a,b \in \{{\texttt{0}},{\texttt{1}}\}:$

$$\begin{aligned}&f(b,a,a) = b\\&f^{{-m}\rightarrow {0}\leftarrow {0}}((x^4_{-m-1},\ldots ,x^4_1)) \\&\quad = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {{\hat{\ell }}}}((b,a,x^4_{-{\hat{m}}+1}, \dots ,x^4_{{\hat{\ell }}},{\texttt{0}}))\\&\quad = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {{\hat{\ell }}}}((b,a,x^4_{-{\hat{m}}+1}, \dots ,x^4_{{\hat{\ell }}},{\texttt{1}}))\\&(\text {if } m={\hat{m}}-1 \text { then } x^4_{-m-1}=x^4_{-{\hat{m}}}=a)\\&x^4_{{\hat{\ell }}} = b \end{aligned}$$

and${\mathcal {I}}(m<{\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right}\,\text {induction})$defined as

$$\begin{aligned}&{\mathcal {I}}(m<{\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right}\,\text {induction},{\textcircled {2}})\\&\quad \wedge {\mathcal {I}}(m<{\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right}\,\text {induction},{\textcircled {1}}) \end{aligned}$$

where

$$\begin{aligned} {\textcircled {2}}&\,\text { is } m'+\ell '=n \wedge m'={\hat{m}}\\ {\textcircled {1}}&\,\text { is } m'+\ell '=n \wedge \ell '={\hat{\ell }} \end{aligned}$$

with ${\mathcal {I}}(m<{\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right}\,\text {induction},{\textcircled {2}})$defined as (where ${\textcircled {2}}$ is $m'+\ell '=n \wedge m'={\hat{m}}$) $\forall m < {\hat{m}} : \exists (x^4_{-{\hat{m}}+1},\ldots ,x^4_0,\ldots ,x^4_{{\hat{\ell }}-1}) : \exists a \in \{{\texttt{0}},{\texttt{1}}\}: f(a,a,a) = a$

$$\begin{aligned}&f^{{-m}\rightarrow {0}\leftarrow {0}}((x^4_{-m-1},\ldots ,x^4_1)) \\&\quad = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {{\hat{\ell }}}}((a,a,x^4_{-{\hat{m}}+1}, \dots ,x^4_{{\hat{\ell }}-1},a,a))\\&(\text {if } m={\hat{m}}-1 \text { then } x^4_{-m-1}=x^4_{-{\hat{m}}}=a)\\&x^4_{-{\hat{m}}+1} = a \end{aligned}$$

and ${\mathcal {I}}(m<{\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right}\,\text {induction},{\textcircled {1}})$ defined as (where ${\textcircled {1}}$ is $m'+\ell '=n \wedge \ell '={\hat{\ell }}$) $\forall m < {\hat{m}} : \exists (x^4_{-{\hat{m}}+1},\ldots ,x^4_0,\ldots ,x^4_{{\hat{\ell }}-1}) : \exists a \in \{{\texttt{0}},{\texttt{1}}\}: f(a,a,a) = a$

$$\begin{aligned}&f^{{-m}\rightarrow {0}\leftarrow {0}}((x^4_{-m-1},\ldots ,x^4_1)) \\&\quad = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {{\hat{\ell }}}}((a,a,x^4_{-{\hat{m}}+1}, \dots ,x^4_{{\hat{\ell }}-1},a,a))\\&\qquad (\text {if } m={\hat{m}}-1 \text { then } x^4_{-m-1}=x^4_{-{\hat{m}}}=a)\\&x^4_{{\hat{\ell }}-1} = a \end{aligned}$$

5.
$\underline{Predicate \, {\mathcal {I}}(m\ge {\hat{m}},m'<{\hat{m}},\ell '<{\hat{\ell }})}$, defined as
$$\begin{aligned}&{\mathcal {I}}(m\ge {\hat{m}},m'<{\hat{m}},\ell '<{\hat{\ell }},\text {left finite})\\&\quad \vee {\mathcal {I}}(m\ge {\hat{m}},m'<{\hat{m}},\ell '<{\hat{\ell }},\text {left}\,\text {induction}) \end{aligned}$$

with ${\mathcal {I}}(m\ge {\hat{m}},m'<{\hat{m}},\ell '<{\hat{\ell }},\text {left finite})$ defined as$\forall m'< {\hat{m}}, 1 \le \ell ' < {\hat{\ell }} : \exists (x^5_{-{\hat{m}}},\ldots ,x^5_0,\ldots ,x^5_{\ell '+1})$:

$$\begin{aligned}&f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {0}}(({\texttt{0}},x^5_{-{\hat{m}}},\ldots ,x^5_1)) \\&\quad =f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {0}}(({\texttt{1}},x^5_{-{\hat{m}}},\ldots ,x^5_1)) \\&\quad = {\texttt{1}}-f^{{-m'}\rightarrow {0}\leftarrow {\ell '}}((x^5_{-m'-1},\ldots ,x^5_{\ell '+1})) \end{aligned}$$

and${\mathcal {I}}(m\ge {\hat{m}},m'<{\hat{m}},\ell '<{\hat{\ell }},\text {left}\,\text {induction})$defined as

$$\begin{aligned}&{\mathcal {I}}(m\ge {\hat{m}},m'<{\hat{m}},\ell '<{\hat{\ell }}, \text {left}\,\text {induction}, {\textcircled {3}})\\&\quad \wedge {\mathcal {I}}(m\ge {\hat{m}},m'<{\hat{m}},\ell '<{\hat{\ell }}, \text {left}\,\text {induction}, {\textcircled {2}})\\&\quad \wedge {\mathcal {I}}(m\ge {\hat{m}},m'<{\hat{m}},\ell '<{\hat{\ell }}, \text {left}\,\text {induction}, {\textcircled {1}}) \end{aligned}$$

where

$$\begin{aligned} {\textcircled {3}}&\,\text { is } m+\ell '=n\\ {\textcircled {2}}&\,\text { is } m+\ell '=n-1\\ {\textcircled {1}}&\,\text { is } m+\ell '=n-2 \end{aligned}$$

with ${\mathcal {I}}(m\ge {\hat{m}},m'<{\hat{m}},\ell '<{\hat{\ell }}, \text {left}\,\text {induction}, {\textcircled {3}})$defined as (where ${\textcircled {3}}$ is $m+\ell '=n$) $\forall m'< {\hat{m}}, 1 \le \ell ' < {\hat{\ell }} : \exists (x^5_{-{\hat{m}}+1},\ldots ,x^5_0,\ldots ,x^5_{\ell '+1}) : \exists a,b \in \{{\texttt{0}},{\texttt{1}}\}: f(b,a,a) = b$

$$\begin{aligned}&f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {0}}((b,a,x^5_{-{\hat{m}}+1},\ldots ,x^5_1)) \\&\quad = {\texttt{1}}-f^{{-m'}\rightarrow {0}\leftarrow {\ell '}}((x^5_{-m'-1},\ldots ,x^5_{\ell '+1}))\\&\qquad (\text {if } m'={\hat{m}}-1 \text { then } x^5_{-m'-1}=x^5_{-{\hat{m}}}=a)\\&x^5_{\ell '+1} = a\\&x^5_{\ell '} = a\\&x^5_{\ell '-1} = b \end{aligned}$$

and ${\mathcal {I}}(m\ge {\hat{m}},m'<{\hat{m}},\ell '<{\hat{\ell }}, \text {left}\,\text {induction}, {\textcircled {2}})$defined as (where ${\textcircled {2}}$ is $m+\ell '=n-1$) $\forall m'< {\hat{m}}, 1 \le \ell ' < {\hat{\ell }} : \exists (x^5_{-{\hat{m}}+1},\ldots ,x^5_0,\ldots ,x^5_{\ell '+1}) : \exists a,b \in \{{\texttt{0}},{\texttt{1}}\}: f(b,a,a) = b$

$$\begin{aligned}&f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {0}}((b,a,x^5_{-{\hat{m}}+1},\ldots ,x^5_1)) \\&\quad = {\texttt{1}}-f^{{-m'}\rightarrow {0}\leftarrow {\ell '}}((x^5_{-m'-1},\ldots ,x^5_{\ell '+1}))\\&\qquad (\text {if } m'={\hat{m}}-1 \text { then } x^5_{-m'-1}=x^5_{-{\hat{m}}}=a)\\&x^5_{\ell '+1} = a\\&x^5_{\ell '} = b \end{aligned}$$

and ${\mathcal {I}}(m\ge {\hat{m}},m'<{\hat{m}},\ell '<{\hat{\ell }}, \text {left}\,\text {induction}, {\textcircled {1}})$defined as (where ${\textcircled {1}}$ is $m+\ell '=n-2$) $\forall m'< {\hat{m}}, 1 \le \ell ' < {\hat{\ell }} : \exists (x^5_{-{\hat{m}}+1},\ldots ,x^5_0,\ldots ,x^5_{\ell '+1}) : \exists a,b \in \{{\texttt{0}},{\texttt{1}}\}: f(b,a,a) = b$

$$\begin{aligned}&f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {0}}((b,a,x^5_{-{\hat{m}}+1},\ldots ,x^5_1)) \\&\quad = {\texttt{1}}-f^{{-m'}\rightarrow {0}\leftarrow {\ell '}}((x^5_{-m'-1},\ldots ,x^5_{\ell '+1}))\\&\qquad (\text {if } m'={\hat{m}}-1 \text { then } x^5_{-m'-1}=x^5_{-{\hat{m}}}=a)\\&x^5_{\ell '+1} = b \end{aligned}$$

6.
$\underline{Predicate \, {\mathcal {I}}(m\ge {\hat{m}},m'<{\hat{m}},\ell '\ge {\hat{\ell }})}$, defined as
$$\begin{aligned}&{\mathcal {I}}(m\ge {\hat{m}},m'<{\hat{m}},\ell '\ge {\hat{\ell }},\text {left finite}, \text {right}\,\text {finite})\\&\quad \vee {\mathcal {I}}(m\ge {\hat{m}},m'<{\hat{m}},\ell '\ge {\hat{\ell }},\text {left finite}, \text {right}\,\text {induction})\\&\quad \vee {\mathcal {I}}(m\ge {\hat{m}},m'<{\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right finite})\\&\quad \vee {\mathcal {I}}(m\ge {\hat{m}},m'<{\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right}\,\text {induction}) \end{aligned}$$

with${\mathcal {I}}(m\ge {\hat{m}},m'<{\hat{m}},\ell '\ge {\hat{\ell }},\text {left finite}, \text {right}\,\text {finite})$defined as

$\forall m' < {\hat{m}} : \exists (x^6_{-{\hat{m}}},\ldots ,x^6_0,\ldots ,x^6_{{\hat{\ell }}}):$

$$\begin{aligned}&f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {0}}(({\texttt{0}},x^6_{-{\hat{m}}},\ldots ,x^6_1)) \\&\quad =f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {0}}(({\texttt{1}},x^6_{-{\hat{m}}},\ldots ,x^6_1)) \\&\quad = {\texttt{1}}-f^{{-m'}\rightarrow {0}\leftarrow {{\hat{\ell }}}}((x^6_{-m'-1}, \dots ,x^6_{{\hat{\ell }}},{\texttt{0}}))\\&\quad = {\texttt{1}}-f^{{-m'}\rightarrow {0}\leftarrow {{\hat{\ell }}}}((x^6_{-m'-1},\ldots ,x^6_{{\hat{\ell }}},{\texttt{1}})) \end{aligned}$$

and${\mathcal {I}}(m\ge {\hat{m}},m'<{\hat{m}},\ell '\ge {\hat{\ell }},\text {left finite}, \text {right}\,\text {induction})$defined as

$$\begin{aligned}&{\mathcal {I}}(m\ge {\hat{m}},m'<{\hat{m}},\ell '\ge {\hat{\ell }},\text {left finite}, \text {right}\,\text {induction},{\textcircled {2}})\\&\quad \wedge {\mathcal {I}}(m\ge {\hat{m}},m'<{\hat{m}},\ell '\ge {\hat{\ell }},\text {left finite}, \text {right}\,\text {induction}, {\textcircled {1}}) \end{aligned}$$

where

$$\begin{aligned} {\textcircled {2}}&\,\text { is } m+\ell '=n \wedge m={\hat{m}}\\ {\textcircled {1}}&\,\text { is } (m+\ell '=n-1 \wedge m={\hat{m}}) \vee (m+\ell '=n \wedge m={\hat{m}}+1) \end{aligned}$$

with ${\mathcal {I}}(m\ge {\hat{m}},m'<{\hat{m}},\ell '\ge {\hat{\ell }},\text {left finite}, \text {right}\,\text {induction},{\textcircled {2}})$defined as (where ${\textcircled {2}}$ is $m+\ell '=n \wedge m={\hat{m}}$) $\forall m' < {\hat{m}} : \exists (x^6_{-{\hat{m}}},\ldots ,x^6_0,\ldots ,x^6_{{\hat{\ell }}-1}) : \exists a,b \in \{{\texttt{0}},{\texttt{1}}\}: f(a,a,b) = b$

$$\begin{aligned}&f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {0}}(({\texttt{0}},x^6_{-{\hat{m}}},\ldots ,x^6_1)) \\&\quad =f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {0}}(({\texttt{1}},x^6_{-{\hat{m}}},\ldots ,x^6_1)) \\&\quad = {\texttt{1}}-f^{{-m'}\rightarrow {0}\leftarrow {{\hat{\ell }}}}((x^6_{-m'-1},\ldots ,x^6_{{\hat{\ell }}-1},a,b))\\&x^6_{-{\hat{m}}} = a\\&x^6_{-{\hat{m}}+1} = b \end{aligned}$$

and ${\mathcal {I}}(m\ge {\hat{m}},m'<{\hat{m}},\ell '\ge {\hat{\ell }},\text {left finite}, \text {right}\,\text {induction}, {\textcircled {1}})$defined as (where ${\textcircled {1}}$ is $(m+\ell '=n-1 \wedge m={\hat{m}}$)

$\forall m' < {\hat{m}} : \exists (x^6_{-{\hat{m}}},\ldots ,x^6_0,\ldots ,x^6_{{\hat{\ell }}-1}) : \exists a,b \in \{{\texttt{0}},{\texttt{1}}\}:$

$$\begin{aligned}&f(a,a,b) = b\\&f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {0}}(({\texttt{0}},x^6_{-{\hat{m}}},\ldots ,x^6_1)) \\&\quad = f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {0}}(({\texttt{1}},x^6_{-{\hat{m}}},\ldots ,x^6_1)) \\&\quad = {\texttt{1}}-f^{{-m'}\rightarrow {0}\leftarrow {{\hat{\ell }}}}((x^6_{-m'-1},\ldots ,x^6_{{\hat{\ell }}-1},a,b))\\&x^6_{-{\hat{m}}} = b \end{aligned}$$

and${\mathcal {I}}(m\ge {\hat{m}},m'<{\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right finite})$ defined as

$$\begin{aligned}&{\mathcal {I}}(m\ge {\hat{m}},m'<{\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right finite},{\textcircled {2}})\\&\quad \wedge {\mathcal {I}}(m\ge {\hat{m}},m'<{\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right finite},{\textcircled {1}}) \end{aligned}$$

where

$$\begin{aligned} {\textcircled {2}}&\,\text { is } m+\ell '=n \wedge \ell '={\hat{\ell }}\\ {\textcircled {1}}&\,\text { is } (m+\ell '=n-1 \wedge \ell '={\hat{\ell }}) \vee (m+\ell '=n \wedge \ell '={\hat{\ell }}+1) \end{aligned}$$

with${\mathcal {I}}(m\ge {\hat{m}},m'<{\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right finite},{\textcircled {2}})$defined as (where ${\textcircled {2}}$ is $m+\ell '=n \wedge \ell '={\hat{\ell }}$) $\forall m' < {\hat{m}} : \exists (x^6_{-{\hat{m}}+1},\ldots ,x^6_0,\ldots ,x^6_{{\hat{\ell }}}) : \exists a,b \in \{{\texttt{0}},{\texttt{1}}\}: f(b,a,a) = b$

$$\begin{aligned}&f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {0}}((b,a,x^6_{-{\hat{m}}+1},\ldots ,x^6_1)) \\&\quad = {\texttt{1}}-f^{{-m'}\rightarrow {0}\leftarrow {{\hat{\ell }}}}((x^6_{-m'-1},\ldots ,x^6_{{\hat{\ell }}},{\texttt{0}}))\\&\quad = {\texttt{1}}-f^{{-m'}\rightarrow {0}\leftarrow {{\hat{\ell }}}}((x^6_{-m'-1},\ldots , x^6_{{\hat{\ell }}},{\texttt{1}}))\\&\qquad (\text {if } m'={\hat{m}}-1 \text { then } x^6_{-m'-1}=x^6_{-{\hat{m}}}=a)\\&x^6_{{\hat{\ell }}} = a\\&x^6_{{\hat{\ell }}-1} = b \end{aligned}$$

and ${\mathcal {I}}(m\ge {\hat{m}},m'<{\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right finite}, {\textcircled {1}})$defined as (where ${\textcircled {1}}$ is $(m+\ell '=n-1 \wedge \ell '={\hat{\ell }}) \vee (m+\ell '=n \wedge \ell '={\hat{\ell }}+1)$)

$\forall m' < {\hat{m}} : \exists (x^6_{-{\hat{m}}+1},\ldots ,x^6_0,\ldots ,x^6_{{\hat{\ell }}}) : \exists a,b \in \{{\texttt{0}},{\texttt{1}}\}:$

$$\begin{aligned}&f(b,a,a) = b\\&f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {0}}((b,a,x^6_{-{\hat{m}}+1},\ldots ,x^6_1))\\&\quad = {\texttt{1}}-f^{{-m'}\rightarrow {0}\leftarrow {{\hat{\ell }}}}((x^6_{-m'-1},\ldots ,x^6_{{\hat{\ell }}},{\texttt{0}}))\\&\quad = {\texttt{1}}-f^{{-m'}\rightarrow {0}\leftarrow {{\hat{\ell }}}}((x^6_{-m'-1},\ldots ,x^6_{{\hat{\ell }}},{\texttt{1}}))\\&\qquad (\text {if } m'={\hat{m}}-1 \text { then } x^6_{-m'-1}=x^6_{-{\hat{m}}}=a)\\&x^6_{{\hat{\ell }}} = b \end{aligned}$$

and${\mathcal {I}}(m\ge {\hat{m}},m'<{\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right}\,\text {induction})$defined as

$$\begin{aligned}&{\mathcal {I}}(m\ge {\hat{m}},m'<{\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right}\,\text {induction}, {\textcircled {2}})\\&\quad \wedge {\mathcal {I}}(m\ge {\hat{m}},m'<{\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right}\,\text {induction}, {\textcircled {1}}) \end{aligned}$$

where

$$\begin{aligned} {\textcircled {2}}&\,\text { is } m+\ell '=n \wedge m={\hat{m}}\\ {\textcircled {1}}&\,\text { is } m+\ell '=n \wedge \ell '={\hat{\ell }} \end{aligned}$$

with${\mathcal {I}}(m\ge {\hat{m}},m'<{\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right}\,\text {induction}, {\textcircled {2}})$defined as (where${\textcircled {2}}$ is $m+\ell '=n \wedge m={\hat{m}}$) $\forall m' < {\hat{m}} : \exists (x^6_{-{\hat{m}}+1},\ldots ,x^6_0,\ldots ,x^6_{{\hat{\ell }}-1}) : \exists a \in \{{\texttt{0}},{\texttt{1}}\}: f(a,a,a) = a$

$$\begin{aligned}&f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {0}}((a,a,x^6_{-{\hat{m}}+1},\ldots ,x^6_1)) \\&\quad = {\texttt{1}}-f^{{-m'}\rightarrow {0}\leftarrow {{\hat{\ell }}}}((x^6_{-m'-1},\ldots ,x^6_{{\hat{\ell }}-1},a,a))\\&\qquad (\text {if } m'={\hat{m}}-1 \text { then } x^6_{-m'-1}=x^6_{-{\hat{m}}}=a)\\&x^6_{-{\hat{m}}+1} = a \end{aligned}$$

and${\mathcal {I}}(m\ge {\hat{m}},m'<{\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right}\,\text {induction}, {\textcircled {1}})$ defined as (where ${\textcircled {1}}$ is $m+\ell '=n \wedge \ell '={\hat{\ell }}$) $\forall m' < {\hat{m}} : \exists (x^6_{-{\hat{m}}+1},\ldots ,x^6_0,\ldots ,x^6_{{\hat{\ell }}-1}) : \exists a \in \{{\texttt{0}},{\texttt{1}}\}: f(a,a,a) = a$

$$\begin{aligned}&f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {0}}((a,a,x^6_{-{\hat{m}}+1},\ldots ,x^6_1))\\&\quad = {\texttt{1}}-f^{{-m'}\rightarrow {0}\leftarrow {{\hat{\ell }}}}((x^6_{-m'-1},\ldots ,x^6_{{\hat{\ell }}-1},a,a))\\&\qquad (\text {if } m'={\hat{m}}-1 \text { then } x^6_{-m'-1}=x^6_{-{\hat{m}}}=a)\\&x^6_{{\hat{\ell }}-1} = a \end{aligned}$$

7.
$\underline{Predicate \, {\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '<{\hat{\ell }})}$, defined as
$$\begin{aligned}&{\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '<{\hat{\ell }},\text {left finite})\\&\quad \vee {\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '<{\hat{\ell }},\text {left}\,\text {induction}) \end{aligned}$$

with ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '<{\hat{\ell }},\text {left finite})$defined as$\forall 1 \le \ell ' < {\hat{\ell }} : \exists (x^3_{-{\hat{m}}},\ldots ,x^3_0,\ldots ,x^3_{\ell '+1})$:

$$\begin{aligned}&f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {0}}((0,x^7_{-{\hat{m}}},\ldots ,x^7_1)) \\&\quad = f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {0}}((1,x^7_{-{\hat{m}}},\ldots ,x^7_1)) \\&\quad = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {\ell '}}(({\texttt{0}},x^7_{-{\hat{m}}},\ldots ,x^7_{\ell '+1}))\\&\quad = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {\ell '}}(({\texttt{1}},x^7_{-{\hat{m}}},\ldots ,x^7_{\ell '+1})) \end{aligned}$$

and ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '<{\hat{\ell }},\text {left}\,\text {induction})$ defined as

$$\begin{aligned}&{\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '<{\hat{\ell }}, \text {left}\,\text {induction}, m=m')\\&\quad \wedge {\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '<{\hat{\ell }}, \text {left}\,\text {induction}, m>m')\\&\quad \wedge {\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '<{\hat{\ell }}, \text {left}\,\text {induction}, m<m') \end{aligned}$$

with ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '<{\hat{\ell }}, \text {left}\,\text {induction}, m=m')$defined as

$$\begin{aligned}&{\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '<{\hat{\ell }}, \text {left}\,\text {induction}, m=m',{\textcircled {3}})\\&\quad \wedge {\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '<{\hat{\ell }}, \text {left}\,\text {induction}, m=m', {\textcircled {2}})\\&\quad \wedge {\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '<{\hat{\ell }}, \text {left}\,\text {induction}, m=m',{\textcircled {1}}) \end{aligned}$$

where

$$\begin{aligned} {\textcircled {3}}&\,\text { is } m+\ell '=n\\ {\textcircled {2}}&\,\text { is } m+\ell '=n-1\\ {\textcircled {1}}&\,\text { is } m+\ell '=n-2 \end{aligned}$$

with ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '<{\hat{\ell }}, \text {left}\,\text {induction}, m=m',{\textcircled {3}})$defined as (where${\textcircled {3}}$is$m+\ell '=n$) $\forall 2 \le \ell ' < {\hat{\ell }} : \exists (x^7_{-{\hat{m}}+1},\ldots ,x^7_0,\ldots ,x^7_{\ell '+1}) : \exists a,b \in \{{\texttt{0}},{\texttt{1}}\}: f(b,a,a) = b$

$$\begin{aligned}&f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {0}}((b,a,x^7_{-{\hat{m}}+1},\ldots ,x^7_1)) \\&\quad = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {\ell '}}((b,a,x^7_{-{\hat{m}}+1},\ldots ,x^7_{\ell '+1}))\\&x^7_{\ell '+1} = a\\&x^7_{\ell '} = a\\&x^7_{\ell '-1} = b \end{aligned}$$

and ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '<{\hat{\ell }}, \text {left}\,\text {induction}, m=m',{\textcircled {2}})$defined as (where ${\textcircled {2}}$ is $m+\ell '=n-1$) $\forall 1 \le \ell ' < {\hat{\ell }} : \exists (x^7_{-{\hat{m}}+1},\ldots ,x^7_0,\ldots ,x^7_{\ell '+1}) : \exists a,b \in \{{\texttt{0}},{\texttt{1}}\}: f(b,a,a) = b$

$$\begin{aligned}&f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {0}}((b,a,x^7_{-{\hat{m}}+1},\ldots ,x^7_1)) \\&\quad = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {\ell '}}((b,a,x^7_{-{\hat{m}}+1},\ldots ,x^7_{\ell '+1}))\\&x^7_{\ell '+1} = a\\&x^7_{\ell '} = b \end{aligned}$$

and ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '<{\hat{\ell }}, \text {left}\,\text {induction}, m=m',{\textcircled {1}})$ defined as (where ${\textcircled {1}}$ is $m+\ell '=n-2$) $\forall 1 \le \ell ' < {\hat{\ell }} : \exists (x^7_{-{\hat{m}}+1},\ldots ,x^7_0,\ldots ,x^7_{\ell '+1}): \exists a,b \in \{{\texttt{0}},{\texttt{1}}\}: f(b,a,a) = b$

$$\begin{aligned}&f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {0}}((b,a,x^7_{-{\hat{m}}+1},\ldots ,x^7_1)) \\&\quad = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {\ell '}}((b,a,x^7_{-{\hat{m}}+1},\ldots ,x^7_{\ell '+1}))\\&x^7_{\ell '+1} = b \end{aligned}$$

and${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '<{\hat{\ell }}, \text {left}\,\text {induction}, m>m')$defined as

$$\begin{aligned}&{\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '<{\hat{\ell }}, \text {left}\,\text {induction}, m>m',{\textcircled {3}})\\&\quad \wedge {\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '<{\hat{\ell }}, \text {left}\,\text {induction}, m>m', {\textcircled {2}})\\&\quad \wedge {\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '<{\hat{\ell }}, \text {left}\,\text {induction}, m>m',{\textcircled {1}}) \end{aligned}$$

where

$$\begin{aligned} {\textcircled {3}}&\,\text { is } m+\ell '=n\\ {\textcircled {2}}&\,\text { is } m+\ell '=n-1\\ {\textcircled {1}}&\,\text { is } m+\ell '=n-2 \end{aligned}$$

with ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '<{\hat{\ell }}, \text {left}\,\text {induction}, m>m',{\textcircled {3}})$defined as (where${\textcircled {3}}$is$m+\ell '=n$) $\forall 2 \le \ell ' < {\hat{\ell }} : \exists (x^7_{-{\hat{m}}+1},\ldots ,x^7_0,\ldots ,x^7_{\ell '+1}) : \exists a,b \in \{{\texttt{0}},{\texttt{1}}\}: f(b,a,a) = b$

$$\begin{aligned}&\left( \begin{aligned} f(a,&a,a)=a\\ f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {0}}((&b,a,x^7_{-{\hat{m}}+1},\ldots ,x^7_1))\\ = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {\ell '}}((&a,a,x^7_{-{\hat{m}}+1},\ldots ,x^7_{\ell '+1})) \end{aligned}\right) \\&\quad \vee \left( \begin{aligned} f(a,&a,a)=b\\ f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {0}}((&b,a,x^7_{-{\hat{m}}+1},\ldots ,x^7_1))\\ = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {\ell '}}((&b,a,x^7_{-{\hat{m}}+1},\ldots ,x^7_{\ell '+1})) \end{aligned}\right) \\&x^7_{\ell '+1} = a\\&x^7_{\ell '} = a\\&x^7_{\ell '-1} = b \end{aligned}$$

and ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '<{\hat{\ell }}, \text {left}\,\text {induction}, m>m',{\textcircled {2}})$defined as (where${\textcircled {2}}$ is $m+\ell '=n-1$) $\forall 1 \le \ell ' < {\hat{\ell }} : \exists (x^7_{-{\hat{m}}+1},\ldots ,x^7_0,\ldots ,x^7_{\ell '+1}): \exists a,b \in \{{\texttt{0}},{\texttt{1}}\}: f(b,a,a) = b$

$$\begin{aligned}&\left( \begin{aligned} f(a,&a,a)=a\\ f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {0}}((&b,a,x^7_{-{\hat{m}}+1},\ldots ,x^7_1))\\ = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {\ell '}}((&a,a,x^7_{-{\hat{m}}+1},\ldots ,x^7_{\ell '+1})) \end{aligned}\right) \\&\quad \vee \left( \begin{aligned} f(a,&a,a)=b\\ f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {0}}((&b,a,x^7_{-{\hat{m}}+1},\ldots ,x^7_1))\\ = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {\ell '}}((&b,a,x^7_{-{\hat{m}}+1},\ldots ,x^7_{\ell '+1})) \end{aligned}\right) \\&x^7_{\ell '+1} = a\\&x^7_{\ell '} = b \end{aligned}$$

and ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '<{\hat{\ell }}, \text {left}\,\text {induction}, m>m',{\textcircled {1}})$defined as (where${\textcircled {1}}$ is $m+\ell '=n-2$) $\forall 1 \le \ell ' < {\hat{\ell }} : \exists (x^7_{-{\hat{m}}+1},\ldots ,x^7_0,\ldots ,x^7_{\ell '+1}) : \exists a,b \in \{{\texttt{0}},{\texttt{1}}\}: f(b,a,a) = b$

$$\begin{aligned}&\left( \begin{aligned} f(a,&a,a)=a\\ f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {0}}((&b,a,x^7_{-{\hat{m}}+1},\ldots ,x^7_1))\\ = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {\ell '}}((&a,a,x^7_{-{\hat{m}}+1},\ldots ,x^7_{\ell '+1})) \end{aligned}\right) \\&\quad \vee \left( \begin{aligned} f(a,&a,a)=b\\ f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {0}}((&b,a,x^7_{-{\hat{m}}+1},\ldots ,x^7_1))\\ = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {\ell '}}((&b,a,x^7_{-{\hat{m}}+1},\ldots ,x^7_{\ell '+1})) \end{aligned}\right) \\&x^7_{\ell '+1} = b \end{aligned}$$

and ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '<{\hat{\ell }}, \text {left}\,\text {induction}, m<m')$ defined as

$$\begin{aligned}&{\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '<{\hat{\ell }}, \text {left}\,\text {induction}, m<m',{\textcircled {3}})\\&\quad \wedge {\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '<{\hat{\ell }}, \text {left}\,\text {induction}, m<m', {\textcircled {2}})\\&\quad \wedge {\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '<{\hat{\ell }}, \text {left}\,\text {induction}, m<m',{\textcircled {1}}) \end{aligned}$$

where

$$\begin{aligned} {\textcircled {3}}&\,\text { is } m'+\ell '=n\\ {\textcircled {2}}&\,\text { is } m'+\ell '=n-1\\ {\textcircled {1}}&\,\text { is } m'+\ell '=n-2 \end{aligned}$$

with ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '<{\hat{\ell }}, \text {left}\,\text {induction}, m<m',{\textcircled {3}})$ defined as (where${\textcircled {3}}$is$m'+\ell '=n$) $\forall 1 \le \ell ' < {\hat{\ell }} : \exists (x^7_{-{\hat{m}}+1},\ldots ,x^7_0,\ldots ,x^7_{\ell '+1}) : \exists a,b \in \{{\texttt{0}},{\texttt{1}}\}: f(b,a,a) = b$

$$\begin{aligned}&\left( \begin{aligned} f(a,&a,a)=a\\ f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {0}}((&a,a,x^7_{-{\hat{m}}+1},\ldots ,x^7_1))\\ = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {\ell '}}((&b,a,x^7_{-{\hat{m}}+1},\ldots ,x^7_{\ell '+1})) \end{aligned}\right) \\&\quad \vee \left( \begin{aligned} f(a,&a,a)=b\\ f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {0}}((&b,a,x^7_{-{\hat{m}}+1},\ldots ,x^7_1))\\ = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {\ell '}}((&b,a,x^7_{-{\hat{m}}+1},\ldots ,x^7_{\ell '+1})) \end{aligned}\right) \\&x^7_{\ell '+1} = a\\&x^7_{\ell '} = a\\&x^7_{\ell '-1} = b \end{aligned}$$

and ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '<{\hat{\ell }}, \text {left}\,\text {induction}, m<m',{\textcircled {2}})$defined as (where ${\textcircled {2}}$ is $m'+\ell '=n-1$) $\forall 1 \le \ell ' < {\hat{\ell }} : \exists (x^7_{-{\hat{m}}+1},\ldots ,x^7_0,\ldots ,x^7_{\ell '+1}) : \exists a,b \in \{{\texttt{0}},{\texttt{1}}\}: f(b,a,a) = b$

$$\begin{aligned}&\left( \begin{aligned} f(a,&a,a)=a\\ f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {0}}((&a,a,x^7_{-{\hat{m}}+1},\ldots ,x^7_1))\\ = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {\ell '}}((&b,a,x^7_{-{\hat{m}}+1},\ldots ,x^7_{\ell '+1})) \end{aligned}\right) \\&\quad \vee \left( \begin{aligned} f(a,&a,a)=b\\ f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {0}}((&b,a,x^7_{-{\hat{m}}+1},\ldots ,x^7_1))\\ = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {\ell '}}((&b,a,x^7_{-{\hat{m}}+1},\ldots ,x^7_{\ell '+1})) \end{aligned}\right) \\&x^7_{\ell '+1} = a\\&x^7_{\ell '} = b \end{aligned}$$

and ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '<{\hat{\ell }}, \text {left}\,\text {induction}, m<m',{\textcircled {1}})$defined as (where ${\textcircled {1}}$ is $m'+\ell '=n-2$) $\forall 1 \le \ell ' < {\hat{\ell }} : \exists (x^7_{-{\hat{m}}+1},\ldots ,x^7_0,\ldots ,x^7_{\ell '+1}) : \exists a,b \in \{{\texttt{0}},{\texttt{1}}\}: f(b,a,a) = b$

$$\begin{aligned}&\left( \begin{aligned} f(a,&a,a)=a\\ f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {0}}((&a,a,x^7_{-{\hat{m}}+1},\ldots ,x^7_1))\\ = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {\ell '}}((&b,a,x^7_{-{\hat{m}}+1},\ldots ,x^7_{\ell '+1})) \end{aligned}\right) \\&\quad \vee \left( \begin{aligned} f(a,&a,a)=b\\ f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {0}}((&b,a,x^7_{-{\hat{m}}+1},\ldots ,x^7_1))\\ = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {\ell '}}((&b,a,x^7_{-{\hat{m}}+1},\ldots ,x^7_{\ell '+1})) \end{aligned}\right) \\&x^7_{\ell '+1} = b \end{aligned}$$

8.
$\underline{Predicate \, {\mathcal {I}}(m\ge {\hat{m}}, m'\ge {\hat{m}},\ell '\ge {\hat{\ell }})}$, defined as
$$\begin{aligned}&{\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }},\text {left finite}, \text {right}\,\text {finite})\\&\quad \vee {\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }},\text {left finite},\text {right}\,\text {induction})\\&\quad \vee {\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right finite})\\&\quad \vee {\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right}\,\text {induction}) \end{aligned}$$

with ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }},\text {left finite}, \text {right}\,\text {finite})$defined as

$\exists (x^8_{-{\hat{m}}},\ldots ,x^8_0,\ldots ,x^8_{{\hat{\ell }}}):$

$$\begin{aligned}&f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {0}}(({\texttt{0}},x^8_{{\hat{m}}},\ldots ,x^8_1)) \\&\quad =f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {0}}(({\texttt{1}},x^8_{-{\hat{m}}},\ldots ,x^8_1)) \\&\quad = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {{\hat{\ell }}}}(({\texttt{0}},x^8_{-{\hat{m}}}, \dots ,x^8_{{\hat{\ell }}},{\texttt{0}}))\\&\quad = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {{\hat{\ell }}}}(({\texttt{1}},x^8_{-{\hat{m}}}, \dots ,x^8_{{\hat{\ell }}},{\texttt{0}}))\\&\quad = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {{\hat{\ell }}}}(({\texttt{0}},x^8_{-{\hat{m}}}, \dots ,x^8_{{\hat{\ell }}},{\texttt{1}}))\\&\quad = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {{\hat{\ell }}}}(({\texttt{1}},x^8_{-{\hat{m}}}, \dots ,x^8_{{\hat{\ell }}},{\texttt{1}})) \end{aligned}$$

and${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }},\text {left finite},\text {right}\,\text {induction})$defined as

$$\begin{aligned}&{\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }},\text {left finite}, \text {right}\,\text {induction}, {\textcircled {2}})\\&\quad \wedge {\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }},\text {left finite}, \text {right}\,\text {induction}, {\textcircled {1}}) \end{aligned}$$

where

$$\begin{aligned} {\textcircled {2}}&\,\text { is } \max \{m,m'\}+\ell '=n \wedge \max \{m,m'\}={\hat{m}}\\ {\textcircled {1}}& \, \text { is } \qquad (\max \{m,m'\}+\ell '=n-1 \wedge \max \{m,m'\}={\hat{m}})\\ & \quad \vee (\max \{m,m'\}+\ell '=n \wedge \max \{m,m'\}={\hat{m}}+1) \end{aligned}$$

with ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }},\text {left finite}, \text {right}\,\text {induction}, {\textcircled {2}})$defined as (where ${\textcircled {2}}$ is $\max \{m,m'\}+\ell '=n \wedge \max \{m,m'\}={\hat{m}}$) $\exists (x^8_{-{\hat{m}}},\ldots ,x^8_0,\ldots ,x^8_{{\hat{\ell }}-1}) : \exists a,b \in \{{\texttt{0}},{\texttt{1}}\}: f(a,a,b) = b$

$$\begin{aligned}&f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {0}}(({\texttt{0}},x^8_{-{\hat{m}}},\ldots ,x^8_1)) \\&\quad = f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {0}}(({\texttt{1}},x^8_{-{\hat{m}}},\ldots ,x^8_1)) \\&\quad = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {{\hat{\ell }}}}(({\texttt{0}},x^8_{-{\hat{m}}},\ldots , x^8_{{\hat{\ell }}-1},a,b))\\&\quad = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {{\hat{\ell }}}}(({\texttt{1}},x^8_{-{\hat{m}}},\ldots , x^8_{{\hat{\ell }}-1},a,b))\\&x^8_{-{\hat{m}}} = a\\&x^8_{-{\hat{m}}+1} = b \end{aligned}$$

and ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }},\text {left finite}, \text {right}\,\text {induction}, {\textcircled {1}})$ defined as (where ${\textcircled {1}}$ is $\begin{aligned} &(\max \{m,m'\}+\ell '=n-1 \wedge \max \{m,m'\}={\hat{m}}) \\ &\quad \vee (\max \{m,m'\}+\ell '=n \wedge \max \{m,m'\}={\hat{m}}+1)\end{aligned}$

$\exists (x^8_{-{\hat{m}}},\ldots ,x^8_0,\ldots ,x^8_{{\hat{\ell }}-1}) : \exists a,b \in \{{\texttt{0}},{\texttt{1}}\}:$

$$\begin{aligned}&f(a,a,b) = b\\&f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {0}}(({\texttt{0}},x^8_{-{\hat{m}}},\ldots ,x^8_1)) \\&\quad = f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {0}}(({\texttt{1}},x^8_{-{\hat{m}}},\ldots ,x^8_1)) \\&\quad = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {{\hat{\ell }}}}(({\texttt{0}},x^8_{-{\hat{m}}}, \dots ,x^8_{{\hat{\ell }}-1},a,b))\\&\quad = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {{\hat{\ell }}}}(({\texttt{1}},x^8_{-{\hat{m}}}, \dots ,x^8_{{\hat{\ell }}-1},a,b))\\&x^8_{-{\hat{m}}} = b \end{aligned}$$

and${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right finite})$defined as

$$\begin{aligned}&{\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right finite},m=m')\\&\quad \wedge {\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right}\,\text {finite},m>m')\\&\quad \wedge {\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right finite},m<m') \end{aligned}$$

with${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right finite},m=m')$defined as

$$\begin{aligned}&{\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right finite},m=m', {\textcircled {2}})\\&\quad \wedge {\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right finite},{\textcircled {1}}) \end{aligned}$$

where

$$\begin{aligned} {\textcircled {2}}&\,\text { is } m+\ell '=n \wedge \ell '={\hat{\ell }}\\ {\textcircled {1}}&\,\text { is } m=m',(m+\ell '=n-1 \wedge \ell '={\hat{\ell }}) \vee (m+\ell '=n \wedge \ell '={\hat{\ell }}+1) \end{aligned}$$

with${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right finite},m=m',{\textcircled {2}})$ defined as (where ${\textcircled {2}}$ is $m+\ell '=n \wedge \ell '={\hat{\ell }}$) $\exists (x^8_{-{\hat{m}}+1},\ldots ,x^8_0,\ldots ,x^8_{{\hat{\ell }}}) : \exists a,b \in \{{\texttt{0}},{\texttt{1}}\}: f(b,a,a) = b$

$$\begin{aligned}&f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {0}}((b,a,x^8_{-{\hat{m}}+1},\ldots ,x^8_1))\\&\quad = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {{\hat{\ell }}}}((b,a,x^8_{-{\hat{m}}+1}, \dots ,x^8_{{\hat{\ell }}},{\texttt{0}}))\\&\quad = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {{\hat{\ell }}}}((b,a,x^8_{-{\hat{m}}+1}, \dots ,x^8_{{\hat{\ell }}},{\texttt{1}}))\\&x^8_{{\hat{\ell }}} = a\\&x^8_{{\hat{\ell }}-1} = b \end{aligned}$$

and${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right finite},m=m',{\textcircled {1}})$ defined as (where ${\textcircled {1}}$ is $(m+\ell '=n-1 \wedge \ell '={\hat{\ell }}) \vee (m+\ell '=n \wedge \ell '={\hat{\ell }}+1)$) $\exists (x^8_{-{\hat{m}}+1},\ldots ,x^8_0,\ldots ,x^8_{{\hat{\ell }}}) : \exists a,b \in \{{\texttt{0}},{\texttt{1}}\}: f(b,a,a) = b$

$$\begin{aligned}&f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {0}}((b,a,x^8_{-{\hat{m}}+1},\ldots ,x^8_1))\\&\quad = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {{\hat{\ell }}}}((b,a,x^8_{-{\hat{m}}+1}, \dots ,x^8_{{\hat{\ell }}},{\texttt{0}}))\\&\quad = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {{\hat{\ell }}}}((b,a,x^8_{-{\hat{m}}+1}, \dots ,x^8_{{\hat{\ell }}},{\texttt{1}}))\\&x^8_{{\hat{\ell }}} = b \end{aligned}$$

and${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right finite},m>m')$ defined as

$$\begin{aligned}&{\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right finite},m>m', {\textcircled {2}})\\&\quad \wedge {\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right finite},m>m',{\textcircled {1}}) \end{aligned}$$

where

$$\begin{aligned} {\textcircled {2}}&\,\text { is } m+\ell '=n \wedge \ell '={\hat{\ell }}\\ {\textcircled {1}}&\,\text { is } (m+\ell '=n-1 \wedge \ell '={\hat{\ell }}) \vee (m+\ell '=n \wedge \ell '={\hat{\ell }}+1) \end{aligned}$$

with ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right}\,\text {finite},m>m',{\textcircled {2}})$ defined as (where ${\textcircled {2}}$ is $m+\ell '=n \wedge \ell '={\hat{\ell }}$) $\exists (x^8_{-{\hat{m}}+1},\ldots ,x^8_0,\ldots ,x^8_{{\hat{\ell }}}) : \exists a,b \in \{{\texttt{0}},{\texttt{1}}\}: f(b,a,a) = b$

$$\begin{aligned}&\left( \begin{aligned} f(a,&a,a)=a\\ f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {0}}((&b,a,x^8_{-{\hat{m}}+1},\ldots ,x^8_1))\\ = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {{\hat{\ell }}}}((&a,a,x^8_{-{\hat{m}}+1}, \dots ,x^8_{{\hat{\ell }}},{\texttt{0}}))\\ = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {{\hat{\ell }}}}((&a,a,x^8_{-{\hat{m}}+1}, \dots ,x^8_{{\hat{\ell }}},{\texttt{1}})) \end{aligned}\right) \\&\quad \vee \left( \begin{aligned} f(a,&a,a)=b\\ f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {0}}((&b,a,x^8_{-{\hat{m}}+1},\ldots ,x^8_1))\\ = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {{\hat{\ell }}}}((&b,a,x^8_{-{\hat{m}}+1}, \dots ,x^8_{{\hat{\ell }}},{\texttt{0}}))\\ = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {{\hat{\ell }}}}((&b,a,x^8_{-{\hat{m}}+1}, \dots ,x^8_{{\hat{\ell }}},{\texttt{1}})) \end{aligned}\right) \\&x^8_{{\hat{\ell }}} = a\\&x^8_{{\hat{\ell }}-1} = b \end{aligned}$$

and ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right}\,\text {finite},m>m',{\textcircled {1}})$ defined as (where ${\textcircled {1}}$ is $(m+\ell '=n-1 \wedge \ell '={\hat{\ell }}) \vee (m+\ell '=n \wedge \ell '={\hat{\ell }}+1)$) $\exists (x^8_{-{\hat{m}}+1},\ldots ,x^8_0,\ldots ,x^8_{{\hat{\ell }}}) : \exists a,b \in \{{\texttt{0}},{\texttt{1}}\}: f(b,a,a) = b$

$$\begin{aligned}&\left( \begin{aligned} f(a,&a,a)=a\\ f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {0}}((&b,a,x^8_{-{\hat{m}}+1},\ldots ,x^8_1))\\ = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {{\hat{\ell }}}}((&a,a,x^8_{-{\hat{m}}+1}, \dots ,x^8_{{\hat{\ell }}},{\texttt{0}}))\\ = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {{\hat{\ell }}}}((&a,a,x^8_{-{\hat{m}}+1}, \dots ,x^8_{{\hat{\ell }}},{\texttt{1}})) \end{aligned}\right) \\&\quad \vee \left( \begin{aligned} f(a,&a,a)=b\\ f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {0}}((&b,a,x^8_{-{\hat{m}}+1},\ldots ,x^8_1))\\ = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {{\hat{\ell }}}}((&b,a,x^8_{-{\hat{m}}+1}, \dots ,x^8_{{\hat{\ell }}},{\texttt{0}}))\\ = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {{\hat{\ell }}}}((&b,a,x^8_{-{\hat{m}}+1}, \dots ,x^8_{{\hat{\ell }}},{\texttt{1}})) \end{aligned}\right) \\&x^8_{{\hat{\ell }}} = b \end{aligned}$$

and ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right finite},m<m')$ defined as

$$\begin{aligned}&{\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right finite},m<m',{\textcircled {2}})\\&\quad \wedge {\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right finite},m<m',{\textcircled {1}}) \end{aligned}$$

where

$$\begin{aligned} {\textcircled {2}}&\,\text { is } m'+\ell '=n \wedge \ell '={\hat{\ell }}\\ {\textcircled {1}}&\,\text { is } (m'+\ell '=n-1 \wedge \ell '={\hat{\ell }}) \vee (m'+\ell '=n \wedge \ell '={\hat{\ell }}+1) \end{aligned}$$

with ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right finite},m<m',{\textcircled {2}})$ defined as (where ${\textcircled {2}}$ is $m'+\ell '=n \wedge \ell '={\hat{\ell }}$)

$\exists (x^8_{-{\hat{m}}+1},\ldots ,x^8_0,\ldots ,x^8_{{\hat{\ell }}}) : \exists a,b \in \{{\texttt{0}},{\texttt{1}}\}: f(b,a,a) = b$

$$\begin{aligned}&\left( \begin{aligned} f(a,&a,a)=a\\ f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {0}}((&a,a,x^8_{-{\hat{m}}+1},\ldots ,x^8_1))\\ = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {{\hat{\ell }}}}((&b,a,x^8_{-{\hat{m}}+1}, \dots ,x^8_{{\hat{\ell }}},{\texttt{0}}))\\ = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {{\hat{\ell }}}}((&b,a,x^8_{-{\hat{m}}+1}, \dots ,x^8_{{\hat{\ell }}},{\texttt{1}})) \end{aligned}\right) \\&\quad \vee \left( \begin{aligned} f(a,&a,a)=b\\ f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {0}}((&b,a,x^8_{-{\hat{m}}+1},\ldots ,x^8_1))\\ = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {{\hat{\ell }}}}((&b,a,x^8_{-{\hat{m}}+1}, \dots ,x^8_{{\hat{\ell }}},{\texttt{0}}))\\ = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {{\hat{\ell }}}}((&b,a,x^8_{-{\hat{m}}+1}, \dots ,x^8_{{\hat{\ell }}},{\texttt{1}})) \end{aligned}\right) \\&x^8_{{\hat{\ell }}} = a\\&x^8_{{\hat{\ell }}-1} = b \end{aligned}$$

and${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right finite},m<m',{\textcircled {1}})$defined as (where ${\textcircled {1}}$ is $(m'+\ell '=n-1 \wedge \ell '={\hat{\ell }}) \vee (m'+\ell '=n \wedge \ell '={\hat{\ell }}+1)$) $\exists (x^8_{-{\hat{m}}+1},\ldots ,x^8_0,\ldots ,x^8_{{\hat{\ell }}}) : \exists a,b \in \{{\texttt{0}},{\texttt{1}}\}: f(b,a,a) = b$

$$\begin{aligned}&\left( \begin{aligned} f(a,&a,a)=a\\ f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {0}}((&a,a,x^8_{-{\hat{m}}+1},\ldots ,x^8_1))\\ = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {{\hat{\ell }}}}((&b,a,x^8_{-{\hat{m}}+1}, \dots ,x^8_{{\hat{\ell }}},{\texttt{0}}))\\ = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {{\hat{\ell }}}}((&b,a,x^8_{-{\hat{m}}+1}, \dots ,x^8_{{\hat{\ell }}},{\texttt{1}})) \end{aligned}\right) \\&\quad \vee \left( \begin{aligned} f(a,&a,a)=b\\ f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {0}}((&b,a,x^8_{-{\hat{m}}+1},\ldots ,x^8_1))\\ = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {{\hat{\ell }}}}((&b,a,x^8_{-{\hat{m}}+1}, \dots ,x^8_{{\hat{\ell }}},{\texttt{0}}))\\ = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {{\hat{\ell }}}}((&b,a,x^8_{-{\hat{m}}+1}, \dots ,x^8_{{\hat{\ell }}},{\texttt{1}})) \end{aligned}\right) \\&x^8_{{\hat{\ell }}} = b \end{aligned}$$

and${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right}\,\text {induction})$defined as

$$\begin{aligned}&{\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right}\,\text {induction}, {\textcircled {2}})\\&\quad \wedge {\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right}\,\text {induction}, {\textcircled {1}}) \end{aligned}$$

where

$$\begin{aligned} {\textcircled {2}}&\,\text { is } \max \{m,m'\}+\ell '=n \wedge \max \{m,m'\}={\hat{m}}\\ {\textcircled {1}}&\,\text { is } \max \{m,m'\}+\ell '=n \wedge \ell '={\hat{\ell }} \end{aligned}$$

with ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right}\,\text {induction}, {\textcircled {2}})$ defined as (where ${\textcircled {2}}$ is $\max \{m,m'\}+\ell '=n \wedge \max \{m,m'\}={\hat{m}}$) $\exists (x^8_{-{\hat{m}}+1},\ldots ,x^8_0,\ldots ,x^8_{{\hat{\ell }}-1}) : \exists a \in \{{\texttt{0}},{\texttt{1}}\}: f(a,a,a) = a$

$$\begin{aligned}&f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {0}}((a,a,x^8_{-{\hat{m}}+1},\ldots ,x^8_1)) \\&\quad = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {{\hat{\ell }}}}((a,a,x^8_{-{\hat{m}}+1}, \dots ,x^8_{{\hat{\ell }}-1},a,a))\\&x^8_{-{\hat{m}}+1} = a \end{aligned}$$

and ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right}\,\text {induction}, {\textcircled {1}})$ defined as (where ${\textcircled {1}}$ is $\max \{m,m'\}+\ell '=n \wedge \ell '={\hat{\ell }}$) $\exists (x^8_{-{\hat{m}}+1},\ldots ,x^8_0,\ldots ,x^8_{{\hat{\ell }}-1}) : \exists a \in \{{\texttt{0}},{\texttt{1}}\}: f(a,a,a) = a$

$$\begin{aligned}&f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {0}}((a,a,x^8_{-{\hat{m}}+1},\ldots ,x^8_1)) \\&\quad = {\texttt{1}}-f^{{-{\hat{m}}}\rightarrow {0}\leftarrow {{\hat{\ell }}}}((a,a,x^8_{-{\hat{m}}+1}, \dots ,x^8_{{\hat{\ell }}-1},a,a))\\&x^8_{{\hat{\ell }}-1} = a \end{aligned}$$

Proof

Let ${\varDelta }\not \equiv {\varDelta }'$ according to the case of Formula (2). Then, according to Property 1 there exist some $i_0,m,m',\ell '$. We use the fact that cellular automata are shift invariant: what is claimed at cell 0 in the hypothesis can be applied to cell $i_0$. Let us now argue that Lemma 3 can always be used (the left (resp. right) side of equalities corresponds to ${\varDelta }$ (resp. ${\varDelta }'$)) to conclude:

$$\begin{aligned} \exists x \in \{{\texttt{0}},{\texttt{1}}\}^n \, F_{{\varDelta }}(x)_{i_0} \ne F_{{\varDelta }'}(x)_{i_0}. \end{aligned}$$

(3)

This proof basically consists in a tedious case disjunction (71 cases), each precise case being straightforward to prove given the hypothesis of the lemma. There is a first case disjunction according to the order of m (resp.$m', \ell '$) compared to ${\hat{m}}$ (resp.${\hat{m}}, {\hat{\ell }}$), consisting of 8 cases (left side of the following list), and for each of these 8 cases we have to argue that Formula (3) holds, which is ensured by the conjunction of the following 8 predicates (right side of the following list, one for each case):

$$\begin{aligned}&m<{\hat{m}} \wedge m'<{\hat{m}} \wedge \ell '<{\hat{\ell }} \quad \qquad \qquad {\mathcal {I}}(m<{\hat{m}},m'<{\hat{m}},\ell '<{\hat{\ell }})\\ \text {or }& \,m<{\hat{m}} \wedge m'<{\hat{m}} \wedge \ell '\ge {\hat{\ell }} \qquad \qquad \wedge {\mathcal {I}}(m<{\hat{m}},m'<{\hat{m}},\ell '\ge {\hat{\ell }})\\ \text {or }& \,m<{\hat{m}} \wedge m'\ge {\hat{m}} \wedge \ell '<{\hat{\ell }} \qquad \qquad \wedge {\mathcal {I}}(m<{\hat{m}},m'\ge {\hat{m}},\ell '<{\hat{\ell }})\\ \text {or }& \,m<{\hat{m}} \wedge m'\ge {\hat{m}} \wedge \ell '\ge {\hat{\ell }} \qquad \qquad \wedge {\mathcal {I}}(m<{\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }})\\ \text {or }& \,m\ge {\hat{m}} \wedge m'<{\hat{m}} \wedge \ell '<{\hat{\ell }} \qquad \qquad \wedge {\mathcal {I}}(m\ge {\hat{m}},m'<{\hat{m}},\ell '<{\hat{\ell }})\\ \text {or }& \,m\ge {\hat{m}} \wedge m'<{\hat{m}} \wedge \ell '\ge {\hat{\ell }} \qquad \qquad \wedge {\mathcal {I}}(m\ge {\hat{m}},m'<{\hat{m}},\ell '\ge {\hat{\ell }})\\ \text {or }& \,m\ge {\hat{m}} \wedge m'\ge {\hat{m}} \wedge \ell '<{\hat{\ell }} \qquad \qquad \wedge {\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '<{\hat{\ell }})\\ \text {or }& \,m\ge {\hat{m}} \wedge m'\ge {\hat{m}} \wedge \ell '\ge {\hat{\ell }} \qquad \qquad \wedge {\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}) \end{aligned}$$

Case 1:$m<{\hat{m}} \wedge m'<{\hat{m}} \wedge \ell '<{\hat{\ell }}$. In this case predicate ${\mathcal {I}}(m<{\hat{m}},m'<{\hat{m}},\ell '<{\hat{\ell }})$ ensures that Formula (3) holds, with an argument analogous to Lemma 5.

Case 2:$m<{\hat{m}} \wedge m'<{\hat{m}} \wedge \ell '\ge {\hat{\ell }}$. We consider two subcases. Since predicate ${\mathcal {I}}(m<{\hat{m}},m'<{\hat{m}},\ell '\ge {\hat{\ell }})$ holds, either predicate ${\mathcal {I}}(m<{\hat{m}},m'\ge {\hat{m}},\ell '<{\hat{\ell }}, \text {right finite})$ or ${\mathcal {I}}(m<{\hat{m}},m'\ge {\hat{m}},\ell '<{\hat{\ell }}, \text {right}\,\text {induction})$ hold.

If ${\mathcal {I}}(m<{\hat{m}},m'\ge {\hat{m}},\ell '<{\hat{\ell }}, \text {right finite})$ holds, then Formula (3) holds with an argument analogous to Lemma 5.
If ${\mathcal {I}}(m<{\hat{m}},m'\ge {\hat{m}},\ell '<{\hat{\ell }}, \text {right}\,\text {induction})$ holds, then we will build a configuration x (with $x_i=x^2_i$ where $x^2$ is defined) with an induction of the form $a,\ldots ,a,b$ on the right side (until the right bounding of $i_0$ in ${\varDelta }'$, i.e. $x_{i_0+\ell '+1}$), which may overlap the left bounding of $i_0$ in ${\varDelta }$ or ${\varDelta }'$. This overlap depends on the value of $\max \{m,m'\}+\ell$ as follows (recall that from Property 1 we have $\max \{m,m'\}+\ell \le n$):
$$\begin{aligned} \text {if } \max \{m,m'\}+\ell '=\left\{ \begin{array}{lll} &{}n &{}\text { then } \begin{aligned} x_{i_0-m-1}=&{}x_{i_0+\ell '-1} \\ \wedge x_{i_0-m}=&{}x_{i_0+\ell '} \\ \wedge x_{i_0-m+1}=&{}x_{i_0+\ell '+1}\end{aligned}\\ &{}n-1 &{}\text { then } \begin{aligned} x_{i_0-m-1}=&{}x_{i_0+\ell '} \\ \wedge x_{i_0-m}=&{}x_{i_0+\ell '+1}\end{aligned}\\ &{}n-2 &{}\text { then } x_{i_0-m-1}=x_{i_0+\ell '+1}\\ \le &{}n-3 &{}\text { then}\,\text {there}\,\text {is}\,\text {no}\,\text {overlap} \end{array}\right. \end{aligned}$$
and we have to prove that in any case Formula (3) holds. The conjunction of predicates
$$\begin{aligned}&{\mathcal {I}}(m<{\hat{m}},m'\ge {\hat{m}},\ell '<{\hat{\ell }}, \text {right}\,\text {induction}, \\&\qquad \qquad \max \{m,m'\}+\ell '=n)\\&\quad \wedge {\mathcal {I}}(m<{\hat{m}},m'\ge {\hat{m}},\ell '<{\hat{\ell }}, \text {right}\,\text {induction}, \\&\qquad \qquad \max \{m,m'\}+\ell '=n-1)\\&\quad \wedge {\mathcal {I}}(m<{\hat{m}},m'\ge {\hat{m}},\ell '<{\hat{\ell }}, \text {right}\,\text {induction}, \\&\qquad \qquad \max \{m,m'\}+\ell '=n-2) \end{aligned}$$
respectively ensures that Formula (3) holds in the three first subsubcases (the proof by induction is straightforward with $f(a,a,b)=b$), and the construction for the fourth subsubcase derives from any of the three first cases (since there is no overlap hence no constraint, an x with additional constraint is still valid to prove Formula (3)).

Case 3:$m<{\hat{m}} \wedge m'\ge {\hat{m}} \wedge \ell '<{\hat{\ell }}$. This case is symmetric to case 2 with an induction on the left side and $m'+\ell '$ in place of $\max \{m,m'\}+\ell '$ (note that in case 3 we have $m'>m$). An additional detail is that if $m={\hat{m}}$ then we have to set $x^3_{-m-1}=x^3_{-{\hat{m}}}=a$ to be coherent (because $x^3_{-{\hat{m}}}$ is not part of the existential quantification on the configuration).

Case 4:$m<{\hat{m}} \wedge m'\ge {\hat{m}} \wedge \ell '\ge {\hat{\ell }}$. This case is a bit more involved because we want to consider an induction on the left side only, on the right side only, or on both side. We want that at least one such construction of x leads to a proof of Formula (3), hence the disjunction among the four predicates.

If ${\mathcal {I}}(m<{\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left finite}, \text {right finite})$ holds, then Formula (3) holds with an argument analogous to Lemma 5.
If ${\mathcal {I}}(m<{\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left finite}, \text {right}\,\text {induction})$ holds, then we will build a configuration x (with $x_i=x^4_i$ where $x^4$ is defined) with an induction of the form $a,\ldots ,a,b$ on the right side (until the right bounding of $i_0$ in ${\varDelta }'$, i.e. $x_{i_0+\ell '+1}$), which may overlap the left bounding of $i_0$ in ${\varDelta }$ or ${\varDelta }'$. The overlap on cells on the left of $i_0-{\hat{m}}$ do not matter, since the Lemma claims that whether the result $x'_{i_0-{\hat{m}}-1}$ of substeps updating the state of cells $i_0-m'$ to $i_0-{\hat{m}}-1$ equals ${\texttt{0}}$ or ${\texttt{1}}$ do not matter to have different images at $i_0$. The overlap we have to consider therefore depends on the value of $m'+\ell '$ and $m'$ as follows (recall that from Property 1 we have $m'+\ell ' \le n$, and that in case 4 we have $m'>m$):
$$\begin{aligned}&\text {if } m'+\ell '=n \wedge m'={\hat{m}} \\&\quad \text { then } x_{i_0-{\hat{m}}}=a \wedge x_{i_0-{\hat{m}}+1}=b\\&\text {if } \left( \begin{aligned}&(m'+\ell '=n-1 \wedge m'={\hat{m}}) \\&\quad \vee (m'+\ell '=n \wedge m'={\hat{m}}+1) \end{aligned}\right) \\&\qquad \text { then } x_{i_0-{\hat{m}}}=b\\&\text {if } \left( \begin{aligned}&m'+\ell ' \le n-2 \\&\quad \vee m' \ge {\hat{m}}+2 \\&\quad \vee (m'+\ell '=n-1 \wedge m'={\hat{m}}+1) \end{aligned}\right) \\&\qquad \text { then there is no overlap} \end{aligned}$$
and we have to prove that in any case Formula (3) holds. The conjunction of predicates
$$\begin{aligned}&{\mathcal {I}}(m<{\hat{m}},m'\ge {\hat{m}},\ell '<{\hat{\ell }}, \text {left finite}, \text {right}\,\text {induction},{\textcircled {2}})\\&\quad \wedge {\mathcal {I}}(m<{\hat{m}},m'\ge {\hat{m}},\ell '<{\hat{\ell }}, \text {left finite}, \text {right}\,\text {induction}, {\textcircled {1}}) \end{aligned}$$
where
$$\begin{aligned} {\textcircled {2}}\,&\,\text { is } m'+\ell '=n \wedge m'={\hat{m}}\\ {\textcircled {1}}&\,\text { is } (m'+\ell '=n-1 \wedge m'={\hat{m}}) \vee (m'+\ell '=n \wedge m'={\hat{m}}+1) \end{aligned}$$
respectively ensures that Formula (3) holds in the two first subsubcases (the proof by induction is straightforward with $f(a,a,b)=b$), and the construction for the third subsubcase derives from any of the two first cases (since there is no overlap hence no constraint, an x with additional constraint is still valid to prove Formula (3)).
If ${\mathcal {I}}(m<{\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right finite})$ holds, then Formula (3) holds with an argument symmetric to the previous subcase, with an induction on the left side and $m'$ in place of $\ell '$.
If ${\mathcal {I}}(m<{\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right}\,\text {induction})$ holds, then we will build a configuration x (with $x_i=x^4_i$ where $x^4$ is defined) with an induction of the form $a,\ldots ,a,a$ on the right side (until the right bounding of $i_0$ in ${\varDelta }'$, i.e. $x_{i_0+\ell '+1}$) and an induction of the form $a,a,\ldots ,a$ on the left side (until the left bounding of $i_0$ in ${\varDelta }'$, i.e. $x_{i_0-m'-1}$), which may overlap. If this overlap occurs away from $i_0-{\hat{m}}$ and $i_0+{\hat{\ell }}$ then we are left with coherent values a and we do not need to pay particular attention to it. The overlap we have to consider with care depends on the value of $m'+\ell '$ (so that there is an overlap), $m'$ and $\ell '$ (so that the overlap affects $x^4$) as follows (recall that from Property 1 we have $m'+\ell ' \le n$, and that in case 4 we have $m'>m$):
$$\begin{aligned}&\text {if } m'+\ell '=n \wedge m'={\hat{m}} \\&\quad \text { then } x_{i_0-{\hat{m}}}=a \wedge x_{i_0-{\hat{m}}+1}=a\\&\text {if } \left( \begin{aligned}&(m'+\ell '=n-1 \wedge m'={\hat{m}}) \\&\quad \vee (m'+\ell '=n \wedge m'={\hat{m}}+1) \end{aligned}\right) \\&\qquad \text { then } x_{i_0-{\hat{m}}}=a\\&\text {if } m'+\ell '=n \wedge \ell '={\hat{\ell }} \\&\quad \text { then } x_{i_0+{\hat{\ell }}}=a \wedge x_{i_0+{\hat{\ell }}-1}=a\\&\text {if } \left( \begin{aligned}&(m'+\ell '=n-1 \wedge \ell '={\hat{\ell }}) \\&\quad \vee (m'+\ell '=n \wedge \ell '={\hat{\ell }}+1) \end{aligned}\right) \\&\qquad \text { then } x_{i_0+{\hat{\ell }}}=a\\&\text {if } \left( \begin{aligned}&m'+\ell ' \le n-2 \\&\quad \vee (m' \ge {\hat{m}}+2 \wedge \ell ' \ge {\hat{\ell }}+2) \\&\quad \vee (m'+\ell '=n-1 \wedge (m'={\hat{m}}+1 \vee \ell '={\hat{\ell }}+1)) \end{aligned}\right) \\&\qquad \text { then there is no overlap} \end{aligned}$$
and we have to prove that in any case Formula (3) holds. The conjunction of predicates
$$\begin{aligned}&{\mathcal {I}}(m<{\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \\&\qquad \qquad \text {right}\,\text {induction}, m'+\ell '=n \wedge m'={\hat{m}})\\&\wedge{\mathcal {I}}(m<{\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \\&\qquad \qquad \text {right}\,\text {induction}, m'+\ell '=n \wedge \ell '={\hat{\ell }}) \end{aligned}$$
respectively ensures that Formula (3) holds in the first plus second and third plus fourth subsubcases (the proof by induction is straightforward with $f(a,a,a)=a$, and note that case two (resp. four) just removes one constraint of case one (resp. three)), and the construction for the last subsubcase derives from any of the four first cases (since there is no overlap hence no constraint, an x with additional constraint is still valid to prove Formula (3)).

Case 5:$m\ge {\hat{m}} \wedge m'<{\hat{m}} \wedge \ell '<{\hat{\ell }}$. This case is identical to case 3 with m in place of $m'$.

Case 6:$m\ge {\hat{m}} \wedge m'<{\hat{m}} \wedge \ell '\ge {\hat{\ell }}$. This case is identical to case 4 with m in place of $m'$.

Case 7:$m\ge {\hat{m}} \wedge m'\ge {\hat{m}} \wedge \ell '\ge {\hat{\ell }}$. This case is similar to cases 3 and 5, with an additional consideration of the order on $m,m'$ ($m=m'$ or $m>m'$ or $m<m'$), so that

we can identify which of $m+\ell '$ or $m'+\ell '$ must be considered to measure the overlap among the left and right boundings of $i_0$ (if equals n then three cells, $n-1$ then two cells, $n-2$ then one cell, and smaller or equal to $n-3$ then no overlap),
we consider identical (if $m=m'$) or differentiated (otherwise) inductions for the left bounding of $i_0$ in ${\varDelta }$ and ${\varDelta }'$. Each formula then allows one possibility for the induction relative to the greatest of $m,m'$ (of the usual form $b,a,\ldots ,a$), and two possibilities for the induction relative to the strictly smallest of $m,m'$:
- either $f(a,a,a)=a$ and the base case is $x^7$ with a, a on the left (induction of the form $a,a,\ldots ,a$ in the update schedule corresponding to the smallest of $m,m'$),
- or $f(a,a,a)=b$ and the base case is $x^7$ with b, a on the left (induction of the form $b,a,\ldots ,a$ in the update schedule corresponding to the smallest of $m,m'$).

Also note that in the cases $m=m'$ and $m>m'$, when $m+\ell =n$ (three cells overlap) we do not need to consider $\ell '=1$ (the corresponding predicates are stated for all $2 \le \ell ' < {\hat{\ell }}$) because in the corresponding case of $i_0,m,m',\ell$ it is supposed to solve, there exists of a forbidden cycle of length n in ${\varDelta }$ (hence there is no corresponding case to solve so it is not needed^{Footnote 1}):

($lab_{n,{\varDelta }}((i_0+1,i_0))=\oplus$ according to Formula (2)).

Case 8:$m\ge {\hat{m}} \wedge m'\ge {\hat{m}} \wedge \ell '\ge {\hat{\ell }}$. This case is similar to cases 4 and 6, with the additional consideration of the order on $m,m'$ that appeared in case 7 (in the case where we have an induction on the left or (exclusive) right side of x). $\square$

In Lemma 6 we could have dissociated the construction of x on the left side for the two update schedules (one finite and one inductive), but if such a dissociated construction works (i.e. verify the corresponding formulas), then the proposed construction with the same induction on the left side for the two update schedules also works.

Note that the hypothesis of Lemma 6 (which can be further factorized and reduced at the cost of clarity) takes again a time in ${\mathcal {O}}({\hat{m}}^2{\hat{\ell }}\,2^{{\hat{m}}+{\hat{\ell }}})$ to check (with a bigger constant than Lemma 5), for a countably infinite number of ${\hat{m}}$ and ${\hat{\ell }}$. Also note that taking different ${\hat{m}}$ and ${\hat{m}}'$ for ${\varDelta }$ and ${\varDelta }'$ would also work with accordingly detailed considerations, and would give qualitatively similar results. Some unintensive computer tests give the next theorem.

Theorem 7

Rule 154 is max-sensitive for any$n \ge 5$.

Proof

The hypothesis of Lemma 6 have been tested for all pair of $1\le {\hat{m}} \le 5$ and $2 \le {\hat{\ell }} \le 5$, and for the two symmetric cases of Formula (2) (equivalently, the hypothesis of Lemma 6 have been tested for a rule and its reflection). As an additional witness to the values of ${\hat{m}}$ and ${\hat{\ell }}$ for a rule and its reflection, we also give the configurations satisfying the 8th and last predicate (this case represents asymptotically a hundred percents of update schedules).

Rule 154 (reflection 210) passed all 8 tests for ${\hat{m}}= 1 , {\hat{\ell }}= 2$, with predicate ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right}\,\text {induction})$ satisfied as follows:
- predicate ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right}\,\text {induction}, {\textcircled {2}})$ with $x^8= ({\texttt{0}}, {\texttt{1}}, {\texttt{1}})$, $a={\texttt{0}}$, $b={\texttt{1}}$,
- predicate ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right}\,\text {induction}, {\textcircled {1}})$ with $x^8= ({\texttt{0}}, {\texttt{1}}, {\texttt{0}})$, $a={\texttt{0}}$, $b={\texttt{0}}$.
Rule 210 (reflection 154) passed all 8 tests for ${\hat{m}}= 2 , {\hat{\ell }}= 2$, with predicate ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right finite})$ satisfied as follows:
- predicate ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right finite},m=m',{\textcircled {2}})$ with $x^8= ({\texttt{0}}, {\texttt{0}}, {\texttt{1}}, {\texttt{0}})$, $a={\texttt{0}}$, $b={\texttt{1}}$,
- predicate ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right finite},m=m',{\textcircled {1}})$ with $x^8= ({\texttt{0}}, {\texttt{0}}, {\texttt{1}}, {\texttt{0}})$, $a={\texttt{0}}$, $b={\texttt{0}}$,
- predicate ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right finite},m>m',{\textcircled {2}})$ with $x^8= ({\texttt{0}}, {\texttt{0}}, {\texttt{0}}, {\texttt{1}})$, $a={\texttt{1}}$, $b={\texttt{0}}$,
- predicate ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right finite},m>m',{\textcircled {1}})$ with $x^8= ({\texttt{0}}, {\texttt{0}}, {\texttt{0}}, {\texttt{1}})$, $a={\texttt{0}}$, $b={\texttt{1}}$,
- predicate ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right finite},m<m',{\textcircled {2}})$ with $x^8= ({\texttt{0}}, {\texttt{0}}, {\texttt{0}}, {\texttt{1}})$, $a={\texttt{1}}$, $b={\texttt{0}}$,
- predicate ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right finite},m<m',{\textcircled {1}})$ with $x^8= ({\texttt{0}}, {\texttt{0}}, {\texttt{0}}, {\texttt{1}})$, $a={\texttt{0}}$, $b={\texttt{1}}$,

$\square$

3.8.1 Using the reflection (6 rules)

We can notice that some rules “almost” passed the tests of max sensitivity corresponding to the hypothesis of Lemma 6. In particular, 9 rules passed the tests only in one of the two symmetric cases of Formula (2), as stated in the following proposition.

Proposition 1

For rules 2, 10, 42, 130, 138 and any $n \ge 4$, for rules 86 (reflection 30), 40, 106, 168 and any $n \ge 5$, we have for all ${\varDelta }\not \equiv {\varDelta }'$ such that Formula (2) holds: $\exists x \in \{0,1\}^n: \exists i_0:F_{{\varDelta }}(x)_{i_0} \ne F_{{\varDelta }'}(x)_{i_0}$.

Proof

The hypothesis of Lemma 6 have been tested for all pair of $1\le {\hat{m}} \le 5$ and $2 \le {\hat{\ell }} \le 5$, and for the two symmetric cases of Formula (2) (equivalently, the hypothesis of Lemma 6 have been tested for a rule and its reflection).

As an additional witness to the values of ${\hat{m}}$ and ${\hat{\ell }}$ for a rule so that it satisfies the hypothesis of Lemma 6, we also give the configurations satisfying the 8th and last predicate (this case represents asymptotically a hundred percents of dynamics).

Rule 2 (reflection 16) passed all 8 tests for ${\hat{m}}= 1 , {\hat{\ell }}= 2$, with predicate ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }},\text {left finite}, \text {right}\,\text {finite})$ satisfied with $x^8=({\texttt{0}}, {\texttt{0}}, {\texttt{1}}, {\texttt{0}})$.
Rule 10 (reflection 80) passed all 8 tests for ${\hat{m}}= 1 , {\hat{\ell }}= 2$, with predicate ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }},\text {left finite}, \text {right}\,\text {finite})$ satisfied with $x^8=({\texttt{0}}, {\texttt{0}}, {\texttt{1}}, {\texttt{0}})$.
Rule 86 (reflection 30) passed all 8 tests for ${\hat{m}}= 1 , {\hat{\ell }}= 3$, with predicate ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }},\text {left finite},\text {right}\,\text {induction})$ satisfied as follows:
- predicate ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }},\text {left finite}, \text {right}\,\text {induction}, {\textcircled {2}})$ with $x^8= ({\texttt{0}}, {\texttt{1}}, {\texttt{1}}, {\texttt{1}})$, $a={\texttt{0}}$, $b={\texttt{1}}$,
- predicate ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }},\text {left finite}, \text {right}\,\text {induction}, {\textcircled {1}})$ with $x^8= ({\texttt{0}}, {\texttt{1}}, {\texttt{0}}, {\texttt{0}})$, $a={\texttt{0}}$, $b={\texttt{0}}$.
Rule 40 (reflection 96) passed all 8 tests for ${\hat{m}}= 2 , {\hat{\ell }}= 2$, with predicate ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }},\text {left finite}, \text {right}\,\text {finite})$ satisfied with $x^8=({\texttt{0}}, {\texttt{0}}, {\texttt{1}}, {\texttt{1}}, {\texttt{0}})$.
Rule 42 (reflection 112) passed all 8 tests for ${\hat{m}}= 1 , {\hat{\ell }}= 2$, with predicate ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }},\text {left finite}, \text {right}\,\text {finite})$ satisfied with $x^8=({\texttt{0}}, {\texttt{0}}, {\texttt{1}}, {\texttt{1}})$.
Rule 106 (reflection 120) passed all 8 tests for ${\hat{m}}= 1 , {\hat{\ell }}= 3$, with predicate ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }},\text {left finite},\text {right}\,\text {induction})$ satisfied as follows:
- predicate ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }},\text {left finite}, \text {right}\,\text {induction}, {\textcircled {2}})$ with $x^8= ({\texttt{0}}, {\texttt{0}}, {\texttt{1}}, {\texttt{0}})$, $a={\texttt{0}}$, $b={\texttt{0}}$,
- predicate ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }},\text {left finite}, \text {right}\,\text {induction}, {\textcircled {1}})$ with $x^8= ({\texttt{0}}, {\texttt{0}}, {\texttt{1}}, {\texttt{0}})$, $a={\texttt{0}}$, $b={\texttt{0}}$.
Rule 130 (reflection 144) passed all 8 tests for ${\hat{m}}= 1 , {\hat{\ell }}= 2$, with predicate ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }},\text {left finite}, \text {right}\,\text {finite})$ satisfied with $x^8=({\texttt{0}}, {\texttt{0}}, {\texttt{1}}, {\texttt{0}})$.
Rule 138 (reflection 208) passed all 8 tests for ${\hat{m}}= 1 , {\hat{\ell }}= 2$, with predicate ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }},\text {left finite}, \text {right}\,\text {finite})$ satisfied with $x^8=({\texttt{0}}, {\texttt{0}}, {\texttt{1}}, {\texttt{0}})$.
Rule 168 (reflection 224) passed all 8 tests for ${\hat{m}}= 1 , {\hat{\ell }}= 3$, with predicate ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }},\text {left finite}, \text {right}\,\text {finite})$ satisfied with $x^8=({\texttt{0}}, {\texttt{1}}, {\texttt{1}}, {\texttt{0}}, {\texttt{0}})$.

$\square$

It turns out that, when a rule (or its reflection) verifies the hypothesis of Lemma 6, then a much lighter version of the hypothesis of Lemma 6 is required for the reflection (or the rule) to conclude about its max-sensitivity. Indeed, in many cases the fact that the reflection verifies the hypothesis of Lemma 6 can be exploited in the symmetric case of Formula (2), as stated in the following result.

Lemma 7

If a rule verifies the hypothesis of Lemma 6, and if furthermore its reflection verifies the hypothesis of Lemma 6 with

$$\begin{aligned}&{\mathcal {I}}(m<{\hat{m}},m'\ge {\hat{m}},\ell '<{\hat{\ell }}) = \mathtt {true}\\&{\mathcal {I}}(m<{\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}) = \mathtt {true}\\&{\mathcal {I}}(m\ge {\hat{m}},m'<{\hat{m}},\ell '<{\hat{\ell }}) = \mathtt {true}\\&{\mathcal {I}}(m<{\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}) = \mathtt {true}\\&{\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '<{\hat{\ell }}, \text {left}\,\text {induction}, m>m') = \mathtt {true}\\&{\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '<{\hat{\ell }}, \text {left}\,\text {induction}, m<m') = \mathtt {true}\\&{\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right finite},m>m') = \mathtt {true}\\&{\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right finite},m<m') = \mathtt {true} \end{aligned}$$

then $\forall {\varDelta }\not \equiv {\varDelta }': \exists x \in \{{\texttt{0}},{\texttt{1}}\}^n: \exists i_0: F_{{\varDelta }}(x)_{i_0} \ne F_{{\varDelta }'}(x)_{i_0}$, for any $n \ge {\hat{m}}+{\hat{\ell }}+1$.

Proof

Let us argue that the discarded predicates (set to $\mathtt {true}$), used to prove the existence of x when $m \ne m'$, are not required when the reflection of the rule verifies the (original) hypothesis of Lemma 6. Indeed, when $m>m'$ or $m<m'$ then we have respectively

$$\begin{aligned}&lab_{n,{\varDelta }'}((i_0-m'-1,i_0-m')) = \oplus \ne \ominus \\&\quad = lab_{n,{\varDelta }}((i_0-m'-1,i_0-m'))\\ \text {or }\,&lab_{n,{\varDelta }}((i_0-m-1,i_0-m)) = \oplus \ne \ominus \\&\quad = lab_{n,{\varDelta }'}((i_0-m-1,i_0-m)) \end{aligned}$$

hence we are in the symmetric of Formula (2), and we can use the fact that the reflection of the rule verifies the hypothesis of Lemma 6 (with the new $i_0$ being $i_0-m'$ or $i_0-m$) to prove the existence of a configuration x such that

$$\begin{aligned} F_{{\varDelta }}(x)_{i_0-m'} \ne F_{{\varDelta }'}(x)_{i_0-m'} \quad \text {or} \quad F_{{\varDelta }}(x)_{i_0-m} \ne F_{{\varDelta }'}(x)_{i_0-m} \end{aligned}$$

respectively. $\square$

With equal time complexity we get the next theorem using Proposition 1.

Theorem 8

Rules 2, 10, 130, 138 are max-sensitive for any $n \ge 4$, and rules 106, 168 are max-sensitive for any$n \ge 5$.

Proof

The hypothesis of Lemma 6 modified as stated in Lemma 7 have been tested for all pair of $0\le {\hat{m}} \le 5$ and $1 \le {\hat{\ell }} \le 5$ on rules 16, 80, 30, 96, 112, 120, 144, 208, 224, for which Proposition 1 states that their reflection verifies the (original) hypothesis of Lemma 6.

As an additional witness to the values of ${\hat{m}}$ and ${\hat{\ell }}$ for a rule so that it satisfies the hypothesis of Lemma 6 modified as stated in Lemma 7, we also give the configurations satisfying the 8th and last predicate (this case represents asymptotically a hundred percents of update schedules).

Rule 16 (reflection 2) passed all 8 tests for ${\hat{m}}= 1 , {\hat{\ell }}= 2$, with predicate ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right finite})$ satisfied as follows:
- predicate ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right finite},m=m',{\textcircled {2}})$
  with $x^8= ({\texttt{0}}, {\texttt{1}}, {\texttt{0}})$, $a={\texttt{0}}$, $b={\texttt{1}}$,
- predicate ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right finite},m=m',{\textcircled {1}})$
  with $x^8= ({\texttt{0}}, {\texttt{1}}, {\texttt{1}})$, $a={\texttt{0}}$, $b={\texttt{1}}$.
Rule 80 (reflection 10) passed all 8 tests for ${\hat{m}}= 1 , {\hat{\ell }}= 2$, with predicate ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right finite})$ satisfied as follows:
- predicate ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right finite},m=m',{\textcircled {2}})$
  with $x^8= ({\texttt{0}}, {\texttt{1}}, {\texttt{0}})$, $a={\texttt{0}}$, $b={\texttt{1}}$,
- predicate ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right finite},m=m',{\textcircled {1}})$
  with $x^8= ({\texttt{0}}, {\texttt{1}}, {\texttt{1}})$, $a={\texttt{0}}$, $b={\texttt{1}}$.
Rule 120 (reflection 106) passed all 8 tests for ${\hat{m}}= 1 , {\hat{\ell }}= 2$, with predicate ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right finite})$ satisfied as follows:
- predicate ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right finite},m=m',{\textcircled {2}})$
  with $x^8= ({\texttt{1}}, {\texttt{0}}, {\texttt{0}})$, $a={\texttt{0}}$, $b={\texttt{0}}$,
- predicate ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right finite},m=m',{\textcircled {1}})$
  with $x^8= ({\texttt{1}}, {\texttt{0}}, {\texttt{0}})$, $a={\texttt{0}}$, $b={\texttt{0}}$,
Rule 144 (reflection 130) passed all 8 tests for ${\hat{m}}= 1 , {\hat{\ell }}= 2$, with predicate ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right finite})$ satisfied as follows:
- predicate ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right finite},m=m',{\textcircled {2}})$
  with $x^8= ({\texttt{0}}, {\texttt{1}}, {\texttt{0}})$, $a={\texttt{0}}$, $b={\texttt{1}}$,
- predicate ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right finite},m=m',{\textcircled {1}})$
  with $x^8= ({\texttt{0}}, {\texttt{1}}, {\texttt{1}})$, $a={\texttt{0}}$, $b={\texttt{1}}$.
Rule 208 (reflection 138) passed all 8 tests for ${\hat{m}}= 1 , {\hat{\ell }}= 2$, with predicate ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right finite})$ satisfied as follows:
- predicate ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right finite},m=m',{\textcircled {2}})$
  with $x^8= ({\texttt{0}}, {\texttt{1}}, {\texttt{0}})$, $a={\texttt{0}}$, $b={\texttt{1}}$,
- predicate ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right finite},m=m',{\textcircled {1}})$
  with $x^8= ({\texttt{0}}, {\texttt{1}}, {\texttt{1}})$, $a={\texttt{0}}$, $b={\texttt{1}}$.
Rule 224 (reflection 168) passed all 8 tests for ${\hat{m}}= 1 , {\hat{\ell }}= 2$, with predicate ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right finite})$ satisfied as follows:
- predicate ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right finite},m=m',{\textcircled {2}})$
  with $x^8= ({\texttt{0}}, {\texttt{1}}, {\texttt{1}})$, $a={\texttt{1}}$, $b={\texttt{1}}$,
- predicate ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right finite},m=m',{\textcircled {1}})$
  with $x^8= ({\texttt{0}}, {\texttt{1}}, {\texttt{1}})$, $a={\texttt{1}}$, $b={\texttt{1}}$.

The result of Proposition 1 proves the other part required by Lemma 7 to conclude. $\square$

3.8.2 Using the reflection symmetricaly (2 rules)

It turns out that a similar argument applies to rules which are their own reflection. We cannot use as such the fact that the reflection verifies all predicates, therefore the statement has to be weakened in that sense, but also strenghened precisely in the sense that we do not require that the reflection verifies all predicates.

Lemma 8

If a rule and its reflection verify the hypothesis of Lemma 6 for ${\hat{m}}>0$ with

$$\begin{aligned}&{\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '<{\hat{\ell }}, \text {left}\,\text {induction}, m>m') = \mathtt {true}\\&{\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '<{\hat{\ell }}, \text {left}\,\text {induction}, m<m') = \mathtt {true}\\&{\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right finite},m>m') = \mathtt {true}\\&{\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right finite},m<m') = \mathtt {true} \end{aligned}$$

then $\forall {\varDelta }\not \equiv {\varDelta }': \exists x \in \{{\texttt{0}},{\texttt{1}}\}^n: \exists i_0: F_{{\varDelta }}(x)_{i_0} \ne F_{{\varDelta }'}(x)_{i_0}$, for any $n \ge {\hat{m}}+{\hat{\ell }}+1$.

Proof

The proof is identical to Lemma 7, with one additional argument when we consider $m>m'$ (resp. $m<m'$). If furthermore ${\hat{m}}>0$ then $m>m'\ge {\hat{m}}\ge 1$ (resp. $1\le \hat{m'}\le m<m'$) in the considered cases, and we are in the following situation around cell $i_0-m'$ (recall that $n\ge 3$):

In the above picture all labels are fixed by definition except two:

$lab_{n,{\varDelta }}((i_0-m'+1,i_0-m'))=\oplus$ (resp. $lab_{n,{\varDelta }}((i_0-m+1,i_0-m))=\oplus$);
$lab_{n,{\varDelta }'}((i_0+m'+1,i_0-m'))=\oplus$ (resp. $lab_{n,{\varDelta }'}((i_0+m+1,i_0-m))=\oplus$),

otherwise there is a negative cycle of size two in both cases because $lab_{n,{\varDelta }}((i_0-m',i_0-m'+1))=\ominus$ and $lab_{n,{\varDelta }'}((i_0+m',i_0-m'+1))=\ominus$ (from the fact that $m,m' \ge m'$ and $i_0$ is m-left-bounded in ${\varDelta }$ and $m'$-left-bounded in ${\varDelta }'$, and $m>m'\ge {\hat{m}}\ge 1$ (resp. $1\le \hat{m'}\le m<m'$)). Consequently, in any case of ${\varDelta },{\varDelta }'$ and $i_0$ such that $m > m'$ (resp. $m < m'$) and ${\hat{m}}>0$, we can consider the symmetric case of Formula (2) corresponding to the reflection of the rule, and apply predicate

$$\begin{aligned}&{\mathcal {I}}(m<{\hat{m}},m'<{\hat{m}},\ell<{\hat{\ell }})\\ \text {or }& \,{\mathcal {I}}(m<{\hat{m}},m'<{\hat{m}},\ell \ge {\hat{\ell }}) \end{aligned}$$

to conclude that there exists a configuration x such that

$$\begin{aligned} F_{{\varDelta }}(x)_{i_0-m'} \ne F_{{\varDelta }'}(x)_{i_0-m'} \quad \text {(resp.} \, F_{{\varDelta }}(x)_{i_0-m} \ne F_{{\varDelta }'}(x)_{i_0-m} \text {)} \end{aligned}$$

since $i_0-m'$ is 0-right-bounded in both ${\varDelta }$ and ${\varDelta }'$. $\square$

Lemma 8 allows to conclude for rule 90, as stated in the next theorem.

Theorem 9

Rule 90 is max-sensitive for any $n \ge 7$.

Proof

Rule 90 (reflection 90) passed all 8 tests corresponding to the hypothesis of Lemma 6 modified as stated in Lemma 8, for ${\hat{m}}=3$, ${\hat{\ell }}=3$, with predicate ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right}\,\text {induction})$ satisfied as follows:

predicate ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right}\,\text {induction}, {\textcircled {2}})$
with $x^8= ({\texttt{0}}, {\texttt{0}}, {\texttt{0}}, {\texttt{0}}, {\texttt{1}})$, $a={\texttt{0}}$,
predicate ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right}\,\text {induction}, {\textcircled {1}})$ with $x^8= ({\texttt{0}}, {\texttt{0}}, {\texttt{1}}, {\texttt{0}}, {\texttt{0}})$, $a={\texttt{0}}$.

Remark that rule 90 proves predicate

$$\begin{aligned} {\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}) \end{aligned}$$

with

$$\begin{aligned} {\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right}\,\text {induction}) \end{aligned}$$

and not

$$\begin{aligned} {\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right finite}), \end{aligned}$$

hence Lemma 8 is (as may have been expected) striclty stronger than necessary. $\square$

Rules 150 (reflection 150) needs a little help for predicate

$$\begin{aligned} {\mathcal {I}}(m<{\hat{m}},m'<{\hat{m}},\ell \ge {\hat{\ell }}, \text {right}\,\text {induction}, {\textcircled {3}}) \, \text { and } \, m=m'=0 \end{aligned}$$

so that we can apply Lemma 8. Recall that ${\textcircled {3}}$ is $\max \{m,m'\}+\ell '=n$ in this case.

Theorem 10

Rule 150 is max-sensitive for any $n \ge 5$.

Proof

If we discard the following case then rule 150 verifies the hypothesis of Lemma 8, so let us argue that it can be avoided.

Case to avoid. In the case that the $i_0,m,m',\ell '$ given by Property 1 are such that $m<{\hat{m}}$, $m'<{\hat{m}}$, $\ell '<{\hat{\ell }}$, $\max \{m,m'\}+\ell '=n$ and $m=m'=0$, we have $lab_{{\varDelta }'}((i_0+1,i_0))=\ominus$ (as usual). Moreover we have $\ell '=n$, consequently $i_0$ is n-right-bounded in ${\varDelta }'$ which implies $lab_{{\varDelta }'}((i_0+n+1 \mod n,i_0+n \mod n))=lab_{{\varDelta }'}((i_0+1,i_0))=\oplus$, a contradiction. As a conclusion we can discard this case.

Test with discarded case. We can now check that the hypothesis of Lemma 8 are verified by rule 150 (reflection 150) for ${\hat{m}}>0$ without considering $m=m'=0$ in the universal quantification of predicate ${\mathcal {I}}(m<{\hat{m}},m'<{\hat{m}},\ell \ge {\hat{\ell }}, \text {right}\,\text {induction}, {\textcircled {3}})$. Note that all the arguments in the proofs of Lemmas 6 and 8 are still valid with this ad-hoc modification.

Then rule 150 (reflection 150) passed all 8 tests for ${\hat{m}}=2,{\hat{\ell }}=2$, with predicate ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right}\,\text {induction})$ satisfied as follows:

predicate ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right}\,\text {induction}, {\textcircled {2}})$ with $x^8= ({\texttt{0}}, {\texttt{0}}, {\texttt{1}})$, $a={\texttt{0}}$,
predicate ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right}\,\text {induction}, {\textcircled {1}})$ with $x^8= ({\texttt{0}}, {\texttt{0}}, {\texttt{1}})$, $a={\texttt{1}}$.

$\square$

3.8.3 Minor improvements (3 rules)

Rules 96 (reflection 40) and 112 (reflection 42) need a little help for predicate

$$\begin{aligned} {\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '<{\hat{\ell }}, \text {left}\,\text {induction}, m=m') \end{aligned}$$

so that we can apply Lemma 7. More precisely, it needs a hand for

$$\begin{aligned} {\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '<{\hat{\ell }}, \text {left}\,\text {induction}, m=m',{\textcircled {2}})&\text { and} \, \ell '=1. \end{aligned}$$

Theorem 11

Rule 42 is max-sensitive for any $n \ge 4$, and rule 40 is max-sensitive for any $n \ge 5$.

Proof

If we discard the following case then rules 96 (reflection 40) and 112 (reflection 42) verify the hypothesis of Lemma 7, so let us argue that it can be avoided. Recall that rules 40 and 42 appear in Proposition 1.

Case to avoid. In the case that the $i_0,m,m',\ell '$ given by Property 1 are such that $m \ge {\hat{m}}, m' \ge {\hat{m}}, \ell ' < {\hat{\ell }}$, $m=m'$ and also $m+\ell '=n-1$ and $\ell '=1$, then ${\varDelta }, {\varDelta }'$ must be as follows:

In the above picture all labels are fixed by definition except two:

$lab_{n,{\varDelta }}((i_0,i_0+1))=\oplus$ otherwise to solve this case we can consider the symmetric case of Formula (2) i.e. rule 40 or 42 which already passed the hypothesis of Lemma 6;
$lab_{n,{\varDelta }}((i_0+2,i_0+1))=\ominus$ otherwise there is a forbidden cycle of length n in ${\varDelta }$.

We can therefore use $i_0+1,0,0,1$ in place of respectively $i_0,m,m',\ell '$, which corresponds to predicate ${\mathcal {I}}(m<{\hat{m}},m'<{\hat{m}},\ell '<{\hat{\ell }})$ if ${\hat{m}} \ge 1$ and ${\hat{\ell }} \ge 2$ (which will be the case thereafter).

Test with discarded case. We can now check that the hypothesis of Lemma 7 are verified by rules 96 (reflection 40) and 112 (reflection 42) for ${\hat{m}} \ge 1$ and ${\hat{\ell }} \ge 2$, without considering $\ell '=1$ in the universal quantification of predicate ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '<{\hat{\ell }}, \text {left}\,\text {induction}, m=m',{\textcircled {2}})$. Note that all the arguments in the proofs of Lemmas 6 and 7 are still valid with this ad-hox modification.

Then rule 96 (reflection 40) passed all 8 tests for ${\hat{m}}=2,{\hat{\ell }}=2$, with predicate ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }},\text {left finite}, \text {right}\,\text {finite})$ satisfied with $x^8= ({\texttt{0}}, {\texttt{0}}, {\texttt{1}}, {\texttt{1}}, {\texttt{0}})$.

And rule 112 (reflection 42) passed all 8 tests for ${\hat{m}}=1,{\hat{\ell }}=2$, with predicate ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right finite})$ satisfied as follows:

predicate ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right finite},m=m',{\textcircled {2}})$
with $x^8= ({\texttt{1}}, {\texttt{1}}, {\texttt{0}})$, $a={\texttt{0}}$, $b={\texttt{1}}$,
predicate ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right finite},m=m',{\textcircled {1}})$
with $x^8= ({\texttt{1}}, {\texttt{0}}, {\texttt{1}})$, $a={\texttt{0}}$, $b={\texttt{1}}$,

$\square$

Rules 30 (reflection 86) needs a little more help for predicate

$$\begin{aligned} {\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '<{\hat{\ell }}, \text {left}\,\text {induction}, m=m') \end{aligned}$$

so that we can apply Lemma 7. More precisely, it needs a hand for

$$\begin{aligned} {\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '<{\hat{\ell }}, \text {left}\,\text {induction}, m=m',{\textcircled {3}})&\text { and} \, \ell '=2\\ {\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '<{\hat{\ell }}, \text {left}\,\text {induction}, m=m',{\textcircled {2}})&\text { and} \, \ell '=1. \end{aligned}$$

Theorem 12

Rule 30 is max-sensitive for any $n \ge 6.$

Proof

If we discard the following cases then rule 30 (reflection 86) verify the hypothesis of Lemma 7, so let us argue that it can be avoided. Recall that rule 86 appear in Proposition 1.

First case to avoid. In the case that the $i_0,m,m',\ell '$ given by Property 1 are such that $m \ge {\hat{m}}, m' \ge {\hat{m}}, \ell ' < {\hat{\ell }}$, $m=m'$ and also $m+\ell '=n$ and $\ell '=2$, then we provide the following configuration $x \in \{{\texttt{0}},{\texttt{1}}\}^n$ such that $F_{{\varDelta }}(x)_{i_0} \ne F_{{\varDelta }'}(x)_{i_0}$ (we recall that $n \ge 3$):

In the above picture all labels are fixed by definition except two:

$lab_{n,{\varDelta }}((i_0,i_0+1))=\oplus$ otherwise to solve this case we can consider the symmetric case of Formula (2) i.e. rule 86 which already passed the hypothesis of Lemma 6;
$lab_{n,{\varDelta }}((i_0+2,i_0+1))=\ominus$ otherwise there is a forbidden cycle of length n in ${\varDelta }$.

At the end $lab_{n,{\varDelta }}=lab_{n,{\varDelta }'}$ everywhere but on $(i_0+1,i_0)$, and we have

$$\begin{aligned} F_{{\varDelta }}(x)_{i_0} = 1 \ne 0 = F_{{\varDelta }'}(x)_{i_0}. \end{aligned}$$

Second case to avoid. this case is identical to the case to avoid for rules 96 (reflection 40) and 112 (reflection 42), and the same argumentation applies.

Test with discarded cases. We can now check that the hypothesis of Lemma 7 are verified by rule 30 (reflection 86) for ${\hat{m}} \ge 1$ and ${\hat{\ell }} \ge 2$, without considering $\ell '=2$ in the universal quantification of predicate ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '<{\hat{\ell }}, \text {left}\,\text {induction}, m=m',{\textcircled {3}})$ and without considering $\ell '=1$ in the universal quantification of predicate ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '<{\hat{\ell }}, \text {left}\,\text {induction}, m=m',{\textcircled {2}})$. Note that all the arguments in the proofs of Lemmas 6 and 7 are still valid with this ad-hoc modification.

Then rule 30 (reflection 86) passed all 8 tests for ${\hat{m}}=2$, ${\hat{\ell }}=3$, with predicate ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right finite})$ satisfied as follows:

predicate ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right finite},m=m',{\textcircled {2}})$ with $x^8= ({\texttt{0}}, {\texttt{0}}, {\texttt{0}}, {\texttt{1}}, {\texttt{0}})$, $a={\texttt{0}}$, $b={\texttt{1}}$,
predicate ${\mathcal {I}}(m\ge {\hat{m}},m'\ge {\hat{m}},\ell '\ge {\hat{\ell }}, \text {left}\,\text {induction}, \text {right finite},m=m',{\textcircled {1}})$ with $x^8= ({\texttt{0}}, {\texttt{0}}, {\texttt{0}}, {\texttt{0}}, {\texttt{1}})$, $a={\texttt{0}}$, $b={\texttt{1}}$.

$\square$

3.9 Particular inductions (2 rules)

It remains to characterise the sensitivity of two ECA rules: 45 (reflection 101) and 105 (reflection 105). The following proofs of max-sensitivity both make use of inductive patterns different than ${\texttt{0}},{\texttt{0}},\ldots ,{\texttt{0}},$ or ${\texttt{1}},{\texttt{0}},\ldots ,{\texttt{0}}$ or ${\texttt{0}},{\texttt{1}},\ldots ,{\texttt{1}}$ or ${\texttt{1}},{\texttt{1}},\ldots ,{\texttt{1}}$ for the left side, or different than ${\texttt{0}},\ldots ,{\texttt{0}},{\texttt{0}}$ or ${\texttt{0}},\ldots ,{\texttt{0}},{\texttt{1}}$ or ${\texttt{1}},\ldots ,{\texttt{1}},{\texttt{0}}$ or ${\texttt{1}},\ldots ,{\texttt{1}},{\texttt{1}}$ for the right side. For rule 45 we will use the right side inductive patterns ${\texttt{0}},\ldots ,{\texttt{0}},{\texttt{0}}$ or ${\texttt{0}},\ldots ,{\texttt{0}},{\texttt{1}}$ depending on the parity of $\ell '$, and for rule 105 we will use the left side inductive pattern $\dots ,{\texttt{1}},{\texttt{1}},{\texttt{0}},{\texttt{0}},{\texttt{1}},{\texttt{1}},{\texttt{0}},{\texttt{0}}$. It naturaly raises a question: do rule 45 and 105 necessarily require such evolved inductions? And if the answer is yes, then what makes them unique regarding max-sensitivity? Note that applying the technic that follows for different ${\texttt{0}}$-${\texttt{1}}$ values rather than those “guessed” below leads to the same consideration of particular inductions for rules 45 and 105.

3.9.1 Rule 45

The reflection of rule 45 is rule 101.

Let us first consider rule 101 for the cases given by Formula (2), and then rule 45 for the cases given by Formula (2), which together cover every cases.

Lemma 9

We consider rule 101. Let ${\varDelta }\not \equiv {\varDelta }'$ in the case of Formula (2) and $i_0,m,m',\ell '$ be given by Property 1. If $n \ge 4$ then for all $\ell ' \ge 1$ we have $\exists x \in \{{\texttt{0}},{\texttt{1}}\}^n: F_{{\varDelta }}(x)_{i_0} \ne F_{{\varDelta }'}(x)_{i_0}$.

Proof

For $\ell '=1$ and $\ell '=2$ the result is straightfoward to obtain: consider respectively $(x_{i_0},x_{i_0+1},x_{i-0+2})=({\texttt{1}},{\texttt{1}},{\texttt{1}})$ and $(x_{i_0},x_{i_0+1},x_{i_0+2},x_{i_0+3})=({\texttt{1}},{\texttt{1}},{\texttt{0}},{\texttt{1}})$, then regardless of other values of $x \in \{{\texttt{0}},{\texttt{1}}\}^n$ with $n \ge 4$, this ensures that $F_{{\varDelta }'}(x)_{i_0}={\texttt{1}} \ne {\texttt{0}}=F_{{\varDelta }}(x)_{i_0}$.

Let us consider the situation $\ell '=3$, as pictured below:

Now remark that

$(x_{i_0},x_{i_0+1},x_{i_0+2},x_{i_0+3},x_{i_0+4})=({\texttt{1}},{\texttt{1}},{\texttt{0}},{\texttt{1}},{\texttt{0}})$ implies $F_{{\varDelta }'}(x)_{i_0}={\texttt{1}} \ne {\texttt{0}}=F_{{\varDelta }}(x)_{i_0}$,
$(x_{i_0},x_{i_0+1},x_{i_0+2},x_{i_0+3},x_{i_0+4})=({\texttt{1}},{\texttt{1}},{\texttt{1}},{\texttt{1}},{\texttt{1}})$ implies $F_{{\varDelta }'}(x)_{i_0}={\texttt{1}} \ne {\texttt{0}}=F_{{\varDelta }}(x)_{i_0}$,

regardless of other values of $x \in \{{\texttt{0}},{\texttt{1}}\}^n$. We can remark that there exist $(x_{i_0},x_{i_0+1},x_{i_0+3})=({\texttt{1}},{\texttt{1}},{\texttt{1}})$ such that, for any value of $x_{i_0+4} \in \{{\texttt{0}},{\texttt{1}}\}$, there exists $x_{i_0+2} \in \{{\texttt{0}},{\texttt{1}}\}$ such that $F_{{\varDelta }'}(x)_{i_0} \ne F_{{\varDelta }}(x)_{i_0}$. As a consequence, if we consider any $\ell ' \ge 3$, we can fix the values $(x_{i_0},x_{i_0+1},x_{i_0+3})=({\texttt{1}},{\texttt{1}},{\texttt{1}})$, fix arbitrary values to other cells different from $i_0+2$, and consider the updates in ${\varDelta }'$ of cells greater or equal to index $i_0+4$ (which are all determined). If the update of cell $i_0+4$ gives $F_{{\varDelta }'}(x)_{i_0+4}={\texttt{0}}$ then we set $x_{i_0+2}={\texttt{0}}$, and if it gives $F_{{\varDelta }'}(x)_{i_0+4}={\texttt{1}}$ then we set $x_{i_0+2}={\texttt{1}}$. As assessed by the two items above, this algorithmic process always constructs a configuration $x \in \{{\texttt{0}},{\texttt{1}}\}^n$ such that $F_{{\varDelta }'}(x)_{i_0}={\texttt{1}} \ne {\texttt{0}}=F_{{\varDelta }}(x)_{i_0}$, which finishes the proof (note that $\ell ' \ge 3$ implies $n \ge 4$, and there is no conflict in the reasoning even if the left and right boundings overlap). $\square$

Theorem 13

Rule 45 is max-sensitive for any $n \ge 4$.

Proof

The reflection of rule 45 is rule 101. We first consider some cases of rule 45 with ${\varDelta }\not \equiv {\varDelta }'$ in the case of Formula (2), and second we use rule 101 and Lemma 9 to conclude in all other cases.

Rule 45. Let us consider ${\varDelta }\not \equiv {\varDelta }'$ in the case of Formula (2) and $i_0,m,m',\ell '$ given by Property 1 Remark that, if we denote $x^{{\varDelta }'}_{i_0-1}$ and $x^{{\varDelta }}_{i_0-1}$ the state of cell $i_0-1$ when cell $i_0$ is updated, then we have

for $\ell '=1$ and $(x_{i_0},x_{i_0+1},x_{i_0+2})=({\texttt{0}},{\texttt{0}},{\texttt{0}})$,
for $\ell '=2$ and $(x_{i_0},x_{i_0+1},x_{i_0+2},x_{i_0+3})=({\texttt{0}},{\texttt{0}},{\texttt{0}},{\texttt{1}})$,
for $\ell '=3$ and $(x_{i_0},x_{i_0+1},x_{i_0+2},x_{i_0+3},x_{i_0+4})=({\texttt{0}},{\texttt{0}},{\texttt{0}},{\texttt{0}},{\texttt{0}})$,
for $\ell '=4$ and $(x_{i_0},x_{i_0+1},x_{i_0+2},x_{i_0+3},x_{i_0+4},x_{i_0+5})=({\texttt{0}},{\texttt{0}},{\texttt{0}},{\texttt{0}},{\texttt{0}},{\texttt{1}})$,
for $\ell '=5$ and $(x_{i_0},x_{i_0+1},x_{i_0+2},x_{i_0+3}, x_{i_0+4},x_{i_0+5},x_{i_0+6})=({\texttt{0}},{\texttt{0}},{\texttt{0}},{\texttt{0}},{\texttt{0}},{\texttt{0}},{\texttt{0}})$,
for $\ell '=6$ and $(x_{i_0},x_{i_0+1},x_{i_0+2},x_{i_0+3},x_{i_0+4}, x_{i_0+5},x_{i_0+6},x_{i_0+7})=({\texttt{0}},{\texttt{0}},{\texttt{0}},{\texttt{0}},{\texttt{0}},{\texttt{0}},{\texttt{0}},{\texttt{1}})$,
...

that

$$\begin{aligned} F_{{\varDelta }'}(x)_{i_0} \ne F_{{\varDelta }}(x)_{i_0} \, \text { if}\,\text {and}\,\text {only}\,\text {if } \, x^{{\varDelta }'}_{i_0-1} = x^{{\varDelta }}_{i_0-1} \end{aligned}$$

because the update of $i_0$ will be respectively given by $f(x^{{\varDelta }'}_{i_0-1},{\texttt{0}},{\texttt{1}})$ and $f(x^{{\varDelta }}_{i_0-1},{\texttt{0}},{\texttt{0}})$. We will use this observation to conclude when $m=m'$ (which directly implies $x^{{\varDelta }'}_{i_0-1} = x^{{\varDelta }}_{i_0-1}$), but before we need to consider possible overlaps between the left and right boundings of $i_0$.

Overlaps. Recall that we consider $m=m'$ only. The overlap may create a conflict between the values of $x_{i_0}$ and $x_{i_0+\ell '+1}$, only when $\ell '$ is even and $\ell '=n-1$ (when $\ell '$ is odd the values that overlap are compatible, and it is not possible that $\ell '=n$ otherwise there is a forbidden cycle of size n in the update digraph of ${\varDelta }'$). Furthermore, if there is another arc $e \in A_{n}, e \ne (i_0+1,i_0)$ of the ECA interaction digraph such that $lab_{n,{\varDelta }}(e) \ne lab_{n,{\varDelta }'}(e)$ then we can avoid the present case $\ell '=n-1$ and conclude that $\exists x \in \{{\texttt{0}},{\texttt{1}}\}^n: F_{{\varDelta }'}(x)_{i_0} \ne F_{{\varDelta }}(x)_{i_0}$. So we are left with the following case to consider:

In the above picture all labels are fixed by definition except $(i_0,i_0-1)$ which is $\ominus$ otherwise there is a forbidden cycle of length n in the update digraph of ${\varDelta }'$. Hence, to sum-up, we have $m=m'=1$, $\ell '=n-1$ and n is odd. In this case (recall that we work modulo n),

${\varDelta }\equiv (\{i_0-1\},\{i_0-2\},\ldots ,\{i_0+2\},\{i_0+1,i_0\})$,
${\varDelta }' \equiv (\{i_0-1\},\{i_0-2\},\ldots ,\{i_0+2\},\{i_0+1\},\{i_0\})$.

It turns out that for all odd $n \ge 4$ the configuration x with $x_{i_0-1}=x_{i_0-2}={\texttt{1}}$ and ${\texttt{0}}$ elsewhere updates to

$F_{{\varDelta }}(x)_{x_{i_0-j}}=F_{{\varDelta }'}(x)_{x_{i_0-j}}={\texttt{0}}$ if $1\le j \le n-1$ is odd,
$F_{{\varDelta }}(x)_{x_{i_0-j}}=F_{{\varDelta }'}(x)_{x_{i_0-j}}={\texttt{1}}$ if $1\le j \le n-1$ is even,
and finaly $F_{{\varDelta }}(x)_{x_{i_0}}={\texttt{1}} \ne {\texttt{0}}=F_{{\varDelta }'}(x)_{x_{i_0}}$, which is our goal.

As a consequence, if $m=m'$ then we can conclude that $\exists x \in \{{\texttt{0}},{\texttt{1}}\}^n: F_{{\varDelta }'}(x)_{i_0} \ne F_{{\varDelta }}(x)_{i_0}$.

Rule 101. For $m \ne m'$ and for the symmetric of Formula (2), we can consider rule 101 and apply Lemma 9 to get the result, again for any $n \ge 4$. $\square$

3.9.2 Rule 105

Rule 105 is its own reflection.

The following reasoning is similar to the proof of Lemma 9, with an additional consideration of the left-bounding of $i_0$.

Theorem 14

Rule 105 is max-sensitive for any $n \ge 9$.

Proof

Rule 105 has the following remarkable feature:

$$\begin{aligned} f(a,b,c) \ne f(a',b',c') \iff (a \ne a') \otimes (c \ne c') \end{aligned}$$

with $\otimes$ the exclusive disjunction. Let ${\varDelta }\not \equiv {\varDelta }'$ in the case of Formula (2) and $i_0,m,m',\ell '$ be given by Property 1. In the following our goal is to construct a configuration x such that when $i_0$ is updated it gives different images, and this will be achieved by inducing a change in the state of cell $i_0+1$ from ${\varDelta }$ to ${\varDelta }'$, while keeping the same state of cell $i_0-1$ for both ${\varDelta }$ and ${\varDelta }'$.

Cell$i_0+1$updates differently. Let us consider the situation $\ell '=3$, as pictured below:

Let $x^{{\varDelta }}_{i_0+1}$ and $x^{{\varDelta }'}_{i_0+1}$ denote the state of cell $i_0+1$ when cell $i_0$ is updated according to ${\varDelta }$ and ${\varDelta }'$ respectively. Our goal is to have $x^{{\varDelta }}_{i_0-1} \ne x^{{\varDelta }'}_{i_0-1}$. Now remark that

$(x_{i_0},x_{i_0+1},x_{i_0+2},x_{i_0+3},x_{i_0+4})=({\texttt{0}},{\texttt{0}},{\texttt{0}},{\texttt{0}},{\texttt{0}})$ implies $x^{{\varDelta }}_{i_0+1}={\texttt{0}} \ne {\texttt{1}}=x^{{\varDelta }'}_{i_0+1}$,
$(x_{i_0},x_{i_0+1},x_{i_0+2},x_{i_0+3},x_{i_0+4})=({\texttt{0}},{\texttt{1}},{\texttt{0}},{\texttt{0}},{\texttt{1}})$ implies $x^{{\varDelta }}_{i_0+1}={\texttt{1}} \ne {\texttt{0}}=x^{{\varDelta }'}_{i_0+1}$,

regardless of other values of $x \in \{{\texttt{0}},{\texttt{1}}\}^n$. We can remark that there exist $(x_{i_0},x_{i_0+2},x_{i_0+3})=({\texttt{0}},{\texttt{0}},{\texttt{0}})$ such that, for any value of $x_{i_0+4} \in \{{\texttt{0}},{\texttt{1}}\}$, there exists $x_{i_0+1} \in \{{\texttt{0}},{\texttt{1}}\}$ such that $x^{{\varDelta }}_{i_0+1} \ne x^{{\varDelta }'}_{i_0+1}$. As a consequence, for any $\ell ' \ge 3$ we can

1.
fix the values $(x_{i_0},x_{i_0+2},x_{i_0+3})=({\texttt{0}},{\texttt{0}},{\texttt{0}})$,

and then, given arbitrary values to other cells different from $i_0+1$ (the values will be given in the next paragraph about the left-bounding of $i_0$ and cell $i_0-1$), we can

2.
consider the updates in ${\varDelta }'$ of cells greater or equal to index $i_0+4$ (which are all determined), and if the update of cell $i_0+4$ gives $F_{{\varDelta }'}(x)_{i_0+4}={\texttt{0}}$ then we set $x_{i_0+1}={\texttt{0}}$, and if it gives $F_{{\varDelta }'}(x)_{i_0+4}={\texttt{1}}$ then we set $x_{i_0+1}={\texttt{1}}$.

As assessed by the two items above, this algorithmic process always constructs a configuration $x \in \{{\texttt{0}},{\texttt{1}}\}^n$ such that $x^{{\varDelta }}_{i_0+1} \ne x^{{\varDelta }'}_{i_0+1}$.

Cell$i_0-1$updates equally. Let $x^{{\varDelta }}_{i_0-1}$ and $x^{{\varDelta }'}_{i_0-1}$ denote the state of cell $i_0-1$ when cell $i_0$ is updated according to ${\varDelta }$ and ${\varDelta }'$ respectively. Our goal is to have $x^{{\varDelta }}_{i_0-1} = x^{{\varDelta }'}_{i_0-1}$. If $m=m'$ this is straightforwardly the case (same left-bounding of $i_0$ in ${\varDelta }$ and ${\varDelta }'$, Lemma 3).

If $m > m'$ (resp. $m < m'$), then by setting

$$\begin{aligned} (x_{i_0-m-1},x_{i_0-m},\ldots ,x_{i_0-m'}) \text { a suffix of }&({\texttt{1100}})^*\\ \text {(resp. } (x_{i_0-m'-1},x_{i_0-m'},\ldots ,x_{i_0-m}) \text { a suffix of }&({\texttt{1100}})^*\text {)} \end{aligned}$$

we can ensure that $x^{{\varDelta }}_{i_0-1} = x^{{\varDelta }'}_{i_0-1}$ regardless of the values $x_{i_0-m'+1}$ to $x_{i_0-1}$ (resp. $x_{i_0-m+1}$ to $x_{i_0-1}$). Indeed, in ${\varDelta }$ (resp. ${\varDelta }'$) the state of every cell from $i_0-m$ to $i_0-m'-1$ (resp. from $i_0-m'$ to $i_0-m-1$) is updated to its own value.

Conclusion. Note that, even when $m'=0$, our constructions of the right and left parts of the configuation x are compatible with each other on cell $x_{i_0}$. Morevover, as soon as $\ell ' \ge 5$ there is no conflict between our constraints relative to the left-bounding (until cell $i_0-m-1$ or $i_0-m'-1$) and our constraints relative to the right-bounding (until cell $i_0+3$ set to ${\texttt{0}}$) because $m'+\ell '\le n$ and $m+\ell '\le n$ (recall that we work modulo n). Therefore we can conclude, for any $\ell ' \ge 3$ and any $m=m'$, and for any $\ell ' \ge 5$ and any $m,m'$, that we have $\exists x \in \{{\texttt{0}},{\texttt{1}}\}^n: x^{{\varDelta }}_{i_0-1}=x^{{\varDelta }'}_{i_0-1} \wedge x^{{\varDelta }}_{i_0+1} \ne x^{{\varDelta }'}_{i_0+1}$ which implies $F_{{\varDelta }'}(x)_{i_0} \ne F_{{\varDelta }}(x)_{i_0}$ in the case of rule 105.

Now to conlude the proof, we study the case $\ell ' \le 4$ and $n \ge 9$:

if $m,m' \le 4$ then there is no overlap between our constraints relative to the left-bounding (until cell $i_0-m-1$ or $i_0-m'-1$) and our constraints relative to the right-bounding (until cell $i_0+3$ set to ${\texttt{0}}$) still because $m'+\ell '\le n$ and $m+\ell '\le n$ (recall again that we work modulo n);
if $m \ge 5$ (resp. $m' \ge 5$) then we can employ the fact that rule 105 is its own reflection: consider the same update schedules ${\varDelta },{\varDelta }'$ but reverse the left and right of $i_0$, we have two update schedules verifying Property 1 with some new $\ell ' \ge 5$ (equal to the previous m (resp. $m'$)). We can therefore apply the reasoning above.

For any ${\varDelta },{\varDelta }'$ and $n \ge 9$, we have the desired configuration x such that $F_{{\varDelta }}(x)_{i_0} \ne F_{{\varDelta }'}(x)_{i_0}$ for some cell $i_0$. $\square$

3.10 Summary of the results

We now sum-up the results obtained in Sect. 3, leading to a complete classification of ECAs, written in Theorem 15 and pictured in Table 1.

Theorem 15

Among the 88 equivalence classes of elementary cellular automata rules, for periodic configurations under fair periodic update schedules, we have the classification:

10 rules have non-effective interactions and are not max-sensitive for any $n \ge 3$: 0, 3, 12, 15, 34, 51, 60, 136, 170, 204 (Theorem 3),
6 rules have finite counter example to max-sensitivity for any $n \ge 3$: 8, 28, 32, 44, 140, 200 (Theorem 4),
3 rules have inductive counter-example to max-sensitivity for any $n \ge 3$: 128, 160, 162 (Theorem 5),
55 rules have finite proof of max-sensitivity for$n \ge n_0$ with various $n_0 \le 7$: 1, 5, 6, 19, 22, 23, 24, 27, 36, 37, 46, 50, 54, 126, 152, 178, 184, 9, 14, 18, 29, 35, 38, 43, 56, 57, 58, 74, 94, 110, 132, 142, 146, 156, 172, 7, 11, 26, 62, 72, 73, 78, 108, 122, 134, 33, 42, 76, 77, 164, 232, 13, 25, 104 (Theorem 6),
12 rules have inductive proof of max-sensitivity for $n \ge n_0$ with various $n_0 \le 7: 2, 10, 30, 40, 42, 90, 106, 130, 138, 150, 154, 168$ (Theorems 7, 8, 9, 10, 11, 12),
2 rules have particular inductive proof of max-sensitivity, respectively for $n \ge 4$ and $n \ge 9$: 45, 105 (Theorems 13, 14).

All the result presented above are in accordence with the exhaustive experimental results for all $n \le 9$ from Montalva et al. (2018). We get the following interesting corollary.

Corollary 1

An elementary cellular automata rule is max-sensitive for all $n \ge 7$ if and only if there exists $n \ge 7$ such that it is max-sensitive.

We conclude this section with Table 1.

Table 1 Partition of the ECA rule space according to ultimate maximum sensitivity to synchronism, for periodic configurations under fair periodic update schedules, for all $n \ge 7$

Full size table

4 Conclusion and perspectives

We have presented a classification of elementary cellular automata as maximal sensitive to update schedule modifications or not, for all period size $n \ge 7$ (Theorem 15 and Table 1). Together with the study presented in Montalva et al. (2018) for $n \le 9$, this closes the problem. All proofs are constructive: either they provide a pair ${\varDelta }\not \equiv {\varDelta }'$ such that the image of any configuration is identical under both update schedules, or for each pair ${\varDelta }\not \equiv {\varDelta }'$ they provide a configuration x and a cell i such that the image of x under ${\varDelta }$ and ${\varDelta }'$ differ at position i.

Let us comment the results of Table 1. Regarding the non-max-sensitive rules, there are 10 obvious cases of rules having non-effective interactions. It is more interesting to underline that 9 non-max-sensitive rules require the exhibition of a counter example (a configuration having the same image under two different update schedules), which may be finite or require induction. Regarding the max-sensitive rules, there are 55 simple cases given by a straightforward proof search: rules for which any two update schedules are distinguished on a cylinder of configurations (a finite size pattern is fixed and the rest may be arbitrary). For 12 other rules the argumentation is analogous but requires an induction, meaning that no cylinder of configurations distinguishes two update schedules (since it failed the previous test), but instead a precise inductive construction is necessary. Finally, 2 rules required special attention to be classified. We can remark that, as n grows, no rule alternate arbitrarily often between max-sensitivity and non-max-sensitivity (Corollary 1). There is no obvious explanation for this classification: though non-max-sensitive rules do not belong to the chaotic and complex intuitive classes of Wolfram (2002), we see that some fairly simple rules (such as 4, 40, 168) are max-sensitive. To reflect the long term sensitivity to synchronism and maybe relate it to the “dynamical complexity” of ECAs, it may be interesting to pursue the present study and extend it in order to measure the sensitivity to synchronism of asymptotic behaviors (attractors) for example.

The notion studied in this paper is more accurately named one-step sensitivity, since it refers to the direct image of a configuration under different update schedules. Stronger notions of k-step sensitivity for any positive integer k, and even in the limit for $k=\omega$, are related to long term perturbations. They would constitute fruitful directions of research in relation with solving new classification tasks, thanks to the introduction of non-uniformity in the schedule of cells update.

As the proof structure is more and more evolved, rules seem to be less and less sensible to update schedules because it requires more work to point a difference in the respective dynamics under two non-equivalent update schedules. A quantitative study of the sensitivity of ECAs to synchronism would give a much finer view on the notion. A straightforward definition is given by the proportion $sensitivity(f,n)=\frac{|{\mathcal {D}}(f,n)|}{|{\mathcal {U}}(n)|}$. More subtle refinements may also be given according to the (maximum/minimum/average) number of configurations x and/or number of cells i such that two dynamics differ under non-equivalent update schedules.

The notion may be generalized to automata networks. Interestingly, in this general framework one naturally defines the equivalence classes of update schedules on the interaction digraph of the network, therefore Lemma 2 would not hold since there is no consideration of a single ECA interaction digraph. As a concrete example, rule 0 would have no arc in its interaction digraph, hence one equivalence class of update schedules (no arc to label), one dynamic (where the image of any configuration x is ${\texttt{0}}^n$), and consequently be max-sensitive to update schedules. Though surprising regarding the family of ECAs, it makes sense as a rule without interaction, hence without anything to be sensible to. This example underlines the fact that the interplay between the set of discrete dynamical systems considered and the interaction digraph plays a crucial role, that ought to be further explored.

Finally, some open questions.

Open question 16

Can we formulate the hypothesis of Lemmas 4, 5and 6 in an algorithmically terminating way?

Open question 17

Is there a direct and shorter proof of Corollary 1?

A proof answering positively Question 17 may also provide a solution to Question 16.

Notes

it turns out that this point is important to prove the max-sensitivity of some rules.

References

Aracena J, Demongeot J, Fanchon E, Montalva M (2013) On the number of update digraphs and its relation with the feedback arc sets and tournaments. Discrete Appl Math 161(10):1345–1355
Article MathSciNet MATH Google Scholar
Aracena J, Fanchon E, Montalva M, Noual M (2011) Combinatorics on update digraphs in boolean networks. Discrete Appl Math 159(6):401–409
Article MathSciNet MATH Google Scholar
Aracena J, Goles E, Moreira A, Salinas L (2009) On the robustness of update schedules in boolean networks. Biosystems 97:1–8
Article Google Scholar
Cook M (2004) Universality in elementary cellular automata. Complex Syst 15(1):1–40
MathSciNet MATH Google Scholar
de Oliveira PPB (2014) On density determination with cellular automata: results, constructions and directions. J Cell Autom 9(5–6):357–385
MathSciNet MATH Google Scholar
Fatès N (2011) Stochastic cellular automata solve the density classification problem with an arbitrary precision. In: STACS’2011, vol 9 of Leibniz international proceedings in informatics (LIPIcs), pp 284–295
Fatès N (2014) A guided tour of asynchronous cellular automata. J Cell Automata 9(5–6):387–416
MathSciNet MATH Google Scholar
Gardner M (1970) Mathematical games: the fantastic combinations of John Conway’s new solitaire game “Life”. Sci Am 223(4):120–123
Article Google Scholar
Kari J (2005) Theory of cellular automata: a survey. Theor Comput Sci 334(1–3):3–33
Article MathSciNet MATH Google Scholar
Montalva M, Perrot K, de Oliveira PPB, Ruivo E (2017) Sensitivity to synchronism in some boolean automata networks. In: AUTOMATA 2017 exploratory papers proceedings, pp 69–76
Montalva M, Perrot K, de Oliveira PPB, Ruivo E (2018) Characterisation of the elementary cellular automata in terms of their maximum sensitivity to all possible asynchronous updates. Chaos Solitons Fractals 113:209–220
Article MathSciNet MATH Google Scholar
Noual M (2012) Mises à jour de réseaux d’automates. Ph.D. thesis, Ecole normale supérieure de lyon, Laboratoire de l’Informatique du Parallélisme
Wolfram S (2002) A new kind of science. Wolfram Media

Download references

Acknowledgements

This work was partially supported by FONDECYT Iniciación 11150827; CNPq; ECOS-CONICYT C16E01; PACA project FRI-2015 01134; PEPS JCJC INS2I project CGETA; Young Researcher project ANR-18-CE40-0002-01 “FANs”; STIC-AmSud CoDANet project: 19-STIC-03 Campus France 43478PD and CAPES 88881.197456/2018-01; CAPES PrInt project 88887.310281/2018-00; and MackPesquisa Edital 2018.

Author information

Authors and Affiliations

Univ. de Toulon, CNRS, LIS, UMR 7020, Aix Marseille Univ., Marseille, France
Kévin Perrot
Fac. de Ingeniería y Ciencias, Univ. Adolfo Ibáñez, Peñalolén, Santiago, Chile
Marco Montalva-Medel
Fac. de Computação e Informática, Univ. Presbiteriana Mackenzie, São Paulo, Brazil
Pedro P. B. de Oliveira & Eurico L. P. Ruivo

Authors

Kévin Perrot
View author publications
You can also search for this author in PubMed Google Scholar
Marco Montalva-Medel
View author publications
You can also search for this author in PubMed Google Scholar
Pedro P. B. de Oliveira
View author publications
You can also search for this author in PubMed Google Scholar
Eurico L. P. Ruivo
View author publications
You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Kévin Perrot.

Additional information

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Perrot, K., Montalva-Medel, M., de Oliveira, P.P.B. et al. Maximum sensitivity to update schedules of elementary cellular automata over periodic configurations. Nat Comput 19, 51–90 (2020). https://doi.org/10.1007/s11047-019-09743-9

Download citation

Published: 10 July 2019
Issue Date: March 2020
DOI: https://doi.org/10.1007/s11047-019-09743-9

Keywords

Use our pre-submission checklist

Avoid common mistakes on your manuscript.

Maximum sensitivity to update schedules of elementary cellular automata over periodic configurations

Abstract

Similar content being viewed by others

Non-maximal Sensitivity to Synchronism in Periodic Elementary Cellular Automata: Exact Asymptotic Measures

The impact of alphabet size on pattern complexity of maxmin- $$\omega$$ cellular automata

A survey of cellular automata: types, dynamics, non-uniformity and applications

1 Introduction

2 Definitions

2.1 Cellular automata

Definition 1

2.2 Elementary cellular automata

Definition 2

2.3 Finite periodic configurations

2.4 ECA interaction digraph

Definition 3

2.5 Update schedule

Definition 4

2.6 Transition digraph and dynamics

Definition 5

Definition 6

2.7 Update digraph and equivalent update schedules

Definition 7

Definition 8

Theorem 1

Theorem 2

2.8 Update schedule sensitivity

Definition 9

Definition 10

2.9 Symmetries among ECAs

2.10 Previous results on ECAs

3 Characterization of max-sensitive ECAs

3.1 Counting update schedules for ECAs

Lemma 1

Proof

3.2 Rules with non-effective interactions (10 rules)

Definition 11

Lemma 2

Proof

Theorem 3

Proof

3.3 Properties of non-equivalent update schedules

Definition 12

Property 1

Proof

Property 2

Proof

3.4 A useful notation

Lemma 3

Proof

3.5 Finite counter-example to max-sensitivity (6 rules)

Lemma 4

Proof

Theorem 4

Proof

3.6 Inductive counter-example to max-sensitivity (3 rules)

Theorem 5

Proof

3.7 Finite proof of max-sensitivity (55 rules)

Lemma 5

Proof

Theorem 6

Proof

3.8 Inductive proof of max-sensitivity (12 rules)

Lemma 6

Proof

Theorem 7

Proof

3.8.1 Using the reflection (6 rules)

Proposition 1

Proof

Lemma 7

Proof

Theorem 8

Proof

3.8.2 Using the reflection symmetricaly (2 rules)

Lemma 8

Proof

Theorem 9

Proof

Theorem 10