reg power4 msd_4 "0*10*":
reg evenpower4 msd_4 "0*1(00)*":
reg oddpower4 msd_4 "0*10(00)*":
eval test2 "?msd_4 HC[0]=@0":
eval test3 "?msd_4 Ax,t ($power4(x) & t<x) =>
     ((HC[t]=@0 <=> HC[x+t]=@1) & (HC[t]=@1 <=> HC[x+t]=@0)
     &(HC[t]=@2 <=> HC[x+t]=@3) & (HC[t]=@3 <=> HC[x+t]=@2))": 
eval test4 "?msd_4 Ax,t ($power4(x) & t+1<x) =>
     ((HC[t]=@0 <=> HC[2*x+t]=@1) & (HC[t]=@1 <=> HC[2*x+t]=@0)
     &(HC[t]=@2 <=> HC[2*x+t]=@3) & (HC[t]=@3 <=> HC[2*x+t]=@2))": 
eval test5 "?msd_4 Ax ($oddpower4(x) => HC[3*x-1]=@3) &
     ($evenpower4(x) => HC[3*x-1]=@2)":
eval test6 "?msd_4 Ax,t ($power4(x) & t+1<x) =>
     ((HC[t]=@0 <=> HC[3*x+t]=@2) & (HC[t]=@1 <=> HC[3*x+t]=@3)
     &(HC[t]=@2 <=> HC[3*x+t]=@0) & (HC[t]=@3 <=> HC[3*x+t]=@1))": 
eval test7 "?msd_4 Ax ($oddpower4(x) => HC[x-1]=@1) &
     ($evenpower4(x) => HC[x-1]=@0)":