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<i2 & i2<i3 & i3<i+m) =>
   E j1,j2,j3 j<=j1 & j1<j2 & j2<j3 & j3<j+n & T[i1]=T[j1]
   & T[i2]=T[j2] & T[i3]=T[j3]":
def simon "$simon1(i,j,m,n) & $simon1(j,i,n,m)":

def incblock "Ej (i<=j & j<i+n & At (i<=t & t<j) =>
   T[t]=T[t+n]) & T[j]=@0 & T[j+n]=@1 & (Au (j<u & u<i+n)
   => (T[u]=@1 & T[u+n]=@0))":

def test101 "T[j]=@1 & T[k]=@1 & k>=j+2 & At (t>j & t<k)
   => 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<n => CA[i+t]=@0) &
   CA[i+n]!=@0 & (i=0|CA[i-1]!=@0)":
def carun1 "?msd_3 n>=1 & (At t<n => 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<n => 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<n => 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<n =>
   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<n => T[i+t]=T[j+t]":
def tmnovelf "Aj j<i => ~$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<n) => 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<j) => ~$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<p) => ~$hasper(k,q))
   & (Aq,k k<i => ~$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<p => ~$hasper(k,q)) &
   (Aq,k k<i => ~$hasper(k,q))":

def fibquasi "?msd_fib Ai (Ej i<j+n&j<=i&$ffactoreq(0,j,n))":

reg isfib msd_fib "0*10*":
eval fibquasicheck "?msd_fib An (~$fibquasi(n)) <=>
   (Es $isfib(s) & n=s-1)":

eval ck2 "Ep,q 0<p & p<q & An (T[n]=T[n+p]|T[n]=T[n+q])":
eval ck3 "Ep,q,r 0<p & p<q & q<r &
    An (T[n]=T[n+p]|T[n]=T[n+q]|T[n]=T[n+r])":

def hassquare "Ei,n n>=1 & Aj j<n => X[i+j]=X[i+j+n]":

eval vtmsquare "Ei,n n>=1 & Aj j<n => VTM[i+j]=VTM[i+j+n]":


eval hanoisq "Ei,n n>=1 & Aj j<n => TH[i+j]=TH[i+j+n]":

def fibsquarelen "?msd_fib n>0 & Ei At t<n => 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<n => F[i+t] = F[i+n+t]":

eval fibals "?msd_fib Ai,m En n>m & At t<n => F[i+t]=F[i+n+t]":


def tribsquarelen "?msd_trib n>0&Ei At t<n=>TR[i+t]=TR[i+n+t]":


def tribsquarelen "?msd_trib n>0 & Ei Aj (j>=i & j<i+n) =>
   TR[j]=TR[j+n]":


eval tribals "?msd_trib Ai,m En (n>=m) &
   Au,v (u>=i & u<i+n & v=u+n) => TR[u]=TR[v]":

eval dean1 "Ei,n n>=1 & At t<n => 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<i+3*n)
   => F[t]=F[t+n]":

eval trib4p "?msd_trib Ei,n n>0 & At (t>=i & t<i+3*n)
   => 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<k
   & k<n & SA[i+j]!=SA[i+n+j] & SA[i+k]!=SA[i+n+k])":

eval leech "?msd_13 Ei,n n>=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<s)
   => X[i]=X[i+p])":
def isover0 "?msd_4 Ep (p>=1) & (s=r+2*p) & (Ai (r<=i & i+p<j)
   => X[i]=X[i+p]) & (j>=r+p => X[j-p]=@0) & (Ai (r<=i & i<j
   & i+p>=j+1 & i+p<=s) => X[i]=X[(i+p)-1]) & (j+p<=s =>
   X[(j+p)-1]=@0) & (Ai (j<=i & i+p<s) => X[i]=X[i+p])":
def isover1 "?msd_4 Ep (p>=1) & (s=r+2*p) & (Ai (r<=i & i+p<j)
   => X[i]=X[i+p]) & (j>=r+p => X[j-p]=@1) & (Ai (r<=i & i<j
   & i+p>=j+1 & i+p<=s) => X[i]=X[(i+p)-1]) & (j+p<=s =>
   X[(j+p)-1]=@1) & (Ai (j<=i & i+p<s) => 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<s & s<=i+n & $isover0(j,r,s)) &
   (Erp,sp rp>=i & rp<sp & sp<=i+n & $isover1(j,rp,sp)))":
reg power4 msd_4 "10*":
eval test_extremal "?msd_4 Ai $power4(i)=>$extremal(18*i,32*i)":

def tmfactoreq "At t<n => T[i+t]=T[j+t]":
def tmprim "~(Ej j>0 & j<n & $tmfactoreq(i,i+j,n-j) &
   $tmfactoreq(i,(i+n)-j,j))":
def tmprimlength "n>0 & $tmprim(0,n)":
eval tmprimcheck "An n>=1 => $tmprimlength(n)":

def sbfactoreq "At t<n => SB[i+t]=SB[j+t]":
def sbprim "~(Ej j>0 & j<n & $sbfactoreq(i,i+j,n-j) &
   $sbfactoreq(i,(i+n)-j,j))":
