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