* 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: UsableRules 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: UsableRules + Details: We replace rewrite rules by usable rules: 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() * Step 4: Trivial WORST_CASE(?,O(1)) + Considered Problem: - Strict 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() - 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: Trivial + Details: Consider the dependency graph 1:S:g#(c(x)) -> c_3() 2:S:g#(c(0())) -> c_4(g#(d(1()))) -->_1 g#(d(x)) -> c_6():4 3:S:g#(c(1())) -> c_5(g#(d(0()))) -->_1 g#(d(x)) -> c_6():4 4:S:g#(d(x)) -> c_6() The dependency graph contains no loops, we remove all dependency pairs. * Step 5: 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/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: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(1))