# 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<m+j) & $evilg(t,v)) => 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<m+j) & $odiousg(t,v)) => 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)":