Certification Problem

Input (TPDB TRS_Equational/Mixed_AC/bag-sum-prod-distr)

The rewrite relation of the following equational TRS is considered.

0(#) # (1)
+(#,x) x (2)
+(0(x),0(y)) 0(+(x,y)) (3)
+(0(x),1(y)) 1(+(x,y)) (4)
+(1(x),1(y)) 0(+(1(#),+(x,y))) (5)
*(#,x) # (6)
*(0(x),y) 0(*(x,y)) (7)
*(1(x),y) +(0(*(x,y)),y) (8)
*(+(y,z),x) +(*(x,y),*(x,z)) (9)
U(empty,b) b (10)
sum(empty) 0(#) (11)
sum(singl(x)) x (12)
sum(U(x,y)) +(sum(x),sum(y)) (13)
prod(empty) 1(#) (14)
prod(singl(x)) x (15)
prod(U(x,y)) *(prod(x),prod(y)) (16)

Associative symbols: *, +, U

Commutative symbols: *, +, U

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
[*(x1, x2)] = 2 + 2 · x2 + 2 · x1 + 1 · x1 · x2
[+(x1, x2)] = 2 + 1 · x2 + 1 · x1
[U(x1, x2)] = 2 + 2 · x2 + 2 · x1 + 1 · x1 · x2
[0(x1)] = 1 · x1
[#] = 1
[1(x1)] = 3 + 1 · x1
[empty] = 3
[sum(x1)] = 2 · x1 · x1
[singl(x1)] = 2 + 1 · x1 + 3 · x1 · x1
[prod(x1)] = 1 · x1 · x1
the rules
+(#,x) x (2)
*(#,x) # (6)
*(1(x),y) +(0(*(x,y)),y) (8)
U(empty,b) b (10)
sum(empty) 0(#) (11)
sum(singl(x)) x (12)
sum(U(x,y)) +(sum(x),sum(y)) (13)
prod(empty) 1(#) (14)
prod(singl(x)) x (15)
prod(U(x,y)) *(prod(x),prod(y)) (16)
can be deleted.

1.1 AC Rule Removal

Using the non-linear polynomial interpretation over the naturals
[*(x1, x2)] = 2 + 3 · x2 + 3 · x1 + 3 · x1 · x2
[+(x1, x2)] = 2 + 1 · x2 + 1 · x1
[U(x1, x2)] = 2 + 3 · x2 + 3 · x1 + 3 · x1 · x2
[0(x1)] = 1 · x1
[#] = 0
[1(x1)] = 2 + 1 · x1
the rule
*(+(y,z),x) +(*(x,y),*(x,z)) (9)
can be deleted.

1.1.1 AC Rule Removal

Using the non-linear polynomial interpretation over the naturals
[*(x1, x2)] = 1 · x2 + 1 · x1
[+(x1, x2)] = 1 + 2 · x2 + 2 · x1 + 2 · x1 · x2
[U(x1, x2)] = 2 + 3 · x2 + 3 · x1 + 3 · x1 · x2
[0(x1)] = 1 · x1
[#] = 0
[1(x1)] = 3 + 3 · x1
the rules
+(0(x),1(y)) 1(+(x,y)) (4)
+(1(x),1(y)) 0(+(1(#),+(x,y))) (5)
can be deleted.

1.1.1.1 AC Rule Removal

Using the non-linear polynomial interpretation over the naturals
[*(x1, x2)] = 1 + 2 · x2 + 2 · x1 + 2 · x1 · x2
[+(x1, x2)] = 3 + 3 · x2 + 3 · x1 + 2 · x1 · x2
[U(x1, x2)] = 2 + 3 · x2 + 3 · x1 + 3 · x1 · x2
[0(x1)] = 2 + 2 · x1
[#] = 3
the rules
0(#) # (1)
+(0(x),0(y)) 0(+(x,y)) (3)
*(0(x),y) 0(*(x,y)) (7)
can be deleted.

1.1.1.1.1 R is empty

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