WORST_CASE(?,O(1)) * Step 1: Sum WORST_CASE(?,O(1)) + Considered Problem: - Strict TRS: f(f(x)) -> f(c(f(x))) f(f(x)) -> f(d(f(x))) g(c(x)) -> x g(c(0())) -> g(d(1())) g(c(1())) -> g(d(0())) g(d(x)) -> x - Signature: {f/1,g/1} / {0/0,1/0,c/1,d/1} - Obligation: innermost runtime complexity wrt. defined symbols {f,g} and constructors {0,1,c,d} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 2: DependencyPairs WORST_CASE(?,O(1)) + Considered Problem: - Strict TRS: f(f(x)) -> f(c(f(x))) f(f(x)) -> f(d(f(x))) g(c(x)) -> x g(c(0())) -> g(d(1())) g(c(1())) -> g(d(0())) g(d(x)) -> x - Signature: {f/1,g/1} / {0/0,1/0,c/1,d/1} - Obligation: innermost runtime complexity wrt. defined symbols {f,g} and constructors {0,1,c,d} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs f#(f(x)) -> c_1(f#(c(f(x))),f#(x)) f#(f(x)) -> c_2(f#(d(f(x))),f#(x)) g#(c(x)) -> c_3() g#(c(0())) -> c_4(g#(d(1()))) g#(c(1())) -> c_5(g#(d(0()))) g#(d(x)) -> c_6() Weak DPs and mark the set of starting terms. * Step 3: PredecessorEstimation WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: f#(f(x)) -> c_1(f#(c(f(x))),f#(x)) f#(f(x)) -> c_2(f#(d(f(x))),f#(x)) g#(c(x)) -> c_3() g#(c(0())) -> c_4(g#(d(1()))) g#(c(1())) -> c_5(g#(d(0()))) g#(d(x)) -> c_6() - Weak TRS: f(f(x)) -> f(c(f(x))) f(f(x)) -> f(d(f(x))) g(c(x)) -> x g(c(0())) -> g(d(1())) g(c(1())) -> g(d(0())) g(d(x)) -> x - Signature: {f/1,g/1,f#/1,g#/1} / {0/0,1/0,c/1,d/1,c_1/2,c_2/2,c_3/0,c_4/1,c_5/1,c_6/0} - Obligation: innermost runtime complexity wrt. defined symbols {f#,g#} and constructors {0,1,c,d} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {3,6} by application of Pre({3,6}) = {4,5}. Here rules are labelled as follows: 1: f#(f(x)) -> c_1(f#(c(f(x))),f#(x)) 2: f#(f(x)) -> c_2(f#(d(f(x))),f#(x)) 3: g#(c(x)) -> c_3() 4: g#(c(0())) -> c_4(g#(d(1()))) 5: g#(c(1())) -> c_5(g#(d(0()))) 6: g#(d(x)) -> c_6() * Step 4: PredecessorEstimation WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: f#(f(x)) -> c_1(f#(c(f(x))),f#(x)) f#(f(x)) -> c_2(f#(d(f(x))),f#(x)) g#(c(0())) -> c_4(g#(d(1()))) g#(c(1())) -> c_5(g#(d(0()))) - Weak DPs: g#(c(x)) -> c_3() g#(d(x)) -> c_6() - Weak TRS: f(f(x)) -> f(c(f(x))) f(f(x)) -> f(d(f(x))) g(c(x)) -> x g(c(0())) -> g(d(1())) g(c(1())) -> g(d(0())) g(d(x)) -> x - Signature: {f/1,g/1,f#/1,g#/1} / {0/0,1/0,c/1,d/1,c_1/2,c_2/2,c_3/0,c_4/1,c_5/1,c_6/0} - Obligation: innermost runtime complexity wrt. defined symbols {f#,g#} and constructors {0,1,c,d} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {3,4} by application of Pre({3,4}) = {}. Here rules are labelled as follows: 1: f#(f(x)) -> c_1(f#(c(f(x))),f#(x)) 2: f#(f(x)) -> c_2(f#(d(f(x))),f#(x)) 3: g#(c(0())) -> c_4(g#(d(1()))) 4: g#(c(1())) -> c_5(g#(d(0()))) 5: g#(c(x)) -> c_3() 6: g#(d(x)) -> c_6() * Step 5: RemoveWeakSuffixes WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: f#(f(x)) -> c_1(f#(c(f(x))),f#(x)) f#(f(x)) -> c_2(f#(d(f(x))),f#(x)) - Weak DPs: g#(c(x)) -> c_3() g#(c(0())) -> c_4(g#(d(1()))) g#(c(1())) -> c_5(g#(d(0()))) g#(d(x)) -> c_6() - Weak TRS: f(f(x)) -> f(c(f(x))) f(f(x)) -> f(d(f(x))) g(c(x)) -> x g(c(0())) -> g(d(1())) g(c(1())) -> g(d(0())) g(d(x)) -> x - Signature: {f/1,g/1,f#/1,g#/1} / {0/0,1/0,c/1,d/1,c_1/2,c_2/2,c_3/0,c_4/1,c_5/1,c_6/0} - Obligation: innermost runtime complexity wrt. defined symbols {f#,g#} and constructors {0,1,c,d} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:f#(f(x)) -> c_1(f#(c(f(x))),f#(x)) -->_2 f#(f(x)) -> c_2(f#(d(f(x))),f#(x)):2 -->_2 f#(f(x)) -> c_1(f#(c(f(x))),f#(x)):1 2:S:f#(f(x)) -> c_2(f#(d(f(x))),f#(x)) -->_2 f#(f(x)) -> c_2(f#(d(f(x))),f#(x)):2 -->_2 f#(f(x)) -> c_1(f#(c(f(x))),f#(x)):1 3:W:g#(c(x)) -> c_3() 4:W:g#(c(0())) -> c_4(g#(d(1()))) -->_1 g#(d(x)) -> c_6():6 5:W:g#(c(1())) -> c_5(g#(d(0()))) -->_1 g#(d(x)) -> c_6():6 6:W:g#(d(x)) -> c_6() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 5: g#(c(1())) -> c_5(g#(d(0()))) 4: g#(c(0())) -> c_4(g#(d(1()))) 6: g#(d(x)) -> c_6() 3: g#(c(x)) -> c_3() * Step 6: SimplifyRHS WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: f#(f(x)) -> c_1(f#(c(f(x))),f#(x)) f#(f(x)) -> c_2(f#(d(f(x))),f#(x)) - Weak TRS: f(f(x)) -> f(c(f(x))) f(f(x)) -> f(d(f(x))) g(c(x)) -> x g(c(0())) -> g(d(1())) g(c(1())) -> g(d(0())) g(d(x)) -> x - Signature: {f/1,g/1,f#/1,g#/1} / {0/0,1/0,c/1,d/1,c_1/2,c_2/2,c_3/0,c_4/1,c_5/1,c_6/0} - Obligation: innermost runtime complexity wrt. defined symbols {f#,g#} and constructors {0,1,c,d} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:f#(f(x)) -> c_1(f#(c(f(x))),f#(x)) -->_2 f#(f(x)) -> c_2(f#(d(f(x))),f#(x)):2 -->_2 f#(f(x)) -> c_1(f#(c(f(x))),f#(x)):1 2:S:f#(f(x)) -> c_2(f#(d(f(x))),f#(x)) -->_2 f#(f(x)) -> c_2(f#(d(f(x))),f#(x)):2 -->_2 f#(f(x)) -> c_1(f#(c(f(x))),f#(x)):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: f#(f(x)) -> c_1(f#(x)) f#(f(x)) -> c_2(f#(x)) * Step 7: UsableRules WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: f#(f(x)) -> c_1(f#(x)) f#(f(x)) -> c_2(f#(x)) - Weak TRS: f(f(x)) -> f(c(f(x))) f(f(x)) -> f(d(f(x))) g(c(x)) -> x g(c(0())) -> g(d(1())) g(c(1())) -> g(d(0())) g(d(x)) -> x - Signature: {f/1,g/1,f#/1,g#/1} / {0/0,1/0,c/1,d/1,c_1/1,c_2/1,c_3/0,c_4/1,c_5/1,c_6/0} - Obligation: innermost runtime complexity wrt. defined symbols {f#,g#} and constructors {0,1,c,d} + Applied Processor: UsableRules + Details: No rule is usable, rules are removed from the input problem. * Step 8: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Signature: {f/1,g/1,f#/1,g#/1} / {0/0,1/0,c/1,d/1,c_1/1,c_2/1,c_3/0,c_4/1,c_5/1,c_6/0} - Obligation: innermost runtime complexity wrt. defined symbols {f#,g#} and constructors {0,1,c,d} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(1))