MAYBE Time: 1.101985 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)} UR: { 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)) } EDG: { (active# p 0() -> mark# 0(), mark# 0() -> active# 0()) (active# leq(s X, 0()) -> mark# false(), mark# false() -> active# false()) (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, 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# 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# 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) (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()) (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#(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)) (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#(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# 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# 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# 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# 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# true() -> active# true()) } STATUS: arrows: 0.850222 SCCS (6): 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# 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 s X -> mark# X, 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 (17): 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# 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 s X -> mark# X, 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)} Open 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)} Open 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)} Open 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)} Open 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)} Open 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)} Open