YES Time: 1.008 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: s > quot# ~ minus ~ 0 ~ plusAC weight function: [quot#](x0, x1) = x0, [s](x0) = x0 + 1, [minus](x0, x1) = x0, [0] = 2, [plusAC](x0, x1) = x0 + x1 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 > minus# ~ s ~ 0 ~ plusAC weight function: [minus#](x0, x1) = x0, [s](x0) = 3x0 + 5, [minus](x0, x1) = x0, [0] = 1, [plusAC](x0, x1) = x0 + x1 + 1 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: minus#(minus(x,y),z) -> minus#(x,plusAC(y,z)) 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) Restore Modifier: 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)) 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-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)) 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) = [] pi(minus#) = 0 precedence: minus# > s > minus ~ 0 ~ plusAC weight function: [minus#](x0, x1) = x0, [s](x0) = 4, [minus](x0, x1) = 4x0 + 4, [0] = 2, [plusAC](x0, x1) = x0 + x1 + 5 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: sum# > sum > app > cons ~ nil ~ s ~ 0 ~ plusAC weight function: [sum#](x0) = 4x0, [sum](x0) = 4, [cons](x0, x1) = x1 + 3, [app](x0, x1) = 2x0 + 4x1, [nil] = 1, [s](x0) = 4, [0] = 1, [plusAC](x0, x1) = x0 + x1 usable rules: sum(cons(x,cons(y,l))) -> sum(cons(plusAC(x,y),l)) sum(cons(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(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 precedence: app# > cons weight function: [app#](x0, x1) = x0, [cons](x0, x1) = x0 + x1 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# > s > cons ~ 0 ~ plusAC weight function: [sum#](x0) = 4x0, [cons](x0, x1) = 4x1 + 1, [s](x0) = 4, [0] = 5, [plusAC](x0, x1) = x0 + x1 + 1 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: plusAC > s ~ 0 weight function: [s](x0) = x0 + 7, [0] = 3, [plusAC](x0, x1) = x0 + x1 + 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