def sq021 "(n > 3)  &  (1 <= p) & (2*p <= n)  &  (s <= i) & (i < s+n)  &
    (Aj ((i<=j)&(j<i+p) &                (j+p  < s+n-3)                ) =>  C[j]  = C[j+p])     &
    (Aj ((i<=j)&(j<i+p) &                (j+p  = s+n-3)                ) =>  C[j]  =  @0)         &
    (Aj ((j>=i)&(j<i+p) & (j  < s+n-3) & (j+p  = s+n-2)                ) =>  C[j]  =  @2)         &
    (Aj ((j>=i)&(j<i+p) & (j  < s+n-3) & (j+p  = s+n-1)                ) =>  C[j]  =  @1)         &
    (Aj ((j>=i)&(j<i+p) & (j  < s+n-3) & (j+p >= s+n)                  ) =>  C[j]  = C[(j+p)-n]) &
    (Aj ~((j>=i)&(j<i+p)& (j  = s+n-3) & (j+p  = s+n-2)               ))                           &
    (Aj ~((j>=i)&(j<i+p)& (j  = s+n-3) & (j+p  = s+n-1)               ))                           &
    (Aj ((j>=i)&(j<i+p) & (j  = s+n-3) & (j+p >= s+n)                  ) =>   @0    = C[(j+p)-n]) &
    (Aj ~((j>=i)&(j<i+p)& (j  = s+n-2) & (j+p  = s+n-1)               ))                           &
    (Aj ((j>=i)&(j<i+p) & (j  = s+n-2) & (j+p >= s+n) & (j+p < s+2*n-3)) =>   @2    = C[(j+p)-n]) &
    (Aj ((j>=i)&(j<i+p) & (j  = s+n-1) &                (j+p < s+2*n-3)) =>   @1    = C[(j+p)-n]) &
    (Aj ~((j>=i)&(j<i+p)& (j  = s+n-1) &                (j+p = s+2*n-3)))                          &
    (Aj ((j>=i)&(j<i+p) & (j >= s+n)  &                 (j+p < s+2*n-3)) => C[j-n] = C[(j+p)-n]) &
    (Aj ((j>=i)&(j<i+p) & (j >= s+n)  &                 (j+p = s+2*n-3)) => C[j-n] =  @0)         &
    (Aj ((i<=j)&(j<i+p) & (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<i+p) &                (j+p  < s+n-4)                ) =>  C[j]  = C[j+p])     &
    (Aj ((i<=j)&(j<i+p) &                (j+p  = s+n-4)                ) =>  C[j]  =  @2)         &
    (Aj ((i<=j)&(j<i+p) & (j  < s+n-4) & (j+p  = s+n-3)                ) =>  C[j]  =  @1)         &
    (Aj ((j>=i)&(j<i+p) & (j  < s+n-4) & (j+p  = s+n-2)                ) =>  C[j]  =  @2)         &
    (Aj ((j>=i)&(j<i+p) & (j  < s+n-4) & (j+p  = s+n-1)                ) =>  C[j]  =  @0)         &
    (Aj ((j>=i)&(j<i+p) & (j  < s+n-4) & (j+p >= s+n)                  ) =>  C[j]  = C[(j+p)-n]) &
    (Aj ~((j>=i)&(j<i+p)& (j  = s+n-4) & (j+p  = s+n-3)               ))                           &
    (Aj ~((j>=i)&(j<i+p)& (j  = s+n-4) & (j+p  = s+n-1)               ))                           &
    (Aj ((j>=i)&(j<i+p) & (j  = s+n-4) & (j+p >= s+n)                  ) =>   @2    = C[(j+p)-n]) &
    (Aj ~((j>=i)&(j<i+p)& (j  = s+n-3) & (j+p  = s+n-2)               ))                           &
    (Aj ~((j>=i)&(j<i+p)& (j  = s+n-3) & (j+p  = s+n-1)               ))                           &
    (Aj ((j>=i)&(j<i+p) & (j  = s+n-3) & (j+p >= s+n) & (j+p < s+2*n-4)) =>   @1    = C[(j+p)-n]) &
    (Aj ~((j>=i)&(j<i+p)& (j  = s+n-3) &                (j+p = s+2*n-4)))                          &
    (Aj ~((j>=i)&(j<i+p)& (j  = s+n-2) & (j+p  = s+n-1)               ))                           &
    (Aj ((j>=i)&(j<i+p) & (j  = s+n-2) & (j+p >= s+n) & (j+p < s+2*n-4)) =>   @2    = C[(j+p)-n]) &
    (Aj ~((j>=i)&(j<i+p)& (j  = s+n-2) &                (j+p = s+2*n-3)))                          &
    (Aj ((j>=i)&(j<i+p) & (j  = s+n-1) & (j+p >= s+n) & (j+p < s+2*n-4)) =>   @0    = C[(j+p)-n]) &
    (Aj ~((j>=i)&(j<i+p)& (j  = s+n-1) &                (j+p = s+2*n-4)))                          &
    (Aj ~((j>=i)&(j<i+p)& (j  = s+n-1) &                (j+p = s+2*n-3)))                          &
    (Aj ~((j>=i)&(j<i+p)& (j  = s+n-1) &                (j+p = s+2*n-2)))                          &
    (Aj ((j>=i)&(j<i+p) & (j >= s+n)   &                (j+p < s+2*n-4)) => C[j-n] = C[(j+p)-n]) &
    (Aj ((j>=i)&(j<i+p) & (j >= s+n)   &                (j+p = s+2*n-4)) => C[j-n] =  @2)         &
    (Aj ((j>=i)&(j<i+p) & (j >= s+n)   &                (j+p = s+2*n-3)) => C[j-n] =  @1)         &
    (Aj ((j>=i)&(j<i+p) & (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)":