YES TRS: { dx(X) -> one(), dx(a()) -> zero(), dx(plus(ALPHA, BETA)) -> plus(dx(ALPHA), dx(BETA)), dx(times(ALPHA, BETA)) -> plus(times(BETA, dx(ALPHA)), times(ALPHA, dx(BETA))), dx(minus(ALPHA, BETA)) -> minus(dx(ALPHA), dx(BETA)), dx(neg(ALPHA)) -> neg(dx(ALPHA)), dx(div(ALPHA, BETA)) -> minus(div(dx(ALPHA), BETA), times(ALPHA, div(dx(BETA), exp(BETA, two())))), dx(exp(ALPHA, BETA)) -> plus(times(BETA, times(exp(ALPHA, minus(BETA, one())), dx(ALPHA))), times(exp(ALPHA, BETA), times(ln(ALPHA), dx(BETA)))), dx(ln(ALPHA)) -> div(dx(ALPHA), ALPHA)} DP: Strict: { dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(exp(ALPHA, BETA)) -> dx#(ALPHA), dx#(exp(ALPHA, BETA)) -> dx#(BETA), dx#(ln(ALPHA)) -> dx#(ALPHA)} Weak: { dx(X) -> one(), dx(a()) -> zero(), dx(plus(ALPHA, BETA)) -> plus(dx(ALPHA), dx(BETA)), dx(times(ALPHA, BETA)) -> plus(times(BETA, dx(ALPHA)), times(ALPHA, dx(BETA))), dx(minus(ALPHA, BETA)) -> minus(dx(ALPHA), dx(BETA)), dx(neg(ALPHA)) -> neg(dx(ALPHA)), dx(div(ALPHA, BETA)) -> minus(div(dx(ALPHA), BETA), times(ALPHA, div(dx(BETA), exp(BETA, two())))), dx(exp(ALPHA, BETA)) -> plus(times(BETA, times(exp(ALPHA, minus(BETA, one())), dx(ALPHA))), times(exp(ALPHA, BETA), times(ln(ALPHA), dx(BETA)))), dx(ln(ALPHA)) -> div(dx(ALPHA), ALPHA)} EDG: { (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(ln(ALPHA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(exp(ALPHA, BETA)) -> dx#(BETA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(exp(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(BETA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(neg(ALPHA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(BETA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(ln(ALPHA)) -> dx#(ALPHA)) (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(exp(ALPHA, BETA)) -> dx#(BETA)) (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(exp(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(BETA)) (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(neg(ALPHA)) -> dx#(ALPHA)) (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(BETA)) (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA)) (dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(exp(ALPHA, BETA)) -> dx#(BETA)) (dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(exp(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(BETA)) (dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA)) (dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA)) (dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(exp(ALPHA, BETA)) -> dx#(BETA)) (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(exp(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(BETA)) (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA)) (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA)) (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(exp(ALPHA, BETA)) -> dx#(BETA)) (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(exp(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(BETA)) (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA)) (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA)) (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA)) (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(exp(ALPHA, BETA)) -> dx#(BETA)) (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(exp(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(BETA)) (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA)) (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA)) (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(exp(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(exp(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(exp(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(exp(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(exp(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(exp(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA)) (dx#(exp(ALPHA, BETA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA)) (dx#(exp(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(exp(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(BETA)) (dx#(exp(ALPHA, BETA)) -> dx#(ALPHA), dx#(exp(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(exp(ALPHA, BETA)) -> dx#(ALPHA), dx#(exp(ALPHA, BETA)) -> dx#(BETA)) (dx#(exp(ALPHA, BETA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA)) (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA)) (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA)) (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(BETA)) (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(exp(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(exp(ALPHA, BETA)) -> dx#(BETA)) (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(BETA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(exp(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(exp(ALPHA, BETA)) -> dx#(BETA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA)) (dx#(exp(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(exp(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(exp(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(exp(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(exp(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(exp(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(BETA)) (dx#(exp(ALPHA, BETA)) -> dx#(BETA), dx#(neg(ALPHA)) -> dx#(ALPHA)) (dx#(exp(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(exp(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(BETA)) (dx#(exp(ALPHA, BETA)) -> dx#(BETA), dx#(exp(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(exp(ALPHA, BETA)) -> dx#(BETA), dx#(exp(ALPHA, BETA)) -> dx#(BETA)) (dx#(exp(ALPHA, BETA)) -> dx#(BETA), dx#(ln(ALPHA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(BETA)) (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(neg(ALPHA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(BETA)) (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(exp(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(exp(ALPHA, BETA)) -> dx#(BETA)) (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(ln(ALPHA)) -> dx#(ALPHA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(BETA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(neg(ALPHA)) -> dx#(ALPHA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(BETA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(exp(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(exp(ALPHA, BETA)) -> dx#(BETA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(ln(ALPHA)) -> dx#(ALPHA)) } SCCS: Scc: { dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(exp(ALPHA, BETA)) -> dx#(ALPHA), dx#(exp(ALPHA, BETA)) -> dx#(BETA), dx#(ln(ALPHA)) -> dx#(ALPHA)} SCC: Strict: { dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(exp(ALPHA, BETA)) -> dx#(ALPHA), dx#(exp(ALPHA, BETA)) -> dx#(BETA), dx#(ln(ALPHA)) -> dx#(ALPHA)} Weak: { dx(X) -> one(), dx(a()) -> zero(), dx(plus(ALPHA, BETA)) -> plus(dx(ALPHA), dx(BETA)), dx(times(ALPHA, BETA)) -> plus(times(BETA, dx(ALPHA)), times(ALPHA, dx(BETA))), dx(minus(ALPHA, BETA)) -> minus(dx(ALPHA), dx(BETA)), dx(neg(ALPHA)) -> neg(dx(ALPHA)), dx(div(ALPHA, BETA)) -> minus(div(dx(ALPHA), BETA), times(ALPHA, div(dx(BETA), exp(BETA, two())))), dx(exp(ALPHA, BETA)) -> plus(times(BETA, times(exp(ALPHA, minus(BETA, one())), dx(ALPHA))), times(exp(ALPHA, BETA), times(ln(ALPHA), dx(BETA)))), dx(ln(ALPHA)) -> div(dx(ALPHA), ALPHA)} SPSC: Simple Projection: pi(dx#) = 0 Strict: { dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(exp(ALPHA, BETA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA)} EDG: {(dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(exp(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(BETA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA)) (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(exp(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(BETA)) (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA)) (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA)) (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(exp(ALPHA, BETA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA)) (dx#(exp(ALPHA, BETA)) -> dx#(ALPHA), dx#(exp(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(exp(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(BETA)) (dx#(exp(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(exp(ALPHA, BETA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA)) (dx#(exp(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA)) (dx#(exp(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(exp(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(exp(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(exp(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(exp(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(ln(ALPHA)) -> dx#(ALPHA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(exp(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(BETA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(neg(ALPHA)) -> dx#(ALPHA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(BETA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(ln(ALPHA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(exp(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(BETA)) (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(neg(ALPHA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(BETA)) (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(BETA)) (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(neg(ALPHA)) -> dx#(ALPHA)) (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(BETA)) (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(exp(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(ln(ALPHA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(BETA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(neg(ALPHA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(BETA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(exp(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(ln(ALPHA)) -> dx#(ALPHA)) (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA)) (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA)) (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(BETA)) (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(exp(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA)) (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA)) (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA)) (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(BETA)) (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(exp(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA)) (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(BETA)) (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(exp(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA)) (dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA)) (dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA)) (dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(BETA)) (dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(exp(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA))} SCCS: Scc: { dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(exp(ALPHA, BETA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA)} SCC: Strict: { dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(exp(ALPHA, BETA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA)} Weak: { dx(X) -> one(), dx(a()) -> zero(), dx(plus(ALPHA, BETA)) -> plus(dx(ALPHA), dx(BETA)), dx(times(ALPHA, BETA)) -> plus(times(BETA, dx(ALPHA)), times(ALPHA, dx(BETA))), dx(minus(ALPHA, BETA)) -> minus(dx(ALPHA), dx(BETA)), dx(neg(ALPHA)) -> neg(dx(ALPHA)), dx(div(ALPHA, BETA)) -> minus(div(dx(ALPHA), BETA), times(ALPHA, div(dx(BETA), exp(BETA, two())))), dx(exp(ALPHA, BETA)) -> plus(times(BETA, times(exp(ALPHA, minus(BETA, one())), dx(ALPHA))), times(exp(ALPHA, BETA), times(ln(ALPHA), dx(BETA)))), dx(ln(ALPHA)) -> div(dx(ALPHA), ALPHA)} SPSC: Simple Projection: pi(dx#) = 0 Strict: { dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(ln(ALPHA)) -> dx#(ALPHA)} EDG: {(dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(BETA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA)) (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(BETA)) (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA)) (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA)) (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA)) (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(BETA)) (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA)) (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA)) (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(ln(ALPHA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(BETA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(neg(ALPHA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(BETA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(ln(ALPHA)) -> dx#(ALPHA)) (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(BETA)) (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(neg(ALPHA)) -> dx#(ALPHA)) (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(BETA)) (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(BETA)) (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(neg(ALPHA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(BETA)) (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(ln(ALPHA)) -> dx#(ALPHA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(BETA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(neg(ALPHA)) -> dx#(ALPHA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(BETA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(ln(ALPHA)) -> dx#(ALPHA)) (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA)) (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA)) (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(BETA)) (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA)) (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(BETA)) (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA)) (dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA)) (dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA)) (dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(BETA)) (dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA))} SCCS: Scc: { dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(ln(ALPHA)) -> dx#(ALPHA)} SCC: Strict: { dx#(plus(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(ln(ALPHA)) -> dx#(ALPHA)} Weak: { dx(X) -> one(), dx(a()) -> zero(), dx(plus(ALPHA, BETA)) -> plus(dx(ALPHA), dx(BETA)), dx(times(ALPHA, BETA)) -> plus(times(BETA, dx(ALPHA)), times(ALPHA, dx(BETA))), dx(minus(ALPHA, BETA)) -> minus(dx(ALPHA), dx(BETA)), dx(neg(ALPHA)) -> neg(dx(ALPHA)), dx(div(ALPHA, BETA)) -> minus(div(dx(ALPHA), BETA), times(ALPHA, div(dx(BETA), exp(BETA, two())))), dx(exp(ALPHA, BETA)) -> plus(times(BETA, times(exp(ALPHA, minus(BETA, one())), dx(ALPHA))), times(exp(ALPHA, BETA), times(ln(ALPHA), dx(BETA)))), dx(ln(ALPHA)) -> div(dx(ALPHA), ALPHA)} SPSC: Simple Projection: pi(dx#) = 0 Strict: { dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(ln(ALPHA)) -> dx#(ALPHA)} EDG: {(dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(BETA)) (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA)) (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA)) (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(BETA)) (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA)) (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA)) (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(ln(ALPHA)) -> dx#(ALPHA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(BETA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(neg(ALPHA)) -> dx#(ALPHA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(BETA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(ln(ALPHA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(BETA)) (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(neg(ALPHA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(BETA)) (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(BETA)) (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(neg(ALPHA)) -> dx#(ALPHA)) (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(BETA)) (dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(ln(ALPHA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(BETA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(neg(ALPHA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(BETA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(ln(ALPHA)) -> dx#(ALPHA)) (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA)) (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA)) (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(BETA)) (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA)) (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA)) (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA)) (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(BETA)) (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(BETA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA))} SCCS: Scc: { dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(ln(ALPHA)) -> dx#(ALPHA)} SCC: Strict: { dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(BETA), dx#(ln(ALPHA)) -> dx#(ALPHA)} Weak: { dx(X) -> one(), dx(a()) -> zero(), dx(plus(ALPHA, BETA)) -> plus(dx(ALPHA), dx(BETA)), dx(times(ALPHA, BETA)) -> plus(times(BETA, dx(ALPHA)), times(ALPHA, dx(BETA))), dx(minus(ALPHA, BETA)) -> minus(dx(ALPHA), dx(BETA)), dx(neg(ALPHA)) -> neg(dx(ALPHA)), dx(div(ALPHA, BETA)) -> minus(div(dx(ALPHA), BETA), times(ALPHA, div(dx(BETA), exp(BETA, two())))), dx(exp(ALPHA, BETA)) -> plus(times(BETA, times(exp(ALPHA, minus(BETA, one())), dx(ALPHA))), times(exp(ALPHA, BETA), times(ln(ALPHA), dx(BETA)))), dx(ln(ALPHA)) -> div(dx(ALPHA), ALPHA)} SPSC: Simple Projection: pi(dx#) = 0 Strict: { dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA)} EDG: {(dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA)) (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA)) (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA)) (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA)) (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(ln(ALPHA)) -> dx#(ALPHA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(neg(ALPHA)) -> dx#(ALPHA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(BETA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(ln(ALPHA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(neg(ALPHA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(BETA)) (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(BETA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(neg(ALPHA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(ln(ALPHA)) -> dx#(ALPHA)) (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA)) (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA)) (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA)) (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA)) (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA)) (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA))} SCCS: Scc: { dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA)} SCC: Strict: { dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(div(ALPHA, BETA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA)} Weak: { dx(X) -> one(), dx(a()) -> zero(), dx(plus(ALPHA, BETA)) -> plus(dx(ALPHA), dx(BETA)), dx(times(ALPHA, BETA)) -> plus(times(BETA, dx(ALPHA)), times(ALPHA, dx(BETA))), dx(minus(ALPHA, BETA)) -> minus(dx(ALPHA), dx(BETA)), dx(neg(ALPHA)) -> neg(dx(ALPHA)), dx(div(ALPHA, BETA)) -> minus(div(dx(ALPHA), BETA), times(ALPHA, div(dx(BETA), exp(BETA, two())))), dx(exp(ALPHA, BETA)) -> plus(times(BETA, times(exp(ALPHA, minus(BETA, one())), dx(ALPHA))), times(exp(ALPHA, BETA), times(ln(ALPHA), dx(BETA)))), dx(ln(ALPHA)) -> div(dx(ALPHA), ALPHA)} SPSC: Simple Projection: pi(dx#) = 0 Strict: { dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA)} EDG: {(dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(ln(ALPHA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(neg(ALPHA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(BETA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA)) (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA)) (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA)) (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA)) (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA)) (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA)) (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(BETA)) (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(neg(ALPHA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(ln(ALPHA)) -> dx#(ALPHA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(BETA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(neg(ALPHA)) -> dx#(ALPHA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(ln(ALPHA)) -> dx#(ALPHA))} SCCS: Scc: { dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA)} SCC: Strict: { dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(BETA), dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA)} Weak: { dx(X) -> one(), dx(a()) -> zero(), dx(plus(ALPHA, BETA)) -> plus(dx(ALPHA), dx(BETA)), dx(times(ALPHA, BETA)) -> plus(times(BETA, dx(ALPHA)), times(ALPHA, dx(BETA))), dx(minus(ALPHA, BETA)) -> minus(dx(ALPHA), dx(BETA)), dx(neg(ALPHA)) -> neg(dx(ALPHA)), dx(div(ALPHA, BETA)) -> minus(div(dx(ALPHA), BETA), times(ALPHA, div(dx(BETA), exp(BETA, two())))), dx(exp(ALPHA, BETA)) -> plus(times(BETA, times(exp(ALPHA, minus(BETA, one())), dx(ALPHA))), times(exp(ALPHA, BETA), times(ln(ALPHA), dx(BETA)))), dx(ln(ALPHA)) -> div(dx(ALPHA), ALPHA)} SPSC: Simple Projection: pi(dx#) = 0 Strict: { dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA)} EDG: {(dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(ln(ALPHA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(neg(ALPHA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA)) (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA)) (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA)) (dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(neg(ALPHA)) -> dx#(ALPHA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(ln(ALPHA)) -> dx#(ALPHA))} SCCS: Scc: { dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA)} SCC: Strict: { dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(neg(ALPHA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA)} Weak: { dx(X) -> one(), dx(a()) -> zero(), dx(plus(ALPHA, BETA)) -> plus(dx(ALPHA), dx(BETA)), dx(times(ALPHA, BETA)) -> plus(times(BETA, dx(ALPHA)), times(ALPHA, dx(BETA))), dx(minus(ALPHA, BETA)) -> minus(dx(ALPHA), dx(BETA)), dx(neg(ALPHA)) -> neg(dx(ALPHA)), dx(div(ALPHA, BETA)) -> minus(div(dx(ALPHA), BETA), times(ALPHA, div(dx(BETA), exp(BETA, two())))), dx(exp(ALPHA, BETA)) -> plus(times(BETA, times(exp(ALPHA, minus(BETA, one())), dx(ALPHA))), times(exp(ALPHA, BETA), times(ln(ALPHA), dx(BETA)))), dx(ln(ALPHA)) -> div(dx(ALPHA), ALPHA)} SPSC: Simple Projection: pi(dx#) = 0 Strict: { dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA)} EDG: {(dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(ln(ALPHA)) -> dx#(ALPHA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(ln(ALPHA)) -> dx#(ALPHA)) (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA))} SCCS: Scc: { dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA)} SCC: Strict: { dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(minus(ALPHA, BETA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA)} Weak: { dx(X) -> one(), dx(a()) -> zero(), dx(plus(ALPHA, BETA)) -> plus(dx(ALPHA), dx(BETA)), dx(times(ALPHA, BETA)) -> plus(times(BETA, dx(ALPHA)), times(ALPHA, dx(BETA))), dx(minus(ALPHA, BETA)) -> minus(dx(ALPHA), dx(BETA)), dx(neg(ALPHA)) -> neg(dx(ALPHA)), dx(div(ALPHA, BETA)) -> minus(div(dx(ALPHA), BETA), times(ALPHA, div(dx(BETA), exp(BETA, two())))), dx(exp(ALPHA, BETA)) -> plus(times(BETA, times(exp(ALPHA, minus(BETA, one())), dx(ALPHA))), times(exp(ALPHA, BETA), times(ln(ALPHA), dx(BETA)))), dx(ln(ALPHA)) -> div(dx(ALPHA), ALPHA)} SPSC: Simple Projection: pi(dx#) = 0 Strict: { dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(ln(ALPHA)) -> dx#(ALPHA)} EDG: {(dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA)) (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(ln(ALPHA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(ln(ALPHA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(ln(ALPHA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(ln(ALPHA)) -> dx#(ALPHA))} SCCS: Scc: { dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(ln(ALPHA)) -> dx#(ALPHA)} SCC: Strict: { dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(ln(ALPHA)) -> dx#(ALPHA)} Weak: { dx(X) -> one(), dx(a()) -> zero(), dx(plus(ALPHA, BETA)) -> plus(dx(ALPHA), dx(BETA)), dx(times(ALPHA, BETA)) -> plus(times(BETA, dx(ALPHA)), times(ALPHA, dx(BETA))), dx(minus(ALPHA, BETA)) -> minus(dx(ALPHA), dx(BETA)), dx(neg(ALPHA)) -> neg(dx(ALPHA)), dx(div(ALPHA, BETA)) -> minus(div(dx(ALPHA), BETA), times(ALPHA, div(dx(BETA), exp(BETA, two())))), dx(exp(ALPHA, BETA)) -> plus(times(BETA, times(exp(ALPHA, minus(BETA, one())), dx(ALPHA))), times(exp(ALPHA, BETA), times(ln(ALPHA), dx(BETA)))), dx(ln(ALPHA)) -> div(dx(ALPHA), ALPHA)} SPSC: Simple Projection: pi(dx#) = 0 Strict: { dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA)} EDG: {(dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(BETA))} SCCS: Scc: { dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA)} SCC: Strict: { dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(ALPHA), dx#(times(ALPHA, BETA)) -> dx#(BETA)} Weak: { dx(X) -> one(), dx(a()) -> zero(), dx(plus(ALPHA, BETA)) -> plus(dx(ALPHA), dx(BETA)), dx(times(ALPHA, BETA)) -> plus(times(BETA, dx(ALPHA)), times(ALPHA, dx(BETA))), dx(minus(ALPHA, BETA)) -> minus(dx(ALPHA), dx(BETA)), dx(neg(ALPHA)) -> neg(dx(ALPHA)), dx(div(ALPHA, BETA)) -> minus(div(dx(ALPHA), BETA), times(ALPHA, div(dx(BETA), exp(BETA, two())))), dx(exp(ALPHA, BETA)) -> plus(times(BETA, times(exp(ALPHA, minus(BETA, one())), dx(ALPHA))), times(exp(ALPHA, BETA), times(ln(ALPHA), dx(BETA)))), dx(ln(ALPHA)) -> div(dx(ALPHA), ALPHA)} SPSC: Simple Projection: pi(dx#) = 0 Strict: { dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(BETA)} EDG: {(dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(BETA)) (dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(plus(ALPHA, BETA)) -> dx#(BETA)) (dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(BETA))} SCCS: Scc: { dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(BETA)} SCC: Strict: { dx#(plus(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(BETA)} Weak: { dx(X) -> one(), dx(a()) -> zero(), dx(plus(ALPHA, BETA)) -> plus(dx(ALPHA), dx(BETA)), dx(times(ALPHA, BETA)) -> plus(times(BETA, dx(ALPHA)), times(ALPHA, dx(BETA))), dx(minus(ALPHA, BETA)) -> minus(dx(ALPHA), dx(BETA)), dx(neg(ALPHA)) -> neg(dx(ALPHA)), dx(div(ALPHA, BETA)) -> minus(div(dx(ALPHA), BETA), times(ALPHA, div(dx(BETA), exp(BETA, two())))), dx(exp(ALPHA, BETA)) -> plus(times(BETA, times(exp(ALPHA, minus(BETA, one())), dx(ALPHA))), times(exp(ALPHA, BETA), times(ln(ALPHA), dx(BETA)))), dx(ln(ALPHA)) -> div(dx(ALPHA), ALPHA)} SPSC: Simple Projection: pi(dx#) = 0 Strict: {dx#(times(ALPHA, BETA)) -> dx#(BETA)} EDG: {(dx#(times(ALPHA, BETA)) -> dx#(BETA), dx#(times(ALPHA, BETA)) -> dx#(BETA))} SCCS: Scc: {dx#(times(ALPHA, BETA)) -> dx#(BETA)} SCC: Strict: {dx#(times(ALPHA, BETA)) -> dx#(BETA)} Weak: { dx(X) -> one(), dx(a()) -> zero(), dx(plus(ALPHA, BETA)) -> plus(dx(ALPHA), dx(BETA)), dx(times(ALPHA, BETA)) -> plus(times(BETA, dx(ALPHA)), times(ALPHA, dx(BETA))), dx(minus(ALPHA, BETA)) -> minus(dx(ALPHA), dx(BETA)), dx(neg(ALPHA)) -> neg(dx(ALPHA)), dx(div(ALPHA, BETA)) -> minus(div(dx(ALPHA), BETA), times(ALPHA, div(dx(BETA), exp(BETA, two())))), dx(exp(ALPHA, BETA)) -> plus(times(BETA, times(exp(ALPHA, minus(BETA, one())), dx(ALPHA))), times(exp(ALPHA, BETA), times(ln(ALPHA), dx(BETA)))), dx(ln(ALPHA)) -> div(dx(ALPHA), ALPHA)} SPSC: Simple Projection: pi(dx#) = 0 Strict: {} Qed