YES Time: 0.128 Problem: Equations: plusAC(plusAC(x2,x3),x4) -> plusAC(x2,plusAC(x3,x4)) plusAC(x2,x3) -> plusAC(x3,x2) plusAC(x2,plusAC(x3,x4)) -> plusAC(plusAC(x2,x3),x4) plusAC(x3,x2) -> plusAC(x2,x3) TRS: plusAC(x,0()) -> x plusAC(x,s(y)) -> s(plusAC(x,y)) bin(0(),s(y)) -> 0() bin(x,0()) -> s(0()) bin(s(x),s(y)) -> plusAC(bin(x,y),bin(x,s(y))) Proof: DP Processor: Equations#: plus{AC,#}(plusAC(x2,x3),x4) -> plus{AC,#}(x2,plusAC(x3,x4)) plus{AC,#}(x2,x3) -> plus{AC,#}(x3,x2) plus{AC,#}(x2,plusAC(x3,x4)) -> plus{AC,#}(plusAC(x2,x3),x4) plus{AC,#}(x3,x2) -> plus{AC,#}(x2,x3) DPs: plus{AC,#}(x,s(y)) -> plus{AC,#}(x,y) bin#(s(x),s(y)) -> bin#(x,s(y)) bin#(s(x),s(y)) -> bin#(x,y) bin#(s(x),s(y)) -> plus{AC,#}(bin(x,y),bin(x,s(y))) plus{AC,#}(x5,plusAC(x,0())) -> plus{AC,#}(x5,x) plus{AC,#}(x6,plusAC(x,s(y))) -> plus{AC,#}(x,y) plus{AC,#}(x6,plusAC(x,s(y))) -> plus{AC,#}(x6,s(plusAC(x,y))) Equations: plusAC(plusAC(x2,x3),x4) -> plusAC(x2,plusAC(x3,x4)) plusAC(x2,x3) -> plusAC(x3,x2) plusAC(x2,plusAC(x3,x4)) -> plusAC(plusAC(x2,x3),x4) plusAC(x3,x2) -> plusAC(x2,x3) TRS: plusAC(x,0()) -> x plusAC(x,s(y)) -> s(plusAC(x,y)) bin(0(),s(y)) -> 0() bin(x,0()) -> s(0()) bin(s(x),s(y)) -> plusAC(bin(x,y),bin(x,s(y))) S: plus{AC,#}(plusAC(x7,x8),x9) -> plus{AC,#}(x7,x8) plus{AC,#}(x7,plusAC(x8,x9)) -> plus{AC,#}(x8,x9) AC-EDG Processor: Equations#: plus{AC,#}(plusAC(x2,x3),x4) -> plus{AC,#}(x2,plusAC(x3,x4)) plus{AC,#}(x2,x3) -> plus{AC,#}(x3,x2) plus{AC,#}(x2,plusAC(x3,x4)) -> plus{AC,#}(plusAC(x2,x3),x4) plus{AC,#}(x3,x2) -> plus{AC,#}(x2,x3) DPs: plus{AC,#}(x,s(y)) -> plus{AC,#}(x,y) bin#(s(x),s(y)) -> bin#(x,s(y)) bin#(s(x),s(y)) -> bin#(x,y) bin#(s(x),s(y)) -> plus{AC,#}(bin(x,y),bin(x,s(y))) plus{AC,#}(x5,plusAC(x,0())) -> plus{AC,#}(x5,x) plus{AC,#}(x6,plusAC(x,s(y))) -> plus{AC,#}(x,y) plus{AC,#}(x6,plusAC(x,s(y))) -> plus{AC,#}(x6,s(plusAC(x,y))) Equations: plusAC(plusAC(x2,x3),x4) -> plusAC(x2,plusAC(x3,x4)) plusAC(x2,x3) -> plusAC(x3,x2) plusAC(x2,plusAC(x3,x4)) -> plusAC(plusAC(x2,x3),x4) plusAC(x3,x2) -> plusAC(x2,x3) TRS: plusAC(x,0()) -> x plusAC(x,s(y)) -> s(plusAC(x,y)) bin(0(),s(y)) -> 0() bin(x,0()) -> s(0()) bin(s(x),s(y)) -> plusAC(bin(x,y),bin(x,s(y))) S: plus{AC,#}(plusAC(x7,x8),x9) -> plus{AC,#}(x7,x8) plus{AC,#}(x7,plusAC(x8,x9)) -> plus{AC,#}(x8,x9) SCC Processor: #sccs: 2 #rules: 6 #arcs: 26/49 Equations#: plus{AC,#}(plusAC(x2,x3),x4) -> plus{AC,#}(x2,plusAC(x3,x4)) plus{AC,#}(x2,x3) -> plus{AC,#}(x3,x2) plus{AC,#}(x2,plusAC(x3,x4)) -> plus{AC,#}(plusAC(x2,x3),x4) plus{AC,#}(x3,x2) -> plus{AC,#}(x2,x3) DPs: bin#(s(x),s(y)) -> bin#(x,s(y)) bin#(s(x),s(y)) -> bin#(x,y) Equations: plusAC(plusAC(x2,x3),x4) -> plusAC(x2,plusAC(x3,x4)) plusAC(x2,x3) -> plusAC(x3,x2) plusAC(x2,plusAC(x3,x4)) -> plusAC(plusAC(x2,x3),x4) plusAC(x3,x2) -> plusAC(x2,x3) TRS: plusAC(x,0()) -> x plusAC(x,s(y)) -> s(plusAC(x,y)) bin(0(),s(y)) -> 0() bin(x,0()) -> s(0()) bin(s(x),s(y)) -> plusAC(bin(x,y),bin(x,s(y))) S: plus{AC,#}(plusAC(x7,x8),x9) -> plus{AC,#}(x7,x8) plus{AC,#}(x7,plusAC(x8,x9)) -> plus{AC,#}(x8,x9) AC-DP unlabeling: Equations#: plusAC(plusAC(x2,x3),x4) -> plusAC(x2,plusAC(x3,x4)) plusAC(x2,x3) -> plusAC(x3,x2) plusAC(x2,plusAC(x3,x4)) -> plusAC(plusAC(x2,x3),x4) plusAC(x3,x2) -> plusAC(x2,x3) DPs: bin#(s(x),s(y)) -> bin#(x,s(y)) bin#(s(x),s(y)) -> bin#(x,y) Equations: plusAC(plusAC(x2,x3),x4) -> plusAC(x2,plusAC(x3,x4)) plusAC(x2,x3) -> plusAC(x3,x2) plusAC(x2,plusAC(x3,x4)) -> plusAC(plusAC(x2,x3),x4) plusAC(x3,x2) -> plusAC(x2,x3) TRS: plusAC(x,0()) -> x plusAC(x,s(y)) -> s(plusAC(x,y)) bin(0(),s(y)) -> 0() bin(x,0()) -> s(0()) bin(s(x),s(y)) -> plusAC(bin(x,y),bin(x,s(y))) S: plusAC(plusAC(x7,x8),x9) -> plusAC(x7,x8) plusAC(x7,plusAC(x8,x9)) -> plusAC(x8,x9) Usable Rule Processor: Equations#: plusAC(plusAC(x2,x3),x4) -> plusAC(x2,plusAC(x3,x4)) plusAC(x2,x3) -> plusAC(x3,x2) plusAC(x2,plusAC(x3,x4)) -> plusAC(plusAC(x2,x3),x4) plusAC(x3,x2) -> plusAC(x2,x3) DPs: bin#(s(x),s(y)) -> bin#(x,s(y)) bin#(s(x),s(y)) -> bin#(x,y) Equations: plusAC(plusAC(x2,x3),x4) -> plusAC(x2,plusAC(x3,x4)) plusAC(x2,x3) -> plusAC(x3,x2) plusAC(x2,plusAC(x3,x4)) -> plusAC(plusAC(x2,x3),x4) plusAC(x3,x2) -> plusAC(x2,x3) TRS: S: plusAC(plusAC(x7,x8),x9) -> plusAC(x7,x8) plusAC(x7,plusAC(x8,x9)) -> plusAC(x8,x9) AC-KBO Processor: argument filtering: pi(s) = [0] pi(bin#) = [1] precedence: bin# ~ s weight function: w0 = 2 w(bin#) = 7 w(s) = 0 usable rules: problem: Equations#: plusAC(plusAC(x2,x3),x4) -> plusAC(x2,plusAC(x3,x4)) plusAC(x2,x3) -> plusAC(x3,x2) plusAC(x2,plusAC(x3,x4)) -> plusAC(plusAC(x2,x3),x4) plusAC(x3,x2) -> plusAC(x2,x3) DPs: bin#(s(x),s(y)) -> bin#(x,s(y)) Equations: plusAC(plusAC(x2,x3),x4) -> plusAC(x2,plusAC(x3,x4)) plusAC(x2,x3) -> plusAC(x3,x2) plusAC(x2,plusAC(x3,x4)) -> plusAC(plusAC(x2,x3),x4) plusAC(x3,x2) -> plusAC(x2,x3) TRS: S: plusAC(plusAC(x7,x8),x9) -> plusAC(x7,x8) plusAC(x7,plusAC(x8,x9)) -> plusAC(x8,x9) Restore Modifier: Equations#: plusAC(plusAC(x2,x3),x4) -> plusAC(x2,plusAC(x3,x4)) plusAC(x2,x3) -> plusAC(x3,x2) plusAC(x2,plusAC(x3,x4)) -> plusAC(plusAC(x2,x3),x4) plusAC(x3,x2) -> plusAC(x2,x3) DPs: bin#(s(x),s(y)) -> bin#(x,s(y)) Equations: plusAC(plusAC(x2,x3),x4) -> plusAC(x2,plusAC(x3,x4)) plusAC(x2,x3) -> plusAC(x3,x2) plusAC(x2,plusAC(x3,x4)) -> plusAC(plusAC(x2,x3),x4) plusAC(x3,x2) -> plusAC(x2,x3) TRS: S: plusAC(plusAC(x7,x8),x9) -> plusAC(x7,x8) plusAC(x7,plusAC(x8,x9)) -> plusAC(x8,x9) AC-DP unlabeling: Equations#: plusAC(plusAC(x2,x3),x4) -> plusAC(x2,plusAC(x3,x4)) plusAC(x2,x3) -> plusAC(x3,x2) plusAC(x2,plusAC(x3,x4)) -> plusAC(plusAC(x2,x3),x4) plusAC(x3,x2) -> plusAC(x2,x3) DPs: bin#(s(x),s(y)) -> bin#(x,s(y)) Equations: plusAC(plusAC(x2,x3),x4) -> plusAC(x2,plusAC(x3,x4)) plusAC(x2,x3) -> plusAC(x3,x2) plusAC(x2,plusAC(x3,x4)) -> plusAC(plusAC(x2,x3),x4) plusAC(x3,x2) -> plusAC(x2,x3) TRS: S: plusAC(plusAC(x7,x8),x9) -> plusAC(x7,x8) plusAC(x7,plusAC(x8,x9)) -> plusAC(x8,x9) AC-KBO Processor: argument filtering: pi(s) = [0] pi(bin#) = 0 precedence: bin# ~ s weight function: w0 = 4 w(bin#) = 4 w(s) = 0 usable rules: problem: Equations#: plusAC(plusAC(x2,x3),x4) -> plusAC(x2,plusAC(x3,x4)) plusAC(x2,x3) -> plusAC(x3,x2) plusAC(x2,plusAC(x3,x4)) -> plusAC(plusAC(x2,x3),x4) plusAC(x3,x2) -> plusAC(x2,x3) DPs: Equations: plusAC(plusAC(x2,x3),x4) -> plusAC(x2,plusAC(x3,x4)) plusAC(x2,x3) -> plusAC(x3,x2) plusAC(x2,plusAC(x3,x4)) -> plusAC(plusAC(x2,x3),x4) plusAC(x3,x2) -> plusAC(x2,x3) TRS: S: plusAC(plusAC(x7,x8),x9) -> plusAC(x7,x8) plusAC(x7,plusAC(x8,x9)) -> plusAC(x8,x9) Qed Equations#: plus{AC,#}(plusAC(x2,x3),x4) -> plus{AC,#}(x2,plusAC(x3,x4)) plus{AC,#}(x2,x3) -> plus{AC,#}(x3,x2) plus{AC,#}(x2,plusAC(x3,x4)) -> plus{AC,#}(plusAC(x2,x3),x4) plus{AC,#}(x3,x2) -> plus{AC,#}(x2,x3) DPs: plus{AC,#}(x6,plusAC(x,s(y))) -> plus{AC,#}(x6,s(plusAC(x,y))) plus{AC,#}(x6,plusAC(x,s(y))) -> plus{AC,#}(x,y) plus{AC,#}(x5,plusAC(x,0())) -> plus{AC,#}(x5,x) plus{AC,#}(x,s(y)) -> plus{AC,#}(x,y) Equations: plusAC(plusAC(x2,x3),x4) -> plusAC(x2,plusAC(x3,x4)) plusAC(x2,x3) -> plusAC(x3,x2) plusAC(x2,plusAC(x3,x4)) -> plusAC(plusAC(x2,x3),x4) plusAC(x3,x2) -> plusAC(x2,x3) TRS: plusAC(x,0()) -> x plusAC(x,s(y)) -> s(plusAC(x,y)) bin(0(),s(y)) -> 0() bin(x,0()) -> s(0()) bin(s(x),s(y)) -> plusAC(bin(x,y),bin(x,s(y))) S: plus{AC,#}(plusAC(x7,x8),x9) -> plus{AC,#}(x7,x8) plus{AC,#}(x7,plusAC(x8,x9)) -> plus{AC,#}(x8,x9) AC-DP unlabeling: Equations#: plusAC(plusAC(x2,x3),x4) -> plusAC(x2,plusAC(x3,x4)) plusAC(x2,x3) -> plusAC(x3,x2) plusAC(x2,plusAC(x3,x4)) -> plusAC(plusAC(x2,x3),x4) plusAC(x3,x2) -> plusAC(x2,x3) DPs: plusAC(x6,plusAC(x,s(y))) -> plusAC(x6,s(plusAC(x,y))) plusAC(x6,plusAC(x,s(y))) -> plusAC(x,y) plusAC(x5,plusAC(x,0())) -> plusAC(x5,x) plusAC(x,s(y)) -> plusAC(x,y) Equations: plusAC(plusAC(x2,x3),x4) -> plusAC(x2,plusAC(x3,x4)) plusAC(x2,x3) -> plusAC(x3,x2) plusAC(x2,plusAC(x3,x4)) -> plusAC(plusAC(x2,x3),x4) plusAC(x3,x2) -> plusAC(x2,x3) TRS: plusAC(x,0()) -> x plusAC(x,s(y)) -> s(plusAC(x,y)) bin(0(),s(y)) -> 0() bin(x,0()) -> s(0()) bin(s(x),s(y)) -> plusAC(bin(x,y),bin(x,s(y))) S: plusAC(plusAC(x7,x8),x9) -> plusAC(x7,x8) plusAC(x7,plusAC(x8,x9)) -> plusAC(x8,x9) Usable Rule Processor: Equations#: plusAC(plusAC(x2,x3),x4) -> plusAC(x2,plusAC(x3,x4)) plusAC(x2,x3) -> plusAC(x3,x2) plusAC(x2,plusAC(x3,x4)) -> plusAC(plusAC(x2,x3),x4) plusAC(x3,x2) -> plusAC(x2,x3) DPs: plusAC(x6,plusAC(x,s(y))) -> plusAC(x6,s(plusAC(x,y))) plusAC(x6,plusAC(x,s(y))) -> plusAC(x,y) plusAC(x5,plusAC(x,0())) -> plusAC(x5,x) plusAC(x,s(y)) -> plusAC(x,y) Equations: plusAC(plusAC(x2,x3),x4) -> plusAC(x2,plusAC(x3,x4)) plusAC(x2,x3) -> plusAC(x3,x2) plusAC(x2,plusAC(x3,x4)) -> plusAC(plusAC(x2,x3),x4) plusAC(x3,x2) -> plusAC(x2,x3) TRS: plusAC(x,s(y)) -> s(plusAC(x,y)) plusAC(x,0()) -> x S: plusAC(plusAC(x7,x8),x9) -> plusAC(x7,x8) plusAC(x7,plusAC(x8,x9)) -> plusAC(x8,x9) 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(x2,x3),x4) -> plusAC(x2,plusAC(x3,x4)) plusAC(x2,x3) -> plusAC(x3,x2) plusAC(x2,plusAC(x3,x4)) -> plusAC(plusAC(x2,x3),x4) plusAC(x3,x2) -> plusAC(x2,x3) DPs: Equations: plusAC(plusAC(x2,x3),x4) -> plusAC(x2,plusAC(x3,x4)) plusAC(x2,x3) -> plusAC(x3,x2) plusAC(x2,plusAC(x3,x4)) -> plusAC(plusAC(x2,x3),x4) plusAC(x3,x2) -> plusAC(x2,x3) TRS: plusAC(x,s(y)) -> s(plusAC(x,y)) plusAC(x,0()) -> x S: plusAC(plusAC(x7,x8),x9) -> plusAC(x7,x8) plusAC(x7,plusAC(x8,x9)) -> plusAC(x8,x9) Qed