def ndmodk "(n<k & z=n & r=0) | (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<k & Aj (j<i) => T[j]=T[k+j-i]":
def tpsb "k>0 & 2*i>=k & i<k & Aj (j<i) => T[j]!=T[k+j-i]":