MAYBE Time: 0.119 Problem: Equations: TRS: plusAC(x,0()) -> x plusAC(x,i(x)) -> 0() i(0()) -> 0() i(i(x)) -> x i(plusAC(x,y)) -> plusAC(i(x),i(y)) timesAC(x,1()) -> x timesAC(x,0()) -> 0() timesAC(x,i(y)) -> i(timesAC(x,y)) timesAC(x,plusAC(y,z)) -> plusAC(timesAC(x,y),timesAC(x,z)) Proof: Open