WORST_CASE(Omega(n^1),O(n^1)) * Step 1: Sum. WORST_CASE(Omega(n^1),O(n^1)) + Considered Problem: - Strict TRS: FOLD(z0,z1) -> c10(FOLDR(z0,z1)) FOLD(z0,z1) -> c9(FOLDL(z0,z1)) FOLDL(z0,Cons(S(0()),z1)) -> c(FOLDL(S(z0),z1)) FOLDL(z0,Nil()) -> c2() FOLDL(S(0()),Cons(z0,z1)) -> c1(FOLDL(S(z0),z1)) FOLDR(z0,Cons(z1,z2)) -> c3(OP(z1,foldr(z0,z2)),FOLDR(z0,z2)) FOLDR(z0,Nil()) -> c4() NOTEMPTY(Cons(z0,z1)) -> c5() NOTEMPTY(Nil()) -> c6() OP(z0,S(0())) -> c7() OP(S(0()),z0) -> c8() - Weak TRS: fold(z0,z1) -> Cons(foldl(z0,z1),Cons(foldr(z0,z1),Nil())) foldl(z0,Cons(S(0()),z1)) -> foldl(S(z0),z1) foldl(z0,Nil()) -> z0 foldl(S(0()),Cons(z0,z1)) -> foldl(S(z0),z1) foldr(z0,Cons(z1,z2)) -> op(z1,foldr(z0,z2)) foldr(z0,Nil()) -> z0 notEmpty(Cons(z0,z1)) -> True() notEmpty(Nil()) -> False() op(z0,S(0())) -> S(z0) op(S(0()),z0) -> S(z0) - Signature: {FOLD/2,FOLDL/2,FOLDR/2,NOTEMPTY/1,OP/2,fold/2,foldl/2,foldr/2,notEmpty/1,op/2} / {0/0,Cons/2,False/0,Nil/0 ,S/1,True/0,c/1,c1/1,c10/1,c2/0,c3/2,c4/0,c5/0,c6/0,c7/0,c8/0,c9/1} - Obligation: innermost runtime complexity wrt. defined symbols {FOLD,FOLDL,FOLDR,NOTEMPTY,OP,fold,foldl,foldr,notEmpty ,op} and constructors {0,Cons,False,Nil,S,True,c,c1,c10,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: FOLD(z0,z1) -> c10(FOLDR(z0,z1)) FOLD(z0,z1) -> c9(FOLDL(z0,z1)) FOLDL(z0,Cons(S(0()),z1)) -> c(FOLDL(S(z0),z1)) FOLDL(z0,Nil()) -> c2() FOLDL(S(0()),Cons(z0,z1)) -> c1(FOLDL(S(z0),z1)) FOLDR(z0,Cons(z1,z2)) -> c3(OP(z1,foldr(z0,z2)),FOLDR(z0,z2)) FOLDR(z0,Nil()) -> c4() NOTEMPTY(Cons(z0,z1)) -> c5() NOTEMPTY(Nil()) -> c6() OP(z0,S(0())) -> c7() OP(S(0()),z0) -> c8() - Weak TRS: fold(z0,z1) -> Cons(foldl(z0,z1),Cons(foldr(z0,z1),Nil())) foldl(z0,Cons(S(0()),z1)) -> foldl(S(z0),z1) foldl(z0,Nil()) -> z0 foldl(S(0()),Cons(z0,z1)) -> foldl(S(z0),z1) foldr(z0,Cons(z1,z2)) -> op(z1,foldr(z0,z2)) foldr(z0,Nil()) -> z0 notEmpty(Cons(z0,z1)) -> True() notEmpty(Nil()) -> False() op(z0,S(0())) -> S(z0) op(S(0()),z0) -> S(z0) - Signature: {FOLD/2,FOLDL/2,FOLDR/2,NOTEMPTY/1,OP/2,fold/2,foldl/2,foldr/2,notEmpty/1,op/2} / {0/0,Cons/2,False/0,Nil/0 ,S/1,True/0,c/1,c1/1,c10/1,c2/0,c3/2,c4/0,c5/0,c6/0,c7/0,c8/0,c9/1} - Obligation: innermost runtime complexity wrt. defined symbols {FOLD,FOLDL,FOLDR,NOTEMPTY,OP,fold,foldl,foldr,notEmpty ,op} and constructors {0,Cons,False,Nil,S,True,c,c1,c10,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: FOLD(z0,z1) -> c10(FOLDR(z0,z1)) FOLD(z0,z1) -> c9(FOLDL(z0,z1)) FOLDL(z0,Cons(S(0()),z1)) -> c(FOLDL(S(z0),z1)) FOLDL(z0,Nil()) -> c2() FOLDL(S(0()),Cons(z0,z1)) -> c1(FOLDL(S(z0),z1)) FOLDR(z0,Cons(z1,z2)) -> c3(OP(z1,foldr(z0,z2)),FOLDR(z0,z2)) FOLDR(z0,Nil()) -> c4() NOTEMPTY(Cons(z0,z1)) -> c5() NOTEMPTY(Nil()) -> c6() OP(z0,S(0())) -> c7() OP(S(0()),z0) -> c8() - Weak TRS: fold(z0,z1) -> Cons(foldl(z0,z1),Cons(foldr(z0,z1),Nil())) foldl(z0,Cons(S(0()),z1)) -> foldl(S(z0),z1) foldl(z0,Nil()) -> z0 foldl(S(0()),Cons(z0,z1)) -> foldl(S(z0),z1) foldr(z0,Cons(z1,z2)) -> op(z1,foldr(z0,z2)) foldr(z0,Nil()) -> z0 notEmpty(Cons(z0,z1)) -> True() notEmpty(Nil()) -> False() op(z0,S(0())) -> S(z0) op(S(0()),z0) -> S(z0) - Signature: {FOLD/2,FOLDL/2,FOLDR/2,NOTEMPTY/1,OP/2,fold/2,foldl/2,foldr/2,notEmpty/1,op/2} / {0/0,Cons/2,False/0,Nil/0 ,S/1,True/0,c/1,c1/1,c10/1,c2/0,c3/2,c4/0,c5/0,c6/0,c7/0,c8/0,c9/1} - Obligation: innermost runtime complexity wrt. defined symbols {FOLD,FOLDL,FOLDR,NOTEMPTY,OP,fold,foldl,foldr,notEmpty ,op} and constructors {0,Cons,False,Nil,S,True,c,c1,c10,c2,c3,c4,c5,c6,c7,c8,c9} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: FOLDL(x,y){y -> Cons(S(0()),y)} = FOLDL(x,Cons(S(0()),y)) ->^+ c(FOLDL(S(x),y)) = C[FOLDL(S(x),y) = FOLDL(x,y){x -> S(x)}] ** Step 1.b:1: DependencyPairs. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: FOLD(z0,z1) -> c10(FOLDR(z0,z1)) FOLD(z0,z1) -> c9(FOLDL(z0,z1)) FOLDL(z0,Cons(S(0()),z1)) -> c(FOLDL(S(z0),z1)) FOLDL(z0,Nil()) -> c2() FOLDL(S(0()),Cons(z0,z1)) -> c1(FOLDL(S(z0),z1)) FOLDR(z0,Cons(z1,z2)) -> c3(OP(z1,foldr(z0,z2)),FOLDR(z0,z2)) FOLDR(z0,Nil()) -> c4() NOTEMPTY(Cons(z0,z1)) -> c5() NOTEMPTY(Nil()) -> c6() OP(z0,S(0())) -> c7() OP(S(0()),z0) -> c8() - Weak TRS: fold(z0,z1) -> Cons(foldl(z0,z1),Cons(foldr(z0,z1),Nil())) foldl(z0,Cons(S(0()),z1)) -> foldl(S(z0),z1) foldl(z0,Nil()) -> z0 foldl(S(0()),Cons(z0,z1)) -> foldl(S(z0),z1) foldr(z0,Cons(z1,z2)) -> op(z1,foldr(z0,z2)) foldr(z0,Nil()) -> z0 notEmpty(Cons(z0,z1)) -> True() notEmpty(Nil()) -> False() op(z0,S(0())) -> S(z0) op(S(0()),z0) -> S(z0) - Signature: {FOLD/2,FOLDL/2,FOLDR/2,NOTEMPTY/1,OP/2,fold/2,foldl/2,foldr/2,notEmpty/1,op/2} / {0/0,Cons/2,False/0,Nil/0 ,S/1,True/0,c/1,c1/1,c10/1,c2/0,c3/2,c4/0,c5/0,c6/0,c7/0,c8/0,c9/1} - Obligation: innermost runtime complexity wrt. defined symbols {FOLD,FOLDL,FOLDR,NOTEMPTY,OP,fold,foldl,foldr,notEmpty ,op} and constructors {0,Cons,False,Nil,S,True,c,c1,c10,c2,c3,c4,c5,c6,c7,c8,c9} + Applied Processor: DependencyPairs {dpKind_ = WIDP} + Details: We add the following weak innermost dependency pairs: Strict DPs FOLD#(z0,z1) -> c_1(FOLDR#(z0,z1)) FOLD#(z0,z1) -> c_2(FOLDL#(z0,z1)) FOLDL#(z0,Cons(S(0()),z1)) -> c_3(FOLDL#(S(z0),z1)) FOLDL#(z0,Nil()) -> c_4() FOLDL#(S(0()),Cons(z0,z1)) -> c_5(FOLDL#(S(z0),z1)) FOLDR#(z0,Cons(z1,z2)) -> c_6(OP#(z1,foldr(z0,z2)),FOLDR#(z0,z2)) FOLDR#(z0,Nil()) -> c_7() NOTEMPTY#(Cons(z0,z1)) -> c_8() NOTEMPTY#(Nil()) -> c_9() OP#(z0,S(0())) -> c_10() OP#(S(0()),z0) -> c_11() Weak DPs fold#(z0,z1) -> c_12(foldl#(z0,z1),foldr#(z0,z1)) foldl#(z0,Cons(S(0()),z1)) -> c_13(foldl#(S(z0),z1)) foldl#(z0,Nil()) -> c_14() foldl#(S(0()),Cons(z0,z1)) -> c_15(foldl#(S(z0),z1)) foldr#(z0,Cons(z1,z2)) -> c_16(op#(z1,foldr(z0,z2))) foldr#(z0,Nil()) -> c_17() notEmpty#(Cons(z0,z1)) -> c_18() notEmpty#(Nil()) -> c_19() op#(z0,S(0())) -> c_20() op#(S(0()),z0) -> c_21() and mark the set of starting terms. ** Step 1.b:2: UsableRules. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: FOLD#(z0,z1) -> c_1(FOLDR#(z0,z1)) FOLD#(z0,z1) -> c_2(FOLDL#(z0,z1)) FOLDL#(z0,Cons(S(0()),z1)) -> c_3(FOLDL#(S(z0),z1)) FOLDL#(z0,Nil()) -> c_4() FOLDL#(S(0()),Cons(z0,z1)) -> c_5(FOLDL#(S(z0),z1)) FOLDR#(z0,Cons(z1,z2)) -> c_6(OP#(z1,foldr(z0,z2)),FOLDR#(z0,z2)) FOLDR#(z0,Nil()) -> c_7() NOTEMPTY#(Cons(z0,z1)) -> c_8() NOTEMPTY#(Nil()) -> c_9() OP#(z0,S(0())) -> c_10() OP#(S(0()),z0) -> c_11() - Strict TRS: FOLD(z0,z1) -> c10(FOLDR(z0,z1)) FOLD(z0,z1) -> c9(FOLDL(z0,z1)) FOLDL(z0,Cons(S(0()),z1)) -> c(FOLDL(S(z0),z1)) FOLDL(z0,Nil()) -> c2() FOLDL(S(0()),Cons(z0,z1)) -> c1(FOLDL(S(z0),z1)) FOLDR(z0,Cons(z1,z2)) -> c3(OP(z1,foldr(z0,z2)),FOLDR(z0,z2)) FOLDR(z0,Nil()) -> c4() NOTEMPTY(Cons(z0,z1)) -> c5() NOTEMPTY(Nil()) -> c6() OP(z0,S(0())) -> c7() OP(S(0()),z0) -> c8() - Weak DPs: fold#(z0,z1) -> c_12(foldl#(z0,z1),foldr#(z0,z1)) foldl#(z0,Cons(S(0()),z1)) -> c_13(foldl#(S(z0),z1)) foldl#(z0,Nil()) -> c_14() foldl#(S(0()),Cons(z0,z1)) -> c_15(foldl#(S(z0),z1)) foldr#(z0,Cons(z1,z2)) -> c_16(op#(z1,foldr(z0,z2))) foldr#(z0,Nil()) -> c_17() notEmpty#(Cons(z0,z1)) -> c_18() notEmpty#(Nil()) -> c_19() op#(z0,S(0())) -> c_20() op#(S(0()),z0) -> c_21() - Weak TRS: fold(z0,z1) -> Cons(foldl(z0,z1),Cons(foldr(z0,z1),Nil())) foldl(z0,Cons(S(0()),z1)) -> foldl(S(z0),z1) foldl(z0,Nil()) -> z0 foldl(S(0()),Cons(z0,z1)) -> foldl(S(z0),z1) foldr(z0,Cons(z1,z2)) -> op(z1,foldr(z0,z2)) foldr(z0,Nil()) -> z0 notEmpty(Cons(z0,z1)) -> True() notEmpty(Nil()) -> False() op(z0,S(0())) -> S(z0) op(S(0()),z0) -> S(z0) - Signature: {FOLD/2,FOLDL/2,FOLDR/2,NOTEMPTY/1,OP/2,fold/2,foldl/2,foldr/2,notEmpty/1,op/2,FOLD#/2,FOLDL#/2,FOLDR#/2 ,NOTEMPTY#/1,OP#/2,fold#/2,foldl#/2,foldr#/2,notEmpty#/1,op#/2} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c/1 ,c1/1,c10/1,c2/0,c3/2,c4/0,c5/0,c6/0,c7/0,c8/0,c9/1,c_1/1,c_2/1,c_3/1,c_4/0,c_5/1,c_6/2,c_7/0,c_8/0,c_9/0 ,c_10/0,c_11/0,c_12/2,c_13/1,c_14/0,c_15/1,c_16/1,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0} - Obligation: innermost runtime complexity wrt. defined symbols {FOLD#,FOLDL#,FOLDR#,NOTEMPTY#,OP#,fold#,foldl#,foldr# ,notEmpty#,op#} and constructors {0,Cons,False,Nil,S,True,c,c1,c10,c2,c3,c4,c5,c6,c7,c8,c9} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: foldr(z0,Cons(z1,z2)) -> op(z1,foldr(z0,z2)) foldr(z0,Nil()) -> z0 op(z0,S(0())) -> S(z0) op(S(0()),z0) -> S(z0) FOLD#(z0,z1) -> c_1(FOLDR#(z0,z1)) FOLD#(z0,z1) -> c_2(FOLDL#(z0,z1)) FOLDL#(z0,Cons(S(0()),z1)) -> c_3(FOLDL#(S(z0),z1)) FOLDL#(z0,Nil()) -> c_4() FOLDL#(S(0()),Cons(z0,z1)) -> c_5(FOLDL#(S(z0),z1)) FOLDR#(z0,Cons(z1,z2)) -> c_6(OP#(z1,foldr(z0,z2)),FOLDR#(z0,z2)) FOLDR#(z0,Nil()) -> c_7() NOTEMPTY#(Cons(z0,z1)) -> c_8() NOTEMPTY#(Nil()) -> c_9() OP#(z0,S(0())) -> c_10() OP#(S(0()),z0) -> c_11() fold#(z0,z1) -> c_12(foldl#(z0,z1),foldr#(z0,z1)) foldl#(z0,Cons(S(0()),z1)) -> c_13(foldl#(S(z0),z1)) foldl#(z0,Nil()) -> c_14() foldl#(S(0()),Cons(z0,z1)) -> c_15(foldl#(S(z0),z1)) foldr#(z0,Cons(z1,z2)) -> c_16(op#(z1,foldr(z0,z2))) foldr#(z0,Nil()) -> c_17() notEmpty#(Cons(z0,z1)) -> c_18() notEmpty#(Nil()) -> c_19() op#(z0,S(0())) -> c_20() op#(S(0()),z0) -> c_21() ** Step 1.b:3: PredecessorEstimation. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: FOLD#(z0,z1) -> c_1(FOLDR#(z0,z1)) FOLD#(z0,z1) -> c_2(FOLDL#(z0,z1)) FOLDL#(z0,Cons(S(0()),z1)) -> c_3(FOLDL#(S(z0),z1)) FOLDL#(z0,Nil()) -> c_4() FOLDL#(S(0()),Cons(z0,z1)) -> c_5(FOLDL#(S(z0),z1)) FOLDR#(z0,Cons(z1,z2)) -> c_6(OP#(z1,foldr(z0,z2)),FOLDR#(z0,z2)) FOLDR#(z0,Nil()) -> c_7() NOTEMPTY#(Cons(z0,z1)) -> c_8() NOTEMPTY#(Nil()) -> c_9() OP#(z0,S(0())) -> c_10() OP#(S(0()),z0) -> c_11() - Weak DPs: fold#(z0,z1) -> c_12(foldl#(z0,z1),foldr#(z0,z1)) foldl#(z0,Cons(S(0()),z1)) -> c_13(foldl#(S(z0),z1)) foldl#(z0,Nil()) -> c_14() foldl#(S(0()),Cons(z0,z1)) -> c_15(foldl#(S(z0),z1)) foldr#(z0,Cons(z1,z2)) -> c_16(op#(z1,foldr(z0,z2))) foldr#(z0,Nil()) -> c_17() notEmpty#(Cons(z0,z1)) -> c_18() notEmpty#(Nil()) -> c_19() op#(z0,S(0())) -> c_20() op#(S(0()),z0) -> c_21() - Weak TRS: foldr(z0,Cons(z1,z2)) -> op(z1,foldr(z0,z2)) foldr(z0,Nil()) -> z0 op(z0,S(0())) -> S(z0) op(S(0()),z0) -> S(z0) - Signature: {FOLD/2,FOLDL/2,FOLDR/2,NOTEMPTY/1,OP/2,fold/2,foldl/2,foldr/2,notEmpty/1,op/2,FOLD#/2,FOLDL#/2,FOLDR#/2 ,NOTEMPTY#/1,OP#/2,fold#/2,foldl#/2,foldr#/2,notEmpty#/1,op#/2} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c/1 ,c1/1,c10/1,c2/0,c3/2,c4/0,c5/0,c6/0,c7/0,c8/0,c9/1,c_1/1,c_2/1,c_3/1,c_4/0,c_5/1,c_6/2,c_7/0,c_8/0,c_9/0 ,c_10/0,c_11/0,c_12/2,c_13/1,c_14/0,c_15/1,c_16/1,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0} - Obligation: innermost runtime complexity wrt. defined symbols {FOLD#,FOLDL#,FOLDR#,NOTEMPTY#,OP#,fold#,foldl#,foldr# ,notEmpty#,op#} and constructors {0,Cons,False,Nil,S,True,c,c1,c10,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 {4,7,8,9,10,11} by application of Pre({4,7,8,9,10,11}) = {1,2,3,5,6}. Here rules are labelled as follows: 1: FOLD#(z0,z1) -> c_1(FOLDR#(z0,z1)) 2: FOLD#(z0,z1) -> c_2(FOLDL#(z0,z1)) 3: FOLDL#(z0,Cons(S(0()),z1)) -> c_3(FOLDL#(S(z0),z1)) 4: FOLDL#(z0,Nil()) -> c_4() 5: FOLDL#(S(0()),Cons(z0,z1)) -> c_5(FOLDL#(S(z0),z1)) 6: FOLDR#(z0,Cons(z1,z2)) -> c_6(OP#(z1,foldr(z0,z2)),FOLDR#(z0,z2)) 7: FOLDR#(z0,Nil()) -> c_7() 8: NOTEMPTY#(Cons(z0,z1)) -> c_8() 9: NOTEMPTY#(Nil()) -> c_9() 10: OP#(z0,S(0())) -> c_10() 11: OP#(S(0()),z0) -> c_11() 12: fold#(z0,z1) -> c_12(foldl#(z0,z1),foldr#(z0,z1)) 13: foldl#(z0,Cons(S(0()),z1)) -> c_13(foldl#(S(z0),z1)) 14: foldl#(z0,Nil()) -> c_14() 15: foldl#(S(0()),Cons(z0,z1)) -> c_15(foldl#(S(z0),z1)) 16: foldr#(z0,Cons(z1,z2)) -> c_16(op#(z1,foldr(z0,z2))) 17: foldr#(z0,Nil()) -> c_17() 18: notEmpty#(Cons(z0,z1)) -> c_18() 19: notEmpty#(Nil()) -> c_19() 20: op#(z0,S(0())) -> c_20() 21: op#(S(0()),z0) -> c_21() ** Step 1.b:4: RemoveWeakSuffixes. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: FOLD#(z0,z1) -> c_1(FOLDR#(z0,z1)) FOLD#(z0,z1) -> c_2(FOLDL#(z0,z1)) FOLDL#(z0,Cons(S(0()),z1)) -> c_3(FOLDL#(S(z0),z1)) FOLDL#(S(0()),Cons(z0,z1)) -> c_5(FOLDL#(S(z0),z1)) FOLDR#(z0,Cons(z1,z2)) -> c_6(OP#(z1,foldr(z0,z2)),FOLDR#(z0,z2)) - Weak DPs: FOLDL#(z0,Nil()) -> c_4() FOLDR#(z0,Nil()) -> c_7() NOTEMPTY#(Cons(z0,z1)) -> c_8() NOTEMPTY#(Nil()) -> c_9() OP#(z0,S(0())) -> c_10() OP#(S(0()),z0) -> c_11() fold#(z0,z1) -> c_12(foldl#(z0,z1),foldr#(z0,z1)) foldl#(z0,Cons(S(0()),z1)) -> c_13(foldl#(S(z0),z1)) foldl#(z0,Nil()) -> c_14() foldl#(S(0()),Cons(z0,z1)) -> c_15(foldl#(S(z0),z1)) foldr#(z0,Cons(z1,z2)) -> c_16(op#(z1,foldr(z0,z2))) foldr#(z0,Nil()) -> c_17() notEmpty#(Cons(z0,z1)) -> c_18() notEmpty#(Nil()) -> c_19() op#(z0,S(0())) -> c_20() op#(S(0()),z0) -> c_21() - Weak TRS: foldr(z0,Cons(z1,z2)) -> op(z1,foldr(z0,z2)) foldr(z0,Nil()) -> z0 op(z0,S(0())) -> S(z0) op(S(0()),z0) -> S(z0) - Signature: {FOLD/2,FOLDL/2,FOLDR/2,NOTEMPTY/1,OP/2,fold/2,foldl/2,foldr/2,notEmpty/1,op/2,FOLD#/2,FOLDL#/2,FOLDR#/2 ,NOTEMPTY#/1,OP#/2,fold#/2,foldl#/2,foldr#/2,notEmpty#/1,op#/2} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c/1 ,c1/1,c10/1,c2/0,c3/2,c4/0,c5/0,c6/0,c7/0,c8/0,c9/1,c_1/1,c_2/1,c_3/1,c_4/0,c_5/1,c_6/2,c_7/0,c_8/0,c_9/0 ,c_10/0,c_11/0,c_12/2,c_13/1,c_14/0,c_15/1,c_16/1,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0} - Obligation: innermost runtime complexity wrt. defined symbols {FOLD#,FOLDL#,FOLDR#,NOTEMPTY#,OP#,fold#,foldl#,foldr# ,notEmpty#,op#} and constructors {0,Cons,False,Nil,S,True,c,c1,c10,c2,c3,c4,c5,c6,c7,c8,c9} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:FOLD#(z0,z1) -> c_1(FOLDR#(z0,z1)) -->_1 FOLDR#(z0,Cons(z1,z2)) -> c_6(OP#(z1,foldr(z0,z2)),FOLDR#(z0,z2)):5 -->_1 FOLDR#(z0,Nil()) -> c_7():7 2:S:FOLD#(z0,z1) -> c_2(FOLDL#(z0,z1)) -->_1 FOLDL#(S(0()),Cons(z0,z1)) -> c_5(FOLDL#(S(z0),z1)):4 -->_1 FOLDL#(z0,Cons(S(0()),z1)) -> c_3(FOLDL#(S(z0),z1)):3 -->_1 FOLDL#(z0,Nil()) -> c_4():6 3:S:FOLDL#(z0,Cons(S(0()),z1)) -> c_3(FOLDL#(S(z0),z1)) -->_1 FOLDL#(S(0()),Cons(z0,z1)) -> c_5(FOLDL#(S(z0),z1)):4 -->_1 FOLDL#(z0,Nil()) -> c_4():6 -->_1 FOLDL#(z0,Cons(S(0()),z1)) -> c_3(FOLDL#(S(z0),z1)):3 4:S:FOLDL#(S(0()),Cons(z0,z1)) -> c_5(FOLDL#(S(z0),z1)) -->_1 FOLDL#(z0,Nil()) -> c_4():6 -->_1 FOLDL#(S(0()),Cons(z0,z1)) -> c_5(FOLDL#(S(z0),z1)):4 -->_1 FOLDL#(z0,Cons(S(0()),z1)) -> c_3(FOLDL#(S(z0),z1)):3 5:S:FOLDR#(z0,Cons(z1,z2)) -> c_6(OP#(z1,foldr(z0,z2)),FOLDR#(z0,z2)) -->_1 OP#(S(0()),z0) -> c_11():11 -->_1 OP#(z0,S(0())) -> c_10():10 -->_2 FOLDR#(z0,Nil()) -> c_7():7 -->_2 FOLDR#(z0,Cons(z1,z2)) -> c_6(OP#(z1,foldr(z0,z2)),FOLDR#(z0,z2)):5 6:W:FOLDL#(z0,Nil()) -> c_4() 7:W:FOLDR#(z0,Nil()) -> c_7() 8:W:NOTEMPTY#(Cons(z0,z1)) -> c_8() 9:W:NOTEMPTY#(Nil()) -> c_9() 10:W:OP#(z0,S(0())) -> c_10() 11:W:OP#(S(0()),z0) -> c_11() 12:W:fold#(z0,z1) -> c_12(foldl#(z0,z1),foldr#(z0,z1)) -->_2 foldr#(z0,Cons(z1,z2)) -> c_16(op#(z1,foldr(z0,z2))):16 -->_1 foldl#(S(0()),Cons(z0,z1)) -> c_15(foldl#(S(z0),z1)):15 -->_1 foldl#(z0,Cons(S(0()),z1)) -> c_13(foldl#(S(z0),z1)):13 -->_2 foldr#(z0,Nil()) -> c_17():17 -->_1 foldl#(z0,Nil()) -> c_14():14 13:W:foldl#(z0,Cons(S(0()),z1)) -> c_13(foldl#(S(z0),z1)) -->_1 foldl#(S(0()),Cons(z0,z1)) -> c_15(foldl#(S(z0),z1)):15 -->_1 foldl#(z0,Nil()) -> c_14():14 -->_1 foldl#(z0,Cons(S(0()),z1)) -> c_13(foldl#(S(z0),z1)):13 14:W:foldl#(z0,Nil()) -> c_14() 15:W:foldl#(S(0()),Cons(z0,z1)) -> c_15(foldl#(S(z0),z1)) -->_1 foldl#(S(0()),Cons(z0,z1)) -> c_15(foldl#(S(z0),z1)):15 -->_1 foldl#(z0,Nil()) -> c_14():14 -->_1 foldl#(z0,Cons(S(0()),z1)) -> c_13(foldl#(S(z0),z1)):13 16:W:foldr#(z0,Cons(z1,z2)) -> c_16(op#(z1,foldr(z0,z2))) -->_1 op#(S(0()),z0) -> c_21():21 -->_1 op#(z0,S(0())) -> c_20():20 17:W:foldr#(z0,Nil()) -> c_17() 18:W:notEmpty#(Cons(z0,z1)) -> c_18() 19:W:notEmpty#(Nil()) -> c_19() 20:W:op#(z0,S(0())) -> c_20() 21:W:op#(S(0()),z0) -> c_21() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 19: notEmpty#(Nil()) -> c_19() 18: notEmpty#(Cons(z0,z1)) -> c_18() 12: fold#(z0,z1) -> c_12(foldl#(z0,z1),foldr#(z0,z1)) 17: foldr#(z0,Nil()) -> c_17() 15: foldl#(S(0()),Cons(z0,z1)) -> c_15(foldl#(S(z0),z1)) 13: foldl#(z0,Cons(S(0()),z1)) -> c_13(foldl#(S(z0),z1)) 14: foldl#(z0,Nil()) -> c_14() 16: foldr#(z0,Cons(z1,z2)) -> c_16(op#(z1,foldr(z0,z2))) 20: op#(z0,S(0())) -> c_20() 21: op#(S(0()),z0) -> c_21() 9: NOTEMPTY#(Nil()) -> c_9() 8: NOTEMPTY#(Cons(z0,z1)) -> c_8() 6: FOLDL#(z0,Nil()) -> c_4() 7: FOLDR#(z0,Nil()) -> c_7() 10: OP#(z0,S(0())) -> c_10() 11: OP#(S(0()),z0) -> c_11() ** Step 1.b:5: SimplifyRHS. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: FOLD#(z0,z1) -> c_1(FOLDR#(z0,z1)) FOLD#(z0,z1) -> c_2(FOLDL#(z0,z1)) FOLDL#(z0,Cons(S(0()),z1)) -> c_3(FOLDL#(S(z0),z1)) FOLDL#(S(0()),Cons(z0,z1)) -> c_5(FOLDL#(S(z0),z1)) FOLDR#(z0,Cons(z1,z2)) -> c_6(OP#(z1,foldr(z0,z2)),FOLDR#(z0,z2)) - Weak TRS: foldr(z0,Cons(z1,z2)) -> op(z1,foldr(z0,z2)) foldr(z0,Nil()) -> z0 op(z0,S(0())) -> S(z0) op(S(0()),z0) -> S(z0) - Signature: {FOLD/2,FOLDL/2,FOLDR/2,NOTEMPTY/1,OP/2,fold/2,foldl/2,foldr/2,notEmpty/1,op/2,FOLD#/2,FOLDL#/2,FOLDR#/2 ,NOTEMPTY#/1,OP#/2,fold#/2,foldl#/2,foldr#/2,notEmpty#/1,op#/2} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c/1 ,c1/1,c10/1,c2/0,c3/2,c4/0,c5/0,c6/0,c7/0,c8/0,c9/1,c_1/1,c_2/1,c_3/1,c_4/0,c_5/1,c_6/2,c_7/0,c_8/0,c_9/0 ,c_10/0,c_11/0,c_12/2,c_13/1,c_14/0,c_15/1,c_16/1,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0} - Obligation: innermost runtime complexity wrt. defined symbols {FOLD#,FOLDL#,FOLDR#,NOTEMPTY#,OP#,fold#,foldl#,foldr# ,notEmpty#,op#} and constructors {0,Cons,False,Nil,S,True,c,c1,c10,c2,c3,c4,c5,c6,c7,c8,c9} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:FOLD#(z0,z1) -> c_1(FOLDR#(z0,z1)) -->_1 FOLDR#(z0,Cons(z1,z2)) -> c_6(OP#(z1,foldr(z0,z2)),FOLDR#(z0,z2)):5 2:S:FOLD#(z0,z1) -> c_2(FOLDL#(z0,z1)) -->_1 FOLDL#(S(0()),Cons(z0,z1)) -> c_5(FOLDL#(S(z0),z1)):4 -->_1 FOLDL#(z0,Cons(S(0()),z1)) -> c_3(FOLDL#(S(z0),z1)):3 3:S:FOLDL#(z0,Cons(S(0()),z1)) -> c_3(FOLDL#(S(z0),z1)) -->_1 FOLDL#(S(0()),Cons(z0,z1)) -> c_5(FOLDL#(S(z0),z1)):4 -->_1 FOLDL#(z0,Cons(S(0()),z1)) -> c_3(FOLDL#(S(z0),z1)):3 4:S:FOLDL#(S(0()),Cons(z0,z1)) -> c_5(FOLDL#(S(z0),z1)) -->_1 FOLDL#(S(0()),Cons(z0,z1)) -> c_5(FOLDL#(S(z0),z1)):4 -->_1 FOLDL#(z0,Cons(S(0()),z1)) -> c_3(FOLDL#(S(z0),z1)):3 5:S:FOLDR#(z0,Cons(z1,z2)) -> c_6(OP#(z1,foldr(z0,z2)),FOLDR#(z0,z2)) -->_2 FOLDR#(z0,Cons(z1,z2)) -> c_6(OP#(z1,foldr(z0,z2)),FOLDR#(z0,z2)):5 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: FOLDR#(z0,Cons(z1,z2)) -> c_6(FOLDR#(z0,z2)) ** Step 1.b:6: UsableRules. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: FOLD#(z0,z1) -> c_1(FOLDR#(z0,z1)) FOLD#(z0,z1) -> c_2(FOLDL#(z0,z1)) FOLDL#(z0,Cons(S(0()),z1)) -> c_3(FOLDL#(S(z0),z1)) FOLDL#(S(0()),Cons(z0,z1)) -> c_5(FOLDL#(S(z0),z1)) FOLDR#(z0,Cons(z1,z2)) -> c_6(FOLDR#(z0,z2)) - Weak TRS: foldr(z0,Cons(z1,z2)) -> op(z1,foldr(z0,z2)) foldr(z0,Nil()) -> z0 op(z0,S(0())) -> S(z0) op(S(0()),z0) -> S(z0) - Signature: {FOLD/2,FOLDL/2,FOLDR/2,NOTEMPTY/1,OP/2,fold/2,foldl/2,foldr/2,notEmpty/1,op/2,FOLD#/2,FOLDL#/2,FOLDR#/2 ,NOTEMPTY#/1,OP#/2,fold#/2,foldl#/2,foldr#/2,notEmpty#/1,op#/2} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c/1 ,c1/1,c10/1,c2/0,c3/2,c4/0,c5/0,c6/0,c7/0,c8/0,c9/1,c_1/1,c_2/1,c_3/1,c_4/0,c_5/1,c_6/1,c_7/0,c_8/0,c_9/0 ,c_10/0,c_11/0,c_12/2,c_13/1,c_14/0,c_15/1,c_16/1,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0} - Obligation: innermost runtime complexity wrt. defined symbols {FOLD#,FOLDL#,FOLDR#,NOTEMPTY#,OP#,fold#,foldl#,foldr# ,notEmpty#,op#} and constructors {0,Cons,False,Nil,S,True,c,c1,c10,c2,c3,c4,c5,c6,c7,c8,c9} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: FOLD#(z0,z1) -> c_1(FOLDR#(z0,z1)) FOLD#(z0,z1) -> c_2(FOLDL#(z0,z1)) FOLDL#(z0,Cons(S(0()),z1)) -> c_3(FOLDL#(S(z0),z1)) FOLDL#(S(0()),Cons(z0,z1)) -> c_5(FOLDL#(S(z0),z1)) FOLDR#(z0,Cons(z1,z2)) -> c_6(FOLDR#(z0,z2)) ** Step 1.b:7: RemoveHeads. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: FOLD#(z0,z1) -> c_1(FOLDR#(z0,z1)) FOLD#(z0,z1) -> c_2(FOLDL#(z0,z1)) FOLDL#(z0,Cons(S(0()),z1)) -> c_3(FOLDL#(S(z0),z1)) FOLDL#(S(0()),Cons(z0,z1)) -> c_5(FOLDL#(S(z0),z1)) FOLDR#(z0,Cons(z1,z2)) -> c_6(FOLDR#(z0,z2)) - Signature: {FOLD/2,FOLDL/2,FOLDR/2,NOTEMPTY/1,OP/2,fold/2,foldl/2,foldr/2,notEmpty/1,op/2,FOLD#/2,FOLDL#/2,FOLDR#/2 ,NOTEMPTY#/1,OP#/2,fold#/2,foldl#/2,foldr#/2,notEmpty#/1,op#/2} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c/1 ,c1/1,c10/1,c2/0,c3/2,c4/0,c5/0,c6/0,c7/0,c8/0,c9/1,c_1/1,c_2/1,c_3/1,c_4/0,c_5/1,c_6/1,c_7/0,c_8/0,c_9/0 ,c_10/0,c_11/0,c_12/2,c_13/1,c_14/0,c_15/1,c_16/1,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0} - Obligation: innermost runtime complexity wrt. defined symbols {FOLD#,FOLDL#,FOLDR#,NOTEMPTY#,OP#,fold#,foldl#,foldr# ,notEmpty#,op#} and constructors {0,Cons,False,Nil,S,True,c,c1,c10,c2,c3,c4,c5,c6,c7,c8,c9} + Applied Processor: RemoveHeads + Details: Consider the dependency graph 1:S:FOLD#(z0,z1) -> c_1(FOLDR#(z0,z1)) -->_1 FOLDR#(z0,Cons(z1,z2)) -> c_6(FOLDR#(z0,z2)):5 2:S:FOLD#(z0,z1) -> c_2(FOLDL#(z0,z1)) -->_1 FOLDL#(S(0()),Cons(z0,z1)) -> c_5(FOLDL#(S(z0),z1)):4 -->_1 FOLDL#(z0,Cons(S(0()),z1)) -> c_3(FOLDL#(S(z0),z1)):3 3:S:FOLDL#(z0,Cons(S(0()),z1)) -> c_3(FOLDL#(S(z0),z1)) -->_1 FOLDL#(S(0()),Cons(z0,z1)) -> c_5(FOLDL#(S(z0),z1)):4 -->_1 FOLDL#(z0,Cons(S(0()),z1)) -> c_3(FOLDL#(S(z0),z1)):3 4:S:FOLDL#(S(0()),Cons(z0,z1)) -> c_5(FOLDL#(S(z0),z1)) -->_1 FOLDL#(S(0()),Cons(z0,z1)) -> c_5(FOLDL#(S(z0),z1)):4 -->_1 FOLDL#(z0,Cons(S(0()),z1)) -> c_3(FOLDL#(S(z0),z1)):3 5:S:FOLDR#(z0,Cons(z1,z2)) -> c_6(FOLDR#(z0,z2)) -->_1 FOLDR#(z0,Cons(z1,z2)) -> c_6(FOLDR#(z0,z2)):5 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). [(1,FOLD#(z0,z1) -> c_1(FOLDR#(z0,z1))),(2,FOLD#(z0,z1) -> c_2(FOLDL#(z0,z1)))] ** Step 1.b:8: Decompose. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: FOLDL#(z0,Cons(S(0()),z1)) -> c_3(FOLDL#(S(z0),z1)) FOLDL#(S(0()),Cons(z0,z1)) -> c_5(FOLDL#(S(z0),z1)) FOLDR#(z0,Cons(z1,z2)) -> c_6(FOLDR#(z0,z2)) - Signature: {FOLD/2,FOLDL/2,FOLDR/2,NOTEMPTY/1,OP/2,fold/2,foldl/2,foldr/2,notEmpty/1,op/2,FOLD#/2,FOLDL#/2,FOLDR#/2 ,NOTEMPTY#/1,OP#/2,fold#/2,foldl#/2,foldr#/2,notEmpty#/1,op#/2} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c/1 ,c1/1,c10/1,c2/0,c3/2,c4/0,c5/0,c6/0,c7/0,c8/0,c9/1,c_1/1,c_2/1,c_3/1,c_4/0,c_5/1,c_6/1,c_7/0,c_8/0,c_9/0 ,c_10/0,c_11/0,c_12/2,c_13/1,c_14/0,c_15/1,c_16/1,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0} - Obligation: innermost runtime complexity wrt. defined symbols {FOLD#,FOLDL#,FOLDR#,NOTEMPTY#,OP#,fold#,foldl#,foldr# ,notEmpty#,op#} and constructors {0,Cons,False,Nil,S,True,c,c1,c10,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: FOLDL#(z0,Cons(S(0()),z1)) -> c_3(FOLDL#(S(z0),z1)) FOLDL#(S(0()),Cons(z0,z1)) -> c_5(FOLDL#(S(z0),z1)) - Weak DPs: FOLDR#(z0,Cons(z1,z2)) -> c_6(FOLDR#(z0,z2)) - Signature: {FOLD/2,FOLDL/2,FOLDR/2,NOTEMPTY/1,OP/2,fold/2,foldl/2,foldr/2,notEmpty/1,op/2,FOLD#/2,FOLDL#/2,FOLDR#/2 ,NOTEMPTY#/1,OP#/2,fold#/2,foldl#/2,foldr#/2,notEmpty#/1,op#/2} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c/1 ,c1/1,c10/1,c2/0,c3/2,c4/0,c5/0,c6/0,c7/0,c8/0,c9/1,c_1/1,c_2/1,c_3/1,c_4/0,c_5/1,c_6/1,c_7/0,c_8/0,c_9/0 ,c_10/0,c_11/0,c_12/2,c_13/1,c_14/0,c_15/1,c_16/1,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0} - Obligation: innermost runtime complexity wrt. defined symbols {FOLD#,FOLDL#,FOLDR#,NOTEMPTY#,OP#,fold#,foldl#,foldr# ,notEmpty#,op#} and constructors {0,Cons,False,Nil,S,True,c,c1,c10,c2,c3,c4,c5,c6,c7,c8,c9} Problem (S) - Strict DPs: FOLDR#(z0,Cons(z1,z2)) -> c_6(FOLDR#(z0,z2)) - Weak DPs: FOLDL#(z0,Cons(S(0()),z1)) -> c_3(FOLDL#(S(z0),z1)) FOLDL#(S(0()),Cons(z0,z1)) -> c_5(FOLDL#(S(z0),z1)) - Signature: {FOLD/2,FOLDL/2,FOLDR/2,NOTEMPTY/1,OP/2,fold/2,foldl/2,foldr/2,notEmpty/1,op/2,FOLD#/2,FOLDL#/2,FOLDR#/2 ,NOTEMPTY#/1,OP#/2,fold#/2,foldl#/2,foldr#/2,notEmpty#/1,op#/2} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c/1 ,c1/1,c10/1,c2/0,c3/2,c4/0,c5/0,c6/0,c7/0,c8/0,c9/1,c_1/1,c_2/1,c_3/1,c_4/0,c_5/1,c_6/1,c_7/0,c_8/0,c_9/0 ,c_10/0,c_11/0,c_12/2,c_13/1,c_14/0,c_15/1,c_16/1,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0} - Obligation: innermost runtime complexity wrt. defined symbols {FOLD#,FOLDL#,FOLDR#,NOTEMPTY#,OP#,fold#,foldl#,foldr# ,notEmpty#,op#} and constructors {0,Cons,False,Nil,S,True,c,c1,c10,c2,c3,c4,c5,c6,c7,c8,c9} *** Step 1.b:8.a:1: RemoveWeakSuffixes. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: FOLDL#(z0,Cons(S(0()),z1)) -> c_3(FOLDL#(S(z0),z1)) FOLDL#(S(0()),Cons(z0,z1)) -> c_5(FOLDL#(S(z0),z1)) - Weak DPs: FOLDR#(z0,Cons(z1,z2)) -> c_6(FOLDR#(z0,z2)) - Signature: {FOLD/2,FOLDL/2,FOLDR/2,NOTEMPTY/1,OP/2,fold/2,foldl/2,foldr/2,notEmpty/1,op/2,FOLD#/2,FOLDL#/2,FOLDR#/2 ,NOTEMPTY#/1,OP#/2,fold#/2,foldl#/2,foldr#/2,notEmpty#/1,op#/2} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c/1 ,c1/1,c10/1,c2/0,c3/2,c4/0,c5/0,c6/0,c7/0,c8/0,c9/1,c_1/1,c_2/1,c_3/1,c_4/0,c_5/1,c_6/1,c_7/0,c_8/0,c_9/0 ,c_10/0,c_11/0,c_12/2,c_13/1,c_14/0,c_15/1,c_16/1,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0} - Obligation: innermost runtime complexity wrt. defined symbols {FOLD#,FOLDL#,FOLDR#,NOTEMPTY#,OP#,fold#,foldl#,foldr# ,notEmpty#,op#} and constructors {0,Cons,False,Nil,S,True,c,c1,c10,c2,c3,c4,c5,c6,c7,c8,c9} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 3:S:FOLDL#(z0,Cons(S(0()),z1)) -> c_3(FOLDL#(S(z0),z1)) -->_1 FOLDL#(S(0()),Cons(z0,z1)) -> c_5(FOLDL#(S(z0),z1)):4 -->_1 FOLDL#(z0,Cons(S(0()),z1)) -> c_3(FOLDL#(S(z0),z1)):3 4:S:FOLDL#(S(0()),Cons(z0,z1)) -> c_5(FOLDL#(S(z0),z1)) -->_1 FOLDL#(z0,Cons(S(0()),z1)) -> c_3(FOLDL#(S(z0),z1)):3 -->_1 FOLDL#(S(0()),Cons(z0,z1)) -> c_5(FOLDL#(S(z0),z1)):4 5:W:FOLDR#(z0,Cons(z1,z2)) -> c_6(FOLDR#(z0,z2)) -->_1 FOLDR#(z0,Cons(z1,z2)) -> c_6(FOLDR#(z0,z2)):5 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 5: FOLDR#(z0,Cons(z1,z2)) -> c_6(FOLDR#(z0,z2)) *** Step 1.b:8.a:2: PredecessorEstimationCP. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: FOLDL#(z0,Cons(S(0()),z1)) -> c_3(FOLDL#(S(z0),z1)) FOLDL#(S(0()),Cons(z0,z1)) -> c_5(FOLDL#(S(z0),z1)) - Signature: {FOLD/2,FOLDL/2,FOLDR/2,NOTEMPTY/1,OP/2,fold/2,foldl/2,foldr/2,notEmpty/1,op/2,FOLD#/2,FOLDL#/2,FOLDR#/2 ,NOTEMPTY#/1,OP#/2,fold#/2,foldl#/2,foldr#/2,notEmpty#/1,op#/2} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c/1 ,c1/1,c10/1,c2/0,c3/2,c4/0,c5/0,c6/0,c7/0,c8/0,c9/1,c_1/1,c_2/1,c_3/1,c_4/0,c_5/1,c_6/1,c_7/0,c_8/0,c_9/0 ,c_10/0,c_11/0,c_12/2,c_13/1,c_14/0,c_15/1,c_16/1,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0} - Obligation: innermost runtime complexity wrt. defined symbols {FOLD#,FOLDL#,FOLDR#,NOTEMPTY#,OP#,fold#,foldl#,foldr# ,notEmpty#,op#} and constructors {0,Cons,False,Nil,S,True,c,c1,c10,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: 3: FOLDL#(z0,Cons(S(0()),z1)) -> c_3(FOLDL#(S(z0),z1)) 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: FOLDL#(z0,Cons(S(0()),z1)) -> c_3(FOLDL#(S(z0),z1)) FOLDL#(S(0()),Cons(z0,z1)) -> c_5(FOLDL#(S(z0),z1)) - Signature: {FOLD/2,FOLDL/2,FOLDR/2,NOTEMPTY/1,OP/2,fold/2,foldl/2,foldr/2,notEmpty/1,op/2,FOLD#/2,FOLDL#/2,FOLDR#/2 ,NOTEMPTY#/1,OP#/2,fold#/2,foldl#/2,foldr#/2,notEmpty#/1,op#/2} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c/1 ,c1/1,c10/1,c2/0,c3/2,c4/0,c5/0,c6/0,c7/0,c8/0,c9/1,c_1/1,c_2/1,c_3/1,c_4/0,c_5/1,c_6/1,c_7/0,c_8/0,c_9/0 ,c_10/0,c_11/0,c_12/2,c_13/1,c_14/0,c_15/1,c_16/1,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0} - Obligation: innermost runtime complexity wrt. defined symbols {FOLD#,FOLDL#,FOLDR#,NOTEMPTY#,OP#,fold#,foldl#,foldr# ,notEmpty#,op#} and constructors {0,Cons,False,Nil,S,True,c,c1,c10,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_3) = {1}, uargs(c_5) = {1} Following symbols are considered usable: {FOLD#,FOLDL#,FOLDR#,NOTEMPTY#,OP#,fold#,foldl#,foldr#,notEmpty#,op#} TcT has computed the following interpretation: p(0) = [1] p(Cons) = [1] x1 + [1] x2 + [0] p(FOLD) = [2] x1 + [0] p(FOLDL) = [4] x2 + [0] p(FOLDR) = [8] x1 + [1] p(False) = [0] p(NOTEMPTY) = [1] x1 + [0] p(Nil) = [0] p(OP) = [4] p(S) = [4] p(True) = [0] p(c) = [2] p(c1) = [0] p(c10) = [1] p(c2) = [0] p(c3) = [1] p(c4) = [2] p(c5) = [2] p(c6) = [1] p(c7) = [1] p(c8) = [2] p(c9) = [1] x1 + [8] p(fold) = [1] x1 + [0] p(foldl) = [1] x2 + [0] p(foldr) = [4] x2 + [2] p(notEmpty) = [1] x1 + [0] p(op) = [1] x1 + [1] p(FOLD#) = [1] x1 + [1] p(FOLDL#) = [4] x2 + [0] p(FOLDR#) = [8] p(NOTEMPTY#) = [8] p(OP#) = [2] x1 + [0] p(fold#) = [1] x1 + [1] p(foldl#) = [1] p(foldr#) = [2] x2 + [1] p(notEmpty#) = [1] x1 + [0] p(op#) = [2] x2 + [0] p(c_1) = [1] p(c_2) = [2] x1 + [0] p(c_3) = [1] x1 + [14] p(c_4) = [2] p(c_5) = [1] x1 + [0] p(c_6) = [0] p(c_7) = [1] p(c_8) = [2] p(c_9) = [1] p(c_10) = [4] p(c_11) = [1] p(c_12) = [1] x1 + [1] p(c_13) = [2] x1 + [8] p(c_14) = [1] p(c_15) = [1] x1 + [0] p(c_16) = [1] x1 + [2] p(c_17) = [1] p(c_18) = [1] p(c_19) = [2] p(c_20) = [2] p(c_21) = [1] Following rules are strictly oriented: FOLDL#(z0,Cons(S(0()),z1)) = [4] z1 + [16] > [4] z1 + [14] = c_3(FOLDL#(S(z0),z1)) Following rules are (at-least) weakly oriented: FOLDL#(S(0()),Cons(z0,z1)) = [4] z0 + [4] z1 + [0] >= [4] z1 + [0] = c_5(FOLDL#(S(z0),z1)) **** Step 1.b:8.a:2.a:2: Assumption. WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: FOLDL#(S(0()),Cons(z0,z1)) -> c_5(FOLDL#(S(z0),z1)) - Weak DPs: FOLDL#(z0,Cons(S(0()),z1)) -> c_3(FOLDL#(S(z0),z1)) - Signature: {FOLD/2,FOLDL/2,FOLDR/2,NOTEMPTY/1,OP/2,fold/2,foldl/2,foldr/2,notEmpty/1,op/2,FOLD#/2,FOLDL#/2,FOLDR#/2 ,NOTEMPTY#/1,OP#/2,fold#/2,foldl#/2,foldr#/2,notEmpty#/1,op#/2} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c/1 ,c1/1,c10/1,c2/0,c3/2,c4/0,c5/0,c6/0,c7/0,c8/0,c9/1,c_1/1,c_2/1,c_3/1,c_4/0,c_5/1,c_6/1,c_7/0,c_8/0,c_9/0 ,c_10/0,c_11/0,c_12/2,c_13/1,c_14/0,c_15/1,c_16/1,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0} - Obligation: innermost runtime complexity wrt. defined symbols {FOLD#,FOLDL#,FOLDR#,NOTEMPTY#,OP#,fold#,foldl#,foldr# ,notEmpty#,op#} and constructors {0,Cons,False,Nil,S,True,c,c1,c10,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: PredecessorEstimationCP. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: FOLDL#(S(0()),Cons(z0,z1)) -> c_5(FOLDL#(S(z0),z1)) - Weak DPs: FOLDL#(z0,Cons(S(0()),z1)) -> c_3(FOLDL#(S(z0),z1)) - Signature: {FOLD/2,FOLDL/2,FOLDR/2,NOTEMPTY/1,OP/2,fold/2,foldl/2,foldr/2,notEmpty/1,op/2,FOLD#/2,FOLDL#/2,FOLDR#/2 ,NOTEMPTY#/1,OP#/2,fold#/2,foldl#/2,foldr#/2,notEmpty#/1,op#/2} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c/1 ,c1/1,c10/1,c2/0,c3/2,c4/0,c5/0,c6/0,c7/0,c8/0,c9/1,c_1/1,c_2/1,c_3/1,c_4/0,c_5/1,c_6/1,c_7/0,c_8/0,c_9/0 ,c_10/0,c_11/0,c_12/2,c_13/1,c_14/0,c_15/1,c_16/1,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0} - Obligation: innermost runtime complexity wrt. defined symbols {FOLD#,FOLDL#,FOLDR#,NOTEMPTY#,OP#,fold#,foldl#,foldr# ,notEmpty#,op#} and constructors {0,Cons,False,Nil,S,True,c,c1,c10,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: FOLDL#(S(0()),Cons(z0,z1)) -> c_5(FOLDL#(S(z0),z1)) The strictly oriented rules are moved into the weak component. ***** Step 1.b:8.a:2.b:1.a:1: NaturalMI. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: FOLDL#(S(0()),Cons(z0,z1)) -> c_5(FOLDL#(S(z0),z1)) - Weak DPs: FOLDL#(z0,Cons(S(0()),z1)) -> c_3(FOLDL#(S(z0),z1)) - Signature: {FOLD/2,FOLDL/2,FOLDR/2,NOTEMPTY/1,OP/2,fold/2,foldl/2,foldr/2,notEmpty/1,op/2,FOLD#/2,FOLDL#/2,FOLDR#/2 ,NOTEMPTY#/1,OP#/2,fold#/2,foldl#/2,foldr#/2,notEmpty#/1,op#/2} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c/1 ,c1/1,c10/1,c2/0,c3/2,c4/0,c5/0,c6/0,c7/0,c8/0,c9/1,c_1/1,c_2/1,c_3/1,c_4/0,c_5/1,c_6/1,c_7/0,c_8/0,c_9/0 ,c_10/0,c_11/0,c_12/2,c_13/1,c_14/0,c_15/1,c_16/1,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0} - Obligation: innermost runtime complexity wrt. defined symbols {FOLD#,FOLDL#,FOLDR#,NOTEMPTY#,OP#,fold#,foldl#,foldr# ,notEmpty#,op#} and constructors {0,Cons,False,Nil,S,True,c,c1,c10,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_3) = {1}, uargs(c_5) = {1} Following symbols are considered usable: {FOLD#,FOLDL#,FOLDR#,NOTEMPTY#,OP#,fold#,foldl#,foldr#,notEmpty#,op#} TcT has computed the following interpretation: p(0) = [1] p(Cons) = [1] x1 + [1] x2 + [0] p(FOLD) = [2] x1 + [1] x2 + [2] p(FOLDL) = [1] p(FOLDR) = [2] x2 + [1] p(False) = [1] p(NOTEMPTY) = [0] p(Nil) = [0] p(OP) = [1] x1 + [1] p(S) = [1] x1 + [2] p(True) = [1] p(c) = [1] x1 + [0] p(c1) = [0] p(c10) = [1] p(c2) = [2] p(c3) = [1] x1 + [1] x2 + [0] p(c4) = [1] p(c5) = [1] p(c6) = [0] p(c7) = [1] p(c8) = [2] p(c9) = [1] x1 + [1] p(fold) = [0] p(foldl) = [1] p(foldr) = [1] x2 + [1] p(notEmpty) = [1] p(op) = [1] x1 + [1] p(FOLD#) = [1] x2 + [1] p(FOLDL#) = [8] x1 + [8] x2 + [0] p(FOLDR#) = [1] x2 + [0] p(NOTEMPTY#) = [1] p(OP#) = [1] x1 + [1] p(fold#) = [1] x1 + [1] x2 + [1] p(foldl#) = [1] p(foldr#) = [8] x2 + [0] p(notEmpty#) = [1] x1 + [2] p(op#) = [8] p(c_1) = [1] x1 + [0] p(c_2) = [1] x1 + [2] p(c_3) = [1] x1 + [1] p(c_4) = [0] p(c_5) = [1] x1 + [6] p(c_6) = [2] p(c_7) = [0] p(c_8) = [1] p(c_9) = [1] p(c_10) = [8] p(c_11) = [1] p(c_12) = [1] x1 + [0] p(c_13) = [1] x1 + [1] p(c_14) = [0] p(c_15) = [1] p(c_16) = [8] p(c_17) = [1] p(c_18) = [8] p(c_19) = [1] p(c_20) = [1] p(c_21) = [0] Following rules are strictly oriented: FOLDL#(S(0()),Cons(z0,z1)) = [8] z0 + [8] z1 + [24] > [8] z0 + [8] z1 + [22] = c_5(FOLDL#(S(z0),z1)) Following rules are (at-least) weakly oriented: FOLDL#(z0,Cons(S(0()),z1)) = [8] z0 + [8] z1 + [24] >= [8] z0 + [8] z1 + [17] = c_3(FOLDL#(S(z0),z1)) ***** Step 1.b:8.a:2.b:1.a:2: Assumption. WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: FOLDL#(z0,Cons(S(0()),z1)) -> c_3(FOLDL#(S(z0),z1)) FOLDL#(S(0()),Cons(z0,z1)) -> c_5(FOLDL#(S(z0),z1)) - Signature: {FOLD/2,FOLDL/2,FOLDR/2,NOTEMPTY/1,OP/2,fold/2,foldl/2,foldr/2,notEmpty/1,op/2,FOLD#/2,FOLDL#/2,FOLDR#/2 ,NOTEMPTY#/1,OP#/2,fold#/2,foldl#/2,foldr#/2,notEmpty#/1,op#/2} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c/1 ,c1/1,c10/1,c2/0,c3/2,c4/0,c5/0,c6/0,c7/0,c8/0,c9/1,c_1/1,c_2/1,c_3/1,c_4/0,c_5/1,c_6/1,c_7/0,c_8/0,c_9/0 ,c_10/0,c_11/0,c_12/2,c_13/1,c_14/0,c_15/1,c_16/1,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0} - Obligation: innermost runtime complexity wrt. defined symbols {FOLD#,FOLDL#,FOLDR#,NOTEMPTY#,OP#,fold#,foldl#,foldr# ,notEmpty#,op#} and constructors {0,Cons,False,Nil,S,True,c,c1,c10,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.b:1: RemoveWeakSuffixes. WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: FOLDL#(z0,Cons(S(0()),z1)) -> c_3(FOLDL#(S(z0),z1)) FOLDL#(S(0()),Cons(z0,z1)) -> c_5(FOLDL#(S(z0),z1)) - Signature: {FOLD/2,FOLDL/2,FOLDR/2,NOTEMPTY/1,OP/2,fold/2,foldl/2,foldr/2,notEmpty/1,op/2,FOLD#/2,FOLDL#/2,FOLDR#/2 ,NOTEMPTY#/1,OP#/2,fold#/2,foldl#/2,foldr#/2,notEmpty#/1,op#/2} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c/1 ,c1/1,c10/1,c2/0,c3/2,c4/0,c5/0,c6/0,c7/0,c8/0,c9/1,c_1/1,c_2/1,c_3/1,c_4/0,c_5/1,c_6/1,c_7/0,c_8/0,c_9/0 ,c_10/0,c_11/0,c_12/2,c_13/1,c_14/0,c_15/1,c_16/1,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0} - Obligation: innermost runtime complexity wrt. defined symbols {FOLD#,FOLDL#,FOLDR#,NOTEMPTY#,OP#,fold#,foldl#,foldr# ,notEmpty#,op#} and constructors {0,Cons,False,Nil,S,True,c,c1,c10,c2,c3,c4,c5,c6,c7,c8,c9} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:W:FOLDL#(z0,Cons(S(0()),z1)) -> c_3(FOLDL#(S(z0),z1)) -->_1 FOLDL#(S(0()),Cons(z0,z1)) -> c_5(FOLDL#(S(z0),z1)):2 -->_1 FOLDL#(z0,Cons(S(0()),z1)) -> c_3(FOLDL#(S(z0),z1)):1 2:W:FOLDL#(S(0()),Cons(z0,z1)) -> c_5(FOLDL#(S(z0),z1)) -->_1 FOLDL#(S(0()),Cons(z0,z1)) -> c_5(FOLDL#(S(z0),z1)):2 -->_1 FOLDL#(z0,Cons(S(0()),z1)) -> c_3(FOLDL#(S(z0),z1)):1 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 1: FOLDL#(z0,Cons(S(0()),z1)) -> c_3(FOLDL#(S(z0),z1)) 2: FOLDL#(S(0()),Cons(z0,z1)) -> c_5(FOLDL#(S(z0),z1)) ***** Step 1.b:8.a:2.b:1.b:2: EmptyProcessor. WORST_CASE(?,O(1)) + Considered Problem: - Signature: {FOLD/2,FOLDL/2,FOLDR/2,NOTEMPTY/1,OP/2,fold/2,foldl/2,foldr/2,notEmpty/1,op/2,FOLD#/2,FOLDL#/2,FOLDR#/2 ,NOTEMPTY#/1,OP#/2,fold#/2,foldl#/2,foldr#/2,notEmpty#/1,op#/2} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c/1 ,c1/1,c10/1,c2/0,c3/2,c4/0,c5/0,c6/0,c7/0,c8/0,c9/1,c_1/1,c_2/1,c_3/1,c_4/0,c_5/1,c_6/1,c_7/0,c_8/0,c_9/0 ,c_10/0,c_11/0,c_12/2,c_13/1,c_14/0,c_15/1,c_16/1,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0} - Obligation: innermost runtime complexity wrt. defined symbols {FOLD#,FOLDL#,FOLDR#,NOTEMPTY#,OP#,fold#,foldl#,foldr# ,notEmpty#,op#} and constructors {0,Cons,False,Nil,S,True,c,c1,c10,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: FOLDR#(z0,Cons(z1,z2)) -> c_6(FOLDR#(z0,z2)) - Weak DPs: FOLDL#(z0,Cons(S(0()),z1)) -> c_3(FOLDL#(S(z0),z1)) FOLDL#(S(0()),Cons(z0,z1)) -> c_5(FOLDL#(S(z0),z1)) - Signature: {FOLD/2,FOLDL/2,FOLDR/2,NOTEMPTY/1,OP/2,fold/2,foldl/2,foldr/2,notEmpty/1,op/2,FOLD#/2,FOLDL#/2,FOLDR#/2 ,NOTEMPTY#/1,OP#/2,fold#/2,foldl#/2,foldr#/2,notEmpty#/1,op#/2} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c/1 ,c1/1,c10/1,c2/0,c3/2,c4/0,c5/0,c6/0,c7/0,c8/0,c9/1,c_1/1,c_2/1,c_3/1,c_4/0,c_5/1,c_6/1,c_7/0,c_8/0,c_9/0 ,c_10/0,c_11/0,c_12/2,c_13/1,c_14/0,c_15/1,c_16/1,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0} - Obligation: innermost runtime complexity wrt. defined symbols {FOLD#,FOLDL#,FOLDR#,NOTEMPTY#,OP#,fold#,foldl#,foldr# ,notEmpty#,op#} and constructors {0,Cons,False,Nil,S,True,c,c1,c10,c2,c3,c4,c5,c6,c7,c8,c9} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:FOLDR#(z0,Cons(z1,z2)) -> c_6(FOLDR#(z0,z2)) -->_1 FOLDR#(z0,Cons(z1,z2)) -> c_6(FOLDR#(z0,z2)):1 2:W:FOLDL#(z0,Cons(S(0()),z1)) -> c_3(FOLDL#(S(z0),z1)) -->_1 FOLDL#(S(0()),Cons(z0,z1)) -> c_5(FOLDL#(S(z0),z1)):3 -->_1 FOLDL#(z0,Cons(S(0()),z1)) -> c_3(FOLDL#(S(z0),z1)):2 3:W:FOLDL#(S(0()),Cons(z0,z1)) -> c_5(FOLDL#(S(z0),z1)) -->_1 FOLDL#(S(0()),Cons(z0,z1)) -> c_5(FOLDL#(S(z0),z1)):3 -->_1 FOLDL#(z0,Cons(S(0()),z1)) -> c_3(FOLDL#(S(z0),z1)):2 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 2: FOLDL#(z0,Cons(S(0()),z1)) -> c_3(FOLDL#(S(z0),z1)) 3: FOLDL#(S(0()),Cons(z0,z1)) -> c_5(FOLDL#(S(z0),z1)) *** Step 1.b:8.b:2: PredecessorEstimationCP. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: FOLDR#(z0,Cons(z1,z2)) -> c_6(FOLDR#(z0,z2)) - Signature: {FOLD/2,FOLDL/2,FOLDR/2,NOTEMPTY/1,OP/2,fold/2,foldl/2,foldr/2,notEmpty/1,op/2,FOLD#/2,FOLDL#/2,FOLDR#/2 ,NOTEMPTY#/1,OP#/2,fold#/2,foldl#/2,foldr#/2,notEmpty#/1,op#/2} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c/1 ,c1/1,c10/1,c2/0,c3/2,c4/0,c5/0,c6/0,c7/0,c8/0,c9/1,c_1/1,c_2/1,c_3/1,c_4/0,c_5/1,c_6/1,c_7/0,c_8/0,c_9/0 ,c_10/0,c_11/0,c_12/2,c_13/1,c_14/0,c_15/1,c_16/1,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0} - Obligation: innermost runtime complexity wrt. defined symbols {FOLD#,FOLDL#,FOLDR#,NOTEMPTY#,OP#,fold#,foldl#,foldr# ,notEmpty#,op#} and constructors {0,Cons,False,Nil,S,True,c,c1,c10,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: FOLDR#(z0,Cons(z1,z2)) -> c_6(FOLDR#(z0,z2)) 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: FOLDR#(z0,Cons(z1,z2)) -> c_6(FOLDR#(z0,z2)) - Signature: {FOLD/2,FOLDL/2,FOLDR/2,NOTEMPTY/1,OP/2,fold/2,foldl/2,foldr/2,notEmpty/1,op/2,FOLD#/2,FOLDL#/2,FOLDR#/2 ,NOTEMPTY#/1,OP#/2,fold#/2,foldl#/2,foldr#/2,notEmpty#/1,op#/2} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c/1 ,c1/1,c10/1,c2/0,c3/2,c4/0,c5/0,c6/0,c7/0,c8/0,c9/1,c_1/1,c_2/1,c_3/1,c_4/0,c_5/1,c_6/1,c_7/0,c_8/0,c_9/0 ,c_10/0,c_11/0,c_12/2,c_13/1,c_14/0,c_15/1,c_16/1,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0} - Obligation: innermost runtime complexity wrt. defined symbols {FOLD#,FOLDL#,FOLDR#,NOTEMPTY#,OP#,fold#,foldl#,foldr# ,notEmpty#,op#} and constructors {0,Cons,False,Nil,S,True,c,c1,c10,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: {FOLD#,FOLDL#,FOLDR#,NOTEMPTY#,OP#,fold#,foldl#,foldr#,notEmpty#,op#} TcT has computed the following interpretation: p(0) = [0] p(Cons) = [1] x1 + [1] x2 + [8] p(FOLD) = [1] x1 + [0] p(FOLDL) = [0] p(FOLDR) = [0] p(False) = [1] p(NOTEMPTY) = [1] x1 + [1] p(Nil) = [0] p(OP) = [1] x1 + [0] p(S) = [1] x1 + [1] p(True) = [0] p(c) = [1] x1 + [0] p(c1) = [1] x1 + [0] p(c10) = [1] x1 + [0] p(c2) = [0] p(c3) = [1] x1 + [1] x2 + [0] p(c4) = [0] p(c5) = [0] p(c6) = [0] p(c7) = [0] p(c8) = [0] p(c9) = [1] x1 + [0] p(fold) = [0] p(foldl) = [0] p(foldr) = [0] p(notEmpty) = [0] p(op) = [0] p(FOLD#) = [0] p(FOLDL#) = [0] p(FOLDR#) = [2] x2 + [8] p(NOTEMPTY#) = [0] p(OP#) = [0] p(fold#) = [0] p(foldl#) = [0] p(foldr#) = [1] p(notEmpty#) = [0] p(op#) = [0] p(c_1) = [0] p(c_2) = [0] p(c_3) = [0] p(c_4) = [0] p(c_5) = [0] p(c_6) = [1] x1 + [4] p(c_7) = [0] p(c_8) = [0] p(c_9) = [0] p(c_10) = [0] p(c_11) = [0] p(c_12) = [2] x1 + [1] x2 + [0] p(c_13) = [0] p(c_14) = [0] p(c_15) = [0] p(c_16) = [2] x1 + [0] p(c_17) = [0] p(c_18) = [0] p(c_19) = [2] p(c_20) = [0] p(c_21) = [1] Following rules are strictly oriented: FOLDR#(z0,Cons(z1,z2)) = [2] z1 + [2] z2 + [24] > [2] z2 + [12] = c_6(FOLDR#(z0,z2)) Following rules are (at-least) weakly oriented: **** Step 1.b:8.b:2.a:2: Assumption. WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: FOLDR#(z0,Cons(z1,z2)) -> c_6(FOLDR#(z0,z2)) - Signature: {FOLD/2,FOLDL/2,FOLDR/2,NOTEMPTY/1,OP/2,fold/2,foldl/2,foldr/2,notEmpty/1,op/2,FOLD#/2,FOLDL#/2,FOLDR#/2 ,NOTEMPTY#/1,OP#/2,fold#/2,foldl#/2,foldr#/2,notEmpty#/1,op#/2} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c/1 ,c1/1,c10/1,c2/0,c3/2,c4/0,c5/0,c6/0,c7/0,c8/0,c9/1,c_1/1,c_2/1,c_3/1,c_4/0,c_5/1,c_6/1,c_7/0,c_8/0,c_9/0 ,c_10/0,c_11/0,c_12/2,c_13/1,c_14/0,c_15/1,c_16/1,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0} - Obligation: innermost runtime complexity wrt. defined symbols {FOLD#,FOLDL#,FOLDR#,NOTEMPTY#,OP#,fold#,foldl#,foldr# ,notEmpty#,op#} and constructors {0,Cons,False,Nil,S,True,c,c1,c10,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: FOLDR#(z0,Cons(z1,z2)) -> c_6(FOLDR#(z0,z2)) - Signature: {FOLD/2,FOLDL/2,FOLDR/2,NOTEMPTY/1,OP/2,fold/2,foldl/2,foldr/2,notEmpty/1,op/2,FOLD#/2,FOLDL#/2,FOLDR#/2 ,NOTEMPTY#/1,OP#/2,fold#/2,foldl#/2,foldr#/2,notEmpty#/1,op#/2} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c/1 ,c1/1,c10/1,c2/0,c3/2,c4/0,c5/0,c6/0,c7/0,c8/0,c9/1,c_1/1,c_2/1,c_3/1,c_4/0,c_5/1,c_6/1,c_7/0,c_8/0,c_9/0 ,c_10/0,c_11/0,c_12/2,c_13/1,c_14/0,c_15/1,c_16/1,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0} - Obligation: innermost runtime complexity wrt. defined symbols {FOLD#,FOLDL#,FOLDR#,NOTEMPTY#,OP#,fold#,foldl#,foldr# ,notEmpty#,op#} and constructors {0,Cons,False,Nil,S,True,c,c1,c10,c2,c3,c4,c5,c6,c7,c8,c9} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:W:FOLDR#(z0,Cons(z1,z2)) -> c_6(FOLDR#(z0,z2)) -->_1 FOLDR#(z0,Cons(z1,z2)) -> c_6(FOLDR#(z0,z2)):1 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 1: FOLDR#(z0,Cons(z1,z2)) -> c_6(FOLDR#(z0,z2)) **** Step 1.b:8.b:2.b:2: EmptyProcessor. WORST_CASE(?,O(1)) + Considered Problem: - Signature: {FOLD/2,FOLDL/2,FOLDR/2,NOTEMPTY/1,OP/2,fold/2,foldl/2,foldr/2,notEmpty/1,op/2,FOLD#/2,FOLDL#/2,FOLDR#/2 ,NOTEMPTY#/1,OP#/2,fold#/2,foldl#/2,foldr#/2,notEmpty#/1,op#/2} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0,c/1 ,c1/1,c10/1,c2/0,c3/2,c4/0,c5/0,c6/0,c7/0,c8/0,c9/1,c_1/1,c_2/1,c_3/1,c_4/0,c_5/1,c_6/1,c_7/0,c_8/0,c_9/0 ,c_10/0,c_11/0,c_12/2,c_13/1,c_14/0,c_15/1,c_16/1,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0} - Obligation: innermost runtime complexity wrt. defined symbols {FOLD#,FOLDL#,FOLDR#,NOTEMPTY#,OP#,fold#,foldl#,foldr# ,notEmpty#,op#} and constructors {0,Cons,False,Nil,S,True,c,c1,c10,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))