The rewrite relation of the following equational TRS is considered.
union(X,empty) | → | X | (1) |
union(empty,X) | → | X | (2) |
0(z) | → | z | (3) |
U101(tt,X) | → | X | (4) |
U11(tt) | → | z | (5) |
U111(tt,A,B) | → | plus(sum(A),sum(B)) | (6) |
U21(tt,X,Y) | → | 0(mult(X,Y)) | (7) |
U31(tt,X,Y) | → | plus(0(mult(X,Y)),Y) | (8) |
U41(tt,X) | → | X | (9) |
U51(tt,X,Y) | → | 0(plus(X,Y)) | (10) |
U61(tt,X,Y) | → | 1(plus(X,Y)) | (11) |
U71(tt,X,Y) | → | 0(plus(plus(X,Y),1(z))) | (12) |
U81(tt,X) | → | X | (13) |
U91(tt,A,B) | → | mult(prod(A),prod(B)) | (14) |
and(tt,X) | → | X | (15) |
isBag(empty) | → | tt | (16) |
isBag(singl(V1)) | → | isBin(V1) | (17) |
isBag(union(V1,V2)) | → | and(isBag(V1),isBag(V2)) | (18) |
isBin(z) | → | tt | (19) |
isBin(0(V1)) | → | isBin(V1) | (20) |
isBin(1(V1)) | → | isBin(V1) | (21) |
isBin(mult(V1,V2)) | → | and(isBin(V1),isBin(V2)) | (22) |
isBin(plus(V1,V2)) | → | and(isBin(V1),isBin(V2)) | (23) |
isBin(prod(V1)) | → | isBag(V1) | (24) |
isBin(sum(V1)) | → | isBag(V1) | (25) |
mult(z,X) | → | U11(isBin(X)) | (26) |
mult(0(X),Y) | → | U21(and(isBin(X),isBin(Y)),X,Y) | (27) |
mult(1(X),Y) | → | U31(and(isBin(X),isBin(Y)),X,Y) | (28) |
plus(z,X) | → | U41(isBin(X),X) | (29) |
plus(0(X),0(Y)) | → | U51(and(isBin(X),isBin(Y)),X,Y) | (30) |
plus(0(X),1(Y)) | → | U61(and(isBin(X),isBin(Y)),X,Y) | (31) |
plus(1(X),1(Y)) | → | U71(and(isBin(X),isBin(Y)),X,Y) | (32) |
prod(empty) | → | 1(z) | (33) |
prod(singl(X)) | → | U81(isBin(X),X) | (34) |
prod(union(A,B)) | → | U91(and(isBag(A),isBag(B)),A,B) | (35) |
sum(empty) | → | 0(z) | (36) |
sum(singl(X)) | → | U101(isBin(X),X) | (37) |
sum(union(A,B)) | → | U111(and(isBag(A),isBag(B)),A,B) | (38) |
Associative symbols: mult, plus, union
Commutative symbols: mult, plus, union
The following set of (strict) dependency pairs is constructed for the TRS.
There are 101 ruless (increase limit for explicit display).
The extended rules of the TRSmult(mult(z,X),ext) | → | mult(U11(isBin(X)),ext) | (155) |
mult(mult(0(X),Y),ext) | → | mult(U21(and(isBin(X),isBin(Y)),X,Y),ext) | (156) |
mult(mult(1(X),Y),ext) | → | mult(U31(and(isBin(X),isBin(Y)),X,Y),ext) | (157) |
plus(plus(z,X),ext) | → | plus(U41(isBin(X),X),ext) | (158) |
plus(plus(0(X),0(Y)),ext) | → | plus(U51(and(isBin(X),isBin(Y)),X,Y),ext) | (159) |
plus(plus(0(X),1(Y)),ext) | → | plus(U61(and(isBin(X),isBin(Y)),X,Y),ext) | (160) |
plus(plus(1(X),1(Y)),ext) | → | plus(U71(and(isBin(X),isBin(Y)),X,Y),ext) | (161) |
union(union(X,empty),ext) | → | union(X,ext) | (162) |
union(union(empty,X),ext) | → | union(X,ext) | (163) |
The dependency pairs are split into 6 components.
U111#(tt,A,B) | → | sum#(A) | (55) |
sum#(union(A,B)) | → | U111#(and(isBag(A),isBag(B)),A,B) | (118) |
U111#(tt,A,B) | → | sum#(B) | (56) |
[isBin(x1)] | = | 2 · x1 |
[plus(x1, x2)] | = | 2 + 3 · x1 + 2 · x2 |
[and(x1, x2)] | = | 2 · x1 + 1 · x2 |
[isBag(x1)] | = | 2 + 2 · x1 |
[singl(x1)] | = | 3 + 3 · x1 |
[0(x1)] | = | 3 · x1 |
[prod(x1)] | = | 1 + 3 · x1 |
[sum(x1)] | = | 2 + 3 · x1 |
[empty] | = | 0 |
[tt] | = | 0 |
[union(x1, x2)] | = | 3 + 3 · x1 + 3 · x2 |
[mult(x1, x2)] | = | 3 + 3 · x1 + 2 · x2 |
[1(x1)] | = | 3 · x1 |
[z] | = | 0 |
[sum#(x1)] | = | 2 · x1 |
[U111#(x1, x2, x3)] | = | 1 · x1 + 2 · x2 + 2 · x3 |
isBin(plus(V1,V2)) | → | and(isBin(V1),isBin(V2)) | (23) |
isBag(singl(V1)) | → | isBin(V1) | (17) |
isBin(0(V1)) | → | isBin(V1) | (20) |
isBin(prod(V1)) | → | isBag(V1) | (24) |
isBin(sum(V1)) | → | isBag(V1) | (25) |
isBag(empty) | → | tt | (16) |
isBag(union(V1,V2)) | → | and(isBag(V1),isBag(V2)) | (18) |
and(tt,X) | → | X | (15) |
isBin(mult(V1,V2)) | → | and(isBin(V1),isBin(V2)) | (22) |
isBin(1(V1)) | → | isBin(V1) | (21) |
isBin(z) | → | tt | (19) |
sum#(union(A,B)) | → | U111#(and(isBag(A),isBag(B)),A,B) | (118) |
union(X,empty) | → | X | (1) |
union(empty,X) | → | X | (2) |
0(z) | → | z | (3) |
U101(tt,X) | → | X | (4) |
U11(tt) | → | z | (5) |
U111(tt,A,B) | → | plus(sum(A),sum(B)) | (6) |
U21(tt,X,Y) | → | 0(mult(X,Y)) | (7) |
U31(tt,X,Y) | → | plus(0(mult(X,Y)),Y) | (8) |
U41(tt,X) | → | X | (9) |
U51(tt,X,Y) | → | 0(plus(X,Y)) | (10) |
U61(tt,X,Y) | → | 1(plus(X,Y)) | (11) |
U71(tt,X,Y) | → | 0(plus(plus(X,Y),1(z))) | (12) |
U81(tt,X) | → | X | (13) |
U91(tt,A,B) | → | mult(prod(A),prod(B)) | (14) |
isBag(empty) | → | tt | (16) |
isBag(singl(V1)) | → | isBin(V1) | (17) |
isBag(union(V1,V2)) | → | and(isBag(V1),isBag(V2)) | (18) |
isBin(z) | → | tt | (19) |
isBin(0(V1)) | → | isBin(V1) | (20) |
isBin(1(V1)) | → | isBin(V1) | (21) |
isBin(mult(V1,V2)) | → | and(isBin(V1),isBin(V2)) | (22) |
isBin(plus(V1,V2)) | → | and(isBin(V1),isBin(V2)) | (23) |
isBin(prod(V1)) | → | isBag(V1) | (24) |
isBin(sum(V1)) | → | isBag(V1) | (25) |
mult(z,X) | → | U11(isBin(X)) | (26) |
mult(0(X),Y) | → | U21(and(isBin(X),isBin(Y)),X,Y) | (27) |
mult(1(X),Y) | → | U31(and(isBin(X),isBin(Y)),X,Y) | (28) |
plus(z,X) | → | U41(isBin(X),X) | (29) |
plus(0(X),0(Y)) | → | U51(and(isBin(X),isBin(Y)),X,Y) | (30) |
plus(0(X),1(Y)) | → | U61(and(isBin(X),isBin(Y)),X,Y) | (31) |
plus(1(X),1(Y)) | → | U71(and(isBin(X),isBin(Y)),X,Y) | (32) |
prod(empty) | → | 1(z) | (33) |
prod(singl(X)) | → | U81(isBin(X),X) | (34) |
prod(union(A,B)) | → | U91(and(isBag(A),isBag(B)),A,B) | (35) |
sum(empty) | → | 0(z) | (36) |
sum(singl(X)) | → | U101(isBin(X),X) | (37) |
sum(union(A,B)) | → | U111(and(isBag(A),isBag(B)),A,B) | (38) |
mult(mult(z,X),ext) | → | mult(U11(isBin(X)),ext) | (155) |
mult(mult(0(X),Y),ext) | → | mult(U21(and(isBin(X),isBin(Y)),X,Y),ext) | (156) |
mult(mult(1(X),Y),ext) | → | mult(U31(and(isBin(X),isBin(Y)),X,Y),ext) | (157) |
plus(plus(z,X),ext) | → | plus(U41(isBin(X),X),ext) | (158) |
plus(plus(0(X),0(Y)),ext) | → | plus(U51(and(isBin(X),isBin(Y)),X,Y),ext) | (159) |
plus(plus(0(X),1(Y)),ext) | → | plus(U61(and(isBin(X),isBin(Y)),X,Y),ext) | (160) |
plus(plus(1(X),1(Y)),ext) | → | plus(U71(and(isBin(X),isBin(Y)),X,Y),ext) | (161) |
union(union(X,empty),ext) | → | union(X,ext) | (162) |
union(union(empty,X),ext) | → | union(X,ext) | (163) |
The dependency pairs are split into 0 components.
U91#(tt,A,B) | → | prod#(A) | (69) |
prod#(union(A,B)) | → | U91#(and(isBag(A),isBag(B)),A,B) | (111) |
U91#(tt,A,B) | → | prod#(B) | (70) |
[isBin(x1)] | = | 2 · x1 |
[plus(x1, x2)] | = | 2 + 3 · x1 + 2 · x2 |
[and(x1, x2)] | = | 2 + 2 · x1 + 1 · x2 |
[isBag(x1)] | = | 1 · x1 |
[singl(x1)] | = | 3 · x1 |
[0(x1)] | = | 3 · x1 |
[prod(x1)] | = | 3 · x1 |
[sum(x1)] | = | 3 · x1 |
[empty] | = | 2 |
[tt] | = | 2 |
[union(x1, x2)] | = | 3 + 3 · x1 + 3 · x2 |
[mult(x1, x2)] | = | 2 + 3 · x1 + 2 · x2 |
[1(x1)] | = | 1 · x1 |
[z] | = | 2 |
[U91#(x1, x2, x3)] | = | 2 · x1 + 2 · x2 + 2 · x3 |
[prod#(x1)] | = | 2 + 2 · x1 |
isBin(plus(V1,V2)) | → | and(isBin(V1),isBin(V2)) | (23) |
isBag(singl(V1)) | → | isBin(V1) | (17) |
isBin(0(V1)) | → | isBin(V1) | (20) |
isBin(prod(V1)) | → | isBag(V1) | (24) |
isBin(sum(V1)) | → | isBag(V1) | (25) |
isBag(empty) | → | tt | (16) |
isBag(union(V1,V2)) | → | and(isBag(V1),isBag(V2)) | (18) |
and(tt,X) | → | X | (15) |
isBin(mult(V1,V2)) | → | and(isBin(V1),isBin(V2)) | (22) |
isBin(1(V1)) | → | isBin(V1) | (21) |
isBin(z) | → | tt | (19) |
U91#(tt,A,B) | → | prod#(A) | (69) |
prod#(union(A,B)) | → | U91#(and(isBag(A),isBag(B)),A,B) | (111) |
U91#(tt,A,B) | → | prod#(B) | (70) |
union(X,empty) | → | X | (1) |
union(empty,X) | → | X | (2) |
0(z) | → | z | (3) |
U101(tt,X) | → | X | (4) |
U11(tt) | → | z | (5) |
U111(tt,A,B) | → | plus(sum(A),sum(B)) | (6) |
U21(tt,X,Y) | → | 0(mult(X,Y)) | (7) |
U31(tt,X,Y) | → | plus(0(mult(X,Y)),Y) | (8) |
U41(tt,X) | → | X | (9) |
U51(tt,X,Y) | → | 0(plus(X,Y)) | (10) |
U61(tt,X,Y) | → | 1(plus(X,Y)) | (11) |
U71(tt,X,Y) | → | 0(plus(plus(X,Y),1(z))) | (12) |
U81(tt,X) | → | X | (13) |
U91(tt,A,B) | → | mult(prod(A),prod(B)) | (14) |
and(tt,X) | → | X | (15) |
isBag(empty) | → | tt | (16) |
isBag(singl(V1)) | → | isBin(V1) | (17) |
isBag(union(V1,V2)) | → | and(isBag(V1),isBag(V2)) | (18) |
isBin(z) | → | tt | (19) |
isBin(0(V1)) | → | isBin(V1) | (20) |
isBin(1(V1)) | → | isBin(V1) | (21) |
isBin(mult(V1,V2)) | → | and(isBin(V1),isBin(V2)) | (22) |
isBin(plus(V1,V2)) | → | and(isBin(V1),isBin(V2)) | (23) |
isBin(prod(V1)) | → | isBag(V1) | (24) |
isBin(sum(V1)) | → | isBag(V1) | (25) |
mult(z,X) | → | U11(isBin(X)) | (26) |
mult(0(X),Y) | → | U21(and(isBin(X),isBin(Y)),X,Y) | (27) |
mult(1(X),Y) | → | U31(and(isBin(X),isBin(Y)),X,Y) | (28) |
plus(z,X) | → | U41(isBin(X),X) | (29) |
plus(0(X),0(Y)) | → | U51(and(isBin(X),isBin(Y)),X,Y) | (30) |
plus(0(X),1(Y)) | → | U61(and(isBin(X),isBin(Y)),X,Y) | (31) |
plus(1(X),1(Y)) | → | U71(and(isBin(X),isBin(Y)),X,Y) | (32) |
prod(empty) | → | 1(z) | (33) |
prod(singl(X)) | → | U81(isBin(X),X) | (34) |
prod(union(A,B)) | → | U91(and(isBag(A),isBag(B)),A,B) | (35) |
sum(empty) | → | 0(z) | (36) |
sum(singl(X)) | → | U101(isBin(X),X) | (37) |
sum(union(A,B)) | → | U111(and(isBag(A),isBag(B)),A,B) | (38) |
mult(mult(z,X),ext) | → | mult(U11(isBin(X)),ext) | (155) |
mult(mult(0(X),Y),ext) | → | mult(U21(and(isBin(X),isBin(Y)),X,Y),ext) | (156) |
mult(mult(1(X),Y),ext) | → | mult(U31(and(isBin(X),isBin(Y)),X,Y),ext) | (157) |
plus(plus(z,X),ext) | → | plus(U41(isBin(X),X),ext) | (158) |
plus(plus(0(X),0(Y)),ext) | → | plus(U51(and(isBin(X),isBin(Y)),X,Y),ext) | (159) |
plus(plus(0(X),1(Y)),ext) | → | plus(U61(and(isBin(X),isBin(Y)),X,Y),ext) | (160) |
plus(plus(1(X),1(Y)),ext) | → | plus(U71(and(isBin(X),isBin(Y)),X,Y),ext) | (161) |
union(union(X,empty),ext) | → | union(X,ext) | (162) |
union(union(empty,X),ext) | → | union(X,ext) | (163) |
U21#(tt,X,Y) | → | mult#(X,Y) | (58) |
mult#(0(X),Y) | → | U21#(and(isBin(X),isBin(Y)),X,Y) | (87) |
mult#(1(X),Y) | → | U31#(and(isBin(X),isBin(Y)),X,Y) | (91) |
U31#(tt,X,Y) | → | mult#(X,Y) | (61) |
mult#(mult(z,X),ext) | → | mult#(U11(isBin(X)),ext) | (122) |
mult#(mult(0(X),Y),ext) | → | mult#(U21(and(isBin(X),isBin(Y)),X,Y),ext) | (125) |
mult#(mult(0(X),Y),ext) | → | U21#(and(isBin(X),isBin(Y)),X,Y) | (126) |
mult#(mult(1(X),Y),ext) | → | mult#(U31(and(isBin(X),isBin(Y)),X,Y),ext) | (130) |
mult#(mult(1(X),Y),ext) | → | U31#(and(isBin(X),isBin(Y)),X,Y) | (131) |
mult#(mult(x,y),z') | → | mult#(y,z') | (51) |
mult#(x,y) | → | mult#(y,x) | (45) |
mult#(mult(x,y),z') | → | mult#(x,mult(y,z')) | (48) |
[mult#(x1, x2)] | = | 1 · x2 + 1 · x1 + 1 · x1 · x2 |
[mult(x1, x2)] | = | 1 · x2 + 1 · x1 + 1 · x1 · x2 |
[1(x1)] | = | 1 + 1 · x1 |
[U31(x1, x2, x3)] | = | 1 · x3 + 1 · x1 + 1 · x1 · x3 + 1 · x1 · x2 + 1 · x1 · x2 · x3 |
[and(x1, x2)] | = | 1 · x1 · x2 |
[isBin(x1)] | = | 1 |
[0(x1)] | = | 1 · x1 |
[U21(x1, x2, x3)] | = | 1 · x3 + 1 · x2 + 1 · x2 · x3 |
[U21#(x1, x2, x3)] | = | 1 · x3 + 1 · x2 + 1 · x2 · x3 |
[U31#(x1, x2, x3)] | = | 1 · x3 + 1 · x2 + 1 · x2 · x3 |
[tt] | = | 1 |
[z] | = | 0 |
[U11(x1)] | = | 0 |
[plus(x1, x2)] | = | 1 · x2 + 1 · x1 |
[U51(x1, x2, x3)] | = | 1 · x3 + 1 · x2 |
[isBag(x1)] | = | 1 |
[singl(x1)] | = | 1 + 1 · x1 + 1 · x1 · x1 |
[empty] | = | 1 |
[union(x1, x2)] | = | 1 · x2 + 1 · x1 + 1 · x1 · x2 |
[U41(x1, x2)] | = | 1 · x2 |
[U61(x1, x2, x3)] | = | 1 + 1 · x3 + 1 · x2 |
[U71(x1, x2, x3)] | = | 1 + 1 · x3 + 1 · x2 |
[sum(x1)] | = | 1 + 1 · x1 + 1 · x1 · x1 |
[prod(x1)] | = | 1 + 1 · x1 + 1 · x1 · x1 |
U31(tt,X,Y) | → | plus(0(mult(X,Y)),Y) | (8) |
U11(tt) | → | z | (5) |
U21(tt,X,Y) | → | 0(mult(X,Y)) | (7) |
U51(tt,X,Y) | → | 0(plus(X,Y)) | (10) |
0(z) | → | z | (3) |
mult(mult(1(X),Y),ext) | → | mult(U31(and(isBin(X),isBin(Y)),X,Y),ext) | (157) |
mult(z,X) | → | U11(isBin(X)) | (26) |
mult(mult(z,X),ext) | → | mult(U11(isBin(X)),ext) | (155) |
mult(0(X),Y) | → | U21(and(isBin(X),isBin(Y)),X,Y) | (27) |
mult(mult(0(X),Y),ext) | → | mult(U21(and(isBin(X),isBin(Y)),X,Y),ext) | (156) |
mult(1(X),Y) | → | U31(and(isBin(X),isBin(Y)),X,Y) | (28) |
isBag(singl(V1)) | → | isBin(V1) | (17) |
isBag(empty) | → | tt | (16) |
isBag(union(V1,V2)) | → | and(isBag(V1),isBag(V2)) | (18) |
U41(tt,X) | → | X | (9) |
plus(plus(0(X),1(Y)),ext) | → | plus(U61(and(isBin(X),isBin(Y)),X,Y),ext) | (160) |
plus(plus(0(X),0(Y)),ext) | → | plus(U51(and(isBin(X),isBin(Y)),X,Y),ext) | (159) |
plus(0(X),1(Y)) | → | U61(and(isBin(X),isBin(Y)),X,Y) | (31) |
plus(0(X),0(Y)) | → | U51(and(isBin(X),isBin(Y)),X,Y) | (30) |
plus(z,X) | → | U41(isBin(X),X) | (29) |
plus(plus(1(X),1(Y)),ext) | → | plus(U71(and(isBin(X),isBin(Y)),X,Y),ext) | (161) |
plus(1(X),1(Y)) | → | U71(and(isBin(X),isBin(Y)),X,Y) | (32) |
plus(plus(z,X),ext) | → | plus(U41(isBin(X),X),ext) | (158) |
U71(tt,X,Y) | → | 0(plus(plus(X,Y),1(z))) | (12) |
isBin(sum(V1)) | → | isBag(V1) | (25) |
isBin(0(V1)) | → | isBin(V1) | (20) |
isBin(1(V1)) | → | isBin(V1) | (21) |
isBin(prod(V1)) | → | isBag(V1) | (24) |
isBin(mult(V1,V2)) | → | and(isBin(V1),isBin(V2)) | (22) |
isBin(z) | → | tt | (19) |
isBin(plus(V1,V2)) | → | and(isBin(V1),isBin(V2)) | (23) |
U61(tt,X,Y) | → | 1(plus(X,Y)) | (11) |
and(tt,X) | → | X | (15) |
mult(x,y) | → | mult(y,x) | (39) |
mult(mult(x,y),z') | → | mult(x,mult(y,z')) | (42) |
plus(plus(x,y),z') | → | plus(x,plus(y,z')) | (43) |
plus(x,y) | → | plus(y,x) | (40) |
mult#(mult(1(X),Y),ext) | → | U31#(and(isBin(X),isBin(Y)),X,Y) | (131) |
mult#(1(X),Y) | → | U31#(and(isBin(X),isBin(Y)),X,Y) | (91) |
The dependency pairs are split into 1 component.
mult#(0(X),Y) | → | U21#(and(isBin(X),isBin(Y)),X,Y) | (87) |
U21#(tt,X,Y) | → | mult#(X,Y) | (58) |
mult#(mult(z,X),ext) | → | mult#(U11(isBin(X)),ext) | (122) |
mult#(mult(0(X),Y),ext) | → | mult#(U21(and(isBin(X),isBin(Y)),X,Y),ext) | (125) |
mult#(mult(0(X),Y),ext) | → | U21#(and(isBin(X),isBin(Y)),X,Y) | (126) |
mult#(mult(1(X),Y),ext) | → | mult#(U31(and(isBin(X),isBin(Y)),X,Y),ext) | (130) |
mult#(mult(x,y),z') | → | mult#(y,z') | (51) |
mult#(x,y) | → | mult#(y,x) | (45) |
mult#(mult(x,y),z') | → | mult#(x,mult(y,z')) | (48) |
[mult#(x1, x2)] | = | 1 · x2 + 1 · x1 + 1 · x1 · x2 |
[mult(x1, x2)] | = | 1 · x2 + 1 · x1 + 1 · x1 · x2 |
[1(x1)] | = | 1 + 1 · x1 |
[U31(x1, x2, x3)] | = | 1 · x3 + 1 · x2 · x3 + 1 · x1 · x3 + 1 · x1 · x2 |
[and(x1, x2)] | = | 1 · x1 · x2 |
[isBin(x1)] | = | 1 |
[0(x1)] | = | 1 · x1 |
[U21(x1, x2, x3)] | = | 1 · x3 + 1 · x2 + 1 · x2 · x3 |
[U21#(x1, x2, x3)] | = | 1 · x3 + 1 · x2 + 1 · x2 · x3 |
[z] | = | 1 |
[U11(x1)] | = | 1 |
[tt] | = | 1 |
[U71(x1, x2, x3)] | = | 1 + 1 · x2 + 1 · x1 + 1 · x1 · x3 |
[plus(x1, x2)] | = | 1 · x2 + 1 · x1 |
[sum(x1)] | = | 1 + 1 · x1 + 1 · x1 · x1 |
[isBag(x1)] | = | 1 |
[prod(x1)] | = | 1 + 1 · x1 + 1 · x1 · x1 |
[U51(x1, x2, x3)] | = | 1 · x3 + 1 · x2 |
[U61(x1, x2, x3)] | = | 1 + 1 · x3 + 1 · x2 |
[U41(x1, x2)] | = | 1 · x1 + 1 · x1 · x2 |
[singl(x1)] | = | 1 + 1 · x1 + 1 · x1 · x1 |
[empty] | = | 1 |
[union(x1, x2)] | = | 1 · x2 + 1 · x1 + 1 · x1 · x2 |
U71(tt,X,Y) | → | 0(plus(plus(X,Y),1(z))) | (12) |
U31(tt,X,Y) | → | plus(0(mult(X,Y)),Y) | (8) |
isBin(sum(V1)) | → | isBag(V1) | (25) |
isBin(0(V1)) | → | isBin(V1) | (20) |
isBin(1(V1)) | → | isBin(V1) | (21) |
isBin(prod(V1)) | → | isBag(V1) | (24) |
isBin(mult(V1,V2)) | → | and(isBin(V1),isBin(V2)) | (22) |
isBin(z) | → | tt | (19) |
isBin(plus(V1,V2)) | → | and(isBin(V1),isBin(V2)) | (23) |
U11(tt) | → | z | (5) |
U51(tt,X,Y) | → | 0(plus(X,Y)) | (10) |
mult(mult(1(X),Y),ext) | → | mult(U31(and(isBin(X),isBin(Y)),X,Y),ext) | (157) |
mult(z,X) | → | U11(isBin(X)) | (26) |
mult(mult(z,X),ext) | → | mult(U11(isBin(X)),ext) | (155) |
mult(0(X),Y) | → | U21(and(isBin(X),isBin(Y)),X,Y) | (27) |
mult(mult(0(X),Y),ext) | → | mult(U21(and(isBin(X),isBin(Y)),X,Y),ext) | (156) |
mult(1(X),Y) | → | U31(and(isBin(X),isBin(Y)),X,Y) | (28) |
plus(plus(0(X),1(Y)),ext) | → | plus(U61(and(isBin(X),isBin(Y)),X,Y),ext) | (160) |
plus(plus(0(X),0(Y)),ext) | → | plus(U51(and(isBin(X),isBin(Y)),X,Y),ext) | (159) |
plus(0(X),1(Y)) | → | U61(and(isBin(X),isBin(Y)),X,Y) | (31) |
plus(0(X),0(Y)) | → | U51(and(isBin(X),isBin(Y)),X,Y) | (30) |
plus(z,X) | → | U41(isBin(X),X) | (29) |
plus(plus(1(X),1(Y)),ext) | → | plus(U71(and(isBin(X),isBin(Y)),X,Y),ext) | (161) |
plus(1(X),1(Y)) | → | U71(and(isBin(X),isBin(Y)),X,Y) | (32) |
plus(plus(z,X),ext) | → | plus(U41(isBin(X),X),ext) | (158) |
U21(tt,X,Y) | → | 0(mult(X,Y)) | (7) |
isBag(singl(V1)) | → | isBin(V1) | (17) |
isBag(empty) | → | tt | (16) |
isBag(union(V1,V2)) | → | and(isBag(V1),isBag(V2)) | (18) |
U61(tt,X,Y) | → | 1(plus(X,Y)) | (11) |
and(tt,X) | → | X | (15) |
0(z) | → | z | (3) |
U41(tt,X) | → | X | (9) |
mult(x,y) | → | mult(y,x) | (39) |
mult(mult(x,y),z') | → | mult(x,mult(y,z')) | (42) |
plus(plus(x,y),z') | → | plus(x,plus(y,z')) | (43) |
plus(x,y) | → | plus(y,x) | (40) |
mult#(mult(1(X),Y),ext) | → | mult#(U31(and(isBin(X),isBin(Y)),X,Y),ext) | (130) |
[mult#(x1, x2)] | = | 1 · x2 + 1 · x1 + 1 · x1 · x2 |
[mult(x1, x2)] | = | 1 · x2 + 1 · x1 + 1 · x1 · x2 |
[0(x1)] | = | 1 + 1 · x1 |
[U21(x1, x2, x3)] | = | 1 + 1 · x3 + 1 · x2 + 1 · x1 · x2 · x3 |
[and(x1, x2)] | = | 1 · x2 |
[isBin(x1)] | = | 1 |
[U21#(x1, x2, x3)] | = | 1 · x3 + 1 · x2 + 1 · x2 · x3 |
[z] | = | 0 |
[U11(x1)] | = | 0 |
[tt] | = | 1 |
[isBag(x1)] | = | 1 |
[singl(x1)] | = | 1 + 1 · x1 + 1 · x1 · x1 |
[empty] | = | 1 |
[union(x1, x2)] | = | 1 · x2 + 1 · x1 + 1 · x1 · x2 |
[U61(x1, x2, x3)] | = | 1 + 1 · x3 + 1 · x2 |
[1(x1)] | = | 1 + 1 · x1 |
[plus(x1, x2)] | = | 1 · x2 + 1 · x1 |
[U31(x1, x2, x3)] | = | 1 · x3 + 1 · x2 + 1 · x1 + 1 · x2 · x3 + 1 · x1 · x3 |
[U41(x1, x2)] | = | 1 · x2 |
[U71(x1, x2, x3)] | = | 1 + 1 · x3 + 1 · x2 + 1 · x1 |
[U51(x1, x2, x3)] | = | 1 + 1 · x3 + 1 · x2 |
[sum(x1)] | = | 1 + 1 · x1 + 1 · x1 · x1 |
[prod(x1)] | = | 1 + 1 · x1 + 1 · x1 · x1 |
isBag(singl(V1)) | → | isBin(V1) | (17) |
isBag(empty) | → | tt | (16) |
isBag(union(V1,V2)) | → | and(isBag(V1),isBag(V2)) | (18) |
U21(tt,X,Y) | → | 0(mult(X,Y)) | (7) |
U61(tt,X,Y) | → | 1(plus(X,Y)) | (11) |
U11(tt) | → | z | (5) |
mult(mult(1(X),Y),ext) | → | mult(U31(and(isBin(X),isBin(Y)),X,Y),ext) | (157) |
mult(z,X) | → | U11(isBin(X)) | (26) |
mult(mult(z,X),ext) | → | mult(U11(isBin(X)),ext) | (155) |
mult(0(X),Y) | → | U21(and(isBin(X),isBin(Y)),X,Y) | (27) |
mult(mult(0(X),Y),ext) | → | mult(U21(and(isBin(X),isBin(Y)),X,Y),ext) | (156) |
mult(1(X),Y) | → | U31(and(isBin(X),isBin(Y)),X,Y) | (28) |
U41(tt,X) | → | X | (9) |
0(z) | → | z | (3) |
and(tt,X) | → | X | (15) |
U71(tt,X,Y) | → | 0(plus(plus(X,Y),1(z))) | (12) |
U51(tt,X,Y) | → | 0(plus(X,Y)) | (10) |
isBin(sum(V1)) | → | isBag(V1) | (25) |
isBin(0(V1)) | → | isBin(V1) | (20) |
isBin(1(V1)) | → | isBin(V1) | (21) |
isBin(prod(V1)) | → | isBag(V1) | (24) |
isBin(mult(V1,V2)) | → | and(isBin(V1),isBin(V2)) | (22) |
isBin(z) | → | tt | (19) |
isBin(plus(V1,V2)) | → | and(isBin(V1),isBin(V2)) | (23) |
plus(plus(0(X),1(Y)),ext) | → | plus(U61(and(isBin(X),isBin(Y)),X,Y),ext) | (160) |
plus(plus(0(X),0(Y)),ext) | → | plus(U51(and(isBin(X),isBin(Y)),X,Y),ext) | (159) |
plus(0(X),1(Y)) | → | U61(and(isBin(X),isBin(Y)),X,Y) | (31) |
plus(0(X),0(Y)) | → | U51(and(isBin(X),isBin(Y)),X,Y) | (30) |
plus(z,X) | → | U41(isBin(X),X) | (29) |
plus(plus(1(X),1(Y)),ext) | → | plus(U71(and(isBin(X),isBin(Y)),X,Y),ext) | (161) |
plus(1(X),1(Y)) | → | U71(and(isBin(X),isBin(Y)),X,Y) | (32) |
plus(plus(z,X),ext) | → | plus(U41(isBin(X),X),ext) | (158) |
U31(tt,X,Y) | → | plus(0(mult(X,Y)),Y) | (8) |
mult(x,y) | → | mult(y,x) | (39) |
mult(mult(x,y),z') | → | mult(x,mult(y,z')) | (42) |
plus(plus(x,y),z') | → | plus(x,plus(y,z')) | (43) |
plus(x,y) | → | plus(y,x) | (40) |
mult#(mult(0(X),Y),ext) | → | U21#(and(isBin(X),isBin(Y)),X,Y) | (126) |
mult#(0(X),Y) | → | U21#(and(isBin(X),isBin(Y)),X,Y) | (87) |
The dependency pairs are split into 1 component.
mult#(mult(z,X),ext) | → | mult#(U11(isBin(X)),ext) | (122) |
mult#(mult(0(X),Y),ext) | → | mult#(U21(and(isBin(X),isBin(Y)),X,Y),ext) | (125) |
mult#(mult(x,y),z') | → | mult#(y,z') | (51) |
mult#(x,y) | → | mult#(y,x) | (45) |
mult#(mult(x,y),z') | → | mult#(x,mult(y,z')) | (48) |
[mult#(x1, x2)] | = | 3 · x1 + 3 · x2 |
[mult(x1, x2)] | = | 3 + 1 · x1 + 1 · x2 |
[0(x1)] | = | 3 |
[U21(x1, x2, x3)] | = | 3 |
[and(x1, x2)] | = | 1 · x2 |
[isBin(x1)] | = | 1 |
[z] | = | 3 |
[U11(x1)] | = | 2 + 1 · x1 |
[U71(x1, x2, x3)] | = | 1 + 2 · x1 |
[tt] | = | 1 |
[plus(x1, x2)] | = | 1 · x1 + 1 · x2 |
[1(x1)] | = | 2 |
[U61(x1, x2, x3)] | = | 2 · x1 |
[isBag(x1)] | = | 1 |
[singl(x1)] | = | 0 |
[empty] | = | 0 |
[union(x1, x2)] | = | 0 |
[sum(x1)] | = | 0 |
[prod(x1)] | = | 3 · x1 |
[U41(x1, x2)] | = | 1 · x2 |
[U31(x1, x2, x3)] | = | 2 + 3 · x1 + 1 · x3 |
[U51(x1, x2, x3)] | = | 2 + 1 · x1 |
0(z) | → | z | (3) |
U71(tt,X,Y) | → | 0(plus(plus(X,Y),1(z))) | (12) |
U21(tt,X,Y) | → | 0(mult(X,Y)) | (7) |
U61(tt,X,Y) | → | 1(plus(X,Y)) | (11) |
isBag(singl(V1)) | → | isBin(V1) | (17) |
isBag(empty) | → | tt | (16) |
isBag(union(V1,V2)) | → | and(isBag(V1),isBag(V2)) | (18) |
isBin(sum(V1)) | → | isBag(V1) | (25) |
isBin(0(V1)) | → | isBin(V1) | (20) |
isBin(1(V1)) | → | isBin(V1) | (21) |
isBin(prod(V1)) | → | isBag(V1) | (24) |
isBin(mult(V1,V2)) | → | and(isBin(V1),isBin(V2)) | (22) |
isBin(z) | → | tt | (19) |
isBin(plus(V1,V2)) | → | and(isBin(V1),isBin(V2)) | (23) |
U41(tt,X) | → | X | (9) |
U31(tt,X,Y) | → | plus(0(mult(X,Y)),Y) | (8) |
and(tt,X) | → | X | (15) |
mult(mult(1(X),Y),ext) | → | mult(U31(and(isBin(X),isBin(Y)),X,Y),ext) | (157) |
mult(z,X) | → | U11(isBin(X)) | (26) |
mult(mult(z,X),ext) | → | mult(U11(isBin(X)),ext) | (155) |
mult(0(X),Y) | → | U21(and(isBin(X),isBin(Y)),X,Y) | (27) |
mult(mult(0(X),Y),ext) | → | mult(U21(and(isBin(X),isBin(Y)),X,Y),ext) | (156) |
mult(1(X),Y) | → | U31(and(isBin(X),isBin(Y)),X,Y) | (28) |
plus(plus(0(X),1(Y)),ext) | → | plus(U61(and(isBin(X),isBin(Y)),X,Y),ext) | (160) |
plus(plus(0(X),0(Y)),ext) | → | plus(U51(and(isBin(X),isBin(Y)),X,Y),ext) | (159) |
plus(0(X),1(Y)) | → | U61(and(isBin(X),isBin(Y)),X,Y) | (31) |
plus(0(X),0(Y)) | → | U51(and(isBin(X),isBin(Y)),X,Y) | (30) |
plus(z,X) | → | U41(isBin(X),X) | (29) |
plus(plus(1(X),1(Y)),ext) | → | plus(U71(and(isBin(X),isBin(Y)),X,Y),ext) | (161) |
plus(1(X),1(Y)) | → | U71(and(isBin(X),isBin(Y)),X,Y) | (32) |
plus(plus(z,X),ext) | → | plus(U41(isBin(X),X),ext) | (158) |
U11(tt) | → | z | (5) |
U51(tt,X,Y) | → | 0(plus(X,Y)) | (10) |
mult(x,y) | → | mult(y,x) | (39) |
mult(mult(x,y),z') | → | mult(x,mult(y,z')) | (42) |
plus(plus(x,y),z') | → | plus(x,plus(y,z')) | (43) |
plus(x,y) | → | plus(y,x) | (40) |
mult#(mult(x,y),z') | → | mult#(y,z') | (51) |
mult#(mult(0(X),Y),ext) | → | mult#(U21(and(isBin(X),isBin(Y)),X,Y),ext) | (125) |
mult#(mult(z,X),ext) | → | mult#(U11(isBin(X)),ext) | (122) |
U51#(tt,X,Y) | → | plus#(X,Y) | (63) |
plus#(0(X),0(Y)) | → | U51#(and(isBin(X),isBin(Y)),X,Y) | (97) |
plus#(0(X),1(Y)) | → | U61#(and(isBin(X),isBin(Y)),X,Y) | (101) |
U61#(tt,X,Y) | → | plus#(X,Y) | (64) |
plus#(1(X),1(Y)) | → | U71#(and(isBin(X),isBin(Y)),X,Y) | (105) |
U71#(tt,X,Y) | → | plus#(plus(X,Y),1(z)) | (66) |
plus#(plus(z,X),ext) | → | plus#(U41(isBin(X),X),ext) | (135) |
plus#(plus(0(X),0(Y)),ext) | → | plus#(U51(and(isBin(X),isBin(Y)),X,Y),ext) | (138) |
plus#(plus(0(X),0(Y)),ext) | → | U51#(and(isBin(X),isBin(Y)),X,Y) | (139) |
plus#(plus(0(X),1(Y)),ext) | → | plus#(U61(and(isBin(X),isBin(Y)),X,Y),ext) | (143) |
plus#(plus(0(X),1(Y)),ext) | → | U61#(and(isBin(X),isBin(Y)),X,Y) | (144) |
plus#(plus(1(X),1(Y)),ext) | → | plus#(U71(and(isBin(X),isBin(Y)),X,Y),ext) | (148) |
plus#(plus(1(X),1(Y)),ext) | → | U71#(and(isBin(X),isBin(Y)),X,Y) | (149) |
U71#(tt,X,Y) | → | plus#(X,Y) | (67) |
plus#(plus(x,y),z') | → | plus#(y,z') | (52) |
plus#(x,y) | → | plus#(y,x) | (46) |
plus#(plus(x,y),z') | → | plus#(x,plus(y,z')) | (49) |
[plus#(x1, x2)] | = | 2 · x1 + 2 · x2 |
[plus(x1, x2)] | = | 1 · x1 + 1 · x2 |
[1(x1)] | = | 1 + 2 · x1 |
[U71#(x1, x2, x3)] | = | 3 + 2 · x2 + 2 · x3 |
[and(x1, x2)] | = | 0 |
[isBin(x1)] | = | 0 |
[0(x1)] | = | 2 · x1 |
[U61(x1, x2, x3)] | = | 1 + 2 · x2 + 2 · x3 |
[U61#(x1, x2, x3)] | = | 1 + 2 · x2 + 2 · x3 |
[tt] | = | 0 |
[z] | = | 0 |
[U41(x1, x2)] | = | 1 · x2 |
[U71(x1, x2, x3)] | = | 2 + 2 · x2 + 2 · x3 |
[U51(x1, x2, x3)] | = | 2 · x2 + 2 · x3 |
[U51#(x1, x2, x3)] | = | 2 · x2 + 2 · x3 |
[sum(x1)] | = | 0 |
[isBag(x1)] | = | 0 |
[prod(x1)] | = | 3 · x1 |
[mult(x1, x2)] | = | 0 |
[singl(x1)] | = | 0 |
[empty] | = | 0 |
[union(x1, x2)] | = | 0 |
U41(tt,X) | → | X | (9) |
U61(tt,X,Y) | → | 1(plus(X,Y)) | (11) |
U71(tt,X,Y) | → | 0(plus(plus(X,Y),1(z))) | (12) |
plus(plus(0(X),1(Y)),ext) | → | plus(U61(and(isBin(X),isBin(Y)),X,Y),ext) | (160) |
plus(plus(0(X),0(Y)),ext) | → | plus(U51(and(isBin(X),isBin(Y)),X,Y),ext) | (159) |
plus(0(X),1(Y)) | → | U61(and(isBin(X),isBin(Y)),X,Y) | (31) |
plus(0(X),0(Y)) | → | U51(and(isBin(X),isBin(Y)),X,Y) | (30) |
plus(z,X) | → | U41(isBin(X),X) | (29) |
plus(plus(1(X),1(Y)),ext) | → | plus(U71(and(isBin(X),isBin(Y)),X,Y),ext) | (161) |
plus(1(X),1(Y)) | → | U71(and(isBin(X),isBin(Y)),X,Y) | (32) |
plus(plus(z,X),ext) | → | plus(U41(isBin(X),X),ext) | (158) |
U51(tt,X,Y) | → | 0(plus(X,Y)) | (10) |
0(z) | → | z | (3) |
plus(plus(x,y),z') | → | plus(x,plus(y,z')) | (43) |
plus(x,y) | → | plus(y,x) | (40) |
plus#(plus(1(X),1(Y)),ext) | → | U71#(and(isBin(X),isBin(Y)),X,Y) | (149) |
U61#(tt,X,Y) | → | plus#(X,Y) | (64) |
plus#(1(X),1(Y)) | → | U71#(and(isBin(X),isBin(Y)),X,Y) | (105) |
U71#(tt,X,Y) | → | plus#(X,Y) | (67) |
plus#(0(X),1(Y)) | → | U61#(and(isBin(X),isBin(Y)),X,Y) | (101) |
U71#(tt,X,Y) | → | plus#(plus(X,Y),1(z)) | (66) |
plus#(plus(0(X),1(Y)),ext) | → | U61#(and(isBin(X),isBin(Y)),X,Y) | (144) |
[plus#(x1, x2)] | = | 2 · x1 + 2 · x2 |
[plus(x1, x2)] | = | 1 · x1 + 1 · x2 |
[0(x1)] | = | 1 · x1 |
[1(x1)] | = | 2 + 1 · x1 |
[U61(x1, x2, x3)] | = | 2 + 1 · x2 + 1 · x3 |
[and(x1, x2)] | = | 0 |
[isBin(x1)] | = | 0 |
[z] | = | 0 |
[U41(x1, x2)] | = | 1 · x2 |
[U71(x1, x2, x3)] | = | 3 + 1 · x2 + 1 · x3 |
[U51(x1, x2, x3)] | = | 1 · x2 + 1 · x3 |
[U51#(x1, x2, x3)] | = | 2 · x2 + 2 · x3 |
[tt] | = | 0 |
[sum(x1)] | = | 0 |
[isBag(x1)] | = | 0 |
[prod(x1)] | = | 3 · x1 |
[mult(x1, x2)] | = | 0 |
[singl(x1)] | = | 0 |
[empty] | = | 0 |
[union(x1, x2)] | = | 0 |
plus(plus(0(X),1(Y)),ext) | → | plus(U61(and(isBin(X),isBin(Y)),X,Y),ext) | (160) |
plus(plus(0(X),0(Y)),ext) | → | plus(U51(and(isBin(X),isBin(Y)),X,Y),ext) | (159) |
plus(0(X),1(Y)) | → | U61(and(isBin(X),isBin(Y)),X,Y) | (31) |
plus(0(X),0(Y)) | → | U51(and(isBin(X),isBin(Y)),X,Y) | (30) |
plus(z,X) | → | U41(isBin(X),X) | (29) |
plus(plus(1(X),1(Y)),ext) | → | plus(U71(and(isBin(X),isBin(Y)),X,Y),ext) | (161) |
plus(1(X),1(Y)) | → | U71(and(isBin(X),isBin(Y)),X,Y) | (32) |
plus(plus(z,X),ext) | → | plus(U41(isBin(X),X),ext) | (158) |
U51(tt,X,Y) | → | 0(plus(X,Y)) | (10) |
U41(tt,X) | → | X | (9) |
0(z) | → | z | (3) |
U61(tt,X,Y) | → | 1(plus(X,Y)) | (11) |
U71(tt,X,Y) | → | 0(plus(plus(X,Y),1(z))) | (12) |
plus(plus(x,y),z') | → | plus(x,plus(y,z')) | (43) |
plus(x,y) | → | plus(y,x) | (40) |
plus#(plus(1(X),1(Y)),ext) | → | plus#(U71(and(isBin(X),isBin(Y)),X,Y),ext) | (148) |
[plus#(x1, x2)] | = | 2 · x1 + 2 · x2 |
[plus(x1, x2)] | = | 1 · x1 + 1 · x2 |
[0(x1)] | = | 1 · x1 |
[1(x1)] | = | 2 + 1 · x1 |
[U61(x1, x2, x3)] | = | 2 + 1 · x2 + 1 · x3 |
[and(x1, x2)] | = | 0 |
[isBin(x1)] | = | 0 |
[z] | = | 1 |
[U41(x1, x2)] | = | 1 · x2 |
[U51(x1, x2, x3)] | = | 1 · x2 + 1 · x3 |
[U51#(x1, x2, x3)] | = | 2 · x2 + 2 · x3 |
[tt] | = | 0 |
[U71(x1, x2, x3)] | = | 3 + 1 · x2 + 1 · x3 |
[isBag(x1)] | = | 0 |
[singl(x1)] | = | 0 |
[empty] | = | 0 |
[union(x1, x2)] | = | 0 |
[sum(x1)] | = | 3 · x1 |
[prod(x1)] | = | 0 |
[mult(x1, x2)] | = | 0 |
plus(plus(0(X),1(Y)),ext) | → | plus(U61(and(isBin(X),isBin(Y)),X,Y),ext) | (160) |
plus(plus(0(X),0(Y)),ext) | → | plus(U51(and(isBin(X),isBin(Y)),X,Y),ext) | (159) |
plus(0(X),1(Y)) | → | U61(and(isBin(X),isBin(Y)),X,Y) | (31) |
plus(0(X),0(Y)) | → | U51(and(isBin(X),isBin(Y)),X,Y) | (30) |
plus(z,X) | → | U41(isBin(X),X) | (29) |
plus(plus(1(X),1(Y)),ext) | → | plus(U71(and(isBin(X),isBin(Y)),X,Y),ext) | (161) |
plus(1(X),1(Y)) | → | U71(and(isBin(X),isBin(Y)),X,Y) | (32) |
plus(plus(z,X),ext) | → | plus(U41(isBin(X),X),ext) | (158) |
0(z) | → | z | (3) |
U61(tt,X,Y) | → | 1(plus(X,Y)) | (11) |
U41(tt,X) | → | X | (9) |
U71(tt,X,Y) | → | 0(plus(plus(X,Y),1(z))) | (12) |
U51(tt,X,Y) | → | 0(plus(X,Y)) | (10) |
plus(plus(x,y),z') | → | plus(x,plus(y,z')) | (43) |
plus(x,y) | → | plus(y,x) | (40) |
plus#(plus(z,X),ext) | → | plus#(U41(isBin(X),X),ext) | (135) |
[plus#(x1, x2)] | = | 2 · x1 + 2 · x2 |
[plus(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[0(x1)] | = | 1 · x1 |
[1(x1)] | = | 1 + 1 · x1 |
[U61(x1, x2, x3)] | = | 2 + 1 · x2 + 1 · x3 |
[and(x1, x2)] | = | 0 |
[isBin(x1)] | = | 0 |
[U51(x1, x2, x3)] | = | 1 + 1 · x2 + 1 · x3 |
[U51#(x1, x2, x3)] | = | 2 · x2 + 2 · x3 |
[tt] | = | 0 |
[sum(x1)] | = | 3 · x1 |
[isBag(x1)] | = | 0 |
[prod(x1)] | = | 0 |
[mult(x1, x2)] | = | 0 |
[z] | = | 0 |
[U41(x1, x2)] | = | 1 + 1 · x2 |
[U71(x1, x2, x3)] | = | 3 + 1 · x2 + 1 · x3 |
[singl(x1)] | = | 0 |
[empty] | = | 0 |
[union(x1, x2)] | = | 0 |
0(z) | → | z | (3) |
U51(tt,X,Y) | → | 0(plus(X,Y)) | (10) |
U41(tt,X) | → | X | (9) |
U71(tt,X,Y) | → | 0(plus(plus(X,Y),1(z))) | (12) |
plus(plus(0(X),1(Y)),ext) | → | plus(U61(and(isBin(X),isBin(Y)),X,Y),ext) | (160) |
plus(plus(0(X),0(Y)),ext) | → | plus(U51(and(isBin(X),isBin(Y)),X,Y),ext) | (159) |
plus(0(X),1(Y)) | → | U61(and(isBin(X),isBin(Y)),X,Y) | (31) |
plus(0(X),0(Y)) | → | U51(and(isBin(X),isBin(Y)),X,Y) | (30) |
plus(z,X) | → | U41(isBin(X),X) | (29) |
plus(plus(1(X),1(Y)),ext) | → | plus(U71(and(isBin(X),isBin(Y)),X,Y),ext) | (161) |
plus(1(X),1(Y)) | → | U71(and(isBin(X),isBin(Y)),X,Y) | (32) |
plus(plus(z,X),ext) | → | plus(U41(isBin(X),X),ext) | (158) |
U61(tt,X,Y) | → | 1(plus(X,Y)) | (11) |
plus(plus(x,y),z') | → | plus(x,plus(y,z')) | (43) |
plus(x,y) | → | plus(y,x) | (40) |
plus#(plus(x,y),z') | → | plus#(y,z') | (52) |
plus#(plus(0(X),0(Y)),ext) | → | U51#(and(isBin(X),isBin(Y)),X,Y) | (139) |
[plus#(x1, x2)] | = | 2 · x1 + 2 · x2 |
[plus(x1, x2)] | = | 1 · x1 + 1 · x2 |
[0(x1)] | = | 1 + 1 · x1 |
[1(x1)] | = | 1 + 1 · x1 |
[U61(x1, x2, x3)] | = | 1 + 1 · x2 + 1 · x3 |
[and(x1, x2)] | = | 0 |
[isBin(x1)] | = | 0 |
[U51(x1, x2, x3)] | = | 1 + 1 · x2 + 1 · x3 |
[U51#(x1, x2, x3)] | = | 2 · x2 + 2 · x3 |
[tt] | = | 0 |
[U41(x1, x2)] | = | 1 · x2 |
[z] | = | 0 |
[isBag(x1)] | = | 0 |
[singl(x1)] | = | 0 |
[empty] | = | 0 |
[union(x1, x2)] | = | 0 |
[sum(x1)] | = | 3 · x1 |
[prod(x1)] | = | 0 |
[mult(x1, x2)] | = | 0 |
[U71(x1, x2, x3)] | = | 2 + 1 · x2 + 1 · x3 |
U51(tt,X,Y) | → | 0(plus(X,Y)) | (10) |
U41(tt,X) | → | X | (9) |
0(z) | → | z | (3) |
U71(tt,X,Y) | → | 0(plus(plus(X,Y),1(z))) | (12) |
plus(plus(0(X),1(Y)),ext) | → | plus(U61(and(isBin(X),isBin(Y)),X,Y),ext) | (160) |
plus(plus(0(X),0(Y)),ext) | → | plus(U51(and(isBin(X),isBin(Y)),X,Y),ext) | (159) |
plus(0(X),1(Y)) | → | U61(and(isBin(X),isBin(Y)),X,Y) | (31) |
plus(0(X),0(Y)) | → | U51(and(isBin(X),isBin(Y)),X,Y) | (30) |
plus(z,X) | → | U41(isBin(X),X) | (29) |
plus(plus(1(X),1(Y)),ext) | → | plus(U71(and(isBin(X),isBin(Y)),X,Y),ext) | (161) |
plus(1(X),1(Y)) | → | U71(and(isBin(X),isBin(Y)),X,Y) | (32) |
plus(plus(z,X),ext) | → | plus(U41(isBin(X),X),ext) | (158) |
U61(tt,X,Y) | → | 1(plus(X,Y)) | (11) |
plus(plus(x,y),z') | → | plus(x,plus(y,z')) | (43) |
plus(x,y) | → | plus(y,x) | (40) |
plus#(plus(0(X),1(Y)),ext) | → | plus#(U61(and(isBin(X),isBin(Y)),X,Y),ext) | (143) |
plus#(plus(0(X),0(Y)),ext) | → | plus#(U51(and(isBin(X),isBin(Y)),X,Y),ext) | (138) |
plus#(0(X),0(Y)) | → | U51#(and(isBin(X),isBin(Y)),X,Y) | (97) |
The dependency pairs are split into 1 component.
plus#(x,y) | → | plus#(y,x) | (46) |
plus#(plus(x,y),z') | → | plus#(x,plus(y,z')) | (49) |
isBin#(0(V1)) | → | isBin#(V1) | (75) |
isBin#(1(V1)) | → | isBin#(V1) | (76) |
isBin#(mult(V1,V2)) | → | isBin#(V1) | (78) |
isBin#(mult(V1,V2)) | → | isBin#(V2) | (79) |
isBin#(plus(V1,V2)) | → | isBin#(V1) | (81) |
isBin#(plus(V1,V2)) | → | isBin#(V2) | (82) |
isBin#(prod(V1)) | → | isBag#(V1) | (83) |
isBag#(singl(V1)) | → | isBin#(V1) | (71) |
isBin#(sum(V1)) | → | isBag#(V1) | (84) |
isBag#(union(V1,V2)) | → | isBag#(V1) | (73) |
isBag#(union(V1,V2)) | → | isBag#(V2) | (74) |
[isBin#(x1)] | = | 1 · x1 |
[1(x1)] | = | 3 · x1 |
[plus(x1, x2)] | = | 3 · x1 + 3 · x2 |
[0(x1)] | = | 3 · x1 |
[sum(x1)] | = | 3 · x1 |
[isBag#(x1)] | = | 2 · x1 |
[union(x1, x2)] | = | 3 · x1 + 3 · x2 |
[mult(x1, x2)] | = | 3 · x1 + 3 · x2 |
[prod(x1)] | = | 3 · x1 |
[singl(x1)] | = | 3 · x1 |
isBin#(1(V1)) | → | isBin#(V1) | (76) |
isBin#(plus(V1,V2)) | → | isBin#(V1) | (81) |
isBin#(0(V1)) | → | isBin#(V1) | (75) |
isBin#(sum(V1)) | → | isBag#(V1) | (84) |
isBin#(plus(V1,V2)) | → | isBin#(V2) | (82) |
isBag#(union(V1,V2)) | → | isBag#(V2) | (74) |
isBin#(mult(V1,V2)) | → | isBin#(V1) | (78) |
isBin#(mult(V1,V2)) | → | isBin#(V2) | (79) |
isBin#(prod(V1)) | → | isBag#(V1) | (83) |
isBag#(singl(V1)) | → | isBin#(V1) | (71) |
isBag#(union(V1,V2)) | → | isBag#(V1) | (73) |
union(X,empty) | → | X | (1) |
union(empty,X) | → | X | (2) |
0(z) | → | z | (3) |
U101(tt,X) | → | X | (4) |
U11(tt) | → | z | (5) |
U111(tt,A,B) | → | plus(sum(A),sum(B)) | (6) |
U21(tt,X,Y) | → | 0(mult(X,Y)) | (7) |
U31(tt,X,Y) | → | plus(0(mult(X,Y)),Y) | (8) |
U41(tt,X) | → | X | (9) |
U51(tt,X,Y) | → | 0(plus(X,Y)) | (10) |
U61(tt,X,Y) | → | 1(plus(X,Y)) | (11) |
U71(tt,X,Y) | → | 0(plus(plus(X,Y),1(z))) | (12) |
U81(tt,X) | → | X | (13) |
U91(tt,A,B) | → | mult(prod(A),prod(B)) | (14) |
and(tt,X) | → | X | (15) |
isBag(empty) | → | tt | (16) |
isBag(singl(V1)) | → | isBin(V1) | (17) |
isBag(union(V1,V2)) | → | and(isBag(V1),isBag(V2)) | (18) |
isBin(z) | → | tt | (19) |
isBin(0(V1)) | → | isBin(V1) | (20) |
isBin(1(V1)) | → | isBin(V1) | (21) |
isBin(mult(V1,V2)) | → | and(isBin(V1),isBin(V2)) | (22) |
isBin(plus(V1,V2)) | → | and(isBin(V1),isBin(V2)) | (23) |
isBin(prod(V1)) | → | isBag(V1) | (24) |
isBin(sum(V1)) | → | isBag(V1) | (25) |
mult(z,X) | → | U11(isBin(X)) | (26) |
mult(0(X),Y) | → | U21(and(isBin(X),isBin(Y)),X,Y) | (27) |
mult(1(X),Y) | → | U31(and(isBin(X),isBin(Y)),X,Y) | (28) |
plus(z,X) | → | U41(isBin(X),X) | (29) |
plus(0(X),0(Y)) | → | U51(and(isBin(X),isBin(Y)),X,Y) | (30) |
plus(0(X),1(Y)) | → | U61(and(isBin(X),isBin(Y)),X,Y) | (31) |
plus(1(X),1(Y)) | → | U71(and(isBin(X),isBin(Y)),X,Y) | (32) |
prod(empty) | → | 1(z) | (33) |
prod(singl(X)) | → | U81(isBin(X),X) | (34) |
prod(union(A,B)) | → | U91(and(isBag(A),isBag(B)),A,B) | (35) |
sum(empty) | → | 0(z) | (36) |
sum(singl(X)) | → | U101(isBin(X),X) | (37) |
sum(union(A,B)) | → | U111(and(isBag(A),isBag(B)),A,B) | (38) |
mult(mult(z,X),ext) | → | mult(U11(isBin(X)),ext) | (155) |
mult(mult(0(X),Y),ext) | → | mult(U21(and(isBin(X),isBin(Y)),X,Y),ext) | (156) |
mult(mult(1(X),Y),ext) | → | mult(U31(and(isBin(X),isBin(Y)),X,Y),ext) | (157) |
plus(plus(z,X),ext) | → | plus(U41(isBin(X),X),ext) | (158) |
plus(plus(0(X),0(Y)),ext) | → | plus(U51(and(isBin(X),isBin(Y)),X,Y),ext) | (159) |
plus(plus(0(X),1(Y)),ext) | → | plus(U61(and(isBin(X),isBin(Y)),X,Y),ext) | (160) |
plus(plus(1(X),1(Y)),ext) | → | plus(U71(and(isBin(X),isBin(Y)),X,Y),ext) | (161) |
union(union(X,empty),ext) | → | union(X,ext) | (162) |
union(union(empty,X),ext) | → | union(X,ext) | (163) |
union#(union(empty,X),ext) | → | union#(X,ext) | (154) |
union#(union(X,empty),ext) | → | union#(X,ext) | (153) |
union#(union(x,y),z') | → | union#(y,z') | (53) |
union#(x,y) | → | union#(y,x) | (47) |
union#(union(x,y),z') | → | union#(x,union(y,z')) | (50) |
[union#(x1, x2)] | = | 3 · x1 + 3 · x2 |
[union(x1, x2)] | = | 1 · x1 + 1 · x2 |
[empty] | = | 0 |
union(X,empty) | → | X | (1) |
union(empty,X) | → | X | (2) |
union(union(X,empty),ext) | → | union(X,ext) | (162) |
union(union(empty,X),ext) | → | union(X,ext) | (163) |
union(union(x,y),z') | → | union(x,union(y,z')) | (44) |
union(x,y) | → | union(y,x) | (41) |
union#(union(empty,X),ext) | → | union#(X,ext) | (154) |
union#(union(X,empty),ext) | → | union#(X,ext) | (153) |
union(X,empty) | → | X | (1) |
union(empty,X) | → | X | (2) |
0(z) | → | z | (3) |
U101(tt,X) | → | X | (4) |
U11(tt) | → | z | (5) |
U111(tt,A,B) | → | plus(sum(A),sum(B)) | (6) |
U21(tt,X,Y) | → | 0(mult(X,Y)) | (7) |
U31(tt,X,Y) | → | plus(0(mult(X,Y)),Y) | (8) |
U41(tt,X) | → | X | (9) |
U51(tt,X,Y) | → | 0(plus(X,Y)) | (10) |
U61(tt,X,Y) | → | 1(plus(X,Y)) | (11) |
U71(tt,X,Y) | → | 0(plus(plus(X,Y),1(z))) | (12) |
U81(tt,X) | → | X | (13) |
U91(tt,A,B) | → | mult(prod(A),prod(B)) | (14) |
and(tt,X) | → | X | (15) |
isBag(empty) | → | tt | (16) |
isBag(singl(V1)) | → | isBin(V1) | (17) |
isBag(union(V1,V2)) | → | and(isBag(V1),isBag(V2)) | (18) |
isBin(z) | → | tt | (19) |
isBin(0(V1)) | → | isBin(V1) | (20) |
isBin(1(V1)) | → | isBin(V1) | (21) |
isBin(mult(V1,V2)) | → | and(isBin(V1),isBin(V2)) | (22) |
isBin(plus(V1,V2)) | → | and(isBin(V1),isBin(V2)) | (23) |
isBin(prod(V1)) | → | isBag(V1) | (24) |
isBin(sum(V1)) | → | isBag(V1) | (25) |
mult(z,X) | → | U11(isBin(X)) | (26) |
mult(0(X),Y) | → | U21(and(isBin(X),isBin(Y)),X,Y) | (27) |
mult(1(X),Y) | → | U31(and(isBin(X),isBin(Y)),X,Y) | (28) |
plus(z,X) | → | U41(isBin(X),X) | (29) |
plus(0(X),0(Y)) | → | U51(and(isBin(X),isBin(Y)),X,Y) | (30) |
plus(0(X),1(Y)) | → | U61(and(isBin(X),isBin(Y)),X,Y) | (31) |
plus(1(X),1(Y)) | → | U71(and(isBin(X),isBin(Y)),X,Y) | (32) |
prod(empty) | → | 1(z) | (33) |
prod(singl(X)) | → | U81(isBin(X),X) | (34) |
prod(union(A,B)) | → | U91(and(isBag(A),isBag(B)),A,B) | (35) |
sum(empty) | → | 0(z) | (36) |
sum(singl(X)) | → | U101(isBin(X),X) | (37) |
sum(union(A,B)) | → | U111(and(isBag(A),isBag(B)),A,B) | (38) |
mult(mult(z,X),ext) | → | mult(U11(isBin(X)),ext) | (155) |
mult(mult(0(X),Y),ext) | → | mult(U21(and(isBin(X),isBin(Y)),X,Y),ext) | (156) |
mult(mult(1(X),Y),ext) | → | mult(U31(and(isBin(X),isBin(Y)),X,Y),ext) | (157) |
plus(plus(z,X),ext) | → | plus(U41(isBin(X),X),ext) | (158) |
plus(plus(0(X),0(Y)),ext) | → | plus(U51(and(isBin(X),isBin(Y)),X,Y),ext) | (159) |
plus(plus(0(X),1(Y)),ext) | → | plus(U61(and(isBin(X),isBin(Y)),X,Y),ext) | (160) |
plus(plus(1(X),1(Y)),ext) | → | plus(U71(and(isBin(X),isBin(Y)),X,Y),ext) | (161) |
union(union(X,empty),ext) | → | union(X,ext) | (162) |
union(union(empty,X),ext) | → | union(X,ext) | (163) |
[union#(x1, x2)] | = | 3 · x1 + 3 · x2 |
[union(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[mult(x1, x2)] | = | 1 · x1 + 1 · x2 |
[plus(x1, x2)] | = | 1 · x1 + 1 · x2 |
mult(x,y) | → | mult(y,x) | (39) |
plus(x,y) | → | plus(y,x) | (40) |
union(x,y) | → | union(y,x) | (41) |
mult(mult(x,y),z') | → | mult(x,mult(y,z')) | (42) |
plus(plus(x,y),z') | → | plus(x,plus(y,z')) | (43) |
union(union(x,y),z') | → | union(x,union(y,z')) | (44) |
union#(union(x,y),z') | → | union#(y,z') | (53) |