YES Time: 0.078204 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#(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()))} STATUS: arrows: 0.744898 SCCS (2): 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: { 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)} 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): SCC (6): Strict: { 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)} 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) = 0, [mark](x0) = x0, [active](x0) = x0 + 1, [b] = 0, [a] = 1, [f#](x0, x1, x2) = x0 Strict: f#(active X1, X2, X3) -> f#(X1, X2, X3) 1 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 f#(mark X1, X2, X3) -> f#(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 f#(X1, active X2, X3) -> f#(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 f#(X1, mark X2, X3) -> f#(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 f#(X1, X2, active X3) -> f#(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 f#(X1, X2, mark X3) -> f#(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 Weak: active b() -> mark a() 1 >= 1 active f(a(), X, X) -> mark f(X, b(), b()) 1 + 0X >= 0 + 0X f(active X1, X2, X3) -> f(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 f(mark X1, X2, X3) -> f(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 f(X1, active X2, X3) -> f(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 f(X1, mark X2, X3) -> f(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 f(X1, X2, active X3) -> f(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 f(X1, X2, mark X3) -> f(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 mark a() -> active a() 1 >= 2 mark b() -> active b() 0 >= 1 mark f(X1, X2, X3) -> active f(X1, mark X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 SCCS (1): Scc: { 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)} SCC (5): Strict: { 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)} 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, [mark](x0) = x0, [active](x0) = x0 + 1, [b] = 0, [a] = 1, [f#](x0, x1, x2) = x0 Strict: f#(mark X1, X2, X3) -> f#(X1, X2, X3) 0 + 0X1 + 1X2 + 0X3 >= 0 + 0X1 + 1X2 + 0X3 f#(X1, active X2, X3) -> f#(X1, X2, X3) 1 + 0X1 + 1X2 + 0X3 >= 0 + 0X1 + 1X2 + 0X3 f#(X1, mark X2, X3) -> f#(X1, X2, X3) 0 + 0X1 + 1X2 + 0X3 >= 0 + 0X1 + 1X2 + 0X3 f#(X1, X2, active X3) -> f#(X1, X2, X3) 0 + 0X1 + 1X2 + 0X3 >= 0 + 0X1 + 1X2 + 0X3 f#(X1, X2, mark X3) -> f#(X1, X2, X3) 0 + 0X1 + 1X2 + 0X3 >= 0 + 0X1 + 1X2 + 0X3 Weak: active b() -> mark a() 1 >= 1 active f(a(), X, X) -> mark f(X, b(), b()) 2 + 0X >= 0 + 1X f(active X1, X2, X3) -> f(X1, X2, X3) 1 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 f(mark X1, X2, X3) -> f(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 f(X1, active X2, X3) -> f(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 f(X1, mark X2, X3) -> f(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 f(X1, X2, active X3) -> f(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 f(X1, X2, mark X3) -> f(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 mark a() -> active a() 1 >= 2 mark b() -> active b() 0 >= 1 mark f(X1, X2, X3) -> active f(X1, mark X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 1 + 1X1 + 0X2 + 0X3 SCCS (1): Scc: { 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#(mark X1, X2, X3) -> f#(X1, X2, X3)} SCC (4): Strict: { 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#(mark X1, X2, X3) -> f#(X1, X2, X3)} 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 + 1, [b] = 1, [a] = 1, [f#](x0, x1, x2) = x0 Strict: f#(mark X1, X2, X3) -> f#(X1, X2, X3) 0 + 0X1 + 0X2 + 1X3 >= 0 + 0X1 + 0X2 + 1X3 f#(X1, mark X2, X3) -> f#(X1, X2, X3) 0 + 0X1 + 0X2 + 1X3 >= 0 + 0X1 + 0X2 + 1X3 f#(X1, X2, active X3) -> f#(X1, X2, X3) 1 + 0X1 + 0X2 + 1X3 >= 0 + 0X1 + 0X2 + 1X3 f#(X1, X2, mark X3) -> f#(X1, X2, X3) 0 + 0X1 + 0X2 + 1X3 >= 0 + 0X1 + 0X2 + 1X3 Weak: active b() -> mark a() 2 >= 1 active f(a(), X, X) -> mark f(X, b(), b()) 1 + 2X >= 2 + 0X f(active X1, X2, X3) -> f(X1, X2, X3) 0 + 0X1 + 1X2 + 1X3 >= 0 + 0X1 + 1X2 + 1X3 f(mark X1, X2, X3) -> f(X1, X2, X3) 0 + 0X1 + 1X2 + 1X3 >= 0 + 0X1 + 1X2 + 1X3 f(X1, active X2, X3) -> f(X1, X2, X3) 1 + 0X1 + 1X2 + 1X3 >= 0 + 0X1 + 1X2 + 1X3 f(X1, mark X2, X3) -> f(X1, X2, X3) 0 + 0X1 + 1X2 + 1X3 >= 0 + 0X1 + 1X2 + 1X3 f(X1, X2, active X3) -> f(X1, X2, X3) 1 + 0X1 + 1X2 + 1X3 >= 0 + 0X1 + 1X2 + 1X3 f(X1, X2, mark X3) -> f(X1, X2, X3) 0 + 0X1 + 1X2 + 1X3 >= 0 + 0X1 + 1X2 + 1X3 mark a() -> active a() 1 >= 2 mark b() -> active b() 1 >= 2 mark f(X1, X2, X3) -> active f(X1, mark X2, X3) 0 + 0X1 + 1X2 + 1X3 >= 1 + 0X1 + 1X2 + 1X3 SCCS (1): Scc: {f#(X1, X2, mark X3) -> f#(X1, X2, X3), f#(X1, mark X2, X3) -> f#(X1, X2, X3), f#(mark X1, X2, X3) -> f#(X1, X2, X3)} SCC (3): Strict: {f#(X1, X2, mark X3) -> f#(X1, X2, X3), f#(X1, mark X2, X3) -> f#(X1, X2, X3), f#(mark X1, X2, X3) -> f#(X1, X2, X3)} 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 + x2 + 1, [mark](x0) = x0 + 1, [active](x0) = 0, [b] = 1, [a] = 1, [f#](x0, x1, x2) = x0 Strict: f#(mark X1, X2, X3) -> f#(X1, X2, X3) 1 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 f#(X1, mark X2, X3) -> f#(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 f#(X1, X2, mark X3) -> f#(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 Weak: active b() -> mark a() 0 >= 2 active f(a(), X, X) -> mark f(X, b(), b()) 0 + 0X >= 4 + 1X f(active X1, X2, X3) -> f(X1, X2, X3) 1 + 0X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 f(mark X1, X2, X3) -> f(X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 f(X1, active X2, X3) -> f(X1, X2, X3) 1 + 1X1 + 0X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 f(X1, mark X2, X3) -> f(X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 f(X1, X2, active X3) -> f(X1, X2, X3) 1 + 1X1 + 1X2 + 0X3 >= 1 + 1X1 + 1X2 + 1X3 f(X1, X2, mark X3) -> f(X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 mark a() -> active a() 2 >= 0 mark b() -> active b() 2 >= 0 mark f(X1, X2, X3) -> active f(X1, mark X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 0 + 0X1 + 0X2 + 0X3 SCCS (1): Scc: {f#(X1, X2, mark X3) -> f#(X1, X2, X3), f#(X1, mark X2, X3) -> f#(X1, X2, X3)} SCC (2): Strict: {f#(X1, X2, mark X3) -> f#(X1, X2, X3), f#(X1, mark X2, X3) -> f#(X1, X2, X3)} 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 + x2 + 1, [mark](x0) = x0 + 1, [active](x0) = x0, [b] = 1, [a] = 0, [f#](x0, x1, x2) = x0 Strict: f#(X1, mark X2, X3) -> f#(X1, X2, X3) 0 + 0X1 + 0X2 + 1X3 >= 0 + 0X1 + 0X2 + 1X3 f#(X1, X2, mark X3) -> f#(X1, X2, X3) 1 + 0X1 + 0X2 + 1X3 >= 0 + 0X1 + 0X2 + 1X3 Weak: active b() -> mark a() 1 >= 1 active f(a(), X, X) -> mark f(X, b(), b()) 1 + 2X >= 4 + 1X f(active X1, X2, X3) -> f(X1, X2, X3) 1 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 f(mark X1, X2, X3) -> f(X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 f(X1, active X2, X3) -> f(X1, X2, X3) 1 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 f(X1, mark X2, X3) -> f(X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 f(X1, X2, active X3) -> f(X1, X2, X3) 1 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 f(X1, X2, mark X3) -> f(X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 mark a() -> active a() 1 >= 0 mark b() -> active b() 2 >= 1 mark f(X1, X2, X3) -> active f(X1, mark X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 2 + 1X1 + 1X2 + 1X3 SCCS (1): Scc: {f#(X1, mark X2, X3) -> f#(X1, X2, X3)} SCC (1): Strict: {f#(X1, mark X2, X3) -> f#(X1, X2, X3)} 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 + x2 + 1, [mark](x0) = x0 + 1, [active](x0) = x0, [b] = 1, [a] = 0, [f#](x0, x1, x2) = x0 Strict: f#(X1, mark X2, X3) -> f#(X1, X2, X3) 1 + 0X1 + 1X2 + 0X3 >= 0 + 0X1 + 1X2 + 0X3 Weak: active b() -> mark a() 1 >= 1 active f(a(), X, X) -> mark f(X, b(), b()) 1 + 2X >= 4 + 1X f(active X1, X2, X3) -> f(X1, X2, X3) 1 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 f(mark X1, X2, X3) -> f(X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 f(X1, active X2, X3) -> f(X1, X2, X3) 1 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 f(X1, mark X2, X3) -> f(X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 f(X1, X2, active X3) -> f(X1, X2, X3) 1 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 f(X1, X2, mark X3) -> f(X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 mark a() -> active a() 1 >= 0 mark b() -> active b() 2 >= 1 mark f(X1, X2, X3) -> active f(X1, mark X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 2 + 1X1 + 1X2 + 1X3 Qed