MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { active(U11(X1, X2, X3)) -> U11(active(X1), X2, X3) , active(U11(tt(), V1, V2)) -> mark(U12(isNat(V1), V2)) , active(U12(X1, X2)) -> U12(active(X1), X2) , active(U12(tt(), V2)) -> mark(U13(isNat(V2))) , active(isNat(s(V1))) -> mark(U21(isNatKind(V1), V1)) , active(isNat(plus(V1, V2))) -> mark(U11(and(isNatKind(V1), isNatKind(V2)), V1, V2)) , active(isNat(0())) -> mark(tt()) , active(isNat(x(V1, V2))) -> mark(U31(and(isNatKind(V1), isNatKind(V2)), V1, V2)) , active(U13(X)) -> U13(active(X)) , active(U13(tt())) -> mark(tt()) , active(U21(X1, X2)) -> U21(active(X1), X2) , active(U21(tt(), V1)) -> mark(U22(isNat(V1))) , active(U22(X)) -> U22(active(X)) , active(U22(tt())) -> mark(tt()) , active(U31(X1, X2, X3)) -> U31(active(X1), X2, X3) , active(U31(tt(), V1, V2)) -> mark(U32(isNat(V1), V2)) , active(U32(X1, X2)) -> U32(active(X1), X2) , active(U32(tt(), V2)) -> mark(U33(isNat(V2))) , active(U33(X)) -> U33(active(X)) , active(U33(tt())) -> mark(tt()) , active(U41(X1, X2)) -> U41(active(X1), X2) , active(U41(tt(), N)) -> mark(N) , active(U51(X1, X2, X3)) -> U51(active(X1), X2, X3) , active(U51(tt(), M, N)) -> mark(s(plus(N, M))) , active(s(X)) -> s(active(X)) , active(plus(X1, X2)) -> plus(X1, active(X2)) , active(plus(X1, X2)) -> plus(active(X1), X2) , active(plus(N, s(M))) -> mark(U51(and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)) , active(plus(N, 0())) -> mark(U41(and(isNat(N), isNatKind(N)), N)) , active(U61(X)) -> U61(active(X)) , active(U61(tt())) -> mark(0()) , active(U71(X1, X2, X3)) -> U71(active(X1), X2, X3) , active(U71(tt(), M, N)) -> mark(plus(x(N, M), N)) , active(x(X1, X2)) -> x(X1, active(X2)) , active(x(X1, X2)) -> x(active(X1), X2) , active(x(N, s(M))) -> mark(U71(and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)) , active(x(N, 0())) -> mark(U61(and(isNat(N), isNatKind(N)))) , active(and(X1, X2)) -> and(active(X1), X2) , active(and(tt(), X)) -> mark(X) , active(isNatKind(s(V1))) -> mark(isNatKind(V1)) , active(isNatKind(plus(V1, V2))) -> mark(and(isNatKind(V1), isNatKind(V2))) , active(isNatKind(0())) -> mark(tt()) , active(isNatKind(x(V1, V2))) -> mark(and(isNatKind(V1), isNatKind(V2))) , U11(mark(X1), X2, X3) -> mark(U11(X1, X2, X3)) , U11(ok(X1), ok(X2), ok(X3)) -> ok(U11(X1, X2, X3)) , U12(mark(X1), X2) -> mark(U12(X1, X2)) , U12(ok(X1), ok(X2)) -> ok(U12(X1, X2)) , isNat(ok(X)) -> ok(isNat(X)) , U13(mark(X)) -> mark(U13(X)) , U13(ok(X)) -> ok(U13(X)) , U21(mark(X1), X2) -> mark(U21(X1, X2)) , U21(ok(X1), ok(X2)) -> ok(U21(X1, X2)) , U22(mark(X)) -> mark(U22(X)) , U22(ok(X)) -> ok(U22(X)) , U31(mark(X1), X2, X3) -> mark(U31(X1, X2, X3)) , U31(ok(X1), ok(X2), ok(X3)) -> ok(U31(X1, X2, X3)) , U32(mark(X1), X2) -> mark(U32(X1, X2)) , U32(ok(X1), ok(X2)) -> ok(U32(X1, X2)) , U33(mark(X)) -> mark(U33(X)) , U33(ok(X)) -> ok(U33(X)) , U41(mark(X1), X2) -> mark(U41(X1, X2)) , U41(ok(X1), ok(X2)) -> ok(U41(X1, X2)) , U51(mark(X1), X2, X3) -> mark(U51(X1, X2, X3)) , U51(ok(X1), ok(X2), ok(X3)) -> ok(U51(X1, X2, X3)) , s(mark(X)) -> mark(s(X)) , s(ok(X)) -> ok(s(X)) , plus(X1, mark(X2)) -> mark(plus(X1, X2)) , plus(mark(X1), X2) -> mark(plus(X1, X2)) , plus(ok(X1), ok(X2)) -> ok(plus(X1, X2)) , U61(mark(X)) -> mark(U61(X)) , U61(ok(X)) -> ok(U61(X)) , U71(mark(X1), X2, X3) -> mark(U71(X1, X2, X3)) , U71(ok(X1), ok(X2), ok(X3)) -> ok(U71(X1, X2, X3)) , x(X1, mark(X2)) -> mark(x(X1, X2)) , x(mark(X1), X2) -> mark(x(X1, X2)) , x(ok(X1), ok(X2)) -> ok(x(X1, X2)) , and(mark(X1), X2) -> mark(and(X1, X2)) , and(ok(X1), ok(X2)) -> ok(and(X1, X2)) , isNatKind(ok(X)) -> ok(isNatKind(X)) , proper(U11(X1, X2, X3)) -> U11(proper(X1), proper(X2), proper(X3)) , proper(tt()) -> ok(tt()) , proper(U12(X1, X2)) -> U12(proper(X1), proper(X2)) , proper(isNat(X)) -> isNat(proper(X)) , proper(U13(X)) -> U13(proper(X)) , proper(U21(X1, X2)) -> U21(proper(X1), proper(X2)) , proper(U22(X)) -> U22(proper(X)) , proper(U31(X1, X2, X3)) -> U31(proper(X1), proper(X2), proper(X3)) , proper(U32(X1, X2)) -> U32(proper(X1), proper(X2)) , proper(U33(X)) -> U33(proper(X)) , proper(U41(X1, X2)) -> U41(proper(X1), proper(X2)) , proper(U51(X1, X2, X3)) -> U51(proper(X1), proper(X2), proper(X3)) , proper(s(X)) -> s(proper(X)) , proper(plus(X1, X2)) -> plus(proper(X1), proper(X2)) , proper(U61(X)) -> U61(proper(X)) , proper(0()) -> ok(0()) , proper(U71(X1, X2, X3)) -> U71(proper(X1), proper(X2), proper(X3)) , proper(x(X1, X2)) -> x(proper(X1), proper(X2)) , proper(and(X1, X2)) -> and(proper(X1), proper(X2)) , proper(isNatKind(X)) -> isNatKind(proper(X)) , top(mark(X)) -> top(proper(X)) , top(ok(X)) -> top(active(X)) } Obligation: runtime complexity Answer: MAYBE None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem (timeout of 60 seconds)' failed due to the following reason: Computation stopped due to timeout after 60.0 seconds. 2) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem (timeout of 30 seconds) (timeout of 60 seconds)' failed due to the following reason: Computation stopped due to timeout after 30.0 seconds. 2) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'bsearch-popstar (timeout of 60 seconds)' failed due to the following reason: The processor is inapplicable, reason: Processor only applicable for innermost runtime complexity analysis 2) 'Polynomial Path Order (PS) (timeout of 60 seconds)' failed due to the following reason: The processor is inapplicable, reason: Processor only applicable for innermost runtime complexity analysis 3) 'Fastest (timeout of 5 seconds) (timeout of 60 seconds)' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'Bounds with minimal-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 3) 'Innermost Weak Dependency Pairs (timeout of 60 seconds)' failed due to the following reason: We add the following weak dependency pairs: Strict DPs: { active^#(U11(X1, X2, X3)) -> c_1(U11^#(active(X1), X2, X3)) , active^#(U11(tt(), V1, V2)) -> c_2(U12^#(isNat(V1), V2)) , active^#(U12(X1, X2)) -> c_3(U12^#(active(X1), X2)) , active^#(U12(tt(), V2)) -> c_4(U13^#(isNat(V2))) , active^#(isNat(s(V1))) -> c_5(U21^#(isNatKind(V1), V1)) , active^#(isNat(plus(V1, V2))) -> c_6(U11^#(and(isNatKind(V1), isNatKind(V2)), V1, V2)) , active^#(isNat(0())) -> c_7() , active^#(isNat(x(V1, V2))) -> c_8(U31^#(and(isNatKind(V1), isNatKind(V2)), V1, V2)) , active^#(U13(X)) -> c_9(U13^#(active(X))) , active^#(U13(tt())) -> c_10() , active^#(U21(X1, X2)) -> c_11(U21^#(active(X1), X2)) , active^#(U21(tt(), V1)) -> c_12(U22^#(isNat(V1))) , active^#(U22(X)) -> c_13(U22^#(active(X))) , active^#(U22(tt())) -> c_14() , active^#(U31(X1, X2, X3)) -> c_15(U31^#(active(X1), X2, X3)) , active^#(U31(tt(), V1, V2)) -> c_16(U32^#(isNat(V1), V2)) , active^#(U32(X1, X2)) -> c_17(U32^#(active(X1), X2)) , active^#(U32(tt(), V2)) -> c_18(U33^#(isNat(V2))) , active^#(U33(X)) -> c_19(U33^#(active(X))) , active^#(U33(tt())) -> c_20() , active^#(U41(X1, X2)) -> c_21(U41^#(active(X1), X2)) , active^#(U41(tt(), N)) -> c_22(N) , active^#(U51(X1, X2, X3)) -> c_23(U51^#(active(X1), X2, X3)) , active^#(U51(tt(), M, N)) -> c_24(s^#(plus(N, M))) , active^#(s(X)) -> c_25(s^#(active(X))) , active^#(plus(X1, X2)) -> c_26(plus^#(X1, active(X2))) , active^#(plus(X1, X2)) -> c_27(plus^#(active(X1), X2)) , active^#(plus(N, s(M))) -> c_28(U51^#(and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)) , active^#(plus(N, 0())) -> c_29(U41^#(and(isNat(N), isNatKind(N)), N)) , active^#(U61(X)) -> c_30(U61^#(active(X))) , active^#(U61(tt())) -> c_31() , active^#(U71(X1, X2, X3)) -> c_32(U71^#(active(X1), X2, X3)) , active^#(U71(tt(), M, N)) -> c_33(plus^#(x(N, M), N)) , active^#(x(X1, X2)) -> c_34(x^#(X1, active(X2))) , active^#(x(X1, X2)) -> c_35(x^#(active(X1), X2)) , active^#(x(N, s(M))) -> c_36(U71^#(and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)) , active^#(x(N, 0())) -> c_37(U61^#(and(isNat(N), isNatKind(N)))) , active^#(and(X1, X2)) -> c_38(and^#(active(X1), X2)) , active^#(and(tt(), X)) -> c_39(X) , active^#(isNatKind(s(V1))) -> c_40(isNatKind^#(V1)) , active^#(isNatKind(plus(V1, V2))) -> c_41(and^#(isNatKind(V1), isNatKind(V2))) , active^#(isNatKind(0())) -> c_42() , active^#(isNatKind(x(V1, V2))) -> c_43(and^#(isNatKind(V1), isNatKind(V2))) , U11^#(mark(X1), X2, X3) -> c_44(U11^#(X1, X2, X3)) , U11^#(ok(X1), ok(X2), ok(X3)) -> c_45(U11^#(X1, X2, X3)) , U12^#(mark(X1), X2) -> c_46(U12^#(X1, X2)) , U12^#(ok(X1), ok(X2)) -> c_47(U12^#(X1, X2)) , U13^#(mark(X)) -> c_49(U13^#(X)) , U13^#(ok(X)) -> c_50(U13^#(X)) , U21^#(mark(X1), X2) -> c_51(U21^#(X1, X2)) , U21^#(ok(X1), ok(X2)) -> c_52(U21^#(X1, X2)) , U31^#(mark(X1), X2, X3) -> c_55(U31^#(X1, X2, X3)) , U31^#(ok(X1), ok(X2), ok(X3)) -> c_56(U31^#(X1, X2, X3)) , U22^#(mark(X)) -> c_53(U22^#(X)) , U22^#(ok(X)) -> c_54(U22^#(X)) , U32^#(mark(X1), X2) -> c_57(U32^#(X1, X2)) , U32^#(ok(X1), ok(X2)) -> c_58(U32^#(X1, X2)) , U33^#(mark(X)) -> c_59(U33^#(X)) , U33^#(ok(X)) -> c_60(U33^#(X)) , U41^#(mark(X1), X2) -> c_61(U41^#(X1, X2)) , U41^#(ok(X1), ok(X2)) -> c_62(U41^#(X1, X2)) , U51^#(mark(X1), X2, X3) -> c_63(U51^#(X1, X2, X3)) , U51^#(ok(X1), ok(X2), ok(X3)) -> c_64(U51^#(X1, X2, X3)) , s^#(mark(X)) -> c_65(s^#(X)) , s^#(ok(X)) -> c_66(s^#(X)) , plus^#(X1, mark(X2)) -> c_67(plus^#(X1, X2)) , plus^#(mark(X1), X2) -> c_68(plus^#(X1, X2)) , plus^#(ok(X1), ok(X2)) -> c_69(plus^#(X1, X2)) , U61^#(mark(X)) -> c_70(U61^#(X)) , U61^#(ok(X)) -> c_71(U61^#(X)) , U71^#(mark(X1), X2, X3) -> c_72(U71^#(X1, X2, X3)) , U71^#(ok(X1), ok(X2), ok(X3)) -> c_73(U71^#(X1, X2, X3)) , x^#(X1, mark(X2)) -> c_74(x^#(X1, X2)) , x^#(mark(X1), X2) -> c_75(x^#(X1, X2)) , x^#(ok(X1), ok(X2)) -> c_76(x^#(X1, X2)) , and^#(mark(X1), X2) -> c_77(and^#(X1, X2)) , and^#(ok(X1), ok(X2)) -> c_78(and^#(X1, X2)) , isNatKind^#(ok(X)) -> c_79(isNatKind^#(X)) , isNat^#(ok(X)) -> c_48(isNat^#(X)) , proper^#(U11(X1, X2, X3)) -> c_80(U11^#(proper(X1), proper(X2), proper(X3))) , proper^#(tt()) -> c_81() , proper^#(U12(X1, X2)) -> c_82(U12^#(proper(X1), proper(X2))) , proper^#(isNat(X)) -> c_83(isNat^#(proper(X))) , proper^#(U13(X)) -> c_84(U13^#(proper(X))) , proper^#(U21(X1, X2)) -> c_85(U21^#(proper(X1), proper(X2))) , proper^#(U22(X)) -> c_86(U22^#(proper(X))) , proper^#(U31(X1, X2, X3)) -> c_87(U31^#(proper(X1), proper(X2), proper(X3))) , proper^#(U32(X1, X2)) -> c_88(U32^#(proper(X1), proper(X2))) , proper^#(U33(X)) -> c_89(U33^#(proper(X))) , proper^#(U41(X1, X2)) -> c_90(U41^#(proper(X1), proper(X2))) , proper^#(U51(X1, X2, X3)) -> c_91(U51^#(proper(X1), proper(X2), proper(X3))) , proper^#(s(X)) -> c_92(s^#(proper(X))) , proper^#(plus(X1, X2)) -> c_93(plus^#(proper(X1), proper(X2))) , proper^#(U61(X)) -> c_94(U61^#(proper(X))) , proper^#(0()) -> c_95() , proper^#(U71(X1, X2, X3)) -> c_96(U71^#(proper(X1), proper(X2), proper(X3))) , proper^#(x(X1, X2)) -> c_97(x^#(proper(X1), proper(X2))) , proper^#(and(X1, X2)) -> c_98(and^#(proper(X1), proper(X2))) , proper^#(isNatKind(X)) -> c_99(isNatKind^#(proper(X))) , top^#(mark(X)) -> c_100(top^#(proper(X))) , top^#(ok(X)) -> c_101(top^#(active(X))) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { active^#(U11(X1, X2, X3)) -> c_1(U11^#(active(X1), X2, X3)) , active^#(U11(tt(), V1, V2)) -> c_2(U12^#(isNat(V1), V2)) , active^#(U12(X1, X2)) -> c_3(U12^#(active(X1), X2)) , active^#(U12(tt(), V2)) -> c_4(U13^#(isNat(V2))) , active^#(isNat(s(V1))) -> c_5(U21^#(isNatKind(V1), V1)) , active^#(isNat(plus(V1, V2))) -> c_6(U11^#(and(isNatKind(V1), isNatKind(V2)), V1, V2)) , active^#(isNat(0())) -> c_7() , active^#(isNat(x(V1, V2))) -> c_8(U31^#(and(isNatKind(V1), isNatKind(V2)), V1, V2)) , active^#(U13(X)) -> c_9(U13^#(active(X))) , active^#(U13(tt())) -> c_10() , active^#(U21(X1, X2)) -> c_11(U21^#(active(X1), X2)) , active^#(U21(tt(), V1)) -> c_12(U22^#(isNat(V1))) , active^#(U22(X)) -> c_13(U22^#(active(X))) , active^#(U22(tt())) -> c_14() , active^#(U31(X1, X2, X3)) -> c_15(U31^#(active(X1), X2, X3)) , active^#(U31(tt(), V1, V2)) -> c_16(U32^#(isNat(V1), V2)) , active^#(U32(X1, X2)) -> c_17(U32^#(active(X1), X2)) , active^#(U32(tt(), V2)) -> c_18(U33^#(isNat(V2))) , active^#(U33(X)) -> c_19(U33^#(active(X))) , active^#(U33(tt())) -> c_20() , active^#(U41(X1, X2)) -> c_21(U41^#(active(X1), X2)) , active^#(U41(tt(), N)) -> c_22(N) , active^#(U51(X1, X2, X3)) -> c_23(U51^#(active(X1), X2, X3)) , active^#(U51(tt(), M, N)) -> c_24(s^#(plus(N, M))) , active^#(s(X)) -> c_25(s^#(active(X))) , active^#(plus(X1, X2)) -> c_26(plus^#(X1, active(X2))) , active^#(plus(X1, X2)) -> c_27(plus^#(active(X1), X2)) , active^#(plus(N, s(M))) -> c_28(U51^#(and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)) , active^#(plus(N, 0())) -> c_29(U41^#(and(isNat(N), isNatKind(N)), N)) , active^#(U61(X)) -> c_30(U61^#(active(X))) , active^#(U61(tt())) -> c_31() , active^#(U71(X1, X2, X3)) -> c_32(U71^#(active(X1), X2, X3)) , active^#(U71(tt(), M, N)) -> c_33(plus^#(x(N, M), N)) , active^#(x(X1, X2)) -> c_34(x^#(X1, active(X2))) , active^#(x(X1, X2)) -> c_35(x^#(active(X1), X2)) , active^#(x(N, s(M))) -> c_36(U71^#(and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)) , active^#(x(N, 0())) -> c_37(U61^#(and(isNat(N), isNatKind(N)))) , active^#(and(X1, X2)) -> c_38(and^#(active(X1), X2)) , active^#(and(tt(), X)) -> c_39(X) , active^#(isNatKind(s(V1))) -> c_40(isNatKind^#(V1)) , active^#(isNatKind(plus(V1, V2))) -> c_41(and^#(isNatKind(V1), isNatKind(V2))) , active^#(isNatKind(0())) -> c_42() , active^#(isNatKind(x(V1, V2))) -> c_43(and^#(isNatKind(V1), isNatKind(V2))) , U11^#(mark(X1), X2, X3) -> c_44(U11^#(X1, X2, X3)) , U11^#(ok(X1), ok(X2), ok(X3)) -> c_45(U11^#(X1, X2, X3)) , U12^#(mark(X1), X2) -> c_46(U12^#(X1, X2)) , U12^#(ok(X1), ok(X2)) -> c_47(U12^#(X1, X2)) , U13^#(mark(X)) -> c_49(U13^#(X)) , U13^#(ok(X)) -> c_50(U13^#(X)) , U21^#(mark(X1), X2) -> c_51(U21^#(X1, X2)) , U21^#(ok(X1), ok(X2)) -> c_52(U21^#(X1, X2)) , U31^#(mark(X1), X2, X3) -> c_55(U31^#(X1, X2, X3)) , U31^#(ok(X1), ok(X2), ok(X3)) -> c_56(U31^#(X1, X2, X3)) , U22^#(mark(X)) -> c_53(U22^#(X)) , U22^#(ok(X)) -> c_54(U22^#(X)) , U32^#(mark(X1), X2) -> c_57(U32^#(X1, X2)) , U32^#(ok(X1), ok(X2)) -> c_58(U32^#(X1, X2)) , U33^#(mark(X)) -> c_59(U33^#(X)) , U33^#(ok(X)) -> c_60(U33^#(X)) , U41^#(mark(X1), X2) -> c_61(U41^#(X1, X2)) , U41^#(ok(X1), ok(X2)) -> c_62(U41^#(X1, X2)) , U51^#(mark(X1), X2, X3) -> c_63(U51^#(X1, X2, X3)) , U51^#(ok(X1), ok(X2), ok(X3)) -> c_64(U51^#(X1, X2, X3)) , s^#(mark(X)) -> c_65(s^#(X)) , s^#(ok(X)) -> c_66(s^#(X)) , plus^#(X1, mark(X2)) -> c_67(plus^#(X1, X2)) , plus^#(mark(X1), X2) -> c_68(plus^#(X1, X2)) , plus^#(ok(X1), ok(X2)) -> c_69(plus^#(X1, X2)) , U61^#(mark(X)) -> c_70(U61^#(X)) , U61^#(ok(X)) -> c_71(U61^#(X)) , U71^#(mark(X1), X2, X3) -> c_72(U71^#(X1, X2, X3)) , U71^#(ok(X1), ok(X2), ok(X3)) -> c_73(U71^#(X1, X2, X3)) , x^#(X1, mark(X2)) -> c_74(x^#(X1, X2)) , x^#(mark(X1), X2) -> c_75(x^#(X1, X2)) , x^#(ok(X1), ok(X2)) -> c_76(x^#(X1, X2)) , and^#(mark(X1), X2) -> c_77(and^#(X1, X2)) , and^#(ok(X1), ok(X2)) -> c_78(and^#(X1, X2)) , isNatKind^#(ok(X)) -> c_79(isNatKind^#(X)) , isNat^#(ok(X)) -> c_48(isNat^#(X)) , proper^#(U11(X1, X2, X3)) -> c_80(U11^#(proper(X1), proper(X2), proper(X3))) , proper^#(tt()) -> c_81() , proper^#(U12(X1, X2)) -> c_82(U12^#(proper(X1), proper(X2))) , proper^#(isNat(X)) -> c_83(isNat^#(proper(X))) , proper^#(U13(X)) -> c_84(U13^#(proper(X))) , proper^#(U21(X1, X2)) -> c_85(U21^#(proper(X1), proper(X2))) , proper^#(U22(X)) -> c_86(U22^#(proper(X))) , proper^#(U31(X1, X2, X3)) -> c_87(U31^#(proper(X1), proper(X2), proper(X3))) , proper^#(U32(X1, X2)) -> c_88(U32^#(proper(X1), proper(X2))) , proper^#(U33(X)) -> c_89(U33^#(proper(X))) , proper^#(U41(X1, X2)) -> c_90(U41^#(proper(X1), proper(X2))) , proper^#(U51(X1, X2, X3)) -> c_91(U51^#(proper(X1), proper(X2), proper(X3))) , proper^#(s(X)) -> c_92(s^#(proper(X))) , proper^#(plus(X1, X2)) -> c_93(plus^#(proper(X1), proper(X2))) , proper^#(U61(X)) -> c_94(U61^#(proper(X))) , proper^#(0()) -> c_95() , proper^#(U71(X1, X2, X3)) -> c_96(U71^#(proper(X1), proper(X2), proper(X3))) , proper^#(x(X1, X2)) -> c_97(x^#(proper(X1), proper(X2))) , proper^#(and(X1, X2)) -> c_98(and^#(proper(X1), proper(X2))) , proper^#(isNatKind(X)) -> c_99(isNatKind^#(proper(X))) , top^#(mark(X)) -> c_100(top^#(proper(X))) , top^#(ok(X)) -> c_101(top^#(active(X))) } Strict Trs: { active(U11(X1, X2, X3)) -> U11(active(X1), X2, X3) , active(U11(tt(), V1, V2)) -> mark(U12(isNat(V1), V2)) , active(U12(X1, X2)) -> U12(active(X1), X2) , active(U12(tt(), V2)) -> mark(U13(isNat(V2))) , active(isNat(s(V1))) -> mark(U21(isNatKind(V1), V1)) , active(isNat(plus(V1, V2))) -> mark(U11(and(isNatKind(V1), isNatKind(V2)), V1, V2)) , active(isNat(0())) -> mark(tt()) , active(isNat(x(V1, V2))) -> mark(U31(and(isNatKind(V1), isNatKind(V2)), V1, V2)) , active(U13(X)) -> U13(active(X)) , active(U13(tt())) -> mark(tt()) , active(U21(X1, X2)) -> U21(active(X1), X2) , active(U21(tt(), V1)) -> mark(U22(isNat(V1))) , active(U22(X)) -> U22(active(X)) , active(U22(tt())) -> mark(tt()) , active(U31(X1, X2, X3)) -> U31(active(X1), X2, X3) , active(U31(tt(), V1, V2)) -> mark(U32(isNat(V1), V2)) , active(U32(X1, X2)) -> U32(active(X1), X2) , active(U32(tt(), V2)) -> mark(U33(isNat(V2))) , active(U33(X)) -> U33(active(X)) , active(U33(tt())) -> mark(tt()) , active(U41(X1, X2)) -> U41(active(X1), X2) , active(U41(tt(), N)) -> mark(N) , active(U51(X1, X2, X3)) -> U51(active(X1), X2, X3) , active(U51(tt(), M, N)) -> mark(s(plus(N, M))) , active(s(X)) -> s(active(X)) , active(plus(X1, X2)) -> plus(X1, active(X2)) , active(plus(X1, X2)) -> plus(active(X1), X2) , active(plus(N, s(M))) -> mark(U51(and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)) , active(plus(N, 0())) -> mark(U41(and(isNat(N), isNatKind(N)), N)) , active(U61(X)) -> U61(active(X)) , active(U61(tt())) -> mark(0()) , active(U71(X1, X2, X3)) -> U71(active(X1), X2, X3) , active(U71(tt(), M, N)) -> mark(plus(x(N, M), N)) , active(x(X1, X2)) -> x(X1, active(X2)) , active(x(X1, X2)) -> x(active(X1), X2) , active(x(N, s(M))) -> mark(U71(and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)) , active(x(N, 0())) -> mark(U61(and(isNat(N), isNatKind(N)))) , active(and(X1, X2)) -> and(active(X1), X2) , active(and(tt(), X)) -> mark(X) , active(isNatKind(s(V1))) -> mark(isNatKind(V1)) , active(isNatKind(plus(V1, V2))) -> mark(and(isNatKind(V1), isNatKind(V2))) , active(isNatKind(0())) -> mark(tt()) , active(isNatKind(x(V1, V2))) -> mark(and(isNatKind(V1), isNatKind(V2))) , U11(mark(X1), X2, X3) -> mark(U11(X1, X2, X3)) , U11(ok(X1), ok(X2), ok(X3)) -> ok(U11(X1, X2, X3)) , U12(mark(X1), X2) -> mark(U12(X1, X2)) , U12(ok(X1), ok(X2)) -> ok(U12(X1, X2)) , isNat(ok(X)) -> ok(isNat(X)) , U13(mark(X)) -> mark(U13(X)) , U13(ok(X)) -> ok(U13(X)) , U21(mark(X1), X2) -> mark(U21(X1, X2)) , U21(ok(X1), ok(X2)) -> ok(U21(X1, X2)) , U22(mark(X)) -> mark(U22(X)) , U22(ok(X)) -> ok(U22(X)) , U31(mark(X1), X2, X3) -> mark(U31(X1, X2, X3)) , U31(ok(X1), ok(X2), ok(X3)) -> ok(U31(X1, X2, X3)) , U32(mark(X1), X2) -> mark(U32(X1, X2)) , U32(ok(X1), ok(X2)) -> ok(U32(X1, X2)) , U33(mark(X)) -> mark(U33(X)) , U33(ok(X)) -> ok(U33(X)) , U41(mark(X1), X2) -> mark(U41(X1, X2)) , U41(ok(X1), ok(X2)) -> ok(U41(X1, X2)) , U51(mark(X1), X2, X3) -> mark(U51(X1, X2, X3)) , U51(ok(X1), ok(X2), ok(X3)) -> ok(U51(X1, X2, X3)) , s(mark(X)) -> mark(s(X)) , s(ok(X)) -> ok(s(X)) , plus(X1, mark(X2)) -> mark(plus(X1, X2)) , plus(mark(X1), X2) -> mark(plus(X1, X2)) , plus(ok(X1), ok(X2)) -> ok(plus(X1, X2)) , U61(mark(X)) -> mark(U61(X)) , U61(ok(X)) -> ok(U61(X)) , U71(mark(X1), X2, X3) -> mark(U71(X1, X2, X3)) , U71(ok(X1), ok(X2), ok(X3)) -> ok(U71(X1, X2, X3)) , x(X1, mark(X2)) -> mark(x(X1, X2)) , x(mark(X1), X2) -> mark(x(X1, X2)) , x(ok(X1), ok(X2)) -> ok(x(X1, X2)) , and(mark(X1), X2) -> mark(and(X1, X2)) , and(ok(X1), ok(X2)) -> ok(and(X1, X2)) , isNatKind(ok(X)) -> ok(isNatKind(X)) , proper(U11(X1, X2, X3)) -> U11(proper(X1), proper(X2), proper(X3)) , proper(tt()) -> ok(tt()) , proper(U12(X1, X2)) -> U12(proper(X1), proper(X2)) , proper(isNat(X)) -> isNat(proper(X)) , proper(U13(X)) -> U13(proper(X)) , proper(U21(X1, X2)) -> U21(proper(X1), proper(X2)) , proper(U22(X)) -> U22(proper(X)) , proper(U31(X1, X2, X3)) -> U31(proper(X1), proper(X2), proper(X3)) , proper(U32(X1, X2)) -> U32(proper(X1), proper(X2)) , proper(U33(X)) -> U33(proper(X)) , proper(U41(X1, X2)) -> U41(proper(X1), proper(X2)) , proper(U51(X1, X2, X3)) -> U51(proper(X1), proper(X2), proper(X3)) , proper(s(X)) -> s(proper(X)) , proper(plus(X1, X2)) -> plus(proper(X1), proper(X2)) , proper(U61(X)) -> U61(proper(X)) , proper(0()) -> ok(0()) , proper(U71(X1, X2, X3)) -> U71(proper(X1), proper(X2), proper(X3)) , proper(x(X1, X2)) -> x(proper(X1), proper(X2)) , proper(and(X1, X2)) -> and(proper(X1), proper(X2)) , proper(isNatKind(X)) -> isNatKind(proper(X)) , top(mark(X)) -> top(proper(X)) , top(ok(X)) -> top(active(X)) } Obligation: runtime complexity Answer: MAYBE Consider the dependency graph: 1: active^#(U11(X1, X2, X3)) -> c_1(U11^#(active(X1), X2, X3)) -->_1 U11^#(ok(X1), ok(X2), ok(X3)) -> c_45(U11^#(X1, X2, X3)) :45 -->_1 U11^#(mark(X1), X2, X3) -> c_44(U11^#(X1, X2, X3)) :44 2: active^#(U11(tt(), V1, V2)) -> c_2(U12^#(isNat(V1), V2)) -->_1 U12^#(ok(X1), ok(X2)) -> c_47(U12^#(X1, X2)) :47 -->_1 U12^#(mark(X1), X2) -> c_46(U12^#(X1, X2)) :46 3: active^#(U12(X1, X2)) -> c_3(U12^#(active(X1), X2)) -->_1 U12^#(ok(X1), ok(X2)) -> c_47(U12^#(X1, X2)) :47 -->_1 U12^#(mark(X1), X2) -> c_46(U12^#(X1, X2)) :46 4: active^#(U12(tt(), V2)) -> c_4(U13^#(isNat(V2))) -->_1 U13^#(ok(X)) -> c_50(U13^#(X)) :49 -->_1 U13^#(mark(X)) -> c_49(U13^#(X)) :48 5: active^#(isNat(s(V1))) -> c_5(U21^#(isNatKind(V1), V1)) -->_1 U21^#(ok(X1), ok(X2)) -> c_52(U21^#(X1, X2)) :51 -->_1 U21^#(mark(X1), X2) -> c_51(U21^#(X1, X2)) :50 6: active^#(isNat(plus(V1, V2))) -> c_6(U11^#(and(isNatKind(V1), isNatKind(V2)), V1, V2)) -->_1 U11^#(ok(X1), ok(X2), ok(X3)) -> c_45(U11^#(X1, X2, X3)) :45 -->_1 U11^#(mark(X1), X2, X3) -> c_44(U11^#(X1, X2, X3)) :44 7: active^#(isNat(0())) -> c_7() 8: active^#(isNat(x(V1, V2))) -> c_8(U31^#(and(isNatKind(V1), isNatKind(V2)), V1, V2)) -->_1 U31^#(ok(X1), ok(X2), ok(X3)) -> c_56(U31^#(X1, X2, X3)) :53 -->_1 U31^#(mark(X1), X2, X3) -> c_55(U31^#(X1, X2, X3)) :52 9: active^#(U13(X)) -> c_9(U13^#(active(X))) -->_1 U13^#(ok(X)) -> c_50(U13^#(X)) :49 -->_1 U13^#(mark(X)) -> c_49(U13^#(X)) :48 10: active^#(U13(tt())) -> c_10() 11: active^#(U21(X1, X2)) -> c_11(U21^#(active(X1), X2)) -->_1 U21^#(ok(X1), ok(X2)) -> c_52(U21^#(X1, X2)) :51 -->_1 U21^#(mark(X1), X2) -> c_51(U21^#(X1, X2)) :50 12: active^#(U21(tt(), V1)) -> c_12(U22^#(isNat(V1))) -->_1 U22^#(ok(X)) -> c_54(U22^#(X)) :55 -->_1 U22^#(mark(X)) -> c_53(U22^#(X)) :54 13: active^#(U22(X)) -> c_13(U22^#(active(X))) -->_1 U22^#(ok(X)) -> c_54(U22^#(X)) :55 -->_1 U22^#(mark(X)) -> c_53(U22^#(X)) :54 14: active^#(U22(tt())) -> c_14() 15: active^#(U31(X1, X2, X3)) -> c_15(U31^#(active(X1), X2, X3)) -->_1 U31^#(ok(X1), ok(X2), ok(X3)) -> c_56(U31^#(X1, X2, X3)) :53 -->_1 U31^#(mark(X1), X2, X3) -> c_55(U31^#(X1, X2, X3)) :52 16: active^#(U31(tt(), V1, V2)) -> c_16(U32^#(isNat(V1), V2)) -->_1 U32^#(ok(X1), ok(X2)) -> c_58(U32^#(X1, X2)) :57 -->_1 U32^#(mark(X1), X2) -> c_57(U32^#(X1, X2)) :56 17: active^#(U32(X1, X2)) -> c_17(U32^#(active(X1), X2)) -->_1 U32^#(ok(X1), ok(X2)) -> c_58(U32^#(X1, X2)) :57 -->_1 U32^#(mark(X1), X2) -> c_57(U32^#(X1, X2)) :56 18: active^#(U32(tt(), V2)) -> c_18(U33^#(isNat(V2))) -->_1 U33^#(ok(X)) -> c_60(U33^#(X)) :59 -->_1 U33^#(mark(X)) -> c_59(U33^#(X)) :58 19: active^#(U33(X)) -> c_19(U33^#(active(X))) -->_1 U33^#(ok(X)) -> c_60(U33^#(X)) :59 -->_1 U33^#(mark(X)) -> c_59(U33^#(X)) :58 20: active^#(U33(tt())) -> c_20() 21: active^#(U41(X1, X2)) -> c_21(U41^#(active(X1), X2)) -->_1 U41^#(ok(X1), ok(X2)) -> c_62(U41^#(X1, X2)) :61 -->_1 U41^#(mark(X1), X2) -> c_61(U41^#(X1, X2)) :60 22: active^#(U41(tt(), N)) -> c_22(N) -->_1 top^#(ok(X)) -> c_101(top^#(active(X))) :101 -->_1 top^#(mark(X)) -> c_100(top^#(proper(X))) :100 -->_1 proper^#(isNatKind(X)) -> c_99(isNatKind^#(proper(X))) :99 -->_1 proper^#(and(X1, X2)) -> c_98(and^#(proper(X1), proper(X2))) :98 -->_1 proper^#(x(X1, X2)) -> c_97(x^#(proper(X1), proper(X2))) :97 -->_1 proper^#(U71(X1, X2, X3)) -> c_96(U71^#(proper(X1), proper(X2), proper(X3))) :96 -->_1 proper^#(U61(X)) -> c_94(U61^#(proper(X))) :94 -->_1 proper^#(plus(X1, X2)) -> c_93(plus^#(proper(X1), proper(X2))) :93 -->_1 proper^#(s(X)) -> c_92(s^#(proper(X))) :92 -->_1 proper^#(U51(X1, X2, X3)) -> c_91(U51^#(proper(X1), proper(X2), proper(X3))) :91 -->_1 proper^#(U41(X1, X2)) -> c_90(U41^#(proper(X1), proper(X2))) :90 -->_1 proper^#(U33(X)) -> c_89(U33^#(proper(X))) :89 -->_1 proper^#(U32(X1, X2)) -> c_88(U32^#(proper(X1), proper(X2))) :88 -->_1 proper^#(U31(X1, X2, X3)) -> c_87(U31^#(proper(X1), proper(X2), proper(X3))) :87 -->_1 proper^#(U22(X)) -> c_86(U22^#(proper(X))) :86 -->_1 proper^#(U21(X1, X2)) -> c_85(U21^#(proper(X1), proper(X2))) :85 -->_1 proper^#(U13(X)) -> c_84(U13^#(proper(X))) :84 -->_1 proper^#(isNat(X)) -> c_83(isNat^#(proper(X))) :83 -->_1 proper^#(U12(X1, X2)) -> c_82(U12^#(proper(X1), proper(X2))) :82 -->_1 proper^#(U11(X1, X2, X3)) -> c_80(U11^#(proper(X1), proper(X2), proper(X3))) :80 -->_1 isNat^#(ok(X)) -> c_48(isNat^#(X)) :79 -->_1 isNatKind^#(ok(X)) -> c_79(isNatKind^#(X)) :78 -->_1 and^#(ok(X1), ok(X2)) -> c_78(and^#(X1, X2)) :77 -->_1 and^#(mark(X1), X2) -> c_77(and^#(X1, X2)) :76 -->_1 x^#(ok(X1), ok(X2)) -> c_76(x^#(X1, X2)) :75 -->_1 x^#(mark(X1), X2) -> c_75(x^#(X1, X2)) :74 -->_1 x^#(X1, mark(X2)) -> c_74(x^#(X1, X2)) :73 -->_1 U71^#(ok(X1), ok(X2), ok(X3)) -> c_73(U71^#(X1, X2, X3)) :72 -->_1 U71^#(mark(X1), X2, X3) -> c_72(U71^#(X1, X2, X3)) :71 -->_1 U61^#(ok(X)) -> c_71(U61^#(X)) :70 -->_1 U61^#(mark(X)) -> c_70(U61^#(X)) :69 -->_1 plus^#(ok(X1), ok(X2)) -> c_69(plus^#(X1, X2)) :68 -->_1 plus^#(mark(X1), X2) -> c_68(plus^#(X1, X2)) :67 -->_1 plus^#(X1, mark(X2)) -> c_67(plus^#(X1, X2)) :66 -->_1 s^#(ok(X)) -> c_66(s^#(X)) :65 -->_1 s^#(mark(X)) -> c_65(s^#(X)) :64 -->_1 U51^#(ok(X1), ok(X2), ok(X3)) -> c_64(U51^#(X1, X2, X3)) :63 -->_1 U51^#(mark(X1), X2, X3) -> c_63(U51^#(X1, X2, X3)) :62 -->_1 U41^#(ok(X1), ok(X2)) -> c_62(U41^#(X1, X2)) :61 -->_1 U41^#(mark(X1), X2) -> c_61(U41^#(X1, X2)) :60 -->_1 U33^#(ok(X)) -> c_60(U33^#(X)) :59 -->_1 U33^#(mark(X)) -> c_59(U33^#(X)) :58 -->_1 U32^#(ok(X1), ok(X2)) -> c_58(U32^#(X1, X2)) :57 -->_1 U32^#(mark(X1), X2) -> c_57(U32^#(X1, X2)) :56 -->_1 U22^#(ok(X)) -> c_54(U22^#(X)) :55 -->_1 U22^#(mark(X)) -> c_53(U22^#(X)) :54 -->_1 U31^#(ok(X1), ok(X2), ok(X3)) -> c_56(U31^#(X1, X2, X3)) :53 -->_1 U31^#(mark(X1), X2, X3) -> c_55(U31^#(X1, X2, X3)) :52 -->_1 U21^#(ok(X1), ok(X2)) -> c_52(U21^#(X1, X2)) :51 -->_1 U21^#(mark(X1), X2) -> c_51(U21^#(X1, X2)) :50 -->_1 U13^#(ok(X)) -> c_50(U13^#(X)) :49 -->_1 U13^#(mark(X)) -> c_49(U13^#(X)) :48 -->_1 U12^#(ok(X1), ok(X2)) -> c_47(U12^#(X1, X2)) :47 -->_1 U12^#(mark(X1), X2) -> c_46(U12^#(X1, X2)) :46 -->_1 U11^#(ok(X1), ok(X2), ok(X3)) -> c_45(U11^#(X1, X2, X3)) :45 -->_1 U11^#(mark(X1), X2, X3) -> c_44(U11^#(X1, X2, X3)) :44 -->_1 active^#(isNatKind(x(V1, V2))) -> c_43(and^#(isNatKind(V1), isNatKind(V2))) :43 -->_1 active^#(isNatKind(plus(V1, V2))) -> c_41(and^#(isNatKind(V1), isNatKind(V2))) :41 -->_1 active^#(isNatKind(s(V1))) -> c_40(isNatKind^#(V1)) :40 -->_1 active^#(and(tt(), X)) -> c_39(X) :39 -->_1 active^#(and(X1, X2)) -> c_38(and^#(active(X1), X2)) :38 -->_1 active^#(x(N, 0())) -> c_37(U61^#(and(isNat(N), isNatKind(N)))) :37 -->_1 active^#(x(N, s(M))) -> c_36(U71^#(and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)) :36 -->_1 active^#(x(X1, X2)) -> c_35(x^#(active(X1), X2)) :35 -->_1 active^#(x(X1, X2)) -> c_34(x^#(X1, active(X2))) :34 -->_1 active^#(U71(tt(), M, N)) -> c_33(plus^#(x(N, M), N)) :33 -->_1 active^#(U71(X1, X2, X3)) -> c_32(U71^#(active(X1), X2, X3)) :32 -->_1 active^#(U61(X)) -> c_30(U61^#(active(X))) :30 -->_1 active^#(plus(N, 0())) -> c_29(U41^#(and(isNat(N), isNatKind(N)), N)) :29 -->_1 active^#(plus(N, s(M))) -> c_28(U51^#(and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)) :28 -->_1 active^#(plus(X1, X2)) -> c_27(plus^#(active(X1), X2)) :27 -->_1 active^#(plus(X1, X2)) -> c_26(plus^#(X1, active(X2))) :26 -->_1 active^#(s(X)) -> c_25(s^#(active(X))) :25 -->_1 active^#(U51(tt(), M, N)) -> c_24(s^#(plus(N, M))) :24 -->_1 active^#(U51(X1, X2, X3)) -> c_23(U51^#(active(X1), X2, X3)) :23 -->_1 proper^#(0()) -> c_95() :95 -->_1 proper^#(tt()) -> c_81() :81 -->_1 active^#(isNatKind(0())) -> c_42() :42 -->_1 active^#(U61(tt())) -> c_31() :31 -->_1 active^#(U41(tt(), N)) -> c_22(N) :22 -->_1 active^#(U41(X1, X2)) -> c_21(U41^#(active(X1), X2)) :21 -->_1 active^#(U33(tt())) -> c_20() :20 -->_1 active^#(U33(X)) -> c_19(U33^#(active(X))) :19 -->_1 active^#(U32(tt(), V2)) -> c_18(U33^#(isNat(V2))) :18 -->_1 active^#(U32(X1, X2)) -> c_17(U32^#(active(X1), X2)) :17 -->_1 active^#(U31(tt(), V1, V2)) -> c_16(U32^#(isNat(V1), V2)) :16 -->_1 active^#(U31(X1, X2, X3)) -> c_15(U31^#(active(X1), X2, X3)) :15 -->_1 active^#(U22(tt())) -> c_14() :14 -->_1 active^#(U22(X)) -> c_13(U22^#(active(X))) :13 -->_1 active^#(U21(tt(), V1)) -> c_12(U22^#(isNat(V1))) :12 -->_1 active^#(U21(X1, X2)) -> c_11(U21^#(active(X1), X2)) :11 -->_1 active^#(U13(tt())) -> c_10() :10 -->_1 active^#(U13(X)) -> c_9(U13^#(active(X))) :9 -->_1 active^#(isNat(x(V1, V2))) -> c_8(U31^#(and(isNatKind(V1), isNatKind(V2)), V1, V2)) :8 -->_1 active^#(isNat(0())) -> c_7() :7 -->_1 active^#(isNat(plus(V1, V2))) -> c_6(U11^#(and(isNatKind(V1), isNatKind(V2)), V1, V2)) :6 -->_1 active^#(isNat(s(V1))) -> c_5(U21^#(isNatKind(V1), V1)) :5 -->_1 active^#(U12(tt(), V2)) -> c_4(U13^#(isNat(V2))) :4 -->_1 active^#(U12(X1, X2)) -> c_3(U12^#(active(X1), X2)) :3 -->_1 active^#(U11(tt(), V1, V2)) -> c_2(U12^#(isNat(V1), V2)) :2 -->_1 active^#(U11(X1, X2, X3)) -> c_1(U11^#(active(X1), X2, X3)) :1 23: active^#(U51(X1, X2, X3)) -> c_23(U51^#(active(X1), X2, X3)) -->_1 U51^#(ok(X1), ok(X2), ok(X3)) -> c_64(U51^#(X1, X2, X3)) :63 -->_1 U51^#(mark(X1), X2, X3) -> c_63(U51^#(X1, X2, X3)) :62 24: active^#(U51(tt(), M, N)) -> c_24(s^#(plus(N, M))) -->_1 s^#(ok(X)) -> c_66(s^#(X)) :65 -->_1 s^#(mark(X)) -> c_65(s^#(X)) :64 25: active^#(s(X)) -> c_25(s^#(active(X))) -->_1 s^#(ok(X)) -> c_66(s^#(X)) :65 -->_1 s^#(mark(X)) -> c_65(s^#(X)) :64 26: active^#(plus(X1, X2)) -> c_26(plus^#(X1, active(X2))) -->_1 plus^#(ok(X1), ok(X2)) -> c_69(plus^#(X1, X2)) :68 -->_1 plus^#(mark(X1), X2) -> c_68(plus^#(X1, X2)) :67 -->_1 plus^#(X1, mark(X2)) -> c_67(plus^#(X1, X2)) :66 27: active^#(plus(X1, X2)) -> c_27(plus^#(active(X1), X2)) -->_1 plus^#(ok(X1), ok(X2)) -> c_69(plus^#(X1, X2)) :68 -->_1 plus^#(mark(X1), X2) -> c_68(plus^#(X1, X2)) :67 -->_1 plus^#(X1, mark(X2)) -> c_67(plus^#(X1, X2)) :66 28: active^#(plus(N, s(M))) -> c_28(U51^#(and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)) -->_1 U51^#(ok(X1), ok(X2), ok(X3)) -> c_64(U51^#(X1, X2, X3)) :63 -->_1 U51^#(mark(X1), X2, X3) -> c_63(U51^#(X1, X2, X3)) :62 29: active^#(plus(N, 0())) -> c_29(U41^#(and(isNat(N), isNatKind(N)), N)) -->_1 U41^#(ok(X1), ok(X2)) -> c_62(U41^#(X1, X2)) :61 -->_1 U41^#(mark(X1), X2) -> c_61(U41^#(X1, X2)) :60 30: active^#(U61(X)) -> c_30(U61^#(active(X))) -->_1 U61^#(ok(X)) -> c_71(U61^#(X)) :70 -->_1 U61^#(mark(X)) -> c_70(U61^#(X)) :69 31: active^#(U61(tt())) -> c_31() 32: active^#(U71(X1, X2, X3)) -> c_32(U71^#(active(X1), X2, X3)) -->_1 U71^#(ok(X1), ok(X2), ok(X3)) -> c_73(U71^#(X1, X2, X3)) :72 -->_1 U71^#(mark(X1), X2, X3) -> c_72(U71^#(X1, X2, X3)) :71 33: active^#(U71(tt(), M, N)) -> c_33(plus^#(x(N, M), N)) -->_1 plus^#(ok(X1), ok(X2)) -> c_69(plus^#(X1, X2)) :68 -->_1 plus^#(mark(X1), X2) -> c_68(plus^#(X1, X2)) :67 -->_1 plus^#(X1, mark(X2)) -> c_67(plus^#(X1, X2)) :66 34: active^#(x(X1, X2)) -> c_34(x^#(X1, active(X2))) -->_1 x^#(ok(X1), ok(X2)) -> c_76(x^#(X1, X2)) :75 -->_1 x^#(mark(X1), X2) -> c_75(x^#(X1, X2)) :74 -->_1 x^#(X1, mark(X2)) -> c_74(x^#(X1, X2)) :73 35: active^#(x(X1, X2)) -> c_35(x^#(active(X1), X2)) -->_1 x^#(ok(X1), ok(X2)) -> c_76(x^#(X1, X2)) :75 -->_1 x^#(mark(X1), X2) -> c_75(x^#(X1, X2)) :74 -->_1 x^#(X1, mark(X2)) -> c_74(x^#(X1, X2)) :73 36: active^#(x(N, s(M))) -> c_36(U71^#(and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)) -->_1 U71^#(ok(X1), ok(X2), ok(X3)) -> c_73(U71^#(X1, X2, X3)) :72 -->_1 U71^#(mark(X1), X2, X3) -> c_72(U71^#(X1, X2, X3)) :71 37: active^#(x(N, 0())) -> c_37(U61^#(and(isNat(N), isNatKind(N)))) -->_1 U61^#(ok(X)) -> c_71(U61^#(X)) :70 -->_1 U61^#(mark(X)) -> c_70(U61^#(X)) :69 38: active^#(and(X1, X2)) -> c_38(and^#(active(X1), X2)) -->_1 and^#(ok(X1), ok(X2)) -> c_78(and^#(X1, X2)) :77 -->_1 and^#(mark(X1), X2) -> c_77(and^#(X1, X2)) :76 39: active^#(and(tt(), X)) -> c_39(X) -->_1 top^#(ok(X)) -> c_101(top^#(active(X))) :101 -->_1 top^#(mark(X)) -> c_100(top^#(proper(X))) :100 -->_1 proper^#(isNatKind(X)) -> c_99(isNatKind^#(proper(X))) :99 -->_1 proper^#(and(X1, X2)) -> c_98(and^#(proper(X1), proper(X2))) :98 -->_1 proper^#(x(X1, X2)) -> c_97(x^#(proper(X1), proper(X2))) :97 -->_1 proper^#(U71(X1, X2, X3)) -> c_96(U71^#(proper(X1), proper(X2), proper(X3))) :96 -->_1 proper^#(U61(X)) -> c_94(U61^#(proper(X))) :94 -->_1 proper^#(plus(X1, X2)) -> c_93(plus^#(proper(X1), proper(X2))) :93 -->_1 proper^#(s(X)) -> c_92(s^#(proper(X))) :92 -->_1 proper^#(U51(X1, X2, X3)) -> c_91(U51^#(proper(X1), proper(X2), proper(X3))) :91 -->_1 proper^#(U41(X1, X2)) -> c_90(U41^#(proper(X1), proper(X2))) :90 -->_1 proper^#(U33(X)) -> c_89(U33^#(proper(X))) :89 -->_1 proper^#(U32(X1, X2)) -> c_88(U32^#(proper(X1), proper(X2))) :88 -->_1 proper^#(U31(X1, X2, X3)) -> c_87(U31^#(proper(X1), proper(X2), proper(X3))) :87 -->_1 proper^#(U22(X)) -> c_86(U22^#(proper(X))) :86 -->_1 proper^#(U21(X1, X2)) -> c_85(U21^#(proper(X1), proper(X2))) :85 -->_1 proper^#(U13(X)) -> c_84(U13^#(proper(X))) :84 -->_1 proper^#(isNat(X)) -> c_83(isNat^#(proper(X))) :83 -->_1 proper^#(U12(X1, X2)) -> c_82(U12^#(proper(X1), proper(X2))) :82 -->_1 proper^#(U11(X1, X2, X3)) -> c_80(U11^#(proper(X1), proper(X2), proper(X3))) :80 -->_1 isNat^#(ok(X)) -> c_48(isNat^#(X)) :79 -->_1 isNatKind^#(ok(X)) -> c_79(isNatKind^#(X)) :78 -->_1 and^#(ok(X1), ok(X2)) -> c_78(and^#(X1, X2)) :77 -->_1 and^#(mark(X1), X2) -> c_77(and^#(X1, X2)) :76 -->_1 x^#(ok(X1), ok(X2)) -> c_76(x^#(X1, X2)) :75 -->_1 x^#(mark(X1), X2) -> c_75(x^#(X1, X2)) :74 -->_1 x^#(X1, mark(X2)) -> c_74(x^#(X1, X2)) :73 -->_1 U71^#(ok(X1), ok(X2), ok(X3)) -> c_73(U71^#(X1, X2, X3)) :72 -->_1 U71^#(mark(X1), X2, X3) -> c_72(U71^#(X1, X2, X3)) :71 -->_1 U61^#(ok(X)) -> c_71(U61^#(X)) :70 -->_1 U61^#(mark(X)) -> c_70(U61^#(X)) :69 -->_1 plus^#(ok(X1), ok(X2)) -> c_69(plus^#(X1, X2)) :68 -->_1 plus^#(mark(X1), X2) -> c_68(plus^#(X1, X2)) :67 -->_1 plus^#(X1, mark(X2)) -> c_67(plus^#(X1, X2)) :66 -->_1 s^#(ok(X)) -> c_66(s^#(X)) :65 -->_1 s^#(mark(X)) -> c_65(s^#(X)) :64 -->_1 U51^#(ok(X1), ok(X2), ok(X3)) -> c_64(U51^#(X1, X2, X3)) :63 -->_1 U51^#(mark(X1), X2, X3) -> c_63(U51^#(X1, X2, X3)) :62 -->_1 U41^#(ok(X1), ok(X2)) -> c_62(U41^#(X1, X2)) :61 -->_1 U41^#(mark(X1), X2) -> c_61(U41^#(X1, X2)) :60 -->_1 U33^#(ok(X)) -> c_60(U33^#(X)) :59 -->_1 U33^#(mark(X)) -> c_59(U33^#(X)) :58 -->_1 U32^#(ok(X1), ok(X2)) -> c_58(U32^#(X1, X2)) :57 -->_1 U32^#(mark(X1), X2) -> c_57(U32^#(X1, X2)) :56 -->_1 U22^#(ok(X)) -> c_54(U22^#(X)) :55 -->_1 U22^#(mark(X)) -> c_53(U22^#(X)) :54 -->_1 U31^#(ok(X1), ok(X2), ok(X3)) -> c_56(U31^#(X1, X2, X3)) :53 -->_1 U31^#(mark(X1), X2, X3) -> c_55(U31^#(X1, X2, X3)) :52 -->_1 U21^#(ok(X1), ok(X2)) -> c_52(U21^#(X1, X2)) :51 -->_1 U21^#(mark(X1), X2) -> c_51(U21^#(X1, X2)) :50 -->_1 U13^#(ok(X)) -> c_50(U13^#(X)) :49 -->_1 U13^#(mark(X)) -> c_49(U13^#(X)) :48 -->_1 U12^#(ok(X1), ok(X2)) -> c_47(U12^#(X1, X2)) :47 -->_1 U12^#(mark(X1), X2) -> c_46(U12^#(X1, X2)) :46 -->_1 U11^#(ok(X1), ok(X2), ok(X3)) -> c_45(U11^#(X1, X2, X3)) :45 -->_1 U11^#(mark(X1), X2, X3) -> c_44(U11^#(X1, X2, X3)) :44 -->_1 active^#(isNatKind(x(V1, V2))) -> c_43(and^#(isNatKind(V1), isNatKind(V2))) :43 -->_1 active^#(isNatKind(plus(V1, V2))) -> c_41(and^#(isNatKind(V1), isNatKind(V2))) :41 -->_1 active^#(isNatKind(s(V1))) -> c_40(isNatKind^#(V1)) :40 -->_1 proper^#(0()) -> c_95() :95 -->_1 proper^#(tt()) -> c_81() :81 -->_1 active^#(isNatKind(0())) -> c_42() :42 -->_1 active^#(and(tt(), X)) -> c_39(X) :39 -->_1 active^#(and(X1, X2)) -> c_38(and^#(active(X1), X2)) :38 -->_1 active^#(x(N, 0())) -> c_37(U61^#(and(isNat(N), isNatKind(N)))) :37 -->_1 active^#(x(N, s(M))) -> c_36(U71^#(and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)) :36 -->_1 active^#(x(X1, X2)) -> c_35(x^#(active(X1), X2)) :35 -->_1 active^#(x(X1, X2)) -> c_34(x^#(X1, active(X2))) :34 -->_1 active^#(U71(tt(), M, N)) -> c_33(plus^#(x(N, M), N)) :33 -->_1 active^#(U71(X1, X2, X3)) -> c_32(U71^#(active(X1), X2, X3)) :32 -->_1 active^#(U61(tt())) -> c_31() :31 -->_1 active^#(U61(X)) -> c_30(U61^#(active(X))) :30 -->_1 active^#(plus(N, 0())) -> c_29(U41^#(and(isNat(N), isNatKind(N)), N)) :29 -->_1 active^#(plus(N, s(M))) -> c_28(U51^#(and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)) :28 -->_1 active^#(plus(X1, X2)) -> c_27(plus^#(active(X1), X2)) :27 -->_1 active^#(plus(X1, X2)) -> c_26(plus^#(X1, active(X2))) :26 -->_1 active^#(s(X)) -> c_25(s^#(active(X))) :25 -->_1 active^#(U51(tt(), M, N)) -> c_24(s^#(plus(N, M))) :24 -->_1 active^#(U51(X1, X2, X3)) -> c_23(U51^#(active(X1), X2, X3)) :23 -->_1 active^#(U41(tt(), N)) -> c_22(N) :22 -->_1 active^#(U41(X1, X2)) -> c_21(U41^#(active(X1), X2)) :21 -->_1 active^#(U33(tt())) -> c_20() :20 -->_1 active^#(U33(X)) -> c_19(U33^#(active(X))) :19 -->_1 active^#(U32(tt(), V2)) -> c_18(U33^#(isNat(V2))) :18 -->_1 active^#(U32(X1, X2)) -> c_17(U32^#(active(X1), X2)) :17 -->_1 active^#(U31(tt(), V1, V2)) -> c_16(U32^#(isNat(V1), V2)) :16 -->_1 active^#(U31(X1, X2, X3)) -> c_15(U31^#(active(X1), X2, X3)) :15 -->_1 active^#(U22(tt())) -> c_14() :14 -->_1 active^#(U22(X)) -> c_13(U22^#(active(X))) :13 -->_1 active^#(U21(tt(), V1)) -> c_12(U22^#(isNat(V1))) :12 -->_1 active^#(U21(X1, X2)) -> c_11(U21^#(active(X1), X2)) :11 -->_1 active^#(U13(tt())) -> c_10() :10 -->_1 active^#(U13(X)) -> c_9(U13^#(active(X))) :9 -->_1 active^#(isNat(x(V1, V2))) -> c_8(U31^#(and(isNatKind(V1), isNatKind(V2)), V1, V2)) :8 -->_1 active^#(isNat(0())) -> c_7() :7 -->_1 active^#(isNat(plus(V1, V2))) -> c_6(U11^#(and(isNatKind(V1), isNatKind(V2)), V1, V2)) :6 -->_1 active^#(isNat(s(V1))) -> c_5(U21^#(isNatKind(V1), V1)) :5 -->_1 active^#(U12(tt(), V2)) -> c_4(U13^#(isNat(V2))) :4 -->_1 active^#(U12(X1, X2)) -> c_3(U12^#(active(X1), X2)) :3 -->_1 active^#(U11(tt(), V1, V2)) -> c_2(U12^#(isNat(V1), V2)) :2 -->_1 active^#(U11(X1, X2, X3)) -> c_1(U11^#(active(X1), X2, X3)) :1 40: active^#(isNatKind(s(V1))) -> c_40(isNatKind^#(V1)) -->_1 isNatKind^#(ok(X)) -> c_79(isNatKind^#(X)) :78 41: active^#(isNatKind(plus(V1, V2))) -> c_41(and^#(isNatKind(V1), isNatKind(V2))) -->_1 and^#(ok(X1), ok(X2)) -> c_78(and^#(X1, X2)) :77 -->_1 and^#(mark(X1), X2) -> c_77(and^#(X1, X2)) :76 42: active^#(isNatKind(0())) -> c_42() 43: active^#(isNatKind(x(V1, V2))) -> c_43(and^#(isNatKind(V1), isNatKind(V2))) -->_1 and^#(ok(X1), ok(X2)) -> c_78(and^#(X1, X2)) :77 -->_1 and^#(mark(X1), X2) -> c_77(and^#(X1, X2)) :76 44: U11^#(mark(X1), X2, X3) -> c_44(U11^#(X1, X2, X3)) -->_1 U11^#(ok(X1), ok(X2), ok(X3)) -> c_45(U11^#(X1, X2, X3)) :45 -->_1 U11^#(mark(X1), X2, X3) -> c_44(U11^#(X1, X2, X3)) :44 45: U11^#(ok(X1), ok(X2), ok(X3)) -> c_45(U11^#(X1, X2, X3)) -->_1 U11^#(ok(X1), ok(X2), ok(X3)) -> c_45(U11^#(X1, X2, X3)) :45 -->_1 U11^#(mark(X1), X2, X3) -> c_44(U11^#(X1, X2, X3)) :44 46: U12^#(mark(X1), X2) -> c_46(U12^#(X1, X2)) -->_1 U12^#(ok(X1), ok(X2)) -> c_47(U12^#(X1, X2)) :47 -->_1 U12^#(mark(X1), X2) -> c_46(U12^#(X1, X2)) :46 47: U12^#(ok(X1), ok(X2)) -> c_47(U12^#(X1, X2)) -->_1 U12^#(ok(X1), ok(X2)) -> c_47(U12^#(X1, X2)) :47 -->_1 U12^#(mark(X1), X2) -> c_46(U12^#(X1, X2)) :46 48: U13^#(mark(X)) -> c_49(U13^#(X)) -->_1 U13^#(ok(X)) -> c_50(U13^#(X)) :49 -->_1 U13^#(mark(X)) -> c_49(U13^#(X)) :48 49: U13^#(ok(X)) -> c_50(U13^#(X)) -->_1 U13^#(ok(X)) -> c_50(U13^#(X)) :49 -->_1 U13^#(mark(X)) -> c_49(U13^#(X)) :48 50: U21^#(mark(X1), X2) -> c_51(U21^#(X1, X2)) -->_1 U21^#(ok(X1), ok(X2)) -> c_52(U21^#(X1, X2)) :51 -->_1 U21^#(mark(X1), X2) -> c_51(U21^#(X1, X2)) :50 51: U21^#(ok(X1), ok(X2)) -> c_52(U21^#(X1, X2)) -->_1 U21^#(ok(X1), ok(X2)) -> c_52(U21^#(X1, X2)) :51 -->_1 U21^#(mark(X1), X2) -> c_51(U21^#(X1, X2)) :50 52: U31^#(mark(X1), X2, X3) -> c_55(U31^#(X1, X2, X3)) -->_1 U31^#(ok(X1), ok(X2), ok(X3)) -> c_56(U31^#(X1, X2, X3)) :53 -->_1 U31^#(mark(X1), X2, X3) -> c_55(U31^#(X1, X2, X3)) :52 53: U31^#(ok(X1), ok(X2), ok(X3)) -> c_56(U31^#(X1, X2, X3)) -->_1 U31^#(ok(X1), ok(X2), ok(X3)) -> c_56(U31^#(X1, X2, X3)) :53 -->_1 U31^#(mark(X1), X2, X3) -> c_55(U31^#(X1, X2, X3)) :52 54: U22^#(mark(X)) -> c_53(U22^#(X)) -->_1 U22^#(ok(X)) -> c_54(U22^#(X)) :55 -->_1 U22^#(mark(X)) -> c_53(U22^#(X)) :54 55: U22^#(ok(X)) -> c_54(U22^#(X)) -->_1 U22^#(ok(X)) -> c_54(U22^#(X)) :55 -->_1 U22^#(mark(X)) -> c_53(U22^#(X)) :54 56: U32^#(mark(X1), X2) -> c_57(U32^#(X1, X2)) -->_1 U32^#(ok(X1), ok(X2)) -> c_58(U32^#(X1, X2)) :57 -->_1 U32^#(mark(X1), X2) -> c_57(U32^#(X1, X2)) :56 57: U32^#(ok(X1), ok(X2)) -> c_58(U32^#(X1, X2)) -->_1 U32^#(ok(X1), ok(X2)) -> c_58(U32^#(X1, X2)) :57 -->_1 U32^#(mark(X1), X2) -> c_57(U32^#(X1, X2)) :56 58: U33^#(mark(X)) -> c_59(U33^#(X)) -->_1 U33^#(ok(X)) -> c_60(U33^#(X)) :59 -->_1 U33^#(mark(X)) -> c_59(U33^#(X)) :58 59: U33^#(ok(X)) -> c_60(U33^#(X)) -->_1 U33^#(ok(X)) -> c_60(U33^#(X)) :59 -->_1 U33^#(mark(X)) -> c_59(U33^#(X)) :58 60: U41^#(mark(X1), X2) -> c_61(U41^#(X1, X2)) -->_1 U41^#(ok(X1), ok(X2)) -> c_62(U41^#(X1, X2)) :61 -->_1 U41^#(mark(X1), X2) -> c_61(U41^#(X1, X2)) :60 61: U41^#(ok(X1), ok(X2)) -> c_62(U41^#(X1, X2)) -->_1 U41^#(ok(X1), ok(X2)) -> c_62(U41^#(X1, X2)) :61 -->_1 U41^#(mark(X1), X2) -> c_61(U41^#(X1, X2)) :60 62: U51^#(mark(X1), X2, X3) -> c_63(U51^#(X1, X2, X3)) -->_1 U51^#(ok(X1), ok(X2), ok(X3)) -> c_64(U51^#(X1, X2, X3)) :63 -->_1 U51^#(mark(X1), X2, X3) -> c_63(U51^#(X1, X2, X3)) :62 63: U51^#(ok(X1), ok(X2), ok(X3)) -> c_64(U51^#(X1, X2, X3)) -->_1 U51^#(ok(X1), ok(X2), ok(X3)) -> c_64(U51^#(X1, X2, X3)) :63 -->_1 U51^#(mark(X1), X2, X3) -> c_63(U51^#(X1, X2, X3)) :62 64: s^#(mark(X)) -> c_65(s^#(X)) -->_1 s^#(ok(X)) -> c_66(s^#(X)) :65 -->_1 s^#(mark(X)) -> c_65(s^#(X)) :64 65: s^#(ok(X)) -> c_66(s^#(X)) -->_1 s^#(ok(X)) -> c_66(s^#(X)) :65 -->_1 s^#(mark(X)) -> c_65(s^#(X)) :64 66: plus^#(X1, mark(X2)) -> c_67(plus^#(X1, X2)) -->_1 plus^#(ok(X1), ok(X2)) -> c_69(plus^#(X1, X2)) :68 -->_1 plus^#(mark(X1), X2) -> c_68(plus^#(X1, X2)) :67 -->_1 plus^#(X1, mark(X2)) -> c_67(plus^#(X1, X2)) :66 67: plus^#(mark(X1), X2) -> c_68(plus^#(X1, X2)) -->_1 plus^#(ok(X1), ok(X2)) -> c_69(plus^#(X1, X2)) :68 -->_1 plus^#(mark(X1), X2) -> c_68(plus^#(X1, X2)) :67 -->_1 plus^#(X1, mark(X2)) -> c_67(plus^#(X1, X2)) :66 68: plus^#(ok(X1), ok(X2)) -> c_69(plus^#(X1, X2)) -->_1 plus^#(ok(X1), ok(X2)) -> c_69(plus^#(X1, X2)) :68 -->_1 plus^#(mark(X1), X2) -> c_68(plus^#(X1, X2)) :67 -->_1 plus^#(X1, mark(X2)) -> c_67(plus^#(X1, X2)) :66 69: U61^#(mark(X)) -> c_70(U61^#(X)) -->_1 U61^#(ok(X)) -> c_71(U61^#(X)) :70 -->_1 U61^#(mark(X)) -> c_70(U61^#(X)) :69 70: U61^#(ok(X)) -> c_71(U61^#(X)) -->_1 U61^#(ok(X)) -> c_71(U61^#(X)) :70 -->_1 U61^#(mark(X)) -> c_70(U61^#(X)) :69 71: U71^#(mark(X1), X2, X3) -> c_72(U71^#(X1, X2, X3)) -->_1 U71^#(ok(X1), ok(X2), ok(X3)) -> c_73(U71^#(X1, X2, X3)) :72 -->_1 U71^#(mark(X1), X2, X3) -> c_72(U71^#(X1, X2, X3)) :71 72: U71^#(ok(X1), ok(X2), ok(X3)) -> c_73(U71^#(X1, X2, X3)) -->_1 U71^#(ok(X1), ok(X2), ok(X3)) -> c_73(U71^#(X1, X2, X3)) :72 -->_1 U71^#(mark(X1), X2, X3) -> c_72(U71^#(X1, X2, X3)) :71 73: x^#(X1, mark(X2)) -> c_74(x^#(X1, X2)) -->_1 x^#(ok(X1), ok(X2)) -> c_76(x^#(X1, X2)) :75 -->_1 x^#(mark(X1), X2) -> c_75(x^#(X1, X2)) :74 -->_1 x^#(X1, mark(X2)) -> c_74(x^#(X1, X2)) :73 74: x^#(mark(X1), X2) -> c_75(x^#(X1, X2)) -->_1 x^#(ok(X1), ok(X2)) -> c_76(x^#(X1, X2)) :75 -->_1 x^#(mark(X1), X2) -> c_75(x^#(X1, X2)) :74 -->_1 x^#(X1, mark(X2)) -> c_74(x^#(X1, X2)) :73 75: x^#(ok(X1), ok(X2)) -> c_76(x^#(X1, X2)) -->_1 x^#(ok(X1), ok(X2)) -> c_76(x^#(X1, X2)) :75 -->_1 x^#(mark(X1), X2) -> c_75(x^#(X1, X2)) :74 -->_1 x^#(X1, mark(X2)) -> c_74(x^#(X1, X2)) :73 76: and^#(mark(X1), X2) -> c_77(and^#(X1, X2)) -->_1 and^#(ok(X1), ok(X2)) -> c_78(and^#(X1, X2)) :77 -->_1 and^#(mark(X1), X2) -> c_77(and^#(X1, X2)) :76 77: and^#(ok(X1), ok(X2)) -> c_78(and^#(X1, X2)) -->_1 and^#(ok(X1), ok(X2)) -> c_78(and^#(X1, X2)) :77 -->_1 and^#(mark(X1), X2) -> c_77(and^#(X1, X2)) :76 78: isNatKind^#(ok(X)) -> c_79(isNatKind^#(X)) -->_1 isNatKind^#(ok(X)) -> c_79(isNatKind^#(X)) :78 79: isNat^#(ok(X)) -> c_48(isNat^#(X)) -->_1 isNat^#(ok(X)) -> c_48(isNat^#(X)) :79 80: proper^#(U11(X1, X2, X3)) -> c_80(U11^#(proper(X1), proper(X2), proper(X3))) -->_1 U11^#(ok(X1), ok(X2), ok(X3)) -> c_45(U11^#(X1, X2, X3)) :45 -->_1 U11^#(mark(X1), X2, X3) -> c_44(U11^#(X1, X2, X3)) :44 81: proper^#(tt()) -> c_81() 82: proper^#(U12(X1, X2)) -> c_82(U12^#(proper(X1), proper(X2))) -->_1 U12^#(ok(X1), ok(X2)) -> c_47(U12^#(X1, X2)) :47 -->_1 U12^#(mark(X1), X2) -> c_46(U12^#(X1, X2)) :46 83: proper^#(isNat(X)) -> c_83(isNat^#(proper(X))) -->_1 isNat^#(ok(X)) -> c_48(isNat^#(X)) :79 84: proper^#(U13(X)) -> c_84(U13^#(proper(X))) -->_1 U13^#(ok(X)) -> c_50(U13^#(X)) :49 -->_1 U13^#(mark(X)) -> c_49(U13^#(X)) :48 85: proper^#(U21(X1, X2)) -> c_85(U21^#(proper(X1), proper(X2))) -->_1 U21^#(ok(X1), ok(X2)) -> c_52(U21^#(X1, X2)) :51 -->_1 U21^#(mark(X1), X2) -> c_51(U21^#(X1, X2)) :50 86: proper^#(U22(X)) -> c_86(U22^#(proper(X))) -->_1 U22^#(ok(X)) -> c_54(U22^#(X)) :55 -->_1 U22^#(mark(X)) -> c_53(U22^#(X)) :54 87: proper^#(U31(X1, X2, X3)) -> c_87(U31^#(proper(X1), proper(X2), proper(X3))) -->_1 U31^#(ok(X1), ok(X2), ok(X3)) -> c_56(U31^#(X1, X2, X3)) :53 -->_1 U31^#(mark(X1), X2, X3) -> c_55(U31^#(X1, X2, X3)) :52 88: proper^#(U32(X1, X2)) -> c_88(U32^#(proper(X1), proper(X2))) -->_1 U32^#(ok(X1), ok(X2)) -> c_58(U32^#(X1, X2)) :57 -->_1 U32^#(mark(X1), X2) -> c_57(U32^#(X1, X2)) :56 89: proper^#(U33(X)) -> c_89(U33^#(proper(X))) -->_1 U33^#(ok(X)) -> c_60(U33^#(X)) :59 -->_1 U33^#(mark(X)) -> c_59(U33^#(X)) :58 90: proper^#(U41(X1, X2)) -> c_90(U41^#(proper(X1), proper(X2))) -->_1 U41^#(ok(X1), ok(X2)) -> c_62(U41^#(X1, X2)) :61 -->_1 U41^#(mark(X1), X2) -> c_61(U41^#(X1, X2)) :60 91: proper^#(U51(X1, X2, X3)) -> c_91(U51^#(proper(X1), proper(X2), proper(X3))) -->_1 U51^#(ok(X1), ok(X2), ok(X3)) -> c_64(U51^#(X1, X2, X3)) :63 -->_1 U51^#(mark(X1), X2, X3) -> c_63(U51^#(X1, X2, X3)) :62 92: proper^#(s(X)) -> c_92(s^#(proper(X))) -->_1 s^#(ok(X)) -> c_66(s^#(X)) :65 -->_1 s^#(mark(X)) -> c_65(s^#(X)) :64 93: proper^#(plus(X1, X2)) -> c_93(plus^#(proper(X1), proper(X2))) -->_1 plus^#(ok(X1), ok(X2)) -> c_69(plus^#(X1, X2)) :68 -->_1 plus^#(mark(X1), X2) -> c_68(plus^#(X1, X2)) :67 -->_1 plus^#(X1, mark(X2)) -> c_67(plus^#(X1, X2)) :66 94: proper^#(U61(X)) -> c_94(U61^#(proper(X))) -->_1 U61^#(ok(X)) -> c_71(U61^#(X)) :70 -->_1 U61^#(mark(X)) -> c_70(U61^#(X)) :69 95: proper^#(0()) -> c_95() 96: proper^#(U71(X1, X2, X3)) -> c_96(U71^#(proper(X1), proper(X2), proper(X3))) -->_1 U71^#(ok(X1), ok(X2), ok(X3)) -> c_73(U71^#(X1, X2, X3)) :72 -->_1 U71^#(mark(X1), X2, X3) -> c_72(U71^#(X1, X2, X3)) :71 97: proper^#(x(X1, X2)) -> c_97(x^#(proper(X1), proper(X2))) -->_1 x^#(ok(X1), ok(X2)) -> c_76(x^#(X1, X2)) :75 -->_1 x^#(mark(X1), X2) -> c_75(x^#(X1, X2)) :74 -->_1 x^#(X1, mark(X2)) -> c_74(x^#(X1, X2)) :73 98: proper^#(and(X1, X2)) -> c_98(and^#(proper(X1), proper(X2))) -->_1 and^#(ok(X1), ok(X2)) -> c_78(and^#(X1, X2)) :77 -->_1 and^#(mark(X1), X2) -> c_77(and^#(X1, X2)) :76 99: proper^#(isNatKind(X)) -> c_99(isNatKind^#(proper(X))) -->_1 isNatKind^#(ok(X)) -> c_79(isNatKind^#(X)) :78 100: top^#(mark(X)) -> c_100(top^#(proper(X))) -->_1 top^#(ok(X)) -> c_101(top^#(active(X))) :101 -->_1 top^#(mark(X)) -> c_100(top^#(proper(X))) :100 101: top^#(ok(X)) -> c_101(top^#(active(X))) -->_1 top^#(ok(X)) -> c_101(top^#(active(X))) :101 -->_1 top^#(mark(X)) -> c_100(top^#(proper(X))) :100 Only the nodes {44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65,66,68,67,69,70,71,72,73,75,74,76,77,78,79,81,95,100,101} are reachable from nodes {44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,81,95,100,101} that start derivation from marked basic terms. The nodes not reachable are removed from the problem. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { U11^#(mark(X1), X2, X3) -> c_44(U11^#(X1, X2, X3)) , U11^#(ok(X1), ok(X2), ok(X3)) -> c_45(U11^#(X1, X2, X3)) , U12^#(mark(X1), X2) -> c_46(U12^#(X1, X2)) , U12^#(ok(X1), ok(X2)) -> c_47(U12^#(X1, X2)) , U13^#(mark(X)) -> c_49(U13^#(X)) , U13^#(ok(X)) -> c_50(U13^#(X)) , U21^#(mark(X1), X2) -> c_51(U21^#(X1, X2)) , U21^#(ok(X1), ok(X2)) -> c_52(U21^#(X1, X2)) , U31^#(mark(X1), X2, X3) -> c_55(U31^#(X1, X2, X3)) , U31^#(ok(X1), ok(X2), ok(X3)) -> c_56(U31^#(X1, X2, X3)) , U22^#(mark(X)) -> c_53(U22^#(X)) , U22^#(ok(X)) -> c_54(U22^#(X)) , U32^#(mark(X1), X2) -> c_57(U32^#(X1, X2)) , U32^#(ok(X1), ok(X2)) -> c_58(U32^#(X1, X2)) , U33^#(mark(X)) -> c_59(U33^#(X)) , U33^#(ok(X)) -> c_60(U33^#(X)) , U41^#(mark(X1), X2) -> c_61(U41^#(X1, X2)) , U41^#(ok(X1), ok(X2)) -> c_62(U41^#(X1, X2)) , U51^#(mark(X1), X2, X3) -> c_63(U51^#(X1, X2, X3)) , U51^#(ok(X1), ok(X2), ok(X3)) -> c_64(U51^#(X1, X2, X3)) , s^#(mark(X)) -> c_65(s^#(X)) , s^#(ok(X)) -> c_66(s^#(X)) , plus^#(X1, mark(X2)) -> c_67(plus^#(X1, X2)) , plus^#(mark(X1), X2) -> c_68(plus^#(X1, X2)) , plus^#(ok(X1), ok(X2)) -> c_69(plus^#(X1, X2)) , U61^#(mark(X)) -> c_70(U61^#(X)) , U61^#(ok(X)) -> c_71(U61^#(X)) , U71^#(mark(X1), X2, X3) -> c_72(U71^#(X1, X2, X3)) , U71^#(ok(X1), ok(X2), ok(X3)) -> c_73(U71^#(X1, X2, X3)) , x^#(X1, mark(X2)) -> c_74(x^#(X1, X2)) , x^#(mark(X1), X2) -> c_75(x^#(X1, X2)) , x^#(ok(X1), ok(X2)) -> c_76(x^#(X1, X2)) , and^#(mark(X1), X2) -> c_77(and^#(X1, X2)) , and^#(ok(X1), ok(X2)) -> c_78(and^#(X1, X2)) , isNatKind^#(ok(X)) -> c_79(isNatKind^#(X)) , isNat^#(ok(X)) -> c_48(isNat^#(X)) , proper^#(tt()) -> c_81() , proper^#(0()) -> c_95() , top^#(mark(X)) -> c_100(top^#(proper(X))) , top^#(ok(X)) -> c_101(top^#(active(X))) } Strict Trs: { active(U11(X1, X2, X3)) -> U11(active(X1), X2, X3) , active(U11(tt(), V1, V2)) -> mark(U12(isNat(V1), V2)) , active(U12(X1, X2)) -> U12(active(X1), X2) , active(U12(tt(), V2)) -> mark(U13(isNat(V2))) , active(isNat(s(V1))) -> mark(U21(isNatKind(V1), V1)) , active(isNat(plus(V1, V2))) -> mark(U11(and(isNatKind(V1), isNatKind(V2)), V1, V2)) , active(isNat(0())) -> mark(tt()) , active(isNat(x(V1, V2))) -> mark(U31(and(isNatKind(V1), isNatKind(V2)), V1, V2)) , active(U13(X)) -> U13(active(X)) , active(U13(tt())) -> mark(tt()) , active(U21(X1, X2)) -> U21(active(X1), X2) , active(U21(tt(), V1)) -> mark(U22(isNat(V1))) , active(U22(X)) -> U22(active(X)) , active(U22(tt())) -> mark(tt()) , active(U31(X1, X2, X3)) -> U31(active(X1), X2, X3) , active(U31(tt(), V1, V2)) -> mark(U32(isNat(V1), V2)) , active(U32(X1, X2)) -> U32(active(X1), X2) , active(U32(tt(), V2)) -> mark(U33(isNat(V2))) , active(U33(X)) -> U33(active(X)) , active(U33(tt())) -> mark(tt()) , active(U41(X1, X2)) -> U41(active(X1), X2) , active(U41(tt(), N)) -> mark(N) , active(U51(X1, X2, X3)) -> U51(active(X1), X2, X3) , active(U51(tt(), M, N)) -> mark(s(plus(N, M))) , active(s(X)) -> s(active(X)) , active(plus(X1, X2)) -> plus(X1, active(X2)) , active(plus(X1, X2)) -> plus(active(X1), X2) , active(plus(N, s(M))) -> mark(U51(and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)) , active(plus(N, 0())) -> mark(U41(and(isNat(N), isNatKind(N)), N)) , active(U61(X)) -> U61(active(X)) , active(U61(tt())) -> mark(0()) , active(U71(X1, X2, X3)) -> U71(active(X1), X2, X3) , active(U71(tt(), M, N)) -> mark(plus(x(N, M), N)) , active(x(X1, X2)) -> x(X1, active(X2)) , active(x(X1, X2)) -> x(active(X1), X2) , active(x(N, s(M))) -> mark(U71(and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)) , active(x(N, 0())) -> mark(U61(and(isNat(N), isNatKind(N)))) , active(and(X1, X2)) -> and(active(X1), X2) , active(and(tt(), X)) -> mark(X) , active(isNatKind(s(V1))) -> mark(isNatKind(V1)) , active(isNatKind(plus(V1, V2))) -> mark(and(isNatKind(V1), isNatKind(V2))) , active(isNatKind(0())) -> mark(tt()) , active(isNatKind(x(V1, V2))) -> mark(and(isNatKind(V1), isNatKind(V2))) , U11(mark(X1), X2, X3) -> mark(U11(X1, X2, X3)) , U11(ok(X1), ok(X2), ok(X3)) -> ok(U11(X1, X2, X3)) , U12(mark(X1), X2) -> mark(U12(X1, X2)) , U12(ok(X1), ok(X2)) -> ok(U12(X1, X2)) , isNat(ok(X)) -> ok(isNat(X)) , U13(mark(X)) -> mark(U13(X)) , U13(ok(X)) -> ok(U13(X)) , U21(mark(X1), X2) -> mark(U21(X1, X2)) , U21(ok(X1), ok(X2)) -> ok(U21(X1, X2)) , U22(mark(X)) -> mark(U22(X)) , U22(ok(X)) -> ok(U22(X)) , U31(mark(X1), X2, X3) -> mark(U31(X1, X2, X3)) , U31(ok(X1), ok(X2), ok(X3)) -> ok(U31(X1, X2, X3)) , U32(mark(X1), X2) -> mark(U32(X1, X2)) , U32(ok(X1), ok(X2)) -> ok(U32(X1, X2)) , U33(mark(X)) -> mark(U33(X)) , U33(ok(X)) -> ok(U33(X)) , U41(mark(X1), X2) -> mark(U41(X1, X2)) , U41(ok(X1), ok(X2)) -> ok(U41(X1, X2)) , U51(mark(X1), X2, X3) -> mark(U51(X1, X2, X3)) , U51(ok(X1), ok(X2), ok(X3)) -> ok(U51(X1, X2, X3)) , s(mark(X)) -> mark(s(X)) , s(ok(X)) -> ok(s(X)) , plus(X1, mark(X2)) -> mark(plus(X1, X2)) , plus(mark(X1), X2) -> mark(plus(X1, X2)) , plus(ok(X1), ok(X2)) -> ok(plus(X1, X2)) , U61(mark(X)) -> mark(U61(X)) , U61(ok(X)) -> ok(U61(X)) , U71(mark(X1), X2, X3) -> mark(U71(X1, X2, X3)) , U71(ok(X1), ok(X2), ok(X3)) -> ok(U71(X1, X2, X3)) , x(X1, mark(X2)) -> mark(x(X1, X2)) , x(mark(X1), X2) -> mark(x(X1, X2)) , x(ok(X1), ok(X2)) -> ok(x(X1, X2)) , and(mark(X1), X2) -> mark(and(X1, X2)) , and(ok(X1), ok(X2)) -> ok(and(X1, X2)) , isNatKind(ok(X)) -> ok(isNatKind(X)) , proper(U11(X1, X2, X3)) -> U11(proper(X1), proper(X2), proper(X3)) , proper(tt()) -> ok(tt()) , proper(U12(X1, X2)) -> U12(proper(X1), proper(X2)) , proper(isNat(X)) -> isNat(proper(X)) , proper(U13(X)) -> U13(proper(X)) , proper(U21(X1, X2)) -> U21(proper(X1), proper(X2)) , proper(U22(X)) -> U22(proper(X)) , proper(U31(X1, X2, X3)) -> U31(proper(X1), proper(X2), proper(X3)) , proper(U32(X1, X2)) -> U32(proper(X1), proper(X2)) , proper(U33(X)) -> U33(proper(X)) , proper(U41(X1, X2)) -> U41(proper(X1), proper(X2)) , proper(U51(X1, X2, X3)) -> U51(proper(X1), proper(X2), proper(X3)) , proper(s(X)) -> s(proper(X)) , proper(plus(X1, X2)) -> plus(proper(X1), proper(X2)) , proper(U61(X)) -> U61(proper(X)) , proper(0()) -> ok(0()) , proper(U71(X1, X2, X3)) -> U71(proper(X1), proper(X2), proper(X3)) , proper(x(X1, X2)) -> x(proper(X1), proper(X2)) , proper(and(X1, X2)) -> and(proper(X1), proper(X2)) , proper(isNatKind(X)) -> isNatKind(proper(X)) , top(mark(X)) -> top(proper(X)) , top(ok(X)) -> top(active(X)) } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {37,38} by applications of Pre({37,38}) = {}. Here rules are labeled as follows: DPs: { 1: U11^#(mark(X1), X2, X3) -> c_44(U11^#(X1, X2, X3)) , 2: U11^#(ok(X1), ok(X2), ok(X3)) -> c_45(U11^#(X1, X2, X3)) , 3: U12^#(mark(X1), X2) -> c_46(U12^#(X1, X2)) , 4: U12^#(ok(X1), ok(X2)) -> c_47(U12^#(X1, X2)) , 5: U13^#(mark(X)) -> c_49(U13^#(X)) , 6: U13^#(ok(X)) -> c_50(U13^#(X)) , 7: U21^#(mark(X1), X2) -> c_51(U21^#(X1, X2)) , 8: U21^#(ok(X1), ok(X2)) -> c_52(U21^#(X1, X2)) , 9: U31^#(mark(X1), X2, X3) -> c_55(U31^#(X1, X2, X3)) , 10: U31^#(ok(X1), ok(X2), ok(X3)) -> c_56(U31^#(X1, X2, X3)) , 11: U22^#(mark(X)) -> c_53(U22^#(X)) , 12: U22^#(ok(X)) -> c_54(U22^#(X)) , 13: U32^#(mark(X1), X2) -> c_57(U32^#(X1, X2)) , 14: U32^#(ok(X1), ok(X2)) -> c_58(U32^#(X1, X2)) , 15: U33^#(mark(X)) -> c_59(U33^#(X)) , 16: U33^#(ok(X)) -> c_60(U33^#(X)) , 17: U41^#(mark(X1), X2) -> c_61(U41^#(X1, X2)) , 18: U41^#(ok(X1), ok(X2)) -> c_62(U41^#(X1, X2)) , 19: U51^#(mark(X1), X2, X3) -> c_63(U51^#(X1, X2, X3)) , 20: U51^#(ok(X1), ok(X2), ok(X3)) -> c_64(U51^#(X1, X2, X3)) , 21: s^#(mark(X)) -> c_65(s^#(X)) , 22: s^#(ok(X)) -> c_66(s^#(X)) , 23: plus^#(X1, mark(X2)) -> c_67(plus^#(X1, X2)) , 24: plus^#(mark(X1), X2) -> c_68(plus^#(X1, X2)) , 25: plus^#(ok(X1), ok(X2)) -> c_69(plus^#(X1, X2)) , 26: U61^#(mark(X)) -> c_70(U61^#(X)) , 27: U61^#(ok(X)) -> c_71(U61^#(X)) , 28: U71^#(mark(X1), X2, X3) -> c_72(U71^#(X1, X2, X3)) , 29: U71^#(ok(X1), ok(X2), ok(X3)) -> c_73(U71^#(X1, X2, X3)) , 30: x^#(X1, mark(X2)) -> c_74(x^#(X1, X2)) , 31: x^#(mark(X1), X2) -> c_75(x^#(X1, X2)) , 32: x^#(ok(X1), ok(X2)) -> c_76(x^#(X1, X2)) , 33: and^#(mark(X1), X2) -> c_77(and^#(X1, X2)) , 34: and^#(ok(X1), ok(X2)) -> c_78(and^#(X1, X2)) , 35: isNatKind^#(ok(X)) -> c_79(isNatKind^#(X)) , 36: isNat^#(ok(X)) -> c_48(isNat^#(X)) , 37: proper^#(tt()) -> c_81() , 38: proper^#(0()) -> c_95() , 39: top^#(mark(X)) -> c_100(top^#(proper(X))) , 40: top^#(ok(X)) -> c_101(top^#(active(X))) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { U11^#(mark(X1), X2, X3) -> c_44(U11^#(X1, X2, X3)) , U11^#(ok(X1), ok(X2), ok(X3)) -> c_45(U11^#(X1, X2, X3)) , U12^#(mark(X1), X2) -> c_46(U12^#(X1, X2)) , U12^#(ok(X1), ok(X2)) -> c_47(U12^#(X1, X2)) , U13^#(mark(X)) -> c_49(U13^#(X)) , U13^#(ok(X)) -> c_50(U13^#(X)) , U21^#(mark(X1), X2) -> c_51(U21^#(X1, X2)) , U21^#(ok(X1), ok(X2)) -> c_52(U21^#(X1, X2)) , U31^#(mark(X1), X2, X3) -> c_55(U31^#(X1, X2, X3)) , U31^#(ok(X1), ok(X2), ok(X3)) -> c_56(U31^#(X1, X2, X3)) , U22^#(mark(X)) -> c_53(U22^#(X)) , U22^#(ok(X)) -> c_54(U22^#(X)) , U32^#(mark(X1), X2) -> c_57(U32^#(X1, X2)) , U32^#(ok(X1), ok(X2)) -> c_58(U32^#(X1, X2)) , U33^#(mark(X)) -> c_59(U33^#(X)) , U33^#(ok(X)) -> c_60(U33^#(X)) , U41^#(mark(X1), X2) -> c_61(U41^#(X1, X2)) , U41^#(ok(X1), ok(X2)) -> c_62(U41^#(X1, X2)) , U51^#(mark(X1), X2, X3) -> c_63(U51^#(X1, X2, X3)) , U51^#(ok(X1), ok(X2), ok(X3)) -> c_64(U51^#(X1, X2, X3)) , s^#(mark(X)) -> c_65(s^#(X)) , s^#(ok(X)) -> c_66(s^#(X)) , plus^#(X1, mark(X2)) -> c_67(plus^#(X1, X2)) , plus^#(mark(X1), X2) -> c_68(plus^#(X1, X2)) , plus^#(ok(X1), ok(X2)) -> c_69(plus^#(X1, X2)) , U61^#(mark(X)) -> c_70(U61^#(X)) , U61^#(ok(X)) -> c_71(U61^#(X)) , U71^#(mark(X1), X2, X3) -> c_72(U71^#(X1, X2, X3)) , U71^#(ok(X1), ok(X2), ok(X3)) -> c_73(U71^#(X1, X2, X3)) , x^#(X1, mark(X2)) -> c_74(x^#(X1, X2)) , x^#(mark(X1), X2) -> c_75(x^#(X1, X2)) , x^#(ok(X1), ok(X2)) -> c_76(x^#(X1, X2)) , and^#(mark(X1), X2) -> c_77(and^#(X1, X2)) , and^#(ok(X1), ok(X2)) -> c_78(and^#(X1, X2)) , isNatKind^#(ok(X)) -> c_79(isNatKind^#(X)) , isNat^#(ok(X)) -> c_48(isNat^#(X)) , top^#(mark(X)) -> c_100(top^#(proper(X))) , top^#(ok(X)) -> c_101(top^#(active(X))) } Strict Trs: { active(U11(X1, X2, X3)) -> U11(active(X1), X2, X3) , active(U11(tt(), V1, V2)) -> mark(U12(isNat(V1), V2)) , active(U12(X1, X2)) -> U12(active(X1), X2) , active(U12(tt(), V2)) -> mark(U13(isNat(V2))) , active(isNat(s(V1))) -> mark(U21(isNatKind(V1), V1)) , active(isNat(plus(V1, V2))) -> mark(U11(and(isNatKind(V1), isNatKind(V2)), V1, V2)) , active(isNat(0())) -> mark(tt()) , active(isNat(x(V1, V2))) -> mark(U31(and(isNatKind(V1), isNatKind(V2)), V1, V2)) , active(U13(X)) -> U13(active(X)) , active(U13(tt())) -> mark(tt()) , active(U21(X1, X2)) -> U21(active(X1), X2) , active(U21(tt(), V1)) -> mark(U22(isNat(V1))) , active(U22(X)) -> U22(active(X)) , active(U22(tt())) -> mark(tt()) , active(U31(X1, X2, X3)) -> U31(active(X1), X2, X3) , active(U31(tt(), V1, V2)) -> mark(U32(isNat(V1), V2)) , active(U32(X1, X2)) -> U32(active(X1), X2) , active(U32(tt(), V2)) -> mark(U33(isNat(V2))) , active(U33(X)) -> U33(active(X)) , active(U33(tt())) -> mark(tt()) , active(U41(X1, X2)) -> U41(active(X1), X2) , active(U41(tt(), N)) -> mark(N) , active(U51(X1, X2, X3)) -> U51(active(X1), X2, X3) , active(U51(tt(), M, N)) -> mark(s(plus(N, M))) , active(s(X)) -> s(active(X)) , active(plus(X1, X2)) -> plus(X1, active(X2)) , active(plus(X1, X2)) -> plus(active(X1), X2) , active(plus(N, s(M))) -> mark(U51(and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)) , active(plus(N, 0())) -> mark(U41(and(isNat(N), isNatKind(N)), N)) , active(U61(X)) -> U61(active(X)) , active(U61(tt())) -> mark(0()) , active(U71(X1, X2, X3)) -> U71(active(X1), X2, X3) , active(U71(tt(), M, N)) -> mark(plus(x(N, M), N)) , active(x(X1, X2)) -> x(X1, active(X2)) , active(x(X1, X2)) -> x(active(X1), X2) , active(x(N, s(M))) -> mark(U71(and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)) , active(x(N, 0())) -> mark(U61(and(isNat(N), isNatKind(N)))) , active(and(X1, X2)) -> and(active(X1), X2) , active(and(tt(), X)) -> mark(X) , active(isNatKind(s(V1))) -> mark(isNatKind(V1)) , active(isNatKind(plus(V1, V2))) -> mark(and(isNatKind(V1), isNatKind(V2))) , active(isNatKind(0())) -> mark(tt()) , active(isNatKind(x(V1, V2))) -> mark(and(isNatKind(V1), isNatKind(V2))) , U11(mark(X1), X2, X3) -> mark(U11(X1, X2, X3)) , U11(ok(X1), ok(X2), ok(X3)) -> ok(U11(X1, X2, X3)) , U12(mark(X1), X2) -> mark(U12(X1, X2)) , U12(ok(X1), ok(X2)) -> ok(U12(X1, X2)) , isNat(ok(X)) -> ok(isNat(X)) , U13(mark(X)) -> mark(U13(X)) , U13(ok(X)) -> ok(U13(X)) , U21(mark(X1), X2) -> mark(U21(X1, X2)) , U21(ok(X1), ok(X2)) -> ok(U21(X1, X2)) , U22(mark(X)) -> mark(U22(X)) , U22(ok(X)) -> ok(U22(X)) , U31(mark(X1), X2, X3) -> mark(U31(X1, X2, X3)) , U31(ok(X1), ok(X2), ok(X3)) -> ok(U31(X1, X2, X3)) , U32(mark(X1), X2) -> mark(U32(X1, X2)) , U32(ok(X1), ok(X2)) -> ok(U32(X1, X2)) , U33(mark(X)) -> mark(U33(X)) , U33(ok(X)) -> ok(U33(X)) , U41(mark(X1), X2) -> mark(U41(X1, X2)) , U41(ok(X1), ok(X2)) -> ok(U41(X1, X2)) , U51(mark(X1), X2, X3) -> mark(U51(X1, X2, X3)) , U51(ok(X1), ok(X2), ok(X3)) -> ok(U51(X1, X2, X3)) , s(mark(X)) -> mark(s(X)) , s(ok(X)) -> ok(s(X)) , plus(X1, mark(X2)) -> mark(plus(X1, X2)) , plus(mark(X1), X2) -> mark(plus(X1, X2)) , plus(ok(X1), ok(X2)) -> ok(plus(X1, X2)) , U61(mark(X)) -> mark(U61(X)) , U61(ok(X)) -> ok(U61(X)) , U71(mark(X1), X2, X3) -> mark(U71(X1, X2, X3)) , U71(ok(X1), ok(X2), ok(X3)) -> ok(U71(X1, X2, X3)) , x(X1, mark(X2)) -> mark(x(X1, X2)) , x(mark(X1), X2) -> mark(x(X1, X2)) , x(ok(X1), ok(X2)) -> ok(x(X1, X2)) , and(mark(X1), X2) -> mark(and(X1, X2)) , and(ok(X1), ok(X2)) -> ok(and(X1, X2)) , isNatKind(ok(X)) -> ok(isNatKind(X)) , proper(U11(X1, X2, X3)) -> U11(proper(X1), proper(X2), proper(X3)) , proper(tt()) -> ok(tt()) , proper(U12(X1, X2)) -> U12(proper(X1), proper(X2)) , proper(isNat(X)) -> isNat(proper(X)) , proper(U13(X)) -> U13(proper(X)) , proper(U21(X1, X2)) -> U21(proper(X1), proper(X2)) , proper(U22(X)) -> U22(proper(X)) , proper(U31(X1, X2, X3)) -> U31(proper(X1), proper(X2), proper(X3)) , proper(U32(X1, X2)) -> U32(proper(X1), proper(X2)) , proper(U33(X)) -> U33(proper(X)) , proper(U41(X1, X2)) -> U41(proper(X1), proper(X2)) , proper(U51(X1, X2, X3)) -> U51(proper(X1), proper(X2), proper(X3)) , proper(s(X)) -> s(proper(X)) , proper(plus(X1, X2)) -> plus(proper(X1), proper(X2)) , proper(U61(X)) -> U61(proper(X)) , proper(0()) -> ok(0()) , proper(U71(X1, X2, X3)) -> U71(proper(X1), proper(X2), proper(X3)) , proper(x(X1, X2)) -> x(proper(X1), proper(X2)) , proper(and(X1, X2)) -> and(proper(X1), proper(X2)) , proper(isNatKind(X)) -> isNatKind(proper(X)) , top(mark(X)) -> top(proper(X)) , top(ok(X)) -> top(active(X)) } Weak DPs: { proper^#(tt()) -> c_81() , proper^#(0()) -> c_95() } Obligation: runtime complexity Answer: MAYBE Empty strict component of the problem is NOT empty. Arrrr..