# Examples for the talk on Walnut
# you can just cut and paste these into Walnut or (recommended)
# the Ostrowski version of Walnut by Baranwal

# Does the Thue-Morse sequence have an overlap?
eval hasolap "Ei,n (n>=1) & As (s<=n) => T[i+s]=T[i+s+n]":

# show that the Cantor sequence has no 10-antipowers
def cfactoreq "?msd_3 At (t<n) => CA[i+t]=CA[j+t]":

eval cno10 "?msd_3 Ai,n (n>=1) => (
     $cfactoreq(i+0*n,i+1*n,n) | $cfactoreq(i+0*n,i+5*n,n) |
     $cfactoreq(i+2*n,i+3*n,n) | $cfactoreq(i+2*n,i+8*n,n) |
     $cfactoreq(i+3*n,i+4*n,n) | $cfactoreq(i+3*n,i+7*n,n) |
     $cfactoreq(i+3*n,i+9*n,n) | $cfactoreq(i+4*n,i+5*n,n) |
     $cfactoreq(i+4*n,i+9*n,n) | $cfactoreq(i+5*n,i+6*n,n) |
     $cfactoreq(i+5*n,i+8*n,n) | $cfactoreq(i+6*n,i+7*n,n) |
     $cfactoreq(i+7*n,i+8*n,n) | $cfactoreq(i+8*n,i+9*n,n))":

# what are the lengths of the unbordered factors of Thue-Morse?
def tmhasbord "Ej (j>=1) & (j<n) & At (t<j) =>
T[i+t]=T[(i+n+t)-j]": # T[i..i+n-1] is bordered
def unbordlen "Ei ~$tmhasbord(i,n)":

# Which n did the Currie-Saari characterization miss?
def missing "$unbordlen(n) & n=1+6*(n/6)":

# show that the guessed word defined by DE is a Dean word
eval dean1 "Ei,n (n>=1) & At (t<n) => DE[i+t]=DE[i+n+t]":
# check if there's a square

eval dean02 "Ei DE[i]=@0 & DE[i+1]=@2":
eval dean20 "Ei DE[i]=@2 & DE[i+1]=@0":
eval dean13 "Ei DE[i]=@1 & DE[i+1]=@3":
eval dean31 "Ei DE[i]=@3 & DE[i+1]=@1":
# check for existence of factors 02, 20, 13, 31

# show that the subsequences of the DE word has the properties we guessed
eval checkde1 "An DE[4*n]=@0 & DE[4*n+2]=@2":
eval checkde2 "An (DE[2*n+1]=@1 => P[n+1]=@0) &
     (DE[2*n+1]=@3 => P[n+1]=@1)":

# for which prefix lengths is the prefix of the Fibonacci
# word quasiperiodic?
def fibfactoreq "?msd_fib At (t<n) => F[i+t]=F[j+t]":
def fibquasi "?msd_fib Ai Ej j<=i & i<n+j &
     $fibfactoreq(0,j,n)":  # F quasiperiodic with per n
reg isfib msd_fib "0*10*":
eval fibquasichk "?msd_fib An $fibquasi(n) <=> ~$isfib(n+1)":

# show that the Thue-Morse word is not quasiperiodic
def tmfactoreq "At (t<n) => T[i+t]=T[j+t]":
def tmquasi "Ai (Ej j<=i & i<n+j & $tmfactoreq(0,j,n))":
eval tmquasicheck "An ~$tmquasi(n)":

# show that every factor of the Fibonacci word is balanced
def unbalfib "?msd_fib E l1,l2,r1,r2 i<=l1 & l1<r1 & r1<i+n
& i<=l2 & l2<r2 & r2<i+n & r1+l2=r2+l1 & F[l1]=@0 & F[r1]=@0
& F[l2]=@1 & F[r2]=@1 & $fibfactoreq(l1+1,l2+1,r1-(l1+1))":
     # F[i..i+n-1] is unbalanced
eval balfib "?msd_fib Ai An ~$unbalfib(i,n)":

# what are the lengths of balanced factors of Thue-Morse ?
def unbaltm "E l1,l2,r1,r2 i<=l1 & l1<r1 & r1<i+n & i<=l2
& l2<r2 & r2<i+n & r1+l2=r2+l1 & T[l1]=@0 & T[r1]=@0 &
T[l2]=@1 & T[r2]=@1 & $tmfactoreq(l1+1,l2+1,r1-(l1+1))":
    # T[i..i+n-1] is unbalanced

eval baltm "Ei ~$unbaltm(i,n)":

