Use Walnut
to prove the results in this 1991 paper: Timothy Chow,
A new characterization of the Fibonacci-free partition,
Fibonacci Quart. 29 (1991), 174-180.
Hints: to find an automaton for the set A,
use the technique of "guessing the automaton", as discussed in the
Walnut book; then prove it is correct and unique using induction.
Since Walnut cannot do induction directly, use Walnut to prove the
induction step, which is "once the numbers from 1 to n have been
assigned to the sets A and B, the choice for the number n+1 is forced".
Now do the same thing to prove a similar result where the Fibonacci
numbers are replaced by the Lucas numbers 2,1,3,4,7,11, ...