MAYBE Time: 0.011247 TRS: { D t() -> s h(), D constant() -> h(), D b(x, y) -> b(D x, D y), D c(x, y) -> b(c(y, D x), c(x, D y)), D m(x, y) -> m(D x, D y), D opp x -> opp D x, D div(x, y) -> m(div(D x, y), div(c(x, D y), pow(y, 2()))), D pow(x, y) -> b(c(c(y, pow(x, m(y, 1()))), D x), c(c(pow(x, y), ln x), D y)), D ln x -> div(D x, x), b(x, h()) -> x, b(s x, s y) -> s s b(x, y), b(h(), x) -> x, b(b(x, y), z) -> b(x, b(y, z))} DP: DP: { D# b(x, y) -> D# x, D# b(x, y) -> D# y, D# b(x, y) -> b#(D x, D y), D# c(x, y) -> D# x, D# c(x, y) -> D# y, D# c(x, y) -> b#(c(y, D x), c(x, D y)), D# m(x, y) -> D# x, D# m(x, y) -> D# y, D# opp x -> D# x, D# div(x, y) -> D# x, D# div(x, y) -> D# y, D# pow(x, y) -> D# x, D# pow(x, y) -> D# y, D# pow(x, y) -> b#(c(c(y, pow(x, m(y, 1()))), D x), c(c(pow(x, y), ln x), D y)), D# ln x -> D# x, b#(s x, s y) -> b#(x, y), b#(b(x, y), z) -> b#(x, b(y, z)), b#(b(x, y), z) -> b#(y, z)} TRS: { D t() -> s h(), D constant() -> h(), D b(x, y) -> b(D x, D y), D c(x, y) -> b(c(y, D x), c(x, D y)), D m(x, y) -> m(D x, D y), D opp x -> opp D x, D div(x, y) -> m(div(D x, y), div(c(x, D y), pow(y, 2()))), D pow(x, y) -> b(c(c(y, pow(x, m(y, 1()))), D x), c(c(pow(x, y), ln x), D y)), D ln x -> div(D x, x), b(x, h()) -> x, b(s x, s y) -> s s b(x, y), b(h(), x) -> x, b(b(x, y), z) -> b(x, b(y, z))} EDG: {(D# c(x, y) -> D# y, D# ln x -> D# x) (D# c(x, y) -> D# y, D# pow(x, y) -> b#(c(c(y, pow(x, m(y, 1()))), D x), c(c(pow(x, y), ln x), D y))) (D# c(x, y) -> D# y, D# pow(x, y) -> D# y) (D# c(x, y) -> D# y, D# pow(x, y) -> D# x) (D# c(x, y) -> D# y, D# div(x, y) -> D# y) (D# c(x, y) -> D# y, D# div(x, y) -> D# x) (D# c(x, y) -> D# y, D# opp x -> D# x) (D# c(x, y) -> D# y, D# m(x, y) -> D# y) (D# c(x, y) -> D# y, D# m(x, y) -> D# x) (D# c(x, y) -> D# y, D# c(x, y) -> b#(c(y, D x), c(x, D y))) (D# c(x, y) -> D# y, D# c(x, y) -> D# y) (D# c(x, y) -> D# y, D# c(x, y) -> D# x) (D# c(x, y) -> D# y, D# b(x, y) -> b#(D x, D y)) (D# c(x, y) -> D# y, D# b(x, y) -> D# y) (D# c(x, y) -> D# y, D# b(x, y) -> D# x) (D# div(x, y) -> D# y, D# ln x -> D# x) (D# div(x, y) -> D# y, D# pow(x, y) -> b#(c(c(y, pow(x, m(y, 1()))), D x), c(c(pow(x, y), ln x), D y))) (D# div(x, y) -> D# y, D# pow(x, y) -> D# y) (D# div(x, y) -> D# y, D# pow(x, y) -> D# x) (D# div(x, y) -> D# y, D# div(x, y) -> D# y) (D# div(x, y) -> D# y, D# div(x, y) -> D# x) (D# div(x, y) -> D# y, D# opp x -> D# x) (D# div(x, y) -> D# y, D# m(x, y) -> D# y) (D# div(x, y) -> D# y, D# m(x, y) -> D# x) (D# div(x, y) -> D# y, D# c(x, y) -> b#(c(y, D x), c(x, D y))) (D# div(x, y) -> D# y, D# c(x, y) -> D# y) (D# div(x, y) -> D# y, D# c(x, y) -> D# x) (D# div(x, y) -> D# y, D# b(x, y) -> b#(D x, D y)) (D# div(x, y) -> D# y, D# b(x, y) -> D# y) (D# div(x, y) -> D# y, D# b(x, y) -> D# x) (b#(b(x, y), z) -> b#(x, b(y, z)), b#(b(x, y), z) -> b#(y, z)) (b#(b(x, y), z) -> b#(x, b(y, z)), b#(b(x, y), z) -> b#(x, b(y, z))) (b#(b(x, y), z) -> b#(x, b(y, z)), b#(s x, s y) -> b#(x, y)) (D# b(x, y) -> D# x, D# ln x -> D# x) (D# b(x, y) -> D# x, D# pow(x, y) -> b#(c(c(y, pow(x, m(y, 1()))), D x), c(c(pow(x, y), ln x), D y))) (D# b(x, y) -> D# x, D# pow(x, y) -> D# y) (D# b(x, y) -> D# x, D# pow(x, y) -> D# x) (D# b(x, y) -> D# x, D# div(x, y) -> D# y) (D# b(x, y) -> D# x, D# div(x, y) -> D# x) (D# b(x, y) -> D# x, D# opp x -> D# x) (D# b(x, y) -> D# x, D# m(x, y) -> D# y) (D# b(x, y) -> D# x, D# m(x, y) -> D# x) (D# b(x, y) -> D# x, D# c(x, y) -> b#(c(y, D x), c(x, D y))) (D# b(x, y) -> D# x, D# c(x, y) -> D# y) (D# b(x, y) -> D# x, D# c(x, y) -> D# x) (D# b(x, y) -> D# x, D# b(x, y) -> b#(D x, D y)) (D# b(x, y) -> D# x, D# b(x, y) -> D# y) (D# b(x, y) -> D# x, D# b(x, y) -> D# x) (D# m(x, y) -> D# x, D# ln x -> D# x) (D# m(x, y) -> D# x, D# pow(x, y) -> b#(c(c(y, pow(x, m(y, 1()))), D x), c(c(pow(x, y), ln x), D y))) (D# m(x, y) -> D# x, D# pow(x, y) -> D# y) (D# m(x, y) -> D# x, D# pow(x, y) -> D# x) (D# m(x, y) -> D# x, D# div(x, y) -> D# y) (D# m(x, y) -> D# x, D# div(x, y) -> D# x) (D# m(x, y) -> D# x, D# opp x -> D# x) (D# m(x, y) -> D# x, D# m(x, y) -> D# y) (D# m(x, y) -> D# x, D# m(x, y) -> D# x) (D# m(x, y) -> D# x, D# c(x, y) -> b#(c(y, D x), c(x, D y))) (D# m(x, y) -> D# x, D# c(x, y) -> D# y) (D# m(x, y) -> D# x, D# c(x, y) -> D# x) (D# m(x, y) -> D# x, D# b(x, y) -> b#(D x, D y)) (D# m(x, y) -> D# x, D# b(x, y) -> D# y) (D# m(x, y) -> D# x, D# b(x, y) -> D# x) (D# div(x, y) -> D# x, D# ln x -> D# x) (D# div(x, y) -> D# x, D# pow(x, y) -> b#(c(c(y, pow(x, m(y, 1()))), D x), c(c(pow(x, y), ln x), D y))) (D# div(x, y) -> D# x, D# pow(x, y) -> D# y) (D# div(x, y) -> D# x, D# pow(x, y) -> D# x) (D# div(x, y) -> D# x, D# div(x, y) -> D# y) (D# div(x, y) -> D# x, D# div(x, y) -> D# x) (D# div(x, y) -> D# x, D# opp x -> D# x) (D# div(x, y) -> D# x, D# m(x, y) -> D# y) (D# div(x, y) -> D# x, D# m(x, y) -> D# x) (D# div(x, y) -> D# x, D# c(x, y) -> b#(c(y, D x), c(x, D y))) (D# div(x, y) -> D# x, D# c(x, y) -> D# y) (D# div(x, y) -> D# x, D# c(x, y) -> D# x) (D# div(x, y) -> D# x, D# b(x, y) -> b#(D x, D y)) (D# div(x, y) -> D# x, D# b(x, y) -> D# y) (D# div(x, y) -> D# x, D# b(x, y) -> D# x) (D# ln x -> D# x, D# ln x -> D# x) (D# ln x -> D# x, D# pow(x, y) -> b#(c(c(y, pow(x, m(y, 1()))), D x), c(c(pow(x, y), ln x), D y))) (D# ln x -> D# x, D# pow(x, y) -> D# y) (D# ln x -> D# x, D# pow(x, y) -> D# x) (D# ln x -> D# x, D# div(x, y) -> D# y) (D# ln x -> D# x, D# div(x, y) -> D# x) (D# ln x -> D# x, D# opp x -> D# x) (D# ln x -> D# x, D# m(x, y) -> D# y) (D# ln x -> D# x, D# m(x, y) -> D# x) (D# ln x -> D# x, D# c(x, y) -> b#(c(y, D x), c(x, D y))) (D# ln x -> D# x, D# c(x, y) -> D# y) (D# ln x -> D# x, D# c(x, y) -> D# x) (D# ln x -> D# x, D# b(x, y) -> b#(D x, D y)) (D# ln x -> D# x, D# b(x, y) -> D# y) (D# ln x -> D# x, D# b(x, y) -> D# x) (b#(s x, s y) -> b#(x, y), b#(b(x, y), z) -> b#(y, z)) (b#(s x, s y) -> b#(x, y), b#(b(x, y), z) -> b#(x, b(y, z))) (b#(s x, s y) -> b#(x, y), b#(s x, s y) -> b#(x, y)) (b#(b(x, y), z) -> b#(y, z), b#(s x, s y) -> b#(x, y)) (b#(b(x, y), z) -> b#(y, z), b#(b(x, y), z) -> b#(x, b(y, z))) (b#(b(x, y), z) -> b#(y, z), b#(b(x, y), z) -> b#(y, z)) (D# pow(x, y) -> D# x, D# b(x, y) -> D# x) (D# pow(x, y) -> D# x, D# b(x, y) -> D# y) (D# pow(x, y) -> D# x, D# b(x, y) -> b#(D x, D y)) (D# pow(x, y) -> D# x, D# c(x, y) -> D# x) (D# pow(x, y) -> D# x, D# c(x, y) -> D# y) (D# pow(x, y) -> D# x, D# c(x, y) -> b#(c(y, D x), c(x, D y))) (D# pow(x, y) -> D# x, D# m(x, y) -> D# x) (D# pow(x, y) -> D# x, D# m(x, y) -> D# y) (D# pow(x, y) -> D# x, D# opp x -> D# x) (D# pow(x, y) -> D# x, D# div(x, y) -> D# x) (D# pow(x, y) -> D# x, D# div(x, y) -> D# y) (D# pow(x, y) -> D# x, D# pow(x, y) -> D# x) (D# pow(x, y) -> D# x, D# pow(x, y) -> D# y) (D# pow(x, y) -> D# x, D# pow(x, y) -> b#(c(c(y, pow(x, m(y, 1()))), D x), c(c(pow(x, y), ln x), D y))) (D# pow(x, y) -> D# x, D# ln x -> D# x) (D# opp x -> D# x, D# b(x, y) -> D# x) (D# opp x -> D# x, D# b(x, y) -> D# y) (D# opp x -> D# x, D# b(x, y) -> b#(D x, D y)) (D# opp x -> D# x, D# c(x, y) -> D# x) (D# opp x -> D# x, D# c(x, y) -> D# y) (D# opp x -> D# x, D# c(x, y) -> b#(c(y, D x), c(x, D y))) (D# opp x -> D# x, D# m(x, y) -> D# x) (D# opp x -> D# x, D# m(x, y) -> D# y) (D# opp x -> D# x, D# opp x -> D# x) (D# opp x -> D# x, D# div(x, y) -> D# x) (D# opp x -> D# x, D# div(x, y) -> D# y) (D# opp x -> D# x, D# pow(x, y) -> D# x) (D# opp x -> D# x, D# pow(x, y) -> D# y) (D# opp x -> D# x, D# pow(x, y) -> b#(c(c(y, pow(x, m(y, 1()))), D x), c(c(pow(x, y), ln x), D y))) (D# opp x -> D# x, D# ln x -> D# x) (D# c(x, y) -> D# x, D# b(x, y) -> D# x) (D# c(x, y) -> D# x, D# b(x, y) -> D# y) (D# c(x, y) -> D# x, D# b(x, y) -> b#(D x, D y)) (D# c(x, y) -> D# x, D# c(x, y) -> D# x) (D# c(x, y) -> D# x, D# c(x, y) -> D# y) (D# c(x, y) -> D# x, D# c(x, y) -> b#(c(y, D x), c(x, D y))) (D# c(x, y) -> D# x, D# m(x, y) -> D# x) (D# c(x, y) -> D# x, D# m(x, y) -> D# y) (D# c(x, y) -> D# x, D# opp x -> D# x) (D# c(x, y) -> D# x, D# div(x, y) -> D# x) (D# c(x, y) -> D# x, D# div(x, y) -> D# y) (D# c(x, y) -> D# x, D# pow(x, y) -> D# x) (D# c(x, y) -> D# x, D# pow(x, y) -> D# y) (D# c(x, y) -> D# x, D# pow(x, y) -> b#(c(c(y, pow(x, m(y, 1()))), D x), c(c(pow(x, y), ln x), D y))) (D# c(x, y) -> D# x, D# ln x -> D# x) (D# b(x, y) -> b#(D x, D y), b#(s x, s y) -> b#(x, y)) (D# b(x, y) -> b#(D x, D y), b#(b(x, y), z) -> b#(x, b(y, z))) (D# b(x, y) -> b#(D x, D y), b#(b(x, y), z) -> b#(y, z)) (D# pow(x, y) -> D# y, D# b(x, y) -> D# x) (D# pow(x, y) -> D# y, D# b(x, y) -> D# y) (D# pow(x, y) -> D# y, D# b(x, y) -> b#(D x, D y)) (D# pow(x, y) -> D# y, D# c(x, y) -> D# x) (D# pow(x, y) -> D# y, D# c(x, y) -> D# y) (D# pow(x, y) -> D# y, D# c(x, y) -> b#(c(y, D x), c(x, D y))) (D# pow(x, y) -> D# y, D# m(x, y) -> D# x) (D# pow(x, y) -> D# y, D# m(x, y) -> D# y) (D# pow(x, y) -> D# y, D# opp x -> D# x) (D# pow(x, y) -> D# y, D# div(x, y) -> D# x) (D# pow(x, y) -> D# y, D# div(x, y) -> D# y) (D# pow(x, y) -> D# y, D# pow(x, y) -> D# x) (D# pow(x, y) -> D# y, D# pow(x, y) -> D# y) (D# pow(x, y) -> D# y, D# pow(x, y) -> b#(c(c(y, pow(x, m(y, 1()))), D x), c(c(pow(x, y), ln x), D y))) (D# pow(x, y) -> D# y, D# ln x -> D# x) (D# m(x, y) -> D# y, D# b(x, y) -> D# x) (D# m(x, y) -> D# y, D# b(x, y) -> D# y) (D# m(x, y) -> D# y, D# b(x, y) -> b#(D x, D y)) (D# m(x, y) -> D# y, D# c(x, y) -> D# x) (D# m(x, y) -> D# y, D# c(x, y) -> D# y) (D# m(x, y) -> D# y, D# c(x, y) -> b#(c(y, D x), c(x, D y))) (D# m(x, y) -> D# y, D# m(x, y) -> D# x) (D# m(x, y) -> D# y, D# m(x, y) -> D# y) (D# m(x, y) -> D# y, D# opp x -> D# x) (D# m(x, y) -> D# y, D# div(x, y) -> D# x) (D# m(x, y) -> D# y, D# div(x, y) -> D# y) (D# m(x, y) -> D# y, D# pow(x, y) -> D# x) (D# m(x, y) -> D# y, D# pow(x, y) -> D# y) (D# m(x, y) -> D# y, D# pow(x, y) -> b#(c(c(y, pow(x, m(y, 1()))), D x), c(c(pow(x, y), ln x), D y))) (D# m(x, y) -> D# y, D# ln x -> D# x) (D# b(x, y) -> D# y, D# b(x, y) -> D# x) (D# b(x, y) -> D# y, D# b(x, y) -> D# y) (D# b(x, y) -> D# y, D# b(x, y) -> b#(D x, D y)) (D# b(x, y) -> D# y, D# c(x, y) -> D# x) (D# b(x, y) -> D# y, D# c(x, y) -> D# y) (D# b(x, y) -> D# y, D# c(x, y) -> b#(c(y, D x), c(x, D y))) (D# b(x, y) -> D# y, D# m(x, y) -> D# x) (D# b(x, y) -> D# y, D# m(x, y) -> D# y) (D# b(x, y) -> D# y, D# opp x -> D# x) (D# b(x, y) -> D# y, D# div(x, y) -> D# x) (D# b(x, y) -> D# y, D# div(x, y) -> D# y) (D# b(x, y) -> D# y, D# pow(x, y) -> D# x) (D# b(x, y) -> D# y, D# pow(x, y) -> D# y) (D# b(x, y) -> D# y, D# pow(x, y) -> b#(c(c(y, pow(x, m(y, 1()))), D x), c(c(pow(x, y), ln x), D y))) (D# b(x, y) -> D# y, D# ln x -> D# x)} STATUS: arrows: 0.407407 SCCS (2): Scc: { D# b(x, y) -> D# x, D# b(x, y) -> D# y, D# c(x, y) -> D# x, D# c(x, y) -> D# y, D# m(x, y) -> D# x, D# m(x, y) -> D# y, D# opp x -> D# x, D# div(x, y) -> D# x, D# div(x, y) -> D# y, D# pow(x, y) -> D# x, D# pow(x, y) -> D# y, D# ln x -> D# x} Scc: { b#(s x, s y) -> b#(x, y), b#(b(x, y), z) -> b#(x, b(y, z)), b#(b(x, y), z) -> b#(y, z)} SCC (12): Strict: { D# b(x, y) -> D# x, D# b(x, y) -> D# y, D# c(x, y) -> D# x, D# c(x, y) -> D# y, D# m(x, y) -> D# x, D# m(x, y) -> D# y, D# opp x -> D# x, D# div(x, y) -> D# x, D# div(x, y) -> D# y, D# pow(x, y) -> D# x, D# pow(x, y) -> D# y, D# ln x -> D# x} Weak: { D t() -> s h(), D constant() -> h(), D b(x, y) -> b(D x, D y), D c(x, y) -> b(c(y, D x), c(x, D y)), D m(x, y) -> m(D x, D y), D opp x -> opp D x, D div(x, y) -> m(div(D x, y), div(c(x, D y), pow(y, 2()))), D pow(x, y) -> b(c(c(y, pow(x, m(y, 1()))), D x), c(c(pow(x, y), ln x), D y)), D ln x -> div(D x, x), b(x, h()) -> x, b(s x, s y) -> s s b(x, y), b(h(), x) -> x, b(b(x, y), z) -> b(x, b(y, z))} Open SCC (3): Strict: { b#(s x, s y) -> b#(x, y), b#(b(x, y), z) -> b#(x, b(y, z)), b#(b(x, y), z) -> b#(y, z)} Weak: { D t() -> s h(), D constant() -> h(), D b(x, y) -> b(D x, D y), D c(x, y) -> b(c(y, D x), c(x, D y)), D m(x, y) -> m(D x, D y), D opp x -> opp D x, D div(x, y) -> m(div(D x, y), div(c(x, D y), pow(y, 2()))), D pow(x, y) -> b(c(c(y, pow(x, m(y, 1()))), D x), c(c(pow(x, y), ln x), D y)), D ln x -> div(D x, x), b(x, h()) -> x, b(s x, s y) -> s s b(x, y), b(h(), x) -> x, b(b(x, y), z) -> b(x, b(y, z))} Open