H. Mousavi and J. Shallit,
Mechanical Proofs of Properties of the Tribonacci Word,
in
F. Manea and D. Nowotka, eds.,
WORDS 2015, LNCS 9304, Springer, 2015, pp. 1-21. Here are the
Walnut predicates you can use to reproduce most of the results in this
paper:
This was one of the first Walnut papers we wrote, and now (in 2024)
we know there are better ways to do some of the things we did in this one.
For example, to check whether TR[i..i+n-1] is a palindrome, where TR denotes
the Tribonacci word, one can simply write
def tribpal "?msd_trib Au,v (u>=i & u<i+n & u+v+1=2*i+n) => TR[u]=TR[v]":
and hence avoid the split into even and odd cases. It runs very quickly!
Similarly, to check that TR is mirror invariant, one can write
def trib_fac_reverse_equiv "?msd_trib Au,v (u>=i & u<i+n & u+v+1=i+j+n) => TR[u]=TR[v]":
def trib_mirror "?msd_trib Ai,n Ej $trib_fac_reverse_equiv(i,j,n)":
which also runs rather quickly.