YES Time: 0.009 Problem: Equations: TRS: fAC(x,one()) -> x fAC(i(x),x) -> one() Proof: AC-RPO Processor: precedence: fAC > one > i status: problem: Equations: TRS: Qed