Termination Proof using AProVE

YES Termination Proof using AProVETerm Rewriting System R:
[X, A, B, Y, V1, V2, y, z', x]
union(X, empty) -> X
union(empty, X) -> X
0(z) -> z
U101(tt, X) -> X
U11(tt) -> z
U111(tt, A, B) -> plus(sum(A), sum(B))
U21(tt, X, Y) -> 0(mult(X, Y))
U31(tt, X, Y) -> plus(0(mult(X, Y)), Y)
U41(tt, X) -> X
U51(tt, X, Y) -> 0(plus(X, Y))
U61(tt, X, Y) -> 1(plus(X, Y))
U71(tt, X, Y) -> 0(plus(plus(X, Y), 1(z)))
U81(tt, X) -> X
U91(tt, A, B) -> mult(prod(A), prod(B))
and(tt, X) -> X
isBag(empty) -> tt
isBag(singl(V1)) -> isBin(V1)
isBag(union(V1, V2)) -> and(isBag(V1), isBag(V2))
isBin(z) -> tt
isBin(0(V1)) -> isBin(V1)
isBin(1(V1)) -> isBin(V1)
isBin(mult(V1, V2)) -> and(isBin(V1), isBin(V2))
isBin(plus(V1, V2)) -> and(isBin(V1), isBin(V2))
isBin(prod(V1)) -> isBag(V1)
isBin(sum(V1)) -> isBag(V1)
mult(z, X) -> U11(isBin(X))
mult(0(X), Y) -> U21(and(isBin(X), isBin(Y)), X, Y)
mult(1(X), Y) -> U31(and(isBin(X), isBin(Y)), X, Y)
plus(z, X) -> U41(isBin(X), X)
plus(0(X), 0(Y)) -> U51(and(isBin(X), isBin(Y)), X, Y)
plus(0(X), 1(Y)) -> U61(and(isBin(X), isBin(Y)), X, Y)
plus(1(X), 1(Y)) -> U71(and(isBin(X), isBin(Y)), X, Y)
prod(empty) -> 1(z)
prod(singl(X)) -> U81(isBin(X), X)
prod(union(A, B)) -> U91(and(isBag(A), isBag(B)), A, B)
sum(empty) -> 0(z)
sum(singl(X)) -> U101(isBin(X), X)
sum(union(A, B)) -> U111(and(isBag(A), isBag(B)), A, B)
union(union(x, y), z') == union(x, union(y, z'))
union(x, y) == union(y, x)
mult(x, mult(y, z')) == mult(mult(x, y), z')
mult(x, y) == mult(y, x)
plus(plus(x, y), z') == plus(x, plus(y, z'))
plus(x, y) == plus(y, x)

Termination of R to be shown.

     ↳Dependency Pair Analysis

R contains the following Dependency Pairs:

U111'(tt, A, B) -> plus(sum(A), sum(B))
U111'(tt, A, B) -> SUM(A)
U111'(tt, A, B) -> SUM(B)
U21'(tt, X, Y) -> 0'(mult(X, Y))
U21'(tt, X, Y) -> mult(X, Y)
U31'(tt, X, Y) -> plus(0(mult(X, Y)), Y)
U31'(tt, X, Y) -> 0'(mult(X, Y))
U31'(tt, X, Y) -> mult(X, Y)
U51'(tt, X, Y) -> 0'(plus(X, Y))
U51'(tt, X, Y) -> plus(X, Y)
U61'(tt, X, Y) -> plus(X, Y)
U71'(tt, X, Y) -> 0'(plus(plus(X, Y), 1(z)))
U71'(tt, X, Y) -> plus(plus(X, Y), 1(z))
U71'(tt, X, Y) -> plus(X, Y)
U91'(tt, A, B) -> mult(prod(A), prod(B))
U91'(tt, A, B) -> PROD(A)
U91'(tt, A, B) -> PROD(B)
ISBAG(singl(V1)) -> ISBIN(V1)
ISBAG(union(V1, V2)) -> AND(isBag(V1), isBag(V2))
ISBAG(union(V1, V2)) -> ISBAG(V1)
ISBAG(union(V1, V2)) -> ISBAG(V2)
ISBIN(0(V1)) -> ISBIN(V1)
ISBIN(1(V1)) -> ISBIN(V1)
ISBIN(mult(V1, V2)) -> AND(isBin(V1), isBin(V2))
ISBIN(mult(V1, V2)) -> ISBIN(V1)
ISBIN(mult(V1, V2)) -> ISBIN(V2)
ISBIN(plus(V1, V2)) -> AND(isBin(V1), isBin(V2))
ISBIN(plus(V1, V2)) -> ISBIN(V1)
ISBIN(plus(V1, V2)) -> ISBIN(V2)
ISBIN(prod(V1)) -> ISBAG(V1)
ISBIN(sum(V1)) -> ISBAG(V1)
mult(z, X) -> U11'(isBin(X))
mult(z, X) -> ISBIN(X)
mult(0(X), Y) -> U21'(and(isBin(X), isBin(Y)), X, Y)
mult(0(X), Y) -> AND(isBin(X), isBin(Y))
mult(0(X), Y) -> ISBIN(X)
mult(0(X), Y) -> ISBIN(Y)
mult(1(X), Y) -> U31'(and(isBin(X), isBin(Y)), X, Y)
mult(1(X), Y) -> AND(isBin(X), isBin(Y))
mult(1(X), Y) -> ISBIN(X)
mult(1(X), Y) -> ISBIN(Y)
mult(mult(z, X), ext) -> mult(U11(isBin(X)), ext)
mult(mult(z, X), ext) -> U11'(isBin(X))
mult(mult(z, X), ext) -> ISBIN(X)
mult(mult(0(X), Y), ext) -> mult(U21(and(isBin(X), isBin(Y)), X, Y), ext)
mult(mult(0(X), Y), ext) -> U21'(and(isBin(X), isBin(Y)), X, Y)
mult(mult(0(X), Y), ext) -> AND(isBin(X), isBin(Y))
mult(mult(0(X), Y), ext) -> ISBIN(X)
mult(mult(0(X), Y), ext) -> ISBIN(Y)
mult(mult(1(X), Y), ext) -> mult(U31(and(isBin(X), isBin(Y)), X, Y), ext)
mult(mult(1(X), Y), ext) -> U31'(and(isBin(X), isBin(Y)), X, Y)
mult(mult(1(X), Y), ext) -> AND(isBin(X), isBin(Y))
mult(mult(1(X), Y), ext) -> ISBIN(X)
mult(mult(1(X), Y), ext) -> ISBIN(Y)
plus(z, X) -> U41'(isBin(X), X)
plus(z, X) -> ISBIN(X)
plus(0(X), 0(Y)) -> U51'(and(isBin(X), isBin(Y)), X, Y)
plus(0(X), 0(Y)) -> AND(isBin(X), isBin(Y))
plus(0(X), 0(Y)) -> ISBIN(X)
plus(0(X), 0(Y)) -> ISBIN(Y)
plus(0(X), 1(Y)) -> U61'(and(isBin(X), isBin(Y)), X, Y)
plus(0(X), 1(Y)) -> AND(isBin(X), isBin(Y))
plus(0(X), 1(Y)) -> ISBIN(X)
plus(0(X), 1(Y)) -> ISBIN(Y)
plus(1(X), 1(Y)) -> U71'(and(isBin(X), isBin(Y)), X, Y)
plus(1(X), 1(Y)) -> AND(isBin(X), isBin(Y))
plus(1(X), 1(Y)) -> ISBIN(X)
plus(1(X), 1(Y)) -> ISBIN(Y)
plus(plus(z, X), ext) -> plus(U41(isBin(X), X), ext)
plus(plus(z, X), ext) -> U41'(isBin(X), X)
plus(plus(z, X), ext) -> ISBIN(X)
plus(plus(0(X), 0(Y)), ext) -> plus(U51(and(isBin(X), isBin(Y)), X, Y), ext)
plus(plus(0(X), 0(Y)), ext) -> U51'(and(isBin(X), isBin(Y)), X, Y)
plus(plus(0(X), 0(Y)), ext) -> AND(isBin(X), isBin(Y))
plus(plus(0(X), 0(Y)), ext) -> ISBIN(X)
plus(plus(0(X), 0(Y)), ext) -> ISBIN(Y)
plus(plus(0(X), 1(Y)), ext) -> plus(U61(and(isBin(X), isBin(Y)), X, Y), ext)
plus(plus(0(X), 1(Y)), ext) -> U61'(and(isBin(X), isBin(Y)), X, Y)
plus(plus(0(X), 1(Y)), ext) -> AND(isBin(X), isBin(Y))
plus(plus(0(X), 1(Y)), ext) -> ISBIN(X)
plus(plus(0(X), 1(Y)), ext) -> ISBIN(Y)
plus(plus(1(X), 1(Y)), ext) -> plus(U71(and(isBin(X), isBin(Y)), X, Y), ext)
plus(plus(1(X), 1(Y)), ext) -> U71'(and(isBin(X), isBin(Y)), X, Y)
plus(plus(1(X), 1(Y)), ext) -> AND(isBin(X), isBin(Y))
plus(plus(1(X), 1(Y)), ext) -> ISBIN(X)
plus(plus(1(X), 1(Y)), ext) -> ISBIN(Y)
PROD(singl(X)) -> U81'(isBin(X), X)
PROD(singl(X)) -> ISBIN(X)
PROD(union(A, B)) -> U91'(and(isBag(A), isBag(B)), A, B)
PROD(union(A, B)) -> AND(isBag(A), isBag(B))
PROD(union(A, B)) -> ISBAG(A)
PROD(union(A, B)) -> ISBAG(B)
SUM(empty) -> 0'(z)
SUM(singl(X)) -> U101'(isBin(X), X)
SUM(singl(X)) -> ISBIN(X)
SUM(union(A, B)) -> U111'(and(isBag(A), isBag(B)), A, B)
SUM(union(A, B)) -> AND(isBag(A), isBag(B))
SUM(union(A, B)) -> ISBAG(A)
SUM(union(A, B)) -> ISBAG(B)

Furthermore, R contains five SCCs.

     ↳DPs

       →DP Problem 1

         ↳Polynomial Ordering

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polo

       →DP Problem 4

         ↳Polo

       →DP Problem 5

         ↳Polo

Dependency Pairs:

ISBAG(union(V1, V2)) -> ISBAG(V2)
ISBAG(union(V1, V2)) -> ISBAG(V1)
ISBIN(sum(V1)) -> ISBAG(V1)
ISBAG(singl(V1)) -> ISBIN(V1)
ISBIN(prod(V1)) -> ISBAG(V1)
ISBIN(plus(V1, V2)) -> ISBIN(V2)
ISBIN(plus(V1, V2)) -> ISBIN(V1)
ISBIN(mult(V1, V2)) -> ISBIN(V2)
ISBIN(mult(V1, V2)) -> ISBIN(V1)
ISBIN(1(V1)) -> ISBIN(V1)
ISBIN(0(V1)) -> ISBIN(V1)

