MAYBE * Step 1: DependencyPairs MAYBE + Considered Problem: - Strict TRS: f(c(s(x),y)) -> g(c(x,y)) f(s(x)) -> f(id_inc(c(x,x))) g(c(x,x)) -> f(x) g(c(x,s(y))) -> g(c(y,x)) g(c(s(x),y)) -> g(c(y,x)) id_inc(0()) -> 0() id_inc(0()) -> s(0()) id_inc(c(x,y)) -> c(id_inc(x),id_inc(y)) id_inc(s(x)) -> s(id_inc(x)) - Signature: {f/1,g/1,id_inc/1} / {0/0,c/2,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {f,g,id_inc} and constructors {0,c,s} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs f#(c(s(x),y)) -> c_1(g#(c(x,y))) f#(s(x)) -> c_2(f#(id_inc(c(x,x))),id_inc#(c(x,x))) g#(c(x,x)) -> c_3(f#(x)) g#(c(x,s(y))) -> c_4(g#(c(y,x))) g#(c(s(x),y)) -> c_5(g#(c(y,x))) id_inc#(0()) -> c_6() id_inc#(0()) -> c_7() id_inc#(c(x,y)) -> c_8(id_inc#(x),id_inc#(y)) id_inc#(s(x)) -> c_9(id_inc#(x)) Weak DPs and mark the set of starting terms. * Step 2: UsableRules MAYBE + Considered Problem: - Strict DPs: f#(c(s(x),y)) -> c_1(g#(c(x,y))) f#(s(x)) -> c_2(f#(id_inc(c(x,x))),id_inc#(c(x,x))) g#(c(x,x)) -> c_3(f#(x)) g#(c(x,s(y))) -> c_4(g#(c(y,x))) g#(c(s(x),y)) -> c_5(g#(c(y,x))) id_inc#(0()) -> c_6() id_inc#(0()) -> c_7() id_inc#(c(x,y)) -> c_8(id_inc#(x),id_inc#(y)) id_inc#(s(x)) -> c_9(id_inc#(x)) - Weak TRS: f(c(s(x),y)) -> g(c(x,y)) f(s(x)) -> f(id_inc(c(x,x))) g(c(x,x)) -> f(x) g(c(x,s(y))) -> g(c(y,x)) g(c(s(x),y)) -> g(c(y,x)) id_inc(0()) -> 0() id_inc(0()) -> s(0()) id_inc(c(x,y)) -> c(id_inc(x),id_inc(y)) id_inc(s(x)) -> s(id_inc(x)) - Signature: {f/1,g/1,id_inc/1,f#/1,g#/1,id_inc#/1} / {0/0,c/2,s/1,c_1/1,c_2/2,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/2,c_9/1} - Obligation: innermost runtime complexity wrt. defined symbols {f#,g#,id_inc#} and constructors {0,c,s} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: id_inc(0()) -> 0() id_inc(0()) -> s(0()) id_inc(c(x,y)) -> c(id_inc(x),id_inc(y)) id_inc(s(x)) -> s(id_inc(x)) f#(c(s(x),y)) -> c_1(g#(c(x,y))) f#(s(x)) -> c_2(f#(id_inc(c(x,x))),id_inc#(c(x,x))) g#(c(x,x)) -> c_3(f#(x)) g#(c(x,s(y))) -> c_4(g#(c(y,x))) g#(c(s(x),y)) -> c_5(g#(c(y,x))) id_inc#(0()) -> c_6() id_inc#(0()) -> c_7() id_inc#(c(x,y)) -> c_8(id_inc#(x),id_inc#(y)) id_inc#(s(x)) -> c_9(id_inc#(x)) * Step 3: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: f#(c(s(x),y)) -> c_1(g#(c(x,y))) f#(s(x)) -> c_2(f#(id_inc(c(x,x))),id_inc#(c(x,x))) g#(c(x,x)) -> c_3(f#(x)) g#(c(x,s(y))) -> c_4(g#(c(y,x))) g#(c(s(x),y)) -> c_5(g#(c(y,x))) id_inc#(0()) -> c_6() id_inc#(0()) -> c_7() id_inc#(c(x,y)) -> c_8(id_inc#(x),id_inc#(y)) id_inc#(s(x)) -> c_9(id_inc#(x)) - Weak TRS: id_inc(0()) -> 0() id_inc(0()) -> s(0()) id_inc(c(x,y)) -> c(id_inc(x),id_inc(y)) id_inc(s(x)) -> s(id_inc(x)) - Signature: {f/1,g/1,id_inc/1,f#/1,g#/1,id_inc#/1} / {0/0,c/2,s/1,c_1/1,c_2/2,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/2,c_9/1} - Obligation: innermost runtime complexity wrt. defined symbols {f#,g#,id_inc#} and constructors {0,c,s} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {6,7} by application of Pre({6,7}) = {8,9}. Here rules are labelled as follows: 1: f#(c(s(x),y)) -> c_1(g#(c(x,y))) 2: f#(s(x)) -> c_2(f#(id_inc(c(x,x))),id_inc#(c(x,x))) 3: g#(c(x,x)) -> c_3(f#(x)) 4: g#(c(x,s(y))) -> c_4(g#(c(y,x))) 5: g#(c(s(x),y)) -> c_5(g#(c(y,x))) 6: id_inc#(0()) -> c_6() 7: id_inc#(0()) -> c_7() 8: id_inc#(c(x,y)) -> c_8(id_inc#(x),id_inc#(y)) 9: id_inc#(s(x)) -> c_9(id_inc#(x)) * Step 4: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: f#(c(s(x),y)) -> c_1(g#(c(x,y))) f#(s(x)) -> c_2(f#(id_inc(c(x,x))),id_inc#(c(x,x))) g#(c(x,x)) -> c_3(f#(x)) g#(c(x,s(y))) -> c_4(g#(c(y,x))) g#(c(s(x),y)) -> c_5(g#(c(y,x))) id_inc#(c(x,y)) -> c_8(id_inc#(x),id_inc#(y)) id_inc#(s(x)) -> c_9(id_inc#(x)) - Weak DPs: id_inc#(0()) -> c_6() id_inc#(0()) -> c_7() - Weak TRS: id_inc(0()) -> 0() id_inc(0()) -> s(0()) id_inc(c(x,y)) -> c(id_inc(x),id_inc(y)) id_inc(s(x)) -> s(id_inc(x)) - Signature: {f/1,g/1,id_inc/1,f#/1,g#/1,id_inc#/1} / {0/0,c/2,s/1,c_1/1,c_2/2,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/2,c_9/1} - Obligation: innermost runtime complexity wrt. defined symbols {f#,g#,id_inc#} and constructors {0,c,s} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:f#(c(s(x),y)) -> c_1(g#(c(x,y))) -->_1 g#(c(s(x),y)) -> c_5(g#(c(y,x))):5 -->_1 g#(c(x,s(y))) -> c_4(g#(c(y,x))):4 -->_1 g#(c(x,x)) -> c_3(f#(x)):3 2:S:f#(s(x)) -> c_2(f#(id_inc(c(x,x))),id_inc#(c(x,x))) -->_2 id_inc#(c(x,y)) -> c_8(id_inc#(x),id_inc#(y)):6 -->_1 f#(s(x)) -> c_2(f#(id_inc(c(x,x))),id_inc#(c(x,x))):2 -->_1 f#(c(s(x),y)) -> c_1(g#(c(x,y))):1 3:S:g#(c(x,x)) -> c_3(f#(x)) -->_1 f#(s(x)) -> c_2(f#(id_inc(c(x,x))),id_inc#(c(x,x))):2 -->_1 f#(c(s(x),y)) -> c_1(g#(c(x,y))):1 4:S:g#(c(x,s(y))) -> c_4(g#(c(y,x))) -->_1 g#(c(s(x),y)) -> c_5(g#(c(y,x))):5 -->_1 g#(c(x,s(y))) -> c_4(g#(c(y,x))):4 -->_1 g#(c(x,x)) -> c_3(f#(x)):3 5:S:g#(c(s(x),y)) -> c_5(g#(c(y,x))) -->_1 g#(c(s(x),y)) -> c_5(g#(c(y,x))):5 -->_1 g#(c(x,s(y))) -> c_4(g#(c(y,x))):4 -->_1 g#(c(x,x)) -> c_3(f#(x)):3 6:S:id_inc#(c(x,y)) -> c_8(id_inc#(x),id_inc#(y)) -->_2 id_inc#(s(x)) -> c_9(id_inc#(x)):7 -->_1 id_inc#(s(x)) -> c_9(id_inc#(x)):7 -->_2 id_inc#(0()) -> c_7():9 -->_1 id_inc#(0()) -> c_7():9 -->_2 id_inc#(0()) -> c_6():8 -->_1 id_inc#(0()) -> c_6():8 -->_2 id_inc#(c(x,y)) -> c_8(id_inc#(x),id_inc#(y)):6 -->_1 id_inc#(c(x,y)) -> c_8(id_inc#(x),id_inc#(y)):6 7:S:id_inc#(s(x)) -> c_9(id_inc#(x)) -->_1 id_inc#(0()) -> c_7():9 -->_1 id_inc#(0()) -> c_6():8 -->_1 id_inc#(s(x)) -> c_9(id_inc#(x)):7 -->_1 id_inc#(c(x,y)) -> c_8(id_inc#(x),id_inc#(y)):6 8:W:id_inc#(0()) -> c_6() 9:W:id_inc#(0()) -> c_7() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 8: id_inc#(0()) -> c_6() 9: id_inc#(0()) -> c_7() * Step 5: Failure MAYBE + Considered Problem: - Strict DPs: f#(c(s(x),y)) -> c_1(g#(c(x,y))) f#(s(x)) -> c_2(f#(id_inc(c(x,x))),id_inc#(c(x,x))) g#(c(x,x)) -> c_3(f#(x)) g#(c(x,s(y))) -> c_4(g#(c(y,x))) g#(c(s(x),y)) -> c_5(g#(c(y,x))) id_inc#(c(x,y)) -> c_8(id_inc#(x),id_inc#(y)) id_inc#(s(x)) -> c_9(id_inc#(x)) - Weak TRS: id_inc(0()) -> 0() id_inc(0()) -> s(0()) id_inc(c(x,y)) -> c(id_inc(x),id_inc(y)) id_inc(s(x)) -> s(id_inc(x)) - Signature: {f/1,g/1,id_inc/1,f#/1,g#/1,id_inc#/1} / {0/0,c/2,s/1,c_1/1,c_2/2,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/2,c_9/1} - Obligation: innermost runtime complexity wrt. defined symbols {f#,g#,id_inc#} and constructors {0,c,s} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE