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