Moving up and down between reflection levels

The functions provided by Core Maude for moving up and down reflection levels (see Section 11.4.1) are not very useful in Full Maude. Although they are available as part of the module META-LEVEL, they take as one of their arguments the name of a module entered into Core Maude. Since the databases of modules are different, these functions work in Full Maude only for Core Maude predefined modules. Full Maude provides its own functions upTerm and upModule for moving, respectively, terms and modules up reflection levels, and an additional down command which allows moving terms down reflection levels.

Let us consider the following module for the examples in the coming sections.

 (fmod NAT-PLUS is
    sort Nat .
    op 0 : -> Nat .
    op s_ : Nat -> Nat .
    op _+_ : Nat Nat -> Nat [assoc comm id: 0] .
    vars N M : Nat .
    eq s N + s M = s s (N + M) .
  endfm)

In what follows we will use the notation $\overline{t}$ and $\overline{M}$ to refer to the metarepresentations of a term $t$ and a module $M$, respectively. For example, we will write the metarepresentation of 0 + s 0 as $\overline{\texttt{0 + s 0}}$ instead of

  '_+_['0.Nat, 's_['0.Nat]]