Equality of morphic sequences

TL;DR

This paper explores methods to determine when different morphic sequence representations are equivalent, focusing on minimal representations of Fibonacci subsequences, using automated induction proofs to establish sequence equality.

Contribution

It introduces an automated approach for proving the equivalence of different morphic sequence representations, especially for Fibonacci subsequences.

Findings

Automated induction proofs successfully verify sequence equivalences.

Minimal representations of Fibonacci subsequences are characterized.

The method generalizes to other morphic sequences.

Abstract

Morphic sequences form a natural class of infinite sequences, typically defined as the coding of a fixed point of a morphism. Different morphisms and codings may yield the same morphic sequence. This paper investigates how to prove that two such representations of a morphic sequence by morphisms represent the same sequence. In particular, we focus on the smallest representations of the subsequences of the binary Fibonacci sequence obtained by only taking the even or odd elements. The proofs we give are induction proofs of several properties simultaneously, and are typically found fully automatically by a tool that we developed.