def sq021 "(n > 3) & (1 <= p) & (2*p <= n) & (s <= i) & (i < s+n) & (Aj ((i<=j)&(j C[j] = C[j+p]) & (Aj ((i<=j)&(j C[j] = @0) & (Aj ((j>=i)&(j C[j] = @2) & (Aj ((j>=i)&(j C[j] = @1) & (Aj ((j>=i)&(j= s+n) ) => C[j] = C[(j+p)-n]) & (Aj ~((j>=i)&(j=i)&(j=i)&(j= s+n) ) => @0 = C[(j+p)-n]) & (Aj ~((j>=i)&(j=i)&(j= s+n) & (j+p < s+2*n-3)) => @2 = C[(j+p)-n]) & (Aj ((j>=i)&(j @1 = C[(j+p)-n]) & (Aj ~((j>=i)&(j=i)&(j= s+n) & (j+p < s+2*n-3)) => C[j-n] = C[(j+p)-n]) & (Aj ((j>=i)&(j= s+n) & (j+p = s+2*n-3)) => C[j-n] = @0) & (Aj ((i<=j)&(j= s+n) & (j < s+2*n-3) & (j+p = s+2*n-2)) => C[j-n] = @2)": def sqfree021 "(n > 3) & (Ai,p ((1 <= p) & (2*p <= n) & (s <= i) & (i < s+n)) => ~(\$sq021(i,n,p,s)))": def test021 "Es \$sqfree021(n,s)": def sq2120 "(n > 4) & (1 <= p) & (2*p <= n) & (s <= i) & (i < s+n) & (Aj ((i<=j)&(j C[j] = C[j+p]) & (Aj ((i<=j)&(j C[j] = @2) & (Aj ((i<=j)&(j C[j] = @1) & (Aj ((j>=i)&(j C[j] = @2) & (Aj ((j>=i)&(j C[j] = @0) & (Aj ((j>=i)&(j= s+n) ) => C[j] = C[(j+p)-n]) & (Aj ~((j>=i)&(j=i)&(j=i)&(j= s+n) ) => @2 = C[(j+p)-n]) & (Aj ~((j>=i)&(j=i)&(j=i)&(j= s+n) & (j+p < s+2*n-4)) => @1 = C[(j+p)-n]) & (Aj ~((j>=i)&(j=i)&(j=i)&(j= s+n) & (j+p < s+2*n-4)) => @2 = C[(j+p)-n]) & (Aj ~((j>=i)&(j=i)&(j= s+n) & (j+p < s+2*n-4)) => @0 = C[(j+p)-n]) & (Aj ~((j>=i)&(j=i)&(j=i)&(j=i)&(j= s+n) & (j+p < s+2*n-4)) => C[j-n] = C[(j+p)-n]) & (Aj ((j>=i)&(j= s+n) & (j+p = s+2*n-4)) => C[j-n] = @2) & (Aj ((j>=i)&(j= s+n) & (j+p = s+2*n-3)) => C[j-n] = @1) & (Aj ((j>=i)&(j= s+n) & (j+p = s+2*n-2)) => C[j-n] = @2)": def sqfree2120 "(n > 4) & (Ai,p ((1 <= p) & (2*p <= n) & (s <= i) & (i < s+n)) => ~(\$sq2120(i,n,p,s)))": def test2120 "Es \$sqfree2120(n,s)": def currie "\$test021(n) | \$test2120(n)":