YES Time: 0.462360 TRS: { mark f(X1, X2, X3) -> active f(X1, mark X2, X3), mark b() -> active b(), mark a() -> active a(), f(X1, X2, mark X3) -> f(X1, X2, X3), f(X1, X2, active X3) -> f(X1, X2, X3), f(X1, mark X2, X3) -> f(X1, X2, X3), f(X1, active X2, X3) -> f(X1, X2, X3), f(mark X1, X2, X3) -> f(X1, X2, X3), f(active X1, X2, X3) -> f(X1, X2, X3), active f(a(), X, X) -> mark f(X, b(), b()), active b() -> mark a()} DP: DP: { mark# f(X1, X2, X3) -> mark# X2, mark# f(X1, X2, X3) -> f#(X1, mark X2, X3), mark# f(X1, X2, X3) -> active# f(X1, mark X2, X3), mark# b() -> active# b(), mark# a() -> active# a(), f#(X1, X2, mark X3) -> f#(X1, X2, X3), f#(X1, X2, active X3) -> f#(X1, X2, X3), f#(X1, mark X2, X3) -> f#(X1, X2, X3), f#(X1, active X2, X3) -> f#(X1, X2, X3), f#(mark X1, X2, X3) -> f#(X1, X2, X3), f#(active X1, X2, X3) -> f#(X1, X2, X3), active# f(a(), X, X) -> mark# f(X, b(), b()), active# f(a(), X, X) -> f#(X, b(), b()), active# b() -> mark# a()} TRS: { mark f(X1, X2, X3) -> active f(X1, mark X2, X3), mark b() -> active b(), mark a() -> active a(), f(X1, X2, mark X3) -> f(X1, X2, X3), f(X1, X2, active X3) -> f(X1, X2, X3), f(X1, mark X2, X3) -> f(X1, X2, X3), f(X1, active X2, X3) -> f(X1, X2, X3), f(mark X1, X2, X3) -> f(X1, X2, X3), f(active X1, X2, X3) -> f(X1, X2, X3), active f(a(), X, X) -> mark f(X, b(), b()), active b() -> mark a()} EDG: {(mark# f(X1, X2, X3) -> f#(X1, mark X2, X3), f#(active X1, X2, X3) -> f#(X1, X2, X3)) (mark# f(X1, X2, X3) -> f#(X1, mark X2, X3), f#(mark X1, X2, X3) -> f#(X1, X2, X3)) (mark# f(X1, X2, X3) -> f#(X1, mark X2, X3), f#(X1, active X2, X3) -> f#(X1, X2, X3)) (mark# f(X1, X2, X3) -> f#(X1, mark X2, X3), f#(X1, mark X2, X3) -> f#(X1, X2, X3)) (mark# f(X1, X2, X3) -> f#(X1, mark X2, X3), f#(X1, X2, active X3) -> f#(X1, X2, X3)) (mark# f(X1, X2, X3) -> f#(X1, mark X2, X3), f#(X1, X2, mark X3) -> f#(X1, X2, X3)) (f#(X1, X2, active X3) -> f#(X1, X2, X3), f#(active X1, X2, X3) -> f#(X1, X2, X3)) (f#(X1, X2, active X3) -> f#(X1, X2, X3), f#(mark X1, X2, X3) -> f#(X1, X2, X3)) (f#(X1, X2, active X3) -> f#(X1, X2, X3), f#(X1, active X2, X3) -> f#(X1, X2, X3)) (f#(X1, X2, active X3) -> f#(X1, X2, X3), f#(X1, mark X2, X3) -> f#(X1, X2, X3)) (f#(X1, X2, active X3) -> f#(X1, X2, X3), f#(X1, X2, active X3) -> f#(X1, X2, X3)) (f#(X1, X2, active X3) -> f#(X1, X2, X3), f#(X1, X2, mark X3) -> f#(X1, X2, X3)) (f#(X1, active X2, X3) -> f#(X1, X2, X3), f#(active X1, X2, X3) -> f#(X1, X2, X3)) (f#(X1, active X2, X3) -> f#(X1, X2, X3), f#(mark X1, X2, X3) -> f#(X1, X2, X3)) (f#(X1, active X2, X3) -> f#(X1, X2, X3), f#(X1, active X2, X3) -> f#(X1, X2, X3)) (f#(X1, active X2, X3) -> f#(X1, X2, X3), f#(X1, mark X2, X3) -> f#(X1, X2, X3)) (f#(X1, active X2, X3) -> f#(X1, X2, X3), f#(X1, X2, active X3) -> f#(X1, X2, X3)) (f#(X1, active X2, X3) -> f#(X1, X2, X3), f#(X1, X2, mark X3) -> f#(X1, X2, X3)) (f#(active X1, X2, X3) -> f#(X1, X2, X3), f#(active X1, X2, X3) -> f#(X1, X2, X3)) (f#(active X1, X2, X3) -> f#(X1, X2, X3), f#(mark X1, X2, X3) -> f#(X1, X2, X3)) (f#(active X1, X2, X3) -> f#(X1, X2, X3), f#(X1, active X2, X3) -> f#(X1, X2, X3)) (f#(active X1, X2, X3) -> f#(X1, X2, X3), f#(X1, mark X2, X3) -> f#(X1, X2, X3)) (f#(active X1, X2, X3) -> f#(X1, X2, X3), f#(X1, X2, active X3) -> f#(X1, X2, X3)) (f#(active X1, X2, X3) -> f#(X1, X2, X3), f#(X1, X2, mark X3) -> f#(X1, X2, X3)) (active# f(a(), X, X) -> mark# f(X, b(), b()), mark# a() -> active# a()) (active# f(a(), X, X) -> mark# f(X, b(), b()), mark# b() -> active# b()) (active# f(a(), X, X) -> mark# f(X, b(), b()), mark# f(X1, X2, X3) -> active# f(X1, mark X2, X3)) (active# f(a(), X, X) -> mark# f(X, b(), b()), mark# f(X1, X2, X3) -> f#(X1, mark X2, X3)) (active# f(a(), X, X) -> mark# f(X, b(), b()), mark# f(X1, X2, X3) -> mark# X2) (mark# b() -> active# b(), active# b() -> mark# a()) (mark# b() -> active# b(), active# f(a(), X, X) -> f#(X, b(), b())) (mark# b() -> active# b(), active# f(a(), X, X) -> mark# f(X, b(), b())) (active# b() -> mark# a(), mark# a() -> active# a()) (active# b() -> mark# a(), mark# b() -> active# b()) (active# b() -> mark# a(), mark# f(X1, X2, X3) -> active# f(X1, mark X2, X3)) (active# b() -> mark# a(), mark# f(X1, X2, X3) -> f#(X1, mark X2, X3)) (active# b() -> mark# a(), mark# f(X1, X2, X3) -> mark# X2) (mark# a() -> active# a(), active# f(a(), X, X) -> mark# f(X, b(), b())) (mark# a() -> active# a(), active# f(a(), X, X) -> f#(X, b(), b())) (mark# a() -> active# a(), active# b() -> mark# a()) (active# f(a(), X, X) -> f#(X, b(), b()), f#(X1, X2, mark X3) -> f#(X1, X2, X3)) (active# f(a(), X, X) -> f#(X, b(), b()), f#(X1, X2, active X3) -> f#(X1, X2, X3)) (active# f(a(), X, X) -> f#(X, b(), b()), f#(X1, mark X2, X3) -> f#(X1, X2, X3)) (active# f(a(), X, X) -> f#(X, b(), b()), f#(X1, active X2, X3) -> f#(X1, X2, X3)) (active# f(a(), X, X) -> f#(X, b(), b()), f#(mark X1, X2, X3) -> f#(X1, X2, X3)) (active# f(a(), X, X) -> f#(X, b(), b()), f#(active X1, X2, X3) -> f#(X1, X2, X3)) (mark# f(X1, X2, X3) -> mark# X2, mark# f(X1, X2, X3) -> mark# X2) (mark# f(X1, X2, X3) -> mark# X2, mark# f(X1, X2, X3) -> f#(X1, mark X2, X3)) (mark# f(X1, X2, X3) -> mark# X2, mark# f(X1, X2, X3) -> active# f(X1, mark X2, X3)) (mark# f(X1, X2, X3) -> mark# X2, mark# b() -> active# b()) (mark# f(X1, X2, X3) -> mark# X2, mark# a() -> active# a()) (f#(mark X1, X2, X3) -> f#(X1, X2, X3), f#(X1, X2, mark X3) -> f#(X1, X2, X3)) (f#(mark X1, X2, X3) -> f#(X1, X2, X3), f#(X1, X2, active X3) -> f#(X1, X2, X3)) (f#(mark X1, X2, X3) -> f#(X1, X2, X3), f#(X1, mark X2, X3) -> f#(X1, X2, X3)) (f#(mark X1, X2, X3) -> f#(X1, X2, X3), f#(X1, active X2, X3) -> f#(X1, X2, X3)) (f#(mark X1, X2, X3) -> f#(X1, X2, X3), f#(mark X1, X2, X3) -> f#(X1, X2, X3)) (f#(mark X1, X2, X3) -> f#(X1, X2, X3), f#(active X1, X2, X3) -> f#(X1, X2, X3)) (f#(X1, mark X2, X3) -> f#(X1, X2, X3), f#(X1, X2, mark X3) -> f#(X1, X2, X3)) (f#(X1, mark X2, X3) -> f#(X1, X2, X3), f#(X1, X2, active X3) -> f#(X1, X2, X3)) (f#(X1, mark X2, X3) -> f#(X1, X2, X3), f#(X1, mark X2, X3) -> f#(X1, X2, X3)) (f#(X1, mark X2, X3) -> f#(X1, X2, X3), f#(X1, active X2, X3) -> f#(X1, X2, X3)) (f#(X1, mark X2, X3) -> f#(X1, X2, X3), f#(mark X1, X2, X3) -> f#(X1, X2, X3)) (f#(X1, mark X2, X3) -> f#(X1, X2, X3), f#(active X1, X2, X3) -> f#(X1, X2, X3)) (f#(X1, X2, mark X3) -> f#(X1, X2, X3), f#(X1, X2, mark X3) -> f#(X1, X2, X3)) (f#(X1, X2, mark X3) -> f#(X1, X2, X3), f#(X1, X2, active X3) -> f#(X1, X2, X3)) (f#(X1, X2, mark X3) -> f#(X1, X2, X3), f#(X1, mark X2, X3) -> f#(X1, X2, X3)) (f#(X1, X2, mark X3) -> f#(X1, X2, X3), f#(X1, active X2, X3) -> f#(X1, X2, X3)) (f#(X1, X2, mark X3) -> f#(X1, X2, X3), f#(mark X1, X2, X3) -> f#(X1, X2, X3)) (f#(X1, X2, mark X3) -> f#(X1, X2, X3), f#(active X1, X2, X3) -> f#(X1, X2, X3)) (mark# f(X1, X2, X3) -> active# f(X1, mark X2, X3), active# f(a(), X, X) -> mark# f(X, b(), b())) (mark# f(X1, X2, X3) -> active# f(X1, mark X2, X3), active# f(a(), X, X) -> f#(X, b(), b())) (mark# f(X1, X2, X3) -> active# f(X1, mark X2, X3), active# b() -> mark# a())} EDG: {(mark# f(X1, X2, X3) -> f#(X1, mark X2, X3), f#(X1, active X2, X3) -> f#(X1, X2, X3)) (mark# f(X1, X2, X3) -> f#(X1, mark X2, X3), f#(X1, mark X2, X3) -> f#(X1, X2, X3)) (f#(X1, X2, active X3) -> f#(X1, X2, X3), f#(active X1, X2, X3) -> f#(X1, X2, X3)) (f#(X1, X2, active X3) -> f#(X1, X2, X3), f#(mark X1, X2, X3) -> f#(X1, X2, X3)) (f#(X1, X2, active X3) -> f#(X1, X2, X3), f#(X1, active X2, X3) -> f#(X1, X2, X3)) (f#(X1, X2, active X3) -> f#(X1, X2, X3), f#(X1, mark X2, X3) -> f#(X1, X2, X3)) (f#(X1, X2, active X3) -> f#(X1, X2, X3), f#(X1, X2, active X3) -> f#(X1, X2, X3)) (f#(X1, X2, active X3) -> f#(X1, X2, X3), f#(X1, X2, mark X3) -> f#(X1, X2, X3)) (f#(X1, active X2, X3) -> f#(X1, X2, X3), f#(active X1, X2, X3) -> f#(X1, X2, X3)) (f#(X1, active X2, X3) -> f#(X1, X2, X3), f#(mark X1, X2, X3) -> f#(X1, X2, X3)) (f#(X1, active X2, X3) -> f#(X1, X2, X3), f#(X1, active X2, X3) -> f#(X1, X2, X3)) (f#(X1, active X2, X3) -> f#(X1, X2, X3), f#(X1, mark X2, X3) -> f#(X1, X2, X3)) (f#(X1, active X2, X3) -> f#(X1, X2, X3), f#(X1, X2, active X3) -> f#(X1, X2, X3)) (f#(X1, active X2, X3) -> f#(X1, X2, X3), f#(X1, X2, mark X3) -> f#(X1, X2, X3)) (f#(active X1, X2, X3) -> f#(X1, X2, X3), f#(active X1, X2, X3) -> f#(X1, X2, X3)) (f#(active X1, X2, X3) -> f#(X1, X2, X3), f#(mark X1, X2, X3) -> f#(X1, X2, X3)) (f#(active X1, X2, X3) -> f#(X1, X2, X3), f#(X1, active X2, X3) -> f#(X1, X2, X3)) (f#(active X1, X2, X3) -> f#(X1, X2, X3), f#(X1, mark X2, X3) -> f#(X1, X2, X3)) (f#(active X1, X2, X3) -> f#(X1, X2, X3), f#(X1, X2, active X3) -> f#(X1, X2, X3)) (f#(active X1, X2, X3) -> f#(X1, X2, X3), f#(X1, X2, mark X3) -> f#(X1, X2, X3)) (active# f(a(), X, X) -> mark# f(X, b(), b()), mark# f(X1, X2, X3) -> active# f(X1, mark X2, X3)) (active# f(a(), X, X) -> mark# f(X, b(), b()), mark# f(X1, X2, X3) -> f#(X1, mark X2, X3)) (active# f(a(), X, X) -> mark# f(X, b(), b()), mark# f(X1, X2, X3) -> mark# X2) (mark# b() -> active# b(), active# b() -> mark# a()) (active# b() -> mark# a(), mark# a() -> active# a()) (mark# f(X1, X2, X3) -> mark# X2, mark# f(X1, X2, X3) -> mark# X2) (mark# f(X1, X2, X3) -> mark# X2, mark# f(X1, X2, X3) -> f#(X1, mark X2, X3)) (mark# f(X1, X2, X3) -> mark# X2, mark# f(X1, X2, X3) -> active# f(X1, mark X2, X3)) (mark# f(X1, X2, X3) -> mark# X2, mark# b() -> active# b()) (mark# f(X1, X2, X3) -> mark# X2, mark# a() -> active# a()) (f#(mark X1, X2, X3) -> f#(X1, X2, X3), f#(X1, X2, mark X3) -> f#(X1, X2, X3)) (f#(mark X1, X2, X3) -> f#(X1, X2, X3), f#(X1, X2, active X3) -> f#(X1, X2, X3)) (f#(mark X1, X2, X3) -> f#(X1, X2, X3), f#(X1, mark X2, X3) -> f#(X1, X2, X3)) (f#(mark X1, X2, X3) -> f#(X1, X2, X3), f#(X1, active X2, X3) -> f#(X1, X2, X3)) (f#(mark X1, X2, X3) -> f#(X1, X2, X3), f#(mark X1, X2, X3) -> f#(X1, X2, X3)) (f#(mark X1, X2, X3) -> f#(X1, X2, X3), f#(active X1, X2, X3) -> f#(X1, X2, X3)) (f#(X1, mark X2, X3) -> f#(X1, X2, X3), f#(X1, X2, mark X3) -> f#(X1, X2, X3)) (f#(X1, mark X2, X3) -> f#(X1, X2, X3), f#(X1, X2, active X3) -> f#(X1, X2, X3)) (f#(X1, mark X2, X3) -> f#(X1, X2, X3), f#(X1, mark X2, X3) -> f#(X1, X2, X3)) (f#(X1, mark X2, X3) -> f#(X1, X2, X3), f#(X1, active X2, X3) -> f#(X1, X2, X3)) (f#(X1, mark X2, X3) -> f#(X1, X2, X3), f#(mark X1, X2, X3) -> f#(X1, X2, X3)) (f#(X1, mark X2, X3) -> f#(X1, X2, X3), f#(active X1, X2, X3) -> f#(X1, X2, X3)) (f#(X1, X2, mark X3) -> f#(X1, X2, X3), f#(X1, X2, mark X3) -> f#(X1, X2, X3)) (f#(X1, X2, mark X3) -> f#(X1, X2, X3), f#(X1, X2, active X3) -> f#(X1, X2, X3)) (f#(X1, X2, mark X3) -> f#(X1, X2, X3), f#(X1, mark X2, X3) -> f#(X1, X2, X3)) (f#(X1, X2, mark X3) -> f#(X1, X2, X3), f#(X1, active X2, X3) -> f#(X1, X2, X3)) (f#(X1, X2, mark X3) -> f#(X1, X2, X3), f#(mark X1, X2, X3) -> f#(X1, X2, X3)) (f#(X1, X2, mark X3) -> f#(X1, X2, X3), f#(active X1, X2, X3) -> f#(X1, X2, X3)) (mark# f(X1, X2, X3) -> active# f(X1, mark X2, X3), active# f(a(), X, X) -> mark# f(X, b(), b())) (mark# f(X1, X2, X3) -> active# f(X1, mark X2, X3), active# f(a(), X, X) -> f#(X, b(), b()))} EDG: {(mark# f(X1, X2, X3) -> f#(X1, mark X2, X3), f#(X1, active X2, X3) -> f#(X1, X2, X3)) (mark# f(X1, X2, X3) -> f#(X1, mark X2, X3), f#(X1, mark X2, X3) -> f#(X1, X2, X3)) (active# f(a(), X, X) -> mark# f(X, b(), b()), mark# f(X1, X2, X3) -> active# f(X1, mark X2, X3)) (active# f(a(), X, X) -> mark# f(X, b(), b()), mark# f(X1, X2, X3) -> f#(X1, mark X2, X3)) (active# f(a(), X, X) -> mark# f(X, b(), b()), mark# f(X1, X2, X3) -> mark# X2) (mark# b() -> active# b(), active# b() -> mark# a()) (active# b() -> mark# a(), mark# a() -> active# a()) (mark# f(X1, X2, X3) -> mark# X2, mark# f(X1, X2, X3) -> mark# X2) (mark# f(X1, X2, X3) -> mark# X2, mark# f(X1, X2, X3) -> f#(X1, mark X2, X3)) (mark# f(X1, X2, X3) -> mark# X2, mark# f(X1, X2, X3) -> active# f(X1, mark X2, X3)) (mark# f(X1, X2, X3) -> mark# X2, mark# b() -> active# b()) (mark# f(X1, X2, X3) -> mark# X2, mark# a() -> active# a()) (mark# f(X1, X2, X3) -> active# f(X1, mark X2, X3), active# f(a(), X, X) -> mark# f(X, b(), b())) (mark# f(X1, X2, X3) -> active# f(X1, mark X2, X3), active# f(a(), X, X) -> f#(X, b(), b()))} EDG: {(mark# f(X1, X2, X3) -> f#(X1, mark X2, X3), f#(X1, active X2, X3) -> f#(X1, X2, X3)) (mark# f(X1, X2, X3) -> f#(X1, mark X2, X3), f#(X1, mark X2, X3) -> f#(X1, X2, X3)) (active# f(a(), X, X) -> mark# f(X, b(), b()), mark# f(X1, X2, X3) -> active# f(X1, mark X2, X3)) (active# f(a(), X, X) -> mark# f(X, b(), b()), mark# f(X1, X2, X3) -> f#(X1, mark X2, X3)) (active# f(a(), X, X) -> mark# f(X, b(), b()), mark# f(X1, X2, X3) -> mark# X2) (mark# b() -> active# b(), active# b() -> mark# a()) (active# b() -> mark# a(), mark# a() -> active# a()) (mark# f(X1, X2, X3) -> mark# X2, mark# f(X1, X2, X3) -> mark# X2) (mark# f(X1, X2, X3) -> mark# X2, mark# f(X1, X2, X3) -> f#(X1, mark X2, X3)) (mark# f(X1, X2, X3) -> mark# X2, mark# f(X1, X2, X3) -> active# f(X1, mark X2, X3)) (mark# f(X1, X2, X3) -> mark# X2, mark# b() -> active# b()) (mark# f(X1, X2, X3) -> mark# X2, mark# a() -> active# a()) (mark# f(X1, X2, X3) -> active# f(X1, mark X2, X3), active# f(a(), X, X) -> mark# f(X, b(), b())) (mark# f(X1, X2, X3) -> active# f(X1, mark X2, X3), active# f(a(), X, X) -> f#(X, b(), b()))} STATUS: arrows: 0.928571 SCCS (1): Scc: { mark# f(X1, X2, X3) -> mark# X2, mark# f(X1, X2, X3) -> active# f(X1, mark X2, X3), active# f(a(), X, X) -> mark# f(X, b(), b())} SCC (3): Strict: { mark# f(X1, X2, X3) -> mark# X2, mark# f(X1, X2, X3) -> active# f(X1, mark X2, X3), active# f(a(), X, X) -> mark# f(X, b(), b())} Weak: { mark f(X1, X2, X3) -> active f(X1, mark X2, X3), mark b() -> active b(), mark a() -> active a(), f(X1, X2, mark X3) -> f(X1, X2, X3), f(X1, X2, active X3) -> f(X1, X2, X3), f(X1, mark X2, X3) -> f(X1, X2, X3), f(X1, active X2, X3) -> f(X1, X2, X3), f(mark X1, X2, X3) -> f(X1, X2, X3), f(active X1, X2, X3) -> f(X1, X2, X3), active f(a(), X, X) -> mark f(X, b(), b()), active b() -> mark a()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [f](x0, x1, x2) = x0 + x1 + 1, [mark](x0) = x0, [active](x0) = x0, [b] = 1, [a] = 1, [mark#](x0) = x0, [active#](x0) = x0 Strict: active# f(a(), X, X) -> mark# f(X, b(), b()) 2 + 1X >= 2 + 1X mark# f(X1, X2, X3) -> active# f(X1, mark X2, X3) 1 + 1X1 + 1X2 + 0X3 >= 1 + 1X1 + 1X2 + 0X3 mark# f(X1, X2, X3) -> mark# X2 1 + 1X1 + 1X2 + 0X3 >= 0 + 1X2 Weak: active b() -> mark a() 1 >= 1 active f(a(), X, X) -> mark f(X, b(), b()) 2 + 1X >= 2 + 1X f(active X1, X2, X3) -> f(X1, X2, X3) 1 + 1X1 + 1X2 + 0X3 >= 1 + 1X1 + 1X2 + 0X3 f(mark X1, X2, X3) -> f(X1, X2, X3) 1 + 1X1 + 1X2 + 0X3 >= 1 + 1X1 + 1X2 + 0X3 f(X1, active X2, X3) -> f(X1, X2, X3) 1 + 1X1 + 1X2 + 0X3 >= 1 + 1X1 + 1X2 + 0X3 f(X1, mark X2, X3) -> f(X1, X2, X3) 1 + 1X1 + 1X2 + 0X3 >= 1 + 1X1 + 1X2 + 0X3 f(X1, X2, active X3) -> f(X1, X2, X3) 1 + 1X1 + 1X2 + 0X3 >= 1 + 1X1 + 1X2 + 0X3 f(X1, X2, mark X3) -> f(X1, X2, X3) 1 + 1X1 + 1X2 + 0X3 >= 1 + 1X1 + 1X2 + 0X3 mark a() -> active a() 1 >= 1 mark b() -> active b() 1 >= 1 mark f(X1, X2, X3) -> active f(X1, mark X2, X3) 1 + 1X1 + 1X2 + 0X3 >= 1 + 1X1 + 1X2 + 0X3 SCCS (1): Scc: { mark# f(X1, X2, X3) -> active# f(X1, mark X2, X3), active# f(a(), X, X) -> mark# f(X, b(), b())} SCC (2): Strict: { mark# f(X1, X2, X3) -> active# f(X1, mark X2, X3), active# f(a(), X, X) -> mark# f(X, b(), b())} Weak: { mark f(X1, X2, X3) -> active f(X1, mark X2, X3), mark b() -> active b(), mark a() -> active a(), f(X1, X2, mark X3) -> f(X1, X2, X3), f(X1, X2, active X3) -> f(X1, X2, X3), f(X1, mark X2, X3) -> f(X1, X2, X3), f(X1, active X2, X3) -> f(X1, X2, X3), f(mark X1, X2, X3) -> f(X1, X2, X3), f(active X1, X2, X3) -> f(X1, X2, X3), active f(a(), X, X) -> mark f(X, b(), b()), active b() -> mark a()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [f](x0, x1, x2) = x0 + x1, [mark](x0) = x0, [active](x0) = x0, [b] = 0, [a] = 1, [mark#](x0) = x0 + 1, [active#](x0) = x0 + 1 Strict: active# f(a(), X, X) -> mark# f(X, b(), b()) 2 + 1X >= 1 + 1X mark# f(X1, X2, X3) -> active# f(X1, mark X2, X3) 1 + 1X1 + 0X2 + 1X3 >= 1 + 1X1 + 0X2 + 1X3 Weak: active b() -> mark a() 0 >= 1 active f(a(), X, X) -> mark f(X, b(), b()) 1 + 1X >= 0 + 1X f(active X1, X2, X3) -> f(X1, X2, X3) 0 + 1X1 + 0X2 + 1X3 >= 0 + 1X1 + 0X2 + 1X3 f(mark X1, X2, X3) -> f(X1, X2, X3) 0 + 1X1 + 0X2 + 1X3 >= 0 + 1X1 + 0X2 + 1X3 f(X1, active X2, X3) -> f(X1, X2, X3) 0 + 1X1 + 0X2 + 1X3 >= 0 + 1X1 + 0X2 + 1X3 f(X1, mark X2, X3) -> f(X1, X2, X3) 0 + 1X1 + 0X2 + 1X3 >= 0 + 1X1 + 0X2 + 1X3 f(X1, X2, active X3) -> f(X1, X2, X3) 0 + 1X1 + 0X2 + 1X3 >= 0 + 1X1 + 0X2 + 1X3 f(X1, X2, mark X3) -> f(X1, X2, X3) 0 + 1X1 + 0X2 + 1X3 >= 0 + 1X1 + 0X2 + 1X3 mark a() -> active a() 1 >= 1 mark b() -> active b() 0 >= 0 mark f(X1, X2, X3) -> active f(X1, mark X2, X3) 0 + 1X1 + 0X2 + 1X3 >= 0 + 1X1 + 0X2 + 1X3 SCCS (0):