MAYBE * Step 1: DependencyPairs MAYBE + Considered Problem: - Strict TRS: -(x,0()) -> x -(0(),s(y)) -> 0() -(s(x),s(y)) -> -(x,y) f(0()) -> 0() f(s(x)) -> -(s(x),g(f(x))) g(0()) -> s(0()) g(s(x)) -> -(s(x),f(g(x))) - Signature: {-/2,f/1,g/1} / {0/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {-,f,g} and constructors {0,s} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs -#(x,0()) -> c_1() -#(0(),s(y)) -> c_2() -#(s(x),s(y)) -> c_3(-#(x,y)) f#(0()) -> c_4() f#(s(x)) -> c_5(-#(s(x),g(f(x))),g#(f(x)),f#(x)) g#(0()) -> c_6() g#(s(x)) -> c_7(-#(s(x),f(g(x))),f#(g(x)),g#(x)) Weak DPs and mark the set of starting terms. * Step 2: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: -#(x,0()) -> c_1() -#(0(),s(y)) -> c_2() -#(s(x),s(y)) -> c_3(-#(x,y)) f#(0()) -> c_4() f#(s(x)) -> c_5(-#(s(x),g(f(x))),g#(f(x)),f#(x)) g#(0()) -> c_6() g#(s(x)) -> c_7(-#(s(x),f(g(x))),f#(g(x)),g#(x)) - Weak TRS: -(x,0()) -> x -(0(),s(y)) -> 0() -(s(x),s(y)) -> -(x,y) f(0()) -> 0() f(s(x)) -> -(s(x),g(f(x))) g(0()) -> s(0()) g(s(x)) -> -(s(x),f(g(x))) - Signature: {-/2,f/1,g/1,-#/2,f#/1,g#/1} / {0/0,s/1,c_1/0,c_2/0,c_3/1,c_4/0,c_5/3,c_6/0,c_7/3} - Obligation: innermost runtime complexity wrt. defined symbols {-#,f#,g#} and constructors {0,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}. Here rules are labelled as follows: 1: -#(x,0()) -> c_1() 2: -#(0(),s(y)) -> c_2() 3: -#(s(x),s(y)) -> c_3(-#(x,y)) 4: f#(0()) -> c_4() 5: f#(s(x)) -> c_5(-#(s(x),g(f(x))),g#(f(x)),f#(x)) 6: g#(0()) -> c_6() 7: g#(s(x)) -> c_7(-#(s(x),f(g(x))),f#(g(x)),g#(x)) * Step 3: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: -#(s(x),s(y)) -> c_3(-#(x,y)) f#(s(x)) -> c_5(-#(s(x),g(f(x))),g#(f(x)),f#(x)) g#(s(x)) -> c_7(-#(s(x),f(g(x))),f#(g(x)),g#(x)) - Weak DPs: -#(x,0()) -> c_1() -#(0(),s(y)) -> c_2() f#(0()) -> c_4() g#(0()) -> c_6() - Weak TRS: -(x,0()) -> x -(0(),s(y)) -> 0() -(s(x),s(y)) -> -(x,y) f(0()) -> 0() f(s(x)) -> -(s(x),g(f(x))) g(0()) -> s(0()) g(s(x)) -> -(s(x),f(g(x))) - Signature: {-/2,f/1,g/1,-#/2,f#/1,g#/1} / {0/0,s/1,c_1/0,c_2/0,c_3/1,c_4/0,c_5/3,c_6/0,c_7/3} - Obligation: innermost runtime complexity wrt. defined symbols {-#,f#,g#} and constructors {0,s} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:-#(s(x),s(y)) -> c_3(-#(x,y)) -->_1 -#(0(),s(y)) -> c_2():5 -->_1 -#(x,0()) -> c_1():4 -->_1 -#(s(x),s(y)) -> c_3(-#(x,y)):1 2:S:f#(s(x)) -> c_5(-#(s(x),g(f(x))),g#(f(x)),f#(x)) -->_2 g#(s(x)) -> c_7(-#(s(x),f(g(x))),f#(g(x)),g#(x)):3 -->_2 g#(0()) -> c_6():7 -->_3 f#(0()) -> c_4():6 -->_1 -#(x,0()) -> c_1():4 -->_3 f#(s(x)) -> c_5(-#(s(x),g(f(x))),g#(f(x)),f#(x)):2 -->_1 -#(s(x),s(y)) -> c_3(-#(x,y)):1 3:S:g#(s(x)) -> c_7(-#(s(x),f(g(x))),f#(g(x)),g#(x)) -->_3 g#(0()) -> c_6():7 -->_2 f#(0()) -> c_4():6 -->_1 -#(x,0()) -> c_1():4 -->_3 g#(s(x)) -> c_7(-#(s(x),f(g(x))),f#(g(x)),g#(x)):3 -->_2 f#(s(x)) -> c_5(-#(s(x),g(f(x))),g#(f(x)),f#(x)):2 -->_1 -#(s(x),s(y)) -> c_3(-#(x,y)):1 4:W:-#(x,0()) -> c_1() 5:W:-#(0(),s(y)) -> c_2() 6:W:f#(0()) -> c_4() 7:W:g#(0()) -> c_6() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 6: f#(0()) -> c_4() 7: g#(0()) -> c_6() 4: -#(x,0()) -> c_1() 5: -#(0(),s(y)) -> c_2() * Step 4: Failure MAYBE + Considered Problem: - Strict DPs: -#(s(x),s(y)) -> c_3(-#(x,y)) f#(s(x)) -> c_5(-#(s(x),g(f(x))),g#(f(x)),f#(x)) g#(s(x)) -> c_7(-#(s(x),f(g(x))),f#(g(x)),g#(x)) - Weak TRS: -(x,0()) -> x -(0(),s(y)) -> 0() -(s(x),s(y)) -> -(x,y) f(0()) -> 0() f(s(x)) -> -(s(x),g(f(x))) g(0()) -> s(0()) g(s(x)) -> -(s(x),f(g(x))) - Signature: {-/2,f/1,g/1,-#/2,f#/1,g#/1} / {0/0,s/1,c_1/0,c_2/0,c_3/1,c_4/0,c_5/3,c_6/0,c_7/3} - Obligation: innermost runtime complexity wrt. defined symbols {-#,f#,g#} and constructors {0,s} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE