Consider the following two functions on natural numbers: $$ F(x) = \left\{ \begin{array}{ll} 5 & \text{if}\ x \leq 7 \\ 1 & \text{if}\ 8 \leq x \end{array}\right. \qquad \text{and} \qquad G(x) = \left\{ \begin{array}{ll} 2 & \text{if}\ x \leq 4 \\ 7 & \text{if}\ 5 \leq x \end{array}\right. $$
The aim is to prove that $9 \leq G(F(x)) + G(x)$ for all natural numbers $x$.
The goal is easily discharged using the theorem of constants (i.e. by adding the variables of the goal to the body of the specification FG-FUN as fresh constants), case analysis, and reduction.
FG-FUN |- eq 9 <= G(F(X:Nat)) + G(X:Nat) = true ; See goal.maude for the full proof.