Certification Problem

Input (TPDB TRS_Equational/Mixed_AC/BAG_nokinds)

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

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 AC Dependency Pair Transformation

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 TRS

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)

give rise to even more dependency pairs (by sharping the root symbols of each rule). Finiteness for all DPs in combination with the equational DPs is proven as follows.

1.1 Dependency Graph Processor

The dependency pairs are split into 6 components.

The 1^st component contains the pair

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)

1.1.1 AC Monotonic Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the naturals

[isBin(x₁)]	=	2 · x₁
[plus(x₁, x₂)]	=	2 + 3 · x₁ + 2 · x₂
[and(x₁, x₂)]	=	2 · x₁ + 1 · x₂
[isBag(x₁)]	=	2 + 2 · x₁
[singl(x₁)]	=	3 + 3 · x₁
[0(x₁)]	=	3 · x₁
[prod(x₁)]	=	1 + 3 · x₁
[sum(x₁)]	=	2 + 3 · x₁
[empty]	=	0
[tt]	=	0
[union(x₁, x₂)]	=	3 + 3 · x₁ + 3 · x₂
[mult(x₁, x₂)]	=	3 + 3 · x₁ + 2 · x₂
[1(x₁)]	=	3 · x₁
[z]	=	0
[sum^#(x₁)]	=	2 · x₁
[U111^#(x₁, x₂, x₃)]	=	1 · x₁ + 2 · x₂ + 2 · x₃

together with the usable rules

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)

(w.r.t. the implicit argument filter of the reduction pair), the pair

sum^#(union(A,B))

→

U111^#(and(isBag(A),isBag(B)),A,B)

(118)

and the rules

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)

could be deleted.

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 2^nd component contains the pair

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)

1.1.2 AC Monotonic Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the naturals

[isBin(x₁)]	=	2 · x₁
[plus(x₁, x₂)]	=	2 + 3 · x₁ + 2 · x₂
[and(x₁, x₂)]	=	2 + 2 · x₁ + 1 · x₂
[isBag(x₁)]	=	1 · x₁
[singl(x₁)]	=	3 · x₁
[0(x₁)]	=	3 · x₁
[prod(x₁)]	=	3 · x₁
[sum(x₁)]	=	3 · x₁
[empty]	=	2
[tt]	=	2
[union(x₁, x₂)]	=	3 + 3 · x₁ + 3 · x₂
[mult(x₁, x₂)]	=	2 + 3 · x₁ + 2 · x₂
[1(x₁)]	=	1 · x₁
[z]	=	2
[U91^#(x₁, x₂, x₃)]	=	2 · x₁ + 2 · x₂ + 2 · x₃
[prod^#(x₁)]	=	2 + 2 · x₁

together with the usable rules

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)

(w.r.t. the implicit argument filter of the reduction pair), the pairs

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)

and the rules

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)

could be deleted.

1.1.2.1 AC Dependency Pair Problem is trivial

There are no strict pairs and rules remaining, or there are no DPs remaining. Therefore, finiteness is trivially satisfied.

The 3^rd component contains the pair

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)

1.1.3 AC Reduction Pair Processor with Usable Rules

Using the non-linear polynomial interpretation over the naturals

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

together with the usable rules

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)

(w.r.t. the implicit argument filter of the reduction pair), the pairs

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)

could be deleted.

1.1.3.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

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)

1.1.3.1.1 AC Reduction Pair Processor with Usable Rules

Using the non-linear polynomial interpretation over the naturals

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

together with the usable rules

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)

(w.r.t. the implicit argument filter of the reduction pair), the pair

mult^#(mult(1(X),Y),ext)

→

mult^#(U31(and(isBin(X),isBin(Y)),X,Y),ext)

(130)

could be deleted.

1.1.3.1.1.1 AC Reduction Pair Processor with Usable Rules

Using the non-linear polynomial interpretation over the naturals

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

together with the usable rules

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)

(w.r.t. the implicit argument filter of the reduction pair), the pairs

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)

could be deleted.

1.1.3.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

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)

1.1.3.1.1.1.1.1 AC Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the naturals

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

together with the usable rules

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)

(w.r.t. the implicit argument filter of the reduction pair), the pairs

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)

could be deleted.

1.1.3.1.1.1.1.1.1 AC Dependency Pair Problem is trivial

There are no strict pairs and rules remaining, or there are no DPs remaining. Therefore, finiteness is trivially satisfied.

The 4^th component contains the pair

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)

1.1.4 AC Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the naturals

