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

def pal "Ak (k<n) => T[i+k] = T[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 priv "(n<=1) | (Am $in(m,1,n) => (Ep $in(p,1,m) &
$border(i,p,n) & ~$occurs(i,i+1,p,m-1) & ~$occurs(i,i+n-m,p,m-1)))":

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

def firstpriv "$priv(i,n) & (Aj (j<i) => ~$factoreq(i,j,n))":

def privpal "$priv(i,n) & $pal(i,n)":

def firstprivpal "$privpal(i,n) & (Aj (j<i) => ~$factoreq(i,j,n))":

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)) => (T[j-1] != T[j+n]))":

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

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

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

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 minrt  "~$rt(j,n,p) & (Ac (~$rt(j,n,c)) => c >=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))":

def trap2 "(n<=1) | (Ep Eq (n=p+q) & $minunrepsuf(j,n,p) & $minrt2(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) & (T[j-1]=T[j+m]) & (T[k-1]=T[k+m]) &
(T[j-1] != T[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)":