MAYBE TRS: { a__U12(X1, X2) -> U12(X1, X2), a__U12(tt(), V2) -> a__U13(a__isNat(V2)), a__isNat(X) -> isNat(X), a__isNat(s(V1)) -> a__U21(a__isNatKind(V1), V1), a__isNat(0()) -> tt(), a__isNat(plus(V1, V2)) -> a__U11(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2), a__isNat(x(V1, V2)) -> a__U31(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2), a__U11(X1, X2, X3) -> U11(X1, X2, X3), a__U11(tt(), V1, V2) -> a__U12(a__isNat(V1), V2), a__U13(X) -> U13(X), a__U13(tt()) -> tt(), a__U22(X) -> U22(X), a__U22(tt()) -> tt(), a__U21(X1, X2) -> U21(X1, X2), a__U21(tt(), V1) -> a__U22(a__isNat(V1)), a__U32(X1, X2) -> U32(X1, X2), a__U32(tt(), V2) -> a__U33(a__isNat(V2)), a__U31(X1, X2, X3) -> U31(X1, X2, X3), a__U31(tt(), V1, V2) -> a__U32(a__isNat(V1), V2), a__U33(X) -> U33(X), a__U33(tt()) -> tt(), mark(tt()) -> tt(), mark(s(X)) -> s(mark(X)), mark(0()) -> 0(), mark(isNatKind(X)) -> a__isNatKind(X), mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)), mark(x(X1, X2)) -> a__x(mark(X1), mark(X2)), mark(and(X1, X2)) -> a__and(mark(X1), X2), mark(isNat(X)) -> a__isNat(X), mark(U11(X1, X2, X3)) -> a__U11(mark(X1), X2, X3), mark(U12(X1, X2)) -> a__U12(mark(X1), X2), mark(U13(X)) -> a__U13(mark(X)), mark(U21(X1, X2)) -> a__U21(mark(X1), X2), mark(U22(X)) -> a__U22(mark(X)), mark(U31(X1, X2, X3)) -> a__U31(mark(X1), X2, X3), mark(U32(X1, X2)) -> a__U32(mark(X1), X2), mark(U33(X)) -> a__U33(mark(X)), mark(U41(X1, X2)) -> a__U41(mark(X1), X2), mark(U51(X1, X2, X3)) -> a__U51(mark(X1), X2, X3), mark(U61(X)) -> a__U61(mark(X)), mark(U71(X1, X2, X3)) -> a__U71(mark(X1), X2, X3), a__U41(X1, X2) -> U41(X1, X2), a__U41(tt(), N) -> mark(N), a__plus(N, s(M)) -> a__U51(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N), a__plus(N, 0()) -> a__U41(a__and(a__isNat(N), isNatKind(N)), N), a__plus(X1, X2) -> plus(X1, X2), a__U51(X1, X2, X3) -> U51(X1, X2, X3), a__U51(tt(), M, N) -> s(a__plus(mark(N), mark(M))), a__U61(X) -> U61(X), a__U61(tt()) -> 0(), a__x(N, s(M)) -> a__U71(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N), a__x(N, 0()) -> a__U61(a__and(a__isNat(N), isNatKind(N))), a__x(X1, X2) -> x(X1, X2), a__U71(X1, X2, X3) -> U71(X1, X2, X3), a__U71(tt(), M, N) -> a__plus(a__x(mark(N), mark(M)), mark(N)), a__and(X1, X2) -> and(X1, X2), a__and(tt(), X) -> mark(X), a__isNatKind(X) -> isNatKind(X), a__isNatKind(s(V1)) -> a__isNatKind(V1), a__isNatKind(0()) -> tt(), a__isNatKind(plus(V1, V2)) -> a__and(a__isNatKind(V1), isNatKind(V2)), a__isNatKind(x(V1, V2)) -> a__and(a__isNatKind(V1), isNatKind(V2))} DP: Strict: { a__U12#(tt(), V2) -> a__isNat#(V2), a__U12#(tt(), V2) -> a__U13#(a__isNat(V2)), a__isNat#(s(V1)) -> a__U21#(a__isNatKind(V1), V1), a__isNat#(s(V1)) -> a__isNatKind#(V1), a__isNat#(plus(V1, V2)) -> a__U11#(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2), a__isNat#(plus(V1, V2)) -> a__and#(a__isNatKind(V1), isNatKind(V2)), a__isNat#(plus(V1, V2)) -> a__isNatKind#(V1), a__isNat#(x(V1, V2)) -> a__U31#(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2), a__isNat#(x(V1, V2)) -> a__and#(a__isNatKind(V1), isNatKind(V2)), a__isNat#(x(V1, V2)) -> a__isNatKind#(V1), a__U11#(tt(), V1, V2) -> a__U12#(a__isNat(V1), V2), a__U11#(tt(), V1, V2) -> a__isNat#(V1), a__U21#(tt(), V1) -> a__isNat#(V1), a__U21#(tt(), V1) -> a__U22#(a__isNat(V1)), a__U32#(tt(), V2) -> a__isNat#(V2), a__U32#(tt(), V2) -> a__U33#(a__isNat(V2)), a__U31#(tt(), V1, V2) -> a__isNat#(V1), a__U31#(tt(), V1, V2) -> a__U32#(a__isNat(V1), V2), mark#(s(X)) -> mark#(X), mark#(isNatKind(X)) -> a__isNatKind#(X), mark#(plus(X1, X2)) -> mark#(X1), mark#(plus(X1, X2)) -> mark#(X2), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)), mark#(x(X1, X2)) -> mark#(X1), mark#(x(X1, X2)) -> mark#(X2), mark#(x(X1, X2)) -> a__x#(mark(X1), mark(X2)), mark#(and(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), X2), mark#(isNat(X)) -> a__isNat#(X), mark#(U11(X1, X2, X3)) -> a__U11#(mark(X1), X2, X3), mark#(U11(X1, X2, X3)) -> mark#(X1), mark#(U12(X1, X2)) -> a__U12#(mark(X1), X2), mark#(U12(X1, X2)) -> mark#(X1), mark#(U13(X)) -> a__U13#(mark(X)), mark#(U13(X)) -> mark#(X), mark#(U21(X1, X2)) -> a__U21#(mark(X1), X2), mark#(U21(X1, X2)) -> mark#(X1), mark#(U22(X)) -> a__U22#(mark(X)), mark#(U22(X)) -> mark#(X), mark#(U31(X1, X2, X3)) -> a__U31#(mark(X1), X2, X3), mark#(U31(X1, X2, X3)) -> mark#(X1), mark#(U32(X1, X2)) -> a__U32#(mark(X1), X2), mark#(U32(X1, X2)) -> mark#(X1), mark#(U33(X)) -> a__U33#(mark(X)), mark#(U33(X)) -> mark#(X), mark#(U41(X1, X2)) -> mark#(X1), mark#(U41(X1, X2)) -> a__U41#(mark(X1), X2), mark#(U51(X1, X2, X3)) -> mark#(X1), mark#(U51(X1, X2, X3)) -> a__U51#(mark(X1), X2, X3), mark#(U61(X)) -> mark#(X), mark#(U61(X)) -> a__U61#(mark(X)), mark#(U71(X1, X2, X3)) -> mark#(X1), mark#(U71(X1, X2, X3)) -> a__U71#(mark(X1), X2, X3), a__U41#(tt(), N) -> mark#(N), a__plus#(N, s(M)) -> a__isNat#(M), a__plus#(N, s(M)) -> a__U51#(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N), a__plus#(N, s(M)) -> a__and#(a__isNat(M), isNatKind(M)), a__plus#(N, s(M)) -> a__and#(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), a__plus#(N, 0()) -> a__isNat#(N), a__plus#(N, 0()) -> a__U41#(a__and(a__isNat(N), isNatKind(N)), N), a__plus#(N, 0()) -> a__and#(a__isNat(N), isNatKind(N)), a__U51#(tt(), M, N) -> mark#(N), a__U51#(tt(), M, N) -> mark#(M), a__U51#(tt(), M, N) -> a__plus#(mark(N), mark(M)), a__x#(N, s(M)) -> a__isNat#(M), a__x#(N, s(M)) -> a__U71#(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N), a__x#(N, s(M)) -> a__and#(a__isNat(M), isNatKind(M)), a__x#(N, s(M)) -> a__and#(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), a__x#(N, 0()) -> a__isNat#(N), a__x#(N, 0()) -> a__U61#(a__and(a__isNat(N), isNatKind(N))), a__x#(N, 0()) -> a__and#(a__isNat(N), isNatKind(N)), a__U71#(tt(), M, N) -> mark#(N), a__U71#(tt(), M, N) -> mark#(M), a__U71#(tt(), M, N) -> a__plus#(a__x(mark(N), mark(M)), mark(N)), a__U71#(tt(), M, N) -> a__x#(mark(N), mark(M)), a__and#(tt(), X) -> mark#(X), a__isNatKind#(s(V1)) -> a__isNatKind#(V1), a__isNatKind#(plus(V1, V2)) -> a__and#(a__isNatKind(V1), isNatKind(V2)), a__isNatKind#(plus(V1, V2)) -> a__isNatKind#(V1), a__isNatKind#(x(V1, V2)) -> a__and#(a__isNatKind(V1), isNatKind(V2)), a__isNatKind#(x(V1, V2)) -> a__isNatKind#(V1)} Weak: { a__U12(X1, X2) -> U12(X1, X2), a__U12(tt(), V2) -> a__U13(a__isNat(V2)), a__isNat(X) -> isNat(X), a__isNat(s(V1)) -> a__U21(a__isNatKind(V1), V1), a__isNat(0()) -> tt(), a__isNat(plus(V1, V2)) -> a__U11(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2), a__isNat(x(V1, V2)) -> a__U31(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2), a__U11(X1, X2, X3) -> U11(X1, X2, X3), a__U11(tt(), V1, V2) -> a__U12(a__isNat(V1), V2), a__U13(X) -> U13(X), a__U13(tt()) -> tt(), a__U22(X) -> U22(X), a__U22(tt()) -> tt(), a__U21(X1, X2) -> U21(X1, X2), a__U21(tt(), V1) -> a__U22(a__isNat(V1)), a__U32(X1, X2) -> U32(X1, X2), a__U32(tt(), V2) -> a__U33(a__isNat(V2)), a__U31(X1, X2, X3) -> U31(X1, X2, X3), a__U31(tt(), V1, V2) -> a__U32(a__isNat(V1), V2), a__U33(X) -> U33(X), a__U33(tt()) -> tt(), mark(tt()) -> tt(), mark(s(X)) -> s(mark(X)), mark(0()) -> 0(), mark(isNatKind(X)) -> a__isNatKind(X), mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)), mark(x(X1, X2)) -> a__x(mark(X1), mark(X2)), mark(and(X1, X2)) -> a__and(mark(X1), X2), mark(isNat(X)) -> a__isNat(X), mark(U11(X1, X2, X3)) -> a__U11(mark(X1), X2, X3), mark(U12(X1, X2)) -> a__U12(mark(X1), X2), mark(U13(X)) -> a__U13(mark(X)), mark(U21(X1, X2)) -> a__U21(mark(X1), X2), mark(U22(X)) -> a__U22(mark(X)), mark(U31(X1, X2, X3)) -> a__U31(mark(X1), X2, X3), mark(U32(X1, X2)) -> a__U32(mark(X1), X2), mark(U33(X)) -> a__U33(mark(X)), mark(U41(X1, X2)) -> a__U41(mark(X1), X2), mark(U51(X1, X2, X3)) -> a__U51(mark(X1), X2, X3), mark(U61(X)) -> a__U61(mark(X)), mark(U71(X1, X2, X3)) -> a__U71(mark(X1), X2, X3), a__U41(X1, X2) -> U41(X1, X2), a__U41(tt(), N) -> mark(N), a__plus(N, s(M)) -> a__U51(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N), a__plus(N, 0()) -> a__U41(a__and(a__isNat(N), isNatKind(N)), N), a__plus(X1, X2) -> plus(X1, X2), a__U51(X1, X2, X3) -> U51(X1, X2, X3), a__U51(tt(), M, N) -> s(a__plus(mark(N), mark(M))), a__U61(X) -> U61(X), a__U61(tt()) -> 0(), a__x(N, s(M)) -> a__U71(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N), a__x(N, 0()) -> a__U61(a__and(a__isNat(N), isNatKind(N))), a__x(X1, X2) -> x(X1, X2), a__U71(X1, X2, X3) -> U71(X1, X2, X3), a__U71(tt(), M, N) -> a__plus(a__x(mark(N), mark(M)), mark(N)), a__and(X1, X2) -> and(X1, X2), a__and(tt(), X) -> mark(X), a__isNatKind(X) -> isNatKind(X), a__isNatKind(s(V1)) -> a__isNatKind(V1), a__isNatKind(0()) -> tt(), a__isNatKind(plus(V1, V2)) -> a__and(a__isNatKind(V1), isNatKind(V2)), a__isNatKind(x(V1, V2)) -> a__and(a__isNatKind(V1), isNatKind(V2))} EDG: { (a__x#(N, s(M)) -> a__U71#(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N), a__U71#(tt(), M, N) -> a__x#(mark(N), mark(M))) (a__x#(N, s(M)) -> a__U71#(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N), a__U71#(tt(), M, N) -> a__plus#(a__x(mark(N), mark(M)), mark(N))) (a__x#(N, s(M)) -> a__U71#(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N), a__U71#(tt(), M, N) -> mark#(M)) (a__x#(N, s(M)) -> a__U71#(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N), a__U71#(tt(), M, N) -> mark#(N)) (a__U32#(tt(), V2) -> a__isNat#(V2), a__isNat#(x(V1, V2)) -> a__isNatKind#(V1)) (a__U32#(tt(), V2) -> a__isNat#(V2), a__isNat#(x(V1, V2)) -> a__and#(a__isNatKind(V1), isNatKind(V2))) (a__U32#(tt(), V2) -> a__isNat#(V2), a__isNat#(x(V1, V2)) -> a__U31#(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)) (a__U32#(tt(), V2) -> a__isNat#(V2), a__isNat#(plus(V1, V2)) -> a__isNatKind#(V1)) (a__U32#(tt(), V2) -> a__isNat#(V2), a__isNat#(plus(V1, V2)) -> a__and#(a__isNatKind(V1), isNatKind(V2))) (a__U32#(tt(), V2) -> a__isNat#(V2), a__isNat#(plus(V1, V2)) -> a__U11#(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)) (a__U32#(tt(), V2) -> a__isNat#(V2), a__isNat#(s(V1)) -> a__isNatKind#(V1)) (a__U32#(tt(), V2) -> a__isNat#(V2), a__isNat#(s(V1)) -> a__U21#(a__isNatKind(V1), V1)) (a__plus#(N, s(M)) -> a__isNat#(M), a__isNat#(x(V1, V2)) -> a__isNatKind#(V1)) (a__plus#(N, s(M)) -> a__isNat#(M), a__isNat#(x(V1, V2)) -> a__and#(a__isNatKind(V1), isNatKind(V2))) (a__plus#(N, s(M)) -> a__isNat#(M), a__isNat#(x(V1, V2)) -> a__U31#(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)) (a__plus#(N, s(M)) -> a__isNat#(M), a__isNat#(plus(V1, V2)) -> a__isNatKind#(V1)) (a__plus#(N, s(M)) -> a__isNat#(M), a__isNat#(plus(V1, V2)) -> a__and#(a__isNatKind(V1), isNatKind(V2))) (a__plus#(N, s(M)) -> a__isNat#(M), a__isNat#(plus(V1, V2)) -> a__U11#(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)) (a__plus#(N, s(M)) -> a__isNat#(M), a__isNat#(s(V1)) -> a__isNatKind#(V1)) (a__plus#(N, s(M)) -> a__isNat#(M), a__isNat#(s(V1)) -> a__U21#(a__isNatKind(V1), V1)) (a__x#(N, s(M)) -> a__isNat#(M), a__isNat#(x(V1, V2)) -> a__isNatKind#(V1)) (a__x#(N, s(M)) -> a__isNat#(M), a__isNat#(x(V1, V2)) -> a__and#(a__isNatKind(V1), isNatKind(V2))) (a__x#(N, s(M)) -> a__isNat#(M), a__isNat#(x(V1, V2)) -> a__U31#(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)) (a__x#(N, s(M)) -> a__isNat#(M), a__isNat#(plus(V1, V2)) -> a__isNatKind#(V1)) (a__x#(N, s(M)) -> a__isNat#(M), a__isNat#(plus(V1, V2)) -> a__and#(a__isNatKind(V1), isNatKind(V2))) (a__x#(N, s(M)) -> a__isNat#(M), a__isNat#(plus(V1, V2)) -> a__U11#(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)) (a__x#(N, s(M)) -> a__isNat#(M), a__isNat#(s(V1)) -> a__isNatKind#(V1)) (a__x#(N, s(M)) -> a__isNat#(M), a__isNat#(s(V1)) -> a__U21#(a__isNatKind(V1), V1)) (a__isNat#(s(V1)) -> a__U21#(a__isNatKind(V1), V1), a__U21#(tt(), V1) -> a__U22#(a__isNat(V1))) (a__isNat#(s(V1)) -> a__U21#(a__isNatKind(V1), V1), a__U21#(tt(), V1) -> a__isNat#(V1)) (a__isNat#(x(V1, V2)) -> a__U31#(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2), a__U31#(tt(), V1, V2) -> a__U32#(a__isNat(V1), V2)) (a__isNat#(x(V1, V2)) -> a__U31#(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2), a__U31#(tt(), V1, V2) -> a__isNat#(V1)) (mark#(x(X1, X2)) -> mark#(X1), mark#(U71(X1, X2, X3)) -> a__U71#(mark(X1), X2, X3)) (mark#(x(X1, X2)) -> mark#(X1), mark#(U71(X1, X2, X3)) -> mark#(X1)) (mark#(x(X1, X2)) -> mark#(X1), mark#(U61(X)) -> a__U61#(mark(X))) (mark#(x(X1, X2)) -> mark#(X1), mark#(U61(X)) -> mark#(X)) (mark#(x(X1, X2)) -> mark#(X1), mark#(U51(X1, X2, X3)) -> a__U51#(mark(X1), X2, X3)) (mark#(x(X1, X2)) -> mark#(X1), mark#(U51(X1, X2, X3)) -> mark#(X1)) (mark#(x(X1, X2)) -> mark#(X1), mark#(U41(X1, X2)) -> a__U41#(mark(X1), X2)) (mark#(x(X1, X2)) -> mark#(X1), mark#(U41(X1, X2)) -> mark#(X1)) (mark#(x(X1, X2)) -> mark#(X1), mark#(U33(X)) -> mark#(X)) (mark#(x(X1, X2)) -> mark#(X1), mark#(U33(X)) -> a__U33#(mark(X))) (mark#(x(X1, X2)) -> mark#(X1), mark#(U32(X1, X2)) -> mark#(X1)) (mark#(x(X1, X2)) -> mark#(X1), mark#(U32(X1, X2)) -> a__U32#(mark(X1), X2)) (mark#(x(X1, X2)) -> mark#(X1), mark#(U31(X1, X2, X3)) -> mark#(X1)) (mark#(x(X1, X2)) -> mark#(X1), mark#(U31(X1, X2, X3)) -> a__U31#(mark(X1), X2, X3)) (mark#(x(X1, X2)) -> mark#(X1), mark#(U22(X)) -> mark#(X)) (mark#(x(X1, X2)) -> mark#(X1), mark#(U22(X)) -> a__U22#(mark(X))) (mark#(x(X1, X2)) -> mark#(X1), mark#(U21(X1, X2)) -> mark#(X1)) (mark#(x(X1, X2)) -> mark#(X1), mark#(U21(X1, X2)) -> a__U21#(mark(X1), X2)) (mark#(x(X1, X2)) -> mark#(X1), mark#(U13(X)) -> mark#(X)) (mark#(x(X1, X2)) -> mark#(X1), mark#(U13(X)) -> a__U13#(mark(X))) (mark#(x(X1, X2)) -> mark#(X1), mark#(U12(X1, X2)) -> mark#(X1)) (mark#(x(X1, X2)) -> mark#(X1), mark#(U12(X1, X2)) -> a__U12#(mark(X1), X2)) (mark#(x(X1, X2)) -> mark#(X1), mark#(U11(X1, X2, X3)) -> mark#(X1)) (mark#(x(X1, X2)) -> mark#(X1), mark#(U11(X1, X2, X3)) -> a__U11#(mark(X1), X2, X3)) (mark#(x(X1, X2)) -> mark#(X1), mark#(isNat(X)) -> a__isNat#(X)) (mark#(x(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), X2)) (mark#(x(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X1)) (mark#(x(X1, X2)) -> mark#(X1), mark#(x(X1, X2)) -> a__x#(mark(X1), mark(X2))) (mark#(x(X1, X2)) -> mark#(X1), mark#(x(X1, X2)) -> mark#(X2)) (mark#(x(X1, X2)) -> mark#(X1), mark#(x(X1, X2)) -> mark#(X1)) (mark#(x(X1, X2)) -> mark#(X1), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2))) (mark#(x(X1, X2)) -> mark#(X1), mark#(plus(X1, X2)) -> mark#(X2)) (mark#(x(X1, X2)) -> mark#(X1), mark#(plus(X1, X2)) -> mark#(X1)) (mark#(x(X1, X2)) -> mark#(X1), mark#(isNatKind(X)) -> a__isNatKind#(X)) (mark#(x(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X)) (mark#(U11(X1, X2, X3)) -> mark#(X1), mark#(U71(X1, X2, X3)) -> a__U71#(mark(X1), X2, X3)) (mark#(U11(X1, X2, X3)) -> mark#(X1), mark#(U71(X1, X2, X3)) -> mark#(X1)) (mark#(U11(X1, X2, X3)) -> mark#(X1), mark#(U61(X)) -> a__U61#(mark(X))) (mark#(U11(X1, X2, X3)) -> mark#(X1), mark#(U61(X)) -> mark#(X)) (mark#(U11(X1, X2, X3)) -> mark#(X1), mark#(U51(X1, X2, X3)) -> a__U51#(mark(X1), X2, X3)) (mark#(U11(X1, X2, X3)) -> mark#(X1), mark#(U51(X1, X2, X3)) -> mark#(X1)) (mark#(U11(X1, X2, X3)) -> mark#(X1), mark#(U41(X1, X2)) -> a__U41#(mark(X1), X2)) (mark#(U11(X1, X2, X3)) -> mark#(X1), mark#(U41(X1, X2)) -> mark#(X1)) (mark#(U11(X1, X2, X3)) -> mark#(X1), mark#(U33(X)) -> mark#(X)) (mark#(U11(X1, X2, X3)) -> mark#(X1), mark#(U33(X)) -> a__U33#(mark(X))) (mark#(U11(X1, X2, X3)) -> mark#(X1), mark#(U32(X1, X2)) -> mark#(X1)) (mark#(U11(X1, X2, X3)) -> mark#(X1), mark#(U32(X1, X2)) -> a__U32#(mark(X1), X2)) (mark#(U11(X1, X2, X3)) -> mark#(X1), mark#(U31(X1, X2, X3)) -> mark#(X1)) (mark#(U11(X1, X2, X3)) -> mark#(X1), mark#(U31(X1, X2, X3)) -> a__U31#(mark(X1), X2, X3)) (mark#(U11(X1, X2, X3)) -> mark#(X1), mark#(U22(X)) -> mark#(X)) (mark#(U11(X1, X2, X3)) -> mark#(X1), mark#(U22(X)) -> a__U22#(mark(X))) (mark#(U11(X1, X2, X3)) -> mark#(X1), mark#(U21(X1, X2)) -> mark#(X1)) (mark#(U11(X1, X2, X3)) -> mark#(X1), mark#(U21(X1, X2)) -> a__U21#(mark(X1), X2)) (mark#(U11(X1, X2, X3)) -> mark#(X1), mark#(U13(X)) -> mark#(X)) (mark#(U11(X1, X2, X3)) -> mark#(X1), mark#(U13(X)) -> a__U13#(mark(X))) (mark#(U11(X1, X2, X3)) -> mark#(X1), mark#(U12(X1, X2)) -> mark#(X1)) (mark#(U11(X1, X2, X3)) -> mark#(X1), mark#(U12(X1, X2)) -> a__U12#(mark(X1), X2)) (mark#(U11(X1, X2, X3)) -> mark#(X1), mark#(U11(X1, X2, X3)) -> mark#(X1)) (mark#(U11(X1, X2, X3)) -> mark#(X1), mark#(U11(X1, X2, X3)) -> a__U11#(mark(X1), X2, X3)) (mark#(U11(X1, X2, X3)) -> mark#(X1), mark#(isNat(X)) -> a__isNat#(X)) (mark#(U11(X1, X2, X3)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), X2)) (mark#(U11(X1, X2, X3)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X1)) (mark#(U11(X1, X2, X3)) -> mark#(X1), mark#(x(X1, X2)) -> a__x#(mark(X1), mark(X2))) (mark#(U11(X1, X2, X3)) -> mark#(X1), mark#(x(X1, X2)) -> mark#(X2)) (mark#(U11(X1, X2, X3)) -> mark#(X1), mark#(x(X1, X2)) -> mark#(X1)) (mark#(U11(X1, X2, X3)) -> mark#(X1), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2))) (mark#(U11(X1, X2, X3)) -> mark#(X1), mark#(plus(X1, X2)) -> mark#(X2)) (mark#(U11(X1, X2, X3)) -> mark#(X1), mark#(plus(X1, X2)) -> mark#(X1)) (mark#(U11(X1, X2, X3)) -> mark#(X1), mark#(isNatKind(X)) -> a__isNatKind#(X)) (mark#(U11(X1, X2, X3)) -> mark#(X1), mark#(s(X)) -> mark#(X)) (mark#(U21(X1, X2)) -> mark#(X1), mark#(U71(X1, X2, X3)) -> a__U71#(mark(X1), X2, X3)) (mark#(U21(X1, X2)) -> mark#(X1), mark#(U71(X1, X2, X3)) -> mark#(X1)) (mark#(U21(X1, X2)) -> mark#(X1), mark#(U61(X)) -> a__U61#(mark(X))) (mark#(U21(X1, X2)) -> mark#(X1), mark#(U61(X)) -> mark#(X)) (mark#(U21(X1, X2)) -> mark#(X1), mark#(U51(X1, X2, X3)) -> a__U51#(mark(X1), X2, X3)) (mark#(U21(X1, X2)) -> mark#(X1), mark#(U51(X1, X2, X3)) -> mark#(X1)) (mark#(U21(X1, X2)) -> mark#(X1), mark#(U41(X1, X2)) -> a__U41#(mark(X1), X2)) (mark#(U21(X1, X2)) -> mark#(X1), mark#(U41(X1, X2)) -> mark#(X1)) (mark#(U21(X1, X2)) -> mark#(X1), mark#(U33(X)) -> mark#(X)) (mark#(U21(X1, X2)) -> mark#(X1), mark#(U33(X)) -> a__U33#(mark(X))) (mark#(U21(X1, X2)) -> mark#(X1), mark#(U32(X1, X2)) -> mark#(X1)) (mark#(U21(X1, X2)) -> mark#(X1), mark#(U32(X1, X2)) -> a__U32#(mark(X1), X2)) (mark#(U21(X1, X2)) -> mark#(X1), mark#(U31(X1, X2, X3)) -> mark#(X1)) (mark#(U21(X1, X2)) -> mark#(X1), mark#(U31(X1, X2, X3)) -> a__U31#(mark(X1), X2, X3)) (mark#(U21(X1, X2)) -> mark#(X1), mark#(U22(X)) -> mark#(X)) (mark#(U21(X1, X2)) -> mark#(X1), mark#(U22(X)) -> a__U22#(mark(X))) (mark#(U21(X1, X2)) -> mark#(X1), mark#(U21(X1, X2)) -> mark#(X1)) (mark#(U21(X1, X2)) -> mark#(X1), mark#(U21(X1, X2)) -> a__U21#(mark(X1), X2)) (mark#(U21(X1, X2)) -> mark#(X1), mark#(U13(X)) -> mark#(X)) (mark#(U21(X1, X2)) -> mark#(X1), mark#(U13(X)) -> a__U13#(mark(X))) (mark#(U21(X1, X2)) -> mark#(X1), mark#(U12(X1, X2)) -> mark#(X1)) (mark#(U21(X1, X2)) -> mark#(X1), mark#(U12(X1, X2)) -> a__U12#(mark(X1), X2)) (mark#(U21(X1, X2)) -> mark#(X1), mark#(U11(X1, X2, X3)) -> mark#(X1)) (mark#(U21(X1, X2)) -> mark#(X1), mark#(U11(X1, X2, X3)) -> a__U11#(mark(X1), X2, X3)) (mark#(U21(X1, X2)) -> mark#(X1), mark#(isNat(X)) -> a__isNat#(X)) (mark#(U21(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), X2)) (mark#(U21(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X1)) (mark#(U21(X1, X2)) -> mark#(X1), mark#(x(X1, X2)) -> a__x#(mark(X1), mark(X2))) (mark#(U21(X1, X2)) -> mark#(X1), mark#(x(X1, X2)) -> mark#(X2)) (mark#(U21(X1, X2)) -> mark#(X1), mark#(x(X1, X2)) -> mark#(X1)) (mark#(U21(X1, X2)) -> mark#(X1), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2))) (mark#(U21(X1, X2)) -> mark#(X1), mark#(plus(X1, X2)) -> mark#(X2)) (mark#(U21(X1, X2)) -> mark#(X1), mark#(plus(X1, X2)) -> mark#(X1)) (mark#(U21(X1, X2)) -> mark#(X1), mark#(isNatKind(X)) -> a__isNatKind#(X)) (mark#(U21(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X)) (mark#(U32(X1, X2)) -> mark#(X1), mark#(U71(X1, X2, X3)) -> a__U71#(mark(X1), X2, X3)) (mark#(U32(X1, X2)) -> mark#(X1), mark#(U71(X1, X2, X3)) -> mark#(X1)) (mark#(U32(X1, X2)) -> mark#(X1), mark#(U61(X)) -> a__U61#(mark(X))) (mark#(U32(X1, X2)) -> mark#(X1), mark#(U61(X)) -> mark#(X)) (mark#(U32(X1, X2)) -> mark#(X1), mark#(U51(X1, X2, X3)) -> a__U51#(mark(X1), X2, X3)) (mark#(U32(X1, X2)) -> mark#(X1), mark#(U51(X1, X2, X3)) -> mark#(X1)) (mark#(U32(X1, X2)) -> mark#(X1), mark#(U41(X1, X2)) -> a__U41#(mark(X1), X2)) (mark#(U32(X1, X2)) -> mark#(X1), mark#(U41(X1, X2)) -> mark#(X1)) (mark#(U32(X1, X2)) -> mark#(X1), mark#(U33(X)) -> mark#(X)) (mark#(U32(X1, X2)) -> mark#(X1), mark#(U33(X)) -> a__U33#(mark(X))) (mark#(U32(X1, X2)) -> mark#(X1), mark#(U32(X1, X2)) -> mark#(X1)) (mark#(U32(X1, X2)) -> mark#(X1), mark#(U32(X1, X2)) -> a__U32#(mark(X1), X2)) (mark#(U32(X1, X2)) -> mark#(X1), mark#(U31(X1, X2, X3)) -> mark#(X1)) (mark#(U32(X1, X2)) -> mark#(X1), mark#(U31(X1, X2, X3)) -> a__U31#(mark(X1), X2, X3)) (mark#(U32(X1, X2)) -> mark#(X1), mark#(U22(X)) -> mark#(X)) (mark#(U32(X1, X2)) -> mark#(X1), mark#(U22(X)) -> a__U22#(mark(X))) (mark#(U32(X1, X2)) -> mark#(X1), mark#(U21(X1, X2)) -> mark#(X1)) (mark#(U32(X1, X2)) -> mark#(X1), mark#(U21(X1, X2)) -> a__U21#(mark(X1), X2)) (mark#(U32(X1, X2)) -> mark#(X1), mark#(U13(X)) -> mark#(X)) (mark#(U32(X1, X2)) -> mark#(X1), mark#(U13(X)) -> a__U13#(mark(X))) (mark#(U32(X1, X2)) -> mark#(X1), mark#(U12(X1, X2)) -> mark#(X1)) (mark#(U32(X1, X2)) -> mark#(X1), mark#(U12(X1, X2)) -> a__U12#(mark(X1), X2)) (mark#(U32(X1, X2)) -> mark#(X1), mark#(U11(X1, X2, X3)) -> mark#(X1)) (mark#(U32(X1, X2)) -> mark#(X1), mark#(U11(X1, X2, X3)) -> a__U11#(mark(X1), X2, X3)) (mark#(U32(X1, X2)) -> mark#(X1), mark#(isNat(X)) -> a__isNat#(X)) (mark#(U32(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), X2)) (mark#(U32(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X1)) (mark#(U32(X1, X2)) -> mark#(X1), mark#(x(X1, X2)) -> a__x#(mark(X1), mark(X2))) (mark#(U32(X1, X2)) -> mark#(X1), mark#(x(X1, X2)) -> mark#(X2)) (mark#(U32(X1, X2)) -> mark#(X1), mark#(x(X1, X2)) -> mark#(X1)) (mark#(U32(X1, X2)) -> mark#(X1), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2))) (mark#(U32(X1, X2)) -> mark#(X1), mark#(plus(X1, X2)) -> mark#(X2)) (mark#(U32(X1, X2)) -> mark#(X1), mark#(plus(X1, X2)) -> mark#(X1)) (mark#(U32(X1, X2)) -> mark#(X1), mark#(isNatKind(X)) -> a__isNatKind#(X)) (mark#(U32(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X)) (mark#(U51(X1, X2, X3)) -> mark#(X1), mark#(U71(X1, X2, X3)) -> a__U71#(mark(X1), X2, X3)) (mark#(U51(X1, X2, X3)) -> mark#(X1), mark#(U71(X1, X2, X3)) -> mark#(X1)) (mark#(U51(X1, X2, X3)) -> mark#(X1), mark#(U61(X)) -> a__U61#(mark(X))) (mark#(U51(X1, X2, X3)) -> mark#(X1), mark#(U61(X)) -> mark#(X)) (mark#(U51(X1, X2, X3)) -> mark#(X1), mark#(U51(X1, X2, X3)) -> a__U51#(mark(X1), X2, X3)) (mark#(U51(X1, X2, X3)) -> mark#(X1), mark#(U51(X1, X2, X3)) -> mark#(X1)) (mark#(U51(X1, X2, X3)) -> mark#(X1), mark#(U41(X1, X2)) -> a__U41#(mark(X1), X2)) (mark#(U51(X1, X2, X3)) -> mark#(X1), mark#(U41(X1, X2)) -> mark#(X1)) (mark#(U51(X1, X2, X3)) -> mark#(X1), mark#(U33(X)) -> mark#(X)) (mark#(U51(X1, X2, X3)) -> mark#(X1), mark#(U33(X)) -> a__U33#(mark(X))) (mark#(U51(X1, X2, X3)) -> mark#(X1), mark#(U32(X1, X2)) -> mark#(X1)) (mark#(U51(X1, X2, X3)) -> mark#(X1), mark#(U32(X1, X2)) -> a__U32#(mark(X1), X2)) (mark#(U51(X1, X2, X3)) -> mark#(X1), mark#(U31(X1, X2, X3)) -> mark#(X1)) (mark#(U51(X1, X2, X3)) -> mark#(X1), mark#(U31(X1, X2, X3)) -> a__U31#(mark(X1), X2, X3)) (mark#(U51(X1, X2, X3)) -> mark#(X1), mark#(U22(X)) -> mark#(X)) (mark#(U51(X1, X2, X3)) -> mark#(X1), mark#(U22(X)) -> a__U22#(mark(X))) (mark#(U51(X1, X2, X3)) -> mark#(X1), mark#(U21(X1, X2)) -> mark#(X1)) (mark#(U51(X1, X2, X3)) -> mark#(X1), mark#(U21(X1, X2)) -> a__U21#(mark(X1), X2)) (mark#(U51(X1, X2, X3)) -> mark#(X1), mark#(U13(X)) -> mark#(X)) (mark#(U51(X1, X2, X3)) -> mark#(X1), mark#(U13(X)) -> a__U13#(mark(X))) (mark#(U51(X1, X2, X3)) -> mark#(X1), mark#(U12(X1, X2)) -> mark#(X1)) (mark#(U51(X1, X2, X3)) -> mark#(X1), mark#(U12(X1, X2)) -> a__U12#(mark(X1), X2)) (mark#(U51(X1, X2, X3)) -> mark#(X1), mark#(U11(X1, X2, X3)) -> mark#(X1)) (mark#(U51(X1, X2, X3)) -> mark#(X1), mark#(U11(X1, X2, X3)) -> a__U11#(mark(X1), X2, X3)) (mark#(U51(X1, X2, X3)) -> mark#(X1), mark#(isNat(X)) -> a__isNat#(X)) (mark#(U51(X1, X2, X3)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), X2)) (mark#(U51(X1, X2, X3)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X1)) (mark#(U51(X1, X2, X3)) -> mark#(X1), mark#(x(X1, X2)) -> a__x#(mark(X1), mark(X2))) (mark#(U51(X1, X2, X3)) -> mark#(X1), mark#(x(X1, X2)) -> mark#(X2)) (mark#(U51(X1, X2, X3)) -> mark#(X1), mark#(x(X1, X2)) -> mark#(X1)) (mark#(U51(X1, X2, X3)) -> mark#(X1), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2))) (mark#(U51(X1, X2, X3)) -> mark#(X1), mark#(plus(X1, X2)) -> mark#(X2)) (mark#(U51(X1, X2, X3)) -> mark#(X1), mark#(plus(X1, X2)) -> mark#(X1)) (mark#(U51(X1, X2, X3)) -> mark#(X1), mark#(isNatKind(X)) -> a__isNatKind#(X)) (mark#(U51(X1, X2, X3)) -> mark#(X1), mark#(s(X)) -> mark#(X)) (mark#(U11(X1, X2, X3)) -> a__U11#(mark(X1), X2, X3), a__U11#(tt(), V1, V2) -> a__isNat#(V1)) (mark#(U11(X1, X2, X3)) -> a__U11#(mark(X1), X2, X3), a__U11#(tt(), V1, V2) -> a__U12#(a__isNat(V1), V2)) (mark#(U51(X1, X2, X3)) -> a__U51#(mark(X1), X2, X3), a__U51#(tt(), M, N) -> a__plus#(mark(N), mark(M))) (mark#(U51(X1, X2, X3)) -> a__U51#(mark(X1), X2, X3), a__U51#(tt(), M, N) -> mark#(M)) (mark#(U51(X1, X2, X3)) -> a__U51#(mark(X1), X2, X3), a__U51#(tt(), M, N) -> mark#(N)) (a__isNat#(s(V1)) -> a__isNatKind#(V1), a__isNatKind#(x(V1, V2)) -> a__isNatKind#(V1)) (a__isNat#(s(V1)) -> a__isNatKind#(V1), a__isNatKind#(x(V1, V2)) -> a__and#(a__isNatKind(V1), isNatKind(V2))) (a__isNat#(s(V1)) -> a__isNatKind#(V1), a__isNatKind#(plus(V1, V2)) -> a__isNatKind#(V1)) (a__isNat#(s(V1)) -> a__isNatKind#(V1), a__isNatKind#(plus(V1, V2)) -> a__and#(a__isNatKind(V1), isNatKind(V2))) (a__isNat#(s(V1)) -> a__isNatKind#(V1), a__isNatKind#(s(V1)) -> a__isNatKind#(V1)) (a__isNat#(x(V1, V2)) -> a__isNatKind#(V1), a__isNatKind#(x(V1, V2)) -> a__isNatKind#(V1)) (a__isNat#(x(V1, V2)) -> a__isNatKind#(V1), a__isNatKind#(x(V1, V2)) -> a__and#(a__isNatKind(V1), isNatKind(V2))) (a__isNat#(x(V1, V2)) -> a__isNatKind#(V1), a__isNatKind#(plus(V1, V2)) -> a__isNatKind#(V1)) (a__isNat#(x(V1, V2)) -> a__isNatKind#(V1), a__isNatKind#(plus(V1, V2)) -> a__and#(a__isNatKind(V1), isNatKind(V2))) (a__isNat#(x(V1, V2)) -> a__isNatKind#(V1), a__isNatKind#(s(V1)) -> a__isNatKind#(V1)) (a__U21#(tt(), V1) -> a__isNat#(V1), a__isNat#(x(V1, V2)) -> a__isNatKind#(V1)) (a__U21#(tt(), V1) -> a__isNat#(V1), a__isNat#(x(V1, V2)) -> a__and#(a__isNatKind(V1), isNatKind(V2))) (a__U21#(tt(), V1) -> a__isNat#(V1), a__isNat#(x(V1, V2)) -> a__U31#(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)) (a__U21#(tt(), V1) -> a__isNat#(V1), a__isNat#(plus(V1, V2)) -> a__isNatKind#(V1)) (a__U21#(tt(), V1) -> a__isNat#(V1), a__isNat#(plus(V1, V2)) -> a__and#(a__isNatKind(V1), isNatKind(V2))) (a__U21#(tt(), V1) -> a__isNat#(V1), a__isNat#(plus(V1, V2)) -> a__U11#(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)) (a__U21#(tt(), V1) -> a__isNat#(V1), a__isNat#(s(V1)) -> a__isNatKind#(V1)) (a__U21#(tt(), V1) -> a__isNat#(V1), a__isNat#(s(V1)) -> a__U21#(a__isNatKind(V1), V1)) (a__isNatKind#(s(V1)) -> a__isNatKind#(V1), a__isNatKind#(x(V1, V2)) -> a__isNatKind#(V1)) (a__isNatKind#(s(V1)) -> a__isNatKind#(V1), a__isNatKind#(x(V1, V2)) -> a__and#(a__isNatKind(V1), isNatKind(V2))) (a__isNatKind#(s(V1)) -> a__isNatKind#(V1), a__isNatKind#(plus(V1, V2)) -> a__isNatKind#(V1)) (a__isNatKind#(s(V1)) -> a__isNatKind#(V1), a__isNatKind#(plus(V1, V2)) -> a__and#(a__isNatKind(V1), isNatKind(V2))) (a__isNatKind#(s(V1)) -> a__isNatKind#(V1), a__isNatKind#(s(V1)) -> a__isNatKind#(V1)) (a__isNatKind#(x(V1, V2)) -> a__isNatKind#(V1), a__isNatKind#(x(V1, V2)) -> a__isNatKind#(V1)) (a__isNatKind#(x(V1, V2)) -> a__isNatKind#(V1), a__isNatKind#(x(V1, V2)) -> a__and#(a__isNatKind(V1), isNatKind(V2))) (a__isNatKind#(x(V1, V2)) -> a__isNatKind#(V1), a__isNatKind#(plus(V1, V2)) -> a__isNatKind#(V1)) (a__isNatKind#(x(V1, V2)) -> a__isNatKind#(V1), a__isNatKind#(plus(V1, V2)) -> a__and#(a__isNatKind(V1), isNatKind(V2))) (a__isNatKind#(x(V1, V2)) -> a__isNatKind#(V1), a__isNatKind#(s(V1)) -> a__isNatKind#(V1)) (a__plus#(N, 0()) -> a__isNat#(N), a__isNat#(x(V1, V2)) -> a__isNatKind#(V1)) (a__plus#(N, 0()) -> a__isNat#(N), a__isNat#(x(V1, V2)) -> a__and#(a__isNatKind(V1), isNatKind(V2))) (a__plus#(N, 0()) -> a__isNat#(N), a__isNat#(x(V1, V2)) -> a__U31#(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)) (a__plus#(N, 0()) -> a__isNat#(N), a__isNat#(plus(V1, V2)) -> a__isNatKind#(V1)) (a__plus#(N, 0()) -> a__isNat#(N), a__isNat#(plus(V1, V2)) -> a__and#(a__isNatKind(V1), isNatKind(V2))) (a__plus#(N, 0()) -> a__isNat#(N), a__isNat#(plus(V1, V2)) -> a__U11#(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)) (a__plus#(N, 0()) -> a__isNat#(N), a__isNat#(s(V1)) -> a__isNatKind#(V1)) (a__plus#(N, 0()) -> a__isNat#(N), a__isNat#(s(V1)) -> a__U21#(a__isNatKind(V1), V1)) (a__x#(N, 0()) -> a__isNat#(N), a__isNat#(x(V1, V2)) -> a__isNatKind#(V1)) (a__x#(N, 0()) -> a__isNat#(N), a__isNat#(x(V1, V2)) -> a__and#(a__isNatKind(V1), isNatKind(V2))) (a__x#(N, 0()) -> a__isNat#(N), a__isNat#(x(V1, V2)) -> a__U31#(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)) (a__x#(N, 0()) -> a__isNat#(N), a__isNat#(plus(V1, V2)) -> a__isNatKind#(V1)) (a__x#(N, 0()) -> a__isNat#(N), a__isNat#(plus(V1, V2)) -> a__and#(a__isNatKind(V1), isNatKind(V2))) (a__x#(N, 0()) -> a__isNat#(N), a__isNat#(plus(V1, V2)) -> a__U11#(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)) (a__x#(N, 0()) -> a__isNat#(N), a__isNat#(s(V1)) -> a__isNatKind#(V1)) (a__x#(N, 0()) -> a__isNat#(N), a__isNat#(s(V1)) -> a__U21#(a__isNatKind(V1), V1)) (mark#(s(X)) -> mark#(X), mark#(U71(X1, X2, X3)) -> a__U71#(mark(X1), X2, X3)) (mark#(s(X)) -> mark#(X), mark#(U71(X1, X2, X3)) -> mark#(X1)) (mark#(s(X)) -> mark#(X), mark#(U61(X)) -> a__U61#(mark(X))) (mark#(s(X)) -> mark#(X), mark#(U61(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(U51(X1, X2, X3)) -> a__U51#(mark(X1), X2, X3)) (mark#(s(X)) -> mark#(X), mark#(U51(X1, X2, X3)) -> mark#(X1)) (mark#(s(X)) -> mark#(X), mark#(U41(X1, X2)) -> a__U41#(mark(X1), X2)) (mark#(s(X)) -> mark#(X), mark#(U41(X1, X2)) -> mark#(X1)) (mark#(s(X)) -> mark#(X), mark#(U33(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(U33(X)) -> a__U33#(mark(X))) (mark#(s(X)) -> mark#(X), mark#(U32(X1, X2)) -> mark#(X1)) (mark#(s(X)) -> mark#(X), mark#(U32(X1, X2)) -> a__U32#(mark(X1), X2)) (mark#(s(X)) -> mark#(X), mark#(U31(X1, X2, X3)) -> mark#(X1)) (mark#(s(X)) -> mark#(X), mark#(U31(X1, X2, X3)) -> a__U31#(mark(X1), X2, X3)) (mark#(s(X)) -> mark#(X), mark#(U22(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(U22(X)) -> a__U22#(mark(X))) (mark#(s(X)) -> mark#(X), mark#(U21(X1, X2)) -> mark#(X1)) (mark#(s(X)) -> mark#(X), mark#(U21(X1, X2)) -> a__U21#(mark(X1), X2)) (mark#(s(X)) -> mark#(X), mark#(U13(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(U13(X)) -> a__U13#(mark(X))) (mark#(s(X)) -> mark#(X), mark#(U12(X1, X2)) -> mark#(X1)) (mark#(s(X)) -> mark#(X), mark#(U12(X1, X2)) -> a__U12#(mark(X1), X2)) (mark#(s(X)) -> mark#(X), mark#(U11(X1, X2, X3)) -> mark#(X1)) (mark#(s(X)) -> mark#(X), mark#(U11(X1, X2, X3)) -> a__U11#(mark(X1), X2, X3)) (mark#(s(X)) -> mark#(X), mark#(isNat(X)) -> a__isNat#(X)) (mark#(s(X)) -> mark#(X), mark#(and(X1, X2)) -> a__and#(mark(X1), X2)) (mark#(s(X)) -> mark#(X), mark#(and(X1, X2)) -> mark#(X1)) (mark#(s(X)) -> mark#(X), mark#(x(X1, X2)) -> a__x#(mark(X1), mark(X2))) (mark#(s(X)) -> mark#(X), mark#(x(X1, X2)) -> mark#(X2)) (mark#(s(X)) -> mark#(X), mark#(x(X1, X2)) -> mark#(X1)) (mark#(s(X)) -> mark#(X), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2))) (mark#(s(X)) -> mark#(X), mark#(plus(X1, X2)) -> mark#(X2)) (mark#(s(X)) -> mark#(X), mark#(plus(X1, X2)) -> mark#(X1)) (mark#(s(X)) -> mark#(X), mark#(isNatKind(X)) -> a__isNatKind#(X)) (mark#(s(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(isNat(X)) -> a__isNat#(X), a__isNat#(x(V1, V2)) -> a__isNatKind#(V1)) (mark#(isNat(X)) -> a__isNat#(X), a__isNat#(x(V1, V2)) -> a__and#(a__isNatKind(V1), isNatKind(V2))) (mark#(isNat(X)) -> a__isNat#(X), a__isNat#(x(V1, V2)) -> a__U31#(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)) (mark#(isNat(X)) -> a__isNat#(X), a__isNat#(plus(V1, V2)) -> a__isNatKind#(V1)) (mark#(isNat(X)) -> a__isNat#(X), a__isNat#(plus(V1, V2)) -> a__and#(a__isNatKind(V1), isNatKind(V2))) (mark#(isNat(X)) -> a__isNat#(X), a__isNat#(plus(V1, V2)) -> a__U11#(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)) (mark#(isNat(X)) -> a__isNat#(X), a__isNat#(s(V1)) -> a__isNatKind#(V1)) (mark#(isNat(X)) -> a__isNat#(X), a__isNat#(s(V1)) -> a__U21#(a__isNatKind(V1), V1)) (mark#(U22(X)) -> mark#(X), mark#(U71(X1, X2, X3)) -> a__U71#(mark(X1), X2, X3)) (mark#(U22(X)) -> mark#(X), mark#(U71(X1, X2, X3)) -> mark#(X1)) (mark#(U22(X)) -> mark#(X), mark#(U61(X)) -> a__U61#(mark(X))) (mark#(U22(X)) -> mark#(X), mark#(U61(X)) -> mark#(X)) (mark#(U22(X)) -> mark#(X), mark#(U51(X1, X2, X3)) -> a__U51#(mark(X1), X2, X3)) (mark#(U22(X)) -> mark#(X), mark#(U51(X1, X2, X3)) -> mark#(X1)) (mark#(U22(X)) -> mark#(X), mark#(U41(X1, X2)) -> a__U41#(mark(X1), X2)) (mark#(U22(X)) -> mark#(X), mark#(U41(X1, X2)) -> mark#(X1)) (mark#(U22(X)) -> mark#(X), mark#(U33(X)) -> mark#(X)) (mark#(U22(X)) -> mark#(X), mark#(U33(X)) -> a__U33#(mark(X))) (mark#(U22(X)) -> mark#(X), mark#(U32(X1, X2)) -> mark#(X1)) (mark#(U22(X)) -> mark#(X), mark#(U32(X1, X2)) -> a__U32#(mark(X1), X2)) (mark#(U22(X)) -> mark#(X), mark#(U31(X1, X2, X3)) -> mark#(X1)) (mark#(U22(X)) -> mark#(X), mark#(U31(X1, X2, X3)) -> a__U31#(mark(X1), X2, X3)) (mark#(U22(X)) -> mark#(X), mark#(U22(X)) -> mark#(X)) (mark#(U22(X)) -> mark#(X), mark#(U22(X)) -> a__U22#(mark(X))) (mark#(U22(X)) -> mark#(X), mark#(U21(X1, X2)) -> mark#(X1)) (mark#(U22(X)) -> mark#(X), mark#(U21(X1, X2)) -> a__U21#(mark(X1), X2)) (mark#(U22(X)) -> mark#(X), mark#(U13(X)) -> mark#(X)) (mark#(U22(X)) -> mark#(X), mark#(U13(X)) -> a__U13#(mark(X))) (mark#(U22(X)) -> mark#(X), mark#(U12(X1, X2)) -> mark#(X1)) (mark#(U22(X)) -> mark#(X), mark#(U12(X1, X2)) -> a__U12#(mark(X1), X2)) (mark#(U22(X)) -> mark#(X), mark#(U11(X1, X2, X3)) -> mark#(X1)) (mark#(U22(X)) -> mark#(X), mark#(U11(X1, X2, X3)) -> a__U11#(mark(X1), X2, X3)) (mark#(U22(X)) -> mark#(X), mark#(isNat(X)) -> a__isNat#(X)) (mark#(U22(X)) -> mark#(X), mark#(and(X1, X2)) -> a__and#(mark(X1), X2)) (mark#(U22(X)) -> mark#(X), mark#(and(X1, X2)) -> mark#(X1)) (mark#(U22(X)) -> mark#(X), mark#(x(X1, X2)) -> a__x#(mark(X1), mark(X2))) (mark#(U22(X)) -> mark#(X), mark#(x(X1, X2)) -> mark#(X2)) (mark#(U22(X)) -> mark#(X), mark#(x(X1, X2)) -> mark#(X1)) (mark#(U22(X)) -> mark#(X), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2))) (mark#(U22(X)) -> mark#(X), mark#(plus(X1, X2)) -> mark#(X2)) (mark#(U22(X)) -> mark#(X), mark#(plus(X1, X2)) -> mark#(X1)) (mark#(U22(X)) -> mark#(X), mark#(isNatKind(X)) -> a__isNatKind#(X)) (mark#(U22(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(U61(X)) -> mark#(X), mark#(U71(X1, X2, X3)) -> a__U71#(mark(X1), X2, X3)) (mark#(U61(X)) -> mark#(X), mark#(U71(X1, X2, X3)) -> mark#(X1)) (mark#(U61(X)) -> mark#(X), mark#(U61(X)) -> a__U61#(mark(X))) (mark#(U61(X)) -> mark#(X), mark#(U61(X)) -> mark#(X)) (mark#(U61(X)) -> mark#(X), mark#(U51(X1, X2, X3)) -> a__U51#(mark(X1), X2, X3)) (mark#(U61(X)) -> mark#(X), mark#(U51(X1, X2, X3)) -> mark#(X1)) (mark#(U61(X)) -> mark#(X), mark#(U41(X1, X2)) -> a__U41#(mark(X1), X2)) (mark#(U61(X)) -> mark#(X), mark#(U41(X1, X2)) -> mark#(X1)) (mark#(U61(X)) -> mark#(X), mark#(U33(X)) -> mark#(X)) (mark#(U61(X)) -> mark#(X), mark#(U33(X)) -> a__U33#(mark(X))) (mark#(U61(X)) -> mark#(X), mark#(U32(X1, X2)) -> mark#(X1)) (mark#(U61(X)) -> mark#(X), mark#(U32(X1, X2)) -> a__U32#(mark(X1), X2)) (mark#(U61(X)) -> mark#(X), mark#(U31(X1, X2, X3)) -> mark#(X1)) (mark#(U61(X)) -> mark#(X), mark#(U31(X1, X2, X3)) -> a__U31#(mark(X1), X2, X3)) (mark#(U61(X)) -> mark#(X), mark#(U22(X)) -> mark#(X)) (mark#(U61(X)) -> mark#(X), mark#(U22(X)) -> a__U22#(mark(X))) (mark#(U61(X)) -> mark#(X), mark#(U21(X1, X2)) -> mark#(X1)) (mark#(U61(X)) -> mark#(X), mark#(U21(X1, X2)) -> a__U21#(mark(X1), X2)) (mark#(U61(X)) -> mark#(X), mark#(U13(X)) -> mark#(X)) (mark#(U61(X)) -> mark#(X), mark#(U13(X)) -> a__U13#(mark(X))) (mark#(U61(X)) -> mark#(X), mark#(U12(X1, X2)) -> mark#(X1)) (mark#(U61(X)) -> mark#(X), mark#(U12(X1, X2)) -> a__U12#(mark(X1), X2)) (mark#(U61(X)) -> mark#(X), mark#(U11(X1, X2, X3)) -> mark#(X1)) (mark#(U61(X)) -> mark#(X), mark#(U11(X1, X2, X3)) -> a__U11#(mark(X1), X2, X3)) (mark#(U61(X)) -> mark#(X), mark#(isNat(X)) -> a__isNat#(X)) (mark#(U61(X)) -> mark#(X), mark#(and(X1, X2)) -> a__and#(mark(X1), X2)) (mark#(U61(X)) -> mark#(X), mark#(and(X1, X2)) -> mark#(X1)) (mark#(U61(X)) -> mark#(X), mark#(x(X1, X2)) -> a__x#(mark(X1), mark(X2))) (mark#(U61(X)) -> mark#(X), mark#(x(X1, X2)) -> mark#(X2)) (mark#(U61(X)) -> mark#(X), mark#(x(X1, X2)) -> mark#(X1)) (mark#(U61(X)) -> mark#(X), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2))) (mark#(U61(X)) -> mark#(X), mark#(plus(X1, X2)) -> mark#(X2)) (mark#(U61(X)) -> mark#(X), mark#(plus(X1, X2)) -> mark#(X1)) (mark#(U61(X)) -> mark#(X), mark#(isNatKind(X)) -> a__isNatKind#(X)) (mark#(U61(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(plus(X1, X2)) -> mark#(X2), mark#(U71(X1, X2, X3)) -> a__U71#(mark(X1), X2, X3)) (mark#(plus(X1, X2)) -> mark#(X2), mark#(U71(X1, X2, X3)) -> mark#(X1)) (mark#(plus(X1, X2)) -> mark#(X2), mark#(U61(X)) -> a__U61#(mark(X))) (mark#(plus(X1, X2)) -> mark#(X2), mark#(U61(X)) -> mark#(X)) (mark#(plus(X1, X2)) -> mark#(X2), mark#(U51(X1, X2, X3)) -> a__U51#(mark(X1), X2, X3)) (mark#(plus(X1, X2)) -> mark#(X2), mark#(U51(X1, X2, X3)) -> mark#(X1)) (mark#(plus(X1, X2)) -> mark#(X2), mark#(U41(X1, X2)) -> a__U41#(mark(X1), X2)) (mark#(plus(X1, X2)) -> mark#(X2), mark#(U41(X1, X2)) -> mark#(X1)) (mark#(plus(X1, X2)) -> mark#(X2), mark#(U33(X)) -> mark#(X)) (mark#(plus(X1, X2)) -> mark#(X2), mark#(U33(X)) -> a__U33#(mark(X))) (mark#(plus(X1, X2)) -> mark#(X2), mark#(U32(X1, X2)) -> mark#(X1)) (mark#(plus(X1, X2)) -> mark#(X2), mark#(U32(X1, X2)) -> a__U32#(mark(X1), X2)) (mark#(plus(X1, X2)) -> mark#(X2), mark#(U31(X1, X2, X3)) -> mark#(X1)) (mark#(plus(X1, X2)) -> mark#(X2), mark#(U31(X1, X2, X3)) -> a__U31#(mark(X1), X2, X3)) (mark#(plus(X1, X2)) -> mark#(X2), mark#(U22(X)) -> mark#(X)) (mark#(plus(X1, X2)) -> mark#(X2), mark#(U22(X)) -> a__U22#(mark(X))) (mark#(plus(X1, X2)) -> mark#(X2), mark#(U21(X1, X2)) -> mark#(X1)) (mark#(plus(X1, X2)) -> mark#(X2), mark#(U21(X1, X2)) -> a__U21#(mark(X1), X2)) (mark#(plus(X1, X2)) -> mark#(X2), mark#(U13(X)) -> mark#(X)) (mark#(plus(X1, X2)) -> mark#(X2), mark#(U13(X)) -> a__U13#(mark(X))) (mark#(plus(X1, X2)) -> mark#(X2), mark#(U12(X1, X2)) -> mark#(X1)) (mark#(plus(X1, X2)) -> mark#(X2), mark#(U12(X1, X2)) -> a__U12#(mark(X1), X2)) (mark#(plus(X1, X2)) -> mark#(X2), mark#(U11(X1, X2, X3)) -> mark#(X1)) (mark#(plus(X1, X2)) -> mark#(X2), mark#(U11(X1, X2, X3)) -> a__U11#(mark(X1), X2, X3)) (mark#(plus(X1, X2)) -> mark#(X2), mark#(isNat(X)) -> a__isNat#(X)) (mark#(plus(X1, X2)) -> mark#(X2), mark#(and(X1, X2)) -> a__and#(mark(X1), X2)) (mark#(plus(X1, X2)) -> mark#(X2), mark#(and(X1, X2)) -> mark#(X1)) (mark#(plus(X1, X2)) -> mark#(X2), mark#(x(X1, X2)) -> a__x#(mark(X1), mark(X2))) (mark#(plus(X1, X2)) -> mark#(X2), mark#(x(X1, X2)) -> mark#(X2)) (mark#(plus(X1, X2)) -> mark#(X2), mark#(x(X1, X2)) -> mark#(X1)) (mark#(plus(X1, X2)) -> mark#(X2), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2))) (mark#(plus(X1, X2)) -> mark#(X2), mark#(plus(X1, X2)) -> mark#(X2)) (mark#(plus(X1, X2)) -> mark#(X2), mark#(plus(X1, X2)) -> mark#(X1)) (mark#(plus(X1, X2)) -> mark#(X2), mark#(isNatKind(X)) -> a__isNatKind#(X)) (mark#(plus(X1, X2)) -> mark#(X2), mark#(s(X)) -> mark#(X)) (a__plus#(N, 0()) -> a__U41#(a__and(a__isNat(N), isNatKind(N)), N), a__U41#(tt(), N) -> mark#(N)) (a__isNat#(x(V1, V2)) -> a__and#(a__isNatKind(V1), isNatKind(V2)), a__and#(tt(), X) -> mark#(X)) (mark#(x(X1, X2)) -> a__x#(mark(X1), mark(X2)), a__x#(N, 0()) -> a__and#(a__isNat(N), isNatKind(N))) (mark#(x(X1, X2)) -> a__x#(mark(X1), mark(X2)), a__x#(N, 0()) -> a__U61#(a__and(a__isNat(N), isNatKind(N)))) (mark#(x(X1, X2)) -> a__x#(mark(X1), mark(X2)), a__x#(N, 0()) -> a__isNat#(N)) (mark#(x(X1, X2)) -> a__x#(mark(X1), mark(X2)), a__x#(N, s(M)) -> a__and#(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N)))) (mark#(x(X1, X2)) -> a__x#(mark(X1), mark(X2)), a__x#(N, s(M)) -> a__and#(a__isNat(M), isNatKind(M))) (mark#(x(X1, X2)) -> a__x#(mark(X1), mark(X2)), a__x#(N, s(M)) -> a__U71#(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)) (mark#(x(X1, X2)) -> a__x#(mark(X1), mark(X2)), a__x#(N, s(M)) -> a__isNat#(M)) (a__plus#(N, 0()) -> a__and#(a__isNat(N), isNatKind(N)), a__and#(tt(), X) -> mark#(X)) (a__x#(N, s(M)) -> a__and#(a__isNat(M), isNatKind(M)), a__and#(tt(), X) -> mark#(X)) (a__U71#(tt(), M, N) -> a__plus#(a__x(mark(N), mark(M)), mark(N)), a__plus#(N, 0()) -> a__and#(a__isNat(N), isNatKind(N))) (a__U71#(tt(), M, N) -> a__plus#(a__x(mark(N), mark(M)), mark(N)), a__plus#(N, 0()) -> a__U41#(a__and(a__isNat(N), isNatKind(N)), N)) (a__U71#(tt(), M, N) -> a__plus#(a__x(mark(N), mark(M)), mark(N)), a__plus#(N, 0()) -> a__isNat#(N)) (a__U71#(tt(), M, N) -> a__plus#(a__x(mark(N), mark(M)), mark(N)), a__plus#(N, s(M)) -> a__and#(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N)))) (a__U71#(tt(), M, N) -> a__plus#(a__x(mark(N), mark(M)), mark(N)), a__plus#(N, s(M)) -> a__and#(a__isNat(M), isNatKind(M))) (a__U71#(tt(), M, N) -> a__plus#(a__x(mark(N), mark(M)), mark(N)), a__plus#(N, s(M)) -> a__U51#(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)) (a__U71#(tt(), M, N) -> a__plus#(a__x(mark(N), mark(M)), mark(N)), a__plus#(N, s(M)) -> a__isNat#(M)) (a__isNatKind#(plus(V1, V2)) -> a__and#(a__isNatKind(V1), isNatKind(V2)), a__and#(tt(), X) -> mark#(X)) (mark#(and(X1, X2)) -> a__and#(mark(X1), X2), a__and#(tt(), X) -> mark#(X)) (mark#(U21(X1, X2)) -> a__U21#(mark(X1), X2), a__U21#(tt(), V1) -> a__U22#(a__isNat(V1))) (mark#(U21(X1, X2)) -> a__U21#(mark(X1), X2), a__U21#(tt(), V1) -> a__isNat#(V1)) (mark#(U41(X1, X2)) -> a__U41#(mark(X1), X2), a__U41#(tt(), N) -> mark#(N)) (a__plus#(N, s(M)) -> a__and#(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), a__and#(tt(), X) -> mark#(X)) (a__U11#(tt(), V1, V2) -> a__U12#(a__isNat(V1), V2), a__U12#(tt(), V2) -> a__U13#(a__isNat(V2))) (a__U11#(tt(), V1, V2) -> a__U12#(a__isNat(V1), V2), a__U12#(tt(), V2) -> a__isNat#(V2)) (a__U31#(tt(), V1, V2) -> a__U32#(a__isNat(V1), V2), a__U32#(tt(), V2) -> a__isNat#(V2)) (a__U31#(tt(), V1, V2) -> a__U32#(a__isNat(V1), V2), a__U32#(tt(), V2) -> a__U33#(a__isNat(V2))) (a__x#(N, s(M)) -> a__and#(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), a__and#(tt(), X) -> mark#(X)) (mark#(U32(X1, X2)) -> a__U32#(mark(X1), X2), a__U32#(tt(), V2) -> a__isNat#(V2)) (mark#(U32(X1, X2)) -> a__U32#(mark(X1), X2), a__U32#(tt(), V2) -> a__U33#(a__isNat(V2))) (mark#(U12(X1, X2)) -> a__U12#(mark(X1), X2), a__U12#(tt(), V2) -> a__isNat#(V2)) (mark#(U12(X1, X2)) -> a__U12#(mark(X1), X2), a__U12#(tt(), V2) -> a__U13#(a__isNat(V2))) (a__isNatKind#(x(V1, V2)) -> a__and#(a__isNatKind(V1), isNatKind(V2)), a__and#(tt(), X) -> mark#(X)) (a__U71#(tt(), M, N) -> a__x#(mark(N), mark(M)), a__x#(N, s(M)) -> a__isNat#(M)) (a__U71#(tt(), M, N) -> a__x#(mark(N), mark(M)), a__x#(N, s(M)) -> a__U71#(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)) (a__U71#(tt(), M, N) -> a__x#(mark(N), mark(M)), a__x#(N, s(M)) -> a__and#(a__isNat(M), isNatKind(M))) (a__U71#(tt(), M, N) -> a__x#(mark(N), mark(M)), a__x#(N, s(M)) -> a__and#(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N)))) (a__U71#(tt(), M, N) -> a__x#(mark(N), mark(M)), a__x#(N, 0()) -> a__isNat#(N)) (a__U71#(tt(), M, N) -> a__x#(mark(N), mark(M)), a__x#(N, 0()) -> a__U61#(a__and(a__isNat(N), isNatKind(N)))) (a__U71#(tt(), M, N) -> a__x#(mark(N), mark(M)), a__x#(N, 0()) -> a__and#(a__isNat(N), isNatKind(N))) (a__x#(N, 0()) -> a__and#(a__isNat(N), isNatKind(N)), a__and#(tt(), X) -> mark#(X)) (a__U51#(tt(), M, N) -> a__plus#(mark(N), mark(M)), a__plus#(N, s(M)) -> a__isNat#(M)) (a__U51#(tt(), M, N) -> a__plus#(mark(N), mark(M)), a__plus#(N, s(M)) -> a__U51#(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)) (a__U51#(tt(), M, N) -> a__plus#(mark(N), mark(M)), a__plus#(N, s(M)) -> a__and#(a__isNat(M), isNatKind(M))) (a__U51#(tt(), M, N) -> a__plus#(mark(N), mark(M)), a__plus#(N, s(M)) -> a__and#(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N)))) (a__U51#(tt(), M, N) -> a__plus#(mark(N), mark(M)), a__plus#(N, 0()) -> a__isNat#(N)) (a__U51#(tt(), M, N) -> a__plus#(mark(N), mark(M)), a__plus#(N, 0()) -> a__U41#(a__and(a__isNat(N), isNatKind(N)), N)) (a__U51#(tt(), M, N) -> a__plus#(mark(N), mark(M)), a__plus#(N, 0()) -> a__and#(a__isNat(N), isNatKind(N))) (a__plus#(N, s(M)) -> a__and#(a__isNat(M), isNatKind(M)), a__and#(tt(), X) -> mark#(X)) (mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)), a__plus#(N, s(M)) -> a__isNat#(M)) (mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)), a__plus#(N, s(M)) -> a__U51#(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N)) (mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)), a__plus#(N, s(M)) -> a__and#(a__isNat(M), isNatKind(M))) (mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)), a__plus#(N, s(M)) -> a__and#(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N)))) (mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)), a__plus#(N, 0()) -> a__isNat#(N)) (mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)), a__plus#(N, 0()) -> a__U41#(a__and(a__isNat(N), isNatKind(N)), N)) (mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)), a__plus#(N, 0()) -> a__and#(a__isNat(N), isNatKind(N))) (a__isNat#(plus(V1, V2)) -> a__and#(a__isNatKind(V1), isNatKind(V2)), a__and#(tt(), X) -> mark#(X)) (mark#(x(X1, X2)) -> mark#(X2), mark#(s(X)) -> mark#(X)) (mark#(x(X1, X2)) -> mark#(X2), mark#(isNatKind(X)) -> a__isNatKind#(X)) (mark#(x(X1, X2)) -> mark#(X2), mark#(plus(X1, X2)) -> mark#(X1)) (mark#(x(X1, X2)) -> mark#(X2), mark#(plus(X1, X2)) -> mark#(X2)) (mark#(x(X1, X2)) -> mark#(X2), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2))) (mark#(x(X1, X2)) -> mark#(X2), mark#(x(X1, X2)) -> mark#(X1)) (mark#(x(X1, X2)) -> mark#(X2), mark#(x(X1, X2)) -> mark#(X2)) (mark#(x(X1, X2)) -> mark#(X2), mark#(x(X1, X2)) -> a__x#(mark(X1), mark(X2))) (mark#(x(X1, X2)) -> mark#(X2), mark#(and(X1, X2)) -> mark#(X1)) (mark#(x(X1, X2)) -> mark#(X2), mark#(and(X1, X2)) -> a__and#(mark(X1), X2)) (mark#(x(X1, X2)) -> mark#(X2), mark#(isNat(X)) -> a__isNat#(X)) (mark#(x(X1, X2)) -> mark#(X2), mark#(U11(X1, X2, X3)) -> a__U11#(mark(X1), X2, X3)) (mark#(x(X1, X2)) -> mark#(X2), mark#(U11(X1, X2, X3)) -> mark#(X1)) (mark#(x(X1, X2)) -> mark#(X2), mark#(U12(X1, X2)) -> a__U12#(mark(X1), X2)) (mark#(x(X1, X2)) -> mark#(X2), mark#(U12(X1, X2)) -> mark#(X1)) (mark#(x(X1, X2)) -> mark#(X2), mark#(U13(X)) -> a__U13#(mark(X))) (mark#(x(X1, X2)) -> mark#(X2), mark#(U13(X)) -> mark#(X)) (mark#(x(X1, X2)) -> mark#(X2), mark#(U21(X1, X2)) -> a__U21#(mark(X1), X2)) (mark#(x(X1, X2)) -> mark#(X2), mark#(U21(X1, X2)) -> mark#(X1)) (mark#(x(X1, X2)) -> mark#(X2), mark#(U22(X)) -> a__U22#(mark(X))) (mark#(x(X1, X2)) -> mark#(X2), mark#(U22(X)) -> mark#(X)) (mark#(x(X1, X2)) -> mark#(X2), mark#(U31(X1, X2, X3)) -> a__U31#(mark(X1), X2, X3)) (mark#(x(X1, X2)) -> mark#(X2), mark#(U31(X1, X2, X3)) -> mark#(X1)) (mark#(x(X1, X2)) -> mark#(X2), mark#(U32(X1, X2)) -> a__U32#(mark(X1), X2)) (mark#(x(X1, X2)) -> mark#(X2), mark#(U32(X1, X2)) -> mark#(X1)) (mark#(x(X1, X2)) -> mark#(X2), mark#(U33(X)) -> a__U33#(mark(X))) (mark#(x(X1, X2)) -> mark#(X2), mark#(U33(X)) -> mark#(X)) (mark#(x(X1, X2)) -> mark#(X2), mark#(U41(X1, X2)) -> mark#(X1)) (mark#(x(X1, X2)) -> mark#(X2), mark#(U41(X1, X2)) -> a__U41#(mark(X1), X2)) (mark#(x(X1, X2)) -> mark#(X2), mark#(U51(X1, X2, X3)) -> mark#(X1)) (mark#(x(X1, X2)) -> mark#(X2), mark#(U51(X1, X2, X3)) -> a__U51#(mark(X1), X2, X3)) (mark#(x(X1, X2)) -> mark#(X2), mark#(U61(X)) -> mark#(X)) (mark#(x(X1, X2)) -> mark#(X2), mark#(U61(X)) -> a__U61#(mark(X))) (mark#(x(X1, X2)) -> mark#(X2), mark#(U71(X1, X2, X3)) -> mark#(X1)) (mark#(x(X1, X2)) -> mark#(X2), mark#(U71(X1, X2, X3)) -> a__U71#(mark(X1), X2, X3)) (a__and#(tt(), X) -> mark#(X), mark#(s(X)) -> mark#(X)) (a__and#(tt(), X) -> mark#(X), mark#(isNatKind(X)) -> a__isNatKind#(X)) (a__and#(tt(), X) -> mark#(X), mark#(plus(X1, X2)) -> mark#(X1)) (a__and#(tt(), X) -> mark#(X), mark#(plus(X1, X2)) -> mark#(X2)) (a__and#(tt(), X) -> mark#(X), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2))) (a__and#(tt(), X) -> mark#(X), mark#(x(X1, X2)) -> mark#(X1)) (a__and#(tt(), X) -> mark#(X), mark#(x(X1, X2)) -> mark#(X2)) (a__and#(tt(), X) -> mark#(X), mark#(x(X1, X2)) -> a__x#(mark(X1), mark(X2))) (a__and#(tt(), X) -> mark#(X), mark#(and(X1, X2)) -> mark#(X1)) (a__and#(tt(), X) -> mark#(X), mark#(and(X1, X2)) -> a__and#(mark(X1), X2)) (a__and#(tt(), X) -> mark#(X), mark#(isNat(X)) -> a__isNat#(X)) (a__and#(tt(), X) -> mark#(X), mark#(U11(X1, X2, X3)) -> a__U11#(mark(X1), X2, X3)) (a__and#(tt(), X) -> mark#(X), mark#(U11(X1, X2, X3)) -> mark#(X1)) (a__and#(tt(), X) -> mark#(X), mark#(U12(X1, X2)) -> a__U12#(mark(X1), X2)) (a__and#(tt(), X) -> mark#(X), mark#(U12(X1, X2)) -> mark#(X1)) (a__and#(tt(), X) -> mark#(X), mark#(U13(X)) -> a__U13#(mark(X))) (a__and#(tt(), X) -> mark#(X), mark#(U13(X)) -> mark#(X)) (a__and#(tt(), X) -> mark#(X), mark#(U21(X1, X2)) -> a__U21#(mark(X1), X2)) (a__and#(tt(), X) -> mark#(X), mark#(U21(X1, X2)) -> mark#(X1)) (a__and#(tt(), X) -> mark#(X), mark#(U22(X)) -> a__U22#(mark(X))) (a__and#(tt(), X) -> mark#(X), mark#(U22(X)) -> mark#(X)) (a__and#(tt(), X) -> mark#(X), mark#(U31(X1, X2, X3)) -> a__U31#(mark(X1), X2, X3)) (a__and#(tt(), X) -> mark#(X), mark#(U31(X1, X2, X3)) -> mark#(X1)) (a__and#(tt(), X) -> mark#(X), mark#(U32(X1, X2)) -> a__U32#(mark(X1), X2)) (a__and#(tt(), X) -> mark#(X), mark#(U32(X1, X2)) -> mark#(X1)) (a__and#(tt(), X) -> mark#(X), mark#(U33(X)) -> a__U33#(mark(X))) (a__and#(tt(), X) -> mark#(X), mark#(U33(X)) -> mark#(X)) (a__and#(tt(), X) -> mark#(X), mark#(U41(X1, X2)) -> mark#(X1)) (a__and#(tt(), X) -> mark#(X), mark#(U41(X1, X2)) -> a__U41#(mark(X1), X2)) (a__and#(tt(), X) -> mark#(X), mark#(U51(X1, X2, X3)) -> mark#(X1)) (a__and#(tt(), X) -> mark#(X), mark#(U51(X1, X2, X3)) -> a__U51#(mark(X1), X2, X3)) (a__and#(tt(), X) -> mark#(X), mark#(U61(X)) -> mark#(X)) (a__and#(tt(), X) -> mark#(X), mark#(U61(X)) -> a__U61#(mark(X))) (a__and#(tt(), X) -> mark#(X), mark#(U71(X1, X2, X3)) -> mark#(X1)) (a__and#(tt(), X) -> mark#(X), mark#(U71(X1, X2, X3)) -> a__U71#(mark(X1), X2, X3)) (mark#(U33(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(U33(X)) -> mark#(X), mark#(isNatKind(X)) -> a__isNatKind#(X)) (mark#(U33(X)) -> mark#(X), mark#(plus(X1, X2)) -> mark#(X1)) (mark#(U33(X)) -> mark#(X), mark#(plus(X1, X2)) -> mark#(X2)) (mark#(U33(X)) -> mark#(X), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2))) (mark#(U33(X)) -> mark#(X), mark#(x(X1, X2)) -> mark#(X1)) (mark#(U33(X)) -> mark#(X), mark#(x(X1, X2)) -> mark#(X2)) (mark#(U33(X)) -> mark#(X), mark#(x(X1, X2)) -> a__x#(mark(X1), mark(X2))) (mark#(U33(X)) -> mark#(X), mark#(and(X1, X2)) -> mark#(X1)) (mark#(U33(X)) -> mark#(X), mark#(and(X1, X2)) -> a__and#(mark(X1), X2)) (mark#(U33(X)) -> mark#(X), mark#(isNat(X)) -> a__isNat#(X)) (mark#(U33(X)) -> mark#(X), mark#(U11(X1, X2, X3)) -> a__U11#(mark(X1), X2, X3)) (mark#(U33(X)) -> mark#(X), mark#(U11(X1, X2, X3)) -> mark#(X1)) (mark#(U33(X)) -> mark#(X), mark#(U12(X1, X2)) -> a__U12#(mark(X1), X2)) (mark#(U33(X)) -> mark#(X), mark#(U12(X1, X2)) -> mark#(X1)) (mark#(U33(X)) -> mark#(X), mark#(U13(X)) -> a__U13#(mark(X))) (mark#(U33(X)) -> mark#(X), mark#(U13(X)) -> mark#(X)) (mark#(U33(X)) -> mark#(X), mark#(U21(X1, X2)) -> a__U21#(mark(X1), X2)) (mark#(U33(X)) -> mark#(X), mark#(U21(X1, X2)) -> mark#(X1)) (mark#(U33(X)) -> mark#(X), mark#(U22(X)) -> a__U22#(mark(X))) (mark#(U33(X)) -> mark#(X), mark#(U22(X)) -> mark#(X)) (mark#(U33(X)) -> mark#(X), mark#(U31(X1, X2, X3)) -> a__U31#(mark(X1), X2, X3)) (mark#(U33(X)) -> mark#(X), mark#(U31(X1, X2, X3)) -> mark#(X1)) (mark#(U33(X)) -> mark#(X), mark#(U32(X1, X2)) -> a__U32#(mark(X1), X2)) (mark#(U33(X)) -> mark#(X), mark#(U32(X1, X2)) -> mark#(X1)) (mark#(U33(X)) -> mark#(X), mark#(U33(X)) -> a__U33#(mark(X))) (mark#(U33(X)) -> mark#(X), mark#(U33(X)) -> mark#(X)) (mark#(U33(X)) -> mark#(X), mark#(U41(X1, X2)) -> mark#(X1)) (mark#(U33(X)) -> mark#(X), mark#(U41(X1, X2)) -> a__U41#(mark(X1), X2)) (mark#(U33(X)) -> mark#(X), mark#(U51(X1, X2, X3)) -> mark#(X1)) (mark#(U33(X)) -> mark#(X), mark#(U51(X1, X2, X3)) -> a__U51#(mark(X1), X2, X3)) (mark#(U33(X)) -> mark#(X), mark#(U61(X)) -> mark#(X)) (mark#(U33(X)) -> mark#(X), mark#(U61(X)) -> a__U61#(mark(X))) (mark#(U33(X)) -> mark#(X), mark#(U71(X1, X2, X3)) -> mark#(X1)) (mark#(U33(X)) -> mark#(X), mark#(U71(X1, X2, X3)) -> a__U71#(mark(X1), X2, X3)) (mark#(U13(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(U13(X)) -> mark#(X), mark#(isNatKind(X)) -> a__isNatKind#(X)) (mark#(U13(X)) -> mark#(X), mark#(plus(X1, X2)) -> mark#(X1)) (mark#(U13(X)) -> mark#(X), mark#(plus(X1, X2)) -> mark#(X2)) (mark#(U13(X)) -> mark#(X), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2))) (mark#(U13(X)) -> mark#(X), mark#(x(X1, X2)) -> mark#(X1)) (mark#(U13(X)) -> mark#(X), mark#(x(X1, X2)) -> mark#(X2)) (mark#(U13(X)) -> mark#(X), mark#(x(X1, X2)) -> a__x#(mark(X1), mark(X2))) (mark#(U13(X)) -> mark#(X), mark#(and(X1, X2)) -> mark#(X1)) (mark#(U13(X)) -> mark#(X), mark#(and(X1, X2)) -> a__and#(mark(X1), X2)) (mark#(U13(X)) -> mark#(X), mark#(isNat(X)) -> a__isNat#(X)) (mark#(U13(X)) -> mark#(X), mark#(U11(X1, X2, X3)) -> a__U11#(mark(X1), X2, X3)) (mark#(U13(X)) -> mark#(X), mark#(U11(X1, X2, X3)) -> mark#(X1)) (mark#(U13(X)) -> mark#(X), mark#(U12(X1, X2)) -> a__U12#(mark(X1), X2)) (mark#(U13(X)) -> mark#(X), mark#(U12(X1, X2)) -> mark#(X1)) (mark#(U13(X)) -> mark#(X), mark#(U13(X)) -> a__U13#(mark(X))) (mark#(U13(X)) -> mark#(X), mark#(U13(X)) -> mark#(X)) (mark#(U13(X)) -> mark#(X), mark#(U21(X1, X2)) -> a__U21#(mark(X1), X2)) (mark#(U13(X)) -> mark#(X), mark#(U21(X1, X2)) -> mark#(X1)) (mark#(U13(X)) -> mark#(X), mark#(U22(X)) -> a__U22#(mark(X))) (mark#(U13(X)) -> mark#(X), mark#(U22(X)) -> mark#(X)) (mark#(U13(X)) -> mark#(X), mark#(U31(X1, X2, X3)) -> a__U31#(mark(X1), X2, X3)) (mark#(U13(X)) -> mark#(X), mark#(U31(X1, X2, X3)) -> mark#(X1)) (mark#(U13(X)) -> mark#(X), mark#(U32(X1, X2)) -> a__U32#(mark(X1), X2)) (mark#(U13(X)) -> mark#(X), mark#(U32(X1, X2)) -> mark#(X1)) (mark#(U13(X)) -> mark#(X), mark#(U33(X)) -> a__U33#(mark(X))) (mark#(U13(X)) -> mark#(X), mark#(U33(X)) -> mark#(X)) (mark#(U13(X)) -> mark#(X), mark#(U41(X1, X2)) -> mark#(X1)) (mark#(U13(X)) -> mark#(X), mark#(U41(X1, X2)) -> a__U41#(mark(X1), X2)) (mark#(U13(X)) -> mark#(X), mark#(U51(X1, X2, X3)) -> mark#(X1)) (mark#(U13(X)) -> mark#(X), mark#(U51(X1, X2, X3)) -> a__U51#(mark(X1), X2, X3)) (mark#(U13(X)) -> mark#(X), mark#(U61(X)) -> mark#(X)) (mark#(U13(X)) -> mark#(X), mark#(U61(X)) -> a__U61#(mark(X))) (mark#(U13(X)) -> mark#(X), mark#(U71(X1, X2, X3)) -> mark#(X1)) (mark#(U13(X)) -> mark#(X), mark#(U71(X1, X2, X3)) -> a__U71#(mark(X1), X2, X3)) (mark#(isNatKind(X)) -> a__isNatKind#(X), a__isNatKind#(s(V1)) -> a__isNatKind#(V1)) (mark#(isNatKind(X)) -> a__isNatKind#(X), a__isNatKind#(plus(V1, V2)) -> a__and#(a__isNatKind(V1), isNatKind(V2))) (mark#(isNatKind(X)) -> a__isNatKind#(X), a__isNatKind#(plus(V1, V2)) -> a__isNatKind#(V1)) (mark#(isNatKind(X)) -> a__isNatKind#(X), a__isNatKind#(x(V1, V2)) -> a__and#(a__isNatKind(V1), isNatKind(V2))) (mark#(isNatKind(X)) -> a__isNatKind#(X), a__isNatKind#(x(V1, V2)) -> a__isNatKind#(V1)) (a__U71#(tt(), M, N) -> mark#(N), mark#(s(X)) -> mark#(X)) (a__U71#(tt(), M, N) -> mark#(N), mark#(isNatKind(X)) -> a__isNatKind#(X)) (a__U71#(tt(), M, N) -> mark#(N), mark#(plus(X1, X2)) -> mark#(X1)) (a__U71#(tt(), M, N) -> mark#(N), mark#(plus(X1, X2)) -> mark#(X2)) (a__U71#(tt(), M, N) -> mark#(N), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2))) (a__U71#(tt(), M, N) -> mark#(N), mark#(x(X1, X2)) -> mark#(X1)) (a__U71#(tt(), M, N) -> mark#(N), mark#(x(X1, X2)) -> mark#(X2)) (a__U71#(tt(), M, N) -> mark#(N), mark#(x(X1, X2)) -> a__x#(mark(X1), mark(X2))) (a__U71#(tt(), M, N) -> mark#(N), mark#(and(X1, X2)) -> mark#(X1)) (a__U71#(tt(), M, N) -> mark#(N), mark#(and(X1, X2)) -> a__and#(mark(X1), X2)) (a__U71#(tt(), M, N) -> mark#(N), mark#(isNat(X)) -> a__isNat#(X)) (a__U71#(tt(), M, N) -> mark#(N), mark#(U11(X1, X2, X3)) -> a__U11#(mark(X1), X2, X3)) (a__U71#(tt(), M, N) -> mark#(N), mark#(U11(X1, X2, X3)) -> mark#(X1)) (a__U71#(tt(), M, N) -> mark#(N), mark#(U12(X1, X2)) -> a__U12#(mark(X1), X2)) (a__U71#(tt(), M, N) -> mark#(N), mark#(U12(X1, X2)) -> mark#(X1)) (a__U71#(tt(), M, N) -> mark#(N), mark#(U13(X)) -> a__U13#(mark(X))) (a__U71#(tt(), M, N) -> mark#(N), mark#(U13(X)) -> mark#(X)) (a__U71#(tt(), M, N) -> mark#(N), mark#(U21(X1, X2)) -> a__U21#(mark(X1), X2)) (a__U71#(tt(), M, N) -> mark#(N), mark#(U21(X1, X2)) -> mark#(X1)) (a__U71#(tt(), M, N) -> mark#(N), mark#(U22(X)) -> a__U22#(mark(X))) (a__U71#(tt(), M, N) -> mark#(N), mark#(U22(X)) -> mark#(X)) (a__U71#(tt(), M, N) -> mark#(N), mark#(U31(X1, X2, X3)) -> a__U31#(mark(X1), X2, X3)) (a__U71#(tt(), M, N) -> mark#(N), mark#(U31(X1, X2, X3)) -> mark#(X1)) (a__U71#(tt(), M, N) -> mark#(N), mark#(U32(X1, X2)) -> a__U32#(mark(X1), X2)) (a__U71#(tt(), M, N) -> mark#(N), mark#(U32(X1, X2)) -> mark#(X1)) (a__U71#(tt(), M, N) -> mark#(N), mark#(U33(X)) -> a__U33#(mark(X))) (a__U71#(tt(), M, N) -> mark#(N), mark#(U33(X)) -> mark#(X)) (a__U71#(tt(), M, N) -> mark#(N), mark#(U41(X1, X2)) -> mark#(X1)) (a__U71#(tt(), M, N) -> mark#(N), mark#(U41(X1, X2)) -> a__U41#(mark(X1), X2)) (a__U71#(tt(), M, N) -> mark#(N), mark#(U51(X1, X2, X3)) -> mark#(X1)) (a__U71#(tt(), M, N) -> mark#(N), mark#(U51(X1, X2, X3)) -> a__U51#(mark(X1), X2, X3)) (a__U71#(tt(), M, N) -> mark#(N), mark#(U61(X)) -> mark#(X)) (a__U71#(tt(), M, N) -> mark#(N), mark#(U61(X)) -> a__U61#(mark(X))) (a__U71#(tt(), M, N) -> mark#(N), mark#(U71(X1, X2, X3)) -> mark#(X1)) (a__U71#(tt(), M, N) -> mark#(N), mark#(U71(X1, X2, X3)) -> a__U71#(mark(X1), X2, X3)) (a__U51#(tt(), M, N) -> mark#(N), mark#(s(X)) -> mark#(X)) (a__U51#(tt(), M, N) -> mark#(N), mark#(isNatKind(X)) -> a__isNatKind#(X)) (a__U51#(tt(), M, N) -> mark#(N), mark#(plus(X1, X2)) -> mark#(X1)) (a__U51#(tt(), M, N) -> mark#(N), mark#(plus(X1, X2)) -> mark#(X2)) (a__U51#(tt(), M, N) -> mark#(N), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2))) (a__U51#(tt(), M, N) -> mark#(N), mark#(x(X1, X2)) -> mark#(X1)) (a__U51#(tt(), M, N) -> mark#(N), mark#(x(X1, X2)) -> mark#(X2)) (a__U51#(tt(), M, N) -> mark#(N), mark#(x(X1, X2)) -> a__x#(mark(X1), mark(X2))) (a__U51#(tt(), M, N) -> mark#(N), mark#(and(X1, X2)) -> mark#(X1)) (a__U51#(tt(), M, N) -> mark#(N), mark#(and(X1, X2)) -> a__and#(mark(X1), X2)) (a__U51#(tt(), M, N) -> mark#(N), mark#(isNat(X)) -> a__isNat#(X)) (a__U51#(tt(), M, N) -> mark#(N), mark#(U11(X1, X2, X3)) -> a__U11#(mark(X1), X2, X3)) (a__U51#(tt(), M, N) -> mark#(N), mark#(U11(X1, X2, X3)) -> mark#(X1)) (a__U51#(tt(), M, N) -> mark#(N), mark#(U12(X1, X2)) -> a__U12#(mark(X1), X2)) (a__U51#(tt(), M, N) -> mark#(N), mark#(U12(X1, X2)) -> mark#(X1)) (a__U51#(tt(), M, N) -> mark#(N), mark#(U13(X)) -> a__U13#(mark(X))) (a__U51#(tt(), M, N) -> mark#(N), mark#(U13(X)) -> mark#(X)) (a__U51#(tt(), M, N) -> mark#(N), mark#(U21(X1, X2)) -> a__U21#(mark(X1), X2)) (a__U51#(tt(), M, N) -> mark#(N), mark#(U21(X1, X2)) -> mark#(X1)) (a__U51#(tt(), M, N) -> mark#(N), mark#(U22(X)) -> a__U22#(mark(X))) (a__U51#(tt(), M, N) -> mark#(N), mark#(U22(X)) -> mark#(X)) (a__U51#(tt(), M, N) -> mark#(N), mark#(U31(X1, X2, X3)) -> a__U31#(mark(X1), X2, X3)) (a__U51#(tt(), M, N) -> mark#(N), mark#(U31(X1, X2, X3)) -> mark#(X1)) (a__U51#(tt(), M, N) -> mark#(N), mark#(U32(X1, X2)) -> a__U32#(mark(X1), X2)) (a__U51#(tt(), M, N) -> mark#(N), mark#(U32(X1, X2)) -> mark#(X1)) (a__U51#(tt(), M, N) -> mark#(N), mark#(U33(X)) -> a__U33#(mark(X))) (a__U51#(tt(), M, N) -> mark#(N), mark#(U33(X)) -> mark#(X)) (a__U51#(tt(), M, N) -> mark#(N), mark#(U41(X1, X2)) -> mark#(X1)) (a__U51#(tt(), M, N) -> mark#(N), mark#(U41(X1, X2)) -> a__U41#(mark(X1), X2)) (a__U51#(tt(), M, N) -> mark#(N), mark#(U51(X1, X2, X3)) -> mark#(X1)) (a__U51#(tt(), M, N) -> mark#(N), mark#(U51(X1, X2, X3)) -> a__U51#(mark(X1), X2, X3)) (a__U51#(tt(), M, N) -> mark#(N), mark#(U61(X)) -> mark#(X)) (a__U51#(tt(), M, N) -> mark#(N), mark#(U61(X)) -> a__U61#(mark(X))) (a__U51#(tt(), M, N) -> mark#(N), mark#(U71(X1, X2, X3)) -> mark#(X1)) (a__U51#(tt(), M, N) -> mark#(N), mark#(U71(X1, X2, X3)) -> a__U71#(mark(X1), X2, X3)) (a__U41#(tt(), N) -> mark#(N), mark#(s(X)) -> mark#(X)) (a__U41#(tt(), N) -> mark#(N), mark#(isNatKind(X)) -> a__isNatKind#(X)) (a__U41#(tt(), N) -> mark#(N), mark#(plus(X1, X2)) -> mark#(X1)) (a__U41#(tt(), N) -> mark#(N), mark#(plus(X1, X2)) -> mark#(X2)) (a__U41#(tt(), N) -> mark#(N), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2))) (a__U41#(tt(), N) -> mark#(N), mark#(x(X1, X2)) -> mark#(X1)) (a__U41#(tt(), N) -> mark#(N), mark#(x(X1, X2)) -> mark#(X2)) (a__U41#(tt(), N) -> mark#(N), mark#(x(X1, X2)) -> a__x#(mark(X1), mark(X2))) (a__U41#(tt(), N) -> mark#(N), mark#(and(X1, X2)) -> mark#(X1)) (a__U41#(tt(), N) -> mark#(N), mark#(and(X1, X2)) -> a__and#(mark(X1), X2)) (a__U41#(tt(), N) -> mark#(N), mark#(isNat(X)) -> a__isNat#(X)) (a__U41#(tt(), N) -> mark#(N), mark#(U11(X1, X2, X3)) -> a__U11#(mark(X1), X2, X3)) (a__U41#(tt(), N) -> mark#(N), mark#(U11(X1, X2, X3)) -> mark#(X1)) (a__U41#(tt(), N) -> mark#(N), mark#(U12(X1, X2)) -> a__U12#(mark(X1), X2)) (a__U41#(tt(), N) -> mark#(N), mark#(U12(X1, X2)) -> mark#(X1)) (a__U41#(tt(), N) -> mark#(N), mark#(U13(X)) -> a__U13#(mark(X))) (a__U41#(tt(), N) -> mark#(N), mark#(U13(X)) -> mark#(X)) (a__U41#(tt(), N) -> mark#(N), mark#(U21(X1, X2)) -> a__U21#(mark(X1), X2)) (a__U41#(tt(), N) -> mark#(N), mark#(U21(X1, X2)) -> mark#(X1)) (a__U41#(tt(), N) -> mark#(N), mark#(U22(X)) -> a__U22#(mark(X))) (a__U41#(tt(), N) -> mark#(N), mark#(U22(X)) -> mark#(X)) (a__U41#(tt(), N) -> mark#(N), mark#(U31(X1, X2, X3)) -> a__U31#(mark(X1), X2, X3)) (a__U41#(tt(), N) -> mark#(N), mark#(U31(X1, X2, X3)) -> mark#(X1)) (a__U41#(tt(), N) -> mark#(N), mark#(U32(X1, X2)) -> a__U32#(mark(X1), X2)) (a__U41#(tt(), N) -> mark#(N), mark#(U32(X1, X2)) -> mark#(X1)) (a__U41#(tt(), N) -> mark#(N), mark#(U33(X)) -> a__U33#(mark(X))) (a__U41#(tt(), N) -> mark#(N), mark#(U33(X)) -> mark#(X)) (a__U41#(tt(), N) -> mark#(N), mark#(U41(X1, X2)) -> mark#(X1)) (a__U41#(tt(), N) -> mark#(N), mark#(U41(X1, X2)) -> a__U41#(mark(X1), X2)) (a__U41#(tt(), N) -> mark#(N), mark#(U51(X1, X2, X3)) -> mark#(X1)) (a__U41#(tt(), N) -> mark#(N), mark#(U51(X1, X2, X3)) -> a__U51#(mark(X1), X2, X3)) (a__U41#(tt(), N) -> mark#(N), mark#(U61(X)) -> mark#(X)) (a__U41#(tt(), N) -> mark#(N), mark#(U61(X)) -> a__U61#(mark(X))) (a__U41#(tt(), N) -> mark#(N), mark#(U71(X1, X2, X3)) -> mark#(X1)) (a__U41#(tt(), N) -> mark#(N), mark#(U71(X1, X2, X3)) -> a__U71#(mark(X1), X2, X3)) (a__isNatKind#(plus(V1, V2)) -> a__isNatKind#(V1), a__isNatKind#(s(V1)) -> a__isNatKind#(V1)) (a__isNatKind#(plus(V1, V2)) -> a__isNatKind#(V1), a__isNatKind#(plus(V1, V2)) -> a__and#(a__isNatKind(V1), isNatKind(V2))) (a__isNatKind#(plus(V1, V2)) -> a__isNatKind#(V1), a__isNatKind#(plus(V1, V2)) -> a__isNatKind#(V1)) (a__isNatKind#(plus(V1, V2)) -> a__isNatKind#(V1), a__isNatKind#(x(V1, V2)) -> a__and#(a__isNatKind(V1), isNatKind(V2))) (a__isNatKind#(plus(V1, V2)) -> a__isNatKind#(V1), a__isNatKind#(x(V1, V2)) -> a__isNatKind#(V1)) (a__U31#(tt(), V1, V2) -> a__isNat#(V1), a__isNat#(s(V1)) -> a__U21#(a__isNatKind(V1), V1)) (a__U31#(tt(), V1, V2) -> a__isNat#(V1), a__isNat#(s(V1)) -> a__isNatKind#(V1)) (a__U31#(tt(), V1, V2) -> a__isNat#(V1), a__isNat#(plus(V1, V2)) -> a__U11#(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)) (a__U31#(tt(), V1, V2) -> a__isNat#(V1), a__isNat#(plus(V1, V2)) -> a__and#(a__isNatKind(V1), isNatKind(V2))) (a__U31#(tt(), V1, V2) -> a__isNat#(V1), a__isNat#(plus(V1, V2)) -> a__isNatKind#(V1)) (a__U31#(tt(), V1, V2) -> a__isNat#(V1), a__isNat#(x(V1, V2)) -> a__U31#(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)) (a__U31#(tt(), V1, V2) -> a__isNat#(V1), a__isNat#(x(V1, V2)) -> a__and#(a__isNatKind(V1), isNatKind(V2))) (a__U31#(tt(), V1, V2) -> a__isNat#(V1), a__isNat#(x(V1, V2)) -> a__isNatKind#(V1)) (a__U11#(tt(), V1, V2) -> a__isNat#(V1), a__isNat#(s(V1)) -> a__U21#(a__isNatKind(V1), V1)) (a__U11#(tt(), V1, V2) -> a__isNat#(V1), a__isNat#(s(V1)) -> a__isNatKind#(V1)) (a__U11#(tt(), V1, V2) -> a__isNat#(V1), a__isNat#(plus(V1, V2)) -> a__U11#(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)) (a__U11#(tt(), V1, V2) -> a__isNat#(V1), a__isNat#(plus(V1, V2)) -> a__and#(a__isNatKind(V1), isNatKind(V2))) (a__U11#(tt(), V1, V2) -> a__isNat#(V1), a__isNat#(plus(V1, V2)) -> a__isNatKind#(V1)) (a__U11#(tt(), V1, V2) -> a__isNat#(V1), a__isNat#(x(V1, V2)) -> a__U31#(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)) (a__U11#(tt(), V1, V2) -> a__isNat#(V1), a__isNat#(x(V1, V2)) -> a__and#(a__isNatKind(V1), isNatKind(V2))) (a__U11#(tt(), V1, V2) -> a__isNat#(V1), a__isNat#(x(V1, V2)) -> a__isNatKind#(V1)) (a__isNat#(plus(V1, V2)) -> a__isNatKind#(V1), a__isNatKind#(s(V1)) -> a__isNatKind#(V1)) (a__isNat#(plus(V1, V2)) -> a__isNatKind#(V1), a__isNatKind#(plus(V1, V2)) -> a__and#(a__isNatKind(V1), isNatKind(V2))) (a__isNat#(plus(V1, V2)) -> a__isNatKind#(V1), a__isNatKind#(plus(V1, V2)) -> a__isNatKind#(V1)) (a__isNat#(plus(V1, V2)) -> a__isNatKind#(V1), a__isNatKind#(x(V1, V2)) -> a__and#(a__isNatKind(V1), isNatKind(V2))) (a__isNat#(plus(V1, V2)) -> a__isNatKind#(V1), a__isNatKind#(x(V1, V2)) -> a__isNatKind#(V1)) (mark#(U71(X1, X2, X3)) -> a__U71#(mark(X1), X2, X3), a__U71#(tt(), M, N) -> mark#(N)) (mark#(U71(X1, X2, X3)) -> a__U71#(mark(X1), X2, X3), a__U71#(tt(), M, N) -> mark#(M)) (mark#(U71(X1, X2, X3)) -> a__U71#(mark(X1), X2, X3), a__U71#(tt(), M, N) -> a__plus#(a__x(mark(N), mark(M)), mark(N))) (mark#(U71(X1, X2, X3)) -> a__U71#(mark(X1), X2, X3), a__U71#(tt(), M, N) -> a__x#(mark(N), mark(M))) (mark#(U31(X1, X2, X3)) -> a__U31#(mark(X1), X2, X3), a__U31#(tt(), V1, V2) -> a__isNat#(V1)) (mark#(U31(X1, X2, X3)) -> a__U31#(mark(X1), X2, X3), a__U31#(tt(), V1, V2) -> a__U32#(a__isNat(V1), V2)) (mark#(U71(X1, X2, X3)) -> mark#(X1), mark#(s(X)) -> mark#(X)) (mark#(U71(X1, X2, X3)) -> mark#(X1), mark#(isNatKind(X)) -> a__isNatKind#(X)) (mark#(U71(X1, X2, X3)) -> mark#(X1), mark#(plus(X1, X2)) -> mark#(X1)) (mark#(U71(X1, X2, X3)) -> mark#(X1), mark#(plus(X1, X2)) -> mark#(X2)) (mark#(U71(X1, X2, X3)) -> mark#(X1), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2))) (mark#(U71(X1, X2, X3)) -> mark#(X1), mark#(x(X1, X2)) -> mark#(X1)) (mark#(U71(X1, X2, X3)) -> mark#(X1), mark#(x(X1, X2)) -> mark#(X2)) (mark#(U71(X1, X2, X3)) -> mark#(X1), mark#(x(X1, X2)) -> a__x#(mark(X1), mark(X2))) (mark#(U71(X1, X2, X3)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X1)) (mark#(U71(X1, X2, X3)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), X2)) (mark#(U71(X1, X2, X3)) -> mark#(X1), mark#(isNat(X)) -> a__isNat#(X)) (mark#(U71(X1, X2, X3)) -> mark#(X1), mark#(U11(X1, X2, X3)) -> a__U11#(mark(X1), X2, X3)) (mark#(U71(X1, X2, X3)) -> mark#(X1), mark#(U11(X1, X2, X3)) -> mark#(X1)) (mark#(U71(X1, X2, X3)) -> mark#(X1), mark#(U12(X1, X2)) -> a__U12#(mark(X1), X2)) (mark#(U71(X1, X2, X3)) -> mark#(X1), mark#(U12(X1, X2)) -> mark#(X1)) (mark#(U71(X1, X2, X3)) -> mark#(X1), mark#(U13(X)) -> a__U13#(mark(X))) (mark#(U71(X1, X2, X3)) -> mark#(X1), mark#(U13(X)) -> mark#(X)) (mark#(U71(X1, X2, X3)) -> mark#(X1), mark#(U21(X1, X2)) -> a__U21#(mark(X1), X2)) (mark#(U71(X1, X2, X3)) -> mark#(X1), mark#(U21(X1, X2)) -> mark#(X1)) (mark#(U71(X1, X2, X3)) -> mark#(X1), mark#(U22(X)) -> a__U22#(mark(X))) (mark#(U71(X1, X2, X3)) -> mark#(X1), mark#(U22(X)) -> mark#(X)) (mark#(U71(X1, X2, X3)) -> mark#(X1), mark#(U31(X1, X2, X3)) -> a__U31#(mark(X1), X2, X3)) (mark#(U71(X1, X2, X3)) -> mark#(X1), mark#(U31(X1, X2, X3)) -> mark#(X1)) (mark#(U71(X1, X2, X3)) -> mark#(X1), mark#(U32(X1, X2)) -> a__U32#(mark(X1), X2)) (mark#(U71(X1, X2, X3)) -> mark#(X1), mark#(U32(X1, X2)) -> mark#(X1)) (mark#(U71(X1, X2, X3)) -> mark#(X1), mark#(U33(X)) -> a__U33#(mark(X))) (mark#(U71(X1, X2, X3)) -> mark#(X1), mark#(U33(X)) -> mark#(X)) (mark#(U71(X1, X2, X3)) -> mark#(X1), mark#(U41(X1, X2)) -> mark#(X1)) (mark#(U71(X1, X2, X3)) -> mark#(X1), mark#(U41(X1, X2)) -> a__U41#(mark(X1), X2)) (mark#(U71(X1, X2, X3)) -> mark#(X1), mark#(U51(X1, X2, X3)) -> mark#(X1)) (mark#(U71(X1, X2, X3)) -> mark#(X1), mark#(U51(X1, X2, X3)) -> a__U51#(mark(X1), X2, X3)) (mark#(U71(X1, X2, X3)) -> mark#(X1), mark#(U61(X)) -> mark#(X)) (mark#(U71(X1, X2, X3)) -> mark#(X1), mark#(U61(X)) -> a__U61#(mark(X))) (mark#(U71(X1, X2, X3)) -> mark#(X1), mark#(U71(X1, X2, X3)) -> mark#(X1)) (mark#(U71(X1, X2, X3)) -> mark#(X1), mark#(U71(X1, X2, X3)) -> a__U71#(mark(X1), X2, X3)) (mark#(U41(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X)) (mark#(U41(X1, X2)) -> mark#(X1), mark#(isNatKind(X)) -> a__isNatKind#(X)) (mark#(U41(X1, X2)) -> mark#(X1), mark#(plus(X1, X2)) -> mark#(X1)) (mark#(U41(X1, X2)) -> mark#(X1), mark#(plus(X1, X2)) -> mark#(X2)) (mark#(U41(X1, X2)) -> mark#(X1), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2))) (mark#(U41(X1, X2)) -> mark#(X1), mark#(x(X1, X2)) -> mark#(X1)) (mark#(U41(X1, X2)) -> mark#(X1), mark#(x(X1, X2)) -> mark#(X2)) (mark#(U41(X1, X2)) -> mark#(X1), mark#(x(X1, X2)) -> a__x#(mark(X1), mark(X2))) (mark#(U41(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X1)) (mark#(U41(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), X2)) (mark#(U41(X1, X2)) -> mark#(X1), mark#(isNat(X)) -> a__isNat#(X)) (mark#(U41(X1, X2)) -> mark#(X1), mark#(U11(X1, X2, X3)) -> a__U11#(mark(X1), X2, X3)) (mark#(U41(X1, X2)) -> mark#(X1), mark#(U11(X1, X2, X3)) -> mark#(X1)) (mark#(U41(X1, X2)) -> mark#(X1), mark#(U12(X1, X2)) -> a__U12#(mark(X1), X2)) (mark#(U41(X1, X2)) -> mark#(X1), mark#(U12(X1, X2)) -> mark#(X1)) (mark#(U41(X1, X2)) -> mark#(X1), mark#(U13(X)) -> a__U13#(mark(X))) (mark#(U41(X1, X2)) -> mark#(X1), mark#(U13(X)) -> mark#(X)) (mark#(U41(X1, X2)) -> mark#(X1), mark#(U21(X1, X2)) -> a__U21#(mark(X1), X2)) (mark#(U41(X1, X2)) -> mark#(X1), mark#(U21(X1, X2)) -> mark#(X1)) (mark#(U41(X1, X2)) -> mark#(X1), mark#(U22(X)) -> a__U22#(mark(X))) (mark#(U41(X1, X2)) -> mark#(X1), mark#(U22(X)) -> mark#(X)) (mark#(U41(X1, X2)) -> mark#(X1), mark#(U31(X1, X2, X3)) -> a__U31#(mark(X1), X2, X3)) (mark#(U41(X1, X2)) -> mark#(X1), mark#(U31(X1, X2, X3)) -> mark#(X1)) (mark#(U41(X1, X2)) -> mark#(X1), mark#(U32(X1, X2)) -> a__U32#(mark(X1), X2)) (mark#(U41(X1, X2)) -> mark#(X1), mark#(U32(X1, X2)) -> mark#(X1)) (mark#(U41(X1, X2)) -> mark#(X1), mark#(U33(X)) -> a__U33#(mark(X))) (mark#(U41(X1, X2)) -> mark#(X1), mark#(U33(X)) -> mark#(X)) (mark#(U41(X1, X2)) -> mark#(X1), mark#(U41(X1, X2)) -> mark#(X1)) (mark#(U41(X1, X2)) -> mark#(X1), mark#(U41(X1, X2)) -> a__U41#(mark(X1), X2)) (mark#(U41(X1, X2)) -> mark#(X1), mark#(U51(X1, X2, X3)) -> mark#(X1)) (mark#(U41(X1, X2)) -> mark#(X1), mark#(U51(X1, X2, X3)) -> a__U51#(mark(X1), X2, X3)) (mark#(U41(X1, X2)) -> mark#(X1), mark#(U61(X)) -> mark#(X)) (mark#(U41(X1, X2)) -> mark#(X1), mark#(U61(X)) -> a__U61#(mark(X))) (mark#(U41(X1, X2)) -> mark#(X1), mark#(U71(X1, X2, X3)) -> mark#(X1)) (mark#(U41(X1, X2)) -> mark#(X1), mark#(U71(X1, X2, X3)) -> a__U71#(mark(X1), X2, X3)) (mark#(U31(X1, X2, X3)) -> mark#(X1), mark#(s(X)) -> mark#(X)) (mark#(U31(X1, X2, X3)) -> mark#(X1), mark#(isNatKind(X)) -> a__isNatKind#(X)) (mark#(U31(X1, X2, X3)) -> mark#(X1), mark#(plus(X1, X2)) -> mark#(X1)) (mark#(U31(X1, X2, X3)) -> mark#(X1), mark#(plus(X1, X2)) -> mark#(X2)) (mark#(U31(X1, X2, X3)) -> mark#(X1), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2))) (mark#(U31(X1, X2, X3)) -> mark#(X1), mark#(x(X1, X2)) -> mark#(X1)) (mark#(U31(X1, X2, X3)) -> mark#(X1), mark#(x(X1, X2)) -> mark#(X2)) (mark#(U31(X1, X2, X3)) -> mark#(X1), mark#(x(X1, X2)) -> a__x#(mark(X1), mark(X2))) (mark#(U31(X1, X2, X3)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X1)) (mark#(U31(X1, X2, X3)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), X2)) (mark#(U31(X1, X2, X3)) -> mark#(X1), mark#(isNat(X)) -> a__isNat#(X)) (mark#(U31(X1, X2, X3)) -> mark#(X1), mark#(U11(X1, X2, X3)) -> a__U11#(mark(X1), X2, X3)) (mark#(U31(X1, X2, X3)) -> mark#(X1), mark#(U11(X1, X2, X3)) -> mark#(X1)) (mark#(U31(X1, X2, X3)) -> mark#(X1), mark#(U12(X1, X2)) -> a__U12#(mark(X1), X2)) (mark#(U31(X1, X2, X3)) -> mark#(X1), mark#(U12(X1, X2)) -> mark#(X1)) (mark#(U31(X1, X2, X3)) -> mark#(X1), mark#(U13(X)) -> a__U13#(mark(X))) (mark#(U31(X1, X2, X3)) -> mark#(X1), mark#(U13(X)) -> mark#(X)) (mark#(U31(X1, X2, X3)) -> mark#(X1), mark#(U21(X1, X2)) -> a__U21#(mark(X1), X2)) (mark#(U31(X1, X2, X3)) -> mark#(X1), mark#(U21(X1, X2)) -> mark#(X1)) (mark#(U31(X1, X2, X3)) -> mark#(X1), mark#(U22(X)) -> a__U22#(mark(X))) (mark#(U31(X1, X2, X3)) -> mark#(X1), mark#(U22(X)) -> mark#(X)) (mark#(U31(X1, X2, X3)) -> mark#(X1), mark#(U31(X1, X2, X3)) -> a__U31#(mark(X1), X2, X3)) (mark#(U31(X1, X2, X3)) -> mark#(X1), mark#(U31(X1, X2, X3)) -> mark#(X1)) (mark#(U31(X1, X2, X3)) -> mark#(X1), mark#(U32(X1, X2)) -> a__U32#(mark(X1), X2)) (mark#(U31(X1, X2, X3)) -> mark#(X1), mark#(U32(X1, X2)) -> mark#(X1)) (mark#(U31(X1, X2, X3)) -> mark#(X1), mark#(U33(X)) -> a__U33#(mark(X))) (mark#(U31(X1, X2, X3)) -> mark#(X1), mark#(U33(X)) -> mark#(X)) (mark#(U31(X1, X2, X3)) -> mark#(X1), mark#(U41(X1, X2)) -> mark#(X1)) (mark#(U31(X1, X2, X3)) -> mark#(X1), mark#(U41(X1, X2)) -> a__U41#(mark(X1), X2)) (mark#(U31(X1, X2, X3)) -> mark#(X1), mark#(U51(X1, X2, X3)) -> mark#(X1)) (mark#(U31(X1, X2, X3)) -> mark#(X1), mark#(U51(X1, X2, X3)) -> a__U51#(mark(X1), X2, X3)) (mark#(U31(X1, X2, X3)) -> mark#(X1), mark#(U61(X)) -> mark#(X)) (mark#(U31(X1, X2, X3)) -> mark#(X1), mark#(U61(X)) -> a__U61#(mark(X))) (mark#(U31(X1, X2, X3)) -> mark#(X1), mark#(U71(X1, X2, X3)) -> mark#(X1)) (mark#(U31(X1, X2, X3)) -> mark#(X1), mark#(U71(X1, X2, X3)) -> a__U71#(mark(X1), X2, X3)) (mark#(U12(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X)) (mark#(U12(X1, X2)) -> mark#(X1), mark#(isNatKind(X)) -> a__isNatKind#(X)) (mark#(U12(X1, X2)) -> mark#(X1), mark#(plus(X1, X2)) -> mark#(X1)) (mark#(U12(X1, X2)) -> mark#(X1), mark#(plus(X1, X2)) -> mark#(X2)) (mark#(U12(X1, X2)) -> mark#(X1), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2))) (mark#(U12(X1, X2)) -> mark#(X1), mark#(x(X1, X2)) -> mark#(X1)) (mark#(U12(X1, X2)) -> mark#(X1), mark#(x(X1, X2)) -> mark#(X2)) (mark#(U12(X1, X2)) -> mark#(X1), mark#(x(X1, X2)) -> a__x#(mark(X1), mark(X2))) (mark#(U12(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X1)) (mark#(U12(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), X2)) (mark#(U12(X1, X2)) -> mark#(X1), mark#(isNat(X)) -> a__isNat#(X)) (mark#(U12(X1, X2)) -> mark#(X1), mark#(U11(X1, X2, X3)) -> a__U11#(mark(X1), X2, X3)) (mark#(U12(X1, X2)) -> mark#(X1), mark#(U11(X1, X2, X3)) -> mark#(X1)) (mark#(U12(X1, X2)) -> mark#(X1), mark#(U12(X1, X2)) -> a__U12#(mark(X1), X2)) (mark#(U12(X1, X2)) -> mark#(X1), mark#(U12(X1, X2)) -> mark#(X1)) (mark#(U12(X1, X2)) -> mark#(X1), mark#(U13(X)) -> a__U13#(mark(X))) (mark#(U12(X1, X2)) -> mark#(X1), mark#(U13(X)) -> mark#(X)) (mark#(U12(X1, X2)) -> mark#(X1), mark#(U21(X1, X2)) -> a__U21#(mark(X1), X2)) (mark#(U12(X1, X2)) -> mark#(X1), mark#(U21(X1, X2)) -> mark#(X1)) (mark#(U12(X1, X2)) -> mark#(X1), mark#(U22(X)) -> a__U22#(mark(X))) (mark#(U12(X1, X2)) -> mark#(X1), mark#(U22(X)) -> mark#(X)) (mark#(U12(X1, X2)) -> mark#(X1), mark#(U31(X1, X2, X3)) -> a__U31#(mark(X1), X2, X3)) (mark#(U12(X1, X2)) -> mark#(X1), mark#(U31(X1, X2, X3)) -> mark#(X1)) (mark#(U12(X1, X2)) -> mark#(X1), mark#(U32(X1, X2)) -> a__U32#(mark(X1), X2)) (mark#(U12(X1, X2)) -> mark#(X1), mark#(U32(X1, X2)) -> mark#(X1)) (mark#(U12(X1, X2)) -> mark#(X1), mark#(U33(X)) -> a__U33#(mark(X))) (mark#(U12(X1, X2)) -> mark#(X1), mark#(U33(X)) -> mark#(X)) (mark#(U12(X1, X2)) -> mark#(X1), mark#(U41(X1, X2)) -> mark#(X1)) (mark#(U12(X1, X2)) -> mark#(X1), mark#(U41(X1, X2)) -> a__U41#(mark(X1), X2)) (mark#(U12(X1, X2)) -> mark#(X1), mark#(U51(X1, X2, X3)) -> mark#(X1)) (mark#(U12(X1, X2)) -> mark#(X1), mark#(U51(X1, X2, X3)) -> a__U51#(mark(X1), X2, X3)) (mark#(U12(X1, X2)) -> mark#(X1), mark#(U61(X)) -> mark#(X)) (mark#(U12(X1, X2)) -> mark#(X1), mark#(U61(X)) -> a__U61#(mark(X))) (mark#(U12(X1, X2)) -> mark#(X1), mark#(U71(X1, X2, X3)) -> mark#(X1)) (mark#(U12(X1, X2)) -> mark#(X1), mark#(U71(X1, X2, X3)) -> a__U71#(mark(X1), X2, X3)) (mark#(and(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X)) (mark#(and(X1, X2)) -> mark#(X1), mark#(isNatKind(X)) -> a__isNatKind#(X)) (mark#(and(X1, X2)) -> mark#(X1), mark#(plus(X1, X2)) -> mark#(X1)) (mark#(and(X1, X2)) -> mark#(X1), mark#(plus(X1, X2)) -> mark#(X2)) (mark#(and(X1, X2)) -> mark#(X1), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2))) (mark#(and(X1, X2)) -> mark#(X1), mark#(x(X1, X2)) -> mark#(X1)) (mark#(and(X1, X2)) -> mark#(X1), mark#(x(X1, X2)) -> mark#(X2)) (mark#(and(X1, X2)) -> mark#(X1), mark#(x(X1, X2)) -> a__x#(mark(X1), mark(X2))) (mark#(and(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X1)) (mark#(and(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), X2)) (mark#(and(X1, X2)) -> mark#(X1), mark#(isNat(X)) -> a__isNat#(X)) (mark#(and(X1, X2)) -> mark#(X1), mark#(U11(X1, X2, X3)) -> a__U11#(mark(X1), X2, X3)) (mark#(and(X1, X2)) -> mark#(X1), mark#(U11(X1, X2, X3)) -> mark#(X1)) (mark#(and(X1, X2)) -> mark#(X1), mark#(U12(X1, X2)) -> a__U12#(mark(X1), X2)) (mark#(and(X1, X2)) -> mark#(X1), mark#(U12(X1, X2)) -> mark#(X1)) (mark#(and(X1, X2)) -> mark#(X1), mark#(U13(X)) -> a__U13#(mark(X))) (mark#(and(X1, X2)) -> mark#(X1), mark#(U13(X)) -> mark#(X)) (mark#(and(X1, X2)) -> mark#(X1), mark#(U21(X1, X2)) -> a__U21#(mark(X1), X2)) (mark#(and(X1, X2)) -> mark#(X1), mark#(U21(X1, X2)) -> mark#(X1)) (mark#(and(X1, X2)) -> mark#(X1), mark#(U22(X)) -> a__U22#(mark(X))) (mark#(and(X1, X2)) -> mark#(X1), mark#(U22(X)) -> mark#(X)) (mark#(and(X1, X2)) -> mark#(X1), mark#(U31(X1, X2, X3)) -> a__U31#(mark(X1), X2, X3)) (mark#(and(X1, X2)) -> mark#(X1), mark#(U31(X1, X2, X3)) -> mark#(X1)) (mark#(and(X1, X2)) -> mark#(X1), mark#(U32(X1, X2)) -> a__U32#(mark(X1), X2)) (mark#(and(X1, X2)) -> mark#(X1), mark#(U32(X1, X2)) -> mark#(X1)) (mark#(and(X1, X2)) -> mark#(X1), mark#(U33(X)) -> a__U33#(mark(X))) (mark#(and(X1, X2)) -> mark#(X1), mark#(U33(X)) -> mark#(X)) (mark#(and(X1, X2)) -> mark#(X1), mark#(U41(X1, X2)) -> mark#(X1)) (mark#(and(X1, X2)) -> mark#(X1), mark#(U41(X1, X2)) -> a__U41#(mark(X1), X2)) (mark#(and(X1, X2)) -> mark#(X1), mark#(U51(X1, X2, X3)) -> mark#(X1)) (mark#(and(X1, X2)) -> mark#(X1), mark#(U51(X1, X2, X3)) -> a__U51#(mark(X1), X2, X3)) (mark#(and(X1, X2)) -> mark#(X1), mark#(U61(X)) -> mark#(X)) (mark#(and(X1, X2)) -> mark#(X1), mark#(U61(X)) -> a__U61#(mark(X))) (mark#(and(X1, X2)) -> mark#(X1), mark#(U71(X1, X2, X3)) -> mark#(X1)) (mark#(and(X1, X2)) -> mark#(X1), mark#(U71(X1, X2, X3)) -> a__U71#(mark(X1), X2, X3)) (mark#(plus(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X)) (mark#(plus(X1, X2)) -> mark#(X1), mark#(isNatKind(X)) -> a__isNatKind#(X)) (mark#(plus(X1, X2)) -> mark#(X1), mark#(plus(X1, X2)) -> mark#(X1)) (mark#(plus(X1, X2)) -> mark#(X1), mark#(plus(X1, X2)) -> mark#(X2)) (mark#(plus(X1, X2)) -> mark#(X1), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2))) (mark#(plus(X1, X2)) -> mark#(X1), mark#(x(X1, X2)) -> mark#(X1)) (mark#(plus(X1, X2)) -> mark#(X1), mark#(x(X1, X2)) -> mark#(X2)) (mark#(plus(X1, X2)) -> mark#(X1), mark#(x(X1, X2)) -> a__x#(mark(X1), mark(X2))) (mark#(plus(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X1)) (mark#(plus(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), X2)) (mark#(plus(X1, X2)) -> mark#(X1), mark#(isNat(X)) -> a__isNat#(X)) (mark#(plus(X1, X2)) -> mark#(X1), mark#(U11(X1, X2, X3)) -> a__U11#(mark(X1), X2, X3)) (mark#(plus(X1, X2)) -> mark#(X1), mark#(U11(X1, X2, X3)) -> mark#(X1)) (mark#(plus(X1, X2)) -> mark#(X1), mark#(U12(X1, X2)) -> a__U12#(mark(X1), X2)) (mark#(plus(X1, X2)) -> mark#(X1), mark#(U12(X1, X2)) -> mark#(X1)) (mark#(plus(X1, X2)) -> mark#(X1), mark#(U13(X)) -> a__U13#(mark(X))) (mark#(plus(X1, X2)) -> mark#(X1), mark#(U13(X)) -> mark#(X)) (mark#(plus(X1, X2)) -> mark#(X1), mark#(U21(X1, X2)) -> a__U21#(mark(X1), X2)) (mark#(plus(X1, X2)) -> mark#(X1), mark#(U21(X1, X2)) -> mark#(X1)) (mark#(plus(X1, X2)) -> mark#(X1), mark#(U22(X)) -> a__U22#(mark(X))) (mark#(plus(X1, X2)) -> mark#(X1), mark#(U22(X)) -> mark#(X)) (mark#(plus(X1, X2)) -> mark#(X1), mark#(U31(X1, X2, X3)) -> a__U31#(mark(X1), X2, X3)) (mark#(plus(X1, X2)) -> mark#(X1), mark#(U31(X1, X2, X3)) -> mark#(X1)) (mark#(plus(X1, X2)) -> mark#(X1), mark#(U32(X1, X2)) -> a__U32#(mark(X1), X2)) (mark#(plus(X1, X2)) -> mark#(X1), mark#(U32(X1, X2)) -> mark#(X1)) (mark#(plus(X1, X2)) -> mark#(X1), mark#(U33(X)) -> a__U33#(mark(X))) (mark#(plus(X1, X2)) -> mark#(X1), mark#(U33(X)) -> mark#(X)) (mark#(plus(X1, X2)) -> mark#(X1), mark#(U41(X1, X2)) -> mark#(X1)) (mark#(plus(X1, X2)) -> mark#(X1), mark#(U41(X1, X2)) -> a__U41#(mark(X1), X2)) (mark#(plus(X1, X2)) -> mark#(X1), mark#(U51(X1, X2, X3)) -> mark#(X1)) (mark#(plus(X1, X2)) -> mark#(X1), mark#(U51(X1, X2, X3)) -> a__U51#(mark(X1), X2, X3)) (mark#(plus(X1, X2)) -> mark#(X1), mark#(U61(X)) -> mark#(X)) (mark#(plus(X1, X2)) -> mark#(X1), mark#(U61(X)) -> a__U61#(mark(X))) (mark#(plus(X1, X2)) -> mark#(X1), mark#(U71(X1, X2, X3)) -> mark#(X1)) (mark#(plus(X1, X2)) -> mark#(X1), mark#(U71(X1, X2, X3)) -> a__U71#(mark(X1), X2, X3)) (a__isNat#(plus(V1, V2)) -> a__U11#(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2), a__U11#(tt(), V1, V2) -> a__U12#(a__isNat(V1), V2)) (a__isNat#(plus(V1, V2)) -> a__U11#(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2), a__U11#(tt(), V1, V2) -> a__isNat#(V1)) (a__U71#(tt(), M, N) -> mark#(M), mark#(s(X)) -> mark#(X)) (a__U71#(tt(), M, N) -> mark#(M), mark#(isNatKind(X)) -> a__isNatKind#(X)) (a__U71#(tt(), M, N) -> mark#(M), mark#(plus(X1, X2)) -> mark#(X1)) (a__U71#(tt(), M, N) -> mark#(M), mark#(plus(X1, X2)) -> mark#(X2)) (a__U71#(tt(), M, N) -> mark#(M), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2))) (a__U71#(tt(), M, N) -> mark#(M), mark#(x(X1, X2)) -> mark#(X1)) (a__U71#(tt(), M, N) -> mark#(M), mark#(x(X1, X2)) -> mark#(X2)) (a__U71#(tt(), M, N) -> mark#(M), mark#(x(X1, X2)) -> a__x#(mark(X1), mark(X2))) (a__U71#(tt(), M, N) -> mark#(M), mark#(and(X1, X2)) -> mark#(X1)) (a__U71#(tt(), M, N) -> mark#(M), mark#(and(X1, X2)) -> a__and#(mark(X1), X2)) (a__U71#(tt(), M, N) -> mark#(M), mark#(isNat(X)) -> a__isNat#(X)) (a__U71#(tt(), M, N) -> mark#(M), mark#(U11(X1, X2, X3)) -> a__U11#(mark(X1), X2, X3)) (a__U71#(tt(), M, N) -> mark#(M), mark#(U11(X1, X2, X3)) -> mark#(X1)) (a__U71#(tt(), M, N) -> mark#(M), mark#(U12(X1, X2)) -> a__U12#(mark(X1), X2)) (a__U71#(tt(), M, N) -> mark#(M), mark#(U12(X1, X2)) -> mark#(X1)) (a__U71#(tt(), M, N) -> mark#(M), mark#(U13(X)) -> a__U13#(mark(X))) (a__U71#(tt(), M, N) -> mark#(M), mark#(U13(X)) -> mark#(X)) (a__U71#(tt(), M, N) -> mark#(M), mark#(U21(X1, X2)) -> a__U21#(mark(X1), X2)) (a__U71#(tt(), M, N) -> mark#(M), mark#(U21(X1, X2)) -> mark#(X1)) (a__U71#(tt(), M, N) -> mark#(M), mark#(U22(X)) -> a__U22#(mark(X))) (a__U71#(tt(), M, N) -> mark#(M), mark#(U22(X)) -> mark#(X)) (a__U71#(tt(), M, N) -> mark#(M), mark#(U31(X1, X2, X3)) -> a__U31#(mark(X1), X2, X3)) (a__U71#(tt(), M, N) -> mark#(M), mark#(U31(X1, X2, X3)) -> mark#(X1)) (a__U71#(tt(), M, N) -> mark#(M), mark#(U32(X1, X2)) -> a__U32#(mark(X1), X2)) (a__U71#(tt(), M, N) -> mark#(M), mark#(U32(X1, X2)) -> mark#(X1)) (a__U71#(tt(), M, N) -> mark#(M), mark#(U33(X)) -> a__U33#(mark(X))) (a__U71#(tt(), M, N) -> mark#(M), mark#(U33(X)) -> mark#(X)) (a__U71#(tt(), M, N) -> mark#(M), mark#(U41(X1, X2)) -> mark#(X1)) (a__U71#(tt(), M, N) -> mark#(M), mark#(U41(X1, X2)) -> a__U41#(mark(X1), X2)) (a__U71#(tt(), M, N) -> mark#(M), mark#(U51(X1, X2, X3)) -> mark#(X1)) (a__U71#(tt(), M, N) -> mark#(M), mark#(U51(X1, X2, X3)) -> a__U51#(mark(X1), X2, X3)) (a__U71#(tt(), M, N) -> mark#(M), mark#(U61(X)) -> mark#(X)) (a__U71#(tt(), M, N) -> mark#(M), mark#(U61(X)) -> a__U61#(mark(X))) (a__U71#(tt(), M, N) -> mark#(M), mark#(U71(X1, X2, X3)) -> mark#(X1)) (a__U71#(tt(), M, N) -> mark#(M), mark#(U71(X1, X2, X3)) -> a__U71#(mark(X1), X2, X3)) (a__U51#(tt(), M, N) -> mark#(M), mark#(s(X)) -> mark#(X)) (a__U51#(tt(), M, N) -> mark#(M), mark#(isNatKind(X)) -> a__isNatKind#(X)) (a__U51#(tt(), M, N) -> mark#(M), mark#(plus(X1, X2)) -> mark#(X1)) (a__U51#(tt(), M, N) -> mark#(M), mark#(plus(X1, X2)) -> mark#(X2)) (a__U51#(tt(), M, N) -> mark#(M), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2))) (a__U51#(tt(), M, N) -> mark#(M), mark#(x(X1, X2)) -> mark#(X1)) (a__U51#(tt(), M, N) -> mark#(M), mark#(x(X1, X2)) -> mark#(X2)) (a__U51#(tt(), M, N) -> mark#(M), mark#(x(X1, X2)) -> a__x#(mark(X1), mark(X2))) (a__U51#(tt(), M, N) -> mark#(M), mark#(and(X1, X2)) -> mark#(X1)) (a__U51#(tt(), M, N) -> mark#(M), mark#(and(X1, X2)) -> a__and#(mark(X1), X2)) (a__U51#(tt(), M, N) -> mark#(M), mark#(isNat(X)) -> a__isNat#(X)) (a__U51#(tt(), M, N) -> mark#(M), mark#(U11(X1, X2, X3)) -> a__U11#(mark(X1), X2, X3)) (a__U51#(tt(), M, N) -> mark#(M), mark#(U11(X1, X2, X3)) -> mark#(X1)) (a__U51#(tt(), M, N) -> mark#(M), mark#(U12(X1, X2)) -> a__U12#(mark(X1), X2)) (a__U51#(tt(), M, N) -> mark#(M), mark#(U12(X1, X2)) -> mark#(X1)) (a__U51#(tt(), M, N) -> mark#(M), mark#(U13(X)) -> a__U13#(mark(X))) (a__U51#(tt(), M, N) -> mark#(M), mark#(U13(X)) -> mark#(X)) (a__U51#(tt(), M, N) -> mark#(M), mark#(U21(X1, X2)) -> a__U21#(mark(X1), X2)) (a__U51#(tt(), M, N) -> mark#(M), mark#(U21(X1, X2)) -> mark#(X1)) (a__U51#(tt(), M, N) -> mark#(M), mark#(U22(X)) -> a__U22#(mark(X))) (a__U51#(tt(), M, N) -> mark#(M), mark#(U22(X)) -> mark#(X)) (a__U51#(tt(), M, N) -> mark#(M), mark#(U31(X1, X2, X3)) -> a__U31#(mark(X1), X2, X3)) (a__U51#(tt(), M, N) -> mark#(M), mark#(U31(X1, X2, X3)) -> mark#(X1)) (a__U51#(tt(), M, N) -> mark#(M), mark#(U32(X1, X2)) -> a__U32#(mark(X1), X2)) (a__U51#(tt(), M, N) -> mark#(M), mark#(U32(X1, X2)) -> mark#(X1)) (a__U51#(tt(), M, N) -> mark#(M), mark#(U33(X)) -> a__U33#(mark(X))) (a__U51#(tt(), M, N) -> mark#(M), mark#(U33(X)) -> mark#(X)) (a__U51#(tt(), M, N) -> mark#(M), mark#(U41(X1, X2)) -> mark#(X1)) (a__U51#(tt(), M, N) -> mark#(M), mark#(U41(X1, X2)) -> a__U41#(mark(X1), X2)) (a__U51#(tt(), M, N) -> mark#(M), mark#(U51(X1, X2, X3)) -> mark#(X1)) (a__U51#(tt(), M, N) -> mark#(M), mark#(U51(X1, X2, X3)) -> a__U51#(mark(X1), X2, X3)) (a__U51#(tt(), M, N) -> mark#(M), mark#(U61(X)) -> mark#(X)) (a__U51#(tt(), M, N) -> mark#(M), mark#(U61(X)) -> a__U61#(mark(X))) (a__U51#(tt(), M, N) -> mark#(M), mark#(U71(X1, X2, X3)) -> mark#(X1)) (a__U51#(tt(), M, N) -> mark#(M), mark#(U71(X1, X2, X3)) -> a__U71#(mark(X1), X2, X3)) (a__U12#(tt(), V2) -> a__isNat#(V2), a__isNat#(s(V1)) -> a__U21#(a__isNatKind(V1), V1)) (a__U12#(tt(), V2) -> a__isNat#(V2), a__isNat#(s(V1)) -> a__isNatKind#(V1)) (a__U12#(tt(), V2) -> a__isNat#(V2), a__isNat#(plus(V1, V2)) -> a__U11#(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)) (a__U12#(tt(), V2) -> a__isNat#(V2), a__isNat#(plus(V1, V2)) -> a__and#(a__isNatKind(V1), isNatKind(V2))) (a__U12#(tt(), V2) -> a__isNat#(V2), a__isNat#(plus(V1, V2)) -> a__isNatKind#(V1)) (a__U12#(tt(), V2) -> a__isNat#(V2), a__isNat#(x(V1, V2)) -> a__U31#(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2)) (a__U12#(tt(), V2) -> a__isNat#(V2), a__isNat#(x(V1, V2)) -> a__and#(a__isNatKind(V1), isNatKind(V2))) (a__U12#(tt(), V2) -> a__isNat#(V2), a__isNat#(x(V1, V2)) -> a__isNatKind#(V1)) (a__plus#(N, s(M)) -> a__U51#(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N), a__U51#(tt(), M, N) -> mark#(N)) (a__plus#(N, s(M)) -> a__U51#(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N), a__U51#(tt(), M, N) -> mark#(M)) (a__plus#(N, s(M)) -> a__U51#(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N), a__U51#(tt(), M, N) -> a__plus#(mark(N), mark(M))) } SCCS: Scc: { a__U12#(tt(), V2) -> a__isNat#(V2), a__isNat#(s(V1)) -> a__U21#(a__isNatKind(V1), V1), a__isNat#(s(V1)) -> a__isNatKind#(V1), a__isNat#(plus(V1, V2)) -> a__U11#(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2), a__isNat#(plus(V1, V2)) -> a__and#(a__isNatKind(V1), isNatKind(V2)), a__isNat#(plus(V1, V2)) -> a__isNatKind#(V1), a__isNat#(x(V1, V2)) -> a__U31#(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2), a__isNat#(x(V1, V2)) -> a__and#(a__isNatKind(V1), isNatKind(V2)), a__isNat#(x(V1, V2)) -> a__isNatKind#(V1), a__U11#(tt(), V1, V2) -> a__U12#(a__isNat(V1), V2), a__U11#(tt(), V1, V2) -> a__isNat#(V1), a__U21#(tt(), V1) -> a__isNat#(V1), a__U32#(tt(), V2) -> a__isNat#(V2), a__U31#(tt(), V1, V2) -> a__isNat#(V1), a__U31#(tt(), V1, V2) -> a__U32#(a__isNat(V1), V2), mark#(s(X)) -> mark#(X), mark#(isNatKind(X)) -> a__isNatKind#(X), mark#(plus(X1, X2)) -> mark#(X1), mark#(plus(X1, X2)) -> mark#(X2), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)), mark#(x(X1, X2)) -> mark#(X1), mark#(x(X1, X2)) -> mark#(X2), mark#(x(X1, X2)) -> a__x#(mark(X1), mark(X2)), mark#(and(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), X2), mark#(isNat(X)) -> a__isNat#(X), mark#(U11(X1, X2, X3)) -> a__U11#(mark(X1), X2, X3), mark#(U11(X1, X2, X3)) -> mark#(X1), mark#(U12(X1, X2)) -> a__U12#(mark(X1), X2), mark#(U12(X1, X2)) -> mark#(X1), mark#(U13(X)) -> mark#(X), mark#(U21(X1, X2)) -> a__U21#(mark(X1), X2), mark#(U21(X1, X2)) -> mark#(X1), mark#(U22(X)) -> mark#(X), mark#(U31(X1, X2, X3)) -> a__U31#(mark(X1), X2, X3), mark#(U31(X1, X2, X3)) -> mark#(X1), mark#(U32(X1, X2)) -> a__U32#(mark(X1), X2), mark#(U32(X1, X2)) -> mark#(X1), mark#(U33(X)) -> mark#(X), mark#(U41(X1, X2)) -> mark#(X1), mark#(U41(X1, X2)) -> a__U41#(mark(X1), X2), mark#(U51(X1, X2, X3)) -> mark#(X1), mark#(U51(X1, X2, X3)) -> a__U51#(mark(X1), X2, X3), mark#(U61(X)) -> mark#(X), mark#(U71(X1, X2, X3)) -> mark#(X1), mark#(U71(X1, X2, X3)) -> a__U71#(mark(X1), X2, X3), a__U41#(tt(), N) -> mark#(N), a__plus#(N, s(M)) -> a__isNat#(M), a__plus#(N, s(M)) -> a__U51#(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N), a__plus#(N, s(M)) -> a__and#(a__isNat(M), isNatKind(M)), a__plus#(N, s(M)) -> a__and#(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), a__plus#(N, 0()) -> a__isNat#(N), a__plus#(N, 0()) -> a__U41#(a__and(a__isNat(N), isNatKind(N)), N), a__plus#(N, 0()) -> a__and#(a__isNat(N), isNatKind(N)), a__U51#(tt(), M, N) -> mark#(N), a__U51#(tt(), M, N) -> mark#(M), a__U51#(tt(), M, N) -> a__plus#(mark(N), mark(M)), a__x#(N, s(M)) -> a__isNat#(M), a__x#(N, s(M)) -> a__U71#(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N), a__x#(N, s(M)) -> a__and#(a__isNat(M), isNatKind(M)), a__x#(N, s(M)) -> a__and#(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), a__x#(N, 0()) -> a__isNat#(N), a__x#(N, 0()) -> a__and#(a__isNat(N), isNatKind(N)), a__U71#(tt(), M, N) -> mark#(N), a__U71#(tt(), M, N) -> mark#(M), a__U71#(tt(), M, N) -> a__plus#(a__x(mark(N), mark(M)), mark(N)), a__U71#(tt(), M, N) -> a__x#(mark(N), mark(M)), a__and#(tt(), X) -> mark#(X), a__isNatKind#(s(V1)) -> a__isNatKind#(V1), a__isNatKind#(plus(V1, V2)) -> a__and#(a__isNatKind(V1), isNatKind(V2)), a__isNatKind#(plus(V1, V2)) -> a__isNatKind#(V1), a__isNatKind#(x(V1, V2)) -> a__and#(a__isNatKind(V1), isNatKind(V2)), a__isNatKind#(x(V1, V2)) -> a__isNatKind#(V1)} SCC: Strict: { a__U12#(tt(), V2) -> a__isNat#(V2), a__isNat#(s(V1)) -> a__U21#(a__isNatKind(V1), V1), a__isNat#(s(V1)) -> a__isNatKind#(V1), a__isNat#(plus(V1, V2)) -> a__U11#(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2), a__isNat#(plus(V1, V2)) -> a__and#(a__isNatKind(V1), isNatKind(V2)), a__isNat#(plus(V1, V2)) -> a__isNatKind#(V1), a__isNat#(x(V1, V2)) -> a__U31#(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2), a__isNat#(x(V1, V2)) -> a__and#(a__isNatKind(V1), isNatKind(V2)), a__isNat#(x(V1, V2)) -> a__isNatKind#(V1), a__U11#(tt(), V1, V2) -> a__U12#(a__isNat(V1), V2), a__U11#(tt(), V1, V2) -> a__isNat#(V1), a__U21#(tt(), V1) -> a__isNat#(V1), a__U32#(tt(), V2) -> a__isNat#(V2), a__U31#(tt(), V1, V2) -> a__isNat#(V1), a__U31#(tt(), V1, V2) -> a__U32#(a__isNat(V1), V2), mark#(s(X)) -> mark#(X), mark#(isNatKind(X)) -> a__isNatKind#(X), mark#(plus(X1, X2)) -> mark#(X1), mark#(plus(X1, X2)) -> mark#(X2), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)), mark#(x(X1, X2)) -> mark#(X1), mark#(x(X1, X2)) -> mark#(X2), mark#(x(X1, X2)) -> a__x#(mark(X1), mark(X2)), mark#(and(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), X2), mark#(isNat(X)) -> a__isNat#(X), mark#(U11(X1, X2, X3)) -> a__U11#(mark(X1), X2, X3), mark#(U11(X1, X2, X3)) -> mark#(X1), mark#(U12(X1, X2)) -> a__U12#(mark(X1), X2), mark#(U12(X1, X2)) -> mark#(X1), mark#(U13(X)) -> mark#(X), mark#(U21(X1, X2)) -> a__U21#(mark(X1), X2), mark#(U21(X1, X2)) -> mark#(X1), mark#(U22(X)) -> mark#(X), mark#(U31(X1, X2, X3)) -> a__U31#(mark(X1), X2, X3), mark#(U31(X1, X2, X3)) -> mark#(X1), mark#(U32(X1, X2)) -> a__U32#(mark(X1), X2), mark#(U32(X1, X2)) -> mark#(X1), mark#(U33(X)) -> mark#(X), mark#(U41(X1, X2)) -> mark#(X1), mark#(U41(X1, X2)) -> a__U41#(mark(X1), X2), mark#(U51(X1, X2, X3)) -> mark#(X1), mark#(U51(X1, X2, X3)) -> a__U51#(mark(X1), X2, X3), mark#(U61(X)) -> mark#(X), mark#(U71(X1, X2, X3)) -> mark#(X1), mark#(U71(X1, X2, X3)) -> a__U71#(mark(X1), X2, X3), a__U41#(tt(), N) -> mark#(N), a__plus#(N, s(M)) -> a__isNat#(M), a__plus#(N, s(M)) -> a__U51#(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N), a__plus#(N, s(M)) -> a__and#(a__isNat(M), isNatKind(M)), a__plus#(N, s(M)) -> a__and#(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), a__plus#(N, 0()) -> a__isNat#(N), a__plus#(N, 0()) -> a__U41#(a__and(a__isNat(N), isNatKind(N)), N), a__plus#(N, 0()) -> a__and#(a__isNat(N), isNatKind(N)), a__U51#(tt(), M, N) -> mark#(N), a__U51#(tt(), M, N) -> mark#(M), a__U51#(tt(), M, N) -> a__plus#(mark(N), mark(M)), a__x#(N, s(M)) -> a__isNat#(M), a__x#(N, s(M)) -> a__U71#(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N), a__x#(N, s(M)) -> a__and#(a__isNat(M), isNatKind(M)), a__x#(N, s(M)) -> a__and#(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), a__x#(N, 0()) -> a__isNat#(N), a__x#(N, 0()) -> a__and#(a__isNat(N), isNatKind(N)), a__U71#(tt(), M, N) -> mark#(N), a__U71#(tt(), M, N) -> mark#(M), a__U71#(tt(), M, N) -> a__plus#(a__x(mark(N), mark(M)), mark(N)), a__U71#(tt(), M, N) -> a__x#(mark(N), mark(M)), a__and#(tt(), X) -> mark#(X), a__isNatKind#(s(V1)) -> a__isNatKind#(V1), a__isNatKind#(plus(V1, V2)) -> a__and#(a__isNatKind(V1), isNatKind(V2)), a__isNatKind#(plus(V1, V2)) -> a__isNatKind#(V1), a__isNatKind#(x(V1, V2)) -> a__and#(a__isNatKind(V1), isNatKind(V2)), a__isNatKind#(x(V1, V2)) -> a__isNatKind#(V1)} Weak: { a__U12(X1, X2) -> U12(X1, X2), a__U12(tt(), V2) -> a__U13(a__isNat(V2)), a__isNat(X) -> isNat(X), a__isNat(s(V1)) -> a__U21(a__isNatKind(V1), V1), a__isNat(0()) -> tt(), a__isNat(plus(V1, V2)) -> a__U11(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2), a__isNat(x(V1, V2)) -> a__U31(a__and(a__isNatKind(V1), isNatKind(V2)), V1, V2), a__U11(X1, X2, X3) -> U11(X1, X2, X3), a__U11(tt(), V1, V2) -> a__U12(a__isNat(V1), V2), a__U13(X) -> U13(X), a__U13(tt()) -> tt(), a__U22(X) -> U22(X), a__U22(tt()) -> tt(), a__U21(X1, X2) -> U21(X1, X2), a__U21(tt(), V1) -> a__U22(a__isNat(V1)), a__U32(X1, X2) -> U32(X1, X2), a__U32(tt(), V2) -> a__U33(a__isNat(V2)), a__U31(X1, X2, X3) -> U31(X1, X2, X3), a__U31(tt(), V1, V2) -> a__U32(a__isNat(V1), V2), a__U33(X) -> U33(X), a__U33(tt()) -> tt(), mark(tt()) -> tt(), mark(s(X)) -> s(mark(X)), mark(0()) -> 0(), mark(isNatKind(X)) -> a__isNatKind(X), mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)), mark(x(X1, X2)) -> a__x(mark(X1), mark(X2)), mark(and(X1, X2)) -> a__and(mark(X1), X2), mark(isNat(X)) -> a__isNat(X), mark(U11(X1, X2, X3)) -> a__U11(mark(X1), X2, X3), mark(U12(X1, X2)) -> a__U12(mark(X1), X2), mark(U13(X)) -> a__U13(mark(X)), mark(U21(X1, X2)) -> a__U21(mark(X1), X2), mark(U22(X)) -> a__U22(mark(X)), mark(U31(X1, X2, X3)) -> a__U31(mark(X1), X2, X3), mark(U32(X1, X2)) -> a__U32(mark(X1), X2), mark(U33(X)) -> a__U33(mark(X)), mark(U41(X1, X2)) -> a__U41(mark(X1), X2), mark(U51(X1, X2, X3)) -> a__U51(mark(X1), X2, X3), mark(U61(X)) -> a__U61(mark(X)), mark(U71(X1, X2, X3)) -> a__U71(mark(X1), X2, X3), a__U41(X1, X2) -> U41(X1, X2), a__U41(tt(), N) -> mark(N), a__plus(N, s(M)) -> a__U51(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N), a__plus(N, 0()) -> a__U41(a__and(a__isNat(N), isNatKind(N)), N), a__plus(X1, X2) -> plus(X1, X2), a__U51(X1, X2, X3) -> U51(X1, X2, X3), a__U51(tt(), M, N) -> s(a__plus(mark(N), mark(M))), a__U61(X) -> U61(X), a__U61(tt()) -> 0(), a__x(N, s(M)) -> a__U71(a__and(a__and(a__isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N), a__x(N, 0()) -> a__U61(a__and(a__isNat(N), isNatKind(N))), a__x(X1, X2) -> x(X1, X2), a__U71(X1, X2, X3) -> U71(X1, X2, X3), a__U71(tt(), M, N) -> a__plus(a__x(mark(N), mark(M)), mark(N)), a__and(X1, X2) -> and(X1, X2), a__and(tt(), X) -> mark(X), a__isNatKind(X) -> isNatKind(X), a__isNatKind(s(V1)) -> a__isNatKind(V1), a__isNatKind(0()) -> tt(), a__isNatKind(plus(V1, V2)) -> a__and(a__isNatKind(V1), isNatKind(V2)), a__isNatKind(x(V1, V2)) -> a__and(a__isNatKind(V1), isNatKind(V2))} Fail