# computing a linear recurrence bound for Thue-Morse
def tmfactoreq "At (t<n) => T[i+t]=T[j+t]":

eval tmlinrec "Ai, n (n>=3) => Ej (j>=1 & j+18<=9*n) &
     $tmfactoreq(i,i+j,n)": # for all i, n the next 
     occurrence of T[i..i+n-1] is at distance <= 9n-18

eval tmopt "Am Ei,n (n>=m) & Aj 
     (j>=1 & $tmfactoreq(i,i+j,n)) => j+18>=9*n":
     # there are arbitrarily large factors where next 
     # occurrence is at distance >= 9n-18.

# additive number theory on the lower & upper Wythoff sequences
reg end0 msd_fib "(0|1)*0":
reg end1 msd_fib "(0|1)*1":
def lower "?msd_fib $end0(n-1)":
def upper "?msd_fib $end1(n-1)":
eval kaw "?msd_fib ~Ea,b,c (n=a+b+c) & $lower(a) &
     $upper(b) & $upper(c)":

# counting novel factors in the Thue-Morse sequence
def tmfactoreq "At (t<n) => T[i+t]=T[j+t]":
eval tmsw n "Aj (j<i) => ~$tmfactoreq(i,j,n)":
     # T[i..i+n-1] is a novel factor

# counting special factors in the Thue-Morse sequence
def tmfactoreq "At (t<n) => T[i+t]=T[j+t]":
def rtspec "Ej $tmfactoreq(i,j,n) & T[i+n]!=T[j+n]":
eval tmrs n "$rtspec(i,n) & Aj (j<i) => ~$tmfactoreq(i,j,n)":

# determining the subword complexity function of Thue-Morse
# via clumping
def nf "Aj (j<i) => Et (t<n) & T[i+t] != T[j+t]": # novel factor
def allnovel "Ai (x<=i & i<y) => $nf(i,z)":
def allnotnov "Ai (x<=i & i<y) => ~$nf(i,z)":

def tmsub "E a2,a3,a4,a5,b1,b2,b3,b4,b5 (b1<=a2 & 
a2<=b2 & b2<=a3 & a3<=b3 & b3<=a4 & a4<=b4 & b4<=a5 & a5<=b5)
& $allnovel(0,b1,n) & $allnovel(a2,b2,n) & $allnovel(a3,b3,n) &
$allnovel(a4,b4,n) & $allnovel(a5,b5,n) & $allnotnov(b1,a2,n) &
$allnotnov(b2,a3,n) & $allnotnov(b3,a4,n) & $allnotnov(b4,a5,n) &
(Ai (i>=b5) => ~$nf(i,n)) & s = b1+(b2-a2)+(b3-a3)+(b4-a4)+(b5-a5)":

# checking a formula for the subword complexity of Thue-Morse
reg power2 msd_2 "0*10*":
eval tmsubcheck "Ax,i,s,n (((n>=3 & $power2(x) & n=x+i & i>=1
& 2*i<=x & s+4=3*x+4*i) => $tmsub(n,s)) & ((n>=3 & $power2(x) &
2*n=3*x+2*i & i>=1 & 2*i<=x & s+2=5*x+2*i) => $tmsub(n,s)))":

# no factor of a paperfolding sequences is a 3+ power
eval pfhaslcube "?lsd_2 En (n>0) & Ef Ei i>=1 &
Ak (k<=2*n) => PF[f][i+k] = PF[f][i+k+n]":

# two different ways to check equality of Tribonacci factors
def tribfaceq "?msd_trib At (t<n) => TR[i+t]=TR[j+t]":
	 # Does TR[i..i+n-1]=TR[j..j+n-1] ?
# This didn't run to completion, even after allocating 120 gigs

def tribfaceq2 "?msd_trib Ax Ay (x>=i & x<i+n & x+j=y+i) 
	=> TR[x]=TR[y]":  # Does TR[i..i+n-1]=TR[j..j+n-1] ?
# This takes only 35 secs of CPU time and uses 7.2 gigs of storage 


# asserts that F[j..j+n-1] is F[i..i+n-1], shifted by t
def fibshift "?msd_fib $fibfactoreq(j,i+t,n-t) &
     $fib(i,(j+n)-t,t)": 

# asserts that F[j..j+n-1] is a conjugate of F[i..i+n-1]
def fibconj "?msd_fib Et (t<n) & $fibshift(i,j,n,t)":
# but it fails for the empty string, replace with

def fibconj "?msd_fib Et (t<=n) & $fibshift(i,j,n,t)":