YES Time: 0.119914 TRS: { mark f X -> active f mark X, mark g X -> active g X, mark a() -> active a(), f mark X -> f X, f active X -> f X, g mark X -> g X, g active X -> g X, active f f a() -> mark f g f a()} DP: DP: { mark# f X -> mark# X, mark# f X -> f# mark X, mark# f X -> active# f mark X, mark# g X -> active# g X, mark# a() -> active# a(), f# mark X -> f# X, f# active X -> f# X, g# mark X -> g# X, g# active X -> g# X, active# f f a() -> mark# f g f a(), active# f f a() -> f# g f a(), active# f f a() -> g# f a()} TRS: { mark f X -> active f mark X, mark g X -> active g X, mark a() -> active a(), f mark X -> f X, f active X -> f X, g mark X -> g X, g active X -> g X, active f f a() -> mark f g f a()} EDG: {(active# f f a() -> g# f a(), g# active X -> g# X) (active# f f a() -> g# f a(), g# mark X -> g# X) (f# mark X -> f# X, f# active X -> f# X) (f# mark X -> f# X, f# mark X -> f# X) (g# mark X -> g# X, g# active X -> g# X) (g# mark X -> g# X, g# mark X -> g# X) (mark# f X -> f# mark X, f# active X -> f# X) (mark# f X -> f# mark X, f# mark X -> f# X) (mark# a() -> active# a(), active# f f a() -> g# f a()) (mark# a() -> active# a(), active# f f a() -> f# g f a()) (mark# a() -> active# a(), active# f f a() -> mark# f g f a()) (active# f f a() -> f# g f a(), f# active X -> f# X) (active# f f a() -> f# g f a(), f# mark X -> f# X) (active# f f a() -> mark# f g f a(), mark# f X -> mark# X) (active# f f a() -> mark# f g f a(), mark# f X -> f# mark X) (active# f f a() -> mark# f g f a(), mark# f X -> active# f mark X) (active# f f a() -> mark# f g f a(), mark# g X -> active# g X) (active# f f a() -> mark# f g f a(), mark# a() -> active# a()) (mark# g X -> active# g X, active# f f a() -> mark# f g f a()) (mark# g X -> active# g X, active# f f a() -> f# g f a()) (mark# g X -> active# g X, active# f f a() -> g# f a()) (g# active X -> g# X, g# mark X -> g# X) (g# active X -> g# X, g# active X -> g# X) (f# active X -> f# X, f# mark X -> f# X) (f# active X -> f# X, f# active X -> f# X) (mark# f X -> mark# X, mark# f X -> mark# X) (mark# f X -> mark# X, mark# f X -> f# mark X) (mark# f X -> mark# X, mark# f X -> active# f mark X) (mark# f X -> mark# X, mark# g X -> active# g X) (mark# f X -> mark# X, mark# a() -> active# a()) (mark# f X -> active# f mark X, active# f f a() -> mark# f g f a()) (mark# f X -> active# f mark X, active# f f a() -> f# g f a()) (mark# f X -> active# f mark X, active# f f a() -> g# f a())} STATUS: arrows: 0.770833 SCCS (3): Scc: { mark# f X -> mark# X, mark# f X -> active# f mark X, mark# g X -> active# g X, mark# a() -> active# a(), active# f f a() -> mark# f g f a()} Scc: { g# mark X -> g# X, g# active X -> g# X} Scc: { f# mark X -> f# X, f# active X -> f# X} SCC (5): Strict: { mark# f X -> mark# X, mark# f X -> active# f mark X, mark# g X -> active# g X, mark# a() -> active# a(), active# f f a() -> mark# f g f a()} Weak: { mark f X -> active f mark X, mark g X -> active g X, mark a() -> active a(), f mark X -> f X, f active X -> f X, g mark X -> g X, g active X -> g X, active f f a() -> mark f g f a()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [mark](x0) = x0, [f](x0) = x0, [g](x0) = 0, [active](x0) = x0, [a] = 1, [mark#](x0) = x0, [active#](x0) = x0 Strict: active# f f a() -> mark# f g f a() 1 >= 0 mark# a() -> active# a() 1 >= 1 mark# g X -> active# g X 0 + 0X >= 0 + 0X mark# f X -> active# f mark X 0 + 1X >= 0 + 1X mark# f X -> mark# X 0 + 1X >= 0 + 1X Weak: active f f a() -> mark f g f a() 1 >= 0 g active X -> g X 0 + 0X >= 0 + 0X g mark X -> g X 0 + 0X >= 0 + 0X f active X -> f X 0 + 1X >= 0 + 1X f mark X -> f X 0 + 1X >= 0 + 1X mark a() -> active a() 1 >= 1 mark g X -> active g X 0 + 0X >= 0 + 0X mark f X -> active f mark X 0 + 1X >= 0 + 1X SCCS (1): Scc: {mark# f X -> mark# X} SCC (1): Strict: {mark# f X -> mark# X} Weak: { mark f X -> active f mark X, mark g X -> active g X, mark a() -> active a(), f mark X -> f X, f active X -> f X, g mark X -> g X, g active X -> g X, active f f a() -> mark f g f a()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [mark](x0) = x0 + 1, [f](x0) = x0 + 1, [g](x0) = x0 + 1, [active](x0) = x0, [a] = 1, [mark#](x0) = x0 + 1 Strict: mark# f X -> mark# X 2 + 1X >= 1 + 1X Weak: active f f a() -> mark f g f a() 3 >= 5 g active X -> g X 1 + 1X >= 1 + 1X g mark X -> g X 2 + 1X >= 1 + 1X f active X -> f X 1 + 1X >= 1 + 1X f mark X -> f X 2 + 1X >= 1 + 1X mark a() -> active a() 2 >= 1 mark g X -> active g X 2 + 1X >= 1 + 1X mark f X -> active f mark X 2 + 1X >= 2 + 1X Qed SCC (2): Strict: { g# mark X -> g# X, g# active X -> g# X} Weak: { mark f X -> active f mark X, mark g X -> active g X, mark a() -> active a(), f mark X -> f X, f active X -> f X, g mark X -> g X, g active X -> g X, active f f a() -> mark f g f a()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [mark](x0) = x0 + 1, [f](x0) = 0, [g](x0) = x0 + 1, [active](x0) = x0 + 1, [a] = 1, [g#](x0) = x0 + 1 Strict: g# active X -> g# X 2 + 1X >= 1 + 1X g# mark X -> g# X 2 + 1X >= 1 + 1X Weak: active f f a() -> mark f g f a() 1 >= 1 g active X -> g X 2 + 1X >= 1 + 1X g mark X -> g X 2 + 1X >= 1 + 1X f active X -> f X 0 + 0X >= 0 + 0X f mark X -> f X 0 + 0X >= 0 + 0X mark a() -> active a() 2 >= 2 mark g X -> active g X 2 + 1X >= 2 + 1X mark f X -> active f mark X 1 + 0X >= 1 + 0X Qed SCC (2): Strict: { f# mark X -> f# X, f# active X -> f# X} Weak: { mark f X -> active f mark X, mark g X -> active g X, mark a() -> active a(), f mark X -> f X, f active X -> f X, g mark X -> g X, g active X -> g X, active f f a() -> mark f g f a()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [mark](x0) = x0 + 1, [f](x0) = 0, [g](x0) = x0 + 1, [active](x0) = x0 + 1, [a] = 1, [f#](x0) = x0 + 1 Strict: f# active X -> f# X 2 + 1X >= 1 + 1X f# mark X -> f# X 2 + 1X >= 1 + 1X Weak: active f f a() -> mark f g f a() 1 >= 1 g active X -> g X 2 + 1X >= 1 + 1X g mark X -> g X 2 + 1X >= 1 + 1X f active X -> f X 0 + 0X >= 0 + 0X f mark X -> f X 0 + 0X >= 0 + 0X mark a() -> active a() 2 >= 2 mark g X -> active g X 2 + 1X >= 2 + 1X mark f X -> active f mark X 1 + 0X >= 1 + 0X Qed