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