(Walnut) % Following code finds the first position of the longest word w of length 2(n+1) or A299174(n) with no length-(n+1) factors of w repeated.% def fibfactoreq "?msd_fib At (t F[i+t]=F[j+t]"; %Asserts that two factors of length n starting at positions i and j resp. in the fibonacci word are equal.% def fibwnuf "?msd_fib Aj,k (i<=j & j+n ~$fibfactoreq(j,k,n)"; %Accepts all the values in tuple (i,n,x) for which a word with no length-n factors repeated in w is of length x and starts at position i.% def fiblongwn "?msd_fib $fibwnuf(i,n,x) & Ay (y>x) => ~$fibwnuf(i,n,y)"; %This accepts only the longest words with unique length-n factors from above formulation.% % The upper bound of the length of the longest w of unique length-x factors is 2x since the subword complexity of length-x factors of the fibonacci word is x+1. It is enough to show that a word of length 2x exists with no repeated length-x factors. This is encoded in Walnut as follows:% eval fiblongwlen2n "?msd_fib An (n>0) => Ek (Ai,j (k<=i & i ~$ffactoreq(i,j,n))"; %This returns TRUE% def fiblongwnfp "?msd_fib $fiblongwn(i,n,x) & Aj (j ~$fibwnuf(j,n,x)"; %This accepts the first position of the longest words accepted in "fiblongwn".% % To prove that the pattern of first positions of these longest words w(n) in the Fibonacci word is the same as A361989(n-1) for all n>0 (Notice the shift in index of the sequence as we begin with n=1,2,3,...), we first state a construction of w as follows: w(n):= (F_p(n-1))^R 0 1 F_p(n-1) or (F_p(n-1))^R 1 0 F_p(n-1) such that |w(n)|=2n; F_p(t) is the length-t prefix of the Fibonacci word and u^R is any word u written in reverse. This is encoded in Walnut as follows% eval fiblongwconchk "?msd_fib An,i (n>0 & $fiblongwnfp(i,n,2*n)) => ((At (t+1 F[i+t]=F[n-2-t]) & ((F[i+n-1]=@0 & F[i+n]=@1)|(F[i+n-1]=@1 & F[i+n]=@0)) & (At (t+1 F[i+n+1+t]=F[t]))"; % This returns TRUE.% % Now, we check TWO boundary patterns in the list of first positions of these words w(n): The first condition is: 1. For all k>2, the factor length n=F_k implies the first position of the longest word with no repeated length-n factors is i=F_{k-1}-1. E.g. n=3=F_4 then i(n)=F_{4-1}-1=F_3-1=2-1=1 which can be confirmed by checking A361989(3-1)=1. We encode this in Walnut as follows:% reg fiboyes msd_fib "0*10*"; %Checks that the argument of the function fiboyes is a fibonacci number greater than 0.% reg fibshift msd_fib "[0,0]*[0,1][1,0][0,0]*"; % Checks that the pair of arguments of the function fibshift are simultaneously the fibonacci numbers F_k and F_{k-1} respectively for all k>2.% eval fibnfposrelchk "?msd_fib Ai,n (n>0 & $fiblongwnfp(i,n,2*n) & $fiboyes(i) & $fiboyes(n)) => $fibshift(i+1,n)"; % This checks if all positions i and factor-lengths n in the longest word defined in fiblongwnfp are fibonacci numbers then the relation fibshift is preserved for arguments i+1 and n. % %Now, the second condition is: 2. For all k>2, the factor length n=F_k-1 implies the first position of the longest word with no repeated length-n factors is i=0. E.g. n=F_5-1=4 then i(n)=0 which can be confirmed by checking A361989(4-1)=0. We encode this in Walnut as follows:% eval fibnfpos0relchk "?msd_fib Ai,n (n>0 & $fiblongwnfp(i,n,2*n) & $fiboyes(n+1)) => F[i]=F[0]"; %This checks the required query and returns TRUE.% %Now along with conditions 1 and 2, and the construction check of the longest word "fiblongwconchk", the first positions shift by 1 to the left because of the structure of the longest word w and once it hits 0, we prove from the boundary conditions that we easily locate the first position of the next longest word in the list. so the pattern of values in the sequence A361989 is as follows: F_k-1, F_k-2,...,0,F_{k+1}-1,F_{k+1}-2,...,0,F_{k+2}-1,... for all positive integers k>2. So with induction argument, one can check that one obtains the sequence A361989(n-1) for the first positions of the longest words with no repeated length-n factors in the fibonacci word.%