MAYBE * Step 1: DependencyPairs MAYBE + Considered Problem: - Strict TRS: f(x,y) -> f(x,x) f(s(x),y) -> f(y,x) - Signature: {f/2} / {s/1} - Obligation: innermost runtime complexity wrt. defined symbols {f} and constructors {s} + Applied Processor: DependencyPairs {dpKind_ = WIDP} + Details: We add the following weak innermost dependency pairs: Strict DPs f#(x,y) -> c_1(f#(x,x)) f#(s(x),y) -> c_2(f#(y,x)) Weak DPs and mark the set of starting terms. * Step 2: UsableRules MAYBE + Considered Problem: - Strict DPs: f#(x,y) -> c_1(f#(x,x)) f#(s(x),y) -> c_2(f#(y,x)) - Strict TRS: f(x,y) -> f(x,x) f(s(x),y) -> f(y,x) - Signature: {f/2,f#/2} / {s/1,c_1/1,c_2/1} - Obligation: innermost runtime complexity wrt. defined symbols {f#} and constructors {s} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: f#(x,y) -> c_1(f#(x,x)) f#(s(x),y) -> c_2(f#(y,x)) * Step 3: Failure MAYBE + Considered Problem: - Strict DPs: f#(x,y) -> c_1(f#(x,x)) f#(s(x),y) -> c_2(f#(y,x)) - Signature: {f/2,f#/2} / {s/1,c_1/1,c_2/1} - Obligation: innermost runtime complexity wrt. defined symbols {f#} and constructors {s} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE