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