MAYBE 1084.46/297.12 MAYBE 1084.46/297.12 1084.46/297.12 We are left with following problem, upon which TcT provides the 1084.46/297.12 certificate MAYBE. 1084.46/297.12 1084.46/297.12 Strict Trs: 1084.46/297.12 { active(U101(X1, X2, X3)) -> U101(active(X1), X2, X3) 1084.46/297.12 , active(U101(tt(), M, N)) -> mark(U102(isNatKind(M), M, N)) 1084.46/297.12 , active(U102(X1, X2, X3)) -> U102(active(X1), X2, X3) 1084.46/297.12 , active(U102(tt(), M, N)) -> mark(U103(isNat(N), M, N)) 1084.46/297.12 , active(isNatKind(plus(V1, V2))) -> mark(U41(isNatKind(V1), V2)) 1084.46/297.12 , active(isNatKind(x(V1, V2))) -> mark(U61(isNatKind(V1), V2)) 1084.46/297.12 , active(isNatKind(s(V1))) -> mark(U51(isNatKind(V1))) 1084.46/297.12 , active(isNatKind(0())) -> mark(tt()) 1084.46/297.12 , active(U103(X1, X2, X3)) -> U103(active(X1), X2, X3) 1084.46/297.12 , active(U103(tt(), M, N)) -> mark(U104(isNatKind(N), M, N)) 1084.46/297.12 , active(isNat(plus(V1, V2))) -> mark(U11(isNatKind(V1), V1, V2)) 1084.46/297.12 , active(isNat(x(V1, V2))) -> mark(U31(isNatKind(V1), V1, V2)) 1084.46/297.12 , active(isNat(s(V1))) -> mark(U21(isNatKind(V1), V1)) 1084.46/297.12 , active(isNat(0())) -> mark(tt()) 1084.46/297.12 , active(U104(X1, X2, X3)) -> U104(active(X1), X2, X3) 1084.46/297.12 , active(U104(tt(), M, N)) -> mark(plus(x(N, M), N)) 1084.46/297.12 , active(plus(X1, X2)) -> plus(X1, active(X2)) 1084.46/297.12 , active(plus(X1, X2)) -> plus(active(X1), X2) 1084.46/297.12 , active(plus(N, s(M))) -> mark(U81(isNat(M), M, N)) 1084.46/297.12 , active(plus(N, 0())) -> mark(U71(isNat(N), N)) 1084.46/297.12 , active(x(X1, X2)) -> x(X1, active(X2)) 1084.46/297.12 , active(x(X1, X2)) -> x(active(X1), X2) 1084.46/297.12 , active(x(N, s(M))) -> mark(U101(isNat(M), M, N)) 1084.46/297.12 , active(x(N, 0())) -> mark(U91(isNat(N), N)) 1084.46/297.12 , active(U11(X1, X2, X3)) -> U11(active(X1), X2, X3) 1084.46/297.12 , active(U11(tt(), V1, V2)) -> mark(U12(isNatKind(V1), V1, V2)) 1084.46/297.12 , active(U12(X1, X2, X3)) -> U12(active(X1), X2, X3) 1084.46/297.12 , active(U12(tt(), V1, V2)) -> mark(U13(isNatKind(V2), V1, V2)) 1084.46/297.12 , active(U13(X1, X2, X3)) -> U13(active(X1), X2, X3) 1084.46/297.12 , active(U13(tt(), V1, V2)) -> mark(U14(isNatKind(V2), V1, V2)) 1084.46/297.12 , active(U14(X1, X2, X3)) -> U14(active(X1), X2, X3) 1084.46/297.12 , active(U14(tt(), V1, V2)) -> mark(U15(isNat(V1), V2)) 1084.46/297.12 , active(U15(X1, X2)) -> U15(active(X1), X2) 1084.46/297.12 , active(U15(tt(), V2)) -> mark(U16(isNat(V2))) 1084.46/297.12 , active(U16(X)) -> U16(active(X)) 1084.46/297.12 , active(U16(tt())) -> mark(tt()) 1084.46/297.12 , active(U21(X1, X2)) -> U21(active(X1), X2) 1084.46/297.12 , active(U21(tt(), V1)) -> mark(U22(isNatKind(V1), V1)) 1084.46/297.12 , active(U22(X1, X2)) -> U22(active(X1), X2) 1084.46/297.12 , active(U22(tt(), V1)) -> mark(U23(isNat(V1))) 1084.46/297.12 , active(U23(X)) -> U23(active(X)) 1084.46/297.12 , active(U23(tt())) -> mark(tt()) 1084.46/297.12 , active(U31(X1, X2, X3)) -> U31(active(X1), X2, X3) 1084.46/297.12 , active(U31(tt(), V1, V2)) -> mark(U32(isNatKind(V1), V1, V2)) 1084.46/297.12 , active(U32(X1, X2, X3)) -> U32(active(X1), X2, X3) 1084.46/297.12 , active(U32(tt(), V1, V2)) -> mark(U33(isNatKind(V2), V1, V2)) 1084.46/297.12 , active(U33(X1, X2, X3)) -> U33(active(X1), X2, X3) 1084.46/297.12 , active(U33(tt(), V1, V2)) -> mark(U34(isNatKind(V2), V1, V2)) 1084.46/297.12 , active(U34(X1, X2, X3)) -> U34(active(X1), X2, X3) 1084.46/297.12 , active(U34(tt(), V1, V2)) -> mark(U35(isNat(V1), V2)) 1084.46/297.12 , active(U35(X1, X2)) -> U35(active(X1), X2) 1084.46/297.12 , active(U35(tt(), V2)) -> mark(U36(isNat(V2))) 1084.46/297.12 , active(U36(X)) -> U36(active(X)) 1084.46/297.12 , active(U36(tt())) -> mark(tt()) 1084.46/297.12 , active(U41(X1, X2)) -> U41(active(X1), X2) 1084.46/297.12 , active(U41(tt(), V2)) -> mark(U42(isNatKind(V2))) 1084.46/297.12 , active(U42(X)) -> U42(active(X)) 1084.46/297.12 , active(U42(tt())) -> mark(tt()) 1084.46/297.12 , active(U51(X)) -> U51(active(X)) 1084.46/297.12 , active(U51(tt())) -> mark(tt()) 1084.46/297.12 , active(U61(X1, X2)) -> U61(active(X1), X2) 1084.46/297.12 , active(U61(tt(), V2)) -> mark(U62(isNatKind(V2))) 1084.46/297.12 , active(U62(X)) -> U62(active(X)) 1084.46/297.12 , active(U62(tt())) -> mark(tt()) 1084.46/297.12 , active(U71(X1, X2)) -> U71(active(X1), X2) 1084.46/297.12 , active(U71(tt(), N)) -> mark(U72(isNatKind(N), N)) 1084.46/297.12 , active(U72(X1, X2)) -> U72(active(X1), X2) 1084.46/297.12 , active(U72(tt(), N)) -> mark(N) 1084.46/297.12 , active(U81(X1, X2, X3)) -> U81(active(X1), X2, X3) 1084.46/297.12 , active(U81(tt(), M, N)) -> mark(U82(isNatKind(M), M, N)) 1084.46/297.12 , active(U82(X1, X2, X3)) -> U82(active(X1), X2, X3) 1084.46/297.12 , active(U82(tt(), M, N)) -> mark(U83(isNat(N), M, N)) 1084.46/297.12 , active(U83(X1, X2, X3)) -> U83(active(X1), X2, X3) 1084.46/297.12 , active(U83(tt(), M, N)) -> mark(U84(isNatKind(N), M, N)) 1084.46/297.12 , active(U84(X1, X2, X3)) -> U84(active(X1), X2, X3) 1084.46/297.12 , active(U84(tt(), M, N)) -> mark(s(plus(N, M))) 1084.46/297.12 , active(s(X)) -> s(active(X)) 1084.46/297.12 , active(U91(X1, X2)) -> U91(active(X1), X2) 1084.46/297.12 , active(U91(tt(), N)) -> mark(U92(isNatKind(N))) 1084.46/297.12 , active(U92(X)) -> U92(active(X)) 1084.46/297.12 , active(U92(tt())) -> mark(0()) 1084.46/297.12 , U101(mark(X1), X2, X3) -> mark(U101(X1, X2, X3)) 1084.46/297.12 , U101(ok(X1), ok(X2), ok(X3)) -> ok(U101(X1, X2, X3)) 1084.46/297.12 , U102(mark(X1), X2, X3) -> mark(U102(X1, X2, X3)) 1084.46/297.12 , U102(ok(X1), ok(X2), ok(X3)) -> ok(U102(X1, X2, X3)) 1084.46/297.12 , isNatKind(ok(X)) -> ok(isNatKind(X)) 1084.46/297.12 , U103(mark(X1), X2, X3) -> mark(U103(X1, X2, X3)) 1084.46/297.12 , U103(ok(X1), ok(X2), ok(X3)) -> ok(U103(X1, X2, X3)) 1084.46/297.12 , isNat(ok(X)) -> ok(isNat(X)) 1084.46/297.12 , U104(mark(X1), X2, X3) -> mark(U104(X1, X2, X3)) 1084.46/297.12 , U104(ok(X1), ok(X2), ok(X3)) -> ok(U104(X1, X2, X3)) 1084.46/297.12 , plus(X1, mark(X2)) -> mark(plus(X1, X2)) 1084.46/297.12 , plus(mark(X1), X2) -> mark(plus(X1, X2)) 1084.46/297.12 , plus(ok(X1), ok(X2)) -> ok(plus(X1, X2)) 1084.46/297.12 , x(X1, mark(X2)) -> mark(x(X1, X2)) 1084.46/297.12 , x(mark(X1), X2) -> mark(x(X1, X2)) 1084.46/297.12 , x(ok(X1), ok(X2)) -> ok(x(X1, X2)) 1084.46/297.12 , U11(mark(X1), X2, X3) -> mark(U11(X1, X2, X3)) 1084.46/297.12 , U11(ok(X1), ok(X2), ok(X3)) -> ok(U11(X1, X2, X3)) 1084.46/297.12 , U12(mark(X1), X2, X3) -> mark(U12(X1, X2, X3)) 1084.46/297.12 , U12(ok(X1), ok(X2), ok(X3)) -> ok(U12(X1, X2, X3)) 1084.46/297.12 , U13(mark(X1), X2, X3) -> mark(U13(X1, X2, X3)) 1084.46/297.12 , U13(ok(X1), ok(X2), ok(X3)) -> ok(U13(X1, X2, X3)) 1084.46/297.12 , U14(mark(X1), X2, X3) -> mark(U14(X1, X2, X3)) 1084.46/297.12 , U14(ok(X1), ok(X2), ok(X3)) -> ok(U14(X1, X2, X3)) 1084.46/297.12 , U15(mark(X1), X2) -> mark(U15(X1, X2)) 1084.46/297.12 , U15(ok(X1), ok(X2)) -> ok(U15(X1, X2)) 1084.46/297.12 , U16(mark(X)) -> mark(U16(X)) 1084.46/297.12 , U16(ok(X)) -> ok(U16(X)) 1084.46/297.12 , U21(mark(X1), X2) -> mark(U21(X1, X2)) 1084.46/297.12 , U21(ok(X1), ok(X2)) -> ok(U21(X1, X2)) 1084.46/297.12 , U22(mark(X1), X2) -> mark(U22(X1, X2)) 1084.46/297.12 , U22(ok(X1), ok(X2)) -> ok(U22(X1, X2)) 1084.46/297.12 , U23(mark(X)) -> mark(U23(X)) 1084.46/297.12 , U23(ok(X)) -> ok(U23(X)) 1084.46/297.12 , U31(mark(X1), X2, X3) -> mark(U31(X1, X2, X3)) 1084.46/297.12 , U31(ok(X1), ok(X2), ok(X3)) -> ok(U31(X1, X2, X3)) 1084.46/297.12 , U32(mark(X1), X2, X3) -> mark(U32(X1, X2, X3)) 1084.46/297.12 , U32(ok(X1), ok(X2), ok(X3)) -> ok(U32(X1, X2, X3)) 1084.46/297.12 , U33(mark(X1), X2, X3) -> mark(U33(X1, X2, X3)) 1084.46/297.12 , U33(ok(X1), ok(X2), ok(X3)) -> ok(U33(X1, X2, X3)) 1084.46/297.12 , U34(mark(X1), X2, X3) -> mark(U34(X1, X2, X3)) 1084.46/297.12 , U34(ok(X1), ok(X2), ok(X3)) -> ok(U34(X1, X2, X3)) 1084.46/297.12 , U35(mark(X1), X2) -> mark(U35(X1, X2)) 1084.46/297.12 , U35(ok(X1), ok(X2)) -> ok(U35(X1, X2)) 1084.46/297.12 , U36(mark(X)) -> mark(U36(X)) 1084.46/297.12 , U36(ok(X)) -> ok(U36(X)) 1084.46/297.12 , U41(mark(X1), X2) -> mark(U41(X1, X2)) 1084.46/297.12 , U41(ok(X1), ok(X2)) -> ok(U41(X1, X2)) 1084.46/297.12 , U42(mark(X)) -> mark(U42(X)) 1084.46/297.12 , U42(ok(X)) -> ok(U42(X)) 1084.46/297.12 , U51(mark(X)) -> mark(U51(X)) 1084.46/297.12 , U51(ok(X)) -> ok(U51(X)) 1084.46/297.12 , U61(mark(X1), X2) -> mark(U61(X1, X2)) 1084.46/297.12 , U61(ok(X1), ok(X2)) -> ok(U61(X1, X2)) 1084.46/297.12 , U62(mark(X)) -> mark(U62(X)) 1084.46/297.12 , U62(ok(X)) -> ok(U62(X)) 1084.46/297.12 , U71(mark(X1), X2) -> mark(U71(X1, X2)) 1084.46/297.12 , U71(ok(X1), ok(X2)) -> ok(U71(X1, X2)) 1084.46/297.12 , U72(mark(X1), X2) -> mark(U72(X1, X2)) 1084.46/297.12 , U72(ok(X1), ok(X2)) -> ok(U72(X1, X2)) 1084.46/297.12 , U81(mark(X1), X2, X3) -> mark(U81(X1, X2, X3)) 1084.46/297.12 , U81(ok(X1), ok(X2), ok(X3)) -> ok(U81(X1, X2, X3)) 1084.46/297.12 , U82(mark(X1), X2, X3) -> mark(U82(X1, X2, X3)) 1084.46/297.12 , U82(ok(X1), ok(X2), ok(X3)) -> ok(U82(X1, X2, X3)) 1084.46/297.12 , U83(mark(X1), X2, X3) -> mark(U83(X1, X2, X3)) 1084.46/297.12 , U83(ok(X1), ok(X2), ok(X3)) -> ok(U83(X1, X2, X3)) 1084.46/297.12 , U84(mark(X1), X2, X3) -> mark(U84(X1, X2, X3)) 1084.46/297.12 , U84(ok(X1), ok(X2), ok(X3)) -> ok(U84(X1, X2, X3)) 1084.46/297.12 , s(mark(X)) -> mark(s(X)) 1084.46/297.12 , s(ok(X)) -> ok(s(X)) 1084.46/297.12 , U91(mark(X1), X2) -> mark(U91(X1, X2)) 1084.46/297.12 , U91(ok(X1), ok(X2)) -> ok(U91(X1, X2)) 1084.46/297.12 , U92(mark(X)) -> mark(U92(X)) 1084.46/297.12 , U92(ok(X)) -> ok(U92(X)) 1084.46/297.12 , proper(U101(X1, X2, X3)) -> 1084.46/297.12 U101(proper(X1), proper(X2), proper(X3)) 1084.46/297.12 , proper(tt()) -> ok(tt()) 1084.46/297.12 , proper(U102(X1, X2, X3)) -> 1084.46/297.12 U102(proper(X1), proper(X2), proper(X3)) 1084.46/297.12 , proper(isNatKind(X)) -> isNatKind(proper(X)) 1084.46/297.12 , proper(U103(X1, X2, X3)) -> 1084.46/297.12 U103(proper(X1), proper(X2), proper(X3)) 1084.46/297.12 , proper(isNat(X)) -> isNat(proper(X)) 1084.46/297.12 , proper(U104(X1, X2, X3)) -> 1084.46/297.12 U104(proper(X1), proper(X2), proper(X3)) 1084.46/297.12 , proper(plus(X1, X2)) -> plus(proper(X1), proper(X2)) 1084.46/297.12 , proper(x(X1, X2)) -> x(proper(X1), proper(X2)) 1084.46/297.12 , proper(U11(X1, X2, X3)) -> 1084.46/297.13 U11(proper(X1), proper(X2), proper(X3)) 1084.46/297.13 , proper(U12(X1, X2, X3)) -> 1084.46/297.13 U12(proper(X1), proper(X2), proper(X3)) 1084.46/297.13 , proper(U13(X1, X2, X3)) -> 1084.46/297.13 U13(proper(X1), proper(X2), proper(X3)) 1084.46/297.13 , proper(U14(X1, X2, X3)) -> 1084.46/297.13 U14(proper(X1), proper(X2), proper(X3)) 1084.46/297.13 , proper(U15(X1, X2)) -> U15(proper(X1), proper(X2)) 1084.46/297.13 , proper(U16(X)) -> U16(proper(X)) 1084.46/297.13 , proper(U21(X1, X2)) -> U21(proper(X1), proper(X2)) 1084.46/297.13 , proper(U22(X1, X2)) -> U22(proper(X1), proper(X2)) 1084.46/297.13 , proper(U23(X)) -> U23(proper(X)) 1084.46/297.13 , proper(U31(X1, X2, X3)) -> 1084.46/297.13 U31(proper(X1), proper(X2), proper(X3)) 1084.46/297.13 , proper(U32(X1, X2, X3)) -> 1084.46/297.13 U32(proper(X1), proper(X2), proper(X3)) 1084.46/297.13 , proper(U33(X1, X2, X3)) -> 1084.46/297.13 U33(proper(X1), proper(X2), proper(X3)) 1084.46/297.13 , proper(U34(X1, X2, X3)) -> 1084.46/297.13 U34(proper(X1), proper(X2), proper(X3)) 1084.46/297.13 , proper(U35(X1, X2)) -> U35(proper(X1), proper(X2)) 1084.46/297.13 , proper(U36(X)) -> U36(proper(X)) 1084.46/297.13 , proper(U41(X1, X2)) -> U41(proper(X1), proper(X2)) 1084.46/297.13 , proper(U42(X)) -> U42(proper(X)) 1084.46/297.13 , proper(U51(X)) -> U51(proper(X)) 1084.46/297.13 , proper(U61(X1, X2)) -> U61(proper(X1), proper(X2)) 1084.46/297.13 , proper(U62(X)) -> U62(proper(X)) 1084.46/297.13 , proper(U71(X1, X2)) -> U71(proper(X1), proper(X2)) 1084.46/297.13 , proper(U72(X1, X2)) -> U72(proper(X1), proper(X2)) 1084.46/297.13 , proper(U81(X1, X2, X3)) -> 1084.46/297.13 U81(proper(X1), proper(X2), proper(X3)) 1084.46/297.13 , proper(U82(X1, X2, X3)) -> 1084.46/297.13 U82(proper(X1), proper(X2), proper(X3)) 1084.46/297.13 , proper(U83(X1, X2, X3)) -> 1084.46/297.13 U83(proper(X1), proper(X2), proper(X3)) 1084.46/297.13 , proper(U84(X1, X2, X3)) -> 1084.46/297.13 U84(proper(X1), proper(X2), proper(X3)) 1084.46/297.13 , proper(s(X)) -> s(proper(X)) 1084.46/297.13 , proper(U91(X1, X2)) -> U91(proper(X1), proper(X2)) 1084.46/297.13 , proper(U92(X)) -> U92(proper(X)) 1084.46/297.13 , proper(0()) -> ok(0()) 1084.46/297.13 , top(mark(X)) -> top(proper(X)) 1084.46/297.13 , top(ok(X)) -> top(active(X)) } 1084.46/297.13 Obligation: 1084.46/297.13 runtime complexity 1084.46/297.13 Answer: 1084.46/297.13 MAYBE 1084.46/297.13 1084.46/297.13 None of the processors succeeded. 1084.46/297.13 1084.46/297.13 Details of failed attempt(s): 1084.46/297.13 ----------------------------- 1084.46/297.13 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 1084.46/297.13 following reason: 1084.46/297.13 1084.46/297.13 Computation stopped due to timeout after 297.0 seconds. 1084.46/297.13 1084.46/297.13 2) 'Best' failed due to the following reason: 1084.46/297.13 1084.46/297.13 None of the processors succeeded. 1084.46/297.13 1084.46/297.13 Details of failed attempt(s): 1084.46/297.13 ----------------------------- 1084.46/297.13 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 1084.46/297.13 seconds)' failed due to the following reason: 1084.46/297.13 1084.46/297.13 Computation stopped due to timeout after 148.0 seconds. 1084.46/297.13 1084.46/297.13 2) 'Best' failed due to the following reason: 1084.46/297.13 1084.46/297.13 None of the processors succeeded. 1084.46/297.13 1084.46/297.13 Details of failed attempt(s): 1084.46/297.13 ----------------------------- 1084.46/297.13 1) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 1084.46/297.13 to the following reason: 1084.46/297.13 1084.46/297.13 The processor is inapplicable, reason: 1084.46/297.13 Processor only applicable for innermost runtime complexity analysis 1084.46/297.13 1084.46/297.13 2) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 1084.46/297.13 following reason: 1084.46/297.13 1084.46/297.13 The processor is inapplicable, reason: 1084.46/297.13 Processor only applicable for innermost runtime complexity analysis 1084.46/297.13 1084.46/297.13 1084.46/297.13 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 1084.46/297.13 failed due to the following reason: 1084.46/297.13 1084.46/297.13 None of the processors succeeded. 1084.46/297.13 1084.46/297.13 Details of failed attempt(s): 1084.46/297.13 ----------------------------- 1084.46/297.13 1) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 1084.46/297.13 failed due to the following reason: 1084.46/297.13 1084.46/297.13 match-boundness of the problem could not be verified. 1084.46/297.13 1084.46/297.13 2) 'Bounds with minimal-enrichment and initial automaton 'match'' 1084.46/297.13 failed due to the following reason: 1084.46/297.13 1084.46/297.13 match-boundness of the problem could not be verified. 1084.46/297.13 1084.46/297.13 1084.46/297.13 1084.46/297.13 3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 1084.46/297.13 the following reason: 1084.46/297.13 1084.46/297.13 We add the following weak dependency pairs: 1084.46/297.13 1084.46/297.13 Strict DPs: 1084.46/297.13 { active^#(U101(X1, X2, X3)) -> c_1(U101^#(active(X1), X2, X3)) 1084.46/297.13 , active^#(U101(tt(), M, N)) -> c_2(U102^#(isNatKind(M), M, N)) 1084.46/297.13 , active^#(U102(X1, X2, X3)) -> c_3(U102^#(active(X1), X2, X3)) 1084.46/297.13 , active^#(U102(tt(), M, N)) -> c_4(U103^#(isNat(N), M, N)) 1084.46/297.13 , active^#(isNatKind(plus(V1, V2))) -> 1084.46/297.13 c_5(U41^#(isNatKind(V1), V2)) 1084.46/297.13 , active^#(isNatKind(x(V1, V2))) -> c_6(U61^#(isNatKind(V1), V2)) 1084.46/297.13 , active^#(isNatKind(s(V1))) -> c_7(U51^#(isNatKind(V1))) 1084.46/297.13 , active^#(isNatKind(0())) -> c_8() 1084.46/297.13 , active^#(U103(X1, X2, X3)) -> c_9(U103^#(active(X1), X2, X3)) 1084.46/297.13 , active^#(U103(tt(), M, N)) -> c_10(U104^#(isNatKind(N), M, N)) 1084.46/297.13 , active^#(isNat(plus(V1, V2))) -> 1084.46/297.13 c_11(U11^#(isNatKind(V1), V1, V2)) 1084.46/297.13 , active^#(isNat(x(V1, V2))) -> c_12(U31^#(isNatKind(V1), V1, V2)) 1084.46/297.13 , active^#(isNat(s(V1))) -> c_13(U21^#(isNatKind(V1), V1)) 1084.46/297.13 , active^#(isNat(0())) -> c_14() 1084.46/297.13 , active^#(U104(X1, X2, X3)) -> c_15(U104^#(active(X1), X2, X3)) 1084.46/297.13 , active^#(U104(tt(), M, N)) -> c_16(plus^#(x(N, M), N)) 1084.46/297.13 , active^#(plus(X1, X2)) -> c_17(plus^#(X1, active(X2))) 1084.46/297.13 , active^#(plus(X1, X2)) -> c_18(plus^#(active(X1), X2)) 1084.46/297.13 , active^#(plus(N, s(M))) -> c_19(U81^#(isNat(M), M, N)) 1084.46/297.13 , active^#(plus(N, 0())) -> c_20(U71^#(isNat(N), N)) 1084.46/297.13 , active^#(x(X1, X2)) -> c_21(x^#(X1, active(X2))) 1084.46/297.13 , active^#(x(X1, X2)) -> c_22(x^#(active(X1), X2)) 1084.46/297.13 , active^#(x(N, s(M))) -> c_23(U101^#(isNat(M), M, N)) 1084.46/297.13 , active^#(x(N, 0())) -> c_24(U91^#(isNat(N), N)) 1084.46/297.13 , active^#(U11(X1, X2, X3)) -> c_25(U11^#(active(X1), X2, X3)) 1084.46/297.13 , active^#(U11(tt(), V1, V2)) -> c_26(U12^#(isNatKind(V1), V1, V2)) 1084.46/297.13 , active^#(U12(X1, X2, X3)) -> c_27(U12^#(active(X1), X2, X3)) 1084.46/297.13 , active^#(U12(tt(), V1, V2)) -> c_28(U13^#(isNatKind(V2), V1, V2)) 1084.46/297.13 , active^#(U13(X1, X2, X3)) -> c_29(U13^#(active(X1), X2, X3)) 1084.46/297.13 , active^#(U13(tt(), V1, V2)) -> c_30(U14^#(isNatKind(V2), V1, V2)) 1084.46/297.13 , active^#(U14(X1, X2, X3)) -> c_31(U14^#(active(X1), X2, X3)) 1084.46/297.13 , active^#(U14(tt(), V1, V2)) -> c_32(U15^#(isNat(V1), V2)) 1084.46/297.13 , active^#(U15(X1, X2)) -> c_33(U15^#(active(X1), X2)) 1084.46/297.13 , active^#(U15(tt(), V2)) -> c_34(U16^#(isNat(V2))) 1084.46/297.13 , active^#(U16(X)) -> c_35(U16^#(active(X))) 1084.46/297.13 , active^#(U16(tt())) -> c_36() 1084.46/297.13 , active^#(U21(X1, X2)) -> c_37(U21^#(active(X1), X2)) 1084.46/297.13 , active^#(U21(tt(), V1)) -> c_38(U22^#(isNatKind(V1), V1)) 1084.46/297.13 , active^#(U22(X1, X2)) -> c_39(U22^#(active(X1), X2)) 1084.46/297.13 , active^#(U22(tt(), V1)) -> c_40(U23^#(isNat(V1))) 1084.46/297.13 , active^#(U23(X)) -> c_41(U23^#(active(X))) 1084.46/297.13 , active^#(U23(tt())) -> c_42() 1084.46/297.13 , active^#(U31(X1, X2, X3)) -> c_43(U31^#(active(X1), X2, X3)) 1084.46/297.13 , active^#(U31(tt(), V1, V2)) -> c_44(U32^#(isNatKind(V1), V1, V2)) 1084.46/297.13 , active^#(U32(X1, X2, X3)) -> c_45(U32^#(active(X1), X2, X3)) 1084.46/297.13 , active^#(U32(tt(), V1, V2)) -> c_46(U33^#(isNatKind(V2), V1, V2)) 1084.46/297.13 , active^#(U33(X1, X2, X3)) -> c_47(U33^#(active(X1), X2, X3)) 1084.46/297.13 , active^#(U33(tt(), V1, V2)) -> c_48(U34^#(isNatKind(V2), V1, V2)) 1084.46/297.13 , active^#(U34(X1, X2, X3)) -> c_49(U34^#(active(X1), X2, X3)) 1084.46/297.13 , active^#(U34(tt(), V1, V2)) -> c_50(U35^#(isNat(V1), V2)) 1084.46/297.13 , active^#(U35(X1, X2)) -> c_51(U35^#(active(X1), X2)) 1084.46/297.13 , active^#(U35(tt(), V2)) -> c_52(U36^#(isNat(V2))) 1084.46/297.13 , active^#(U36(X)) -> c_53(U36^#(active(X))) 1084.46/297.13 , active^#(U36(tt())) -> c_54() 1084.46/297.13 , active^#(U41(X1, X2)) -> c_55(U41^#(active(X1), X2)) 1084.46/297.13 , active^#(U41(tt(), V2)) -> c_56(U42^#(isNatKind(V2))) 1084.46/297.13 , active^#(U42(X)) -> c_57(U42^#(active(X))) 1084.46/297.13 , active^#(U42(tt())) -> c_58() 1084.46/297.13 , active^#(U51(X)) -> c_59(U51^#(active(X))) 1084.46/297.13 , active^#(U51(tt())) -> c_60() 1084.46/297.13 , active^#(U61(X1, X2)) -> c_61(U61^#(active(X1), X2)) 1084.46/297.13 , active^#(U61(tt(), V2)) -> c_62(U62^#(isNatKind(V2))) 1084.46/297.13 , active^#(U62(X)) -> c_63(U62^#(active(X))) 1084.46/297.13 , active^#(U62(tt())) -> c_64() 1084.46/297.13 , active^#(U71(X1, X2)) -> c_65(U71^#(active(X1), X2)) 1084.46/297.13 , active^#(U71(tt(), N)) -> c_66(U72^#(isNatKind(N), N)) 1084.46/297.13 , active^#(U72(X1, X2)) -> c_67(U72^#(active(X1), X2)) 1084.46/297.13 , active^#(U72(tt(), N)) -> c_68(N) 1084.46/297.13 , active^#(U81(X1, X2, X3)) -> c_69(U81^#(active(X1), X2, X3)) 1084.46/297.13 , active^#(U81(tt(), M, N)) -> c_70(U82^#(isNatKind(M), M, N)) 1084.46/297.13 , active^#(U82(X1, X2, X3)) -> c_71(U82^#(active(X1), X2, X3)) 1084.46/297.13 , active^#(U82(tt(), M, N)) -> c_72(U83^#(isNat(N), M, N)) 1084.46/297.13 , active^#(U83(X1, X2, X3)) -> c_73(U83^#(active(X1), X2, X3)) 1084.46/297.13 , active^#(U83(tt(), M, N)) -> c_74(U84^#(isNatKind(N), M, N)) 1084.46/297.13 , active^#(U84(X1, X2, X3)) -> c_75(U84^#(active(X1), X2, X3)) 1084.46/297.13 , active^#(U84(tt(), M, N)) -> c_76(s^#(plus(N, M))) 1084.46/297.13 , active^#(s(X)) -> c_77(s^#(active(X))) 1084.46/297.13 , active^#(U91(X1, X2)) -> c_78(U91^#(active(X1), X2)) 1084.46/297.13 , active^#(U91(tt(), N)) -> c_79(U92^#(isNatKind(N))) 1084.46/297.13 , active^#(U92(X)) -> c_80(U92^#(active(X))) 1084.46/297.13 , active^#(U92(tt())) -> c_81() 1084.46/297.13 , U101^#(mark(X1), X2, X3) -> c_82(U101^#(X1, X2, X3)) 1084.46/297.13 , U101^#(ok(X1), ok(X2), ok(X3)) -> c_83(U101^#(X1, X2, X3)) 1084.46/297.13 , U102^#(mark(X1), X2, X3) -> c_84(U102^#(X1, X2, X3)) 1084.46/297.13 , U102^#(ok(X1), ok(X2), ok(X3)) -> c_85(U102^#(X1, X2, X3)) 1084.46/297.13 , U103^#(mark(X1), X2, X3) -> c_87(U103^#(X1, X2, X3)) 1084.46/297.13 , U103^#(ok(X1), ok(X2), ok(X3)) -> c_88(U103^#(X1, X2, X3)) 1084.46/297.13 , U41^#(mark(X1), X2) -> c_128(U41^#(X1, X2)) 1084.46/297.13 , U41^#(ok(X1), ok(X2)) -> c_129(U41^#(X1, X2)) 1084.46/297.13 , U61^#(mark(X1), X2) -> c_134(U61^#(X1, X2)) 1084.46/297.13 , U61^#(ok(X1), ok(X2)) -> c_135(U61^#(X1, X2)) 1084.46/297.13 , U51^#(mark(X)) -> c_132(U51^#(X)) 1084.46/297.13 , U51^#(ok(X)) -> c_133(U51^#(X)) 1084.46/297.13 , U104^#(mark(X1), X2, X3) -> c_90(U104^#(X1, X2, X3)) 1084.46/297.13 , U104^#(ok(X1), ok(X2), ok(X3)) -> c_91(U104^#(X1, X2, X3)) 1084.46/297.13 , U11^#(mark(X1), X2, X3) -> c_98(U11^#(X1, X2, X3)) 1084.46/297.13 , U11^#(ok(X1), ok(X2), ok(X3)) -> c_99(U11^#(X1, X2, X3)) 1084.46/297.13 , U31^#(mark(X1), X2, X3) -> c_116(U31^#(X1, X2, X3)) 1084.46/297.13 , U31^#(ok(X1), ok(X2), ok(X3)) -> c_117(U31^#(X1, X2, X3)) 1084.46/297.13 , U21^#(mark(X1), X2) -> c_110(U21^#(X1, X2)) 1084.46/297.13 , U21^#(ok(X1), ok(X2)) -> c_111(U21^#(X1, X2)) 1084.46/297.13 , plus^#(X1, mark(X2)) -> c_92(plus^#(X1, X2)) 1084.46/297.13 , plus^#(mark(X1), X2) -> c_93(plus^#(X1, X2)) 1084.46/297.13 , plus^#(ok(X1), ok(X2)) -> c_94(plus^#(X1, X2)) 1084.46/297.13 , U81^#(mark(X1), X2, X3) -> c_142(U81^#(X1, X2, X3)) 1084.46/297.13 , U81^#(ok(X1), ok(X2), ok(X3)) -> c_143(U81^#(X1, X2, X3)) 1084.46/297.13 , U71^#(mark(X1), X2) -> c_138(U71^#(X1, X2)) 1084.46/297.13 , U71^#(ok(X1), ok(X2)) -> c_139(U71^#(X1, X2)) 1084.46/297.13 , x^#(X1, mark(X2)) -> c_95(x^#(X1, X2)) 1084.46/297.13 , x^#(mark(X1), X2) -> c_96(x^#(X1, X2)) 1084.46/297.13 , x^#(ok(X1), ok(X2)) -> c_97(x^#(X1, X2)) 1084.46/297.13 , U91^#(mark(X1), X2) -> c_152(U91^#(X1, X2)) 1084.46/297.13 , U91^#(ok(X1), ok(X2)) -> c_153(U91^#(X1, X2)) 1084.46/297.13 , U12^#(mark(X1), X2, X3) -> c_100(U12^#(X1, X2, X3)) 1084.46/297.13 , U12^#(ok(X1), ok(X2), ok(X3)) -> c_101(U12^#(X1, X2, X3)) 1084.46/297.13 , U13^#(mark(X1), X2, X3) -> c_102(U13^#(X1, X2, X3)) 1084.46/297.13 , U13^#(ok(X1), ok(X2), ok(X3)) -> c_103(U13^#(X1, X2, X3)) 1084.46/297.13 , U14^#(mark(X1), X2, X3) -> c_104(U14^#(X1, X2, X3)) 1084.46/297.13 , U14^#(ok(X1), ok(X2), ok(X3)) -> c_105(U14^#(X1, X2, X3)) 1084.46/297.13 , U15^#(mark(X1), X2) -> c_106(U15^#(X1, X2)) 1084.46/297.13 , U15^#(ok(X1), ok(X2)) -> c_107(U15^#(X1, X2)) 1084.46/297.13 , U16^#(mark(X)) -> c_108(U16^#(X)) 1084.46/297.13 , U16^#(ok(X)) -> c_109(U16^#(X)) 1084.46/297.13 , U22^#(mark(X1), X2) -> c_112(U22^#(X1, X2)) 1084.46/297.13 , U22^#(ok(X1), ok(X2)) -> c_113(U22^#(X1, X2)) 1084.46/297.13 , U23^#(mark(X)) -> c_114(U23^#(X)) 1084.46/297.13 , U23^#(ok(X)) -> c_115(U23^#(X)) 1084.46/297.13 , U32^#(mark(X1), X2, X3) -> c_118(U32^#(X1, X2, X3)) 1084.46/297.13 , U32^#(ok(X1), ok(X2), ok(X3)) -> c_119(U32^#(X1, X2, X3)) 1084.46/297.13 , U33^#(mark(X1), X2, X3) -> c_120(U33^#(X1, X2, X3)) 1084.46/297.13 , U33^#(ok(X1), ok(X2), ok(X3)) -> c_121(U33^#(X1, X2, X3)) 1084.46/297.13 , U34^#(mark(X1), X2, X3) -> c_122(U34^#(X1, X2, X3)) 1084.46/297.13 , U34^#(ok(X1), ok(X2), ok(X3)) -> c_123(U34^#(X1, X2, X3)) 1084.46/297.13 , U35^#(mark(X1), X2) -> c_124(U35^#(X1, X2)) 1084.46/297.13 , U35^#(ok(X1), ok(X2)) -> c_125(U35^#(X1, X2)) 1084.46/297.13 , U36^#(mark(X)) -> c_126(U36^#(X)) 1084.46/297.13 , U36^#(ok(X)) -> c_127(U36^#(X)) 1084.46/297.13 , U42^#(mark(X)) -> c_130(U42^#(X)) 1084.46/297.13 , U42^#(ok(X)) -> c_131(U42^#(X)) 1084.46/297.13 , U62^#(mark(X)) -> c_136(U62^#(X)) 1084.46/297.13 , U62^#(ok(X)) -> c_137(U62^#(X)) 1084.46/297.13 , U72^#(mark(X1), X2) -> c_140(U72^#(X1, X2)) 1084.46/297.13 , U72^#(ok(X1), ok(X2)) -> c_141(U72^#(X1, X2)) 1084.46/297.13 , U82^#(mark(X1), X2, X3) -> c_144(U82^#(X1, X2, X3)) 1084.46/297.13 , U82^#(ok(X1), ok(X2), ok(X3)) -> c_145(U82^#(X1, X2, X3)) 1084.46/297.13 , U83^#(mark(X1), X2, X3) -> c_146(U83^#(X1, X2, X3)) 1084.46/297.13 , U83^#(ok(X1), ok(X2), ok(X3)) -> c_147(U83^#(X1, X2, X3)) 1084.46/297.13 , U84^#(mark(X1), X2, X3) -> c_148(U84^#(X1, X2, X3)) 1084.46/297.13 , U84^#(ok(X1), ok(X2), ok(X3)) -> c_149(U84^#(X1, X2, X3)) 1084.46/297.13 , s^#(mark(X)) -> c_150(s^#(X)) 1084.46/297.13 , s^#(ok(X)) -> c_151(s^#(X)) 1084.46/297.13 , U92^#(mark(X)) -> c_154(U92^#(X)) 1084.46/297.13 , U92^#(ok(X)) -> c_155(U92^#(X)) 1084.46/297.13 , isNatKind^#(ok(X)) -> c_86(isNatKind^#(X)) 1084.46/297.13 , isNat^#(ok(X)) -> c_89(isNat^#(X)) 1084.46/297.13 , proper^#(U101(X1, X2, X3)) -> 1084.46/297.13 c_156(U101^#(proper(X1), proper(X2), proper(X3))) 1084.46/297.13 , proper^#(tt()) -> c_157() 1084.46/297.13 , proper^#(U102(X1, X2, X3)) -> 1084.46/297.13 c_158(U102^#(proper(X1), proper(X2), proper(X3))) 1084.46/297.13 , proper^#(isNatKind(X)) -> c_159(isNatKind^#(proper(X))) 1084.46/297.13 , proper^#(U103(X1, X2, X3)) -> 1084.46/297.13 c_160(U103^#(proper(X1), proper(X2), proper(X3))) 1084.46/297.13 , proper^#(isNat(X)) -> c_161(isNat^#(proper(X))) 1084.46/297.13 , proper^#(U104(X1, X2, X3)) -> 1084.46/297.13 c_162(U104^#(proper(X1), proper(X2), proper(X3))) 1084.46/297.13 , proper^#(plus(X1, X2)) -> c_163(plus^#(proper(X1), proper(X2))) 1084.46/297.13 , proper^#(x(X1, X2)) -> c_164(x^#(proper(X1), proper(X2))) 1084.46/297.13 , proper^#(U11(X1, X2, X3)) -> 1084.46/297.13 c_165(U11^#(proper(X1), proper(X2), proper(X3))) 1084.46/297.13 , proper^#(U12(X1, X2, X3)) -> 1084.46/297.13 c_166(U12^#(proper(X1), proper(X2), proper(X3))) 1084.46/297.13 , proper^#(U13(X1, X2, X3)) -> 1084.46/297.13 c_167(U13^#(proper(X1), proper(X2), proper(X3))) 1084.46/297.13 , proper^#(U14(X1, X2, X3)) -> 1084.46/297.13 c_168(U14^#(proper(X1), proper(X2), proper(X3))) 1084.46/297.13 , proper^#(U15(X1, X2)) -> c_169(U15^#(proper(X1), proper(X2))) 1084.46/297.13 , proper^#(U16(X)) -> c_170(U16^#(proper(X))) 1084.46/297.13 , proper^#(U21(X1, X2)) -> c_171(U21^#(proper(X1), proper(X2))) 1084.46/297.13 , proper^#(U22(X1, X2)) -> c_172(U22^#(proper(X1), proper(X2))) 1084.46/297.13 , proper^#(U23(X)) -> c_173(U23^#(proper(X))) 1084.46/297.13 , proper^#(U31(X1, X2, X3)) -> 1084.46/297.13 c_174(U31^#(proper(X1), proper(X2), proper(X3))) 1084.46/297.13 , proper^#(U32(X1, X2, X3)) -> 1084.46/297.13 c_175(U32^#(proper(X1), proper(X2), proper(X3))) 1084.46/297.13 , proper^#(U33(X1, X2, X3)) -> 1084.46/297.13 c_176(U33^#(proper(X1), proper(X2), proper(X3))) 1084.46/297.13 , proper^#(U34(X1, X2, X3)) -> 1084.46/297.13 c_177(U34^#(proper(X1), proper(X2), proper(X3))) 1084.46/297.13 , proper^#(U35(X1, X2)) -> c_178(U35^#(proper(X1), proper(X2))) 1084.46/297.13 , proper^#(U36(X)) -> c_179(U36^#(proper(X))) 1084.46/297.13 , proper^#(U41(X1, X2)) -> c_180(U41^#(proper(X1), proper(X2))) 1084.46/297.13 , proper^#(U42(X)) -> c_181(U42^#(proper(X))) 1084.46/297.13 , proper^#(U51(X)) -> c_182(U51^#(proper(X))) 1084.46/297.13 , proper^#(U61(X1, X2)) -> c_183(U61^#(proper(X1), proper(X2))) 1084.46/297.13 , proper^#(U62(X)) -> c_184(U62^#(proper(X))) 1084.46/297.13 , proper^#(U71(X1, X2)) -> c_185(U71^#(proper(X1), proper(X2))) 1084.46/297.13 , proper^#(U72(X1, X2)) -> c_186(U72^#(proper(X1), proper(X2))) 1084.46/297.13 , proper^#(U81(X1, X2, X3)) -> 1084.46/297.13 c_187(U81^#(proper(X1), proper(X2), proper(X3))) 1084.46/297.13 , proper^#(U82(X1, X2, X3)) -> 1084.46/297.13 c_188(U82^#(proper(X1), proper(X2), proper(X3))) 1084.46/297.13 , proper^#(U83(X1, X2, X3)) -> 1084.46/297.13 c_189(U83^#(proper(X1), proper(X2), proper(X3))) 1084.46/297.13 , proper^#(U84(X1, X2, X3)) -> 1084.46/297.13 c_190(U84^#(proper(X1), proper(X2), proper(X3))) 1084.46/297.13 , proper^#(s(X)) -> c_191(s^#(proper(X))) 1084.46/297.13 , proper^#(U91(X1, X2)) -> c_192(U91^#(proper(X1), proper(X2))) 1084.46/297.13 , proper^#(U92(X)) -> c_193(U92^#(proper(X))) 1084.46/297.13 , proper^#(0()) -> c_194() 1084.46/297.13 , top^#(mark(X)) -> c_195(top^#(proper(X))) 1084.46/297.13 , top^#(ok(X)) -> c_196(top^#(active(X))) } 1084.46/297.13 1084.46/297.13 and mark the set of starting terms. 1084.46/297.13 1084.46/297.13 We are left with following problem, upon which TcT provides the 1084.46/297.13 certificate MAYBE. 1084.46/297.13 1084.46/297.13 Strict DPs: 1084.46/297.13 { active^#(U101(X1, X2, X3)) -> c_1(U101^#(active(X1), X2, X3)) 1084.46/297.13 , active^#(U101(tt(), M, N)) -> c_2(U102^#(isNatKind(M), M, N)) 1084.46/297.13 , active^#(U102(X1, X2, X3)) -> c_3(U102^#(active(X1), X2, X3)) 1084.46/297.13 , active^#(U102(tt(), M, N)) -> c_4(U103^#(isNat(N), M, N)) 1084.46/297.13 , active^#(isNatKind(plus(V1, V2))) -> 1084.46/297.13 c_5(U41^#(isNatKind(V1), V2)) 1084.46/297.13 , active^#(isNatKind(x(V1, V2))) -> c_6(U61^#(isNatKind(V1), V2)) 1084.46/297.14 , active^#(isNatKind(s(V1))) -> c_7(U51^#(isNatKind(V1))) 1084.46/297.14 , active^#(isNatKind(0())) -> c_8() 1084.46/297.14 , active^#(U103(X1, X2, X3)) -> c_9(U103^#(active(X1), X2, X3)) 1084.46/297.14 , active^#(U103(tt(), M, N)) -> c_10(U104^#(isNatKind(N), M, N)) 1084.46/297.14 , active^#(isNat(plus(V1, V2))) -> 1084.46/297.14 c_11(U11^#(isNatKind(V1), V1, V2)) 1084.46/297.14 , active^#(isNat(x(V1, V2))) -> c_12(U31^#(isNatKind(V1), V1, V2)) 1084.46/297.14 , active^#(isNat(s(V1))) -> c_13(U21^#(isNatKind(V1), V1)) 1084.46/297.14 , active^#(isNat(0())) -> c_14() 1084.46/297.14 , active^#(U104(X1, X2, X3)) -> c_15(U104^#(active(X1), X2, X3)) 1084.46/297.14 , active^#(U104(tt(), M, N)) -> c_16(plus^#(x(N, M), N)) 1084.46/297.14 , active^#(plus(X1, X2)) -> c_17(plus^#(X1, active(X2))) 1084.46/297.14 , active^#(plus(X1, X2)) -> c_18(plus^#(active(X1), X2)) 1084.46/297.14 , active^#(plus(N, s(M))) -> c_19(U81^#(isNat(M), M, N)) 1084.46/297.14 , active^#(plus(N, 0())) -> c_20(U71^#(isNat(N), N)) 1084.46/297.14 , active^#(x(X1, X2)) -> c_21(x^#(X1, active(X2))) 1084.46/297.14 , active^#(x(X1, X2)) -> c_22(x^#(active(X1), X2)) 1084.46/297.14 , active^#(x(N, s(M))) -> c_23(U101^#(isNat(M), M, N)) 1084.46/297.14 , active^#(x(N, 0())) -> c_24(U91^#(isNat(N), N)) 1084.46/297.14 , active^#(U11(X1, X2, X3)) -> c_25(U11^#(active(X1), X2, X3)) 1084.46/297.14 , active^#(U11(tt(), V1, V2)) -> c_26(U12^#(isNatKind(V1), V1, V2)) 1084.46/297.14 , active^#(U12(X1, X2, X3)) -> c_27(U12^#(active(X1), X2, X3)) 1084.46/297.14 , active^#(U12(tt(), V1, V2)) -> c_28(U13^#(isNatKind(V2), V1, V2)) 1084.46/297.14 , active^#(U13(X1, X2, X3)) -> c_29(U13^#(active(X1), X2, X3)) 1084.46/297.14 , active^#(U13(tt(), V1, V2)) -> c_30(U14^#(isNatKind(V2), V1, V2)) 1084.46/297.14 , active^#(U14(X1, X2, X3)) -> c_31(U14^#(active(X1), X2, X3)) 1084.46/297.14 , active^#(U14(tt(), V1, V2)) -> c_32(U15^#(isNat(V1), V2)) 1084.46/297.14 , active^#(U15(X1, X2)) -> c_33(U15^#(active(X1), X2)) 1084.46/297.14 , active^#(U15(tt(), V2)) -> c_34(U16^#(isNat(V2))) 1084.46/297.14 , active^#(U16(X)) -> c_35(U16^#(active(X))) 1084.46/297.14 , active^#(U16(tt())) -> c_36() 1084.46/297.14 , active^#(U21(X1, X2)) -> c_37(U21^#(active(X1), X2)) 1084.46/297.14 , active^#(U21(tt(), V1)) -> c_38(U22^#(isNatKind(V1), V1)) 1084.46/297.14 , active^#(U22(X1, X2)) -> c_39(U22^#(active(X1), X2)) 1084.46/297.14 , active^#(U22(tt(), V1)) -> c_40(U23^#(isNat(V1))) 1084.46/297.14 , active^#(U23(X)) -> c_41(U23^#(active(X))) 1084.46/297.14 , active^#(U23(tt())) -> c_42() 1084.46/297.14 , active^#(U31(X1, X2, X3)) -> c_43(U31^#(active(X1), X2, X3)) 1084.46/297.14 , active^#(U31(tt(), V1, V2)) -> c_44(U32^#(isNatKind(V1), V1, V2)) 1084.46/297.14 , active^#(U32(X1, X2, X3)) -> c_45(U32^#(active(X1), X2, X3)) 1084.46/297.14 , active^#(U32(tt(), V1, V2)) -> c_46(U33^#(isNatKind(V2), V1, V2)) 1084.46/297.14 , active^#(U33(X1, X2, X3)) -> c_47(U33^#(active(X1), X2, X3)) 1084.46/297.14 , active^#(U33(tt(), V1, V2)) -> c_48(U34^#(isNatKind(V2), V1, V2)) 1084.46/297.14 , active^#(U34(X1, X2, X3)) -> c_49(U34^#(active(X1), X2, X3)) 1084.46/297.14 , active^#(U34(tt(), V1, V2)) -> c_50(U35^#(isNat(V1), V2)) 1084.46/297.14 , active^#(U35(X1, X2)) -> c_51(U35^#(active(X1), X2)) 1084.46/297.14 , active^#(U35(tt(), V2)) -> c_52(U36^#(isNat(V2))) 1084.46/297.14 , active^#(U36(X)) -> c_53(U36^#(active(X))) 1084.46/297.14 , active^#(U36(tt())) -> c_54() 1084.46/297.14 , active^#(U41(X1, X2)) -> c_55(U41^#(active(X1), X2)) 1084.46/297.14 , active^#(U41(tt(), V2)) -> c_56(U42^#(isNatKind(V2))) 1084.46/297.14 , active^#(U42(X)) -> c_57(U42^#(active(X))) 1084.46/297.14 , active^#(U42(tt())) -> c_58() 1084.46/297.14 , active^#(U51(X)) -> c_59(U51^#(active(X))) 1084.46/297.14 , active^#(U51(tt())) -> c_60() 1084.46/297.14 , active^#(U61(X1, X2)) -> c_61(U61^#(active(X1), X2)) 1084.46/297.14 , active^#(U61(tt(), V2)) -> c_62(U62^#(isNatKind(V2))) 1084.46/297.14 , active^#(U62(X)) -> c_63(U62^#(active(X))) 1084.46/297.14 , active^#(U62(tt())) -> c_64() 1084.46/297.14 , active^#(U71(X1, X2)) -> c_65(U71^#(active(X1), X2)) 1084.46/297.14 , active^#(U71(tt(), N)) -> c_66(U72^#(isNatKind(N), N)) 1084.46/297.14 , active^#(U72(X1, X2)) -> c_67(U72^#(active(X1), X2)) 1084.46/297.14 , active^#(U72(tt(), N)) -> c_68(N) 1084.46/297.14 , active^#(U81(X1, X2, X3)) -> c_69(U81^#(active(X1), X2, X3)) 1084.46/297.14 , active^#(U81(tt(), M, N)) -> c_70(U82^#(isNatKind(M), M, N)) 1084.46/297.14 , active^#(U82(X1, X2, X3)) -> c_71(U82^#(active(X1), X2, X3)) 1084.46/297.14 , active^#(U82(tt(), M, N)) -> c_72(U83^#(isNat(N), M, N)) 1084.46/297.14 , active^#(U83(X1, X2, X3)) -> c_73(U83^#(active(X1), X2, X3)) 1084.46/297.14 , active^#(U83(tt(), M, N)) -> c_74(U84^#(isNatKind(N), M, N)) 1084.46/297.14 , active^#(U84(X1, X2, X3)) -> c_75(U84^#(active(X1), X2, X3)) 1084.46/297.14 , active^#(U84(tt(), M, N)) -> c_76(s^#(plus(N, M))) 1084.46/297.14 , active^#(s(X)) -> c_77(s^#(active(X))) 1084.46/297.14 , active^#(U91(X1, X2)) -> c_78(U91^#(active(X1), X2)) 1084.46/297.14 , active^#(U91(tt(), N)) -> c_79(U92^#(isNatKind(N))) 1084.46/297.14 , active^#(U92(X)) -> c_80(U92^#(active(X))) 1084.46/297.14 , active^#(U92(tt())) -> c_81() 1084.46/297.14 , U101^#(mark(X1), X2, X3) -> c_82(U101^#(X1, X2, X3)) 1084.46/297.14 , U101^#(ok(X1), ok(X2), ok(X3)) -> c_83(U101^#(X1, X2, X3)) 1084.46/297.14 , U102^#(mark(X1), X2, X3) -> c_84(U102^#(X1, X2, X3)) 1084.46/297.14 , U102^#(ok(X1), ok(X2), ok(X3)) -> c_85(U102^#(X1, X2, X3)) 1084.46/297.14 , U103^#(mark(X1), X2, X3) -> c_87(U103^#(X1, X2, X3)) 1084.46/297.14 , U103^#(ok(X1), ok(X2), ok(X3)) -> c_88(U103^#(X1, X2, X3)) 1084.46/297.14 , U41^#(mark(X1), X2) -> c_128(U41^#(X1, X2)) 1084.46/297.14 , U41^#(ok(X1), ok(X2)) -> c_129(U41^#(X1, X2)) 1084.46/297.14 , U61^#(mark(X1), X2) -> c_134(U61^#(X1, X2)) 1084.46/297.14 , U61^#(ok(X1), ok(X2)) -> c_135(U61^#(X1, X2)) 1084.46/297.14 , U51^#(mark(X)) -> c_132(U51^#(X)) 1084.46/297.14 , U51^#(ok(X)) -> c_133(U51^#(X)) 1084.46/297.14 , U104^#(mark(X1), X2, X3) -> c_90(U104^#(X1, X2, X3)) 1084.46/297.14 , U104^#(ok(X1), ok(X2), ok(X3)) -> c_91(U104^#(X1, X2, X3)) 1084.46/297.14 , U11^#(mark(X1), X2, X3) -> c_98(U11^#(X1, X2, X3)) 1084.46/297.14 , U11^#(ok(X1), ok(X2), ok(X3)) -> c_99(U11^#(X1, X2, X3)) 1084.46/297.14 , U31^#(mark(X1), X2, X3) -> c_116(U31^#(X1, X2, X3)) 1084.46/297.14 , U31^#(ok(X1), ok(X2), ok(X3)) -> c_117(U31^#(X1, X2, X3)) 1084.46/297.14 , U21^#(mark(X1), X2) -> c_110(U21^#(X1, X2)) 1084.46/297.14 , U21^#(ok(X1), ok(X2)) -> c_111(U21^#(X1, X2)) 1084.46/297.14 , plus^#(X1, mark(X2)) -> c_92(plus^#(X1, X2)) 1084.46/297.14 , plus^#(mark(X1), X2) -> c_93(plus^#(X1, X2)) 1084.46/297.14 , plus^#(ok(X1), ok(X2)) -> c_94(plus^#(X1, X2)) 1084.46/297.14 , U81^#(mark(X1), X2, X3) -> c_142(U81^#(X1, X2, X3)) 1084.46/297.14 , U81^#(ok(X1), ok(X2), ok(X3)) -> c_143(U81^#(X1, X2, X3)) 1084.46/297.14 , U71^#(mark(X1), X2) -> c_138(U71^#(X1, X2)) 1084.46/297.14 , U71^#(ok(X1), ok(X2)) -> c_139(U71^#(X1, X2)) 1084.46/297.14 , x^#(X1, mark(X2)) -> c_95(x^#(X1, X2)) 1084.46/297.14 , x^#(mark(X1), X2) -> c_96(x^#(X1, X2)) 1084.46/297.14 , x^#(ok(X1), ok(X2)) -> c_97(x^#(X1, X2)) 1084.46/297.14 , U91^#(mark(X1), X2) -> c_152(U91^#(X1, X2)) 1084.46/297.14 , U91^#(ok(X1), ok(X2)) -> c_153(U91^#(X1, X2)) 1084.46/297.14 , U12^#(mark(X1), X2, X3) -> c_100(U12^#(X1, X2, X3)) 1084.46/297.14 , U12^#(ok(X1), ok(X2), ok(X3)) -> c_101(U12^#(X1, X2, X3)) 1084.46/297.14 , U13^#(mark(X1), X2, X3) -> c_102(U13^#(X1, X2, X3)) 1084.46/297.14 , U13^#(ok(X1), ok(X2), ok(X3)) -> c_103(U13^#(X1, X2, X3)) 1084.46/297.14 , U14^#(mark(X1), X2, X3) -> c_104(U14^#(X1, X2, X3)) 1084.46/297.14 , U14^#(ok(X1), ok(X2), ok(X3)) -> c_105(U14^#(X1, X2, X3)) 1084.46/297.14 , U15^#(mark(X1), X2) -> c_106(U15^#(X1, X2)) 1084.46/297.14 , U15^#(ok(X1), ok(X2)) -> c_107(U15^#(X1, X2)) 1084.46/297.14 , U16^#(mark(X)) -> c_108(U16^#(X)) 1084.46/297.14 , U16^#(ok(X)) -> c_109(U16^#(X)) 1084.46/297.14 , U22^#(mark(X1), X2) -> c_112(U22^#(X1, X2)) 1084.46/297.14 , U22^#(ok(X1), ok(X2)) -> c_113(U22^#(X1, X2)) 1084.46/297.14 , U23^#(mark(X)) -> c_114(U23^#(X)) 1084.46/297.14 , U23^#(ok(X)) -> c_115(U23^#(X)) 1084.46/297.14 , U32^#(mark(X1), X2, X3) -> c_118(U32^#(X1, X2, X3)) 1084.46/297.14 , U32^#(ok(X1), ok(X2), ok(X3)) -> c_119(U32^#(X1, X2, X3)) 1084.46/297.14 , U33^#(mark(X1), X2, X3) -> c_120(U33^#(X1, X2, X3)) 1084.46/297.14 , U33^#(ok(X1), ok(X2), ok(X3)) -> c_121(U33^#(X1, X2, X3)) 1084.46/297.14 , U34^#(mark(X1), X2, X3) -> c_122(U34^#(X1, X2, X3)) 1084.46/297.14 , U34^#(ok(X1), ok(X2), ok(X3)) -> c_123(U34^#(X1, X2, X3)) 1084.46/297.14 , U35^#(mark(X1), X2) -> c_124(U35^#(X1, X2)) 1084.46/297.14 , U35^#(ok(X1), ok(X2)) -> c_125(U35^#(X1, X2)) 1084.46/297.14 , U36^#(mark(X)) -> c_126(U36^#(X)) 1084.46/297.14 , U36^#(ok(X)) -> c_127(U36^#(X)) 1084.46/297.14 , U42^#(mark(X)) -> c_130(U42^#(X)) 1084.46/297.14 , U42^#(ok(X)) -> c_131(U42^#(X)) 1084.46/297.14 , U62^#(mark(X)) -> c_136(U62^#(X)) 1084.46/297.14 , U62^#(ok(X)) -> c_137(U62^#(X)) 1084.46/297.14 , U72^#(mark(X1), X2) -> c_140(U72^#(X1, X2)) 1084.46/297.14 , U72^#(ok(X1), ok(X2)) -> c_141(U72^#(X1, X2)) 1084.46/297.14 , U82^#(mark(X1), X2, X3) -> c_144(U82^#(X1, X2, X3)) 1084.46/297.14 , U82^#(ok(X1), ok(X2), ok(X3)) -> c_145(U82^#(X1, X2, X3)) 1084.46/297.14 , U83^#(mark(X1), X2, X3) -> c_146(U83^#(X1, X2, X3)) 1084.46/297.14 , U83^#(ok(X1), ok(X2), ok(X3)) -> c_147(U83^#(X1, X2, X3)) 1084.46/297.14 , U84^#(mark(X1), X2, X3) -> c_148(U84^#(X1, X2, X3)) 1084.46/297.14 , U84^#(ok(X1), ok(X2), ok(X3)) -> c_149(U84^#(X1, X2, X3)) 1084.46/297.14 , s^#(mark(X)) -> c_150(s^#(X)) 1084.46/297.14 , s^#(ok(X)) -> c_151(s^#(X)) 1084.46/297.14 , U92^#(mark(X)) -> c_154(U92^#(X)) 1084.46/297.14 , U92^#(ok(X)) -> c_155(U92^#(X)) 1084.46/297.14 , isNatKind^#(ok(X)) -> c_86(isNatKind^#(X)) 1084.46/297.14 , isNat^#(ok(X)) -> c_89(isNat^#(X)) 1084.46/297.14 , proper^#(U101(X1, X2, X3)) -> 1084.46/297.14 c_156(U101^#(proper(X1), proper(X2), proper(X3))) 1084.46/297.14 , proper^#(tt()) -> c_157() 1084.46/297.14 , proper^#(U102(X1, X2, X3)) -> 1084.46/297.14 c_158(U102^#(proper(X1), proper(X2), proper(X3))) 1084.46/297.14 , proper^#(isNatKind(X)) -> c_159(isNatKind^#(proper(X))) 1084.46/297.14 , proper^#(U103(X1, X2, X3)) -> 1084.46/297.14 c_160(U103^#(proper(X1), proper(X2), proper(X3))) 1084.46/297.14 , proper^#(isNat(X)) -> c_161(isNat^#(proper(X))) 1084.46/297.14 , proper^#(U104(X1, X2, X3)) -> 1084.46/297.14 c_162(U104^#(proper(X1), proper(X2), proper(X3))) 1084.46/297.14 , proper^#(plus(X1, X2)) -> c_163(plus^#(proper(X1), proper(X2))) 1084.46/297.14 , proper^#(x(X1, X2)) -> c_164(x^#(proper(X1), proper(X2))) 1084.46/297.14 , proper^#(U11(X1, X2, X3)) -> 1084.46/297.14 c_165(U11^#(proper(X1), proper(X2), proper(X3))) 1084.46/297.14 , proper^#(U12(X1, X2, X3)) -> 1084.46/297.14 c_166(U12^#(proper(X1), proper(X2), proper(X3))) 1084.46/297.14 , proper^#(U13(X1, X2, X3)) -> 1084.46/297.14 c_167(U13^#(proper(X1), proper(X2), proper(X3))) 1084.46/297.14 , proper^#(U14(X1, X2, X3)) -> 1084.46/297.14 c_168(U14^#(proper(X1), proper(X2), proper(X3))) 1084.46/297.14 , proper^#(U15(X1, X2)) -> c_169(U15^#(proper(X1), proper(X2))) 1084.46/297.14 , proper^#(U16(X)) -> c_170(U16^#(proper(X))) 1084.46/297.14 , proper^#(U21(X1, X2)) -> c_171(U21^#(proper(X1), proper(X2))) 1084.46/297.14 , proper^#(U22(X1, X2)) -> c_172(U22^#(proper(X1), proper(X2))) 1084.46/297.14 , proper^#(U23(X)) -> c_173(U23^#(proper(X))) 1084.46/297.14 , proper^#(U31(X1, X2, X3)) -> 1084.46/297.14 c_174(U31^#(proper(X1), proper(X2), proper(X3))) 1084.46/297.14 , proper^#(U32(X1, X2, X3)) -> 1084.46/297.14 c_175(U32^#(proper(X1), proper(X2), proper(X3))) 1084.46/297.14 , proper^#(U33(X1, X2, X3)) -> 1084.46/297.14 c_176(U33^#(proper(X1), proper(X2), proper(X3))) 1084.46/297.14 , proper^#(U34(X1, X2, X3)) -> 1084.46/297.14 c_177(U34^#(proper(X1), proper(X2), proper(X3))) 1084.46/297.14 , proper^#(U35(X1, X2)) -> c_178(U35^#(proper(X1), proper(X2))) 1084.46/297.14 , proper^#(U36(X)) -> c_179(U36^#(proper(X))) 1084.46/297.14 , proper^#(U41(X1, X2)) -> c_180(U41^#(proper(X1), proper(X2))) 1084.46/297.14 , proper^#(U42(X)) -> c_181(U42^#(proper(X))) 1084.46/297.14 , proper^#(U51(X)) -> c_182(U51^#(proper(X))) 1084.46/297.14 , proper^#(U61(X1, X2)) -> c_183(U61^#(proper(X1), proper(X2))) 1084.46/297.14 , proper^#(U62(X)) -> c_184(U62^#(proper(X))) 1084.46/297.14 , proper^#(U71(X1, X2)) -> c_185(U71^#(proper(X1), proper(X2))) 1084.46/297.14 , proper^#(U72(X1, X2)) -> c_186(U72^#(proper(X1), proper(X2))) 1084.46/297.14 , proper^#(U81(X1, X2, X3)) -> 1084.46/297.14 c_187(U81^#(proper(X1), proper(X2), proper(X3))) 1084.46/297.14 , proper^#(U82(X1, X2, X3)) -> 1084.46/297.14 c_188(U82^#(proper(X1), proper(X2), proper(X3))) 1084.46/297.14 , proper^#(U83(X1, X2, X3)) -> 1084.46/297.14 c_189(U83^#(proper(X1), proper(X2), proper(X3))) 1084.46/297.14 , proper^#(U84(X1, X2, X3)) -> 1084.46/297.14 c_190(U84^#(proper(X1), proper(X2), proper(X3))) 1084.46/297.14 , proper^#(s(X)) -> c_191(s^#(proper(X))) 1084.46/297.14 , proper^#(U91(X1, X2)) -> c_192(U91^#(proper(X1), proper(X2))) 1084.46/297.14 , proper^#(U92(X)) -> c_193(U92^#(proper(X))) 1084.46/297.14 , proper^#(0()) -> c_194() 1084.46/297.14 , top^#(mark(X)) -> c_195(top^#(proper(X))) 1084.46/297.14 , top^#(ok(X)) -> c_196(top^#(active(X))) } 1084.46/297.14 Strict Trs: 1084.46/297.14 { active(U101(X1, X2, X3)) -> U101(active(X1), X2, X3) 1084.46/297.14 , active(U101(tt(), M, N)) -> mark(U102(isNatKind(M), M, N)) 1084.46/297.14 , active(U102(X1, X2, X3)) -> U102(active(X1), X2, X3) 1084.46/297.14 , active(U102(tt(), M, N)) -> mark(U103(isNat(N), M, N)) 1084.46/297.14 , active(isNatKind(plus(V1, V2))) -> mark(U41(isNatKind(V1), V2)) 1084.46/297.14 , active(isNatKind(x(V1, V2))) -> mark(U61(isNatKind(V1), V2)) 1084.46/297.14 , active(isNatKind(s(V1))) -> mark(U51(isNatKind(V1))) 1084.46/297.14 , active(isNatKind(0())) -> mark(tt()) 1084.46/297.14 , active(U103(X1, X2, X3)) -> U103(active(X1), X2, X3) 1084.46/297.14 , active(U103(tt(), M, N)) -> mark(U104(isNatKind(N), M, N)) 1084.46/297.14 , active(isNat(plus(V1, V2))) -> mark(U11(isNatKind(V1), V1, V2)) 1084.46/297.14 , active(isNat(x(V1, V2))) -> mark(U31(isNatKind(V1), V1, V2)) 1084.46/297.14 , active(isNat(s(V1))) -> mark(U21(isNatKind(V1), V1)) 1084.46/297.14 , active(isNat(0())) -> mark(tt()) 1084.46/297.14 , active(U104(X1, X2, X3)) -> U104(active(X1), X2, X3) 1084.46/297.14 , active(U104(tt(), M, N)) -> mark(plus(x(N, M), N)) 1084.46/297.14 , active(plus(X1, X2)) -> plus(X1, active(X2)) 1084.46/297.14 , active(plus(X1, X2)) -> plus(active(X1), X2) 1084.46/297.14 , active(plus(N, s(M))) -> mark(U81(isNat(M), M, N)) 1084.46/297.14 , active(plus(N, 0())) -> mark(U71(isNat(N), N)) 1084.46/297.14 , active(x(X1, X2)) -> x(X1, active(X2)) 1084.46/297.14 , active(x(X1, X2)) -> x(active(X1), X2) 1084.46/297.14 , active(x(N, s(M))) -> mark(U101(isNat(M), M, N)) 1084.46/297.14 , active(x(N, 0())) -> mark(U91(isNat(N), N)) 1084.46/297.14 , active(U11(X1, X2, X3)) -> U11(active(X1), X2, X3) 1084.46/297.14 , active(U11(tt(), V1, V2)) -> mark(U12(isNatKind(V1), V1, V2)) 1084.46/297.14 , active(U12(X1, X2, X3)) -> U12(active(X1), X2, X3) 1084.46/297.14 , active(U12(tt(), V1, V2)) -> mark(U13(isNatKind(V2), V1, V2)) 1084.46/297.14 , active(U13(X1, X2, X3)) -> U13(active(X1), X2, X3) 1084.46/297.14 , active(U13(tt(), V1, V2)) -> mark(U14(isNatKind(V2), V1, V2)) 1084.46/297.14 , active(U14(X1, X2, X3)) -> U14(active(X1), X2, X3) 1084.46/297.14 , active(U14(tt(), V1, V2)) -> mark(U15(isNat(V1), V2)) 1084.46/297.14 , active(U15(X1, X2)) -> U15(active(X1), X2) 1084.46/297.14 , active(U15(tt(), V2)) -> mark(U16(isNat(V2))) 1084.46/297.14 , active(U16(X)) -> U16(active(X)) 1084.46/297.14 , active(U16(tt())) -> mark(tt()) 1084.46/297.14 , active(U21(X1, X2)) -> U21(active(X1), X2) 1084.46/297.14 , active(U21(tt(), V1)) -> mark(U22(isNatKind(V1), V1)) 1084.46/297.14 , active(U22(X1, X2)) -> U22(active(X1), X2) 1084.46/297.14 , active(U22(tt(), V1)) -> mark(U23(isNat(V1))) 1084.46/297.14 , active(U23(X)) -> U23(active(X)) 1084.46/297.14 , active(U23(tt())) -> mark(tt()) 1084.46/297.14 , active(U31(X1, X2, X3)) -> U31(active(X1), X2, X3) 1084.46/297.14 , active(U31(tt(), V1, V2)) -> mark(U32(isNatKind(V1), V1, V2)) 1084.46/297.14 , active(U32(X1, X2, X3)) -> U32(active(X1), X2, X3) 1084.46/297.14 , active(U32(tt(), V1, V2)) -> mark(U33(isNatKind(V2), V1, V2)) 1084.46/297.14 , active(U33(X1, X2, X3)) -> U33(active(X1), X2, X3) 1084.46/297.14 , active(U33(tt(), V1, V2)) -> mark(U34(isNatKind(V2), V1, V2)) 1084.46/297.14 , active(U34(X1, X2, X3)) -> U34(active(X1), X2, X3) 1084.46/297.14 , active(U34(tt(), V1, V2)) -> mark(U35(isNat(V1), V2)) 1084.46/297.14 , active(U35(X1, X2)) -> U35(active(X1), X2) 1084.46/297.14 , active(U35(tt(), V2)) -> mark(U36(isNat(V2))) 1084.46/297.14 , active(U36(X)) -> U36(active(X)) 1084.46/297.14 , active(U36(tt())) -> mark(tt()) 1084.46/297.14 , active(U41(X1, X2)) -> U41(active(X1), X2) 1084.46/297.14 , active(U41(tt(), V2)) -> mark(U42(isNatKind(V2))) 1084.46/297.14 , active(U42(X)) -> U42(active(X)) 1084.46/297.14 , active(U42(tt())) -> mark(tt()) 1084.46/297.14 , active(U51(X)) -> U51(active(X)) 1084.46/297.14 , active(U51(tt())) -> mark(tt()) 1084.46/297.14 , active(U61(X1, X2)) -> U61(active(X1), X2) 1084.46/297.14 , active(U61(tt(), V2)) -> mark(U62(isNatKind(V2))) 1084.46/297.14 , active(U62(X)) -> U62(active(X)) 1084.46/297.14 , active(U62(tt())) -> mark(tt()) 1084.46/297.14 , active(U71(X1, X2)) -> U71(active(X1), X2) 1084.46/297.14 , active(U71(tt(), N)) -> mark(U72(isNatKind(N), N)) 1084.46/297.14 , active(U72(X1, X2)) -> U72(active(X1), X2) 1084.46/297.14 , active(U72(tt(), N)) -> mark(N) 1084.46/297.14 , active(U81(X1, X2, X3)) -> U81(active(X1), X2, X3) 1084.46/297.14 , active(U81(tt(), M, N)) -> mark(U82(isNatKind(M), M, N)) 1084.46/297.14 , active(U82(X1, X2, X3)) -> U82(active(X1), X2, X3) 1084.46/297.14 , active(U82(tt(), M, N)) -> mark(U83(isNat(N), M, N)) 1084.46/297.14 , active(U83(X1, X2, X3)) -> U83(active(X1), X2, X3) 1084.46/297.14 , active(U83(tt(), M, N)) -> mark(U84(isNatKind(N), M, N)) 1084.46/297.14 , active(U84(X1, X2, X3)) -> U84(active(X1), X2, X3) 1084.46/297.14 , active(U84(tt(), M, N)) -> mark(s(plus(N, M))) 1084.46/297.14 , active(s(X)) -> s(active(X)) 1084.46/297.14 , active(U91(X1, X2)) -> U91(active(X1), X2) 1084.46/297.14 , active(U91(tt(), N)) -> mark(U92(isNatKind(N))) 1084.46/297.14 , active(U92(X)) -> U92(active(X)) 1084.46/297.14 , active(U92(tt())) -> mark(0()) 1084.46/297.14 , U101(mark(X1), X2, X3) -> mark(U101(X1, X2, X3)) 1084.46/297.14 , U101(ok(X1), ok(X2), ok(X3)) -> ok(U101(X1, X2, X3)) 1084.46/297.14 , U102(mark(X1), X2, X3) -> mark(U102(X1, X2, X3)) 1084.46/297.14 , U102(ok(X1), ok(X2), ok(X3)) -> ok(U102(X1, X2, X3)) 1084.46/297.14 , isNatKind(ok(X)) -> ok(isNatKind(X)) 1084.46/297.14 , U103(mark(X1), X2, X3) -> mark(U103(X1, X2, X3)) 1084.46/297.14 , U103(ok(X1), ok(X2), ok(X3)) -> ok(U103(X1, X2, X3)) 1084.46/297.14 , isNat(ok(X)) -> ok(isNat(X)) 1084.46/297.14 , U104(mark(X1), X2, X3) -> mark(U104(X1, X2, X3)) 1084.46/297.15 , U104(ok(X1), ok(X2), ok(X3)) -> ok(U104(X1, X2, X3)) 1084.46/297.15 , plus(X1, mark(X2)) -> mark(plus(X1, X2)) 1084.46/297.15 , plus(mark(X1), X2) -> mark(plus(X1, X2)) 1084.46/297.15 , plus(ok(X1), ok(X2)) -> ok(plus(X1, X2)) 1084.46/297.15 , x(X1, mark(X2)) -> mark(x(X1, X2)) 1084.46/297.15 , x(mark(X1), X2) -> mark(x(X1, X2)) 1084.46/297.15 , x(ok(X1), ok(X2)) -> ok(x(X1, X2)) 1084.46/297.15 , U11(mark(X1), X2, X3) -> mark(U11(X1, X2, X3)) 1084.46/297.15 , U11(ok(X1), ok(X2), ok(X3)) -> ok(U11(X1, X2, X3)) 1084.46/297.15 , U12(mark(X1), X2, X3) -> mark(U12(X1, X2, X3)) 1084.46/297.15 , U12(ok(X1), ok(X2), ok(X3)) -> ok(U12(X1, X2, X3)) 1084.46/297.15 , U13(mark(X1), X2, X3) -> mark(U13(X1, X2, X3)) 1084.46/297.15 , U13(ok(X1), ok(X2), ok(X3)) -> ok(U13(X1, X2, X3)) 1084.46/297.15 , U14(mark(X1), X2, X3) -> mark(U14(X1, X2, X3)) 1084.46/297.15 , U14(ok(X1), ok(X2), ok(X3)) -> ok(U14(X1, X2, X3)) 1084.46/297.15 , U15(mark(X1), X2) -> mark(U15(X1, X2)) 1084.46/297.15 , U15(ok(X1), ok(X2)) -> ok(U15(X1, X2)) 1084.46/297.15 , U16(mark(X)) -> mark(U16(X)) 1084.46/297.15 , U16(ok(X)) -> ok(U16(X)) 1084.46/297.15 , U21(mark(X1), X2) -> mark(U21(X1, X2)) 1084.46/297.15 , U21(ok(X1), ok(X2)) -> ok(U21(X1, X2)) 1084.46/297.15 , U22(mark(X1), X2) -> mark(U22(X1, X2)) 1084.46/297.15 , U22(ok(X1), ok(X2)) -> ok(U22(X1, X2)) 1084.46/297.15 , U23(mark(X)) -> mark(U23(X)) 1084.46/297.15 , U23(ok(X)) -> ok(U23(X)) 1084.46/297.15 , U31(mark(X1), X2, X3) -> mark(U31(X1, X2, X3)) 1084.46/297.15 , U31(ok(X1), ok(X2), ok(X3)) -> ok(U31(X1, X2, X3)) 1084.46/297.15 , U32(mark(X1), X2, X3) -> mark(U32(X1, X2, X3)) 1084.46/297.15 , U32(ok(X1), ok(X2), ok(X3)) -> ok(U32(X1, X2, X3)) 1084.46/297.15 , U33(mark(X1), X2, X3) -> mark(U33(X1, X2, X3)) 1084.46/297.15 , U33(ok(X1), ok(X2), ok(X3)) -> ok(U33(X1, X2, X3)) 1084.46/297.15 , U34(mark(X1), X2, X3) -> mark(U34(X1, X2, X3)) 1084.46/297.15 , U34(ok(X1), ok(X2), ok(X3)) -> ok(U34(X1, X2, X3)) 1084.46/297.15 , U35(mark(X1), X2) -> mark(U35(X1, X2)) 1084.46/297.15 , U35(ok(X1), ok(X2)) -> ok(U35(X1, X2)) 1084.46/297.15 , U36(mark(X)) -> mark(U36(X)) 1084.46/297.15 , U36(ok(X)) -> ok(U36(X)) 1084.46/297.15 , U41(mark(X1), X2) -> mark(U41(X1, X2)) 1084.46/297.15 , U41(ok(X1), ok(X2)) -> ok(U41(X1, X2)) 1084.46/297.15 , U42(mark(X)) -> mark(U42(X)) 1084.46/297.15 , U42(ok(X)) -> ok(U42(X)) 1084.46/297.15 , U51(mark(X)) -> mark(U51(X)) 1084.46/297.15 , U51(ok(X)) -> ok(U51(X)) 1084.46/297.15 , U61(mark(X1), X2) -> mark(U61(X1, X2)) 1084.46/297.15 , U61(ok(X1), ok(X2)) -> ok(U61(X1, X2)) 1084.46/297.15 , U62(mark(X)) -> mark(U62(X)) 1084.46/297.15 , U62(ok(X)) -> ok(U62(X)) 1084.46/297.15 , U71(mark(X1), X2) -> mark(U71(X1, X2)) 1084.46/297.15 , U71(ok(X1), ok(X2)) -> ok(U71(X1, X2)) 1084.46/297.15 , U72(mark(X1), X2) -> mark(U72(X1, X2)) 1084.46/297.15 , U72(ok(X1), ok(X2)) -> ok(U72(X1, X2)) 1084.46/297.15 , U81(mark(X1), X2, X3) -> mark(U81(X1, X2, X3)) 1084.46/297.15 , U81(ok(X1), ok(X2), ok(X3)) -> ok(U81(X1, X2, X3)) 1084.46/297.15 , U82(mark(X1), X2, X3) -> mark(U82(X1, X2, X3)) 1084.46/297.15 , U82(ok(X1), ok(X2), ok(X3)) -> ok(U82(X1, X2, X3)) 1084.46/297.15 , U83(mark(X1), X2, X3) -> mark(U83(X1, X2, X3)) 1084.46/297.15 , U83(ok(X1), ok(X2), ok(X3)) -> ok(U83(X1, X2, X3)) 1084.46/297.15 , U84(mark(X1), X2, X3) -> mark(U84(X1, X2, X3)) 1084.46/297.15 , U84(ok(X1), ok(X2), ok(X3)) -> ok(U84(X1, X2, X3)) 1084.46/297.15 , s(mark(X)) -> mark(s(X)) 1084.46/297.15 , s(ok(X)) -> ok(s(X)) 1084.46/297.15 , U91(mark(X1), X2) -> mark(U91(X1, X2)) 1084.46/297.15 , U91(ok(X1), ok(X2)) -> ok(U91(X1, X2)) 1084.46/297.15 , U92(mark(X)) -> mark(U92(X)) 1084.46/297.15 , U92(ok(X)) -> ok(U92(X)) 1084.46/297.15 , proper(U101(X1, X2, X3)) -> 1084.46/297.15 U101(proper(X1), proper(X2), proper(X3)) 1084.46/297.15 , proper(tt()) -> ok(tt()) 1084.46/297.15 , proper(U102(X1, X2, X3)) -> 1084.46/297.15 U102(proper(X1), proper(X2), proper(X3)) 1084.46/297.15 , proper(isNatKind(X)) -> isNatKind(proper(X)) 1084.46/297.15 , proper(U103(X1, X2, X3)) -> 1084.46/297.15 U103(proper(X1), proper(X2), proper(X3)) 1084.46/297.15 , proper(isNat(X)) -> isNat(proper(X)) 1084.46/297.15 , proper(U104(X1, X2, X3)) -> 1084.46/297.15 U104(proper(X1), proper(X2), proper(X3)) 1084.46/297.15 , proper(plus(X1, X2)) -> plus(proper(X1), proper(X2)) 1084.46/297.15 , proper(x(X1, X2)) -> x(proper(X1), proper(X2)) 1084.46/297.15 , proper(U11(X1, X2, X3)) -> 1084.46/297.15 U11(proper(X1), proper(X2), proper(X3)) 1084.46/297.15 , proper(U12(X1, X2, X3)) -> 1084.46/297.15 U12(proper(X1), proper(X2), proper(X3)) 1084.46/297.15 , proper(U13(X1, X2, X3)) -> 1084.46/297.15 U13(proper(X1), proper(X2), proper(X3)) 1084.46/297.15 , proper(U14(X1, X2, X3)) -> 1084.46/297.15 U14(proper(X1), proper(X2), proper(X3)) 1084.46/297.15 , proper(U15(X1, X2)) -> U15(proper(X1), proper(X2)) 1084.46/297.15 , proper(U16(X)) -> U16(proper(X)) 1084.46/297.15 , proper(U21(X1, X2)) -> U21(proper(X1), proper(X2)) 1084.46/297.15 , proper(U22(X1, X2)) -> U22(proper(X1), proper(X2)) 1084.46/297.15 , proper(U23(X)) -> U23(proper(X)) 1084.46/297.15 , proper(U31(X1, X2, X3)) -> 1084.46/297.15 U31(proper(X1), proper(X2), proper(X3)) 1084.46/297.15 , proper(U32(X1, X2, X3)) -> 1084.46/297.15 U32(proper(X1), proper(X2), proper(X3)) 1084.46/297.15 , proper(U33(X1, X2, X3)) -> 1084.46/297.15 U33(proper(X1), proper(X2), proper(X3)) 1084.46/297.15 , proper(U34(X1, X2, X3)) -> 1084.46/297.15 U34(proper(X1), proper(X2), proper(X3)) 1084.46/297.15 , proper(U35(X1, X2)) -> U35(proper(X1), proper(X2)) 1084.46/297.15 , proper(U36(X)) -> U36(proper(X)) 1084.46/297.15 , proper(U41(X1, X2)) -> U41(proper(X1), proper(X2)) 1084.46/297.15 , proper(U42(X)) -> U42(proper(X)) 1084.46/297.15 , proper(U51(X)) -> U51(proper(X)) 1084.46/297.15 , proper(U61(X1, X2)) -> U61(proper(X1), proper(X2)) 1084.46/297.15 , proper(U62(X)) -> U62(proper(X)) 1084.46/297.15 , proper(U71(X1, X2)) -> U71(proper(X1), proper(X2)) 1084.46/297.15 , proper(U72(X1, X2)) -> U72(proper(X1), proper(X2)) 1084.46/297.15 , proper(U81(X1, X2, X3)) -> 1084.46/297.15 U81(proper(X1), proper(X2), proper(X3)) 1084.46/297.15 , proper(U82(X1, X2, X3)) -> 1084.46/297.15 U82(proper(X1), proper(X2), proper(X3)) 1084.46/297.15 , proper(U83(X1, X2, X3)) -> 1084.46/297.15 U83(proper(X1), proper(X2), proper(X3)) 1084.46/297.15 , proper(U84(X1, X2, X3)) -> 1084.46/297.15 U84(proper(X1), proper(X2), proper(X3)) 1084.46/297.15 , proper(s(X)) -> s(proper(X)) 1084.46/297.15 , proper(U91(X1, X2)) -> U91(proper(X1), proper(X2)) 1084.46/297.15 , proper(U92(X)) -> U92(proper(X)) 1084.46/297.15 , proper(0()) -> ok(0()) 1084.46/297.15 , top(mark(X)) -> top(proper(X)) 1084.46/297.15 , top(ok(X)) -> top(active(X)) } 1084.46/297.15 Obligation: 1084.46/297.15 runtime complexity 1084.46/297.15 Answer: 1084.46/297.15 MAYBE 1084.46/297.15 1084.46/297.15 Consider the dependency graph: 1084.46/297.15 1084.46/297.15 1: active^#(U101(X1, X2, X3)) -> c_1(U101^#(active(X1), X2, X3)) 1084.46/297.15 -->_1 U101^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.15 c_83(U101^#(X1, X2, X3)) :83 1084.46/297.15 -->_1 U101^#(mark(X1), X2, X3) -> c_82(U101^#(X1, X2, X3)) :82 1084.46/297.15 1084.46/297.15 2: active^#(U101(tt(), M, N)) -> c_2(U102^#(isNatKind(M), M, N)) 1084.46/297.15 -->_1 U102^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.15 c_85(U102^#(X1, X2, X3)) :85 1084.46/297.15 -->_1 U102^#(mark(X1), X2, X3) -> c_84(U102^#(X1, X2, X3)) :84 1084.46/297.15 1084.46/297.15 3: active^#(U102(X1, X2, X3)) -> c_3(U102^#(active(X1), X2, X3)) 1084.46/297.15 -->_1 U102^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.15 c_85(U102^#(X1, X2, X3)) :85 1084.46/297.15 -->_1 U102^#(mark(X1), X2, X3) -> c_84(U102^#(X1, X2, X3)) :84 1084.46/297.15 1084.46/297.15 4: active^#(U102(tt(), M, N)) -> c_4(U103^#(isNat(N), M, N)) 1084.46/297.15 -->_1 U103^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.15 c_88(U103^#(X1, X2, X3)) :87 1084.46/297.15 -->_1 U103^#(mark(X1), X2, X3) -> c_87(U103^#(X1, X2, X3)) :86 1084.46/297.15 1084.46/297.15 5: active^#(isNatKind(plus(V1, V2))) -> 1084.46/297.15 c_5(U41^#(isNatKind(V1), V2)) 1084.46/297.15 -->_1 U41^#(ok(X1), ok(X2)) -> c_129(U41^#(X1, X2)) :89 1084.46/297.15 -->_1 U41^#(mark(X1), X2) -> c_128(U41^#(X1, X2)) :88 1084.46/297.15 1084.46/297.15 6: active^#(isNatKind(x(V1, V2))) -> c_6(U61^#(isNatKind(V1), V2)) 1084.46/297.15 -->_1 U61^#(ok(X1), ok(X2)) -> c_135(U61^#(X1, X2)) :91 1084.46/297.15 -->_1 U61^#(mark(X1), X2) -> c_134(U61^#(X1, X2)) :90 1084.46/297.15 1084.46/297.15 7: active^#(isNatKind(s(V1))) -> c_7(U51^#(isNatKind(V1))) 1084.46/297.15 -->_1 U51^#(ok(X)) -> c_133(U51^#(X)) :93 1084.46/297.15 -->_1 U51^#(mark(X)) -> c_132(U51^#(X)) :92 1084.46/297.15 1084.46/297.15 8: active^#(isNatKind(0())) -> c_8() 1084.46/297.15 1084.46/297.15 9: active^#(U103(X1, X2, X3)) -> c_9(U103^#(active(X1), X2, X3)) 1084.46/297.15 -->_1 U103^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.15 c_88(U103^#(X1, X2, X3)) :87 1084.46/297.15 -->_1 U103^#(mark(X1), X2, X3) -> c_87(U103^#(X1, X2, X3)) :86 1084.46/297.15 1084.46/297.15 10: active^#(U103(tt(), M, N)) -> c_10(U104^#(isNatKind(N), M, N)) 1084.46/297.15 -->_1 U104^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.15 c_91(U104^#(X1, X2, X3)) :95 1084.46/297.15 -->_1 U104^#(mark(X1), X2, X3) -> c_90(U104^#(X1, X2, X3)) :94 1084.46/297.15 1084.46/297.15 11: active^#(isNat(plus(V1, V2))) -> 1084.46/297.15 c_11(U11^#(isNatKind(V1), V1, V2)) 1084.46/297.15 -->_1 U11^#(ok(X1), ok(X2), ok(X3)) -> c_99(U11^#(X1, X2, X3)) :97 1084.46/297.15 -->_1 U11^#(mark(X1), X2, X3) -> c_98(U11^#(X1, X2, X3)) :96 1084.46/297.15 1084.46/297.15 12: active^#(isNat(x(V1, V2))) -> 1084.46/297.15 c_12(U31^#(isNatKind(V1), V1, V2)) 1084.46/297.15 -->_1 U31^#(ok(X1), ok(X2), ok(X3)) -> c_117(U31^#(X1, X2, X3)) :99 1084.46/297.15 -->_1 U31^#(mark(X1), X2, X3) -> c_116(U31^#(X1, X2, X3)) :98 1084.46/297.15 1084.46/297.15 13: active^#(isNat(s(V1))) -> c_13(U21^#(isNatKind(V1), V1)) 1084.46/297.15 -->_1 U21^#(ok(X1), ok(X2)) -> c_111(U21^#(X1, X2)) :101 1084.46/297.15 -->_1 U21^#(mark(X1), X2) -> c_110(U21^#(X1, X2)) :100 1084.46/297.15 1084.46/297.15 14: active^#(isNat(0())) -> c_14() 1084.46/297.15 1084.46/297.15 15: active^#(U104(X1, X2, X3)) -> c_15(U104^#(active(X1), X2, X3)) 1084.46/297.15 -->_1 U104^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.15 c_91(U104^#(X1, X2, X3)) :95 1084.46/297.15 -->_1 U104^#(mark(X1), X2, X3) -> c_90(U104^#(X1, X2, X3)) :94 1084.46/297.15 1084.46/297.15 16: active^#(U104(tt(), M, N)) -> c_16(plus^#(x(N, M), N)) 1084.46/297.15 -->_1 plus^#(ok(X1), ok(X2)) -> c_94(plus^#(X1, X2)) :104 1084.46/297.15 -->_1 plus^#(mark(X1), X2) -> c_93(plus^#(X1, X2)) :103 1084.46/297.15 -->_1 plus^#(X1, mark(X2)) -> c_92(plus^#(X1, X2)) :102 1084.46/297.15 1084.46/297.15 17: active^#(plus(X1, X2)) -> c_17(plus^#(X1, active(X2))) 1084.46/297.15 -->_1 plus^#(ok(X1), ok(X2)) -> c_94(plus^#(X1, X2)) :104 1084.46/297.15 -->_1 plus^#(mark(X1), X2) -> c_93(plus^#(X1, X2)) :103 1084.46/297.15 -->_1 plus^#(X1, mark(X2)) -> c_92(plus^#(X1, X2)) :102 1084.46/297.15 1084.46/297.15 18: active^#(plus(X1, X2)) -> c_18(plus^#(active(X1), X2)) 1084.46/297.15 -->_1 plus^#(ok(X1), ok(X2)) -> c_94(plus^#(X1, X2)) :104 1084.46/297.15 -->_1 plus^#(mark(X1), X2) -> c_93(plus^#(X1, X2)) :103 1084.46/297.15 -->_1 plus^#(X1, mark(X2)) -> c_92(plus^#(X1, X2)) :102 1084.46/297.15 1084.46/297.15 19: active^#(plus(N, s(M))) -> c_19(U81^#(isNat(M), M, N)) 1084.46/297.15 -->_1 U81^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.15 c_143(U81^#(X1, X2, X3)) :106 1084.46/297.15 -->_1 U81^#(mark(X1), X2, X3) -> c_142(U81^#(X1, X2, X3)) :105 1084.46/297.15 1084.46/297.15 20: active^#(plus(N, 0())) -> c_20(U71^#(isNat(N), N)) 1084.46/297.15 -->_1 U71^#(ok(X1), ok(X2)) -> c_139(U71^#(X1, X2)) :108 1084.46/297.15 -->_1 U71^#(mark(X1), X2) -> c_138(U71^#(X1, X2)) :107 1084.46/297.15 1084.46/297.15 21: active^#(x(X1, X2)) -> c_21(x^#(X1, active(X2))) 1084.46/297.15 -->_1 x^#(ok(X1), ok(X2)) -> c_97(x^#(X1, X2)) :111 1084.46/297.15 -->_1 x^#(mark(X1), X2) -> c_96(x^#(X1, X2)) :110 1084.46/297.15 -->_1 x^#(X1, mark(X2)) -> c_95(x^#(X1, X2)) :109 1084.46/297.15 1084.46/297.15 22: active^#(x(X1, X2)) -> c_22(x^#(active(X1), X2)) 1084.46/297.15 -->_1 x^#(ok(X1), ok(X2)) -> c_97(x^#(X1, X2)) :111 1084.46/297.15 -->_1 x^#(mark(X1), X2) -> c_96(x^#(X1, X2)) :110 1084.46/297.15 -->_1 x^#(X1, mark(X2)) -> c_95(x^#(X1, X2)) :109 1084.46/297.15 1084.46/297.15 23: active^#(x(N, s(M))) -> c_23(U101^#(isNat(M), M, N)) 1084.46/297.15 -->_1 U101^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.15 c_83(U101^#(X1, X2, X3)) :83 1084.46/297.15 -->_1 U101^#(mark(X1), X2, X3) -> c_82(U101^#(X1, X2, X3)) :82 1084.46/297.15 1084.46/297.15 24: active^#(x(N, 0())) -> c_24(U91^#(isNat(N), N)) 1084.46/297.15 -->_1 U91^#(ok(X1), ok(X2)) -> c_153(U91^#(X1, X2)) :113 1084.46/297.15 -->_1 U91^#(mark(X1), X2) -> c_152(U91^#(X1, X2)) :112 1084.46/297.15 1084.46/297.15 25: active^#(U11(X1, X2, X3)) -> c_25(U11^#(active(X1), X2, X3)) 1084.46/297.15 -->_1 U11^#(ok(X1), ok(X2), ok(X3)) -> c_99(U11^#(X1, X2, X3)) :97 1084.46/297.15 -->_1 U11^#(mark(X1), X2, X3) -> c_98(U11^#(X1, X2, X3)) :96 1084.46/297.15 1084.46/297.15 26: active^#(U11(tt(), V1, V2)) -> 1084.46/297.15 c_26(U12^#(isNatKind(V1), V1, V2)) 1084.46/297.15 -->_1 U12^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.15 c_101(U12^#(X1, X2, X3)) :115 1084.46/297.15 -->_1 U12^#(mark(X1), X2, X3) -> c_100(U12^#(X1, X2, X3)) :114 1084.46/297.15 1084.46/297.15 27: active^#(U12(X1, X2, X3)) -> c_27(U12^#(active(X1), X2, X3)) 1084.46/297.15 -->_1 U12^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.15 c_101(U12^#(X1, X2, X3)) :115 1084.46/297.15 -->_1 U12^#(mark(X1), X2, X3) -> c_100(U12^#(X1, X2, X3)) :114 1084.46/297.15 1084.46/297.15 28: active^#(U12(tt(), V1, V2)) -> 1084.46/297.15 c_28(U13^#(isNatKind(V2), V1, V2)) 1084.46/297.15 -->_1 U13^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.15 c_103(U13^#(X1, X2, X3)) :117 1084.46/297.15 -->_1 U13^#(mark(X1), X2, X3) -> c_102(U13^#(X1, X2, X3)) :116 1084.46/297.15 1084.46/297.15 29: active^#(U13(X1, X2, X3)) -> c_29(U13^#(active(X1), X2, X3)) 1084.46/297.15 -->_1 U13^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.15 c_103(U13^#(X1, X2, X3)) :117 1084.46/297.15 -->_1 U13^#(mark(X1), X2, X3) -> c_102(U13^#(X1, X2, X3)) :116 1084.46/297.15 1084.46/297.15 30: active^#(U13(tt(), V1, V2)) -> 1084.46/297.15 c_30(U14^#(isNatKind(V2), V1, V2)) 1084.46/297.15 -->_1 U14^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.15 c_105(U14^#(X1, X2, X3)) :119 1084.46/297.15 -->_1 U14^#(mark(X1), X2, X3) -> c_104(U14^#(X1, X2, X3)) :118 1084.46/297.15 1084.46/297.15 31: active^#(U14(X1, X2, X3)) -> c_31(U14^#(active(X1), X2, X3)) 1084.46/297.15 -->_1 U14^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.15 c_105(U14^#(X1, X2, X3)) :119 1084.46/297.15 -->_1 U14^#(mark(X1), X2, X3) -> c_104(U14^#(X1, X2, X3)) :118 1084.46/297.15 1084.46/297.15 32: active^#(U14(tt(), V1, V2)) -> c_32(U15^#(isNat(V1), V2)) 1084.46/297.15 -->_1 U15^#(ok(X1), ok(X2)) -> c_107(U15^#(X1, X2)) :121 1084.46/297.15 -->_1 U15^#(mark(X1), X2) -> c_106(U15^#(X1, X2)) :120 1084.46/297.15 1084.46/297.15 33: active^#(U15(X1, X2)) -> c_33(U15^#(active(X1), X2)) 1084.46/297.15 -->_1 U15^#(ok(X1), ok(X2)) -> c_107(U15^#(X1, X2)) :121 1084.46/297.15 -->_1 U15^#(mark(X1), X2) -> c_106(U15^#(X1, X2)) :120 1084.46/297.15 1084.46/297.15 34: active^#(U15(tt(), V2)) -> c_34(U16^#(isNat(V2))) 1084.46/297.15 -->_1 U16^#(ok(X)) -> c_109(U16^#(X)) :123 1084.46/297.15 -->_1 U16^#(mark(X)) -> c_108(U16^#(X)) :122 1084.46/297.15 1084.46/297.15 35: active^#(U16(X)) -> c_35(U16^#(active(X))) 1084.46/297.15 -->_1 U16^#(ok(X)) -> c_109(U16^#(X)) :123 1084.46/297.15 -->_1 U16^#(mark(X)) -> c_108(U16^#(X)) :122 1084.46/297.15 1084.46/297.15 36: active^#(U16(tt())) -> c_36() 1084.46/297.15 1084.46/297.15 37: active^#(U21(X1, X2)) -> c_37(U21^#(active(X1), X2)) 1084.46/297.15 -->_1 U21^#(ok(X1), ok(X2)) -> c_111(U21^#(X1, X2)) :101 1084.46/297.15 -->_1 U21^#(mark(X1), X2) -> c_110(U21^#(X1, X2)) :100 1084.46/297.15 1084.46/297.15 38: active^#(U21(tt(), V1)) -> c_38(U22^#(isNatKind(V1), V1)) 1084.46/297.15 -->_1 U22^#(ok(X1), ok(X2)) -> c_113(U22^#(X1, X2)) :125 1084.46/297.15 -->_1 U22^#(mark(X1), X2) -> c_112(U22^#(X1, X2)) :124 1084.46/297.15 1084.46/297.15 39: active^#(U22(X1, X2)) -> c_39(U22^#(active(X1), X2)) 1084.46/297.15 -->_1 U22^#(ok(X1), ok(X2)) -> c_113(U22^#(X1, X2)) :125 1084.46/297.15 -->_1 U22^#(mark(X1), X2) -> c_112(U22^#(X1, X2)) :124 1084.46/297.15 1084.46/297.15 40: active^#(U22(tt(), V1)) -> c_40(U23^#(isNat(V1))) 1084.46/297.15 -->_1 U23^#(ok(X)) -> c_115(U23^#(X)) :127 1084.46/297.15 -->_1 U23^#(mark(X)) -> c_114(U23^#(X)) :126 1084.46/297.15 1084.46/297.15 41: active^#(U23(X)) -> c_41(U23^#(active(X))) 1084.46/297.15 -->_1 U23^#(ok(X)) -> c_115(U23^#(X)) :127 1084.46/297.15 -->_1 U23^#(mark(X)) -> c_114(U23^#(X)) :126 1084.46/297.15 1084.46/297.15 42: active^#(U23(tt())) -> c_42() 1084.46/297.15 1084.46/297.15 43: active^#(U31(X1, X2, X3)) -> c_43(U31^#(active(X1), X2, X3)) 1084.46/297.15 -->_1 U31^#(ok(X1), ok(X2), ok(X3)) -> c_117(U31^#(X1, X2, X3)) :99 1084.46/297.15 -->_1 U31^#(mark(X1), X2, X3) -> c_116(U31^#(X1, X2, X3)) :98 1084.46/297.15 1084.46/297.15 44: active^#(U31(tt(), V1, V2)) -> 1084.46/297.15 c_44(U32^#(isNatKind(V1), V1, V2)) 1084.46/297.15 -->_1 U32^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.15 c_119(U32^#(X1, X2, X3)) :129 1084.46/297.15 -->_1 U32^#(mark(X1), X2, X3) -> c_118(U32^#(X1, X2, X3)) :128 1084.46/297.15 1084.46/297.15 45: active^#(U32(X1, X2, X3)) -> c_45(U32^#(active(X1), X2, X3)) 1084.46/297.15 -->_1 U32^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.15 c_119(U32^#(X1, X2, X3)) :129 1084.46/297.15 -->_1 U32^#(mark(X1), X2, X3) -> c_118(U32^#(X1, X2, X3)) :128 1084.46/297.15 1084.46/297.15 46: active^#(U32(tt(), V1, V2)) -> 1084.46/297.15 c_46(U33^#(isNatKind(V2), V1, V2)) 1084.46/297.15 -->_1 U33^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.15 c_121(U33^#(X1, X2, X3)) :131 1084.46/297.15 -->_1 U33^#(mark(X1), X2, X3) -> c_120(U33^#(X1, X2, X3)) :130 1084.46/297.15 1084.46/297.15 47: active^#(U33(X1, X2, X3)) -> c_47(U33^#(active(X1), X2, X3)) 1084.46/297.15 -->_1 U33^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.15 c_121(U33^#(X1, X2, X3)) :131 1084.46/297.15 -->_1 U33^#(mark(X1), X2, X3) -> c_120(U33^#(X1, X2, X3)) :130 1084.46/297.15 1084.46/297.15 48: active^#(U33(tt(), V1, V2)) -> 1084.46/297.15 c_48(U34^#(isNatKind(V2), V1, V2)) 1084.46/297.15 -->_1 U34^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.15 c_123(U34^#(X1, X2, X3)) :133 1084.46/297.15 -->_1 U34^#(mark(X1), X2, X3) -> c_122(U34^#(X1, X2, X3)) :132 1084.46/297.15 1084.46/297.15 49: active^#(U34(X1, X2, X3)) -> c_49(U34^#(active(X1), X2, X3)) 1084.46/297.15 -->_1 U34^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.15 c_123(U34^#(X1, X2, X3)) :133 1084.46/297.15 -->_1 U34^#(mark(X1), X2, X3) -> c_122(U34^#(X1, X2, X3)) :132 1084.46/297.15 1084.46/297.15 50: active^#(U34(tt(), V1, V2)) -> c_50(U35^#(isNat(V1), V2)) 1084.46/297.15 -->_1 U35^#(ok(X1), ok(X2)) -> c_125(U35^#(X1, X2)) :135 1084.46/297.15 -->_1 U35^#(mark(X1), X2) -> c_124(U35^#(X1, X2)) :134 1084.46/297.15 1084.46/297.15 51: active^#(U35(X1, X2)) -> c_51(U35^#(active(X1), X2)) 1084.46/297.16 -->_1 U35^#(ok(X1), ok(X2)) -> c_125(U35^#(X1, X2)) :135 1084.46/297.16 -->_1 U35^#(mark(X1), X2) -> c_124(U35^#(X1, X2)) :134 1084.46/297.16 1084.46/297.16 52: active^#(U35(tt(), V2)) -> c_52(U36^#(isNat(V2))) 1084.46/297.16 -->_1 U36^#(ok(X)) -> c_127(U36^#(X)) :137 1084.46/297.16 -->_1 U36^#(mark(X)) -> c_126(U36^#(X)) :136 1084.46/297.16 1084.46/297.16 53: active^#(U36(X)) -> c_53(U36^#(active(X))) 1084.46/297.16 -->_1 U36^#(ok(X)) -> c_127(U36^#(X)) :137 1084.46/297.16 -->_1 U36^#(mark(X)) -> c_126(U36^#(X)) :136 1084.46/297.16 1084.46/297.16 54: active^#(U36(tt())) -> c_54() 1084.46/297.16 1084.46/297.16 55: active^#(U41(X1, X2)) -> c_55(U41^#(active(X1), X2)) 1084.46/297.16 -->_1 U41^#(ok(X1), ok(X2)) -> c_129(U41^#(X1, X2)) :89 1084.46/297.16 -->_1 U41^#(mark(X1), X2) -> c_128(U41^#(X1, X2)) :88 1084.46/297.16 1084.46/297.16 56: active^#(U41(tt(), V2)) -> c_56(U42^#(isNatKind(V2))) 1084.46/297.16 -->_1 U42^#(ok(X)) -> c_131(U42^#(X)) :139 1084.46/297.16 -->_1 U42^#(mark(X)) -> c_130(U42^#(X)) :138 1084.46/297.16 1084.46/297.16 57: active^#(U42(X)) -> c_57(U42^#(active(X))) 1084.46/297.16 -->_1 U42^#(ok(X)) -> c_131(U42^#(X)) :139 1084.46/297.16 -->_1 U42^#(mark(X)) -> c_130(U42^#(X)) :138 1084.46/297.16 1084.46/297.16 58: active^#(U42(tt())) -> c_58() 1084.46/297.16 1084.46/297.16 59: active^#(U51(X)) -> c_59(U51^#(active(X))) 1084.46/297.16 -->_1 U51^#(ok(X)) -> c_133(U51^#(X)) :93 1084.46/297.16 -->_1 U51^#(mark(X)) -> c_132(U51^#(X)) :92 1084.46/297.16 1084.46/297.16 60: active^#(U51(tt())) -> c_60() 1084.46/297.16 1084.46/297.16 61: active^#(U61(X1, X2)) -> c_61(U61^#(active(X1), X2)) 1084.46/297.16 -->_1 U61^#(ok(X1), ok(X2)) -> c_135(U61^#(X1, X2)) :91 1084.46/297.16 -->_1 U61^#(mark(X1), X2) -> c_134(U61^#(X1, X2)) :90 1084.46/297.16 1084.46/297.16 62: active^#(U61(tt(), V2)) -> c_62(U62^#(isNatKind(V2))) 1084.46/297.16 -->_1 U62^#(ok(X)) -> c_137(U62^#(X)) :141 1084.46/297.16 -->_1 U62^#(mark(X)) -> c_136(U62^#(X)) :140 1084.46/297.16 1084.46/297.16 63: active^#(U62(X)) -> c_63(U62^#(active(X))) 1084.46/297.16 -->_1 U62^#(ok(X)) -> c_137(U62^#(X)) :141 1084.46/297.16 -->_1 U62^#(mark(X)) -> c_136(U62^#(X)) :140 1084.46/297.16 1084.46/297.16 64: active^#(U62(tt())) -> c_64() 1084.46/297.16 1084.46/297.16 65: active^#(U71(X1, X2)) -> c_65(U71^#(active(X1), X2)) 1084.46/297.16 -->_1 U71^#(ok(X1), ok(X2)) -> c_139(U71^#(X1, X2)) :108 1084.46/297.16 -->_1 U71^#(mark(X1), X2) -> c_138(U71^#(X1, X2)) :107 1084.46/297.16 1084.46/297.16 66: active^#(U71(tt(), N)) -> c_66(U72^#(isNatKind(N), N)) 1084.46/297.16 -->_1 U72^#(ok(X1), ok(X2)) -> c_141(U72^#(X1, X2)) :143 1084.46/297.16 -->_1 U72^#(mark(X1), X2) -> c_140(U72^#(X1, X2)) :142 1084.46/297.16 1084.46/297.16 67: active^#(U72(X1, X2)) -> c_67(U72^#(active(X1), X2)) 1084.46/297.16 -->_1 U72^#(ok(X1), ok(X2)) -> c_141(U72^#(X1, X2)) :143 1084.46/297.16 -->_1 U72^#(mark(X1), X2) -> c_140(U72^#(X1, X2)) :142 1084.46/297.16 1084.46/297.16 68: active^#(U72(tt(), N)) -> c_68(N) 1084.46/297.16 -->_1 top^#(ok(X)) -> c_196(top^#(active(X))) :196 1084.46/297.16 -->_1 top^#(mark(X)) -> c_195(top^#(proper(X))) :195 1084.46/297.16 -->_1 proper^#(U92(X)) -> c_193(U92^#(proper(X))) :193 1084.46/297.16 -->_1 proper^#(U91(X1, X2)) -> 1084.46/297.16 c_192(U91^#(proper(X1), proper(X2))) :192 1084.46/297.16 -->_1 proper^#(s(X)) -> c_191(s^#(proper(X))) :191 1084.46/297.16 -->_1 proper^#(U84(X1, X2, X3)) -> 1084.46/297.16 c_190(U84^#(proper(X1), proper(X2), proper(X3))) :190 1084.46/297.16 -->_1 proper^#(U83(X1, X2, X3)) -> 1084.46/297.16 c_189(U83^#(proper(X1), proper(X2), proper(X3))) :189 1084.46/297.16 -->_1 proper^#(U82(X1, X2, X3)) -> 1084.46/297.16 c_188(U82^#(proper(X1), proper(X2), proper(X3))) :188 1084.46/297.16 -->_1 proper^#(U81(X1, X2, X3)) -> 1084.46/297.16 c_187(U81^#(proper(X1), proper(X2), proper(X3))) :187 1084.46/297.16 -->_1 proper^#(U72(X1, X2)) -> 1084.46/297.16 c_186(U72^#(proper(X1), proper(X2))) :186 1084.46/297.16 -->_1 proper^#(U71(X1, X2)) -> 1084.46/297.16 c_185(U71^#(proper(X1), proper(X2))) :185 1084.46/297.16 -->_1 proper^#(U62(X)) -> c_184(U62^#(proper(X))) :184 1084.46/297.16 -->_1 proper^#(U61(X1, X2)) -> 1084.46/297.16 c_183(U61^#(proper(X1), proper(X2))) :183 1084.46/297.16 -->_1 proper^#(U51(X)) -> c_182(U51^#(proper(X))) :182 1084.46/297.16 -->_1 proper^#(U42(X)) -> c_181(U42^#(proper(X))) :181 1084.46/297.16 -->_1 proper^#(U41(X1, X2)) -> 1084.46/297.16 c_180(U41^#(proper(X1), proper(X2))) :180 1084.46/297.16 -->_1 proper^#(U36(X)) -> c_179(U36^#(proper(X))) :179 1084.46/297.16 -->_1 proper^#(U35(X1, X2)) -> 1084.46/297.16 c_178(U35^#(proper(X1), proper(X2))) :178 1084.46/297.16 -->_1 proper^#(U34(X1, X2, X3)) -> 1084.46/297.16 c_177(U34^#(proper(X1), proper(X2), proper(X3))) :177 1084.46/297.16 -->_1 proper^#(U33(X1, X2, X3)) -> 1084.46/297.16 c_176(U33^#(proper(X1), proper(X2), proper(X3))) :176 1084.46/297.16 -->_1 proper^#(U32(X1, X2, X3)) -> 1084.46/297.16 c_175(U32^#(proper(X1), proper(X2), proper(X3))) :175 1084.46/297.16 -->_1 proper^#(U31(X1, X2, X3)) -> 1084.46/297.16 c_174(U31^#(proper(X1), proper(X2), proper(X3))) :174 1084.46/297.16 -->_1 proper^#(U23(X)) -> c_173(U23^#(proper(X))) :173 1084.46/297.16 -->_1 proper^#(U22(X1, X2)) -> 1084.46/297.16 c_172(U22^#(proper(X1), proper(X2))) :172 1084.46/297.16 -->_1 proper^#(U21(X1, X2)) -> 1084.46/297.16 c_171(U21^#(proper(X1), proper(X2))) :171 1084.46/297.16 -->_1 proper^#(U16(X)) -> c_170(U16^#(proper(X))) :170 1084.46/297.16 -->_1 proper^#(U15(X1, X2)) -> 1084.46/297.16 c_169(U15^#(proper(X1), proper(X2))) :169 1084.46/297.16 -->_1 proper^#(U14(X1, X2, X3)) -> 1084.46/297.16 c_168(U14^#(proper(X1), proper(X2), proper(X3))) :168 1084.46/297.16 -->_1 proper^#(U13(X1, X2, X3)) -> 1084.46/297.16 c_167(U13^#(proper(X1), proper(X2), proper(X3))) :167 1084.46/297.16 -->_1 proper^#(U12(X1, X2, X3)) -> 1084.46/297.16 c_166(U12^#(proper(X1), proper(X2), proper(X3))) :166 1084.46/297.16 -->_1 proper^#(U11(X1, X2, X3)) -> 1084.46/297.16 c_165(U11^#(proper(X1), proper(X2), proper(X3))) :165 1084.46/297.16 -->_1 proper^#(x(X1, X2)) -> 1084.46/297.16 c_164(x^#(proper(X1), proper(X2))) :164 1084.46/297.16 -->_1 proper^#(plus(X1, X2)) -> 1084.46/297.16 c_163(plus^#(proper(X1), proper(X2))) :163 1084.46/297.16 -->_1 proper^#(U104(X1, X2, X3)) -> 1084.46/297.16 c_162(U104^#(proper(X1), proper(X2), proper(X3))) :162 1084.46/297.16 -->_1 proper^#(isNat(X)) -> c_161(isNat^#(proper(X))) :161 1084.46/297.16 -->_1 proper^#(U103(X1, X2, X3)) -> 1084.46/297.16 c_160(U103^#(proper(X1), proper(X2), proper(X3))) :160 1084.46/297.16 -->_1 proper^#(isNatKind(X)) -> c_159(isNatKind^#(proper(X))) :159 1084.46/297.16 -->_1 proper^#(U102(X1, X2, X3)) -> 1084.46/297.16 c_158(U102^#(proper(X1), proper(X2), proper(X3))) :158 1084.46/297.16 -->_1 proper^#(U101(X1, X2, X3)) -> 1084.46/297.16 c_156(U101^#(proper(X1), proper(X2), proper(X3))) :156 1084.46/297.16 -->_1 isNat^#(ok(X)) -> c_89(isNat^#(X)) :155 1084.46/297.16 -->_1 isNatKind^#(ok(X)) -> c_86(isNatKind^#(X)) :154 1084.46/297.16 -->_1 U92^#(ok(X)) -> c_155(U92^#(X)) :153 1084.46/297.16 -->_1 U92^#(mark(X)) -> c_154(U92^#(X)) :152 1084.46/297.16 -->_1 s^#(ok(X)) -> c_151(s^#(X)) :151 1084.46/297.16 -->_1 s^#(mark(X)) -> c_150(s^#(X)) :150 1084.46/297.16 -->_1 U84^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.16 c_149(U84^#(X1, X2, X3)) :149 1084.46/297.16 -->_1 U84^#(mark(X1), X2, X3) -> c_148(U84^#(X1, X2, X3)) :148 1084.46/297.16 -->_1 U83^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.16 c_147(U83^#(X1, X2, X3)) :147 1084.46/297.16 -->_1 U83^#(mark(X1), X2, X3) -> c_146(U83^#(X1, X2, X3)) :146 1084.46/297.16 -->_1 U82^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.16 c_145(U82^#(X1, X2, X3)) :145 1084.46/297.16 -->_1 U82^#(mark(X1), X2, X3) -> c_144(U82^#(X1, X2, X3)) :144 1084.46/297.16 -->_1 U72^#(ok(X1), ok(X2)) -> c_141(U72^#(X1, X2)) :143 1084.46/297.16 -->_1 U72^#(mark(X1), X2) -> c_140(U72^#(X1, X2)) :142 1084.46/297.16 -->_1 U62^#(ok(X)) -> c_137(U62^#(X)) :141 1084.46/297.16 -->_1 U62^#(mark(X)) -> c_136(U62^#(X)) :140 1084.46/297.16 -->_1 U42^#(ok(X)) -> c_131(U42^#(X)) :139 1084.46/297.16 -->_1 U42^#(mark(X)) -> c_130(U42^#(X)) :138 1084.46/297.16 -->_1 U36^#(ok(X)) -> c_127(U36^#(X)) :137 1084.46/297.16 -->_1 U36^#(mark(X)) -> c_126(U36^#(X)) :136 1084.46/297.16 -->_1 U35^#(ok(X1), ok(X2)) -> c_125(U35^#(X1, X2)) :135 1084.46/297.16 -->_1 U35^#(mark(X1), X2) -> c_124(U35^#(X1, X2)) :134 1084.46/297.16 -->_1 U34^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.16 c_123(U34^#(X1, X2, X3)) :133 1084.46/297.16 -->_1 U34^#(mark(X1), X2, X3) -> c_122(U34^#(X1, X2, X3)) :132 1084.46/297.16 -->_1 U33^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.16 c_121(U33^#(X1, X2, X3)) :131 1084.46/297.16 -->_1 U33^#(mark(X1), X2, X3) -> c_120(U33^#(X1, X2, X3)) :130 1084.46/297.16 -->_1 U32^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.16 c_119(U32^#(X1, X2, X3)) :129 1084.46/297.16 -->_1 U32^#(mark(X1), X2, X3) -> c_118(U32^#(X1, X2, X3)) :128 1084.46/297.16 -->_1 U23^#(ok(X)) -> c_115(U23^#(X)) :127 1084.46/297.16 -->_1 U23^#(mark(X)) -> c_114(U23^#(X)) :126 1084.46/297.16 -->_1 U22^#(ok(X1), ok(X2)) -> c_113(U22^#(X1, X2)) :125 1084.46/297.16 -->_1 U22^#(mark(X1), X2) -> c_112(U22^#(X1, X2)) :124 1084.46/297.16 -->_1 U16^#(ok(X)) -> c_109(U16^#(X)) :123 1084.46/297.16 -->_1 U16^#(mark(X)) -> c_108(U16^#(X)) :122 1084.46/297.16 -->_1 U15^#(ok(X1), ok(X2)) -> c_107(U15^#(X1, X2)) :121 1084.46/297.16 -->_1 U15^#(mark(X1), X2) -> c_106(U15^#(X1, X2)) :120 1084.46/297.16 -->_1 U14^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.16 c_105(U14^#(X1, X2, X3)) :119 1084.46/297.16 -->_1 U14^#(mark(X1), X2, X3) -> c_104(U14^#(X1, X2, X3)) :118 1084.46/297.16 -->_1 U13^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.16 c_103(U13^#(X1, X2, X3)) :117 1084.46/297.16 -->_1 U13^#(mark(X1), X2, X3) -> c_102(U13^#(X1, X2, X3)) :116 1084.46/297.16 -->_1 U12^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.16 c_101(U12^#(X1, X2, X3)) :115 1084.46/297.16 -->_1 U12^#(mark(X1), X2, X3) -> c_100(U12^#(X1, X2, X3)) :114 1084.46/297.16 -->_1 U91^#(ok(X1), ok(X2)) -> c_153(U91^#(X1, X2)) :113 1084.46/297.16 -->_1 U91^#(mark(X1), X2) -> c_152(U91^#(X1, X2)) :112 1084.46/297.16 -->_1 x^#(ok(X1), ok(X2)) -> c_97(x^#(X1, X2)) :111 1084.46/297.16 -->_1 x^#(mark(X1), X2) -> c_96(x^#(X1, X2)) :110 1084.46/297.16 -->_1 x^#(X1, mark(X2)) -> c_95(x^#(X1, X2)) :109 1084.46/297.16 -->_1 U71^#(ok(X1), ok(X2)) -> c_139(U71^#(X1, X2)) :108 1084.46/297.16 -->_1 U71^#(mark(X1), X2) -> c_138(U71^#(X1, X2)) :107 1084.46/297.16 -->_1 U81^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.16 c_143(U81^#(X1, X2, X3)) :106 1084.46/297.16 -->_1 U81^#(mark(X1), X2, X3) -> c_142(U81^#(X1, X2, X3)) :105 1084.46/297.16 -->_1 plus^#(ok(X1), ok(X2)) -> c_94(plus^#(X1, X2)) :104 1084.46/297.16 -->_1 plus^#(mark(X1), X2) -> c_93(plus^#(X1, X2)) :103 1084.46/297.16 -->_1 plus^#(X1, mark(X2)) -> c_92(plus^#(X1, X2)) :102 1084.46/297.16 -->_1 U21^#(ok(X1), ok(X2)) -> c_111(U21^#(X1, X2)) :101 1084.46/297.16 -->_1 U21^#(mark(X1), X2) -> c_110(U21^#(X1, X2)) :100 1084.46/297.16 -->_1 U31^#(ok(X1), ok(X2), ok(X3)) -> c_117(U31^#(X1, X2, X3)) :99 1084.46/297.16 -->_1 U31^#(mark(X1), X2, X3) -> c_116(U31^#(X1, X2, X3)) :98 1084.46/297.16 -->_1 U11^#(ok(X1), ok(X2), ok(X3)) -> c_99(U11^#(X1, X2, X3)) :97 1084.46/297.16 -->_1 U11^#(mark(X1), X2, X3) -> c_98(U11^#(X1, X2, X3)) :96 1084.46/297.16 -->_1 U104^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.16 c_91(U104^#(X1, X2, X3)) :95 1084.46/297.16 -->_1 U104^#(mark(X1), X2, X3) -> c_90(U104^#(X1, X2, X3)) :94 1084.46/297.16 -->_1 U51^#(ok(X)) -> c_133(U51^#(X)) :93 1084.46/297.16 -->_1 U51^#(mark(X)) -> c_132(U51^#(X)) :92 1084.46/297.16 -->_1 U61^#(ok(X1), ok(X2)) -> c_135(U61^#(X1, X2)) :91 1084.46/297.16 -->_1 U61^#(mark(X1), X2) -> c_134(U61^#(X1, X2)) :90 1084.46/297.16 -->_1 U41^#(ok(X1), ok(X2)) -> c_129(U41^#(X1, X2)) :89 1084.46/297.16 -->_1 U41^#(mark(X1), X2) -> c_128(U41^#(X1, X2)) :88 1084.46/297.16 -->_1 U103^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.16 c_88(U103^#(X1, X2, X3)) :87 1084.46/297.16 -->_1 U103^#(mark(X1), X2, X3) -> c_87(U103^#(X1, X2, X3)) :86 1084.46/297.16 -->_1 U102^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.16 c_85(U102^#(X1, X2, X3)) :85 1084.46/297.16 -->_1 U102^#(mark(X1), X2, X3) -> c_84(U102^#(X1, X2, X3)) :84 1084.46/297.16 -->_1 U101^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.16 c_83(U101^#(X1, X2, X3)) :83 1084.46/297.16 -->_1 U101^#(mark(X1), X2, X3) -> c_82(U101^#(X1, X2, X3)) :82 1084.46/297.16 -->_1 active^#(U92(X)) -> c_80(U92^#(active(X))) :80 1084.46/297.16 -->_1 active^#(U91(tt(), N)) -> c_79(U92^#(isNatKind(N))) :79 1084.46/297.16 -->_1 active^#(U91(X1, X2)) -> c_78(U91^#(active(X1), X2)) :78 1084.46/297.16 -->_1 active^#(s(X)) -> c_77(s^#(active(X))) :77 1084.46/297.16 -->_1 active^#(U84(tt(), M, N)) -> c_76(s^#(plus(N, M))) :76 1084.46/297.16 -->_1 active^#(U84(X1, X2, X3)) -> 1084.46/297.16 c_75(U84^#(active(X1), X2, X3)) :75 1084.46/297.16 -->_1 active^#(U83(tt(), M, N)) -> 1084.46/297.16 c_74(U84^#(isNatKind(N), M, N)) :74 1084.46/297.16 -->_1 active^#(U83(X1, X2, X3)) -> 1084.46/297.16 c_73(U83^#(active(X1), X2, X3)) :73 1084.46/297.16 -->_1 active^#(U82(tt(), M, N)) -> c_72(U83^#(isNat(N), M, N)) :72 1084.46/297.16 -->_1 active^#(U82(X1, X2, X3)) -> 1084.46/297.16 c_71(U82^#(active(X1), X2, X3)) :71 1084.46/297.16 -->_1 active^#(U81(tt(), M, N)) -> 1084.46/297.16 c_70(U82^#(isNatKind(M), M, N)) :70 1084.46/297.16 -->_1 active^#(U81(X1, X2, X3)) -> 1084.46/297.16 c_69(U81^#(active(X1), X2, X3)) :69 1084.46/297.16 -->_1 proper^#(0()) -> c_194() :194 1084.46/297.16 -->_1 proper^#(tt()) -> c_157() :157 1084.46/297.16 -->_1 active^#(U92(tt())) -> c_81() :81 1084.46/297.16 -->_1 active^#(U72(tt(), N)) -> c_68(N) :68 1084.46/297.16 -->_1 active^#(U72(X1, X2)) -> c_67(U72^#(active(X1), X2)) :67 1084.46/297.16 -->_1 active^#(U71(tt(), N)) -> c_66(U72^#(isNatKind(N), N)) :66 1084.46/297.16 -->_1 active^#(U71(X1, X2)) -> c_65(U71^#(active(X1), X2)) :65 1084.46/297.16 -->_1 active^#(U62(tt())) -> c_64() :64 1084.46/297.16 -->_1 active^#(U62(X)) -> c_63(U62^#(active(X))) :63 1084.46/297.16 -->_1 active^#(U61(tt(), V2)) -> c_62(U62^#(isNatKind(V2))) :62 1084.46/297.16 -->_1 active^#(U61(X1, X2)) -> c_61(U61^#(active(X1), X2)) :61 1084.46/297.16 -->_1 active^#(U51(tt())) -> c_60() :60 1084.46/297.16 -->_1 active^#(U51(X)) -> c_59(U51^#(active(X))) :59 1084.46/297.16 -->_1 active^#(U42(tt())) -> c_58() :58 1084.46/297.16 -->_1 active^#(U42(X)) -> c_57(U42^#(active(X))) :57 1084.46/297.16 -->_1 active^#(U41(tt(), V2)) -> c_56(U42^#(isNatKind(V2))) :56 1084.46/297.16 -->_1 active^#(U41(X1, X2)) -> c_55(U41^#(active(X1), X2)) :55 1084.46/297.16 -->_1 active^#(U36(tt())) -> c_54() :54 1084.46/297.16 -->_1 active^#(U36(X)) -> c_53(U36^#(active(X))) :53 1084.46/297.16 -->_1 active^#(U35(tt(), V2)) -> c_52(U36^#(isNat(V2))) :52 1084.46/297.16 -->_1 active^#(U35(X1, X2)) -> c_51(U35^#(active(X1), X2)) :51 1084.46/297.16 -->_1 active^#(U34(tt(), V1, V2)) -> c_50(U35^#(isNat(V1), V2)) :50 1084.46/297.16 -->_1 active^#(U34(X1, X2, X3)) -> 1084.46/297.16 c_49(U34^#(active(X1), X2, X3)) :49 1084.46/297.16 -->_1 active^#(U33(tt(), V1, V2)) -> 1084.46/297.16 c_48(U34^#(isNatKind(V2), V1, V2)) :48 1084.46/297.16 -->_1 active^#(U33(X1, X2, X3)) -> 1084.46/297.16 c_47(U33^#(active(X1), X2, X3)) :47 1084.46/297.16 -->_1 active^#(U32(tt(), V1, V2)) -> 1084.46/297.16 c_46(U33^#(isNatKind(V2), V1, V2)) :46 1084.46/297.16 -->_1 active^#(U32(X1, X2, X3)) -> 1084.46/297.16 c_45(U32^#(active(X1), X2, X3)) :45 1084.46/297.16 -->_1 active^#(U31(tt(), V1, V2)) -> 1084.46/297.16 c_44(U32^#(isNatKind(V1), V1, V2)) :44 1084.46/297.16 -->_1 active^#(U31(X1, X2, X3)) -> 1084.46/297.16 c_43(U31^#(active(X1), X2, X3)) :43 1084.46/297.16 -->_1 active^#(U23(tt())) -> c_42() :42 1084.46/297.16 -->_1 active^#(U23(X)) -> c_41(U23^#(active(X))) :41 1084.46/297.16 -->_1 active^#(U22(tt(), V1)) -> c_40(U23^#(isNat(V1))) :40 1084.46/297.16 -->_1 active^#(U22(X1, X2)) -> c_39(U22^#(active(X1), X2)) :39 1084.46/297.16 -->_1 active^#(U21(tt(), V1)) -> c_38(U22^#(isNatKind(V1), V1)) :38 1084.46/297.16 -->_1 active^#(U21(X1, X2)) -> c_37(U21^#(active(X1), X2)) :37 1084.46/297.16 -->_1 active^#(U16(tt())) -> c_36() :36 1084.46/297.16 -->_1 active^#(U16(X)) -> c_35(U16^#(active(X))) :35 1084.46/297.16 -->_1 active^#(U15(tt(), V2)) -> c_34(U16^#(isNat(V2))) :34 1084.46/297.16 -->_1 active^#(U15(X1, X2)) -> c_33(U15^#(active(X1), X2)) :33 1084.46/297.16 -->_1 active^#(U14(tt(), V1, V2)) -> c_32(U15^#(isNat(V1), V2)) :32 1084.46/297.16 -->_1 active^#(U14(X1, X2, X3)) -> 1084.46/297.16 c_31(U14^#(active(X1), X2, X3)) :31 1084.46/297.16 -->_1 active^#(U13(tt(), V1, V2)) -> 1084.46/297.16 c_30(U14^#(isNatKind(V2), V1, V2)) :30 1084.46/297.16 -->_1 active^#(U13(X1, X2, X3)) -> 1084.46/297.16 c_29(U13^#(active(X1), X2, X3)) :29 1084.46/297.16 -->_1 active^#(U12(tt(), V1, V2)) -> 1084.46/297.16 c_28(U13^#(isNatKind(V2), V1, V2)) :28 1084.46/297.16 -->_1 active^#(U12(X1, X2, X3)) -> 1084.46/297.16 c_27(U12^#(active(X1), X2, X3)) :27 1084.46/297.16 -->_1 active^#(U11(tt(), V1, V2)) -> 1084.46/297.16 c_26(U12^#(isNatKind(V1), V1, V2)) :26 1084.46/297.16 -->_1 active^#(U11(X1, X2, X3)) -> 1084.46/297.16 c_25(U11^#(active(X1), X2, X3)) :25 1084.46/297.16 -->_1 active^#(x(N, 0())) -> c_24(U91^#(isNat(N), N)) :24 1084.46/297.16 -->_1 active^#(x(N, s(M))) -> c_23(U101^#(isNat(M), M, N)) :23 1084.46/297.16 -->_1 active^#(x(X1, X2)) -> c_22(x^#(active(X1), X2)) :22 1084.46/297.16 -->_1 active^#(x(X1, X2)) -> c_21(x^#(X1, active(X2))) :21 1084.46/297.16 -->_1 active^#(plus(N, 0())) -> c_20(U71^#(isNat(N), N)) :20 1084.46/297.16 -->_1 active^#(plus(N, s(M))) -> c_19(U81^#(isNat(M), M, N)) :19 1084.46/297.16 -->_1 active^#(plus(X1, X2)) -> c_18(plus^#(active(X1), X2)) :18 1084.46/297.16 -->_1 active^#(plus(X1, X2)) -> c_17(plus^#(X1, active(X2))) :17 1084.46/297.16 -->_1 active^#(U104(tt(), M, N)) -> c_16(plus^#(x(N, M), N)) :16 1084.46/297.16 -->_1 active^#(U104(X1, X2, X3)) -> 1084.46/297.16 c_15(U104^#(active(X1), X2, X3)) :15 1084.46/297.16 -->_1 active^#(isNat(0())) -> c_14() :14 1084.46/297.17 -->_1 active^#(isNat(s(V1))) -> c_13(U21^#(isNatKind(V1), V1)) :13 1084.46/297.17 -->_1 active^#(isNat(x(V1, V2))) -> 1084.46/297.17 c_12(U31^#(isNatKind(V1), V1, V2)) :12 1084.46/297.17 -->_1 active^#(isNat(plus(V1, V2))) -> 1084.46/297.17 c_11(U11^#(isNatKind(V1), V1, V2)) :11 1084.46/297.17 -->_1 active^#(U103(tt(), M, N)) -> 1084.46/297.17 c_10(U104^#(isNatKind(N), M, N)) :10 1084.46/297.17 -->_1 active^#(U103(X1, X2, X3)) -> 1084.46/297.17 c_9(U103^#(active(X1), X2, X3)) :9 1084.46/297.17 -->_1 active^#(isNatKind(0())) -> c_8() :8 1084.46/297.17 -->_1 active^#(isNatKind(s(V1))) -> c_7(U51^#(isNatKind(V1))) :7 1084.46/297.17 -->_1 active^#(isNatKind(x(V1, V2))) -> 1084.46/297.17 c_6(U61^#(isNatKind(V1), V2)) :6 1084.46/297.17 -->_1 active^#(isNatKind(plus(V1, V2))) -> 1084.46/297.17 c_5(U41^#(isNatKind(V1), V2)) :5 1084.46/297.17 -->_1 active^#(U102(tt(), M, N)) -> c_4(U103^#(isNat(N), M, N)) :4 1084.46/297.17 -->_1 active^#(U102(X1, X2, X3)) -> 1084.46/297.17 c_3(U102^#(active(X1), X2, X3)) :3 1084.46/297.17 -->_1 active^#(U101(tt(), M, N)) -> 1084.46/297.17 c_2(U102^#(isNatKind(M), M, N)) :2 1084.46/297.17 -->_1 active^#(U101(X1, X2, X3)) -> 1084.46/297.17 c_1(U101^#(active(X1), X2, X3)) :1 1084.46/297.17 1084.46/297.17 69: active^#(U81(X1, X2, X3)) -> c_69(U81^#(active(X1), X2, X3)) 1084.46/297.17 -->_1 U81^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.17 c_143(U81^#(X1, X2, X3)) :106 1084.46/297.17 -->_1 U81^#(mark(X1), X2, X3) -> c_142(U81^#(X1, X2, X3)) :105 1084.46/297.17 1084.46/297.17 70: active^#(U81(tt(), M, N)) -> c_70(U82^#(isNatKind(M), M, N)) 1084.46/297.17 -->_1 U82^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.17 c_145(U82^#(X1, X2, X3)) :145 1084.46/297.17 -->_1 U82^#(mark(X1), X2, X3) -> c_144(U82^#(X1, X2, X3)) :144 1084.46/297.17 1084.46/297.17 71: active^#(U82(X1, X2, X3)) -> c_71(U82^#(active(X1), X2, X3)) 1084.46/297.17 -->_1 U82^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.17 c_145(U82^#(X1, X2, X3)) :145 1084.46/297.17 -->_1 U82^#(mark(X1), X2, X3) -> c_144(U82^#(X1, X2, X3)) :144 1084.46/297.17 1084.46/297.17 72: active^#(U82(tt(), M, N)) -> c_72(U83^#(isNat(N), M, N)) 1084.46/297.17 -->_1 U83^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.17 c_147(U83^#(X1, X2, X3)) :147 1084.46/297.17 -->_1 U83^#(mark(X1), X2, X3) -> c_146(U83^#(X1, X2, X3)) :146 1084.46/297.17 1084.46/297.17 73: active^#(U83(X1, X2, X3)) -> c_73(U83^#(active(X1), X2, X3)) 1084.46/297.17 -->_1 U83^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.17 c_147(U83^#(X1, X2, X3)) :147 1084.46/297.17 -->_1 U83^#(mark(X1), X2, X3) -> c_146(U83^#(X1, X2, X3)) :146 1084.46/297.17 1084.46/297.17 74: active^#(U83(tt(), M, N)) -> c_74(U84^#(isNatKind(N), M, N)) 1084.46/297.17 -->_1 U84^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.17 c_149(U84^#(X1, X2, X3)) :149 1084.46/297.17 -->_1 U84^#(mark(X1), X2, X3) -> c_148(U84^#(X1, X2, X3)) :148 1084.46/297.17 1084.46/297.17 75: active^#(U84(X1, X2, X3)) -> c_75(U84^#(active(X1), X2, X3)) 1084.46/297.17 -->_1 U84^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.17 c_149(U84^#(X1, X2, X3)) :149 1084.46/297.17 -->_1 U84^#(mark(X1), X2, X3) -> c_148(U84^#(X1, X2, X3)) :148 1084.46/297.17 1084.46/297.17 76: active^#(U84(tt(), M, N)) -> c_76(s^#(plus(N, M))) 1084.46/297.17 -->_1 s^#(ok(X)) -> c_151(s^#(X)) :151 1084.46/297.17 -->_1 s^#(mark(X)) -> c_150(s^#(X)) :150 1084.46/297.17 1084.46/297.17 77: active^#(s(X)) -> c_77(s^#(active(X))) 1084.46/297.17 -->_1 s^#(ok(X)) -> c_151(s^#(X)) :151 1084.46/297.17 -->_1 s^#(mark(X)) -> c_150(s^#(X)) :150 1084.46/297.17 1084.46/297.17 78: active^#(U91(X1, X2)) -> c_78(U91^#(active(X1), X2)) 1084.46/297.17 -->_1 U91^#(ok(X1), ok(X2)) -> c_153(U91^#(X1, X2)) :113 1084.46/297.17 -->_1 U91^#(mark(X1), X2) -> c_152(U91^#(X1, X2)) :112 1084.46/297.17 1084.46/297.17 79: active^#(U91(tt(), N)) -> c_79(U92^#(isNatKind(N))) 1084.46/297.17 -->_1 U92^#(ok(X)) -> c_155(U92^#(X)) :153 1084.46/297.17 -->_1 U92^#(mark(X)) -> c_154(U92^#(X)) :152 1084.46/297.17 1084.46/297.17 80: active^#(U92(X)) -> c_80(U92^#(active(X))) 1084.46/297.17 -->_1 U92^#(ok(X)) -> c_155(U92^#(X)) :153 1084.46/297.17 -->_1 U92^#(mark(X)) -> c_154(U92^#(X)) :152 1084.46/297.17 1084.46/297.17 81: active^#(U92(tt())) -> c_81() 1084.46/297.17 1084.46/297.17 82: U101^#(mark(X1), X2, X3) -> c_82(U101^#(X1, X2, X3)) 1084.46/297.17 -->_1 U101^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.17 c_83(U101^#(X1, X2, X3)) :83 1084.46/297.17 -->_1 U101^#(mark(X1), X2, X3) -> c_82(U101^#(X1, X2, X3)) :82 1084.46/297.17 1084.46/297.17 83: U101^#(ok(X1), ok(X2), ok(X3)) -> c_83(U101^#(X1, X2, X3)) 1084.46/297.17 -->_1 U101^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.17 c_83(U101^#(X1, X2, X3)) :83 1084.46/297.17 -->_1 U101^#(mark(X1), X2, X3) -> c_82(U101^#(X1, X2, X3)) :82 1084.46/297.17 1084.46/297.17 84: U102^#(mark(X1), X2, X3) -> c_84(U102^#(X1, X2, X3)) 1084.46/297.17 -->_1 U102^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.17 c_85(U102^#(X1, X2, X3)) :85 1084.46/297.17 -->_1 U102^#(mark(X1), X2, X3) -> c_84(U102^#(X1, X2, X3)) :84 1084.46/297.17 1084.46/297.17 85: U102^#(ok(X1), ok(X2), ok(X3)) -> c_85(U102^#(X1, X2, X3)) 1084.46/297.17 -->_1 U102^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.17 c_85(U102^#(X1, X2, X3)) :85 1084.46/297.17 -->_1 U102^#(mark(X1), X2, X3) -> c_84(U102^#(X1, X2, X3)) :84 1084.46/297.17 1084.46/297.17 86: U103^#(mark(X1), X2, X3) -> c_87(U103^#(X1, X2, X3)) 1084.46/297.17 -->_1 U103^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.17 c_88(U103^#(X1, X2, X3)) :87 1084.46/297.17 -->_1 U103^#(mark(X1), X2, X3) -> c_87(U103^#(X1, X2, X3)) :86 1084.46/297.17 1084.46/297.17 87: U103^#(ok(X1), ok(X2), ok(X3)) -> c_88(U103^#(X1, X2, X3)) 1084.46/297.17 -->_1 U103^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.17 c_88(U103^#(X1, X2, X3)) :87 1084.46/297.17 -->_1 U103^#(mark(X1), X2, X3) -> c_87(U103^#(X1, X2, X3)) :86 1084.46/297.17 1084.46/297.17 88: U41^#(mark(X1), X2) -> c_128(U41^#(X1, X2)) 1084.46/297.17 -->_1 U41^#(ok(X1), ok(X2)) -> c_129(U41^#(X1, X2)) :89 1084.46/297.17 -->_1 U41^#(mark(X1), X2) -> c_128(U41^#(X1, X2)) :88 1084.46/297.17 1084.46/297.17 89: U41^#(ok(X1), ok(X2)) -> c_129(U41^#(X1, X2)) 1084.46/297.17 -->_1 U41^#(ok(X1), ok(X2)) -> c_129(U41^#(X1, X2)) :89 1084.46/297.17 -->_1 U41^#(mark(X1), X2) -> c_128(U41^#(X1, X2)) :88 1084.46/297.17 1084.46/297.17 90: U61^#(mark(X1), X2) -> c_134(U61^#(X1, X2)) 1084.46/297.17 -->_1 U61^#(ok(X1), ok(X2)) -> c_135(U61^#(X1, X2)) :91 1084.46/297.17 -->_1 U61^#(mark(X1), X2) -> c_134(U61^#(X1, X2)) :90 1084.46/297.17 1084.46/297.17 91: U61^#(ok(X1), ok(X2)) -> c_135(U61^#(X1, X2)) 1084.46/297.17 -->_1 U61^#(ok(X1), ok(X2)) -> c_135(U61^#(X1, X2)) :91 1084.46/297.17 -->_1 U61^#(mark(X1), X2) -> c_134(U61^#(X1, X2)) :90 1084.46/297.17 1084.46/297.17 92: U51^#(mark(X)) -> c_132(U51^#(X)) 1084.46/297.17 -->_1 U51^#(ok(X)) -> c_133(U51^#(X)) :93 1084.46/297.17 -->_1 U51^#(mark(X)) -> c_132(U51^#(X)) :92 1084.46/297.17 1084.46/297.17 93: U51^#(ok(X)) -> c_133(U51^#(X)) 1084.46/297.17 -->_1 U51^#(ok(X)) -> c_133(U51^#(X)) :93 1084.46/297.17 -->_1 U51^#(mark(X)) -> c_132(U51^#(X)) :92 1084.46/297.17 1084.46/297.17 94: U104^#(mark(X1), X2, X3) -> c_90(U104^#(X1, X2, X3)) 1084.46/297.17 -->_1 U104^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.17 c_91(U104^#(X1, X2, X3)) :95 1084.46/297.17 -->_1 U104^#(mark(X1), X2, X3) -> c_90(U104^#(X1, X2, X3)) :94 1084.46/297.17 1084.46/297.17 95: U104^#(ok(X1), ok(X2), ok(X3)) -> c_91(U104^#(X1, X2, X3)) 1084.46/297.17 -->_1 U104^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.17 c_91(U104^#(X1, X2, X3)) :95 1084.46/297.17 -->_1 U104^#(mark(X1), X2, X3) -> c_90(U104^#(X1, X2, X3)) :94 1084.46/297.17 1084.46/297.17 96: U11^#(mark(X1), X2, X3) -> c_98(U11^#(X1, X2, X3)) 1084.46/297.17 -->_1 U11^#(ok(X1), ok(X2), ok(X3)) -> c_99(U11^#(X1, X2, X3)) :97 1084.46/297.17 -->_1 U11^#(mark(X1), X2, X3) -> c_98(U11^#(X1, X2, X3)) :96 1084.46/297.17 1084.46/297.17 97: U11^#(ok(X1), ok(X2), ok(X3)) -> c_99(U11^#(X1, X2, X3)) 1084.46/297.17 -->_1 U11^#(ok(X1), ok(X2), ok(X3)) -> c_99(U11^#(X1, X2, X3)) :97 1084.46/297.17 -->_1 U11^#(mark(X1), X2, X3) -> c_98(U11^#(X1, X2, X3)) :96 1084.46/297.17 1084.46/297.17 98: U31^#(mark(X1), X2, X3) -> c_116(U31^#(X1, X2, X3)) 1084.46/297.17 -->_1 U31^#(ok(X1), ok(X2), ok(X3)) -> c_117(U31^#(X1, X2, X3)) :99 1084.46/297.17 -->_1 U31^#(mark(X1), X2, X3) -> c_116(U31^#(X1, X2, X3)) :98 1084.46/297.17 1084.46/297.17 99: U31^#(ok(X1), ok(X2), ok(X3)) -> c_117(U31^#(X1, X2, X3)) 1084.46/297.17 -->_1 U31^#(ok(X1), ok(X2), ok(X3)) -> c_117(U31^#(X1, X2, X3)) :99 1084.46/297.17 -->_1 U31^#(mark(X1), X2, X3) -> c_116(U31^#(X1, X2, X3)) :98 1084.46/297.17 1084.46/297.17 100: U21^#(mark(X1), X2) -> c_110(U21^#(X1, X2)) 1084.46/297.17 -->_1 U21^#(ok(X1), ok(X2)) -> c_111(U21^#(X1, X2)) :101 1084.46/297.17 -->_1 U21^#(mark(X1), X2) -> c_110(U21^#(X1, X2)) :100 1084.46/297.17 1084.46/297.17 101: U21^#(ok(X1), ok(X2)) -> c_111(U21^#(X1, X2)) 1084.46/297.17 -->_1 U21^#(ok(X1), ok(X2)) -> c_111(U21^#(X1, X2)) :101 1084.46/297.17 -->_1 U21^#(mark(X1), X2) -> c_110(U21^#(X1, X2)) :100 1084.46/297.17 1084.46/297.17 102: plus^#(X1, mark(X2)) -> c_92(plus^#(X1, X2)) 1084.46/297.17 -->_1 plus^#(ok(X1), ok(X2)) -> c_94(plus^#(X1, X2)) :104 1084.46/297.17 -->_1 plus^#(mark(X1), X2) -> c_93(plus^#(X1, X2)) :103 1084.46/297.17 -->_1 plus^#(X1, mark(X2)) -> c_92(plus^#(X1, X2)) :102 1084.46/297.17 1084.46/297.17 103: plus^#(mark(X1), X2) -> c_93(plus^#(X1, X2)) 1084.46/297.17 -->_1 plus^#(ok(X1), ok(X2)) -> c_94(plus^#(X1, X2)) :104 1084.46/297.17 -->_1 plus^#(mark(X1), X2) -> c_93(plus^#(X1, X2)) :103 1084.46/297.17 -->_1 plus^#(X1, mark(X2)) -> c_92(plus^#(X1, X2)) :102 1084.46/297.17 1084.46/297.17 104: plus^#(ok(X1), ok(X2)) -> c_94(plus^#(X1, X2)) 1084.46/297.17 -->_1 plus^#(ok(X1), ok(X2)) -> c_94(plus^#(X1, X2)) :104 1084.46/297.17 -->_1 plus^#(mark(X1), X2) -> c_93(plus^#(X1, X2)) :103 1084.46/297.17 -->_1 plus^#(X1, mark(X2)) -> c_92(plus^#(X1, X2)) :102 1084.46/297.17 1084.46/297.17 105: U81^#(mark(X1), X2, X3) -> c_142(U81^#(X1, X2, X3)) 1084.46/297.17 -->_1 U81^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.17 c_143(U81^#(X1, X2, X3)) :106 1084.46/297.17 -->_1 U81^#(mark(X1), X2, X3) -> c_142(U81^#(X1, X2, X3)) :105 1084.46/297.17 1084.46/297.17 106: U81^#(ok(X1), ok(X2), ok(X3)) -> c_143(U81^#(X1, X2, X3)) 1084.46/297.17 -->_1 U81^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.17 c_143(U81^#(X1, X2, X3)) :106 1084.46/297.17 -->_1 U81^#(mark(X1), X2, X3) -> c_142(U81^#(X1, X2, X3)) :105 1084.46/297.17 1084.46/297.17 107: U71^#(mark(X1), X2) -> c_138(U71^#(X1, X2)) 1084.46/297.17 -->_1 U71^#(ok(X1), ok(X2)) -> c_139(U71^#(X1, X2)) :108 1084.46/297.17 -->_1 U71^#(mark(X1), X2) -> c_138(U71^#(X1, X2)) :107 1084.46/297.17 1084.46/297.17 108: U71^#(ok(X1), ok(X2)) -> c_139(U71^#(X1, X2)) 1084.46/297.17 -->_1 U71^#(ok(X1), ok(X2)) -> c_139(U71^#(X1, X2)) :108 1084.46/297.17 -->_1 U71^#(mark(X1), X2) -> c_138(U71^#(X1, X2)) :107 1084.46/297.17 1084.46/297.17 109: x^#(X1, mark(X2)) -> c_95(x^#(X1, X2)) 1084.46/297.17 -->_1 x^#(ok(X1), ok(X2)) -> c_97(x^#(X1, X2)) :111 1084.46/297.17 -->_1 x^#(mark(X1), X2) -> c_96(x^#(X1, X2)) :110 1084.46/297.17 -->_1 x^#(X1, mark(X2)) -> c_95(x^#(X1, X2)) :109 1084.46/297.17 1084.46/297.17 110: x^#(mark(X1), X2) -> c_96(x^#(X1, X2)) 1084.46/297.17 -->_1 x^#(ok(X1), ok(X2)) -> c_97(x^#(X1, X2)) :111 1084.46/297.17 -->_1 x^#(mark(X1), X2) -> c_96(x^#(X1, X2)) :110 1084.46/297.17 -->_1 x^#(X1, mark(X2)) -> c_95(x^#(X1, X2)) :109 1084.46/297.17 1084.46/297.17 111: x^#(ok(X1), ok(X2)) -> c_97(x^#(X1, X2)) 1084.46/297.17 -->_1 x^#(ok(X1), ok(X2)) -> c_97(x^#(X1, X2)) :111 1084.46/297.17 -->_1 x^#(mark(X1), X2) -> c_96(x^#(X1, X2)) :110 1084.46/297.17 -->_1 x^#(X1, mark(X2)) -> c_95(x^#(X1, X2)) :109 1084.46/297.17 1084.46/297.17 112: U91^#(mark(X1), X2) -> c_152(U91^#(X1, X2)) 1084.46/297.17 -->_1 U91^#(ok(X1), ok(X2)) -> c_153(U91^#(X1, X2)) :113 1084.46/297.17 -->_1 U91^#(mark(X1), X2) -> c_152(U91^#(X1, X2)) :112 1084.46/297.17 1084.46/297.17 113: U91^#(ok(X1), ok(X2)) -> c_153(U91^#(X1, X2)) 1084.46/297.17 -->_1 U91^#(ok(X1), ok(X2)) -> c_153(U91^#(X1, X2)) :113 1084.46/297.17 -->_1 U91^#(mark(X1), X2) -> c_152(U91^#(X1, X2)) :112 1084.46/297.17 1084.46/297.17 114: U12^#(mark(X1), X2, X3) -> c_100(U12^#(X1, X2, X3)) 1084.46/297.17 -->_1 U12^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.17 c_101(U12^#(X1, X2, X3)) :115 1084.46/297.17 -->_1 U12^#(mark(X1), X2, X3) -> c_100(U12^#(X1, X2, X3)) :114 1084.46/297.17 1084.46/297.17 115: U12^#(ok(X1), ok(X2), ok(X3)) -> c_101(U12^#(X1, X2, X3)) 1084.46/297.17 -->_1 U12^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.17 c_101(U12^#(X1, X2, X3)) :115 1084.46/297.17 -->_1 U12^#(mark(X1), X2, X3) -> c_100(U12^#(X1, X2, X3)) :114 1084.46/297.17 1084.46/297.17 116: U13^#(mark(X1), X2, X3) -> c_102(U13^#(X1, X2, X3)) 1084.46/297.17 -->_1 U13^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.17 c_103(U13^#(X1, X2, X3)) :117 1084.46/297.17 -->_1 U13^#(mark(X1), X2, X3) -> c_102(U13^#(X1, X2, X3)) :116 1084.46/297.17 1084.46/297.17 117: U13^#(ok(X1), ok(X2), ok(X3)) -> c_103(U13^#(X1, X2, X3)) 1084.46/297.17 -->_1 U13^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.17 c_103(U13^#(X1, X2, X3)) :117 1084.46/297.17 -->_1 U13^#(mark(X1), X2, X3) -> c_102(U13^#(X1, X2, X3)) :116 1084.46/297.17 1084.46/297.17 118: U14^#(mark(X1), X2, X3) -> c_104(U14^#(X1, X2, X3)) 1084.46/297.17 -->_1 U14^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.17 c_105(U14^#(X1, X2, X3)) :119 1084.46/297.17 -->_1 U14^#(mark(X1), X2, X3) -> c_104(U14^#(X1, X2, X3)) :118 1084.46/297.17 1084.46/297.17 119: U14^#(ok(X1), ok(X2), ok(X3)) -> c_105(U14^#(X1, X2, X3)) 1084.46/297.17 -->_1 U14^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.17 c_105(U14^#(X1, X2, X3)) :119 1084.46/297.17 -->_1 U14^#(mark(X1), X2, X3) -> c_104(U14^#(X1, X2, X3)) :118 1084.46/297.17 1084.46/297.17 120: U15^#(mark(X1), X2) -> c_106(U15^#(X1, X2)) 1084.46/297.17 -->_1 U15^#(ok(X1), ok(X2)) -> c_107(U15^#(X1, X2)) :121 1084.46/297.17 -->_1 U15^#(mark(X1), X2) -> c_106(U15^#(X1, X2)) :120 1084.46/297.17 1084.46/297.17 121: U15^#(ok(X1), ok(X2)) -> c_107(U15^#(X1, X2)) 1084.46/297.17 -->_1 U15^#(ok(X1), ok(X2)) -> c_107(U15^#(X1, X2)) :121 1084.46/297.17 -->_1 U15^#(mark(X1), X2) -> c_106(U15^#(X1, X2)) :120 1084.46/297.17 1084.46/297.17 122: U16^#(mark(X)) -> c_108(U16^#(X)) 1084.46/297.17 -->_1 U16^#(ok(X)) -> c_109(U16^#(X)) :123 1084.46/297.17 -->_1 U16^#(mark(X)) -> c_108(U16^#(X)) :122 1084.46/297.17 1084.46/297.17 123: U16^#(ok(X)) -> c_109(U16^#(X)) 1084.46/297.17 -->_1 U16^#(ok(X)) -> c_109(U16^#(X)) :123 1084.46/297.17 -->_1 U16^#(mark(X)) -> c_108(U16^#(X)) :122 1084.46/297.17 1084.46/297.17 124: U22^#(mark(X1), X2) -> c_112(U22^#(X1, X2)) 1084.46/297.17 -->_1 U22^#(ok(X1), ok(X2)) -> c_113(U22^#(X1, X2)) :125 1084.46/297.17 -->_1 U22^#(mark(X1), X2) -> c_112(U22^#(X1, X2)) :124 1084.46/297.17 1084.46/297.17 125: U22^#(ok(X1), ok(X2)) -> c_113(U22^#(X1, X2)) 1084.46/297.17 -->_1 U22^#(ok(X1), ok(X2)) -> c_113(U22^#(X1, X2)) :125 1084.46/297.17 -->_1 U22^#(mark(X1), X2) -> c_112(U22^#(X1, X2)) :124 1084.46/297.17 1084.46/297.17 126: U23^#(mark(X)) -> c_114(U23^#(X)) 1084.46/297.17 -->_1 U23^#(ok(X)) -> c_115(U23^#(X)) :127 1084.46/297.17 -->_1 U23^#(mark(X)) -> c_114(U23^#(X)) :126 1084.46/297.17 1084.46/297.17 127: U23^#(ok(X)) -> c_115(U23^#(X)) 1084.46/297.17 -->_1 U23^#(ok(X)) -> c_115(U23^#(X)) :127 1084.46/297.17 -->_1 U23^#(mark(X)) -> c_114(U23^#(X)) :126 1084.46/297.17 1084.46/297.17 128: U32^#(mark(X1), X2, X3) -> c_118(U32^#(X1, X2, X3)) 1084.46/297.17 -->_1 U32^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.17 c_119(U32^#(X1, X2, X3)) :129 1084.46/297.17 -->_1 U32^#(mark(X1), X2, X3) -> c_118(U32^#(X1, X2, X3)) :128 1084.46/297.17 1084.46/297.17 129: U32^#(ok(X1), ok(X2), ok(X3)) -> c_119(U32^#(X1, X2, X3)) 1084.46/297.17 -->_1 U32^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.17 c_119(U32^#(X1, X2, X3)) :129 1084.46/297.17 -->_1 U32^#(mark(X1), X2, X3) -> c_118(U32^#(X1, X2, X3)) :128 1084.46/297.17 1084.46/297.17 130: U33^#(mark(X1), X2, X3) -> c_120(U33^#(X1, X2, X3)) 1084.46/297.17 -->_1 U33^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.17 c_121(U33^#(X1, X2, X3)) :131 1084.46/297.17 -->_1 U33^#(mark(X1), X2, X3) -> c_120(U33^#(X1, X2, X3)) :130 1084.46/297.17 1084.46/297.17 131: U33^#(ok(X1), ok(X2), ok(X3)) -> c_121(U33^#(X1, X2, X3)) 1084.46/297.17 -->_1 U33^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.17 c_121(U33^#(X1, X2, X3)) :131 1084.46/297.17 -->_1 U33^#(mark(X1), X2, X3) -> c_120(U33^#(X1, X2, X3)) :130 1084.46/297.17 1084.46/297.17 132: U34^#(mark(X1), X2, X3) -> c_122(U34^#(X1, X2, X3)) 1084.46/297.17 -->_1 U34^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.17 c_123(U34^#(X1, X2, X3)) :133 1084.46/297.17 -->_1 U34^#(mark(X1), X2, X3) -> c_122(U34^#(X1, X2, X3)) :132 1084.46/297.17 1084.46/297.17 133: U34^#(ok(X1), ok(X2), ok(X3)) -> c_123(U34^#(X1, X2, X3)) 1084.46/297.17 -->_1 U34^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.17 c_123(U34^#(X1, X2, X3)) :133 1084.46/297.17 -->_1 U34^#(mark(X1), X2, X3) -> c_122(U34^#(X1, X2, X3)) :132 1084.46/297.17 1084.46/297.17 134: U35^#(mark(X1), X2) -> c_124(U35^#(X1, X2)) 1084.46/297.17 -->_1 U35^#(ok(X1), ok(X2)) -> c_125(U35^#(X1, X2)) :135 1084.46/297.17 -->_1 U35^#(mark(X1), X2) -> c_124(U35^#(X1, X2)) :134 1084.46/297.17 1084.46/297.17 135: U35^#(ok(X1), ok(X2)) -> c_125(U35^#(X1, X2)) 1084.46/297.17 -->_1 U35^#(ok(X1), ok(X2)) -> c_125(U35^#(X1, X2)) :135 1084.46/297.17 -->_1 U35^#(mark(X1), X2) -> c_124(U35^#(X1, X2)) :134 1084.46/297.17 1084.46/297.17 136: U36^#(mark(X)) -> c_126(U36^#(X)) 1084.46/297.17 -->_1 U36^#(ok(X)) -> c_127(U36^#(X)) :137 1084.46/297.17 -->_1 U36^#(mark(X)) -> c_126(U36^#(X)) :136 1084.46/297.17 1084.46/297.17 137: U36^#(ok(X)) -> c_127(U36^#(X)) 1084.46/297.17 -->_1 U36^#(ok(X)) -> c_127(U36^#(X)) :137 1084.46/297.17 -->_1 U36^#(mark(X)) -> c_126(U36^#(X)) :136 1084.46/297.17 1084.46/297.17 138: U42^#(mark(X)) -> c_130(U42^#(X)) 1084.46/297.17 -->_1 U42^#(ok(X)) -> c_131(U42^#(X)) :139 1084.46/297.17 -->_1 U42^#(mark(X)) -> c_130(U42^#(X)) :138 1084.46/297.17 1084.46/297.17 139: U42^#(ok(X)) -> c_131(U42^#(X)) 1084.46/297.17 -->_1 U42^#(ok(X)) -> c_131(U42^#(X)) :139 1084.46/297.17 -->_1 U42^#(mark(X)) -> c_130(U42^#(X)) :138 1084.46/297.17 1084.46/297.17 140: U62^#(mark(X)) -> c_136(U62^#(X)) 1084.46/297.17 -->_1 U62^#(ok(X)) -> c_137(U62^#(X)) :141 1084.46/297.17 -->_1 U62^#(mark(X)) -> c_136(U62^#(X)) :140 1084.46/297.17 1084.46/297.17 141: U62^#(ok(X)) -> c_137(U62^#(X)) 1084.46/297.17 -->_1 U62^#(ok(X)) -> c_137(U62^#(X)) :141 1084.46/297.17 -->_1 U62^#(mark(X)) -> c_136(U62^#(X)) :140 1084.46/297.17 1084.46/297.17 142: U72^#(mark(X1), X2) -> c_140(U72^#(X1, X2)) 1084.46/297.17 -->_1 U72^#(ok(X1), ok(X2)) -> c_141(U72^#(X1, X2)) :143 1084.46/297.17 -->_1 U72^#(mark(X1), X2) -> c_140(U72^#(X1, X2)) :142 1084.46/297.18 1084.46/297.18 143: U72^#(ok(X1), ok(X2)) -> c_141(U72^#(X1, X2)) 1084.46/297.18 -->_1 U72^#(ok(X1), ok(X2)) -> c_141(U72^#(X1, X2)) :143 1084.46/297.18 -->_1 U72^#(mark(X1), X2) -> c_140(U72^#(X1, X2)) :142 1084.46/297.18 1084.46/297.18 144: U82^#(mark(X1), X2, X3) -> c_144(U82^#(X1, X2, X3)) 1084.46/297.18 -->_1 U82^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.18 c_145(U82^#(X1, X2, X3)) :145 1084.46/297.18 -->_1 U82^#(mark(X1), X2, X3) -> c_144(U82^#(X1, X2, X3)) :144 1084.46/297.18 1084.46/297.18 145: U82^#(ok(X1), ok(X2), ok(X3)) -> c_145(U82^#(X1, X2, X3)) 1084.46/297.18 -->_1 U82^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.18 c_145(U82^#(X1, X2, X3)) :145 1084.46/297.18 -->_1 U82^#(mark(X1), X2, X3) -> c_144(U82^#(X1, X2, X3)) :144 1084.46/297.18 1084.46/297.18 146: U83^#(mark(X1), X2, X3) -> c_146(U83^#(X1, X2, X3)) 1084.46/297.18 -->_1 U83^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.18 c_147(U83^#(X1, X2, X3)) :147 1084.46/297.18 -->_1 U83^#(mark(X1), X2, X3) -> c_146(U83^#(X1, X2, X3)) :146 1084.46/297.18 1084.46/297.18 147: U83^#(ok(X1), ok(X2), ok(X3)) -> c_147(U83^#(X1, X2, X3)) 1084.46/297.18 -->_1 U83^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.18 c_147(U83^#(X1, X2, X3)) :147 1084.46/297.18 -->_1 U83^#(mark(X1), X2, X3) -> c_146(U83^#(X1, X2, X3)) :146 1084.46/297.18 1084.46/297.18 148: U84^#(mark(X1), X2, X3) -> c_148(U84^#(X1, X2, X3)) 1084.46/297.18 -->_1 U84^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.18 c_149(U84^#(X1, X2, X3)) :149 1084.46/297.18 -->_1 U84^#(mark(X1), X2, X3) -> c_148(U84^#(X1, X2, X3)) :148 1084.46/297.18 1084.46/297.18 149: U84^#(ok(X1), ok(X2), ok(X3)) -> c_149(U84^#(X1, X2, X3)) 1084.46/297.18 -->_1 U84^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.18 c_149(U84^#(X1, X2, X3)) :149 1084.46/297.18 -->_1 U84^#(mark(X1), X2, X3) -> c_148(U84^#(X1, X2, X3)) :148 1084.46/297.18 1084.46/297.18 150: s^#(mark(X)) -> c_150(s^#(X)) 1084.46/297.18 -->_1 s^#(ok(X)) -> c_151(s^#(X)) :151 1084.46/297.18 -->_1 s^#(mark(X)) -> c_150(s^#(X)) :150 1084.46/297.18 1084.46/297.18 151: s^#(ok(X)) -> c_151(s^#(X)) 1084.46/297.18 -->_1 s^#(ok(X)) -> c_151(s^#(X)) :151 1084.46/297.18 -->_1 s^#(mark(X)) -> c_150(s^#(X)) :150 1084.46/297.18 1084.46/297.18 152: U92^#(mark(X)) -> c_154(U92^#(X)) 1084.46/297.18 -->_1 U92^#(ok(X)) -> c_155(U92^#(X)) :153 1084.46/297.18 -->_1 U92^#(mark(X)) -> c_154(U92^#(X)) :152 1084.46/297.18 1084.46/297.18 153: U92^#(ok(X)) -> c_155(U92^#(X)) 1084.46/297.18 -->_1 U92^#(ok(X)) -> c_155(U92^#(X)) :153 1084.46/297.18 -->_1 U92^#(mark(X)) -> c_154(U92^#(X)) :152 1084.46/297.18 1084.46/297.18 154: isNatKind^#(ok(X)) -> c_86(isNatKind^#(X)) 1084.46/297.18 -->_1 isNatKind^#(ok(X)) -> c_86(isNatKind^#(X)) :154 1084.46/297.18 1084.46/297.18 155: isNat^#(ok(X)) -> c_89(isNat^#(X)) 1084.46/297.18 -->_1 isNat^#(ok(X)) -> c_89(isNat^#(X)) :155 1084.46/297.18 1084.46/297.18 156: proper^#(U101(X1, X2, X3)) -> 1084.46/297.18 c_156(U101^#(proper(X1), proper(X2), proper(X3))) 1084.46/297.18 -->_1 U101^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.18 c_83(U101^#(X1, X2, X3)) :83 1084.46/297.18 -->_1 U101^#(mark(X1), X2, X3) -> c_82(U101^#(X1, X2, X3)) :82 1084.46/297.18 1084.46/297.18 157: proper^#(tt()) -> c_157() 1084.46/297.18 1084.46/297.18 158: proper^#(U102(X1, X2, X3)) -> 1084.46/297.18 c_158(U102^#(proper(X1), proper(X2), proper(X3))) 1084.46/297.18 -->_1 U102^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.18 c_85(U102^#(X1, X2, X3)) :85 1084.46/297.18 -->_1 U102^#(mark(X1), X2, X3) -> c_84(U102^#(X1, X2, X3)) :84 1084.46/297.18 1084.46/297.18 159: proper^#(isNatKind(X)) -> c_159(isNatKind^#(proper(X))) 1084.46/297.18 -->_1 isNatKind^#(ok(X)) -> c_86(isNatKind^#(X)) :154 1084.46/297.18 1084.46/297.18 160: proper^#(U103(X1, X2, X3)) -> 1084.46/297.18 c_160(U103^#(proper(X1), proper(X2), proper(X3))) 1084.46/297.18 -->_1 U103^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.18 c_88(U103^#(X1, X2, X3)) :87 1084.46/297.18 -->_1 U103^#(mark(X1), X2, X3) -> c_87(U103^#(X1, X2, X3)) :86 1084.46/297.18 1084.46/297.18 161: proper^#(isNat(X)) -> c_161(isNat^#(proper(X))) 1084.46/297.18 -->_1 isNat^#(ok(X)) -> c_89(isNat^#(X)) :155 1084.46/297.18 1084.46/297.18 162: proper^#(U104(X1, X2, X3)) -> 1084.46/297.18 c_162(U104^#(proper(X1), proper(X2), proper(X3))) 1084.46/297.18 -->_1 U104^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.18 c_91(U104^#(X1, X2, X3)) :95 1084.46/297.18 -->_1 U104^#(mark(X1), X2, X3) -> c_90(U104^#(X1, X2, X3)) :94 1084.46/297.18 1084.46/297.18 163: proper^#(plus(X1, X2)) -> 1084.46/297.18 c_163(plus^#(proper(X1), proper(X2))) 1084.46/297.18 -->_1 plus^#(ok(X1), ok(X2)) -> c_94(plus^#(X1, X2)) :104 1084.46/297.18 -->_1 plus^#(mark(X1), X2) -> c_93(plus^#(X1, X2)) :103 1084.46/297.18 -->_1 plus^#(X1, mark(X2)) -> c_92(plus^#(X1, X2)) :102 1084.46/297.18 1084.46/297.18 164: proper^#(x(X1, X2)) -> c_164(x^#(proper(X1), proper(X2))) 1084.46/297.18 -->_1 x^#(ok(X1), ok(X2)) -> c_97(x^#(X1, X2)) :111 1084.46/297.18 -->_1 x^#(mark(X1), X2) -> c_96(x^#(X1, X2)) :110 1084.46/297.18 -->_1 x^#(X1, mark(X2)) -> c_95(x^#(X1, X2)) :109 1084.46/297.18 1084.46/297.18 165: proper^#(U11(X1, X2, X3)) -> 1084.46/297.18 c_165(U11^#(proper(X1), proper(X2), proper(X3))) 1084.46/297.18 -->_1 U11^#(ok(X1), ok(X2), ok(X3)) -> c_99(U11^#(X1, X2, X3)) :97 1084.46/297.18 -->_1 U11^#(mark(X1), X2, X3) -> c_98(U11^#(X1, X2, X3)) :96 1084.46/297.18 1084.46/297.18 166: proper^#(U12(X1, X2, X3)) -> 1084.46/297.18 c_166(U12^#(proper(X1), proper(X2), proper(X3))) 1084.46/297.18 -->_1 U12^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.18 c_101(U12^#(X1, X2, X3)) :115 1084.46/297.18 -->_1 U12^#(mark(X1), X2, X3) -> c_100(U12^#(X1, X2, X3)) :114 1084.46/297.18 1084.46/297.18 167: proper^#(U13(X1, X2, X3)) -> 1084.46/297.18 c_167(U13^#(proper(X1), proper(X2), proper(X3))) 1084.46/297.18 -->_1 U13^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.18 c_103(U13^#(X1, X2, X3)) :117 1084.46/297.18 -->_1 U13^#(mark(X1), X2, X3) -> c_102(U13^#(X1, X2, X3)) :116 1084.46/297.18 1084.46/297.18 168: proper^#(U14(X1, X2, X3)) -> 1084.46/297.18 c_168(U14^#(proper(X1), proper(X2), proper(X3))) 1084.46/297.18 -->_1 U14^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.18 c_105(U14^#(X1, X2, X3)) :119 1084.46/297.18 -->_1 U14^#(mark(X1), X2, X3) -> c_104(U14^#(X1, X2, X3)) :118 1084.46/297.18 1084.46/297.18 169: proper^#(U15(X1, X2)) -> c_169(U15^#(proper(X1), proper(X2))) 1084.46/297.18 -->_1 U15^#(ok(X1), ok(X2)) -> c_107(U15^#(X1, X2)) :121 1084.46/297.18 -->_1 U15^#(mark(X1), X2) -> c_106(U15^#(X1, X2)) :120 1084.46/297.18 1084.46/297.18 170: proper^#(U16(X)) -> c_170(U16^#(proper(X))) 1084.46/297.18 -->_1 U16^#(ok(X)) -> c_109(U16^#(X)) :123 1084.46/297.18 -->_1 U16^#(mark(X)) -> c_108(U16^#(X)) :122 1084.46/297.18 1084.46/297.18 171: proper^#(U21(X1, X2)) -> c_171(U21^#(proper(X1), proper(X2))) 1084.46/297.18 -->_1 U21^#(ok(X1), ok(X2)) -> c_111(U21^#(X1, X2)) :101 1084.46/297.18 -->_1 U21^#(mark(X1), X2) -> c_110(U21^#(X1, X2)) :100 1084.46/297.18 1084.46/297.18 172: proper^#(U22(X1, X2)) -> c_172(U22^#(proper(X1), proper(X2))) 1084.46/297.18 -->_1 U22^#(ok(X1), ok(X2)) -> c_113(U22^#(X1, X2)) :125 1084.46/297.18 -->_1 U22^#(mark(X1), X2) -> c_112(U22^#(X1, X2)) :124 1084.46/297.18 1084.46/297.18 173: proper^#(U23(X)) -> c_173(U23^#(proper(X))) 1084.46/297.18 -->_1 U23^#(ok(X)) -> c_115(U23^#(X)) :127 1084.46/297.18 -->_1 U23^#(mark(X)) -> c_114(U23^#(X)) :126 1084.46/297.18 1084.46/297.18 174: proper^#(U31(X1, X2, X3)) -> 1084.46/297.18 c_174(U31^#(proper(X1), proper(X2), proper(X3))) 1084.46/297.18 -->_1 U31^#(ok(X1), ok(X2), ok(X3)) -> c_117(U31^#(X1, X2, X3)) :99 1084.46/297.18 -->_1 U31^#(mark(X1), X2, X3) -> c_116(U31^#(X1, X2, X3)) :98 1084.46/297.18 1084.46/297.18 175: proper^#(U32(X1, X2, X3)) -> 1084.46/297.18 c_175(U32^#(proper(X1), proper(X2), proper(X3))) 1084.46/297.18 -->_1 U32^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.18 c_119(U32^#(X1, X2, X3)) :129 1084.46/297.18 -->_1 U32^#(mark(X1), X2, X3) -> c_118(U32^#(X1, X2, X3)) :128 1084.46/297.18 1084.46/297.18 176: proper^#(U33(X1, X2, X3)) -> 1084.46/297.18 c_176(U33^#(proper(X1), proper(X2), proper(X3))) 1084.46/297.18 -->_1 U33^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.18 c_121(U33^#(X1, X2, X3)) :131 1084.46/297.18 -->_1 U33^#(mark(X1), X2, X3) -> c_120(U33^#(X1, X2, X3)) :130 1084.46/297.18 1084.46/297.18 177: proper^#(U34(X1, X2, X3)) -> 1084.46/297.18 c_177(U34^#(proper(X1), proper(X2), proper(X3))) 1084.46/297.18 -->_1 U34^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.18 c_123(U34^#(X1, X2, X3)) :133 1084.46/297.18 -->_1 U34^#(mark(X1), X2, X3) -> c_122(U34^#(X1, X2, X3)) :132 1084.46/297.18 1084.46/297.18 178: proper^#(U35(X1, X2)) -> c_178(U35^#(proper(X1), proper(X2))) 1084.46/297.18 -->_1 U35^#(ok(X1), ok(X2)) -> c_125(U35^#(X1, X2)) :135 1084.46/297.18 -->_1 U35^#(mark(X1), X2) -> c_124(U35^#(X1, X2)) :134 1084.46/297.18 1084.46/297.18 179: proper^#(U36(X)) -> c_179(U36^#(proper(X))) 1084.46/297.18 -->_1 U36^#(ok(X)) -> c_127(U36^#(X)) :137 1084.46/297.18 -->_1 U36^#(mark(X)) -> c_126(U36^#(X)) :136 1084.46/297.18 1084.46/297.18 180: proper^#(U41(X1, X2)) -> c_180(U41^#(proper(X1), proper(X2))) 1084.46/297.18 -->_1 U41^#(ok(X1), ok(X2)) -> c_129(U41^#(X1, X2)) :89 1084.46/297.18 -->_1 U41^#(mark(X1), X2) -> c_128(U41^#(X1, X2)) :88 1084.46/297.18 1084.46/297.18 181: proper^#(U42(X)) -> c_181(U42^#(proper(X))) 1084.46/297.18 -->_1 U42^#(ok(X)) -> c_131(U42^#(X)) :139 1084.46/297.18 -->_1 U42^#(mark(X)) -> c_130(U42^#(X)) :138 1084.46/297.18 1084.46/297.18 182: proper^#(U51(X)) -> c_182(U51^#(proper(X))) 1084.46/297.18 -->_1 U51^#(ok(X)) -> c_133(U51^#(X)) :93 1084.46/297.18 -->_1 U51^#(mark(X)) -> c_132(U51^#(X)) :92 1084.46/297.18 1084.46/297.18 183: proper^#(U61(X1, X2)) -> c_183(U61^#(proper(X1), proper(X2))) 1084.46/297.18 -->_1 U61^#(ok(X1), ok(X2)) -> c_135(U61^#(X1, X2)) :91 1084.46/297.18 -->_1 U61^#(mark(X1), X2) -> c_134(U61^#(X1, X2)) :90 1084.46/297.18 1084.46/297.18 184: proper^#(U62(X)) -> c_184(U62^#(proper(X))) 1084.46/297.18 -->_1 U62^#(ok(X)) -> c_137(U62^#(X)) :141 1084.46/297.18 -->_1 U62^#(mark(X)) -> c_136(U62^#(X)) :140 1084.46/297.18 1084.46/297.18 185: proper^#(U71(X1, X2)) -> c_185(U71^#(proper(X1), proper(X2))) 1084.46/297.18 -->_1 U71^#(ok(X1), ok(X2)) -> c_139(U71^#(X1, X2)) :108 1084.46/297.18 -->_1 U71^#(mark(X1), X2) -> c_138(U71^#(X1, X2)) :107 1084.46/297.18 1084.46/297.18 186: proper^#(U72(X1, X2)) -> c_186(U72^#(proper(X1), proper(X2))) 1084.46/297.18 -->_1 U72^#(ok(X1), ok(X2)) -> c_141(U72^#(X1, X2)) :143 1084.46/297.18 -->_1 U72^#(mark(X1), X2) -> c_140(U72^#(X1, X2)) :142 1084.46/297.18 1084.46/297.18 187: proper^#(U81(X1, X2, X3)) -> 1084.46/297.18 c_187(U81^#(proper(X1), proper(X2), proper(X3))) 1084.46/297.18 -->_1 U81^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.18 c_143(U81^#(X1, X2, X3)) :106 1084.46/297.18 -->_1 U81^#(mark(X1), X2, X3) -> c_142(U81^#(X1, X2, X3)) :105 1084.46/297.18 1084.46/297.18 188: proper^#(U82(X1, X2, X3)) -> 1084.46/297.18 c_188(U82^#(proper(X1), proper(X2), proper(X3))) 1084.46/297.18 -->_1 U82^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.18 c_145(U82^#(X1, X2, X3)) :145 1084.46/297.18 -->_1 U82^#(mark(X1), X2, X3) -> c_144(U82^#(X1, X2, X3)) :144 1084.46/297.18 1084.46/297.18 189: proper^#(U83(X1, X2, X3)) -> 1084.46/297.18 c_189(U83^#(proper(X1), proper(X2), proper(X3))) 1084.46/297.18 -->_1 U83^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.18 c_147(U83^#(X1, X2, X3)) :147 1084.46/297.18 -->_1 U83^#(mark(X1), X2, X3) -> c_146(U83^#(X1, X2, X3)) :146 1084.46/297.18 1084.46/297.18 190: proper^#(U84(X1, X2, X3)) -> 1084.46/297.18 c_190(U84^#(proper(X1), proper(X2), proper(X3))) 1084.46/297.18 -->_1 U84^#(ok(X1), ok(X2), ok(X3)) -> 1084.46/297.18 c_149(U84^#(X1, X2, X3)) :149 1084.46/297.18 -->_1 U84^#(mark(X1), X2, X3) -> c_148(U84^#(X1, X2, X3)) :148 1084.46/297.18 1084.46/297.18 191: proper^#(s(X)) -> c_191(s^#(proper(X))) 1084.46/297.18 -->_1 s^#(ok(X)) -> c_151(s^#(X)) :151 1084.46/297.18 -->_1 s^#(mark(X)) -> c_150(s^#(X)) :150 1084.46/297.18 1084.46/297.18 192: proper^#(U91(X1, X2)) -> c_192(U91^#(proper(X1), proper(X2))) 1084.46/297.18 -->_1 U91^#(ok(X1), ok(X2)) -> c_153(U91^#(X1, X2)) :113 1084.46/297.18 -->_1 U91^#(mark(X1), X2) -> c_152(U91^#(X1, X2)) :112 1084.46/297.18 1084.46/297.18 193: proper^#(U92(X)) -> c_193(U92^#(proper(X))) 1084.46/297.18 -->_1 U92^#(ok(X)) -> c_155(U92^#(X)) :153 1084.46/297.18 -->_1 U92^#(mark(X)) -> c_154(U92^#(X)) :152 1084.46/297.18 1084.46/297.18 194: proper^#(0()) -> c_194() 1084.46/297.18 1084.46/297.18 195: top^#(mark(X)) -> c_195(top^#(proper(X))) 1084.46/297.18 -->_1 top^#(ok(X)) -> c_196(top^#(active(X))) :196 1084.46/297.18 -->_1 top^#(mark(X)) -> c_195(top^#(proper(X))) :195 1084.46/297.18 1084.46/297.18 196: top^#(ok(X)) -> c_196(top^#(active(X))) 1084.46/297.18 -->_1 top^#(ok(X)) -> c_196(top^#(active(X))) :196 1084.46/297.18 -->_1 top^#(mark(X)) -> c_195(top^#(proper(X))) :195 1084.46/297.18 1084.46/297.18 1084.46/297.18 Only the nodes 1084.46/297.18 {82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,104,103,105,106,107,108,109,111,110,112,113,114,115,116,117,118,119,120,121,122,123,124,125,126,127,128,129,130,131,132,133,134,135,136,137,138,139,140,141,142,143,144,145,146,147,148,149,150,151,152,153,154,155,157,194,195,196} 1084.46/297.18 are reachable from nodes 1084.46/297.18 {82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110,111,112,113,114,115,116,117,118,119,120,121,122,123,124,125,126,127,128,129,130,131,132,133,134,135,136,137,138,139,140,141,142,143,144,145,146,147,148,149,150,151,152,153,154,155,157,194,195,196} 1084.46/297.18 that start derivation from marked basic terms. The nodes not 1084.46/297.18 reachable are removed from the problem. 1084.46/297.18 1084.46/297.18 We are left with following problem, upon which TcT provides the 1084.46/297.18 certificate MAYBE. 1084.46/297.18 1084.46/297.18 Strict DPs: 1084.46/297.18 { U101^#(mark(X1), X2, X3) -> c_82(U101^#(X1, X2, X3)) 1084.46/297.18 , U101^#(ok(X1), ok(X2), ok(X3)) -> c_83(U101^#(X1, X2, X3)) 1084.46/297.18 , U102^#(mark(X1), X2, X3) -> c_84(U102^#(X1, X2, X3)) 1084.46/297.18 , U102^#(ok(X1), ok(X2), ok(X3)) -> c_85(U102^#(X1, X2, X3)) 1084.46/297.18 , U103^#(mark(X1), X2, X3) -> c_87(U103^#(X1, X2, X3)) 1084.46/297.18 , U103^#(ok(X1), ok(X2), ok(X3)) -> c_88(U103^#(X1, X2, X3)) 1084.46/297.18 , U41^#(mark(X1), X2) -> c_128(U41^#(X1, X2)) 1084.46/297.18 , U41^#(ok(X1), ok(X2)) -> c_129(U41^#(X1, X2)) 1084.46/297.18 , U61^#(mark(X1), X2) -> c_134(U61^#(X1, X2)) 1084.46/297.18 , U61^#(ok(X1), ok(X2)) -> c_135(U61^#(X1, X2)) 1084.46/297.18 , U51^#(mark(X)) -> c_132(U51^#(X)) 1084.46/297.18 , U51^#(ok(X)) -> c_133(U51^#(X)) 1084.46/297.18 , U104^#(mark(X1), X2, X3) -> c_90(U104^#(X1, X2, X3)) 1084.46/297.18 , U104^#(ok(X1), ok(X2), ok(X3)) -> c_91(U104^#(X1, X2, X3)) 1084.46/297.18 , U11^#(mark(X1), X2, X3) -> c_98(U11^#(X1, X2, X3)) 1084.46/297.18 , U11^#(ok(X1), ok(X2), ok(X3)) -> c_99(U11^#(X1, X2, X3)) 1084.46/297.18 , U31^#(mark(X1), X2, X3) -> c_116(U31^#(X1, X2, X3)) 1084.46/297.18 , U31^#(ok(X1), ok(X2), ok(X3)) -> c_117(U31^#(X1, X2, X3)) 1084.46/297.18 , U21^#(mark(X1), X2) -> c_110(U21^#(X1, X2)) 1084.46/297.18 , U21^#(ok(X1), ok(X2)) -> c_111(U21^#(X1, X2)) 1084.46/297.18 , plus^#(X1, mark(X2)) -> c_92(plus^#(X1, X2)) 1084.46/297.18 , plus^#(mark(X1), X2) -> c_93(plus^#(X1, X2)) 1084.46/297.18 , plus^#(ok(X1), ok(X2)) -> c_94(plus^#(X1, X2)) 1084.46/297.18 , U81^#(mark(X1), X2, X3) -> c_142(U81^#(X1, X2, X3)) 1084.46/297.18 , U81^#(ok(X1), ok(X2), ok(X3)) -> c_143(U81^#(X1, X2, X3)) 1084.46/297.18 , U71^#(mark(X1), X2) -> c_138(U71^#(X1, X2)) 1084.46/297.18 , U71^#(ok(X1), ok(X2)) -> c_139(U71^#(X1, X2)) 1084.46/297.18 , x^#(X1, mark(X2)) -> c_95(x^#(X1, X2)) 1084.46/297.18 , x^#(mark(X1), X2) -> c_96(x^#(X1, X2)) 1084.46/297.18 , x^#(ok(X1), ok(X2)) -> c_97(x^#(X1, X2)) 1084.46/297.18 , U91^#(mark(X1), X2) -> c_152(U91^#(X1, X2)) 1084.46/297.18 , U91^#(ok(X1), ok(X2)) -> c_153(U91^#(X1, X2)) 1084.46/297.18 , U12^#(mark(X1), X2, X3) -> c_100(U12^#(X1, X2, X3)) 1084.46/297.18 , U12^#(ok(X1), ok(X2), ok(X3)) -> c_101(U12^#(X1, X2, X3)) 1084.46/297.18 , U13^#(mark(X1), X2, X3) -> c_102(U13^#(X1, X2, X3)) 1084.46/297.18 , U13^#(ok(X1), ok(X2), ok(X3)) -> c_103(U13^#(X1, X2, X3)) 1084.46/297.18 , U14^#(mark(X1), X2, X3) -> c_104(U14^#(X1, X2, X3)) 1084.46/297.18 , U14^#(ok(X1), ok(X2), ok(X3)) -> c_105(U14^#(X1, X2, X3)) 1084.46/297.18 , U15^#(mark(X1), X2) -> c_106(U15^#(X1, X2)) 1084.46/297.18 , U15^#(ok(X1), ok(X2)) -> c_107(U15^#(X1, X2)) 1084.46/297.18 , U16^#(mark(X)) -> c_108(U16^#(X)) 1084.46/297.18 , U16^#(ok(X)) -> c_109(U16^#(X)) 1084.46/297.18 , U22^#(mark(X1), X2) -> c_112(U22^#(X1, X2)) 1084.46/297.18 , U22^#(ok(X1), ok(X2)) -> c_113(U22^#(X1, X2)) 1084.46/297.18 , U23^#(mark(X)) -> c_114(U23^#(X)) 1084.46/297.18 , U23^#(ok(X)) -> c_115(U23^#(X)) 1084.46/297.18 , U32^#(mark(X1), X2, X3) -> c_118(U32^#(X1, X2, X3)) 1084.46/297.18 , U32^#(ok(X1), ok(X2), ok(X3)) -> c_119(U32^#(X1, X2, X3)) 1084.46/297.18 , U33^#(mark(X1), X2, X3) -> c_120(U33^#(X1, X2, X3)) 1084.46/297.18 , U33^#(ok(X1), ok(X2), ok(X3)) -> c_121(U33^#(X1, X2, X3)) 1084.46/297.18 , U34^#(mark(X1), X2, X3) -> c_122(U34^#(X1, X2, X3)) 1084.46/297.18 , U34^#(ok(X1), ok(X2), ok(X3)) -> c_123(U34^#(X1, X2, X3)) 1084.46/297.18 , U35^#(mark(X1), X2) -> c_124(U35^#(X1, X2)) 1084.46/297.18 , U35^#(ok(X1), ok(X2)) -> c_125(U35^#(X1, X2)) 1084.46/297.18 , U36^#(mark(X)) -> c_126(U36^#(X)) 1084.46/297.18 , U36^#(ok(X)) -> c_127(U36^#(X)) 1084.46/297.18 , U42^#(mark(X)) -> c_130(U42^#(X)) 1084.46/297.18 , U42^#(ok(X)) -> c_131(U42^#(X)) 1084.46/297.18 , U62^#(mark(X)) -> c_136(U62^#(X)) 1084.46/297.18 , U62^#(ok(X)) -> c_137(U62^#(X)) 1084.46/297.18 , U72^#(mark(X1), X2) -> c_140(U72^#(X1, X2)) 1084.46/297.18 , U72^#(ok(X1), ok(X2)) -> c_141(U72^#(X1, X2)) 1084.46/297.18 , U82^#(mark(X1), X2, X3) -> c_144(U82^#(X1, X2, X3)) 1084.46/297.18 , U82^#(ok(X1), ok(X2), ok(X3)) -> c_145(U82^#(X1, X2, X3)) 1084.46/297.18 , U83^#(mark(X1), X2, X3) -> c_146(U83^#(X1, X2, X3)) 1084.46/297.18 , U83^#(ok(X1), ok(X2), ok(X3)) -> c_147(U83^#(X1, X2, X3)) 1084.46/297.18 , U84^#(mark(X1), X2, X3) -> c_148(U84^#(X1, X2, X3)) 1084.46/297.18 , U84^#(ok(X1), ok(X2), ok(X3)) -> c_149(U84^#(X1, X2, X3)) 1084.46/297.18 , s^#(mark(X)) -> c_150(s^#(X)) 1084.46/297.18 , s^#(ok(X)) -> c_151(s^#(X)) 1084.46/297.18 , U92^#(mark(X)) -> c_154(U92^#(X)) 1084.46/297.18 , U92^#(ok(X)) -> c_155(U92^#(X)) 1084.46/297.18 , isNatKind^#(ok(X)) -> c_86(isNatKind^#(X)) 1084.46/297.18 , isNat^#(ok(X)) -> c_89(isNat^#(X)) 1084.46/297.18 , proper^#(tt()) -> c_157() 1084.46/297.18 , proper^#(0()) -> c_194() 1084.46/297.18 , top^#(mark(X)) -> c_195(top^#(proper(X))) 1084.46/297.18 , top^#(ok(X)) -> c_196(top^#(active(X))) } 1084.46/297.18 Strict Trs: 1084.46/297.18 { active(U101(X1, X2, X3)) -> U101(active(X1), X2, X3) 1084.46/297.18 , active(U101(tt(), M, N)) -> mark(U102(isNatKind(M), M, N)) 1084.46/297.18 , active(U102(X1, X2, X3)) -> U102(active(X1), X2, X3) 1084.46/297.19 , active(U102(tt(), M, N)) -> mark(U103(isNat(N), M, N)) 1084.46/297.19 , active(isNatKind(plus(V1, V2))) -> mark(U41(isNatKind(V1), V2)) 1084.46/297.19 , active(isNatKind(x(V1, V2))) -> mark(U61(isNatKind(V1), V2)) 1084.46/297.19 , active(isNatKind(s(V1))) -> mark(U51(isNatKind(V1))) 1084.46/297.19 , active(isNatKind(0())) -> mark(tt()) 1084.46/297.19 , active(U103(X1, X2, X3)) -> U103(active(X1), X2, X3) 1084.46/297.19 , active(U103(tt(), M, N)) -> mark(U104(isNatKind(N), M, N)) 1084.46/297.19 , active(isNat(plus(V1, V2))) -> mark(U11(isNatKind(V1), V1, V2)) 1084.46/297.19 , active(isNat(x(V1, V2))) -> mark(U31(isNatKind(V1), V1, V2)) 1084.46/297.19 , active(isNat(s(V1))) -> mark(U21(isNatKind(V1), V1)) 1084.46/297.19 , active(isNat(0())) -> mark(tt()) 1084.46/297.19 , active(U104(X1, X2, X3)) -> U104(active(X1), X2, X3) 1084.46/297.19 , active(U104(tt(), M, N)) -> mark(plus(x(N, M), N)) 1084.46/297.19 , active(plus(X1, X2)) -> plus(X1, active(X2)) 1084.46/297.19 , active(plus(X1, X2)) -> plus(active(X1), X2) 1084.46/297.19 , active(plus(N, s(M))) -> mark(U81(isNat(M), M, N)) 1084.46/297.19 , active(plus(N, 0())) -> mark(U71(isNat(N), N)) 1084.46/297.19 , active(x(X1, X2)) -> x(X1, active(X2)) 1084.46/297.19 , active(x(X1, X2)) -> x(active(X1), X2) 1084.46/297.19 , active(x(N, s(M))) -> mark(U101(isNat(M), M, N)) 1084.46/297.19 , active(x(N, 0())) -> mark(U91(isNat(N), N)) 1084.46/297.19 , active(U11(X1, X2, X3)) -> U11(active(X1), X2, X3) 1084.46/297.19 , active(U11(tt(), V1, V2)) -> mark(U12(isNatKind(V1), V1, V2)) 1084.46/297.19 , active(U12(X1, X2, X3)) -> U12(active(X1), X2, X3) 1084.46/297.19 , active(U12(tt(), V1, V2)) -> mark(U13(isNatKind(V2), V1, V2)) 1084.46/297.19 , active(U13(X1, X2, X3)) -> U13(active(X1), X2, X3) 1084.46/297.19 , active(U13(tt(), V1, V2)) -> mark(U14(isNatKind(V2), V1, V2)) 1084.46/297.19 , active(U14(X1, X2, X3)) -> U14(active(X1), X2, X3) 1084.46/297.19 , active(U14(tt(), V1, V2)) -> mark(U15(isNat(V1), V2)) 1084.46/297.19 , active(U15(X1, X2)) -> U15(active(X1), X2) 1084.46/297.19 , active(U15(tt(), V2)) -> mark(U16(isNat(V2))) 1084.46/297.19 , active(U16(X)) -> U16(active(X)) 1084.46/297.19 , active(U16(tt())) -> mark(tt()) 1084.46/297.19 , active(U21(X1, X2)) -> U21(active(X1), X2) 1084.46/297.19 , active(U21(tt(), V1)) -> mark(U22(isNatKind(V1), V1)) 1084.46/297.19 , active(U22(X1, X2)) -> U22(active(X1), X2) 1084.46/297.19 , active(U22(tt(), V1)) -> mark(U23(isNat(V1))) 1084.46/297.19 , active(U23(X)) -> U23(active(X)) 1084.46/297.19 , active(U23(tt())) -> mark(tt()) 1084.46/297.19 , active(U31(X1, X2, X3)) -> U31(active(X1), X2, X3) 1084.46/297.19 , active(U31(tt(), V1, V2)) -> mark(U32(isNatKind(V1), V1, V2)) 1084.46/297.19 , active(U32(X1, X2, X3)) -> U32(active(X1), X2, X3) 1084.46/297.19 , active(U32(tt(), V1, V2)) -> mark(U33(isNatKind(V2), V1, V2)) 1084.46/297.19 , active(U33(X1, X2, X3)) -> U33(active(X1), X2, X3) 1084.46/297.19 , active(U33(tt(), V1, V2)) -> mark(U34(isNatKind(V2), V1, V2)) 1084.46/297.19 , active(U34(X1, X2, X3)) -> U34(active(X1), X2, X3) 1084.46/297.19 , active(U34(tt(), V1, V2)) -> mark(U35(isNat(V1), V2)) 1084.46/297.19 , active(U35(X1, X2)) -> U35(active(X1), X2) 1084.46/297.19 , active(U35(tt(), V2)) -> mark(U36(isNat(V2))) 1084.46/297.19 , active(U36(X)) -> U36(active(X)) 1084.46/297.19 , active(U36(tt())) -> mark(tt()) 1084.46/297.19 , active(U41(X1, X2)) -> U41(active(X1), X2) 1084.46/297.19 , active(U41(tt(), V2)) -> mark(U42(isNatKind(V2))) 1084.46/297.19 , active(U42(X)) -> U42(active(X)) 1084.46/297.19 , active(U42(tt())) -> mark(tt()) 1084.46/297.19 , active(U51(X)) -> U51(active(X)) 1084.46/297.19 , active(U51(tt())) -> mark(tt()) 1084.46/297.19 , active(U61(X1, X2)) -> U61(active(X1), X2) 1084.46/297.19 , active(U61(tt(), V2)) -> mark(U62(isNatKind(V2))) 1084.46/297.19 , active(U62(X)) -> U62(active(X)) 1084.46/297.19 , active(U62(tt())) -> mark(tt()) 1084.46/297.19 , active(U71(X1, X2)) -> U71(active(X1), X2) 1084.46/297.19 , active(U71(tt(), N)) -> mark(U72(isNatKind(N), N)) 1084.46/297.19 , active(U72(X1, X2)) -> U72(active(X1), X2) 1084.46/297.19 , active(U72(tt(), N)) -> mark(N) 1084.46/297.19 , active(U81(X1, X2, X3)) -> U81(active(X1), X2, X3) 1084.46/297.19 , active(U81(tt(), M, N)) -> mark(U82(isNatKind(M), M, N)) 1084.46/297.19 , active(U82(X1, X2, X3)) -> U82(active(X1), X2, X3) 1084.46/297.19 , active(U82(tt(), M, N)) -> mark(U83(isNat(N), M, N)) 1084.46/297.19 , active(U83(X1, X2, X3)) -> U83(active(X1), X2, X3) 1084.46/297.19 , active(U83(tt(), M, N)) -> mark(U84(isNatKind(N), M, N)) 1084.46/297.19 , active(U84(X1, X2, X3)) -> U84(active(X1), X2, X3) 1084.46/297.19 , active(U84(tt(), M, N)) -> mark(s(plus(N, M))) 1084.46/297.19 , active(s(X)) -> s(active(X)) 1084.46/297.19 , active(U91(X1, X2)) -> U91(active(X1), X2) 1084.46/297.19 , active(U91(tt(), N)) -> mark(U92(isNatKind(N))) 1084.46/297.19 , active(U92(X)) -> U92(active(X)) 1084.46/297.19 , active(U92(tt())) -> mark(0()) 1084.46/297.19 , U101(mark(X1), X2, X3) -> mark(U101(X1, X2, X3)) 1084.46/297.19 , U101(ok(X1), ok(X2), ok(X3)) -> ok(U101(X1, X2, X3)) 1084.46/297.19 , U102(mark(X1), X2, X3) -> mark(U102(X1, X2, X3)) 1084.46/297.19 , U102(ok(X1), ok(X2), ok(X3)) -> ok(U102(X1, X2, X3)) 1084.46/297.19 , isNatKind(ok(X)) -> ok(isNatKind(X)) 1084.46/297.19 , U103(mark(X1), X2, X3) -> mark(U103(X1, X2, X3)) 1084.46/297.19 , U103(ok(X1), ok(X2), ok(X3)) -> ok(U103(X1, X2, X3)) 1084.46/297.19 , isNat(ok(X)) -> ok(isNat(X)) 1084.46/297.19 , U104(mark(X1), X2, X3) -> mark(U104(X1, X2, X3)) 1084.46/297.19 , U104(ok(X1), ok(X2), ok(X3)) -> ok(U104(X1, X2, X3)) 1084.46/297.19 , plus(X1, mark(X2)) -> mark(plus(X1, X2)) 1084.46/297.19 , plus(mark(X1), X2) -> mark(plus(X1, X2)) 1084.46/297.19 , plus(ok(X1), ok(X2)) -> ok(plus(X1, X2)) 1084.46/297.19 , x(X1, mark(X2)) -> mark(x(X1, X2)) 1084.46/297.19 , x(mark(X1), X2) -> mark(x(X1, X2)) 1084.46/297.19 , x(ok(X1), ok(X2)) -> ok(x(X1, X2)) 1084.46/297.19 , U11(mark(X1), X2, X3) -> mark(U11(X1, X2, X3)) 1084.46/297.19 , U11(ok(X1), ok(X2), ok(X3)) -> ok(U11(X1, X2, X3)) 1084.46/297.19 , U12(mark(X1), X2, X3) -> mark(U12(X1, X2, X3)) 1084.46/297.19 , U12(ok(X1), ok(X2), ok(X3)) -> ok(U12(X1, X2, X3)) 1084.46/297.19 , U13(mark(X1), X2, X3) -> mark(U13(X1, X2, X3)) 1084.46/297.19 , U13(ok(X1), ok(X2), ok(X3)) -> ok(U13(X1, X2, X3)) 1084.46/297.19 , U14(mark(X1), X2, X3) -> mark(U14(X1, X2, X3)) 1084.46/297.19 , U14(ok(X1), ok(X2), ok(X3)) -> ok(U14(X1, X2, X3)) 1084.46/297.19 , U15(mark(X1), X2) -> mark(U15(X1, X2)) 1084.46/297.19 , U15(ok(X1), ok(X2)) -> ok(U15(X1, X2)) 1084.46/297.19 , U16(mark(X)) -> mark(U16(X)) 1084.46/297.19 , U16(ok(X)) -> ok(U16(X)) 1084.46/297.19 , U21(mark(X1), X2) -> mark(U21(X1, X2)) 1084.46/297.19 , U21(ok(X1), ok(X2)) -> ok(U21(X1, X2)) 1084.46/297.19 , U22(mark(X1), X2) -> mark(U22(X1, X2)) 1084.46/297.19 , U22(ok(X1), ok(X2)) -> ok(U22(X1, X2)) 1084.46/297.19 , U23(mark(X)) -> mark(U23(X)) 1084.46/297.19 , U23(ok(X)) -> ok(U23(X)) 1084.46/297.19 , U31(mark(X1), X2, X3) -> mark(U31(X1, X2, X3)) 1084.46/297.19 , U31(ok(X1), ok(X2), ok(X3)) -> ok(U31(X1, X2, X3)) 1084.46/297.19 , U32(mark(X1), X2, X3) -> mark(U32(X1, X2, X3)) 1084.46/297.19 , U32(ok(X1), ok(X2), ok(X3)) -> ok(U32(X1, X2, X3)) 1084.46/297.19 , U33(mark(X1), X2, X3) -> mark(U33(X1, X2, X3)) 1084.46/297.19 , U33(ok(X1), ok(X2), ok(X3)) -> ok(U33(X1, X2, X3)) 1084.46/297.19 , U34(mark(X1), X2, X3) -> mark(U34(X1, X2, X3)) 1084.46/297.19 , U34(ok(X1), ok(X2), ok(X3)) -> ok(U34(X1, X2, X3)) 1084.46/297.19 , U35(mark(X1), X2) -> mark(U35(X1, X2)) 1084.46/297.19 , U35(ok(X1), ok(X2)) -> ok(U35(X1, X2)) 1084.46/297.19 , U36(mark(X)) -> mark(U36(X)) 1084.46/297.19 , U36(ok(X)) -> ok(U36(X)) 1084.46/297.19 , U41(mark(X1), X2) -> mark(U41(X1, X2)) 1084.46/297.19 , U41(ok(X1), ok(X2)) -> ok(U41(X1, X2)) 1084.46/297.19 , U42(mark(X)) -> mark(U42(X)) 1084.46/297.19 , U42(ok(X)) -> ok(U42(X)) 1084.46/297.19 , U51(mark(X)) -> mark(U51(X)) 1084.46/297.19 , U51(ok(X)) -> ok(U51(X)) 1084.46/297.19 , U61(mark(X1), X2) -> mark(U61(X1, X2)) 1084.46/297.19 , U61(ok(X1), ok(X2)) -> ok(U61(X1, X2)) 1084.46/297.19 , U62(mark(X)) -> mark(U62(X)) 1084.46/297.19 , U62(ok(X)) -> ok(U62(X)) 1084.46/297.19 , U71(mark(X1), X2) -> mark(U71(X1, X2)) 1084.46/297.19 , U71(ok(X1), ok(X2)) -> ok(U71(X1, X2)) 1084.46/297.19 , U72(mark(X1), X2) -> mark(U72(X1, X2)) 1084.46/297.19 , U72(ok(X1), ok(X2)) -> ok(U72(X1, X2)) 1084.46/297.19 , U81(mark(X1), X2, X3) -> mark(U81(X1, X2, X3)) 1084.46/297.19 , U81(ok(X1), ok(X2), ok(X3)) -> ok(U81(X1, X2, X3)) 1084.46/297.19 , U82(mark(X1), X2, X3) -> mark(U82(X1, X2, X3)) 1084.46/297.19 , U82(ok(X1), ok(X2), ok(X3)) -> ok(U82(X1, X2, X3)) 1084.46/297.19 , U83(mark(X1), X2, X3) -> mark(U83(X1, X2, X3)) 1084.46/297.19 , U83(ok(X1), ok(X2), ok(X3)) -> ok(U83(X1, X2, X3)) 1084.46/297.19 , U84(mark(X1), X2, X3) -> mark(U84(X1, X2, X3)) 1084.46/297.19 , U84(ok(X1), ok(X2), ok(X3)) -> ok(U84(X1, X2, X3)) 1084.46/297.19 , s(mark(X)) -> mark(s(X)) 1084.46/297.19 , s(ok(X)) -> ok(s(X)) 1084.46/297.19 , U91(mark(X1), X2) -> mark(U91(X1, X2)) 1084.46/297.19 , U91(ok(X1), ok(X2)) -> ok(U91(X1, X2)) 1084.46/297.19 , U92(mark(X)) -> mark(U92(X)) 1084.46/297.19 , U92(ok(X)) -> ok(U92(X)) 1084.46/297.19 , proper(U101(X1, X2, X3)) -> 1084.46/297.19 U101(proper(X1), proper(X2), proper(X3)) 1084.46/297.19 , proper(tt()) -> ok(tt()) 1084.46/297.19 , proper(U102(X1, X2, X3)) -> 1084.46/297.19 U102(proper(X1), proper(X2), proper(X3)) 1084.46/297.19 , proper(isNatKind(X)) -> isNatKind(proper(X)) 1084.46/297.19 , proper(U103(X1, X2, X3)) -> 1084.46/297.19 U103(proper(X1), proper(X2), proper(X3)) 1084.46/297.19 , proper(isNat(X)) -> isNat(proper(X)) 1084.46/297.19 , proper(U104(X1, X2, X3)) -> 1084.46/297.19 U104(proper(X1), proper(X2), proper(X3)) 1084.46/297.19 , proper(plus(X1, X2)) -> plus(proper(X1), proper(X2)) 1084.46/297.19 , proper(x(X1, X2)) -> x(proper(X1), proper(X2)) 1084.46/297.19 , proper(U11(X1, X2, X3)) -> 1084.46/297.19 U11(proper(X1), proper(X2), proper(X3)) 1084.46/297.19 , proper(U12(X1, X2, X3)) -> 1084.46/297.19 U12(proper(X1), proper(X2), proper(X3)) 1084.46/297.19 , proper(U13(X1, X2, X3)) -> 1084.46/297.19 U13(proper(X1), proper(X2), proper(X3)) 1084.46/297.19 , proper(U14(X1, X2, X3)) -> 1084.46/297.19 U14(proper(X1), proper(X2), proper(X3)) 1084.46/297.19 , proper(U15(X1, X2)) -> U15(proper(X1), proper(X2)) 1084.46/297.19 , proper(U16(X)) -> U16(proper(X)) 1084.46/297.19 , proper(U21(X1, X2)) -> U21(proper(X1), proper(X2)) 1084.46/297.19 , proper(U22(X1, X2)) -> U22(proper(X1), proper(X2)) 1084.46/297.19 , proper(U23(X)) -> U23(proper(X)) 1084.46/297.19 , proper(U31(X1, X2, X3)) -> 1084.46/297.19 U31(proper(X1), proper(X2), proper(X3)) 1084.46/297.19 , proper(U32(X1, X2, X3)) -> 1084.46/297.19 U32(proper(X1), proper(X2), proper(X3)) 1084.46/297.19 , proper(U33(X1, X2, X3)) -> 1084.46/297.19 U33(proper(X1), proper(X2), proper(X3)) 1084.46/297.19 , proper(U34(X1, X2, X3)) -> 1084.46/297.19 U34(proper(X1), proper(X2), proper(X3)) 1084.46/297.19 , proper(U35(X1, X2)) -> U35(proper(X1), proper(X2)) 1084.46/297.19 , proper(U36(X)) -> U36(proper(X)) 1084.46/297.19 , proper(U41(X1, X2)) -> U41(proper(X1), proper(X2)) 1084.46/297.19 , proper(U42(X)) -> U42(proper(X)) 1084.46/297.19 , proper(U51(X)) -> U51(proper(X)) 1084.46/297.19 , proper(U61(X1, X2)) -> U61(proper(X1), proper(X2)) 1084.46/297.19 , proper(U62(X)) -> U62(proper(X)) 1084.46/297.19 , proper(U71(X1, X2)) -> U71(proper(X1), proper(X2)) 1084.46/297.19 , proper(U72(X1, X2)) -> U72(proper(X1), proper(X2)) 1084.46/297.19 , proper(U81(X1, X2, X3)) -> 1084.46/297.19 U81(proper(X1), proper(X2), proper(X3)) 1084.46/297.19 , proper(U82(X1, X2, X3)) -> 1084.46/297.19 U82(proper(X1), proper(X2), proper(X3)) 1084.46/297.19 , proper(U83(X1, X2, X3)) -> 1084.46/297.19 U83(proper(X1), proper(X2), proper(X3)) 1084.46/297.19 , proper(U84(X1, X2, X3)) -> 1084.46/297.19 U84(proper(X1), proper(X2), proper(X3)) 1084.46/297.19 , proper(s(X)) -> s(proper(X)) 1084.46/297.19 , proper(U91(X1, X2)) -> U91(proper(X1), proper(X2)) 1084.46/297.19 , proper(U92(X)) -> U92(proper(X)) 1084.46/297.19 , proper(0()) -> ok(0()) 1084.46/297.19 , top(mark(X)) -> top(proper(X)) 1084.46/297.19 , top(ok(X)) -> top(active(X)) } 1084.46/297.19 Obligation: 1084.46/297.19 runtime complexity 1084.46/297.19 Answer: 1084.46/297.19 MAYBE 1084.46/297.19 1084.46/297.19 We estimate the number of application of {75,76} by applications of 1084.46/297.19 Pre({75,76}) = {}. Here rules are labeled as follows: 1084.46/297.19 1084.46/297.19 DPs: 1084.46/297.19 { 1: U101^#(mark(X1), X2, X3) -> c_82(U101^#(X1, X2, X3)) 1084.46/297.19 , 2: U101^#(ok(X1), ok(X2), ok(X3)) -> c_83(U101^#(X1, X2, X3)) 1084.46/297.19 , 3: U102^#(mark(X1), X2, X3) -> c_84(U102^#(X1, X2, X3)) 1084.46/297.19 , 4: U102^#(ok(X1), ok(X2), ok(X3)) -> c_85(U102^#(X1, X2, X3)) 1084.46/297.19 , 5: U103^#(mark(X1), X2, X3) -> c_87(U103^#(X1, X2, X3)) 1084.46/297.19 , 6: U103^#(ok(X1), ok(X2), ok(X3)) -> c_88(U103^#(X1, X2, X3)) 1084.46/297.19 , 7: U41^#(mark(X1), X2) -> c_128(U41^#(X1, X2)) 1084.46/297.19 , 8: U41^#(ok(X1), ok(X2)) -> c_129(U41^#(X1, X2)) 1084.46/297.19 , 9: U61^#(mark(X1), X2) -> c_134(U61^#(X1, X2)) 1084.46/297.19 , 10: U61^#(ok(X1), ok(X2)) -> c_135(U61^#(X1, X2)) 1084.46/297.19 , 11: U51^#(mark(X)) -> c_132(U51^#(X)) 1084.46/297.19 , 12: U51^#(ok(X)) -> c_133(U51^#(X)) 1084.46/297.19 , 13: U104^#(mark(X1), X2, X3) -> c_90(U104^#(X1, X2, X3)) 1084.46/297.19 , 14: U104^#(ok(X1), ok(X2), ok(X3)) -> c_91(U104^#(X1, X2, X3)) 1084.46/297.19 , 15: U11^#(mark(X1), X2, X3) -> c_98(U11^#(X1, X2, X3)) 1084.46/297.19 , 16: U11^#(ok(X1), ok(X2), ok(X3)) -> c_99(U11^#(X1, X2, X3)) 1084.46/297.19 , 17: U31^#(mark(X1), X2, X3) -> c_116(U31^#(X1, X2, X3)) 1084.46/297.19 , 18: U31^#(ok(X1), ok(X2), ok(X3)) -> c_117(U31^#(X1, X2, X3)) 1084.46/297.19 , 19: U21^#(mark(X1), X2) -> c_110(U21^#(X1, X2)) 1084.46/297.19 , 20: U21^#(ok(X1), ok(X2)) -> c_111(U21^#(X1, X2)) 1084.46/297.19 , 21: plus^#(X1, mark(X2)) -> c_92(plus^#(X1, X2)) 1084.46/297.19 , 22: plus^#(mark(X1), X2) -> c_93(plus^#(X1, X2)) 1084.46/297.19 , 23: plus^#(ok(X1), ok(X2)) -> c_94(plus^#(X1, X2)) 1084.46/297.19 , 24: U81^#(mark(X1), X2, X3) -> c_142(U81^#(X1, X2, X3)) 1084.46/297.19 , 25: U81^#(ok(X1), ok(X2), ok(X3)) -> c_143(U81^#(X1, X2, X3)) 1084.46/297.19 , 26: U71^#(mark(X1), X2) -> c_138(U71^#(X1, X2)) 1084.46/297.19 , 27: U71^#(ok(X1), ok(X2)) -> c_139(U71^#(X1, X2)) 1084.46/297.19 , 28: x^#(X1, mark(X2)) -> c_95(x^#(X1, X2)) 1084.46/297.19 , 29: x^#(mark(X1), X2) -> c_96(x^#(X1, X2)) 1084.46/297.19 , 30: x^#(ok(X1), ok(X2)) -> c_97(x^#(X1, X2)) 1084.46/297.19 , 31: U91^#(mark(X1), X2) -> c_152(U91^#(X1, X2)) 1084.46/297.19 , 32: U91^#(ok(X1), ok(X2)) -> c_153(U91^#(X1, X2)) 1084.46/297.19 , 33: U12^#(mark(X1), X2, X3) -> c_100(U12^#(X1, X2, X3)) 1084.46/297.19 , 34: U12^#(ok(X1), ok(X2), ok(X3)) -> c_101(U12^#(X1, X2, X3)) 1084.46/297.19 , 35: U13^#(mark(X1), X2, X3) -> c_102(U13^#(X1, X2, X3)) 1084.46/297.19 , 36: U13^#(ok(X1), ok(X2), ok(X3)) -> c_103(U13^#(X1, X2, X3)) 1084.46/297.19 , 37: U14^#(mark(X1), X2, X3) -> c_104(U14^#(X1, X2, X3)) 1084.46/297.19 , 38: U14^#(ok(X1), ok(X2), ok(X3)) -> c_105(U14^#(X1, X2, X3)) 1084.46/297.19 , 39: U15^#(mark(X1), X2) -> c_106(U15^#(X1, X2)) 1084.46/297.19 , 40: U15^#(ok(X1), ok(X2)) -> c_107(U15^#(X1, X2)) 1084.46/297.19 , 41: U16^#(mark(X)) -> c_108(U16^#(X)) 1084.46/297.19 , 42: U16^#(ok(X)) -> c_109(U16^#(X)) 1084.46/297.19 , 43: U22^#(mark(X1), X2) -> c_112(U22^#(X1, X2)) 1084.46/297.19 , 44: U22^#(ok(X1), ok(X2)) -> c_113(U22^#(X1, X2)) 1084.46/297.19 , 45: U23^#(mark(X)) -> c_114(U23^#(X)) 1084.46/297.19 , 46: U23^#(ok(X)) -> c_115(U23^#(X)) 1084.46/297.19 , 47: U32^#(mark(X1), X2, X3) -> c_118(U32^#(X1, X2, X3)) 1084.46/297.19 , 48: U32^#(ok(X1), ok(X2), ok(X3)) -> c_119(U32^#(X1, X2, X3)) 1084.46/297.19 , 49: U33^#(mark(X1), X2, X3) -> c_120(U33^#(X1, X2, X3)) 1084.46/297.19 , 50: U33^#(ok(X1), ok(X2), ok(X3)) -> c_121(U33^#(X1, X2, X3)) 1084.46/297.19 , 51: U34^#(mark(X1), X2, X3) -> c_122(U34^#(X1, X2, X3)) 1084.46/297.19 , 52: U34^#(ok(X1), ok(X2), ok(X3)) -> c_123(U34^#(X1, X2, X3)) 1084.46/297.19 , 53: U35^#(mark(X1), X2) -> c_124(U35^#(X1, X2)) 1084.46/297.19 , 54: U35^#(ok(X1), ok(X2)) -> c_125(U35^#(X1, X2)) 1084.46/297.19 , 55: U36^#(mark(X)) -> c_126(U36^#(X)) 1084.46/297.19 , 56: U36^#(ok(X)) -> c_127(U36^#(X)) 1084.46/297.19 , 57: U42^#(mark(X)) -> c_130(U42^#(X)) 1084.46/297.19 , 58: U42^#(ok(X)) -> c_131(U42^#(X)) 1084.46/297.19 , 59: U62^#(mark(X)) -> c_136(U62^#(X)) 1084.46/297.19 , 60: U62^#(ok(X)) -> c_137(U62^#(X)) 1084.46/297.19 , 61: U72^#(mark(X1), X2) -> c_140(U72^#(X1, X2)) 1084.46/297.19 , 62: U72^#(ok(X1), ok(X2)) -> c_141(U72^#(X1, X2)) 1084.46/297.19 , 63: U82^#(mark(X1), X2, X3) -> c_144(U82^#(X1, X2, X3)) 1084.46/297.19 , 64: U82^#(ok(X1), ok(X2), ok(X3)) -> c_145(U82^#(X1, X2, X3)) 1084.46/297.19 , 65: U83^#(mark(X1), X2, X3) -> c_146(U83^#(X1, X2, X3)) 1084.46/297.19 , 66: U83^#(ok(X1), ok(X2), ok(X3)) -> c_147(U83^#(X1, X2, X3)) 1084.46/297.19 , 67: U84^#(mark(X1), X2, X3) -> c_148(U84^#(X1, X2, X3)) 1084.46/297.19 , 68: U84^#(ok(X1), ok(X2), ok(X3)) -> c_149(U84^#(X1, X2, X3)) 1084.46/297.19 , 69: s^#(mark(X)) -> c_150(s^#(X)) 1084.46/297.19 , 70: s^#(ok(X)) -> c_151(s^#(X)) 1084.46/297.19 , 71: U92^#(mark(X)) -> c_154(U92^#(X)) 1084.46/297.19 , 72: U92^#(ok(X)) -> c_155(U92^#(X)) 1084.46/297.19 , 73: isNatKind^#(ok(X)) -> c_86(isNatKind^#(X)) 1084.46/297.19 , 74: isNat^#(ok(X)) -> c_89(isNat^#(X)) 1084.46/297.19 , 75: proper^#(tt()) -> c_157() 1084.46/297.19 , 76: proper^#(0()) -> c_194() 1084.46/297.19 , 77: top^#(mark(X)) -> c_195(top^#(proper(X))) 1084.46/297.19 , 78: top^#(ok(X)) -> c_196(top^#(active(X))) } 1084.46/297.19 1084.46/297.19 We are left with following problem, upon which TcT provides the 1084.46/297.19 certificate MAYBE. 1084.46/297.19 1084.46/297.19 Strict DPs: 1084.46/297.19 { U101^#(mark(X1), X2, X3) -> c_82(U101^#(X1, X2, X3)) 1084.46/297.19 , U101^#(ok(X1), ok(X2), ok(X3)) -> c_83(U101^#(X1, X2, X3)) 1084.46/297.19 , U102^#(mark(X1), X2, X3) -> c_84(U102^#(X1, X2, X3)) 1084.46/297.19 , U102^#(ok(X1), ok(X2), ok(X3)) -> c_85(U102^#(X1, X2, X3)) 1084.46/297.19 , U103^#(mark(X1), X2, X3) -> c_87(U103^#(X1, X2, X3)) 1084.46/297.19 , U103^#(ok(X1), ok(X2), ok(X3)) -> c_88(U103^#(X1, X2, X3)) 1084.46/297.19 , U41^#(mark(X1), X2) -> c_128(U41^#(X1, X2)) 1084.46/297.19 , U41^#(ok(X1), ok(X2)) -> c_129(U41^#(X1, X2)) 1084.46/297.19 , U61^#(mark(X1), X2) -> c_134(U61^#(X1, X2)) 1084.46/297.19 , U61^#(ok(X1), ok(X2)) -> c_135(U61^#(X1, X2)) 1084.46/297.19 , U51^#(mark(X)) -> c_132(U51^#(X)) 1084.46/297.19 , U51^#(ok(X)) -> c_133(U51^#(X)) 1084.46/297.19 , U104^#(mark(X1), X2, X3) -> c_90(U104^#(X1, X2, X3)) 1084.46/297.19 , U104^#(ok(X1), ok(X2), ok(X3)) -> c_91(U104^#(X1, X2, X3)) 1084.46/297.19 , U11^#(mark(X1), X2, X3) -> c_98(U11^#(X1, X2, X3)) 1084.46/297.19 , U11^#(ok(X1), ok(X2), ok(X3)) -> c_99(U11^#(X1, X2, X3)) 1084.46/297.19 , U31^#(mark(X1), X2, X3) -> c_116(U31^#(X1, X2, X3)) 1084.46/297.19 , U31^#(ok(X1), ok(X2), ok(X3)) -> c_117(U31^#(X1, X2, X3)) 1084.46/297.19 , U21^#(mark(X1), X2) -> c_110(U21^#(X1, X2)) 1084.67/297.20 , U21^#(ok(X1), ok(X2)) -> c_111(U21^#(X1, X2)) 1084.67/297.20 , plus^#(X1, mark(X2)) -> c_92(plus^#(X1, X2)) 1084.67/297.20 , plus^#(mark(X1), X2) -> c_93(plus^#(X1, X2)) 1084.67/297.20 , plus^#(ok(X1), ok(X2)) -> c_94(plus^#(X1, X2)) 1084.67/297.20 , U81^#(mark(X1), X2, X3) -> c_142(U81^#(X1, X2, X3)) 1084.67/297.20 , U81^#(ok(X1), ok(X2), ok(X3)) -> c_143(U81^#(X1, X2, X3)) 1084.67/297.20 , U71^#(mark(X1), X2) -> c_138(U71^#(X1, X2)) 1084.67/297.20 , U71^#(ok(X1), ok(X2)) -> c_139(U71^#(X1, X2)) 1084.67/297.20 , x^#(X1, mark(X2)) -> c_95(x^#(X1, X2)) 1084.67/297.20 , x^#(mark(X1), X2) -> c_96(x^#(X1, X2)) 1084.67/297.20 , x^#(ok(X1), ok(X2)) -> c_97(x^#(X1, X2)) 1084.67/297.20 , U91^#(mark(X1), X2) -> c_152(U91^#(X1, X2)) 1084.67/297.20 , U91^#(ok(X1), ok(X2)) -> c_153(U91^#(X1, X2)) 1084.67/297.20 , U12^#(mark(X1), X2, X3) -> c_100(U12^#(X1, X2, X3)) 1084.67/297.20 , U12^#(ok(X1), ok(X2), ok(X3)) -> c_101(U12^#(X1, X2, X3)) 1084.67/297.20 , U13^#(mark(X1), X2, X3) -> c_102(U13^#(X1, X2, X3)) 1084.67/297.20 , U13^#(ok(X1), ok(X2), ok(X3)) -> c_103(U13^#(X1, X2, X3)) 1084.67/297.20 , U14^#(mark(X1), X2, X3) -> c_104(U14^#(X1, X2, X3)) 1084.67/297.20 , U14^#(ok(X1), ok(X2), ok(X3)) -> c_105(U14^#(X1, X2, X3)) 1084.67/297.20 , U15^#(mark(X1), X2) -> c_106(U15^#(X1, X2)) 1084.67/297.20 , U15^#(ok(X1), ok(X2)) -> c_107(U15^#(X1, X2)) 1084.67/297.20 , U16^#(mark(X)) -> c_108(U16^#(X)) 1084.67/297.20 , U16^#(ok(X)) -> c_109(U16^#(X)) 1084.67/297.20 , U22^#(mark(X1), X2) -> c_112(U22^#(X1, X2)) 1084.67/297.20 , U22^#(ok(X1), ok(X2)) -> c_113(U22^#(X1, X2)) 1084.67/297.20 , U23^#(mark(X)) -> c_114(U23^#(X)) 1084.67/297.20 , U23^#(ok(X)) -> c_115(U23^#(X)) 1084.67/297.20 , U32^#(mark(X1), X2, X3) -> c_118(U32^#(X1, X2, X3)) 1084.67/297.20 , U32^#(ok(X1), ok(X2), ok(X3)) -> c_119(U32^#(X1, X2, X3)) 1084.67/297.20 , U33^#(mark(X1), X2, X3) -> c_120(U33^#(X1, X2, X3)) 1084.67/297.20 , U33^#(ok(X1), ok(X2), ok(X3)) -> c_121(U33^#(X1, X2, X3)) 1084.67/297.20 , U34^#(mark(X1), X2, X3) -> c_122(U34^#(X1, X2, X3)) 1084.67/297.20 , U34^#(ok(X1), ok(X2), ok(X3)) -> c_123(U34^#(X1, X2, X3)) 1084.67/297.20 , U35^#(mark(X1), X2) -> c_124(U35^#(X1, X2)) 1084.67/297.20 , U35^#(ok(X1), ok(X2)) -> c_125(U35^#(X1, X2)) 1084.67/297.20 , U36^#(mark(X)) -> c_126(U36^#(X)) 1084.67/297.20 , U36^#(ok(X)) -> c_127(U36^#(X)) 1084.67/297.20 , U42^#(mark(X)) -> c_130(U42^#(X)) 1084.67/297.20 , U42^#(ok(X)) -> c_131(U42^#(X)) 1084.67/297.20 , U62^#(mark(X)) -> c_136(U62^#(X)) 1084.67/297.20 , U62^#(ok(X)) -> c_137(U62^#(X)) 1084.67/297.20 , U72^#(mark(X1), X2) -> c_140(U72^#(X1, X2)) 1084.67/297.20 , U72^#(ok(X1), ok(X2)) -> c_141(U72^#(X1, X2)) 1084.67/297.20 , U82^#(mark(X1), X2, X3) -> c_144(U82^#(X1, X2, X3)) 1084.67/297.20 , U82^#(ok(X1), ok(X2), ok(X3)) -> c_145(U82^#(X1, X2, X3)) 1084.67/297.20 , U83^#(mark(X1), X2, X3) -> c_146(U83^#(X1, X2, X3)) 1084.67/297.20 , U83^#(ok(X1), ok(X2), ok(X3)) -> c_147(U83^#(X1, X2, X3)) 1084.67/297.20 , U84^#(mark(X1), X2, X3) -> c_148(U84^#(X1, X2, X3)) 1084.67/297.20 , U84^#(ok(X1), ok(X2), ok(X3)) -> c_149(U84^#(X1, X2, X3)) 1084.67/297.20 , s^#(mark(X)) -> c_150(s^#(X)) 1084.67/297.20 , s^#(ok(X)) -> c_151(s^#(X)) 1084.67/297.20 , U92^#(mark(X)) -> c_154(U92^#(X)) 1084.67/297.20 , U92^#(ok(X)) -> c_155(U92^#(X)) 1084.67/297.20 , isNatKind^#(ok(X)) -> c_86(isNatKind^#(X)) 1084.67/297.20 , isNat^#(ok(X)) -> c_89(isNat^#(X)) 1084.67/297.20 , top^#(mark(X)) -> c_195(top^#(proper(X))) 1084.67/297.20 , top^#(ok(X)) -> c_196(top^#(active(X))) } 1084.67/297.20 Strict Trs: 1084.67/297.20 { active(U101(X1, X2, X3)) -> U101(active(X1), X2, X3) 1084.67/297.20 , active(U101(tt(), M, N)) -> mark(U102(isNatKind(M), M, N)) 1084.67/297.20 , active(U102(X1, X2, X3)) -> U102(active(X1), X2, X3) 1084.67/297.20 , active(U102(tt(), M, N)) -> mark(U103(isNat(N), M, N)) 1084.67/297.20 , active(isNatKind(plus(V1, V2))) -> mark(U41(isNatKind(V1), V2)) 1084.67/297.20 , active(isNatKind(x(V1, V2))) -> mark(U61(isNatKind(V1), V2)) 1084.67/297.20 , active(isNatKind(s(V1))) -> mark(U51(isNatKind(V1))) 1084.67/297.20 , active(isNatKind(0())) -> mark(tt()) 1084.67/297.20 , active(U103(X1, X2, X3)) -> U103(active(X1), X2, X3) 1084.67/297.20 , active(U103(tt(), M, N)) -> mark(U104(isNatKind(N), M, N)) 1084.67/297.20 , active(isNat(plus(V1, V2))) -> mark(U11(isNatKind(V1), V1, V2)) 1084.67/297.20 , active(isNat(x(V1, V2))) -> mark(U31(isNatKind(V1), V1, V2)) 1084.67/297.20 , active(isNat(s(V1))) -> mark(U21(isNatKind(V1), V1)) 1084.67/297.20 , active(isNat(0())) -> mark(tt()) 1084.67/297.20 , active(U104(X1, X2, X3)) -> U104(active(X1), X2, X3) 1084.67/297.20 , active(U104(tt(), M, N)) -> mark(plus(x(N, M), N)) 1084.67/297.20 , active(plus(X1, X2)) -> plus(X1, active(X2)) 1084.67/297.20 , active(plus(X1, X2)) -> plus(active(X1), X2) 1084.67/297.20 , active(plus(N, s(M))) -> mark(U81(isNat(M), M, N)) 1084.67/297.20 , active(plus(N, 0())) -> mark(U71(isNat(N), N)) 1084.67/297.20 , active(x(X1, X2)) -> x(X1, active(X2)) 1084.67/297.20 , active(x(X1, X2)) -> x(active(X1), X2) 1084.67/297.20 , active(x(N, s(M))) -> mark(U101(isNat(M), M, N)) 1084.67/297.20 , active(x(N, 0())) -> mark(U91(isNat(N), N)) 1084.67/297.20 , active(U11(X1, X2, X3)) -> U11(active(X1), X2, X3) 1084.67/297.20 , active(U11(tt(), V1, V2)) -> mark(U12(isNatKind(V1), V1, V2)) 1084.67/297.20 , active(U12(X1, X2, X3)) -> U12(active(X1), X2, X3) 1084.67/297.20 , active(U12(tt(), V1, V2)) -> mark(U13(isNatKind(V2), V1, V2)) 1084.67/297.20 , active(U13(X1, X2, X3)) -> U13(active(X1), X2, X3) 1084.67/297.20 , active(U13(tt(), V1, V2)) -> mark(U14(isNatKind(V2), V1, V2)) 1084.67/297.20 , active(U14(X1, X2, X3)) -> U14(active(X1), X2, X3) 1084.67/297.20 , active(U14(tt(), V1, V2)) -> mark(U15(isNat(V1), V2)) 1084.67/297.20 , active(U15(X1, X2)) -> U15(active(X1), X2) 1084.67/297.20 , active(U15(tt(), V2)) -> mark(U16(isNat(V2))) 1084.67/297.20 , active(U16(X)) -> U16(active(X)) 1084.67/297.20 , active(U16(tt())) -> mark(tt()) 1084.67/297.20 , active(U21(X1, X2)) -> U21(active(X1), X2) 1084.67/297.20 , active(U21(tt(), V1)) -> mark(U22(isNatKind(V1), V1)) 1084.67/297.20 , active(U22(X1, X2)) -> U22(active(X1), X2) 1084.67/297.20 , active(U22(tt(), V1)) -> mark(U23(isNat(V1))) 1084.67/297.20 , active(U23(X)) -> U23(active(X)) 1084.67/297.20 , active(U23(tt())) -> mark(tt()) 1084.67/297.20 , active(U31(X1, X2, X3)) -> U31(active(X1), X2, X3) 1084.67/297.20 , active(U31(tt(), V1, V2)) -> mark(U32(isNatKind(V1), V1, V2)) 1084.67/297.20 , active(U32(X1, X2, X3)) -> U32(active(X1), X2, X3) 1084.67/297.20 , active(U32(tt(), V1, V2)) -> mark(U33(isNatKind(V2), V1, V2)) 1084.67/297.20 , active(U33(X1, X2, X3)) -> U33(active(X1), X2, X3) 1084.67/297.20 , active(U33(tt(), V1, V2)) -> mark(U34(isNatKind(V2), V1, V2)) 1084.67/297.20 , active(U34(X1, X2, X3)) -> U34(active(X1), X2, X3) 1084.67/297.20 , active(U34(tt(), V1, V2)) -> mark(U35(isNat(V1), V2)) 1084.67/297.20 , active(U35(X1, X2)) -> U35(active(X1), X2) 1084.67/297.20 , active(U35(tt(), V2)) -> mark(U36(isNat(V2))) 1084.67/297.20 , active(U36(X)) -> U36(active(X)) 1084.67/297.20 , active(U36(tt())) -> mark(tt()) 1084.67/297.20 , active(U41(X1, X2)) -> U41(active(X1), X2) 1084.67/297.20 , active(U41(tt(), V2)) -> mark(U42(isNatKind(V2))) 1084.67/297.20 , active(U42(X)) -> U42(active(X)) 1084.67/297.20 , active(U42(tt())) -> mark(tt()) 1084.67/297.20 , active(U51(X)) -> U51(active(X)) 1084.67/297.20 , active(U51(tt())) -> mark(tt()) 1084.67/297.20 , active(U61(X1, X2)) -> U61(active(X1), X2) 1084.67/297.20 , active(U61(tt(), V2)) -> mark(U62(isNatKind(V2))) 1084.67/297.20 , active(U62(X)) -> U62(active(X)) 1084.67/297.20 , active(U62(tt())) -> mark(tt()) 1084.67/297.20 , active(U71(X1, X2)) -> U71(active(X1), X2) 1084.67/297.20 , active(U71(tt(), N)) -> mark(U72(isNatKind(N), N)) 1084.67/297.20 , active(U72(X1, X2)) -> U72(active(X1), X2) 1084.67/297.20 , active(U72(tt(), N)) -> mark(N) 1084.67/297.20 , active(U81(X1, X2, X3)) -> U81(active(X1), X2, X3) 1084.67/297.20 , active(U81(tt(), M, N)) -> mark(U82(isNatKind(M), M, N)) 1084.67/297.20 , active(U82(X1, X2, X3)) -> U82(active(X1), X2, X3) 1084.67/297.20 , active(U82(tt(), M, N)) -> mark(U83(isNat(N), M, N)) 1084.67/297.20 , active(U83(X1, X2, X3)) -> U83(active(X1), X2, X3) 1084.67/297.20 , active(U83(tt(), M, N)) -> mark(U84(isNatKind(N), M, N)) 1084.67/297.20 , active(U84(X1, X2, X3)) -> U84(active(X1), X2, X3) 1084.67/297.20 , active(U84(tt(), M, N)) -> mark(s(plus(N, M))) 1084.67/297.20 , active(s(X)) -> s(active(X)) 1084.67/297.20 , active(U91(X1, X2)) -> U91(active(X1), X2) 1084.67/297.20 , active(U91(tt(), N)) -> mark(U92(isNatKind(N))) 1084.67/297.20 , active(U92(X)) -> U92(active(X)) 1084.67/297.20 , active(U92(tt())) -> mark(0()) 1084.67/297.20 , U101(mark(X1), X2, X3) -> mark(U101(X1, X2, X3)) 1084.67/297.20 , U101(ok(X1), ok(X2), ok(X3)) -> ok(U101(X1, X2, X3)) 1084.67/297.20 , U102(mark(X1), X2, X3) -> mark(U102(X1, X2, X3)) 1084.67/297.20 , U102(ok(X1), ok(X2), ok(X3)) -> ok(U102(X1, X2, X3)) 1084.67/297.20 , isNatKind(ok(X)) -> ok(isNatKind(X)) 1084.67/297.20 , U103(mark(X1), X2, X3) -> mark(U103(X1, X2, X3)) 1084.67/297.20 , U103(ok(X1), ok(X2), ok(X3)) -> ok(U103(X1, X2, X3)) 1084.67/297.20 , isNat(ok(X)) -> ok(isNat(X)) 1084.67/297.20 , U104(mark(X1), X2, X3) -> mark(U104(X1, X2, X3)) 1084.67/297.20 , U104(ok(X1), ok(X2), ok(X3)) -> ok(U104(X1, X2, X3)) 1084.67/297.20 , plus(X1, mark(X2)) -> mark(plus(X1, X2)) 1084.67/297.20 , plus(mark(X1), X2) -> mark(plus(X1, X2)) 1084.67/297.20 , plus(ok(X1), ok(X2)) -> ok(plus(X1, X2)) 1084.67/297.20 , x(X1, mark(X2)) -> mark(x(X1, X2)) 1084.67/297.20 , x(mark(X1), X2) -> mark(x(X1, X2)) 1084.67/297.20 , x(ok(X1), ok(X2)) -> ok(x(X1, X2)) 1084.67/297.20 , U11(mark(X1), X2, X3) -> mark(U11(X1, X2, X3)) 1084.67/297.20 , U11(ok(X1), ok(X2), ok(X3)) -> ok(U11(X1, X2, X3)) 1084.67/297.20 , U12(mark(X1), X2, X3) -> mark(U12(X1, X2, X3)) 1084.67/297.20 , U12(ok(X1), ok(X2), ok(X3)) -> ok(U12(X1, X2, X3)) 1084.67/297.20 , U13(mark(X1), X2, X3) -> mark(U13(X1, X2, X3)) 1084.67/297.20 , U13(ok(X1), ok(X2), ok(X3)) -> ok(U13(X1, X2, X3)) 1084.67/297.20 , U14(mark(X1), X2, X3) -> mark(U14(X1, X2, X3)) 1084.67/297.20 , U14(ok(X1), ok(X2), ok(X3)) -> ok(U14(X1, X2, X3)) 1084.67/297.20 , U15(mark(X1), X2) -> mark(U15(X1, X2)) 1084.67/297.20 , U15(ok(X1), ok(X2)) -> ok(U15(X1, X2)) 1084.67/297.20 , U16(mark(X)) -> mark(U16(X)) 1084.67/297.20 , U16(ok(X)) -> ok(U16(X)) 1084.67/297.20 , U21(mark(X1), X2) -> mark(U21(X1, X2)) 1084.67/297.20 , U21(ok(X1), ok(X2)) -> ok(U21(X1, X2)) 1084.67/297.20 , U22(mark(X1), X2) -> mark(U22(X1, X2)) 1084.67/297.20 , U22(ok(X1), ok(X2)) -> ok(U22(X1, X2)) 1084.67/297.20 , U23(mark(X)) -> mark(U23(X)) 1084.67/297.20 , U23(ok(X)) -> ok(U23(X)) 1084.67/297.20 , U31(mark(X1), X2, X3) -> mark(U31(X1, X2, X3)) 1084.67/297.20 , U31(ok(X1), ok(X2), ok(X3)) -> ok(U31(X1, X2, X3)) 1084.67/297.20 , U32(mark(X1), X2, X3) -> mark(U32(X1, X2, X3)) 1084.67/297.20 , U32(ok(X1), ok(X2), ok(X3)) -> ok(U32(X1, X2, X3)) 1084.67/297.20 , U33(mark(X1), X2, X3) -> mark(U33(X1, X2, X3)) 1084.67/297.20 , U33(ok(X1), ok(X2), ok(X3)) -> ok(U33(X1, X2, X3)) 1084.67/297.20 , U34(mark(X1), X2, X3) -> mark(U34(X1, X2, X3)) 1084.67/297.20 , U34(ok(X1), ok(X2), ok(X3)) -> ok(U34(X1, X2, X3)) 1084.67/297.20 , U35(mark(X1), X2) -> mark(U35(X1, X2)) 1084.67/297.20 , U35(ok(X1), ok(X2)) -> ok(U35(X1, X2)) 1084.67/297.20 , U36(mark(X)) -> mark(U36(X)) 1084.67/297.20 , U36(ok(X)) -> ok(U36(X)) 1084.67/297.20 , U41(mark(X1), X2) -> mark(U41(X1, X2)) 1084.67/297.20 , U41(ok(X1), ok(X2)) -> ok(U41(X1, X2)) 1084.67/297.20 , U42(mark(X)) -> mark(U42(X)) 1084.67/297.20 , U42(ok(X)) -> ok(U42(X)) 1084.67/297.20 , U51(mark(X)) -> mark(U51(X)) 1084.67/297.20 , U51(ok(X)) -> ok(U51(X)) 1084.67/297.20 , U61(mark(X1), X2) -> mark(U61(X1, X2)) 1084.67/297.20 , U61(ok(X1), ok(X2)) -> ok(U61(X1, X2)) 1084.67/297.20 , U62(mark(X)) -> mark(U62(X)) 1084.67/297.20 , U62(ok(X)) -> ok(U62(X)) 1084.67/297.20 , U71(mark(X1), X2) -> mark(U71(X1, X2)) 1084.67/297.20 , U71(ok(X1), ok(X2)) -> ok(U71(X1, X2)) 1084.67/297.20 , U72(mark(X1), X2) -> mark(U72(X1, X2)) 1084.67/297.20 , U72(ok(X1), ok(X2)) -> ok(U72(X1, X2)) 1084.67/297.20 , U81(mark(X1), X2, X3) -> mark(U81(X1, X2, X3)) 1084.67/297.20 , U81(ok(X1), ok(X2), ok(X3)) -> ok(U81(X1, X2, X3)) 1084.67/297.20 , U82(mark(X1), X2, X3) -> mark(U82(X1, X2, X3)) 1084.67/297.20 , U82(ok(X1), ok(X2), ok(X3)) -> ok(U82(X1, X2, X3)) 1084.67/297.20 , U83(mark(X1), X2, X3) -> mark(U83(X1, X2, X3)) 1084.67/297.20 , U83(ok(X1), ok(X2), ok(X3)) -> ok(U83(X1, X2, X3)) 1084.67/297.20 , U84(mark(X1), X2, X3) -> mark(U84(X1, X2, X3)) 1084.67/297.20 , U84(ok(X1), ok(X2), ok(X3)) -> ok(U84(X1, X2, X3)) 1084.67/297.20 , s(mark(X)) -> mark(s(X)) 1084.67/297.20 , s(ok(X)) -> ok(s(X)) 1084.67/297.20 , U91(mark(X1), X2) -> mark(U91(X1, X2)) 1084.67/297.20 , U91(ok(X1), ok(X2)) -> ok(U91(X1, X2)) 1084.67/297.20 , U92(mark(X)) -> mark(U92(X)) 1084.67/297.20 , U92(ok(X)) -> ok(U92(X)) 1084.67/297.20 , proper(U101(X1, X2, X3)) -> 1084.67/297.20 U101(proper(X1), proper(X2), proper(X3)) 1084.67/297.20 , proper(tt()) -> ok(tt()) 1084.67/297.20 , proper(U102(X1, X2, X3)) -> 1084.67/297.20 U102(proper(X1), proper(X2), proper(X3)) 1084.67/297.20 , proper(isNatKind(X)) -> isNatKind(proper(X)) 1084.67/297.20 , proper(U103(X1, X2, X3)) -> 1084.67/297.20 U103(proper(X1), proper(X2), proper(X3)) 1084.67/297.20 , proper(isNat(X)) -> isNat(proper(X)) 1084.67/297.20 , proper(U104(X1, X2, X3)) -> 1084.67/297.20 U104(proper(X1), proper(X2), proper(X3)) 1084.67/297.20 , proper(plus(X1, X2)) -> plus(proper(X1), proper(X2)) 1084.67/297.20 , proper(x(X1, X2)) -> x(proper(X1), proper(X2)) 1084.67/297.20 , proper(U11(X1, X2, X3)) -> 1084.67/297.20 U11(proper(X1), proper(X2), proper(X3)) 1084.67/297.20 , proper(U12(X1, X2, X3)) -> 1084.67/297.20 U12(proper(X1), proper(X2), proper(X3)) 1084.67/297.20 , proper(U13(X1, X2, X3)) -> 1084.67/297.20 U13(proper(X1), proper(X2), proper(X3)) 1084.67/297.20 , proper(U14(X1, X2, X3)) -> 1084.67/297.20 U14(proper(X1), proper(X2), proper(X3)) 1084.67/297.20 , proper(U15(X1, X2)) -> U15(proper(X1), proper(X2)) 1084.67/297.20 , proper(U16(X)) -> U16(proper(X)) 1084.67/297.20 , proper(U21(X1, X2)) -> U21(proper(X1), proper(X2)) 1084.67/297.20 , proper(U22(X1, X2)) -> U22(proper(X1), proper(X2)) 1084.67/297.20 , proper(U23(X)) -> U23(proper(X)) 1084.67/297.20 , proper(U31(X1, X2, X3)) -> 1084.67/297.20 U31(proper(X1), proper(X2), proper(X3)) 1084.67/297.20 , proper(U32(X1, X2, X3)) -> 1084.67/297.20 U32(proper(X1), proper(X2), proper(X3)) 1084.67/297.20 , proper(U33(X1, X2, X3)) -> 1084.67/297.20 U33(proper(X1), proper(X2), proper(X3)) 1084.67/297.20 , proper(U34(X1, X2, X3)) -> 1084.67/297.20 U34(proper(X1), proper(X2), proper(X3)) 1084.67/297.20 , proper(U35(X1, X2)) -> U35(proper(X1), proper(X2)) 1084.67/297.20 , proper(U36(X)) -> U36(proper(X)) 1084.67/297.20 , proper(U41(X1, X2)) -> U41(proper(X1), proper(X2)) 1084.67/297.20 , proper(U42(X)) -> U42(proper(X)) 1084.67/297.20 , proper(U51(X)) -> U51(proper(X)) 1084.67/297.20 , proper(U61(X1, X2)) -> U61(proper(X1), proper(X2)) 1084.67/297.20 , proper(U62(X)) -> U62(proper(X)) 1084.67/297.20 , proper(U71(X1, X2)) -> U71(proper(X1), proper(X2)) 1084.67/297.20 , proper(U72(X1, X2)) -> U72(proper(X1), proper(X2)) 1084.67/297.20 , proper(U81(X1, X2, X3)) -> 1084.67/297.20 U81(proper(X1), proper(X2), proper(X3)) 1084.67/297.20 , proper(U82(X1, X2, X3)) -> 1084.67/297.20 U82(proper(X1), proper(X2), proper(X3)) 1084.67/297.20 , proper(U83(X1, X2, X3)) -> 1084.67/297.20 U83(proper(X1), proper(X2), proper(X3)) 1084.67/297.20 , proper(U84(X1, X2, X3)) -> 1084.67/297.20 U84(proper(X1), proper(X2), proper(X3)) 1084.67/297.20 , proper(s(X)) -> s(proper(X)) 1084.67/297.20 , proper(U91(X1, X2)) -> U91(proper(X1), proper(X2)) 1084.67/297.20 , proper(U92(X)) -> U92(proper(X)) 1084.67/297.20 , proper(0()) -> ok(0()) 1084.67/297.20 , top(mark(X)) -> top(proper(X)) 1084.67/297.20 , top(ok(X)) -> top(active(X)) } 1084.67/297.20 Weak DPs: 1084.67/297.20 { proper^#(tt()) -> c_157() 1084.67/297.20 , proper^#(0()) -> c_194() } 1084.67/297.20 Obligation: 1084.67/297.20 runtime complexity 1084.67/297.20 Answer: 1084.67/297.20 MAYBE 1084.67/297.20 1084.67/297.20 Empty strict component of the problem is NOT empty. 1084.67/297.20 1084.67/297.20 1084.67/297.20 Arrrr.. 1084.78/297.35 EOF