eval thm1test "(~Ei, n (n>=3) & At (t T1[i+t]=T1[i+n+t]) & (~Ej T1[j]=@1 & T1[j+1]=@1 & T1[j+2]=@1 & T1[j+3]=@1)": # no squares of order >= 3, and only squares of smaller order # are allowed to be 00, 11, 0000, 0101, 1010, but not 1111. def ochem "Ei Ej (n=50*i+j) & (j < 50) & ((VTM[i]=@0 & (j=3|j=4|j=7|j=9|j=10|j=14|j=15|j=16|j=19|j=21|j=22|j=25|j=26|j=27|j=31|j=33|j=34|j=35|j=38|j=40|j=41|j=45|j=47|j=48|j=49)) | (VTM[i]=@1 & (j=3|j=4|j=7|j=9|j=10|j=14|j=16|j=17|j=18|j=21|j=23|j=24|j=27|j=28|j=29|j=33|j=35|j=36|j=40|j=41|j=42|j=45|j=47|j=48|j=49)) | (VTM[i]=@2 & (j=3|j=4|j=7|j=9|j=10|j=14|j=16|j=17|j=18|j=21|j=23|j=24|j=28|j=29|j=30|j=33|j=35|j=36|j=37|j=41|j=43|j=44|j=47|j=48|j=49)))": def thm2test "(~Ei, n (n>=3) & At (t (\$ochem(i+t) <=> \$ochem(i+n+t))) & (~Ej (\$ochem(j) <=> \$ochem(j+1)) & (\$ochem(j) <=> \$ochem(j+2)) & (\$ochem(j) <=> \$ochem(j+3))) & (~Ej (\$ochem(j) & (~\$ochem(j+1)) & \$ochem(j+2) & (~\$ochem(j+3))))": # 95 gigs of main memory needed! def thm4test "(~Ei, n (n>=3) & At (t HN[i+t]=HN[i+t+n]) & (~Ej HN[j]=HN[j+1] & HN[j]=HN[j+2] & HN[j]=HN[j+3]) & (~Ej HN[j]=@1 & HN[j+1]=@0 & HN[j+2]=@1 & HN[j+3]=@0)": # 24 gigs of main memory needed! def thm5test "(~Ei, n (n>=3) & At (t GAB[i+t]=GAB[i+t+n]) & (~Ej GAB[j]=GAB[j+1] & GAB[j]=GAB[j+2] & GAB[j]=GAB[j+3]) & (~Ej GAB[j]=@0 & GAB[j+1]=@1 & GAB[j+2]=@0 & GAB[j+3]=@1)": eval thm6test "(~Ei En (n>=3) & At (t Q[i+t] = Q[i+t+n]) & (~Ei (Q[i]=Q[i+1])&(Q[i]=Q[i+2])&(Q[i]=Q[i+3])) & (~Ei (Q[i]=@0)&(Q[i+1]=@1)&(Q[i+2]=@0)&(Q[i+3]=@1))":