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