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.

翻译：态序列构成一类自然的无限序列，通常定义为态射不动点的编码。不同的态射与编码可能产生相同的态序列。本文研究如何证明由态射给出的两种态序列表示对应于同一序列。特别地，我们关注通过仅取偶数或奇数元素得到的二进制斐波那契序列子序列的最小表示。所给出的证明通过归纳法同时验证若干性质，这些证明通常可由我们开发的工具完全自动地发现。