eval test1 "?msd_4 An,y ($rss(n,y) & RS4[n+1]=@1) => $rss(n+1,?msd_2 y+1)":
eval test2 "?msd_4 An,y ($rss(n,y) & RS4[n+1]=@-1) => $rss(n+1,?msd_2 y-1)":
# show that rss is correct

def even4 "?msd_4 Ek n=2*k":
def odd4 "?msd_4 Ek n=2*k+1":
eval test3 "?msd_4 An,y ($rst(n,y) & ((RS4[n+1]=@1 & $even4(n+1)) | 
   (RS4[n+1]=@-1 & $odd4(n+1)))) => $rst(n+1,?msd_2 y+1)":
eval test4 "?msd_4 An,y ($rst(n,y) & ((RS4[n+1]=@-1 & $even4(n+1)) | 
   (RS4[n+1]=@1 & $odd4(n+1)))) => $rst(n+1, ?msd_2 y-1)":

eval test5 "?msd_4 (An Ey $rss(n,y)) & 
   An ~Ex,y ($rss(n,x) & $rss(n,y) & (?msd_2 x!=y))":
eval test6 "?msd_4 (An Ey $rst(n,y)) & 
   An ~Ex,y ($rst(n,x) & $rst(n,y) & (?msd_2 x!=y))":

eval eq3 "?msd_4 An,x,y,z (n>=1 & $rss(2*n,x) & $rss(n,y) & $rst(n-1,z)) 
   => ?msd_2 x=y+z":

eval eq4 "?msd_4 An,x,y,z ($rss(2*n+1,x) & $rss(n,y) & $rst(n,z)) 
   => ?msd_2 x=y+z":

eval eq5 "?msd_4 An,x,y,z (n>=1 & $rst(2*n,x) & $rss(n,y) & $rst(n-1,z)) 
   => ?msd_2 x+z=y":

eval eq6 "?msd_4 An,x,y,z ($rst(2*n+1,x) & $rss(n,y) & $rst(n,z)) 
   => ?msd_2 x+z=y":


eval eq7 "?msd_4 An,x,y ($rss(4*n,x) & $rss(n,y)) => 
   ((RS4[n]=@1 => ?msd_2 x+1=2*y) & (RS4[n]=@-1 => ?msd_2 x=2*y+1))":

eval eq8 "?msd_4 An,x,y,z ($rss(4*n+1,x) & $rss(4*n+3,y) & $rss(n,z)) 
   => ?msd_2 x=y & x=2*z":

eval eq9 "?msd_4 An,x,y ($rss(4*n+2,x) & $rss(n,y)) => 
   (((RS4[n]=@1 & $even4(n)) => ?msd_2 x=2*y+1) &
   ((RS4[n]=@-1 & $even4(n)) => ?msd_2 x+1=2*y) &
   ((RS4[n]=@1 & $odd4(n)) => ?msd_2 x+1=2*y) &
   ((RS4[n]=@-1 & $odd4(n)) => ?msd_2 x=2*y+1))":


eval eq10 "?msd_4 An,x,y (n>=1 & $rst(4*n,x) & $rst(n-1,y)) => 
   ((RS4[n]=@1 => ?msd_2 x=2*y+1) & (RS4[n]=@-1 => ?msd_2 x+1=2*y))":

eval eq11 "?msd_4 An,x,y (n>=1 & $rst(?msd_4 4*n+1,x) &
   $rst(?msd_4 n-1,y)) => ?msd_2 x=2*y":

eval eq12 "?msd_4 An,x,y,z (n>=1 & $rst(4*n+2,x) &
   $rst(n,y) & $rst(n-1,z)) => ?msd_2 x=y+z":

eval eq13 "?msd_4 An,x,y ($rst(4*n+3,x) & $rst(n,y)) => ?msd_2 x=2*y":


reg rss_int msd_4 msd_4 "[0,0]*[1,3][0,3]*":

eval min_rss "?msd_4 n>=4 & $rss(n, x) & Ei,j $rss_int(i,j) &
   i<=n & n<=j & (Ay,m (i<=m & m<=j & $rss(m,y)) =>
   ?msd_2 y>=x)":

eval max_rss "?msd_4 $rss(n, x) & Ei,j $rss_int(i,j) &
   i<=n & n<=j & (Ay,m (i<=m & m<=j & $rss(m,y)) =>
   ?msd_2 y<=x)":


def omega "?msd_4 $rss(n,k) & At (t>n) => ~$rss(t,k)":

def omegadiff "?msd_4 Et,u $omega((?msd_2 n+1),t) & 
   $omega(n,u) & t=x+u":

def omegas "?msd_4 Ek $rss(n,k) & $omega(k,x)":
eval check_bounds "?msd_4 An,t (n>=2 & $omegas(n,t)) => 3*t+2<=10*n":


eval eq14 "?msd_4 An,x,y ((?msd_2 n>=1) & $omega(n,x) & 
   $omega((?msd_2 2*n), y)) => y=4*x+3":

reg power2 msd_2 "0*10*":
eval eq15 "?msd_4 An,x,y (?msd_2 n>=2 & (~$power2(?msd_2 n+1)) & 
   $omega((?msd_2 n+1),x) & $omega((?msd_2 2*n+1),y)) => y=4*x+2":


reg power4 msd_4 "0*10*":
reg link42 msd_4 msd_2 "([0,0]|[1,1])*":


eval eq16 "?msd_4 An,x,y,z ($power4(x) & x>=4 & 2*n+2<=x & 
   $rss(n,y) & $link42(x,z)) => $rss(n+x,?msd_2 y+z)":
eval eq17 "?msd_4 An,x,y,z ($power4(x) & x>=4 & 2*n>=x & n<x & $rss(n,y)
   & $link42(x,z)) => $rss(n+x,?msd_2 3*z-y)":
eval eq18 "?msd_4 An,x,y,z ($power4(x) & n<x & $rss(n,y) & $link42(x,z))
   => $rss(n+2*x,?msd_2 y+2*z)":
eval eq19 "?msd_4 An,x,y,z ($power4(x) & x<=n & n<2*x & $rss(n,y) &    
   $link42(x,z)) => $rss(n+2*x,?msd_2 4*z-y)":


eval lemma4 "?msd_4 An,x,y,z ($power4(x) & x<=n & n<2*x & 
    $link42(x,z) & $rss(n,y)) => ?msd_2 y<=2*z":

def lemma4a "?msd_4 Ez $power4(x) & x<=n & n<2*x & 
    $link42(x,z) & $rss(n,?msd_2 2*z)":


reg sqrtpow2 msd_4 msd_2 "[0,0]*([1,1]|[0,1][2,0])[0,0]*":
reg oddpow2 msd_4 "0*20*":
eval specval_a "?msd_4 Ax,y $sqrtpow2(x,y) => $rss(x,?msd_2 y+1)":
eval specval_b "?msd_4 Ax,y $sqrtpow2(x,y) => $rss(x-1,?msd_2 y)":
eval specval_c1 "?msd_4 Ax,y ($power4(x) & x>1 & $sqrtpow2(x,y))
   => $rss(x-2, ?msd_2 y+1)":
eval specval_c2 "?msd_4 Ax,y ($oddpow2(x) & $sqrtpow2(x,y)) 
   => $rss(x-2, ?msd_2 y-1)":
eval specval_d "?msd_4 Ax,y ($power4(x) & $link42(x,y)) 
   => $rss(3*x-1,?msd_2 3*y)":
eval specval_e "?msd_4 Ax,y ($oddpow2(x) & $sqrtpow2(x,y)) 
   => $rss(3*x-1,?msd_2 2*y)":
eval specval_f "?msd_4 Ax,y ($power4(x) & x>1 & $link42(x,y)) 
   => $rst(x,?msd_2 y+1)":
eval specval_g "?msd_4 Ax $oddpow2(x) => $rst(x,?msd_2 1)":
eval specval_h "?msd_4 Ax,y ($power4(x) & $link42(x,y)) 
   => $rst(x-1,?msd_2 y)":
eval specval_i "?msd_4 Ax $oddpow2(x) => $rst(x-1,?msd_2 0)":
eval specval_j "?msd_4 Ax,y ($power4(x) & x>1 & $link42(x,y)) 
   => $rst(x-2, ?msd_2 y-1)":
eval specval_k "?msd_4 Ax $oddpow2(x) => $rst(x-2,?msd_2 1)":
eval specval_l "?msd_4 Ax,y $sqrtpow2(x,y) => $rst(3*x-1,y)":


reg rst_int1 msd_4 msd_4 "[0,0]*[1,1][0,3]*":
reg rst_int2 msd_4 msd_4 "[0,0]*[2,3][0,3]*":

eval max_rst1 "?msd_4 n>=2 & $rst(n, ?msd_2 x) & Ei,j $rst_int1(i,j) &
i<=n & n<=j & (Ay,m (i<=m & m<=j & $rst(m,?msd_2 y)) => ?msd_2 y<=x)":

eval max_rst2 "?msd_4 n>=4 & $rst(n, ?msd_2 x) & Ei,j $rst_int2(i,j) &
i<=n & n<=j & (Ay,m (i<=m & m<=j & $rst(m,?msd_2 y)) => ?msd_2 y<=x)":


eval eq24a1 "?msd_4 An,x,y,z ($power4(x) & $link42(x,y) & 3*n+4=4*x & 
   $rss(n,z)) => ?msd_2 z+1=2*y":
eval eq24a2 "?msd_4 An,x,y,z ($power4(x) & $link42(x,y) & n+1=4*x & 
   $rss(n,z)) => ?msd_2 z=2*y":
eval eq24b1 "?msd_4 Ax,y,z ($power4(x) & x>1 & $link42(x,y) & $rst(x,z)) 
   => ?msd_2 z=y+1":
