Maude provides a built-in mechanism called the iter (short for iterated operator) theory whose goal is to permit the efficient input, output, and manipulation of very large stacks of a unary operator.
Unary operators may be declared to belong to the iter theory by including iter in their attributes. After declaring
sort Foo . op f : Foo -> Foo [iter] .
the term f(f(f(X:Foo))) can be input as f^3(X:Foo) and will be output in that form. A term such as f^1234567890123456789(X:Foo) is too large to be input, output or manipulated in regular notation, but can be input and output in this compact notation and certain (built-in) manipulations may thus be made efficient.
The precise form of the compact iter theory notation is the prefix name of the
operator followed by ^[1-9][0-9]* (in Lex regular expression notation)
with no intervening white space. Note that f^0123(X:Foo) is not
acceptable. Of course, regular notation (and mixfix notation if appropriate)
can still be used.
Membership axioms may also interact in undesirable ways with operators declared with the iter attribute; see Section 13.2.9 for details.