def sbnovelf "Aj j<i => ~$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<n => F[i+j]!=F[i+j+n]":
def antisf "?msd_fib Ei $isantif(i,n)":

def pdfactoreq "At t<n => PD[i+t]=PD[j+t]":
def pdrevcheck "At t<n => 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<n => 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<n) => 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<n) => 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<n) => 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<n) => 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<i+n) => T[j]=T[j+p]":
def tmlper "$tmperi(i,n,p)&(Aq (q>=1&q<p)=>~$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<i+n)
   => F[j]=F[j+p]":
def fiblper "?msd_fib $fibperi(i,n,p) & (Aq (q>=1 & q<p)
   => ~$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<i+n) =>
   TR[j]=TR[j+p]":
def triblper "?msd_trib $tribperi(i,n,p) & (Aq (q>=1 & q<p) =>
   ~$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<n => F[i+j]=F[i+j+p]":
def fiblper "?msd_fib $fibperi(i,n,p) & Aq q<p =>
   ~$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<n => T[j]=T[j+p]":
def lpertm "$pptm(n,p) & Aq q<p => ~$pptm(n,q)":
def longestm "$lpertm(n,p) & (Ar $lpertm(r,p) => r<=n)":

def crep "(Aj (j>=i & j+p<s+n & j+p<i+m) => T[j]=T[j+p]) &
   (Aj (j>=i & j<s+n & j+p>=s+n & j+p<i+m) =>
   T[j]=T[(j+p)-n]) & (Aj (j>=i & j>=s+n & j+p<i+m)
   => 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<s+n & $crep(i,m,n,p,s)) => 2*m <= 5*p":

def vfactoreq "At t<n => 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<j => 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<j & j+1<i+n) => $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<n => 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<n => TI[i+t]=TI[j+t]":
eval titest "An,i,j (n>=1 & i<j & $tifaceq(i,j,n)) => 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<i+n) =>
   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<i+n) =>
   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<i+n) =>
   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<n => 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<n => 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<n => T[i+t] = T[(i+n)-(t+1)]":
def tmfactoreq "At t<n => 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<n => RS[i+t] = RS[(i+n)-(t+1)]":
def rsfaceq "At t<n => 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<k & u+v+1=j+k) => T[u]=T[v]":
def threepal "Ej,k j>0 & j<k & k<n & $ispal(0,j) &
   $ispal(j,k) & $ispal(k,n)":


def revchktm "As,t (s>=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<n & F[i+k]!=F[(i+n)-(k+1)] &
   At (2*t+1<n & t!=k) => 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<n => F[i+t]=F[j+t]":
def foapf "?msd_fib $antipalf(i,n)&Aj j<i=>~$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<n) => T[i+t]=T[(i+2*n)-t]":

def ffactoreq "?msd_fib At t<n => F[i+t]=F[j+t]":
def fibbord "?msd_fib j>=1 & j<n & $ffactoreq(i,(i+n)-j,j)":
def bordfibpref "?msd_fib $fibbord(0,m,n)":

reg isfib msd_fib "0*10*":
def cummings "?msd_fib $isfib(n) & $bordfibpref(m,n)":

def tmfactoreq "At t<n => T[i+t]=T[j+t]":
def tmbord "j>=1 & j<n & $tmfactoreq(i,(i+n)-j,m)":
def tmunblength "Ei Am ~$tmbord(i,m,n)":
reg nobord msd_2 "0*1(01*0)*10*1":
eval tmchk "An $tmunblength(n) <=> ~$nobord(n)":

def ffactoreq "?msd_fib At t<n => 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<n & At t<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<n => T[i+t]=T[j+t]":
def tmbord "m>=1 & m<n & At t<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<l&l<n&T[i+k]!=T[j+k]&T[i+l]!=T[j+l]
   & At (t<n & t!=k & t!=l) => T[i+t]=T[j+t]":
def border2m "$factordist2(i,(i+n)-k,k)":
eval b2test "An (n>=3) <=> Ei,k k>0 & k<n & $border2m(i,k,n)":


eval tmur "An Ec Ai Ej j<=i+c & j>i & $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<n => F[i+t] = F[j+t])":
def fibgf "?msd_fib Ai Ej (j>=s & j<s+t & $ffactoreq(i,j,n)
   & (Ak (k>=s & k<s+t &  j!=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<m & m<j)
   => ~$tmfactoreq(i,m,n)":

def tmfactoreq "At t<n => T[i+t]=T[j+t]":
def tmprim "~(Ej j>0 & j<n & $tmfactoreq(i,i+j,n-j) &
   $tmfactoreq(i,(i+n)-j,j))":
def tmpref "m<n & $tmfactoreq(i,j,m)":
def tmlesst "$tmpref(i,j,m,n) | (Et t<m & t<n &
   (Al (l<t) => T[i+l]=T[j+l]) & T[i+t]=@0 & T[j+t]=@1)":