Rules:

union(X, empty) -> X
union(empty, X) -> X
0(z) -> z
U101(tt, X) -> X
U11(tt) -> z
U111(tt, A, B) -> plus(sum(A), sum(B))
U21(tt, X, Y) -> 0(mult(X, Y))
U31(tt, X, Y) -> plus(0(mult(X, Y)), Y)
U41(tt, X) -> X
U51(tt, X, Y) -> 0(plus(X, Y))
U61(tt, X, Y) -> 1(plus(X, Y))
U71(tt, X, Y) -> 0(plus(plus(X, Y), 1(z)))
U81(tt, X) -> X
U91(tt, A, B) -> mult(prod(A), prod(B))
and(tt, X) -> X
isBag(empty) -> tt
isBag(singl(V1)) -> isBin(V1)
isBag(union(V1, V2)) -> and(isBag(V1), isBag(V2))
isBin(z) -> tt
isBin(0(V1)) -> isBin(V1)
isBin(1(V1)) -> isBin(V1)
isBin(mult(V1, V2)) -> and(isBin(V1), isBin(V2))
isBin(plus(V1, V2)) -> and(isBin(V1), isBin(V2))
isBin(prod(V1)) -> isBag(V1)
isBin(sum(V1)) -> isBag(V1)
mult(z, X) -> U11(isBin(X))
mult(0(X), Y) -> U21(and(isBin(X), isBin(Y)), X, Y)
mult(1(X), Y) -> U31(and(isBin(X), isBin(Y)), X, Y)
plus(z, X) -> U41(isBin(X), X)
plus(0(X), 0(Y)) -> U51(and(isBin(X), isBin(Y)), X, Y)
plus(0(X), 1(Y)) -> U61(and(isBin(X), isBin(Y)), X, Y)
plus(1(X), 1(Y)) -> U71(and(isBin(X), isBin(Y)), X, Y)
prod(empty) -> 1(z)
prod(singl(X)) -> U81(isBin(X), X)
prod(union(A, B)) -> U91(and(isBag(A), isBag(B)), A, B)
sum(empty) -> 0(z)
sum(singl(X)) -> U101(isBin(X), X)
sum(union(A, B)) -> U111(and(isBag(A), isBag(B)), A, B)

The following dependency pairs can be strictly oriented:

ISBIN(plus(V1, V2)) -> ISBIN(V2)
ISBIN(plus(V1, V2)) -> ISBIN(V1)

There are no usable rules using the Ce-refinement that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(mult(x₁, x₂)) = x₁ + x₂

POL(plus(x₁, x₂)) = 1 + x₁ + x₂

POL(0(x₁)) = x₁

POL(prod(x₁)) = x₁

POL(ISBAG(x₁)) = x₁

POL(union(x₁, x₂)) = x₁ + x₂

POL(1(x₁)) = x₁

POL(ISBIN(x₁)) = x₁

POL(sum(x₁)) = x₁

POL(singl(x₁)) = x₁

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Polo

           →DP Problem 6

             ↳Polynomial Ordering

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polo

       →DP Problem 4

         ↳Polo

       →DP Problem 5

         ↳Polo

Dependency Pairs:

ISBAG(union(V1, V2)) -> ISBAG(V2)
ISBAG(union(V1, V2)) -> ISBAG(V1)
ISBIN(sum(V1)) -> ISBAG(V1)
ISBAG(singl(V1)) -> ISBIN(V1)
ISBIN(prod(V1)) -> ISBAG(V1)
ISBIN(mult(V1, V2)) -> ISBIN(V2)
ISBIN(mult(V1, V2)) -> ISBIN(V1)
ISBIN(1(V1)) -> ISBIN(V1)
ISBIN(0(V1)) -> ISBIN(V1)

Rules:

union(X, empty) -> X
union(empty, X) -> X
0(z) -> z
U101(tt, X) -> X
U11(tt) -> z
U111(tt, A, B) -> plus(sum(A), sum(B))
U21(tt, X, Y) -> 0(mult(X, Y))
U31(tt, X, Y) -> plus(0(mult(X, Y)), Y)
U41(tt, X) -> X
U51(tt, X, Y) -> 0(plus(X, Y))
U61(tt, X, Y) -> 1(plus(X, Y))
U71(tt, X, Y) -> 0(plus(plus(X, Y), 1(z)))
U81(tt, X) -> X
U91(tt, A, B) -> mult(prod(A), prod(B))
and(tt, X) -> X
isBag(empty) -> tt
isBag(singl(V1)) -> isBin(V1)
isBag(union(V1, V2)) -> and(isBag(V1), isBag(V2))
isBin(z) -> tt
isBin(0(V1)) -> isBin(V1)
isBin(1(V1)) -> isBin(V1)
isBin(mult(V1, V2)) -> and(isBin(V1), isBin(V2))
isBin(plus(V1, V2)) -> and(isBin(V1), isBin(V2))
isBin(prod(V1)) -> isBag(V1)
isBin(sum(V1)) -> isBag(V1)
mult(z, X) -> U11(isBin(X))
mult(0(X), Y) -> U21(and(isBin(X), isBin(Y)), X, Y)
mult(1(X), Y) -> U31(and(isBin(X), isBin(Y)), X, Y)
plus(z, X) -> U41(isBin(X), X)
plus(0(X), 0(Y)) -> U51(and(isBin(X), isBin(Y)), X, Y)
plus(0(X), 1(Y)) -> U61(and(isBin(X), isBin(Y)), X, Y)
plus(1(X), 1(Y)) -> U71(and(isBin(X), isBin(Y)), X, Y)
prod(empty) -> 1(z)
prod(singl(X)) -> U81(isBin(X), X)
prod(union(A, B)) -> U91(and(isBag(A), isBag(B)), A, B)
sum(empty) -> 0(z)
sum(singl(X)) -> U101(isBin(X), X)
sum(union(A, B)) -> U111(and(isBag(A), isBag(B)), A, B)

The following dependency pairs can be strictly oriented:

ISBIN(mult(V1, V2)) -> ISBIN(V2)
ISBIN(mult(V1, V2)) -> ISBIN(V1)

There are no usable rules using the Ce-refinement that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(mult(x₁, x₂)) = 1 + x₁ + x₂

POL(0(x₁)) = x₁

POL(prod(x₁)) = x₁

POL(ISBAG(x₁)) = x₁

POL(union(x₁, x₂)) = x₁ + x₂

POL(1(x₁)) = x₁

POL(ISBIN(x₁)) = x₁

POL(sum(x₁)) = x₁

POL(singl(x₁)) = x₁

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Polo

           →DP Problem 6

             ↳Polo

...

               →DP Problem 12

                 ↳Polynomial Ordering

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polo

       →DP Problem 4

         ↳Polo

       →DP Problem 5

         ↳Polo

Dependency Pairs:

Rules:

union(X, empty) -> X
union(empty, X) -> X
0(z) -> z
U101(tt, X) -> X
U11(tt) -> z
U111(tt, A, B) -> plus(sum(A), sum(B))
U21(tt, X, Y) -> 0(mult(X, Y))
U31(tt, X, Y) -> plus(0(mult(X, Y)), Y)
U41(tt, X) -> X
U51(tt, X, Y) -> 0(plus(X, Y))
U61(tt, X, Y) -> 1(plus(X, Y))
U71(tt, X, Y) -> 0(plus(plus(X, Y), 1(z)))
U81(tt, X) -> X
U91(tt, A, B) -> mult(prod(A), prod(B))
and(tt, X) -> X
isBag(empty) -> tt
isBag(singl(V1)) -> isBin(V1)
isBag(union(V1, V2)) -> and(isBag(V1), isBag(V2))
isBin(z) -> tt
isBin(0(V1)) -> isBin(V1)
isBin(1(V1)) -> isBin(V1)
isBin(mult(V1, V2)) -> and(isBin(V1), isBin(V2))
isBin(plus(V1, V2)) -> and(isBin(V1), isBin(V2))
isBin(prod(V1)) -> isBag(V1)
isBin(sum(V1)) -> isBag(V1)
mult(z, X) -> U11(isBin(X))
mult(0(X), Y) -> U21(and(isBin(X), isBin(Y)), X, Y)
mult(1(X), Y) -> U31(and(isBin(X), isBin(Y)), X, Y)
plus(z, X) -> U41(isBin(X), X)
plus(0(X), 0(Y)) -> U51(and(isBin(X), isBin(Y)), X, Y)
plus(0(X), 1(Y)) -> U61(and(isBin(X), isBin(Y)), X, Y)
plus(1(X), 1(Y)) -> U71(and(isBin(X), isBin(Y)), X, Y)
prod(empty) -> 1(z)
prod(singl(X)) -> U81(isBin(X), X)
prod(union(A, B)) -> U91(and(isBag(A), isBag(B)), A, B)
sum(empty) -> 0(z)
sum(singl(X)) -> U101(isBin(X), X)
sum(union(A, B)) -> U111(and(isBag(A), isBag(B)), A, B)

The following dependency pair can be strictly oriented:

ISBIN(1(V1)) -> ISBIN(V1)

There are no usable rules using the Ce-refinement that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(0(x₁)) = x₁

POL(prod(x₁)) = x₁

POL(ISBAG(x₁)) = x₁

POL(union(x₁, x₂)) = x₁ + x₂

POL(1(x₁)) = 1 + x₁

POL(ISBIN(x₁)) = x₁

POL(sum(x₁)) = x₁

POL(singl(x₁)) = x₁

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Polo

           →DP Problem 6

             ↳Polo

...

               →DP Problem 14

                 ↳Polynomial Ordering

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polo

       →DP Problem 4

         ↳Polo

       →DP Problem 5

         ↳Polo

Dependency Pairs:

Rules:

