WORST_CASE(?,O(n^1)) * Step 1: DependencyPairs WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: even(Cons(x,Nil())) -> False() even(Cons(x',Cons(x,xs))) -> even(xs) even(Nil()) -> True() goal(x,y) -> and(lte(x,y),even(x)) lte(Cons(x,xs),Nil()) -> False() lte(Cons(x',xs'),Cons(x,xs)) -> lte(xs',xs) lte(Nil(),y) -> True() notEmpty(Cons(x,xs)) -> True() notEmpty(Nil()) -> False() - Weak TRS: and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() - Signature: {and/2,even/1,goal/2,lte/2,notEmpty/1} / {Cons/2,False/0,Nil/0,True/0} - Obligation: innermost runtime complexity wrt. defined symbols {and,even,goal,lte,notEmpty} and constructors {Cons,False ,Nil,True} + Applied Processor: DependencyPairs {dpKind_ = WIDP} + Details: We add the following weak innermost dependency pairs: Strict DPs even#(Cons(x,Nil())) -> c_1() even#(Cons(x',Cons(x,xs))) -> c_2(even#(xs)) even#(Nil()) -> c_3() goal#(x,y) -> c_4(and#(lte(x,y),even(x))) lte#(Cons(x,xs),Nil()) -> c_5() lte#(Cons(x',xs'),Cons(x,xs)) -> c_6(lte#(xs',xs)) lte#(Nil(),y) -> c_7() notEmpty#(Cons(x,xs)) -> c_8() notEmpty#(Nil()) -> c_9() Weak DPs and#(False(),False()) -> c_10() and#(False(),True()) -> c_11() and#(True(),False()) -> c_12() and#(True(),True()) -> c_13() and mark the set of starting terms. * Step 2: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: even#(Cons(x,Nil())) -> c_1() even#(Cons(x',Cons(x,xs))) -> c_2(even#(xs)) even#(Nil()) -> c_3() goal#(x,y) -> c_4(and#(lte(x,y),even(x))) lte#(Cons(x,xs),Nil()) -> c_5() lte#(Cons(x',xs'),Cons(x,xs)) -> c_6(lte#(xs',xs)) lte#(Nil(),y) -> c_7() notEmpty#(Cons(x,xs)) -> c_8() notEmpty#(Nil()) -> c_9() - Strict TRS: even(Cons(x,Nil())) -> False() even(Cons(x',Cons(x,xs))) -> even(xs) even(Nil()) -> True() goal(x,y) -> and(lte(x,y),even(x)) lte(Cons(x,xs),Nil()) -> False() lte(Cons(x',xs'),Cons(x,xs)) -> lte(xs',xs) lte(Nil(),y) -> True() notEmpty(Cons(x,xs)) -> True() notEmpty(Nil()) -> False() - Weak DPs: and#(False(),False()) -> c_10() and#(False(),True()) -> c_11() and#(True(),False()) -> c_12() and#(True(),True()) -> c_13() - Weak TRS: and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() - Signature: {and/2,even/1,goal/2,lte/2,notEmpty/1,and#/2,even#/1,goal#/2,lte#/2,notEmpty#/1} / {Cons/2,False/0,Nil/0 ,True/0,c_1/0,c_2/1,c_3/0,c_4/1,c_5/0,c_6/1,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/0} - Obligation: innermost runtime complexity wrt. defined symbols {and#,even#,goal#,lte#,notEmpty#} and constructors {Cons ,False,Nil,True} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: even(Cons(x,Nil())) -> False() even(Cons(x',Cons(x,xs))) -> even(xs) even(Nil()) -> True() lte(Cons(x,xs),Nil()) -> False() lte(Cons(x',xs'),Cons(x,xs)) -> lte(xs',xs) lte(Nil(),y) -> True() and#(False(),False()) -> c_10() and#(False(),True()) -> c_11() and#(True(),False()) -> c_12() and#(True(),True()) -> c_13() even#(Cons(x,Nil())) -> c_1() even#(Cons(x',Cons(x,xs))) -> c_2(even#(xs)) even#(Nil()) -> c_3() goal#(x,y) -> c_4(and#(lte(x,y),even(x))) lte#(Cons(x,xs),Nil()) -> c_5() lte#(Cons(x',xs'),Cons(x,xs)) -> c_6(lte#(xs',xs)) lte#(Nil(),y) -> c_7() notEmpty#(Cons(x,xs)) -> c_8() notEmpty#(Nil()) -> c_9() * Step 3: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: even#(Cons(x,Nil())) -> c_1() even#(Cons(x',Cons(x,xs))) -> c_2(even#(xs)) even#(Nil()) -> c_3() goal#(x,y) -> c_4(and#(lte(x,y),even(x))) lte#(Cons(x,xs),Nil()) -> c_5() lte#(Cons(x',xs'),Cons(x,xs)) -> c_6(lte#(xs',xs)) lte#(Nil(),y) -> c_7() notEmpty#(Cons(x,xs)) -> c_8() notEmpty#(Nil()) -> c_9() - Strict TRS: even(Cons(x,Nil())) -> False() even(Cons(x',Cons(x,xs))) -> even(xs) even(Nil()) -> True() lte(Cons(x,xs),Nil()) -> False() lte(Cons(x',xs'),Cons(x,xs)) -> lte(xs',xs) lte(Nil(),y) -> True() - Weak DPs: and#(False(),False()) -> c_10() and#(False(),True()) -> c_11() and#(True(),False()) -> c_12() and#(True(),True()) -> c_13() - Signature: {and/2,even/1,goal/2,lte/2,notEmpty/1,and#/2,even#/1,goal#/2,lte#/2,notEmpty#/1} / {Cons/2,False/0,Nil/0 ,True/0,c_1/0,c_2/1,c_3/0,c_4/1,c_5/0,c_6/1,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/0} - Obligation: innermost runtime complexity wrt. defined symbols {and#,even#,goal#,lte#,notEmpty#} and constructors {Cons ,False,Nil,True} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnTrs} + 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(and#) = {1,2}, uargs(c_2) = {1}, uargs(c_4) = {1}, uargs(c_6) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(Cons) = [1] x1 + [1] x2 + [4] p(False) = [2] p(Nil) = [7] p(True) = [0] p(and) = [0] p(even) = [2] x1 + [1] p(goal) = [0] p(lte) = [1] x2 + [1] p(notEmpty) = [0] p(and#) = [1] x1 + [1] x2 + [1] p(even#) = [0] p(goal#) = [2] x1 + [2] x2 + [0] p(lte#) = [1] x2 + [0] p(notEmpty#) = [3] x1 + [4] p(c_1) = [0] p(c_2) = [1] x1 + [0] p(c_3) = [2] p(c_4) = [1] x1 + [1] p(c_5) = [0] p(c_6) = [1] x1 + [8] p(c_7) = [8] p(c_8) = [0] p(c_9) = [1] p(c_10) = [0] p(c_11) = [3] p(c_12) = [0] p(c_13) = [0] Following rules are strictly oriented: lte#(Cons(x,xs),Nil()) = [7] > [0] = c_5() notEmpty#(Cons(x,xs)) = [3] x + [3] xs + [16] > [0] = c_8() notEmpty#(Nil()) = [25] > [1] = c_9() even(Cons(x,Nil())) = [2] x + [23] > [2] = False() even(Cons(x',Cons(x,xs))) = [2] x + [2] x' + [2] xs + [17] > [2] xs + [1] = even(xs) even(Nil()) = [15] > [0] = True() lte(Cons(x,xs),Nil()) = [8] > [2] = False() lte(Cons(x',xs'),Cons(x,xs)) = [1] x + [1] xs + [5] > [1] xs + [1] = lte(xs',xs) lte(Nil(),y) = [1] y + [1] > [0] = True() Following rules are (at-least) weakly oriented: and#(False(),False()) = [5] >= [0] = c_10() and#(False(),True()) = [3] >= [3] = c_11() and#(True(),False()) = [3] >= [0] = c_12() and#(True(),True()) = [1] >= [0] = c_13() even#(Cons(x,Nil())) = [0] >= [0] = c_1() even#(Cons(x',Cons(x,xs))) = [0] >= [0] = c_2(even#(xs)) even#(Nil()) = [0] >= [2] = c_3() goal#(x,y) = [2] x + [2] y + [0] >= [2] x + [1] y + [4] = c_4(and#(lte(x,y),even(x))) lte#(Cons(x',xs'),Cons(x,xs)) = [1] x + [1] xs + [4] >= [1] xs + [8] = c_6(lte#(xs',xs)) lte#(Nil(),y) = [1] y + [0] >= [8] = c_7() Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 4: PredecessorEstimation WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: even#(Cons(x,Nil())) -> c_1() even#(Cons(x',Cons(x,xs))) -> c_2(even#(xs)) even#(Nil()) -> c_3() goal#(x,y) -> c_4(and#(lte(x,y),even(x))) lte#(Cons(x',xs'),Cons(x,xs)) -> c_6(lte#(xs',xs)) lte#(Nil(),y) -> c_7() - Weak DPs: and#(False(),False()) -> c_10() and#(False(),True()) -> c_11() and#(True(),False()) -> c_12() and#(True(),True()) -> c_13() lte#(Cons(x,xs),Nil()) -> c_5() notEmpty#(Cons(x,xs)) -> c_8() notEmpty#(Nil()) -> c_9() - Weak TRS: even(Cons(x,Nil())) -> False() even(Cons(x',Cons(x,xs))) -> even(xs) even(Nil()) -> True() lte(Cons(x,xs),Nil()) -> False() lte(Cons(x',xs'),Cons(x,xs)) -> lte(xs',xs) lte(Nil(),y) -> True() - Signature: {and/2,even/1,goal/2,lte/2,notEmpty/1,and#/2,even#/1,goal#/2,lte#/2,notEmpty#/1} / {Cons/2,False/0,Nil/0 ,True/0,c_1/0,c_2/1,c_3/0,c_4/1,c_5/0,c_6/1,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/0} - Obligation: innermost runtime complexity wrt. defined symbols {and#,even#,goal#,lte#,notEmpty#} and constructors {Cons ,False,Nil,True} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,3,4,6} by application of Pre({1,3,4,6}) = {2,5}. Here rules are labelled as follows: 1: even#(Cons(x,Nil())) -> c_1() 2: even#(Cons(x',Cons(x,xs))) -> c_2(even#(xs)) 3: even#(Nil()) -> c_3() 4: goal#(x,y) -> c_4(and#(lte(x,y),even(x))) 5: lte#(Cons(x',xs'),Cons(x,xs)) -> c_6(lte#(xs',xs)) 6: lte#(Nil(),y) -> c_7() 7: and#(False(),False()) -> c_10() 8: and#(False(),True()) -> c_11() 9: and#(True(),False()) -> c_12() 10: and#(True(),True()) -> c_13() 11: lte#(Cons(x,xs),Nil()) -> c_5() 12: notEmpty#(Cons(x,xs)) -> c_8() 13: notEmpty#(Nil()) -> c_9() * Step 5: RemoveWeakSuffixes WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: even#(Cons(x',Cons(x,xs))) -> c_2(even#(xs)) lte#(Cons(x',xs'),Cons(x,xs)) -> c_6(lte#(xs',xs)) - Weak DPs: and#(False(),False()) -> c_10() and#(False(),True()) -> c_11() and#(True(),False()) -> c_12() and#(True(),True()) -> c_13() even#(Cons(x,Nil())) -> c_1() even#(Nil()) -> c_3() goal#(x,y) -> c_4(and#(lte(x,y),even(x))) lte#(Cons(x,xs),Nil()) -> c_5() lte#(Nil(),y) -> c_7() notEmpty#(Cons(x,xs)) -> c_8() notEmpty#(Nil()) -> c_9() - Weak TRS: even(Cons(x,Nil())) -> False() even(Cons(x',Cons(x,xs))) -> even(xs) even(Nil()) -> True() lte(Cons(x,xs),Nil()) -> False() lte(Cons(x',xs'),Cons(x,xs)) -> lte(xs',xs) lte(Nil(),y) -> True() - Signature: {and/2,even/1,goal/2,lte/2,notEmpty/1,and#/2,even#/1,goal#/2,lte#/2,notEmpty#/1} / {Cons/2,False/0,Nil/0 ,True/0,c_1/0,c_2/1,c_3/0,c_4/1,c_5/0,c_6/1,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/0} - Obligation: innermost runtime complexity wrt. defined symbols {and#,even#,goal#,lte#,notEmpty#} and constructors {Cons ,False,Nil,True} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:even#(Cons(x',Cons(x,xs))) -> c_2(even#(xs)) -->_1 even#(Nil()) -> c_3():8 -->_1 even#(Cons(x,Nil())) -> c_1():7 -->_1 even#(Cons(x',Cons(x,xs))) -> c_2(even#(xs)):1 2:S:lte#(Cons(x',xs'),Cons(x,xs)) -> c_6(lte#(xs',xs)) -->_1 lte#(Nil(),y) -> c_7():11 -->_1 lte#(Cons(x,xs),Nil()) -> c_5():10 -->_1 lte#(Cons(x',xs'),Cons(x,xs)) -> c_6(lte#(xs',xs)):2 3:W:and#(False(),False()) -> c_10() 4:W:and#(False(),True()) -> c_11() 5:W:and#(True(),False()) -> c_12() 6:W:and#(True(),True()) -> c_13() 7:W:even#(Cons(x,Nil())) -> c_1() 8:W:even#(Nil()) -> c_3() 9:W:goal#(x,y) -> c_4(and#(lte(x,y),even(x))) -->_1 and#(True(),True()) -> c_13():6 -->_1 and#(True(),False()) -> c_12():5 -->_1 and#(False(),True()) -> c_11():4 -->_1 and#(False(),False()) -> c_10():3 10:W:lte#(Cons(x,xs),Nil()) -> c_5() 11:W:lte#(Nil(),y) -> c_7() 12:W:notEmpty#(Cons(x,xs)) -> c_8() 13:W:notEmpty#(Nil()) -> c_9() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 13: notEmpty#(Nil()) -> c_9() 12: notEmpty#(Cons(x,xs)) -> c_8() 9: goal#(x,y) -> c_4(and#(lte(x,y),even(x))) 6: and#(True(),True()) -> c_13() 5: and#(True(),False()) -> c_12() 4: and#(False(),True()) -> c_11() 3: and#(False(),False()) -> c_10() 10: lte#(Cons(x,xs),Nil()) -> c_5() 11: lte#(Nil(),y) -> c_7() 7: even#(Cons(x,Nil())) -> c_1() 8: even#(Nil()) -> c_3() * Step 6: Decompose WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: even#(Cons(x',Cons(x,xs))) -> c_2(even#(xs)) lte#(Cons(x',xs'),Cons(x,xs)) -> c_6(lte#(xs',xs)) - Weak TRS: even(Cons(x,Nil())) -> False() even(Cons(x',Cons(x,xs))) -> even(xs) even(Nil()) -> True() lte(Cons(x,xs),Nil()) -> False() lte(Cons(x',xs'),Cons(x,xs)) -> lte(xs',xs) lte(Nil(),y) -> True() - Signature: {and/2,even/1,goal/2,lte/2,notEmpty/1,and#/2,even#/1,goal#/2,lte#/2,notEmpty#/1} / {Cons/2,False/0,Nil/0 ,True/0,c_1/0,c_2/1,c_3/0,c_4/1,c_5/0,c_6/1,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/0} - Obligation: innermost runtime complexity wrt. defined symbols {and#,even#,goal#,lte#,notEmpty#} and constructors {Cons ,False,Nil,True} + Applied Processor: Decompose {onSelection = all cycle independent sub-graph, withBound = RelativeAdd} + Details: We analyse the complexity of following sub-problems (R) and (S). Problem (S) is obtained from the input problem by shifting strict rules from (R) into the weak component. Problem (R) - Strict DPs: even#(Cons(x',Cons(x,xs))) -> c_2(even#(xs)) - Weak DPs: lte#(Cons(x',xs'),Cons(x,xs)) -> c_6(lte#(xs',xs)) - Weak TRS: even(Cons(x,Nil())) -> False() even(Cons(x',Cons(x,xs))) -> even(xs) even(Nil()) -> True() lte(Cons(x,xs),Nil()) -> False() lte(Cons(x',xs'),Cons(x,xs)) -> lte(xs',xs) lte(Nil(),y) -> True() - Signature: {and/2,even/1,goal/2,lte/2,notEmpty/1,and#/2,even#/1,goal#/2,lte#/2,notEmpty#/1} / {Cons/2,False/0,Nil/0 ,True/0,c_1/0,c_2/1,c_3/0,c_4/1,c_5/0,c_6/1,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/0} - Obligation: innermost runtime complexity wrt. defined symbols {and#,even#,goal#,lte#,notEmpty#} and constructors {Cons ,False,Nil,True} Problem (S) - Strict DPs: lte#(Cons(x',xs'),Cons(x,xs)) -> c_6(lte#(xs',xs)) - Weak DPs: even#(Cons(x',Cons(x,xs))) -> c_2(even#(xs)) - Weak TRS: even(Cons(x,Nil())) -> False() even(Cons(x',Cons(x,xs))) -> even(xs) even(Nil()) -> True() lte(Cons(x,xs),Nil()) -> False() lte(Cons(x',xs'),Cons(x,xs)) -> lte(xs',xs) lte(Nil(),y) -> True() - Signature: {and/2,even/1,goal/2,lte/2,notEmpty/1,and#/2,even#/1,goal#/2,lte#/2,notEmpty#/1} / {Cons/2,False/0,Nil/0 ,True/0,c_1/0,c_2/1,c_3/0,c_4/1,c_5/0,c_6/1,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/0} - Obligation: innermost runtime complexity wrt. defined symbols {and#,even#,goal#,lte#,notEmpty#} and constructors {Cons ,False,Nil,True} ** Step 6.a:1: RemoveWeakSuffixes WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: even#(Cons(x',Cons(x,xs))) -> c_2(even#(xs)) - Weak DPs: lte#(Cons(x',xs'),Cons(x,xs)) -> c_6(lte#(xs',xs)) - Weak TRS: even(Cons(x,Nil())) -> False() even(Cons(x',Cons(x,xs))) -> even(xs) even(Nil()) -> True() lte(Cons(x,xs),Nil()) -> False() lte(Cons(x',xs'),Cons(x,xs)) -> lte(xs',xs) lte(Nil(),y) -> True() - Signature: {and/2,even/1,goal/2,lte/2,notEmpty/1,and#/2,even#/1,goal#/2,lte#/2,notEmpty#/1} / {Cons/2,False/0,Nil/0 ,True/0,c_1/0,c_2/1,c_3/0,c_4/1,c_5/0,c_6/1,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/0} - Obligation: innermost runtime complexity wrt. defined symbols {and#,even#,goal#,lte#,notEmpty#} and constructors {Cons ,False,Nil,True} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:even#(Cons(x',Cons(x,xs))) -> c_2(even#(xs)) -->_1 even#(Cons(x',Cons(x,xs))) -> c_2(even#(xs)):1 2:W:lte#(Cons(x',xs'),Cons(x,xs)) -> c_6(lte#(xs',xs)) -->_1 lte#(Cons(x',xs'),Cons(x,xs)) -> c_6(lte#(xs',xs)):2 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 2: lte#(Cons(x',xs'),Cons(x,xs)) -> c_6(lte#(xs',xs)) ** Step 6.a:2: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: even#(Cons(x',Cons(x,xs))) -> c_2(even#(xs)) - Weak TRS: even(Cons(x,Nil())) -> False() even(Cons(x',Cons(x,xs))) -> even(xs) even(Nil()) -> True() lte(Cons(x,xs),Nil()) -> False() lte(Cons(x',xs'),Cons(x,xs)) -> lte(xs',xs) lte(Nil(),y) -> True() - Signature: {and/2,even/1,goal/2,lte/2,notEmpty/1,and#/2,even#/1,goal#/2,lte#/2,notEmpty#/1} / {Cons/2,False/0,Nil/0 ,True/0,c_1/0,c_2/1,c_3/0,c_4/1,c_5/0,c_6/1,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/0} - Obligation: innermost runtime complexity wrt. defined symbols {and#,even#,goal#,lte#,notEmpty#} and constructors {Cons ,False,Nil,True} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: even#(Cons(x',Cons(x,xs))) -> c_2(even#(xs)) ** Step 6.a:3: PredecessorEstimationCP WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: even#(Cons(x',Cons(x,xs))) -> c_2(even#(xs)) - Signature: {and/2,even/1,goal/2,lte/2,notEmpty/1,and#/2,even#/1,goal#/2,lte#/2,notEmpty#/1} / {Cons/2,False/0,Nil/0 ,True/0,c_1/0,c_2/1,c_3/0,c_4/1,c_5/0,c_6/1,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/0} - Obligation: innermost runtime complexity wrt. defined symbols {and#,even#,goal#,lte#,notEmpty#} and constructors {Cons ,False,Nil,True} + Applied Processor: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 1: even#(Cons(x',Cons(x,xs))) -> c_2(even#(xs)) The strictly oriented rules are moved into the weak component. *** Step 6.a:3.a:1: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: even#(Cons(x',Cons(x,xs))) -> c_2(even#(xs)) - Signature: {and/2,even/1,goal/2,lte/2,notEmpty/1,and#/2,even#/1,goal#/2,lte#/2,notEmpty#/1} / {Cons/2,False/0,Nil/0 ,True/0,c_1/0,c_2/1,c_3/0,c_4/1,c_5/0,c_6/1,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/0} - Obligation: innermost runtime complexity wrt. defined symbols {and#,even#,goal#,lte#,notEmpty#} and constructors {Cons ,False,Nil,True} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_2) = {1} Following symbols are considered usable: {and#,even#,goal#,lte#,notEmpty#} TcT has computed the following interpretation: p(Cons) = [1] x1 + [1] x2 + [1] p(False) = [0] p(Nil) = [0] p(True) = [0] p(and) = [0] p(even) = [0] p(goal) = [0] p(lte) = [0] p(notEmpty) = [0] p(and#) = [0] p(even#) = [6] x1 + [0] p(goal#) = [8] p(lte#) = [1] x1 + [8] p(notEmpty#) = [1] x1 + [0] p(c_1) = [2] p(c_2) = [1] x1 + [4] p(c_3) = [2] p(c_4) = [1] x1 + [0] p(c_5) = [2] p(c_6) = [4] x1 + [2] p(c_7) = [0] p(c_8) = [0] p(c_9) = [0] p(c_10) = [0] p(c_11) = [2] p(c_12) = [1] p(c_13) = [1] Following rules are strictly oriented: even#(Cons(x',Cons(x,xs))) = [6] x + [6] x' + [6] xs + [12] > [6] xs + [4] = c_2(even#(xs)) Following rules are (at-least) weakly oriented: *** Step 6.a:3.a:2: Assumption WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: even#(Cons(x',Cons(x,xs))) -> c_2(even#(xs)) - Signature: {and/2,even/1,goal/2,lte/2,notEmpty/1,and#/2,even#/1,goal#/2,lte#/2,notEmpty#/1} / {Cons/2,False/0,Nil/0 ,True/0,c_1/0,c_2/1,c_3/0,c_4/1,c_5/0,c_6/1,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/0} - Obligation: innermost runtime complexity wrt. defined symbols {and#,even#,goal#,lte#,notEmpty#} and constructors {Cons ,False,Nil,True} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}} + Details: () *** Step 6.a:3.b:1: RemoveWeakSuffixes WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: even#(Cons(x',Cons(x,xs))) -> c_2(even#(xs)) - Signature: {and/2,even/1,goal/2,lte/2,notEmpty/1,and#/2,even#/1,goal#/2,lte#/2,notEmpty#/1} / {Cons/2,False/0,Nil/0 ,True/0,c_1/0,c_2/1,c_3/0,c_4/1,c_5/0,c_6/1,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/0} - Obligation: innermost runtime complexity wrt. defined symbols {and#,even#,goal#,lte#,notEmpty#} and constructors {Cons ,False,Nil,True} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:W:even#(Cons(x',Cons(x,xs))) -> c_2(even#(xs)) -->_1 even#(Cons(x',Cons(x,xs))) -> c_2(even#(xs)):1 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 1: even#(Cons(x',Cons(x,xs))) -> c_2(even#(xs)) *** Step 6.a:3.b:2: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Signature: {and/2,even/1,goal/2,lte/2,notEmpty/1,and#/2,even#/1,goal#/2,lte#/2,notEmpty#/1} / {Cons/2,False/0,Nil/0 ,True/0,c_1/0,c_2/1,c_3/0,c_4/1,c_5/0,c_6/1,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/0} - Obligation: innermost runtime complexity wrt. defined symbols {and#,even#,goal#,lte#,notEmpty#} and constructors {Cons ,False,Nil,True} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). ** Step 6.b:1: RemoveWeakSuffixes WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: lte#(Cons(x',xs'),Cons(x,xs)) -> c_6(lte#(xs',xs)) - Weak DPs: even#(Cons(x',Cons(x,xs))) -> c_2(even#(xs)) - Weak TRS: even(Cons(x,Nil())) -> False() even(Cons(x',Cons(x,xs))) -> even(xs) even(Nil()) -> True() lte(Cons(x,xs),Nil()) -> False() lte(Cons(x',xs'),Cons(x,xs)) -> lte(xs',xs) lte(Nil(),y) -> True() - Signature: {and/2,even/1,goal/2,lte/2,notEmpty/1,and#/2,even#/1,goal#/2,lte#/2,notEmpty#/1} / {Cons/2,False/0,Nil/0 ,True/0,c_1/0,c_2/1,c_3/0,c_4/1,c_5/0,c_6/1,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/0} - Obligation: innermost runtime complexity wrt. defined symbols {and#,even#,goal#,lte#,notEmpty#} and constructors {Cons ,False,Nil,True} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:lte#(Cons(x',xs'),Cons(x,xs)) -> c_6(lte#(xs',xs)) -->_1 lte#(Cons(x',xs'),Cons(x,xs)) -> c_6(lte#(xs',xs)):1 2:W:even#(Cons(x',Cons(x,xs))) -> c_2(even#(xs)) -->_1 even#(Cons(x',Cons(x,xs))) -> c_2(even#(xs)):2 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 2: even#(Cons(x',Cons(x,xs))) -> c_2(even#(xs)) ** Step 6.b:2: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: lte#(Cons(x',xs'),Cons(x,xs)) -> c_6(lte#(xs',xs)) - Weak TRS: even(Cons(x,Nil())) -> False() even(Cons(x',Cons(x,xs))) -> even(xs) even(Nil()) -> True() lte(Cons(x,xs),Nil()) -> False() lte(Cons(x',xs'),Cons(x,xs)) -> lte(xs',xs) lte(Nil(),y) -> True() - Signature: {and/2,even/1,goal/2,lte/2,notEmpty/1,and#/2,even#/1,goal#/2,lte#/2,notEmpty#/1} / {Cons/2,False/0,Nil/0 ,True/0,c_1/0,c_2/1,c_3/0,c_4/1,c_5/0,c_6/1,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/0} - Obligation: innermost runtime complexity wrt. defined symbols {and#,even#,goal#,lte#,notEmpty#} and constructors {Cons ,False,Nil,True} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: lte#(Cons(x',xs'),Cons(x,xs)) -> c_6(lte#(xs',xs)) ** Step 6.b:3: PredecessorEstimationCP WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: lte#(Cons(x',xs'),Cons(x,xs)) -> c_6(lte#(xs',xs)) - Signature: {and/2,even/1,goal/2,lte/2,notEmpty/1,and#/2,even#/1,goal#/2,lte#/2,notEmpty#/1} / {Cons/2,False/0,Nil/0 ,True/0,c_1/0,c_2/1,c_3/0,c_4/1,c_5/0,c_6/1,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/0} - Obligation: innermost runtime complexity wrt. defined symbols {and#,even#,goal#,lte#,notEmpty#} and constructors {Cons ,False,Nil,True} + Applied Processor: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 1: lte#(Cons(x',xs'),Cons(x,xs)) -> c_6(lte#(xs',xs)) The strictly oriented rules are moved into the weak component. *** Step 6.b:3.a:1: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: lte#(Cons(x',xs'),Cons(x,xs)) -> c_6(lte#(xs',xs)) - Signature: {and/2,even/1,goal/2,lte/2,notEmpty/1,and#/2,even#/1,goal#/2,lte#/2,notEmpty#/1} / {Cons/2,False/0,Nil/0 ,True/0,c_1/0,c_2/1,c_3/0,c_4/1,c_5/0,c_6/1,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/0} - Obligation: innermost runtime complexity wrt. defined symbols {and#,even#,goal#,lte#,notEmpty#} and constructors {Cons ,False,Nil,True} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_6) = {1} Following symbols are considered usable: {and#,even#,goal#,lte#,notEmpty#} TcT has computed the following interpretation: p(Cons) = [1] x2 + [2] p(False) = [1] p(Nil) = [2] p(True) = [0] p(and) = [2] x2 + [0] p(even) = [2] p(goal) = [1] x1 + [2] x2 + [8] p(lte) = [1] x1 + [1] x2 + [2] p(notEmpty) = [1] x1 + [1] p(and#) = [1] x2 + [2] p(even#) = [2] x1 + [2] p(goal#) = [1] x1 + [0] p(lte#) = [1] x1 + [0] p(notEmpty#) = [1] x1 + [1] p(c_1) = [1] p(c_2) = [1] p(c_3) = [4] p(c_4) = [0] p(c_5) = [1] p(c_6) = [1] x1 + [0] p(c_7) = [2] p(c_8) = [8] p(c_9) = [1] p(c_10) = [1] p(c_11) = [1] p(c_12) = [0] p(c_13) = [0] Following rules are strictly oriented: lte#(Cons(x',xs'),Cons(x,xs)) = [1] xs' + [2] > [1] xs' + [0] = c_6(lte#(xs',xs)) Following rules are (at-least) weakly oriented: *** Step 6.b:3.a:2: Assumption WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: lte#(Cons(x',xs'),Cons(x,xs)) -> c_6(lte#(xs',xs)) - Signature: {and/2,even/1,goal/2,lte/2,notEmpty/1,and#/2,even#/1,goal#/2,lte#/2,notEmpty#/1} / {Cons/2,False/0,Nil/0 ,True/0,c_1/0,c_2/1,c_3/0,c_4/1,c_5/0,c_6/1,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/0} - Obligation: innermost runtime complexity wrt. defined symbols {and#,even#,goal#,lte#,notEmpty#} and constructors {Cons ,False,Nil,True} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}} + Details: () *** Step 6.b:3.b:1: RemoveWeakSuffixes WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: lte#(Cons(x',xs'),Cons(x,xs)) -> c_6(lte#(xs',xs)) - Signature: {and/2,even/1,goal/2,lte/2,notEmpty/1,and#/2,even#/1,goal#/2,lte#/2,notEmpty#/1} / {Cons/2,False/0,Nil/0 ,True/0,c_1/0,c_2/1,c_3/0,c_4/1,c_5/0,c_6/1,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/0} - Obligation: innermost runtime complexity wrt. defined symbols {and#,even#,goal#,lte#,notEmpty#} and constructors {Cons ,False,Nil,True} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:W:lte#(Cons(x',xs'),Cons(x,xs)) -> c_6(lte#(xs',xs)) -->_1 lte#(Cons(x',xs'),Cons(x,xs)) -> c_6(lte#(xs',xs)):1 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 1: lte#(Cons(x',xs'),Cons(x,xs)) -> c_6(lte#(xs',xs)) *** Step 6.b:3.b:2: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Signature: {and/2,even/1,goal/2,lte/2,notEmpty/1,and#/2,even#/1,goal#/2,lte#/2,notEmpty#/1} / {Cons/2,False/0,Nil/0 ,True/0,c_1/0,c_2/1,c_3/0,c_4/1,c_5/0,c_6/1,c_7/0,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/0} - Obligation: innermost runtime complexity wrt. defined symbols {and#,even#,goal#,lte#,notEmpty#} and constructors {Cons ,False,Nil,True} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^1))