MAYBE * Step 1: DependencyPairs MAYBE + Considered Problem: - Strict TRS: addchild(node(y,ys),node(n,xs)) -> node(y,cons(node(n,xs),ys)) f(node(s(n),xs)) -> f(addchild(select(xs),node(n,xs))) select(cons(ap,xs)) -> ap select(cons(ap,xs)) -> select(xs) - Signature: {addchild/2,f/1,select/1} / {cons/2,node/2,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {addchild,f,select} and constructors {cons,node,s} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs addchild#(node(y,ys),node(n,xs)) -> c_1() f#(node(s(n),xs)) -> c_2(f#(addchild(select(xs),node(n,xs))),addchild#(select(xs),node(n,xs)),select#(xs)) select#(cons(ap,xs)) -> c_3() select#(cons(ap,xs)) -> c_4(select#(xs)) Weak DPs and mark the set of starting terms. * Step 2: UsableRules MAYBE + Considered Problem: - Strict DPs: addchild#(node(y,ys),node(n,xs)) -> c_1() f#(node(s(n),xs)) -> c_2(f#(addchild(select(xs),node(n,xs))),addchild#(select(xs),node(n,xs)),select#(xs)) select#(cons(ap,xs)) -> c_3() select#(cons(ap,xs)) -> c_4(select#(xs)) - Weak TRS: addchild(node(y,ys),node(n,xs)) -> node(y,cons(node(n,xs),ys)) f(node(s(n),xs)) -> f(addchild(select(xs),node(n,xs))) select(cons(ap,xs)) -> ap select(cons(ap,xs)) -> select(xs) - Signature: {addchild/2,f/1,select/1,addchild#/2,f#/1,select#/1} / {cons/2,node/2,s/1,c_1/0,c_2/3,c_3/0,c_4/1} - Obligation: innermost runtime complexity wrt. defined symbols {addchild#,f#,select#} and constructors {cons,node,s} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: addchild(node(y,ys),node(n,xs)) -> node(y,cons(node(n,xs),ys)) select(cons(ap,xs)) -> ap select(cons(ap,xs)) -> select(xs) addchild#(node(y,ys),node(n,xs)) -> c_1() f#(node(s(n),xs)) -> c_2(f#(addchild(select(xs),node(n,xs))),addchild#(select(xs),node(n,xs)),select#(xs)) select#(cons(ap,xs)) -> c_3() select#(cons(ap,xs)) -> c_4(select#(xs)) * Step 3: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: addchild#(node(y,ys),node(n,xs)) -> c_1() f#(node(s(n),xs)) -> c_2(f#(addchild(select(xs),node(n,xs))),addchild#(select(xs),node(n,xs)),select#(xs)) select#(cons(ap,xs)) -> c_3() select#(cons(ap,xs)) -> c_4(select#(xs)) - Weak TRS: addchild(node(y,ys),node(n,xs)) -> node(y,cons(node(n,xs),ys)) select(cons(ap,xs)) -> ap select(cons(ap,xs)) -> select(xs) - Signature: {addchild/2,f/1,select/1,addchild#/2,f#/1,select#/1} / {cons/2,node/2,s/1,c_1/0,c_2/3,c_3/0,c_4/1} - Obligation: innermost runtime complexity wrt. defined symbols {addchild#,f#,select#} and constructors {cons,node,s} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,3} by application of Pre({1,3}) = {2,4}. Here rules are labelled as follows: 1: addchild#(node(y,ys),node(n,xs)) -> c_1() 2: f#(node(s(n),xs)) -> c_2(f#(addchild(select(xs),node(n,xs))) ,addchild#(select(xs),node(n,xs)) ,select#(xs)) 3: select#(cons(ap,xs)) -> c_3() 4: select#(cons(ap,xs)) -> c_4(select#(xs)) * Step 4: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: f#(node(s(n),xs)) -> c_2(f#(addchild(select(xs),node(n,xs))),addchild#(select(xs),node(n,xs)),select#(xs)) select#(cons(ap,xs)) -> c_4(select#(xs)) - Weak DPs: addchild#(node(y,ys),node(n,xs)) -> c_1() select#(cons(ap,xs)) -> c_3() - Weak TRS: addchild(node(y,ys),node(n,xs)) -> node(y,cons(node(n,xs),ys)) select(cons(ap,xs)) -> ap select(cons(ap,xs)) -> select(xs) - Signature: {addchild/2,f/1,select/1,addchild#/2,f#/1,select#/1} / {cons/2,node/2,s/1,c_1/0,c_2/3,c_3/0,c_4/1} - Obligation: innermost runtime complexity wrt. defined symbols {addchild#,f#,select#} and constructors {cons,node,s} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:f#(node(s(n),xs)) -> c_2(f#(addchild(select(xs),node(n,xs))) ,addchild#(select(xs),node(n,xs)) ,select#(xs)) -->_3 select#(cons(ap,xs)) -> c_4(select#(xs)):2 -->_3 select#(cons(ap,xs)) -> c_3():4 -->_2 addchild#(node(y,ys),node(n,xs)) -> c_1():3 -->_1 f#(node(s(n),xs)) -> c_2(f#(addchild(select(xs),node(n,xs))) ,addchild#(select(xs),node(n,xs)) ,select#(xs)):1 2:S:select#(cons(ap,xs)) -> c_4(select#(xs)) -->_1 select#(cons(ap,xs)) -> c_3():4 -->_1 select#(cons(ap,xs)) -> c_4(select#(xs)):2 3:W:addchild#(node(y,ys),node(n,xs)) -> c_1() 4:W:select#(cons(ap,xs)) -> c_3() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 3: addchild#(node(y,ys),node(n,xs)) -> c_1() 4: select#(cons(ap,xs)) -> c_3() * Step 5: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: f#(node(s(n),xs)) -> c_2(f#(addchild(select(xs),node(n,xs))),addchild#(select(xs),node(n,xs)),select#(xs)) select#(cons(ap,xs)) -> c_4(select#(xs)) - Weak TRS: addchild(node(y,ys),node(n,xs)) -> node(y,cons(node(n,xs),ys)) select(cons(ap,xs)) -> ap select(cons(ap,xs)) -> select(xs) - Signature: {addchild/2,f/1,select/1,addchild#/2,f#/1,select#/1} / {cons/2,node/2,s/1,c_1/0,c_2/3,c_3/0,c_4/1} - Obligation: innermost runtime complexity wrt. defined symbols {addchild#,f#,select#} and constructors {cons,node,s} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:f#(node(s(n),xs)) -> c_2(f#(addchild(select(xs),node(n,xs))) ,addchild#(select(xs),node(n,xs)) ,select#(xs)) -->_3 select#(cons(ap,xs)) -> c_4(select#(xs)):2 -->_1 f#(node(s(n),xs)) -> c_2(f#(addchild(select(xs),node(n,xs))) ,addchild#(select(xs),node(n,xs)) ,select#(xs)):1 2:S:select#(cons(ap,xs)) -> c_4(select#(xs)) -->_1 select#(cons(ap,xs)) -> c_4(select#(xs)):2 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: f#(node(s(n),xs)) -> c_2(f#(addchild(select(xs),node(n,xs))),select#(xs)) * Step 6: Failure MAYBE + Considered Problem: - Strict DPs: f#(node(s(n),xs)) -> c_2(f#(addchild(select(xs),node(n,xs))),select#(xs)) select#(cons(ap,xs)) -> c_4(select#(xs)) - Weak TRS: addchild(node(y,ys),node(n,xs)) -> node(y,cons(node(n,xs),ys)) select(cons(ap,xs)) -> ap select(cons(ap,xs)) -> select(xs) - Signature: {addchild/2,f/1,select/1,addchild#/2,f#/1,select#/1} / {cons/2,node/2,s/1,c_1/0,c_2/2,c_3/0,c_4/1} - Obligation: innermost runtime complexity wrt. defined symbols {addchild#,f#,select#} and constructors {cons,node,s} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE