eval test30_1 "An Ey $f30(n,y)":
eval test30_2 "~En,y1,y2 $f30(n,y1) & $f30(n,y2) & ?msd_3 y1!=y2":
morphism tm4 "0->0110 1->1001":
promote TM4 tm4:
eval test30_3 "?msd_4 An,x (n>=1 & $f30(n, ?msd_3 x) &
   TM4[3*n]=@0) => $f30(n+1, ?msd_3 x+1)":
eval test30_4 "?msd_4 An,x (n>=1 & $f30(n, ?msd_3 x) & 
   TM4[3*n]=@1) => $f30(n+1, ?msd_3 x-1)":
eval test30_5 "?msd_4 An,y (n>=1 & $f30(n,y)) => ?msd_3 y>0":
eval test30_6 "?msd_4 Ay En,x $f30(n,x) & ?msd_3 x>y":

reg p34 msd_3 msd_4 "([0,0]|[1,1]|[2,2])*":
eval bnd1 "?msd_4 An,x,m ($f30(n,x) & $p34(x,m)) => n<=m":
eval bnd2 "?msd_4 An,x,m (n>=1 & $f30(n,x) & $p34(x,m)) => 2*m+1<=3*n":
def bnd3 "?msd_4 Ex $f30(n,x) & $p34(x,n)":
def bnd4 "?msd_4 Ex,m $f30(n,x) & $p34(x,m) & 2*m+1=3*n":

reg power43 msd_4 msd_3 "[0,0]*[1,1][0,0]*":
eval bound1 "?msd_4 Ax,y,w,z ($power43(x,y) & 3*w=260*x+1 & 
   ?msd_3 z=55*y) => $f30(w,z)":
eval bound2 "?msd_4 Ax,y,w,z ($power43(x,y) & w=2*x &
   ?msd_3 z=2*y) => $f30(w,z)":

eval test31_1 "An Ey $mf31(n,y)":
eval test31_2 "~En,y1,y2 $mf31(n,y1) & $mf31(n,y2) & ?msd_3 y1!=y2":
eval test31_3 "?msd_4 An,x (n>=1 & $mf31(n, ?msd_3 x) &
   TM4[3*n+1]=@1) => $mf31(n+1, ?msd_3 x+1)":
eval test31_4 "?msd_4 An,x (n>=1 & $mf31(n, ?msd_3 x) &
   TM4[3*n+1]=@0) => $mf31(n+1, ?msd_3 x-1)":
eval test31_5 "?msd_4 An,y (n>=1 & $mf31(n,y)) => ?msd_3 y>0":
eval test31_6 "?msd_4 Ay En,x $mf31(n,x) & ?msd_3 x>y":

eval test31_bnd1 "?msd_4 An,x,m ($mf31(n,x) & $p34(x,m)) => n<=2*m":
eval test31_bnd2 "?msd_4 An,x,m (n>=1 & $mf31(n,x) & $p34(x,m)) => 2*m+1<=3*n":
def test31_bnd3 "?msd_4 Ex $mf31(n,x) & $p34(x,n)":
def test31_bnd4 "?msd_4 Ex,m $mf31(n,x) & $p34(x,m) & 2*m+1=3*n":

morphism tm16 "0->0110100110010110 1->1001011001101001":
promote TM16 tm16:
eval test51_1 "An Ey $f51(n,y)":
eval test51_2 "~En,y1,y2 $f51(n,y1) & $f51(n,y2) & ?msd_neg_5 y1!=y2":
eval test51_3 "?msd_16 An,x (n>=1 & $f51(n, ?msd_neg_5 x) &
   TM16[5*n+1]=@0) => $f51(n+1, ?msd_neg_5 x+1)":
eval test51_4 "?msd_16 An,x (n>=1 & $f51(n, ?msd_neg_5 x) &
   TM16[5*n+1]=@1) => $f51(n+1, ?msd_neg_5 x-1)":
eval test51_5 "?msd_16 Ay En,x $f51(n,x) & ?msd_neg_5 x>y":
eval test51_6 "?msd_16 Ay En,x $f51(n,x) & ?msd_neg_5 x<y":

reg p165 msd_16 msd_5 "([0,0]|[1,1]|[2,2]|[3,3]|[4,4])*":
eval negvalues51 "?msd_16 An,x,y,w ((?msd_neg_5 x<0) & 
   $f51(n,?msd_neg_5 x) & $conv55((?msd_neg_5 _x),?msd_5 y) &
   $p165(w,?msd_5 y)) => 2*w+3<=5*n":
def negvalues51_match "?msd_16 Ex,y,w (?msd_neg_5 x<0) &
   $f51(n,?msd_neg_5 x) & $conv55((?msd_neg_5 _x),?msd_5 y) &
   $p165(w,?msd_5 y) & 2*w+3=5*n":

def pv51 "?msd_16 Ex,y (?msd_neg_5 x>=0) & $f51(n,?msd_neg_5 x)
   & $conv55((?msd_neg_5 x),?msd_5 y) & $p165(w,?msd_5 y)":
eval f51pcheck "?msd_16 An,w (n>=30 & $pv51(n,w)) => 3412*w+463<=121*n":
def f51p_equal "?msd_16 Ew $pv51(n,w) & 3412*w+463=121*n":

def f51eq0 "?msd_16 $f51(n,?msd_neg_5 0)":