MAYBE * Step 1: DependencyPairs MAYBE + Considered Problem: - Strict TRS: *(N,0()) -> 0() *(s(N),s(M)) -> s(+(N,+(M,*(N,M)))) +(N,0()) -> N +(s(N),s(M)) -> s(s(+(N,M))) d(0(),N) -> N d(s(N),s(M)) -> d(N,M) gcd(NzM,NzM) -> u_02(is_NzNat(NzM),NzM) gcd(NzN,NzM) -> u_31(is_NzNat(NzN),is_NzNat(NzM),NzN,NzM) gcd(0(),N) -> 0() gt(NzN,0()) -> u_4(is_NzNat(NzN)) gt(0(),M) -> False() gt(s(N),s(M)) -> gt(N,M) is_NzNat(0()) -> False() is_NzNat(s(N)) -> True() lt(N,M) -> gt(M,N) p(s(N)) -> N quot(N,NzM) -> u_11(is_NzNat(NzM),N,NzM) quot(N,NzM) -> u_21(is_NzNat(NzM),NzM,N) quot(NzM,NzM) -> u_01(is_NzNat(NzM)) u_01(True()) -> s(0()) u_02(True(),NzM) -> NzM u_1(True(),N,NzM) -> s(quot(d(N,NzM),NzM)) u_11(True(),N,NzM) -> u_1(gt(N,NzM),N,NzM) u_2(True()) -> 0() u_21(True(),NzM,N) -> u_2(gt(NzM,N)) u_3(True(),NzN,NzM) -> gcd(d(NzN,NzM),NzM) u_31(True(),True(),NzN,NzM) -> u_3(gt(NzN,NzM),NzN,NzM) u_4(True()) -> True() - Signature: {*/2,+/2,d/2,gcd/2,gt/2,is_NzNat/1,lt/2,p/1,quot/2,u_01/1,u_02/2,u_1/3,u_11/3,u_2/1,u_21/3,u_3/3,u_31/4 ,u_4/1} / {0/0,False/0,True/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {*,+,d,gcd,gt,is_NzNat,lt,p,quot,u_01,u_02,u_1,u_11,u_2 ,u_21,u_3,u_31,u_4} and constructors {0,False,True,s} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs *#(N,0()) -> c_1() *#(s(N),s(M)) -> c_2(+#(N,+(M,*(N,M))),+#(M,*(N,M)),*#(N,M)) +#(N,0()) -> c_3() +#(s(N),s(M)) -> c_4(+#(N,M)) d#(0(),N) -> c_5() d#(s(N),s(M)) -> c_6(d#(N,M)) gcd#(NzM,NzM) -> c_7(u_02#(is_NzNat(NzM),NzM),is_NzNat#(NzM)) gcd#(NzN,NzM) -> c_8(u_31#(is_NzNat(NzN),is_NzNat(NzM),NzN,NzM),is_NzNat#(NzN),is_NzNat#(NzM)) gcd#(0(),N) -> c_9() gt#(NzN,0()) -> c_10(u_4#(is_NzNat(NzN)),is_NzNat#(NzN)) gt#(0(),M) -> c_11() gt#(s(N),s(M)) -> c_12(gt#(N,M)) is_NzNat#(0()) -> c_13() is_NzNat#(s(N)) -> c_14() lt#(N,M) -> c_15(gt#(M,N)) p#(s(N)) -> c_16() quot#(N,NzM) -> c_17(u_11#(is_NzNat(NzM),N,NzM),is_NzNat#(NzM)) quot#(N,NzM) -> c_18(u_21#(is_NzNat(NzM),NzM,N),is_NzNat#(NzM)) quot#(NzM,NzM) -> c_19(u_01#(is_NzNat(NzM)),is_NzNat#(NzM)) u_01#(True()) -> c_20() u_02#(True(),NzM) -> c_21() u_1#(True(),N,NzM) -> c_22(quot#(d(N,NzM),NzM),d#(N,NzM)) u_11#(True(),N,NzM) -> c_23(u_1#(gt(N,NzM),N,NzM),gt#(N,NzM)) u_2#(True()) -> c_24() u_21#(True(),NzM,N) -> c_25(u_2#(gt(NzM,N)),gt#(NzM,N)) u_3#(True(),NzN,NzM) -> c_26(gcd#(d(NzN,NzM),NzM),d#(NzN,NzM)) u_31#(True(),True(),NzN,NzM) -> c_27(u_3#(gt(NzN,NzM),NzN,NzM),gt#(NzN,NzM)) u_4#(True()) -> c_28() Weak DPs and mark the set of starting terms. * Step 2: UsableRules MAYBE + Considered Problem: - Strict DPs: *#(N,0()) -> c_1() *#(s(N),s(M)) -> c_2(+#(N,+(M,*(N,M))),+#(M,*(N,M)),*#(N,M)) +#(N,0()) -> c_3() +#(s(N),s(M)) -> c_4(+#(N,M)) d#(0(),N) -> c_5() d#(s(N),s(M)) -> c_6(d#(N,M)) gcd#(NzM,NzM) -> c_7(u_02#(is_NzNat(NzM),NzM),is_NzNat#(NzM)) gcd#(NzN,NzM) -> c_8(u_31#(is_NzNat(NzN),is_NzNat(NzM),NzN,NzM),is_NzNat#(NzN),is_NzNat#(NzM)) gcd#(0(),N) -> c_9() gt#(NzN,0()) -> c_10(u_4#(is_NzNat(NzN)),is_NzNat#(NzN)) gt#(0(),M) -> c_11() gt#(s(N),s(M)) -> c_12(gt#(N,M)) is_NzNat#(0()) -> c_13() is_NzNat#(s(N)) -> c_14() lt#(N,M) -> c_15(gt#(M,N)) p#(s(N)) -> c_16() quot#(N,NzM) -> c_17(u_11#(is_NzNat(NzM),N,NzM),is_NzNat#(NzM)) quot#(N,NzM) -> c_18(u_21#(is_NzNat(NzM),NzM,N),is_NzNat#(NzM)) quot#(NzM,NzM) -> c_19(u_01#(is_NzNat(NzM)),is_NzNat#(NzM)) u_01#(True()) -> c_20() u_02#(True(),NzM) -> c_21() u_1#(True(),N,NzM) -> c_22(quot#(d(N,NzM),NzM),d#(N,NzM)) u_11#(True(),N,NzM) -> c_23(u_1#(gt(N,NzM),N,NzM),gt#(N,NzM)) u_2#(True()) -> c_24() u_21#(True(),NzM,N) -> c_25(u_2#(gt(NzM,N)),gt#(NzM,N)) u_3#(True(),NzN,NzM) -> c_26(gcd#(d(NzN,NzM),NzM),d#(NzN,NzM)) u_31#(True(),True(),NzN,NzM) -> c_27(u_3#(gt(NzN,NzM),NzN,NzM),gt#(NzN,NzM)) u_4#(True()) -> c_28() - Weak TRS: *(N,0()) -> 0() *(s(N),s(M)) -> s(+(N,+(M,*(N,M)))) +(N,0()) -> N +(s(N),s(M)) -> s(s(+(N,M))) d(0(),N) -> N d(s(N),s(M)) -> d(N,M) gcd(NzM,NzM) -> u_02(is_NzNat(NzM),NzM) gcd(NzN,NzM) -> u_31(is_NzNat(NzN),is_NzNat(NzM),NzN,NzM) gcd(0(),N) -> 0() gt(NzN,0()) -> u_4(is_NzNat(NzN)) gt(0(),M) -> False() gt(s(N),s(M)) -> gt(N,M) is_NzNat(0()) -> False() is_NzNat(s(N)) -> True() lt(N,M) -> gt(M,N) p(s(N)) -> N quot(N,NzM) -> u_11(is_NzNat(NzM),N,NzM) quot(N,NzM) -> u_21(is_NzNat(NzM),NzM,N) quot(NzM,NzM) -> u_01(is_NzNat(NzM)) u_01(True()) -> s(0()) u_02(True(),NzM) -> NzM u_1(True(),N,NzM) -> s(quot(d(N,NzM),NzM)) u_11(True(),N,NzM) -> u_1(gt(N,NzM),N,NzM) u_2(True()) -> 0() u_21(True(),NzM,N) -> u_2(gt(NzM,N)) u_3(True(),NzN,NzM) -> gcd(d(NzN,NzM),NzM) u_31(True(),True(),NzN,NzM) -> u_3(gt(NzN,NzM),NzN,NzM) u_4(True()) -> True() - Signature: {*/2,+/2,d/2,gcd/2,gt/2,is_NzNat/1,lt/2,p/1,quot/2,u_01/1,u_02/2,u_1/3,u_11/3,u_2/1,u_21/3,u_3/3,u_31/4 ,u_4/1,*#/2,+#/2,d#/2,gcd#/2,gt#/2,is_NzNat#/1,lt#/2,p#/1,quot#/2,u_01#/1,u_02#/2,u_1#/3,u_11#/3,u_2#/1 ,u_21#/3,u_3#/3,u_31#/4,u_4#/1} / {0/0,False/0,True/0,s/1,c_1/0,c_2/3,c_3/0,c_4/1,c_5/0,c_6/1,c_7/2,c_8/3 ,c_9/0,c_10/2,c_11/0,c_12/1,c_13/0,c_14/0,c_15/1,c_16/0,c_17/2,c_18/2,c_19/2,c_20/0,c_21/0,c_22/2,c_23/2 ,c_24/0,c_25/2,c_26/2,c_27/2,c_28/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,d#,gcd#,gt#,is_NzNat#,lt#,p#,quot#,u_01#,u_02#,u_1# ,u_11#,u_2#,u_21#,u_3#,u_31#,u_4#} and constructors {0,False,True,s} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: *(N,0()) -> 0() *(s(N),s(M)) -> s(+(N,+(M,*(N,M)))) +(N,0()) -> N +(s(N),s(M)) -> s(s(+(N,M))) d(0(),N) -> N d(s(N),s(M)) -> d(N,M) gt(NzN,0()) -> u_4(is_NzNat(NzN)) gt(0(),M) -> False() gt(s(N),s(M)) -> gt(N,M) is_NzNat(0()) -> False() is_NzNat(s(N)) -> True() u_4(True()) -> True() *#(N,0()) -> c_1() *#(s(N),s(M)) -> c_2(+#(N,+(M,*(N,M))),+#(M,*(N,M)),*#(N,M)) +#(N,0()) -> c_3() +#(s(N),s(M)) -> c_4(+#(N,M)) d#(0(),N) -> c_5() d#(s(N),s(M)) -> c_6(d#(N,M)) gcd#(NzM,NzM) -> c_7(u_02#(is_NzNat(NzM),NzM),is_NzNat#(NzM)) gcd#(NzN,NzM) -> c_8(u_31#(is_NzNat(NzN),is_NzNat(NzM),NzN,NzM),is_NzNat#(NzN),is_NzNat#(NzM)) gcd#(0(),N) -> c_9() gt#(NzN,0()) -> c_10(u_4#(is_NzNat(NzN)),is_NzNat#(NzN)) gt#(0(),M) -> c_11() gt#(s(N),s(M)) -> c_12(gt#(N,M)) is_NzNat#(0()) -> c_13() is_NzNat#(s(N)) -> c_14() lt#(N,M) -> c_15(gt#(M,N)) p#(s(N)) -> c_16() quot#(N,NzM) -> c_17(u_11#(is_NzNat(NzM),N,NzM),is_NzNat#(NzM)) quot#(N,NzM) -> c_18(u_21#(is_NzNat(NzM),NzM,N),is_NzNat#(NzM)) quot#(NzM,NzM) -> c_19(u_01#(is_NzNat(NzM)),is_NzNat#(NzM)) u_01#(True()) -> c_20() u_02#(True(),NzM) -> c_21() u_1#(True(),N,NzM) -> c_22(quot#(d(N,NzM),NzM),d#(N,NzM)) u_11#(True(),N,NzM) -> c_23(u_1#(gt(N,NzM),N,NzM),gt#(N,NzM)) u_2#(True()) -> c_24() u_21#(True(),NzM,N) -> c_25(u_2#(gt(NzM,N)),gt#(NzM,N)) u_3#(True(),NzN,NzM) -> c_26(gcd#(d(NzN,NzM),NzM),d#(NzN,NzM)) u_31#(True(),True(),NzN,NzM) -> c_27(u_3#(gt(NzN,NzM),NzN,NzM),gt#(NzN,NzM)) u_4#(True()) -> c_28() * Step 3: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: *#(N,0()) -> c_1() *#(s(N),s(M)) -> c_2(+#(N,+(M,*(N,M))),+#(M,*(N,M)),*#(N,M)) +#(N,0()) -> c_3() +#(s(N),s(M)) -> c_4(+#(N,M)) d#(0(),N) -> c_5() d#(s(N),s(M)) -> c_6(d#(N,M)) gcd#(NzM,NzM) -> c_7(u_02#(is_NzNat(NzM),NzM),is_NzNat#(NzM)) gcd#(NzN,NzM) -> c_8(u_31#(is_NzNat(NzN),is_NzNat(NzM),NzN,NzM),is_NzNat#(NzN),is_NzNat#(NzM)) gcd#(0(),N) -> c_9() gt#(NzN,0()) -> c_10(u_4#(is_NzNat(NzN)),is_NzNat#(NzN)) gt#(0(),M) -> c_11() gt#(s(N),s(M)) -> c_12(gt#(N,M)) is_NzNat#(0()) -> c_13() is_NzNat#(s(N)) -> c_14() lt#(N,M) -> c_15(gt#(M,N)) p#(s(N)) -> c_16() quot#(N,NzM) -> c_17(u_11#(is_NzNat(NzM),N,NzM),is_NzNat#(NzM)) quot#(N,NzM) -> c_18(u_21#(is_NzNat(NzM),NzM,N),is_NzNat#(NzM)) quot#(NzM,NzM) -> c_19(u_01#(is_NzNat(NzM)),is_NzNat#(NzM)) u_01#(True()) -> c_20() u_02#(True(),NzM) -> c_21() u_1#(True(),N,NzM) -> c_22(quot#(d(N,NzM),NzM),d#(N,NzM)) u_11#(True(),N,NzM) -> c_23(u_1#(gt(N,NzM),N,NzM),gt#(N,NzM)) u_2#(True()) -> c_24() u_21#(True(),NzM,N) -> c_25(u_2#(gt(NzM,N)),gt#(NzM,N)) u_3#(True(),NzN,NzM) -> c_26(gcd#(d(NzN,NzM),NzM),d#(NzN,NzM)) u_31#(True(),True(),NzN,NzM) -> c_27(u_3#(gt(NzN,NzM),NzN,NzM),gt#(NzN,NzM)) u_4#(True()) -> c_28() - Weak TRS: *(N,0()) -> 0() *(s(N),s(M)) -> s(+(N,+(M,*(N,M)))) +(N,0()) -> N +(s(N),s(M)) -> s(s(+(N,M))) d(0(),N) -> N d(s(N),s(M)) -> d(N,M) gt(NzN,0()) -> u_4(is_NzNat(NzN)) gt(0(),M) -> False() gt(s(N),s(M)) -> gt(N,M) is_NzNat(0()) -> False() is_NzNat(s(N)) -> True() u_4(True()) -> True() - Signature: {*/2,+/2,d/2,gcd/2,gt/2,is_NzNat/1,lt/2,p/1,quot/2,u_01/1,u_02/2,u_1/3,u_11/3,u_2/1,u_21/3,u_3/3,u_31/4 ,u_4/1,*#/2,+#/2,d#/2,gcd#/2,gt#/2,is_NzNat#/1,lt#/2,p#/1,quot#/2,u_01#/1,u_02#/2,u_1#/3,u_11#/3,u_2#/1 ,u_21#/3,u_3#/3,u_31#/4,u_4#/1} / {0/0,False/0,True/0,s/1,c_1/0,c_2/3,c_3/0,c_4/1,c_5/0,c_6/1,c_7/2,c_8/3 ,c_9/0,c_10/2,c_11/0,c_12/1,c_13/0,c_14/0,c_15/1,c_16/0,c_17/2,c_18/2,c_19/2,c_20/0,c_21/0,c_22/2,c_23/2 ,c_24/0,c_25/2,c_26/2,c_27/2,c_28/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,d#,gcd#,gt#,is_NzNat#,lt#,p#,quot#,u_01#,u_02#,u_1# ,u_11#,u_2#,u_21#,u_3#,u_31#,u_4#} and constructors {0,False,True,s} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,3,5,9,11,13,14,16,20,21,24,28} by application of Pre({1,3,5,9,11,13,14,16,20,21,24,28}) = {2,4,6,7,8,10,12,15,17,18,19,22,23,25,26,27}. Here rules are labelled as follows: 1: *#(N,0()) -> c_1() 2: *#(s(N),s(M)) -> c_2(+#(N,+(M,*(N,M))),+#(M,*(N,M)),*#(N,M)) 3: +#(N,0()) -> c_3() 4: +#(s(N),s(M)) -> c_4(+#(N,M)) 5: d#(0(),N) -> c_5() 6: d#(s(N),s(M)) -> c_6(d#(N,M)) 7: gcd#(NzM,NzM) -> c_7(u_02#(is_NzNat(NzM),NzM),is_NzNat#(NzM)) 8: gcd#(NzN,NzM) -> c_8(u_31#(is_NzNat(NzN),is_NzNat(NzM),NzN,NzM),is_NzNat#(NzN),is_NzNat#(NzM)) 9: gcd#(0(),N) -> c_9() 10: gt#(NzN,0()) -> c_10(u_4#(is_NzNat(NzN)),is_NzNat#(NzN)) 11: gt#(0(),M) -> c_11() 12: gt#(s(N),s(M)) -> c_12(gt#(N,M)) 13: is_NzNat#(0()) -> c_13() 14: is_NzNat#(s(N)) -> c_14() 15: lt#(N,M) -> c_15(gt#(M,N)) 16: p#(s(N)) -> c_16() 17: quot#(N,NzM) -> c_17(u_11#(is_NzNat(NzM),N,NzM),is_NzNat#(NzM)) 18: quot#(N,NzM) -> c_18(u_21#(is_NzNat(NzM),NzM,N),is_NzNat#(NzM)) 19: quot#(NzM,NzM) -> c_19(u_01#(is_NzNat(NzM)),is_NzNat#(NzM)) 20: u_01#(True()) -> c_20() 21: u_02#(True(),NzM) -> c_21() 22: u_1#(True(),N,NzM) -> c_22(quot#(d(N,NzM),NzM),d#(N,NzM)) 23: u_11#(True(),N,NzM) -> c_23(u_1#(gt(N,NzM),N,NzM),gt#(N,NzM)) 24: u_2#(True()) -> c_24() 25: u_21#(True(),NzM,N) -> c_25(u_2#(gt(NzM,N)),gt#(NzM,N)) 26: u_3#(True(),NzN,NzM) -> c_26(gcd#(d(NzN,NzM),NzM),d#(NzN,NzM)) 27: u_31#(True(),True(),NzN,NzM) -> c_27(u_3#(gt(NzN,NzM),NzN,NzM),gt#(NzN,NzM)) 28: u_4#(True()) -> c_28() * Step 4: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: *#(s(N),s(M)) -> c_2(+#(N,+(M,*(N,M))),+#(M,*(N,M)),*#(N,M)) +#(s(N),s(M)) -> c_4(+#(N,M)) d#(s(N),s(M)) -> c_6(d#(N,M)) gcd#(NzM,NzM) -> c_7(u_02#(is_NzNat(NzM),NzM),is_NzNat#(NzM)) gcd#(NzN,NzM) -> c_8(u_31#(is_NzNat(NzN),is_NzNat(NzM),NzN,NzM),is_NzNat#(NzN),is_NzNat#(NzM)) gt#(NzN,0()) -> c_10(u_4#(is_NzNat(NzN)),is_NzNat#(NzN)) gt#(s(N),s(M)) -> c_12(gt#(N,M)) lt#(N,M) -> c_15(gt#(M,N)) quot#(N,NzM) -> c_17(u_11#(is_NzNat(NzM),N,NzM),is_NzNat#(NzM)) quot#(N,NzM) -> c_18(u_21#(is_NzNat(NzM),NzM,N),is_NzNat#(NzM)) quot#(NzM,NzM) -> c_19(u_01#(is_NzNat(NzM)),is_NzNat#(NzM)) u_1#(True(),N,NzM) -> c_22(quot#(d(N,NzM),NzM),d#(N,NzM)) u_11#(True(),N,NzM) -> c_23(u_1#(gt(N,NzM),N,NzM),gt#(N,NzM)) u_21#(True(),NzM,N) -> c_25(u_2#(gt(NzM,N)),gt#(NzM,N)) u_3#(True(),NzN,NzM) -> c_26(gcd#(d(NzN,NzM),NzM),d#(NzN,NzM)) u_31#(True(),True(),NzN,NzM) -> c_27(u_3#(gt(NzN,NzM),NzN,NzM),gt#(NzN,NzM)) - Weak DPs: *#(N,0()) -> c_1() +#(N,0()) -> c_3() d#(0(),N) -> c_5() gcd#(0(),N) -> c_9() gt#(0(),M) -> c_11() is_NzNat#(0()) -> c_13() is_NzNat#(s(N)) -> c_14() p#(s(N)) -> c_16() u_01#(True()) -> c_20() u_02#(True(),NzM) -> c_21() u_2#(True()) -> c_24() u_4#(True()) -> c_28() - Weak TRS: *(N,0()) -> 0() *(s(N),s(M)) -> s(+(N,+(M,*(N,M)))) +(N,0()) -> N +(s(N),s(M)) -> s(s(+(N,M))) d(0(),N) -> N d(s(N),s(M)) -> d(N,M) gt(NzN,0()) -> u_4(is_NzNat(NzN)) gt(0(),M) -> False() gt(s(N),s(M)) -> gt(N,M) is_NzNat(0()) -> False() is_NzNat(s(N)) -> True() u_4(True()) -> True() - Signature: {*/2,+/2,d/2,gcd/2,gt/2,is_NzNat/1,lt/2,p/1,quot/2,u_01/1,u_02/2,u_1/3,u_11/3,u_2/1,u_21/3,u_3/3,u_31/4 ,u_4/1,*#/2,+#/2,d#/2,gcd#/2,gt#/2,is_NzNat#/1,lt#/2,p#/1,quot#/2,u_01#/1,u_02#/2,u_1#/3,u_11#/3,u_2#/1 ,u_21#/3,u_3#/3,u_31#/4,u_4#/1} / {0/0,False/0,True/0,s/1,c_1/0,c_2/3,c_3/0,c_4/1,c_5/0,c_6/1,c_7/2,c_8/3 ,c_9/0,c_10/2,c_11/0,c_12/1,c_13/0,c_14/0,c_15/1,c_16/0,c_17/2,c_18/2,c_19/2,c_20/0,c_21/0,c_22/2,c_23/2 ,c_24/0,c_25/2,c_26/2,c_27/2,c_28/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,d#,gcd#,gt#,is_NzNat#,lt#,p#,quot#,u_01#,u_02#,u_1# ,u_11#,u_2#,u_21#,u_3#,u_31#,u_4#} and constructors {0,False,True,s} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {4,6,11} by application of Pre({4,6,11}) = {7,8,12,13,14,15,16}. Here rules are labelled as follows: 1: *#(s(N),s(M)) -> c_2(+#(N,+(M,*(N,M))),+#(M,*(N,M)),*#(N,M)) 2: +#(s(N),s(M)) -> c_4(+#(N,M)) 3: d#(s(N),s(M)) -> c_6(d#(N,M)) 4: gcd#(NzM,NzM) -> c_7(u_02#(is_NzNat(NzM),NzM),is_NzNat#(NzM)) 5: gcd#(NzN,NzM) -> c_8(u_31#(is_NzNat(NzN),is_NzNat(NzM),NzN,NzM),is_NzNat#(NzN),is_NzNat#(NzM)) 6: gt#(NzN,0()) -> c_10(u_4#(is_NzNat(NzN)),is_NzNat#(NzN)) 7: gt#(s(N),s(M)) -> c_12(gt#(N,M)) 8: lt#(N,M) -> c_15(gt#(M,N)) 9: quot#(N,NzM) -> c_17(u_11#(is_NzNat(NzM),N,NzM),is_NzNat#(NzM)) 10: quot#(N,NzM) -> c_18(u_21#(is_NzNat(NzM),NzM,N),is_NzNat#(NzM)) 11: quot#(NzM,NzM) -> c_19(u_01#(is_NzNat(NzM)),is_NzNat#(NzM)) 12: u_1#(True(),N,NzM) -> c_22(quot#(d(N,NzM),NzM),d#(N,NzM)) 13: u_11#(True(),N,NzM) -> c_23(u_1#(gt(N,NzM),N,NzM),gt#(N,NzM)) 14: u_21#(True(),NzM,N) -> c_25(u_2#(gt(NzM,N)),gt#(NzM,N)) 15: u_3#(True(),NzN,NzM) -> c_26(gcd#(d(NzN,NzM),NzM),d#(NzN,NzM)) 16: u_31#(True(),True(),NzN,NzM) -> c_27(u_3#(gt(NzN,NzM),NzN,NzM),gt#(NzN,NzM)) 17: *#(N,0()) -> c_1() 18: +#(N,0()) -> c_3() 19: d#(0(),N) -> c_5() 20: gcd#(0(),N) -> c_9() 21: gt#(0(),M) -> c_11() 22: is_NzNat#(0()) -> c_13() 23: is_NzNat#(s(N)) -> c_14() 24: p#(s(N)) -> c_16() 25: u_01#(True()) -> c_20() 26: u_02#(True(),NzM) -> c_21() 27: u_2#(True()) -> c_24() 28: u_4#(True()) -> c_28() * Step 5: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: *#(s(N),s(M)) -> c_2(+#(N,+(M,*(N,M))),+#(M,*(N,M)),*#(N,M)) +#(s(N),s(M)) -> c_4(+#(N,M)) d#(s(N),s(M)) -> c_6(d#(N,M)) gcd#(NzN,NzM) -> c_8(u_31#(is_NzNat(NzN),is_NzNat(NzM),NzN,NzM),is_NzNat#(NzN),is_NzNat#(NzM)) gt#(s(N),s(M)) -> c_12(gt#(N,M)) lt#(N,M) -> c_15(gt#(M,N)) quot#(N,NzM) -> c_17(u_11#(is_NzNat(NzM),N,NzM),is_NzNat#(NzM)) quot#(N,NzM) -> c_18(u_21#(is_NzNat(NzM),NzM,N),is_NzNat#(NzM)) u_1#(True(),N,NzM) -> c_22(quot#(d(N,NzM),NzM),d#(N,NzM)) u_11#(True(),N,NzM) -> c_23(u_1#(gt(N,NzM),N,NzM),gt#(N,NzM)) u_21#(True(),NzM,N) -> c_25(u_2#(gt(NzM,N)),gt#(NzM,N)) u_3#(True(),NzN,NzM) -> c_26(gcd#(d(NzN,NzM),NzM),d#(NzN,NzM)) u_31#(True(),True(),NzN,NzM) -> c_27(u_3#(gt(NzN,NzM),NzN,NzM),gt#(NzN,NzM)) - Weak DPs: *#(N,0()) -> c_1() +#(N,0()) -> c_3() d#(0(),N) -> c_5() gcd#(NzM,NzM) -> c_7(u_02#(is_NzNat(NzM),NzM),is_NzNat#(NzM)) gcd#(0(),N) -> c_9() gt#(NzN,0()) -> c_10(u_4#(is_NzNat(NzN)),is_NzNat#(NzN)) gt#(0(),M) -> c_11() is_NzNat#(0()) -> c_13() is_NzNat#(s(N)) -> c_14() p#(s(N)) -> c_16() quot#(NzM,NzM) -> c_19(u_01#(is_NzNat(NzM)),is_NzNat#(NzM)) u_01#(True()) -> c_20() u_02#(True(),NzM) -> c_21() u_2#(True()) -> c_24() u_4#(True()) -> c_28() - Weak TRS: *(N,0()) -> 0() *(s(N),s(M)) -> s(+(N,+(M,*(N,M)))) +(N,0()) -> N +(s(N),s(M)) -> s(s(+(N,M))) d(0(),N) -> N d(s(N),s(M)) -> d(N,M) gt(NzN,0()) -> u_4(is_NzNat(NzN)) gt(0(),M) -> False() gt(s(N),s(M)) -> gt(N,M) is_NzNat(0()) -> False() is_NzNat(s(N)) -> True() u_4(True()) -> True() - Signature: {*/2,+/2,d/2,gcd/2,gt/2,is_NzNat/1,lt/2,p/1,quot/2,u_01/1,u_02/2,u_1/3,u_11/3,u_2/1,u_21/3,u_3/3,u_31/4 ,u_4/1,*#/2,+#/2,d#/2,gcd#/2,gt#/2,is_NzNat#/1,lt#/2,p#/1,quot#/2,u_01#/1,u_02#/2,u_1#/3,u_11#/3,u_2#/1 ,u_21#/3,u_3#/3,u_31#/4,u_4#/1} / {0/0,False/0,True/0,s/1,c_1/0,c_2/3,c_3/0,c_4/1,c_5/0,c_6/1,c_7/2,c_8/3 ,c_9/0,c_10/2,c_11/0,c_12/1,c_13/0,c_14/0,c_15/1,c_16/0,c_17/2,c_18/2,c_19/2,c_20/0,c_21/0,c_22/2,c_23/2 ,c_24/0,c_25/2,c_26/2,c_27/2,c_28/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,d#,gcd#,gt#,is_NzNat#,lt#,p#,quot#,u_01#,u_02#,u_1# ,u_11#,u_2#,u_21#,u_3#,u_31#,u_4#} and constructors {0,False,True,s} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:*#(s(N),s(M)) -> c_2(+#(N,+(M,*(N,M))),+#(M,*(N,M)),*#(N,M)) -->_2 +#(s(N),s(M)) -> c_4(+#(N,M)):2 -->_1 +#(s(N),s(M)) -> c_4(+#(N,M)):2 -->_2 +#(N,0()) -> c_3():15 -->_1 +#(N,0()) -> c_3():15 -->_3 *#(N,0()) -> c_1():14 -->_3 *#(s(N),s(M)) -> c_2(+#(N,+(M,*(N,M))),+#(M,*(N,M)),*#(N,M)):1 2:S:+#(s(N),s(M)) -> c_4(+#(N,M)) -->_1 +#(N,0()) -> c_3():15 -->_1 +#(s(N),s(M)) -> c_4(+#(N,M)):2 3:S:d#(s(N),s(M)) -> c_6(d#(N,M)) -->_1 d#(0(),N) -> c_5():16 -->_1 d#(s(N),s(M)) -> c_6(d#(N,M)):3 4:S:gcd#(NzN,NzM) -> c_8(u_31#(is_NzNat(NzN),is_NzNat(NzM),NzN,NzM),is_NzNat#(NzN),is_NzNat#(NzM)) -->_1 u_31#(True(),True(),NzN,NzM) -> c_27(u_3#(gt(NzN,NzM),NzN,NzM),gt#(NzN,NzM)):13 -->_3 is_NzNat#(s(N)) -> c_14():22 -->_2 is_NzNat#(s(N)) -> c_14():22 -->_3 is_NzNat#(0()) -> c_13():21 -->_2 is_NzNat#(0()) -> c_13():21 5:S:gt#(s(N),s(M)) -> c_12(gt#(N,M)) -->_1 gt#(NzN,0()) -> c_10(u_4#(is_NzNat(NzN)),is_NzNat#(NzN)):19 -->_1 gt#(0(),M) -> c_11():20 -->_1 gt#(s(N),s(M)) -> c_12(gt#(N,M)):5 6:S:lt#(N,M) -> c_15(gt#(M,N)) -->_1 gt#(NzN,0()) -> c_10(u_4#(is_NzNat(NzN)),is_NzNat#(NzN)):19 -->_1 gt#(0(),M) -> c_11():20 -->_1 gt#(s(N),s(M)) -> c_12(gt#(N,M)):5 7:S:quot#(N,NzM) -> c_17(u_11#(is_NzNat(NzM),N,NzM),is_NzNat#(NzM)) -->_1 u_11#(True(),N,NzM) -> c_23(u_1#(gt(N,NzM),N,NzM),gt#(N,NzM)):10 -->_2 is_NzNat#(s(N)) -> c_14():22 -->_2 is_NzNat#(0()) -> c_13():21 8:S:quot#(N,NzM) -> c_18(u_21#(is_NzNat(NzM),NzM,N),is_NzNat#(NzM)) -->_1 u_21#(True(),NzM,N) -> c_25(u_2#(gt(NzM,N)),gt#(NzM,N)):11 -->_2 is_NzNat#(s(N)) -> c_14():22 -->_2 is_NzNat#(0()) -> c_13():21 9:S:u_1#(True(),N,NzM) -> c_22(quot#(d(N,NzM),NzM),d#(N,NzM)) -->_1 quot#(NzM,NzM) -> c_19(u_01#(is_NzNat(NzM)),is_NzNat#(NzM)):24 -->_2 d#(0(),N) -> c_5():16 -->_1 quot#(N,NzM) -> c_18(u_21#(is_NzNat(NzM),NzM,N),is_NzNat#(NzM)):8 -->_1 quot#(N,NzM) -> c_17(u_11#(is_NzNat(NzM),N,NzM),is_NzNat#(NzM)):7 -->_2 d#(s(N),s(M)) -> c_6(d#(N,M)):3 10:S:u_11#(True(),N,NzM) -> c_23(u_1#(gt(N,NzM),N,NzM),gt#(N,NzM)) -->_2 gt#(NzN,0()) -> c_10(u_4#(is_NzNat(NzN)),is_NzNat#(NzN)):19 -->_2 gt#(0(),M) -> c_11():20 -->_1 u_1#(True(),N,NzM) -> c_22(quot#(d(N,NzM),NzM),d#(N,NzM)):9 -->_2 gt#(s(N),s(M)) -> c_12(gt#(N,M)):5 11:S:u_21#(True(),NzM,N) -> c_25(u_2#(gt(NzM,N)),gt#(NzM,N)) -->_2 gt#(NzN,0()) -> c_10(u_4#(is_NzNat(NzN)),is_NzNat#(NzN)):19 -->_1 u_2#(True()) -> c_24():27 -->_2 gt#(0(),M) -> c_11():20 -->_2 gt#(s(N),s(M)) -> c_12(gt#(N,M)):5 12:S:u_3#(True(),NzN,NzM) -> c_26(gcd#(d(NzN,NzM),NzM),d#(NzN,NzM)) -->_1 gcd#(NzM,NzM) -> c_7(u_02#(is_NzNat(NzM),NzM),is_NzNat#(NzM)):17 -->_1 gcd#(0(),N) -> c_9():18 -->_2 d#(0(),N) -> c_5():16 -->_1 gcd#(NzN,NzM) -> c_8(u_31#(is_NzNat(NzN),is_NzNat(NzM),NzN,NzM),is_NzNat#(NzN),is_NzNat#(NzM)):4 -->_2 d#(s(N),s(M)) -> c_6(d#(N,M)):3 13:S:u_31#(True(),True(),NzN,NzM) -> c_27(u_3#(gt(NzN,NzM),NzN,NzM),gt#(NzN,NzM)) -->_2 gt#(NzN,0()) -> c_10(u_4#(is_NzNat(NzN)),is_NzNat#(NzN)):19 -->_2 gt#(0(),M) -> c_11():20 -->_1 u_3#(True(),NzN,NzM) -> c_26(gcd#(d(NzN,NzM),NzM),d#(NzN,NzM)):12 -->_2 gt#(s(N),s(M)) -> c_12(gt#(N,M)):5 14:W:*#(N,0()) -> c_1() 15:W:+#(N,0()) -> c_3() 16:W:d#(0(),N) -> c_5() 17:W:gcd#(NzM,NzM) -> c_7(u_02#(is_NzNat(NzM),NzM),is_NzNat#(NzM)) -->_1 u_02#(True(),NzM) -> c_21():26 -->_2 is_NzNat#(s(N)) -> c_14():22 -->_2 is_NzNat#(0()) -> c_13():21 18:W:gcd#(0(),N) -> c_9() 19:W:gt#(NzN,0()) -> c_10(u_4#(is_NzNat(NzN)),is_NzNat#(NzN)) -->_1 u_4#(True()) -> c_28():28 -->_2 is_NzNat#(s(N)) -> c_14():22 -->_2 is_NzNat#(0()) -> c_13():21 20:W:gt#(0(),M) -> c_11() 21:W:is_NzNat#(0()) -> c_13() 22:W:is_NzNat#(s(N)) -> c_14() 23:W:p#(s(N)) -> c_16() 24:W:quot#(NzM,NzM) -> c_19(u_01#(is_NzNat(NzM)),is_NzNat#(NzM)) -->_1 u_01#(True()) -> c_20():25 -->_2 is_NzNat#(s(N)) -> c_14():22 -->_2 is_NzNat#(0()) -> c_13():21 25:W:u_01#(True()) -> c_20() 26:W:u_02#(True(),NzM) -> c_21() 27:W:u_2#(True()) -> c_24() 28:W:u_4#(True()) -> c_28() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 23: p#(s(N)) -> c_16() 27: u_2#(True()) -> c_24() 24: quot#(NzM,NzM) -> c_19(u_01#(is_NzNat(NzM)),is_NzNat#(NzM)) 25: u_01#(True()) -> c_20() 18: gcd#(0(),N) -> c_9() 17: gcd#(NzM,NzM) -> c_7(u_02#(is_NzNat(NzM),NzM),is_NzNat#(NzM)) 26: u_02#(True(),NzM) -> c_21() 20: gt#(0(),M) -> c_11() 19: gt#(NzN,0()) -> c_10(u_4#(is_NzNat(NzN)),is_NzNat#(NzN)) 21: is_NzNat#(0()) -> c_13() 22: is_NzNat#(s(N)) -> c_14() 28: u_4#(True()) -> c_28() 16: d#(0(),N) -> c_5() 14: *#(N,0()) -> c_1() 15: +#(N,0()) -> c_3() * Step 6: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: *#(s(N),s(M)) -> c_2(+#(N,+(M,*(N,M))),+#(M,*(N,M)),*#(N,M)) +#(s(N),s(M)) -> c_4(+#(N,M)) d#(s(N),s(M)) -> c_6(d#(N,M)) gcd#(NzN,NzM) -> c_8(u_31#(is_NzNat(NzN),is_NzNat(NzM),NzN,NzM),is_NzNat#(NzN),is_NzNat#(NzM)) gt#(s(N),s(M)) -> c_12(gt#(N,M)) lt#(N,M) -> c_15(gt#(M,N)) quot#(N,NzM) -> c_17(u_11#(is_NzNat(NzM),N,NzM),is_NzNat#(NzM)) quot#(N,NzM) -> c_18(u_21#(is_NzNat(NzM),NzM,N),is_NzNat#(NzM)) u_1#(True(),N,NzM) -> c_22(quot#(d(N,NzM),NzM),d#(N,NzM)) u_11#(True(),N,NzM) -> c_23(u_1#(gt(N,NzM),N,NzM),gt#(N,NzM)) u_21#(True(),NzM,N) -> c_25(u_2#(gt(NzM,N)),gt#(NzM,N)) u_3#(True(),NzN,NzM) -> c_26(gcd#(d(NzN,NzM),NzM),d#(NzN,NzM)) u_31#(True(),True(),NzN,NzM) -> c_27(u_3#(gt(NzN,NzM),NzN,NzM),gt#(NzN,NzM)) - Weak TRS: *(N,0()) -> 0() *(s(N),s(M)) -> s(+(N,+(M,*(N,M)))) +(N,0()) -> N +(s(N),s(M)) -> s(s(+(N,M))) d(0(),N) -> N d(s(N),s(M)) -> d(N,M) gt(NzN,0()) -> u_4(is_NzNat(NzN)) gt(0(),M) -> False() gt(s(N),s(M)) -> gt(N,M) is_NzNat(0()) -> False() is_NzNat(s(N)) -> True() u_4(True()) -> True() - Signature: {*/2,+/2,d/2,gcd/2,gt/2,is_NzNat/1,lt/2,p/1,quot/2,u_01/1,u_02/2,u_1/3,u_11/3,u_2/1,u_21/3,u_3/3,u_31/4 ,u_4/1,*#/2,+#/2,d#/2,gcd#/2,gt#/2,is_NzNat#/1,lt#/2,p#/1,quot#/2,u_01#/1,u_02#/2,u_1#/3,u_11#/3,u_2#/1 ,u_21#/3,u_3#/3,u_31#/4,u_4#/1} / {0/0,False/0,True/0,s/1,c_1/0,c_2/3,c_3/0,c_4/1,c_5/0,c_6/1,c_7/2,c_8/3 ,c_9/0,c_10/2,c_11/0,c_12/1,c_13/0,c_14/0,c_15/1,c_16/0,c_17/2,c_18/2,c_19/2,c_20/0,c_21/0,c_22/2,c_23/2 ,c_24/0,c_25/2,c_26/2,c_27/2,c_28/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,d#,gcd#,gt#,is_NzNat#,lt#,p#,quot#,u_01#,u_02#,u_1# ,u_11#,u_2#,u_21#,u_3#,u_31#,u_4#} and constructors {0,False,True,s} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:*#(s(N),s(M)) -> c_2(+#(N,+(M,*(N,M))),+#(M,*(N,M)),*#(N,M)) -->_2 +#(s(N),s(M)) -> c_4(+#(N,M)):2 -->_1 +#(s(N),s(M)) -> c_4(+#(N,M)):2 -->_3 *#(s(N),s(M)) -> c_2(+#(N,+(M,*(N,M))),+#(M,*(N,M)),*#(N,M)):1 2:S:+#(s(N),s(M)) -> c_4(+#(N,M)) -->_1 +#(s(N),s(M)) -> c_4(+#(N,M)):2 3:S:d#(s(N),s(M)) -> c_6(d#(N,M)) -->_1 d#(s(N),s(M)) -> c_6(d#(N,M)):3 4:S:gcd#(NzN,NzM) -> c_8(u_31#(is_NzNat(NzN),is_NzNat(NzM),NzN,NzM),is_NzNat#(NzN),is_NzNat#(NzM)) -->_1 u_31#(True(),True(),NzN,NzM) -> c_27(u_3#(gt(NzN,NzM),NzN,NzM),gt#(NzN,NzM)):13 5:S:gt#(s(N),s(M)) -> c_12(gt#(N,M)) -->_1 gt#(s(N),s(M)) -> c_12(gt#(N,M)):5 6:S:lt#(N,M) -> c_15(gt#(M,N)) -->_1 gt#(s(N),s(M)) -> c_12(gt#(N,M)):5 7:S:quot#(N,NzM) -> c_17(u_11#(is_NzNat(NzM),N,NzM),is_NzNat#(NzM)) -->_1 u_11#(True(),N,NzM) -> c_23(u_1#(gt(N,NzM),N,NzM),gt#(N,NzM)):10 8:S:quot#(N,NzM) -> c_18(u_21#(is_NzNat(NzM),NzM,N),is_NzNat#(NzM)) -->_1 u_21#(True(),NzM,N) -> c_25(u_2#(gt(NzM,N)),gt#(NzM,N)):11 9:S:u_1#(True(),N,NzM) -> c_22(quot#(d(N,NzM),NzM),d#(N,NzM)) -->_1 quot#(N,NzM) -> c_18(u_21#(is_NzNat(NzM),NzM,N),is_NzNat#(NzM)):8 -->_1 quot#(N,NzM) -> c_17(u_11#(is_NzNat(NzM),N,NzM),is_NzNat#(NzM)):7 -->_2 d#(s(N),s(M)) -> c_6(d#(N,M)):3 10:S:u_11#(True(),N,NzM) -> c_23(u_1#(gt(N,NzM),N,NzM),gt#(N,NzM)) -->_1 u_1#(True(),N,NzM) -> c_22(quot#(d(N,NzM),NzM),d#(N,NzM)):9 -->_2 gt#(s(N),s(M)) -> c_12(gt#(N,M)):5 11:S:u_21#(True(),NzM,N) -> c_25(u_2#(gt(NzM,N)),gt#(NzM,N)) -->_2 gt#(s(N),s(M)) -> c_12(gt#(N,M)):5 12:S:u_3#(True(),NzN,NzM) -> c_26(gcd#(d(NzN,NzM),NzM),d#(NzN,NzM)) -->_1 gcd#(NzN,NzM) -> c_8(u_31#(is_NzNat(NzN),is_NzNat(NzM),NzN,NzM),is_NzNat#(NzN),is_NzNat#(NzM)):4 -->_2 d#(s(N),s(M)) -> c_6(d#(N,M)):3 13:S:u_31#(True(),True(),NzN,NzM) -> c_27(u_3#(gt(NzN,NzM),NzN,NzM),gt#(NzN,NzM)) -->_1 u_3#(True(),NzN,NzM) -> c_26(gcd#(d(NzN,NzM),NzM),d#(NzN,NzM)):12 -->_2 gt#(s(N),s(M)) -> c_12(gt#(N,M)):5 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: gcd#(NzN,NzM) -> c_8(u_31#(is_NzNat(NzN),is_NzNat(NzM),NzN,NzM)) quot#(N,NzM) -> c_17(u_11#(is_NzNat(NzM),N,NzM)) quot#(N,NzM) -> c_18(u_21#(is_NzNat(NzM),NzM,N)) u_21#(True(),NzM,N) -> c_25(gt#(NzM,N)) * Step 7: RemoveHeads MAYBE + Considered Problem: - Strict DPs: *#(s(N),s(M)) -> c_2(+#(N,+(M,*(N,M))),+#(M,*(N,M)),*#(N,M)) +#(s(N),s(M)) -> c_4(+#(N,M)) d#(s(N),s(M)) -> c_6(d#(N,M)) gcd#(NzN,NzM) -> c_8(u_31#(is_NzNat(NzN),is_NzNat(NzM),NzN,NzM)) gt#(s(N),s(M)) -> c_12(gt#(N,M)) lt#(N,M) -> c_15(gt#(M,N)) quot#(N,NzM) -> c_17(u_11#(is_NzNat(NzM),N,NzM)) quot#(N,NzM) -> c_18(u_21#(is_NzNat(NzM),NzM,N)) u_1#(True(),N,NzM) -> c_22(quot#(d(N,NzM),NzM),d#(N,NzM)) u_11#(True(),N,NzM) -> c_23(u_1#(gt(N,NzM),N,NzM),gt#(N,NzM)) u_21#(True(),NzM,N) -> c_25(gt#(NzM,N)) u_3#(True(),NzN,NzM) -> c_26(gcd#(d(NzN,NzM),NzM),d#(NzN,NzM)) u_31#(True(),True(),NzN,NzM) -> c_27(u_3#(gt(NzN,NzM),NzN,NzM),gt#(NzN,NzM)) - Weak TRS: *(N,0()) -> 0() *(s(N),s(M)) -> s(+(N,+(M,*(N,M)))) +(N,0()) -> N +(s(N),s(M)) -> s(s(+(N,M))) d(0(),N) -> N d(s(N),s(M)) -> d(N,M) gt(NzN,0()) -> u_4(is_NzNat(NzN)) gt(0(),M) -> False() gt(s(N),s(M)) -> gt(N,M) is_NzNat(0()) -> False() is_NzNat(s(N)) -> True() u_4(True()) -> True() - Signature: {*/2,+/2,d/2,gcd/2,gt/2,is_NzNat/1,lt/2,p/1,quot/2,u_01/1,u_02/2,u_1/3,u_11/3,u_2/1,u_21/3,u_3/3,u_31/4 ,u_4/1,*#/2,+#/2,d#/2,gcd#/2,gt#/2,is_NzNat#/1,lt#/2,p#/1,quot#/2,u_01#/1,u_02#/2,u_1#/3,u_11#/3,u_2#/1 ,u_21#/3,u_3#/3,u_31#/4,u_4#/1} / {0/0,False/0,True/0,s/1,c_1/0,c_2/3,c_3/0,c_4/1,c_5/0,c_6/1,c_7/2,c_8/1 ,c_9/0,c_10/2,c_11/0,c_12/1,c_13/0,c_14/0,c_15/1,c_16/0,c_17/1,c_18/1,c_19/2,c_20/0,c_21/0,c_22/2,c_23/2 ,c_24/0,c_25/1,c_26/2,c_27/2,c_28/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,d#,gcd#,gt#,is_NzNat#,lt#,p#,quot#,u_01#,u_02#,u_1# ,u_11#,u_2#,u_21#,u_3#,u_31#,u_4#} and constructors {0,False,True,s} + Applied Processor: RemoveHeads + Details: Consider the dependency graph 1:S:*#(s(N),s(M)) -> c_2(+#(N,+(M,*(N,M))),+#(M,*(N,M)),*#(N,M)) -->_2 +#(s(N),s(M)) -> c_4(+#(N,M)):2 -->_1 +#(s(N),s(M)) -> c_4(+#(N,M)):2 -->_3 *#(s(N),s(M)) -> c_2(+#(N,+(M,*(N,M))),+#(M,*(N,M)),*#(N,M)):1 2:S:+#(s(N),s(M)) -> c_4(+#(N,M)) -->_1 +#(s(N),s(M)) -> c_4(+#(N,M)):2 3:S:d#(s(N),s(M)) -> c_6(d#(N,M)) -->_1 d#(s(N),s(M)) -> c_6(d#(N,M)):3 4:S:gcd#(NzN,NzM) -> c_8(u_31#(is_NzNat(NzN),is_NzNat(NzM),NzN,NzM)) -->_1 u_31#(True(),True(),NzN,NzM) -> c_27(u_3#(gt(NzN,NzM),NzN,NzM),gt#(NzN,NzM)):13 5:S:gt#(s(N),s(M)) -> c_12(gt#(N,M)) -->_1 gt#(s(N),s(M)) -> c_12(gt#(N,M)):5 6:S:lt#(N,M) -> c_15(gt#(M,N)) -->_1 gt#(s(N),s(M)) -> c_12(gt#(N,M)):5 7:S:quot#(N,NzM) -> c_17(u_11#(is_NzNat(NzM),N,NzM)) -->_1 u_11#(True(),N,NzM) -> c_23(u_1#(gt(N,NzM),N,NzM),gt#(N,NzM)):10 8:S:quot#(N,NzM) -> c_18(u_21#(is_NzNat(NzM),NzM,N)) -->_1 u_21#(True(),NzM,N) -> c_25(gt#(NzM,N)):11 9:S:u_1#(True(),N,NzM) -> c_22(quot#(d(N,NzM),NzM),d#(N,NzM)) -->_1 quot#(N,NzM) -> c_18(u_21#(is_NzNat(NzM),NzM,N)):8 -->_1 quot#(N,NzM) -> c_17(u_11#(is_NzNat(NzM),N,NzM)):7 -->_2 d#(s(N),s(M)) -> c_6(d#(N,M)):3 10:S:u_11#(True(),N,NzM) -> c_23(u_1#(gt(N,NzM),N,NzM),gt#(N,NzM)) -->_1 u_1#(True(),N,NzM) -> c_22(quot#(d(N,NzM),NzM),d#(N,NzM)):9 -->_2 gt#(s(N),s(M)) -> c_12(gt#(N,M)):5 11:S:u_21#(True(),NzM,N) -> c_25(gt#(NzM,N)) -->_1 gt#(s(N),s(M)) -> c_12(gt#(N,M)):5 12:S:u_3#(True(),NzN,NzM) -> c_26(gcd#(d(NzN,NzM),NzM),d#(NzN,NzM)) -->_1 gcd#(NzN,NzM) -> c_8(u_31#(is_NzNat(NzN),is_NzNat(NzM),NzN,NzM)):4 -->_2 d#(s(N),s(M)) -> c_6(d#(N,M)):3 13:S:u_31#(True(),True(),NzN,NzM) -> c_27(u_3#(gt(NzN,NzM),NzN,NzM),gt#(NzN,NzM)) -->_1 u_3#(True(),NzN,NzM) -> c_26(gcd#(d(NzN,NzM),NzM),d#(NzN,NzM)):12 -->_2 gt#(s(N),s(M)) -> c_12(gt#(N,M)):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). [(6,lt#(N,M) -> c_15(gt#(M,N)))] * Step 8: NaturalMI MAYBE + Considered Problem: - Strict DPs: *#(s(N),s(M)) -> c_2(+#(N,+(M,*(N,M))),+#(M,*(N,M)),*#(N,M)) +#(s(N),s(M)) -> c_4(+#(N,M)) d#(s(N),s(M)) -> c_6(d#(N,M)) gcd#(NzN,NzM) -> c_8(u_31#(is_NzNat(NzN),is_NzNat(NzM),NzN,NzM)) gt#(s(N),s(M)) -> c_12(gt#(N,M)) quot#(N,NzM) -> c_17(u_11#(is_NzNat(NzM),N,NzM)) quot#(N,NzM) -> c_18(u_21#(is_NzNat(NzM),NzM,N)) u_1#(True(),N,NzM) -> c_22(quot#(d(N,NzM),NzM),d#(N,NzM)) u_11#(True(),N,NzM) -> c_23(u_1#(gt(N,NzM),N,NzM),gt#(N,NzM)) u_21#(True(),NzM,N) -> c_25(gt#(NzM,N)) u_3#(True(),NzN,NzM) -> c_26(gcd#(d(NzN,NzM),NzM),d#(NzN,NzM)) u_31#(True(),True(),NzN,NzM) -> c_27(u_3#(gt(NzN,NzM),NzN,NzM),gt#(NzN,NzM)) - Weak TRS: *(N,0()) -> 0() *(s(N),s(M)) -> s(+(N,+(M,*(N,M)))) +(N,0()) -> N +(s(N),s(M)) -> s(s(+(N,M))) d(0(),N) -> N d(s(N),s(M)) -> d(N,M) gt(NzN,0()) -> u_4(is_NzNat(NzN)) gt(0(),M) -> False() gt(s(N),s(M)) -> gt(N,M) is_NzNat(0()) -> False() is_NzNat(s(N)) -> True() u_4(True()) -> True() - Signature: {*/2,+/2,d/2,gcd/2,gt/2,is_NzNat/1,lt/2,p/1,quot/2,u_01/1,u_02/2,u_1/3,u_11/3,u_2/1,u_21/3,u_3/3,u_31/4 ,u_4/1,*#/2,+#/2,d#/2,gcd#/2,gt#/2,is_NzNat#/1,lt#/2,p#/1,quot#/2,u_01#/1,u_02#/2,u_1#/3,u_11#/3,u_2#/1 ,u_21#/3,u_3#/3,u_31#/4,u_4#/1} / {0/0,False/0,True/0,s/1,c_1/0,c_2/3,c_3/0,c_4/1,c_5/0,c_6/1,c_7/2,c_8/1 ,c_9/0,c_10/2,c_11/0,c_12/1,c_13/0,c_14/0,c_15/1,c_16/0,c_17/1,c_18/1,c_19/2,c_20/0,c_21/0,c_22/2,c_23/2 ,c_24/0,c_25/1,c_26/2,c_27/2,c_28/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,d#,gcd#,gt#,is_NzNat#,lt#,p#,quot#,u_01#,u_02#,u_1# ,u_11#,u_2#,u_21#,u_3#,u_31#,u_4#} and constructors {0,False,True,s} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 0, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 0 non-zero interpretation-entries in the diagonal of the component-wise maxima): The following argument positions are considered usable: uargs(c_2) = {1,2,3}, uargs(c_4) = {1}, uargs(c_6) = {1}, uargs(c_8) = {1}, uargs(c_12) = {1}, uargs(c_17) = {1}, uargs(c_18) = {1}, uargs(c_22) = {1,2}, uargs(c_23) = {1,2}, uargs(c_25) = {1}, uargs(c_26) = {1,2}, uargs(c_27) = {1,2} Following symbols are considered usable: {is_NzNat,*#,+#,d#,gcd#,gt#,is_NzNat#,lt#,p#,quot#,u_01#,u_02#,u_1#,u_11#,u_2#,u_21#,u_3#,u_31#,u_4#} TcT has computed the following interpretation: p(*) = [4] x2 + [6] p(+) = [2] x1 + [1] x2 + [0] p(0) = [1] p(False) = [0] p(True) = [1] p(d) = [0] p(gcd) = [1] x1 + [0] p(gt) = [0] p(is_NzNat) = [1] p(lt) = [4] x2 + [0] p(p) = [0] p(quot) = [1] p(s) = [0] p(u_01) = [4] x1 + [4] p(u_02) = [4] x1 + [1] x2 + [0] p(u_1) = [1] x2 + [1] x3 + [2] p(u_11) = [4] x3 + [2] p(u_2) = [2] x1 + [1] p(u_21) = [2] x2 + [0] p(u_3) = [1] x1 + [1] x2 + [1] x3 + [2] p(u_31) = [2] x1 + [1] x4 + [0] p(u_4) = [6] x1 + [6] p(*#) = [0] p(+#) = [0] p(d#) = [0] p(gcd#) = [0] p(gt#) = [0] p(is_NzNat#) = [0] p(lt#) = [1] x1 + [2] p(p#) = [0] p(quot#) = [4] x2 + [4] p(u_01#) = [1] p(u_02#) = [4] x1 + [4] p(u_1#) = [4] x3 + [4] p(u_11#) = [3] x1 + [4] x3 + [1] p(u_2#) = [0] p(u_21#) = [4] x1 + [0] p(u_3#) = [0] p(u_31#) = [0] p(u_4#) = [4] p(c_1) = [1] p(c_2) = [2] x1 + [4] x2 + [4] x3 + [0] p(c_3) = [4] p(c_4) = [4] x1 + [0] p(c_5) = [0] p(c_6) = [4] x1 + [0] p(c_7) = [1] x1 + [1] p(c_8) = [2] x1 + [0] p(c_9) = [2] p(c_10) = [4] x2 + [1] p(c_11) = [1] p(c_12) = [4] x1 + [0] p(c_13) = [0] p(c_14) = [1] p(c_15) = [0] p(c_16) = [4] p(c_17) = [1] x1 + [0] p(c_18) = [1] x1 + [0] p(c_19) = [2] p(c_20) = [1] p(c_21) = [0] p(c_22) = [1] x1 + [2] x2 + [0] p(c_23) = [1] x1 + [2] x2 + [0] p(c_24) = [4] p(c_25) = [2] x1 + [0] p(c_26) = [2] x1 + [2] x2 + [0] p(c_27) = [4] x1 + [4] x2 + [0] p(c_28) = [0] Following rules are strictly oriented: u_21#(True(),NzM,N) = [4] > [0] = c_25(gt#(NzM,N)) Following rules are (at-least) weakly oriented: *#(s(N),s(M)) = [0] >= [0] = c_2(+#(N,+(M,*(N,M))),+#(M,*(N,M)),*#(N,M)) +#(s(N),s(M)) = [0] >= [0] = c_4(+#(N,M)) d#(s(N),s(M)) = [0] >= [0] = c_6(d#(N,M)) gcd#(NzN,NzM) = [0] >= [0] = c_8(u_31#(is_NzNat(NzN),is_NzNat(NzM),NzN,NzM)) gt#(s(N),s(M)) = [0] >= [0] = c_12(gt#(N,M)) quot#(N,NzM) = [4] NzM + [4] >= [4] NzM + [4] = c_17(u_11#(is_NzNat(NzM),N,NzM)) quot#(N,NzM) = [4] NzM + [4] >= [4] = c_18(u_21#(is_NzNat(NzM),NzM,N)) u_1#(True(),N,NzM) = [4] NzM + [4] >= [4] NzM + [4] = c_22(quot#(d(N,NzM),NzM),d#(N,NzM)) u_11#(True(),N,NzM) = [4] NzM + [4] >= [4] NzM + [4] = c_23(u_1#(gt(N,NzM),N,NzM),gt#(N,NzM)) u_3#(True(),NzN,NzM) = [0] >= [0] = c_26(gcd#(d(NzN,NzM),NzM),d#(NzN,NzM)) u_31#(True(),True(),NzN,NzM) = [0] >= [0] = c_27(u_3#(gt(NzN,NzM),NzN,NzM),gt#(NzN,NzM)) is_NzNat(0()) = [1] >= [0] = False() is_NzNat(s(N)) = [1] >= [1] = True() * Step 9: NaturalMI MAYBE + Considered Problem: - Strict DPs: *#(s(N),s(M)) -> c_2(+#(N,+(M,*(N,M))),+#(M,*(N,M)),*#(N,M)) +#(s(N),s(M)) -> c_4(+#(N,M)) d#(s(N),s(M)) -> c_6(d#(N,M)) gcd#(NzN,NzM) -> c_8(u_31#(is_NzNat(NzN),is_NzNat(NzM),NzN,NzM)) gt#(s(N),s(M)) -> c_12(gt#(N,M)) quot#(N,NzM) -> c_17(u_11#(is_NzNat(NzM),N,NzM)) quot#(N,NzM) -> c_18(u_21#(is_NzNat(NzM),NzM,N)) u_1#(True(),N,NzM) -> c_22(quot#(d(N,NzM),NzM),d#(N,NzM)) u_11#(True(),N,NzM) -> c_23(u_1#(gt(N,NzM),N,NzM),gt#(N,NzM)) u_3#(True(),NzN,NzM) -> c_26(gcd#(d(NzN,NzM),NzM),d#(NzN,NzM)) u_31#(True(),True(),NzN,NzM) -> c_27(u_3#(gt(NzN,NzM),NzN,NzM),gt#(NzN,NzM)) - Weak DPs: u_21#(True(),NzM,N) -> c_25(gt#(NzM,N)) - Weak TRS: *(N,0()) -> 0() *(s(N),s(M)) -> s(+(N,+(M,*(N,M)))) +(N,0()) -> N +(s(N),s(M)) -> s(s(+(N,M))) d(0(),N) -> N d(s(N),s(M)) -> d(N,M) gt(NzN,0()) -> u_4(is_NzNat(NzN)) gt(0(),M) -> False() gt(s(N),s(M)) -> gt(N,M) is_NzNat(0()) -> False() is_NzNat(s(N)) -> True() u_4(True()) -> True() - Signature: {*/2,+/2,d/2,gcd/2,gt/2,is_NzNat/1,lt/2,p/1,quot/2,u_01/1,u_02/2,u_1/3,u_11/3,u_2/1,u_21/3,u_3/3,u_31/4 ,u_4/1,*#/2,+#/2,d#/2,gcd#/2,gt#/2,is_NzNat#/1,lt#/2,p#/1,quot#/2,u_01#/1,u_02#/2,u_1#/3,u_11#/3,u_2#/1 ,u_21#/3,u_3#/3,u_31#/4,u_4#/1} / {0/0,False/0,True/0,s/1,c_1/0,c_2/3,c_3/0,c_4/1,c_5/0,c_6/1,c_7/2,c_8/1 ,c_9/0,c_10/2,c_11/0,c_12/1,c_13/0,c_14/0,c_15/1,c_16/0,c_17/1,c_18/1,c_19/2,c_20/0,c_21/0,c_22/2,c_23/2 ,c_24/0,c_25/1,c_26/2,c_27/2,c_28/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,d#,gcd#,gt#,is_NzNat#,lt#,p#,quot#,u_01#,u_02#,u_1# ,u_11#,u_2#,u_21#,u_3#,u_31#,u_4#} and constructors {0,False,True,s} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 0, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 0 non-zero interpretation-entries in the diagonal of the component-wise maxima): The following argument positions are considered usable: uargs(c_2) = {1,2,3}, uargs(c_4) = {1}, uargs(c_6) = {1}, uargs(c_8) = {1}, uargs(c_12) = {1}, uargs(c_17) = {1}, uargs(c_18) = {1}, uargs(c_22) = {1,2}, uargs(c_23) = {1,2}, uargs(c_25) = {1}, uargs(c_26) = {1,2}, uargs(c_27) = {1,2} Following symbols are considered usable: {gt,u_4,*#,+#,d#,gcd#,gt#,is_NzNat#,lt#,p#,quot#,u_01#,u_02#,u_1#,u_11#,u_2#,u_21#,u_3#,u_31#,u_4#} TcT has computed the following interpretation: p(*) = [1] x1 + [1] x2 + [0] p(+) = [0] p(0) = [0] p(False) = [0] p(True) = [1] p(d) = [4] x1 + [0] p(gcd) = [4] x1 + [1] p(gt) = [1] p(is_NzNat) = [0] p(lt) = [2] x1 + [1] p(p) = [1] p(quot) = [4] x1 + [1] p(s) = [0] p(u_01) = [0] p(u_02) = [2] p(u_1) = [1] x1 + [1] p(u_11) = [1] x1 + [1] p(u_2) = [1] x1 + [1] p(u_21) = [1] p(u_3) = [4] x2 + [2] x3 + [0] p(u_31) = [2] x1 + [1] x3 + [2] p(u_4) = [1] p(*#) = [0] p(+#) = [0] p(d#) = [0] p(gcd#) = [0] p(gt#) = [0] p(is_NzNat#) = [1] p(lt#) = [1] x1 + [1] x2 + [2] p(p#) = [4] p(quot#) = [4] p(u_01#) = [1] p(u_02#) = [0] p(u_1#) = [4] x1 + [0] p(u_11#) = [4] p(u_2#) = [1] p(u_21#) = [0] p(u_3#) = [0] p(u_31#) = [0] p(u_4#) = [1] p(c_1) = [0] p(c_2) = [2] x1 + [1] x2 + [1] x3 + [0] p(c_3) = [1] p(c_4) = [4] x1 + [0] p(c_5) = [4] p(c_6) = [4] x1 + [0] p(c_7) = [0] p(c_8) = [2] x1 + [0] p(c_9) = [4] p(c_10) = [4] x1 + [0] p(c_11) = [1] p(c_12) = [4] x1 + [0] p(c_13) = [0] p(c_14) = [0] p(c_15) = [4] x1 + [4] p(c_16) = [0] p(c_17) = [1] x1 + [0] p(c_18) = [4] x1 + [2] p(c_19) = [1] x1 + [1] x2 + [0] p(c_20) = [1] p(c_21) = [0] p(c_22) = [1] x1 + [4] x2 + [0] p(c_23) = [1] x1 + [4] x2 + [0] p(c_24) = [1] p(c_25) = [4] x1 + [0] p(c_26) = [2] x1 + [1] x2 + [0] p(c_27) = [2] x1 + [4] x2 + [0] p(c_28) = [0] Following rules are strictly oriented: quot#(N,NzM) = [4] > [2] = c_18(u_21#(is_NzNat(NzM),NzM,N)) Following rules are (at-least) weakly oriented: *#(s(N),s(M)) = [0] >= [0] = c_2(+#(N,+(M,*(N,M))),+#(M,*(N,M)),*#(N,M)) +#(s(N),s(M)) = [0] >= [0] = c_4(+#(N,M)) d#(s(N),s(M)) = [0] >= [0] = c_6(d#(N,M)) gcd#(NzN,NzM) = [0] >= [0] = c_8(u_31#(is_NzNat(NzN),is_NzNat(NzM),NzN,NzM)) gt#(s(N),s(M)) = [0] >= [0] = c_12(gt#(N,M)) quot#(N,NzM) = [4] >= [4] = c_17(u_11#(is_NzNat(NzM),N,NzM)) u_1#(True(),N,NzM) = [4] >= [4] = c_22(quot#(d(N,NzM),NzM),d#(N,NzM)) u_11#(True(),N,NzM) = [4] >= [4] = c_23(u_1#(gt(N,NzM),N,NzM),gt#(N,NzM)) u_21#(True(),NzM,N) = [0] >= [0] = c_25(gt#(NzM,N)) u_3#(True(),NzN,NzM) = [0] >= [0] = c_26(gcd#(d(NzN,NzM),NzM),d#(NzN,NzM)) u_31#(True(),True(),NzN,NzM) = [0] >= [0] = c_27(u_3#(gt(NzN,NzM),NzN,NzM),gt#(NzN,NzM)) gt(NzN,0()) = [1] >= [1] = u_4(is_NzNat(NzN)) gt(0(),M) = [1] >= [0] = False() gt(s(N),s(M)) = [1] >= [1] = gt(N,M) u_4(True()) = [1] >= [1] = True() * Step 10: Failure MAYBE + Considered Problem: - Strict DPs: *#(s(N),s(M)) -> c_2(+#(N,+(M,*(N,M))),+#(M,*(N,M)),*#(N,M)) +#(s(N),s(M)) -> c_4(+#(N,M)) d#(s(N),s(M)) -> c_6(d#(N,M)) gcd#(NzN,NzM) -> c_8(u_31#(is_NzNat(NzN),is_NzNat(NzM),NzN,NzM)) gt#(s(N),s(M)) -> c_12(gt#(N,M)) quot#(N,NzM) -> c_17(u_11#(is_NzNat(NzM),N,NzM)) u_1#(True(),N,NzM) -> c_22(quot#(d(N,NzM),NzM),d#(N,NzM)) u_11#(True(),N,NzM) -> c_23(u_1#(gt(N,NzM),N,NzM),gt#(N,NzM)) u_3#(True(),NzN,NzM) -> c_26(gcd#(d(NzN,NzM),NzM),d#(NzN,NzM)) u_31#(True(),True(),NzN,NzM) -> c_27(u_3#(gt(NzN,NzM),NzN,NzM),gt#(NzN,NzM)) - Weak DPs: quot#(N,NzM) -> c_18(u_21#(is_NzNat(NzM),NzM,N)) u_21#(True(),NzM,N) -> c_25(gt#(NzM,N)) - Weak TRS: *(N,0()) -> 0() *(s(N),s(M)) -> s(+(N,+(M,*(N,M)))) +(N,0()) -> N +(s(N),s(M)) -> s(s(+(N,M))) d(0(),N) -> N d(s(N),s(M)) -> d(N,M) gt(NzN,0()) -> u_4(is_NzNat(NzN)) gt(0(),M) -> False() gt(s(N),s(M)) -> gt(N,M) is_NzNat(0()) -> False() is_NzNat(s(N)) -> True() u_4(True()) -> True() - Signature: {*/2,+/2,d/2,gcd/2,gt/2,is_NzNat/1,lt/2,p/1,quot/2,u_01/1,u_02/2,u_1/3,u_11/3,u_2/1,u_21/3,u_3/3,u_31/4 ,u_4/1,*#/2,+#/2,d#/2,gcd#/2,gt#/2,is_NzNat#/1,lt#/2,p#/1,quot#/2,u_01#/1,u_02#/2,u_1#/3,u_11#/3,u_2#/1 ,u_21#/3,u_3#/3,u_31#/4,u_4#/1} / {0/0,False/0,True/0,s/1,c_1/0,c_2/3,c_3/0,c_4/1,c_5/0,c_6/1,c_7/2,c_8/1 ,c_9/0,c_10/2,c_11/0,c_12/1,c_13/0,c_14/0,c_15/1,c_16/0,c_17/1,c_18/1,c_19/2,c_20/0,c_21/0,c_22/2,c_23/2 ,c_24/0,c_25/1,c_26/2,c_27/2,c_28/0} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,d#,gcd#,gt#,is_NzNat#,lt#,p#,quot#,u_01#,u_02#,u_1# ,u_11#,u_2#,u_21#,u_3#,u_31#,u_4#} and constructors {0,False,True,s} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE