reg isfib msd_fib "0*10*":
reg evenfib msd_fib "0*1(00)*":
reg oddfib msd_fib "0*10(00)*":
reg adjfib msd_fib msd_fib "([0,0]*[1,1])|[0,0]*[1,0][0,1][0,0]*":
def ffactoreq "?msd_fib At (t<n) => F[i+t]=F[j+t]":
def suff "?msd_fib n>=x & x>=y & y>=1 & $ffactoreq(n-x,(n+y)-x,x-y)":
reg shift {0,1} {0,1} "([0,0]|[0,1][1,1]*[1,0])*":
def phi2n "?msd_fib (s=0 & n=0) | Ex,y $shift(n-1,x) & $shift(x,y) & s=y+2":
def good "?msd_fib Ex,y,z $suff(n,x,y) & $phi2n(y,z) & x>z":

def b1 "?msd_fib $isfib(x) & $isfib(y) & x>2*y & y>=2 & n+1+y=x":
def b2 "?msd_fib $isfib(x) & $oddfib(y) & x>2*y & n>=y & y>=2 & n+y=x":

eval test "?msd_fib An (n>=2) => ( (~$good(n)) <=> (Ex,y $b1(n,x,y)|$b2(n,x,y)) )":

eval check1 "?msd_fib An,x,y,z,w (n>=2 & $b1(n,x+y,w+z) & $adjfib(x,y) & $adjfib(w,z) & z>=1 & x>w & n+w+z+1=x+y) => ($suff(n,w+z-1,z) & $suff(n,n,y))":

eval check2a "?msd_fib An,x,y,z,w (n>=3 & $b2(n,x+y,w+z) & $adjfib(x,y) & $adjfib(w,z) & n+w+z=x+y) => $suff(n,n,y)":
eval check2b "?msd_fib An,x,y,z,w (n>=3 & $b2(n,x+y,w+z) & $adjfib(x,y) & $adjfib(w,z) & n+w+z=x+y & w>=2) => $suff(n,w+z,z)":

def emm52 "?msd_fib Ex,y $suff(n,x,y) & 5*y<=2*x":

def has_suff "?msd_fib Ex,y $suff(n,x,y) & 5*y<2*x":
def largest_index "?msd_fib (~$has_suff(n)) & Am (m>n) => $has_suff(m)":
test largest_index 1: