WORST_CASE(?,O(1)) * Step 1: Sum 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: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 2: 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 3: PredecessorEstimation 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: 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}. Here rules are labelled as follows: 1: *#(x,0()) -> c_1() 2: *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)) 3: *#(1(),y) -> c_3() 4: *#(i(x),x) -> c_4() * Step 4: RemoveWeakSuffixes WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)) - Weak DPs: *#(x,0()) -> c_1() *#(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: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:*#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)) -->_2 *#(i(x),x) -> c_4():4 -->_1 *#(i(x),x) -> c_4():4 -->_2 *#(1(),y) -> c_3():3 -->_1 *#(1(),y) -> c_3():3 -->_2 *#(x,0()) -> c_1():2 -->_1 *#(x,0()) -> c_1():2 -->_2 *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)):1 -->_1 *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)):1 2:W:*#(x,0()) -> c_1() 3:W:*#(1(),y) -> c_3() 4:W:*#(i(x),x) -> c_4() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 2: *#(x,0()) -> c_1() 3: *#(1(),y) -> c_3() 4: *#(i(x),x) -> c_4() * Step 5: RemoveInapplicable WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)) - 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: RemoveInapplicable + Details: Only the nodes {} are reachable from nodes {} that start derivation from marked basic terms. The nodes not reachable are removed from the problem. * Step 6: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - 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: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(1))