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