MAYBE Time: 0.157552 TRS: { mark U12(X1, X2, X3) -> active U12(mark X1, X2, X3), mark tt() -> active tt(), mark U11(X1, X2, X3) -> active U11(mark X1, X2, X3), mark s X -> active s mark X, mark plus(X1, X2) -> active plus(mark X1, mark X2), mark U22(X1, X2, X3) -> active U22(mark X1, X2, X3), mark U21(X1, X2, X3) -> active U21(mark X1, X2, X3), mark x(X1, X2) -> active x(mark X1, mark X2), mark 0() -> active 0(), U12(X1, X2, mark X3) -> U12(X1, X2, X3), U12(X1, X2, active X3) -> U12(X1, X2, X3), U12(X1, mark X2, X3) -> U12(X1, X2, X3), U12(X1, active X2, X3) -> U12(X1, X2, X3), U12(mark X1, X2, X3) -> U12(X1, X2, X3), U12(active X1, X2, X3) -> U12(X1, X2, X3), active U12(tt(), M, N) -> mark s plus(N, M), active U11(tt(), M, N) -> mark U12(tt(), M, N), active plus(N, s M) -> mark U11(tt(), M, N), active plus(N, 0()) -> mark N, active U22(tt(), M, N) -> mark plus(x(N, M), N), active U21(tt(), M, N) -> mark U22(tt(), M, N), active x(N, s M) -> mark U21(tt(), M, N), active x(N, 0()) -> mark 0(), U11(X1, X2, mark X3) -> U11(X1, X2, X3), U11(X1, X2, active X3) -> U11(X1, X2, X3), U11(X1, mark X2, X3) -> U11(X1, X2, X3), U11(X1, active X2, X3) -> U11(X1, X2, X3), U11(mark X1, X2, X3) -> U11(X1, X2, X3), U11(active X1, X2, X3) -> U11(X1, X2, X3), s mark X -> s X, s active X -> s X, plus(X1, mark X2) -> plus(X1, X2), plus(X1, active X2) -> plus(X1, X2), plus(mark X1, X2) -> plus(X1, X2), plus(active X1, X2) -> plus(X1, X2), U22(X1, X2, mark X3) -> U22(X1, X2, X3), U22(X1, X2, active X3) -> U22(X1, X2, X3), U22(X1, mark X2, X3) -> U22(X1, X2, X3), U22(X1, active X2, X3) -> U22(X1, X2, X3), U22(mark X1, X2, X3) -> U22(X1, X2, X3), U22(active X1, X2, X3) -> U22(X1, X2, X3), U21(X1, X2, mark X3) -> U21(X1, X2, X3), U21(X1, X2, active X3) -> U21(X1, X2, X3), U21(X1, mark X2, X3) -> U21(X1, X2, X3), U21(X1, active X2, X3) -> U21(X1, X2, X3), U21(mark X1, X2, X3) -> U21(X1, X2, X3), U21(active X1, X2, X3) -> U21(X1, X2, X3), x(X1, mark X2) -> x(X1, X2), x(X1, active X2) -> x(X1, X2), x(mark X1, X2) -> x(X1, X2), x(active X1, X2) -> x(X1, X2)} DP: DP: { mark# U12(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> U12#(mark X1, X2, X3), mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3), mark# tt() -> active# tt(), mark# U11(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> active# U11(mark X1, X2, X3), mark# U11(X1, X2, X3) -> U11#(mark X1, X2, X3), mark# s X -> mark# X, mark# s X -> active# s mark X, mark# s X -> s# mark X, mark# plus(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X2, mark# plus(X1, X2) -> active# plus(mark X1, mark X2), mark# plus(X1, X2) -> plus#(mark X1, mark X2), mark# U22(X1, X2, X3) -> mark# X1, mark# U22(X1, X2, X3) -> active# U22(mark X1, X2, X3), mark# U22(X1, X2, X3) -> U22#(mark X1, X2, X3), mark# U21(X1, X2, X3) -> mark# X1, mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3), mark# U21(X1, X2, X3) -> U21#(mark X1, X2, X3), mark# x(X1, X2) -> mark# X1, mark# x(X1, X2) -> mark# X2, mark# x(X1, X2) -> active# x(mark X1, mark X2), mark# x(X1, X2) -> x#(mark X1, mark X2), mark# 0() -> active# 0(), U12#(X1, X2, mark X3) -> U12#(X1, X2, X3), U12#(X1, X2, active X3) -> U12#(X1, X2, X3), U12#(X1, mark X2, X3) -> U12#(X1, X2, X3), U12#(X1, active X2, X3) -> U12#(X1, X2, X3), U12#(mark X1, X2, X3) -> U12#(X1, X2, X3), U12#(active X1, X2, X3) -> U12#(X1, X2, X3), active# U12(tt(), M, N) -> mark# s plus(N, M), active# U12(tt(), M, N) -> s# plus(N, M), active# U12(tt(), M, N) -> plus#(N, M), active# U11(tt(), M, N) -> mark# U12(tt(), M, N), active# U11(tt(), M, N) -> U12#(tt(), M, N), active# plus(N, s M) -> mark# U11(tt(), M, N), active# plus(N, s M) -> U11#(tt(), M, N), active# plus(N, 0()) -> mark# N, active# U22(tt(), M, N) -> mark# plus(x(N, M), N), active# U22(tt(), M, N) -> plus#(x(N, M), N), active# U22(tt(), M, N) -> x#(N, M), active# U21(tt(), M, N) -> mark# U22(tt(), M, N), active# U21(tt(), M, N) -> U22#(tt(), M, N), active# x(N, s M) -> mark# U21(tt(), M, N), active# x(N, s M) -> U21#(tt(), M, N), active# x(N, 0()) -> mark# 0(), U11#(X1, X2, mark X3) -> U11#(X1, X2, X3), U11#(X1, X2, active X3) -> U11#(X1, X2, X3), U11#(X1, mark X2, X3) -> U11#(X1, X2, X3), U11#(X1, active X2, X3) -> U11#(X1, X2, X3), U11#(mark X1, X2, X3) -> U11#(X1, X2, X3), U11#(active X1, X2, X3) -> U11#(X1, X2, X3), s# mark X -> s# X, s# active X -> s# X, plus#(X1, mark X2) -> plus#(X1, X2), plus#(X1, active X2) -> plus#(X1, X2), plus#(mark X1, X2) -> plus#(X1, X2), plus#(active X1, X2) -> plus#(X1, X2), U22#(X1, X2, mark X3) -> U22#(X1, X2, X3), U22#(X1, X2, active X3) -> U22#(X1, X2, X3), U22#(X1, mark X2, X3) -> U22#(X1, X2, X3), U22#(X1, active X2, X3) -> U22#(X1, X2, X3), U22#(mark X1, X2, X3) -> U22#(X1, X2, X3), U22#(active X1, X2, X3) -> U22#(X1, X2, X3), U21#(X1, X2, mark X3) -> U21#(X1, X2, X3), U21#(X1, X2, active X3) -> U21#(X1, X2, X3), U21#(X1, mark X2, X3) -> U21#(X1, X2, X3), U21#(X1, active X2, X3) -> U21#(X1, X2, X3), U21#(mark X1, X2, X3) -> U21#(X1, X2, X3), U21#(active X1, X2, X3) -> U21#(X1, X2, X3), x#(X1, mark X2) -> x#(X1, X2), x#(X1, active X2) -> x#(X1, X2), x#(mark X1, X2) -> x#(X1, X2), x#(active X1, X2) -> x#(X1, X2)} TRS: { mark U12(X1, X2, X3) -> active U12(mark X1, X2, X3), mark tt() -> active tt(), mark U11(X1, X2, X3) -> active U11(mark X1, X2, X3), mark s X -> active s mark X, mark plus(X1, X2) -> active plus(mark X1, mark X2), mark U22(X1, X2, X3) -> active U22(mark X1, X2, X3), mark U21(X1, X2, X3) -> active U21(mark X1, X2, X3), mark x(X1, X2) -> active x(mark X1, mark X2), mark 0() -> active 0(), U12(X1, X2, mark X3) -> U12(X1, X2, X3), U12(X1, X2, active X3) -> U12(X1, X2, X3), U12(X1, mark X2, X3) -> U12(X1, X2, X3), U12(X1, active X2, X3) -> U12(X1, X2, X3), U12(mark X1, X2, X3) -> U12(X1, X2, X3), U12(active X1, X2, X3) -> U12(X1, X2, X3), active U12(tt(), M, N) -> mark s plus(N, M), active U11(tt(), M, N) -> mark U12(tt(), M, N), active plus(N, s M) -> mark U11(tt(), M, N), active plus(N, 0()) -> mark N, active U22(tt(), M, N) -> mark plus(x(N, M), N), active U21(tt(), M, N) -> mark U22(tt(), M, N), active x(N, s M) -> mark U21(tt(), M, N), active x(N, 0()) -> mark 0(), U11(X1, X2, mark X3) -> U11(X1, X2, X3), U11(X1, X2, active X3) -> U11(X1, X2, X3), U11(X1, mark X2, X3) -> U11(X1, X2, X3), U11(X1, active X2, X3) -> U11(X1, X2, X3), U11(mark X1, X2, X3) -> U11(X1, X2, X3), U11(active X1, X2, X3) -> U11(X1, X2, X3), s mark X -> s X, s active X -> s X, plus(X1, mark X2) -> plus(X1, X2), plus(X1, active X2) -> plus(X1, X2), plus(mark X1, X2) -> plus(X1, X2), plus(active X1, X2) -> plus(X1, X2), U22(X1, X2, mark X3) -> U22(X1, X2, X3), U22(X1, X2, active X3) -> U22(X1, X2, X3), U22(X1, mark X2, X3) -> U22(X1, X2, X3), U22(X1, active X2, X3) -> U22(X1, X2, X3), U22(mark X1, X2, X3) -> U22(X1, X2, X3), U22(active X1, X2, X3) -> U22(X1, X2, X3), U21(X1, X2, mark X3) -> U21(X1, X2, X3), U21(X1, X2, active X3) -> U21(X1, X2, X3), U21(X1, mark X2, X3) -> U21(X1, X2, X3), U21(X1, active X2, X3) -> U21(X1, X2, X3), U21(mark X1, X2, X3) -> U21(X1, X2, X3), U21(active X1, X2, X3) -> U21(X1, X2, X3), x(X1, mark X2) -> x(X1, X2), x(X1, active X2) -> x(X1, X2), x(mark X1, X2) -> x(X1, X2), x(active X1, X2) -> x(X1, X2)} EDG: { (s# mark X -> s# X, s# active X -> s# X) (s# mark X -> s# X, s# mark X -> s# X) (mark# U12(X1, X2, X3) -> U12#(mark X1, X2, X3), U12#(active X1, X2, X3) -> U12#(X1, X2, X3)) (mark# U12(X1, X2, X3) -> U12#(mark X1, X2, X3), U12#(mark X1, X2, X3) -> U12#(X1, X2, X3)) (mark# U12(X1, X2, X3) -> U12#(mark X1, X2, X3), U12#(X1, active X2, X3) -> U12#(X1, X2, X3)) (mark# U12(X1, X2, X3) -> U12#(mark X1, X2, X3), U12#(X1, mark X2, X3) -> U12#(X1, X2, X3)) (mark# U12(X1, X2, X3) -> U12#(mark X1, X2, X3), U12#(X1, X2, active X3) -> U12#(X1, X2, X3)) (mark# U12(X1, X2, X3) -> U12#(mark X1, X2, X3), U12#(X1, X2, mark X3) -> U12#(X1, X2, X3)) (mark# U22(X1, X2, X3) -> U22#(mark X1, X2, X3), U22#(active X1, X2, X3) -> U22#(X1, X2, X3)) (mark# U22(X1, X2, X3) -> U22#(mark X1, X2, X3), U22#(mark X1, X2, X3) -> U22#(X1, X2, X3)) (mark# U22(X1, X2, X3) -> U22#(mark X1, X2, X3), U22#(X1, active X2, X3) -> U22#(X1, X2, X3)) (mark# U22(X1, X2, X3) -> U22#(mark X1, X2, X3), U22#(X1, mark X2, X3) -> U22#(X1, X2, X3)) (mark# U22(X1, X2, X3) -> U22#(mark X1, X2, X3), U22#(X1, X2, active X3) -> U22#(X1, X2, X3)) (mark# U22(X1, X2, X3) -> U22#(mark X1, X2, X3), U22#(X1, X2, mark X3) -> U22#(X1, X2, X3)) (U12#(X1, X2, mark X3) -> U12#(X1, X2, X3), U12#(active X1, X2, X3) -> U12#(X1, X2, X3)) (U12#(X1, X2, mark X3) -> U12#(X1, X2, X3), U12#(mark X1, X2, X3) -> U12#(X1, X2, X3)) (U12#(X1, X2, mark X3) -> U12#(X1, X2, X3), U12#(X1, active X2, X3) -> U12#(X1, X2, X3)) (U12#(X1, X2, mark X3) -> U12#(X1, X2, X3), U12#(X1, mark X2, X3) -> U12#(X1, X2, X3)) (U12#(X1, X2, mark X3) -> U12#(X1, X2, X3), U12#(X1, X2, active X3) -> U12#(X1, X2, X3)) (U12#(X1, X2, mark X3) -> U12#(X1, X2, X3), U12#(X1, X2, mark X3) -> U12#(X1, X2, X3)) (U12#(X1, mark X2, X3) -> U12#(X1, X2, X3), U12#(active X1, X2, X3) -> U12#(X1, X2, X3)) (U12#(X1, mark X2, X3) -> U12#(X1, X2, X3), U12#(mark X1, X2, X3) -> U12#(X1, X2, X3)) (U12#(X1, mark X2, X3) -> U12#(X1, X2, X3), U12#(X1, active X2, X3) -> U12#(X1, X2, X3)) (U12#(X1, mark X2, X3) -> U12#(X1, X2, X3), U12#(X1, mark X2, X3) -> U12#(X1, X2, X3)) (U12#(X1, mark X2, X3) -> U12#(X1, X2, X3), U12#(X1, X2, active X3) -> U12#(X1, X2, X3)) (U12#(X1, mark X2, X3) -> U12#(X1, X2, X3), U12#(X1, X2, mark X3) -> U12#(X1, X2, X3)) (U12#(mark X1, X2, X3) -> U12#(X1, X2, X3), U12#(active X1, X2, X3) -> U12#(X1, X2, X3)) (U12#(mark X1, X2, X3) -> U12#(X1, X2, X3), U12#(mark X1, X2, X3) -> U12#(X1, X2, X3)) (U12#(mark X1, X2, X3) -> U12#(X1, X2, X3), U12#(X1, active X2, X3) -> U12#(X1, X2, X3)) (U12#(mark X1, X2, X3) -> U12#(X1, X2, X3), U12#(X1, mark X2, X3) -> U12#(X1, X2, X3)) (U12#(mark X1, X2, X3) -> U12#(X1, X2, X3), U12#(X1, X2, active X3) -> U12#(X1, X2, X3)) (U12#(mark X1, X2, X3) -> U12#(X1, X2, X3), U12#(X1, X2, mark X3) -> U12#(X1, X2, X3)) (U11#(X1, X2, mark X3) -> U11#(X1, X2, X3), U11#(active X1, X2, X3) -> U11#(X1, X2, X3)) (U11#(X1, X2, mark X3) -> U11#(X1, X2, X3), U11#(mark X1, X2, X3) -> U11#(X1, X2, X3)) (U11#(X1, X2, mark X3) -> U11#(X1, X2, X3), U11#(X1, active X2, X3) -> U11#(X1, X2, X3)) (U11#(X1, X2, mark X3) -> U11#(X1, X2, X3), U11#(X1, mark X2, X3) -> U11#(X1, X2, X3)) (U11#(X1, X2, mark X3) -> U11#(X1, X2, X3), U11#(X1, X2, active X3) -> U11#(X1, X2, X3)) (U11#(X1, X2, mark X3) -> U11#(X1, X2, X3), U11#(X1, X2, mark X3) -> U11#(X1, X2, X3)) (U11#(X1, mark X2, X3) -> U11#(X1, X2, X3), U11#(active X1, X2, X3) -> U11#(X1, X2, X3)) (U11#(X1, mark X2, X3) -> U11#(X1, X2, X3), U11#(mark X1, X2, X3) -> U11#(X1, X2, X3)) (U11#(X1, mark X2, X3) -> U11#(X1, X2, X3), U11#(X1, active X2, X3) -> U11#(X1, X2, X3)) (U11#(X1, mark X2, X3) -> U11#(X1, X2, X3), U11#(X1, mark X2, X3) -> U11#(X1, X2, X3)) (U11#(X1, mark X2, X3) -> U11#(X1, X2, X3), U11#(X1, X2, active X3) -> U11#(X1, X2, X3)) (U11#(X1, mark X2, X3) -> U11#(X1, X2, X3), U11#(X1, X2, mark X3) -> U11#(X1, X2, X3)) (U11#(mark X1, X2, X3) -> U11#(X1, X2, X3), U11#(active X1, X2, X3) -> U11#(X1, X2, X3)) (U11#(mark X1, X2, X3) -> U11#(X1, X2, X3), U11#(mark X1, X2, X3) -> U11#(X1, X2, X3)) (U11#(mark X1, X2, X3) -> U11#(X1, X2, X3), U11#(X1, active X2, X3) -> U11#(X1, X2, X3)) (U11#(mark X1, X2, X3) -> U11#(X1, X2, X3), U11#(X1, mark X2, X3) -> U11#(X1, X2, X3)) (U11#(mark X1, X2, X3) -> U11#(X1, X2, X3), U11#(X1, X2, active X3) -> U11#(X1, X2, X3)) (U11#(mark X1, X2, X3) -> U11#(X1, X2, X3), U11#(X1, X2, mark X3) -> U11#(X1, X2, X3)) (U22#(X1, X2, mark X3) -> U22#(X1, X2, X3), U22#(active X1, X2, X3) -> U22#(X1, X2, X3)) (U22#(X1, X2, mark X3) -> U22#(X1, X2, X3), U22#(mark X1, X2, X3) -> U22#(X1, X2, X3)) (U22#(X1, X2, mark X3) -> U22#(X1, X2, X3), U22#(X1, active X2, X3) -> U22#(X1, X2, X3)) (U22#(X1, X2, mark X3) -> U22#(X1, X2, X3), U22#(X1, mark X2, X3) -> U22#(X1, X2, X3)) (U22#(X1, X2, mark X3) -> U22#(X1, X2, X3), U22#(X1, X2, active X3) -> U22#(X1, X2, X3)) (U22#(X1, X2, mark X3) -> U22#(X1, X2, X3), U22#(X1, X2, mark X3) -> U22#(X1, X2, X3)) (U22#(X1, mark X2, X3) -> U22#(X1, X2, X3), U22#(active X1, X2, X3) -> U22#(X1, X2, X3)) (U22#(X1, mark X2, X3) -> U22#(X1, X2, X3), U22#(mark X1, X2, X3) -> U22#(X1, X2, X3)) (U22#(X1, mark X2, X3) -> U22#(X1, X2, X3), U22#(X1, active X2, X3) -> U22#(X1, X2, X3)) (U22#(X1, mark X2, X3) -> U22#(X1, X2, X3), U22#(X1, mark X2, X3) -> U22#(X1, X2, X3)) (U22#(X1, mark X2, X3) -> U22#(X1, X2, X3), U22#(X1, X2, active X3) -> U22#(X1, X2, X3)) (U22#(X1, mark X2, X3) -> U22#(X1, X2, X3), U22#(X1, X2, mark X3) -> U22#(X1, X2, X3)) (U22#(mark X1, X2, X3) -> U22#(X1, X2, X3), U22#(active X1, X2, X3) -> U22#(X1, X2, X3)) (U22#(mark X1, X2, X3) -> U22#(X1, X2, X3), U22#(mark X1, X2, X3) -> U22#(X1, X2, X3)) (U22#(mark X1, X2, X3) -> U22#(X1, X2, X3), U22#(X1, active X2, X3) -> U22#(X1, X2, X3)) (U22#(mark X1, X2, X3) -> U22#(X1, X2, X3), U22#(X1, mark X2, X3) -> U22#(X1, X2, X3)) (U22#(mark X1, X2, X3) -> U22#(X1, X2, X3), U22#(X1, X2, active X3) -> U22#(X1, X2, X3)) (U22#(mark X1, X2, X3) -> U22#(X1, X2, X3), U22#(X1, X2, mark X3) -> U22#(X1, X2, X3)) (U21#(X1, X2, mark X3) -> U21#(X1, X2, X3), U21#(active X1, X2, X3) -> U21#(X1, X2, X3)) (U21#(X1, X2, mark X3) -> U21#(X1, X2, X3), U21#(mark X1, X2, X3) -> U21#(X1, X2, X3)) (U21#(X1, X2, mark X3) -> U21#(X1, X2, X3), U21#(X1, active X2, X3) -> U21#(X1, X2, X3)) (U21#(X1, X2, mark X3) -> U21#(X1, X2, X3), U21#(X1, mark X2, X3) -> U21#(X1, X2, X3)) (U21#(X1, X2, mark X3) -> U21#(X1, X2, X3), U21#(X1, X2, active X3) -> U21#(X1, X2, X3)) (U21#(X1, X2, mark X3) -> U21#(X1, X2, X3), U21#(X1, X2, mark X3) -> U21#(X1, X2, X3)) (U21#(X1, mark X2, X3) -> U21#(X1, X2, X3), U21#(active X1, X2, X3) -> U21#(X1, X2, X3)) (U21#(X1, mark X2, X3) -> U21#(X1, X2, X3), U21#(mark X1, X2, X3) -> U21#(X1, X2, X3)) (U21#(X1, mark X2, X3) -> U21#(X1, X2, X3), U21#(X1, active X2, X3) -> U21#(X1, X2, X3)) (U21#(X1, mark X2, X3) -> U21#(X1, X2, X3), U21#(X1, mark X2, X3) -> U21#(X1, X2, X3)) (U21#(X1, mark X2, X3) -> U21#(X1, X2, X3), U21#(X1, X2, active X3) -> U21#(X1, X2, X3)) (U21#(X1, mark X2, X3) -> U21#(X1, X2, X3), U21#(X1, X2, mark X3) -> U21#(X1, X2, X3)) (U21#(mark X1, X2, X3) -> U21#(X1, X2, X3), U21#(active X1, X2, X3) -> U21#(X1, X2, X3)) (U21#(mark X1, X2, X3) -> U21#(X1, X2, X3), U21#(mark X1, X2, X3) -> U21#(X1, X2, X3)) (U21#(mark X1, X2, X3) -> U21#(X1, X2, X3), U21#(X1, active X2, X3) -> U21#(X1, X2, X3)) (U21#(mark X1, X2, X3) -> U21#(X1, X2, X3), U21#(X1, mark X2, X3) -> U21#(X1, X2, X3)) (U21#(mark X1, X2, X3) -> U21#(X1, X2, X3), U21#(X1, X2, active X3) -> U21#(X1, X2, X3)) (U21#(mark X1, X2, X3) -> U21#(X1, X2, X3), U21#(X1, X2, mark X3) -> U21#(X1, X2, X3)) (plus#(X1, mark X2) -> plus#(X1, X2), plus#(active X1, X2) -> plus#(X1, X2)) (plus#(X1, mark X2) -> plus#(X1, X2), plus#(mark X1, X2) -> plus#(X1, X2)) (plus#(X1, mark X2) -> plus#(X1, X2), plus#(X1, active X2) -> plus#(X1, X2)) (plus#(X1, mark X2) -> plus#(X1, X2), plus#(X1, mark X2) -> plus#(X1, X2)) (plus#(mark X1, X2) -> plus#(X1, X2), plus#(active X1, X2) -> plus#(X1, X2)) (plus#(mark X1, X2) -> plus#(X1, X2), plus#(mark X1, X2) -> plus#(X1, X2)) (plus#(mark X1, X2) -> plus#(X1, X2), plus#(X1, active X2) -> plus#(X1, X2)) (plus#(mark X1, X2) -> plus#(X1, X2), plus#(X1, mark X2) -> plus#(X1, X2)) (x#(X1, mark X2) -> x#(X1, X2), x#(active X1, X2) -> x#(X1, X2)) (x#(X1, mark X2) -> x#(X1, X2), x#(mark X1, X2) -> x#(X1, X2)) (x#(X1, mark X2) -> x#(X1, X2), x#(X1, active X2) -> x#(X1, X2)) (x#(X1, mark X2) -> x#(X1, X2), x#(X1, mark X2) -> x#(X1, X2)) (x#(mark X1, X2) -> x#(X1, X2), x#(active X1, X2) -> x#(X1, X2)) (x#(mark X1, X2) -> x#(X1, X2), x#(mark X1, X2) -> x#(X1, X2)) (x#(mark X1, X2) -> x#(X1, X2), x#(X1, active X2) -> x#(X1, X2)) (x#(mark X1, X2) -> x#(X1, X2), x#(X1, mark X2) -> x#(X1, X2)) (mark# plus(X1, X2) -> active# plus(mark X1, mark X2), active# x(N, 0()) -> mark# 0()) (mark# plus(X1, X2) -> active# plus(mark X1, mark X2), active# x(N, s M) -> U21#(tt(), M, N)) (mark# plus(X1, X2) -> active# plus(mark X1, mark X2), active# x(N, s M) -> mark# U21(tt(), M, N)) (mark# plus(X1, X2) -> active# plus(mark X1, mark X2), active# U21(tt(), M, N) -> U22#(tt(), M, N)) (mark# plus(X1, X2) -> active# plus(mark X1, mark X2), active# U21(tt(), M, N) -> mark# U22(tt(), M, N)) (mark# plus(X1, X2) -> active# plus(mark X1, mark X2), active# U22(tt(), M, N) -> x#(N, M)) (mark# plus(X1, X2) -> active# plus(mark X1, mark X2), active# U22(tt(), M, N) -> plus#(x(N, M), N)) (mark# plus(X1, X2) -> active# plus(mark X1, mark X2), active# U22(tt(), M, N) -> mark# plus(x(N, M), N)) (mark# plus(X1, X2) -> active# plus(mark X1, mark X2), active# plus(N, 0()) -> mark# N) (mark# plus(X1, X2) -> active# plus(mark X1, mark X2), active# plus(N, s M) -> U11#(tt(), M, N)) (mark# plus(X1, X2) -> active# plus(mark X1, mark X2), active# plus(N, s M) -> mark# U11(tt(), M, N)) (mark# plus(X1, X2) -> active# plus(mark X1, mark X2), active# U11(tt(), M, N) -> U12#(tt(), M, N)) (mark# plus(X1, X2) -> active# plus(mark X1, mark X2), active# U11(tt(), M, N) -> mark# U12(tt(), M, N)) (mark# plus(X1, X2) -> active# plus(mark X1, mark X2), active# U12(tt(), M, N) -> plus#(N, M)) (mark# plus(X1, X2) -> active# plus(mark X1, mark X2), active# U12(tt(), M, N) -> s# plus(N, M)) (mark# plus(X1, X2) -> active# plus(mark X1, mark X2), active# U12(tt(), M, N) -> mark# s plus(N, M)) (mark# s X -> s# mark X, s# active X -> s# X) (mark# s X -> s# mark X, s# mark X -> s# X) (active# U22(tt(), M, N) -> x#(N, M), x#(active X1, X2) -> x#(X1, X2)) (active# U22(tt(), M, N) -> x#(N, M), x#(mark X1, X2) -> x#(X1, X2)) (active# U22(tt(), M, N) -> x#(N, M), x#(X1, active X2) -> x#(X1, X2)) (active# U22(tt(), M, N) -> x#(N, M), x#(X1, mark X2) -> x#(X1, X2)) (active# U12(tt(), M, N) -> s# plus(N, M), s# active X -> s# X) (active# U12(tt(), M, N) -> s# plus(N, M), s# mark X -> s# X) (mark# plus(X1, X2) -> plus#(mark X1, mark X2), plus#(active X1, X2) -> plus#(X1, X2)) (mark# plus(X1, X2) -> plus#(mark X1, mark X2), plus#(mark X1, X2) -> plus#(X1, X2)) (mark# plus(X1, X2) -> plus#(mark X1, mark X2), plus#(X1, active X2) -> plus#(X1, X2)) (mark# plus(X1, X2) -> plus#(mark X1, mark X2), plus#(X1, mark X2) -> plus#(X1, X2)) (mark# s X -> active# s mark X, active# x(N, 0()) -> mark# 0()) (mark# s X -> active# s mark X, active# x(N, s M) -> U21#(tt(), M, N)) (mark# s X -> active# s mark X, active# x(N, s M) -> mark# U21(tt(), M, N)) (mark# s X -> active# s mark X, active# U21(tt(), M, N) -> U22#(tt(), M, N)) (mark# s X -> active# s mark X, active# U21(tt(), M, N) -> mark# U22(tt(), M, N)) (mark# s X -> active# s mark X, active# U22(tt(), M, N) -> x#(N, M)) (mark# s X -> active# s mark X, active# U22(tt(), M, N) -> plus#(x(N, M), N)) (mark# s X -> active# s mark X, active# U22(tt(), M, N) -> mark# plus(x(N, M), N)) (mark# s X -> active# s mark X, active# plus(N, 0()) -> mark# N) (mark# s X -> active# s mark X, active# plus(N, s M) -> U11#(tt(), M, N)) (mark# s X -> active# s mark X, active# plus(N, s M) -> mark# U11(tt(), M, N)) (mark# s X -> active# s mark X, active# U11(tt(), M, N) -> U12#(tt(), M, N)) (mark# s X -> active# s mark X, active# U11(tt(), M, N) -> mark# U12(tt(), M, N)) (mark# s X -> active# s mark X, active# U12(tt(), M, N) -> plus#(N, M)) (mark# s X -> active# s mark X, active# U12(tt(), M, N) -> s# plus(N, M)) (mark# s X -> active# s mark X, active# U12(tt(), M, N) -> mark# s plus(N, M)) (active# U11(tt(), M, N) -> U12#(tt(), M, N), U12#(X1, active X2, X3) -> U12#(X1, X2, X3)) (active# U11(tt(), M, N) -> U12#(tt(), M, N), U12#(X1, mark X2, X3) -> U12#(X1, X2, X3)) (active# U11(tt(), M, N) -> U12#(tt(), M, N), U12#(X1, X2, active X3) -> U12#(X1, X2, X3)) (active# U11(tt(), M, N) -> U12#(tt(), M, N), U12#(X1, X2, mark X3) -> U12#(X1, X2, X3)) (active# U21(tt(), M, N) -> U22#(tt(), M, N), U22#(X1, active X2, X3) -> U22#(X1, X2, X3)) (active# U21(tt(), M, N) -> U22#(tt(), M, N), U22#(X1, mark X2, X3) -> U22#(X1, X2, X3)) (active# U21(tt(), M, N) -> U22#(tt(), M, N), U22#(X1, X2, active X3) -> U22#(X1, X2, X3)) (active# U21(tt(), M, N) -> U22#(tt(), M, N), U22#(X1, X2, mark X3) -> U22#(X1, X2, X3)) (mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3), active# x(N, 0()) -> mark# 0()) (mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3), active# x(N, s M) -> U21#(tt(), M, N)) (mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3), active# x(N, s M) -> mark# U21(tt(), M, N)) (mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3), active# U21(tt(), M, N) -> U22#(tt(), M, N)) (mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3), active# U21(tt(), M, N) -> mark# U22(tt(), M, N)) (mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3), active# U22(tt(), M, N) -> x#(N, M)) (mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3), active# U22(tt(), M, N) -> plus#(x(N, M), N)) (mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3), active# U22(tt(), M, N) -> mark# plus(x(N, M), N)) (mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3), active# plus(N, 0()) -> mark# N) (mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3), active# plus(N, s M) -> U11#(tt(), M, N)) (mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3), active# plus(N, s M) -> mark# U11(tt(), M, N)) (mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3), active# U11(tt(), M, N) -> U12#(tt(), M, N)) (mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3), active# U11(tt(), M, N) -> mark# U12(tt(), M, N)) (mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3), active# U12(tt(), M, N) -> plus#(N, M)) (mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3), active# U12(tt(), M, N) -> s# plus(N, M)) (mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3), active# U12(tt(), M, N) -> mark# s plus(N, M)) (mark# U22(X1, X2, X3) -> active# U22(mark X1, X2, X3), active# x(N, 0()) -> mark# 0()) (mark# U22(X1, X2, X3) -> active# U22(mark X1, X2, X3), active# x(N, s M) -> U21#(tt(), M, N)) (mark# U22(X1, X2, X3) -> active# U22(mark X1, X2, X3), active# x(N, s M) -> mark# U21(tt(), M, N)) (mark# U22(X1, X2, X3) -> active# U22(mark X1, X2, X3), active# U21(tt(), M, N) -> U22#(tt(), M, N)) (mark# U22(X1, X2, X3) -> active# U22(mark X1, X2, X3), active# U21(tt(), M, N) -> mark# U22(tt(), M, N)) (mark# U22(X1, X2, X3) -> active# U22(mark X1, X2, X3), active# U22(tt(), M, N) -> x#(N, M)) (mark# U22(X1, X2, X3) -> active# U22(mark X1, X2, X3), active# U22(tt(), M, N) -> plus#(x(N, M), N)) (mark# U22(X1, X2, X3) -> active# U22(mark X1, X2, X3), active# U22(tt(), M, N) -> mark# plus(x(N, M), N)) (mark# U22(X1, X2, X3) -> active# U22(mark X1, X2, X3), active# plus(N, 0()) -> mark# N) (mark# U22(X1, X2, X3) -> active# U22(mark X1, X2, X3), active# plus(N, s M) -> U11#(tt(), M, N)) (mark# U22(X1, X2, X3) -> active# U22(mark X1, X2, X3), active# plus(N, s M) -> mark# U11(tt(), M, N)) (mark# U22(X1, X2, X3) -> active# U22(mark X1, X2, X3), active# U11(tt(), M, N) -> U12#(tt(), M, N)) (mark# U22(X1, X2, X3) -> active# U22(mark X1, X2, X3), active# U11(tt(), M, N) -> mark# U12(tt(), M, N)) (mark# U22(X1, X2, X3) -> active# U22(mark X1, X2, X3), active# U12(tt(), M, N) -> plus#(N, M)) (mark# U22(X1, X2, X3) -> active# U22(mark X1, X2, X3), active# U12(tt(), M, N) -> s# plus(N, M)) (mark# U22(X1, X2, X3) -> active# U22(mark X1, X2, X3), active# U12(tt(), M, N) -> mark# s plus(N, M)) (active# U11(tt(), M, N) -> mark# U12(tt(), M, N), mark# x(X1, X2) -> x#(mark X1, mark X2)) (active# U11(tt(), M, N) -> mark# U12(tt(), M, N), mark# x(X1, X2) -> active# x(mark X1, mark X2)) (active# U11(tt(), M, N) -> mark# U12(tt(), M, N), mark# x(X1, X2) -> mark# X2) (active# U11(tt(), M, N) -> mark# U12(tt(), M, N), mark# x(X1, X2) -> mark# X1) (active# U11(tt(), M, N) -> mark# U12(tt(), M, N), mark# U21(X1, X2, X3) -> U21#(mark X1, X2, X3)) (active# U11(tt(), M, N) -> mark# U12(tt(), M, N), mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3)) (active# U11(tt(), M, N) -> mark# U12(tt(), M, N), mark# U21(X1, X2, X3) -> mark# X1) (active# U11(tt(), M, N) -> mark# U12(tt(), M, N), mark# U22(X1, X2, X3) -> U22#(mark X1, X2, X3)) (active# U11(tt(), M, N) -> mark# U12(tt(), M, N), mark# U22(X1, X2, X3) -> active# U22(mark X1, X2, X3)) (active# U11(tt(), M, N) -> mark# U12(tt(), M, N), mark# U22(X1, X2, X3) -> mark# X1) (active# U11(tt(), M, N) -> mark# U12(tt(), M, N), mark# plus(X1, X2) -> plus#(mark X1, mark X2)) (active# U11(tt(), M, N) -> mark# U12(tt(), M, N), mark# plus(X1, X2) -> active# plus(mark X1, mark X2)) (active# U11(tt(), M, N) -> mark# U12(tt(), M, N), mark# plus(X1, X2) -> mark# X2) (active# U11(tt(), M, N) -> mark# U12(tt(), M, N), mark# plus(X1, X2) -> mark# X1) (active# U11(tt(), M, N) -> mark# U12(tt(), M, N), mark# s X -> s# mark X) (active# U11(tt(), M, N) -> mark# U12(tt(), M, N), mark# s X -> active# s mark X) (active# U11(tt(), M, N) -> mark# U12(tt(), M, N), mark# s X -> mark# X) (active# U11(tt(), M, N) -> mark# U12(tt(), M, N), mark# U11(X1, X2, X3) -> U11#(mark X1, X2, X3)) (active# U11(tt(), M, N) -> mark# U12(tt(), M, N), mark# U11(X1, X2, X3) -> active# U11(mark X1, X2, X3)) (active# U11(tt(), M, N) -> mark# U12(tt(), M, N), mark# U11(X1, X2, X3) -> mark# X1) (active# U11(tt(), M, N) -> mark# U12(tt(), M, N), mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3)) (active# U11(tt(), M, N) -> mark# U12(tt(), M, N), mark# U12(X1, X2, X3) -> U12#(mark X1, X2, X3)) (active# U11(tt(), M, N) -> mark# U12(tt(), M, N), mark# U12(X1, X2, X3) -> mark# X1) (active# U21(tt(), M, N) -> mark# U22(tt(), M, N), mark# x(X1, X2) -> x#(mark X1, mark X2)) (active# U21(tt(), M, N) -> mark# U22(tt(), M, N), mark# x(X1, X2) -> active# x(mark X1, mark X2)) (active# U21(tt(), M, N) -> mark# U22(tt(), M, N), mark# x(X1, X2) -> mark# X2) (active# U21(tt(), M, N) -> mark# U22(tt(), M, N), mark# x(X1, X2) -> mark# X1) (active# U21(tt(), M, N) -> mark# U22(tt(), M, N), mark# U21(X1, X2, X3) -> U21#(mark X1, X2, X3)) (active# U21(tt(), M, N) -> mark# U22(tt(), M, N), mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3)) (active# U21(tt(), M, N) -> mark# U22(tt(), M, N), mark# U21(X1, X2, X3) -> mark# X1) (active# U21(tt(), M, N) -> mark# U22(tt(), M, N), mark# U22(X1, X2, X3) -> U22#(mark X1, X2, X3)) (active# U21(tt(), M, N) -> mark# U22(tt(), M, N), mark# U22(X1, X2, X3) -> active# U22(mark X1, X2, X3)) (active# U21(tt(), M, N) -> mark# U22(tt(), M, N), mark# U22(X1, X2, X3) -> mark# X1) (active# U21(tt(), M, N) -> mark# U22(tt(), M, N), mark# plus(X1, X2) -> plus#(mark X1, mark X2)) (active# U21(tt(), M, N) -> mark# U22(tt(), M, N), mark# plus(X1, X2) -> active# plus(mark X1, mark X2)) (active# U21(tt(), M, N) -> mark# U22(tt(), M, N), mark# plus(X1, X2) -> mark# X2) (active# U21(tt(), M, N) -> mark# U22(tt(), M, N), mark# plus(X1, X2) -> mark# X1) (active# U21(tt(), M, N) -> mark# U22(tt(), M, N), mark# s X -> s# mark X) (active# U21(tt(), M, N) -> mark# U22(tt(), M, N), mark# s X -> active# s mark X) (active# U21(tt(), M, N) -> mark# U22(tt(), M, N), mark# s X -> mark# X) (active# U21(tt(), M, N) -> mark# U22(tt(), M, N), mark# U11(X1, X2, X3) -> U11#(mark X1, X2, X3)) (active# U21(tt(), M, N) -> mark# U22(tt(), M, N), mark# U11(X1, X2, X3) -> active# U11(mark X1, X2, X3)) (active# U21(tt(), M, N) -> mark# U22(tt(), M, N), mark# U11(X1, X2, X3) -> mark# X1) (active# U21(tt(), M, N) -> mark# U22(tt(), M, N), mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3)) (active# U21(tt(), M, N) -> mark# U22(tt(), M, N), mark# U12(X1, X2, X3) -> U12#(mark X1, X2, X3)) (active# U21(tt(), M, N) -> mark# U22(tt(), M, N), mark# U12(X1, X2, X3) -> mark# X1) (active# plus(N, 0()) -> mark# N, mark# 0() -> active# 0()) (active# plus(N, 0()) -> mark# N, mark# x(X1, X2) -> x#(mark X1, mark X2)) (active# plus(N, 0()) -> mark# N, mark# x(X1, X2) -> active# x(mark X1, mark X2)) (active# plus(N, 0()) -> mark# N, mark# x(X1, X2) -> mark# X2) (active# plus(N, 0()) -> mark# N, mark# x(X1, X2) -> mark# X1) (active# plus(N, 0()) -> mark# N, mark# U21(X1, X2, X3) -> U21#(mark X1, X2, X3)) (active# plus(N, 0()) -> mark# N, mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3)) (active# plus(N, 0()) -> mark# N, mark# U21(X1, X2, X3) -> mark# X1) (active# plus(N, 0()) -> mark# N, mark# U22(X1, X2, X3) -> U22#(mark X1, X2, X3)) (active# plus(N, 0()) -> mark# N, mark# U22(X1, X2, X3) -> active# U22(mark X1, X2, X3)) (active# plus(N, 0()) -> mark# N, mark# U22(X1, X2, X3) -> mark# X1) (active# plus(N, 0()) -> mark# N, mark# plus(X1, X2) -> plus#(mark X1, mark X2)) (active# plus(N, 0()) -> mark# N, mark# plus(X1, X2) -> active# plus(mark X1, mark X2)) (active# plus(N, 0()) -> mark# N, mark# plus(X1, X2) -> mark# X2) (active# plus(N, 0()) -> mark# N, mark# plus(X1, X2) -> mark# X1) (active# plus(N, 0()) -> mark# N, mark# s X -> s# mark X) (active# plus(N, 0()) -> mark# N, mark# s X -> active# s mark X) (active# plus(N, 0()) -> mark# N, mark# s X -> mark# X) (active# plus(N, 0()) -> mark# N, mark# U11(X1, X2, X3) -> U11#(mark X1, X2, X3)) (active# plus(N, 0()) -> mark# N, mark# U11(X1, X2, X3) -> active# U11(mark X1, X2, X3)) (active# plus(N, 0()) -> mark# N, mark# U11(X1, X2, X3) -> mark# X1) (active# plus(N, 0()) -> mark# N, mark# tt() -> active# tt()) (active# plus(N, 0()) -> mark# N, mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3)) (active# plus(N, 0()) -> mark# N, mark# U12(X1, X2, X3) -> U12#(mark X1, X2, X3)) (active# plus(N, 0()) -> mark# N, mark# U12(X1, X2, X3) -> mark# X1) (mark# U12(X1, X2, X3) -> mark# X1, mark# 0() -> active# 0()) (mark# U12(X1, X2, X3) -> mark# X1, mark# x(X1, X2) -> x#(mark X1, mark X2)) (mark# U12(X1, X2, X3) -> mark# X1, mark# x(X1, X2) -> active# 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# U21(X1, X2, X3) -> U21#(mark X1, X2, X3)) (mark# U12(X1, X2, X3) -> mark# X1, mark# U21(X1, X2, X3) -> active# 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# U22(X1, X2, X3) -> U22#(mark X1, X2, X3)) (mark# U12(X1, X2, X3) -> mark# X1, mark# U22(X1, X2, X3) -> active# 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# plus(X1, X2) -> plus#(mark X1, mark X2)) (mark# U12(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> active# plus(mark X1, mark X2)) (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# s X -> s# mark X) (mark# U12(X1, X2, X3) -> mark# X1, mark# s X -> active# s mark X) (mark# U12(X1, X2, X3) -> mark# X1, mark# s X -> mark# X) (mark# U12(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> U11#(mark X1, X2, X3)) (mark# U12(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> active# U11(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# tt() -> active# tt()) (mark# U12(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3)) (mark# U12(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> U12#(mark X1, X2, X3)) (mark# U12(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# 0() -> active# 0()) (mark# plus(X1, X2) -> mark# X1, mark# x(X1, X2) -> x#(mark X1, mark X2)) (mark# plus(X1, X2) -> mark# X1, mark# x(X1, X2) -> active# x(mark X1, mark X2)) (mark# plus(X1, X2) -> mark# X1, mark# x(X1, X2) -> mark# X2) (mark# plus(X1, X2) -> mark# X1, mark# x(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# U21(X1, X2, X3) -> U21#(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X1, mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X1, mark# U21(X1, X2, X3) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# U22(X1, X2, X3) -> U22#(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X1, mark# U22(X1, X2, X3) -> active# U22(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X1, mark# U22(X1, X2, X3) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# plus(X1, X2) -> plus#(mark X1, mark X2)) (mark# plus(X1, X2) -> mark# X1, mark# plus(X1, X2) -> active# plus(mark X1, mark X2)) (mark# plus(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# plus(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# s X -> s# mark X) (mark# plus(X1, X2) -> mark# X1, mark# s X -> active# s mark X) (mark# plus(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# plus(X1, X2) -> mark# X1, mark# U11(X1, X2, X3) -> U11#(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X1, mark# U11(X1, X2, X3) -> active# 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# tt() -> active# tt()) (mark# plus(X1, X2) -> mark# X1, mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X1, mark# U12(X1, X2, X3) -> U12#(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X1, mark# U12(X1, X2, X3) -> mark# X1) (mark# U21(X1, X2, X3) -> mark# X1, mark# 0() -> active# 0()) (mark# U21(X1, X2, X3) -> mark# X1, mark# x(X1, X2) -> x#(mark X1, mark X2)) (mark# U21(X1, X2, X3) -> mark# X1, mark# x(X1, X2) -> active# 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# U21(X1, X2, X3) -> U21#(mark X1, X2, X3)) (mark# U21(X1, X2, X3) -> mark# X1, mark# U21(X1, X2, X3) -> active# 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# U22(X1, X2, X3) -> U22#(mark X1, X2, X3)) (mark# U21(X1, X2, X3) -> mark# X1, mark# U22(X1, X2, X3) -> active# 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# plus(X1, X2) -> plus#(mark X1, mark X2)) (mark# U21(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> active# 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# s X -> s# mark X) (mark# U21(X1, X2, X3) -> mark# X1, mark# s X -> active# s mark X) (mark# U21(X1, X2, X3) -> mark# X1, mark# s X -> mark# X) (mark# U21(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> U11#(mark X1, X2, X3)) (mark# U21(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> active# U11(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# tt() -> active# tt()) (mark# U21(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3)) (mark# U21(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> U12#(mark X1, X2, X3)) (mark# U21(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> mark# X1) (mark# plus(X1, X2) -> mark# X2, mark# 0() -> active# 0()) (mark# plus(X1, X2) -> mark# X2, mark# x(X1, X2) -> x#(mark X1, mark X2)) (mark# plus(X1, X2) -> mark# X2, mark# x(X1, X2) -> active# 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# U21(X1, X2, X3) -> U21#(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X2, mark# U21(X1, X2, X3) -> active# 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# U22(X1, X2, X3) -> U22#(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X2, mark# U22(X1, X2, X3) -> active# 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# plus(X1, X2) -> plus#(mark X1, mark X2)) (mark# plus(X1, X2) -> mark# X2, mark# plus(X1, X2) -> active# plus(mark X1, mark X2)) (mark# plus(X1, X2) -> mark# X2, mark# plus(X1, X2) -> mark# X2) (mark# plus(X1, X2) -> mark# X2, mark# plus(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X2, mark# s X -> s# mark X) (mark# plus(X1, X2) -> mark# X2, mark# s X -> active# s mark X) (mark# plus(X1, X2) -> mark# X2, mark# s X -> mark# X) (mark# plus(X1, X2) -> mark# X2, mark# U11(X1, X2, X3) -> U11#(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X2, mark# U11(X1, X2, X3) -> active# U11(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X2, mark# U11(X1, X2, X3) -> mark# X1) (mark# plus(X1, X2) -> mark# X2, mark# tt() -> active# tt()) (mark# plus(X1, X2) -> mark# X2, mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X2, mark# U12(X1, X2, X3) -> U12#(mark X1, X2, X3)) (mark# plus(X1, X2) -> 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# X2, mark# U12(X1, X2, X3) -> U12#(mark X1, X2, X3)) (mark# x(X1, X2) -> mark# X2, mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3)) (mark# x(X1, X2) -> mark# X2, mark# tt() -> active# tt()) (mark# x(X1, X2) -> mark# X2, mark# U11(X1, X2, X3) -> mark# X1) (mark# x(X1, X2) -> mark# X2, mark# U11(X1, X2, X3) -> active# U11(mark X1, X2, X3)) (mark# x(X1, X2) -> mark# X2, mark# U11(X1, X2, X3) -> U11#(mark X1, X2, X3)) (mark# x(X1, X2) -> mark# X2, mark# s X -> mark# X) (mark# x(X1, X2) -> mark# X2, mark# s X -> active# s mark X) (mark# x(X1, X2) -> mark# X2, mark# s X -> s# mark X) (mark# x(X1, X2) -> mark# X2, mark# plus(X1, X2) -> mark# X1) (mark# x(X1, X2) -> mark# X2, mark# plus(X1, X2) -> mark# X2) (mark# x(X1, X2) -> mark# X2, mark# plus(X1, X2) -> active# plus(mark X1, mark X2)) (mark# x(X1, X2) -> mark# X2, mark# plus(X1, X2) -> plus#(mark X1, mark X2)) (mark# x(X1, X2) -> mark# X2, mark# U22(X1, X2, X3) -> mark# X1) (mark# x(X1, X2) -> mark# X2, mark# U22(X1, X2, X3) -> active# U22(mark X1, X2, X3)) (mark# x(X1, X2) -> mark# X2, mark# U22(X1, X2, X3) -> U22#(mark X1, X2, X3)) (mark# x(X1, X2) -> mark# X2, mark# U21(X1, X2, X3) -> mark# X1) (mark# x(X1, X2) -> mark# X2, mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3)) (mark# x(X1, X2) -> mark# X2, mark# U21(X1, X2, X3) -> U21#(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) -> active# x(mark X1, mark X2)) (mark# x(X1, X2) -> mark# X2, mark# x(X1, X2) -> x#(mark X1, mark X2)) (mark# x(X1, X2) -> mark# X2, mark# 0() -> active# 0()) (mark# x(X1, X2) -> mark# X1, mark# U12(X1, X2, X3) -> mark# X1) (mark# x(X1, X2) -> mark# X1, mark# U12(X1, X2, X3) -> U12#(mark X1, X2, X3)) (mark# x(X1, X2) -> mark# X1, mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3)) (mark# x(X1, X2) -> mark# X1, mark# tt() -> active# tt()) (mark# x(X1, X2) -> mark# X1, mark# U11(X1, X2, X3) -> mark# X1) (mark# x(X1, X2) -> mark# X1, mark# U11(X1, X2, X3) -> active# U11(mark X1, X2, X3)) (mark# x(X1, X2) -> mark# X1, mark# U11(X1, X2, X3) -> U11#(mark X1, X2, X3)) (mark# x(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# x(X1, X2) -> mark# X1, mark# s X -> active# s mark X) (mark# x(X1, X2) -> mark# X1, mark# s X -> s# mark X) (mark# x(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# x(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# x(X1, X2) -> mark# X1, mark# plus(X1, X2) -> active# plus(mark X1, mark X2)) (mark# x(X1, X2) -> mark# X1, mark# plus(X1, X2) -> plus#(mark X1, mark X2)) (mark# x(X1, X2) -> mark# X1, mark# U22(X1, X2, X3) -> mark# X1) (mark# x(X1, X2) -> mark# X1, mark# U22(X1, X2, X3) -> active# U22(mark X1, X2, X3)) (mark# x(X1, X2) -> mark# X1, mark# U22(X1, X2, X3) -> U22#(mark X1, X2, X3)) (mark# x(X1, X2) -> mark# X1, mark# U21(X1, X2, X3) -> mark# X1) (mark# x(X1, X2) -> mark# X1, mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3)) (mark# x(X1, X2) -> mark# X1, mark# U21(X1, X2, X3) -> U21#(mark X1, X2, X3)) (mark# x(X1, X2) -> mark# X1, mark# x(X1, X2) -> mark# X1) (mark# x(X1, X2) -> mark# X1, mark# x(X1, X2) -> mark# X2) (mark# x(X1, X2) -> mark# X1, mark# x(X1, X2) -> active# x(mark X1, mark X2)) (mark# x(X1, X2) -> mark# X1, mark# x(X1, X2) -> x#(mark X1, mark X2)) (mark# x(X1, X2) -> mark# X1, mark# 0() -> active# 0()) (mark# U22(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> mark# X1) (mark# U22(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> U12#(mark X1, X2, X3)) (mark# U22(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3)) (mark# U22(X1, X2, X3) -> mark# X1, mark# tt() -> active# tt()) (mark# U22(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> mark# X1) (mark# U22(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> active# U11(mark X1, X2, X3)) (mark# U22(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> U11#(mark X1, X2, X3)) (mark# U22(X1, X2, X3) -> mark# X1, mark# s X -> mark# X) (mark# U22(X1, X2, X3) -> mark# X1, mark# s X -> active# s mark X) (mark# U22(X1, X2, X3) -> mark# X1, mark# s X -> s# mark X) (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# plus(X1, X2) -> active# plus(mark X1, mark X2)) (mark# U22(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> plus#(mark X1, mark X2)) (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) -> active# U22(mark X1, X2, X3)) (mark# U22(X1, X2, X3) -> mark# X1, mark# U22(X1, X2, X3) -> U22#(mark X1, X2, X3)) (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) -> active# U21(mark X1, X2, X3)) (mark# U22(X1, X2, X3) -> mark# X1, mark# U21(X1, X2, X3) -> U21#(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) -> active# x(mark X1, mark X2)) (mark# U22(X1, X2, X3) -> mark# X1, mark# x(X1, X2) -> x#(mark X1, mark X2)) (mark# U22(X1, X2, X3) -> mark# X1, mark# 0() -> active# 0()) (mark# U11(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> mark# X1) (mark# U11(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> U12#(mark X1, X2, X3)) (mark# U11(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3)) (mark# U11(X1, X2, X3) -> mark# X1, mark# tt() -> active# tt()) (mark# U11(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> mark# X1) (mark# U11(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> active# U11(mark X1, X2, X3)) (mark# U11(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> U11#(mark X1, X2, X3)) (mark# U11(X1, X2, X3) -> mark# X1, mark# s X -> mark# X) (mark# U11(X1, X2, X3) -> mark# X1, mark# s X -> active# s mark X) (mark# U11(X1, X2, X3) -> mark# X1, mark# s X -> s# mark X) (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# plus(X1, X2) -> active# plus(mark X1, mark X2)) (mark# U11(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> plus#(mark X1, mark X2)) (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) -> active# U22(mark X1, X2, X3)) (mark# U11(X1, X2, X3) -> mark# X1, mark# U22(X1, X2, X3) -> U22#(mark X1, X2, X3)) (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) -> active# U21(mark X1, X2, X3)) (mark# U11(X1, X2, X3) -> mark# X1, mark# U21(X1, X2, X3) -> U21#(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) -> active# x(mark X1, mark X2)) (mark# U11(X1, X2, X3) -> mark# X1, mark# x(X1, X2) -> x#(mark X1, mark X2)) (mark# U11(X1, X2, X3) -> mark# X1, mark# 0() -> active# 0()) (active# U22(tt(), M, N) -> plus#(x(N, M), N), plus#(X1, mark X2) -> plus#(X1, X2)) (active# U22(tt(), M, N) -> plus#(x(N, M), N), plus#(X1, active X2) -> plus#(X1, X2)) (active# U22(tt(), M, N) -> plus#(x(N, M), N), plus#(mark X1, X2) -> plus#(X1, X2)) (active# U22(tt(), M, N) -> plus#(x(N, M), N), plus#(active X1, X2) -> plus#(X1, X2)) (active# x(N, s M) -> mark# U21(tt(), M, N), mark# U12(X1, X2, X3) -> mark# X1) (active# x(N, s M) -> mark# U21(tt(), M, N), mark# U12(X1, X2, X3) -> U12#(mark X1, X2, X3)) (active# x(N, s M) -> mark# U21(tt(), M, N), mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3)) (active# x(N, s M) -> mark# U21(tt(), M, N), mark# U11(X1, X2, X3) -> mark# X1) (active# x(N, s M) -> mark# U21(tt(), M, N), mark# U11(X1, X2, X3) -> active# U11(mark X1, X2, X3)) (active# x(N, s M) -> mark# U21(tt(), M, N), mark# U11(X1, X2, X3) -> U11#(mark X1, X2, X3)) (active# x(N, s M) -> mark# U21(tt(), M, N), mark# s X -> mark# X) (active# x(N, s M) -> mark# U21(tt(), M, N), mark# s X -> active# s mark X) (active# x(N, s M) -> mark# U21(tt(), M, N), mark# s X -> s# mark X) (active# x(N, s M) -> mark# U21(tt(), M, N), mark# plus(X1, X2) -> mark# X1) (active# x(N, s M) -> mark# U21(tt(), M, N), mark# plus(X1, X2) -> mark# X2) (active# x(N, s M) -> mark# U21(tt(), M, N), mark# plus(X1, X2) -> active# plus(mark X1, mark X2)) (active# x(N, s M) -> mark# U21(tt(), M, N), mark# plus(X1, X2) -> plus#(mark X1, mark X2)) (active# x(N, s M) -> mark# U21(tt(), M, N), mark# U22(X1, X2, X3) -> mark# X1) (active# x(N, s M) -> mark# U21(tt(), M, N), mark# U22(X1, X2, X3) -> active# U22(mark X1, X2, X3)) (active# x(N, s M) -> mark# U21(tt(), M, N), mark# U22(X1, X2, X3) -> U22#(mark X1, X2, X3)) (active# x(N, s M) -> mark# U21(tt(), M, N), mark# U21(X1, X2, X3) -> mark# X1) (active# x(N, s M) -> mark# U21(tt(), M, N), mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3)) (active# x(N, s M) -> mark# U21(tt(), M, N), mark# U21(X1, X2, X3) -> U21#(mark X1, X2, X3)) (active# x(N, s M) -> mark# U21(tt(), M, N), mark# x(X1, X2) -> mark# X1) (active# x(N, s M) -> mark# U21(tt(), M, N), mark# x(X1, X2) -> mark# X2) (active# x(N, s M) -> mark# U21(tt(), M, N), mark# x(X1, X2) -> active# x(mark X1, mark X2)) (active# x(N, s M) -> mark# U21(tt(), M, N), mark# x(X1, X2) -> x#(mark X1, mark X2)) (active# plus(N, s M) -> mark# U11(tt(), M, N), mark# U12(X1, X2, X3) -> mark# X1) (active# plus(N, s M) -> mark# U11(tt(), M, N), mark# U12(X1, X2, X3) -> U12#(mark X1, X2, X3)) (active# plus(N, s M) -> mark# U11(tt(), M, N), mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3)) (active# plus(N, s M) -> mark# U11(tt(), M, N), mark# U11(X1, X2, X3) -> mark# X1) (active# plus(N, s M) -> mark# U11(tt(), M, N), mark# U11(X1, X2, X3) -> active# U11(mark X1, X2, X3)) (active# plus(N, s M) -> mark# U11(tt(), M, N), mark# U11(X1, X2, X3) -> U11#(mark X1, X2, X3)) (active# plus(N, s M) -> mark# U11(tt(), M, N), mark# s X -> mark# X) (active# plus(N, s M) -> mark# U11(tt(), M, N), mark# s X -> active# s mark X) (active# plus(N, s M) -> mark# U11(tt(), M, N), mark# s X -> s# mark X) (active# plus(N, s M) -> mark# U11(tt(), M, N), mark# plus(X1, X2) -> mark# X1) (active# plus(N, s M) -> mark# U11(tt(), M, N), mark# plus(X1, X2) -> mark# X2) (active# plus(N, s M) -> mark# U11(tt(), M, N), mark# plus(X1, X2) -> active# plus(mark X1, mark X2)) (active# plus(N, s M) -> mark# U11(tt(), M, N), mark# plus(X1, X2) -> plus#(mark X1, mark X2)) (active# plus(N, s M) -> mark# U11(tt(), M, N), mark# U22(X1, X2, X3) -> mark# X1) (active# plus(N, s M) -> mark# U11(tt(), M, N), mark# U22(X1, X2, X3) -> active# U22(mark X1, X2, X3)) (active# plus(N, s M) -> mark# U11(tt(), M, N), mark# U22(X1, X2, X3) -> U22#(mark X1, X2, X3)) (active# plus(N, s M) -> mark# U11(tt(), M, N), mark# U21(X1, X2, X3) -> mark# X1) (active# plus(N, s M) -> mark# U11(tt(), M, N), mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3)) (active# plus(N, s M) -> mark# U11(tt(), M, N), mark# U21(X1, X2, X3) -> U21#(mark X1, X2, X3)) (active# plus(N, s M) -> mark# U11(tt(), M, N), mark# x(X1, X2) -> mark# X1) (active# plus(N, s M) -> mark# U11(tt(), M, N), mark# x(X1, X2) -> mark# X2) (active# plus(N, s M) -> mark# U11(tt(), M, N), mark# x(X1, X2) -> active# x(mark X1, mark X2)) (active# plus(N, s M) -> mark# U11(tt(), M, N), mark# x(X1, X2) -> x#(mark X1, mark X2)) (mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3), active# U12(tt(), M, N) -> mark# s plus(N, M)) (mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3), active# U12(tt(), M, N) -> s# plus(N, M)) (mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3), active# U12(tt(), M, N) -> plus#(N, M)) (mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3), active# U11(tt(), M, N) -> mark# U12(tt(), M, N)) (mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3), active# U11(tt(), M, N) -> U12#(tt(), M, N)) (mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3), active# plus(N, s M) -> mark# U11(tt(), M, N)) (mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3), active# plus(N, s M) -> U11#(tt(), M, N)) (mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3), active# plus(N, 0()) -> mark# N) (mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3), active# U22(tt(), M, N) -> mark# plus(x(N, M), N)) (mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3), active# U22(tt(), M, N) -> plus#(x(N, M), N)) (mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3), active# U22(tt(), M, N) -> x#(N, M)) (mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3), active# U21(tt(), M, N) -> mark# U22(tt(), M, N)) (mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3), active# U21(tt(), M, N) -> U22#(tt(), M, N)) (mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3), active# x(N, s M) -> mark# U21(tt(), M, N)) (mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3), active# x(N, s M) -> U21#(tt(), M, N)) (mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3), active# x(N, 0()) -> mark# 0()) (mark# U11(X1, X2, X3) -> active# U11(mark X1, X2, X3), active# U12(tt(), M, N) -> mark# s plus(N, M)) (mark# U11(X1, X2, X3) -> active# U11(mark X1, X2, X3), active# U12(tt(), M, N) -> s# plus(N, M)) (mark# U11(X1, X2, X3) -> active# U11(mark X1, X2, X3), active# U12(tt(), M, N) -> plus#(N, M)) (mark# U11(X1, X2, X3) -> active# U11(mark X1, X2, X3), active# U11(tt(), M, N) -> mark# U12(tt(), M, N)) (mark# U11(X1, X2, X3) -> active# U11(mark X1, X2, X3), active# U11(tt(), M, N) -> U12#(tt(), M, N)) (mark# U11(X1, X2, X3) -> active# U11(mark X1, X2, X3), active# plus(N, s M) -> mark# U11(tt(), M, N)) (mark# U11(X1, X2, X3) -> active# U11(mark X1, X2, X3), active# plus(N, s M) -> U11#(tt(), M, N)) (mark# U11(X1, X2, X3) -> active# U11(mark X1, X2, X3), active# plus(N, 0()) -> mark# N) (mark# U11(X1, X2, X3) -> active# U11(mark X1, X2, X3), active# U22(tt(), M, N) -> mark# plus(x(N, M), N)) (mark# U11(X1, X2, X3) -> active# U11(mark X1, X2, X3), active# U22(tt(), M, N) -> plus#(x(N, M), N)) (mark# U11(X1, X2, X3) -> active# U11(mark X1, X2, X3), active# U22(tt(), M, N) -> x#(N, M)) (mark# U11(X1, X2, X3) -> active# U11(mark X1, X2, X3), active# U21(tt(), M, N) -> mark# U22(tt(), M, N)) (mark# U11(X1, X2, X3) -> active# U11(mark X1, X2, X3), active# U21(tt(), M, N) -> U22#(tt(), M, N)) (mark# U11(X1, X2, X3) -> active# U11(mark X1, X2, X3), active# x(N, s M) -> mark# U21(tt(), M, N)) (mark# U11(X1, X2, X3) -> active# U11(mark X1, X2, X3), active# x(N, s M) -> U21#(tt(), M, N)) (mark# U11(X1, X2, X3) -> active# U11(mark X1, X2, X3), active# x(N, 0()) -> mark# 0()) (active# x(N, s M) -> U21#(tt(), M, N), U21#(X1, X2, mark X3) -> U21#(X1, X2, X3)) (active# x(N, s M) -> U21#(tt(), M, N), U21#(X1, X2, active X3) -> U21#(X1, X2, X3)) (active# x(N, s M) -> U21#(tt(), M, N), U21#(X1, mark X2, X3) -> U21#(X1, X2, X3)) (active# x(N, s M) -> U21#(tt(), M, N), U21#(X1, active X2, X3) -> U21#(X1, X2, X3)) (active# plus(N, s M) -> U11#(tt(), M, N), U11#(X1, X2, mark X3) -> U11#(X1, X2, X3)) (active# plus(N, s M) -> U11#(tt(), M, N), U11#(X1, X2, active X3) -> U11#(X1, X2, X3)) (active# plus(N, s M) -> U11#(tt(), M, N), U11#(X1, mark X2, X3) -> U11#(X1, X2, X3)) (active# plus(N, s M) -> U11#(tt(), M, N), U11#(X1, active X2, X3) -> U11#(X1, X2, X3)) (active# U12(tt(), M, N) -> mark# s plus(N, M), mark# U12(X1, X2, X3) -> mark# X1) (active# U12(tt(), M, N) -> mark# s plus(N, M), mark# U12(X1, X2, X3) -> U12#(mark X1, X2, X3)) (active# U12(tt(), M, N) -> mark# s plus(N, M), mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3)) (active# U12(tt(), M, N) -> mark# s plus(N, M), mark# U11(X1, X2, X3) -> mark# X1) (active# U12(tt(), M, N) -> mark# s plus(N, M), mark# U11(X1, X2, X3) -> active# U11(mark X1, X2, X3)) (active# U12(tt(), M, N) -> mark# s plus(N, M), mark# U11(X1, X2, X3) -> U11#(mark X1, X2, X3)) (active# U12(tt(), M, N) -> mark# s plus(N, M), mark# s X -> mark# X) (active# U12(tt(), M, N) -> mark# s plus(N, M), mark# s X -> active# s mark X) (active# U12(tt(), M, N) -> mark# s plus(N, M), mark# s X -> s# mark X) (active# U12(tt(), M, N) -> mark# s plus(N, M), mark# plus(X1, X2) -> mark# X1) (active# U12(tt(), M, N) -> mark# s plus(N, M), mark# plus(X1, X2) -> mark# X2) (active# U12(tt(), M, N) -> mark# s plus(N, M), mark# plus(X1, X2) -> active# plus(mark X1, mark X2)) (active# U12(tt(), M, N) -> mark# s plus(N, M), mark# plus(X1, X2) -> plus#(mark X1, mark X2)) (active# U12(tt(), M, N) -> mark# s plus(N, M), mark# U22(X1, X2, X3) -> mark# X1) (active# U12(tt(), M, N) -> mark# s plus(N, M), mark# U22(X1, X2, X3) -> active# U22(mark X1, X2, X3)) (active# U12(tt(), M, N) -> mark# s plus(N, M), mark# U22(X1, X2, X3) -> U22#(mark X1, X2, X3)) (active# U12(tt(), M, N) -> mark# s plus(N, M), mark# U21(X1, X2, X3) -> mark# X1) (active# U12(tt(), M, N) -> mark# s plus(N, M), mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3)) (active# U12(tt(), M, N) -> mark# s plus(N, M), mark# U21(X1, X2, X3) -> U21#(mark X1, X2, X3)) (active# U12(tt(), M, N) -> mark# s plus(N, M), mark# x(X1, X2) -> mark# X1) (active# U12(tt(), M, N) -> mark# s plus(N, M), mark# x(X1, X2) -> mark# X2) (active# U12(tt(), M, N) -> mark# s plus(N, M), mark# x(X1, X2) -> active# x(mark X1, mark X2)) (active# U12(tt(), M, N) -> mark# s plus(N, M), mark# x(X1, X2) -> x#(mark X1, mark X2)) (mark# x(X1, X2) -> x#(mark X1, mark X2), x#(X1, mark X2) -> x#(X1, X2)) (mark# x(X1, X2) -> x#(mark X1, mark X2), x#(X1, active X2) -> x#(X1, X2)) (mark# x(X1, X2) -> x#(mark X1, mark X2), x#(mark X1, X2) -> x#(X1, X2)) (mark# x(X1, X2) -> x#(mark X1, mark X2), x#(active X1, X2) -> x#(X1, X2)) (active# U22(tt(), M, N) -> mark# plus(x(N, M), N), mark# U12(X1, X2, X3) -> mark# X1) (active# U22(tt(), M, N) -> mark# plus(x(N, M), N), mark# U12(X1, X2, X3) -> U12#(mark X1, X2, X3)) (active# U22(tt(), M, N) -> mark# plus(x(N, M), N), mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3)) (active# U22(tt(), M, N) -> mark# plus(x(N, M), N), mark# U11(X1, X2, X3) -> mark# X1) (active# U22(tt(), M, N) -> mark# plus(x(N, M), N), mark# U11(X1, X2, X3) -> active# U11(mark X1, X2, X3)) (active# U22(tt(), M, N) -> mark# plus(x(N, M), N), mark# U11(X1, X2, X3) -> U11#(mark X1, X2, X3)) (active# U22(tt(), M, N) -> mark# plus(x(N, M), N), mark# s X -> mark# X) (active# U22(tt(), M, N) -> mark# plus(x(N, M), N), mark# s X -> active# s mark X) (active# U22(tt(), M, N) -> mark# plus(x(N, M), N), mark# s X -> s# mark X) (active# U22(tt(), M, N) -> mark# plus(x(N, M), N), mark# plus(X1, X2) -> mark# X1) (active# U22(tt(), M, N) -> mark# plus(x(N, M), N), mark# plus(X1, X2) -> mark# X2) (active# U22(tt(), M, N) -> mark# plus(x(N, M), N), mark# plus(X1, X2) -> active# plus(mark X1, mark X2)) (active# U22(tt(), M, N) -> mark# plus(x(N, M), N), mark# plus(X1, X2) -> plus#(mark X1, mark X2)) (active# U22(tt(), M, N) -> mark# plus(x(N, M), N), mark# U22(X1, X2, X3) -> mark# X1) (active# U22(tt(), M, N) -> mark# plus(x(N, M), N), mark# U22(X1, X2, X3) -> active# U22(mark X1, X2, X3)) (active# U22(tt(), M, N) -> mark# plus(x(N, M), N), mark# U22(X1, X2, X3) -> U22#(mark X1, X2, X3)) (active# U22(tt(), M, N) -> mark# plus(x(N, M), N), mark# U21(X1, X2, X3) -> mark# X1) (active# U22(tt(), M, N) -> mark# plus(x(N, M), N), mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3)) (active# U22(tt(), M, N) -> mark# plus(x(N, M), N), mark# U21(X1, X2, X3) -> U21#(mark X1, X2, X3)) (active# U22(tt(), M, N) -> mark# plus(x(N, M), N), mark# x(X1, X2) -> mark# X1) (active# U22(tt(), M, N) -> mark# plus(x(N, M), N), mark# x(X1, X2) -> mark# X2) (active# U22(tt(), M, N) -> mark# plus(x(N, M), N), mark# x(X1, X2) -> active# x(mark X1, mark X2)) (active# U22(tt(), M, N) -> mark# plus(x(N, M), N), mark# x(X1, X2) -> x#(mark X1, mark X2)) (active# x(N, 0()) -> mark# 0(), mark# 0() -> active# 0()) (active# U12(tt(), M, N) -> plus#(N, M), plus#(X1, mark X2) -> plus#(X1, X2)) (active# U12(tt(), M, N) -> plus#(N, M), plus#(X1, active X2) -> plus#(X1, X2)) (active# U12(tt(), M, N) -> plus#(N, M), plus#(mark X1, X2) -> plus#(X1, X2)) (active# U12(tt(), M, N) -> plus#(N, M), plus#(active X1, X2) -> plus#(X1, X2)) (mark# x(X1, X2) -> active# x(mark X1, mark X2), active# U12(tt(), M, N) -> mark# s plus(N, M)) (mark# x(X1, X2) -> active# x(mark X1, mark X2), active# U12(tt(), M, N) -> s# plus(N, M)) (mark# x(X1, X2) -> active# x(mark X1, mark X2), active# U12(tt(), M, N) -> plus#(N, M)) (mark# x(X1, X2) -> active# x(mark X1, mark X2), active# U11(tt(), M, N) -> mark# U12(tt(), M, N)) (mark# x(X1, X2) -> active# x(mark X1, mark X2), active# U11(tt(), M, N) -> U12#(tt(), M, N)) (mark# x(X1, X2) -> active# x(mark X1, mark X2), active# plus(N, s M) -> mark# U11(tt(), M, N)) (mark# x(X1, X2) -> active# x(mark X1, mark X2), active# plus(N, s M) -> U11#(tt(), M, N)) (mark# x(X1, X2) -> active# x(mark X1, mark X2), active# plus(N, 0()) -> mark# N) (mark# x(X1, X2) -> active# x(mark X1, mark X2), active# U22(tt(), M, N) -> mark# plus(x(N, M), N)) (mark# x(X1, X2) -> active# x(mark X1, mark X2), active# U22(tt(), M, N) -> plus#(x(N, M), N)) (mark# x(X1, X2) -> active# x(mark X1, mark X2), active# U22(tt(), M, N) -> x#(N, M)) (mark# x(X1, X2) -> active# x(mark X1, mark X2), active# U21(tt(), M, N) -> mark# U22(tt(), M, N)) (mark# x(X1, X2) -> active# x(mark X1, mark X2), active# U21(tt(), M, N) -> U22#(tt(), M, N)) (mark# x(X1, X2) -> active# x(mark X1, mark X2), active# x(N, s M) -> mark# U21(tt(), M, N)) (mark# x(X1, X2) -> active# x(mark X1, mark X2), active# x(N, s M) -> U21#(tt(), M, N)) (mark# x(X1, X2) -> active# x(mark X1, mark X2), active# x(N, 0()) -> mark# 0()) (x#(active X1, X2) -> x#(X1, X2), x#(X1, mark X2) -> x#(X1, X2)) (x#(active X1, X2) -> x#(X1, X2), x#(X1, active X2) -> x#(X1, X2)) (x#(active X1, X2) -> x#(X1, X2), x#(mark X1, X2) -> x#(X1, X2)) (x#(active X1, X2) -> x#(X1, X2), x#(active X1, X2) -> x#(X1, X2)) (x#(X1, active X2) -> x#(X1, X2), x#(X1, mark X2) -> x#(X1, X2)) (x#(X1, active X2) -> x#(X1, X2), x#(X1, active X2) -> x#(X1, X2)) (x#(X1, active X2) -> x#(X1, X2), x#(mark X1, X2) -> x#(X1, X2)) (x#(X1, active X2) -> x#(X1, X2), x#(active X1, X2) -> x#(X1, X2)) (plus#(active X1, X2) -> plus#(X1, X2), plus#(X1, mark X2) -> plus#(X1, X2)) (plus#(active X1, X2) -> plus#(X1, X2), plus#(X1, active X2) -> plus#(X1, X2)) (plus#(active X1, X2) -> plus#(X1, X2), plus#(mark X1, X2) -> plus#(X1, X2)) (plus#(active X1, X2) -> plus#(X1, X2), plus#(active X1, X2) -> plus#(X1, X2)) (plus#(X1, active X2) -> plus#(X1, X2), plus#(X1, mark X2) -> plus#(X1, X2)) (plus#(X1, active X2) -> plus#(X1, X2), plus#(X1, active X2) -> plus#(X1, X2)) (plus#(X1, active X2) -> plus#(X1, X2), plus#(mark X1, X2) -> plus#(X1, X2)) (plus#(X1, active X2) -> plus#(X1, X2), plus#(active X1, X2) -> plus#(X1, X2)) (U21#(active X1, X2, X3) -> U21#(X1, X2, X3), U21#(X1, X2, mark X3) -> U21#(X1, X2, X3)) (U21#(active X1, X2, X3) -> U21#(X1, X2, X3), U21#(X1, X2, active X3) -> U21#(X1, X2, X3)) (U21#(active X1, X2, X3) -> U21#(X1, X2, X3), U21#(X1, mark X2, X3) -> U21#(X1, X2, X3)) (U21#(active X1, X2, X3) -> U21#(X1, X2, X3), U21#(X1, active X2, X3) -> U21#(X1, X2, X3)) (U21#(active X1, X2, X3) -> U21#(X1, X2, X3), U21#(mark X1, X2, X3) -> U21#(X1, X2, X3)) (U21#(active X1, X2, X3) -> U21#(X1, X2, X3), U21#(active X1, X2, X3) -> U21#(X1, X2, X3)) (U21#(X1, active X2, X3) -> U21#(X1, X2, X3), U21#(X1, X2, mark X3) -> U21#(X1, X2, X3)) (U21#(X1, active X2, X3) -> U21#(X1, X2, X3), U21#(X1, X2, active X3) -> U21#(X1, X2, X3)) (U21#(X1, active X2, X3) -> U21#(X1, X2, X3), U21#(X1, mark X2, X3) -> U21#(X1, X2, X3)) (U21#(X1, active X2, X3) -> U21#(X1, X2, X3), U21#(X1, active X2, X3) -> U21#(X1, X2, X3)) (U21#(X1, active X2, X3) -> U21#(X1, X2, X3), U21#(mark X1, X2, X3) -> U21#(X1, X2, X3)) (U21#(X1, active X2, X3) -> U21#(X1, X2, X3), U21#(active X1, X2, X3) -> U21#(X1, X2, X3)) (U21#(X1, X2, active X3) -> U21#(X1, X2, X3), U21#(X1, X2, mark X3) -> U21#(X1, X2, X3)) (U21#(X1, X2, active X3) -> U21#(X1, X2, X3), U21#(X1, X2, active X3) -> U21#(X1, X2, X3)) (U21#(X1, X2, active X3) -> U21#(X1, X2, X3), U21#(X1, mark X2, X3) -> U21#(X1, X2, X3)) (U21#(X1, X2, active X3) -> U21#(X1, X2, X3), U21#(X1, active X2, X3) -> U21#(X1, X2, X3)) (U21#(X1, X2, active X3) -> U21#(X1, X2, X3), U21#(mark X1, X2, X3) -> U21#(X1, X2, X3)) (U21#(X1, X2, active X3) -> U21#(X1, X2, X3), U21#(active X1, X2, X3) -> U21#(X1, X2, X3)) (U22#(active X1, X2, X3) -> U22#(X1, X2, X3), U22#(X1, X2, mark X3) -> U22#(X1, X2, X3)) (U22#(active X1, X2, X3) -> U22#(X1, X2, X3), U22#(X1, X2, active X3) -> U22#(X1, X2, X3)) (U22#(active X1, X2, X3) -> U22#(X1, X2, X3), U22#(X1, mark X2, X3) -> U22#(X1, X2, X3)) (U22#(active X1, X2, X3) -> U22#(X1, X2, X3), U22#(X1, active X2, X3) -> U22#(X1, X2, X3)) (U22#(active X1, X2, X3) -> U22#(X1, X2, X3), U22#(mark X1, X2, X3) -> U22#(X1, X2, X3)) (U22#(active X1, X2, X3) -> U22#(X1, X2, X3), U22#(active X1, X2, X3) -> U22#(X1, X2, X3)) (U22#(X1, active X2, X3) -> U22#(X1, X2, X3), U22#(X1, X2, mark X3) -> U22#(X1, X2, X3)) (U22#(X1, active X2, X3) -> U22#(X1, X2, X3), U22#(X1, X2, active X3) -> U22#(X1, X2, X3)) (U22#(X1, active X2, X3) -> U22#(X1, X2, X3), U22#(X1, mark X2, X3) -> U22#(X1, X2, X3)) (U22#(X1, active X2, X3) -> U22#(X1, X2, X3), U22#(X1, active X2, X3) -> U22#(X1, X2, X3)) (U22#(X1, active X2, X3) -> U22#(X1, X2, X3), U22#(mark X1, X2, X3) -> U22#(X1, X2, X3)) (U22#(X1, active X2, X3) -> U22#(X1, X2, X3), U22#(active X1, X2, X3) -> U22#(X1, X2, X3)) (U22#(X1, X2, active X3) -> U22#(X1, X2, X3), U22#(X1, X2, mark X3) -> U22#(X1, X2, X3)) (U22#(X1, X2, active X3) -> U22#(X1, X2, X3), U22#(X1, X2, active X3) -> U22#(X1, X2, X3)) (U22#(X1, X2, active X3) -> U22#(X1, X2, X3), U22#(X1, mark X2, X3) -> U22#(X1, X2, X3)) (U22#(X1, X2, active X3) -> U22#(X1, X2, X3), U22#(X1, active X2, X3) -> U22#(X1, X2, X3)) (U22#(X1, X2, active X3) -> U22#(X1, X2, X3), U22#(mark X1, X2, X3) -> U22#(X1, X2, X3)) (U22#(X1, X2, active X3) -> U22#(X1, X2, X3), U22#(active X1, X2, X3) -> U22#(X1, X2, X3)) (U11#(active X1, X2, X3) -> U11#(X1, X2, X3), U11#(X1, X2, mark X3) -> U11#(X1, X2, X3)) (U11#(active X1, X2, X3) -> U11#(X1, X2, X3), U11#(X1, X2, active X3) -> U11#(X1, X2, X3)) (U11#(active X1, X2, X3) -> U11#(X1, X2, X3), U11#(X1, mark X2, X3) -> U11#(X1, X2, X3)) (U11#(active X1, X2, X3) -> U11#(X1, X2, X3), U11#(X1, active X2, X3) -> U11#(X1, X2, X3)) (U11#(active X1, X2, X3) -> U11#(X1, X2, X3), U11#(mark X1, X2, X3) -> U11#(X1, X2, X3)) (U11#(active X1, X2, X3) -> U11#(X1, X2, X3), U11#(active X1, X2, X3) -> U11#(X1, X2, X3)) (U11#(X1, active X2, X3) -> U11#(X1, X2, X3), U11#(X1, X2, mark X3) -> U11#(X1, X2, X3)) (U11#(X1, active X2, X3) -> U11#(X1, X2, X3), U11#(X1, X2, active X3) -> U11#(X1, X2, X3)) (U11#(X1, active X2, X3) -> U11#(X1, X2, X3), U11#(X1, mark X2, X3) -> U11#(X1, X2, X3)) (U11#(X1, active X2, X3) -> U11#(X1, X2, X3), U11#(X1, active X2, X3) -> U11#(X1, X2, X3)) (U11#(X1, active X2, X3) -> U11#(X1, X2, X3), U11#(mark X1, X2, X3) -> U11#(X1, X2, X3)) (U11#(X1, active X2, X3) -> U11#(X1, X2, X3), U11#(active X1, X2, X3) -> U11#(X1, X2, X3)) (U11#(X1, X2, active X3) -> U11#(X1, X2, X3), U11#(X1, X2, mark X3) -> U11#(X1, X2, X3)) (U11#(X1, X2, active X3) -> U11#(X1, X2, X3), U11#(X1, X2, active X3) -> U11#(X1, X2, X3)) (U11#(X1, X2, active X3) -> U11#(X1, X2, X3), U11#(X1, mark X2, X3) -> U11#(X1, X2, X3)) (U11#(X1, X2, active X3) -> U11#(X1, X2, X3), U11#(X1, active X2, X3) -> U11#(X1, X2, X3)) (U11#(X1, X2, active X3) -> U11#(X1, X2, X3), U11#(mark X1, X2, X3) -> U11#(X1, X2, X3)) (U11#(X1, X2, active X3) -> U11#(X1, X2, X3), U11#(active X1, X2, X3) -> U11#(X1, X2, X3)) (U12#(active X1, X2, X3) -> U12#(X1, X2, X3), U12#(X1, X2, mark X3) -> U12#(X1, X2, X3)) (U12#(active X1, X2, X3) -> U12#(X1, X2, X3), U12#(X1, X2, active X3) -> U12#(X1, X2, X3)) (U12#(active X1, X2, X3) -> U12#(X1, X2, X3), U12#(X1, mark X2, X3) -> U12#(X1, X2, X3)) (U12#(active X1, X2, X3) -> U12#(X1, X2, X3), U12#(X1, active X2, X3) -> U12#(X1, X2, X3)) (U12#(active X1, X2, X3) -> U12#(X1, X2, X3), U12#(mark X1, X2, X3) -> U12#(X1, X2, X3)) (U12#(active X1, X2, X3) -> U12#(X1, X2, X3), U12#(active X1, X2, X3) -> U12#(X1, X2, X3)) (U12#(X1, active X2, X3) -> U12#(X1, X2, X3), U12#(X1, X2, mark X3) -> U12#(X1, X2, X3)) (U12#(X1, active X2, X3) -> U12#(X1, X2, X3), U12#(X1, X2, active X3) -> U12#(X1, X2, X3)) (U12#(X1, active X2, X3) -> U12#(X1, X2, X3), U12#(X1, mark X2, X3) -> U12#(X1, X2, X3)) (U12#(X1, active X2, X3) -> U12#(X1, X2, X3), U12#(X1, active X2, X3) -> U12#(X1, X2, X3)) (U12#(X1, active X2, X3) -> U12#(X1, X2, X3), U12#(mark X1, X2, X3) -> U12#(X1, X2, X3)) (U12#(X1, active X2, X3) -> U12#(X1, X2, X3), U12#(active X1, X2, X3) -> U12#(X1, X2, X3)) (U12#(X1, X2, active X3) -> U12#(X1, X2, X3), U12#(X1, X2, mark X3) -> U12#(X1, X2, X3)) (U12#(X1, X2, active X3) -> U12#(X1, X2, X3), U12#(X1, X2, active X3) -> U12#(X1, X2, X3)) (U12#(X1, X2, active X3) -> U12#(X1, X2, X3), U12#(X1, mark X2, X3) -> U12#(X1, X2, X3)) (U12#(X1, X2, active X3) -> U12#(X1, X2, X3), U12#(X1, active X2, X3) -> U12#(X1, X2, X3)) (U12#(X1, X2, active X3) -> U12#(X1, X2, X3), U12#(mark X1, X2, X3) -> U12#(X1, X2, X3)) (U12#(X1, X2, active X3) -> U12#(X1, X2, X3), U12#(active X1, X2, X3) -> U12#(X1, X2, X3)) (mark# U21(X1, X2, X3) -> U21#(mark X1, X2, X3), U21#(X1, X2, mark X3) -> U21#(X1, X2, X3)) (mark# U21(X1, X2, X3) -> U21#(mark X1, X2, X3), U21#(X1, X2, active X3) -> U21#(X1, X2, X3)) (mark# U21(X1, X2, X3) -> U21#(mark X1, X2, X3), U21#(X1, mark X2, X3) -> U21#(X1, X2, X3)) (mark# U21(X1, X2, X3) -> U21#(mark X1, X2, X3), U21#(X1, active X2, X3) -> U21#(X1, X2, X3)) (mark# U21(X1, X2, X3) -> U21#(mark X1, X2, X3), U21#(mark X1, X2, X3) -> U21#(X1, X2, X3)) (mark# U21(X1, X2, X3) -> U21#(mark X1, X2, X3), U21#(active X1, X2, X3) -> U21#(X1, X2, X3)) (mark# U11(X1, X2, X3) -> U11#(mark X1, X2, X3), U11#(X1, X2, mark X3) -> U11#(X1, X2, X3)) (mark# U11(X1, X2, X3) -> U11#(mark X1, X2, X3), U11#(X1, X2, active X3) -> U11#(X1, X2, X3)) (mark# U11(X1, X2, X3) -> U11#(mark X1, X2, X3), U11#(X1, mark X2, X3) -> U11#(X1, X2, X3)) (mark# U11(X1, X2, X3) -> U11#(mark X1, X2, X3), U11#(X1, active X2, X3) -> U11#(X1, X2, X3)) (mark# U11(X1, X2, X3) -> U11#(mark X1, X2, X3), U11#(mark X1, X2, X3) -> U11#(X1, X2, X3)) (mark# U11(X1, X2, X3) -> U11#(mark X1, X2, X3), U11#(active X1, X2, X3) -> U11#(X1, X2, X3)) (s# active X -> s# X, s# mark X -> s# X) (s# active X -> s# X, s# active X -> s# X) (mark# s X -> mark# X, mark# U12(X1, X2, X3) -> mark# X1) (mark# s X -> mark# X, mark# U12(X1, X2, X3) -> U12#(mark X1, X2, X3)) (mark# s X -> mark# X, mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3)) (mark# s X -> mark# X, mark# tt() -> active# tt()) (mark# s X -> mark# X, mark# U11(X1, X2, X3) -> mark# X1) (mark# s X -> mark# X, mark# U11(X1, X2, X3) -> active# U11(mark X1, X2, X3)) (mark# s X -> mark# X, mark# U11(X1, X2, X3) -> U11#(mark X1, X2, X3)) (mark# s X -> mark# X, mark# s X -> mark# X) (mark# s X -> mark# X, mark# s X -> active# s mark X) (mark# s X -> mark# X, mark# s X -> s# mark 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) -> active# plus(mark X1, mark X2)) (mark# s X -> mark# X, mark# plus(X1, X2) -> plus#(mark X1, mark X2)) (mark# s X -> mark# X, mark# U22(X1, X2, X3) -> mark# X1) (mark# s X -> mark# X, mark# U22(X1, X2, X3) -> active# U22(mark X1, X2, X3)) (mark# s X -> mark# X, mark# U22(X1, X2, X3) -> U22#(mark X1, X2, X3)) (mark# s X -> mark# X, mark# U21(X1, X2, X3) -> mark# X1) (mark# s X -> mark# X, mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3)) (mark# s X -> mark# X, mark# U21(X1, X2, X3) -> U21#(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) -> active# x(mark X1, mark X2)) (mark# s X -> mark# X, mark# x(X1, X2) -> x#(mark X1, mark X2)) (mark# s X -> mark# X, mark# 0() -> active# 0()) } EDG: { (s# mark X -> s# X, s# active X -> s# X) (s# mark X -> s# X, s# mark X -> s# X) (mark# U12(X1, X2, X3) -> U12#(mark X1, X2, X3), U12#(active X1, X2, X3) -> U12#(X1, X2, X3)) (mark# U12(X1, X2, X3) -> U12#(mark X1, X2, X3), U12#(mark X1, X2, X3) -> U12#(X1, X2, X3)) (mark# U12(X1, X2, X3) -> U12#(mark X1, X2, X3), U12#(X1, active X2, X3) -> U12#(X1, X2, X3)) (mark# U12(X1, X2, X3) -> U12#(mark X1, X2, X3), U12#(X1, mark X2, X3) -> U12#(X1, X2, X3)) (mark# U12(X1, X2, X3) -> U12#(mark X1, X2, X3), U12#(X1, X2, active X3) -> U12#(X1, X2, X3)) (mark# U12(X1, X2, X3) -> U12#(mark X1, X2, X3), U12#(X1, X2, mark X3) -> U12#(X1, X2, X3)) (mark# U22(X1, X2, X3) -> U22#(mark X1, X2, X3), U22#(active X1, X2, X3) -> U22#(X1, X2, X3)) (mark# U22(X1, X2, X3) -> U22#(mark X1, X2, X3), U22#(mark X1, X2, X3) -> U22#(X1, X2, X3)) (mark# U22(X1, X2, X3) -> U22#(mark X1, X2, X3), U22#(X1, active X2, X3) -> U22#(X1, X2, X3)) (mark# U22(X1, X2, X3) -> U22#(mark X1, X2, X3), U22#(X1, mark X2, X3) -> U22#(X1, X2, X3)) (mark# U22(X1, X2, X3) -> U22#(mark X1, X2, X3), U22#(X1, X2, active X3) -> U22#(X1, X2, X3)) (mark# U22(X1, X2, X3) -> U22#(mark X1, X2, X3), U22#(X1, X2, mark X3) -> U22#(X1, X2, X3)) (U12#(X1, X2, mark X3) -> U12#(X1, X2, X3), U12#(active X1, X2, X3) -> U12#(X1, X2, X3)) (U12#(X1, X2, mark X3) -> U12#(X1, X2, X3), U12#(mark X1, X2, X3) -> U12#(X1, X2, X3)) (U12#(X1, X2, mark X3) -> U12#(X1, X2, X3), U12#(X1, active X2, X3) -> U12#(X1, X2, X3)) (U12#(X1, X2, mark X3) -> U12#(X1, X2, X3), U12#(X1, mark X2, X3) -> U12#(X1, X2, X3)) (U12#(X1, X2, mark X3) -> U12#(X1, X2, X3), U12#(X1, X2, active X3) -> U12#(X1, X2, X3)) (U12#(X1, X2, mark X3) -> U12#(X1, X2, X3), U12#(X1, X2, mark X3) -> U12#(X1, X2, X3)) (U12#(X1, mark X2, X3) -> U12#(X1, X2, X3), U12#(active X1, X2, X3) -> U12#(X1, X2, X3)) (U12#(X1, mark X2, X3) -> U12#(X1, X2, X3), U12#(mark X1, X2, X3) -> U12#(X1, X2, X3)) (U12#(X1, mark X2, X3) -> U12#(X1, X2, X3), U12#(X1, active X2, X3) -> U12#(X1, X2, X3)) (U12#(X1, mark X2, X3) -> U12#(X1, X2, X3), U12#(X1, mark X2, X3) -> U12#(X1, X2, X3)) (U12#(X1, mark X2, X3) -> U12#(X1, X2, X3), U12#(X1, X2, active X3) -> U12#(X1, X2, X3)) (U12#(X1, mark X2, X3) -> U12#(X1, X2, X3), U12#(X1, X2, mark X3) -> U12#(X1, X2, X3)) (U12#(mark X1, X2, X3) -> U12#(X1, X2, X3), U12#(active X1, X2, X3) -> U12#(X1, X2, X3)) (U12#(mark X1, X2, X3) -> U12#(X1, X2, X3), U12#(mark X1, X2, X3) -> U12#(X1, X2, X3)) (U12#(mark X1, X2, X3) -> U12#(X1, X2, X3), U12#(X1, active X2, X3) -> U12#(X1, X2, X3)) (U12#(mark X1, X2, X3) -> U12#(X1, X2, X3), U12#(X1, mark X2, X3) -> U12#(X1, X2, X3)) (U12#(mark X1, X2, X3) -> U12#(X1, X2, X3), U12#(X1, X2, active X3) -> U12#(X1, X2, X3)) (U12#(mark X1, X2, X3) -> U12#(X1, X2, X3), U12#(X1, X2, mark X3) -> U12#(X1, X2, X3)) (U11#(X1, X2, mark X3) -> U11#(X1, X2, X3), U11#(active X1, X2, X3) -> U11#(X1, X2, X3)) (U11#(X1, X2, mark X3) -> U11#(X1, X2, X3), U11#(mark X1, X2, X3) -> U11#(X1, X2, X3)) (U11#(X1, X2, mark X3) -> U11#(X1, X2, X3), U11#(X1, active X2, X3) -> U11#(X1, X2, X3)) (U11#(X1, X2, mark X3) -> U11#(X1, X2, X3), U11#(X1, mark X2, X3) -> U11#(X1, X2, X3)) (U11#(X1, X2, mark X3) -> U11#(X1, X2, X3), U11#(X1, X2, active X3) -> U11#(X1, X2, X3)) (U11#(X1, X2, mark X3) -> U11#(X1, X2, X3), U11#(X1, X2, mark X3) -> U11#(X1, X2, X3)) (U11#(X1, mark X2, X3) -> U11#(X1, X2, X3), U11#(active X1, X2, X3) -> U11#(X1, X2, X3)) (U11#(X1, mark X2, X3) -> U11#(X1, X2, X3), U11#(mark X1, X2, X3) -> U11#(X1, X2, X3)) (U11#(X1, mark X2, X3) -> U11#(X1, X2, X3), U11#(X1, active X2, X3) -> U11#(X1, X2, X3)) (U11#(X1, mark X2, X3) -> U11#(X1, X2, X3), U11#(X1, mark X2, X3) -> U11#(X1, X2, X3)) (U11#(X1, mark X2, X3) -> U11#(X1, X2, X3), U11#(X1, X2, active X3) -> U11#(X1, X2, X3)) (U11#(X1, mark X2, X3) -> U11#(X1, X2, X3), U11#(X1, X2, mark X3) -> U11#(X1, X2, X3)) (U11#(mark X1, X2, X3) -> U11#(X1, X2, X3), U11#(active X1, X2, X3) -> U11#(X1, X2, X3)) (U11#(mark X1, X2, X3) -> U11#(X1, X2, X3), U11#(mark X1, X2, X3) -> U11#(X1, X2, X3)) (U11#(mark X1, X2, X3) -> U11#(X1, X2, X3), U11#(X1, active X2, X3) -> U11#(X1, X2, X3)) (U11#(mark X1, X2, X3) -> U11#(X1, X2, X3), U11#(X1, mark X2, X3) -> U11#(X1, X2, X3)) (U11#(mark X1, X2, X3) -> U11#(X1, X2, X3), U11#(X1, X2, active X3) -> U11#(X1, X2, X3)) (U11#(mark X1, X2, X3) -> U11#(X1, X2, X3), U11#(X1, X2, mark X3) -> U11#(X1, X2, X3)) (U22#(X1, X2, mark X3) -> U22#(X1, X2, X3), U22#(active X1, X2, X3) -> U22#(X1, X2, X3)) (U22#(X1, X2, mark X3) -> U22#(X1, X2, X3), U22#(mark X1, X2, X3) -> U22#(X1, X2, X3)) (U22#(X1, X2, mark X3) -> U22#(X1, X2, X3), U22#(X1, active X2, X3) -> U22#(X1, X2, X3)) (U22#(X1, X2, mark X3) -> U22#(X1, X2, X3), U22#(X1, mark X2, X3) -> U22#(X1, X2, X3)) (U22#(X1, X2, mark X3) -> U22#(X1, X2, X3), U22#(X1, X2, active X3) -> U22#(X1, X2, X3)) (U22#(X1, X2, mark X3) -> U22#(X1, X2, X3), U22#(X1, X2, mark X3) -> U22#(X1, X2, X3)) (U22#(X1, mark X2, X3) -> U22#(X1, X2, X3), U22#(active X1, X2, X3) -> U22#(X1, X2, X3)) (U22#(X1, mark X2, X3) -> U22#(X1, X2, X3), U22#(mark X1, X2, X3) -> U22#(X1, X2, X3)) (U22#(X1, mark X2, X3) -> U22#(X1, X2, X3), U22#(X1, active X2, X3) -> U22#(X1, X2, X3)) (U22#(X1, mark X2, X3) -> U22#(X1, X2, X3), U22#(X1, mark X2, X3) -> U22#(X1, X2, X3)) (U22#(X1, mark X2, X3) -> U22#(X1, X2, X3), U22#(X1, X2, active X3) -> U22#(X1, X2, X3)) (U22#(X1, mark X2, X3) -> U22#(X1, X2, X3), U22#(X1, X2, mark X3) -> U22#(X1, X2, X3)) (U22#(mark X1, X2, X3) -> U22#(X1, X2, X3), U22#(active X1, X2, X3) -> U22#(X1, X2, X3)) (U22#(mark X1, X2, X3) -> U22#(X1, X2, X3), U22#(mark X1, X2, X3) -> U22#(X1, X2, X3)) (U22#(mark X1, X2, X3) -> U22#(X1, X2, X3), U22#(X1, active X2, X3) -> U22#(X1, X2, X3)) (U22#(mark X1, X2, X3) -> U22#(X1, X2, X3), U22#(X1, mark X2, X3) -> U22#(X1, X2, X3)) (U22#(mark X1, X2, X3) -> U22#(X1, X2, X3), U22#(X1, X2, active X3) -> U22#(X1, X2, X3)) (U22#(mark X1, X2, X3) -> U22#(X1, X2, X3), U22#(X1, X2, mark X3) -> U22#(X1, X2, X3)) (U21#(X1, X2, mark X3) -> U21#(X1, X2, X3), U21#(active X1, X2, X3) -> U21#(X1, X2, X3)) (U21#(X1, X2, mark X3) -> U21#(X1, X2, X3), U21#(mark X1, X2, X3) -> U21#(X1, X2, X3)) (U21#(X1, X2, mark X3) -> U21#(X1, X2, X3), U21#(X1, active X2, X3) -> U21#(X1, X2, X3)) (U21#(X1, X2, mark X3) -> U21#(X1, X2, X3), U21#(X1, mark X2, X3) -> U21#(X1, X2, X3)) (U21#(X1, X2, mark X3) -> U21#(X1, X2, X3), U21#(X1, X2, active X3) -> U21#(X1, X2, X3)) (U21#(X1, X2, mark X3) -> U21#(X1, X2, X3), U21#(X1, X2, mark X3) -> U21#(X1, X2, X3)) (U21#(X1, mark X2, X3) -> U21#(X1, X2, X3), U21#(active X1, X2, X3) -> U21#(X1, X2, X3)) (U21#(X1, mark X2, X3) -> U21#(X1, X2, X3), U21#(mark X1, X2, X3) -> U21#(X1, X2, X3)) (U21#(X1, mark X2, X3) -> U21#(X1, X2, X3), U21#(X1, active X2, X3) -> U21#(X1, X2, X3)) (U21#(X1, mark X2, X3) -> U21#(X1, X2, X3), U21#(X1, mark X2, X3) -> U21#(X1, X2, X3)) (U21#(X1, mark X2, X3) -> U21#(X1, X2, X3), U21#(X1, X2, active X3) -> U21#(X1, X2, X3)) (U21#(X1, mark X2, X3) -> U21#(X1, X2, X3), U21#(X1, X2, mark X3) -> U21#(X1, X2, X3)) (U21#(mark X1, X2, X3) -> U21#(X1, X2, X3), U21#(active X1, X2, X3) -> U21#(X1, X2, X3)) (U21#(mark X1, X2, X3) -> U21#(X1, X2, X3), U21#(mark X1, X2, X3) -> U21#(X1, X2, X3)) (U21#(mark X1, X2, X3) -> U21#(X1, X2, X3), U21#(X1, active X2, X3) -> U21#(X1, X2, X3)) (U21#(mark X1, X2, X3) -> U21#(X1, X2, X3), U21#(X1, mark X2, X3) -> U21#(X1, X2, X3)) (U21#(mark X1, X2, X3) -> U21#(X1, X2, X3), U21#(X1, X2, active X3) -> U21#(X1, X2, X3)) (U21#(mark X1, X2, X3) -> U21#(X1, X2, X3), U21#(X1, X2, mark X3) -> U21#(X1, X2, X3)) (plus#(X1, mark X2) -> plus#(X1, X2), plus#(active X1, X2) -> plus#(X1, X2)) (plus#(X1, mark X2) -> plus#(X1, X2), plus#(mark X1, X2) -> plus#(X1, X2)) (plus#(X1, mark X2) -> plus#(X1, X2), plus#(X1, active X2) -> plus#(X1, X2)) (plus#(X1, mark X2) -> plus#(X1, X2), plus#(X1, mark X2) -> plus#(X1, X2)) (plus#(mark X1, X2) -> plus#(X1, X2), plus#(active X1, X2) -> plus#(X1, X2)) (plus#(mark X1, X2) -> plus#(X1, X2), plus#(mark X1, X2) -> plus#(X1, X2)) (plus#(mark X1, X2) -> plus#(X1, X2), plus#(X1, active X2) -> plus#(X1, X2)) (plus#(mark X1, X2) -> plus#(X1, X2), plus#(X1, mark X2) -> plus#(X1, X2)) (x#(X1, mark X2) -> x#(X1, X2), x#(active X1, X2) -> x#(X1, X2)) (x#(X1, mark X2) -> x#(X1, X2), x#(mark X1, X2) -> x#(X1, X2)) (x#(X1, mark X2) -> x#(X1, X2), x#(X1, active X2) -> x#(X1, X2)) (x#(X1, mark X2) -> x#(X1, X2), x#(X1, mark X2) -> x#(X1, X2)) (x#(mark X1, X2) -> x#(X1, X2), x#(active X1, X2) -> x#(X1, X2)) (x#(mark X1, X2) -> x#(X1, X2), x#(mark X1, X2) -> x#(X1, X2)) (x#(mark X1, X2) -> x#(X1, X2), x#(X1, active X2) -> x#(X1, X2)) (x#(mark X1, X2) -> x#(X1, X2), x#(X1, mark X2) -> x#(X1, X2)) (mark# plus(X1, X2) -> active# plus(mark X1, mark X2), active# plus(N, 0()) -> mark# N) (mark# plus(X1, X2) -> active# plus(mark X1, mark X2), active# plus(N, s M) -> U11#(tt(), M, N)) (mark# plus(X1, X2) -> active# plus(mark X1, mark X2), active# plus(N, s M) -> mark# U11(tt(), M, N)) (mark# s X -> s# mark X, s# active X -> s# X) (mark# s X -> s# mark X, s# mark X -> s# X) (active# U22(tt(), M, N) -> x#(N, M), x#(active X1, X2) -> x#(X1, X2)) (active# U22(tt(), M, N) -> x#(N, M), x#(mark X1, X2) -> x#(X1, X2)) (active# U22(tt(), M, N) -> x#(N, M), x#(X1, active X2) -> x#(X1, X2)) (active# U22(tt(), M, N) -> x#(N, M), x#(X1, mark X2) -> x#(X1, X2)) (mark# plus(X1, X2) -> plus#(mark X1, mark X2), plus#(active X1, X2) -> plus#(X1, X2)) (mark# plus(X1, X2) -> plus#(mark X1, mark X2), plus#(mark X1, X2) -> plus#(X1, X2)) (mark# plus(X1, X2) -> plus#(mark X1, mark X2), plus#(X1, active X2) -> plus#(X1, X2)) (mark# plus(X1, X2) -> plus#(mark X1, mark X2), plus#(X1, mark X2) -> plus#(X1, X2)) (active# U11(tt(), M, N) -> U12#(tt(), M, N), U12#(X1, active X2, X3) -> U12#(X1, X2, X3)) (active# U11(tt(), M, N) -> U12#(tt(), M, N), U12#(X1, mark X2, X3) -> U12#(X1, X2, X3)) (active# U11(tt(), M, N) -> U12#(tt(), M, N), U12#(X1, X2, active X3) -> U12#(X1, X2, X3)) (active# U11(tt(), M, N) -> U12#(tt(), M, N), U12#(X1, X2, mark X3) -> U12#(X1, X2, X3)) (active# U21(tt(), M, N) -> U22#(tt(), M, N), U22#(X1, active X2, X3) -> U22#(X1, X2, X3)) (active# U21(tt(), M, N) -> U22#(tt(), M, N), U22#(X1, mark X2, X3) -> U22#(X1, X2, X3)) (active# U21(tt(), M, N) -> U22#(tt(), M, N), U22#(X1, X2, active X3) -> U22#(X1, X2, X3)) (active# U21(tt(), M, N) -> U22#(tt(), M, N), U22#(X1, X2, mark X3) -> U22#(X1, X2, X3)) (mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3), active# U12(tt(), M, N) -> plus#(N, M)) (mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3), active# U12(tt(), M, N) -> s# plus(N, M)) (mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3), active# U12(tt(), M, N) -> mark# s plus(N, M)) (mark# U22(X1, X2, X3) -> active# U22(mark X1, X2, X3), active# U22(tt(), M, N) -> x#(N, M)) (mark# U22(X1, X2, X3) -> active# U22(mark X1, X2, X3), active# U22(tt(), M, N) -> plus#(x(N, M), N)) (mark# U22(X1, X2, X3) -> active# U22(mark X1, X2, X3), active# U22(tt(), M, N) -> mark# plus(x(N, M), N)) (active# U11(tt(), M, N) -> mark# U12(tt(), M, N), mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3)) (active# U11(tt(), M, N) -> mark# U12(tt(), M, N), mark# U12(X1, X2, X3) -> U12#(mark X1, X2, X3)) (active# U11(tt(), M, N) -> mark# U12(tt(), M, N), mark# U12(X1, X2, X3) -> mark# X1) (active# U21(tt(), M, N) -> mark# U22(tt(), M, N), mark# U22(X1, X2, X3) -> U22#(mark X1, X2, X3)) (active# U21(tt(), M, N) -> mark# U22(tt(), M, N), mark# U22(X1, X2, X3) -> active# U22(mark X1, X2, X3)) (active# U21(tt(), M, N) -> mark# U22(tt(), M, N), mark# U22(X1, X2, X3) -> mark# X1) (active# plus(N, 0()) -> mark# N, mark# 0() -> active# 0()) (active# plus(N, 0()) -> mark# N, mark# x(X1, X2) -> x#(mark X1, mark X2)) (active# plus(N, 0()) -> mark# N, mark# x(X1, X2) -> active# x(mark X1, mark X2)) (active# plus(N, 0()) -> mark# N, mark# x(X1, X2) -> mark# X2) (active# plus(N, 0()) -> mark# N, mark# x(X1, X2) -> mark# X1) (active# plus(N, 0()) -> mark# N, mark# U21(X1, X2, X3) -> U21#(mark X1, X2, X3)) (active# plus(N, 0()) -> mark# N, mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3)) (active# plus(N, 0()) -> mark# N, mark# U21(X1, X2, X3) -> mark# X1) (active# plus(N, 0()) -> mark# N, mark# U22(X1, X2, X3) -> U22#(mark X1, X2, X3)) (active# plus(N, 0()) -> mark# N, mark# U22(X1, X2, X3) -> active# U22(mark X1, X2, X3)) (active# plus(N, 0()) -> mark# N, mark# U22(X1, X2, X3) -> mark# X1) (active# plus(N, 0()) -> mark# N, mark# plus(X1, X2) -> plus#(mark X1, mark X2)) (active# plus(N, 0()) -> mark# N, mark# plus(X1, X2) -> active# plus(mark X1, mark X2)) (active# plus(N, 0()) -> mark# N, mark# plus(X1, X2) -> mark# X2) (active# plus(N, 0()) -> mark# N, mark# plus(X1, X2) -> mark# X1) (active# plus(N, 0()) -> mark# N, mark# s X -> s# mark X) (active# plus(N, 0()) -> mark# N, mark# s X -> active# s mark X) (active# plus(N, 0()) -> mark# N, mark# s X -> mark# X) (active# plus(N, 0()) -> mark# N, mark# U11(X1, X2, X3) -> U11#(mark X1, X2, X3)) (active# plus(N, 0()) -> mark# N, mark# U11(X1, X2, X3) -> active# U11(mark X1, X2, X3)) (active# plus(N, 0()) -> mark# N, mark# U11(X1, X2, X3) -> mark# X1) (active# plus(N, 0()) -> mark# N, mark# tt() -> active# tt()) (active# plus(N, 0()) -> mark# N, mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3)) (active# plus(N, 0()) -> mark# N, mark# U12(X1, X2, X3) -> U12#(mark X1, X2, X3)) (active# plus(N, 0()) -> mark# N, mark# U12(X1, X2, X3) -> mark# X1) (mark# U12(X1, X2, X3) -> mark# X1, mark# 0() -> active# 0()) (mark# U12(X1, X2, X3) -> mark# X1, mark# x(X1, X2) -> x#(mark X1, mark X2)) (mark# U12(X1, X2, X3) -> mark# X1, mark# x(X1, X2) -> active# 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# U21(X1, X2, X3) -> U21#(mark X1, X2, X3)) (mark# U12(X1, X2, X3) -> mark# X1, mark# U21(X1, X2, X3) -> active# 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# U22(X1, X2, X3) -> U22#(mark X1, X2, X3)) (mark# U12(X1, X2, X3) -> mark# X1, mark# U22(X1, X2, X3) -> active# 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# plus(X1, X2) -> plus#(mark X1, mark X2)) (mark# U12(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> active# plus(mark X1, mark X2)) (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# s X -> s# mark X) (mark# U12(X1, X2, X3) -> mark# X1, mark# s X -> active# s mark X) (mark# U12(X1, X2, X3) -> mark# X1, mark# s X -> mark# X) (mark# U12(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> U11#(mark X1, X2, X3)) (mark# U12(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> active# U11(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# tt() -> active# tt()) (mark# U12(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3)) (mark# U12(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> U12#(mark X1, X2, X3)) (mark# U12(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# 0() -> active# 0()) (mark# plus(X1, X2) -> mark# X1, mark# x(X1, X2) -> x#(mark X1, mark X2)) (mark# plus(X1, X2) -> mark# X1, mark# x(X1, X2) -> active# x(mark X1, mark X2)) (mark# plus(X1, X2) -> mark# X1, mark# x(X1, X2) -> mark# X2) (mark# plus(X1, X2) -> mark# X1, mark# x(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# U21(X1, X2, X3) -> U21#(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X1, mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X1, mark# U21(X1, X2, X3) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# U22(X1, X2, X3) -> U22#(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X1, mark# U22(X1, X2, X3) -> active# U22(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X1, mark# U22(X1, X2, X3) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# plus(X1, X2) -> plus#(mark X1, mark X2)) (mark# plus(X1, X2) -> mark# X1, mark# plus(X1, X2) -> active# plus(mark X1, mark X2)) (mark# plus(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# plus(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# s X -> s# mark X) (mark# plus(X1, X2) -> mark# X1, mark# s X -> active# s mark X) (mark# plus(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# plus(X1, X2) -> mark# X1, mark# U11(X1, X2, X3) -> U11#(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X1, mark# U11(X1, X2, X3) -> active# 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# tt() -> active# tt()) (mark# plus(X1, X2) -> mark# X1, mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X1, mark# U12(X1, X2, X3) -> U12#(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X1, mark# U12(X1, X2, X3) -> mark# X1) (mark# U21(X1, X2, X3) -> mark# X1, mark# 0() -> active# 0()) (mark# U21(X1, X2, X3) -> mark# X1, mark# x(X1, X2) -> x#(mark X1, mark X2)) (mark# U21(X1, X2, X3) -> mark# X1, mark# x(X1, X2) -> active# 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# U21(X1, X2, X3) -> U21#(mark X1, X2, X3)) (mark# U21(X1, X2, X3) -> mark# X1, mark# U21(X1, X2, X3) -> active# 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# U22(X1, X2, X3) -> U22#(mark X1, X2, X3)) (mark# U21(X1, X2, X3) -> mark# X1, mark# U22(X1, X2, X3) -> active# 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# plus(X1, X2) -> plus#(mark X1, mark X2)) (mark# U21(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> active# 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# s X -> s# mark X) (mark# U21(X1, X2, X3) -> mark# X1, mark# s X -> active# s mark X) (mark# U21(X1, X2, X3) -> mark# X1, mark# s X -> mark# X) (mark# U21(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> U11#(mark X1, X2, X3)) (mark# U21(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> active# U11(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# tt() -> active# tt()) (mark# U21(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3)) (mark# U21(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> U12#(mark X1, X2, X3)) (mark# U21(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> mark# X1) (mark# plus(X1, X2) -> mark# X2, mark# 0() -> active# 0()) (mark# plus(X1, X2) -> mark# X2, mark# x(X1, X2) -> x#(mark X1, mark X2)) (mark# plus(X1, X2) -> mark# X2, mark# x(X1, X2) -> active# 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# U21(X1, X2, X3) -> U21#(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X2, mark# U21(X1, X2, X3) -> active# 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# U22(X1, X2, X3) -> U22#(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X2, mark# U22(X1, X2, X3) -> active# 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# plus(X1, X2) -> plus#(mark X1, mark X2)) (mark# plus(X1, X2) -> mark# X2, mark# plus(X1, X2) -> active# plus(mark X1, mark X2)) (mark# plus(X1, X2) -> mark# X2, mark# plus(X1, X2) -> mark# X2) (mark# plus(X1, X2) -> mark# X2, mark# plus(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X2, mark# s X -> s# mark X) (mark# plus(X1, X2) -> mark# X2, mark# s X -> active# s mark X) (mark# plus(X1, X2) -> mark# X2, mark# s X -> mark# X) (mark# plus(X1, X2) -> mark# X2, mark# U11(X1, X2, X3) -> U11#(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X2, mark# U11(X1, X2, X3) -> active# U11(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X2, mark# U11(X1, X2, X3) -> mark# X1) (mark# plus(X1, X2) -> mark# X2, mark# tt() -> active# tt()) (mark# plus(X1, X2) -> mark# X2, mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X2, mark# U12(X1, X2, X3) -> U12#(mark X1, X2, X3)) (mark# plus(X1, X2) -> 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# X2, mark# U12(X1, X2, X3) -> U12#(mark X1, X2, X3)) (mark# x(X1, X2) -> mark# X2, mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3)) (mark# x(X1, X2) -> mark# X2, mark# tt() -> active# tt()) (mark# x(X1, X2) -> mark# X2, mark# U11(X1, X2, X3) -> mark# X1) (mark# x(X1, X2) -> mark# X2, mark# U11(X1, X2, X3) -> active# U11(mark X1, X2, X3)) (mark# x(X1, X2) -> mark# X2, mark# U11(X1, X2, X3) -> U11#(mark X1, X2, X3)) (mark# x(X1, X2) -> mark# X2, mark# s X -> mark# X) (mark# x(X1, X2) -> mark# X2, mark# s X -> active# s mark X) (mark# x(X1, X2) -> mark# X2, mark# s X -> s# mark X) (mark# x(X1, X2) -> mark# X2, mark# plus(X1, X2) -> mark# X1) (mark# x(X1, X2) -> mark# X2, mark# plus(X1, X2) -> mark# X2) (mark# x(X1, X2) -> mark# X2, mark# plus(X1, X2) -> active# plus(mark X1, mark X2)) (mark# x(X1, X2) -> mark# X2, mark# plus(X1, X2) -> plus#(mark X1, mark X2)) (mark# x(X1, X2) -> mark# X2, mark# U22(X1, X2, X3) -> mark# X1) (mark# x(X1, X2) -> mark# X2, mark# U22(X1, X2, X3) -> active# U22(mark X1, X2, X3)) (mark# x(X1, X2) -> mark# X2, mark# U22(X1, X2, X3) -> U22#(mark X1, X2, X3)) (mark# x(X1, X2) -> mark# X2, mark# U21(X1, X2, X3) -> mark# X1) (mark# x(X1, X2) -> mark# X2, mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3)) (mark# x(X1, X2) -> mark# X2, mark# U21(X1, X2, X3) -> U21#(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) -> active# x(mark X1, mark X2)) (mark# x(X1, X2) -> mark# X2, mark# x(X1, X2) -> x#(mark X1, mark X2)) (mark# x(X1, X2) -> mark# X2, mark# 0() -> active# 0()) (mark# x(X1, X2) -> mark# X1, mark# U12(X1, X2, X3) -> mark# X1) (mark# x(X1, X2) -> mark# X1, mark# U12(X1, X2, X3) -> U12#(mark X1, X2, X3)) (mark# x(X1, X2) -> mark# X1, mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3)) (mark# x(X1, X2) -> mark# X1, mark# tt() -> active# tt()) (mark# x(X1, X2) -> mark# X1, mark# U11(X1, X2, X3) -> mark# X1) (mark# x(X1, X2) -> mark# X1, mark# U11(X1, X2, X3) -> active# U11(mark X1, X2, X3)) (mark# x(X1, X2) -> mark# X1, mark# U11(X1, X2, X3) -> U11#(mark X1, X2, X3)) (mark# x(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# x(X1, X2) -> mark# X1, mark# s X -> active# s mark X) (mark# x(X1, X2) -> mark# X1, mark# s X -> s# mark X) (mark# x(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# x(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# x(X1, X2) -> mark# X1, mark# plus(X1, X2) -> active# plus(mark X1, mark X2)) (mark# x(X1, X2) -> mark# X1, mark# plus(X1, X2) -> plus#(mark X1, mark X2)) (mark# x(X1, X2) -> mark# X1, mark# U22(X1, X2, X3) -> mark# X1) (mark# x(X1, X2) -> mark# X1, mark# U22(X1, X2, X3) -> active# U22(mark X1, X2, X3)) (mark# x(X1, X2) -> mark# X1, mark# U22(X1, X2, X3) -> U22#(mark X1, X2, X3)) (mark# x(X1, X2) -> mark# X1, mark# U21(X1, X2, X3) -> mark# X1) (mark# x(X1, X2) -> mark# X1, mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3)) (mark# x(X1, X2) -> mark# X1, mark# U21(X1, X2, X3) -> U21#(mark X1, X2, X3)) (mark# x(X1, X2) -> mark# X1, mark# x(X1, X2) -> mark# X1) (mark# x(X1, X2) -> mark# X1, mark# x(X1, X2) -> mark# X2) (mark# x(X1, X2) -> mark# X1, mark# x(X1, X2) -> active# x(mark X1, mark X2)) (mark# x(X1, X2) -> mark# X1, mark# x(X1, X2) -> x#(mark X1, mark X2)) (mark# x(X1, X2) -> mark# X1, mark# 0() -> active# 0()) (mark# U22(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> mark# X1) (mark# U22(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> U12#(mark X1, X2, X3)) (mark# U22(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3)) (mark# U22(X1, X2, X3) -> mark# X1, mark# tt() -> active# tt()) (mark# U22(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> mark# X1) (mark# U22(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> active# U11(mark X1, X2, X3)) (mark# U22(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> U11#(mark X1, X2, X3)) (mark# U22(X1, X2, X3) -> mark# X1, mark# s X -> mark# X) (mark# U22(X1, X2, X3) -> mark# X1, mark# s X -> active# s mark X) (mark# U22(X1, X2, X3) -> mark# X1, mark# s X -> s# mark X) (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# plus(X1, X2) -> active# plus(mark X1, mark X2)) (mark# U22(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> plus#(mark X1, mark X2)) (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) -> active# U22(mark X1, X2, X3)) (mark# U22(X1, X2, X3) -> mark# X1, mark# U22(X1, X2, X3) -> U22#(mark X1, X2, X3)) (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) -> active# U21(mark X1, X2, X3)) (mark# U22(X1, X2, X3) -> mark# X1, mark# U21(X1, X2, X3) -> U21#(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) -> active# x(mark X1, mark X2)) (mark# U22(X1, X2, X3) -> mark# X1, mark# x(X1, X2) -> x#(mark X1, mark X2)) (mark# U22(X1, X2, X3) -> mark# X1, mark# 0() -> active# 0()) (mark# U11(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> mark# X1) (mark# U11(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> U12#(mark X1, X2, X3)) (mark# U11(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3)) (mark# U11(X1, X2, X3) -> mark# X1, mark# tt() -> active# tt()) (mark# U11(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> mark# X1) (mark# U11(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> active# U11(mark X1, X2, X3)) (mark# U11(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> U11#(mark X1, X2, X3)) (mark# U11(X1, X2, X3) -> mark# X1, mark# s X -> mark# X) (mark# U11(X1, X2, X3) -> mark# X1, mark# s X -> active# s mark X) (mark# U11(X1, X2, X3) -> mark# X1, mark# s X -> s# mark X) (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# plus(X1, X2) -> active# plus(mark X1, mark X2)) (mark# U11(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> plus#(mark X1, mark X2)) (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) -> active# U22(mark X1, X2, X3)) (mark# U11(X1, X2, X3) -> mark# X1, mark# U22(X1, X2, X3) -> U22#(mark X1, X2, X3)) (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) -> active# U21(mark X1, X2, X3)) (mark# U11(X1, X2, X3) -> mark# X1, mark# U21(X1, X2, X3) -> U21#(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) -> active# x(mark X1, mark X2)) (mark# U11(X1, X2, X3) -> mark# X1, mark# x(X1, X2) -> x#(mark X1, mark X2)) (mark# U11(X1, X2, X3) -> mark# X1, mark# 0() -> active# 0()) (active# U22(tt(), M, N) -> plus#(x(N, M), N), plus#(X1, mark X2) -> plus#(X1, X2)) (active# U22(tt(), M, N) -> plus#(x(N, M), N), plus#(X1, active X2) -> plus#(X1, X2)) (active# x(N, s M) -> mark# U21(tt(), M, N), mark# U21(X1, X2, X3) -> mark# X1) (active# x(N, s M) -> mark# U21(tt(), M, N), mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3)) (active# x(N, s M) -> mark# U21(tt(), M, N), mark# U21(X1, X2, X3) -> U21#(mark X1, X2, X3)) (active# plus(N, s M) -> mark# U11(tt(), M, N), mark# U11(X1, X2, X3) -> mark# X1) (active# plus(N, s M) -> mark# U11(tt(), M, N), mark# U11(X1, X2, X3) -> active# U11(mark X1, X2, X3)) (active# plus(N, s M) -> mark# U11(tt(), M, N), mark# U11(X1, X2, X3) -> U11#(mark X1, X2, X3)) (mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3), active# U21(tt(), M, N) -> mark# U22(tt(), M, N)) (mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3), active# U21(tt(), M, N) -> U22#(tt(), M, N)) (mark# U11(X1, X2, X3) -> active# U11(mark X1, X2, X3), active# U11(tt(), M, N) -> mark# U12(tt(), M, N)) (mark# U11(X1, X2, X3) -> active# U11(mark X1, X2, X3), active# U11(tt(), M, N) -> U12#(tt(), M, N)) (active# x(N, s M) -> U21#(tt(), M, N), U21#(X1, X2, mark X3) -> U21#(X1, X2, X3)) (active# x(N, s M) -> U21#(tt(), M, N), U21#(X1, X2, active X3) -> U21#(X1, X2, X3)) (active# x(N, s M) -> U21#(tt(), M, N), U21#(X1, mark X2, X3) -> U21#(X1, X2, X3)) (active# x(N, s M) -> U21#(tt(), M, N), U21#(X1, active X2, X3) -> U21#(X1, X2, X3)) (active# plus(N, s M) -> U11#(tt(), M, N), U11#(X1, X2, mark X3) -> U11#(X1, X2, X3)) (active# plus(N, s M) -> U11#(tt(), M, N), U11#(X1, X2, active X3) -> U11#(X1, X2, X3)) (active# plus(N, s M) -> U11#(tt(), M, N), U11#(X1, mark X2, X3) -> U11#(X1, X2, X3)) (active# plus(N, s M) -> U11#(tt(), M, N), U11#(X1, active X2, X3) -> U11#(X1, X2, X3)) (active# U12(tt(), M, N) -> mark# s plus(N, M), mark# s X -> mark# X) (active# U12(tt(), M, N) -> mark# s plus(N, M), mark# s X -> active# s mark X) (active# U12(tt(), M, N) -> mark# s plus(N, M), mark# s X -> s# mark X) (mark# x(X1, X2) -> x#(mark X1, mark X2), x#(X1, mark X2) -> x#(X1, X2)) (mark# x(X1, X2) -> x#(mark X1, mark X2), x#(X1, active X2) -> x#(X1, X2)) (mark# x(X1, X2) -> x#(mark X1, mark X2), x#(mark X1, X2) -> x#(X1, X2)) (mark# x(X1, X2) -> x#(mark X1, mark X2), x#(active X1, X2) -> x#(X1, X2)) (active# U22(tt(), M, N) -> mark# plus(x(N, M), N), mark# plus(X1, X2) -> mark# X1) (active# U22(tt(), M, N) -> mark# plus(x(N, M), N), mark# plus(X1, X2) -> mark# X2) (active# U22(tt(), M, N) -> mark# plus(x(N, M), N), mark# plus(X1, X2) -> active# plus(mark X1, mark X2)) (active# U22(tt(), M, N) -> mark# plus(x(N, M), N), mark# plus(X1, X2) -> plus#(mark X1, mark X2)) (active# x(N, 0()) -> mark# 0(), mark# 0() -> active# 0()) (active# U12(tt(), M, N) -> plus#(N, M), plus#(X1, mark X2) -> plus#(X1, X2)) (active# U12(tt(), M, N) -> plus#(N, M), plus#(X1, active X2) -> plus#(X1, X2)) (active# U12(tt(), M, N) -> plus#(N, M), plus#(mark X1, X2) -> plus#(X1, X2)) (active# U12(tt(), M, N) -> plus#(N, M), plus#(active X1, X2) -> plus#(X1, X2)) (mark# x(X1, X2) -> active# x(mark X1, mark X2), active# x(N, s M) -> mark# U21(tt(), M, N)) (mark# x(X1, X2) -> active# x(mark X1, mark X2), active# x(N, s M) -> U21#(tt(), M, N)) (mark# x(X1, X2) -> active# x(mark X1, mark X2), active# x(N, 0()) -> mark# 0()) (x#(active X1, X2) -> x#(X1, X2), x#(X1, mark X2) -> x#(X1, X2)) (x#(active X1, X2) -> x#(X1, X2), x#(X1, active X2) -> x#(X1, X2)) (x#(active X1, X2) -> x#(X1, X2), x#(mark X1, X2) -> x#(X1, X2)) (x#(active X1, X2) -> x#(X1, X2), x#(active X1, X2) -> x#(X1, X2)) (x#(X1, active X2) -> x#(X1, X2), x#(X1, mark X2) -> x#(X1, X2)) (x#(X1, active X2) -> x#(X1, X2), x#(X1, active X2) -> x#(X1, X2)) (x#(X1, active X2) -> x#(X1, X2), x#(mark X1, X2) -> x#(X1, X2)) (x#(X1, active X2) -> x#(X1, X2), x#(active X1, X2) -> x#(X1, X2)) (plus#(active X1, X2) -> plus#(X1, X2), plus#(X1, mark X2) -> plus#(X1, X2)) (plus#(active X1, X2) -> plus#(X1, X2), plus#(X1, active X2) -> plus#(X1, X2)) (plus#(active X1, X2) -> plus#(X1, X2), plus#(mark X1, X2) -> plus#(X1, X2)) (plus#(active X1, X2) -> plus#(X1, X2), plus#(active X1, X2) -> plus#(X1, X2)) (plus#(X1, active X2) -> plus#(X1, X2), plus#(X1, mark X2) -> plus#(X1, X2)) (plus#(X1, active X2) -> plus#(X1, X2), plus#(X1, active X2) -> plus#(X1, X2)) (plus#(X1, active X2) -> plus#(X1, X2), plus#(mark X1, X2) -> plus#(X1, X2)) (plus#(X1, active X2) -> plus#(X1, X2), plus#(active X1, X2) -> plus#(X1, X2)) (U21#(active X1, X2, X3) -> U21#(X1, X2, X3), U21#(X1, X2, mark X3) -> U21#(X1, X2, X3)) (U21#(active X1, X2, X3) -> U21#(X1, X2, X3), U21#(X1, X2, active X3) -> U21#(X1, X2, X3)) (U21#(active X1, X2, X3) -> U21#(X1, X2, X3), U21#(X1, mark X2, X3) -> U21#(X1, X2, X3)) (U21#(active X1, X2, X3) -> U21#(X1, X2, X3), U21#(X1, active X2, X3) -> U21#(X1, X2, X3)) (U21#(active X1, X2, X3) -> U21#(X1, X2, X3), U21#(mark X1, X2, X3) -> U21#(X1, X2, X3)) (U21#(active X1, X2, X3) -> U21#(X1, X2, X3), U21#(active X1, X2, X3) -> U21#(X1, X2, X3)) (U21#(X1, active X2, X3) -> U21#(X1, X2, X3), U21#(X1, X2, mark X3) -> U21#(X1, X2, X3)) (U21#(X1, active X2, X3) -> U21#(X1, X2, X3), U21#(X1, X2, active X3) -> U21#(X1, X2, X3)) (U21#(X1, active X2, X3) -> U21#(X1, X2, X3), U21#(X1, mark X2, X3) -> U21#(X1, X2, X3)) (U21#(X1, active X2, X3) -> U21#(X1, X2, X3), U21#(X1, active X2, X3) -> U21#(X1, X2, X3)) (U21#(X1, active X2, X3) -> U21#(X1, X2, X3), U21#(mark X1, X2, X3) -> U21#(X1, X2, X3)) (U21#(X1, active X2, X3) -> U21#(X1, X2, X3), U21#(active X1, X2, X3) -> U21#(X1, X2, X3)) (U21#(X1, X2, active X3) -> U21#(X1, X2, X3), U21#(X1, X2, mark X3) -> U21#(X1, X2, X3)) (U21#(X1, X2, active X3) -> U21#(X1, X2, X3), U21#(X1, X2, active X3) -> U21#(X1, X2, X3)) (U21#(X1, X2, active X3) -> U21#(X1, X2, X3), U21#(X1, mark X2, X3) -> U21#(X1, X2, X3)) (U21#(X1, X2, active X3) -> U21#(X1, X2, X3), U21#(X1, active X2, X3) -> U21#(X1, X2, X3)) (U21#(X1, X2, active X3) -> U21#(X1, X2, X3), U21#(mark X1, X2, X3) -> U21#(X1, X2, X3)) (U21#(X1, X2, active X3) -> U21#(X1, X2, X3), U21#(active X1, X2, X3) -> U21#(X1, X2, X3)) (U22#(active X1, X2, X3) -> U22#(X1, X2, X3), U22#(X1, X2, mark X3) -> U22#(X1, X2, X3)) (U22#(active X1, X2, X3) -> U22#(X1, X2, X3), U22#(X1, X2, active X3) -> U22#(X1, X2, X3)) (U22#(active X1, X2, X3) -> U22#(X1, X2, X3), U22#(X1, mark X2, X3) -> U22#(X1, X2, X3)) (U22#(active X1, X2, X3) -> U22#(X1, X2, X3), U22#(X1, active X2, X3) -> U22#(X1, X2, X3)) (U22#(active X1, X2, X3) -> U22#(X1, X2, X3), U22#(mark X1, X2, X3) -> U22#(X1, X2, X3)) (U22#(active X1, X2, X3) -> U22#(X1, X2, X3), U22#(active X1, X2, X3) -> U22#(X1, X2, X3)) (U22#(X1, active X2, X3) -> U22#(X1, X2, X3), U22#(X1, X2, mark X3) -> U22#(X1, X2, X3)) (U22#(X1, active X2, X3) -> U22#(X1, X2, X3), U22#(X1, X2, active X3) -> U22#(X1, X2, X3)) (U22#(X1, active X2, X3) -> U22#(X1, X2, X3), U22#(X1, mark X2, X3) -> U22#(X1, X2, X3)) (U22#(X1, active X2, X3) -> U22#(X1, X2, X3), U22#(X1, active X2, X3) -> U22#(X1, X2, X3)) (U22#(X1, active X2, X3) -> U22#(X1, X2, X3), U22#(mark X1, X2, X3) -> U22#(X1, X2, X3)) (U22#(X1, active X2, X3) -> U22#(X1, X2, X3), U22#(active X1, X2, X3) -> U22#(X1, X2, X3)) (U22#(X1, X2, active X3) -> U22#(X1, X2, X3), U22#(X1, X2, mark X3) -> U22#(X1, X2, X3)) (U22#(X1, X2, active X3) -> U22#(X1, X2, X3), U22#(X1, X2, active X3) -> U22#(X1, X2, X3)) (U22#(X1, X2, active X3) -> U22#(X1, X2, X3), U22#(X1, mark X2, X3) -> U22#(X1, X2, X3)) (U22#(X1, X2, active X3) -> U22#(X1, X2, X3), U22#(X1, active X2, X3) -> U22#(X1, X2, X3)) (U22#(X1, X2, active X3) -> U22#(X1, X2, X3), U22#(mark X1, X2, X3) -> U22#(X1, X2, X3)) (U22#(X1, X2, active X3) -> U22#(X1, X2, X3), U22#(active X1, X2, X3) -> U22#(X1, X2, X3)) (U11#(active X1, X2, X3) -> U11#(X1, X2, X3), U11#(X1, X2, mark X3) -> U11#(X1, X2, X3)) (U11#(active X1, X2, X3) -> U11#(X1, X2, X3), U11#(X1, X2, active X3) -> U11#(X1, X2, X3)) (U11#(active X1, X2, X3) -> U11#(X1, X2, X3), U11#(X1, mark X2, X3) -> U11#(X1, X2, X3)) (U11#(active X1, X2, X3) -> U11#(X1, X2, X3), U11#(X1, active X2, X3) -> U11#(X1, X2, X3)) (U11#(active X1, X2, X3) -> U11#(X1, X2, X3), U11#(mark X1, X2, X3) -> U11#(X1, X2, X3)) (U11#(active X1, X2, X3) -> U11#(X1, X2, X3), U11#(active X1, X2, X3) -> U11#(X1, X2, X3)) (U11#(X1, active X2, X3) -> U11#(X1, X2, X3), U11#(X1, X2, mark X3) -> U11#(X1, X2, X3)) (U11#(X1, active X2, X3) -> U11#(X1, X2, X3), U11#(X1, X2, active X3) -> U11#(X1, X2, X3)) (U11#(X1, active X2, X3) -> U11#(X1, X2, X3), U11#(X1, mark X2, X3) -> U11#(X1, X2, X3)) (U11#(X1, active X2, X3) -> U11#(X1, X2, X3), U11#(X1, active X2, X3) -> U11#(X1, X2, X3)) (U11#(X1, active X2, X3) -> U11#(X1, X2, X3), U11#(mark X1, X2, X3) -> U11#(X1, X2, X3)) (U11#(X1, active X2, X3) -> U11#(X1, X2, X3), U11#(active X1, X2, X3) -> U11#(X1, X2, X3)) (U11#(X1, X2, active X3) -> U11#(X1, X2, X3), U11#(X1, X2, mark X3) -> U11#(X1, X2, X3)) (U11#(X1, X2, active X3) -> U11#(X1, X2, X3), U11#(X1, X2, active X3) -> U11#(X1, X2, X3)) (U11#(X1, X2, active X3) -> U11#(X1, X2, X3), U11#(X1, mark X2, X3) -> U11#(X1, X2, X3)) (U11#(X1, X2, active X3) -> U11#(X1, X2, X3), U11#(X1, active X2, X3) -> U11#(X1, X2, X3)) (U11#(X1, X2, active X3) -> U11#(X1, X2, X3), U11#(mark X1, X2, X3) -> U11#(X1, X2, X3)) (U11#(X1, X2, active X3) -> U11#(X1, X2, X3), U11#(active X1, X2, X3) -> U11#(X1, X2, X3)) (U12#(active X1, X2, X3) -> U12#(X1, X2, X3), U12#(X1, X2, mark X3) -> U12#(X1, X2, X3)) (U12#(active X1, X2, X3) -> U12#(X1, X2, X3), U12#(X1, X2, active X3) -> U12#(X1, X2, X3)) (U12#(active X1, X2, X3) -> U12#(X1, X2, X3), U12#(X1, mark X2, X3) -> U12#(X1, X2, X3)) (U12#(active X1, X2, X3) -> U12#(X1, X2, X3), U12#(X1, active X2, X3) -> U12#(X1, X2, X3)) (U12#(active X1, X2, X3) -> U12#(X1, X2, X3), U12#(mark X1, X2, X3) -> U12#(X1, X2, X3)) (U12#(active X1, X2, X3) -> U12#(X1, X2, X3), U12#(active X1, X2, X3) -> U12#(X1, X2, X3)) (U12#(X1, active X2, X3) -> U12#(X1, X2, X3), U12#(X1, X2, mark X3) -> U12#(X1, X2, X3)) (U12#(X1, active X2, X3) -> U12#(X1, X2, X3), U12#(X1, X2, active X3) -> U12#(X1, X2, X3)) (U12#(X1, active X2, X3) -> U12#(X1, X2, X3), U12#(X1, mark X2, X3) -> U12#(X1, X2, X3)) (U12#(X1, active X2, X3) -> U12#(X1, X2, X3), U12#(X1, active X2, X3) -> U12#(X1, X2, X3)) (U12#(X1, active X2, X3) -> U12#(X1, X2, X3), U12#(mark X1, X2, X3) -> U12#(X1, X2, X3)) (U12#(X1, active X2, X3) -> U12#(X1, X2, X3), U12#(active X1, X2, X3) -> U12#(X1, X2, X3)) (U12#(X1, X2, active X3) -> U12#(X1, X2, X3), U12#(X1, X2, mark X3) -> U12#(X1, X2, X3)) (U12#(X1, X2, active X3) -> U12#(X1, X2, X3), U12#(X1, X2, active X3) -> U12#(X1, X2, X3)) (U12#(X1, X2, active X3) -> U12#(X1, X2, X3), U12#(X1, mark X2, X3) -> U12#(X1, X2, X3)) (U12#(X1, X2, active X3) -> U12#(X1, X2, X3), U12#(X1, active X2, X3) -> U12#(X1, X2, X3)) (U12#(X1, X2, active X3) -> U12#(X1, X2, X3), U12#(mark X1, X2, X3) -> U12#(X1, X2, X3)) (U12#(X1, X2, active X3) -> U12#(X1, X2, X3), U12#(active X1, X2, X3) -> U12#(X1, X2, X3)) (mark# U21(X1, X2, X3) -> U21#(mark X1, X2, X3), U21#(X1, X2, mark X3) -> U21#(X1, X2, X3)) (mark# U21(X1, X2, X3) -> U21#(mark X1, X2, X3), U21#(X1, X2, active X3) -> U21#(X1, X2, X3)) (mark# U21(X1, X2, X3) -> U21#(mark X1, X2, X3), U21#(X1, mark X2, X3) -> U21#(X1, X2, X3)) (mark# U21(X1, X2, X3) -> U21#(mark X1, X2, X3), U21#(X1, active X2, X3) -> U21#(X1, X2, X3)) (mark# U21(X1, X2, X3) -> U21#(mark X1, X2, X3), U21#(mark X1, X2, X3) -> U21#(X1, X2, X3)) (mark# U21(X1, X2, X3) -> U21#(mark X1, X2, X3), U21#(active X1, X2, X3) -> U21#(X1, X2, X3)) (mark# U11(X1, X2, X3) -> U11#(mark X1, X2, X3), U11#(X1, X2, mark X3) -> U11#(X1, X2, X3)) (mark# U11(X1, X2, X3) -> U11#(mark X1, X2, X3), U11#(X1, X2, active X3) -> U11#(X1, X2, X3)) (mark# U11(X1, X2, X3) -> U11#(mark X1, X2, X3), U11#(X1, mark X2, X3) -> U11#(X1, X2, X3)) (mark# U11(X1, X2, X3) -> U11#(mark X1, X2, X3), U11#(X1, active X2, X3) -> U11#(X1, X2, X3)) (mark# U11(X1, X2, X3) -> U11#(mark X1, X2, X3), U11#(mark X1, X2, X3) -> U11#(X1, X2, X3)) (mark# U11(X1, X2, X3) -> U11#(mark X1, X2, X3), U11#(active X1, X2, X3) -> U11#(X1, X2, X3)) (s# active X -> s# X, s# mark X -> s# X) (s# active X -> s# X, s# active X -> s# X) (mark# s X -> mark# X, mark# U12(X1, X2, X3) -> mark# X1) (mark# s X -> mark# X, mark# U12(X1, X2, X3) -> U12#(mark X1, X2, X3)) (mark# s X -> mark# X, mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3)) (mark# s X -> mark# X, mark# tt() -> active# tt()) (mark# s X -> mark# X, mark# U11(X1, X2, X3) -> mark# X1) (mark# s X -> mark# X, mark# U11(X1, X2, X3) -> active# U11(mark X1, X2, X3)) (mark# s X -> mark# X, mark# U11(X1, X2, X3) -> U11#(mark X1, X2, X3)) (mark# s X -> mark# X, mark# s X -> mark# X) (mark# s X -> mark# X, mark# s X -> active# s mark X) (mark# s X -> mark# X, mark# s X -> s# mark 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) -> active# plus(mark X1, mark X2)) (mark# s X -> mark# X, mark# plus(X1, X2) -> plus#(mark X1, mark X2)) (mark# s X -> mark# X, mark# U22(X1, X2, X3) -> mark# X1) (mark# s X -> mark# X, mark# U22(X1, X2, X3) -> active# U22(mark X1, X2, X3)) (mark# s X -> mark# X, mark# U22(X1, X2, X3) -> U22#(mark X1, X2, X3)) (mark# s X -> mark# X, mark# U21(X1, X2, X3) -> mark# X1) (mark# s X -> mark# X, mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3)) (mark# s X -> mark# X, mark# U21(X1, X2, X3) -> U21#(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) -> active# x(mark X1, mark X2)) (mark# s X -> mark# X, mark# x(X1, X2) -> x#(mark X1, mark X2)) (mark# s X -> mark# X, mark# 0() -> active# 0()) } EDG: { (s# mark X -> s# X, s# active X -> s# X) (s# mark X -> s# X, s# mark X -> s# X) (mark# U12(X1, X2, X3) -> U12#(mark X1, X2, X3), U12#(active X1, X2, X3) -> U12#(X1, X2, X3)) (mark# U12(X1, X2, X3) -> U12#(mark X1, X2, X3), U12#(mark X1, X2, X3) -> U12#(X1, X2, X3)) (mark# U12(X1, X2, X3) -> U12#(mark X1, X2, X3), U12#(X1, active X2, X3) -> U12#(X1, X2, X3)) (mark# U12(X1, X2, X3) -> U12#(mark X1, X2, X3), U12#(X1, mark X2, X3) -> U12#(X1, X2, X3)) (mark# U12(X1, X2, X3) -> U12#(mark X1, X2, X3), U12#(X1, X2, active X3) -> U12#(X1, X2, X3)) (mark# U12(X1, X2, X3) -> U12#(mark X1, X2, X3), U12#(X1, X2, mark X3) -> U12#(X1, X2, X3)) (mark# U22(X1, X2, X3) -> U22#(mark X1, X2, X3), U22#(active X1, X2, X3) -> U22#(X1, X2, X3)) (mark# U22(X1, X2, X3) -> U22#(mark X1, X2, X3), U22#(mark X1, X2, X3) -> U22#(X1, X2, X3)) (mark# U22(X1, X2, X3) -> U22#(mark X1, X2, X3), U22#(X1, active X2, X3) -> U22#(X1, X2, X3)) (mark# U22(X1, X2, X3) -> U22#(mark X1, X2, X3), U22#(X1, mark X2, X3) -> U22#(X1, X2, X3)) (mark# U22(X1, X2, X3) -> U22#(mark X1, X2, X3), U22#(X1, X2, active X3) -> U22#(X1, X2, X3)) (mark# U22(X1, X2, X3) -> U22#(mark X1, X2, X3), U22#(X1, X2, mark X3) -> U22#(X1, X2, X3)) (U12#(X1, X2, mark X3) -> U12#(X1, X2, X3), U12#(active X1, X2, X3) -> U12#(X1, X2, X3)) (U12#(X1, X2, mark X3) -> U12#(X1, X2, X3), U12#(mark X1, X2, X3) -> U12#(X1, X2, X3)) (U12#(X1, X2, mark X3) -> U12#(X1, X2, X3), U12#(X1, active X2, X3) -> U12#(X1, X2, X3)) (U12#(X1, X2, mark X3) -> U12#(X1, X2, X3), U12#(X1, mark X2, X3) -> U12#(X1, X2, X3)) (U12#(X1, X2, mark X3) -> U12#(X1, X2, X3), U12#(X1, X2, active X3) -> U12#(X1, X2, X3)) (U12#(X1, X2, mark X3) -> U12#(X1, X2, X3), U12#(X1, X2, mark X3) -> U12#(X1, X2, X3)) (U12#(X1, mark X2, X3) -> U12#(X1, X2, X3), U12#(active X1, X2, X3) -> U12#(X1, X2, X3)) (U12#(X1, mark X2, X3) -> U12#(X1, X2, X3), U12#(mark X1, X2, X3) -> U12#(X1, X2, X3)) (U12#(X1, mark X2, X3) -> U12#(X1, X2, X3), U12#(X1, active X2, X3) -> U12#(X1, X2, X3)) (U12#(X1, mark X2, X3) -> U12#(X1, X2, X3), U12#(X1, mark X2, X3) -> U12#(X1, X2, X3)) (U12#(X1, mark X2, X3) -> U12#(X1, X2, X3), U12#(X1, X2, active X3) -> U12#(X1, X2, X3)) (U12#(X1, mark X2, X3) -> U12#(X1, X2, X3), U12#(X1, X2, mark X3) -> U12#(X1, X2, X3)) (U12#(mark X1, X2, X3) -> U12#(X1, X2, X3), U12#(active X1, X2, X3) -> U12#(X1, X2, X3)) (U12#(mark X1, X2, X3) -> U12#(X1, X2, X3), U12#(mark X1, X2, X3) -> U12#(X1, X2, X3)) (U12#(mark X1, X2, X3) -> U12#(X1, X2, X3), U12#(X1, active X2, X3) -> U12#(X1, X2, X3)) (U12#(mark X1, X2, X3) -> U12#(X1, X2, X3), U12#(X1, mark X2, X3) -> U12#(X1, X2, X3)) (U12#(mark X1, X2, X3) -> U12#(X1, X2, X3), U12#(X1, X2, active X3) -> U12#(X1, X2, X3)) (U12#(mark X1, X2, X3) -> U12#(X1, X2, X3), U12#(X1, X2, mark X3) -> U12#(X1, X2, X3)) (U11#(X1, X2, mark X3) -> U11#(X1, X2, X3), U11#(active X1, X2, X3) -> U11#(X1, X2, X3)) (U11#(X1, X2, mark X3) -> U11#(X1, X2, X3), U11#(mark X1, X2, X3) -> U11#(X1, X2, X3)) (U11#(X1, X2, mark X3) -> U11#(X1, X2, X3), U11#(X1, active X2, X3) -> U11#(X1, X2, X3)) (U11#(X1, X2, mark X3) -> U11#(X1, X2, X3), U11#(X1, mark X2, X3) -> U11#(X1, X2, X3)) (U11#(X1, X2, mark X3) -> U11#(X1, X2, X3), U11#(X1, X2, active X3) -> U11#(X1, X2, X3)) (U11#(X1, X2, mark X3) -> U11#(X1, X2, X3), U11#(X1, X2, mark X3) -> U11#(X1, X2, X3)) (U11#(X1, mark X2, X3) -> U11#(X1, X2, X3), U11#(active X1, X2, X3) -> U11#(X1, X2, X3)) (U11#(X1, mark X2, X3) -> U11#(X1, X2, X3), U11#(mark X1, X2, X3) -> U11#(X1, X2, X3)) (U11#(X1, mark X2, X3) -> U11#(X1, X2, X3), U11#(X1, active X2, X3) -> U11#(X1, X2, X3)) (U11#(X1, mark X2, X3) -> U11#(X1, X2, X3), U11#(X1, mark X2, X3) -> U11#(X1, X2, X3)) (U11#(X1, mark X2, X3) -> U11#(X1, X2, X3), U11#(X1, X2, active X3) -> U11#(X1, X2, X3)) (U11#(X1, mark X2, X3) -> U11#(X1, X2, X3), U11#(X1, X2, mark X3) -> U11#(X1, X2, X3)) (U11#(mark X1, X2, X3) -> U11#(X1, X2, X3), U11#(active X1, X2, X3) -> U11#(X1, X2, X3)) (U11#(mark X1, X2, X3) -> U11#(X1, X2, X3), U11#(mark X1, X2, X3) -> U11#(X1, X2, X3)) (U11#(mark X1, X2, X3) -> U11#(X1, X2, X3), U11#(X1, active X2, X3) -> U11#(X1, X2, X3)) (U11#(mark X1, X2, X3) -> U11#(X1, X2, X3), U11#(X1, mark X2, X3) -> U11#(X1, X2, X3)) (U11#(mark X1, X2, X3) -> U11#(X1, X2, X3), U11#(X1, X2, active X3) -> U11#(X1, X2, X3)) (U11#(mark X1, X2, X3) -> U11#(X1, X2, X3), U11#(X1, X2, mark X3) -> U11#(X1, X2, X3)) (U22#(X1, X2, mark X3) -> U22#(X1, X2, X3), U22#(active X1, X2, X3) -> U22#(X1, X2, X3)) (U22#(X1, X2, mark X3) -> U22#(X1, X2, X3), U22#(mark X1, X2, X3) -> U22#(X1, X2, X3)) (U22#(X1, X2, mark X3) -> U22#(X1, X2, X3), U22#(X1, active X2, X3) -> U22#(X1, X2, X3)) (U22#(X1, X2, mark X3) -> U22#(X1, X2, X3), U22#(X1, mark X2, X3) -> U22#(X1, X2, X3)) (U22#(X1, X2, mark X3) -> U22#(X1, X2, X3), U22#(X1, X2, active X3) -> U22#(X1, X2, X3)) (U22#(X1, X2, mark X3) -> U22#(X1, X2, X3), U22#(X1, X2, mark X3) -> U22#(X1, X2, X3)) (U22#(X1, mark X2, X3) -> U22#(X1, X2, X3), U22#(active X1, X2, X3) -> U22#(X1, X2, X3)) (U22#(X1, mark X2, X3) -> U22#(X1, X2, X3), U22#(mark X1, X2, X3) -> U22#(X1, X2, X3)) (U22#(X1, mark X2, X3) -> U22#(X1, X2, X3), U22#(X1, active X2, X3) -> U22#(X1, X2, X3)) (U22#(X1, mark X2, X3) -> U22#(X1, X2, X3), U22#(X1, mark X2, X3) -> U22#(X1, X2, X3)) (U22#(X1, mark X2, X3) -> U22#(X1, X2, X3), U22#(X1, X2, active X3) -> U22#(X1, X2, X3)) (U22#(X1, mark X2, X3) -> U22#(X1, X2, X3), U22#(X1, X2, mark X3) -> U22#(X1, X2, X3)) (U22#(mark X1, X2, X3) -> U22#(X1, X2, X3), U22#(active X1, X2, X3) -> U22#(X1, X2, X3)) (U22#(mark X1, X2, X3) -> U22#(X1, X2, X3), U22#(mark X1, X2, X3) -> U22#(X1, X2, X3)) (U22#(mark X1, X2, X3) -> U22#(X1, X2, X3), U22#(X1, active X2, X3) -> U22#(X1, X2, X3)) (U22#(mark X1, X2, X3) -> U22#(X1, X2, X3), U22#(X1, mark X2, X3) -> U22#(X1, X2, X3)) (U22#(mark X1, X2, X3) -> U22#(X1, X2, X3), U22#(X1, X2, active X3) -> U22#(X1, X2, X3)) (U22#(mark X1, X2, X3) -> U22#(X1, X2, X3), U22#(X1, X2, mark X3) -> U22#(X1, X2, X3)) (U21#(X1, X2, mark X3) -> U21#(X1, X2, X3), U21#(active X1, X2, X3) -> U21#(X1, X2, X3)) (U21#(X1, X2, mark X3) -> U21#(X1, X2, X3), U21#(mark X1, X2, X3) -> U21#(X1, X2, X3)) (U21#(X1, X2, mark X3) -> U21#(X1, X2, X3), U21#(X1, active X2, X3) -> U21#(X1, X2, X3)) (U21#(X1, X2, mark X3) -> U21#(X1, X2, X3), U21#(X1, mark X2, X3) -> U21#(X1, X2, X3)) (U21#(X1, X2, mark X3) -> U21#(X1, X2, X3), U21#(X1, X2, active X3) -> U21#(X1, X2, X3)) (U21#(X1, X2, mark X3) -> U21#(X1, X2, X3), U21#(X1, X2, mark X3) -> U21#(X1, X2, X3)) (U21#(X1, mark X2, X3) -> U21#(X1, X2, X3), U21#(active X1, X2, X3) -> U21#(X1, X2, X3)) (U21#(X1, mark X2, X3) -> U21#(X1, X2, X3), U21#(mark X1, X2, X3) -> U21#(X1, X2, X3)) (U21#(X1, mark X2, X3) -> U21#(X1, X2, X3), U21#(X1, active X2, X3) -> U21#(X1, X2, X3)) (U21#(X1, mark X2, X3) -> U21#(X1, X2, X3), U21#(X1, mark X2, X3) -> U21#(X1, X2, X3)) (U21#(X1, mark X2, X3) -> U21#(X1, X2, X3), U21#(X1, X2, active X3) -> U21#(X1, X2, X3)) (U21#(X1, mark X2, X3) -> U21#(X1, X2, X3), U21#(X1, X2, mark X3) -> U21#(X1, X2, X3)) (U21#(mark X1, X2, X3) -> U21#(X1, X2, X3), U21#(active X1, X2, X3) -> U21#(X1, X2, X3)) (U21#(mark X1, X2, X3) -> U21#(X1, X2, X3), U21#(mark X1, X2, X3) -> U21#(X1, X2, X3)) (U21#(mark X1, X2, X3) -> U21#(X1, X2, X3), U21#(X1, active X2, X3) -> U21#(X1, X2, X3)) (U21#(mark X1, X2, X3) -> U21#(X1, X2, X3), U21#(X1, mark X2, X3) -> U21#(X1, X2, X3)) (U21#(mark X1, X2, X3) -> U21#(X1, X2, X3), U21#(X1, X2, active X3) -> U21#(X1, X2, X3)) (U21#(mark X1, X2, X3) -> U21#(X1, X2, X3), U21#(X1, X2, mark X3) -> U21#(X1, X2, X3)) (plus#(X1, mark X2) -> plus#(X1, X2), plus#(active X1, X2) -> plus#(X1, X2)) (plus#(X1, mark X2) -> plus#(X1, X2), plus#(mark X1, X2) -> plus#(X1, X2)) (plus#(X1, mark X2) -> plus#(X1, X2), plus#(X1, active X2) -> plus#(X1, X2)) (plus#(X1, mark X2) -> plus#(X1, X2), plus#(X1, mark X2) -> plus#(X1, X2)) (plus#(mark X1, X2) -> plus#(X1, X2), plus#(active X1, X2) -> plus#(X1, X2)) (plus#(mark X1, X2) -> plus#(X1, X2), plus#(mark X1, X2) -> plus#(X1, X2)) (plus#(mark X1, X2) -> plus#(X1, X2), plus#(X1, active X2) -> plus#(X1, X2)) (plus#(mark X1, X2) -> plus#(X1, X2), plus#(X1, mark X2) -> plus#(X1, X2)) (x#(X1, mark X2) -> x#(X1, X2), x#(active X1, X2) -> x#(X1, X2)) (x#(X1, mark X2) -> x#(X1, X2), x#(mark X1, X2) -> x#(X1, X2)) (x#(X1, mark X2) -> x#(X1, X2), x#(X1, active X2) -> x#(X1, X2)) (x#(X1, mark X2) -> x#(X1, X2), x#(X1, mark X2) -> x#(X1, X2)) (x#(mark X1, X2) -> x#(X1, X2), x#(active X1, X2) -> x#(X1, X2)) (x#(mark X1, X2) -> x#(X1, X2), x#(mark X1, X2) -> x#(X1, X2)) (x#(mark X1, X2) -> x#(X1, X2), x#(X1, active X2) -> x#(X1, X2)) (x#(mark X1, X2) -> x#(X1, X2), x#(X1, mark X2) -> x#(X1, X2)) (mark# plus(X1, X2) -> active# plus(mark X1, mark X2), active# plus(N, 0()) -> mark# N) (mark# plus(X1, X2) -> active# plus(mark X1, mark X2), active# plus(N, s M) -> U11#(tt(), M, N)) (mark# plus(X1, X2) -> active# plus(mark X1, mark X2), active# plus(N, s M) -> mark# U11(tt(), M, N)) (mark# s X -> s# mark X, s# active X -> s# X) (mark# s X -> s# mark X, s# mark X -> s# X) (active# U22(tt(), M, N) -> x#(N, M), x#(active X1, X2) -> x#(X1, X2)) (active# U22(tt(), M, N) -> x#(N, M), x#(mark X1, X2) -> x#(X1, X2)) (active# U22(tt(), M, N) -> x#(N, M), x#(X1, active X2) -> x#(X1, X2)) (active# U22(tt(), M, N) -> x#(N, M), x#(X1, mark X2) -> x#(X1, X2)) (mark# plus(X1, X2) -> plus#(mark X1, mark X2), plus#(active X1, X2) -> plus#(X1, X2)) (mark# plus(X1, X2) -> plus#(mark X1, mark X2), plus#(mark X1, X2) -> plus#(X1, X2)) (mark# plus(X1, X2) -> plus#(mark X1, mark X2), plus#(X1, active X2) -> plus#(X1, X2)) (mark# plus(X1, X2) -> plus#(mark X1, mark X2), plus#(X1, mark X2) -> plus#(X1, X2)) (active# U11(tt(), M, N) -> U12#(tt(), M, N), U12#(X1, active X2, X3) -> U12#(X1, X2, X3)) (active# U11(tt(), M, N) -> U12#(tt(), M, N), U12#(X1, mark X2, X3) -> U12#(X1, X2, X3)) (active# U11(tt(), M, N) -> U12#(tt(), M, N), U12#(X1, X2, active X3) -> U12#(X1, X2, X3)) (active# U11(tt(), M, N) -> U12#(tt(), M, N), U12#(X1, X2, mark X3) -> U12#(X1, X2, X3)) (active# U21(tt(), M, N) -> U22#(tt(), M, N), U22#(X1, active X2, X3) -> U22#(X1, X2, X3)) (active# U21(tt(), M, N) -> U22#(tt(), M, N), U22#(X1, mark X2, X3) -> U22#(X1, X2, X3)) (active# U21(tt(), M, N) -> U22#(tt(), M, N), U22#(X1, X2, active X3) -> U22#(X1, X2, X3)) (active# U21(tt(), M, N) -> U22#(tt(), M, N), U22#(X1, X2, mark X3) -> U22#(X1, X2, X3)) (mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3), active# U12(tt(), M, N) -> plus#(N, M)) (mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3), active# U12(tt(), M, N) -> s# plus(N, M)) (mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3), active# U12(tt(), M, N) -> mark# s plus(N, M)) (mark# U22(X1, X2, X3) -> active# U22(mark X1, X2, X3), active# U22(tt(), M, N) -> x#(N, M)) (mark# U22(X1, X2, X3) -> active# U22(mark X1, X2, X3), active# U22(tt(), M, N) -> plus#(x(N, M), N)) (mark# U22(X1, X2, X3) -> active# U22(mark X1, X2, X3), active# U22(tt(), M, N) -> mark# plus(x(N, M), N)) (active# U11(tt(), M, N) -> mark# U12(tt(), M, N), mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3)) (active# U11(tt(), M, N) -> mark# U12(tt(), M, N), mark# U12(X1, X2, X3) -> U12#(mark X1, X2, X3)) (active# U11(tt(), M, N) -> mark# U12(tt(), M, N), mark# U12(X1, X2, X3) -> mark# X1) (active# U21(tt(), M, N) -> mark# U22(tt(), M, N), mark# U22(X1, X2, X3) -> U22#(mark X1, X2, X3)) (active# U21(tt(), M, N) -> mark# U22(tt(), M, N), mark# U22(X1, X2, X3) -> active# U22(mark X1, X2, X3)) (active# U21(tt(), M, N) -> mark# U22(tt(), M, N), mark# U22(X1, X2, X3) -> mark# X1) (active# plus(N, 0()) -> mark# N, mark# 0() -> active# 0()) (active# plus(N, 0()) -> mark# N, mark# x(X1, X2) -> x#(mark X1, mark X2)) (active# plus(N, 0()) -> mark# N, mark# x(X1, X2) -> active# x(mark X1, mark X2)) (active# plus(N, 0()) -> mark# N, mark# x(X1, X2) -> mark# X2) (active# plus(N, 0()) -> mark# N, mark# x(X1, X2) -> mark# X1) (active# plus(N, 0()) -> mark# N, mark# U21(X1, X2, X3) -> U21#(mark X1, X2, X3)) (active# plus(N, 0()) -> mark# N, mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3)) (active# plus(N, 0()) -> mark# N, mark# U21(X1, X2, X3) -> mark# X1) (active# plus(N, 0()) -> mark# N, mark# U22(X1, X2, X3) -> U22#(mark X1, X2, X3)) (active# plus(N, 0()) -> mark# N, mark# U22(X1, X2, X3) -> active# U22(mark X1, X2, X3)) (active# plus(N, 0()) -> mark# N, mark# U22(X1, X2, X3) -> mark# X1) (active# plus(N, 0()) -> mark# N, mark# plus(X1, X2) -> plus#(mark X1, mark X2)) (active# plus(N, 0()) -> mark# N, mark# plus(X1, X2) -> active# plus(mark X1, mark X2)) (active# plus(N, 0()) -> mark# N, mark# plus(X1, X2) -> mark# X2) (active# plus(N, 0()) -> mark# N, mark# plus(X1, X2) -> mark# X1) (active# plus(N, 0()) -> mark# N, mark# s X -> s# mark X) (active# plus(N, 0()) -> mark# N, mark# s X -> active# s mark X) (active# plus(N, 0()) -> mark# N, mark# s X -> mark# X) (active# plus(N, 0()) -> mark# N, mark# U11(X1, X2, X3) -> U11#(mark X1, X2, X3)) (active# plus(N, 0()) -> mark# N, mark# U11(X1, X2, X3) -> active# U11(mark X1, X2, X3)) (active# plus(N, 0()) -> mark# N, mark# U11(X1, X2, X3) -> mark# X1) (active# plus(N, 0()) -> mark# N, mark# tt() -> active# tt()) (active# plus(N, 0()) -> mark# N, mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3)) (active# plus(N, 0()) -> mark# N, mark# U12(X1, X2, X3) -> U12#(mark X1, X2, X3)) (active# plus(N, 0()) -> mark# N, mark# U12(X1, X2, X3) -> mark# X1) (mark# U12(X1, X2, X3) -> mark# X1, mark# 0() -> active# 0()) (mark# U12(X1, X2, X3) -> mark# X1, mark# x(X1, X2) -> x#(mark X1, mark X2)) (mark# U12(X1, X2, X3) -> mark# X1, mark# x(X1, X2) -> active# 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# U21(X1, X2, X3) -> U21#(mark X1, X2, X3)) (mark# U12(X1, X2, X3) -> mark# X1, mark# U21(X1, X2, X3) -> active# 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# U22(X1, X2, X3) -> U22#(mark X1, X2, X3)) (mark# U12(X1, X2, X3) -> mark# X1, mark# U22(X1, X2, X3) -> active# 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# plus(X1, X2) -> plus#(mark X1, mark X2)) (mark# U12(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> active# plus(mark X1, mark X2)) (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# s X -> s# mark X) (mark# U12(X1, X2, X3) -> mark# X1, mark# s X -> active# s mark X) (mark# U12(X1, X2, X3) -> mark# X1, mark# s X -> mark# X) (mark# U12(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> U11#(mark X1, X2, X3)) (mark# U12(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> active# U11(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# tt() -> active# tt()) (mark# U12(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3)) (mark# U12(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> U12#(mark X1, X2, X3)) (mark# U12(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# 0() -> active# 0()) (mark# plus(X1, X2) -> mark# X1, mark# x(X1, X2) -> x#(mark X1, mark X2)) (mark# plus(X1, X2) -> mark# X1, mark# x(X1, X2) -> active# x(mark X1, mark X2)) (mark# plus(X1, X2) -> mark# X1, mark# x(X1, X2) -> mark# X2) (mark# plus(X1, X2) -> mark# X1, mark# x(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# U21(X1, X2, X3) -> U21#(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X1, mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X1, mark# U21(X1, X2, X3) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# U22(X1, X2, X3) -> U22#(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X1, mark# U22(X1, X2, X3) -> active# U22(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X1, mark# U22(X1, X2, X3) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# plus(X1, X2) -> plus#(mark X1, mark X2)) (mark# plus(X1, X2) -> mark# X1, mark# plus(X1, X2) -> active# plus(mark X1, mark X2)) (mark# plus(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# plus(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# s X -> s# mark X) (mark# plus(X1, X2) -> mark# X1, mark# s X -> active# s mark X) (mark# plus(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# plus(X1, X2) -> mark# X1, mark# U11(X1, X2, X3) -> U11#(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X1, mark# U11(X1, X2, X3) -> active# 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# tt() -> active# tt()) (mark# plus(X1, X2) -> mark# X1, mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X1, mark# U12(X1, X2, X3) -> U12#(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X1, mark# U12(X1, X2, X3) -> mark# X1) (mark# U21(X1, X2, X3) -> mark# X1, mark# 0() -> active# 0()) (mark# U21(X1, X2, X3) -> mark# X1, mark# x(X1, X2) -> x#(mark X1, mark X2)) (mark# U21(X1, X2, X3) -> mark# X1, mark# x(X1, X2) -> active# 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# U21(X1, X2, X3) -> U21#(mark X1, X2, X3)) (mark# U21(X1, X2, X3) -> mark# X1, mark# U21(X1, X2, X3) -> active# 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# U22(X1, X2, X3) -> U22#(mark X1, X2, X3)) (mark# U21(X1, X2, X3) -> mark# X1, mark# U22(X1, X2, X3) -> active# 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# plus(X1, X2) -> plus#(mark X1, mark X2)) (mark# U21(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> active# 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# s X -> s# mark X) (mark# U21(X1, X2, X3) -> mark# X1, mark# s X -> active# s mark X) (mark# U21(X1, X2, X3) -> mark# X1, mark# s X -> mark# X) (mark# U21(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> U11#(mark X1, X2, X3)) (mark# U21(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> active# U11(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# tt() -> active# tt()) (mark# U21(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3)) (mark# U21(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> U12#(mark X1, X2, X3)) (mark# U21(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> mark# X1) (mark# plus(X1, X2) -> mark# X2, mark# 0() -> active# 0()) (mark# plus(X1, X2) -> mark# X2, mark# x(X1, X2) -> x#(mark X1, mark X2)) (mark# plus(X1, X2) -> mark# X2, mark# x(X1, X2) -> active# 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# U21(X1, X2, X3) -> U21#(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X2, mark# U21(X1, X2, X3) -> active# 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# U22(X1, X2, X3) -> U22#(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X2, mark# U22(X1, X2, X3) -> active# 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# plus(X1, X2) -> plus#(mark X1, mark X2)) (mark# plus(X1, X2) -> mark# X2, mark# plus(X1, X2) -> active# plus(mark X1, mark X2)) (mark# plus(X1, X2) -> mark# X2, mark# plus(X1, X2) -> mark# X2) (mark# plus(X1, X2) -> mark# X2, mark# plus(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X2, mark# s X -> s# mark X) (mark# plus(X1, X2) -> mark# X2, mark# s X -> active# s mark X) (mark# plus(X1, X2) -> mark# X2, mark# s X -> mark# X) (mark# plus(X1, X2) -> mark# X2, mark# U11(X1, X2, X3) -> U11#(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X2, mark# U11(X1, X2, X3) -> active# U11(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X2, mark# U11(X1, X2, X3) -> mark# X1) (mark# plus(X1, X2) -> mark# X2, mark# tt() -> active# tt()) (mark# plus(X1, X2) -> mark# X2, mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X2, mark# U12(X1, X2, X3) -> U12#(mark X1, X2, X3)) (mark# plus(X1, X2) -> 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# X2, mark# U12(X1, X2, X3) -> U12#(mark X1, X2, X3)) (mark# x(X1, X2) -> mark# X2, mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3)) (mark# x(X1, X2) -> mark# X2, mark# tt() -> active# tt()) (mark# x(X1, X2) -> mark# X2, mark# U11(X1, X2, X3) -> mark# X1) (mark# x(X1, X2) -> mark# X2, mark# U11(X1, X2, X3) -> active# U11(mark X1, X2, X3)) (mark# x(X1, X2) -> mark# X2, mark# U11(X1, X2, X3) -> U11#(mark X1, X2, X3)) (mark# x(X1, X2) -> mark# X2, mark# s X -> mark# X) (mark# x(X1, X2) -> mark# X2, mark# s X -> active# s mark X) (mark# x(X1, X2) -> mark# X2, mark# s X -> s# mark X) (mark# x(X1, X2) -> mark# X2, mark# plus(X1, X2) -> mark# X1) (mark# x(X1, X2) -> mark# X2, mark# plus(X1, X2) -> mark# X2) (mark# x(X1, X2) -> mark# X2, mark# plus(X1, X2) -> active# plus(mark X1, mark X2)) (mark# x(X1, X2) -> mark# X2, mark# plus(X1, X2) -> plus#(mark X1, mark X2)) (mark# x(X1, X2) -> mark# X2, mark# U22(X1, X2, X3) -> mark# X1) (mark# x(X1, X2) -> mark# X2, mark# U22(X1, X2, X3) -> active# U22(mark X1, X2, X3)) (mark# x(X1, X2) -> mark# X2, mark# U22(X1, X2, X3) -> U22#(mark X1, X2, X3)) (mark# x(X1, X2) -> mark# X2, mark# U21(X1, X2, X3) -> mark# X1) (mark# x(X1, X2) -> mark# X2, mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3)) (mark# x(X1, X2) -> mark# X2, mark# U21(X1, X2, X3) -> U21#(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) -> active# x(mark X1, mark X2)) (mark# x(X1, X2) -> mark# X2, mark# x(X1, X2) -> x#(mark X1, mark X2)) (mark# x(X1, X2) -> mark# X2, mark# 0() -> active# 0()) (mark# x(X1, X2) -> mark# X1, mark# U12(X1, X2, X3) -> mark# X1) (mark# x(X1, X2) -> mark# X1, mark# U12(X1, X2, X3) -> U12#(mark X1, X2, X3)) (mark# x(X1, X2) -> mark# X1, mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3)) (mark# x(X1, X2) -> mark# X1, mark# tt() -> active# tt()) (mark# x(X1, X2) -> mark# X1, mark# U11(X1, X2, X3) -> mark# X1) (mark# x(X1, X2) -> mark# X1, mark# U11(X1, X2, X3) -> active# U11(mark X1, X2, X3)) (mark# x(X1, X2) -> mark# X1, mark# U11(X1, X2, X3) -> U11#(mark X1, X2, X3)) (mark# x(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# x(X1, X2) -> mark# X1, mark# s X -> active# s mark X) (mark# x(X1, X2) -> mark# X1, mark# s X -> s# mark X) (mark# x(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# x(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# x(X1, X2) -> mark# X1, mark# plus(X1, X2) -> active# plus(mark X1, mark X2)) (mark# x(X1, X2) -> mark# X1, mark# plus(X1, X2) -> plus#(mark X1, mark X2)) (mark# x(X1, X2) -> mark# X1, mark# U22(X1, X2, X3) -> mark# X1) (mark# x(X1, X2) -> mark# X1, mark# U22(X1, X2, X3) -> active# U22(mark X1, X2, X3)) (mark# x(X1, X2) -> mark# X1, mark# U22(X1, X2, X3) -> U22#(mark X1, X2, X3)) (mark# x(X1, X2) -> mark# X1, mark# U21(X1, X2, X3) -> mark# X1) (mark# x(X1, X2) -> mark# X1, mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3)) (mark# x(X1, X2) -> mark# X1, mark# U21(X1, X2, X3) -> U21#(mark X1, X2, X3)) (mark# x(X1, X2) -> mark# X1, mark# x(X1, X2) -> mark# X1) (mark# x(X1, X2) -> mark# X1, mark# x(X1, X2) -> mark# X2) (mark# x(X1, X2) -> mark# X1, mark# x(X1, X2) -> active# x(mark X1, mark X2)) (mark# x(X1, X2) -> mark# X1, mark# x(X1, X2) -> x#(mark X1, mark X2)) (mark# x(X1, X2) -> mark# X1, mark# 0() -> active# 0()) (mark# U22(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> mark# X1) (mark# U22(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> U12#(mark X1, X2, X3)) (mark# U22(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3)) (mark# U22(X1, X2, X3) -> mark# X1, mark# tt() -> active# tt()) (mark# U22(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> mark# X1) (mark# U22(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> active# U11(mark X1, X2, X3)) (mark# U22(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> U11#(mark X1, X2, X3)) (mark# U22(X1, X2, X3) -> mark# X1, mark# s X -> mark# X) (mark# U22(X1, X2, X3) -> mark# X1, mark# s X -> active# s mark X) (mark# U22(X1, X2, X3) -> mark# X1, mark# s X -> s# mark X) (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# plus(X1, X2) -> active# plus(mark X1, mark X2)) (mark# U22(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> plus#(mark X1, mark X2)) (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) -> active# U22(mark X1, X2, X3)) (mark# U22(X1, X2, X3) -> mark# X1, mark# U22(X1, X2, X3) -> U22#(mark X1, X2, X3)) (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) -> active# U21(mark X1, X2, X3)) (mark# U22(X1, X2, X3) -> mark# X1, mark# U21(X1, X2, X3) -> U21#(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) -> active# x(mark X1, mark X2)) (mark# U22(X1, X2, X3) -> mark# X1, mark# x(X1, X2) -> x#(mark X1, mark X2)) (mark# U22(X1, X2, X3) -> mark# X1, mark# 0() -> active# 0()) (mark# U11(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> mark# X1) (mark# U11(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> U12#(mark X1, X2, X3)) (mark# U11(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3)) (mark# U11(X1, X2, X3) -> mark# X1, mark# tt() -> active# tt()) (mark# U11(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> mark# X1) (mark# U11(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> active# U11(mark X1, X2, X3)) (mark# U11(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> U11#(mark X1, X2, X3)) (mark# U11(X1, X2, X3) -> mark# X1, mark# s X -> mark# X) (mark# U11(X1, X2, X3) -> mark# X1, mark# s X -> active# s mark X) (mark# U11(X1, X2, X3) -> mark# X1, mark# s X -> s# mark X) (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# plus(X1, X2) -> active# plus(mark X1, mark X2)) (mark# U11(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> plus#(mark X1, mark X2)) (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) -> active# U22(mark X1, X2, X3)) (mark# U11(X1, X2, X3) -> mark# X1, mark# U22(X1, X2, X3) -> U22#(mark X1, X2, X3)) (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) -> active# U21(mark X1, X2, X3)) (mark# U11(X1, X2, X3) -> mark# X1, mark# U21(X1, X2, X3) -> U21#(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) -> active# x(mark X1, mark X2)) (mark# U11(X1, X2, X3) -> mark# X1, mark# x(X1, X2) -> x#(mark X1, mark X2)) (mark# U11(X1, X2, X3) -> mark# X1, mark# 0() -> active# 0()) (active# U22(tt(), M, N) -> plus#(x(N, M), N), plus#(X1, mark X2) -> plus#(X1, X2)) (active# U22(tt(), M, N) -> plus#(x(N, M), N), plus#(X1, active X2) -> plus#(X1, X2)) (active# x(N, s M) -> mark# U21(tt(), M, N), mark# U21(X1, X2, X3) -> mark# X1) (active# x(N, s M) -> mark# U21(tt(), M, N), mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3)) (active# x(N, s M) -> mark# U21(tt(), M, N), mark# U21(X1, X2, X3) -> U21#(mark X1, X2, X3)) (active# plus(N, s M) -> mark# U11(tt(), M, N), mark# U11(X1, X2, X3) -> mark# X1) (active# plus(N, s M) -> mark# U11(tt(), M, N), mark# U11(X1, X2, X3) -> active# U11(mark X1, X2, X3)) (active# plus(N, s M) -> mark# U11(tt(), M, N), mark# U11(X1, X2, X3) -> U11#(mark X1, X2, X3)) (mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3), active# U21(tt(), M, N) -> mark# U22(tt(), M, N)) (mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3), active# U21(tt(), M, N) -> U22#(tt(), M, N)) (mark# U11(X1, X2, X3) -> active# U11(mark X1, X2, X3), active# U11(tt(), M, N) -> mark# U12(tt(), M, N)) (mark# U11(X1, X2, X3) -> active# U11(mark X1, X2, X3), active# U11(tt(), M, N) -> U12#(tt(), M, N)) (active# x(N, s M) -> U21#(tt(), M, N), U21#(X1, X2, mark X3) -> U21#(X1, X2, X3)) (active# x(N, s M) -> U21#(tt(), M, N), U21#(X1, X2, active X3) -> U21#(X1, X2, X3)) (active# x(N, s M) -> U21#(tt(), M, N), U21#(X1, mark X2, X3) -> U21#(X1, X2, X3)) (active# x(N, s M) -> U21#(tt(), M, N), U21#(X1, active X2, X3) -> U21#(X1, X2, X3)) (active# plus(N, s M) -> U11#(tt(), M, N), U11#(X1, X2, mark X3) -> U11#(X1, X2, X3)) (active# plus(N, s M) -> U11#(tt(), M, N), U11#(X1, X2, active X3) -> U11#(X1, X2, X3)) (active# plus(N, s M) -> U11#(tt(), M, N), U11#(X1, mark X2, X3) -> U11#(X1, X2, X3)) (active# plus(N, s M) -> U11#(tt(), M, N), U11#(X1, active X2, X3) -> U11#(X1, X2, X3)) (active# U12(tt(), M, N) -> mark# s plus(N, M), mark# s X -> mark# X) (active# U12(tt(), M, N) -> mark# s plus(N, M), mark# s X -> active# s mark X) (active# U12(tt(), M, N) -> mark# s plus(N, M), mark# s X -> s# mark X) (mark# x(X1, X2) -> x#(mark X1, mark X2), x#(X1, mark X2) -> x#(X1, X2)) (mark# x(X1, X2) -> x#(mark X1, mark X2), x#(X1, active X2) -> x#(X1, X2)) (mark# x(X1, X2) -> x#(mark X1, mark X2), x#(mark X1, X2) -> x#(X1, X2)) (mark# x(X1, X2) -> x#(mark X1, mark X2), x#(active X1, X2) -> x#(X1, X2)) (active# U22(tt(), M, N) -> mark# plus(x(N, M), N), mark# plus(X1, X2) -> mark# X1) (active# U22(tt(), M, N) -> mark# plus(x(N, M), N), mark# plus(X1, X2) -> mark# X2) (active# U22(tt(), M, N) -> mark# plus(x(N, M), N), mark# plus(X1, X2) -> active# plus(mark X1, mark X2)) (active# U22(tt(), M, N) -> mark# plus(x(N, M), N), mark# plus(X1, X2) -> plus#(mark X1, mark X2)) (active# x(N, 0()) -> mark# 0(), mark# 0() -> active# 0()) (active# U12(tt(), M, N) -> plus#(N, M), plus#(X1, mark X2) -> plus#(X1, X2)) (active# U12(tt(), M, N) -> plus#(N, M), plus#(X1, active X2) -> plus#(X1, X2)) (active# U12(tt(), M, N) -> plus#(N, M), plus#(mark X1, X2) -> plus#(X1, X2)) (active# U12(tt(), M, N) -> plus#(N, M), plus#(active X1, X2) -> plus#(X1, X2)) (mark# x(X1, X2) -> active# x(mark X1, mark X2), active# x(N, s M) -> mark# U21(tt(), M, N)) (mark# x(X1, X2) -> active# x(mark X1, mark X2), active# x(N, s M) -> U21#(tt(), M, N)) (mark# x(X1, X2) -> active# x(mark X1, mark X2), active# x(N, 0()) -> mark# 0()) (x#(active X1, X2) -> x#(X1, X2), x#(X1, mark X2) -> x#(X1, X2)) (x#(active X1, X2) -> x#(X1, X2), x#(X1, active X2) -> x#(X1, X2)) (x#(active X1, X2) -> x#(X1, X2), x#(mark X1, X2) -> x#(X1, X2)) (x#(active X1, X2) -> x#(X1, X2), x#(active X1, X2) -> x#(X1, X2)) (x#(X1, active X2) -> x#(X1, X2), x#(X1, mark X2) -> x#(X1, X2)) (x#(X1, active X2) -> x#(X1, X2), x#(X1, active X2) -> x#(X1, X2)) (x#(X1, active X2) -> x#(X1, X2), x#(mark X1, X2) -> x#(X1, X2)) (x#(X1, active X2) -> x#(X1, X2), x#(active X1, X2) -> x#(X1, X2)) (plus#(active X1, X2) -> plus#(X1, X2), plus#(X1, mark X2) -> plus#(X1, X2)) (plus#(active X1, X2) -> plus#(X1, X2), plus#(X1, active X2) -> plus#(X1, X2)) (plus#(active X1, X2) -> plus#(X1, X2), plus#(mark X1, X2) -> plus#(X1, X2)) (plus#(active X1, X2) -> plus#(X1, X2), plus#(active X1, X2) -> plus#(X1, X2)) (plus#(X1, active X2) -> plus#(X1, X2), plus#(X1, mark X2) -> plus#(X1, X2)) (plus#(X1, active X2) -> plus#(X1, X2), plus#(X1, active X2) -> plus#(X1, X2)) (plus#(X1, active X2) -> plus#(X1, X2), plus#(mark X1, X2) -> plus#(X1, X2)) (plus#(X1, active X2) -> plus#(X1, X2), plus#(active X1, X2) -> plus#(X1, X2)) (U21#(active X1, X2, X3) -> U21#(X1, X2, X3), U21#(X1, X2, mark X3) -> U21#(X1, X2, X3)) (U21#(active X1, X2, X3) -> U21#(X1, X2, X3), U21#(X1, X2, active X3) -> U21#(X1, X2, X3)) (U21#(active X1, X2, X3) -> U21#(X1, X2, X3), U21#(X1, mark X2, X3) -> U21#(X1, X2, X3)) (U21#(active X1, X2, X3) -> U21#(X1, X2, X3), U21#(X1, active X2, X3) -> U21#(X1, X2, X3)) (U21#(active X1, X2, X3) -> U21#(X1, X2, X3), U21#(mark X1, X2, X3) -> U21#(X1, X2, X3)) (U21#(active X1, X2, X3) -> U21#(X1, X2, X3), U21#(active X1, X2, X3) -> U21#(X1, X2, X3)) (U21#(X1, active X2, X3) -> U21#(X1, X2, X3), U21#(X1, X2, mark X3) -> U21#(X1, X2, X3)) (U21#(X1, active X2, X3) -> U21#(X1, X2, X3), U21#(X1, X2, active X3) -> U21#(X1, X2, X3)) (U21#(X1, active X2, X3) -> U21#(X1, X2, X3), U21#(X1, mark X2, X3) -> U21#(X1, X2, X3)) (U21#(X1, active X2, X3) -> U21#(X1, X2, X3), U21#(X1, active X2, X3) -> U21#(X1, X2, X3)) (U21#(X1, active X2, X3) -> U21#(X1, X2, X3), U21#(mark X1, X2, X3) -> U21#(X1, X2, X3)) (U21#(X1, active X2, X3) -> U21#(X1, X2, X3), U21#(active X1, X2, X3) -> U21#(X1, X2, X3)) (U21#(X1, X2, active X3) -> U21#(X1, X2, X3), U21#(X1, X2, mark X3) -> U21#(X1, X2, X3)) (U21#(X1, X2, active X3) -> U21#(X1, X2, X3), U21#(X1, X2, active X3) -> U21#(X1, X2, X3)) (U21#(X1, X2, active X3) -> U21#(X1, X2, X3), U21#(X1, mark X2, X3) -> U21#(X1, X2, X3)) (U21#(X1, X2, active X3) -> U21#(X1, X2, X3), U21#(X1, active X2, X3) -> U21#(X1, X2, X3)) (U21#(X1, X2, active X3) -> U21#(X1, X2, X3), U21#(mark X1, X2, X3) -> U21#(X1, X2, X3)) (U21#(X1, X2, active X3) -> U21#(X1, X2, X3), U21#(active X1, X2, X3) -> U21#(X1, X2, X3)) (U22#(active X1, X2, X3) -> U22#(X1, X2, X3), U22#(X1, X2, mark X3) -> U22#(X1, X2, X3)) (U22#(active X1, X2, X3) -> U22#(X1, X2, X3), U22#(X1, X2, active X3) -> U22#(X1, X2, X3)) (U22#(active X1, X2, X3) -> U22#(X1, X2, X3), U22#(X1, mark X2, X3) -> U22#(X1, X2, X3)) (U22#(active X1, X2, X3) -> U22#(X1, X2, X3), U22#(X1, active X2, X3) -> U22#(X1, X2, X3)) (U22#(active X1, X2, X3) -> U22#(X1, X2, X3), U22#(mark X1, X2, X3) -> U22#(X1, X2, X3)) (U22#(active X1, X2, X3) -> U22#(X1, X2, X3), U22#(active X1, X2, X3) -> U22#(X1, X2, X3)) (U22#(X1, active X2, X3) -> U22#(X1, X2, X3), U22#(X1, X2, mark X3) -> U22#(X1, X2, X3)) (U22#(X1, active X2, X3) -> U22#(X1, X2, X3), U22#(X1, X2, active X3) -> U22#(X1, X2, X3)) (U22#(X1, active X2, X3) -> U22#(X1, X2, X3), U22#(X1, mark X2, X3) -> U22#(X1, X2, X3)) (U22#(X1, active X2, X3) -> U22#(X1, X2, X3), U22#(X1, active X2, X3) -> U22#(X1, X2, X3)) (U22#(X1, active X2, X3) -> U22#(X1, X2, X3), U22#(mark X1, X2, X3) -> U22#(X1, X2, X3)) (U22#(X1, active X2, X3) -> U22#(X1, X2, X3), U22#(active X1, X2, X3) -> U22#(X1, X2, X3)) (U22#(X1, X2, active X3) -> U22#(X1, X2, X3), U22#(X1, X2, mark X3) -> U22#(X1, X2, X3)) (U22#(X1, X2, active X3) -> U22#(X1, X2, X3), U22#(X1, X2, active X3) -> U22#(X1, X2, X3)) (U22#(X1, X2, active X3) -> U22#(X1, X2, X3), U22#(X1, mark X2, X3) -> U22#(X1, X2, X3)) (U22#(X1, X2, active X3) -> U22#(X1, X2, X3), U22#(X1, active X2, X3) -> U22#(X1, X2, X3)) (U22#(X1, X2, active X3) -> U22#(X1, X2, X3), U22#(mark X1, X2, X3) -> U22#(X1, X2, X3)) (U22#(X1, X2, active X3) -> U22#(X1, X2, X3), U22#(active X1, X2, X3) -> U22#(X1, X2, X3)) (U11#(active X1, X2, X3) -> U11#(X1, X2, X3), U11#(X1, X2, mark X3) -> U11#(X1, X2, X3)) (U11#(active X1, X2, X3) -> U11#(X1, X2, X3), U11#(X1, X2, active X3) -> U11#(X1, X2, X3)) (U11#(active X1, X2, X3) -> U11#(X1, X2, X3), U11#(X1, mark X2, X3) -> U11#(X1, X2, X3)) (U11#(active X1, X2, X3) -> U11#(X1, X2, X3), U11#(X1, active X2, X3) -> U11#(X1, X2, X3)) (U11#(active X1, X2, X3) -> U11#(X1, X2, X3), U11#(mark X1, X2, X3) -> U11#(X1, X2, X3)) (U11#(active X1, X2, X3) -> U11#(X1, X2, X3), U11#(active X1, X2, X3) -> U11#(X1, X2, X3)) (U11#(X1, active X2, X3) -> U11#(X1, X2, X3), U11#(X1, X2, mark X3) -> U11#(X1, X2, X3)) (U11#(X1, active X2, X3) -> U11#(X1, X2, X3), U11#(X1, X2, active X3) -> U11#(X1, X2, X3)) (U11#(X1, active X2, X3) -> U11#(X1, X2, X3), U11#(X1, mark X2, X3) -> U11#(X1, X2, X3)) (U11#(X1, active X2, X3) -> U11#(X1, X2, X3), U11#(X1, active X2, X3) -> U11#(X1, X2, X3)) (U11#(X1, active X2, X3) -> U11#(X1, X2, X3), U11#(mark X1, X2, X3) -> U11#(X1, X2, X3)) (U11#(X1, active X2, X3) -> U11#(X1, X2, X3), U11#(active X1, X2, X3) -> U11#(X1, X2, X3)) (U11#(X1, X2, active X3) -> U11#(X1, X2, X3), U11#(X1, X2, mark X3) -> U11#(X1, X2, X3)) (U11#(X1, X2, active X3) -> U11#(X1, X2, X3), U11#(X1, X2, active X3) -> U11#(X1, X2, X3)) (U11#(X1, X2, active X3) -> U11#(X1, X2, X3), U11#(X1, mark X2, X3) -> U11#(X1, X2, X3)) (U11#(X1, X2, active X3) -> U11#(X1, X2, X3), U11#(X1, active X2, X3) -> U11#(X1, X2, X3)) (U11#(X1, X2, active X3) -> U11#(X1, X2, X3), U11#(mark X1, X2, X3) -> U11#(X1, X2, X3)) (U11#(X1, X2, active X3) -> U11#(X1, X2, X3), U11#(active X1, X2, X3) -> U11#(X1, X2, X3)) (U12#(active X1, X2, X3) -> U12#(X1, X2, X3), U12#(X1, X2, mark X3) -> U12#(X1, X2, X3)) (U12#(active X1, X2, X3) -> U12#(X1, X2, X3), U12#(X1, X2, active X3) -> U12#(X1, X2, X3)) (U12#(active X1, X2, X3) -> U12#(X1, X2, X3), U12#(X1, mark X2, X3) -> U12#(X1, X2, X3)) (U12#(active X1, X2, X3) -> U12#(X1, X2, X3), U12#(X1, active X2, X3) -> U12#(X1, X2, X3)) (U12#(active X1, X2, X3) -> U12#(X1, X2, X3), U12#(mark X1, X2, X3) -> U12#(X1, X2, X3)) (U12#(active X1, X2, X3) -> U12#(X1, X2, X3), U12#(active X1, X2, X3) -> U12#(X1, X2, X3)) (U12#(X1, active X2, X3) -> U12#(X1, X2, X3), U12#(X1, X2, mark X3) -> U12#(X1, X2, X3)) (U12#(X1, active X2, X3) -> U12#(X1, X2, X3), U12#(X1, X2, active X3) -> U12#(X1, X2, X3)) (U12#(X1, active X2, X3) -> U12#(X1, X2, X3), U12#(X1, mark X2, X3) -> U12#(X1, X2, X3)) (U12#(X1, active X2, X3) -> U12#(X1, X2, X3), U12#(X1, active X2, X3) -> U12#(X1, X2, X3)) (U12#(X1, active X2, X3) -> U12#(X1, X2, X3), U12#(mark X1, X2, X3) -> U12#(X1, X2, X3)) (U12#(X1, active X2, X3) -> U12#(X1, X2, X3), U12#(active X1, X2, X3) -> U12#(X1, X2, X3)) (U12#(X1, X2, active X3) -> U12#(X1, X2, X3), U12#(X1, X2, mark X3) -> U12#(X1, X2, X3)) (U12#(X1, X2, active X3) -> U12#(X1, X2, X3), U12#(X1, X2, active X3) -> U12#(X1, X2, X3)) (U12#(X1, X2, active X3) -> U12#(X1, X2, X3), U12#(X1, mark X2, X3) -> U12#(X1, X2, X3)) (U12#(X1, X2, active X3) -> U12#(X1, X2, X3), U12#(X1, active X2, X3) -> U12#(X1, X2, X3)) (U12#(X1, X2, active X3) -> U12#(X1, X2, X3), U12#(mark X1, X2, X3) -> U12#(X1, X2, X3)) (U12#(X1, X2, active X3) -> U12#(X1, X2, X3), U12#(active X1, X2, X3) -> U12#(X1, X2, X3)) (mark# U21(X1, X2, X3) -> U21#(mark X1, X2, X3), U21#(X1, X2, mark X3) -> U21#(X1, X2, X3)) (mark# U21(X1, X2, X3) -> U21#(mark X1, X2, X3), U21#(X1, X2, active X3) -> U21#(X1, X2, X3)) (mark# U21(X1, X2, X3) -> U21#(mark X1, X2, X3), U21#(X1, mark X2, X3) -> U21#(X1, X2, X3)) (mark# U21(X1, X2, X3) -> U21#(mark X1, X2, X3), U21#(X1, active X2, X3) -> U21#(X1, X2, X3)) (mark# U21(X1, X2, X3) -> U21#(mark X1, X2, X3), U21#(mark X1, X2, X3) -> U21#(X1, X2, X3)) (mark# U21(X1, X2, X3) -> U21#(mark X1, X2, X3), U21#(active X1, X2, X3) -> U21#(X1, X2, X3)) (mark# U11(X1, X2, X3) -> U11#(mark X1, X2, X3), U11#(X1, X2, mark X3) -> U11#(X1, X2, X3)) (mark# U11(X1, X2, X3) -> U11#(mark X1, X2, X3), U11#(X1, X2, active X3) -> U11#(X1, X2, X3)) (mark# U11(X1, X2, X3) -> U11#(mark X1, X2, X3), U11#(X1, mark X2, X3) -> U11#(X1, X2, X3)) (mark# U11(X1, X2, X3) -> U11#(mark X1, X2, X3), U11#(X1, active X2, X3) -> U11#(X1, X2, X3)) (mark# U11(X1, X2, X3) -> U11#(mark X1, X2, X3), U11#(mark X1, X2, X3) -> U11#(X1, X2, X3)) (mark# U11(X1, X2, X3) -> U11#(mark X1, X2, X3), U11#(active X1, X2, X3) -> U11#(X1, X2, X3)) (s# active X -> s# X, s# mark X -> s# X) (s# active X -> s# X, s# active X -> s# X) (mark# s X -> mark# X, mark# U12(X1, X2, X3) -> mark# X1) (mark# s X -> mark# X, mark# U12(X1, X2, X3) -> U12#(mark X1, X2, X3)) (mark# s X -> mark# X, mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3)) (mark# s X -> mark# X, mark# tt() -> active# tt()) (mark# s X -> mark# X, mark# U11(X1, X2, X3) -> mark# X1) (mark# s X -> mark# X, mark# U11(X1, X2, X3) -> active# U11(mark X1, X2, X3)) (mark# s X -> mark# X, mark# U11(X1, X2, X3) -> U11#(mark X1, X2, X3)) (mark# s X -> mark# X, mark# s X -> mark# X) (mark# s X -> mark# X, mark# s X -> active# s mark X) (mark# s X -> mark# X, mark# s X -> s# mark 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) -> active# plus(mark X1, mark X2)) (mark# s X -> mark# X, mark# plus(X1, X2) -> plus#(mark X1, mark X2)) (mark# s X -> mark# X, mark# U22(X1, X2, X3) -> mark# X1) (mark# s X -> mark# X, mark# U22(X1, X2, X3) -> active# U22(mark X1, X2, X3)) (mark# s X -> mark# X, mark# U22(X1, X2, X3) -> U22#(mark X1, X2, X3)) (mark# s X -> mark# X, mark# U21(X1, X2, X3) -> mark# X1) (mark# s X -> mark# X, mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3)) (mark# s X -> mark# X, mark# U21(X1, X2, X3) -> U21#(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) -> active# x(mark X1, mark X2)) (mark# s X -> mark# X, mark# x(X1, X2) -> x#(mark X1, mark X2)) (mark# s X -> mark# X, mark# 0() -> active# 0()) } STATUS: arrows: 0.906489 SCCS (8): Scc: { mark# U12(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3), mark# U11(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> active# U11(mark X1, X2, X3), mark# s X -> mark# X, mark# plus(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X2, mark# plus(X1, X2) -> active# plus(mark X1, mark X2), mark# U22(X1, X2, X3) -> mark# X1, mark# U22(X1, X2, X3) -> active# U22(mark X1, X2, X3), mark# U21(X1, X2, X3) -> mark# X1, mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3), mark# x(X1, X2) -> mark# X1, mark# x(X1, X2) -> mark# X2, mark# x(X1, X2) -> active# x(mark X1, mark X2), active# U12(tt(), M, N) -> mark# s plus(N, M), active# U11(tt(), M, N) -> mark# U12(tt(), M, N), active# plus(N, s M) -> mark# U11(tt(), M, N), active# plus(N, 0()) -> mark# N, active# U22(tt(), M, N) -> mark# plus(x(N, M), N), active# U21(tt(), M, N) -> mark# U22(tt(), M, N), active# x(N, s M) -> mark# U21(tt(), M, N)} Scc: { U21#(X1, X2, mark X3) -> U21#(X1, X2, X3), U21#(X1, X2, active X3) -> U21#(X1, X2, X3), U21#(X1, mark X2, X3) -> U21#(X1, X2, X3), U21#(X1, active X2, X3) -> U21#(X1, X2, X3), U21#(mark X1, X2, X3) -> U21#(X1, X2, X3), U21#(active X1, X2, X3) -> U21#(X1, X2, X3)} Scc: { U22#(X1, X2, mark X3) -> U22#(X1, X2, X3), U22#(X1, X2, active X3) -> U22#(X1, X2, X3), U22#(X1, mark X2, X3) -> U22#(X1, X2, X3), U22#(X1, active X2, X3) -> U22#(X1, X2, X3), U22#(mark X1, X2, X3) -> U22#(X1, X2, X3), U22#(active X1, X2, X3) -> U22#(X1, X2, X3)} Scc: { x#(X1, mark X2) -> x#(X1, X2), x#(X1, active X2) -> x#(X1, X2), x#(mark X1, X2) -> x#(X1, X2), x#(active X1, X2) -> x#(X1, X2)} Scc: { U11#(X1, X2, mark X3) -> U11#(X1, X2, X3), U11#(X1, X2, active X3) -> U11#(X1, X2, X3), U11#(X1, mark X2, X3) -> U11#(X1, X2, X3), U11#(X1, active X2, X3) -> U11#(X1, X2, X3), U11#(mark X1, X2, X3) -> U11#(X1, X2, X3), U11#(active X1, X2, X3) -> U11#(X1, X2, X3)} Scc: { plus#(X1, mark X2) -> plus#(X1, X2), plus#(X1, active X2) -> plus#(X1, X2), plus#(mark X1, X2) -> plus#(X1, X2), plus#(active X1, X2) -> plus#(X1, X2)} Scc: { s# mark X -> s# X, s# active X -> s# X} Scc: { U12#(X1, X2, mark X3) -> U12#(X1, X2, X3), U12#(X1, X2, active X3) -> U12#(X1, X2, X3), U12#(X1, mark X2, X3) -> U12#(X1, X2, X3), U12#(X1, active X2, X3) -> U12#(X1, X2, X3), U12#(mark X1, X2, X3) -> U12#(X1, X2, X3), U12#(active X1, X2, X3) -> U12#(X1, X2, X3)} SCC (22): Strict: { mark# U12(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3), mark# U11(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> active# U11(mark X1, X2, X3), mark# s X -> mark# X, mark# plus(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X2, mark# plus(X1, X2) -> active# plus(mark X1, mark X2), mark# U22(X1, X2, X3) -> mark# X1, mark# U22(X1, X2, X3) -> active# U22(mark X1, X2, X3), mark# U21(X1, X2, X3) -> mark# X1, mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3), mark# x(X1, X2) -> mark# X1, mark# x(X1, X2) -> mark# X2, mark# x(X1, X2) -> active# x(mark X1, mark X2), active# U12(tt(), M, N) -> mark# s plus(N, M), active# U11(tt(), M, N) -> mark# U12(tt(), M, N), active# plus(N, s M) -> mark# U11(tt(), M, N), active# plus(N, 0()) -> mark# N, active# U22(tt(), M, N) -> mark# plus(x(N, M), N), active# U21(tt(), M, N) -> mark# U22(tt(), M, N), active# x(N, s M) -> mark# U21(tt(), M, N)} Weak: { mark U12(X1, X2, X3) -> active U12(mark X1, X2, X3), mark tt() -> active tt(), mark U11(X1, X2, X3) -> active U11(mark X1, X2, X3), mark s X -> active s mark X, mark plus(X1, X2) -> active plus(mark X1, mark X2), mark U22(X1, X2, X3) -> active U22(mark X1, X2, X3), mark U21(X1, X2, X3) -> active U21(mark X1, X2, X3), mark x(X1, X2) -> active x(mark X1, mark X2), mark 0() -> active 0(), U12(X1, X2, mark X3) -> U12(X1, X2, X3), U12(X1, X2, active X3) -> U12(X1, X2, X3), U12(X1, mark X2, X3) -> U12(X1, X2, X3), U12(X1, active X2, X3) -> U12(X1, X2, X3), U12(mark X1, X2, X3) -> U12(X1, X2, X3), U12(active X1, X2, X3) -> U12(X1, X2, X3), active U12(tt(), M, N) -> mark s plus(N, M), active U11(tt(), M, N) -> mark U12(tt(), M, N), active plus(N, s M) -> mark U11(tt(), M, N), active plus(N, 0()) -> mark N, active U22(tt(), M, N) -> mark plus(x(N, M), N), active U21(tt(), M, N) -> mark U22(tt(), M, N), active x(N, s M) -> mark U21(tt(), M, N), active x(N, 0()) -> mark 0(), U11(X1, X2, mark X3) -> U11(X1, X2, X3), U11(X1, X2, active X3) -> U11(X1, X2, X3), U11(X1, mark X2, X3) -> U11(X1, X2, X3), U11(X1, active X2, X3) -> U11(X1, X2, X3), U11(mark X1, X2, X3) -> U11(X1, X2, X3), U11(active X1, X2, X3) -> U11(X1, X2, X3), s mark X -> s X, s active X -> s X, plus(X1, mark X2) -> plus(X1, X2), plus(X1, active X2) -> plus(X1, X2), plus(mark X1, X2) -> plus(X1, X2), plus(active X1, X2) -> plus(X1, X2), U22(X1, X2, mark X3) -> U22(X1, X2, X3), U22(X1, X2, active X3) -> U22(X1, X2, X3), U22(X1, mark X2, X3) -> U22(X1, X2, X3), U22(X1, active X2, X3) -> U22(X1, X2, X3), U22(mark X1, X2, X3) -> U22(X1, X2, X3), U22(active X1, X2, X3) -> U22(X1, X2, X3), U21(X1, X2, mark X3) -> U21(X1, X2, X3), U21(X1, X2, active X3) -> U21(X1, X2, X3), U21(X1, mark X2, X3) -> U21(X1, X2, X3), U21(X1, active X2, X3) -> U21(X1, X2, X3), U21(mark X1, X2, X3) -> U21(X1, X2, X3), U21(active X1, X2, X3) -> U21(X1, X2, X3), x(X1, mark X2) -> x(X1, X2), x(X1, active X2) -> x(X1, X2), x(mark X1, X2) -> x(X1, X2), x(active X1, X2) -> x(X1, X2)} Open SCC (6): Strict: { U21#(X1, X2, mark X3) -> U21#(X1, X2, X3), U21#(X1, X2, active X3) -> U21#(X1, X2, X3), U21#(X1, mark X2, X3) -> U21#(X1, X2, X3), U21#(X1, active X2, X3) -> U21#(X1, X2, X3), U21#(mark X1, X2, X3) -> U21#(X1, X2, X3), U21#(active X1, X2, X3) -> U21#(X1, X2, X3)} Weak: { mark U12(X1, X2, X3) -> active U12(mark X1, X2, X3), mark tt() -> active tt(), mark U11(X1, X2, X3) -> active U11(mark X1, X2, X3), mark s X -> active s mark X, mark plus(X1, X2) -> active plus(mark X1, mark X2), mark U22(X1, X2, X3) -> active U22(mark X1, X2, X3), mark U21(X1, X2, X3) -> active U21(mark X1, X2, X3), mark x(X1, X2) -> active x(mark X1, mark X2), mark 0() -> active 0(), U12(X1, X2, mark X3) -> U12(X1, X2, X3), U12(X1, X2, active X3) -> U12(X1, X2, X3), U12(X1, mark X2, X3) -> U12(X1, X2, X3), U12(X1, active X2, X3) -> U12(X1, X2, X3), U12(mark X1, X2, X3) -> U12(X1, X2, X3), U12(active X1, X2, X3) -> U12(X1, X2, X3), active U12(tt(), M, N) -> mark s plus(N, M), active U11(tt(), M, N) -> mark U12(tt(), M, N), active plus(N, s M) -> mark U11(tt(), M, N), active plus(N, 0()) -> mark N, active U22(tt(), M, N) -> mark plus(x(N, M), N), active U21(tt(), M, N) -> mark U22(tt(), M, N), active x(N, s M) -> mark U21(tt(), M, N), active x(N, 0()) -> mark 0(), U11(X1, X2, mark X3) -> U11(X1, X2, X3), U11(X1, X2, active X3) -> U11(X1, X2, X3), U11(X1, mark X2, X3) -> U11(X1, X2, X3), U11(X1, active X2, X3) -> U11(X1, X2, X3), U11(mark X1, X2, X3) -> U11(X1, X2, X3), U11(active X1, X2, X3) -> U11(X1, X2, X3), s mark X -> s X, s active X -> s X, plus(X1, mark X2) -> plus(X1, X2), plus(X1, active X2) -> plus(X1, X2), plus(mark X1, X2) -> plus(X1, X2), plus(active X1, X2) -> plus(X1, X2), U22(X1, X2, mark X3) -> U22(X1, X2, X3), U22(X1, X2, active X3) -> U22(X1, X2, X3), U22(X1, mark X2, X3) -> U22(X1, X2, X3), U22(X1, active X2, X3) -> U22(X1, X2, X3), U22(mark X1, X2, X3) -> U22(X1, X2, X3), U22(active X1, X2, X3) -> U22(X1, X2, X3), U21(X1, X2, mark X3) -> U21(X1, X2, X3), U21(X1, X2, active X3) -> U21(X1, X2, X3), U21(X1, mark X2, X3) -> U21(X1, X2, X3), U21(X1, active X2, X3) -> U21(X1, X2, X3), U21(mark X1, X2, X3) -> U21(X1, X2, X3), U21(active X1, X2, X3) -> U21(X1, X2, X3), x(X1, mark X2) -> x(X1, X2), x(X1, active X2) -> x(X1, X2), x(mark X1, X2) -> x(X1, X2), x(active X1, X2) -> x(X1, X2)} Open SCC (6): Strict: { U22#(X1, X2, mark X3) -> U22#(X1, X2, X3), U22#(X1, X2, active X3) -> U22#(X1, X2, X3), U22#(X1, mark X2, X3) -> U22#(X1, X2, X3), U22#(X1, active X2, X3) -> U22#(X1, X2, X3), U22#(mark X1, X2, X3) -> U22#(X1, X2, X3), U22#(active X1, X2, X3) -> U22#(X1, X2, X3)} Weak: { mark U12(X1, X2, X3) -> active U12(mark X1, X2, X3), mark tt() -> active tt(), mark U11(X1, X2, X3) -> active U11(mark X1, X2, X3), mark s X -> active s mark X, mark plus(X1, X2) -> active plus(mark X1, mark X2), mark U22(X1, X2, X3) -> active U22(mark X1, X2, X3), mark U21(X1, X2, X3) -> active U21(mark X1, X2, X3), mark x(X1, X2) -> active x(mark X1, mark X2), mark 0() -> active 0(), U12(X1, X2, mark X3) -> U12(X1, X2, X3), U12(X1, X2, active X3) -> U12(X1, X2, X3), U12(X1, mark X2, X3) -> U12(X1, X2, X3), U12(X1, active X2, X3) -> U12(X1, X2, X3), U12(mark X1, X2, X3) -> U12(X1, X2, X3), U12(active X1, X2, X3) -> U12(X1, X2, X3), active U12(tt(), M, N) -> mark s plus(N, M), active U11(tt(), M, N) -> mark U12(tt(), M, N), active plus(N, s M) -> mark U11(tt(), M, N), active plus(N, 0()) -> mark N, active U22(tt(), M, N) -> mark plus(x(N, M), N), active U21(tt(), M, N) -> mark U22(tt(), M, N), active x(N, s M) -> mark U21(tt(), M, N), active x(N, 0()) -> mark 0(), U11(X1, X2, mark X3) -> U11(X1, X2, X3), U11(X1, X2, active X3) -> U11(X1, X2, X3), U11(X1, mark X2, X3) -> U11(X1, X2, X3), U11(X1, active X2, X3) -> U11(X1, X2, X3), U11(mark X1, X2, X3) -> U11(X1, X2, X3), U11(active X1, X2, X3) -> U11(X1, X2, X3), s mark X -> s X, s active X -> s X, plus(X1, mark X2) -> plus(X1, X2), plus(X1, active X2) -> plus(X1, X2), plus(mark X1, X2) -> plus(X1, X2), plus(active X1, X2) -> plus(X1, X2), U22(X1, X2, mark X3) -> U22(X1, X2, X3), U22(X1, X2, active X3) -> U22(X1, X2, X3), U22(X1, mark X2, X3) -> U22(X1, X2, X3), U22(X1, active X2, X3) -> U22(X1, X2, X3), U22(mark X1, X2, X3) -> U22(X1, X2, X3), U22(active X1, X2, X3) -> U22(X1, X2, X3), U21(X1, X2, mark X3) -> U21(X1, X2, X3), U21(X1, X2, active X3) -> U21(X1, X2, X3), U21(X1, mark X2, X3) -> U21(X1, X2, X3), U21(X1, active X2, X3) -> U21(X1, X2, X3), U21(mark X1, X2, X3) -> U21(X1, X2, X3), U21(active X1, X2, X3) -> U21(X1, X2, X3), x(X1, mark X2) -> x(X1, X2), x(X1, active X2) -> x(X1, X2), x(mark X1, X2) -> x(X1, X2), x(active X1, X2) -> x(X1, X2)} Open SCC (4): Strict: { x#(X1, mark X2) -> x#(X1, X2), x#(X1, active X2) -> x#(X1, X2), x#(mark X1, X2) -> x#(X1, X2), x#(active X1, X2) -> x#(X1, X2)} Weak: { mark U12(X1, X2, X3) -> active U12(mark X1, X2, X3), mark tt() -> active tt(), mark U11(X1, X2, X3) -> active U11(mark X1, X2, X3), mark s X -> active s mark X, mark plus(X1, X2) -> active plus(mark X1, mark X2), mark U22(X1, X2, X3) -> active U22(mark X1, X2, X3), mark U21(X1, X2, X3) -> active U21(mark X1, X2, X3), mark x(X1, X2) -> active x(mark X1, mark X2), mark 0() -> active 0(), U12(X1, X2, mark X3) -> U12(X1, X2, X3), U12(X1, X2, active X3) -> U12(X1, X2, X3), U12(X1, mark X2, X3) -> U12(X1, X2, X3), U12(X1, active X2, X3) -> U12(X1, X2, X3), U12(mark X1, X2, X3) -> U12(X1, X2, X3), U12(active X1, X2, X3) -> U12(X1, X2, X3), active U12(tt(), M, N) -> mark s plus(N, M), active U11(tt(), M, N) -> mark U12(tt(), M, N), active plus(N, s M) -> mark U11(tt(), M, N), active plus(N, 0()) -> mark N, active U22(tt(), M, N) -> mark plus(x(N, M), N), active U21(tt(), M, N) -> mark U22(tt(), M, N), active x(N, s M) -> mark U21(tt(), M, N), active x(N, 0()) -> mark 0(), U11(X1, X2, mark X3) -> U11(X1, X2, X3), U11(X1, X2, active X3) -> U11(X1, X2, X3), U11(X1, mark X2, X3) -> U11(X1, X2, X3), U11(X1, active X2, X3) -> U11(X1, X2, X3), U11(mark X1, X2, X3) -> U11(X1, X2, X3), U11(active X1, X2, X3) -> U11(X1, X2, X3), s mark X -> s X, s active X -> s X, plus(X1, mark X2) -> plus(X1, X2), plus(X1, active X2) -> plus(X1, X2), plus(mark X1, X2) -> plus(X1, X2), plus(active X1, X2) -> plus(X1, X2), U22(X1, X2, mark X3) -> U22(X1, X2, X3), U22(X1, X2, active X3) -> U22(X1, X2, X3), U22(X1, mark X2, X3) -> U22(X1, X2, X3), U22(X1, active X2, X3) -> U22(X1, X2, X3), U22(mark X1, X2, X3) -> U22(X1, X2, X3), U22(active X1, X2, X3) -> U22(X1, X2, X3), U21(X1, X2, mark X3) -> U21(X1, X2, X3), U21(X1, X2, active X3) -> U21(X1, X2, X3), U21(X1, mark X2, X3) -> U21(X1, X2, X3), U21(X1, active X2, X3) -> U21(X1, X2, X3), U21(mark X1, X2, X3) -> U21(X1, X2, X3), U21(active X1, X2, X3) -> U21(X1, X2, X3), x(X1, mark X2) -> x(X1, X2), x(X1, active X2) -> x(X1, X2), x(mark X1, X2) -> x(X1, X2), x(active X1, X2) -> x(X1, X2)} Open SCC (6): Strict: { U11#(X1, X2, mark X3) -> U11#(X1, X2, X3), U11#(X1, X2, active X3) -> U11#(X1, X2, X3), U11#(X1, mark X2, X3) -> U11#(X1, X2, X3), U11#(X1, active X2, X3) -> U11#(X1, X2, X3), U11#(mark X1, X2, X3) -> U11#(X1, X2, X3), U11#(active X1, X2, X3) -> U11#(X1, X2, X3)} Weak: { mark U12(X1, X2, X3) -> active U12(mark X1, X2, X3), mark tt() -> active tt(), mark U11(X1, X2, X3) -> active U11(mark X1, X2, X3), mark s X -> active s mark X, mark plus(X1, X2) -> active plus(mark X1, mark X2), mark U22(X1, X2, X3) -> active U22(mark X1, X2, X3), mark U21(X1, X2, X3) -> active U21(mark X1, X2, X3), mark x(X1, X2) -> active x(mark X1, mark X2), mark 0() -> active 0(), U12(X1, X2, mark X3) -> U12(X1, X2, X3), U12(X1, X2, active X3) -> U12(X1, X2, X3), U12(X1, mark X2, X3) -> U12(X1, X2, X3), U12(X1, active X2, X3) -> U12(X1, X2, X3), U12(mark X1, X2, X3) -> U12(X1, X2, X3), U12(active X1, X2, X3) -> U12(X1, X2, X3), active U12(tt(), M, N) -> mark s plus(N, M), active U11(tt(), M, N) -> mark U12(tt(), M, N), active plus(N, s M) -> mark U11(tt(), M, N), active plus(N, 0()) -> mark N, active U22(tt(), M, N) -> mark plus(x(N, M), N), active U21(tt(), M, N) -> mark U22(tt(), M, N), active x(N, s M) -> mark U21(tt(), M, N), active x(N, 0()) -> mark 0(), U11(X1, X2, mark X3) -> U11(X1, X2, X3), U11(X1, X2, active X3) -> U11(X1, X2, X3), U11(X1, mark X2, X3) -> U11(X1, X2, X3), U11(X1, active X2, X3) -> U11(X1, X2, X3), U11(mark X1, X2, X3) -> U11(X1, X2, X3), U11(active X1, X2, X3) -> U11(X1, X2, X3), s mark X -> s X, s active X -> s X, plus(X1, mark X2) -> plus(X1, X2), plus(X1, active X2) -> plus(X1, X2), plus(mark X1, X2) -> plus(X1, X2), plus(active X1, X2) -> plus(X1, X2), U22(X1, X2, mark X3) -> U22(X1, X2, X3), U22(X1, X2, active X3) -> U22(X1, X2, X3), U22(X1, mark X2, X3) -> U22(X1, X2, X3), U22(X1, active X2, X3) -> U22(X1, X2, X3), U22(mark X1, X2, X3) -> U22(X1, X2, X3), U22(active X1, X2, X3) -> U22(X1, X2, X3), U21(X1, X2, mark X3) -> U21(X1, X2, X3), U21(X1, X2, active X3) -> U21(X1, X2, X3), U21(X1, mark X2, X3) -> U21(X1, X2, X3), U21(X1, active X2, X3) -> U21(X1, X2, X3), U21(mark X1, X2, X3) -> U21(X1, X2, X3), U21(active X1, X2, X3) -> U21(X1, X2, X3), x(X1, mark X2) -> x(X1, X2), x(X1, active X2) -> x(X1, X2), x(mark X1, X2) -> x(X1, X2), x(active X1, X2) -> x(X1, X2)} Open SCC (4): Strict: { plus#(X1, mark X2) -> plus#(X1, X2), plus#(X1, active X2) -> plus#(X1, X2), plus#(mark X1, X2) -> plus#(X1, X2), plus#(active X1, X2) -> plus#(X1, X2)} Weak: { mark U12(X1, X2, X3) -> active U12(mark X1, X2, X3), mark tt() -> active tt(), mark U11(X1, X2, X3) -> active U11(mark X1, X2, X3), mark s X -> active s mark X, mark plus(X1, X2) -> active plus(mark X1, mark X2), mark U22(X1, X2, X3) -> active U22(mark X1, X2, X3), mark U21(X1, X2, X3) -> active U21(mark X1, X2, X3), mark x(X1, X2) -> active x(mark X1, mark X2), mark 0() -> active 0(), U12(X1, X2, mark X3) -> U12(X1, X2, X3), U12(X1, X2, active X3) -> U12(X1, X2, X3), U12(X1, mark X2, X3) -> U12(X1, X2, X3), U12(X1, active X2, X3) -> U12(X1, X2, X3), U12(mark X1, X2, X3) -> U12(X1, X2, X3), U12(active X1, X2, X3) -> U12(X1, X2, X3), active U12(tt(), M, N) -> mark s plus(N, M), active U11(tt(), M, N) -> mark U12(tt(), M, N), active plus(N, s M) -> mark U11(tt(), M, N), active plus(N, 0()) -> mark N, active U22(tt(), M, N) -> mark plus(x(N, M), N), active U21(tt(), M, N) -> mark U22(tt(), M, N), active x(N, s M) -> mark U21(tt(), M, N), active x(N, 0()) -> mark 0(), U11(X1, X2, mark X3) -> U11(X1, X2, X3), U11(X1, X2, active X3) -> U11(X1, X2, X3), U11(X1, mark X2, X3) -> U11(X1, X2, X3), U11(X1, active X2, X3) -> U11(X1, X2, X3), U11(mark X1, X2, X3) -> U11(X1, X2, X3), U11(active X1, X2, X3) -> U11(X1, X2, X3), s mark X -> s X, s active X -> s X, plus(X1, mark X2) -> plus(X1, X2), plus(X1, active X2) -> plus(X1, X2), plus(mark X1, X2) -> plus(X1, X2), plus(active X1, X2) -> plus(X1, X2), U22(X1, X2, mark X3) -> U22(X1, X2, X3), U22(X1, X2, active X3) -> U22(X1, X2, X3), U22(X1, mark X2, X3) -> U22(X1, X2, X3), U22(X1, active X2, X3) -> U22(X1, X2, X3), U22(mark X1, X2, X3) -> U22(X1, X2, X3), U22(active X1, X2, X3) -> U22(X1, X2, X3), U21(X1, X2, mark X3) -> U21(X1, X2, X3), U21(X1, X2, active X3) -> U21(X1, X2, X3), U21(X1, mark X2, X3) -> U21(X1, X2, X3), U21(X1, active X2, X3) -> U21(X1, X2, X3), U21(mark X1, X2, X3) -> U21(X1, X2, X3), U21(active X1, X2, X3) -> U21(X1, X2, X3), x(X1, mark X2) -> x(X1, X2), x(X1, active X2) -> x(X1, X2), x(mark X1, X2) -> x(X1, X2), x(active X1, X2) -> x(X1, X2)} Open SCC (2): Strict: { s# mark X -> s# X, s# active X -> s# X} Weak: { mark U12(X1, X2, X3) -> active U12(mark X1, X2, X3), mark tt() -> active tt(), mark U11(X1, X2, X3) -> active U11(mark X1, X2, X3), mark s X -> active s mark X, mark plus(X1, X2) -> active plus(mark X1, mark X2), mark U22(X1, X2, X3) -> active U22(mark X1, X2, X3), mark U21(X1, X2, X3) -> active U21(mark X1, X2, X3), mark x(X1, X2) -> active x(mark X1, mark X2), mark 0() -> active 0(), U12(X1, X2, mark X3) -> U12(X1, X2, X3), U12(X1, X2, active X3) -> U12(X1, X2, X3), U12(X1, mark X2, X3) -> U12(X1, X2, X3), U12(X1, active X2, X3) -> U12(X1, X2, X3), U12(mark X1, X2, X3) -> U12(X1, X2, X3), U12(active X1, X2, X3) -> U12(X1, X2, X3), active U12(tt(), M, N) -> mark s plus(N, M), active U11(tt(), M, N) -> mark U12(tt(), M, N), active plus(N, s M) -> mark U11(tt(), M, N), active plus(N, 0()) -> mark N, active U22(tt(), M, N) -> mark plus(x(N, M), N), active U21(tt(), M, N) -> mark U22(tt(), M, N), active x(N, s M) -> mark U21(tt(), M, N), active x(N, 0()) -> mark 0(), U11(X1, X2, mark X3) -> U11(X1, X2, X3), U11(X1, X2, active X3) -> U11(X1, X2, X3), U11(X1, mark X2, X3) -> U11(X1, X2, X3), U11(X1, active X2, X3) -> U11(X1, X2, X3), U11(mark X1, X2, X3) -> U11(X1, X2, X3), U11(active X1, X2, X3) -> U11(X1, X2, X3), s mark X -> s X, s active X -> s X, plus(X1, mark X2) -> plus(X1, X2), plus(X1, active X2) -> plus(X1, X2), plus(mark X1, X2) -> plus(X1, X2), plus(active X1, X2) -> plus(X1, X2), U22(X1, X2, mark X3) -> U22(X1, X2, X3), U22(X1, X2, active X3) -> U22(X1, X2, X3), U22(X1, mark X2, X3) -> U22(X1, X2, X3), U22(X1, active X2, X3) -> U22(X1, X2, X3), U22(mark X1, X2, X3) -> U22(X1, X2, X3), U22(active X1, X2, X3) -> U22(X1, X2, X3), U21(X1, X2, mark X3) -> U21(X1, X2, X3), U21(X1, X2, active X3) -> U21(X1, X2, X3), U21(X1, mark X2, X3) -> U21(X1, X2, X3), U21(X1, active X2, X3) -> U21(X1, X2, X3), U21(mark X1, X2, X3) -> U21(X1, X2, X3), U21(active X1, X2, X3) -> U21(X1, X2, X3), x(X1, mark X2) -> x(X1, X2), x(X1, active X2) -> x(X1, X2), x(mark X1, X2) -> x(X1, X2), x(active X1, X2) -> x(X1, X2)} Open SCC (6): Strict: { U12#(X1, X2, mark X3) -> U12#(X1, X2, X3), U12#(X1, X2, active X3) -> U12#(X1, X2, X3), U12#(X1, mark X2, X3) -> U12#(X1, X2, X3), U12#(X1, active X2, X3) -> U12#(X1, X2, X3), U12#(mark X1, X2, X3) -> U12#(X1, X2, X3), U12#(active X1, X2, X3) -> U12#(X1, X2, X3)} Weak: { mark U12(X1, X2, X3) -> active U12(mark X1, X2, X3), mark tt() -> active tt(), mark U11(X1, X2, X3) -> active U11(mark X1, X2, X3), mark s X -> active s mark X, mark plus(X1, X2) -> active plus(mark X1, mark X2), mark U22(X1, X2, X3) -> active U22(mark X1, X2, X3), mark U21(X1, X2, X3) -> active U21(mark X1, X2, X3), mark x(X1, X2) -> active x(mark X1, mark X2), mark 0() -> active 0(), U12(X1, X2, mark X3) -> U12(X1, X2, X3), U12(X1, X2, active X3) -> U12(X1, X2, X3), U12(X1, mark X2, X3) -> U12(X1, X2, X3), U12(X1, active X2, X3) -> U12(X1, X2, X3), U12(mark X1, X2, X3) -> U12(X1, X2, X3), U12(active X1, X2, X3) -> U12(X1, X2, X3), active U12(tt(), M, N) -> mark s plus(N, M), active U11(tt(), M, N) -> mark U12(tt(), M, N), active plus(N, s M) -> mark U11(tt(), M, N), active plus(N, 0()) -> mark N, active U22(tt(), M, N) -> mark plus(x(N, M), N), active U21(tt(), M, N) -> mark U22(tt(), M, N), active x(N, s M) -> mark U21(tt(), M, N), active x(N, 0()) -> mark 0(), U11(X1, X2, mark X3) -> U11(X1, X2, X3), U11(X1, X2, active X3) -> U11(X1, X2, X3), U11(X1, mark X2, X3) -> U11(X1, X2, X3), U11(X1, active X2, X3) -> U11(X1, X2, X3), U11(mark X1, X2, X3) -> U11(X1, X2, X3), U11(active X1, X2, X3) -> U11(X1, X2, X3), s mark X -> s X, s active X -> s X, plus(X1, mark X2) -> plus(X1, X2), plus(X1, active X2) -> plus(X1, X2), plus(mark X1, X2) -> plus(X1, X2), plus(active X1, X2) -> plus(X1, X2), U22(X1, X2, mark X3) -> U22(X1, X2, X3), U22(X1, X2, active X3) -> U22(X1, X2, X3), U22(X1, mark X2, X3) -> U22(X1, X2, X3), U22(X1, active X2, X3) -> U22(X1, X2, X3), U22(mark X1, X2, X3) -> U22(X1, X2, X3), U22(active X1, X2, X3) -> U22(X1, X2, X3), U21(X1, X2, mark X3) -> U21(X1, X2, X3), U21(X1, X2, active X3) -> U21(X1, X2, X3), U21(X1, mark X2, X3) -> U21(X1, X2, X3), U21(X1, active X2, X3) -> U21(X1, X2, X3), U21(mark X1, X2, X3) -> U21(X1, X2, X3), U21(active X1, X2, X3) -> U21(X1, X2, X3), x(X1, mark X2) -> x(X1, X2), x(X1, active X2) -> x(X1, X2), x(mark X1, X2) -> x(X1, X2), x(active X1, X2) -> x(X1, X2)} Open