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