WORST_CASE(Omega(n^1),O(n^2)) * Step 1: Sum. WORST_CASE(Omega(n^1),O(n^2)) + Considered Problem: - Strict TRS: -'(z0,0()) -> c() -'(0(),s(z0)) -> c1() -'(s(z0),s(z1)) -> c2(-'(z0,z1)) DIV(z0,0()) -> c8() DIV(0(),z0) -> c9() DIV(s(z0),s(z1)) -> c10(IF(lt(z0,z1),0(),s(div(-(z0,z1),s(z1)))),LT(z0,z1)) DIV(s(z0),s(z1)) -> c11(IF(lt(z0,z1),0(),s(div(-(z0,z1),s(z1)))),DIV(-(z0,z1),s(z1)),-'(z0,z1)) IF(false(),z0,z1) -> c7() IF(true(),z0,z1) -> c6() LT(z0,0()) -> c3() LT(0(),s(z0)) -> c4() LT(s(z0),s(z1)) -> c5(LT(z0,z1)) - Weak TRS: -(z0,0()) -> z0 -(0(),s(z0)) -> 0() -(s(z0),s(z1)) -> -(z0,z1) div(z0,0()) -> 0() div(0(),z0) -> 0() div(s(z0),s(z1)) -> if(lt(z0,z1),0(),s(div(-(z0,z1),s(z1)))) if(false(),z0,z1) -> z1 if(true(),z0,z1) -> z0 lt(z0,0()) -> false() lt(0(),s(z0)) -> true() lt(s(z0),s(z1)) -> lt(z0,z1) - Signature: {-/2,-'/2,DIV/2,IF/3,LT/2,div/2,if/3,lt/2} / {0/0,c/0,c1/0,c10/2,c11/3,c2/1,c3/0,c4/0,c5/1,c6/0,c7/0,c8/0 ,c9/0,false/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {-,-',DIV,IF,LT,div,if,lt} and constructors {0,c,c1,c10 ,c11,c2,c3,c4,c5,c6,c7,c8,c9,false,s,true} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: -'(z0,0()) -> c() -'(0(),s(z0)) -> c1() -'(s(z0),s(z1)) -> c2(-'(z0,z1)) DIV(z0,0()) -> c8() DIV(0(),z0) -> c9() DIV(s(z0),s(z1)) -> c10(IF(lt(z0,z1),0(),s(div(-(z0,z1),s(z1)))),LT(z0,z1)) DIV(s(z0),s(z1)) -> c11(IF(lt(z0,z1),0(),s(div(-(z0,z1),s(z1)))),DIV(-(z0,z1),s(z1)),-'(z0,z1)) IF(false(),z0,z1) -> c7() IF(true(),z0,z1) -> c6() LT(z0,0()) -> c3() LT(0(),s(z0)) -> c4() LT(s(z0),s(z1)) -> c5(LT(z0,z1)) - Weak TRS: -(z0,0()) -> z0 -(0(),s(z0)) -> 0() -(s(z0),s(z1)) -> -(z0,z1) div(z0,0()) -> 0() div(0(),z0) -> 0() div(s(z0),s(z1)) -> if(lt(z0,z1),0(),s(div(-(z0,z1),s(z1)))) if(false(),z0,z1) -> z1 if(true(),z0,z1) -> z0 lt(z0,0()) -> false() lt(0(),s(z0)) -> true() lt(s(z0),s(z1)) -> lt(z0,z1) - Signature: {-/2,-'/2,DIV/2,IF/3,LT/2,div/2,if/3,lt/2} / {0/0,c/0,c1/0,c10/2,c11/3,c2/1,c3/0,c4/0,c5/1,c6/0,c7/0,c8/0 ,c9/0,false/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {-,-',DIV,IF,LT,div,if,lt} and constructors {0,c,c1,c10 ,c11,c2,c3,c4,c5,c6,c7,c8,c9,false,s,true} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:2: DecreasingLoops. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: -'(z0,0()) -> c() -'(0(),s(z0)) -> c1() -'(s(z0),s(z1)) -> c2(-'(z0,z1)) DIV(z0,0()) -> c8() DIV(0(),z0) -> c9() DIV(s(z0),s(z1)) -> c10(IF(lt(z0,z1),0(),s(div(-(z0,z1),s(z1)))),LT(z0,z1)) DIV(s(z0),s(z1)) -> c11(IF(lt(z0,z1),0(),s(div(-(z0,z1),s(z1)))),DIV(-(z0,z1),s(z1)),-'(z0,z1)) IF(false(),z0,z1) -> c7() IF(true(),z0,z1) -> c6() LT(z0,0()) -> c3() LT(0(),s(z0)) -> c4() LT(s(z0),s(z1)) -> c5(LT(z0,z1)) - Weak TRS: -(z0,0()) -> z0 -(0(),s(z0)) -> 0() -(s(z0),s(z1)) -> -(z0,z1) div(z0,0()) -> 0() div(0(),z0) -> 0() div(s(z0),s(z1)) -> if(lt(z0,z1),0(),s(div(-(z0,z1),s(z1)))) if(false(),z0,z1) -> z1 if(true(),z0,z1) -> z0 lt(z0,0()) -> false() lt(0(),s(z0)) -> true() lt(s(z0),s(z1)) -> lt(z0,z1) - Signature: {-/2,-'/2,DIV/2,IF/3,LT/2,div/2,if/3,lt/2} / {0/0,c/0,c1/0,c10/2,c11/3,c2/1,c3/0,c4/0,c5/1,c6/0,c7/0,c8/0 ,c9/0,false/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {-,-',DIV,IF,LT,div,if,lt} and constructors {0,c,c1,c10 ,c11,c2,c3,c4,c5,c6,c7,c8,c9,false,s,true} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: -'(x,y){x -> s(x),y -> s(y)} = -'(s(x),s(y)) ->^+ c2(-'(x,y)) = C[-'(x,y) = -'(x,y){}] ** Step 1.b:1: DependencyPairs. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: -'(z0,0()) -> c() -'(0(),s(z0)) -> c1() -'(s(z0),s(z1)) -> c2(-'(z0,z1)) DIV(z0,0()) -> c8() DIV(0(),z0) -> c9() DIV(s(z0),s(z1)) -> c10(IF(lt(z0,z1),0(),s(div(-(z0,z1),s(z1)))),LT(z0,z1)) DIV(s(z0),s(z1)) -> c11(IF(lt(z0,z1),0(),s(div(-(z0,z1),s(z1)))),DIV(-(z0,z1),s(z1)),-'(z0,z1)) IF(false(),z0,z1) -> c7() IF(true(),z0,z1) -> c6() LT(z0,0()) -> c3() LT(0(),s(z0)) -> c4() LT(s(z0),s(z1)) -> c5(LT(z0,z1)) - Weak TRS: -(z0,0()) -> z0 -(0(),s(z0)) -> 0() -(s(z0),s(z1)) -> -(z0,z1) div(z0,0()) -> 0() div(0(),z0) -> 0() div(s(z0),s(z1)) -> if(lt(z0,z1),0(),s(div(-(z0,z1),s(z1)))) if(false(),z0,z1) -> z1 if(true(),z0,z1) -> z0 lt(z0,0()) -> false() lt(0(),s(z0)) -> true() lt(s(z0),s(z1)) -> lt(z0,z1) - Signature: {-/2,-'/2,DIV/2,IF/3,LT/2,div/2,if/3,lt/2} / {0/0,c/0,c1/0,c10/2,c11/3,c2/1,c3/0,c4/0,c5/1,c6/0,c7/0,c8/0 ,c9/0,false/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {-,-',DIV,IF,LT,div,if,lt} and constructors {0,c,c1,c10 ,c11,c2,c3,c4,c5,c6,c7,c8,c9,false,s,true} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs -'#(z0,0()) -> c_1() -'#(0(),s(z0)) -> c_2() -'#(s(z0),s(z1)) -> c_3(-'#(z0,z1)) DIV#(z0,0()) -> c_4() DIV#(0(),z0) -> c_5() DIV#(s(z0),s(z1)) -> c_6(IF#(lt(z0,z1),0(),s(div(-(z0,z1),s(z1)))) ,lt#(z0,z1) ,div#(-(z0,z1),s(z1)) ,-#(z0,z1) ,LT#(z0,z1)) DIV#(s(z0),s(z1)) -> c_7(IF#(lt(z0,z1),0(),s(div(-(z0,z1),s(z1)))) ,lt#(z0,z1) ,div#(-(z0,z1),s(z1)) ,-#(z0,z1) ,DIV#(-(z0,z1),s(z1)) ,-#(z0,z1) ,-'#(z0,z1)) IF#(false(),z0,z1) -> c_8() IF#(true(),z0,z1) -> c_9() LT#(z0,0()) -> c_10() LT#(0(),s(z0)) -> c_11() LT#(s(z0),s(z1)) -> c_12(LT#(z0,z1)) Weak DPs -#(z0,0()) -> c_13() -#(0(),s(z0)) -> c_14() -#(s(z0),s(z1)) -> c_15(-#(z0,z1)) div#(z0,0()) -> c_16() div#(0(),z0) -> c_17() div#(s(z0),s(z1)) -> c_18(if#(lt(z0,z1),0(),s(div(-(z0,z1),s(z1)))) ,lt#(z0,z1) ,div#(-(z0,z1),s(z1)) ,-#(z0,z1)) if#(false(),z0,z1) -> c_19() if#(true(),z0,z1) -> c_20() lt#(z0,0()) -> c_21() lt#(0(),s(z0)) -> c_22() lt#(s(z0),s(z1)) -> c_23(lt#(z0,z1)) and mark the set of starting terms. ** Step 1.b:2: PredecessorEstimation. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: -'#(z0,0()) -> c_1() -'#(0(),s(z0)) -> c_2() -'#(s(z0),s(z1)) -> c_3(-'#(z0,z1)) DIV#(z0,0()) -> c_4() DIV#(0(),z0) -> c_5() DIV#(s(z0),s(z1)) -> c_6(IF#(lt(z0,z1),0(),s(div(-(z0,z1),s(z1)))) ,lt#(z0,z1) ,div#(-(z0,z1),s(z1)) ,-#(z0,z1) ,LT#(z0,z1)) DIV#(s(z0),s(z1)) -> c_7(IF#(lt(z0,z1),0(),s(div(-(z0,z1),s(z1)))) ,lt#(z0,z1) ,div#(-(z0,z1),s(z1)) ,-#(z0,z1) ,DIV#(-(z0,z1),s(z1)) ,-#(z0,z1) ,-'#(z0,z1)) IF#(false(),z0,z1) -> c_8() IF#(true(),z0,z1) -> c_9() LT#(z0,0()) -> c_10() LT#(0(),s(z0)) -> c_11() LT#(s(z0),s(z1)) -> c_12(LT#(z0,z1)) - Weak DPs: -#(z0,0()) -> c_13() -#(0(),s(z0)) -> c_14() -#(s(z0),s(z1)) -> c_15(-#(z0,z1)) div#(z0,0()) -> c_16() div#(0(),z0) -> c_17() div#(s(z0),s(z1)) -> c_18(if#(lt(z0,z1),0(),s(div(-(z0,z1),s(z1)))) ,lt#(z0,z1) ,div#(-(z0,z1),s(z1)) ,-#(z0,z1)) if#(false(),z0,z1) -> c_19() if#(true(),z0,z1) -> c_20() lt#(z0,0()) -> c_21() lt#(0(),s(z0)) -> c_22() lt#(s(z0),s(z1)) -> c_23(lt#(z0,z1)) - Weak TRS: -(z0,0()) -> z0 -(0(),s(z0)) -> 0() -(s(z0),s(z1)) -> -(z0,z1) -'(z0,0()) -> c() -'(0(),s(z0)) -> c1() -'(s(z0),s(z1)) -> c2(-'(z0,z1)) DIV(z0,0()) -> c8() DIV(0(),z0) -> c9() DIV(s(z0),s(z1)) -> c10(IF(lt(z0,z1),0(),s(div(-(z0,z1),s(z1)))),LT(z0,z1)) DIV(s(z0),s(z1)) -> c11(IF(lt(z0,z1),0(),s(div(-(z0,z1),s(z1)))),DIV(-(z0,z1),s(z1)),-'(z0,z1)) IF(false(),z0,z1) -> c7() IF(true(),z0,z1) -> c6() LT(z0,0()) -> c3() LT(0(),s(z0)) -> c4() LT(s(z0),s(z1)) -> c5(LT(z0,z1)) div(z0,0()) -> 0() div(0(),z0) -> 0() div(s(z0),s(z1)) -> if(lt(z0,z1),0(),s(div(-(z0,z1),s(z1)))) if(false(),z0,z1) -> z1 if(true(),z0,z1) -> z0 lt(z0,0()) -> false() lt(0(),s(z0)) -> true() lt(s(z0),s(z1)) -> lt(z0,z1) - Signature: {-/2,-'/2,DIV/2,IF/3,LT/2,div/2,if/3,lt/2,-#/2,-'#/2,DIV#/2,IF#/3,LT#/2,div#/2,if#/3,lt#/2} / {0/0,c/0,c1/0 ,c10/2,c11/3,c2/1,c3/0,c4/0,c5/1,c6/0,c7/0,c8/0,c9/0,false/0,s/1,true/0,c_1/0,c_2/0,c_3/1,c_4/0,c_5/0,c_6/5 ,c_7/7,c_8/0,c_9/0,c_10/0,c_11/0,c_12/1,c_13/0,c_14/0,c_15/1,c_16/0,c_17/0,c_18/4,c_19/0,c_20/0,c_21/0 ,c_22/0,c_23/1} - Obligation: innermost runtime complexity wrt. defined symbols {-#,-'#,DIV#,IF#,LT#,div#,if#,lt#} and constructors {0,c ,c1,c10,c11,c2,c3,c4,c5,c6,c7,c8,c9,false,s,true} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,2,4,5,8,9,10,11} by application of Pre({1,2,4,5,8,9,10,11}) = {3,6,7,12}. Here rules are labelled as follows: 1: -'#(z0,0()) -> c_1() 2: -'#(0(),s(z0)) -> c_2() 3: -'#(s(z0),s(z1)) -> c_3(-'#(z0,z1)) 4: DIV#(z0,0()) -> c_4() 5: DIV#(0(),z0) -> c_5() 6: DIV#(s(z0),s(z1)) -> c_6(IF#(lt(z0,z1),0(),s(div(-(z0,z1),s(z1)))) ,lt#(z0,z1) ,div#(-(z0,z1),s(z1)) ,-#(z0,z1) ,LT#(z0,z1)) 7: DIV#(s(z0),s(z1)) -> c_7(IF#(lt(z0,z1),0(),s(div(-(z0,z1),s(z1)))) ,lt#(z0,z1) ,div#(-(z0,z1),s(z1)) ,-#(z0,z1) ,DIV#(-(z0,z1),s(z1)) ,-#(z0,z1) ,-'#(z0,z1)) 8: IF#(false(),z0,z1) -> c_8() 9: IF#(true(),z0,z1) -> c_9() 10: LT#(z0,0()) -> c_10() 11: LT#(0(),s(z0)) -> c_11() 12: LT#(s(z0),s(z1)) -> c_12(LT#(z0,z1)) 13: -#(z0,0()) -> c_13() 14: -#(0(),s(z0)) -> c_14() 15: -#(s(z0),s(z1)) -> c_15(-#(z0,z1)) 16: div#(z0,0()) -> c_16() 17: div#(0(),z0) -> c_17() 18: div#(s(z0),s(z1)) -> c_18(if#(lt(z0,z1),0(),s(div(-(z0,z1),s(z1)))) ,lt#(z0,z1) ,div#(-(z0,z1),s(z1)) ,-#(z0,z1)) 19: if#(false(),z0,z1) -> c_19() 20: if#(true(),z0,z1) -> c_20() 21: lt#(z0,0()) -> c_21() 22: lt#(0(),s(z0)) -> c_22() 23: lt#(s(z0),s(z1)) -> c_23(lt#(z0,z1)) ** Step 1.b:3: RemoveWeakSuffixes. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: -'#(s(z0),s(z1)) -> c_3(-'#(z0,z1)) DIV#(s(z0),s(z1)) -> c_6(IF#(lt(z0,z1),0(),s(div(-(z0,z1),s(z1)))) ,lt#(z0,z1) ,div#(-(z0,z1),s(z1)) ,-#(z0,z1) ,LT#(z0,z1)) DIV#(s(z0),s(z1)) -> c_7(IF#(lt(z0,z1),0(),s(div(-(z0,z1),s(z1)))) ,lt#(z0,z1) ,div#(-(z0,z1),s(z1)) ,-#(z0,z1) ,DIV#(-(z0,z1),s(z1)) ,-#(z0,z1) ,-'#(z0,z1)) LT#(s(z0),s(z1)) -> c_12(LT#(z0,z1)) - Weak DPs: -#(z0,0()) -> c_13() -#(0(),s(z0)) -> c_14() -#(s(z0),s(z1)) -> c_15(-#(z0,z1)) -'#(z0,0()) -> c_1() -'#(0(),s(z0)) -> c_2() DIV#(z0,0()) -> c_4() DIV#(0(),z0) -> c_5() IF#(false(),z0,z1) -> c_8() IF#(true(),z0,z1) -> c_9() LT#(z0,0()) -> c_10() LT#(0(),s(z0)) -> c_11() div#(z0,0()) -> c_16() div#(0(),z0) -> c_17() div#(s(z0),s(z1)) -> c_18(if#(lt(z0,z1),0(),s(div(-(z0,z1),s(z1)))) ,lt#(z0,z1) ,div#(-(z0,z1),s(z1)) ,-#(z0,z1)) if#(false(),z0,z1) -> c_19() if#(true(),z0,z1) -> c_20() lt#(z0,0()) -> c_21() lt#(0(),s(z0)) -> c_22() lt#(s(z0),s(z1)) -> c_23(lt#(z0,z1)) - Weak TRS: -(z0,0()) -> z0 -(0(),s(z0)) -> 0() -(s(z0),s(z1)) -> -(z0,z1) -'(z0,0()) -> c() -'(0(),s(z0)) -> c1() -'(s(z0),s(z1)) -> c2(-'(z0,z1)) DIV(z0,0()) -> c8() DIV(0(),z0) -> c9() DIV(s(z0),s(z1)) -> c10(IF(lt(z0,z1),0(),s(div(-(z0,z1),s(z1)))),LT(z0,z1)) DIV(s(z0),s(z1)) -> c11(IF(lt(z0,z1),0(),s(div(-(z0,z1),s(z1)))),DIV(-(z0,z1),s(z1)),-'(z0,z1)) IF(false(),z0,z1) -> c7() IF(true(),z0,z1) -> c6() LT(z0,0()) -> c3() LT(0(),s(z0)) -> c4() LT(s(z0),s(z1)) -> c5(LT(z0,z1)) div(z0,0()) -> 0() div(0(),z0) -> 0() div(s(z0),s(z1)) -> if(lt(z0,z1),0(),s(div(-(z0,z1),s(z1)))) if(false(),z0,z1) -> z1 if(true(),z0,z1) -> z0 lt(z0,0()) -> false() lt(0(),s(z0)) -> true() lt(s(z0),s(z1)) -> lt(z0,z1) - Signature: {-/2,-'/2,DIV/2,IF/3,LT/2,div/2,if/3,lt/2,-#/2,-'#/2,DIV#/2,IF#/3,LT#/2,div#/2,if#/3,lt#/2} / {0/0,c/0,c1/0 ,c10/2,c11/3,c2/1,c3/0,c4/0,c5/1,c6/0,c7/0,c8/0,c9/0,false/0,s/1,true/0,c_1/0,c_2/0,c_3/1,c_4/0,c_5/0,c_6/5 ,c_7/7,c_8/0,c_9/0,c_10/0,c_11/0,c_12/1,c_13/0,c_14/0,c_15/1,c_16/0,c_17/0,c_18/4,c_19/0,c_20/0,c_21/0 ,c_22/0,c_23/1} - Obligation: innermost runtime complexity wrt. defined symbols {-#,-'#,DIV#,IF#,LT#,div#,if#,lt#} and constructors {0,c ,c1,c10,c11,c2,c3,c4,c5,c6,c7,c8,c9,false,s,true} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:-'#(s(z0),s(z1)) -> c_3(-'#(z0,z1)) -->_1 -'#(0(),s(z0)) -> c_2():9 -->_1 -'#(z0,0()) -> c_1():8 -->_1 -'#(s(z0),s(z1)) -> c_3(-'#(z0,z1)):1 2:S:DIV#(s(z0),s(z1)) -> c_6(IF#(lt(z0,z1),0(),s(div(-(z0,z1),s(z1)))) ,lt#(z0,z1) ,div#(-(z0,z1),s(z1)) ,-#(z0,z1) ,LT#(z0,z1)) -->_2 lt#(s(z0),s(z1)) -> c_23(lt#(z0,z1)):23 -->_3 div#(s(z0),s(z1)) -> c_18(if#(lt(z0,z1),0(),s(div(-(z0,z1),s(z1)))) ,lt#(z0,z1) ,div#(-(z0,z1),s(z1)) ,-#(z0,z1)):18 -->_4 -#(s(z0),s(z1)) -> c_15(-#(z0,z1)):7 -->_5 LT#(s(z0),s(z1)) -> c_12(LT#(z0,z1)):4 -->_2 lt#(0(),s(z0)) -> c_22():22 -->_2 lt#(z0,0()) -> c_21():21 -->_3 div#(0(),z0) -> c_17():17 -->_5 LT#(0(),s(z0)) -> c_11():15 -->_5 LT#(z0,0()) -> c_10():14 -->_1 IF#(true(),z0,z1) -> c_9():13 -->_1 IF#(false(),z0,z1) -> c_8():12 -->_4 -#(0(),s(z0)) -> c_14():6 -->_4 -#(z0,0()) -> c_13():5 3:S:DIV#(s(z0),s(z1)) -> c_7(IF#(lt(z0,z1),0(),s(div(-(z0,z1),s(z1)))) ,lt#(z0,z1) ,div#(-(z0,z1),s(z1)) ,-#(z0,z1) ,DIV#(-(z0,z1),s(z1)) ,-#(z0,z1) ,-'#(z0,z1)) -->_2 lt#(s(z0),s(z1)) -> c_23(lt#(z0,z1)):23 -->_3 div#(s(z0),s(z1)) -> c_18(if#(lt(z0,z1),0(),s(div(-(z0,z1),s(z1)))) ,lt#(z0,z1) ,div#(-(z0,z1),s(z1)) ,-#(z0,z1)):18 -->_6 -#(s(z0),s(z1)) -> c_15(-#(z0,z1)):7 -->_4 -#(s(z0),s(z1)) -> c_15(-#(z0,z1)):7 -->_2 lt#(0(),s(z0)) -> c_22():22 -->_2 lt#(z0,0()) -> c_21():21 -->_3 div#(0(),z0) -> c_17():17 -->_1 IF#(true(),z0,z1) -> c_9():13 -->_1 IF#(false(),z0,z1) -> c_8():12 -->_5 DIV#(0(),z0) -> c_5():11 -->_7 -'#(0(),s(z0)) -> c_2():9 -->_7 -'#(z0,0()) -> c_1():8 -->_6 -#(0(),s(z0)) -> c_14():6 -->_4 -#(0(),s(z0)) -> c_14():6 -->_6 -#(z0,0()) -> c_13():5 -->_4 -#(z0,0()) -> c_13():5 -->_5 DIV#(s(z0),s(z1)) -> c_7(IF#(lt(z0,z1),0(),s(div(-(z0,z1),s(z1)))) ,lt#(z0,z1) ,div#(-(z0,z1),s(z1)) ,-#(z0,z1) ,DIV#(-(z0,z1),s(z1)) ,-#(z0,z1) ,-'#(z0,z1)):3 -->_5 DIV#(s(z0),s(z1)) -> c_6(IF#(lt(z0,z1),0(),s(div(-(z0,z1),s(z1)))) ,lt#(z0,z1) ,div#(-(z0,z1),s(z1)) ,-#(z0,z1) ,LT#(z0,z1)):2 -->_7 -'#(s(z0),s(z1)) -> c_3(-'#(z0,z1)):1 4:S:LT#(s(z0),s(z1)) -> c_12(LT#(z0,z1)) -->_1 LT#(0(),s(z0)) -> c_11():15 -->_1 LT#(z0,0()) -> c_10():14 -->_1 LT#(s(z0),s(z1)) -> c_12(LT#(z0,z1)):4 5:W:-#(z0,0()) -> c_13() 6:W:-#(0(),s(z0)) -> c_14() 7:W:-#(s(z0),s(z1)) -> c_15(-#(z0,z1)) -->_1 -#(s(z0),s(z1)) -> c_15(-#(z0,z1)):7 -->_1 -#(0(),s(z0)) -> c_14():6 -->_1 -#(z0,0()) -> c_13():5 8:W:-'#(z0,0()) -> c_1() 9:W:-'#(0(),s(z0)) -> c_2() 10:W:DIV#(z0,0()) -> c_4() 11:W:DIV#(0(),z0) -> c_5() 12:W:IF#(false(),z0,z1) -> c_8() 13:W:IF#(true(),z0,z1) -> c_9() 14:W:LT#(z0,0()) -> c_10() 15:W:LT#(0(),s(z0)) -> c_11() 16:W:div#(z0,0()) -> c_16() 17:W:div#(0(),z0) -> c_17() 18:W:div#(s(z0),s(z1)) -> c_18(if#(lt(z0,z1),0(),s(div(-(z0,z1),s(z1)))) ,lt#(z0,z1) ,div#(-(z0,z1),s(z1)) ,-#(z0,z1)) -->_2 lt#(s(z0),s(z1)) -> c_23(lt#(z0,z1)):23 -->_2 lt#(0(),s(z0)) -> c_22():22 -->_2 lt#(z0,0()) -> c_21():21 -->_1 if#(true(),z0,z1) -> c_20():20 -->_1 if#(false(),z0,z1) -> c_19():19 -->_3 div#(s(z0),s(z1)) -> c_18(if#(lt(z0,z1),0(),s(div(-(z0,z1),s(z1)))) ,lt#(z0,z1) ,div#(-(z0,z1),s(z1)) ,-#(z0,z1)):18 -->_3 div#(0(),z0) -> c_17():17 -->_4 -#(s(z0),s(z1)) -> c_15(-#(z0,z1)):7 -->_4 -#(0(),s(z0)) -> c_14():6 -->_4 -#(z0,0()) -> c_13():5 19:W:if#(false(),z0,z1) -> c_19() 20:W:if#(true(),z0,z1) -> c_20() 21:W:lt#(z0,0()) -> c_21() 22:W:lt#(0(),s(z0)) -> c_22() 23:W:lt#(s(z0),s(z1)) -> c_23(lt#(z0,z1)) -->_1 lt#(s(z0),s(z1)) -> c_23(lt#(z0,z1)):23 -->_1 lt#(0(),s(z0)) -> c_22():22 -->_1 lt#(z0,0()) -> c_21():21 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 16: div#(z0,0()) -> c_16() 10: DIV#(z0,0()) -> c_4() 11: DIV#(0(),z0) -> c_5() 12: IF#(false(),z0,z1) -> c_8() 13: IF#(true(),z0,z1) -> c_9() 14: LT#(z0,0()) -> c_10() 15: LT#(0(),s(z0)) -> c_11() 18: div#(s(z0),s(z1)) -> c_18(if#(lt(z0,z1),0(),s(div(-(z0,z1),s(z1)))) ,lt#(z0,z1) ,div#(-(z0,z1),s(z1)) ,-#(z0,z1)) 7: -#(s(z0),s(z1)) -> c_15(-#(z0,z1)) 5: -#(z0,0()) -> c_13() 6: -#(0(),s(z0)) -> c_14() 17: div#(0(),z0) -> c_17() 19: if#(false(),z0,z1) -> c_19() 20: if#(true(),z0,z1) -> c_20() 23: lt#(s(z0),s(z1)) -> c_23(lt#(z0,z1)) 21: lt#(z0,0()) -> c_21() 22: lt#(0(),s(z0)) -> c_22() 8: -'#(z0,0()) -> c_1() 9: -'#(0(),s(z0)) -> c_2() ** Step 1.b:4: SimplifyRHS. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: -'#(s(z0),s(z1)) -> c_3(-'#(z0,z1)) DIV#(s(z0),s(z1)) -> c_6(IF#(lt(z0,z1),0(),s(div(-(z0,z1),s(z1)))) ,lt#(z0,z1) ,div#(-(z0,z1),s(z1)) ,-#(z0,z1) ,LT#(z0,z1)) DIV#(s(z0),s(z1)) -> c_7(IF#(lt(z0,z1),0(),s(div(-(z0,z1),s(z1)))) ,lt#(z0,z1) ,div#(-(z0,z1),s(z1)) ,-#(z0,z1) ,DIV#(-(z0,z1),s(z1)) ,-#(z0,z1) ,-'#(z0,z1)) LT#(s(z0),s(z1)) -> c_12(LT#(z0,z1)) - Weak TRS: -(z0,0()) -> z0 -(0(),s(z0)) -> 0() -(s(z0),s(z1)) -> -(z0,z1) -'(z0,0()) -> c() -'(0(),s(z0)) -> c1() -'(s(z0),s(z1)) -> c2(-'(z0,z1)) DIV(z0,0()) -> c8() DIV(0(),z0) -> c9() DIV(s(z0),s(z1)) -> c10(IF(lt(z0,z1),0(),s(div(-(z0,z1),s(z1)))),LT(z0,z1)) DIV(s(z0),s(z1)) -> c11(IF(lt(z0,z1),0(),s(div(-(z0,z1),s(z1)))),DIV(-(z0,z1),s(z1)),-'(z0,z1)) IF(false(),z0,z1) -> c7() IF(true(),z0,z1) -> c6() LT(z0,0()) -> c3() LT(0(),s(z0)) -> c4() LT(s(z0),s(z1)) -> c5(LT(z0,z1)) div(z0,0()) -> 0() div(0(),z0) -> 0() div(s(z0),s(z1)) -> if(lt(z0,z1),0(),s(div(-(z0,z1),s(z1)))) if(false(),z0,z1) -> z1 if(true(),z0,z1) -> z0 lt(z0,0()) -> false() lt(0(),s(z0)) -> true() lt(s(z0),s(z1)) -> lt(z0,z1) - Signature: {-/2,-'/2,DIV/2,IF/3,LT/2,div/2,if/3,lt/2,-#/2,-'#/2,DIV#/2,IF#/3,LT#/2,div#/2,if#/3,lt#/2} / {0/0,c/0,c1/0 ,c10/2,c11/3,c2/1,c3/0,c4/0,c5/1,c6/0,c7/0,c8/0,c9/0,false/0,s/1,true/0,c_1/0,c_2/0,c_3/1,c_4/0,c_5/0,c_6/5 ,c_7/7,c_8/0,c_9/0,c_10/0,c_11/0,c_12/1,c_13/0,c_14/0,c_15/1,c_16/0,c_17/0,c_18/4,c_19/0,c_20/0,c_21/0 ,c_22/0,c_23/1} - Obligation: innermost runtime complexity wrt. defined symbols {-#,-'#,DIV#,IF#,LT#,div#,if#,lt#} and constructors {0,c ,c1,c10,c11,c2,c3,c4,c5,c6,c7,c8,c9,false,s,true} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:-'#(s(z0),s(z1)) -> c_3(-'#(z0,z1)) -->_1 -'#(s(z0),s(z1)) -> c_3(-'#(z0,z1)):1 2:S:DIV#(s(z0),s(z1)) -> c_6(IF#(lt(z0,z1),0(),s(div(-(z0,z1),s(z1)))) ,lt#(z0,z1) ,div#(-(z0,z1),s(z1)) ,-#(z0,z1) ,LT#(z0,z1)) -->_5 LT#(s(z0),s(z1)) -> c_12(LT#(z0,z1)):4 3:S:DIV#(s(z0),s(z1)) -> c_7(IF#(lt(z0,z1),0(),s(div(-(z0,z1),s(z1)))) ,lt#(z0,z1) ,div#(-(z0,z1),s(z1)) ,-#(z0,z1) ,DIV#(-(z0,z1),s(z1)) ,-#(z0,z1) ,-'#(z0,z1)) -->_5 DIV#(s(z0),s(z1)) -> c_7(IF#(lt(z0,z1),0(),s(div(-(z0,z1),s(z1)))) ,lt#(z0,z1) ,div#(-(z0,z1),s(z1)) ,-#(z0,z1) ,DIV#(-(z0,z1),s(z1)) ,-#(z0,z1) ,-'#(z0,z1)):3 -->_5 DIV#(s(z0),s(z1)) -> c_6(IF#(lt(z0,z1),0(),s(div(-(z0,z1),s(z1)))) ,lt#(z0,z1) ,div#(-(z0,z1),s(z1)) ,-#(z0,z1) ,LT#(z0,z1)):2 -->_7 -'#(s(z0),s(z1)) -> c_3(-'#(z0,z1)):1 4:S:LT#(s(z0),s(z1)) -> c_12(LT#(z0,z1)) -->_1 LT#(s(z0),s(z1)) -> c_12(LT#(z0,z1)):4 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: DIV#(s(z0),s(z1)) -> c_6(LT#(z0,z1)) DIV#(s(z0),s(z1)) -> c_7(DIV#(-(z0,z1),s(z1)),-'#(z0,z1)) ** Step 1.b:5: UsableRules. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: -'#(s(z0),s(z1)) -> c_3(-'#(z0,z1)) DIV#(s(z0),s(z1)) -> c_6(LT#(z0,z1)) DIV#(s(z0),s(z1)) -> c_7(DIV#(-(z0,z1),s(z1)),-'#(z0,z1)) LT#(s(z0),s(z1)) -> c_12(LT#(z0,z1)) - Weak TRS: -(z0,0()) -> z0 -(0(),s(z0)) -> 0() -(s(z0),s(z1)) -> -(z0,z1) -'(z0,0()) -> c() -'(0(),s(z0)) -> c1() -'(s(z0),s(z1)) -> c2(-'(z0,z1)) DIV(z0,0()) -> c8() DIV(0(),z0) -> c9() DIV(s(z0),s(z1)) -> c10(IF(lt(z0,z1),0(),s(div(-(z0,z1),s(z1)))),LT(z0,z1)) DIV(s(z0),s(z1)) -> c11(IF(lt(z0,z1),0(),s(div(-(z0,z1),s(z1)))),DIV(-(z0,z1),s(z1)),-'(z0,z1)) IF(false(),z0,z1) -> c7() IF(true(),z0,z1) -> c6() LT(z0,0()) -> c3() LT(0(),s(z0)) -> c4() LT(s(z0),s(z1)) -> c5(LT(z0,z1)) div(z0,0()) -> 0() div(0(),z0) -> 0() div(s(z0),s(z1)) -> if(lt(z0,z1),0(),s(div(-(z0,z1),s(z1)))) if(false(),z0,z1) -> z1 if(true(),z0,z1) -> z0 lt(z0,0()) -> false() lt(0(),s(z0)) -> true() lt(s(z0),s(z1)) -> lt(z0,z1) - Signature: {-/2,-'/2,DIV/2,IF/3,LT/2,div/2,if/3,lt/2,-#/2,-'#/2,DIV#/2,IF#/3,LT#/2,div#/2,if#/3,lt#/2} / {0/0,c/0,c1/0 ,c10/2,c11/3,c2/1,c3/0,c4/0,c5/1,c6/0,c7/0,c8/0,c9/0,false/0,s/1,true/0,c_1/0,c_2/0,c_3/1,c_4/0,c_5/0,c_6/1 ,c_7/2,c_8/0,c_9/0,c_10/0,c_11/0,c_12/1,c_13/0,c_14/0,c_15/1,c_16/0,c_17/0,c_18/4,c_19/0,c_20/0,c_21/0 ,c_22/0,c_23/1} - Obligation: innermost runtime complexity wrt. defined symbols {-#,-'#,DIV#,IF#,LT#,div#,if#,lt#} and constructors {0,c ,c1,c10,c11,c2,c3,c4,c5,c6,c7,c8,c9,false,s,true} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: -(z0,0()) -> z0 -(0(),s(z0)) -> 0() -(s(z0),s(z1)) -> -(z0,z1) -'#(s(z0),s(z1)) -> c_3(-'#(z0,z1)) DIV#(s(z0),s(z1)) -> c_6(LT#(z0,z1)) DIV#(s(z0),s(z1)) -> c_7(DIV#(-(z0,z1),s(z1)),-'#(z0,z1)) LT#(s(z0),s(z1)) -> c_12(LT#(z0,z1)) ** Step 1.b:6: DecomposeDG. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: -'#(s(z0),s(z1)) -> c_3(-'#(z0,z1)) DIV#(s(z0),s(z1)) -> c_6(LT#(z0,z1)) DIV#(s(z0),s(z1)) -> c_7(DIV#(-(z0,z1),s(z1)),-'#(z0,z1)) LT#(s(z0),s(z1)) -> c_12(LT#(z0,z1)) - Weak TRS: -(z0,0()) -> z0 -(0(),s(z0)) -> 0() -(s(z0),s(z1)) -> -(z0,z1) - Signature: {-/2,-'/2,DIV/2,IF/3,LT/2,div/2,if/3,lt/2,-#/2,-'#/2,DIV#/2,IF#/3,LT#/2,div#/2,if#/3,lt#/2} / {0/0,c/0,c1/0 ,c10/2,c11/3,c2/1,c3/0,c4/0,c5/1,c6/0,c7/0,c8/0,c9/0,false/0,s/1,true/0,c_1/0,c_2/0,c_3/1,c_4/0,c_5/0,c_6/1 ,c_7/2,c_8/0,c_9/0,c_10/0,c_11/0,c_12/1,c_13/0,c_14/0,c_15/1,c_16/0,c_17/0,c_18/4,c_19/0,c_20/0,c_21/0 ,c_22/0,c_23/1} - Obligation: innermost runtime complexity wrt. defined symbols {-#,-'#,DIV#,IF#,LT#,div#,if#,lt#} and constructors {0,c ,c1,c10,c11,c2,c3,c4,c5,c6,c7,c8,c9,false,s,true} + Applied Processor: DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing} + Details: We decompose the input problem according to the dependency graph into the upper component DIV#(s(z0),s(z1)) -> c_7(DIV#(-(z0,z1),s(z1)),-'#(z0,z1)) and a lower component -'#(s(z0),s(z1)) -> c_3(-'#(z0,z1)) DIV#(s(z0),s(z1)) -> c_6(LT#(z0,z1)) LT#(s(z0),s(z1)) -> c_12(LT#(z0,z1)) Further, following extension rules are added to the lower component. DIV#(s(z0),s(z1)) -> -'#(z0,z1) DIV#(s(z0),s(z1)) -> DIV#(-(z0,z1),s(z1)) *** Step 1.b:6.a:1: SimplifyRHS. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: DIV#(s(z0),s(z1)) -> c_7(DIV#(-(z0,z1),s(z1)),-'#(z0,z1)) - Weak TRS: -(z0,0()) -> z0 -(0(),s(z0)) -> 0() -(s(z0),s(z1)) -> -(z0,z1) - Signature: {-/2,-'/2,DIV/2,IF/3,LT/2,div/2,if/3,lt/2,-#/2,-'#/2,DIV#/2,IF#/3,LT#/2,div#/2,if#/3,lt#/2} / {0/0,c/0,c1/0 ,c10/2,c11/3,c2/1,c3/0,c4/0,c5/1,c6/0,c7/0,c8/0,c9/0,false/0,s/1,true/0,c_1/0,c_2/0,c_3/1,c_4/0,c_5/0,c_6/1 ,c_7/2,c_8/0,c_9/0,c_10/0,c_11/0,c_12/1,c_13/0,c_14/0,c_15/1,c_16/0,c_17/0,c_18/4,c_19/0,c_20/0,c_21/0 ,c_22/0,c_23/1} - Obligation: innermost runtime complexity wrt. defined symbols {-#,-'#,DIV#,IF#,LT#,div#,if#,lt#} and constructors {0,c ,c1,c10,c11,c2,c3,c4,c5,c6,c7,c8,c9,false,s,true} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:DIV#(s(z0),s(z1)) -> c_7(DIV#(-(z0,z1),s(z1)),-'#(z0,z1)) -->_1 DIV#(s(z0),s(z1)) -> c_7(DIV#(-(z0,z1),s(z1)),-'#(z0,z1)):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: DIV#(s(z0),s(z1)) -> c_7(DIV#(-(z0,z1),s(z1))) *** Step 1.b:6.a:2: NaturalMI. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: DIV#(s(z0),s(z1)) -> c_7(DIV#(-(z0,z1),s(z1))) - Weak TRS: -(z0,0()) -> z0 -(0(),s(z0)) -> 0() -(s(z0),s(z1)) -> -(z0,z1) - Signature: {-/2,-'/2,DIV/2,IF/3,LT/2,div/2,if/3,lt/2,-#/2,-'#/2,DIV#/2,IF#/3,LT#/2,div#/2,if#/3,lt#/2} / {0/0,c/0,c1/0 ,c10/2,c11/3,c2/1,c3/0,c4/0,c5/1,c6/0,c7/0,c8/0,c9/0,false/0,s/1,true/0,c_1/0,c_2/0,c_3/1,c_4/0,c_5/0,c_6/1 ,c_7/1,c_8/0,c_9/0,c_10/0,c_11/0,c_12/1,c_13/0,c_14/0,c_15/1,c_16/0,c_17/0,c_18/4,c_19/0,c_20/0,c_21/0 ,c_22/0,c_23/1} - Obligation: innermost runtime complexity wrt. defined symbols {-#,-'#,DIV#,IF#,LT#,div#,if#,lt#} and constructors {0,c ,c1,c10,c11,c2,c3,c4,c5,c6,c7,c8,c9,false,s,true} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_7) = {1} Following symbols are considered usable: {-,-#,-'#,DIV#,IF#,LT#,div#,if#,lt#} TcT has computed the following interpretation: p(-) = [1] x1 + [0] p(-') = [0] p(0) = [1] p(DIV) = [1] x2 + [0] p(IF) = [0] p(LT) = [0] p(c) = [0] p(c1) = [0] p(c10) = [1] x1 + [1] x2 + [0] p(c11) = [1] x1 + [1] x2 + [0] p(c2) = [1] x1 + [0] p(c3) = [0] p(c4) = [0] p(c5) = [0] p(c6) = [0] p(c7) = [0] p(c8) = [0] p(c9) = [0] p(div) = [1] x2 + [0] p(false) = [0] p(if) = [1] x3 + [0] p(lt) = [1] x1 + [1] x2 + [0] p(s) = [1] x1 + [4] p(true) = [0] p(-#) = [0] p(-'#) = [1] x2 + [0] p(DIV#) = [4] x1 + [0] p(IF#) = [0] p(LT#) = [0] p(div#) = [0] p(if#) = [2] x3 + [0] p(lt#) = [2] x2 + [0] p(c_1) = [1] p(c_2) = [0] p(c_3) = [1] x1 + [1] p(c_4) = [0] p(c_5) = [1] p(c_6) = [1] p(c_7) = [1] x1 + [14] p(c_8) = [0] p(c_9) = [0] p(c_10) = [1] p(c_11) = [1] p(c_12) = [0] p(c_13) = [1] p(c_14) = [8] p(c_15) = [1] x1 + [1] p(c_16) = [2] p(c_17) = [1] p(c_18) = [1] x1 + [4] x2 + [2] x3 + [1] x4 + [0] p(c_19) = [1] p(c_20) = [2] p(c_21) = [0] p(c_22) = [1] p(c_23) = [8] x1 + [0] Following rules are strictly oriented: DIV#(s(z0),s(z1)) = [4] z0 + [16] > [4] z0 + [14] = c_7(DIV#(-(z0,z1),s(z1))) Following rules are (at-least) weakly oriented: -(z0,0()) = [1] z0 + [0] >= [1] z0 + [0] = z0 -(0(),s(z0)) = [1] >= [1] = 0() -(s(z0),s(z1)) = [1] z0 + [4] >= [1] z0 + [0] = -(z0,z1) *** Step 1.b:6.a:3: EmptyProcessor. WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: DIV#(s(z0),s(z1)) -> c_7(DIV#(-(z0,z1),s(z1))) - Weak TRS: -(z0,0()) -> z0 -(0(),s(z0)) -> 0() -(s(z0),s(z1)) -> -(z0,z1) - Signature: {-/2,-'/2,DIV/2,IF/3,LT/2,div/2,if/3,lt/2,-#/2,-'#/2,DIV#/2,IF#/3,LT#/2,div#/2,if#/3,lt#/2} / {0/0,c/0,c1/0 ,c10/2,c11/3,c2/1,c3/0,c4/0,c5/1,c6/0,c7/0,c8/0,c9/0,false/0,s/1,true/0,c_1/0,c_2/0,c_3/1,c_4/0,c_5/0,c_6/1 ,c_7/1,c_8/0,c_9/0,c_10/0,c_11/0,c_12/1,c_13/0,c_14/0,c_15/1,c_16/0,c_17/0,c_18/4,c_19/0,c_20/0,c_21/0 ,c_22/0,c_23/1} - Obligation: innermost runtime complexity wrt. defined symbols {-#,-'#,DIV#,IF#,LT#,div#,if#,lt#} and constructors {0,c ,c1,c10,c11,c2,c3,c4,c5,c6,c7,c8,c9,false,s,true} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). *** Step 1.b:6.b:1: NaturalMI. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: -'#(s(z0),s(z1)) -> c_3(-'#(z0,z1)) DIV#(s(z0),s(z1)) -> c_6(LT#(z0,z1)) LT#(s(z0),s(z1)) -> c_12(LT#(z0,z1)) - Weak DPs: DIV#(s(z0),s(z1)) -> -'#(z0,z1) DIV#(s(z0),s(z1)) -> DIV#(-(z0,z1),s(z1)) - Weak TRS: -(z0,0()) -> z0 -(0(),s(z0)) -> 0() -(s(z0),s(z1)) -> -(z0,z1) - Signature: {-/2,-'/2,DIV/2,IF/3,LT/2,div/2,if/3,lt/2,-#/2,-'#/2,DIV#/2,IF#/3,LT#/2,div#/2,if#/3,lt#/2} / {0/0,c/0,c1/0 ,c10/2,c11/3,c2/1,c3/0,c4/0,c5/1,c6/0,c7/0,c8/0,c9/0,false/0,s/1,true/0,c_1/0,c_2/0,c_3/1,c_4/0,c_5/0,c_6/1 ,c_7/2,c_8/0,c_9/0,c_10/0,c_11/0,c_12/1,c_13/0,c_14/0,c_15/1,c_16/0,c_17/0,c_18/4,c_19/0,c_20/0,c_21/0 ,c_22/0,c_23/1} - Obligation: innermost runtime complexity wrt. defined symbols {-#,-'#,DIV#,IF#,LT#,div#,if#,lt#} and constructors {0,c ,c1,c10,c11,c2,c3,c4,c5,c6,c7,c8,c9,false,s,true} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any 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_6) = {1}, uargs(c_12) = {1} Following symbols are considered usable: {-#,-'#,DIV#,IF#,LT#,div#,if#,lt#} TcT has computed the following interpretation: p(-) = [2] x2 + [0] p(-') = [0] p(0) = [0] p(DIV) = [0] p(IF) = [0] p(LT) = [0] p(c) = [0] p(c1) = [0] p(c10) = [0] p(c11) = [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(div) = [0] p(false) = [0] p(if) = [0] p(lt) = [0] p(s) = [15] p(true) = [0] p(-#) = [0] p(-'#) = [0] p(DIV#) = [9] p(IF#) = [0] p(LT#) = [1] p(div#) = [1] x2 + [0] p(if#) = [1] x1 + [1] x2 + [4] x3 + [0] p(lt#) = [2] x2 + [0] p(c_1) = [0] p(c_2) = [0] p(c_3) = [1] x1 + [0] p(c_4) = [0] p(c_5) = [1] p(c_6) = [4] x1 + [1] p(c_7) = [1] x1 + [1] x2 + [0] p(c_8) = [0] p(c_9) = [0] p(c_10) = [0] p(c_11) = [0] p(c_12) = [1] x1 + [0] p(c_13) = [0] p(c_14) = [0] p(c_15) = [1] x1 + [0] p(c_16) = [0] p(c_17) = [0] p(c_18) = [1] x1 + [0] p(c_19) = [0] p(c_20) = [0] p(c_21) = [0] p(c_22) = [0] p(c_23) = [0] Following rules are strictly oriented: DIV#(s(z0),s(z1)) = [9] > [5] = c_6(LT#(z0,z1)) Following rules are (at-least) weakly oriented: -'#(s(z0),s(z1)) = [0] >= [0] = c_3(-'#(z0,z1)) DIV#(s(z0),s(z1)) = [9] >= [0] = -'#(z0,z1) DIV#(s(z0),s(z1)) = [9] >= [9] = DIV#(-(z0,z1),s(z1)) LT#(s(z0),s(z1)) = [1] >= [1] = c_12(LT#(z0,z1)) *** Step 1.b:6.b:2: NaturalMI. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: -'#(s(z0),s(z1)) -> c_3(-'#(z0,z1)) LT#(s(z0),s(z1)) -> c_12(LT#(z0,z1)) - Weak DPs: DIV#(s(z0),s(z1)) -> -'#(z0,z1) DIV#(s(z0),s(z1)) -> DIV#(-(z0,z1),s(z1)) DIV#(s(z0),s(z1)) -> c_6(LT#(z0,z1)) - Weak TRS: -(z0,0()) -> z0 -(0(),s(z0)) -> 0() -(s(z0),s(z1)) -> -(z0,z1) - Signature: {-/2,-'/2,DIV/2,IF/3,LT/2,div/2,if/3,lt/2,-#/2,-'#/2,DIV#/2,IF#/3,LT#/2,div#/2,if#/3,lt#/2} / {0/0,c/0,c1/0 ,c10/2,c11/3,c2/1,c3/0,c4/0,c5/1,c6/0,c7/0,c8/0,c9/0,false/0,s/1,true/0,c_1/0,c_2/0,c_3/1,c_4/0,c_5/0,c_6/1 ,c_7/2,c_8/0,c_9/0,c_10/0,c_11/0,c_12/1,c_13/0,c_14/0,c_15/1,c_16/0,c_17/0,c_18/4,c_19/0,c_20/0,c_21/0 ,c_22/0,c_23/1} - Obligation: innermost runtime complexity wrt. defined symbols {-#,-'#,DIV#,IF#,LT#,div#,if#,lt#} and constructors {0,c ,c1,c10,c11,c2,c3,c4,c5,c6,c7,c8,c9,false,s,true} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any 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_6) = {1}, uargs(c_12) = {1} Following symbols are considered usable: {-#,-'#,DIV#,IF#,LT#,div#,if#,lt#} TcT has computed the following interpretation: p(-) = [1] x1 + [8] x2 + [1] p(-') = [0] p(0) = [0] p(DIV) = [0] p(IF) = [0] p(LT) = [0] p(c) = [0] p(c1) = [0] p(c10) = [1] x1 + [1] x2 + [0] p(c11) = [1] x1 + [0] p(c2) = [0] p(c3) = [0] p(c4) = [0] p(c5) = [1] x1 + [0] p(c6) = [0] p(c7) = [0] p(c8) = [0] p(c9) = [0] p(div) = [1] x1 + [0] p(false) = [0] p(if) = [2] x1 + [1] x2 + [1] x3 + [0] p(lt) = [4] x2 + [0] p(s) = [1] x1 + [3] p(true) = [0] p(-#) = [8] x1 + [1] x2 + [0] p(-'#) = [4] x2 + [6] p(DIV#) = [8] x2 + [3] p(IF#) = [2] x2 + [0] p(LT#) = [0] p(div#) = [2] x2 + [0] p(if#) = [1] x1 + [4] x2 + [1] x3 + [4] p(lt#) = [4] x2 + [1] p(c_1) = [1] p(c_2) = [1] p(c_3) = [1] x1 + [1] p(c_4) = [0] p(c_5) = [4] p(c_6) = [2] x1 + [13] p(c_7) = [1] x1 + [0] p(c_8) = [0] p(c_9) = [0] p(c_10) = [0] p(c_11) = [2] p(c_12) = [4] x1 + [0] p(c_13) = [0] p(c_14) = [0] p(c_15) = [0] p(c_16) = [1] p(c_17) = [4] p(c_18) = [1] x1 + [1] x3 + [1] x4 + [0] p(c_19) = [0] p(c_20) = [1] p(c_21) = [1] p(c_22) = [1] p(c_23) = [1] Following rules are strictly oriented: -'#(s(z0),s(z1)) = [4] z1 + [18] > [4] z1 + [7] = c_3(-'#(z0,z1)) Following rules are (at-least) weakly oriented: DIV#(s(z0),s(z1)) = [8] z1 + [27] >= [4] z1 + [6] = -'#(z0,z1) DIV#(s(z0),s(z1)) = [8] z1 + [27] >= [8] z1 + [27] = DIV#(-(z0,z1),s(z1)) DIV#(s(z0),s(z1)) = [8] z1 + [27] >= [13] = c_6(LT#(z0,z1)) LT#(s(z0),s(z1)) = [0] >= [0] = c_12(LT#(z0,z1)) *** Step 1.b:6.b:3: NaturalMI. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: LT#(s(z0),s(z1)) -> c_12(LT#(z0,z1)) - Weak DPs: -'#(s(z0),s(z1)) -> c_3(-'#(z0,z1)) DIV#(s(z0),s(z1)) -> -'#(z0,z1) DIV#(s(z0),s(z1)) -> DIV#(-(z0,z1),s(z1)) DIV#(s(z0),s(z1)) -> c_6(LT#(z0,z1)) - Weak TRS: -(z0,0()) -> z0 -(0(),s(z0)) -> 0() -(s(z0),s(z1)) -> -(z0,z1) - Signature: {-/2,-'/2,DIV/2,IF/3,LT/2,div/2,if/3,lt/2,-#/2,-'#/2,DIV#/2,IF#/3,LT#/2,div#/2,if#/3,lt#/2} / {0/0,c/0,c1/0 ,c10/2,c11/3,c2/1,c3/0,c4/0,c5/1,c6/0,c7/0,c8/0,c9/0,false/0,s/1,true/0,c_1/0,c_2/0,c_3/1,c_4/0,c_5/0,c_6/1 ,c_7/2,c_8/0,c_9/0,c_10/0,c_11/0,c_12/1,c_13/0,c_14/0,c_15/1,c_16/0,c_17/0,c_18/4,c_19/0,c_20/0,c_21/0 ,c_22/0,c_23/1} - Obligation: innermost runtime complexity wrt. defined symbols {-#,-'#,DIV#,IF#,LT#,div#,if#,lt#} and constructors {0,c ,c1,c10,c11,c2,c3,c4,c5,c6,c7,c8,c9,false,s,true} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any 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_6) = {1}, uargs(c_12) = {1} Following symbols are considered usable: {-#,-'#,DIV#,IF#,LT#,div#,if#,lt#} TcT has computed the following interpretation: p(-) = [0] p(-') = [0] p(0) = [0] p(DIV) = [0] p(IF) = [0] p(LT) = [0] p(c) = [2] p(c1) = [0] p(c10) = [1] x1 + [1] x2 + [0] p(c11) = [1] x1 + [1] x3 + [0] p(c2) = [1] x1 + [0] p(c3) = [0] p(c4) = [0] p(c5) = [1] x1 + [0] p(c6) = [0] p(c7) = [0] p(c8) = [0] p(c9) = [0] p(div) = [0] p(false) = [0] p(if) = [0] p(lt) = [1] x2 + [0] p(s) = [1] x1 + [4] p(true) = [0] p(-#) = [2] x1 + [1] x2 + [0] p(-'#) = [0] p(DIV#) = [4] x2 + [3] p(IF#) = [1] x1 + [2] x3 + [0] p(LT#) = [4] x2 + [2] p(div#) = [0] p(if#) = [4] x1 + [0] p(lt#) = [1] x2 + [0] p(c_1) = [0] p(c_2) = [1] p(c_3) = [8] x1 + [0] p(c_4) = [0] p(c_5) = [2] p(c_6) = [1] x1 + [4] p(c_7) = [1] x1 + [0] p(c_8) = [2] p(c_9) = [8] p(c_10) = [1] p(c_11) = [0] p(c_12) = [1] x1 + [6] p(c_13) = [0] p(c_14) = [0] p(c_15) = [0] p(c_16) = [0] p(c_17) = [8] p(c_18) = [1] x2 + [2] x3 + [1] p(c_19) = [0] p(c_20) = [0] p(c_21) = [0] p(c_22) = [0] p(c_23) = [2] Following rules are strictly oriented: LT#(s(z0),s(z1)) = [4] z1 + [18] > [4] z1 + [8] = c_12(LT#(z0,z1)) Following rules are (at-least) weakly oriented: -'#(s(z0),s(z1)) = [0] >= [0] = c_3(-'#(z0,z1)) DIV#(s(z0),s(z1)) = [4] z1 + [19] >= [0] = -'#(z0,z1) DIV#(s(z0),s(z1)) = [4] z1 + [19] >= [4] z1 + [19] = DIV#(-(z0,z1),s(z1)) DIV#(s(z0),s(z1)) = [4] z1 + [19] >= [4] z1 + [6] = c_6(LT#(z0,z1)) *** Step 1.b:6.b:4: EmptyProcessor. WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: -'#(s(z0),s(z1)) -> c_3(-'#(z0,z1)) DIV#(s(z0),s(z1)) -> -'#(z0,z1) DIV#(s(z0),s(z1)) -> DIV#(-(z0,z1),s(z1)) DIV#(s(z0),s(z1)) -> c_6(LT#(z0,z1)) LT#(s(z0),s(z1)) -> c_12(LT#(z0,z1)) - Weak TRS: -(z0,0()) -> z0 -(0(),s(z0)) -> 0() -(s(z0),s(z1)) -> -(z0,z1) - Signature: {-/2,-'/2,DIV/2,IF/3,LT/2,div/2,if/3,lt/2,-#/2,-'#/2,DIV#/2,IF#/3,LT#/2,div#/2,if#/3,lt#/2} / {0/0,c/0,c1/0 ,c10/2,c11/3,c2/1,c3/0,c4/0,c5/1,c6/0,c7/0,c8/0,c9/0,false/0,s/1,true/0,c_1/0,c_2/0,c_3/1,c_4/0,c_5/0,c_6/1 ,c_7/2,c_8/0,c_9/0,c_10/0,c_11/0,c_12/1,c_13/0,c_14/0,c_15/1,c_16/0,c_17/0,c_18/4,c_19/0,c_20/0,c_21/0 ,c_22/0,c_23/1} - Obligation: innermost runtime complexity wrt. defined symbols {-#,-'#,DIV#,IF#,LT#,div#,if#,lt#} and constructors {0,c ,c1,c10,c11,c2,c3,c4,c5,c6,c7,c8,c9,false,s,true} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(Omega(n^1),O(n^2))