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: Decompose 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: Decompose {onSelection = all cycle independent sub-graph, withBound = RelativeAdd} + Details: We analyse the complexity of following sub-problems (R) and (S). Problem (S) is obtained from the input problem by shifting strict rules from (R) into the weak component. Problem (R) - Strict DPs: -#(s(x),s(y)) -> c_3(-#(x,y)) - Weak DPs: 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} Problem (S) - Strict DPs: 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: -#(s(x),s(y)) -> c_3(-#(x,y)) - 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} ** Step 4.a:1: Failure MAYBE + Considered Problem: - Strict DPs: -#(s(x),s(y)) -> c_3(-#(x,y)) - Weak DPs: 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. ** Step 4.b:1: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: 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: -#(s(x),s(y)) -> c_3(-#(x,y)) - 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:f#(s(x)) -> c_5(-#(s(x),g(f(x))),g#(f(x)),f#(x)) -->_1 -#(s(x),s(y)) -> c_3(-#(x,y)):3 -->_2 g#(s(x)) -> c_7(-#(s(x),f(g(x))),f#(g(x)),g#(x)):2 -->_3 f#(s(x)) -> c_5(-#(s(x),g(f(x))),g#(f(x)),f#(x)):1 2:S:g#(s(x)) -> c_7(-#(s(x),f(g(x))),f#(g(x)),g#(x)) -->_1 -#(s(x),s(y)) -> c_3(-#(x,y)):3 -->_3 g#(s(x)) -> c_7(-#(s(x),f(g(x))),f#(g(x)),g#(x)):2 -->_2 f#(s(x)) -> c_5(-#(s(x),g(f(x))),g#(f(x)),f#(x)):1 3:W:-#(s(x),s(y)) -> c_3(-#(x,y)) -->_1 -#(s(x),s(y)) -> c_3(-#(x,y)):3 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 3: -#(s(x),s(y)) -> c_3(-#(x,y)) ** Step 4.b:2: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: 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: SimplifyRHS + Details: Consider the dependency graph 1: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)):2 -->_3 f#(s(x)) -> c_5(-#(s(x),g(f(x))),g#(f(x)),f#(x)):1 2:S:g#(s(x)) -> c_7(-#(s(x),f(g(x))),f#(g(x)),g#(x)) -->_3 g#(s(x)) -> c_7(-#(s(x),f(g(x))),f#(g(x)),g#(x)):2 -->_2 f#(s(x)) -> c_5(-#(s(x),g(f(x))),g#(f(x)),f#(x)):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: f#(s(x)) -> c_5(g#(f(x)),f#(x)) g#(s(x)) -> c_7(f#(g(x)),g#(x)) ** Step 4.b:3: Failure MAYBE + Considered Problem: - Strict DPs: f#(s(x)) -> c_5(g#(f(x)),f#(x)) g#(s(x)) -> c_7(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/2,c_6/0,c_7/2} - Obligation: innermost runtime complexity wrt. defined symbols {-#,f#,g#} and constructors {0,s} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE