MAYBE 919.71/297.26 MAYBE 919.71/297.26 919.71/297.26 We are left with following problem, upon which TcT provides the 919.71/297.26 certificate MAYBE. 919.71/297.26 919.71/297.26 Strict Trs: 919.71/297.26 { U11(tt(), V1, V2) -> U12(isNat(activate(V1)), activate(V2)) 919.71/297.26 , U12(tt(), V2) -> U13(isNat(activate(V2))) 919.71/297.26 , isNat(X) -> n__isNat(X) 919.71/297.26 , isNat(n__0()) -> tt() 919.71/297.26 , isNat(n__plus(V1, V2)) -> 919.71/297.26 U11(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 919.71/297.26 activate(V1), 919.71/297.26 activate(V2)) 919.71/297.26 , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) 919.71/297.26 , isNat(n__x(V1, V2)) -> 919.71/297.26 U31(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 919.71/297.26 activate(V1), 919.71/297.26 activate(V2)) 919.71/297.26 , activate(X) -> X 919.71/297.26 , activate(n__0()) -> 0() 919.71/297.26 , activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)) 919.71/297.26 , activate(n__isNatKind(X)) -> isNatKind(X) 919.71/297.26 , activate(n__s(X)) -> s(activate(X)) 919.71/297.26 , activate(n__x(X1, X2)) -> x(activate(X1), activate(X2)) 919.71/297.26 , activate(n__and(X1, X2)) -> and(activate(X1), X2) 919.71/297.26 , activate(n__isNat(X)) -> isNat(X) 919.71/297.26 , U13(tt()) -> tt() 919.71/297.26 , U21(tt(), V1) -> U22(isNat(activate(V1))) 919.71/297.26 , U22(tt()) -> tt() 919.71/297.26 , U31(tt(), V1, V2) -> U32(isNat(activate(V1)), activate(V2)) 919.71/297.26 , U32(tt(), V2) -> U33(isNat(activate(V2))) 919.71/297.26 , U33(tt()) -> tt() 919.71/297.26 , U41(tt(), N) -> activate(N) 919.71/297.26 , U51(tt(), M, N) -> s(plus(activate(N), activate(M))) 919.71/297.26 , s(X) -> n__s(X) 919.71/297.26 , plus(X1, X2) -> n__plus(X1, X2) 919.71/297.26 , plus(N, s(M)) -> 919.71/297.26 U51(and(and(isNat(M), n__isNatKind(M)), 919.71/297.26 n__and(n__isNat(N), n__isNatKind(N))), 919.71/297.26 M, 919.71/297.26 N) 919.71/297.26 , plus(N, 0()) -> U41(and(isNat(N), n__isNatKind(N)), N) 919.71/297.26 , U61(tt()) -> 0() 919.71/297.26 , 0() -> n__0() 919.71/297.26 , U71(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N)) 919.71/297.26 , x(X1, X2) -> n__x(X1, X2) 919.71/297.26 , x(N, s(M)) -> 919.71/297.26 U71(and(and(isNat(M), n__isNatKind(M)), 919.71/297.26 n__and(n__isNat(N), n__isNatKind(N))), 919.71/297.26 M, 919.71/297.26 N) 919.71/297.26 , x(N, 0()) -> U61(and(isNat(N), n__isNatKind(N))) 919.71/297.26 , and(X1, X2) -> n__and(X1, X2) 919.71/297.26 , and(tt(), X) -> activate(X) 919.71/297.26 , isNatKind(X) -> n__isNatKind(X) 919.71/297.26 , isNatKind(n__0()) -> tt() 919.71/297.26 , isNatKind(n__plus(V1, V2)) -> 919.71/297.26 and(isNatKind(activate(V1)), n__isNatKind(activate(V2))) 919.71/297.26 , isNatKind(n__s(V1)) -> isNatKind(activate(V1)) 919.71/297.26 , isNatKind(n__x(V1, V2)) -> 919.71/297.26 and(isNatKind(activate(V1)), n__isNatKind(activate(V2))) } 919.71/297.26 Obligation: 919.71/297.26 runtime complexity 919.71/297.26 Answer: 919.71/297.26 MAYBE 919.71/297.26 919.71/297.26 None of the processors succeeded. 919.71/297.26 919.71/297.26 Details of failed attempt(s): 919.71/297.26 ----------------------------- 919.71/297.26 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 919.71/297.26 following reason: 919.71/297.26 919.71/297.26 Computation stopped due to timeout after 297.0 seconds. 919.71/297.26 919.71/297.26 2) 'Best' failed due to the following reason: 919.71/297.26 919.71/297.26 None of the processors succeeded. 919.71/297.26 919.71/297.26 Details of failed attempt(s): 919.71/297.26 ----------------------------- 919.71/297.26 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 919.71/297.26 seconds)' failed due to the following reason: 919.71/297.26 919.71/297.26 Computation stopped due to timeout after 148.0 seconds. 919.71/297.26 919.71/297.26 2) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 919.71/297.26 failed due to the following reason: 919.71/297.26 919.71/297.26 None of the processors succeeded. 919.71/297.26 919.71/297.26 Details of failed attempt(s): 919.71/297.26 ----------------------------- 919.71/297.26 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 919.71/297.26 failed due to the following reason: 919.71/297.26 919.71/297.26 match-boundness of the problem could not be verified. 919.71/297.26 919.71/297.26 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 919.71/297.26 failed due to the following reason: 919.71/297.26 919.71/297.26 match-boundness of the problem could not be verified. 919.71/297.26 919.71/297.26 919.71/297.26 3) 'Best' failed due to the following reason: 919.71/297.26 919.71/297.26 None of the processors succeeded. 919.71/297.26 919.71/297.26 Details of failed attempt(s): 919.71/297.26 ----------------------------- 919.71/297.26 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 919.71/297.26 following reason: 919.71/297.26 919.71/297.26 The processor is inapplicable, reason: 919.71/297.26 Processor only applicable for innermost runtime complexity analysis 919.71/297.26 919.71/297.26 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 919.71/297.26 to the following reason: 919.71/297.26 919.71/297.26 The processor is inapplicable, reason: 919.71/297.26 Processor only applicable for innermost runtime complexity analysis 919.71/297.26 919.71/297.26 919.71/297.26 919.71/297.26 3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 919.71/297.26 the following reason: 919.71/297.26 919.71/297.26 We add the following weak dependency pairs: 919.71/297.26 919.71/297.26 Strict DPs: 919.71/297.26 { U11^#(tt(), V1, V2) -> 919.71/297.26 c_1(U12^#(isNat(activate(V1)), activate(V2))) 919.71/297.26 , U12^#(tt(), V2) -> c_2(U13^#(isNat(activate(V2)))) 919.71/297.26 , U13^#(tt()) -> c_16() 919.71/297.26 , isNat^#(X) -> c_3(X) 919.71/297.26 , isNat^#(n__0()) -> c_4() 919.71/297.26 , isNat^#(n__plus(V1, V2)) -> 919.71/297.26 c_5(U11^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 919.71/297.26 activate(V1), 919.71/297.26 activate(V2))) 919.71/297.26 , isNat^#(n__s(V1)) -> 919.71/297.26 c_6(U21^#(isNatKind(activate(V1)), activate(V1))) 919.71/297.26 , isNat^#(n__x(V1, V2)) -> 919.71/297.26 c_7(U31^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 919.71/297.26 activate(V1), 919.71/297.26 activate(V2))) 919.71/297.26 , U21^#(tt(), V1) -> c_17(U22^#(isNat(activate(V1)))) 919.71/297.26 , U31^#(tt(), V1, V2) -> 919.71/297.26 c_19(U32^#(isNat(activate(V1)), activate(V2))) 919.71/297.26 , activate^#(X) -> c_8(X) 919.71/297.26 , activate^#(n__0()) -> c_9(0^#()) 919.71/297.26 , activate^#(n__plus(X1, X2)) -> 919.71/297.26 c_10(plus^#(activate(X1), activate(X2))) 919.71/297.26 , activate^#(n__isNatKind(X)) -> c_11(isNatKind^#(X)) 919.71/297.26 , activate^#(n__s(X)) -> c_12(s^#(activate(X))) 919.71/297.26 , activate^#(n__x(X1, X2)) -> c_13(x^#(activate(X1), activate(X2))) 919.71/297.26 , activate^#(n__and(X1, X2)) -> c_14(and^#(activate(X1), X2)) 919.71/297.26 , activate^#(n__isNat(X)) -> c_15(isNat^#(X)) 919.71/297.26 , 0^#() -> c_29() 919.71/297.26 , plus^#(X1, X2) -> c_25(X1, X2) 919.71/297.26 , plus^#(N, s(M)) -> 919.71/297.26 c_26(U51^#(and(and(isNat(M), n__isNatKind(M)), 919.71/297.26 n__and(n__isNat(N), n__isNatKind(N))), 919.71/297.26 M, 919.71/297.26 N)) 919.71/297.26 , plus^#(N, 0()) -> c_27(U41^#(and(isNat(N), n__isNatKind(N)), N)) 919.71/297.26 , isNatKind^#(X) -> c_36(X) 919.71/297.26 , isNatKind^#(n__0()) -> c_37() 919.71/297.26 , isNatKind^#(n__plus(V1, V2)) -> 919.71/297.26 c_38(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2)))) 919.71/297.26 , isNatKind^#(n__s(V1)) -> c_39(isNatKind^#(activate(V1))) 919.71/297.26 , isNatKind^#(n__x(V1, V2)) -> 919.71/297.26 c_40(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2)))) 919.71/297.26 , s^#(X) -> c_24(X) 919.71/297.26 , x^#(X1, X2) -> c_31(X1, X2) 919.71/297.26 , x^#(N, s(M)) -> 919.71/297.26 c_32(U71^#(and(and(isNat(M), n__isNatKind(M)), 919.71/297.26 n__and(n__isNat(N), n__isNatKind(N))), 919.71/297.26 M, 919.71/297.26 N)) 919.71/297.26 , x^#(N, 0()) -> c_33(U61^#(and(isNat(N), n__isNatKind(N)))) 919.71/297.26 , and^#(X1, X2) -> c_34(X1, X2) 919.71/297.26 , and^#(tt(), X) -> c_35(activate^#(X)) 919.71/297.26 , U22^#(tt()) -> c_18() 919.71/297.26 , U32^#(tt(), V2) -> c_20(U33^#(isNat(activate(V2)))) 919.71/297.26 , U33^#(tt()) -> c_21() 919.71/297.26 , U41^#(tt(), N) -> c_22(activate^#(N)) 919.71/297.26 , U51^#(tt(), M, N) -> c_23(s^#(plus(activate(N), activate(M)))) 919.71/297.26 , U61^#(tt()) -> c_28(0^#()) 919.71/297.26 , U71^#(tt(), M, N) -> 919.71/297.26 c_30(plus^#(x(activate(N), activate(M)), activate(N))) } 919.71/297.26 919.71/297.26 and mark the set of starting terms. 919.71/297.26 919.71/297.26 We are left with following problem, upon which TcT provides the 919.71/297.26 certificate MAYBE. 919.71/297.26 919.71/297.26 Strict DPs: 919.71/297.26 { U11^#(tt(), V1, V2) -> 919.71/297.26 c_1(U12^#(isNat(activate(V1)), activate(V2))) 919.71/297.26 , U12^#(tt(), V2) -> c_2(U13^#(isNat(activate(V2)))) 919.71/297.26 , U13^#(tt()) -> c_16() 919.71/297.26 , isNat^#(X) -> c_3(X) 919.71/297.26 , isNat^#(n__0()) -> c_4() 919.71/297.26 , isNat^#(n__plus(V1, V2)) -> 919.71/297.26 c_5(U11^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 919.71/297.26 activate(V1), 919.71/297.26 activate(V2))) 919.71/297.26 , isNat^#(n__s(V1)) -> 919.71/297.26 c_6(U21^#(isNatKind(activate(V1)), activate(V1))) 919.71/297.26 , isNat^#(n__x(V1, V2)) -> 919.71/297.26 c_7(U31^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 919.71/297.26 activate(V1), 919.71/297.26 activate(V2))) 919.71/297.26 , U21^#(tt(), V1) -> c_17(U22^#(isNat(activate(V1)))) 919.71/297.26 , U31^#(tt(), V1, V2) -> 919.71/297.26 c_19(U32^#(isNat(activate(V1)), activate(V2))) 919.71/297.26 , activate^#(X) -> c_8(X) 919.71/297.26 , activate^#(n__0()) -> c_9(0^#()) 919.71/297.26 , activate^#(n__plus(X1, X2)) -> 919.71/297.26 c_10(plus^#(activate(X1), activate(X2))) 919.71/297.26 , activate^#(n__isNatKind(X)) -> c_11(isNatKind^#(X)) 919.71/297.26 , activate^#(n__s(X)) -> c_12(s^#(activate(X))) 919.71/297.26 , activate^#(n__x(X1, X2)) -> c_13(x^#(activate(X1), activate(X2))) 919.71/297.26 , activate^#(n__and(X1, X2)) -> c_14(and^#(activate(X1), X2)) 919.71/297.26 , activate^#(n__isNat(X)) -> c_15(isNat^#(X)) 919.71/297.26 , 0^#() -> c_29() 919.71/297.26 , plus^#(X1, X2) -> c_25(X1, X2) 919.71/297.26 , plus^#(N, s(M)) -> 919.71/297.26 c_26(U51^#(and(and(isNat(M), n__isNatKind(M)), 919.71/297.26 n__and(n__isNat(N), n__isNatKind(N))), 919.71/297.26 M, 919.71/297.26 N)) 919.71/297.26 , plus^#(N, 0()) -> c_27(U41^#(and(isNat(N), n__isNatKind(N)), N)) 919.71/297.26 , isNatKind^#(X) -> c_36(X) 919.71/297.26 , isNatKind^#(n__0()) -> c_37() 919.71/297.26 , isNatKind^#(n__plus(V1, V2)) -> 919.71/297.26 c_38(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2)))) 919.71/297.26 , isNatKind^#(n__s(V1)) -> c_39(isNatKind^#(activate(V1))) 919.71/297.26 , isNatKind^#(n__x(V1, V2)) -> 919.71/297.26 c_40(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2)))) 919.71/297.26 , s^#(X) -> c_24(X) 919.71/297.26 , x^#(X1, X2) -> c_31(X1, X2) 919.71/297.26 , x^#(N, s(M)) -> 919.71/297.26 c_32(U71^#(and(and(isNat(M), n__isNatKind(M)), 919.71/297.26 n__and(n__isNat(N), n__isNatKind(N))), 919.71/297.26 M, 919.71/297.26 N)) 919.71/297.26 , x^#(N, 0()) -> c_33(U61^#(and(isNat(N), n__isNatKind(N)))) 919.71/297.26 , and^#(X1, X2) -> c_34(X1, X2) 919.71/297.26 , and^#(tt(), X) -> c_35(activate^#(X)) 919.71/297.26 , U22^#(tt()) -> c_18() 919.71/297.26 , U32^#(tt(), V2) -> c_20(U33^#(isNat(activate(V2)))) 919.71/297.26 , U33^#(tt()) -> c_21() 919.71/297.26 , U41^#(tt(), N) -> c_22(activate^#(N)) 919.71/297.26 , U51^#(tt(), M, N) -> c_23(s^#(plus(activate(N), activate(M)))) 919.71/297.26 , U61^#(tt()) -> c_28(0^#()) 919.71/297.26 , U71^#(tt(), M, N) -> 919.71/297.26 c_30(plus^#(x(activate(N), activate(M)), activate(N))) } 919.71/297.26 Strict Trs: 919.71/297.26 { U11(tt(), V1, V2) -> U12(isNat(activate(V1)), activate(V2)) 919.71/297.26 , U12(tt(), V2) -> U13(isNat(activate(V2))) 919.71/297.26 , isNat(X) -> n__isNat(X) 919.71/297.26 , isNat(n__0()) -> tt() 919.71/297.26 , isNat(n__plus(V1, V2)) -> 919.71/297.26 U11(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 919.71/297.26 activate(V1), 919.71/297.26 activate(V2)) 919.71/297.26 , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) 919.71/297.26 , isNat(n__x(V1, V2)) -> 919.71/297.26 U31(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 919.71/297.26 activate(V1), 919.71/297.26 activate(V2)) 919.71/297.26 , activate(X) -> X 919.71/297.26 , activate(n__0()) -> 0() 919.71/297.26 , activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)) 919.71/297.26 , activate(n__isNatKind(X)) -> isNatKind(X) 919.71/297.26 , activate(n__s(X)) -> s(activate(X)) 919.71/297.26 , activate(n__x(X1, X2)) -> x(activate(X1), activate(X2)) 919.71/297.26 , activate(n__and(X1, X2)) -> and(activate(X1), X2) 919.71/297.26 , activate(n__isNat(X)) -> isNat(X) 919.71/297.26 , U13(tt()) -> tt() 919.71/297.26 , U21(tt(), V1) -> U22(isNat(activate(V1))) 919.71/297.26 , U22(tt()) -> tt() 919.71/297.26 , U31(tt(), V1, V2) -> U32(isNat(activate(V1)), activate(V2)) 919.71/297.26 , U32(tt(), V2) -> U33(isNat(activate(V2))) 919.71/297.26 , U33(tt()) -> tt() 919.71/297.26 , U41(tt(), N) -> activate(N) 919.71/297.26 , U51(tt(), M, N) -> s(plus(activate(N), activate(M))) 919.71/297.26 , s(X) -> n__s(X) 919.71/297.26 , plus(X1, X2) -> n__plus(X1, X2) 919.71/297.26 , plus(N, s(M)) -> 919.71/297.26 U51(and(and(isNat(M), n__isNatKind(M)), 919.71/297.26 n__and(n__isNat(N), n__isNatKind(N))), 919.71/297.26 M, 919.71/297.26 N) 919.71/297.26 , plus(N, 0()) -> U41(and(isNat(N), n__isNatKind(N)), N) 919.71/297.26 , U61(tt()) -> 0() 919.71/297.26 , 0() -> n__0() 919.71/297.26 , U71(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N)) 919.71/297.26 , x(X1, X2) -> n__x(X1, X2) 919.71/297.26 , x(N, s(M)) -> 919.71/297.26 U71(and(and(isNat(M), n__isNatKind(M)), 919.71/297.26 n__and(n__isNat(N), n__isNatKind(N))), 919.71/297.26 M, 919.71/297.26 N) 919.71/297.26 , x(N, 0()) -> U61(and(isNat(N), n__isNatKind(N))) 919.71/297.26 , and(X1, X2) -> n__and(X1, X2) 919.71/297.26 , and(tt(), X) -> activate(X) 919.71/297.26 , isNatKind(X) -> n__isNatKind(X) 919.71/297.26 , isNatKind(n__0()) -> tt() 919.71/297.26 , isNatKind(n__plus(V1, V2)) -> 919.71/297.26 and(isNatKind(activate(V1)), n__isNatKind(activate(V2))) 919.71/297.26 , isNatKind(n__s(V1)) -> isNatKind(activate(V1)) 919.71/297.26 , isNatKind(n__x(V1, V2)) -> 919.71/297.26 and(isNatKind(activate(V1)), n__isNatKind(activate(V2))) } 919.71/297.26 Obligation: 919.71/297.26 runtime complexity 919.71/297.26 Answer: 919.71/297.26 MAYBE 919.71/297.26 919.71/297.26 We estimate the number of application of {3,5,19,24,34,36} by 919.71/297.26 applications of Pre({3,5,19,24,34,36}) = 919.71/297.26 {2,4,9,11,12,14,18,20,23,26,28,29,32,35,39}. Here rules are labeled 919.71/297.26 as follows: 919.71/297.26 919.71/297.26 DPs: 919.71/297.26 { 1: U11^#(tt(), V1, V2) -> 919.71/297.26 c_1(U12^#(isNat(activate(V1)), activate(V2))) 919.71/297.26 , 2: U12^#(tt(), V2) -> c_2(U13^#(isNat(activate(V2)))) 919.71/297.26 , 3: U13^#(tt()) -> c_16() 919.71/297.26 , 4: isNat^#(X) -> c_3(X) 919.71/297.26 , 5: isNat^#(n__0()) -> c_4() 919.71/297.26 , 6: isNat^#(n__plus(V1, V2)) -> 919.71/297.26 c_5(U11^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 919.71/297.26 activate(V1), 919.71/297.26 activate(V2))) 919.71/297.26 , 7: isNat^#(n__s(V1)) -> 919.71/297.26 c_6(U21^#(isNatKind(activate(V1)), activate(V1))) 919.71/297.26 , 8: isNat^#(n__x(V1, V2)) -> 919.71/297.26 c_7(U31^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 919.71/297.26 activate(V1), 919.71/297.26 activate(V2))) 919.71/297.26 , 9: U21^#(tt(), V1) -> c_17(U22^#(isNat(activate(V1)))) 919.71/297.26 , 10: U31^#(tt(), V1, V2) -> 919.71/297.26 c_19(U32^#(isNat(activate(V1)), activate(V2))) 919.71/297.26 , 11: activate^#(X) -> c_8(X) 919.71/297.26 , 12: activate^#(n__0()) -> c_9(0^#()) 919.71/297.26 , 13: activate^#(n__plus(X1, X2)) -> 919.71/297.26 c_10(plus^#(activate(X1), activate(X2))) 919.71/297.26 , 14: activate^#(n__isNatKind(X)) -> c_11(isNatKind^#(X)) 919.71/297.26 , 15: activate^#(n__s(X)) -> c_12(s^#(activate(X))) 919.71/297.26 , 16: activate^#(n__x(X1, X2)) -> 919.71/297.26 c_13(x^#(activate(X1), activate(X2))) 919.71/297.26 , 17: activate^#(n__and(X1, X2)) -> c_14(and^#(activate(X1), X2)) 919.71/297.26 , 18: activate^#(n__isNat(X)) -> c_15(isNat^#(X)) 919.71/297.26 , 19: 0^#() -> c_29() 919.71/297.26 , 20: plus^#(X1, X2) -> c_25(X1, X2) 919.71/297.26 , 21: plus^#(N, s(M)) -> 919.71/297.26 c_26(U51^#(and(and(isNat(M), n__isNatKind(M)), 919.71/297.26 n__and(n__isNat(N), n__isNatKind(N))), 919.71/297.26 M, 919.71/297.26 N)) 919.71/297.26 , 22: plus^#(N, 0()) -> 919.71/297.26 c_27(U41^#(and(isNat(N), n__isNatKind(N)), N)) 919.71/297.26 , 23: isNatKind^#(X) -> c_36(X) 919.71/297.26 , 24: isNatKind^#(n__0()) -> c_37() 919.71/297.26 , 25: isNatKind^#(n__plus(V1, V2)) -> 919.71/297.26 c_38(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2)))) 919.71/297.26 , 26: isNatKind^#(n__s(V1)) -> c_39(isNatKind^#(activate(V1))) 919.71/297.26 , 27: isNatKind^#(n__x(V1, V2)) -> 919.71/297.26 c_40(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2)))) 919.71/297.26 , 28: s^#(X) -> c_24(X) 919.71/297.26 , 29: x^#(X1, X2) -> c_31(X1, X2) 919.71/297.26 , 30: x^#(N, s(M)) -> 919.71/297.26 c_32(U71^#(and(and(isNat(M), n__isNatKind(M)), 919.71/297.26 n__and(n__isNat(N), n__isNatKind(N))), 919.71/297.26 M, 919.71/297.26 N)) 919.71/297.26 , 31: x^#(N, 0()) -> c_33(U61^#(and(isNat(N), n__isNatKind(N)))) 919.71/297.26 , 32: and^#(X1, X2) -> c_34(X1, X2) 919.71/297.26 , 33: and^#(tt(), X) -> c_35(activate^#(X)) 919.71/297.26 , 34: U22^#(tt()) -> c_18() 919.71/297.26 , 35: U32^#(tt(), V2) -> c_20(U33^#(isNat(activate(V2)))) 919.71/297.26 , 36: U33^#(tt()) -> c_21() 919.71/297.26 , 37: U41^#(tt(), N) -> c_22(activate^#(N)) 919.71/297.26 , 38: U51^#(tt(), M, N) -> 919.71/297.26 c_23(s^#(plus(activate(N), activate(M)))) 919.71/297.26 , 39: U61^#(tt()) -> c_28(0^#()) 919.71/297.26 , 40: U71^#(tt(), M, N) -> 919.71/297.26 c_30(plus^#(x(activate(N), activate(M)), activate(N))) } 919.71/297.26 919.71/297.26 We are left with following problem, upon which TcT provides the 919.71/297.26 certificate MAYBE. 919.71/297.26 919.71/297.26 Strict DPs: 919.71/297.26 { U11^#(tt(), V1, V2) -> 919.71/297.26 c_1(U12^#(isNat(activate(V1)), activate(V2))) 919.71/297.26 , U12^#(tt(), V2) -> c_2(U13^#(isNat(activate(V2)))) 919.71/297.26 , isNat^#(X) -> c_3(X) 919.71/297.26 , isNat^#(n__plus(V1, V2)) -> 919.71/297.26 c_5(U11^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 919.71/297.26 activate(V1), 919.71/297.26 activate(V2))) 919.71/297.26 , isNat^#(n__s(V1)) -> 919.71/297.26 c_6(U21^#(isNatKind(activate(V1)), activate(V1))) 919.71/297.26 , isNat^#(n__x(V1, V2)) -> 919.71/297.26 c_7(U31^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 919.71/297.26 activate(V1), 919.71/297.26 activate(V2))) 919.71/297.27 , U21^#(tt(), V1) -> c_17(U22^#(isNat(activate(V1)))) 919.71/297.27 , U31^#(tt(), V1, V2) -> 919.71/297.27 c_19(U32^#(isNat(activate(V1)), activate(V2))) 919.71/297.27 , activate^#(X) -> c_8(X) 919.71/297.27 , activate^#(n__0()) -> c_9(0^#()) 919.71/297.27 , activate^#(n__plus(X1, X2)) -> 919.71/297.27 c_10(plus^#(activate(X1), activate(X2))) 919.71/297.27 , activate^#(n__isNatKind(X)) -> c_11(isNatKind^#(X)) 919.71/297.27 , activate^#(n__s(X)) -> c_12(s^#(activate(X))) 919.71/297.27 , activate^#(n__x(X1, X2)) -> c_13(x^#(activate(X1), activate(X2))) 919.71/297.27 , activate^#(n__and(X1, X2)) -> c_14(and^#(activate(X1), X2)) 919.71/297.27 , activate^#(n__isNat(X)) -> c_15(isNat^#(X)) 919.71/297.27 , plus^#(X1, X2) -> c_25(X1, X2) 919.71/297.27 , plus^#(N, s(M)) -> 919.71/297.27 c_26(U51^#(and(and(isNat(M), n__isNatKind(M)), 919.71/297.27 n__and(n__isNat(N), n__isNatKind(N))), 919.71/297.27 M, 919.71/297.27 N)) 919.71/297.27 , plus^#(N, 0()) -> c_27(U41^#(and(isNat(N), n__isNatKind(N)), N)) 919.71/297.27 , isNatKind^#(X) -> c_36(X) 919.71/297.27 , isNatKind^#(n__plus(V1, V2)) -> 919.71/297.27 c_38(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2)))) 919.71/297.27 , isNatKind^#(n__s(V1)) -> c_39(isNatKind^#(activate(V1))) 919.71/297.27 , isNatKind^#(n__x(V1, V2)) -> 919.71/297.27 c_40(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2)))) 919.71/297.27 , s^#(X) -> c_24(X) 919.71/297.27 , x^#(X1, X2) -> c_31(X1, X2) 919.71/297.27 , x^#(N, s(M)) -> 919.71/297.27 c_32(U71^#(and(and(isNat(M), n__isNatKind(M)), 919.71/297.27 n__and(n__isNat(N), n__isNatKind(N))), 919.71/297.27 M, 919.71/297.27 N)) 919.71/297.27 , x^#(N, 0()) -> c_33(U61^#(and(isNat(N), n__isNatKind(N)))) 919.71/297.27 , and^#(X1, X2) -> c_34(X1, X2) 919.71/297.27 , and^#(tt(), X) -> c_35(activate^#(X)) 919.71/297.27 , U32^#(tt(), V2) -> c_20(U33^#(isNat(activate(V2)))) 919.71/297.27 , U41^#(tt(), N) -> c_22(activate^#(N)) 919.71/297.27 , U51^#(tt(), M, N) -> c_23(s^#(plus(activate(N), activate(M)))) 919.71/297.27 , U61^#(tt()) -> c_28(0^#()) 919.71/297.27 , U71^#(tt(), M, N) -> 919.71/297.27 c_30(plus^#(x(activate(N), activate(M)), activate(N))) } 919.71/297.27 Strict Trs: 919.71/297.27 { U11(tt(), V1, V2) -> U12(isNat(activate(V1)), activate(V2)) 919.71/297.27 , U12(tt(), V2) -> U13(isNat(activate(V2))) 919.71/297.27 , isNat(X) -> n__isNat(X) 919.71/297.27 , isNat(n__0()) -> tt() 919.71/297.27 , isNat(n__plus(V1, V2)) -> 919.71/297.27 U11(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 919.71/297.27 activate(V1), 919.71/297.27 activate(V2)) 919.71/297.27 , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) 919.71/297.27 , isNat(n__x(V1, V2)) -> 919.71/297.27 U31(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 919.71/297.27 activate(V1), 919.71/297.27 activate(V2)) 919.71/297.27 , activate(X) -> X 919.71/297.27 , activate(n__0()) -> 0() 919.71/297.27 , activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)) 919.71/297.27 , activate(n__isNatKind(X)) -> isNatKind(X) 919.71/297.27 , activate(n__s(X)) -> s(activate(X)) 919.71/297.27 , activate(n__x(X1, X2)) -> x(activate(X1), activate(X2)) 919.71/297.27 , activate(n__and(X1, X2)) -> and(activate(X1), X2) 919.71/297.27 , activate(n__isNat(X)) -> isNat(X) 919.71/297.27 , U13(tt()) -> tt() 919.71/297.27 , U21(tt(), V1) -> U22(isNat(activate(V1))) 919.71/297.27 , U22(tt()) -> tt() 919.71/297.27 , U31(tt(), V1, V2) -> U32(isNat(activate(V1)), activate(V2)) 919.71/297.27 , U32(tt(), V2) -> U33(isNat(activate(V2))) 919.71/297.27 , U33(tt()) -> tt() 919.71/297.27 , U41(tt(), N) -> activate(N) 919.71/297.27 , U51(tt(), M, N) -> s(plus(activate(N), activate(M))) 919.71/297.27 , s(X) -> n__s(X) 919.71/297.27 , plus(X1, X2) -> n__plus(X1, X2) 919.71/297.27 , plus(N, s(M)) -> 919.71/297.27 U51(and(and(isNat(M), n__isNatKind(M)), 919.71/297.27 n__and(n__isNat(N), n__isNatKind(N))), 919.71/297.27 M, 919.71/297.27 N) 919.71/297.27 , plus(N, 0()) -> U41(and(isNat(N), n__isNatKind(N)), N) 919.71/297.27 , U61(tt()) -> 0() 919.71/297.27 , 0() -> n__0() 919.71/297.27 , U71(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N)) 919.71/297.27 , x(X1, X2) -> n__x(X1, X2) 919.71/297.27 , x(N, s(M)) -> 919.71/297.27 U71(and(and(isNat(M), n__isNatKind(M)), 919.71/297.27 n__and(n__isNat(N), n__isNatKind(N))), 919.71/297.27 M, 919.71/297.27 N) 919.71/297.27 , x(N, 0()) -> U61(and(isNat(N), n__isNatKind(N))) 919.71/297.27 , and(X1, X2) -> n__and(X1, X2) 919.71/297.27 , and(tt(), X) -> activate(X) 919.71/297.27 , isNatKind(X) -> n__isNatKind(X) 919.71/297.27 , isNatKind(n__0()) -> tt() 919.71/297.27 , isNatKind(n__plus(V1, V2)) -> 919.71/297.27 and(isNatKind(activate(V1)), n__isNatKind(activate(V2))) 919.71/297.27 , isNatKind(n__s(V1)) -> isNatKind(activate(V1)) 919.71/297.27 , isNatKind(n__x(V1, V2)) -> 919.71/297.27 and(isNatKind(activate(V1)), n__isNatKind(activate(V2))) } 919.71/297.27 Weak DPs: 919.71/297.27 { U13^#(tt()) -> c_16() 919.71/297.27 , isNat^#(n__0()) -> c_4() 919.71/297.27 , 0^#() -> c_29() 919.71/297.27 , isNatKind^#(n__0()) -> c_37() 919.71/297.27 , U22^#(tt()) -> c_18() 919.71/297.27 , U33^#(tt()) -> c_21() } 919.71/297.27 Obligation: 919.71/297.27 runtime complexity 919.71/297.27 Answer: 919.71/297.27 MAYBE 919.71/297.27 919.71/297.27 We estimate the number of application of {2,7,10,30,33} by 919.71/297.27 applications of Pre({2,7,10,30,33}) = 919.71/297.27 {1,3,5,8,9,17,20,24,25,27,28,29,31}. Here rules are labeled as 919.71/297.27 follows: 919.71/297.27 919.71/297.27 DPs: 919.71/297.27 { 1: U11^#(tt(), V1, V2) -> 919.71/297.27 c_1(U12^#(isNat(activate(V1)), activate(V2))) 919.71/297.27 , 2: U12^#(tt(), V2) -> c_2(U13^#(isNat(activate(V2)))) 919.71/297.27 , 3: isNat^#(X) -> c_3(X) 919.71/297.27 , 4: isNat^#(n__plus(V1, V2)) -> 919.71/297.27 c_5(U11^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 919.71/297.27 activate(V1), 919.71/297.27 activate(V2))) 919.71/297.27 , 5: isNat^#(n__s(V1)) -> 919.71/297.27 c_6(U21^#(isNatKind(activate(V1)), activate(V1))) 919.71/297.27 , 6: isNat^#(n__x(V1, V2)) -> 919.71/297.27 c_7(U31^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 919.71/297.27 activate(V1), 919.71/297.27 activate(V2))) 919.71/297.27 , 7: U21^#(tt(), V1) -> c_17(U22^#(isNat(activate(V1)))) 919.71/297.27 , 8: U31^#(tt(), V1, V2) -> 919.71/297.27 c_19(U32^#(isNat(activate(V1)), activate(V2))) 919.71/297.27 , 9: activate^#(X) -> c_8(X) 919.71/297.27 , 10: activate^#(n__0()) -> c_9(0^#()) 919.71/297.27 , 11: activate^#(n__plus(X1, X2)) -> 919.71/297.27 c_10(plus^#(activate(X1), activate(X2))) 919.71/297.27 , 12: activate^#(n__isNatKind(X)) -> c_11(isNatKind^#(X)) 919.71/297.27 , 13: activate^#(n__s(X)) -> c_12(s^#(activate(X))) 919.71/297.27 , 14: activate^#(n__x(X1, X2)) -> 919.71/297.27 c_13(x^#(activate(X1), activate(X2))) 919.71/297.27 , 15: activate^#(n__and(X1, X2)) -> c_14(and^#(activate(X1), X2)) 919.71/297.27 , 16: activate^#(n__isNat(X)) -> c_15(isNat^#(X)) 919.71/297.27 , 17: plus^#(X1, X2) -> c_25(X1, X2) 919.71/297.27 , 18: plus^#(N, s(M)) -> 919.71/297.27 c_26(U51^#(and(and(isNat(M), n__isNatKind(M)), 919.71/297.27 n__and(n__isNat(N), n__isNatKind(N))), 919.71/297.27 M, 919.71/297.27 N)) 919.71/297.27 , 19: plus^#(N, 0()) -> 919.71/297.27 c_27(U41^#(and(isNat(N), n__isNatKind(N)), N)) 919.71/297.27 , 20: isNatKind^#(X) -> c_36(X) 919.71/297.27 , 21: isNatKind^#(n__plus(V1, V2)) -> 919.71/297.27 c_38(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2)))) 919.71/297.27 , 22: isNatKind^#(n__s(V1)) -> c_39(isNatKind^#(activate(V1))) 919.71/297.27 , 23: isNatKind^#(n__x(V1, V2)) -> 919.71/297.27 c_40(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2)))) 919.71/297.27 , 24: s^#(X) -> c_24(X) 919.71/297.27 , 25: x^#(X1, X2) -> c_31(X1, X2) 919.71/297.27 , 26: x^#(N, s(M)) -> 919.71/297.27 c_32(U71^#(and(and(isNat(M), n__isNatKind(M)), 919.71/297.27 n__and(n__isNat(N), n__isNatKind(N))), 919.71/297.27 M, 919.71/297.27 N)) 919.71/297.27 , 27: x^#(N, 0()) -> c_33(U61^#(and(isNat(N), n__isNatKind(N)))) 919.71/297.27 , 28: and^#(X1, X2) -> c_34(X1, X2) 919.71/297.27 , 29: and^#(tt(), X) -> c_35(activate^#(X)) 919.71/297.27 , 30: U32^#(tt(), V2) -> c_20(U33^#(isNat(activate(V2)))) 919.71/297.27 , 31: U41^#(tt(), N) -> c_22(activate^#(N)) 919.71/297.27 , 32: U51^#(tt(), M, N) -> 919.71/297.27 c_23(s^#(plus(activate(N), activate(M)))) 919.71/297.27 , 33: U61^#(tt()) -> c_28(0^#()) 919.71/297.27 , 34: U71^#(tt(), M, N) -> 919.71/297.27 c_30(plus^#(x(activate(N), activate(M)), activate(N))) 919.71/297.27 , 35: U13^#(tt()) -> c_16() 919.71/297.27 , 36: isNat^#(n__0()) -> c_4() 919.71/297.27 , 37: 0^#() -> c_29() 919.71/297.27 , 38: isNatKind^#(n__0()) -> c_37() 919.71/297.27 , 39: U22^#(tt()) -> c_18() 919.71/297.27 , 40: U33^#(tt()) -> c_21() } 919.71/297.27 919.71/297.27 We are left with following problem, upon which TcT provides the 919.71/297.27 certificate MAYBE. 919.71/297.27 919.71/297.27 Strict DPs: 919.71/297.27 { U11^#(tt(), V1, V2) -> 919.71/297.27 c_1(U12^#(isNat(activate(V1)), activate(V2))) 919.71/297.27 , isNat^#(X) -> c_3(X) 919.71/297.27 , isNat^#(n__plus(V1, V2)) -> 919.71/297.27 c_5(U11^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 919.71/297.27 activate(V1), 919.71/297.27 activate(V2))) 919.71/297.27 , isNat^#(n__s(V1)) -> 919.71/297.27 c_6(U21^#(isNatKind(activate(V1)), activate(V1))) 919.71/297.27 , isNat^#(n__x(V1, V2)) -> 919.71/297.27 c_7(U31^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 919.71/297.27 activate(V1), 919.71/297.27 activate(V2))) 919.71/297.27 , U31^#(tt(), V1, V2) -> 919.71/297.27 c_19(U32^#(isNat(activate(V1)), activate(V2))) 919.71/297.27 , activate^#(X) -> c_8(X) 919.71/297.27 , activate^#(n__plus(X1, X2)) -> 919.71/297.27 c_10(plus^#(activate(X1), activate(X2))) 919.71/297.27 , activate^#(n__isNatKind(X)) -> c_11(isNatKind^#(X)) 919.71/297.27 , activate^#(n__s(X)) -> c_12(s^#(activate(X))) 919.71/297.27 , activate^#(n__x(X1, X2)) -> c_13(x^#(activate(X1), activate(X2))) 919.71/297.27 , activate^#(n__and(X1, X2)) -> c_14(and^#(activate(X1), X2)) 919.71/297.27 , activate^#(n__isNat(X)) -> c_15(isNat^#(X)) 919.71/297.27 , plus^#(X1, X2) -> c_25(X1, X2) 919.71/297.27 , plus^#(N, s(M)) -> 919.71/297.27 c_26(U51^#(and(and(isNat(M), n__isNatKind(M)), 919.71/297.27 n__and(n__isNat(N), n__isNatKind(N))), 919.71/297.27 M, 919.71/297.27 N)) 919.71/297.27 , plus^#(N, 0()) -> c_27(U41^#(and(isNat(N), n__isNatKind(N)), N)) 919.71/297.27 , isNatKind^#(X) -> c_36(X) 919.71/297.27 , isNatKind^#(n__plus(V1, V2)) -> 919.71/297.27 c_38(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2)))) 919.71/297.27 , isNatKind^#(n__s(V1)) -> c_39(isNatKind^#(activate(V1))) 919.71/297.27 , isNatKind^#(n__x(V1, V2)) -> 919.71/297.27 c_40(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2)))) 919.71/297.27 , s^#(X) -> c_24(X) 919.71/297.27 , x^#(X1, X2) -> c_31(X1, X2) 919.71/297.27 , x^#(N, s(M)) -> 919.71/297.27 c_32(U71^#(and(and(isNat(M), n__isNatKind(M)), 919.71/297.27 n__and(n__isNat(N), n__isNatKind(N))), 919.71/297.27 M, 919.71/297.27 N)) 919.71/297.27 , x^#(N, 0()) -> c_33(U61^#(and(isNat(N), n__isNatKind(N)))) 919.71/297.27 , and^#(X1, X2) -> c_34(X1, X2) 919.71/297.27 , and^#(tt(), X) -> c_35(activate^#(X)) 919.71/297.27 , U41^#(tt(), N) -> c_22(activate^#(N)) 919.71/297.27 , U51^#(tt(), M, N) -> c_23(s^#(plus(activate(N), activate(M)))) 919.71/297.27 , U71^#(tt(), M, N) -> 919.71/297.27 c_30(plus^#(x(activate(N), activate(M)), activate(N))) } 919.71/297.27 Strict Trs: 919.71/297.27 { U11(tt(), V1, V2) -> U12(isNat(activate(V1)), activate(V2)) 919.71/297.27 , U12(tt(), V2) -> U13(isNat(activate(V2))) 919.71/297.27 , isNat(X) -> n__isNat(X) 919.71/297.27 , isNat(n__0()) -> tt() 919.71/297.27 , isNat(n__plus(V1, V2)) -> 919.71/297.27 U11(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 919.71/297.27 activate(V1), 919.71/297.27 activate(V2)) 919.71/297.27 , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) 919.71/297.27 , isNat(n__x(V1, V2)) -> 919.71/297.27 U31(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 919.71/297.27 activate(V1), 919.71/297.27 activate(V2)) 919.71/297.27 , activate(X) -> X 919.71/297.27 , activate(n__0()) -> 0() 919.71/297.27 , activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)) 919.71/297.27 , activate(n__isNatKind(X)) -> isNatKind(X) 919.71/297.27 , activate(n__s(X)) -> s(activate(X)) 919.71/297.27 , activate(n__x(X1, X2)) -> x(activate(X1), activate(X2)) 919.71/297.27 , activate(n__and(X1, X2)) -> and(activate(X1), X2) 919.71/297.27 , activate(n__isNat(X)) -> isNat(X) 919.71/297.27 , U13(tt()) -> tt() 919.71/297.27 , U21(tt(), V1) -> U22(isNat(activate(V1))) 919.71/297.27 , U22(tt()) -> tt() 919.71/297.27 , U31(tt(), V1, V2) -> U32(isNat(activate(V1)), activate(V2)) 919.71/297.27 , U32(tt(), V2) -> U33(isNat(activate(V2))) 919.71/297.27 , U33(tt()) -> tt() 919.71/297.27 , U41(tt(), N) -> activate(N) 919.71/297.27 , U51(tt(), M, N) -> s(plus(activate(N), activate(M))) 919.71/297.27 , s(X) -> n__s(X) 919.71/297.27 , plus(X1, X2) -> n__plus(X1, X2) 919.71/297.27 , plus(N, s(M)) -> 919.71/297.27 U51(and(and(isNat(M), n__isNatKind(M)), 919.71/297.27 n__and(n__isNat(N), n__isNatKind(N))), 919.71/297.27 M, 919.71/297.27 N) 919.71/297.27 , plus(N, 0()) -> U41(and(isNat(N), n__isNatKind(N)), N) 919.71/297.27 , U61(tt()) -> 0() 919.71/297.27 , 0() -> n__0() 919.71/297.27 , U71(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N)) 919.71/297.27 , x(X1, X2) -> n__x(X1, X2) 919.71/297.27 , x(N, s(M)) -> 919.71/297.27 U71(and(and(isNat(M), n__isNatKind(M)), 919.71/297.27 n__and(n__isNat(N), n__isNatKind(N))), 919.71/297.27 M, 919.71/297.27 N) 919.71/297.27 , x(N, 0()) -> U61(and(isNat(N), n__isNatKind(N))) 919.71/297.27 , and(X1, X2) -> n__and(X1, X2) 919.71/297.27 , and(tt(), X) -> activate(X) 919.71/297.27 , isNatKind(X) -> n__isNatKind(X) 919.71/297.27 , isNatKind(n__0()) -> tt() 919.71/297.27 , isNatKind(n__plus(V1, V2)) -> 919.71/297.27 and(isNatKind(activate(V1)), n__isNatKind(activate(V2))) 919.71/297.27 , isNatKind(n__s(V1)) -> isNatKind(activate(V1)) 919.71/297.27 , isNatKind(n__x(V1, V2)) -> 919.71/297.27 and(isNatKind(activate(V1)), n__isNatKind(activate(V2))) } 919.71/297.27 Weak DPs: 919.71/297.27 { U12^#(tt(), V2) -> c_2(U13^#(isNat(activate(V2)))) 919.71/297.27 , U13^#(tt()) -> c_16() 919.71/297.27 , isNat^#(n__0()) -> c_4() 919.71/297.27 , U21^#(tt(), V1) -> c_17(U22^#(isNat(activate(V1)))) 919.71/297.27 , activate^#(n__0()) -> c_9(0^#()) 919.71/297.27 , 0^#() -> c_29() 919.71/297.27 , isNatKind^#(n__0()) -> c_37() 919.71/297.27 , U22^#(tt()) -> c_18() 919.71/297.27 , U32^#(tt(), V2) -> c_20(U33^#(isNat(activate(V2)))) 919.71/297.27 , U33^#(tt()) -> c_21() 919.71/297.27 , U61^#(tt()) -> c_28(0^#()) } 919.71/297.27 Obligation: 919.71/297.27 runtime complexity 919.71/297.27 Answer: 919.71/297.27 MAYBE 919.71/297.27 919.71/297.27 We estimate the number of application of {1,4,6,24} by applications 919.71/297.27 of Pre({1,4,6,24}) = {2,3,5,7,11,13,14,17,21,22,25}. Here rules are 919.71/297.27 labeled as follows: 919.71/297.27 919.71/297.27 DPs: 919.71/297.27 { 1: U11^#(tt(), V1, V2) -> 919.71/297.27 c_1(U12^#(isNat(activate(V1)), activate(V2))) 919.71/297.27 , 2: isNat^#(X) -> c_3(X) 919.71/297.27 , 3: isNat^#(n__plus(V1, V2)) -> 919.71/297.27 c_5(U11^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 919.71/297.27 activate(V1), 919.71/297.27 activate(V2))) 919.71/297.27 , 4: isNat^#(n__s(V1)) -> 919.71/297.27 c_6(U21^#(isNatKind(activate(V1)), activate(V1))) 919.71/297.27 , 5: isNat^#(n__x(V1, V2)) -> 919.71/297.27 c_7(U31^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 919.71/297.27 activate(V1), 919.71/297.27 activate(V2))) 919.71/297.27 , 6: U31^#(tt(), V1, V2) -> 919.71/297.27 c_19(U32^#(isNat(activate(V1)), activate(V2))) 919.71/297.27 , 7: activate^#(X) -> c_8(X) 919.71/297.27 , 8: activate^#(n__plus(X1, X2)) -> 919.71/297.27 c_10(plus^#(activate(X1), activate(X2))) 919.71/297.27 , 9: activate^#(n__isNatKind(X)) -> c_11(isNatKind^#(X)) 919.71/297.27 , 10: activate^#(n__s(X)) -> c_12(s^#(activate(X))) 919.71/297.27 , 11: activate^#(n__x(X1, X2)) -> 919.71/297.27 c_13(x^#(activate(X1), activate(X2))) 919.71/297.27 , 12: activate^#(n__and(X1, X2)) -> c_14(and^#(activate(X1), X2)) 919.71/297.27 , 13: activate^#(n__isNat(X)) -> c_15(isNat^#(X)) 919.71/297.27 , 14: plus^#(X1, X2) -> c_25(X1, X2) 919.71/297.27 , 15: plus^#(N, s(M)) -> 919.71/297.27 c_26(U51^#(and(and(isNat(M), n__isNatKind(M)), 919.71/297.27 n__and(n__isNat(N), n__isNatKind(N))), 919.71/297.27 M, 919.71/297.27 N)) 919.71/297.27 , 16: plus^#(N, 0()) -> 919.71/297.27 c_27(U41^#(and(isNat(N), n__isNatKind(N)), N)) 919.71/297.27 , 17: isNatKind^#(X) -> c_36(X) 919.71/297.27 , 18: isNatKind^#(n__plus(V1, V2)) -> 919.71/297.27 c_38(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2)))) 919.71/297.27 , 19: isNatKind^#(n__s(V1)) -> c_39(isNatKind^#(activate(V1))) 919.71/297.27 , 20: isNatKind^#(n__x(V1, V2)) -> 919.71/297.27 c_40(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2)))) 919.71/297.27 , 21: s^#(X) -> c_24(X) 919.71/297.27 , 22: x^#(X1, X2) -> c_31(X1, X2) 919.71/297.27 , 23: x^#(N, s(M)) -> 919.71/297.27 c_32(U71^#(and(and(isNat(M), n__isNatKind(M)), 919.71/297.27 n__and(n__isNat(N), n__isNatKind(N))), 919.71/297.27 M, 919.71/297.27 N)) 919.71/297.27 , 24: x^#(N, 0()) -> c_33(U61^#(and(isNat(N), n__isNatKind(N)))) 919.71/297.27 , 25: and^#(X1, X2) -> c_34(X1, X2) 919.71/297.27 , 26: and^#(tt(), X) -> c_35(activate^#(X)) 919.71/297.27 , 27: U41^#(tt(), N) -> c_22(activate^#(N)) 919.71/297.27 , 28: U51^#(tt(), M, N) -> 919.71/297.27 c_23(s^#(plus(activate(N), activate(M)))) 919.71/297.27 , 29: U71^#(tt(), M, N) -> 919.71/297.27 c_30(plus^#(x(activate(N), activate(M)), activate(N))) 919.71/297.27 , 30: U12^#(tt(), V2) -> c_2(U13^#(isNat(activate(V2)))) 919.71/297.27 , 31: U13^#(tt()) -> c_16() 919.71/297.27 , 32: isNat^#(n__0()) -> c_4() 919.71/297.27 , 33: U21^#(tt(), V1) -> c_17(U22^#(isNat(activate(V1)))) 919.71/297.27 , 34: activate^#(n__0()) -> c_9(0^#()) 919.71/297.27 , 35: 0^#() -> c_29() 919.71/297.27 , 36: isNatKind^#(n__0()) -> c_37() 919.71/297.27 , 37: U22^#(tt()) -> c_18() 919.71/297.27 , 38: U32^#(tt(), V2) -> c_20(U33^#(isNat(activate(V2)))) 919.71/297.27 , 39: U33^#(tt()) -> c_21() 919.71/297.27 , 40: U61^#(tt()) -> c_28(0^#()) } 919.71/297.27 919.71/297.27 We are left with following problem, upon which TcT provides the 919.71/297.27 certificate MAYBE. 919.71/297.27 919.71/297.27 Strict DPs: 919.71/297.27 { isNat^#(X) -> c_3(X) 919.71/297.27 , isNat^#(n__plus(V1, V2)) -> 919.71/297.27 c_5(U11^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 919.71/297.27 activate(V1), 919.71/297.27 activate(V2))) 919.71/297.27 , isNat^#(n__x(V1, V2)) -> 919.71/297.27 c_7(U31^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 919.71/297.27 activate(V1), 919.71/297.27 activate(V2))) 919.71/297.27 , activate^#(X) -> c_8(X) 919.71/297.27 , activate^#(n__plus(X1, X2)) -> 919.71/297.27 c_10(plus^#(activate(X1), activate(X2))) 919.71/297.27 , activate^#(n__isNatKind(X)) -> c_11(isNatKind^#(X)) 919.71/297.27 , activate^#(n__s(X)) -> c_12(s^#(activate(X))) 919.71/297.27 , activate^#(n__x(X1, X2)) -> c_13(x^#(activate(X1), activate(X2))) 919.71/297.27 , activate^#(n__and(X1, X2)) -> c_14(and^#(activate(X1), X2)) 919.71/297.27 , activate^#(n__isNat(X)) -> c_15(isNat^#(X)) 919.71/297.27 , plus^#(X1, X2) -> c_25(X1, X2) 919.71/297.27 , plus^#(N, s(M)) -> 919.71/297.27 c_26(U51^#(and(and(isNat(M), n__isNatKind(M)), 919.71/297.27 n__and(n__isNat(N), n__isNatKind(N))), 919.71/297.27 M, 919.71/297.27 N)) 919.71/297.27 , plus^#(N, 0()) -> c_27(U41^#(and(isNat(N), n__isNatKind(N)), N)) 919.71/297.27 , isNatKind^#(X) -> c_36(X) 919.71/297.27 , isNatKind^#(n__plus(V1, V2)) -> 919.71/297.27 c_38(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2)))) 919.71/297.27 , isNatKind^#(n__s(V1)) -> c_39(isNatKind^#(activate(V1))) 919.71/297.27 , isNatKind^#(n__x(V1, V2)) -> 919.71/297.27 c_40(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2)))) 919.71/297.27 , s^#(X) -> c_24(X) 919.71/297.27 , x^#(X1, X2) -> c_31(X1, X2) 919.71/297.27 , x^#(N, s(M)) -> 919.71/297.27 c_32(U71^#(and(and(isNat(M), n__isNatKind(M)), 919.71/297.27 n__and(n__isNat(N), n__isNatKind(N))), 919.71/297.27 M, 919.71/297.27 N)) 919.71/297.27 , and^#(X1, X2) -> c_34(X1, X2) 919.71/297.27 , and^#(tt(), X) -> c_35(activate^#(X)) 919.71/297.27 , U41^#(tt(), N) -> c_22(activate^#(N)) 919.71/297.27 , U51^#(tt(), M, N) -> c_23(s^#(plus(activate(N), activate(M)))) 919.71/297.27 , U71^#(tt(), M, N) -> 919.71/297.27 c_30(plus^#(x(activate(N), activate(M)), activate(N))) } 919.71/297.27 Strict Trs: 919.71/297.27 { U11(tt(), V1, V2) -> U12(isNat(activate(V1)), activate(V2)) 919.71/297.27 , U12(tt(), V2) -> U13(isNat(activate(V2))) 919.71/297.27 , isNat(X) -> n__isNat(X) 919.71/297.27 , isNat(n__0()) -> tt() 919.71/297.27 , isNat(n__plus(V1, V2)) -> 919.71/297.27 U11(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 919.71/297.27 activate(V1), 919.71/297.27 activate(V2)) 919.71/297.27 , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) 919.71/297.27 , isNat(n__x(V1, V2)) -> 919.71/297.27 U31(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 919.71/297.27 activate(V1), 919.71/297.27 activate(V2)) 919.71/297.27 , activate(X) -> X 919.71/297.27 , activate(n__0()) -> 0() 919.71/297.27 , activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)) 919.71/297.27 , activate(n__isNatKind(X)) -> isNatKind(X) 919.71/297.27 , activate(n__s(X)) -> s(activate(X)) 919.71/297.27 , activate(n__x(X1, X2)) -> x(activate(X1), activate(X2)) 919.71/297.27 , activate(n__and(X1, X2)) -> and(activate(X1), X2) 919.71/297.27 , activate(n__isNat(X)) -> isNat(X) 919.71/297.27 , U13(tt()) -> tt() 919.71/297.27 , U21(tt(), V1) -> U22(isNat(activate(V1))) 919.71/297.27 , U22(tt()) -> tt() 919.71/297.27 , U31(tt(), V1, V2) -> U32(isNat(activate(V1)), activate(V2)) 919.71/297.27 , U32(tt(), V2) -> U33(isNat(activate(V2))) 919.71/297.27 , U33(tt()) -> tt() 919.71/297.27 , U41(tt(), N) -> activate(N) 919.71/297.27 , U51(tt(), M, N) -> s(plus(activate(N), activate(M))) 919.71/297.27 , s(X) -> n__s(X) 919.71/297.27 , plus(X1, X2) -> n__plus(X1, X2) 919.71/297.27 , plus(N, s(M)) -> 919.71/297.27 U51(and(and(isNat(M), n__isNatKind(M)), 919.71/297.27 n__and(n__isNat(N), n__isNatKind(N))), 919.71/297.27 M, 919.71/297.27 N) 919.71/297.27 , plus(N, 0()) -> U41(and(isNat(N), n__isNatKind(N)), N) 919.71/297.27 , U61(tt()) -> 0() 919.71/297.27 , 0() -> n__0() 919.71/297.27 , U71(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N)) 919.71/297.27 , x(X1, X2) -> n__x(X1, X2) 919.71/297.27 , x(N, s(M)) -> 919.71/297.27 U71(and(and(isNat(M), n__isNatKind(M)), 919.71/297.27 n__and(n__isNat(N), n__isNatKind(N))), 919.71/297.27 M, 919.71/297.27 N) 919.71/297.27 , x(N, 0()) -> U61(and(isNat(N), n__isNatKind(N))) 919.71/297.27 , and(X1, X2) -> n__and(X1, X2) 919.71/297.27 , and(tt(), X) -> activate(X) 919.71/297.27 , isNatKind(X) -> n__isNatKind(X) 919.71/297.27 , isNatKind(n__0()) -> tt() 919.71/297.27 , isNatKind(n__plus(V1, V2)) -> 919.71/297.27 and(isNatKind(activate(V1)), n__isNatKind(activate(V2))) 919.71/297.27 , isNatKind(n__s(V1)) -> isNatKind(activate(V1)) 919.71/297.27 , isNatKind(n__x(V1, V2)) -> 919.71/297.27 and(isNatKind(activate(V1)), n__isNatKind(activate(V2))) } 919.71/297.27 Weak DPs: 919.71/297.27 { U11^#(tt(), V1, V2) -> 919.71/297.27 c_1(U12^#(isNat(activate(V1)), activate(V2))) 919.71/297.27 , U12^#(tt(), V2) -> c_2(U13^#(isNat(activate(V2)))) 919.71/297.27 , U13^#(tt()) -> c_16() 919.71/297.27 , isNat^#(n__0()) -> c_4() 919.71/297.27 , isNat^#(n__s(V1)) -> 919.71/297.27 c_6(U21^#(isNatKind(activate(V1)), activate(V1))) 919.71/297.27 , U21^#(tt(), V1) -> c_17(U22^#(isNat(activate(V1)))) 919.71/297.27 , U31^#(tt(), V1, V2) -> 919.71/297.27 c_19(U32^#(isNat(activate(V1)), activate(V2))) 919.71/297.27 , activate^#(n__0()) -> c_9(0^#()) 919.71/297.27 , 0^#() -> c_29() 919.71/297.27 , isNatKind^#(n__0()) -> c_37() 919.71/297.27 , x^#(N, 0()) -> c_33(U61^#(and(isNat(N), n__isNatKind(N)))) 919.71/297.27 , U22^#(tt()) -> c_18() 919.71/297.27 , U32^#(tt(), V2) -> c_20(U33^#(isNat(activate(V2)))) 919.71/297.27 , U33^#(tt()) -> c_21() 919.71/297.27 , U61^#(tt()) -> c_28(0^#()) } 919.71/297.27 Obligation: 919.71/297.27 runtime complexity 919.71/297.27 Answer: 919.71/297.27 MAYBE 919.71/297.27 919.71/297.27 We estimate the number of application of {2,3} by applications of 919.71/297.27 Pre({2,3}) = {1,4,10,11,14,18,19,21}. Here rules are labeled as 919.71/297.27 follows: 919.71/297.27 919.71/297.27 DPs: 919.71/297.27 { 1: isNat^#(X) -> c_3(X) 919.71/297.27 , 2: isNat^#(n__plus(V1, V2)) -> 919.71/297.27 c_5(U11^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 919.71/297.27 activate(V1), 919.71/297.27 activate(V2))) 919.71/297.27 , 3: isNat^#(n__x(V1, V2)) -> 919.71/297.27 c_7(U31^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 919.71/297.27 activate(V1), 919.71/297.27 activate(V2))) 919.71/297.27 , 4: activate^#(X) -> c_8(X) 919.71/297.27 , 5: activate^#(n__plus(X1, X2)) -> 919.71/297.27 c_10(plus^#(activate(X1), activate(X2))) 919.71/297.27 , 6: activate^#(n__isNatKind(X)) -> c_11(isNatKind^#(X)) 919.71/297.27 , 7: activate^#(n__s(X)) -> c_12(s^#(activate(X))) 919.71/297.27 , 8: activate^#(n__x(X1, X2)) -> 919.71/297.27 c_13(x^#(activate(X1), activate(X2))) 919.71/297.27 , 9: activate^#(n__and(X1, X2)) -> c_14(and^#(activate(X1), X2)) 919.71/297.27 , 10: activate^#(n__isNat(X)) -> c_15(isNat^#(X)) 919.71/297.27 , 11: plus^#(X1, X2) -> c_25(X1, X2) 919.71/297.27 , 12: plus^#(N, s(M)) -> 919.71/297.27 c_26(U51^#(and(and(isNat(M), n__isNatKind(M)), 919.71/297.27 n__and(n__isNat(N), n__isNatKind(N))), 919.71/297.27 M, 919.71/297.27 N)) 919.71/297.27 , 13: plus^#(N, 0()) -> 919.71/297.27 c_27(U41^#(and(isNat(N), n__isNatKind(N)), N)) 919.71/297.27 , 14: isNatKind^#(X) -> c_36(X) 919.71/297.27 , 15: isNatKind^#(n__plus(V1, V2)) -> 919.71/297.27 c_38(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2)))) 919.71/297.27 , 16: isNatKind^#(n__s(V1)) -> c_39(isNatKind^#(activate(V1))) 919.71/297.27 , 17: isNatKind^#(n__x(V1, V2)) -> 919.71/297.27 c_40(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2)))) 919.71/297.27 , 18: s^#(X) -> c_24(X) 919.71/297.27 , 19: x^#(X1, X2) -> c_31(X1, X2) 919.71/297.27 , 20: x^#(N, s(M)) -> 919.71/297.27 c_32(U71^#(and(and(isNat(M), n__isNatKind(M)), 919.71/297.27 n__and(n__isNat(N), n__isNatKind(N))), 919.71/297.27 M, 919.71/297.27 N)) 919.71/297.27 , 21: and^#(X1, X2) -> c_34(X1, X2) 919.71/297.27 , 22: and^#(tt(), X) -> c_35(activate^#(X)) 919.71/297.27 , 23: U41^#(tt(), N) -> c_22(activate^#(N)) 919.71/297.27 , 24: U51^#(tt(), M, N) -> 919.71/297.27 c_23(s^#(plus(activate(N), activate(M)))) 919.71/297.27 , 25: U71^#(tt(), M, N) -> 919.71/297.27 c_30(plus^#(x(activate(N), activate(M)), activate(N))) 919.71/297.27 , 26: U11^#(tt(), V1, V2) -> 919.71/297.27 c_1(U12^#(isNat(activate(V1)), activate(V2))) 919.71/297.27 , 27: U12^#(tt(), V2) -> c_2(U13^#(isNat(activate(V2)))) 919.71/297.27 , 28: U13^#(tt()) -> c_16() 919.71/297.27 , 29: isNat^#(n__0()) -> c_4() 919.71/297.27 , 30: isNat^#(n__s(V1)) -> 919.71/297.27 c_6(U21^#(isNatKind(activate(V1)), activate(V1))) 919.71/297.27 , 31: U21^#(tt(), V1) -> c_17(U22^#(isNat(activate(V1)))) 919.71/297.27 , 32: U31^#(tt(), V1, V2) -> 919.71/297.27 c_19(U32^#(isNat(activate(V1)), activate(V2))) 919.71/297.27 , 33: activate^#(n__0()) -> c_9(0^#()) 919.71/297.27 , 34: 0^#() -> c_29() 919.71/297.27 , 35: isNatKind^#(n__0()) -> c_37() 919.71/297.28 , 36: x^#(N, 0()) -> c_33(U61^#(and(isNat(N), n__isNatKind(N)))) 919.71/297.28 , 37: U22^#(tt()) -> c_18() 919.71/297.28 , 38: U32^#(tt(), V2) -> c_20(U33^#(isNat(activate(V2)))) 919.71/297.28 , 39: U33^#(tt()) -> c_21() 919.71/297.28 , 40: U61^#(tt()) -> c_28(0^#()) } 919.71/297.28 919.71/297.28 We are left with following problem, upon which TcT provides the 919.71/297.28 certificate MAYBE. 919.71/297.28 919.71/297.28 Strict DPs: 919.71/297.28 { isNat^#(X) -> c_3(X) 919.71/297.28 , activate^#(X) -> c_8(X) 919.71/297.28 , activate^#(n__plus(X1, X2)) -> 919.71/297.28 c_10(plus^#(activate(X1), activate(X2))) 919.71/297.28 , activate^#(n__isNatKind(X)) -> c_11(isNatKind^#(X)) 919.71/297.28 , activate^#(n__s(X)) -> c_12(s^#(activate(X))) 919.71/297.28 , activate^#(n__x(X1, X2)) -> c_13(x^#(activate(X1), activate(X2))) 919.71/297.28 , activate^#(n__and(X1, X2)) -> c_14(and^#(activate(X1), X2)) 919.71/297.28 , activate^#(n__isNat(X)) -> c_15(isNat^#(X)) 919.71/297.28 , plus^#(X1, X2) -> c_25(X1, X2) 919.71/297.28 , plus^#(N, s(M)) -> 919.71/297.28 c_26(U51^#(and(and(isNat(M), n__isNatKind(M)), 919.71/297.28 n__and(n__isNat(N), n__isNatKind(N))), 919.71/297.28 M, 919.71/297.28 N)) 919.71/297.28 , plus^#(N, 0()) -> c_27(U41^#(and(isNat(N), n__isNatKind(N)), N)) 919.71/297.28 , isNatKind^#(X) -> c_36(X) 919.71/297.28 , isNatKind^#(n__plus(V1, V2)) -> 919.71/297.28 c_38(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2)))) 919.71/297.28 , isNatKind^#(n__s(V1)) -> c_39(isNatKind^#(activate(V1))) 919.71/297.28 , isNatKind^#(n__x(V1, V2)) -> 919.71/297.28 c_40(and^#(isNatKind(activate(V1)), n__isNatKind(activate(V2)))) 919.71/297.28 , s^#(X) -> c_24(X) 919.71/297.28 , x^#(X1, X2) -> c_31(X1, X2) 919.71/297.28 , x^#(N, s(M)) -> 919.71/297.28 c_32(U71^#(and(and(isNat(M), n__isNatKind(M)), 919.71/297.28 n__and(n__isNat(N), n__isNatKind(N))), 919.71/297.28 M, 919.71/297.28 N)) 919.71/297.28 , and^#(X1, X2) -> c_34(X1, X2) 919.71/297.28 , and^#(tt(), X) -> c_35(activate^#(X)) 919.71/297.28 , U41^#(tt(), N) -> c_22(activate^#(N)) 919.71/297.28 , U51^#(tt(), M, N) -> c_23(s^#(plus(activate(N), activate(M)))) 919.71/297.28 , U71^#(tt(), M, N) -> 919.71/297.28 c_30(plus^#(x(activate(N), activate(M)), activate(N))) } 919.71/297.28 Strict Trs: 919.71/297.28 { U11(tt(), V1, V2) -> U12(isNat(activate(V1)), activate(V2)) 919.71/297.28 , U12(tt(), V2) -> U13(isNat(activate(V2))) 919.71/297.28 , isNat(X) -> n__isNat(X) 919.71/297.28 , isNat(n__0()) -> tt() 919.71/297.28 , isNat(n__plus(V1, V2)) -> 919.71/297.28 U11(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 919.71/297.28 activate(V1), 919.71/297.28 activate(V2)) 919.71/297.28 , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) 919.71/297.28 , isNat(n__x(V1, V2)) -> 919.71/297.28 U31(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 919.71/297.28 activate(V1), 919.71/297.28 activate(V2)) 919.71/297.28 , activate(X) -> X 919.71/297.28 , activate(n__0()) -> 0() 919.71/297.28 , activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)) 919.71/297.28 , activate(n__isNatKind(X)) -> isNatKind(X) 919.71/297.28 , activate(n__s(X)) -> s(activate(X)) 919.71/297.28 , activate(n__x(X1, X2)) -> x(activate(X1), activate(X2)) 919.71/297.28 , activate(n__and(X1, X2)) -> and(activate(X1), X2) 919.71/297.28 , activate(n__isNat(X)) -> isNat(X) 919.71/297.28 , U13(tt()) -> tt() 919.71/297.28 , U21(tt(), V1) -> U22(isNat(activate(V1))) 919.71/297.28 , U22(tt()) -> tt() 919.71/297.28 , U31(tt(), V1, V2) -> U32(isNat(activate(V1)), activate(V2)) 919.71/297.28 , U32(tt(), V2) -> U33(isNat(activate(V2))) 919.71/297.28 , U33(tt()) -> tt() 919.71/297.28 , U41(tt(), N) -> activate(N) 919.71/297.28 , U51(tt(), M, N) -> s(plus(activate(N), activate(M))) 919.71/297.28 , s(X) -> n__s(X) 919.71/297.28 , plus(X1, X2) -> n__plus(X1, X2) 919.71/297.28 , plus(N, s(M)) -> 919.71/297.28 U51(and(and(isNat(M), n__isNatKind(M)), 919.71/297.28 n__and(n__isNat(N), n__isNatKind(N))), 919.71/297.28 M, 919.71/297.28 N) 919.71/297.28 , plus(N, 0()) -> U41(and(isNat(N), n__isNatKind(N)), N) 919.71/297.28 , U61(tt()) -> 0() 919.71/297.28 , 0() -> n__0() 919.71/297.28 , U71(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N)) 919.71/297.28 , x(X1, X2) -> n__x(X1, X2) 919.71/297.28 , x(N, s(M)) -> 919.71/297.28 U71(and(and(isNat(M), n__isNatKind(M)), 919.71/297.28 n__and(n__isNat(N), n__isNatKind(N))), 919.71/297.28 M, 919.71/297.28 N) 919.71/297.28 , x(N, 0()) -> U61(and(isNat(N), n__isNatKind(N))) 919.71/297.28 , and(X1, X2) -> n__and(X1, X2) 919.71/297.28 , and(tt(), X) -> activate(X) 919.71/297.28 , isNatKind(X) -> n__isNatKind(X) 919.71/297.28 , isNatKind(n__0()) -> tt() 919.71/297.28 , isNatKind(n__plus(V1, V2)) -> 919.71/297.28 and(isNatKind(activate(V1)), n__isNatKind(activate(V2))) 919.71/297.28 , isNatKind(n__s(V1)) -> isNatKind(activate(V1)) 919.71/297.28 , isNatKind(n__x(V1, V2)) -> 919.71/297.28 and(isNatKind(activate(V1)), n__isNatKind(activate(V2))) } 919.71/297.28 Weak DPs: 919.71/297.28 { U11^#(tt(), V1, V2) -> 919.71/297.28 c_1(U12^#(isNat(activate(V1)), activate(V2))) 919.71/297.28 , U12^#(tt(), V2) -> c_2(U13^#(isNat(activate(V2)))) 919.71/297.28 , U13^#(tt()) -> c_16() 919.71/297.28 , isNat^#(n__0()) -> c_4() 919.71/297.28 , isNat^#(n__plus(V1, V2)) -> 919.71/297.28 c_5(U11^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 919.71/297.28 activate(V1), 919.71/297.28 activate(V2))) 919.71/297.28 , isNat^#(n__s(V1)) -> 919.71/297.28 c_6(U21^#(isNatKind(activate(V1)), activate(V1))) 919.71/297.28 , isNat^#(n__x(V1, V2)) -> 919.71/297.28 c_7(U31^#(and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), 919.71/297.28 activate(V1), 919.71/297.28 activate(V2))) 919.71/297.28 , U21^#(tt(), V1) -> c_17(U22^#(isNat(activate(V1)))) 919.71/297.28 , U31^#(tt(), V1, V2) -> 919.71/297.28 c_19(U32^#(isNat(activate(V1)), activate(V2))) 919.71/297.28 , activate^#(n__0()) -> c_9(0^#()) 919.71/297.28 , 0^#() -> c_29() 919.71/297.28 , isNatKind^#(n__0()) -> c_37() 919.71/297.28 , x^#(N, 0()) -> c_33(U61^#(and(isNat(N), n__isNatKind(N)))) 919.71/297.28 , U22^#(tt()) -> c_18() 919.71/297.28 , U32^#(tt(), V2) -> c_20(U33^#(isNat(activate(V2)))) 919.71/297.28 , U33^#(tt()) -> c_21() 919.71/297.28 , U61^#(tt()) -> c_28(0^#()) } 919.71/297.28 Obligation: 919.71/297.28 runtime complexity 919.71/297.28 Answer: 919.71/297.28 MAYBE 919.71/297.28 919.71/297.28 Empty strict component of the problem is NOT empty. 919.71/297.28 919.71/297.28 919.71/297.28 Arrrr.. 920.00/297.35 EOF