MAYBE TRS: { mark(tt()) -> tt(), mark(s(X)) -> s(mark(X)), mark(0()) -> 0(), mark(isNat(X)) -> a__isNat(X), mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)), mark(x(X1, X2)) -> a__x(mark(X1), mark(X2)), mark(U11(X1, X2)) -> a__U11(mark(X1), X2), mark(U21(X1, X2, X3)) -> a__U21(mark(X1), X2, X3), mark(U31(X)) -> a__U31(mark(X)), mark(U41(X1, X2, X3)) -> a__U41(mark(X1), X2, X3), mark(and(X1, X2)) -> a__and(mark(X1), X2), a__U11(X1, X2) -> U11(X1, X2), a__U11(tt(), N) -> mark(N), a__plus(N, s(M)) -> a__U21(a__and(a__isNat(M), isNat(N)), M, N), a__plus(N, 0()) -> a__U11(a__isNat(N), N), a__plus(X1, X2) -> plus(X1, X2), a__U21(X1, X2, X3) -> U21(X1, X2, X3), a__U21(tt(), M, N) -> s(a__plus(mark(N), mark(M))), a__U31(X) -> U31(X), a__U31(tt()) -> 0(), a__x(N, s(M)) -> a__U41(a__and(a__isNat(M), isNat(N)), M, N), a__x(N, 0()) -> a__U31(a__isNat(N)), a__x(X1, X2) -> x(X1, X2), a__U41(X1, X2, X3) -> U41(X1, X2, X3), a__U41(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__isNat(X) -> isNat(X), a__isNat(s(V1)) -> a__isNat(V1), a__isNat(0()) -> tt(), a__isNat(plus(V1, V2)) -> a__and(a__isNat(V1), isNat(V2)), a__isNat(x(V1, V2)) -> a__and(a__isNat(V1), isNat(V2))} DP: Strict: { mark#(s(X)) -> mark#(X), mark#(isNat(X)) -> a__isNat#(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#(U11(X1, X2)) -> mark#(X1), mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2), mark#(U21(X1, X2, X3)) -> mark#(X1), mark#(U21(X1, X2, X3)) -> a__U21#(mark(X1), X2, X3), mark#(U31(X)) -> mark#(X), mark#(U31(X)) -> a__U31#(mark(X)), mark#(U41(X1, X2, X3)) -> mark#(X1), mark#(U41(X1, X2, X3)) -> a__U41#(mark(X1), X2, X3), mark#(and(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), X2), a__U11#(tt(), N) -> mark#(N), a__plus#(N, s(M)) -> a__U21#(a__and(a__isNat(M), isNat(N)), M, N), a__plus#(N, s(M)) -> a__and#(a__isNat(M), isNat(N)), a__plus#(N, s(M)) -> a__isNat#(M), a__plus#(N, 0()) -> a__U11#(a__isNat(N), N), a__plus#(N, 0()) -> a__isNat#(N), a__U21#(tt(), M, N) -> mark#(N), a__U21#(tt(), M, N) -> mark#(M), a__U21#(tt(), M, N) -> a__plus#(mark(N), mark(M)), a__x#(N, s(M)) -> a__U41#(a__and(a__isNat(M), isNat(N)), M, N), a__x#(N, s(M)) -> a__and#(a__isNat(M), isNat(N)), a__x#(N, s(M)) -> a__isNat#(M), a__x#(N, 0()) -> a__U31#(a__isNat(N)), a__x#(N, 0()) -> a__isNat#(N), a__U41#(tt(), M, N) -> mark#(N), a__U41#(tt(), M, N) -> mark#(M), a__U41#(tt(), M, N) -> a__plus#(a__x(mark(N), mark(M)), mark(N)), a__U41#(tt(), M, N) -> a__x#(mark(N), mark(M)), a__and#(tt(), X) -> mark#(X), a__isNat#(s(V1)) -> a__isNat#(V1), a__isNat#(plus(V1, V2)) -> a__and#(a__isNat(V1), isNat(V2)), a__isNat#(plus(V1, V2)) -> a__isNat#(V1), a__isNat#(x(V1, V2)) -> a__and#(a__isNat(V1), isNat(V2)), a__isNat#(x(V1, V2)) -> a__isNat#(V1)} Weak: { mark(tt()) -> tt(), mark(s(X)) -> s(mark(X)), mark(0()) -> 0(), mark(isNat(X)) -> a__isNat(X), mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)), mark(x(X1, X2)) -> a__x(mark(X1), mark(X2)), mark(U11(X1, X2)) -> a__U11(mark(X1), X2), mark(U21(X1, X2, X3)) -> a__U21(mark(X1), X2, X3), mark(U31(X)) -> a__U31(mark(X)), mark(U41(X1, X2, X3)) -> a__U41(mark(X1), X2, X3), mark(and(X1, X2)) -> a__and(mark(X1), X2), a__U11(X1, X2) -> U11(X1, X2), a__U11(tt(), N) -> mark(N), a__plus(N, s(M)) -> a__U21(a__and(a__isNat(M), isNat(N)), M, N), a__plus(N, 0()) -> a__U11(a__isNat(N), N), a__plus(X1, X2) -> plus(X1, X2), a__U21(X1, X2, X3) -> U21(X1, X2, X3), a__U21(tt(), M, N) -> s(a__plus(mark(N), mark(M))), a__U31(X) -> U31(X), a__U31(tt()) -> 0(), a__x(N, s(M)) -> a__U41(a__and(a__isNat(M), isNat(N)), M, N), a__x(N, 0()) -> a__U31(a__isNat(N)), a__x(X1, X2) -> x(X1, X2), a__U41(X1, X2, X3) -> U41(X1, X2, X3), a__U41(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__isNat(X) -> isNat(X), a__isNat(s(V1)) -> a__isNat(V1), a__isNat(0()) -> tt(), a__isNat(plus(V1, V2)) -> a__and(a__isNat(V1), isNat(V2)), a__isNat(x(V1, V2)) -> a__and(a__isNat(V1), isNat(V2))} EDG: { (a__plus#(N, 0()) -> a__U11#(a__isNat(N), N), a__U11#(tt(), N) -> mark#(N)) (mark#(plus(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), X2)) (mark#(plus(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X1)) (mark#(plus(X1, X2)) -> mark#(X1), mark#(U41(X1, X2, X3)) -> a__U41#(mark(X1), X2, X3)) (mark#(plus(X1, X2)) -> mark#(X1), mark#(U41(X1, X2, X3)) -> mark#(X1)) (mark#(plus(X1, X2)) -> mark#(X1), mark#(U31(X)) -> a__U31#(mark(X))) (mark#(plus(X1, X2)) -> mark#(X1), mark#(U31(X)) -> mark#(X)) (mark#(plus(X1, X2)) -> mark#(X1), mark#(U21(X1, X2, X3)) -> a__U21#(mark(X1), X2, X3)) (mark#(plus(X1, X2)) -> mark#(X1), mark#(U21(X1, X2, X3)) -> mark#(X1)) (mark#(plus(X1, X2)) -> mark#(X1), mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2)) (mark#(plus(X1, X2)) -> mark#(X1), mark#(U11(X1, X2)) -> mark#(X1)) (mark#(plus(X1, X2)) -> mark#(X1), mark#(x(X1, X2)) -> a__x#(mark(X1), mark(X2))) (mark#(plus(X1, X2)) -> mark#(X1), mark#(x(X1, X2)) -> mark#(X2)) (mark#(plus(X1, X2)) -> mark#(X1), mark#(x(X1, X2)) -> mark#(X1)) (mark#(plus(X1, X2)) -> mark#(X1), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2))) (mark#(plus(X1, X2)) -> mark#(X1), mark#(plus(X1, X2)) -> mark#(X2)) (mark#(plus(X1, X2)) -> mark#(X1), mark#(plus(X1, X2)) -> mark#(X1)) (mark#(plus(X1, X2)) -> mark#(X1), mark#(isNat(X)) -> a__isNat#(X)) (mark#(plus(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(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#(U41(X1, X2, X3)) -> a__U41#(mark(X1), X2, X3)) (mark#(x(X1, X2)) -> mark#(X1), mark#(U41(X1, X2, X3)) -> mark#(X1)) (mark#(x(X1, X2)) -> mark#(X1), mark#(U31(X)) -> a__U31#(mark(X))) (mark#(x(X1, X2)) -> mark#(X1), mark#(U31(X)) -> mark#(X)) (mark#(x(X1, X2)) -> mark#(X1), mark#(U21(X1, X2, X3)) -> a__U21#(mark(X1), X2, X3)) (mark#(x(X1, X2)) -> mark#(X1), mark#(U21(X1, X2, X3)) -> mark#(X1)) (mark#(x(X1, X2)) -> mark#(X1), mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2)) (mark#(x(X1, X2)) -> mark#(X1), mark#(U11(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#(isNat(X)) -> a__isNat#(X)) (mark#(x(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X)) (mark#(U11(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), X2)) (mark#(U11(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X1)) (mark#(U11(X1, X2)) -> mark#(X1), mark#(U41(X1, X2, X3)) -> a__U41#(mark(X1), X2, X3)) (mark#(U11(X1, X2)) -> mark#(X1), mark#(U41(X1, X2, X3)) -> mark#(X1)) (mark#(U11(X1, X2)) -> mark#(X1), mark#(U31(X)) -> a__U31#(mark(X))) (mark#(U11(X1, X2)) -> mark#(X1), mark#(U31(X)) -> mark#(X)) (mark#(U11(X1, X2)) -> mark#(X1), mark#(U21(X1, X2, X3)) -> a__U21#(mark(X1), X2, X3)) (mark#(U11(X1, X2)) -> mark#(X1), mark#(U21(X1, X2, X3)) -> mark#(X1)) (mark#(U11(X1, X2)) -> mark#(X1), mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2)) (mark#(U11(X1, X2)) -> mark#(X1), mark#(U11(X1, X2)) -> mark#(X1)) (mark#(U11(X1, X2)) -> mark#(X1), mark#(x(X1, X2)) -> a__x#(mark(X1), mark(X2))) (mark#(U11(X1, X2)) -> mark#(X1), mark#(x(X1, X2)) -> mark#(X2)) (mark#(U11(X1, X2)) -> mark#(X1), mark#(x(X1, X2)) -> mark#(X1)) (mark#(U11(X1, X2)) -> mark#(X1), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2))) (mark#(U11(X1, X2)) -> mark#(X1), mark#(plus(X1, X2)) -> mark#(X2)) (mark#(U11(X1, X2)) -> mark#(X1), mark#(plus(X1, X2)) -> mark#(X1)) (mark#(U11(X1, X2)) -> mark#(X1), mark#(isNat(X)) -> a__isNat#(X)) (mark#(U11(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X)) (mark#(U41(X1, X2, X3)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), X2)) (mark#(U41(X1, X2, X3)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X1)) (mark#(U41(X1, X2, X3)) -> mark#(X1), mark#(U41(X1, X2, X3)) -> a__U41#(mark(X1), X2, X3)) (mark#(U41(X1, X2, X3)) -> mark#(X1), mark#(U41(X1, X2, X3)) -> mark#(X1)) (mark#(U41(X1, X2, X3)) -> mark#(X1), mark#(U31(X)) -> a__U31#(mark(X))) (mark#(U41(X1, X2, X3)) -> mark#(X1), mark#(U31(X)) -> mark#(X)) (mark#(U41(X1, X2, X3)) -> mark#(X1), mark#(U21(X1, X2, X3)) -> a__U21#(mark(X1), X2, X3)) (mark#(U41(X1, X2, X3)) -> mark#(X1), mark#(U21(X1, X2, X3)) -> mark#(X1)) (mark#(U41(X1, X2, X3)) -> mark#(X1), mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2)) (mark#(U41(X1, X2, X3)) -> mark#(X1), mark#(U11(X1, X2)) -> mark#(X1)) (mark#(U41(X1, X2, X3)) -> mark#(X1), mark#(x(X1, X2)) -> a__x#(mark(X1), mark(X2))) (mark#(U41(X1, X2, X3)) -> mark#(X1), mark#(x(X1, X2)) -> mark#(X2)) (mark#(U41(X1, X2, X3)) -> mark#(X1), mark#(x(X1, X2)) -> mark#(X1)) (mark#(U41(X1, X2, X3)) -> mark#(X1), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2))) (mark#(U41(X1, X2, X3)) -> mark#(X1), mark#(plus(X1, X2)) -> mark#(X2)) (mark#(U41(X1, X2, X3)) -> mark#(X1), mark#(plus(X1, X2)) -> mark#(X1)) (mark#(U41(X1, X2, X3)) -> mark#(X1), mark#(isNat(X)) -> a__isNat#(X)) (mark#(U41(X1, X2, X3)) -> mark#(X1), mark#(s(X)) -> mark#(X)) (a__plus#(N, s(M)) -> a__and#(a__isNat(M), isNat(N)), a__and#(tt(), X) -> mark#(X)) (a__x#(N, s(M)) -> a__and#(a__isNat(M), isNat(N)), a__and#(tt(), X) -> mark#(X)) (a__U41#(tt(), M, N) -> a__x#(mark(N), mark(M)), a__x#(N, 0()) -> a__isNat#(N)) (a__U41#(tt(), M, N) -> a__x#(mark(N), mark(M)), a__x#(N, 0()) -> a__U31#(a__isNat(N))) (a__U41#(tt(), M, N) -> a__x#(mark(N), mark(M)), a__x#(N, s(M)) -> a__isNat#(M)) (a__U41#(tt(), M, N) -> a__x#(mark(N), mark(M)), a__x#(N, s(M)) -> a__and#(a__isNat(M), isNat(N))) (a__U41#(tt(), M, N) -> a__x#(mark(N), mark(M)), a__x#(N, s(M)) -> a__U41#(a__and(a__isNat(M), isNat(N)), M, N)) (a__isNat#(x(V1, V2)) -> a__and#(a__isNat(V1), isNat(V2)), a__and#(tt(), X) -> mark#(X)) (a__isNat#(plus(V1, V2)) -> a__isNat#(V1), a__isNat#(x(V1, V2)) -> a__isNat#(V1)) (a__isNat#(plus(V1, V2)) -> a__isNat#(V1), a__isNat#(x(V1, V2)) -> a__and#(a__isNat(V1), isNat(V2))) (a__isNat#(plus(V1, V2)) -> a__isNat#(V1), a__isNat#(plus(V1, V2)) -> a__isNat#(V1)) (a__isNat#(plus(V1, V2)) -> a__isNat#(V1), a__isNat#(plus(V1, V2)) -> a__and#(a__isNat(V1), isNat(V2))) (a__isNat#(plus(V1, V2)) -> a__isNat#(V1), a__isNat#(s(V1)) -> a__isNat#(V1)) (a__plus#(N, s(M)) -> a__isNat#(M), a__isNat#(x(V1, V2)) -> a__isNat#(V1)) (a__plus#(N, s(M)) -> a__isNat#(M), a__isNat#(x(V1, V2)) -> a__and#(a__isNat(V1), isNat(V2))) (a__plus#(N, s(M)) -> a__isNat#(M), a__isNat#(plus(V1, V2)) -> a__isNat#(V1)) (a__plus#(N, s(M)) -> a__isNat#(M), a__isNat#(plus(V1, V2)) -> a__and#(a__isNat(V1), isNat(V2))) (a__plus#(N, s(M)) -> a__isNat#(M), a__isNat#(s(V1)) -> a__isNat#(V1)) (a__x#(N, s(M)) -> a__isNat#(M), a__isNat#(x(V1, V2)) -> a__isNat#(V1)) (a__x#(N, s(M)) -> a__isNat#(M), a__isNat#(x(V1, V2)) -> a__and#(a__isNat(V1), isNat(V2))) (a__x#(N, s(M)) -> a__isNat#(M), a__isNat#(plus(V1, V2)) -> a__isNat#(V1)) (a__x#(N, s(M)) -> a__isNat#(M), a__isNat#(plus(V1, V2)) -> a__and#(a__isNat(V1), isNat(V2))) (a__x#(N, s(M)) -> a__isNat#(M), a__isNat#(s(V1)) -> a__isNat#(V1)) (mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2), a__U11#(tt(), N) -> mark#(N)) (a__plus#(N, s(M)) -> a__U21#(a__and(a__isNat(M), isNat(N)), M, N), a__U21#(tt(), M, N) -> a__plus#(mark(N), mark(M))) (a__plus#(N, s(M)) -> a__U21#(a__and(a__isNat(M), isNat(N)), M, N), a__U21#(tt(), M, N) -> mark#(M)) (a__plus#(N, s(M)) -> a__U21#(a__and(a__isNat(M), isNat(N)), M, N), a__U21#(tt(), M, N) -> mark#(N)) (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#(U41(X1, X2, X3)) -> a__U41#(mark(X1), X2, X3)) (mark#(plus(X1, X2)) -> mark#(X2), mark#(U41(X1, X2, X3)) -> mark#(X1)) (mark#(plus(X1, X2)) -> mark#(X2), mark#(U31(X)) -> a__U31#(mark(X))) (mark#(plus(X1, X2)) -> mark#(X2), mark#(U31(X)) -> mark#(X)) (mark#(plus(X1, X2)) -> mark#(X2), mark#(U21(X1, X2, X3)) -> a__U21#(mark(X1), X2, X3)) (mark#(plus(X1, X2)) -> mark#(X2), mark#(U21(X1, X2, X3)) -> mark#(X1)) (mark#(plus(X1, X2)) -> mark#(X2), mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2)) (mark#(plus(X1, X2)) -> mark#(X2), mark#(U11(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#(isNat(X)) -> a__isNat#(X)) (mark#(plus(X1, X2)) -> mark#(X2), mark#(s(X)) -> mark#(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#(U41(X1, X2, X3)) -> a__U41#(mark(X1), X2, X3)) (mark#(s(X)) -> mark#(X), mark#(U41(X1, X2, X3)) -> mark#(X1)) (mark#(s(X)) -> mark#(X), mark#(U31(X)) -> a__U31#(mark(X))) (mark#(s(X)) -> mark#(X), mark#(U31(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(U21(X1, X2, X3)) -> a__U21#(mark(X1), X2, X3)) (mark#(s(X)) -> mark#(X), mark#(U21(X1, X2, X3)) -> mark#(X1)) (mark#(s(X)) -> mark#(X), mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2)) (mark#(s(X)) -> mark#(X), mark#(U11(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#(isNat(X)) -> a__isNat#(X)) (mark#(s(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(U31(X)) -> mark#(X), mark#(and(X1, X2)) -> a__and#(mark(X1), X2)) (mark#(U31(X)) -> mark#(X), mark#(and(X1, X2)) -> mark#(X1)) (mark#(U31(X)) -> mark#(X), mark#(U41(X1, X2, X3)) -> a__U41#(mark(X1), X2, X3)) (mark#(U31(X)) -> mark#(X), mark#(U41(X1, X2, X3)) -> mark#(X1)) (mark#(U31(X)) -> mark#(X), mark#(U31(X)) -> a__U31#(mark(X))) (mark#(U31(X)) -> mark#(X), mark#(U31(X)) -> mark#(X)) (mark#(U31(X)) -> mark#(X), mark#(U21(X1, X2, X3)) -> a__U21#(mark(X1), X2, X3)) (mark#(U31(X)) -> mark#(X), mark#(U21(X1, X2, X3)) -> mark#(X1)) (mark#(U31(X)) -> mark#(X), mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2)) (mark#(U31(X)) -> mark#(X), mark#(U11(X1, X2)) -> mark#(X1)) (mark#(U31(X)) -> mark#(X), mark#(x(X1, X2)) -> a__x#(mark(X1), mark(X2))) (mark#(U31(X)) -> mark#(X), mark#(x(X1, X2)) -> mark#(X2)) (mark#(U31(X)) -> mark#(X), mark#(x(X1, X2)) -> mark#(X1)) (mark#(U31(X)) -> mark#(X), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2))) (mark#(U31(X)) -> mark#(X), mark#(plus(X1, X2)) -> mark#(X2)) (mark#(U31(X)) -> mark#(X), mark#(plus(X1, X2)) -> mark#(X1)) (mark#(U31(X)) -> mark#(X), mark#(isNat(X)) -> a__isNat#(X)) (mark#(U31(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(U21(X1, X2, X3)) -> a__U21#(mark(X1), X2, X3), a__U21#(tt(), M, N) -> a__plus#(mark(N), mark(M))) (mark#(U21(X1, X2, X3)) -> a__U21#(mark(X1), X2, X3), a__U21#(tt(), M, N) -> mark#(M)) (mark#(U21(X1, X2, X3)) -> a__U21#(mark(X1), X2, X3), a__U21#(tt(), M, N) -> mark#(N)) (a__U11#(tt(), N) -> mark#(N), mark#(and(X1, X2)) -> a__and#(mark(X1), X2)) (a__U11#(tt(), N) -> mark#(N), mark#(and(X1, X2)) -> mark#(X1)) (a__U11#(tt(), N) -> mark#(N), mark#(U41(X1, X2, X3)) -> a__U41#(mark(X1), X2, X3)) (a__U11#(tt(), N) -> mark#(N), mark#(U41(X1, X2, X3)) -> mark#(X1)) (a__U11#(tt(), N) -> mark#(N), mark#(U31(X)) -> a__U31#(mark(X))) (a__U11#(tt(), N) -> mark#(N), mark#(U31(X)) -> mark#(X)) (a__U11#(tt(), N) -> mark#(N), mark#(U21(X1, X2, X3)) -> a__U21#(mark(X1), X2, X3)) (a__U11#(tt(), N) -> mark#(N), mark#(U21(X1, X2, X3)) -> mark#(X1)) (a__U11#(tt(), N) -> mark#(N), mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2)) (a__U11#(tt(), N) -> mark#(N), mark#(U11(X1, X2)) -> mark#(X1)) (a__U11#(tt(), N) -> mark#(N), mark#(x(X1, X2)) -> a__x#(mark(X1), mark(X2))) (a__U11#(tt(), N) -> mark#(N), mark#(x(X1, X2)) -> mark#(X2)) (a__U11#(tt(), N) -> mark#(N), mark#(x(X1, X2)) -> mark#(X1)) (a__U11#(tt(), N) -> mark#(N), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2))) (a__U11#(tt(), N) -> mark#(N), mark#(plus(X1, X2)) -> mark#(X2)) (a__U11#(tt(), N) -> mark#(N), mark#(plus(X1, X2)) -> mark#(X1)) (a__U11#(tt(), N) -> mark#(N), mark#(isNat(X)) -> a__isNat#(X)) (a__U11#(tt(), N) -> mark#(N), mark#(s(X)) -> mark#(X)) (a__U21#(tt(), M, N) -> mark#(N), mark#(and(X1, X2)) -> a__and#(mark(X1), X2)) (a__U21#(tt(), M, N) -> mark#(N), mark#(and(X1, X2)) -> mark#(X1)) (a__U21#(tt(), M, N) -> mark#(N), mark#(U41(X1, X2, X3)) -> a__U41#(mark(X1), X2, X3)) (a__U21#(tt(), M, N) -> mark#(N), mark#(U41(X1, X2, X3)) -> mark#(X1)) (a__U21#(tt(), M, N) -> mark#(N), mark#(U31(X)) -> a__U31#(mark(X))) (a__U21#(tt(), M, N) -> mark#(N), mark#(U31(X)) -> mark#(X)) (a__U21#(tt(), M, N) -> mark#(N), mark#(U21(X1, X2, X3)) -> a__U21#(mark(X1), X2, X3)) (a__U21#(tt(), M, N) -> mark#(N), mark#(U21(X1, X2, X3)) -> mark#(X1)) (a__U21#(tt(), M, N) -> mark#(N), mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2)) (a__U21#(tt(), M, N) -> mark#(N), mark#(U11(X1, X2)) -> mark#(X1)) (a__U21#(tt(), M, N) -> mark#(N), mark#(x(X1, X2)) -> a__x#(mark(X1), mark(X2))) (a__U21#(tt(), M, N) -> mark#(N), mark#(x(X1, X2)) -> mark#(X2)) (a__U21#(tt(), M, N) -> mark#(N), mark#(x(X1, X2)) -> mark#(X1)) (a__U21#(tt(), M, N) -> mark#(N), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2))) (a__U21#(tt(), M, N) -> mark#(N), mark#(plus(X1, X2)) -> mark#(X2)) (a__U21#(tt(), M, N) -> mark#(N), mark#(plus(X1, X2)) -> mark#(X1)) (a__U21#(tt(), M, N) -> mark#(N), mark#(isNat(X)) -> a__isNat#(X)) (a__U21#(tt(), M, N) -> mark#(N), mark#(s(X)) -> mark#(X)) (a__U41#(tt(), M, N) -> mark#(N), mark#(and(X1, X2)) -> a__and#(mark(X1), X2)) (a__U41#(tt(), M, N) -> mark#(N), mark#(and(X1, X2)) -> mark#(X1)) (a__U41#(tt(), M, N) -> mark#(N), mark#(U41(X1, X2, X3)) -> a__U41#(mark(X1), X2, X3)) (a__U41#(tt(), M, N) -> mark#(N), mark#(U41(X1, X2, X3)) -> mark#(X1)) (a__U41#(tt(), M, N) -> mark#(N), mark#(U31(X)) -> a__U31#(mark(X))) (a__U41#(tt(), M, N) -> mark#(N), mark#(U31(X)) -> mark#(X)) (a__U41#(tt(), M, N) -> mark#(N), mark#(U21(X1, X2, X3)) -> a__U21#(mark(X1), X2, X3)) (a__U41#(tt(), M, N) -> mark#(N), mark#(U21(X1, X2, X3)) -> mark#(X1)) (a__U41#(tt(), M, N) -> mark#(N), mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2)) (a__U41#(tt(), M, N) -> mark#(N), mark#(U11(X1, X2)) -> mark#(X1)) (a__U41#(tt(), M, N) -> mark#(N), mark#(x(X1, X2)) -> a__x#(mark(X1), mark(X2))) (a__U41#(tt(), M, N) -> mark#(N), mark#(x(X1, X2)) -> mark#(X2)) (a__U41#(tt(), M, N) -> mark#(N), mark#(x(X1, X2)) -> mark#(X1)) (a__U41#(tt(), M, N) -> mark#(N), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2))) (a__U41#(tt(), M, N) -> mark#(N), mark#(plus(X1, X2)) -> mark#(X2)) (a__U41#(tt(), M, N) -> mark#(N), mark#(plus(X1, X2)) -> mark#(X1)) (a__U41#(tt(), M, N) -> mark#(N), mark#(isNat(X)) -> a__isNat#(X)) (a__U41#(tt(), M, N) -> mark#(N), mark#(s(X)) -> mark#(X)) (a__x#(N, 0()) -> a__isNat#(N), a__isNat#(s(V1)) -> a__isNat#(V1)) (a__x#(N, 0()) -> a__isNat#(N), a__isNat#(plus(V1, V2)) -> a__and#(a__isNat(V1), isNat(V2))) (a__x#(N, 0()) -> a__isNat#(N), a__isNat#(plus(V1, V2)) -> a__isNat#(V1)) (a__x#(N, 0()) -> a__isNat#(N), a__isNat#(x(V1, V2)) -> a__and#(a__isNat(V1), isNat(V2))) (a__x#(N, 0()) -> a__isNat#(N), a__isNat#(x(V1, V2)) -> a__isNat#(V1)) (a__plus#(N, 0()) -> a__isNat#(N), a__isNat#(s(V1)) -> a__isNat#(V1)) (a__plus#(N, 0()) -> a__isNat#(N), a__isNat#(plus(V1, V2)) -> a__and#(a__isNat(V1), isNat(V2))) (a__plus#(N, 0()) -> a__isNat#(N), a__isNat#(plus(V1, V2)) -> a__isNat#(V1)) (a__plus#(N, 0()) -> a__isNat#(N), a__isNat#(x(V1, V2)) -> a__and#(a__isNat(V1), isNat(V2))) (a__plus#(N, 0()) -> a__isNat#(N), a__isNat#(x(V1, V2)) -> a__isNat#(V1)) (mark#(U41(X1, X2, X3)) -> a__U41#(mark(X1), X2, X3), a__U41#(tt(), M, N) -> mark#(N)) (mark#(U41(X1, X2, X3)) -> a__U41#(mark(X1), X2, X3), a__U41#(tt(), M, N) -> mark#(M)) (mark#(U41(X1, X2, X3)) -> a__U41#(mark(X1), X2, X3), a__U41#(tt(), M, N) -> a__plus#(a__x(mark(N), mark(M)), mark(N))) (mark#(U41(X1, X2, X3)) -> a__U41#(mark(X1), X2, X3), a__U41#(tt(), M, N) -> a__x#(mark(N), mark(M))) (a__and#(tt(), X) -> mark#(X), mark#(s(X)) -> mark#(X)) (a__and#(tt(), X) -> mark#(X), mark#(isNat(X)) -> a__isNat#(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#(U11(X1, X2)) -> mark#(X1)) (a__and#(tt(), X) -> mark#(X), mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2)) (a__and#(tt(), X) -> mark#(X), mark#(U21(X1, X2, X3)) -> mark#(X1)) (a__and#(tt(), X) -> mark#(X), mark#(U21(X1, X2, X3)) -> a__U21#(mark(X1), X2, X3)) (a__and#(tt(), X) -> mark#(X), mark#(U31(X)) -> mark#(X)) (a__and#(tt(), X) -> mark#(X), mark#(U31(X)) -> a__U31#(mark(X))) (a__and#(tt(), X) -> mark#(X), mark#(U41(X1, X2, X3)) -> mark#(X1)) (a__and#(tt(), X) -> mark#(X), mark#(U41(X1, X2, X3)) -> a__U41#(mark(X1), X2, X3)) (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)) (mark#(isNat(X)) -> a__isNat#(X), a__isNat#(s(V1)) -> a__isNat#(V1)) (mark#(isNat(X)) -> a__isNat#(X), a__isNat#(plus(V1, V2)) -> a__and#(a__isNat(V1), isNat(V2))) (mark#(isNat(X)) -> a__isNat#(X), a__isNat#(plus(V1, V2)) -> a__isNat#(V1)) (mark#(isNat(X)) -> a__isNat#(X), a__isNat#(x(V1, V2)) -> a__and#(a__isNat(V1), isNat(V2))) (mark#(isNat(X)) -> a__isNat#(X), a__isNat#(x(V1, V2)) -> a__isNat#(V1)) (mark#(x(X1, X2)) -> mark#(X2), mark#(s(X)) -> mark#(X)) (mark#(x(X1, X2)) -> mark#(X2), mark#(isNat(X)) -> a__isNat#(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#(U11(X1, X2)) -> mark#(X1)) (mark#(x(X1, X2)) -> mark#(X2), mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2)) (mark#(x(X1, X2)) -> mark#(X2), mark#(U21(X1, X2, X3)) -> mark#(X1)) (mark#(x(X1, X2)) -> mark#(X2), mark#(U21(X1, X2, X3)) -> a__U21#(mark(X1), X2, X3)) (mark#(x(X1, X2)) -> mark#(X2), mark#(U31(X)) -> mark#(X)) (mark#(x(X1, X2)) -> mark#(X2), mark#(U31(X)) -> a__U31#(mark(X))) (mark#(x(X1, X2)) -> mark#(X2), mark#(U41(X1, X2, X3)) -> mark#(X1)) (mark#(x(X1, X2)) -> mark#(X2), mark#(U41(X1, X2, X3)) -> a__U41#(mark(X1), X2, X3)) (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)) (a__x#(N, s(M)) -> a__U41#(a__and(a__isNat(M), isNat(N)), M, N), a__U41#(tt(), M, N) -> mark#(N)) (a__x#(N, s(M)) -> a__U41#(a__and(a__isNat(M), isNat(N)), M, N), a__U41#(tt(), M, N) -> mark#(M)) (a__x#(N, s(M)) -> a__U41#(a__and(a__isNat(M), isNat(N)), M, N), a__U41#(tt(), M, N) -> a__plus#(a__x(mark(N), mark(M)), mark(N))) (a__x#(N, s(M)) -> a__U41#(a__and(a__isNat(M), isNat(N)), M, N), a__U41#(tt(), M, N) -> a__x#(mark(N), mark(M))) (mark#(and(X1, X2)) -> a__and#(mark(X1), X2), a__and#(tt(), X) -> mark#(X)) (a__U41#(tt(), M, N) -> mark#(M), mark#(s(X)) -> mark#(X)) (a__U41#(tt(), M, N) -> mark#(M), mark#(isNat(X)) -> a__isNat#(X)) (a__U41#(tt(), M, N) -> mark#(M), mark#(plus(X1, X2)) -> mark#(X1)) (a__U41#(tt(), M, N) -> mark#(M), mark#(plus(X1, X2)) -> mark#(X2)) (a__U41#(tt(), M, N) -> mark#(M), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2))) (a__U41#(tt(), M, N) -> mark#(M), mark#(x(X1, X2)) -> mark#(X1)) (a__U41#(tt(), M, N) -> mark#(M), mark#(x(X1, X2)) -> mark#(X2)) (a__U41#(tt(), M, N) -> mark#(M), mark#(x(X1, X2)) -> a__x#(mark(X1), mark(X2))) (a__U41#(tt(), M, N) -> mark#(M), mark#(U11(X1, X2)) -> mark#(X1)) (a__U41#(tt(), M, N) -> mark#(M), mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2)) (a__U41#(tt(), M, N) -> mark#(M), mark#(U21(X1, X2, X3)) -> mark#(X1)) (a__U41#(tt(), M, N) -> mark#(M), mark#(U21(X1, X2, X3)) -> a__U21#(mark(X1), X2, X3)) (a__U41#(tt(), M, N) -> mark#(M), mark#(U31(X)) -> mark#(X)) (a__U41#(tt(), M, N) -> mark#(M), mark#(U31(X)) -> a__U31#(mark(X))) (a__U41#(tt(), M, N) -> mark#(M), mark#(U41(X1, X2, X3)) -> mark#(X1)) (a__U41#(tt(), M, N) -> mark#(M), mark#(U41(X1, X2, X3)) -> a__U41#(mark(X1), X2, X3)) (a__U41#(tt(), M, N) -> mark#(M), mark#(and(X1, X2)) -> mark#(X1)) (a__U41#(tt(), M, N) -> mark#(M), mark#(and(X1, X2)) -> a__and#(mark(X1), X2)) (a__U21#(tt(), M, N) -> mark#(M), mark#(s(X)) -> mark#(X)) (a__U21#(tt(), M, N) -> mark#(M), mark#(isNat(X)) -> a__isNat#(X)) (a__U21#(tt(), M, N) -> mark#(M), mark#(plus(X1, X2)) -> mark#(X1)) (a__U21#(tt(), M, N) -> mark#(M), mark#(plus(X1, X2)) -> mark#(X2)) (a__U21#(tt(), M, N) -> mark#(M), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2))) (a__U21#(tt(), M, N) -> mark#(M), mark#(x(X1, X2)) -> mark#(X1)) (a__U21#(tt(), M, N) -> mark#(M), mark#(x(X1, X2)) -> mark#(X2)) (a__U21#(tt(), M, N) -> mark#(M), mark#(x(X1, X2)) -> a__x#(mark(X1), mark(X2))) (a__U21#(tt(), M, N) -> mark#(M), mark#(U11(X1, X2)) -> mark#(X1)) (a__U21#(tt(), M, N) -> mark#(M), mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2)) (a__U21#(tt(), M, N) -> mark#(M), mark#(U21(X1, X2, X3)) -> mark#(X1)) (a__U21#(tt(), M, N) -> mark#(M), mark#(U21(X1, X2, X3)) -> a__U21#(mark(X1), X2, X3)) (a__U21#(tt(), M, N) -> mark#(M), mark#(U31(X)) -> mark#(X)) (a__U21#(tt(), M, N) -> mark#(M), mark#(U31(X)) -> a__U31#(mark(X))) (a__U21#(tt(), M, N) -> mark#(M), mark#(U41(X1, X2, X3)) -> mark#(X1)) (a__U21#(tt(), M, N) -> mark#(M), mark#(U41(X1, X2, X3)) -> a__U41#(mark(X1), X2, X3)) (a__U21#(tt(), M, N) -> mark#(M), mark#(and(X1, X2)) -> mark#(X1)) (a__U21#(tt(), M, N) -> mark#(M), mark#(and(X1, X2)) -> a__and#(mark(X1), X2)) (a__isNat#(x(V1, V2)) -> a__isNat#(V1), a__isNat#(s(V1)) -> a__isNat#(V1)) (a__isNat#(x(V1, V2)) -> a__isNat#(V1), a__isNat#(plus(V1, V2)) -> a__and#(a__isNat(V1), isNat(V2))) (a__isNat#(x(V1, V2)) -> a__isNat#(V1), a__isNat#(plus(V1, V2)) -> a__isNat#(V1)) (a__isNat#(x(V1, V2)) -> a__isNat#(V1), a__isNat#(x(V1, V2)) -> a__and#(a__isNat(V1), isNat(V2))) (a__isNat#(x(V1, V2)) -> a__isNat#(V1), a__isNat#(x(V1, V2)) -> a__isNat#(V1)) (a__isNat#(s(V1)) -> a__isNat#(V1), a__isNat#(s(V1)) -> a__isNat#(V1)) (a__isNat#(s(V1)) -> a__isNat#(V1), a__isNat#(plus(V1, V2)) -> a__and#(a__isNat(V1), isNat(V2))) (a__isNat#(s(V1)) -> a__isNat#(V1), a__isNat#(plus(V1, V2)) -> a__isNat#(V1)) (a__isNat#(s(V1)) -> a__isNat#(V1), a__isNat#(x(V1, V2)) -> a__and#(a__isNat(V1), isNat(V2))) (a__isNat#(s(V1)) -> a__isNat#(V1), a__isNat#(x(V1, V2)) -> a__isNat#(V1)) (a__isNat#(plus(V1, V2)) -> a__and#(a__isNat(V1), isNat(V2)), a__and#(tt(), X) -> mark#(X)) (a__U41#(tt(), M, N) -> a__plus#(a__x(mark(N), mark(M)), mark(N)), a__plus#(N, s(M)) -> a__U21#(a__and(a__isNat(M), isNat(N)), M, N)) (a__U41#(tt(), M, N) -> a__plus#(a__x(mark(N), mark(M)), mark(N)), a__plus#(N, s(M)) -> a__and#(a__isNat(M), isNat(N))) (a__U41#(tt(), M, N) -> a__plus#(a__x(mark(N), mark(M)), mark(N)), a__plus#(N, s(M)) -> a__isNat#(M)) (a__U41#(tt(), M, N) -> a__plus#(a__x(mark(N), mark(M)), mark(N)), a__plus#(N, 0()) -> a__U11#(a__isNat(N), N)) (a__U41#(tt(), M, N) -> a__plus#(a__x(mark(N), mark(M)), mark(N)), a__plus#(N, 0()) -> a__isNat#(N)) (a__U21#(tt(), M, N) -> a__plus#(mark(N), mark(M)), a__plus#(N, s(M)) -> a__U21#(a__and(a__isNat(M), isNat(N)), M, N)) (a__U21#(tt(), M, N) -> a__plus#(mark(N), mark(M)), a__plus#(N, s(M)) -> a__and#(a__isNat(M), isNat(N))) (a__U21#(tt(), M, N) -> a__plus#(mark(N), mark(M)), a__plus#(N, s(M)) -> a__isNat#(M)) (a__U21#(tt(), M, N) -> a__plus#(mark(N), mark(M)), a__plus#(N, 0()) -> a__U11#(a__isNat(N), N)) (a__U21#(tt(), M, N) -> a__plus#(mark(N), mark(M)), a__plus#(N, 0()) -> a__isNat#(N)) (mark#(and(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X)) (mark#(and(X1, X2)) -> mark#(X1), mark#(isNat(X)) -> a__isNat#(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#(U11(X1, X2)) -> mark#(X1)) (mark#(and(X1, X2)) -> mark#(X1), mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2)) (mark#(and(X1, X2)) -> mark#(X1), mark#(U21(X1, X2, X3)) -> mark#(X1)) (mark#(and(X1, X2)) -> mark#(X1), mark#(U21(X1, X2, X3)) -> a__U21#(mark(X1), X2, X3)) (mark#(and(X1, X2)) -> mark#(X1), mark#(U31(X)) -> mark#(X)) (mark#(and(X1, X2)) -> mark#(X1), mark#(U31(X)) -> a__U31#(mark(X))) (mark#(and(X1, X2)) -> mark#(X1), mark#(U41(X1, X2, X3)) -> mark#(X1)) (mark#(and(X1, X2)) -> mark#(X1), mark#(U41(X1, X2, X3)) -> a__U41#(mark(X1), X2, X3)) (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#(U21(X1, X2, X3)) -> mark#(X1), mark#(s(X)) -> mark#(X)) (mark#(U21(X1, X2, X3)) -> mark#(X1), mark#(isNat(X)) -> a__isNat#(X)) (mark#(U21(X1, X2, X3)) -> mark#(X1), mark#(plus(X1, X2)) -> mark#(X1)) (mark#(U21(X1, X2, X3)) -> mark#(X1), mark#(plus(X1, X2)) -> mark#(X2)) (mark#(U21(X1, X2, X3)) -> mark#(X1), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2))) (mark#(U21(X1, X2, X3)) -> mark#(X1), mark#(x(X1, X2)) -> mark#(X1)) (mark#(U21(X1, X2, X3)) -> mark#(X1), mark#(x(X1, X2)) -> mark#(X2)) (mark#(U21(X1, X2, X3)) -> mark#(X1), mark#(x(X1, X2)) -> a__x#(mark(X1), mark(X2))) (mark#(U21(X1, X2, X3)) -> mark#(X1), mark#(U11(X1, X2)) -> mark#(X1)) (mark#(U21(X1, X2, X3)) -> mark#(X1), mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2)) (mark#(U21(X1, X2, X3)) -> mark#(X1), mark#(U21(X1, X2, X3)) -> mark#(X1)) (mark#(U21(X1, X2, X3)) -> mark#(X1), mark#(U21(X1, X2, X3)) -> a__U21#(mark(X1), X2, X3)) (mark#(U21(X1, X2, X3)) -> mark#(X1), mark#(U31(X)) -> mark#(X)) (mark#(U21(X1, X2, X3)) -> mark#(X1), mark#(U31(X)) -> a__U31#(mark(X))) (mark#(U21(X1, X2, X3)) -> mark#(X1), mark#(U41(X1, X2, X3)) -> mark#(X1)) (mark#(U21(X1, X2, X3)) -> mark#(X1), mark#(U41(X1, X2, X3)) -> a__U41#(mark(X1), X2, X3)) (mark#(U21(X1, X2, X3)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X1)) (mark#(U21(X1, X2, X3)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), X2)) (mark#(x(X1, X2)) -> a__x#(mark(X1), mark(X2)), a__x#(N, s(M)) -> a__U41#(a__and(a__isNat(M), isNat(N)), M, N)) (mark#(x(X1, X2)) -> a__x#(mark(X1), mark(X2)), a__x#(N, s(M)) -> a__and#(a__isNat(M), isNat(N))) (mark#(x(X1, X2)) -> a__x#(mark(X1), mark(X2)), a__x#(N, s(M)) -> a__isNat#(M)) (mark#(x(X1, X2)) -> a__x#(mark(X1), mark(X2)), a__x#(N, 0()) -> a__U31#(a__isNat(N))) (mark#(x(X1, X2)) -> a__x#(mark(X1), mark(X2)), a__x#(N, 0()) -> a__isNat#(N)) (mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)), a__plus#(N, s(M)) -> a__U21#(a__and(a__isNat(M), isNat(N)), M, N)) (mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)), a__plus#(N, s(M)) -> a__and#(a__isNat(M), isNat(N))) (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, 0()) -> a__U11#(a__isNat(N), N)) (mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)), a__plus#(N, 0()) -> a__isNat#(N)) } SCCS: Scc: { mark#(s(X)) -> mark#(X), mark#(isNat(X)) -> a__isNat#(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#(U11(X1, X2)) -> mark#(X1), mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2), mark#(U21(X1, X2, X3)) -> mark#(X1), mark#(U21(X1, X2, X3)) -> a__U21#(mark(X1), X2, X3), mark#(U31(X)) -> mark#(X), mark#(U41(X1, X2, X3)) -> mark#(X1), mark#(U41(X1, X2, X3)) -> a__U41#(mark(X1), X2, X3), mark#(and(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), X2), a__U11#(tt(), N) -> mark#(N), a__plus#(N, s(M)) -> a__U21#(a__and(a__isNat(M), isNat(N)), M, N), a__plus#(N, s(M)) -> a__and#(a__isNat(M), isNat(N)), a__plus#(N, s(M)) -> a__isNat#(M), a__plus#(N, 0()) -> a__U11#(a__isNat(N), N), a__plus#(N, 0()) -> a__isNat#(N), a__U21#(tt(), M, N) -> mark#(N), a__U21#(tt(), M, N) -> mark#(M), a__U21#(tt(), M, N) -> a__plus#(mark(N), mark(M)), a__x#(N, s(M)) -> a__U41#(a__and(a__isNat(M), isNat(N)), M, N), a__x#(N, s(M)) -> a__and#(a__isNat(M), isNat(N)), a__x#(N, s(M)) -> a__isNat#(M), a__x#(N, 0()) -> a__isNat#(N), a__U41#(tt(), M, N) -> mark#(N), a__U41#(tt(), M, N) -> mark#(M), a__U41#(tt(), M, N) -> a__plus#(a__x(mark(N), mark(M)), mark(N)), a__U41#(tt(), M, N) -> a__x#(mark(N), mark(M)), a__and#(tt(), X) -> mark#(X), a__isNat#(s(V1)) -> a__isNat#(V1), a__isNat#(plus(V1, V2)) -> a__and#(a__isNat(V1), isNat(V2)), a__isNat#(plus(V1, V2)) -> a__isNat#(V1), a__isNat#(x(V1, V2)) -> a__and#(a__isNat(V1), isNat(V2)), a__isNat#(x(V1, V2)) -> a__isNat#(V1)} SCC: Strict: { mark#(s(X)) -> mark#(X), mark#(isNat(X)) -> a__isNat#(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#(U11(X1, X2)) -> mark#(X1), mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2), mark#(U21(X1, X2, X3)) -> mark#(X1), mark#(U21(X1, X2, X3)) -> a__U21#(mark(X1), X2, X3), mark#(U31(X)) -> mark#(X), mark#(U41(X1, X2, X3)) -> mark#(X1), mark#(U41(X1, X2, X3)) -> a__U41#(mark(X1), X2, X3), mark#(and(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), X2), a__U11#(tt(), N) -> mark#(N), a__plus#(N, s(M)) -> a__U21#(a__and(a__isNat(M), isNat(N)), M, N), a__plus#(N, s(M)) -> a__and#(a__isNat(M), isNat(N)), a__plus#(N, s(M)) -> a__isNat#(M), a__plus#(N, 0()) -> a__U11#(a__isNat(N), N), a__plus#(N, 0()) -> a__isNat#(N), a__U21#(tt(), M, N) -> mark#(N), a__U21#(tt(), M, N) -> mark#(M), a__U21#(tt(), M, N) -> a__plus#(mark(N), mark(M)), a__x#(N, s(M)) -> a__U41#(a__and(a__isNat(M), isNat(N)), M, N), a__x#(N, s(M)) -> a__and#(a__isNat(M), isNat(N)), a__x#(N, s(M)) -> a__isNat#(M), a__x#(N, 0()) -> a__isNat#(N), a__U41#(tt(), M, N) -> mark#(N), a__U41#(tt(), M, N) -> mark#(M), a__U41#(tt(), M, N) -> a__plus#(a__x(mark(N), mark(M)), mark(N)), a__U41#(tt(), M, N) -> a__x#(mark(N), mark(M)), a__and#(tt(), X) -> mark#(X), a__isNat#(s(V1)) -> a__isNat#(V1), a__isNat#(plus(V1, V2)) -> a__and#(a__isNat(V1), isNat(V2)), a__isNat#(plus(V1, V2)) -> a__isNat#(V1), a__isNat#(x(V1, V2)) -> a__and#(a__isNat(V1), isNat(V2)), a__isNat#(x(V1, V2)) -> a__isNat#(V1)} Weak: { mark(tt()) -> tt(), mark(s(X)) -> s(mark(X)), mark(0()) -> 0(), mark(isNat(X)) -> a__isNat(X), mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)), mark(x(X1, X2)) -> a__x(mark(X1), mark(X2)), mark(U11(X1, X2)) -> a__U11(mark(X1), X2), mark(U21(X1, X2, X3)) -> a__U21(mark(X1), X2, X3), mark(U31(X)) -> a__U31(mark(X)), mark(U41(X1, X2, X3)) -> a__U41(mark(X1), X2, X3), mark(and(X1, X2)) -> a__and(mark(X1), X2), a__U11(X1, X2) -> U11(X1, X2), a__U11(tt(), N) -> mark(N), a__plus(N, s(M)) -> a__U21(a__and(a__isNat(M), isNat(N)), M, N), a__plus(N, 0()) -> a__U11(a__isNat(N), N), a__plus(X1, X2) -> plus(X1, X2), a__U21(X1, X2, X3) -> U21(X1, X2, X3), a__U21(tt(), M, N) -> s(a__plus(mark(N), mark(M))), a__U31(X) -> U31(X), a__U31(tt()) -> 0(), a__x(N, s(M)) -> a__U41(a__and(a__isNat(M), isNat(N)), M, N), a__x(N, 0()) -> a__U31(a__isNat(N)), a__x(X1, X2) -> x(X1, X2), a__U41(X1, X2, X3) -> U41(X1, X2, X3), a__U41(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__isNat(X) -> isNat(X), a__isNat(s(V1)) -> a__isNat(V1), a__isNat(0()) -> tt(), a__isNat(plus(V1, V2)) -> a__and(a__isNat(V1), isNat(V2)), a__isNat(x(V1, V2)) -> a__and(a__isNat(V1), isNat(V2))} Fail