YES Time: 0.269389 TRS: { c ok X -> ok c X, f mark X -> mark f X, f ok X -> ok f X, g mark X -> mark g X, g ok X -> ok g X, active f X -> f active X, active f f a() -> mark c f g f a(), active g X -> g active X, proper c X -> c proper X, proper f X -> f proper X, proper g X -> g proper X, proper a() -> ok a(), top mark X -> top proper X, top ok X -> top active X} DP: DP: { c# ok X -> c# X, f# mark X -> f# X, f# ok X -> f# X, g# mark X -> g# X, g# ok X -> g# X, active# f X -> f# active X, active# f X -> active# X, active# f f a() -> c# f g f a(), active# f f a() -> f# g f a(), active# f f a() -> g# f a(), active# g X -> g# active X, active# g X -> active# X, proper# c X -> c# proper X, proper# c X -> proper# X, proper# f X -> f# proper X, proper# f X -> proper# X, proper# g X -> g# proper X, proper# g 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: { c ok X -> ok c X, f mark X -> mark f X, f ok X -> ok f X, g mark X -> mark g X, g ok X -> ok g X, active f X -> f active X, active f f a() -> mark c f g f a(), active g X -> g active X, proper c X -> c proper X, proper f X -> f proper X, proper g X -> g proper X, proper a() -> ok a(), top mark X -> top proper X, top ok X -> top active X} EDG: {(f# mark X -> f# X, f# ok X -> f# X) (f# mark X -> f# X, f# mark X -> f# X) (g# mark X -> g# X, g# ok X -> g# X) (g# mark X -> g# X, g# mark X -> g# X) (active# f X -> active# X, active# g X -> active# X) (active# f X -> active# X, active# g X -> g# active X) (active# f X -> active# X, active# f f a() -> g# f a()) (active# f X -> active# X, active# f f a() -> f# g f a()) (active# f X -> active# X, active# f f a() -> c# f g f a()) (active# f X -> active# X, active# f X -> active# X) (active# f X -> active# X, active# f X -> f# active X) (proper# c X -> proper# X, proper# g X -> proper# X) (proper# c X -> proper# X, proper# g X -> g# proper X) (proper# c X -> proper# X, proper# f X -> proper# X) (proper# c X -> proper# X, proper# f X -> f# proper X) (proper# c X -> proper# X, proper# c X -> proper# X) (proper# c X -> proper# X, proper# c X -> c# proper X) (proper# g X -> proper# X, proper# g X -> proper# X) (proper# g X -> proper# X, proper# g X -> g# proper X) (proper# g X -> proper# X, proper# f X -> proper# X) (proper# g X -> proper# X, proper# f X -> f# proper X) (proper# g X -> proper# X, proper# c X -> proper# X) (proper# g X -> proper# X, proper# c X -> c# proper X) (top# ok X -> active# X, active# g X -> active# X) (top# ok X -> active# X, active# g X -> g# active X) (top# ok X -> active# X, active# f f a() -> g# f a()) (top# ok X -> active# X, active# f f a() -> f# g f a()) (top# ok X -> active# X, active# f f a() -> c# f g f a()) (top# ok X -> active# X, active# f X -> active# X) (top# ok X -> active# X, active# f X -> f# active X) (active# f f a() -> f# g f a(), f# ok X -> f# X) (active# f f a() -> f# g f a(), f# mark X -> f# X) (active# f X -> f# active X, f# ok X -> f# X) (active# f X -> f# active X, f# mark X -> f# X) (proper# c X -> c# proper X, c# ok X -> c# X) (proper# g X -> g# proper X, g# ok X -> g# X) (proper# g X -> g# proper X, g# mark X -> g# X) (top# ok X -> top# active X, top# ok X -> top# active X) (top# ok X -> top# active X, top# ok X -> active# X) (top# ok X -> top# active X, top# mark X -> top# proper X) (top# ok X -> top# active X, top# mark X -> proper# X) (top# mark X -> top# proper X, top# mark X -> proper# X) (top# mark X -> top# proper X, top# mark X -> top# proper X) (top# mark X -> top# proper X, top# ok X -> active# X) (top# mark X -> top# proper 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) (active# g X -> g# active X, g# mark X -> g# X) (active# g X -> g# active X, g# ok X -> g# X) (active# f f a() -> g# f a(), g# mark X -> g# X) (active# f f a() -> g# f a(), g# ok X -> g# X) (active# f f a() -> c# f g f a(), c# ok X -> c# X) (top# mark X -> proper# X, proper# c X -> c# proper X) (top# mark X -> proper# X, proper# c X -> proper# X) (top# mark X -> proper# X, proper# f X -> f# proper X) (top# mark X -> proper# X, proper# f X -> proper# X) (top# mark X -> proper# X, proper# g X -> g# proper X) (top# mark X -> proper# X, proper# g X -> proper# X) (proper# f X -> proper# X, proper# c X -> c# proper X) (proper# f X -> proper# X, proper# c 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# f X -> proper# X, proper# g X -> g# proper X) (proper# f X -> proper# X, proper# g X -> proper# X) (active# g X -> active# X, active# f X -> f# active X) (active# g X -> active# X, active# f X -> active# X) (active# g X -> active# X, active# f f a() -> c# f g f a()) (active# g X -> active# X, active# f f a() -> f# g f a()) (active# g X -> active# X, active# f f a() -> g# f a()) (active# g X -> active# X, active# g X -> g# active X) (active# g X -> active# X, active# g X -> active# X) (g# ok X -> g# X, g# mark X -> g# X) (g# ok X -> g# X, g# ok X -> g# X) (f# ok X -> f# X, f# mark X -> f# X) (f# ok X -> f# X, f# ok X -> f# X) (c# ok X -> c# X, c# ok X -> c# X)} STATUS: arrows: 0.842975 SCCS (6): Scc: {top# mark X -> top# proper X, top# ok X -> top# active X} Scc: {proper# c X -> proper# X, proper# f X -> proper# X, proper# g X -> proper# X} Scc: {active# f X -> active# X, active# g X -> active# X} Scc: {g# mark X -> g# X, g# ok X -> g# X} Scc: {f# mark X -> f# X, f# ok X -> f# X} Scc: {c# ok X -> c# X} SCC (2): Strict: {top# mark X -> top# proper X, top# ok X -> top# active X} Weak: { c ok X -> ok c X, f mark X -> mark f X, f ok X -> ok f X, g mark X -> mark g X, g ok X -> ok g X, active f X -> f active X, active f f a() -> mark c f g f a(), active g X -> g active X, proper c X -> c proper X, proper f X -> f proper X, proper g X -> g proper X, proper a() -> ok a(), 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, [c](x0) = 0, [f](x0) = x0, [g](x0) = x0, [active](x0) = x0, [proper](x0) = x0, [ok](x0) = x0, [top](x0) = 0, [a] = 1, [top#](x0) = x0 Strict: top# ok X -> top# active X 0 + 1X >= 0 + 1X top# mark X -> top# proper X 1 + 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 a() -> ok a() 1 >= 1 proper g X -> g proper X 0 + 1X >= 0 + 1X proper f X -> f proper X 0 + 1X >= 0 + 1X proper c X -> c proper X 0 + 0X >= 0 + 0X active g X -> g active X 0 + 1X >= 0 + 1X active f f a() -> mark c f g f a() 1 >= 1 active f X -> f active X 0 + 1X >= 0 + 1X g ok X -> ok g X 0 + 1X >= 0 + 1X g mark X -> mark g X 1 + 1X >= 1 + 1X f ok X -> ok f X 0 + 1X >= 0 + 1X f mark X -> mark f X 1 + 1X >= 1 + 1X c ok X -> ok c X 0 + 0X >= 0 + 0X SCCS (1): Scc: {top# ok X -> top# active X} SCC (1): Strict: {top# ok X -> top# active X} Weak: { c ok X -> ok c X, f mark X -> mark f X, f ok X -> ok f X, g mark X -> mark g X, g ok X -> ok g X, active f X -> f active X, active f f a() -> mark c f g f a(), active g X -> g active X, proper c X -> c proper X, proper f X -> f proper X, proper g X -> g proper X, proper a() -> ok a(), 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, [c](x0) = x0 + 1, [f](x0) = x0, [g](x0) = x0, [active](x0) = 0, [proper](x0) = x0 + 1, [ok](x0) = 1, [top](x0) = 0, [a] = 0, [top#](x0) = x0 + 1 Strict: top# ok X -> top# active 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 a() -> ok a() 1 >= 1 proper g X -> g proper X 1 + 1X >= 1 + 1X proper f X -> f proper X 1 + 1X >= 1 + 1X proper c X -> c proper X 2 + 1X >= 2 + 1X active g X -> g active X 0 + 0X >= 0 + 0X active f f a() -> mark c f g f a() 0 >= 0 active f X -> f active X 0 + 0X >= 0 + 0X g ok X -> ok g X 1 + 0X >= 1 + 0X g mark X -> mark g 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 c ok X -> ok c X 2 + 0X >= 1 + 0X Qed SCC (3): Strict: {proper# c X -> proper# X, proper# f X -> proper# X, proper# g X -> proper# X} Weak: { c ok X -> ok c X, f mark X -> mark f X, f ok X -> ok f X, g mark X -> mark g X, g ok X -> ok g X, active f X -> f active X, active f f a() -> mark c f g f a(), active g X -> g active X, proper c X -> c proper X, proper f X -> f proper X, proper g X -> g proper X, proper a() -> ok a(), 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, [c](x0) = x0, [f](x0) = x0, [g](x0) = x0 + 1, [active](x0) = 0, [proper](x0) = 0, [ok](x0) = 0, [top](x0) = x0, [a] = 1, [proper#](x0) = x0 Strict: proper# g X -> proper# X 1 + 1X >= 0 + 1X proper# f X -> proper# X 0 + 1X >= 0 + 1X proper# c X -> proper# X 0 + 1X >= 0 + 1X Weak: top ok X -> top active X 0 + 0X >= 0 + 0X top mark X -> top proper X 1 + 1X >= 0 + 0X proper a() -> ok a() 0 >= 0 proper g X -> g proper X 0 + 0X >= 1 + 0X proper f X -> f proper X 0 + 0X >= 0 + 0X proper c X -> c proper X 0 + 0X >= 0 + 0X active g X -> g active X 0 + 0X >= 1 + 0X active f f a() -> mark c f g f a() 0 >= 3 active f X -> f active X 0 + 0X >= 0 + 0X g ok X -> ok g X 1 + 0X >= 0 + 0X g mark X -> mark g X 2 + 1X >= 2 + 1X f ok X -> ok f X 0 + 0X >= 0 + 0X f mark X -> mark f X 1 + 1X >= 1 + 1X c ok X -> ok c X 0 + 0X >= 0 + 0X SCCS (1): Scc: {proper# c X -> proper# X, proper# f X -> proper# X} SCC (2): Strict: {proper# c X -> proper# X, proper# f X -> proper# X} Weak: { c ok X -> ok c X, f mark X -> mark f X, f ok X -> ok f X, g mark X -> mark g X, g ok X -> ok g X, active f X -> f active X, active f f a() -> mark c f g f a(), active g X -> g active X, proper c X -> c proper X, proper f X -> f proper X, proper g X -> g proper X, proper a() -> ok a(), 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, [c](x0) = x0 + 1, [f](x0) = x0 + 1, [g](x0) = 1, [active](x0) = x0 + 1, [proper](x0) = x0 + 1, [ok](x0) = x0 + 1, [top](x0) = 0, [a] = 1, [proper#](x0) = x0 + 1 Strict: proper# f X -> proper# X 2 + 1X >= 1 + 1X proper# c X -> proper# X 2 + 1X >= 1 + 1X Weak: top ok X -> top active X 0 + 0X >= 0 + 0X top mark X -> top proper X 0 + 0X >= 0 + 0X proper a() -> ok a() 2 >= 2 proper g X -> g proper X 2 + 0X >= 1 + 0X proper f X -> f proper X 2 + 1X >= 2 + 1X proper c X -> c proper X 2 + 1X >= 2 + 1X active g X -> g active X 2 + 0X >= 1 + 0X active f f a() -> mark c f g f a() 4 >= 4 active f X -> f active X 2 + 1X >= 2 + 1X g ok X -> ok g X 1 + 0X >= 2 + 0X g mark X -> mark g X 1 + 0X >= 2 + 0X f ok X -> ok f X 2 + 1X >= 2 + 1X f mark X -> mark f X 2 + 1X >= 2 + 1X c ok X -> ok c X 2 + 1X >= 2 + 1X Qed SCC (2): Strict: {active# f X -> active# X, active# g X -> active# X} Weak: { c ok X -> ok c X, f mark X -> mark f X, f ok X -> ok f X, g mark X -> mark g X, g ok X -> ok g X, active f X -> f active X, active f f a() -> mark c f g f a(), active g X -> g active X, proper c X -> c proper X, proper f X -> f proper X, proper g X -> g proper X, proper a() -> ok a(), 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, [c](x0) = x0 + 1, [f](x0) = x0, [g](x0) = x0 + 1, [active](x0) = 0, [proper](x0) = x0 + 1, [ok](x0) = x0 + 1, [top](x0) = 0, [a] = 0, [active#](x0) = x0 Strict: active# g X -> active# X 1 + 1X >= 0 + 1X active# f 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 a() -> ok a() 1 >= 1 proper g X -> g proper X 2 + 1X >= 2 + 1X proper f X -> f proper X 1 + 1X >= 1 + 1X proper c X -> c proper X 2 + 1X >= 2 + 1X active g X -> g active X 0 + 0X >= 1 + 0X active f f a() -> mark c f g f a() 0 >= 0 active f X -> f active X 0 + 0X >= 0 + 0X g ok X -> ok g X 2 + 1X >= 2 + 1X g mark X -> mark g X 1 + 0X >= 0 + 0X f ok X -> ok f X 1 + 1X >= 1 + 1X f mark X -> mark f X 0 + 0X >= 0 + 0X c ok X -> ok c X 2 + 1X >= 2 + 1X SCCS (1): Scc: {active# f X -> active# X} SCC (1): Strict: {active# f X -> active# X} Weak: { c ok X -> ok c X, f mark X -> mark f X, f ok X -> ok f X, g mark X -> mark g X, g ok X -> ok g X, active f X -> f active X, active f f a() -> mark c f g f a(), active g X -> g active X, proper c X -> c proper X, proper f X -> f proper X, proper g X -> g proper X, proper a() -> ok a(), 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, [c](x0) = x0 + 1, [f](x0) = x0 + 1, [g](x0) = x0 + 1, [active](x0) = x0 + 1, [proper](x0) = x0 + 1, [ok](x0) = x0 + 1, [top](x0) = 0, [a] = 0, [active#](x0) = x0 Strict: active# f X -> active# X 1 + 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 a() -> ok a() 1 >= 1 proper g X -> g proper X 2 + 1X >= 2 + 1X proper f X -> f proper X 2 + 1X >= 2 + 1X proper c X -> c proper X 2 + 1X >= 2 + 1X active g X -> g active X 2 + 1X >= 2 + 1X active f f a() -> mark c f g f a() 3 >= 5 active f X -> f active X 2 + 1X >= 2 + 1X g ok X -> ok g X 2 + 1X >= 2 + 1X g mark X -> mark g 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 c ok X -> ok c X 2 + 1X >= 2 + 1X Qed SCC (2): Strict: {g# mark X -> g# X, g# ok X -> g# X} Weak: { c ok X -> ok c X, f mark X -> mark f X, f ok X -> ok f X, g mark X -> mark g X, g ok X -> ok g X, active f X -> f active X, active f f a() -> mark c f g f a(), active g X -> g active X, proper c X -> c proper X, proper f X -> f proper X, proper g X -> g proper X, proper a() -> ok a(), 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, [c](x0) = x0 + 1, [f](x0) = 0, [g](x0) = 0, [active](x0) = 0, [proper](x0) = x0 + 1, [ok](x0) = x0 + 1, [top](x0) = 0, [a] = 1, [g#](x0) = x0 Strict: g# ok X -> g# X 1 + 1X >= 0 + 1X g# mark X -> g# 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 a() -> ok a() 2 >= 2 proper g X -> g proper X 1 + 0X >= 0 + 0X proper f X -> f proper X 1 + 0X >= 0 + 0X proper c X -> c proper X 2 + 1X >= 2 + 1X active g X -> g active X 0 + 0X >= 0 + 0X active f f a() -> mark c f g f a() 0 >= 1 active f X -> f active X 0 + 0X >= 0 + 0X g ok X -> ok g X 0 + 0X >= 1 + 0X g mark X -> mark g X 0 + 0X >= 0 + 0X f ok X -> ok f X 0 + 0X >= 1 + 0X f mark X -> mark f X 0 + 0X >= 0 + 0X c ok X -> ok c X 2 + 1X >= 2 + 1X SCCS (1): Scc: {g# mark X -> g# X} SCC (1): Strict: {g# mark X -> g# X} Weak: { c ok X -> ok c X, f mark X -> mark f X, f ok X -> ok f X, g mark X -> mark g X, g ok X -> ok g X, active f X -> f active X, active f f a() -> mark c f g f a(), active g X -> g active X, proper c X -> c proper X, proper f X -> f proper X, proper g X -> g proper X, proper a() -> ok a(), 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, [c](x0) = x0 + 1, [f](x0) = x0 + 1, [g](x0) = x0 + 1, [active](x0) = x0 + 1, [proper](x0) = x0 + 1, [ok](x0) = x0 + 1, [top](x0) = 0, [a] = 0, [g#](x0) = x0 Strict: g# mark X -> g# X 1 + 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 a() -> ok a() 1 >= 1 proper g X -> g proper X 2 + 1X >= 2 + 1X proper f X -> f proper X 2 + 1X >= 2 + 1X proper c X -> c proper X 2 + 1X >= 2 + 1X active g X -> g active X 2 + 1X >= 2 + 1X active f f a() -> mark c f g f a() 3 >= 5 active f X -> f active X 2 + 1X >= 2 + 1X g ok X -> ok g X 2 + 1X >= 2 + 1X g mark X -> mark g 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 c ok X -> ok c X 2 + 1X >= 2 + 1X Qed SCC (2): Strict: {f# mark X -> f# X, f# ok X -> f# X} Weak: { c ok X -> ok c X, f mark X -> mark f X, f ok X -> ok f X, g mark X -> mark g X, g ok X -> ok g X, active f X -> f active X, active f f a() -> mark c f g f a(), active g X -> g active X, proper c X -> c proper X, proper f X -> f proper X, proper g X -> g proper X, proper a() -> ok a(), 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, [c](x0) = x0 + 1, [f](x0) = 0, [g](x0) = 0, [active](x0) = 0, [proper](x0) = x0 + 1, [ok](x0) = x0 + 1, [top](x0) = 0, [a] = 1, [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 a() -> ok a() 2 >= 2 proper g X -> g proper X 1 + 0X >= 0 + 0X proper f X -> f proper X 1 + 0X >= 0 + 0X proper c X -> c proper X 2 + 1X >= 2 + 1X active g X -> g active X 0 + 0X >= 0 + 0X active f f a() -> mark c f g f a() 0 >= 1 active f X -> f active X 0 + 0X >= 0 + 0X g ok X -> ok g X 0 + 0X >= 1 + 0X g mark X -> mark g X 0 + 0X >= 0 + 0X f ok X -> ok f X 0 + 0X >= 1 + 0X f mark X -> mark f X 0 + 0X >= 0 + 0X c ok X -> ok c X 2 + 1X >= 2 + 1X SCCS (1): Scc: {f# mark X -> f# X} SCC (1): Strict: {f# mark X -> f# X} Weak: { c ok X -> ok c X, f mark X -> mark f X, f ok X -> ok f X, g mark X -> mark g X, g ok X -> ok g X, active f X -> f active X, active f f a() -> mark c f g f a(), active g X -> g active X, proper c X -> c proper X, proper f X -> f proper X, proper g X -> g proper X, proper a() -> ok a(), 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, [c](x0) = x0 + 1, [f](x0) = x0 + 1, [g](x0) = x0 + 1, [active](x0) = x0 + 1, [proper](x0) = x0 + 1, [ok](x0) = x0 + 1, [top](x0) = 0, [a] = 0, [f#](x0) = x0 Strict: f# mark X -> f# X 1 + 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 a() -> ok a() 1 >= 1 proper g X -> g proper X 2 + 1X >= 2 + 1X proper f X -> f proper X 2 + 1X >= 2 + 1X proper c X -> c proper X 2 + 1X >= 2 + 1X active g X -> g active X 2 + 1X >= 2 + 1X active f f a() -> mark c f g f a() 3 >= 5 active f X -> f active X 2 + 1X >= 2 + 1X g ok X -> ok g X 2 + 1X >= 2 + 1X g mark X -> mark g 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 c ok X -> ok c X 2 + 1X >= 2 + 1X Qed SCC (1): Strict: {c# ok X -> c# X} Weak: { c ok X -> ok c X, f mark X -> mark f X, f ok X -> ok f X, g mark X -> mark g X, g ok X -> ok g X, active f X -> f active X, active f f a() -> mark c f g f a(), active g X -> g active X, proper c X -> c proper X, proper f X -> f proper X, proper g X -> g proper X, proper a() -> ok a(), 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, [c](x0) = x0 + 1, [f](x0) = x0 + 1, [g](x0) = x0 + 1, [active](x0) = x0 + 1, [proper](x0) = x0 + 1, [ok](x0) = x0 + 1, [top](x0) = 0, [a] = 0, [c#](x0) = x0 Strict: c# ok X -> c# X 1 + 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 a() -> ok a() 1 >= 1 proper g X -> g proper X 2 + 1X >= 2 + 1X proper f X -> f proper X 2 + 1X >= 2 + 1X proper c X -> c proper X 2 + 1X >= 2 + 1X active g X -> g active X 2 + 1X >= 2 + 1X active f f a() -> mark c f g f a() 3 >= 5 active f X -> f active X 2 + 1X >= 2 + 1X g ok X -> ok g X 2 + 1X >= 2 + 1X g mark X -> mark g 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 c ok X -> ok c X 2 + 1X >= 2 + 1X Qed