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<n => F[i+t]=F[j+t]":

def ftmeqfact1 "?msd_fib At Au (t>=i & t<i+n & i+u=t+j)
   => FTM[t]=FTM[u]":

def ftmeqfact2 "?msd_fib At,u (t>=i & t<i+n & i+u=t+j)
   => 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<n => X[i+k]=X[j+k]":
def pal "Ak k<n => 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<n) => 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)":