Some examples of Walnut Jeffrey Shallit You can just cut and paste these examples directly into the window running the program. -- 1. For which n does the Thue-Morse word have a square xx where |x| = n ? eval tmsquarelengths "Ej Ai ((i T[j+i] = T[j+n+i])": -- 2. For which n does the Thue-Morse word have a palindrome of length n? eval paltm "Ei Aj (j < n) => (T[i+j] = T[(i+n)-(j+1)])": -- 3. For which n does the Thue-Morse word have an overlap axaxa where |ax| = n? eval tmoverlaplengths "Ej Ai ((i<=n) => T[j+i] = T[j+n+i])": -- 4. For which n does the Fibonacci word have a cube xxx where |x| = n? eval fibcubes "?msd_fib Ei Ak (k < 2*n) => F[i+k]=F[i+n+k]": -- 5. Is the Thue-Morse sequence ultimately periodic, yes or no? eval tmup "En Ei (n >= 1) & (Aj (j>= i) => T[j] = T[n+j])": -- 6. Is the Thue-Morse sequence mirror invariant, yes or no? eval thuemirror "An Ai Ej (At (t (T[i+t] = T[(j+n)-(t+1)]))": -- 7. Is the Thue-Morse sequence recurrent, yes or no? eval tmrecur "An Ai Ek ((k>i) & (At ((t (T[i+t] = T[k+t]))))": -- 8. Is the Thue-Morse sequence uniformly recurrent, yes or no? eval tmur "An El Ai Es (s>i)&(s<=i+l)&(Aj (j (T[i+j]=T[s+j]))": -- 9. For which n does the Thue-Morse word have an unbordered factor of length n? eval tmunb "Ei ( Aj (((j>=1)&((2*j)<=n)) => (Et (t < j) & (T[i+t] != T[(i+n+t)-j]))))": -- 10. For which n does the Thue-Morse word have a rich word of length n? Here we use the characterization that a word is rich if the longest palindromic suffix of every prefix p occurs exactly once in p. eval richtm "El As Ar ((l<=r)&(r<=s)&(s (( (Ai (i+r<=s) => T[r+i]=T[s-i]) & (Au ((l<=u)&(u (Ej (j+u<=s) & T[u+j] != T[s-j]))) => (Ah ((l<=h)&(h (Ek (k+r<=s) & T[h+k] != T[r+k])))": -- 11. For which p is the Fibonacci word quasiperiodic of period p? def fibquasi "?msd_fib Ai Ej i F[k]=F[k+j]": -- 12. For which n are there anti-palindromes x x' with |x| = n in Thue-Morse? eval tmantipal "Ei (Aj (j (T[i+j] != T[i+j+n]))": -- 13. For which n is there a factor of length n occurring both in Thue-Morse AND Rudin-Shapiro? eval tmrs "Ei Ej (Ak (k (T[i+k] = RS[j+k]))": -- 14. For which n is there a factor of the form x x x^R in Thue-Morse, with |x| = n? eval tmxxxr "Ei At ((t ((T[i+t]=T[i+t+n]) & (T[i+t]=T[(i+3*n)-(t+1)])))": -- 15. For which n is there a factor of the form x x x^R in the Rote-Fibonacci word with |x| = n? You'd like to write eval rote1 "?msd_fib Ei At ((t ((R[i+t]=R[i+t+n]) & (R[i+t]=R[(i+3*n)-(t+1)])))": as in the previous example, but this runs out of space. So instead write eval rote2 "?msd_fib Ei (At (t(R[i+t]=R[i+t+n])) & (At (t (R[i+2*n+t] = R[(i+2*n)-(t+1)]))": Even faster is eval rote3 "?msd_fib Ei Ej (j=i+2*n) & (At (t(R[i+t]=R[i+t+n])) & (At (t (R[j+t]=R[j-(t+1)]))": which illustrates the idea of introducing auxiliary variables to decrease state blow-up. 16. For which n is there a privileged factor of length n in the Thue-Morse word? Here we use a criterion of Luke Schaeffer, which says that a word w is privileged if for all m, 1 <= m <= |w|, there exists a word x with 1 <= |x| <= m such that x occurs as both a prefix and suffix of w and there are no other occurrences of x in the first m symbols of w, nor in the last m symbols of w. eval tmpriv "Ei Am ((m >= 1)&(m <= n)) => Et (t >= 1)&(t <= m)& (As (s T[i+s]=T[(i+n+s)-t]) & (Aj ((j >= 1)&(j <= m-t)) => ((Ek (k T[i+k] = T[j+k]": def thueuniquepref "Aj (j > 0 & j+m < n) => ~$thuefactoreq(i,i+j,m)": def thueuniquesuff "Aj (j > 0 & j+m < n) => ~$thuefactoreq((i+n)-m,(i+n)-(m+j),m)": def thuepriv "(n >= 1) & Am (m <= n & m >= 1) => (Ep (p <= m & p >= 1) & $thueuniquepref(i,p,m) & $thueuniquesuff((i+n)-m,p,m) & $thuefactoreq(i, (i+n)-p, p))": eval thuepriv2 "Ei $thuepriv(i,n)": (Solution by Luke Schaeffer)