YES Time: 0.139819 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)} UR: {} 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)} STATUS: arrows: 0.000000 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)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [plus](x0, x1) = x0 + x1, [times](x0, x1) = x0 + x1, [minus](x0, x1) = x0 + x1, [div](x0, x1) = x0 + x1, [exp](x0, x1) = x0 + x1, [dx](x0) = 0, [neg](x0) = x0, [ln](x0) = x0 + 1, [one] = 0, [zero] = 0, [a] = 0, [two] = 0, [dx#](x0) = x0 Strict: dx# ln ALPHA -> dx# ALPHA 1 + 1ALPHA >= 0 + 1ALPHA dx# exp(ALPHA, BETA) -> dx# BETA 0 + 1ALPHA + 1BETA >= 0 + 1BETA dx# exp(ALPHA, BETA) -> dx# ALPHA 0 + 1ALPHA + 1BETA >= 0 + 1ALPHA dx# div(ALPHA, BETA) -> dx# BETA 0 + 1ALPHA + 1BETA >= 0 + 1BETA dx# div(ALPHA, BETA) -> dx# ALPHA 0 + 1ALPHA + 1BETA >= 0 + 1ALPHA dx# neg ALPHA -> dx# ALPHA 0 + 1ALPHA >= 0 + 1ALPHA dx# minus(ALPHA, BETA) -> dx# BETA 0 + 1ALPHA + 1BETA >= 0 + 1BETA dx# minus(ALPHA, BETA) -> dx# ALPHA 0 + 1ALPHA + 1BETA >= 0 + 1ALPHA dx# times(ALPHA, BETA) -> dx# BETA 0 + 1ALPHA + 1BETA >= 0 + 1BETA dx# times(ALPHA, BETA) -> dx# ALPHA 0 + 1ALPHA + 1BETA >= 0 + 1ALPHA dx# plus(ALPHA, BETA) -> dx# BETA 0 + 1ALPHA + 1BETA >= 0 + 1BETA dx# plus(ALPHA, BETA) -> dx# ALPHA 0 + 1ALPHA + 1BETA >= 0 + 1ALPHA Weak: dx ln ALPHA -> div(dx ALPHA, ALPHA) 0 + 0ALPHA >= 0 + 1ALPHA dx exp(ALPHA, BETA) -> plus(times(BETA, times(exp(ALPHA, minus(BETA, one())), dx ALPHA)), times(exp(ALPHA, BETA), times(ln ALPHA, dx BETA))) 0 + 0ALPHA + 0BETA >= 1 + 3ALPHA + 3BETA dx div(ALPHA, BETA) -> minus(div(dx ALPHA, BETA), times(ALPHA, div(dx BETA, exp(BETA, two())))) 0 + 0ALPHA + 0BETA >= 0 + 1ALPHA + 2BETA dx neg ALPHA -> neg dx ALPHA 0 + 0ALPHA >= 0 + 0ALPHA dx minus(ALPHA, BETA) -> minus(dx ALPHA, dx BETA) 0 + 0ALPHA + 0BETA >= 0 + 0ALPHA + 0BETA dx times(ALPHA, BETA) -> plus(times(BETA, dx ALPHA), times(ALPHA, dx BETA)) 0 + 0ALPHA + 0BETA >= 0 + 1ALPHA + 1BETA dx plus(ALPHA, BETA) -> plus(dx ALPHA, dx BETA) 0 + 0ALPHA + 0BETA >= 0 + 0ALPHA + 0BETA dx a() -> zero() 0 >= 0 dx X -> one() 0 + 0X >= 0 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} 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# exp(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)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [plus](x0, x1) = x0 + x1 + 1, [times](x0, x1) = x0 + x1 + 1, [minus](x0, x1) = x0 + x1, [div](x0, x1) = x0 + x1, [exp](x0, x1) = x0 + x1 + 1, [dx](x0) = 0, [neg](x0) = x0, [ln](x0) = x0 + 1, [one] = 0, [zero] = 0, [a] = 0, [two] = 0, [dx#](x0) = x0 + 1 Strict: dx# exp(ALPHA, BETA) -> dx# BETA 2 + 1ALPHA + 1BETA >= 1 + 1BETA dx# exp(ALPHA, BETA) -> dx# ALPHA 2 + 1ALPHA + 1BETA >= 1 + 1ALPHA dx# div(ALPHA, BETA) -> dx# BETA 1 + 1ALPHA + 1BETA >= 1 + 1BETA dx# div(ALPHA, BETA) -> dx# ALPHA 1 + 1ALPHA + 1BETA >= 1 + 1ALPHA dx# neg ALPHA -> dx# ALPHA 1 + 1ALPHA >= 1 + 1ALPHA dx# minus(ALPHA, BETA) -> dx# BETA 1 + 1ALPHA + 1BETA >= 1 + 1BETA dx# minus(ALPHA, BETA) -> dx# ALPHA 1 + 1ALPHA + 1BETA >= 1 + 1ALPHA dx# times(ALPHA, BETA) -> dx# BETA 2 + 1ALPHA + 1BETA >= 1 + 1BETA dx# times(ALPHA, BETA) -> dx# ALPHA 2 + 1ALPHA + 1BETA >= 1 + 1ALPHA dx# plus(ALPHA, BETA) -> dx# BETA 2 + 1ALPHA + 1BETA >= 1 + 1BETA dx# plus(ALPHA, BETA) -> dx# ALPHA 2 + 1ALPHA + 1BETA >= 1 + 1ALPHA Weak: dx ln ALPHA -> div(dx ALPHA, ALPHA) 0 + 0ALPHA >= 0 + 1ALPHA dx exp(ALPHA, BETA) -> plus(times(BETA, times(exp(ALPHA, minus(BETA, one())), dx ALPHA)), times(exp(ALPHA, BETA), times(ln ALPHA, dx BETA))) 0 + 0ALPHA + 0BETA >= 8 + 3ALPHA + 3BETA dx div(ALPHA, BETA) -> minus(div(dx ALPHA, BETA), times(ALPHA, div(dx BETA, exp(BETA, two())))) 0 + 0ALPHA + 0BETA >= 2 + 1ALPHA + 2BETA dx neg ALPHA -> neg dx ALPHA 0 + 0ALPHA >= 0 + 0ALPHA dx minus(ALPHA, BETA) -> minus(dx ALPHA, dx BETA) 0 + 0ALPHA + 0BETA >= 0 + 0ALPHA + 0BETA dx times(ALPHA, BETA) -> plus(times(BETA, dx ALPHA), times(ALPHA, dx BETA)) 0 + 0ALPHA + 0BETA >= 3 + 1ALPHA + 1BETA dx plus(ALPHA, BETA) -> plus(dx ALPHA, dx BETA) 0 + 0ALPHA + 0BETA >= 1 + 0ALPHA + 0BETA dx a() -> zero() 0 >= 0 dx X -> one() 0 + 0X >= 0 SCCS (1): Scc: {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} SCC (5): Strict: {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} 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)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [plus](x0, x1) = 0, [times](x0, x1) = 0, [minus](x0, x1) = x0 + x1, [div](x0, x1) = x0 + x1 + 1, [exp](x0, x1) = x0 + 1, [dx](x0) = 0, [neg](x0) = x0, [ln](x0) = 0, [one] = 1, [zero] = 0, [a] = 0, [two] = 0, [dx#](x0) = x0 Strict: dx# div(ALPHA, BETA) -> dx# BETA 1 + 1ALPHA + 1BETA >= 0 + 1BETA dx# div(ALPHA, BETA) -> dx# ALPHA 1 + 1ALPHA + 1BETA >= 0 + 1ALPHA dx# neg ALPHA -> dx# ALPHA 0 + 1ALPHA >= 0 + 1ALPHA dx# minus(ALPHA, BETA) -> dx# BETA 0 + 1ALPHA + 1BETA >= 0 + 1BETA dx# minus(ALPHA, BETA) -> dx# ALPHA 0 + 1ALPHA + 1BETA >= 0 + 1ALPHA Weak: dx ln ALPHA -> div(dx ALPHA, ALPHA) 0 + 0ALPHA >= 1 + 1ALPHA dx exp(ALPHA, BETA) -> plus(times(BETA, times(exp(ALPHA, minus(BETA, one())), dx ALPHA)), times(exp(ALPHA, BETA), times(ln ALPHA, dx BETA))) 0 + 0ALPHA + 0BETA >= 0 + 0ALPHA + 0BETA dx div(ALPHA, BETA) -> minus(div(dx ALPHA, BETA), times(ALPHA, div(dx BETA, exp(BETA, two())))) 0 + 0ALPHA + 0BETA >= 1 + 0ALPHA + 1BETA dx neg ALPHA -> neg dx ALPHA 0 + 0ALPHA >= 0 + 0ALPHA dx minus(ALPHA, BETA) -> minus(dx ALPHA, dx BETA) 0 + 0ALPHA + 0BETA >= 0 + 0ALPHA + 0BETA dx times(ALPHA, BETA) -> plus(times(BETA, dx ALPHA), times(ALPHA, dx BETA)) 0 + 0ALPHA + 0BETA >= 0 + 0ALPHA + 0BETA dx plus(ALPHA, BETA) -> plus(dx ALPHA, dx BETA) 0 + 0ALPHA + 0BETA >= 0 + 0ALPHA + 0BETA dx a() -> zero() 0 >= 0 dx X -> one() 0 + 0X >= 1 SCCS (1): Scc: {dx# minus(ALPHA, BETA) -> dx# ALPHA, dx# minus(ALPHA, BETA) -> dx# BETA, dx# neg ALPHA -> dx# ALPHA} SCC (3): Strict: {dx# minus(ALPHA, BETA) -> dx# ALPHA, dx# minus(ALPHA, BETA) -> dx# BETA, dx# neg 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)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [plus](x0, x1) = 0, [times](x0, x1) = 0, [minus](x0, x1) = x0 + x1, [div](x0, x1) = 0, [exp](x0, x1) = 0, [dx](x0) = 0, [neg](x0) = x0 + 1, [ln](x0) = 0, [one] = 0, [zero] = 0, [a] = 0, [two] = 0, [dx#](x0) = x0 Strict: dx# neg ALPHA -> dx# ALPHA 1 + 1ALPHA >= 0 + 1ALPHA dx# minus(ALPHA, BETA) -> dx# BETA 0 + 1ALPHA + 1BETA >= 0 + 1BETA dx# minus(ALPHA, BETA) -> dx# ALPHA 0 + 1ALPHA + 1BETA >= 0 + 1ALPHA Weak: dx ln ALPHA -> div(dx ALPHA, ALPHA) 0 + 0ALPHA >= 0 + 0ALPHA dx exp(ALPHA, BETA) -> plus(times(BETA, times(exp(ALPHA, minus(BETA, one())), dx ALPHA)), times(exp(ALPHA, BETA), times(ln ALPHA, dx BETA))) 0 + 0ALPHA + 0BETA >= 0 + 0ALPHA + 0BETA dx div(ALPHA, BETA) -> minus(div(dx ALPHA, BETA), times(ALPHA, div(dx BETA, exp(BETA, two())))) 0 + 0ALPHA + 0BETA >= 0 + 0ALPHA + 0BETA dx neg ALPHA -> neg dx ALPHA 0 + 0ALPHA >= 1 + 0ALPHA dx minus(ALPHA, BETA) -> minus(dx ALPHA, dx BETA) 0 + 0ALPHA + 0BETA >= 0 + 0ALPHA + 0BETA dx times(ALPHA, BETA) -> plus(times(BETA, dx ALPHA), times(ALPHA, dx BETA)) 0 + 0ALPHA + 0BETA >= 0 + 0ALPHA + 0BETA dx plus(ALPHA, BETA) -> plus(dx ALPHA, dx BETA) 0 + 0ALPHA + 0BETA >= 0 + 0ALPHA + 0BETA dx a() -> zero() 0 >= 0 dx X -> one() 0 + 0X >= 0 SCCS (1): Scc: {dx# minus(ALPHA, BETA) -> dx# ALPHA, dx# minus(ALPHA, BETA) -> dx# BETA} SCC (2): Strict: {dx# minus(ALPHA, BETA) -> dx# ALPHA, dx# minus(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)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [plus](x0, x1) = 0, [times](x0, x1) = 0, [minus](x0, x1) = x0 + x1 + 1, [div](x0, x1) = x0 + 1, [exp](x0, x1) = x0 + 1, [dx](x0) = 0, [neg](x0) = 0, [ln](x0) = 0, [one] = 0, [zero] = 0, [a] = 0, [two] = 0, [dx#](x0) = x0 Strict: dx# minus(ALPHA, BETA) -> dx# BETA 1 + 1ALPHA + 1BETA >= 0 + 1BETA dx# minus(ALPHA, BETA) -> dx# ALPHA 1 + 1ALPHA + 1BETA >= 0 + 1ALPHA Weak: dx ln ALPHA -> div(dx ALPHA, ALPHA) 0 + 0ALPHA >= 1 + 1ALPHA dx exp(ALPHA, BETA) -> plus(times(BETA, times(exp(ALPHA, minus(BETA, one())), dx ALPHA)), times(exp(ALPHA, BETA), times(ln ALPHA, dx BETA))) 0 + 0ALPHA + 0BETA >= 0 + 0ALPHA + 0BETA dx div(ALPHA, BETA) -> minus(div(dx ALPHA, BETA), times(ALPHA, div(dx BETA, exp(BETA, two())))) 0 + 0ALPHA + 0BETA >= 2 + 0ALPHA + 1BETA dx neg ALPHA -> neg dx ALPHA 0 + 0ALPHA >= 0 + 0ALPHA dx minus(ALPHA, BETA) -> minus(dx ALPHA, dx BETA) 0 + 0ALPHA + 0BETA >= 1 + 0ALPHA + 0BETA dx times(ALPHA, BETA) -> plus(times(BETA, dx ALPHA), times(ALPHA, dx BETA)) 0 + 0ALPHA + 0BETA >= 0 + 0ALPHA + 0BETA dx plus(ALPHA, BETA) -> plus(dx ALPHA, dx BETA) 0 + 0ALPHA + 0BETA >= 0 + 0ALPHA + 0BETA dx a() -> zero() 0 >= 0 dx X -> one() 0 + 0X >= 0 Qed