MAYBE Time: 0.239084 TRS: { if(X1, mark X2, X3) -> mark if(X1, X2, X3), if(mark X1, X2, X3) -> mark if(X1, X2, X3), if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3), f mark X -> mark f X, f ok X -> ok f X, active if(X1, X2, X3) -> if(X1, active X2, X3), active if(X1, X2, X3) -> if(active X1, X2, X3), active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active f X -> mark if(X, c(), f true()), active f X -> f active X, proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3), proper c() -> ok c(), proper f X -> f proper X, proper true() -> ok true(), proper false() -> ok false(), top mark X -> top proper X, top ok X -> top active X} DP: DP: { if#(X1, mark X2, X3) -> if#(X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3), if#(ok X1, ok X2, ok X3) -> if#(X1, X2, X3), f# mark X -> f# X, f# ok X -> f# X, active# if(X1, X2, X3) -> if#(X1, active X2, X3), active# if(X1, X2, X3) -> if#(active X1, X2, X3), active# if(X1, X2, X3) -> active# X1, active# if(X1, X2, X3) -> active# X2, active# f X -> if#(X, c(), f true()), active# f X -> f# true(), active# f X -> f# active X, active# f X -> active# X, proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3), proper# if(X1, X2, X3) -> proper# X1, proper# if(X1, X2, X3) -> proper# X2, proper# if(X1, X2, X3) -> proper# X3, 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: { if(X1, mark X2, X3) -> mark if(X1, X2, X3), if(mark X1, X2, X3) -> mark if(X1, X2, X3), if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3), f mark X -> mark f X, f ok X -> ok f X, active if(X1, X2, X3) -> if(X1, active X2, X3), active if(X1, X2, X3) -> if(active X1, X2, X3), active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active f X -> mark if(X, c(), f true()), active f X -> f active X, proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3), proper c() -> ok c(), proper f X -> f proper X, proper true() -> ok true(), proper false() -> ok false(), top mark X -> top proper X, top ok X -> top active X} UR: { if(X1, mark X2, X3) -> mark if(X1, X2, X3), if(mark X1, X2, X3) -> mark if(X1, X2, X3), if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3), f mark X -> mark f X, f ok X -> ok f X, active if(X1, X2, X3) -> if(X1, active X2, X3), active if(X1, X2, X3) -> if(active X1, X2, X3), active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active f X -> mark if(X, c(), f true()), active f X -> f active X, proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3), proper c() -> ok c(), proper f X -> f proper X, proper true() -> ok true(), proper false() -> ok false()} EDG: {(active# f X -> if#(X, c(), f true()), if#(ok X1, ok X2, ok X3) -> if#(X1, X2, X3)) (active# f X -> if#(X, c(), f true()), if#(mark X1, X2, X3) -> if#(X1, X2, X3)) (active# f X -> if#(X, c(), f true()), if#(X1, mark X2, X3) -> if#(X1, X2, X3)) (proper# f X -> f# proper X, f# ok X -> f# X) (proper# f X -> f# proper X, f# mark X -> f# 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) (proper# if(X1, X2, X3) -> proper# X3, proper# f X -> proper# X) (proper# if(X1, X2, X3) -> proper# X3, proper# f X -> f# proper X) (proper# if(X1, X2, X3) -> proper# X3, proper# if(X1, X2, X3) -> proper# X3) (proper# if(X1, X2, X3) -> proper# X3, proper# if(X1, X2, X3) -> proper# X2) (proper# if(X1, X2, X3) -> proper# X3, proper# if(X1, X2, X3) -> proper# X1) (proper# if(X1, X2, X3) -> proper# X3, proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3)) (if#(X1, mark X2, X3) -> if#(X1, X2, X3), if#(ok X1, ok X2, ok X3) -> if#(X1, X2, X3)) (if#(X1, mark X2, X3) -> if#(X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3)) (if#(X1, mark X2, X3) -> if#(X1, X2, X3), if#(X1, mark X2, X3) -> if#(X1, X2, X3)) (if#(ok X1, ok X2, ok X3) -> if#(X1, X2, X3), if#(ok X1, ok X2, ok X3) -> if#(X1, X2, X3)) (if#(ok X1, ok X2, ok X3) -> if#(X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3)) (if#(ok X1, ok X2, ok X3) -> if#(X1, X2, X3), if#(X1, mark X2, X3) -> if#(X1, X2, X3)) (active# if(X1, X2, X3) -> active# X1, active# f X -> active# X) (active# if(X1, X2, X3) -> active# X1, active# f X -> f# active X) (active# if(X1, X2, X3) -> active# X1, active# f X -> f# true()) (active# if(X1, X2, X3) -> active# X1, active# f X -> if#(X, c(), f true())) (active# if(X1, X2, X3) -> active# X1, active# if(X1, X2, X3) -> active# X2) (active# if(X1, X2, X3) -> active# X1, active# if(X1, X2, X3) -> active# X1) (active# if(X1, X2, X3) -> active# X1, active# if(X1, X2, X3) -> if#(active X1, X2, X3)) (active# if(X1, X2, X3) -> active# X1, active# if(X1, X2, X3) -> if#(X1, active X2, X3)) (f# mark X -> f# X, f# ok X -> f# X) (f# mark 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 -> f# true()) (active# f X -> active# X, active# f X -> if#(X, c(), f true())) (active# f X -> active# X, active# if(X1, X2, X3) -> active# X2) (active# f X -> active# X, active# if(X1, X2, X3) -> active# X1) (active# f X -> active# X, active# if(X1, X2, X3) -> if#(active X1, X2, X3)) (active# f X -> active# X, active# if(X1, X2, X3) -> if#(X1, active X2, X3)) (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# if(X1, X2, X3) -> proper# X3) (top# mark X -> proper# X, proper# if(X1, X2, X3) -> proper# X2) (top# mark X -> proper# X, proper# if(X1, X2, X3) -> proper# X1) (top# mark X -> proper# X, proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3)) (active# if(X1, X2, X3) -> active# X2, active# f X -> active# X) (active# if(X1, X2, X3) -> active# X2, active# f X -> f# active X) (active# if(X1, X2, X3) -> active# X2, active# f X -> f# true()) (active# if(X1, X2, X3) -> active# X2, active# f X -> if#(X, c(), f true())) (active# if(X1, X2, X3) -> active# X2, active# if(X1, X2, X3) -> active# X2) (active# if(X1, X2, X3) -> active# X2, active# if(X1, X2, X3) -> active# X1) (active# if(X1, X2, X3) -> active# X2, active# if(X1, X2, X3) -> if#(active X1, X2, X3)) (active# if(X1, X2, X3) -> active# X2, active# if(X1, X2, X3) -> if#(X1, active X2, X3)) (proper# if(X1, X2, X3) -> proper# X2, proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3)) (proper# if(X1, X2, X3) -> proper# X2, proper# if(X1, X2, X3) -> proper# X1) (proper# if(X1, X2, X3) -> proper# X2, proper# if(X1, X2, X3) -> proper# X2) (proper# if(X1, X2, X3) -> proper# X2, proper# if(X1, X2, X3) -> proper# X3) (proper# if(X1, X2, X3) -> proper# X2, proper# f X -> f# proper X) (proper# if(X1, X2, X3) -> proper# X2, proper# f X -> proper# X) (top# ok X -> active# X, active# if(X1, X2, X3) -> if#(X1, active X2, X3)) (top# ok X -> active# X, active# if(X1, X2, X3) -> if#(active X1, X2, X3)) (top# ok X -> active# X, active# if(X1, X2, X3) -> active# X1) (top# ok X -> active# X, active# if(X1, X2, X3) -> active# X2) (top# ok X -> active# X, active# f X -> if#(X, c(), f true())) (top# ok X -> active# X, active# f X -> f# true()) (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# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3)) (proper# f X -> proper# X, proper# if(X1, X2, X3) -> proper# X1) (proper# f X -> proper# X, proper# if(X1, X2, X3) -> proper# X2) (proper# f X -> proper# X, proper# if(X1, X2, X3) -> proper# X3) (proper# f X -> proper# X, proper# f X -> f# proper X) (proper# f X -> proper# X, proper# f X -> proper# X) (f# ok X -> f# X, f# mark X -> f# X) (f# ok X -> f# X, f# ok X -> f# X) (proper# if(X1, X2, X3) -> proper# X1, proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3)) (proper# if(X1, X2, X3) -> proper# X1, proper# if(X1, X2, X3) -> proper# X1) (proper# if(X1, X2, X3) -> proper# X1, proper# if(X1, X2, X3) -> proper# X2) (proper# if(X1, X2, X3) -> proper# X1, proper# if(X1, X2, X3) -> proper# X3) (proper# if(X1, X2, X3) -> proper# X1, proper# f X -> f# proper X) (proper# if(X1, X2, X3) -> proper# X1, proper# f X -> proper# X) (active# if(X1, X2, X3) -> if#(active X1, X2, X3), if#(X1, mark X2, X3) -> if#(X1, X2, X3)) (active# if(X1, X2, X3) -> if#(active X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3)) (active# if(X1, X2, X3) -> if#(active X1, X2, X3), if#(ok X1, ok X2, ok X3) -> if#(X1, X2, X3)) (if#(mark X1, X2, X3) -> if#(X1, X2, X3), if#(X1, mark X2, X3) -> if#(X1, X2, X3)) (if#(mark X1, X2, X3) -> if#(X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3)) (if#(mark X1, X2, X3) -> if#(X1, X2, X3), if#(ok X1, ok X2, ok X3) -> if#(X1, X2, X3)) (active# if(X1, X2, X3) -> if#(X1, active X2, X3), if#(X1, mark X2, X3) -> if#(X1, X2, X3)) (active# if(X1, X2, X3) -> if#(X1, active X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3)) (active# if(X1, X2, X3) -> if#(X1, active X2, X3), if#(ok X1, ok X2, ok X3) -> if#(X1, X2, X3)) (proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3), if#(X1, mark X2, X3) -> if#(X1, X2, X3)) (proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3)) (proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3), if#(ok X1, ok X2, ok X3) -> if#(X1, X2, X3)) (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) (active# f X -> f# active X, f# mark X -> f# X) (active# f X -> f# active X, f# ok X -> f# X) (active# f X -> f# true(), f# mark X -> f# X) (active# f X -> f# true(), f# ok X -> f# X)} STATUS: arrows: 0.809074 SCCS (5): Scc: {top# mark X -> top# proper X, top# ok X -> top# active X} Scc: {active# if(X1, X2, X3) -> active# X1, active# if(X1, X2, X3) -> active# X2, active# f X -> active# X} Scc: {proper# if(X1, X2, X3) -> proper# X1, proper# if(X1, X2, X3) -> proper# X2, proper# if(X1, X2, X3) -> proper# X3, proper# f X -> proper# X} Scc: { if#(X1, mark X2, X3) -> if#(X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3), if#(ok X1, ok X2, ok X3) -> if#(X1, X2, X3)} Scc: {f# mark X -> f# X, f# ok X -> f# X} SCC (2): Strict: {top# mark X -> top# proper X, top# ok X -> top# active X} Weak: { if(X1, mark X2, X3) -> mark if(X1, X2, X3), if(mark X1, X2, X3) -> mark if(X1, X2, X3), if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3), f mark X -> mark f X, f ok X -> ok f X, active if(X1, X2, X3) -> if(X1, active X2, X3), active if(X1, X2, X3) -> if(active X1, X2, X3), active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active f X -> mark if(X, c(), f true()), active f X -> f active X, proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3), proper c() -> ok c(), proper f X -> f proper X, proper true() -> ok true(), proper false() -> ok false(), top mark X -> top proper X, top ok X -> top active X} Fail SCC (3): Strict: {active# if(X1, X2, X3) -> active# X1, active# if(X1, X2, X3) -> active# X2, active# f X -> active# X} Weak: { if(X1, mark X2, X3) -> mark if(X1, X2, X3), if(mark X1, X2, X3) -> mark if(X1, X2, X3), if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3), f mark X -> mark f X, f ok X -> ok f X, active if(X1, X2, X3) -> if(X1, active X2, X3), active if(X1, X2, X3) -> if(active X1, X2, X3), active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active f X -> mark if(X, c(), f true()), active f X -> f active X, proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3), proper c() -> ok c(), proper f X -> f proper X, proper true() -> ok true(), proper false() -> ok false(), 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: [if](x0, x1, x2) = x0 + x1 + x2, [mark](x0) = 0, [f](x0) = x0 + 1, [active](x0) = 0, [proper](x0) = 0, [ok](x0) = 0, [top](x0) = 0, [c] = 1, [true] = 0, [false] = 0, [active#](x0) = x0 Strict: active# f X -> active# X 1 + 1X >= 0 + 1X active# if(X1, X2, X3) -> active# X2 0 + 1X1 + 1X2 + 1X3 >= 0 + 1X2 active# if(X1, X2, X3) -> active# X1 0 + 1X1 + 1X2 + 1X3 >= 0 + 1X1 Weak: top ok X -> top active X 0 + 0X >= 0 + 0X top mark X -> top proper X 0 + 0X >= 0 + 0X proper false() -> ok false() 0 >= 0 proper true() -> ok true() 0 >= 0 proper f X -> f proper X 0 + 0X >= 1 + 0X proper c() -> ok c() 0 >= 0 proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 active f X -> f active X 0 + 0X >= 1 + 0X active f X -> mark if(X, c(), f true()) 0 + 0X >= 0 + 0X active if(false(), X, Y) -> mark Y 0 + 0X + 0Y >= 0 + 0Y active if(true(), X, Y) -> mark X 0 + 0X + 0Y >= 0 + 0X active if(X1, X2, X3) -> if(active X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 1X2 + 1X3 active if(X1, X2, X3) -> if(X1, active X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 1X3 f ok X -> ok f X 1 + 0X >= 0 + 0X f mark X -> mark f X 1 + 0X >= 0 + 0X if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 if(mark X1, X2, X3) -> mark if(X1, X2, X3) 0 + 0X1 + 1X2 + 1X3 >= 0 + 0X1 + 0X2 + 0X3 if(X1, mark X2, X3) -> mark if(X1, X2, X3) 0 + 1X1 + 0X2 + 1X3 >= 0 + 0X1 + 0X2 + 0X3 SCCS (1): Scc: {active# if(X1, X2, X3) -> active# X1, active# if(X1, X2, X3) -> active# X2} SCC (2): Strict: {active# if(X1, X2, X3) -> active# X1, active# if(X1, X2, X3) -> active# X2} Weak: { if(X1, mark X2, X3) -> mark if(X1, X2, X3), if(mark X1, X2, X3) -> mark if(X1, X2, X3), if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3), f mark X -> mark f X, f ok X -> ok f X, active if(X1, X2, X3) -> if(X1, active X2, X3), active if(X1, X2, X3) -> if(active X1, X2, X3), active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active f X -> mark if(X, c(), f true()), active f X -> f active X, proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3), proper c() -> ok c(), proper f X -> f proper X, proper true() -> ok true(), proper false() -> ok false(), 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: [if](x0, x1, x2) = x0 + x1 + 1, [mark](x0) = x0 + 1, [f](x0) = x0 + 1, [active](x0) = 0, [proper](x0) = x0 + 1, [ok](x0) = 0, [top](x0) = 0, [c] = 1, [true] = 1, [false] = 1, [active#](x0) = x0 + 1 Strict: active# if(X1, X2, X3) -> active# X2 2 + 1X1 + 1X2 + 0X3 >= 1 + 1X2 active# if(X1, X2, X3) -> active# X1 2 + 1X1 + 1X2 + 0X3 >= 1 + 1X1 Weak: top ok X -> top active X 0 + 0X >= 0 + 0X top mark X -> top proper X 0 + 0X >= 0 + 0X proper false() -> ok false() 2 >= 0 proper true() -> ok true() 2 >= 0 proper f X -> f proper X 2 + 1X >= 2 + 1X proper c() -> ok c() 2 >= 0 proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3) 2 + 1X1 + 1X2 + 0X3 >= 3 + 1X1 + 1X2 + 0X3 active f X -> f active X 0 + 0X >= 1 + 0X active f X -> mark if(X, c(), f true()) 0 + 0X >= 3 + 1X active if(false(), X, Y) -> mark Y 0 + 0X + 0Y >= 1 + 1Y active if(true(), X, Y) -> mark X 0 + 0X + 0Y >= 1 + 1X active if(X1, X2, X3) -> if(active X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 1X2 + 0X3 active if(X1, X2, X3) -> if(X1, active X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 1 + 1X1 + 0X2 + 0X3 f ok X -> ok f X 1 + 0X >= 0 + 0X f mark X -> mark f X 2 + 1X >= 2 + 1X if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 if(mark X1, X2, X3) -> mark if(X1, X2, X3) 2 + 1X1 + 1X2 + 0X3 >= 2 + 1X1 + 1X2 + 0X3 if(X1, mark X2, X3) -> mark if(X1, X2, X3) 2 + 1X1 + 1X2 + 0X3 >= 2 + 1X1 + 1X2 + 0X3 Qed SCC (4): Strict: {proper# if(X1, X2, X3) -> proper# X1, proper# if(X1, X2, X3) -> proper# X2, proper# if(X1, X2, X3) -> proper# X3, proper# f X -> proper# X} Weak: { if(X1, mark X2, X3) -> mark if(X1, X2, X3), if(mark X1, X2, X3) -> mark if(X1, X2, X3), if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3), f mark X -> mark f X, f ok X -> ok f X, active if(X1, X2, X3) -> if(X1, active X2, X3), active if(X1, X2, X3) -> if(active X1, X2, X3), active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active f X -> mark if(X, c(), f true()), active f X -> f active X, proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3), proper c() -> ok c(), proper f X -> f proper X, proper true() -> ok true(), proper false() -> ok false(), 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: [if](x0, x1, x2) = x0 + x1 + x2, [mark](x0) = 0, [f](x0) = x0 + 1, [active](x0) = 0, [proper](x0) = 0, [ok](x0) = 0, [top](x0) = 0, [c] = 1, [true] = 0, [false] = 0, [proper#](x0) = x0 Strict: proper# f X -> proper# X 1 + 1X >= 0 + 1X proper# if(X1, X2, X3) -> proper# X3 0 + 1X1 + 1X2 + 1X3 >= 0 + 1X3 proper# if(X1, X2, X3) -> proper# X2 0 + 1X1 + 1X2 + 1X3 >= 0 + 1X2 proper# if(X1, X2, X3) -> proper# X1 0 + 1X1 + 1X2 + 1X3 >= 0 + 1X1 Weak: top ok X -> top active X 0 + 0X >= 0 + 0X top mark X -> top proper X 0 + 0X >= 0 + 0X proper false() -> ok false() 0 >= 0 proper true() -> ok true() 0 >= 0 proper f X -> f proper X 0 + 0X >= 1 + 0X proper c() -> ok c() 0 >= 0 proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 active f X -> f active X 0 + 0X >= 1 + 0X active f X -> mark if(X, c(), f true()) 0 + 0X >= 0 + 0X active if(false(), X, Y) -> mark Y 0 + 0X + 0Y >= 0 + 0Y active if(true(), X, Y) -> mark X 0 + 0X + 0Y >= 0 + 0X active if(X1, X2, X3) -> if(active X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 1X2 + 1X3 active if(X1, X2, X3) -> if(X1, active X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 1X3 f ok X -> ok f X 1 + 0X >= 0 + 0X f mark X -> mark f X 1 + 0X >= 0 + 0X if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 if(mark X1, X2, X3) -> mark if(X1, X2, X3) 0 + 0X1 + 1X2 + 1X3 >= 0 + 0X1 + 0X2 + 0X3 if(X1, mark X2, X3) -> mark if(X1, X2, X3) 0 + 1X1 + 0X2 + 1X3 >= 0 + 0X1 + 0X2 + 0X3 SCCS (1): Scc: {proper# if(X1, X2, X3) -> proper# X1, proper# if(X1, X2, X3) -> proper# X2, proper# if(X1, X2, X3) -> proper# X3} SCC (3): Strict: {proper# if(X1, X2, X3) -> proper# X1, proper# if(X1, X2, X3) -> proper# X2, proper# if(X1, X2, X3) -> proper# X3} Weak: { if(X1, mark X2, X3) -> mark if(X1, X2, X3), if(mark X1, X2, X3) -> mark if(X1, X2, X3), if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3), f mark X -> mark f X, f ok X -> ok f X, active if(X1, X2, X3) -> if(X1, active X2, X3), active if(X1, X2, X3) -> if(active X1, X2, X3), active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active f X -> mark if(X, c(), f true()), active f X -> f active X, proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3), proper c() -> ok c(), proper f X -> f proper X, proper true() -> ok true(), proper false() -> ok false(), 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: [if](x0, x1, x2) = x0 + x1 + x2 + 1, [mark](x0) = x0, [f](x0) = 0, [active](x0) = x0 + 1, [proper](x0) = 0, [ok](x0) = x0 + 1, [top](x0) = 0, [c] = 0, [true] = 0, [false] = 0, [proper#](x0) = x0 + 1 Strict: proper# if(X1, X2, X3) -> proper# X3 2 + 1X1 + 1X2 + 1X3 >= 1 + 1X3 proper# if(X1, X2, X3) -> proper# X2 2 + 1X1 + 1X2 + 1X3 >= 1 + 1X2 proper# if(X1, X2, X3) -> proper# X1 2 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 Weak: top ok X -> top active X 0 + 0X >= 0 + 0X top mark X -> top proper X 0 + 0X >= 0 + 0X proper false() -> ok false() 0 >= 1 proper true() -> ok true() 0 >= 1 proper f X -> f proper X 0 + 0X >= 0 + 0X proper c() -> ok c() 0 >= 1 proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3) 0 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 active f X -> f active X 1 + 0X >= 0 + 0X active f X -> mark if(X, c(), f true()) 1 + 0X >= 1 + 1X active if(false(), X, Y) -> mark Y 2 + 1X + 1Y >= 0 + 1Y active if(true(), X, Y) -> mark X 2 + 1X + 1Y >= 0 + 1X active if(X1, X2, X3) -> if(active X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 2 + 1X1 + 1X2 + 1X3 active if(X1, X2, X3) -> if(X1, active X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 2 + 1X1 + 1X2 + 1X3 f ok X -> ok f X 0 + 0X >= 1 + 0X f mark X -> mark f X 0 + 0X >= 0 + 0X if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3) 4 + 1X1 + 1X2 + 1X3 >= 2 + 1X1 + 1X2 + 1X3 if(mark X1, X2, X3) -> mark if(X1, X2, X3) 1 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 if(X1, mark X2, X3) -> mark if(X1, X2, X3) 1 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 Qed SCC (3): Strict: { if#(X1, mark X2, X3) -> if#(X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3), if#(ok X1, ok X2, ok X3) -> if#(X1, X2, X3)} Weak: { if(X1, mark X2, X3) -> mark if(X1, X2, X3), if(mark X1, X2, X3) -> mark if(X1, X2, X3), if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3), f mark X -> mark f X, f ok X -> ok f X, active if(X1, X2, X3) -> if(X1, active X2, X3), active if(X1, X2, X3) -> if(active X1, X2, X3), active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active f X -> mark if(X, c(), f true()), active f X -> f active X, proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3), proper c() -> ok c(), proper f X -> f proper X, proper true() -> ok true(), proper false() -> ok false(), 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: [if](x0, x1, x2) = x0 + x1 + 1, [mark](x0) = x0 + 1, [f](x0) = x0 + 1, [active](x0) = x0 + 1, [proper](x0) = x0 + 1, [ok](x0) = x0 + 1, [top](x0) = 0, [c] = 1, [true] = 0, [false] = 0, [if#](x0, x1, x2) = x0 Strict: if#(ok X1, ok X2, ok X3) -> if#(X1, X2, X3) 1 + 0X1 + 0X2 + 1X3 >= 0 + 0X1 + 0X2 + 1X3 if#(mark X1, X2, X3) -> if#(X1, X2, X3) 0 + 0X1 + 0X2 + 1X3 >= 0 + 0X1 + 0X2 + 1X3 if#(X1, mark X2, X3) -> if#(X1, X2, X3) 0 + 0X1 + 0X2 + 1X3 >= 0 + 0X1 + 0X2 + 1X3 Weak: top ok X -> top active X 0 + 0X >= 0 + 0X top mark X -> top proper X 0 + 0X >= 0 + 0X proper false() -> ok false() 1 >= 1 proper true() -> ok true() 1 >= 1 proper f X -> f proper X 2 + 1X >= 2 + 1X proper c() -> ok c() 2 >= 2 proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3) 2 + 1X1 + 1X2 + 0X3 >= 3 + 1X1 + 1X2 + 0X3 active f X -> f active X 2 + 1X >= 2 + 1X active f X -> mark if(X, c(), f true()) 2 + 1X >= 3 + 1X active if(false(), X, Y) -> mark Y 2 + 1X + 0Y >= 1 + 1Y active if(true(), X, Y) -> mark X 2 + 1X + 0Y >= 1 + 1X active if(X1, X2, X3) -> if(active X1, X2, X3) 2 + 1X1 + 1X2 + 0X3 >= 2 + 1X1 + 1X2 + 0X3 active if(X1, X2, X3) -> if(X1, active X2, X3) 2 + 1X1 + 1X2 + 0X3 >= 2 + 1X1 + 1X2 + 0X3 f ok X -> ok f X 2 + 1X >= 2 + 1X f mark X -> mark f X 2 + 1X >= 2 + 1X if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3) 3 + 1X1 + 1X2 + 0X3 >= 2 + 1X1 + 1X2 + 0X3 if(mark X1, X2, X3) -> mark if(X1, X2, X3) 2 + 1X1 + 1X2 + 0X3 >= 2 + 1X1 + 1X2 + 0X3 if(X1, mark X2, X3) -> mark if(X1, X2, X3) 2 + 1X1 + 1X2 + 0X3 >= 2 + 1X1 + 1X2 + 0X3 SCCS (1): Scc: {if#(X1, mark X2, X3) -> if#(X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3)} SCC (2): Strict: {if#(X1, mark X2, X3) -> if#(X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3)} Weak: { if(X1, mark X2, X3) -> mark if(X1, X2, X3), if(mark X1, X2, X3) -> mark if(X1, X2, X3), if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3), f mark X -> mark f X, f ok X -> ok f X, active if(X1, X2, X3) -> if(X1, active X2, X3), active if(X1, X2, X3) -> if(active X1, X2, X3), active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active f X -> mark if(X, c(), f true()), active f X -> f active X, proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3), proper c() -> ok c(), proper f X -> f proper X, proper true() -> ok true(), proper false() -> ok false(), 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: [if](x0, x1, x2) = x0 + x1 + 1, [mark](x0) = x0 + 1, [f](x0) = x0 + 1, [active](x0) = x0 + 1, [proper](x0) = x0 + 1, [ok](x0) = 0, [top](x0) = 0, [c] = 1, [true] = 0, [false] = 1, [if#](x0, x1, x2) = x0 Strict: if#(mark X1, X2, X3) -> if#(X1, X2, X3) 1 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 if#(X1, mark X2, X3) -> if#(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 Weak: top ok X -> top active X 0 + 0X >= 0 + 0X top mark X -> top proper X 0 + 0X >= 0 + 0X proper false() -> ok false() 2 >= 0 proper true() -> ok true() 1 >= 0 proper f X -> f proper X 2 + 1X >= 2 + 1X proper c() -> ok c() 2 >= 0 proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3) 2 + 1X1 + 1X2 + 0X3 >= 3 + 1X1 + 1X2 + 0X3 active f X -> f active X 2 + 1X >= 2 + 1X active f X -> mark if(X, c(), f true()) 2 + 1X >= 3 + 1X active if(false(), X, Y) -> mark Y 3 + 1X + 0Y >= 1 + 1Y active if(true(), X, Y) -> mark X 2 + 1X + 0Y >= 1 + 1X active if(X1, X2, X3) -> if(active X1, X2, X3) 2 + 1X1 + 1X2 + 0X3 >= 2 + 1X1 + 1X2 + 0X3 active if(X1, X2, X3) -> if(X1, active X2, X3) 2 + 1X1 + 1X2 + 0X3 >= 2 + 1X1 + 1X2 + 0X3 f ok X -> ok f X 1 + 0X >= 0 + 0X f mark X -> mark f X 2 + 1X >= 2 + 1X if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 if(mark X1, X2, X3) -> mark if(X1, X2, X3) 2 + 1X1 + 1X2 + 0X3 >= 2 + 1X1 + 1X2 + 0X3 if(X1, mark X2, X3) -> mark if(X1, X2, X3) 2 + 1X1 + 1X2 + 0X3 >= 2 + 1X1 + 1X2 + 0X3 SCCS (1): Scc: {if#(X1, mark X2, X3) -> if#(X1, X2, X3)} SCC (1): Strict: {if#(X1, mark X2, X3) -> if#(X1, X2, X3)} Weak: { if(X1, mark X2, X3) -> mark if(X1, X2, X3), if(mark X1, X2, X3) -> mark if(X1, X2, X3), if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3), f mark X -> mark f X, f ok X -> ok f X, active if(X1, X2, X3) -> if(X1, active X2, X3), active if(X1, X2, X3) -> if(active X1, X2, X3), active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active f X -> mark if(X, c(), f true()), active f X -> f active X, proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3), proper c() -> ok c(), proper f X -> f proper X, proper true() -> ok true(), proper false() -> ok false(), 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: [if](x0, x1, x2) = x0 + x1 + 1, [mark](x0) = x0 + 1, [f](x0) = x0 + 1, [active](x0) = 0, [proper](x0) = x0 + 1, [ok](x0) = 0, [top](x0) = x0 + 1, [c] = 1, [true] = 1, [false] = 1, [if#](x0, x1, x2) = x0 Strict: if#(X1, mark X2, X3) -> if#(X1, X2, X3) 1 + 0X1 + 1X2 + 0X3 >= 0 + 0X1 + 1X2 + 0X3 Weak: top ok X -> top active X 1 + 0X >= 1 + 0X top mark X -> top proper X 2 + 1X >= 2 + 1X proper false() -> ok false() 2 >= 0 proper true() -> ok true() 2 >= 0 proper f X -> f proper X 2 + 1X >= 2 + 1X proper c() -> ok c() 2 >= 0 proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3) 2 + 1X1 + 1X2 + 0X3 >= 3 + 1X1 + 1X2 + 0X3 active f X -> f active X 0 + 0X >= 1 + 0X active f X -> mark if(X, c(), f true()) 0 + 0X >= 3 + 1X active if(false(), X, Y) -> mark Y 0 + 0X + 0Y >= 1 + 1Y active if(true(), X, Y) -> mark X 0 + 0X + 0Y >= 1 + 1X active if(X1, X2, X3) -> if(active X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 1X2 + 0X3 active if(X1, X2, X3) -> if(X1, active X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 1 + 1X1 + 0X2 + 0X3 f ok X -> ok f X 1 + 0X >= 0 + 0X f mark X -> mark f X 2 + 1X >= 2 + 1X if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 if(mark X1, X2, X3) -> mark if(X1, X2, X3) 2 + 1X1 + 1X2 + 0X3 >= 2 + 1X1 + 1X2 + 0X3 if(X1, mark X2, X3) -> mark if(X1, X2, X3) 2 + 1X1 + 1X2 + 0X3 >= 2 + 1X1 + 1X2 + 0X3 Qed SCC (2): Strict: {f# mark X -> f# X, f# ok X -> f# X} Weak: { if(X1, mark X2, X3) -> mark if(X1, X2, X3), if(mark X1, X2, X3) -> mark if(X1, X2, X3), if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3), f mark X -> mark f X, f ok X -> ok f X, active if(X1, X2, X3) -> if(X1, active X2, X3), active if(X1, X2, X3) -> if(active X1, X2, X3), active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active f X -> mark if(X, c(), f true()), active f X -> f active X, proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3), proper c() -> ok c(), proper f X -> f proper X, proper true() -> ok true(), proper false() -> ok false(), 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: [if](x0, x1, x2) = 0, [mark](x0) = x0, [f](x0) = 0, [active](x0) = 0, [proper](x0) = 0, [ok](x0) = x0 + 1, [top](x0) = x0, [c] = 1, [true] = 1, [false] = 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 1 + 1X >= 0 + 0X top mark X -> top proper X 0 + 1X >= 0 + 0X proper false() -> ok false() 0 >= 2 proper true() -> ok true() 0 >= 2 proper f X -> f proper X 0 + 0X >= 0 + 0X proper c() -> ok c() 0 >= 2 proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 active f X -> f active X 0 + 0X >= 0 + 0X active f X -> mark if(X, c(), f true()) 0 + 0X >= 0 + 0X active if(false(), X, Y) -> mark Y 0 + 0X + 0Y >= 0 + 1Y active if(true(), X, Y) -> mark X 0 + 0X + 0Y >= 0 + 1X active if(X1, X2, X3) -> if(active X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 active if(X1, X2, X3) -> if(X1, active X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 f ok X -> ok f X 0 + 0X >= 1 + 0X f mark X -> mark f X 0 + 0X >= 0 + 0X if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 if(mark X1, X2, X3) -> mark if(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 if(X1, mark X2, X3) -> mark if(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 SCCS (1): Scc: {f# mark X -> f# X} SCC (1): Strict: {f# mark X -> f# X} Weak: { if(X1, mark X2, X3) -> mark if(X1, X2, X3), if(mark X1, X2, X3) -> mark if(X1, X2, X3), if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3), f mark X -> mark f X, f ok X -> ok f X, active if(X1, X2, X3) -> if(X1, active X2, X3), active if(X1, X2, X3) -> if(active X1, X2, X3), active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active f X -> mark if(X, c(), f true()), active f X -> f active X, proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3), proper c() -> ok c(), proper f X -> f proper X, proper true() -> ok true(), proper false() -> ok false(), 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: [if](x0, x1, x2) = x0 + x1 + 1, [mark](x0) = x0 + 1, [f](x0) = x0 + 1, [active](x0) = 0, [proper](x0) = x0 + 1, [ok](x0) = 0, [top](x0) = x0 + 1, [c] = 1, [true] = 1, [false] = 1, [f#](x0) = x0 Strict: f# mark X -> f# X 1 + 1X >= 0 + 1X Weak: top ok X -> top active X 1 + 0X >= 1 + 0X top mark X -> top proper X 2 + 1X >= 2 + 1X proper false() -> ok false() 2 >= 0 proper true() -> ok true() 2 >= 0 proper f X -> f proper X 2 + 1X >= 2 + 1X proper c() -> ok c() 2 >= 0 proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3) 2 + 1X1 + 1X2 + 0X3 >= 3 + 1X1 + 1X2 + 0X3 active f X -> f active X 0 + 0X >= 1 + 0X active f X -> mark if(X, c(), f true()) 0 + 0X >= 3 + 1X active if(false(), X, Y) -> mark Y 0 + 0X + 0Y >= 1 + 1Y active if(true(), X, Y) -> mark X 0 + 0X + 0Y >= 1 + 1X active if(X1, X2, X3) -> if(active X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 1X2 + 0X3 active if(X1, X2, X3) -> if(X1, active X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 1 + 1X1 + 0X2 + 0X3 f ok X -> ok f X 1 + 0X >= 0 + 0X f mark X -> mark f X 2 + 1X >= 2 + 1X if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 if(mark X1, X2, X3) -> mark if(X1, X2, X3) 2 + 1X1 + 1X2 + 0X3 >= 2 + 1X1 + 1X2 + 0X3 if(X1, mark X2, X3) -> mark if(X1, X2, X3) 2 + 1X1 + 1X2 + 0X3 >= 2 + 1X1 + 1X2 + 0X3 Qed