WORST_CASE(?,O(n^2)) * Step 1: DependencyPairs WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: ++(.(x,y),z) -> .(x,++(y,z)) ++(nil(),y) -> y car(.(x,y)) -> x cdr(.(x,y)) -> y null(.(x,y)) -> false() null(nil()) -> true() rev(.(x,y)) -> ++(rev(y),.(x,nil())) rev(nil()) -> nil() - Signature: {++/2,car/1,cdr/1,null/1,rev/1} / {./2,false/0,nil/0,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {++,car,cdr,null,rev} and constructors {.,false,nil,true} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs ++#(.(x,y),z) -> c_1(++#(y,z)) ++#(nil(),y) -> c_2() car#(.(x,y)) -> c_3() cdr#(.(x,y)) -> c_4() null#(.(x,y)) -> c_5() null#(nil()) -> c_6() rev#(.(x,y)) -> c_7(++#(rev(y),.(x,nil())),rev#(y)) rev#(nil()) -> c_8() Weak DPs and mark the set of starting terms. * Step 2: PredecessorEstimation WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: ++#(.(x,y),z) -> c_1(++#(y,z)) ++#(nil(),y) -> c_2() car#(.(x,y)) -> c_3() cdr#(.(x,y)) -> c_4() null#(.(x,y)) -> c_5() null#(nil()) -> c_6() rev#(.(x,y)) -> c_7(++#(rev(y),.(x,nil())),rev#(y)) rev#(nil()) -> c_8() - Weak TRS: ++(.(x,y),z) -> .(x,++(y,z)) ++(nil(),y) -> y car(.(x,y)) -> x cdr(.(x,y)) -> y null(.(x,y)) -> false() null(nil()) -> true() rev(.(x,y)) -> ++(rev(y),.(x,nil())) rev(nil()) -> nil() - Signature: {++/2,car/1,cdr/1,null/1,rev/1,++#/2,car#/1,cdr#/1,null#/1,rev#/1} / {./2,false/0,nil/0,true/0,c_1/1,c_2/0 ,c_3/0,c_4/0,c_5/0,c_6/0,c_7/2,c_8/0} - Obligation: innermost runtime complexity wrt. defined symbols {++#,car#,cdr#,null#,rev#} and constructors {.,false,nil ,true} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {2,3,4,5,6,8} by application of Pre({2,3,4,5,6,8}) = {1,7}. Here rules are labelled as follows: 1: ++#(.(x,y),z) -> c_1(++#(y,z)) 2: ++#(nil(),y) -> c_2() 3: car#(.(x,y)) -> c_3() 4: cdr#(.(x,y)) -> c_4() 5: null#(.(x,y)) -> c_5() 6: null#(nil()) -> c_6() 7: rev#(.(x,y)) -> c_7(++#(rev(y),.(x,nil())),rev#(y)) 8: rev#(nil()) -> c_8() * Step 3: RemoveWeakSuffixes WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: ++#(.(x,y),z) -> c_1(++#(y,z)) rev#(.(x,y)) -> c_7(++#(rev(y),.(x,nil())),rev#(y)) - Weak DPs: ++#(nil(),y) -> c_2() car#(.(x,y)) -> c_3() cdr#(.(x,y)) -> c_4() null#(.(x,y)) -> c_5() null#(nil()) -> c_6() rev#(nil()) -> c_8() - Weak TRS: ++(.(x,y),z) -> .(x,++(y,z)) ++(nil(),y) -> y car(.(x,y)) -> x cdr(.(x,y)) -> y null(.(x,y)) -> false() null(nil()) -> true() rev(.(x,y)) -> ++(rev(y),.(x,nil())) rev(nil()) -> nil() - Signature: {++/2,car/1,cdr/1,null/1,rev/1,++#/2,car#/1,cdr#/1,null#/1,rev#/1} / {./2,false/0,nil/0,true/0,c_1/1,c_2/0 ,c_3/0,c_4/0,c_5/0,c_6/0,c_7/2,c_8/0} - Obligation: innermost runtime complexity wrt. defined symbols {++#,car#,cdr#,null#,rev#} and constructors {.,false,nil ,true} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:++#(.(x,y),z) -> c_1(++#(y,z)) -->_1 ++#(nil(),y) -> c_2():3 -->_1 ++#(.(x,y),z) -> c_1(++#(y,z)):1 2:S:rev#(.(x,y)) -> c_7(++#(rev(y),.(x,nil())),rev#(y)) -->_2 rev#(nil()) -> c_8():8 -->_1 ++#(nil(),y) -> c_2():3 -->_2 rev#(.(x,y)) -> c_7(++#(rev(y),.(x,nil())),rev#(y)):2 -->_1 ++#(.(x,y),z) -> c_1(++#(y,z)):1 3:W:++#(nil(),y) -> c_2() 4:W:car#(.(x,y)) -> c_3() 5:W:cdr#(.(x,y)) -> c_4() 6:W:null#(.(x,y)) -> c_5() 7:W:null#(nil()) -> c_6() 8:W:rev#(nil()) -> c_8() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 7: null#(nil()) -> c_6() 6: null#(.(x,y)) -> c_5() 5: cdr#(.(x,y)) -> c_4() 4: car#(.(x,y)) -> c_3() 8: rev#(nil()) -> c_8() 3: ++#(nil(),y) -> c_2() * Step 4: UsableRules WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: ++#(.(x,y),z) -> c_1(++#(y,z)) rev#(.(x,y)) -> c_7(++#(rev(y),.(x,nil())),rev#(y)) - Weak TRS: ++(.(x,y),z) -> .(x,++(y,z)) ++(nil(),y) -> y car(.(x,y)) -> x cdr(.(x,y)) -> y null(.(x,y)) -> false() null(nil()) -> true() rev(.(x,y)) -> ++(rev(y),.(x,nil())) rev(nil()) -> nil() - Signature: {++/2,car/1,cdr/1,null/1,rev/1,++#/2,car#/1,cdr#/1,null#/1,rev#/1} / {./2,false/0,nil/0,true/0,c_1/1,c_2/0 ,c_3/0,c_4/0,c_5/0,c_6/0,c_7/2,c_8/0} - Obligation: innermost runtime complexity wrt. defined symbols {++#,car#,cdr#,null#,rev#} and constructors {.,false,nil ,true} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: ++(.(x,y),z) -> .(x,++(y,z)) ++(nil(),y) -> y rev(.(x,y)) -> ++(rev(y),.(x,nil())) rev(nil()) -> nil() ++#(.(x,y),z) -> c_1(++#(y,z)) rev#(.(x,y)) -> c_7(++#(rev(y),.(x,nil())),rev#(y)) * Step 5: DecomposeDG WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: ++#(.(x,y),z) -> c_1(++#(y,z)) rev#(.(x,y)) -> c_7(++#(rev(y),.(x,nil())),rev#(y)) - Weak TRS: ++(.(x,y),z) -> .(x,++(y,z)) ++(nil(),y) -> y rev(.(x,y)) -> ++(rev(y),.(x,nil())) rev(nil()) -> nil() - Signature: {++/2,car/1,cdr/1,null/1,rev/1,++#/2,car#/1,cdr#/1,null#/1,rev#/1} / {./2,false/0,nil/0,true/0,c_1/1,c_2/0 ,c_3/0,c_4/0,c_5/0,c_6/0,c_7/2,c_8/0} - Obligation: innermost runtime complexity wrt. defined symbols {++#,car#,cdr#,null#,rev#} and constructors {.,false,nil ,true} + Applied Processor: DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing} + Details: We decompose the input problem according to the dependency graph into the upper component rev#(.(x,y)) -> c_7(++#(rev(y),.(x,nil())),rev#(y)) and a lower component ++#(.(x,y),z) -> c_1(++#(y,z)) Further, following extension rules are added to the lower component. rev#(.(x,y)) -> ++#(rev(y),.(x,nil())) rev#(.(x,y)) -> rev#(y) ** Step 5.a:1: SimplifyRHS WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: rev#(.(x,y)) -> c_7(++#(rev(y),.(x,nil())),rev#(y)) - Weak TRS: ++(.(x,y),z) -> .(x,++(y,z)) ++(nil(),y) -> y rev(.(x,y)) -> ++(rev(y),.(x,nil())) rev(nil()) -> nil() - Signature: {++/2,car/1,cdr/1,null/1,rev/1,++#/2,car#/1,cdr#/1,null#/1,rev#/1} / {./2,false/0,nil/0,true/0,c_1/1,c_2/0 ,c_3/0,c_4/0,c_5/0,c_6/0,c_7/2,c_8/0} - Obligation: innermost runtime complexity wrt. defined symbols {++#,car#,cdr#,null#,rev#} and constructors {.,false,nil ,true} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:rev#(.(x,y)) -> c_7(++#(rev(y),.(x,nil())),rev#(y)) -->_2 rev#(.(x,y)) -> c_7(++#(rev(y),.(x,nil())),rev#(y)):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: rev#(.(x,y)) -> c_7(rev#(y)) ** Step 5.a:2: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: rev#(.(x,y)) -> c_7(rev#(y)) - Weak TRS: ++(.(x,y),z) -> .(x,++(y,z)) ++(nil(),y) -> y rev(.(x,y)) -> ++(rev(y),.(x,nil())) rev(nil()) -> nil() - Signature: {++/2,car/1,cdr/1,null/1,rev/1,++#/2,car#/1,cdr#/1,null#/1,rev#/1} / {./2,false/0,nil/0,true/0,c_1/1,c_2/0 ,c_3/0,c_4/0,c_5/0,c_6/0,c_7/1,c_8/0} - Obligation: innermost runtime complexity wrt. defined symbols {++#,car#,cdr#,null#,rev#} and constructors {.,false,nil ,true} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: rev#(.(x,y)) -> c_7(rev#(y)) ** Step 5.a:3: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: rev#(.(x,y)) -> c_7(rev#(y)) - Signature: {++/2,car/1,cdr/1,null/1,rev/1,++#/2,car#/1,cdr#/1,null#/1,rev#/1} / {./2,false/0,nil/0,true/0,c_1/1,c_2/0 ,c_3/0,c_4/0,c_5/0,c_6/0,c_7/1,c_8/0} - Obligation: innermost runtime complexity wrt. defined symbols {++#,car#,cdr#,null#,rev#} and constructors {.,false,nil ,true} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_7) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(++) = [0] p(.) = [1] x1 + [1] x2 + [9] p(car) = [0] p(cdr) = [0] p(false) = [0] p(nil) = [0] p(null) = [0] p(rev) = [0] p(true) = [0] p(++#) = [0] p(car#) = [0] p(cdr#) = [0] p(null#) = [0] p(rev#) = [1] x1 + [0] p(c_1) = [0] p(c_2) = [0] p(c_3) = [0] p(c_4) = [0] p(c_5) = [0] p(c_6) = [0] p(c_7) = [1] x1 + [0] p(c_8) = [0] Following rules are strictly oriented: rev#(.(x,y)) = [1] x + [1] y + [9] > [1] y + [0] = c_7(rev#(y)) Following rules are (at-least) weakly oriented: Further, it can be verified that all rules not oriented are covered by the weightgap condition. ** Step 5.a:4: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: rev#(.(x,y)) -> c_7(rev#(y)) - Signature: {++/2,car/1,cdr/1,null/1,rev/1,++#/2,car#/1,cdr#/1,null#/1,rev#/1} / {./2,false/0,nil/0,true/0,c_1/1,c_2/0 ,c_3/0,c_4/0,c_5/0,c_6/0,c_7/1,c_8/0} - Obligation: innermost runtime complexity wrt. defined symbols {++#,car#,cdr#,null#,rev#} and constructors {.,false,nil ,true} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). ** Step 5.b:1: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: ++#(.(x,y),z) -> c_1(++#(y,z)) - Weak DPs: rev#(.(x,y)) -> ++#(rev(y),.(x,nil())) rev#(.(x,y)) -> rev#(y) - Weak TRS: ++(.(x,y),z) -> .(x,++(y,z)) ++(nil(),y) -> y rev(.(x,y)) -> ++(rev(y),.(x,nil())) rev(nil()) -> nil() - Signature: {++/2,car/1,cdr/1,null/1,rev/1,++#/2,car#/1,cdr#/1,null#/1,rev#/1} / {./2,false/0,nil/0,true/0,c_1/1,c_2/0 ,c_3/0,c_4/0,c_5/0,c_6/0,c_7/2,c_8/0} - Obligation: innermost runtime complexity wrt. defined symbols {++#,car#,cdr#,null#,rev#} and constructors {.,false,nil ,true} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(++) = {1}, uargs(.) = {2}, uargs(++#) = {1}, uargs(c_1) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(++) = [1] x1 + [3] x2 + [0] p(.) = [1] x1 + [1] x2 + [2] p(car) = [0] p(cdr) = [0] p(false) = [0] p(nil) = [0] p(null) = [0] p(rev) = [10] x1 + [11] p(true) = [0] p(++#) = [1] x1 + [13] p(car#) = [0] p(cdr#) = [0] p(null#) = [0] p(rev#) = [10] x1 + [4] p(c_1) = [1] x1 + [1] p(c_2) = [0] p(c_3) = [0] p(c_4) = [0] p(c_5) = [0] p(c_6) = [0] p(c_7) = [0] p(c_8) = [0] Following rules are strictly oriented: ++#(.(x,y),z) = [1] x + [1] y + [15] > [1] y + [14] = c_1(++#(y,z)) Following rules are (at-least) weakly oriented: rev#(.(x,y)) = [10] x + [10] y + [24] >= [10] y + [24] = ++#(rev(y),.(x,nil())) rev#(.(x,y)) = [10] x + [10] y + [24] >= [10] y + [4] = rev#(y) ++(.(x,y),z) = [1] x + [1] y + [3] z + [2] >= [1] x + [1] y + [3] z + [2] = .(x,++(y,z)) ++(nil(),y) = [3] y + [0] >= [1] y + [0] = y rev(.(x,y)) = [10] x + [10] y + [31] >= [3] x + [10] y + [17] = ++(rev(y),.(x,nil())) rev(nil()) = [11] >= [0] = nil() Further, it can be verified that all rules not oriented are covered by the weightgap condition. ** Step 5.b:2: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: ++#(.(x,y),z) -> c_1(++#(y,z)) rev#(.(x,y)) -> ++#(rev(y),.(x,nil())) rev#(.(x,y)) -> rev#(y) - Weak TRS: ++(.(x,y),z) -> .(x,++(y,z)) ++(nil(),y) -> y rev(.(x,y)) -> ++(rev(y),.(x,nil())) rev(nil()) -> nil() - Signature: {++/2,car/1,cdr/1,null/1,rev/1,++#/2,car#/1,cdr#/1,null#/1,rev#/1} / {./2,false/0,nil/0,true/0,c_1/1,c_2/0 ,c_3/0,c_4/0,c_5/0,c_6/0,c_7/2,c_8/0} - Obligation: innermost runtime complexity wrt. defined symbols {++#,car#,cdr#,null#,rev#} and constructors {.,false,nil ,true} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^2))