union(X, empty) -> X
union(empty, X) -> X
0(z) -> z
U101(tt, X) -> X
U11(tt) -> z
U111(tt, A, B) -> plus(sum(A), sum(B))
U21(tt, X, Y) -> 0(mult(X, Y))
U31(tt, X, Y) -> plus(0(mult(X, Y)), Y)
U41(tt, X) -> X
U51(tt, X, Y) -> 0(plus(X, Y))
U61(tt, X, Y) -> 1(plus(X, Y))
U71(tt, X, Y) -> 0(plus(plus(X, Y), 1(z)))
U81(tt, X) -> X
U91(tt, A, B) -> mult(prod(A), prod(B))
and(tt, X) -> X
isBag(empty) -> tt
isBag(singl(V1)) -> isBin(V1)
isBag(union(V1, V2)) -> and(isBag(V1), isBag(V2))
isBin(z) -> tt
isBin(0(V1)) -> isBin(V1)
isBin(1(V1)) -> isBin(V1)
isBin(mult(V1, V2)) -> and(isBin(V1), isBin(V2))
isBin(plus(V1, V2)) -> and(isBin(V1), isBin(V2))
isBin(prod(V1)) -> isBag(V1)
isBin(sum(V1)) -> isBag(V1)
mult(z, X) -> U11(isBin(X))
mult(0(X), Y) -> U21(and(isBin(X), isBin(Y)), X, Y)
mult(1(X), Y) -> U31(and(isBin(X), isBin(Y)), X, Y)
plus(z, X) -> U41(isBin(X), X)
plus(0(X), 0(Y)) -> U51(and(isBin(X), isBin(Y)), X, Y)
plus(0(X), 1(Y)) -> U61(and(isBin(X), isBin(Y)), X, Y)
plus(1(X), 1(Y)) -> U71(and(isBin(X), isBin(Y)), X, Y)
prod(empty) -> 1(z)
prod(singl(X)) -> U81(isBin(X), X)
prod(union(A, B)) -> U91(and(isBag(A), isBag(B)), A, B)
sum(empty) -> 0(z)
sum(singl(X)) -> U101(isBin(X), X)
sum(union(A, B)) -> U111(and(isBag(A), isBag(B)), A, B)

The following dependency pair can be strictly oriented:

ISBIN(0(V1)) -> ISBIN(V1)

There are no usable rules using the Ce-refinement that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(0(x₁)) = 1 + x₁

POL(prod(x₁)) = x₁

POL(ISBAG(x₁)) = x₁

POL(union(x₁, x₂)) = x₁ + x₂

POL(ISBIN(x₁)) = x₁

POL(sum(x₁)) = x₁

POL(singl(x₁)) = x₁

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Polo

           →DP Problem 6

             ↳Polo

...

               →DP Problem 16

                 ↳Polynomial Ordering

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polo

       →DP Problem 4

         ↳Polo

       →DP Problem 5

         ↳Polo

Dependency Pairs:

ISBAG(union(V1, V2)) -> ISBAG(V2)
ISBAG(union(V1, V2)) -> ISBAG(V1)
ISBIN(sum(V1)) -> ISBAG(V1)
ISBAG(singl(V1)) -> ISBIN(V1)
ISBIN(prod(V1)) -> ISBAG(V1)

Rules:

union(X, empty) -> X
union(empty, X) -> X
0(z) -> z
U101(tt, X) -> X
U11(tt) -> z
U111(tt, A, B) -> plus(sum(A), sum(B))
U21(tt, X, Y) -> 0(mult(X, Y))
U31(tt, X, Y) -> plus(0(mult(X, Y)), Y)
U41(tt, X) -> X
U51(tt, X, Y) -> 0(plus(X, Y))
U61(tt, X, Y) -> 1(plus(X, Y))
U71(tt, X, Y) -> 0(plus(plus(X, Y), 1(z)))
U81(tt, X) -> X
U91(tt, A, B) -> mult(prod(A), prod(B))
and(tt, X) -> X
isBag(empty) -> tt
isBag(singl(V1)) -> isBin(V1)
isBag(union(V1, V2)) -> and(isBag(V1), isBag(V2))
isBin(z) -> tt
isBin(0(V1)) -> isBin(V1)
isBin(1(V1)) -> isBin(V1)
isBin(mult(V1, V2)) -> and(isBin(V1), isBin(V2))
isBin(plus(V1, V2)) -> and(isBin(V1), isBin(V2))
isBin(prod(V1)) -> isBag(V1)
isBin(sum(V1)) -> isBag(V1)
mult(z, X) -> U11(isBin(X))
mult(0(X), Y) -> U21(and(isBin(X), isBin(Y)), X, Y)
mult(1(X), Y) -> U31(and(isBin(X), isBin(Y)), X, Y)
plus(z, X) -> U41(isBin(X), X)
plus(0(X), 0(Y)) -> U51(and(isBin(X), isBin(Y)), X, Y)
plus(0(X), 1(Y)) -> U61(and(isBin(X), isBin(Y)), X, Y)
plus(1(X), 1(Y)) -> U71(and(isBin(X), isBin(Y)), X, Y)
prod(empty) -> 1(z)
prod(singl(X)) -> U81(isBin(X), X)
prod(union(A, B)) -> U91(and(isBag(A), isBag(B)), A, B)
sum(empty) -> 0(z)
sum(singl(X)) -> U101(isBin(X), X)
sum(union(A, B)) -> U111(and(isBag(A), isBag(B)), A, B)

The following dependency pairs can be strictly oriented:

ISBAG(union(V1, V2)) -> ISBAG(V2)
ISBAG(union(V1, V2)) -> ISBAG(V1)

There are no usable rules using the Ce-refinement that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(prod(x₁)) = x₁

POL(ISBAG(x₁)) = x₁

POL(union(x₁, x₂)) = 1 + x₁ + x₂

POL(ISBIN(x₁)) = x₁

POL(sum(x₁)) = x₁

POL(singl(x₁)) = x₁

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Polo

           →DP Problem 6

             ↳Polo

...

               →DP Problem 17

                 ↳Polynomial Ordering

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polo

       →DP Problem 4

         ↳Polo

       →DP Problem 5

         ↳Polo

Dependency Pairs:

ISBIN(sum(V1)) -> ISBAG(V1)
ISBAG(singl(V1)) -> ISBIN(V1)
ISBIN(prod(V1)) -> ISBAG(V1)

Rules:

union(X, empty) -> X
union(empty, X) -> X
0(z) -> z
U101(tt, X) -> X
U11(tt) -> z
U111(tt, A, B) -> plus(sum(A), sum(B))
U21(tt, X, Y) -> 0(mult(X, Y))
U31(tt, X, Y) -> plus(0(mult(X, Y)), Y)
U41(tt, X) -> X
U51(tt, X, Y) -> 0(plus(X, Y))
U61(tt, X, Y) -> 1(plus(X, Y))
U71(tt, X, Y) -> 0(plus(plus(X, Y), 1(z)))
U81(tt, X) -> X
U91(tt, A, B) -> mult(prod(A), prod(B))
and(tt, X) -> X
isBag(empty) -> tt
isBag(singl(V1)) -> isBin(V1)
isBag(union(V1, V2)) -> and(isBag(V1), isBag(V2))
isBin(z) -> tt
isBin(0(V1)) -> isBin(V1)
isBin(1(V1)) -> isBin(V1)
isBin(mult(V1, V2)) -> and(isBin(V1), isBin(V2))
isBin(plus(V1, V2)) -> and(isBin(V1), isBin(V2))
isBin(prod(V1)) -> isBag(V1)
isBin(sum(V1)) -> isBag(V1)
mult(z, X) -> U11(isBin(X))
mult(0(X), Y) -> U21(and(isBin(X), isBin(Y)), X, Y)
mult(1(X), Y) -> U31(and(isBin(X), isBin(Y)), X, Y)
plus(z, X) -> U41(isBin(X), X)
plus(0(X), 0(Y)) -> U51(and(isBin(X), isBin(Y)), X, Y)
plus(0(X), 1(Y)) -> U61(and(isBin(X), isBin(Y)), X, Y)
plus(1(X), 1(Y)) -> U71(and(isBin(X), isBin(Y)), X, Y)
prod(empty) -> 1(z)
prod(singl(X)) -> U81(isBin(X), X)
prod(union(A, B)) -> U91(and(isBag(A), isBag(B)), A, B)
sum(empty) -> 0(z)
sum(singl(X)) -> U101(isBin(X), X)
sum(union(A, B)) -> U111(and(isBag(A), isBag(B)), A, B)

The following dependency pair can be strictly oriented:

ISBIN(sum(V1)) -> ISBAG(V1)

There are no usable rules using the Ce-refinement that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(prod(x₁)) = x₁

POL(ISBAG(x₁)) = x₁

POL(ISBIN(x₁)) = x₁

POL(sum(x₁)) = 1 + x₁

POL(singl(x₁)) = x₁

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Polo

           →DP Problem 6

             ↳Polo

...

               →DP Problem 18

                 ↳Polynomial Ordering

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polo

       →DP Problem 4

         ↳Polo

       →DP Problem 5

         ↳Polo

Dependency Pairs:

ISBAG(singl(V1)) -> ISBIN(V1)
ISBIN(prod(V1)) -> ISBAG(V1)

Rules:

union(X, empty) -> X
union(empty, X) -> X
0(z) -> z
U101(tt, X) -> X
U11(tt) -> z
U111(tt, A, B) -> plus(sum(A), sum(B))
U21(tt, X, Y) -> 0(mult(X, Y))
U31(tt, X, Y) -> plus(0(mult(X, Y)), Y)
U41(tt, X) -> X
U51(tt, X, Y) -> 0(plus(X, Y))
U61(tt, X, Y) -> 1(plus(X, Y))
U71(tt, X, Y) -> 0(plus(plus(X, Y), 1(z)))
U81(tt, X) -> X
U91(tt, A, B) -> mult(prod(A), prod(B))
and(tt, X) -> X
isBag(empty) -> tt
isBag(singl(V1)) -> isBin(V1)
isBag(union(V1, V2)) -> and(isBag(V1), isBag(V2))
isBin(z) -> tt
isBin(0(V1)) -> isBin(V1)
isBin(1(V1)) -> isBin(V1)
isBin(mult(V1, V2)) -> and(isBin(V1), isBin(V2))
isBin(plus(V1, V2)) -> and(isBin(V1), isBin(V2))
isBin(prod(V1)) -> isBag(V1)
isBin(sum(V1)) -> isBag(V1)
mult(z, X) -> U11(isBin(X))
mult(0(X), Y) -> U21(and(isBin(X), isBin(Y)), X, Y)
mult(1(X), Y) -> U31(and(isBin(X), isBin(Y)), X, Y)
plus(z, X) -> U41(isBin(X), X)
plus(0(X), 0(Y)) -> U51(and(isBin(X), isBin(Y)), X, Y)
plus(0(X), 1(Y)) -> U61(and(isBin(X), isBin(Y)), X, Y)
plus(1(X), 1(Y)) -> U71(and(isBin(X), isBin(Y)), X, Y)
prod(empty) -> 1(z)
prod(singl(X)) -> U81(isBin(X), X)
prod(union(A, B)) -> U91(and(isBag(A), isBag(B)), A, B)
sum(empty) -> 0(z)
sum(singl(X)) -> U101(isBin(X), X)
sum(union(A, B)) -> U111(and(isBag(A), isBag(B)), A, B)

The following dependency pair can be strictly oriented:

ISBIN(prod(V1)) -> ISBAG(V1)

