MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { p(s(N)) -> N , +(N, 0()) -> N , +(s(N), s(M)) -> s(s(+(N, M))) , *(N, 0()) -> 0() , *(s(N), s(M)) -> s(+(N, +(M, *(N, M)))) , gt(NzN, 0()) -> u_4(is_NzNat(NzN)) , gt(s(N), s(M)) -> gt(N, M) , gt(0(), M) -> False() , u_4(True()) -> True() , is_NzNat(s(N)) -> True() , is_NzNat(0()) -> False() , lt(N, M) -> gt(M, N) , d(s(N), s(M)) -> d(N, M) , d(0(), N) -> N , quot(NzM, NzM) -> u_01(is_NzNat(NzM)) , quot(N, NzM) -> u_11(is_NzNat(NzM), N, NzM) , quot(N, NzM) -> u_21(is_NzNat(NzM), NzM, N) , u_11(True(), N, NzM) -> u_1(gt(N, NzM), N, NzM) , u_1(True(), N, NzM) -> s(quot(d(N, NzM), NzM)) , u_01(True()) -> s(0()) , u_21(True(), NzM, N) -> u_2(gt(NzM, N)) , u_2(True()) -> 0() , 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() , u_02(True(), NzM) -> NzM , u_31(True(), True(), NzN, NzM) -> u_3(gt(NzN, NzM), NzN, NzM) , u_3(True(), NzN, NzM) -> gcd(d(NzN, NzM), NzM) } Obligation: runtime complexity Answer: MAYBE None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem (timeout of 60 seconds)' failed due to the following reason: Computation stopped due to timeout after 60.0 seconds. 2) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem (timeout of 30 seconds) (timeout of 60 seconds)' failed due to the following reason: Computation stopped due to timeout after 30.0 seconds. 2) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'bsearch-popstar (timeout of 60 seconds)' failed due to the following reason: The processor is inapplicable, reason: Processor only applicable for innermost runtime complexity analysis 2) 'Polynomial Path Order (PS) (timeout of 60 seconds)' failed due to the following reason: The processor is inapplicable, reason: Processor only applicable for innermost runtime complexity analysis 3) 'Fastest (timeout of 5 seconds) (timeout of 60 seconds)' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'Bounds with perSymbol-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 2) 'Bounds with minimal-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 3) 'Innermost Weak Dependency Pairs (timeout of 60 seconds)' failed due to the following reason: We add the following weak dependency pairs: Strict DPs: { p^#(s(N)) -> c_1(N) , +^#(N, 0()) -> c_2(N) , +^#(s(N), s(M)) -> c_3(+^#(N, M)) , *^#(N, 0()) -> c_4() , *^#(s(N), s(M)) -> c_5(+^#(N, +(M, *(N, M)))) , gt^#(NzN, 0()) -> c_6(u_4^#(is_NzNat(NzN))) , gt^#(s(N), s(M)) -> c_7(gt^#(N, M)) , gt^#(0(), M) -> c_8() , u_4^#(True()) -> c_9() , is_NzNat^#(s(N)) -> c_10() , is_NzNat^#(0()) -> c_11() , lt^#(N, M) -> c_12(gt^#(M, N)) , d^#(s(N), s(M)) -> c_13(d^#(N, M)) , d^#(0(), N) -> c_14(N) , quot^#(NzM, NzM) -> c_15(u_01^#(is_NzNat(NzM))) , quot^#(N, NzM) -> c_16(u_11^#(is_NzNat(NzM), N, NzM)) , quot^#(N, NzM) -> c_17(u_21^#(is_NzNat(NzM), NzM, N)) , u_01^#(True()) -> c_20() , u_11^#(True(), N, NzM) -> c_18(u_1^#(gt(N, NzM), N, NzM)) , u_21^#(True(), NzM, N) -> c_21(u_2^#(gt(NzM, N))) , u_1^#(True(), N, NzM) -> c_19(quot^#(d(N, NzM), NzM)) , u_2^#(True()) -> c_22() , gcd^#(NzM, NzM) -> c_23(u_02^#(is_NzNat(NzM), NzM)) , gcd^#(NzN, NzM) -> c_24(u_31^#(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM)) , gcd^#(0(), N) -> c_25() , u_02^#(True(), NzM) -> c_26(NzM) , u_31^#(True(), True(), NzN, NzM) -> c_27(u_3^#(gt(NzN, NzM), NzN, NzM)) , u_3^#(True(), NzN, NzM) -> c_28(gcd^#(d(NzN, NzM), NzM)) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { p^#(s(N)) -> c_1(N) , +^#(N, 0()) -> c_2(N) , +^#(s(N), s(M)) -> c_3(+^#(N, M)) , *^#(N, 0()) -> c_4() , *^#(s(N), s(M)) -> c_5(+^#(N, +(M, *(N, M)))) , gt^#(NzN, 0()) -> c_6(u_4^#(is_NzNat(NzN))) , gt^#(s(N), s(M)) -> c_7(gt^#(N, M)) , gt^#(0(), M) -> c_8() , u_4^#(True()) -> c_9() , is_NzNat^#(s(N)) -> c_10() , is_NzNat^#(0()) -> c_11() , lt^#(N, M) -> c_12(gt^#(M, N)) , d^#(s(N), s(M)) -> c_13(d^#(N, M)) , d^#(0(), N) -> c_14(N) , quot^#(NzM, NzM) -> c_15(u_01^#(is_NzNat(NzM))) , quot^#(N, NzM) -> c_16(u_11^#(is_NzNat(NzM), N, NzM)) , quot^#(N, NzM) -> c_17(u_21^#(is_NzNat(NzM), NzM, N)) , u_01^#(True()) -> c_20() , u_11^#(True(), N, NzM) -> c_18(u_1^#(gt(N, NzM), N, NzM)) , u_21^#(True(), NzM, N) -> c_21(u_2^#(gt(NzM, N))) , u_1^#(True(), N, NzM) -> c_19(quot^#(d(N, NzM), NzM)) , u_2^#(True()) -> c_22() , gcd^#(NzM, NzM) -> c_23(u_02^#(is_NzNat(NzM), NzM)) , gcd^#(NzN, NzM) -> c_24(u_31^#(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM)) , gcd^#(0(), N) -> c_25() , u_02^#(True(), NzM) -> c_26(NzM) , u_31^#(True(), True(), NzN, NzM) -> c_27(u_3^#(gt(NzN, NzM), NzN, NzM)) , u_3^#(True(), NzN, NzM) -> c_28(gcd^#(d(NzN, NzM), NzM)) } Strict Trs: { p(s(N)) -> N , +(N, 0()) -> N , +(s(N), s(M)) -> s(s(+(N, M))) , *(N, 0()) -> 0() , *(s(N), s(M)) -> s(+(N, +(M, *(N, M)))) , gt(NzN, 0()) -> u_4(is_NzNat(NzN)) , gt(s(N), s(M)) -> gt(N, M) , gt(0(), M) -> False() , u_4(True()) -> True() , is_NzNat(s(N)) -> True() , is_NzNat(0()) -> False() , lt(N, M) -> gt(M, N) , d(s(N), s(M)) -> d(N, M) , d(0(), N) -> N , quot(NzM, NzM) -> u_01(is_NzNat(NzM)) , quot(N, NzM) -> u_11(is_NzNat(NzM), N, NzM) , quot(N, NzM) -> u_21(is_NzNat(NzM), NzM, N) , u_11(True(), N, NzM) -> u_1(gt(N, NzM), N, NzM) , u_1(True(), N, NzM) -> s(quot(d(N, NzM), NzM)) , u_01(True()) -> s(0()) , u_21(True(), NzM, N) -> u_2(gt(NzM, N)) , u_2(True()) -> 0() , 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() , u_02(True(), NzM) -> NzM , u_31(True(), True(), NzN, NzM) -> u_3(gt(NzN, NzM), NzN, NzM) , u_3(True(), NzN, NzM) -> gcd(d(NzN, NzM), NzM) } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {4,8,9,10,11,18,22,25} by applications of Pre({4,8,9,10,11,18,22,25}) = {1,2,6,7,12,14,15,20,26,28}. Here rules are labeled as follows: DPs: { 1: p^#(s(N)) -> c_1(N) , 2: +^#(N, 0()) -> c_2(N) , 3: +^#(s(N), s(M)) -> c_3(+^#(N, M)) , 4: *^#(N, 0()) -> c_4() , 5: *^#(s(N), s(M)) -> c_5(+^#(N, +(M, *(N, M)))) , 6: gt^#(NzN, 0()) -> c_6(u_4^#(is_NzNat(NzN))) , 7: gt^#(s(N), s(M)) -> c_7(gt^#(N, M)) , 8: gt^#(0(), M) -> c_8() , 9: u_4^#(True()) -> c_9() , 10: is_NzNat^#(s(N)) -> c_10() , 11: is_NzNat^#(0()) -> c_11() , 12: lt^#(N, M) -> c_12(gt^#(M, N)) , 13: d^#(s(N), s(M)) -> c_13(d^#(N, M)) , 14: d^#(0(), N) -> c_14(N) , 15: quot^#(NzM, NzM) -> c_15(u_01^#(is_NzNat(NzM))) , 16: quot^#(N, NzM) -> c_16(u_11^#(is_NzNat(NzM), N, NzM)) , 17: quot^#(N, NzM) -> c_17(u_21^#(is_NzNat(NzM), NzM, N)) , 18: u_01^#(True()) -> c_20() , 19: u_11^#(True(), N, NzM) -> c_18(u_1^#(gt(N, NzM), N, NzM)) , 20: u_21^#(True(), NzM, N) -> c_21(u_2^#(gt(NzM, N))) , 21: u_1^#(True(), N, NzM) -> c_19(quot^#(d(N, NzM), NzM)) , 22: u_2^#(True()) -> c_22() , 23: gcd^#(NzM, NzM) -> c_23(u_02^#(is_NzNat(NzM), NzM)) , 24: gcd^#(NzN, NzM) -> c_24(u_31^#(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM)) , 25: gcd^#(0(), N) -> c_25() , 26: u_02^#(True(), NzM) -> c_26(NzM) , 27: u_31^#(True(), True(), NzN, NzM) -> c_27(u_3^#(gt(NzN, NzM), NzN, NzM)) , 28: u_3^#(True(), NzN, NzM) -> c_28(gcd^#(d(NzN, NzM), NzM)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { p^#(s(N)) -> c_1(N) , +^#(N, 0()) -> c_2(N) , +^#(s(N), s(M)) -> c_3(+^#(N, M)) , *^#(s(N), s(M)) -> c_5(+^#(N, +(M, *(N, M)))) , gt^#(NzN, 0()) -> c_6(u_4^#(is_NzNat(NzN))) , gt^#(s(N), s(M)) -> c_7(gt^#(N, M)) , lt^#(N, M) -> c_12(gt^#(M, N)) , d^#(s(N), s(M)) -> c_13(d^#(N, M)) , d^#(0(), N) -> c_14(N) , quot^#(NzM, NzM) -> c_15(u_01^#(is_NzNat(NzM))) , quot^#(N, NzM) -> c_16(u_11^#(is_NzNat(NzM), N, NzM)) , quot^#(N, NzM) -> c_17(u_21^#(is_NzNat(NzM), NzM, N)) , u_11^#(True(), N, NzM) -> c_18(u_1^#(gt(N, NzM), N, NzM)) , u_21^#(True(), NzM, N) -> c_21(u_2^#(gt(NzM, N))) , u_1^#(True(), N, NzM) -> c_19(quot^#(d(N, NzM), NzM)) , gcd^#(NzM, NzM) -> c_23(u_02^#(is_NzNat(NzM), NzM)) , gcd^#(NzN, NzM) -> c_24(u_31^#(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM)) , u_02^#(True(), NzM) -> c_26(NzM) , u_31^#(True(), True(), NzN, NzM) -> c_27(u_3^#(gt(NzN, NzM), NzN, NzM)) , u_3^#(True(), NzN, NzM) -> c_28(gcd^#(d(NzN, NzM), NzM)) } Strict Trs: { p(s(N)) -> N , +(N, 0()) -> N , +(s(N), s(M)) -> s(s(+(N, M))) , *(N, 0()) -> 0() , *(s(N), s(M)) -> s(+(N, +(M, *(N, M)))) , gt(NzN, 0()) -> u_4(is_NzNat(NzN)) , gt(s(N), s(M)) -> gt(N, M) , gt(0(), M) -> False() , u_4(True()) -> True() , is_NzNat(s(N)) -> True() , is_NzNat(0()) -> False() , lt(N, M) -> gt(M, N) , d(s(N), s(M)) -> d(N, M) , d(0(), N) -> N , quot(NzM, NzM) -> u_01(is_NzNat(NzM)) , quot(N, NzM) -> u_11(is_NzNat(NzM), N, NzM) , quot(N, NzM) -> u_21(is_NzNat(NzM), NzM, N) , u_11(True(), N, NzM) -> u_1(gt(N, NzM), N, NzM) , u_1(True(), N, NzM) -> s(quot(d(N, NzM), NzM)) , u_01(True()) -> s(0()) , u_21(True(), NzM, N) -> u_2(gt(NzM, N)) , u_2(True()) -> 0() , 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() , u_02(True(), NzM) -> NzM , u_31(True(), True(), NzN, NzM) -> u_3(gt(NzN, NzM), NzN, NzM) , u_3(True(), NzN, NzM) -> gcd(d(NzN, NzM), NzM) } Weak DPs: { *^#(N, 0()) -> c_4() , gt^#(0(), M) -> c_8() , u_4^#(True()) -> c_9() , is_NzNat^#(s(N)) -> c_10() , is_NzNat^#(0()) -> c_11() , u_01^#(True()) -> c_20() , u_2^#(True()) -> c_22() , gcd^#(0(), N) -> c_25() } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {5,10,14} by applications of Pre({5,10,14}) = {1,2,6,7,9,12,15,18}. Here rules are labeled as follows: DPs: { 1: p^#(s(N)) -> c_1(N) , 2: +^#(N, 0()) -> c_2(N) , 3: +^#(s(N), s(M)) -> c_3(+^#(N, M)) , 4: *^#(s(N), s(M)) -> c_5(+^#(N, +(M, *(N, M)))) , 5: gt^#(NzN, 0()) -> c_6(u_4^#(is_NzNat(NzN))) , 6: gt^#(s(N), s(M)) -> c_7(gt^#(N, M)) , 7: lt^#(N, M) -> c_12(gt^#(M, N)) , 8: d^#(s(N), s(M)) -> c_13(d^#(N, M)) , 9: d^#(0(), N) -> c_14(N) , 10: quot^#(NzM, NzM) -> c_15(u_01^#(is_NzNat(NzM))) , 11: quot^#(N, NzM) -> c_16(u_11^#(is_NzNat(NzM), N, NzM)) , 12: quot^#(N, NzM) -> c_17(u_21^#(is_NzNat(NzM), NzM, N)) , 13: u_11^#(True(), N, NzM) -> c_18(u_1^#(gt(N, NzM), N, NzM)) , 14: u_21^#(True(), NzM, N) -> c_21(u_2^#(gt(NzM, N))) , 15: u_1^#(True(), N, NzM) -> c_19(quot^#(d(N, NzM), NzM)) , 16: gcd^#(NzM, NzM) -> c_23(u_02^#(is_NzNat(NzM), NzM)) , 17: gcd^#(NzN, NzM) -> c_24(u_31^#(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM)) , 18: u_02^#(True(), NzM) -> c_26(NzM) , 19: u_31^#(True(), True(), NzN, NzM) -> c_27(u_3^#(gt(NzN, NzM), NzN, NzM)) , 20: u_3^#(True(), NzN, NzM) -> c_28(gcd^#(d(NzN, NzM), NzM)) , 21: *^#(N, 0()) -> c_4() , 22: gt^#(0(), M) -> c_8() , 23: u_4^#(True()) -> c_9() , 24: is_NzNat^#(s(N)) -> c_10() , 25: is_NzNat^#(0()) -> c_11() , 26: u_01^#(True()) -> c_20() , 27: u_2^#(True()) -> c_22() , 28: gcd^#(0(), N) -> c_25() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { p^#(s(N)) -> c_1(N) , +^#(N, 0()) -> c_2(N) , +^#(s(N), s(M)) -> c_3(+^#(N, M)) , *^#(s(N), s(M)) -> c_5(+^#(N, +(M, *(N, M)))) , gt^#(s(N), s(M)) -> c_7(gt^#(N, M)) , lt^#(N, M) -> c_12(gt^#(M, N)) , d^#(s(N), s(M)) -> c_13(d^#(N, M)) , d^#(0(), N) -> c_14(N) , quot^#(N, NzM) -> c_16(u_11^#(is_NzNat(NzM), N, NzM)) , quot^#(N, NzM) -> c_17(u_21^#(is_NzNat(NzM), NzM, N)) , u_11^#(True(), N, NzM) -> c_18(u_1^#(gt(N, NzM), N, NzM)) , u_1^#(True(), N, NzM) -> c_19(quot^#(d(N, NzM), NzM)) , gcd^#(NzM, NzM) -> c_23(u_02^#(is_NzNat(NzM), NzM)) , gcd^#(NzN, NzM) -> c_24(u_31^#(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM)) , u_02^#(True(), NzM) -> c_26(NzM) , u_31^#(True(), True(), NzN, NzM) -> c_27(u_3^#(gt(NzN, NzM), NzN, NzM)) , u_3^#(True(), NzN, NzM) -> c_28(gcd^#(d(NzN, NzM), NzM)) } Strict Trs: { p(s(N)) -> N , +(N, 0()) -> N , +(s(N), s(M)) -> s(s(+(N, M))) , *(N, 0()) -> 0() , *(s(N), s(M)) -> s(+(N, +(M, *(N, M)))) , gt(NzN, 0()) -> u_4(is_NzNat(NzN)) , gt(s(N), s(M)) -> gt(N, M) , gt(0(), M) -> False() , u_4(True()) -> True() , is_NzNat(s(N)) -> True() , is_NzNat(0()) -> False() , lt(N, M) -> gt(M, N) , d(s(N), s(M)) -> d(N, M) , d(0(), N) -> N , quot(NzM, NzM) -> u_01(is_NzNat(NzM)) , quot(N, NzM) -> u_11(is_NzNat(NzM), N, NzM) , quot(N, NzM) -> u_21(is_NzNat(NzM), NzM, N) , u_11(True(), N, NzM) -> u_1(gt(N, NzM), N, NzM) , u_1(True(), N, NzM) -> s(quot(d(N, NzM), NzM)) , u_01(True()) -> s(0()) , u_21(True(), NzM, N) -> u_2(gt(NzM, N)) , u_2(True()) -> 0() , 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() , u_02(True(), NzM) -> NzM , u_31(True(), True(), NzN, NzM) -> u_3(gt(NzN, NzM), NzN, NzM) , u_3(True(), NzN, NzM) -> gcd(d(NzN, NzM), NzM) } Weak DPs: { *^#(N, 0()) -> c_4() , gt^#(NzN, 0()) -> c_6(u_4^#(is_NzNat(NzN))) , gt^#(0(), M) -> c_8() , u_4^#(True()) -> c_9() , is_NzNat^#(s(N)) -> c_10() , is_NzNat^#(0()) -> c_11() , quot^#(NzM, NzM) -> c_15(u_01^#(is_NzNat(NzM))) , u_01^#(True()) -> c_20() , u_21^#(True(), NzM, N) -> c_21(u_2^#(gt(NzM, N))) , u_2^#(True()) -> c_22() , gcd^#(0(), N) -> c_25() } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {10} by applications of Pre({10}) = {1,2,8,12,15}. Here rules are labeled as follows: DPs: { 1: p^#(s(N)) -> c_1(N) , 2: +^#(N, 0()) -> c_2(N) , 3: +^#(s(N), s(M)) -> c_3(+^#(N, M)) , 4: *^#(s(N), s(M)) -> c_5(+^#(N, +(M, *(N, M)))) , 5: gt^#(s(N), s(M)) -> c_7(gt^#(N, M)) , 6: lt^#(N, M) -> c_12(gt^#(M, N)) , 7: d^#(s(N), s(M)) -> c_13(d^#(N, M)) , 8: d^#(0(), N) -> c_14(N) , 9: quot^#(N, NzM) -> c_16(u_11^#(is_NzNat(NzM), N, NzM)) , 10: quot^#(N, NzM) -> c_17(u_21^#(is_NzNat(NzM), NzM, N)) , 11: u_11^#(True(), N, NzM) -> c_18(u_1^#(gt(N, NzM), N, NzM)) , 12: u_1^#(True(), N, NzM) -> c_19(quot^#(d(N, NzM), NzM)) , 13: gcd^#(NzM, NzM) -> c_23(u_02^#(is_NzNat(NzM), NzM)) , 14: gcd^#(NzN, NzM) -> c_24(u_31^#(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM)) , 15: u_02^#(True(), NzM) -> c_26(NzM) , 16: u_31^#(True(), True(), NzN, NzM) -> c_27(u_3^#(gt(NzN, NzM), NzN, NzM)) , 17: u_3^#(True(), NzN, NzM) -> c_28(gcd^#(d(NzN, NzM), NzM)) , 18: *^#(N, 0()) -> c_4() , 19: gt^#(NzN, 0()) -> c_6(u_4^#(is_NzNat(NzN))) , 20: gt^#(0(), M) -> c_8() , 21: u_4^#(True()) -> c_9() , 22: is_NzNat^#(s(N)) -> c_10() , 23: is_NzNat^#(0()) -> c_11() , 24: quot^#(NzM, NzM) -> c_15(u_01^#(is_NzNat(NzM))) , 25: u_01^#(True()) -> c_20() , 26: u_21^#(True(), NzM, N) -> c_21(u_2^#(gt(NzM, N))) , 27: u_2^#(True()) -> c_22() , 28: gcd^#(0(), N) -> c_25() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { p^#(s(N)) -> c_1(N) , +^#(N, 0()) -> c_2(N) , +^#(s(N), s(M)) -> c_3(+^#(N, M)) , *^#(s(N), s(M)) -> c_5(+^#(N, +(M, *(N, M)))) , gt^#(s(N), s(M)) -> c_7(gt^#(N, M)) , lt^#(N, M) -> c_12(gt^#(M, N)) , d^#(s(N), s(M)) -> c_13(d^#(N, M)) , d^#(0(), N) -> c_14(N) , quot^#(N, NzM) -> c_16(u_11^#(is_NzNat(NzM), N, NzM)) , u_11^#(True(), N, NzM) -> c_18(u_1^#(gt(N, NzM), N, NzM)) , u_1^#(True(), N, NzM) -> c_19(quot^#(d(N, NzM), NzM)) , gcd^#(NzM, NzM) -> c_23(u_02^#(is_NzNat(NzM), NzM)) , gcd^#(NzN, NzM) -> c_24(u_31^#(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM)) , u_02^#(True(), NzM) -> c_26(NzM) , u_31^#(True(), True(), NzN, NzM) -> c_27(u_3^#(gt(NzN, NzM), NzN, NzM)) , u_3^#(True(), NzN, NzM) -> c_28(gcd^#(d(NzN, NzM), NzM)) } Strict Trs: { p(s(N)) -> N , +(N, 0()) -> N , +(s(N), s(M)) -> s(s(+(N, M))) , *(N, 0()) -> 0() , *(s(N), s(M)) -> s(+(N, +(M, *(N, M)))) , gt(NzN, 0()) -> u_4(is_NzNat(NzN)) , gt(s(N), s(M)) -> gt(N, M) , gt(0(), M) -> False() , u_4(True()) -> True() , is_NzNat(s(N)) -> True() , is_NzNat(0()) -> False() , lt(N, M) -> gt(M, N) , d(s(N), s(M)) -> d(N, M) , d(0(), N) -> N , quot(NzM, NzM) -> u_01(is_NzNat(NzM)) , quot(N, NzM) -> u_11(is_NzNat(NzM), N, NzM) , quot(N, NzM) -> u_21(is_NzNat(NzM), NzM, N) , u_11(True(), N, NzM) -> u_1(gt(N, NzM), N, NzM) , u_1(True(), N, NzM) -> s(quot(d(N, NzM), NzM)) , u_01(True()) -> s(0()) , u_21(True(), NzM, N) -> u_2(gt(NzM, N)) , u_2(True()) -> 0() , 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() , u_02(True(), NzM) -> NzM , u_31(True(), True(), NzN, NzM) -> u_3(gt(NzN, NzM), NzN, NzM) , u_3(True(), NzN, NzM) -> gcd(d(NzN, NzM), NzM) } Weak DPs: { *^#(N, 0()) -> c_4() , gt^#(NzN, 0()) -> c_6(u_4^#(is_NzNat(NzN))) , gt^#(0(), M) -> c_8() , u_4^#(True()) -> c_9() , is_NzNat^#(s(N)) -> c_10() , is_NzNat^#(0()) -> c_11() , quot^#(NzM, NzM) -> c_15(u_01^#(is_NzNat(NzM))) , quot^#(N, NzM) -> c_17(u_21^#(is_NzNat(NzM), NzM, N)) , u_01^#(True()) -> c_20() , u_21^#(True(), NzM, N) -> c_21(u_2^#(gt(NzM, N))) , u_2^#(True()) -> c_22() , gcd^#(0(), N) -> c_25() } Obligation: runtime complexity Answer: MAYBE Empty strict component of the problem is NOT empty. Arrrr..