(GOAL COMPLEXITY)
(STARTTERM CONSTRUCTOR-BASED)
(STRATEGY INNERMOST)
(STRATEGY
    INNERMOST)

(VAR
    x)
(DATATYPES
    A = µX.< free(X), serve >)
(SIGNATURES
    top :: [A] -> A
    new :: [A] -> A
    old :: [A] -> A
    check :: [A] -> A)
(RULES
    top(free(x)) ->
      top(check(new(x)))
    new(free(x)) -> free(new(x))
    old(free(x)) -> free(old(x))
    new(serve()) -> free(serve())
    old(serve()) -> free(serve())
    check(free(x)) -> free(check(x))
    check(new(x)) -> new(check(x))
    check(old(x)) -> old(check(x))
    check(old(x)) -> old(x))