YES Time: 1.078 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: app(nil(),k) -> k app(l,nil()) -> l app(cons(x,l),k) -> cons(x,app(l,k)) sum(cons(x,nil())) -> cons(x,nil()) sum(cons(x,cons(y,l))) -> sum(cons(plusAC(x,y),l)) sum(app(l,cons(x,cons(y,k)))) -> sum(app(l,sum(cons(x,cons(y,k))))) sum(cons(0(),cons(plusAC(x,y),l))) -> pred(sum(cons(s(x),cons(y,l)))) plusAC(0(),y) -> y plusAC(s(x),y) -> s(plusAC(x,y)) pred(cons(s(x),nil())) -> cons(x,nil()) 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: app#(cons(x,l),k) -> app#(l,k) sum#(cons(x,cons(y,l))) -> plus{AC,#}(x,y) sum#(cons(x,cons(y,l))) -> sum#(cons(plusAC(x,y),l)) sum#(app(l,cons(x,cons(y,k)))) -> sum#(cons(x,cons(y,k))) sum#(app(l,cons(x,cons(y,k)))) -> app#(l,sum(cons(x,cons(y,k)))) sum#(app(l,cons(x,cons(y,k)))) -> sum#(app(l,sum(cons(x,cons(y,k))))) sum#(cons(0(),cons(plusAC(x,y),l))) -> sum#(cons(s(x),cons(y,l))) sum#(cons(0(),cons(plusAC(x,y),l))) -> pred#(sum(cons(s(x),cons(y,l)))) plus{AC,#}(s(x),y) -> plus{AC,#}(x,y) plus{AC,#}(x7,plusAC(0(),y)) -> plus{AC,#}(x7,y) plus{AC,#}(x8,plusAC(s(x),y)) -> plus{AC,#}(x,y) plus{AC,#}(x8,plusAC(s(x),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: app(nil(),k) -> k app(l,nil()) -> l app(cons(x,l),k) -> cons(x,app(l,k)) sum(cons(x,nil())) -> cons(x,nil()) sum(cons(x,cons(y,l))) -> sum(cons(plusAC(x,y),l)) sum(app(l,cons(x,cons(y,k)))) -> sum(app(l,sum(cons(x,cons(y,k))))) sum(cons(0(),cons(plusAC(x,y),l))) -> pred(sum(cons(s(x),cons(y,l)))) plusAC(0(),y) -> y plusAC(s(x),y) -> s(plusAC(x,y)) pred(cons(s(x),nil())) -> cons(x,nil()) 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: app#(cons(x,l),k) -> app#(l,k) sum#(cons(x,cons(y,l))) -> plus{AC,#}(x,y) sum#(cons(x,cons(y,l))) -> sum#(cons(plusAC(x,y),l)) sum#(app(l,cons(x,cons(y,k)))) -> sum#(cons(x,cons(y,k))) sum#(app(l,cons(x,cons(y,k)))) -> app#(l,sum(cons(x,cons(y,k)))) sum#(app(l,cons(x,cons(y,k)))) -> sum#(app(l,sum(cons(x,cons(y,k))))) sum#(cons(0(),cons(plusAC(x,y),l))) -> sum#(cons(s(x),cons(y,l))) sum#(cons(0(),cons(plusAC(x,y),l))) -> pred#(sum(cons(s(x),cons(y,l)))) plus{AC,#}(s(x),y) -> plus{AC,#}(x,y) plus{AC,#}(x7,plusAC(0(),y)) -> plus{AC,#}(x7,y) plus{AC,#}(x8,plusAC(s(x),y)) -> plus{AC,#}(x,y) plus{AC,#}(x8,plusAC(s(x),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: app(nil(),k) -> k app(l,nil()) -> l app(cons(x,l),k) -> cons(x,app(l,k)) sum(cons(x,nil())) -> cons(x,nil()) sum(cons(x,cons(y,l))) -> sum(cons(plusAC(x,y),l)) sum(app(l,cons(x,cons(y,k)))) -> sum(app(l,sum(cons(x,cons(y,k))))) sum(cons(0(),cons(plusAC(x,y),l))) -> pred(sum(cons(s(x),cons(y,l)))) plusAC(0(),y) -> y plusAC(s(x),y) -> s(plusAC(x,y)) pred(cons(s(x),nil())) -> cons(x,nil()) 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: 8 #arcs: 39/144 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#(app(l,cons(x,cons(y,k)))) -> sum#(app(l,sum(cons(x,cons(y,k))))) 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: app(nil(),k) -> k app(l,nil()) -> l app(cons(x,l),k) -> cons(x,app(l,k)) sum(cons(x,nil())) -> cons(x,nil()) sum(cons(x,cons(y,l))) -> sum(cons(plusAC(x,y),l)) sum(app(l,cons(x,cons(y,k)))) -> sum(app(l,sum(cons(x,cons(y,k))))) sum(cons(0(),cons(plusAC(x,y),l))) -> pred(sum(cons(s(x),cons(y,l)))) plusAC(0(),y) -> y plusAC(s(x),y) -> s(plusAC(x,y)) pred(cons(s(x),nil())) -> cons(x,nil()) 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#(app(l,cons(x,cons(y,k)))) -> sum#(app(l,sum(cons(x,cons(y,k))))) 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: app(nil(),k) -> k app(l,nil()) -> l app(cons(x,l),k) -> cons(x,app(l,k)) sum(cons(x,nil())) -> cons(x,nil()) sum(cons(x,cons(y,l))) -> sum(cons(plusAC(x,y),l)) sum(app(l,cons(x,cons(y,k)))) -> sum(app(l,sum(cons(x,cons(y,k))))) sum(cons(0(),cons(plusAC(x,y),l))) -> pred(sum(cons(s(x),cons(y,l)))) plusAC(0(),y) -> y plusAC(s(x),y) -> s(plusAC(x,y)) pred(cons(s(x),nil())) -> cons(x,nil()) 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#(app(l,cons(x,cons(y,k)))) -> sum#(app(l,sum(cons(x,cons(y,k))))) 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: sum(cons(x,cons(y,l))) -> sum(cons(plusAC(x,y),l)) sum(cons(0(),cons(plusAC(x,y),l))) -> pred(sum(cons(s(x),cons(y,l)))) sum(cons(x,nil())) -> cons(x,nil()) plusAC(0(),y) -> y plusAC(s(x),y) -> s(plusAC(x,y)) pred(cons(s(x),nil())) -> cons(x,nil()) app(nil(),k) -> k app(l,nil()) -> l app(cons(x,l),k) -> cons(x,app(l,k)) 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(nil) = [] pi(app) = [0,1] pi(cons) = [1] pi(sum) = [] pi(0) = [] pi(s) = [] pi(pred) = [] pi(sum#) = [0] precedence: pred ~ s > sum# ~ 0 ~ sum ~ cons ~ app ~ nil ~ plusAC weight function: [sum#](x0) = x0 + 2, [pred](x0) = 6, [s](x0) = 4, [0] = 4, [sum](x0) = 7, [cons](x0, x1) = x1 + 4, [app](x0, x1) = 4x0 + 4x1 + 4, [nil] = 2, [plusAC](x0, x1) = x0 + x1 + 4 usable rules: sum(cons(x,cons(y,l))) -> sum(cons(plusAC(x,y),l)) sum(cons(0(),cons(plusAC(x,y),l))) -> pred(sum(cons(s(x),cons(y,l)))) sum(cons(x,nil())) -> cons(x,nil()) pred(cons(s(x),nil())) -> cons(x,nil()) app(nil(),k) -> k app(l,nil()) -> l app(cons(x,l),k) -> cons(x,app(l,k)) 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: sum(cons(x,cons(y,l))) -> sum(cons(plusAC(x,y),l)) sum(cons(0(),cons(plusAC(x,y),l))) -> pred(sum(cons(s(x),cons(y,l)))) sum(cons(x,nil())) -> cons(x,nil()) plusAC(0(),y) -> y plusAC(s(x),y) -> s(plusAC(x,y)) pred(cons(s(x),nil())) -> cons(x,nil()) app(nil(),k) -> k app(l,nil()) -> l app(cons(x,l),k) -> cons(x,app(l,k)) 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: app#(cons(x,l),k) -> app#(l,k) 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: app(nil(),k) -> k app(l,nil()) -> l app(cons(x,l),k) -> cons(x,app(l,k)) sum(cons(x,nil())) -> cons(x,nil()) sum(cons(x,cons(y,l))) -> sum(cons(plusAC(x,y),l)) sum(app(l,cons(x,cons(y,k)))) -> sum(app(l,sum(cons(x,cons(y,k))))) sum(cons(0(),cons(plusAC(x,y),l))) -> pred(sum(cons(s(x),cons(y,l)))) plusAC(0(),y) -> y plusAC(s(x),y) -> s(plusAC(x,y)) pred(cons(s(x),nil())) -> cons(x,nil()) 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: app#(cons(x,l),k) -> app#(l,k) 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: app(nil(),k) -> k app(l,nil()) -> l app(cons(x,l),k) -> cons(x,app(l,k)) sum(cons(x,nil())) -> cons(x,nil()) sum(cons(x,cons(y,l))) -> sum(cons(plusAC(x,y),l)) sum(app(l,cons(x,cons(y,k)))) -> sum(app(l,sum(cons(x,cons(y,k))))) sum(cons(0(),cons(plusAC(x,y),l))) -> pred(sum(cons(s(x),cons(y,l)))) plusAC(0(),y) -> y plusAC(s(x),y) -> s(plusAC(x,y)) pred(cons(s(x),nil())) -> cons(x,nil()) 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: app#(cons(x,l),k) -> app#(l,k) 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) = [0,1] pi(app#) = 0 precedence: app# > cons weight function: [app#](x0, x1) = x0, [cons](x0, x1) = x0 + x1 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(0(),cons(plusAC(x,y),l))) -> sum#(cons(s(x),cons(y,l))) sum#(cons(x,cons(y,l))) -> sum#(cons(plusAC(x,y),l)) 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: app(nil(),k) -> k app(l,nil()) -> l app(cons(x,l),k) -> cons(x,app(l,k)) sum(cons(x,nil())) -> cons(x,nil()) sum(cons(x,cons(y,l))) -> sum(cons(plusAC(x,y),l)) sum(app(l,cons(x,cons(y,k)))) -> sum(app(l,sum(cons(x,cons(y,k))))) sum(cons(0(),cons(plusAC(x,y),l))) -> pred(sum(cons(s(x),cons(y,l)))) plusAC(0(),y) -> y plusAC(s(x),y) -> s(plusAC(x,y)) pred(cons(s(x),nil())) -> cons(x,nil()) 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(0(),cons(plusAC(x,y),l))) -> sum#(cons(s(x),cons(y,l))) sum#(cons(x,cons(y,l))) -> sum#(cons(plusAC(x,y),l)) 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: app(nil(),k) -> k app(l,nil()) -> l app(cons(x,l),k) -> cons(x,app(l,k)) sum(cons(x,nil())) -> cons(x,nil()) sum(cons(x,cons(y,l))) -> sum(cons(plusAC(x,y),l)) sum(app(l,cons(x,cons(y,k)))) -> sum(app(l,sum(cons(x,cons(y,k))))) sum(cons(0(),cons(plusAC(x,y),l))) -> pred(sum(cons(s(x),cons(y,l)))) plusAC(0(),y) -> y plusAC(s(x),y) -> s(plusAC(x,y)) pred(cons(s(x),nil())) -> cons(x,nil()) 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(0(),cons(plusAC(x,y),l))) -> sum#(cons(s(x),cons(y,l))) sum#(cons(x,cons(y,l))) -> sum#(cons(plusAC(x,y),l)) 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(0(),y) -> y plusAC(s(x),y) -> s(plusAC(x,y)) 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(cons) = [0,1] pi(0) = [] pi(s) = [] pi(sum#) = [0] precedence: sum# > plusAC > s ~ 0 ~ cons weight function: [sum#](x0) = 2x0, [s](x0) = 6, [0] = 7, [cons](x0, x1) = x0 + 4x1 + 2, [plusAC](x0, x1) = x0 + x1 usable rules: plusAC(0(),y) -> y plusAC(s(x),y) -> s(plusAC(x,y)) 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(0(),y) -> y plusAC(s(x),y) -> s(plusAC(x,y)) 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,#}(s(x),y) -> plus{AC,#}(x,y) plus{AC,#}(x8,plusAC(s(x),y)) -> plus{AC,#}(x8,s(plusAC(x,y))) plus{AC,#}(x8,plusAC(s(x),y)) -> plus{AC,#}(x,y) plus{AC,#}(x7,plusAC(0(),y)) -> plus{AC,#}(x7,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: app(nil(),k) -> k app(l,nil()) -> l app(cons(x,l),k) -> cons(x,app(l,k)) sum(cons(x,nil())) -> cons(x,nil()) sum(cons(x,cons(y,l))) -> sum(cons(plusAC(x,y),l)) sum(app(l,cons(x,cons(y,k)))) -> sum(app(l,sum(cons(x,cons(y,k))))) sum(cons(0(),cons(plusAC(x,y),l))) -> pred(sum(cons(s(x),cons(y,l)))) plusAC(0(),y) -> y plusAC(s(x),y) -> s(plusAC(x,y)) pred(cons(s(x),nil())) -> cons(x,nil()) 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(s(x),y) -> plusAC(x,y) plusAC(x8,plusAC(s(x),y)) -> plusAC(x8,s(plusAC(x,y))) plusAC(x8,plusAC(s(x),y)) -> plusAC(x,y) plusAC(x7,plusAC(0(),y)) -> plusAC(x7,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: app(nil(),k) -> k app(l,nil()) -> l app(cons(x,l),k) -> cons(x,app(l,k)) sum(cons(x,nil())) -> cons(x,nil()) sum(cons(x,cons(y,l))) -> sum(cons(plusAC(x,y),l)) sum(app(l,cons(x,cons(y,k)))) -> sum(app(l,sum(cons(x,cons(y,k))))) sum(cons(0(),cons(plusAC(x,y),l))) -> pred(sum(cons(s(x),cons(y,l)))) plusAC(0(),y) -> y plusAC(s(x),y) -> s(plusAC(x,y)) pred(cons(s(x),nil())) -> cons(x,nil()) 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(s(x),y) -> plusAC(x,y) plusAC(x8,plusAC(s(x),y)) -> plusAC(x8,s(plusAC(x,y))) plusAC(x8,plusAC(s(x),y)) -> plusAC(x,y) plusAC(x7,plusAC(0(),y)) -> plusAC(x7,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(0(),y) -> y plusAC(s(x),y) -> s(plusAC(x,y)) 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: plusAC > s ~ 0 weight function: [s](x0) = x0 + 4, [0] = 4, [plusAC](x0, x1) = x0 + x1 usable rules: plusAC(0(),y) -> y plusAC(s(x),y) -> s(plusAC(x,y)) 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(0(),y) -> y plusAC(s(x),y) -> s(plusAC(x,y)) S: plusAC(plusAC(x9,x10),x11) -> plusAC(x9,x10) plusAC(x9,plusAC(x10,x11)) -> plusAC(x10,x11) Qed