# proof of Lemma 2 def evil123rep "Ej,k,l (T[j]=@0) & (T[k]=@0) & (T[l]=@0) & j>=m & k>=m & l>=m & (n=j | n=j+k | n=j+k+l)": def evil4rep "Ei,j,k,l (T[i]=@0) & (T[j]=@0) & (T[k]=@0) & (T[l]=@0) & i >= m & j>=m & k>=m & l>=m & (n=j+k+l+m)": eval evilcheck "Am,n \$evil4rep(m,n) => \$evil123rep(m,n)": # proof of Theorem 1 def evilg "(Aj (j>n) => \$evil123rep(2*m,j)) & ~\$evil123rep(2*m,n)": # proof of Theorem 6 eval upperb "Am,n \$evilg(m,n) => n <= 6*m+7": eval upperopt "Ai Em,n (m>i) & \$evilg(m,n) & n=6*m+7": eval lowerb "Am,n \$evilg(m,n) => n >= 4*m": eval loweropt "Ai Em,n (m>i) & \$evilg(m,n) & n=4*m": # proof of Theorem 8 eval evilgdiff "Ai Ej,m,n1,n2 (j>=i) & \$evilg(m,n1) & \$evilg(m+1,n2) & n2=n1+j": eval evalmonotone "Ai Ej,m,u (j>=i) & \$evilg(m,u) & (At,v ((t>m) & (t u=v)": # analogues of the theorems above for the odious numbers def odious123rep "Ej,k,l (T[j]=@1) & (T[k]=@1) & (T[l]=@1) & j>=m & k>=m & l>=m & (n=j | n=j+k | n=j+k+l)": def odious4rep "Ei,j,k,l (T[i]=@1) & (T[j]=@1) & (T[k]=@1) & (T[l]=@1) & i >= m & j>=m & k>=m & l>=m & (n=j+k+l+m)": eval odiouscheck "Am,n \$odious4rep(m,n) => \$odious123rep(m,n)": def odiousg "(Aj (j>n) => \$odious123rep(2*m,j)) & ~\$odious123rep(2*m,n)": eval upperb2 "Am,n ((m>=1) & \$odiousg(m,n)) => n <= 6*m-1": eval upperopt2 "Ai Em,n (m>i) & \$odiousg(m,n) & n=6*m-1": eval lowerb2 "Am,n \$odiousg(m,n) => n >= 4*m": eval loweropt2 "Ai Em,n (m>i) & \$odiousg(m,n) & n=4*m": eval odiousgdiff "Ai Ej,m,n1,n2 (j>=i) & \$odiousg(m,n1) & \$odiousg(m+1,n2) & n2=n1+j": eval evalmonotone2 "Ai Ej,m,u (j>=i) & \$odiousg(m,u) & (At,v ((t>m) & (t u=v)": # before running the following commands you need to put # the files fibinc.txt and shift.txt, supplied elsewhere, in # the directory "Automata Library" # proof of Theorem 11 def fibna "?msd_fib ((s=0)&(n=0)) | Et,u \$fibinc(u,n) & \$shift(u,t) & \$fibinc(t,s)": def fibna2 "?msd_fib ((s=0)&(n=0)) | Et,u,v,w \$fibinc(u,n) & \$shift(u,t) & \$shift(t,v) & \$fibinc(v,w) & \$fibinc(w,s)": # proof of Lemma 12 def lower12rep "?msd_fib Ej,k (F[j-1]=@0) & (F[k-1]=@0) & j>=m & k>=m & (n=j|n=j+k)": def lower3rep "?msd_fib Ej,k,l (F[j-1]=@0) & (F[k-1]=@0) & (F[l-1]=@0) & j>=m & k>=m & l>=m & n=j+k+l": eval lowercheck "?msd_fib Am An \$lower3rep(m,n) => \$lower12rep(m,n)": # proof of Lemma 13 def lowerunrep "?msd_fib (Aj (j>n) => \$lower12rep(m,j)) & ~\$lower12rep(m,n)": def lowerg "?msd_fib Et \$fibna(m,t) & \$lowerunrep(t,n)": # proof of Theorem 14 eval lowerb1 "?msd_fib Am En,r \$lowerg(m,n) & \$fibna(m,r) & n+3>=2*r": eval lowerb2 "?msd_fib Am En,r \$lowerg(m,n) & \$fibna(m,r) & n<=2*r+1": eval lowerbinf1 "?msd_fib As Em,n,r (m>=s) & \$lowerg(m,n) & \$fibna(m,r) & n+3>=2*r": eval lowerbinf2 "?msd_fib As Em,n,r (m>=s) & \$lowerg(m,n) & \$fibna(m,r) & n<=2*r+1": # proof of Theorem 16 eval lowerdiff "?msd_fib Am Eu,v \$lowerg(m,u) & \$lowerg(m+1,v) & (v=u|v=u+2|v=u+3|v=u+5|v=u+6|v=u+8)": def ldi "?msd_fib Am Et,u,v (t>=m) & \$lowerg(t,u) & \$lowerg(t+1,v) & v=u+d": eval lowerdiffinfcheck "?msd_fib \$ldi(0) & \$ldi(2) & \$ldi(3) & \$ldi(5) & \$ldi(6) & \$ldi(8)": # analogues of the theorems above for the upper Wythoff sequence: def upper123rep "?msd_fib Ej,k,l (F[j-1]=@1) & (F[k-1]=@1) & (F[l-1]=@1) & j>=m & k>=m & l>=m & (n=j | n=j+k | n=j+k+l )": def upper4rep "?msd_fib Ei,j,k,l (F[i-1]=@1) & (F[j-1]=@1) & (F[k-1]=@1) & (F[l-1]=@1) & i>=m & j>=m & k>=m & l>=m & n=i+j+k+l": eval uppercheck "?msd_fib Am An (m>=3 & \$upper4rep(m,n)) => \$upper123rep(m,n)": def upperunrep "?msd_fib (Aj (j>n) => \$upper123rep(m,j)) & ~\$upper123rep(m,n)": def upperg "?msd_fib Et \$fibna2(m,t) & \$upperunrep(t,n)": eval upperb1 "?msd_fib Am En,r \$upperg(m,n) & \$fibna2(m,r) & n+5>=3*r": eval upperb2 "?msd_fib Am En,r \$upperg(m,n) & \$fibna2(m,r) & n<=3*r+20": eval upperbinf1 "?msd_fib As Em,n,r (m>=s) & \$upperg(m,n) & \$fibna2(m,r) & n+5>=3*r": eval upperbinf2 "?msd_fib As Em,n,r (m>=s) & \$upperg(m,n) & \$fibna2(m,r) & n<=3*r+20": eval upperdiff "?msd_fib Am Eu,v \$upperg(m,u) & \$upperg(m+1,v) & (v=u|v=u+3|v=u+5|v=u+8|v=u+11|v=u+13|v=u+18|v=u+21|v=u+23|v=u+26|v=u+31)": def udi "?msd_fib Am Et,u,v (t>=m) & \$upperg(t,u) & \$upperg(t+1,v) & v=u+d": eval upperdiffinfcheck "?msd_fib \$udi(0) & \$udi(3) & \$udi(5) & \$udi(8) & \$udi(11) & \$udi(13) & \$udi(18) & \$udi(21) & \$udi(23) & \$udi(26) & \$udi(31)":