eval zeros "?msd_pisot4 Ai,j \$pisi(i,j,0)": eval induc "?msd_pisot4 Ai,j,n (\$pisi(i,j,n) & PI[i+n]=PI[j+n]) => \$pisi(i,j,n+1)": eval pisotsc n "?msd_pisot4 Aj j ~\$pisi(i,j,n)": eval c2n1 n "?msd_pisot4 i<2*n+1": def pisotlargepow "?msd_pisot4 Ei (n>=1) & At (t>=i & t<=i+n) => PI[t]=PI[t+n]": # this will require 90 Gigs of storage and # approximately 1200000ms of CPU time def maximalreps "?msd_pisot4 Ei (PI[i+n] != PI[i+n+p]) & \$pisotlargepow(p) & (Aj (j PI[i+j] = PI[i+j+p])": def highestpow "?msd_pisot4 (p>=1) & \$pisotlargepow(p) & \$maximalreps(n,p) & (Am \$maximalreps(m,p) => m <= n)": eval tmp0 "?msd_pisot4 An,x ((\$psynch0(n,x) & PI[n]=@0) => \$psynch0(n+1,x+1)) & ((\$psynch0(n,x) & PI[n]!=@0) => \$psynch0(n+1,x))": eval tmp1 "?msd_pisot4 An,x ((\$psynch1(n,x) & PI[n]=@1) => \$psynch1(n+1,x+1)) & ((\$psynch1(n,x) & PI[n]!=@1) => \$psynch1(n+1,x))": eval tmp2 "?msd_pisot4 An,x ((\$psynch2(n,x) & PI[n]=@2) => \$psynch2(n+1,x+1)) & ((\$psynch2(n,x) & PI[n]!=@2) => \$psynch2(n+1,x))": def pcount0 "?msd_pisot4 Ex,y \$psynch0(i,x) & \$psynch0(i+n,y) & y=x+z": def pcount1 "?msd_pisot4 Ex,y \$psynch1(i,x) & \$psynch1(i+n,y) & y=x+z": def pcount2 "?msd_pisot4 Ex,y \$psynch2(i,x) & \$psynch2(i+n,y) & y=x+z": def twobalanced0 "?msd_pisot4 Ai,j,n,x,y (\$pcount0(i,n,x) & \$pcount0(j,n,y)) => (y<=x+2 & x<=y+2)": def twobalanced1 "?msd_pisot4 Ai,j,n,x,y (\$pcount1(i,n,x) & \$pcount1(j,n,y)) => (y<=x+2 & x<=y+2)": def twobalanced2 "?msd_pisot4 Ai,j,n,x,y (\$pcount2(i,n,x) & \$pcount2(j,n,y)) => (y<=x+2 & x<=y+2)": def min0 "?msd_pisot4 Ei \$pcount0(i,n,x) & Aj,y \$pcount0(j,n,y) => y>=x": def min1 "?msd_pisot4 Ei \$pcount1(i,n,x) & Aj,y \$pcount1(j,n,y) => y>=x": def min2 "?msd_pisot4 Ei \$pcount2(i,n,x) & Aj,y \$pcount2(j,n,y) => y>=x": def validtriples "?msd_pisot4 Ei,n,a,b,c \$pcount0(i,n,a+x) & \$min0(n,a) & \$pcount1(i,n,b+y) & \$min1(n,b) & \$pcount2(i,n,c+z) & \$min2(n,c)": def a001 "?msd_pisot4 Ei,x,y,z \$pcount0(i,n,x) & \$min0(n,x) & \$pcount1(i,n,y) & \$min1(n,y)& \$pcount2(i,n,z+1) & \$min2(n,z)": def a002 "?msd_pisot4 Ei,x,y,z \$pcount0(i,n,x) & \$min0(n,x) & \$pcount1(i,n,y) & \$min1(n,y) & \$pcount2(i,n,z+2) & \$min2(n,z)": def a010 "?msd_pisot4 Ei,x,y,z \$pcount0(i,n,x) & \$min0(n,x) & \$pcount1(i,n,y+1) & \$min1(n,y) & \$pcount2(i,n,z) & \$min2(n,z)": def a011 "?msd_pisot4 Ei,x,y,z \$pcount0(i,n,x) & \$min0(n,x) & \$pcount1(i,n,y+1) & \$min1(n,y) & \$pcount2(i,n,z+1) & \$min2(n,z)": def a012 "?msd_pisot4 Ei,x,y,z \$pcount0(i,n,x) & \$min0(n,x) & \$pcount1(i,n,y+1) & \$min1(n,y) & \$pcount2(i,n,z+2) & \$min2(n,z)": def a020 "?msd_pisot4 Ei,x,y,z \$pcount0(i,n,x) & \$min0(n,x) & \$pcount1(i,n,y+2) & \$min1(n,y) & \$pcount2(i,n,z) & \$min2(n,z)": def a021 "?msd_pisot4 Ei,x,y,z \$pcount0(i,n,x) & \$min0(n,x) & \$pcount1(i,n,y+2) & \$min1(n,y) & \$pcount2(i,n,z+1) & \$min2(n,z)": def a100 "?msd_pisot4 Ei,x,y,z \$pcount0(i,n,x+1) & \$min0(n,x) & \$pcount1(i,n,y) & \$min1(n,y) & \$pcount2(i,n,z) & \$min2(n,z)": def a101 "?msd_pisot4 Ei,x,y,z \$pcount0(i,n,x+1) & \$min0(n,x) & \$pcount1(i,n,y) & \$min1(n,y) & \$pcount2(i,n,z+1) & \$min2(n,z)": def a102 "?msd_pisot4 Ei,x,y,z \$pcount0(i,n,x+1) & \$min0(n,x) & \$pcount1(i,n,y) & \$min1(n,y) & \$pcount2(i,n,z+2) & \$min2(n,z)": def a110 "?msd_pisot4 Ei,x,y,z \$pcount0(i,n,x+1) & \$min0(n,x) & \$pcount1(i,n,y+1) & \$min1(n,y) & \$pcount2(i,n,z) & \$min2(n,z)": def a111 "?msd_pisot4 Ei,x,y,z \$pcount0(i,n,x+1) & \$min0(n,x) & \$pcount1(i,n,y+1) & \$min1(n,y) & \$pcount2(i,n,z+1) & \$min2(n,z)": def a120 "?msd_pisot4 Ei,x,y,z \$pcount0(i,n,x+1) & \$min0(n,x) & \$pcount1(i,n,y+2) & \$min1(n,y) & \$pcount2(i,n,z) & \$min2(n,z)": def a200 "?msd_pisot4 Ei,x,y,z \$pcount0(i,n,x+2) & \$min0(n,x) & \$pcount1(i,n,y) & \$min1(n,y) & \$pcount2(i,n,z) & \$min2(n,z)": def a201 "?msd_pisot4 Ei,x,y,z \$pcount0(i,n,x+2) & \$min0(n,x) & \$pcount1(i,n,y) & \$min1(n,y) & \$pcount2(i,n,z+1) & \$min2(n,z)": def a210 "?msd_pisot4 Ei,x,y,z \$pcount0(i,n,x+2) & \$min0(n,x) & \$pcount1(i,n,y+1) & \$min1(n,y) & \$pcount2(i,n,z) & \$min2(n,z)": def num1 "?msd_pisot4 \$a001(n) & ~\$a002(n) & \$a010(n) & ~\$a011(n) & ~\$a012(n) & ~\$a020(n) & ~\$a021(n) & \$a100(n) & ~\$a101(n) & ~\$a102(n) & ~\$a110(n) & ~\$a111(n) & ~\$a120(n) & ~\$a200(n) & ~\$a201(n) & ~\$a210(n)": def num2 "?msd_pisot4 ~\$a001(n) & ~\$a002(n) & ~\$a010(n) & \$a011(n) & ~\$a012(n) & ~\$a020(n) & ~\$a021(n) & ~\$a100(n) & \$a101(n) & ~\$a102(n) & \$a110(n) & ~\$a111(n) & ~\$a120(n) & ~\$a200(n) & ~\$a201(n) & ~\$a210(n)": def num3 "?msd_pisot4 ~\$a001(n) & ~\$a002(n) & ~\$a010(n) & \$a011(n) & ~\$a012(n) & ~\$a020(n) & ~\$a021(n) & ~\$a100(n) & \$a101(n) & ~\$a102(n) & \$a110(n) & ~\$a111(n) & ~\$a120(n) & \$a200(n) & ~\$a201(n) & ~\$a210(n)": def num4 "?msd_pisot4 ~\$a001(n) & \$a002(n) & ~\$a010(n) & \$a011(n) & ~\$a012(n) & ~\$a020(n) & ~\$a021(n) & ~\$a100(n) & \$a101(n) & ~\$a102(n) & \$a110(n) & ~\$a111(n) & ~\$a120(n) & ~\$a200(n) & ~\$a201(n) & ~\$a210(n)": def num5 "?msd_pisot4 ~\$a001(n) & ~\$a002(n) & ~\$a010(n) & \$a011(n) & ~\$a012(n) & \$a020(n) & ~\$a021(n) & ~\$a100(n) & \$a101(n) & ~\$a102(n) & \$a110(n) & ~\$a111(n) & ~\$a120(n) & ~\$a200(n) & ~\$a201(n) & ~\$a210(n)": def num6 "?msd_pisot4 ~\$a001(n) & \$a002(n) & ~\$a010(n) & \$a011(n) & ~\$a012(n) & ~\$a020(n) & ~\$a021(n) & ~\$a100(n) & \$a101(n) & ~\$a102(n) & \$a110(n) & ~\$a111(n) & ~\$a120(n) & \$a200(n) & ~\$a201(n) & ~\$a210(n)": def num7 "?msd_pisot4 ~\$a001(n) & ~\$a002(n) & ~\$a010(n) & ~\$a011(n) & \$a012(n) & ~\$a020(n) & ~\$a021(n) & ~\$a100(n) & ~\$a101(n) & \$a102(n) & ~\$a110(n) & \$a111(n) & ~\$a120(n) & ~\$a200(n) & \$a201(n) & \$a210(n)": def num8 "?msd_pisot4 ~\$a001(n) & ~\$a002(n) & ~\$a010(n) & ~\$a011(n) & ~\$a012(n) & ~\$a020(n) & \$a021(n) & ~\$a100(n) & ~\$a101(n) & ~\$a102(n) & ~\$a110(n) & \$a111(n) & \$a120(n) & ~\$a200(n) & \$a201(n) & \$a210(n)": def num9 "?msd_pisot4 ~\$a001(n) & ~\$a002(n) & ~\$a010(n) & \$a011(n) & ~\$a012(n) & \$a020(n) & ~\$a021(n) & ~\$a100(n) & \$a101(n) & ~\$a102(n) & \$a110(n) & ~\$a111(n) & ~\$a120(n) & \$a200(n) & ~\$a201(n) & ~\$a210(n)": def num10 "?msd_pisot4 ~\$a001(n) & \$a002(n) & ~\$a010(n) & \$a011(n) & ~\$a012(n) & \$a020(n) & ~\$a021(n) & ~\$a100(n) & \$a101(n) & ~\$a102(n) & \$a110(n) & ~\$a111(n) & ~\$a120(n) & ~\$a200(n) & ~\$a201(n) & ~\$a210(n)": def num11 "?msd_pisot4 ~\$a001(n) & ~\$a002(n) & ~\$a010(n) & ~\$a011(n) & \$a012(n) & ~\$a020(n) & \$a021(n) & ~\$a100(n) & ~\$a101(n) & \$a102(n) & ~\$a110(n) & \$a111(n) & \$a120(n) & ~\$a200(n) & ~\$a201(n) & ~\$a210(n)": def num12 "?msd_pisot4 ~\$a001(n) & ~\$a002(n) & ~\$a010(n) & ~\$a011(n) & \$a012(n) & ~\$a020(n) & \$a021(n) & ~\$a100(n) & ~\$a101(n) & ~\$a102(n) & ~\$a110(n) & \$a111(n) & \$a120(n) & ~\$a200(n) & \$a201(n) & \$a210(n)": def num13 "?msd_pisot4 ~\$a001(n) & ~\$a002(n) & ~\$a010(n) & ~\$a011(n) & \$a012(n) & ~\$a020(n) & \$a021(n) & ~\$a100(n) & ~\$a101(n) & \$a102(n) & ~\$a110(n) & \$a111(n) & ~\$a120(n) & ~\$a200(n) & \$a201(n) & \$a210(n)": def num14 "?msd_pisot4 ~\$a001(n) & ~\$a002(n) & ~\$a010(n) & ~\$a011(n) & \$a012(n) & ~\$a020(n) & \$a021(n) & ~\$a100(n) & ~\$a101(n) & \$a102(n) & ~\$a110(n) & \$a111(n) & \$a120(n) & ~\$a200(n) & ~\$a201(n) & \$a210(n)": def num15 "?msd_pisot4 ~\$a001(n) & ~\$a002(n) & ~\$a010(n) & ~\$a011(n) & \$a012(n) & ~\$a020(n) & ~\$a021(n) & ~\$a100(n) & ~\$a101(n) & \$a102(n) & ~\$a110(n) & \$a111(n) & \$a120(n) & ~\$a200(n) & \$a201(n) & \$a210(n)": def num16 "?msd_pisot4 ~\$a001(n) & ~\$a002(n) & ~\$a010(n) & ~\$a011(n) & ~\$a012(n) & ~\$a020(n) & \$a021(n) & ~\$a100(n) & ~\$a101(n) & \$a102(n) & ~\$a110(n) & \$a111(n) & \$a120(n) & ~\$a200(n) & \$a201(n) & \$a210(n)": def num17 "?msd_pisot4 ~\$a001(n) & ~\$a002(n) & ~\$a010(n) & ~\$a011(n) & \$a012(n) & ~\$a020(n) & \$a021(n) & ~\$a100(n) & ~\$a101(n) & \$a102(n) & ~\$a110(n) & \$a111(n) & \$a120(n) & ~\$a200(n) & \$a201(n) & ~\$a210(n)": def num18 "?msd_pisot4 ~\$a001(n) & ~\$a002(n) & ~\$a010(n) & ~\$a011(n) & \$a012(n) & ~\$a020(n) & \$a021(n) & ~\$a100(n) & ~\$a101(n) & \$a102(n) & ~\$a110(n) & \$a111(n) & \$a120(n) & ~\$a200(n) & \$a201(n) & \$a210(n)": eval coverall "?msd_pisot4 An (n>=1) => (\$num1(n)|\$num2(n)|\$num3(n)|\$num4(n)|\$num5(n)| \$num6(n)|\$num7(n)|\$num8(n)|\$num9(n)|\$num10(n)|\$num11(n)|\$num12(n)| \$num13(n)|\$num14(n)|\$num15(n)|\$num16(n)|\$num17(n)|\$num18(n))": combine pab num1 num2 num3 num4 num5 num6 num7 num8 num9 num10 num11 num12 num13 num14 num15 num16 num17 num18: morphism abc "0->1 1->3 2->3 3->4 4->4 5->4 6->5 7->5 8->5 9->5 10->5 11->5 12->6 13->6 14->6 15->6 16->6 17->6 18->7": image BC3 abc pab: def pisotrightspec "?msd_pisot4 Ej \$pisi(i,j,n) & PI[i+n]!=PI[j+n]": def pisotleftspec "?msd_pisot4 Ej \$pisi(i,j,n) & PI[i-1]!=PI[j-1]": def pisotbispec "?msd_pisot4 \$pisotrightspec(i,n) & \$pisotleftspec(i,n)": def pisotbispeclen "?msd_pisot4 Ei \$pisotbispec(i,n)": def poccur "?msd_pisot4 Ai Ej j>i & j<=i+x & \$pisi(i,j,n)": def precur "?msd_pisot4 \$poccur(n,x) & ~\$poccur(n,x-1)": reg pix msd_pisot4 "0*10*": def precB "?msd_pisot4 Ex \$pix(x) & \$precur(n,x) & ~\$precur(n-1,x)": def precC "?msd_pisot4 Ex \$pix(x) & \$precur(n,x) & ~\$precur(n+1,x)":