Certification Problem

Input (TPDB TRS_Equational/Mixed_AC/BAG_complete)

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,Y)	→	0(mult(X,Y))	(4)
U11(tt,V1)	→	U12(isBin(V1))	(5)
U111(tt,X,Y)	→	plus(0(mult(X,Y)),Y)	(6)
U12(tt)	→	tt	(7)
U121(tt,X)	→	X	(8)
U131(tt,X,Y)	→	0(plus(X,Y))	(9)
U141(tt,X,Y)	→	1(plus(X,Y))	(10)
U151(tt,X,Y)	→	0(plus(plus(X,Y),1(z)))	(11)
U161(tt,X)	→	X	(12)
U171(tt,A,B)	→	mult(prod(A),prod(B))	(13)
U181(tt,X)	→	X	(14)
U191(tt,A,B)	→	plus(sum(A),sum(B))	(15)
U21(tt,V1,V2)	→	U22(isBag(V1),V2)	(16)
U22(tt,V2)	→	U23(isBag(V2))	(17)
U23(tt)	→	tt	(18)
U31(tt,V1)	→	U32(isBin(V1))	(19)
U32(tt)	→	tt	(20)
U41(tt,V1)	→	U42(isBin(V1))	(21)
U42(tt)	→	tt	(22)
U51(tt,V1,V2)	→	U52(isBin(V1),V2)	(23)
U52(tt,V2)	→	U53(isBin(V2))	(24)
U53(tt)	→	tt	(25)
U61(tt,V1,V2)	→	U62(isBin(V1),V2)	(26)
U62(tt,V2)	→	U63(isBin(V2))	(27)
U63(tt)	→	tt	(28)
U71(tt,V1)	→	U72(isBag(V1))	(29)
U72(tt)	→	tt	(30)
U81(tt,V1)	→	U82(isBag(V1))	(31)
U82(tt)	→	tt	(32)
U91(tt)	→	z	(33)
and(tt,X)	→	X	(34)
isBag(empty)	→	tt	(35)
isBag(singl(V1))	→	U11(isBinKind(V1),V1)	(36)
isBag(union(V1,V2))	→	U21(and(isBagKind(V1),isBagKind(V2)),V1,V2)	(37)
isBagKind(empty)	→	tt	(38)
isBagKind(singl(V1))	→	isBinKind(V1)	(39)
isBagKind(union(V1,V2))	→	and(isBagKind(V1),isBagKind(V2))	(40)
isBin(z)	→	tt	(41)
isBin(0(V1))	→	U31(isBinKind(V1),V1)	(42)
isBin(1(V1))	→	U41(isBinKind(V1),V1)	(43)
isBin(mult(V1,V2))	→	U51(and(isBinKind(V1),isBinKind(V2)),V1,V2)	(44)
isBin(plus(V1,V2))	→	U61(and(isBinKind(V1),isBinKind(V2)),V1,V2)	(45)
isBin(prod(V1))	→	U71(isBagKind(V1),V1)	(46)
isBin(sum(V1))	→	U81(isBagKind(V1),V1)	(47)
isBinKind(z)	→	tt	(48)
isBinKind(0(V1))	→	isBinKind(V1)	(49)
isBinKind(1(V1))	→	isBinKind(V1)	(50)
isBinKind(mult(V1,V2))	→	and(isBinKind(V1),isBinKind(V2))	(51)
isBinKind(plus(V1,V2))	→	and(isBinKind(V1),isBinKind(V2))	(52)
isBinKind(prod(V1))	→	isBagKind(V1)	(53)
isBinKind(sum(V1))	→	isBagKind(V1)	(54)
mult(z,X)	→	U91(and(isBin(X),isBinKind(X)))	(55)
mult(0(X),Y)	→	U101(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)	(56)
mult(1(X),Y)	→	U111(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)	(57)
plus(z,X)	→	U121(and(isBin(X),isBinKind(X)),X)	(58)
plus(0(X),0(Y))	→	U131(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)	(59)
plus(0(X),1(Y))	→	U141(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)	(60)
plus(1(X),1(Y))	→	U151(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)	(61)
prod(empty)	→	1(z)	(62)
prod(singl(X))	→	U161(and(isBin(X),isBinKind(X)),X)	(63)
prod(union(A,B))	→	U171(and(and(isBag(A),isBagKind(A)),and(isBag(B),isBagKind(B))),A,B)	(64)
sum(empty)	→	0(z)	(65)
sum(singl(X))	→	U181(and(isBin(X),isBinKind(X)),X)	(66)
sum(union(A,B))	→	U191(and(and(isBag(A),isBagKind(A)),and(isBag(B),isBagKind(B))),A,B)	(67)

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 205 ruless (increase limit for explicit display).

The extended rules of the TRS

mult(mult(z,X),ext)	→	mult(U91(and(isBin(X),isBinKind(X))),ext)	(288)
mult(mult(0(X),Y),ext)	→	mult(U101(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y),ext)	(289)
mult(mult(1(X),Y),ext)	→	mult(U111(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y),ext)	(290)
plus(plus(z,X),ext)	→	plus(U121(and(isBin(X),isBinKind(X)),X),ext)	(291)
plus(plus(0(X),0(Y)),ext)	→	plus(U131(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y),ext)	(292)
plus(plus(0(X),1(Y)),ext)	→	plus(U141(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y),ext)	(293)
plus(plus(1(X),1(Y)),ext)	→	plus(U151(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y),ext)	(294)
union(union(X,empty),ext)	→	union(X,ext)	(295)
union(union(empty,X),ext)	→	union(X,ext)	(296)

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 7 components.

The 1^st component contains the pair

U171^#(tt,A,B)	→	prod^#(A)	(97)
prod^#(union(A,B))	→	U171^#(and(and(isBag(A),isBagKind(A)),and(isBag(B),isBagKind(B))),A,B)	(210)
U171^#(tt,A,B)	→	prod^#(B)	(98)

1.1.1 AC Monotonic Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the naturals

