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