* Step 1: DependencyPairs WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: 0() -> 1() f(s(x)) -> f(g(x,x)) g(0(),1()) -> s(0()) - Signature: {0/0,f/1,g/2} / {1/0,s/1} - Obligation: runtime complexity wrt. defined symbols {0,f,g} and constructors {1,s} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following weak dependency pairs: Strict DPs 0#() -> c_1() f#(s(x)) -> c_2(f#(g(x,x))) g#(0(),1()) -> c_3(0#()) Weak DPs and mark the set of starting terms. * Step 2: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: 0#() -> c_1() f#(s(x)) -> c_2(f#(g(x,x))) g#(0(),1()) -> c_3(0#()) - Strict TRS: 0() -> 1() f(s(x)) -> f(g(x,x)) g(0(),1()) -> s(0()) - Signature: {0/0,f/1,g/2,0#/0,f#/1,g#/2} / {1/0,s/1,c_1/0,c_2/1,c_3/1} - Obligation: runtime complexity wrt. defined symbols {0#,f#,g#} and constructors {1,s} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: 0() -> 1() g(0(),1()) -> s(0()) 0#() -> c_1() f#(s(x)) -> c_2(f#(g(x,x))) * Step 3: PredecessorEstimation WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: 0#() -> c_1() f#(s(x)) -> c_2(f#(g(x,x))) - Strict TRS: 0() -> 1() g(0(),1()) -> s(0()) - Signature: {0/0,f/1,g/2,0#/0,f#/1,g#/2} / {1/0,s/1,c_1/0,c_2/1,c_3/1} - Obligation: runtime complexity wrt. defined symbols {0#,f#,g#} and constructors {1,s} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1} by application of Pre({1}) = {}. Here rules are labelled as follows: 1: 0#() -> c_1() 2: f#(s(x)) -> c_2(f#(g(x,x))) * Step 4: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: f#(s(x)) -> c_2(f#(g(x,x))) - Strict TRS: 0() -> 1() g(0(),1()) -> s(0()) - Weak DPs: 0#() -> c_1() - Signature: {0/0,f/1,g/2,0#/0,f#/1,g#/2} / {1/0,s/1,c_1/0,c_2/1,c_3/1} - Obligation: runtime complexity wrt. defined symbols {0#,f#,g#} and constructors {1,s} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 0, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following nonconstant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: none Following symbols are considered usable: all TcT has computed the following interpretation: p(0) = [0] p(1) = [5] p(f) = [0] p(g) = [1] x2 + [0] p(s) = [1] x1 + [0] p(0#) = [0] p(f#) = [3] p(g#) = [0] p(c_1) = [0] p(c_2) = [0] p(c_3) = [0] Following rules are strictly oriented: f#(s(x)) = [3] > [0] = c_2(f#(g(x,x))) g(0(),1()) = [5] > [0] = s(0()) Following rules are (at-least) weakly oriented: 0#() = [0] >= [0] = c_1() 0() = [0] >= [5] = 1() Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 5: MI WORST_CASE(?,O(1)) + Considered Problem: - Strict TRS: 0() -> 1() - Weak DPs: 0#() -> c_1() f#(s(x)) -> c_2(f#(g(x,x))) - Weak TRS: g(0(),1()) -> s(0()) - Signature: {0/0,f/1,g/2,0#/0,f#/1,g#/2} / {1/0,s/1,c_1/0,c_2/1,c_3/1} - Obligation: runtime complexity wrt. defined symbols {0#,f#,g#} and constructors {1,s} + Applied Processor: MI {miKind = MaximalMatrix (UpperTriangular (Multiplicity (Just 0))), miDimension = 1, miUArgs = UArgs, miURules = URules, miSelector = Just any strict-rules} + Details: We apply a matrix interpretation of kind MaximalMatrix (UpperTriangular (Multiplicity (Just 0))): The following argument positions are considered usable: none Following symbols are considered usable: all TcT has computed the following interpretation: p(0) = [8] p(1) = [0] p(f) = [0] p(g) = [0] p(s) = [0] p(0#) = [1] p(f#) = [0] p(g#) = [0] p(c_1) = [1] p(c_2) = [8] x_1 + [0] p(c_3) = [1] x_1 + [1] Following rules are strictly oriented: 0() = [8] > [0] = 1() Following rules are (at-least) weakly oriented: 0#() = [1] >= [1] = c_1() f#(s(x)) = [0] >= [0] = c_2(f#(g(x,x))) g(0(),1()) = [0] >= [0] = s(0()) * Step 6: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: 0#() -> c_1() f#(s(x)) -> c_2(f#(g(x,x))) - Weak TRS: 0() -> 1() g(0(),1()) -> s(0()) - Signature: {0/0,f/1,g/2,0#/0,f#/1,g#/2} / {1/0,s/1,c_1/0,c_2/1,c_3/1} - Obligation: runtime complexity wrt. defined symbols {0#,f#,g#} and constructors {1,s} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^1))