Fibonacci Challenge

The infinite sequence of Fibonacci words is defined recursively as

w(0) = b
w(1) = a
w(i_+2) = w(i)w(i+1)

and consists of the words b, a, ba, aba, baaba, ababaaba, ...

After quick inspection one may notice that none of the words in the sequence above contains 'bb' as a subword. The same seems to be true for the subword 'aaa'. Indeed, these are known properties of Fibonacci words and the reader may wish to try to prove it himself/herself, or consult String Rewriting and the Fibonacci Word by Steve Whealton for further hints and easygoing introduction.

I call the problem(s) of proving that netheir 'bb' nor 'aaa' appear as the subwords in Fibonachhi words the Fibonacci puzzle(s).

Automated Solution

In Tackling Fibonacci words puzzles by finite countermodels (to appear in Proc. of FWFM 2013 ) I have demonstrated the automated solution to both variants of the Fibonacci puzzle using automated finite model finding for first-order logic. In that I have followed the general FCM (Finite CounterModels) methodology for the safety verification of infinite state and parameterized systems.

I was surprised by the simplicity of these soultions and the power of FCM method in this context. I strongly suspect that it would be difficult to get such a solution in any other way. That is why the challenge below.

Fibonacci Challenge

I would like to challenge anyone to demonstrate an alternative automated solution(s) to both variants of Fibonacci puzzle above (no 'bb' and no 'aaa' as the subwords).

Original condition (ceased by 25.07.2013):
I, Alexei Lisitsa, will pay 50 GBP (fifty British pounds, or an equivalent in an agreed currency) to the author of the first submitted solution satisfying the conditions below.

Update: As the first correct solution has arrived (see below) and the author of the solution has declined to accept the award, the conditions of the challenge have changed to

New condition (starts 25.07.2013, 15:30 UTC time)
I, Alexei Lisitsa, will pay 30 GBP (thirty British pounds, or an equivalent in an agreed currency) and 20 GBP (twenty British pounds, or an equivalent in an agreed currency) to the authors of the second and third submitted solutions, respectively. The solutions should satisfy the conditions below.

The challenge starts 13.07.2013 at 13:00 UTC time

The updated challenge starts 25.07.2013 at 15.30 UTC time

Please submit your solution to (sub: Fibonacci challenge). The second and third soultions will be judged by the time they received at the email box. If you have any questions on the challenge please send an email to (subj: Q on Fibonacci challenge)

Solutions arrived

Last updated 25.07.2013