def ndmodk "(n=k & n<2*k & z+k=n & r=1) | (n>=2*k & n<3*k & z+2*k=n & r=2) | (n>=3*k & n<4*k & z+3*k=n & r=3)": def h0001 "(Er,z r<=2 & \$ndmodk(k,n,r,z) & T[z]=@1) | (Er,z r=3 & \$ndmodk(k,n,r,z) & T[z]=@0)": def h0010 "(Er,z (r<=1|r=3) & \$ndmodk(k,n,r,z) & T[z]=@1) | (Er,z r=2 & \$ndmodk(k,n,r,z) & T[z]=@0)": def h0011 "(Er,z r<=1 & \$ndmodk(k,n,r,z) & T[z]=@1) | (Er,z (r=2|r=3) & \$ndmodk(k,n,r,z) & T[z]=@0)": def h0101 "(Er,z (r=0|r=2) & \$ndmodk(k,n,r,z) & T[z]=@1) | (Er,z (r=1|r=3) & \$ndmodk(k,n,r,z) & T[z]=@0)": def h0110 "(Er,z (r=0|r=3) & \$ndmodk(k,n,r,z) & T[z]=@1) | (Er,z (r=1|r=2) & \$ndmodk(k,n,r,z) & T[z]=@0)": def test0001 "Au,v (u>=i & u<=i+2*n & v=u+n) => (\$h0001(k,u) <=> \$h0001(k,v))":: eval check0001 "~Ek,i,n n>=1 & k>=1 & (i+3*n<4*k) & \$test0001(i,k,n)": def test0010 "Au,v (u>=i & u<=i+2*n & v=u+n) => (\$h0010(k,u) <=> \$h0010(k,v))":: eval check0010 "~Ek,i,n n>=1 & k>=1 & (i+3*n<4*k) & \$test0010(i,k,n)": def test0011 "Au,v (u>=i & u<=i+2*n & v=u+n) => (\$h0011(k,u) <=> \$h0011(k,v))":: eval check0011 "~Ek,i,n n>=1 & k>=1 & (i+3*n<4*k) & \$test0011(i,k,n)": def test0101 "Au,v (u>=i & u<=i+2*n & v=u+n) => (\$h0101(k,u) <=> \$h0101(k,v))":: eval check0101 "~Ek,i,n n>=1 & k>=1 & (i+3*n<4*k) & \$test0101(i,k,n)": def test0110 "Au,v (u>=i & u<=i+2*n & v=u+n) => (\$h0110(k,u) <=> \$h0110(k,v))":: eval check0110 "~Ek,i,n n>=1 & k>=1 & (i+3*n<4*k) & \$test0110(i,k,n)": def tpsa "k>0 & 2*i>=k & i T[j]=T[k+j-i]": def tpsb "k>0 & 2*i>=k & i T[j]!=T[k+j-i]":