MAYBE Time: 31.987 Problem: Equations: unionAC(unionAC(x7,x8),x9) -> unionAC(x7,unionAC(x8,x9)) unionAC(x7,x8) -> unionAC(x8,x7) multAC(multAC(x7,x8),x9) -> multAC(x7,multAC(x8,x9)) multAC(x7,x8) -> multAC(x8,x7) plusAC(plusAC(x7,x8),x9) -> plusAC(x7,plusAC(x8,x9)) plusAC(x7,x8) -> plusAC(x8,x7) unionAC(x7,unionAC(x8,x9)) -> unionAC(unionAC(x7,x8),x9) unionAC(x8,x7) -> unionAC(x7,x8) multAC(x7,multAC(x8,x9)) -> multAC(multAC(x7,x8),x9) multAC(x8,x7) -> multAC(x7,x8) plusAC(x7,plusAC(x8,x9)) -> plusAC(plusAC(x7,x8),x9) plusAC(x8,x7) -> plusAC(x7,x8) TRS: unionAC(X,empty()) -> X unionAC(empty(),X) -> X 0(z()) -> z() U101(tt(),X,Y) -> 0(multAC(X,Y)) U11(tt(),V1) -> U12(isBin(V1)) U111(tt(),X,Y) -> plusAC(0(multAC(X,Y)),Y) U12(tt()) -> tt() U121(tt(),X) -> X U131(tt(),X,Y) -> 0(plusAC(X,Y)) U141(tt(),X,Y) -> 1(plusAC(X,Y)) U151(tt(),X,Y) -> 0(plusAC(plusAC(X,Y),1(z()))) U161(tt(),X) -> X U171(tt(),A,B) -> multAC(prod(A),prod(B)) U181(tt(),X) -> X U191(tt(),A,B) -> plusAC(sum(A),sum(B)) U21(tt(),V1,V2) -> U22(isBag(V1),V2) U22(tt(),V2) -> U23(isBag(V2)) U23(tt()) -> tt() U31(tt(),V1) -> U32(isBin(V1)) U32(tt()) -> tt() U41(tt(),V1) -> U42(isBin(V1)) U42(tt()) -> tt() U51(tt(),V1,V2) -> U52(isBin(V1),V2) U52(tt(),V2) -> U53(isBin(V2)) U53(tt()) -> tt() U61(tt(),V1,V2) -> U62(isBin(V1),V2) U62(tt(),V2) -> U63(isBin(V2)) U63(tt()) -> tt() U71(tt(),V1) -> U72(isBag(V1)) U72(tt()) -> tt() U81(tt(),V1) -> U82(isBag(V1)) U82(tt()) -> tt() U91(tt()) -> z() and(tt(),X) -> X isBag(empty()) -> tt() isBag(singl(V1)) -> U11(isBinKind(V1),V1) isBag(unionAC(V1,V2)) -> U21(and(isBagKind(V1),isBagKind(V2)),V1,V2) isBagKind(empty()) -> tt() isBagKind(singl(V1)) -> isBinKind(V1) isBagKind(unionAC(V1,V2)) -> and(isBagKind(V1),isBagKind(V2)) isBin(z()) -> tt() isBin(0(V1)) -> U31(isBinKind(V1),V1) isBin(1(V1)) -> U41(isBinKind(V1),V1) isBin(multAC(V1,V2)) -> U51(and(isBinKind(V1),isBinKind(V2)),V1,V2) isBin(plusAC(V1,V2)) -> U61(and(isBinKind(V1),isBinKind(V2)),V1,V2) isBin(prod(V1)) -> U71(isBagKind(V1),V1) isBin(sum(V1)) -> U81(isBagKind(V1),V1) isBinKind(z()) -> tt() isBinKind(0(V1)) -> isBinKind(V1) isBinKind(1(V1)) -> isBinKind(V1) isBinKind(multAC(V1,V2)) -> and(isBinKind(V1),isBinKind(V2)) isBinKind(plusAC(V1,V2)) -> and(isBinKind(V1),isBinKind(V2)) isBinKind(prod(V1)) -> isBagKind(V1) isBinKind(sum(V1)) -> isBagKind(V1) multAC(z(),X) -> U91(and(isBin(X),isBinKind(X))) multAC(0(X),Y) -> U101(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y) multAC(1(X),Y) -> U111(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y) plusAC(z(),X) -> U121(and(isBin(X),isBinKind(X)),X) plusAC(0(X),0(Y)) -> U131(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y) plusAC(0(X),1(Y)) -> U141(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y) plusAC(1(X),1(Y)) -> U151(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y) prod(empty()) -> 1(z()) prod(singl(X)) -> U161(and(isBin(X),isBinKind(X)),X) prod(unionAC(A,B)) -> U171(and(and(isBag(A),isBagKind(A)),and(isBag(B),isBagKind(B))),A,B) sum(empty()) -> 0(z()) sum(singl(X)) -> U181(and(isBin(X),isBinKind(X)),X) sum(unionAC(A,B)) -> U191(and(and(isBag(A),isBagKind(A)),and(isBag(B),isBagKind(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) mult{AC,#}(multAC(x7,x8),x9) -> mult{AC,#}(x7,multAC(x8,x9)) mult{AC,#}(x7,x8) -> mult{AC,#}(x8,x7) plus{AC,#}(plusAC(x7,x8),x9) -> plus{AC,#}(x7,plusAC(x8,x9)) plus{AC,#}(x7,x8) -> plus{AC,#}(x8,x7) union{AC,#}(x7,unionAC(x8,x9)) -> union{AC,#}(unionAC(x7,x8),x9) union{AC,#}(x8,x7) -> union{AC,#}(x7,x8) mult{AC,#}(x7,multAC(x8,x9)) -> mult{AC,#}(multAC(x7,x8),x9) mult{AC,#}(x8,x7) -> mult{AC,#}(x7,x8) plus{AC,#}(x7,plusAC(x8,x9)) -> plus{AC,#}(plusAC(x7,x8),x9) plus{AC,#}(x8,x7) -> plus{AC,#}(x7,x8) DPs: U101#(tt(),X,Y) -> mult{AC,#}(X,Y) U101#(tt(),X,Y) -> 0#(multAC(X,Y)) U11#(tt(),V1) -> isBin#(V1) U11#(tt(),V1) -> U12#(isBin(V1)) U111#(tt(),X,Y) -> mult{AC,#}(X,Y) U111#(tt(),X,Y) -> 0#(multAC(X,Y)) U111#(tt(),X,Y) -> plus{AC,#}(0(multAC(X,Y)),Y) U131#(tt(),X,Y) -> plus{AC,#}(X,Y) U131#(tt(),X,Y) -> 0#(plusAC(X,Y)) U141#(tt(),X,Y) -> plus{AC,#}(X,Y) U151#(tt(),X,Y) -> plus{AC,#}(X,Y) U151#(tt(),X,Y) -> plus{AC,#}(plusAC(X,Y),1(z())) U151#(tt(),X,Y) -> 0#(plusAC(plusAC(X,Y),1(z()))) U171#(tt(),A,B) -> prod#(B) U171#(tt(),A,B) -> prod#(A) U171#(tt(),A,B) -> mult{AC,#}(prod(A),prod(B)) U191#(tt(),A,B) -> sum#(B) U191#(tt(),A,B) -> sum#(A) U191#(tt(),A,B) -> plus{AC,#}(sum(A),sum(B)) U21#(tt(),V1,V2) -> isBag#(V1) U21#(tt(),V1,V2) -> U22#(isBag(V1),V2) U22#(tt(),V2) -> isBag#(V2) U22#(tt(),V2) -> U23#(isBag(V2)) U31#(tt(),V1) -> isBin#(V1) U31#(tt(),V1) -> U32#(isBin(V1)) U41#(tt(),V1) -> isBin#(V1) U41#(tt(),V1) -> U42#(isBin(V1)) U51#(tt(),V1,V2) -> isBin#(V1) U51#(tt(),V1,V2) -> U52#(isBin(V1),V2) U52#(tt(),V2) -> isBin#(V2) U52#(tt(),V2) -> U53#(isBin(V2)) U61#(tt(),V1,V2) -> isBin#(V1) U61#(tt(),V1,V2) -> U62#(isBin(V1),V2) U62#(tt(),V2) -> isBin#(V2) U62#(tt(),V2) -> U63#(isBin(V2)) U71#(tt(),V1) -> isBag#(V1) U71#(tt(),V1) -> U72#(isBag(V1)) U81#(tt(),V1) -> isBag#(V1) U81#(tt(),V1) -> U82#(isBag(V1)) isBag#(singl(V1)) -> isBinKind#(V1) isBag#(singl(V1)) -> U11#(isBinKind(V1),V1) isBag#(unionAC(V1,V2)) -> isBagKind#(V2) isBag#(unionAC(V1,V2)) -> isBagKind#(V1) isBag#(unionAC(V1,V2)) -> and#(isBagKind(V1),isBagKind(V2)) isBag#(unionAC(V1,V2)) -> U21#(and(isBagKind(V1),isBagKind(V2)),V1,V2) isBagKind#(singl(V1)) -> isBinKind#(V1) isBagKind#(unionAC(V1,V2)) -> isBagKind#(V2) isBagKind#(unionAC(V1,V2)) -> isBagKind#(V1) isBagKind#(unionAC(V1,V2)) -> and#(isBagKind(V1),isBagKind(V2)) isBin#(0(V1)) -> isBinKind#(V1) isBin#(0(V1)) -> U31#(isBinKind(V1),V1) isBin#(1(V1)) -> isBinKind#(V1) isBin#(1(V1)) -> U41#(isBinKind(V1),V1) isBin#(multAC(V1,V2)) -> isBinKind#(V2) isBin#(multAC(V1,V2)) -> isBinKind#(V1) isBin#(multAC(V1,V2)) -> and#(isBinKind(V1),isBinKind(V2)) isBin#(multAC(V1,V2)) -> U51#(and(isBinKind(V1),isBinKind(V2)),V1,V2) isBin#(plusAC(V1,V2)) -> isBinKind#(V2) isBin#(plusAC(V1,V2)) -> isBinKind#(V1) isBin#(plusAC(V1,V2)) -> and#(isBinKind(V1),isBinKind(V2)) isBin#(plusAC(V1,V2)) -> U61#(and(isBinKind(V1),isBinKind(V2)),V1,V2) isBin#(prod(V1)) -> isBagKind#(V1) isBin#(prod(V1)) -> U71#(isBagKind(V1),V1) isBin#(sum(V1)) -> isBagKind#(V1) isBin#(sum(V1)) -> U81#(isBagKind(V1),V1) isBinKind#(0(V1)) -> isBinKind#(V1) isBinKind#(1(V1)) -> isBinKind#(V1) isBinKind#(multAC(V1,V2)) -> isBinKind#(V2) isBinKind#(multAC(V1,V2)) -> isBinKind#(V1) isBinKind#(multAC(V1,V2)) -> and#(isBinKind(V1),isBinKind(V2)) isBinKind#(plusAC(V1,V2)) -> isBinKind#(V2) isBinKind#(plusAC(V1,V2)) -> isBinKind#(V1) isBinKind#(plusAC(V1,V2)) -> and#(isBinKind(V1),isBinKind(V2)) isBinKind#(prod(V1)) -> isBagKind#(V1) isBinKind#(sum(V1)) -> isBagKind#(V1) mult{AC,#}(z(),X) -> isBinKind#(X) mult{AC,#}(z(),X) -> isBin#(X) mult{AC,#}(z(),X) -> and#(isBin(X),isBinKind(X)) mult{AC,#}(z(),X) -> U91#(and(isBin(X),isBinKind(X))) mult{AC,#}(0(X),Y) -> isBinKind#(Y) mult{AC,#}(0(X),Y) -> isBin#(Y) mult{AC,#}(0(X),Y) -> and#(isBin(Y),isBinKind(Y)) mult{AC,#}(0(X),Y) -> isBinKind#(X) mult{AC,#}(0(X),Y) -> isBin#(X) mult{AC,#}(0(X),Y) -> and#(isBin(X),isBinKind(X)) mult{AC,#}(0(X),Y) -> and#(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))) mult{AC,#}(0(X),Y) -> U101#(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y) mult{AC,#}(1(X),Y) -> isBinKind#(Y) mult{AC,#}(1(X),Y) -> isBin#(Y) mult{AC,#}(1(X),Y) -> and#(isBin(Y),isBinKind(Y)) mult{AC,#}(1(X),Y) -> isBinKind#(X) mult{AC,#}(1(X),Y) -> isBin#(X) mult{AC,#}(1(X),Y) -> and#(isBin(X),isBinKind(X)) mult{AC,#}(1(X),Y) -> and#(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))) mult{AC,#}(1(X),Y) -> U111#(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y) plus{AC,#}(z(),X) -> isBinKind#(X) plus{AC,#}(z(),X) -> isBin#(X) plus{AC,#}(z(),X) -> and#(isBin(X),isBinKind(X)) plus{AC,#}(z(),X) -> U121#(and(isBin(X),isBinKind(X)),X) plus{AC,#}(0(X),0(Y)) -> isBinKind#(Y) plus{AC,#}(0(X),0(Y)) -> isBin#(Y) plus{AC,#}(0(X),0(Y)) -> and#(isBin(Y),isBinKind(Y)) plus{AC,#}(0(X),0(Y)) -> isBinKind#(X) plus{AC,#}(0(X),0(Y)) -> isBin#(X) plus{AC,#}(0(X),0(Y)) -> and#(isBin(X),isBinKind(X)) plus{AC,#}(0(X),0(Y)) -> and#(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))) plus{AC,#}(0(X),0(Y)) -> U131#(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y) plus{AC,#}(0(X),1(Y)) -> isBinKind#(Y) plus{AC,#}(0(X),1(Y)) -> isBin#(Y) plus{AC,#}(0(X),1(Y)) -> and#(isBin(Y),isBinKind(Y)) plus{AC,#}(0(X),1(Y)) -> isBinKind#(X) plus{AC,#}(0(X),1(Y)) -> isBin#(X) plus{AC,#}(0(X),1(Y)) -> and#(isBin(X),isBinKind(X)) plus{AC,#}(0(X),1(Y)) -> and#(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))) plus{AC,#}(0(X),1(Y)) -> U141#(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y) plus{AC,#}(1(X),1(Y)) -> isBinKind#(Y) plus{AC,#}(1(X),1(Y)) -> isBin#(Y) plus{AC,#}(1(X),1(Y)) -> and#(isBin(Y),isBinKind(Y)) plus{AC,#}(1(X),1(Y)) -> isBinKind#(X) plus{AC,#}(1(X),1(Y)) -> isBin#(X) plus{AC,#}(1(X),1(Y)) -> and#(isBin(X),isBinKind(X)) plus{AC,#}(1(X),1(Y)) -> and#(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))) plus{AC,#}(1(X),1(Y)) -> U151#(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y) prod#(singl(X)) -> isBinKind#(X) prod#(singl(X)) -> isBin#(X) prod#(singl(X)) -> and#(isBin(X),isBinKind(X)) prod#(singl(X)) -> U161#(and(isBin(X),isBinKind(X)),X) prod#(unionAC(A,B)) -> isBagKind#(B) prod#(unionAC(A,B)) -> isBag#(B) prod#(unionAC(A,B)) -> and#(isBag(B),isBagKind(B)) prod#(unionAC(A,B)) -> isBagKind#(A) prod#(unionAC(A,B)) -> isBag#(A) prod#(unionAC(A,B)) -> and#(isBag(A),isBagKind(A)) prod#(unionAC(A,B)) -> and#(and(isBag(A),isBagKind(A)),and(isBag(B),isBagKind(B))) prod#(unionAC(A,B)) -> U171#(and(and(isBag(A),isBagKind(A)),and(isBag(B),isBagKind(B))),A,B) sum#(empty()) -> 0#(z()) sum#(singl(X)) -> isBinKind#(X) sum#(singl(X)) -> isBin#(X) sum#(singl(X)) -> and#(isBin(X),isBinKind(X)) sum#(singl(X)) -> U181#(and(isBin(X),isBinKind(X)),X) sum#(unionAC(A,B)) -> isBagKind#(B) sum#(unionAC(A,B)) -> isBag#(B) sum#(unionAC(A,B)) -> and#(isBag(B),isBagKind(B)) sum#(unionAC(A,B)) -> isBagKind#(A) sum#(unionAC(A,B)) -> isBag#(A) sum#(unionAC(A,B)) -> and#(isBag(A),isBagKind(A)) sum#(unionAC(A,B)) -> and#(and(isBag(A),isBagKind(A)),and(isBag(B),isBagKind(B))) sum#(unionAC(A,B)) -> U191#(and(and(isBag(A),isBagKind(A)),and(isBag(B),isBagKind(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)) -> isBinKind#(X) mult{AC,#}(x12,multAC(z(),X)) -> isBin#(X) mult{AC,#}(x12,multAC(z(),X)) -> and#(isBin(X),isBinKind(X)) mult{AC,#}(x12,multAC(z(),X)) -> U91#(and(isBin(X),isBinKind(X))) mult{AC,#}(x12,multAC(z(),X)) -> mult{AC,#}(x12,U91(and(isBin(X),isBinKind(X)))) mult{AC,#}(x13,multAC(0(X),Y)) -> isBinKind#(Y) mult{AC,#}(x13,multAC(0(X),Y)) -> isBin#(Y) mult{AC,#}(x13,multAC(0(X),Y)) -> and#(isBin(Y),isBinKind(Y)) mult{AC,#}(x13,multAC(0(X),Y)) -> isBinKind#(X) mult{AC,#}(x13,multAC(0(X),Y)) -> isBin#(X) mult{AC,#}(x13,multAC(0(X),Y)) -> and#(isBin(X),isBinKind(X)) mult{AC,#}(x13,multAC(0(X),Y)) -> and#(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))) mult{AC,#}(x13,multAC(0(X),Y)) -> U101#(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y) mult{AC,#}(x13,multAC(0(X),Y)) -> mult{AC,#}(x13,U101(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)) mult{AC,#}(x14,multAC(1(X),Y)) -> isBinKind#(Y) mult{AC,#}(x14,multAC(1(X),Y)) -> isBin#(Y) mult{AC,#}(x14,multAC(1(X),Y)) -> and#(isBin(Y),isBinKind(Y)) mult{AC,#}(x14,multAC(1(X),Y)) -> isBinKind#(X) mult{AC,#}(x14,multAC(1(X),Y)) -> isBin#(X) mult{AC,#}(x14,multAC(1(X),Y)) -> and#(isBin(X),isBinKind(X)) mult{AC,#}(x14,multAC(1(X),Y)) -> and#(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))) mult{AC,#}(x14,multAC(1(X),Y)) -> U111#(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y) mult{AC,#}(x14,multAC(1(X),Y)) -> mult{AC,#}(x14,U111(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)) plus{AC,#}(x15,plusAC(z(),X)) -> isBinKind#(X) plus{AC,#}(x15,plusAC(z(),X)) -> isBin#(X) plus{AC,#}(x15,plusAC(z(),X)) -> and#(isBin(X),isBinKind(X)) plus{AC,#}(x15,plusAC(z(),X)) -> U121#(and(isBin(X),isBinKind(X)),X) plus{AC,#}(x15,plusAC(z(),X)) -> plus{AC,#}(x15,U121(and(isBin(X),isBinKind(X)),X)) plus{AC,#}(x16,plusAC(0(X),0(Y))) -> isBinKind#(Y) plus{AC,#}(x16,plusAC(0(X),0(Y))) -> isBin#(Y) plus{AC,#}(x16,plusAC(0(X),0(Y))) -> and#(isBin(Y),isBinKind(Y)) plus{AC,#}(x16,plusAC(0(X),0(Y))) -> isBinKind#(X) plus{AC,#}(x16,plusAC(0(X),0(Y))) -> isBin#(X) plus{AC,#}(x16,plusAC(0(X),0(Y))) -> and#(isBin(X),isBinKind(X)) plus{AC,#}(x16,plusAC(0(X),0(Y))) -> and#(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))) plus{AC,#}(x16,plusAC(0(X),0(Y))) -> U131#(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y) plus{AC,#}(x16,plusAC(0(X),0(Y))) -> plus{AC,#}(x16,U131(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)) plus{AC,#}(x17,plusAC(0(X),1(Y))) -> isBinKind#(Y) plus{AC,#}(x17,plusAC(0(X),1(Y))) -> isBin#(Y) plus{AC,#}(x17,plusAC(0(X),1(Y))) -> and#(isBin(Y),isBinKind(Y)) plus{AC,#}(x17,plusAC(0(X),1(Y))) -> isBinKind#(X) plus{AC,#}(x17,plusAC(0(X),1(Y))) -> isBin#(X) plus{AC,#}(x17,plusAC(0(X),1(Y))) -> and#(isBin(X),isBinKind(X)) plus{AC,#}(x17,plusAC(0(X),1(Y))) -> and#(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))) plus{AC,#}(x17,plusAC(0(X),1(Y))) -> U141#(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y) plus{AC,#}(x17,plusAC(0(X),1(Y))) -> plus{AC,#}(x17,U141(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)) plus{AC,#}(x18,plusAC(1(X),1(Y))) -> isBinKind#(Y) plus{AC,#}(x18,plusAC(1(X),1(Y))) -> isBin#(Y) plus{AC,#}(x18,plusAC(1(X),1(Y))) -> and#(isBin(Y),isBinKind(Y)) plus{AC,#}(x18,plusAC(1(X),1(Y))) -> isBinKind#(X) plus{AC,#}(x18,plusAC(1(X),1(Y))) -> isBin#(X) plus{AC,#}(x18,plusAC(1(X),1(Y))) -> and#(isBin(X),isBinKind(X)) plus{AC,#}(x18,plusAC(1(X),1(Y))) -> and#(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))) plus{AC,#}(x18,plusAC(1(X),1(Y))) -> U151#(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y) plus{AC,#}(x18,plusAC(1(X),1(Y))) -> plus{AC,#}(x18,U151(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)) Equations: unionAC(unionAC(x7,x8),x9) -> unionAC(x7,unionAC(x8,x9)) unionAC(x7,x8) -> unionAC(x8,x7) multAC(multAC(x7,x8),x9) -> multAC(x7,multAC(x8,x9)) multAC(x7,x8) -> multAC(x8,x7) plusAC(plusAC(x7,x8),x9) -> plusAC(x7,plusAC(x8,x9)) plusAC(x7,x8) -> plusAC(x8,x7) unionAC(x7,unionAC(x8,x9)) -> unionAC(unionAC(x7,x8),x9) unionAC(x8,x7) -> unionAC(x7,x8) multAC(x7,multAC(x8,x9)) -> multAC(multAC(x7,x8),x9) multAC(x8,x7) -> multAC(x7,x8) plusAC(x7,plusAC(x8,x9)) -> plusAC(plusAC(x7,x8),x9) plusAC(x8,x7) -> plusAC(x7,x8) TRS: unionAC(X,empty()) -> X unionAC(empty(),X) -> X 0(z()) -> z() U101(tt(),X,Y) -> 0(multAC(X,Y)) U11(tt(),V1) -> U12(isBin(V1)) U111(tt(),X,Y) -> plusAC(0(multAC(X,Y)),Y) U12(tt()) -> tt() U121(tt(),X) -> X U131(tt(),X,Y) -> 0(plusAC(X,Y)) U141(tt(),X,Y) -> 1(plusAC(X,Y)) U151(tt(),X,Y) -> 0(plusAC(plusAC(X,Y),1(z()))) U161(tt(),X) -> X U171(tt(),A,B) -> multAC(prod(A),prod(B)) U181(tt(),X) -> X U191(tt(),A,B) -> plusAC(sum(A),sum(B)) U21(tt(),V1,V2) -> U22(isBag(V1),V2) U22(tt(),V2) -> U23(isBag(V2)) U23(tt()) -> tt() U31(tt(),V1) -> U32(isBin(V1)) U32(tt()) -> tt() U41(tt(),V1) -> U42(isBin(V1)) U42(tt()) -> tt() U51(tt(),V1,V2) -> U52(isBin(V1),V2) U52(tt(),V2) -> U53(isBin(V2)) U53(tt()) -> tt() U61(tt(),V1,V2) -> U62(isBin(V1),V2) U62(tt(),V2) -> U63(isBin(V2)) U63(tt()) -> tt() U71(tt(),V1) -> U72(isBag(V1)) U72(tt()) -> tt() U81(tt(),V1) -> U82(isBag(V1)) U82(tt()) -> tt() U91(tt()) -> z() and(tt(),X) -> X isBag(empty()) -> tt() isBag(singl(V1)) -> U11(isBinKind(V1),V1) isBag(unionAC(V1,V2)) -> U21(and(isBagKind(V1),isBagKind(V2)),V1,V2) isBagKind(empty()) -> tt() isBagKind(singl(V1)) -> isBinKind(V1) isBagKind(unionAC(V1,V2)) -> and(isBagKind(V1),isBagKind(V2)) isBin(z()) -> tt() isBin(0(V1)) -> U31(isBinKind(V1),V1) isBin(1(V1)) -> U41(isBinKind(V1),V1) isBin(multAC(V1,V2)) -> U51(and(isBinKind(V1),isBinKind(V2)),V1,V2) isBin(plusAC(V1,V2)) -> U61(and(isBinKind(V1),isBinKind(V2)),V1,V2) isBin(prod(V1)) -> U71(isBagKind(V1),V1) isBin(sum(V1)) -> U81(isBagKind(V1),V1) isBinKind(z()) -> tt() isBinKind(0(V1)) -> isBinKind(V1) isBinKind(1(V1)) -> isBinKind(V1) isBinKind(multAC(V1,V2)) -> and(isBinKind(V1),isBinKind(V2)) isBinKind(plusAC(V1,V2)) -> and(isBinKind(V1),isBinKind(V2)) isBinKind(prod(V1)) -> isBagKind(V1) isBinKind(sum(V1)) -> isBagKind(V1) multAC(z(),X) -> U91(and(isBin(X),isBinKind(X))) multAC(0(X),Y) -> U101(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y) multAC(1(X),Y) -> U111(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y) plusAC(z(),X) -> U121(and(isBin(X),isBinKind(X)),X) plusAC(0(X),0(Y)) -> U131(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y) plusAC(0(X),1(Y)) -> U141(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y) plusAC(1(X),1(Y)) -> U151(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y) prod(empty()) -> 1(z()) prod(singl(X)) -> U161(and(isBin(X),isBinKind(X)),X) prod(unionAC(A,B)) -> U171(and(and(isBag(A),isBagKind(A)),and(isBag(B),isBagKind(B))),A,B) sum(empty()) -> 0(z()) sum(singl(X)) -> U181(and(isBin(X),isBinKind(X)),X) sum(unionAC(A,B)) -> U191(and(and(isBag(A),isBagKind(A)),and(isBag(B),isBagKind(B))),A,B) S: union{AC,#}(unionAC(x19,x20),x21) -> union{AC,#}(x19,x20) union{AC,#}(x19,unionAC(x20,x21)) -> union{AC,#}(x20,x21) mult{AC,#}(multAC(x19,x20),x21) -> mult{AC,#}(x19,x20) mult{AC,#}(x19,multAC(x20,x21)) -> mult{AC,#}(x20,x21) plus{AC,#}(plusAC(x19,x20),x21) -> plus{AC,#}(x19,x20) plus{AC,#}(x19,plusAC(x20,x21)) -> plus{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) mult{AC,#}(multAC(x7,x8),x9) -> mult{AC,#}(x7,multAC(x8,x9)) mult{AC,#}(x7,x8) -> mult{AC,#}(x8,x7) plus{AC,#}(plusAC(x7,x8),x9) -> plus{AC,#}(x7,plusAC(x8,x9)) plus{AC,#}(x7,x8) -> plus{AC,#}(x8,x7) union{AC,#}(x7,unionAC(x8,x9)) -> union{AC,#}(unionAC(x7,x8),x9) union{AC,#}(x8,x7) -> union{AC,#}(x7,x8) mult{AC,#}(x7,multAC(x8,x9)) -> mult{AC,#}(multAC(x7,x8),x9) mult{AC,#}(x8,x7) -> mult{AC,#}(x7,x8) plus{AC,#}(x7,plusAC(x8,x9)) -> plus{AC,#}(plusAC(x7,x8),x9) plus{AC,#}(x8,x7) -> plus{AC,#}(x7,x8) DPs: U101#(tt(),X,Y) -> mult{AC,#}(X,Y) U101#(tt(),X,Y) -> 0#(multAC(X,Y)) U11#(tt(),V1) -> isBin#(V1) U11#(tt(),V1) -> U12#(isBin(V1)) U111#(tt(),X,Y) -> mult{AC,#}(X,Y) U111#(tt(),X,Y) -> 0#(multAC(X,Y)) U111#(tt(),X,Y) -> plus{AC,#}(0(multAC(X,Y)),Y) U131#(tt(),X,Y) -> plus{AC,#}(X,Y) U131#(tt(),X,Y) -> 0#(plusAC(X,Y)) U141#(tt(),X,Y) -> plus{AC,#}(X,Y) U151#(tt(),X,Y) -> plus{AC,#}(X,Y) U151#(tt(),X,Y) -> plus{AC,#}(plusAC(X,Y),1(z())) U151#(tt(),X,Y) -> 0#(plusAC(plusAC(X,Y),1(z()))) U171#(tt(),A,B) -> prod#(B) U171#(tt(),A,B) -> prod#(A) U171#(tt(),A,B) -> mult{AC,#}(prod(A),prod(B)) U191#(tt(),A,B) -> sum#(B) U191#(tt(),A,B) -> sum#(A) U191#(tt(),A,B) -> plus{AC,#}(sum(A),sum(B)) U21#(tt(),V1,V2) -> isBag#(V1) U21#(tt(),V1,V2) -> U22#(isBag(V1),V2) U22#(tt(),V2) -> isBag#(V2) U22#(tt(),V2) -> U23#(isBag(V2)) U31#(tt(),V1) -> isBin#(V1) U31#(tt(),V1) -> U32#(isBin(V1)) U41#(tt(),V1) -> isBin#(V1) U41#(tt(),V1) -> U42#(isBin(V1)) U51#(tt(),V1,V2) -> isBin#(V1) U51#(tt(),V1,V2) -> U52#(isBin(V1),V2) U52#(tt(),V2) -> isBin#(V2) U52#(tt(),V2) -> U53#(isBin(V2)) U61#(tt(),V1,V2) -> isBin#(V1) U61#(tt(),V1,V2) -> U62#(isBin(V1),V2) U62#(tt(),V2) -> isBin#(V2) U62#(tt(),V2) -> U63#(isBin(V2)) U71#(tt(),V1) -> isBag#(V1) U71#(tt(),V1) -> U72#(isBag(V1)) U81#(tt(),V1) -> isBag#(V1) U81#(tt(),V1) -> U82#(isBag(V1)) isBag#(singl(V1)) -> isBinKind#(V1) isBag#(singl(V1)) -> U11#(isBinKind(V1),V1) isBag#(unionAC(V1,V2)) -> isBagKind#(V2) isBag#(unionAC(V1,V2)) -> isBagKind#(V1) isBag#(unionAC(V1,V2)) -> and#(isBagKind(V1),isBagKind(V2)) isBag#(unionAC(V1,V2)) -> U21#(and(isBagKind(V1),isBagKind(V2)),V1,V2) isBagKind#(singl(V1)) -> isBinKind#(V1) isBagKind#(unionAC(V1,V2)) -> isBagKind#(V2) isBagKind#(unionAC(V1,V2)) -> isBagKind#(V1) isBagKind#(unionAC(V1,V2)) -> and#(isBagKind(V1),isBagKind(V2)) isBin#(0(V1)) -> isBinKind#(V1) isBin#(0(V1)) -> U31#(isBinKind(V1),V1) isBin#(1(V1)) -> isBinKind#(V1) isBin#(1(V1)) -> U41#(isBinKind(V1),V1) isBin#(multAC(V1,V2)) -> isBinKind#(V2) isBin#(multAC(V1,V2)) -> isBinKind#(V1) isBin#(multAC(V1,V2)) -> and#(isBinKind(V1),isBinKind(V2)) isBin#(multAC(V1,V2)) -> U51#(and(isBinKind(V1),isBinKind(V2)),V1,V2) isBin#(plusAC(V1,V2)) -> isBinKind#(V2) isBin#(plusAC(V1,V2)) -> isBinKind#(V1) isBin#(plusAC(V1,V2)) -> and#(isBinKind(V1),isBinKind(V2)) isBin#(plusAC(V1,V2)) -> U61#(and(isBinKind(V1),isBinKind(V2)),V1,V2) isBin#(prod(V1)) -> isBagKind#(V1) isBin#(prod(V1)) -> U71#(isBagKind(V1),V1) isBin#(sum(V1)) -> isBagKind#(V1) isBin#(sum(V1)) -> U81#(isBagKind(V1),V1) isBinKind#(0(V1)) -> isBinKind#(V1) isBinKind#(1(V1)) -> isBinKind#(V1) isBinKind#(multAC(V1,V2)) -> isBinKind#(V2) isBinKind#(multAC(V1,V2)) -> isBinKind#(V1) isBinKind#(multAC(V1,V2)) -> and#(isBinKind(V1),isBinKind(V2)) isBinKind#(plusAC(V1,V2)) -> isBinKind#(V2) isBinKind#(plusAC(V1,V2)) -> isBinKind#(V1) isBinKind#(plusAC(V1,V2)) -> and#(isBinKind(V1),isBinKind(V2)) isBinKind#(prod(V1)) -> isBagKind#(V1) isBinKind#(sum(V1)) -> isBagKind#(V1) mult{AC,#}(z(),X) -> isBinKind#(X) mult{AC,#}(z(),X) -> isBin#(X) mult{AC,#}(z(),X) -> and#(isBin(X),isBinKind(X)) mult{AC,#}(z(),X) -> U91#(and(isBin(X),isBinKind(X))) mult{AC,#}(0(X),Y) -> isBinKind#(Y) mult{AC,#}(0(X),Y) -> isBin#(Y) mult{AC,#}(0(X),Y) -> and#(isBin(Y),isBinKind(Y)) mult{AC,#}(0(X),Y) -> isBinKind#(X) mult{AC,#}(0(X),Y) -> isBin#(X) mult{AC,#}(0(X),Y) -> and#(isBin(X),isBinKind(X)) mult{AC,#}(0(X),Y) -> and#(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))) mult{AC,#}(0(X),Y) -> U101#(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y) mult{AC,#}(1(X),Y) -> isBinKind#(Y) mult{AC,#}(1(X),Y) -> isBin#(Y) mult{AC,#}(1(X),Y) -> and#(isBin(Y),isBinKind(Y)) mult{AC,#}(1(X),Y) -> isBinKind#(X) mult{AC,#}(1(X),Y) -> isBin#(X) mult{AC,#}(1(X),Y) -> and#(isBin(X),isBinKind(X)) mult{AC,#}(1(X),Y) -> and#(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))) mult{AC,#}(1(X),Y) -> U111#(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y) plus{AC,#}(z(),X) -> isBinKind#(X) plus{AC,#}(z(),X) -> isBin#(X) plus{AC,#}(z(),X) -> and#(isBin(X),isBinKind(X)) plus{AC,#}(z(),X) -> U121#(and(isBin(X),isBinKind(X)),X) plus{AC,#}(0(X),0(Y)) -> isBinKind#(Y) plus{AC,#}(0(X),0(Y)) -> isBin#(Y) plus{AC,#}(0(X),0(Y)) -> and#(isBin(Y),isBinKind(Y)) plus{AC,#}(0(X),0(Y)) -> isBinKind#(X) plus{AC,#}(0(X),0(Y)) -> isBin#(X) plus{AC,#}(0(X),0(Y)) -> and#(isBin(X),isBinKind(X)) plus{AC,#}(0(X),0(Y)) -> and#(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))) plus{AC,#}(0(X),0(Y)) -> U131#(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y) plus{AC,#}(0(X),1(Y)) -> isBinKind#(Y) plus{AC,#}(0(X),1(Y)) -> isBin#(Y) plus{AC,#}(0(X),1(Y)) -> and#(isBin(Y),isBinKind(Y)) plus{AC,#}(0(X),1(Y)) -> isBinKind#(X) plus{AC,#}(0(X),1(Y)) -> isBin#(X) plus{AC,#}(0(X),1(Y)) -> and#(isBin(X),isBinKind(X)) plus{AC,#}(0(X),1(Y)) -> and#(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))) plus{AC,#}(0(X),1(Y)) -> U141#(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y) plus{AC,#}(1(X),1(Y)) -> isBinKind#(Y) plus{AC,#}(1(X),1(Y)) -> isBin#(Y) plus{AC,#}(1(X),1(Y)) -> and#(isBin(Y),isBinKind(Y)) plus{AC,#}(1(X),1(Y)) -> isBinKind#(X) plus{AC,#}(1(X),1(Y)) -> isBin#(X) plus{AC,#}(1(X),1(Y)) -> and#(isBin(X),isBinKind(X)) plus{AC,#}(1(X),1(Y)) -> and#(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))) plus{AC,#}(1(X),1(Y)) -> U151#(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y) prod#(singl(X)) -> isBinKind#(X) prod#(singl(X)) -> isBin#(X) prod#(singl(X)) -> and#(isBin(X),isBinKind(X)) prod#(singl(X)) -> U161#(and(isBin(X),isBinKind(X)),X) prod#(unionAC(A,B)) -> isBagKind#(B) prod#(unionAC(A,B)) -> isBag#(B) prod#(unionAC(A,B)) -> and#(isBag(B),isBagKind(B)) prod#(unionAC(A,B)) -> isBagKind#(A) prod#(unionAC(A,B)) -> isBag#(A) prod#(unionAC(A,B)) -> and#(isBag(A),isBagKind(A)) prod#(unionAC(A,B)) -> and#(and(isBag(A),isBagKind(A)),and(isBag(B),isBagKind(B))) prod#(unionAC(A,B)) -> U171#(and(and(isBag(A),isBagKind(A)),and(isBag(B),isBagKind(B))),A,B) sum#(empty()) -> 0#(z()) sum#(singl(X)) -> isBinKind#(X) sum#(singl(X)) -> isBin#(X) sum#(singl(X)) -> and#(isBin(X),isBinKind(X)) sum#(singl(X)) -> U181#(and(isBin(X),isBinKind(X)),X) sum#(unionAC(A,B)) -> isBagKind#(B) sum#(unionAC(A,B)) -> isBag#(B) sum#(unionAC(A,B)) -> and#(isBag(B),isBagKind(B)) sum#(unionAC(A,B)) -> isBagKind#(A) sum#(unionAC(A,B)) -> isBag#(A) sum#(unionAC(A,B)) -> and#(isBag(A),isBagKind(A)) sum#(unionAC(A,B)) -> and#(and(isBag(A),isBagKind(A)),and(isBag(B),isBagKind(B))) sum#(unionAC(A,B)) -> U191#(and(and(isBag(A),isBagKind(A)),and(isBag(B),isBagKind(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)) -> isBinKind#(X) mult{AC,#}(x12,multAC(z(),X)) -> isBin#(X) mult{AC,#}(x12,multAC(z(),X)) -> and#(isBin(X),isBinKind(X)) mult{AC,#}(x12,multAC(z(),X)) -> U91#(and(isBin(X),isBinKind(X))) mult{AC,#}(x12,multAC(z(),X)) -> mult{AC,#}(x12,U91(and(isBin(X),isBinKind(X)))) mult{AC,#}(x13,multAC(0(X),Y)) -> isBinKind#(Y) mult{AC,#}(x13,multAC(0(X),Y)) -> isBin#(Y) mult{AC,#}(x13,multAC(0(X),Y)) -> and#(isBin(Y),isBinKind(Y)) mult{AC,#}(x13,multAC(0(X),Y)) -> isBinKind#(X) mult{AC,#}(x13,multAC(0(X),Y)) -> isBin#(X) mult{AC,#}(x13,multAC(0(X),Y)) -> and#(isBin(X),isBinKind(X)) mult{AC,#}(x13,multAC(0(X),Y)) -> and#(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))) mult{AC,#}(x13,multAC(0(X),Y)) -> U101#(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y) mult{AC,#}(x13,multAC(0(X),Y)) -> mult{AC,#}(x13,U101(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)) mult{AC,#}(x14,multAC(1(X),Y)) -> isBinKind#(Y) mult{AC,#}(x14,multAC(1(X),Y)) -> isBin#(Y) mult{AC,#}(x14,multAC(1(X),Y)) -> and#(isBin(Y),isBinKind(Y)) mult{AC,#}(x14,multAC(1(X),Y)) -> isBinKind#(X) mult{AC,#}(x14,multAC(1(X),Y)) -> isBin#(X) mult{AC,#}(x14,multAC(1(X),Y)) -> and#(isBin(X),isBinKind(X)) mult{AC,#}(x14,multAC(1(X),Y)) -> and#(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))) mult{AC,#}(x14,multAC(1(X),Y)) -> U111#(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y) mult{AC,#}(x14,multAC(1(X),Y)) -> mult{AC,#}(x14,U111(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)) plus{AC,#}(x15,plusAC(z(),X)) -> isBinKind#(X) plus{AC,#}(x15,plusAC(z(),X)) -> isBin#(X) plus{AC,#}(x15,plusAC(z(),X)) -> and#(isBin(X),isBinKind(X)) plus{AC,#}(x15,plusAC(z(),X)) -> U121#(and(isBin(X),isBinKind(X)),X) plus{AC,#}(x15,plusAC(z(),X)) -> plus{AC,#}(x15,U121(and(isBin(X),isBinKind(X)),X)) plus{AC,#}(x16,plusAC(0(X),0(Y))) -> isBinKind#(Y) plus{AC,#}(x16,plusAC(0(X),0(Y))) -> isBin#(Y) plus{AC,#}(x16,plusAC(0(X),0(Y))) -> and#(isBin(Y),isBinKind(Y)) plus{AC,#}(x16,plusAC(0(X),0(Y))) -> isBinKind#(X) plus{AC,#}(x16,plusAC(0(X),0(Y))) -> isBin#(X) plus{AC,#}(x16,plusAC(0(X),0(Y))) -> and#(isBin(X),isBinKind(X)) plus{AC,#}(x16,plusAC(0(X),0(Y))) -> and#(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))) plus{AC,#}(x16,plusAC(0(X),0(Y))) -> U131#(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y) plus{AC,#}(x16,plusAC(0(X),0(Y))) -> plus{AC,#}(x16,U131(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)) plus{AC,#}(x17,plusAC(0(X),1(Y))) -> isBinKind#(Y) plus{AC,#}(x17,plusAC(0(X),1(Y))) -> isBin#(Y) plus{AC,#}(x17,plusAC(0(X),1(Y))) -> and#(isBin(Y),isBinKind(Y)) plus{AC,#}(x17,plusAC(0(X),1(Y))) -> isBinKind#(X) plus{AC,#}(x17,plusAC(0(X),1(Y))) -> isBin#(X) plus{AC,#}(x17,plusAC(0(X),1(Y))) -> and#(isBin(X),isBinKind(X)) plus{AC,#}(x17,plusAC(0(X),1(Y))) -> and#(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))) plus{AC,#}(x17,plusAC(0(X),1(Y))) -> U141#(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y) plus{AC,#}(x17,plusAC(0(X),1(Y))) -> plus{AC,#}(x17,U141(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)) plus{AC,#}(x18,plusAC(1(X),1(Y))) -> isBinKind#(Y) plus{AC,#}(x18,plusAC(1(X),1(Y))) -> isBin#(Y) plus{AC,#}(x18,plusAC(1(X),1(Y))) -> and#(isBin(Y),isBinKind(Y)) plus{AC,#}(x18,plusAC(1(X),1(Y))) -> isBinKind#(X) plus{AC,#}(x18,plusAC(1(X),1(Y))) -> isBin#(X) plus{AC,#}(x18,plusAC(1(X),1(Y))) -> and#(isBin(X),isBinKind(X)) plus{AC,#}(x18,plusAC(1(X),1(Y))) -> and#(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))) plus{AC,#}(x18,plusAC(1(X),1(Y))) -> U151#(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y) plus{AC,#}(x18,plusAC(1(X),1(Y))) -> plus{AC,#}(x18,U151(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)) Equations: unionAC(unionAC(x7,x8),x9) -> unionAC(x7,unionAC(x8,x9)) unionAC(x7,x8) -> unionAC(x8,x7) multAC(multAC(x7,x8),x9) -> multAC(x7,multAC(x8,x9)) multAC(x7,x8) -> multAC(x8,x7) plusAC(plusAC(x7,x8),x9) -> plusAC(x7,plusAC(x8,x9)) plusAC(x7,x8) -> plusAC(x8,x7) unionAC(x7,unionAC(x8,x9)) -> unionAC(unionAC(x7,x8),x9) unionAC(x8,x7) -> unionAC(x7,x8) multAC(x7,multAC(x8,x9)) -> multAC(multAC(x7,x8),x9) multAC(x8,x7) -> multAC(x7,x8) plusAC(x7,plusAC(x8,x9)) -> plusAC(plusAC(x7,x8),x9) plusAC(x8,x7) -> plusAC(x7,x8) TRS: unionAC(X,empty()) -> X unionAC(empty(),X) -> X 0(z()) -> z() U101(tt(),X,Y) -> 0(multAC(X,Y)) U11(tt(),V1) -> U12(isBin(V1)) U111(tt(),X,Y) -> plusAC(0(multAC(X,Y)),Y) U12(tt()) -> tt() U121(tt(),X) -> X U131(tt(),X,Y) -> 0(plusAC(X,Y)) U141(tt(),X,Y) -> 1(plusAC(X,Y)) U151(tt(),X,Y) -> 0(plusAC(plusAC(X,Y),1(z()))) U161(tt(),X) -> X U171(tt(),A,B) -> multAC(prod(A),prod(B)) U181(tt(),X) -> X U191(tt(),A,B) -> plusAC(sum(A),sum(B)) U21(tt(),V1,V2) -> U22(isBag(V1),V2) U22(tt(),V2) -> U23(isBag(V2)) U23(tt()) -> tt() U31(tt(),V1) -> U32(isBin(V1)) U32(tt()) -> tt() U41(tt(),V1) -> U42(isBin(V1)) U42(tt()) -> tt() U51(tt(),V1,V2) -> U52(isBin(V1),V2) U52(tt(),V2) -> U53(isBin(V2)) U53(tt()) -> tt() U61(tt(),V1,V2) -> U62(isBin(V1),V2) U62(tt(),V2) -> U63(isBin(V2)) U63(tt()) -> tt() U71(tt(),V1) -> U72(isBag(V1)) U72(tt()) -> tt() U81(tt(),V1) -> U82(isBag(V1)) U82(tt()) -> tt() U91(tt()) -> z() and(tt(),X) -> X isBag(empty()) -> tt() isBag(singl(V1)) -> U11(isBinKind(V1),V1) isBag(unionAC(V1,V2)) -> U21(and(isBagKind(V1),isBagKind(V2)),V1,V2) isBagKind(empty()) -> tt() isBagKind(singl(V1)) -> isBinKind(V1) isBagKind(unionAC(V1,V2)) -> and(isBagKind(V1),isBagKind(V2)) isBin(z()) -> tt() isBin(0(V1)) -> U31(isBinKind(V1),V1) isBin(1(V1)) -> U41(isBinKind(V1),V1) isBin(multAC(V1,V2)) -> U51(and(isBinKind(V1),isBinKind(V2)),V1,V2) isBin(plusAC(V1,V2)) -> U61(and(isBinKind(V1),isBinKind(V2)),V1,V2) isBin(prod(V1)) -> U71(isBagKind(V1),V1) isBin(sum(V1)) -> U81(isBagKind(V1),V1) isBinKind(z()) -> tt() isBinKind(0(V1)) -> isBinKind(V1) isBinKind(1(V1)) -> isBinKind(V1) isBinKind(multAC(V1,V2)) -> and(isBinKind(V1),isBinKind(V2)) isBinKind(plusAC(V1,V2)) -> and(isBinKind(V1),isBinKind(V2)) isBinKind(prod(V1)) -> isBagKind(V1) isBinKind(sum(V1)) -> isBagKind(V1) multAC(z(),X) -> U91(and(isBin(X),isBinKind(X))) multAC(0(X),Y) -> U101(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y) multAC(1(X),Y) -> U111(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y) plusAC(z(),X) -> U121(and(isBin(X),isBinKind(X)),X) plusAC(0(X),0(Y)) -> U131(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y) plusAC(0(X),1(Y)) -> U141(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y) plusAC(1(X),1(Y)) -> U151(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y) prod(empty()) -> 1(z()) prod(singl(X)) -> U161(and(isBin(X),isBinKind(X)),X) prod(unionAC(A,B)) -> U171(and(and(isBag(A),isBagKind(A)),and(isBag(B),isBagKind(B))),A,B) sum(empty()) -> 0(z()) sum(singl(X)) -> U181(and(isBin(X),isBinKind(X)),X) sum(unionAC(A,B)) -> U191(and(and(isBag(A),isBagKind(A)),and(isBag(B),isBagKind(B))),A,B) S: union{AC,#}(unionAC(x19,x20),x21) -> union{AC,#}(x19,x20) union{AC,#}(x19,unionAC(x20,x21)) -> union{AC,#}(x20,x21) mult{AC,#}(multAC(x19,x20),x21) -> mult{AC,#}(x19,x20) mult{AC,#}(x19,multAC(x20,x21)) -> mult{AC,#}(x20,x21) plus{AC,#}(plusAC(x19,x20),x21) -> plus{AC,#}(x19,x20) plus{AC,#}(x19,plusAC(x20,x21)) -> plus{AC,#}(x20,x21) Open