reg pow2_4 msd_4 "0*(1|2)0*";
def eqfac_qma "?msd_4 Ai (i<n) => QMA[x+i]=QMA[y+i]";
def firstfac_qma "?msd_4 Ai (i<x) => ~$eqfac_qma(n,i,x)";
def rs_qma "?msd_4 Ey ($eqfac_qma(n,x,y) & QMA[x+n]!=QMA[y+n])";
def crs_qma "?msd_4 $rs_qma(n,x) & $firstfac_qma(n,x)";
def rs2_qma "?msd_4 Eu,v (u!=v & $crs_qma(n,u) & $crs_qma(n,v) & Ax ($crs_qma(n,x) => (x=u|x=v)))";
def rs3_qma "?msd_4 Eu,v,w (u!=v & u!=w & v!=w & $crs_qma(n,u) & $crs_qma(n,v) & $crs_qma(n,w) & Ax ($crs_qma(n,x) => (x=u|x=v|x=w)))";
def rs4_qma "?msd_4 Eu,v,w,z (u!=v & u!=w & u!=z & v!=w & v!=z & w!=z & $crs_qma(n,u) & $crs_qma(n,v) & $crs_qma(n,w) & $crs_qma(n,z) & Ax ($crs_qma(n,x) => (x=u|x=v|x=w|x=z)))";
def qma_rs4_range "?msd_4 EP ($pow2_4(P) & P>=16 & P<n & n<2*P & 2*n<=3*P)";
def qma_rs3_range "?msd_4 EP ($pow2_4(P) & P>=16 & n<2*P & 2*n>3*P & 4*n<=7*P)";
def qma_rs2_range "?msd_4 EP ($pow2_4(P) & P>=16 & P<=n & n<2*P & (n=P | 4*n>7*P))";
eval qma_rs2_check "?msd_4 An (n>=16 => ($rs2_qma(n) <=> $qma_rs2_range(n)))";
eval qma_rs3_check "?msd_4 An (n>=16 => ($rs3_qma(n) <=> $qma_rs3_range(n)))";
eval qma_rs4_check "?msd_4 An (n>=16 => ($rs4_qma(n) <=> $qma_rs4_range(n)))";
