YES Time: 0.240126 TRS: { mark c X -> active c X, mark f X -> active f mark X, mark g X -> active g X, mark d X -> active d X, mark h X -> active h mark X, c mark X -> c X, c active X -> c X, f mark X -> f X, f active X -> f X, g mark X -> g X, g active X -> g X, active c X -> mark d X, active f f X -> mark c f g f X, active h X -> mark c d X, d mark X -> d X, d active X -> d X, h mark X -> h X, h active X -> h X} DP: DP: { mark# c X -> active# c X, 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# d X -> active# d X, mark# h X -> mark# X, mark# h X -> active# h mark X, mark# h X -> h# mark X, c# mark X -> c# X, c# active X -> c# X, f# mark X -> f# X, f# active X -> f# X, g# mark X -> g# X, g# active X -> g# X, active# c X -> mark# d X, active# c X -> d# X, active# f f X -> mark# c f g f X, active# f f X -> c# f g f X, active# f f X -> f# g f X, active# f f X -> g# f X, active# h X -> mark# c d X, active# h X -> c# d X, active# h X -> d# X, d# mark X -> d# X, d# active X -> d# X, h# mark X -> h# X, h# active X -> h# X} TRS: { mark c X -> active c X, mark f X -> active f mark X, mark g X -> active g X, mark d X -> active d X, mark h X -> active h mark X, c mark X -> c X, c active X -> c X, f mark X -> f X, f active X -> f X, g mark X -> g X, g active X -> g X, active c X -> mark d X, active f f X -> mark c f g f X, active h X -> mark c d X, d mark X -> d X, d active X -> d X, h mark X -> h X, h active X -> h X} EDG: {(mark# h X -> active# h mark X, active# h X -> d# X) (mark# h X -> active# h mark X, active# h X -> c# d X) (mark# h X -> active# h mark X, active# h X -> mark# c d X) (mark# h X -> active# h mark X, active# f f X -> g# f X) (mark# h X -> active# h mark X, active# f f X -> f# g f X) (mark# h X -> active# h mark X, active# f f X -> c# f g f X) (mark# h X -> active# h mark X, active# f f X -> mark# c f g f X) (mark# h X -> active# h mark X, active# c X -> d# X) (mark# h X -> active# h mark X, active# c X -> mark# d X) (active# h X -> mark# c d X, mark# h X -> h# mark X) (active# h X -> mark# c d X, mark# h X -> active# h mark X) (active# h X -> mark# c d X, mark# h X -> mark# X) (active# h X -> mark# c d X, mark# d X -> active# d X) (active# h X -> mark# c d X, mark# g X -> active# g X) (active# h X -> mark# c d X, mark# f X -> active# f mark X) (active# h X -> mark# c d X, mark# f X -> f# mark X) (active# h X -> mark# c d X, mark# f X -> mark# X) (active# h X -> mark# c d X, mark# c X -> active# c X) (mark# h X -> mark# X, mark# h X -> h# mark X) (mark# h X -> mark# X, mark# h X -> active# h mark X) (mark# h X -> mark# X, mark# h X -> mark# X) (mark# h X -> mark# X, mark# d X -> active# d X) (mark# h X -> mark# X, mark# g X -> active# g X) (mark# h X -> mark# X, mark# f X -> active# f mark X) (mark# h X -> mark# X, mark# f X -> f# mark X) (mark# h X -> mark# X, mark# f X -> mark# X) (mark# h X -> mark# X, mark# c X -> active# c X) (c# active X -> c# X, c# active X -> c# X) (c# active X -> c# X, c# mark X -> c# X) (f# active X -> f# X, f# active X -> f# X) (f# active X -> f# X, f# mark X -> f# X) (g# active X -> g# X, g# active X -> g# X) (g# active X -> g# X, g# mark X -> g# X) (d# active X -> d# X, d# active X -> d# X) (d# active X -> d# X, d# mark X -> d# X) (h# active X -> h# X, h# active X -> h# X) (h# active X -> h# X, h# mark X -> h# X) (mark# f X -> f# mark X, f# active X -> f# X) (mark# f X -> f# mark X, f# mark X -> f# X) (mark# d X -> active# d X, active# h X -> d# X) (mark# d X -> active# d X, active# h X -> c# d X) (mark# d X -> active# d X, active# h X -> mark# c d X) (mark# d X -> active# d X, active# f f X -> g# f X) (mark# d X -> active# d X, active# f f X -> f# g f X) (mark# d X -> active# d X, active# f f X -> c# f g f X) (mark# d X -> active# d X, active# f f X -> mark# c f g f X) (mark# d X -> active# d X, active# c X -> d# X) (mark# d X -> active# d X, active# c X -> mark# d X) (active# c X -> mark# d X, mark# h X -> h# mark X) (active# c X -> mark# d X, mark# h X -> active# h mark X) (active# c X -> mark# d X, mark# h X -> mark# X) (active# c X -> mark# d X, mark# d X -> active# d X) (active# c X -> mark# d X, mark# g X -> active# g X) (active# c X -> mark# d X, mark# f X -> active# f mark X) (active# c X -> mark# d X, mark# f X -> f# mark X) (active# c X -> mark# d X, mark# f X -> mark# X) (active# c X -> mark# d X, mark# c X -> active# c X) (active# h X -> c# d X, c# active X -> c# X) (active# h X -> c# d X, c# mark X -> c# X) (active# f f X -> c# f g f X, c# active X -> c# X) (active# f f X -> c# f g f X, c# mark X -> c# X) (active# f f X -> mark# c f g f X, mark# c X -> active# c X) (active# f f X -> mark# c f g f X, mark# f X -> mark# X) (active# f f X -> mark# c f g f X, mark# f X -> f# mark X) (active# f f X -> mark# c f g f X, mark# f X -> active# f mark X) (active# f f X -> mark# c f g f X, mark# g X -> active# g X) (active# f f X -> mark# c f g f X, mark# d X -> active# d X) (active# f f X -> mark# c f g f X, mark# h X -> mark# X) (active# f f X -> mark# c f g f X, mark# h X -> active# h mark X) (active# f f X -> mark# c f g f X, mark# h X -> h# mark X) (active# f f X -> g# f X, g# mark X -> g# X) (active# f f X -> g# f X, g# active X -> g# X) (mark# h X -> h# mark X, h# mark X -> h# X) (mark# h X -> h# mark X, h# active X -> h# X) (mark# g X -> active# g X, active# c X -> mark# d X) (mark# g X -> active# g X, active# c X -> d# X) (mark# g X -> active# g X, active# f f X -> mark# c f g f X) (mark# g X -> active# g X, active# f f X -> c# f g f X) (mark# g X -> active# g X, active# f f X -> f# g f X) (mark# g X -> active# g X, active# f f X -> g# f X) (mark# g X -> active# g X, active# h X -> mark# c d X) (mark# g X -> active# g X, active# h X -> c# d X) (mark# g X -> active# g X, active# h X -> d# X) (mark# c X -> active# c X, active# c X -> mark# d X) (mark# c X -> active# c X, active# c X -> d# X) (mark# c X -> active# c X, active# f f X -> mark# c f g f X) (mark# c X -> active# c X, active# f f X -> c# f g f X) (mark# c X -> active# c X, active# f f X -> f# g f X) (mark# c X -> active# c X, active# f f X -> g# f X) (mark# c X -> active# c X, active# h X -> mark# c d X) (mark# c X -> active# c X, active# h X -> c# d X) (mark# c X -> active# c X, active# h X -> d# X) (h# mark X -> h# X, h# mark X -> h# X) (h# mark X -> h# X, h# active X -> h# X) (d# mark X -> d# X, d# mark X -> d# X) (d# mark X -> d# X, d# active X -> d# X) (g# mark X -> g# X, g# mark X -> g# X) (g# mark X -> g# X, g# active X -> g# X) (f# mark X -> f# X, f# mark X -> f# X) (f# mark X -> f# X, f# active X -> f# X) (c# mark X -> c# X, c# mark X -> c# X) (c# mark X -> c# X, c# active X -> c# X) (mark# f X -> mark# X, mark# c X -> active# c 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# d X -> active# d X) (mark# f X -> mark# X, mark# h X -> mark# X) (mark# f X -> mark# X, mark# h X -> active# h mark X) (mark# f X -> mark# X, mark# h X -> h# mark X) (active# f f X -> f# g f X, f# mark X -> f# X) (active# f f X -> f# g f X, f# active X -> f# X) (mark# f X -> active# f mark X, active# c X -> mark# d X) (mark# f X -> active# f mark X, active# c X -> d# X) (mark# f X -> active# f mark X, active# f f X -> mark# c f g f X) (mark# f X -> active# f mark X, active# f f X -> c# f g f X) (mark# f X -> active# f mark X, active# f f X -> f# g f X) (mark# f X -> active# f mark X, active# f f X -> g# f X) (mark# f X -> active# f mark X, active# h X -> mark# c d X) (mark# f X -> active# f mark X, active# h X -> c# d X) (mark# f X -> active# f mark X, active# h X -> d# X)} STATUS: arrows: 0.844388 SCCS (6): Scc: { d# mark X -> d# X, d# active X -> d# X} Scc: { mark# c X -> active# c X, mark# f X -> mark# X, mark# f X -> active# f mark X, mark# g X -> active# g X, mark# d X -> active# d X, mark# h X -> mark# X, mark# h X -> active# h mark X, active# c X -> mark# d X, active# f f X -> mark# c f g f X, active# h X -> mark# c d X} Scc: { h# mark X -> h# X, h# active X -> h# X} Scc: { g# mark X -> g# X, g# active X -> g# X} Scc: { c# mark X -> c# X, c# active X -> c# X} Scc: { f# mark X -> f# X, f# active X -> f# X} SCC (2): Strict: { d# mark X -> d# X, d# active X -> d# X} Weak: { mark c X -> active c X, mark f X -> active f mark X, mark g X -> active g X, mark d X -> active d X, mark h X -> active h mark X, c mark X -> c X, c active X -> c X, f mark X -> f X, f active X -> f X, g mark X -> g X, g active X -> g X, active c X -> mark d X, active f f X -> mark c f g f X, active h X -> mark c d X, d mark X -> d X, d active X -> d X, h mark X -> h X, h active X -> h X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [mark](x0) = x0, [c](x0) = 0, [f](x0) = 0, [g](x0) = 0, [active](x0) = x0 + 1, [d](x0) = x0 + 1, [h](x0) = 0, [d#](x0) = x0 Strict: d# active X -> d# X 1 + 1X >= 0 + 1X d# mark X -> d# X 0 + 1X >= 0 + 1X Weak: h active X -> h X 0 + 0X >= 0 + 0X h mark X -> h X 0 + 0X >= 0 + 0X d active X -> d X 2 + 1X >= 1 + 1X d mark X -> d X 1 + 1X >= 1 + 1X active h X -> mark c d X 1 + 0X >= 0 + 0X active f f X -> mark c f g f X 1 + 0X >= 0 + 0X active c X -> mark d X 1 + 0X >= 1 + 1X g active X -> g X 0 + 0X >= 0 + 0X g mark X -> g X 0 + 0X >= 0 + 0X f active X -> f X 0 + 0X >= 0 + 0X f mark X -> f X 0 + 0X >= 0 + 0X c active X -> c X 0 + 0X >= 0 + 0X c mark X -> c X 0 + 0X >= 0 + 0X mark h X -> active h mark X 0 + 0X >= 1 + 0X mark d X -> active d X 1 + 1X >= 2 + 1X mark g X -> active g X 0 + 0X >= 1 + 0X mark f X -> active f mark X 0 + 0X >= 1 + 0X mark c X -> active c X 0 + 0X >= 1 + 0X SCCS (1): Scc: {d# mark X -> d# X} SCC (1): Strict: {d# mark X -> d# X} Weak: { mark c X -> active c X, mark f X -> active f mark X, mark g X -> active g X, mark d X -> active d X, mark h X -> active h mark X, c mark X -> c X, c active X -> c X, f mark X -> f X, f active X -> f X, g mark X -> g X, g active X -> g X, active c X -> mark d X, active f f X -> mark c f g f X, active h X -> mark c d X, d mark X -> d X, d active X -> d X, h mark X -> h X, h active X -> h X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [mark](x0) = x0 + 1, [c](x0) = x0 + 1, [f](x0) = x0 + 1, [g](x0) = x0 + 1, [active](x0) = x0, [d](x0) = 0, [h](x0) = x0 + 1, [d#](x0) = x0 Strict: d# mark X -> d# X 1 + 1X >= 0 + 1X Weak: h active X -> h X 1 + 1X >= 1 + 1X h mark X -> h X 2 + 1X >= 1 + 1X d active X -> d X 0 + 0X >= 0 + 0X d mark X -> d X 0 + 0X >= 0 + 0X active h X -> mark c d X 1 + 1X >= 2 + 0X active f f X -> mark c f g f X 2 + 1X >= 5 + 1X active c X -> mark d X 1 + 1X >= 1 + 0X 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 c active X -> c X 1 + 1X >= 1 + 1X c mark X -> c X 2 + 1X >= 1 + 1X mark h X -> active h mark X 2 + 1X >= 2 + 1X mark d X -> active d X 1 + 0X >= 0 + 0X mark g X -> active g X 2 + 1X >= 1 + 1X mark f X -> active f mark X 2 + 1X >= 2 + 1X mark c X -> active c X 2 + 1X >= 1 + 1X Qed SCC (10): Strict: { mark# c X -> active# c X, mark# f X -> mark# X, mark# f X -> active# f mark X, mark# g X -> active# g X, mark# d X -> active# d X, mark# h X -> mark# X, mark# h X -> active# h mark X, active# c X -> mark# d X, active# f f X -> mark# c f g f X, active# h X -> mark# c d X} Weak: { mark c X -> active c X, mark f X -> active f mark X, mark g X -> active g X, mark d X -> active d X, mark h X -> active h mark X, c mark X -> c X, c active X -> c X, f mark X -> f X, f active X -> f X, g mark X -> g X, g active X -> g X, active c X -> mark d X, active f f X -> mark c f g f X, active h X -> mark c d X, d mark X -> d X, d active X -> d X, h mark X -> h X, h active X -> h X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [mark](x0) = x0, [c](x0) = 0, [f](x0) = x0 + 1, [g](x0) = 0, [active](x0) = x0, [d](x0) = 0, [h](x0) = x0, [mark#](x0) = x0, [active#](x0) = x0 Strict: active# h X -> mark# c d X 0 + 1X >= 0 + 0X active# f f X -> mark# c f g f X 2 + 1X >= 0 + 0X active# c X -> mark# d X 0 + 0X >= 0 + 0X mark# h X -> active# h mark X 0 + 1X >= 0 + 1X mark# h X -> mark# X 0 + 1X >= 0 + 1X mark# d X -> active# d X 0 + 0X >= 0 + 0X mark# g X -> active# g X 0 + 0X >= 0 + 0X mark# f X -> active# f mark X 1 + 1X >= 1 + 1X mark# f X -> mark# X 1 + 1X >= 0 + 1X mark# c X -> active# c X 0 + 0X >= 0 + 0X Weak: h active X -> h X 0 + 1X >= 0 + 1X h mark X -> h X 0 + 1X >= 0 + 1X d active X -> d X 0 + 0X >= 0 + 0X d mark X -> d X 0 + 0X >= 0 + 0X active h X -> mark c d X 0 + 1X >= 0 + 0X active f f X -> mark c f g f X 2 + 1X >= 0 + 0X active c X -> mark d X 0 + 0X >= 0 + 0X g active X -> g X 0 + 0X >= 0 + 0X g mark X -> g X 0 + 0X >= 0 + 0X f active X -> f X 1 + 1X >= 1 + 1X f mark X -> f X 1 + 1X >= 1 + 1X c active X -> c X 0 + 0X >= 0 + 0X c mark X -> c X 0 + 0X >= 0 + 0X mark h X -> active h mark X 0 + 1X >= 0 + 1X mark d X -> active d X 0 + 0X >= 0 + 0X mark g X -> active g X 0 + 0X >= 0 + 0X mark f X -> active f mark X 1 + 1X >= 1 + 1X mark c X -> active c X 0 + 0X >= 0 + 0X SCCS (1): Scc: { mark# c X -> active# c X, mark# f X -> active# f mark X, mark# g X -> active# g X, mark# d X -> active# d X, mark# h X -> mark# X, mark# h X -> active# h mark X, active# c X -> mark# d X, active# h X -> mark# c d X} SCC (8): Strict: { mark# c X -> active# c X, mark# f X -> active# f mark X, mark# g X -> active# g X, mark# d X -> active# d X, mark# h X -> mark# X, mark# h X -> active# h mark X, active# c X -> mark# d X, active# h X -> mark# c d X} Weak: { mark c X -> active c X, mark f X -> active f mark X, mark g X -> active g X, mark d X -> active d X, mark h X -> active h mark X, c mark X -> c X, c active X -> c X, f mark X -> f X, f active X -> f X, g mark X -> g X, g active X -> g X, active c X -> mark d X, active f f X -> mark c f g f X, active h X -> mark c d X, d mark X -> d X, d active X -> d X, h mark X -> h X, h active X -> h X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [mark](x0) = x0, [c](x0) = x0, [f](x0) = 0, [g](x0) = 1, [active](x0) = x0, [d](x0) = 0, [h](x0) = x0, [mark#](x0) = x0, [active#](x0) = 0 Strict: active# h X -> mark# c d X 0 + 0X >= 0 + 0X active# c X -> mark# d X 0 + 0X >= 0 + 0X mark# h X -> active# h mark X 0 + 1X >= 0 + 0X mark# h X -> mark# X 0 + 1X >= 0 + 1X mark# d X -> active# d X 0 + 0X >= 0 + 0X mark# g X -> active# g X 1 + 0X >= 0 + 0X mark# f X -> active# f mark X 0 + 0X >= 0 + 0X mark# c X -> active# c X 0 + 1X >= 0 + 0X Weak: h active X -> h X 0 + 1X >= 0 + 1X h mark X -> h X 0 + 1X >= 0 + 1X d active X -> d X 0 + 0X >= 0 + 0X d mark X -> d X 0 + 0X >= 0 + 0X active h X -> mark c d X 0 + 1X >= 0 + 0X active f f X -> mark c f g f X 0 + 0X >= 0 + 0X active c X -> mark d X 0 + 1X >= 0 + 0X g active X -> g X 1 + 0X >= 1 + 0X g mark X -> g X 1 + 0X >= 1 + 0X f active X -> f X 0 + 0X >= 0 + 0X f mark X -> f X 0 + 0X >= 0 + 0X c active X -> c X 0 + 1X >= 0 + 1X c mark X -> c X 0 + 1X >= 0 + 1X mark h X -> active h mark X 0 + 1X >= 0 + 1X mark d X -> active d X 0 + 0X >= 0 + 0X mark g X -> active g X 1 + 0X >= 1 + 0X mark f X -> active f mark X 0 + 0X >= 0 + 0X mark c X -> active c X 0 + 1X >= 0 + 1X SCCS (1): Scc: { mark# c X -> active# c X, mark# f X -> active# f mark X, mark# d X -> active# d X, mark# h X -> mark# X, mark# h X -> active# h mark X, active# c X -> mark# d X, active# h X -> mark# c d X} SCC (7): Strict: { mark# c X -> active# c X, mark# f X -> active# f mark X, mark# d X -> active# d X, mark# h X -> mark# X, mark# h X -> active# h mark X, active# c X -> mark# d X, active# h X -> mark# c d X} Weak: { mark c X -> active c X, mark f X -> active f mark X, mark g X -> active g X, mark d X -> active d X, mark h X -> active h mark X, c mark X -> c X, c active X -> c X, f mark X -> f X, f active X -> f X, g mark X -> g X, g active X -> g X, active c X -> mark d X, active f f X -> mark c f g f X, active h X -> mark c d X, d mark X -> d X, d active X -> d X, h mark X -> h X, h active X -> h X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [mark](x0) = 0, [c](x0) = 0, [f](x0) = 1, [g](x0) = 0, [active](x0) = 0, [d](x0) = 0, [h](x0) = x0, [mark#](x0) = x0, [active#](x0) = 0 Strict: active# h X -> mark# c d X 0 + 0X >= 0 + 0X active# c X -> mark# d X 0 + 0X >= 0 + 0X mark# h X -> active# h mark X 0 + 1X >= 0 + 0X mark# h X -> mark# X 0 + 1X >= 0 + 1X mark# d X -> active# d X 0 + 0X >= 0 + 0X mark# f X -> active# f mark X 1 + 0X >= 0 + 0X mark# c X -> active# c X 0 + 0X >= 0 + 0X Weak: h active X -> h X 0 + 0X >= 0 + 1X h mark X -> h X 0 + 0X >= 0 + 1X d active X -> d X 0 + 0X >= 0 + 0X d mark X -> d X 0 + 0X >= 0 + 0X active h X -> mark c d X 0 + 0X >= 0 + 0X active f f X -> mark c f g f X 0 + 0X >= 0 + 0X active c X -> mark d X 0 + 0X >= 0 + 0X g active X -> g X 0 + 0X >= 0 + 0X g mark X -> g X 0 + 0X >= 0 + 0X f active X -> f X 1 + 0X >= 1 + 0X f mark X -> f X 1 + 0X >= 1 + 0X c active X -> c X 0 + 0X >= 0 + 0X c mark X -> c X 0 + 0X >= 0 + 0X mark h X -> active h mark X 0 + 0X >= 0 + 0X mark d X -> active d X 0 + 0X >= 0 + 0X mark g X -> active g X 0 + 0X >= 0 + 0X mark f X -> active f mark X 0 + 0X >= 0 + 0X mark c X -> active c X 0 + 0X >= 0 + 0X SCCS (1): Scc: { mark# c X -> active# c X, mark# d X -> active# d X, mark# h X -> mark# X, mark# h X -> active# h mark X, active# c X -> mark# d X, active# h X -> mark# c d X} SCC (6): Strict: { mark# c X -> active# c X, mark# d X -> active# d X, mark# h X -> mark# X, mark# h X -> active# h mark X, active# c X -> mark# d X, active# h X -> mark# c d X} Weak: { mark c X -> active c X, mark f X -> active f mark X, mark g X -> active g X, mark d X -> active d X, mark h X -> active h mark X, c mark X -> c X, c active X -> c X, f mark X -> f X, f active X -> f X, g mark X -> g X, g active X -> g X, active c X -> mark d X, active f f X -> mark c f g f X, active h X -> mark c d X, d mark X -> d X, d active X -> d X, h mark X -> h X, h active X -> h X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [mark](x0) = 0, [c](x0) = 0, [f](x0) = 0, [g](x0) = 0, [active](x0) = 0, [d](x0) = 0, [h](x0) = x0 + 1, [mark#](x0) = x0, [active#](x0) = 0 Strict: active# h X -> mark# c d X 0 + 0X >= 0 + 0X active# c X -> mark# d X 0 + 0X >= 0 + 0X mark# h X -> active# h mark X 1 + 1X >= 0 + 0X mark# h X -> mark# X 1 + 1X >= 0 + 1X mark# d X -> active# d X 0 + 0X >= 0 + 0X mark# c X -> active# c X 0 + 0X >= 0 + 0X Weak: h active X -> h X 1 + 0X >= 1 + 1X h mark X -> h X 1 + 0X >= 1 + 1X d active X -> d X 0 + 0X >= 0 + 0X d mark X -> d X 0 + 0X >= 0 + 0X active h X -> mark c d X 0 + 0X >= 0 + 0X active f f X -> mark c f g f X 0 + 0X >= 0 + 0X active c X -> mark d X 0 + 0X >= 0 + 0X g active X -> g X 0 + 0X >= 0 + 0X g mark X -> g X 0 + 0X >= 0 + 0X f active X -> f X 0 + 0X >= 0 + 0X f mark X -> f X 0 + 0X >= 0 + 0X c active X -> c X 0 + 0X >= 0 + 0X c mark X -> c X 0 + 0X >= 0 + 0X mark h X -> active h mark X 0 + 0X >= 0 + 0X mark d X -> active d X 0 + 0X >= 0 + 0X mark g X -> active g X 0 + 0X >= 0 + 0X mark f X -> active f mark X 0 + 0X >= 0 + 0X mark c X -> active c X 0 + 0X >= 0 + 0X SCCS (1): Scc: { mark# c X -> active# c X, mark# d X -> active# d X, active# c X -> mark# d X, active# h X -> mark# c d X} SCC (4): Strict: { mark# c X -> active# c X, mark# d X -> active# d X, active# c X -> mark# d X, active# h X -> mark# c d X} Weak: { mark c X -> active c X, mark f X -> active f mark X, mark g X -> active g X, mark d X -> active d X, mark h X -> active h mark X, c mark X -> c X, c active X -> c X, f mark X -> f X, f active X -> f X, g mark X -> g X, g active X -> g X, active c X -> mark d X, active f f X -> mark c f g f X, active h X -> mark c d X, d mark X -> d X, d active X -> d X, h mark X -> h X, h active X -> h X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [mark](x0) = 0, [c](x0) = 0, [f](x0) = 0, [g](x0) = 0, [active](x0) = 0, [d](x0) = 0, [h](x0) = 1, [mark#](x0) = 0, [active#](x0) = x0 Strict: active# h X -> mark# c d X 1 + 0X >= 0 + 0X active# c X -> mark# d X 0 + 0X >= 0 + 0X mark# d X -> active# d X 0 + 0X >= 0 + 0X mark# c X -> active# c X 0 + 0X >= 0 + 0X Weak: h active X -> h X 1 + 0X >= 1 + 0X h mark X -> h X 1 + 0X >= 1 + 0X d active X -> d X 0 + 0X >= 0 + 0X d mark X -> d X 0 + 0X >= 0 + 0X active h X -> mark c d X 0 + 0X >= 0 + 0X active f f X -> mark c f g f X 0 + 0X >= 0 + 0X active c X -> mark d X 0 + 0X >= 0 + 0X g active X -> g X 0 + 0X >= 0 + 0X g mark X -> g X 0 + 0X >= 0 + 0X f active X -> f X 0 + 0X >= 0 + 0X f mark X -> f X 0 + 0X >= 0 + 0X c active X -> c X 0 + 0X >= 0 + 0X c mark X -> c X 0 + 0X >= 0 + 0X mark h X -> active h mark X 0 + 0X >= 0 + 0X mark d X -> active d X 0 + 0X >= 0 + 0X mark g X -> active g X 0 + 0X >= 0 + 0X mark f X -> active f mark X 0 + 0X >= 0 + 0X mark c X -> active c X 0 + 0X >= 0 + 0X SCCS (1): Scc: { mark# c X -> active# c X, mark# d X -> active# d X, active# c X -> mark# d X} SCC (3): Strict: { mark# c X -> active# c X, mark# d X -> active# d X, active# c X -> mark# d X} Weak: { mark c X -> active c X, mark f X -> active f mark X, mark g X -> active g X, mark d X -> active d X, mark h X -> active h mark X, c mark X -> c X, c active X -> c X, f mark X -> f X, f active X -> f X, g mark X -> g X, g active X -> g X, active c X -> mark d X, active f f X -> mark c f g f X, active h X -> mark c d X, d mark X -> d X, d active X -> d X, h mark X -> h X, h active X -> h X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [mark](x0) = x0 + 1, [c](x0) = 1, [f](x0) = x0 + 1, [g](x0) = x0 + 1, [active](x0) = x0, [d](x0) = 0, [h](x0) = 0, [mark#](x0) = x0 + 1, [active#](x0) = x0 + 1 Strict: active# c X -> mark# d X 2 + 0X >= 1 + 0X mark# d X -> active# d X 1 + 0X >= 1 + 0X mark# c X -> active# c X 2 + 0X >= 2 + 0X Weak: h active X -> h X 0 + 0X >= 0 + 0X h mark X -> h X 0 + 0X >= 0 + 0X d active X -> d X 0 + 0X >= 0 + 0X d mark X -> d X 0 + 0X >= 0 + 0X active h X -> mark c d X 0 + 0X >= 2 + 0X active f f X -> mark c f g f X 2 + 1X >= 2 + 0X active c X -> mark d X 1 + 0X >= 1 + 0X 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 c active X -> c X 1 + 0X >= 1 + 0X c mark X -> c X 1 + 0X >= 1 + 0X mark h X -> active h mark X 1 + 0X >= 0 + 0X mark d X -> active d X 1 + 0X >= 0 + 0X mark g X -> active g X 2 + 1X >= 1 + 1X mark f X -> active f mark X 2 + 1X >= 2 + 1X mark c X -> active c X 2 + 0X >= 1 + 0X SCCS (0): SCC (2): Strict: { h# mark X -> h# X, h# active X -> h# X} Weak: { mark c X -> active c X, mark f X -> active f mark X, mark g X -> active g X, mark d X -> active d X, mark h X -> active h mark X, c mark X -> c X, c active X -> c X, f mark X -> f X, f active X -> f X, g mark X -> g X, g active X -> g X, active c X -> mark d X, active f f X -> mark c f g f X, active h X -> mark c d X, d mark X -> d X, d active X -> d X, h mark X -> h X, h active X -> h X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [mark](x0) = x0, [c](x0) = 0, [f](x0) = 0, [g](x0) = 0, [active](x0) = x0 + 1, [d](x0) = x0 + 1, [h](x0) = 0, [h#](x0) = x0 Strict: h# active X -> h# X 1 + 1X >= 0 + 1X h# mark X -> h# X 0 + 1X >= 0 + 1X Weak: h active X -> h X 0 + 0X >= 0 + 0X h mark X -> h X 0 + 0X >= 0 + 0X d active X -> d X 2 + 1X >= 1 + 1X d mark X -> d X 1 + 1X >= 1 + 1X active h X -> mark c d X 1 + 0X >= 0 + 0X active f f X -> mark c f g f X 1 + 0X >= 0 + 0X active c X -> mark d X 1 + 0X >= 1 + 1X g active X -> g X 0 + 0X >= 0 + 0X g mark X -> g X 0 + 0X >= 0 + 0X f active X -> f X 0 + 0X >= 0 + 0X f mark X -> f X 0 + 0X >= 0 + 0X c active X -> c X 0 + 0X >= 0 + 0X c mark X -> c X 0 + 0X >= 0 + 0X mark h X -> active h mark X 0 + 0X >= 1 + 0X mark d X -> active d X 1 + 1X >= 2 + 1X mark g X -> active g X 0 + 0X >= 1 + 0X mark f X -> active f mark X 0 + 0X >= 1 + 0X mark c X -> active c X 0 + 0X >= 1 + 0X SCCS (1): Scc: {h# mark X -> h# X} SCC (1): Strict: {h# mark X -> h# X} Weak: { mark c X -> active c X, mark f X -> active f mark X, mark g X -> active g X, mark d X -> active d X, mark h X -> active h mark X, c mark X -> c X, c active X -> c X, f mark X -> f X, f active X -> f X, g mark X -> g X, g active X -> g X, active c X -> mark d X, active f f X -> mark c f g f X, active h X -> mark c d X, d mark X -> d X, d active X -> d X, h mark X -> h X, h active X -> h X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [mark](x0) = x0 + 1, [c](x0) = x0 + 1, [f](x0) = x0 + 1, [g](x0) = x0 + 1, [active](x0) = x0, [d](x0) = 0, [h](x0) = x0 + 1, [h#](x0) = x0 Strict: h# mark X -> h# X 1 + 1X >= 0 + 1X Weak: h active X -> h X 1 + 1X >= 1 + 1X h mark X -> h X 2 + 1X >= 1 + 1X d active X -> d X 0 + 0X >= 0 + 0X d mark X -> d X 0 + 0X >= 0 + 0X active h X -> mark c d X 1 + 1X >= 2 + 0X active f f X -> mark c f g f X 2 + 1X >= 5 + 1X active c X -> mark d X 1 + 1X >= 1 + 0X 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 c active X -> c X 1 + 1X >= 1 + 1X c mark X -> c X 2 + 1X >= 1 + 1X mark h X -> active h mark X 2 + 1X >= 2 + 1X mark d X -> active d X 1 + 0X >= 0 + 0X mark g X -> active g X 2 + 1X >= 1 + 1X mark f X -> active f mark X 2 + 1X >= 2 + 1X mark c X -> active c X 2 + 1X >= 1 + 1X Qed SCC (2): Strict: { g# mark X -> g# X, g# active X -> g# X} Weak: { mark c X -> active c X, mark f X -> active f mark X, mark g X -> active g X, mark d X -> active d X, mark h X -> active h mark X, c mark X -> c X, c active X -> c X, f mark X -> f X, f active X -> f X, g mark X -> g X, g active X -> g X, active c X -> mark d X, active f f X -> mark c f g f X, active h X -> mark c d X, d mark X -> d X, d active X -> d X, h mark X -> h X, h active X -> h X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [mark](x0) = x0, [c](x0) = 0, [f](x0) = 0, [g](x0) = 0, [active](x0) = x0 + 1, [d](x0) = x0 + 1, [h](x0) = 0, [g#](x0) = x0 Strict: g# active X -> g# X 1 + 1X >= 0 + 1X g# mark X -> g# X 0 + 1X >= 0 + 1X Weak: h active X -> h X 0 + 0X >= 0 + 0X h mark X -> h X 0 + 0X >= 0 + 0X d active X -> d X 2 + 1X >= 1 + 1X d mark X -> d X 1 + 1X >= 1 + 1X active h X -> mark c d X 1 + 0X >= 0 + 0X active f f X -> mark c f g f X 1 + 0X >= 0 + 0X active c X -> mark d X 1 + 0X >= 1 + 1X g active X -> g X 0 + 0X >= 0 + 0X g mark X -> g X 0 + 0X >= 0 + 0X f active X -> f X 0 + 0X >= 0 + 0X f mark X -> f X 0 + 0X >= 0 + 0X c active X -> c X 0 + 0X >= 0 + 0X c mark X -> c X 0 + 0X >= 0 + 0X mark h X -> active h mark X 0 + 0X >= 1 + 0X mark d X -> active d X 1 + 1X >= 2 + 1X mark g X -> active g X 0 + 0X >= 1 + 0X mark f X -> active f mark X 0 + 0X >= 1 + 0X mark c X -> active c X 0 + 0X >= 1 + 0X SCCS (1): Scc: {g# mark X -> g# X} SCC (1): Strict: {g# mark X -> g# X} Weak: { mark c X -> active c X, mark f X -> active f mark X, mark g X -> active g X, mark d X -> active d X, mark h X -> active h mark X, c mark X -> c X, c active X -> c X, f mark X -> f X, f active X -> f X, g mark X -> g X, g active X -> g X, active c X -> mark d X, active f f X -> mark c f g f X, active h X -> mark c d X, d mark X -> d X, d active X -> d X, h mark X -> h X, h active X -> h X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [mark](x0) = x0 + 1, [c](x0) = x0 + 1, [f](x0) = x0 + 1, [g](x0) = x0 + 1, [active](x0) = x0, [d](x0) = 0, [h](x0) = x0 + 1, [g#](x0) = x0 Strict: g# mark X -> g# X 1 + 1X >= 0 + 1X Weak: h active X -> h X 1 + 1X >= 1 + 1X h mark X -> h X 2 + 1X >= 1 + 1X d active X -> d X 0 + 0X >= 0 + 0X d mark X -> d X 0 + 0X >= 0 + 0X active h X -> mark c d X 1 + 1X >= 2 + 0X active f f X -> mark c f g f X 2 + 1X >= 5 + 1X active c X -> mark d X 1 + 1X >= 1 + 0X 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 c active X -> c X 1 + 1X >= 1 + 1X c mark X -> c X 2 + 1X >= 1 + 1X mark h X -> active h mark X 2 + 1X >= 2 + 1X mark d X -> active d X 1 + 0X >= 0 + 0X mark g X -> active g X 2 + 1X >= 1 + 1X mark f X -> active f mark X 2 + 1X >= 2 + 1X mark c X -> active c X 2 + 1X >= 1 + 1X Qed SCC (2): Strict: { c# mark X -> c# X, c# active X -> c# X} Weak: { mark c X -> active c X, mark f X -> active f mark X, mark g X -> active g X, mark d X -> active d X, mark h X -> active h mark X, c mark X -> c X, c active X -> c X, f mark X -> f X, f active X -> f X, g mark X -> g X, g active X -> g X, active c X -> mark d X, active f f X -> mark c f g f X, active h X -> mark c d X, d mark X -> d X, d active X -> d X, h mark X -> h X, h active X -> h X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [mark](x0) = x0, [c](x0) = 0, [f](x0) = 0, [g](x0) = 0, [active](x0) = x0 + 1, [d](x0) = x0 + 1, [h](x0) = 0, [c#](x0) = x0 Strict: c# active X -> c# X 1 + 1X >= 0 + 1X c# mark X -> c# X 0 + 1X >= 0 + 1X Weak: h active X -> h X 0 + 0X >= 0 + 0X h mark X -> h X 0 + 0X >= 0 + 0X d active X -> d X 2 + 1X >= 1 + 1X d mark X -> d X 1 + 1X >= 1 + 1X active h X -> mark c d X 1 + 0X >= 0 + 0X active f f X -> mark c f g f X 1 + 0X >= 0 + 0X active c X -> mark d X 1 + 0X >= 1 + 1X g active X -> g X 0 + 0X >= 0 + 0X g mark X -> g X 0 + 0X >= 0 + 0X f active X -> f X 0 + 0X >= 0 + 0X f mark X -> f X 0 + 0X >= 0 + 0X c active X -> c X 0 + 0X >= 0 + 0X c mark X -> c X 0 + 0X >= 0 + 0X mark h X -> active h mark X 0 + 0X >= 1 + 0X mark d X -> active d X 1 + 1X >= 2 + 1X mark g X -> active g X 0 + 0X >= 1 + 0X mark f X -> active f mark X 0 + 0X >= 1 + 0X mark c X -> active c X 0 + 0X >= 1 + 0X SCCS (1): Scc: {c# mark X -> c# X} SCC (1): Strict: {c# mark X -> c# X} Weak: { mark c X -> active c X, mark f X -> active f mark X, mark g X -> active g X, mark d X -> active d X, mark h X -> active h mark X, c mark X -> c X, c active X -> c X, f mark X -> f X, f active X -> f X, g mark X -> g X, g active X -> g X, active c X -> mark d X, active f f X -> mark c f g f X, active h X -> mark c d X, d mark X -> d X, d active X -> d X, h mark X -> h X, h active X -> h X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [mark](x0) = x0 + 1, [c](x0) = x0 + 1, [f](x0) = x0 + 1, [g](x0) = x0 + 1, [active](x0) = x0, [d](x0) = 0, [h](x0) = x0 + 1, [c#](x0) = x0 Strict: c# mark X -> c# X 1 + 1X >= 0 + 1X Weak: h active X -> h X 1 + 1X >= 1 + 1X h mark X -> h X 2 + 1X >= 1 + 1X d active X -> d X 0 + 0X >= 0 + 0X d mark X -> d X 0 + 0X >= 0 + 0X active h X -> mark c d X 1 + 1X >= 2 + 0X active f f X -> mark c f g f X 2 + 1X >= 5 + 1X active c X -> mark d X 1 + 1X >= 1 + 0X 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 c active X -> c X 1 + 1X >= 1 + 1X c mark X -> c X 2 + 1X >= 1 + 1X mark h X -> active h mark X 2 + 1X >= 2 + 1X mark d X -> active d X 1 + 0X >= 0 + 0X mark g X -> active g X 2 + 1X >= 1 + 1X mark f X -> active f mark X 2 + 1X >= 2 + 1X mark c X -> active c X 2 + 1X >= 1 + 1X Qed SCC (2): Strict: { f# mark X -> f# X, f# active X -> f# X} Weak: { mark c X -> active c X, mark f X -> active f mark X, mark g X -> active g X, mark d X -> active d X, mark h X -> active h mark X, c mark X -> c X, c active X -> c X, f mark X -> f X, f active X -> f X, g mark X -> g X, g active X -> g X, active c X -> mark d X, active f f X -> mark c f g f X, active h X -> mark c d X, d mark X -> d X, d active X -> d X, h mark X -> h X, h active X -> h X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [mark](x0) = x0, [c](x0) = 0, [f](x0) = 0, [g](x0) = 0, [active](x0) = x0 + 1, [d](x0) = x0 + 1, [h](x0) = 0, [f#](x0) = x0 Strict: f# active X -> f# X 1 + 1X >= 0 + 1X f# mark X -> f# X 0 + 1X >= 0 + 1X Weak: h active X -> h X 0 + 0X >= 0 + 0X h mark X -> h X 0 + 0X >= 0 + 0X d active X -> d X 2 + 1X >= 1 + 1X d mark X -> d X 1 + 1X >= 1 + 1X active h X -> mark c d X 1 + 0X >= 0 + 0X active f f X -> mark c f g f X 1 + 0X >= 0 + 0X active c X -> mark d X 1 + 0X >= 1 + 1X g active X -> g X 0 + 0X >= 0 + 0X g mark X -> g X 0 + 0X >= 0 + 0X f active X -> f X 0 + 0X >= 0 + 0X f mark X -> f X 0 + 0X >= 0 + 0X c active X -> c X 0 + 0X >= 0 + 0X c mark X -> c X 0 + 0X >= 0 + 0X mark h X -> active h mark X 0 + 0X >= 1 + 0X mark d X -> active d X 1 + 1X >= 2 + 1X mark g X -> active g X 0 + 0X >= 1 + 0X mark f X -> active f mark X 0 + 0X >= 1 + 0X mark c X -> active c X 0 + 0X >= 1 + 0X SCCS (1): Scc: {f# mark X -> f# X} SCC (1): Strict: {f# mark X -> f# X} Weak: { mark c X -> active c X, mark f X -> active f mark X, mark g X -> active g X, mark d X -> active d X, mark h X -> active h mark X, c mark X -> c X, c active X -> c X, f mark X -> f X, f active X -> f X, g mark X -> g X, g active X -> g X, active c X -> mark d X, active f f X -> mark c f g f X, active h X -> mark c d X, d mark X -> d X, d active X -> d X, h mark X -> h X, h active X -> h X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [mark](x0) = x0 + 1, [c](x0) = x0 + 1, [f](x0) = x0 + 1, [g](x0) = x0 + 1, [active](x0) = x0, [d](x0) = 0, [h](x0) = x0 + 1, [f#](x0) = x0 Strict: f# mark X -> f# X 1 + 1X >= 0 + 1X Weak: h active X -> h X 1 + 1X >= 1 + 1X h mark X -> h X 2 + 1X >= 1 + 1X d active X -> d X 0 + 0X >= 0 + 0X d mark X -> d X 0 + 0X >= 0 + 0X active h X -> mark c d X 1 + 1X >= 2 + 0X active f f X -> mark c f g f X 2 + 1X >= 5 + 1X active c X -> mark d X 1 + 1X >= 1 + 0X 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 c active X -> c X 1 + 1X >= 1 + 1X c mark X -> c X 2 + 1X >= 1 + 1X mark h X -> active h mark X 2 + 1X >= 2 + 1X mark d X -> active d X 1 + 0X >= 0 + 0X mark g X -> active g X 2 + 1X >= 1 + 1X mark f X -> active f mark X 2 + 1X >= 2 + 1X mark c X -> active c X 2 + 1X >= 1 + 1X Qed