# 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))":