MAYBE * Step 1: DependencyPairs MAYBE + Considered Problem: - Strict TRS: +(X,0()) -> X +(X,s(Y)) -> s(+(X,Y)) f(0(),s(0()),X) -> f(X,+(X,X),X) g(X,Y) -> X g(X,Y) -> Y - Signature: {+/2,f/3,g/2} / {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() +#(X,s(Y)) -> c_2(+#(X,Y)) f#(0(),s(0()),X) -> c_3(f#(X,+(X,X),X),+#(X,X)) g#(X,Y) -> c_4() g#(X,Y) -> c_5() Weak DPs and mark the set of starting terms. * Step 2: UsableRules MAYBE + Considered Problem: - Strict DPs: +#(X,0()) -> c_1() +#(X,s(Y)) -> c_2(+#(X,Y)) f#(0(),s(0()),X) -> c_3(f#(X,+(X,X),X),+#(X,X)) g#(X,Y) -> c_4() g#(X,Y) -> c_5() - Weak TRS: +(X,0()) -> X +(X,s(Y)) -> s(+(X,Y)) f(0(),s(0()),X) -> f(X,+(X,X),X) g(X,Y) -> X g(X,Y) -> Y - Signature: {+/2,f/3,g/2,+#/2,f#/3,g#/2} / {0/0,s/1,c_1/0,c_2/1,c_3/2,c_4/0,c_5/0} - Obligation: innermost runtime complexity wrt. defined symbols {+#,f#,g#} and constructors {0,s} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: +(X,0()) -> X +(X,s(Y)) -> s(+(X,Y)) +#(X,0()) -> c_1() +#(X,s(Y)) -> c_2(+#(X,Y)) f#(0(),s(0()),X) -> c_3(f#(X,+(X,X),X),+#(X,X)) g#(X,Y) -> c_4() g#(X,Y) -> c_5() * Step 3: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: +#(X,0()) -> c_1() +#(X,s(Y)) -> c_2(+#(X,Y)) f#(0(),s(0()),X) -> c_3(f#(X,+(X,X),X),+#(X,X)) g#(X,Y) -> c_4() g#(X,Y) -> c_5() - Weak TRS: +(X,0()) -> X +(X,s(Y)) -> s(+(X,Y)) - Signature: {+/2,f/3,g/2,+#/2,f#/3,g#/2} / {0/0,s/1,c_1/0,c_2/1,c_3/2,c_4/0,c_5/0} - 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,4,5} by application of Pre({1,4,5}) = {2,3}. Here rules are labelled as follows: 1: +#(X,0()) -> c_1() 2: +#(X,s(Y)) -> c_2(+#(X,Y)) 3: f#(0(),s(0()),X) -> c_3(f#(X,+(X,X),X),+#(X,X)) 4: g#(X,Y) -> c_4() 5: g#(X,Y) -> c_5() * Step 4: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: +#(X,s(Y)) -> c_2(+#(X,Y)) f#(0(),s(0()),X) -> c_3(f#(X,+(X,X),X),+#(X,X)) - Weak DPs: +#(X,0()) -> c_1() g#(X,Y) -> c_4() g#(X,Y) -> c_5() - Weak TRS: +(X,0()) -> X +(X,s(Y)) -> s(+(X,Y)) - Signature: {+/2,f/3,g/2,+#/2,f#/3,g#/2} / {0/0,s/1,c_1/0,c_2/1,c_3/2,c_4/0,c_5/0} - Obligation: innermost runtime complexity wrt. defined symbols {+#,f#,g#} and constructors {0,s} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:+#(X,s(Y)) -> c_2(+#(X,Y)) -->_1 +#(X,0()) -> c_1():3 -->_1 +#(X,s(Y)) -> c_2(+#(X,Y)):1 2:S:f#(0(),s(0()),X) -> c_3(f#(X,+(X,X),X),+#(X,X)) -->_2 +#(X,0()) -> c_1():3 -->_1 f#(0(),s(0()),X) -> c_3(f#(X,+(X,X),X),+#(X,X)):2 -->_2 +#(X,s(Y)) -> c_2(+#(X,Y)):1 3:W:+#(X,0()) -> c_1() 4:W:g#(X,Y) -> c_4() 5:W:g#(X,Y) -> c_5() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 5: g#(X,Y) -> c_5() 4: g#(X,Y) -> c_4() 3: +#(X,0()) -> c_1() * Step 5: Decompose MAYBE + Considered Problem: - Strict DPs: +#(X,s(Y)) -> c_2(+#(X,Y)) f#(0(),s(0()),X) -> c_3(f#(X,+(X,X),X),+#(X,X)) - Weak TRS: +(X,0()) -> X +(X,s(Y)) -> s(+(X,Y)) - Signature: {+/2,f/3,g/2,+#/2,f#/3,g#/2} / {0/0,s/1,c_1/0,c_2/1,c_3/2,c_4/0,c_5/0} - 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: +#(X,s(Y)) -> c_2(+#(X,Y)) - Weak DPs: f#(0(),s(0()),X) -> c_3(f#(X,+(X,X),X),+#(X,X)) - Weak TRS: +(X,0()) -> X +(X,s(Y)) -> s(+(X,Y)) - Signature: {+/2,f/3,g/2,+#/2,f#/3,g#/2} / {0/0,s/1,c_1/0,c_2/1,c_3/2,c_4/0,c_5/0} - Obligation: innermost runtime complexity wrt. defined symbols {+#,f#,g#} and constructors {0,s} Problem (S) - Strict DPs: f#(0(),s(0()),X) -> c_3(f#(X,+(X,X),X),+#(X,X)) - Weak DPs: +#(X,s(Y)) -> c_2(+#(X,Y)) - Weak TRS: +(X,0()) -> X +(X,s(Y)) -> s(+(X,Y)) - Signature: {+/2,f/3,g/2,+#/2,f#/3,g#/2} / {0/0,s/1,c_1/0,c_2/1,c_3/2,c_4/0,c_5/0} - Obligation: innermost runtime complexity wrt. defined symbols {+#,f#,g#} and constructors {0,s} ** Step 5.a:1: Failure MAYBE + Considered Problem: - Strict DPs: +#(X,s(Y)) -> c_2(+#(X,Y)) - Weak DPs: f#(0(),s(0()),X) -> c_3(f#(X,+(X,X),X),+#(X,X)) - Weak TRS: +(X,0()) -> X +(X,s(Y)) -> s(+(X,Y)) - Signature: {+/2,f/3,g/2,+#/2,f#/3,g#/2} / {0/0,s/1,c_1/0,c_2/1,c_3/2,c_4/0,c_5/0} - Obligation: innermost runtime complexity wrt. defined symbols {+#,f#,g#} and constructors {0,s} + Applied Processor: EmptyProcessor + Details: The problem is still open. ** Step 5.b:1: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: f#(0(),s(0()),X) -> c_3(f#(X,+(X,X),X),+#(X,X)) - Weak DPs: +#(X,s(Y)) -> c_2(+#(X,Y)) - Weak TRS: +(X,0()) -> X +(X,s(Y)) -> s(+(X,Y)) - Signature: {+/2,f/3,g/2,+#/2,f#/3,g#/2} / {0/0,s/1,c_1/0,c_2/1,c_3/2,c_4/0,c_5/0} - Obligation: innermost runtime complexity wrt. defined symbols {+#,f#,g#} and constructors {0,s} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:f#(0(),s(0()),X) -> c_3(f#(X,+(X,X),X),+#(X,X)) -->_2 +#(X,s(Y)) -> c_2(+#(X,Y)):2 -->_1 f#(0(),s(0()),X) -> c_3(f#(X,+(X,X),X),+#(X,X)):1 2:W:+#(X,s(Y)) -> c_2(+#(X,Y)) -->_1 +#(X,s(Y)) -> c_2(+#(X,Y)):2 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 2: +#(X,s(Y)) -> c_2(+#(X,Y)) ** Step 5.b:2: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: f#(0(),s(0()),X) -> c_3(f#(X,+(X,X),X),+#(X,X)) - Weak TRS: +(X,0()) -> X +(X,s(Y)) -> s(+(X,Y)) - Signature: {+/2,f/3,g/2,+#/2,f#/3,g#/2} / {0/0,s/1,c_1/0,c_2/1,c_3/2,c_4/0,c_5/0} - Obligation: innermost runtime complexity wrt. defined symbols {+#,f#,g#} and constructors {0,s} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:f#(0(),s(0()),X) -> c_3(f#(X,+(X,X),X),+#(X,X)) -->_1 f#(0(),s(0()),X) -> c_3(f#(X,+(X,X),X),+#(X,X)):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: f#(0(),s(0()),X) -> c_3(f#(X,+(X,X),X)) ** Step 5.b:3: Failure MAYBE + Considered Problem: - Strict DPs: f#(0(),s(0()),X) -> c_3(f#(X,+(X,X),X)) - Weak TRS: +(X,0()) -> X +(X,s(Y)) -> s(+(X,Y)) - Signature: {+/2,f/3,g/2,+#/2,f#/3,g#/2} / {0/0,s/1,c_1/0,c_2/1,c_3/1,c_4/0,c_5/0} - Obligation: innermost runtime complexity wrt. defined symbols {+#,f#,g#} and constructors {0,s} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE