MAYBE Time: 0.154557 TRS: { mark if(X1, X2, X3) -> active if(mark X1, X2, X3), mark zero X -> active zero mark X, mark s X -> active s mark X, mark 0() -> active 0(), mark prod(X1, X2) -> active prod(mark X1, mark X2), mark fact X -> active fact mark X, mark p X -> active p mark X, mark add(X1, X2) -> active add(mark X1, mark X2), mark true() -> active true(), mark false() -> active false(), 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), zero mark X -> zero X, zero active X -> zero X, s mark X -> s X, s active X -> s X, prod(X1, mark X2) -> prod(X1, X2), prod(X1, active X2) -> prod(X1, X2), prod(mark X1, X2) -> prod(X1, X2), prod(active X1, X2) -> prod(X1, X2), fact mark X -> fact X, fact active X -> fact X, p mark X -> p X, p active X -> p X, active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active zero s X -> mark false(), active zero 0() -> mark true(), active prod(s X, Y) -> mark add(Y, prod(X, Y)), active prod(0(), X) -> mark 0(), active fact X -> mark if(zero X, s 0(), prod(X, fact p X)), active p s X -> mark X, active add(s X, Y) -> mark s add(X, Y), active add(0(), X) -> mark X, add(X1, mark X2) -> add(X1, X2), add(X1, active X2) -> add(X1, X2), add(mark X1, X2) -> add(X1, X2), add(active X1, X2) -> add(X1, X2)} DP: DP: { mark# if(X1, X2, X3) -> mark# X1, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3), mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), mark# zero X -> mark# X, mark# zero X -> zero# mark X, mark# zero X -> active# zero mark X, mark# s X -> mark# X, mark# s X -> s# mark X, mark# s X -> active# s mark X, mark# 0() -> active# 0(), mark# prod(X1, X2) -> mark# X1, mark# prod(X1, X2) -> mark# X2, mark# prod(X1, X2) -> prod#(mark X1, mark X2), mark# prod(X1, X2) -> active# prod(mark X1, mark X2), mark# fact X -> mark# X, mark# fact X -> fact# mark X, mark# fact X -> active# fact mark X, mark# p X -> mark# X, mark# p X -> p# mark X, mark# p X -> active# p mark X, mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X2, mark# add(X1, X2) -> active# add(mark X1, mark X2), mark# add(X1, X2) -> add#(mark X1, mark X2), mark# true() -> active# true(), mark# false() -> active# false(), 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), zero# mark X -> zero# X, zero# active X -> zero# X, s# mark X -> s# X, s# active X -> s# X, prod#(X1, mark X2) -> prod#(X1, X2), prod#(X1, active X2) -> prod#(X1, X2), prod#(mark X1, X2) -> prod#(X1, X2), prod#(active X1, X2) -> prod#(X1, X2), fact# mark X -> fact# X, fact# active X -> fact# X, p# mark X -> p# X, p# active X -> p# X, active# if(true(), X, Y) -> mark# X, active# if(false(), X, Y) -> mark# Y, active# zero s X -> mark# false(), active# zero 0() -> mark# true(), active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), active# prod(s X, Y) -> prod#(X, Y), active# prod(s X, Y) -> add#(Y, prod(X, Y)), active# prod(0(), X) -> mark# 0(), active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), active# fact X -> if#(zero X, s 0(), prod(X, fact p X)), active# fact X -> zero# X, active# fact X -> s# 0(), active# fact X -> prod#(X, fact p X), active# fact X -> fact# p X, active# fact X -> p# X, active# p s X -> mark# X, active# add(s X, Y) -> mark# s add(X, Y), active# add(s X, Y) -> s# add(X, Y), active# add(s X, Y) -> add#(X, Y), active# add(0(), X) -> mark# X, add#(X1, mark X2) -> add#(X1, X2), add#(X1, active X2) -> add#(X1, X2), add#(mark X1, X2) -> add#(X1, X2), add#(active X1, X2) -> add#(X1, X2)} TRS: { mark if(X1, X2, X3) -> active if(mark X1, X2, X3), mark zero X -> active zero mark X, mark s X -> active s mark X, mark 0() -> active 0(), mark prod(X1, X2) -> active prod(mark X1, mark X2), mark fact X -> active fact mark X, mark p X -> active p mark X, mark add(X1, X2) -> active add(mark X1, mark X2), mark true() -> active true(), mark false() -> active false(), 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), zero mark X -> zero X, zero active X -> zero X, s mark X -> s X, s active X -> s X, prod(X1, mark X2) -> prod(X1, X2), prod(X1, active X2) -> prod(X1, X2), prod(mark X1, X2) -> prod(X1, X2), prod(active X1, X2) -> prod(X1, X2), fact mark X -> fact X, fact active X -> fact X, p mark X -> p X, p active X -> p X, active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active zero s X -> mark false(), active zero 0() -> mark true(), active prod(s X, Y) -> mark add(Y, prod(X, Y)), active prod(0(), X) -> mark 0(), active fact X -> mark if(zero X, s 0(), prod(X, fact p X)), active p s X -> mark X, active add(s X, Y) -> mark s add(X, Y), active add(0(), X) -> mark X, add(X1, mark X2) -> add(X1, X2), add(X1, active X2) -> add(X1, X2), add(mark X1, X2) -> add(X1, X2), add(active X1, X2) -> add(X1, X2)} UR: { mark if(X1, X2, X3) -> active if(mark X1, X2, X3), mark zero X -> active zero mark X, mark s X -> active s mark X, mark 0() -> active 0(), mark prod(X1, X2) -> active prod(mark X1, mark X2), mark fact X -> active fact mark X, mark p X -> active p mark X, mark add(X1, X2) -> active add(mark X1, mark X2), mark true() -> active true(), mark false() -> active false(), 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), zero mark X -> zero X, zero active X -> zero X, s mark X -> s X, s active X -> s X, prod(X1, mark X2) -> prod(X1, X2), prod(X1, active X2) -> prod(X1, X2), prod(mark X1, X2) -> prod(X1, X2), prod(active X1, X2) -> prod(X1, X2), fact mark X -> fact X, fact active X -> fact X, p mark X -> p X, p active X -> p X, active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active zero s X -> mark false(), active zero 0() -> mark true(), active prod(s X, Y) -> mark add(Y, prod(X, Y)), active prod(0(), X) -> mark 0(), active fact X -> mark if(zero X, s 0(), prod(X, fact p X)), active p s X -> mark X, active add(s X, Y) -> mark s add(X, Y), active add(0(), X) -> mark X, add(X1, mark X2) -> add(X1, X2), add(X1, active X2) -> add(X1, X2), add(mark X1, X2) -> add(X1, X2), add(active X1, X2) -> add(X1, X2), a(x, y) -> x, a(x, y) -> y} EDG: { (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# active X -> p# X) (mark# p X -> p# mark X, p# mark X -> p# X) (mark# zero X -> mark# X, mark# false() -> active# false()) (mark# zero X -> mark# X, mark# true() -> active# true()) (mark# zero X -> mark# X, mark# add(X1, X2) -> add#(mark X1, mark X2)) (mark# zero X -> mark# X, mark# add(X1, X2) -> active# add(mark X1, mark X2)) (mark# zero X -> mark# X, mark# add(X1, X2) -> mark# X2) (mark# zero X -> mark# X, mark# add(X1, X2) -> mark# X1) (mark# zero X -> mark# X, mark# p X -> active# p mark X) (mark# zero X -> mark# X, mark# p X -> p# mark X) (mark# zero X -> mark# X, mark# p X -> mark# X) (mark# zero X -> mark# X, mark# fact X -> active# fact mark X) (mark# zero X -> mark# X, mark# fact X -> fact# mark X) (mark# zero X -> mark# X, mark# fact X -> mark# X) (mark# zero X -> mark# X, mark# prod(X1, X2) -> active# prod(mark X1, mark X2)) (mark# zero X -> mark# X, mark# prod(X1, X2) -> prod#(mark X1, mark X2)) (mark# zero X -> mark# X, mark# prod(X1, X2) -> mark# X2) (mark# zero X -> mark# X, mark# prod(X1, X2) -> mark# X1) (mark# zero X -> mark# X, mark# 0() -> active# 0()) (mark# zero X -> mark# X, mark# s X -> active# s mark X) (mark# zero X -> mark# X, mark# s X -> s# mark X) (mark# zero X -> mark# X, mark# s X -> mark# X) (mark# zero X -> mark# X, mark# zero X -> active# zero mark X) (mark# zero X -> mark# X, mark# zero X -> zero# mark X) (mark# zero X -> mark# X, mark# zero X -> mark# X) (mark# zero X -> mark# X, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (mark# zero X -> mark# X, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (mark# zero X -> mark# X, mark# if(X1, X2, X3) -> mark# X1) (mark# fact X -> mark# X, mark# false() -> active# false()) (mark# fact X -> mark# X, mark# true() -> active# true()) (mark# fact X -> mark# X, mark# add(X1, X2) -> add#(mark X1, mark X2)) (mark# fact X -> mark# X, mark# add(X1, X2) -> active# add(mark X1, mark X2)) (mark# fact X -> mark# X, mark# add(X1, X2) -> mark# X2) (mark# fact X -> mark# X, mark# add(X1, X2) -> mark# X1) (mark# fact X -> mark# X, mark# p X -> active# p mark X) (mark# fact X -> mark# X, mark# p X -> p# mark X) (mark# fact X -> mark# X, mark# p X -> mark# X) (mark# fact X -> mark# X, mark# fact X -> active# fact mark X) (mark# fact X -> mark# X, mark# fact X -> fact# mark X) (mark# fact X -> mark# X, mark# fact X -> mark# X) (mark# fact X -> mark# X, mark# prod(X1, X2) -> active# prod(mark X1, mark X2)) (mark# fact X -> mark# X, mark# prod(X1, X2) -> prod#(mark X1, mark X2)) (mark# fact X -> mark# X, mark# prod(X1, X2) -> mark# X2) (mark# fact X -> mark# X, mark# prod(X1, X2) -> mark# X1) (mark# fact X -> mark# X, mark# 0() -> active# 0()) (mark# fact X -> mark# X, mark# s X -> active# s mark X) (mark# fact X -> mark# X, mark# s X -> s# mark X) (mark# fact X -> mark# X, mark# s X -> mark# X) (mark# fact X -> mark# X, mark# zero X -> active# zero mark X) (mark# fact X -> mark# X, mark# zero X -> zero# mark X) (mark# fact X -> mark# X, mark# zero X -> mark# X) (mark# fact X -> mark# X, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (mark# fact X -> mark# X, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (mark# fact X -> mark# X, mark# if(X1, X2, X3) -> mark# X1) (zero# mark X -> zero# X, zero# active X -> zero# X) (zero# mark X -> zero# X, zero# mark X -> zero# X) (s# mark X -> s# X, s# active X -> s# X) (s# mark X -> s# X, s# mark X -> s# X) (fact# mark X -> fact# X, fact# active X -> fact# X) (fact# mark X -> fact# X, fact# mark X -> fact# X) (p# mark X -> p# X, p# active X -> p# X) (p# mark X -> p# X, p# mark X -> p# X) (active# if(true(), X, Y) -> mark# X, mark# false() -> active# false()) (active# if(true(), X, Y) -> mark# X, mark# true() -> active# true()) (active# if(true(), X, Y) -> mark# X, mark# add(X1, X2) -> add#(mark X1, mark X2)) (active# if(true(), X, Y) -> mark# X, mark# add(X1, X2) -> active# add(mark X1, mark X2)) (active# if(true(), X, Y) -> mark# X, mark# add(X1, X2) -> mark# X2) (active# if(true(), X, Y) -> mark# X, mark# add(X1, X2) -> mark# X1) (active# if(true(), X, Y) -> mark# X, mark# p X -> active# p 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 -> mark# X) (active# if(true(), X, Y) -> mark# X, mark# fact X -> active# fact mark X) (active# if(true(), X, Y) -> mark# X, mark# fact X -> fact# mark X) (active# if(true(), X, Y) -> mark# X, mark# fact X -> mark# X) (active# if(true(), X, Y) -> mark# X, mark# prod(X1, X2) -> active# prod(mark X1, mark X2)) (active# if(true(), X, Y) -> mark# X, mark# prod(X1, X2) -> prod#(mark X1, mark X2)) (active# if(true(), X, Y) -> mark# X, mark# prod(X1, X2) -> mark# X2) (active# if(true(), X, Y) -> mark# X, mark# prod(X1, X2) -> mark# X1) (active# if(true(), X, Y) -> mark# X, mark# 0() -> active# 0()) (active# if(true(), X, Y) -> mark# X, mark# s X -> active# s mark X) (active# if(true(), X, Y) -> mark# X, mark# s X -> s# mark X) (active# if(true(), X, Y) -> mark# X, mark# s X -> mark# X) (active# if(true(), X, Y) -> mark# X, mark# zero X -> active# zero mark X) (active# if(true(), X, Y) -> mark# X, mark# zero X -> zero# mark X) (active# if(true(), X, Y) -> mark# X, mark# zero X -> mark# X) (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) -> if#(mark X1, X2, X3)) (active# if(true(), X, Y) -> mark# X, mark# if(X1, X2, X3) -> mark# X1) (active# fact X -> p# X, p# active X -> p# X) (active# fact X -> p# X, p# mark X -> p# X) (active# add(0(), X) -> mark# X, mark# false() -> active# false()) (active# add(0(), X) -> mark# X, mark# true() -> active# true()) (active# add(0(), X) -> mark# X, mark# add(X1, X2) -> add#(mark X1, mark X2)) (active# add(0(), X) -> mark# X, mark# add(X1, X2) -> active# add(mark X1, mark X2)) (active# add(0(), X) -> mark# X, mark# add(X1, X2) -> mark# X2) (active# add(0(), X) -> mark# X, mark# add(X1, X2) -> mark# X1) (active# add(0(), X) -> mark# X, mark# p X -> active# p mark X) (active# add(0(), X) -> mark# X, mark# p X -> p# mark X) (active# add(0(), X) -> mark# X, mark# p X -> mark# X) (active# add(0(), X) -> mark# X, mark# fact X -> active# fact mark X) (active# add(0(), X) -> mark# X, mark# fact X -> fact# mark X) (active# add(0(), X) -> mark# X, mark# fact X -> mark# X) (active# add(0(), X) -> mark# X, mark# prod(X1, X2) -> active# prod(mark X1, mark X2)) (active# add(0(), X) -> mark# X, mark# prod(X1, X2) -> prod#(mark X1, mark X2)) (active# add(0(), X) -> mark# X, mark# prod(X1, X2) -> mark# X2) (active# add(0(), X) -> mark# X, mark# prod(X1, X2) -> mark# X1) (active# add(0(), X) -> mark# X, mark# 0() -> active# 0()) (active# add(0(), X) -> mark# X, mark# s X -> active# s mark X) (active# add(0(), X) -> mark# X, mark# s X -> s# mark X) (active# add(0(), X) -> mark# X, mark# s X -> mark# X) (active# add(0(), X) -> mark# X, mark# zero X -> active# zero mark X) (active# add(0(), X) -> mark# X, mark# zero X -> zero# mark X) (active# add(0(), X) -> mark# X, mark# zero X -> mark# X) (active# add(0(), X) -> mark# X, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (active# add(0(), X) -> mark# X, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (active# add(0(), X) -> mark# X, mark# if(X1, X2, X3) -> mark# X1) (mark# zero X -> active# zero mark X, active# add(0(), X) -> mark# X) (mark# zero X -> active# zero mark X, active# add(s X, Y) -> add#(X, Y)) (mark# zero X -> active# zero mark X, active# add(s X, Y) -> s# add(X, Y)) (mark# zero X -> active# zero mark X, active# add(s X, Y) -> mark# s add(X, Y)) (mark# zero X -> active# zero mark X, active# p s X -> mark# X) (mark# zero X -> active# zero mark X, active# fact X -> p# X) (mark# zero X -> active# zero mark X, active# fact X -> fact# p X) (mark# zero X -> active# zero mark X, active# fact X -> prod#(X, fact p X)) (mark# zero X -> active# zero mark X, active# fact X -> s# 0()) (mark# zero X -> active# zero mark X, active# fact X -> zero# X) (mark# zero X -> active# zero mark X, active# fact X -> if#(zero X, s 0(), prod(X, fact p X))) (mark# zero X -> active# zero mark X, active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X))) (mark# zero X -> active# zero mark X, active# prod(0(), X) -> mark# 0()) (mark# zero X -> active# zero mark X, active# prod(s X, Y) -> add#(Y, prod(X, Y))) (mark# zero X -> active# zero mark X, active# prod(s X, Y) -> prod#(X, Y)) (mark# zero X -> active# zero mark X, active# prod(s X, Y) -> mark# add(Y, prod(X, Y))) (mark# zero X -> active# zero mark X, active# zero 0() -> mark# true()) (mark# zero X -> active# zero mark X, active# zero s X -> mark# false()) (mark# zero X -> active# zero mark X, active# if(false(), X, Y) -> mark# Y) (mark# zero X -> active# zero mark X, active# if(true(), X, Y) -> mark# X) (mark# fact X -> active# fact mark X, active# add(0(), X) -> mark# X) (mark# fact X -> active# fact mark X, active# add(s X, Y) -> add#(X, Y)) (mark# fact X -> active# fact mark X, active# add(s X, Y) -> s# add(X, Y)) (mark# fact X -> active# fact mark X, active# add(s X, Y) -> mark# s add(X, Y)) (mark# fact X -> active# fact mark X, active# p s X -> mark# X) (mark# fact X -> active# fact mark X, active# fact X -> p# X) (mark# fact X -> active# fact mark X, active# fact X -> fact# p X) (mark# fact X -> active# fact mark X, active# fact X -> prod#(X, fact p X)) (mark# fact X -> active# fact mark X, active# fact X -> s# 0()) (mark# fact X -> active# fact mark X, active# fact X -> zero# X) (mark# fact X -> active# fact mark X, active# fact X -> if#(zero X, s 0(), prod(X, fact p X))) (mark# fact X -> active# fact mark X, active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X))) (mark# fact X -> active# fact mark X, active# prod(0(), X) -> mark# 0()) (mark# fact X -> active# fact mark X, active# prod(s X, Y) -> add#(Y, prod(X, Y))) (mark# fact X -> active# fact mark X, active# prod(s X, Y) -> prod#(X, Y)) (mark# fact X -> active# fact mark X, active# prod(s X, Y) -> mark# add(Y, prod(X, Y))) (mark# fact X -> active# fact mark X, active# zero 0() -> mark# true()) (mark# fact X -> active# fact mark X, active# zero s X -> mark# false()) (mark# fact X -> active# fact mark X, active# if(false(), X, Y) -> mark# Y) (mark# fact X -> active# fact mark X, active# if(true(), X, Y) -> mark# X) (active# add(s X, Y) -> mark# s add(X, Y), mark# false() -> active# false()) (active# add(s X, Y) -> mark# s add(X, Y), mark# true() -> active# true()) (active# add(s X, Y) -> mark# s add(X, Y), mark# add(X1, X2) -> add#(mark X1, mark X2)) (active# add(s X, Y) -> mark# s add(X, Y), mark# add(X1, X2) -> active# add(mark X1, mark X2)) (active# add(s X, Y) -> mark# s add(X, Y), mark# add(X1, X2) -> mark# X2) (active# add(s X, Y) -> mark# s add(X, Y), mark# add(X1, X2) -> mark# X1) (active# add(s X, Y) -> mark# s add(X, Y), mark# p X -> active# p mark X) (active# add(s X, Y) -> mark# s add(X, Y), mark# p X -> p# mark X) (active# add(s X, Y) -> mark# s add(X, Y), mark# p X -> mark# X) (active# add(s X, Y) -> mark# s add(X, Y), mark# fact X -> active# fact mark X) (active# add(s X, Y) -> mark# s add(X, Y), mark# fact X -> fact# mark X) (active# add(s X, Y) -> mark# s add(X, Y), mark# fact X -> mark# X) (active# add(s X, Y) -> mark# s add(X, Y), mark# prod(X1, X2) -> active# prod(mark X1, mark X2)) (active# add(s X, Y) -> mark# s add(X, Y), mark# prod(X1, X2) -> prod#(mark X1, mark X2)) (active# add(s X, Y) -> mark# s add(X, Y), mark# prod(X1, X2) -> mark# X2) (active# add(s X, Y) -> mark# s add(X, Y), mark# prod(X1, X2) -> mark# X1) (active# add(s X, Y) -> mark# s add(X, Y), mark# 0() -> active# 0()) (active# add(s X, Y) -> mark# s add(X, Y), mark# s X -> active# s mark X) (active# add(s X, Y) -> mark# s add(X, Y), mark# s X -> s# mark X) (active# add(s X, Y) -> mark# s add(X, Y), mark# s X -> mark# X) (active# add(s X, Y) -> mark# s add(X, Y), mark# zero X -> active# zero mark X) (active# add(s X, Y) -> mark# s add(X, Y), mark# zero X -> zero# mark X) (active# add(s X, Y) -> mark# s add(X, Y), mark# zero X -> mark# X) (active# add(s X, Y) -> mark# s add(X, Y), mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (active# add(s X, Y) -> mark# s add(X, Y), mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (active# add(s X, Y) -> mark# s add(X, Y), mark# if(X1, X2, X3) -> mark# X1) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# add(0(), X) -> mark# X) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# add(s X, Y) -> add#(X, Y)) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# add(s X, Y) -> s# add(X, Y)) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# add(s X, Y) -> mark# s add(X, Y)) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# p s X -> mark# X) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# fact X -> p# X) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# fact X -> fact# p X) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# fact X -> prod#(X, fact p X)) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# fact X -> s# 0()) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# fact X -> zero# X) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# fact X -> if#(zero X, s 0(), prod(X, fact p X))) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X))) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# prod(0(), X) -> mark# 0()) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# prod(s X, Y) -> add#(Y, prod(X, Y))) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# prod(s X, Y) -> prod#(X, Y)) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# prod(s X, Y) -> mark# add(Y, prod(X, Y))) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# zero 0() -> mark# true()) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# zero s X -> mark# false()) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# if(false(), X, Y) -> mark# Y) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# if(true(), X, Y) -> mark# X) (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# false() -> active# false()) (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# true() -> active# true()) (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# add(X1, X2) -> add#(mark X1, mark X2)) (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# add(X1, X2) -> active# add(mark X1, mark X2)) (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# add(X1, X2) -> mark# X2) (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# add(X1, X2) -> mark# X1) (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# p X -> active# p mark X) (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# p X -> p# mark X) (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# p X -> mark# X) (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# fact X -> active# fact mark X) (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# fact X -> fact# mark X) (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# fact X -> mark# X) (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# prod(X1, X2) -> active# prod(mark X1, mark X2)) (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# prod(X1, X2) -> prod#(mark X1, mark X2)) (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# prod(X1, X2) -> mark# X2) (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# prod(X1, X2) -> mark# X1) (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# 0() -> active# 0()) (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# s X -> active# s mark X) (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# s X -> s# mark X) (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# s X -> mark# X) (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# zero X -> active# zero mark X) (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# zero X -> zero# mark X) (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# zero X -> mark# X) (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# if(X1, X2, X3) -> mark# X1) (mark# add(X1, X2) -> add#(mark X1, mark X2), add#(active X1, X2) -> add#(X1, X2)) (mark# add(X1, X2) -> add#(mark X1, mark X2), add#(mark X1, X2) -> add#(X1, X2)) (mark# add(X1, X2) -> add#(mark X1, mark X2), add#(X1, active X2) -> add#(X1, X2)) (mark# add(X1, X2) -> add#(mark X1, mark X2), add#(X1, mark X2) -> add#(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)) (mark# if(X1, X2, X3) -> mark# X1, mark# false() -> active# false()) (mark# if(X1, X2, X3) -> mark# X1, mark# true() -> active# true()) (mark# if(X1, X2, X3) -> mark# X1, mark# add(X1, X2) -> add#(mark X1, mark X2)) (mark# if(X1, X2, X3) -> mark# X1, mark# add(X1, X2) -> active# add(mark X1, mark X2)) (mark# if(X1, X2, X3) -> mark# X1, mark# add(X1, X2) -> mark# X2) (mark# if(X1, X2, X3) -> mark# X1, mark# add(X1, X2) -> mark# X1) (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# p X -> mark# X) (mark# if(X1, X2, X3) -> mark# X1, mark# fact X -> active# fact mark X) (mark# if(X1, X2, X3) -> mark# X1, mark# fact X -> fact# mark X) (mark# if(X1, X2, X3) -> mark# X1, mark# fact X -> mark# X) (mark# if(X1, X2, X3) -> mark# X1, mark# prod(X1, X2) -> active# prod(mark X1, mark X2)) (mark# if(X1, X2, X3) -> mark# X1, mark# prod(X1, X2) -> prod#(mark X1, mark X2)) (mark# if(X1, X2, X3) -> mark# X1, mark# prod(X1, X2) -> mark# X2) (mark# if(X1, X2, X3) -> mark# X1, mark# prod(X1, X2) -> mark# X1) (mark# if(X1, X2, X3) -> mark# X1, mark# 0() -> active# 0()) (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# s X -> mark# X) (mark# if(X1, X2, X3) -> mark# X1, mark# zero X -> active# zero mark X) (mark# if(X1, X2, X3) -> mark# X1, mark# zero X -> zero# mark X) (mark# if(X1, X2, X3) -> mark# X1, mark# zero X -> mark# X) (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# if(X1, X2, X3) -> mark# X1) (mark# add(X1, X2) -> mark# X1, mark# false() -> active# false()) (mark# add(X1, X2) -> mark# X1, mark# true() -> active# true()) (mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> add#(mark X1, mark X2)) (mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> active# add(mark X1, mark X2)) (mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X2) (mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X1) (mark# add(X1, X2) -> mark# X1, mark# p X -> active# p mark X) (mark# add(X1, X2) -> mark# X1, mark# p X -> p# mark X) (mark# add(X1, X2) -> mark# X1, mark# p X -> mark# X) (mark# add(X1, X2) -> mark# X1, mark# fact X -> active# fact mark X) (mark# add(X1, X2) -> mark# X1, mark# fact X -> fact# mark X) (mark# add(X1, X2) -> mark# X1, mark# fact X -> mark# X) (mark# add(X1, X2) -> mark# X1, mark# prod(X1, X2) -> active# prod(mark X1, mark X2)) (mark# add(X1, X2) -> mark# X1, mark# prod(X1, X2) -> prod#(mark X1, mark X2)) (mark# add(X1, X2) -> mark# X1, mark# prod(X1, X2) -> mark# X2) (mark# add(X1, X2) -> mark# X1, mark# prod(X1, X2) -> mark# X1) (mark# add(X1, X2) -> mark# X1, mark# 0() -> active# 0()) (mark# add(X1, X2) -> mark# X1, mark# s X -> active# s mark X) (mark# add(X1, X2) -> mark# X1, mark# s X -> s# mark X) (mark# add(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# add(X1, X2) -> mark# X1, mark# zero X -> active# zero mark X) (mark# add(X1, X2) -> mark# X1, mark# zero X -> zero# mark X) (mark# add(X1, X2) -> mark# X1, mark# zero X -> mark# X) (mark# add(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (mark# add(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (mark# add(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> mark# X1) (prod#(X1, mark X2) -> prod#(X1, X2), prod#(active X1, X2) -> prod#(X1, X2)) (prod#(X1, mark X2) -> prod#(X1, X2), prod#(mark X1, X2) -> prod#(X1, X2)) (prod#(X1, mark X2) -> prod#(X1, X2), prod#(X1, active X2) -> prod#(X1, X2)) (prod#(X1, mark X2) -> prod#(X1, X2), prod#(X1, mark X2) -> prod#(X1, X2)) (prod#(mark X1, X2) -> prod#(X1, X2), prod#(active X1, X2) -> prod#(X1, X2)) (prod#(mark X1, X2) -> prod#(X1, X2), prod#(mark X1, X2) -> prod#(X1, X2)) (prod#(mark X1, X2) -> prod#(X1, X2), prod#(X1, active X2) -> prod#(X1, X2)) (prod#(mark X1, X2) -> prod#(X1, X2), prod#(X1, mark X2) -> prod#(X1, X2)) (add#(X1, mark X2) -> add#(X1, X2), add#(active X1, X2) -> add#(X1, X2)) (add#(X1, mark X2) -> add#(X1, X2), add#(mark X1, X2) -> add#(X1, X2)) (add#(X1, mark X2) -> add#(X1, X2), add#(X1, active X2) -> add#(X1, X2)) (add#(X1, mark X2) -> add#(X1, X2), add#(X1, mark X2) -> add#(X1, X2)) (add#(mark X1, X2) -> add#(X1, X2), add#(active X1, X2) -> add#(X1, X2)) (add#(mark X1, X2) -> add#(X1, X2), add#(mark X1, X2) -> add#(X1, X2)) (add#(mark X1, X2) -> add#(X1, X2), add#(X1, active X2) -> add#(X1, X2)) (add#(mark X1, X2) -> add#(X1, X2), add#(X1, mark X2) -> add#(X1, X2)) (mark# 0() -> active# 0(), active# add(0(), X) -> mark# X) (mark# 0() -> active# 0(), active# add(s X, Y) -> add#(X, Y)) (mark# 0() -> active# 0(), active# add(s X, Y) -> s# add(X, Y)) (mark# 0() -> active# 0(), active# add(s X, Y) -> mark# s add(X, Y)) (mark# 0() -> active# 0(), active# p s X -> mark# X) (mark# 0() -> active# 0(), active# fact X -> p# X) (mark# 0() -> active# 0(), active# fact X -> fact# p X) (mark# 0() -> active# 0(), active# fact X -> prod#(X, fact p X)) (mark# 0() -> active# 0(), active# fact X -> s# 0()) (mark# 0() -> active# 0(), active# fact X -> zero# X) (mark# 0() -> active# 0(), active# fact X -> if#(zero X, s 0(), prod(X, fact p X))) (mark# 0() -> active# 0(), active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X))) (mark# 0() -> active# 0(), active# prod(0(), X) -> mark# 0()) (mark# 0() -> active# 0(), active# prod(s X, Y) -> add#(Y, prod(X, Y))) (mark# 0() -> active# 0(), active# prod(s X, Y) -> prod#(X, Y)) (mark# 0() -> active# 0(), active# prod(s X, Y) -> mark# add(Y, prod(X, Y))) (mark# 0() -> active# 0(), active# zero 0() -> mark# true()) (mark# 0() -> active# 0(), active# zero s X -> mark# false()) (mark# 0() -> active# 0(), active# if(false(), X, Y) -> mark# Y) (mark# 0() -> active# 0(), active# if(true(), X, Y) -> mark# X) (mark# false() -> active# false(), active# add(0(), X) -> mark# X) (mark# false() -> active# false(), active# add(s X, Y) -> add#(X, Y)) (mark# false() -> active# false(), active# add(s X, Y) -> s# add(X, Y)) (mark# false() -> active# false(), active# add(s X, Y) -> mark# s add(X, Y)) (mark# false() -> active# false(), active# p s X -> mark# X) (mark# false() -> active# false(), active# fact X -> p# X) (mark# false() -> active# false(), active# fact X -> fact# p X) (mark# false() -> active# false(), active# fact X -> prod#(X, fact p X)) (mark# false() -> active# false(), active# fact X -> s# 0()) (mark# false() -> active# false(), active# fact X -> zero# X) (mark# false() -> active# false(), active# fact X -> if#(zero X, s 0(), prod(X, fact p X))) (mark# false() -> active# false(), active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X))) (mark# false() -> active# false(), active# prod(0(), X) -> mark# 0()) (mark# false() -> active# false(), active# prod(s X, Y) -> add#(Y, prod(X, Y))) (mark# false() -> active# false(), active# prod(s X, Y) -> prod#(X, Y)) (mark# false() -> active# false(), active# prod(s X, Y) -> mark# add(Y, prod(X, Y))) (mark# false() -> active# false(), active# zero 0() -> mark# true()) (mark# false() -> active# false(), active# zero s X -> mark# false()) (mark# false() -> active# false(), active# if(false(), X, Y) -> mark# Y) (mark# false() -> active# false(), active# if(true(), X, Y) -> mark# X) (active# zero 0() -> mark# true(), mark# false() -> active# false()) (active# zero 0() -> mark# true(), mark# true() -> active# true()) (active# zero 0() -> mark# true(), mark# add(X1, X2) -> add#(mark X1, mark X2)) (active# zero 0() -> mark# true(), mark# add(X1, X2) -> active# add(mark X1, mark X2)) (active# zero 0() -> mark# true(), mark# add(X1, X2) -> mark# X2) (active# zero 0() -> mark# true(), mark# add(X1, X2) -> mark# X1) (active# zero 0() -> mark# true(), mark# p X -> active# p mark X) (active# zero 0() -> mark# true(), mark# p X -> p# mark X) (active# zero 0() -> mark# true(), mark# p X -> mark# X) (active# zero 0() -> mark# true(), mark# fact X -> active# fact mark X) (active# zero 0() -> mark# true(), mark# fact X -> fact# mark X) (active# zero 0() -> mark# true(), mark# fact X -> mark# X) (active# zero 0() -> mark# true(), mark# prod(X1, X2) -> active# prod(mark X1, mark X2)) (active# zero 0() -> mark# true(), mark# prod(X1, X2) -> prod#(mark X1, mark X2)) (active# zero 0() -> mark# true(), mark# prod(X1, X2) -> mark# X2) (active# zero 0() -> mark# true(), mark# prod(X1, X2) -> mark# X1) (active# zero 0() -> mark# true(), mark# 0() -> active# 0()) (active# zero 0() -> mark# true(), mark# s X -> active# s mark X) (active# zero 0() -> mark# true(), mark# s X -> s# mark X) (active# zero 0() -> mark# true(), mark# s X -> mark# X) (active# zero 0() -> mark# true(), mark# zero X -> active# zero mark X) (active# zero 0() -> mark# true(), mark# zero X -> zero# mark X) (active# zero 0() -> mark# true(), mark# zero X -> mark# X) (active# zero 0() -> mark# true(), mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (active# zero 0() -> mark# true(), mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (active# zero 0() -> mark# true(), mark# if(X1, X2, X3) -> mark# X1) (active# fact X -> s# 0(), s# active X -> s# X) (active# fact X -> s# 0(), s# mark X -> s# X) (mark# add(X1, X2) -> mark# X2, mark# false() -> active# false()) (mark# add(X1, X2) -> mark# X2, mark# true() -> active# true()) (mark# add(X1, X2) -> mark# X2, mark# add(X1, X2) -> add#(mark X1, mark X2)) (mark# add(X1, X2) -> mark# X2, mark# add(X1, X2) -> active# add(mark X1, mark X2)) (mark# add(X1, X2) -> mark# X2, mark# add(X1, X2) -> mark# X2) (mark# add(X1, X2) -> mark# X2, mark# add(X1, X2) -> mark# X1) (mark# add(X1, X2) -> mark# X2, mark# p X -> active# p mark X) (mark# add(X1, X2) -> mark# X2, mark# p X -> p# mark X) (mark# add(X1, X2) -> mark# X2, mark# p X -> mark# X) (mark# add(X1, X2) -> mark# X2, mark# fact X -> active# fact mark X) (mark# add(X1, X2) -> mark# X2, mark# fact X -> fact# mark X) (mark# add(X1, X2) -> mark# X2, mark# fact X -> mark# X) (mark# add(X1, X2) -> mark# X2, mark# prod(X1, X2) -> active# prod(mark X1, mark X2)) (mark# add(X1, X2) -> mark# X2, mark# prod(X1, X2) -> prod#(mark X1, mark X2)) (mark# add(X1, X2) -> mark# X2, mark# prod(X1, X2) -> mark# X2) (mark# add(X1, X2) -> mark# X2, mark# prod(X1, X2) -> mark# X1) (mark# add(X1, X2) -> mark# X2, mark# 0() -> active# 0()) (mark# add(X1, X2) -> mark# X2, mark# s X -> active# s mark X) (mark# add(X1, X2) -> mark# X2, mark# s X -> s# mark X) (mark# add(X1, X2) -> mark# X2, mark# s X -> mark# X) (mark# add(X1, X2) -> mark# X2, mark# zero X -> active# zero mark X) (mark# add(X1, X2) -> mark# X2, mark# zero X -> zero# mark X) (mark# add(X1, X2) -> mark# X2, mark# zero X -> mark# X) (mark# add(X1, X2) -> mark# X2, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (mark# add(X1, X2) -> mark# X2, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (mark# add(X1, X2) -> mark# X2, mark# if(X1, X2, X3) -> mark# X1) (active# add(s X, Y) -> s# add(X, Y), s# active X -> s# X) (active# add(s X, Y) -> s# add(X, Y), s# mark X -> s# X) (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# false() -> active# false()) (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# true() -> active# true()) (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# add(X1, X2) -> add#(mark X1, mark X2)) (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# add(X1, X2) -> active# add(mark X1, mark X2)) (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# add(X1, X2) -> mark# X2) (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# add(X1, X2) -> mark# X1) (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# p X -> active# p mark X) (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# p X -> p# mark X) (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# p X -> mark# X) (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# fact X -> active# fact mark X) (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# fact X -> fact# mark X) (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# fact X -> mark# X) (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# prod(X1, X2) -> active# prod(mark X1, mark X2)) (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# prod(X1, X2) -> prod#(mark X1, mark X2)) (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# prod(X1, X2) -> mark# X2) (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# prod(X1, X2) -> mark# X1) (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# 0() -> active# 0()) (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# s X -> active# s mark X) (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# s X -> s# mark X) (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# s X -> mark# X) (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# zero X -> active# zero mark X) (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# zero X -> zero# mark X) (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# zero X -> mark# X) (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# if(X1, X2, X3) -> mark# X1) (active# add(s X, Y) -> add#(X, Y), add#(active X1, X2) -> add#(X1, X2)) (active# add(s X, Y) -> add#(X, Y), add#(mark X1, X2) -> add#(X1, X2)) (active# add(s X, Y) -> add#(X, Y), add#(X1, active X2) -> add#(X1, X2)) (active# add(s X, Y) -> add#(X, Y), add#(X1, mark X2) -> add#(X1, X2)) (active# prod(s X, Y) -> prod#(X, Y), prod#(X1, mark X2) -> prod#(X1, X2)) (active# prod(s X, Y) -> prod#(X, Y), prod#(X1, active X2) -> prod#(X1, X2)) (active# prod(s X, Y) -> prod#(X, Y), prod#(mark X1, X2) -> prod#(X1, X2)) (active# prod(s X, Y) -> prod#(X, Y), prod#(active X1, X2) -> prod#(X1, X2)) (active# fact X -> prod#(X, fact p X), prod#(X1, mark X2) -> prod#(X1, X2)) (active# fact X -> prod#(X, fact p X), prod#(X1, active X2) -> prod#(X1, X2)) (active# fact X -> prod#(X, fact p X), prod#(mark X1, X2) -> prod#(X1, X2)) (active# fact X -> prod#(X, fact p X), prod#(active X1, X2) -> prod#(X1, X2)) (active# fact X -> if#(zero X, s 0(), prod(X, fact p X)), if#(X1, X2, mark X3) -> if#(X1, X2, X3)) (active# fact X -> if#(zero X, s 0(), prod(X, fact p X)), if#(X1, X2, active X3) -> if#(X1, X2, X3)) (active# fact X -> if#(zero X, s 0(), prod(X, fact p X)), if#(X1, mark X2, X3) -> if#(X1, X2, X3)) (active# fact X -> if#(zero X, s 0(), prod(X, fact p X)), if#(X1, active X2, X3) -> if#(X1, X2, X3)) (active# fact X -> if#(zero X, s 0(), prod(X, fact p X)), if#(mark X1, X2, X3) -> if#(X1, X2, X3)) (active# fact X -> if#(zero X, s 0(), prod(X, fact p X)), if#(active X1, X2, X3) -> if#(X1, X2, X3)) (mark# prod(X1, X2) -> mark# X2, mark# if(X1, X2, X3) -> mark# X1) (mark# prod(X1, X2) -> mark# X2, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (mark# prod(X1, X2) -> mark# X2, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (mark# prod(X1, X2) -> mark# X2, mark# zero X -> mark# X) (mark# prod(X1, X2) -> mark# X2, mark# zero X -> zero# mark X) (mark# prod(X1, X2) -> mark# X2, mark# zero X -> active# zero mark X) (mark# prod(X1, X2) -> mark# X2, mark# s X -> mark# X) (mark# prod(X1, X2) -> mark# X2, mark# s X -> s# mark X) (mark# prod(X1, X2) -> mark# X2, mark# s X -> active# s mark X) (mark# prod(X1, X2) -> mark# X2, mark# 0() -> active# 0()) (mark# prod(X1, X2) -> mark# X2, mark# prod(X1, X2) -> mark# X1) (mark# prod(X1, X2) -> mark# X2, mark# prod(X1, X2) -> mark# X2) (mark# prod(X1, X2) -> mark# X2, mark# prod(X1, X2) -> prod#(mark X1, mark X2)) (mark# prod(X1, X2) -> mark# X2, mark# prod(X1, X2) -> active# prod(mark X1, mark X2)) (mark# prod(X1, X2) -> mark# X2, mark# fact X -> mark# X) (mark# prod(X1, X2) -> mark# X2, mark# fact X -> fact# mark X) (mark# prod(X1, X2) -> mark# X2, mark# fact X -> active# fact mark X) (mark# prod(X1, X2) -> mark# X2, mark# p X -> mark# X) (mark# prod(X1, X2) -> mark# X2, mark# p X -> p# mark X) (mark# prod(X1, X2) -> mark# X2, mark# p X -> active# p mark X) (mark# prod(X1, X2) -> mark# X2, mark# add(X1, X2) -> mark# X1) (mark# prod(X1, X2) -> mark# X2, mark# add(X1, X2) -> mark# X2) (mark# prod(X1, X2) -> mark# X2, mark# add(X1, X2) -> active# add(mark X1, mark X2)) (mark# prod(X1, X2) -> mark# X2, mark# add(X1, X2) -> add#(mark X1, mark X2)) (mark# prod(X1, X2) -> mark# X2, mark# true() -> active# true()) (mark# prod(X1, X2) -> mark# X2, mark# false() -> active# false()) (active# prod(0(), X) -> mark# 0(), mark# if(X1, X2, X3) -> mark# X1) (active# prod(0(), X) -> mark# 0(), mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (active# prod(0(), X) -> mark# 0(), mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (active# prod(0(), X) -> mark# 0(), mark# zero X -> mark# X) (active# prod(0(), X) -> mark# 0(), mark# zero X -> zero# mark X) (active# prod(0(), X) -> mark# 0(), mark# zero X -> active# zero mark X) (active# prod(0(), X) -> mark# 0(), mark# s X -> mark# X) (active# prod(0(), X) -> mark# 0(), mark# s X -> s# mark X) (active# prod(0(), X) -> mark# 0(), mark# s X -> active# s mark X) (active# prod(0(), X) -> mark# 0(), mark# 0() -> active# 0()) (active# prod(0(), X) -> mark# 0(), mark# prod(X1, X2) -> mark# X1) (active# prod(0(), X) -> mark# 0(), mark# prod(X1, X2) -> mark# X2) (active# prod(0(), X) -> mark# 0(), mark# prod(X1, X2) -> prod#(mark X1, mark X2)) (active# prod(0(), X) -> mark# 0(), mark# prod(X1, X2) -> active# prod(mark X1, mark X2)) (active# prod(0(), X) -> mark# 0(), mark# fact X -> mark# X) (active# prod(0(), X) -> mark# 0(), mark# fact X -> fact# mark X) (active# prod(0(), X) -> mark# 0(), mark# fact X -> active# fact mark X) (active# prod(0(), X) -> mark# 0(), mark# p X -> mark# X) (active# prod(0(), X) -> mark# 0(), mark# p X -> p# mark X) (active# prod(0(), X) -> mark# 0(), mark# p X -> active# p mark X) (active# prod(0(), X) -> mark# 0(), mark# add(X1, X2) -> mark# X1) (active# prod(0(), X) -> mark# 0(), mark# add(X1, X2) -> mark# X2) (active# prod(0(), X) -> mark# 0(), mark# add(X1, X2) -> active# add(mark X1, mark X2)) (active# prod(0(), X) -> mark# 0(), mark# add(X1, X2) -> add#(mark X1, mark X2)) (active# prod(0(), X) -> mark# 0(), mark# true() -> active# true()) (active# prod(0(), X) -> mark# 0(), mark# false() -> active# false()) (active# zero s X -> mark# false(), mark# if(X1, X2, X3) -> mark# X1) (active# zero s X -> mark# false(), mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (active# zero s X -> mark# false(), mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (active# zero s X -> mark# false(), mark# zero X -> mark# X) (active# zero s X -> mark# false(), mark# zero X -> zero# mark X) (active# zero s X -> mark# false(), mark# zero X -> active# zero mark X) (active# zero s X -> mark# false(), mark# s X -> mark# X) (active# zero s X -> mark# false(), mark# s X -> s# mark X) (active# zero s X -> mark# false(), mark# s X -> active# s mark X) (active# zero s X -> mark# false(), mark# 0() -> active# 0()) (active# zero s X -> mark# false(), mark# prod(X1, X2) -> mark# X1) (active# zero s X -> mark# false(), mark# prod(X1, X2) -> mark# X2) (active# zero s X -> mark# false(), mark# prod(X1, X2) -> prod#(mark X1, mark X2)) (active# zero s X -> mark# false(), mark# prod(X1, X2) -> active# prod(mark X1, mark X2)) (active# zero s X -> mark# false(), mark# fact X -> mark# X) (active# zero s X -> mark# false(), mark# fact X -> fact# mark X) (active# zero s X -> mark# false(), mark# fact X -> active# fact mark X) (active# zero s X -> mark# false(), mark# p X -> mark# X) (active# zero s X -> mark# false(), mark# p X -> p# mark X) (active# zero s X -> mark# false(), mark# p X -> active# p mark X) (active# zero s X -> mark# false(), mark# add(X1, X2) -> mark# X1) (active# zero s X -> mark# false(), mark# add(X1, X2) -> mark# X2) (active# zero s X -> mark# false(), mark# add(X1, X2) -> active# add(mark X1, mark X2)) (active# zero s X -> mark# false(), mark# add(X1, X2) -> add#(mark X1, mark X2)) (active# zero s X -> mark# false(), mark# true() -> active# true()) (active# zero s X -> mark# false(), mark# false() -> active# false()) (mark# true() -> active# true(), active# if(true(), X, Y) -> mark# X) (mark# true() -> active# true(), active# if(false(), X, Y) -> mark# Y) (mark# true() -> active# true(), active# zero s X -> mark# false()) (mark# true() -> active# true(), active# zero 0() -> mark# true()) (mark# true() -> active# true(), active# prod(s X, Y) -> mark# add(Y, prod(X, Y))) (mark# true() -> active# true(), active# prod(s X, Y) -> prod#(X, Y)) (mark# true() -> active# true(), active# prod(s X, Y) -> add#(Y, prod(X, Y))) (mark# true() -> active# true(), active# prod(0(), X) -> mark# 0()) (mark# true() -> active# true(), active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X))) (mark# true() -> active# true(), active# fact X -> if#(zero X, s 0(), prod(X, fact p X))) (mark# true() -> active# true(), active# fact X -> zero# X) (mark# true() -> active# true(), active# fact X -> s# 0()) (mark# true() -> active# true(), active# fact X -> prod#(X, fact p X)) (mark# true() -> active# true(), active# fact X -> fact# p X) (mark# true() -> active# true(), active# fact X -> p# X) (mark# true() -> active# true(), active# p s X -> mark# X) (mark# true() -> active# true(), active# add(s X, Y) -> mark# s add(X, Y)) (mark# true() -> active# true(), active# add(s X, Y) -> s# add(X, Y)) (mark# true() -> active# true(), active# add(s X, Y) -> add#(X, Y)) (mark# true() -> active# true(), active# add(0(), X) -> mark# X) (add#(active X1, X2) -> add#(X1, X2), add#(X1, mark X2) -> add#(X1, X2)) (add#(active X1, X2) -> add#(X1, X2), add#(X1, active X2) -> add#(X1, X2)) (add#(active X1, X2) -> add#(X1, X2), add#(mark X1, X2) -> add#(X1, X2)) (add#(active X1, X2) -> add#(X1, X2), add#(active X1, X2) -> add#(X1, X2)) (add#(X1, active X2) -> add#(X1, X2), add#(X1, mark X2) -> add#(X1, X2)) (add#(X1, active X2) -> add#(X1, X2), add#(X1, active X2) -> add#(X1, X2)) (add#(X1, active X2) -> add#(X1, X2), add#(mark X1, X2) -> add#(X1, X2)) (add#(X1, active X2) -> add#(X1, X2), add#(active X1, X2) -> add#(X1, X2)) (prod#(active X1, X2) -> prod#(X1, X2), prod#(X1, mark X2) -> prod#(X1, X2)) (prod#(active X1, X2) -> prod#(X1, X2), prod#(X1, active X2) -> prod#(X1, X2)) (prod#(active X1, X2) -> prod#(X1, X2), prod#(mark X1, X2) -> prod#(X1, X2)) (prod#(active X1, X2) -> prod#(X1, X2), prod#(active X1, X2) -> prod#(X1, X2)) (prod#(X1, active X2) -> prod#(X1, X2), prod#(X1, mark X2) -> prod#(X1, X2)) (prod#(X1, active X2) -> prod#(X1, X2), prod#(X1, active X2) -> prod#(X1, X2)) (prod#(X1, active X2) -> prod#(X1, X2), prod#(mark X1, X2) -> prod#(X1, X2)) (prod#(X1, active X2) -> prod#(X1, X2), prod#(active X1, X2) -> prod#(X1, X2)) (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# if(false(), X, Y) -> mark# Y) (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# zero s X -> mark# false()) (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# zero 0() -> mark# true()) (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# prod(s X, Y) -> mark# add(Y, prod(X, Y))) (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# prod(s X, Y) -> prod#(X, Y)) (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# prod(s X, Y) -> add#(Y, prod(X, Y))) (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# prod(0(), X) -> mark# 0()) (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X))) (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# fact X -> if#(zero X, s 0(), prod(X, fact p X))) (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# fact X -> zero# X) (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# fact X -> s# 0()) (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# fact X -> prod#(X, fact p X)) (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# fact X -> fact# p X) (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# fact X -> p# X) (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# add(s X, Y) -> mark# s add(X, Y)) (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# add(s X, Y) -> s# add(X, Y)) (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# add(s X, Y) -> add#(X, Y)) (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# add(0(), X) -> mark# X) (mark# prod(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> mark# X1) (mark# prod(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (mark# prod(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (mark# prod(X1, X2) -> mark# X1, mark# zero X -> mark# X) (mark# prod(X1, X2) -> mark# X1, mark# zero X -> zero# mark X) (mark# prod(X1, X2) -> mark# X1, mark# zero X -> active# zero mark X) (mark# prod(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# prod(X1, X2) -> mark# X1, mark# s X -> s# mark X) (mark# prod(X1, X2) -> mark# X1, mark# s X -> active# s mark X) (mark# prod(X1, X2) -> mark# X1, mark# 0() -> active# 0()) (mark# prod(X1, X2) -> mark# X1, mark# prod(X1, X2) -> mark# X1) (mark# prod(X1, X2) -> mark# X1, mark# prod(X1, X2) -> mark# X2) (mark# prod(X1, X2) -> mark# X1, mark# prod(X1, X2) -> prod#(mark X1, mark X2)) (mark# prod(X1, X2) -> mark# X1, mark# prod(X1, X2) -> active# prod(mark X1, mark X2)) (mark# prod(X1, X2) -> mark# X1, mark# fact X -> mark# X) (mark# prod(X1, X2) -> mark# X1, mark# fact X -> fact# mark X) (mark# prod(X1, X2) -> mark# X1, mark# fact X -> active# fact mark X) (mark# prod(X1, X2) -> mark# X1, mark# p X -> mark# X) (mark# prod(X1, X2) -> mark# X1, mark# p X -> p# mark X) (mark# prod(X1, X2) -> mark# X1, mark# p X -> active# p mark X) (mark# prod(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X1) (mark# prod(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X2) (mark# prod(X1, X2) -> mark# X1, mark# add(X1, X2) -> active# add(mark X1, mark X2)) (mark# prod(X1, X2) -> mark# X1, mark# add(X1, X2) -> add#(mark X1, mark X2)) (mark# prod(X1, X2) -> mark# X1, mark# true() -> active# true()) (mark# prod(X1, X2) -> mark# X1, mark# false() -> active# false()) (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)) (mark# prod(X1, X2) -> prod#(mark X1, mark X2), prod#(X1, mark X2) -> prod#(X1, X2)) (mark# prod(X1, X2) -> prod#(mark X1, mark X2), prod#(X1, active X2) -> prod#(X1, X2)) (mark# prod(X1, X2) -> prod#(mark X1, mark X2), prod#(mark X1, X2) -> prod#(X1, X2)) (mark# prod(X1, X2) -> prod#(mark X1, mark X2), prod#(active X1, X2) -> prod#(X1, X2)) (active# if(false(), X, Y) -> mark# Y, mark# if(X1, X2, X3) -> 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# zero X -> mark# X) (active# if(false(), X, Y) -> mark# Y, mark# zero X -> zero# mark X) (active# if(false(), X, Y) -> mark# Y, mark# zero X -> active# zero mark X) (active# if(false(), X, Y) -> mark# Y, mark# s X -> mark# X) (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# 0() -> active# 0()) (active# if(false(), X, Y) -> mark# Y, mark# prod(X1, X2) -> mark# X1) (active# if(false(), X, Y) -> mark# Y, mark# prod(X1, X2) -> mark# X2) (active# if(false(), X, Y) -> mark# Y, mark# prod(X1, X2) -> prod#(mark X1, mark X2)) (active# if(false(), X, Y) -> mark# Y, mark# prod(X1, X2) -> active# prod(mark X1, mark X2)) (active# if(false(), X, Y) -> mark# Y, mark# fact X -> mark# X) (active# if(false(), X, Y) -> mark# Y, mark# fact X -> fact# mark X) (active# if(false(), X, Y) -> mark# Y, mark# fact X -> active# fact mark X) (active# if(false(), X, Y) -> mark# Y, mark# p 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# add(X1, X2) -> mark# X1) (active# if(false(), X, Y) -> mark# Y, mark# add(X1, X2) -> mark# X2) (active# if(false(), X, Y) -> mark# Y, mark# add(X1, X2) -> active# add(mark X1, mark X2)) (active# if(false(), X, Y) -> mark# Y, mark# add(X1, X2) -> add#(mark X1, mark X2)) (active# if(false(), X, Y) -> mark# Y, mark# true() -> active# true()) (active# if(false(), X, Y) -> mark# Y, mark# false() -> active# false()) (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# if(true(), X, Y) -> mark# X) (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# if(false(), X, Y) -> mark# Y) (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# zero s X -> mark# false()) (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# zero 0() -> mark# true()) (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# prod(s X, Y) -> mark# add(Y, prod(X, Y))) (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# prod(s X, Y) -> prod#(X, Y)) (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# prod(s X, Y) -> add#(Y, prod(X, Y))) (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# prod(0(), X) -> mark# 0()) (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X))) (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# fact X -> if#(zero X, s 0(), prod(X, fact p X))) (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# fact X -> zero# X) (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# fact X -> s# 0()) (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# fact X -> prod#(X, fact p X)) (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# fact X -> fact# p X) (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# fact X -> p# X) (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# p s X -> mark# X) (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# add(s X, Y) -> mark# s add(X, Y)) (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# add(s X, Y) -> s# add(X, Y)) (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# add(s X, Y) -> add#(X, Y)) (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# add(0(), X) -> mark# X) (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# zero s X -> mark# false()) (mark# p X -> active# p mark X, active# zero 0() -> mark# true()) (mark# p X -> active# p mark X, active# prod(s X, Y) -> mark# add(Y, prod(X, Y))) (mark# p X -> active# p mark X, active# prod(s X, Y) -> prod#(X, Y)) (mark# p X -> active# p mark X, active# prod(s X, Y) -> add#(Y, prod(X, Y))) (mark# p X -> active# p mark X, active# prod(0(), X) -> mark# 0()) (mark# p X -> active# p mark X, active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X))) (mark# p X -> active# p mark X, active# fact X -> if#(zero X, s 0(), prod(X, fact p X))) (mark# p X -> active# p mark X, active# fact X -> zero# X) (mark# p X -> active# p mark X, active# fact X -> s# 0()) (mark# p X -> active# p mark X, active# fact X -> prod#(X, fact p X)) (mark# p X -> active# p mark X, active# fact X -> fact# p X) (mark# p X -> active# p mark X, active# fact X -> p# X) (mark# p X -> active# p mark X, active# p s X -> mark# X) (mark# p X -> active# p mark X, active# add(s X, Y) -> mark# s add(X, Y)) (mark# p X -> active# p mark X, active# add(s X, Y) -> s# add(X, Y)) (mark# p X -> active# p mark X, active# add(s X, Y) -> add#(X, Y)) (mark# p X -> active# p mark X, active# add(0(), X) -> mark# X) (mark# s X -> active# s mark X, active# if(true(), X, Y) -> mark# X) (mark# s X -> active# s mark X, active# if(false(), X, Y) -> mark# Y) (mark# s X -> active# s mark X, active# zero s X -> mark# false()) (mark# s X -> active# s mark X, active# zero 0() -> mark# true()) (mark# s X -> active# s mark X, active# prod(s X, Y) -> mark# add(Y, prod(X, Y))) (mark# s X -> active# s mark X, active# prod(s X, Y) -> prod#(X, Y)) (mark# s X -> active# s mark X, active# prod(s X, Y) -> add#(Y, prod(X, Y))) (mark# s X -> active# s mark X, active# prod(0(), X) -> mark# 0()) (mark# s X -> active# s mark X, active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X))) (mark# s X -> active# s mark X, active# fact X -> if#(zero X, s 0(), prod(X, fact p X))) (mark# s X -> active# s mark X, active# fact X -> zero# X) (mark# s X -> active# s mark X, active# fact X -> s# 0()) (mark# s X -> active# s mark X, active# fact X -> prod#(X, fact p X)) (mark# s X -> active# s mark X, active# fact X -> fact# p X) (mark# s X -> active# s mark X, active# fact X -> p# X) (mark# s X -> active# s mark X, active# p s X -> mark# X) (mark# s X -> active# s mark X, active# add(s X, Y) -> mark# s add(X, Y)) (mark# s X -> active# s mark X, active# add(s X, Y) -> s# add(X, Y)) (mark# s X -> active# s mark X, active# add(s X, Y) -> add#(X, Y)) (mark# s X -> active# s mark X, active# add(0(), X) -> mark# X) (active# prod(s X, Y) -> add#(Y, prod(X, Y)), add#(X1, mark X2) -> add#(X1, X2)) (active# prod(s X, Y) -> add#(Y, prod(X, Y)), add#(X1, active X2) -> add#(X1, X2)) (active# prod(s X, Y) -> add#(Y, prod(X, Y)), add#(mark X1, X2) -> add#(X1, X2)) (active# prod(s X, Y) -> add#(Y, prod(X, Y)), add#(active X1, X2) -> add#(X1, X2)) (active# p s X -> mark# X, mark# if(X1, X2, X3) -> mark# X1) (active# p s X -> mark# X, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (active# p s X -> mark# X, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (active# p s X -> mark# X, mark# zero X -> mark# X) (active# p s X -> mark# X, mark# zero X -> zero# mark X) (active# p s X -> mark# X, mark# zero X -> active# zero mark X) (active# p s X -> mark# X, mark# s X -> mark# X) (active# p s X -> mark# X, mark# s X -> s# mark X) (active# p s X -> mark# X, mark# s X -> active# s mark X) (active# p s X -> mark# X, mark# 0() -> active# 0()) (active# p s X -> mark# X, mark# prod(X1, X2) -> mark# X1) (active# p s X -> mark# X, mark# prod(X1, X2) -> mark# X2) (active# p s X -> mark# X, mark# prod(X1, X2) -> prod#(mark X1, mark X2)) (active# p s X -> mark# X, mark# prod(X1, X2) -> active# prod(mark X1, mark X2)) (active# p s X -> mark# X, mark# fact X -> mark# X) (active# p s X -> mark# X, mark# fact X -> fact# mark X) (active# p s X -> mark# X, mark# fact X -> active# fact mark X) (active# p s X -> mark# X, mark# p X -> mark# X) (active# p s X -> mark# X, mark# p X -> p# mark X) (active# p s X -> mark# X, mark# p X -> active# p mark X) (active# p s X -> mark# X, mark# add(X1, X2) -> mark# X1) (active# p s X -> mark# X, mark# add(X1, X2) -> mark# X2) (active# p s X -> mark# X, mark# add(X1, X2) -> active# add(mark X1, mark X2)) (active# p s X -> mark# X, mark# add(X1, X2) -> add#(mark X1, mark X2)) (active# p s X -> mark# X, mark# true() -> active# true()) (active# p s X -> mark# X, mark# false() -> active# false()) (active# fact X -> zero# X, zero# mark X -> zero# X) (active# fact X -> zero# X, zero# active X -> zero# X) (p# active X -> p# X, p# mark X -> p# X) (p# active X -> p# X, p# active X -> p# X) (fact# active X -> fact# X, fact# mark X -> fact# X) (fact# active X -> fact# X, fact# active X -> fact# X) (s# active X -> s# X, s# mark X -> s# X) (s# active X -> s# X, s# active X -> s# X) (zero# active X -> zero# X, zero# mark X -> zero# X) (zero# active X -> zero# X, zero# active X -> zero# X) (mark# p X -> mark# X, mark# if(X1, X2, X3) -> mark# X1) (mark# p X -> mark# X, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (mark# p X -> mark# X, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (mark# p X -> mark# X, mark# zero X -> mark# X) (mark# p X -> mark# X, mark# zero X -> zero# mark X) (mark# p X -> mark# X, mark# zero X -> active# zero mark X) (mark# p X -> mark# X, mark# s X -> mark# X) (mark# p X -> mark# X, mark# s X -> s# mark X) (mark# p X -> mark# X, mark# s X -> active# s mark X) (mark# p X -> mark# X, mark# 0() -> active# 0()) (mark# p X -> mark# X, mark# prod(X1, X2) -> mark# X1) (mark# p X -> mark# X, mark# prod(X1, X2) -> mark# X2) (mark# p X -> mark# X, mark# prod(X1, X2) -> prod#(mark X1, mark X2)) (mark# p X -> mark# X, mark# prod(X1, X2) -> active# prod(mark X1, mark X2)) (mark# p X -> mark# X, mark# fact X -> mark# X) (mark# p X -> mark# X, mark# fact X -> fact# mark X) (mark# p X -> mark# X, mark# fact X -> active# fact mark X) (mark# p X -> mark# X, mark# p X -> mark# X) (mark# p X -> mark# X, mark# p X -> p# mark X) (mark# p X -> mark# X, mark# p X -> active# p mark X) (mark# p X -> mark# X, mark# add(X1, X2) -> mark# X1) (mark# p X -> mark# X, mark# add(X1, X2) -> mark# X2) (mark# p X -> mark# X, mark# add(X1, X2) -> active# add(mark X1, mark X2)) (mark# p X -> mark# X, mark# add(X1, X2) -> add#(mark X1, mark X2)) (mark# p X -> mark# X, mark# true() -> active# true()) (mark# p X -> mark# X, mark# false() -> active# false()) (mark# s X -> mark# X, mark# if(X1, X2, X3) -> 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# zero X -> mark# X) (mark# s X -> mark# X, mark# zero X -> zero# mark X) (mark# s X -> mark# X, mark# zero X -> active# zero mark X) (mark# s X -> mark# X, mark# s X -> mark# X) (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# 0() -> active# 0()) (mark# s X -> mark# X, mark# prod(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# prod(X1, X2) -> mark# X2) (mark# s X -> mark# X, mark# prod(X1, X2) -> prod#(mark X1, mark X2)) (mark# s X -> mark# X, mark# prod(X1, X2) -> active# prod(mark X1, mark X2)) (mark# s X -> mark# X, mark# fact X -> mark# X) (mark# s X -> mark# X, mark# fact X -> fact# mark X) (mark# s X -> mark# X, mark# fact X -> active# fact mark X) (mark# s X -> mark# X, mark# p 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# add(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# add(X1, X2) -> mark# X2) (mark# s X -> mark# X, mark# add(X1, X2) -> active# add(mark X1, mark X2)) (mark# s X -> mark# X, mark# add(X1, X2) -> add#(mark X1, mark X2)) (mark# s X -> mark# X, mark# true() -> active# true()) (mark# s X -> mark# X, mark# false() -> active# false()) (active# fact X -> fact# p X, fact# mark X -> fact# X) (active# fact X -> fact# p X, fact# active X -> fact# X) (mark# fact X -> fact# mark X, fact# mark X -> fact# X) (mark# fact X -> fact# mark X, fact# active X -> fact# X) (mark# zero X -> zero# mark X, zero# mark X -> zero# X) (mark# zero X -> zero# mark X, zero# active X -> zero# X) } EDG: { (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# active X -> p# X) (mark# p X -> p# mark X, p# mark X -> p# X) (mark# zero X -> mark# X, mark# false() -> active# false()) (mark# zero X -> mark# X, mark# true() -> active# true()) (mark# zero X -> mark# X, mark# add(X1, X2) -> add#(mark X1, mark X2)) (mark# zero X -> mark# X, mark# add(X1, X2) -> active# add(mark X1, mark X2)) (mark# zero X -> mark# X, mark# add(X1, X2) -> mark# X2) (mark# zero X -> mark# X, mark# add(X1, X2) -> mark# X1) (mark# zero X -> mark# X, mark# p X -> active# p mark X) (mark# zero X -> mark# X, mark# p X -> p# mark X) (mark# zero X -> mark# X, mark# p X -> mark# X) (mark# zero X -> mark# X, mark# fact X -> active# fact mark X) (mark# zero X -> mark# X, mark# fact X -> fact# mark X) (mark# zero X -> mark# X, mark# fact X -> mark# X) (mark# zero X -> mark# X, mark# prod(X1, X2) -> active# prod(mark X1, mark X2)) (mark# zero X -> mark# X, mark# prod(X1, X2) -> prod#(mark X1, mark X2)) (mark# zero X -> mark# X, mark# prod(X1, X2) -> mark# X2) (mark# zero X -> mark# X, mark# prod(X1, X2) -> mark# X1) (mark# zero X -> mark# X, mark# 0() -> active# 0()) (mark# zero X -> mark# X, mark# s X -> active# s mark X) (mark# zero X -> mark# X, mark# s X -> s# mark X) (mark# zero X -> mark# X, mark# s X -> mark# X) (mark# zero X -> mark# X, mark# zero X -> active# zero mark X) (mark# zero X -> mark# X, mark# zero X -> zero# mark X) (mark# zero X -> mark# X, mark# zero X -> mark# X) (mark# zero X -> mark# X, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (mark# zero X -> mark# X, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (mark# zero X -> mark# X, mark# if(X1, X2, X3) -> mark# X1) (mark# fact X -> mark# X, mark# false() -> active# false()) (mark# fact X -> mark# X, mark# true() -> active# true()) (mark# fact X -> mark# X, mark# add(X1, X2) -> add#(mark X1, mark X2)) (mark# fact X -> mark# X, mark# add(X1, X2) -> active# add(mark X1, mark X2)) (mark# fact X -> mark# X, mark# add(X1, X2) -> mark# X2) (mark# fact X -> mark# X, mark# add(X1, X2) -> mark# X1) (mark# fact X -> mark# X, mark# p X -> active# p mark X) (mark# fact X -> mark# X, mark# p X -> p# mark X) (mark# fact X -> mark# X, mark# p X -> mark# X) (mark# fact X -> mark# X, mark# fact X -> active# fact mark X) (mark# fact X -> mark# X, mark# fact X -> fact# mark X) (mark# fact X -> mark# X, mark# fact X -> mark# X) (mark# fact X -> mark# X, mark# prod(X1, X2) -> active# prod(mark X1, mark X2)) (mark# fact X -> mark# X, mark# prod(X1, X2) -> prod#(mark X1, mark X2)) (mark# fact X -> mark# X, mark# prod(X1, X2) -> mark# X2) (mark# fact X -> mark# X, mark# prod(X1, X2) -> mark# X1) (mark# fact X -> mark# X, mark# 0() -> active# 0()) (mark# fact X -> mark# X, mark# s X -> active# s mark X) (mark# fact X -> mark# X, mark# s X -> s# mark X) (mark# fact X -> mark# X, mark# s X -> mark# X) (mark# fact X -> mark# X, mark# zero X -> active# zero mark X) (mark# fact X -> mark# X, mark# zero X -> zero# mark X) (mark# fact X -> mark# X, mark# zero X -> mark# X) (mark# fact X -> mark# X, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (mark# fact X -> mark# X, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (mark# fact X -> mark# X, mark# if(X1, X2, X3) -> mark# X1) (zero# mark X -> zero# X, zero# active X -> zero# X) (zero# mark X -> zero# X, zero# mark X -> zero# X) (s# mark X -> s# X, s# active X -> s# X) (s# mark X -> s# X, s# mark X -> s# X) (fact# mark X -> fact# X, fact# active X -> fact# X) (fact# mark X -> fact# X, fact# mark X -> fact# X) (p# mark X -> p# X, p# active X -> p# X) (p# mark X -> p# X, p# mark X -> p# X) (active# if(true(), X, Y) -> mark# X, mark# false() -> active# false()) (active# if(true(), X, Y) -> mark# X, mark# true() -> active# true()) (active# if(true(), X, Y) -> mark# X, mark# add(X1, X2) -> add#(mark X1, mark X2)) (active# if(true(), X, Y) -> mark# X, mark# add(X1, X2) -> active# add(mark X1, mark X2)) (active# if(true(), X, Y) -> mark# X, mark# add(X1, X2) -> mark# X2) (active# if(true(), X, Y) -> mark# X, mark# add(X1, X2) -> mark# X1) (active# if(true(), X, Y) -> mark# X, mark# p X -> active# p 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 -> mark# X) (active# if(true(), X, Y) -> mark# X, mark# fact X -> active# fact mark X) (active# if(true(), X, Y) -> mark# X, mark# fact X -> fact# mark X) (active# if(true(), X, Y) -> mark# X, mark# fact X -> mark# X) (active# if(true(), X, Y) -> mark# X, mark# prod(X1, X2) -> active# prod(mark X1, mark X2)) (active# if(true(), X, Y) -> mark# X, mark# prod(X1, X2) -> prod#(mark X1, mark X2)) (active# if(true(), X, Y) -> mark# X, mark# prod(X1, X2) -> mark# X2) (active# if(true(), X, Y) -> mark# X, mark# prod(X1, X2) -> mark# X1) (active# if(true(), X, Y) -> mark# X, mark# 0() -> active# 0()) (active# if(true(), X, Y) -> mark# X, mark# s X -> active# s mark X) (active# if(true(), X, Y) -> mark# X, mark# s X -> s# mark X) (active# if(true(), X, Y) -> mark# X, mark# s X -> mark# X) (active# if(true(), X, Y) -> mark# X, mark# zero X -> active# zero mark X) (active# if(true(), X, Y) -> mark# X, mark# zero X -> zero# mark X) (active# if(true(), X, Y) -> mark# X, mark# zero X -> mark# X) (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) -> if#(mark X1, X2, X3)) (active# if(true(), X, Y) -> mark# X, mark# if(X1, X2, X3) -> mark# X1) (active# fact X -> p# X, p# active X -> p# X) (active# fact X -> p# X, p# mark X -> p# X) (active# add(0(), X) -> mark# X, mark# false() -> active# false()) (active# add(0(), X) -> mark# X, mark# true() -> active# true()) (active# add(0(), X) -> mark# X, mark# add(X1, X2) -> add#(mark X1, mark X2)) (active# add(0(), X) -> mark# X, mark# add(X1, X2) -> active# add(mark X1, mark X2)) (active# add(0(), X) -> mark# X, mark# add(X1, X2) -> mark# X2) (active# add(0(), X) -> mark# X, mark# add(X1, X2) -> mark# X1) (active# add(0(), X) -> mark# X, mark# p X -> active# p mark X) (active# add(0(), X) -> mark# X, mark# p X -> p# mark X) (active# add(0(), X) -> mark# X, mark# p X -> mark# X) (active# add(0(), X) -> mark# X, mark# fact X -> active# fact mark X) (active# add(0(), X) -> mark# X, mark# fact X -> fact# mark X) (active# add(0(), X) -> mark# X, mark# fact X -> mark# X) (active# add(0(), X) -> mark# X, mark# prod(X1, X2) -> active# prod(mark X1, mark X2)) (active# add(0(), X) -> mark# X, mark# prod(X1, X2) -> prod#(mark X1, mark X2)) (active# add(0(), X) -> mark# X, mark# prod(X1, X2) -> mark# X2) (active# add(0(), X) -> mark# X, mark# prod(X1, X2) -> mark# X1) (active# add(0(), X) -> mark# X, mark# 0() -> active# 0()) (active# add(0(), X) -> mark# X, mark# s X -> active# s mark X) (active# add(0(), X) -> mark# X, mark# s X -> s# mark X) (active# add(0(), X) -> mark# X, mark# s X -> mark# X) (active# add(0(), X) -> mark# X, mark# zero X -> active# zero mark X) (active# add(0(), X) -> mark# X, mark# zero X -> zero# mark X) (active# add(0(), X) -> mark# X, mark# zero X -> mark# X) (active# add(0(), X) -> mark# X, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (active# add(0(), X) -> mark# X, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (active# add(0(), X) -> mark# X, mark# if(X1, X2, X3) -> mark# X1) (mark# zero X -> active# zero mark X, active# add(0(), X) -> mark# X) (mark# zero X -> active# zero mark X, active# add(s X, Y) -> add#(X, Y)) (mark# zero X -> active# zero mark X, active# add(s X, Y) -> s# add(X, Y)) (mark# zero X -> active# zero mark X, active# add(s X, Y) -> mark# s add(X, Y)) (mark# zero X -> active# zero mark X, active# p s X -> mark# X) (mark# zero X -> active# zero mark X, active# fact X -> p# X) (mark# zero X -> active# zero mark X, active# fact X -> fact# p X) (mark# zero X -> active# zero mark X, active# fact X -> prod#(X, fact p X)) (mark# zero X -> active# zero mark X, active# fact X -> s# 0()) (mark# zero X -> active# zero mark X, active# fact X -> zero# X) (mark# zero X -> active# zero mark X, active# fact X -> if#(zero X, s 0(), prod(X, fact p X))) (mark# zero X -> active# zero mark X, active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X))) (mark# zero X -> active# zero mark X, active# prod(0(), X) -> mark# 0()) (mark# zero X -> active# zero mark X, active# prod(s X, Y) -> add#(Y, prod(X, Y))) (mark# zero X -> active# zero mark X, active# prod(s X, Y) -> prod#(X, Y)) (mark# zero X -> active# zero mark X, active# prod(s X, Y) -> mark# add(Y, prod(X, Y))) (mark# zero X -> active# zero mark X, active# zero 0() -> mark# true()) (mark# zero X -> active# zero mark X, active# zero s X -> mark# false()) (mark# zero X -> active# zero mark X, active# if(false(), X, Y) -> mark# Y) (mark# zero X -> active# zero mark X, active# if(true(), X, Y) -> mark# X) (mark# fact X -> active# fact mark X, active# add(0(), X) -> mark# X) (mark# fact X -> active# fact mark X, active# add(s X, Y) -> add#(X, Y)) (mark# fact X -> active# fact mark X, active# add(s X, Y) -> s# add(X, Y)) (mark# fact X -> active# fact mark X, active# add(s X, Y) -> mark# s add(X, Y)) (mark# fact X -> active# fact mark X, active# p s X -> mark# X) (mark# fact X -> active# fact mark X, active# fact X -> p# X) (mark# fact X -> active# fact mark X, active# fact X -> fact# p X) (mark# fact X -> active# fact mark X, active# fact X -> prod#(X, fact p X)) (mark# fact X -> active# fact mark X, active# fact X -> s# 0()) (mark# fact X -> active# fact mark X, active# fact X -> zero# X) (mark# fact X -> active# fact mark X, active# fact X -> if#(zero X, s 0(), prod(X, fact p X))) (mark# fact X -> active# fact mark X, active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X))) (mark# fact X -> active# fact mark X, active# prod(0(), X) -> mark# 0()) (mark# fact X -> active# fact mark X, active# prod(s X, Y) -> add#(Y, prod(X, Y))) (mark# fact X -> active# fact mark X, active# prod(s X, Y) -> prod#(X, Y)) (mark# fact X -> active# fact mark X, active# prod(s X, Y) -> mark# add(Y, prod(X, Y))) (mark# fact X -> active# fact mark X, active# zero 0() -> mark# true()) (mark# fact X -> active# fact mark X, active# zero s X -> mark# false()) (mark# fact X -> active# fact mark X, active# if(false(), X, Y) -> mark# Y) (mark# fact X -> active# fact mark X, active# if(true(), X, Y) -> mark# X) (active# add(s X, Y) -> mark# s add(X, Y), mark# false() -> active# false()) (active# add(s X, Y) -> mark# s add(X, Y), mark# true() -> active# true()) (active# add(s X, Y) -> mark# s add(X, Y), mark# add(X1, X2) -> add#(mark X1, mark X2)) (active# add(s X, Y) -> mark# s add(X, Y), mark# add(X1, X2) -> active# add(mark X1, mark X2)) (active# add(s X, Y) -> mark# s add(X, Y), mark# add(X1, X2) -> mark# X2) (active# add(s X, Y) -> mark# s add(X, Y), mark# add(X1, X2) -> mark# X1) (active# add(s X, Y) -> mark# s add(X, Y), mark# p X -> active# p mark X) (active# add(s X, Y) -> mark# s add(X, Y), mark# p X -> p# mark X) (active# add(s X, Y) -> mark# s add(X, Y), mark# p X -> mark# X) (active# add(s X, Y) -> mark# s add(X, Y), mark# fact X -> active# fact mark X) (active# add(s X, Y) -> mark# s add(X, Y), mark# fact X -> fact# mark X) (active# add(s X, Y) -> mark# s add(X, Y), mark# fact X -> mark# X) (active# add(s X, Y) -> mark# s add(X, Y), mark# prod(X1, X2) -> active# prod(mark X1, mark X2)) (active# add(s X, Y) -> mark# s add(X, Y), mark# prod(X1, X2) -> prod#(mark X1, mark X2)) (active# add(s X, Y) -> mark# s add(X, Y), mark# prod(X1, X2) -> mark# X2) (active# add(s X, Y) -> mark# s add(X, Y), mark# prod(X1, X2) -> mark# X1) (active# add(s X, Y) -> mark# s add(X, Y), mark# 0() -> active# 0()) (active# add(s X, Y) -> mark# s add(X, Y), mark# s X -> active# s mark X) (active# add(s X, Y) -> mark# s add(X, Y), mark# s X -> s# mark X) (active# add(s X, Y) -> mark# s add(X, Y), mark# s X -> mark# X) (active# add(s X, Y) -> mark# s add(X, Y), mark# zero X -> active# zero mark X) (active# add(s X, Y) -> mark# s add(X, Y), mark# zero X -> zero# mark X) (active# add(s X, Y) -> mark# s add(X, Y), mark# zero X -> mark# X) (active# add(s X, Y) -> mark# s add(X, Y), mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (active# add(s X, Y) -> mark# s add(X, Y), mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (active# add(s X, Y) -> mark# s add(X, Y), mark# if(X1, X2, X3) -> mark# X1) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# add(0(), X) -> mark# X) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# add(s X, Y) -> add#(X, Y)) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# add(s X, Y) -> s# add(X, Y)) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# add(s X, Y) -> mark# s add(X, Y)) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# p s X -> mark# X) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# fact X -> p# X) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# fact X -> fact# p X) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# fact X -> prod#(X, fact p X)) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# fact X -> s# 0()) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# fact X -> zero# X) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# fact X -> if#(zero X, s 0(), prod(X, fact p X))) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X))) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# prod(0(), X) -> mark# 0()) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# prod(s X, Y) -> add#(Y, prod(X, Y))) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# prod(s X, Y) -> prod#(X, Y)) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# prod(s X, Y) -> mark# add(Y, prod(X, Y))) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# zero 0() -> mark# true()) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# zero s X -> mark# false()) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# if(false(), X, Y) -> mark# Y) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# if(true(), X, Y) -> mark# X) (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# false() -> active# false()) (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# true() -> active# true()) (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# add(X1, X2) -> add#(mark X1, mark X2)) (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# add(X1, X2) -> active# add(mark X1, mark X2)) (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# add(X1, X2) -> mark# X2) (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# add(X1, X2) -> mark# X1) (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# p X -> active# p mark X) (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# p X -> p# mark X) (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# p X -> mark# X) (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# fact X -> active# fact mark X) (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# fact X -> fact# mark X) (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# fact X -> mark# X) (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# prod(X1, X2) -> active# prod(mark X1, mark X2)) (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# prod(X1, X2) -> prod#(mark X1, mark X2)) (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# prod(X1, X2) -> mark# X2) (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# prod(X1, X2) -> mark# X1) (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# 0() -> active# 0()) (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# s X -> active# s mark X) (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# s X -> s# mark X) (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# s X -> mark# X) (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# zero X -> active# zero mark X) (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# zero X -> zero# mark X) (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# zero X -> mark# X) (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# if(X1, X2, X3) -> mark# X1) (mark# add(X1, X2) -> add#(mark X1, mark X2), add#(active X1, X2) -> add#(X1, X2)) (mark# add(X1, X2) -> add#(mark X1, mark X2), add#(mark X1, X2) -> add#(X1, X2)) (mark# add(X1, X2) -> add#(mark X1, mark X2), add#(X1, active X2) -> add#(X1, X2)) (mark# add(X1, X2) -> add#(mark X1, mark X2), add#(X1, mark X2) -> add#(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)) (mark# if(X1, X2, X3) -> mark# X1, mark# false() -> active# false()) (mark# if(X1, X2, X3) -> mark# X1, mark# true() -> active# true()) (mark# if(X1, X2, X3) -> mark# X1, mark# add(X1, X2) -> add#(mark X1, mark X2)) (mark# if(X1, X2, X3) -> mark# X1, mark# add(X1, X2) -> active# add(mark X1, mark X2)) (mark# if(X1, X2, X3) -> mark# X1, mark# add(X1, X2) -> mark# X2) (mark# if(X1, X2, X3) -> mark# X1, mark# add(X1, X2) -> mark# X1) (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# p X -> mark# X) (mark# if(X1, X2, X3) -> mark# X1, mark# fact X -> active# fact mark X) (mark# if(X1, X2, X3) -> mark# X1, mark# fact X -> fact# mark X) (mark# if(X1, X2, X3) -> mark# X1, mark# fact X -> mark# X) (mark# if(X1, X2, X3) -> mark# X1, mark# prod(X1, X2) -> active# prod(mark X1, mark X2)) (mark# if(X1, X2, X3) -> mark# X1, mark# prod(X1, X2) -> prod#(mark X1, mark X2)) (mark# if(X1, X2, X3) -> mark# X1, mark# prod(X1, X2) -> mark# X2) (mark# if(X1, X2, X3) -> mark# X1, mark# prod(X1, X2) -> mark# X1) (mark# if(X1, X2, X3) -> mark# X1, mark# 0() -> active# 0()) (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# s X -> mark# X) (mark# if(X1, X2, X3) -> mark# X1, mark# zero X -> active# zero mark X) (mark# if(X1, X2, X3) -> mark# X1, mark# zero X -> zero# mark X) (mark# if(X1, X2, X3) -> mark# X1, mark# zero X -> mark# X) (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# if(X1, X2, X3) -> mark# X1) (mark# add(X1, X2) -> mark# X1, mark# false() -> active# false()) (mark# add(X1, X2) -> mark# X1, mark# true() -> active# true()) (mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> add#(mark X1, mark X2)) (mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> active# add(mark X1, mark X2)) (mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X2) (mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X1) (mark# add(X1, X2) -> mark# X1, mark# p X -> active# p mark X) (mark# add(X1, X2) -> mark# X1, mark# p X -> p# mark X) (mark# add(X1, X2) -> mark# X1, mark# p X -> mark# X) (mark# add(X1, X2) -> mark# X1, mark# fact X -> active# fact mark X) (mark# add(X1, X2) -> mark# X1, mark# fact X -> fact# mark X) (mark# add(X1, X2) -> mark# X1, mark# fact X -> mark# X) (mark# add(X1, X2) -> mark# X1, mark# prod(X1, X2) -> active# prod(mark X1, mark X2)) (mark# add(X1, X2) -> mark# X1, mark# prod(X1, X2) -> prod#(mark X1, mark X2)) (mark# add(X1, X2) -> mark# X1, mark# prod(X1, X2) -> mark# X2) (mark# add(X1, X2) -> mark# X1, mark# prod(X1, X2) -> mark# X1) (mark# add(X1, X2) -> mark# X1, mark# 0() -> active# 0()) (mark# add(X1, X2) -> mark# X1, mark# s X -> active# s mark X) (mark# add(X1, X2) -> mark# X1, mark# s X -> s# mark X) (mark# add(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# add(X1, X2) -> mark# X1, mark# zero X -> active# zero mark X) (mark# add(X1, X2) -> mark# X1, mark# zero X -> zero# mark X) (mark# add(X1, X2) -> mark# X1, mark# zero X -> mark# X) (mark# add(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (mark# add(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (mark# add(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> mark# X1) (prod#(X1, mark X2) -> prod#(X1, X2), prod#(active X1, X2) -> prod#(X1, X2)) (prod#(X1, mark X2) -> prod#(X1, X2), prod#(mark X1, X2) -> prod#(X1, X2)) (prod#(X1, mark X2) -> prod#(X1, X2), prod#(X1, active X2) -> prod#(X1, X2)) (prod#(X1, mark X2) -> prod#(X1, X2), prod#(X1, mark X2) -> prod#(X1, X2)) (prod#(mark X1, X2) -> prod#(X1, X2), prod#(active X1, X2) -> prod#(X1, X2)) (prod#(mark X1, X2) -> prod#(X1, X2), prod#(mark X1, X2) -> prod#(X1, X2)) (prod#(mark X1, X2) -> prod#(X1, X2), prod#(X1, active X2) -> prod#(X1, X2)) (prod#(mark X1, X2) -> prod#(X1, X2), prod#(X1, mark X2) -> prod#(X1, X2)) (add#(X1, mark X2) -> add#(X1, X2), add#(active X1, X2) -> add#(X1, X2)) (add#(X1, mark X2) -> add#(X1, X2), add#(mark X1, X2) -> add#(X1, X2)) (add#(X1, mark X2) -> add#(X1, X2), add#(X1, active X2) -> add#(X1, X2)) (add#(X1, mark X2) -> add#(X1, X2), add#(X1, mark X2) -> add#(X1, X2)) (add#(mark X1, X2) -> add#(X1, X2), add#(active X1, X2) -> add#(X1, X2)) (add#(mark X1, X2) -> add#(X1, X2), add#(mark X1, X2) -> add#(X1, X2)) (add#(mark X1, X2) -> add#(X1, X2), add#(X1, active X2) -> add#(X1, X2)) (add#(mark X1, X2) -> add#(X1, X2), add#(X1, mark X2) -> add#(X1, X2)) (active# zero 0() -> mark# true(), mark# true() -> active# true()) (mark# add(X1, X2) -> mark# X2, mark# false() -> active# false()) (mark# add(X1, X2) -> mark# X2, mark# true() -> active# true()) (mark# add(X1, X2) -> mark# X2, mark# add(X1, X2) -> add#(mark X1, mark X2)) (mark# add(X1, X2) -> mark# X2, mark# add(X1, X2) -> active# add(mark X1, mark X2)) (mark# add(X1, X2) -> mark# X2, mark# add(X1, X2) -> mark# X2) (mark# add(X1, X2) -> mark# X2, mark# add(X1, X2) -> mark# X1) (mark# add(X1, X2) -> mark# X2, mark# p X -> active# p mark X) (mark# add(X1, X2) -> mark# X2, mark# p X -> p# mark X) (mark# add(X1, X2) -> mark# X2, mark# p X -> mark# X) (mark# add(X1, X2) -> mark# X2, mark# fact X -> active# fact mark X) (mark# add(X1, X2) -> mark# X2, mark# fact X -> fact# mark X) (mark# add(X1, X2) -> mark# X2, mark# fact X -> mark# X) (mark# add(X1, X2) -> mark# X2, mark# prod(X1, X2) -> active# prod(mark X1, mark X2)) (mark# add(X1, X2) -> mark# X2, mark# prod(X1, X2) -> prod#(mark X1, mark X2)) (mark# add(X1, X2) -> mark# X2, mark# prod(X1, X2) -> mark# X2) (mark# add(X1, X2) -> mark# X2, mark# prod(X1, X2) -> mark# X1) (mark# add(X1, X2) -> mark# X2, mark# 0() -> active# 0()) (mark# add(X1, X2) -> mark# X2, mark# s X -> active# s mark X) (mark# add(X1, X2) -> mark# X2, mark# s X -> s# mark X) (mark# add(X1, X2) -> mark# X2, mark# s X -> mark# X) (mark# add(X1, X2) -> mark# X2, mark# zero X -> active# zero mark X) (mark# add(X1, X2) -> mark# X2, mark# zero X -> zero# mark X) (mark# add(X1, X2) -> mark# X2, mark# zero X -> mark# X) (mark# add(X1, X2) -> mark# X2, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (mark# add(X1, X2) -> mark# X2, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (mark# add(X1, X2) -> mark# X2, mark# if(X1, X2, X3) -> mark# X1) (active# add(s X, Y) -> s# add(X, Y), s# active X -> s# X) (active# add(s X, Y) -> s# add(X, Y), s# mark X -> s# X) (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# false() -> active# false()) (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# true() -> active# true()) (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# add(X1, X2) -> add#(mark X1, mark X2)) (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# add(X1, X2) -> active# add(mark X1, mark X2)) (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# add(X1, X2) -> mark# X2) (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# add(X1, X2) -> mark# X1) (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# p X -> active# p mark X) (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# p X -> p# mark X) (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# p X -> mark# X) (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# fact X -> active# fact mark X) (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# fact X -> fact# mark X) (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# fact X -> mark# X) (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# prod(X1, X2) -> active# prod(mark X1, mark X2)) (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# prod(X1, X2) -> prod#(mark X1, mark X2)) (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# prod(X1, X2) -> mark# X2) (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# prod(X1, X2) -> mark# X1) (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# 0() -> active# 0()) (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# s X -> active# s mark X) (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# s X -> s# mark X) (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# s X -> mark# X) (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# zero X -> active# zero mark X) (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# zero X -> zero# mark X) (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# zero X -> mark# X) (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# if(X1, X2, X3) -> mark# X1) (active# add(s X, Y) -> add#(X, Y), add#(active X1, X2) -> add#(X1, X2)) (active# add(s X, Y) -> add#(X, Y), add#(mark X1, X2) -> add#(X1, X2)) (active# add(s X, Y) -> add#(X, Y), add#(X1, active X2) -> add#(X1, X2)) (active# add(s X, Y) -> add#(X, Y), add#(X1, mark X2) -> add#(X1, X2)) (active# prod(s X, Y) -> prod#(X, Y), prod#(X1, mark X2) -> prod#(X1, X2)) (active# prod(s X, Y) -> prod#(X, Y), prod#(X1, active X2) -> prod#(X1, X2)) (active# prod(s X, Y) -> prod#(X, Y), prod#(mark X1, X2) -> prod#(X1, X2)) (active# prod(s X, Y) -> prod#(X, Y), prod#(active X1, X2) -> prod#(X1, X2)) (active# fact X -> prod#(X, fact p X), prod#(X1, mark X2) -> prod#(X1, X2)) (active# fact X -> prod#(X, fact p X), prod#(X1, active X2) -> prod#(X1, X2)) (active# fact X -> prod#(X, fact p X), prod#(mark X1, X2) -> prod#(X1, X2)) (active# fact X -> prod#(X, fact p X), prod#(active X1, X2) -> prod#(X1, X2)) (active# fact X -> if#(zero X, s 0(), prod(X, fact p X)), if#(X1, X2, mark X3) -> if#(X1, X2, X3)) (active# fact X -> if#(zero X, s 0(), prod(X, fact p X)), if#(X1, X2, active X3) -> if#(X1, X2, X3)) (active# fact X -> if#(zero X, s 0(), prod(X, fact p X)), if#(mark X1, X2, X3) -> if#(X1, X2, X3)) (active# fact X -> if#(zero X, s 0(), prod(X, fact p X)), if#(active X1, X2, X3) -> if#(X1, X2, X3)) (mark# prod(X1, X2) -> mark# X2, mark# if(X1, X2, X3) -> mark# X1) (mark# prod(X1, X2) -> mark# X2, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (mark# prod(X1, X2) -> mark# X2, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (mark# prod(X1, X2) -> mark# X2, mark# zero X -> mark# X) (mark# prod(X1, X2) -> mark# X2, mark# zero X -> zero# mark X) (mark# prod(X1, X2) -> mark# X2, mark# zero X -> active# zero mark X) (mark# prod(X1, X2) -> mark# X2, mark# s X -> mark# X) (mark# prod(X1, X2) -> mark# X2, mark# s X -> s# mark X) (mark# prod(X1, X2) -> mark# X2, mark# s X -> active# s mark X) (mark# prod(X1, X2) -> mark# X2, mark# 0() -> active# 0()) (mark# prod(X1, X2) -> mark# X2, mark# prod(X1, X2) -> mark# X1) (mark# prod(X1, X2) -> mark# X2, mark# prod(X1, X2) -> mark# X2) (mark# prod(X1, X2) -> mark# X2, mark# prod(X1, X2) -> prod#(mark X1, mark X2)) (mark# prod(X1, X2) -> mark# X2, mark# prod(X1, X2) -> active# prod(mark X1, mark X2)) (mark# prod(X1, X2) -> mark# X2, mark# fact X -> mark# X) (mark# prod(X1, X2) -> mark# X2, mark# fact X -> fact# mark X) (mark# prod(X1, X2) -> mark# X2, mark# fact X -> active# fact mark X) (mark# prod(X1, X2) -> mark# X2, mark# p X -> mark# X) (mark# prod(X1, X2) -> mark# X2, mark# p X -> p# mark X) (mark# prod(X1, X2) -> mark# X2, mark# p X -> active# p mark X) (mark# prod(X1, X2) -> mark# X2, mark# add(X1, X2) -> mark# X1) (mark# prod(X1, X2) -> mark# X2, mark# add(X1, X2) -> mark# X2) (mark# prod(X1, X2) -> mark# X2, mark# add(X1, X2) -> active# add(mark X1, mark X2)) (mark# prod(X1, X2) -> mark# X2, mark# add(X1, X2) -> add#(mark X1, mark X2)) (mark# prod(X1, X2) -> mark# X2, mark# true() -> active# true()) (mark# prod(X1, X2) -> mark# X2, mark# false() -> active# false()) (active# prod(0(), X) -> mark# 0(), mark# 0() -> active# 0()) (active# zero s X -> mark# false(), mark# false() -> active# false()) (add#(active X1, X2) -> add#(X1, X2), add#(X1, mark X2) -> add#(X1, X2)) (add#(active X1, X2) -> add#(X1, X2), add#(X1, active X2) -> add#(X1, X2)) (add#(active X1, X2) -> add#(X1, X2), add#(mark X1, X2) -> add#(X1, X2)) (add#(active X1, X2) -> add#(X1, X2), add#(active X1, X2) -> add#(X1, X2)) (add#(X1, active X2) -> add#(X1, X2), add#(X1, mark X2) -> add#(X1, X2)) (add#(X1, active X2) -> add#(X1, X2), add#(X1, active X2) -> add#(X1, X2)) (add#(X1, active X2) -> add#(X1, X2), add#(mark X1, X2) -> add#(X1, X2)) (add#(X1, active X2) -> add#(X1, X2), add#(active X1, X2) -> add#(X1, X2)) (prod#(active X1, X2) -> prod#(X1, X2), prod#(X1, mark X2) -> prod#(X1, X2)) (prod#(active X1, X2) -> prod#(X1, X2), prod#(X1, active X2) -> prod#(X1, X2)) (prod#(active X1, X2) -> prod#(X1, X2), prod#(mark X1, X2) -> prod#(X1, X2)) (prod#(active X1, X2) -> prod#(X1, X2), prod#(active X1, X2) -> prod#(X1, X2)) (prod#(X1, active X2) -> prod#(X1, X2), prod#(X1, mark X2) -> prod#(X1, X2)) (prod#(X1, active X2) -> prod#(X1, X2), prod#(X1, active X2) -> prod#(X1, X2)) (prod#(X1, active X2) -> prod#(X1, X2), prod#(mark X1, X2) -> prod#(X1, X2)) (prod#(X1, active X2) -> prod#(X1, X2), prod#(active X1, X2) -> prod#(X1, X2)) (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# if(false(), X, Y) -> mark# Y) (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# zero s X -> mark# false()) (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# zero 0() -> mark# true()) (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# prod(s X, Y) -> mark# add(Y, prod(X, Y))) (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# prod(s X, Y) -> prod#(X, Y)) (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# prod(s X, Y) -> add#(Y, prod(X, Y))) (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# prod(0(), X) -> mark# 0()) (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X))) (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# fact X -> if#(zero X, s 0(), prod(X, fact p X))) (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# fact X -> zero# X) (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# fact X -> s# 0()) (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# fact X -> prod#(X, fact p X)) (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# fact X -> fact# p X) (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# fact X -> p# X) (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# add(s X, Y) -> mark# s add(X, Y)) (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# add(s X, Y) -> s# add(X, Y)) (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# add(s X, Y) -> add#(X, Y)) (mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), active# add(0(), X) -> mark# X) (mark# prod(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> mark# X1) (mark# prod(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (mark# prod(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (mark# prod(X1, X2) -> mark# X1, mark# zero X -> mark# X) (mark# prod(X1, X2) -> mark# X1, mark# zero X -> zero# mark X) (mark# prod(X1, X2) -> mark# X1, mark# zero X -> active# zero mark X) (mark# prod(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# prod(X1, X2) -> mark# X1, mark# s X -> s# mark X) (mark# prod(X1, X2) -> mark# X1, mark# s X -> active# s mark X) (mark# prod(X1, X2) -> mark# X1, mark# 0() -> active# 0()) (mark# prod(X1, X2) -> mark# X1, mark# prod(X1, X2) -> mark# X1) (mark# prod(X1, X2) -> mark# X1, mark# prod(X1, X2) -> mark# X2) (mark# prod(X1, X2) -> mark# X1, mark# prod(X1, X2) -> prod#(mark X1, mark X2)) (mark# prod(X1, X2) -> mark# X1, mark# prod(X1, X2) -> active# prod(mark X1, mark X2)) (mark# prod(X1, X2) -> mark# X1, mark# fact X -> mark# X) (mark# prod(X1, X2) -> mark# X1, mark# fact X -> fact# mark X) (mark# prod(X1, X2) -> mark# X1, mark# fact X -> active# fact mark X) (mark# prod(X1, X2) -> mark# X1, mark# p X -> mark# X) (mark# prod(X1, X2) -> mark# X1, mark# p X -> p# mark X) (mark# prod(X1, X2) -> mark# X1, mark# p X -> active# p mark X) (mark# prod(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X1) (mark# prod(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X2) (mark# prod(X1, X2) -> mark# X1, mark# add(X1, X2) -> active# add(mark X1, mark X2)) (mark# prod(X1, X2) -> mark# X1, mark# add(X1, X2) -> add#(mark X1, mark X2)) (mark# prod(X1, X2) -> mark# X1, mark# true() -> active# true()) (mark# prod(X1, X2) -> mark# X1, mark# false() -> active# false()) (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)) (mark# prod(X1, X2) -> prod#(mark X1, mark X2), prod#(X1, mark X2) -> prod#(X1, X2)) (mark# prod(X1, X2) -> prod#(mark X1, mark X2), prod#(X1, active X2) -> prod#(X1, X2)) (mark# prod(X1, X2) -> prod#(mark X1, mark X2), prod#(mark X1, X2) -> prod#(X1, X2)) (mark# prod(X1, X2) -> prod#(mark X1, mark X2), prod#(active X1, X2) -> prod#(X1, X2)) (active# if(false(), X, Y) -> mark# Y, mark# if(X1, X2, X3) -> 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# zero X -> mark# X) (active# if(false(), X, Y) -> mark# Y, mark# zero X -> zero# mark X) (active# if(false(), X, Y) -> mark# Y, mark# zero X -> active# zero mark X) (active# if(false(), X, Y) -> mark# Y, mark# s X -> mark# X) (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# 0() -> active# 0()) (active# if(false(), X, Y) -> mark# Y, mark# prod(X1, X2) -> mark# X1) (active# if(false(), X, Y) -> mark# Y, mark# prod(X1, X2) -> mark# X2) (active# if(false(), X, Y) -> mark# Y, mark# prod(X1, X2) -> prod#(mark X1, mark X2)) (active# if(false(), X, Y) -> mark# Y, mark# prod(X1, X2) -> active# prod(mark X1, mark X2)) (active# if(false(), X, Y) -> mark# Y, mark# fact X -> mark# X) (active# if(false(), X, Y) -> mark# Y, mark# fact X -> fact# mark X) (active# if(false(), X, Y) -> mark# Y, mark# fact X -> active# fact mark X) (active# if(false(), X, Y) -> mark# Y, mark# p 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# add(X1, X2) -> mark# X1) (active# if(false(), X, Y) -> mark# Y, mark# add(X1, X2) -> mark# X2) (active# if(false(), X, Y) -> mark# Y, mark# add(X1, X2) -> active# add(mark X1, mark X2)) (active# if(false(), X, Y) -> mark# Y, mark# add(X1, X2) -> add#(mark X1, mark X2)) (active# if(false(), X, Y) -> mark# Y, mark# true() -> active# true()) (active# if(false(), X, Y) -> mark# Y, mark# false() -> active# false()) (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# if(true(), X, Y) -> mark# X) (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# if(false(), X, Y) -> mark# Y) (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# zero s X -> mark# false()) (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# zero 0() -> mark# true()) (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# prod(s X, Y) -> mark# add(Y, prod(X, Y))) (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# prod(s X, Y) -> prod#(X, Y)) (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# prod(s X, Y) -> add#(Y, prod(X, Y))) (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# prod(0(), X) -> mark# 0()) (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X))) (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# fact X -> if#(zero X, s 0(), prod(X, fact p X))) (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# fact X -> zero# X) (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# fact X -> s# 0()) (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# fact X -> prod#(X, fact p X)) (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# fact X -> fact# p X) (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# fact X -> p# X) (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# p s X -> mark# X) (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# add(s X, Y) -> mark# s add(X, Y)) (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# add(s X, Y) -> s# add(X, Y)) (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# add(s X, Y) -> add#(X, Y)) (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# add(0(), X) -> mark# X) (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# zero s X -> mark# false()) (mark# p X -> active# p mark X, active# zero 0() -> mark# true()) (mark# p X -> active# p mark X, active# prod(s X, Y) -> mark# add(Y, prod(X, Y))) (mark# p X -> active# p mark X, active# prod(s X, Y) -> prod#(X, Y)) (mark# p X -> active# p mark X, active# prod(s X, Y) -> add#(Y, prod(X, Y))) (mark# p X -> active# p mark X, active# prod(0(), X) -> mark# 0()) (mark# p X -> active# p mark X, active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X))) (mark# p X -> active# p mark X, active# fact X -> if#(zero X, s 0(), prod(X, fact p X))) (mark# p X -> active# p mark X, active# fact X -> zero# X) (mark# p X -> active# p mark X, active# fact X -> s# 0()) (mark# p X -> active# p mark X, active# fact X -> prod#(X, fact p X)) (mark# p X -> active# p mark X, active# fact X -> fact# p X) (mark# p X -> active# p mark X, active# fact X -> p# X) (mark# p X -> active# p mark X, active# p s X -> mark# X) (mark# p X -> active# p mark X, active# add(s X, Y) -> mark# s add(X, Y)) (mark# p X -> active# p mark X, active# add(s X, Y) -> s# add(X, Y)) (mark# p X -> active# p mark X, active# add(s X, Y) -> add#(X, Y)) (mark# p X -> active# p mark X, active# add(0(), X) -> mark# X) (mark# s X -> active# s mark X, active# if(true(), X, Y) -> mark# X) (mark# s X -> active# s mark X, active# if(false(), X, Y) -> mark# Y) (mark# s X -> active# s mark X, active# zero s X -> mark# false()) (mark# s X -> active# s mark X, active# zero 0() -> mark# true()) (mark# s X -> active# s mark X, active# prod(s X, Y) -> mark# add(Y, prod(X, Y))) (mark# s X -> active# s mark X, active# prod(s X, Y) -> prod#(X, Y)) (mark# s X -> active# s mark X, active# prod(s X, Y) -> add#(Y, prod(X, Y))) (mark# s X -> active# s mark X, active# prod(0(), X) -> mark# 0()) (mark# s X -> active# s mark X, active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X))) (mark# s X -> active# s mark X, active# fact X -> if#(zero X, s 0(), prod(X, fact p X))) (mark# s X -> active# s mark X, active# fact X -> zero# X) (mark# s X -> active# s mark X, active# fact X -> s# 0()) (mark# s X -> active# s mark X, active# fact X -> prod#(X, fact p X)) (mark# s X -> active# s mark X, active# fact X -> fact# p X) (mark# s X -> active# s mark X, active# fact X -> p# X) (mark# s X -> active# s mark X, active# p s X -> mark# X) (mark# s X -> active# s mark X, active# add(s X, Y) -> mark# s add(X, Y)) (mark# s X -> active# s mark X, active# add(s X, Y) -> s# add(X, Y)) (mark# s X -> active# s mark X, active# add(s X, Y) -> add#(X, Y)) (mark# s X -> active# s mark X, active# add(0(), X) -> mark# X) (active# prod(s X, Y) -> add#(Y, prod(X, Y)), add#(X1, mark X2) -> add#(X1, X2)) (active# prod(s X, Y) -> add#(Y, prod(X, Y)), add#(X1, active X2) -> add#(X1, X2)) (active# prod(s X, Y) -> add#(Y, prod(X, Y)), add#(mark X1, X2) -> add#(X1, X2)) (active# prod(s X, Y) -> add#(Y, prod(X, Y)), add#(active X1, X2) -> add#(X1, X2)) (active# p s X -> mark# X, mark# if(X1, X2, X3) -> mark# X1) (active# p s X -> mark# X, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (active# p s X -> mark# X, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (active# p s X -> mark# X, mark# zero X -> mark# X) (active# p s X -> mark# X, mark# zero X -> zero# mark X) (active# p s X -> mark# X, mark# zero X -> active# zero mark X) (active# p s X -> mark# X, mark# s X -> mark# X) (active# p s X -> mark# X, mark# s X -> s# mark X) (active# p s X -> mark# X, mark# s X -> active# s mark X) (active# p s X -> mark# X, mark# 0() -> active# 0()) (active# p s X -> mark# X, mark# prod(X1, X2) -> mark# X1) (active# p s X -> mark# X, mark# prod(X1, X2) -> mark# X2) (active# p s X -> mark# X, mark# prod(X1, X2) -> prod#(mark X1, mark X2)) (active# p s X -> mark# X, mark# prod(X1, X2) -> active# prod(mark X1, mark X2)) (active# p s X -> mark# X, mark# fact X -> mark# X) (active# p s X -> mark# X, mark# fact X -> fact# mark X) (active# p s X -> mark# X, mark# fact X -> active# fact mark X) (active# p s X -> mark# X, mark# p X -> mark# X) (active# p s X -> mark# X, mark# p X -> p# mark X) (active# p s X -> mark# X, mark# p X -> active# p mark X) (active# p s X -> mark# X, mark# add(X1, X2) -> mark# X1) (active# p s X -> mark# X, mark# add(X1, X2) -> mark# X2) (active# p s X -> mark# X, mark# add(X1, X2) -> active# add(mark X1, mark X2)) (active# p s X -> mark# X, mark# add(X1, X2) -> add#(mark X1, mark X2)) (active# p s X -> mark# X, mark# true() -> active# true()) (active# p s X -> mark# X, mark# false() -> active# false()) (active# fact X -> zero# X, zero# mark X -> zero# X) (active# fact X -> zero# X, zero# active X -> zero# X) (p# active X -> p# X, p# mark X -> p# X) (p# active X -> p# X, p# active X -> p# X) (fact# active X -> fact# X, fact# mark X -> fact# X) (fact# active X -> fact# X, fact# active X -> fact# X) (s# active X -> s# X, s# mark X -> s# X) (s# active X -> s# X, s# active X -> s# X) (zero# active X -> zero# X, zero# mark X -> zero# X) (zero# active X -> zero# X, zero# active X -> zero# X) (mark# p X -> mark# X, mark# if(X1, X2, X3) -> mark# X1) (mark# p X -> mark# X, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (mark# p X -> mark# X, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (mark# p X -> mark# X, mark# zero X -> mark# X) (mark# p X -> mark# X, mark# zero X -> zero# mark X) (mark# p X -> mark# X, mark# zero X -> active# zero mark X) (mark# p X -> mark# X, mark# s X -> mark# X) (mark# p X -> mark# X, mark# s X -> s# mark X) (mark# p X -> mark# X, mark# s X -> active# s mark X) (mark# p X -> mark# X, mark# 0() -> active# 0()) (mark# p X -> mark# X, mark# prod(X1, X2) -> mark# X1) (mark# p X -> mark# X, mark# prod(X1, X2) -> mark# X2) (mark# p X -> mark# X, mark# prod(X1, X2) -> prod#(mark X1, mark X2)) (mark# p X -> mark# X, mark# prod(X1, X2) -> active# prod(mark X1, mark X2)) (mark# p X -> mark# X, mark# fact X -> mark# X) (mark# p X -> mark# X, mark# fact X -> fact# mark X) (mark# p X -> mark# X, mark# fact X -> active# fact mark X) (mark# p X -> mark# X, mark# p X -> mark# X) (mark# p X -> mark# X, mark# p X -> p# mark X) (mark# p X -> mark# X, mark# p X -> active# p mark X) (mark# p X -> mark# X, mark# add(X1, X2) -> mark# X1) (mark# p X -> mark# X, mark# add(X1, X2) -> mark# X2) (mark# p X -> mark# X, mark# add(X1, X2) -> active# add(mark X1, mark X2)) (mark# p X -> mark# X, mark# add(X1, X2) -> add#(mark X1, mark X2)) (mark# p X -> mark# X, mark# true() -> active# true()) (mark# p X -> mark# X, mark# false() -> active# false()) (mark# s X -> mark# X, mark# if(X1, X2, X3) -> 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# zero X -> mark# X) (mark# s X -> mark# X, mark# zero X -> zero# mark X) (mark# s X -> mark# X, mark# zero X -> active# zero mark X) (mark# s X -> mark# X, mark# s X -> mark# X) (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# 0() -> active# 0()) (mark# s X -> mark# X, mark# prod(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# prod(X1, X2) -> mark# X2) (mark# s X -> mark# X, mark# prod(X1, X2) -> prod#(mark X1, mark X2)) (mark# s X -> mark# X, mark# prod(X1, X2) -> active# prod(mark X1, mark X2)) (mark# s X -> mark# X, mark# fact X -> mark# X) (mark# s X -> mark# X, mark# fact X -> fact# mark X) (mark# s X -> mark# X, mark# fact X -> active# fact mark X) (mark# s X -> mark# X, mark# p 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# add(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# add(X1, X2) -> mark# X2) (mark# s X -> mark# X, mark# add(X1, X2) -> active# add(mark X1, mark X2)) (mark# s X -> mark# X, mark# add(X1, X2) -> add#(mark X1, mark X2)) (mark# s X -> mark# X, mark# true() -> active# true()) (mark# s X -> mark# X, mark# false() -> active# false()) (active# fact X -> fact# p X, fact# mark X -> fact# X) (active# fact X -> fact# p X, fact# active X -> fact# X) (mark# fact X -> fact# mark X, fact# mark X -> fact# X) (mark# fact X -> fact# mark X, fact# active X -> fact# X) (mark# zero X -> zero# mark X, zero# mark X -> zero# X) (mark# zero X -> zero# mark X, zero# active X -> zero# X) } EDG: { (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# active X -> p# X) (mark# p X -> p# mark X, p# mark X -> p# X) (mark# zero X -> mark# X, mark# false() -> active# false()) (mark# zero X -> mark# X, mark# true() -> active# true()) (mark# zero X -> mark# X, mark# add(X1, X2) -> add#(mark X1, mark X2)) (mark# zero X -> mark# X, mark# add(X1, X2) -> active# add(mark X1, mark X2)) (mark# zero X -> mark# X, mark# add(X1, X2) -> mark# X2) (mark# zero X -> mark# X, mark# add(X1, X2) -> mark# X1) (mark# zero X -> mark# X, mark# p X -> active# p mark X) (mark# zero X -> mark# X, mark# p X -> p# mark X) (mark# zero X -> mark# X, mark# p X -> mark# X) (mark# zero X -> mark# X, mark# fact X -> active# fact mark X) (mark# zero X -> mark# X, mark# fact X -> fact# mark X) (mark# zero X -> mark# X, mark# fact X -> mark# X) (mark# zero X -> mark# X, mark# prod(X1, X2) -> active# prod(mark X1, mark X2)) (mark# zero X -> mark# X, mark# prod(X1, X2) -> prod#(mark X1, mark X2)) (mark# zero X -> mark# X, mark# prod(X1, X2) -> mark# X2) (mark# zero X -> mark# X, mark# prod(X1, X2) -> mark# X1) (mark# zero X -> mark# X, mark# 0() -> active# 0()) (mark# zero X -> mark# X, mark# s X -> active# s mark X) (mark# zero X -> mark# X, mark# s X -> s# mark X) (mark# zero X -> mark# X, mark# s X -> mark# X) (mark# zero X -> mark# X, mark# zero X -> active# zero mark X) (mark# zero X -> mark# X, mark# zero X -> zero# mark X) (mark# zero X -> mark# X, mark# zero X -> mark# X) (mark# zero X -> mark# X, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (mark# zero X -> mark# X, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (mark# zero X -> mark# X, mark# if(X1, X2, X3) -> mark# X1) (mark# fact X -> mark# X, mark# false() -> active# false()) (mark# fact X -> mark# X, mark# true() -> active# true()) (mark# fact X -> mark# X, mark# add(X1, X2) -> add#(mark X1, mark X2)) (mark# fact X -> mark# X, mark# add(X1, X2) -> active# add(mark X1, mark X2)) (mark# fact X -> mark# X, mark# add(X1, X2) -> mark# X2) (mark# fact X -> mark# X, mark# add(X1, X2) -> mark# X1) (mark# fact X -> mark# X, mark# p X -> active# p mark X) (mark# fact X -> mark# X, mark# p X -> p# mark X) (mark# fact X -> mark# X, mark# p X -> mark# X) (mark# fact X -> mark# X, mark# fact X -> active# fact mark X) (mark# fact X -> mark# X, mark# fact X -> fact# mark X) (mark# fact X -> mark# X, mark# fact X -> mark# X) (mark# fact X -> mark# X, mark# prod(X1, X2) -> active# prod(mark X1, mark X2)) (mark# fact X -> mark# X, mark# prod(X1, X2) -> prod#(mark X1, mark X2)) (mark# fact X -> mark# X, mark# prod(X1, X2) -> mark# X2) (mark# fact X -> mark# X, mark# prod(X1, X2) -> mark# X1) (mark# fact X -> mark# X, mark# 0() -> active# 0()) (mark# fact X -> mark# X, mark# s X -> active# s mark X) (mark# fact X -> mark# X, mark# s X -> s# mark X) (mark# fact X -> mark# X, mark# s X -> mark# X) (mark# fact X -> mark# X, mark# zero X -> active# zero mark X) (mark# fact X -> mark# X, mark# zero X -> zero# mark X) (mark# fact X -> mark# X, mark# zero X -> mark# X) (mark# fact X -> mark# X, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (mark# fact X -> mark# X, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (mark# fact X -> mark# X, mark# if(X1, X2, X3) -> mark# X1) (zero# mark X -> zero# X, zero# active X -> zero# X) (zero# mark X -> zero# X, zero# mark X -> zero# X) (s# mark X -> s# X, s# active X -> s# X) (s# mark X -> s# X, s# mark X -> s# X) (fact# mark X -> fact# X, fact# active X -> fact# X) (fact# mark X -> fact# X, fact# mark X -> fact# X) (p# mark X -> p# X, p# active X -> p# X) (p# mark X -> p# X, p# mark X -> p# X) (active# if(true(), X, Y) -> mark# X, mark# false() -> active# false()) (active# if(true(), X, Y) -> mark# X, mark# true() -> active# true()) (active# if(true(), X, Y) -> mark# X, mark# add(X1, X2) -> add#(mark X1, mark X2)) (active# if(true(), X, Y) -> mark# X, mark# add(X1, X2) -> active# add(mark X1, mark X2)) (active# if(true(), X, Y) -> mark# X, mark# add(X1, X2) -> mark# X2) (active# if(true(), X, Y) -> mark# X, mark# add(X1, X2) -> mark# X1) (active# if(true(), X, Y) -> mark# X, mark# p X -> active# p 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 -> mark# X) (active# if(true(), X, Y) -> mark# X, mark# fact X -> active# fact mark X) (active# if(true(), X, Y) -> mark# X, mark# fact X -> fact# mark X) (active# if(true(), X, Y) -> mark# X, mark# fact X -> mark# X) (active# if(true(), X, Y) -> mark# X, mark# prod(X1, X2) -> active# prod(mark X1, mark X2)) (active# if(true(), X, Y) -> mark# X, mark# prod(X1, X2) -> prod#(mark X1, mark X2)) (active# if(true(), X, Y) -> mark# X, mark# prod(X1, X2) -> mark# X2) (active# if(true(), X, Y) -> mark# X, mark# prod(X1, X2) -> mark# X1) (active# if(true(), X, Y) -> mark# X, mark# 0() -> active# 0()) (active# if(true(), X, Y) -> mark# X, mark# s X -> active# s mark X) (active# if(true(), X, Y) -> mark# X, mark# s X -> s# mark X) (active# if(true(), X, Y) -> mark# X, mark# s X -> mark# X) (active# if(true(), X, Y) -> mark# X, mark# zero X -> active# zero mark X) (active# if(true(), X, Y) -> mark# X, mark# zero X -> zero# mark X) (active# if(true(), X, Y) -> mark# X, mark# zero X -> mark# X) (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) -> if#(mark X1, X2, X3)) (active# if(true(), X, Y) -> mark# X, mark# if(X1, X2, X3) -> mark# X1) (active# fact X -> p# X, p# active X -> p# X) (active# fact X -> p# X, p# mark X -> p# X) (active# add(0(), X) -> mark# X, mark# false() -> active# false()) (active# add(0(), X) -> mark# X, mark# true() -> active# true()) (active# add(0(), X) -> mark# X, mark# add(X1, X2) -> add#(mark X1, mark X2)) (active# add(0(), X) -> mark# X, mark# add(X1, X2) -> active# add(mark X1, mark X2)) (active# add(0(), X) -> mark# X, mark# add(X1, X2) -> mark# X2) (active# add(0(), X) -> mark# X, mark# add(X1, X2) -> mark# X1) (active# add(0(), X) -> mark# X, mark# p X -> active# p mark X) (active# add(0(), X) -> mark# X, mark# p X -> p# mark X) (active# add(0(), X) -> mark# X, mark# p X -> mark# X) (active# add(0(), X) -> mark# X, mark# fact X -> active# fact mark X) (active# add(0(), X) -> mark# X, mark# fact X -> fact# mark X) (active# add(0(), X) -> mark# X, mark# fact X -> mark# X) (active# add(0(), X) -> mark# X, mark# prod(X1, X2) -> active# prod(mark X1, mark X2)) (active# add(0(), X) -> mark# X, mark# prod(X1, X2) -> prod#(mark X1, mark X2)) (active# add(0(), X) -> mark# X, mark# prod(X1, X2) -> mark# X2) (active# add(0(), X) -> mark# X, mark# prod(X1, X2) -> mark# X1) (active# add(0(), X) -> mark# X, mark# 0() -> active# 0()) (active# add(0(), X) -> mark# X, mark# s X -> active# s mark X) (active# add(0(), X) -> mark# X, mark# s X -> s# mark X) (active# add(0(), X) -> mark# X, mark# s X -> mark# X) (active# add(0(), X) -> mark# X, mark# zero X -> active# zero mark X) (active# add(0(), X) -> mark# X, mark# zero X -> zero# mark X) (active# add(0(), X) -> mark# X, mark# zero X -> mark# X) (active# add(0(), X) -> mark# X, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (active# add(0(), X) -> mark# X, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (active# add(0(), X) -> mark# X, mark# if(X1, X2, X3) -> mark# X1) (mark# zero X -> active# zero mark X, active# zero 0() -> mark# true()) (mark# zero X -> active# zero mark X, active# zero s X -> mark# false()) (mark# fact X -> active# fact mark X, active# fact X -> p# X) (mark# fact X -> active# fact mark X, active# fact X -> fact# p X) (mark# fact X -> active# fact mark X, active# fact X -> prod#(X, fact p X)) (mark# fact X -> active# fact mark X, active# fact X -> s# 0()) (mark# fact X -> active# fact mark X, active# fact X -> zero# X) (mark# fact X -> active# fact mark X, active# fact X -> if#(zero X, s 0(), prod(X, fact p X))) (mark# fact X -> active# fact mark X, active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X))) (active# add(s X, Y) -> mark# s add(X, Y), mark# s X -> active# s mark X) (active# add(s X, Y) -> mark# s add(X, Y), mark# s X -> s# mark X) (active# add(s X, Y) -> mark# s add(X, Y), mark# s X -> mark# X) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# add(0(), X) -> mark# X) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# add(s X, Y) -> add#(X, Y)) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# add(s X, Y) -> s# add(X, Y)) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# add(s X, Y) -> mark# s add(X, Y)) (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# if(X1, X2, X3) -> mark# X1) (mark# add(X1, X2) -> add#(mark X1, mark X2), add#(active X1, X2) -> add#(X1, X2)) (mark# add(X1, X2) -> add#(mark X1, mark X2), add#(mark X1, X2) -> add#(X1, X2)) (mark# add(X1, X2) -> add#(mark X1, mark X2), add#(X1, active X2) -> add#(X1, X2)) (mark# add(X1, X2) -> add#(mark X1, mark X2), add#(X1, mark X2) -> add#(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)) (mark# if(X1, X2, X3) -> mark# X1, mark# false() -> active# false()) (mark# if(X1, X2, X3) -> mark# X1, mark# true() -> active# true()) (mark# if(X1, X2, X3) -> mark# X1, mark# add(X1, X2) -> add#(mark X1, mark X2)) (mark# if(X1, X2, X3) -> mark# X1, mark# add(X1, X2) -> active# add(mark X1, mark X2)) (mark# if(X1, X2, X3) -> mark# X1, mark# add(X1, X2) -> mark# X2) (mark# if(X1, X2, X3) -> mark# X1, mark# add(X1, X2) -> mark# X1) (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# p X -> mark# X) (mark# if(X1, X2, X3) -> mark# X1, mark# fact X -> active# fact mark X) (mark# if(X1, X2, X3) -> mark# X1, mark# fact X -> fact# mark X) (mark# if(X1, X2, X3) -> mark# X1, mark# fact X -> mark# X) (mark# if(X1, X2, X3) -> mark# X1, mark# prod(X1, X2) -> active# prod(mark X1, mark X2)) (mark# if(X1, X2, X3) -> mark# X1, mark# prod(X1, X2) -> prod#(mark X1, mark X2)) (mark# if(X1, X2, X3) -> mark# X1, mark# prod(X1, X2) -> mark# X2) (mark# if(X1, X2, X3) -> mark# X1, mark# prod(X1, X2) -> mark# X1) (mark# if(X1, X2, X3) -> mark# X1, mark# 0() -> active# 0()) (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# s X -> mark# X) (mark# if(X1, X2, X3) -> mark# X1, mark# zero X -> active# zero mark X) (mark# if(X1, X2, X3) -> mark# X1, mark# zero X -> zero# mark X) (mark# if(X1, X2, X3) -> mark# X1, mark# zero X -> mark# X) (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# if(X1, X2, X3) -> mark# X1) (mark# add(X1, X2) -> mark# X1, mark# false() -> active# false()) (mark# add(X1, X2) -> mark# X1, mark# true() -> active# true()) (mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> add#(mark X1, mark X2)) (mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> active# add(mark X1, mark X2)) (mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X2) (mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X1) (mark# add(X1, X2) -> mark# X1, mark# p X -> active# p mark X) (mark# add(X1, X2) -> mark# X1, mark# p X -> p# mark X) (mark# add(X1, X2) -> mark# X1, mark# p X -> mark# X) (mark# add(X1, X2) -> mark# X1, mark# fact X -> active# fact mark X) (mark# add(X1, X2) -> mark# X1, mark# fact X -> fact# mark X) (mark# add(X1, X2) -> mark# X1, mark# fact X -> mark# X) (mark# add(X1, X2) -> mark# X1, mark# prod(X1, X2) -> active# prod(mark X1, mark X2)) (mark# add(X1, X2) -> mark# X1, mark# prod(X1, X2) -> prod#(mark X1, mark X2)) (mark# add(X1, X2) -> mark# X1, mark# prod(X1, X2) -> mark# X2) (mark# add(X1, X2) -> mark# X1, mark# prod(X1, X2) -> mark# X1) (mark# add(X1, X2) -> mark# X1, mark# 0() -> active# 0()) (mark# add(X1, X2) -> mark# X1, mark# s X -> active# s mark X) (mark# add(X1, X2) -> mark# X1, mark# s X -> s# mark X) (mark# add(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# add(X1, X2) -> mark# X1, mark# zero X -> active# zero mark X) (mark# add(X1, X2) -> mark# X1, mark# zero X -> zero# mark X) (mark# add(X1, X2) -> mark# X1, mark# zero X -> mark# X) (mark# add(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (mark# add(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (mark# add(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> mark# X1) (prod#(X1, mark X2) -> prod#(X1, X2), prod#(active X1, X2) -> prod#(X1, X2)) (prod#(X1, mark X2) -> prod#(X1, X2), prod#(mark X1, X2) -> prod#(X1, X2)) (prod#(X1, mark X2) -> prod#(X1, X2), prod#(X1, active X2) -> prod#(X1, X2)) (prod#(X1, mark X2) -> prod#(X1, X2), prod#(X1, mark X2) -> prod#(X1, X2)) (prod#(mark X1, X2) -> prod#(X1, X2), prod#(active X1, X2) -> prod#(X1, X2)) (prod#(mark X1, X2) -> prod#(X1, X2), prod#(mark X1, X2) -> prod#(X1, X2)) (prod#(mark X1, X2) -> prod#(X1, X2), prod#(X1, active X2) -> prod#(X1, X2)) (prod#(mark X1, X2) -> prod#(X1, X2), prod#(X1, mark X2) -> prod#(X1, X2)) (add#(X1, mark X2) -> add#(X1, X2), add#(active X1, X2) -> add#(X1, X2)) (add#(X1, mark X2) -> add#(X1, X2), add#(mark X1, X2) -> add#(X1, X2)) (add#(X1, mark X2) -> add#(X1, X2), add#(X1, active X2) -> add#(X1, X2)) (add#(X1, mark X2) -> add#(X1, X2), add#(X1, mark X2) -> add#(X1, X2)) (add#(mark X1, X2) -> add#(X1, X2), add#(active X1, X2) -> add#(X1, X2)) (add#(mark X1, X2) -> add#(X1, X2), add#(mark X1, X2) -> add#(X1, X2)) (add#(mark X1, X2) -> add#(X1, X2), add#(X1, active X2) -> add#(X1, X2)) (add#(mark X1, X2) -> add#(X1, X2), add#(X1, mark X2) -> add#(X1, X2)) (active# zero 0() -> mark# true(), mark# true() -> active# true()) (mark# add(X1, X2) -> mark# X2, mark# false() -> active# false()) (mark# add(X1, X2) -> mark# X2, mark# true() -> active# true()) (mark# add(X1, X2) -> mark# X2, mark# add(X1, X2) -> add#(mark X1, mark X2)) (mark# add(X1, X2) -> mark# X2, mark# add(X1, X2) -> active# add(mark X1, mark X2)) (mark# add(X1, X2) -> mark# X2, mark# add(X1, X2) -> mark# X2) (mark# add(X1, X2) -> mark# X2, mark# add(X1, X2) -> mark# X1) (mark# add(X1, X2) -> mark# X2, mark# p X -> active# p mark X) (mark# add(X1, X2) -> mark# X2, mark# p X -> p# mark X) (mark# add(X1, X2) -> mark# X2, mark# p X -> mark# X) (mark# add(X1, X2) -> mark# X2, mark# fact X -> active# fact mark X) (mark# add(X1, X2) -> mark# X2, mark# fact X -> fact# mark X) (mark# add(X1, X2) -> mark# X2, mark# fact X -> mark# X) (mark# add(X1, X2) -> mark# X2, mark# prod(X1, X2) -> active# prod(mark X1, mark X2)) (mark# add(X1, X2) -> mark# X2, mark# prod(X1, X2) -> prod#(mark X1, mark X2)) (mark# add(X1, X2) -> mark# X2, mark# prod(X1, X2) -> mark# X2) (mark# add(X1, X2) -> mark# X2, mark# prod(X1, X2) -> mark# X1) (mark# add(X1, X2) -> mark# X2, mark# 0() -> active# 0()) (mark# add(X1, X2) -> mark# X2, mark# s X -> active# s mark X) (mark# add(X1, X2) -> mark# X2, mark# s X -> s# mark X) (mark# add(X1, X2) -> mark# X2, mark# s X -> mark# X) (mark# add(X1, X2) -> mark# X2, mark# zero X -> active# zero mark X) (mark# add(X1, X2) -> mark# X2, mark# zero X -> zero# mark X) (mark# add(X1, X2) -> mark# X2, mark# zero X -> mark# X) (mark# add(X1, X2) -> mark# X2, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (mark# add(X1, X2) -> mark# X2, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (mark# add(X1, X2) -> mark# X2, mark# if(X1, X2, X3) -> mark# X1) (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# add(X1, X2) -> add#(mark X1, mark X2)) (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# add(X1, X2) -> active# add(mark X1, mark X2)) (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# add(X1, X2) -> mark# X2) (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# add(X1, X2) -> mark# X1) (active# add(s X, Y) -> add#(X, Y), add#(active X1, X2) -> add#(X1, X2)) (active# add(s X, Y) -> add#(X, Y), add#(mark X1, X2) -> add#(X1, X2)) (active# add(s X, Y) -> add#(X, Y), add#(X1, active X2) -> add#(X1, X2)) (active# add(s X, Y) -> add#(X, Y), add#(X1, mark X2) -> add#(X1, X2)) (active# prod(s X, Y) -> prod#(X, Y), prod#(X1, mark X2) -> prod#(X1, X2)) (active# prod(s X, Y) -> prod#(X, Y), prod#(X1, active X2) -> prod#(X1, X2)) (active# prod(s X, Y) -> prod#(X, Y), prod#(mark X1, X2) -> prod#(X1, X2)) (active# prod(s X, Y) -> prod#(X, Y), prod#(active X1, X2) -> prod#(X1, X2)) (active# fact X -> prod#(X, fact p X), prod#(mark X1, X2) -> prod#(X1, X2)) (active# fact X -> prod#(X, fact p X), prod#(active X1, X2) -> prod#(X1, X2)) (mark# prod(X1, X2) -> mark# X2, mark# if(X1, X2, X3) -> mark# X1) (mark# prod(X1, X2) -> mark# X2, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (mark# prod(X1, X2) -> mark# X2, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (mark# prod(X1, X2) -> mark# X2, mark# zero X -> mark# X) (mark# prod(X1, X2) -> mark# X2, mark# zero X -> zero# mark X) (mark# prod(X1, X2) -> mark# X2, mark# zero X -> active# zero mark X) (mark# prod(X1, X2) -> mark# X2, mark# s X -> mark# X) (mark# prod(X1, X2) -> mark# X2, mark# s X -> s# mark X) (mark# prod(X1, X2) -> mark# X2, mark# s X -> active# s mark X) (mark# prod(X1, X2) -> mark# X2, mark# 0() -> active# 0()) (mark# prod(X1, X2) -> mark# X2, mark# prod(X1, X2) -> mark# X1) (mark# prod(X1, X2) -> mark# X2, mark# prod(X1, X2) -> mark# X2) (mark# prod(X1, X2) -> mark# X2, mark# prod(X1, X2) -> prod#(mark X1, mark X2)) (mark# prod(X1, X2) -> mark# X2, mark# prod(X1, X2) -> active# prod(mark X1, mark X2)) (mark# prod(X1, X2) -> mark# X2, mark# fact X -> mark# X) (mark# prod(X1, X2) -> mark# X2, mark# fact X -> fact# mark X) (mark# prod(X1, X2) -> mark# X2, mark# fact X -> active# fact mark X) (mark# prod(X1, X2) -> mark# X2, mark# p X -> mark# X) (mark# prod(X1, X2) -> mark# X2, mark# p X -> p# mark X) (mark# prod(X1, X2) -> mark# X2, mark# p X -> active# p mark X) (mark# prod(X1, X2) -> mark# X2, mark# add(X1, X2) -> mark# X1) (mark# prod(X1, X2) -> mark# X2, mark# add(X1, X2) -> mark# X2) (mark# prod(X1, X2) -> mark# X2, mark# add(X1, X2) -> active# add(mark X1, mark X2)) (mark# prod(X1, X2) -> mark# X2, mark# add(X1, X2) -> add#(mark X1, mark X2)) (mark# prod(X1, X2) -> mark# X2, mark# true() -> active# true()) (mark# prod(X1, X2) -> mark# X2, mark# false() -> active# false()) (active# prod(0(), X) -> mark# 0(), mark# 0() -> active# 0()) (active# zero s X -> mark# false(), mark# false() -> active# false()) (add#(active X1, X2) -> add#(X1, X2), add#(X1, mark X2) -> add#(X1, X2)) (add#(active X1, X2) -> add#(X1, X2), add#(X1, active X2) -> add#(X1, X2)) (add#(active X1, X2) -> add#(X1, X2), add#(mark X1, X2) -> add#(X1, X2)) (add#(active X1, X2) -> add#(X1, X2), add#(active X1, X2) -> add#(X1, X2)) (add#(X1, active X2) -> add#(X1, X2), add#(X1, mark X2) -> add#(X1, X2)) (add#(X1, active X2) -> add#(X1, X2), add#(X1, active X2) -> add#(X1, X2)) (add#(X1, active X2) -> add#(X1, X2), add#(mark X1, X2) -> add#(X1, X2)) (add#(X1, active X2) -> add#(X1, X2), add#(active X1, X2) -> add#(X1, X2)) (prod#(active X1, X2) -> prod#(X1, X2), prod#(X1, mark X2) -> prod#(X1, X2)) (prod#(active X1, X2) -> prod#(X1, X2), prod#(X1, active X2) -> prod#(X1, X2)) (prod#(active X1, X2) -> prod#(X1, X2), prod#(mark X1, X2) -> prod#(X1, X2)) (prod#(active X1, X2) -> prod#(X1, X2), prod#(active X1, X2) -> prod#(X1, X2)) (prod#(X1, active X2) -> prod#(X1, X2), prod#(X1, mark X2) -> prod#(X1, X2)) (prod#(X1, active X2) -> prod#(X1, X2), prod#(X1, active X2) -> prod#(X1, X2)) (prod#(X1, active X2) -> prod#(X1, X2), prod#(mark X1, X2) -> prod#(X1, X2)) (prod#(X1, active X2) -> prod#(X1, X2), prod#(active X1, X2) -> prod#(X1, X2)) (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# if(false(), X, Y) -> mark# Y) (mark# prod(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> mark# X1) (mark# prod(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (mark# prod(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (mark# prod(X1, X2) -> mark# X1, mark# zero X -> mark# X) (mark# prod(X1, X2) -> mark# X1, mark# zero X -> zero# mark X) (mark# prod(X1, X2) -> mark# X1, mark# zero X -> active# zero mark X) (mark# prod(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# prod(X1, X2) -> mark# X1, mark# s X -> s# mark X) (mark# prod(X1, X2) -> mark# X1, mark# s X -> active# s mark X) (mark# prod(X1, X2) -> mark# X1, mark# 0() -> active# 0()) (mark# prod(X1, X2) -> mark# X1, mark# prod(X1, X2) -> mark# X1) (mark# prod(X1, X2) -> mark# X1, mark# prod(X1, X2) -> mark# X2) (mark# prod(X1, X2) -> mark# X1, mark# prod(X1, X2) -> prod#(mark X1, mark X2)) (mark# prod(X1, X2) -> mark# X1, mark# prod(X1, X2) -> active# prod(mark X1, mark X2)) (mark# prod(X1, X2) -> mark# X1, mark# fact X -> mark# X) (mark# prod(X1, X2) -> mark# X1, mark# fact X -> fact# mark X) (mark# prod(X1, X2) -> mark# X1, mark# fact X -> active# fact mark X) (mark# prod(X1, X2) -> mark# X1, mark# p X -> mark# X) (mark# prod(X1, X2) -> mark# X1, mark# p X -> p# mark X) (mark# prod(X1, X2) -> mark# X1, mark# p X -> active# p mark X) (mark# prod(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X1) (mark# prod(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X2) (mark# prod(X1, X2) -> mark# X1, mark# add(X1, X2) -> active# add(mark X1, mark X2)) (mark# prod(X1, X2) -> mark# X1, mark# add(X1, X2) -> add#(mark X1, mark X2)) (mark# prod(X1, X2) -> mark# X1, mark# true() -> active# true()) (mark# prod(X1, X2) -> mark# X1, mark# false() -> active# false()) (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)) (mark# prod(X1, X2) -> prod#(mark X1, mark X2), prod#(X1, mark X2) -> prod#(X1, X2)) (mark# prod(X1, X2) -> prod#(mark X1, mark X2), prod#(X1, active X2) -> prod#(X1, X2)) (mark# prod(X1, X2) -> prod#(mark X1, mark X2), prod#(mark X1, X2) -> prod#(X1, X2)) (mark# prod(X1, X2) -> prod#(mark X1, mark X2), prod#(active X1, X2) -> prod#(X1, X2)) (active# if(false(), X, Y) -> mark# Y, mark# if(X1, X2, X3) -> 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# zero X -> mark# X) (active# if(false(), X, Y) -> mark# Y, mark# zero X -> zero# mark X) (active# if(false(), X, Y) -> mark# Y, mark# zero X -> active# zero mark X) (active# if(false(), X, Y) -> mark# Y, mark# s X -> mark# X) (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# 0() -> active# 0()) (active# if(false(), X, Y) -> mark# Y, mark# prod(X1, X2) -> mark# X1) (active# if(false(), X, Y) -> mark# Y, mark# prod(X1, X2) -> mark# X2) (active# if(false(), X, Y) -> mark# Y, mark# prod(X1, X2) -> prod#(mark X1, mark X2)) (active# if(false(), X, Y) -> mark# Y, mark# prod(X1, X2) -> active# prod(mark X1, mark X2)) (active# if(false(), X, Y) -> mark# Y, mark# fact X -> mark# X) (active# if(false(), X, Y) -> mark# Y, mark# fact X -> fact# mark X) (active# if(false(), X, Y) -> mark# Y, mark# fact X -> active# fact mark X) (active# if(false(), X, Y) -> mark# Y, mark# p 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# add(X1, X2) -> mark# X1) (active# if(false(), X, Y) -> mark# Y, mark# add(X1, X2) -> mark# X2) (active# if(false(), X, Y) -> mark# Y, mark# add(X1, X2) -> active# add(mark X1, mark X2)) (active# if(false(), X, Y) -> mark# Y, mark# add(X1, X2) -> add#(mark X1, mark X2)) (active# if(false(), X, Y) -> mark# Y, mark# true() -> active# true()) (active# if(false(), X, Y) -> mark# Y, mark# false() -> active# false()) (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# prod(s X, Y) -> mark# add(Y, prod(X, Y))) (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# prod(s X, Y) -> prod#(X, Y)) (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# prod(s X, Y) -> add#(Y, prod(X, Y))) (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# prod(0(), X) -> mark# 0()) (mark# p X -> active# p mark X, active# p s X -> mark# X) (active# prod(s X, Y) -> add#(Y, prod(X, Y)), add#(mark X1, X2) -> add#(X1, X2)) (active# prod(s X, Y) -> add#(Y, prod(X, Y)), add#(active X1, X2) -> add#(X1, X2)) (active# p s X -> mark# X, mark# if(X1, X2, X3) -> mark# X1) (active# p s X -> mark# X, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (active# p s X -> mark# X, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (active# p s X -> mark# X, mark# zero X -> mark# X) (active# p s X -> mark# X, mark# zero X -> zero# mark X) (active# p s X -> mark# X, mark# zero X -> active# zero mark X) (active# p s X -> mark# X, mark# s X -> mark# X) (active# p s X -> mark# X, mark# s X -> s# mark X) (active# p s X -> mark# X, mark# s X -> active# s mark X) (active# p s X -> mark# X, mark# 0() -> active# 0()) (active# p s X -> mark# X, mark# prod(X1, X2) -> mark# X1) (active# p s X -> mark# X, mark# prod(X1, X2) -> mark# X2) (active# p s X -> mark# X, mark# prod(X1, X2) -> prod#(mark X1, mark X2)) (active# p s X -> mark# X, mark# prod(X1, X2) -> active# prod(mark X1, mark X2)) (active# p s X -> mark# X, mark# fact X -> mark# X) (active# p s X -> mark# X, mark# fact X -> fact# mark X) (active# p s X -> mark# X, mark# fact X -> active# fact mark X) (active# p s X -> mark# X, mark# p X -> mark# X) (active# p s X -> mark# X, mark# p X -> p# mark X) (active# p s X -> mark# X, mark# p X -> active# p mark X) (active# p s X -> mark# X, mark# add(X1, X2) -> mark# X1) (active# p s X -> mark# X, mark# add(X1, X2) -> mark# X2) (active# p s X -> mark# X, mark# add(X1, X2) -> active# add(mark X1, mark X2)) (active# p s X -> mark# X, mark# add(X1, X2) -> add#(mark X1, mark X2)) (active# p s X -> mark# X, mark# true() -> active# true()) (active# p s X -> mark# X, mark# false() -> active# false()) (active# fact X -> zero# X, zero# mark X -> zero# X) (active# fact X -> zero# X, zero# active X -> zero# X) (p# active X -> p# X, p# mark X -> p# X) (p# active X -> p# X, p# active X -> p# X) (fact# active X -> fact# X, fact# mark X -> fact# X) (fact# active X -> fact# X, fact# active X -> fact# X) (s# active X -> s# X, s# mark X -> s# X) (s# active X -> s# X, s# active X -> s# X) (zero# active X -> zero# X, zero# mark X -> zero# X) (zero# active X -> zero# X, zero# active X -> zero# X) (mark# p X -> mark# X, mark# if(X1, X2, X3) -> mark# X1) (mark# p X -> mark# X, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (mark# p X -> mark# X, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (mark# p X -> mark# X, mark# zero X -> mark# X) (mark# p X -> mark# X, mark# zero X -> zero# mark X) (mark# p X -> mark# X, mark# zero X -> active# zero mark X) (mark# p X -> mark# X, mark# s X -> mark# X) (mark# p X -> mark# X, mark# s X -> s# mark X) (mark# p X -> mark# X, mark# s X -> active# s mark X) (mark# p X -> mark# X, mark# 0() -> active# 0()) (mark# p X -> mark# X, mark# prod(X1, X2) -> mark# X1) (mark# p X -> mark# X, mark# prod(X1, X2) -> mark# X2) (mark# p X -> mark# X, mark# prod(X1, X2) -> prod#(mark X1, mark X2)) (mark# p X -> mark# X, mark# prod(X1, X2) -> active# prod(mark X1, mark X2)) (mark# p X -> mark# X, mark# fact X -> mark# X) (mark# p X -> mark# X, mark# fact X -> fact# mark X) (mark# p X -> mark# X, mark# fact X -> active# fact mark X) (mark# p X -> mark# X, mark# p X -> mark# X) (mark# p X -> mark# X, mark# p X -> p# mark X) (mark# p X -> mark# X, mark# p X -> active# p mark X) (mark# p X -> mark# X, mark# add(X1, X2) -> mark# X1) (mark# p X -> mark# X, mark# add(X1, X2) -> mark# X2) (mark# p X -> mark# X, mark# add(X1, X2) -> active# add(mark X1, mark X2)) (mark# p X -> mark# X, mark# add(X1, X2) -> add#(mark X1, mark X2)) (mark# p X -> mark# X, mark# true() -> active# true()) (mark# p X -> mark# X, mark# false() -> active# false()) (mark# s X -> mark# X, mark# if(X1, X2, X3) -> 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# zero X -> mark# X) (mark# s X -> mark# X, mark# zero X -> zero# mark X) (mark# s X -> mark# X, mark# zero X -> active# zero mark X) (mark# s X -> mark# X, mark# s X -> mark# X) (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# 0() -> active# 0()) (mark# s X -> mark# X, mark# prod(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# prod(X1, X2) -> mark# X2) (mark# s X -> mark# X, mark# prod(X1, X2) -> prod#(mark X1, mark X2)) (mark# s X -> mark# X, mark# prod(X1, X2) -> active# prod(mark X1, mark X2)) (mark# s X -> mark# X, mark# fact X -> mark# X) (mark# s X -> mark# X, mark# fact X -> fact# mark X) (mark# s X -> mark# X, mark# fact X -> active# fact mark X) (mark# s X -> mark# X, mark# p 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# add(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# add(X1, X2) -> mark# X2) (mark# s X -> mark# X, mark# add(X1, X2) -> active# add(mark X1, mark X2)) (mark# s X -> mark# X, mark# add(X1, X2) -> add#(mark X1, mark X2)) (mark# s X -> mark# X, mark# true() -> active# true()) (mark# s X -> mark# X, mark# false() -> active# false()) (mark# fact X -> fact# mark X, fact# mark X -> fact# X) (mark# fact X -> fact# mark X, fact# active X -> fact# X) (mark# zero X -> zero# mark X, zero# mark X -> zero# X) (mark# zero X -> zero# mark X, zero# active X -> zero# X) } EDG: { (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# active X -> p# X) (mark# p X -> p# mark X, p# mark X -> p# X) (mark# zero X -> mark# X, mark# false() -> active# false()) (mark# zero X -> mark# X, mark# true() -> active# true()) (mark# zero X -> mark# X, mark# add(X1, X2) -> add#(mark X1, mark X2)) (mark# zero X -> mark# X, mark# add(X1, X2) -> active# add(mark X1, mark X2)) (mark# zero X -> mark# X, mark# add(X1, X2) -> mark# X2) (mark# zero X -> mark# X, mark# add(X1, X2) -> mark# X1) (mark# zero X -> mark# X, mark# p X -> active# p mark X) (mark# zero X -> mark# X, mark# p X -> p# mark X) (mark# zero X -> mark# X, mark# p X -> mark# X) (mark# zero X -> mark# X, mark# fact X -> active# fact mark X) (mark# zero X -> mark# X, mark# fact X -> fact# mark X) (mark# zero X -> mark# X, mark# fact X -> mark# X) (mark# zero X -> mark# X, mark# prod(X1, X2) -> active# prod(mark X1, mark X2)) (mark# zero X -> mark# X, mark# prod(X1, X2) -> prod#(mark X1, mark X2)) (mark# zero X -> mark# X, mark# prod(X1, X2) -> mark# X2) (mark# zero X -> mark# X, mark# prod(X1, X2) -> mark# X1) (mark# zero X -> mark# X, mark# 0() -> active# 0()) (mark# zero X -> mark# X, mark# s X -> active# s mark X) (mark# zero X -> mark# X, mark# s X -> s# mark X) (mark# zero X -> mark# X, mark# s X -> mark# X) (mark# zero X -> mark# X, mark# zero X -> active# zero mark X) (mark# zero X -> mark# X, mark# zero X -> zero# mark X) (mark# zero X -> mark# X, mark# zero X -> mark# X) (mark# zero X -> mark# X, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (mark# zero X -> mark# X, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (mark# zero X -> mark# X, mark# if(X1, X2, X3) -> mark# X1) (mark# fact X -> mark# X, mark# false() -> active# false()) (mark# fact X -> mark# X, mark# true() -> active# true()) (mark# fact X -> mark# X, mark# add(X1, X2) -> add#(mark X1, mark X2)) (mark# fact X -> mark# X, mark# add(X1, X2) -> active# add(mark X1, mark X2)) (mark# fact X -> mark# X, mark# add(X1, X2) -> mark# X2) (mark# fact X -> mark# X, mark# add(X1, X2) -> mark# X1) (mark# fact X -> mark# X, mark# p X -> active# p mark X) (mark# fact X -> mark# X, mark# p X -> p# mark X) (mark# fact X -> mark# X, mark# p X -> mark# X) (mark# fact X -> mark# X, mark# fact X -> active# fact mark X) (mark# fact X -> mark# X, mark# fact X -> fact# mark X) (mark# fact X -> mark# X, mark# fact X -> mark# X) (mark# fact X -> mark# X, mark# prod(X1, X2) -> active# prod(mark X1, mark X2)) (mark# fact X -> mark# X, mark# prod(X1, X2) -> prod#(mark X1, mark X2)) (mark# fact X -> mark# X, mark# prod(X1, X2) -> mark# X2) (mark# fact X -> mark# X, mark# prod(X1, X2) -> mark# X1) (mark# fact X -> mark# X, mark# 0() -> active# 0()) (mark# fact X -> mark# X, mark# s X -> active# s mark X) (mark# fact X -> mark# X, mark# s X -> s# mark X) (mark# fact X -> mark# X, mark# s X -> mark# X) (mark# fact X -> mark# X, mark# zero X -> active# zero mark X) (mark# fact X -> mark# X, mark# zero X -> zero# mark X) (mark# fact X -> mark# X, mark# zero X -> mark# X) (mark# fact X -> mark# X, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (mark# fact X -> mark# X, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (mark# fact X -> mark# X, mark# if(X1, X2, X3) -> mark# X1) (zero# mark X -> zero# X, zero# active X -> zero# X) (zero# mark X -> zero# X, zero# mark X -> zero# X) (s# mark X -> s# X, s# active X -> s# X) (s# mark X -> s# X, s# mark X -> s# X) (fact# mark X -> fact# X, fact# active X -> fact# X) (fact# mark X -> fact# X, fact# mark X -> fact# X) (p# mark X -> p# X, p# active X -> p# X) (p# mark X -> p# X, p# mark X -> p# X) (active# if(true(), X, Y) -> mark# X, mark# false() -> active# false()) (active# if(true(), X, Y) -> mark# X, mark# true() -> active# true()) (active# if(true(), X, Y) -> mark# X, mark# add(X1, X2) -> add#(mark X1, mark X2)) (active# if(true(), X, Y) -> mark# X, mark# add(X1, X2) -> active# add(mark X1, mark X2)) (active# if(true(), X, Y) -> mark# X, mark# add(X1, X2) -> mark# X2) (active# if(true(), X, Y) -> mark# X, mark# add(X1, X2) -> mark# X1) (active# if(true(), X, Y) -> mark# X, mark# p X -> active# p 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 -> mark# X) (active# if(true(), X, Y) -> mark# X, mark# fact X -> active# fact mark X) (active# if(true(), X, Y) -> mark# X, mark# fact X -> fact# mark X) (active# if(true(), X, Y) -> mark# X, mark# fact X -> mark# X) (active# if(true(), X, Y) -> mark# X, mark# prod(X1, X2) -> active# prod(mark X1, mark X2)) (active# if(true(), X, Y) -> mark# X, mark# prod(X1, X2) -> prod#(mark X1, mark X2)) (active# if(true(), X, Y) -> mark# X, mark# prod(X1, X2) -> mark# X2) (active# if(true(), X, Y) -> mark# X, mark# prod(X1, X2) -> mark# X1) (active# if(true(), X, Y) -> mark# X, mark# 0() -> active# 0()) (active# if(true(), X, Y) -> mark# X, mark# s X -> active# s mark X) (active# if(true(), X, Y) -> mark# X, mark# s X -> s# mark X) (active# if(true(), X, Y) -> mark# X, mark# s X -> mark# X) (active# if(true(), X, Y) -> mark# X, mark# zero X -> active# zero mark X) (active# if(true(), X, Y) -> mark# X, mark# zero X -> zero# mark X) (active# if(true(), X, Y) -> mark# X, mark# zero X -> mark# X) (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) -> if#(mark X1, X2, X3)) (active# if(true(), X, Y) -> mark# X, mark# if(X1, X2, X3) -> mark# X1) (active# fact X -> p# X, p# active X -> p# X) (active# fact X -> p# X, p# mark X -> p# X) (active# add(0(), X) -> mark# X, mark# false() -> active# false()) (active# add(0(), X) -> mark# X, mark# true() -> active# true()) (active# add(0(), X) -> mark# X, mark# add(X1, X2) -> add#(mark X1, mark X2)) (active# add(0(), X) -> mark# X, mark# add(X1, X2) -> active# add(mark X1, mark X2)) (active# add(0(), X) -> mark# X, mark# add(X1, X2) -> mark# X2) (active# add(0(), X) -> mark# X, mark# add(X1, X2) -> mark# X1) (active# add(0(), X) -> mark# X, mark# p X -> active# p mark X) (active# add(0(), X) -> mark# X, mark# p X -> p# mark X) (active# add(0(), X) -> mark# X, mark# p X -> mark# X) (active# add(0(), X) -> mark# X, mark# fact X -> active# fact mark X) (active# add(0(), X) -> mark# X, mark# fact X -> fact# mark X) (active# add(0(), X) -> mark# X, mark# fact X -> mark# X) (active# add(0(), X) -> mark# X, mark# prod(X1, X2) -> active# prod(mark X1, mark X2)) (active# add(0(), X) -> mark# X, mark# prod(X1, X2) -> prod#(mark X1, mark X2)) (active# add(0(), X) -> mark# X, mark# prod(X1, X2) -> mark# X2) (active# add(0(), X) -> mark# X, mark# prod(X1, X2) -> mark# X1) (active# add(0(), X) -> mark# X, mark# 0() -> active# 0()) (active# add(0(), X) -> mark# X, mark# s X -> active# s mark X) (active# add(0(), X) -> mark# X, mark# s X -> s# mark X) (active# add(0(), X) -> mark# X, mark# s X -> mark# X) (active# add(0(), X) -> mark# X, mark# zero X -> active# zero mark X) (active# add(0(), X) -> mark# X, mark# zero X -> zero# mark X) (active# add(0(), X) -> mark# X, mark# zero X -> mark# X) (active# add(0(), X) -> mark# X, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (active# add(0(), X) -> mark# X, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (active# add(0(), X) -> mark# X, mark# if(X1, X2, X3) -> mark# X1) (mark# zero X -> active# zero mark X, active# zero 0() -> mark# true()) (mark# zero X -> active# zero mark X, active# zero s X -> mark# false()) (mark# fact X -> active# fact mark X, active# fact X -> p# X) (mark# fact X -> active# fact mark X, active# fact X -> fact# p X) (mark# fact X -> active# fact mark X, active# fact X -> prod#(X, fact p X)) (mark# fact X -> active# fact mark X, active# fact X -> s# 0()) (mark# fact X -> active# fact mark X, active# fact X -> zero# X) (mark# fact X -> active# fact mark X, active# fact X -> if#(zero X, s 0(), prod(X, fact p X))) (mark# fact X -> active# fact mark X, active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X))) (active# add(s X, Y) -> mark# s add(X, Y), mark# s X -> active# s mark X) (active# add(s X, Y) -> mark# s add(X, Y), mark# s X -> s# mark X) (active# add(s X, Y) -> mark# s add(X, Y), mark# s X -> mark# X) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# add(0(), X) -> mark# X) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# add(s X, Y) -> add#(X, Y)) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# add(s X, Y) -> s# add(X, Y)) (mark# add(X1, X2) -> active# add(mark X1, mark X2), active# add(s X, Y) -> mark# s add(X, Y)) (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), mark# if(X1, X2, X3) -> mark# X1) (mark# add(X1, X2) -> add#(mark X1, mark X2), add#(active X1, X2) -> add#(X1, X2)) (mark# add(X1, X2) -> add#(mark X1, mark X2), add#(mark X1, X2) -> add#(X1, X2)) (mark# add(X1, X2) -> add#(mark X1, mark X2), add#(X1, active X2) -> add#(X1, X2)) (mark# add(X1, X2) -> add#(mark X1, mark X2), add#(X1, mark X2) -> add#(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)) (mark# if(X1, X2, X3) -> mark# X1, mark# false() -> active# false()) (mark# if(X1, X2, X3) -> mark# X1, mark# true() -> active# true()) (mark# if(X1, X2, X3) -> mark# X1, mark# add(X1, X2) -> add#(mark X1, mark X2)) (mark# if(X1, X2, X3) -> mark# X1, mark# add(X1, X2) -> active# add(mark X1, mark X2)) (mark# if(X1, X2, X3) -> mark# X1, mark# add(X1, X2) -> mark# X2) (mark# if(X1, X2, X3) -> mark# X1, mark# add(X1, X2) -> mark# X1) (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# p X -> mark# X) (mark# if(X1, X2, X3) -> mark# X1, mark# fact X -> active# fact mark X) (mark# if(X1, X2, X3) -> mark# X1, mark# fact X -> fact# mark X) (mark# if(X1, X2, X3) -> mark# X1, mark# fact X -> mark# X) (mark# if(X1, X2, X3) -> mark# X1, mark# prod(X1, X2) -> active# prod(mark X1, mark X2)) (mark# if(X1, X2, X3) -> mark# X1, mark# prod(X1, X2) -> prod#(mark X1, mark X2)) (mark# if(X1, X2, X3) -> mark# X1, mark# prod(X1, X2) -> mark# X2) (mark# if(X1, X2, X3) -> mark# X1, mark# prod(X1, X2) -> mark# X1) (mark# if(X1, X2, X3) -> mark# X1, mark# 0() -> active# 0()) (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# s X -> mark# X) (mark# if(X1, X2, X3) -> mark# X1, mark# zero X -> active# zero mark X) (mark# if(X1, X2, X3) -> mark# X1, mark# zero X -> zero# mark X) (mark# if(X1, X2, X3) -> mark# X1, mark# zero X -> mark# X) (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# if(X1, X2, X3) -> mark# X1) (mark# add(X1, X2) -> mark# X1, mark# false() -> active# false()) (mark# add(X1, X2) -> mark# X1, mark# true() -> active# true()) (mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> add#(mark X1, mark X2)) (mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> active# add(mark X1, mark X2)) (mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X2) (mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X1) (mark# add(X1, X2) -> mark# X1, mark# p X -> active# p mark X) (mark# add(X1, X2) -> mark# X1, mark# p X -> p# mark X) (mark# add(X1, X2) -> mark# X1, mark# p X -> mark# X) (mark# add(X1, X2) -> mark# X1, mark# fact X -> active# fact mark X) (mark# add(X1, X2) -> mark# X1, mark# fact X -> fact# mark X) (mark# add(X1, X2) -> mark# X1, mark# fact X -> mark# X) (mark# add(X1, X2) -> mark# X1, mark# prod(X1, X2) -> active# prod(mark X1, mark X2)) (mark# add(X1, X2) -> mark# X1, mark# prod(X1, X2) -> prod#(mark X1, mark X2)) (mark# add(X1, X2) -> mark# X1, mark# prod(X1, X2) -> mark# X2) (mark# add(X1, X2) -> mark# X1, mark# prod(X1, X2) -> mark# X1) (mark# add(X1, X2) -> mark# X1, mark# 0() -> active# 0()) (mark# add(X1, X2) -> mark# X1, mark# s X -> active# s mark X) (mark# add(X1, X2) -> mark# X1, mark# s X -> s# mark X) (mark# add(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# add(X1, X2) -> mark# X1, mark# zero X -> active# zero mark X) (mark# add(X1, X2) -> mark# X1, mark# zero X -> zero# mark X) (mark# add(X1, X2) -> mark# X1, mark# zero X -> mark# X) (mark# add(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (mark# add(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (mark# add(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> mark# X1) (prod#(X1, mark X2) -> prod#(X1, X2), prod#(active X1, X2) -> prod#(X1, X2)) (prod#(X1, mark X2) -> prod#(X1, X2), prod#(mark X1, X2) -> prod#(X1, X2)) (prod#(X1, mark X2) -> prod#(X1, X2), prod#(X1, active X2) -> prod#(X1, X2)) (prod#(X1, mark X2) -> prod#(X1, X2), prod#(X1, mark X2) -> prod#(X1, X2)) (prod#(mark X1, X2) -> prod#(X1, X2), prod#(active X1, X2) -> prod#(X1, X2)) (prod#(mark X1, X2) -> prod#(X1, X2), prod#(mark X1, X2) -> prod#(X1, X2)) (prod#(mark X1, X2) -> prod#(X1, X2), prod#(X1, active X2) -> prod#(X1, X2)) (prod#(mark X1, X2) -> prod#(X1, X2), prod#(X1, mark X2) -> prod#(X1, X2)) (add#(X1, mark X2) -> add#(X1, X2), add#(active X1, X2) -> add#(X1, X2)) (add#(X1, mark X2) -> add#(X1, X2), add#(mark X1, X2) -> add#(X1, X2)) (add#(X1, mark X2) -> add#(X1, X2), add#(X1, active X2) -> add#(X1, X2)) (add#(X1, mark X2) -> add#(X1, X2), add#(X1, mark X2) -> add#(X1, X2)) (add#(mark X1, X2) -> add#(X1, X2), add#(active X1, X2) -> add#(X1, X2)) (add#(mark X1, X2) -> add#(X1, X2), add#(mark X1, X2) -> add#(X1, X2)) (add#(mark X1, X2) -> add#(X1, X2), add#(X1, active X2) -> add#(X1, X2)) (add#(mark X1, X2) -> add#(X1, X2), add#(X1, mark X2) -> add#(X1, X2)) (active# zero 0() -> mark# true(), mark# true() -> active# true()) (mark# add(X1, X2) -> mark# X2, mark# false() -> active# false()) (mark# add(X1, X2) -> mark# X2, mark# true() -> active# true()) (mark# add(X1, X2) -> mark# X2, mark# add(X1, X2) -> add#(mark X1, mark X2)) (mark# add(X1, X2) -> mark# X2, mark# add(X1, X2) -> active# add(mark X1, mark X2)) (mark# add(X1, X2) -> mark# X2, mark# add(X1, X2) -> mark# X2) (mark# add(X1, X2) -> mark# X2, mark# add(X1, X2) -> mark# X1) (mark# add(X1, X2) -> mark# X2, mark# p X -> active# p mark X) (mark# add(X1, X2) -> mark# X2, mark# p X -> p# mark X) (mark# add(X1, X2) -> mark# X2, mark# p X -> mark# X) (mark# add(X1, X2) -> mark# X2, mark# fact X -> active# fact mark X) (mark# add(X1, X2) -> mark# X2, mark# fact X -> fact# mark X) (mark# add(X1, X2) -> mark# X2, mark# fact X -> mark# X) (mark# add(X1, X2) -> mark# X2, mark# prod(X1, X2) -> active# prod(mark X1, mark X2)) (mark# add(X1, X2) -> mark# X2, mark# prod(X1, X2) -> prod#(mark X1, mark X2)) (mark# add(X1, X2) -> mark# X2, mark# prod(X1, X2) -> mark# X2) (mark# add(X1, X2) -> mark# X2, mark# prod(X1, X2) -> mark# X1) (mark# add(X1, X2) -> mark# X2, mark# 0() -> active# 0()) (mark# add(X1, X2) -> mark# X2, mark# s X -> active# s mark X) (mark# add(X1, X2) -> mark# X2, mark# s X -> s# mark X) (mark# add(X1, X2) -> mark# X2, mark# s X -> mark# X) (mark# add(X1, X2) -> mark# X2, mark# zero X -> active# zero mark X) (mark# add(X1, X2) -> mark# X2, mark# zero X -> zero# mark X) (mark# add(X1, X2) -> mark# X2, mark# zero X -> mark# X) (mark# add(X1, X2) -> mark# X2, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (mark# add(X1, X2) -> mark# X2, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (mark# add(X1, X2) -> mark# X2, mark# if(X1, X2, X3) -> mark# X1) (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# add(X1, X2) -> add#(mark X1, mark X2)) (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# add(X1, X2) -> active# add(mark X1, mark X2)) (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# add(X1, X2) -> mark# X2) (active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), mark# add(X1, X2) -> mark# X1) (active# add(s X, Y) -> add#(X, Y), add#(active X1, X2) -> add#(X1, X2)) (active# add(s X, Y) -> add#(X, Y), add#(mark X1, X2) -> add#(X1, X2)) (active# add(s X, Y) -> add#(X, Y), add#(X1, active X2) -> add#(X1, X2)) (active# add(s X, Y) -> add#(X, Y), add#(X1, mark X2) -> add#(X1, X2)) (active# prod(s X, Y) -> prod#(X, Y), prod#(X1, mark X2) -> prod#(X1, X2)) (active# prod(s X, Y) -> prod#(X, Y), prod#(X1, active X2) -> prod#(X1, X2)) (active# prod(s X, Y) -> prod#(X, Y), prod#(mark X1, X2) -> prod#(X1, X2)) (active# prod(s X, Y) -> prod#(X, Y), prod#(active X1, X2) -> prod#(X1, X2)) (active# fact X -> prod#(X, fact p X), prod#(mark X1, X2) -> prod#(X1, X2)) (active# fact X -> prod#(X, fact p X), prod#(active X1, X2) -> prod#(X1, X2)) (mark# prod(X1, X2) -> mark# X2, mark# if(X1, X2, X3) -> mark# X1) (mark# prod(X1, X2) -> mark# X2, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (mark# prod(X1, X2) -> mark# X2, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (mark# prod(X1, X2) -> mark# X2, mark# zero X -> mark# X) (mark# prod(X1, X2) -> mark# X2, mark# zero X -> zero# mark X) (mark# prod(X1, X2) -> mark# X2, mark# zero X -> active# zero mark X) (mark# prod(X1, X2) -> mark# X2, mark# s X -> mark# X) (mark# prod(X1, X2) -> mark# X2, mark# s X -> s# mark X) (mark# prod(X1, X2) -> mark# X2, mark# s X -> active# s mark X) (mark# prod(X1, X2) -> mark# X2, mark# 0() -> active# 0()) (mark# prod(X1, X2) -> mark# X2, mark# prod(X1, X2) -> mark# X1) (mark# prod(X1, X2) -> mark# X2, mark# prod(X1, X2) -> mark# X2) (mark# prod(X1, X2) -> mark# X2, mark# prod(X1, X2) -> prod#(mark X1, mark X2)) (mark# prod(X1, X2) -> mark# X2, mark# prod(X1, X2) -> active# prod(mark X1, mark X2)) (mark# prod(X1, X2) -> mark# X2, mark# fact X -> mark# X) (mark# prod(X1, X2) -> mark# X2, mark# fact X -> fact# mark X) (mark# prod(X1, X2) -> mark# X2, mark# fact X -> active# fact mark X) (mark# prod(X1, X2) -> mark# X2, mark# p X -> mark# X) (mark# prod(X1, X2) -> mark# X2, mark# p X -> p# mark X) (mark# prod(X1, X2) -> mark# X2, mark# p X -> active# p mark X) (mark# prod(X1, X2) -> mark# X2, mark# add(X1, X2) -> mark# X1) (mark# prod(X1, X2) -> mark# X2, mark# add(X1, X2) -> mark# X2) (mark# prod(X1, X2) -> mark# X2, mark# add(X1, X2) -> active# add(mark X1, mark X2)) (mark# prod(X1, X2) -> mark# X2, mark# add(X1, X2) -> add#(mark X1, mark X2)) (mark# prod(X1, X2) -> mark# X2, mark# true() -> active# true()) (mark# prod(X1, X2) -> mark# X2, mark# false() -> active# false()) (active# prod(0(), X) -> mark# 0(), mark# 0() -> active# 0()) (active# zero s X -> mark# false(), mark# false() -> active# false()) (add#(active X1, X2) -> add#(X1, X2), add#(X1, mark X2) -> add#(X1, X2)) (add#(active X1, X2) -> add#(X1, X2), add#(X1, active X2) -> add#(X1, X2)) (add#(active X1, X2) -> add#(X1, X2), add#(mark X1, X2) -> add#(X1, X2)) (add#(active X1, X2) -> add#(X1, X2), add#(active X1, X2) -> add#(X1, X2)) (add#(X1, active X2) -> add#(X1, X2), add#(X1, mark X2) -> add#(X1, X2)) (add#(X1, active X2) -> add#(X1, X2), add#(X1, active X2) -> add#(X1, X2)) (add#(X1, active X2) -> add#(X1, X2), add#(mark X1, X2) -> add#(X1, X2)) (add#(X1, active X2) -> add#(X1, X2), add#(active X1, X2) -> add#(X1, X2)) (prod#(active X1, X2) -> prod#(X1, X2), prod#(X1, mark X2) -> prod#(X1, X2)) (prod#(active X1, X2) -> prod#(X1, X2), prod#(X1, active X2) -> prod#(X1, X2)) (prod#(active X1, X2) -> prod#(X1, X2), prod#(mark X1, X2) -> prod#(X1, X2)) (prod#(active X1, X2) -> prod#(X1, X2), prod#(active X1, X2) -> prod#(X1, X2)) (prod#(X1, active X2) -> prod#(X1, X2), prod#(X1, mark X2) -> prod#(X1, X2)) (prod#(X1, active X2) -> prod#(X1, X2), prod#(X1, active X2) -> prod#(X1, X2)) (prod#(X1, active X2) -> prod#(X1, X2), prod#(mark X1, X2) -> prod#(X1, X2)) (prod#(X1, active X2) -> prod#(X1, X2), prod#(active X1, X2) -> prod#(X1, X2)) (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# if(false(), X, Y) -> mark# Y) (mark# prod(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> mark# X1) (mark# prod(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (mark# prod(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (mark# prod(X1, X2) -> mark# X1, mark# zero X -> mark# X) (mark# prod(X1, X2) -> mark# X1, mark# zero X -> zero# mark X) (mark# prod(X1, X2) -> mark# X1, mark# zero X -> active# zero mark X) (mark# prod(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# prod(X1, X2) -> mark# X1, mark# s X -> s# mark X) (mark# prod(X1, X2) -> mark# X1, mark# s X -> active# s mark X) (mark# prod(X1, X2) -> mark# X1, mark# 0() -> active# 0()) (mark# prod(X1, X2) -> mark# X1, mark# prod(X1, X2) -> mark# X1) (mark# prod(X1, X2) -> mark# X1, mark# prod(X1, X2) -> mark# X2) (mark# prod(X1, X2) -> mark# X1, mark# prod(X1, X2) -> prod#(mark X1, mark X2)) (mark# prod(X1, X2) -> mark# X1, mark# prod(X1, X2) -> active# prod(mark X1, mark X2)) (mark# prod(X1, X2) -> mark# X1, mark# fact X -> mark# X) (mark# prod(X1, X2) -> mark# X1, mark# fact X -> fact# mark X) (mark# prod(X1, X2) -> mark# X1, mark# fact X -> active# fact mark X) (mark# prod(X1, X2) -> mark# X1, mark# p X -> mark# X) (mark# prod(X1, X2) -> mark# X1, mark# p X -> p# mark X) (mark# prod(X1, X2) -> mark# X1, mark# p X -> active# p mark X) (mark# prod(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X1) (mark# prod(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X2) (mark# prod(X1, X2) -> mark# X1, mark# add(X1, X2) -> active# add(mark X1, mark X2)) (mark# prod(X1, X2) -> mark# X1, mark# add(X1, X2) -> add#(mark X1, mark X2)) (mark# prod(X1, X2) -> mark# X1, mark# true() -> active# true()) (mark# prod(X1, X2) -> mark# X1, mark# false() -> active# false()) (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)) (mark# prod(X1, X2) -> prod#(mark X1, mark X2), prod#(X1, mark X2) -> prod#(X1, X2)) (mark# prod(X1, X2) -> prod#(mark X1, mark X2), prod#(X1, active X2) -> prod#(X1, X2)) (mark# prod(X1, X2) -> prod#(mark X1, mark X2), prod#(mark X1, X2) -> prod#(X1, X2)) (mark# prod(X1, X2) -> prod#(mark X1, mark X2), prod#(active X1, X2) -> prod#(X1, X2)) (active# if(false(), X, Y) -> mark# Y, mark# if(X1, X2, X3) -> 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# zero X -> mark# X) (active# if(false(), X, Y) -> mark# Y, mark# zero X -> zero# mark X) (active# if(false(), X, Y) -> mark# Y, mark# zero X -> active# zero mark X) (active# if(false(), X, Y) -> mark# Y, mark# s X -> mark# X) (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# 0() -> active# 0()) (active# if(false(), X, Y) -> mark# Y, mark# prod(X1, X2) -> mark# X1) (active# if(false(), X, Y) -> mark# Y, mark# prod(X1, X2) -> mark# X2) (active# if(false(), X, Y) -> mark# Y, mark# prod(X1, X2) -> prod#(mark X1, mark X2)) (active# if(false(), X, Y) -> mark# Y, mark# prod(X1, X2) -> active# prod(mark X1, mark X2)) (active# if(false(), X, Y) -> mark# Y, mark# fact X -> mark# X) (active# if(false(), X, Y) -> mark# Y, mark# fact X -> fact# mark X) (active# if(false(), X, Y) -> mark# Y, mark# fact X -> active# fact mark X) (active# if(false(), X, Y) -> mark# Y, mark# p 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# add(X1, X2) -> mark# X1) (active# if(false(), X, Y) -> mark# Y, mark# add(X1, X2) -> mark# X2) (active# if(false(), X, Y) -> mark# Y, mark# add(X1, X2) -> active# add(mark X1, mark X2)) (active# if(false(), X, Y) -> mark# Y, mark# add(X1, X2) -> add#(mark X1, mark X2)) (active# if(false(), X, Y) -> mark# Y, mark# true() -> active# true()) (active# if(false(), X, Y) -> mark# Y, mark# false() -> active# false()) (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# prod(s X, Y) -> mark# add(Y, prod(X, Y))) (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# prod(s X, Y) -> prod#(X, Y)) (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# prod(s X, Y) -> add#(Y, prod(X, Y))) (mark# prod(X1, X2) -> active# prod(mark X1, mark X2), active# prod(0(), X) -> mark# 0()) (mark# p X -> active# p mark X, active# p s X -> mark# X) (active# prod(s X, Y) -> add#(Y, prod(X, Y)), add#(mark X1, X2) -> add#(X1, X2)) (active# prod(s X, Y) -> add#(Y, prod(X, Y)), add#(active X1, X2) -> add#(X1, X2)) (active# p s X -> mark# X, mark# if(X1, X2, X3) -> mark# X1) (active# p s X -> mark# X, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (active# p s X -> mark# X, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (active# p s X -> mark# X, mark# zero X -> mark# X) (active# p s X -> mark# X, mark# zero X -> zero# mark X) (active# p s X -> mark# X, mark# zero X -> active# zero mark X) (active# p s X -> mark# X, mark# s X -> mark# X) (active# p s X -> mark# X, mark# s X -> s# mark X) (active# p s X -> mark# X, mark# s X -> active# s mark X) (active# p s X -> mark# X, mark# 0() -> active# 0()) (active# p s X -> mark# X, mark# prod(X1, X2) -> mark# X1) (active# p s X -> mark# X, mark# prod(X1, X2) -> mark# X2) (active# p s X -> mark# X, mark# prod(X1, X2) -> prod#(mark X1, mark X2)) (active# p s X -> mark# X, mark# prod(X1, X2) -> active# prod(mark X1, mark X2)) (active# p s X -> mark# X, mark# fact X -> mark# X) (active# p s X -> mark# X, mark# fact X -> fact# mark X) (active# p s X -> mark# X, mark# fact X -> active# fact mark X) (active# p s X -> mark# X, mark# p X -> mark# X) (active# p s X -> mark# X, mark# p X -> p# mark X) (active# p s X -> mark# X, mark# p X -> active# p mark X) (active# p s X -> mark# X, mark# add(X1, X2) -> mark# X1) (active# p s X -> mark# X, mark# add(X1, X2) -> mark# X2) (active# p s X -> mark# X, mark# add(X1, X2) -> active# add(mark X1, mark X2)) (active# p s X -> mark# X, mark# add(X1, X2) -> add#(mark X1, mark X2)) (active# p s X -> mark# X, mark# true() -> active# true()) (active# p s X -> mark# X, mark# false() -> active# false()) (active# fact X -> zero# X, zero# mark X -> zero# X) (active# fact X -> zero# X, zero# active X -> zero# X) (p# active X -> p# X, p# mark X -> p# X) (p# active X -> p# X, p# active X -> p# X) (fact# active X -> fact# X, fact# mark X -> fact# X) (fact# active X -> fact# X, fact# active X -> fact# X) (s# active X -> s# X, s# mark X -> s# X) (s# active X -> s# X, s# active X -> s# X) (zero# active X -> zero# X, zero# mark X -> zero# X) (zero# active X -> zero# X, zero# active X -> zero# X) (mark# p X -> mark# X, mark# if(X1, X2, X3) -> mark# X1) (mark# p X -> mark# X, mark# if(X1, X2, X3) -> if#(mark X1, X2, X3)) (mark# p X -> mark# X, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3)) (mark# p X -> mark# X, mark# zero X -> mark# X) (mark# p X -> mark# X, mark# zero X -> zero# mark X) (mark# p X -> mark# X, mark# zero X -> active# zero mark X) (mark# p X -> mark# X, mark# s X -> mark# X) (mark# p X -> mark# X, mark# s X -> s# mark X) (mark# p X -> mark# X, mark# s X -> active# s mark X) (mark# p X -> mark# X, mark# 0() -> active# 0()) (mark# p X -> mark# X, mark# prod(X1, X2) -> mark# X1) (mark# p X -> mark# X, mark# prod(X1, X2) -> mark# X2) (mark# p X -> mark# X, mark# prod(X1, X2) -> prod#(mark X1, mark X2)) (mark# p X -> mark# X, mark# prod(X1, X2) -> active# prod(mark X1, mark X2)) (mark# p X -> mark# X, mark# fact X -> mark# X) (mark# p X -> mark# X, mark# fact X -> fact# mark X) (mark# p X -> mark# X, mark# fact X -> active# fact mark X) (mark# p X -> mark# X, mark# p X -> mark# X) (mark# p X -> mark# X, mark# p X -> p# mark X) (mark# p X -> mark# X, mark# p X -> active# p mark X) (mark# p X -> mark# X, mark# add(X1, X2) -> mark# X1) (mark# p X -> mark# X, mark# add(X1, X2) -> mark# X2) (mark# p X -> mark# X, mark# add(X1, X2) -> active# add(mark X1, mark X2)) (mark# p X -> mark# X, mark# add(X1, X2) -> add#(mark X1, mark X2)) (mark# p X -> mark# X, mark# true() -> active# true()) (mark# p X -> mark# X, mark# false() -> active# false()) (mark# s X -> mark# X, mark# if(X1, X2, X3) -> 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# zero X -> mark# X) (mark# s X -> mark# X, mark# zero X -> zero# mark X) (mark# s X -> mark# X, mark# zero X -> active# zero mark X) (mark# s X -> mark# X, mark# s X -> mark# X) (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# 0() -> active# 0()) (mark# s X -> mark# X, mark# prod(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# prod(X1, X2) -> mark# X2) (mark# s X -> mark# X, mark# prod(X1, X2) -> prod#(mark X1, mark X2)) (mark# s X -> mark# X, mark# prod(X1, X2) -> active# prod(mark X1, mark X2)) (mark# s X -> mark# X, mark# fact X -> mark# X) (mark# s X -> mark# X, mark# fact X -> fact# mark X) (mark# s X -> mark# X, mark# fact X -> active# fact mark X) (mark# s X -> mark# X, mark# p 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# add(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# add(X1, X2) -> mark# X2) (mark# s X -> mark# X, mark# add(X1, X2) -> active# add(mark X1, mark X2)) (mark# s X -> mark# X, mark# add(X1, X2) -> add#(mark X1, mark X2)) (mark# s X -> mark# X, mark# true() -> active# true()) (mark# s X -> mark# X, mark# false() -> active# false()) (mark# fact X -> fact# mark X, fact# mark X -> fact# X) (mark# fact X -> fact# mark X, fact# active X -> fact# X) (mark# zero X -> zero# mark X, zero# mark X -> zero# X) (mark# zero X -> zero# mark X, zero# active X -> zero# X) } STATUS: arrows: 0.893382 SCCS (8): Scc: { mark# if(X1, X2, X3) -> mark# X1, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), mark# zero X -> mark# X, mark# s X -> mark# X, mark# prod(X1, X2) -> mark# X1, mark# prod(X1, X2) -> mark# X2, mark# prod(X1, X2) -> active# prod(mark X1, mark X2), mark# fact X -> mark# X, mark# fact X -> active# fact mark X, mark# p X -> mark# X, mark# p X -> active# p mark X, mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X2, mark# add(X1, X2) -> active# add(mark X1, mark X2), active# if(true(), X, Y) -> mark# X, active# if(false(), X, Y) -> mark# Y, active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), active# p s X -> mark# X, active# add(s X, Y) -> mark# s add(X, Y), active# add(0(), X) -> mark# X} Scc: { add#(X1, mark X2) -> add#(X1, X2), add#(X1, active X2) -> add#(X1, X2), add#(mark X1, X2) -> add#(X1, X2), add#(active X1, X2) -> add#(X1, X2)} Scc: { prod#(X1, mark X2) -> prod#(X1, X2), prod#(X1, active X2) -> prod#(X1, X2), prod#(mark X1, X2) -> prod#(X1, X2), prod#(active X1, X2) -> prod#(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: { p# mark X -> p# X, p# active X -> p# X} Scc: { fact# mark X -> fact# X, fact# active X -> fact# X} Scc: { s# mark X -> s# X, s# active X -> s# X} Scc: { zero# mark X -> zero# X, zero# active X -> zero# X} SCC (21): Strict: { mark# if(X1, X2, X3) -> mark# X1, mark# if(X1, X2, X3) -> active# if(mark X1, X2, X3), mark# zero X -> mark# X, mark# s X -> mark# X, mark# prod(X1, X2) -> mark# X1, mark# prod(X1, X2) -> mark# X2, mark# prod(X1, X2) -> active# prod(mark X1, mark X2), mark# fact X -> mark# X, mark# fact X -> active# fact mark X, mark# p X -> mark# X, mark# p X -> active# p mark X, mark# add(X1, X2) -> mark# X1, mark# add(X1, X2) -> mark# X2, mark# add(X1, X2) -> active# add(mark X1, mark X2), active# if(true(), X, Y) -> mark# X, active# if(false(), X, Y) -> mark# Y, active# prod(s X, Y) -> mark# add(Y, prod(X, Y)), active# fact X -> mark# if(zero X, s 0(), prod(X, fact p X)), active# p s X -> mark# X, active# add(s X, Y) -> mark# s add(X, Y), active# add(0(), X) -> mark# X} Weak: { mark if(X1, X2, X3) -> active if(mark X1, X2, X3), mark zero X -> active zero mark X, mark s X -> active s mark X, mark 0() -> active 0(), mark prod(X1, X2) -> active prod(mark X1, mark X2), mark fact X -> active fact mark X, mark p X -> active p mark X, mark add(X1, X2) -> active add(mark X1, mark X2), mark true() -> active true(), mark false() -> active false(), 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), zero mark X -> zero X, zero active X -> zero X, s mark X -> s X, s active X -> s X, prod(X1, mark X2) -> prod(X1, X2), prod(X1, active X2) -> prod(X1, X2), prod(mark X1, X2) -> prod(X1, X2), prod(active X1, X2) -> prod(X1, X2), fact mark X -> fact X, fact active X -> fact X, p mark X -> p X, p active X -> p X, active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active zero s X -> mark false(), active zero 0() -> mark true(), active prod(s X, Y) -> mark add(Y, prod(X, Y)), active prod(0(), X) -> mark 0(), active fact X -> mark if(zero X, s 0(), prod(X, fact p X)), active p s X -> mark X, active add(s X, Y) -> mark s add(X, Y), active add(0(), X) -> mark X, add(X1, mark X2) -> add(X1, X2), add(X1, active X2) -> add(X1, X2), add(mark X1, X2) -> add(X1, X2), add(active X1, X2) -> add(X1, X2)} Open SCC (4): Strict: { add#(X1, mark X2) -> add#(X1, X2), add#(X1, active X2) -> add#(X1, X2), add#(mark X1, X2) -> add#(X1, X2), add#(active X1, X2) -> add#(X1, X2)} Weak: { mark if(X1, X2, X3) -> active if(mark X1, X2, X3), mark zero X -> active zero mark X, mark s X -> active s mark X, mark 0() -> active 0(), mark prod(X1, X2) -> active prod(mark X1, mark X2), mark fact X -> active fact mark X, mark p X -> active p mark X, mark add(X1, X2) -> active add(mark X1, mark X2), mark true() -> active true(), mark false() -> active false(), 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), zero mark X -> zero X, zero active X -> zero X, s mark X -> s X, s active X -> s X, prod(X1, mark X2) -> prod(X1, X2), prod(X1, active X2) -> prod(X1, X2), prod(mark X1, X2) -> prod(X1, X2), prod(active X1, X2) -> prod(X1, X2), fact mark X -> fact X, fact active X -> fact X, p mark X -> p X, p active X -> p X, active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active zero s X -> mark false(), active zero 0() -> mark true(), active prod(s X, Y) -> mark add(Y, prod(X, Y)), active prod(0(), X) -> mark 0(), active fact X -> mark if(zero X, s 0(), prod(X, fact p X)), active p s X -> mark X, active add(s X, Y) -> mark s add(X, Y), active add(0(), X) -> mark X, add(X1, mark X2) -> add(X1, X2), add(X1, active X2) -> add(X1, X2), add(mark X1, X2) -> add(X1, X2), add(active X1, X2) -> add(X1, X2)} Open SCC (4): Strict: { prod#(X1, mark X2) -> prod#(X1, X2), prod#(X1, active X2) -> prod#(X1, X2), prod#(mark X1, X2) -> prod#(X1, X2), prod#(active X1, X2) -> prod#(X1, X2)} Weak: { mark if(X1, X2, X3) -> active if(mark X1, X2, X3), mark zero X -> active zero mark X, mark s X -> active s mark X, mark 0() -> active 0(), mark prod(X1, X2) -> active prod(mark X1, mark X2), mark fact X -> active fact mark X, mark p X -> active p mark X, mark add(X1, X2) -> active add(mark X1, mark X2), mark true() -> active true(), mark false() -> active false(), 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), zero mark X -> zero X, zero active X -> zero X, s mark X -> s X, s active X -> s X, prod(X1, mark X2) -> prod(X1, X2), prod(X1, active X2) -> prod(X1, X2), prod(mark X1, X2) -> prod(X1, X2), prod(active X1, X2) -> prod(X1, X2), fact mark X -> fact X, fact active X -> fact X, p mark X -> p X, p active X -> p X, active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active zero s X -> mark false(), active zero 0() -> mark true(), active prod(s X, Y) -> mark add(Y, prod(X, Y)), active prod(0(), X) -> mark 0(), active fact X -> mark if(zero X, s 0(), prod(X, fact p X)), active p s X -> mark X, active add(s X, Y) -> mark s add(X, Y), active add(0(), X) -> mark X, add(X1, mark X2) -> add(X1, X2), add(X1, active X2) -> add(X1, X2), add(mark X1, X2) -> add(X1, X2), add(active X1, X2) -> add(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 if(X1, X2, X3) -> active if(mark X1, X2, X3), mark zero X -> active zero mark X, mark s X -> active s mark X, mark 0() -> active 0(), mark prod(X1, X2) -> active prod(mark X1, mark X2), mark fact X -> active fact mark X, mark p X -> active p mark X, mark add(X1, X2) -> active add(mark X1, mark X2), mark true() -> active true(), mark false() -> active false(), 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), zero mark X -> zero X, zero active X -> zero X, s mark X -> s X, s active X -> s X, prod(X1, mark X2) -> prod(X1, X2), prod(X1, active X2) -> prod(X1, X2), prod(mark X1, X2) -> prod(X1, X2), prod(active X1, X2) -> prod(X1, X2), fact mark X -> fact X, fact active X -> fact X, p mark X -> p X, p active X -> p X, active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active zero s X -> mark false(), active zero 0() -> mark true(), active prod(s X, Y) -> mark add(Y, prod(X, Y)), active prod(0(), X) -> mark 0(), active fact X -> mark if(zero X, s 0(), prod(X, fact p X)), active p s X -> mark X, active add(s X, Y) -> mark s add(X, Y), active add(0(), X) -> mark X, add(X1, mark X2) -> add(X1, X2), add(X1, active X2) -> add(X1, X2), add(mark X1, X2) -> add(X1, X2), add(active X1, X2) -> add(X1, X2)} Open SCC (2): Strict: { p# mark X -> p# X, p# active X -> p# X} Weak: { mark if(X1, X2, X3) -> active if(mark X1, X2, X3), mark zero X -> active zero mark X, mark s X -> active s mark X, mark 0() -> active 0(), mark prod(X1, X2) -> active prod(mark X1, mark X2), mark fact X -> active fact mark X, mark p X -> active p mark X, mark add(X1, X2) -> active add(mark X1, mark X2), mark true() -> active true(), mark false() -> active false(), 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), zero mark X -> zero X, zero active X -> zero X, s mark X -> s X, s active X -> s X, prod(X1, mark X2) -> prod(X1, X2), prod(X1, active X2) -> prod(X1, X2), prod(mark X1, X2) -> prod(X1, X2), prod(active X1, X2) -> prod(X1, X2), fact mark X -> fact X, fact active X -> fact X, p mark X -> p X, p active X -> p X, active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active zero s X -> mark false(), active zero 0() -> mark true(), active prod(s X, Y) -> mark add(Y, prod(X, Y)), active prod(0(), X) -> mark 0(), active fact X -> mark if(zero X, s 0(), prod(X, fact p X)), active p s X -> mark X, active add(s X, Y) -> mark s add(X, Y), active add(0(), X) -> mark X, add(X1, mark X2) -> add(X1, X2), add(X1, active X2) -> add(X1, X2), add(mark X1, X2) -> add(X1, X2), add(active X1, X2) -> add(X1, X2)} Open SCC (2): Strict: { fact# mark X -> fact# X, fact# active X -> fact# X} Weak: { mark if(X1, X2, X3) -> active if(mark X1, X2, X3), mark zero X -> active zero mark X, mark s X -> active s mark X, mark 0() -> active 0(), mark prod(X1, X2) -> active prod(mark X1, mark X2), mark fact X -> active fact mark X, mark p X -> active p mark X, mark add(X1, X2) -> active add(mark X1, mark X2), mark true() -> active true(), mark false() -> active false(), 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), zero mark X -> zero X, zero active X -> zero X, s mark X -> s X, s active X -> s X, prod(X1, mark X2) -> prod(X1, X2), prod(X1, active X2) -> prod(X1, X2), prod(mark X1, X2) -> prod(X1, X2), prod(active X1, X2) -> prod(X1, X2), fact mark X -> fact X, fact active X -> fact X, p mark X -> p X, p active X -> p X, active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active zero s X -> mark false(), active zero 0() -> mark true(), active prod(s X, Y) -> mark add(Y, prod(X, Y)), active prod(0(), X) -> mark 0(), active fact X -> mark if(zero X, s 0(), prod(X, fact p X)), active p s X -> mark X, active add(s X, Y) -> mark s add(X, Y), active add(0(), X) -> mark X, add(X1, mark X2) -> add(X1, X2), add(X1, active X2) -> add(X1, X2), add(mark X1, X2) -> add(X1, X2), add(active X1, X2) -> add(X1, X2)} Open SCC (2): Strict: { s# mark X -> s# X, s# active X -> s# X} Weak: { mark if(X1, X2, X3) -> active if(mark X1, X2, X3), mark zero X -> active zero mark X, mark s X -> active s mark X, mark 0() -> active 0(), mark prod(X1, X2) -> active prod(mark X1, mark X2), mark fact X -> active fact mark X, mark p X -> active p mark X, mark add(X1, X2) -> active add(mark X1, mark X2), mark true() -> active true(), mark false() -> active false(), 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), zero mark X -> zero X, zero active X -> zero X, s mark X -> s X, s active X -> s X, prod(X1, mark X2) -> prod(X1, X2), prod(X1, active X2) -> prod(X1, X2), prod(mark X1, X2) -> prod(X1, X2), prod(active X1, X2) -> prod(X1, X2), fact mark X -> fact X, fact active X -> fact X, p mark X -> p X, p active X -> p X, active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active zero s X -> mark false(), active zero 0() -> mark true(), active prod(s X, Y) -> mark add(Y, prod(X, Y)), active prod(0(), X) -> mark 0(), active fact X -> mark if(zero X, s 0(), prod(X, fact p X)), active p s X -> mark X, active add(s X, Y) -> mark s add(X, Y), active add(0(), X) -> mark X, add(X1, mark X2) -> add(X1, X2), add(X1, active X2) -> add(X1, X2), add(mark X1, X2) -> add(X1, X2), add(active X1, X2) -> add(X1, X2)} Open SCC (2): Strict: { zero# mark X -> zero# X, zero# active X -> zero# X} Weak: { mark if(X1, X2, X3) -> active if(mark X1, X2, X3), mark zero X -> active zero mark X, mark s X -> active s mark X, mark 0() -> active 0(), mark prod(X1, X2) -> active prod(mark X1, mark X2), mark fact X -> active fact mark X, mark p X -> active p mark X, mark add(X1, X2) -> active add(mark X1, mark X2), mark true() -> active true(), mark false() -> active false(), 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), zero mark X -> zero X, zero active X -> zero X, s mark X -> s X, s active X -> s X, prod(X1, mark X2) -> prod(X1, X2), prod(X1, active X2) -> prod(X1, X2), prod(mark X1, X2) -> prod(X1, X2), prod(active X1, X2) -> prod(X1, X2), fact mark X -> fact X, fact active X -> fact X, p mark X -> p X, p active X -> p X, active if(true(), X, Y) -> mark X, active if(false(), X, Y) -> mark Y, active zero s X -> mark false(), active zero 0() -> mark true(), active prod(s X, Y) -> mark add(Y, prod(X, Y)), active prod(0(), X) -> mark 0(), active fact X -> mark if(zero X, s 0(), prod(X, fact p X)), active p s X -> mark X, active add(s X, Y) -> mark s add(X, Y), active add(0(), X) -> mark X, add(X1, mark X2) -> add(X1, X2), add(X1, active X2) -> add(X1, X2), add(mark X1, X2) -> add(X1, X2), add(active X1, X2) -> add(X1, X2)} Open