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: innermost runtime complexity Answer: MAYBE We add following dependency tuples: Strict DPs: { p^#(s(N)) -> c_1() , +^#(N, 0()) -> c_2() , +^#(s(N), s(M)) -> c_3(+^#(N, M)) , *^#(N, 0()) -> c_4() , *^#(s(N), s(M)) -> c_5(+^#(N, +(M, *(N, M))), +^#(M, *(N, M)), *^#(N, M)) , gt^#(NzN, 0()) -> c_6(u_4^#(is_NzNat(NzN)), 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() , quot^#(NzM, NzM) -> c_15(u_01^#(is_NzNat(NzM)), is_NzNat^#(NzM)) , quot^#(N, NzM) -> c_16(u_11^#(is_NzNat(NzM), N, NzM), is_NzNat^#(NzM)) , quot^#(N, NzM) -> c_17(u_21^#(is_NzNat(NzM), NzM, N), is_NzNat^#(NzM)) , u_01^#(True()) -> c_20() , u_11^#(True(), N, NzM) -> c_18(u_1^#(gt(N, NzM), N, NzM), gt^#(N, NzM)) , u_21^#(True(), NzM, N) -> c_21(u_2^#(gt(NzM, N)), gt^#(NzM, N)) , u_1^#(True(), N, NzM) -> c_19(quot^#(d(N, NzM), NzM), d^#(N, NzM)) , u_2^#(True()) -> c_22() , gcd^#(NzM, NzM) -> c_23(u_02^#(is_NzNat(NzM), NzM), is_NzNat^#(NzM)) , gcd^#(NzN, NzM) -> c_24(u_31^#(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM), is_NzNat^#(NzN), is_NzNat^#(NzM)) , gcd^#(0(), N) -> c_25() , u_02^#(True(), NzM) -> c_26() , u_31^#(True(), True(), NzN, NzM) -> c_27(u_3^#(gt(NzN, NzM), NzN, NzM), gt^#(NzN, NzM)) , u_3^#(True(), NzN, NzM) -> c_28(gcd^#(d(NzN, NzM), NzM), d^#(NzN, 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, 0()) -> c_2() , +^#(s(N), s(M)) -> c_3(+^#(N, M)) , *^#(N, 0()) -> c_4() , *^#(s(N), s(M)) -> c_5(+^#(N, +(M, *(N, M))), +^#(M, *(N, M)), *^#(N, M)) , gt^#(NzN, 0()) -> c_6(u_4^#(is_NzNat(NzN)), 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() , quot^#(NzM, NzM) -> c_15(u_01^#(is_NzNat(NzM)), is_NzNat^#(NzM)) , quot^#(N, NzM) -> c_16(u_11^#(is_NzNat(NzM), N, NzM), is_NzNat^#(NzM)) , quot^#(N, NzM) -> c_17(u_21^#(is_NzNat(NzM), NzM, N), is_NzNat^#(NzM)) , u_01^#(True()) -> c_20() , u_11^#(True(), N, NzM) -> c_18(u_1^#(gt(N, NzM), N, NzM), gt^#(N, NzM)) , u_21^#(True(), NzM, N) -> c_21(u_2^#(gt(NzM, N)), gt^#(NzM, N)) , u_1^#(True(), N, NzM) -> c_19(quot^#(d(N, NzM), NzM), d^#(N, NzM)) , u_2^#(True()) -> c_22() , gcd^#(NzM, NzM) -> c_23(u_02^#(is_NzNat(NzM), NzM), is_NzNat^#(NzM)) , gcd^#(NzN, NzM) -> c_24(u_31^#(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM), is_NzNat^#(NzN), is_NzNat^#(NzM)) , gcd^#(0(), N) -> c_25() , u_02^#(True(), NzM) -> c_26() , u_31^#(True(), True(), NzN, NzM) -> c_27(u_3^#(gt(NzN, NzM), NzN, NzM), gt^#(NzN, NzM)) , u_3^#(True(), NzN, NzM) -> c_28(gcd^#(d(NzN, NzM), NzM), d^#(NzN, NzM)) } Weak 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: innermost runtime complexity Answer: MAYBE We estimate the number of application of {1,2,4,8,9,10,11,14,18,22,25,26} by applications of Pre({1,2,4,8,9,10,11,14,18,22,25,26}) = {3,5,6,7,12,13,15,16,17,19,20,21,23,24,27,28}. Here rules are labeled as follows: DPs: { 1: p^#(s(N)) -> c_1() , 2: +^#(N, 0()) -> c_2() , 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))), +^#(M, *(N, M)), *^#(N, M)) , 6: gt^#(NzN, 0()) -> c_6(u_4^#(is_NzNat(NzN)), 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() , 15: quot^#(NzM, NzM) -> c_15(u_01^#(is_NzNat(NzM)), is_NzNat^#(NzM)) , 16: quot^#(N, NzM) -> c_16(u_11^#(is_NzNat(NzM), N, NzM), is_NzNat^#(NzM)) , 17: quot^#(N, NzM) -> c_17(u_21^#(is_NzNat(NzM), NzM, N), is_NzNat^#(NzM)) , 18: u_01^#(True()) -> c_20() , 19: u_11^#(True(), N, NzM) -> c_18(u_1^#(gt(N, NzM), N, NzM), gt^#(N, NzM)) , 20: u_21^#(True(), NzM, N) -> c_21(u_2^#(gt(NzM, N)), gt^#(NzM, N)) , 21: u_1^#(True(), N, NzM) -> c_19(quot^#(d(N, NzM), NzM), d^#(N, NzM)) , 22: u_2^#(True()) -> c_22() , 23: gcd^#(NzM, NzM) -> c_23(u_02^#(is_NzNat(NzM), NzM), is_NzNat^#(NzM)) , 24: gcd^#(NzN, NzM) -> c_24(u_31^#(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM), is_NzNat^#(NzN), is_NzNat^#(NzM)) , 25: gcd^#(0(), N) -> c_25() , 26: u_02^#(True(), NzM) -> c_26() , 27: u_31^#(True(), True(), NzN, NzM) -> c_27(u_3^#(gt(NzN, NzM), NzN, NzM), gt^#(NzN, NzM)) , 28: u_3^#(True(), NzN, NzM) -> c_28(gcd^#(d(NzN, NzM), NzM), d^#(NzN, NzM)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { +^#(s(N), s(M)) -> c_3(+^#(N, M)) , *^#(s(N), s(M)) -> c_5(+^#(N, +(M, *(N, M))), +^#(M, *(N, M)), *^#(N, M)) , gt^#(NzN, 0()) -> c_6(u_4^#(is_NzNat(NzN)), 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)) , quot^#(NzM, NzM) -> c_15(u_01^#(is_NzNat(NzM)), is_NzNat^#(NzM)) , quot^#(N, NzM) -> c_16(u_11^#(is_NzNat(NzM), N, NzM), is_NzNat^#(NzM)) , quot^#(N, NzM) -> c_17(u_21^#(is_NzNat(NzM), NzM, N), is_NzNat^#(NzM)) , u_11^#(True(), N, NzM) -> c_18(u_1^#(gt(N, NzM), N, NzM), gt^#(N, NzM)) , u_21^#(True(), NzM, N) -> c_21(u_2^#(gt(NzM, N)), gt^#(NzM, N)) , u_1^#(True(), N, NzM) -> c_19(quot^#(d(N, NzM), NzM), d^#(N, NzM)) , gcd^#(NzM, NzM) -> c_23(u_02^#(is_NzNat(NzM), NzM), is_NzNat^#(NzM)) , gcd^#(NzN, NzM) -> c_24(u_31^#(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM), is_NzNat^#(NzN), is_NzNat^#(NzM)) , u_31^#(True(), True(), NzN, NzM) -> c_27(u_3^#(gt(NzN, NzM), NzN, NzM), gt^#(NzN, NzM)) , u_3^#(True(), NzN, NzM) -> c_28(gcd^#(d(NzN, NzM), NzM), d^#(NzN, NzM)) } Weak DPs: { p^#(s(N)) -> c_1() , +^#(N, 0()) -> c_2() , *^#(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() , d^#(0(), N) -> c_14() , u_01^#(True()) -> c_20() , u_2^#(True()) -> c_22() , gcd^#(0(), N) -> c_25() , u_02^#(True(), NzM) -> c_26() } Weak 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: innermost runtime complexity Answer: MAYBE We estimate the number of application of {3,7,13} by applications of Pre({3,7,13}) = {4,5,10,11,12,15,16}. Here rules are labeled as follows: DPs: { 1: +^#(s(N), s(M)) -> c_3(+^#(N, M)) , 2: *^#(s(N), s(M)) -> c_5(+^#(N, +(M, *(N, M))), +^#(M, *(N, M)), *^#(N, M)) , 3: gt^#(NzN, 0()) -> c_6(u_4^#(is_NzNat(NzN)), is_NzNat^#(NzN)) , 4: gt^#(s(N), s(M)) -> c_7(gt^#(N, M)) , 5: lt^#(N, M) -> c_12(gt^#(M, N)) , 6: d^#(s(N), s(M)) -> c_13(d^#(N, M)) , 7: quot^#(NzM, NzM) -> c_15(u_01^#(is_NzNat(NzM)), is_NzNat^#(NzM)) , 8: quot^#(N, NzM) -> c_16(u_11^#(is_NzNat(NzM), N, NzM), is_NzNat^#(NzM)) , 9: quot^#(N, NzM) -> c_17(u_21^#(is_NzNat(NzM), NzM, N), is_NzNat^#(NzM)) , 10: u_11^#(True(), N, NzM) -> c_18(u_1^#(gt(N, NzM), N, NzM), gt^#(N, NzM)) , 11: u_21^#(True(), NzM, N) -> c_21(u_2^#(gt(NzM, N)), gt^#(NzM, N)) , 12: u_1^#(True(), N, NzM) -> c_19(quot^#(d(N, NzM), NzM), d^#(N, NzM)) , 13: gcd^#(NzM, NzM) -> c_23(u_02^#(is_NzNat(NzM), NzM), is_NzNat^#(NzM)) , 14: gcd^#(NzN, NzM) -> c_24(u_31^#(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM), is_NzNat^#(NzN), is_NzNat^#(NzM)) , 15: u_31^#(True(), True(), NzN, NzM) -> c_27(u_3^#(gt(NzN, NzM), NzN, NzM), gt^#(NzN, NzM)) , 16: u_3^#(True(), NzN, NzM) -> c_28(gcd^#(d(NzN, NzM), NzM), d^#(NzN, NzM)) , 17: p^#(s(N)) -> c_1() , 18: +^#(N, 0()) -> c_2() , 19: *^#(N, 0()) -> c_4() , 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: d^#(0(), N) -> c_14() , 25: u_01^#(True()) -> c_20() , 26: u_2^#(True()) -> c_22() , 27: gcd^#(0(), N) -> c_25() , 28: u_02^#(True(), NzM) -> c_26() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { +^#(s(N), s(M)) -> c_3(+^#(N, M)) , *^#(s(N), s(M)) -> c_5(+^#(N, +(M, *(N, M))), +^#(M, *(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)) , quot^#(N, NzM) -> c_16(u_11^#(is_NzNat(NzM), N, NzM), is_NzNat^#(NzM)) , quot^#(N, NzM) -> c_17(u_21^#(is_NzNat(NzM), NzM, N), is_NzNat^#(NzM)) , u_11^#(True(), N, NzM) -> c_18(u_1^#(gt(N, NzM), N, NzM), gt^#(N, NzM)) , u_21^#(True(), NzM, N) -> c_21(u_2^#(gt(NzM, N)), gt^#(NzM, N)) , u_1^#(True(), N, NzM) -> c_19(quot^#(d(N, NzM), NzM), d^#(N, NzM)) , gcd^#(NzN, NzM) -> c_24(u_31^#(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM), is_NzNat^#(NzN), is_NzNat^#(NzM)) , u_31^#(True(), True(), NzN, NzM) -> c_27(u_3^#(gt(NzN, NzM), NzN, NzM), gt^#(NzN, NzM)) , u_3^#(True(), NzN, NzM) -> c_28(gcd^#(d(NzN, NzM), NzM), d^#(NzN, NzM)) } Weak DPs: { p^#(s(N)) -> c_1() , +^#(N, 0()) -> c_2() , *^#(N, 0()) -> c_4() , gt^#(NzN, 0()) -> c_6(u_4^#(is_NzNat(NzN)), is_NzNat^#(NzN)) , gt^#(0(), M) -> c_8() , u_4^#(True()) -> c_9() , is_NzNat^#(s(N)) -> c_10() , is_NzNat^#(0()) -> c_11() , d^#(0(), N) -> c_14() , quot^#(NzM, NzM) -> c_15(u_01^#(is_NzNat(NzM)), is_NzNat^#(NzM)) , u_01^#(True()) -> c_20() , u_2^#(True()) -> c_22() , gcd^#(NzM, NzM) -> c_23(u_02^#(is_NzNat(NzM), NzM), is_NzNat^#(NzM)) , gcd^#(0(), N) -> c_25() , u_02^#(True(), NzM) -> c_26() } Weak 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: innermost runtime complexity Answer: MAYBE The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { p^#(s(N)) -> c_1() , +^#(N, 0()) -> c_2() , *^#(N, 0()) -> c_4() , gt^#(NzN, 0()) -> c_6(u_4^#(is_NzNat(NzN)), is_NzNat^#(NzN)) , gt^#(0(), M) -> c_8() , u_4^#(True()) -> c_9() , is_NzNat^#(s(N)) -> c_10() , is_NzNat^#(0()) -> c_11() , d^#(0(), N) -> c_14() , quot^#(NzM, NzM) -> c_15(u_01^#(is_NzNat(NzM)), is_NzNat^#(NzM)) , u_01^#(True()) -> c_20() , u_2^#(True()) -> c_22() , gcd^#(NzM, NzM) -> c_23(u_02^#(is_NzNat(NzM), NzM), is_NzNat^#(NzM)) , gcd^#(0(), N) -> c_25() , u_02^#(True(), NzM) -> c_26() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { +^#(s(N), s(M)) -> c_3(+^#(N, M)) , *^#(s(N), s(M)) -> c_5(+^#(N, +(M, *(N, M))), +^#(M, *(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)) , quot^#(N, NzM) -> c_16(u_11^#(is_NzNat(NzM), N, NzM), is_NzNat^#(NzM)) , quot^#(N, NzM) -> c_17(u_21^#(is_NzNat(NzM), NzM, N), is_NzNat^#(NzM)) , u_11^#(True(), N, NzM) -> c_18(u_1^#(gt(N, NzM), N, NzM), gt^#(N, NzM)) , u_21^#(True(), NzM, N) -> c_21(u_2^#(gt(NzM, N)), gt^#(NzM, N)) , u_1^#(True(), N, NzM) -> c_19(quot^#(d(N, NzM), NzM), d^#(N, NzM)) , gcd^#(NzN, NzM) -> c_24(u_31^#(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM), is_NzNat^#(NzN), is_NzNat^#(NzM)) , u_31^#(True(), True(), NzN, NzM) -> c_27(u_3^#(gt(NzN, NzM), NzN, NzM), gt^#(NzN, NzM)) , u_3^#(True(), NzN, NzM) -> c_28(gcd^#(d(NzN, NzM), NzM), d^#(NzN, NzM)) } Weak 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: innermost runtime complexity Answer: MAYBE Due to missing edges in the dependency-graph, the right-hand sides of following rules could be simplified: { quot^#(N, NzM) -> c_16(u_11^#(is_NzNat(NzM), N, NzM), is_NzNat^#(NzM)) , quot^#(N, NzM) -> c_17(u_21^#(is_NzNat(NzM), NzM, N), is_NzNat^#(NzM)) , u_21^#(True(), NzM, N) -> c_21(u_2^#(gt(NzM, N)), gt^#(NzM, N)) , gcd^#(NzN, NzM) -> c_24(u_31^#(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM), is_NzNat^#(NzN), is_NzNat^#(NzM)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { +^#(s(N), s(M)) -> c_1(+^#(N, M)) , *^#(s(N), s(M)) -> c_2(+^#(N, +(M, *(N, M))), +^#(M, *(N, M)), *^#(N, M)) , gt^#(s(N), s(M)) -> c_3(gt^#(N, M)) , lt^#(N, M) -> c_4(gt^#(M, N)) , d^#(s(N), s(M)) -> c_5(d^#(N, M)) , quot^#(N, NzM) -> c_6(u_11^#(is_NzNat(NzM), N, NzM)) , quot^#(N, NzM) -> c_7(u_21^#(is_NzNat(NzM), NzM, N)) , u_11^#(True(), N, NzM) -> c_8(u_1^#(gt(N, NzM), N, NzM), gt^#(N, NzM)) , u_21^#(True(), NzM, N) -> c_9(gt^#(NzM, N)) , u_1^#(True(), N, NzM) -> c_10(quot^#(d(N, NzM), NzM), d^#(N, NzM)) , gcd^#(NzN, NzM) -> c_11(u_31^#(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM)) , u_31^#(True(), True(), NzN, NzM) -> c_12(u_3^#(gt(NzN, NzM), NzN, NzM), gt^#(NzN, NzM)) , u_3^#(True(), NzN, NzM) -> c_13(gcd^#(d(NzN, NzM), NzM), d^#(NzN, NzM)) } Weak 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: innermost runtime complexity Answer: MAYBE We replace rewrite rules by usable rules: Weak Usable Rules: { +(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() , d(s(N), s(M)) -> d(N, M) , d(0(), N) -> N } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { +^#(s(N), s(M)) -> c_1(+^#(N, M)) , *^#(s(N), s(M)) -> c_2(+^#(N, +(M, *(N, M))), +^#(M, *(N, M)), *^#(N, M)) , gt^#(s(N), s(M)) -> c_3(gt^#(N, M)) , lt^#(N, M) -> c_4(gt^#(M, N)) , d^#(s(N), s(M)) -> c_5(d^#(N, M)) , quot^#(N, NzM) -> c_6(u_11^#(is_NzNat(NzM), N, NzM)) , quot^#(N, NzM) -> c_7(u_21^#(is_NzNat(NzM), NzM, N)) , u_11^#(True(), N, NzM) -> c_8(u_1^#(gt(N, NzM), N, NzM), gt^#(N, NzM)) , u_21^#(True(), NzM, N) -> c_9(gt^#(NzM, N)) , u_1^#(True(), N, NzM) -> c_10(quot^#(d(N, NzM), NzM), d^#(N, NzM)) , gcd^#(NzN, NzM) -> c_11(u_31^#(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM)) , u_31^#(True(), True(), NzN, NzM) -> c_12(u_3^#(gt(NzN, NzM), NzN, NzM), gt^#(NzN, NzM)) , u_3^#(True(), NzN, NzM) -> c_13(gcd^#(d(NzN, NzM), NzM), d^#(NzN, NzM)) } Weak Trs: { +(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() , d(s(N), s(M)) -> d(N, M) , d(0(), N) -> N } Obligation: innermost runtime complexity Answer: MAYBE Consider the dependency graph 1: +^#(s(N), s(M)) -> c_1(+^#(N, M)) -->_1 +^#(s(N), s(M)) -> c_1(+^#(N, M)) :1 2: *^#(s(N), s(M)) -> c_2(+^#(N, +(M, *(N, M))), +^#(M, *(N, M)), *^#(N, M)) -->_3 *^#(s(N), s(M)) -> c_2(+^#(N, +(M, *(N, M))), +^#(M, *(N, M)), *^#(N, M)) :2 -->_2 +^#(s(N), s(M)) -> c_1(+^#(N, M)) :1 -->_1 +^#(s(N), s(M)) -> c_1(+^#(N, M)) :1 3: gt^#(s(N), s(M)) -> c_3(gt^#(N, M)) -->_1 gt^#(s(N), s(M)) -> c_3(gt^#(N, M)) :3 4: lt^#(N, M) -> c_4(gt^#(M, N)) -->_1 gt^#(s(N), s(M)) -> c_3(gt^#(N, M)) :3 5: d^#(s(N), s(M)) -> c_5(d^#(N, M)) -->_1 d^#(s(N), s(M)) -> c_5(d^#(N, M)) :5 6: quot^#(N, NzM) -> c_6(u_11^#(is_NzNat(NzM), N, NzM)) -->_1 u_11^#(True(), N, NzM) -> c_8(u_1^#(gt(N, NzM), N, NzM), gt^#(N, NzM)) :8 7: quot^#(N, NzM) -> c_7(u_21^#(is_NzNat(NzM), NzM, N)) -->_1 u_21^#(True(), NzM, N) -> c_9(gt^#(NzM, N)) :9 8: u_11^#(True(), N, NzM) -> c_8(u_1^#(gt(N, NzM), N, NzM), gt^#(N, NzM)) -->_1 u_1^#(True(), N, NzM) -> c_10(quot^#(d(N, NzM), NzM), d^#(N, NzM)) :10 -->_2 gt^#(s(N), s(M)) -> c_3(gt^#(N, M)) :3 9: u_21^#(True(), NzM, N) -> c_9(gt^#(NzM, N)) -->_1 gt^#(s(N), s(M)) -> c_3(gt^#(N, M)) :3 10: u_1^#(True(), N, NzM) -> c_10(quot^#(d(N, NzM), NzM), d^#(N, NzM)) -->_1 quot^#(N, NzM) -> c_7(u_21^#(is_NzNat(NzM), NzM, N)) :7 -->_1 quot^#(N, NzM) -> c_6(u_11^#(is_NzNat(NzM), N, NzM)) :6 -->_2 d^#(s(N), s(M)) -> c_5(d^#(N, M)) :5 11: gcd^#(NzN, NzM) -> c_11(u_31^#(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM)) -->_1 u_31^#(True(), True(), NzN, NzM) -> c_12(u_3^#(gt(NzN, NzM), NzN, NzM), gt^#(NzN, NzM)) :12 12: u_31^#(True(), True(), NzN, NzM) -> c_12(u_3^#(gt(NzN, NzM), NzN, NzM), gt^#(NzN, NzM)) -->_1 u_3^#(True(), NzN, NzM) -> c_13(gcd^#(d(NzN, NzM), NzM), d^#(NzN, NzM)) :13 -->_2 gt^#(s(N), s(M)) -> c_3(gt^#(N, M)) :3 13: u_3^#(True(), NzN, NzM) -> c_13(gcd^#(d(NzN, NzM), NzM), d^#(NzN, NzM)) -->_1 gcd^#(NzN, NzM) -> c_11(u_31^#(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM)) :11 -->_2 d^#(s(N), s(M)) -> c_5(d^#(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). { lt^#(N, M) -> c_4(gt^#(M, N)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { +^#(s(N), s(M)) -> c_1(+^#(N, M)) , *^#(s(N), s(M)) -> c_2(+^#(N, +(M, *(N, M))), +^#(M, *(N, M)), *^#(N, M)) , gt^#(s(N), s(M)) -> c_3(gt^#(N, M)) , d^#(s(N), s(M)) -> c_5(d^#(N, M)) , quot^#(N, NzM) -> c_6(u_11^#(is_NzNat(NzM), N, NzM)) , quot^#(N, NzM) -> c_7(u_21^#(is_NzNat(NzM), NzM, N)) , u_11^#(True(), N, NzM) -> c_8(u_1^#(gt(N, NzM), N, NzM), gt^#(N, NzM)) , u_21^#(True(), NzM, N) -> c_9(gt^#(NzM, N)) , u_1^#(True(), N, NzM) -> c_10(quot^#(d(N, NzM), NzM), d^#(N, NzM)) , gcd^#(NzN, NzM) -> c_11(u_31^#(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM)) , u_31^#(True(), True(), NzN, NzM) -> c_12(u_3^#(gt(NzN, NzM), NzN, NzM), gt^#(NzN, NzM)) , u_3^#(True(), NzN, NzM) -> c_13(gcd^#(d(NzN, NzM), NzM), d^#(NzN, NzM)) } Weak Trs: { +(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() , d(s(N), s(M)) -> d(N, M) , d(0(), N) -> N } Obligation: innermost runtime complexity Answer: MAYBE The input cannot be shown compatible Arrrr..