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