YES(?,ELEMENTARY) 'epo* (timeout of 60.0 seconds)' -------------------------------- Answer: YES(?,ELEMENTARY) Input Problem: innermost runtime-complexity with respect to Rules: { norm(nil()) -> 0() , norm(g(x, y)) -> s(norm(x)) , f(x, nil()) -> g(nil(), x) , f(x, g(y, z)) -> g(f(x, y), z) , rem(nil(), y) -> nil() , rem(g(x, y), 0()) -> g(x, y) , rem(g(x, y), s(z)) -> rem(x, z)} Proof Output: Strict Rules in Predicative Notation: { norm(nil();) -> 0() , norm(g(; x, y);) -> s(; norm(x;)) , f(nil(); x) -> g(; nil(), x) , f(g(; y, z); x) -> g(; f(y; x), z) , rem(nil(); y) -> nil() , rem(g(; x, y); 0()) -> g(; x, y) , rem(g(; x, y); s(; z)) -> rem(x; z)} Safe Mapping: safe(norm) = {}, safe(nil) = {}, safe(0) = {}, safe(g) = {1, 2}, safe(s) = {1}, safe(f) = {1}, safe(rem) = {2} Argument Permutation: mu(norm) = [1], mu(f) = [2, 1], mu(rem) = [2, 1] Precedence: rem ~ rem, f > rem, f ~ f, f > norm, norm > rem, norm ~ norm