YES Time: 0.629 Problem: Equations: +AC(+AC(x3,x4),x5) -> +AC(x3,+AC(x4,x5)) +AC(x3,x4) -> +AC(x4,x3) *AC(*AC(x3,x4),x5) -> *AC(x3,*AC(x4,x5)) *AC(x3,x4) -> *AC(x4,x3) UAC(UAC(x3,x4),x5) -> UAC(x3,UAC(x4,x5)) UAC(x3,x4) -> UAC(x4,x3) +AC(x3,+AC(x4,x5)) -> +AC(+AC(x3,x4),x5) +AC(x4,x3) -> +AC(x3,x4) *AC(x3,*AC(x4,x5)) -> *AC(*AC(x3,x4),x5) *AC(x4,x3) -> *AC(x3,x4) UAC(x3,UAC(x4,x5)) -> UAC(UAC(x3,x4),x5) UAC(x4,x3) -> UAC(x3,x4) TRS: +AC(0(),x) -> x +AC(s(x),s(y)) -> s(s(+AC(x,y))) *AC(0(),x) -> 0() *AC(s(x),s(y)) -> s(+AC(+AC(x,y),*AC(x,y))) UAC(empty(),b) -> b sum(empty()) -> 0() sum(singl(x)) -> x sum(UAC(x,y)) -> +AC(sum(x),sum(y)) prod(empty()) -> s(0()) prod(singl(x)) -> x prod(UAC(x,y)) -> *AC(prod(x),prod(y)) Proof: DP Processor: Equations#: +{AC,#}(+AC(x3,x4),x5) -> +{AC,#}(x3,+AC(x4,x5)) +{AC,#}(x3,x4) -> +{AC,#}(x4,x3) *{AC,#}(*AC(x3,x4),x5) -> *{AC,#}(x3,*AC(x4,x5)) *{AC,#}(x3,x4) -> *{AC,#}(x4,x3) U{AC,#}(UAC(x3,x4),x5) -> U{AC,#}(x3,UAC(x4,x5)) U{AC,#}(x3,x4) -> U{AC,#}(x4,x3) +{AC,#}(x3,+AC(x4,x5)) -> +{AC,#}(+AC(x3,x4),x5) +{AC,#}(x4,x3) -> +{AC,#}(x3,x4) *{AC,#}(x3,*AC(x4,x5)) -> *{AC,#}(*AC(x3,x4),x5) *{AC,#}(x4,x3) -> *{AC,#}(x3,x4) U{AC,#}(x3,UAC(x4,x5)) -> U{AC,#}(UAC(x3,x4),x5) U{AC,#}(x4,x3) -> U{AC,#}(x3,x4) DPs: +{AC,#}(s(x),s(y)) -> +{AC,#}(x,y) *{AC,#}(s(x),s(y)) -> *{AC,#}(x,y) *{AC,#}(s(x),s(y)) -> +{AC,#}(x,y) *{AC,#}(s(x),s(y)) -> +{AC,#}(+AC(x,y),*AC(x,y)) sum#(UAC(x,y)) -> sum#(y) sum#(UAC(x,y)) -> sum#(x) sum#(UAC(x,y)) -> +{AC,#}(sum(x),sum(y)) prod#(UAC(x,y)) -> prod#(y) prod#(UAC(x,y)) -> prod#(x) prod#(UAC(x,y)) -> *{AC,#}(prod(x),prod(y)) +{AC,#}(x6,+AC(0(),x)) -> +{AC,#}(x6,x) +{AC,#}(x7,+AC(s(x),s(y))) -> +{AC,#}(x,y) +{AC,#}(x7,+AC(s(x),s(y))) -> +{AC,#}(x7,s(s(+AC(x,y)))) *{AC,#}(x8,*AC(0(),x)) -> *{AC,#}(x8,0()) *{AC,#}(x9,*AC(s(x),s(y))) -> *{AC,#}(x,y) *{AC,#}(x9,*AC(s(x),s(y))) -> +{AC,#}(x,y) *{AC,#}(x9,*AC(s(x),s(y))) -> +{AC,#}(+AC(x,y),*AC(x,y)) *{AC,#}(x9,*AC(s(x),s(y))) -> *{AC,#}(x9,s(+AC(+AC(x,y),*AC(x,y)))) U{AC,#}(x10,UAC(empty(),b)) -> U{AC,#}(x10,b) Equations: +AC(+AC(x3,x4),x5) -> +AC(x3,+AC(x4,x5)) +AC(x3,x4) -> +AC(x4,x3) *AC(*AC(x3,x4),x5) -> *AC(x3,*AC(x4,x5)) *AC(x3,x4) -> *AC(x4,x3) UAC(UAC(x3,x4),x5) -> UAC(x3,UAC(x4,x5)) UAC(x3,x4) -> UAC(x4,x3) +AC(x3,+AC(x4,x5)) -> +AC(+AC(x3,x4),x5) +AC(x4,x3) -> +AC(x3,x4) *AC(x3,*AC(x4,x5)) -> *AC(*AC(x3,x4),x5) *AC(x4,x3) -> *AC(x3,x4) UAC(x3,UAC(x4,x5)) -> UAC(UAC(x3,x4),x5) UAC(x4,x3) -> UAC(x3,x4) TRS: +AC(0(),x) -> x +AC(s(x),s(y)) -> s(s(+AC(x,y))) *AC(0(),x) -> 0() *AC(s(x),s(y)) -> s(+AC(+AC(x,y),*AC(x,y))) UAC(empty(),b) -> b sum(empty()) -> 0() sum(singl(x)) -> x sum(UAC(x,y)) -> +AC(sum(x),sum(y)) prod(empty()) -> s(0()) prod(singl(x)) -> x prod(UAC(x,y)) -> *AC(prod(x),prod(y)) S: +{AC,#}(+AC(x11,x12),x13) -> +{AC,#}(x11,x12) +{AC,#}(x11,+AC(x12,x13)) -> +{AC,#}(x12,x13) *{AC,#}(*AC(x11,x12),x13) -> *{AC,#}(x11,x12) *{AC,#}(x11,*AC(x12,x13)) -> *{AC,#}(x12,x13) U{AC,#}(UAC(x11,x12),x13) -> U{AC,#}(x11,x12) U{AC,#}(x11,UAC(x12,x13)) -> U{AC,#}(x12,x13) AC-EDG Processor: Equations#: +{AC,#}(+AC(x3,x4),x5) -> +{AC,#}(x3,+AC(x4,x5)) +{AC,#}(x3,x4) -> +{AC,#}(x4,x3) *{AC,#}(*AC(x3,x4),x5) -> *{AC,#}(x3,*AC(x4,x5)) *{AC,#}(x3,x4) -> *{AC,#}(x4,x3) U{AC,#}(UAC(x3,x4),x5) -> U{AC,#}(x3,UAC(x4,x5)) U{AC,#}(x3,x4) -> U{AC,#}(x4,x3) +{AC,#}(x3,+AC(x4,x5)) -> +{AC,#}(+AC(x3,x4),x5) +{AC,#}(x4,x3) -> +{AC,#}(x3,x4) *{AC,#}(x3,*AC(x4,x5)) -> *{AC,#}(*AC(x3,x4),x5) *{AC,#}(x4,x3) -> *{AC,#}(x3,x4) U{AC,#}(x3,UAC(x4,x5)) -> U{AC,#}(UAC(x3,x4),x5) U{AC,#}(x4,x3) -> U{AC,#}(x3,x4) DPs: +{AC,#}(s(x),s(y)) -> +{AC,#}(x,y) *{AC,#}(s(x),s(y)) -> *{AC,#}(x,y) *{AC,#}(s(x),s(y)) -> +{AC,#}(x,y) *{AC,#}(s(x),s(y)) -> +{AC,#}(+AC(x,y),*AC(x,y)) sum#(UAC(x,y)) -> sum#(y) sum#(UAC(x,y)) -> sum#(x) sum#(UAC(x,y)) -> +{AC,#}(sum(x),sum(y)) prod#(UAC(x,y)) -> prod#(y) prod#(UAC(x,y)) -> prod#(x) prod#(UAC(x,y)) -> *{AC,#}(prod(x),prod(y)) +{AC,#}(x6,+AC(0(),x)) -> +{AC,#}(x6,x) +{AC,#}(x7,+AC(s(x),s(y))) -> +{AC,#}(x,y) +{AC,#}(x7,+AC(s(x),s(y))) -> +{AC,#}(x7,s(s(+AC(x,y)))) *{AC,#}(x8,*AC(0(),x)) -> *{AC,#}(x8,0()) *{AC,#}(x9,*AC(s(x),s(y))) -> *{AC,#}(x,y) *{AC,#}(x9,*AC(s(x),s(y))) -> +{AC,#}(x,y) *{AC,#}(x9,*AC(s(x),s(y))) -> +{AC,#}(+AC(x,y),*AC(x,y)) *{AC,#}(x9,*AC(s(x),s(y))) -> *{AC,#}(x9,s(+AC(+AC(x,y),*AC(x,y)))) U{AC,#}(x10,UAC(empty(),b)) -> U{AC,#}(x10,b) Equations: +AC(+AC(x3,x4),x5) -> +AC(x3,+AC(x4,x5)) +AC(x3,x4) -> +AC(x4,x3) *AC(*AC(x3,x4),x5) -> *AC(x3,*AC(x4,x5)) *AC(x3,x4) -> *AC(x4,x3) UAC(UAC(x3,x4),x5) -> UAC(x3,UAC(x4,x5)) UAC(x3,x4) -> UAC(x4,x3) +AC(x3,+AC(x4,x5)) -> +AC(+AC(x3,x4),x5) +AC(x4,x3) -> +AC(x3,x4) *AC(x3,*AC(x4,x5)) -> *AC(*AC(x3,x4),x5) *AC(x4,x3) -> *AC(x3,x4) UAC(x3,UAC(x4,x5)) -> UAC(UAC(x3,x4),x5) UAC(x4,x3) -> UAC(x3,x4) TRS: +AC(0(),x) -> x +AC(s(x),s(y)) -> s(s(+AC(x,y))) *AC(0(),x) -> 0() *AC(s(x),s(y)) -> s(+AC(+AC(x,y),*AC(x,y))) UAC(empty(),b) -> b sum(empty()) -> 0() sum(singl(x)) -> x sum(UAC(x,y)) -> +AC(sum(x),sum(y)) prod(empty()) -> s(0()) prod(singl(x)) -> x prod(UAC(x,y)) -> *AC(prod(x),prod(y)) S: +{AC,#}(+AC(x11,x12),x13) -> +{AC,#}(x11,x12) +{AC,#}(x11,+AC(x12,x13)) -> +{AC,#}(x12,x13) *{AC,#}(*AC(x11,x12),x13) -> *{AC,#}(x11,x12) *{AC,#}(x11,*AC(x12,x13)) -> *{AC,#}(x12,x13) U{AC,#}(UAC(x11,x12),x13) -> U{AC,#}(x11,x12) U{AC,#}(x11,UAC(x12,x13)) -> U{AC,#}(x12,x13) SCC Processor: #sccs: 5 #rules: 13 #arcs: 89/361 Equations#: +{AC,#}(+AC(x3,x4),x5) -> +{AC,#}(x3,+AC(x4,x5)) +{AC,#}(x3,x4) -> +{AC,#}(x4,x3) *{AC,#}(*AC(x3,x4),x5) -> *{AC,#}(x3,*AC(x4,x5)) *{AC,#}(x3,x4) -> *{AC,#}(x4,x3) U{AC,#}(UAC(x3,x4),x5) -> U{AC,#}(x3,UAC(x4,x5)) U{AC,#}(x3,x4) -> U{AC,#}(x4,x3) +{AC,#}(x3,+AC(x4,x5)) -> +{AC,#}(+AC(x3,x4),x5) +{AC,#}(x4,x3) -> +{AC,#}(x3,x4) *{AC,#}(x3,*AC(x4,x5)) -> *{AC,#}(*AC(x3,x4),x5) *{AC,#}(x4,x3) -> *{AC,#}(x3,x4) U{AC,#}(x3,UAC(x4,x5)) -> U{AC,#}(UAC(x3,x4),x5) U{AC,#}(x4,x3) -> U{AC,#}(x3,x4) DPs: U{AC,#}(x10,UAC(empty(),b)) -> U{AC,#}(x10,b) Equations: +AC(+AC(x3,x4),x5) -> +AC(x3,+AC(x4,x5)) +AC(x3,x4) -> +AC(x4,x3) *AC(*AC(x3,x4),x5) -> *AC(x3,*AC(x4,x5)) *AC(x3,x4) -> *AC(x4,x3) UAC(UAC(x3,x4),x5) -> UAC(x3,UAC(x4,x5)) UAC(x3,x4) -> UAC(x4,x3) +AC(x3,+AC(x4,x5)) -> +AC(+AC(x3,x4),x5) +AC(x4,x3) -> +AC(x3,x4) *AC(x3,*AC(x4,x5)) -> *AC(*AC(x3,x4),x5) *AC(x4,x3) -> *AC(x3,x4) UAC(x3,UAC(x4,x5)) -> UAC(UAC(x3,x4),x5) UAC(x4,x3) -> UAC(x3,x4) TRS: +AC(0(),x) -> x +AC(s(x),s(y)) -> s(s(+AC(x,y))) *AC(0(),x) -> 0() *AC(s(x),s(y)) -> s(+AC(+AC(x,y),*AC(x,y))) UAC(empty(),b) -> b sum(empty()) -> 0() sum(singl(x)) -> x sum(UAC(x,y)) -> +AC(sum(x),sum(y)) prod(empty()) -> s(0()) prod(singl(x)) -> x prod(UAC(x,y)) -> *AC(prod(x),prod(y)) S: +{AC,#}(+AC(x11,x12),x13) -> +{AC,#}(x11,x12) +{AC,#}(x11,+AC(x12,x13)) -> +{AC,#}(x12,x13) *{AC,#}(*AC(x11,x12),x13) -> *{AC,#}(x11,x12) *{AC,#}(x11,*AC(x12,x13)) -> *{AC,#}(x12,x13) U{AC,#}(UAC(x11,x12),x13) -> U{AC,#}(x11,x12) U{AC,#}(x11,UAC(x12,x13)) -> U{AC,#}(x12,x13) AC-DP unlabeling: Equations#: +AC(+AC(x3,x4),x5) -> +AC(x3,+AC(x4,x5)) +AC(x3,x4) -> +AC(x4,x3) *AC(*AC(x3,x4),x5) -> *AC(x3,*AC(x4,x5)) *AC(x3,x4) -> *AC(x4,x3) UAC(UAC(x3,x4),x5) -> UAC(x3,UAC(x4,x5)) UAC(x3,x4) -> UAC(x4,x3) +AC(x3,+AC(x4,x5)) -> +AC(+AC(x3,x4),x5) +AC(x4,x3) -> +AC(x3,x4) *AC(x3,*AC(x4,x5)) -> *AC(*AC(x3,x4),x5) *AC(x4,x3) -> *AC(x3,x4) UAC(x3,UAC(x4,x5)) -> UAC(UAC(x3,x4),x5) UAC(x4,x3) -> UAC(x3,x4) DPs: UAC(x10,UAC(empty(),b)) -> UAC(x10,b) Equations: +AC(+AC(x3,x4),x5) -> +AC(x3,+AC(x4,x5)) +AC(x3,x4) -> +AC(x4,x3) *AC(*AC(x3,x4),x5) -> *AC(x3,*AC(x4,x5)) *AC(x3,x4) -> *AC(x4,x3) UAC(UAC(x3,x4),x5) -> UAC(x3,UAC(x4,x5)) UAC(x3,x4) -> UAC(x4,x3) +AC(x3,+AC(x4,x5)) -> +AC(+AC(x3,x4),x5) +AC(x4,x3) -> +AC(x3,x4) *AC(x3,*AC(x4,x5)) -> *AC(*AC(x3,x4),x5) *AC(x4,x3) -> *AC(x3,x4) UAC(x3,UAC(x4,x5)) -> UAC(UAC(x3,x4),x5) UAC(x4,x3) -> UAC(x3,x4) TRS: +AC(0(),x) -> x +AC(s(x),s(y)) -> s(s(+AC(x,y))) *AC(0(),x) -> 0() *AC(s(x),s(y)) -> s(+AC(+AC(x,y),*AC(x,y))) UAC(empty(),b) -> b sum(empty()) -> 0() sum(singl(x)) -> x sum(UAC(x,y)) -> +AC(sum(x),sum(y)) prod(empty()) -> s(0()) prod(singl(x)) -> x prod(UAC(x,y)) -> *AC(prod(x),prod(y)) S: +AC(+AC(x11,x12),x13) -> +AC(x11,x12) +AC(x11,+AC(x12,x13)) -> +AC(x12,x13) *AC(*AC(x11,x12),x13) -> *AC(x11,x12) *AC(x11,*AC(x12,x13)) -> *AC(x12,x13) UAC(UAC(x11,x12),x13) -> UAC(x11,x12) UAC(x11,UAC(x12,x13)) -> UAC(x12,x13) Usable Rule Processor: Equations#: +AC(+AC(x3,x4),x5) -> +AC(x3,+AC(x4,x5)) +AC(x3,x4) -> +AC(x4,x3) *AC(*AC(x3,x4),x5) -> *AC(x3,*AC(x4,x5)) *AC(x3,x4) -> *AC(x4,x3) UAC(UAC(x3,x4),x5) -> UAC(x3,UAC(x4,x5)) UAC(x3,x4) -> UAC(x4,x3) +AC(x3,+AC(x4,x5)) -> +AC(+AC(x3,x4),x5) +AC(x4,x3) -> +AC(x3,x4) *AC(x3,*AC(x4,x5)) -> *AC(*AC(x3,x4),x5) *AC(x4,x3) -> *AC(x3,x4) UAC(x3,UAC(x4,x5)) -> UAC(UAC(x3,x4),x5) UAC(x4,x3) -> UAC(x3,x4) DPs: UAC(x10,UAC(empty(),b)) -> UAC(x10,b) Equations: +AC(+AC(x3,x4),x5) -> +AC(x3,+AC(x4,x5)) +AC(x3,x4) -> +AC(x4,x3) *AC(*AC(x3,x4),x5) -> *AC(x3,*AC(x4,x5)) *AC(x3,x4) -> *AC(x4,x3) UAC(UAC(x3,x4),x5) -> UAC(x3,UAC(x4,x5)) UAC(x3,x4) -> UAC(x4,x3) +AC(x3,+AC(x4,x5)) -> +AC(+AC(x3,x4),x5) +AC(x4,x3) -> +AC(x3,x4) *AC(x3,*AC(x4,x5)) -> *AC(*AC(x3,x4),x5) *AC(x4,x3) -> *AC(x3,x4) UAC(x3,UAC(x4,x5)) -> UAC(UAC(x3,x4),x5) UAC(x4,x3) -> UAC(x3,x4) TRS: UAC(empty(),b) -> b S: +AC(+AC(x11,x12),x13) -> +AC(x11,x12) +AC(x11,+AC(x12,x13)) -> +AC(x12,x13) *AC(*AC(x11,x12),x13) -> *AC(x11,x12) *AC(x11,*AC(x12,x13)) -> *AC(x12,x13) UAC(UAC(x11,x12),x13) -> UAC(x11,x12) UAC(x11,UAC(x12,x13)) -> UAC(x12,x13) AC-RPO Processor: argument filtering: pi(UAC) = [0,1] pi(*AC) = [] pi(+AC) = [] pi(empty) = [] precedence: empty > +AC > *AC > UAC status: problem: Equations#: +AC(+AC(x3,x4),x5) -> +AC(x3,+AC(x4,x5)) +AC(x3,x4) -> +AC(x4,x3) *AC(*AC(x3,x4),x5) -> *AC(x3,*AC(x4,x5)) *AC(x3,x4) -> *AC(x4,x3) UAC(UAC(x3,x4),x5) -> UAC(x3,UAC(x4,x5)) UAC(x3,x4) -> UAC(x4,x3) +AC(x3,+AC(x4,x5)) -> +AC(+AC(x3,x4),x5) +AC(x4,x3) -> +AC(x3,x4) *AC(x3,*AC(x4,x5)) -> *AC(*AC(x3,x4),x5) *AC(x4,x3) -> *AC(x3,x4) UAC(x3,UAC(x4,x5)) -> UAC(UAC(x3,x4),x5) UAC(x4,x3) -> UAC(x3,x4) DPs: Equations: +AC(+AC(x3,x4),x5) -> +AC(x3,+AC(x4,x5)) +AC(x3,x4) -> +AC(x4,x3) *AC(*AC(x3,x4),x5) -> *AC(x3,*AC(x4,x5)) *AC(x3,x4) -> *AC(x4,x3) UAC(UAC(x3,x4),x5) -> UAC(x3,UAC(x4,x5)) UAC(x3,x4) -> UAC(x4,x3) +AC(x3,+AC(x4,x5)) -> +AC(+AC(x3,x4),x5) +AC(x4,x3) -> +AC(x3,x4) *AC(x3,*AC(x4,x5)) -> *AC(*AC(x3,x4),x5) *AC(x4,x3) -> *AC(x3,x4) UAC(x3,UAC(x4,x5)) -> UAC(UAC(x3,x4),x5) UAC(x4,x3) -> UAC(x3,x4) TRS: UAC(empty(),b) -> b S: +AC(+AC(x11,x12),x13) -> +AC(x11,x12) +AC(x11,+AC(x12,x13)) -> +AC(x12,x13) *AC(*AC(x11,x12),x13) -> *AC(x11,x12) *AC(x11,*AC(x12,x13)) -> *AC(x12,x13) UAC(UAC(x11,x12),x13) -> UAC(x11,x12) UAC(x11,UAC(x12,x13)) -> UAC(x12,x13) Qed Equations#: +{AC,#}(+AC(x3,x4),x5) -> +{AC,#}(x3,+AC(x4,x5)) +{AC,#}(x3,x4) -> +{AC,#}(x4,x3) *{AC,#}(*AC(x3,x4),x5) -> *{AC,#}(x3,*AC(x4,x5)) *{AC,#}(x3,x4) -> *{AC,#}(x4,x3) U{AC,#}(UAC(x3,x4),x5) -> U{AC,#}(x3,UAC(x4,x5)) U{AC,#}(x3,x4) -> U{AC,#}(x4,x3) +{AC,#}(x3,+AC(x4,x5)) -> +{AC,#}(+AC(x3,x4),x5) +{AC,#}(x4,x3) -> +{AC,#}(x3,x4) *{AC,#}(x3,*AC(x4,x5)) -> *{AC,#}(*AC(x3,x4),x5) *{AC,#}(x4,x3) -> *{AC,#}(x3,x4) U{AC,#}(x3,UAC(x4,x5)) -> U{AC,#}(UAC(x3,x4),x5) U{AC,#}(x4,x3) -> U{AC,#}(x3,x4) DPs: sum#(UAC(x,y)) -> sum#(x) sum#(UAC(x,y)) -> sum#(y) Equations: +AC(+AC(x3,x4),x5) -> +AC(x3,+AC(x4,x5)) +AC(x3,x4) -> +AC(x4,x3) *AC(*AC(x3,x4),x5) -> *AC(x3,*AC(x4,x5)) *AC(x3,x4) -> *AC(x4,x3) UAC(UAC(x3,x4),x5) -> UAC(x3,UAC(x4,x5)) UAC(x3,x4) -> UAC(x4,x3) +AC(x3,+AC(x4,x5)) -> +AC(+AC(x3,x4),x5) +AC(x4,x3) -> +AC(x3,x4) *AC(x3,*AC(x4,x5)) -> *AC(*AC(x3,x4),x5) *AC(x4,x3) -> *AC(x3,x4) UAC(x3,UAC(x4,x5)) -> UAC(UAC(x3,x4),x5) UAC(x4,x3) -> UAC(x3,x4) TRS: +AC(0(),x) -> x +AC(s(x),s(y)) -> s(s(+AC(x,y))) *AC(0(),x) -> 0() *AC(s(x),s(y)) -> s(+AC(+AC(x,y),*AC(x,y))) UAC(empty(),b) -> b sum(empty()) -> 0() sum(singl(x)) -> x sum(UAC(x,y)) -> +AC(sum(x),sum(y)) prod(empty()) -> s(0()) prod(singl(x)) -> x prod(UAC(x,y)) -> *AC(prod(x),prod(y)) S: +{AC,#}(+AC(x11,x12),x13) -> +{AC,#}(x11,x12) +{AC,#}(x11,+AC(x12,x13)) -> +{AC,#}(x12,x13) *{AC,#}(*AC(x11,x12),x13) -> *{AC,#}(x11,x12) *{AC,#}(x11,*AC(x12,x13)) -> *{AC,#}(x12,x13) U{AC,#}(UAC(x11,x12),x13) -> U{AC,#}(x11,x12) U{AC,#}(x11,UAC(x12,x13)) -> U{AC,#}(x12,x13) AC-DP unlabeling: Equations#: +AC(+AC(x3,x4),x5) -> +AC(x3,+AC(x4,x5)) +AC(x3,x4) -> +AC(x4,x3) *AC(*AC(x3,x4),x5) -> *AC(x3,*AC(x4,x5)) *AC(x3,x4) -> *AC(x4,x3) UAC(UAC(x3,x4),x5) -> UAC(x3,UAC(x4,x5)) UAC(x3,x4) -> UAC(x4,x3) +AC(x3,+AC(x4,x5)) -> +AC(+AC(x3,x4),x5) +AC(x4,x3) -> +AC(x3,x4) *AC(x3,*AC(x4,x5)) -> *AC(*AC(x3,x4),x5) *AC(x4,x3) -> *AC(x3,x4) UAC(x3,UAC(x4,x5)) -> UAC(UAC(x3,x4),x5) UAC(x4,x3) -> UAC(x3,x4) DPs: sum#(UAC(x,y)) -> sum#(x) sum#(UAC(x,y)) -> sum#(y) Equations: +AC(+AC(x3,x4),x5) -> +AC(x3,+AC(x4,x5)) +AC(x3,x4) -> +AC(x4,x3) *AC(*AC(x3,x4),x5) -> *AC(x3,*AC(x4,x5)) *AC(x3,x4) -> *AC(x4,x3) UAC(UAC(x3,x4),x5) -> UAC(x3,UAC(x4,x5)) UAC(x3,x4) -> UAC(x4,x3) +AC(x3,+AC(x4,x5)) -> +AC(+AC(x3,x4),x5) +AC(x4,x3) -> +AC(x3,x4) *AC(x3,*AC(x4,x5)) -> *AC(*AC(x3,x4),x5) *AC(x4,x3) -> *AC(x3,x4) UAC(x3,UAC(x4,x5)) -> UAC(UAC(x3,x4),x5) UAC(x4,x3) -> UAC(x3,x4) TRS: +AC(0(),x) -> x +AC(s(x),s(y)) -> s(s(+AC(x,y))) *AC(0(),x) -> 0() *AC(s(x),s(y)) -> s(+AC(+AC(x,y),*AC(x,y))) UAC(empty(),b) -> b sum(empty()) -> 0() sum(singl(x)) -> x sum(UAC(x,y)) -> +AC(sum(x),sum(y)) prod(empty()) -> s(0()) prod(singl(x)) -> x prod(UAC(x,y)) -> *AC(prod(x),prod(y)) S: +AC(+AC(x11,x12),x13) -> +AC(x11,x12) +AC(x11,+AC(x12,x13)) -> +AC(x12,x13) *AC(*AC(x11,x12),x13) -> *AC(x11,x12) *AC(x11,*AC(x12,x13)) -> *AC(x12,x13) UAC(UAC(x11,x12),x13) -> UAC(x11,x12) UAC(x11,UAC(x12,x13)) -> UAC(x12,x13) Usable Rule Processor: Equations#: +AC(+AC(x3,x4),x5) -> +AC(x3,+AC(x4,x5)) +AC(x3,x4) -> +AC(x4,x3) *AC(*AC(x3,x4),x5) -> *AC(x3,*AC(x4,x5)) *AC(x3,x4) -> *AC(x4,x3) UAC(UAC(x3,x4),x5) -> UAC(x3,UAC(x4,x5)) UAC(x3,x4) -> UAC(x4,x3) +AC(x3,+AC(x4,x5)) -> +AC(+AC(x3,x4),x5) +AC(x4,x3) -> +AC(x3,x4) *AC(x3,*AC(x4,x5)) -> *AC(*AC(x3,x4),x5) *AC(x4,x3) -> *AC(x3,x4) UAC(x3,UAC(x4,x5)) -> UAC(UAC(x3,x4),x5) UAC(x4,x3) -> UAC(x3,x4) DPs: sum#(UAC(x,y)) -> sum#(x) sum#(UAC(x,y)) -> sum#(y) Equations: +AC(+AC(x3,x4),x5) -> +AC(x3,+AC(x4,x5)) +AC(x3,x4) -> +AC(x4,x3) *AC(*AC(x3,x4),x5) -> *AC(x3,*AC(x4,x5)) *AC(x3,x4) -> *AC(x4,x3) UAC(UAC(x3,x4),x5) -> UAC(x3,UAC(x4,x5)) UAC(x3,x4) -> UAC(x4,x3) +AC(x3,+AC(x4,x5)) -> +AC(+AC(x3,x4),x5) +AC(x4,x3) -> +AC(x3,x4) *AC(x3,*AC(x4,x5)) -> *AC(*AC(x3,x4),x5) *AC(x4,x3) -> *AC(x3,x4) UAC(x3,UAC(x4,x5)) -> UAC(UAC(x3,x4),x5) UAC(x4,x3) -> UAC(x3,x4) TRS: S: +AC(+AC(x11,x12),x13) -> +AC(x11,x12) +AC(x11,+AC(x12,x13)) -> +AC(x12,x13) *AC(*AC(x11,x12),x13) -> *AC(x11,x12) *AC(x11,*AC(x12,x13)) -> *AC(x12,x13) UAC(UAC(x11,x12),x13) -> UAC(x11,x12) UAC(x11,UAC(x12,x13)) -> UAC(x12,x13) AC-RPO Processor: argument filtering: pi(UAC) = [0,1] pi(*AC) = [0,1] pi(+AC) = [0,1] pi(sum#) = [0] precedence: +AC > UAC > sum# > *AC status: problem: Equations#: +AC(+AC(x3,x4),x5) -> +AC(x3,+AC(x4,x5)) +AC(x3,x4) -> +AC(x4,x3) *AC(*AC(x3,x4),x5) -> *AC(x3,*AC(x4,x5)) *AC(x3,x4) -> *AC(x4,x3) UAC(UAC(x3,x4),x5) -> UAC(x3,UAC(x4,x5)) UAC(x3,x4) -> UAC(x4,x3) +AC(x3,+AC(x4,x5)) -> +AC(+AC(x3,x4),x5) +AC(x4,x3) -> +AC(x3,x4) *AC(x3,*AC(x4,x5)) -> *AC(*AC(x3,x4),x5) *AC(x4,x3) -> *AC(x3,x4) UAC(x3,UAC(x4,x5)) -> UAC(UAC(x3,x4),x5) UAC(x4,x3) -> UAC(x3,x4) DPs: Equations: +AC(+AC(x3,x4),x5) -> +AC(x3,+AC(x4,x5)) +AC(x3,x4) -> +AC(x4,x3) *AC(*AC(x3,x4),x5) -> *AC(x3,*AC(x4,x5)) *AC(x3,x4) -> *AC(x4,x3) UAC(UAC(x3,x4),x5) -> UAC(x3,UAC(x4,x5)) UAC(x3,x4) -> UAC(x4,x3) +AC(x3,+AC(x4,x5)) -> +AC(+AC(x3,x4),x5) +AC(x4,x3) -> +AC(x3,x4) *AC(x3,*AC(x4,x5)) -> *AC(*AC(x3,x4),x5) *AC(x4,x3) -> *AC(x3,x4) UAC(x3,UAC(x4,x5)) -> UAC(UAC(x3,x4),x5) UAC(x4,x3) -> UAC(x3,x4) TRS: S: +AC(+AC(x11,x12),x13) -> +AC(x11,x12) +AC(x11,+AC(x12,x13)) -> +AC(x12,x13) *AC(*AC(x11,x12),x13) -> *AC(x11,x12) *AC(x11,*AC(x12,x13)) -> *AC(x12,x13) UAC(UAC(x11,x12),x13) -> UAC(x11,x12) UAC(x11,UAC(x12,x13)) -> UAC(x12,x13) Qed Equations#: +{AC,#}(+AC(x3,x4),x5) -> +{AC,#}(x3,+AC(x4,x5)) +{AC,#}(x3,x4) -> +{AC,#}(x4,x3) *{AC,#}(*AC(x3,x4),x5) -> *{AC,#}(x3,*AC(x4,x5)) *{AC,#}(x3,x4) -> *{AC,#}(x4,x3) U{AC,#}(UAC(x3,x4),x5) -> U{AC,#}(x3,UAC(x4,x5)) U{AC,#}(x3,x4) -> U{AC,#}(x4,x3) +{AC,#}(x3,+AC(x4,x5)) -> +{AC,#}(+AC(x3,x4),x5) +{AC,#}(x4,x3) -> +{AC,#}(x3,x4) *{AC,#}(x3,*AC(x4,x5)) -> *{AC,#}(*AC(x3,x4),x5) *{AC,#}(x4,x3) -> *{AC,#}(x3,x4) U{AC,#}(x3,UAC(x4,x5)) -> U{AC,#}(UAC(x3,x4),x5) U{AC,#}(x4,x3) -> U{AC,#}(x3,x4) DPs: prod#(UAC(x,y)) -> prod#(x) prod#(UAC(x,y)) -> prod#(y) Equations: +AC(+AC(x3,x4),x5) -> +AC(x3,+AC(x4,x5)) +AC(x3,x4) -> +AC(x4,x3) *AC(*AC(x3,x4),x5) -> *AC(x3,*AC(x4,x5)) *AC(x3,x4) -> *AC(x4,x3) UAC(UAC(x3,x4),x5) -> UAC(x3,UAC(x4,x5)) UAC(x3,x4) -> UAC(x4,x3) +AC(x3,+AC(x4,x5)) -> +AC(+AC(x3,x4),x5) +AC(x4,x3) -> +AC(x3,x4) *AC(x3,*AC(x4,x5)) -> *AC(*AC(x3,x4),x5) *AC(x4,x3) -> *AC(x3,x4) UAC(x3,UAC(x4,x5)) -> UAC(UAC(x3,x4),x5) UAC(x4,x3) -> UAC(x3,x4) TRS: +AC(0(),x) -> x +AC(s(x),s(y)) -> s(s(+AC(x,y))) *AC(0(),x) -> 0() *AC(s(x),s(y)) -> s(+AC(+AC(x,y),*AC(x,y))) UAC(empty(),b) -> b sum(empty()) -> 0() sum(singl(x)) -> x sum(UAC(x,y)) -> +AC(sum(x),sum(y)) prod(empty()) -> s(0()) prod(singl(x)) -> x prod(UAC(x,y)) -> *AC(prod(x),prod(y)) S: +{AC,#}(+AC(x11,x12),x13) -> +{AC,#}(x11,x12) +{AC,#}(x11,+AC(x12,x13)) -> +{AC,#}(x12,x13) *{AC,#}(*AC(x11,x12),x13) -> *{AC,#}(x11,x12) *{AC,#}(x11,*AC(x12,x13)) -> *{AC,#}(x12,x13) U{AC,#}(UAC(x11,x12),x13) -> U{AC,#}(x11,x12) U{AC,#}(x11,UAC(x12,x13)) -> U{AC,#}(x12,x13) AC-DP unlabeling: Equations#: +AC(+AC(x3,x4),x5) -> +AC(x3,+AC(x4,x5)) +AC(x3,x4) -> +AC(x4,x3) *AC(*AC(x3,x4),x5) -> *AC(x3,*AC(x4,x5)) *AC(x3,x4) -> *AC(x4,x3) UAC(UAC(x3,x4),x5) -> UAC(x3,UAC(x4,x5)) UAC(x3,x4) -> UAC(x4,x3) +AC(x3,+AC(x4,x5)) -> +AC(+AC(x3,x4),x5) +AC(x4,x3) -> +AC(x3,x4) *AC(x3,*AC(x4,x5)) -> *AC(*AC(x3,x4),x5) *AC(x4,x3) -> *AC(x3,x4) UAC(x3,UAC(x4,x5)) -> UAC(UAC(x3,x4),x5) UAC(x4,x3) -> UAC(x3,x4) DPs: prod#(UAC(x,y)) -> prod#(x) prod#(UAC(x,y)) -> prod#(y) Equations: +AC(+AC(x3,x4),x5) -> +AC(x3,+AC(x4,x5)) +AC(x3,x4) -> +AC(x4,x3) *AC(*AC(x3,x4),x5) -> *AC(x3,*AC(x4,x5)) *AC(x3,x4) -> *AC(x4,x3) UAC(UAC(x3,x4),x5) -> UAC(x3,UAC(x4,x5)) UAC(x3,x4) -> UAC(x4,x3) +AC(x3,+AC(x4,x5)) -> +AC(+AC(x3,x4),x5) +AC(x4,x3) -> +AC(x3,x4) *AC(x3,*AC(x4,x5)) -> *AC(*AC(x3,x4),x5) *AC(x4,x3) -> *AC(x3,x4) UAC(x3,UAC(x4,x5)) -> UAC(UAC(x3,x4),x5) UAC(x4,x3) -> UAC(x3,x4) TRS: +AC(0(),x) -> x +AC(s(x),s(y)) -> s(s(+AC(x,y))) *AC(0(),x) -> 0() *AC(s(x),s(y)) -> s(+AC(+AC(x,y),*AC(x,y))) UAC(empty(),b) -> b sum(empty()) -> 0() sum(singl(x)) -> x sum(UAC(x,y)) -> +AC(sum(x),sum(y)) prod(empty()) -> s(0()) prod(singl(x)) -> x prod(UAC(x,y)) -> *AC(prod(x),prod(y)) S: +AC(+AC(x11,x12),x13) -> +AC(x11,x12) +AC(x11,+AC(x12,x13)) -> +AC(x12,x13) *AC(*AC(x11,x12),x13) -> *AC(x11,x12) *AC(x11,*AC(x12,x13)) -> *AC(x12,x13) UAC(UAC(x11,x12),x13) -> UAC(x11,x12) UAC(x11,UAC(x12,x13)) -> UAC(x12,x13) Usable Rule Processor: Equations#: +AC(+AC(x3,x4),x5) -> +AC(x3,+AC(x4,x5)) +AC(x3,x4) -> +AC(x4,x3) *AC(*AC(x3,x4),x5) -> *AC(x3,*AC(x4,x5)) *AC(x3,x4) -> *AC(x4,x3) UAC(UAC(x3,x4),x5) -> UAC(x3,UAC(x4,x5)) UAC(x3,x4) -> UAC(x4,x3) +AC(x3,+AC(x4,x5)) -> +AC(+AC(x3,x4),x5) +AC(x4,x3) -> +AC(x3,x4) *AC(x3,*AC(x4,x5)) -> *AC(*AC(x3,x4),x5) *AC(x4,x3) -> *AC(x3,x4) UAC(x3,UAC(x4,x5)) -> UAC(UAC(x3,x4),x5) UAC(x4,x3) -> UAC(x3,x4) DPs: prod#(UAC(x,y)) -> prod#(x) prod#(UAC(x,y)) -> prod#(y) Equations: +AC(+AC(x3,x4),x5) -> +AC(x3,+AC(x4,x5)) +AC(x3,x4) -> +AC(x4,x3) *AC(*AC(x3,x4),x5) -> *AC(x3,*AC(x4,x5)) *AC(x3,x4) -> *AC(x4,x3) UAC(UAC(x3,x4),x5) -> UAC(x3,UAC(x4,x5)) UAC(x3,x4) -> UAC(x4,x3) +AC(x3,+AC(x4,x5)) -> +AC(+AC(x3,x4),x5) +AC(x4,x3) -> +AC(x3,x4) *AC(x3,*AC(x4,x5)) -> *AC(*AC(x3,x4),x5) *AC(x4,x3) -> *AC(x3,x4) UAC(x3,UAC(x4,x5)) -> UAC(UAC(x3,x4),x5) UAC(x4,x3) -> UAC(x3,x4) TRS: S: +AC(+AC(x11,x12),x13) -> +AC(x11,x12) +AC(x11,+AC(x12,x13)) -> +AC(x12,x13) *AC(*AC(x11,x12),x13) -> *AC(x11,x12) *AC(x11,*AC(x12,x13)) -> *AC(x12,x13) UAC(UAC(x11,x12),x13) -> UAC(x11,x12) UAC(x11,UAC(x12,x13)) -> UAC(x12,x13) AC-RPO Processor: argument filtering: pi(UAC) = [0,1] pi(*AC) = [0,1] pi(+AC) = [0,1] pi(prod#) = [0] precedence: +AC > UAC > prod# > *AC status: problem: Equations#: +AC(+AC(x3,x4),x5) -> +AC(x3,+AC(x4,x5)) +AC(x3,x4) -> +AC(x4,x3) *AC(*AC(x3,x4),x5) -> *AC(x3,*AC(x4,x5)) *AC(x3,x4) -> *AC(x4,x3) UAC(UAC(x3,x4),x5) -> UAC(x3,UAC(x4,x5)) UAC(x3,x4) -> UAC(x4,x3) +AC(x3,+AC(x4,x5)) -> +AC(+AC(x3,x4),x5) +AC(x4,x3) -> +AC(x3,x4) *AC(x3,*AC(x4,x5)) -> *AC(*AC(x3,x4),x5) *AC(x4,x3) -> *AC(x3,x4) UAC(x3,UAC(x4,x5)) -> UAC(UAC(x3,x4),x5) UAC(x4,x3) -> UAC(x3,x4) DPs: Equations: +AC(+AC(x3,x4),x5) -> +AC(x3,+AC(x4,x5)) +AC(x3,x4) -> +AC(x4,x3) *AC(*AC(x3,x4),x5) -> *AC(x3,*AC(x4,x5)) *AC(x3,x4) -> *AC(x4,x3) UAC(UAC(x3,x4),x5) -> UAC(x3,UAC(x4,x5)) UAC(x3,x4) -> UAC(x4,x3) +AC(x3,+AC(x4,x5)) -> +AC(+AC(x3,x4),x5) +AC(x4,x3) -> +AC(x3,x4) *AC(x3,*AC(x4,x5)) -> *AC(*AC(x3,x4),x5) *AC(x4,x3) -> *AC(x3,x4) UAC(x3,UAC(x4,x5)) -> UAC(UAC(x3,x4),x5) UAC(x4,x3) -> UAC(x3,x4) TRS: S: +AC(+AC(x11,x12),x13) -> +AC(x11,x12) +AC(x11,+AC(x12,x13)) -> +AC(x12,x13) *AC(*AC(x11,x12),x13) -> *AC(x11,x12) *AC(x11,*AC(x12,x13)) -> *AC(x12,x13) UAC(UAC(x11,x12),x13) -> UAC(x11,x12) UAC(x11,UAC(x12,x13)) -> UAC(x12,x13) Qed Equations#: +{AC,#}(+AC(x3,x4),x5) -> +{AC,#}(x3,+AC(x4,x5)) +{AC,#}(x3,x4) -> +{AC,#}(x4,x3) *{AC,#}(*AC(x3,x4),x5) -> *{AC,#}(x3,*AC(x4,x5)) *{AC,#}(x3,x4) -> *{AC,#}(x4,x3) U{AC,#}(UAC(x3,x4),x5) -> U{AC,#}(x3,UAC(x4,x5)) U{AC,#}(x3,x4) -> U{AC,#}(x4,x3) +{AC,#}(x3,+AC(x4,x5)) -> +{AC,#}(+AC(x3,x4),x5) +{AC,#}(x4,x3) -> +{AC,#}(x3,x4) *{AC,#}(x3,*AC(x4,x5)) -> *{AC,#}(*AC(x3,x4),x5) *{AC,#}(x4,x3) -> *{AC,#}(x3,x4) U{AC,#}(x3,UAC(x4,x5)) -> U{AC,#}(UAC(x3,x4),x5) U{AC,#}(x4,x3) -> U{AC,#}(x3,x4) DPs: *{AC,#}(x9,*AC(s(x),s(y))) -> *{AC,#}(x9,s(+AC(+AC(x,y),*AC(x,y)))) *{AC,#}(x9,*AC(s(x),s(y))) -> *{AC,#}(x,y) *{AC,#}(x8,*AC(0(),x)) -> *{AC,#}(x8,0()) *{AC,#}(s(x),s(y)) -> *{AC,#}(x,y) Equations: +AC(+AC(x3,x4),x5) -> +AC(x3,+AC(x4,x5)) +AC(x3,x4) -> +AC(x4,x3) *AC(*AC(x3,x4),x5) -> *AC(x3,*AC(x4,x5)) *AC(x3,x4) -> *AC(x4,x3) UAC(UAC(x3,x4),x5) -> UAC(x3,UAC(x4,x5)) UAC(x3,x4) -> UAC(x4,x3) +AC(x3,+AC(x4,x5)) -> +AC(+AC(x3,x4),x5) +AC(x4,x3) -> +AC(x3,x4) *AC(x3,*AC(x4,x5)) -> *AC(*AC(x3,x4),x5) *AC(x4,x3) -> *AC(x3,x4) UAC(x3,UAC(x4,x5)) -> UAC(UAC(x3,x4),x5) UAC(x4,x3) -> UAC(x3,x4) TRS: +AC(0(),x) -> x +AC(s(x),s(y)) -> s(s(+AC(x,y))) *AC(0(),x) -> 0() *AC(s(x),s(y)) -> s(+AC(+AC(x,y),*AC(x,y))) UAC(empty(),b) -> b sum(empty()) -> 0() sum(singl(x)) -> x sum(UAC(x,y)) -> +AC(sum(x),sum(y)) prod(empty()) -> s(0()) prod(singl(x)) -> x prod(UAC(x,y)) -> *AC(prod(x),prod(y)) S: +{AC,#}(+AC(x11,x12),x13) -> +{AC,#}(x11,x12) +{AC,#}(x11,+AC(x12,x13)) -> +{AC,#}(x12,x13) *{AC,#}(*AC(x11,x12),x13) -> *{AC,#}(x11,x12) *{AC,#}(x11,*AC(x12,x13)) -> *{AC,#}(x12,x13) U{AC,#}(UAC(x11,x12),x13) -> U{AC,#}(x11,x12) U{AC,#}(x11,UAC(x12,x13)) -> U{AC,#}(x12,x13) AC-DP unlabeling: Equations#: +AC(+AC(x3,x4),x5) -> +AC(x3,+AC(x4,x5)) +AC(x3,x4) -> +AC(x4,x3) *AC(*AC(x3,x4),x5) -> *AC(x3,*AC(x4,x5)) *AC(x3,x4) -> *AC(x4,x3) UAC(UAC(x3,x4),x5) -> UAC(x3,UAC(x4,x5)) UAC(x3,x4) -> UAC(x4,x3) +AC(x3,+AC(x4,x5)) -> +AC(+AC(x3,x4),x5) +AC(x4,x3) -> +AC(x3,x4) *AC(x3,*AC(x4,x5)) -> *AC(*AC(x3,x4),x5) *AC(x4,x3) -> *AC(x3,x4) UAC(x3,UAC(x4,x5)) -> UAC(UAC(x3,x4),x5) UAC(x4,x3) -> UAC(x3,x4) DPs: *AC(x9,*AC(s(x),s(y))) -> *AC(x9,s(+AC(+AC(x,y),*AC(x,y)))) *AC(x9,*AC(s(x),s(y))) -> *AC(x,y) *AC(x8,*AC(0(),x)) -> *AC(x8,0()) *AC(s(x),s(y)) -> *AC(x,y) Equations: +AC(+AC(x3,x4),x5) -> +AC(x3,+AC(x4,x5)) +AC(x3,x4) -> +AC(x4,x3) *AC(*AC(x3,x4),x5) -> *AC(x3,*AC(x4,x5)) *AC(x3,x4) -> *AC(x4,x3) UAC(UAC(x3,x4),x5) -> UAC(x3,UAC(x4,x5)) UAC(x3,x4) -> UAC(x4,x3) +AC(x3,+AC(x4,x5)) -> +AC(+AC(x3,x4),x5) +AC(x4,x3) -> +AC(x3,x4) *AC(x3,*AC(x4,x5)) -> *AC(*AC(x3,x4),x5) *AC(x4,x3) -> *AC(x3,x4) UAC(x3,UAC(x4,x5)) -> UAC(UAC(x3,x4),x5) UAC(x4,x3) -> UAC(x3,x4) TRS: +AC(0(),x) -> x +AC(s(x),s(y)) -> s(s(+AC(x,y))) *AC(0(),x) -> 0() *AC(s(x),s(y)) -> s(+AC(+AC(x,y),*AC(x,y))) UAC(empty(),b) -> b sum(empty()) -> 0() sum(singl(x)) -> x sum(UAC(x,y)) -> +AC(sum(x),sum(y)) prod(empty()) -> s(0()) prod(singl(x)) -> x prod(UAC(x,y)) -> *AC(prod(x),prod(y)) S: +AC(+AC(x11,x12),x13) -> +AC(x11,x12) +AC(x11,+AC(x12,x13)) -> +AC(x12,x13) *AC(*AC(x11,x12),x13) -> *AC(x11,x12) *AC(x11,*AC(x12,x13)) -> *AC(x12,x13) UAC(UAC(x11,x12),x13) -> UAC(x11,x12) UAC(x11,UAC(x12,x13)) -> UAC(x12,x13) Usable Rule Processor: Equations#: +AC(+AC(x3,x4),x5) -> +AC(x3,+AC(x4,x5)) +AC(x3,x4) -> +AC(x4,x3) *AC(*AC(x3,x4),x5) -> *AC(x3,*AC(x4,x5)) *AC(x3,x4) -> *AC(x4,x3) UAC(UAC(x3,x4),x5) -> UAC(x3,UAC(x4,x5)) UAC(x3,x4) -> UAC(x4,x3) +AC(x3,+AC(x4,x5)) -> +AC(+AC(x3,x4),x5) +AC(x4,x3) -> +AC(x3,x4) *AC(x3,*AC(x4,x5)) -> *AC(*AC(x3,x4),x5) *AC(x4,x3) -> *AC(x3,x4) UAC(x3,UAC(x4,x5)) -> UAC(UAC(x3,x4),x5) UAC(x4,x3) -> UAC(x3,x4) DPs: *AC(x9,*AC(s(x),s(y))) -> *AC(x9,s(+AC(+AC(x,y),*AC(x,y)))) *AC(x9,*AC(s(x),s(y))) -> *AC(x,y) *AC(x8,*AC(0(),x)) -> *AC(x8,0()) *AC(s(x),s(y)) -> *AC(x,y) Equations: +AC(+AC(x3,x4),x5) -> +AC(x3,+AC(x4,x5)) +AC(x3,x4) -> +AC(x4,x3) *AC(*AC(x3,x4),x5) -> *AC(x3,*AC(x4,x5)) *AC(x3,x4) -> *AC(x4,x3) UAC(UAC(x3,x4),x5) -> UAC(x3,UAC(x4,x5)) UAC(x3,x4) -> UAC(x4,x3) +AC(x3,+AC(x4,x5)) -> +AC(+AC(x3,x4),x5) +AC(x4,x3) -> +AC(x3,x4) *AC(x3,*AC(x4,x5)) -> *AC(*AC(x3,x4),x5) *AC(x4,x3) -> *AC(x3,x4) UAC(x3,UAC(x4,x5)) -> UAC(UAC(x3,x4),x5) UAC(x4,x3) -> UAC(x3,x4) TRS: *AC(0(),x) -> 0() *AC(s(x),s(y)) -> s(+AC(+AC(x,y),*AC(x,y))) +AC(0(),x) -> x +AC(s(x),s(y)) -> s(s(+AC(x,y))) S: +AC(+AC(x11,x12),x13) -> +AC(x11,x12) +AC(x11,+AC(x12,x13)) -> +AC(x12,x13) *AC(*AC(x11,x12),x13) -> *AC(x11,x12) *AC(x11,*AC(x12,x13)) -> *AC(x12,x13) UAC(UAC(x11,x12),x13) -> UAC(x11,x12) UAC(x11,UAC(x12,x13)) -> UAC(x12,x13) AC-RPO Processor: argument filtering: pi(UAC) = [0,1] pi(*AC) = [0,1] pi(+AC) = [] pi(0) = [] pi(s) = [] precedence: *AC > 0 > s > +AC > UAC status: problem: Equations#: +AC(+AC(x3,x4),x5) -> +AC(x3,+AC(x4,x5)) +AC(x3,x4) -> +AC(x4,x3) *AC(*AC(x3,x4),x5) -> *AC(x3,*AC(x4,x5)) *AC(x3,x4) -> *AC(x4,x3) UAC(UAC(x3,x4),x5) -> UAC(x3,UAC(x4,x5)) UAC(x3,x4) -> UAC(x4,x3) +AC(x3,+AC(x4,x5)) -> +AC(+AC(x3,x4),x5) +AC(x4,x3) -> +AC(x3,x4) *AC(x3,*AC(x4,x5)) -> *AC(*AC(x3,x4),x5) *AC(x4,x3) -> *AC(x3,x4) UAC(x3,UAC(x4,x5)) -> UAC(UAC(x3,x4),x5) UAC(x4,x3) -> UAC(x3,x4) DPs: Equations: +AC(+AC(x3,x4),x5) -> +AC(x3,+AC(x4,x5)) +AC(x3,x4) -> +AC(x4,x3) *AC(*AC(x3,x4),x5) -> *AC(x3,*AC(x4,x5)) *AC(x3,x4) -> *AC(x4,x3) UAC(UAC(x3,x4),x5) -> UAC(x3,UAC(x4,x5)) UAC(x3,x4) -> UAC(x4,x3) +AC(x3,+AC(x4,x5)) -> +AC(+AC(x3,x4),x5) +AC(x4,x3) -> +AC(x3,x4) *AC(x3,*AC(x4,x5)) -> *AC(*AC(x3,x4),x5) *AC(x4,x3) -> *AC(x3,x4) UAC(x3,UAC(x4,x5)) -> UAC(UAC(x3,x4),x5) UAC(x4,x3) -> UAC(x3,x4) TRS: *AC(0(),x) -> 0() *AC(s(x),s(y)) -> s(+AC(+AC(x,y),*AC(x,y))) +AC(0(),x) -> x +AC(s(x),s(y)) -> s(s(+AC(x,y))) S: +AC(+AC(x11,x12),x13) -> +AC(x11,x12) +AC(x11,+AC(x12,x13)) -> +AC(x12,x13) *AC(*AC(x11,x12),x13) -> *AC(x11,x12) *AC(x11,*AC(x12,x13)) -> *AC(x12,x13) UAC(UAC(x11,x12),x13) -> UAC(x11,x12) UAC(x11,UAC(x12,x13)) -> UAC(x12,x13) Qed Equations#: +{AC,#}(+AC(x3,x4),x5) -> +{AC,#}(x3,+AC(x4,x5)) +{AC,#}(x3,x4) -> +{AC,#}(x4,x3) *{AC,#}(*AC(x3,x4),x5) -> *{AC,#}(x3,*AC(x4,x5)) *{AC,#}(x3,x4) -> *{AC,#}(x4,x3) U{AC,#}(UAC(x3,x4),x5) -> U{AC,#}(x3,UAC(x4,x5)) U{AC,#}(x3,x4) -> U{AC,#}(x4,x3) +{AC,#}(x3,+AC(x4,x5)) -> +{AC,#}(+AC(x3,x4),x5) +{AC,#}(x4,x3) -> +{AC,#}(x3,x4) *{AC,#}(x3,*AC(x4,x5)) -> *{AC,#}(*AC(x3,x4),x5) *{AC,#}(x4,x3) -> *{AC,#}(x3,x4) U{AC,#}(x3,UAC(x4,x5)) -> U{AC,#}(UAC(x3,x4),x5) U{AC,#}(x4,x3) -> U{AC,#}(x3,x4) DPs: +{AC,#}(x7,+AC(s(x),s(y))) -> +{AC,#}(x7,s(s(+AC(x,y)))) +{AC,#}(x7,+AC(s(x),s(y))) -> +{AC,#}(x,y) +{AC,#}(x6,+AC(0(),x)) -> +{AC,#}(x6,x) +{AC,#}(s(x),s(y)) -> +{AC,#}(x,y) Equations: +AC(+AC(x3,x4),x5) -> +AC(x3,+AC(x4,x5)) +AC(x3,x4) -> +AC(x4,x3) *AC(*AC(x3,x4),x5) -> *AC(x3,*AC(x4,x5)) *AC(x3,x4) -> *AC(x4,x3) UAC(UAC(x3,x4),x5) -> UAC(x3,UAC(x4,x5)) UAC(x3,x4) -> UAC(x4,x3) +AC(x3,+AC(x4,x5)) -> +AC(+AC(x3,x4),x5) +AC(x4,x3) -> +AC(x3,x4) *AC(x3,*AC(x4,x5)) -> *AC(*AC(x3,x4),x5) *AC(x4,x3) -> *AC(x3,x4) UAC(x3,UAC(x4,x5)) -> UAC(UAC(x3,x4),x5) UAC(x4,x3) -> UAC(x3,x4) TRS: +AC(0(),x) -> x +AC(s(x),s(y)) -> s(s(+AC(x,y))) *AC(0(),x) -> 0() *AC(s(x),s(y)) -> s(+AC(+AC(x,y),*AC(x,y))) UAC(empty(),b) -> b sum(empty()) -> 0() sum(singl(x)) -> x sum(UAC(x,y)) -> +AC(sum(x),sum(y)) prod(empty()) -> s(0()) prod(singl(x)) -> x prod(UAC(x,y)) -> *AC(prod(x),prod(y)) S: +{AC,#}(+AC(x11,x12),x13) -> +{AC,#}(x11,x12) +{AC,#}(x11,+AC(x12,x13)) -> +{AC,#}(x12,x13) *{AC,#}(*AC(x11,x12),x13) -> *{AC,#}(x11,x12) *{AC,#}(x11,*AC(x12,x13)) -> *{AC,#}(x12,x13) U{AC,#}(UAC(x11,x12),x13) -> U{AC,#}(x11,x12) U{AC,#}(x11,UAC(x12,x13)) -> U{AC,#}(x12,x13) AC-DP unlabeling: Equations#: +AC(+AC(x3,x4),x5) -> +AC(x3,+AC(x4,x5)) +AC(x3,x4) -> +AC(x4,x3) *AC(*AC(x3,x4),x5) -> *AC(x3,*AC(x4,x5)) *AC(x3,x4) -> *AC(x4,x3) UAC(UAC(x3,x4),x5) -> UAC(x3,UAC(x4,x5)) UAC(x3,x4) -> UAC(x4,x3) +AC(x3,+AC(x4,x5)) -> +AC(+AC(x3,x4),x5) +AC(x4,x3) -> +AC(x3,x4) *AC(x3,*AC(x4,x5)) -> *AC(*AC(x3,x4),x5) *AC(x4,x3) -> *AC(x3,x4) UAC(x3,UAC(x4,x5)) -> UAC(UAC(x3,x4),x5) UAC(x4,x3) -> UAC(x3,x4) DPs: +AC(x7,+AC(s(x),s(y))) -> +AC(x7,s(s(+AC(x,y)))) +AC(x7,+AC(s(x),s(y))) -> +AC(x,y) +AC(x6,+AC(0(),x)) -> +AC(x6,x) +AC(s(x),s(y)) -> +AC(x,y) Equations: +AC(+AC(x3,x4),x5) -> +AC(x3,+AC(x4,x5)) +AC(x3,x4) -> +AC(x4,x3) *AC(*AC(x3,x4),x5) -> *AC(x3,*AC(x4,x5)) *AC(x3,x4) -> *AC(x4,x3) UAC(UAC(x3,x4),x5) -> UAC(x3,UAC(x4,x5)) UAC(x3,x4) -> UAC(x4,x3) +AC(x3,+AC(x4,x5)) -> +AC(+AC(x3,x4),x5) +AC(x4,x3) -> +AC(x3,x4) *AC(x3,*AC(x4,x5)) -> *AC(*AC(x3,x4),x5) *AC(x4,x3) -> *AC(x3,x4) UAC(x3,UAC(x4,x5)) -> UAC(UAC(x3,x4),x5) UAC(x4,x3) -> UAC(x3,x4) TRS: +AC(0(),x) -> x +AC(s(x),s(y)) -> s(s(+AC(x,y))) *AC(0(),x) -> 0() *AC(s(x),s(y)) -> s(+AC(+AC(x,y),*AC(x,y))) UAC(empty(),b) -> b sum(empty()) -> 0() sum(singl(x)) -> x sum(UAC(x,y)) -> +AC(sum(x),sum(y)) prod(empty()) -> s(0()) prod(singl(x)) -> x prod(UAC(x,y)) -> *AC(prod(x),prod(y)) S: +AC(+AC(x11,x12),x13) -> +AC(x11,x12) +AC(x11,+AC(x12,x13)) -> +AC(x12,x13) *AC(*AC(x11,x12),x13) -> *AC(x11,x12) *AC(x11,*AC(x12,x13)) -> *AC(x12,x13) UAC(UAC(x11,x12),x13) -> UAC(x11,x12) UAC(x11,UAC(x12,x13)) -> UAC(x12,x13) Usable Rule Processor: Equations#: +AC(+AC(x3,x4),x5) -> +AC(x3,+AC(x4,x5)) +AC(x3,x4) -> +AC(x4,x3) *AC(*AC(x3,x4),x5) -> *AC(x3,*AC(x4,x5)) *AC(x3,x4) -> *AC(x4,x3) UAC(UAC(x3,x4),x5) -> UAC(x3,UAC(x4,x5)) UAC(x3,x4) -> UAC(x4,x3) +AC(x3,+AC(x4,x5)) -> +AC(+AC(x3,x4),x5) +AC(x4,x3) -> +AC(x3,x4) *AC(x3,*AC(x4,x5)) -> *AC(*AC(x3,x4),x5) *AC(x4,x3) -> *AC(x3,x4) UAC(x3,UAC(x4,x5)) -> UAC(UAC(x3,x4),x5) UAC(x4,x3) -> UAC(x3,x4) DPs: +AC(x7,+AC(s(x),s(y))) -> +AC(x7,s(s(+AC(x,y)))) +AC(x7,+AC(s(x),s(y))) -> +AC(x,y) +AC(x6,+AC(0(),x)) -> +AC(x6,x) +AC(s(x),s(y)) -> +AC(x,y) Equations: +AC(+AC(x3,x4),x5) -> +AC(x3,+AC(x4,x5)) +AC(x3,x4) -> +AC(x4,x3) *AC(*AC(x3,x4),x5) -> *AC(x3,*AC(x4,x5)) *AC(x3,x4) -> *AC(x4,x3) UAC(UAC(x3,x4),x5) -> UAC(x3,UAC(x4,x5)) UAC(x3,x4) -> UAC(x4,x3) +AC(x3,+AC(x4,x5)) -> +AC(+AC(x3,x4),x5) +AC(x4,x3) -> +AC(x3,x4) *AC(x3,*AC(x4,x5)) -> *AC(*AC(x3,x4),x5) *AC(x4,x3) -> *AC(x3,x4) UAC(x3,UAC(x4,x5)) -> UAC(UAC(x3,x4),x5) UAC(x4,x3) -> UAC(x3,x4) TRS: +AC(0(),x) -> x +AC(s(x),s(y)) -> s(s(+AC(x,y))) S: +AC(+AC(x11,x12),x13) -> +AC(x11,x12) +AC(x11,+AC(x12,x13)) -> +AC(x12,x13) *AC(*AC(x11,x12),x13) -> *AC(x11,x12) *AC(x11,*AC(x12,x13)) -> *AC(x12,x13) UAC(UAC(x11,x12),x13) -> UAC(x11,x12) UAC(x11,UAC(x12,x13)) -> UAC(x12,x13) AC-RPO Processor: argument filtering: pi(UAC) = [] pi(*AC) = [0,1] pi(+AC) = [0,1] pi(0) = [] pi(s) = [0] precedence: +AC > UAC > s > 0 > *AC status: problem: Equations#: +AC(+AC(x3,x4),x5) -> +AC(x3,+AC(x4,x5)) +AC(x3,x4) -> +AC(x4,x3) *AC(*AC(x3,x4),x5) -> *AC(x3,*AC(x4,x5)) *AC(x3,x4) -> *AC(x4,x3) UAC(UAC(x3,x4),x5) -> UAC(x3,UAC(x4,x5)) UAC(x3,x4) -> UAC(x4,x3) +AC(x3,+AC(x4,x5)) -> +AC(+AC(x3,x4),x5) +AC(x4,x3) -> +AC(x3,x4) *AC(x3,*AC(x4,x5)) -> *AC(*AC(x3,x4),x5) *AC(x4,x3) -> *AC(x3,x4) UAC(x3,UAC(x4,x5)) -> UAC(UAC(x3,x4),x5) UAC(x4,x3) -> UAC(x3,x4) DPs: Equations: +AC(+AC(x3,x4),x5) -> +AC(x3,+AC(x4,x5)) +AC(x3,x4) -> +AC(x4,x3) *AC(*AC(x3,x4),x5) -> *AC(x3,*AC(x4,x5)) *AC(x3,x4) -> *AC(x4,x3) UAC(UAC(x3,x4),x5) -> UAC(x3,UAC(x4,x5)) UAC(x3,x4) -> UAC(x4,x3) +AC(x3,+AC(x4,x5)) -> +AC(+AC(x3,x4),x5) +AC(x4,x3) -> +AC(x3,x4) *AC(x3,*AC(x4,x5)) -> *AC(*AC(x3,x4),x5) *AC(x4,x3) -> *AC(x3,x4) UAC(x3,UAC(x4,x5)) -> UAC(UAC(x3,x4),x5) UAC(x4,x3) -> UAC(x3,x4) TRS: +AC(0(),x) -> x +AC(s(x),s(y)) -> s(s(+AC(x,y))) S: +AC(+AC(x11,x12),x13) -> +AC(x11,x12) +AC(x11,+AC(x12,x13)) -> +AC(x12,x13) *AC(*AC(x11,x12),x13) -> *AC(x11,x12) *AC(x11,*AC(x12,x13)) -> *AC(x12,x13) UAC(UAC(x11,x12),x13) -> UAC(x11,x12) UAC(x11,UAC(x12,x13)) -> UAC(x12,x13) Qed