YES Time: 0.015 Problem: Equations: TRS: fAC(x,one()) -> x fAC(i(x),x) -> one() g(one()) -> one() g(fAC(x,y)) -> fAC(g(x),g(y)) Proof: AC-KBO Processor: precedence: g > fAC > i ~ one weight function: w0 = 2 w(one) = 6 w(i) = 2 w(g) = w(fAC) = 0 problem: Equations: TRS: Qed