Certification Problem

Input (TPDB TRS_Equational/Mixed_AC/BAG_nosorts-noand)

The rewrite relation of the following equational TRS is considered.

union(X,empty) → X (1)
union(empty,X) → X (2)
0(z) → z (3)
U11(tt,X,Y) → U12(tt,X,Y) (4)
U12(tt,X,Y) → 0(mult(X,Y)) (5)
U21(tt,X,Y) → U22(tt,X,Y) (6)
U22(tt,X,Y) → plus(0(mult(X,Y)),Y) (7)
U31(tt,X,Y) → U32(tt,X,Y) (8)
U32(tt,X,Y) → 0(plus(X,Y)) (9)
U41(tt,X,Y) → U42(tt,X,Y) (10)
U42(tt,X,Y) → 1(plus(X,Y)) (11)
U51(tt,X,Y) → U52(tt,X,Y) (12)
U52(tt,X,Y) → 0(plus(plus(X,Y),1(z))) (13)
U61(tt,A,B) → U62(tt,A,B) (14)
U62(tt,A,B) → mult(prod(A),prod(B)) (15)
U71(tt,A,B) → U72(tt,A,B) (16)
U72(tt,A,B) → plus(sum(A),sum(B)) (17)
mult(z,X) → z (18)
mult(0(X),Y) → U11(tt,X,Y) (19)
mult(1(X),Y) → U21(tt,X,Y) (20)
plus(z,X) → X (21)
plus(0(X),0(Y)) → U31(tt,X,Y) (22)
plus(0(X),1(Y)) → U41(tt,X,Y) (23)
plus(1(X),1(Y)) → U51(tt,X,Y) (24)
prod(empty) → 1(z) (25)
prod(singl(X)) → X (26)
prod(union(A,B)) → U61(tt,A,B) (27)
sum(empty) → 0(z) (28)
sum(singl(X)) → X (29)
sum(union(A,B)) → U71(tt,A,B) (30)

Associative symbols: mult, plus, union

Commutative symbols: mult, plus, union

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 AC Rule Removal

Using the non-linear polynomial interpretation over the naturals
[mult(x1, x2)] = 1 · x2 + 1 · x1 + 2 · x1 · x2
[plus(x1, x2)] = 1 · x2 + 1 · x1
[union(x1, x2)] = 1 · x2 + 1 · x1 + 2 · x1 · x2
[empty] = 2
[0(x1)] = 1 · x1
[z] = 0
[U11(x1, x2, x3)] = 1 · x3 + 1 · x2 + 2 · x1 + 2 · x2 · x3 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
[tt] = 0
[U12(x1, x2, x3)] = 1 · x3 + 1 · x2 + 2 · x1 + 2 · x2 · x3 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
[U21(x1, x2, x3)] = 1 + 3 · x3 + 1 · x2 + 2 · x1 + 2 · x2 · x3 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
[U22(x1, x2, x3)] = 1 + 2 · x3 + 1 · x2 + 2 · x1 + 2 · x2 · x3 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
[U31(x1, x2, x3)] = 1 · x3 + 1 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 3 · x1 · x2 · x3
[U32(x1, x2, x3)] = 1 · x3 + 1 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 3 · x1 · x2 · x3
[U41(x1, x2, x3)] = 1 + 1 · x3 + 1 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 3 · x1 · x2 · x3
[U42(x1, x2, x3)] = 1 + 1 · x3 + 1 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 3 · x1 · x2 · x3
[1(x1)] = 1 + 1 · x1
[U51(x1, x2, x3)] = 2 + 1 · x3 + 1 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 3 · x1 · x2 · x3
[U52(x1, x2, x3)] = 1 + 1 · x3 + 1 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 3 · x1 · x2 · x3
[U61(x1, x2, x3)] = 1 · x3 + 1 · x2 + 2 · x1 + 2 · x2 · x3 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
[U62(x1, x2, x3)] = 1 · x3 + 1 · x2 + 2 · x1 + 2 · x2 · x3 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
[prod(x1)] = 1 · x1
[U71(x1, x2, x3)] = 2 · x3 + 2 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
[U72(x1, x2, x3)] = 2 · x3 + 2 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
[sum(x1)] = 2 · x1
[singl(x1)] = 3 · x1 + 3 · x1 · x1
the rules
union(X,empty) → X (1)
union(empty,X) → X (2)
U22(tt,X,Y) → plus(0(mult(X,Y)),Y) (7)
U51(tt,X,Y) → U52(tt,X,Y) (12)
prod(empty) → 1(z) (25)
sum(empty) → 0(z) (28)
can be deleted.

1.1 AC Rule Removal

