reg pow2_k0_4 msd_4 "0*(1(000)*|20(000)*)";
reg pow2_k1_4 msd_4 "0*(100(000)*|2(000)*)";
reg pow2_k2_4 msd_4 "0*(10(000)*|200(000)*)";
reg pow2_4 msd_4 "0*(1|2)0*";
def eqfac_m2a "?msd_4 Ai (i<n) => M2A[x+i]=M2A[y+i]";
def firstfac_m2a "?msd_4 Ai (i<x) => ~$eqfac_m2a(n,i,x)";
def rs_m2a "?msd_4 Ey ($eqfac_m2a(n,x,y) & M2A[x+n]!=M2A[y+n])";
def crs_m2a "?msd_4 $rs_m2a(n,x) & $firstfac_m2a(n,x)";
def rs2_m2a "?msd_4 Eu,v (u!=v & $crs_m2a(n,u) & $crs_m2a(n,v) & Ax ($crs_m2a(n,x) => (x=u|x=v)))";
def rs4_m2a "?msd_4 Eu,v,w,z (u!=v & u!=w & u!=z & v!=w & v!=z & w!=z & $crs_m2a(n,u) & $crs_m2a(n,v) & $crs_m2a(n,w) & $crs_m2a(n,z) & Ax ($crs_m2a(n,x) => (x=u|x=v|x=w|x=z)))";
def m2a_rs4_range "?msd_4 EP (P>=8 & P<n & n<2*P & (($pow2_k0_4(P) & 4*n<=7*P) | ($pow2_k1_4(P) & 2*n<=3*P)))";
def m2a_rs2_range "?msd_4 n>=1 & ~$m2a_rs4_range(n)";
eval m2a_rs2_check "?msd_4 An (n>=8 => ($rs2_m2a(n) <=> $m2a_rs2_range(n)))";
eval m2a_rs4_check "?msd_4 An (n>=8 => ($rs4_m2a(n) <=> $m2a_rs4_range(n)))";
