YES Time: 0.604 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) = 0 pi(sum#) = 0 precedence: s ~ 0 ~ app ~ nil > sum > sum# ~ pred ~ cons ~ plusAC weight function: w0 = 4 w(sum) = 6 w(sum#) = w(pred) = w(s) = w(0) = w(nil) = w(plusAC) = 4 w(cons) = 2 w(app) = 1 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,1] precedence: app# ~ cons weight function: w0 = 4 w(app#) = w(cons) = 4 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) = [1] pi(0) = [] pi(s) = [0] pi(sum#) = [0] precedence: sum# ~ s ~ 0 ~ cons ~ plusAC weight function: w0 = 4 w(plusAC) = 6 w(sum#) = w(0) = 4 w(s) = 2 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: sum#(cons(0(),cons(plusAC(x,y),l))) -> sum#(cons(s(x),cons(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) Restore Modifier: 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))) 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) SCC Processor: #sccs: 0 #rules: 0 #arcs: 3/1 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: 0 ~ plusAC > s weight function: w0 = 4 w(0) = 5 w(s) = 4 w(plusAC) = 0 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