def odd "Ek n=2*k+1";
def even "Ek n=2*k";
eval thm "Am,n ($odd(m) & $odd(n)) => $even(m+n)":

eval shev1 "Ei,j 0<i & i<j & An (T[n]=T[n+i]|T[n]=T[n+j])":
def shev2 "0<i & i<j & j<k &
   An (T[n]=T[n+i]|T[n]=T[n+j]|T[n]=T[n+k])":

reg isfib msd_fib "0*10*":
reg shift {0,1} {0,1} "([0,0]|[0,1][1,1]*[1,0])*":
def phin "?msd_fib (s=0 & n=0) | Ex $shift(n-1,x) & s=x+1":
def phi2n "?msd_fib (s=0 & n=0) | Ex,y $shift(n-1,x) &
   $shift(x,y) & s=y+2":
def s2uw "?msd_fib ~Em,n,x,y z=x+y & $phi2n(m,x) & $phi2n(n,y)
   & 1<=m & m<=n-1 & n>=2":
# z is not the sum of two upper-Wythoff numbers
# in other words, those z in A260317
def gap "?msd_fib Et,v t<v & $s2uw(t) & $s2uw(v) & (Au (u>t & u<v) => ~$s2uw(u)) & g=v-t":
# gap g between two consecutive numbers in A260317
# in other words, A260311
eval thm "?msd_fib Ax $gap(x) => $isfib(x)":
eval tm2 "?msd_fib Ax $gap(x) <=> (x=1|x=2|x=3|x=5)":

def good "?msd_trib y>x &
   (~Ek k<n & $xaut(k,x)) &
   (~Ek k<n & $xaut(k,y)) &
   (~Ek k<n & $yaut(k,x)) &
   (~Ek k<n & $yaut(k,y)) &
   (~Ek,a,b k<n & $xaut(k,a) & $yaut(k,b) & y-x=b-a) &
   (~Ek,a,b k<n & $xaut(k,a) & $yaut(k,b) & y-x=b+a)":
eval check1 "?msd_trib An,x,y (n>=1 & $xaut(n,x) & $yaut(n,y)) =>
   $good(n,x,y)":
eval check2 "?msd_trib An,x,y (n>=1 & $good(n,x,y)) =>
   (Ez $xaut(n,z) & x>=z)":
eval check3 "?msd_trib An,x,y (n>=1 & $xaut(n,x) & $good(n,x,y)) =>
   (Ez $yaut(n,z) & y>=z)":

eval julien1 "?msd_trib An,x,y,xy,yx ($xaut(n,x) &
   $yaut(n,y) & $xaut(y,xy) & $yaut(x,yx)) =>
   (xy=x+y|yx=x+y)":

def equalblock "At (t<n) => T[i+t]=T[j+t]":
def novelblock "Ak (k<i) => ~$equalblock(i,k,n)":
def countblock n "$novelblock(i,n)":