def subs "?lsd_2 (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 "?lsd_2 Ak (k RS[i+k]=RS[j+k]": def pal "?lsd_2 Ak (k RS[i+k] = RS[i+n-1-k]": def occurs "?lsd_2 (m<=n) & (Ek (k+m<=n) & $factoreq(i,j+k,m))": def rt2 "?lsd_2 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 "?lsd_2 ~$rt2(j,n,p) & (Ac (~$rt2(j,n,c)) => c >=p)": def unrepsuf "?lsd_2 ~$occurs(j+n-q,j,q,n-1)": def minunrepsuf "?lsd_2 $unrepsuf(j,n,q) & (Ac $unrepsuf(j,n,c) => (c >= q))": def trap2 "?lsd_2 (n<=1) | (Ep Eq (n=p+q) & $minunrepsuf(j,n,p) & $minrt2(j,n,q))": eval trap2n "?lsd_2 Ej $trap2(j,n)":