YES Time: 0.026036 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: DP: { 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} 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)} 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 (1): 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 (12): 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# BETA, dx# ln ALPHA -> dx# ALPHA) (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# 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# 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# 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) (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# 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# ln ALPHA -> dx# ALPHA)} SCCS (1): 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 (11): 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# 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# 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# 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) (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)} SCCS (1): 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 (10): 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# 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# ln ALPHA -> dx# ALPHA} EDG: {(dx# times(ALPHA, BETA) -> dx# BETA, dx# ln ALPHA -> dx# ALPHA) (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# plus(ALPHA, BETA) -> dx# ALPHA, dx# ln ALPHA -> dx# ALPHA) (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# 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# 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# 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# 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# 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# 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# 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# ln ALPHA -> dx# ALPHA)} SCCS (1): 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# ln ALPHA -> dx# ALPHA} SCC (9): 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# 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# 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# 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# 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# 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# 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# 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# 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# 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# 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# 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# ln ALPHA -> dx# ALPHA)} SCCS (1): 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# ln ALPHA -> dx# ALPHA} SCC (8): 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# 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# ln ALPHA -> dx# ALPHA} EDG: {(dx# times(ALPHA, BETA) -> dx# BETA, dx# ln 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# plus(ALPHA, BETA) -> dx# ALPHA, dx# ln 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# 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# 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# 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# 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# 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# ln ALPHA -> dx# ALPHA)} SCCS (1): 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# ln ALPHA -> dx# ALPHA} SCC (7): 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# 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# ln ALPHA -> dx# ALPHA} EDG: {(dx# times(ALPHA, BETA) -> dx# BETA, dx# ln 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# times(ALPHA, BETA) -> dx# BETA, dx# plus(ALPHA, BETA) -> dx# ALPHA) (dx# times(ALPHA, BETA) -> dx# ALPHA, dx# ln ALPHA -> dx# ALPHA) (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# ln ALPHA -> dx# ALPHA, dx# ln 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# ln ALPHA -> dx# ALPHA, dx# plus(ALPHA, BETA) -> 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# 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# 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# ln ALPHA -> dx# ALPHA)} SCCS (1): 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# ln ALPHA -> dx# ALPHA} SCC (6): 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# 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# ln ALPHA -> dx# ALPHA} EDG: {(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# times(ALPHA, BETA) -> dx# BETA, dx# plus(ALPHA, BETA) -> dx# ALPHA) (dx# times(ALPHA, BETA) -> dx# ALPHA, dx# ln ALPHA -> 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# 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# 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# 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# ln ALPHA -> dx# ALPHA)} SCCS (1): 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# ln ALPHA -> dx# ALPHA} SCC (5): 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# 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# ln ALPHA -> dx# ALPHA} EDG: {(dx# plus(ALPHA, BETA) -> dx# ALPHA, dx# ln ALPHA -> dx# ALPHA) (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# ln ALPHA -> dx# ALPHA, dx# ln ALPHA -> dx# ALPHA) (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# 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# 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# ln ALPHA -> dx# ALPHA)} SCCS (1): Scc: { dx# plus(ALPHA, BETA) -> dx# ALPHA, dx# plus(ALPHA, BETA) -> dx# BETA, dx# times(ALPHA, BETA) -> dx# ALPHA, dx# ln ALPHA -> dx# ALPHA} SCC (4): Strict: { dx# plus(ALPHA, BETA) -> dx# ALPHA, dx# plus(ALPHA, BETA) -> dx# BETA, dx# times(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# ln ALPHA -> dx# ALPHA} EDG: {(dx# plus(ALPHA, BETA) -> dx# ALPHA, dx# ln ALPHA -> 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# 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# 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# ln ALPHA -> dx# ALPHA)} SCCS (1): Scc: {dx# plus(ALPHA, BETA) -> dx# ALPHA, dx# plus(ALPHA, BETA) -> dx# BETA, dx# ln ALPHA -> dx# ALPHA} SCC (3): Strict: {dx# plus(ALPHA, BETA) -> dx# ALPHA, dx# plus(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# ln ALPHA -> dx# ALPHA} EDG: {(dx# ln ALPHA -> dx# ALPHA, dx# ln ALPHA -> 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# ALPHA, dx# ln ALPHA -> dx# ALPHA)} SCCS (1): Scc: {dx# plus(ALPHA, BETA) -> dx# ALPHA, dx# ln ALPHA -> dx# ALPHA} SCC (2): Strict: {dx# plus(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# ln ALPHA -> dx# ALPHA} EDG: {(dx# ln ALPHA -> dx# ALPHA, dx# ln ALPHA -> dx# ALPHA)} SCCS (1): Scc: {dx# ln ALPHA -> dx# ALPHA} SCC (1): Strict: {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: {} Qed