MAYBE Time: 0.832842 TRS: { mark 0() -> active 0(), mark p X -> active p mark X, mark s X -> active s mark X, mark true() -> active true(), mark leq(X1, X2) -> active leq(mark X1, mark X2), mark false() -> active false(), mark if(X1, X2, X3) -> active if(mark X1, X2, X3), mark diff(X1, X2) -> active diff(mark X1, mark X2), active p 0() -> mark 0(), active p s X -> mark X, active leq(0(), Y) -> mark true(), active leq(s X, 0()) -> mark false(), active leq(s X, s Y) -> mark leq(X, Y), active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active diff(X, Y) -> mark if(leq(X, Y), 0(), s diff(p X, Y)), p mark X -> p X, p active X -> p X, s mark X -> s X, s active X -> s X, leq(X1, mark X2) -> leq(X1, X2), leq(X1, active X2) -> leq(X1, X2), leq(mark X1, X2) -> leq(X1, X2), leq(active X1, X2) -> leq(X1, X2), if(X1, X2, mark X3) -> if(X1, X2, X3), if(X1, X2, active X3) -> if(X1, X2, X3), if(X1, mark X2, X3) -> if(X1, X2, X3), if(X1, active X2, X3) -> if(X1, X2, X3), if(mark X1, X2, X3) -> if(X1, X2, X3), if(active X1, X2, X3) -> if(X1, X2, X3), diff(X1, mark X2) -> diff(X1, X2), diff(X1, active X2) -> diff(X1, X2), diff(mark X1, X2) -> diff(X1, X2), diff(active X1, X2) -> diff(X1, X2)} DP: DP: { mark# 0() -> active# 0(), mark# p X -> mark# X, mark# p X -> active# p mark X, mark# p X -> p# mark X, mark# s X -> mark# X, mark# s X -> active# s mark X, mark# s X -> s# mark X, mark# true() -> active# true(), mark# leq(X1, X2) -> mark# X1, mark# leq(X1, X2) -> mark# X2, mark# leq(X1, X2) -> active# leq(mark X1, mark X2), mark# leq(X1, X2) -> leq#(mark X1, mark X2), mark# false() -> active# false(), mark# if(X1, X2, X3) -> mark# X1, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), mark# if(X1, X2, X3) -> if#(mark X1, X2, X3), mark# diff(X1, X2) -> mark# X1, mark# diff(X1, X2) -> mark# X2, mark# diff(X1, X2) -> active# diff(mark X1, mark X2), mark# diff(X1, X2) -> diff#(mark X1, mark X2), active# p 0() -> mark# 0(), active# p s X -> mark# X, active# leq(0(), Y) -> mark# true(), active# leq(s X, 0()) -> mark# false(), active# leq(s X, s Y) -> mark# leq(X, Y), active# leq(s X, s Y) -> leq#(X, Y), active# if(true(), X, Y) -> mark# X, active# if(false(), X, Y) -> mark# Y, active# diff(X, Y) -> mark# if(leq(X, Y), 0(), s diff(p X, Y)), active# diff(X, Y) -> p# X, active# diff(X, Y) -> s# diff(p X, Y), active# diff(X, Y) -> leq#(X, Y), active# diff(X, Y) -> if#(leq(X, Y), 0(), s diff(p X, Y)), active# diff(X, Y) -> diff#(p X, Y), p# mark X -> p# X, p# active X -> p# X, s# mark X -> s# X, s# active X -> s# X, leq#(X1, mark X2) -> leq#(X1, X2), leq#(X1, active X2) -> leq#(X1, X2), leq#(mark X1, X2) -> leq#(X1, X2), leq#(active X1, X2) -> leq#(X1, X2), if#(X1, X2, mark X3) -> if#(X1, X2, X3), if#(X1, X2, active X3) -> if#(X1, X2, X3), if#(X1, mark X2, X3) -> if#(X1, X2, X3), if#(X1, active X2, X3) -> if#(X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3), if#(active X1, X2, X3) -> if#(X1, X2, X3), diff#(X1, mark X2) -> diff#(X1, X2), diff#(X1, active X2) -> diff#(X1, X2), diff#(mark X1, X2) -> diff#(X1, X2), diff#(active X1, X2) -> diff#(X1, X2)} TRS: { mark 0() -> active 0(), mark p X -> active p mark X, mark s X -> active s mark X, mark true() -> active true(), mark leq(X1, X2) -> active leq(mark X1, mark X2), mark false() -> active false(), mark if(X1, X2, X3) -> active if(mark X1, X2, X3), mark diff(X1, X2) -> active diff(mark X1, mark X2), active p 0() -> mark 0(), active p s X -> mark X, active leq(0(), Y) -> mark true(), active leq(s X, 0()) -> mark false(), active leq(s X, s Y) -> mark leq(X, Y), active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active diff(X, Y) -> mark if(leq(X, Y), 0(), s diff(p X, Y)), p mark X -> p X, p active X -> p X, s mark X -> s X, s active X -> s X, leq(X1, mark X2) -> leq(X1, X2), leq(X1, active X2) -> leq(X1, X2), leq(mark X1, X2) -> leq(X1, X2), leq(active X1, X2) -> leq(X1, X2), if(X1, X2, mark X3) -> if(X1, X2, X3), if(X1, X2, active X3) -> if(X1, X2, X3), if(X1, mark X2, X3) -> if(X1, X2, X3), if(X1, active X2, X3) -> if(X1, X2, X3), if(mark X1, X2, X3) -> if(X1, X2, X3), if(active X1, X2, X3) -> if(X1, X2, X3), diff(X1, mark X2) -> diff(X1, X2), diff(X1, active X2) -> diff(X1, X2), diff(mark X1, X2) -> diff(X1, X2), diff(active X1, X2) -> diff(X1, X2)} EDG: { (mark# true() -> active# true(), active# diff(X, Y) -> diff#(p X, Y)) (mark# true() -> active# true(), active# diff(X, Y) -> if#(leq(X, Y), 0(), s diff(p X, Y))) (mark# true() -> active# true(), active# diff(X, Y) -> leq#(X, Y)) (mark# true() -> active# true(), active# diff(X, Y) -> s# diff(p X, Y)) (mark# true() -> active# true(), active# diff(X, Y) -> p# X) (mark# true() -> active# true(), active# diff(X, Y) -> mark# if(leq(X, Y), 0(), s diff(p X, Y))) (mark# true() -> active# true(), active# if(false(), X, Y) -> mark# Y) (mark# true() -> active# true(), active# if(true(), X, Y) -> mark# X) (mark# true() -> active# true(), active# leq(s X, s Y) -> leq#(X, Y)) (mark# true() -> active# true(), active# leq(s X, s Y) -> mark# leq(X, Y)) (mark# true() -> active# true(), active# leq(s X, 0()) -> mark# false()) (mark# true() -> active# true(), active# leq(0(), Y) -> mark# true()) (mark# true() -> active# true(), active# p s X -> mark# X) (mark# true() -> active# true(), active# p 0() -> mark# 0()) (active# p 0() -> mark# 0(), mark# diff(X1, X2) -> diff#(mark X1, mark X2)) (active# p 0() -> mark# 0(), mark# diff(X1, X2) -> active# diff(mark X1, mark X2)) (active# p 0() -> mark# 0(), mark# diff(X1, X2) -> mark# X2) (active# p 0() -> mark# 0(), mark# diff(X1, X2) -> mark# X1) (active# p 0() -> mark# 0(), mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (active# p 0() -> mark# 0(), mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (active# p 0() -> mark# 0(), mark# if(X1, X2, X3) -> mark# X1) (active# p 0() -> mark# 0(), mark# false() -> active# false()) (active# p 0() -> mark# 0(), mark# leq(X1, X2) -> leq#(mark X1, mark X2)) (active# p 0() -> mark# 0(), mark# leq(X1, X2) -> active# leq(mark X1, mark X2)) (active# p 0() -> mark# 0(), mark# leq(X1, X2) -> mark# X2) (active# p 0() -> mark# 0(), mark# leq(X1, X2) -> mark# X1) (active# p 0() -> mark# 0(), mark# true() -> active# true()) (active# p 0() -> mark# 0(), mark# s X -> s# mark X) (active# p 0() -> mark# 0(), mark# s X -> active# s mark X) (active# p 0() -> mark# 0(), mark# s X -> mark# X) (active# p 0() -> mark# 0(), mark# p X -> p# mark X) (active# p 0() -> mark# 0(), mark# p X -> active# p mark X) (active# p 0() -> mark# 0(), mark# p X -> mark# X) (active# p 0() -> mark# 0(), mark# 0() -> active# 0()) (active# leq(s X, 0()) -> mark# false(), mark# diff(X1, X2) -> diff#(mark X1, mark X2)) (active# leq(s X, 0()) -> mark# false(), mark# diff(X1, X2) -> active# diff(mark X1, mark X2)) (active# leq(s X, 0()) -> mark# false(), mark# diff(X1, X2) -> mark# X2) (active# leq(s X, 0()) -> mark# false(), mark# diff(X1, X2) -> mark# X1) (active# leq(s X, 0()) -> mark# false(), mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (active# leq(s X, 0()) -> mark# false(), mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (active# leq(s X, 0()) -> mark# false(), mark# if(X1, X2, X3) -> mark# X1) (active# leq(s X, 0()) -> mark# false(), mark# false() -> active# false()) (active# leq(s X, 0()) -> mark# false(), mark# leq(X1, X2) -> leq#(mark X1, mark X2)) (active# leq(s X, 0()) -> mark# false(), mark# leq(X1, X2) -> active# leq(mark X1, mark X2)) (active# leq(s X, 0()) -> mark# false(), mark# leq(X1, X2) -> mark# X2) (active# leq(s X, 0()) -> mark# false(), mark# leq(X1, X2) -> mark# X1) (active# leq(s X, 0()) -> mark# false(), mark# true() -> active# true()) (active# leq(s X, 0()) -> mark# false(), mark# s X -> s# mark X) (active# leq(s X, 0()) -> mark# false(), mark# s X -> active# s mark X) (active# leq(s X, 0()) -> mark# false(), mark# s X -> mark# X) (active# leq(s X, 0()) -> mark# false(), mark# p X -> p# mark X) (active# leq(s X, 0()) -> mark# false(), mark# p X -> active# p mark X) (active# leq(s X, 0()) -> mark# false(), mark# p X -> mark# X) (active# leq(s X, 0()) -> mark# false(), mark# 0() -> active# 0()) (mark# s X -> mark# X, mark# diff(X1, X2) -> diff#(mark X1, mark X2)) (mark# s X -> mark# X, mark# diff(X1, X2) -> active# diff(mark X1, mark X2)) (mark# s X -> mark# X, mark# diff(X1, X2) -> mark# X2) (mark# s X -> mark# X, mark# diff(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (mark# s X -> mark# X, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (mark# s X -> mark# X, mark# if(X1, X2, X3) -> mark# X1) (mark# s X -> mark# X, mark# false() -> active# false()) (mark# s X -> mark# X, mark# leq(X1, X2) -> leq#(mark X1, mark X2)) (mark# s X -> mark# X, mark# leq(X1, X2) -> active# leq(mark X1, mark X2)) (mark# s X -> mark# X, mark# leq(X1, X2) -> mark# X2) (mark# s X -> mark# X, mark# leq(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# true() -> active# true()) (mark# s X -> mark# X, mark# s X -> s# mark X) (mark# s X -> mark# X, mark# s X -> active# s mark X) (mark# s X -> mark# X, mark# s X -> mark# X) (mark# s X -> mark# X, mark# p X -> p# mark X) (mark# s X -> mark# X, mark# p X -> active# p mark X) (mark# s X -> mark# X, mark# p X -> mark# X) (mark# s X -> mark# X, mark# 0() -> active# 0()) (active# if(true(), X, Y) -> mark# X, mark# diff(X1, X2) -> diff#(mark X1, mark X2)) (active# if(true(), X, Y) -> mark# X, mark# diff(X1, X2) -> active# diff(mark X1, mark X2)) (active# if(true(), X, Y) -> mark# X, mark# diff(X1, X2) -> mark# X2) (active# if(true(), X, Y) -> mark# X, mark# diff(X1, X2) -> mark# X1) (active# if(true(), X, Y) -> mark# X, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (active# if(true(), X, Y) -> mark# X, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (active# if(true(), X, Y) -> mark# X, mark# if(X1, X2, X3) -> mark# X1) (active# if(true(), X, Y) -> mark# X, mark# false() -> active# false()) (active# if(true(), X, Y) -> mark# X, mark# leq(X1, X2) -> leq#(mark X1, mark X2)) (active# if(true(), X, Y) -> mark# X, mark# leq(X1, X2) -> active# leq(mark X1, mark X2)) (active# if(true(), X, Y) -> mark# X, mark# leq(X1, X2) -> mark# X2) (active# if(true(), X, Y) -> mark# X, mark# leq(X1, X2) -> mark# X1) (active# if(true(), X, Y) -> mark# X, mark# true() -> active# true()) (active# if(true(), X, Y) -> mark# X, mark# s X -> s# mark X) (active# if(true(), X, Y) -> mark# X, mark# s X -> active# s mark X) (active# if(true(), X, Y) -> mark# X, mark# s X -> mark# X) (active# if(true(), X, Y) -> mark# X, mark# p X -> p# mark X) (active# if(true(), X, Y) -> mark# X, mark# p X -> active# p mark X) (active# if(true(), X, Y) -> mark# X, mark# p X -> mark# X) (active# if(true(), X, Y) -> mark# X, mark# 0() -> active# 0()) (p# mark X -> p# X, p# active X -> p# X) (p# mark X -> p# X, p# mark X -> p# X) (s# mark X -> s# X, s# active X -> s# X) (s# mark X -> s# X, s# mark X -> s# X) (active# diff(X, Y) -> if#(leq(X, Y), 0(), s diff(p X, Y)), if#(active X1, X2, X3) -> if#(X1, X2, X3)) (active# diff(X, Y) -> if#(leq(X, Y), 0(), s diff(p X, Y)), if#(mark X1, X2, X3) -> if#(X1, X2, X3)) (active# diff(X, Y) -> if#(leq(X, Y), 0(), s diff(p X, Y)), if#(X1, active X2, X3) -> if#(X1, X2, X3)) (active# diff(X, Y) -> if#(leq(X, Y), 0(), s diff(p X, Y)), if#(X1, mark X2, X3) -> if#(X1, X2, X3)) (active# diff(X, Y) -> if#(leq(X, Y), 0(), s diff(p X, Y)), if#(X1, X2, active X3) -> if#(X1, X2, X3)) (active# diff(X, Y) -> if#(leq(X, Y), 0(), s diff(p X, Y)), if#(X1, X2, mark X3) -> if#(X1, X2, X3)) (mark# s X -> active# s mark X, active# diff(X, Y) -> diff#(p X, Y)) (mark# s X -> active# s mark X, active# diff(X, Y) -> if#(leq(X, Y), 0(), s diff(p X, Y))) (mark# s X -> active# s mark X, active# diff(X, Y) -> leq#(X, Y)) (mark# s X -> active# s mark X, active# diff(X, Y) -> s# diff(p X, Y)) (mark# s X -> active# s mark X, active# diff(X, Y) -> p# X) (mark# s X -> active# s mark X, active# diff(X, Y) -> mark# if(leq(X, Y), 0(), s diff(p X, Y))) (mark# s X -> active# s mark X, active# if(false(), X, Y) -> mark# Y) (mark# s X -> active# s mark X, active# if(true(), X, Y) -> mark# X) (mark# s X -> active# s mark X, active# leq(s X, s Y) -> leq#(X, Y)) (mark# s X -> active# s mark X, active# leq(s X, s Y) -> mark# leq(X, Y)) (mark# s X -> active# s mark X, active# leq(s X, 0()) -> mark# false()) (mark# s X -> active# s mark X, active# leq(0(), Y) -> mark# true()) (mark# s X -> active# s mark X, active# p s X -> mark# X) (mark# s X -> active# s mark X, active# p 0() -> mark# 0()) (active# leq(s X, s Y) -> mark# leq(X, Y), mark# diff(X1, X2) -> diff#(mark X1, mark X2)) (active# leq(s X, s Y) -> mark# leq(X, Y), mark# diff(X1, X2) -> active# diff(mark X1, mark X2)) (active# leq(s X, s Y) -> mark# leq(X, Y), mark# diff(X1, X2) -> mark# X2) (active# leq(s X, s Y) -> mark# leq(X, Y), mark# diff(X1, X2) -> mark# X1) (active# leq(s X, s Y) -> mark# leq(X, Y), mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (active# leq(s X, s Y) -> mark# leq(X, Y), mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (active# leq(s X, s Y) -> mark# leq(X, Y), mark# if(X1, X2, X3) -> mark# X1) (active# leq(s X, s Y) -> mark# leq(X, Y), mark# false() -> active# false()) (active# leq(s X, s Y) -> mark# leq(X, Y), mark# leq(X1, X2) -> leq#(mark X1, mark X2)) (active# leq(s X, s Y) -> mark# leq(X, Y), mark# leq(X1, X2) -> active# leq(mark X1, mark X2)) (active# leq(s X, s Y) -> mark# leq(X, Y), mark# leq(X1, X2) -> mark# X2) (active# leq(s X, s Y) -> mark# leq(X, Y), mark# leq(X1, X2) -> mark# X1) (active# leq(s X, s Y) -> mark# leq(X, Y), mark# true() -> active# true()) (active# leq(s X, s Y) -> mark# leq(X, Y), mark# s X -> s# mark X) (active# leq(s X, s Y) -> mark# leq(X, Y), mark# s X -> active# s mark X) (active# leq(s X, s Y) -> mark# leq(X, Y), mark# s X -> mark# X) (active# leq(s X, s Y) -> mark# leq(X, Y), mark# p X -> p# mark X) (active# leq(s X, s Y) -> mark# leq(X, Y), mark# p X -> active# p mark X) (active# leq(s X, s Y) -> mark# leq(X, Y), mark# p X -> mark# X) (active# leq(s X, s Y) -> mark# leq(X, Y), mark# 0() -> active# 0()) (mark# leq(X1, X2) -> leq#(mark X1, mark X2), leq#(active X1, X2) -> leq#(X1, X2)) (mark# leq(X1, X2) -> leq#(mark X1, mark X2), leq#(mark X1, X2) -> leq#(X1, X2)) (mark# leq(X1, X2) -> leq#(mark X1, mark X2), leq#(X1, active X2) -> leq#(X1, X2)) (mark# leq(X1, X2) -> leq#(mark X1, mark X2), leq#(X1, mark X2) -> leq#(X1, X2)) (mark# leq(X1, X2) -> mark# X2, mark# diff(X1, X2) -> diff#(mark X1, mark X2)) (mark# leq(X1, X2) -> mark# X2, mark# diff(X1, X2) -> active# diff(mark X1, mark X2)) (mark# leq(X1, X2) -> mark# X2, mark# diff(X1, X2) -> mark# X2) (mark# leq(X1, X2) -> mark# X2, mark# diff(X1, X2) -> mark# X1) (mark# leq(X1, X2) -> mark# X2, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (mark# leq(X1, X2) -> mark# X2, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (mark# leq(X1, X2) -> mark# X2, mark# if(X1, X2, X3) -> mark# X1) (mark# leq(X1, X2) -> mark# X2, mark# false() -> active# false()) (mark# leq(X1, X2) -> mark# X2, mark# leq(X1, X2) -> leq#(mark X1, mark X2)) (mark# leq(X1, X2) -> mark# X2, mark# leq(X1, X2) -> active# leq(mark X1, mark X2)) (mark# leq(X1, X2) -> mark# X2, mark# leq(X1, X2) -> mark# X2) (mark# leq(X1, X2) -> mark# X2, mark# leq(X1, X2) -> mark# X1) (mark# leq(X1, X2) -> mark# X2, mark# true() -> active# true()) (mark# leq(X1, X2) -> mark# X2, mark# s X -> s# mark X) (mark# leq(X1, X2) -> mark# X2, mark# s X -> active# s mark X) (mark# leq(X1, X2) -> mark# X2, mark# s X -> mark# X) (mark# leq(X1, X2) -> mark# X2, mark# p X -> p# mark X) (mark# leq(X1, X2) -> mark# X2, mark# p X -> active# p mark X) (mark# leq(X1, X2) -> mark# X2, mark# p X -> mark# X) (mark# leq(X1, X2) -> mark# X2, mark# 0() -> active# 0()) (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# diff(X, Y) -> diff#(p X, Y)) (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# diff(X, Y) -> if#(leq(X, Y), 0(), s diff(p X, Y))) (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# diff(X, Y) -> leq#(X, Y)) (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# diff(X, Y) -> s# diff(p X, Y)) (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# diff(X, Y) -> p# X) (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# diff(X, Y) -> mark# if(leq(X, Y), 0(), s diff(p X, Y))) (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# if(false(), X, Y) -> mark# Y) (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# if(true(), X, Y) -> mark# X) (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# leq(s X, s Y) -> leq#(X, Y)) (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# leq(s X, s Y) -> mark# leq(X, Y)) (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# leq(s X, 0()) -> mark# false()) (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# leq(0(), Y) -> mark# true()) (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# p s X -> mark# X) (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# p 0() -> mark# 0()) (mark# leq(X1, X2) -> mark# X1, mark# diff(X1, X2) -> diff#(mark X1, mark X2)) (mark# leq(X1, X2) -> mark# X1, mark# diff(X1, X2) -> active# diff(mark X1, mark X2)) (mark# leq(X1, X2) -> mark# X1, mark# diff(X1, X2) -> mark# X2) (mark# leq(X1, X2) -> mark# X1, mark# diff(X1, X2) -> mark# X1) (mark# leq(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (mark# leq(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (mark# leq(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> mark# X1) (mark# leq(X1, X2) -> mark# X1, mark# false() -> active# false()) (mark# leq(X1, X2) -> mark# X1, mark# leq(X1, X2) -> leq#(mark X1, mark X2)) (mark# leq(X1, X2) -> mark# X1, mark# leq(X1, X2) -> active# leq(mark X1, mark X2)) (mark# leq(X1, X2) -> mark# X1, mark# leq(X1, X2) -> mark# X2) (mark# leq(X1, X2) -> mark# X1, mark# leq(X1, X2) -> mark# X1) (mark# leq(X1, X2) -> mark# X1, mark# true() -> active# true()) (mark# leq(X1, X2) -> mark# X1, mark# s X -> s# mark X) (mark# leq(X1, X2) -> mark# X1, mark# s X -> active# s mark X) (mark# leq(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# leq(X1, X2) -> mark# X1, mark# p X -> p# mark X) (mark# leq(X1, X2) -> mark# X1, mark# p X -> active# p mark X) (mark# leq(X1, X2) -> mark# X1, mark# p X -> mark# X) (mark# leq(X1, X2) -> mark# X1, mark# 0() -> active# 0()) (mark# diff(X1, X2) -> mark# X1, mark# diff(X1, X2) -> diff#(mark X1, mark X2)) (mark# diff(X1, X2) -> mark# X1, mark# diff(X1, X2) -> active# diff(mark X1, mark X2)) (mark# diff(X1, X2) -> mark# X1, mark# diff(X1, X2) -> mark# X2) (mark# diff(X1, X2) -> mark# X1, mark# diff(X1, X2) -> mark# X1) (mark# diff(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (mark# diff(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (mark# diff(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> mark# X1) (mark# diff(X1, X2) -> mark# X1, mark# false() -> active# false()) (mark# diff(X1, X2) -> mark# X1, mark# leq(X1, X2) -> leq#(mark X1, mark X2)) (mark# diff(X1, X2) -> mark# X1, mark# leq(X1, X2) -> active# leq(mark X1, mark X2)) (mark# diff(X1, X2) -> mark# X1, mark# leq(X1, X2) -> mark# X2) (mark# diff(X1, X2) -> mark# X1, mark# leq(X1, X2) -> mark# X1) (mark# diff(X1, X2) -> mark# X1, mark# true() -> active# true()) (mark# diff(X1, X2) -> mark# X1, mark# s X -> s# mark X) (mark# diff(X1, X2) -> mark# X1, mark# s X -> active# s mark X) (mark# diff(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# diff(X1, X2) -> mark# X1, mark# p X -> p# mark X) (mark# diff(X1, X2) -> mark# X1, mark# p X -> active# p mark X) (mark# diff(X1, X2) -> mark# X1, mark# p X -> mark# X) (mark# diff(X1, X2) -> mark# X1, mark# 0() -> active# 0()) (active# diff(X, Y) -> leq#(X, Y), leq#(active X1, X2) -> leq#(X1, X2)) (active# diff(X, Y) -> leq#(X, Y), leq#(mark X1, X2) -> leq#(X1, X2)) (active# diff(X, Y) -> leq#(X, Y), leq#(X1, active X2) -> leq#(X1, X2)) (active# diff(X, Y) -> leq#(X, Y), leq#(X1, mark X2) -> leq#(X1, X2)) (if#(X1, X2, mark X3) -> if#(X1, X2, X3), if#(active X1, X2, X3) -> if#(X1, X2, X3)) (if#(X1, X2, mark X3) -> if#(X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3)) (if#(X1, X2, mark X3) -> if#(X1, X2, X3), if#(X1, active X2, X3) -> if#(X1, X2, X3)) (if#(X1, X2, mark X3) -> if#(X1, X2, X3), if#(X1, mark X2, X3) -> if#(X1, X2, X3)) (if#(X1, X2, mark X3) -> if#(X1, X2, X3), if#(X1, X2, active X3) -> if#(X1, X2, X3)) (if#(X1, X2, mark X3) -> if#(X1, X2, X3), if#(X1, X2, mark X3) -> if#(X1, X2, X3)) (if#(X1, mark X2, X3) -> if#(X1, X2, X3), if#(active 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#(X1, mark X2, X3) -> if#(X1, X2, X3), if#(X1, active 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#(X1, mark X2, X3) -> if#(X1, X2, X3), if#(X1, X2, active X3) -> if#(X1, X2, X3)) (if#(X1, mark X2, X3) -> if#(X1, X2, X3), if#(X1, X2, mark X3) -> if#(X1, X2, X3)) (if#(mark X1, X2, X3) -> if#(X1, X2, X3), if#(active 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#(mark X1, X2, X3) -> if#(X1, X2, X3), if#(X1, active 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#(mark X1, X2, X3) -> if#(X1, X2, X3), if#(X1, X2, active X3) -> if#(X1, X2, X3)) (if#(mark X1, X2, X3) -> if#(X1, X2, X3), if#(X1, X2, mark X3) -> if#(X1, X2, X3)) (leq#(X1, mark X2) -> leq#(X1, X2), leq#(active X1, X2) -> leq#(X1, X2)) (leq#(X1, mark X2) -> leq#(X1, X2), leq#(mark X1, X2) -> leq#(X1, X2)) (leq#(X1, mark X2) -> leq#(X1, X2), leq#(X1, active X2) -> leq#(X1, X2)) (leq#(X1, mark X2) -> leq#(X1, X2), leq#(X1, mark X2) -> leq#(X1, X2)) (leq#(mark X1, X2) -> leq#(X1, X2), leq#(active X1, X2) -> leq#(X1, X2)) (leq#(mark X1, X2) -> leq#(X1, X2), leq#(mark X1, X2) -> leq#(X1, X2)) (leq#(mark X1, X2) -> leq#(X1, X2), leq#(X1, active X2) -> leq#(X1, X2)) (leq#(mark X1, X2) -> leq#(X1, X2), leq#(X1, mark X2) -> leq#(X1, X2)) (diff#(X1, mark X2) -> diff#(X1, X2), diff#(active X1, X2) -> diff#(X1, X2)) (diff#(X1, mark X2) -> diff#(X1, X2), diff#(mark X1, X2) -> diff#(X1, X2)) (diff#(X1, mark X2) -> diff#(X1, X2), diff#(X1, active X2) -> diff#(X1, X2)) (diff#(X1, mark X2) -> diff#(X1, X2), diff#(X1, mark X2) -> diff#(X1, X2)) (diff#(mark X1, X2) -> diff#(X1, X2), diff#(active X1, X2) -> diff#(X1, X2)) (diff#(mark X1, X2) -> diff#(X1, X2), diff#(mark X1, X2) -> diff#(X1, X2)) (diff#(mark X1, X2) -> diff#(X1, X2), diff#(X1, active X2) -> diff#(X1, X2)) (diff#(mark X1, X2) -> diff#(X1, X2), diff#(X1, mark X2) -> diff#(X1, X2)) (active# if(false(), X, Y) -> mark# Y, mark# diff(X1, X2) -> diff#(mark X1, mark X2)) (active# if(false(), X, Y) -> mark# Y, mark# diff(X1, X2) -> active# diff(mark X1, mark X2)) (active# if(false(), X, Y) -> mark# Y, mark# diff(X1, X2) -> mark# X2) (active# if(false(), X, Y) -> mark# Y, mark# diff(X1, X2) -> mark# X1) (active# if(false(), X, Y) -> mark# Y, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (active# if(false(), X, Y) -> mark# Y, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (active# if(false(), X, Y) -> mark# Y, mark# if(X1, X2, X3) -> mark# X1) (active# if(false(), X, Y) -> mark# Y, mark# false() -> active# false()) (active# if(false(), X, Y) -> mark# Y, mark# leq(X1, X2) -> leq#(mark X1, mark X2)) (active# if(false(), X, Y) -> mark# Y, mark# leq(X1, X2) -> active# leq(mark X1, mark X2)) (active# if(false(), X, Y) -> mark# Y, mark# leq(X1, X2) -> mark# X2) (active# if(false(), X, Y) -> mark# Y, mark# leq(X1, X2) -> mark# X1) (active# if(false(), X, Y) -> mark# Y, mark# true() -> active# true()) (active# if(false(), X, Y) -> mark# Y, mark# s X -> s# mark X) (active# if(false(), X, Y) -> mark# Y, mark# s X -> active# s mark X) (active# if(false(), X, Y) -> mark# Y, mark# s X -> mark# X) (active# if(false(), X, Y) -> mark# Y, mark# p X -> p# mark X) (active# if(false(), X, Y) -> mark# Y, mark# p X -> active# p mark X) (active# if(false(), X, Y) -> mark# Y, mark# p X -> mark# X) (active# if(false(), X, Y) -> mark# Y, mark# 0() -> active# 0()) (mark# diff(X1, X2) -> active# diff(mark X1, mark X2), active# diff(X, Y) -> diff#(p X, Y)) (mark# diff(X1, X2) -> active# diff(mark X1, mark X2), active# diff(X, Y) -> if#(leq(X, Y), 0(), s diff(p X, Y))) (mark# diff(X1, X2) -> active# diff(mark X1, mark X2), active# diff(X, Y) -> leq#(X, Y)) (mark# diff(X1, X2) -> active# diff(mark X1, mark X2), active# diff(X, Y) -> s# diff(p X, Y)) (mark# diff(X1, X2) -> active# diff(mark X1, mark X2), active# diff(X, Y) -> p# X) (mark# diff(X1, X2) -> active# diff(mark X1, mark X2), active# diff(X, Y) -> mark# if(leq(X, Y), 0(), s diff(p X, Y))) (mark# diff(X1, X2) -> active# diff(mark X1, mark X2), active# if(false(), X, Y) -> mark# Y) (mark# diff(X1, X2) -> active# diff(mark X1, mark X2), active# if(true(), X, Y) -> mark# X) (mark# diff(X1, X2) -> active# diff(mark X1, mark X2), active# leq(s X, s Y) -> leq#(X, Y)) (mark# diff(X1, X2) -> active# diff(mark X1, mark X2), active# leq(s X, s Y) -> mark# leq(X, Y)) (mark# diff(X1, X2) -> active# diff(mark X1, mark X2), active# leq(s X, 0()) -> mark# false()) (mark# diff(X1, X2) -> active# diff(mark X1, mark X2), active# leq(0(), Y) -> mark# true()) (mark# diff(X1, X2) -> active# diff(mark X1, mark X2), active# p s X -> mark# X) (mark# diff(X1, X2) -> active# diff(mark X1, mark X2), active# p 0() -> mark# 0()) (mark# s X -> s# mark X, s# active X -> s# X) (mark# s X -> s# mark X, s# mark X -> s# X) (mark# p X -> p# mark X, p# mark X -> p# X) (mark# p X -> p# mark X, p# active X -> p# X) (mark# leq(X1, X2) -> active# leq(mark X1, mark X2), active# p 0() -> mark# 0()) (mark# leq(X1, X2) -> active# leq(mark X1, mark X2), active# p s X -> mark# X) (mark# leq(X1, X2) -> active# leq(mark X1, mark X2), active# leq(0(), Y) -> mark# true()) (mark# leq(X1, X2) -> active# leq(mark X1, mark X2), active# leq(s X, 0()) -> mark# false()) (mark# leq(X1, X2) -> active# leq(mark X1, mark X2), active# leq(s X, s Y) -> mark# leq(X, Y)) (mark# leq(X1, X2) -> active# leq(mark X1, mark X2), active# leq(s X, s Y) -> leq#(X, Y)) (mark# leq(X1, X2) -> active# leq(mark X1, mark X2), active# if(true(), X, Y) -> mark# X) (mark# leq(X1, X2) -> active# leq(mark X1, mark X2), active# if(false(), X, Y) -> mark# Y) (mark# leq(X1, X2) -> active# leq(mark X1, mark X2), active# diff(X, Y) -> mark# if(leq(X, Y), 0(), s diff(p X, Y))) (mark# leq(X1, X2) -> active# leq(mark X1, mark X2), active# diff(X, Y) -> p# X) (mark# leq(X1, X2) -> active# leq(mark X1, mark X2), active# diff(X, Y) -> s# diff(p X, Y)) (mark# leq(X1, X2) -> active# leq(mark X1, mark X2), active# diff(X, Y) -> leq#(X, Y)) (mark# leq(X1, X2) -> active# leq(mark X1, mark X2), active# diff(X, Y) -> if#(leq(X, Y), 0(), s diff(p X, Y))) (mark# leq(X1, X2) -> active# leq(mark X1, mark X2), active# diff(X, Y) -> diff#(p X, Y)) (diff#(active X1, X2) -> diff#(X1, X2), diff#(X1, mark X2) -> diff#(X1, X2)) (diff#(active X1, X2) -> diff#(X1, X2), diff#(X1, active X2) -> diff#(X1, X2)) (diff#(active X1, X2) -> diff#(X1, X2), diff#(mark X1, X2) -> diff#(X1, X2)) (diff#(active X1, X2) -> diff#(X1, X2), diff#(active X1, X2) -> diff#(X1, X2)) (diff#(X1, active X2) -> diff#(X1, X2), diff#(X1, mark X2) -> diff#(X1, X2)) (diff#(X1, active X2) -> diff#(X1, X2), diff#(X1, active X2) -> diff#(X1, X2)) (diff#(X1, active X2) -> diff#(X1, X2), diff#(mark X1, X2) -> diff#(X1, X2)) (diff#(X1, active X2) -> diff#(X1, X2), diff#(active X1, X2) -> diff#(X1, X2)) (leq#(active X1, X2) -> leq#(X1, X2), leq#(X1, mark X2) -> leq#(X1, X2)) (leq#(active X1, X2) -> leq#(X1, X2), leq#(X1, active X2) -> leq#(X1, X2)) (leq#(active X1, X2) -> leq#(X1, X2), leq#(mark X1, X2) -> leq#(X1, X2)) (leq#(active X1, X2) -> leq#(X1, X2), leq#(active X1, X2) -> leq#(X1, X2)) (leq#(X1, active X2) -> leq#(X1, X2), leq#(X1, mark X2) -> leq#(X1, X2)) (leq#(X1, active X2) -> leq#(X1, X2), leq#(X1, active X2) -> leq#(X1, X2)) (leq#(X1, active X2) -> leq#(X1, X2), leq#(mark X1, X2) -> leq#(X1, X2)) (leq#(X1, active X2) -> leq#(X1, X2), leq#(active X1, X2) -> leq#(X1, X2)) (if#(active X1, X2, X3) -> if#(X1, X2, X3), if#(X1, X2, mark X3) -> if#(X1, X2, X3)) (if#(active X1, X2, X3) -> if#(X1, X2, X3), if#(X1, X2, active X3) -> if#(X1, X2, X3)) (if#(active X1, X2, X3) -> if#(X1, X2, X3), if#(X1, mark X2, X3) -> if#(X1, X2, X3)) (if#(active X1, X2, X3) -> if#(X1, X2, X3), if#(X1, active X2, X3) -> if#(X1, X2, X3)) (if#(active X1, X2, X3) -> if#(X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3)) (if#(active X1, X2, X3) -> if#(X1, X2, X3), if#(active X1, X2, X3) -> if#(X1, X2, X3)) (if#(X1, active X2, X3) -> if#(X1, X2, X3), if#(X1, X2, mark X3) -> if#(X1, X2, X3)) (if#(X1, active X2, X3) -> if#(X1, X2, X3), if#(X1, X2, active X3) -> if#(X1, X2, X3)) (if#(X1, active X2, X3) -> if#(X1, X2, X3), if#(X1, mark X2, X3) -> if#(X1, X2, X3)) (if#(X1, active X2, X3) -> if#(X1, X2, X3), if#(X1, active X2, X3) -> if#(X1, X2, X3)) (if#(X1, active X2, X3) -> if#(X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3)) (if#(X1, active X2, X3) -> if#(X1, X2, X3), if#(active X1, X2, X3) -> if#(X1, X2, X3)) (if#(X1, X2, active X3) -> if#(X1, X2, X3), if#(X1, X2, mark X3) -> if#(X1, X2, X3)) (if#(X1, X2, active X3) -> if#(X1, X2, X3), if#(X1, X2, active X3) -> if#(X1, X2, X3)) (if#(X1, X2, active X3) -> if#(X1, X2, X3), if#(X1, mark X2, X3) -> if#(X1, X2, X3)) (if#(X1, X2, active X3) -> if#(X1, X2, X3), if#(X1, active X2, X3) -> if#(X1, X2, X3)) (if#(X1, X2, active X3) -> if#(X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3)) (if#(X1, X2, active X3) -> if#(X1, X2, X3), if#(active X1, X2, X3) -> if#(X1, X2, X3)) (mark# if(X1, X2, X3) -> if#(mark X1, X2, X3), if#(X1, X2, mark X3) -> if#(X1, X2, X3)) (mark# if(X1, X2, X3) -> if#(mark X1, X2, X3), if#(X1, X2, active X3) -> if#(X1, X2, X3)) (mark# if(X1, X2, X3) -> if#(mark X1, X2, X3), if#(X1, mark X2, X3) -> if#(X1, X2, X3)) (mark# if(X1, X2, X3) -> if#(mark X1, X2, X3), if#(X1, active X2, X3) -> if#(X1, X2, X3)) (mark# if(X1, X2, X3) -> if#(mark X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3)) (mark# if(X1, X2, X3) -> if#(mark X1, X2, X3), if#(active X1, X2, X3) -> if#(X1, X2, X3)) (active# leq(s X, s Y) -> leq#(X, Y), leq#(X1, mark X2) -> leq#(X1, X2)) (active# leq(s X, s Y) -> leq#(X, Y), leq#(X1, active X2) -> leq#(X1, X2)) (active# leq(s X, s Y) -> leq#(X, Y), leq#(mark X1, X2) -> leq#(X1, X2)) (active# leq(s X, s Y) -> leq#(X, Y), leq#(active X1, X2) -> leq#(X1, X2)) (mark# if(X1, X2, X3) -> mark# X1, mark# 0() -> active# 0()) (mark# if(X1, X2, X3) -> mark# X1, mark# p X -> mark# X) (mark# if(X1, X2, X3) -> mark# X1, mark# p X -> active# p mark X) (mark# if(X1, X2, X3) -> mark# X1, mark# p X -> p# mark X) (mark# if(X1, X2, X3) -> mark# X1, mark# s X -> mark# X) (mark# if(X1, X2, X3) -> mark# X1, mark# s X -> active# s mark X) (mark# if(X1, X2, X3) -> mark# X1, mark# s X -> s# mark X) (mark# if(X1, X2, X3) -> mark# X1, mark# true() -> active# true()) (mark# if(X1, X2, X3) -> mark# X1, mark# leq(X1, X2) -> mark# X1) (mark# if(X1, X2, X3) -> mark# X1, mark# leq(X1, X2) -> mark# X2) (mark# if(X1, X2, X3) -> mark# X1, mark# leq(X1, X2) -> active# leq(mark X1, mark X2)) (mark# if(X1, X2, X3) -> mark# X1, mark# leq(X1, X2) -> leq#(mark X1, mark X2)) (mark# if(X1, X2, X3) -> mark# X1, mark# false() -> active# false()) (mark# if(X1, X2, X3) -> mark# X1, mark# if(X1, X2, X3) -> mark# X1) (mark# if(X1, X2, X3) -> mark# X1, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (mark# if(X1, X2, X3) -> mark# X1, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (mark# if(X1, X2, X3) -> mark# X1, mark# diff(X1, X2) -> mark# X1) (mark# if(X1, X2, X3) -> mark# X1, mark# diff(X1, X2) -> mark# X2) (mark# if(X1, X2, X3) -> mark# X1, mark# diff(X1, X2) -> active# diff(mark X1, mark X2)) (mark# if(X1, X2, X3) -> mark# X1, mark# diff(X1, X2) -> diff#(mark X1, mark X2)) (active# diff(X, Y) -> diff#(p X, Y), diff#(X1, mark X2) -> diff#(X1, X2)) (active# diff(X, Y) -> diff#(p X, Y), diff#(X1, active X2) -> diff#(X1, X2)) (active# diff(X, Y) -> diff#(p X, Y), diff#(mark X1, X2) -> diff#(X1, X2)) (active# diff(X, Y) -> diff#(p X, Y), diff#(active X1, X2) -> diff#(X1, X2)) (mark# diff(X1, X2) -> mark# X2, mark# 0() -> active# 0()) (mark# diff(X1, X2) -> mark# X2, mark# p X -> mark# X) (mark# diff(X1, X2) -> mark# X2, mark# p X -> active# p mark X) (mark# diff(X1, X2) -> mark# X2, mark# p X -> p# mark X) (mark# diff(X1, X2) -> mark# X2, mark# s X -> mark# X) (mark# diff(X1, X2) -> mark# X2, mark# s X -> active# s mark X) (mark# diff(X1, X2) -> mark# X2, mark# s X -> s# mark X) (mark# diff(X1, X2) -> mark# X2, mark# true() -> active# true()) (mark# diff(X1, X2) -> mark# X2, mark# leq(X1, X2) -> mark# X1) (mark# diff(X1, X2) -> mark# X2, mark# leq(X1, X2) -> mark# X2) (mark# diff(X1, X2) -> mark# X2, mark# leq(X1, X2) -> active# leq(mark X1, mark X2)) (mark# diff(X1, X2) -> mark# X2, mark# leq(X1, X2) -> leq#(mark X1, mark X2)) (mark# diff(X1, X2) -> mark# X2, mark# false() -> active# false()) (mark# diff(X1, X2) -> mark# X2, mark# if(X1, X2, X3) -> mark# X1) (mark# diff(X1, X2) -> mark# X2, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (mark# diff(X1, X2) -> mark# X2, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (mark# diff(X1, X2) -> mark# X2, mark# diff(X1, X2) -> mark# X1) (mark# diff(X1, X2) -> mark# X2, mark# diff(X1, X2) -> mark# X2) (mark# diff(X1, X2) -> mark# X2, mark# diff(X1, X2) -> active# diff(mark X1, mark X2)) (mark# diff(X1, X2) -> mark# X2, mark# diff(X1, X2) -> diff#(mark X1, mark X2)) (mark# diff(X1, X2) -> diff#(mark X1, mark X2), diff#(X1, mark X2) -> diff#(X1, X2)) (mark# diff(X1, X2) -> diff#(mark X1, mark X2), diff#(X1, active X2) -> diff#(X1, X2)) (mark# diff(X1, X2) -> diff#(mark X1, mark X2), diff#(mark X1, X2) -> diff#(X1, X2)) (mark# diff(X1, X2) -> diff#(mark X1, mark X2), diff#(active X1, X2) -> diff#(X1, X2)) (active# diff(X, Y) -> s# diff(p X, Y), s# mark X -> s# X) (active# diff(X, Y) -> s# diff(p X, Y), s# active X -> s# X) (active# diff(X, Y) -> mark# if(leq(X, Y), 0(), s diff(p X, Y)), mark# 0() -> active# 0()) (active# diff(X, Y) -> mark# if(leq(X, Y), 0(), s diff(p X, Y)), mark# p X -> mark# X) (active# diff(X, Y) -> mark# if(leq(X, Y), 0(), s diff(p X, Y)), mark# p X -> active# p mark X) (active# diff(X, Y) -> mark# if(leq(X, Y), 0(), s diff(p X, Y)), mark# p X -> p# mark X) (active# diff(X, Y) -> mark# if(leq(X, Y), 0(), s diff(p X, Y)), mark# s X -> mark# X) (active# diff(X, Y) -> mark# if(leq(X, Y), 0(), s diff(p X, Y)), mark# s X -> active# s mark X) (active# diff(X, Y) -> mark# if(leq(X, Y), 0(), s diff(p X, Y)), mark# s X -> s# mark X) (active# diff(X, Y) -> mark# if(leq(X, Y), 0(), s diff(p X, Y)), mark# true() -> active# true()) (active# diff(X, Y) -> mark# if(leq(X, Y), 0(), s diff(p X, Y)), mark# leq(X1, X2) -> mark# X1) (active# diff(X, Y) -> mark# if(leq(X, Y), 0(), s diff(p X, Y)), mark# leq(X1, X2) -> mark# X2) (active# diff(X, Y) -> mark# if(leq(X, Y), 0(), s diff(p X, Y)), mark# leq(X1, X2) -> active# leq(mark X1, mark X2)) (active# diff(X, Y) -> mark# if(leq(X, Y), 0(), s diff(p X, Y)), mark# leq(X1, X2) -> leq#(mark X1, mark X2)) (active# diff(X, Y) -> mark# if(leq(X, Y), 0(), s diff(p X, Y)), mark# false() -> active# false()) (active# diff(X, Y) -> mark# if(leq(X, Y), 0(), s diff(p X, Y)), mark# if(X1, X2, X3) -> mark# X1) (active# diff(X, Y) -> mark# if(leq(X, Y), 0(), s diff(p X, Y)), mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (active# diff(X, Y) -> mark# if(leq(X, Y), 0(), s diff(p X, Y)), mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (active# diff(X, Y) -> mark# if(leq(X, Y), 0(), s diff(p X, Y)), mark# diff(X1, X2) -> mark# X1) (active# diff(X, Y) -> mark# if(leq(X, Y), 0(), s diff(p X, Y)), mark# diff(X1, X2) -> mark# X2) (active# diff(X, Y) -> mark# if(leq(X, Y), 0(), s diff(p X, Y)), mark# diff(X1, X2) -> active# diff(mark X1, mark X2)) (active# diff(X, Y) -> mark# if(leq(X, Y), 0(), s diff(p X, Y)), mark# diff(X1, X2) -> diff#(mark X1, mark X2)) (mark# p X -> active# p mark X, active# p 0() -> mark# 0()) (mark# p X -> active# p mark X, active# p s X -> mark# X) (mark# p X -> active# p mark X, active# leq(0(), Y) -> mark# true()) (mark# p X -> active# p mark X, active# leq(s X, 0()) -> mark# false()) (mark# p X -> active# p mark X, active# leq(s X, s Y) -> mark# leq(X, Y)) (mark# p X -> active# p mark X, active# leq(s X, s Y) -> leq#(X, Y)) (mark# p X -> active# p mark X, active# if(true(), X, Y) -> mark# X) (mark# p X -> active# p mark X, active# if(false(), X, Y) -> mark# Y) (mark# p X -> active# p mark X, active# diff(X, Y) -> mark# if(leq(X, Y), 0(), s diff(p X, Y))) (mark# p X -> active# p mark X, active# diff(X, Y) -> p# X) (mark# p X -> active# p mark X, active# diff(X, Y) -> s# diff(p X, Y)) (mark# p X -> active# p mark X, active# diff(X, Y) -> leq#(X, Y)) (mark# p X -> active# p mark X, active# diff(X, Y) -> if#(leq(X, Y), 0(), s diff(p X, Y))) (mark# p X -> active# p mark X, active# diff(X, Y) -> diff#(p X, Y)) (s# active X -> s# X, s# mark X -> s# X) (s# active X -> s# X, s# active X -> s# X) (p# active X -> p# X, p# mark X -> p# X) (p# active X -> p# X, p# active X -> p# X) (active# diff(X, Y) -> p# X, p# mark X -> p# X) (active# diff(X, Y) -> p# X, p# active X -> p# X) (active# p s X -> mark# X, mark# 0() -> active# 0()) (active# p s X -> mark# X, mark# p X -> mark# X) (active# p s X -> mark# X, mark# p X -> active# p mark X) (active# p s X -> mark# X, mark# p X -> p# mark X) (active# p s X -> mark# X, mark# s X -> mark# X) (active# p s X -> mark# X, mark# s X -> active# s mark X) (active# p s X -> mark# X, mark# s X -> s# mark X) (active# p s X -> mark# X, mark# true() -> active# true()) (active# p s X -> mark# X, mark# leq(X1, X2) -> mark# X1) (active# p s X -> mark# X, mark# leq(X1, X2) -> mark# X2) (active# p s X -> mark# X, mark# leq(X1, X2) -> active# leq(mark X1, mark X2)) (active# p s X -> mark# X, mark# leq(X1, X2) -> leq#(mark X1, mark X2)) (active# p s X -> mark# X, mark# false() -> active# false()) (active# p s X -> mark# X, mark# if(X1, X2, X3) -> mark# X1) (active# p s X -> mark# X, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (active# p s X -> mark# X, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (active# p s X -> mark# X, mark# diff(X1, X2) -> mark# X1) (active# p s X -> mark# X, mark# diff(X1, X2) -> mark# X2) (active# p s X -> mark# X, mark# diff(X1, X2) -> active# diff(mark X1, mark X2)) (active# p s X -> mark# X, mark# diff(X1, X2) -> diff#(mark X1, mark X2)) (mark# p X -> mark# X, mark# 0() -> active# 0()) (mark# p X -> mark# X, mark# p X -> mark# X) (mark# p X -> mark# X, mark# p X -> active# p mark X) (mark# p X -> mark# X, mark# p X -> p# mark X) (mark# p X -> mark# X, mark# s X -> mark# X) (mark# p X -> mark# X, mark# s X -> active# s mark X) (mark# p X -> mark# X, mark# s X -> s# mark X) (mark# p X -> mark# X, mark# true() -> active# true()) (mark# p X -> mark# X, mark# leq(X1, X2) -> mark# X1) (mark# p X -> mark# X, mark# leq(X1, X2) -> mark# X2) (mark# p X -> mark# X, mark# leq(X1, X2) -> active# leq(mark X1, mark X2)) (mark# p X -> mark# X, mark# leq(X1, X2) -> leq#(mark X1, mark X2)) (mark# p X -> mark# X, mark# false() -> active# false()) (mark# p X -> mark# X, mark# if(X1, X2, X3) -> mark# X1) (mark# p X -> mark# X, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (mark# p X -> mark# X, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (mark# p X -> mark# X, mark# diff(X1, X2) -> mark# X1) (mark# p X -> mark# X, mark# diff(X1, X2) -> mark# X2) (mark# p X -> mark# X, mark# diff(X1, X2) -> active# diff(mark X1, mark X2)) (mark# p X -> mark# X, mark# diff(X1, X2) -> diff#(mark X1, mark X2)) (active# leq(0(), Y) -> mark# true(), mark# 0() -> active# 0()) (active# leq(0(), Y) -> mark# true(), mark# p X -> mark# X) (active# leq(0(), Y) -> mark# true(), mark# p X -> active# p mark X) (active# leq(0(), Y) -> mark# true(), mark# p X -> p# mark X) (active# leq(0(), Y) -> mark# true(), mark# s X -> mark# X) (active# leq(0(), Y) -> mark# true(), mark# s X -> active# s mark X) (active# leq(0(), Y) -> mark# true(), mark# s X -> s# mark X) (active# leq(0(), Y) -> mark# true(), mark# true() -> active# true()) (active# leq(0(), Y) -> mark# true(), mark# leq(X1, X2) -> mark# X1) (active# leq(0(), Y) -> mark# true(), mark# leq(X1, X2) -> mark# X2) (active# leq(0(), Y) -> mark# true(), mark# leq(X1, X2) -> active# leq(mark X1, mark X2)) (active# leq(0(), Y) -> mark# true(), mark# leq(X1, X2) -> leq#(mark X1, mark X2)) (active# leq(0(), Y) -> mark# true(), mark# false() -> active# false()) (active# leq(0(), Y) -> mark# true(), mark# if(X1, X2, X3) -> mark# X1) (active# leq(0(), Y) -> mark# true(), mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (active# leq(0(), Y) -> mark# true(), mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (active# leq(0(), Y) -> mark# true(), mark# diff(X1, X2) -> mark# X1) (active# leq(0(), Y) -> mark# true(), mark# diff(X1, X2) -> mark# X2) (active# leq(0(), Y) -> mark# true(), mark# diff(X1, X2) -> active# diff(mark X1, mark X2)) (active# leq(0(), Y) -> mark# true(), mark# diff(X1, X2) -> diff#(mark X1, mark X2)) (mark# false() -> active# false(), active# p 0() -> mark# 0()) (mark# false() -> active# false(), active# p s X -> mark# X) (mark# false() -> active# false(), active# leq(0(), Y) -> mark# true()) (mark# false() -> active# false(), active# leq(s X, 0()) -> mark# false()) (mark# false() -> active# false(), active# leq(s X, s Y) -> mark# leq(X, Y)) (mark# false() -> active# false(), active# leq(s X, s Y) -> leq#(X, Y)) (mark# false() -> active# false(), active# if(true(), X, Y) -> mark# X) (mark# false() -> active# false(), active# if(false(), X, Y) -> mark# Y) (mark# false() -> active# false(), active# diff(X, Y) -> mark# if(leq(X, Y), 0(), s diff(p X, Y))) (mark# false() -> active# false(), active# diff(X, Y) -> p# X) (mark# false() -> active# false(), active# diff(X, Y) -> s# diff(p X, Y)) (mark# false() -> active# false(), active# diff(X, Y) -> leq#(X, Y)) (mark# false() -> active# false(), active# diff(X, Y) -> if#(leq(X, Y), 0(), s diff(p X, Y))) (mark# false() -> active# false(), active# diff(X, Y) -> diff#(p X, Y)) (mark# 0() -> active# 0(), active# p 0() -> mark# 0()) (mark# 0() -> active# 0(), active# p s X -> mark# X) (mark# 0() -> active# 0(), active# leq(0(), Y) -> mark# true()) (mark# 0() -> active# 0(), active# leq(s X, 0()) -> mark# false()) (mark# 0() -> active# 0(), active# leq(s X, s Y) -> mark# leq(X, Y)) (mark# 0() -> active# 0(), active# leq(s X, s Y) -> leq#(X, Y)) (mark# 0() -> active# 0(), active# if(true(), X, Y) -> mark# X) (mark# 0() -> active# 0(), active# if(false(), X, Y) -> mark# Y) (mark# 0() -> active# 0(), active# diff(X, Y) -> mark# if(leq(X, Y), 0(), s diff(p X, Y))) (mark# 0() -> active# 0(), active# diff(X, Y) -> p# X) (mark# 0() -> active# 0(), active# diff(X, Y) -> s# diff(p X, Y)) (mark# 0() -> active# 0(), active# diff(X, Y) -> leq#(X, Y)) (mark# 0() -> active# 0(), active# diff(X, Y) -> if#(leq(X, Y), 0(), s diff(p X, Y))) (mark# 0() -> active# 0(), active# diff(X, Y) -> diff#(p X, Y)) } STATUS: arrows: 0.804734 SCCS (6): Scc: { mark# 0() -> active# 0(), mark# p X -> mark# X, mark# p X -> active# p mark X, mark# s X -> mark# X, mark# s X -> active# s mark X, mark# true() -> active# true(), mark# leq(X1, X2) -> mark# X1, mark# leq(X1, X2) -> mark# X2, mark# leq(X1, X2) -> active# leq(mark X1, mark X2), mark# false() -> active# false(), mark# if(X1, X2, X3) -> mark# X1, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), mark# diff(X1, X2) -> mark# X1, mark# diff(X1, X2) -> mark# X2, mark# diff(X1, X2) -> active# diff(mark X1, mark X2), active# p 0() -> mark# 0(), active# p s X -> mark# X, active# leq(0(), Y) -> mark# true(), active# leq(s X, 0()) -> mark# false(), active# leq(s X, s Y) -> mark# leq(X, Y), active# if(true(), X, Y) -> mark# X, active# if(false(), X, Y) -> mark# Y, active# diff(X, Y) -> mark# if(leq(X, Y), 0(), s diff(p X, Y))} Scc: { diff#(X1, mark X2) -> diff#(X1, X2), diff#(X1, active X2) -> diff#(X1, X2), diff#(mark X1, X2) -> diff#(X1, X2), diff#(active X1, X2) -> diff#(X1, X2)} Scc: { if#(X1, X2, mark X3) -> if#(X1, X2, X3), if#(X1, X2, active X3) -> if#(X1, X2, X3), if#(X1, mark X2, X3) -> if#(X1, X2, X3), if#(X1, active X2, X3) -> if#(X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3), if#(active X1, X2, X3) -> if#(X1, X2, X3)} Scc: { leq#(X1, mark X2) -> leq#(X1, X2), leq#(X1, active X2) -> leq#(X1, X2), leq#(mark X1, X2) -> leq#(X1, X2), leq#(active X1, X2) -> leq#(X1, X2)} Scc: { s# mark X -> s# X, s# active X -> s# X} Scc: { p# mark X -> p# X, p# active X -> p# X} SCC (23): Strict: { mark# 0() -> active# 0(), mark# p X -> mark# X, mark# p X -> active# p mark X, mark# s X -> mark# X, mark# s X -> active# s mark X, mark# true() -> active# true(), mark# leq(X1, X2) -> mark# X1, mark# leq(X1, X2) -> mark# X2, mark# leq(X1, X2) -> active# leq(mark X1, mark X2), mark# false() -> active# false(), mark# if(X1, X2, X3) -> mark# X1, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), mark# diff(X1, X2) -> mark# X1, mark# diff(X1, X2) -> mark# X2, mark# diff(X1, X2) -> active# diff(mark X1, mark X2), active# p 0() -> mark# 0(), active# p s X -> mark# X, active# leq(0(), Y) -> mark# true(), active# leq(s X, 0()) -> mark# false(), active# leq(s X, s Y) -> mark# leq(X, Y), active# if(true(), X, Y) -> mark# X, active# if(false(), X, Y) -> mark# Y, active# diff(X, Y) -> mark# if(leq(X, Y), 0(), s diff(p X, Y))} Weak: { mark 0() -> active 0(), mark p X -> active p mark X, mark s X -> active s mark X, mark true() -> active true(), mark leq(X1, X2) -> active leq(mark X1, mark X2), mark false() -> active false(), mark if(X1, X2, X3) -> active if(mark X1, X2, X3), mark diff(X1, X2) -> active diff(mark X1, mark X2), active p 0() -> mark 0(), active p s X -> mark X, active leq(0(), Y) -> mark true(), active leq(s X, 0()) -> mark false(), active leq(s X, s Y) -> mark leq(X, Y), active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active diff(X, Y) -> mark if(leq(X, Y), 0(), s diff(p X, Y)), p mark X -> p X, p active X -> p X, s mark X -> s X, s active X -> s X, leq(X1, mark X2) -> leq(X1, X2), leq(X1, active X2) -> leq(X1, X2), leq(mark X1, X2) -> leq(X1, X2), leq(active X1, X2) -> leq(X1, X2), if(X1, X2, mark X3) -> if(X1, X2, X3), if(X1, X2, active X3) -> if(X1, X2, X3), if(X1, mark X2, X3) -> if(X1, X2, X3), if(X1, active X2, X3) -> if(X1, X2, X3), if(mark X1, X2, X3) -> if(X1, X2, X3), if(active X1, X2, X3) -> if(X1, X2, X3), diff(X1, mark X2) -> diff(X1, X2), diff(X1, active X2) -> diff(X1, X2), diff(mark X1, X2) -> diff(X1, X2), diff(active X1, X2) -> diff(X1, X2)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2) = 1, [leq](x0, x1) = 1, [diff](x0, x1) = 1, [mark](x0) = x0 + 1, [active](x0) = 0, [p](x0) = 1, [s](x0) = 1, [0] = 0, [true] = 1, [false] = 1, [mark#](x0) = 1, [active#](x0) = x0 Strict: active# diff(X, Y) -> mark# if(leq(X, Y), 0(), s diff(p X, Y)) 1 + 0X + 0Y >= 1 + 0X + 0Y active# if(false(), X, Y) -> mark# Y 1 + 0X + 0Y >= 1 + 0Y active# if(true(), X, Y) -> mark# X 1 + 0X + 0Y >= 1 + 0X active# leq(s X, s Y) -> mark# leq(X, Y) 1 + 0X + 0Y >= 1 + 0X + 0Y active# leq(s X, 0()) -> mark# false() 1 + 0X >= 1 active# leq(0(), Y) -> mark# true() 1 + 0Y >= 1 active# p s X -> mark# X 1 + 0X >= 1 + 0X active# p 0() -> mark# 0() 1 >= 1 mark# diff(X1, X2) -> active# diff(mark X1, mark X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 mark# diff(X1, X2) -> mark# X2 1 + 0X1 + 0X2 >= 1 + 0X2 mark# diff(X1, X2) -> mark# X1 1 + 0X1 + 0X2 >= 1 + 0X1 mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 mark# if(X1, X2, X3) -> mark# X1 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 mark# false() -> active# false() 1 >= 1 mark# leq(X1, X2) -> active# leq(mark X1, mark X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 mark# leq(X1, X2) -> mark# X2 1 + 0X1 + 0X2 >= 1 + 0X2 mark# leq(X1, X2) -> mark# X1 1 + 0X1 + 0X2 >= 1 + 0X1 mark# true() -> active# true() 1 >= 1 mark# s X -> active# s mark X 1 + 0X >= 1 + 0X mark# s X -> mark# X 1 + 0X >= 1 + 0X mark# p X -> active# p mark X 1 + 0X >= 1 + 0X mark# p X -> mark# X 1 + 0X >= 1 + 0X mark# 0() -> active# 0() 1 >= 0 Weak: diff(active X1, X2) -> diff(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 diff(mark X1, X2) -> diff(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 diff(X1, active X2) -> diff(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 diff(X1, mark X2) -> diff(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 if(active X1, X2, X3) -> if(X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 if(mark X1, X2, X3) -> if(X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 if(X1, active X2, X3) -> if(X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 if(X1, mark X2, X3) -> if(X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 if(X1, X2, active X3) -> if(X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 if(X1, X2, mark X3) -> if(X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 leq(active X1, X2) -> leq(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 leq(mark X1, X2) -> leq(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 leq(X1, active X2) -> leq(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 leq(X1, mark X2) -> leq(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 s active X -> s X 1 + 0X >= 1 + 0X s mark X -> s X 1 + 0X >= 1 + 0X p active X -> p X 1 + 0X >= 1 + 0X p mark X -> p X 1 + 0X >= 1 + 0X active diff(X, Y) -> mark if(leq(X, Y), 0(), s diff(p X, Y)) 0 + 0X + 0Y >= 2 + 0X + 0Y 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 leq(s X, s Y) -> mark leq(X, Y) 0 + 0X + 0Y >= 2 + 0X + 0Y active leq(s X, 0()) -> mark false() 0 + 0X >= 2 active leq(0(), Y) -> mark true() 0 + 0Y >= 2 active p s X -> mark X 0 + 0X >= 1 + 1X active p 0() -> mark 0() 0 >= 1 mark diff(X1, X2) -> active diff(mark X1, mark X2) 2 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 mark if(X1, X2, X3) -> active if(mark X1, X2, X3) 2 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 mark false() -> active false() 2 >= 0 mark leq(X1, X2) -> active leq(mark X1, mark X2) 2 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 mark true() -> active true() 2 >= 0 mark s X -> active s mark X 2 + 0X >= 0 + 0X mark p X -> active p mark X 2 + 0X >= 0 + 0X mark 0() -> active 0() 1 >= 0 SCCS (1): Scc: { mark# p X -> mark# X, mark# p X -> active# p mark X, mark# s X -> mark# X, mark# s X -> active# s mark X, mark# true() -> active# true(), mark# leq(X1, X2) -> mark# X1, mark# leq(X1, X2) -> mark# X2, mark# leq(X1, X2) -> active# leq(mark X1, mark X2), mark# false() -> active# false(), mark# if(X1, X2, X3) -> mark# X1, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), mark# diff(X1, X2) -> mark# X1, mark# diff(X1, X2) -> mark# X2, mark# diff(X1, X2) -> active# diff(mark X1, mark X2), active# p 0() -> mark# 0(), active# p s X -> mark# X, active# leq(0(), Y) -> mark# true(), active# leq(s X, 0()) -> mark# false(), active# leq(s X, s Y) -> mark# leq(X, Y), active# if(true(), X, Y) -> mark# X, active# if(false(), X, Y) -> mark# Y, active# diff(X, Y) -> mark# if(leq(X, Y), 0(), s diff(p X, Y))} SCC (22): Strict: { mark# p X -> mark# X, mark# p X -> active# p mark X, mark# s X -> mark# X, mark# s X -> active# s mark X, mark# true() -> active# true(), mark# leq(X1, X2) -> mark# X1, mark# leq(X1, X2) -> mark# X2, mark# leq(X1, X2) -> active# leq(mark X1, mark X2), mark# false() -> active# false(), mark# if(X1, X2, X3) -> mark# X1, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), mark# diff(X1, X2) -> mark# X1, mark# diff(X1, X2) -> mark# X2, mark# diff(X1, X2) -> active# diff(mark X1, mark X2), active# p 0() -> mark# 0(), active# p s X -> mark# X, active# leq(0(), Y) -> mark# true(), active# leq(s X, 0()) -> mark# false(), active# leq(s X, s Y) -> mark# leq(X, Y), active# if(true(), X, Y) -> mark# X, active# if(false(), X, Y) -> mark# Y, active# diff(X, Y) -> mark# if(leq(X, Y), 0(), s diff(p X, Y))} Weak: { mark 0() -> active 0(), mark p X -> active p mark X, mark s X -> active s mark X, mark true() -> active true(), mark leq(X1, X2) -> active leq(mark X1, mark X2), mark false() -> active false(), mark if(X1, X2, X3) -> active if(mark X1, X2, X3), mark diff(X1, X2) -> active diff(mark X1, mark X2), active p 0() -> mark 0(), active p s X -> mark X, active leq(0(), Y) -> mark true(), active leq(s X, 0()) -> mark false(), active leq(s X, s Y) -> mark leq(X, Y), active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active diff(X, Y) -> mark if(leq(X, Y), 0(), s diff(p X, Y)), p mark X -> p X, p active X -> p X, s mark X -> s X, s active X -> s X, leq(X1, mark X2) -> leq(X1, X2), leq(X1, active X2) -> leq(X1, X2), leq(mark X1, X2) -> leq(X1, X2), leq(active X1, X2) -> leq(X1, X2), if(X1, X2, mark X3) -> if(X1, X2, X3), if(X1, X2, active X3) -> if(X1, X2, X3), if(X1, mark X2, X3) -> if(X1, X2, X3), if(X1, active X2, X3) -> if(X1, X2, X3), if(mark X1, X2, X3) -> if(X1, X2, X3), if(active X1, X2, X3) -> if(X1, X2, X3), diff(X1, mark X2) -> diff(X1, X2), diff(X1, active X2) -> diff(X1, X2), diff(mark X1, X2) -> diff(X1, X2), diff(active X1, X2) -> diff(X1, X2)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2) = 1, [leq](x0, x1) = 1, [diff](x0, x1) = 1, [mark](x0) = x0 + 1, [active](x0) = 0, [p](x0) = 1, [s](x0) = 1, [0] = 0, [true] = 0, [false] = 1, [mark#](x0) = 1, [active#](x0) = x0 Strict: active# diff(X, Y) -> mark# if(leq(X, Y), 0(), s diff(p X, Y)) 1 + 0X + 0Y >= 1 + 0X + 0Y active# if(false(), X, Y) -> mark# Y 1 + 0X + 0Y >= 1 + 0Y active# if(true(), X, Y) -> mark# X 1 + 0X + 0Y >= 1 + 0X active# leq(s X, s Y) -> mark# leq(X, Y) 1 + 0X + 0Y >= 1 + 0X + 0Y active# leq(s X, 0()) -> mark# false() 1 + 0X >= 1 active# leq(0(), Y) -> mark# true() 1 + 0Y >= 1 active# p s X -> mark# X 1 + 0X >= 1 + 0X active# p 0() -> mark# 0() 1 >= 1 mark# diff(X1, X2) -> active# diff(mark X1, mark X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 mark# diff(X1, X2) -> mark# X2 1 + 0X1 + 0X2 >= 1 + 0X2 mark# diff(X1, X2) -> mark# X1 1 + 0X1 + 0X2 >= 1 + 0X1 mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 mark# if(X1, X2, X3) -> mark# X1 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 mark# false() -> active# false() 1 >= 1 mark# leq(X1, X2) -> active# leq(mark X1, mark X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 mark# leq(X1, X2) -> mark# X2 1 + 0X1 + 0X2 >= 1 + 0X2 mark# leq(X1, X2) -> mark# X1 1 + 0X1 + 0X2 >= 1 + 0X1 mark# true() -> active# true() 1 >= 0 mark# s X -> active# s mark X 1 + 0X >= 1 + 0X mark# s X -> mark# X 1 + 0X >= 1 + 0X mark# p X -> active# p mark X 1 + 0X >= 1 + 0X mark# p X -> mark# X 1 + 0X >= 1 + 0X Weak: diff(active X1, X2) -> diff(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 diff(mark X1, X2) -> diff(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 diff(X1, active X2) -> diff(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 diff(X1, mark X2) -> diff(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 if(active X1, X2, X3) -> if(X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 if(mark X1, X2, X3) -> if(X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 if(X1, active X2, X3) -> if(X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 if(X1, mark X2, X3) -> if(X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 if(X1, X2, active X3) -> if(X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 if(X1, X2, mark X3) -> if(X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 leq(active X1, X2) -> leq(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 leq(mark X1, X2) -> leq(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 leq(X1, active X2) -> leq(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 leq(X1, mark X2) -> leq(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 s active X -> s X 1 + 0X >= 1 + 0X s mark X -> s X 1 + 0X >= 1 + 0X p active X -> p X 1 + 0X >= 1 + 0X p mark X -> p X 1 + 0X >= 1 + 0X active diff(X, Y) -> mark if(leq(X, Y), 0(), s diff(p X, Y)) 0 + 0X + 0Y >= 2 + 0X + 0Y 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 leq(s X, s Y) -> mark leq(X, Y) 0 + 0X + 0Y >= 2 + 0X + 0Y active leq(s X, 0()) -> mark false() 0 + 0X >= 2 active leq(0(), Y) -> mark true() 0 + 0Y >= 1 active p s X -> mark X 0 + 0X >= 1 + 1X active p 0() -> mark 0() 0 >= 1 mark diff(X1, X2) -> active diff(mark X1, mark X2) 2 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 mark if(X1, X2, X3) -> active if(mark X1, X2, X3) 2 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 mark false() -> active false() 2 >= 0 mark leq(X1, X2) -> active leq(mark X1, mark X2) 2 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 mark true() -> active true() 1 >= 0 mark s X -> active s mark X 2 + 0X >= 0 + 0X mark p X -> active p mark X 2 + 0X >= 0 + 0X mark 0() -> active 0() 1 >= 0 SCCS (1): Scc: { mark# p X -> mark# X, mark# p X -> active# p mark X, mark# s X -> mark# X, mark# s X -> active# s mark X, mark# leq(X1, X2) -> mark# X1, mark# leq(X1, X2) -> mark# X2, mark# leq(X1, X2) -> active# leq(mark X1, mark X2), mark# false() -> active# false(), mark# if(X1, X2, X3) -> mark# X1, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), mark# diff(X1, X2) -> mark# X1, mark# diff(X1, X2) -> mark# X2, mark# diff(X1, X2) -> active# diff(mark X1, mark X2), active# p 0() -> mark# 0(), active# p s X -> mark# X, active# leq(0(), Y) -> mark# true(), active# leq(s X, 0()) -> mark# false(), active# leq(s X, s Y) -> mark# leq(X, Y), active# if(true(), X, Y) -> mark# X, active# if(false(), X, Y) -> mark# Y, active# diff(X, Y) -> mark# if(leq(X, Y), 0(), s diff(p X, Y))} SCC (21): Strict: { mark# p X -> mark# X, mark# p X -> active# p mark X, mark# s X -> mark# X, mark# s X -> active# s mark X, mark# leq(X1, X2) -> mark# X1, mark# leq(X1, X2) -> mark# X2, mark# leq(X1, X2) -> active# leq(mark X1, mark X2), mark# false() -> active# false(), mark# if(X1, X2, X3) -> mark# X1, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), mark# diff(X1, X2) -> mark# X1, mark# diff(X1, X2) -> mark# X2, mark# diff(X1, X2) -> active# diff(mark X1, mark X2), active# p 0() -> mark# 0(), active# p s X -> mark# X, active# leq(0(), Y) -> mark# true(), active# leq(s X, 0()) -> mark# false(), active# leq(s X, s Y) -> mark# leq(X, Y), active# if(true(), X, Y) -> mark# X, active# if(false(), X, Y) -> mark# Y, active# diff(X, Y) -> mark# if(leq(X, Y), 0(), s diff(p X, Y))} Weak: { mark 0() -> active 0(), mark p X -> active p mark X, mark s X -> active s mark X, mark true() -> active true(), mark leq(X1, X2) -> active leq(mark X1, mark X2), mark false() -> active false(), mark if(X1, X2, X3) -> active if(mark X1, X2, X3), mark diff(X1, X2) -> active diff(mark X1, mark X2), active p 0() -> mark 0(), active p s X -> mark X, active leq(0(), Y) -> mark true(), active leq(s X, 0()) -> mark false(), active leq(s X, s Y) -> mark leq(X, Y), active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active diff(X, Y) -> mark if(leq(X, Y), 0(), s diff(p X, Y)), p mark X -> p X, p active X -> p X, s mark X -> s X, s active X -> s X, leq(X1, mark X2) -> leq(X1, X2), leq(X1, active X2) -> leq(X1, X2), leq(mark X1, X2) -> leq(X1, X2), leq(active X1, X2) -> leq(X1, X2), if(X1, X2, mark X3) -> if(X1, X2, X3), if(X1, X2, active X3) -> if(X1, X2, X3), if(X1, mark X2, X3) -> if(X1, X2, X3), if(X1, active X2, X3) -> if(X1, X2, X3), if(mark X1, X2, X3) -> if(X1, X2, X3), if(active X1, X2, X3) -> if(X1, X2, X3), diff(X1, mark X2) -> diff(X1, X2), diff(X1, active X2) -> diff(X1, X2), diff(mark X1, X2) -> diff(X1, X2), diff(active X1, X2) -> diff(X1, X2)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2) = 1, [leq](x0, x1) = 1, [diff](x0, x1) = 1, [mark](x0) = x0 + 1, [active](x0) = 0, [p](x0) = 1, [s](x0) = 0, [0] = 0, [true] = 0, [false] = 1, [mark#](x0) = 1, [active#](x0) = x0 Strict: active# diff(X, Y) -> mark# if(leq(X, Y), 0(), s diff(p X, Y)) 1 + 0X + 0Y >= 1 + 0X + 0Y active# if(false(), X, Y) -> mark# Y 1 + 0X + 0Y >= 1 + 0Y active# if(true(), X, Y) -> mark# X 1 + 0X + 0Y >= 1 + 0X active# leq(s X, s Y) -> mark# leq(X, Y) 1 + 0X + 0Y >= 1 + 0X + 0Y active# leq(s X, 0()) -> mark# false() 1 + 0X >= 1 active# leq(0(), Y) -> mark# true() 1 + 0Y >= 1 active# p s X -> mark# X 1 + 0X >= 1 + 0X active# p 0() -> mark# 0() 1 >= 1 mark# diff(X1, X2) -> active# diff(mark X1, mark X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 mark# diff(X1, X2) -> mark# X2 1 + 0X1 + 0X2 >= 1 + 0X2 mark# diff(X1, X2) -> mark# X1 1 + 0X1 + 0X2 >= 1 + 0X1 mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 mark# if(X1, X2, X3) -> mark# X1 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 mark# false() -> active# false() 1 >= 1 mark# leq(X1, X2) -> active# leq(mark X1, mark X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 mark# leq(X1, X2) -> mark# X2 1 + 0X1 + 0X2 >= 1 + 0X2 mark# leq(X1, X2) -> mark# X1 1 + 0X1 + 0X2 >= 1 + 0X1 mark# s X -> active# s mark X 1 + 0X >= 0 + 0X mark# s X -> mark# X 1 + 0X >= 1 + 0X mark# p X -> active# p mark X 1 + 0X >= 1 + 0X mark# p X -> mark# X 1 + 0X >= 1 + 0X Weak: diff(active X1, X2) -> diff(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 diff(mark X1, X2) -> diff(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 diff(X1, active X2) -> diff(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 diff(X1, mark X2) -> diff(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 if(active X1, X2, X3) -> if(X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 if(mark X1, X2, X3) -> if(X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 if(X1, active X2, X3) -> if(X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 if(X1, mark X2, X3) -> if(X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 if(X1, X2, active X3) -> if(X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 if(X1, X2, mark X3) -> if(X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 leq(active X1, X2) -> leq(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 leq(mark X1, X2) -> leq(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 leq(X1, active X2) -> leq(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 leq(X1, mark X2) -> leq(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 s active X -> s X 0 + 0X >= 0 + 0X s mark X -> s X 0 + 0X >= 0 + 0X p active X -> p X 1 + 0X >= 1 + 0X p mark X -> p X 1 + 0X >= 1 + 0X active diff(X, Y) -> mark if(leq(X, Y), 0(), s diff(p X, Y)) 0 + 0X + 0Y >= 2 + 0X + 0Y 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 leq(s X, s Y) -> mark leq(X, Y) 0 + 0X + 0Y >= 2 + 0X + 0Y active leq(s X, 0()) -> mark false() 0 + 0X >= 2 active leq(0(), Y) -> mark true() 0 + 0Y >= 1 active p s X -> mark X 0 + 0X >= 1 + 1X active p 0() -> mark 0() 0 >= 1 mark diff(X1, X2) -> active diff(mark X1, mark X2) 2 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 mark if(X1, X2, X3) -> active if(mark X1, X2, X3) 2 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 mark false() -> active false() 2 >= 0 mark leq(X1, X2) -> active leq(mark X1, mark X2) 2 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 mark true() -> active true() 1 >= 0 mark s X -> active s mark X 1 + 0X >= 0 + 0X mark p X -> active p mark X 2 + 0X >= 0 + 0X mark 0() -> active 0() 1 >= 0 SCCS (1): Scc: { mark# p X -> mark# X, mark# p X -> active# p mark X, mark# s X -> mark# X, mark# leq(X1, X2) -> mark# X1, mark# leq(X1, X2) -> mark# X2, mark# leq(X1, X2) -> active# leq(mark X1, mark X2), mark# false() -> active# false(), mark# if(X1, X2, X3) -> mark# X1, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), mark# diff(X1, X2) -> mark# X1, mark# diff(X1, X2) -> mark# X2, mark# diff(X1, X2) -> active# diff(mark X1, mark X2), active# p 0() -> mark# 0(), active# p s X -> mark# X, active# leq(0(), Y) -> mark# true(), active# leq(s X, 0()) -> mark# false(), active# leq(s X, s Y) -> mark# leq(X, Y), active# if(true(), X, Y) -> mark# X, active# if(false(), X, Y) -> mark# Y, active# diff(X, Y) -> mark# if(leq(X, Y), 0(), s diff(p X, Y))} SCC (20): Strict: { mark# p X -> mark# X, mark# p X -> active# p mark X, mark# s X -> mark# X, mark# leq(X1, X2) -> mark# X1, mark# leq(X1, X2) -> mark# X2, mark# leq(X1, X2) -> active# leq(mark X1, mark X2), mark# false() -> active# false(), mark# if(X1, X2, X3) -> mark# X1, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), mark# diff(X1, X2) -> mark# X1, mark# diff(X1, X2) -> mark# X2, mark# diff(X1, X2) -> active# diff(mark X1, mark X2), active# p 0() -> mark# 0(), active# p s X -> mark# X, active# leq(0(), Y) -> mark# true(), active# leq(s X, 0()) -> mark# false(), active# leq(s X, s Y) -> mark# leq(X, Y), active# if(true(), X, Y) -> mark# X, active# if(false(), X, Y) -> mark# Y, active# diff(X, Y) -> mark# if(leq(X, Y), 0(), s diff(p X, Y))} Weak: { mark 0() -> active 0(), mark p X -> active p mark X, mark s X -> active s mark X, mark true() -> active true(), mark leq(X1, X2) -> active leq(mark X1, mark X2), mark false() -> active false(), mark if(X1, X2, X3) -> active if(mark X1, X2, X3), mark diff(X1, X2) -> active diff(mark X1, mark X2), active p 0() -> mark 0(), active p s X -> mark X, active leq(0(), Y) -> mark true(), active leq(s X, 0()) -> mark false(), active leq(s X, s Y) -> mark leq(X, Y), active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active diff(X, Y) -> mark if(leq(X, Y), 0(), s diff(p X, Y)), p mark X -> p X, p active X -> p X, s mark X -> s X, s active X -> s X, leq(X1, mark X2) -> leq(X1, X2), leq(X1, active X2) -> leq(X1, X2), leq(mark X1, X2) -> leq(X1, X2), leq(active X1, X2) -> leq(X1, X2), if(X1, X2, mark X3) -> if(X1, X2, X3), if(X1, X2, active X3) -> if(X1, X2, X3), if(X1, mark X2, X3) -> if(X1, X2, X3), if(X1, active X2, X3) -> if(X1, X2, X3), if(mark X1, X2, X3) -> if(X1, X2, X3), if(active X1, X2, X3) -> if(X1, X2, X3), diff(X1, mark X2) -> diff(X1, X2), diff(X1, active X2) -> diff(X1, X2), diff(mark X1, X2) -> diff(X1, X2), diff(active X1, X2) -> diff(X1, X2)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2) = 1, [leq](x0, x1) = 1, [diff](x0, x1) = 1, [mark](x0) = x0 + 1, [active](x0) = 0, [p](x0) = 1, [s](x0) = 0, [0] = 0, [true] = 0, [false] = 0, [mark#](x0) = 1, [active#](x0) = x0 Strict: active# diff(X, Y) -> mark# if(leq(X, Y), 0(), s diff(p X, Y)) 1 + 0X + 0Y >= 1 + 0X + 0Y active# if(false(), X, Y) -> mark# Y 1 + 0X + 0Y >= 1 + 0Y active# if(true(), X, Y) -> mark# X 1 + 0X + 0Y >= 1 + 0X active# leq(s X, s Y) -> mark# leq(X, Y) 1 + 0X + 0Y >= 1 + 0X + 0Y active# leq(s X, 0()) -> mark# false() 1 + 0X >= 1 active# leq(0(), Y) -> mark# true() 1 + 0Y >= 1 active# p s X -> mark# X 1 + 0X >= 1 + 0X active# p 0() -> mark# 0() 1 >= 1 mark# diff(X1, X2) -> active# diff(mark X1, mark X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 mark# diff(X1, X2) -> mark# X2 1 + 0X1 + 0X2 >= 1 + 0X2 mark# diff(X1, X2) -> mark# X1 1 + 0X1 + 0X2 >= 1 + 0X1 mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 mark# if(X1, X2, X3) -> mark# X1 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 mark# false() -> active# false() 1 >= 0 mark# leq(X1, X2) -> active# leq(mark X1, mark X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 mark# leq(X1, X2) -> mark# X2 1 + 0X1 + 0X2 >= 1 + 0X2 mark# leq(X1, X2) -> mark# X1 1 + 0X1 + 0X2 >= 1 + 0X1 mark# s X -> mark# X 1 + 0X >= 1 + 0X mark# p X -> active# p mark X 1 + 0X >= 1 + 0X mark# p X -> mark# X 1 + 0X >= 1 + 0X Weak: diff(active X1, X2) -> diff(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 diff(mark X1, X2) -> diff(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 diff(X1, active X2) -> diff(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 diff(X1, mark X2) -> diff(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 if(active X1, X2, X3) -> if(X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 if(mark X1, X2, X3) -> if(X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 if(X1, active X2, X3) -> if(X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 if(X1, mark X2, X3) -> if(X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 if(X1, X2, active X3) -> if(X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 if(X1, X2, mark X3) -> if(X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 leq(active X1, X2) -> leq(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 leq(mark X1, X2) -> leq(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 leq(X1, active X2) -> leq(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 leq(X1, mark X2) -> leq(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 s active X -> s X 0 + 0X >= 0 + 0X s mark X -> s X 0 + 0X >= 0 + 0X p active X -> p X 1 + 0X >= 1 + 0X p mark X -> p X 1 + 0X >= 1 + 0X active diff(X, Y) -> mark if(leq(X, Y), 0(), s diff(p X, Y)) 0 + 0X + 0Y >= 2 + 0X + 0Y 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 leq(s X, s Y) -> mark leq(X, Y) 0 + 0X + 0Y >= 2 + 0X + 0Y active leq(s X, 0()) -> mark false() 0 + 0X >= 1 active leq(0(), Y) -> mark true() 0 + 0Y >= 1 active p s X -> mark X 0 + 0X >= 1 + 1X active p 0() -> mark 0() 0 >= 1 mark diff(X1, X2) -> active diff(mark X1, mark X2) 2 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 mark if(X1, X2, X3) -> active if(mark X1, X2, X3) 2 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 mark false() -> active false() 1 >= 0 mark leq(X1, X2) -> active leq(mark X1, mark X2) 2 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 mark true() -> active true() 1 >= 0 mark s X -> active s mark X 1 + 0X >= 0 + 0X mark p X -> active p mark X 2 + 0X >= 0 + 0X mark 0() -> active 0() 1 >= 0 SCCS (1): Scc: { mark# p X -> mark# X, mark# p X -> active# p mark X, mark# s X -> mark# X, mark# leq(X1, X2) -> mark# X1, mark# leq(X1, X2) -> mark# X2, mark# leq(X1, X2) -> active# leq(mark X1, mark X2), mark# if(X1, X2, X3) -> mark# X1, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), mark# diff(X1, X2) -> mark# X1, mark# diff(X1, X2) -> mark# X2, mark# diff(X1, X2) -> active# diff(mark X1, mark X2), active# p 0() -> mark# 0(), active# p s X -> mark# X, active# leq(0(), Y) -> mark# true(), active# leq(s X, 0()) -> mark# false(), active# leq(s X, s Y) -> mark# leq(X, Y), active# if(true(), X, Y) -> mark# X, active# if(false(), X, Y) -> mark# Y, active# diff(X, Y) -> mark# if(leq(X, Y), 0(), s diff(p X, Y))} SCC (19): Strict: { mark# p X -> mark# X, mark# p X -> active# p mark X, mark# s X -> mark# X, mark# leq(X1, X2) -> mark# X1, mark# leq(X1, X2) -> mark# X2, mark# leq(X1, X2) -> active# leq(mark X1, mark X2), mark# if(X1, X2, X3) -> mark# X1, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), mark# diff(X1, X2) -> mark# X1, mark# diff(X1, X2) -> mark# X2, mark# diff(X1, X2) -> active# diff(mark X1, mark X2), active# p 0() -> mark# 0(), active# p s X -> mark# X, active# leq(0(), Y) -> mark# true(), active# leq(s X, 0()) -> mark# false(), active# leq(s X, s Y) -> mark# leq(X, Y), active# if(true(), X, Y) -> mark# X, active# if(false(), X, Y) -> mark# Y, active# diff(X, Y) -> mark# if(leq(X, Y), 0(), s diff(p X, Y))} Weak: { mark 0() -> active 0(), mark p X -> active p mark X, mark s X -> active s mark X, mark true() -> active true(), mark leq(X1, X2) -> active leq(mark X1, mark X2), mark false() -> active false(), mark if(X1, X2, X3) -> active if(mark X1, X2, X3), mark diff(X1, X2) -> active diff(mark X1, mark X2), active p 0() -> mark 0(), active p s X -> mark X, active leq(0(), Y) -> mark true(), active leq(s X, 0()) -> mark false(), active leq(s X, s Y) -> mark leq(X, Y), active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active diff(X, Y) -> mark if(leq(X, Y), 0(), s diff(p X, Y)), p mark X -> p X, p active X -> p X, s mark X -> s X, s active X -> s X, leq(X1, mark X2) -> leq(X1, X2), leq(X1, active X2) -> leq(X1, X2), leq(mark X1, X2) -> leq(X1, X2), leq(active X1, X2) -> leq(X1, X2), if(X1, X2, mark X3) -> if(X1, X2, X3), if(X1, X2, active X3) -> if(X1, X2, X3), if(X1, mark X2, X3) -> if(X1, X2, X3), if(X1, active X2, X3) -> if(X1, X2, X3), if(mark X1, X2, X3) -> if(X1, X2, X3), if(active X1, X2, X3) -> if(X1, X2, X3), diff(X1, mark X2) -> diff(X1, X2), diff(X1, active X2) -> diff(X1, X2), diff(mark X1, X2) -> diff(X1, X2), diff(active X1, X2) -> diff(X1, X2)} Fail SCC (4): Strict: { diff#(X1, mark X2) -> diff#(X1, X2), diff#(X1, active X2) -> diff#(X1, X2), diff#(mark X1, X2) -> diff#(X1, X2), diff#(active X1, X2) -> diff#(X1, X2)} Weak: { mark 0() -> active 0(), mark p X -> active p mark X, mark s X -> active s mark X, mark true() -> active true(), mark leq(X1, X2) -> active leq(mark X1, mark X2), mark false() -> active false(), mark if(X1, X2, X3) -> active if(mark X1, X2, X3), mark diff(X1, X2) -> active diff(mark X1, mark X2), active p 0() -> mark 0(), active p s X -> mark X, active leq(0(), Y) -> mark true(), active leq(s X, 0()) -> mark false(), active leq(s X, s Y) -> mark leq(X, Y), active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active diff(X, Y) -> mark if(leq(X, Y), 0(), s diff(p X, Y)), p mark X -> p X, p active X -> p X, s mark X -> s X, s active X -> s X, leq(X1, mark X2) -> leq(X1, X2), leq(X1, active X2) -> leq(X1, X2), leq(mark X1, X2) -> leq(X1, X2), leq(active X1, X2) -> leq(X1, X2), if(X1, X2, mark X3) -> if(X1, X2, X3), if(X1, X2, active X3) -> if(X1, X2, X3), if(X1, mark X2, X3) -> if(X1, X2, X3), if(X1, active X2, X3) -> if(X1, X2, X3), if(mark X1, X2, X3) -> if(X1, X2, X3), if(active X1, X2, X3) -> if(X1, X2, X3), diff(X1, mark X2) -> diff(X1, X2), diff(X1, active X2) -> diff(X1, X2), diff(mark X1, X2) -> diff(X1, X2), diff(active X1, X2) -> diff(X1, X2)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2) = 0, [leq](x0, x1) = 0, [diff](x0, x1) = 0, [mark](x0) = x0, [active](x0) = x0 + 1, [p](x0) = 0, [s](x0) = 0, [0] = 1, [true] = 1, [false] = 1, [diff#](x0, x1) = x0 Strict: diff#(active X1, X2) -> diff#(X1, X2) 1 + 1X1 + 0X2 >= 0 + 1X1 + 0X2 diff#(mark X1, X2) -> diff#(X1, X2) 0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2 diff#(X1, active X2) -> diff#(X1, X2) 0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2 diff#(X1, mark X2) -> diff#(X1, X2) 0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2 Weak: diff(active X1, X2) -> diff(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 diff(mark X1, X2) -> diff(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 diff(X1, active X2) -> diff(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 diff(X1, mark X2) -> diff(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 if(active X1, X2, X3) -> if(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 if(mark X1, X2, X3) -> if(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 if(X1, active X2, X3) -> if(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 if(X1, mark X2, X3) -> if(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 if(X1, X2, active X3) -> if(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 if(X1, X2, mark X3) -> if(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 leq(active X1, X2) -> leq(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 leq(mark X1, X2) -> leq(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 leq(X1, active X2) -> leq(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 leq(X1, mark X2) -> leq(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 s active X -> s X 0 + 0X >= 0 + 0X s mark X -> s X 0 + 0X >= 0 + 0X p active X -> p X 0 + 0X >= 0 + 0X p mark X -> p X 0 + 0X >= 0 + 0X active diff(X, Y) -> mark if(leq(X, Y), 0(), s diff(p X, Y)) 1 + 0X + 0Y >= 0 + 0X + 0Y active if(false(), X, Y) -> mark Y 1 + 0X + 0Y >= 0 + 1Y active if(true(), X, Y) -> mark X 1 + 0X + 0Y >= 0 + 1X active leq(s X, s Y) -> mark leq(X, Y) 1 + 0X + 0Y >= 0 + 0X + 0Y active leq(s X, 0()) -> mark false() 1 + 0X >= 1 active leq(0(), Y) -> mark true() 1 + 0Y >= 1 active p s X -> mark X 1 + 0X >= 0 + 1X active p 0() -> mark 0() 1 >= 1 mark diff(X1, X2) -> active diff(mark X1, mark X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 mark if(X1, X2, X3) -> active if(mark X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 mark false() -> active false() 1 >= 2 mark leq(X1, X2) -> active leq(mark X1, mark X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 mark true() -> active true() 1 >= 2 mark s X -> active s mark X 0 + 0X >= 1 + 0X mark p X -> active p mark X 0 + 0X >= 1 + 0X mark 0() -> active 0() 1 >= 2 SCCS (1): Scc: { diff#(X1, mark X2) -> diff#(X1, X2), diff#(X1, active X2) -> diff#(X1, X2), diff#(mark X1, X2) -> diff#(X1, X2)} SCC (3): Strict: { diff#(X1, mark X2) -> diff#(X1, X2), diff#(X1, active X2) -> diff#(X1, X2), diff#(mark X1, X2) -> diff#(X1, X2)} Weak: { mark 0() -> active 0(), mark p X -> active p mark X, mark s X -> active s mark X, mark true() -> active true(), mark leq(X1, X2) -> active leq(mark X1, mark X2), mark false() -> active false(), mark if(X1, X2, X3) -> active if(mark X1, X2, X3), mark diff(X1, X2) -> active diff(mark X1, mark X2), active p 0() -> mark 0(), active p s X -> mark X, active leq(0(), Y) -> mark true(), active leq(s X, 0()) -> mark false(), active leq(s X, s Y) -> mark leq(X, Y), active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active diff(X, Y) -> mark if(leq(X, Y), 0(), s diff(p X, Y)), p mark X -> p X, p active X -> p X, s mark X -> s X, s active X -> s X, leq(X1, mark X2) -> leq(X1, X2), leq(X1, active X2) -> leq(X1, X2), leq(mark X1, X2) -> leq(X1, X2), leq(active X1, X2) -> leq(X1, X2), if(X1, X2, mark X3) -> if(X1, X2, X3), if(X1, X2, active X3) -> if(X1, X2, X3), if(X1, mark X2, X3) -> if(X1, X2, X3), if(X1, active X2, X3) -> if(X1, X2, X3), if(mark X1, X2, X3) -> if(X1, X2, X3), if(active X1, X2, X3) -> if(X1, X2, X3), diff(X1, mark X2) -> diff(X1, X2), diff(X1, active X2) -> diff(X1, X2), diff(mark X1, X2) -> diff(X1, X2), diff(active X1, X2) -> diff(X1, X2)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2) = x0 + 1, [leq](x0, x1) = x0 + 1, [diff](x0, x1) = x0 + x1, [mark](x0) = x0 + 1, [active](x0) = x0 + 1, [p](x0) = x0 + 1, [s](x0) = x0 + 1, [0] = 1, [true] = 1, [false] = 1, [diff#](x0, x1) = x0 Strict: diff#(mark X1, X2) -> diff#(X1, X2) 1 + 1X1 + 0X2 >= 0 + 1X1 + 0X2 diff#(X1, active X2) -> diff#(X1, X2) 0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2 diff#(X1, mark X2) -> diff#(X1, X2) 0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2 Weak: diff(active X1, X2) -> diff(X1, X2) 1 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 diff(mark X1, X2) -> diff(X1, X2) 1 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 diff(X1, active X2) -> diff(X1, X2) 1 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 diff(X1, mark X2) -> diff(X1, X2) 1 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 if(active X1, X2, X3) -> if(X1, X2, X3) 2 + 1X1 + 0X2 + 0X3 >= 1 + 1X1 + 0X2 + 0X3 if(mark X1, X2, X3) -> if(X1, X2, X3) 2 + 1X1 + 0X2 + 0X3 >= 1 + 1X1 + 0X2 + 0X3 if(X1, active X2, X3) -> if(X1, X2, X3) 1 + 1X1 + 0X2 + 0X3 >= 1 + 1X1 + 0X2 + 0X3 if(X1, mark X2, X3) -> if(X1, X2, X3) 1 + 1X1 + 0X2 + 0X3 >= 1 + 1X1 + 0X2 + 0X3 if(X1, X2, active X3) -> if(X1, X2, X3) 1 + 1X1 + 0X2 + 0X3 >= 1 + 1X1 + 0X2 + 0X3 if(X1, X2, mark X3) -> if(X1, X2, X3) 1 + 1X1 + 0X2 + 0X3 >= 1 + 1X1 + 0X2 + 0X3 leq(active X1, X2) -> leq(X1, X2) 1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2 leq(mark X1, X2) -> leq(X1, X2) 1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2 leq(X1, active X2) -> leq(X1, X2) 2 + 0X1 + 1X2 >= 1 + 0X1 + 1X2 leq(X1, mark X2) -> leq(X1, X2) 2 + 0X1 + 1X2 >= 1 + 0X1 + 1X2 s active X -> s X 2 + 1X >= 1 + 1X s mark X -> s X 2 + 1X >= 1 + 1X p active X -> p X 2 + 1X >= 1 + 1X p mark X -> p X 2 + 1X >= 1 + 1X active diff(X, Y) -> mark if(leq(X, Y), 0(), s diff(p X, Y)) 1 + 1X + 1Y >= 3 + 0X + 1Y active if(false(), X, Y) -> mark Y 3 + 0X + 0Y >= 1 + 1Y active if(true(), X, Y) -> mark X 3 + 0X + 0Y >= 1 + 1X active leq(s X, s Y) -> mark leq(X, Y) 3 + 0X + 1Y >= 2 + 0X + 1Y active leq(s X, 0()) -> mark false() 3 + 0X >= 2 active leq(0(), Y) -> mark true() 2 + 1Y >= 2 active p s X -> mark X 3 + 1X >= 1 + 1X active p 0() -> mark 0() 3 >= 2 mark diff(X1, X2) -> active diff(mark X1, mark X2) 1 + 1X1 + 1X2 >= 3 + 1X1 + 1X2 mark if(X1, X2, X3) -> active if(mark X1, X2, X3) 2 + 1X1 + 0X2 + 0X3 >= 3 + 1X1 + 0X2 + 0X3 mark false() -> active false() 2 >= 2 mark leq(X1, X2) -> active leq(mark X1, mark X2) 2 + 0X1 + 1X2 >= 3 + 0X1 + 1X2 mark true() -> active true() 2 >= 2 mark s X -> active s mark X 2 + 1X >= 3 + 1X mark p X -> active p mark X 2 + 1X >= 3 + 1X mark 0() -> active 0() 2 >= 2 SCCS (1): Scc: { diff#(X1, mark X2) -> diff#(X1, X2), diff#(X1, active X2) -> diff#(X1, X2)} SCC (2): Strict: { diff#(X1, mark X2) -> diff#(X1, X2), diff#(X1, active X2) -> diff#(X1, X2)} Weak: { mark 0() -> active 0(), mark p X -> active p mark X, mark s X -> active s mark X, mark true() -> active true(), mark leq(X1, X2) -> active leq(mark X1, mark X2), mark false() -> active false(), mark if(X1, X2, X3) -> active if(mark X1, X2, X3), mark diff(X1, X2) -> active diff(mark X1, mark X2), active p 0() -> mark 0(), active p s X -> mark X, active leq(0(), Y) -> mark true(), active leq(s X, 0()) -> mark false(), active leq(s X, s Y) -> mark leq(X, Y), active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active diff(X, Y) -> mark if(leq(X, Y), 0(), s diff(p X, Y)), p mark X -> p X, p active X -> p X, s mark X -> s X, s active X -> s X, leq(X1, mark X2) -> leq(X1, X2), leq(X1, active X2) -> leq(X1, X2), leq(mark X1, X2) -> leq(X1, X2), leq(active X1, X2) -> leq(X1, X2), if(X1, X2, mark X3) -> if(X1, X2, X3), if(X1, X2, active X3) -> if(X1, X2, X3), if(X1, mark X2, X3) -> if(X1, X2, X3), if(X1, active X2, X3) -> if(X1, X2, X3), if(mark X1, X2, X3) -> if(X1, X2, X3), if(active X1, X2, X3) -> if(X1, X2, X3), diff(X1, mark X2) -> diff(X1, X2), diff(X1, active X2) -> diff(X1, X2), diff(mark X1, X2) -> diff(X1, X2), diff(active X1, X2) -> diff(X1, X2)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2) = 0, [leq](x0, x1) = 0, [diff](x0, x1) = 0, [mark](x0) = x0, [active](x0) = x0 + 1, [p](x0) = 0, [s](x0) = 0, [0] = 1, [true] = 1, [false] = 1, [diff#](x0, x1) = x0 Strict: diff#(X1, active X2) -> diff#(X1, X2) 1 + 0X1 + 1X2 >= 0 + 0X1 + 1X2 diff#(X1, mark X2) -> diff#(X1, X2) 0 + 0X1 + 1X2 >= 0 + 0X1 + 1X2 Weak: diff(active X1, X2) -> diff(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 diff(mark X1, X2) -> diff(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 diff(X1, active X2) -> diff(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 diff(X1, mark X2) -> diff(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 if(active X1, X2, X3) -> if(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 if(mark X1, X2, X3) -> if(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 if(X1, active X2, X3) -> if(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 if(X1, mark X2, X3) -> if(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 if(X1, X2, active X3) -> if(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 if(X1, X2, mark X3) -> if(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 leq(active X1, X2) -> leq(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 leq(mark X1, X2) -> leq(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 leq(X1, active X2) -> leq(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 leq(X1, mark X2) -> leq(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 s active X -> s X 0 + 0X >= 0 + 0X s mark X -> s X 0 + 0X >= 0 + 0X p active X -> p X 0 + 0X >= 0 + 0X p mark X -> p X 0 + 0X >= 0 + 0X active diff(X, Y) -> mark if(leq(X, Y), 0(), s diff(p X, Y)) 1 + 0X + 0Y >= 0 + 0X + 0Y active if(false(), X, Y) -> mark Y 1 + 0X + 0Y >= 0 + 1Y active if(true(), X, Y) -> mark X 1 + 0X + 0Y >= 0 + 1X active leq(s X, s Y) -> mark leq(X, Y) 1 + 0X + 0Y >= 0 + 0X + 0Y active leq(s X, 0()) -> mark false() 1 + 0X >= 1 active leq(0(), Y) -> mark true() 1 + 0Y >= 1 active p s X -> mark X 1 + 0X >= 0 + 1X active p 0() -> mark 0() 1 >= 1 mark diff(X1, X2) -> active diff(mark X1, mark X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 mark if(X1, X2, X3) -> active if(mark X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 mark false() -> active false() 1 >= 2 mark leq(X1, X2) -> active leq(mark X1, mark X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 mark true() -> active true() 1 >= 2 mark s X -> active s mark X 0 + 0X >= 1 + 0X mark p X -> active p mark X 0 + 0X >= 1 + 0X mark 0() -> active 0() 1 >= 2 SCCS (1): Scc: {diff#(X1, mark X2) -> diff#(X1, X2)} SCC (1): Strict: {diff#(X1, mark X2) -> diff#(X1, X2)} Weak: { mark 0() -> active 0(), mark p X -> active p mark X, mark s X -> active s mark X, mark true() -> active true(), mark leq(X1, X2) -> active leq(mark X1, mark X2), mark false() -> active false(), mark if(X1, X2, X3) -> active if(mark X1, X2, X3), mark diff(X1, X2) -> active diff(mark X1, mark X2), active p 0() -> mark 0(), active p s X -> mark X, active leq(0(), Y) -> mark true(), active leq(s X, 0()) -> mark false(), active leq(s X, s Y) -> mark leq(X, Y), active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active diff(X, Y) -> mark if(leq(X, Y), 0(), s diff(p X, Y)), p mark X -> p X, p active X -> p X, s mark X -> s X, s active X -> s X, leq(X1, mark X2) -> leq(X1, X2), leq(X1, active X2) -> leq(X1, X2), leq(mark X1, X2) -> leq(X1, X2), leq(active X1, X2) -> leq(X1, X2), if(X1, X2, mark X3) -> if(X1, X2, X3), if(X1, X2, active X3) -> if(X1, X2, X3), if(X1, mark X2, X3) -> if(X1, X2, X3), if(X1, active X2, X3) -> if(X1, X2, X3), if(mark X1, X2, X3) -> if(X1, X2, X3), if(active X1, X2, X3) -> if(X1, X2, X3), diff(X1, mark X2) -> diff(X1, X2), diff(X1, active X2) -> diff(X1, X2), diff(mark X1, X2) -> diff(X1, X2), diff(active X1, X2) -> diff(X1, X2)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2) = x0 + 1, [leq](x0, x1) = 1, [diff](x0, x1) = 1, [mark](x0) = x0 + 1, [active](x0) = x0 + 1, [p](x0) = x0 + 1, [s](x0) = x0 + 1, [0] = 1, [true] = 1, [false] = 1, [diff#](x0, x1) = x0 Strict: diff#(X1, mark X2) -> diff#(X1, X2) 1 + 0X1 + 1X2 >= 0 + 0X1 + 1X2 Weak: diff(active X1, X2) -> diff(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 diff(mark X1, X2) -> diff(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 diff(X1, active X2) -> diff(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 diff(X1, mark X2) -> diff(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 if(active X1, X2, X3) -> if(X1, X2, X3) 2 + 1X1 + 0X2 + 0X3 >= 1 + 1X1 + 0X2 + 0X3 if(mark X1, X2, X3) -> if(X1, X2, X3) 2 + 1X1 + 0X2 + 0X3 >= 1 + 1X1 + 0X2 + 0X3 if(X1, active X2, X3) -> if(X1, X2, X3) 1 + 1X1 + 0X2 + 0X3 >= 1 + 1X1 + 0X2 + 0X3 if(X1, mark X2, X3) -> if(X1, X2, X3) 1 + 1X1 + 0X2 + 0X3 >= 1 + 1X1 + 0X2 + 0X3 if(X1, X2, active X3) -> if(X1, X2, X3) 1 + 1X1 + 0X2 + 0X3 >= 1 + 1X1 + 0X2 + 0X3 if(X1, X2, mark X3) -> if(X1, X2, X3) 1 + 1X1 + 0X2 + 0X3 >= 1 + 1X1 + 0X2 + 0X3 leq(active X1, X2) -> leq(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 leq(mark X1, X2) -> leq(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 leq(X1, active X2) -> leq(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 leq(X1, mark X2) -> leq(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 s active X -> s X 2 + 1X >= 1 + 1X s mark X -> s X 2 + 1X >= 1 + 1X p active X -> p X 2 + 1X >= 1 + 1X p mark X -> p X 2 + 1X >= 1 + 1X active diff(X, Y) -> mark if(leq(X, Y), 0(), s diff(p X, Y)) 2 + 0X + 0Y >= 3 + 0X + 0Y active if(false(), X, Y) -> mark Y 3 + 0X + 0Y >= 1 + 1Y active if(true(), X, Y) -> mark X 3 + 0X + 0Y >= 1 + 1X active leq(s X, s Y) -> mark leq(X, Y) 2 + 0X + 0Y >= 2 + 0X + 0Y active leq(s X, 0()) -> mark false() 2 + 0X >= 2 active leq(0(), Y) -> mark true() 2 + 0Y >= 2 active p s X -> mark X 3 + 1X >= 1 + 1X active p 0() -> mark 0() 3 >= 2 mark diff(X1, X2) -> active diff(mark X1, mark X2) 2 + 0X1 + 0X2 >= 2 + 0X1 + 0X2 mark if(X1, X2, X3) -> active if(mark X1, X2, X3) 2 + 1X1 + 0X2 + 0X3 >= 3 + 1X1 + 0X2 + 0X3 mark false() -> active false() 2 >= 2 mark leq(X1, X2) -> active leq(mark X1, mark X2) 2 + 0X1 + 0X2 >= 2 + 0X1 + 0X2 mark true() -> active true() 2 >= 2 mark s X -> active s mark X 2 + 1X >= 3 + 1X mark p X -> active p mark X 2 + 1X >= 3 + 1X mark 0() -> active 0() 2 >= 2 Qed SCC (6): Strict: { if#(X1, X2, mark X3) -> if#(X1, X2, X3), if#(X1, X2, active X3) -> if#(X1, X2, X3), if#(X1, mark X2, X3) -> if#(X1, X2, X3), if#(X1, active X2, X3) -> if#(X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3), if#(active X1, X2, X3) -> if#(X1, X2, X3)} Weak: { mark 0() -> active 0(), mark p X -> active p mark X, mark s X -> active s mark X, mark true() -> active true(), mark leq(X1, X2) -> active leq(mark X1, mark X2), mark false() -> active false(), mark if(X1, X2, X3) -> active if(mark X1, X2, X3), mark diff(X1, X2) -> active diff(mark X1, mark X2), active p 0() -> mark 0(), active p s X -> mark X, active leq(0(), Y) -> mark true(), active leq(s X, 0()) -> mark false(), active leq(s X, s Y) -> mark leq(X, Y), active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active diff(X, Y) -> mark if(leq(X, Y), 0(), s diff(p X, Y)), p mark X -> p X, p active X -> p X, s mark X -> s X, s active X -> s X, leq(X1, mark X2) -> leq(X1, X2), leq(X1, active X2) -> leq(X1, X2), leq(mark X1, X2) -> leq(X1, X2), leq(active X1, X2) -> leq(X1, X2), if(X1, X2, mark X3) -> if(X1, X2, X3), if(X1, X2, active X3) -> if(X1, X2, X3), if(X1, mark X2, X3) -> if(X1, X2, X3), if(X1, active X2, X3) -> if(X1, X2, X3), if(mark X1, X2, X3) -> if(X1, X2, X3), if(active X1, X2, X3) -> if(X1, X2, X3), diff(X1, mark X2) -> diff(X1, X2), diff(X1, active X2) -> diff(X1, X2), diff(mark X1, X2) -> diff(X1, X2), diff(active X1, X2) -> diff(X1, X2)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2) = 0, [leq](x0, x1) = 0, [diff](x0, x1) = 0, [mark](x0) = x0, [active](x0) = x0 + 1, [p](x0) = 0, [s](x0) = 0, [0] = 1, [true] = 1, [false] = 1, [if#](x0, x1, x2) = x0 Strict: if#(active X1, X2, X3) -> if#(X1, X2, X3) 1 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 if#(mark X1, X2, X3) -> if#(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 if#(X1, active X2, X3) -> if#(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 if#(X1, mark X2, X3) -> if#(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 if#(X1, X2, active X3) -> if#(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 if#(X1, X2, mark X3) -> if#(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 Weak: diff(active X1, X2) -> diff(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 diff(mark X1, X2) -> diff(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 diff(X1, active X2) -> diff(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 diff(X1, mark X2) -> diff(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 if(active X1, X2, X3) -> if(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 if(mark X1, X2, X3) -> if(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 if(X1, active X2, X3) -> if(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 if(X1, mark X2, X3) -> if(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 if(X1, X2, active X3) -> if(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 if(X1, X2, mark X3) -> if(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 leq(active X1, X2) -> leq(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 leq(mark X1, X2) -> leq(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 leq(X1, active X2) -> leq(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 leq(X1, mark X2) -> leq(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 s active X -> s X 0 + 0X >= 0 + 0X s mark X -> s X 0 + 0X >= 0 + 0X p active X -> p X 0 + 0X >= 0 + 0X p mark X -> p X 0 + 0X >= 0 + 0X active diff(X, Y) -> mark if(leq(X, Y), 0(), s diff(p X, Y)) 1 + 0X + 0Y >= 0 + 0X + 0Y active if(false(), X, Y) -> mark Y 1 + 0X + 0Y >= 0 + 1Y active if(true(), X, Y) -> mark X 1 + 0X + 0Y >= 0 + 1X active leq(s X, s Y) -> mark leq(X, Y) 1 + 0X + 0Y >= 0 + 0X + 0Y active leq(s X, 0()) -> mark false() 1 + 0X >= 1 active leq(0(), Y) -> mark true() 1 + 0Y >= 1 active p s X -> mark X 1 + 0X >= 0 + 1X active p 0() -> mark 0() 1 >= 1 mark diff(X1, X2) -> active diff(mark X1, mark X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 mark if(X1, X2, X3) -> active if(mark X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 mark false() -> active false() 1 >= 2 mark leq(X1, X2) -> active leq(mark X1, mark X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 mark true() -> active true() 1 >= 2 mark s X -> active s mark X 0 + 0X >= 1 + 0X mark p X -> active p mark X 0 + 0X >= 1 + 0X mark 0() -> active 0() 1 >= 2 SCCS (1): Scc: { if#(X1, X2, mark X3) -> if#(X1, X2, X3), if#(X1, X2, active X3) -> if#(X1, X2, X3), if#(X1, mark X2, X3) -> if#(X1, X2, X3), if#(X1, active X2, X3) -> if#(X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3)} SCC (5): Strict: { if#(X1, X2, mark X3) -> if#(X1, X2, X3), if#(X1, X2, active X3) -> if#(X1, X2, X3), if#(X1, mark X2, X3) -> if#(X1, X2, X3), if#(X1, active X2, X3) -> if#(X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3)} Weak: { mark 0() -> active 0(), mark p X -> active p mark X, mark s X -> active s mark X, mark true() -> active true(), mark leq(X1, X2) -> active leq(mark X1, mark X2), mark false() -> active false(), mark if(X1, X2, X3) -> active if(mark X1, X2, X3), mark diff(X1, X2) -> active diff(mark X1, mark X2), active p 0() -> mark 0(), active p s X -> mark X, active leq(0(), Y) -> mark true(), active leq(s X, 0()) -> mark false(), active leq(s X, s Y) -> mark leq(X, Y), active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active diff(X, Y) -> mark if(leq(X, Y), 0(), s diff(p X, Y)), p mark X -> p X, p active X -> p X, s mark X -> s X, s active X -> s X, leq(X1, mark X2) -> leq(X1, X2), leq(X1, active X2) -> leq(X1, X2), leq(mark X1, X2) -> leq(X1, X2), leq(active X1, X2) -> leq(X1, X2), if(X1, X2, mark X3) -> if(X1, X2, X3), if(X1, X2, active X3) -> if(X1, X2, X3), if(X1, mark X2, X3) -> if(X1, X2, X3), if(X1, active X2, X3) -> if(X1, X2, X3), if(mark X1, X2, X3) -> if(X1, X2, X3), if(active X1, X2, X3) -> if(X1, X2, X3), diff(X1, mark X2) -> diff(X1, X2), diff(X1, active X2) -> diff(X1, X2), diff(mark X1, X2) -> diff(X1, X2), diff(active X1, X2) -> diff(X1, X2)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2) = 0, [leq](x0, x1) = 0, [diff](x0, x1) = 0, [mark](x0) = x0, [active](x0) = x0 + 1, [p](x0) = 0, [s](x0) = 0, [0] = 1, [true] = 1, [false] = 1, [if#](x0, x1, x2) = x0 Strict: if#(mark X1, X2, X3) -> if#(X1, X2, X3) 0 + 0X1 + 1X2 + 0X3 >= 0 + 0X1 + 1X2 + 0X3 if#(X1, active X2, X3) -> if#(X1, X2, X3) 1 + 0X1 + 1X2 + 0X3 >= 0 + 0X1 + 1X2 + 0X3 if#(X1, mark X2, X3) -> if#(X1, X2, X3) 0 + 0X1 + 1X2 + 0X3 >= 0 + 0X1 + 1X2 + 0X3 if#(X1, X2, active X3) -> if#(X1, X2, X3) 0 + 0X1 + 1X2 + 0X3 >= 0 + 0X1 + 1X2 + 0X3 if#(X1, X2, mark X3) -> if#(X1, X2, X3) 0 + 0X1 + 1X2 + 0X3 >= 0 + 0X1 + 1X2 + 0X3 Weak: diff(active X1, X2) -> diff(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 diff(mark X1, X2) -> diff(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 diff(X1, active X2) -> diff(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 diff(X1, mark X2) -> diff(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 if(active X1, X2, X3) -> if(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 if(mark X1, X2, X3) -> if(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 if(X1, active X2, X3) -> if(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 if(X1, mark X2, X3) -> if(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 if(X1, X2, active X3) -> if(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 if(X1, X2, mark X3) -> if(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 leq(active X1, X2) -> leq(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 leq(mark X1, X2) -> leq(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 leq(X1, active X2) -> leq(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 leq(X1, mark X2) -> leq(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 s active X -> s X 0 + 0X >= 0 + 0X s mark X -> s X 0 + 0X >= 0 + 0X p active X -> p X 0 + 0X >= 0 + 0X p mark X -> p X 0 + 0X >= 0 + 0X active diff(X, Y) -> mark if(leq(X, Y), 0(), s diff(p X, Y)) 1 + 0X + 0Y >= 0 + 0X + 0Y active if(false(), X, Y) -> mark Y 1 + 0X + 0Y >= 0 + 1Y active if(true(), X, Y) -> mark X 1 + 0X + 0Y >= 0 + 1X active leq(s X, s Y) -> mark leq(X, Y) 1 + 0X + 0Y >= 0 + 0X + 0Y active leq(s X, 0()) -> mark false() 1 + 0X >= 1 active leq(0(), Y) -> mark true() 1 + 0Y >= 1 active p s X -> mark X 1 + 0X >= 0 + 1X active p 0() -> mark 0() 1 >= 1 mark diff(X1, X2) -> active diff(mark X1, mark X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 mark if(X1, X2, X3) -> active if(mark X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 mark false() -> active false() 1 >= 2 mark leq(X1, X2) -> active leq(mark X1, mark X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 mark true() -> active true() 1 >= 2 mark s X -> active s mark X 0 + 0X >= 1 + 0X mark p X -> active p mark X 0 + 0X >= 1 + 0X mark 0() -> active 0() 1 >= 2 SCCS (1): Scc: { if#(X1, X2, mark X3) -> if#(X1, X2, X3), if#(X1, X2, active X3) -> if#(X1, X2, X3), if#(X1, mark X2, X3) -> if#(X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3)} SCC (4): Strict: { if#(X1, X2, mark X3) -> if#(X1, X2, X3), if#(X1, X2, active X3) -> if#(X1, X2, X3), if#(X1, mark X2, X3) -> if#(X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3)} Weak: { mark 0() -> active 0(), mark p X -> active p mark X, mark s X -> active s mark X, mark true() -> active true(), mark leq(X1, X2) -> active leq(mark X1, mark X2), mark false() -> active false(), mark if(X1, X2, X3) -> active if(mark X1, X2, X3), mark diff(X1, X2) -> active diff(mark X1, mark X2), active p 0() -> mark 0(), active p s X -> mark X, active leq(0(), Y) -> mark true(), active leq(s X, 0()) -> mark false(), active leq(s X, s Y) -> mark leq(X, Y), active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active diff(X, Y) -> mark if(leq(X, Y), 0(), s diff(p X, Y)), p mark X -> p X, p active X -> p X, s mark X -> s X, s active X -> s X, leq(X1, mark X2) -> leq(X1, X2), leq(X1, active X2) -> leq(X1, X2), leq(mark X1, X2) -> leq(X1, X2), leq(active X1, X2) -> leq(X1, X2), if(X1, X2, mark X3) -> if(X1, X2, X3), if(X1, X2, active X3) -> if(X1, X2, X3), if(X1, mark X2, X3) -> if(X1, X2, X3), if(X1, active X2, X3) -> if(X1, X2, X3), if(mark X1, X2, X3) -> if(X1, X2, X3), if(active X1, X2, X3) -> if(X1, X2, X3), diff(X1, mark X2) -> diff(X1, X2), diff(X1, active X2) -> diff(X1, X2), diff(mark X1, X2) -> diff(X1, X2), diff(active X1, X2) -> diff(X1, X2)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2) = x0 + x1 + 1, [leq](x0, x1) = x0 + 1, [diff](x0, x1) = x0 + x1, [mark](x0) = x0 + 1, [active](x0) = x0 + 1, [p](x0) = x0 + 1, [s](x0) = x0 + 1, [0] = 1, [true] = 1, [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 if#(X1, X2, active X3) -> if#(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 if#(X1, X2, mark X3) -> if#(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 Weak: diff(active X1, X2) -> diff(X1, X2) 1 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 diff(mark X1, X2) -> diff(X1, X2) 1 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 diff(X1, active X2) -> diff(X1, X2) 1 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 diff(X1, mark X2) -> diff(X1, X2) 1 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 if(active X1, X2, X3) -> if(X1, X2, X3) 2 + 1X1 + 0X2 + 1X3 >= 1 + 1X1 + 0X2 + 1X3 if(mark X1, X2, X3) -> if(X1, X2, X3) 2 + 1X1 + 0X2 + 1X3 >= 1 + 1X1 + 0X2 + 1X3 if(X1, active X2, X3) -> if(X1, X2, X3) 1 + 1X1 + 0X2 + 1X3 >= 1 + 1X1 + 0X2 + 1X3 if(X1, mark X2, X3) -> if(X1, X2, X3) 1 + 1X1 + 0X2 + 1X3 >= 1 + 1X1 + 0X2 + 1X3 if(X1, X2, active X3) -> if(X1, X2, X3) 2 + 1X1 + 0X2 + 1X3 >= 1 + 1X1 + 0X2 + 1X3 if(X1, X2, mark X3) -> if(X1, X2, X3) 2 + 1X1 + 0X2 + 1X3 >= 1 + 1X1 + 0X2 + 1X3 leq(active X1, X2) -> leq(X1, X2) 1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2 leq(mark X1, X2) -> leq(X1, X2) 1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2 leq(X1, active X2) -> leq(X1, X2) 2 + 0X1 + 1X2 >= 1 + 0X1 + 1X2 leq(X1, mark X2) -> leq(X1, X2) 2 + 0X1 + 1X2 >= 1 + 0X1 + 1X2 s active X -> s X 2 + 1X >= 1 + 1X s mark X -> s X 2 + 1X >= 1 + 1X p active X -> p X 2 + 1X >= 1 + 1X p mark X -> p X 2 + 1X >= 1 + 1X active diff(X, Y) -> mark if(leq(X, Y), 0(), s diff(p X, Y)) 1 + 1X + 1Y >= 5 + 1X + 2Y active if(false(), X, Y) -> mark Y 3 + 0X + 1Y >= 1 + 1Y active if(true(), X, Y) -> mark X 3 + 0X + 1Y >= 1 + 1X active leq(s X, s Y) -> mark leq(X, Y) 3 + 0X + 1Y >= 2 + 0X + 1Y active leq(s X, 0()) -> mark false() 3 + 0X >= 2 active leq(0(), Y) -> mark true() 2 + 1Y >= 2 active p s X -> mark X 3 + 1X >= 1 + 1X active p 0() -> mark 0() 3 >= 2 mark diff(X1, X2) -> active diff(mark X1, mark X2) 1 + 1X1 + 1X2 >= 3 + 1X1 + 1X2 mark if(X1, X2, X3) -> active if(mark X1, X2, X3) 2 + 1X1 + 0X2 + 1X3 >= 3 + 1X1 + 0X2 + 1X3 mark false() -> active false() 2 >= 2 mark leq(X1, X2) -> active leq(mark X1, mark X2) 2 + 0X1 + 1X2 >= 3 + 0X1 + 1X2 mark true() -> active true() 2 >= 2 mark s X -> active s mark X 2 + 1X >= 3 + 1X mark p X -> active p mark X 2 + 1X >= 3 + 1X mark 0() -> active 0() 2 >= 2 SCCS (1): Scc: { if#(X1, X2, mark X3) -> if#(X1, X2, X3), if#(X1, X2, active X3) -> if#(X1, X2, X3), if#(X1, mark X2, X3) -> if#(X1, X2, X3)} SCC (3): Strict: { if#(X1, X2, mark X3) -> if#(X1, X2, X3), if#(X1, X2, active X3) -> if#(X1, X2, X3), if#(X1, mark X2, X3) -> if#(X1, X2, X3)} Weak: { mark 0() -> active 0(), mark p X -> active p mark X, mark s X -> active s mark X, mark true() -> active true(), mark leq(X1, X2) -> active leq(mark X1, mark X2), mark false() -> active false(), mark if(X1, X2, X3) -> active if(mark X1, X2, X3), mark diff(X1, X2) -> active diff(mark X1, mark X2), active p 0() -> mark 0(), active p s X -> mark X, active leq(0(), Y) -> mark true(), active leq(s X, 0()) -> mark false(), active leq(s X, s Y) -> mark leq(X, Y), active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active diff(X, Y) -> mark if(leq(X, Y), 0(), s diff(p X, Y)), p mark X -> p X, p active X -> p X, s mark X -> s X, s active X -> s X, leq(X1, mark X2) -> leq(X1, X2), leq(X1, active X2) -> leq(X1, X2), leq(mark X1, X2) -> leq(X1, X2), leq(active X1, X2) -> leq(X1, X2), if(X1, X2, mark X3) -> if(X1, X2, X3), if(X1, X2, active X3) -> if(X1, X2, X3), if(X1, mark X2, X3) -> if(X1, X2, X3), if(X1, active X2, X3) -> if(X1, X2, X3), if(mark X1, X2, X3) -> if(X1, X2, X3), if(active X1, X2, X3) -> if(X1, X2, X3), diff(X1, mark X2) -> diff(X1, X2), diff(X1, active X2) -> diff(X1, X2), diff(mark X1, X2) -> diff(X1, X2), diff(active X1, X2) -> diff(X1, X2)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2) = x0 + 1, [leq](x0, x1) = x0 + 1, [diff](x0, x1) = x0 + x1, [mark](x0) = x0 + 1, [active](x0) = x0 + 1, [p](x0) = x0 + 1, [s](x0) = x0 + 1, [0] = 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 if#(X1, X2, active X3) -> if#(X1, X2, X3) 0 + 0X1 + 1X2 + 0X3 >= 0 + 0X1 + 1X2 + 0X3 if#(X1, X2, mark X3) -> if#(X1, X2, X3) 0 + 0X1 + 1X2 + 0X3 >= 0 + 0X1 + 1X2 + 0X3 Weak: diff(active X1, X2) -> diff(X1, X2) 1 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 diff(mark X1, X2) -> diff(X1, X2) 1 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 diff(X1, active X2) -> diff(X1, X2) 1 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 diff(X1, mark X2) -> diff(X1, X2) 1 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 if(active X1, X2, X3) -> if(X1, X2, X3) 2 + 1X1 + 0X2 + 0X3 >= 1 + 1X1 + 0X2 + 0X3 if(mark X1, X2, X3) -> if(X1, X2, X3) 2 + 1X1 + 0X2 + 0X3 >= 1 + 1X1 + 0X2 + 0X3 if(X1, active X2, X3) -> if(X1, X2, X3) 1 + 1X1 + 0X2 + 0X3 >= 1 + 1X1 + 0X2 + 0X3 if(X1, mark X2, X3) -> if(X1, X2, X3) 1 + 1X1 + 0X2 + 0X3 >= 1 + 1X1 + 0X2 + 0X3 if(X1, X2, active X3) -> if(X1, X2, X3) 1 + 1X1 + 0X2 + 0X3 >= 1 + 1X1 + 0X2 + 0X3 if(X1, X2, mark X3) -> if(X1, X2, X3) 1 + 1X1 + 0X2 + 0X3 >= 1 + 1X1 + 0X2 + 0X3 leq(active X1, X2) -> leq(X1, X2) 1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2 leq(mark X1, X2) -> leq(X1, X2) 1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2 leq(X1, active X2) -> leq(X1, X2) 2 + 0X1 + 1X2 >= 1 + 0X1 + 1X2 leq(X1, mark X2) -> leq(X1, X2) 2 + 0X1 + 1X2 >= 1 + 0X1 + 1X2 s active X -> s X 2 + 1X >= 1 + 1X s mark X -> s X 2 + 1X >= 1 + 1X p active X -> p X 2 + 1X >= 1 + 1X p mark X -> p X 2 + 1X >= 1 + 1X active diff(X, Y) -> mark if(leq(X, Y), 0(), s diff(p X, Y)) 1 + 1X + 1Y >= 3 + 0X + 1Y active if(false(), X, Y) -> mark Y 3 + 0X + 0Y >= 1 + 1Y active if(true(), X, Y) -> mark X 3 + 0X + 0Y >= 1 + 1X active leq(s X, s Y) -> mark leq(X, Y) 3 + 0X + 1Y >= 2 + 0X + 1Y active leq(s X, 0()) -> mark false() 3 + 0X >= 2 active leq(0(), Y) -> mark true() 2 + 1Y >= 2 active p s X -> mark X 3 + 1X >= 1 + 1X active p 0() -> mark 0() 3 >= 2 mark diff(X1, X2) -> active diff(mark X1, mark X2) 1 + 1X1 + 1X2 >= 3 + 1X1 + 1X2 mark if(X1, X2, X3) -> active if(mark X1, X2, X3) 2 + 1X1 + 0X2 + 0X3 >= 3 + 1X1 + 0X2 + 0X3 mark false() -> active false() 2 >= 2 mark leq(X1, X2) -> active leq(mark X1, mark X2) 2 + 0X1 + 1X2 >= 3 + 0X1 + 1X2 mark true() -> active true() 2 >= 2 mark s X -> active s mark X 2 + 1X >= 3 + 1X mark p X -> active p mark X 2 + 1X >= 3 + 1X mark 0() -> active 0() 2 >= 2 SCCS (1): Scc: { if#(X1, X2, mark X3) -> if#(X1, X2, X3), if#(X1, X2, active X3) -> if#(X1, X2, X3)} SCC (2): Strict: { if#(X1, X2, mark X3) -> if#(X1, X2, X3), if#(X1, X2, active X3) -> if#(X1, X2, X3)} Weak: { mark 0() -> active 0(), mark p X -> active p mark X, mark s X -> active s mark X, mark true() -> active true(), mark leq(X1, X2) -> active leq(mark X1, mark X2), mark false() -> active false(), mark if(X1, X2, X3) -> active if(mark X1, X2, X3), mark diff(X1, X2) -> active diff(mark X1, mark X2), active p 0() -> mark 0(), active p s X -> mark X, active leq(0(), Y) -> mark true(), active leq(s X, 0()) -> mark false(), active leq(s X, s Y) -> mark leq(X, Y), active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active diff(X, Y) -> mark if(leq(X, Y), 0(), s diff(p X, Y)), p mark X -> p X, p active X -> p X, s mark X -> s X, s active X -> s X, leq(X1, mark X2) -> leq(X1, X2), leq(X1, active X2) -> leq(X1, X2), leq(mark X1, X2) -> leq(X1, X2), leq(active X1, X2) -> leq(X1, X2), if(X1, X2, mark X3) -> if(X1, X2, X3), if(X1, X2, active X3) -> if(X1, X2, X3), if(X1, mark X2, X3) -> if(X1, X2, X3), if(X1, active X2, X3) -> if(X1, X2, X3), if(mark X1, X2, X3) -> if(X1, X2, X3), if(active X1, X2, X3) -> if(X1, X2, X3), diff(X1, mark X2) -> diff(X1, X2), diff(X1, active X2) -> diff(X1, X2), diff(mark X1, X2) -> diff(X1, X2), diff(active X1, X2) -> diff(X1, X2)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2) = 0, [leq](x0, x1) = 0, [diff](x0, x1) = 0, [mark](x0) = x0, [active](x0) = x0 + 1, [p](x0) = 0, [s](x0) = 0, [0] = 1, [true] = 1, [false] = 1, [if#](x0, x1, x2) = x0 Strict: if#(X1, X2, active X3) -> if#(X1, X2, X3) 1 + 0X1 + 0X2 + 1X3 >= 0 + 0X1 + 0X2 + 1X3 if#(X1, X2, mark X3) -> if#(X1, X2, X3) 0 + 0X1 + 0X2 + 1X3 >= 0 + 0X1 + 0X2 + 1X3 Weak: diff(active X1, X2) -> diff(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 diff(mark X1, X2) -> diff(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 diff(X1, active X2) -> diff(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 diff(X1, mark X2) -> diff(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 if(active X1, X2, X3) -> if(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 if(mark X1, X2, X3) -> if(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 if(X1, active X2, X3) -> if(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 if(X1, mark X2, X3) -> if(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 if(X1, X2, active X3) -> if(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 if(X1, X2, mark X3) -> if(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 leq(active X1, X2) -> leq(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 leq(mark X1, X2) -> leq(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 leq(X1, active X2) -> leq(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 leq(X1, mark X2) -> leq(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 s active X -> s X 0 + 0X >= 0 + 0X s mark X -> s X 0 + 0X >= 0 + 0X p active X -> p X 0 + 0X >= 0 + 0X p mark X -> p X 0 + 0X >= 0 + 0X active diff(X, Y) -> mark if(leq(X, Y), 0(), s diff(p X, Y)) 1 + 0X + 0Y >= 0 + 0X + 0Y active if(false(), X, Y) -> mark Y 1 + 0X + 0Y >= 0 + 1Y active if(true(), X, Y) -> mark X 1 + 0X + 0Y >= 0 + 1X active leq(s X, s Y) -> mark leq(X, Y) 1 + 0X + 0Y >= 0 + 0X + 0Y active leq(s X, 0()) -> mark false() 1 + 0X >= 1 active leq(0(), Y) -> mark true() 1 + 0Y >= 1 active p s X -> mark X 1 + 0X >= 0 + 1X active p 0() -> mark 0() 1 >= 1 mark diff(X1, X2) -> active diff(mark X1, mark X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 mark if(X1, X2, X3) -> active if(mark X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 mark false() -> active false() 1 >= 2 mark leq(X1, X2) -> active leq(mark X1, mark X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 mark true() -> active true() 1 >= 2 mark s X -> active s mark X 0 + 0X >= 1 + 0X mark p X -> active p mark X 0 + 0X >= 1 + 0X mark 0() -> active 0() 1 >= 2 SCCS (1): Scc: {if#(X1, X2, mark X3) -> if#(X1, X2, X3)} SCC (1): Strict: {if#(X1, X2, mark X3) -> if#(X1, X2, X3)} Weak: { mark 0() -> active 0(), mark p X -> active p mark X, mark s X -> active s mark X, mark true() -> active true(), mark leq(X1, X2) -> active leq(mark X1, mark X2), mark false() -> active false(), mark if(X1, X2, X3) -> active if(mark X1, X2, X3), mark diff(X1, X2) -> active diff(mark X1, mark X2), active p 0() -> mark 0(), active p s X -> mark X, active leq(0(), Y) -> mark true(), active leq(s X, 0()) -> mark false(), active leq(s X, s Y) -> mark leq(X, Y), active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active diff(X, Y) -> mark if(leq(X, Y), 0(), s diff(p X, Y)), p mark X -> p X, p active X -> p X, s mark X -> s X, s active X -> s X, leq(X1, mark X2) -> leq(X1, X2), leq(X1, active X2) -> leq(X1, X2), leq(mark X1, X2) -> leq(X1, X2), leq(active X1, X2) -> leq(X1, X2), if(X1, X2, mark X3) -> if(X1, X2, X3), if(X1, X2, active X3) -> if(X1, X2, X3), if(X1, mark X2, X3) -> if(X1, X2, X3), if(X1, active X2, X3) -> if(X1, X2, X3), if(mark X1, X2, X3) -> if(X1, X2, X3), if(active X1, X2, X3) -> if(X1, X2, X3), diff(X1, mark X2) -> diff(X1, X2), diff(X1, active X2) -> diff(X1, X2), diff(mark X1, X2) -> diff(X1, X2), diff(active X1, X2) -> diff(X1, X2)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2) = x0 + 1, [leq](x0, x1) = 1, [diff](x0, x1) = 1, [mark](x0) = x0 + 1, [active](x0) = x0 + 1, [p](x0) = x0 + 1, [s](x0) = x0 + 1, [0] = 1, [true] = 1, [false] = 1, [if#](x0, x1, x2) = x0 Strict: if#(X1, X2, mark X3) -> if#(X1, X2, X3) 1 + 0X1 + 0X2 + 1X3 >= 0 + 0X1 + 0X2 + 1X3 Weak: diff(active X1, X2) -> diff(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 diff(mark X1, X2) -> diff(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 diff(X1, active X2) -> diff(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 diff(X1, mark X2) -> diff(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 if(active X1, X2, X3) -> if(X1, X2, X3) 2 + 1X1 + 0X2 + 0X3 >= 1 + 1X1 + 0X2 + 0X3 if(mark X1, X2, X3) -> if(X1, X2, X3) 2 + 1X1 + 0X2 + 0X3 >= 1 + 1X1 + 0X2 + 0X3 if(X1, active X2, X3) -> if(X1, X2, X3) 1 + 1X1 + 0X2 + 0X3 >= 1 + 1X1 + 0X2 + 0X3 if(X1, mark X2, X3) -> if(X1, X2, X3) 1 + 1X1 + 0X2 + 0X3 >= 1 + 1X1 + 0X2 + 0X3 if(X1, X2, active X3) -> if(X1, X2, X3) 1 + 1X1 + 0X2 + 0X3 >= 1 + 1X1 + 0X2 + 0X3 if(X1, X2, mark X3) -> if(X1, X2, X3) 1 + 1X1 + 0X2 + 0X3 >= 1 + 1X1 + 0X2 + 0X3 leq(active X1, X2) -> leq(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 leq(mark X1, X2) -> leq(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 leq(X1, active X2) -> leq(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 leq(X1, mark X2) -> leq(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 s active X -> s X 2 + 1X >= 1 + 1X s mark X -> s X 2 + 1X >= 1 + 1X p active X -> p X 2 + 1X >= 1 + 1X p mark X -> p X 2 + 1X >= 1 + 1X active diff(X, Y) -> mark if(leq(X, Y), 0(), s diff(p X, Y)) 2 + 0X + 0Y >= 3 + 0X + 0Y active if(false(), X, Y) -> mark Y 3 + 0X + 0Y >= 1 + 1Y active if(true(), X, Y) -> mark X 3 + 0X + 0Y >= 1 + 1X active leq(s X, s Y) -> mark leq(X, Y) 2 + 0X + 0Y >= 2 + 0X + 0Y active leq(s X, 0()) -> mark false() 2 + 0X >= 2 active leq(0(), Y) -> mark true() 2 + 0Y >= 2 active p s X -> mark X 3 + 1X >= 1 + 1X active p 0() -> mark 0() 3 >= 2 mark diff(X1, X2) -> active diff(mark X1, mark X2) 2 + 0X1 + 0X2 >= 2 + 0X1 + 0X2 mark if(X1, X2, X3) -> active if(mark X1, X2, X3) 2 + 1X1 + 0X2 + 0X3 >= 3 + 1X1 + 0X2 + 0X3 mark false() -> active false() 2 >= 2 mark leq(X1, X2) -> active leq(mark X1, mark X2) 2 + 0X1 + 0X2 >= 2 + 0X1 + 0X2 mark true() -> active true() 2 >= 2 mark s X -> active s mark X 2 + 1X >= 3 + 1X mark p X -> active p mark X 2 + 1X >= 3 + 1X mark 0() -> active 0() 2 >= 2 Qed SCC (4): Strict: { leq#(X1, mark X2) -> leq#(X1, X2), leq#(X1, active X2) -> leq#(X1, X2), leq#(mark X1, X2) -> leq#(X1, X2), leq#(active X1, X2) -> leq#(X1, X2)} Weak: { mark 0() -> active 0(), mark p X -> active p mark X, mark s X -> active s mark X, mark true() -> active true(), mark leq(X1, X2) -> active leq(mark X1, mark X2), mark false() -> active false(), mark if(X1, X2, X3) -> active if(mark X1, X2, X3), mark diff(X1, X2) -> active diff(mark X1, mark X2), active p 0() -> mark 0(), active p s X -> mark X, active leq(0(), Y) -> mark true(), active leq(s X, 0()) -> mark false(), active leq(s X, s Y) -> mark leq(X, Y), active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active diff(X, Y) -> mark if(leq(X, Y), 0(), s diff(p X, Y)), p mark X -> p X, p active X -> p X, s mark X -> s X, s active X -> s X, leq(X1, mark X2) -> leq(X1, X2), leq(X1, active X2) -> leq(X1, X2), leq(mark X1, X2) -> leq(X1, X2), leq(active X1, X2) -> leq(X1, X2), if(X1, X2, mark X3) -> if(X1, X2, X3), if(X1, X2, active X3) -> if(X1, X2, X3), if(X1, mark X2, X3) -> if(X1, X2, X3), if(X1, active X2, X3) -> if(X1, X2, X3), if(mark X1, X2, X3) -> if(X1, X2, X3), if(active X1, X2, X3) -> if(X1, X2, X3), diff(X1, mark X2) -> diff(X1, X2), diff(X1, active X2) -> diff(X1, X2), diff(mark X1, X2) -> diff(X1, X2), diff(active X1, X2) -> diff(X1, X2)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2) = 0, [leq](x0, x1) = 0, [diff](x0, x1) = 0, [mark](x0) = x0, [active](x0) = x0 + 1, [p](x0) = 0, [s](x0) = 0, [0] = 1, [true] = 1, [false] = 1, [leq#](x0, x1) = x0 Strict: leq#(active X1, X2) -> leq#(X1, X2) 1 + 1X1 + 0X2 >= 0 + 1X1 + 0X2 leq#(mark X1, X2) -> leq#(X1, X2) 0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2 leq#(X1, active X2) -> leq#(X1, X2) 0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2 leq#(X1, mark X2) -> leq#(X1, X2) 0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2 Weak: diff(active X1, X2) -> diff(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 diff(mark X1, X2) -> diff(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 diff(X1, active X2) -> diff(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 diff(X1, mark X2) -> diff(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 if(active X1, X2, X3) -> if(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 if(mark X1, X2, X3) -> if(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 if(X1, active X2, X3) -> if(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 if(X1, mark X2, X3) -> if(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 if(X1, X2, active X3) -> if(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 if(X1, X2, mark X3) -> if(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 leq(active X1, X2) -> leq(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 leq(mark X1, X2) -> leq(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 leq(X1, active X2) -> leq(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 leq(X1, mark X2) -> leq(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 s active X -> s X 0 + 0X >= 0 + 0X s mark X -> s X 0 + 0X >= 0 + 0X p active X -> p X 0 + 0X >= 0 + 0X p mark X -> p X 0 + 0X >= 0 + 0X active diff(X, Y) -> mark if(leq(X, Y), 0(), s diff(p X, Y)) 1 + 0X + 0Y >= 0 + 0X + 0Y active if(false(), X, Y) -> mark Y 1 + 0X + 0Y >= 0 + 1Y active if(true(), X, Y) -> mark X 1 + 0X + 0Y >= 0 + 1X active leq(s X, s Y) -> mark leq(X, Y) 1 + 0X + 0Y >= 0 + 0X + 0Y active leq(s X, 0()) -> mark false() 1 + 0X >= 1 active leq(0(), Y) -> mark true() 1 + 0Y >= 1 active p s X -> mark X 1 + 0X >= 0 + 1X active p 0() -> mark 0() 1 >= 1 mark diff(X1, X2) -> active diff(mark X1, mark X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 mark if(X1, X2, X3) -> active if(mark X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 mark false() -> active false() 1 >= 2 mark leq(X1, X2) -> active leq(mark X1, mark X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 mark true() -> active true() 1 >= 2 mark s X -> active s mark X 0 + 0X >= 1 + 0X mark p X -> active p mark X 0 + 0X >= 1 + 0X mark 0() -> active 0() 1 >= 2 SCCS (1): Scc: { leq#(X1, mark X2) -> leq#(X1, X2), leq#(X1, active X2) -> leq#(X1, X2), leq#(mark X1, X2) -> leq#(X1, X2)} SCC (3): Strict: { leq#(X1, mark X2) -> leq#(X1, X2), leq#(X1, active X2) -> leq#(X1, X2), leq#(mark X1, X2) -> leq#(X1, X2)} Weak: { mark 0() -> active 0(), mark p X -> active p mark X, mark s X -> active s mark X, mark true() -> active true(), mark leq(X1, X2) -> active leq(mark X1, mark X2), mark false() -> active false(), mark if(X1, X2, X3) -> active if(mark X1, X2, X3), mark diff(X1, X2) -> active diff(mark X1, mark X2), active p 0() -> mark 0(), active p s X -> mark X, active leq(0(), Y) -> mark true(), active leq(s X, 0()) -> mark false(), active leq(s X, s Y) -> mark leq(X, Y), active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active diff(X, Y) -> mark if(leq(X, Y), 0(), s diff(p X, Y)), p mark X -> p X, p active X -> p X, s mark X -> s X, s active X -> s X, leq(X1, mark X2) -> leq(X1, X2), leq(X1, active X2) -> leq(X1, X2), leq(mark X1, X2) -> leq(X1, X2), leq(active X1, X2) -> leq(X1, X2), if(X1, X2, mark X3) -> if(X1, X2, X3), if(X1, X2, active X3) -> if(X1, X2, X3), if(X1, mark X2, X3) -> if(X1, X2, X3), if(X1, active X2, X3) -> if(X1, X2, X3), if(mark X1, X2, X3) -> if(X1, X2, X3), if(active X1, X2, X3) -> if(X1, X2, X3), diff(X1, mark X2) -> diff(X1, X2), diff(X1, active X2) -> diff(X1, X2), diff(mark X1, X2) -> diff(X1, X2), diff(active X1, X2) -> diff(X1, X2)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2) = x0 + 1, [leq](x0, x1) = x0 + 1, [diff](x0, x1) = x0 + x1, [mark](x0) = x0 + 1, [active](x0) = x0 + 1, [p](x0) = x0 + 1, [s](x0) = x0 + 1, [0] = 1, [true] = 1, [false] = 1, [leq#](x0, x1) = x0 Strict: leq#(mark X1, X2) -> leq#(X1, X2) 1 + 1X1 + 0X2 >= 0 + 1X1 + 0X2 leq#(X1, active X2) -> leq#(X1, X2) 0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2 leq#(X1, mark X2) -> leq#(X1, X2) 0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2 Weak: diff(active X1, X2) -> diff(X1, X2) 1 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 diff(mark X1, X2) -> diff(X1, X2) 1 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 diff(X1, active X2) -> diff(X1, X2) 1 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 diff(X1, mark X2) -> diff(X1, X2) 1 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 if(active X1, X2, X3) -> if(X1, X2, X3) 2 + 1X1 + 0X2 + 0X3 >= 1 + 1X1 + 0X2 + 0X3 if(mark X1, X2, X3) -> if(X1, X2, X3) 2 + 1X1 + 0X2 + 0X3 >= 1 + 1X1 + 0X2 + 0X3 if(X1, active X2, X3) -> if(X1, X2, X3) 1 + 1X1 + 0X2 + 0X3 >= 1 + 1X1 + 0X2 + 0X3 if(X1, mark X2, X3) -> if(X1, X2, X3) 1 + 1X1 + 0X2 + 0X3 >= 1 + 1X1 + 0X2 + 0X3 if(X1, X2, active X3) -> if(X1, X2, X3) 1 + 1X1 + 0X2 + 0X3 >= 1 + 1X1 + 0X2 + 0X3 if(X1, X2, mark X3) -> if(X1, X2, X3) 1 + 1X1 + 0X2 + 0X3 >= 1 + 1X1 + 0X2 + 0X3 leq(active X1, X2) -> leq(X1, X2) 1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2 leq(mark X1, X2) -> leq(X1, X2) 1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2 leq(X1, active X2) -> leq(X1, X2) 2 + 0X1 + 1X2 >= 1 + 0X1 + 1X2 leq(X1, mark X2) -> leq(X1, X2) 2 + 0X1 + 1X2 >= 1 + 0X1 + 1X2 s active X -> s X 2 + 1X >= 1 + 1X s mark X -> s X 2 + 1X >= 1 + 1X p active X -> p X 2 + 1X >= 1 + 1X p mark X -> p X 2 + 1X >= 1 + 1X active diff(X, Y) -> mark if(leq(X, Y), 0(), s diff(p X, Y)) 1 + 1X + 1Y >= 3 + 0X + 1Y active if(false(), X, Y) -> mark Y 3 + 0X + 0Y >= 1 + 1Y active if(true(), X, Y) -> mark X 3 + 0X + 0Y >= 1 + 1X active leq(s X, s Y) -> mark leq(X, Y) 3 + 0X + 1Y >= 2 + 0X + 1Y active leq(s X, 0()) -> mark false() 3 + 0X >= 2 active leq(0(), Y) -> mark true() 2 + 1Y >= 2 active p s X -> mark X 3 + 1X >= 1 + 1X active p 0() -> mark 0() 3 >= 2 mark diff(X1, X2) -> active diff(mark X1, mark X2) 1 + 1X1 + 1X2 >= 3 + 1X1 + 1X2 mark if(X1, X2, X3) -> active if(mark X1, X2, X3) 2 + 1X1 + 0X2 + 0X3 >= 3 + 1X1 + 0X2 + 0X3 mark false() -> active false() 2 >= 2 mark leq(X1, X2) -> active leq(mark X1, mark X2) 2 + 0X1 + 1X2 >= 3 + 0X1 + 1X2 mark true() -> active true() 2 >= 2 mark s X -> active s mark X 2 + 1X >= 3 + 1X mark p X -> active p mark X 2 + 1X >= 3 + 1X mark 0() -> active 0() 2 >= 2 SCCS (1): Scc: { leq#(X1, mark X2) -> leq#(X1, X2), leq#(X1, active X2) -> leq#(X1, X2)} SCC (2): Strict: { leq#(X1, mark X2) -> leq#(X1, X2), leq#(X1, active X2) -> leq#(X1, X2)} Weak: { mark 0() -> active 0(), mark p X -> active p mark X, mark s X -> active s mark X, mark true() -> active true(), mark leq(X1, X2) -> active leq(mark X1, mark X2), mark false() -> active false(), mark if(X1, X2, X3) -> active if(mark X1, X2, X3), mark diff(X1, X2) -> active diff(mark X1, mark X2), active p 0() -> mark 0(), active p s X -> mark X, active leq(0(), Y) -> mark true(), active leq(s X, 0()) -> mark false(), active leq(s X, s Y) -> mark leq(X, Y), active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active diff(X, Y) -> mark if(leq(X, Y), 0(), s diff(p X, Y)), p mark X -> p X, p active X -> p X, s mark X -> s X, s active X -> s X, leq(X1, mark X2) -> leq(X1, X2), leq(X1, active X2) -> leq(X1, X2), leq(mark X1, X2) -> leq(X1, X2), leq(active X1, X2) -> leq(X1, X2), if(X1, X2, mark X3) -> if(X1, X2, X3), if(X1, X2, active X3) -> if(X1, X2, X3), if(X1, mark X2, X3) -> if(X1, X2, X3), if(X1, active X2, X3) -> if(X1, X2, X3), if(mark X1, X2, X3) -> if(X1, X2, X3), if(active X1, X2, X3) -> if(X1, X2, X3), diff(X1, mark X2) -> diff(X1, X2), diff(X1, active X2) -> diff(X1, X2), diff(mark X1, X2) -> diff(X1, X2), diff(active X1, X2) -> diff(X1, X2)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2) = 0, [leq](x0, x1) = 0, [diff](x0, x1) = 0, [mark](x0) = x0, [active](x0) = x0 + 1, [p](x0) = 0, [s](x0) = 0, [0] = 1, [true] = 1, [false] = 1, [leq#](x0, x1) = x0 Strict: leq#(X1, active X2) -> leq#(X1, X2) 1 + 0X1 + 1X2 >= 0 + 0X1 + 1X2 leq#(X1, mark X2) -> leq#(X1, X2) 0 + 0X1 + 1X2 >= 0 + 0X1 + 1X2 Weak: diff(active X1, X2) -> diff(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 diff(mark X1, X2) -> diff(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 diff(X1, active X2) -> diff(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 diff(X1, mark X2) -> diff(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 if(active X1, X2, X3) -> if(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 if(mark X1, X2, X3) -> if(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 if(X1, active X2, X3) -> if(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 if(X1, mark X2, X3) -> if(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 if(X1, X2, active X3) -> if(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 if(X1, X2, mark X3) -> if(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 leq(active X1, X2) -> leq(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 leq(mark X1, X2) -> leq(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 leq(X1, active X2) -> leq(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 leq(X1, mark X2) -> leq(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 s active X -> s X 0 + 0X >= 0 + 0X s mark X -> s X 0 + 0X >= 0 + 0X p active X -> p X 0 + 0X >= 0 + 0X p mark X -> p X 0 + 0X >= 0 + 0X active diff(X, Y) -> mark if(leq(X, Y), 0(), s diff(p X, Y)) 1 + 0X + 0Y >= 0 + 0X + 0Y active if(false(), X, Y) -> mark Y 1 + 0X + 0Y >= 0 + 1Y active if(true(), X, Y) -> mark X 1 + 0X + 0Y >= 0 + 1X active leq(s X, s Y) -> mark leq(X, Y) 1 + 0X + 0Y >= 0 + 0X + 0Y active leq(s X, 0()) -> mark false() 1 + 0X >= 1 active leq(0(), Y) -> mark true() 1 + 0Y >= 1 active p s X -> mark X 1 + 0X >= 0 + 1X active p 0() -> mark 0() 1 >= 1 mark diff(X1, X2) -> active diff(mark X1, mark X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 mark if(X1, X2, X3) -> active if(mark X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 mark false() -> active false() 1 >= 2 mark leq(X1, X2) -> active leq(mark X1, mark X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 mark true() -> active true() 1 >= 2 mark s X -> active s mark X 0 + 0X >= 1 + 0X mark p X -> active p mark X 0 + 0X >= 1 + 0X mark 0() -> active 0() 1 >= 2 SCCS (1): Scc: {leq#(X1, mark X2) -> leq#(X1, X2)} SCC (1): Strict: {leq#(X1, mark X2) -> leq#(X1, X2)} Weak: { mark 0() -> active 0(), mark p X -> active p mark X, mark s X -> active s mark X, mark true() -> active true(), mark leq(X1, X2) -> active leq(mark X1, mark X2), mark false() -> active false(), mark if(X1, X2, X3) -> active if(mark X1, X2, X3), mark diff(X1, X2) -> active diff(mark X1, mark X2), active p 0() -> mark 0(), active p s X -> mark X, active leq(0(), Y) -> mark true(), active leq(s X, 0()) -> mark false(), active leq(s X, s Y) -> mark leq(X, Y), active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active diff(X, Y) -> mark if(leq(X, Y), 0(), s diff(p X, Y)), p mark X -> p X, p active X -> p X, s mark X -> s X, s active X -> s X, leq(X1, mark X2) -> leq(X1, X2), leq(X1, active X2) -> leq(X1, X2), leq(mark X1, X2) -> leq(X1, X2), leq(active X1, X2) -> leq(X1, X2), if(X1, X2, mark X3) -> if(X1, X2, X3), if(X1, X2, active X3) -> if(X1, X2, X3), if(X1, mark X2, X3) -> if(X1, X2, X3), if(X1, active X2, X3) -> if(X1, X2, X3), if(mark X1, X2, X3) -> if(X1, X2, X3), if(active X1, X2, X3) -> if(X1, X2, X3), diff(X1, mark X2) -> diff(X1, X2), diff(X1, active X2) -> diff(X1, X2), diff(mark X1, X2) -> diff(X1, X2), diff(active X1, X2) -> diff(X1, X2)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2) = x0 + 1, [leq](x0, x1) = 1, [diff](x0, x1) = 1, [mark](x0) = x0 + 1, [active](x0) = x0 + 1, [p](x0) = x0 + 1, [s](x0) = x0 + 1, [0] = 1, [true] = 1, [false] = 1, [leq#](x0, x1) = x0 Strict: leq#(X1, mark X2) -> leq#(X1, X2) 1 + 0X1 + 1X2 >= 0 + 0X1 + 1X2 Weak: diff(active X1, X2) -> diff(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 diff(mark X1, X2) -> diff(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 diff(X1, active X2) -> diff(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 diff(X1, mark X2) -> diff(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 if(active X1, X2, X3) -> if(X1, X2, X3) 2 + 1X1 + 0X2 + 0X3 >= 1 + 1X1 + 0X2 + 0X3 if(mark X1, X2, X3) -> if(X1, X2, X3) 2 + 1X1 + 0X2 + 0X3 >= 1 + 1X1 + 0X2 + 0X3 if(X1, active X2, X3) -> if(X1, X2, X3) 1 + 1X1 + 0X2 + 0X3 >= 1 + 1X1 + 0X2 + 0X3 if(X1, mark X2, X3) -> if(X1, X2, X3) 1 + 1X1 + 0X2 + 0X3 >= 1 + 1X1 + 0X2 + 0X3 if(X1, X2, active X3) -> if(X1, X2, X3) 1 + 1X1 + 0X2 + 0X3 >= 1 + 1X1 + 0X2 + 0X3 if(X1, X2, mark X3) -> if(X1, X2, X3) 1 + 1X1 + 0X2 + 0X3 >= 1 + 1X1 + 0X2 + 0X3 leq(active X1, X2) -> leq(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 leq(mark X1, X2) -> leq(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 leq(X1, active X2) -> leq(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 leq(X1, mark X2) -> leq(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 s active X -> s X 2 + 1X >= 1 + 1X s mark X -> s X 2 + 1X >= 1 + 1X p active X -> p X 2 + 1X >= 1 + 1X p mark X -> p X 2 + 1X >= 1 + 1X active diff(X, Y) -> mark if(leq(X, Y), 0(), s diff(p X, Y)) 2 + 0X + 0Y >= 3 + 0X + 0Y active if(false(), X, Y) -> mark Y 3 + 0X + 0Y >= 1 + 1Y active if(true(), X, Y) -> mark X 3 + 0X + 0Y >= 1 + 1X active leq(s X, s Y) -> mark leq(X, Y) 2 + 0X + 0Y >= 2 + 0X + 0Y active leq(s X, 0()) -> mark false() 2 + 0X >= 2 active leq(0(), Y) -> mark true() 2 + 0Y >= 2 active p s X -> mark X 3 + 1X >= 1 + 1X active p 0() -> mark 0() 3 >= 2 mark diff(X1, X2) -> active diff(mark X1, mark X2) 2 + 0X1 + 0X2 >= 2 + 0X1 + 0X2 mark if(X1, X2, X3) -> active if(mark X1, X2, X3) 2 + 1X1 + 0X2 + 0X3 >= 3 + 1X1 + 0X2 + 0X3 mark false() -> active false() 2 >= 2 mark leq(X1, X2) -> active leq(mark X1, mark X2) 2 + 0X1 + 0X2 >= 2 + 0X1 + 0X2 mark true() -> active true() 2 >= 2 mark s X -> active s mark X 2 + 1X >= 3 + 1X mark p X -> active p mark X 2 + 1X >= 3 + 1X mark 0() -> active 0() 2 >= 2 Qed SCC (2): Strict: { s# mark X -> s# X, s# active X -> s# X} Weak: { mark 0() -> active 0(), mark p X -> active p mark X, mark s X -> active s mark X, mark true() -> active true(), mark leq(X1, X2) -> active leq(mark X1, mark X2), mark false() -> active false(), mark if(X1, X2, X3) -> active if(mark X1, X2, X3), mark diff(X1, X2) -> active diff(mark X1, mark X2), active p 0() -> mark 0(), active p s X -> mark X, active leq(0(), Y) -> mark true(), active leq(s X, 0()) -> mark false(), active leq(s X, s Y) -> mark leq(X, Y), active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active diff(X, Y) -> mark if(leq(X, Y), 0(), s diff(p X, Y)), p mark X -> p X, p active X -> p X, s mark X -> s X, s active X -> s X, leq(X1, mark X2) -> leq(X1, X2), leq(X1, active X2) -> leq(X1, X2), leq(mark X1, X2) -> leq(X1, X2), leq(active X1, X2) -> leq(X1, X2), if(X1, X2, mark X3) -> if(X1, X2, X3), if(X1, X2, active X3) -> if(X1, X2, X3), if(X1, mark X2, X3) -> if(X1, X2, X3), if(X1, active X2, X3) -> if(X1, X2, X3), if(mark X1, X2, X3) -> if(X1, X2, X3), if(active X1, X2, X3) -> if(X1, X2, X3), diff(X1, mark X2) -> diff(X1, X2), diff(X1, active X2) -> diff(X1, X2), diff(mark X1, X2) -> diff(X1, X2), diff(active X1, X2) -> diff(X1, X2)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2) = 0, [leq](x0, x1) = 0, [diff](x0, x1) = 0, [mark](x0) = x0, [active](x0) = x0 + 1, [p](x0) = 0, [s](x0) = 0, [0] = 1, [true] = 1, [false] = 1, [s#](x0) = x0 Strict: s# active X -> s# X 1 + 1X >= 0 + 1X s# mark X -> s# X 0 + 1X >= 0 + 1X Weak: diff(active X1, X2) -> diff(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 diff(mark X1, X2) -> diff(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 diff(X1, active X2) -> diff(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 diff(X1, mark X2) -> diff(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 if(active X1, X2, X3) -> if(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 if(mark X1, X2, X3) -> if(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 if(X1, active X2, X3) -> if(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 if(X1, mark X2, X3) -> if(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 if(X1, X2, active X3) -> if(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 if(X1, X2, mark X3) -> if(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 leq(active X1, X2) -> leq(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 leq(mark X1, X2) -> leq(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 leq(X1, active X2) -> leq(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 leq(X1, mark X2) -> leq(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 s active X -> s X 0 + 0X >= 0 + 0X s mark X -> s X 0 + 0X >= 0 + 0X p active X -> p X 0 + 0X >= 0 + 0X p mark X -> p X 0 + 0X >= 0 + 0X active diff(X, Y) -> mark if(leq(X, Y), 0(), s diff(p X, Y)) 1 + 0X + 0Y >= 0 + 0X + 0Y active if(false(), X, Y) -> mark Y 1 + 0X + 0Y >= 0 + 1Y active if(true(), X, Y) -> mark X 1 + 0X + 0Y >= 0 + 1X active leq(s X, s Y) -> mark leq(X, Y) 1 + 0X + 0Y >= 0 + 0X + 0Y active leq(s X, 0()) -> mark false() 1 + 0X >= 1 active leq(0(), Y) -> mark true() 1 + 0Y >= 1 active p s X -> mark X 1 + 0X >= 0 + 1X active p 0() -> mark 0() 1 >= 1 mark diff(X1, X2) -> active diff(mark X1, mark X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 mark if(X1, X2, X3) -> active if(mark X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 mark false() -> active false() 1 >= 2 mark leq(X1, X2) -> active leq(mark X1, mark X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 mark true() -> active true() 1 >= 2 mark s X -> active s mark X 0 + 0X >= 1 + 0X mark p X -> active p mark X 0 + 0X >= 1 + 0X mark 0() -> active 0() 1 >= 2 SCCS (1): Scc: {s# mark X -> s# X} SCC (1): Strict: {s# mark X -> s# X} Weak: { mark 0() -> active 0(), mark p X -> active p mark X, mark s X -> active s mark X, mark true() -> active true(), mark leq(X1, X2) -> active leq(mark X1, mark X2), mark false() -> active false(), mark if(X1, X2, X3) -> active if(mark X1, X2, X3), mark diff(X1, X2) -> active diff(mark X1, mark X2), active p 0() -> mark 0(), active p s X -> mark X, active leq(0(), Y) -> mark true(), active leq(s X, 0()) -> mark false(), active leq(s X, s Y) -> mark leq(X, Y), active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active diff(X, Y) -> mark if(leq(X, Y), 0(), s diff(p X, Y)), p mark X -> p X, p active X -> p X, s mark X -> s X, s active X -> s X, leq(X1, mark X2) -> leq(X1, X2), leq(X1, active X2) -> leq(X1, X2), leq(mark X1, X2) -> leq(X1, X2), leq(active X1, X2) -> leq(X1, X2), if(X1, X2, mark X3) -> if(X1, X2, X3), if(X1, X2, active X3) -> if(X1, X2, X3), if(X1, mark X2, X3) -> if(X1, X2, X3), if(X1, active X2, X3) -> if(X1, X2, X3), if(mark X1, X2, X3) -> if(X1, X2, X3), if(active X1, X2, X3) -> if(X1, X2, X3), diff(X1, mark X2) -> diff(X1, X2), diff(X1, active X2) -> diff(X1, X2), diff(mark X1, X2) -> diff(X1, X2), diff(active X1, X2) -> diff(X1, X2)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2) = x0 + 1, [leq](x0, x1) = 1, [diff](x0, x1) = 1, [mark](x0) = x0 + 1, [active](x0) = x0 + 1, [p](x0) = x0 + 1, [s](x0) = x0 + 1, [0] = 1, [true] = 1, [false] = 1, [s#](x0) = x0 Strict: s# mark X -> s# X 1 + 1X >= 0 + 1X Weak: diff(active X1, X2) -> diff(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 diff(mark X1, X2) -> diff(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 diff(X1, active X2) -> diff(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 diff(X1, mark X2) -> diff(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 if(active X1, X2, X3) -> if(X1, X2, X3) 2 + 1X1 + 0X2 + 0X3 >= 1 + 1X1 + 0X2 + 0X3 if(mark X1, X2, X3) -> if(X1, X2, X3) 2 + 1X1 + 0X2 + 0X3 >= 1 + 1X1 + 0X2 + 0X3 if(X1, active X2, X3) -> if(X1, X2, X3) 1 + 1X1 + 0X2 + 0X3 >= 1 + 1X1 + 0X2 + 0X3 if(X1, mark X2, X3) -> if(X1, X2, X3) 1 + 1X1 + 0X2 + 0X3 >= 1 + 1X1 + 0X2 + 0X3 if(X1, X2, active X3) -> if(X1, X2, X3) 1 + 1X1 + 0X2 + 0X3 >= 1 + 1X1 + 0X2 + 0X3 if(X1, X2, mark X3) -> if(X1, X2, X3) 1 + 1X1 + 0X2 + 0X3 >= 1 + 1X1 + 0X2 + 0X3 leq(active X1, X2) -> leq(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 leq(mark X1, X2) -> leq(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 leq(X1, active X2) -> leq(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 leq(X1, mark X2) -> leq(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 s active X -> s X 2 + 1X >= 1 + 1X s mark X -> s X 2 + 1X >= 1 + 1X p active X -> p X 2 + 1X >= 1 + 1X p mark X -> p X 2 + 1X >= 1 + 1X active diff(X, Y) -> mark if(leq(X, Y), 0(), s diff(p X, Y)) 2 + 0X + 0Y >= 3 + 0X + 0Y active if(false(), X, Y) -> mark Y 3 + 0X + 0Y >= 1 + 1Y active if(true(), X, Y) -> mark X 3 + 0X + 0Y >= 1 + 1X active leq(s X, s Y) -> mark leq(X, Y) 2 + 0X + 0Y >= 2 + 0X + 0Y active leq(s X, 0()) -> mark false() 2 + 0X >= 2 active leq(0(), Y) -> mark true() 2 + 0Y >= 2 active p s X -> mark X 3 + 1X >= 1 + 1X active p 0() -> mark 0() 3 >= 2 mark diff(X1, X2) -> active diff(mark X1, mark X2) 2 + 0X1 + 0X2 >= 2 + 0X1 + 0X2 mark if(X1, X2, X3) -> active if(mark X1, X2, X3) 2 + 1X1 + 0X2 + 0X3 >= 3 + 1X1 + 0X2 + 0X3 mark false() -> active false() 2 >= 2 mark leq(X1, X2) -> active leq(mark X1, mark X2) 2 + 0X1 + 0X2 >= 2 + 0X1 + 0X2 mark true() -> active true() 2 >= 2 mark s X -> active s mark X 2 + 1X >= 3 + 1X mark p X -> active p mark X 2 + 1X >= 3 + 1X mark 0() -> active 0() 2 >= 2 Qed SCC (2): Strict: { p# mark X -> p# X, p# active X -> p# X} Weak: { mark 0() -> active 0(), mark p X -> active p mark X, mark s X -> active s mark X, mark true() -> active true(), mark leq(X1, X2) -> active leq(mark X1, mark X2), mark false() -> active false(), mark if(X1, X2, X3) -> active if(mark X1, X2, X3), mark diff(X1, X2) -> active diff(mark X1, mark X2), active p 0() -> mark 0(), active p s X -> mark X, active leq(0(), Y) -> mark true(), active leq(s X, 0()) -> mark false(), active leq(s X, s Y) -> mark leq(X, Y), active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active diff(X, Y) -> mark if(leq(X, Y), 0(), s diff(p X, Y)), p mark X -> p X, p active X -> p X, s mark X -> s X, s active X -> s X, leq(X1, mark X2) -> leq(X1, X2), leq(X1, active X2) -> leq(X1, X2), leq(mark X1, X2) -> leq(X1, X2), leq(active X1, X2) -> leq(X1, X2), if(X1, X2, mark X3) -> if(X1, X2, X3), if(X1, X2, active X3) -> if(X1, X2, X3), if(X1, mark X2, X3) -> if(X1, X2, X3), if(X1, active X2, X3) -> if(X1, X2, X3), if(mark X1, X2, X3) -> if(X1, X2, X3), if(active X1, X2, X3) -> if(X1, X2, X3), diff(X1, mark X2) -> diff(X1, X2), diff(X1, active X2) -> diff(X1, X2), diff(mark X1, X2) -> diff(X1, X2), diff(active X1, X2) -> diff(X1, X2)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2) = 0, [leq](x0, x1) = 0, [diff](x0, x1) = 0, [mark](x0) = x0, [active](x0) = x0 + 1, [p](x0) = 0, [s](x0) = 0, [0] = 1, [true] = 1, [false] = 1, [p#](x0) = x0 Strict: p# active X -> p# X 1 + 1X >= 0 + 1X p# mark X -> p# X 0 + 1X >= 0 + 1X Weak: diff(active X1, X2) -> diff(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 diff(mark X1, X2) -> diff(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 diff(X1, active X2) -> diff(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 diff(X1, mark X2) -> diff(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 if(active X1, X2, X3) -> if(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 if(mark X1, X2, X3) -> if(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 if(X1, active X2, X3) -> if(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 if(X1, mark X2, X3) -> if(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 if(X1, X2, active X3) -> if(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 if(X1, X2, mark X3) -> if(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 leq(active X1, X2) -> leq(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 leq(mark X1, X2) -> leq(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 leq(X1, active X2) -> leq(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 leq(X1, mark X2) -> leq(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 s active X -> s X 0 + 0X >= 0 + 0X s mark X -> s X 0 + 0X >= 0 + 0X p active X -> p X 0 + 0X >= 0 + 0X p mark X -> p X 0 + 0X >= 0 + 0X active diff(X, Y) -> mark if(leq(X, Y), 0(), s diff(p X, Y)) 1 + 0X + 0Y >= 0 + 0X + 0Y active if(false(), X, Y) -> mark Y 1 + 0X + 0Y >= 0 + 1Y active if(true(), X, Y) -> mark X 1 + 0X + 0Y >= 0 + 1X active leq(s X, s Y) -> mark leq(X, Y) 1 + 0X + 0Y >= 0 + 0X + 0Y active leq(s X, 0()) -> mark false() 1 + 0X >= 1 active leq(0(), Y) -> mark true() 1 + 0Y >= 1 active p s X -> mark X 1 + 0X >= 0 + 1X active p 0() -> mark 0() 1 >= 1 mark diff(X1, X2) -> active diff(mark X1, mark X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 mark if(X1, X2, X3) -> active if(mark X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 mark false() -> active false() 1 >= 2 mark leq(X1, X2) -> active leq(mark X1, mark X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 mark true() -> active true() 1 >= 2 mark s X -> active s mark X 0 + 0X >= 1 + 0X mark p X -> active p mark X 0 + 0X >= 1 + 0X mark 0() -> active 0() 1 >= 2 SCCS (1): Scc: {p# mark X -> p# X} SCC (1): Strict: {p# mark X -> p# X} Weak: { mark 0() -> active 0(), mark p X -> active p mark X, mark s X -> active s mark X, mark true() -> active true(), mark leq(X1, X2) -> active leq(mark X1, mark X2), mark false() -> active false(), mark if(X1, X2, X3) -> active if(mark X1, X2, X3), mark diff(X1, X2) -> active diff(mark X1, mark X2), active p 0() -> mark 0(), active p s X -> mark X, active leq(0(), Y) -> mark true(), active leq(s X, 0()) -> mark false(), active leq(s X, s Y) -> mark leq(X, Y), active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active diff(X, Y) -> mark if(leq(X, Y), 0(), s diff(p X, Y)), p mark X -> p X, p active X -> p X, s mark X -> s X, s active X -> s X, leq(X1, mark X2) -> leq(X1, X2), leq(X1, active X2) -> leq(X1, X2), leq(mark X1, X2) -> leq(X1, X2), leq(active X1, X2) -> leq(X1, X2), if(X1, X2, mark X3) -> if(X1, X2, X3), if(X1, X2, active X3) -> if(X1, X2, X3), if(X1, mark X2, X3) -> if(X1, X2, X3), if(X1, active X2, X3) -> if(X1, X2, X3), if(mark X1, X2, X3) -> if(X1, X2, X3), if(active X1, X2, X3) -> if(X1, X2, X3), diff(X1, mark X2) -> diff(X1, X2), diff(X1, active X2) -> diff(X1, X2), diff(mark X1, X2) -> diff(X1, X2), diff(active X1, X2) -> diff(X1, X2)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2) = x0 + 1, [leq](x0, x1) = 1, [diff](x0, x1) = 1, [mark](x0) = x0 + 1, [active](x0) = x0 + 1, [p](x0) = x0 + 1, [s](x0) = x0 + 1, [0] = 1, [true] = 1, [false] = 1, [p#](x0) = x0 Strict: p# mark X -> p# X 1 + 1X >= 0 + 1X Weak: diff(active X1, X2) -> diff(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 diff(mark X1, X2) -> diff(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 diff(X1, active X2) -> diff(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 diff(X1, mark X2) -> diff(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 if(active X1, X2, X3) -> if(X1, X2, X3) 2 + 1X1 + 0X2 + 0X3 >= 1 + 1X1 + 0X2 + 0X3 if(mark X1, X2, X3) -> if(X1, X2, X3) 2 + 1X1 + 0X2 + 0X3 >= 1 + 1X1 + 0X2 + 0X3 if(X1, active X2, X3) -> if(X1, X2, X3) 1 + 1X1 + 0X2 + 0X3 >= 1 + 1X1 + 0X2 + 0X3 if(X1, mark X2, X3) -> if(X1, X2, X3) 1 + 1X1 + 0X2 + 0X3 >= 1 + 1X1 + 0X2 + 0X3 if(X1, X2, active X3) -> if(X1, X2, X3) 1 + 1X1 + 0X2 + 0X3 >= 1 + 1X1 + 0X2 + 0X3 if(X1, X2, mark X3) -> if(X1, X2, X3) 1 + 1X1 + 0X2 + 0X3 >= 1 + 1X1 + 0X2 + 0X3 leq(active X1, X2) -> leq(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 leq(mark X1, X2) -> leq(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 leq(X1, active X2) -> leq(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 leq(X1, mark X2) -> leq(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 s active X -> s X 2 + 1X >= 1 + 1X s mark X -> s X 2 + 1X >= 1 + 1X p active X -> p X 2 + 1X >= 1 + 1X p mark X -> p X 2 + 1X >= 1 + 1X active diff(X, Y) -> mark if(leq(X, Y), 0(), s diff(p X, Y)) 2 + 0X + 0Y >= 3 + 0X + 0Y active if(false(), X, Y) -> mark Y 3 + 0X + 0Y >= 1 + 1Y active if(true(), X, Y) -> mark X 3 + 0X + 0Y >= 1 + 1X active leq(s X, s Y) -> mark leq(X, Y) 2 + 0X + 0Y >= 2 + 0X + 0Y active leq(s X, 0()) -> mark false() 2 + 0X >= 2 active leq(0(), Y) -> mark true() 2 + 0Y >= 2 active p s X -> mark X 3 + 1X >= 1 + 1X active p 0() -> mark 0() 3 >= 2 mark diff(X1, X2) -> active diff(mark X1, mark X2) 2 + 0X1 + 0X2 >= 2 + 0X1 + 0X2 mark if(X1, X2, X3) -> active if(mark X1, X2, X3) 2 + 1X1 + 0X2 + 0X3 >= 3 + 1X1 + 0X2 + 0X3 mark false() -> active false() 2 >= 2 mark leq(X1, X2) -> active leq(mark X1, mark X2) 2 + 0X1 + 0X2 >= 2 + 0X1 + 0X2 mark true() -> active true() 2 >= 2 mark s X -> active s mark X 2 + 1X >= 3 + 1X mark p X -> active p mark X 2 + 1X >= 3 + 1X mark 0() -> active 0() 2 >= 2 Qed