eval fn1 "An Ex,y HS[?msd_4 n][x][y]=@1":
# f(n) takes an ordered pair value for each n
eval fn2 "An,x,y,xp,yp (HS[?msd_4 n][x][y]=@1 & HS[?msd_4 n][xp][yp]=@1) => (x=xp & y=yp)": 
# f(n) takes only one value for each n
eval check_up "An (HC[?msd_4 n]=@0 <=> Ex,xp,y,yp HS[?msd_4 n][x][y]=@1 & HS[?msd_4 n+1][xp][yp]=@1 & xp=x & yp=y+1)":
eval check_right "An (HC[?msd_4 n]=@1 <=> Ex,xp,y,yp HS[?msd_4 n][x][y]=@1 & HS[?msd_4 n+1][xp][yp]=@1 & xp=x+1 & yp=y)":
eval check_down "An (HC[?msd_4 n]=@2 <=> Ex,xp,y,yp HS[?msd_4 n][x][y]=@1 &
HS[?msd_4 n+1][xp][yp]=@1 & xp=x & yp+1=y)":
eval check_left "An (HC[?msd_4 n]=@3 <=> Ex,xp,y,yp HS[?msd_4 n][x][y]=@1 & HS[?msd_4 n+1][xp][yp]=@1 & xp+1=x & yp=y)":
eval allhit "Ax,y En HS[?msd_4 n][x][y]=@1":
eval hitonce "An,np,x,y (HS[?msd_4 n][x][y]=@1 & HS[?msd_4 np][x][y]=@1)
=> (?msd_4 n=?msd_4 np)":