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 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)":