There are no usable rules using the Ce-refinement that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(prod(x₁)) = 1 + x₁

POL(ISBAG(x₁)) = x₁

POL(ISBIN(x₁)) = x₁

POL(singl(x₁)) = x₁

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Polo

           →DP Problem 6

             ↳Polo

...

               →DP Problem 19

                 ↳Dependency Graph

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polo

       →DP Problem 4

         ↳Polo

       →DP Problem 5

         ↳Polo

Dependency Pair:

ISBAG(singl(V1)) -> ISBIN(V1)

Rules:

union(X, empty) -> X
union(empty, X) -> X
0(z) -> z
U101(tt, X) -> X
U11(tt) -> z
U111(tt, A, B) -> plus(sum(A), sum(B))
U21(tt, X, Y) -> 0(mult(X, Y))
U31(tt, X, Y) -> plus(0(mult(X, Y)), Y)
U41(tt, X) -> X
U51(tt, X, Y) -> 0(plus(X, Y))
U61(tt, X, Y) -> 1(plus(X, Y))
U71(tt, X, Y) -> 0(plus(plus(X, Y), 1(z)))
U81(tt, X) -> X
U91(tt, A, B) -> mult(prod(A), prod(B))
and(tt, X) -> X
isBag(empty) -> tt
isBag(singl(V1)) -> isBin(V1)
isBag(union(V1, V2)) -> and(isBag(V1), isBag(V2))
isBin(z) -> tt
isBin(0(V1)) -> isBin(V1)
isBin(1(V1)) -> isBin(V1)
isBin(mult(V1, V2)) -> and(isBin(V1), isBin(V2))
isBin(plus(V1, V2)) -> and(isBin(V1), isBin(V2))
isBin(prod(V1)) -> isBag(V1)
isBin(sum(V1)) -> isBag(V1)
mult(z, X) -> U11(isBin(X))
mult(0(X), Y) -> U21(and(isBin(X), isBin(Y)), X, Y)
mult(1(X), Y) -> U31(and(isBin(X), isBin(Y)), X, Y)
plus(z, X) -> U41(isBin(X), X)
plus(0(X), 0(Y)) -> U51(and(isBin(X), isBin(Y)), X, Y)
plus(0(X), 1(Y)) -> U61(and(isBin(X), isBin(Y)), X, Y)
plus(1(X), 1(Y)) -> U71(and(isBin(X), isBin(Y)), X, Y)
prod(empty) -> 1(z)
prod(singl(X)) -> U81(isBin(X), X)
prod(union(A, B)) -> U91(and(isBag(A), isBag(B)), A, B)
sum(empty) -> 0(z)
sum(singl(X)) -> U101(isBin(X), X)
sum(union(A, B)) -> U111(and(isBag(A), isBag(B)), A, B)

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polynomial Ordering

       →DP Problem 3

         ↳Polo

       →DP Problem 4

         ↳Polo

       →DP Problem 5

         ↳Polo

Dependency Pairs:

U71'(tt, X, Y) -> plus(X, Y)
plus(plus(1(X), 1(Y)), ext) -> U71'(and(isBin(X), isBin(Y)), X, Y)
plus(plus(1(X), 1(Y)), ext) -> plus(U71(and(isBin(X), isBin(Y)), X, Y), ext)
plus(plus(0(X), 1(Y)), ext) -> U61'(and(isBin(X), isBin(Y)), X, Y)
plus(plus(0(X), 1(Y)), ext) -> plus(U61(and(isBin(X), isBin(Y)), X, Y), ext)
plus(plus(0(X), 0(Y)), ext) -> U51'(and(isBin(X), isBin(Y)), X, Y)
plus(plus(0(X), 0(Y)), ext) -> plus(U51(and(isBin(X), isBin(Y)), X, Y), ext)
plus(plus(z, X), ext) -> plus(U41(isBin(X), X), ext)
U71'(tt, X, Y) -> plus(plus(X, Y), 1(z))
plus(1(X), 1(Y)) -> U71'(and(isBin(X), isBin(Y)), X, Y)
U61'(tt, X, Y) -> plus(X, Y)
plus(0(X), 1(Y)) -> U61'(and(isBin(X), isBin(Y)), X, Y)
U51'(tt, X, Y) -> plus(X, Y)
plus(0(X), 0(Y)) -> U51'(and(isBin(X), isBin(Y)), X, Y)

Rules:

union(X, empty) -> X
union(empty, X) -> X
0(z) -> z
U101(tt, X) -> X
U11(tt) -> z
U111(tt, A, B) -> plus(sum(A), sum(B))
U21(tt, X, Y) -> 0(mult(X, Y))
U31(tt, X, Y) -> plus(0(mult(X, Y)), Y)
U41(tt, X) -> X
U51(tt, X, Y) -> 0(plus(X, Y))
U61(tt, X, Y) -> 1(plus(X, Y))
U71(tt, X, Y) -> 0(plus(plus(X, Y), 1(z)))
U81(tt, X) -> X
U91(tt, A, B) -> mult(prod(A), prod(B))
and(tt, X) -> X
isBag(empty) -> tt
isBag(singl(V1)) -> isBin(V1)
isBag(union(V1, V2)) -> and(isBag(V1), isBag(V2))
isBin(z) -> tt
isBin(0(V1)) -> isBin(V1)
isBin(1(V1)) -> isBin(V1)
isBin(mult(V1, V2)) -> and(isBin(V1), isBin(V2))
isBin(plus(V1, V2)) -> and(isBin(V1), isBin(V2))
isBin(prod(V1)) -> isBag(V1)
isBin(sum(V1)) -> isBag(V1)
mult(z, X) -> U11(isBin(X))
mult(0(X), Y) -> U21(and(isBin(X), isBin(Y)), X, Y)
mult(1(X), Y) -> U31(and(isBin(X), isBin(Y)), X, Y)
plus(z, X) -> U41(isBin(X), X)
plus(0(X), 0(Y)) -> U51(and(isBin(X), isBin(Y)), X, Y)
plus(0(X), 1(Y)) -> U61(and(isBin(X), isBin(Y)), X, Y)
plus(1(X), 1(Y)) -> U71(and(isBin(X), isBin(Y)), X, Y)
prod(empty) -> 1(z)
prod(singl(X)) -> U81(isBin(X), X)
prod(union(A, B)) -> U91(and(isBag(A), isBag(B)), A, B)
sum(empty) -> 0(z)
sum(singl(X)) -> U101(isBin(X), X)
sum(union(A, B)) -> U111(and(isBag(A), isBag(B)), A, B)

The following dependency pairs can be strictly oriented:

U71'(tt, X, Y) -> plus(X, Y)
plus(plus(1(X), 1(Y)), ext) -> U71'(and(isBin(X), isBin(Y)), X, Y)
plus(plus(1(X), 1(Y)), ext) -> plus(U71(and(isBin(X), isBin(Y)), X, Y), ext)
plus(plus(0(X), 1(Y)), ext) -> U61'(and(isBin(X), isBin(Y)), X, Y)
plus(1(X), 1(Y)) -> U71'(and(isBin(X), isBin(Y)), X, Y)
plus(0(X), 1(Y)) -> U61'(and(isBin(X), isBin(Y)), X, Y)

Additionally, the following usable rules using the Ce-refinement can be oriented:

plus(z, X) -> U41(isBin(X), X)
plus(0(X), 0(Y)) -> U51(and(isBin(X), isBin(Y)), X, Y)
plus(0(X), 1(Y)) -> U61(and(isBin(X), isBin(Y)), X, Y)
plus(1(X), 1(Y)) -> U71(and(isBin(X), isBin(Y)), X, Y)
U71(tt, X, Y) -> 0(plus(plus(X, Y), 1(z)))
U61(tt, X, Y) -> 1(plus(X, Y))
U51(tt, X, Y) -> 0(plus(X, Y))
and(tt, X) -> X
isBin(z) -> tt
isBin(0(V1)) -> isBin(V1)
isBin(1(V1)) -> isBin(V1)
isBin(mult(V1, V2)) -> and(isBin(V1), isBin(V2))
isBin(plus(V1, V2)) -> and(isBin(V1), isBin(V2))
isBin(prod(V1)) -> isBag(V1)
isBin(sum(V1)) -> isBag(V1)
isBag(empty) -> tt
isBag(singl(V1)) -> isBin(V1)
isBag(union(V1, V2)) -> and(isBag(V1), isBag(V2))
U41(tt, X) -> X
0(z) -> z

Oriented Equations:

plus(plus(x, y), z') == plus(x, plus(y, z'))
plus(x, y) == plus(y, x)

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(mult(x₁, x₂)) = 0

POL(U71(x₁, x₂, x₃)) = 1 + x₂ + x₃

POL(and(x₁, x₂)) = x₂

POL(plus(x₁, x₂)) = x₁ + x₂

POL(prod(x₁)) = 0

POL(z) = 0

POL(isBag(x₁)) = 0