Using the non-linear polynomial interpretation over the naturals
[mult(x1, x2)] = 1 · x2 + 1 · x1
[plus(x1, x2)] = 1 · x2 + 1 · x1
[union(x1, x2)] = 1 + 2 · x2 + 2 · x1 + 2 · x1 · x2
[0(x1)] = 1 · x1
[z] = 0
[U11(x1, x2, x3)] = 1 · x3 + 1 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
[tt] = 0
[U12(x1, x2, x3)] = 1 · x3 + 1 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
[U21(x1, x2, x3)] = 1 · x3 + 1 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
[U22(x1, x2, x3)] = 1 · x3 + 1 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
[U31(x1, x2, x3)] = 1 · x3 + 1 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
[U32(x1, x2, x3)] = 1 · x3 + 1 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
[U41(x1, x2, x3)] = 1 · x3 + 1 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
[U42(x1, x2, x3)] = 1 · x3 + 1 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
[1(x1)] = 1 · x1
[U52(x1, x2, x3)] = 1 · x3 + 2 · x2 + 2 · x1 + 2 · x2 · x3 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
[U61(x1, x2, x3)] = 2 · x3 + 3 · x2 + 2 · x1 + 1 · x2 · x3 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
[U62(x1, x2, x3)] = 2 · x3 + 2 · x2 + 2 · x1 + 1 · x2 · x3 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
[prod(x1)] = 2 · x1
[U71(x1, x2, x3)] = 2 + 1 · x3 + 1 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
[U72(x1, x2, x3)] = 2 + 1 · x3 + 1 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
[sum(x1)] = 1 + 1 · x1
[U51(x1, x2, x3)] = 1 · x3 + 1 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
[singl(x1)] = 3 · x1 + 3 · x1 · x1
the rules
prod(union(A,B)) → U61(tt,A,B) (27)
sum(singl(X)) → X (29)
can be deleted.

1.1.1 AC Rule Removal

Using the non-linear polynomial interpretation over the naturals
[mult(x1, x2)] = 1 · x2 + 1 · x1 + 1 · x1 · x2
[plus(x1, x2)] = 1 · x2 + 1 · x1
[union(x1, x2)] = 1 · x2 + 1 · x1 + 1 · x1 · x2
[0(x1)] = 2 + 2 · x1
[z] = 0
[U11(x1, x2, x3)] = 2 + 2 · x3 + 2 · x2 + 2 · x1 + 2 · x2 · x3 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
[tt] = 0
[U12(x1, x2, x3)] = 2 + 2 · x3 + 2 · x2 + 2 · x1 + 2 · x2 · x3 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
[U21(x1, x2, x3)] = 1 · x3 + 1 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
[U22(x1, x2, x3)] = 1 · x3 + 1 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
[U31(x1, x2, x3)] = 3 + 2 · x3 + 2 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
[U32(x1, x2, x3)] = 2 + 2 · x3 + 2 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
[U41(x1, x2, x3)] = 1 + 2 · x3 + 2 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
[U42(x1, x2, x3)] = 2 · x3 + 2 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
[1(x1)] = 2 · x1
[U52(x1, x2, x3)] = 2 + 2 · x3 + 2 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
[U61(x1, x2, x3)] = 1 + 1 · x3 + 1 · x2 + 2 · x1 + 1 · x2 · x3 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
[U62(x1, x2, x3)] = 1 · x3 + 1 · x2 + 2 · x1 + 1 · x2 · x3 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
[prod(x1)] = 1 · x1
[U71(x1, x2, x3)] = 2 · x3 + 2 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
[U72(x1, x2, x3)] = 2 · x3 + 2 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
[sum(x1)] = 2 · x1
[U51(x1, x2, x3)] = 1 · x3 + 1 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
[singl(x1)] = 3 + 3 · x1 + 3 · x1 · x1
the rules
0(z) → z (3)
U31(tt,X,Y) → U32(tt,X,Y) (8)
U41(tt,X,Y) → U42(tt,X,Y) (10)
U61(tt,A,B) → U62(tt,A,B) (14)
plus(0(X),0(Y)) → U31(tt,X,Y) (22)
plus(0(X),1(Y)) → U41(tt,X,Y) (23)
prod(singl(X)) → X (26)
can be deleted.

1.1.1.1 AC Rule Removal

