YES Time: 0.625 Problem: Equations: plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6)) plusAC(x4,x5) -> plusAC(x5,x4) sumAC(sumAC(x4,x5),x6) -> sumAC(x4,sumAC(x5,x6)) sumAC(x4,x5) -> sumAC(x5,x4) plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6) plusAC(x5,x4) -> plusAC(x4,x5) sumAC(x4,sumAC(x5,x6)) -> sumAC(sumAC(x4,x5),x6) sumAC(x5,x4) -> sumAC(x4,x5) TRS: plusAC(x,0()) -> x plusAC(x,s(y)) -> s(plusAC(x,y)) sumAC(nil(),nil()) -> 0() sumAC(cons(x,xs),nil()) -> plusAC(x,sumAC(xs,nil())) sumAC(nil(),cons(x,xs)) -> plusAC(x,sumAC(nil(),xs)) sumAC(cons(x,xs),cons(y,ys)) -> plusAC(plusAC(x,y),sumAC(xs,ys)) Proof: DP Processor: Equations#: plus{AC,#}(plusAC(x4,x5),x6) -> plus{AC,#}(x4,plusAC(x5,x6)) plus{AC,#}(x4,x5) -> plus{AC,#}(x5,x4) sum{AC,#}(sumAC(x4,x5),x6) -> sum{AC,#}(x4,sumAC(x5,x6)) sum{AC,#}(x4,x5) -> sum{AC,#}(x5,x4) plus{AC,#}(x4,plusAC(x5,x6)) -> plus{AC,#}(plusAC(x4,x5),x6) plus{AC,#}(x5,x4) -> plus{AC,#}(x4,x5) sum{AC,#}(x4,sumAC(x5,x6)) -> sum{AC,#}(sumAC(x4,x5),x6) sum{AC,#}(x5,x4) -> sum{AC,#}(x4,x5) DPs: plus{AC,#}(x,s(y)) -> plus{AC,#}(x,y) sum{AC,#}(cons(x,xs),nil()) -> sum{AC,#}(xs,nil()) sum{AC,#}(cons(x,xs),nil()) -> plus{AC,#}(x,sumAC(xs,nil())) sum{AC,#}(nil(),cons(x,xs)) -> sum{AC,#}(nil(),xs) sum{AC,#}(nil(),cons(x,xs)) -> plus{AC,#}(x,sumAC(nil(),xs)) sum{AC,#}(cons(x,xs),cons(y,ys)) -> sum{AC,#}(xs,ys) sum{AC,#}(cons(x,xs),cons(y,ys)) -> plus{AC,#}(x,y) sum{AC,#}(cons(x,xs),cons(y,ys)) -> plus{AC,#}(plusAC(x,y),sumAC(xs,ys)) plus{AC,#}(x7,plusAC(x,0())) -> plus{AC,#}(x7,x) plus{AC,#}(x8,plusAC(x,s(y))) -> plus{AC,#}(x,y) plus{AC,#}(x8,plusAC(x,s(y))) -> plus{AC,#}(x8,s(plusAC(x,y))) sum{AC,#}(x9,sumAC(nil(),nil())) -> sum{AC,#}(x9,0()) sum{AC,#}(x10,sumAC(cons(x,xs),nil())) -> sum{AC,#}(xs,nil()) sum{AC,#}(x10,sumAC(cons(x,xs),nil())) -> plus{AC,#}(x,sumAC(xs,nil())) sum{AC,#}(x10,sumAC(cons(x,xs),nil())) -> sum{AC,#}(x10,plusAC(x,sumAC(xs,nil()))) sum{AC,#}(x11,sumAC(nil(),cons(x,xs))) -> sum{AC,#}(nil(),xs) sum{AC,#}(x11,sumAC(nil(),cons(x,xs))) -> plus{AC,#}(x,sumAC(nil(),xs)) sum{AC,#}(x11,sumAC(nil(),cons(x,xs))) -> sum{AC,#}(x11,plusAC(x,sumAC(nil(),xs))) sum{AC,#}(x12,sumAC(cons(x,xs),cons(y,ys))) -> sum{AC,#}(xs,ys) sum{AC,#}(x12,sumAC(cons(x,xs),cons(y,ys))) -> plus{AC,#}(x,y) sum{AC,#}(x12,sumAC(cons(x,xs),cons(y,ys))) -> plus{AC,#}(plusAC(x,y),sumAC(xs,ys)) sum{AC,#}(x12,sumAC(cons(x,xs),cons(y,ys))) -> sum{AC,#}(x12,plusAC(plusAC(x,y),sumAC(xs,ys))) Equations: plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6)) plusAC(x4,x5) -> plusAC(x5,x4) sumAC(sumAC(x4,x5),x6) -> sumAC(x4,sumAC(x5,x6)) sumAC(x4,x5) -> sumAC(x5,x4) plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6) plusAC(x5,x4) -> plusAC(x4,x5) sumAC(x4,sumAC(x5,x6)) -> sumAC(sumAC(x4,x5),x6) sumAC(x5,x4) -> sumAC(x4,x5) TRS: plusAC(x,0()) -> x plusAC(x,s(y)) -> s(plusAC(x,y)) sumAC(nil(),nil()) -> 0() sumAC(cons(x,xs),nil()) -> plusAC(x,sumAC(xs,nil())) sumAC(nil(),cons(x,xs)) -> plusAC(x,sumAC(nil(),xs)) sumAC(cons(x,xs),cons(y,ys)) -> plusAC(plusAC(x,y),sumAC(xs,ys)) S: plus{AC,#}(plusAC(x13,x14),x15) -> plus{AC,#}(x13,x14) plus{AC,#}(x13,plusAC(x14,x15)) -> plus{AC,#}(x14,x15) sum{AC,#}(sumAC(x13,x14),x15) -> sum{AC,#}(x13,x14) sum{AC,#}(x13,sumAC(x14,x15)) -> sum{AC,#}(x14,x15) AC-EDG Processor: Equations#: plus{AC,#}(plusAC(x4,x5),x6) -> plus{AC,#}(x4,plusAC(x5,x6)) plus{AC,#}(x4,x5) -> plus{AC,#}(x5,x4) sum{AC,#}(sumAC(x4,x5),x6) -> sum{AC,#}(x4,sumAC(x5,x6)) sum{AC,#}(x4,x5) -> sum{AC,#}(x5,x4) plus{AC,#}(x4,plusAC(x5,x6)) -> plus{AC,#}(plusAC(x4,x5),x6) plus{AC,#}(x5,x4) -> plus{AC,#}(x4,x5) sum{AC,#}(x4,sumAC(x5,x6)) -> sum{AC,#}(sumAC(x4,x5),x6) sum{AC,#}(x5,x4) -> sum{AC,#}(x4,x5) DPs: plus{AC,#}(x,s(y)) -> plus{AC,#}(x,y) sum{AC,#}(cons(x,xs),nil()) -> sum{AC,#}(xs,nil()) sum{AC,#}(cons(x,xs),nil()) -> plus{AC,#}(x,sumAC(xs,nil())) sum{AC,#}(nil(),cons(x,xs)) -> sum{AC,#}(nil(),xs) sum{AC,#}(nil(),cons(x,xs)) -> plus{AC,#}(x,sumAC(nil(),xs)) sum{AC,#}(cons(x,xs),cons(y,ys)) -> sum{AC,#}(xs,ys) sum{AC,#}(cons(x,xs),cons(y,ys)) -> plus{AC,#}(x,y) sum{AC,#}(cons(x,xs),cons(y,ys)) -> plus{AC,#}(plusAC(x,y),sumAC(xs,ys)) plus{AC,#}(x7,plusAC(x,0())) -> plus{AC,#}(x7,x) plus{AC,#}(x8,plusAC(x,s(y))) -> plus{AC,#}(x,y) plus{AC,#}(x8,plusAC(x,s(y))) -> plus{AC,#}(x8,s(plusAC(x,y))) sum{AC,#}(x9,sumAC(nil(),nil())) -> sum{AC,#}(x9,0()) sum{AC,#}(x10,sumAC(cons(x,xs),nil())) -> sum{AC,#}(xs,nil()) sum{AC,#}(x10,sumAC(cons(x,xs),nil())) -> plus{AC,#}(x,sumAC(xs,nil())) sum{AC,#}(x10,sumAC(cons(x,xs),nil())) -> sum{AC,#}(x10,plusAC(x,sumAC(xs,nil()))) sum{AC,#}(x11,sumAC(nil(),cons(x,xs))) -> sum{AC,#}(nil(),xs) sum{AC,#}(x11,sumAC(nil(),cons(x,xs))) -> plus{AC,#}(x,sumAC(nil(),xs)) sum{AC,#}(x11,sumAC(nil(),cons(x,xs))) -> sum{AC,#}(x11,plusAC(x,sumAC(nil(),xs))) sum{AC,#}(x12,sumAC(cons(x,xs),cons(y,ys))) -> sum{AC,#}(xs,ys) sum{AC,#}(x12,sumAC(cons(x,xs),cons(y,ys))) -> plus{AC,#}(x,y) sum{AC,#}(x12,sumAC(cons(x,xs),cons(y,ys))) -> plus{AC,#}(plusAC(x,y),sumAC(xs,ys)) sum{AC,#}(x12,sumAC(cons(x,xs),cons(y,ys))) -> sum{AC,#}(x12,plusAC(plusAC(x,y),sumAC(xs,ys))) Equations: plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6)) plusAC(x4,x5) -> plusAC(x5,x4) sumAC(sumAC(x4,x5),x6) -> sumAC(x4,sumAC(x5,x6)) sumAC(x4,x5) -> sumAC(x5,x4) plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6) plusAC(x5,x4) -> plusAC(x4,x5) sumAC(x4,sumAC(x5,x6)) -> sumAC(sumAC(x4,x5),x6) sumAC(x5,x4) -> sumAC(x4,x5) TRS: plusAC(x,0()) -> x plusAC(x,s(y)) -> s(plusAC(x,y)) sumAC(nil(),nil()) -> 0() sumAC(cons(x,xs),nil()) -> plusAC(x,sumAC(xs,nil())) sumAC(nil(),cons(x,xs)) -> plusAC(x,sumAC(nil(),xs)) sumAC(cons(x,xs),cons(y,ys)) -> plusAC(plusAC(x,y),sumAC(xs,ys)) S: plus{AC,#}(plusAC(x13,x14),x15) -> plus{AC,#}(x13,x14) plus{AC,#}(x13,plusAC(x14,x15)) -> plus{AC,#}(x14,x15) sum{AC,#}(sumAC(x13,x14),x15) -> sum{AC,#}(x13,x14) sum{AC,#}(x13,sumAC(x14,x15)) -> sum{AC,#}(x14,x15) SCC Processor: #sccs: 2 #rules: 14 #arcs: 228/484 Equations#: plus{AC,#}(plusAC(x4,x5),x6) -> plus{AC,#}(x4,plusAC(x5,x6)) plus{AC,#}(x4,x5) -> plus{AC,#}(x5,x4) sum{AC,#}(sumAC(x4,x5),x6) -> sum{AC,#}(x4,sumAC(x5,x6)) sum{AC,#}(x4,x5) -> sum{AC,#}(x5,x4) plus{AC,#}(x4,plusAC(x5,x6)) -> plus{AC,#}(plusAC(x4,x5),x6) plus{AC,#}(x5,x4) -> plus{AC,#}(x4,x5) sum{AC,#}(x4,sumAC(x5,x6)) -> sum{AC,#}(sumAC(x4,x5),x6) sum{AC,#}(x5,x4) -> sum{AC,#}(x4,x5) DPs: sum{AC,#}(cons(x,xs),cons(y,ys)) -> sum{AC,#}(xs,ys) sum{AC,#}(x12,sumAC(cons(x,xs),cons(y,ys))) -> sum{AC,#}(x12,plusAC(plusAC(x,y),sumAC(xs,ys))) sum{AC,#}(x12,sumAC(cons(x,xs),cons(y,ys))) -> sum{AC,#}(xs,ys) sum{AC,#}(x11,sumAC(nil(),cons(x,xs))) -> sum{AC,#}(x11,plusAC(x,sumAC(nil(),xs))) sum{AC,#}(x11,sumAC(nil(),cons(x,xs))) -> sum{AC,#}(nil(),xs) sum{AC,#}(x10,sumAC(cons(x,xs),nil())) -> sum{AC,#}(x10,plusAC(x,sumAC(xs,nil()))) sum{AC,#}(x10,sumAC(cons(x,xs),nil())) -> sum{AC,#}(xs,nil()) sum{AC,#}(x9,sumAC(nil(),nil())) -> sum{AC,#}(x9,0()) sum{AC,#}(nil(),cons(x,xs)) -> sum{AC,#}(nil(),xs) sum{AC,#}(cons(x,xs),nil()) -> sum{AC,#}(xs,nil()) Equations: plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6)) plusAC(x4,x5) -> plusAC(x5,x4) sumAC(sumAC(x4,x5),x6) -> sumAC(x4,sumAC(x5,x6)) sumAC(x4,x5) -> sumAC(x5,x4) plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6) plusAC(x5,x4) -> plusAC(x4,x5) sumAC(x4,sumAC(x5,x6)) -> sumAC(sumAC(x4,x5),x6) sumAC(x5,x4) -> sumAC(x4,x5) TRS: plusAC(x,0()) -> x plusAC(x,s(y)) -> s(plusAC(x,y)) sumAC(nil(),nil()) -> 0() sumAC(cons(x,xs),nil()) -> plusAC(x,sumAC(xs,nil())) sumAC(nil(),cons(x,xs)) -> plusAC(x,sumAC(nil(),xs)) sumAC(cons(x,xs),cons(y,ys)) -> plusAC(plusAC(x,y),sumAC(xs,ys)) S: plus{AC,#}(plusAC(x13,x14),x15) -> plus{AC,#}(x13,x14) plus{AC,#}(x13,plusAC(x14,x15)) -> plus{AC,#}(x14,x15) sum{AC,#}(sumAC(x13,x14),x15) -> sum{AC,#}(x13,x14) sum{AC,#}(x13,sumAC(x14,x15)) -> sum{AC,#}(x14,x15) AC-DP unlabeling: Equations#: plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6)) plusAC(x4,x5) -> plusAC(x5,x4) sumAC(sumAC(x4,x5),x6) -> sumAC(x4,sumAC(x5,x6)) sumAC(x4,x5) -> sumAC(x5,x4) plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6) plusAC(x5,x4) -> plusAC(x4,x5) sumAC(x4,sumAC(x5,x6)) -> sumAC(sumAC(x4,x5),x6) sumAC(x5,x4) -> sumAC(x4,x5) DPs: sumAC(cons(x,xs),cons(y,ys)) -> sumAC(xs,ys) sumAC(x12,sumAC(cons(x,xs),cons(y,ys))) -> sumAC(x12,plusAC(plusAC(x,y),sumAC(xs,ys))) sumAC(x12,sumAC(cons(x,xs),cons(y,ys))) -> sumAC(xs,ys) sumAC(x11,sumAC(nil(),cons(x,xs))) -> sumAC(x11,plusAC(x,sumAC(nil(),xs))) sumAC(x11,sumAC(nil(),cons(x,xs))) -> sumAC(nil(),xs) sumAC(x10,sumAC(cons(x,xs),nil())) -> sumAC(x10,plusAC(x,sumAC(xs,nil()))) sumAC(x10,sumAC(cons(x,xs),nil())) -> sumAC(xs,nil()) sumAC(x9,sumAC(nil(),nil())) -> sumAC(x9,0()) sumAC(nil(),cons(x,xs)) -> sumAC(nil(),xs) sumAC(cons(x,xs),nil()) -> sumAC(xs,nil()) Equations: plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6)) plusAC(x4,x5) -> plusAC(x5,x4) sumAC(sumAC(x4,x5),x6) -> sumAC(x4,sumAC(x5,x6)) sumAC(x4,x5) -> sumAC(x5,x4) plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6) plusAC(x5,x4) -> plusAC(x4,x5) sumAC(x4,sumAC(x5,x6)) -> sumAC(sumAC(x4,x5),x6) sumAC(x5,x4) -> sumAC(x4,x5) TRS: plusAC(x,0()) -> x plusAC(x,s(y)) -> s(plusAC(x,y)) sumAC(nil(),nil()) -> 0() sumAC(cons(x,xs),nil()) -> plusAC(x,sumAC(xs,nil())) sumAC(nil(),cons(x,xs)) -> plusAC(x,sumAC(nil(),xs)) sumAC(cons(x,xs),cons(y,ys)) -> plusAC(plusAC(x,y),sumAC(xs,ys)) S: plusAC(plusAC(x13,x14),x15) -> plusAC(x13,x14) plusAC(x13,plusAC(x14,x15)) -> plusAC(x14,x15) sumAC(sumAC(x13,x14),x15) -> sumAC(x13,x14) sumAC(x13,sumAC(x14,x15)) -> sumAC(x14,x15) AC-KBO Processor: argument filtering: pi(plusAC) = [0,1] pi(sumAC) = [0,1] pi(0) = [] pi(s) = [] pi(nil) = [] pi(cons) = [0,1] precedence: cons ~ nil ~ s ~ 0 ~ sumAC ~ plusAC weight function: w0 = 1 w(nil) = 6 w(0) = 4 w(cons) = w(s) = 1 w(sumAC) = w(plusAC) = 0 usable rules: plusAC(x,0()) -> x plusAC(x,s(y)) -> s(plusAC(x,y)) sumAC(nil(),nil()) -> 0() sumAC(cons(x,xs),nil()) -> plusAC(x,sumAC(xs,nil())) sumAC(nil(),cons(x,xs)) -> plusAC(x,sumAC(nil(),xs)) sumAC(cons(x,xs),cons(y,ys)) -> plusAC(plusAC(x,y),sumAC(xs,ys)) problem: Equations#: plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6)) plusAC(x4,x5) -> plusAC(x5,x4) sumAC(sumAC(x4,x5),x6) -> sumAC(x4,sumAC(x5,x6)) sumAC(x4,x5) -> sumAC(x5,x4) plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6) plusAC(x5,x4) -> plusAC(x4,x5) sumAC(x4,sumAC(x5,x6)) -> sumAC(sumAC(x4,x5),x6) sumAC(x5,x4) -> sumAC(x4,x5) DPs: Equations: plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6)) plusAC(x4,x5) -> plusAC(x5,x4) sumAC(sumAC(x4,x5),x6) -> sumAC(x4,sumAC(x5,x6)) sumAC(x4,x5) -> sumAC(x5,x4) plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6) plusAC(x5,x4) -> plusAC(x4,x5) sumAC(x4,sumAC(x5,x6)) -> sumAC(sumAC(x4,x5),x6) sumAC(x5,x4) -> sumAC(x4,x5) TRS: plusAC(x,0()) -> x plusAC(x,s(y)) -> s(plusAC(x,y)) sumAC(nil(),nil()) -> 0() sumAC(cons(x,xs),nil()) -> plusAC(x,sumAC(xs,nil())) sumAC(nil(),cons(x,xs)) -> plusAC(x,sumAC(nil(),xs)) sumAC(cons(x,xs),cons(y,ys)) -> plusAC(plusAC(x,y),sumAC(xs,ys)) S: plusAC(plusAC(x13,x14),x15) -> plusAC(x13,x14) plusAC(x13,plusAC(x14,x15)) -> plusAC(x14,x15) sumAC(sumAC(x13,x14),x15) -> sumAC(x13,x14) sumAC(x13,sumAC(x14,x15)) -> sumAC(x14,x15) Qed Equations#: plus{AC,#}(plusAC(x4,x5),x6) -> plus{AC,#}(x4,plusAC(x5,x6)) plus{AC,#}(x4,x5) -> plus{AC,#}(x5,x4) sum{AC,#}(sumAC(x4,x5),x6) -> sum{AC,#}(x4,sumAC(x5,x6)) sum{AC,#}(x4,x5) -> sum{AC,#}(x5,x4) plus{AC,#}(x4,plusAC(x5,x6)) -> plus{AC,#}(plusAC(x4,x5),x6) plus{AC,#}(x5,x4) -> plus{AC,#}(x4,x5) sum{AC,#}(x4,sumAC(x5,x6)) -> sum{AC,#}(sumAC(x4,x5),x6) sum{AC,#}(x5,x4) -> sum{AC,#}(x4,x5) DPs: plus{AC,#}(x8,plusAC(x,s(y))) -> plus{AC,#}(x8,s(plusAC(x,y))) plus{AC,#}(x8,plusAC(x,s(y))) -> plus{AC,#}(x,y) plus{AC,#}(x7,plusAC(x,0())) -> plus{AC,#}(x7,x) plus{AC,#}(x,s(y)) -> plus{AC,#}(x,y) Equations: plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6)) plusAC(x4,x5) -> plusAC(x5,x4) sumAC(sumAC(x4,x5),x6) -> sumAC(x4,sumAC(x5,x6)) sumAC(x4,x5) -> sumAC(x5,x4) plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6) plusAC(x5,x4) -> plusAC(x4,x5) sumAC(x4,sumAC(x5,x6)) -> sumAC(sumAC(x4,x5),x6) sumAC(x5,x4) -> sumAC(x4,x5) TRS: plusAC(x,0()) -> x plusAC(x,s(y)) -> s(plusAC(x,y)) sumAC(nil(),nil()) -> 0() sumAC(cons(x,xs),nil()) -> plusAC(x,sumAC(xs,nil())) sumAC(nil(),cons(x,xs)) -> plusAC(x,sumAC(nil(),xs)) sumAC(cons(x,xs),cons(y,ys)) -> plusAC(plusAC(x,y),sumAC(xs,ys)) S: plus{AC,#}(plusAC(x13,x14),x15) -> plus{AC,#}(x13,x14) plus{AC,#}(x13,plusAC(x14,x15)) -> plus{AC,#}(x14,x15) sum{AC,#}(sumAC(x13,x14),x15) -> sum{AC,#}(x13,x14) sum{AC,#}(x13,sumAC(x14,x15)) -> sum{AC,#}(x14,x15) AC-DP unlabeling: Equations#: plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6)) plusAC(x4,x5) -> plusAC(x5,x4) sumAC(sumAC(x4,x5),x6) -> sumAC(x4,sumAC(x5,x6)) sumAC(x4,x5) -> sumAC(x5,x4) plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6) plusAC(x5,x4) -> plusAC(x4,x5) sumAC(x4,sumAC(x5,x6)) -> sumAC(sumAC(x4,x5),x6) sumAC(x5,x4) -> sumAC(x4,x5) DPs: plusAC(x8,plusAC(x,s(y))) -> plusAC(x8,s(plusAC(x,y))) plusAC(x8,plusAC(x,s(y))) -> plusAC(x,y) plusAC(x7,plusAC(x,0())) -> plusAC(x7,x) plusAC(x,s(y)) -> plusAC(x,y) Equations: plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6)) plusAC(x4,x5) -> plusAC(x5,x4) sumAC(sumAC(x4,x5),x6) -> sumAC(x4,sumAC(x5,x6)) sumAC(x4,x5) -> sumAC(x5,x4) plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6) plusAC(x5,x4) -> plusAC(x4,x5) sumAC(x4,sumAC(x5,x6)) -> sumAC(sumAC(x4,x5),x6) sumAC(x5,x4) -> sumAC(x4,x5) TRS: plusAC(x,0()) -> x plusAC(x,s(y)) -> s(plusAC(x,y)) sumAC(nil(),nil()) -> 0() sumAC(cons(x,xs),nil()) -> plusAC(x,sumAC(xs,nil())) sumAC(nil(),cons(x,xs)) -> plusAC(x,sumAC(nil(),xs)) sumAC(cons(x,xs),cons(y,ys)) -> plusAC(plusAC(x,y),sumAC(xs,ys)) S: plusAC(plusAC(x13,x14),x15) -> plusAC(x13,x14) plusAC(x13,plusAC(x14,x15)) -> plusAC(x14,x15) sumAC(sumAC(x13,x14),x15) -> sumAC(x13,x14) sumAC(x13,sumAC(x14,x15)) -> sumAC(x14,x15) Usable Rule Processor: Equations#: plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6)) plusAC(x4,x5) -> plusAC(x5,x4) sumAC(sumAC(x4,x5),x6) -> sumAC(x4,sumAC(x5,x6)) sumAC(x4,x5) -> sumAC(x5,x4) plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6) plusAC(x5,x4) -> plusAC(x4,x5) sumAC(x4,sumAC(x5,x6)) -> sumAC(sumAC(x4,x5),x6) sumAC(x5,x4) -> sumAC(x4,x5) DPs: plusAC(x8,plusAC(x,s(y))) -> plusAC(x8,s(plusAC(x,y))) plusAC(x8,plusAC(x,s(y))) -> plusAC(x,y) plusAC(x7,plusAC(x,0())) -> plusAC(x7,x) plusAC(x,s(y)) -> plusAC(x,y) Equations: plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6)) plusAC(x4,x5) -> plusAC(x5,x4) sumAC(sumAC(x4,x5),x6) -> sumAC(x4,sumAC(x5,x6)) sumAC(x4,x5) -> sumAC(x5,x4) plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6) plusAC(x5,x4) -> plusAC(x4,x5) sumAC(x4,sumAC(x5,x6)) -> sumAC(sumAC(x4,x5),x6) sumAC(x5,x4) -> sumAC(x4,x5) TRS: plusAC(x,s(y)) -> s(plusAC(x,y)) plusAC(x,0()) -> x S: plusAC(plusAC(x13,x14),x15) -> plusAC(x13,x14) plusAC(x13,plusAC(x14,x15)) -> plusAC(x14,x15) sumAC(sumAC(x13,x14),x15) -> sumAC(x13,x14) sumAC(x13,sumAC(x14,x15)) -> sumAC(x14,x15) AC-KBO Processor: argument filtering: pi(plusAC) = [0,1] pi(0) = [] pi(s) = [0] precedence: 0 ~ plusAC > s weight function: w0 = 4 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(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6)) plusAC(x4,x5) -> plusAC(x5,x4) sumAC(sumAC(x4,x5),x6) -> sumAC(x4,sumAC(x5,x6)) sumAC(x4,x5) -> sumAC(x5,x4) plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6) plusAC(x5,x4) -> plusAC(x4,x5) sumAC(x4,sumAC(x5,x6)) -> sumAC(sumAC(x4,x5),x6) sumAC(x5,x4) -> sumAC(x4,x5) DPs: Equations: plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6)) plusAC(x4,x5) -> plusAC(x5,x4) sumAC(sumAC(x4,x5),x6) -> sumAC(x4,sumAC(x5,x6)) sumAC(x4,x5) -> sumAC(x5,x4) plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6) plusAC(x5,x4) -> plusAC(x4,x5) sumAC(x4,sumAC(x5,x6)) -> sumAC(sumAC(x4,x5),x6) sumAC(x5,x4) -> sumAC(x4,x5) TRS: plusAC(x,s(y)) -> s(plusAC(x,y)) plusAC(x,0()) -> x S: plusAC(plusAC(x13,x14),x15) -> plusAC(x13,x14) plusAC(x13,plusAC(x14,x15)) -> plusAC(x14,x15) sumAC(sumAC(x13,x14),x15) -> sumAC(x13,x14) sumAC(x13,sumAC(x14,x15)) -> sumAC(x14,x15) Qed