def tmlyndon "$tmprim(i,n) & Aj (i<j & j<i+n) =>
   $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) & (ip<i | jp>j)":
def tmfactoreq "At t<n => T[i+t]=T[j+t]":
def tmprim "~(Ej j>0 & j<n & $tmfactoreq(i,i+j,n-j) &
   $tmfactoreq(i,(i+n)-j,j))":
def tmpref "m<n & $tmfactoreq(i,j,m)":
def tmlesst "$tmpref(i,j,m,n) | (Et t<m & t<n & (Al l<t
   => T[i+l]=T[j+l]) & T[i+t]=@0 & T[j+t]=@1)":
def tmlyndon "$tmprim(i,n) & Aj (i<j & j<i+n) =>
   $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<n => T[i+t]=T[j+t]":
def tmoccurs "m<=n & Ek k+m<=n & $tmfactoreq(i,j+k,m)":
def tmbord "m>=1 & m<n & At t<m => $tmfactoreq(i,(i+n)-m,m)":
def tmclo "n<=1 | (Ej j<n & $tmbord(i,j,n) &
   ~$tmoccurs(i,i+1,j,n-2))":
eval tmclosall "An n>=1 => Ei $tmclo(i,n)":


def pffactoreq "At t<n => P[i+t]=P[j+t]":
def pfoccurs "m<=n & Ek k+m<=n & $pffactoreq(i,j+k,m)":
def pfbord "m>=1 & m<n & At t<m => $pffactoreq(i,(i+n)-m,m)":
def pfclosed "n<=1 | (Ej j<n & $pfbord(i,j,n) &
   ~$pfoccurs(i,i+1,j,n-2))":
def pfclosedlen "Ei $pfclosed(i,n)":

def in "i>=r & i<=s":
def subs "j<=i & i+m<=j+n":
def pdpal "Ak k<n => PD[i+k] = PD[i+n-1-k]":
def pdfactoreq "Ak k<n => 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<n => PD[i+k] = PD[j+k]":
def unipref "Aj (j>0 & j+m<n) => ~$pdfactoreq(i,i+j,m)":
def unisuff "Aj (j>0 & j+m<n) =>
   ~$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<n => T[i+k] = T[j+k]":
def tmunipref "Aj (j>0 & j+m<n) => ~$tmfactoreq(i,i+j,m)":
def tmunisuff "Aj (j>0 & j+m<n) =>
   ~$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<n => ~$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<n & $isrs(i,n)) =>
   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<i & $ismf(j,n)) =>
   ~$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<n => 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<n => MA[i+j]=MA[i+j+n]":
def mephbsq "?msd_3 Ei Aj j<n => MB[i+j]=MB[i+j+n]":
eval mephabcheck "?msd_3 Ec An ($mephasq(n) => n<c) &
   ($mephbsq(n) => n<c)":

def mwsq "?msd_3 Ei Aj j<n => MW[i+j]=MW[i+j+n]":
eval mwsqcheck "?msd_3 Ac En n>c & $mephsq(n)":

def common "Ei,j At t<n => T[i+t]=RS[j+t]":

def tmsubttm "Ej At t<n => T[i]=TTM[j]":
def ttmsubtm "Ej At t<n => TTM[i]=T[j]":
eval equal "Ai,n $tmsubttm(i,n) & $ttmsubtm(i,n)":

eval checkproxttm "An Ei Aj j<n => T[i+j]=TTM[i+j]":

def yy "T[i+j]=@1":
eval framecheck "Em,n,p,q m<n & p<q &
   (Ai (m<=i & i<=n) => ($yy(i,p) <=> $yy(i,q))) &
   (Aj (p<=j & j<=q) => ($yy(m,j) <=> $yy(n,j)))":

def tmfactoreq "At t<n => T[i+t]=T[j+t]":
def tmlt "Et t<n & $tmfactoreq(i,j,t) & T[i+t]<T[j+t]":
def tmleq "$tmlt(i,j,n) | $tmfactoreq(i,j,n)":
def lleast "Ei T[i+n]=@1 & Aj $tmleq(i,j,n+1)":
def checklltm "An $lleast(n) <=> T[n+1]=@0":

def rfactoreq "At t<n => RS[i+t]=RS[j+t]":
def ltr "Et t<n & $rfactoreq(i,j,t) & RS[i+t]<RS[j+t]":
def leqr "$ltr(i,j,n) | $rfactoreq(i,j,n)":
def lleastr "Ei RS[i+n]=@1 & Aj $leqr(i,j,n+1)":
def checkllrs "(~$lleastr(0)) & An (n>=1) =>
   ($lleastr(n) <=> RS[n-1]=@1)":

reg power2 msd_2 "0*10*":
eval bcheck1 "Ax,i ($power2(x) & x>=4 & i>=2 & i<x) =>
   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<n) & (i2<n) & Ak,l (k<=l & l<n)
   => (Er,s r<=s & s<n & (s+k=r+l) & $tmfe(k,l,s) &
   ((r<=i1 & i1<=s) | (r<=i2 & i2<=s)))":