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