Long halting times [in symbolic systems]

Symbolic systems with rules of the form ℯ[x_][y_]  Nest[x, y, r]

ℯ[x_][y_]  Nest[x, y, r] always evolve to fixed points—though with initial conditions of size n this can take of order Nest[r^#&, 0, n]

✖

Nest[\!\(\*SuperscriptBox[\(r\),\(#\)]\)&,0,n] steps (see above). In general there will be symbolic systems where the number of steps to evolve to a fixed point grows arbitrarily rapidly with n (see page 1145), and indeed I suspect that there are even systems with quite simple rules where proving that a fixed point is always reached in a finite number of steps is beyond, for example, the axiom system for arithmetic (see page 1163).