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