[plus^#(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[plus(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[1(x₁)]	=	1 + 2 · x₁
[U71^#(x₁, x₂, x₃)]	=	3 + 2 · x₂ + 2 · x₃
[and(x₁, x₂)]	=	0
[isBin(x₁)]	=	0
[0(x₁)]	=	2 · x₁
[U61(x₁, x₂, x₃)]	=	1 + 2 · x₂ + 2 · x₃
[U61^#(x₁, x₂, x₃)]	=	1 + 2 · x₂ + 2 · x₃
[tt]	=	0
[z]	=	0
[U41(x₁, x₂)]	=	1 · x₂
[U71(x₁, x₂, x₃)]	=	2 + 2 · x₂ + 2 · x₃
[U51(x₁, x₂, x₃)]	=	2 · x₂ + 2 · x₃
[U51^#(x₁, x₂, x₃)]	=	2 · x₂ + 2 · x₃
[sum(x₁)]	=	0
[isBag(x₁)]	=	0
[prod(x₁)]	=	3 · x₁
[mult(x₁, x₂)]	=	0
[singl(x₁)]	=	0
[empty]	=	0
[union(x₁, x₂)]	=	0

together with the usable rules

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)

(w.r.t. the implicit argument filter of the reduction pair), the pairs

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)

could be deleted.

1.1.4.1 AC Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the naturals

[plus^#(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[plus(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[0(x₁)]	=	1 · x₁
[1(x₁)]	=	2 + 1 · x₁
[U61(x₁, x₂, x₃)]	=	2 + 1 · x₂ + 1 · x₃
[and(x₁, x₂)]	=	0
[isBin(x₁)]	=	0
[z]	=	0
[U41(x₁, x₂)]	=	1 · x₂
[U71(x₁, x₂, x₃)]	=	3 + 1 · x₂ + 1 · x₃
[U51(x₁, x₂, x₃)]	=	1 · x₂ + 1 · x₃
[U51^#(x₁, x₂, x₃)]	=	2 · x₂ + 2 · x₃
[tt]	=	0
[sum(x₁)]	=	0
[isBag(x₁)]	=	0
[prod(x₁)]	=	3 · x₁
[mult(x₁, x₂)]	=	0
[singl(x₁)]	=	0
[empty]	=	0
[union(x₁, x₂)]	=	0

together with the usable rules

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)

(w.r.t. the implicit argument filter of the reduction pair), the pair

plus^#(plus(1(X),1(Y)),ext)

→

plus^#(U71(and(isBin(X),isBin(Y)),X,Y),ext)

(148)

could be deleted.

1.1.4.1.1 AC Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the naturals

[plus^#(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[plus(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[0(x₁)]	=	1 · x₁
[1(x₁)]	=	2 + 1 · x₁
[U61(x₁, x₂, x₃)]	=	2 + 1 · x₂ + 1 · x₃
[and(x₁, x₂)]	=	0
[isBin(x₁)]	=	0
[z]	=	1
[U41(x₁, x₂)]	=	1 · x₂
[U51(x₁, x₂, x₃)]	=	1 · x₂ + 1 · x₃
[U51^#(x₁, x₂, x₃)]	=	2 · x₂ + 2 · x₃
[tt]	=	0
[U71(x₁, x₂, x₃)]	=	3 + 1 · x₂ + 1 · x₃
[isBag(x₁)]	=	0
[singl(x₁)]	=	0
[empty]	=	0
[union(x₁, x₂)]	=	0
[sum(x₁)]	=	3 · x₁
[prod(x₁)]	=	0
[mult(x₁, x₂)]	=	0

together with the usable rules

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)

(w.r.t. the implicit argument filter of the reduction pair), the pair

plus^#(plus(z,X),ext)

→

plus^#(U41(isBin(X),X),ext)

(135)

could be deleted.

1.1.4.1.1.1 AC Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the naturals

[plus^#(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[plus(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[0(x₁)]	=	1 · x₁
[1(x₁)]	=	1 + 1 · x₁
[U61(x₁, x₂, x₃)]	=	2 + 1 · x₂ + 1 · x₃
[and(x₁, x₂)]	=	0
[isBin(x₁)]	=	0
[U51(x₁, x₂, x₃)]	=	1 + 1 · x₂ + 1 · x₃
[U51^#(x₁, x₂, x₃)]	=	2 · x₂ + 2 · x₃
[tt]	=	0
[sum(x₁)]	=	3 · x₁
[isBag(x₁)]	=	0
[prod(x₁)]	=	0
[mult(x₁, x₂)]	=	0
[z]	=	0
[U41(x₁, x₂)]	=	1 + 1 · x₂
[U71(x₁, x₂, x₃)]	=	3 + 1 · x₂ + 1 · x₃
[singl(x₁)]	=	0
[empty]	=	0
[union(x₁, x₂)]	=	0

together with the usable rules

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)

(w.r.t. the implicit argument filter of the reduction pair), the pairs

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)

could be deleted.

1.1.4.1.1.1.1 AC Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the naturals

[plus^#(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[plus(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[0(x₁)]	=	1 + 1 · x₁
[1(x₁)]	=	1 + 1 · x₁
[U61(x₁, x₂, x₃)]	=	1 + 1 · x₂ + 1 · x₃
[and(x₁, x₂)]	=	0
[isBin(x₁)]	=	0
[U51(x₁, x₂, x₃)]	=	1 + 1 · x₂ + 1 · x₃
[U51^#(x₁, x₂, x₃)]	=	2 · x₂ + 2 · x₃
[tt]	=	0
[U41(x₁, x₂)]	=	1 · x₂
[z]	=	0
[isBag(x₁)]	=	0
[singl(x₁)]	=	0
[empty]	=	0
[union(x₁, x₂)]	=	0
[sum(x₁)]	=	3 · x₁
[prod(x₁)]	=	0
[mult(x₁, x₂)]	=	0
[U71(x₁, x₂, x₃)]	=	2 + 1 · x₂ + 1 · x₃

together with the usable rules

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)

(w.r.t. the implicit argument filter of the reduction pair), the pairs

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)

could be deleted.

1.1.4.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

plus^#(x,y) → plus^#(y,x) (46)

plus^#(plus(x,y),z') → plus^#(x,plus(y,z')) (49)

1.1.4.1.1.1.1.1.1 AC Dependency Pair Problem is trivial
There are no strict pairs and rules remaining, or there are no DPs remaining. Therefore, finiteness is trivially satisfied.

The 5^th component contains the pair

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)

1.1.5 AC Monotonic Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the naturals

[isBin^#(x₁)]	=	1 · x₁
[1(x₁)]	=	3 · x₁
[plus(x₁, x₂)]	=	3 · x₁ + 3 · x₂
[0(x₁)]	=	3 · x₁
[sum(x₁)]	=	3 · x₁
[isBag^#(x₁)]	=	2 · x₁
[union(x₁, x₂)]	=	3 · x₁ + 3 · x₂
[mult(x₁, x₂)]	=	3 · x₁ + 3 · x₂
[prod(x₁)]	=	3 · x₁
[singl(x₁)]	=	3 · x₁

having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the pairs

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)

and the rules

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)

could be deleted.

1.1.5.1 AC Dependency Pair Problem is trivial

There are no strict pairs and rules remaining, or there are no DPs remaining. Therefore, finiteness is trivially satisfied.

The 6^th component contains the pair

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)

1.1.6 AC Monotonic Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the naturals

[union^#(x₁, x₂)]	=	3 · x₁ + 3 · x₂
[union(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[empty]	=	0

together with the usable rules

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)

(w.r.t. the implicit argument filter of the reduction pair), the pairs

union^#(union(empty,X),ext)	→	union^#(X,ext)	(154)
union^#(union(X,empty),ext)	→	union^#(X,ext)	(153)

and the rules

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)

could be deleted.

1.1.6.1 AC Monotonic Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the naturals

[union^#(x₁, x₂)]	=	3 · x₁ + 3 · x₂
[union(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[mult(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[plus(x₁, x₂)]	=	1 · x₁ + 1 · x₂

together with the usable rules

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)

(w.r.t. the implicit argument filter of the reduction pair), the pair

union^#(union(x,y),z')

→

union^#(y,z')

(53)

and no rules could be deleted.

1.1.6.1.1 AC Dependency Pair Problem is trivial

There are no strict pairs and rules remaining, or there are no DPs remaining. Therefore, finiteness is trivially satisfied.

Certification Problem

Input (TPDB TRS_Equational/Mixed_AC/BAG_nokinds)

Property / Task

Answer / Result

Proof (by AProVE @ termCOMP 2023)

1 AC Dependency Pair Transformation

1.1 Dependency Graph Processor

1.1.1 AC Monotonic Reduction Pair Processor with Usable Rules

1.1.1.1 Dependency Graph Processor

1.1.2 AC Monotonic Reduction Pair Processor with Usable Rules

1.1.2.1 AC Dependency Pair Problem is trivial

1.1.3 AC Reduction Pair Processor with Usable Rules

1.1.3.1 Dependency Graph Processor

1.1.3.1.1 AC Reduction Pair Processor with Usable Rules

1.1.3.1.1.1 AC Reduction Pair Processor with Usable Rules

1.1.3.1.1.1.1 Dependency Graph Processor

1.1.3.1.1.1.1.1 AC Reduction Pair Processor with Usable Rules

1.1.3.1.1.1.1.1.1 AC Dependency Pair Problem is trivial

1.1.4 AC Reduction Pair Processor with Usable Rules

1.1.4.1 AC Reduction Pair Processor with Usable Rules

1.1.4.1.1 AC Reduction Pair Processor with Usable Rules

1.1.4.1.1.1 AC Reduction Pair Processor with Usable Rules

1.1.4.1.1.1.1 AC Reduction Pair Processor with Usable Rules

1.1.4.1.1.1.1.1 Dependency Graph Processor

1.1.4.1.1.1.1.1.1 AC Dependency Pair Problem is trivial

1.1.5 AC Monotonic Reduction Pair Processor with Usable Rules

1.1.5.1 AC Dependency Pair Problem is trivial

1.1.6 AC Monotonic Reduction Pair Processor with Usable Rules

1.1.6.1 AC Monotonic Reduction Pair Processor with Usable Rules

1.1.6.1.1 AC Dependency Pair Problem is trivial