MAYBE Time: 25.402 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(),V1) -> U102(isBagKind(V1),V1) U102(tt(),V1) -> U103(isBag(V1)) U103(tt()) -> tt() U11(tt(),V1) -> U12(isBinKind(V1),V1) U111(tt()) -> tt() U12(tt(),V1) -> U13(isBin(V1)) U121(tt()) -> tt() U13(tt()) -> tt() U131(tt(),V2) -> U132(isBinKind(V2)) U132(tt()) -> tt() U141(tt(),V2) -> U142(isBinKind(V2)) U142(tt()) -> tt() U151(tt()) -> tt() U161(tt()) -> tt() U171(tt(),X) -> U172(isBinKind(X)) U172(tt()) -> z() U181(tt(),X,Y) -> U182(isBinKind(X),X,Y) U182(tt(),X,Y) -> U183(isBin(Y),X,Y) U183(tt(),X,Y) -> U184(isBinKind(Y),X,Y) U184(tt(),X,Y) -> 0(multAC(X,Y)) U191(tt(),X,Y) -> U192(isBinKind(X),X,Y) U192(tt(),X,Y) -> U193(isBin(Y),X,Y) U193(tt(),X,Y) -> U194(isBinKind(Y),X,Y) U194(tt(),X,Y) -> plusAC(0(multAC(X,Y)),Y) U201(tt(),X) -> U202(isBinKind(X),X) U202(tt(),X) -> X U21(tt(),V1,V2) -> U22(isBagKind(V1),V1,V2) U211(tt(),X,Y) -> U212(isBinKind(X),X,Y) U212(tt(),X,Y) -> U213(isBin(Y),X,Y) U213(tt(),X,Y) -> U214(isBinKind(Y),X,Y) U214(tt(),X,Y) -> 0(plusAC(X,Y)) U22(tt(),V1,V2) -> U23(isBagKind(V2),V1,V2) U221(tt(),X,Y) -> U222(isBinKind(X),X,Y) U222(tt(),X,Y) -> U223(isBin(Y),X,Y) U223(tt(),X,Y) -> U224(isBinKind(Y),X,Y) U224(tt(),X,Y) -> 1(plusAC(X,Y)) U23(tt(),V1,V2) -> U24(isBagKind(V2),V1,V2) U231(tt(),X,Y) -> U232(isBinKind(X),X,Y) U232(tt(),X,Y) -> U233(isBin(Y),X,Y) U233(tt(),X,Y) -> U234(isBinKind(Y),X,Y) U234(tt(),X,Y) -> 0(plusAC(plusAC(X,Y),1(z()))) U24(tt(),V1,V2) -> U25(isBag(V1),V2) U241(tt(),X) -> U242(isBinKind(X),X) U242(tt(),X) -> X U25(tt(),V2) -> U26(isBag(V2)) U251(tt(),A,B) -> U252(isBagKind(A),A,B) U252(tt(),A,B) -> U253(isBag(B),A,B) U253(tt(),A,B) -> U254(isBagKind(B),A,B) U254(tt(),A,B) -> multAC(prod(A),prod(B)) U26(tt()) -> tt() U261(tt(),X) -> U262(isBinKind(X),X) U262(tt(),X) -> X U271(tt(),A,B) -> U272(isBagKind(A),A,B) U272(tt(),A,B) -> U273(isBag(B),A,B) U273(tt(),A,B) -> U274(isBagKind(B),A,B) U274(tt(),A,B) -> plusAC(sum(A),sum(B)) U31(tt()) -> tt() U41(tt(),V2) -> U42(isBagKind(V2)) U42(tt()) -> tt() U51(tt(),V1) -> U52(isBinKind(V1),V1) U52(tt(),V1) -> U53(isBin(V1)) U53(tt()) -> tt() U61(tt(),V1) -> U62(isBinKind(V1),V1) U62(tt(),V1) -> U63(isBin(V1)) U63(tt()) -> tt() U71(tt(),V1,V2) -> U72(isBinKind(V1),V1,V2) U72(tt(),V1,V2) -> U73(isBinKind(V2),V1,V2) U73(tt(),V1,V2) -> U74(isBinKind(V2),V1,V2) U74(tt(),V1,V2) -> U75(isBin(V1),V2) U75(tt(),V2) -> U76(isBin(V2)) U76(tt()) -> tt() U81(tt(),V1,V2) -> U82(isBinKind(V1),V1,V2) U82(tt(),V1,V2) -> U83(isBinKind(V2),V1,V2) U83(tt(),V1,V2) -> U84(isBinKind(V2),V1,V2) U84(tt(),V1,V2) -> U85(isBin(V1),V2) U85(tt(),V2) -> U86(isBin(V2)) U86(tt()) -> tt() U91(tt(),V1) -> U92(isBagKind(V1),V1) U92(tt(),V1) -> U93(isBag(V1)) U93(tt()) -> tt() isBag(empty()) -> tt() isBag(singl(V1)) -> U11(isBinKind(V1),V1) isBag(unionAC(V1,V2)) -> U21(isBagKind(V1),V1,V2) isBagKind(empty()) -> tt() isBagKind(singl(V1)) -> U31(isBinKind(V1)) isBagKind(unionAC(V1,V2)) -> U41(isBagKind(V1),V2) isBin(z()) -> tt() isBin(0(V1)) -> U51(isBinKind(V1),V1) isBin(1(V1)) -> U61(isBinKind(V1),V1) isBin(multAC(V1,V2)) -> U71(isBinKind(V1),V1,V2) isBin(plusAC(V1,V2)) -> U81(isBinKind(V1),V1,V2) isBin(prod(V1)) -> U91(isBagKind(V1),V1) isBin(sum(V1)) -> U101(isBagKind(V1),V1) isBinKind(z()) -> tt() isBinKind(0(V1)) -> U111(isBinKind(V1)) isBinKind(1(V1)) -> U121(isBinKind(V1)) isBinKind(multAC(V1,V2)) -> U131(isBinKind(V1),V2) isBinKind(plusAC(V1,V2)) -> U141(isBinKind(V1),V2) isBinKind(prod(V1)) -> U151(isBagKind(V1)) isBinKind(sum(V1)) -> U161(isBagKind(V1)) multAC(z(),X) -> U171(isBin(X),X) multAC(0(X),Y) -> U181(isBin(X),X,Y) multAC(1(X),Y) -> U191(isBin(X),X,Y) plusAC(z(),X) -> U201(isBin(X),X) plusAC(0(X),0(Y)) -> U211(isBin(X),X,Y) plusAC(0(X),1(Y)) -> U221(isBin(X),X,Y) plusAC(1(X),1(Y)) -> U231(isBin(X),X,Y) prod(empty()) -> 1(z()) prod(singl(X)) -> U241(isBin(X),X) prod(unionAC(A,B)) -> U251(isBag(A),A,B) sum(empty()) -> 0(z()) sum(singl(X)) -> U261(isBin(X),X) sum(unionAC(A,B)) -> U271(isBag(A),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(),V1) -> isBagKind#(V1) U101#(tt(),V1) -> U102#(isBagKind(V1),V1) U102#(tt(),V1) -> isBag#(V1) U102#(tt(),V1) -> U103#(isBag(V1)) U11#(tt(),V1) -> isBinKind#(V1) U11#(tt(),V1) -> U12#(isBinKind(V1),V1) U12#(tt(),V1) -> isBin#(V1) U12#(tt(),V1) -> U13#(isBin(V1)) U131#(tt(),V2) -> isBinKind#(V2) U131#(tt(),V2) -> U132#(isBinKind(V2)) U141#(tt(),V2) -> isBinKind#(V2) U141#(tt(),V2) -> U142#(isBinKind(V2)) U171#(tt(),X) -> isBinKind#(X) U171#(tt(),X) -> U172#(isBinKind(X)) U181#(tt(),X,Y) -> isBinKind#(X) U181#(tt(),X,Y) -> U182#(isBinKind(X),X,Y) U182#(tt(),X,Y) -> isBin#(Y) U182#(tt(),X,Y) -> U183#(isBin(Y),X,Y) U183#(tt(),X,Y) -> isBinKind#(Y) U183#(tt(),X,Y) -> U184#(isBinKind(Y),X,Y) U184#(tt(),X,Y) -> mult{AC,#}(X,Y) U184#(tt(),X,Y) -> 0#(multAC(X,Y)) U191#(tt(),X,Y) -> isBinKind#(X) U191#(tt(),X,Y) -> U192#(isBinKind(X),X,Y) U192#(tt(),X,Y) -> isBin#(Y) U192#(tt(),X,Y) -> U193#(isBin(Y),X,Y) U193#(tt(),X,Y) -> isBinKind#(Y) U193#(tt(),X,Y) -> U194#(isBinKind(Y),X,Y) U194#(tt(),X,Y) -> mult{AC,#}(X,Y) U194#(tt(),X,Y) -> 0#(multAC(X,Y)) U194#(tt(),X,Y) -> plus{AC,#}(0(multAC(X,Y)),Y) U201#(tt(),X) -> isBinKind#(X) U201#(tt(),X) -> U202#(isBinKind(X),X) U21#(tt(),V1,V2) -> isBagKind#(V1) U21#(tt(),V1,V2) -> U22#(isBagKind(V1),V1,V2) U211#(tt(),X,Y) -> isBinKind#(X) U211#(tt(),X,Y) -> U212#(isBinKind(X),X,Y) U212#(tt(),X,Y) -> isBin#(Y) U212#(tt(),X,Y) -> U213#(isBin(Y),X,Y) U213#(tt(),X,Y) -> isBinKind#(Y) U213#(tt(),X,Y) -> U214#(isBinKind(Y),X,Y) U214#(tt(),X,Y) -> plus{AC,#}(X,Y) U214#(tt(),X,Y) -> 0#(plusAC(X,Y)) U22#(tt(),V1,V2) -> isBagKind#(V2) U22#(tt(),V1,V2) -> U23#(isBagKind(V2),V1,V2) U221#(tt(),X,Y) -> isBinKind#(X) U221#(tt(),X,Y) -> U222#(isBinKind(X),X,Y) U222#(tt(),X,Y) -> isBin#(Y) U222#(tt(),X,Y) -> U223#(isBin(Y),X,Y) U223#(tt(),X,Y) -> isBinKind#(Y) U223#(tt(),X,Y) -> U224#(isBinKind(Y),X,Y) U224#(tt(),X,Y) -> plus{AC,#}(X,Y) U23#(tt(),V1,V2) -> isBagKind#(V2) U23#(tt(),V1,V2) -> U24#(isBagKind(V2),V1,V2) U231#(tt(),X,Y) -> isBinKind#(X) U231#(tt(),X,Y) -> U232#(isBinKind(X),X,Y) U232#(tt(),X,Y) -> isBin#(Y) U232#(tt(),X,Y) -> U233#(isBin(Y),X,Y) U233#(tt(),X,Y) -> isBinKind#(Y) U233#(tt(),X,Y) -> U234#(isBinKind(Y),X,Y) U234#(tt(),X,Y) -> plus{AC,#}(X,Y) U234#(tt(),X,Y) -> plus{AC,#}(plusAC(X,Y),1(z())) U234#(tt(),X,Y) -> 0#(plusAC(plusAC(X,Y),1(z()))) U24#(tt(),V1,V2) -> isBag#(V1) U24#(tt(),V1,V2) -> U25#(isBag(V1),V2) U241#(tt(),X) -> isBinKind#(X) U241#(tt(),X) -> U242#(isBinKind(X),X) U25#(tt(),V2) -> isBag#(V2) U25#(tt(),V2) -> U26#(isBag(V2)) U251#(tt(),A,B) -> isBagKind#(A) U251#(tt(),A,B) -> U252#(isBagKind(A),A,B) U252#(tt(),A,B) -> isBag#(B) U252#(tt(),A,B) -> U253#(isBag(B),A,B) U253#(tt(),A,B) -> isBagKind#(B) U253#(tt(),A,B) -> U254#(isBagKind(B),A,B) U254#(tt(),A,B) -> prod#(B) U254#(tt(),A,B) -> prod#(A) U254#(tt(),A,B) -> mult{AC,#}(prod(A),prod(B)) U261#(tt(),X) -> isBinKind#(X) U261#(tt(),X) -> U262#(isBinKind(X),X) U271#(tt(),A,B) -> isBagKind#(A) U271#(tt(),A,B) -> U272#(isBagKind(A),A,B) U272#(tt(),A,B) -> isBag#(B) U272#(tt(),A,B) -> U273#(isBag(B),A,B) U273#(tt(),A,B) -> isBagKind#(B) U273#(tt(),A,B) -> U274#(isBagKind(B),A,B) U274#(tt(),A,B) -> sum#(B) U274#(tt(),A,B) -> sum#(A) U274#(tt(),A,B) -> plus{AC,#}(sum(A),sum(B)) U41#(tt(),V2) -> isBagKind#(V2) U41#(tt(),V2) -> U42#(isBagKind(V2)) U51#(tt(),V1) -> isBinKind#(V1) U51#(tt(),V1) -> U52#(isBinKind(V1),V1) U52#(tt(),V1) -> isBin#(V1) U52#(tt(),V1) -> U53#(isBin(V1)) U61#(tt(),V1) -> isBinKind#(V1) U61#(tt(),V1) -> U62#(isBinKind(V1),V1) U62#(tt(),V1) -> isBin#(V1) U62#(tt(),V1) -> U63#(isBin(V1)) U71#(tt(),V1,V2) -> isBinKind#(V1) U71#(tt(),V1,V2) -> U72#(isBinKind(V1),V1,V2) U72#(tt(),V1,V2) -> isBinKind#(V2) U72#(tt(),V1,V2) -> U73#(isBinKind(V2),V1,V2) U73#(tt(),V1,V2) -> isBinKind#(V2) U73#(tt(),V1,V2) -> U74#(isBinKind(V2),V1,V2) U74#(tt(),V1,V2) -> isBin#(V1) U74#(tt(),V1,V2) -> U75#(isBin(V1),V2) U75#(tt(),V2) -> isBin#(V2) U75#(tt(),V2) -> U76#(isBin(V2)) U81#(tt(),V1,V2) -> isBinKind#(V1) U81#(tt(),V1,V2) -> U82#(isBinKind(V1),V1,V2) U82#(tt(),V1,V2) -> isBinKind#(V2) U82#(tt(),V1,V2) -> U83#(isBinKind(V2),V1,V2) U83#(tt(),V1,V2) -> isBinKind#(V2) U83#(tt(),V1,V2) -> U84#(isBinKind(V2),V1,V2) U84#(tt(),V1,V2) -> isBin#(V1) U84#(tt(),V1,V2) -> U85#(isBin(V1),V2) U85#(tt(),V2) -> isBin#(V2) U85#(tt(),V2) -> U86#(isBin(V2)) U91#(tt(),V1) -> isBagKind#(V1) U91#(tt(),V1) -> U92#(isBagKind(V1),V1) U92#(tt(),V1) -> isBag#(V1) U92#(tt(),V1) -> U93#(isBag(V1)) isBag#(singl(V1)) -> isBinKind#(V1) isBag#(singl(V1)) -> U11#(isBinKind(V1),V1) isBag#(unionAC(V1,V2)) -> isBagKind#(V1) isBag#(unionAC(V1,V2)) -> U21#(isBagKind(V1),V1,V2) isBagKind#(singl(V1)) -> isBinKind#(V1) isBagKind#(singl(V1)) -> U31#(isBinKind(V1)) isBagKind#(unionAC(V1,V2)) -> isBagKind#(V1) isBagKind#(unionAC(V1,V2)) -> U41#(isBagKind(V1),V2) isBin#(0(V1)) -> isBinKind#(V1) isBin#(0(V1)) -> U51#(isBinKind(V1),V1) isBin#(1(V1)) -> isBinKind#(V1) isBin#(1(V1)) -> U61#(isBinKind(V1),V1) isBin#(multAC(V1,V2)) -> isBinKind#(V1) isBin#(multAC(V1,V2)) -> U71#(isBinKind(V1),V1,V2) isBin#(plusAC(V1,V2)) -> isBinKind#(V1) isBin#(plusAC(V1,V2)) -> U81#(isBinKind(V1),V1,V2) isBin#(prod(V1)) -> isBagKind#(V1) isBin#(prod(V1)) -> U91#(isBagKind(V1),V1) isBin#(sum(V1)) -> isBagKind#(V1) isBin#(sum(V1)) -> U101#(isBagKind(V1),V1) isBinKind#(0(V1)) -> isBinKind#(V1) isBinKind#(0(V1)) -> U111#(isBinKind(V1)) isBinKind#(1(V1)) -> isBinKind#(V1) isBinKind#(1(V1)) -> U121#(isBinKind(V1)) isBinKind#(multAC(V1,V2)) -> isBinKind#(V1) isBinKind#(multAC(V1,V2)) -> U131#(isBinKind(V1),V2) isBinKind#(plusAC(V1,V2)) -> isBinKind#(V1) isBinKind#(plusAC(V1,V2)) -> U141#(isBinKind(V1),V2) isBinKind#(prod(V1)) -> isBagKind#(V1) isBinKind#(prod(V1)) -> U151#(isBagKind(V1)) isBinKind#(sum(V1)) -> isBagKind#(V1) isBinKind#(sum(V1)) -> U161#(isBagKind(V1)) mult{AC,#}(z(),X) -> isBin#(X) mult{AC,#}(z(),X) -> U171#(isBin(X),X) mult{AC,#}(0(X),Y) -> isBin#(X) mult{AC,#}(0(X),Y) -> U181#(isBin(X),X,Y) mult{AC,#}(1(X),Y) -> isBin#(X) mult{AC,#}(1(X),Y) -> U191#(isBin(X),X,Y) plus{AC,#}(z(),X) -> isBin#(X) plus{AC,#}(z(),X) -> U201#(isBin(X),X) plus{AC,#}(0(X),0(Y)) -> isBin#(X) plus{AC,#}(0(X),0(Y)) -> U211#(isBin(X),X,Y) plus{AC,#}(0(X),1(Y)) -> isBin#(X) plus{AC,#}(0(X),1(Y)) -> U221#(isBin(X),X,Y) plus{AC,#}(1(X),1(Y)) -> isBin#(X) plus{AC,#}(1(X),1(Y)) -> U231#(isBin(X),X,Y) prod#(singl(X)) -> isBin#(X) prod#(singl(X)) -> U241#(isBin(X),X) prod#(unionAC(A,B)) -> isBag#(A) prod#(unionAC(A,B)) -> U251#(isBag(A),A,B) sum#(empty()) -> 0#(z()) sum#(singl(X)) -> isBin#(X) sum#(singl(X)) -> U261#(isBin(X),X) sum#(unionAC(A,B)) -> isBag#(A) sum#(unionAC(A,B)) -> U271#(isBag(A),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)) -> U171#(isBin(X),X) mult{AC,#}(x12,multAC(z(),X)) -> mult{AC,#}(x12,U171(isBin(X),X)) mult{AC,#}(x13,multAC(0(X),Y)) -> isBin#(X) mult{AC,#}(x13,multAC(0(X),Y)) -> U181#(isBin(X),X,Y) mult{AC,#}(x13,multAC(0(X),Y)) -> mult{AC,#}(x13,U181(isBin(X),X,Y)) mult{AC,#}(x14,multAC(1(X),Y)) -> isBin#(X) mult{AC,#}(x14,multAC(1(X),Y)) -> U191#(isBin(X),X,Y) mult{AC,#}(x14,multAC(1(X),Y)) -> mult{AC,#}(x14,U191(isBin(X),X,Y)) plus{AC,#}(x15,plusAC(z(),X)) -> isBin#(X) plus{AC,#}(x15,plusAC(z(),X)) -> U201#(isBin(X),X) plus{AC,#}(x15,plusAC(z(),X)) -> plus{AC,#}(x15,U201(isBin(X),X)) plus{AC,#}(x16,plusAC(0(X),0(Y))) -> isBin#(X) plus{AC,#}(x16,plusAC(0(X),0(Y))) -> U211#(isBin(X),X,Y) plus{AC,#}(x16,plusAC(0(X),0(Y))) -> plus{AC,#}(x16,U211(isBin(X),X,Y)) plus{AC,#}(x17,plusAC(0(X),1(Y))) -> isBin#(X) plus{AC,#}(x17,plusAC(0(X),1(Y))) -> U221#(isBin(X),X,Y) plus{AC,#}(x17,plusAC(0(X),1(Y))) -> plus{AC,#}(x17,U221(isBin(X),X,Y)) plus{AC,#}(x18,plusAC(1(X),1(Y))) -> isBin#(X) plus{AC,#}(x18,plusAC(1(X),1(Y))) -> U231#(isBin(X),X,Y) plus{AC,#}(x18,plusAC(1(X),1(Y))) -> plus{AC,#}(x18,U231(isBin(X),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(),V1) -> U102(isBagKind(V1),V1) U102(tt(),V1) -> U103(isBag(V1)) U103(tt()) -> tt() U11(tt(),V1) -> U12(isBinKind(V1),V1) U111(tt()) -> tt() U12(tt(),V1) -> U13(isBin(V1)) U121(tt()) -> tt() U13(tt()) -> tt() U131(tt(),V2) -> U132(isBinKind(V2)) U132(tt()) -> tt() U141(tt(),V2) -> U142(isBinKind(V2)) U142(tt()) -> tt() U151(tt()) -> tt() U161(tt()) -> tt() U171(tt(),X) -> U172(isBinKind(X)) U172(tt()) -> z() U181(tt(),X,Y) -> U182(isBinKind(X),X,Y) U182(tt(),X,Y) -> U183(isBin(Y),X,Y) U183(tt(),X,Y) -> U184(isBinKind(Y),X,Y) U184(tt(),X,Y) -> 0(multAC(X,Y)) U191(tt(),X,Y) -> U192(isBinKind(X),X,Y) U192(tt(),X,Y) -> U193(isBin(Y),X,Y) U193(tt(),X,Y) -> U194(isBinKind(Y),X,Y) U194(tt(),X,Y) -> plusAC(0(multAC(X,Y)),Y) U201(tt(),X) -> U202(isBinKind(X),X) U202(tt(),X) -> X U21(tt(),V1,V2) -> U22(isBagKind(V1),V1,V2) U211(tt(),X,Y) -> U212(isBinKind(X),X,Y) U212(tt(),X,Y) -> U213(isBin(Y),X,Y) U213(tt(),X,Y) -> U214(isBinKind(Y),X,Y) U214(tt(),X,Y) -> 0(plusAC(X,Y)) U22(tt(),V1,V2) -> U23(isBagKind(V2),V1,V2) U221(tt(),X,Y) -> U222(isBinKind(X),X,Y) U222(tt(),X,Y) -> U223(isBin(Y),X,Y) U223(tt(),X,Y) -> U224(isBinKind(Y),X,Y) U224(tt(),X,Y) -> 1(plusAC(X,Y)) U23(tt(),V1,V2) -> U24(isBagKind(V2),V1,V2) U231(tt(),X,Y) -> U232(isBinKind(X),X,Y) U232(tt(),X,Y) -> U233(isBin(Y),X,Y) U233(tt(),X,Y) -> U234(isBinKind(Y),X,Y) U234(tt(),X,Y) -> 0(plusAC(plusAC(X,Y),1(z()))) U24(tt(),V1,V2) -> U25(isBag(V1),V2) U241(tt(),X) -> U242(isBinKind(X),X) U242(tt(),X) -> X U25(tt(),V2) -> U26(isBag(V2)) U251(tt(),A,B) -> U252(isBagKind(A),A,B) U252(tt(),A,B) -> U253(isBag(B),A,B) U253(tt(),A,B) -> U254(isBagKind(B),A,B) U254(tt(),A,B) -> multAC(prod(A),prod(B)) U26(tt()) -> tt() U261(tt(),X) -> U262(isBinKind(X),X) U262(tt(),X) -> X U271(tt(),A,B) -> U272(isBagKind(A),A,B) U272(tt(),A,B) -> U273(isBag(B),A,B) U273(tt(),A,B) -> U274(isBagKind(B),A,B) U274(tt(),A,B) -> plusAC(sum(A),sum(B)) U31(tt()) -> tt() U41(tt(),V2) -> U42(isBagKind(V2)) U42(tt()) -> tt() U51(tt(),V1) -> U52(isBinKind(V1),V1) U52(tt(),V1) -> U53(isBin(V1)) U53(tt()) -> tt() U61(tt(),V1) -> U62(isBinKind(V1),V1) U62(tt(),V1) -> U63(isBin(V1)) U63(tt()) -> tt() U71(tt(),V1,V2) -> U72(isBinKind(V1),V1,V2) U72(tt(),V1,V2) -> U73(isBinKind(V2),V1,V2) U73(tt(),V1,V2) -> U74(isBinKind(V2),V1,V2) U74(tt(),V1,V2) -> U75(isBin(V1),V2) U75(tt(),V2) -> U76(isBin(V2)) U76(tt()) -> tt() U81(tt(),V1,V2) -> U82(isBinKind(V1),V1,V2) U82(tt(),V1,V2) -> U83(isBinKind(V2),V1,V2) U83(tt(),V1,V2) -> U84(isBinKind(V2),V1,V2) U84(tt(),V1,V2) -> U85(isBin(V1),V2) U85(tt(),V2) -> U86(isBin(V2)) U86(tt()) -> tt() U91(tt(),V1) -> U92(isBagKind(V1),V1) U92(tt(),V1) -> U93(isBag(V1)) U93(tt()) -> tt() isBag(empty()) -> tt() isBag(singl(V1)) -> U11(isBinKind(V1),V1) isBag(unionAC(V1,V2)) -> U21(isBagKind(V1),V1,V2) isBagKind(empty()) -> tt() isBagKind(singl(V1)) -> U31(isBinKind(V1)) isBagKind(unionAC(V1,V2)) -> U41(isBagKind(V1),V2) isBin(z()) -> tt() isBin(0(V1)) -> U51(isBinKind(V1),V1) isBin(1(V1)) -> U61(isBinKind(V1),V1) isBin(multAC(V1,V2)) -> U71(isBinKind(V1),V1,V2) isBin(plusAC(V1,V2)) -> U81(isBinKind(V1),V1,V2) isBin(prod(V1)) -> U91(isBagKind(V1),V1) isBin(sum(V1)) -> U101(isBagKind(V1),V1) isBinKind(z()) -> tt() isBinKind(0(V1)) -> U111(isBinKind(V1)) isBinKind(1(V1)) -> U121(isBinKind(V1)) isBinKind(multAC(V1,V2)) -> U131(isBinKind(V1),V2) isBinKind(plusAC(V1,V2)) -> U141(isBinKind(V1),V2) isBinKind(prod(V1)) -> U151(isBagKind(V1)) isBinKind(sum(V1)) -> U161(isBagKind(V1)) multAC(z(),X) -> U171(isBin(X),X) multAC(0(X),Y) -> U181(isBin(X),X,Y) multAC(1(X),Y) -> U191(isBin(X),X,Y) plusAC(z(),X) -> U201(isBin(X),X) plusAC(0(X),0(Y)) -> U211(isBin(X),X,Y) plusAC(0(X),1(Y)) -> U221(isBin(X),X,Y) plusAC(1(X),1(Y)) -> U231(isBin(X),X,Y) prod(empty()) -> 1(z()) prod(singl(X)) -> U241(isBin(X),X) prod(unionAC(A,B)) -> U251(isBag(A),A,B) sum(empty()) -> 0(z()) sum(singl(X)) -> U261(isBin(X),X) sum(unionAC(A,B)) -> U271(isBag(A),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(),V1) -> isBagKind#(V1) U101#(tt(),V1) -> U102#(isBagKind(V1),V1) U102#(tt(),V1) -> isBag#(V1) U102#(tt(),V1) -> U103#(isBag(V1)) U11#(tt(),V1) -> isBinKind#(V1) U11#(tt(),V1) -> U12#(isBinKind(V1),V1) U12#(tt(),V1) -> isBin#(V1) U12#(tt(),V1) -> U13#(isBin(V1)) U131#(tt(),V2) -> isBinKind#(V2) U131#(tt(),V2) -> U132#(isBinKind(V2)) U141#(tt(),V2) -> isBinKind#(V2) U141#(tt(),V2) -> U142#(isBinKind(V2)) U171#(tt(),X) -> isBinKind#(X) U171#(tt(),X) -> U172#(isBinKind(X)) U181#(tt(),X,Y) -> isBinKind#(X) U181#(tt(),X,Y) -> U182#(isBinKind(X),X,Y) U182#(tt(),X,Y) -> isBin#(Y) U182#(tt(),X,Y) -> U183#(isBin(Y),X,Y) U183#(tt(),X,Y) -> isBinKind#(Y) U183#(tt(),X,Y) -> U184#(isBinKind(Y),X,Y) U184#(tt(),X,Y) -> mult{AC,#}(X,Y) U184#(tt(),X,Y) -> 0#(multAC(X,Y)) U191#(tt(),X,Y) -> isBinKind#(X) U191#(tt(),X,Y) -> U192#(isBinKind(X),X,Y) U192#(tt(),X,Y) -> isBin#(Y) U192#(tt(),X,Y) -> U193#(isBin(Y),X,Y) U193#(tt(),X,Y) -> isBinKind#(Y) U193#(tt(),X,Y) -> U194#(isBinKind(Y),X,Y) U194#(tt(),X,Y) -> mult{AC,#}(X,Y) U194#(tt(),X,Y) -> 0#(multAC(X,Y)) U194#(tt(),X,Y) -> plus{AC,#}(0(multAC(X,Y)),Y) U201#(tt(),X) -> isBinKind#(X) U201#(tt(),X) -> U202#(isBinKind(X),X) U21#(tt(),V1,V2) -> isBagKind#(V1) U21#(tt(),V1,V2) -> U22#(isBagKind(V1),V1,V2) U211#(tt(),X,Y) -> isBinKind#(X) U211#(tt(),X,Y) -> U212#(isBinKind(X),X,Y) U212#(tt(),X,Y) -> isBin#(Y) U212#(tt(),X,Y) -> U213#(isBin(Y),X,Y) U213#(tt(),X,Y) -> isBinKind#(Y) U213#(tt(),X,Y) -> U214#(isBinKind(Y),X,Y) U214#(tt(),X,Y) -> plus{AC,#}(X,Y) U214#(tt(),X,Y) -> 0#(plusAC(X,Y)) U22#(tt(),V1,V2) -> isBagKind#(V2) U22#(tt(),V1,V2) -> U23#(isBagKind(V2),V1,V2) U221#(tt(),X,Y) -> isBinKind#(X) U221#(tt(),X,Y) -> U222#(isBinKind(X),X,Y) U222#(tt(),X,Y) -> isBin#(Y) U222#(tt(),X,Y) -> U223#(isBin(Y),X,Y) U223#(tt(),X,Y) -> isBinKind#(Y) U223#(tt(),X,Y) -> U224#(isBinKind(Y),X,Y) U224#(tt(),X,Y) -> plus{AC,#}(X,Y) U23#(tt(),V1,V2) -> isBagKind#(V2) U23#(tt(),V1,V2) -> U24#(isBagKind(V2),V1,V2) U231#(tt(),X,Y) -> isBinKind#(X) U231#(tt(),X,Y) -> U232#(isBinKind(X),X,Y) U232#(tt(),X,Y) -> isBin#(Y) U232#(tt(),X,Y) -> U233#(isBin(Y),X,Y) U233#(tt(),X,Y) -> isBinKind#(Y) U233#(tt(),X,Y) -> U234#(isBinKind(Y),X,Y) U234#(tt(),X,Y) -> plus{AC,#}(X,Y) U234#(tt(),X,Y) -> plus{AC,#}(plusAC(X,Y),1(z())) U234#(tt(),X,Y) -> 0#(plusAC(plusAC(X,Y),1(z()))) U24#(tt(),V1,V2) -> isBag#(V1) U24#(tt(),V1,V2) -> U25#(isBag(V1),V2) U241#(tt(),X) -> isBinKind#(X) U241#(tt(),X) -> U242#(isBinKind(X),X) U25#(tt(),V2) -> isBag#(V2) U25#(tt(),V2) -> U26#(isBag(V2)) U251#(tt(),A,B) -> isBagKind#(A) U251#(tt(),A,B) -> U252#(isBagKind(A),A,B) U252#(tt(),A,B) -> isBag#(B) U252#(tt(),A,B) -> U253#(isBag(B),A,B) U253#(tt(),A,B) -> isBagKind#(B) U253#(tt(),A,B) -> U254#(isBagKind(B),A,B) U254#(tt(),A,B) -> prod#(B) U254#(tt(),A,B) -> prod#(A) U254#(tt(),A,B) -> mult{AC,#}(prod(A),prod(B)) U261#(tt(),X) -> isBinKind#(X) U261#(tt(),X) -> U262#(isBinKind(X),X) U271#(tt(),A,B) -> isBagKind#(A) U271#(tt(),A,B) -> U272#(isBagKind(A),A,B) U272#(tt(),A,B) -> isBag#(B) U272#(tt(),A,B) -> U273#(isBag(B),A,B) U273#(tt(),A,B) -> isBagKind#(B) U273#(tt(),A,B) -> U274#(isBagKind(B),A,B) U274#(tt(),A,B) -> sum#(B) U274#(tt(),A,B) -> sum#(A) U274#(tt(),A,B) -> plus{AC,#}(sum(A),sum(B)) U41#(tt(),V2) -> isBagKind#(V2) U41#(tt(),V2) -> U42#(isBagKind(V2)) U51#(tt(),V1) -> isBinKind#(V1) U51#(tt(),V1) -> U52#(isBinKind(V1),V1) U52#(tt(),V1) -> isBin#(V1) U52#(tt(),V1) -> U53#(isBin(V1)) U61#(tt(),V1) -> isBinKind#(V1) U61#(tt(),V1) -> U62#(isBinKind(V1),V1) U62#(tt(),V1) -> isBin#(V1) U62#(tt(),V1) -> U63#(isBin(V1)) U71#(tt(),V1,V2) -> isBinKind#(V1) U71#(tt(),V1,V2) -> U72#(isBinKind(V1),V1,V2) U72#(tt(),V1,V2) -> isBinKind#(V2) U72#(tt(),V1,V2) -> U73#(isBinKind(V2),V1,V2) U73#(tt(),V1,V2) -> isBinKind#(V2) U73#(tt(),V1,V2) -> U74#(isBinKind(V2),V1,V2) U74#(tt(),V1,V2) -> isBin#(V1) U74#(tt(),V1,V2) -> U75#(isBin(V1),V2) U75#(tt(),V2) -> isBin#(V2) U75#(tt(),V2) -> U76#(isBin(V2)) U81#(tt(),V1,V2) -> isBinKind#(V1) U81#(tt(),V1,V2) -> U82#(isBinKind(V1),V1,V2) U82#(tt(),V1,V2) -> isBinKind#(V2) U82#(tt(),V1,V2) -> U83#(isBinKind(V2),V1,V2) U83#(tt(),V1,V2) -> isBinKind#(V2) U83#(tt(),V1,V2) -> U84#(isBinKind(V2),V1,V2) U84#(tt(),V1,V2) -> isBin#(V1) U84#(tt(),V1,V2) -> U85#(isBin(V1),V2) U85#(tt(),V2) -> isBin#(V2) U85#(tt(),V2) -> U86#(isBin(V2)) U91#(tt(),V1) -> isBagKind#(V1) U91#(tt(),V1) -> U92#(isBagKind(V1),V1) U92#(tt(),V1) -> isBag#(V1) U92#(tt(),V1) -> U93#(isBag(V1)) isBag#(singl(V1)) -> isBinKind#(V1) isBag#(singl(V1)) -> U11#(isBinKind(V1),V1) isBag#(unionAC(V1,V2)) -> isBagKind#(V1) isBag#(unionAC(V1,V2)) -> U21#(isBagKind(V1),V1,V2) isBagKind#(singl(V1)) -> isBinKind#(V1) isBagKind#(singl(V1)) -> U31#(isBinKind(V1)) isBagKind#(unionAC(V1,V2)) -> isBagKind#(V1) isBagKind#(unionAC(V1,V2)) -> U41#(isBagKind(V1),V2) isBin#(0(V1)) -> isBinKind#(V1) isBin#(0(V1)) -> U51#(isBinKind(V1),V1) isBin#(1(V1)) -> isBinKind#(V1) isBin#(1(V1)) -> U61#(isBinKind(V1),V1) isBin#(multAC(V1,V2)) -> isBinKind#(V1) isBin#(multAC(V1,V2)) -> U71#(isBinKind(V1),V1,V2) isBin#(plusAC(V1,V2)) -> isBinKind#(V1) isBin#(plusAC(V1,V2)) -> U81#(isBinKind(V1),V1,V2) isBin#(prod(V1)) -> isBagKind#(V1) isBin#(prod(V1)) -> U91#(isBagKind(V1),V1) isBin#(sum(V1)) -> isBagKind#(V1) isBin#(sum(V1)) -> U101#(isBagKind(V1),V1) isBinKind#(0(V1)) -> isBinKind#(V1) isBinKind#(0(V1)) -> U111#(isBinKind(V1)) isBinKind#(1(V1)) -> isBinKind#(V1) isBinKind#(1(V1)) -> U121#(isBinKind(V1)) isBinKind#(multAC(V1,V2)) -> isBinKind#(V1) isBinKind#(multAC(V1,V2)) -> U131#(isBinKind(V1),V2) isBinKind#(plusAC(V1,V2)) -> isBinKind#(V1) isBinKind#(plusAC(V1,V2)) -> U141#(isBinKind(V1),V2) isBinKind#(prod(V1)) -> isBagKind#(V1) isBinKind#(prod(V1)) -> U151#(isBagKind(V1)) isBinKind#(sum(V1)) -> isBagKind#(V1) isBinKind#(sum(V1)) -> U161#(isBagKind(V1)) mult{AC,#}(z(),X) -> isBin#(X) mult{AC,#}(z(),X) -> U171#(isBin(X),X) mult{AC,#}(0(X),Y) -> isBin#(X) mult{AC,#}(0(X),Y) -> U181#(isBin(X),X,Y) mult{AC,#}(1(X),Y) -> isBin#(X) mult{AC,#}(1(X),Y) -> U191#(isBin(X),X,Y) plus{AC,#}(z(),X) -> isBin#(X) plus{AC,#}(z(),X) -> U201#(isBin(X),X) plus{AC,#}(0(X),0(Y)) -> isBin#(X) plus{AC,#}(0(X),0(Y)) -> U211#(isBin(X),X,Y) plus{AC,#}(0(X),1(Y)) -> isBin#(X) plus{AC,#}(0(X),1(Y)) -> U221#(isBin(X),X,Y) plus{AC,#}(1(X),1(Y)) -> isBin#(X) plus{AC,#}(1(X),1(Y)) -> U231#(isBin(X),X,Y) prod#(singl(X)) -> isBin#(X) prod#(singl(X)) -> U241#(isBin(X),X) prod#(unionAC(A,B)) -> isBag#(A) prod#(unionAC(A,B)) -> U251#(isBag(A),A,B) sum#(empty()) -> 0#(z()) sum#(singl(X)) -> isBin#(X) sum#(singl(X)) -> U261#(isBin(X),X) sum#(unionAC(A,B)) -> isBag#(A) sum#(unionAC(A,B)) -> U271#(isBag(A),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)) -> U171#(isBin(X),X) mult{AC,#}(x12,multAC(z(),X)) -> mult{AC,#}(x12,U171(isBin(X),X)) mult{AC,#}(x13,multAC(0(X),Y)) -> isBin#(X) mult{AC,#}(x13,multAC(0(X),Y)) -> U181#(isBin(X),X,Y) mult{AC,#}(x13,multAC(0(X),Y)) -> mult{AC,#}(x13,U181(isBin(X),X,Y)) mult{AC,#}(x14,multAC(1(X),Y)) -> isBin#(X) mult{AC,#}(x14,multAC(1(X),Y)) -> U191#(isBin(X),X,Y) mult{AC,#}(x14,multAC(1(X),Y)) -> mult{AC,#}(x14,U191(isBin(X),X,Y)) plus{AC,#}(x15,plusAC(z(),X)) -> isBin#(X) plus{AC,#}(x15,plusAC(z(),X)) -> U201#(isBin(X),X) plus{AC,#}(x15,plusAC(z(),X)) -> plus{AC,#}(x15,U201(isBin(X),X)) plus{AC,#}(x16,plusAC(0(X),0(Y))) -> isBin#(X) plus{AC,#}(x16,plusAC(0(X),0(Y))) -> U211#(isBin(X),X,Y) plus{AC,#}(x16,plusAC(0(X),0(Y))) -> plus{AC,#}(x16,U211(isBin(X),X,Y)) plus{AC,#}(x17,plusAC(0(X),1(Y))) -> isBin#(X) plus{AC,#}(x17,plusAC(0(X),1(Y))) -> U221#(isBin(X),X,Y) plus{AC,#}(x17,plusAC(0(X),1(Y))) -> plus{AC,#}(x17,U221(isBin(X),X,Y)) plus{AC,#}(x18,plusAC(1(X),1(Y))) -> isBin#(X) plus{AC,#}(x18,plusAC(1(X),1(Y))) -> U231#(isBin(X),X,Y) plus{AC,#}(x18,plusAC(1(X),1(Y))) -> plus{AC,#}(x18,U231(isBin(X),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(),V1) -> U102(isBagKind(V1),V1) U102(tt(),V1) -> U103(isBag(V1)) U103(tt()) -> tt() U11(tt(),V1) -> U12(isBinKind(V1),V1) U111(tt()) -> tt() U12(tt(),V1) -> U13(isBin(V1)) U121(tt()) -> tt() U13(tt()) -> tt() U131(tt(),V2) -> U132(isBinKind(V2)) U132(tt()) -> tt() U141(tt(),V2) -> U142(isBinKind(V2)) U142(tt()) -> tt() U151(tt()) -> tt() U161(tt()) -> tt() U171(tt(),X) -> U172(isBinKind(X)) U172(tt()) -> z() U181(tt(),X,Y) -> U182(isBinKind(X),X,Y) U182(tt(),X,Y) -> U183(isBin(Y),X,Y) U183(tt(),X,Y) -> U184(isBinKind(Y),X,Y) U184(tt(),X,Y) -> 0(multAC(X,Y)) U191(tt(),X,Y) -> U192(isBinKind(X),X,Y) U192(tt(),X,Y) -> U193(isBin(Y),X,Y) U193(tt(),X,Y) -> U194(isBinKind(Y),X,Y) U194(tt(),X,Y) -> plusAC(0(multAC(X,Y)),Y) U201(tt(),X) -> U202(isBinKind(X),X) U202(tt(),X) -> X U21(tt(),V1,V2) -> U22(isBagKind(V1),V1,V2) U211(tt(),X,Y) -> U212(isBinKind(X),X,Y) U212(tt(),X,Y) -> U213(isBin(Y),X,Y) U213(tt(),X,Y) -> U214(isBinKind(Y),X,Y) U214(tt(),X,Y) -> 0(plusAC(X,Y)) U22(tt(),V1,V2) -> U23(isBagKind(V2),V1,V2) U221(tt(),X,Y) -> U222(isBinKind(X),X,Y) U222(tt(),X,Y) -> U223(isBin(Y),X,Y) U223(tt(),X,Y) -> U224(isBinKind(Y),X,Y) U224(tt(),X,Y) -> 1(plusAC(X,Y)) U23(tt(),V1,V2) -> U24(isBagKind(V2),V1,V2) U231(tt(),X,Y) -> U232(isBinKind(X),X,Y) U232(tt(),X,Y) -> U233(isBin(Y),X,Y) U233(tt(),X,Y) -> U234(isBinKind(Y),X,Y) U234(tt(),X,Y) -> 0(plusAC(plusAC(X,Y),1(z()))) U24(tt(),V1,V2) -> U25(isBag(V1),V2) U241(tt(),X) -> U242(isBinKind(X),X) U242(tt(),X) -> X U25(tt(),V2) -> U26(isBag(V2)) U251(tt(),A,B) -> U252(isBagKind(A),A,B) U252(tt(),A,B) -> U253(isBag(B),A,B) U253(tt(),A,B) -> U254(isBagKind(B),A,B) U254(tt(),A,B) -> multAC(prod(A),prod(B)) U26(tt()) -> tt() U261(tt(),X) -> U262(isBinKind(X),X) U262(tt(),X) -> X U271(tt(),A,B) -> U272(isBagKind(A),A,B) U272(tt(),A,B) -> U273(isBag(B),A,B) U273(tt(),A,B) -> U274(isBagKind(B),A,B) U274(tt(),A,B) -> plusAC(sum(A),sum(B)) U31(tt()) -> tt() U41(tt(),V2) -> U42(isBagKind(V2)) U42(tt()) -> tt() U51(tt(),V1) -> U52(isBinKind(V1),V1) U52(tt(),V1) -> U53(isBin(V1)) U53(tt()) -> tt() U61(tt(),V1) -> U62(isBinKind(V1),V1) U62(tt(),V1) -> U63(isBin(V1)) U63(tt()) -> tt() U71(tt(),V1,V2) -> U72(isBinKind(V1),V1,V2) U72(tt(),V1,V2) -> U73(isBinKind(V2),V1,V2) U73(tt(),V1,V2) -> U74(isBinKind(V2),V1,V2) U74(tt(),V1,V2) -> U75(isBin(V1),V2) U75(tt(),V2) -> U76(isBin(V2)) U76(tt()) -> tt() U81(tt(),V1,V2) -> U82(isBinKind(V1),V1,V2) U82(tt(),V1,V2) -> U83(isBinKind(V2),V1,V2) U83(tt(),V1,V2) -> U84(isBinKind(V2),V1,V2) U84(tt(),V1,V2) -> U85(isBin(V1),V2) U85(tt(),V2) -> U86(isBin(V2)) U86(tt()) -> tt() U91(tt(),V1) -> U92(isBagKind(V1),V1) U92(tt(),V1) -> U93(isBag(V1)) U93(tt()) -> tt() isBag(empty()) -> tt() isBag(singl(V1)) -> U11(isBinKind(V1),V1) isBag(unionAC(V1,V2)) -> U21(isBagKind(V1),V1,V2) isBagKind(empty()) -> tt() isBagKind(singl(V1)) -> U31(isBinKind(V1)) isBagKind(unionAC(V1,V2)) -> U41(isBagKind(V1),V2) isBin(z()) -> tt() isBin(0(V1)) -> U51(isBinKind(V1),V1) isBin(1(V1)) -> U61(isBinKind(V1),V1) isBin(multAC(V1,V2)) -> U71(isBinKind(V1),V1,V2) isBin(plusAC(V1,V2)) -> U81(isBinKind(V1),V1,V2) isBin(prod(V1)) -> U91(isBagKind(V1),V1) isBin(sum(V1)) -> U101(isBagKind(V1),V1) isBinKind(z()) -> tt() isBinKind(0(V1)) -> U111(isBinKind(V1)) isBinKind(1(V1)) -> U121(isBinKind(V1)) isBinKind(multAC(V1,V2)) -> U131(isBinKind(V1),V2) isBinKind(plusAC(V1,V2)) -> U141(isBinKind(V1),V2) isBinKind(prod(V1)) -> U151(isBagKind(V1)) isBinKind(sum(V1)) -> U161(isBagKind(V1)) multAC(z(),X) -> U171(isBin(X),X) multAC(0(X),Y) -> U181(isBin(X),X,Y) multAC(1(X),Y) -> U191(isBin(X),X,Y) plusAC(z(),X) -> U201(isBin(X),X) plusAC(0(X),0(Y)) -> U211(isBin(X),X,Y) plusAC(0(X),1(Y)) -> U221(isBin(X),X,Y) plusAC(1(X),1(Y)) -> U231(isBin(X),X,Y) prod(empty()) -> 1(z()) prod(singl(X)) -> U241(isBin(X),X) prod(unionAC(A,B)) -> U251(isBag(A),A,B) sum(empty()) -> 0(z()) sum(singl(X)) -> U261(isBin(X),X) sum(unionAC(A,B)) -> U271(isBag(A),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