YES Time: 0.119807 TRS: { g ok X -> ok g X, h mark X -> mark h X, h ok X -> ok h X, f mark X -> mark f X, f ok X -> ok f X, active h X -> h active X, active f X -> mark g h f X, active f X -> f active X, proper g X -> g proper X, proper h X -> h proper X, proper f X -> f proper X, top mark X -> top proper X, top ok X -> top active X} DP: DP: { g# ok X -> g# X, h# mark X -> h# X, h# ok X -> h# X, f# mark X -> f# X, f# ok X -> f# X, active# h X -> h# active X, active# h X -> active# X, active# f X -> g# h f X, active# f X -> h# f X, active# f X -> f# active X, active# f X -> active# X, proper# g X -> g# proper X, proper# g X -> proper# X, proper# h X -> h# proper X, proper# h X -> proper# X, proper# f X -> f# proper X, proper# f X -> proper# X, top# mark X -> proper# X, top# mark X -> top# proper X, top# ok X -> active# X, top# ok X -> top# active X} TRS: { g ok X -> ok g X, h mark X -> mark h X, h ok X -> ok h X, f mark X -> mark f X, f ok X -> ok f X, active h X -> h active X, active f X -> mark g h f X, active f X -> f active X, proper g X -> g proper X, proper h X -> h proper X, proper f X -> f proper X, top mark X -> top proper X, top ok X -> top active X} EDG: {(active# h X -> h# active X, h# ok X -> h# X) (active# h X -> h# active X, h# mark X -> h# X) (active# f X -> f# active X, f# ok X -> f# X) (active# f X -> f# active X, f# mark X -> f# X) (proper# h X -> h# proper X, h# ok X -> h# X) (proper# h X -> h# proper X, h# mark X -> h# X) (top# mark X -> top# proper X, top# ok X -> top# active X) (top# mark X -> top# proper X, top# ok X -> active# X) (top# mark X -> top# proper X, top# mark X -> top# proper X) (top# mark X -> top# proper X, top# mark X -> proper# X) (g# ok X -> g# X, g# ok X -> g# X) (h# ok X -> h# X, h# ok X -> h# X) (h# ok X -> h# X, h# mark X -> h# X) (f# ok X -> f# X, f# ok X -> f# X) (f# ok X -> f# X, f# mark X -> f# X) (active# f X -> active# X, active# f X -> active# X) (active# f X -> active# X, active# f X -> f# active X) (active# f X -> active# X, active# f X -> h# f X) (active# f X -> active# X, active# f X -> g# h f X) (active# f X -> active# X, active# h X -> active# X) (active# f X -> active# X, active# h X -> h# active X) (proper# h X -> proper# X, proper# f X -> proper# X) (proper# h X -> proper# X, proper# f X -> f# proper X) (proper# h X -> proper# X, proper# h X -> proper# X) (proper# h X -> proper# X, proper# h X -> h# proper X) (proper# h X -> proper# X, proper# g X -> proper# X) (proper# h X -> proper# X, proper# g X -> g# proper X) (top# mark X -> proper# X, proper# f X -> proper# X) (top# mark X -> proper# X, proper# f X -> f# proper X) (top# mark X -> proper# X, proper# h X -> proper# X) (top# mark X -> proper# X, proper# h X -> h# proper X) (top# mark X -> proper# X, proper# g X -> proper# X) (top# mark X -> proper# X, proper# g X -> g# proper X) (top# ok X -> active# X, active# h X -> h# active X) (top# ok X -> active# X, active# h X -> active# X) (top# ok X -> active# X, active# f X -> g# h f X) (top# ok X -> active# X, active# f X -> h# f X) (top# ok X -> active# X, active# f X -> f# active X) (top# ok X -> active# X, active# f X -> active# X) (proper# f X -> proper# X, proper# g X -> g# proper X) (proper# f X -> proper# X, proper# g X -> proper# X) (proper# f X -> proper# X, proper# h X -> h# proper X) (proper# f X -> proper# X, proper# h X -> proper# X) (proper# f X -> proper# X, proper# f X -> f# proper X) (proper# f X -> proper# X, proper# f X -> proper# X) (proper# g X -> proper# X, proper# g X -> g# proper X) (proper# g X -> proper# X, proper# g X -> proper# X) (proper# g X -> proper# X, proper# h X -> h# proper X) (proper# g X -> proper# X, proper# h X -> proper# X) (proper# g X -> proper# X, proper# f X -> f# proper X) (proper# g X -> proper# X, proper# f X -> proper# X) (active# h X -> active# X, active# h X -> h# active X) (active# h X -> active# X, active# h X -> active# X) (active# h X -> active# X, active# f X -> g# h f X) (active# h X -> active# X, active# f X -> h# f X) (active# h X -> active# X, active# f X -> f# active X) (active# h X -> active# X, active# f X -> active# X) (f# mark X -> f# X, f# mark X -> f# X) (f# mark X -> f# X, f# ok X -> f# X) (h# mark X -> h# X, h# mark X -> h# X) (h# mark X -> h# X, h# ok X -> h# X) (top# ok X -> top# active X, top# mark X -> proper# X) (top# ok X -> top# active X, top# mark X -> top# proper X) (top# ok X -> top# active X, top# ok X -> active# X) (top# ok X -> top# active X, top# ok X -> top# active X) (proper# f X -> f# proper X, f# mark X -> f# X) (proper# f X -> f# proper X, f# ok X -> f# X) (proper# g X -> g# proper X, g# ok X -> g# X) (active# f X -> h# f X, h# mark X -> h# X) (active# f X -> h# f X, h# ok X -> h# X) (active# f X -> g# h f X, g# ok X -> g# X)} STATUS: arrows: 0.839002 SCCS (6): Scc: {top# mark X -> top# proper X, top# ok X -> top# active X} Scc: {active# h X -> active# X, active# f X -> active# X} Scc: {proper# g X -> proper# X, proper# h X -> proper# X, proper# f X -> proper# X} Scc: {f# mark X -> f# X, f# ok X -> f# X} Scc: {h# mark X -> h# X, h# ok X -> h# X} Scc: {g# ok X -> g# X} SCC (2): Strict: {top# mark X -> top# proper X, top# ok X -> top# active X} Weak: { g ok X -> ok g X, h mark X -> mark h X, h ok X -> ok h X, f mark X -> mark f X, f ok X -> ok f X, active h X -> h active X, active f X -> mark g h f X, active f X -> f active X, proper g X -> g proper X, proper h X -> h proper X, proper f X -> f proper X, top mark X -> top proper X, top ok X -> top active X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [mark](x0) = 0, [g](x0) = x0, [h](x0) = x0, [f](x0) = x0, [active](x0) = 0, [proper](x0) = 0, [ok](x0) = 1, [top](x0) = 0, [top#](x0) = x0 + 1 Strict: top# ok X -> top# active X 2 + 0X >= 1 + 0X top# mark X -> top# proper X 1 + 0X >= 1 + 0X Weak: top ok X -> top active X 0 + 0X >= 0 + 0X top mark X -> top proper X 0 + 0X >= 0 + 0X proper f X -> f proper X 0 + 0X >= 0 + 0X proper h X -> h proper X 0 + 0X >= 0 + 0X proper g X -> g proper X 0 + 0X >= 0 + 0X active f X -> f active X 0 + 0X >= 0 + 0X active f X -> mark g h f X 0 + 0X >= 0 + 0X active h X -> h active X 0 + 0X >= 0 + 0X f ok X -> ok f X 1 + 0X >= 1 + 0X f mark X -> mark f X 0 + 0X >= 0 + 0X h ok X -> ok h X 1 + 0X >= 1 + 0X h mark X -> mark h X 0 + 0X >= 0 + 0X g ok X -> ok g X 1 + 0X >= 1 + 0X SCCS (1): Scc: {top# mark X -> top# proper X} SCC (1): Strict: {top# mark X -> top# proper X} Weak: { g ok X -> ok g X, h mark X -> mark h X, h ok X -> ok h X, f mark X -> mark f X, f ok X -> ok f X, active h X -> h active X, active f X -> mark g h f X, active f X -> f active X, proper g X -> g proper X, proper h X -> h proper X, proper f X -> f proper X, top mark X -> top proper X, top ok X -> top active X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [mark](x0) = 1, [g](x0) = 0, [h](x0) = x0, [f](x0) = x0, [active](x0) = 0, [proper](x0) = 0, [ok](x0) = 0, [top](x0) = 0, [top#](x0) = x0 + 1 Strict: top# mark X -> top# proper X 2 + 0X >= 1 + 0X Weak: top ok X -> top active X 0 + 0X >= 0 + 0X top mark X -> top proper X 0 + 0X >= 0 + 0X proper f X -> f proper X 0 + 0X >= 0 + 0X proper h X -> h proper X 0 + 0X >= 0 + 0X proper g X -> g proper X 0 + 0X >= 0 + 0X active f X -> f active X 0 + 0X >= 0 + 0X active f X -> mark g h f X 0 + 0X >= 1 + 0X active h X -> h active X 0 + 0X >= 0 + 0X f ok X -> ok f X 0 + 0X >= 0 + 0X f mark X -> mark f X 1 + 0X >= 1 + 0X h ok X -> ok h X 0 + 0X >= 0 + 0X h mark X -> mark h X 1 + 0X >= 1 + 0X g ok X -> ok g X 0 + 0X >= 0 + 0X Qed SCC (2): Strict: {active# h X -> active# X, active# f X -> active# X} Weak: { g ok X -> ok g X, h mark X -> mark h X, h ok X -> ok h X, f mark X -> mark f X, f ok X -> ok f X, active h X -> h active X, active f X -> mark g h f X, active f X -> f active X, proper g X -> g proper X, proper h X -> h proper X, proper f X -> f proper X, top mark X -> top proper X, top ok X -> top active X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [mark](x0) = 0, [g](x0) = 0, [h](x0) = x0, [f](x0) = x0 + 1, [active](x0) = 0, [proper](x0) = x0 + 1, [ok](x0) = 0, [top](x0) = 0, [active#](x0) = x0 Strict: active# f X -> active# X 1 + 1X >= 0 + 1X active# h X -> active# X 0 + 1X >= 0 + 1X Weak: top ok X -> top active X 0 + 0X >= 0 + 0X top mark X -> top proper X 0 + 0X >= 0 + 0X proper f X -> f proper X 2 + 1X >= 2 + 1X proper h X -> h proper X 1 + 1X >= 1 + 1X proper g X -> g proper X 1 + 0X >= 0 + 0X active f X -> f active X 0 + 0X >= 1 + 0X active f X -> mark g h f X 0 + 0X >= 0 + 0X active h X -> h active X 0 + 0X >= 0 + 0X f ok X -> ok f X 1 + 0X >= 0 + 0X f mark X -> mark f X 1 + 0X >= 0 + 0X h ok X -> ok h X 0 + 0X >= 0 + 0X h mark X -> mark h X 0 + 0X >= 0 + 0X g ok X -> ok g X 0 + 0X >= 0 + 0X SCCS (1): Scc: {active# h X -> active# X} SCC (1): Strict: {active# h X -> active# X} Weak: { g ok X -> ok g X, h mark X -> mark h X, h ok X -> ok h X, f mark X -> mark f X, f ok X -> ok f X, active h X -> h active X, active f X -> mark g h f X, active f X -> f active X, proper g X -> g proper X, proper h X -> h proper X, proper f X -> f proper X, top mark X -> top proper X, top ok X -> top active X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [mark](x0) = x0 + 1, [g](x0) = x0 + 1, [h](x0) = x0 + 1, [f](x0) = x0 + 1, [active](x0) = x0 + 1, [proper](x0) = x0 + 1, [ok](x0) = x0 + 1, [top](x0) = x0 + 1, [active#](x0) = x0 Strict: active# h X -> active# X 1 + 1X >= 0 + 1X Weak: top ok X -> top active X 2 + 1X >= 2 + 1X top mark X -> top proper X 2 + 1X >= 2 + 1X proper f X -> f proper X 2 + 1X >= 2 + 1X proper h X -> h proper X 2 + 1X >= 2 + 1X proper g X -> g proper X 2 + 1X >= 2 + 1X active f X -> f active X 2 + 1X >= 2 + 1X active f X -> mark g h f X 2 + 1X >= 4 + 1X active h X -> h active X 2 + 1X >= 2 + 1X f ok X -> ok f X 2 + 1X >= 2 + 1X f mark X -> mark f X 2 + 1X >= 2 + 1X h ok X -> ok h X 2 + 1X >= 2 + 1X h mark X -> mark h X 2 + 1X >= 2 + 1X g ok X -> ok g X 2 + 1X >= 2 + 1X Qed SCC (3): Strict: {proper# g X -> proper# X, proper# h X -> proper# X, proper# f X -> proper# X} Weak: { g ok X -> ok g X, h mark X -> mark h X, h ok X -> ok h X, f mark X -> mark f X, f ok X -> ok f X, active h X -> h active X, active f X -> mark g h f X, active f X -> f active X, proper g X -> g proper X, proper h X -> h proper X, proper f X -> f proper X, top mark X -> top proper X, top ok X -> top active X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [mark](x0) = 0, [g](x0) = x0, [h](x0) = x0, [f](x0) = x0 + 1, [active](x0) = 0, [proper](x0) = x0 + 1, [ok](x0) = 0, [top](x0) = 0, [proper#](x0) = x0 Strict: proper# f X -> proper# X 1 + 1X >= 0 + 1X proper# h X -> proper# X 0 + 1X >= 0 + 1X proper# g X -> proper# X 0 + 1X >= 0 + 1X Weak: top ok X -> top active X 0 + 0X >= 0 + 0X top mark X -> top proper X 0 + 0X >= 0 + 0X proper f X -> f proper X 2 + 1X >= 2 + 1X proper h X -> h proper X 1 + 1X >= 1 + 1X proper g X -> g proper X 1 + 1X >= 1 + 1X active f X -> f active X 0 + 0X >= 1 + 0X active f X -> mark g h f X 0 + 0X >= 0 + 0X active h X -> h active X 0 + 0X >= 0 + 0X f ok X -> ok f X 1 + 0X >= 0 + 0X f mark X -> mark f X 1 + 0X >= 0 + 0X h ok X -> ok h X 0 + 0X >= 0 + 0X h mark X -> mark h X 0 + 0X >= 0 + 0X g ok X -> ok g X 0 + 0X >= 0 + 0X SCCS (1): Scc: {proper# g X -> proper# X, proper# h X -> proper# X} SCC (2): Strict: {proper# g X -> proper# X, proper# h X -> proper# X} Weak: { g ok X -> ok g X, h mark X -> mark h X, h ok X -> ok h X, f mark X -> mark f X, f ok X -> ok f X, active h X -> h active X, active f X -> mark g h f X, active f X -> f active X, proper g X -> g proper X, proper h X -> h proper X, proper f X -> f proper X, top mark X -> top proper X, top ok X -> top active X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [mark](x0) = x0 + 1, [g](x0) = x0, [h](x0) = x0 + 1, [f](x0) = x0 + 1, [active](x0) = x0 + 1, [proper](x0) = x0 + 1, [ok](x0) = 0, [top](x0) = 0, [proper#](x0) = x0 Strict: proper# h X -> proper# X 1 + 1X >= 0 + 1X proper# g X -> proper# X 0 + 1X >= 0 + 1X Weak: top ok X -> top active X 0 + 0X >= 0 + 0X top mark X -> top proper X 0 + 0X >= 0 + 0X proper f X -> f proper X 2 + 1X >= 2 + 1X proper h X -> h proper X 2 + 1X >= 2 + 1X proper g X -> g proper X 1 + 1X >= 1 + 1X active f X -> f active X 2 + 1X >= 2 + 1X active f X -> mark g h f X 2 + 1X >= 3 + 1X active h X -> h active X 2 + 1X >= 2 + 1X f ok X -> ok f X 1 + 0X >= 0 + 0X f mark X -> mark f X 2 + 1X >= 2 + 1X h ok X -> ok h X 1 + 0X >= 0 + 0X h mark X -> mark h X 2 + 1X >= 2 + 1X g ok X -> ok g X 0 + 0X >= 0 + 0X SCCS (1): Scc: {proper# g X -> proper# X} SCC (1): Strict: {proper# g X -> proper# X} Weak: { g ok X -> ok g X, h mark X -> mark h X, h ok X -> ok h X, f mark X -> mark f X, f ok X -> ok f X, active h X -> h active X, active f X -> mark g h f X, active f X -> f active X, proper g X -> g proper X, proper h X -> h proper X, proper f X -> f proper X, top mark X -> top proper X, top ok X -> top active X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [mark](x0) = x0 + 1, [g](x0) = x0 + 1, [h](x0) = x0 + 1, [f](x0) = x0 + 1, [active](x0) = x0 + 1, [proper](x0) = x0 + 1, [ok](x0) = x0 + 1, [top](x0) = x0 + 1, [proper#](x0) = x0 Strict: proper# g X -> proper# X 1 + 1X >= 0 + 1X Weak: top ok X -> top active X 2 + 1X >= 2 + 1X top mark X -> top proper X 2 + 1X >= 2 + 1X proper f X -> f proper X 2 + 1X >= 2 + 1X proper h X -> h proper X 2 + 1X >= 2 + 1X proper g X -> g proper X 2 + 1X >= 2 + 1X active f X -> f active X 2 + 1X >= 2 + 1X active f X -> mark g h f X 2 + 1X >= 4 + 1X active h X -> h active X 2 + 1X >= 2 + 1X f ok X -> ok f X 2 + 1X >= 2 + 1X f mark X -> mark f X 2 + 1X >= 2 + 1X h ok X -> ok h X 2 + 1X >= 2 + 1X h mark X -> mark h X 2 + 1X >= 2 + 1X g ok X -> ok g X 2 + 1X >= 2 + 1X Qed SCC (2): Strict: {f# mark X -> f# X, f# ok X -> f# X} Weak: { g ok X -> ok g X, h mark X -> mark h X, h ok X -> ok h X, f mark X -> mark f X, f ok X -> ok f X, active h X -> h active X, active f X -> mark g h f X, active f X -> f active X, proper g X -> g proper X, proper h X -> h proper X, proper f X -> f proper X, top mark X -> top proper X, top ok X -> top active X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [mark](x0) = x0, [g](x0) = x0 + 1, [h](x0) = 0, [f](x0) = x0 + 1, [active](x0) = 0, [proper](x0) = x0 + 1, [ok](x0) = x0 + 1, [top](x0) = 0, [f#](x0) = x0 Strict: f# ok X -> f# X 1 + 1X >= 0 + 1X f# mark X -> f# X 0 + 1X >= 0 + 1X Weak: top ok X -> top active X 0 + 0X >= 0 + 0X top mark X -> top proper X 0 + 0X >= 0 + 0X proper f X -> f proper X 2 + 1X >= 2 + 1X proper h X -> h proper X 1 + 0X >= 0 + 0X proper g X -> g proper X 2 + 1X >= 2 + 1X active f X -> f active X 0 + 0X >= 1 + 0X active f X -> mark g h f X 0 + 0X >= 1 + 0X active h X -> h active X 0 + 0X >= 0 + 0X f ok X -> ok f X 2 + 1X >= 2 + 1X f mark X -> mark f X 1 + 1X >= 1 + 1X h ok X -> ok h X 0 + 0X >= 1 + 0X h mark X -> mark h X 0 + 0X >= 0 + 0X g ok X -> ok g X 2 + 1X >= 2 + 1X SCCS (1): Scc: {f# mark X -> f# X} SCC (1): Strict: {f# mark X -> f# X} Weak: { g ok X -> ok g X, h mark X -> mark h X, h ok X -> ok h X, f mark X -> mark f X, f ok X -> ok f X, active h X -> h active X, active f X -> mark g h f X, active f X -> f active X, proper g X -> g proper X, proper h X -> h proper X, proper f X -> f proper X, top mark X -> top proper X, top ok X -> top active X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [mark](x0) = x0 + 1, [g](x0) = x0 + 1, [h](x0) = x0 + 1, [f](x0) = x0 + 1, [active](x0) = x0 + 1, [proper](x0) = x0 + 1, [ok](x0) = x0 + 1, [top](x0) = x0 + 1, [f#](x0) = x0 Strict: f# mark X -> f# X 1 + 1X >= 0 + 1X Weak: top ok X -> top active X 2 + 1X >= 2 + 1X top mark X -> top proper X 2 + 1X >= 2 + 1X proper f X -> f proper X 2 + 1X >= 2 + 1X proper h X -> h proper X 2 + 1X >= 2 + 1X proper g X -> g proper X 2 + 1X >= 2 + 1X active f X -> f active X 2 + 1X >= 2 + 1X active f X -> mark g h f X 2 + 1X >= 4 + 1X active h X -> h active X 2 + 1X >= 2 + 1X f ok X -> ok f X 2 + 1X >= 2 + 1X f mark X -> mark f X 2 + 1X >= 2 + 1X h ok X -> ok h X 2 + 1X >= 2 + 1X h mark X -> mark h X 2 + 1X >= 2 + 1X g ok X -> ok g X 2 + 1X >= 2 + 1X Qed SCC (2): Strict: {h# mark X -> h# X, h# ok X -> h# X} Weak: { g ok X -> ok g X, h mark X -> mark h X, h ok X -> ok h X, f mark X -> mark f X, f ok X -> ok f X, active h X -> h active X, active f X -> mark g h f X, active f X -> f active X, proper g X -> g proper X, proper h X -> h proper X, proper f X -> f proper X, top mark X -> top proper X, top ok X -> top active X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [mark](x0) = x0, [g](x0) = x0 + 1, [h](x0) = 0, [f](x0) = x0 + 1, [active](x0) = 0, [proper](x0) = x0 + 1, [ok](x0) = x0 + 1, [top](x0) = 0, [h#](x0) = x0 Strict: h# ok X -> h# X 1 + 1X >= 0 + 1X h# mark X -> h# X 0 + 1X >= 0 + 1X Weak: top ok X -> top active X 0 + 0X >= 0 + 0X top mark X -> top proper X 0 + 0X >= 0 + 0X proper f X -> f proper X 2 + 1X >= 2 + 1X proper h X -> h proper X 1 + 0X >= 0 + 0X proper g X -> g proper X 2 + 1X >= 2 + 1X active f X -> f active X 0 + 0X >= 1 + 0X active f X -> mark g h f X 0 + 0X >= 1 + 0X active h X -> h active X 0 + 0X >= 0 + 0X f ok X -> ok f X 2 + 1X >= 2 + 1X f mark X -> mark f X 1 + 1X >= 1 + 1X h ok X -> ok h X 0 + 0X >= 1 + 0X h mark X -> mark h X 0 + 0X >= 0 + 0X g ok X -> ok g X 2 + 1X >= 2 + 1X SCCS (1): Scc: {h# mark X -> h# X} SCC (1): Strict: {h# mark X -> h# X} Weak: { g ok X -> ok g X, h mark X -> mark h X, h ok X -> ok h X, f mark X -> mark f X, f ok X -> ok f X, active h X -> h active X, active f X -> mark g h f X, active f X -> f active X, proper g X -> g proper X, proper h X -> h proper X, proper f X -> f proper X, top mark X -> top proper X, top ok X -> top active X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [mark](x0) = x0 + 1, [g](x0) = x0 + 1, [h](x0) = x0 + 1, [f](x0) = x0 + 1, [active](x0) = x0 + 1, [proper](x0) = x0 + 1, [ok](x0) = x0 + 1, [top](x0) = x0 + 1, [h#](x0) = x0 Strict: h# mark X -> h# X 1 + 1X >= 0 + 1X Weak: top ok X -> top active X 2 + 1X >= 2 + 1X top mark X -> top proper X 2 + 1X >= 2 + 1X proper f X -> f proper X 2 + 1X >= 2 + 1X proper h X -> h proper X 2 + 1X >= 2 + 1X proper g X -> g proper X 2 + 1X >= 2 + 1X active f X -> f active X 2 + 1X >= 2 + 1X active f X -> mark g h f X 2 + 1X >= 4 + 1X active h X -> h active X 2 + 1X >= 2 + 1X f ok X -> ok f X 2 + 1X >= 2 + 1X f mark X -> mark f X 2 + 1X >= 2 + 1X h ok X -> ok h X 2 + 1X >= 2 + 1X h mark X -> mark h X 2 + 1X >= 2 + 1X g ok X -> ok g X 2 + 1X >= 2 + 1X Qed SCC (1): Strict: {g# ok X -> g# X} Weak: { g ok X -> ok g X, h mark X -> mark h X, h ok X -> ok h X, f mark X -> mark f X, f ok X -> ok f X, active h X -> h active X, active f X -> mark g h f X, active f X -> f active X, proper g X -> g proper X, proper h X -> h proper X, proper f X -> f proper X, top mark X -> top proper X, top ok X -> top active X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [mark](x0) = x0 + 1, [g](x0) = x0 + 1, [h](x0) = x0 + 1, [f](x0) = x0 + 1, [active](x0) = x0 + 1, [proper](x0) = x0 + 1, [ok](x0) = x0 + 1, [top](x0) = x0 + 1, [g#](x0) = x0 Strict: g# ok X -> g# X 1 + 1X >= 0 + 1X Weak: top ok X -> top active X 2 + 1X >= 2 + 1X top mark X -> top proper X 2 + 1X >= 2 + 1X proper f X -> f proper X 2 + 1X >= 2 + 1X proper h X -> h proper X 2 + 1X >= 2 + 1X proper g X -> g proper X 2 + 1X >= 2 + 1X active f X -> f active X 2 + 1X >= 2 + 1X active f X -> mark g h f X 2 + 1X >= 4 + 1X active h X -> h active X 2 + 1X >= 2 + 1X f ok X -> ok f X 2 + 1X >= 2 + 1X f mark X -> mark f X 2 + 1X >= 2 + 1X h ok X -> ok h X 2 + 1X >= 2 + 1X h mark X -> mark h X 2 + 1X >= 2 + 1X g ok X -> ok g X 2 + 1X >= 2 + 1X Qed