eval vtm212 "Ei (VTM[i]=@2 & VTM[i+1]=@1 & VTM[i+2]=@2)": eval vtm010 "Ei (VTM[i]=@0 & VTM[i+1]=@1 & VTM[i+2]=@0)": eval tm01 "T[i]=@0 & T[i+1]=@1": eval thueinf "An Ei (i>n) & T[i]=T[n]": def fibdist1 "?msd_fib Ei F[i]=@1 & F[i+d]=@1": eval chor "An (n>=3) => ((Ei VTM[i]=@0 & VTM[i+n]=@0) & (Ej VTM[j]=@2 & VTM[j+n]=@2))": eval test3cantor "?msd_3 Ei,j (j>=1) & CA[i]=@1 & CA[i+j]=@1 & CA[i+2*j]=@1": def run3f "?msd_fib Ei (F[i]=F[i+n] & F[i]=F[i+2*n])": def run2f "?msd_fib Ei F[i]=F[i+n]": def a339950 "?msd_fib \$run2f(n) & ~\$run3f(n)": def simon1 "A i1,i2,i3 (i<=i1 & i1 E j1,j2,j3 j<=j1 & j1 T[t]=T[t+n]) & T[j]=@0 & T[j+n]=@1 & (Au (j (T[u]=@1 & T[u+n]=@0))": def test101 "T[j]=@1 & T[k]=@1 & k>=j+2 & At (t>j & t T[t]=@0": def weirdfac "T[m]=@1 & T[m+1]=@0 & T[m+2]=@1 & Er \$test101(r,n) & A j,k (j>=m & k<=r & j<=k & \$test101(j,k)) => \$test101(k,(2*k+1)-j)": def weirdfaclen "Em,n \$weirdfac(m,n) & s+m=n+1": def carun0 "?msd_3 n>=1 & (At t CA[i+t]=@0) & CA[i+n]!=@0 & (i=0|CA[i-1]!=@0)": def carun1 "?msd_3 n>=1 & (At t CA[i+t]=@1) & CA[i+n]!=@1 & (i=0|CA[i-1]!=@1)": eval cantor0 "?msd_3 Am Ei,n (n>m) & \$carun0(i,n)": eval cantor1 "?msd_3 Am Ei,n (n>m) & \$carun1(i,n)": def rsrun0 "n>=1 & (At t RS[i+t]=@0) & RS[i+n]!=@0 & (i=0|RS[i-1]!=@0)": def rsmaxrun0 "(Ei \$rsrun0(i,n)) & (Aj,m m>n => ~\$rsrun0(j,m))": eval sbrl "Ei n>=1 & (At t SB[i+t]=SB[i]) & (SB[i+n]!=SB[i]) & (i=0 | SB[i-1]!=SB[i])": reg validpell msd_pell "0*|0*(1|20)(0|1|20)*": reg has0 msd_pell "(0|1|2)*(1|2)0(0|1|2)*": reg has1 msd_pell "(0|1|2)*1(0|1|2)*": reg has2 msd_pell "(0|1|2)*2(0|1|2)*": def has012 "?msd_pell \$validpell(n)&\$has0(n)&\$has1(n)&\$has2(n)": combine PAD has012: eval padrunlengths "?msd_pell Ei n>=1 & (At t PAD[i+t]=PAD[i]) & (PAD[i+n]!=PAD[i]) & (i=0 | PAD[i-1]!=PAD[i])": def fib00 "?msd_fib Ei F[i]=@0 & F[i+n]=@0": def fib01 "?msd_fib Ei F[i]=@0 & F[i+n]=@1": def fib10 "?msd_fib Ei F[i]=@1 & F[i+n]=@0": def fib11 "?msd_fib Ei F[i]=@1 & F[i+n]=@1": def tmfactoreq "At t T[i+t]=T[j+t]": def tmnovelf "Aj j ~\$tmfactoreq(i,j,n)": morphism g "0->01 1->23 2->45 3->46 4->54 5->66 6->66": morphism h "0->2 1->2 2->2 3->0 4->1 5->0 6->1": promote GG g: image WSA h GG: reg power2 msd_2 "0*10*": eval wcheck "Ai WSA[i]=@0<=>(Ex \$power2(x)&(i+2=5*x|i+2=7*x))": def wfactoreq "At (t WSA[i+t]=WSA[j+t]": def woccurs "m<=n & Es (s+m<=n & \$wfactoreq(i,j+s,m))": eval wsatest "Ai,j (i>=1 & i ~\$woccurs(i,j,i+1,j+1)": reg odd1 msd_2 "0*10*(10*10*)*": eval tmchk "An \$odd1(n) <=> T[n]=@1": reg pfc msd_2 "0*10*|0*1(0|1)*010*": eval pfchk "An n>=1 => (\$pfc(n) <=> ZP[n]=@0)": eval tmup "Ep,n (p>=1) & (Ai (i>=n) => T[i]=T[i+p])": def hasper "p>=1 & Aj j>=i => X[j] = X[j+p]": def ultper "\$hasper(i,p) & (Aq,k (q ~\$hasper(k,q)) & (Aq,k k ~\$hasper(k,q))": morphism g "0->01 1->23 2->45 3->67 4->89 5->34 6->56 7->78 8->93 9->45": promote UP g: def hasper "(p>=1) & Aj (j>=i) => UP[j] = UP[j+p]": def ultper "\$hasper(i,p) & (Aq,k q

