MAYBE Time: 0.036239 TRS: { a__U12(X1, X2, X3) -> U12(X1, X2, X3), a__U12(tt(), M, N) -> s a__plus(mark N, mark M), a__U11(X1, X2, X3) -> U11(X1, X2, X3), a__U11(tt(), M, N) -> a__U12(tt(), M, N), a__plus(N, s M) -> a__U11(tt(), M, N), a__plus(N, 0()) -> mark N, a__plus(X1, X2) -> plus(X1, X2), mark tt() -> tt(), mark s X -> s mark X, mark 0() -> 0(), mark U11(X1, X2, X3) -> a__U11(mark X1, X2, X3), mark U12(X1, X2, X3) -> a__U12(mark X1, X2, X3), mark plus(X1, X2) -> a__plus(mark X1, mark X2), mark U21(X1, X2, X3) -> a__U21(mark X1, X2, X3), mark U22(X1, X2, X3) -> a__U22(mark X1, X2, X3), mark x(X1, X2) -> a__x(mark X1, mark X2), a__U22(X1, X2, X3) -> U22(X1, X2, X3), a__U22(tt(), M, N) -> a__plus(a__x(mark N, mark M), mark N), a__U21(X1, X2, X3) -> U21(X1, X2, X3), a__U21(tt(), M, N) -> a__U22(tt(), M, N), a__x(N, s M) -> a__U21(tt(), M, N), a__x(N, 0()) -> 0(), a__x(X1, X2) -> x(X1, X2)} DP: DP: { a__U12#(tt(), M, N) -> a__plus#(mark N, mark M), a__U12#(tt(), M, N) -> mark# M, a__U12#(tt(), M, N) -> mark# N, a__U11#(tt(), M, N) -> a__U12#(tt(), M, N), a__plus#(N, s M) -> a__U11#(tt(), M, N), a__plus#(N, 0()) -> mark# N, mark# s X -> mark# X, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3), mark# U11(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3), mark# U12(X1, X2, X3) -> 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# U21(X1, X2, X3) -> mark# X1, mark# U21(X1, X2, X3) -> a__U21#(mark X1, X2, X3), mark# U22(X1, X2, X3) -> mark# X1, mark# U22(X1, X2, X3) -> a__U22#(mark X1, X2, X3), mark# x(X1, X2) -> mark# X1, mark# x(X1, X2) -> mark# X2, mark# x(X1, X2) -> a__x#(mark X1, mark X2), a__U22#(tt(), M, N) -> a__plus#(a__x(mark N, mark M), mark N), a__U22#(tt(), M, N) -> mark# M, a__U22#(tt(), M, N) -> mark# N, a__U22#(tt(), M, N) -> a__x#(mark N, mark M), a__U21#(tt(), M, N) -> a__U22#(tt(), M, N), a__x#(N, s M) -> a__U21#(tt(), M, N)} TRS: { a__U12(X1, X2, X3) -> U12(X1, X2, X3), a__U12(tt(), M, N) -> s a__plus(mark N, mark M), a__U11(X1, X2, X3) -> U11(X1, X2, X3), a__U11(tt(), M, N) -> a__U12(tt(), M, N), a__plus(N, s M) -> a__U11(tt(), M, N), a__plus(N, 0()) -> mark N, a__plus(X1, X2) -> plus(X1, X2), mark tt() -> tt(), mark s X -> s mark X, mark 0() -> 0(), mark U11(X1, X2, X3) -> a__U11(mark X1, X2, X3), mark U12(X1, X2, X3) -> a__U12(mark X1, X2, X3), mark plus(X1, X2) -> a__plus(mark X1, mark X2), mark U21(X1, X2, X3) -> a__U21(mark X1, X2, X3), mark U22(X1, X2, X3) -> a__U22(mark X1, X2, X3), mark x(X1, X2) -> a__x(mark X1, mark X2), a__U22(X1, X2, X3) -> U22(X1, X2, X3), a__U22(tt(), M, N) -> a__plus(a__x(mark N, mark M), mark N), a__U21(X1, X2, X3) -> U21(X1, X2, X3), a__U21(tt(), M, N) -> a__U22(tt(), M, N), a__x(N, s M) -> a__U21(tt(), M, N), a__x(N, 0()) -> 0(), a__x(X1, X2) -> x(X1, X2)} EDG: { (mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3), a__U11#(tt(), M, N) -> a__U12#(tt(), M, N)) (mark# U21(X1, X2, X3) -> a__U21#(mark X1, X2, X3), a__U21#(tt(), M, N) -> a__U22#(tt(), M, N)) (a__U11#(tt(), M, N) -> a__U12#(tt(), M, N), a__U12#(tt(), M, N) -> mark# N) (a__U11#(tt(), M, N) -> a__U12#(tt(), M, N), a__U12#(tt(), M, N) -> mark# M) (a__U11#(tt(), M, N) -> a__U12#(tt(), M, N), a__U12#(tt(), M, N) -> a__plus#(mark N, mark M)) (a__U21#(tt(), M, N) -> a__U22#(tt(), M, N), a__U22#(tt(), M, N) -> a__x#(mark N, mark M)) (a__U21#(tt(), M, N) -> a__U22#(tt(), M, N), a__U22#(tt(), M, N) -> mark# N) (a__U21#(tt(), M, N) -> a__U22#(tt(), M, N), a__U22#(tt(), M, N) -> mark# M) (a__U21#(tt(), M, N) -> a__U22#(tt(), M, N), a__U22#(tt(), M, N) -> a__plus#(a__x(mark N, mark M), mark N)) (a__U12#(tt(), M, N) -> a__plus#(mark N, mark M), a__plus#(N, 0()) -> mark# N) (a__U12#(tt(), M, N) -> a__plus#(mark N, mark M), a__plus#(N, s M) -> a__U11#(tt(), M, N)) (mark# x(X1, X2) -> a__x#(mark X1, mark X2), a__x#(N, s M) -> a__U21#(tt(), M, N)) (a__U22#(tt(), M, N) -> a__x#(mark N, mark M), a__x#(N, s M) -> a__U21#(tt(), M, N)) (a__U22#(tt(), M, N) -> mark# M, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (a__U22#(tt(), M, N) -> mark# M, mark# x(X1, X2) -> mark# X2) (a__U22#(tt(), M, N) -> mark# M, mark# x(X1, X2) -> mark# X1) (a__U22#(tt(), M, N) -> mark# M, mark# U22(X1, X2, X3) -> a__U22#(mark X1, X2, X3)) (a__U22#(tt(), M, N) -> mark# M, mark# U22(X1, X2, X3) -> mark# X1) (a__U22#(tt(), M, N) -> mark# M, mark# U21(X1, X2, X3) -> a__U21#(mark X1, X2, X3)) (a__U22#(tt(), M, N) -> mark# M, mark# U21(X1, X2, X3) -> mark# X1) (a__U22#(tt(), M, N) -> mark# M, mark# plus(X1, X2) -> mark# X2) (a__U22#(tt(), M, N) -> mark# M, mark# plus(X1, X2) -> mark# X1) (a__U22#(tt(), M, N) -> mark# M, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (a__U22#(tt(), M, N) -> mark# M, mark# U12(X1, X2, X3) -> mark# X1) (a__U22#(tt(), M, N) -> mark# M, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3)) (a__U22#(tt(), M, N) -> mark# M, mark# U11(X1, X2, X3) -> mark# X1) (a__U22#(tt(), M, N) -> mark# M, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (a__U22#(tt(), M, N) -> mark# M, mark# s X -> mark# X) (mark# U12(X1, X2, X3) -> mark# X1, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (mark# U12(X1, X2, X3) -> mark# X1, mark# x(X1, X2) -> mark# X2) (mark# U12(X1, X2, X3) -> mark# X1, mark# x(X1, X2) -> mark# X1) (mark# U12(X1, X2, X3) -> mark# X1, mark# U22(X1, X2, X3) -> a__U22#(mark X1, X2, X3)) (mark# U12(X1, X2, X3) -> mark# X1, mark# U22(X1, X2, X3) -> mark# X1) (mark# U12(X1, X2, X3) -> mark# X1, mark# U21(X1, X2, X3) -> a__U21#(mark X1, X2, X3)) (mark# U12(X1, X2, X3) -> mark# X1, mark# U21(X1, X2, X3) -> mark# X1) (mark# U12(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# U12(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# U12(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# U12(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> mark# X1) (mark# U12(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3)) (mark# U12(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> mark# X1) (mark# U12(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (mark# U12(X1, X2, X3) -> mark# X1, mark# s X -> mark# X) (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# U22(X1, X2, X3) -> a__U22#(mark X1, X2, X3)) (mark# U21(X1, X2, X3) -> mark# X1, mark# U22(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# U21(X1, X2, X3) -> 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) -> 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# U12(X1, X2, X3) -> mark# X1) (mark# U21(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3)) (mark# U21(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> mark# X1) (mark# U21(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (mark# U21(X1, X2, X3) -> mark# X1, mark# s X -> mark# X) (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# U22(X1, X2, X3) -> a__U22#(mark X1, X2, X3)) (mark# x(X1, X2) -> mark# X1, mark# U22(X1, X2, X3) -> mark# X1) (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# plus(X1, X2) -> mark# X2) (mark# x(X1, X2) -> mark# X1, mark# plus(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# U12(X1, X2, X3) -> mark# X1) (mark# x(X1, X2) -> mark# X1, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3)) (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# s X -> mark# X) (a__plus#(N, 0()) -> mark# N, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (a__plus#(N, 0()) -> mark# N, mark# x(X1, X2) -> mark# X2) (a__plus#(N, 0()) -> mark# N, mark# x(X1, X2) -> mark# X1) (a__plus#(N, 0()) -> mark# N, mark# U22(X1, X2, X3) -> a__U22#(mark X1, X2, X3)) (a__plus#(N, 0()) -> mark# N, mark# U22(X1, X2, X3) -> mark# X1) (a__plus#(N, 0()) -> mark# N, mark# U21(X1, X2, X3) -> a__U21#(mark X1, X2, X3)) (a__plus#(N, 0()) -> mark# N, mark# U21(X1, X2, X3) -> mark# X1) (a__plus#(N, 0()) -> mark# N, mark# plus(X1, X2) -> mark# X2) (a__plus#(N, 0()) -> mark# N, mark# plus(X1, X2) -> mark# X1) (a__plus#(N, 0()) -> mark# N, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (a__plus#(N, 0()) -> mark# N, mark# U12(X1, X2, X3) -> mark# X1) (a__plus#(N, 0()) -> mark# N, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3)) (a__plus#(N, 0()) -> mark# N, mark# U11(X1, X2, X3) -> mark# X1) (a__plus#(N, 0()) -> mark# N, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (a__plus#(N, 0()) -> mark# N, mark# s X -> mark# X) (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# U22(X1, X2, X3) -> a__U22#(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X2, mark# U22(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# U21(X1, X2, X3) -> mark# X1) (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# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# plus(X1, X2) -> mark# X2, mark# U12(X1, X2, X3) -> mark# X1) (mark# plus(X1, X2) -> mark# X2, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3)) (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# s X -> mark# X) (mark# x(X1, X2) -> mark# X2, mark# s X -> mark# 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, X3) -> a__U12#(mark X1, X2, X3)) (mark# x(X1, X2) -> mark# X2, mark# U12(X1, X2, X3) -> 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# X1) (mark# x(X1, X2) -> mark# X2, mark# plus(X1, X2) -> mark# 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# U22(X1, X2, X3) -> mark# X1) (mark# x(X1, X2) -> mark# X2, mark# U22(X1, X2, X3) -> a__U22#(mark X1, X2, X3)) (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)) (a__U22#(tt(), M, N) -> mark# N, mark# s X -> mark# X) (a__U22#(tt(), M, N) -> mark# N, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (a__U22#(tt(), M, N) -> mark# N, mark# U11(X1, X2, X3) -> mark# X1) (a__U22#(tt(), M, N) -> mark# N, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3)) (a__U22#(tt(), M, N) -> mark# N, mark# U12(X1, X2, X3) -> mark# X1) (a__U22#(tt(), M, N) -> mark# N, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (a__U22#(tt(), M, N) -> mark# N, mark# plus(X1, X2) -> mark# X1) (a__U22#(tt(), M, N) -> mark# N, mark# plus(X1, X2) -> mark# X2) (a__U22#(tt(), M, N) -> mark# N, mark# U21(X1, X2, X3) -> mark# X1) (a__U22#(tt(), M, N) -> mark# N, mark# U21(X1, X2, X3) -> a__U21#(mark X1, X2, X3)) (a__U22#(tt(), M, N) -> mark# N, mark# U22(X1, X2, X3) -> mark# X1) (a__U22#(tt(), M, N) -> mark# N, mark# U22(X1, X2, X3) -> a__U22#(mark X1, X2, X3)) (a__U22#(tt(), M, N) -> mark# N, mark# x(X1, X2) -> mark# X1) (a__U22#(tt(), M, N) -> mark# N, mark# x(X1, X2) -> mark# X2) (a__U22#(tt(), M, N) -> mark# N, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (a__U12#(tt(), M, N) -> mark# N, mark# s X -> mark# X) (a__U12#(tt(), M, N) -> mark# N, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (a__U12#(tt(), M, N) -> mark# N, mark# U11(X1, X2, X3) -> mark# X1) (a__U12#(tt(), M, N) -> mark# N, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3)) (a__U12#(tt(), M, N) -> mark# N, mark# U12(X1, X2, X3) -> mark# X1) (a__U12#(tt(), M, N) -> mark# N, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (a__U12#(tt(), M, N) -> mark# N, mark# plus(X1, X2) -> mark# X1) (a__U12#(tt(), M, N) -> mark# N, mark# plus(X1, X2) -> mark# X2) (a__U12#(tt(), M, N) -> mark# N, mark# U21(X1, X2, X3) -> mark# X1) (a__U12#(tt(), M, N) -> mark# N, mark# U21(X1, X2, X3) -> a__U21#(mark X1, X2, X3)) (a__U12#(tt(), M, N) -> mark# N, mark# U22(X1, X2, X3) -> mark# X1) (a__U12#(tt(), M, N) -> mark# N, mark# U22(X1, X2, X3) -> a__U22#(mark X1, X2, X3)) (a__U12#(tt(), M, N) -> mark# N, mark# x(X1, X2) -> mark# X1) (a__U12#(tt(), M, N) -> mark# N, mark# x(X1, X2) -> mark# X2) (a__U12#(tt(), M, N) -> mark# N, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (mark# U22(X1, X2, X3) -> mark# X1, mark# s X -> mark# X) (mark# U22(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (mark# U22(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> mark# X1) (mark# U22(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3)) (mark# U22(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> mark# X1) (mark# U22(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# U22(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# U22(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# U22(X1, X2, X3) -> mark# X1, mark# U21(X1, X2, X3) -> mark# X1) (mark# U22(X1, X2, X3) -> mark# X1, mark# U21(X1, X2, X3) -> a__U21#(mark X1, X2, X3)) (mark# U22(X1, X2, X3) -> mark# X1, mark# U22(X1, X2, X3) -> mark# X1) (mark# U22(X1, X2, X3) -> mark# X1, mark# U22(X1, X2, X3) -> a__U22#(mark X1, X2, X3)) (mark# U22(X1, X2, X3) -> mark# X1, mark# x(X1, X2) -> mark# X1) (mark# U22(X1, X2, X3) -> mark# X1, mark# x(X1, X2) -> mark# X2) (mark# U22(X1, X2, X3) -> mark# X1, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (mark# plus(X1, X2) -> mark# X1, mark# s X -> mark# 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, X3) -> a__U12#(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X1, mark# U12(X1, X2, X3) -> 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# X1) (mark# plus(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# 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# U22(X1, X2, X3) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# U22(X1, X2, X3) -> a__U22#(mark X1, X2, X3)) (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# U11(X1, X2, X3) -> mark# X1, mark# s X -> mark# X) (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# U11(X1, X2, X3) -> mark# X1) (mark# U11(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3)) (mark# U11(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> 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# X1) (mark# U11(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# U11(X1, X2, X3) -> mark# X1, mark# U21(X1, X2, X3) -> mark# X1) (mark# U11(X1, X2, X3) -> mark# X1, mark# U21(X1, X2, X3) -> a__U21#(mark X1, X2, X3)) (mark# U11(X1, X2, X3) -> mark# X1, mark# U22(X1, X2, X3) -> mark# X1) (mark# U11(X1, X2, X3) -> mark# X1, mark# U22(X1, X2, X3) -> a__U22#(mark X1, X2, X3)) (mark# U11(X1, X2, X3) -> mark# X1, mark# x(X1, X2) -> mark# X1) (mark# U11(X1, X2, X3) -> mark# X1, mark# x(X1, X2) -> mark# X2) (mark# U11(X1, X2, X3) -> mark# X1, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (a__U12#(tt(), M, N) -> mark# M, mark# s X -> mark# X) (a__U12#(tt(), M, N) -> mark# M, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (a__U12#(tt(), M, N) -> mark# M, mark# U11(X1, X2, X3) -> mark# X1) (a__U12#(tt(), M, N) -> mark# M, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3)) (a__U12#(tt(), M, N) -> mark# M, mark# U12(X1, X2, X3) -> mark# X1) (a__U12#(tt(), M, N) -> mark# M, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (a__U12#(tt(), M, N) -> mark# M, mark# plus(X1, X2) -> mark# X1) (a__U12#(tt(), M, N) -> mark# M, mark# plus(X1, X2) -> mark# X2) (a__U12#(tt(), M, N) -> mark# M, mark# U21(X1, X2, X3) -> mark# X1) (a__U12#(tt(), M, N) -> mark# M, mark# U21(X1, X2, X3) -> a__U21#(mark X1, X2, X3)) (a__U12#(tt(), M, N) -> mark# M, mark# U22(X1, X2, X3) -> mark# X1) (a__U12#(tt(), M, N) -> mark# M, mark# U22(X1, X2, X3) -> a__U22#(mark X1, X2, X3)) (a__U12#(tt(), M, N) -> mark# M, mark# x(X1, X2) -> mark# X1) (a__U12#(tt(), M, N) -> mark# M, mark# x(X1, X2) -> mark# X2) (a__U12#(tt(), M, N) -> mark# M, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (a__U22#(tt(), M, N) -> a__plus#(a__x(mark N, mark M), mark N), a__plus#(N, s M) -> a__U11#(tt(), M, N)) (a__U22#(tt(), M, N) -> a__plus#(a__x(mark N, mark M), mark N), a__plus#(N, 0()) -> mark# N) (mark# plus(X1, X2) -> a__plus#(mark X1, mark X2), a__plus#(N, s M) -> a__U11#(tt(), M, N)) (mark# plus(X1, X2) -> a__plus#(mark X1, mark X2), a__plus#(N, 0()) -> mark# N) (a__x#(N, s M) -> a__U21#(tt(), M, N), a__U21#(tt(), M, N) -> a__U22#(tt(), M, N)) (a__plus#(N, s M) -> a__U11#(tt(), M, N), a__U11#(tt(), M, N) -> a__U12#(tt(), M, N)) (mark# U22(X1, X2, X3) -> a__U22#(mark X1, X2, X3), a__U22#(tt(), M, N) -> a__plus#(a__x(mark N, mark M), mark N)) (mark# U22(X1, X2, X3) -> a__U22#(mark X1, X2, X3), a__U22#(tt(), M, N) -> mark# M) (mark# U22(X1, X2, X3) -> a__U22#(mark X1, X2, X3), a__U22#(tt(), M, N) -> mark# N) (mark# U22(X1, X2, X3) -> a__U22#(mark X1, X2, X3), a__U22#(tt(), M, N) -> a__x#(mark N, mark M)) (mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3), a__U12#(tt(), M, N) -> a__plus#(mark N, mark M)) (mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3), a__U12#(tt(), M, N) -> mark# M) (mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3), a__U12#(tt(), M, N) -> mark# N) (mark# s X -> mark# X, mark# s X -> mark# X) (mark# s X -> mark# X, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (mark# s X -> mark# X, mark# U11(X1, X2, X3) -> mark# X1) (mark# s X -> mark# X, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3)) (mark# s X -> mark# X, mark# U12(X1, X2, X3) -> 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# X1) (mark# s X -> mark# X, mark# plus(X1, X2) -> mark# 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# U22(X1, X2, X3) -> mark# X1) (mark# s X -> mark# X, mark# U22(X1, X2, X3) -> a__U22#(mark X1, X2, X3)) (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)) } EDG: { (mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3), a__U11#(tt(), M, N) -> a__U12#(tt(), M, N)) (mark# U21(X1, X2, X3) -> a__U21#(mark X1, X2, X3), a__U21#(tt(), M, N) -> a__U22#(tt(), M, N)) (a__U11#(tt(), M, N) -> a__U12#(tt(), M, N), a__U12#(tt(), M, N) -> mark# N) (a__U11#(tt(), M, N) -> a__U12#(tt(), M, N), a__U12#(tt(), M, N) -> mark# M) (a__U11#(tt(), M, N) -> a__U12#(tt(), M, N), a__U12#(tt(), M, N) -> a__plus#(mark N, mark M)) (a__U21#(tt(), M, N) -> a__U22#(tt(), M, N), a__U22#(tt(), M, N) -> a__x#(mark N, mark M)) (a__U21#(tt(), M, N) -> a__U22#(tt(), M, N), a__U22#(tt(), M, N) -> mark# N) (a__U21#(tt(), M, N) -> a__U22#(tt(), M, N), a__U22#(tt(), M, N) -> mark# M) (a__U21#(tt(), M, N) -> a__U22#(tt(), M, N), a__U22#(tt(), M, N) -> a__plus#(a__x(mark N, mark M), mark N)) (a__U12#(tt(), M, N) -> a__plus#(mark N, mark M), a__plus#(N, 0()) -> mark# N) (a__U12#(tt(), M, N) -> a__plus#(mark N, mark M), a__plus#(N, s M) -> a__U11#(tt(), M, N)) (mark# x(X1, X2) -> a__x#(mark X1, mark X2), a__x#(N, s M) -> a__U21#(tt(), M, N)) (a__U22#(tt(), M, N) -> a__x#(mark N, mark M), a__x#(N, s M) -> a__U21#(tt(), M, N)) (a__U22#(tt(), M, N) -> mark# M, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (a__U22#(tt(), M, N) -> mark# M, mark# x(X1, X2) -> mark# X2) (a__U22#(tt(), M, N) -> mark# M, mark# x(X1, X2) -> mark# X1) (a__U22#(tt(), M, N) -> mark# M, mark# U22(X1, X2, X3) -> a__U22#(mark X1, X2, X3)) (a__U22#(tt(), M, N) -> mark# M, mark# U22(X1, X2, X3) -> mark# X1) (a__U22#(tt(), M, N) -> mark# M, mark# U21(X1, X2, X3) -> a__U21#(mark X1, X2, X3)) (a__U22#(tt(), M, N) -> mark# M, mark# U21(X1, X2, X3) -> mark# X1) (a__U22#(tt(), M, N) -> mark# M, mark# plus(X1, X2) -> mark# X2) (a__U22#(tt(), M, N) -> mark# M, mark# plus(X1, X2) -> mark# X1) (a__U22#(tt(), M, N) -> mark# M, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (a__U22#(tt(), M, N) -> mark# M, mark# U12(X1, X2, X3) -> mark# X1) (a__U22#(tt(), M, N) -> mark# M, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3)) (a__U22#(tt(), M, N) -> mark# M, mark# U11(X1, X2, X3) -> mark# X1) (a__U22#(tt(), M, N) -> mark# M, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (a__U22#(tt(), M, N) -> mark# M, mark# s X -> mark# X) (mark# U12(X1, X2, X3) -> mark# X1, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (mark# U12(X1, X2, X3) -> mark# X1, mark# x(X1, X2) -> mark# X2) (mark# U12(X1, X2, X3) -> mark# X1, mark# x(X1, X2) -> mark# X1) (mark# U12(X1, X2, X3) -> mark# X1, mark# U22(X1, X2, X3) -> a__U22#(mark X1, X2, X3)) (mark# U12(X1, X2, X3) -> mark# X1, mark# U22(X1, X2, X3) -> mark# X1) (mark# U12(X1, X2, X3) -> mark# X1, mark# U21(X1, X2, X3) -> a__U21#(mark X1, X2, X3)) (mark# U12(X1, X2, X3) -> mark# X1, mark# U21(X1, X2, X3) -> mark# X1) (mark# U12(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# U12(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# U12(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# U12(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> mark# X1) (mark# U12(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3)) (mark# U12(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> mark# X1) (mark# U12(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (mark# U12(X1, X2, X3) -> mark# X1, mark# s X -> mark# X) (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# U22(X1, X2, X3) -> a__U22#(mark X1, X2, X3)) (mark# U21(X1, X2, X3) -> mark# X1, mark# U22(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# U21(X1, X2, X3) -> 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) -> 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# U12(X1, X2, X3) -> mark# X1) (mark# U21(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3)) (mark# U21(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> mark# X1) (mark# U21(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (mark# U21(X1, X2, X3) -> mark# X1, mark# s X -> mark# X) (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# U22(X1, X2, X3) -> a__U22#(mark X1, X2, X3)) (mark# x(X1, X2) -> mark# X1, mark# U22(X1, X2, X3) -> mark# X1) (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# plus(X1, X2) -> mark# X2) (mark# x(X1, X2) -> mark# X1, mark# plus(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# U12(X1, X2, X3) -> mark# X1) (mark# x(X1, X2) -> mark# X1, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3)) (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# s X -> mark# X) (a__plus#(N, 0()) -> mark# N, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (a__plus#(N, 0()) -> mark# N, mark# x(X1, X2) -> mark# X2) (a__plus#(N, 0()) -> mark# N, mark# x(X1, X2) -> mark# X1) (a__plus#(N, 0()) -> mark# N, mark# U22(X1, X2, X3) -> a__U22#(mark X1, X2, X3)) (a__plus#(N, 0()) -> mark# N, mark# U22(X1, X2, X3) -> mark# X1) (a__plus#(N, 0()) -> mark# N, mark# U21(X1, X2, X3) -> a__U21#(mark X1, X2, X3)) (a__plus#(N, 0()) -> mark# N, mark# U21(X1, X2, X3) -> mark# X1) (a__plus#(N, 0()) -> mark# N, mark# plus(X1, X2) -> mark# X2) (a__plus#(N, 0()) -> mark# N, mark# plus(X1, X2) -> mark# X1) (a__plus#(N, 0()) -> mark# N, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (a__plus#(N, 0()) -> mark# N, mark# U12(X1, X2, X3) -> mark# X1) (a__plus#(N, 0()) -> mark# N, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3)) (a__plus#(N, 0()) -> mark# N, mark# U11(X1, X2, X3) -> mark# X1) (a__plus#(N, 0()) -> mark# N, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (a__plus#(N, 0()) -> mark# N, mark# s X -> mark# X) (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# U22(X1, X2, X3) -> a__U22#(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X2, mark# U22(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# U21(X1, X2, X3) -> mark# X1) (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# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# plus(X1, X2) -> mark# X2, mark# U12(X1, X2, X3) -> mark# X1) (mark# plus(X1, X2) -> mark# X2, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3)) (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# s X -> mark# X) (mark# x(X1, X2) -> mark# X2, mark# s X -> mark# 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, X3) -> a__U12#(mark X1, X2, X3)) (mark# x(X1, X2) -> mark# X2, mark# U12(X1, X2, X3) -> 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# X1) (mark# x(X1, X2) -> mark# X2, mark# plus(X1, X2) -> mark# 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# U22(X1, X2, X3) -> mark# X1) (mark# x(X1, X2) -> mark# X2, mark# U22(X1, X2, X3) -> a__U22#(mark X1, X2, X3)) (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)) (a__U22#(tt(), M, N) -> mark# N, mark# s X -> mark# X) (a__U22#(tt(), M, N) -> mark# N, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (a__U22#(tt(), M, N) -> mark# N, mark# U11(X1, X2, X3) -> mark# X1) (a__U22#(tt(), M, N) -> mark# N, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3)) (a__U22#(tt(), M, N) -> mark# N, mark# U12(X1, X2, X3) -> mark# X1) (a__U22#(tt(), M, N) -> mark# N, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (a__U22#(tt(), M, N) -> mark# N, mark# plus(X1, X2) -> mark# X1) (a__U22#(tt(), M, N) -> mark# N, mark# plus(X1, X2) -> mark# X2) (a__U22#(tt(), M, N) -> mark# N, mark# U21(X1, X2, X3) -> mark# X1) (a__U22#(tt(), M, N) -> mark# N, mark# U21(X1, X2, X3) -> a__U21#(mark X1, X2, X3)) (a__U22#(tt(), M, N) -> mark# N, mark# U22(X1, X2, X3) -> mark# X1) (a__U22#(tt(), M, N) -> mark# N, mark# U22(X1, X2, X3) -> a__U22#(mark X1, X2, X3)) (a__U22#(tt(), M, N) -> mark# N, mark# x(X1, X2) -> mark# X1) (a__U22#(tt(), M, N) -> mark# N, mark# x(X1, X2) -> mark# X2) (a__U22#(tt(), M, N) -> mark# N, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (a__U12#(tt(), M, N) -> mark# N, mark# s X -> mark# X) (a__U12#(tt(), M, N) -> mark# N, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (a__U12#(tt(), M, N) -> mark# N, mark# U11(X1, X2, X3) -> mark# X1) (a__U12#(tt(), M, N) -> mark# N, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3)) (a__U12#(tt(), M, N) -> mark# N, mark# U12(X1, X2, X3) -> mark# X1) (a__U12#(tt(), M, N) -> mark# N, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (a__U12#(tt(), M, N) -> mark# N, mark# plus(X1, X2) -> mark# X1) (a__U12#(tt(), M, N) -> mark# N, mark# plus(X1, X2) -> mark# X2) (a__U12#(tt(), M, N) -> mark# N, mark# U21(X1, X2, X3) -> mark# X1) (a__U12#(tt(), M, N) -> mark# N, mark# U21(X1, X2, X3) -> a__U21#(mark X1, X2, X3)) (a__U12#(tt(), M, N) -> mark# N, mark# U22(X1, X2, X3) -> mark# X1) (a__U12#(tt(), M, N) -> mark# N, mark# U22(X1, X2, X3) -> a__U22#(mark X1, X2, X3)) (a__U12#(tt(), M, N) -> mark# N, mark# x(X1, X2) -> mark# X1) (a__U12#(tt(), M, N) -> mark# N, mark# x(X1, X2) -> mark# X2) (a__U12#(tt(), M, N) -> mark# N, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (mark# U22(X1, X2, X3) -> mark# X1, mark# s X -> mark# X) (mark# U22(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (mark# U22(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> mark# X1) (mark# U22(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3)) (mark# U22(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> mark# X1) (mark# U22(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# U22(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# U22(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# U22(X1, X2, X3) -> mark# X1, mark# U21(X1, X2, X3) -> mark# X1) (mark# U22(X1, X2, X3) -> mark# X1, mark# U21(X1, X2, X3) -> a__U21#(mark X1, X2, X3)) (mark# U22(X1, X2, X3) -> mark# X1, mark# U22(X1, X2, X3) -> mark# X1) (mark# U22(X1, X2, X3) -> mark# X1, mark# U22(X1, X2, X3) -> a__U22#(mark X1, X2, X3)) (mark# U22(X1, X2, X3) -> mark# X1, mark# x(X1, X2) -> mark# X1) (mark# U22(X1, X2, X3) -> mark# X1, mark# x(X1, X2) -> mark# X2) (mark# U22(X1, X2, X3) -> mark# X1, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (mark# plus(X1, X2) -> mark# X1, mark# s X -> mark# 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, X3) -> a__U12#(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X1, mark# U12(X1, X2, X3) -> 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# X1) (mark# plus(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# 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# U22(X1, X2, X3) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# U22(X1, X2, X3) -> a__U22#(mark X1, X2, X3)) (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# U11(X1, X2, X3) -> mark# X1, mark# s X -> mark# X) (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# U11(X1, X2, X3) -> mark# X1) (mark# U11(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3)) (mark# U11(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> 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# X1) (mark# U11(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# U11(X1, X2, X3) -> mark# X1, mark# U21(X1, X2, X3) -> mark# X1) (mark# U11(X1, X2, X3) -> mark# X1, mark# U21(X1, X2, X3) -> a__U21#(mark X1, X2, X3)) (mark# U11(X1, X2, X3) -> mark# X1, mark# U22(X1, X2, X3) -> mark# X1) (mark# U11(X1, X2, X3) -> mark# X1, mark# U22(X1, X2, X3) -> a__U22#(mark X1, X2, X3)) (mark# U11(X1, X2, X3) -> mark# X1, mark# x(X1, X2) -> mark# X1) (mark# U11(X1, X2, X3) -> mark# X1, mark# x(X1, X2) -> mark# X2) (mark# U11(X1, X2, X3) -> mark# X1, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (a__U12#(tt(), M, N) -> mark# M, mark# s X -> mark# X) (a__U12#(tt(), M, N) -> mark# M, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (a__U12#(tt(), M, N) -> mark# M, mark# U11(X1, X2, X3) -> mark# X1) (a__U12#(tt(), M, N) -> mark# M, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3)) (a__U12#(tt(), M, N) -> mark# M, mark# U12(X1, X2, X3) -> mark# X1) (a__U12#(tt(), M, N) -> mark# M, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (a__U12#(tt(), M, N) -> mark# M, mark# plus(X1, X2) -> mark# X1) (a__U12#(tt(), M, N) -> mark# M, mark# plus(X1, X2) -> mark# X2) (a__U12#(tt(), M, N) -> mark# M, mark# U21(X1, X2, X3) -> mark# X1) (a__U12#(tt(), M, N) -> mark# M, mark# U21(X1, X2, X3) -> a__U21#(mark X1, X2, X3)) (a__U12#(tt(), M, N) -> mark# M, mark# U22(X1, X2, X3) -> mark# X1) (a__U12#(tt(), M, N) -> mark# M, mark# U22(X1, X2, X3) -> a__U22#(mark X1, X2, X3)) (a__U12#(tt(), M, N) -> mark# M, mark# x(X1, X2) -> mark# X1) (a__U12#(tt(), M, N) -> mark# M, mark# x(X1, X2) -> mark# X2) (a__U12#(tt(), M, N) -> mark# M, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (a__U22#(tt(), M, N) -> a__plus#(a__x(mark N, mark M), mark N), a__plus#(N, s M) -> a__U11#(tt(), M, N)) (a__U22#(tt(), M, N) -> a__plus#(a__x(mark N, mark M), mark N), a__plus#(N, 0()) -> mark# N) (mark# plus(X1, X2) -> a__plus#(mark X1, mark X2), a__plus#(N, s M) -> a__U11#(tt(), M, N)) (mark# plus(X1, X2) -> a__plus#(mark X1, mark X2), a__plus#(N, 0()) -> mark# N) (a__x#(N, s M) -> a__U21#(tt(), M, N), a__U21#(tt(), M, N) -> a__U22#(tt(), M, N)) (a__plus#(N, s M) -> a__U11#(tt(), M, N), a__U11#(tt(), M, N) -> a__U12#(tt(), M, N)) (mark# U22(X1, X2, X3) -> a__U22#(mark X1, X2, X3), a__U22#(tt(), M, N) -> a__plus#(a__x(mark N, mark M), mark N)) (mark# U22(X1, X2, X3) -> a__U22#(mark X1, X2, X3), a__U22#(tt(), M, N) -> mark# M) (mark# U22(X1, X2, X3) -> a__U22#(mark X1, X2, X3), a__U22#(tt(), M, N) -> mark# N) (mark# U22(X1, X2, X3) -> a__U22#(mark X1, X2, X3), a__U22#(tt(), M, N) -> a__x#(mark N, mark M)) (mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3), a__U12#(tt(), M, N) -> a__plus#(mark N, mark M)) (mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3), a__U12#(tt(), M, N) -> mark# M) (mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3), a__U12#(tt(), M, N) -> mark# N) (mark# s X -> mark# X, mark# s X -> mark# X) (mark# s X -> mark# X, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (mark# s X -> mark# X, mark# U11(X1, X2, X3) -> mark# X1) (mark# s X -> mark# X, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3)) (mark# s X -> mark# X, mark# U12(X1, X2, X3) -> 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# X1) (mark# s X -> mark# X, mark# plus(X1, X2) -> mark# 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# U22(X1, X2, X3) -> mark# X1) (mark# s X -> mark# X, mark# U22(X1, X2, X3) -> a__U22#(mark X1, X2, X3)) (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)) } EDG: { (mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3), a__U11#(tt(), M, N) -> a__U12#(tt(), M, N)) (mark# U21(X1, X2, X3) -> a__U21#(mark X1, X2, X3), a__U21#(tt(), M, N) -> a__U22#(tt(), M, N)) (a__U11#(tt(), M, N) -> a__U12#(tt(), M, N), a__U12#(tt(), M, N) -> mark# N) (a__U11#(tt(), M, N) -> a__U12#(tt(), M, N), a__U12#(tt(), M, N) -> mark# M) (a__U11#(tt(), M, N) -> a__U12#(tt(), M, N), a__U12#(tt(), M, N) -> a__plus#(mark N, mark M)) (a__U21#(tt(), M, N) -> a__U22#(tt(), M, N), a__U22#(tt(), M, N) -> a__x#(mark N, mark M)) (a__U21#(tt(), M, N) -> a__U22#(tt(), M, N), a__U22#(tt(), M, N) -> mark# N) (a__U21#(tt(), M, N) -> a__U22#(tt(), M, N), a__U22#(tt(), M, N) -> mark# M) (a__U21#(tt(), M, N) -> a__U22#(tt(), M, N), a__U22#(tt(), M, N) -> a__plus#(a__x(mark N, mark M), mark N)) (a__U12#(tt(), M, N) -> a__plus#(mark N, mark M), a__plus#(N, 0()) -> mark# N) (a__U12#(tt(), M, N) -> a__plus#(mark N, mark M), a__plus#(N, s M) -> a__U11#(tt(), M, N)) (mark# x(X1, X2) -> a__x#(mark X1, mark X2), a__x#(N, s M) -> a__U21#(tt(), M, N)) (a__U22#(tt(), M, N) -> a__x#(mark N, mark M), a__x#(N, s M) -> a__U21#(tt(), M, N)) (a__U22#(tt(), M, N) -> mark# M, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (a__U22#(tt(), M, N) -> mark# M, mark# x(X1, X2) -> mark# X2) (a__U22#(tt(), M, N) -> mark# M, mark# x(X1, X2) -> mark# X1) (a__U22#(tt(), M, N) -> mark# M, mark# U22(X1, X2, X3) -> a__U22#(mark X1, X2, X3)) (a__U22#(tt(), M, N) -> mark# M, mark# U22(X1, X2, X3) -> mark# X1) (a__U22#(tt(), M, N) -> mark# M, mark# U21(X1, X2, X3) -> a__U21#(mark X1, X2, X3)) (a__U22#(tt(), M, N) -> mark# M, mark# U21(X1, X2, X3) -> mark# X1) (a__U22#(tt(), M, N) -> mark# M, mark# plus(X1, X2) -> mark# X2) (a__U22#(tt(), M, N) -> mark# M, mark# plus(X1, X2) -> mark# X1) (a__U22#(tt(), M, N) -> mark# M, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (a__U22#(tt(), M, N) -> mark# M, mark# U12(X1, X2, X3) -> mark# X1) (a__U22#(tt(), M, N) -> mark# M, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3)) (a__U22#(tt(), M, N) -> mark# M, mark# U11(X1, X2, X3) -> mark# X1) (a__U22#(tt(), M, N) -> mark# M, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (a__U22#(tt(), M, N) -> mark# M, mark# s X -> mark# X) (mark# U12(X1, X2, X3) -> mark# X1, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (mark# U12(X1, X2, X3) -> mark# X1, mark# x(X1, X2) -> mark# X2) (mark# U12(X1, X2, X3) -> mark# X1, mark# x(X1, X2) -> mark# X1) (mark# U12(X1, X2, X3) -> mark# X1, mark# U22(X1, X2, X3) -> a__U22#(mark X1, X2, X3)) (mark# U12(X1, X2, X3) -> mark# X1, mark# U22(X1, X2, X3) -> mark# X1) (mark# U12(X1, X2, X3) -> mark# X1, mark# U21(X1, X2, X3) -> a__U21#(mark X1, X2, X3)) (mark# U12(X1, X2, X3) -> mark# X1, mark# U21(X1, X2, X3) -> mark# X1) (mark# U12(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# U12(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# U12(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# U12(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> mark# X1) (mark# U12(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3)) (mark# U12(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> mark# X1) (mark# U12(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (mark# U12(X1, X2, X3) -> mark# X1, mark# s X -> mark# X) (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# U22(X1, X2, X3) -> a__U22#(mark X1, X2, X3)) (mark# U21(X1, X2, X3) -> mark# X1, mark# U22(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# U21(X1, X2, X3) -> 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) -> 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# U12(X1, X2, X3) -> mark# X1) (mark# U21(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3)) (mark# U21(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> mark# X1) (mark# U21(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (mark# U21(X1, X2, X3) -> mark# X1, mark# s X -> mark# X) (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# U22(X1, X2, X3) -> a__U22#(mark X1, X2, X3)) (mark# x(X1, X2) -> mark# X1, mark# U22(X1, X2, X3) -> mark# X1) (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# plus(X1, X2) -> mark# X2) (mark# x(X1, X2) -> mark# X1, mark# plus(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# U12(X1, X2, X3) -> mark# X1) (mark# x(X1, X2) -> mark# X1, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3)) (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# s X -> mark# X) (a__plus#(N, 0()) -> mark# N, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (a__plus#(N, 0()) -> mark# N, mark# x(X1, X2) -> mark# X2) (a__plus#(N, 0()) -> mark# N, mark# x(X1, X2) -> mark# X1) (a__plus#(N, 0()) -> mark# N, mark# U22(X1, X2, X3) -> a__U22#(mark X1, X2, X3)) (a__plus#(N, 0()) -> mark# N, mark# U22(X1, X2, X3) -> mark# X1) (a__plus#(N, 0()) -> mark# N, mark# U21(X1, X2, X3) -> a__U21#(mark X1, X2, X3)) (a__plus#(N, 0()) -> mark# N, mark# U21(X1, X2, X3) -> mark# X1) (a__plus#(N, 0()) -> mark# N, mark# plus(X1, X2) -> mark# X2) (a__plus#(N, 0()) -> mark# N, mark# plus(X1, X2) -> mark# X1) (a__plus#(N, 0()) -> mark# N, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (a__plus#(N, 0()) -> mark# N, mark# U12(X1, X2, X3) -> mark# X1) (a__plus#(N, 0()) -> mark# N, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3)) (a__plus#(N, 0()) -> mark# N, mark# U11(X1, X2, X3) -> mark# X1) (a__plus#(N, 0()) -> mark# N, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (a__plus#(N, 0()) -> mark# N, mark# s X -> mark# X) (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# U22(X1, X2, X3) -> a__U22#(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X2, mark# U22(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# U21(X1, X2, X3) -> mark# X1) (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# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# plus(X1, X2) -> mark# X2, mark# U12(X1, X2, X3) -> mark# X1) (mark# plus(X1, X2) -> mark# X2, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3)) (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# s X -> mark# X) (mark# x(X1, X2) -> mark# X2, mark# s X -> mark# 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, X3) -> a__U12#(mark X1, X2, X3)) (mark# x(X1, X2) -> mark# X2, mark# U12(X1, X2, X3) -> 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# X1) (mark# x(X1, X2) -> mark# X2, mark# plus(X1, X2) -> mark# 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# U22(X1, X2, X3) -> mark# X1) (mark# x(X1, X2) -> mark# X2, mark# U22(X1, X2, X3) -> a__U22#(mark X1, X2, X3)) (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)) (a__U22#(tt(), M, N) -> mark# N, mark# s X -> mark# X) (a__U22#(tt(), M, N) -> mark# N, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (a__U22#(tt(), M, N) -> mark# N, mark# U11(X1, X2, X3) -> mark# X1) (a__U22#(tt(), M, N) -> mark# N, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3)) (a__U22#(tt(), M, N) -> mark# N, mark# U12(X1, X2, X3) -> mark# X1) (a__U22#(tt(), M, N) -> mark# N, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (a__U22#(tt(), M, N) -> mark# N, mark# plus(X1, X2) -> mark# X1) (a__U22#(tt(), M, N) -> mark# N, mark# plus(X1, X2) -> mark# X2) (a__U22#(tt(), M, N) -> mark# N, mark# U21(X1, X2, X3) -> mark# X1) (a__U22#(tt(), M, N) -> mark# N, mark# U21(X1, X2, X3) -> a__U21#(mark X1, X2, X3)) (a__U22#(tt(), M, N) -> mark# N, mark# U22(X1, X2, X3) -> mark# X1) (a__U22#(tt(), M, N) -> mark# N, mark# U22(X1, X2, X3) -> a__U22#(mark X1, X2, X3)) (a__U22#(tt(), M, N) -> mark# N, mark# x(X1, X2) -> mark# X1) (a__U22#(tt(), M, N) -> mark# N, mark# x(X1, X2) -> mark# X2) (a__U22#(tt(), M, N) -> mark# N, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (a__U12#(tt(), M, N) -> mark# N, mark# s X -> mark# X) (a__U12#(tt(), M, N) -> mark# N, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (a__U12#(tt(), M, N) -> mark# N, mark# U11(X1, X2, X3) -> mark# X1) (a__U12#(tt(), M, N) -> mark# N, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3)) (a__U12#(tt(), M, N) -> mark# N, mark# U12(X1, X2, X3) -> mark# X1) (a__U12#(tt(), M, N) -> mark# N, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (a__U12#(tt(), M, N) -> mark# N, mark# plus(X1, X2) -> mark# X1) (a__U12#(tt(), M, N) -> mark# N, mark# plus(X1, X2) -> mark# X2) (a__U12#(tt(), M, N) -> mark# N, mark# U21(X1, X2, X3) -> mark# X1) (a__U12#(tt(), M, N) -> mark# N, mark# U21(X1, X2, X3) -> a__U21#(mark X1, X2, X3)) (a__U12#(tt(), M, N) -> mark# N, mark# U22(X1, X2, X3) -> mark# X1) (a__U12#(tt(), M, N) -> mark# N, mark# U22(X1, X2, X3) -> a__U22#(mark X1, X2, X3)) (a__U12#(tt(), M, N) -> mark# N, mark# x(X1, X2) -> mark# X1) (a__U12#(tt(), M, N) -> mark# N, mark# x(X1, X2) -> mark# X2) (a__U12#(tt(), M, N) -> mark# N, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (mark# U22(X1, X2, X3) -> mark# X1, mark# s X -> mark# X) (mark# U22(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (mark# U22(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> mark# X1) (mark# U22(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3)) (mark# U22(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> mark# X1) (mark# U22(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (mark# U22(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# U22(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# U22(X1, X2, X3) -> mark# X1, mark# U21(X1, X2, X3) -> mark# X1) (mark# U22(X1, X2, X3) -> mark# X1, mark# U21(X1, X2, X3) -> a__U21#(mark X1, X2, X3)) (mark# U22(X1, X2, X3) -> mark# X1, mark# U22(X1, X2, X3) -> mark# X1) (mark# U22(X1, X2, X3) -> mark# X1, mark# U22(X1, X2, X3) -> a__U22#(mark X1, X2, X3)) (mark# U22(X1, X2, X3) -> mark# X1, mark# x(X1, X2) -> mark# X1) (mark# U22(X1, X2, X3) -> mark# X1, mark# x(X1, X2) -> mark# X2) (mark# U22(X1, X2, X3) -> mark# X1, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (mark# plus(X1, X2) -> mark# X1, mark# s X -> mark# 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, X3) -> a__U12#(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X1, mark# U12(X1, X2, X3) -> 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# X1) (mark# plus(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# 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# U22(X1, X2, X3) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# U22(X1, X2, X3) -> a__U22#(mark X1, X2, X3)) (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# U11(X1, X2, X3) -> mark# X1, mark# s X -> mark# X) (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# U11(X1, X2, X3) -> mark# X1) (mark# U11(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3)) (mark# U11(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> 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# X1) (mark# U11(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# U11(X1, X2, X3) -> mark# X1, mark# U21(X1, X2, X3) -> mark# X1) (mark# U11(X1, X2, X3) -> mark# X1, mark# U21(X1, X2, X3) -> a__U21#(mark X1, X2, X3)) (mark# U11(X1, X2, X3) -> mark# X1, mark# U22(X1, X2, X3) -> mark# X1) (mark# U11(X1, X2, X3) -> mark# X1, mark# U22(X1, X2, X3) -> a__U22#(mark X1, X2, X3)) (mark# U11(X1, X2, X3) -> mark# X1, mark# x(X1, X2) -> mark# X1) (mark# U11(X1, X2, X3) -> mark# X1, mark# x(X1, X2) -> mark# X2) (mark# U11(X1, X2, X3) -> mark# X1, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (a__U12#(tt(), M, N) -> mark# M, mark# s X -> mark# X) (a__U12#(tt(), M, N) -> mark# M, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (a__U12#(tt(), M, N) -> mark# M, mark# U11(X1, X2, X3) -> mark# X1) (a__U12#(tt(), M, N) -> mark# M, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3)) (a__U12#(tt(), M, N) -> mark# M, mark# U12(X1, X2, X3) -> mark# X1) (a__U12#(tt(), M, N) -> mark# M, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2)) (a__U12#(tt(), M, N) -> mark# M, mark# plus(X1, X2) -> mark# X1) (a__U12#(tt(), M, N) -> mark# M, mark# plus(X1, X2) -> mark# X2) (a__U12#(tt(), M, N) -> mark# M, mark# U21(X1, X2, X3) -> mark# X1) (a__U12#(tt(), M, N) -> mark# M, mark# U21(X1, X2, X3) -> a__U21#(mark X1, X2, X3)) (a__U12#(tt(), M, N) -> mark# M, mark# U22(X1, X2, X3) -> mark# X1) (a__U12#(tt(), M, N) -> mark# M, mark# U22(X1, X2, X3) -> a__U22#(mark X1, X2, X3)) (a__U12#(tt(), M, N) -> mark# M, mark# x(X1, X2) -> mark# X1) (a__U12#(tt(), M, N) -> mark# M, mark# x(X1, X2) -> mark# X2) (a__U12#(tt(), M, N) -> mark# M, mark# x(X1, X2) -> a__x#(mark X1, mark X2)) (a__U22#(tt(), M, N) -> a__plus#(a__x(mark N, mark M), mark N), a__plus#(N, s M) -> a__U11#(tt(), M, N)) (a__U22#(tt(), M, N) -> a__plus#(a__x(mark N, mark M), mark N), a__plus#(N, 0()) -> mark# N) (mark# plus(X1, X2) -> a__plus#(mark X1, mark X2), a__plus#(N, s M) -> a__U11#(tt(), M, N)) (mark# plus(X1, X2) -> a__plus#(mark X1, mark X2), a__plus#(N, 0()) -> mark# N) (a__x#(N, s M) -> a__U21#(tt(), M, N), a__U21#(tt(), M, N) -> a__U22#(tt(), M, N)) (a__plus#(N, s M) -> a__U11#(tt(), M, N), a__U11#(tt(), M, N) -> a__U12#(tt(), M, N)) (mark# U22(X1, X2, X3) -> a__U22#(mark X1, X2, X3), a__U22#(tt(), M, N) -> a__plus#(a__x(mark N, mark M), mark N)) (mark# U22(X1, X2, X3) -> a__U22#(mark X1, X2, X3), a__U22#(tt(), M, N) -> mark# M) (mark# U22(X1, X2, X3) -> a__U22#(mark X1, X2, X3), a__U22#(tt(), M, N) -> mark# N) (mark# U22(X1, X2, X3) -> a__U22#(mark X1, X2, X3), a__U22#(tt(), M, N) -> a__x#(mark N, mark M)) (mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3), a__U12#(tt(), M, N) -> a__plus#(mark N, mark M)) (mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3), a__U12#(tt(), M, N) -> mark# M) (mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3), a__U12#(tt(), M, N) -> mark# N) (mark# s X -> mark# X, mark# s X -> mark# X) (mark# s X -> mark# X, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3)) (mark# s X -> mark# X, mark# U11(X1, X2, X3) -> mark# X1) (mark# s X -> mark# X, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3)) (mark# s X -> mark# X, mark# U12(X1, X2, X3) -> 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# X1) (mark# s X -> mark# X, mark# plus(X1, X2) -> mark# 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# U22(X1, X2, X3) -> mark# X1) (mark# s X -> mark# X, mark# U22(X1, X2, X3) -> a__U22#(mark X1, X2, X3)) (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)) } STATUS: arrows: 0.676269 SCCS (1): Scc: { a__U12#(tt(), M, N) -> a__plus#(mark N, mark M), a__U12#(tt(), M, N) -> mark# M, a__U12#(tt(), M, N) -> mark# N, a__U11#(tt(), M, N) -> a__U12#(tt(), M, N), a__plus#(N, s M) -> a__U11#(tt(), M, N), a__plus#(N, 0()) -> mark# N, mark# s X -> mark# X, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3), mark# U11(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3), mark# U12(X1, X2, X3) -> 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# U21(X1, X2, X3) -> mark# X1, mark# U21(X1, X2, X3) -> a__U21#(mark X1, X2, X3), mark# U22(X1, X2, X3) -> mark# X1, mark# U22(X1, X2, X3) -> a__U22#(mark X1, X2, X3), mark# x(X1, X2) -> mark# X1, mark# x(X1, X2) -> mark# X2, mark# x(X1, X2) -> a__x#(mark X1, mark X2), a__U22#(tt(), M, N) -> a__plus#(a__x(mark N, mark M), mark N), a__U22#(tt(), M, N) -> mark# M, a__U22#(tt(), M, N) -> mark# N, a__U22#(tt(), M, N) -> a__x#(mark N, mark M), a__U21#(tt(), M, N) -> a__U22#(tt(), M, N), a__x#(N, s M) -> a__U21#(tt(), M, N)} SCC (27): Strict: { a__U12#(tt(), M, N) -> a__plus#(mark N, mark M), a__U12#(tt(), M, N) -> mark# M, a__U12#(tt(), M, N) -> mark# N, a__U11#(tt(), M, N) -> a__U12#(tt(), M, N), a__plus#(N, s M) -> a__U11#(tt(), M, N), a__plus#(N, 0()) -> mark# N, mark# s X -> mark# X, mark# U11(X1, X2, X3) -> a__U11#(mark X1, X2, X3), mark# U11(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> a__U12#(mark X1, X2, X3), mark# U12(X1, X2, X3) -> 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# U21(X1, X2, X3) -> mark# X1, mark# U21(X1, X2, X3) -> a__U21#(mark X1, X2, X3), mark# U22(X1, X2, X3) -> mark# X1, mark# U22(X1, X2, X3) -> a__U22#(mark X1, X2, X3), mark# x(X1, X2) -> mark# X1, mark# x(X1, X2) -> mark# X2, mark# x(X1, X2) -> a__x#(mark X1, mark X2), a__U22#(tt(), M, N) -> a__plus#(a__x(mark N, mark M), mark N), a__U22#(tt(), M, N) -> mark# M, a__U22#(tt(), M, N) -> mark# N, a__U22#(tt(), M, N) -> a__x#(mark N, mark M), a__U21#(tt(), M, N) -> a__U22#(tt(), M, N), a__x#(N, s M) -> a__U21#(tt(), M, N)} Weak: { a__U12(X1, X2, X3) -> U12(X1, X2, X3), a__U12(tt(), M, N) -> s a__plus(mark N, mark M), a__U11(X1, X2, X3) -> U11(X1, X2, X3), a__U11(tt(), M, N) -> a__U12(tt(), M, N), a__plus(N, s M) -> a__U11(tt(), M, N), a__plus(N, 0()) -> mark N, a__plus(X1, X2) -> plus(X1, X2), mark tt() -> tt(), mark s X -> s mark X, mark 0() -> 0(), mark U11(X1, X2, X3) -> a__U11(mark X1, X2, X3), mark U12(X1, X2, X3) -> a__U12(mark X1, X2, X3), mark plus(X1, X2) -> a__plus(mark X1, mark X2), mark U21(X1, X2, X3) -> a__U21(mark X1, X2, X3), mark U22(X1, X2, X3) -> a__U22(mark X1, X2, X3), mark x(X1, X2) -> a__x(mark X1, mark X2), a__U22(X1, X2, X3) -> U22(X1, X2, X3), a__U22(tt(), M, N) -> a__plus(a__x(mark N, mark M), mark N), a__U21(X1, X2, X3) -> U21(X1, X2, X3), a__U21(tt(), M, N) -> a__U22(tt(), M, N), a__x(N, s M) -> a__U21(tt(), M, N), a__x(N, 0()) -> 0(), a__x(X1, X2) -> x(X1, X2)} Open