MAYBE Time: 0.018 Problem: Equations: TRS: plusAC(x,0()) -> x plusAC(x,s(y)) -> s(plusAC(x,y)) sumAC(nil(),nil()) -> 0() sumAC(cons(x,xs),nil()) -> plusAC(x,sumAC(xs,nil())) sumAC(nil(),cons(x,xs)) -> plusAC(x,sumAC(nil(),xs)) sumAC(cons(x,xs),cons(y,ys)) -> plusAC(plusAC(x,y),sumAC(xs,ys)) Proof: Open