MAYBE Time: 0.033802 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: DP: { 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} 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)} EDG: { (mark# and(X1, X2) -> a__and#(mark X1, X2), a__and#(tt(), X) -> mark# X) (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# x(X1, X2) -> mark# X2, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# x(X1, X2) -> mark# X2, mark# and(X1, X2) -> 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# U41(X1, X2, X3) -> mark# X1) (mark# x(X1, X2) -> mark# X2, mark# U31 X -> a__U31# mark X) (mark# x(X1, X2) -> mark# X2, mark# U31 X -> mark# X) (mark# x(X1, X2) -> mark# X2, mark# U21(X1, X2, X3) -> a__U21#(mark X1, X2, X3)) (mark# x(X1, X2) -> mark# X2, mark# U21(X1, X2, X3) -> mark# X1) (mark# x(X1, X2) -> mark# X2, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (mark# x(X1, X2) -> mark# X2, mark# U11(X1, X2) -> mark# X1) (mark# x(X1, X2) -> mark# X2, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (mark# x(X1, X2) -> mark# X2, mark# x(X1, X2) -> mark# X2) (mark# x(X1, X2) -> mark# X2, mark# x(X1, X2) -> mark# X1) (mark# x(X1, X2) -> mark# X2, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# x(X1, X2) -> mark# X2, mark# plus(X1, X2) -> mark# X2) (mark# x(X1, X2) -> mark# X2, mark# plus(X1, X2) -> mark# X1) (mark# x(X1, X2) -> mark# X2, mark# isNat X -> a__isNat# X) (mark# x(X1, X2) -> mark# X2, mark# s X -> mark# X) (mark# isNat X -> a__isNat# X, a__isNat# x(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# plus(V1, V2) -> 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# s V1 -> a__isNat# V1) (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, 0()) -> a__U31# a__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, 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__U41#(a__and(a__isNat M, isNat N), M, N)) (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# plus(V1, V2) -> a__and#(a__isNat V1, isNat V2), a__and#(tt(), X) -> mark# X) (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) (mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3), a__U41#(tt(), M, N) -> a__x#(mark 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) -> mark# M) (mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3), a__U41#(tt(), M, N) -> mark# N) (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# U21(X1, X2, X3) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# U21(X1, X2, X3) -> mark# X1, mark# and(X1, X2) -> 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# U41(X1, X2, X3) -> mark# X1) (mark# U21(X1, X2, X3) -> mark# X1, mark# U31 X -> a__U31# mark X) (mark# U21(X1, X2, X3) -> mark# X1, mark# U31 X -> mark# X) (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# U21(X1, X2, X3) -> 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# U11(X1, X2) -> mark# X1) (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# x(X1, X2) -> mark# X2) (mark# U21(X1, X2, X3) -> mark# X1, mark# x(X1, X2) -> mark# X1) (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# plus(X1, X2) -> mark# X2) (mark# U21(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# U21(X1, X2, X3) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# U21(X1, X2, X3) -> mark# X1, mark# s X -> mark# X) (mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> 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# U41(X1, X2, X3) -> mark# X1) (mark# and(X1, X2) -> mark# X1, mark# U31 X -> a__U31# mark X) (mark# and(X1, X2) -> mark# X1, mark# U31 X -> mark# X) (mark# and(X1, X2) -> mark# X1, mark# U21(X1, X2, X3) -> a__U21#(mark X1, X2, X3)) (mark# and(X1, X2) -> mark# X1, mark# U21(X1, X2, X3) -> mark# X1) (mark# and(X1, X2) -> mark# X1, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (mark# and(X1, X2) -> mark# X1, mark# U11(X1, X2) -> mark# X1) (mark# and(X1, X2) -> mark# X1, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (mark# and(X1, X2) -> mark# X1, mark# x(X1, X2) -> mark# X2) (mark# and(X1, X2) -> mark# X1, mark# x(X1, X2) -> mark# X1) (mark# and(X1, X2) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# and(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# and(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# and(X1, X2) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# and(X1, X2) -> mark# X1, mark# s 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) (a__plus#(N, 0()) -> a__U11#(a__isNat N, N), a__U11#(tt(), N) -> mark# N) (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) (mark# U41(X1, X2, X3) -> mark# X1, mark# s X -> mark# X) (mark# U41(X1, X2, X3) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# U41(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# U41(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (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# x(X1, X2) -> mark# X1) (mark# U41(X1, X2, X3) -> mark# X1, mark# x(X1, X2) -> mark# X2) (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# U11(X1, X2) -> 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# U21(X1, X2, X3) -> mark# X1) (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# U31 X -> mark# X) (mark# U41(X1, X2, X3) -> mark# X1, mark# U31 X -> a__U31# mark X) (mark# U41(X1, X2, X3) -> mark# X1, mark# U41(X1, X2, X3) -> 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# and(X1, X2) -> mark# X1) (mark# U41(X1, X2, X3) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# U11(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# U11(X1, X2) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# U11(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# U11(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# U11(X1, X2) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# U11(X1, X2) -> mark# X1, mark# x(X1, X2) -> mark# X1) (mark# U11(X1, X2) -> mark# X1, mark# x(X1, X2) -> mark# X2) (mark# U11(X1, X2) -> mark# X1, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (mark# U11(X1, X2) -> mark# X1, mark# U11(X1, X2) -> mark# X1) (mark# U11(X1, X2) -> mark# X1, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (mark# U11(X1, X2) -> mark# X1, mark# U21(X1, X2, X3) -> mark# X1) (mark# U11(X1, X2) -> mark# X1, mark# U21(X1, X2, X3) -> a__U21#(mark X1, X2, X3)) (mark# U11(X1, X2) -> mark# X1, mark# U31 X -> mark# X) (mark# U11(X1, X2) -> mark# X1, mark# U31 X -> a__U31# mark X) (mark# U11(X1, X2) -> mark# X1, mark# U41(X1, X2, X3) -> 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# and(X1, X2) -> mark# X1) (mark# U11(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# plus(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# plus(X1, X2) -> mark# X1, mark# isNat X -> a__isNat# 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# U11(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (mark# plus(X1, X2) -> mark# X1, mark# U21(X1, X2, X3) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# U21(X1, X2, X3) -> a__U21#(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X1, mark# U31 X -> mark# X) (mark# plus(X1, X2) -> mark# X1, mark# U31 X -> a__U31# mark X) (mark# plus(X1, X2) -> mark# X1, mark# U41(X1, X2, X3) -> 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# and(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# U21(X1, X2, X3) -> a__U21#(mark X1, X2, X3), a__U21#(tt(), M, N) -> mark# N) (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) -> a__plus#(mark N, mark M)) (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) (a__isNat# x(V1, V2) -> a__and#(a__isNat V1, isNat V2), a__and#(tt(), X) -> mark# X) (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)) (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# U31 X -> mark# X, mark# s X -> mark# X) (mark# U31 X -> mark# X, mark# isNat X -> a__isNat# X) (mark# U31 X -> mark# X, mark# plus(X1, X2) -> mark# X1) (mark# U31 X -> mark# X, mark# plus(X1, X2) -> mark# X2) (mark# U31 X -> mark# X, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# U31 X -> mark# X, mark# x(X1, X2) -> mark# X1) (mark# U31 X -> mark# X, mark# x(X1, X2) -> mark# X2) (mark# U31 X -> mark# X, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (mark# U31 X -> mark# X, mark# U11(X1, X2) -> mark# X1) (mark# U31 X -> mark# X, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (mark# U31 X -> mark# X, mark# U21(X1, X2, X3) -> mark# X1) (mark# U31 X -> mark# X, mark# U21(X1, X2, X3) -> a__U21#(mark X1, X2, X3)) (mark# U31 X -> mark# X, mark# U31 X -> mark# X) (mark# U31 X -> mark# X, mark# U31 X -> a__U31# mark X) (mark# U31 X -> mark# X, mark# U41(X1, X2, X3) -> mark# X1) (mark# U31 X -> mark# X, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (mark# U31 X -> mark# X, mark# and(X1, X2) -> mark# X1) (mark# U31 X -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2)) (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) (mark# s X -> mark# X, mark# s X -> mark# X) (mark# s X -> mark# X, mark# isNat X -> a__isNat# X) (mark# s X -> mark# X, mark# plus(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# plus(X1, X2) -> mark# X2) (mark# s X -> mark# X, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# s X -> mark# X, mark# x(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# x(X1, X2) -> mark# X2) (mark# s X -> mark# X, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (mark# s X -> mark# X, mark# U11(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (mark# s X -> mark# X, mark# U21(X1, X2, X3) -> mark# X1) (mark# s X -> mark# X, mark# U21(X1, X2, X3) -> a__U21#(mark X1, X2, X3)) (mark# s X -> mark# X, mark# U31 X -> mark# X) (mark# s X -> mark# X, mark# U31 X -> a__U31# mark X) (mark# s X -> mark# X, mark# U41(X1, X2, X3) -> mark# X1) (mark# s X -> mark# X, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (mark# s X -> mark# X, mark# and(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# plus(X1, X2) -> mark# X2, mark# s X -> mark# X) (mark# plus(X1, X2) -> mark# X2, mark# isNat X -> a__isNat# X) (mark# plus(X1, X2) -> mark# X2, mark# plus(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X2, mark# plus(X1, X2) -> mark# X2) (mark# plus(X1, X2) -> mark# X2, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# plus(X1, X2) -> mark# X2, mark# x(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X2, mark# x(X1, X2) -> mark# X2) (mark# plus(X1, X2) -> mark# X2, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (mark# plus(X1, X2) -> mark# X2, mark# U11(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X2, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (mark# plus(X1, X2) -> mark# X2, mark# U21(X1, X2, X3) -> mark# X1) (mark# plus(X1, X2) -> mark# X2, mark# U21(X1, X2, X3) -> a__U21#(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X2, mark# U31 X -> mark# X) (mark# plus(X1, X2) -> mark# X2, mark# U31 X -> a__U31# mark X) (mark# plus(X1, X2) -> mark# X2, mark# U41(X1, X2, X3) -> 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# and(X1, X2) -> mark# X1) (mark# plus(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# U11(X1, X2) -> a__U11#(mark X1, X2), a__U11#(tt(), N) -> mark# N) } STATUS: arrows: 0.787982 SCCS (1): 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 (40): 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)} Open