YES Time: 0.011 Problem: Equations: TRS: plusAC(x,0()) -> x plusAC(x,s(y)) -> s(plusAC(x,y)) timesAC(x,0()) -> 0() timesAC(x,s(y)) -> plusAC(x,timesAC(x,y)) power(x,0()) -> s(0()) power(x,s(y)) -> timesAC(x,power(x,y)) Proof: AC-RPO Processor: precedence: power > 0 > timesAC > plusAC > s status: power:mul problem: Equations: TRS: Qed