YES Time: 0.195 Problem: Equations: plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6)) plusAC(x4,x5) -> plusAC(x5,x4) plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6) plusAC(x5,x4) -> plusAC(x4,x5) TRS: plusAC(x,0()) -> x plusAC(x,s(y)) -> s(plusAC(x,y)) sum(nil(),nil()) -> 0() sum(cons(x,xs),nil()) -> plusAC(x,sum(xs,nil())) sum(nil(),cons(x,xs)) -> plusAC(x,sum(nil(),xs)) sum(cons(x,xs),cons(y,ys)) -> plusAC(plusAC(x,y),sum(xs,ys)) Proof: DP Processor: Equations#: plus{AC,#}(plusAC(x4,x5),x6) -> plus{AC,#}(x4,plusAC(x5,x6)) plus{AC,#}(x4,x5) -> plus{AC,#}(x5,x4) plus{AC,#}(x4,plusAC(x5,x6)) -> plus{AC,#}(plusAC(x4,x5),x6) plus{AC,#}(x5,x4) -> plus{AC,#}(x4,x5) DPs: plus{AC,#}(x,s(y)) -> plus{AC,#}(x,y) sum#(cons(x,xs),nil()) -> sum#(xs,nil()) sum#(cons(x,xs),nil()) -> plus{AC,#}(x,sum(xs,nil())) sum#(nil(),cons(x,xs)) -> sum#(nil(),xs) sum#(nil(),cons(x,xs)) -> plus{AC,#}(x,sum(nil(),xs)) sum#(cons(x,xs),cons(y,ys)) -> sum#(xs,ys) sum#(cons(x,xs),cons(y,ys)) -> plus{AC,#}(x,y) sum#(cons(x,xs),cons(y,ys)) -> plus{AC,#}(plusAC(x,y),sum(xs,ys)) plus{AC,#}(x7,plusAC(x,0())) -> plus{AC,#}(x7,x) plus{AC,#}(x8,plusAC(x,s(y))) -> plus{AC,#}(x,y) plus{AC,#}(x8,plusAC(x,s(y))) -> plus{AC,#}(x8,s(plusAC(x,y))) Equations: plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6)) plusAC(x4,x5) -> plusAC(x5,x4) plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6) plusAC(x5,x4) -> plusAC(x4,x5) TRS: plusAC(x,0()) -> x plusAC(x,s(y)) -> s(plusAC(x,y)) sum(nil(),nil()) -> 0() sum(cons(x,xs),nil()) -> plusAC(x,sum(xs,nil())) sum(nil(),cons(x,xs)) -> plusAC(x,sum(nil(),xs)) sum(cons(x,xs),cons(y,ys)) -> plusAC(plusAC(x,y),sum(xs,ys)) S: plus{AC,#}(plusAC(x9,x10),x11) -> plus{AC,#}(x9,x10) plus{AC,#}(x9,plusAC(x10,x11)) -> plus{AC,#}(x10,x11) AC-EDG Processor: Equations#: plus{AC,#}(plusAC(x4,x5),x6) -> plus{AC,#}(x4,plusAC(x5,x6)) plus{AC,#}(x4,x5) -> plus{AC,#}(x5,x4) plus{AC,#}(x4,plusAC(x5,x6)) -> plus{AC,#}(plusAC(x4,x5),x6) plus{AC,#}(x5,x4) -> plus{AC,#}(x4,x5) DPs: plus{AC,#}(x,s(y)) -> plus{AC,#}(x,y) sum#(cons(x,xs),nil()) -> sum#(xs,nil()) sum#(cons(x,xs),nil()) -> plus{AC,#}(x,sum(xs,nil())) sum#(nil(),cons(x,xs)) -> sum#(nil(),xs) sum#(nil(),cons(x,xs)) -> plus{AC,#}(x,sum(nil(),xs)) sum#(cons(x,xs),cons(y,ys)) -> sum#(xs,ys) sum#(cons(x,xs),cons(y,ys)) -> plus{AC,#}(x,y) sum#(cons(x,xs),cons(y,ys)) -> plus{AC,#}(plusAC(x,y),sum(xs,ys)) plus{AC,#}(x7,plusAC(x,0())) -> plus{AC,#}(x7,x) plus{AC,#}(x8,plusAC(x,s(y))) -> plus{AC,#}(x,y) plus{AC,#}(x8,plusAC(x,s(y))) -> plus{AC,#}(x8,s(plusAC(x,y))) Equations: plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6)) plusAC(x4,x5) -> plusAC(x5,x4) plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6) plusAC(x5,x4) -> plusAC(x4,x5) TRS: plusAC(x,0()) -> x plusAC(x,s(y)) -> s(plusAC(x,y)) sum(nil(),nil()) -> 0() sum(cons(x,xs),nil()) -> plusAC(x,sum(xs,nil())) sum(nil(),cons(x,xs)) -> plusAC(x,sum(nil(),xs)) sum(cons(x,xs),cons(y,ys)) -> plusAC(plusAC(x,y),sum(xs,ys)) S: plus{AC,#}(plusAC(x9,x10),x11) -> plus{AC,#}(x9,x10) plus{AC,#}(x9,plusAC(x10,x11)) -> plus{AC,#}(x10,x11) SCC Processor: #sccs: 4 #rules: 7 #arcs: 43/121 Equations#: plus{AC,#}(plusAC(x4,x5),x6) -> plus{AC,#}(x4,plusAC(x5,x6)) plus{AC,#}(x4,x5) -> plus{AC,#}(x5,x4) plus{AC,#}(x4,plusAC(x5,x6)) -> plus{AC,#}(plusAC(x4,x5),x6) plus{AC,#}(x5,x4) -> plus{AC,#}(x4,x5) DPs: sum#(cons(x,xs),cons(y,ys)) -> sum#(xs,ys) Equations: plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6)) plusAC(x4,x5) -> plusAC(x5,x4) plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6) plusAC(x5,x4) -> plusAC(x4,x5) TRS: plusAC(x,0()) -> x plusAC(x,s(y)) -> s(plusAC(x,y)) sum(nil(),nil()) -> 0() sum(cons(x,xs),nil()) -> plusAC(x,sum(xs,nil())) sum(nil(),cons(x,xs)) -> plusAC(x,sum(nil(),xs)) sum(cons(x,xs),cons(y,ys)) -> plusAC(plusAC(x,y),sum(xs,ys)) S: plus{AC,#}(plusAC(x9,x10),x11) -> plus{AC,#}(x9,x10) plus{AC,#}(x9,plusAC(x10,x11)) -> plus{AC,#}(x10,x11) AC-DP unlabeling: Equations#: plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6)) plusAC(x4,x5) -> plusAC(x5,x4) plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6) plusAC(x5,x4) -> plusAC(x4,x5) DPs: sum#(cons(x,xs),cons(y,ys)) -> sum#(xs,ys) Equations: plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6)) plusAC(x4,x5) -> plusAC(x5,x4) plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6) plusAC(x5,x4) -> plusAC(x4,x5) TRS: plusAC(x,0()) -> x plusAC(x,s(y)) -> s(plusAC(x,y)) sum(nil(),nil()) -> 0() sum(cons(x,xs),nil()) -> plusAC(x,sum(xs,nil())) sum(nil(),cons(x,xs)) -> plusAC(x,sum(nil(),xs)) sum(cons(x,xs),cons(y,ys)) -> plusAC(plusAC(x,y),sum(xs,ys)) S: plusAC(plusAC(x9,x10),x11) -> plusAC(x9,x10) plusAC(x9,plusAC(x10,x11)) -> plusAC(x10,x11) Usable Rule Processor: Equations#: plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6)) plusAC(x4,x5) -> plusAC(x5,x4) plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6) plusAC(x5,x4) -> plusAC(x4,x5) DPs: sum#(cons(x,xs),cons(y,ys)) -> sum#(xs,ys) Equations: plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6)) plusAC(x4,x5) -> plusAC(x5,x4) plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6) plusAC(x5,x4) -> plusAC(x4,x5) TRS: S: plusAC(plusAC(x9,x10),x11) -> plusAC(x9,x10) plusAC(x9,plusAC(x10,x11)) -> plusAC(x10,x11) AC-KBO Processor: argument filtering: pi(cons) = [1] pi(sum#) = 1 precedence: sum# ~ cons weight function: w0 = 1 w(sum#) = 1 w(cons) = 0 usable rules: problem: Equations#: plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6)) plusAC(x4,x5) -> plusAC(x5,x4) plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6) plusAC(x5,x4) -> plusAC(x4,x5) DPs: Equations: plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6)) plusAC(x4,x5) -> plusAC(x5,x4) plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6) plusAC(x5,x4) -> plusAC(x4,x5) TRS: S: plusAC(plusAC(x9,x10),x11) -> plusAC(x9,x10) plusAC(x9,plusAC(x10,x11)) -> plusAC(x10,x11) Qed Equations#: plus{AC,#}(plusAC(x4,x5),x6) -> plus{AC,#}(x4,plusAC(x5,x6)) plus{AC,#}(x4,x5) -> plus{AC,#}(x5,x4) plus{AC,#}(x4,plusAC(x5,x6)) -> plus{AC,#}(plusAC(x4,x5),x6) plus{AC,#}(x5,x4) -> plus{AC,#}(x4,x5) DPs: sum#(cons(x,xs),nil()) -> sum#(xs,nil()) Equations: plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6)) plusAC(x4,x5) -> plusAC(x5,x4) plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6) plusAC(x5,x4) -> plusAC(x4,x5) TRS: plusAC(x,0()) -> x plusAC(x,s(y)) -> s(plusAC(x,y)) sum(nil(),nil()) -> 0() sum(cons(x,xs),nil()) -> plusAC(x,sum(xs,nil())) sum(nil(),cons(x,xs)) -> plusAC(x,sum(nil(),xs)) sum(cons(x,xs),cons(y,ys)) -> plusAC(plusAC(x,y),sum(xs,ys)) S: plus{AC,#}(plusAC(x9,x10),x11) -> plus{AC,#}(x9,x10) plus{AC,#}(x9,plusAC(x10,x11)) -> plus{AC,#}(x10,x11) AC-DP unlabeling: Equations#: plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6)) plusAC(x4,x5) -> plusAC(x5,x4) plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6) plusAC(x5,x4) -> plusAC(x4,x5) DPs: sum#(cons(x,xs),nil()) -> sum#(xs,nil()) Equations: plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6)) plusAC(x4,x5) -> plusAC(x5,x4) plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6) plusAC(x5,x4) -> plusAC(x4,x5) TRS: plusAC(x,0()) -> x plusAC(x,s(y)) -> s(plusAC(x,y)) sum(nil(),nil()) -> 0() sum(cons(x,xs),nil()) -> plusAC(x,sum(xs,nil())) sum(nil(),cons(x,xs)) -> plusAC(x,sum(nil(),xs)) sum(cons(x,xs),cons(y,ys)) -> plusAC(plusAC(x,y),sum(xs,ys)) S: plusAC(plusAC(x9,x10),x11) -> plusAC(x9,x10) plusAC(x9,plusAC(x10,x11)) -> plusAC(x10,x11) Usable Rule Processor: Equations#: plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6)) plusAC(x4,x5) -> plusAC(x5,x4) plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6) plusAC(x5,x4) -> plusAC(x4,x5) DPs: sum#(cons(x,xs),nil()) -> sum#(xs,nil()) Equations: plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6)) plusAC(x4,x5) -> plusAC(x5,x4) plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6) plusAC(x5,x4) -> plusAC(x4,x5) TRS: S: plusAC(plusAC(x9,x10),x11) -> plusAC(x9,x10) plusAC(x9,plusAC(x10,x11)) -> plusAC(x10,x11) AC-KBO Processor: argument filtering: pi(nil) = [] pi(cons) = [1] pi(sum#) = 0 precedence: sum# ~ cons ~ nil weight function: w0 = 1 w(sum#) = 4 w(cons) = w(nil) = 1 usable rules: problem: Equations#: plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6)) plusAC(x4,x5) -> plusAC(x5,x4) plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6) plusAC(x5,x4) -> plusAC(x4,x5) DPs: Equations: plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6)) plusAC(x4,x5) -> plusAC(x5,x4) plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6) plusAC(x5,x4) -> plusAC(x4,x5) TRS: S: plusAC(plusAC(x9,x10),x11) -> plusAC(x9,x10) plusAC(x9,plusAC(x10,x11)) -> plusAC(x10,x11) Qed Equations#: plus{AC,#}(plusAC(x4,x5),x6) -> plus{AC,#}(x4,plusAC(x5,x6)) plus{AC,#}(x4,x5) -> plus{AC,#}(x5,x4) plus{AC,#}(x4,plusAC(x5,x6)) -> plus{AC,#}(plusAC(x4,x5),x6) plus{AC,#}(x5,x4) -> plus{AC,#}(x4,x5) DPs: sum#(nil(),cons(x,xs)) -> sum#(nil(),xs) Equations: plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6)) plusAC(x4,x5) -> plusAC(x5,x4) plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6) plusAC(x5,x4) -> plusAC(x4,x5) TRS: plusAC(x,0()) -> x plusAC(x,s(y)) -> s(plusAC(x,y)) sum(nil(),nil()) -> 0() sum(cons(x,xs),nil()) -> plusAC(x,sum(xs,nil())) sum(nil(),cons(x,xs)) -> plusAC(x,sum(nil(),xs)) sum(cons(x,xs),cons(y,ys)) -> plusAC(plusAC(x,y),sum(xs,ys)) S: plus{AC,#}(plusAC(x9,x10),x11) -> plus{AC,#}(x9,x10) plus{AC,#}(x9,plusAC(x10,x11)) -> plus{AC,#}(x10,x11) AC-DP unlabeling: Equations#: plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6)) plusAC(x4,x5) -> plusAC(x5,x4) plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6) plusAC(x5,x4) -> plusAC(x4,x5) DPs: sum#(nil(),cons(x,xs)) -> sum#(nil(),xs) Equations: plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6)) plusAC(x4,x5) -> plusAC(x5,x4) plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6) plusAC(x5,x4) -> plusAC(x4,x5) TRS: plusAC(x,0()) -> x plusAC(x,s(y)) -> s(plusAC(x,y)) sum(nil(),nil()) -> 0() sum(cons(x,xs),nil()) -> plusAC(x,sum(xs,nil())) sum(nil(),cons(x,xs)) -> plusAC(x,sum(nil(),xs)) sum(cons(x,xs),cons(y,ys)) -> plusAC(plusAC(x,y),sum(xs,ys)) S: plusAC(plusAC(x9,x10),x11) -> plusAC(x9,x10) plusAC(x9,plusAC(x10,x11)) -> plusAC(x10,x11) Usable Rule Processor: Equations#: plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6)) plusAC(x4,x5) -> plusAC(x5,x4) plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6) plusAC(x5,x4) -> plusAC(x4,x5) DPs: sum#(nil(),cons(x,xs)) -> sum#(nil(),xs) Equations: plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6)) plusAC(x4,x5) -> plusAC(x5,x4) plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6) plusAC(x5,x4) -> plusAC(x4,x5) TRS: S: plusAC(plusAC(x9,x10),x11) -> plusAC(x9,x10) plusAC(x9,plusAC(x10,x11)) -> plusAC(x10,x11) AC-KBO Processor: argument filtering: pi(nil) = [] pi(cons) = [1] pi(sum#) = [0,1] precedence: sum# ~ cons ~ nil weight function: w0 = 2 w(nil) = 2 w(sum#) = 1 w(cons) = 0 usable rules: problem: Equations#: plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6)) plusAC(x4,x5) -> plusAC(x5,x4) plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6) plusAC(x5,x4) -> plusAC(x4,x5) DPs: Equations: plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6)) plusAC(x4,x5) -> plusAC(x5,x4) plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6) plusAC(x5,x4) -> plusAC(x4,x5) TRS: S: plusAC(plusAC(x9,x10),x11) -> plusAC(x9,x10) plusAC(x9,plusAC(x10,x11)) -> plusAC(x10,x11) Qed Equations#: plus{AC,#}(plusAC(x4,x5),x6) -> plus{AC,#}(x4,plusAC(x5,x6)) plus{AC,#}(x4,x5) -> plus{AC,#}(x5,x4) plus{AC,#}(x4,plusAC(x5,x6)) -> plus{AC,#}(plusAC(x4,x5),x6) plus{AC,#}(x5,x4) -> plus{AC,#}(x4,x5) DPs: plus{AC,#}(x8,plusAC(x,s(y))) -> plus{AC,#}(x8,s(plusAC(x,y))) plus{AC,#}(x8,plusAC(x,s(y))) -> plus{AC,#}(x,y) plus{AC,#}(x7,plusAC(x,0())) -> plus{AC,#}(x7,x) plus{AC,#}(x,s(y)) -> plus{AC,#}(x,y) Equations: plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6)) plusAC(x4,x5) -> plusAC(x5,x4) plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6) plusAC(x5,x4) -> plusAC(x4,x5) TRS: plusAC(x,0()) -> x plusAC(x,s(y)) -> s(plusAC(x,y)) sum(nil(),nil()) -> 0() sum(cons(x,xs),nil()) -> plusAC(x,sum(xs,nil())) sum(nil(),cons(x,xs)) -> plusAC(x,sum(nil(),xs)) sum(cons(x,xs),cons(y,ys)) -> plusAC(plusAC(x,y),sum(xs,ys)) S: plus{AC,#}(plusAC(x9,x10),x11) -> plus{AC,#}(x9,x10) plus{AC,#}(x9,plusAC(x10,x11)) -> plus{AC,#}(x10,x11) AC-DP unlabeling: Equations#: plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6)) plusAC(x4,x5) -> plusAC(x5,x4) plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6) plusAC(x5,x4) -> plusAC(x4,x5) DPs: plusAC(x8,plusAC(x,s(y))) -> plusAC(x8,s(plusAC(x,y))) plusAC(x8,plusAC(x,s(y))) -> plusAC(x,y) plusAC(x7,plusAC(x,0())) -> plusAC(x7,x) plusAC(x,s(y)) -> plusAC(x,y) Equations: plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6)) plusAC(x4,x5) -> plusAC(x5,x4) plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6) plusAC(x5,x4) -> plusAC(x4,x5) TRS: plusAC(x,0()) -> x plusAC(x,s(y)) -> s(plusAC(x,y)) sum(nil(),nil()) -> 0() sum(cons(x,xs),nil()) -> plusAC(x,sum(xs,nil())) sum(nil(),cons(x,xs)) -> plusAC(x,sum(nil(),xs)) sum(cons(x,xs),cons(y,ys)) -> plusAC(plusAC(x,y),sum(xs,ys)) S: plusAC(plusAC(x9,x10),x11) -> plusAC(x9,x10) plusAC(x9,plusAC(x10,x11)) -> plusAC(x10,x11) Usable Rule Processor: Equations#: plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6)) plusAC(x4,x5) -> plusAC(x5,x4) plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6) plusAC(x5,x4) -> plusAC(x4,x5) DPs: plusAC(x8,plusAC(x,s(y))) -> plusAC(x8,s(plusAC(x,y))) plusAC(x8,plusAC(x,s(y))) -> plusAC(x,y) plusAC(x7,plusAC(x,0())) -> plusAC(x7,x) plusAC(x,s(y)) -> plusAC(x,y) Equations: plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6)) plusAC(x4,x5) -> plusAC(x5,x4) plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6) plusAC(x5,x4) -> plusAC(x4,x5) TRS: plusAC(x,s(y)) -> s(plusAC(x,y)) plusAC(x,0()) -> x S: plusAC(plusAC(x9,x10),x11) -> plusAC(x9,x10) plusAC(x9,plusAC(x10,x11)) -> plusAC(x10,x11) AC-KBO Processor: argument filtering: pi(plusAC) = [0,1] pi(0) = [] pi(s) = [0] precedence: 0 ~ plusAC > s weight function: w0 = 4 w(plusAC) = 5 w(0) = 4 w(s) = 2 usable rules: plusAC(x,s(y)) -> s(plusAC(x,y)) plusAC(x,0()) -> x problem: Equations#: plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6)) plusAC(x4,x5) -> plusAC(x5,x4) plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6) plusAC(x5,x4) -> plusAC(x4,x5) DPs: Equations: plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6)) plusAC(x4,x5) -> plusAC(x5,x4) plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6) plusAC(x5,x4) -> plusAC(x4,x5) TRS: plusAC(x,s(y)) -> s(plusAC(x,y)) plusAC(x,0()) -> x S: plusAC(plusAC(x9,x10),x11) -> plusAC(x9,x10) plusAC(x9,plusAC(x10,x11)) -> plusAC(x10,x11) Qed