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

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

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

def rt2 "Er Es ($subs(r,j,p+1,n) & $subs(s,j,p+1,n) & $factoreq(r,s,p) & RS[s+p] != RS[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 trap2 "(n<=1) | (Ep Eq (n=p+q) & $minunrepsuf(j,n,p) & $minrt2(j,n,q))":

eval trap2n "Ej $trap2(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) & (RS[j-1]=RS[j+m]) & (RS[k-1]=RS[k+m]) &
(RS[j-1] != RS[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) & RS[j]!=RS[k]))”:

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