MAYBE 982.99/297.05 MAYBE 982.99/297.05 982.99/297.05 We are left with following problem, upon which TcT provides the 982.99/297.05 certificate MAYBE. 982.99/297.05 982.99/297.05 Strict Trs: 982.99/297.05 { active(U11(X1, X2)) -> U11(active(X1), X2) 982.99/297.05 , active(U11(tt(), V2)) -> mark(U12(isNat(V2))) 982.99/297.05 , active(U12(X)) -> U12(active(X)) 982.99/297.05 , active(U12(tt())) -> mark(tt()) 982.99/297.05 , active(isNat(s(V1))) -> mark(U21(isNat(V1))) 982.99/297.05 , active(isNat(plus(V1, V2))) -> mark(U11(isNat(V1), V2)) 982.99/297.05 , active(isNat(0())) -> mark(tt()) 982.99/297.05 , active(U21(X)) -> U21(active(X)) 982.99/297.05 , active(U21(tt())) -> mark(tt()) 982.99/297.05 , active(U31(X1, X2)) -> U31(active(X1), X2) 982.99/297.05 , active(U31(tt(), N)) -> mark(N) 982.99/297.05 , active(U41(X1, X2, X3)) -> U41(active(X1), X2, X3) 982.99/297.05 , active(U41(tt(), M, N)) -> mark(U42(isNat(N), M, N)) 982.99/297.05 , active(U42(X1, X2, X3)) -> U42(active(X1), X2, X3) 982.99/297.05 , active(U42(tt(), M, N)) -> mark(s(plus(N, M))) 982.99/297.05 , active(s(X)) -> s(active(X)) 982.99/297.05 , active(plus(X1, X2)) -> plus(X1, active(X2)) 982.99/297.05 , active(plus(X1, X2)) -> plus(active(X1), X2) 982.99/297.05 , active(plus(N, s(M))) -> mark(U41(isNat(M), M, N)) 982.99/297.05 , active(plus(N, 0())) -> mark(U31(isNat(N), N)) 982.99/297.05 , U11(mark(X1), X2) -> mark(U11(X1, X2)) 982.99/297.05 , U11(ok(X1), ok(X2)) -> ok(U11(X1, X2)) 982.99/297.05 , U12(mark(X)) -> mark(U12(X)) 982.99/297.05 , U12(ok(X)) -> ok(U12(X)) 982.99/297.05 , isNat(ok(X)) -> ok(isNat(X)) 982.99/297.05 , U21(mark(X)) -> mark(U21(X)) 982.99/297.05 , U21(ok(X)) -> ok(U21(X)) 982.99/297.05 , U31(mark(X1), X2) -> mark(U31(X1, X2)) 982.99/297.05 , U31(ok(X1), ok(X2)) -> ok(U31(X1, X2)) 982.99/297.05 , U41(mark(X1), X2, X3) -> mark(U41(X1, X2, X3)) 982.99/297.05 , U41(ok(X1), ok(X2), ok(X3)) -> ok(U41(X1, X2, X3)) 982.99/297.05 , U42(mark(X1), X2, X3) -> mark(U42(X1, X2, X3)) 982.99/297.05 , U42(ok(X1), ok(X2), ok(X3)) -> ok(U42(X1, X2, X3)) 982.99/297.05 , s(mark(X)) -> mark(s(X)) 982.99/297.05 , s(ok(X)) -> ok(s(X)) 982.99/297.05 , plus(X1, mark(X2)) -> mark(plus(X1, X2)) 982.99/297.05 , plus(mark(X1), X2) -> mark(plus(X1, X2)) 982.99/297.05 , plus(ok(X1), ok(X2)) -> ok(plus(X1, X2)) 982.99/297.05 , proper(U11(X1, X2)) -> U11(proper(X1), proper(X2)) 982.99/297.05 , proper(tt()) -> ok(tt()) 982.99/297.05 , proper(U12(X)) -> U12(proper(X)) 982.99/297.05 , proper(isNat(X)) -> isNat(proper(X)) 982.99/297.05 , proper(U21(X)) -> U21(proper(X)) 982.99/297.05 , proper(U31(X1, X2)) -> U31(proper(X1), proper(X2)) 982.99/297.05 , proper(U41(X1, X2, X3)) -> 982.99/297.05 U41(proper(X1), proper(X2), proper(X3)) 982.99/297.05 , proper(U42(X1, X2, X3)) -> 982.99/297.05 U42(proper(X1), proper(X2), proper(X3)) 982.99/297.05 , proper(s(X)) -> s(proper(X)) 982.99/297.05 , proper(plus(X1, X2)) -> plus(proper(X1), proper(X2)) 982.99/297.05 , proper(0()) -> ok(0()) 982.99/297.05 , top(mark(X)) -> top(proper(X)) 982.99/297.05 , top(ok(X)) -> top(active(X)) } 982.99/297.05 Obligation: 982.99/297.05 runtime complexity 982.99/297.05 Answer: 982.99/297.05 MAYBE 982.99/297.05 982.99/297.05 None of the processors succeeded. 982.99/297.05 982.99/297.05 Details of failed attempt(s): 982.99/297.05 ----------------------------- 982.99/297.05 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 982.99/297.05 following reason: 982.99/297.05 982.99/297.05 Computation stopped due to timeout after 297.0 seconds. 982.99/297.05 982.99/297.05 2) 'Best' failed due to the following reason: 982.99/297.05 982.99/297.05 None of the processors succeeded. 982.99/297.05 982.99/297.05 Details of failed attempt(s): 982.99/297.05 ----------------------------- 982.99/297.05 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 982.99/297.05 seconds)' failed due to the following reason: 982.99/297.05 982.99/297.05 Computation stopped due to timeout after 148.0 seconds. 982.99/297.05 982.99/297.05 2) 'Best' failed due to the following reason: 982.99/297.05 982.99/297.05 None of the processors succeeded. 982.99/297.05 982.99/297.05 Details of failed attempt(s): 982.99/297.05 ----------------------------- 982.99/297.05 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 982.99/297.05 following reason: 982.99/297.05 982.99/297.05 The processor is inapplicable, reason: 982.99/297.05 Processor only applicable for innermost runtime complexity analysis 982.99/297.05 982.99/297.05 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 982.99/297.05 to the following reason: 982.99/297.05 982.99/297.05 The processor is inapplicable, reason: 982.99/297.05 Processor only applicable for innermost runtime complexity analysis 982.99/297.05 982.99/297.05 982.99/297.05 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 982.99/297.05 failed due to the following reason: 982.99/297.05 982.99/297.05 None of the processors succeeded. 982.99/297.05 982.99/297.05 Details of failed attempt(s): 982.99/297.05 ----------------------------- 982.99/297.05 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 982.99/297.05 failed due to the following reason: 982.99/297.05 982.99/297.05 match-boundness of the problem could not be verified. 982.99/297.05 982.99/297.05 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 982.99/297.05 failed due to the following reason: 982.99/297.05 982.99/297.05 match-boundness of the problem could not be verified. 982.99/297.05 982.99/297.05 982.99/297.05 982.99/297.05 3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 982.99/297.05 the following reason: 982.99/297.05 982.99/297.05 We add the following weak dependency pairs: 982.99/297.05 982.99/297.05 Strict DPs: 982.99/297.05 { active^#(U11(X1, X2)) -> c_1(U11^#(active(X1), X2)) 982.99/297.05 , active^#(U11(tt(), V2)) -> c_2(U12^#(isNat(V2))) 982.99/297.05 , active^#(U12(X)) -> c_3(U12^#(active(X))) 982.99/297.05 , active^#(U12(tt())) -> c_4() 982.99/297.05 , active^#(isNat(s(V1))) -> c_5(U21^#(isNat(V1))) 982.99/297.05 , active^#(isNat(plus(V1, V2))) -> c_6(U11^#(isNat(V1), V2)) 982.99/297.05 , active^#(isNat(0())) -> c_7() 982.99/297.05 , active^#(U21(X)) -> c_8(U21^#(active(X))) 982.99/297.05 , active^#(U21(tt())) -> c_9() 982.99/297.05 , active^#(U31(X1, X2)) -> c_10(U31^#(active(X1), X2)) 982.99/297.05 , active^#(U31(tt(), N)) -> c_11(N) 982.99/297.05 , active^#(U41(X1, X2, X3)) -> c_12(U41^#(active(X1), X2, X3)) 982.99/297.05 , active^#(U41(tt(), M, N)) -> c_13(U42^#(isNat(N), M, N)) 982.99/297.05 , active^#(U42(X1, X2, X3)) -> c_14(U42^#(active(X1), X2, X3)) 982.99/297.05 , active^#(U42(tt(), M, N)) -> c_15(s^#(plus(N, M))) 982.99/297.05 , active^#(s(X)) -> c_16(s^#(active(X))) 982.99/297.05 , active^#(plus(X1, X2)) -> c_17(plus^#(X1, active(X2))) 982.99/297.05 , active^#(plus(X1, X2)) -> c_18(plus^#(active(X1), X2)) 982.99/297.05 , active^#(plus(N, s(M))) -> c_19(U41^#(isNat(M), M, N)) 982.99/297.05 , active^#(plus(N, 0())) -> c_20(U31^#(isNat(N), N)) 982.99/297.05 , U11^#(mark(X1), X2) -> c_21(U11^#(X1, X2)) 982.99/297.05 , U11^#(ok(X1), ok(X2)) -> c_22(U11^#(X1, X2)) 982.99/297.05 , U12^#(mark(X)) -> c_23(U12^#(X)) 982.99/297.05 , U12^#(ok(X)) -> c_24(U12^#(X)) 982.99/297.05 , U21^#(mark(X)) -> c_26(U21^#(X)) 982.99/297.05 , U21^#(ok(X)) -> c_27(U21^#(X)) 982.99/297.05 , U31^#(mark(X1), X2) -> c_28(U31^#(X1, X2)) 982.99/297.05 , U31^#(ok(X1), ok(X2)) -> c_29(U31^#(X1, X2)) 982.99/297.05 , U41^#(mark(X1), X2, X3) -> c_30(U41^#(X1, X2, X3)) 982.99/297.05 , U41^#(ok(X1), ok(X2), ok(X3)) -> c_31(U41^#(X1, X2, X3)) 982.99/297.05 , U42^#(mark(X1), X2, X3) -> c_32(U42^#(X1, X2, X3)) 982.99/297.05 , U42^#(ok(X1), ok(X2), ok(X3)) -> c_33(U42^#(X1, X2, X3)) 982.99/297.05 , s^#(mark(X)) -> c_34(s^#(X)) 982.99/297.05 , s^#(ok(X)) -> c_35(s^#(X)) 982.99/297.05 , plus^#(X1, mark(X2)) -> c_36(plus^#(X1, X2)) 982.99/297.05 , plus^#(mark(X1), X2) -> c_37(plus^#(X1, X2)) 982.99/297.05 , plus^#(ok(X1), ok(X2)) -> c_38(plus^#(X1, X2)) 982.99/297.05 , isNat^#(ok(X)) -> c_25(isNat^#(X)) 982.99/297.05 , proper^#(U11(X1, X2)) -> c_39(U11^#(proper(X1), proper(X2))) 982.99/297.05 , proper^#(tt()) -> c_40() 982.99/297.05 , proper^#(U12(X)) -> c_41(U12^#(proper(X))) 982.99/297.05 , proper^#(isNat(X)) -> c_42(isNat^#(proper(X))) 982.99/297.05 , proper^#(U21(X)) -> c_43(U21^#(proper(X))) 982.99/297.05 , proper^#(U31(X1, X2)) -> c_44(U31^#(proper(X1), proper(X2))) 982.99/297.05 , proper^#(U41(X1, X2, X3)) -> 982.99/297.05 c_45(U41^#(proper(X1), proper(X2), proper(X3))) 982.99/297.05 , proper^#(U42(X1, X2, X3)) -> 982.99/297.05 c_46(U42^#(proper(X1), proper(X2), proper(X3))) 982.99/297.05 , proper^#(s(X)) -> c_47(s^#(proper(X))) 982.99/297.05 , proper^#(plus(X1, X2)) -> c_48(plus^#(proper(X1), proper(X2))) 982.99/297.05 , proper^#(0()) -> c_49() 982.99/297.05 , top^#(mark(X)) -> c_50(top^#(proper(X))) 982.99/297.05 , top^#(ok(X)) -> c_51(top^#(active(X))) } 982.99/297.05 982.99/297.05 and mark the set of starting terms. 982.99/297.05 982.99/297.05 We are left with following problem, upon which TcT provides the 982.99/297.05 certificate MAYBE. 982.99/297.05 982.99/297.05 Strict DPs: 982.99/297.05 { active^#(U11(X1, X2)) -> c_1(U11^#(active(X1), X2)) 982.99/297.05 , active^#(U11(tt(), V2)) -> c_2(U12^#(isNat(V2))) 982.99/297.05 , active^#(U12(X)) -> c_3(U12^#(active(X))) 982.99/297.05 , active^#(U12(tt())) -> c_4() 982.99/297.05 , active^#(isNat(s(V1))) -> c_5(U21^#(isNat(V1))) 982.99/297.05 , active^#(isNat(plus(V1, V2))) -> c_6(U11^#(isNat(V1), V2)) 982.99/297.05 , active^#(isNat(0())) -> c_7() 982.99/297.05 , active^#(U21(X)) -> c_8(U21^#(active(X))) 982.99/297.05 , active^#(U21(tt())) -> c_9() 982.99/297.05 , active^#(U31(X1, X2)) -> c_10(U31^#(active(X1), X2)) 982.99/297.05 , active^#(U31(tt(), N)) -> c_11(N) 982.99/297.05 , active^#(U41(X1, X2, X3)) -> c_12(U41^#(active(X1), X2, X3)) 982.99/297.05 , active^#(U41(tt(), M, N)) -> c_13(U42^#(isNat(N), M, N)) 982.99/297.05 , active^#(U42(X1, X2, X3)) -> c_14(U42^#(active(X1), X2, X3)) 982.99/297.05 , active^#(U42(tt(), M, N)) -> c_15(s^#(plus(N, M))) 982.99/297.06 , active^#(s(X)) -> c_16(s^#(active(X))) 982.99/297.06 , active^#(plus(X1, X2)) -> c_17(plus^#(X1, active(X2))) 982.99/297.06 , active^#(plus(X1, X2)) -> c_18(plus^#(active(X1), X2)) 982.99/297.06 , active^#(plus(N, s(M))) -> c_19(U41^#(isNat(M), M, N)) 982.99/297.06 , active^#(plus(N, 0())) -> c_20(U31^#(isNat(N), N)) 982.99/297.06 , U11^#(mark(X1), X2) -> c_21(U11^#(X1, X2)) 982.99/297.06 , U11^#(ok(X1), ok(X2)) -> c_22(U11^#(X1, X2)) 982.99/297.06 , U12^#(mark(X)) -> c_23(U12^#(X)) 982.99/297.06 , U12^#(ok(X)) -> c_24(U12^#(X)) 982.99/297.06 , U21^#(mark(X)) -> c_26(U21^#(X)) 982.99/297.06 , U21^#(ok(X)) -> c_27(U21^#(X)) 982.99/297.06 , U31^#(mark(X1), X2) -> c_28(U31^#(X1, X2)) 982.99/297.06 , U31^#(ok(X1), ok(X2)) -> c_29(U31^#(X1, X2)) 982.99/297.06 , U41^#(mark(X1), X2, X3) -> c_30(U41^#(X1, X2, X3)) 982.99/297.06 , U41^#(ok(X1), ok(X2), ok(X3)) -> c_31(U41^#(X1, X2, X3)) 982.99/297.06 , U42^#(mark(X1), X2, X3) -> c_32(U42^#(X1, X2, X3)) 982.99/297.06 , U42^#(ok(X1), ok(X2), ok(X3)) -> c_33(U42^#(X1, X2, X3)) 982.99/297.06 , s^#(mark(X)) -> c_34(s^#(X)) 982.99/297.06 , s^#(ok(X)) -> c_35(s^#(X)) 982.99/297.06 , plus^#(X1, mark(X2)) -> c_36(plus^#(X1, X2)) 982.99/297.06 , plus^#(mark(X1), X2) -> c_37(plus^#(X1, X2)) 982.99/297.06 , plus^#(ok(X1), ok(X2)) -> c_38(plus^#(X1, X2)) 982.99/297.06 , isNat^#(ok(X)) -> c_25(isNat^#(X)) 982.99/297.06 , proper^#(U11(X1, X2)) -> c_39(U11^#(proper(X1), proper(X2))) 982.99/297.06 , proper^#(tt()) -> c_40() 982.99/297.06 , proper^#(U12(X)) -> c_41(U12^#(proper(X))) 982.99/297.06 , proper^#(isNat(X)) -> c_42(isNat^#(proper(X))) 982.99/297.06 , proper^#(U21(X)) -> c_43(U21^#(proper(X))) 982.99/297.06 , proper^#(U31(X1, X2)) -> c_44(U31^#(proper(X1), proper(X2))) 982.99/297.06 , proper^#(U41(X1, X2, X3)) -> 982.99/297.06 c_45(U41^#(proper(X1), proper(X2), proper(X3))) 982.99/297.06 , proper^#(U42(X1, X2, X3)) -> 982.99/297.06 c_46(U42^#(proper(X1), proper(X2), proper(X3))) 982.99/297.06 , proper^#(s(X)) -> c_47(s^#(proper(X))) 982.99/297.06 , proper^#(plus(X1, X2)) -> c_48(plus^#(proper(X1), proper(X2))) 982.99/297.06 , proper^#(0()) -> c_49() 982.99/297.06 , top^#(mark(X)) -> c_50(top^#(proper(X))) 982.99/297.06 , top^#(ok(X)) -> c_51(top^#(active(X))) } 982.99/297.06 Strict Trs: 982.99/297.06 { active(U11(X1, X2)) -> U11(active(X1), X2) 982.99/297.06 , active(U11(tt(), V2)) -> mark(U12(isNat(V2))) 982.99/297.06 , active(U12(X)) -> U12(active(X)) 982.99/297.06 , active(U12(tt())) -> mark(tt()) 982.99/297.06 , active(isNat(s(V1))) -> mark(U21(isNat(V1))) 982.99/297.06 , active(isNat(plus(V1, V2))) -> mark(U11(isNat(V1), V2)) 982.99/297.06 , active(isNat(0())) -> mark(tt()) 982.99/297.06 , active(U21(X)) -> U21(active(X)) 982.99/297.06 , active(U21(tt())) -> mark(tt()) 982.99/297.06 , active(U31(X1, X2)) -> U31(active(X1), X2) 982.99/297.06 , active(U31(tt(), N)) -> mark(N) 982.99/297.06 , active(U41(X1, X2, X3)) -> U41(active(X1), X2, X3) 982.99/297.06 , active(U41(tt(), M, N)) -> mark(U42(isNat(N), M, N)) 982.99/297.06 , active(U42(X1, X2, X3)) -> U42(active(X1), X2, X3) 982.99/297.06 , active(U42(tt(), M, N)) -> mark(s(plus(N, M))) 982.99/297.06 , active(s(X)) -> s(active(X)) 982.99/297.06 , active(plus(X1, X2)) -> plus(X1, active(X2)) 982.99/297.06 , active(plus(X1, X2)) -> plus(active(X1), X2) 982.99/297.06 , active(plus(N, s(M))) -> mark(U41(isNat(M), M, N)) 982.99/297.06 , active(plus(N, 0())) -> mark(U31(isNat(N), N)) 982.99/297.06 , U11(mark(X1), X2) -> mark(U11(X1, X2)) 982.99/297.06 , U11(ok(X1), ok(X2)) -> ok(U11(X1, X2)) 982.99/297.06 , U12(mark(X)) -> mark(U12(X)) 982.99/297.06 , U12(ok(X)) -> ok(U12(X)) 982.99/297.06 , isNat(ok(X)) -> ok(isNat(X)) 982.99/297.06 , U21(mark(X)) -> mark(U21(X)) 982.99/297.06 , U21(ok(X)) -> ok(U21(X)) 982.99/297.06 , U31(mark(X1), X2) -> mark(U31(X1, X2)) 982.99/297.06 , U31(ok(X1), ok(X2)) -> ok(U31(X1, X2)) 982.99/297.06 , U41(mark(X1), X2, X3) -> mark(U41(X1, X2, X3)) 982.99/297.06 , U41(ok(X1), ok(X2), ok(X3)) -> ok(U41(X1, X2, X3)) 982.99/297.06 , U42(mark(X1), X2, X3) -> mark(U42(X1, X2, X3)) 982.99/297.06 , U42(ok(X1), ok(X2), ok(X3)) -> ok(U42(X1, X2, X3)) 982.99/297.06 , s(mark(X)) -> mark(s(X)) 982.99/297.06 , s(ok(X)) -> ok(s(X)) 982.99/297.06 , plus(X1, mark(X2)) -> mark(plus(X1, X2)) 982.99/297.06 , plus(mark(X1), X2) -> mark(plus(X1, X2)) 982.99/297.06 , plus(ok(X1), ok(X2)) -> ok(plus(X1, X2)) 982.99/297.06 , proper(U11(X1, X2)) -> U11(proper(X1), proper(X2)) 982.99/297.06 , proper(tt()) -> ok(tt()) 982.99/297.06 , proper(U12(X)) -> U12(proper(X)) 982.99/297.06 , proper(isNat(X)) -> isNat(proper(X)) 982.99/297.06 , proper(U21(X)) -> U21(proper(X)) 982.99/297.06 , proper(U31(X1, X2)) -> U31(proper(X1), proper(X2)) 982.99/297.06 , proper(U41(X1, X2, X3)) -> 982.99/297.06 U41(proper(X1), proper(X2), proper(X3)) 982.99/297.06 , proper(U42(X1, X2, X3)) -> 982.99/297.06 U42(proper(X1), proper(X2), proper(X3)) 982.99/297.06 , proper(s(X)) -> s(proper(X)) 982.99/297.06 , proper(plus(X1, X2)) -> plus(proper(X1), proper(X2)) 982.99/297.06 , proper(0()) -> ok(0()) 982.99/297.06 , top(mark(X)) -> top(proper(X)) 982.99/297.06 , top(ok(X)) -> top(active(X)) } 982.99/297.06 Obligation: 982.99/297.06 runtime complexity 982.99/297.06 Answer: 982.99/297.06 MAYBE 982.99/297.06 982.99/297.06 Consider the dependency graph: 982.99/297.06 982.99/297.06 1: active^#(U11(X1, X2)) -> c_1(U11^#(active(X1), X2)) 982.99/297.06 -->_1 U11^#(ok(X1), ok(X2)) -> c_22(U11^#(X1, X2)) :22 982.99/297.06 -->_1 U11^#(mark(X1), X2) -> c_21(U11^#(X1, X2)) :21 982.99/297.06 982.99/297.06 2: active^#(U11(tt(), V2)) -> c_2(U12^#(isNat(V2))) 982.99/297.06 -->_1 U12^#(ok(X)) -> c_24(U12^#(X)) :24 982.99/297.06 -->_1 U12^#(mark(X)) -> c_23(U12^#(X)) :23 982.99/297.06 982.99/297.06 3: active^#(U12(X)) -> c_3(U12^#(active(X))) 982.99/297.06 -->_1 U12^#(ok(X)) -> c_24(U12^#(X)) :24 982.99/297.06 -->_1 U12^#(mark(X)) -> c_23(U12^#(X)) :23 982.99/297.06 982.99/297.06 4: active^#(U12(tt())) -> c_4() 982.99/297.06 982.99/297.06 5: active^#(isNat(s(V1))) -> c_5(U21^#(isNat(V1))) 982.99/297.06 -->_1 U21^#(ok(X)) -> c_27(U21^#(X)) :26 982.99/297.06 -->_1 U21^#(mark(X)) -> c_26(U21^#(X)) :25 982.99/297.06 982.99/297.06 6: active^#(isNat(plus(V1, V2))) -> c_6(U11^#(isNat(V1), V2)) 982.99/297.06 -->_1 U11^#(ok(X1), ok(X2)) -> c_22(U11^#(X1, X2)) :22 982.99/297.06 -->_1 U11^#(mark(X1), X2) -> c_21(U11^#(X1, X2)) :21 982.99/297.06 982.99/297.06 7: active^#(isNat(0())) -> c_7() 982.99/297.06 982.99/297.06 8: active^#(U21(X)) -> c_8(U21^#(active(X))) 982.99/297.06 -->_1 U21^#(ok(X)) -> c_27(U21^#(X)) :26 982.99/297.06 -->_1 U21^#(mark(X)) -> c_26(U21^#(X)) :25 982.99/297.06 982.99/297.06 9: active^#(U21(tt())) -> c_9() 982.99/297.06 982.99/297.06 10: active^#(U31(X1, X2)) -> c_10(U31^#(active(X1), X2)) 982.99/297.06 -->_1 U31^#(ok(X1), ok(X2)) -> c_29(U31^#(X1, X2)) :28 982.99/297.06 -->_1 U31^#(mark(X1), X2) -> c_28(U31^#(X1, X2)) :27 982.99/297.06 982.99/297.06 11: active^#(U31(tt(), N)) -> c_11(N) 982.99/297.06 -->_1 top^#(ok(X)) -> c_51(top^#(active(X))) :51 982.99/297.06 -->_1 top^#(mark(X)) -> c_50(top^#(proper(X))) :50 982.99/297.06 -->_1 proper^#(plus(X1, X2)) -> 982.99/297.06 c_48(plus^#(proper(X1), proper(X2))) :48 982.99/297.06 -->_1 proper^#(s(X)) -> c_47(s^#(proper(X))) :47 982.99/297.06 -->_1 proper^#(U42(X1, X2, X3)) -> 982.99/297.06 c_46(U42^#(proper(X1), proper(X2), proper(X3))) :46 982.99/297.06 -->_1 proper^#(U41(X1, X2, X3)) -> 982.99/297.06 c_45(U41^#(proper(X1), proper(X2), proper(X3))) :45 982.99/297.06 -->_1 proper^#(U31(X1, X2)) -> 982.99/297.06 c_44(U31^#(proper(X1), proper(X2))) :44 982.99/297.06 -->_1 proper^#(U21(X)) -> c_43(U21^#(proper(X))) :43 982.99/297.06 -->_1 proper^#(isNat(X)) -> c_42(isNat^#(proper(X))) :42 982.99/297.06 -->_1 proper^#(U12(X)) -> c_41(U12^#(proper(X))) :41 982.99/297.06 -->_1 proper^#(U11(X1, X2)) -> 982.99/297.06 c_39(U11^#(proper(X1), proper(X2))) :39 982.99/297.06 -->_1 isNat^#(ok(X)) -> c_25(isNat^#(X)) :38 982.99/297.06 -->_1 plus^#(ok(X1), ok(X2)) -> c_38(plus^#(X1, X2)) :37 982.99/297.06 -->_1 plus^#(mark(X1), X2) -> c_37(plus^#(X1, X2)) :36 982.99/297.06 -->_1 plus^#(X1, mark(X2)) -> c_36(plus^#(X1, X2)) :35 982.99/297.06 -->_1 s^#(ok(X)) -> c_35(s^#(X)) :34 982.99/297.06 -->_1 s^#(mark(X)) -> c_34(s^#(X)) :33 982.99/297.06 -->_1 U42^#(ok(X1), ok(X2), ok(X3)) -> c_33(U42^#(X1, X2, X3)) :32 982.99/297.06 -->_1 U42^#(mark(X1), X2, X3) -> c_32(U42^#(X1, X2, X3)) :31 982.99/297.06 -->_1 U41^#(ok(X1), ok(X2), ok(X3)) -> c_31(U41^#(X1, X2, X3)) :30 982.99/297.06 -->_1 U41^#(mark(X1), X2, X3) -> c_30(U41^#(X1, X2, X3)) :29 982.99/297.06 -->_1 U31^#(ok(X1), ok(X2)) -> c_29(U31^#(X1, X2)) :28 982.99/297.06 -->_1 U31^#(mark(X1), X2) -> c_28(U31^#(X1, X2)) :27 982.99/297.06 -->_1 U21^#(ok(X)) -> c_27(U21^#(X)) :26 982.99/297.06 -->_1 U21^#(mark(X)) -> c_26(U21^#(X)) :25 982.99/297.06 -->_1 U12^#(ok(X)) -> c_24(U12^#(X)) :24 982.99/297.06 -->_1 U12^#(mark(X)) -> c_23(U12^#(X)) :23 982.99/297.06 -->_1 U11^#(ok(X1), ok(X2)) -> c_22(U11^#(X1, X2)) :22 982.99/297.06 -->_1 U11^#(mark(X1), X2) -> c_21(U11^#(X1, X2)) :21 982.99/297.06 -->_1 active^#(plus(N, 0())) -> c_20(U31^#(isNat(N), N)) :20 982.99/297.06 -->_1 active^#(plus(N, s(M))) -> c_19(U41^#(isNat(M), M, N)) :19 982.99/297.06 -->_1 active^#(plus(X1, X2)) -> c_18(plus^#(active(X1), X2)) :18 982.99/297.06 -->_1 active^#(plus(X1, X2)) -> c_17(plus^#(X1, active(X2))) :17 982.99/297.06 -->_1 active^#(s(X)) -> c_16(s^#(active(X))) :16 982.99/297.06 -->_1 active^#(U42(tt(), M, N)) -> c_15(s^#(plus(N, M))) :15 982.99/297.06 -->_1 active^#(U42(X1, X2, X3)) -> 982.99/297.06 c_14(U42^#(active(X1), X2, X3)) :14 982.99/297.06 -->_1 active^#(U41(tt(), M, N)) -> c_13(U42^#(isNat(N), M, N)) :13 982.99/297.06 -->_1 active^#(U41(X1, X2, X3)) -> 982.99/297.06 c_12(U41^#(active(X1), X2, X3)) :12 982.99/297.06 -->_1 proper^#(0()) -> c_49() :49 982.99/297.06 -->_1 proper^#(tt()) -> c_40() :40 982.99/297.06 -->_1 active^#(U31(tt(), N)) -> c_11(N) :11 982.99/297.06 -->_1 active^#(U31(X1, X2)) -> c_10(U31^#(active(X1), X2)) :10 982.99/297.06 -->_1 active^#(U21(tt())) -> c_9() :9 982.99/297.06 -->_1 active^#(U21(X)) -> c_8(U21^#(active(X))) :8 982.99/297.06 -->_1 active^#(isNat(0())) -> c_7() :7 982.99/297.06 -->_1 active^#(isNat(plus(V1, V2))) -> c_6(U11^#(isNat(V1), V2)) :6 982.99/297.06 -->_1 active^#(isNat(s(V1))) -> c_5(U21^#(isNat(V1))) :5 982.99/297.06 -->_1 active^#(U12(tt())) -> c_4() :4 982.99/297.06 -->_1 active^#(U12(X)) -> c_3(U12^#(active(X))) :3 982.99/297.06 -->_1 active^#(U11(tt(), V2)) -> c_2(U12^#(isNat(V2))) :2 982.99/297.06 -->_1 active^#(U11(X1, X2)) -> c_1(U11^#(active(X1), X2)) :1 982.99/297.06 982.99/297.06 12: active^#(U41(X1, X2, X3)) -> c_12(U41^#(active(X1), X2, X3)) 982.99/297.06 -->_1 U41^#(ok(X1), ok(X2), ok(X3)) -> c_31(U41^#(X1, X2, X3)) :30 982.99/297.06 -->_1 U41^#(mark(X1), X2, X3) -> c_30(U41^#(X1, X2, X3)) :29 982.99/297.06 982.99/297.06 13: active^#(U41(tt(), M, N)) -> c_13(U42^#(isNat(N), M, N)) 982.99/297.06 -->_1 U42^#(ok(X1), ok(X2), ok(X3)) -> c_33(U42^#(X1, X2, X3)) :32 982.99/297.06 -->_1 U42^#(mark(X1), X2, X3) -> c_32(U42^#(X1, X2, X3)) :31 982.99/297.06 982.99/297.06 14: active^#(U42(X1, X2, X3)) -> c_14(U42^#(active(X1), X2, X3)) 982.99/297.06 -->_1 U42^#(ok(X1), ok(X2), ok(X3)) -> c_33(U42^#(X1, X2, X3)) :32 982.99/297.06 -->_1 U42^#(mark(X1), X2, X3) -> c_32(U42^#(X1, X2, X3)) :31 982.99/297.06 982.99/297.06 15: active^#(U42(tt(), M, N)) -> c_15(s^#(plus(N, M))) 982.99/297.06 -->_1 s^#(ok(X)) -> c_35(s^#(X)) :34 982.99/297.06 -->_1 s^#(mark(X)) -> c_34(s^#(X)) :33 982.99/297.06 982.99/297.06 16: active^#(s(X)) -> c_16(s^#(active(X))) 982.99/297.06 -->_1 s^#(ok(X)) -> c_35(s^#(X)) :34 982.99/297.06 -->_1 s^#(mark(X)) -> c_34(s^#(X)) :33 982.99/297.06 982.99/297.06 17: active^#(plus(X1, X2)) -> c_17(plus^#(X1, active(X2))) 982.99/297.06 -->_1 plus^#(ok(X1), ok(X2)) -> c_38(plus^#(X1, X2)) :37 982.99/297.06 -->_1 plus^#(mark(X1), X2) -> c_37(plus^#(X1, X2)) :36 982.99/297.06 -->_1 plus^#(X1, mark(X2)) -> c_36(plus^#(X1, X2)) :35 982.99/297.06 982.99/297.06 18: active^#(plus(X1, X2)) -> c_18(plus^#(active(X1), X2)) 982.99/297.06 -->_1 plus^#(ok(X1), ok(X2)) -> c_38(plus^#(X1, X2)) :37 982.99/297.06 -->_1 plus^#(mark(X1), X2) -> c_37(plus^#(X1, X2)) :36 982.99/297.06 -->_1 plus^#(X1, mark(X2)) -> c_36(plus^#(X1, X2)) :35 982.99/297.06 982.99/297.06 19: active^#(plus(N, s(M))) -> c_19(U41^#(isNat(M), M, N)) 982.99/297.06 -->_1 U41^#(ok(X1), ok(X2), ok(X3)) -> c_31(U41^#(X1, X2, X3)) :30 982.99/297.06 -->_1 U41^#(mark(X1), X2, X3) -> c_30(U41^#(X1, X2, X3)) :29 982.99/297.06 982.99/297.06 20: active^#(plus(N, 0())) -> c_20(U31^#(isNat(N), N)) 982.99/297.06 -->_1 U31^#(ok(X1), ok(X2)) -> c_29(U31^#(X1, X2)) :28 982.99/297.06 -->_1 U31^#(mark(X1), X2) -> c_28(U31^#(X1, X2)) :27 982.99/297.06 982.99/297.06 21: U11^#(mark(X1), X2) -> c_21(U11^#(X1, X2)) 982.99/297.06 -->_1 U11^#(ok(X1), ok(X2)) -> c_22(U11^#(X1, X2)) :22 982.99/297.06 -->_1 U11^#(mark(X1), X2) -> c_21(U11^#(X1, X2)) :21 982.99/297.06 982.99/297.06 22: U11^#(ok(X1), ok(X2)) -> c_22(U11^#(X1, X2)) 982.99/297.06 -->_1 U11^#(ok(X1), ok(X2)) -> c_22(U11^#(X1, X2)) :22 982.99/297.06 -->_1 U11^#(mark(X1), X2) -> c_21(U11^#(X1, X2)) :21 982.99/297.06 982.99/297.06 23: U12^#(mark(X)) -> c_23(U12^#(X)) 982.99/297.06 -->_1 U12^#(ok(X)) -> c_24(U12^#(X)) :24 982.99/297.06 -->_1 U12^#(mark(X)) -> c_23(U12^#(X)) :23 982.99/297.06 982.99/297.06 24: U12^#(ok(X)) -> c_24(U12^#(X)) 982.99/297.06 -->_1 U12^#(ok(X)) -> c_24(U12^#(X)) :24 982.99/297.06 -->_1 U12^#(mark(X)) -> c_23(U12^#(X)) :23 982.99/297.06 982.99/297.06 25: U21^#(mark(X)) -> c_26(U21^#(X)) 982.99/297.06 -->_1 U21^#(ok(X)) -> c_27(U21^#(X)) :26 982.99/297.06 -->_1 U21^#(mark(X)) -> c_26(U21^#(X)) :25 982.99/297.06 982.99/297.06 26: U21^#(ok(X)) -> c_27(U21^#(X)) 982.99/297.06 -->_1 U21^#(ok(X)) -> c_27(U21^#(X)) :26 982.99/297.06 -->_1 U21^#(mark(X)) -> c_26(U21^#(X)) :25 982.99/297.06 982.99/297.06 27: U31^#(mark(X1), X2) -> c_28(U31^#(X1, X2)) 982.99/297.06 -->_1 U31^#(ok(X1), ok(X2)) -> c_29(U31^#(X1, X2)) :28 982.99/297.06 -->_1 U31^#(mark(X1), X2) -> c_28(U31^#(X1, X2)) :27 982.99/297.06 982.99/297.06 28: U31^#(ok(X1), ok(X2)) -> c_29(U31^#(X1, X2)) 982.99/297.06 -->_1 U31^#(ok(X1), ok(X2)) -> c_29(U31^#(X1, X2)) :28 982.99/297.06 -->_1 U31^#(mark(X1), X2) -> c_28(U31^#(X1, X2)) :27 982.99/297.06 982.99/297.06 29: U41^#(mark(X1), X2, X3) -> c_30(U41^#(X1, X2, X3)) 982.99/297.06 -->_1 U41^#(ok(X1), ok(X2), ok(X3)) -> c_31(U41^#(X1, X2, X3)) :30 982.99/297.06 -->_1 U41^#(mark(X1), X2, X3) -> c_30(U41^#(X1, X2, X3)) :29 982.99/297.06 982.99/297.06 30: U41^#(ok(X1), ok(X2), ok(X3)) -> c_31(U41^#(X1, X2, X3)) 982.99/297.06 -->_1 U41^#(ok(X1), ok(X2), ok(X3)) -> c_31(U41^#(X1, X2, X3)) :30 982.99/297.06 -->_1 U41^#(mark(X1), X2, X3) -> c_30(U41^#(X1, X2, X3)) :29 982.99/297.06 982.99/297.06 31: U42^#(mark(X1), X2, X3) -> c_32(U42^#(X1, X2, X3)) 982.99/297.06 -->_1 U42^#(ok(X1), ok(X2), ok(X3)) -> c_33(U42^#(X1, X2, X3)) :32 982.99/297.06 -->_1 U42^#(mark(X1), X2, X3) -> c_32(U42^#(X1, X2, X3)) :31 982.99/297.06 982.99/297.06 32: U42^#(ok(X1), ok(X2), ok(X3)) -> c_33(U42^#(X1, X2, X3)) 982.99/297.06 -->_1 U42^#(ok(X1), ok(X2), ok(X3)) -> c_33(U42^#(X1, X2, X3)) :32 982.99/297.06 -->_1 U42^#(mark(X1), X2, X3) -> c_32(U42^#(X1, X2, X3)) :31 982.99/297.06 982.99/297.06 33: s^#(mark(X)) -> c_34(s^#(X)) 982.99/297.06 -->_1 s^#(ok(X)) -> c_35(s^#(X)) :34 982.99/297.06 -->_1 s^#(mark(X)) -> c_34(s^#(X)) :33 982.99/297.06 982.99/297.06 34: s^#(ok(X)) -> c_35(s^#(X)) 982.99/297.06 -->_1 s^#(ok(X)) -> c_35(s^#(X)) :34 982.99/297.06 -->_1 s^#(mark(X)) -> c_34(s^#(X)) :33 982.99/297.06 982.99/297.06 35: plus^#(X1, mark(X2)) -> c_36(plus^#(X1, X2)) 982.99/297.06 -->_1 plus^#(ok(X1), ok(X2)) -> c_38(plus^#(X1, X2)) :37 982.99/297.06 -->_1 plus^#(mark(X1), X2) -> c_37(plus^#(X1, X2)) :36 982.99/297.06 -->_1 plus^#(X1, mark(X2)) -> c_36(plus^#(X1, X2)) :35 982.99/297.06 982.99/297.06 36: plus^#(mark(X1), X2) -> c_37(plus^#(X1, X2)) 982.99/297.06 -->_1 plus^#(ok(X1), ok(X2)) -> c_38(plus^#(X1, X2)) :37 982.99/297.06 -->_1 plus^#(mark(X1), X2) -> c_37(plus^#(X1, X2)) :36 982.99/297.06 -->_1 plus^#(X1, mark(X2)) -> c_36(plus^#(X1, X2)) :35 982.99/297.06 982.99/297.06 37: plus^#(ok(X1), ok(X2)) -> c_38(plus^#(X1, X2)) 982.99/297.06 -->_1 plus^#(ok(X1), ok(X2)) -> c_38(plus^#(X1, X2)) :37 982.99/297.06 -->_1 plus^#(mark(X1), X2) -> c_37(plus^#(X1, X2)) :36 982.99/297.06 -->_1 plus^#(X1, mark(X2)) -> c_36(plus^#(X1, X2)) :35 982.99/297.06 982.99/297.06 38: isNat^#(ok(X)) -> c_25(isNat^#(X)) 982.99/297.06 -->_1 isNat^#(ok(X)) -> c_25(isNat^#(X)) :38 982.99/297.06 982.99/297.06 39: proper^#(U11(X1, X2)) -> c_39(U11^#(proper(X1), proper(X2))) 982.99/297.06 -->_1 U11^#(ok(X1), ok(X2)) -> c_22(U11^#(X1, X2)) :22 982.99/297.06 -->_1 U11^#(mark(X1), X2) -> c_21(U11^#(X1, X2)) :21 982.99/297.06 982.99/297.06 40: proper^#(tt()) -> c_40() 982.99/297.06 982.99/297.06 41: proper^#(U12(X)) -> c_41(U12^#(proper(X))) 982.99/297.06 -->_1 U12^#(ok(X)) -> c_24(U12^#(X)) :24 982.99/297.06 -->_1 U12^#(mark(X)) -> c_23(U12^#(X)) :23 982.99/297.06 982.99/297.06 42: proper^#(isNat(X)) -> c_42(isNat^#(proper(X))) 982.99/297.06 -->_1 isNat^#(ok(X)) -> c_25(isNat^#(X)) :38 982.99/297.06 982.99/297.06 43: proper^#(U21(X)) -> c_43(U21^#(proper(X))) 982.99/297.06 -->_1 U21^#(ok(X)) -> c_27(U21^#(X)) :26 982.99/297.06 -->_1 U21^#(mark(X)) -> c_26(U21^#(X)) :25 982.99/297.06 982.99/297.06 44: proper^#(U31(X1, X2)) -> c_44(U31^#(proper(X1), proper(X2))) 982.99/297.06 -->_1 U31^#(ok(X1), ok(X2)) -> c_29(U31^#(X1, X2)) :28 982.99/297.06 -->_1 U31^#(mark(X1), X2) -> c_28(U31^#(X1, X2)) :27 982.99/297.06 982.99/297.06 45: proper^#(U41(X1, X2, X3)) -> 982.99/297.06 c_45(U41^#(proper(X1), proper(X2), proper(X3))) 982.99/297.06 -->_1 U41^#(ok(X1), ok(X2), ok(X3)) -> c_31(U41^#(X1, X2, X3)) :30 982.99/297.06 -->_1 U41^#(mark(X1), X2, X3) -> c_30(U41^#(X1, X2, X3)) :29 982.99/297.06 982.99/297.06 46: proper^#(U42(X1, X2, X3)) -> 982.99/297.06 c_46(U42^#(proper(X1), proper(X2), proper(X3))) 982.99/297.06 -->_1 U42^#(ok(X1), ok(X2), ok(X3)) -> c_33(U42^#(X1, X2, X3)) :32 982.99/297.06 -->_1 U42^#(mark(X1), X2, X3) -> c_32(U42^#(X1, X2, X3)) :31 982.99/297.06 982.99/297.06 47: proper^#(s(X)) -> c_47(s^#(proper(X))) 982.99/297.06 -->_1 s^#(ok(X)) -> c_35(s^#(X)) :34 982.99/297.06 -->_1 s^#(mark(X)) -> c_34(s^#(X)) :33 982.99/297.06 982.99/297.06 48: proper^#(plus(X1, X2)) -> c_48(plus^#(proper(X1), proper(X2))) 982.99/297.06 -->_1 plus^#(ok(X1), ok(X2)) -> c_38(plus^#(X1, X2)) :37 982.99/297.06 -->_1 plus^#(mark(X1), X2) -> c_37(plus^#(X1, X2)) :36 982.99/297.06 -->_1 plus^#(X1, mark(X2)) -> c_36(plus^#(X1, X2)) :35 982.99/297.06 982.99/297.06 49: proper^#(0()) -> c_49() 982.99/297.07 982.99/297.07 50: top^#(mark(X)) -> c_50(top^#(proper(X))) 982.99/297.07 -->_1 top^#(ok(X)) -> c_51(top^#(active(X))) :51 982.99/297.07 -->_1 top^#(mark(X)) -> c_50(top^#(proper(X))) :50 982.99/297.07 982.99/297.07 51: top^#(ok(X)) -> c_51(top^#(active(X))) 982.99/297.07 -->_1 top^#(ok(X)) -> c_51(top^#(active(X))) :51 982.99/297.07 -->_1 top^#(mark(X)) -> c_50(top^#(proper(X))) :50 982.99/297.07 982.99/297.07 982.99/297.07 Only the nodes 982.99/297.07 {21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,37,36,38,40,49,50,51} 982.99/297.07 are reachable from nodes 982.99/297.07 {21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,40,49,50,51} 982.99/297.07 that start derivation from marked basic terms. The nodes not 982.99/297.07 reachable are removed from the problem. 982.99/297.07 982.99/297.07 We are left with following problem, upon which TcT provides the 982.99/297.07 certificate MAYBE. 982.99/297.07 982.99/297.07 Strict DPs: 982.99/297.07 { U11^#(mark(X1), X2) -> c_21(U11^#(X1, X2)) 982.99/297.07 , U11^#(ok(X1), ok(X2)) -> c_22(U11^#(X1, X2)) 982.99/297.07 , U12^#(mark(X)) -> c_23(U12^#(X)) 982.99/297.07 , U12^#(ok(X)) -> c_24(U12^#(X)) 982.99/297.07 , U21^#(mark(X)) -> c_26(U21^#(X)) 982.99/297.07 , U21^#(ok(X)) -> c_27(U21^#(X)) 982.99/297.07 , U31^#(mark(X1), X2) -> c_28(U31^#(X1, X2)) 982.99/297.07 , U31^#(ok(X1), ok(X2)) -> c_29(U31^#(X1, X2)) 982.99/297.07 , U41^#(mark(X1), X2, X3) -> c_30(U41^#(X1, X2, X3)) 982.99/297.07 , U41^#(ok(X1), ok(X2), ok(X3)) -> c_31(U41^#(X1, X2, X3)) 982.99/297.07 , U42^#(mark(X1), X2, X3) -> c_32(U42^#(X1, X2, X3)) 982.99/297.07 , U42^#(ok(X1), ok(X2), ok(X3)) -> c_33(U42^#(X1, X2, X3)) 982.99/297.07 , s^#(mark(X)) -> c_34(s^#(X)) 982.99/297.07 , s^#(ok(X)) -> c_35(s^#(X)) 982.99/297.07 , plus^#(X1, mark(X2)) -> c_36(plus^#(X1, X2)) 982.99/297.07 , plus^#(mark(X1), X2) -> c_37(plus^#(X1, X2)) 982.99/297.07 , plus^#(ok(X1), ok(X2)) -> c_38(plus^#(X1, X2)) 982.99/297.07 , isNat^#(ok(X)) -> c_25(isNat^#(X)) 982.99/297.07 , proper^#(tt()) -> c_40() 982.99/297.07 , proper^#(0()) -> c_49() 982.99/297.07 , top^#(mark(X)) -> c_50(top^#(proper(X))) 982.99/297.07 , top^#(ok(X)) -> c_51(top^#(active(X))) } 982.99/297.07 Strict Trs: 982.99/297.07 { active(U11(X1, X2)) -> U11(active(X1), X2) 982.99/297.07 , active(U11(tt(), V2)) -> mark(U12(isNat(V2))) 982.99/297.07 , active(U12(X)) -> U12(active(X)) 982.99/297.07 , active(U12(tt())) -> mark(tt()) 982.99/297.07 , active(isNat(s(V1))) -> mark(U21(isNat(V1))) 982.99/297.07 , active(isNat(plus(V1, V2))) -> mark(U11(isNat(V1), V2)) 982.99/297.07 , active(isNat(0())) -> mark(tt()) 982.99/297.07 , active(U21(X)) -> U21(active(X)) 982.99/297.07 , active(U21(tt())) -> mark(tt()) 982.99/297.07 , active(U31(X1, X2)) -> U31(active(X1), X2) 982.99/297.07 , active(U31(tt(), N)) -> mark(N) 982.99/297.07 , active(U41(X1, X2, X3)) -> U41(active(X1), X2, X3) 982.99/297.07 , active(U41(tt(), M, N)) -> mark(U42(isNat(N), M, N)) 982.99/297.07 , active(U42(X1, X2, X3)) -> U42(active(X1), X2, X3) 982.99/297.07 , active(U42(tt(), M, N)) -> mark(s(plus(N, M))) 982.99/297.07 , active(s(X)) -> s(active(X)) 982.99/297.07 , active(plus(X1, X2)) -> plus(X1, active(X2)) 982.99/297.07 , active(plus(X1, X2)) -> plus(active(X1), X2) 982.99/297.07 , active(plus(N, s(M))) -> mark(U41(isNat(M), M, N)) 982.99/297.07 , active(plus(N, 0())) -> mark(U31(isNat(N), N)) 982.99/297.07 , U11(mark(X1), X2) -> mark(U11(X1, X2)) 982.99/297.07 , U11(ok(X1), ok(X2)) -> ok(U11(X1, X2)) 982.99/297.07 , U12(mark(X)) -> mark(U12(X)) 982.99/297.07 , U12(ok(X)) -> ok(U12(X)) 982.99/297.07 , isNat(ok(X)) -> ok(isNat(X)) 982.99/297.07 , U21(mark(X)) -> mark(U21(X)) 982.99/297.07 , U21(ok(X)) -> ok(U21(X)) 982.99/297.07 , U31(mark(X1), X2) -> mark(U31(X1, X2)) 982.99/297.07 , U31(ok(X1), ok(X2)) -> ok(U31(X1, X2)) 982.99/297.07 , U41(mark(X1), X2, X3) -> mark(U41(X1, X2, X3)) 982.99/297.07 , U41(ok(X1), ok(X2), ok(X3)) -> ok(U41(X1, X2, X3)) 982.99/297.07 , U42(mark(X1), X2, X3) -> mark(U42(X1, X2, X3)) 982.99/297.07 , U42(ok(X1), ok(X2), ok(X3)) -> ok(U42(X1, X2, X3)) 982.99/297.07 , s(mark(X)) -> mark(s(X)) 982.99/297.07 , s(ok(X)) -> ok(s(X)) 982.99/297.07 , plus(X1, mark(X2)) -> mark(plus(X1, X2)) 982.99/297.07 , plus(mark(X1), X2) -> mark(plus(X1, X2)) 982.99/297.07 , plus(ok(X1), ok(X2)) -> ok(plus(X1, X2)) 982.99/297.07 , proper(U11(X1, X2)) -> U11(proper(X1), proper(X2)) 982.99/297.07 , proper(tt()) -> ok(tt()) 982.99/297.07 , proper(U12(X)) -> U12(proper(X)) 982.99/297.07 , proper(isNat(X)) -> isNat(proper(X)) 982.99/297.07 , proper(U21(X)) -> U21(proper(X)) 982.99/297.07 , proper(U31(X1, X2)) -> U31(proper(X1), proper(X2)) 982.99/297.07 , proper(U41(X1, X2, X3)) -> 982.99/297.07 U41(proper(X1), proper(X2), proper(X3)) 982.99/297.07 , proper(U42(X1, X2, X3)) -> 982.99/297.07 U42(proper(X1), proper(X2), proper(X3)) 982.99/297.07 , proper(s(X)) -> s(proper(X)) 982.99/297.07 , proper(plus(X1, X2)) -> plus(proper(X1), proper(X2)) 982.99/297.07 , proper(0()) -> ok(0()) 982.99/297.07 , top(mark(X)) -> top(proper(X)) 982.99/297.07 , top(ok(X)) -> top(active(X)) } 982.99/297.07 Obligation: 982.99/297.07 runtime complexity 982.99/297.07 Answer: 982.99/297.07 MAYBE 982.99/297.07 982.99/297.07 We estimate the number of application of {19,20} by applications of 982.99/297.07 Pre({19,20}) = {}. Here rules are labeled as follows: 982.99/297.07 982.99/297.07 DPs: 982.99/297.07 { 1: U11^#(mark(X1), X2) -> c_21(U11^#(X1, X2)) 982.99/297.07 , 2: U11^#(ok(X1), ok(X2)) -> c_22(U11^#(X1, X2)) 982.99/297.07 , 3: U12^#(mark(X)) -> c_23(U12^#(X)) 982.99/297.07 , 4: U12^#(ok(X)) -> c_24(U12^#(X)) 982.99/297.07 , 5: U21^#(mark(X)) -> c_26(U21^#(X)) 982.99/297.07 , 6: U21^#(ok(X)) -> c_27(U21^#(X)) 982.99/297.07 , 7: U31^#(mark(X1), X2) -> c_28(U31^#(X1, X2)) 982.99/297.07 , 8: U31^#(ok(X1), ok(X2)) -> c_29(U31^#(X1, X2)) 982.99/297.07 , 9: U41^#(mark(X1), X2, X3) -> c_30(U41^#(X1, X2, X3)) 982.99/297.07 , 10: U41^#(ok(X1), ok(X2), ok(X3)) -> c_31(U41^#(X1, X2, X3)) 982.99/297.07 , 11: U42^#(mark(X1), X2, X3) -> c_32(U42^#(X1, X2, X3)) 982.99/297.07 , 12: U42^#(ok(X1), ok(X2), ok(X3)) -> c_33(U42^#(X1, X2, X3)) 982.99/297.07 , 13: s^#(mark(X)) -> c_34(s^#(X)) 982.99/297.07 , 14: s^#(ok(X)) -> c_35(s^#(X)) 982.99/297.07 , 15: plus^#(X1, mark(X2)) -> c_36(plus^#(X1, X2)) 982.99/297.07 , 16: plus^#(mark(X1), X2) -> c_37(plus^#(X1, X2)) 982.99/297.07 , 17: plus^#(ok(X1), ok(X2)) -> c_38(plus^#(X1, X2)) 982.99/297.07 , 18: isNat^#(ok(X)) -> c_25(isNat^#(X)) 982.99/297.07 , 19: proper^#(tt()) -> c_40() 982.99/297.07 , 20: proper^#(0()) -> c_49() 982.99/297.07 , 21: top^#(mark(X)) -> c_50(top^#(proper(X))) 982.99/297.07 , 22: top^#(ok(X)) -> c_51(top^#(active(X))) } 982.99/297.07 982.99/297.07 We are left with following problem, upon which TcT provides the 982.99/297.07 certificate MAYBE. 982.99/297.07 982.99/297.07 Strict DPs: 982.99/297.07 { U11^#(mark(X1), X2) -> c_21(U11^#(X1, X2)) 982.99/297.07 , U11^#(ok(X1), ok(X2)) -> c_22(U11^#(X1, X2)) 982.99/297.07 , U12^#(mark(X)) -> c_23(U12^#(X)) 982.99/297.07 , U12^#(ok(X)) -> c_24(U12^#(X)) 982.99/297.07 , U21^#(mark(X)) -> c_26(U21^#(X)) 982.99/297.07 , U21^#(ok(X)) -> c_27(U21^#(X)) 982.99/297.07 , U31^#(mark(X1), X2) -> c_28(U31^#(X1, X2)) 982.99/297.07 , U31^#(ok(X1), ok(X2)) -> c_29(U31^#(X1, X2)) 982.99/297.07 , U41^#(mark(X1), X2, X3) -> c_30(U41^#(X1, X2, X3)) 982.99/297.07 , U41^#(ok(X1), ok(X2), ok(X3)) -> c_31(U41^#(X1, X2, X3)) 982.99/297.07 , U42^#(mark(X1), X2, X3) -> c_32(U42^#(X1, X2, X3)) 982.99/297.07 , U42^#(ok(X1), ok(X2), ok(X3)) -> c_33(U42^#(X1, X2, X3)) 982.99/297.07 , s^#(mark(X)) -> c_34(s^#(X)) 982.99/297.07 , s^#(ok(X)) -> c_35(s^#(X)) 982.99/297.07 , plus^#(X1, mark(X2)) -> c_36(plus^#(X1, X2)) 982.99/297.07 , plus^#(mark(X1), X2) -> c_37(plus^#(X1, X2)) 982.99/297.07 , plus^#(ok(X1), ok(X2)) -> c_38(plus^#(X1, X2)) 982.99/297.07 , isNat^#(ok(X)) -> c_25(isNat^#(X)) 982.99/297.07 , top^#(mark(X)) -> c_50(top^#(proper(X))) 982.99/297.07 , top^#(ok(X)) -> c_51(top^#(active(X))) } 982.99/297.07 Strict Trs: 982.99/297.07 { active(U11(X1, X2)) -> U11(active(X1), X2) 982.99/297.07 , active(U11(tt(), V2)) -> mark(U12(isNat(V2))) 982.99/297.07 , active(U12(X)) -> U12(active(X)) 982.99/297.07 , active(U12(tt())) -> mark(tt()) 982.99/297.07 , active(isNat(s(V1))) -> mark(U21(isNat(V1))) 982.99/297.07 , active(isNat(plus(V1, V2))) -> mark(U11(isNat(V1), V2)) 982.99/297.07 , active(isNat(0())) -> mark(tt()) 982.99/297.07 , active(U21(X)) -> U21(active(X)) 982.99/297.07 , active(U21(tt())) -> mark(tt()) 982.99/297.07 , active(U31(X1, X2)) -> U31(active(X1), X2) 982.99/297.07 , active(U31(tt(), N)) -> mark(N) 982.99/297.07 , active(U41(X1, X2, X3)) -> U41(active(X1), X2, X3) 982.99/297.07 , active(U41(tt(), M, N)) -> mark(U42(isNat(N), M, N)) 982.99/297.07 , active(U42(X1, X2, X3)) -> U42(active(X1), X2, X3) 982.99/297.07 , active(U42(tt(), M, N)) -> mark(s(plus(N, M))) 982.99/297.07 , active(s(X)) -> s(active(X)) 982.99/297.07 , active(plus(X1, X2)) -> plus(X1, active(X2)) 982.99/297.07 , active(plus(X1, X2)) -> plus(active(X1), X2) 982.99/297.07 , active(plus(N, s(M))) -> mark(U41(isNat(M), M, N)) 982.99/297.07 , active(plus(N, 0())) -> mark(U31(isNat(N), N)) 982.99/297.07 , U11(mark(X1), X2) -> mark(U11(X1, X2)) 982.99/297.07 , U11(ok(X1), ok(X2)) -> ok(U11(X1, X2)) 982.99/297.07 , U12(mark(X)) -> mark(U12(X)) 982.99/297.07 , U12(ok(X)) -> ok(U12(X)) 982.99/297.07 , isNat(ok(X)) -> ok(isNat(X)) 982.99/297.07 , U21(mark(X)) -> mark(U21(X)) 982.99/297.07 , U21(ok(X)) -> ok(U21(X)) 982.99/297.07 , U31(mark(X1), X2) -> mark(U31(X1, X2)) 982.99/297.07 , U31(ok(X1), ok(X2)) -> ok(U31(X1, X2)) 982.99/297.07 , U41(mark(X1), X2, X3) -> mark(U41(X1, X2, X3)) 982.99/297.07 , U41(ok(X1), ok(X2), ok(X3)) -> ok(U41(X1, X2, X3)) 982.99/297.07 , U42(mark(X1), X2, X3) -> mark(U42(X1, X2, X3)) 982.99/297.07 , U42(ok(X1), ok(X2), ok(X3)) -> ok(U42(X1, X2, X3)) 982.99/297.07 , s(mark(X)) -> mark(s(X)) 982.99/297.07 , s(ok(X)) -> ok(s(X)) 982.99/297.07 , plus(X1, mark(X2)) -> mark(plus(X1, X2)) 982.99/297.07 , plus(mark(X1), X2) -> mark(plus(X1, X2)) 982.99/297.07 , plus(ok(X1), ok(X2)) -> ok(plus(X1, X2)) 982.99/297.07 , proper(U11(X1, X2)) -> U11(proper(X1), proper(X2)) 982.99/297.07 , proper(tt()) -> ok(tt()) 982.99/297.07 , proper(U12(X)) -> U12(proper(X)) 982.99/297.07 , proper(isNat(X)) -> isNat(proper(X)) 982.99/297.07 , proper(U21(X)) -> U21(proper(X)) 982.99/297.07 , proper(U31(X1, X2)) -> U31(proper(X1), proper(X2)) 982.99/297.07 , proper(U41(X1, X2, X3)) -> 982.99/297.07 U41(proper(X1), proper(X2), proper(X3)) 982.99/297.07 , proper(U42(X1, X2, X3)) -> 982.99/297.07 U42(proper(X1), proper(X2), proper(X3)) 982.99/297.07 , proper(s(X)) -> s(proper(X)) 982.99/297.07 , proper(plus(X1, X2)) -> plus(proper(X1), proper(X2)) 982.99/297.07 , proper(0()) -> ok(0()) 982.99/297.07 , top(mark(X)) -> top(proper(X)) 982.99/297.07 , top(ok(X)) -> top(active(X)) } 982.99/297.07 Weak DPs: 982.99/297.07 { proper^#(tt()) -> c_40() 982.99/297.07 , proper^#(0()) -> c_49() } 982.99/297.07 Obligation: 982.99/297.07 runtime complexity 982.99/297.07 Answer: 982.99/297.07 MAYBE 982.99/297.07 982.99/297.07 Empty strict component of the problem is NOT empty. 982.99/297.07 982.99/297.07 982.99/297.07 Arrrr.. 983.30/297.28 EOF