YES Time: 0.510 Problem: Equations: plusAC(plusAC(x5,x6),x7) -> plusAC(x5,plusAC(x6,x7)) plusAC(x5,x6) -> plusAC(x6,x5) plusAC(x5,plusAC(x6,x7)) -> plusAC(plusAC(x5,x6),x7) plusAC(x6,x5) -> plusAC(x5,x6) TRS: minus(x,0()) -> x minus(s(x),s(y)) -> minus(x,y) minus(minus(x,y),z) -> minus(x,plusAC(y,z)) quot(0(),s(y)) -> 0() quot(s(x),s(y)) -> s(quot(minus(x,y),s(y))) plusAC(0(),y) -> y plusAC(s(x),y) -> s(plusAC(x,y)) 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))))) Proof: DP Processor: Equations#: plus{AC,#}(plusAC(x5,x6),x7) -> plus{AC,#}(x5,plusAC(x6,x7)) plus{AC,#}(x5,x6) -> plus{AC,#}(x6,x5) plus{AC,#}(x5,plusAC(x6,x7)) -> plus{AC,#}(plusAC(x5,x6),x7) plus{AC,#}(x6,x5) -> plus{AC,#}(x5,x6) DPs: minus#(s(x),s(y)) -> minus#(x,y) minus#(minus(x,y),z) -> plus{AC,#}(y,z) minus#(minus(x,y),z) -> minus#(x,plusAC(y,z)) quot#(s(x),s(y)) -> minus#(x,y) quot#(s(x),s(y)) -> quot#(minus(x,y),s(y)) plus{AC,#}(s(x),y) -> plus{AC,#}(x,y) 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))))) plus{AC,#}(x8,plusAC(0(),y)) -> plus{AC,#}(x8,y) plus{AC,#}(x9,plusAC(s(x),y)) -> plus{AC,#}(x,y) plus{AC,#}(x9,plusAC(s(x),y)) -> plus{AC,#}(x9,s(plusAC(x,y))) Equations: plusAC(plusAC(x5,x6),x7) -> plusAC(x5,plusAC(x6,x7)) plusAC(x5,x6) -> plusAC(x6,x5) plusAC(x5,plusAC(x6,x7)) -> plusAC(plusAC(x5,x6),x7) plusAC(x6,x5) -> plusAC(x5,x6) TRS: minus(x,0()) -> x minus(s(x),s(y)) -> minus(x,y) minus(minus(x,y),z) -> minus(x,plusAC(y,z)) quot(0(),s(y)) -> 0() quot(s(x),s(y)) -> s(quot(minus(x,y),s(y))) plusAC(0(),y) -> y plusAC(s(x),y) -> s(plusAC(x,y)) 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))))) S: plus{AC,#}(plusAC(x10,x11),x12) -> plus{AC,#}(x10,x11) plus{AC,#}(x10,plusAC(x11,x12)) -> plus{AC,#}(x11,x12) AC-EDG Processor: Equations#: plus{AC,#}(plusAC(x5,x6),x7) -> plus{AC,#}(x5,plusAC(x6,x7)) plus{AC,#}(x5,x6) -> plus{AC,#}(x6,x5) plus{AC,#}(x5,plusAC(x6,x7)) -> plus{AC,#}(plusAC(x5,x6),x7) plus{AC,#}(x6,x5) -> plus{AC,#}(x5,x6) DPs: minus#(s(x),s(y)) -> minus#(x,y) minus#(minus(x,y),z) -> plus{AC,#}(y,z) minus#(minus(x,y),z) -> minus#(x,plusAC(y,z)) quot#(s(x),s(y)) -> minus#(x,y) quot#(s(x),s(y)) -> quot#(minus(x,y),s(y)) plus{AC,#}(s(x),y) -> plus{AC,#}(x,y) 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))))) plus{AC,#}(x8,plusAC(0(),y)) -> plus{AC,#}(x8,y) plus{AC,#}(x9,plusAC(s(x),y)) -> plus{AC,#}(x,y) plus{AC,#}(x9,plusAC(s(x),y)) -> plus{AC,#}(x9,s(plusAC(x,y))) Equations: plusAC(plusAC(x5,x6),x7) -> plusAC(x5,plusAC(x6,x7)) plusAC(x5,x6) -> plusAC(x6,x5) plusAC(x5,plusAC(x6,x7)) -> plusAC(plusAC(x5,x6),x7) plusAC(x6,x5) -> plusAC(x5,x6) TRS: minus(x,0()) -> x minus(s(x),s(y)) -> minus(x,y) minus(minus(x,y),z) -> minus(x,plusAC(y,z)) quot(0(),s(y)) -> 0() quot(s(x),s(y)) -> s(quot(minus(x,y),s(y))) plusAC(0(),y) -> y plusAC(s(x),y) -> s(plusAC(x,y)) 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))))) S: plus{AC,#}(plusAC(x10,x11),x12) -> plus{AC,#}(x10,x11) plus{AC,#}(x10,plusAC(x11,x12)) -> plus{AC,#}(x11,x12) SCC Processor: #sccs: 6 #rules: 10 #arcs: 46/225 Equations#: plus{AC,#}(plusAC(x5,x6),x7) -> plus{AC,#}(x5,plusAC(x6,x7)) plus{AC,#}(x5,x6) -> plus{AC,#}(x6,x5) plus{AC,#}(x5,plusAC(x6,x7)) -> plus{AC,#}(plusAC(x5,x6),x7) plus{AC,#}(x6,x5) -> plus{AC,#}(x5,x6) DPs: quot#(s(x),s(y)) -> quot#(minus(x,y),s(y)) Equations: plusAC(plusAC(x5,x6),x7) -> plusAC(x5,plusAC(x6,x7)) plusAC(x5,x6) -> plusAC(x6,x5) plusAC(x5,plusAC(x6,x7)) -> plusAC(plusAC(x5,x6),x7) plusAC(x6,x5) -> plusAC(x5,x6) TRS: minus(x,0()) -> x minus(s(x),s(y)) -> minus(x,y) minus(minus(x,y),z) -> minus(x,plusAC(y,z)) quot(0(),s(y)) -> 0() quot(s(x),s(y)) -> s(quot(minus(x,y),s(y))) plusAC(0(),y) -> y plusAC(s(x),y) -> s(plusAC(x,y)) 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))))) S: plus{AC,#}(plusAC(x10,x11),x12) -> plus{AC,#}(x10,x11) plus{AC,#}(x10,plusAC(x11,x12)) -> plus{AC,#}(x11,x12) AC-DP unlabeling: Equations#: plusAC(plusAC(x5,x6),x7) -> plusAC(x5,plusAC(x6,x7)) plusAC(x5,x6) -> plusAC(x6,x5) plusAC(x5,plusAC(x6,x7)) -> plusAC(plusAC(x5,x6),x7) plusAC(x6,x5) -> plusAC(x5,x6) DPs: quot#(s(x),s(y)) -> quot#(minus(x,y),s(y)) Equations: plusAC(plusAC(x5,x6),x7) -> plusAC(x5,plusAC(x6,x7)) plusAC(x5,x6) -> plusAC(x6,x5) plusAC(x5,plusAC(x6,x7)) -> plusAC(plusAC(x5,x6),x7) plusAC(x6,x5) -> plusAC(x5,x6) TRS: minus(x,0()) -> x minus(s(x),s(y)) -> minus(x,y) minus(minus(x,y),z) -> minus(x,plusAC(y,z)) quot(0(),s(y)) -> 0() quot(s(x),s(y)) -> s(quot(minus(x,y),s(y))) plusAC(0(),y) -> y plusAC(s(x),y) -> s(plusAC(x,y)) 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))))) S: plusAC(plusAC(x10,x11),x12) -> plusAC(x10,x11) plusAC(x10,plusAC(x11,x12)) -> plusAC(x11,x12) Usable Rule Processor: Equations#: plusAC(plusAC(x5,x6),x7) -> plusAC(x5,plusAC(x6,x7)) plusAC(x5,x6) -> plusAC(x6,x5) plusAC(x5,plusAC(x6,x7)) -> plusAC(plusAC(x5,x6),x7) plusAC(x6,x5) -> plusAC(x5,x6) DPs: quot#(s(x),s(y)) -> quot#(minus(x,y),s(y)) Equations: plusAC(plusAC(x5,x6),x7) -> plusAC(x5,plusAC(x6,x7)) plusAC(x5,x6) -> plusAC(x6,x5) plusAC(x5,plusAC(x6,x7)) -> plusAC(plusAC(x5,x6),x7) plusAC(x6,x5) -> plusAC(x5,x6) TRS: minus(x,0()) -> x minus(s(x),s(y)) -> minus(x,y) minus(minus(x,y),z) -> minus(x,plusAC(y,z)) plusAC(0(),y) -> y plusAC(s(x),y) -> s(plusAC(x,y)) S: plusAC(plusAC(x10,x11),x12) -> plusAC(x10,x11) plusAC(x10,plusAC(x11,x12)) -> plusAC(x11,x12) AC-KBO Processor: argument filtering: pi(plusAC) = [0,1] pi(0) = [] pi(minus) = 0 pi(s) = [0] pi(quot#) = 0 precedence: quot# ~ s ~ minus ~ 0 > plusAC weight function: w0 = 2 w(minus) = 4 w(quot#) = w(0) = 2 w(s) = w(plusAC) = 0 usable rules: minus(x,0()) -> x minus(s(x),s(y)) -> minus(x,y) minus(minus(x,y),z) -> minus(x,plusAC(y,z)) problem: Equations#: plusAC(plusAC(x5,x6),x7) -> plusAC(x5,plusAC(x6,x7)) plusAC(x5,x6) -> plusAC(x6,x5) plusAC(x5,plusAC(x6,x7)) -> plusAC(plusAC(x5,x6),x7) plusAC(x6,x5) -> plusAC(x5,x6) DPs: Equations: plusAC(plusAC(x5,x6),x7) -> plusAC(x5,plusAC(x6,x7)) plusAC(x5,x6) -> plusAC(x6,x5) plusAC(x5,plusAC(x6,x7)) -> plusAC(plusAC(x5,x6),x7) plusAC(x6,x5) -> plusAC(x5,x6) TRS: minus(x,0()) -> x minus(s(x),s(y)) -> minus(x,y) minus(minus(x,y),z) -> minus(x,plusAC(y,z)) plusAC(0(),y) -> y plusAC(s(x),y) -> s(plusAC(x,y)) S: plusAC(plusAC(x10,x11),x12) -> plusAC(x10,x11) plusAC(x10,plusAC(x11,x12)) -> plusAC(x11,x12) Qed Equations#: plus{AC,#}(plusAC(x5,x6),x7) -> plus{AC,#}(x5,plusAC(x6,x7)) plus{AC,#}(x5,x6) -> plus{AC,#}(x6,x5) plus{AC,#}(x5,plusAC(x6,x7)) -> plus{AC,#}(plusAC(x5,x6),x7) plus{AC,#}(x6,x5) -> plus{AC,#}(x5,x6) DPs: minus#(minus(x,y),z) -> minus#(x,plusAC(y,z)) minus#(s(x),s(y)) -> minus#(x,y) Equations: plusAC(plusAC(x5,x6),x7) -> plusAC(x5,plusAC(x6,x7)) plusAC(x5,x6) -> plusAC(x6,x5) plusAC(x5,plusAC(x6,x7)) -> plusAC(plusAC(x5,x6),x7) plusAC(x6,x5) -> plusAC(x5,x6) TRS: minus(x,0()) -> x minus(s(x),s(y)) -> minus(x,y) minus(minus(x,y),z) -> minus(x,plusAC(y,z)) quot(0(),s(y)) -> 0() quot(s(x),s(y)) -> s(quot(minus(x,y),s(y))) plusAC(0(),y) -> y plusAC(s(x),y) -> s(plusAC(x,y)) 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))))) S: plus{AC,#}(plusAC(x10,x11),x12) -> plus{AC,#}(x10,x11) plus{AC,#}(x10,plusAC(x11,x12)) -> plus{AC,#}(x11,x12) AC-DP unlabeling: Equations#: plusAC(plusAC(x5,x6),x7) -> plusAC(x5,plusAC(x6,x7)) plusAC(x5,x6) -> plusAC(x6,x5) plusAC(x5,plusAC(x6,x7)) -> plusAC(plusAC(x5,x6),x7) plusAC(x6,x5) -> plusAC(x5,x6) DPs: minus#(minus(x,y),z) -> minus#(x,plusAC(y,z)) minus#(s(x),s(y)) -> minus#(x,y) Equations: plusAC(plusAC(x5,x6),x7) -> plusAC(x5,plusAC(x6,x7)) plusAC(x5,x6) -> plusAC(x6,x5) plusAC(x5,plusAC(x6,x7)) -> plusAC(plusAC(x5,x6),x7) plusAC(x6,x5) -> plusAC(x5,x6) TRS: minus(x,0()) -> x minus(s(x),s(y)) -> minus(x,y) minus(minus(x,y),z) -> minus(x,plusAC(y,z)) quot(0(),s(y)) -> 0() quot(s(x),s(y)) -> s(quot(minus(x,y),s(y))) plusAC(0(),y) -> y plusAC(s(x),y) -> s(plusAC(x,y)) 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))))) S: plusAC(plusAC(x10,x11),x12) -> plusAC(x10,x11) plusAC(x10,plusAC(x11,x12)) -> plusAC(x11,x12) Usable Rule Processor: Equations#: plusAC(plusAC(x5,x6),x7) -> plusAC(x5,plusAC(x6,x7)) plusAC(x5,x6) -> plusAC(x6,x5) plusAC(x5,plusAC(x6,x7)) -> plusAC(plusAC(x5,x6),x7) plusAC(x6,x5) -> plusAC(x5,x6) DPs: minus#(minus(x,y),z) -> minus#(x,plusAC(y,z)) minus#(s(x),s(y)) -> minus#(x,y) Equations: plusAC(plusAC(x5,x6),x7) -> plusAC(x5,plusAC(x6,x7)) plusAC(x5,x6) -> plusAC(x6,x5) plusAC(x5,plusAC(x6,x7)) -> plusAC(plusAC(x5,x6),x7) plusAC(x6,x5) -> plusAC(x5,x6) TRS: plusAC(0(),y) -> y plusAC(s(x),y) -> s(plusAC(x,y)) S: plusAC(plusAC(x10,x11),x12) -> plusAC(x10,x11) plusAC(x10,plusAC(x11,x12)) -> plusAC(x11,x12) AC-KBO Processor: argument filtering: pi(plusAC) = [0,1] pi(0) = [] pi(minus) = [0] pi(s) = [0] pi(minus#) = 0 precedence: minus# ~ s ~ minus ~ 0 > plusAC weight function: w0 = 4 w(0) = 7 w(plusAC) = 6 w(s) = 5 w(minus#) = 4 w(minus) = 0 usable rules: problem: Equations#: plusAC(plusAC(x5,x6),x7) -> plusAC(x5,plusAC(x6,x7)) plusAC(x5,x6) -> plusAC(x6,x5) plusAC(x5,plusAC(x6,x7)) -> plusAC(plusAC(x5,x6),x7) plusAC(x6,x5) -> plusAC(x5,x6) DPs: Equations: plusAC(plusAC(x5,x6),x7) -> plusAC(x5,plusAC(x6,x7)) plusAC(x5,x6) -> plusAC(x6,x5) plusAC(x5,plusAC(x6,x7)) -> plusAC(plusAC(x5,x6),x7) plusAC(x6,x5) -> plusAC(x5,x6) TRS: plusAC(0(),y) -> y plusAC(s(x),y) -> s(plusAC(x,y)) S: plusAC(plusAC(x10,x11),x12) -> plusAC(x10,x11) plusAC(x10,plusAC(x11,x12)) -> plusAC(x11,x12) Qed Equations#: plus{AC,#}(plusAC(x5,x6),x7) -> plus{AC,#}(x5,plusAC(x6,x7)) plus{AC,#}(x5,x6) -> plus{AC,#}(x6,x5) plus{AC,#}(x5,plusAC(x6,x7)) -> plus{AC,#}(plusAC(x5,x6),x7) plus{AC,#}(x6,x5) -> plus{AC,#}(x5,x6) DPs: sum#(app(l,cons(x,cons(y,k)))) -> sum#(app(l,sum(cons(x,cons(y,k))))) Equations: plusAC(plusAC(x5,x6),x7) -> plusAC(x5,plusAC(x6,x7)) plusAC(x5,x6) -> plusAC(x6,x5) plusAC(x5,plusAC(x6,x7)) -> plusAC(plusAC(x5,x6),x7) plusAC(x6,x5) -> plusAC(x5,x6) TRS: minus(x,0()) -> x minus(s(x),s(y)) -> minus(x,y) minus(minus(x,y),z) -> minus(x,plusAC(y,z)) quot(0(),s(y)) -> 0() quot(s(x),s(y)) -> s(quot(minus(x,y),s(y))) plusAC(0(),y) -> y plusAC(s(x),y) -> s(plusAC(x,y)) 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))))) S: plus{AC,#}(plusAC(x10,x11),x12) -> plus{AC,#}(x10,x11) plus{AC,#}(x10,plusAC(x11,x12)) -> plus{AC,#}(x11,x12) AC-DP unlabeling: Equations#: plusAC(plusAC(x5,x6),x7) -> plusAC(x5,plusAC(x6,x7)) plusAC(x5,x6) -> plusAC(x6,x5) plusAC(x5,plusAC(x6,x7)) -> plusAC(plusAC(x5,x6),x7) plusAC(x6,x5) -> plusAC(x5,x6) DPs: sum#(app(l,cons(x,cons(y,k)))) -> sum#(app(l,sum(cons(x,cons(y,k))))) Equations: plusAC(plusAC(x5,x6),x7) -> plusAC(x5,plusAC(x6,x7)) plusAC(x5,x6) -> plusAC(x6,x5) plusAC(x5,plusAC(x6,x7)) -> plusAC(plusAC(x5,x6),x7) plusAC(x6,x5) -> plusAC(x5,x6) TRS: minus(x,0()) -> x minus(s(x),s(y)) -> minus(x,y) minus(minus(x,y),z) -> minus(x,plusAC(y,z)) quot(0(),s(y)) -> 0() quot(s(x),s(y)) -> s(quot(minus(x,y),s(y))) plusAC(0(),y) -> y plusAC(s(x),y) -> s(plusAC(x,y)) 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))))) S: plusAC(plusAC(x10,x11),x12) -> plusAC(x10,x11) plusAC(x10,plusAC(x11,x12)) -> plusAC(x11,x12) Usable Rule Processor: Equations#: plusAC(plusAC(x5,x6),x7) -> plusAC(x5,plusAC(x6,x7)) plusAC(x5,x6) -> plusAC(x6,x5) plusAC(x5,plusAC(x6,x7)) -> plusAC(plusAC(x5,x6),x7) plusAC(x6,x5) -> plusAC(x5,x6) DPs: sum#(app(l,cons(x,cons(y,k)))) -> sum#(app(l,sum(cons(x,cons(y,k))))) Equations: plusAC(plusAC(x5,x6),x7) -> plusAC(x5,plusAC(x6,x7)) plusAC(x5,x6) -> plusAC(x6,x5) plusAC(x5,plusAC(x6,x7)) -> plusAC(plusAC(x5,x6),x7) plusAC(x6,x5) -> plusAC(x5,x6) TRS: sum(cons(x,cons(y,l))) -> sum(cons(plusAC(x,y),l)) sum(cons(x,nil())) -> cons(x,nil()) plusAC(0(),y) -> y plusAC(s(x),y) -> s(plusAC(x,y)) app(nil(),k) -> k app(l,nil()) -> l app(cons(x,l),k) -> cons(x,app(l,k)) S: plusAC(plusAC(x10,x11),x12) -> plusAC(x10,x11) plusAC(x10,plusAC(x11,x12)) -> plusAC(x11,x12) AC-KBO Processor: argument filtering: pi(plusAC) = [0,1] pi(0) = [] pi(s) = [] pi(nil) = [] pi(app) = [0,1] pi(cons) = [1] pi(sum) = [] pi(sum#) = 0 precedence: app ~ nil ~ s ~ 0 > cons > sum# ~ sum ~ plusAC weight function: w0 = 2 w(plusAC) = 7 w(sum) = 6 w(sum#) = 5 w(0) = 4 w(cons) = w(app) = w(nil) = w(s) = 2 usable rules: sum(cons(x,cons(y,l))) -> sum(cons(plusAC(x,y),l)) sum(cons(x,nil())) -> cons(x,nil()) plusAC(0(),y) -> y plusAC(s(x),y) -> s(plusAC(x,y)) app(nil(),k) -> k app(l,nil()) -> l app(cons(x,l),k) -> cons(x,app(l,k)) problem: Equations#: plusAC(plusAC(x5,x6),x7) -> plusAC(x5,plusAC(x6,x7)) plusAC(x5,x6) -> plusAC(x6,x5) plusAC(x5,plusAC(x6,x7)) -> plusAC(plusAC(x5,x6),x7) plusAC(x6,x5) -> plusAC(x5,x6) DPs: Equations: plusAC(plusAC(x5,x6),x7) -> plusAC(x5,plusAC(x6,x7)) plusAC(x5,x6) -> plusAC(x6,x5) plusAC(x5,plusAC(x6,x7)) -> plusAC(plusAC(x5,x6),x7) plusAC(x6,x5) -> plusAC(x5,x6) TRS: sum(cons(x,cons(y,l))) -> sum(cons(plusAC(x,y),l)) sum(cons(x,nil())) -> cons(x,nil()) plusAC(0(),y) -> y plusAC(s(x),y) -> s(plusAC(x,y)) app(nil(),k) -> k app(l,nil()) -> l app(cons(x,l),k) -> cons(x,app(l,k)) S: plusAC(plusAC(x10,x11),x12) -> plusAC(x10,x11) plusAC(x10,plusAC(x11,x12)) -> plusAC(x11,x12) Qed Equations#: plus{AC,#}(plusAC(x5,x6),x7) -> plus{AC,#}(x5,plusAC(x6,x7)) plus{AC,#}(x5,x6) -> plus{AC,#}(x6,x5) plus{AC,#}(x5,plusAC(x6,x7)) -> plus{AC,#}(plusAC(x5,x6),x7) plus{AC,#}(x6,x5) -> plus{AC,#}(x5,x6) DPs: app#(cons(x,l),k) -> app#(l,k) Equations: plusAC(plusAC(x5,x6),x7) -> plusAC(x5,plusAC(x6,x7)) plusAC(x5,x6) -> plusAC(x6,x5) plusAC(x5,plusAC(x6,x7)) -> plusAC(plusAC(x5,x6),x7) plusAC(x6,x5) -> plusAC(x5,x6) TRS: minus(x,0()) -> x minus(s(x),s(y)) -> minus(x,y) minus(minus(x,y),z) -> minus(x,plusAC(y,z)) quot(0(),s(y)) -> 0() quot(s(x),s(y)) -> s(quot(minus(x,y),s(y))) plusAC(0(),y) -> y plusAC(s(x),y) -> s(plusAC(x,y)) 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))))) S: plus{AC,#}(plusAC(x10,x11),x12) -> plus{AC,#}(x10,x11) plus{AC,#}(x10,plusAC(x11,x12)) -> plus{AC,#}(x11,x12) AC-DP unlabeling: Equations#: plusAC(plusAC(x5,x6),x7) -> plusAC(x5,plusAC(x6,x7)) plusAC(x5,x6) -> plusAC(x6,x5) plusAC(x5,plusAC(x6,x7)) -> plusAC(plusAC(x5,x6),x7) plusAC(x6,x5) -> plusAC(x5,x6) DPs: app#(cons(x,l),k) -> app#(l,k) Equations: plusAC(plusAC(x5,x6),x7) -> plusAC(x5,plusAC(x6,x7)) plusAC(x5,x6) -> plusAC(x6,x5) plusAC(x5,plusAC(x6,x7)) -> plusAC(plusAC(x5,x6),x7) plusAC(x6,x5) -> plusAC(x5,x6) TRS: minus(x,0()) -> x minus(s(x),s(y)) -> minus(x,y) minus(minus(x,y),z) -> minus(x,plusAC(y,z)) quot(0(),s(y)) -> 0() quot(s(x),s(y)) -> s(quot(minus(x,y),s(y))) plusAC(0(),y) -> y plusAC(s(x),y) -> s(plusAC(x,y)) 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))))) S: plusAC(plusAC(x10,x11),x12) -> plusAC(x10,x11) plusAC(x10,plusAC(x11,x12)) -> plusAC(x11,x12) Usable Rule Processor: Equations#: plusAC(plusAC(x5,x6),x7) -> plusAC(x5,plusAC(x6,x7)) plusAC(x5,x6) -> plusAC(x6,x5) plusAC(x5,plusAC(x6,x7)) -> plusAC(plusAC(x5,x6),x7) plusAC(x6,x5) -> plusAC(x5,x6) DPs: app#(cons(x,l),k) -> app#(l,k) Equations: plusAC(plusAC(x5,x6),x7) -> plusAC(x5,plusAC(x6,x7)) plusAC(x5,x6) -> plusAC(x6,x5) plusAC(x5,plusAC(x6,x7)) -> plusAC(plusAC(x5,x6),x7) plusAC(x6,x5) -> plusAC(x5,x6) TRS: S: plusAC(plusAC(x10,x11),x12) -> plusAC(x10,x11) plusAC(x10,plusAC(x11,x12)) -> plusAC(x11,x12) 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(x5,x6),x7) -> plusAC(x5,plusAC(x6,x7)) plusAC(x5,x6) -> plusAC(x6,x5) plusAC(x5,plusAC(x6,x7)) -> plusAC(plusAC(x5,x6),x7) plusAC(x6,x5) -> plusAC(x5,x6) DPs: Equations: plusAC(plusAC(x5,x6),x7) -> plusAC(x5,plusAC(x6,x7)) plusAC(x5,x6) -> plusAC(x6,x5) plusAC(x5,plusAC(x6,x7)) -> plusAC(plusAC(x5,x6),x7) plusAC(x6,x5) -> plusAC(x5,x6) TRS: S: plusAC(plusAC(x10,x11),x12) -> plusAC(x10,x11) plusAC(x10,plusAC(x11,x12)) -> plusAC(x11,x12) Qed Equations#: plus{AC,#}(plusAC(x5,x6),x7) -> plus{AC,#}(x5,plusAC(x6,x7)) plus{AC,#}(x5,x6) -> plus{AC,#}(x6,x5) plus{AC,#}(x5,plusAC(x6,x7)) -> plus{AC,#}(plusAC(x5,x6),x7) plus{AC,#}(x6,x5) -> plus{AC,#}(x5,x6) DPs: sum#(cons(x,cons(y,l))) -> sum#(cons(plusAC(x,y),l)) Equations: plusAC(plusAC(x5,x6),x7) -> plusAC(x5,plusAC(x6,x7)) plusAC(x5,x6) -> plusAC(x6,x5) plusAC(x5,plusAC(x6,x7)) -> plusAC(plusAC(x5,x6),x7) plusAC(x6,x5) -> plusAC(x5,x6) TRS: minus(x,0()) -> x minus(s(x),s(y)) -> minus(x,y) minus(minus(x,y),z) -> minus(x,plusAC(y,z)) quot(0(),s(y)) -> 0() quot(s(x),s(y)) -> s(quot(minus(x,y),s(y))) plusAC(0(),y) -> y plusAC(s(x),y) -> s(plusAC(x,y)) 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))))) S: plus{AC,#}(plusAC(x10,x11),x12) -> plus{AC,#}(x10,x11) plus{AC,#}(x10,plusAC(x11,x12)) -> plus{AC,#}(x11,x12) AC-DP unlabeling: Equations#: plusAC(plusAC(x5,x6),x7) -> plusAC(x5,plusAC(x6,x7)) plusAC(x5,x6) -> plusAC(x6,x5) plusAC(x5,plusAC(x6,x7)) -> plusAC(plusAC(x5,x6),x7) plusAC(x6,x5) -> plusAC(x5,x6) DPs: sum#(cons(x,cons(y,l))) -> sum#(cons(plusAC(x,y),l)) Equations: plusAC(plusAC(x5,x6),x7) -> plusAC(x5,plusAC(x6,x7)) plusAC(x5,x6) -> plusAC(x6,x5) plusAC(x5,plusAC(x6,x7)) -> plusAC(plusAC(x5,x6),x7) plusAC(x6,x5) -> plusAC(x5,x6) TRS: minus(x,0()) -> x minus(s(x),s(y)) -> minus(x,y) minus(minus(x,y),z) -> minus(x,plusAC(y,z)) quot(0(),s(y)) -> 0() quot(s(x),s(y)) -> s(quot(minus(x,y),s(y))) plusAC(0(),y) -> y plusAC(s(x),y) -> s(plusAC(x,y)) 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))))) S: plusAC(plusAC(x10,x11),x12) -> plusAC(x10,x11) plusAC(x10,plusAC(x11,x12)) -> plusAC(x11,x12) Usable Rule Processor: Equations#: plusAC(plusAC(x5,x6),x7) -> plusAC(x5,plusAC(x6,x7)) plusAC(x5,x6) -> plusAC(x6,x5) plusAC(x5,plusAC(x6,x7)) -> plusAC(plusAC(x5,x6),x7) plusAC(x6,x5) -> plusAC(x5,x6) DPs: sum#(cons(x,cons(y,l))) -> sum#(cons(plusAC(x,y),l)) Equations: plusAC(plusAC(x5,x6),x7) -> plusAC(x5,plusAC(x6,x7)) plusAC(x5,x6) -> plusAC(x6,x5) plusAC(x5,plusAC(x6,x7)) -> plusAC(plusAC(x5,x6),x7) plusAC(x6,x5) -> plusAC(x5,x6) TRS: plusAC(0(),y) -> y plusAC(s(x),y) -> s(plusAC(x,y)) S: plusAC(plusAC(x10,x11),x12) -> plusAC(x10,x11) plusAC(x10,plusAC(x11,x12)) -> plusAC(x11,x12) AC-KBO Processor: argument filtering: pi(plusAC) = [0,1] pi(0) = [] pi(s) = [] pi(cons) = [1] pi(sum#) = 0 precedence: sum# ~ cons ~ s ~ 0 ~ plusAC weight function: w0 = 4 w(plusAC) = 7 w(s) = 6 w(sum#) = w(0) = 4 w(cons) = 0 usable rules: problem: Equations#: plusAC(plusAC(x5,x6),x7) -> plusAC(x5,plusAC(x6,x7)) plusAC(x5,x6) -> plusAC(x6,x5) plusAC(x5,plusAC(x6,x7)) -> plusAC(plusAC(x5,x6),x7) plusAC(x6,x5) -> plusAC(x5,x6) DPs: Equations: plusAC(plusAC(x5,x6),x7) -> plusAC(x5,plusAC(x6,x7)) plusAC(x5,x6) -> plusAC(x6,x5) plusAC(x5,plusAC(x6,x7)) -> plusAC(plusAC(x5,x6),x7) plusAC(x6,x5) -> plusAC(x5,x6) TRS: plusAC(0(),y) -> y plusAC(s(x),y) -> s(plusAC(x,y)) S: plusAC(plusAC(x10,x11),x12) -> plusAC(x10,x11) plusAC(x10,plusAC(x11,x12)) -> plusAC(x11,x12) Qed Equations#: plus{AC,#}(plusAC(x5,x6),x7) -> plus{AC,#}(x5,plusAC(x6,x7)) plus{AC,#}(x5,x6) -> plus{AC,#}(x6,x5) plus{AC,#}(x5,plusAC(x6,x7)) -> plus{AC,#}(plusAC(x5,x6),x7) plus{AC,#}(x6,x5) -> plus{AC,#}(x5,x6) DPs: plus{AC,#}(x9,plusAC(s(x),y)) -> plus{AC,#}(x9,s(plusAC(x,y))) plus{AC,#}(x9,plusAC(s(x),y)) -> plus{AC,#}(x,y) plus{AC,#}(x8,plusAC(0(),y)) -> plus{AC,#}(x8,y) plus{AC,#}(s(x),y) -> plus{AC,#}(x,y) Equations: plusAC(plusAC(x5,x6),x7) -> plusAC(x5,plusAC(x6,x7)) plusAC(x5,x6) -> plusAC(x6,x5) plusAC(x5,plusAC(x6,x7)) -> plusAC(plusAC(x5,x6),x7) plusAC(x6,x5) -> plusAC(x5,x6) TRS: minus(x,0()) -> x minus(s(x),s(y)) -> minus(x,y) minus(minus(x,y),z) -> minus(x,plusAC(y,z)) quot(0(),s(y)) -> 0() quot(s(x),s(y)) -> s(quot(minus(x,y),s(y))) plusAC(0(),y) -> y plusAC(s(x),y) -> s(plusAC(x,y)) 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))))) S: plus{AC,#}(plusAC(x10,x11),x12) -> plus{AC,#}(x10,x11) plus{AC,#}(x10,plusAC(x11,x12)) -> plus{AC,#}(x11,x12) AC-DP unlabeling: Equations#: plusAC(plusAC(x5,x6),x7) -> plusAC(x5,plusAC(x6,x7)) plusAC(x5,x6) -> plusAC(x6,x5) plusAC(x5,plusAC(x6,x7)) -> plusAC(plusAC(x5,x6),x7) plusAC(x6,x5) -> plusAC(x5,x6) DPs: plusAC(x9,plusAC(s(x),y)) -> plusAC(x9,s(plusAC(x,y))) plusAC(x9,plusAC(s(x),y)) -> plusAC(x,y) plusAC(x8,plusAC(0(),y)) -> plusAC(x8,y) plusAC(s(x),y) -> plusAC(x,y) Equations: plusAC(plusAC(x5,x6),x7) -> plusAC(x5,plusAC(x6,x7)) plusAC(x5,x6) -> plusAC(x6,x5) plusAC(x5,plusAC(x6,x7)) -> plusAC(plusAC(x5,x6),x7) plusAC(x6,x5) -> plusAC(x5,x6) TRS: minus(x,0()) -> x minus(s(x),s(y)) -> minus(x,y) minus(minus(x,y),z) -> minus(x,plusAC(y,z)) quot(0(),s(y)) -> 0() quot(s(x),s(y)) -> s(quot(minus(x,y),s(y))) plusAC(0(),y) -> y plusAC(s(x),y) -> s(plusAC(x,y)) 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))))) S: plusAC(plusAC(x10,x11),x12) -> plusAC(x10,x11) plusAC(x10,plusAC(x11,x12)) -> plusAC(x11,x12) Usable Rule Processor: Equations#: plusAC(plusAC(x5,x6),x7) -> plusAC(x5,plusAC(x6,x7)) plusAC(x5,x6) -> plusAC(x6,x5) plusAC(x5,plusAC(x6,x7)) -> plusAC(plusAC(x5,x6),x7) plusAC(x6,x5) -> plusAC(x5,x6) DPs: plusAC(x9,plusAC(s(x),y)) -> plusAC(x9,s(plusAC(x,y))) plusAC(x9,plusAC(s(x),y)) -> plusAC(x,y) plusAC(x8,plusAC(0(),y)) -> plusAC(x8,y) plusAC(s(x),y) -> plusAC(x,y) Equations: plusAC(plusAC(x5,x6),x7) -> plusAC(x5,plusAC(x6,x7)) plusAC(x5,x6) -> plusAC(x6,x5) plusAC(x5,plusAC(x6,x7)) -> plusAC(plusAC(x5,x6),x7) plusAC(x6,x5) -> plusAC(x5,x6) TRS: plusAC(0(),y) -> y plusAC(s(x),y) -> s(plusAC(x,y)) S: plusAC(plusAC(x10,x11),x12) -> plusAC(x10,x11) plusAC(x10,plusAC(x11,x12)) -> plusAC(x11,x12) AC-KBO Processor: argument filtering: pi(plusAC) = [0,1] pi(0) = [] pi(s) = [0] precedence: 0 ~ plusAC > s weight function: w0 = 1 w(s) = 4 w(0) = w(plusAC) = 1 usable rules: plusAC(0(),y) -> y plusAC(s(x),y) -> s(plusAC(x,y)) problem: Equations#: plusAC(plusAC(x5,x6),x7) -> plusAC(x5,plusAC(x6,x7)) plusAC(x5,x6) -> plusAC(x6,x5) plusAC(x5,plusAC(x6,x7)) -> plusAC(plusAC(x5,x6),x7) plusAC(x6,x5) -> plusAC(x5,x6) DPs: Equations: plusAC(plusAC(x5,x6),x7) -> plusAC(x5,plusAC(x6,x7)) plusAC(x5,x6) -> plusAC(x6,x5) plusAC(x5,plusAC(x6,x7)) -> plusAC(plusAC(x5,x6),x7) plusAC(x6,x5) -> plusAC(x5,x6) TRS: plusAC(0(),y) -> y plusAC(s(x),y) -> s(plusAC(x,y)) S: plusAC(plusAC(x10,x11),x12) -> plusAC(x10,x11) plusAC(x10,plusAC(x11,x12)) -> plusAC(x11,x12) Qed