WORST_CASE(Omega(n^1),O(n^1)) * Step 1: Sum. WORST_CASE(Omega(n^1),O(n^1)) + Considered Problem: - Strict TRS: EVEN(Cons(z0,Cons(z1,z2))) -> c8(EVEN(z2)) EVEN(Cons(z0,Nil())) -> c7() EVEN(Nil()) -> c9() GOAL(z0,z1) -> c12(AND(lte(z0,z1),even(z0)),LTE(z0,z1)) GOAL(z0,z1) -> c13(AND(lte(z0,z1),even(z0)),EVEN(z0)) LTE(Cons(z0,z1),Cons(z2,z3)) -> c4(LTE(z1,z3)) LTE(Cons(z0,z1),Nil()) -> c5() LTE(Nil(),z0) -> c6() NOTEMPTY(Cons(z0,z1)) -> c10() NOTEMPTY(Nil()) -> c11() - Weak TRS: AND(False(),False()) -> c() AND(False(),True()) -> c2() AND(True(),False()) -> c1() AND(True(),True()) -> c3() and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() even(Cons(z0,Cons(z1,z2))) -> even(z2) even(Cons(z0,Nil())) -> False() even(Nil()) -> True() goal(z0,z1) -> and(lte(z0,z1),even(z0)) lte(Cons(z0,z1),Cons(z2,z3)) -> lte(z1,z3) lte(Cons(z0,z1),Nil()) -> False() lte(Nil(),z0) -> True() notEmpty(Cons(z0,z1)) -> True() notEmpty(Nil()) -> False() - 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/0,c1/0,c10/0,c11/0,c12/2,c13/2,c2/0,c3/0,c4/1,c5/0,c6/0,c7/0,c8/1,c9/0} - Obligation: innermost runtime complexity wrt. defined symbols {AND,EVEN,GOAL,LTE,NOTEMPTY,and,even,goal,lte ,notEmpty} and constructors {Cons,False,Nil,True,c,c1,c10,c11,c12,c13,c2,c3,c4,c5,c6,c7,c8,c9} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: EVEN(Cons(z0,Cons(z1,z2))) -> c8(EVEN(z2)) EVEN(Cons(z0,Nil())) -> c7() EVEN(Nil()) -> c9() GOAL(z0,z1) -> c12(AND(lte(z0,z1),even(z0)),LTE(z0,z1)) GOAL(z0,z1) -> c13(AND(lte(z0,z1),even(z0)),EVEN(z0)) LTE(Cons(z0,z1),Cons(z2,z3)) -> c4(LTE(z1,z3)) LTE(Cons(z0,z1),Nil()) -> c5() LTE(Nil(),z0) -> c6() NOTEMPTY(Cons(z0,z1)) -> c10() NOTEMPTY(Nil()) -> c11() - Weak TRS: AND(False(),False()) -> c() AND(False(),True()) -> c2() AND(True(),False()) -> c1() AND(True(),True()) -> c3() and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() even(Cons(z0,Cons(z1,z2))) -> even(z2) even(Cons(z0,Nil())) -> False() even(Nil()) -> True() goal(z0,z1) -> and(lte(z0,z1),even(z0)) lte(Cons(z0,z1),Cons(z2,z3)) -> lte(z1,z3) lte(Cons(z0,z1),Nil()) -> False() lte(Nil(),z0) -> True() notEmpty(Cons(z0,z1)) -> True() notEmpty(Nil()) -> False() - 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/0,c1/0,c10/0,c11/0,c12/2,c13/2,c2/0,c3/0,c4/1,c5/0,c6/0,c7/0,c8/1,c9/0} - Obligation: innermost runtime complexity wrt. defined symbols {AND,EVEN,GOAL,LTE,NOTEMPTY,and,even,goal,lte ,notEmpty} and constructors {Cons,False,Nil,True,c,c1,c10,c11,c12,c13,c2,c3,c4,c5,c6,c7,c8,c9} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:2: DecreasingLoops. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: EVEN(Cons(z0,Cons(z1,z2))) -> c8(EVEN(z2)) EVEN(Cons(z0,Nil())) -> c7() EVEN(Nil()) -> c9() GOAL(z0,z1) -> c12(AND(lte(z0,z1),even(z0)),LTE(z0,z1)) GOAL(z0,z1) -> c13(AND(lte(z0,z1),even(z0)),EVEN(z0)) LTE(Cons(z0,z1),Cons(z2,z3)) -> c4(LTE(z1,z3)) LTE(Cons(z0,z1),Nil()) -> c5() LTE(Nil(),z0) -> c6() NOTEMPTY(Cons(z0,z1)) -> c10() NOTEMPTY(Nil()) -> c11() - Weak TRS: AND(False(),False()) -> c() AND(False(),True()) -> c2() AND(True(),False()) -> c1() AND(True(),True()) -> c3() and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() even(Cons(z0,Cons(z1,z2))) -> even(z2) even(Cons(z0,Nil())) -> False() even(Nil()) -> True() goal(z0,z1) -> and(lte(z0,z1),even(z0)) lte(Cons(z0,z1),Cons(z2,z3)) -> lte(z1,z3) lte(Cons(z0,z1),Nil()) -> False() lte(Nil(),z0) -> True() notEmpty(Cons(z0,z1)) -> True() notEmpty(Nil()) -> False() - 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/0,c1/0,c10/0,c11/0,c12/2,c13/2,c2/0,c3/0,c4/1,c5/0,c6/0,c7/0,c8/1,c9/0} - Obligation: innermost runtime complexity wrt. defined symbols {AND,EVEN,GOAL,LTE,NOTEMPTY,and,even,goal,lte ,notEmpty} and constructors {Cons,False,Nil,True,c,c1,c10,c11,c12,c13,c2,c3,c4,c5,c6,c7,c8,c9} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: EVEN(z){z -> Cons(x,Cons(y,z))} = EVEN(Cons(x,Cons(y,z))) ->^+ c8(EVEN(z)) = C[EVEN(z) = EVEN(z){}] ** Step 1.b:1: DependencyPairs. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: EVEN(Cons(z0,Cons(z1,z2))) -> c8(EVEN(z2)) EVEN(Cons(z0,Nil())) -> c7() EVEN(Nil()) -> c9() GOAL(z0,z1) -> c12(AND(lte(z0,z1),even(z0)),LTE(z0,z1)) GOAL(z0,z1) -> c13(AND(lte(z0,z1),even(z0)),EVEN(z0)) LTE(Cons(z0,z1),Cons(z2,z3)) -> c4(LTE(z1,z3)) LTE(Cons(z0,z1),Nil()) -> c5() LTE(Nil(),z0) -> c6() NOTEMPTY(Cons(z0,z1)) -> c10() NOTEMPTY(Nil()) -> c11() - Weak TRS: AND(False(),False()) -> c() AND(False(),True()) -> c2() AND(True(),False()) -> c1() AND(True(),True()) -> c3() and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() even(Cons(z0,Cons(z1,z2))) -> even(z2) even(Cons(z0,Nil())) -> False() even(Nil()) -> True() goal(z0,z1) -> and(lte(z0,z1),even(z0)) lte(Cons(z0,z1),Cons(z2,z3)) -> lte(z1,z3) lte(Cons(z0,z1),Nil()) -> False() lte(Nil(),z0) -> True() notEmpty(Cons(z0,z1)) -> True() notEmpty(Nil()) -> False() - 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/0,c1/0,c10/0,c11/0,c12/2,c13/2,c2/0,c3/0,c4/1,c5/0,c6/0,c7/0,c8/1,c9/0} - Obligation: innermost runtime complexity wrt. defined symbols {AND,EVEN,GOAL,LTE,NOTEMPTY,and,even,goal,lte ,notEmpty} and constructors {Cons,False,Nil,True,c,c1,c10,c11,c12,c13,c2,c3,c4,c5,c6,c7,c8,c9} + Applied Processor: DependencyPairs {dpKind_ = WIDP} + Details: We add the following weak innermost dependency pairs: Strict DPs EVEN#(Cons(z0,Cons(z1,z2))) -> c_1(EVEN#(z2)) EVEN#(Cons(z0,Nil())) -> c_2() EVEN#(Nil()) -> c_3() GOAL#(z0,z1) -> c_4(AND#(lte(z0,z1),even(z0)),LTE#(z0,z1)) GOAL#(z0,z1) -> c_5(AND#(lte(z0,z1),even(z0)),EVEN#(z0)) LTE#(Cons(z0,z1),Cons(z2,z3)) -> c_6(LTE#(z1,z3)) LTE#(Cons(z0,z1),Nil()) -> c_7() LTE#(Nil(),z0) -> c_8() NOTEMPTY#(Cons(z0,z1)) -> c_9() NOTEMPTY#(Nil()) -> c_10() Weak DPs AND#(False(),False()) -> c_11() AND#(False(),True()) -> c_12() AND#(True(),False()) -> c_13() AND#(True(),True()) -> c_14() and#(False(),False()) -> c_15() and#(False(),True()) -> c_16() and#(True(),False()) -> c_17() and#(True(),True()) -> c_18() even#(Cons(z0,Cons(z1,z2))) -> c_19(even#(z2)) even#(Cons(z0,Nil())) -> c_20() even#(Nil()) -> c_21() goal#(z0,z1) -> c_22(and#(lte(z0,z1),even(z0))) lte#(Cons(z0,z1),Cons(z2,z3)) -> c_23(lte#(z1,z3)) lte#(Cons(z0,z1),Nil()) -> c_24() lte#(Nil(),z0) -> c_25() notEmpty#(Cons(z0,z1)) -> c_26() notEmpty#(Nil()) -> c_27() and mark the set of starting terms. ** Step 1.b:2: UsableRules. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: EVEN#(Cons(z0,Cons(z1,z2))) -> c_1(EVEN#(z2)) EVEN#(Cons(z0,Nil())) -> c_2() EVEN#(Nil()) -> c_3() GOAL#(z0,z1) -> c_4(AND#(lte(z0,z1),even(z0)),LTE#(z0,z1)) GOAL#(z0,z1) -> c_5(AND#(lte(z0,z1),even(z0)),EVEN#(z0)) LTE#(Cons(z0,z1),Cons(z2,z3)) -> c_6(LTE#(z1,z3)) LTE#(Cons(z0,z1),Nil()) -> c_7() LTE#(Nil(),z0) -> c_8() NOTEMPTY#(Cons(z0,z1)) -> c_9() NOTEMPTY#(Nil()) -> c_10() - Strict TRS: EVEN(Cons(z0,Cons(z1,z2))) -> c8(EVEN(z2)) EVEN(Cons(z0,Nil())) -> c7() EVEN(Nil()) -> c9() GOAL(z0,z1) -> c12(AND(lte(z0,z1),even(z0)),LTE(z0,z1)) GOAL(z0,z1) -> c13(AND(lte(z0,z1),even(z0)),EVEN(z0)) LTE(Cons(z0,z1),Cons(z2,z3)) -> c4(LTE(z1,z3)) LTE(Cons(z0,z1),Nil()) -> c5() LTE(Nil(),z0) -> c6() NOTEMPTY(Cons(z0,z1)) -> c10() NOTEMPTY(Nil()) -> c11() - Weak DPs: AND#(False(),False()) -> c_11() AND#(False(),True()) -> c_12() AND#(True(),False()) -> c_13() AND#(True(),True()) -> c_14() and#(False(),False()) -> c_15() and#(False(),True()) -> c_16() and#(True(),False()) -> c_17() and#(True(),True()) -> c_18() even#(Cons(z0,Cons(z1,z2))) -> c_19(even#(z2)) even#(Cons(z0,Nil())) -> c_20() even#(Nil()) -> c_21() goal#(z0,z1) -> c_22(and#(lte(z0,z1),even(z0))) lte#(Cons(z0,z1),Cons(z2,z3)) -> c_23(lte#(z1,z3)) lte#(Cons(z0,z1),Nil()) -> c_24() lte#(Nil(),z0) -> c_25() notEmpty#(Cons(z0,z1)) -> c_26() notEmpty#(Nil()) -> c_27() - Weak TRS: AND(False(),False()) -> c() AND(False(),True()) -> c2() AND(True(),False()) -> c1() AND(True(),True()) -> c3() and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() even(Cons(z0,Cons(z1,z2))) -> even(z2) even(Cons(z0,Nil())) -> False() even(Nil()) -> True() goal(z0,z1) -> and(lte(z0,z1),even(z0)) lte(Cons(z0,z1),Cons(z2,z3)) -> lte(z1,z3) lte(Cons(z0,z1),Nil()) -> False() lte(Nil(),z0) -> True() notEmpty(Cons(z0,z1)) -> True() notEmpty(Nil()) -> False() - Signature: {AND/2,EVEN/1,GOAL/2,LTE/2,NOTEMPTY/1,and/2,even/1,goal/2,lte/2,notEmpty/1,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/0,c1/0,c10/0,c11/0 ,c12/2,c13/2,c2/0,c3/0,c4/1,c5/0,c6/0,c7/0,c8/1,c9/0,c_1/1,c_2/0,c_3/0,c_4/2,c_5/2,c_6/1,c_7/0,c_8/0,c_9/0 ,c_10/0,c_11/0,c_12/0,c_13/0,c_14/0,c_15/0,c_16/0,c_17/0,c_18/0,c_19/1,c_20/0,c_21/0,c_22/1,c_23/1,c_24/0 ,c_25/0,c_26/0,c_27/0} - Obligation: innermost runtime complexity wrt. defined symbols {AND#,EVEN#,GOAL#,LTE#,NOTEMPTY#,and#,even#,goal#,lte# ,notEmpty#} and constructors {Cons,False,Nil,True,c,c1,c10,c11,c12,c13,c2,c3,c4,c5,c6,c7,c8,c9} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: even(Cons(z0,Cons(z1,z2))) -> even(z2) even(Cons(z0,Nil())) -> False() even(Nil()) -> True() lte(Cons(z0,z1),Cons(z2,z3)) -> lte(z1,z3) lte(Cons(z0,z1),Nil()) -> False() lte(Nil(),z0) -> True() AND#(False(),False()) -> c_11() AND#(False(),True()) -> c_12() AND#(True(),False()) -> c_13() AND#(True(),True()) -> c_14() EVEN#(Cons(z0,Cons(z1,z2))) -> c_1(EVEN#(z2)) EVEN#(Cons(z0,Nil())) -> c_2() EVEN#(Nil()) -> c_3() GOAL#(z0,z1) -> c_4(AND#(lte(z0,z1),even(z0)),LTE#(z0,z1)) GOAL#(z0,z1) -> c_5(AND#(lte(z0,z1),even(z0)),EVEN#(z0)) LTE#(Cons(z0,z1),Cons(z2,z3)) -> c_6(LTE#(z1,z3)) LTE#(Cons(z0,z1),Nil()) -> c_7() LTE#(Nil(),z0) -> c_8() NOTEMPTY#(Cons(z0,z1)) -> c_9() NOTEMPTY#(Nil()) -> c_10() and#(False(),False()) -> c_15() and#(False(),True()) -> c_16() and#(True(),False()) -> c_17() and#(True(),True()) -> c_18() even#(Cons(z0,Cons(z1,z2))) -> c_19(even#(z2)) even#(Cons(z0,Nil())) -> c_20() even#(Nil()) -> c_21() goal#(z0,z1) -> c_22(and#(lte(z0,z1),even(z0))) lte#(Cons(z0,z1),Cons(z2,z3)) -> c_23(lte#(z1,z3)) lte#(Cons(z0,z1),Nil()) -> c_24() lte#(Nil(),z0) -> c_25() notEmpty#(Cons(z0,z1)) -> c_26() notEmpty#(Nil()) -> c_27() ** Step 1.b:3: PredecessorEstimation. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: EVEN#(Cons(z0,Cons(z1,z2))) -> c_1(EVEN#(z2)) EVEN#(Cons(z0,Nil())) -> c_2() EVEN#(Nil()) -> c_3() GOAL#(z0,z1) -> c_4(AND#(lte(z0,z1),even(z0)),LTE#(z0,z1)) GOAL#(z0,z1) -> c_5(AND#(lte(z0,z1),even(z0)),EVEN#(z0)) LTE#(Cons(z0,z1),Cons(z2,z3)) -> c_6(LTE#(z1,z3)) LTE#(Cons(z0,z1),Nil()) -> c_7() LTE#(Nil(),z0) -> c_8() NOTEMPTY#(Cons(z0,z1)) -> c_9() NOTEMPTY#(Nil()) -> c_10() - Weak DPs: AND#(False(),False()) -> c_11() AND#(False(),True()) -> c_12() AND#(True(),False()) -> c_13() AND#(True(),True()) -> c_14() and#(False(),False()) -> c_15() and#(False(),True()) -> c_16() and#(True(),False()) -> c_17() and#(True(),True()) -> c_18() even#(Cons(z0,Cons(z1,z2))) -> c_19(even#(z2)) even#(Cons(z0,Nil())) -> c_20() even#(Nil()) -> c_21() goal#(z0,z1) -> c_22(and#(lte(z0,z1),even(z0))) lte#(Cons(z0,z1),Cons(z2,z3)) -> c_23(lte#(z1,z3)) lte#(Cons(z0,z1),Nil()) -> c_24() lte#(Nil(),z0) -> c_25() notEmpty#(Cons(z0,z1)) -> c_26() notEmpty#(Nil()) -> c_27() - Weak TRS: even(Cons(z0,Cons(z1,z2))) -> even(z2) even(Cons(z0,Nil())) -> False() even(Nil()) -> True() lte(Cons(z0,z1),Cons(z2,z3)) -> lte(z1,z3) lte(Cons(z0,z1),Nil()) -> False() lte(Nil(),z0) -> True() - Signature: {AND/2,EVEN/1,GOAL/2,LTE/2,NOTEMPTY/1,and/2,even/1,goal/2,lte/2,notEmpty/1,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/0,c1/0,c10/0,c11/0 ,c12/2,c13/2,c2/0,c3/0,c4/1,c5/0,c6/0,c7/0,c8/1,c9/0,c_1/1,c_2/0,c_3/0,c_4/2,c_5/2,c_6/1,c_7/0,c_8/0,c_9/0 ,c_10/0,c_11/0,c_12/0,c_13/0,c_14/0,c_15/0,c_16/0,c_17/0,c_18/0,c_19/1,c_20/0,c_21/0,c_22/1,c_23/1,c_24/0 ,c_25/0,c_26/0,c_27/0} - Obligation: innermost runtime complexity wrt. defined symbols {AND#,EVEN#,GOAL#,LTE#,NOTEMPTY#,and#,even#,goal#,lte# ,notEmpty#} and constructors {Cons,False,Nil,True,c,c1,c10,c11,c12,c13,c2,c3,c4,c5,c6,c7,c8,c9} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {2,3,7,8,9,10} by application of Pre({2,3,7,8,9,10}) = {1,4,5,6}. Here rules are labelled as follows: 1: EVEN#(Cons(z0,Cons(z1,z2))) -> c_1(EVEN#(z2)) 2: EVEN#(Cons(z0,Nil())) -> c_2() 3: EVEN#(Nil()) -> c_3() 4: GOAL#(z0,z1) -> c_4(AND#(lte(z0,z1),even(z0)),LTE#(z0,z1)) 5: GOAL#(z0,z1) -> c_5(AND#(lte(z0,z1),even(z0)),EVEN#(z0)) 6: LTE#(Cons(z0,z1),Cons(z2,z3)) -> c_6(LTE#(z1,z3)) 7: LTE#(Cons(z0,z1),Nil()) -> c_7() 8: LTE#(Nil(),z0) -> c_8() 9: NOTEMPTY#(Cons(z0,z1)) -> c_9() 10: NOTEMPTY#(Nil()) -> c_10() 11: AND#(False(),False()) -> c_11() 12: AND#(False(),True()) -> c_12() 13: AND#(True(),False()) -> c_13() 14: AND#(True(),True()) -> c_14() 15: and#(False(),False()) -> c_15() 16: and#(False(),True()) -> c_16() 17: and#(True(),False()) -> c_17() 18: and#(True(),True()) -> c_18() 19: even#(Cons(z0,Cons(z1,z2))) -> c_19(even#(z2)) 20: even#(Cons(z0,Nil())) -> c_20() 21: even#(Nil()) -> c_21() 22: goal#(z0,z1) -> c_22(and#(lte(z0,z1),even(z0))) 23: lte#(Cons(z0,z1),Cons(z2,z3)) -> c_23(lte#(z1,z3)) 24: lte#(Cons(z0,z1),Nil()) -> c_24() 25: lte#(Nil(),z0) -> c_25() 26: notEmpty#(Cons(z0,z1)) -> c_26() 27: notEmpty#(Nil()) -> c_27() ** Step 1.b:4: RemoveWeakSuffixes. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: EVEN#(Cons(z0,Cons(z1,z2))) -> c_1(EVEN#(z2)) GOAL#(z0,z1) -> c_4(AND#(lte(z0,z1),even(z0)),LTE#(z0,z1)) GOAL#(z0,z1) -> c_5(AND#(lte(z0,z1),even(z0)),EVEN#(z0)) LTE#(Cons(z0,z1),Cons(z2,z3)) -> c_6(LTE#(z1,z3)) - Weak DPs: AND#(False(),False()) -> c_11() AND#(False(),True()) -> c_12() AND#(True(),False()) -> c_13() AND#(True(),True()) -> c_14() EVEN#(Cons(z0,Nil())) -> c_2() EVEN#(Nil()) -> c_3() LTE#(Cons(z0,z1),Nil()) -> c_7() LTE#(Nil(),z0) -> c_8() NOTEMPTY#(Cons(z0,z1)) -> c_9() NOTEMPTY#(Nil()) -> c_10() and#(False(),False()) -> c_15() and#(False(),True()) -> c_16() and#(True(),False()) -> c_17() and#(True(),True()) -> c_18() even#(Cons(z0,Cons(z1,z2))) -> c_19(even#(z2)) even#(Cons(z0,Nil())) -> c_20() even#(Nil()) -> c_21() goal#(z0,z1) -> c_22(and#(lte(z0,z1),even(z0))) lte#(Cons(z0,z1),Cons(z2,z3)) -> c_23(lte#(z1,z3)) lte#(Cons(z0,z1),Nil()) -> c_24() lte#(Nil(),z0) -> c_25() notEmpty#(Cons(z0,z1)) -> c_26() notEmpty#(Nil()) -> c_27() - Weak TRS: even(Cons(z0,Cons(z1,z2))) -> even(z2) even(Cons(z0,Nil())) -> False() even(Nil()) -> True() lte(Cons(z0,z1),Cons(z2,z3)) -> lte(z1,z3) lte(Cons(z0,z1),Nil()) -> False() lte(Nil(),z0) -> True() - Signature: {AND/2,EVEN/1,GOAL/2,LTE/2,NOTEMPTY/1,and/2,even/1,goal/2,lte/2,notEmpty/1,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/0,c1/0,c10/0,c11/0 ,c12/2,c13/2,c2/0,c3/0,c4/1,c5/0,c6/0,c7/0,c8/1,c9/0,c_1/1,c_2/0,c_3/0,c_4/2,c_5/2,c_6/1,c_7/0,c_8/0,c_9/0 ,c_10/0,c_11/0,c_12/0,c_13/0,c_14/0,c_15/0,c_16/0,c_17/0,c_18/0,c_19/1,c_20/0,c_21/0,c_22/1,c_23/1,c_24/0 ,c_25/0,c_26/0,c_27/0} - Obligation: innermost runtime complexity wrt. defined symbols {AND#,EVEN#,GOAL#,LTE#,NOTEMPTY#,and#,even#,goal#,lte# ,notEmpty#} and constructors {Cons,False,Nil,True,c,c1,c10,c11,c12,c13,c2,c3,c4,c5,c6,c7,c8,c9} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:EVEN#(Cons(z0,Cons(z1,z2))) -> c_1(EVEN#(z2)) -->_1 EVEN#(Nil()) -> c_3():10 -->_1 EVEN#(Cons(z0,Nil())) -> c_2():9 -->_1 EVEN#(Cons(z0,Cons(z1,z2))) -> c_1(EVEN#(z2)):1 2:S:GOAL#(z0,z1) -> c_4(AND#(lte(z0,z1),even(z0)),LTE#(z0,z1)) -->_2 LTE#(Cons(z0,z1),Cons(z2,z3)) -> c_6(LTE#(z1,z3)):4 -->_2 LTE#(Nil(),z0) -> c_8():12 -->_2 LTE#(Cons(z0,z1),Nil()) -> c_7():11 -->_1 AND#(True(),True()) -> c_14():8 -->_1 AND#(True(),False()) -> c_13():7 -->_1 AND#(False(),True()) -> c_12():6 -->_1 AND#(False(),False()) -> c_11():5 3:S:GOAL#(z0,z1) -> c_5(AND#(lte(z0,z1),even(z0)),EVEN#(z0)) -->_2 EVEN#(Nil()) -> c_3():10 -->_2 EVEN#(Cons(z0,Nil())) -> c_2():9 -->_1 AND#(True(),True()) -> c_14():8 -->_1 AND#(True(),False()) -> c_13():7 -->_1 AND#(False(),True()) -> c_12():6 -->_1 AND#(False(),False()) -> c_11():5 -->_2 EVEN#(Cons(z0,Cons(z1,z2))) -> c_1(EVEN#(z2)):1 4:S:LTE#(Cons(z0,z1),Cons(z2,z3)) -> c_6(LTE#(z1,z3)) -->_1 LTE#(Nil(),z0) -> c_8():12 -->_1 LTE#(Cons(z0,z1),Nil()) -> c_7():11 -->_1 LTE#(Cons(z0,z1),Cons(z2,z3)) -> c_6(LTE#(z1,z3)):4 5:W:AND#(False(),False()) -> c_11() 6:W:AND#(False(),True()) -> c_12() 7:W:AND#(True(),False()) -> c_13() 8:W:AND#(True(),True()) -> c_14() 9:W:EVEN#(Cons(z0,Nil())) -> c_2() 10:W:EVEN#(Nil()) -> c_3() 11:W:LTE#(Cons(z0,z1),Nil()) -> c_7() 12:W:LTE#(Nil(),z0) -> c_8() 13:W:NOTEMPTY#(Cons(z0,z1)) -> c_9() 14:W:NOTEMPTY#(Nil()) -> c_10() 15:W:and#(False(),False()) -> c_15() 16:W:and#(False(),True()) -> c_16() 17:W:and#(True(),False()) -> c_17() 18:W:and#(True(),True()) -> c_18() 19:W:even#(Cons(z0,Cons(z1,z2))) -> c_19(even#(z2)) -->_1 even#(Nil()) -> c_21():21 -->_1 even#(Cons(z0,Nil())) -> c_20():20 -->_1 even#(Cons(z0,Cons(z1,z2))) -> c_19(even#(z2)):19 20:W:even#(Cons(z0,Nil())) -> c_20() 21:W:even#(Nil()) -> c_21() 22:W:goal#(z0,z1) -> c_22(and#(lte(z0,z1),even(z0))) -->_1 and#(True(),True()) -> c_18():18 -->_1 and#(True(),False()) -> c_17():17 -->_1 and#(False(),True()) -> c_16():16 -->_1 and#(False(),False()) -> c_15():15 23:W:lte#(Cons(z0,z1),Cons(z2,z3)) -> c_23(lte#(z1,z3)) -->_1 lte#(Nil(),z0) -> c_25():25 -->_1 lte#(Cons(z0,z1),Nil()) -> c_24():24 -->_1 lte#(Cons(z0,z1),Cons(z2,z3)) -> c_23(lte#(z1,z3)):23 24:W:lte#(Cons(z0,z1),Nil()) -> c_24() 25:W:lte#(Nil(),z0) -> c_25() 26:W:notEmpty#(Cons(z0,z1)) -> c_26() 27:W:notEmpty#(Nil()) -> c_27() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 27: notEmpty#(Nil()) -> c_27() 26: notEmpty#(Cons(z0,z1)) -> c_26() 23: lte#(Cons(z0,z1),Cons(z2,z3)) -> c_23(lte#(z1,z3)) 24: lte#(Cons(z0,z1),Nil()) -> c_24() 25: lte#(Nil(),z0) -> c_25() 22: goal#(z0,z1) -> c_22(and#(lte(z0,z1),even(z0))) 19: even#(Cons(z0,Cons(z1,z2))) -> c_19(even#(z2)) 20: even#(Cons(z0,Nil())) -> c_20() 21: even#(Nil()) -> c_21() 18: and#(True(),True()) -> c_18() 17: and#(True(),False()) -> c_17() 16: and#(False(),True()) -> c_16() 15: and#(False(),False()) -> c_15() 14: NOTEMPTY#(Nil()) -> c_10() 13: NOTEMPTY#(Cons(z0,z1)) -> c_9() 5: AND#(False(),False()) -> c_11() 6: AND#(False(),True()) -> c_12() 7: AND#(True(),False()) -> c_13() 8: AND#(True(),True()) -> c_14() 11: LTE#(Cons(z0,z1),Nil()) -> c_7() 12: LTE#(Nil(),z0) -> c_8() 9: EVEN#(Cons(z0,Nil())) -> c_2() 10: EVEN#(Nil()) -> c_3() ** Step 1.b:5: SimplifyRHS. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: EVEN#(Cons(z0,Cons(z1,z2))) -> c_1(EVEN#(z2)) GOAL#(z0,z1) -> c_4(AND#(lte(z0,z1),even(z0)),LTE#(z0,z1)) GOAL#(z0,z1) -> c_5(AND#(lte(z0,z1),even(z0)),EVEN#(z0)) LTE#(Cons(z0,z1),Cons(z2,z3)) -> c_6(LTE#(z1,z3)) - Weak TRS: even(Cons(z0,Cons(z1,z2))) -> even(z2) even(Cons(z0,Nil())) -> False() even(Nil()) -> True() lte(Cons(z0,z1),Cons(z2,z3)) -> lte(z1,z3) lte(Cons(z0,z1),Nil()) -> False() lte(Nil(),z0) -> True() - Signature: {AND/2,EVEN/1,GOAL/2,LTE/2,NOTEMPTY/1,and/2,even/1,goal/2,lte/2,notEmpty/1,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/0,c1/0,c10/0,c11/0 ,c12/2,c13/2,c2/0,c3/0,c4/1,c5/0,c6/0,c7/0,c8/1,c9/0,c_1/1,c_2/0,c_3/0,c_4/2,c_5/2,c_6/1,c_7/0,c_8/0,c_9/0 ,c_10/0,c_11/0,c_12/0,c_13/0,c_14/0,c_15/0,c_16/0,c_17/0,c_18/0,c_19/1,c_20/0,c_21/0,c_22/1,c_23/1,c_24/0 ,c_25/0,c_26/0,c_27/0} - Obligation: innermost runtime complexity wrt. defined symbols {AND#,EVEN#,GOAL#,LTE#,NOTEMPTY#,and#,even#,goal#,lte# ,notEmpty#} and constructors {Cons,False,Nil,True,c,c1,c10,c11,c12,c13,c2,c3,c4,c5,c6,c7,c8,c9} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:EVEN#(Cons(z0,Cons(z1,z2))) -> c_1(EVEN#(z2)) -->_1 EVEN#(Cons(z0,Cons(z1,z2))) -> c_1(EVEN#(z2)):1 2:S:GOAL#(z0,z1) -> c_4(AND#(lte(z0,z1),even(z0)),LTE#(z0,z1)) -->_2 LTE#(Cons(z0,z1),Cons(z2,z3)) -> c_6(LTE#(z1,z3)):4 3:S:GOAL#(z0,z1) -> c_5(AND#(lte(z0,z1),even(z0)),EVEN#(z0)) -->_2 EVEN#(Cons(z0,Cons(z1,z2))) -> c_1(EVEN#(z2)):1 4:S:LTE#(Cons(z0,z1),Cons(z2,z3)) -> c_6(LTE#(z1,z3)) -->_1 LTE#(Cons(z0,z1),Cons(z2,z3)) -> c_6(LTE#(z1,z3)):4 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: GOAL#(z0,z1) -> c_4(LTE#(z0,z1)) GOAL#(z0,z1) -> c_5(EVEN#(z0)) ** Step 1.b:6: UsableRules. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: EVEN#(Cons(z0,Cons(z1,z2))) -> c_1(EVEN#(z2)) GOAL#(z0,z1) -> c_4(LTE#(z0,z1)) GOAL#(z0,z1) -> c_5(EVEN#(z0)) LTE#(Cons(z0,z1),Cons(z2,z3)) -> c_6(LTE#(z1,z3)) - Weak TRS: even(Cons(z0,Cons(z1,z2))) -> even(z2) even(Cons(z0,Nil())) -> False() even(Nil()) -> True() lte(Cons(z0,z1),Cons(z2,z3)) -> lte(z1,z3) lte(Cons(z0,z1),Nil()) -> False() lte(Nil(),z0) -> True() - Signature: {AND/2,EVEN/1,GOAL/2,LTE/2,NOTEMPTY/1,and/2,even/1,goal/2,lte/2,notEmpty/1,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/0,c1/0,c10/0,c11/0 ,c12/2,c13/2,c2/0,c3/0,c4/1,c5/0,c6/0,c7/0,c8/1,c9/0,c_1/1,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/0,c_8/0,c_9/0 ,c_10/0,c_11/0,c_12/0,c_13/0,c_14/0,c_15/0,c_16/0,c_17/0,c_18/0,c_19/1,c_20/0,c_21/0,c_22/1,c_23/1,c_24/0 ,c_25/0,c_26/0,c_27/0} - Obligation: innermost runtime complexity wrt. defined symbols {AND#,EVEN#,GOAL#,LTE#,NOTEMPTY#,and#,even#,goal#,lte# ,notEmpty#} and constructors {Cons,False,Nil,True,c,c1,c10,c11,c12,c13,c2,c3,c4,c5,c6,c7,c8,c9} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: EVEN#(Cons(z0,Cons(z1,z2))) -> c_1(EVEN#(z2)) GOAL#(z0,z1) -> c_4(LTE#(z0,z1)) GOAL#(z0,z1) -> c_5(EVEN#(z0)) LTE#(Cons(z0,z1),Cons(z2,z3)) -> c_6(LTE#(z1,z3)) ** Step 1.b:7: RemoveHeads. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: EVEN#(Cons(z0,Cons(z1,z2))) -> c_1(EVEN#(z2)) GOAL#(z0,z1) -> c_4(LTE#(z0,z1)) GOAL#(z0,z1) -> c_5(EVEN#(z0)) LTE#(Cons(z0,z1),Cons(z2,z3)) -> c_6(LTE#(z1,z3)) - Signature: {AND/2,EVEN/1,GOAL/2,LTE/2,NOTEMPTY/1,and/2,even/1,goal/2,lte/2,notEmpty/1,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/0,c1/0,c10/0,c11/0 ,c12/2,c13/2,c2/0,c3/0,c4/1,c5/0,c6/0,c7/0,c8/1,c9/0,c_1/1,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/0,c_8/0,c_9/0 ,c_10/0,c_11/0,c_12/0,c_13/0,c_14/0,c_15/0,c_16/0,c_17/0,c_18/0,c_19/1,c_20/0,c_21/0,c_22/1,c_23/1,c_24/0 ,c_25/0,c_26/0,c_27/0} - Obligation: innermost runtime complexity wrt. defined symbols {AND#,EVEN#,GOAL#,LTE#,NOTEMPTY#,and#,even#,goal#,lte# ,notEmpty#} and constructors {Cons,False,Nil,True,c,c1,c10,c11,c12,c13,c2,c3,c4,c5,c6,c7,c8,c9} + Applied Processor: RemoveHeads + Details: Consider the dependency graph 1:S:EVEN#(Cons(z0,Cons(z1,z2))) -> c_1(EVEN#(z2)) -->_1 EVEN#(Cons(z0,Cons(z1,z2))) -> c_1(EVEN#(z2)):1 2:S:GOAL#(z0,z1) -> c_4(LTE#(z0,z1)) -->_1 LTE#(Cons(z0,z1),Cons(z2,z3)) -> c_6(LTE#(z1,z3)):4 3:S:GOAL#(z0,z1) -> c_5(EVEN#(z0)) -->_1 EVEN#(Cons(z0,Cons(z1,z2))) -> c_1(EVEN#(z2)):1 4:S:LTE#(Cons(z0,z1),Cons(z2,z3)) -> c_6(LTE#(z1,z3)) -->_1 LTE#(Cons(z0,z1),Cons(z2,z3)) -> c_6(LTE#(z1,z3)):4 Following roots of the dependency graph are removed, as the considered set of starting terms is closed under reduction with respect to these rules (modulo compound contexts). [(2,GOAL#(z0,z1) -> c_4(LTE#(z0,z1))),(3,GOAL#(z0,z1) -> c_5(EVEN#(z0)))] ** Step 1.b:8: Decompose. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: EVEN#(Cons(z0,Cons(z1,z2))) -> c_1(EVEN#(z2)) LTE#(Cons(z0,z1),Cons(z2,z3)) -> c_6(LTE#(z1,z3)) - Signature: {AND/2,EVEN/1,GOAL/2,LTE/2,NOTEMPTY/1,and/2,even/1,goal/2,lte/2,notEmpty/1,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/0,c1/0,c10/0,c11/0 ,c12/2,c13/2,c2/0,c3/0,c4/1,c5/0,c6/0,c7/0,c8/1,c9/0,c_1/1,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/0,c_8/0,c_9/0 ,c_10/0,c_11/0,c_12/0,c_13/0,c_14/0,c_15/0,c_16/0,c_17/0,c_18/0,c_19/1,c_20/0,c_21/0,c_22/1,c_23/1,c_24/0 ,c_25/0,c_26/0,c_27/0} - Obligation: innermost runtime complexity wrt. defined symbols {AND#,EVEN#,GOAL#,LTE#,NOTEMPTY#,and#,even#,goal#,lte# ,notEmpty#} and constructors {Cons,False,Nil,True,c,c1,c10,c11,c12,c13,c2,c3,c4,c5,c6,c7,c8,c9} + 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(z0,Cons(z1,z2))) -> c_1(EVEN#(z2)) - Weak DPs: LTE#(Cons(z0,z1),Cons(z2,z3)) -> c_6(LTE#(z1,z3)) - Signature: {AND/2,EVEN/1,GOAL/2,LTE/2,NOTEMPTY/1,and/2,even/1,goal/2,lte/2,notEmpty/1,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/0,c1/0,c10/0 ,c11/0,c12/2,c13/2,c2/0,c3/0,c4/1,c5/0,c6/0,c7/0,c8/1,c9/0,c_1/1,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/0,c_8/0 ,c_9/0,c_10/0,c_11/0,c_12/0,c_13/0,c_14/0,c_15/0,c_16/0,c_17/0,c_18/0,c_19/1,c_20/0,c_21/0,c_22/1,c_23/1 ,c_24/0,c_25/0,c_26/0,c_27/0} - Obligation: innermost runtime complexity wrt. defined symbols {AND#,EVEN#,GOAL#,LTE#,NOTEMPTY#,and#,even#,goal#,lte# ,notEmpty#} and constructors {Cons,False,Nil,True,c,c1,c10,c11,c12,c13,c2,c3,c4,c5,c6,c7,c8,c9} Problem (S) - Strict DPs: LTE#(Cons(z0,z1),Cons(z2,z3)) -> c_6(LTE#(z1,z3)) - Weak DPs: EVEN#(Cons(z0,Cons(z1,z2))) -> c_1(EVEN#(z2)) - Signature: {AND/2,EVEN/1,GOAL/2,LTE/2,NOTEMPTY/1,and/2,even/1,goal/2,lte/2,notEmpty/1,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/0,c1/0,c10/0 ,c11/0,c12/2,c13/2,c2/0,c3/0,c4/1,c5/0,c6/0,c7/0,c8/1,c9/0,c_1/1,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/0,c_8/0 ,c_9/0,c_10/0,c_11/0,c_12/0,c_13/0,c_14/0,c_15/0,c_16/0,c_17/0,c_18/0,c_19/1,c_20/0,c_21/0,c_22/1,c_23/1 ,c_24/0,c_25/0,c_26/0,c_27/0} - Obligation: innermost runtime complexity wrt. defined symbols {AND#,EVEN#,GOAL#,LTE#,NOTEMPTY#,and#,even#,goal#,lte# ,notEmpty#} and constructors {Cons,False,Nil,True,c,c1,c10,c11,c12,c13,c2,c3,c4,c5,c6,c7,c8,c9} *** Step 1.b:8.a:1: RemoveWeakSuffixes. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: EVEN#(Cons(z0,Cons(z1,z2))) -> c_1(EVEN#(z2)) - Weak DPs: LTE#(Cons(z0,z1),Cons(z2,z3)) -> c_6(LTE#(z1,z3)) - Signature: {AND/2,EVEN/1,GOAL/2,LTE/2,NOTEMPTY/1,and/2,even/1,goal/2,lte/2,notEmpty/1,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/0,c1/0,c10/0,c11/0 ,c12/2,c13/2,c2/0,c3/0,c4/1,c5/0,c6/0,c7/0,c8/1,c9/0,c_1/1,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/0,c_8/0,c_9/0 ,c_10/0,c_11/0,c_12/0,c_13/0,c_14/0,c_15/0,c_16/0,c_17/0,c_18/0,c_19/1,c_20/0,c_21/0,c_22/1,c_23/1,c_24/0 ,c_25/0,c_26/0,c_27/0} - Obligation: innermost runtime complexity wrt. defined symbols {AND#,EVEN#,GOAL#,LTE#,NOTEMPTY#,and#,even#,goal#,lte# ,notEmpty#} and constructors {Cons,False,Nil,True,c,c1,c10,c11,c12,c13,c2,c3,c4,c5,c6,c7,c8,c9} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:EVEN#(Cons(z0,Cons(z1,z2))) -> c_1(EVEN#(z2)) -->_1 EVEN#(Cons(z0,Cons(z1,z2))) -> c_1(EVEN#(z2)):1 4:W:LTE#(Cons(z0,z1),Cons(z2,z3)) -> c_6(LTE#(z1,z3)) -->_1 LTE#(Cons(z0,z1),Cons(z2,z3)) -> c_6(LTE#(z1,z3)):4 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 4: LTE#(Cons(z0,z1),Cons(z2,z3)) -> c_6(LTE#(z1,z3)) *** Step 1.b:8.a:2: PredecessorEstimationCP. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: EVEN#(Cons(z0,Cons(z1,z2))) -> c_1(EVEN#(z2)) - Signature: {AND/2,EVEN/1,GOAL/2,LTE/2,NOTEMPTY/1,and/2,even/1,goal/2,lte/2,notEmpty/1,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/0,c1/0,c10/0,c11/0 ,c12/2,c13/2,c2/0,c3/0,c4/1,c5/0,c6/0,c7/0,c8/1,c9/0,c_1/1,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/0,c_8/0,c_9/0 ,c_10/0,c_11/0,c_12/0,c_13/0,c_14/0,c_15/0,c_16/0,c_17/0,c_18/0,c_19/1,c_20/0,c_21/0,c_22/1,c_23/1,c_24/0 ,c_25/0,c_26/0,c_27/0} - Obligation: innermost runtime complexity wrt. defined symbols {AND#,EVEN#,GOAL#,LTE#,NOTEMPTY#,and#,even#,goal#,lte# ,notEmpty#} and constructors {Cons,False,Nil,True,c,c1,c10,c11,c12,c13,c2,c3,c4,c5,c6,c7,c8,c9} + 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(z0,Cons(z1,z2))) -> c_1(EVEN#(z2)) The strictly oriented rules are moved into the weak component. **** Step 1.b:8.a:2.a:1: NaturalMI. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: EVEN#(Cons(z0,Cons(z1,z2))) -> c_1(EVEN#(z2)) - Signature: {AND/2,EVEN/1,GOAL/2,LTE/2,NOTEMPTY/1,and/2,even/1,goal/2,lte/2,notEmpty/1,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/0,c1/0,c10/0,c11/0 ,c12/2,c13/2,c2/0,c3/0,c4/1,c5/0,c6/0,c7/0,c8/1,c9/0,c_1/1,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/0,c_8/0,c_9/0 ,c_10/0,c_11/0,c_12/0,c_13/0,c_14/0,c_15/0,c_16/0,c_17/0,c_18/0,c_19/1,c_20/0,c_21/0,c_22/1,c_23/1,c_24/0 ,c_25/0,c_26/0,c_27/0} - Obligation: innermost runtime complexity wrt. defined symbols {AND#,EVEN#,GOAL#,LTE#,NOTEMPTY#,and#,even#,goal#,lte# ,notEmpty#} and constructors {Cons,False,Nil,True,c,c1,c10,c11,c12,c13,c2,c3,c4,c5,c6,c7,c8,c9} + 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_1) = {1} Following symbols are considered usable: {AND#,EVEN#,GOAL#,LTE#,NOTEMPTY#,and#,even#,goal#,lte#,notEmpty#} TcT has computed the following interpretation: p(AND) = [0] p(Cons) = [1] x2 + [9] p(EVEN) = [0] p(False) = [0] p(GOAL) = [1] x1 + [0] p(LTE) = [0] p(NOTEMPTY) = [0] p(Nil) = [0] p(True) = [0] p(and) = [0] p(c) = [0] p(c1) = [0] p(c10) = [0] p(c11) = [0] p(c12) = [1] x1 + [1] x2 + [0] p(c13) = [1] x1 + [1] x2 + [0] p(c2) = [0] p(c3) = [0] p(c4) = [1] x1 + [0] p(c5) = [0] p(c6) = [0] p(c7) = [0] p(c8) = [1] x1 + [0] p(c9) = [0] p(even) = [0] p(goal) = [0] p(lte) = [0] p(notEmpty) = [0] p(AND#) = [0] p(EVEN#) = [1] x1 + [9] p(GOAL#) = [0] p(LTE#) = [0] p(NOTEMPTY#) = [0] p(and#) = [0] p(even#) = [0] p(goal#) = [0] p(lte#) = [0] p(notEmpty#) = [0] p(c_1) = [1] x1 + [10] p(c_2) = [0] p(c_3) = [0] p(c_4) = [1] x1 + [0] p(c_5) = [4] x1 + [0] p(c_6) = [2] x1 + [0] p(c_7) = [0] p(c_8) = [0] p(c_9) = [0] p(c_10) = [0] p(c_11) = [0] p(c_12) = [0] p(c_13) = [0] p(c_14) = [0] p(c_15) = [0] p(c_16) = [0] p(c_17) = [0] p(c_18) = [0] p(c_19) = [2] x1 + [0] p(c_20) = [0] p(c_21) = [0] p(c_22) = [2] x1 + [0] p(c_23) = [1] x1 + [0] p(c_24) = [8] p(c_25) = [0] p(c_26) = [4] p(c_27) = [1] Following rules are strictly oriented: EVEN#(Cons(z0,Cons(z1,z2))) = [1] z2 + [27] > [1] z2 + [19] = c_1(EVEN#(z2)) Following rules are (at-least) weakly oriented: **** Step 1.b:8.a:2.a:2: Assumption. WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: EVEN#(Cons(z0,Cons(z1,z2))) -> c_1(EVEN#(z2)) - Signature: {AND/2,EVEN/1,GOAL/2,LTE/2,NOTEMPTY/1,and/2,even/1,goal/2,lte/2,notEmpty/1,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/0,c1/0,c10/0,c11/0 ,c12/2,c13/2,c2/0,c3/0,c4/1,c5/0,c6/0,c7/0,c8/1,c9/0,c_1/1,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/0,c_8/0,c_9/0 ,c_10/0,c_11/0,c_12/0,c_13/0,c_14/0,c_15/0,c_16/0,c_17/0,c_18/0,c_19/1,c_20/0,c_21/0,c_22/1,c_23/1,c_24/0 ,c_25/0,c_26/0,c_27/0} - Obligation: innermost runtime complexity wrt. defined symbols {AND#,EVEN#,GOAL#,LTE#,NOTEMPTY#,and#,even#,goal#,lte# ,notEmpty#} and constructors {Cons,False,Nil,True,c,c1,c10,c11,c12,c13,c2,c3,c4,c5,c6,c7,c8,c9} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown, timeBCUB = Unknown, timeBCLB = Unknown}} + Details: () **** Step 1.b:8.a:2.b:1: RemoveWeakSuffixes. WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: EVEN#(Cons(z0,Cons(z1,z2))) -> c_1(EVEN#(z2)) - Signature: {AND/2,EVEN/1,GOAL/2,LTE/2,NOTEMPTY/1,and/2,even/1,goal/2,lte/2,notEmpty/1,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/0,c1/0,c10/0,c11/0 ,c12/2,c13/2,c2/0,c3/0,c4/1,c5/0,c6/0,c7/0,c8/1,c9/0,c_1/1,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/0,c_8/0,c_9/0 ,c_10/0,c_11/0,c_12/0,c_13/0,c_14/0,c_15/0,c_16/0,c_17/0,c_18/0,c_19/1,c_20/0,c_21/0,c_22/1,c_23/1,c_24/0 ,c_25/0,c_26/0,c_27/0} - Obligation: innermost runtime complexity wrt. defined symbols {AND#,EVEN#,GOAL#,LTE#,NOTEMPTY#,and#,even#,goal#,lte# ,notEmpty#} and constructors {Cons,False,Nil,True,c,c1,c10,c11,c12,c13,c2,c3,c4,c5,c6,c7,c8,c9} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:W:EVEN#(Cons(z0,Cons(z1,z2))) -> c_1(EVEN#(z2)) -->_1 EVEN#(Cons(z0,Cons(z1,z2))) -> c_1(EVEN#(z2)):1 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 1: EVEN#(Cons(z0,Cons(z1,z2))) -> c_1(EVEN#(z2)) **** Step 1.b:8.a:2.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,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/0,c1/0,c10/0,c11/0 ,c12/2,c13/2,c2/0,c3/0,c4/1,c5/0,c6/0,c7/0,c8/1,c9/0,c_1/1,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/0,c_8/0,c_9/0 ,c_10/0,c_11/0,c_12/0,c_13/0,c_14/0,c_15/0,c_16/0,c_17/0,c_18/0,c_19/1,c_20/0,c_21/0,c_22/1,c_23/1,c_24/0 ,c_25/0,c_26/0,c_27/0} - Obligation: innermost runtime complexity wrt. defined symbols {AND#,EVEN#,GOAL#,LTE#,NOTEMPTY#,and#,even#,goal#,lte# ,notEmpty#} and constructors {Cons,False,Nil,True,c,c1,c10,c11,c12,c13,c2,c3,c4,c5,c6,c7,c8,c9} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). *** Step 1.b:8.b:1: RemoveWeakSuffixes. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: LTE#(Cons(z0,z1),Cons(z2,z3)) -> c_6(LTE#(z1,z3)) - Weak DPs: EVEN#(Cons(z0,Cons(z1,z2))) -> c_1(EVEN#(z2)) - Signature: {AND/2,EVEN/1,GOAL/2,LTE/2,NOTEMPTY/1,and/2,even/1,goal/2,lte/2,notEmpty/1,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/0,c1/0,c10/0,c11/0 ,c12/2,c13/2,c2/0,c3/0,c4/1,c5/0,c6/0,c7/0,c8/1,c9/0,c_1/1,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/0,c_8/0,c_9/0 ,c_10/0,c_11/0,c_12/0,c_13/0,c_14/0,c_15/0,c_16/0,c_17/0,c_18/0,c_19/1,c_20/0,c_21/0,c_22/1,c_23/1,c_24/0 ,c_25/0,c_26/0,c_27/0} - Obligation: innermost runtime complexity wrt. defined symbols {AND#,EVEN#,GOAL#,LTE#,NOTEMPTY#,and#,even#,goal#,lte# ,notEmpty#} and constructors {Cons,False,Nil,True,c,c1,c10,c11,c12,c13,c2,c3,c4,c5,c6,c7,c8,c9} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:LTE#(Cons(z0,z1),Cons(z2,z3)) -> c_6(LTE#(z1,z3)) -->_1 LTE#(Cons(z0,z1),Cons(z2,z3)) -> c_6(LTE#(z1,z3)):1 2:W:EVEN#(Cons(z0,Cons(z1,z2))) -> c_1(EVEN#(z2)) -->_1 EVEN#(Cons(z0,Cons(z1,z2))) -> c_1(EVEN#(z2)):2 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 2: EVEN#(Cons(z0,Cons(z1,z2))) -> c_1(EVEN#(z2)) *** Step 1.b:8.b:2: PredecessorEstimationCP. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: LTE#(Cons(z0,z1),Cons(z2,z3)) -> c_6(LTE#(z1,z3)) - Signature: {AND/2,EVEN/1,GOAL/2,LTE/2,NOTEMPTY/1,and/2,even/1,goal/2,lte/2,notEmpty/1,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/0,c1/0,c10/0,c11/0 ,c12/2,c13/2,c2/0,c3/0,c4/1,c5/0,c6/0,c7/0,c8/1,c9/0,c_1/1,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/0,c_8/0,c_9/0 ,c_10/0,c_11/0,c_12/0,c_13/0,c_14/0,c_15/0,c_16/0,c_17/0,c_18/0,c_19/1,c_20/0,c_21/0,c_22/1,c_23/1,c_24/0 ,c_25/0,c_26/0,c_27/0} - Obligation: innermost runtime complexity wrt. defined symbols {AND#,EVEN#,GOAL#,LTE#,NOTEMPTY#,and#,even#,goal#,lte# ,notEmpty#} and constructors {Cons,False,Nil,True,c,c1,c10,c11,c12,c13,c2,c3,c4,c5,c6,c7,c8,c9} + 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(z0,z1),Cons(z2,z3)) -> c_6(LTE#(z1,z3)) The strictly oriented rules are moved into the weak component. **** Step 1.b:8.b:2.a:1: NaturalMI. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: LTE#(Cons(z0,z1),Cons(z2,z3)) -> c_6(LTE#(z1,z3)) - Signature: {AND/2,EVEN/1,GOAL/2,LTE/2,NOTEMPTY/1,and/2,even/1,goal/2,lte/2,notEmpty/1,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/0,c1/0,c10/0,c11/0 ,c12/2,c13/2,c2/0,c3/0,c4/1,c5/0,c6/0,c7/0,c8/1,c9/0,c_1/1,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/0,c_8/0,c_9/0 ,c_10/0,c_11/0,c_12/0,c_13/0,c_14/0,c_15/0,c_16/0,c_17/0,c_18/0,c_19/1,c_20/0,c_21/0,c_22/1,c_23/1,c_24/0 ,c_25/0,c_26/0,c_27/0} - Obligation: innermost runtime complexity wrt. defined symbols {AND#,EVEN#,GOAL#,LTE#,NOTEMPTY#,and#,even#,goal#,lte# ,notEmpty#} and constructors {Cons,False,Nil,True,c,c1,c10,c11,c12,c13,c2,c3,c4,c5,c6,c7,c8,c9} + 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#,and#,even#,goal#,lte#,notEmpty#} TcT has computed the following interpretation: p(AND) = [0] p(Cons) = [1] x1 + [1] x2 + [1] p(EVEN) = [0] p(False) = [0] p(GOAL) = [0] p(LTE) = [0] p(NOTEMPTY) = [0] p(Nil) = [0] p(True) = [0] p(and) = [0] p(c) = [0] p(c1) = [0] p(c10) = [0] p(c11) = [0] p(c12) = [0] p(c13) = [0] p(c2) = [0] p(c3) = [0] p(c4) = [0] p(c5) = [0] p(c6) = [0] p(c7) = [0] p(c8) = [0] p(c9) = [0] p(even) = [0] p(goal) = [0] p(lte) = [0] p(notEmpty) = [0] p(AND#) = [0] p(EVEN#) = [0] p(GOAL#) = [1] p(LTE#) = [8] x2 + [7] p(NOTEMPTY#) = [0] p(and#) = [2] x1 + [1] x2 + [0] p(even#) = [1] x1 + [0] p(goal#) = [2] x1 + [2] x2 + [0] p(lte#) = [1] x1 + [0] p(notEmpty#) = [1] x1 + [0] p(c_1) = [1] x1 + [0] p(c_2) = [0] p(c_3) = [0] p(c_4) = [1] x1 + [0] p(c_5) = [0] p(c_6) = [1] x1 + [6] p(c_7) = [0] p(c_8) = [0] p(c_9) = [0] p(c_10) = [0] p(c_11) = [0] p(c_12) = [0] p(c_13) = [0] p(c_14) = [0] p(c_15) = [0] p(c_16) = [0] p(c_17) = [0] p(c_18) = [0] p(c_19) = [0] p(c_20) = [2] p(c_21) = [4] p(c_22) = [1] x1 + [1] p(c_23) = [1] x1 + [1] p(c_24) = [1] p(c_25) = [8] p(c_26) = [2] p(c_27) = [1] Following rules are strictly oriented: LTE#(Cons(z0,z1),Cons(z2,z3)) = [8] z2 + [8] z3 + [15] > [8] z3 + [13] = c_6(LTE#(z1,z3)) Following rules are (at-least) weakly oriented: **** Step 1.b:8.b:2.a:2: Assumption. WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: LTE#(Cons(z0,z1),Cons(z2,z3)) -> c_6(LTE#(z1,z3)) - Signature: {AND/2,EVEN/1,GOAL/2,LTE/2,NOTEMPTY/1,and/2,even/1,goal/2,lte/2,notEmpty/1,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/0,c1/0,c10/0,c11/0 ,c12/2,c13/2,c2/0,c3/0,c4/1,c5/0,c6/0,c7/0,c8/1,c9/0,c_1/1,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/0,c_8/0,c_9/0 ,c_10/0,c_11/0,c_12/0,c_13/0,c_14/0,c_15/0,c_16/0,c_17/0,c_18/0,c_19/1,c_20/0,c_21/0,c_22/1,c_23/1,c_24/0 ,c_25/0,c_26/0,c_27/0} - Obligation: innermost runtime complexity wrt. defined symbols {AND#,EVEN#,GOAL#,LTE#,NOTEMPTY#,and#,even#,goal#,lte# ,notEmpty#} and constructors {Cons,False,Nil,True,c,c1,c10,c11,c12,c13,c2,c3,c4,c5,c6,c7,c8,c9} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown, timeBCUB = Unknown, timeBCLB = Unknown}} + Details: () **** Step 1.b:8.b:2.b:1: RemoveWeakSuffixes. WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: LTE#(Cons(z0,z1),Cons(z2,z3)) -> c_6(LTE#(z1,z3)) - Signature: {AND/2,EVEN/1,GOAL/2,LTE/2,NOTEMPTY/1,and/2,even/1,goal/2,lte/2,notEmpty/1,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/0,c1/0,c10/0,c11/0 ,c12/2,c13/2,c2/0,c3/0,c4/1,c5/0,c6/0,c7/0,c8/1,c9/0,c_1/1,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/0,c_8/0,c_9/0 ,c_10/0,c_11/0,c_12/0,c_13/0,c_14/0,c_15/0,c_16/0,c_17/0,c_18/0,c_19/1,c_20/0,c_21/0,c_22/1,c_23/1,c_24/0 ,c_25/0,c_26/0,c_27/0} - Obligation: innermost runtime complexity wrt. defined symbols {AND#,EVEN#,GOAL#,LTE#,NOTEMPTY#,and#,even#,goal#,lte# ,notEmpty#} and constructors {Cons,False,Nil,True,c,c1,c10,c11,c12,c13,c2,c3,c4,c5,c6,c7,c8,c9} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:W:LTE#(Cons(z0,z1),Cons(z2,z3)) -> c_6(LTE#(z1,z3)) -->_1 LTE#(Cons(z0,z1),Cons(z2,z3)) -> c_6(LTE#(z1,z3)):1 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 1: LTE#(Cons(z0,z1),Cons(z2,z3)) -> c_6(LTE#(z1,z3)) **** Step 1.b:8.b:2.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,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/0,c1/0,c10/0,c11/0 ,c12/2,c13/2,c2/0,c3/0,c4/1,c5/0,c6/0,c7/0,c8/1,c9/0,c_1/1,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/0,c_8/0,c_9/0 ,c_10/0,c_11/0,c_12/0,c_13/0,c_14/0,c_15/0,c_16/0,c_17/0,c_18/0,c_19/1,c_20/0,c_21/0,c_22/1,c_23/1,c_24/0 ,c_25/0,c_26/0,c_27/0} - Obligation: innermost runtime complexity wrt. defined symbols {AND#,EVEN#,GOAL#,LTE#,NOTEMPTY#,and#,even#,goal#,lte# ,notEmpty#} and constructors {Cons,False,Nil,True,c,c1,c10,c11,c12,c13,c2,c3,c4,c5,c6,c7,c8,c9} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(Omega(n^1),O(n^1))