def isBorderC1 "((k+l > n) =>((Ai (i<n-l) => T[m+l+i] = T[m+l-k+i]) & (Ai (i<k+l-n) => T[m+i] = T[m+n-k+i])))":

def isBorderC2 "(((k+l <= n) & (l >= k)) => (Ai (i< k) => T[m+l+i] = T[m+l-k+i]))":

def isBorderC3 "(((k+l <= n) & (l < k )) =>( (Ai (i< k-l) => T[m+n-k+l+i] = T[m+l+i]) & (Ai (i< l) => T[m+i] = T[m+k+i])))":

def isBorder "$isBorderC1(k,l,m,n) & $isBorderC2(k,l,m,n) & $isBorderC3(k,l,m,n)":

def isBordered "Ei (2*i <= n & i >= 1 & $isBorder(i,l,m,n))": 

def isAlternatingE "(Ai (((i != l & i!= e & i<n-1) => ($isBordered(i,m,n) <=> ~$isBordered(i+1,m,n)))) & (((i != l) & (i!= e) & (i=n-1)) => ($isBordered(n-1,m,n) <=>  ~$isBordered(0,m,n))))":

def isAlternatingO "(Ai (((i != l & i<n-1) => ($isBordered(i,m,n) <=> ~$isBordered(i+1,m,n)))) & (((i != l) & (i=n-1)) => ($isBordered(n-1,m,n) <=>  ~$isBordered(0,m,n))))":

def hasMNUCE "(Ei,j ((i < j) & (i<n-1 & $isBordered(i,m,n) & $isBordered(i+1,m,n)) & ((j=n-1 & $isBordered(n-1,m,n) & $isBordered(0,m,n)) | ((j<n-1) & $isBordered(j,m,n) & $isBordered(j+1,m,n))) & $isAlternating(i,j,m,n))) | $isAlternatingE(n,n,m,n)":

def hasMNUCO "Ei (((i<n-1 & $isBordered(i,m,n) & $isBordered(i+1,m,n)) | (i=n-1 & $isBordered(n-1,m,n) & $isBordered(0,m,n))) & $isAlternatingO(i,m,n))":

eval verifyEven "An((n>=2) => (Ei $hasMNUCE(i,2*n)))":

eval verifyOdd "An ((n>=2) => (Ei (i <= 2*n+1)  & $hasMNUCO(i,2*n+1)))":