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

def subs "?msd_fib (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 "?msd_fib Ak (k<n) => F[i+k]=F[j+k]":

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

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

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

def rich "?msd_fib 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 "?msd_fib Ei $rich(i,n)":

eval allrich "?msd_fib Ai An $rich(i,n)":

def priv "?msd_fib (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)))":

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

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

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

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

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

eval maxpallengthfib "?msd_fib Ei $maxpal(i,n)":

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

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

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

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

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

def trap "?msd_fib (Ep Eq (n=p+q) & $minunrepsuf(j,n,p)
& $minrt(j,n,q))":

eval trapn "?msd_fib Ai An  $trap(j,n)":

def unbal "?msd_fib 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) & (F[j-1]=F[j+m]) & (F[k-1]=F[k+m]) &
(F[j-1] != F[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) & F[j]!=F[k]))":

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

eval ball "?msd_fib Ej En ~$unbal(j,n)":