* Step 1: Sum WORST_CASE(?,O(1)) + Considered Problem: - Strict TRS: a__c() -> a__f(g(c())) a__c() -> c() a__f(X) -> f(X) a__f(g(X)) -> g(X) mark(c()) -> a__c() mark(f(X)) -> a__f(X) mark(g(X)) -> g(X) - Signature: {a__c/0,a__f/1,mark/1} / {c/0,f/1,g/1} - Obligation: innermost runtime complexity wrt. defined symbols {a__c,a__f,mark} and constructors {c,f,g} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 2: DependencyPairs WORST_CASE(?,O(1)) + Considered Problem: - Strict TRS: a__c() -> a__f(g(c())) a__c() -> c() a__f(X) -> f(X) a__f(g(X)) -> g(X) mark(c()) -> a__c() mark(f(X)) -> a__f(X) mark(g(X)) -> g(X) - Signature: {a__c/0,a__f/1,mark/1} / {c/0,f/1,g/1} - Obligation: innermost runtime complexity wrt. defined symbols {a__c,a__f,mark} and constructors {c,f,g} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs a__c#() -> c_1(a__f#(g(c()))) a__c#() -> c_2() a__f#(X) -> c_3() a__f#(g(X)) -> c_4() mark#(c()) -> c_5(a__c#()) mark#(f(X)) -> c_6(a__f#(X)) mark#(g(X)) -> c_7() Weak DPs and mark the set of starting terms. * Step 3: UsableRules WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: a__c#() -> c_1(a__f#(g(c()))) a__c#() -> c_2() a__f#(X) -> c_3() a__f#(g(X)) -> c_4() mark#(c()) -> c_5(a__c#()) mark#(f(X)) -> c_6(a__f#(X)) mark#(g(X)) -> c_7() - Weak TRS: a__c() -> a__f(g(c())) a__c() -> c() a__f(X) -> f(X) a__f(g(X)) -> g(X) mark(c()) -> a__c() mark(f(X)) -> a__f(X) mark(g(X)) -> g(X) - Signature: {a__c/0,a__f/1,mark/1,a__c#/0,a__f#/1,mark#/1} / {c/0,f/1,g/1,c_1/1,c_2/0,c_3/0,c_4/0,c_5/1,c_6/1,c_7/0} - Obligation: innermost runtime complexity wrt. defined symbols {a__c#,a__f#,mark#} and constructors {c,f,g} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: a__c#() -> c_1(a__f#(g(c()))) a__c#() -> c_2() a__f#(X) -> c_3() a__f#(g(X)) -> c_4() mark#(c()) -> c_5(a__c#()) mark#(f(X)) -> c_6(a__f#(X)) mark#(g(X)) -> c_7() * Step 4: Trivial WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: a__c#() -> c_1(a__f#(g(c()))) a__c#() -> c_2() a__f#(X) -> c_3() a__f#(g(X)) -> c_4() mark#(c()) -> c_5(a__c#()) mark#(f(X)) -> c_6(a__f#(X)) mark#(g(X)) -> c_7() - Signature: {a__c/0,a__f/1,mark/1,a__c#/0,a__f#/1,mark#/1} / {c/0,f/1,g/1,c_1/1,c_2/0,c_3/0,c_4/0,c_5/1,c_6/1,c_7/0} - Obligation: innermost runtime complexity wrt. defined symbols {a__c#,a__f#,mark#} and constructors {c,f,g} + Applied Processor: Trivial + Details: Consider the dependency graph 1:S:a__c#() -> c_1(a__f#(g(c()))) -->_1 a__f#(g(X)) -> c_4():4 -->_1 a__f#(X) -> c_3():3 2:S:a__c#() -> c_2() 3:S:a__f#(X) -> c_3() 4:S:a__f#(g(X)) -> c_4() 5:S:mark#(c()) -> c_5(a__c#()) -->_1 a__c#() -> c_2():2 -->_1 a__c#() -> c_1(a__f#(g(c()))):1 6:S:mark#(f(X)) -> c_6(a__f#(X)) -->_1 a__f#(g(X)) -> c_4():4 -->_1 a__f#(X) -> c_3():3 7:S:mark#(g(X)) -> c_7() The dependency graph contains no loops, we remove all dependency pairs. * Step 5: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Signature: {a__c/0,a__f/1,mark/1,a__c#/0,a__f#/1,mark#/1} / {c/0,f/1,g/1,c_1/1,c_2/0,c_3/0,c_4/0,c_5/1,c_6/1,c_7/0} - Obligation: innermost runtime complexity wrt. defined symbols {a__c#,a__f#,mark#} and constructors {c,f,g} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(1))