def in "(i>=r) & (i<=s)":
# in(i,r,s) := is i in [r,s]?

def subs "(j<=i) & (i+m<=j+n)":
# subs(i,j,m,n) := is [i..i+m-1] a subset of [j..j+n-1] ?

def factoreq "Ak (k<n) => P[i+k]=P[j+k]":

def pal "Ak (k<n) => P[i+k] = P[i+n-1-k]":

def occurs "(m<=n) & (Ek (k+m<=n) & $factoreq(i,j+k,m))":

def border "$in(m,1,n) & $factoreq(i,i+n-m,m)":

def rich "Am $in(m,1,n) => (Ej $subs(j,i,1,m) & $pal(j,i+m-j) &
	~$occurs(j,i,i+m-j,m-1))":

eval richn "Ei $rich(i,n)":

def uniqpref "Aj $in(j,1,n-m-1) => ~$factoreq(i,i+j,m)":

def uniqsuff "Aj $in(j,1,n-m-1) => ~$factoreq(i+n-m,i+n-m-j,m)":

def priv "(n<=1) | (Am $in(m,1,n) => (Ep $in(p,1,m) & ($border(i,p,n) & 
$uniqpref(i,p,m) & $uniqsuff(i+n-m,p,m))))":

eval privn "Ei $priv(i,n)":

def closed "(n<=1) | (Ej (j<n)& $border(i,j,n) & ~$occurs(i,i+1,j,n-2))":

def ucf "$closed(i,n) & ~$occurs(i,0,n,i+n-1)":

def closedn "Ei $closed(i,n)":

def maxpal "$pal(i,n) & (Aj ((j>=1)&$factoreq(i,j,n)) => (P[j-1] != P[j+n]))":

eval maxpallengthpaperf "Ei $maxpal(i,n)":

def unbal "Em (m+2 <= n) & Ej Ek ($subs(j,i+1,m,n-2) & $subs(k,i+1,m,n-2) &
$pal(j,m) & $factoreq(j,k,m) & (P[j-1]=P[j+m]) & (P[k-1]=P[k+m]) &
(P[j-1] != P[k-1]))":

def unbal2 "Em (m >= 2) & (Ej Ek ($subs(j,i,m,n) & $subs(k,i,m,n) & $pal(j,m) & $pal(k,m) & $factoreq(j+1,k+1,m-2) & T[j]!=T[k]))":

eval baln "Ej ~$unbal(j,n)":