~\$hasper(k,q)) & (Aq,k k ~\$hasper(k,q))": def fibquasi "?msd_fib Ai (Ej i (Es \$isfib(s) & n=s-1)": eval ck2 "Ep,q 0

=1 & Aj j X[i+j]=X[i+j+n]": eval vtmsquare "Ei,n n>=1 & Aj j VTM[i+j]=VTM[i+j+n]": eval hanoisq "Ei,n n>=1 & Aj j TH[i+j]=TH[i+j+n]": def fibsquarelen "?msd_fib n>0 & Ei At t F[i+t]=F[i+n+t]": reg isfib msd_fib "0*10*": eval seebold "?msd_fib An \$isfib(n) <=> \$fibsquarelen(n)": def fibsquarepos "?msd_fib n>0 & At t F[i+t] = F[i+n+t]": eval fibals "?msd_fib Ai,m En n>m & At t F[i+t]=F[i+n+t]": def tribsquarelen "?msd_trib n>0&Ei At tTR[i+t]=TR[i+n+t]": def tribsquarelen "?msd_trib n>0 & Ei Aj (j>=i & j TR[j]=TR[j+n]": eval tribals "?msd_trib Ai,m En (n>=m) & Au,v (u>=i & u TR[u]=TR[v]": eval dean1 "Ei,n n>=1 & At t DE[i+t]=DE[i+n+t]": eval dean02 "Ei DE[i]=@0 & DE[i+1]=@2": eval dean20 "Ei DE[i]=@2 & DE[i+1]=@0": eval dean13 "Ei DE[i]=@1 & DE[i+1]=@3": eval dean31 "Ei DE[i]=@3 & DE[i+1]=@1": eval pansiot "VTM[n]!=VTM[n+2]": eval ttmolf "Ei, p (p>=1) & Aj (j<=p) => TTM[i+j]=TTM[i+j+p]": eval fibcube "?msd_fib n>0 & Ei \$ffactoreq(i,i+n,2*n)": eval sccube "?msd_3 Ei,n n>0& At (t<2*n)=>SC[i+t]=SC[i+n+t]": eval stewap "?msd_3 Ei,j,k,l,m k+i=2*j & j+l=2*k & m+k=2*l & SC[i]=SC[k] & SC[j]=SC[l] & SC[k]=SC[m] & SC[i]!=SC[j]": eval karhu "?msd_fib Ei,n n>0 & At (t>=i & t F[t]=F[t+n]": eval trib4p "?msd_trib Ei,n n>0 & At (t>=i & t TR[t]=TR[t+n]": morphism h "0->01 1->20 2->34 3->34 4->53 5->01": morphism tau "0->0 1->1 2->2 3->3 4->4 5->2": promote HH h: image SA tau HH: def satest "(At SA[t] != SA[t+1]) & Ai,n n>=2 => (Ej,k j=1 & Aj (j>=i & 8*j<=8*i+7*n) => LE[j]=LE[j+n]": eval leechp "?msd_13 n>=1 & Aj (j>=i & 8*j<8*i+7*n) => LE[j]=LE[j+n]": eval dej74e "?msd_19 Ei,n n>=1 & Aj (j>=i & 4*j<=4*i+3*n) => DEJ[j]=DEJ[j+n]": eval dej74 "?msd_19 Ei n>=1 & Aj (j>=i & 4*j<4*i+3*n) => DEJ[j]=DEJ[j+n]": def tmc "(i=n & T[n]=@0) | (i!=n & T[n]=@1)": combine TMC tmc: def tmc52 "(Ej,n n>=1 & At (2*t<3*n) => TMC[i][j+t]=TMC[i][j+t+n]) & (~Ej,n n>=1 & At (2*t<=3*n) => TMC[i][j+t]=TMC[i][j+t+n])": def tmc83 "(Ej,n n>=1 & At (3*t<5*n) => TMC[i][j+t]=TMC[i][j+t+n]) & (~Ej,n n>=1 & At (3*t<=5*n) => TMC[i][j+t]=TMC[i][j+t+n])": def tmc31 "(Ej,n n>=1 & At (t<2*n) => TMC[i][j+t]=TMC[i][j+t+n]) & (~Ej,n n>=1 & At (t<=2*n) => TMC[i][j+t]=TMC[i][j+t+n])": def tmc103 "(Ej,n n>=1 & At (3*t<7*n) => TMC[i][j+t]=TMC[i][j+t+n]) & (~Ej,n n>=1 & At (3*t<=7*n) => TMC[i][j+t]=TMC[i][j+t+n])": def tmc113 "(Ej,n n>=1 & At (3*t<8*n) => TMC[i][j+t]=TMC[i][j+t+n]) & (~Ej,n n>=1 & At (3*t<=8*n) => TMC[i][j+t]=TMC[i][j+t+n])": def tmc41 "(Ej,n n>=1 & At (t<3*n) => TMC[i][j+t]=TMC[i][j+t+n]) & (~Ej,n n>=1 & At (t<=3*n) => TMC[i][j+t]=TMC[i][j+t+n])": eval test "(Ei \$tmc52(i)) & (Ei \$tmc83(i)) & (Ei \$tmc31(i)) & (Ei \$tmc103(i)) & (Ei \$tmc113(i)) & (Ei \$tmc41(i)) & Ai (\$tmc52(i)|\$tmc83(i)|\$tmc31(i)|\$tmc103(i)|\$tmc113(i)| \$tmc41(i))": morphism ext "0->0111 1->1221 2->2112": promote XT ext: morphism codi "0->2 1->1 2->0": image X codi XT: def isover "?msd_4 Ep (p>=1) & 2*p+r+1=s & (Ai (r<=i & i+p X[i]=X[i+p])": def isover0 "?msd_4 Ep (p>=1) & (s=r+2*p) & (Ai (r<=i & i+p X[i]=X[i+p]) & (j>=r+p => X[j-p]=@0) & (Ai (r<=i & i=j+1 & i+p<=s) => X[i]=X[(i+p)-1]) & (j+p<=s => X[(j+p)-1]=@0) & (Ai (j<=i & i+p X[i]=X[i+p])": def isover1 "?msd_4 Ep (p>=1) & (s=r+2*p) & (Ai (r<=i & i+p X[i]=X[i+p]) & (j>=r+p => X[j-p]=@1) & (Ai (r<=i & i=j+1 & i+p<=s) => X[i]=X[(i+p)-1]) & (j+p<=s => X[(j+p)-1]=@1) & (Ai (j<=i & i+p X[i]=X[i+p])": def hasover "?msd_4 Er,s i<=r & r<=s & s<=i+n & \$isover(r,s)": def extremal "?msd_4 (~\$hasover(i,n)) & Aj (j>=i & j<=i+n) => ((Er,s r>=i & r=i & rp\$extremal(18*i,32*i)": def tmfactoreq "At t T[i+t]=T[j+t]": def tmprim "~(Ej j>0 & j0 & \$tmprim(0,n)": eval tmprimcheck "An n>=1 => \$tmprimlength(n)": def sbfactoreq "At t SB[i+t]=SB[j+t]": def sbprim "~(Ej j>0 & j ~\$sbfactoreq(i,j,n)": def sbarbexp "Am m>n => Ej \$sbfactoreq(i,j,n) & \$sbfactoreq(j,j+n,m)": def sbfirstarbexp "n>=1 & \$sbnovelf(i,n) & \$sbprim(i,n) & \$sbarbexp(i,n)": def isantif "?msd_fib Aj j F[i+j]!=F[i+j+n]": def antisf "?msd_fib Ei \$isantif(i,n)": def pdfactoreq "At t PD[i+t]=PD[j+t]": def pdrevcheck "At t PD[i+t]=PD[(j+n)-(t+1)]": eval checkpd4 "Ei,n n>=1 & (\$pdfactoreq(i,i+n,n) | \$pdrevcheck(i,i+n,n)) & (\$pdfactoreq(i,i+2*n,n) | \$pdrevcheck(i,i+2*n,n)) & (\$pdfactoreq(i,i+3*n,n) | \$pdrevcheck(i,i+3*n,n))": def rffactoreq "?msd_fib At t RF[i+t]=RF[j+t]": def rfrevcheck "?msd_fib As,t (s>=i & t>=j & s+t+1=i+j+n) => RF[s]=RF[t]": eval rfprop "?msd_fib Ei,n n>=1 & \$rffactoreq(i,i+n,n) & \$rfrevcheck(i,i+2*n,n)": def factoreq "?msd_3 At (t SC[i+t]=SC[j+t]": eval xxyyxx "?msd_3 Ei,m,n (m>=1) & \$factoreq(i,i+m,m) & \$factoreq(i+2*m,i+2*m+n,n) & \$factoreq(i,i+2*m+2*n,2*n)": morphism h1 "0->0110010 1->1001101": promote H1 h1: def factoreq "?msd_7 At (t H1[i+t]=H1[j+t]": eval testh1 "?msd_7 Ei,m,n (m>=1) & \$factoreq(i,i+m,m) & \$factoreq(i,i+2*m+n,m) & \$factoreq(i+2*m,i+3*m+n,n) & \$factoreq(i+3*m+n,i+3*m+2*n,n)": eval cubetesth1 "?msd_7 Ei,n (n>=1) & \$factoreq(i,i+n,2*n)": morphism h2 "0->01001 1->10110": promote H2 h2: def factoreq "?msd_5 At (t H2[i+t]=H2[j+t]": eval testh2 "?msd_5 Ei,m,n (m>=1) & \$factoreq(i,i+m,m) & \$factoreq(i,i+2*m+2*n,m) & \$factoreq(i,i+3*m+3*n,m) & \$factoreq(i+2*m,i+2*m+n,n) & \$factoreq(i+2*m,i+3*m+3*n,n)": eval cubetesth2 "?msd_5 Ei,n (n>=1) & \$factoreq(i,i+n,2*n)": morphism h3 "0->010011 1->011001": promote H3 h3: def factoreq "?msd_6 At (t H3[i+t]=H3[j+t]": eval testh3 "?msd_6 Ei,m,n (m>=1) & \$factoreq(i,i+m+n,m) & \$factoreq(i,i+2*m+n,m) & \$factoreq(i,i+3*m+2*n,m) & \$factoreq(i+m,i+3*m+n,n) & \$factoreq(i+m,i+4*m+2*n,n)": eval cubetesth3 "?msd_6 Ei,n (n>=1) & \$factoreq(i,i+n,2*n)": def tmperi "p>0 & p<=n & Aj (j>=i & j+p T[j]=T[j+p]": def tmlper "\$tmperi(i,n,p)&(Aq (q>=1&q~\$tmperi(i,n,q))": eval tmleastpcheck "Ap p>=1 => Ei,n n>=1 & \$tmlper(i,n,p)": def fibperi "?msd_fib p>0 & p<=n & Aj (j>=i & j+p F[j]=F[j+p]": def fiblper "?msd_fib \$fibperi(i,n,p) & (Aq (q>=1 & q ~\$fibperi(i,n,q))": def fibleastp "?msd_fib Ei,n n>=1 & \$fiblper(i,n,p)": def tribperi "?msd_trib p>0 & p<=n & Aj (j>=i & j+p TR[j]=TR[j+p]": def triblper "?msd_trib \$tribperi(i,n,p) & (Aq (q>=1 & q ~\$tribperi(i,n,q))": def tribleastp "?msd_trib Ei,n n>=1 & \$triblper(i,n,p)": def fibperi "?msd_fib p>0 & p<=n & Aj j+p F[i+j]=F[i+j+p]": def fiblper "?msd_fib \$fibperi(i,n,p) & Aq q

~\$fibperi(i,n,q)": def fiblongest "?msd_fib (Ei \$fiblper(i,n,p)) & (Ar,i \$fiblper(i,r,p) => r<=n)": def pptm "p>0 & p<=n & Aj j+p T[j]=T[j+p]": def lpertm "\$pptm(n,p) & Aq q

~\$pptm(n,q)": def longestm "\$lpertm(n,p) & (Ar \$lpertm(r,p) => r<=n)": def crep "(Aj (j>=i & j+p T[j]=T[j+p]) & (Aj (j>=i & j=s+n & j+p T[j]=T[(j+p)-n]) & (Aj (j>=i & j>=s+n & j+p T[j-n]=T[(j+p)-n])": eval aberkane "An n>=1 => Es Am,p,i (p>=1 & m>=1 & m<=n & i>=s & i 2*m <= 5*p": def vfactoreq "At t VTM[i+t]=VTM[j+t]": def dispos "~Ei,n n>=1 & ((i<=k & k<=i+n & \$vfactoreq(i,i+n+1,k-i) & \$vfactoreq(k+1,n+k+1,(n+i)-k)) | (i+n<=k & k<=i+2*n & \$vfactoreq(i,i+n,k-(i+n)) & \$vfactoreq(k-n,k+1,(i+2*n)-k)))": def delsp "(i+t T[i+t]=@1) & (i+t>=j => T[i+t+1]=@1)": def deloverlap "Ac c<=s => (\$delsp(i,j,r+c) <=> \$delsp(i,j,r+c+s))": def delover "Er,s (s>=1) & (r+2*s+2<=n) & \$deloverlap(i,j,r,s)": def irredover "Aj (i \$delover(i,j,n)": def irredoverlength "(n>=3) & Ei \$irredover(i,n)": eval checkover "An \$irredoverlength(n) <=> n=6 | n=8 | n=9 | n=10 | n>=12": def cfaceq "?msd_3 At t CA[i+t]=CA[j+t]": eval cno10 "?msd_3 Ai,n n>=1 => ( \$cfaceq(i+0*n,i+1*n,n) | \$cfaceq(i+0*n,i+5*n,n) | \$cfaceq(i+2*n,i+3*n,n) | \$cfaceq(i+2*n,i+8*n,n) | \$cfaceq(i+3*n,i+4*n,n) | \$cfaceq(i+3*n,i+7*n,n) | \$cfaceq(i+3*n,i+9*n,n) | \$cfaceq(i+4*n,i+5*n,n) | \$cfaceq(i+4*n,i+9*n,n) | \$cfaceq(i+5*n,i+6*n,n) | \$cfaceq(i+5*n,i+8*n,n) | \$cfaceq(i+6*n,i+7*n,n) | \$cfaceq(i+7*n,i+8*n,n) | \$cfaceq(i+8*n,i+9*n,n))": morphism g "0->01 1->23 2->45 3->63 4->41 5->27 6->05 7->67": promote GG g: morphism tau "0->0 1->1 2->2 3->0 4->3 5->2 6->1 7->3": image TI tau GG: def tifaceq "At t TI[i+t]=TI[j+t]": eval titest "An,i,j (n>=1 & i j>=i+n+2": def tmconj "Et t<=n & \$tmfactoreq(j,i+t,n-t) & \$tmfactoreq(i,(j+n)-t,t)": def tmcu "Aj \$tmconj(i,j,n) => \$tmfactoreq(i,j,n)": def tmculen "Ei \$tmcu(i,n)": morphism gam "0->01 1->21 2->03 3->23": promote B4 gam: morphism g2 "0->0000101001110110100 1->0011100010100111101 2->0000111100010110100 3->0011110110100111101": morphism g3 "0->0010 1->1122 2->0200 3->1212": morphism g6 "0->01230 1->24134 2->52340 3->24513": image G2B4 g2 B4: image G3B4 g3 B4: image G6B4 g6 B4: def gamard6factoreq "Au,v (i+v=j+u & u>=i & u G6B4[u]=G6B4[v]": def gamard6shift "\$gamard6factoreq(j,i+t,n-t) & \$gamard6factoreq(i,(j+n)-t,t)": def gamard6conj "Et t<=n & \$gamard6shift(i,j,n,t)": def gamard6allconj "At t<=n => Ej \$gamard6shift(i,j,n,t)": eval gamard6check "An n>=2 => ~(Ei \$gamard6allconj(i,n))": def gamard3factoreq "Au,v (i+v=j+u & u>=i & u G3B4[u]=G3B4[v]": def gamard3shift "\$gamard3factoreq(j,i+t,n-t) & \$gamard3factoreq(i,(j+n)-t,t)": def gamard3conj "Et t<=n & \$gamard3shift(i,j,n,t)": def gamard3allconj "At t<=n => Ej \$gamard3shift(i,j,n,t)": eval gamard3check "An n>=3 => ~(Ei \$gamard3allconj(i,n))": def gamard2factoreq "Au,v (i+v=j+u & u>=i & u G2B4[u]=G2B4[v]": def gamard2shift "\$gamard2factoreq(j,i+t,n-t) & \$gamard2factoreq(i,(j+n)-t,t)": def gamard2conj "Et t<=n & \$gamard2shift(i,j,n,t)": def gamard2allconj "At t<=n => Ej \$gamard2shift(i,j,n,t)": eval gamard2check "An n>=5 => ~(Ei \$gamard2allconj(i,n))": def tmconj "Et t<=n & \$tmfactoreq(j,i+t,n-t) & \$tmfactoreq(i,(j+n)-t,t)": def tmmeso "\$tmconj(i,i+n,n) & ~\$tmfactoreq(i,i+n,n)": def tmmesolength "Ei \$tmmeso(i,n)": def thuepal "Ei At t T[i+t] = T[(i+n)-(t+1)]": eval fibpal "?msd_fib An Ei As,t (s>=i & t>=i & s+t+1=2*i+n) => F[s]=F[t]": eval pal "?msd_fib n>=1 & As,t (s>=i & t>=i & s+t+1=2*i+n) => F[s]=F[t]": def fpal "?msd_fib As,t (s>=i&t>=i&s+t+1=2*i+n) => F[s]=F[t]": def feven "?msd_fib Em n=2*m": def fodd "?msd_fib Em n=2*m+1": def ffactoreq "?msd_fib At t F[i+t]=F[j+t]": def onepal "?msd_fib Ei (\$fpal(i,n) & Aj \$fpal(j,n) => \$ffactoreq(i,j,n))": def twopal "?msd_fib Ei,j (\$fpal(i,n) & \$fpal(j,n) & (~\$ffactoreq(i,j,n)) & Ak (\$fpal(k,n)=>(\$ffactoreq(i,k,n)| \$ffactoreq(j,k,n))))": eval checkonepal "?msd_fib An \$onepal(n) <=> \$feven(n)": eval checktwopal "?msd_fib An \$twopal(n) <=> \$fodd(n)": reg isfib msd_fib "0*10*": eval fpalp "?msd_fib An \$fpal(0,n)<=>(Es (\$isfib(s) & s=n+2))": def tmpal "At t T[i+t] = T[(i+n)-(t+1)]": def tmfactoreq "At t T[i+t]=T[j+t]": def mpotm "Ei \$tmpal(i,n) & ~\$tmpal(i-1,n+2)": def mptm "Ei \$tmpal(i,n) & ~(Ej \$tmfactoreq(i,j,n) & T[j-1]=T[j+n])": def rspal "At t RS[i+t] = RS[(i+n)-(t+1)]": def rsfaceq "At t RS[i+t]=RS[j+t]": def mpors "Ei \$rspal(i,n) & ~\$rspal(i-1,n+2)": def mprs "Ei \$rspal(i,n) & ~(Ej \$rsfaceq(i,j,n) & RS[j-1]=RS[j+n])": def ispal "Au,v (u>=j & u T[u]=T[v]": def threepal "Ej,k j>0 & j=i & t>=j & s+t+1=i+j+n) => T[s]=T[t]": eval tmmi "Ai,n Ej \$revchktm(i,j,n)": def fibnearpal "?msd_fib Ek 2*k+1 F[i+t]=F[(i+n)-(t+1)]": def fibnearpallen "?msd_fib Ei \$fibnearpal(i,n)": morphism revmor "0->0012 1->0112": image FS revmor T: def fsrevchk "As,t (s>=i & t>=j & s+t+1=i+j+n) => FS[s]=FS[t]": eval fsrevfree "Ai,j,n (n>=3) => ~\$fsrevchk(i,j,n)": eval fsaper "~Ep,n (p>=1) & (Ai (i>=n) => FS[i]=FS[i+p])": def antipalf "?msd_fib As,t (s>=i & t>=i & s+t+1=2*i+n) => F[s]!=F[t]": def ffactoreq "?msd_fib At t F[i+t]=F[j+t]": def foapf "?msd_fib \$antipalf(i,n)&Aj j~\$ffactoreq(i,j,n)": eval tmhasoverpal "Ei,n n>=1 & (T[i]=T[i+n]) & (T[i]=T[i+2*n]) & At (t>=1 & t T[i+t]=T[(i+2*n)-t]": def ffactoreq "?msd_fib At t F[i+t]=F[j+t]": def fibbord "?msd_fib j>=1 & j T[i+t]=T[j+t]": def tmbord "j>=1 & j ~\$nobord(n)": def ffactoreq "?msd_fib At t F[i+t]=F[j+t]": def fibrevchk "?msd_fib As,t (s>=i & t>=j & s+t+1=i+j+n) => F[s]=F[t]": def fibbord "?msd_fib m>=1 & m \$ffactoreq(i,(i+n)-m,m)": def funbord "?msd_fib Am ~\$fibbord(i,m,n)": def funbordlength "?msd_fib Ei \$funbord(i,n)": def funbordtwo "?msd_fib Ei,j (\$funbord(i,n) & \$funbord(j,n) & ~\$ffactoreq(i,j,n))": def funbordrev "?msd_fib \$funbordlength(n) & Ai,j (\$funbord(i,n) & \$funbord(j,n)) => (\$ffactoreq(i,j,n) | \$fibrevchk(i,j,n))": def tmfactoreq "At t T[i+t]=T[j+t]": def tmbord "m>=1 & m \$tmfactoreq(i,(i+n)-m,m)": def tmsquare "\$tmfactoreq(i,i+n,n)": def tmunb "Am ~\$tmbord(i,m,n)": def tmframe "n>=1 & \$tmunb(i,n) & \$tmsquare(i,n)": def factordist2 "Ek,l k T[i+t]=T[j+t]": def border2m "\$factordist2(i,(i+n)-k,k)": eval b2test "An (n>=3) <=> Ei,k k>0 & ki & \$tmfactoreq(i,j,n)": def tmlinrec "Ai,n n>=3 => Ej (j>=1 & j+18<=9*n & \$tmfactoreq(i,i+j,n))": def ffactoreq "?msd_fib At (t F[i+t] = F[j+t])": def fibgf "?msd_fib Ai Ej (j>=s & j=s & k (~\$ffactoreq(i,k,n))))": eval fibhasgf "?msd_fib An Es,t \$fibgf(n,s,t)": def returntm "En \$tmfactoreq(i,j,n) & Am (i ~\$tmfactoreq(i,m,n)": def tmfactoreq "At t T[i+t]=T[j+t]": def tmprim "~(Ej j>0 & j T[i+l]=T[j+l]) & T[i+t]=@0 & T[j+t]=@1)": def tmlyndon "\$tmprim(i,n) & Aj (i \$tmlesst(i,j,n,(n+i)-j)": def tmlynlen "Ei \$tmlyndon(i,n)": def isin "ip<=i & jp>=j": def strictlyin "\$isin(i,ip,j,jp) & (ipj)": def tmfactoreq "At t T[i+t]=T[j+t]": def tmprim "~(Ej j>0 & j T[i+l]=T[j+l]) & T[i+t]=@0 & T[j+t]=@1)": def tmlyndon "\$tmprim(i,n) & Aj (i \$tmlesst(i,j,n,(n+i)-j)": def islynd "\$tmlyndon(i,(j+1)-i)": def lyndonf "\$islynd(i,j) & A ip,jp \$strictlyin(i,ip,j,jp) => ~\$islynd(ip,jp)": def tmfactoreq "At t T[i+t]=T[j+t]": def tmoccurs "m<=n & Ek k+m<=n & \$tmfactoreq(i,j+k,m)": def tmbord "m>=1 & m \$tmfactoreq(i,(i+n)-m,m)": def tmclo "n<=1 | (Ej j=1 => Ei \$tmclo(i,n)": def pffactoreq "At t P[i+t]=P[j+t]": def pfoccurs "m<=n & Ek k+m<=n & \$pffactoreq(i,j+k,m)": def pfbord "m>=1 & m \$pffactoreq(i,(i+n)-m,m)": def pfclosed "n<=1 | (Ej j=r & i<=s": def subs "j<=i & i+m<=j+n": def pdpal "Ak k PD[i+k] = PD[i+n-1-k]": def pdfactoreq "Ak k PD[i+k]=PD[j+k]": def pdoccurs "m<=n & (Ek k+m<=n & \$pdfactoreq(i,j+k,m))": def pdrich "Am \$in(m,1,n) => Ej \$subs(j,i,1,m) & \$pdpal(j,(i+m)-j) & ~\$pdoccurs(j,i,(i+m)-j,m-1)": eval testpdrich "Ai,n \$pdrich(i,n)": def in "i>=r & i<=s": def pdfactoreq "Ak k PD[i+k] = PD[j+k]": def unipref "Aj (j>0 & j+m ~\$pdfactoreq(i,i+j,m)": def unisuff "Aj (j>0 & j+m ~\$pdfactoreq((i+n)-m,(i+n)-(m+j),m)": def pdbord "\$in(m,1,n) & \$pdfactoreq(i,(i+n)-m,m)": def pdpriv "n>=1&Am \$in(m,1,n) => Ep p<=m&p>=1&\$unipref(i,p,m) & \$unisuff((i+n)-m,p,m) & \$pdbord(i,p,n)": eval pdprivlen "Ei \$pdpriv(i,n)": def in "i>=r & i<=s": def tmfactoreq "Ak k T[i+k] = T[j+k]": def tmunipref "Aj (j>0 & j+m ~\$tmfactoreq(i,i+j,m)": def tmunisuff "Aj (j>0 & j+m ~\$tmfactoreq((i+n)-m,(i+n)-(m+j),m)": def tmbord "\$in(m,1,n) & \$tmfactoreq(i,(i+n)-m,m)": def tmpriv "n>=1 & Am \$in(m,1,n) => Ep p<=m & p>=1 & \$tmunipref(i,p,m)&\$tmunisuff((i+n)-m,p,m)&\$tmbord(i,p,n)": def tmprivlen "Ei \$tmpriv(i,n)": eval tmunprivlrun "An Ei At t ~\$tmprivlen(i+t)": eval tmprivlinf "Am En (n>m) & \$tmprivlen(n)": def isrs "?msd_fib Ej \$ffactoreq(i,j,n) & F[i+n] != F[j+n]": eval unirs "?msd_fib (An Ei \$isrs(i,n)) & ~(En,i,j \$isrs(i,n) & \$isrs(j,n) & ~\$ffactoreq(i,j,n))": def berstel "?msd_fib Aj,n,i (j F[i+j]=F[n-(j+1)]": def isbi "Ej,m \$tmfactoreq(i,j,n)&T[i+n]!=T[j+n] & \$tmfactoreq(i,m,n) & T[i-1]!=T[m-1]": def hasbi "Ei \$isbi(i,n)": def hastwobi "Ei,j \$isbi(i,n)&\$isbi(j,n)&~\$tmfactoreq(i,j,n)": eval hasthreebi "Ei,j,k,n \$isbi(i,n)&\$isbi(j,n)&\$isbi(k,n)& ~\$tmfactoreq(i,j,n)&~\$tmfactoreq(i,k,n)&~\$tmfactoreq(j,k,n)": def ismf "(~Ej \$tmfactoreq(i,j,n) & T[i+n]!=T[j+n]) & (Ejp \$tmfactoreq(i+1,jp,n-1) & T[i+n]!=T[(jp+n)-1])": def lengthmf "Ei \$ismf(i,n-1)": def firstmf "\$ismf(i,n) & Aj (j ~\$tmfactoreq(i,j,n)": reg power2 msd_2 "0*10*": eval shurtest "An \$lengthmf(n) <=> ((n=3) | Ei \$power2(i) & n=3*i+2)": def fibsubs "?msd_fib j<=i & i+m<=j+n": def ffactoreq "?msd_fib At t F[i+t]=F[j+t]": def fibunbal "?msd_fib Em m>=2 & (Ej,k \$fibsubs(j,i,m,n) & \$fibsubs(k,i,m,n) & \$ffactoreq(j+1,k+1,m-2) & F[j]=F[(j+m)-1] & F[k]=F[(k+m)-1] & F[j]!=F[k])": eval fibbal "?msd_fib Ai,n ~\$fibunbal(i,n)": def fibispal "?msd_fib As,t (s>=i&t>=i&s+t+1=2*i+n)=>F[s]=F[t]": def christof "?msd_fib (~\$fibunbal(i,n)) & F[i]=@0 & F[i+n-1]=@1 & \$fibispal(i+1,n-2)": morphism h "0->012 1->302 2->031 3->321": morphism tau1 "0->0 1->1 2->0 3->1": morphism tau2 "0->0 1->0 2->1 3->1": promote HH h: image MA tau1 HH: image MB tau2 HH: eval meph1 "?msd_3 Ai MW[2*i]=MA[i]": eval meph2 "?msd_3 Ai MW[2*i+1]=MB[i]": def mephasq "?msd_3 Ei Aj j MA[i+j]=MA[i+j+n]": def mephbsq "?msd_3 Ei Aj j MB[i+j]=MB[i+j+n]": eval mephabcheck "?msd_3 Ec An (\$mephasq(n) => n n MW[i+j]=MW[i+j+n]": eval mwsqcheck "?msd_3 Ac En n>c & \$mephsq(n)": def common "Ei,j At t T[i+t]=RS[j+t]": def tmsubttm "Ej At t T[i]=TTM[j]": def ttmsubtm "Ej At t TTM[i]=T[j]": eval equal "Ai,n \$tmsubttm(i,n) & \$ttmsubtm(i,n)": eval checkproxttm "An Ei Aj j T[i+j]=TTM[i+j]": def yy "T[i+j]=@1": eval framecheck "Em,n,p,q m (\$yy(i,p) <=> \$yy(i,q))) & (Aj (p<=j & j<=q) => (\$yy(m,j) <=> \$yy(n,j)))": def tmfactoreq "At t T[i+t]=T[j+t]": def tmlt "Et t T[n+1]=@0": def rfactoreq "At t RS[i+t]=RS[j+t]": def ltr "Et t=1) => (\$lleastr(n) <=> RS[n-1]=@1)": reg power2 msd_2 "0*10*": eval bcheck1 "Ax,i (\$power2(x) & x>=4 & i>=2 & i B[i]=B[2*x+1-i]": eval bcheck2 "Ax (\$power2(x) & x>=4) => (B[x]=@3 & B[x+1]=@1)": def tmfe "A u,v (u>=i & u<=j & v+j=u+k) => T[u]=T[v]": def stringatt2 "Ei1,i2 (i1 (Er,s r<=s & s