YES Time: 0.658217 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 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, 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)} 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# 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, 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)} 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 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, 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)} EDG: { (s# mark X -> s# X, s# active X -> s# X) (s# mark X -> s# X, 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)) (active# plus(N, 0()) -> mark# N, mark# 0() -> active# 0()) (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) (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)) (mark# s X -> s# mark X, s# active X -> s# X) (mark# s X -> s# mark X, s# mark X -> s# X) (mark# U11(X1, X2, X3) -> mark# X1, mark# 0() -> active# 0()) (mark# U11(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> plus#(mark X1, 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) -> mark# X2) (mark# U11(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# U11(X1, X2, X3) -> mark# X1, mark# s X -> s# 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 -> mark# X) (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# U11(X1, X2, X3) -> active# U11(mark X1, X2, X3)) (mark# U11(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> mark# X1) (mark# U11(X1, X2, X3) -> mark# X1, mark# tt() -> active# tt()) (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# U12(X1, X2, X3) -> U12#(mark X1, X2, X3)) (mark# U11(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> mark# X1) (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)) (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)) (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) (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)) (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)) (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# 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)) (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)) (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) (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)) (mark# plus(X1, X2) -> mark# X1, mark# U12(X1, X2, X3) -> mark# X1) (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) -> active# U12(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X1, mark# tt() -> active# tt()) (mark# plus(X1, X2) -> mark# X1, mark# U11(X1, X2, X3) -> mark# X1) (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) -> U11#(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# plus(X1, X2) -> mark# X1, mark# s X -> active# s mark X) (mark# plus(X1, X2) -> mark# X1, mark# s X -> s# mark X) (mark# plus(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# plus(X1, X2) -> mark# X1, mark# plus(X1, X2) -> active# plus(mark X1, mark X2)) (mark# plus(X1, X2) -> mark# X1, mark# plus(X1, X2) -> plus#(mark X1, mark X2)) (mark# plus(X1, X2) -> mark# X1, mark# 0() -> active# 0()) (mark# U12(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> mark# X1) (mark# U12(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> U12#(mark X1, X2, X3)) (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# tt() -> active# tt()) (mark# U12(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> mark# X1) (mark# U12(X1, X2, X3) -> mark# X1, mark# U11(X1, X2, X3) -> active# U11(mark X1, X2, X3)) (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# s X -> 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 -> s# mark X) (mark# U12(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> mark# X1) (mark# U12(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> mark# X2) (mark# U12(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> active# plus(mark X1, mark X2)) (mark# U12(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> plus#(mark X1, mark X2)) (mark# U12(X1, X2, X3) -> mark# X1, mark# 0() -> active# 0()) (mark# plus(X1, X2) -> active# plus(mark X1, 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) -> s# plus(N, M)) (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# U11(tt(), M, N) -> mark# U12(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# plus(N, s M) -> mark# U11(tt(), M, 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, 0()) -> mark# N) (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)) (active# U12(tt(), M, N) -> s# plus(N, M), s# mark X -> s# X) (active# U12(tt(), M, N) -> s# plus(N, M), s# active X -> s# X) (mark# plus(X1, X2) -> mark# X2, mark# U12(X1, X2, X3) -> mark# X1) (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) -> active# U12(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X2, mark# tt() -> active# tt()) (mark# plus(X1, X2) -> mark# X2, mark# U11(X1, X2, X3) -> mark# X1) (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) -> U11#(mark X1, X2, X3)) (mark# plus(X1, X2) -> mark# X2, mark# s X -> mark# X) (mark# plus(X1, X2) -> mark# X2, mark# s X -> active# s mark X) (mark# plus(X1, X2) -> mark# X2, mark# s X -> s# mark X) (mark# plus(X1, X2) -> mark# X2, mark# plus(X1, X2) -> mark# X1) (mark# plus(X1, X2) -> mark# X2, mark# plus(X1, X2) -> mark# X2) (mark# plus(X1, X2) -> mark# X2, mark# plus(X1, X2) -> active# plus(mark X1, mark X2)) (mark# plus(X1, X2) -> mark# X2, mark# plus(X1, X2) -> plus#(mark X1, mark X2)) (mark# plus(X1, X2) -> mark# X2, mark# 0() -> active# 0()) (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# 0() -> active# 0()) } STATUS: arrows: 0.842356 SCCS (5): 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# s X -> active# 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), 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} 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: { 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: { 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 (13): 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# s X -> active# 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), 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} 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 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, 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)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [U12](x0, x1, x2) = x0 + x1 + x2, [U11](x0, x1, x2) = x0 + x1 + x2, [plus](x0, x1) = x0 + x1, [mark](x0) = x0, [active](x0) = x0, [s](x0) = x0 + 1, [tt] = 1, [0] = 0, [mark#](x0) = x0, [active#](x0) = x0 Strict: active# plus(N, 0()) -> mark# N 0 + 1N >= 0 + 1N active# plus(N, s M) -> mark# U11(tt(), M, N) 1 + 1M + 1N >= 1 + 1M + 1N active# U11(tt(), M, N) -> mark# U12(tt(), M, N) 1 + 1M + 1N >= 1 + 1M + 1N active# U12(tt(), M, N) -> mark# s plus(N, M) 1 + 1M + 1N >= 1 + 1M + 1N mark# plus(X1, X2) -> active# plus(mark X1, mark X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 mark# plus(X1, X2) -> mark# X2 0 + 1X1 + 1X2 >= 0 + 1X2 mark# plus(X1, X2) -> mark# X1 0 + 1X1 + 1X2 >= 0 + 1X1 mark# s X -> active# s mark X 1 + 1X >= 1 + 1X mark# s X -> mark# X 1 + 1X >= 0 + 1X mark# U11(X1, X2, X3) -> active# U11(mark X1, X2, X3) 0 + 1X1 + 1X2 + 1X3 >= 0 + 1X1 + 1X2 + 1X3 mark# U11(X1, X2, X3) -> mark# X1 0 + 1X1 + 1X2 + 1X3 >= 0 + 1X1 mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3) 0 + 1X1 + 1X2 + 1X3 >= 0 + 1X1 + 1X2 + 1X3 mark# U12(X1, X2, X3) -> mark# X1 0 + 1X1 + 1X2 + 1X3 >= 0 + 1X1 Weak: plus(active X1, X2) -> plus(X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 plus(mark X1, X2) -> plus(X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 plus(X1, active X2) -> plus(X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 plus(X1, mark X2) -> plus(X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 s active X -> s X 1 + 1X >= 1 + 1X s mark X -> s X 1 + 1X >= 1 + 1X U11(active X1, X2, X3) -> U11(X1, X2, X3) 0 + 1X1 + 1X2 + 1X3 >= 0 + 1X1 + 1X2 + 1X3 U11(mark X1, X2, X3) -> U11(X1, X2, X3) 0 + 1X1 + 1X2 + 1X3 >= 0 + 1X1 + 1X2 + 1X3 U11(X1, active X2, X3) -> U11(X1, X2, X3) 0 + 1X1 + 1X2 + 1X3 >= 0 + 1X1 + 1X2 + 1X3 U11(X1, mark X2, X3) -> U11(X1, X2, X3) 0 + 1X1 + 1X2 + 1X3 >= 0 + 1X1 + 1X2 + 1X3 U11(X1, X2, active X3) -> U11(X1, X2, X3) 0 + 1X1 + 1X2 + 1X3 >= 0 + 1X1 + 1X2 + 1X3 U11(X1, X2, mark X3) -> U11(X1, X2, X3) 0 + 1X1 + 1X2 + 1X3 >= 0 + 1X1 + 1X2 + 1X3 active plus(N, 0()) -> mark N 0 + 1N >= 0 + 1N active plus(N, s M) -> mark U11(tt(), M, N) 1 + 1M + 1N >= 1 + 1M + 1N active U11(tt(), M, N) -> mark U12(tt(), M, N) 1 + 1M + 1N >= 1 + 1M + 1N active U12(tt(), M, N) -> mark s plus(N, M) 1 + 1M + 1N >= 1 + 1M + 1N U12(active X1, X2, X3) -> U12(X1, X2, X3) 0 + 1X1 + 1X2 + 1X3 >= 0 + 1X1 + 1X2 + 1X3 U12(mark X1, X2, X3) -> U12(X1, X2, X3) 0 + 1X1 + 1X2 + 1X3 >= 0 + 1X1 + 1X2 + 1X3 U12(X1, active X2, X3) -> U12(X1, X2, X3) 0 + 1X1 + 1X2 + 1X3 >= 0 + 1X1 + 1X2 + 1X3 U12(X1, mark X2, X3) -> U12(X1, X2, X3) 0 + 1X1 + 1X2 + 1X3 >= 0 + 1X1 + 1X2 + 1X3 U12(X1, X2, active X3) -> U12(X1, X2, X3) 0 + 1X1 + 1X2 + 1X3 >= 0 + 1X1 + 1X2 + 1X3 U12(X1, X2, mark X3) -> U12(X1, X2, X3) 0 + 1X1 + 1X2 + 1X3 >= 0 + 1X1 + 1X2 + 1X3 mark 0() -> active 0() 0 >= 0 mark plus(X1, X2) -> active plus(mark X1, mark X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 mark s X -> active s mark X 1 + 1X >= 1 + 1X mark U11(X1, X2, X3) -> active U11(mark X1, X2, X3) 0 + 1X1 + 1X2 + 1X3 >= 0 + 1X1 + 1X2 + 1X3 mark tt() -> active tt() 1 >= 1 mark U12(X1, X2, X3) -> active U12(mark X1, X2, X3) 0 + 1X1 + 1X2 + 1X3 >= 0 + 1X1 + 1X2 + 1X3 SCCS (1): 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 -> active# 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), 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} SCC (12): 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 -> active# 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), 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} 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 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, 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)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [U12](x0, x1, x2) = x0, [U11](x0, x1, x2) = x0, [plus](x0, x1) = x0 + x1 + 1, [mark](x0) = x0, [active](x0) = x0, [s](x0) = 1, [tt] = 1, [0] = 1, [mark#](x0) = x0, [active#](x0) = x0 Strict: active# plus(N, 0()) -> mark# N 2 + 1N >= 0 + 1N active# plus(N, s M) -> mark# U11(tt(), M, N) 2 + 0M + 1N >= 1 + 0M + 0N active# U11(tt(), M, N) -> mark# U12(tt(), M, N) 1 + 0M + 0N >= 1 + 0M + 0N active# U12(tt(), M, N) -> mark# s plus(N, M) 1 + 0M + 0N >= 1 + 0M + 0N mark# plus(X1, X2) -> active# plus(mark X1, mark X2) 1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2 mark# plus(X1, X2) -> mark# X2 1 + 1X1 + 1X2 >= 0 + 1X2 mark# plus(X1, X2) -> mark# X1 1 + 1X1 + 1X2 >= 0 + 1X1 mark# s X -> active# s mark X 1 + 0X >= 1 + 0X mark# U11(X1, X2, X3) -> active# U11(mark X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 mark# U11(X1, X2, X3) -> mark# X1 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 mark# U12(X1, X2, X3) -> mark# X1 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 Weak: plus(active X1, X2) -> plus(X1, X2) 1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2 plus(mark X1, X2) -> plus(X1, X2) 1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2 plus(X1, active X2) -> plus(X1, X2) 1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2 plus(X1, mark X2) -> plus(X1, X2) 1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2 s active X -> s X 1 + 0X >= 1 + 0X s mark X -> s X 1 + 0X >= 1 + 0X U11(active X1, X2, X3) -> U11(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 U11(mark X1, X2, X3) -> U11(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 U11(X1, active X2, X3) -> U11(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 U11(X1, mark X2, X3) -> U11(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 U11(X1, X2, active X3) -> U11(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 U11(X1, X2, mark X3) -> U11(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 active plus(N, 0()) -> mark N 2 + 1N >= 0 + 1N active plus(N, s M) -> mark U11(tt(), M, N) 2 + 0M + 1N >= 1 + 0M + 0N active U11(tt(), M, N) -> mark U12(tt(), M, N) 1 + 0M + 0N >= 1 + 0M + 0N active U12(tt(), M, N) -> mark s plus(N, M) 1 + 0M + 0N >= 1 + 0M + 0N U12(active X1, X2, X3) -> U12(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 U12(mark X1, X2, X3) -> U12(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 U12(X1, active X2, X3) -> U12(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 U12(X1, mark X2, X3) -> U12(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 U12(X1, X2, active X3) -> U12(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 U12(X1, X2, mark X3) -> U12(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 mark 0() -> active 0() 1 >= 1 mark plus(X1, X2) -> active plus(mark X1, mark X2) 1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2 mark s X -> active s mark X 1 + 0X >= 1 + 0X mark U11(X1, X2, X3) -> active U11(mark X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 mark tt() -> active tt() 1 >= 1 mark U12(X1, X2, X3) -> active U12(mark X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 SCCS (1): 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 -> active# s mark X, mark# plus(X1, X2) -> active# plus(mark X1, mark X2), active# U12(tt(), M, N) -> mark# s plus(N, M), active# U11(tt(), M, N) -> mark# U12(tt(), M, N)} SCC (8): 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 -> active# s mark X, mark# plus(X1, X2) -> active# plus(mark X1, mark X2), active# U12(tt(), M, N) -> mark# s plus(N, M), active# U11(tt(), M, N) -> mark# U12(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 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, 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)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [U12](x0, x1, x2) = 1, [U11](x0, x1, x2) = 1, [plus](x0, x1) = 0, [mark](x0) = x0 + 1, [active](x0) = 0, [s](x0) = 1, [tt] = 1, [0] = 1, [mark#](x0) = 1, [active#](x0) = x0 Strict: active# U11(tt(), M, N) -> mark# U12(tt(), M, N) 1 + 0M + 0N >= 1 + 0M + 0N active# U12(tt(), M, N) -> mark# s plus(N, M) 1 + 0M + 0N >= 1 + 0M + 0N mark# plus(X1, X2) -> active# plus(mark X1, mark X2) 1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 mark# s X -> active# s mark X 1 + 0X >= 1 + 0X mark# U11(X1, X2, X3) -> active# U11(mark X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 mark# U11(X1, X2, X3) -> mark# X1 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 mark# U12(X1, X2, X3) -> mark# X1 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 Weak: plus(active X1, X2) -> plus(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 plus(mark X1, X2) -> plus(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 plus(X1, active X2) -> plus(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 plus(X1, mark X2) -> plus(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 s active X -> s X 1 + 0X >= 1 + 0X s mark X -> s X 1 + 0X >= 1 + 0X U11(active X1, X2, X3) -> U11(X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 U11(mark X1, X2, X3) -> U11(X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 U11(X1, active X2, X3) -> U11(X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 U11(X1, mark X2, X3) -> U11(X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 U11(X1, X2, active X3) -> U11(X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 U11(X1, X2, mark X3) -> U11(X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 active plus(N, 0()) -> mark N 0 + 0N >= 1 + 1N active plus(N, s M) -> mark U11(tt(), M, N) 0 + 0M + 0N >= 2 + 0M + 0N active U11(tt(), M, N) -> mark U12(tt(), M, N) 0 + 0M + 0N >= 2 + 0M + 0N active U12(tt(), M, N) -> mark s plus(N, M) 0 + 0M + 0N >= 2 + 0M + 0N U12(active X1, X2, X3) -> U12(X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 U12(mark X1, X2, X3) -> U12(X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 U12(X1, active X2, X3) -> U12(X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 U12(X1, mark X2, X3) -> U12(X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 U12(X1, X2, active X3) -> U12(X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 U12(X1, X2, mark X3) -> U12(X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 mark 0() -> active 0() 2 >= 0 mark plus(X1, X2) -> active plus(mark X1, mark X2) 1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 mark s X -> active s mark X 2 + 0X >= 0 + 0X mark U11(X1, X2, X3) -> active U11(mark X1, X2, X3) 2 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 mark tt() -> active tt() 2 >= 0 mark U12(X1, X2, X3) -> active U12(mark X1, X2, X3) 2 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 SCCS (1): 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 -> active# s mark X, active# U12(tt(), M, N) -> mark# s plus(N, M), active# U11(tt(), M, N) -> mark# U12(tt(), M, N)} SCC (7): 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 -> active# s mark X, active# U12(tt(), M, N) -> mark# s plus(N, M), active# U11(tt(), M, N) -> mark# U12(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 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, 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)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [U12](x0, x1, x2) = x0, [U11](x0, x1, x2) = x0 + x1 + 1, [plus](x0, x1) = x0 + x1, [mark](x0) = x0 + 1, [active](x0) = x0, [s](x0) = 0, [tt] = 0, [0] = 0, [mark#](x0) = x0, [active#](x0) = 0 Strict: active# U11(tt(), M, N) -> mark# U12(tt(), M, N) 0 + 0M + 0N >= 0 + 0M + 0N active# U12(tt(), M, N) -> mark# s plus(N, M) 0 + 0M + 0N >= 0 + 0M + 0N mark# s X -> active# s mark X 0 + 0X >= 0 + 0X mark# U11(X1, X2, X3) -> active# U11(mark X1, X2, X3) 1 + 1X1 + 0X2 + 1X3 >= 0 + 0X1 + 0X2 + 0X3 mark# U11(X1, X2, X3) -> mark# X1 1 + 1X1 + 0X2 + 1X3 >= 0 + 1X1 mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 mark# U12(X1, X2, X3) -> mark# X1 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 Weak: plus(active X1, X2) -> plus(X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 plus(mark X1, X2) -> plus(X1, X2) 1 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 plus(X1, active X2) -> plus(X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 plus(X1, mark X2) -> plus(X1, X2) 1 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 s active X -> s X 0 + 0X >= 0 + 0X s mark X -> s X 0 + 0X >= 0 + 0X U11(active X1, X2, X3) -> U11(X1, X2, X3) 1 + 1X1 + 0X2 + 1X3 >= 1 + 1X1 + 0X2 + 1X3 U11(mark X1, X2, X3) -> U11(X1, X2, X3) 2 + 1X1 + 0X2 + 1X3 >= 1 + 1X1 + 0X2 + 1X3 U11(X1, active X2, X3) -> U11(X1, X2, X3) 1 + 1X1 + 0X2 + 1X3 >= 1 + 1X1 + 0X2 + 1X3 U11(X1, mark X2, X3) -> U11(X1, X2, X3) 1 + 1X1 + 0X2 + 1X3 >= 1 + 1X1 + 0X2 + 1X3 U11(X1, X2, active X3) -> U11(X1, X2, X3) 1 + 1X1 + 0X2 + 1X3 >= 1 + 1X1 + 0X2 + 1X3 U11(X1, X2, mark X3) -> U11(X1, X2, X3) 2 + 1X1 + 0X2 + 1X3 >= 1 + 1X1 + 0X2 + 1X3 active plus(N, 0()) -> mark N 0 + 1N >= 1 + 1N active plus(N, s M) -> mark U11(tt(), M, N) 0 + 0M + 1N >= 2 + 0M + 1N active U11(tt(), M, N) -> mark U12(tt(), M, N) 1 + 0M + 1N >= 1 + 0M + 0N active U12(tt(), M, N) -> mark s plus(N, M) 0 + 0M + 0N >= 1 + 0M + 0N U12(active X1, X2, X3) -> U12(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 U12(mark X1, X2, X3) -> U12(X1, X2, X3) 1 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 U12(X1, active X2, X3) -> U12(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 U12(X1, mark X2, X3) -> U12(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 U12(X1, X2, active X3) -> U12(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 U12(X1, X2, mark X3) -> U12(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 mark 0() -> active 0() 1 >= 0 mark plus(X1, X2) -> active plus(mark X1, mark X2) 1 + 1X1 + 1X2 >= 2 + 1X1 + 1X2 mark s X -> active s mark X 1 + 0X >= 0 + 0X mark U11(X1, X2, X3) -> active U11(mark X1, X2, X3) 2 + 1X1 + 0X2 + 1X3 >= 2 + 1X1 + 0X2 + 1X3 mark tt() -> active tt() 1 >= 0 mark U12(X1, X2, X3) -> active U12(mark X1, X2, X3) 1 + 1X1 + 0X2 + 0X3 >= 1 + 1X1 + 0X2 + 0X3 SCCS (1): Scc: { mark# U12(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3), mark# s X -> active# s mark X, active# U12(tt(), M, N) -> mark# s plus(N, M), active# U11(tt(), M, N) -> mark# U12(tt(), M, N)} SCC (5): Strict: { mark# U12(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3), mark# s X -> active# s mark X, active# U12(tt(), M, N) -> mark# s plus(N, M), active# U11(tt(), M, N) -> mark# U12(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 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, 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)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [U12](x0, x1, x2) = x0, [U11](x0, x1, x2) = x0, [plus](x0, x1) = x0 + x1 + 1, [mark](x0) = x0, [active](x0) = x0, [s](x0) = 0, [tt] = 1, [0] = 1, [mark#](x0) = x0, [active#](x0) = x0 Strict: active# U11(tt(), M, N) -> mark# U12(tt(), M, N) 1 + 0M + 0N >= 1 + 0M + 0N active# U12(tt(), M, N) -> mark# s plus(N, M) 1 + 0M + 0N >= 0 + 0M + 0N mark# s X -> active# s mark X 0 + 0X >= 0 + 0X mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 mark# U12(X1, X2, X3) -> mark# X1 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 Weak: plus(active X1, X2) -> plus(X1, X2) 1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2 plus(mark X1, X2) -> plus(X1, X2) 1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2 plus(X1, active X2) -> plus(X1, X2) 1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2 plus(X1, mark X2) -> plus(X1, X2) 1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2 s active X -> s X 0 + 0X >= 0 + 0X s mark X -> s X 0 + 0X >= 0 + 0X U11(active X1, X2, X3) -> U11(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 U11(mark X1, X2, X3) -> U11(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 U11(X1, active X2, X3) -> U11(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 U11(X1, mark X2, X3) -> U11(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 U11(X1, X2, active X3) -> U11(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 U11(X1, X2, mark X3) -> U11(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 active plus(N, 0()) -> mark N 2 + 1N >= 0 + 1N active plus(N, s M) -> mark U11(tt(), M, N) 1 + 0M + 1N >= 1 + 0M + 0N active U11(tt(), M, N) -> mark U12(tt(), M, N) 1 + 0M + 0N >= 1 + 0M + 0N active U12(tt(), M, N) -> mark s plus(N, M) 1 + 0M + 0N >= 0 + 0M + 0N U12(active X1, X2, X3) -> U12(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 U12(mark X1, X2, X3) -> U12(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 U12(X1, active X2, X3) -> U12(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 U12(X1, mark X2, X3) -> U12(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 U12(X1, X2, active X3) -> U12(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 U12(X1, X2, mark X3) -> U12(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 mark 0() -> active 0() 1 >= 1 mark plus(X1, X2) -> active plus(mark X1, mark X2) 1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2 mark s X -> active s mark X 0 + 0X >= 0 + 0X mark U11(X1, X2, X3) -> active U11(mark X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 mark tt() -> active tt() 1 >= 1 mark U12(X1, X2, X3) -> active U12(mark X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 SCCS (1): Scc: { mark# U12(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3), mark# s X -> active# s mark X, active# U11(tt(), M, N) -> mark# U12(tt(), M, N)} SCC (4): Strict: { mark# U12(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3), mark# s X -> active# s mark X, active# U11(tt(), M, N) -> mark# U12(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 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, 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)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [U12](x0, x1, x2) = x0, [U11](x0, x1, x2) = 0, [plus](x0, x1) = 0, [mark](x0) = x0, [active](x0) = x0, [s](x0) = 1, [tt] = 0, [0] = 0, [mark#](x0) = x0, [active#](x0) = 0 Strict: active# U11(tt(), M, N) -> mark# U12(tt(), M, N) 0 + 0M + 0N >= 0 + 0M + 0N mark# s X -> active# s mark X 1 + 0X >= 0 + 0X mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 mark# U12(X1, X2, X3) -> mark# X1 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 Weak: plus(active X1, X2) -> plus(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 plus(mark X1, X2) -> plus(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 plus(X1, active X2) -> plus(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 plus(X1, mark X2) -> plus(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 s active X -> s X 1 + 0X >= 1 + 0X s mark X -> s X 1 + 0X >= 1 + 0X U11(active X1, X2, X3) -> U11(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U11(mark X1, X2, X3) -> U11(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U11(X1, active X2, X3) -> U11(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U11(X1, mark X2, X3) -> U11(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U11(X1, X2, active X3) -> U11(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U11(X1, X2, mark X3) -> U11(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 active plus(N, 0()) -> mark N 0 + 0N >= 0 + 1N active plus(N, s M) -> mark U11(tt(), M, N) 0 + 0M + 0N >= 0 + 0M + 0N active U11(tt(), M, N) -> mark U12(tt(), M, N) 0 + 0M + 0N >= 0 + 0M + 0N active U12(tt(), M, N) -> mark s plus(N, M) 0 + 0M + 0N >= 1 + 0M + 0N U12(active X1, X2, X3) -> U12(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 U12(mark X1, X2, X3) -> U12(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 U12(X1, active X2, X3) -> U12(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 U12(X1, mark X2, X3) -> U12(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 U12(X1, X2, active X3) -> U12(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 U12(X1, X2, mark X3) -> U12(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 mark 0() -> active 0() 0 >= 0 mark plus(X1, X2) -> active plus(mark X1, mark X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 mark s X -> active s mark X 1 + 0X >= 1 + 0X mark U11(X1, X2, X3) -> active U11(mark X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 mark tt() -> active tt() 0 >= 0 mark U12(X1, X2, X3) -> active U12(mark X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 SCCS (1): Scc: { mark# U12(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3), active# U11(tt(), M, N) -> mark# U12(tt(), M, N)} SCC (3): Strict: { mark# U12(X1, X2, X3) -> mark# X1, mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3), active# U11(tt(), M, N) -> mark# U12(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 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, 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)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [U12](x0, x1, x2) = 0, [U11](x0, x1, x2) = x0, [plus](x0, x1) = 0, [mark](x0) = 0, [active](x0) = 0, [s](x0) = 0, [tt] = 1, [0] = 0, [mark#](x0) = 0, [active#](x0) = x0 Strict: active# U11(tt(), M, N) -> mark# U12(tt(), M, N) 1 + 0M + 0N >= 0 + 0M + 0N mark# U12(X1, X2, X3) -> active# U12(mark X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 mark# U12(X1, X2, X3) -> mark# X1 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 Weak: plus(active X1, X2) -> plus(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 plus(mark X1, X2) -> plus(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 plus(X1, active X2) -> plus(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 plus(X1, mark X2) -> plus(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 s active X -> s X 0 + 0X >= 0 + 0X s mark X -> s X 0 + 0X >= 0 + 0X U11(active X1, X2, X3) -> U11(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 U11(mark X1, X2, X3) -> U11(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 U11(X1, active X2, X3) -> U11(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 U11(X1, mark X2, X3) -> U11(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 U11(X1, X2, active X3) -> U11(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 U11(X1, X2, mark X3) -> U11(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 active plus(N, 0()) -> mark N 0 + 0N >= 0 + 0N active plus(N, s M) -> mark U11(tt(), M, N) 0 + 0M + 0N >= 0 + 0M + 0N active U11(tt(), M, N) -> mark U12(tt(), M, N) 0 + 0M + 0N >= 0 + 0M + 0N active U12(tt(), M, N) -> mark s plus(N, M) 0 + 0M + 0N >= 0 + 0M + 0N U12(active X1, X2, X3) -> U12(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U12(mark X1, X2, X3) -> U12(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U12(X1, active X2, X3) -> U12(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U12(X1, mark X2, X3) -> U12(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U12(X1, X2, active X3) -> U12(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U12(X1, X2, mark X3) -> U12(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 mark 0() -> active 0() 0 >= 0 mark plus(X1, X2) -> active plus(mark X1, mark X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 mark s X -> active s mark X 0 + 0X >= 0 + 0X mark U11(X1, X2, X3) -> active U11(mark X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 mark tt() -> active tt() 0 >= 0 mark U12(X1, X2, X3) -> active U12(mark X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 SCCS (1): Scc: {mark# U12(X1, X2, X3) -> mark# X1} SCC (1): Strict: {mark# U12(X1, X2, X3) -> mark# X1} 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 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, 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)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [U12](x0, x1, x2) = x0 + x1 + x2 + 1, [U11](x0, x1, x2) = x0 + x1 + x2 + 1, [plus](x0, x1) = x0 + 1, [mark](x0) = x0 + 1, [active](x0) = x0, [s](x0) = x0 + 1, [tt] = 1, [0] = 1, [mark#](x0) = x0 Strict: mark# U12(X1, X2, X3) -> mark# X1 1 + 1X1 + 1X2 + 1X3 >= 0 + 1X1 Weak: plus(active X1, X2) -> plus(X1, X2) 1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2 plus(mark X1, X2) -> plus(X1, X2) 1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2 plus(X1, active X2) -> plus(X1, X2) 1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2 plus(X1, mark X2) -> plus(X1, X2) 2 + 0X1 + 1X2 >= 1 + 0X1 + 1X2 s active X -> s X 1 + 1X >= 1 + 1X s mark X -> s X 2 + 1X >= 1 + 1X U11(active X1, X2, X3) -> U11(X1, X2, X3) 1 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U11(mark X1, X2, X3) -> U11(X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U11(X1, active X2, X3) -> U11(X1, X2, X3) 1 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U11(X1, mark X2, X3) -> U11(X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U11(X1, X2, active X3) -> U11(X1, X2, X3) 1 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U11(X1, X2, mark X3) -> U11(X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 active plus(N, 0()) -> mark N 2 + 0N >= 1 + 1N active plus(N, s M) -> mark U11(tt(), M, N) 2 + 1M + 0N >= 3 + 1M + 1N active U11(tt(), M, N) -> mark U12(tt(), M, N) 2 + 1M + 1N >= 3 + 1M + 1N active U12(tt(), M, N) -> mark s plus(N, M) 2 + 1M + 1N >= 3 + 1M + 0N U12(active X1, X2, X3) -> U12(X1, X2, X3) 1 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U12(mark X1, X2, X3) -> U12(X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U12(X1, active X2, X3) -> U12(X1, X2, X3) 1 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U12(X1, mark X2, X3) -> U12(X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U12(X1, X2, active X3) -> U12(X1, X2, X3) 1 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U12(X1, X2, mark X3) -> U12(X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 mark 0() -> active 0() 2 >= 1 mark plus(X1, X2) -> active plus(mark X1, mark X2) 2 + 0X1 + 1X2 >= 2 + 0X1 + 1X2 mark s X -> active s mark X 2 + 1X >= 2 + 1X mark U11(X1, X2, X3) -> active U11(mark X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 2 + 1X1 + 1X2 + 1X3 mark tt() -> active tt() 2 >= 1 mark U12(X1, X2, X3) -> active U12(mark X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 2 + 1X1 + 1X2 + 1X3 Qed 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 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, 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)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [U12](x0, x1, x2) = 0, [U11](x0, x1, x2) = 0, [plus](x0, x1) = 0, [mark](x0) = x0, [active](x0) = x0 + 1, [s](x0) = 0, [tt] = 0, [0] = 0, [plus#](x0, x1) = x0 Strict: plus#(active X1, X2) -> plus#(X1, X2) 1 + 1X1 + 0X2 >= 0 + 1X1 + 0X2 plus#(mark X1, X2) -> plus#(X1, X2) 0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2 plus#(X1, active X2) -> plus#(X1, X2) 0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2 plus#(X1, mark X2) -> plus#(X1, X2) 0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2 Weak: plus(active X1, X2) -> plus(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 plus(mark X1, X2) -> plus(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 plus(X1, active X2) -> plus(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 plus(X1, mark X2) -> plus(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 s active X -> s X 0 + 0X >= 0 + 0X s mark X -> s X 0 + 0X >= 0 + 0X U11(active X1, X2, X3) -> U11(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U11(mark X1, X2, X3) -> U11(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U11(X1, active X2, X3) -> U11(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U11(X1, mark X2, X3) -> U11(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U11(X1, X2, active X3) -> U11(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U11(X1, X2, mark X3) -> U11(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 active plus(N, 0()) -> mark N 1 + 0N >= 0 + 1N active plus(N, s M) -> mark U11(tt(), M, N) 1 + 0M + 0N >= 0 + 0M + 0N active U11(tt(), M, N) -> mark U12(tt(), M, N) 1 + 0M + 0N >= 0 + 0M + 0N active U12(tt(), M, N) -> mark s plus(N, M) 1 + 0M + 0N >= 0 + 0M + 0N U12(active X1, X2, X3) -> U12(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U12(mark X1, X2, X3) -> U12(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U12(X1, active X2, X3) -> U12(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U12(X1, mark X2, X3) -> U12(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U12(X1, X2, active X3) -> U12(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U12(X1, X2, mark X3) -> U12(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 mark 0() -> active 0() 0 >= 1 mark plus(X1, X2) -> active plus(mark X1, mark X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 mark s X -> active s mark X 0 + 0X >= 1 + 0X mark U11(X1, X2, X3) -> active U11(mark X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 mark tt() -> active tt() 0 >= 1 mark U12(X1, X2, X3) -> active U12(mark X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 SCCS (1): Scc: { plus#(X1, mark X2) -> plus#(X1, X2), plus#(X1, active X2) -> plus#(X1, X2), plus#(mark X1, X2) -> plus#(X1, X2)} SCC (3): Strict: { plus#(X1, mark X2) -> plus#(X1, X2), plus#(X1, active X2) -> plus#(X1, X2), plus#(mark 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 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, 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)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [U12](x0, x1, x2) = x0 + x1 + x2 + 1, [U11](x0, x1, x2) = x0 + x1 + x2 + 1, [plus](x0, x1) = x0 + x1, [mark](x0) = x0 + 1, [active](x0) = x0, [s](x0) = x0 + 1, [tt] = 1, [0] = 1, [plus#](x0, x1) = x0 Strict: plus#(mark X1, X2) -> plus#(X1, X2) 1 + 1X1 + 0X2 >= 0 + 1X1 + 0X2 plus#(X1, active X2) -> plus#(X1, X2) 0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2 plus#(X1, mark X2) -> plus#(X1, X2) 0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2 Weak: plus(active X1, X2) -> plus(X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 plus(mark X1, X2) -> plus(X1, X2) 1 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 plus(X1, active X2) -> plus(X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 plus(X1, mark X2) -> plus(X1, X2) 1 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 s active X -> s X 1 + 1X >= 1 + 1X s mark X -> s X 2 + 1X >= 1 + 1X U11(active X1, X2, X3) -> U11(X1, X2, X3) 1 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U11(mark X1, X2, X3) -> U11(X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U11(X1, active X2, X3) -> U11(X1, X2, X3) 1 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U11(X1, mark X2, X3) -> U11(X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U11(X1, X2, active X3) -> U11(X1, X2, X3) 1 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U11(X1, X2, mark X3) -> U11(X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 active plus(N, 0()) -> mark N 1 + 1N >= 1 + 1N active plus(N, s M) -> mark U11(tt(), M, N) 1 + 1M + 1N >= 3 + 1M + 1N active U11(tt(), M, N) -> mark U12(tt(), M, N) 2 + 1M + 1N >= 3 + 1M + 1N active U12(tt(), M, N) -> mark s plus(N, M) 2 + 1M + 1N >= 2 + 1M + 1N U12(active X1, X2, X3) -> U12(X1, X2, X3) 1 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U12(mark X1, X2, X3) -> U12(X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U12(X1, active X2, X3) -> U12(X1, X2, X3) 1 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U12(X1, mark X2, X3) -> U12(X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U12(X1, X2, active X3) -> U12(X1, X2, X3) 1 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U12(X1, X2, mark X3) -> U12(X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 mark 0() -> active 0() 2 >= 1 mark plus(X1, X2) -> active plus(mark X1, mark X2) 1 + 1X1 + 1X2 >= 2 + 1X1 + 1X2 mark s X -> active s mark X 2 + 1X >= 2 + 1X mark U11(X1, X2, X3) -> active U11(mark X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 2 + 1X1 + 1X2 + 1X3 mark tt() -> active tt() 2 >= 1 mark U12(X1, X2, X3) -> active U12(mark X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 2 + 1X1 + 1X2 + 1X3 SCCS (1): Scc: { plus#(X1, mark X2) -> plus#(X1, X2), plus#(X1, active X2) -> plus#(X1, X2)} SCC (2): Strict: { plus#(X1, mark X2) -> plus#(X1, X2), plus#(X1, active 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 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, 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)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [U12](x0, x1, x2) = 0, [U11](x0, x1, x2) = 0, [plus](x0, x1) = 0, [mark](x0) = x0, [active](x0) = x0 + 1, [s](x0) = 0, [tt] = 0, [0] = 0, [plus#](x0, x1) = x0 Strict: plus#(X1, active X2) -> plus#(X1, X2) 1 + 0X1 + 1X2 >= 0 + 0X1 + 1X2 plus#(X1, mark X2) -> plus#(X1, X2) 0 + 0X1 + 1X2 >= 0 + 0X1 + 1X2 Weak: plus(active X1, X2) -> plus(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 plus(mark X1, X2) -> plus(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 plus(X1, active X2) -> plus(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 plus(X1, mark X2) -> plus(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 s active X -> s X 0 + 0X >= 0 + 0X s mark X -> s X 0 + 0X >= 0 + 0X U11(active X1, X2, X3) -> U11(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U11(mark X1, X2, X3) -> U11(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U11(X1, active X2, X3) -> U11(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U11(X1, mark X2, X3) -> U11(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U11(X1, X2, active X3) -> U11(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U11(X1, X2, mark X3) -> U11(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 active plus(N, 0()) -> mark N 1 + 0N >= 0 + 1N active plus(N, s M) -> mark U11(tt(), M, N) 1 + 0M + 0N >= 0 + 0M + 0N active U11(tt(), M, N) -> mark U12(tt(), M, N) 1 + 0M + 0N >= 0 + 0M + 0N active U12(tt(), M, N) -> mark s plus(N, M) 1 + 0M + 0N >= 0 + 0M + 0N U12(active X1, X2, X3) -> U12(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U12(mark X1, X2, X3) -> U12(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U12(X1, active X2, X3) -> U12(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U12(X1, mark X2, X3) -> U12(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U12(X1, X2, active X3) -> U12(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U12(X1, X2, mark X3) -> U12(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 mark 0() -> active 0() 0 >= 1 mark plus(X1, X2) -> active plus(mark X1, mark X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 mark s X -> active s mark X 0 + 0X >= 1 + 0X mark U11(X1, X2, X3) -> active U11(mark X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 mark tt() -> active tt() 0 >= 1 mark U12(X1, X2, X3) -> active U12(mark X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 SCCS (1): Scc: {plus#(X1, mark X2) -> plus#(X1, X2)} SCC (1): Strict: {plus#(X1, mark 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 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, 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)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [U12](x0, x1, x2) = x0 + x1 + x2 + 1, [U11](x0, x1, x2) = x0 + x1 + 1, [plus](x0, x1) = x0 + 1, [mark](x0) = x0 + 1, [active](x0) = x0, [s](x0) = x0 + 1, [tt] = 1, [0] = 1, [plus#](x0, x1) = x0 Strict: plus#(X1, mark X2) -> plus#(X1, X2) 1 + 0X1 + 1X2 >= 0 + 0X1 + 1X2 Weak: plus(active X1, X2) -> plus(X1, X2) 1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2 plus(mark X1, X2) -> plus(X1, X2) 1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2 plus(X1, active X2) -> plus(X1, X2) 1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2 plus(X1, mark X2) -> plus(X1, X2) 2 + 0X1 + 1X2 >= 1 + 0X1 + 1X2 s active X -> s X 1 + 1X >= 1 + 1X s mark X -> s X 2 + 1X >= 1 + 1X U11(active X1, X2, X3) -> U11(X1, X2, X3) 1 + 1X1 + 1X2 + 0X3 >= 1 + 1X1 + 1X2 + 0X3 U11(mark X1, X2, X3) -> U11(X1, X2, X3) 2 + 1X1 + 1X2 + 0X3 >= 1 + 1X1 + 1X2 + 0X3 U11(X1, active X2, X3) -> U11(X1, X2, X3) 1 + 1X1 + 1X2 + 0X3 >= 1 + 1X1 + 1X2 + 0X3 U11(X1, mark X2, X3) -> U11(X1, X2, X3) 2 + 1X1 + 1X2 + 0X3 >= 1 + 1X1 + 1X2 + 0X3 U11(X1, X2, active X3) -> U11(X1, X2, X3) 1 + 1X1 + 1X2 + 0X3 >= 1 + 1X1 + 1X2 + 0X3 U11(X1, X2, mark X3) -> U11(X1, X2, X3) 1 + 1X1 + 1X2 + 0X3 >= 1 + 1X1 + 1X2 + 0X3 active plus(N, 0()) -> mark N 2 + 0N >= 1 + 1N active plus(N, s M) -> mark U11(tt(), M, N) 2 + 1M + 0N >= 3 + 1M + 0N active U11(tt(), M, N) -> mark U12(tt(), M, N) 2 + 1M + 0N >= 3 + 1M + 1N active U12(tt(), M, N) -> mark s plus(N, M) 2 + 1M + 1N >= 3 + 1M + 0N U12(active X1, X2, X3) -> U12(X1, X2, X3) 1 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U12(mark X1, X2, X3) -> U12(X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U12(X1, active X2, X3) -> U12(X1, X2, X3) 1 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U12(X1, mark X2, X3) -> U12(X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U12(X1, X2, active X3) -> U12(X1, X2, X3) 1 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U12(X1, X2, mark X3) -> U12(X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 mark 0() -> active 0() 2 >= 1 mark plus(X1, X2) -> active plus(mark X1, mark X2) 2 + 0X1 + 1X2 >= 2 + 0X1 + 1X2 mark s X -> active s mark X 2 + 1X >= 2 + 1X mark U11(X1, X2, X3) -> active U11(mark X1, X2, X3) 2 + 1X1 + 1X2 + 0X3 >= 2 + 1X1 + 1X2 + 0X3 mark tt() -> active tt() 2 >= 1 mark U12(X1, X2, X3) -> active U12(mark X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 2 + 1X1 + 1X2 + 1X3 Qed 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 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, 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)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [U12](x0, x1, x2) = 0, [U11](x0, x1, x2) = 0, [plus](x0, x1) = x0, [mark](x0) = x0, [active](x0) = x0 + 1, [s](x0) = 1, [tt] = 0, [0] = 0, [U11#](x0, x1, x2) = x0 Strict: U11#(active X1, X2, X3) -> U11#(X1, X2, X3) 1 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 U11#(mark X1, X2, X3) -> U11#(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 U11#(X1, active X2, X3) -> U11#(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 U11#(X1, mark X2, X3) -> U11#(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 U11#(X1, X2, active X3) -> U11#(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 U11#(X1, X2, mark X3) -> U11#(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 Weak: plus(active X1, X2) -> plus(X1, X2) 0 + 0X1 + 1X2 >= 0 + 0X1 + 1X2 plus(mark X1, X2) -> plus(X1, X2) 0 + 0X1 + 1X2 >= 0 + 0X1 + 1X2 plus(X1, active X2) -> plus(X1, X2) 1 + 0X1 + 1X2 >= 0 + 0X1 + 1X2 plus(X1, mark X2) -> plus(X1, X2) 0 + 0X1 + 1X2 >= 0 + 0X1 + 1X2 s active X -> s X 1 + 0X >= 1 + 0X s mark X -> s X 1 + 0X >= 1 + 0X U11(active X1, X2, X3) -> U11(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U11(mark X1, X2, X3) -> U11(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U11(X1, active X2, X3) -> U11(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U11(X1, mark X2, X3) -> U11(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U11(X1, X2, active X3) -> U11(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U11(X1, X2, mark X3) -> U11(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 active plus(N, 0()) -> mark N 1 + 0N >= 0 + 1N active plus(N, s M) -> mark U11(tt(), M, N) 2 + 0M + 0N >= 0 + 0M + 0N active U11(tt(), M, N) -> mark U12(tt(), M, N) 1 + 0M + 0N >= 0 + 0M + 0N active U12(tt(), M, N) -> mark s plus(N, M) 1 + 0M + 0N >= 1 + 0M + 0N U12(active X1, X2, X3) -> U12(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U12(mark X1, X2, X3) -> U12(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U12(X1, active X2, X3) -> U12(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U12(X1, mark X2, X3) -> U12(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U12(X1, X2, active X3) -> U12(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U12(X1, X2, mark X3) -> U12(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 mark 0() -> active 0() 0 >= 1 mark plus(X1, X2) -> active plus(mark X1, mark X2) 0 + 0X1 + 1X2 >= 1 + 0X1 + 1X2 mark s X -> active s mark X 1 + 0X >= 2 + 0X mark U11(X1, X2, X3) -> active U11(mark X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 mark tt() -> active tt() 0 >= 1 mark U12(X1, X2, X3) -> active U12(mark X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 SCCS (1): 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)} SCC (5): 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)} 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 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, 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)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [U12](x0, x1, x2) = 0, [U11](x0, x1, x2) = 0, [plus](x0, x1) = 0, [mark](x0) = x0, [active](x0) = x0 + 1, [s](x0) = 0, [tt] = 0, [0] = 0, [U11#](x0, x1, x2) = x0 Strict: U11#(mark X1, X2, X3) -> U11#(X1, X2, X3) 0 + 0X1 + 1X2 + 0X3 >= 0 + 0X1 + 1X2 + 0X3 U11#(X1, active X2, X3) -> U11#(X1, X2, X3) 1 + 0X1 + 1X2 + 0X3 >= 0 + 0X1 + 1X2 + 0X3 U11#(X1, mark X2, X3) -> U11#(X1, X2, X3) 0 + 0X1 + 1X2 + 0X3 >= 0 + 0X1 + 1X2 + 0X3 U11#(X1, X2, active X3) -> U11#(X1, X2, X3) 0 + 0X1 + 1X2 + 0X3 >= 0 + 0X1 + 1X2 + 0X3 U11#(X1, X2, mark X3) -> U11#(X1, X2, X3) 0 + 0X1 + 1X2 + 0X3 >= 0 + 0X1 + 1X2 + 0X3 Weak: plus(active X1, X2) -> plus(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 plus(mark X1, X2) -> plus(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 plus(X1, active X2) -> plus(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 plus(X1, mark X2) -> plus(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 s active X -> s X 0 + 0X >= 0 + 0X s mark X -> s X 0 + 0X >= 0 + 0X U11(active X1, X2, X3) -> U11(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U11(mark X1, X2, X3) -> U11(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U11(X1, active X2, X3) -> U11(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U11(X1, mark X2, X3) -> U11(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U11(X1, X2, active X3) -> U11(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U11(X1, X2, mark X3) -> U11(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 active plus(N, 0()) -> mark N 1 + 0N >= 0 + 1N active plus(N, s M) -> mark U11(tt(), M, N) 1 + 0M + 0N >= 0 + 0M + 0N active U11(tt(), M, N) -> mark U12(tt(), M, N) 1 + 0M + 0N >= 0 + 0M + 0N active U12(tt(), M, N) -> mark s plus(N, M) 1 + 0M + 0N >= 0 + 0M + 0N U12(active X1, X2, X3) -> U12(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U12(mark X1, X2, X3) -> U12(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U12(X1, active X2, X3) -> U12(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U12(X1, mark X2, X3) -> U12(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U12(X1, X2, active X3) -> U12(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U12(X1, X2, mark X3) -> U12(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 mark 0() -> active 0() 0 >= 1 mark plus(X1, X2) -> active plus(mark X1, mark X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 mark s X -> active s mark X 0 + 0X >= 1 + 0X mark U11(X1, X2, X3) -> active U11(mark X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 mark tt() -> active tt() 0 >= 1 mark U12(X1, X2, X3) -> active U12(mark X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 SCCS (1): 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#(mark X1, X2, X3) -> U11#(X1, X2, X3)} SCC (4): 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#(mark 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 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, 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)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [U12](x0, x1, x2) = x0 + x1 + x2 + 1, [U11](x0, x1, x2) = x0 + x1 + x2 + 1, [plus](x0, x1) = x0 + x1, [mark](x0) = x0 + 1, [active](x0) = x0, [s](x0) = x0 + 1, [tt] = 1, [0] = 1, [U11#](x0, x1, x2) = x0 Strict: U11#(mark X1, X2, X3) -> U11#(X1, X2, X3) 1 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 U11#(X1, mark X2, X3) -> U11#(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 U11#(X1, X2, active X3) -> U11#(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 U11#(X1, X2, mark X3) -> U11#(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 Weak: plus(active X1, X2) -> plus(X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 plus(mark X1, X2) -> plus(X1, X2) 1 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 plus(X1, active X2) -> plus(X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 plus(X1, mark X2) -> plus(X1, X2) 1 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 s active X -> s X 1 + 1X >= 1 + 1X s mark X -> s X 2 + 1X >= 1 + 1X U11(active X1, X2, X3) -> U11(X1, X2, X3) 1 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U11(mark X1, X2, X3) -> U11(X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U11(X1, active X2, X3) -> U11(X1, X2, X3) 1 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U11(X1, mark X2, X3) -> U11(X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U11(X1, X2, active X3) -> U11(X1, X2, X3) 1 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U11(X1, X2, mark X3) -> U11(X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 active plus(N, 0()) -> mark N 1 + 1N >= 1 + 1N active plus(N, s M) -> mark U11(tt(), M, N) 1 + 1M + 1N >= 3 + 1M + 1N active U11(tt(), M, N) -> mark U12(tt(), M, N) 2 + 1M + 1N >= 3 + 1M + 1N active U12(tt(), M, N) -> mark s plus(N, M) 2 + 1M + 1N >= 2 + 1M + 1N U12(active X1, X2, X3) -> U12(X1, X2, X3) 1 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U12(mark X1, X2, X3) -> U12(X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U12(X1, active X2, X3) -> U12(X1, X2, X3) 1 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U12(X1, mark X2, X3) -> U12(X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U12(X1, X2, active X3) -> U12(X1, X2, X3) 1 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U12(X1, X2, mark X3) -> U12(X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 mark 0() -> active 0() 2 >= 1 mark plus(X1, X2) -> active plus(mark X1, mark X2) 1 + 1X1 + 1X2 >= 2 + 1X1 + 1X2 mark s X -> active s mark X 2 + 1X >= 2 + 1X mark U11(X1, X2, X3) -> active U11(mark X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 2 + 1X1 + 1X2 + 1X3 mark tt() -> active tt() 2 >= 1 mark U12(X1, X2, X3) -> active U12(mark X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 2 + 1X1 + 1X2 + 1X3 SCCS (1): 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)} SCC (3): 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)} 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 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, 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)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [U12](x0, x1, x2) = x0 + x1 + x2 + 1, [U11](x0, x1, x2) = x0 + x1 + x2 + 1, [plus](x0, x1) = x0 + x1, [mark](x0) = x0 + 1, [active](x0) = x0, [s](x0) = x0 + 1, [tt] = 1, [0] = 1, [U11#](x0, x1, x2) = x0 Strict: U11#(X1, mark X2, X3) -> U11#(X1, X2, X3) 1 + 0X1 + 1X2 + 0X3 >= 0 + 0X1 + 1X2 + 0X3 U11#(X1, X2, active X3) -> U11#(X1, X2, X3) 0 + 0X1 + 1X2 + 0X3 >= 0 + 0X1 + 1X2 + 0X3 U11#(X1, X2, mark X3) -> U11#(X1, X2, X3) 0 + 0X1 + 1X2 + 0X3 >= 0 + 0X1 + 1X2 + 0X3 Weak: plus(active X1, X2) -> plus(X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 plus(mark X1, X2) -> plus(X1, X2) 1 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 plus(X1, active X2) -> plus(X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 plus(X1, mark X2) -> plus(X1, X2) 1 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 s active X -> s X 1 + 1X >= 1 + 1X s mark X -> s X 2 + 1X >= 1 + 1X U11(active X1, X2, X3) -> U11(X1, X2, X3) 1 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U11(mark X1, X2, X3) -> U11(X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U11(X1, active X2, X3) -> U11(X1, X2, X3) 1 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U11(X1, mark X2, X3) -> U11(X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U11(X1, X2, active X3) -> U11(X1, X2, X3) 1 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U11(X1, X2, mark X3) -> U11(X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 active plus(N, 0()) -> mark N 1 + 1N >= 1 + 1N active plus(N, s M) -> mark U11(tt(), M, N) 1 + 1M + 1N >= 3 + 1M + 1N active U11(tt(), M, N) -> mark U12(tt(), M, N) 2 + 1M + 1N >= 3 + 1M + 1N active U12(tt(), M, N) -> mark s plus(N, M) 2 + 1M + 1N >= 2 + 1M + 1N U12(active X1, X2, X3) -> U12(X1, X2, X3) 1 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U12(mark X1, X2, X3) -> U12(X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U12(X1, active X2, X3) -> U12(X1, X2, X3) 1 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U12(X1, mark X2, X3) -> U12(X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U12(X1, X2, active X3) -> U12(X1, X2, X3) 1 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U12(X1, X2, mark X3) -> U12(X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 mark 0() -> active 0() 2 >= 1 mark plus(X1, X2) -> active plus(mark X1, mark X2) 1 + 1X1 + 1X2 >= 2 + 1X1 + 1X2 mark s X -> active s mark X 2 + 1X >= 2 + 1X mark U11(X1, X2, X3) -> active U11(mark X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 2 + 1X1 + 1X2 + 1X3 mark tt() -> active tt() 2 >= 1 mark U12(X1, X2, X3) -> active U12(mark X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 2 + 1X1 + 1X2 + 1X3 SCCS (1): Scc: { U11#(X1, X2, mark X3) -> U11#(X1, X2, X3), U11#(X1, X2, active X3) -> U11#(X1, X2, X3)} SCC (2): Strict: { U11#(X1, X2, mark X3) -> U11#(X1, X2, X3), U11#(X1, X2, active 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 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, 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)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [U12](x0, x1, x2) = 0, [U11](x0, x1, x2) = 0, [plus](x0, x1) = 0, [mark](x0) = x0, [active](x0) = x0 + 1, [s](x0) = 0, [tt] = 0, [0] = 0, [U11#](x0, x1, x2) = x0 Strict: U11#(X1, X2, active X3) -> U11#(X1, X2, X3) 1 + 0X1 + 0X2 + 1X3 >= 0 + 0X1 + 0X2 + 1X3 U11#(X1, X2, mark X3) -> U11#(X1, X2, X3) 0 + 0X1 + 0X2 + 1X3 >= 0 + 0X1 + 0X2 + 1X3 Weak: plus(active X1, X2) -> plus(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 plus(mark X1, X2) -> plus(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 plus(X1, active X2) -> plus(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 plus(X1, mark X2) -> plus(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 s active X -> s X 0 + 0X >= 0 + 0X s mark X -> s X 0 + 0X >= 0 + 0X U11(active X1, X2, X3) -> U11(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U11(mark X1, X2, X3) -> U11(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U11(X1, active X2, X3) -> U11(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U11(X1, mark X2, X3) -> U11(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U11(X1, X2, active X3) -> U11(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U11(X1, X2, mark X3) -> U11(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 active plus(N, 0()) -> mark N 1 + 0N >= 0 + 1N active plus(N, s M) -> mark U11(tt(), M, N) 1 + 0M + 0N >= 0 + 0M + 0N active U11(tt(), M, N) -> mark U12(tt(), M, N) 1 + 0M + 0N >= 0 + 0M + 0N active U12(tt(), M, N) -> mark s plus(N, M) 1 + 0M + 0N >= 0 + 0M + 0N U12(active X1, X2, X3) -> U12(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U12(mark X1, X2, X3) -> U12(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U12(X1, active X2, X3) -> U12(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U12(X1, mark X2, X3) -> U12(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U12(X1, X2, active X3) -> U12(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U12(X1, X2, mark X3) -> U12(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 mark 0() -> active 0() 0 >= 1 mark plus(X1, X2) -> active plus(mark X1, mark X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 mark s X -> active s mark X 0 + 0X >= 1 + 0X mark U11(X1, X2, X3) -> active U11(mark X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 mark tt() -> active tt() 0 >= 1 mark U12(X1, X2, X3) -> active U12(mark X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 SCCS (1): Scc: {U11#(X1, X2, mark X3) -> U11#(X1, X2, X3)} SCC (1): Strict: {U11#(X1, X2, mark 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 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, 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)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [U12](x0, x1, x2) = x0 + x1 + x2 + 1, [U11](x0, x1, x2) = x0 + x1 + 1, [plus](x0, x1) = x0 + 1, [mark](x0) = x0 + 1, [active](x0) = x0, [s](x0) = x0 + 1, [tt] = 1, [0] = 1, [U11#](x0, x1, x2) = x0 Strict: U11#(X1, X2, mark X3) -> U11#(X1, X2, X3) 1 + 0X1 + 0X2 + 1X3 >= 0 + 0X1 + 0X2 + 1X3 Weak: plus(active X1, X2) -> plus(X1, X2) 1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2 plus(mark X1, X2) -> plus(X1, X2) 1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2 plus(X1, active X2) -> plus(X1, X2) 1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2 plus(X1, mark X2) -> plus(X1, X2) 2 + 0X1 + 1X2 >= 1 + 0X1 + 1X2 s active X -> s X 1 + 1X >= 1 + 1X s mark X -> s X 2 + 1X >= 1 + 1X U11(active X1, X2, X3) -> U11(X1, X2, X3) 1 + 1X1 + 1X2 + 0X3 >= 1 + 1X1 + 1X2 + 0X3 U11(mark X1, X2, X3) -> U11(X1, X2, X3) 2 + 1X1 + 1X2 + 0X3 >= 1 + 1X1 + 1X2 + 0X3 U11(X1, active X2, X3) -> U11(X1, X2, X3) 1 + 1X1 + 1X2 + 0X3 >= 1 + 1X1 + 1X2 + 0X3 U11(X1, mark X2, X3) -> U11(X1, X2, X3) 2 + 1X1 + 1X2 + 0X3 >= 1 + 1X1 + 1X2 + 0X3 U11(X1, X2, active X3) -> U11(X1, X2, X3) 1 + 1X1 + 1X2 + 0X3 >= 1 + 1X1 + 1X2 + 0X3 U11(X1, X2, mark X3) -> U11(X1, X2, X3) 1 + 1X1 + 1X2 + 0X3 >= 1 + 1X1 + 1X2 + 0X3 active plus(N, 0()) -> mark N 2 + 0N >= 1 + 1N active plus(N, s M) -> mark U11(tt(), M, N) 2 + 1M + 0N >= 3 + 1M + 0N active U11(tt(), M, N) -> mark U12(tt(), M, N) 2 + 1M + 0N >= 3 + 1M + 1N active U12(tt(), M, N) -> mark s plus(N, M) 2 + 1M + 1N >= 3 + 1M + 0N U12(active X1, X2, X3) -> U12(X1, X2, X3) 1 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U12(mark X1, X2, X3) -> U12(X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U12(X1, active X2, X3) -> U12(X1, X2, X3) 1 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U12(X1, mark X2, X3) -> U12(X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U12(X1, X2, active X3) -> U12(X1, X2, X3) 1 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U12(X1, X2, mark X3) -> U12(X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 mark 0() -> active 0() 2 >= 1 mark plus(X1, X2) -> active plus(mark X1, mark X2) 2 + 0X1 + 1X2 >= 2 + 0X1 + 1X2 mark s X -> active s mark X 2 + 1X >= 2 + 1X mark U11(X1, X2, X3) -> active U11(mark X1, X2, X3) 2 + 1X1 + 1X2 + 0X3 >= 2 + 1X1 + 1X2 + 0X3 mark tt() -> active tt() 2 >= 1 mark U12(X1, X2, X3) -> active U12(mark X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 2 + 1X1 + 1X2 + 1X3 Qed 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 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, 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)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [U12](x0, x1, x2) = 0, [U11](x0, x1, x2) = 0, [plus](x0, x1) = 0, [mark](x0) = x0, [active](x0) = x0 + 1, [s](x0) = 0, [tt] = 0, [0] = 0, [s#](x0) = x0 Strict: s# active X -> s# X 1 + 1X >= 0 + 1X s# mark X -> s# X 0 + 1X >= 0 + 1X Weak: plus(active X1, X2) -> plus(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 plus(mark X1, X2) -> plus(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 plus(X1, active X2) -> plus(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 plus(X1, mark X2) -> plus(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 s active X -> s X 0 + 0X >= 0 + 0X s mark X -> s X 0 + 0X >= 0 + 0X U11(active X1, X2, X3) -> U11(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U11(mark X1, X2, X3) -> U11(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U11(X1, active X2, X3) -> U11(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U11(X1, mark X2, X3) -> U11(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U11(X1, X2, active X3) -> U11(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U11(X1, X2, mark X3) -> U11(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 active plus(N, 0()) -> mark N 1 + 0N >= 0 + 1N active plus(N, s M) -> mark U11(tt(), M, N) 1 + 0M + 0N >= 0 + 0M + 0N active U11(tt(), M, N) -> mark U12(tt(), M, N) 1 + 0M + 0N >= 0 + 0M + 0N active U12(tt(), M, N) -> mark s plus(N, M) 1 + 0M + 0N >= 0 + 0M + 0N U12(active X1, X2, X3) -> U12(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U12(mark X1, X2, X3) -> U12(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U12(X1, active X2, X3) -> U12(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U12(X1, mark X2, X3) -> U12(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U12(X1, X2, active X3) -> U12(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U12(X1, X2, mark X3) -> U12(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 mark 0() -> active 0() 0 >= 1 mark plus(X1, X2) -> active plus(mark X1, mark X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 mark s X -> active s mark X 0 + 0X >= 1 + 0X mark U11(X1, X2, X3) -> active U11(mark X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 mark tt() -> active tt() 0 >= 1 mark U12(X1, X2, X3) -> active U12(mark X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 SCCS (1): Scc: {s# mark X -> s# X} SCC (1): Strict: {s# mark 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 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, 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)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [U12](x0, x1, x2) = x0 + x1 + x2 + 1, [U11](x0, x1, x2) = x0 + x1 + 1, [plus](x0, x1) = x0 + 1, [mark](x0) = x0 + 1, [active](x0) = x0, [s](x0) = x0 + 1, [tt] = 1, [0] = 1, [s#](x0) = x0 Strict: s# mark X -> s# X 1 + 1X >= 0 + 1X Weak: plus(active X1, X2) -> plus(X1, X2) 1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2 plus(mark X1, X2) -> plus(X1, X2) 1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2 plus(X1, active X2) -> plus(X1, X2) 1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2 plus(X1, mark X2) -> plus(X1, X2) 2 + 0X1 + 1X2 >= 1 + 0X1 + 1X2 s active X -> s X 1 + 1X >= 1 + 1X s mark X -> s X 2 + 1X >= 1 + 1X U11(active X1, X2, X3) -> U11(X1, X2, X3) 1 + 1X1 + 1X2 + 0X3 >= 1 + 1X1 + 1X2 + 0X3 U11(mark X1, X2, X3) -> U11(X1, X2, X3) 2 + 1X1 + 1X2 + 0X3 >= 1 + 1X1 + 1X2 + 0X3 U11(X1, active X2, X3) -> U11(X1, X2, X3) 1 + 1X1 + 1X2 + 0X3 >= 1 + 1X1 + 1X2 + 0X3 U11(X1, mark X2, X3) -> U11(X1, X2, X3) 2 + 1X1 + 1X2 + 0X3 >= 1 + 1X1 + 1X2 + 0X3 U11(X1, X2, active X3) -> U11(X1, X2, X3) 1 + 1X1 + 1X2 + 0X3 >= 1 + 1X1 + 1X2 + 0X3 U11(X1, X2, mark X3) -> U11(X1, X2, X3) 1 + 1X1 + 1X2 + 0X3 >= 1 + 1X1 + 1X2 + 0X3 active plus(N, 0()) -> mark N 2 + 0N >= 1 + 1N active plus(N, s M) -> mark U11(tt(), M, N) 2 + 1M + 0N >= 3 + 1M + 0N active U11(tt(), M, N) -> mark U12(tt(), M, N) 2 + 1M + 0N >= 3 + 1M + 1N active U12(tt(), M, N) -> mark s plus(N, M) 2 + 1M + 1N >= 3 + 1M + 0N U12(active X1, X2, X3) -> U12(X1, X2, X3) 1 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U12(mark X1, X2, X3) -> U12(X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U12(X1, active X2, X3) -> U12(X1, X2, X3) 1 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U12(X1, mark X2, X3) -> U12(X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U12(X1, X2, active X3) -> U12(X1, X2, X3) 1 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U12(X1, X2, mark X3) -> U12(X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 mark 0() -> active 0() 2 >= 1 mark plus(X1, X2) -> active plus(mark X1, mark X2) 2 + 0X1 + 1X2 >= 2 + 0X1 + 1X2 mark s X -> active s mark X 2 + 1X >= 2 + 1X mark U11(X1, X2, X3) -> active U11(mark X1, X2, X3) 2 + 1X1 + 1X2 + 0X3 >= 2 + 1X1 + 1X2 + 0X3 mark tt() -> active tt() 2 >= 1 mark U12(X1, X2, X3) -> active U12(mark X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 2 + 1X1 + 1X2 + 1X3 Qed 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 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, 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)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [U12](x0, x1, x2) = 0, [U11](x0, x1, x2) = 0, [plus](x0, x1) = x0, [mark](x0) = x0, [active](x0) = x0 + 1, [s](x0) = 1, [tt] = 0, [0] = 0, [U12#](x0, x1, x2) = x0 Strict: U12#(active X1, X2, X3) -> U12#(X1, X2, X3) 1 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 U12#(mark X1, X2, X3) -> U12#(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 U12#(X1, active X2, X3) -> U12#(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 U12#(X1, mark X2, X3) -> U12#(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 U12#(X1, X2, active X3) -> U12#(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 U12#(X1, X2, mark X3) -> U12#(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 Weak: plus(active X1, X2) -> plus(X1, X2) 0 + 0X1 + 1X2 >= 0 + 0X1 + 1X2 plus(mark X1, X2) -> plus(X1, X2) 0 + 0X1 + 1X2 >= 0 + 0X1 + 1X2 plus(X1, active X2) -> plus(X1, X2) 1 + 0X1 + 1X2 >= 0 + 0X1 + 1X2 plus(X1, mark X2) -> plus(X1, X2) 0 + 0X1 + 1X2 >= 0 + 0X1 + 1X2 s active X -> s X 1 + 0X >= 1 + 0X s mark X -> s X 1 + 0X >= 1 + 0X U11(active X1, X2, X3) -> U11(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U11(mark X1, X2, X3) -> U11(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U11(X1, active X2, X3) -> U11(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U11(X1, mark X2, X3) -> U11(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U11(X1, X2, active X3) -> U11(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U11(X1, X2, mark X3) -> U11(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 active plus(N, 0()) -> mark N 1 + 0N >= 0 + 1N active plus(N, s M) -> mark U11(tt(), M, N) 2 + 0M + 0N >= 0 + 0M + 0N active U11(tt(), M, N) -> mark U12(tt(), M, N) 1 + 0M + 0N >= 0 + 0M + 0N active U12(tt(), M, N) -> mark s plus(N, M) 1 + 0M + 0N >= 1 + 0M + 0N U12(active X1, X2, X3) -> U12(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U12(mark X1, X2, X3) -> U12(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U12(X1, active X2, X3) -> U12(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U12(X1, mark X2, X3) -> U12(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U12(X1, X2, active X3) -> U12(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U12(X1, X2, mark X3) -> U12(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 mark 0() -> active 0() 0 >= 1 mark plus(X1, X2) -> active plus(mark X1, mark X2) 0 + 0X1 + 1X2 >= 1 + 0X1 + 1X2 mark s X -> active s mark X 1 + 0X >= 2 + 0X mark U11(X1, X2, X3) -> active U11(mark X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 mark tt() -> active tt() 0 >= 1 mark U12(X1, X2, X3) -> active U12(mark X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 SCCS (1): 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)} SCC (5): 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)} 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 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, 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)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [U12](x0, x1, x2) = 0, [U11](x0, x1, x2) = 0, [plus](x0, x1) = 0, [mark](x0) = x0, [active](x0) = x0 + 1, [s](x0) = 0, [tt] = 0, [0] = 0, [U12#](x0, x1, x2) = x0 Strict: U12#(mark X1, X2, X3) -> U12#(X1, X2, X3) 0 + 0X1 + 1X2 + 0X3 >= 0 + 0X1 + 1X2 + 0X3 U12#(X1, active X2, X3) -> U12#(X1, X2, X3) 1 + 0X1 + 1X2 + 0X3 >= 0 + 0X1 + 1X2 + 0X3 U12#(X1, mark X2, X3) -> U12#(X1, X2, X3) 0 + 0X1 + 1X2 + 0X3 >= 0 + 0X1 + 1X2 + 0X3 U12#(X1, X2, active X3) -> U12#(X1, X2, X3) 0 + 0X1 + 1X2 + 0X3 >= 0 + 0X1 + 1X2 + 0X3 U12#(X1, X2, mark X3) -> U12#(X1, X2, X3) 0 + 0X1 + 1X2 + 0X3 >= 0 + 0X1 + 1X2 + 0X3 Weak: plus(active X1, X2) -> plus(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 plus(mark X1, X2) -> plus(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 plus(X1, active X2) -> plus(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 plus(X1, mark X2) -> plus(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 s active X -> s X 0 + 0X >= 0 + 0X s mark X -> s X 0 + 0X >= 0 + 0X U11(active X1, X2, X3) -> U11(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U11(mark X1, X2, X3) -> U11(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U11(X1, active X2, X3) -> U11(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U11(X1, mark X2, X3) -> U11(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U11(X1, X2, active X3) -> U11(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U11(X1, X2, mark X3) -> U11(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 active plus(N, 0()) -> mark N 1 + 0N >= 0 + 1N active plus(N, s M) -> mark U11(tt(), M, N) 1 + 0M + 0N >= 0 + 0M + 0N active U11(tt(), M, N) -> mark U12(tt(), M, N) 1 + 0M + 0N >= 0 + 0M + 0N active U12(tt(), M, N) -> mark s plus(N, M) 1 + 0M + 0N >= 0 + 0M + 0N U12(active X1, X2, X3) -> U12(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U12(mark X1, X2, X3) -> U12(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U12(X1, active X2, X3) -> U12(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U12(X1, mark X2, X3) -> U12(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U12(X1, X2, active X3) -> U12(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U12(X1, X2, mark X3) -> U12(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 mark 0() -> active 0() 0 >= 1 mark plus(X1, X2) -> active plus(mark X1, mark X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 mark s X -> active s mark X 0 + 0X >= 1 + 0X mark U11(X1, X2, X3) -> active U11(mark X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 mark tt() -> active tt() 0 >= 1 mark U12(X1, X2, X3) -> active U12(mark X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 SCCS (1): 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#(mark X1, X2, X3) -> U12#(X1, X2, X3)} SCC (4): 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#(mark 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 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, 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)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [U12](x0, x1, x2) = x0 + x1 + x2 + 1, [U11](x0, x1, x2) = x0 + x1 + x2 + 1, [plus](x0, x1) = x0 + x1, [mark](x0) = x0 + 1, [active](x0) = x0, [s](x0) = x0 + 1, [tt] = 1, [0] = 1, [U12#](x0, x1, x2) = x0 Strict: U12#(mark X1, X2, X3) -> U12#(X1, X2, X3) 1 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 U12#(X1, mark X2, X3) -> U12#(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 U12#(X1, X2, active X3) -> U12#(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 U12#(X1, X2, mark X3) -> U12#(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 Weak: plus(active X1, X2) -> plus(X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 plus(mark X1, X2) -> plus(X1, X2) 1 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 plus(X1, active X2) -> plus(X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 plus(X1, mark X2) -> plus(X1, X2) 1 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 s active X -> s X 1 + 1X >= 1 + 1X s mark X -> s X 2 + 1X >= 1 + 1X U11(active X1, X2, X3) -> U11(X1, X2, X3) 1 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U11(mark X1, X2, X3) -> U11(X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U11(X1, active X2, X3) -> U11(X1, X2, X3) 1 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U11(X1, mark X2, X3) -> U11(X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U11(X1, X2, active X3) -> U11(X1, X2, X3) 1 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U11(X1, X2, mark X3) -> U11(X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 active plus(N, 0()) -> mark N 1 + 1N >= 1 + 1N active plus(N, s M) -> mark U11(tt(), M, N) 1 + 1M + 1N >= 3 + 1M + 1N active U11(tt(), M, N) -> mark U12(tt(), M, N) 2 + 1M + 1N >= 3 + 1M + 1N active U12(tt(), M, N) -> mark s plus(N, M) 2 + 1M + 1N >= 2 + 1M + 1N U12(active X1, X2, X3) -> U12(X1, X2, X3) 1 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U12(mark X1, X2, X3) -> U12(X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U12(X1, active X2, X3) -> U12(X1, X2, X3) 1 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U12(X1, mark X2, X3) -> U12(X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U12(X1, X2, active X3) -> U12(X1, X2, X3) 1 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U12(X1, X2, mark X3) -> U12(X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 mark 0() -> active 0() 2 >= 1 mark plus(X1, X2) -> active plus(mark X1, mark X2) 1 + 1X1 + 1X2 >= 2 + 1X1 + 1X2 mark s X -> active s mark X 2 + 1X >= 2 + 1X mark U11(X1, X2, X3) -> active U11(mark X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 2 + 1X1 + 1X2 + 1X3 mark tt() -> active tt() 2 >= 1 mark U12(X1, X2, X3) -> active U12(mark X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 2 + 1X1 + 1X2 + 1X3 SCCS (1): 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)} SCC (3): 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)} 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 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, 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)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [U12](x0, x1, x2) = x0 + x1 + x2 + 1, [U11](x0, x1, x2) = x0 + x1 + x2 + 1, [plus](x0, x1) = x0 + x1, [mark](x0) = x0 + 1, [active](x0) = x0, [s](x0) = x0 + 1, [tt] = 1, [0] = 1, [U12#](x0, x1, x2) = x0 Strict: U12#(X1, mark X2, X3) -> U12#(X1, X2, X3) 1 + 0X1 + 1X2 + 0X3 >= 0 + 0X1 + 1X2 + 0X3 U12#(X1, X2, active X3) -> U12#(X1, X2, X3) 0 + 0X1 + 1X2 + 0X3 >= 0 + 0X1 + 1X2 + 0X3 U12#(X1, X2, mark X3) -> U12#(X1, X2, X3) 0 + 0X1 + 1X2 + 0X3 >= 0 + 0X1 + 1X2 + 0X3 Weak: plus(active X1, X2) -> plus(X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 plus(mark X1, X2) -> plus(X1, X2) 1 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 plus(X1, active X2) -> plus(X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 plus(X1, mark X2) -> plus(X1, X2) 1 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 s active X -> s X 1 + 1X >= 1 + 1X s mark X -> s X 2 + 1X >= 1 + 1X U11(active X1, X2, X3) -> U11(X1, X2, X3) 1 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U11(mark X1, X2, X3) -> U11(X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U11(X1, active X2, X3) -> U11(X1, X2, X3) 1 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U11(X1, mark X2, X3) -> U11(X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U11(X1, X2, active X3) -> U11(X1, X2, X3) 1 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U11(X1, X2, mark X3) -> U11(X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 active plus(N, 0()) -> mark N 1 + 1N >= 1 + 1N active plus(N, s M) -> mark U11(tt(), M, N) 1 + 1M + 1N >= 3 + 1M + 1N active U11(tt(), M, N) -> mark U12(tt(), M, N) 2 + 1M + 1N >= 3 + 1M + 1N active U12(tt(), M, N) -> mark s plus(N, M) 2 + 1M + 1N >= 2 + 1M + 1N U12(active X1, X2, X3) -> U12(X1, X2, X3) 1 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U12(mark X1, X2, X3) -> U12(X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U12(X1, active X2, X3) -> U12(X1, X2, X3) 1 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U12(X1, mark X2, X3) -> U12(X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U12(X1, X2, active X3) -> U12(X1, X2, X3) 1 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U12(X1, X2, mark X3) -> U12(X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 mark 0() -> active 0() 2 >= 1 mark plus(X1, X2) -> active plus(mark X1, mark X2) 1 + 1X1 + 1X2 >= 2 + 1X1 + 1X2 mark s X -> active s mark X 2 + 1X >= 2 + 1X mark U11(X1, X2, X3) -> active U11(mark X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 2 + 1X1 + 1X2 + 1X3 mark tt() -> active tt() 2 >= 1 mark U12(X1, X2, X3) -> active U12(mark X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 2 + 1X1 + 1X2 + 1X3 SCCS (1): Scc: { U12#(X1, X2, mark X3) -> U12#(X1, X2, X3), U12#(X1, X2, active X3) -> U12#(X1, X2, X3)} SCC (2): Strict: { U12#(X1, X2, mark X3) -> U12#(X1, X2, X3), U12#(X1, X2, active 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 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, 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)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [U12](x0, x1, x2) = 0, [U11](x0, x1, x2) = 0, [plus](x0, x1) = 0, [mark](x0) = x0, [active](x0) = x0 + 1, [s](x0) = 0, [tt] = 0, [0] = 0, [U12#](x0, x1, x2) = x0 Strict: U12#(X1, X2, active X3) -> U12#(X1, X2, X3) 1 + 0X1 + 0X2 + 1X3 >= 0 + 0X1 + 0X2 + 1X3 U12#(X1, X2, mark X3) -> U12#(X1, X2, X3) 0 + 0X1 + 0X2 + 1X3 >= 0 + 0X1 + 0X2 + 1X3 Weak: plus(active X1, X2) -> plus(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 plus(mark X1, X2) -> plus(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 plus(X1, active X2) -> plus(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 plus(X1, mark X2) -> plus(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 s active X -> s X 0 + 0X >= 0 + 0X s mark X -> s X 0 + 0X >= 0 + 0X U11(active X1, X2, X3) -> U11(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U11(mark X1, X2, X3) -> U11(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U11(X1, active X2, X3) -> U11(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U11(X1, mark X2, X3) -> U11(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U11(X1, X2, active X3) -> U11(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U11(X1, X2, mark X3) -> U11(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 active plus(N, 0()) -> mark N 1 + 0N >= 0 + 1N active plus(N, s M) -> mark U11(tt(), M, N) 1 + 0M + 0N >= 0 + 0M + 0N active U11(tt(), M, N) -> mark U12(tt(), M, N) 1 + 0M + 0N >= 0 + 0M + 0N active U12(tt(), M, N) -> mark s plus(N, M) 1 + 0M + 0N >= 0 + 0M + 0N U12(active X1, X2, X3) -> U12(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U12(mark X1, X2, X3) -> U12(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U12(X1, active X2, X3) -> U12(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U12(X1, mark X2, X3) -> U12(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U12(X1, X2, active X3) -> U12(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 U12(X1, X2, mark X3) -> U12(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 mark 0() -> active 0() 0 >= 1 mark plus(X1, X2) -> active plus(mark X1, mark X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 mark s X -> active s mark X 0 + 0X >= 1 + 0X mark U11(X1, X2, X3) -> active U11(mark X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 mark tt() -> active tt() 0 >= 1 mark U12(X1, X2, X3) -> active U12(mark X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 SCCS (1): Scc: {U12#(X1, X2, mark X3) -> U12#(X1, X2, X3)} SCC (1): Strict: {U12#(X1, X2, mark 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 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, 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)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [U12](x0, x1, x2) = x0 + x1 + x2 + 1, [U11](x0, x1, x2) = x0 + x1 + 1, [plus](x0, x1) = x0 + 1, [mark](x0) = x0 + 1, [active](x0) = x0, [s](x0) = x0 + 1, [tt] = 1, [0] = 1, [U12#](x0, x1, x2) = x0 Strict: U12#(X1, X2, mark X3) -> U12#(X1, X2, X3) 1 + 0X1 + 0X2 + 1X3 >= 0 + 0X1 + 0X2 + 1X3 Weak: plus(active X1, X2) -> plus(X1, X2) 1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2 plus(mark X1, X2) -> plus(X1, X2) 1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2 plus(X1, active X2) -> plus(X1, X2) 1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2 plus(X1, mark X2) -> plus(X1, X2) 2 + 0X1 + 1X2 >= 1 + 0X1 + 1X2 s active X -> s X 1 + 1X >= 1 + 1X s mark X -> s X 2 + 1X >= 1 + 1X U11(active X1, X2, X3) -> U11(X1, X2, X3) 1 + 1X1 + 1X2 + 0X3 >= 1 + 1X1 + 1X2 + 0X3 U11(mark X1, X2, X3) -> U11(X1, X2, X3) 2 + 1X1 + 1X2 + 0X3 >= 1 + 1X1 + 1X2 + 0X3 U11(X1, active X2, X3) -> U11(X1, X2, X3) 1 + 1X1 + 1X2 + 0X3 >= 1 + 1X1 + 1X2 + 0X3 U11(X1, mark X2, X3) -> U11(X1, X2, X3) 2 + 1X1 + 1X2 + 0X3 >= 1 + 1X1 + 1X2 + 0X3 U11(X1, X2, active X3) -> U11(X1, X2, X3) 1 + 1X1 + 1X2 + 0X3 >= 1 + 1X1 + 1X2 + 0X3 U11(X1, X2, mark X3) -> U11(X1, X2, X3) 1 + 1X1 + 1X2 + 0X3 >= 1 + 1X1 + 1X2 + 0X3 active plus(N, 0()) -> mark N 2 + 0N >= 1 + 1N active plus(N, s M) -> mark U11(tt(), M, N) 2 + 1M + 0N >= 3 + 1M + 0N active U11(tt(), M, N) -> mark U12(tt(), M, N) 2 + 1M + 0N >= 3 + 1M + 1N active U12(tt(), M, N) -> mark s plus(N, M) 2 + 1M + 1N >= 3 + 1M + 0N U12(active X1, X2, X3) -> U12(X1, X2, X3) 1 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U12(mark X1, X2, X3) -> U12(X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U12(X1, active X2, X3) -> U12(X1, X2, X3) 1 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U12(X1, mark X2, X3) -> U12(X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U12(X1, X2, active X3) -> U12(X1, X2, X3) 1 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 U12(X1, X2, mark X3) -> U12(X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 mark 0() -> active 0() 2 >= 1 mark plus(X1, X2) -> active plus(mark X1, mark X2) 2 + 0X1 + 1X2 >= 2 + 0X1 + 1X2 mark s X -> active s mark X 2 + 1X >= 2 + 1X mark U11(X1, X2, X3) -> active U11(mark X1, X2, X3) 2 + 1X1 + 1X2 + 0X3 >= 2 + 1X1 + 1X2 + 0X3 mark tt() -> active tt() 2 >= 1 mark U12(X1, X2, X3) -> active U12(mark X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 2 + 1X1 + 1X2 + 1X3 Qed