def aut1 "(x+y)-z=0": def aut2 "x+(y-z)=0": eval test1 "\$aut1(1,1,2)": eval test2 "\$aut2(1,1,2)": ost name [0 1 2] [3 4]: def ffactoreq "?msd_fib At t F[i+t]=F[j+t]": def ftmeqfact1 "?msd_fib At Au (t>=i & t FTM[t]=FTM[u]": def ftmeqfact2 "?msd_fib At,u (t>=i & t FTM[t]=FTM[u]": def name n "\$func(i,n)": reg power2 msd_2 "0*10*": reg tmp20 msd_20 "[19][13]*": reg adjfib msd_fib msd_fib "[0,0]*[1,0][0,1][0,0]*": morphism h "0->01 1->12 2->20": promote T3 h: image F2 h F: morphism rud "0->01 1->02 2->31 3->32": promote RS1 rud: morphism codi "0->0 1->0 2->1 3->1": image RS2 codi RS1: eval test "An RS[n]=RS2[n]": combine Z dfa1 dfa2 dfa3: combine Z dfa1=3 dfa2=5: eval thuetest "Ei,n n>=1 & Aj j<=n => T[i+j] = T[i+j+n]": def in "i>=r & i<=s": def subs "j<=i & i+m<=j+n": def odd "Ei n=2*i+1": def even "Ei n=2*i": def factoreq "Ak k X[i+k]=X[j+k]": def pal "Ak k X[i+k] = X[(i+n)-(k+1)]": def occurs "m<=n & Ek k+m<=n & \$factoreq(i,j+k,m)": reg power2 msd_2 "0*10*": reg adjfib msd_fib msd_fib "[0,0]*[1,0][0,1][0,0]*": reg f3n1 msd_fib "0*1(001)*": eval fibidentitycheck "?msd_fib Ax,y,z (\$adjfib(z,x) & \$f3n1(y) & x<=y & y<=z) => (2*y+1=x+z)": def factoreq "At (t X[i+t]=X[j+t]": eval zeros "Ai,j \$feq(i,j,0)": eval induc "Ai,j,n (\$feq(i,j,n) & X[i+n]=X[j+n]) => \$feq(i,j,n+1)":