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