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