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.

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