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) => PD[i+k]=PD[j+k]":

def pal "Ak (k<n) => PD[i+k] = PD[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)":

eval allrich "Ai An $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)) => (PD[j-1] != PD[j+n]))":

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

def rtspec "$subs(i,j,m,n-1) & (Er $subs(r,j,m,n-1) & $factoreq(i,r,m) &
	PD[r+m]=@0) & (Es $subs(s,j,m,n-1) & $factoreq(i,s,m) & PD[s+m] = @1)":

def rt "Ei $rtspec(i,j,p,n)":

def minrt  "~$rt(j,n,p) & (Ac (~$rt(j,n,c)) => (c >=p)) ":

def rt2 "Er Es ($subs(r,j,p+1,n) & $subs(s,j,p+1,n) & $factoreq(r,s,p) & T[s+p] != T[r+p])":

def minrt2  "~$rt2(j,n,p) & (Ac (~$rt2(j,n,c)) => (c >=p)) ":

def unrepsuf "~$occurs(j+n-q,j,q,n-1)":

def minunrepsuf "$unrepsuf(j,n,q) & (Ac $unrepsuf(j,n,c) => (c >= q))":

def trap "(n <=1) | (Ep Eq (n=p+q) & $minunrepsuf(j,n,p) & $minrt(j,n,q))":

eval trapn "Ej $trap(j,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) & (PD[j-1]=PD[j+m]) & (PD[k-1]=PD[k+m]) &
(PD[j-1] != PD[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)":