[U51(x₁, x₂, x₃)]	=	2 · x₁ + 1 · x₂ + 1 · x₃
[tt]	=	0
[U52(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[isBin(x₁)]	=	1 · x₁
[U42(x₁)]	=	1 · x₁
[isBag(x₁)]	=	1 · x₁
[empty]	=	0
[and(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[1(x₁)]	=	2 · x₁
[U41(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[isBinKind(x₁)]	=	1 · x₁
[U21(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 1 · x₃
[U22(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[singl(x₁)]	=	1 + 3 · x₁
[U11(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[U82(x₁)]	=	1 · x₁
[isBagKind(x₁)]	=	2 · x₁
[U12(x₁)]	=	2 · x₁
[U31(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[U32(x₁)]	=	1 · x₁
[U72(x₁)]	=	1 · x₁
[plus(x₁, x₂)]	=	3 + 3 · x₁ + 3 · x₂
[U61(x₁, x₂, x₃)]	=	3 + 1 · x₁ + 1 · x₂ + 2 · x₃
[sum(x₁)]	=	3 · x₁
[U53(x₁)]	=	1 · x₁
[U23(x₁)]	=	1 · x₁
[union(x₁, x₂)]	=	3 · x₁ + 3 · x₂
[U71(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[prod(x₁)]	=	1 + 3 · x₁
[z]	=	0
[U81(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[0(x₁)]	=	2 + 3 · x₁
[U62(x₁, x₂)]	=	2 + 1 · x₁ + 1 · x₂
[U63(x₁)]	=	1 · x₁
[mult(x₁, x₂)]	=	3 · x₁ + 3 · x₂
[prod^#(x₁)]	=	3 · x₁
[U171^#(x₁, x₂, x₃)]	=	1 · x₁ + 3 · x₂ + 3 · x₃

together with the usable rules

U51(tt,V1,V2)	→	U52(isBin(V1),V2)	(23)
U42(tt)	→	tt	(22)
isBag(empty)	→	tt	(35)
and(tt,X)	→	X	(34)
isBin(1(V1))	→	U41(isBinKind(V1),V1)	(43)
U21(tt,V1,V2)	→	U22(isBag(V1),V2)	(16)
isBag(singl(V1))	→	U11(isBinKind(V1),V1)	(36)
U82(tt)	→	tt	(32)
isBagKind(empty)	→	tt	(38)
U41(tt,V1)	→	U42(isBin(V1))	(21)
U11(tt,V1)	→	U12(isBin(V1))	(5)
U31(tt,V1)	→	U32(isBin(V1))	(19)
U72(tt)	→	tt	(30)
isBin(plus(V1,V2))	→	U61(and(isBinKind(V1),isBinKind(V2)),V1,V2)	(45)
isBinKind(sum(V1))	→	isBagKind(V1)	(54)
U52(tt,V2)	→	U53(isBin(V2))	(24)
U23(tt)	→	tt	(18)
isBagKind(union(V1,V2))	→	and(isBagKind(V1),isBagKind(V2))	(40)
U71(tt,V1)	→	U72(isBag(V1))	(29)
isBagKind(singl(V1))	→	isBinKind(V1)	(39)
isBag(union(V1,V2))	→	U21(and(isBagKind(V1),isBagKind(V2)),V1,V2)	(37)
U22(tt,V2)	→	U23(isBag(V2))	(17)
isBinKind(prod(V1))	→	isBagKind(V1)	(53)
isBin(z)	→	tt	(41)
isBin(sum(V1))	→	U81(isBagKind(V1),V1)	(47)
U12(tt)	→	tt	(7)
isBin(0(V1))	→	U31(isBinKind(V1),V1)	(42)
isBinKind(plus(V1,V2))	→	and(isBinKind(V1),isBinKind(V2))	(52)
isBinKind(0(V1))	→	isBinKind(V1)	(49)
U32(tt)	→	tt	(20)
U61(tt,V1,V2)	→	U62(isBin(V1),V2)	(26)
U53(tt)	→	tt	(25)
U62(tt,V2)	→	U63(isBin(V2))	(27)
U81(tt,V1)	→	U82(isBag(V1))	(31)
isBinKind(1(V1))	→	isBinKind(V1)	(50)
U63(tt)	→	tt	(28)
isBin(prod(V1))	→	U71(isBagKind(V1),V1)	(46)
isBin(mult(V1,V2))	→	U51(and(isBinKind(V1),isBinKind(V2)),V1,V2)	(44)
isBinKind(z)	→	tt	(48)
isBinKind(mult(V1,V2))	→	and(isBinKind(V1),isBinKind(V2))	(51)

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

prod^#(union(A,B))

→

U171^#(and(and(isBag(A),isBagKind(A)),and(isBag(B),isBagKind(B))),A,B)

(210)

and the rules

union(X,empty)	→	X	(1)
union(empty,X)	→	X	(2)
0(z)	→	z	(3)
U101(tt,X,Y)	→	0(mult(X,Y))	(4)
U111(tt,X,Y)	→	plus(0(mult(X,Y)),Y)	(6)
U121(tt,X)	→	X	(8)
U131(tt,X,Y)	→	0(plus(X,Y))	(9)
U141(tt,X,Y)	→	1(plus(X,Y))	(10)
U151(tt,X,Y)	→	0(plus(plus(X,Y),1(z)))	(11)
U161(tt,X)	→	X	(12)
U171(tt,A,B)	→	mult(prod(A),prod(B))	(13)
U181(tt,X)	→	X	(14)
U191(tt,A,B)	→	plus(sum(A),sum(B))	(15)
U61(tt,V1,V2)	→	U62(isBin(V1),V2)	(26)
U62(tt,V2)	→	U63(isBin(V2))	(27)
U91(tt)	→	z	(33)
isBag(empty)	→	tt	(35)
isBag(singl(V1))	→	U11(isBinKind(V1),V1)	(36)
isBag(union(V1,V2))	→	U21(and(isBagKind(V1),isBagKind(V2)),V1,V2)	(37)
isBagKind(empty)	→	tt	(38)
isBagKind(singl(V1))	→	isBinKind(V1)	(39)
isBagKind(union(V1,V2))	→	and(isBagKind(V1),isBagKind(V2))	(40)
isBin(z)	→	tt	(41)
isBin(0(V1))	→	U31(isBinKind(V1),V1)	(42)
isBin(1(V1))	→	U41(isBinKind(V1),V1)	(43)
isBin(mult(V1,V2))	→	U51(and(isBinKind(V1),isBinKind(V2)),V1,V2)	(44)
isBin(plus(V1,V2))	→	U61(and(isBinKind(V1),isBinKind(V2)),V1,V2)	(45)
isBin(prod(V1))	→	U71(isBagKind(V1),V1)	(46)
isBin(sum(V1))	→	U81(isBagKind(V1),V1)	(47)
isBinKind(z)	→	tt	(48)
isBinKind(0(V1))	→	isBinKind(V1)	(49)
isBinKind(1(V1))	→	isBinKind(V1)	(50)
isBinKind(mult(V1,V2))	→	and(isBinKind(V1),isBinKind(V2))	(51)
isBinKind(plus(V1,V2))	→	and(isBinKind(V1),isBinKind(V2))	(52)
isBinKind(prod(V1))	→	isBagKind(V1)	(53)
isBinKind(sum(V1))	→	isBagKind(V1)	(54)
mult(z,X)	→	U91(and(isBin(X),isBinKind(X)))	(55)
mult(0(X),Y)	→	U101(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)	(56)
mult(1(X),Y)	→	U111(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)	(57)
plus(z,X)	→	U121(and(isBin(X),isBinKind(X)),X)	(58)
plus(0(X),0(Y))	→	U131(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)	(59)
plus(0(X),1(Y))	→	U141(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)	(60)
plus(1(X),1(Y))	→	U151(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)	(61)
prod(empty)	→	1(z)	(62)
prod(singl(X))	→	U161(and(isBin(X),isBinKind(X)),X)	(63)
prod(union(A,B))	→	U171(and(and(isBag(A),isBagKind(A)),and(isBag(B),isBagKind(B))),A,B)	(64)
sum(empty)	→	0(z)	(65)
sum(singl(X))	→	U181(and(isBin(X),isBinKind(X)),X)	(66)
sum(union(A,B))	→	U191(and(and(isBag(A),isBagKind(A)),and(isBag(B),isBagKind(B))),A,B)	(67)
mult(mult(z,X),ext)	→	mult(U91(and(isBin(X),isBinKind(X))),ext)	(288)
mult(mult(0(X),Y),ext)	→	mult(U101(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y),ext)	(289)
mult(mult(1(X),Y),ext)	→	mult(U111(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y),ext)	(290)
plus(plus(z,X),ext)	→	plus(U121(and(isBin(X),isBinKind(X)),X),ext)	(291)
plus(plus(0(X),0(Y)),ext)	→	plus(U131(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y),ext)	(292)
plus(plus(0(X),1(Y)),ext)	→	plus(U141(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y),ext)	(293)
plus(plus(1(X),1(Y)),ext)	→	plus(U151(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y),ext)	(294)
union(union(X,empty),ext)	→	union(X,ext)	(295)
union(union(empty,X),ext)	→	union(X,ext)	(296)

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

U101^#(tt,X,Y)	→	mult^#(X,Y)	(84)
mult^#(0(X),Y)	→	U101^#(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)	(162)
mult^#(1(X),Y)	→	U111^#(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)	(170)
U111^#(tt,X,Y)	→	mult^#(X,Y)	(89)
mult^#(mult(z,X),ext)	→	mult^#(U91(and(isBin(X),isBinKind(X))),ext)	(231)
mult^#(mult(0(X),Y),ext)	→	mult^#(U101(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y),ext)	(236)
mult^#(mult(0(X),Y),ext)	→	U101^#(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)	(237)
mult^#(mult(1(X),Y),ext)	→	mult^#(U111(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y),ext)	(245)
mult^#(mult(1(X),Y),ext)	→	U111^#(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)	(246)
mult^#(mult(x,y),z')	→	mult^#(y,z')	(80)
mult^#(x,y)	→	mult^#(y,x)	(74)
mult^#(mult(x,y),z')	→	mult^#(x,mult(y,z'))	(77)

1.1.2 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₂
[z]	=	0
[U91(x₁)]	=	0
[and(x₁, x₂)]	=	1 · x₂
[isBin(x₁)]	=	0
[isBinKind(x₁)]	=	1
[0(x₁)]	=	1 + 1 · x₁
[U101^#(x₁, x₂, x₃)]	=	1 · x₃ + 1 · x₂ + 1 · x₂ · x₃
[U111^#(x₁, x₂, x₃)]	=	1 · x₃ + 1 · x₂ + 1 · x₂ · x₃
[tt]	=	1
[U101(x₁, x₂, x₃)]	=	1 · x₃ + 1 · x₂ + 1 · x₁ + 1 · x₂ · x₃
[1(x₁)]	=	1 + 1 · x₁
[U111(x₁, x₂, x₃)]	=	1 · x₃ + 1 · x₂ + 1 · x₁ + 1 · x₂ · x₃ + 1 · x₁ · x₃
[isBagKind(x₁)]	=	1
[empty]	=	1
[union(x₁, x₂)]	=	0
[singl(x₁)]	=	0
[U52(x₁, x₂)]	=	1 · x₂ + 1 · x₁ · x₂
[U53(x₁)]	=	1
[U62(x₁, x₂)]	=	1 · x₂
[U63(x₁)]	=	1
[U81(x₁, x₂)]	=	1 + 1 · x₂
[U82(x₁)]	=	1 + 1 · x₁
[isBag(x₁)]	=	0
[U121(x₁, x₂)]	=	1 · x₂
[U141(x₁, x₂, x₃)]	=	1 + 1 · x₃ + 1 · x₂
[plus(x₁, x₂)]	=	1 · x₂ + 1 · x₁
[U12(x₁)]	=	1 + 1 · x₁
[U71(x₁, x₂)]	=	1 · x₂
[U72(x₁)]	=	1 + 1 · x₁
[U61(x₁, x₂, x₃)]	=	1 · x₂ + 1 · x₂ · x₃
[U151(x₁, x₂, x₃)]	=	1 + 1 · x₃ + 1 · x₂ + 1 · x₁
[U31(x₁, x₂)]	=	1 · x₂
[U41(x₁, x₂)]	=	1 · x₂
[sum(x₁)]	=	0
[prod(x₁)]	=	0
[U51(x₁, x₂, x₃)]	=	1 + 1 · x₃ + 1 · x₂ + 1 · x₂ · x₃
[U11(x₁, x₂)]	=	1 + 1 · x₂
[U22(x₁, x₂)]	=	1 · x₂
[U23(x₁)]	=	1 + 1 · x₁
[U32(x₁)]	=	1
[U21(x₁, x₂, x₃)]	=	1 · x₃ + 1 · x₂ + 1 · x₂ · x₃
[U42(x₁)]	=	1
[U131(x₁, x₂, x₃)]	=	1 + 1 · x₃ + 1 · x₂

together with the usable rules

isBagKind(empty)	→	tt	(38)
isBagKind(union(V1,V2))	→	and(isBagKind(V1),isBagKind(V2))	(40)
isBagKind(singl(V1))	→	isBinKind(V1)	(39)
U121(tt,X)	→	X	(8)
mult(mult(0(X),Y),ext)	→	mult(U101(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y),ext)	(289)
mult(z,X)	→	U91(and(isBin(X),isBinKind(X)))	(55)
mult(mult(z,X),ext)	→	mult(U91(and(isBin(X),isBinKind(X))),ext)	(288)
mult(0(X),Y)	→	U101(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)	(56)
mult(1(X),Y)	→	U111(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)	(57)
mult(mult(1(X),Y),ext)	→	mult(U111(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y),ext)	(290)
U141(tt,X,Y)	→	1(plus(X,Y))	(10)
U91(tt)	→	z	(33)
U101(tt,X,Y)	→	0(mult(X,Y))	(4)
U151(tt,X,Y)	→	0(plus(plus(X,Y),1(z)))	(11)
0(z)	→	z	(3)
and(tt,X)	→	X	(34)
isBinKind(sum(V1))	→	isBagKind(V1)	(54)
isBinKind(prod(V1))	→	isBagKind(V1)	(53)
isBinKind(plus(V1,V2))	→	and(isBinKind(V1),isBinKind(V2))	(52)
isBinKind(mult(V1,V2))	→	and(isBinKind(V1),isBinKind(V2))	(51)
isBinKind(0(V1))	→	isBinKind(V1)	(49)
isBinKind(1(V1))	→	isBinKind(V1)	(50)
isBinKind(z)	→	tt	(48)
U111(tt,X,Y)	→	plus(0(mult(X,Y)),Y)	(6)
U131(tt,X,Y)	→	0(plus(X,Y))	(9)
plus(0(X),1(Y))	→	U141(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)	(60)
plus(plus(0(X),0(Y)),ext)	→	plus(U131(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y),ext)	(292)
plus(plus(z,X),ext)	→	plus(U121(and(isBin(X),isBinKind(X)),X),ext)	(291)
plus(0(X),0(Y))	→	U131(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)	(59)
plus(plus(1(X),1(Y)),ext)	→	plus(U151(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y),ext)	(294)
plus(z,X)	→	U121(and(isBin(X),isBinKind(X)),X)	(58)
plus(1(X),1(Y))	→	U151(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)	(61)
plus(plus(0(X),1(Y)),ext)	→	plus(U141(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y),ext)	(293)
mult(x,y)	→	mult(y,x)	(68)
mult(mult(x,y),z')	→	mult(x,mult(y,z'))	(71)
plus(plus(x,y),z')	→	plus(x,plus(y,z'))	(72)
plus(x,y)	→	plus(y,x)	(69)

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

mult^#(mult(0(X),Y),ext)	→	U101^#(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)	(237)
mult^#(0(X),Y)	→	U101^#(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)	(162)
mult^#(mult(1(X),Y),ext)	→	U111^#(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)	(246)
mult^#(1(X),Y)	→	U111^#(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)	(170)

could be deleted.

1.1.2.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

mult^#(mult(0(X),Y),ext)	→	mult^#(U101(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y),ext)	(236)
mult^#(mult(z,X),ext)	→	mult^#(U91(and(isBin(X),isBinKind(X))),ext)	(231)
mult^#(mult(1(X),Y),ext)	→	mult^#(U111(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y),ext)	(245)
mult^#(mult(x,y),z')	→	mult^#(y,z')	(80)
mult^#(x,y)	→	mult^#(y,x)	(74)
mult^#(mult(x,y),z')	→	mult^#(x,mult(y,z'))	(77)

1.1.2.1.1 AC Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the naturals

[mult^#(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[mult(x₁, x₂)]	=	3 + 1 · x₁ + 1 · x₂
[z]	=	0
[U91(x₁)]	=	0
[and(x₁, x₂)]	=	0
[isBin(x₁)]	=	0
[isBinKind(x₁)]	=	0
[0(x₁)]	=	0
[U101(x₁, x₂, x₃)]	=	0
[1(x₁)]	=	2
[U111(x₁, x₂, x₃)]	=	2 + 1 · x₃
[U12(x₁)]	=	3
[tt]	=	0
[sum(x₁)]	=	0
[isBagKind(x₁)]	=	0
[prod(x₁)]	=	0
[plus(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[U62(x₁, x₂)]	=	3 + 3 · x₂
[U63(x₁)]	=	3
[U23(x₁)]	=	3
[empty]	=	0
[union(x₁, x₂)]	=	0
[singl(x₁)]	=	0
[U32(x₁)]	=	3
[U51(x₁, x₂, x₃)]	=	3 + 3 · x₂ + 3 · x₃
[U52(x₁, x₂)]	=	3 + 3 · x₂
[isBag(x₁)]	=	0
[U11(x₁, x₂)]	=	3 + 3 · x₂
[U21(x₁, x₂, x₃)]	=	3 + 3 · x₂ + 3 · x₃
[U151(x₁, x₂, x₃)]	=	2
[U71(x₁, x₂)]	=	3 + 3 · x₂
[U72(x₁)]	=	3
[U22(x₁, x₂)]	=	3 + 3 · x₂
[U31(x₁, x₂)]	=	3 + 3 · x₂
[U42(x₁)]	=	3
[U41(x₁, x₂)]	=	3 + 3 · x₂
[U53(x₁)]	=	3
[U82(x₁)]	=	3
[U131(x₁, x₂, x₃)]	=	1
[U61(x₁, x₂, x₃)]	=	3 + 3 · x₂ + 3 · x₃
[U141(x₁, x₂, x₃)]	=	2
[U121(x₁, x₂)]	=	1 + 1 · x₂
[U81(x₁, x₂)]	=	3 + 3 · x₂

together with the usable rules

U91(tt)	→	z	(33)
mult(mult(0(X),Y),ext)	→	mult(U101(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y),ext)	(289)
mult(z,X)	→	U91(and(isBin(X),isBinKind(X)))	(55)
mult(mult(z,X),ext)	→	mult(U91(and(isBin(X),isBinKind(X))),ext)	(288)
mult(0(X),Y)	→	U101(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)	(56)
mult(1(X),Y)	→	U111(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)	(57)
mult(mult(1(X),Y),ext)	→	mult(U111(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y),ext)	(290)
U151(tt,X,Y)	→	0(plus(plus(X,Y),1(z)))	(11)
U101(tt,X,Y)	→	0(mult(X,Y))	(4)
U131(tt,X,Y)	→	0(plus(X,Y))	(9)
U111(tt,X,Y)	→	plus(0(mult(X,Y)),Y)	(6)
plus(0(X),1(Y))	→	U141(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)	(60)
plus(plus(0(X),0(Y)),ext)	→	plus(U131(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y),ext)	(292)
plus(plus(z,X),ext)	→	plus(U121(and(isBin(X),isBinKind(X)),X),ext)	(291)
plus(0(X),0(Y))	→	U131(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)	(59)
plus(plus(1(X),1(Y)),ext)	→	plus(U151(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y),ext)	(294)
plus(z,X)	→	U121(and(isBin(X),isBinKind(X)),X)	(58)
plus(1(X),1(Y))	→	U151(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)	(61)
plus(plus(0(X),1(Y)),ext)	→	plus(U141(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y),ext)	(293)
U141(tt,X,Y)	→	1(plus(X,Y))	(10)
U121(tt,X)	→	X	(8)
0(z)	→	z	(3)
mult(x,y)	→	mult(y,x)	(68)
mult(mult(x,y),z')	→	mult(x,mult(y,z'))	(71)
plus(plus(x,y),z')	→	plus(x,plus(y,z'))	(72)
plus(x,y)	→	plus(y,x)	(69)

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

mult^#(mult(z,X),ext)	→	mult^#(U91(and(isBin(X),isBinKind(X))),ext)	(231)
mult^#(mult(x,y),z')	→	mult^#(y,z')	(80)
mult^#(mult(0(X),Y),ext)	→	mult^#(U101(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y),ext)	(236)
mult^#(mult(1(X),Y),ext)	→	mult^#(U111(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y),ext)	(245)

could be deleted.

1.1.2.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 3^rd component contains the pair

U191^#(tt,A,B)	→	sum^#(A)	(100)
sum^#(union(A,B))	→	U191^#(and(and(isBag(A),isBagKind(A)),and(isBag(B),isBagKind(B))),A,B)	(223)
U191^#(tt,A,B)	→	sum^#(B)	(101)

1.1.3 AC Monotonic Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the naturals

[U51(x₁, x₂, x₃)]	=	2 · x₁ + 1 · x₂ + 1 · x₃
[tt]	=	0
[U52(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[isBin(x₁)]	=	1 · x₁
[U42(x₁)]	=	1 · x₁
[isBag(x₁)]	=	1 · x₁
[empty]	=	0
[and(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[1(x₁)]	=	2 · x₁
[U41(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[isBinKind(x₁)]	=	1 · x₁
[U21(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 1 · x₃
[U22(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[singl(x₁)]	=	1 + 3 · x₁
[U11(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[U82(x₁)]	=	1 · x₁
[isBagKind(x₁)]	=	2 · x₁
[U12(x₁)]	=	2 · x₁
[U31(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[U32(x₁)]	=	1 · x₁
[U72(x₁)]	=	1 · x₁
[plus(x₁, x₂)]	=	3 + 3 · x₁ + 3 · x₂
[U61(x₁, x₂, x₃)]	=	3 + 1 · x₁ + 1 · x₂ + 2 · x₃
[sum(x₁)]	=	3 · x₁
[U53(x₁)]	=	1 · x₁
[U23(x₁)]	=	1 · x₁
[union(x₁, x₂)]	=	3 · x₁ + 3 · x₂
[U71(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[prod(x₁)]	=	1 + 3 · x₁
[z]	=	0
[U81(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[0(x₁)]	=	2 + 3 · x₁
[U62(x₁, x₂)]	=	2 + 1 · x₁ + 1 · x₂
[U63(x₁)]	=	1 · x₁
[mult(x₁, x₂)]	=	3 · x₁ + 3 · x₂
[sum^#(x₁)]	=	3 · x₁
[U191^#(x₁, x₂, x₃)]	=	1 · x₁ + 3 · x₂ + 3 · x₃

together with the usable rules

U51(tt,V1,V2)	→	U52(isBin(V1),V2)	(23)
U42(tt)	→	tt	(22)
isBag(empty)	→	tt	(35)
and(tt,X)	→	X	(34)
isBin(1(V1))	→	U41(isBinKind(V1),V1)	(43)
U21(tt,V1,V2)	→	U22(isBag(V1),V2)	(16)
isBag(singl(V1))	→	U11(isBinKind(V1),V1)	(36)
U82(tt)	→	tt	(32)
isBagKind(empty)	→	tt	(38)
U41(tt,V1)	→	U42(isBin(V1))	(21)
U11(tt,V1)	→	U12(isBin(V1))	(5)
U31(tt,V1)	→	U32(isBin(V1))	(19)
U72(tt)	→	tt	(30)
isBin(plus(V1,V2))	→	U61(and(isBinKind(V1),isBinKind(V2)),V1,V2)	(45)
isBinKind(sum(V1))	→	isBagKind(V1)	(54)
U52(tt,V2)	→	U53(isBin(V2))	(24)
U23(tt)	→	tt	(18)
isBagKind(union(V1,V2))	→	and(isBagKind(V1),isBagKind(V2))	(40)
U71(tt,V1)	→	U72(isBag(V1))	(29)
isBagKind(singl(V1))	→	isBinKind(V1)	(39)
isBag(union(V1,V2))	→	U21(and(isBagKind(V1),isBagKind(V2)),V1,V2)	(37)
U22(tt,V2)	→	U23(isBag(V2))	(17)
isBinKind(prod(V1))	→	isBagKind(V1)	(53)
isBin(z)	→	tt	(41)
isBin(sum(V1))	→	U81(isBagKind(V1),V1)	(47)
U12(tt)	→	tt	(7)
isBin(0(V1))	→	U31(isBinKind(V1),V1)	(42)
isBinKind(plus(V1,V2))	→	and(isBinKind(V1),isBinKind(V2))	(52)
isBinKind(0(V1))	→	isBinKind(V1)	(49)
U32(tt)	→	tt	(20)
U61(tt,V1,V2)	→	U62(isBin(V1),V2)	(26)
U53(tt)	→	tt	(25)
U62(tt,V2)	→	U63(isBin(V2))	(27)
U81(tt,V1)	→	U82(isBag(V1))	(31)
isBinKind(1(V1))	→	isBinKind(V1)	(50)
U63(tt)	→	tt	(28)
isBin(prod(V1))	→	U71(isBagKind(V1),V1)	(46)
isBin(mult(V1,V2))	→	U51(and(isBinKind(V1),isBinKind(V2)),V1,V2)	(44)
isBinKind(z)	→	tt	(48)
isBinKind(mult(V1,V2))	→	and(isBinKind(V1),isBinKind(V2))	(51)

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

sum^#(union(A,B))

→

U191^#(and(and(isBag(A),isBagKind(A)),and(isBag(B),isBagKind(B))),A,B)

(223)

and the rules

union(X,empty)	→	X	(1)
union(empty,X)	→	X	(2)
0(z)	→	z	(3)
U101(tt,X,Y)	→	0(mult(X,Y))	(4)
U111(tt,X,Y)	→	plus(0(mult(X,Y)),Y)	(6)
U121(tt,X)	→	X	(8)
U131(tt,X,Y)	→	0(plus(X,Y))	(9)
U141(tt,X,Y)	→	1(plus(X,Y))	(10)
U151(tt,X,Y)	→	0(plus(plus(X,Y),1(z)))	(11)
U161(tt,X)	→	X	(12)
U171(tt,A,B)	→	mult(prod(A),prod(B))	(13)
U181(tt,X)	→	X	(14)
U191(tt,A,B)	→	plus(sum(A),sum(B))	(15)
U61(tt,V1,V2)	→	U62(isBin(V1),V2)	(26)
U62(tt,V2)	→	U63(isBin(V2))	(27)
U91(tt)	→	z	(33)
isBag(empty)	→	tt	(35)
isBag(singl(V1))	→	U11(isBinKind(V1),V1)	(36)
isBag(union(V1,V2))	→	U21(and(isBagKind(V1),isBagKind(V2)),V1,V2)	(37)
isBagKind(empty)	→	tt	(38)
isBagKind(singl(V1))	→	isBinKind(V1)	(39)
isBagKind(union(V1,V2))	→	and(isBagKind(V1),isBagKind(V2))	(40)
isBin(z)	→	tt	(41)
isBin(0(V1))	→	U31(isBinKind(V1),V1)	(42)
isBin(1(V1))	→	U41(isBinKind(V1),V1)	(43)
isBin(mult(V1,V2))	→	U51(and(isBinKind(V1),isBinKind(V2)),V1,V2)	(44)
isBin(plus(V1,V2))	→	U61(and(isBinKind(V1),isBinKind(V2)),V1,V2)	(45)
isBin(prod(V1))	→	U71(isBagKind(V1),V1)	(46)
isBin(sum(V1))	→	U81(isBagKind(V1),V1)	(47)
isBinKind(z)	→	tt	(48)
isBinKind(0(V1))	→	isBinKind(V1)	(49)
isBinKind(1(V1))	→	isBinKind(V1)	(50)
isBinKind(mult(V1,V2))	→	and(isBinKind(V1),isBinKind(V2))	(51)
isBinKind(plus(V1,V2))	→	and(isBinKind(V1),isBinKind(V2))	(52)
isBinKind(prod(V1))	→	isBagKind(V1)	(53)
isBinKind(sum(V1))	→	isBagKind(V1)	(54)
mult(z,X)	→	U91(and(isBin(X),isBinKind(X)))	(55)
mult(0(X),Y)	→	U101(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)	(56)
mult(1(X),Y)	→	U111(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)	(57)
plus(z,X)	→	U121(and(isBin(X),isBinKind(X)),X)	(58)
plus(0(X),0(Y))	→	U131(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)	(59)
plus(0(X),1(Y))	→	U141(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)	(60)
plus(1(X),1(Y))	→	U151(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)	(61)
prod(empty)	→	1(z)	(62)
prod(singl(X))	→	U161(and(isBin(X),isBinKind(X)),X)	(63)
prod(union(A,B))	→	U171(and(and(isBag(A),isBagKind(A)),and(isBag(B),isBagKind(B))),A,B)	(64)
sum(empty)	→	0(z)	(65)
sum(singl(X))	→	U181(and(isBin(X),isBinKind(X)),X)	(66)
sum(union(A,B))	→	U191(and(and(isBag(A),isBagKind(A)),and(isBag(B),isBagKind(B))),A,B)	(67)
mult(mult(z,X),ext)	→	mult(U91(and(isBin(X),isBinKind(X))),ext)	(288)
mult(mult(0(X),Y),ext)	→	mult(U101(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y),ext)	(289)
mult(mult(1(X),Y),ext)	→	mult(U111(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y),ext)	(290)
plus(plus(z,X),ext)	→	plus(U121(and(isBin(X),isBinKind(X)),X),ext)	(291)
plus(plus(0(X),0(Y)),ext)	→	plus(U131(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y),ext)	(292)
plus(plus(0(X),1(Y)),ext)	→	plus(U141(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y),ext)	(293)
plus(plus(1(X),1(Y)),ext)	→	plus(U151(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y),ext)	(294)
union(union(X,empty),ext)	→	union(X,ext)	(295)
union(union(empty,X),ext)	→	union(X,ext)	(296)

could be deleted.

1.1.3.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 4^th component contains the pair

plus^#(0(X),0(Y))	→	U131^#(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)	(182)
U131^#(tt,X,Y)	→	plus^#(X,Y)	(91)
plus^#(0(X),1(Y))	→	U141^#(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)	(190)
U141^#(tt,X,Y)	→	plus^#(X,Y)	(92)
plus^#(1(X),1(Y))	→	U151^#(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)	(198)
U151^#(tt,X,Y)	→	plus^#(plus(X,Y),1(z))	(94)
plus^#(plus(z,X),ext)	→	plus^#(U121(and(isBin(X),isBinKind(X)),X),ext)	(254)
plus^#(plus(0(X),0(Y)),ext)	→	plus^#(U131(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y),ext)	(259)
plus^#(plus(0(X),0(Y)),ext)	→	U131^#(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)	(260)
plus^#(plus(0(X),1(Y)),ext)	→	plus^#(U141(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y),ext)	(268)
plus^#(plus(0(X),1(Y)),ext)	→	U141^#(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)	(269)
plus^#(plus(1(X),1(Y)),ext)	→	plus^#(U151(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y),ext)	(277)
plus^#(plus(1(X),1(Y)),ext)	→	U151^#(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)	(278)
U151^#(tt,X,Y)	→	plus^#(X,Y)	(95)
plus^#(plus(x,y),z')	→	plus^#(y,z')	(81)
plus^#(x,y)	→	plus^#(y,x)	(75)
plus^#(plus(x,y),z')	→	plus^#(x,plus(y,z'))	(78)

1.1.4 AC Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the naturals

[U151^#(x₁, x₂, x₃)]	=	2 + 1 · x₂ + 1 · x₃
[tt]	=	0
[plus^#(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[plus(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[0(x₁)]	=	1 + 1 · x₁
[1(x₁)]	=	1 + 1 · x₁
[U141(x₁, x₂, x₃)]	=	1 + 1 · x₂ + 1 · x₃
[and(x₁, x₂)]	=	0
[isBin(x₁)]	=	0
[isBinKind(x₁)]	=	0
[U141^#(x₁, x₂, x₃)]	=	1 · x₂ + 1 · x₃
[U131(x₁, x₂, x₃)]	=	1 + 1 · x₂ + 1 · x₃
[U151(x₁, x₂, x₃)]	=	2 + 1 · x₂ + 1 · x₃
[z]	=	0
[U121(x₁, x₂)]	=	1 · x₂
[U131^#(x₁, x₂, x₃)]	=	1 + 1 · x₂ + 1 · x₃
[U52(x₁, x₂)]	=	3 + 3 · x₂
[U53(x₁)]	=	3
[isBag(x₁)]	=	0
[empty]	=	0
[singl(x₁)]	=	0
[U11(x₁, x₂)]	=	3 + 3 · x₂
[union(x₁, x₂)]	=	0
[U21(x₁, x₂, x₃)]	=	3 + 3 · x₂ + 3 · x₃
[isBagKind(x₁)]	=	0
[U61(x₁, x₂, x₃)]	=	3 + 3 · x₂ + 3 · x₃
[U62(x₁, x₂)]	=	3 + 3 · x₂
[U63(x₁)]	=	3
[U32(x₁)]	=	3
[sum(x₁)]	=	0
[prod(x₁)]	=	0
[mult(x₁, x₂)]	=	0
[U82(x₁)]	=	3
[U41(x₁, x₂)]	=	3 + 3 · x₂
[U42(x₁)]	=	3
[U12(x₁)]	=	3
[U22(x₁, x₂)]	=	3 + 3 · x₂
[U23(x₁)]	=	3
[U31(x₁, x₂)]	=	3 + 3 · x₂
[U51(x₁, x₂, x₃)]	=	3 + 3 · x₂ + 3 · x₃
[U81(x₁, x₂)]	=	3 + 3 · x₂
[U71(x₁, x₂)]	=	3 + 3 · x₂
[U72(x₁)]	=	3

together with the usable rules

0(z)	→	z	(3)
plus(0(X),1(Y))	→	U141(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)	(60)
plus(plus(0(X),0(Y)),ext)	→	plus(U131(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y),ext)	(292)
plus(plus(z,X),ext)	→	plus(U121(and(isBin(X),isBinKind(X)),X),ext)	(291)
plus(0(X),0(Y))	→	U131(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)	(59)
plus(plus(1(X),1(Y)),ext)	→	plus(U151(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y),ext)	(294)
plus(z,X)	→	U121(and(isBin(X),isBinKind(X)),X)	(58)
plus(1(X),1(Y))	→	U151(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)	(61)
plus(plus(0(X),1(Y)),ext)	→	plus(U141(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y),ext)	(293)
U151(tt,X,Y)	→	0(plus(plus(X,Y),1(z)))	(11)
U131(tt,X,Y)	→	0(plus(X,Y))	(9)
U121(tt,X)	→	X	(8)
U141(tt,X,Y)	→	1(plus(X,Y))	(10)
plus(plus(x,y),z')	→	plus(x,plus(y,z'))	(72)
plus(x,y)	→	plus(y,x)	(69)

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

U151^#(tt,X,Y)	→	plus^#(X,Y)	(95)
plus^#(plus(0(X),1(Y)),ext)	→	plus^#(U141(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y),ext)	(268)
plus^#(0(X),1(Y))	→	U141^#(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)	(190)
plus^#(plus(0(X),1(Y)),ext)	→	U141^#(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)	(269)
plus^#(plus(0(X),0(Y)),ext)	→	plus^#(U131(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y),ext)	(259)
U151^#(tt,X,Y)	→	plus^#(plus(X,Y),1(z))	(94)
plus^#(0(X),0(Y))	→	U131^#(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)	(182)
U131^#(tt,X,Y)	→	plus^#(X,Y)	(91)
plus^#(plus(0(X),0(Y)),ext)	→	U131^#(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)	(260)

could be deleted.

1.1.4.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

plus^#(plus(z,X),ext)	→	plus^#(U121(and(isBin(X),isBinKind(X)),X),ext)	(254)
plus^#(plus(1(X),1(Y)),ext)	→	plus^#(U151(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y),ext)	(277)
plus^#(plus(x,y),z')	→	plus^#(y,z')	(81)
plus^#(x,y)	→	plus^#(y,x)	(75)
plus^#(plus(x,y),z')	→	plus^#(x,plus(y,z'))	(78)

1.1.4.1.1 AC Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the naturals

[plus^#(x₁, x₂)]	=	3 · x₁ + 3 · x₂
[plus(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[1(x₁)]	=	0
[U151(x₁, x₂, x₃)]	=	1
[and(x₁, x₂)]	=	0
[isBin(x₁)]	=	0
[isBinKind(x₁)]	=	0
[z]	=	0
[U121(x₁, x₂)]	=	1 · x₂
[U23(x₁)]	=	3
[tt]	=	0
[U82(x₁)]	=	3
[isBag(x₁)]	=	0
[empty]	=	0
[singl(x₁)]	=	0
[U11(x₁, x₂)]	=	3 + 3 · x₂
[union(x₁, x₂)]	=	0
[U21(x₁, x₂, x₃)]	=	3 + 3 · x₂ + 3 · x₃
[isBagKind(x₁)]	=	0
[0(x₁)]	=	0
[U141(x₁, x₂, x₃)]	=	1
[U131(x₁, x₂, x₃)]	=	0
[U63(x₁)]	=	3
[U22(x₁, x₂)]	=	3 + 3 · x₂
[U72(x₁)]	=	3
[U32(x₁)]	=	3
[U61(x₁, x₂, x₃)]	=	3 + 3 · x₂ + 3 · x₃
[U62(x₁, x₂)]	=	3 + 3 · x₂
[U51(x₁, x₂, x₃)]	=	3 + 3 · x₂ + 3 · x₃
[U52(x₁, x₂)]	=	3 + 3 · x₂
[U53(x₁)]	=	3
[U12(x₁)]	=	3
[U42(x₁)]	=	3
[sum(x₁)]	=	0
[prod(x₁)]	=	0
[mult(x₁, x₂)]	=	0
[U71(x₁, x₂)]	=	3 + 3 · x₂
[U81(x₁, x₂)]	=	3 + 3 · x₂
[U31(x₁, x₂)]	=	3 + 3 · x₂
[U41(x₁, x₂)]	=	3 + 3 · x₂

together with the usable rules

0(z)	→	z	(3)
plus(0(X),1(Y))	→	U141(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)	(60)
plus(plus(0(X),0(Y)),ext)	→	plus(U131(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y),ext)	(292)
plus(plus(z,X),ext)	→	plus(U121(and(isBin(X),isBinKind(X)),X),ext)	(291)
plus(0(X),0(Y))	→	U131(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)	(59)
plus(plus(1(X),1(Y)),ext)	→	plus(U151(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y),ext)	(294)
plus(z,X)	→	U121(and(isBin(X),isBinKind(X)),X)	(58)
plus(1(X),1(Y))	→	U151(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)	(61)
plus(plus(0(X),1(Y)),ext)	→	plus(U141(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y),ext)	(293)
U151(tt,X,Y)	→	0(plus(plus(X,Y),1(z)))	(11)
U141(tt,X,Y)	→	1(plus(X,Y))	(10)
U121(tt,X)	→	X	(8)
U131(tt,X,Y)	→	0(plus(X,Y))	(9)
plus(plus(x,y),z')	→	plus(x,plus(y,z'))	(72)
plus(x,y)	→	plus(y,x)	(69)

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

plus^#(plus(z,X),ext)	→	plus^#(U121(and(isBin(X),isBinKind(X)),X),ext)	(254)
plus^#(plus(x,y),z')	→	plus^#(y,z')	(81)

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₂)]	=	1 · x₁ + 1 · x₂
[plus(x₁, x₂)]	=	3 + 1 · x₁ + 1 · x₂
[1(x₁)]	=	3
[U151(x₁, x₂, x₃)]	=	2 + 2 · x₁
[and(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[isBin(x₁)]	=	1
[isBinKind(x₁)]	=	0
[tt]	=	0
[0(x₁)]	=	2
[z]	=	1
[U31(x₁, x₂)]	=	0
[U32(x₁)]	=	0
[U121(x₁, x₂)]	=	2 + 2 · x₁ + 1 · x₂
[U141(x₁, x₂, x₃)]	=	3 + 1 · x₁
[U52(x₁, x₂)]	=	0
[U53(x₁)]	=	0
[U82(x₁)]	=	0
[U62(x₁, x₂)]	=	0
[U63(x₁)]	=	0
[U131(x₁, x₂, x₃)]	=	2
[U71(x₁, x₂)]	=	1
[U72(x₁)]	=	0
[isBag(x₁)]	=	2 + 2 · x₁
[U22(x₁, x₂)]	=	1
[U23(x₁)]	=	0
[U11(x₁, x₂)]	=	2
[U12(x₁)]	=	0
[U61(x₁, x₂, x₃)]	=	1
[U41(x₁, x₂)]	=	0
[sum(x₁)]	=	0
[U81(x₁, x₂)]	=	0
[isBagKind(x₁)]	=	0
[prod(x₁)]	=	0
[mult(x₁, x₂)]	=	0
[U51(x₁, x₂, x₃)]	=	0
[U42(x₁)]	=	0
[empty]	=	0
[singl(x₁)]	=	3 + 3 · x₁
[union(x₁, x₂)]	=	1 · x₁
[U21(x₁, x₂, x₃)]	=	1

together with the usable rules

U151(tt,X,Y)	→	0(plus(plus(X,Y),1(z)))	(11)
U31(tt,V1)	→	U32(isBin(V1))	(19)
U121(tt,X)	→	X	(8)
U141(tt,X,Y)	→	1(plus(X,Y))	(10)
U52(tt,V2)	→	U53(isBin(V2))	(24)
U82(tt)	→	tt	(32)
U62(tt,V2)	→	U63(isBin(V2))	(27)
U131(tt,X,Y)	→	0(plus(X,Y))	(9)
U71(tt,V1)	→	U72(isBag(V1))	(29)
U22(tt,V2)	→	U23(isBag(V2))	(17)
U11(tt,V1)	→	U12(isBin(V1))	(5)
U63(tt)	→	tt	(28)
U61(tt,V1,V2)	→	U62(isBin(V1),V2)	(26)
isBin(z)	→	tt	(41)
isBin(0(V1))	→	U31(isBinKind(V1),V1)	(42)
isBin(1(V1))	→	U41(isBinKind(V1),V1)	(43)
isBin(plus(V1,V2))	→	U61(and(isBinKind(V1),isBinKind(V2)),V1,V2)	(45)
isBin(sum(V1))	→	U81(isBagKind(V1),V1)	(47)
isBin(prod(V1))	→	U71(isBagKind(V1),V1)	(46)
isBin(mult(V1,V2))	→	U51(and(isBinKind(V1),isBinKind(V2)),V1,V2)	(44)
U51(tt,V1,V2)	→	U52(isBin(V1),V2)	(23)
U42(tt)	→	tt	(22)
U23(tt)	→	tt	(18)
U53(tt)	→	tt	(25)
U81(tt,V1)	→	U82(isBag(V1))	(31)
plus(0(X),1(Y))	→	U141(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)	(60)
plus(plus(0(X),0(Y)),ext)	→	plus(U131(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y),ext)	(292)
plus(plus(z,X),ext)	→	plus(U121(and(isBin(X),isBinKind(X)),X),ext)	(291)
plus(0(X),0(Y))	→	U131(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)	(59)
plus(plus(1(X),1(Y)),ext)	→	plus(U151(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y),ext)	(294)
plus(z,X)	→	U121(and(isBin(X),isBinKind(X)),X)	(58)
plus(1(X),1(Y))	→	U151(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)	(61)
plus(plus(0(X),1(Y)),ext)	→	plus(U141(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y),ext)	(293)
U12(tt)	→	tt	(7)
isBag(empty)	→	tt	(35)
isBag(singl(V1))	→	U11(isBinKind(V1),V1)	(36)
isBag(union(V1,V2))	→	U21(and(isBagKind(V1),isBagKind(V2)),V1,V2)	(37)
U32(tt)	→	tt	(20)
isBagKind(empty)	→	tt	(38)
isBagKind(union(V1,V2))	→	and(isBagKind(V1),isBagKind(V2))	(40)
isBagKind(singl(V1))	→	isBinKind(V1)	(39)
U21(tt,V1,V2)	→	U22(isBag(V1),V2)	(16)
isBinKind(sum(V1))	→	isBagKind(V1)	(54)
isBinKind(prod(V1))	→	isBagKind(V1)	(53)
isBinKind(plus(V1,V2))	→	and(isBinKind(V1),isBinKind(V2))	(52)
isBinKind(mult(V1,V2))	→	and(isBinKind(V1),isBinKind(V2))	(51)
isBinKind(0(V1))	→	isBinKind(V1)	(49)
isBinKind(1(V1))	→	isBinKind(V1)	(50)
isBinKind(z)	→	tt	(48)
0(z)	→	z	(3)
U41(tt,V1)	→	U42(isBin(V1))	(21)
and(tt,X)	→	X	(34)
U72(tt)	→	tt	(30)
plus(plus(x,y),z')	→	plus(x,plus(y,z'))	(72)
plus(x,y)	→	plus(y,x)	(69)

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

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

→

plus^#(U151(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y),ext)

(277)

could be deleted.

1.1.4.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

U11^#(tt,V1)	→	isBin^#(V1)	(86)
isBin^#(0(V1))	→	U31^#(isBinKind(V1),V1)	(132)
U31^#(tt,V1)	→	isBin^#(V1)	(107)
isBin^#(1(V1))	→	U41^#(isBinKind(V1),V1)	(134)
U41^#(tt,V1)	→	isBin^#(V1)	(109)
isBin^#(mult(V1,V2))	→	U51^#(and(isBinKind(V1),isBinKind(V2)),V1,V2)	(136)
U51^#(tt,V1,V2)	→	U52^#(isBin(V1),V2)	(110)
U52^#(tt,V2)	→	isBin^#(V2)	(113)
isBin^#(plus(V1,V2))	→	U61^#(and(isBinKind(V1),isBinKind(V2)),V1,V2)	(140)
U61^#(tt,V1,V2)	→	U62^#(isBin(V1),V2)	(114)
U62^#(tt,V2)	→	isBin^#(V2)	(117)
isBin^#(prod(V1))	→	U71^#(isBagKind(V1),V1)	(144)
U71^#(tt,V1)	→	isBag^#(V1)	(119)
isBag^#(singl(V1))	→	U11^#(isBinKind(V1),V1)	(122)
isBag^#(union(V1,V2))	→	U21^#(and(isBagKind(V1),isBagKind(V2)),V1,V2)	(124)
U21^#(tt,V1,V2)	→	U22^#(isBag(V1),V2)	(102)
U22^#(tt,V2)	→	isBag^#(V2)	(105)
U21^#(tt,V1,V2)	→	isBag^#(V1)	(103)
isBin^#(sum(V1))	→	U81^#(isBagKind(V1),V1)	(146)
U81^#(tt,V1)	→	isBag^#(V1)	(121)
U61^#(tt,V1,V2)	→	isBin^#(V1)	(115)
U51^#(tt,V1,V2)	→	isBin^#(V1)	(111)

1.1.5 AC Monotonic Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the naturals

[U51(x₁, x₂, x₃)]	=	2 · x₁ + 2 · x₂ + 2 · x₃
[tt]	=	0
[U52(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[isBin(x₁)]	=	2 · x₁
[U42(x₁)]	=	1 · x₁
[isBag(x₁)]	=	2 · x₁
[empty]	=	0
[and(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[1(x₁)]	=	2 · x₁
[U41(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[isBinKind(x₁)]	=	2 · x₁
[U21(x₁, x₂, x₃)]	=	1 · x₁ + 2 · x₂ + 2 · x₃
[U22(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[singl(x₁)]	=	3 · x₁
[U11(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[U82(x₁)]	=	1 · x₁
[isBagKind(x₁)]	=	2 · x₁
[U12(x₁)]	=	1 · x₁
[U31(x₁, x₂)]	=	2 + 1 · x₁ + 2 · x₂
[U32(x₁)]	=	1 · x₁
[U72(x₁)]	=	1 · x₁
[plus(x₁, x₂)]	=	2 · x₁ + 3 · x₂
[U61(x₁, x₂, x₃)]	=	1 · x₁ + 2 · x₂ + 2 · x₃
[sum(x₁)]	=	3 + 3 · x₁
[U53(x₁)]	=	1 · x₁
[U23(x₁)]	=	1 · x₁
[union(x₁, x₂)]	=	2 + 3 · x₁ + 3 · x₂
[U71(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[prod(x₁)]	=	2 + 3 · x₁
[z]	=	0
[U81(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[0(x₁)]	=	2 + 3 · x₁
[U62(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[U63(x₁)]	=	1 · x₁
[mult(x₁, x₂)]	=	3 · x₁ + 3 · x₂
[U71^#(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[isBag^#(x₁)]	=	2 · x₁
[U61^#(x₁, x₂, x₃)]	=	1 · x₁ + 2 · x₂ + 2 · x₃
[U62^#(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[U51^#(x₁, x₂, x₃)]	=	1 · x₁ + 2 · x₂ + 2 · x₃
[U52^#(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[isBin^#(x₁)]	=	2 · x₁
[U41^#(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[U21^#(x₁, x₂, x₃)]	=	1 · x₁ + 2 · x₂ + 2 · x₃
[U22^#(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[U11^#(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[U31^#(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[U81^#(x₁, x₂)]	=	1 · x₁ + 2 · x₂

together with the usable rules

U51(tt,V1,V2)	→	U52(isBin(V1),V2)	(23)
U42(tt)	→	tt	(22)
isBag(empty)	→	tt	(35)
and(tt,X)	→	X	(34)
isBin(1(V1))	→	U41(isBinKind(V1),V1)	(43)
U21(tt,V1,V2)	→	U22(isBag(V1),V2)	(16)
isBag(singl(V1))	→	U11(isBinKind(V1),V1)	(36)
U82(tt)	→	tt	(32)
isBagKind(empty)	→	tt	(38)
U41(tt,V1)	→	U42(isBin(V1))	(21)
U11(tt,V1)	→	U12(isBin(V1))	(5)
U31(tt,V1)	→	U32(isBin(V1))	(19)
U72(tt)	→	tt	(30)
isBin(plus(V1,V2))	→	U61(and(isBinKind(V1),isBinKind(V2)),V1,V2)	(45)
isBinKind(sum(V1))	→	isBagKind(V1)	(54)
U52(tt,V2)	→	U53(isBin(V2))	(24)
U23(tt)	→	tt	(18)
isBagKind(union(V1,V2))	→	and(isBagKind(V1),isBagKind(V2))	(40)
U71(tt,V1)	→	U72(isBag(V1))	(29)
isBagKind(singl(V1))	→	isBinKind(V1)	(39)
isBag(union(V1,V2))	→	U21(and(isBagKind(V1),isBagKind(V2)),V1,V2)	(37)
U22(tt,V2)	→	U23(isBag(V2))	(17)
isBinKind(prod(V1))	→	isBagKind(V1)	(53)
isBin(z)	→	tt	(41)
isBin(sum(V1))	→	U81(isBagKind(V1),V1)	(47)
U12(tt)	→	tt	(7)
isBin(0(V1))	→	U31(isBinKind(V1),V1)	(42)
isBinKind(plus(V1,V2))	→	and(isBinKind(V1),isBinKind(V2))	(52)
isBinKind(0(V1))	→	isBinKind(V1)	(49)
U32(tt)	→	tt	(20)
U61(tt,V1,V2)	→	U62(isBin(V1),V2)	(26)
U53(tt)	→	tt	(25)
U62(tt,V2)	→	U63(isBin(V2))	(27)
U81(tt,V1)	→	U82(isBag(V1))	(31)
isBinKind(1(V1))	→	isBinKind(V1)	(50)
U63(tt)	→	tt	(28)
isBin(prod(V1))	→	U71(isBagKind(V1),V1)	(46)
isBin(mult(V1,V2))	→	U51(and(isBinKind(V1),isBinKind(V2)),V1,V2)	(44)
isBinKind(z)	→	tt	(48)
isBinKind(mult(V1,V2))	→	and(isBinKind(V1),isBinKind(V2))	(51)

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

isBin^#(1(V1))	→	U41^#(isBinKind(V1),V1)	(134)
isBin^#(plus(V1,V2))	→	U61^#(and(isBinKind(V1),isBinKind(V2)),V1,V2)	(140)
isBin^#(0(V1))	→	U31^#(isBinKind(V1),V1)	(132)
isBin^#(prod(V1))	→	U71^#(isBagKind(V1),V1)	(144)
isBag^#(singl(V1))	→	U11^#(isBinKind(V1),V1)	(122)
isBag^#(union(V1,V2))	→	U21^#(and(isBagKind(V1),isBagKind(V2)),V1,V2)	(124)
isBin^#(mult(V1,V2))	→	U51^#(and(isBinKind(V1),isBinKind(V2)),V1,V2)	(136)
isBin^#(sum(V1))	→	U81^#(isBagKind(V1),V1)	(146)

and the rules

union(X,empty)	→	X	(1)
union(empty,X)	→	X	(2)
0(z)	→	z	(3)
U101(tt,X,Y)	→	0(mult(X,Y))	(4)
U111(tt,X,Y)	→	plus(0(mult(X,Y)),Y)	(6)
U121(tt,X)	→	X	(8)
U131(tt,X,Y)	→	0(plus(X,Y))	(9)
U141(tt,X,Y)	→	1(plus(X,Y))	(10)
U151(tt,X,Y)	→	0(plus(plus(X,Y),1(z)))	(11)
U161(tt,X)	→	X	(12)
U171(tt,A,B)	→	mult(prod(A),prod(B))	(13)
U181(tt,X)	→	X	(14)
U191(tt,A,B)	→	plus(sum(A),sum(B))	(15)
U31(tt,V1)	→	U32(isBin(V1))	(19)
U91(tt)	→	z	(33)
isBag(empty)	→	tt	(35)
isBag(singl(V1))	→	U11(isBinKind(V1),V1)	(36)
isBag(union(V1,V2))	→	U21(and(isBagKind(V1),isBagKind(V2)),V1,V2)	(37)
isBagKind(empty)	→	tt	(38)
isBagKind(singl(V1))	→	isBinKind(V1)	(39)
isBagKind(union(V1,V2))	→	and(isBagKind(V1),isBagKind(V2))	(40)
isBin(z)	→	tt	(41)
isBin(0(V1))	→	U31(isBinKind(V1),V1)	(42)
isBin(1(V1))	→	U41(isBinKind(V1),V1)	(43)
isBin(mult(V1,V2))	→	U51(and(isBinKind(V1),isBinKind(V2)),V1,V2)	(44)
isBin(plus(V1,V2))	→	U61(and(isBinKind(V1),isBinKind(V2)),V1,V2)	(45)
isBin(prod(V1))	→	U71(isBagKind(V1),V1)	(46)
isBin(sum(V1))	→	U81(isBagKind(V1),V1)	(47)
isBinKind(z)	→	tt	(48)
isBinKind(0(V1))	→	isBinKind(V1)	(49)
isBinKind(1(V1))	→	isBinKind(V1)	(50)
isBinKind(mult(V1,V2))	→	and(isBinKind(V1),isBinKind(V2))	(51)
isBinKind(plus(V1,V2))	→	and(isBinKind(V1),isBinKind(V2))	(52)
isBinKind(prod(V1))	→	isBagKind(V1)	(53)
isBinKind(sum(V1))	→	isBagKind(V1)	(54)
mult(z,X)	→	U91(and(isBin(X),isBinKind(X)))	(55)
mult(0(X),Y)	→	U101(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)	(56)
mult(1(X),Y)	→	U111(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)	(57)
plus(z,X)	→	U121(and(isBin(X),isBinKind(X)),X)	(58)
plus(0(X),0(Y))	→	U131(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)	(59)
plus(0(X),1(Y))	→	U141(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)	(60)
plus(1(X),1(Y))	→	U151(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)	(61)
prod(empty)	→	1(z)	(62)
prod(singl(X))	→	U161(and(isBin(X),isBinKind(X)),X)	(63)
prod(union(A,B))	→	U171(and(and(isBag(A),isBagKind(A)),and(isBag(B),isBagKind(B))),A,B)	(64)
sum(empty)	→	0(z)	(65)
sum(singl(X))	→	U181(and(isBin(X),isBinKind(X)),X)	(66)
sum(union(A,B))	→	U191(and(and(isBag(A),isBagKind(A)),and(isBag(B),isBagKind(B))),A,B)	(67)
mult(mult(z,X),ext)	→	mult(U91(and(isBin(X),isBinKind(X))),ext)	(288)
mult(mult(0(X),Y),ext)	→	mult(U101(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y),ext)	(289)
mult(mult(1(X),Y),ext)	→	mult(U111(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y),ext)	(290)
plus(plus(z,X),ext)	→	plus(U121(and(isBin(X),isBinKind(X)),X),ext)	(291)
plus(plus(0(X),0(Y)),ext)	→	plus(U131(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y),ext)	(292)
plus(plus(0(X),1(Y)),ext)	→	plus(U141(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y),ext)	(293)
plus(plus(1(X),1(Y)),ext)	→	plus(U151(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y),ext)	(294)
union(union(X,empty),ext)	→	union(X,ext)	(295)
union(union(empty,X),ext)	→	union(X,ext)	(296)

could be deleted.

1.1.5.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 6^th component contains the pair

isBinKind^#(0(V1))	→	isBinKind^#(V1)	(148)
isBinKind^#(1(V1))	→	isBinKind^#(V1)	(149)
isBinKind^#(mult(V1,V2))	→	isBinKind^#(V1)	(151)
isBinKind^#(mult(V1,V2))	→	isBinKind^#(V2)	(152)
isBinKind^#(plus(V1,V2))	→	isBinKind^#(V1)	(154)
isBinKind^#(plus(V1,V2))	→	isBinKind^#(V2)	(155)
isBinKind^#(prod(V1))	→	isBagKind^#(V1)	(156)
isBagKind^#(singl(V1))	→	isBinKind^#(V1)	(128)
isBinKind^#(sum(V1))	→	isBagKind^#(V1)	(157)
isBagKind^#(union(V1,V2))	→	isBagKind^#(V1)	(130)
isBagKind^#(union(V1,V2))	→	isBagKind^#(V2)	(131)

1.1.6 AC Monotonic Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the naturals

[isBagKind^#(x₁)]	=	1 · x₁
[union(x₁, x₂)]	=	3 · x₁ + 3 · x₂
[isBinKind^#(x₁)]	=	2 · x₁
[0(x₁)]	=	3 · x₁
[plus(x₁, x₂)]	=	3 · x₁ + 3 · x₂
[1(x₁)]	=	3 · x₁
[sum(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

isBagKind^#(union(V1,V2))	→	isBagKind^#(V1)	(130)
isBinKind^#(0(V1))	→	isBinKind^#(V1)	(148)
isBinKind^#(plus(V1,V2))	→	isBinKind^#(V2)	(155)
isBinKind^#(1(V1))	→	isBinKind^#(V1)	(149)
isBinKind^#(plus(V1,V2))	→	isBinKind^#(V1)	(154)
isBinKind^#(sum(V1))	→	isBagKind^#(V1)	(157)
isBinKind^#(mult(V1,V2))	→	isBinKind^#(V2)	(152)
isBinKind^#(prod(V1))	→	isBagKind^#(V1)	(156)
isBagKind^#(union(V1,V2))	→	isBagKind^#(V2)	(131)
isBinKind^#(mult(V1,V2))	→	isBinKind^#(V1)	(151)
isBagKind^#(singl(V1))	→	isBinKind^#(V1)	(128)

and the rules

union(X,empty)	→	X	(1)
union(empty,X)	→	X	(2)
0(z)	→	z	(3)
U101(tt,X,Y)	→	0(mult(X,Y))	(4)
U11(tt,V1)	→	U12(isBin(V1))	(5)
U111(tt,X,Y)	→	plus(0(mult(X,Y)),Y)	(6)
U12(tt)	→	tt	(7)
U121(tt,X)	→	X	(8)
U131(tt,X,Y)	→	0(plus(X,Y))	(9)
U141(tt,X,Y)	→	1(plus(X,Y))	(10)
U151(tt,X,Y)	→	0(plus(plus(X,Y),1(z)))	(11)
U161(tt,X)	→	X	(12)
U171(tt,A,B)	→	mult(prod(A),prod(B))	(13)
U181(tt,X)	→	X	(14)
U191(tt,A,B)	→	plus(sum(A),sum(B))	(15)
U21(tt,V1,V2)	→	U22(isBag(V1),V2)	(16)
U22(tt,V2)	→	U23(isBag(V2))	(17)
U23(tt)	→	tt	(18)
U31(tt,V1)	→	U32(isBin(V1))	(19)
U32(tt)	→	tt	(20)
U41(tt,V1)	→	U42(isBin(V1))	(21)
U42(tt)	→	tt	(22)
U51(tt,V1,V2)	→	U52(isBin(V1),V2)	(23)
U52(tt,V2)	→	U53(isBin(V2))	(24)
U53(tt)	→	tt	(25)
U61(tt,V1,V2)	→	U62(isBin(V1),V2)	(26)
U62(tt,V2)	→	U63(isBin(V2))	(27)
U63(tt)	→	tt	(28)
U71(tt,V1)	→	U72(isBag(V1))	(29)
U72(tt)	→	tt	(30)
U81(tt,V1)	→	U82(isBag(V1))	(31)
U82(tt)	→	tt	(32)
U91(tt)	→	z	(33)
and(tt,X)	→	X	(34)
isBag(empty)	→	tt	(35)
isBag(singl(V1))	→	U11(isBinKind(V1),V1)	(36)
isBag(union(V1,V2))	→	U21(and(isBagKind(V1),isBagKind(V2)),V1,V2)	(37)
isBagKind(empty)	→	tt	(38)
isBagKind(singl(V1))	→	isBinKind(V1)	(39)
isBagKind(union(V1,V2))	→	and(isBagKind(V1),isBagKind(V2))	(40)
isBin(z)	→	tt	(41)
isBin(0(V1))	→	U31(isBinKind(V1),V1)	(42)
isBin(1(V1))	→	U41(isBinKind(V1),V1)	(43)
isBin(mult(V1,V2))	→	U51(and(isBinKind(V1),isBinKind(V2)),V1,V2)	(44)
isBin(plus(V1,V2))	→	U61(and(isBinKind(V1),isBinKind(V2)),V1,V2)	(45)
isBin(prod(V1))	→	U71(isBagKind(V1),V1)	(46)
isBin(sum(V1))	→	U81(isBagKind(V1),V1)	(47)
isBinKind(z)	→	tt	(48)
isBinKind(0(V1))	→	isBinKind(V1)	(49)
isBinKind(1(V1))	→	isBinKind(V1)	(50)
isBinKind(mult(V1,V2))	→	and(isBinKind(V1),isBinKind(V2))	(51)
isBinKind(plus(V1,V2))	→	and(isBinKind(V1),isBinKind(V2))	(52)
isBinKind(prod(V1))	→	isBagKind(V1)	(53)
isBinKind(sum(V1))	→	isBagKind(V1)	(54)
mult(z,X)	→	U91(and(isBin(X),isBinKind(X)))	(55)
mult(0(X),Y)	→	U101(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)	(56)
mult(1(X),Y)	→	U111(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)	(57)
plus(z,X)	→	U121(and(isBin(X),isBinKind(X)),X)	(58)
plus(0(X),0(Y))	→	U131(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)	(59)
plus(0(X),1(Y))	→	U141(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)	(60)
plus(1(X),1(Y))	→	U151(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)	(61)
prod(empty)	→	1(z)	(62)
prod(singl(X))	→	U161(and(isBin(X),isBinKind(X)),X)	(63)
prod(union(A,B))	→	U171(and(and(isBag(A),isBagKind(A)),and(isBag(B),isBagKind(B))),A,B)	(64)
sum(empty)	→	0(z)	(65)
sum(singl(X))	→	U181(and(isBin(X),isBinKind(X)),X)	(66)
sum(union(A,B))	→	U191(and(and(isBag(A),isBagKind(A)),and(isBag(B),isBagKind(B))),A,B)	(67)
mult(mult(z,X),ext)	→	mult(U91(and(isBin(X),isBinKind(X))),ext)	(288)
mult(mult(0(X),Y),ext)	→	mult(U101(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y),ext)	(289)
mult(mult(1(X),Y),ext)	→	mult(U111(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y),ext)	(290)
plus(plus(z,X),ext)	→	plus(U121(and(isBin(X),isBinKind(X)),X),ext)	(291)
plus(plus(0(X),0(Y)),ext)	→	plus(U131(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y),ext)	(292)
plus(plus(0(X),1(Y)),ext)	→	plus(U141(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y),ext)	(293)
plus(plus(1(X),1(Y)),ext)	→	plus(U151(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y),ext)	(294)
union(union(X,empty),ext)	→	union(X,ext)	(295)
union(union(empty,X),ext)	→	union(X,ext)	(296)

could be deleted.

1.1.6.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 7^th component contains the pair

union^#(union(empty,X),ext)	→	union^#(X,ext)	(287)
union^#(union(X,empty),ext)	→	union^#(X,ext)	(286)
union^#(union(x,y),z')	→	union^#(y,z')	(82)
union^#(x,y)	→	union^#(y,x)	(76)
union^#(union(x,y),z')	→	union^#(x,union(y,z'))	(79)

1.1.7 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)	(295)
union(union(empty,X),ext)	→	union(X,ext)	(296)
union(union(x,y),z')	→	union(x,union(y,z'))	(73)
union(x,y)	→	union(y,x)	(70)

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

union^#(union(empty,X),ext)	→	union^#(X,ext)	(287)
union^#(union(X,empty),ext)	→	union^#(X,ext)	(286)

and the rules

union(X,empty)	→	X	(1)
union(empty,X)	→	X	(2)
0(z)	→	z	(3)
U101(tt,X,Y)	→	0(mult(X,Y))	(4)
U11(tt,V1)	→	U12(isBin(V1))	(5)
U111(tt,X,Y)	→	plus(0(mult(X,Y)),Y)	(6)
U12(tt)	→	tt	(7)
U121(tt,X)	→	X	(8)
U131(tt,X,Y)	→	0(plus(X,Y))	(9)
U141(tt,X,Y)	→	1(plus(X,Y))	(10)
U151(tt,X,Y)	→	0(plus(plus(X,Y),1(z)))	(11)
U161(tt,X)	→	X	(12)
U171(tt,A,B)	→	mult(prod(A),prod(B))	(13)
U181(tt,X)	→	X	(14)
U191(tt,A,B)	→	plus(sum(A),sum(B))	(15)
U21(tt,V1,V2)	→	U22(isBag(V1),V2)	(16)
U22(tt,V2)	→	U23(isBag(V2))	(17)
U23(tt)	→	tt	(18)
U31(tt,V1)	→	U32(isBin(V1))	(19)
U32(tt)	→	tt	(20)
U41(tt,V1)	→	U42(isBin(V1))	(21)
U42(tt)	→	tt	(22)
U51(tt,V1,V2)	→	U52(isBin(V1),V2)	(23)
U52(tt,V2)	→	U53(isBin(V2))	(24)
U53(tt)	→	tt	(25)
U61(tt,V1,V2)	→	U62(isBin(V1),V2)	(26)
U62(tt,V2)	→	U63(isBin(V2))	(27)
U63(tt)	→	tt	(28)
U71(tt,V1)	→	U72(isBag(V1))	(29)
U72(tt)	→	tt	(30)
U81(tt,V1)	→	U82(isBag(V1))	(31)
U82(tt)	→	tt	(32)
U91(tt)	→	z	(33)
and(tt,X)	→	X	(34)
isBag(empty)	→	tt	(35)
isBag(singl(V1))	→	U11(isBinKind(V1),V1)	(36)
isBag(union(V1,V2))	→	U21(and(isBagKind(V1),isBagKind(V2)),V1,V2)	(37)
isBagKind(empty)	→	tt	(38)
isBagKind(singl(V1))	→	isBinKind(V1)	(39)
isBagKind(union(V1,V2))	→	and(isBagKind(V1),isBagKind(V2))	(40)
isBin(z)	→	tt	(41)
isBin(0(V1))	→	U31(isBinKind(V1),V1)	(42)
isBin(1(V1))	→	U41(isBinKind(V1),V1)	(43)
isBin(mult(V1,V2))	→	U51(and(isBinKind(V1),isBinKind(V2)),V1,V2)	(44)
isBin(plus(V1,V2))	→	U61(and(isBinKind(V1),isBinKind(V2)),V1,V2)	(45)
isBin(prod(V1))	→	U71(isBagKind(V1),V1)	(46)
isBin(sum(V1))	→	U81(isBagKind(V1),V1)	(47)
isBinKind(z)	→	tt	(48)
isBinKind(0(V1))	→	isBinKind(V1)	(49)
isBinKind(1(V1))	→	isBinKind(V1)	(50)
isBinKind(mult(V1,V2))	→	and(isBinKind(V1),isBinKind(V2))	(51)
isBinKind(plus(V1,V2))	→	and(isBinKind(V1),isBinKind(V2))	(52)
isBinKind(prod(V1))	→	isBagKind(V1)	(53)
isBinKind(sum(V1))	→	isBagKind(V1)	(54)
mult(z,X)	→	U91(and(isBin(X),isBinKind(X)))	(55)
mult(0(X),Y)	→	U101(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)	(56)
mult(1(X),Y)	→	U111(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)	(57)
plus(z,X)	→	U121(and(isBin(X),isBinKind(X)),X)	(58)
plus(0(X),0(Y))	→	U131(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)	(59)
plus(0(X),1(Y))	→	U141(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)	(60)
plus(1(X),1(Y))	→	U151(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y)	(61)
prod(empty)	→	1(z)	(62)
prod(singl(X))	→	U161(and(isBin(X),isBinKind(X)),X)	(63)
prod(union(A,B))	→	U171(and(and(isBag(A),isBagKind(A)),and(isBag(B),isBagKind(B))),A,B)	(64)
sum(empty)	→	0(z)	(65)
sum(singl(X))	→	U181(and(isBin(X),isBinKind(X)),X)	(66)
sum(union(A,B))	→	U191(and(and(isBag(A),isBagKind(A)),and(isBag(B),isBagKind(B))),A,B)	(67)
mult(mult(z,X),ext)	→	mult(U91(and(isBin(X),isBinKind(X))),ext)	(288)
mult(mult(0(X),Y),ext)	→	mult(U101(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y),ext)	(289)
mult(mult(1(X),Y),ext)	→	mult(U111(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y),ext)	(290)
plus(plus(z,X),ext)	→	plus(U121(and(isBin(X),isBinKind(X)),X),ext)	(291)
plus(plus(0(X),0(Y)),ext)	→	plus(U131(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y),ext)	(292)
plus(plus(0(X),1(Y)),ext)	→	plus(U141(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y),ext)	(293)
plus(plus(1(X),1(Y)),ext)	→	plus(U151(and(and(isBin(X),isBinKind(X)),and(isBin(Y),isBinKind(Y))),X,Y),ext)	(294)
union(union(X,empty),ext)	→	union(X,ext)	(295)
union(union(empty,X),ext)	→	union(X,ext)	(296)

could be deleted.

1.1.7.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)	(68)
plus(x,y)	→	plus(y,x)	(69)
union(x,y)	→	union(y,x)	(70)
mult(mult(x,y),z')	→	mult(x,mult(y,z'))	(71)
plus(plus(x,y),z')	→	plus(x,plus(y,z'))	(72)
union(union(x,y),z')	→	union(x,union(y,z'))	(73)

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

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

→

union^#(y,z')

(82)

and no rules could be deleted.

1.1.7.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.