Using the non-linear polynomial interpretation over the naturals
[mult(x1, x2)] = 2 + 2 · x2 + 2 · x1 + 1 · x1 · x2
[plus(x1, x2)] = 1 · x2 + 1 · x1
[union(x1, x2)] = 1 · x2 + 1 · x1 + 3 · x1 · x2
[U11(x1, x2, x3)] = 2 + 2 · x3 + 2 · x2 + 2 · x1 + 1 · x2 · x3 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
[tt] = 0
[U12(x1, x2, x3)] = 2 + 2 · x3 + 2 · x2 + 2 · x1 + 1 · x2 · x3 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
[0(x1)] = 1 · x1
[U21(x1, x2, x3)] = 2 + 1 · x3 + 1 · x2 + 2 · x1 + 2 · x2 · x3 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
[U22(x1, x2, x3)] = 1 · x3 + 1 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
[U32(x1, x2, x3)] = 1 + 2 · x3 + 2 · x2 + 2 · x1 + 2 · x2 · x3 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
[U42(x1, x2, x3)] = 1 + 2 · x3 + 2 · x2 + 2 · x1 + 3 · x2 · x3 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
[1(x1)] = 2 · x1
[U52(x1, x2, x3)] = 3 + 2 · x3 + 1 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
[z] = 0
[U62(x1, x2, x3)] = 2 + 2 · x3 + 3 · x2 + 2 · x1 + 2 · x2 · x3 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
[prod(x1)] = 1 · x1
[U71(x1, x2, x3)] = 3 · x3 + 3 · x2 + 2 · x1 + 2 · x2 · x3 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
[U72(x1, x2, x3)] = 3 · x3 + 3 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
[sum(x1)] = 3 · x1
[U51(x1, x2, x3)] = 1 · x3 + 1 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
the rules
U21(tt,X,Y) → U22(tt,X,Y) (6)
U32(tt,X,Y) → 0(plus(X,Y)) (9)
U42(tt,X,Y) → 1(plus(X,Y)) (11)
U52(tt,X,Y) → 0(plus(plus(X,Y),1(z))) (13)
mult(z,X) → z (18)
can be deleted.

1.1.1.1.1 AC Rule Removal

Using the non-linear polynomial interpretation over the naturals
[mult(x1, x2)] = 1 + 2 · x2 + 2 · x1 + 2 · x1 · x2
[plus(x1, x2)] = 1 · x2 + 1 · x1
[union(x1, x2)] = 1 · x2 + 1 · x1 + 2 · x1 · x2
[U11(x1, x2, x3)] = 2 + 2 · x3 + 2 · x2 + 2 · x1 + 2 · x2 · x3 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
[tt] = 0
[U12(x1, x2, x3)] = 2 + 2 · x3 + 2 · x2 + 2 · x1 + 2 · x2 · x3 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
[0(x1)] = 1 + 1 · x1
[U62(x1, x2, x3)] = 1 + 2 · x3 + 2 · x2 + 2 · x1 + 3 · x2 · x3 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
[prod(x1)] = 1 · x1
[U71(x1, x2, x3)] = 1 · x3 + 1 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
[U72(x1, x2, x3)] = 1 · x3 + 1 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
[sum(x1)] = 1 · x1
[1(x1)] = 3 + 2 · x1 + 3 · x1 · x1
[U21(x1, x2, x3)] = 2 · x3 + 1 · x2 + 2 · x1 + 2 · x2 · x3 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
[z] = 1
[U51(x1, x2, x3)] = 1 · x3 + 1 · x2 + 2 · x1 + 2 · x1 · x3 + 2 · x1 · x2 + 2 · x1 · x2 · x3
the rules
mult(0(X),Y) → U11(tt,X,Y) (19)
mult(1(X),Y) → U21(tt,X,Y) (20)
plus(z,X) → X (21)
plus(1(X),1(Y)) → U51(tt,X,Y) (24)
can be deleted.

1.1.1.1.1.1 AC Rule Removal

Using the non-linear polynomial interpretation over the naturals
[mult(x1, x2)] = 1 · x2 + 1 · x1
[plus(x1, x2)] = 1 · x2 + 1 · x1
[union(x1, x2)] = 3 + 3 · x2 + 3 · x1 + 2 · x1 · x2
[U11(x1, x2, x3)] = 3 + 1 · x3 + 2 · x2 + 1 · x1 + 2 · x1 · x3 + 1 · x1 · x2 + 2 · x1 · x2 · x3
[tt] = 2
[U12(x1, x2, x3)] = 2 · x3 + 1 · x2 + 2 · x1 + 2 · x2 · x3
[0(x1)] = 1 + 1 · x1
[U62(x1, x2, x3)] = 1 · x3 + 1 · x2 + 1 · x1 + 1 · x2 · x3 + 2 · x1 · x3
[prod(x1)] = 1 · x1
[U71(x1, x2, x3)] = 2 + 2 · x3 + 2 · x2 + 3 · x1 + 3 · x1 · x3 + 3 · x1 · x2 + 2 · x1 · x2 · x3
[U72(x1, x2, x3)] = 3 + 3 · x3 + 1 · x2 + 2 · x1 + 2 · x2 · x3 + 2 · x1 · x2
[sum(x1)] = 3 · x1
the rules
U11(tt,X,Y) → U12(tt,X,Y) (4)
U12(tt,X,Y) → 0(mult(X,Y)) (5)
U62(tt,A,B) → mult(prod(A),prod(B)) (15)
U71(tt,A,B) → U72(tt,A,B) (16)
U72(tt,A,B) → plus(sum(A),sum(B)) (17)
sum(union(A,B)) → U71(tt,A,B) (30)
can be deleted.

1.1.1.1.1.1.1 R is empty

There are no rules in the TRS. Hence, it is AC-terminating.