# commands for circular critical exponents of # prefixes and factors of Thue-Morse # this accompanies the paper "Circular critical exponents for Thue-Morse factors" # by Shallit and Zarifi 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])": def prefge11 "E i,m,p (p >= 1) & (m <= n) & (i < n) & (m >= p) & $crep(i,m,n,p,0)": def prefgt11 "E i,m,p (p >= 1) & (m <= n) & (i < n) & (m > p) & $crep(i,m,n,p,0)": def prefeq11 "$prefge11(n) & ~$prefgt11(n)": def prefge21 "E i,m,p (p >= 1) & (m <= n) & (i < n) & (m >= 2*p) & $crep(i,m,n,p,0)": def prefgt21 "E i,m,p (p >= 1) & (m <= n) & (i < n) & (m > 2*p) & $crep(i,m,n,p,0)": def prefeq21 "$prefge21(n) & ~$prefgt21(n)": def prefge73 "E i,m,p (p >= 1) & (m <= n) & (i < n) & (3*m >= 7*p) & $crep(i,m,n,p,0)": def prefgt73 "E i,m,p (p >= 1) & (m <= n) & (i < n) & (3*m > 7*p) & $crep(i,m,n,p,0)": def prefeq73 "$prefge73(n) & ~$prefgt73(n)": def prefge52 "E i,m,p (p >= 1) & (m <= n) & (i < n) & (2*m >= 5*p) & $crep(i,m,n,p,0)": def prefgt52 "E i,m,p (p >= 1) & (m <= n) & (i < n) & (2*m > 5*p) & $crep(i,m,n,p,0)": def prefeq52 "$prefge52(n) & ~$prefgt52(n)": def prefge135 "E i,m,p (p >= 1) & (m <= n) & (i < n) & (5*m >= 13*p) & $crep(i,m,n,p,0)": def prefgt135 "E i,m,p (p >= 1) & (m <= n) & (i < n) & (5*m > 13*p) & $crep(i,m,n,p,0)": def prefeq135 "$prefge135(n) & ~$prefgt135(n)": def prefge83 "E i,m,p (p >= 1) & (m <= n) & (i < n) & (3*m >= 8*p) & $crep(i,m,n,p,0)": def prefgt83 "E i,m,p (p >= 1) & (m <= n) & (i < n) & (3*m > 8*p) & $crep(i,m,n,p,0)": def prefeq83 "$prefge83(n) & ~$prefgt83(n)": def prefge31 "E i,m,p (p >= 1) & (m <= n) & (i < n) & (m >= 3*p) & $crep(i,m,n,p,0)": def prefgt31 "E i,m,p (p >= 1) & (m <= n) & (i < n) & (m > 3*p) & $crep(i,m,n,p,0)": def prefeq31 "$prefge31(n) & ~$prefgt31(n)": eval testpref "An (n>=1) => ($prefeq11(n) | $prefeq21(n) | $prefeq73(n) | $prefeq52(n) | $prefeq135(n) | $prefeq83(n) | $prefeq31(n))": def facge11 "E i,m,p (p>=1) & (m <= n) & (i>=s) & (i= p) & $crep(i,m,n,p,s)": def facgt11 "E i,m,p (p>=1) & (m <= n) & (i>=s) & (i p) & $crep(i,m,n,p,s)": def faceq11 "$facge11(n,s) & ~$facgt11(n,s)": def facex11 "Es $faceq11(n,s)": def facge21 "E i,m,p (p>=1) & (m <= n) & (i>=s) & (i= 2*p) & $crep(i,m,n,p,s)": def facgt21 "E i,m,p (p>=1) & (m <= n) & (i>=s) & (i 2*p) & $crep(i,m,n,p,s)": def faceq21 "$facge21(n,s) & ~$facgt21(n,s)": def facex21 "Es $faceq21(n,s)": def facge73 "E i,m,p (p>=1) & (m <= n) & (i>=s) & (i= 7*p) & $crep(i,m,n,p,s)": def facgt73 "E i,m,p (p>=1) & (m <= n) & (i>=s) & (i 7*p) & $crep(i,m,n,p,s)": def faceq73 "$facge73(n,s) & ~$facgt73(n,s)": def facex73 "Es $faceq73(n,s)": def facge177 "E i,m,p (p>=1) & (m <= n) & (i>=s) & (i= 17*p) & $crep(i,m,n,p,s)": def facgt177 "E i,m,p (p>=1) & (m <= n) & (i>=s) & (i 17*p) & $crep(i,m,n,p,s)": def faceq177 "$facge177(n,s) & ~$facgt177(n,s)": def facex177 "Es $faceq177(n,s)": def facge52 "E i,m,p (p>=1) & (m <= n) & (i>=s) & (i= 5*p) & $crep(i,m,n,p,s)": def facgt52 "E i,m,p (p>=1) & (m <= n) & (i>=s) & (i 5*p) & $crep(i,m,n,p,s)": def faceq52 "$facge52(n,s) & ~$facgt52(n,s)": def facex52 "Es $faceq52(n,s)": def facge135 "E i,m,p (p>=1) & (m <= n) & (i>=s) & (i= 13*p) & $crep(i,m,n,p,s)": def facgt135 "E i,m,p (p>=1) & (m <= n) & (i>=s) & (i 13*p) & $crep(i,m,n,p,s)": def faceq135 "$facge135(n,s) & ~$facgt135(n,s)": def facex135 "Es $faceq135(n,s)": def facge83 "E i,m,p (p>=1) & (m <= n) & (i>=s) & (i= 8*p) & $crep(i,m,n,p,s)": def facgt83 "E i,m,p (p>=1) & (m <= n) & (i>=s) & (i 8*p) & $crep(i,m,n,p,s)": def faceq83 "$facge83(n,s) & ~$facgt83(n,s)": def facex83 "Es $faceq83(n,s)": def facge31 "E i,m,p (p>=1) & (m <= n) & (i>=s) & (i= 3*p) & $crep(i,m,n,p,s)": def facgt31 "E i,m,p (p>=1) & (m <= n) & (i>=s) & (i 3*p) & $crep(i,m,n,p,s)": def faceq31 "$facge31(n,s) & ~$facgt31(n,s)": def facex31 "Es $faceq31(n,s)": def facge103 "E i,m,p (p>=1) & (m <= n) & (i>=s) & (i= 10*p) & $crep(i,m,n,p,s)": def facgt103 "E i,m,p (p>=1) & (m <= n) & (i>=s) & (i 10*p) & $crep(i,m,n,p,s)": def faceq103 "$facge103(n,s) & ~$facgt103(n,s)": def facex103 "Es $faceq103(n,s)": def facge72 "E i,m,p (p>=1) & (m <= n) & (i>=s) & (i= 7*p) & $crep(i,m,n,p,s)": def facgt72 "E i,m,p (p>=1) & (m <= n) & (i>=s) & (i 7*p) & $crep(i,m,n,p,s)": def faceq72 "$facge72(n,s) & ~$facgt72(n,s)": def facex72 "Es $faceq72(n,s)": def facge113 "E i,m,p (p>=1) & (m <= n) & (i>=s) & (i= 11*p) & $crep(i,m,n,p,s)": def facgt113 "E i,m,p (p>=1) & (m <= n) & (i>=s) & (i 11*p) & $crep(i,m,n,p,s)": def faceq113 "$facge113(n,s) & ~$facgt113(n,s)": def facex113 "Es $faceq113(n,s)": def facge41 "E i,m,p (p>=1) & (m <= n) & (i>=s) & (i= 4*p) & $crep(i,m,n,p,s)": def facgt41 "E i,m,p (p>=1) & (m <= n) & (i>=s) & (i 4*p) & $crep(i,m,n,p,s)": def faceq41 "$facge41(n,s) & ~$facgt41(n,s)": def facex41 "Es $faceq41(n,s)": eval testfac "An (n>=1) => (As ($faceq11(n,s) | $faceq21(n,s) | $faceq73(n,s) | $faceq177(n,s) | $faceq52(n,s) | $faceq135(n,s) | $faceq83(n,s) | $faceq31(n,s) | $faceq103(n,s) | $faceq72(n,s) | $faceq113(n,s) | $faceq41(n,s)))": def facex11 "Es $faceq11(n,s)": def facex21 "Es $faceq21(n,s)": def facex73 "Es $faceq73(n,s)": def facex177 "Es $faceq177(n,s)": def facex52 "Es $faceq52(n,s)": def facsmall11 "$facex11(n) & (As $facge11(n,s))": def facsmall21 "$facex21(n) & (As $facge21(n,s))": def facsmall73 "$facex73(n) & (As $facge73(n,s))": def facsmall177 "$facex177(n) & (As $facge177(n,s))": def facsmall52 "$facex52(n) & (As $facge52(n,s))": eval smallfactest "An (n>=1) => ($facsmall11(n) | $facsmall21(n) | $facsmall73(n) | $facsmall177(n) | $facsmall52(n))": def faclarge11 "$facex11(n) & (As ~$facgt11(n,s))": def faclarge21 "$facex21(n) & (As ~$facgt21(n,s))": def faclarge31 "$facex31(n) & (As ~$facgt31(n,s))": def faclarge72 "$facex72(n) & (As ~$facgt72(n,s))": def faclarge41 "$facex41(n) & (As ~$facgt41(n,s))": eval largefactest "An (n>=1) => ($faclarge11(n) | $faclarge21(n) | $faclarge31(n) | $faclarge72(n) | $faclarge41(n))":