YES Time: 0.164 Problem: Equations: plusAC(plusAC(x3,x4),x5) -> plusAC(x3,plusAC(x4,x5)) plusAC(x3,x4) -> plusAC(x4,x3) plusAC(x3,plusAC(x4,x5)) -> plusAC(plusAC(x3,x4),x5) plusAC(x4,x3) -> plusAC(x3,x4) TRS: sum(x,y) -> S(int(x,y)) S(nil()) -> 0() S(cons(x,xs)) -> plusAC(x,S(xs)) plusAC(x,0()) -> x plusAC(x,s(y)) -> s(plusAC(x,y)) int(0(),0()) -> cons(0(),nil()) int(0(),s(y)) -> cons(0(),int(s(0()),s(y))) int(s(x),0()) -> nil() int(s(x),s(y)) -> intlist(int(x,y)) intlist(nil()) -> nil() intlist(cons(x,y)) -> cons(s(x),intlist(y)) Proof: DP Processor: Equations#: plus{AC,#}(plusAC(x3,x4),x5) -> plus{AC,#}(x3,plusAC(x4,x5)) plus{AC,#}(x3,x4) -> plus{AC,#}(x4,x3) plus{AC,#}(x3,plusAC(x4,x5)) -> plus{AC,#}(plusAC(x3,x4),x5) plus{AC,#}(x4,x3) -> plus{AC,#}(x3,x4) DPs: sum#(x,y) -> int#(x,y) sum#(x,y) -> S#(int(x,y)) S#(cons(x,xs)) -> S#(xs) S#(cons(x,xs)) -> plus{AC,#}(x,S(xs)) plus{AC,#}(x,s(y)) -> plus{AC,#}(x,y) int#(0(),s(y)) -> int#(s(0()),s(y)) int#(s(x),s(y)) -> int#(x,y) int#(s(x),s(y)) -> intlist#(int(x,y)) intlist#(cons(x,y)) -> intlist#(y) plus{AC,#}(x6,plusAC(x,0())) -> plus{AC,#}(x6,x) plus{AC,#}(x7,plusAC(x,s(y))) -> plus{AC,#}(x,y) plus{AC,#}(x7,plusAC(x,s(y))) -> plus{AC,#}(x7,s(plusAC(x,y))) Equations: plusAC(plusAC(x3,x4),x5) -> plusAC(x3,plusAC(x4,x5)) plusAC(x3,x4) -> plusAC(x4,x3) plusAC(x3,plusAC(x4,x5)) -> plusAC(plusAC(x3,x4),x5) plusAC(x4,x3) -> plusAC(x3,x4) TRS: sum(x,y) -> S(int(x,y)) S(nil()) -> 0() S(cons(x,xs)) -> plusAC(x,S(xs)) plusAC(x,0()) -> x plusAC(x,s(y)) -> s(plusAC(x,y)) int(0(),0()) -> cons(0(),nil()) int(0(),s(y)) -> cons(0(),int(s(0()),s(y))) int(s(x),0()) -> nil() int(s(x),s(y)) -> intlist(int(x,y)) intlist(nil()) -> nil() intlist(cons(x,y)) -> cons(s(x),intlist(y)) S: plus{AC,#}(plusAC(x8,x9),x10) -> plus{AC,#}(x8,x9) plus{AC,#}(x8,plusAC(x9,x10)) -> plus{AC,#}(x9,x10) AC-EDG Processor: Equations#: plus{AC,#}(plusAC(x3,x4),x5) -> plus{AC,#}(x3,plusAC(x4,x5)) plus{AC,#}(x3,x4) -> plus{AC,#}(x4,x3) plus{AC,#}(x3,plusAC(x4,x5)) -> plus{AC,#}(plusAC(x3,x4),x5) plus{AC,#}(x4,x3) -> plus{AC,#}(x3,x4) DPs: sum#(x,y) -> int#(x,y) sum#(x,y) -> S#(int(x,y)) S#(cons(x,xs)) -> S#(xs) S#(cons(x,xs)) -> plus{AC,#}(x,S(xs)) plus{AC,#}(x,s(y)) -> plus{AC,#}(x,y) int#(0(),s(y)) -> int#(s(0()),s(y)) int#(s(x),s(y)) -> int#(x,y) int#(s(x),s(y)) -> intlist#(int(x,y)) intlist#(cons(x,y)) -> intlist#(y) plus{AC,#}(x6,plusAC(x,0())) -> plus{AC,#}(x6,x) plus{AC,#}(x7,plusAC(x,s(y))) -> plus{AC,#}(x,y) plus{AC,#}(x7,plusAC(x,s(y))) -> plus{AC,#}(x7,s(plusAC(x,y))) Equations: plusAC(plusAC(x3,x4),x5) -> plusAC(x3,plusAC(x4,x5)) plusAC(x3,x4) -> plusAC(x4,x3) plusAC(x3,plusAC(x4,x5)) -> plusAC(plusAC(x3,x4),x5) plusAC(x4,x3) -> plusAC(x3,x4) TRS: sum(x,y) -> S(int(x,y)) S(nil()) -> 0() S(cons(x,xs)) -> plusAC(x,S(xs)) plusAC(x,0()) -> x plusAC(x,s(y)) -> s(plusAC(x,y)) int(0(),0()) -> cons(0(),nil()) int(0(),s(y)) -> cons(0(),int(s(0()),s(y))) int(s(x),0()) -> nil() int(s(x),s(y)) -> intlist(int(x,y)) intlist(nil()) -> nil() intlist(cons(x,y)) -> cons(s(x),intlist(y)) S: plus{AC,#}(plusAC(x8,x9),x10) -> plus{AC,#}(x8,x9) plus{AC,#}(x8,plusAC(x9,x10)) -> plus{AC,#}(x9,x10) SCC Processor: #sccs: 4 #rules: 8 #arcs: 34/144 Equations#: plus{AC,#}(plusAC(x3,x4),x5) -> plus{AC,#}(x3,plusAC(x4,x5)) plus{AC,#}(x3,x4) -> plus{AC,#}(x4,x3) plus{AC,#}(x3,plusAC(x4,x5)) -> plus{AC,#}(plusAC(x3,x4),x5) plus{AC,#}(x4,x3) -> plus{AC,#}(x3,x4) DPs: int#(s(x),s(y)) -> int#(x,y) int#(0(),s(y)) -> int#(s(0()),s(y)) Equations: plusAC(plusAC(x3,x4),x5) -> plusAC(x3,plusAC(x4,x5)) plusAC(x3,x4) -> plusAC(x4,x3) plusAC(x3,plusAC(x4,x5)) -> plusAC(plusAC(x3,x4),x5) plusAC(x4,x3) -> plusAC(x3,x4) TRS: sum(x,y) -> S(int(x,y)) S(nil()) -> 0() S(cons(x,xs)) -> plusAC(x,S(xs)) plusAC(x,0()) -> x plusAC(x,s(y)) -> s(plusAC(x,y)) int(0(),0()) -> cons(0(),nil()) int(0(),s(y)) -> cons(0(),int(s(0()),s(y))) int(s(x),0()) -> nil() int(s(x),s(y)) -> intlist(int(x,y)) intlist(nil()) -> nil() intlist(cons(x,y)) -> cons(s(x),intlist(y)) S: plus{AC,#}(plusAC(x8,x9),x10) -> plus{AC,#}(x8,x9) plus{AC,#}(x8,plusAC(x9,x10)) -> plus{AC,#}(x9,x10) AC-DP unlabeling: Equations#: plusAC(plusAC(x3,x4),x5) -> plusAC(x3,plusAC(x4,x5)) plusAC(x3,x4) -> plusAC(x4,x3) plusAC(x3,plusAC(x4,x5)) -> plusAC(plusAC(x3,x4),x5) plusAC(x4,x3) -> plusAC(x3,x4) DPs: int#(s(x),s(y)) -> int#(x,y) int#(0(),s(y)) -> int#(s(0()),s(y)) Equations: plusAC(plusAC(x3,x4),x5) -> plusAC(x3,plusAC(x4,x5)) plusAC(x3,x4) -> plusAC(x4,x3) plusAC(x3,plusAC(x4,x5)) -> plusAC(plusAC(x3,x4),x5) plusAC(x4,x3) -> plusAC(x3,x4) TRS: sum(x,y) -> S(int(x,y)) S(nil()) -> 0() S(cons(x,xs)) -> plusAC(x,S(xs)) plusAC(x,0()) -> x plusAC(x,s(y)) -> s(plusAC(x,y)) int(0(),0()) -> cons(0(),nil()) int(0(),s(y)) -> cons(0(),int(s(0()),s(y))) int(s(x),0()) -> nil() int(s(x),s(y)) -> intlist(int(x,y)) intlist(nil()) -> nil() intlist(cons(x,y)) -> cons(s(x),intlist(y)) S: plusAC(plusAC(x8,x9),x10) -> plusAC(x8,x9) plusAC(x8,plusAC(x9,x10)) -> plusAC(x9,x10) Usable Rule Processor: Equations#: plusAC(plusAC(x3,x4),x5) -> plusAC(x3,plusAC(x4,x5)) plusAC(x3,x4) -> plusAC(x4,x3) plusAC(x3,plusAC(x4,x5)) -> plusAC(plusAC(x3,x4),x5) plusAC(x4,x3) -> plusAC(x3,x4) DPs: int#(s(x),s(y)) -> int#(x,y) int#(0(),s(y)) -> int#(s(0()),s(y)) Equations: plusAC(plusAC(x3,x4),x5) -> plusAC(x3,plusAC(x4,x5)) plusAC(x3,x4) -> plusAC(x4,x3) plusAC(x3,plusAC(x4,x5)) -> plusAC(plusAC(x3,x4),x5) plusAC(x4,x3) -> plusAC(x3,x4) TRS: S: plusAC(plusAC(x8,x9),x10) -> plusAC(x8,x9) plusAC(x8,plusAC(x9,x10)) -> plusAC(x9,x10) AC-KBO Processor: argument filtering: pi(0) = [] pi(s) = [0] pi(int#) = 1 precedence: int# ~ s ~ 0 weight function: w0 = 1 w(int#) = 6 w(0) = 2 w(s) = 0 usable rules: problem: Equations#: plusAC(plusAC(x3,x4),x5) -> plusAC(x3,plusAC(x4,x5)) plusAC(x3,x4) -> plusAC(x4,x3) plusAC(x3,plusAC(x4,x5)) -> plusAC(plusAC(x3,x4),x5) plusAC(x4,x3) -> plusAC(x3,x4) DPs: int#(0(),s(y)) -> int#(s(0()),s(y)) Equations: plusAC(plusAC(x3,x4),x5) -> plusAC(x3,plusAC(x4,x5)) plusAC(x3,x4) -> plusAC(x4,x3) plusAC(x3,plusAC(x4,x5)) -> plusAC(plusAC(x3,x4),x5) plusAC(x4,x3) -> plusAC(x3,x4) TRS: S: plusAC(plusAC(x8,x9),x10) -> plusAC(x8,x9) plusAC(x8,plusAC(x9,x10)) -> plusAC(x9,x10) Restore Modifier: Equations#: plusAC(plusAC(x3,x4),x5) -> plusAC(x3,plusAC(x4,x5)) plusAC(x3,x4) -> plusAC(x4,x3) plusAC(x3,plusAC(x4,x5)) -> plusAC(plusAC(x3,x4),x5) plusAC(x4,x3) -> plusAC(x3,x4) DPs: int#(0(),s(y)) -> int#(s(0()),s(y)) Equations: plusAC(plusAC(x3,x4),x5) -> plusAC(x3,plusAC(x4,x5)) plusAC(x3,x4) -> plusAC(x4,x3) plusAC(x3,plusAC(x4,x5)) -> plusAC(plusAC(x3,x4),x5) plusAC(x4,x3) -> plusAC(x3,x4) TRS: S: plusAC(plusAC(x8,x9),x10) -> plusAC(x8,x9) plusAC(x8,plusAC(x9,x10)) -> plusAC(x9,x10) SCC Processor: #sccs: 0 #rules: 0 #arcs: 3/1 Equations#: plus{AC,#}(plusAC(x3,x4),x5) -> plus{AC,#}(x3,plusAC(x4,x5)) plus{AC,#}(x3,x4) -> plus{AC,#}(x4,x3) plus{AC,#}(x3,plusAC(x4,x5)) -> plus{AC,#}(plusAC(x3,x4),x5) plus{AC,#}(x4,x3) -> plus{AC,#}(x3,x4) DPs: S#(cons(x,xs)) -> S#(xs) Equations: plusAC(plusAC(x3,x4),x5) -> plusAC(x3,plusAC(x4,x5)) plusAC(x3,x4) -> plusAC(x4,x3) plusAC(x3,plusAC(x4,x5)) -> plusAC(plusAC(x3,x4),x5) plusAC(x4,x3) -> plusAC(x3,x4) TRS: sum(x,y) -> S(int(x,y)) S(nil()) -> 0() S(cons(x,xs)) -> plusAC(x,S(xs)) plusAC(x,0()) -> x plusAC(x,s(y)) -> s(plusAC(x,y)) int(0(),0()) -> cons(0(),nil()) int(0(),s(y)) -> cons(0(),int(s(0()),s(y))) int(s(x),0()) -> nil() int(s(x),s(y)) -> intlist(int(x,y)) intlist(nil()) -> nil() intlist(cons(x,y)) -> cons(s(x),intlist(y)) S: plus{AC,#}(plusAC(x8,x9),x10) -> plus{AC,#}(x8,x9) plus{AC,#}(x8,plusAC(x9,x10)) -> plus{AC,#}(x9,x10) AC-DP unlabeling: Equations#: plusAC(plusAC(x3,x4),x5) -> plusAC(x3,plusAC(x4,x5)) plusAC(x3,x4) -> plusAC(x4,x3) plusAC(x3,plusAC(x4,x5)) -> plusAC(plusAC(x3,x4),x5) plusAC(x4,x3) -> plusAC(x3,x4) DPs: S#(cons(x,xs)) -> S#(xs) Equations: plusAC(plusAC(x3,x4),x5) -> plusAC(x3,plusAC(x4,x5)) plusAC(x3,x4) -> plusAC(x4,x3) plusAC(x3,plusAC(x4,x5)) -> plusAC(plusAC(x3,x4),x5) plusAC(x4,x3) -> plusAC(x3,x4) TRS: sum(x,y) -> S(int(x,y)) S(nil()) -> 0() S(cons(x,xs)) -> plusAC(x,S(xs)) plusAC(x,0()) -> x plusAC(x,s(y)) -> s(plusAC(x,y)) int(0(),0()) -> cons(0(),nil()) int(0(),s(y)) -> cons(0(),int(s(0()),s(y))) int(s(x),0()) -> nil() int(s(x),s(y)) -> intlist(int(x,y)) intlist(nil()) -> nil() intlist(cons(x,y)) -> cons(s(x),intlist(y)) S: plusAC(plusAC(x8,x9),x10) -> plusAC(x8,x9) plusAC(x8,plusAC(x9,x10)) -> plusAC(x9,x10) Usable Rule Processor: Equations#: plusAC(plusAC(x3,x4),x5) -> plusAC(x3,plusAC(x4,x5)) plusAC(x3,x4) -> plusAC(x4,x3) plusAC(x3,plusAC(x4,x5)) -> plusAC(plusAC(x3,x4),x5) plusAC(x4,x3) -> plusAC(x3,x4) DPs: S#(cons(x,xs)) -> S#(xs) Equations: plusAC(plusAC(x3,x4),x5) -> plusAC(x3,plusAC(x4,x5)) plusAC(x3,x4) -> plusAC(x4,x3) plusAC(x3,plusAC(x4,x5)) -> plusAC(plusAC(x3,x4),x5) plusAC(x4,x3) -> plusAC(x3,x4) TRS: S: plusAC(plusAC(x8,x9),x10) -> plusAC(x8,x9) plusAC(x8,plusAC(x9,x10)) -> plusAC(x9,x10) AC-KBO Processor: argument filtering: pi(cons) = [1] pi(S#) = 0 precedence: S# ~ cons weight function: w0 = 1 w(cons) = 2 w(S#) = 1 usable rules: problem: Equations#: plusAC(plusAC(x3,x4),x5) -> plusAC(x3,plusAC(x4,x5)) plusAC(x3,x4) -> plusAC(x4,x3) plusAC(x3,plusAC(x4,x5)) -> plusAC(plusAC(x3,x4),x5) plusAC(x4,x3) -> plusAC(x3,x4) DPs: Equations: plusAC(plusAC(x3,x4),x5) -> plusAC(x3,plusAC(x4,x5)) plusAC(x3,x4) -> plusAC(x4,x3) plusAC(x3,plusAC(x4,x5)) -> plusAC(plusAC(x3,x4),x5) plusAC(x4,x3) -> plusAC(x3,x4) TRS: S: plusAC(plusAC(x8,x9),x10) -> plusAC(x8,x9) plusAC(x8,plusAC(x9,x10)) -> plusAC(x9,x10) Qed Equations#: plus{AC,#}(plusAC(x3,x4),x5) -> plus{AC,#}(x3,plusAC(x4,x5)) plus{AC,#}(x3,x4) -> plus{AC,#}(x4,x3) plus{AC,#}(x3,plusAC(x4,x5)) -> plus{AC,#}(plusAC(x3,x4),x5) plus{AC,#}(x4,x3) -> plus{AC,#}(x3,x4) DPs: plus{AC,#}(x7,plusAC(x,s(y))) -> plus{AC,#}(x7,s(plusAC(x,y))) plus{AC,#}(x7,plusAC(x,s(y))) -> plus{AC,#}(x,y) plus{AC,#}(x6,plusAC(x,0())) -> plus{AC,#}(x6,x) plus{AC,#}(x,s(y)) -> plus{AC,#}(x,y) Equations: plusAC(plusAC(x3,x4),x5) -> plusAC(x3,plusAC(x4,x5)) plusAC(x3,x4) -> plusAC(x4,x3) plusAC(x3,plusAC(x4,x5)) -> plusAC(plusAC(x3,x4),x5) plusAC(x4,x3) -> plusAC(x3,x4) TRS: sum(x,y) -> S(int(x,y)) S(nil()) -> 0() S(cons(x,xs)) -> plusAC(x,S(xs)) plusAC(x,0()) -> x plusAC(x,s(y)) -> s(plusAC(x,y)) int(0(),0()) -> cons(0(),nil()) int(0(),s(y)) -> cons(0(),int(s(0()),s(y))) int(s(x),0()) -> nil() int(s(x),s(y)) -> intlist(int(x,y)) intlist(nil()) -> nil() intlist(cons(x,y)) -> cons(s(x),intlist(y)) S: plus{AC,#}(plusAC(x8,x9),x10) -> plus{AC,#}(x8,x9) plus{AC,#}(x8,plusAC(x9,x10)) -> plus{AC,#}(x9,x10) AC-DP unlabeling: Equations#: plusAC(plusAC(x3,x4),x5) -> plusAC(x3,plusAC(x4,x5)) plusAC(x3,x4) -> plusAC(x4,x3) plusAC(x3,plusAC(x4,x5)) -> plusAC(plusAC(x3,x4),x5) plusAC(x4,x3) -> plusAC(x3,x4) DPs: plusAC(x7,plusAC(x,s(y))) -> plusAC(x7,s(plusAC(x,y))) plusAC(x7,plusAC(x,s(y))) -> plusAC(x,y) plusAC(x6,plusAC(x,0())) -> plusAC(x6,x) plusAC(x,s(y)) -> plusAC(x,y) Equations: plusAC(plusAC(x3,x4),x5) -> plusAC(x3,plusAC(x4,x5)) plusAC(x3,x4) -> plusAC(x4,x3) plusAC(x3,plusAC(x4,x5)) -> plusAC(plusAC(x3,x4),x5) plusAC(x4,x3) -> plusAC(x3,x4) TRS: sum(x,y) -> S(int(x,y)) S(nil()) -> 0() S(cons(x,xs)) -> plusAC(x,S(xs)) plusAC(x,0()) -> x plusAC(x,s(y)) -> s(plusAC(x,y)) int(0(),0()) -> cons(0(),nil()) int(0(),s(y)) -> cons(0(),int(s(0()),s(y))) int(s(x),0()) -> nil() int(s(x),s(y)) -> intlist(int(x,y)) intlist(nil()) -> nil() intlist(cons(x,y)) -> cons(s(x),intlist(y)) S: plusAC(plusAC(x8,x9),x10) -> plusAC(x8,x9) plusAC(x8,plusAC(x9,x10)) -> plusAC(x9,x10) Usable Rule Processor: Equations#: plusAC(plusAC(x3,x4),x5) -> plusAC(x3,plusAC(x4,x5)) plusAC(x3,x4) -> plusAC(x4,x3) plusAC(x3,plusAC(x4,x5)) -> plusAC(plusAC(x3,x4),x5) plusAC(x4,x3) -> plusAC(x3,x4) DPs: plusAC(x7,plusAC(x,s(y))) -> plusAC(x7,s(plusAC(x,y))) plusAC(x7,plusAC(x,s(y))) -> plusAC(x,y) plusAC(x6,plusAC(x,0())) -> plusAC(x6,x) plusAC(x,s(y)) -> plusAC(x,y) Equations: plusAC(plusAC(x3,x4),x5) -> plusAC(x3,plusAC(x4,x5)) plusAC(x3,x4) -> plusAC(x4,x3) plusAC(x3,plusAC(x4,x5)) -> plusAC(plusAC(x3,x4),x5) plusAC(x4,x3) -> plusAC(x3,x4) TRS: plusAC(x,s(y)) -> s(plusAC(x,y)) plusAC(x,0()) -> x S: plusAC(plusAC(x8,x9),x10) -> plusAC(x8,x9) plusAC(x8,plusAC(x9,x10)) -> plusAC(x9,x10) AC-KBO Processor: argument filtering: pi(plusAC) = [0,1] pi(0) = [] pi(s) = [0] precedence: 0 ~ plusAC > s weight function: w0 = 1 w(plusAC) = 6 w(0) = 4 w(s) = 2 usable rules: plusAC(x,s(y)) -> s(plusAC(x,y)) plusAC(x,0()) -> x problem: Equations#: plusAC(plusAC(x3,x4),x5) -> plusAC(x3,plusAC(x4,x5)) plusAC(x3,x4) -> plusAC(x4,x3) plusAC(x3,plusAC(x4,x5)) -> plusAC(plusAC(x3,x4),x5) plusAC(x4,x3) -> plusAC(x3,x4) DPs: Equations: plusAC(plusAC(x3,x4),x5) -> plusAC(x3,plusAC(x4,x5)) plusAC(x3,x4) -> plusAC(x4,x3) plusAC(x3,plusAC(x4,x5)) -> plusAC(plusAC(x3,x4),x5) plusAC(x4,x3) -> plusAC(x3,x4) TRS: plusAC(x,s(y)) -> s(plusAC(x,y)) plusAC(x,0()) -> x S: plusAC(plusAC(x8,x9),x10) -> plusAC(x8,x9) plusAC(x8,plusAC(x9,x10)) -> plusAC(x9,x10) Qed Equations#: plus{AC,#}(plusAC(x3,x4),x5) -> plus{AC,#}(x3,plusAC(x4,x5)) plus{AC,#}(x3,x4) -> plus{AC,#}(x4,x3) plus{AC,#}(x3,plusAC(x4,x5)) -> plus{AC,#}(plusAC(x3,x4),x5) plus{AC,#}(x4,x3) -> plus{AC,#}(x3,x4) DPs: intlist#(cons(x,y)) -> intlist#(y) Equations: plusAC(plusAC(x3,x4),x5) -> plusAC(x3,plusAC(x4,x5)) plusAC(x3,x4) -> plusAC(x4,x3) plusAC(x3,plusAC(x4,x5)) -> plusAC(plusAC(x3,x4),x5) plusAC(x4,x3) -> plusAC(x3,x4) TRS: sum(x,y) -> S(int(x,y)) S(nil()) -> 0() S(cons(x,xs)) -> plusAC(x,S(xs)) plusAC(x,0()) -> x plusAC(x,s(y)) -> s(plusAC(x,y)) int(0(),0()) -> cons(0(),nil()) int(0(),s(y)) -> cons(0(),int(s(0()),s(y))) int(s(x),0()) -> nil() int(s(x),s(y)) -> intlist(int(x,y)) intlist(nil()) -> nil() intlist(cons(x,y)) -> cons(s(x),intlist(y)) S: plus{AC,#}(plusAC(x8,x9),x10) -> plus{AC,#}(x8,x9) plus{AC,#}(x8,plusAC(x9,x10)) -> plus{AC,#}(x9,x10) AC-DP unlabeling: Equations#: plusAC(plusAC(x3,x4),x5) -> plusAC(x3,plusAC(x4,x5)) plusAC(x3,x4) -> plusAC(x4,x3) plusAC(x3,plusAC(x4,x5)) -> plusAC(plusAC(x3,x4),x5) plusAC(x4,x3) -> plusAC(x3,x4) DPs: intlist#(cons(x,y)) -> intlist#(y) Equations: plusAC(plusAC(x3,x4),x5) -> plusAC(x3,plusAC(x4,x5)) plusAC(x3,x4) -> plusAC(x4,x3) plusAC(x3,plusAC(x4,x5)) -> plusAC(plusAC(x3,x4),x5) plusAC(x4,x3) -> plusAC(x3,x4) TRS: sum(x,y) -> S(int(x,y)) S(nil()) -> 0() S(cons(x,xs)) -> plusAC(x,S(xs)) plusAC(x,0()) -> x plusAC(x,s(y)) -> s(plusAC(x,y)) int(0(),0()) -> cons(0(),nil()) int(0(),s(y)) -> cons(0(),int(s(0()),s(y))) int(s(x),0()) -> nil() int(s(x),s(y)) -> intlist(int(x,y)) intlist(nil()) -> nil() intlist(cons(x,y)) -> cons(s(x),intlist(y)) S: plusAC(plusAC(x8,x9),x10) -> plusAC(x8,x9) plusAC(x8,plusAC(x9,x10)) -> plusAC(x9,x10) Usable Rule Processor: Equations#: plusAC(plusAC(x3,x4),x5) -> plusAC(x3,plusAC(x4,x5)) plusAC(x3,x4) -> plusAC(x4,x3) plusAC(x3,plusAC(x4,x5)) -> plusAC(plusAC(x3,x4),x5) plusAC(x4,x3) -> plusAC(x3,x4) DPs: intlist#(cons(x,y)) -> intlist#(y) Equations: plusAC(plusAC(x3,x4),x5) -> plusAC(x3,plusAC(x4,x5)) plusAC(x3,x4) -> plusAC(x4,x3) plusAC(x3,plusAC(x4,x5)) -> plusAC(plusAC(x3,x4),x5) plusAC(x4,x3) -> plusAC(x3,x4) TRS: S: plusAC(plusAC(x8,x9),x10) -> plusAC(x8,x9) plusAC(x8,plusAC(x9,x10)) -> plusAC(x9,x10) AC-KBO Processor: argument filtering: pi(cons) = [1] pi(intlist#) = 0 precedence: intlist# ~ cons weight function: w0 = 1 w(cons) = 2 w(intlist#) = 1 usable rules: problem: Equations#: plusAC(plusAC(x3,x4),x5) -> plusAC(x3,plusAC(x4,x5)) plusAC(x3,x4) -> plusAC(x4,x3) plusAC(x3,plusAC(x4,x5)) -> plusAC(plusAC(x3,x4),x5) plusAC(x4,x3) -> plusAC(x3,x4) DPs: Equations: plusAC(plusAC(x3,x4),x5) -> plusAC(x3,plusAC(x4,x5)) plusAC(x3,x4) -> plusAC(x4,x3) plusAC(x3,plusAC(x4,x5)) -> plusAC(plusAC(x3,x4),x5) plusAC(x4,x3) -> plusAC(x3,x4) TRS: S: plusAC(plusAC(x8,x9),x10) -> plusAC(x8,x9) plusAC(x8,plusAC(x9,x10)) -> plusAC(x9,x10) Qed