2The predefined module LOOP-MODE described in Section 13.1 is not supported in Full Maude.