eval eq24b2 "?msd_4 An,x,y,z ($power4(x) & $link42(x,y) & 3*n+2=5*x & 
   $rst(n,z)) => ?msd_2 z+1=y":
eval eq24c "?msd_4 An,s,x,y,w,z ($power4(x) & $link42(x,w) & $link42(y,s) 
   & (?msd_2 s<w) & n+2*y+1=2*x & $rst(n,z)) => ?msd_2 z=2*s":
eval eq24d "?msd_4 An,s,x,y,w,z ($power4(x) & $link42(x,w) & $link42(y,s) 
   & (?msd_2 s<w) & n+2*y+1=4*x & $rst(n,z)) => ?msd_2 z+2*s=2*w":
eval eq24e "?msd_4 Ax,n ($power4(x) & 3*n+2=8*x) => $rst(n,?msd_2 1)":


def maps "?msd_4 Ex $rss(n,x) & $link42(y,x)":
eval ms_lowerbnd "?msd_4 An,y (n>=1 & $maps(n,y)) => y<=3*n+1":
eval ms_upperbnd "?msd_4 An,y (n>=1 & $maps(n,y)) => 3*n+7<=5*y":


eval lowerbnd_tight "?msd_4 Am En,y (n>m) & $maps(n,y) & y=3*n+1":
eval upperbnd_tight "?msd_4 Am En,y (n>m) & $maps(n,y) & 5*y=3*n+7":

def exceptional_set "?msd_4 Em $maps(n,m) & m>2*n":

eval maxcheck "?msd_4 An,x,y,z ($power4(x) & 3*n+1>=4*x & n<2*x
   & $rss(n,y) & $link42(x,z)) => ?msd_2 y<=2*z":

eval J_inequality "?msd_4 An,x,y,z,w,m ($rss(n,m) & $power4(x) & $power4(y) 
   & x>y & $link42(x,w) & $link42(y,z) & 8*x<=3*n+8*y & 3*n+2*y<8*x) 
   => ?msd_2 m+2*z<=4*w":

def left_endpoint "?msd_4 3*z+8*y=8*x":
def right_endpoint "?msd_4 3*z+2*y=8*x":
eval check_all "?msd_4 An (n>=1) => ((~$exceptional_set(n)) |
   (Ex $power4(x) & 4*x<=3*n+1 & n<2*x) |
   (Ex,y,z,w $power4(x) & $power4(y) & x>y & 
   $left_endpoint(x,y,z) & $right_endpoint(x,y,w) & n>=z & n<w) | 
   (Ex $power4(x) & 3*n+2=8*x))":


def mapt "?msd_4 Ex $rst(n,x) & $link42(y,x)":
eval bnd "?msd_4 An,z $mapt(n,z) => z<=n+1":
def except2 "?msd_4 Ez $mapt(n,z) & z=n+1":

eval omegabound "?msd_4 Ak,x,y ($omega(k,x) & $link42(y,k)) => 3*x<=5*y":

eval satz22 n "$rss(?msd_4 k,n)":

eval gfunc n "i<n":

eval tvalues "?msd_4 An,k Em (m>n) & $rst(m,k)":

def counta1 k x "?msd_4 $rst(n,k) & $power4(x) & n<x":

def counta2 k x "?msd_4 Ey $power4(x) & $link42(x,y) & 
   (?msd_2 (k=0 & n+1<y)|(k=y & n=0)|(1<=k & k<y & n+2*k<2*y))":

def countb1 k x "?msd_4 $rst(n,k) & $power4(x) & x>1 & 2*n<x ":

def countb2 k x "?msd_4 Ey $power4(x) & x>1 & $link42(x,y) & 
   (?msd_2 (k=0 & 2*n<y)|(1<=k & k<y & n+k<y))":


def alpha "?msd_4 $rss(n,k) & At (t<n) => ~$rss(t,k)":

def alphap "?msd_4 $rst(n,k) & At (t<n) => ~$rst(t,k)":
eval verify_alphap "?msd_4 Ak,t ((?msd_2 k>=1) & $alphap(k,t)) => 
   $link42(t+1,k)":


def even2 "Ek n=2*k":
def curve "?msd_4 $rss(n,x) & $rst(n,y)":
eval curvecheck "?msd_4 Ax,y (?msd_2 x>=y & x+y>0 & $even2(?msd_2 x-y)) <=> 
   En $curve(n,x,y)":
eval curvecheck3 "?msd_4 Ex,y,n1,n2,n3 n1<n2 & n2<n3 &
   $curve(n1,x,y) & $curve(n2,x,y) & $curve(n3,x,y)":



eval selfint1 "?msd_4 Em,x1,y1,x2,y2,n $curve(m,x1,y1) & 
   $curve(m+1,x2,y2) & $curve(n,x1,y1) & $curve(n+1,x2,y2) & m!=n":

eval selfint2 "?msd_4 Em,x1,y1,x2,y2,n $curve(m,x1,y1) & 
   $curve(m+1,x2,y2) & $curve(n+1,x1,y1) & $curve(n,x2,y2) & m!=n":