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 (\$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 (\$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 (\$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 (\$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 (\$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 (\$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 (\$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 (\$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 X[j]=X[k+j-i]": def x_pref_suff_01 "k>0 & 2*i>=k & i X[j]!=X[k+j-i]": def y_pref_suff_00 "k>0 & 2*i>=k & i Y[j]=Y[k+j-i]": def y_pref_suff_01 "k>0 & 2*i>=k & i Y[j]!=Y[k+j-i]":