def h0010b "(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 test0010b "Au,v (u>=i & u<i+2*n & v=u+n) =>
   ($h0010b(k,u) <=> $h0010b(k,v))"::
def check0010b "~Ei,n n>=1 & (i+3*n<4*k) & $test0010b(i,k,n)"::

def h0011b "(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 test0011b "Au,v (u>=i & u<i+2*n & v=u+n) =>
   ($h0011b(k,u) <=> $h0011b(k,v))"::
def check0011b "~Ei,n n>=1 & (i+3*n<4*k) & $test0011b(i,k,n)"::

def h0101b "(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 test0101b "Au,v (u>=i & u<i+2*n & v=u+n) =>
   ($h0101b(k,u) <=> $h0101b(k,v))"::
def check0101b "~Ei,n n>=1 & (i+3*n<4*k) & $test0101b(i,k,n)"::

def h0110b "(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 test0110b "Au,v (u>=i & u<i+2*n & v=u+n) =>
   ($h0110b(k,u) <=> $h0110b(k,v))"::
def check0110b "~Ei,n n>=1 & (i+3*n<4*k) & $test0110b(i,k,n)"::

def hcubefree "$check0010b(k) & $check0011b(k) & $check0101b(k) &
   $check0011b(k)":

def f0010 "(Er,z (r<=1|r=3) & $ndmodk(k,n,r,z) & X[z]=@1) |
   (Er,z r=2 & $ndmodk(k,n,r,z) & X[z]=@0)":
def testf0010 "Au,v (u>=i & u<i+2*n & v=u+n) =>
   ($f0010(k,u) <=> $f0010(k,v))"::
def checkf0010 "~Ei,n n>=1 & (i+3*n<4*k) & $testf0010(i,k,n)"::
def g0010 "(Er,z (r<=1|r=3) & $ndmodk(k,n,r,z) & Y[z]=@1) |
   (Er,z r=2 & $ndmodk(k,n,r,z) & Y[z]=@0)":
def testg0010 "Ax (x<2*n) =>($g0010(k,i+x) <=> $g0010(k,i+n+x))"::
def checkg0010 "~Ei,n n>=1 & (i+3*n<4*k) & $testg0010(i,k,n)"::

def f0011 "(Er,z (r<=1|r=3) & $ndmodk(k,n,r,z) & X[z]=@1) |
   (Er,z r=2 & $ndmodk(k,n,r,z) & X[z]=@0)":
def testf0011 "Au,v (u>=i & u<i+2*n & v=u+n) =>
   ($f0011(k,u) <=> $f0011(k,v))"::
def checkf0011 "~Ei,n n>=1 & (i+3*n<4*k) & $testf0011(i,k,n)"::
def g0011 "(Er,z (r<=1|r=3) & $ndmodk(k,n,r,z) & Y[z]=@1) |
   (Er,z r=2 & $ndmodk(k,n,r,z) & Y[z]=@0)":
def testg0011 "Ax (x<2*n) =>($g0011(k,i+x) <=> $g0011(k,i+n+x))"::
def checkg0011 "~Ei,n n>=1 & (i+3*n<4*k) & $testg0011(i,k,n)"::

def f0101 "(Er,z (r<=1|r=3) & $ndmodk(k,n,r,z) & X[z]=@1) |
   (Er,z r=2 & $ndmodk(k,n,r,z) & X[z]=@0)":
def testf0101 "Au,v (u>=i & u<i+2*n & v=u+n) =>
   ($f0101(k,u) <=> $f0101(k,v))"::
def checkf0101 "~Ei,n n>=1 & (i+3*n<4*k) & $testf0101(i,k,n)"::
def g0101 "(Er,z (r<=1|r=3) & $ndmodk(k,n,r,z) & Y[z]=@1) |
   (Er,z r=2 & $ndmodk(k,n,r,z) & Y[z]=@0)":
def testg0101 "Ax (x<2*n) =>($g0101(k,i+x) <=> $g0101(k,i+n+x))"::
def checkg0101 "~Ei,n n>=1 & (i+3*n<4*k) & $testg0101(i,k,n)"::

def f0110 "(Er,z (r<=1|r=3) & $ndmodk(k,n,r,z) & X[z]=@1) |
   (Er,z r=2 & $ndmodk(k,n,r,z) & X[z]=@0)":
def testf0110 "Au,v (u>=i & u<i+2*n & v=u+n) =>
   ($f0110(k,u) <=> $f0110(k,v))"::
def checkf0110 "~Ei,n n>=1 & (i+3*n<4*k) & $testf0110(i,k,n)"::
def g0110 "(Er,z (r<=1|r=3) & $ndmodk(k,n,r,z) & Y[z]=@1) |
   (Er,z r=2 & $ndmodk(k,n,r,z) & Y[z]=@0)":
def testg0110 "Ax (x<2*n) =>($g0110(k,i+x) <=> $g0110(k,i+n+x))"::
def checkg0110 "~Ei,n n>=1 & (i+3*n<4*k) & $testg0110(i,k,n)"::

def mod12 "Ej k=12*j+r":
def fcubefree "$checkf0010(k) & $checkf0011(k) & $checkf0101(k) &
   $checkf0110(k)":
def gcubefree "$checkg0010(k) & $checkg0011(k) & $checkg0101(k) &
   $checkg0110(k)":
eval thm2a "Ak ($mod12(k,1)|$mod12(k,5)) => $fcubefree(k)":
eval thm2b "Ak ($mod12(k,7)|$mod12(k,11)) => $gcubefree(k)":

def x_pref_suff_00 "k>0 & 2*i>=k & i<k & Aj (j<i) => X[j]=X[k+j-i]":
def x_pref_suff_01 "k>0 & 2*i>=k & i<k & Aj (j<i) => X[j]!=X[k+j-i]":
def y_pref_suff_00 "k>0 & 2*i>=k & i<k & Aj (j<i) => Y[j]=Y[k+j-i]":
def y_pref_suff_01 "k>0 & 2*i>=k & i<k & Aj (j<i) => Y[j]!=Y[k+j-i]":