MAYBE Time: 0.008 Problem: Equations: TRS: plusAC(x,0()) -> x plusAC(x,s(y)) -> s(plusAC(x,y)) timesAC(x,0()) -> 0() timesAC(x,s(y)) -> plusAC(timesAC(x,y),x) minus(x,0()) -> x minus(s(x),s(y)) -> minus(x,y) div(0(),s(y)) -> 0() div(s(x),s(y)) -> s(div(minus(x,y),s(y))) Proof: Open