MAYBE Time: 7.261 Problem: Equations: unionAC(unionAC(x7,x8),x9) -> unionAC(x7,unionAC(x8,x9)) unionAC(x7,x8) -> unionAC(x8,x7) plusAC(plusAC(x7,x8),x9) -> plusAC(x7,plusAC(x8,x9)) plusAC(x7,x8) -> plusAC(x8,x7) multAC(multAC(x7,x8),x9) -> multAC(x7,multAC(x8,x9)) multAC(x7,x8) -> multAC(x8,x7) unionAC(x7,unionAC(x8,x9)) -> unionAC(unionAC(x7,x8),x9) unionAC(x8,x7) -> unionAC(x7,x8) plusAC(x7,plusAC(x8,x9)) -> plusAC(plusAC(x7,x8),x9) plusAC(x8,x7) -> plusAC(x7,x8) multAC(x7,multAC(x8,x9)) -> multAC(multAC(x7,x8),x9) multAC(x8,x7) -> multAC(x7,x8) TRS: unionAC(X,empty()) -> X unionAC(empty(),X) -> X 0(z()) -> z() U101(tt(),X) -> X U11(tt()) -> z() U111(tt(),A,B) -> plusAC(sum(A),sum(B)) U21(tt(),X,Y) -> 0(multAC(X,Y)) U31(tt(),X,Y) -> plusAC(0(multAC(X,Y)),Y) U41(tt(),X) -> X U51(tt(),X,Y) -> 0(plusAC(X,Y)) U61(tt(),X,Y) -> 1(plusAC(X,Y)) U71(tt(),X,Y) -> 0(plusAC(plusAC(X,Y),1(z()))) U81(tt(),X) -> X U91(tt(),A,B) -> multAC(prod(A),prod(B)) and(tt(),X) -> X isBag(empty()) -> tt() isBag(singl(V1)) -> isBin(V1) isBag(unionAC(V1,V2)) -> and(isBag(V1),isBag(V2)) isBin(z()) -> tt() isBin(0(V1)) -> isBin(V1) isBin(1(V1)) -> isBin(V1) isBin(multAC(V1,V2)) -> and(isBin(V1),isBin(V2)) isBin(plusAC(V1,V2)) -> and(isBin(V1),isBin(V2)) isBin(prod(V1)) -> isBag(V1) isBin(sum(V1)) -> isBag(V1) multAC(z(),X) -> U11(isBin(X)) multAC(0(X),Y) -> U21(and(isBin(X),isBin(Y)),X,Y) multAC(1(X),Y) -> U31(and(isBin(X),isBin(Y)),X,Y) plusAC(z(),X) -> U41(isBin(X),X) plusAC(0(X),0(Y)) -> U51(and(isBin(X),isBin(Y)),X,Y) plusAC(0(X),1(Y)) -> U61(and(isBin(X),isBin(Y)),X,Y) plusAC(1(X),1(Y)) -> U71(and(isBin(X),isBin(Y)),X,Y) prod(empty()) -> 1(z()) prod(singl(X)) -> U81(isBin(X),X) prod(unionAC(A,B)) -> U91(and(isBag(A),isBag(B)),A,B) sum(empty()) -> 0(z()) sum(singl(X)) -> U101(isBin(X),X) sum(unionAC(A,B)) -> U111(and(isBag(A),isBag(B)),A,B) Proof: DP Processor: Equations#: union{AC,#}(unionAC(x7,x8),x9) -> union{AC,#}(x7,unionAC(x8,x9)) union{AC,#}(x7,x8) -> union{AC,#}(x8,x7) plus{AC,#}(plusAC(x7,x8),x9) -> plus{AC,#}(x7,plusAC(x8,x9)) plus{AC,#}(x7,x8) -> plus{AC,#}(x8,x7) mult{AC,#}(multAC(x7,x8),x9) -> mult{AC,#}(x7,multAC(x8,x9)) mult{AC,#}(x7,x8) -> mult{AC,#}(x8,x7) union{AC,#}(x7,unionAC(x8,x9)) -> union{AC,#}(unionAC(x7,x8),x9) union{AC,#}(x8,x7) -> union{AC,#}(x7,x8) plus{AC,#}(x7,plusAC(x8,x9)) -> plus{AC,#}(plusAC(x7,x8),x9) plus{AC,#}(x8,x7) -> plus{AC,#}(x7,x8) mult{AC,#}(x7,multAC(x8,x9)) -> mult{AC,#}(multAC(x7,x8),x9) mult{AC,#}(x8,x7) -> mult{AC,#}(x7,x8) DPs: U111#(tt(),A,B) -> sum#(B) U111#(tt(),A,B) -> sum#(A) U111#(tt(),A,B) -> plus{AC,#}(sum(A),sum(B)) U21#(tt(),X,Y) -> mult{AC,#}(X,Y) U21#(tt(),X,Y) -> 0#(multAC(X,Y)) U31#(tt(),X,Y) -> mult{AC,#}(X,Y) U31#(tt(),X,Y) -> 0#(multAC(X,Y)) U31#(tt(),X,Y) -> plus{AC,#}(0(multAC(X,Y)),Y) U51#(tt(),X,Y) -> plus{AC,#}(X,Y) U51#(tt(),X,Y) -> 0#(plusAC(X,Y)) U61#(tt(),X,Y) -> plus{AC,#}(X,Y) U71#(tt(),X,Y) -> plus{AC,#}(X,Y) U71#(tt(),X,Y) -> plus{AC,#}(plusAC(X,Y),1(z())) U71#(tt(),X,Y) -> 0#(plusAC(plusAC(X,Y),1(z()))) U91#(tt(),A,B) -> prod#(B) U91#(tt(),A,B) -> prod#(A) U91#(tt(),A,B) -> mult{AC,#}(prod(A),prod(B)) isBag#(singl(V1)) -> isBin#(V1) isBag#(unionAC(V1,V2)) -> isBag#(V2) isBag#(unionAC(V1,V2)) -> isBag#(V1) isBag#(unionAC(V1,V2)) -> and#(isBag(V1),isBag(V2)) isBin#(0(V1)) -> isBin#(V1) isBin#(1(V1)) -> isBin#(V1) isBin#(multAC(V1,V2)) -> isBin#(V2) isBin#(multAC(V1,V2)) -> isBin#(V1) isBin#(multAC(V1,V2)) -> and#(isBin(V1),isBin(V2)) isBin#(plusAC(V1,V2)) -> isBin#(V2) isBin#(plusAC(V1,V2)) -> isBin#(V1) isBin#(plusAC(V1,V2)) -> and#(isBin(V1),isBin(V2)) isBin#(prod(V1)) -> isBag#(V1) isBin#(sum(V1)) -> isBag#(V1) mult{AC,#}(z(),X) -> isBin#(X) mult{AC,#}(z(),X) -> U11#(isBin(X)) mult{AC,#}(0(X),Y) -> isBin#(Y) mult{AC,#}(0(X),Y) -> isBin#(X) mult{AC,#}(0(X),Y) -> and#(isBin(X),isBin(Y)) mult{AC,#}(0(X),Y) -> U21#(and(isBin(X),isBin(Y)),X,Y) mult{AC,#}(1(X),Y) -> isBin#(Y) mult{AC,#}(1(X),Y) -> isBin#(X) mult{AC,#}(1(X),Y) -> and#(isBin(X),isBin(Y)) mult{AC,#}(1(X),Y) -> U31#(and(isBin(X),isBin(Y)),X,Y) plus{AC,#}(z(),X) -> isBin#(X) plus{AC,#}(z(),X) -> U41#(isBin(X),X) plus{AC,#}(0(X),0(Y)) -> isBin#(Y) plus{AC,#}(0(X),0(Y)) -> isBin#(X) plus{AC,#}(0(X),0(Y)) -> and#(isBin(X),isBin(Y)) plus{AC,#}(0(X),0(Y)) -> U51#(and(isBin(X),isBin(Y)),X,Y) plus{AC,#}(0(X),1(Y)) -> isBin#(Y) plus{AC,#}(0(X),1(Y)) -> isBin#(X) plus{AC,#}(0(X),1(Y)) -> and#(isBin(X),isBin(Y)) plus{AC,#}(0(X),1(Y)) -> U61#(and(isBin(X),isBin(Y)),X,Y) plus{AC,#}(1(X),1(Y)) -> isBin#(Y) plus{AC,#}(1(X),1(Y)) -> isBin#(X) plus{AC,#}(1(X),1(Y)) -> and#(isBin(X),isBin(Y)) plus{AC,#}(1(X),1(Y)) -> U71#(and(isBin(X),isBin(Y)),X,Y) prod#(singl(X)) -> isBin#(X) prod#(singl(X)) -> U81#(isBin(X),X) prod#(unionAC(A,B)) -> isBag#(B) prod#(unionAC(A,B)) -> isBag#(A) prod#(unionAC(A,B)) -> and#(isBag(A),isBag(B)) prod#(unionAC(A,B)) -> U91#(and(isBag(A),isBag(B)),A,B) sum#(empty()) -> 0#(z()) sum#(singl(X)) -> isBin#(X) sum#(singl(X)) -> U101#(isBin(X),X) sum#(unionAC(A,B)) -> isBag#(B) sum#(unionAC(A,B)) -> isBag#(A) sum#(unionAC(A,B)) -> and#(isBag(A),isBag(B)) sum#(unionAC(A,B)) -> U111#(and(isBag(A),isBag(B)),A,B) union{AC,#}(x10,unionAC(X,empty())) -> union{AC,#}(x10,X) union{AC,#}(x11,unionAC(empty(),X)) -> union{AC,#}(x11,X) mult{AC,#}(x12,multAC(z(),X)) -> isBin#(X) mult{AC,#}(x12,multAC(z(),X)) -> U11#(isBin(X)) mult{AC,#}(x12,multAC(z(),X)) -> mult{AC,#}(x12,U11(isBin(X))) mult{AC,#}(x13,multAC(0(X),Y)) -> isBin#(Y) mult{AC,#}(x13,multAC(0(X),Y)) -> isBin#(X) mult{AC,#}(x13,multAC(0(X),Y)) -> and#(isBin(X),isBin(Y)) mult{AC,#}(x13,multAC(0(X),Y)) -> U21#(and(isBin(X),isBin(Y)),X,Y) mult{AC,#}(x13,multAC(0(X),Y)) -> mult{AC,#}(x13,U21(and(isBin(X),isBin(Y)),X,Y)) mult{AC,#}(x14,multAC(1(X),Y)) -> isBin#(Y) mult{AC,#}(x14,multAC(1(X),Y)) -> isBin#(X) mult{AC,#}(x14,multAC(1(X),Y)) -> and#(isBin(X),isBin(Y)) mult{AC,#}(x14,multAC(1(X),Y)) -> U31#(and(isBin(X),isBin(Y)),X,Y) mult{AC,#}(x14,multAC(1(X),Y)) -> mult{AC,#}(x14,U31(and(isBin(X),isBin(Y)),X,Y)) plus{AC,#}(x15,plusAC(z(),X)) -> isBin#(X) plus{AC,#}(x15,plusAC(z(),X)) -> U41#(isBin(X),X) plus{AC,#}(x15,plusAC(z(),X)) -> plus{AC,#}(x15,U41(isBin(X),X)) plus{AC,#}(x16,plusAC(0(X),0(Y))) -> isBin#(Y) plus{AC,#}(x16,plusAC(0(X),0(Y))) -> isBin#(X) plus{AC,#}(x16,plusAC(0(X),0(Y))) -> and#(isBin(X),isBin(Y)) plus{AC,#}(x16,plusAC(0(X),0(Y))) -> U51#(and(isBin(X),isBin(Y)),X,Y) plus{AC,#}(x16,plusAC(0(X),0(Y))) -> plus{AC,#}(x16,U51(and(isBin(X),isBin(Y)),X,Y)) plus{AC,#}(x17,plusAC(0(X),1(Y))) -> isBin#(Y) plus{AC,#}(x17,plusAC(0(X),1(Y))) -> isBin#(X) plus{AC,#}(x17,plusAC(0(X),1(Y))) -> and#(isBin(X),isBin(Y)) plus{AC,#}(x17,plusAC(0(X),1(Y))) -> U61#(and(isBin(X),isBin(Y)),X,Y) plus{AC,#}(x17,plusAC(0(X),1(Y))) -> plus{AC,#}(x17,U61(and(isBin(X),isBin(Y)),X,Y)) plus{AC,#}(x18,plusAC(1(X),1(Y))) -> isBin#(Y) plus{AC,#}(x18,plusAC(1(X),1(Y))) -> isBin#(X) plus{AC,#}(x18,plusAC(1(X),1(Y))) -> and#(isBin(X),isBin(Y)) plus{AC,#}(x18,plusAC(1(X),1(Y))) -> U71#(and(isBin(X),isBin(Y)),X,Y) plus{AC,#}(x18,plusAC(1(X),1(Y))) -> plus{AC,#}(x18,U71(and(isBin(X),isBin(Y)),X,Y)) Equations: unionAC(unionAC(x7,x8),x9) -> unionAC(x7,unionAC(x8,x9)) unionAC(x7,x8) -> unionAC(x8,x7) plusAC(plusAC(x7,x8),x9) -> plusAC(x7,plusAC(x8,x9)) plusAC(x7,x8) -> plusAC(x8,x7) multAC(multAC(x7,x8),x9) -> multAC(x7,multAC(x8,x9)) multAC(x7,x8) -> multAC(x8,x7) unionAC(x7,unionAC(x8,x9)) -> unionAC(unionAC(x7,x8),x9) unionAC(x8,x7) -> unionAC(x7,x8) plusAC(x7,plusAC(x8,x9)) -> plusAC(plusAC(x7,x8),x9) plusAC(x8,x7) -> plusAC(x7,x8) multAC(x7,multAC(x8,x9)) -> multAC(multAC(x7,x8),x9) multAC(x8,x7) -> multAC(x7,x8) TRS: unionAC(X,empty()) -> X unionAC(empty(),X) -> X 0(z()) -> z() U101(tt(),X) -> X U11(tt()) -> z() U111(tt(),A,B) -> plusAC(sum(A),sum(B)) U21(tt(),X,Y) -> 0(multAC(X,Y)) U31(tt(),X,Y) -> plusAC(0(multAC(X,Y)),Y) U41(tt(),X) -> X U51(tt(),X,Y) -> 0(plusAC(X,Y)) U61(tt(),X,Y) -> 1(plusAC(X,Y)) U71(tt(),X,Y) -> 0(plusAC(plusAC(X,Y),1(z()))) U81(tt(),X) -> X U91(tt(),A,B) -> multAC(prod(A),prod(B)) and(tt(),X) -> X isBag(empty()) -> tt() isBag(singl(V1)) -> isBin(V1) isBag(unionAC(V1,V2)) -> and(isBag(V1),isBag(V2)) isBin(z()) -> tt() isBin(0(V1)) -> isBin(V1) isBin(1(V1)) -> isBin(V1) isBin(multAC(V1,V2)) -> and(isBin(V1),isBin(V2)) isBin(plusAC(V1,V2)) -> and(isBin(V1),isBin(V2)) isBin(prod(V1)) -> isBag(V1) isBin(sum(V1)) -> isBag(V1) multAC(z(),X) -> U11(isBin(X)) multAC(0(X),Y) -> U21(and(isBin(X),isBin(Y)),X,Y) multAC(1(X),Y) -> U31(and(isBin(X),isBin(Y)),X,Y) plusAC(z(),X) -> U41(isBin(X),X) plusAC(0(X),0(Y)) -> U51(and(isBin(X),isBin(Y)),X,Y) plusAC(0(X),1(Y)) -> U61(and(isBin(X),isBin(Y)),X,Y) plusAC(1(X),1(Y)) -> U71(and(isBin(X),isBin(Y)),X,Y) prod(empty()) -> 1(z()) prod(singl(X)) -> U81(isBin(X),X) prod(unionAC(A,B)) -> U91(and(isBag(A),isBag(B)),A,B) sum(empty()) -> 0(z()) sum(singl(X)) -> U101(isBin(X),X) sum(unionAC(A,B)) -> U111(and(isBag(A),isBag(B)),A,B) S: union{AC,#}(unionAC(x19,x20),x21) -> union{AC,#}(x19,x20) union{AC,#}(x19,unionAC(x20,x21)) -> union{AC,#}(x20,x21) plus{AC,#}(plusAC(x19,x20),x21) -> plus{AC,#}(x19,x20) plus{AC,#}(x19,plusAC(x20,x21)) -> plus{AC,#}(x20,x21) mult{AC,#}(multAC(x19,x20),x21) -> mult{AC,#}(x19,x20) mult{AC,#}(x19,multAC(x20,x21)) -> mult{AC,#}(x20,x21) AC-EDG Processor: Equations#: union{AC,#}(unionAC(x7,x8),x9) -> union{AC,#}(x7,unionAC(x8,x9)) union{AC,#}(x7,x8) -> union{AC,#}(x8,x7) plus{AC,#}(plusAC(x7,x8),x9) -> plus{AC,#}(x7,plusAC(x8,x9)) plus{AC,#}(x7,x8) -> plus{AC,#}(x8,x7) mult{AC,#}(multAC(x7,x8),x9) -> mult{AC,#}(x7,multAC(x8,x9)) mult{AC,#}(x7,x8) -> mult{AC,#}(x8,x7) union{AC,#}(x7,unionAC(x8,x9)) -> union{AC,#}(unionAC(x7,x8),x9) union{AC,#}(x8,x7) -> union{AC,#}(x7,x8) plus{AC,#}(x7,plusAC(x8,x9)) -> plus{AC,#}(plusAC(x7,x8),x9) plus{AC,#}(x8,x7) -> plus{AC,#}(x7,x8) mult{AC,#}(x7,multAC(x8,x9)) -> mult{AC,#}(multAC(x7,x8),x9) mult{AC,#}(x8,x7) -> mult{AC,#}(x7,x8) DPs: U111#(tt(),A,B) -> sum#(B) U111#(tt(),A,B) -> sum#(A) U111#(tt(),A,B) -> plus{AC,#}(sum(A),sum(B)) U21#(tt(),X,Y) -> mult{AC,#}(X,Y) U21#(tt(),X,Y) -> 0#(multAC(X,Y)) U31#(tt(),X,Y) -> mult{AC,#}(X,Y) U31#(tt(),X,Y) -> 0#(multAC(X,Y)) U31#(tt(),X,Y) -> plus{AC,#}(0(multAC(X,Y)),Y) U51#(tt(),X,Y) -> plus{AC,#}(X,Y) U51#(tt(),X,Y) -> 0#(plusAC(X,Y)) U61#(tt(),X,Y) -> plus{AC,#}(X,Y) U71#(tt(),X,Y) -> plus{AC,#}(X,Y) U71#(tt(),X,Y) -> plus{AC,#}(plusAC(X,Y),1(z())) U71#(tt(),X,Y) -> 0#(plusAC(plusAC(X,Y),1(z()))) U91#(tt(),A,B) -> prod#(B) U91#(tt(),A,B) -> prod#(A) U91#(tt(),A,B) -> mult{AC,#}(prod(A),prod(B)) isBag#(singl(V1)) -> isBin#(V1) isBag#(unionAC(V1,V2)) -> isBag#(V2) isBag#(unionAC(V1,V2)) -> isBag#(V1) isBag#(unionAC(V1,V2)) -> and#(isBag(V1),isBag(V2)) isBin#(0(V1)) -> isBin#(V1) isBin#(1(V1)) -> isBin#(V1) isBin#(multAC(V1,V2)) -> isBin#(V2) isBin#(multAC(V1,V2)) -> isBin#(V1) isBin#(multAC(V1,V2)) -> and#(isBin(V1),isBin(V2)) isBin#(plusAC(V1,V2)) -> isBin#(V2) isBin#(plusAC(V1,V2)) -> isBin#(V1) isBin#(plusAC(V1,V2)) -> and#(isBin(V1),isBin(V2)) isBin#(prod(V1)) -> isBag#(V1) isBin#(sum(V1)) -> isBag#(V1) mult{AC,#}(z(),X) -> isBin#(X) mult{AC,#}(z(),X) -> U11#(isBin(X)) mult{AC,#}(0(X),Y) -> isBin#(Y) mult{AC,#}(0(X),Y) -> isBin#(X) mult{AC,#}(0(X),Y) -> and#(isBin(X),isBin(Y)) mult{AC,#}(0(X),Y) -> U21#(and(isBin(X),isBin(Y)),X,Y) mult{AC,#}(1(X),Y) -> isBin#(Y) mult{AC,#}(1(X),Y) -> isBin#(X) mult{AC,#}(1(X),Y) -> and#(isBin(X),isBin(Y)) mult{AC,#}(1(X),Y) -> U31#(and(isBin(X),isBin(Y)),X,Y) plus{AC,#}(z(),X) -> isBin#(X) plus{AC,#}(z(),X) -> U41#(isBin(X),X) plus{AC,#}(0(X),0(Y)) -> isBin#(Y) plus{AC,#}(0(X),0(Y)) -> isBin#(X) plus{AC,#}(0(X),0(Y)) -> and#(isBin(X),isBin(Y)) plus{AC,#}(0(X),0(Y)) -> U51#(and(isBin(X),isBin(Y)),X,Y) plus{AC,#}(0(X),1(Y)) -> isBin#(Y) plus{AC,#}(0(X),1(Y)) -> isBin#(X) plus{AC,#}(0(X),1(Y)) -> and#(isBin(X),isBin(Y)) plus{AC,#}(0(X),1(Y)) -> U61#(and(isBin(X),isBin(Y)),X,Y) plus{AC,#}(1(X),1(Y)) -> isBin#(Y) plus{AC,#}(1(X),1(Y)) -> isBin#(X) plus{AC,#}(1(X),1(Y)) -> and#(isBin(X),isBin(Y)) plus{AC,#}(1(X),1(Y)) -> U71#(and(isBin(X),isBin(Y)),X,Y) prod#(singl(X)) -> isBin#(X) prod#(singl(X)) -> U81#(isBin(X),X) prod#(unionAC(A,B)) -> isBag#(B) prod#(unionAC(A,B)) -> isBag#(A) prod#(unionAC(A,B)) -> and#(isBag(A),isBag(B)) prod#(unionAC(A,B)) -> U91#(and(isBag(A),isBag(B)),A,B) sum#(empty()) -> 0#(z()) sum#(singl(X)) -> isBin#(X) sum#(singl(X)) -> U101#(isBin(X),X) sum#(unionAC(A,B)) -> isBag#(B) sum#(unionAC(A,B)) -> isBag#(A) sum#(unionAC(A,B)) -> and#(isBag(A),isBag(B)) sum#(unionAC(A,B)) -> U111#(and(isBag(A),isBag(B)),A,B) union{AC,#}(x10,unionAC(X,empty())) -> union{AC,#}(x10,X) union{AC,#}(x11,unionAC(empty(),X)) -> union{AC,#}(x11,X) mult{AC,#}(x12,multAC(z(),X)) -> isBin#(X) mult{AC,#}(x12,multAC(z(),X)) -> U11#(isBin(X)) mult{AC,#}(x12,multAC(z(),X)) -> mult{AC,#}(x12,U11(isBin(X))) mult{AC,#}(x13,multAC(0(X),Y)) -> isBin#(Y) mult{AC,#}(x13,multAC(0(X),Y)) -> isBin#(X) mult{AC,#}(x13,multAC(0(X),Y)) -> and#(isBin(X),isBin(Y)) mult{AC,#}(x13,multAC(0(X),Y)) -> U21#(and(isBin(X),isBin(Y)),X,Y) mult{AC,#}(x13,multAC(0(X),Y)) -> mult{AC,#}(x13,U21(and(isBin(X),isBin(Y)),X,Y)) mult{AC,#}(x14,multAC(1(X),Y)) -> isBin#(Y) mult{AC,#}(x14,multAC(1(X),Y)) -> isBin#(X) mult{AC,#}(x14,multAC(1(X),Y)) -> and#(isBin(X),isBin(Y)) mult{AC,#}(x14,multAC(1(X),Y)) -> U31#(and(isBin(X),isBin(Y)),X,Y) mult{AC,#}(x14,multAC(1(X),Y)) -> mult{AC,#}(x14,U31(and(isBin(X),isBin(Y)),X,Y)) plus{AC,#}(x15,plusAC(z(),X)) -> isBin#(X) plus{AC,#}(x15,plusAC(z(),X)) -> U41#(isBin(X),X) plus{AC,#}(x15,plusAC(z(),X)) -> plus{AC,#}(x15,U41(isBin(X),X)) plus{AC,#}(x16,plusAC(0(X),0(Y))) -> isBin#(Y) plus{AC,#}(x16,plusAC(0(X),0(Y))) -> isBin#(X) plus{AC,#}(x16,plusAC(0(X),0(Y))) -> and#(isBin(X),isBin(Y)) plus{AC,#}(x16,plusAC(0(X),0(Y))) -> U51#(and(isBin(X),isBin(Y)),X,Y) plus{AC,#}(x16,plusAC(0(X),0(Y))) -> plus{AC,#}(x16,U51(and(isBin(X),isBin(Y)),X,Y)) plus{AC,#}(x17,plusAC(0(X),1(Y))) -> isBin#(Y) plus{AC,#}(x17,plusAC(0(X),1(Y))) -> isBin#(X) plus{AC,#}(x17,plusAC(0(X),1(Y))) -> and#(isBin(X),isBin(Y)) plus{AC,#}(x17,plusAC(0(X),1(Y))) -> U61#(and(isBin(X),isBin(Y)),X,Y) plus{AC,#}(x17,plusAC(0(X),1(Y))) -> plus{AC,#}(x17,U61(and(isBin(X),isBin(Y)),X,Y)) plus{AC,#}(x18,plusAC(1(X),1(Y))) -> isBin#(Y) plus{AC,#}(x18,plusAC(1(X),1(Y))) -> isBin#(X) plus{AC,#}(x18,plusAC(1(X),1(Y))) -> and#(isBin(X),isBin(Y)) plus{AC,#}(x18,plusAC(1(X),1(Y))) -> U71#(and(isBin(X),isBin(Y)),X,Y) plus{AC,#}(x18,plusAC(1(X),1(Y))) -> plus{AC,#}(x18,U71(and(isBin(X),isBin(Y)),X,Y)) Equations: unionAC(unionAC(x7,x8),x9) -> unionAC(x7,unionAC(x8,x9)) unionAC(x7,x8) -> unionAC(x8,x7) plusAC(plusAC(x7,x8),x9) -> plusAC(x7,plusAC(x8,x9)) plusAC(x7,x8) -> plusAC(x8,x7) multAC(multAC(x7,x8),x9) -> multAC(x7,multAC(x8,x9)) multAC(x7,x8) -> multAC(x8,x7) unionAC(x7,unionAC(x8,x9)) -> unionAC(unionAC(x7,x8),x9) unionAC(x8,x7) -> unionAC(x7,x8) plusAC(x7,plusAC(x8,x9)) -> plusAC(plusAC(x7,x8),x9) plusAC(x8,x7) -> plusAC(x7,x8) multAC(x7,multAC(x8,x9)) -> multAC(multAC(x7,x8),x9) multAC(x8,x7) -> multAC(x7,x8) TRS: unionAC(X,empty()) -> X unionAC(empty(),X) -> X 0(z()) -> z() U101(tt(),X) -> X U11(tt()) -> z() U111(tt(),A,B) -> plusAC(sum(A),sum(B)) U21(tt(),X,Y) -> 0(multAC(X,Y)) U31(tt(),X,Y) -> plusAC(0(multAC(X,Y)),Y) U41(tt(),X) -> X U51(tt(),X,Y) -> 0(plusAC(X,Y)) U61(tt(),X,Y) -> 1(plusAC(X,Y)) U71(tt(),X,Y) -> 0(plusAC(plusAC(X,Y),1(z()))) U81(tt(),X) -> X U91(tt(),A,B) -> multAC(prod(A),prod(B)) and(tt(),X) -> X isBag(empty()) -> tt() isBag(singl(V1)) -> isBin(V1) isBag(unionAC(V1,V2)) -> and(isBag(V1),isBag(V2)) isBin(z()) -> tt() isBin(0(V1)) -> isBin(V1) isBin(1(V1)) -> isBin(V1) isBin(multAC(V1,V2)) -> and(isBin(V1),isBin(V2)) isBin(plusAC(V1,V2)) -> and(isBin(V1),isBin(V2)) isBin(prod(V1)) -> isBag(V1) isBin(sum(V1)) -> isBag(V1) multAC(z(),X) -> U11(isBin(X)) multAC(0(X),Y) -> U21(and(isBin(X),isBin(Y)),X,Y) multAC(1(X),Y) -> U31(and(isBin(X),isBin(Y)),X,Y) plusAC(z(),X) -> U41(isBin(X),X) plusAC(0(X),0(Y)) -> U51(and(isBin(X),isBin(Y)),X,Y) plusAC(0(X),1(Y)) -> U61(and(isBin(X),isBin(Y)),X,Y) plusAC(1(X),1(Y)) -> U71(and(isBin(X),isBin(Y)),X,Y) prod(empty()) -> 1(z()) prod(singl(X)) -> U81(isBin(X),X) prod(unionAC(A,B)) -> U91(and(isBag(A),isBag(B)),A,B) sum(empty()) -> 0(z()) sum(singl(X)) -> U101(isBin(X),X) sum(unionAC(A,B)) -> U111(and(isBag(A),isBag(B)),A,B) S: union{AC,#}(unionAC(x19,x20),x21) -> union{AC,#}(x19,x20) union{AC,#}(x19,unionAC(x20,x21)) -> union{AC,#}(x20,x21) plus{AC,#}(plusAC(x19,x20),x21) -> plus{AC,#}(x19,x20) plus{AC,#}(x19,plusAC(x20,x21)) -> plus{AC,#}(x20,x21) mult{AC,#}(multAC(x19,x20),x21) -> mult{AC,#}(x19,x20) mult{AC,#}(x19,multAC(x20,x21)) -> mult{AC,#}(x20,x21) Open