POL(U51'(x₁, x₂, x₃)) = x₂ + x₃

POL(sum(x₁)) = 0

POL(isBin(x₁)) = 0

POL(U51(x₁, x₂, x₃)) = x₂ + x₃

POL(U41(x₁, x₂)) = x₂

POL(0(x₁)) = x₁

POL(1(x₁)) = 1 + x₁

POL(union(x₁, x₂)) = 0

POL(U71'(x₁, x₂, x₃)) = 1 + x₂ + x₃

POL(tt) = 0

POL(U61(x₁, x₂, x₃)) = 1 + x₂ + x₃

POL(U61'(x₁, x₂, x₃)) = x₂ + x₃

POL(empty) = 0

POL(singl(x₁)) = 0

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polo

           →DP Problem 7

             ↳Dependency Graph

       →DP Problem 3

         ↳Polo

       →DP Problem 4

         ↳Polo

       →DP Problem 5

         ↳Polo

Dependency Pairs:

plus(plus(0(X), 1(Y)), ext) -> plus(U61(and(isBin(X), isBin(Y)), X, Y), ext)
plus(plus(0(X), 0(Y)), ext) -> U51'(and(isBin(X), isBin(Y)), X, Y)
plus(plus(0(X), 0(Y)), ext) -> plus(U51(and(isBin(X), isBin(Y)), X, Y), ext)
plus(plus(z, X), ext) -> plus(U41(isBin(X), X), ext)
U71'(tt, X, Y) -> plus(plus(X, Y), 1(z))
U61'(tt, X, Y) -> plus(X, Y)
U51'(tt, X, Y) -> plus(X, Y)
plus(0(X), 0(Y)) -> U51'(and(isBin(X), isBin(Y)), X, Y)

Rules:

union(X, empty) -> X
union(empty, X) -> X
0(z) -> z
U101(tt, X) -> X
U11(tt) -> z
U111(tt, A, B) -> plus(sum(A), sum(B))
U21(tt, X, Y) -> 0(mult(X, Y))
U31(tt, X, Y) -> plus(0(mult(X, Y)), Y)
U41(tt, X) -> X
U51(tt, X, Y) -> 0(plus(X, Y))
U61(tt, X, Y) -> 1(plus(X, Y))
U71(tt, X, Y) -> 0(plus(plus(X, Y), 1(z)))
U81(tt, X) -> X
U91(tt, A, B) -> mult(prod(A), prod(B))
and(tt, X) -> X
isBag(empty) -> tt
isBag(singl(V1)) -> isBin(V1)
isBag(union(V1, V2)) -> and(isBag(V1), isBag(V2))
isBin(z) -> tt
isBin(0(V1)) -> isBin(V1)
isBin(1(V1)) -> isBin(V1)
isBin(mult(V1, V2)) -> and(isBin(V1), isBin(V2))
isBin(plus(V1, V2)) -> and(isBin(V1), isBin(V2))
isBin(prod(V1)) -> isBag(V1)
isBin(sum(V1)) -> isBag(V1)
mult(z, X) -> U11(isBin(X))
mult(0(X), Y) -> U21(and(isBin(X), isBin(Y)), X, Y)
mult(1(X), Y) -> U31(and(isBin(X), isBin(Y)), X, Y)
plus(z, X) -> U41(isBin(X), X)
plus(0(X), 0(Y)) -> U51(and(isBin(X), isBin(Y)), X, Y)
plus(0(X), 1(Y)) -> U61(and(isBin(X), isBin(Y)), X, Y)
plus(1(X), 1(Y)) -> U71(and(isBin(X), isBin(Y)), X, Y)
prod(empty) -> 1(z)
prod(singl(X)) -> U81(isBin(X), X)
prod(union(A, B)) -> U91(and(isBag(A), isBag(B)), A, B)
sum(empty) -> 0(z)
sum(singl(X)) -> U101(isBin(X), X)
sum(union(A, B)) -> U111(and(isBag(A), isBag(B)), A, B)

Using the Dependency Graph the DP problem was split into 1 DP problems.

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polo

           →DP Problem 7

             ↳DGraph

...

               →DP Problem 11

                 ↳Polynomial Ordering

       →DP Problem 3

         ↳Polo

       →DP Problem 4

         ↳Polo

       →DP Problem 5

         ↳Polo

Dependency Pairs:

plus(plus(0(X), 0(Y)), ext) -> U51'(and(isBin(X), isBin(Y)), X, Y)
plus(plus(0(X), 0(Y)), ext) -> plus(U51(and(isBin(X), isBin(Y)), X, Y), ext)
plus(plus(z, X), ext) -> plus(U41(isBin(X), X), ext)
U51'(tt, X, Y) -> plus(X, Y)
plus(0(X), 0(Y)) -> U51'(and(isBin(X), isBin(Y)), X, Y)
plus(plus(0(X), 1(Y)), ext) -> plus(U61(and(isBin(X), isBin(Y)), X, Y), ext)

Rules:

union(X, empty) -> X
union(empty, X) -> X
0(z) -> z
U101(tt, X) -> X
U11(tt) -> z
U111(tt, A, B) -> plus(sum(A), sum(B))
U21(tt, X, Y) -> 0(mult(X, Y))
U31(tt, X, Y) -> plus(0(mult(X, Y)), Y)
U41(tt, X) -> X
U51(tt, X, Y) -> 0(plus(X, Y))
U61(tt, X, Y) -> 1(plus(X, Y))
U71(tt, X, Y) -> 0(plus(plus(X, Y), 1(z)))
U81(tt, X) -> X
U91(tt, A, B) -> mult(prod(A), prod(B))
and(tt, X) -> X
isBag(empty) -> tt
isBag(singl(V1)) -> isBin(V1)
isBag(union(V1, V2)) -> and(isBag(V1), isBag(V2))
isBin(z) -> tt
isBin(0(V1)) -> isBin(V1)
isBin(1(V1)) -> isBin(V1)
isBin(mult(V1, V2)) -> and(isBin(V1), isBin(V2))
isBin(plus(V1, V2)) -> and(isBin(V1), isBin(V2))
isBin(prod(V1)) -> isBag(V1)
isBin(sum(V1)) -> isBag(V1)
mult(z, X) -> U11(isBin(X))
mult(0(X), Y) -> U21(and(isBin(X), isBin(Y)), X, Y)
mult(1(X), Y) -> U31(and(isBin(X), isBin(Y)), X, Y)
plus(z, X) -> U41(isBin(X), X)
plus(0(X), 0(Y)) -> U51(and(isBin(X), isBin(Y)), X, Y)
plus(0(X), 1(Y)) -> U61(and(isBin(X), isBin(Y)), X, Y)
plus(1(X), 1(Y)) -> U71(and(isBin(X), isBin(Y)), X, Y)
prod(empty) -> 1(z)
prod(singl(X)) -> U81(isBin(X), X)
prod(union(A, B)) -> U91(and(isBag(A), isBag(B)), A, B)
sum(empty) -> 0(z)
sum(singl(X)) -> U101(isBin(X), X)
sum(union(A, B)) -> U111(and(isBag(A), isBag(B)), A, B)

The following dependency pair can be strictly oriented:

plus(plus(z, X), ext) -> plus(U41(isBin(X), X), ext)

Additionally, the following usable rules using the Ce-refinement can be oriented:

and(tt, X) -> X
isBin(z) -> tt
isBin(0(V1)) -> isBin(V1)
isBin(1(V1)) -> isBin(V1)
isBin(mult(V1, V2)) -> and(isBin(V1), isBin(V2))
isBin(plus(V1, V2)) -> and(isBin(V1), isBin(V2))
isBin(prod(V1)) -> isBag(V1)
isBin(sum(V1)) -> isBag(V1)
isBag(empty) -> tt
isBag(singl(V1)) -> isBin(V1)
isBag(union(V1, V2)) -> and(isBag(V1), isBag(V2))
U51(tt, X, Y) -> 0(plus(X, Y))
plus(z, X) -> U41(isBin(X), X)
plus(0(X), 0(Y)) -> U51(and(isBin(X), isBin(Y)), X, Y)
plus(0(X), 1(Y)) -> U61(and(isBin(X), isBin(Y)), X, Y)
plus(1(X), 1(Y)) -> U71(and(isBin(X), isBin(Y)), X, Y)
U71(tt, X, Y) -> 0(plus(plus(X, Y), 1(z)))
U61(tt, X, Y) -> 1(plus(X, Y))
U41(tt, X) -> X
0(z) -> z

Oriented Equations:

plus(plus(x, y), z') == plus(x, plus(y, z'))
plus(x, y) == plus(y, x)

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(U71(x₁, x₂, x₃)) = 1 + x₁ + x₂ + x₃

POL(mult(x₁, x₂)) = 0

POL(and(x₁, x₂)) = x₂

POL(plus(x₁, x₂)) = x₁ + x₂

POL(prod(x₁)) = 0

POL(z) = 1

POL(isBag(x₁)) = 1

POL(U51'(x₁, x₂, x₃)) = x₂ + x₃

POL(sum(x₁)) = 0

POL(isBin(x₁)) = 1

POL(U51(x₁, x₂, x₃)) = x₂ + x₃

POL(0(x₁)) = x₁

POL(U41(x₁, x₂)) = x₂

POL(1(x₁)) = 1 + x₁

POL(union(x₁, x₂)) = x₁·x₂

POL(tt) = 1

POL(U61(x₁, x₂, x₃)) = 1 + x₂ + x₃

POL(empty) = 0

POL(singl(x₁)) = 0

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polo

           →DP Problem 7

             ↳DGraph

...

               →DP Problem 13

                 ↳Polynomial Ordering

       →DP Problem 3

         ↳Polo

       →DP Problem 4

         ↳Polo

       →DP Problem 5

         ↳Polo

Dependency Pairs:

plus(plus(0(X), 0(Y)), ext) -> U51'(and(isBin(X), isBin(Y)), X, Y)
plus(plus(0(X), 0(Y)), ext) -> plus(U51(and(isBin(X), isBin(Y)), X, Y), ext)
U51'(tt, X, Y) -> plus(X, Y)
plus(0(X), 0(Y)) -> U51'(and(isBin(X), isBin(Y)), X, Y)
plus(plus(0(X), 1(Y)), ext) -> plus(U61(and(isBin(X), isBin(Y)), X, Y), ext)

Rules:

union(X, empty) -> X
union(empty, X) -> X
0(z) -> z
U101(tt, X) -> X
U11(tt) -> z
U111(tt, A, B) -> plus(sum(A), sum(B))
U21(tt, X, Y) -> 0(mult(X, Y))
U31(tt, X, Y) -> plus(0(mult(X, Y)), Y)
U41(tt, X) -> X
U51(tt, X, Y) -> 0(plus(X, Y))
U61(tt, X, Y) -> 1(plus(X, Y))
U71(tt, X, Y) -> 0(plus(plus(X, Y), 1(z)))
U81(tt, X) -> X
U91(tt, A, B) -> mult(prod(A), prod(B))
and(tt, X) -> X
isBag(empty) -> tt
isBag(singl(V1)) -> isBin(V1)
isBag(union(V1, V2)) -> and(isBag(V1), isBag(V2))
isBin(z) -> tt
isBin(0(V1)) -> isBin(V1)
isBin(1(V1)) -> isBin(V1)
isBin(mult(V1, V2)) -> and(isBin(V1), isBin(V2))
isBin(plus(V1, V2)) -> and(isBin(V1), isBin(V2))
isBin(prod(V1)) -> isBag(V1)
isBin(sum(V1)) -> isBag(V1)
mult(z, X) -> U11(isBin(X))
mult(0(X), Y) -> U21(and(isBin(X), isBin(Y)), X, Y)
mult(1(X), Y) -> U31(and(isBin(X), isBin(Y)), X, Y)
plus(z, X) -> U41(isBin(X), X)
plus(0(X), 0(Y)) -> U51(and(isBin(X), isBin(Y)), X, Y)
plus(0(X), 1(Y)) -> U61(and(isBin(X), isBin(Y)), X, Y)
plus(1(X), 1(Y)) -> U71(and(isBin(X), isBin(Y)), X, Y)
prod(empty) -> 1(z)
prod(singl(X)) -> U81(isBin(X), X)
prod(union(A, B)) -> U91(and(isBag(A), isBag(B)), A, B)
sum(empty) -> 0(z)
sum(singl(X)) -> U101(isBin(X), X)
sum(union(A, B)) -> U111(and(isBag(A), isBag(B)), A, B)

The following dependency pairs can be strictly oriented:

plus(plus(0(X), 0(Y)), ext) -> U51'(and(isBin(X), isBin(Y)), X, Y)
plus(plus(0(X), 0(Y)), ext) -> plus(U51(and(isBin(X), isBin(Y)), X, Y), ext)
plus(0(X), 0(Y)) -> U51'(and(isBin(X), isBin(Y)), X, Y)
plus(plus(0(X), 1(Y)), ext) -> plus(U61(and(isBin(X), isBin(Y)), X, Y), ext)

Additionally, the following usable rules using the Ce-refinement can be oriented:

and(tt, X) -> X
isBin(z) -> tt
isBin(0(V1)) -> isBin(V1)
isBin(1(V1)) -> isBin(V1)
isBin(mult(V1, V2)) -> and(isBin(V1), isBin(V2))
isBin(plus(V1, V2)) -> and(isBin(V1), isBin(V2))
isBin(prod(V1)) -> isBag(V1)
isBin(sum(V1)) -> isBag(V1)
isBag(empty) -> tt
isBag(singl(V1)) -> isBin(V1)
isBag(union(V1, V2)) -> and(isBag(V1), isBag(V2))
U51(tt, X, Y) -> 0(plus(X, Y))
plus(z, X) -> U41(isBin(X), X)
plus(0(X), 0(Y)) -> U51(and(isBin(X), isBin(Y)), X, Y)
plus(0(X), 1(Y)) -> U61(and(isBin(X), isBin(Y)), X, Y)
plus(1(X), 1(Y)) -> U71(and(isBin(X), isBin(Y)), X, Y)
U71(tt, X, Y) -> 0(plus(plus(X, Y), 1(z)))
U61(tt, X, Y) -> 1(plus(X, Y))
0(z) -> z
U41(tt, X) -> X

Oriented Equations:

plus(plus(x, y), z') == plus(x, plus(y, z'))
plus(x, y) == plus(y, x)

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(U71(x₁, x₂, x₃)) = 1 + x₁ + x₂ + x₃

POL(mult(x₁, x₂)) = 0

POL(and(x₁, x₂)) = x₂

POL(plus(x₁, x₂)) = x₁ + x₂

POL(prod(x₁)) = 0

POL(z) = 0

POL(isBag(x₁)) = 1

POL(U51'(x₁, x₂, x₃)) = x₂ + x₃

POL(sum(x₁)) = 0

POL(isBin(x₁)) = 1

POL(U51(x₁, x₂, x₃)) = 1 + x₂ + x₃

POL(U41(x₁, x₂)) = x₂

POL(0(x₁)) = 1 + x₁

POL(1(x₁)) = 1 + x₁

POL(union(x₁, x₂)) = x₁·x₂

POL(tt) = 1

POL(U61(x₁, x₂, x₃)) = 1 + x₂ + x₃

POL(empty) = 0

POL(singl(x₁)) = 0

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polo

           →DP Problem 7

             ↳DGraph

...

               →DP Problem 15

                 ↳Dependency Graph

       →DP Problem 3

         ↳Polo

       →DP Problem 4

         ↳Polo

       →DP Problem 5

         ↳Polo

Dependency Pair:

U51'(tt, X, Y) -> plus(X, Y)

Rules:

union(X, empty) -> X
union(empty, X) -> X
0(z) -> z
U101(tt, X) -> X
U11(tt) -> z
U111(tt, A, B) -> plus(sum(A), sum(B))
U21(tt, X, Y) -> 0(mult(X, Y))
U31(tt, X, Y) -> plus(0(mult(X, Y)), Y)
U41(tt, X) -> X
U51(tt, X, Y) -> 0(plus(X, Y))
U61(tt, X, Y) -> 1(plus(X, Y))
U71(tt, X, Y) -> 0(plus(plus(X, Y), 1(z)))
U81(tt, X) -> X
U91(tt, A, B) -> mult(prod(A), prod(B))
and(tt, X) -> X
isBag(empty) -> tt
isBag(singl(V1)) -> isBin(V1)
isBag(union(V1, V2)) -> and(isBag(V1), isBag(V2))
isBin(z) -> tt
isBin(0(V1)) -> isBin(V1)
isBin(1(V1)) -> isBin(V1)
isBin(mult(V1, V2)) -> and(isBin(V1), isBin(V2))
isBin(plus(V1, V2)) -> and(isBin(V1), isBin(V2))
isBin(prod(V1)) -> isBag(V1)
isBin(sum(V1)) -> isBag(V1)
mult(z, X) -> U11(isBin(X))
mult(0(X), Y) -> U21(and(isBin(X), isBin(Y)), X, Y)
mult(1(X), Y) -> U31(and(isBin(X), isBin(Y)), X, Y)
plus(z, X) -> U41(isBin(X), X)
plus(0(X), 0(Y)) -> U51(and(isBin(X), isBin(Y)), X, Y)
plus(0(X), 1(Y)) -> U61(and(isBin(X), isBin(Y)), X, Y)
plus(1(X), 1(Y)) -> U71(and(isBin(X), isBin(Y)), X, Y)
prod(empty) -> 1(z)
prod(singl(X)) -> U81(isBin(X), X)
prod(union(A, B)) -> U91(and(isBag(A), isBag(B)), A, B)
sum(empty) -> 0(z)
sum(singl(X)) -> U101(isBin(X), X)
sum(union(A, B)) -> U111(and(isBag(A), isBag(B)), A, B)

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polynomial Ordering

       →DP Problem 4

         ↳Polo

       →DP Problem 5

         ↳Polo

Dependency Pairs:

U111'(tt, A, B) -> SUM(B)
SUM(union(A, B)) -> U111'(and(isBag(A), isBag(B)), A, B)
U111'(tt, A, B) -> SUM(A)

Rules:

union(X, empty) -> X
union(empty, X) -> X
0(z) -> z
U101(tt, X) -> X
U11(tt) -> z
U111(tt, A, B) -> plus(sum(A), sum(B))
U21(tt, X, Y) -> 0(mult(X, Y))
U31(tt, X, Y) -> plus(0(mult(X, Y)), Y)
U41(tt, X) -> X
U51(tt, X, Y) -> 0(plus(X, Y))
U61(tt, X, Y) -> 1(plus(X, Y))
U71(tt, X, Y) -> 0(plus(plus(X, Y), 1(z)))
U81(tt, X) -> X
U91(tt, A, B) -> mult(prod(A), prod(B))
and(tt, X) -> X
isBag(empty) -> tt
isBag(singl(V1)) -> isBin(V1)
isBag(union(V1, V2)) -> and(isBag(V1), isBag(V2))
isBin(z) -> tt
isBin(0(V1)) -> isBin(V1)
isBin(1(V1)) -> isBin(V1)
isBin(mult(V1, V2)) -> and(isBin(V1), isBin(V2))
isBin(plus(V1, V2)) -> and(isBin(V1), isBin(V2))
isBin(prod(V1)) -> isBag(V1)
isBin(sum(V1)) -> isBag(V1)
mult(z, X) -> U11(isBin(X))
mult(0(X), Y) -> U21(and(isBin(X), isBin(Y)), X, Y)
mult(1(X), Y) -> U31(and(isBin(X), isBin(Y)), X, Y)
plus(z, X) -> U41(isBin(X), X)
plus(0(X), 0(Y)) -> U51(and(isBin(X), isBin(Y)), X, Y)
plus(0(X), 1(Y)) -> U61(and(isBin(X), isBin(Y)), X, Y)
plus(1(X), 1(Y)) -> U71(and(isBin(X), isBin(Y)), X, Y)
prod(empty) -> 1(z)
prod(singl(X)) -> U81(isBin(X), X)
prod(union(A, B)) -> U91(and(isBag(A), isBag(B)), A, B)
sum(empty) -> 0(z)
sum(singl(X)) -> U101(isBin(X), X)
sum(union(A, B)) -> U111(and(isBag(A), isBag(B)), A, B)

The following dependency pair can be strictly oriented:

SUM(union(A, B)) -> U111'(and(isBag(A), isBag(B)), A, B)

Additionally, the following usable rules using the Ce-refinement can be oriented:

and(tt, X) -> X
isBag(empty) -> tt
isBag(singl(V1)) -> isBin(V1)
isBag(union(V1, V2)) -> and(isBag(V1), isBag(V2))
isBin(z) -> tt
isBin(0(V1)) -> isBin(V1)
isBin(1(V1)) -> isBin(V1)
isBin(mult(V1, V2)) -> and(isBin(V1), isBin(V2))
isBin(plus(V1, V2)) -> and(isBin(V1), isBin(V2))
isBin(prod(V1)) -> isBag(V1)
isBin(sum(V1)) -> isBag(V1)

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(mult(x₁, x₂)) = 0

POL(and(x₁, x₂)) = x₂

POL(plus(x₁, x₂)) = 0

POL(prod(x₁)) = 0

POL(z) = 0

POL(isBag(x₁)) = 0

POL(sum(x₁)) = 0

POL(isBin(x₁)) = 0

POL(U111'(x₁, x₂, x₃)) = x₂ + x₃

POL(SUM(x₁)) = x₁

POL(0(x₁)) = 0

POL(union(x₁, x₂)) = 1 + x₁ + x₂

POL(1(x₁)) = 0

POL(tt) = 0

POL(empty) = 0

POL(singl(x₁)) = 0

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polo

           →DP Problem 8

             ↳Dependency Graph

       →DP Problem 4

         ↳Polo

       →DP Problem 5

         ↳Polo

Dependency Pairs:

U111'(tt, A, B) -> SUM(B)
U111'(tt, A, B) -> SUM(A)

Rules:

union(X, empty) -> X
union(empty, X) -> X
0(z) -> z
U101(tt, X) -> X
U11(tt) -> z
U111(tt, A, B) -> plus(sum(A), sum(B))
U21(tt, X, Y) -> 0(mult(X, Y))
U31(tt, X, Y) -> plus(0(mult(X, Y)), Y)
U41(tt, X) -> X
U51(tt, X, Y) -> 0(plus(X, Y))
U61(tt, X, Y) -> 1(plus(X, Y))
U71(tt, X, Y) -> 0(plus(plus(X, Y), 1(z)))
U81(tt, X) -> X
U91(tt, A, B) -> mult(prod(A), prod(B))
and(tt, X) -> X
isBag(empty) -> tt
isBag(singl(V1)) -> isBin(V1)
isBag(union(V1, V2)) -> and(isBag(V1), isBag(V2))
isBin(z) -> tt
isBin(0(V1)) -> isBin(V1)
isBin(1(V1)) -> isBin(V1)
isBin(mult(V1, V2)) -> and(isBin(V1), isBin(V2))
isBin(plus(V1, V2)) -> and(isBin(V1), isBin(V2))
isBin(prod(V1)) -> isBag(V1)
isBin(sum(V1)) -> isBag(V1)
mult(z, X) -> U11(isBin(X))
mult(0(X), Y) -> U21(and(isBin(X), isBin(Y)), X, Y)
mult(1(X), Y) -> U31(and(isBin(X), isBin(Y)), X, Y)
plus(z, X) -> U41(isBin(X), X)
plus(0(X), 0(Y)) -> U51(and(isBin(X), isBin(Y)), X, Y)
plus(0(X), 1(Y)) -> U61(and(isBin(X), isBin(Y)), X, Y)
plus(1(X), 1(Y)) -> U71(and(isBin(X), isBin(Y)), X, Y)
prod(empty) -> 1(z)
prod(singl(X)) -> U81(isBin(X), X)
prod(union(A, B)) -> U91(and(isBag(A), isBag(B)), A, B)
sum(empty) -> 0(z)
sum(singl(X)) -> U101(isBin(X), X)
sum(union(A, B)) -> U111(and(isBag(A), isBag(B)), A, B)

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polo

       →DP Problem 4

         ↳Polynomial Ordering

       →DP Problem 5

         ↳Polo

Dependency Pairs:

mult(mult(1(X), Y), ext) -> U31'(and(isBin(X), isBin(Y)), X, Y)
mult(mult(1(X), Y), ext) -> mult(U31(and(isBin(X), isBin(Y)), X, Y), ext)
mult(mult(0(X), Y), ext) -> U21'(and(isBin(X), isBin(Y)), X, Y)
mult(mult(0(X), Y), ext) -> mult(U21(and(isBin(X), isBin(Y)), X, Y), ext)
mult(mult(z, X), ext) -> mult(U11(isBin(X)), ext)
U31'(tt, X, Y) -> mult(X, Y)
mult(1(X), Y) -> U31'(and(isBin(X), isBin(Y)), X, Y)
mult(0(X), Y) -> U21'(and(isBin(X), isBin(Y)), X, Y)
U21'(tt, X, Y) -> mult(X, Y)

Rules:

union(X, empty) -> X
union(empty, X) -> X
0(z) -> z
U101(tt, X) -> X
U11(tt) -> z
U111(tt, A, B) -> plus(sum(A), sum(B))
U21(tt, X, Y) -> 0(mult(X, Y))
U31(tt, X, Y) -> plus(0(mult(X, Y)), Y)
U41(tt, X) -> X
U51(tt, X, Y) -> 0(plus(X, Y))
U61(tt, X, Y) -> 1(plus(X, Y))
U71(tt, X, Y) -> 0(plus(plus(X, Y), 1(z)))
U81(tt, X) -> X
U91(tt, A, B) -> mult(prod(A), prod(B))
and(tt, X) -> X
isBag(empty) -> tt
isBag(singl(V1)) -> isBin(V1)
isBag(union(V1, V2)) -> and(isBag(V1), isBag(V2))
isBin(z) -> tt
isBin(0(V1)) -> isBin(V1)
isBin(1(V1)) -> isBin(V1)
isBin(mult(V1, V2)) -> and(isBin(V1), isBin(V2))
isBin(plus(V1, V2)) -> and(isBin(V1), isBin(V2))
isBin(prod(V1)) -> isBag(V1)
isBin(sum(V1)) -> isBag(V1)
mult(z, X) -> U11(isBin(X))
mult(0(X), Y) -> U21(and(isBin(X), isBin(Y)), X, Y)
mult(1(X), Y) -> U31(and(isBin(X), isBin(Y)), X, Y)
plus(z, X) -> U41(isBin(X), X)
plus(0(X), 0(Y)) -> U51(and(isBin(X), isBin(Y)), X, Y)
plus(0(X), 1(Y)) -> U61(and(isBin(X), isBin(Y)), X, Y)
plus(1(X), 1(Y)) -> U71(and(isBin(X), isBin(Y)), X, Y)
prod(empty) -> 1(z)
prod(singl(X)) -> U81(isBin(X), X)
prod(union(A, B)) -> U91(and(isBag(A), isBag(B)), A, B)
sum(empty) -> 0(z)
sum(singl(X)) -> U101(isBin(X), X)
sum(union(A, B)) -> U111(and(isBag(A), isBag(B)), A, B)

The following dependency pairs can be strictly oriented:

U21'(tt, X, Y) -> mult(X, Y)
mult(mult(z, X), ext) -> mult(U11(isBin(X)), ext)
mult(mult(0(X), Y), ext) -> U21'(and(isBin(X), isBin(Y)), X, Y)
mult(mult(1(X), Y), ext) -> mult(U31(and(isBin(X), isBin(Y)), X, Y), ext)
mult(0(X), Y) -> U21'(and(isBin(X), isBin(Y)), X, Y)
mult(1(X), Y) -> U31'(and(isBin(X), isBin(Y)), X, Y)
U31'(tt, X, Y) -> mult(X, Y)
mult(mult(1(X), Y), ext) -> U31'(and(isBin(X), isBin(Y)), X, Y)
mult(mult(0(X), Y), ext) -> mult(U21(and(isBin(X), isBin(Y)), X, Y), ext)

Additionally, the following usable rules using the Ce-refinement can be oriented:

and(tt, X) -> X
isBin(z) -> tt
isBin(0(V1)) -> isBin(V1)
isBin(1(V1)) -> isBin(V1)
isBin(mult(V1, V2)) -> and(isBin(V1), isBin(V2))
isBin(plus(V1, V2)) -> and(isBin(V1), isBin(V2))
isBin(prod(V1)) -> isBag(V1)
isBin(sum(V1)) -> isBag(V1)
isBag(empty) -> tt
isBag(singl(V1)) -> isBin(V1)
isBag(union(V1, V2)) -> and(isBag(V1), isBag(V2))
U31(tt, X, Y) -> plus(0(mult(X, Y)), Y)
mult(z, X) -> U11(isBin(X))
mult(0(X), Y) -> U21(and(isBin(X), isBin(Y)), X, Y)
mult(1(X), Y) -> U31(and(isBin(X), isBin(Y)), X, Y)
U21(tt, X, Y) -> 0(mult(X, Y))
U11(tt) -> z
plus(z, X) -> U41(isBin(X), X)
plus(0(X), 0(Y)) -> U51(and(isBin(X), isBin(Y)), X, Y)
plus(0(X), 1(Y)) -> U61(and(isBin(X), isBin(Y)), X, Y)
plus(1(X), 1(Y)) -> U71(and(isBin(X), isBin(Y)), X, Y)
0(z) -> z
U71(tt, X, Y) -> 0(plus(plus(X, Y), 1(z)))
U61(tt, X, Y) -> 1(plus(X, Y))
U51(tt, X, Y) -> 0(plus(X, Y))
U41(tt, X) -> X

Oriented Equations:

mult(x, mult(y, z')) == mult(mult(x, y), z')
mult(x, y) == mult(y, x)
plus(plus(x, y), z') == plus(x, plus(y, z'))
plus(x, y) == plus(y, x)

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(U71(x₁, x₂, x₃)) = 2 + x₂ + x₃

POL(mult(x₁, x₂)) = 1 + 2·x₁ + 2·x₁·x₂ + 2·x₂

POL(and(x₁, x₂)) = x₂

POL(plus(x₁, x₂)) = x₁ + x₂

POL(prod(x₁)) = 0

POL(U31(x₁, x₂, x₃)) = 2 + 2·x₁·x₃ + 2·x₂ + 2·x₂·x₃

POL(z) = 0

POL(isBag(x₁)) = 2

POL(sum(x₁)) = 0

POL(U31'(x₁, x₂, x₃)) = 2 + 2·x₂ + 2·x₂·x₃ + 2·x₃

POL(U11(x₁)) = 0

POL(U51(x₁, x₂, x₃)) = 1 + x₂ + x₃

POL(isBin(x₁)) = 2

POL(0(x₁)) = 1 + x₁

POL(U41(x₁, x₂)) = x₂

POL(U21(x₁, x₂, x₃)) = 2 + 2·x₂ + 2·x₂·x₃ + 2·x₃

POL(1(x₁)) = 1 + x₁

POL(union(x₁, x₂)) = 0

POL(tt) = 2

POL(U21'(x₁, x₂, x₃)) = 2 + 2·x₂ + 2·x₂·x₃ + 2·x₃

POL(U61(x₁, x₂, x₃)) = 1 + x₂ + x₃

POL(empty) = 0

POL(singl(x₁)) = 0

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polo

       →DP Problem 4

         ↳Polo

           →DP Problem 9

             ↳Dependency Graph

       →DP Problem 5

         ↳Polo

Dependency Pair:

Rules:

union(X, empty) -> X
union(empty, X) -> X
0(z) -> z
U101(tt, X) -> X
U11(tt) -> z
U111(tt, A, B) -> plus(sum(A), sum(B))
U21(tt, X, Y) -> 0(mult(X, Y))
U31(tt, X, Y) -> plus(0(mult(X, Y)), Y)
U41(tt, X) -> X
U51(tt, X, Y) -> 0(plus(X, Y))
U61(tt, X, Y) -> 1(plus(X, Y))
U71(tt, X, Y) -> 0(plus(plus(X, Y), 1(z)))
U81(tt, X) -> X
U91(tt, A, B) -> mult(prod(A), prod(B))
and(tt, X) -> X
isBag(empty) -> tt
isBag(singl(V1)) -> isBin(V1)
isBag(union(V1, V2)) -> and(isBag(V1), isBag(V2))
isBin(z) -> tt
isBin(0(V1)) -> isBin(V1)
isBin(1(V1)) -> isBin(V1)
isBin(mult(V1, V2)) -> and(isBin(V1), isBin(V2))
isBin(plus(V1, V2)) -> and(isBin(V1), isBin(V2))
isBin(prod(V1)) -> isBag(V1)
isBin(sum(V1)) -> isBag(V1)
mult(z, X) -> U11(isBin(X))
mult(0(X), Y) -> U21(and(isBin(X), isBin(Y)), X, Y)
mult(1(X), Y) -> U31(and(isBin(X), isBin(Y)), X, Y)
plus(z, X) -> U41(isBin(X), X)
plus(0(X), 0(Y)) -> U51(and(isBin(X), isBin(Y)), X, Y)
plus(0(X), 1(Y)) -> U61(and(isBin(X), isBin(Y)), X, Y)
plus(1(X), 1(Y)) -> U71(and(isBin(X), isBin(Y)), X, Y)
prod(empty) -> 1(z)
prod(singl(X)) -> U81(isBin(X), X)
prod(union(A, B)) -> U91(and(isBag(A), isBag(B)), A, B)
sum(empty) -> 0(z)
sum(singl(X)) -> U101(isBin(X), X)
sum(union(A, B)) -> U111(and(isBag(A), isBag(B)), A, B)

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polo

       →DP Problem 4

         ↳Polo

       →DP Problem 5

         ↳Polynomial Ordering

Dependency Pairs:

U91'(tt, A, B) -> PROD(B)
PROD(union(A, B)) -> U91'(and(isBag(A), isBag(B)), A, B)
U91'(tt, A, B) -> PROD(A)

Rules:

union(X, empty) -> X
union(empty, X) -> X
0(z) -> z
U101(tt, X) -> X
U11(tt) -> z
U111(tt, A, B) -> plus(sum(A), sum(B))
U21(tt, X, Y) -> 0(mult(X, Y))
U31(tt, X, Y) -> plus(0(mult(X, Y)), Y)
U41(tt, X) -> X
U51(tt, X, Y) -> 0(plus(X, Y))
U61(tt, X, Y) -> 1(plus(X, Y))
U71(tt, X, Y) -> 0(plus(plus(X, Y), 1(z)))
U81(tt, X) -> X
U91(tt, A, B) -> mult(prod(A), prod(B))
and(tt, X) -> X
isBag(empty) -> tt
isBag(singl(V1)) -> isBin(V1)
isBag(union(V1, V2)) -> and(isBag(V1), isBag(V2))
isBin(z) -> tt
isBin(0(V1)) -> isBin(V1)
isBin(1(V1)) -> isBin(V1)
isBin(mult(V1, V2)) -> and(isBin(V1), isBin(V2))
isBin(plus(V1, V2)) -> and(isBin(V1), isBin(V2))
isBin(prod(V1)) -> isBag(V1)
isBin(sum(V1)) -> isBag(V1)
mult(z, X) -> U11(isBin(X))
mult(0(X), Y) -> U21(and(isBin(X), isBin(Y)), X, Y)
mult(1(X), Y) -> U31(and(isBin(X), isBin(Y)), X, Y)
plus(z, X) -> U41(isBin(X), X)
plus(0(X), 0(Y)) -> U51(and(isBin(X), isBin(Y)), X, Y)
plus(0(X), 1(Y)) -> U61(and(isBin(X), isBin(Y)), X, Y)
plus(1(X), 1(Y)) -> U71(and(isBin(X), isBin(Y)), X, Y)
prod(empty) -> 1(z)
prod(singl(X)) -> U81(isBin(X), X)
prod(union(A, B)) -> U91(and(isBag(A), isBag(B)), A, B)
sum(empty) -> 0(z)
sum(singl(X)) -> U101(isBin(X), X)
sum(union(A, B)) -> U111(and(isBag(A), isBag(B)), A, B)

The following dependency pair can be strictly oriented:

PROD(union(A, B)) -> U91'(and(isBag(A), isBag(B)), A, B)

Additionally, the following usable rules using the Ce-refinement can be oriented:

and(tt, X) -> X
isBag(empty) -> tt
isBag(singl(V1)) -> isBin(V1)
isBag(union(V1, V2)) -> and(isBag(V1), isBag(V2))
isBin(z) -> tt
isBin(0(V1)) -> isBin(V1)
isBin(1(V1)) -> isBin(V1)
isBin(mult(V1, V2)) -> and(isBin(V1), isBin(V2))
isBin(plus(V1, V2)) -> and(isBin(V1), isBin(V2))
isBin(prod(V1)) -> isBag(V1)
isBin(sum(V1)) -> isBag(V1)

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(mult(x₁, x₂)) = 0

POL(and(x₁, x₂)) = x₂

POL(plus(x₁, x₂)) = 0

POL(prod(x₁)) = 0

POL(z) = 0

POL(isBag(x₁)) = 0

POL(sum(x₁)) = 0

POL(PROD(x₁)) = x₁

POL(U91'(x₁, x₂, x₃)) = x₂ + x₃

POL(isBin(x₁)) = 0

POL(0(x₁)) = 0

POL(union(x₁, x₂)) = 1 + x₁ + x₂

POL(1(x₁)) = 0

POL(tt) = 0

POL(empty) = 0

POL(singl(x₁)) = 0

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Polo

       →DP Problem 2

         ↳Polo

       →DP Problem 3

         ↳Polo

       →DP Problem 4

         ↳Polo

       →DP Problem 5

         ↳Polo

           →DP Problem 10

             ↳Dependency Graph

Dependency Pairs:

U91'(tt, A, B) -> PROD(B)
U91'(tt, A, B) -> PROD(A)

Rules:

union(X, empty) -> X
union(empty, X) -> X
0(z) -> z
U101(tt, X) -> X
U11(tt) -> z
U111(tt, A, B) -> plus(sum(A), sum(B))
U21(tt, X, Y) -> 0(mult(X, Y))
U31(tt, X, Y) -> plus(0(mult(X, Y)), Y)
U41(tt, X) -> X
U51(tt, X, Y) -> 0(plus(X, Y))
U61(tt, X, Y) -> 1(plus(X, Y))
U71(tt, X, Y) -> 0(plus(plus(X, Y), 1(z)))
U81(tt, X) -> X
U91(tt, A, B) -> mult(prod(A), prod(B))
and(tt, X) -> X
isBag(empty) -> tt
isBag(singl(V1)) -> isBin(V1)
isBag(union(V1, V2)) -> and(isBag(V1), isBag(V2))
isBin(z) -> tt
isBin(0(V1)) -> isBin(V1)
isBin(1(V1)) -> isBin(V1)
isBin(mult(V1, V2)) -> and(isBin(V1), isBin(V2))
isBin(plus(V1, V2)) -> and(isBin(V1), isBin(V2))
isBin(prod(V1)) -> isBag(V1)
isBin(sum(V1)) -> isBag(V1)
mult(z, X) -> U11(isBin(X))
mult(0(X), Y) -> U21(and(isBin(X), isBin(Y)), X, Y)
mult(1(X), Y) -> U31(and(isBin(X), isBin(Y)), X, Y)
plus(z, X) -> U41(isBin(X), X)
plus(0(X), 0(Y)) -> U51(and(isBin(X), isBin(Y)), X, Y)
plus(0(X), 1(Y)) -> U61(and(isBin(X), isBin(Y)), X, Y)
plus(1(X), 1(Y)) -> U71(and(isBin(X), isBin(Y)), X, Y)
prod(empty) -> 1(z)
prod(singl(X)) -> U81(isBin(X), X)
prod(union(A, B)) -> U91(and(isBag(A), isBag(B)), A, B)
sum(empty) -> 0(z)
sum(singl(X)) -> U101(isBin(X), X)
sum(union(A, B)) -> U111(and(isBag(A), isBag(B)), A, B)

Using the Dependency Graph resulted in no new DP problems.

Termination of R successfully shown.
Duration:
0:31 minutes

POL(mult(x₁, x₂))	= x₁ + x₂
POL(plus(x₁, x₂))	= 1 + x₁ + x₂
POL(0(x₁))	= x₁
POL(prod(x₁))	= x₁
POL(ISBAG(x₁))	= x₁
POL(union(x₁, x₂))	= x₁ + x₂
POL(1(x₁))	= x₁
POL(ISBIN(x₁))	= x₁
POL(sum(x₁))	= x₁
POL(singl(x₁))	= x₁

POL(0(x₁))	= 1 + x₁
POL(prod(x₁))	= x₁
POL(ISBAG(x₁))	= x₁
POL(union(x₁, x₂))	= x₁ + x₂
POL(ISBIN(x₁))	= x₁
POL(sum(x₁))	= x₁
POL(singl(x₁))	= x₁

POL(mult(x₁, x₂))	= 0
POL(U71(x₁, x₂, x₃))	= 1 + x₂ + x₃
POL(and(x₁, x₂))	= x₂
POL(plus(x₁, x₂))	= x₁ + x₂
POL(prod(x₁))	= 0
POL(z)	= 0
POL(isBag(x₁))	= 0
POL(U51'(x₁, x₂, x₃))	= x₂ + x₃
POL(sum(x₁))	= 0
POL(isBin(x₁))	= 0
POL(U51(x₁, x₂, x₃))	= x₂ + x₃
POL(U41(x₁, x₂))	= x₂
POL(0(x₁))	= x₁
POL(1(x₁))	= 1 + x₁
POL(union(x₁, x₂))	= 0
POL(U71'(x₁, x₂, x₃))	= 1 + x₂ + x₃
POL(tt)	= 0
POL(U61(x₁, x₂, x₃))	= 1 + x₂ + x₃
POL(U61'(x₁, x₂, x₃))	= x₂ + x₃
POL(empty)	= 0
POL(singl(x₁))	= 0

POL(U71(x₁, x₂, x₃))	= 1 + x₁ + x₂ + x₃
POL(mult(x₁, x₂))	= 0
POL(and(x₁, x₂))	= x₂
POL(plus(x₁, x₂))	= x₁ + x₂
POL(prod(x₁))	= 0
POL(z)	= 1
POL(isBag(x₁))	= 1
POL(U51'(x₁, x₂, x₃))	= x₂ + x₃
POL(sum(x₁))	= 0
POL(isBin(x₁))	= 1
POL(U51(x₁, x₂, x₃))	= x₂ + x₃
POL(0(x₁))	= x₁
POL(U41(x₁, x₂))	= x₂
POL(1(x₁))	= 1 + x₁
POL(union(x₁, x₂))	= x₁·x₂
POL(tt)	= 1
POL(U61(x₁, x₂, x₃))	= 1 + x₂ + x₃
POL(empty)	= 0
POL(singl(x₁))	= 0

POL(U71(x₁, x₂, x₃))	= 2 + x₂ + x₃
POL(mult(x₁, x₂))	= 1 + 2·x₁ + 2·x₁·x₂ + 2·x₂
POL(and(x₁, x₂))	= x₂
POL(plus(x₁, x₂))	= x₁ + x₂
POL(prod(x₁))	= 0
POL(U31(x₁, x₂, x₃))	= 2 + 2·x₁·x₃ + 2·x₂ + 2·x₂·x₃
POL(z)	= 0
POL(isBag(x₁))	= 2
POL(sum(x₁))	= 0
POL(U31'(x₁, x₂, x₃))	= 2 + 2·x₂ + 2·x₂·x₃ + 2·x₃
POL(U11(x₁))	= 0
POL(U51(x₁, x₂, x₃))	= 1 + x₂ + x₃
POL(isBin(x₁))	= 2
POL(0(x₁))	= 1 + x₁
POL(U41(x₁, x₂))	= x₂
POL(U21(x₁, x₂, x₃))	= 2 + 2·x₂ + 2·x₂·x₃ + 2·x₃
POL(1(x₁))	= 1 + x₁
POL(union(x₁, x₂))	= 0
POL(tt)	= 2
POL(U21'(x₁, x₂, x₃))	= 2 + 2·x₂ + 2·x₂·x₃ + 2·x₃
POL(U61(x₁, x₂, x₃))	= 1 + x₂ + x₃
POL(empty)	= 0
POL(singl(x₁))	= 0