Certification Problem

Input (TPDB TRS_Equational/Mixed_AC/BAG_complete-noand)

The rewrite relation of the following equational TRS is considered.

There are 116 ruless (increase limit for explicit display).

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

The extended rules of the TRS

mult(mult(z,X),ext)	→	mult(U171(isBin(X),X),ext)	(333)
mult(mult(0(X),Y),ext)	→	mult(U181(isBin(X),X,Y),ext)	(334)
mult(mult(1(X),Y),ext)	→	mult(U191(isBin(X),X,Y),ext)	(335)
plus(plus(z,X),ext)	→	plus(U201(isBin(X),X),ext)	(336)
plus(plus(0(X),0(Y)),ext)	→	plus(U211(isBin(X),X,Y),ext)	(337)
plus(plus(0(X),1(Y)),ext)	→	plus(U221(isBin(X),X,Y),ext)	(338)
plus(plus(1(X),1(Y)),ext)	→	plus(U231(isBin(X),X,Y),ext)	(339)
union(union(X,empty),ext)	→	union(X,ext)	(340)
union(union(empty,X),ext)	→	union(X,ext)	(341)

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

U252^#(tt,A,B)	→	U253^#(isBag(B),A,B)	(203)
U253^#(tt,A,B)	→	U254^#(isBagKind(B),A,B)	(205)
U254^#(tt,A,B)	→	prod^#(A)	(208)
prod^#(union(A,B))	→	U251^#(isBag(A),A,B)	(303)
U251^#(tt,A,B)	→	U252^#(isBagKind(A),A,B)	(201)
U254^#(tt,A,B)	→	prod^#(B)	(209)

1.1.1 AC Monotonic Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the naturals

[isBin(x₁)]	=	1 · x₁
[1(x₁)]	=	3 · x₁
[U61(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[isBinKind(x₁)]	=	1 · x₁
[sum(x₁)]	=	2 + 3 · x₁
[U101(x₁, x₂)]	=	1 + 1 · x₁ + 2 · x₂
[isBagKind(x₁)]	=	1 · x₁
[mult(x₁, x₂)]	=	3 + 3 · x₁ + 3 · x₂
[U131(x₁, x₂)]	=	1 + 2 · x₁ + 2 · x₂
[U103(x₁)]	=	1 · x₁
[tt]	=	0
[isBag(x₁)]	=	1 · x₁
[empty]	=	0
[U81(x₁, x₂, x₃)]	=	2 + 1 · x₁ + 2 · x₂ + 3 · x₃
[U82(x₁, x₂, x₃)]	=	1 + 1 · x₁ + 1 · x₂ + 3 · x₃
[U25(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[U26(x₁)]	=	1 · x₁
[U71(x₁, x₂, x₃)]	=	2 + 1 · x₁ + 2 · x₂ + 3 · x₃
[U72(x₁, x₂, x₃)]	=	2 + 1 · x₁ + 1 · x₂ + 3 · x₃
[prod(x₁)]	=	2 + 3 · x₁
[U151(x₁)]	=	1 · x₁
[U74(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 1 · x₃
[U75(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[plus(x₁, x₂)]	=	2 + 3 · x₁ + 3 · x₂
[U62(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[U84(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 1 · x₃
[U85(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[U141(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[U142(x₁)]	=	1 · x₁
[U12(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[U13(x₁)]	=	1 · x₁
[U86(x₁)]	=	1 · x₁
[U24(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 1 · x₃
[U93(x₁)]	=	1 · x₁
[U111(x₁)]	=	1 · x₁
[U121(x₁)]	=	1 · x₁
[union(x₁, x₂)]	=	1 + 3 · x₁ + 3 · x₂
[U21(x₁, x₂, x₃)]	=	1 · x₁ + 2 · x₂ + 3 · x₃
[U22(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 3 · x₃
[U76(x₁)]	=	1 · x₁
[U132(x₁)]	=	1 · x₁
[U51(x₁, x₂)]	=	2 + 1 · x₁ + 2 · x₂
[U52(x₁, x₂)]	=	2 + 1 · x₁ + 1 · x₂
[z]	=	0
[U91(x₁, x₂)]	=	2 + 1 · x₁ + 2 · x₂
[U102(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[U41(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[U23(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 2 · x₃
[U42(x₁)]	=	2 · x₁
[U83(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 2 · x₃
[U92(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[singl(x₁)]	=	2 + 3 · x₁
[U11(x₁, x₂)]	=	1 + 1 · x₁ + 2 · x₂
[U73(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 2 · x₃
[U53(x₁)]	=	1 · x₁
[U31(x₁)]	=	1 · x₁
[U161(x₁)]	=	1 · x₁
[0(x₁)]	=	2 + 3 · x₁
[U63(x₁)]	=	1 · x₁
[U254^#(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 1 · x₃
[prod^#(x₁)]	=	1 · x₁
[U252^#(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 3 · x₃
[U253^#(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 2 · x₃
[U251^#(x₁, x₂, x₃)]	=	1 + 1 · x₁ + 2 · x₂ + 3 · x₃

together with the usable rules

isBin(1(V1))	→	U61(isBinKind(V1),V1)	(92)
isBin(sum(V1))	→	U101(isBagKind(V1),V1)	(96)
isBinKind(mult(V1,V2))	→	U131(isBinKind(V1),V2)	(100)
U103(tt)	→	tt	(6)
isBag(empty)	→	tt	(84)
U81(tt,V1,V2)	→	U82(isBinKind(V1),V1,V2)	(75)
U25(tt,V2)	→	U26(isBag(V2))	(48)
U71(tt,V1,V2)	→	U72(isBinKind(V1),V1,V2)	(69)
isBinKind(prod(V1))	→	U151(isBagKind(V1))	(102)
U74(tt,V1,V2)	→	U75(isBin(V1),V2)	(72)
isBin(plus(V1,V2))	→	U81(isBinKind(V1),V1,V2)	(94)
U61(tt,V1)	→	U62(isBinKind(V1),V1)	(66)
isBagKind(empty)	→	tt	(87)
U84(tt,V1,V2)	→	U85(isBin(V1),V2)	(78)
U141(tt,V2)	→	U142(isBinKind(V2))	(14)
U12(tt,V1)	→	U13(isBin(V1))	(9)
U85(tt,V2)	→	U86(isBin(V2))	(79)
U24(tt,V1,V2)	→	U25(isBag(V1),V2)	(45)
U93(tt)	→	tt	(83)
U111(tt)	→	tt	(8)
U121(tt)	→	tt	(10)
isBag(union(V1,V2))	→	U21(isBagKind(V1),V1,V2)	(86)
U21(tt,V1,V2)	→	U22(isBagKind(V1),V1,V2)	(30)
U75(tt,V2)	→	U76(isBin(V2))	(73)
U131(tt,V2)	→	U132(isBinKind(V2))	(12)
U51(tt,V1)	→	U52(isBinKind(V1),V1)	(63)
isBinKind(1(V1))	→	U121(isBinKind(V1))	(99)
isBin(z)	→	tt	(90)
U13(tt)	→	tt	(11)
isBin(mult(V1,V2))	→	U71(isBinKind(V1),V1,V2)	(93)
isBin(prod(V1))	→	U91(isBagKind(V1),V1)	(95)
U102(tt,V1)	→	U103(isBag(V1))	(5)
isBagKind(union(V1,V2))	→	U41(isBagKind(V1),V2)	(89)
U23(tt,V1,V2)	→	U24(isBagKind(V2),V1,V2)	(40)
U26(tt)	→	tt	(53)
U42(tt)	→	tt	(62)
U82(tt,V1,V2)	→	U83(isBinKind(V2),V1,V2)	(76)
U92(tt,V1)	→	U93(isBag(V1))	(82)
isBag(singl(V1))	→	U11(isBinKind(V1),V1)	(85)
U101(tt,V1)	→	U102(isBagKind(V1),V1)	(4)
U72(tt,V1,V2)	→	U73(isBinKind(V2),V1,V2)	(70)
U11(tt,V1)	→	U12(isBinKind(V1),V1)	(7)
U52(tt,V1)	→	U53(isBin(V1))	(64)
U22(tt,V1,V2)	→	U23(isBagKind(V2),V1,V2)	(35)
isBagKind(singl(V1))	→	U31(isBinKind(V1))	(88)
isBinKind(sum(V1))	→	U161(isBagKind(V1))	(103)
U31(tt)	→	tt	(60)
U41(tt,V2)	→	U42(isBagKind(V2))	(61)
U83(tt,V1,V2)	→	U84(isBinKind(V2),V1,V2)	(77)
U142(tt)	→	tt	(15)
U161(tt)	→	tt	(17)
U91(tt,V1)	→	U92(isBagKind(V1),V1)	(81)
U76(tt)	→	tt	(74)
U132(tt)	→	tt	(13)
isBinKind(0(V1))	→	U111(isBinKind(V1))	(98)
isBinKind(plus(V1,V2))	→	U141(isBinKind(V1),V2)	(101)
U86(tt)	→	tt	(80)
U53(tt)	→	tt	(65)
U62(tt,V1)	→	U63(isBin(V1))	(67)
U63(tt)	→	tt	(68)
isBin(0(V1))	→	U51(isBinKind(V1),V1)	(91)
U151(tt)	→	tt	(16)
isBinKind(z)	→	tt	(97)
U73(tt,V1,V2)	→	U74(isBinKind(V2),V1,V2)	(71)

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

prod^#(union(A,B))	→	U251^#(isBag(A),A,B)	(303)
U251^#(tt,A,B)	→	U252^#(isBagKind(A),A,B)	(201)

and the rules

union(X,empty)	→	X	(1)
union(empty,X)	→	X	(2)
0(z)	→	z	(3)
U101(tt,V1)	→	U102(isBagKind(V1),V1)	(4)
U12(tt,V1)	→	U13(isBin(V1))	(9)
U131(tt,V2)	→	U132(isBinKind(V2))	(12)
U171(tt,X)	→	U172(isBinKind(X))	(18)
U172(tt)	→	z	(19)
U181(tt,X,Y)	→	U182(isBinKind(X),X,Y)	(20)
U182(tt,X,Y)	→	U183(isBin(Y),X,Y)	(21)
U183(tt,X,Y)	→	U184(isBinKind(Y),X,Y)	(22)
U184(tt,X,Y)	→	0(mult(X,Y))	(23)
U191(tt,X,Y)	→	U192(isBinKind(X),X,Y)	(24)
U192(tt,X,Y)	→	U193(isBin(Y),X,Y)	(25)
U193(tt,X,Y)	→	U194(isBinKind(Y),X,Y)	(26)
U194(tt,X,Y)	→	plus(0(mult(X,Y)),Y)	(27)
U201(tt,X)	→	U202(isBinKind(X),X)	(28)
U202(tt,X)	→	X	(29)
U211(tt,X,Y)	→	U212(isBinKind(X),X,Y)	(31)
U212(tt,X,Y)	→	U213(isBin(Y),X,Y)	(32)
U213(tt,X,Y)	→	U214(isBinKind(Y),X,Y)	(33)
U214(tt,X,Y)	→	0(plus(X,Y))	(34)
U221(tt,X,Y)	→	U222(isBinKind(X),X,Y)	(36)
U222(tt,X,Y)	→	U223(isBin(Y),X,Y)	(37)
U223(tt,X,Y)	→	U224(isBinKind(Y),X,Y)	(38)
U224(tt,X,Y)	→	1(plus(X,Y))	(39)
U231(tt,X,Y)	→	U232(isBinKind(X),X,Y)	(41)
U232(tt,X,Y)	→	U233(isBin(Y),X,Y)	(42)
U233(tt,X,Y)	→	U234(isBinKind(Y),X,Y)	(43)
U234(tt,X,Y)	→	0(plus(plus(X,Y),1(z)))	(44)
U241(tt,X)	→	U242(isBinKind(X),X)	(46)
U242(tt,X)	→	X	(47)
U251(tt,A,B)	→	U252(isBagKind(A),A,B)	(49)
U252(tt,A,B)	→	U253(isBag(B),A,B)	(50)
U253(tt,A,B)	→	U254(isBagKind(B),A,B)	(51)
U254(tt,A,B)	→	mult(prod(A),prod(B))	(52)
U261(tt,X)	→	U262(isBinKind(X),X)	(54)
U262(tt,X)	→	X	(55)
U271(tt,A,B)	→	U272(isBagKind(A),A,B)	(56)
U272(tt,A,B)	→	U273(isBag(B),A,B)	(57)
U273(tt,A,B)	→	U274(isBagKind(B),A,B)	(58)
U274(tt,A,B)	→	plus(sum(A),sum(B))	(59)
U52(tt,V1)	→	U53(isBin(V1))	(64)
U72(tt,V1,V2)	→	U73(isBinKind(V2),V1,V2)	(70)
U81(tt,V1,V2)	→	U82(isBinKind(V1),V1,V2)	(75)
U82(tt,V1,V2)	→	U83(isBinKind(V2),V1,V2)	(76)
U91(tt,V1)	→	U92(isBagKind(V1),V1)	(81)
isBag(empty)	→	tt	(84)
isBag(singl(V1))	→	U11(isBinKind(V1),V1)	(85)
isBag(union(V1,V2))	→	U21(isBagKind(V1),V1,V2)	(86)
isBagKind(empty)	→	tt	(87)
isBagKind(singl(V1))	→	U31(isBinKind(V1))	(88)
isBagKind(union(V1,V2))	→	U41(isBagKind(V1),V2)	(89)
isBin(z)	→	tt	(90)
isBin(0(V1))	→	U51(isBinKind(V1),V1)	(91)
isBin(1(V1))	→	U61(isBinKind(V1),V1)	(92)
isBin(mult(V1,V2))	→	U71(isBinKind(V1),V1,V2)	(93)
isBin(plus(V1,V2))	→	U81(isBinKind(V1),V1,V2)	(94)
isBin(prod(V1))	→	U91(isBagKind(V1),V1)	(95)
isBin(sum(V1))	→	U101(isBagKind(V1),V1)	(96)
isBinKind(z)	→	tt	(97)
isBinKind(0(V1))	→	U111(isBinKind(V1))	(98)
isBinKind(1(V1))	→	U121(isBinKind(V1))	(99)
isBinKind(mult(V1,V2))	→	U131(isBinKind(V1),V2)	(100)
isBinKind(plus(V1,V2))	→	U141(isBinKind(V1),V2)	(101)
isBinKind(prod(V1))	→	U151(isBagKind(V1))	(102)
isBinKind(sum(V1))	→	U161(isBagKind(V1))	(103)
mult(z,X)	→	U171(isBin(X),X)	(104)
mult(0(X),Y)	→	U181(isBin(X),X,Y)	(105)
mult(1(X),Y)	→	U191(isBin(X),X,Y)	(106)
plus(z,X)	→	U201(isBin(X),X)	(107)
plus(0(X),0(Y))	→	U211(isBin(X),X,Y)	(108)
plus(0(X),1(Y))	→	U221(isBin(X),X,Y)	(109)
plus(1(X),1(Y))	→	U231(isBin(X),X,Y)	(110)
prod(empty)	→	1(z)	(111)
prod(singl(X))	→	U241(isBin(X),X)	(112)
prod(union(A,B))	→	U251(isBag(A),A,B)	(113)
sum(empty)	→	0(z)	(114)
sum(singl(X))	→	U261(isBin(X),X)	(115)
sum(union(A,B))	→	U271(isBag(A),A,B)	(116)
mult(mult(z,X),ext)	→	mult(U171(isBin(X),X),ext)	(333)
mult(mult(0(X),Y),ext)	→	mult(U181(isBin(X),X,Y),ext)	(334)
mult(mult(1(X),Y),ext)	→	mult(U191(isBin(X),X,Y),ext)	(335)
plus(plus(z,X),ext)	→	plus(U201(isBin(X),X),ext)	(336)
plus(plus(0(X),0(Y)),ext)	→	plus(U211(isBin(X),X,Y),ext)	(337)
plus(plus(0(X),1(Y)),ext)	→	plus(U221(isBin(X),X,Y),ext)	(338)
plus(plus(1(X),1(Y)),ext)	→	plus(U231(isBin(X),X,Y),ext)	(339)
union(union(X,empty),ext)	→	union(X,ext)	(340)
union(union(empty,X),ext)	→	union(X,ext)	(341)

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

U272^#(tt,A,B)	→	U273^#(isBag(B),A,B)	(214)
U273^#(tt,A,B)	→	U274^#(isBagKind(B),A,B)	(216)
U274^#(tt,A,B)	→	sum^#(A)	(219)
sum^#(union(A,B))	→	U271^#(isBag(A),A,B)	(308)
U271^#(tt,A,B)	→	U272^#(isBagKind(A),A,B)	(212)
U274^#(tt,A,B)	→	sum^#(B)	(220)

1.1.2 AC Monotonic Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the naturals

[isBin(x₁)]	=	1 · x₁
[1(x₁)]	=	3 · x₁
[U61(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[isBinKind(x₁)]	=	1 · x₁
[sum(x₁)]	=	2 + 3 · x₁
[U101(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[isBagKind(x₁)]	=	1 · x₁
[mult(x₁, x₂)]	=	1 + 3 · x₁ + 3 · x₂
[U131(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[U103(x₁)]	=	1 · x₁
[tt]	=	0
[isBag(x₁)]	=	1 · x₁
[empty]	=	0
[U81(x₁, x₂, x₃)]	=	1 · x₁ + 2 · x₂ + 3 · x₃
[U82(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 3 · x₃
[U25(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[U26(x₁)]	=	1 · x₁
[U71(x₁, x₂, x₃)]	=	1 · x₁ + 2 · x₂ + 3 · x₃
[U72(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 3 · x₃
[prod(x₁)]	=	3 + 3 · x₁
[U151(x₁)]	=	1 · x₁
[U74(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 1 · x₃
[U75(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[plus(x₁, x₂)]	=	3 · x₁ + 3 · x₂
[U62(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[U84(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 1 · x₃
[U85(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[U141(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[U142(x₁)]	=	1 · x₁
[U12(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[U13(x₁)]	=	1 · x₁
[U86(x₁)]	=	1 · x₁
[U24(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 1 · x₃
[U93(x₁)]	=	1 · x₁
[U111(x₁)]	=	1 · x₁
[U121(x₁)]	=	1 · x₁
[union(x₁, x₂)]	=	3 · x₁ + 3 · x₂
[U21(x₁, x₂, x₃)]	=	1 · x₁ + 2 · x₂ + 3 · x₃
[U22(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 3 · x₃
[U76(x₁)]	=	1 · x₁
[U132(x₁)]	=	2 · x₁
[U51(x₁, x₂)]	=	1 + 1 · x₁ + 2 · x₂
[U52(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[z]	=	0
[U91(x₁, x₂)]	=	2 + 1 · x₁ + 2 · x₂
[U102(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[U41(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[U23(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 2 · x₃
[U42(x₁)]	=	2 · x₁
[U83(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 2 · x₃
[U92(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[singl(x₁)]	=	3 · x₁
[U11(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[U73(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 2 · x₃
[U53(x₁)]	=	1 · x₁
[U31(x₁)]	=	1 · x₁
[U161(x₁)]	=	2 + 1 · x₁
[0(x₁)]	=	2 + 3 · x₁
[U63(x₁)]	=	1 · x₁
[U271^#(x₁, x₂, x₃)]	=	1 · x₁ + 2 · x₂ + 3 · x₃
[U272^#(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 3 · x₃
[U273^#(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 2 · x₃
[U274^#(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 1 · x₃
[sum^#(x₁)]	=	1 · x₁

together with the usable rules

isBin(1(V1))	→	U61(isBinKind(V1),V1)	(92)
isBin(sum(V1))	→	U101(isBagKind(V1),V1)	(96)
isBinKind(mult(V1,V2))	→	U131(isBinKind(V1),V2)	(100)
U103(tt)	→	tt	(6)
isBag(empty)	→	tt	(84)
U81(tt,V1,V2)	→	U82(isBinKind(V1),V1,V2)	(75)
U25(tt,V2)	→	U26(isBag(V2))	(48)
U71(tt,V1,V2)	→	U72(isBinKind(V1),V1,V2)	(69)
isBinKind(prod(V1))	→	U151(isBagKind(V1))	(102)
U74(tt,V1,V2)	→	U75(isBin(V1),V2)	(72)
isBin(plus(V1,V2))	→	U81(isBinKind(V1),V1,V2)	(94)
U61(tt,V1)	→	U62(isBinKind(V1),V1)	(66)
isBagKind(empty)	→	tt	(87)
U84(tt,V1,V2)	→	U85(isBin(V1),V2)	(78)
U141(tt,V2)	→	U142(isBinKind(V2))	(14)
U12(tt,V1)	→	U13(isBin(V1))	(9)
U85(tt,V2)	→	U86(isBin(V2))	(79)
U24(tt,V1,V2)	→	U25(isBag(V1),V2)	(45)
U93(tt)	→	tt	(83)
U111(tt)	→	tt	(8)
U121(tt)	→	tt	(10)
isBag(union(V1,V2))	→	U21(isBagKind(V1),V1,V2)	(86)
U21(tt,V1,V2)	→	U22(isBagKind(V1),V1,V2)	(30)
U75(tt,V2)	→	U76(isBin(V2))	(73)
U131(tt,V2)	→	U132(isBinKind(V2))	(12)
U51(tt,V1)	→	U52(isBinKind(V1),V1)	(63)
isBinKind(1(V1))	→	U121(isBinKind(V1))	(99)
isBin(z)	→	tt	(90)
U13(tt)	→	tt	(11)
isBin(mult(V1,V2))	→	U71(isBinKind(V1),V1,V2)	(93)
isBin(prod(V1))	→	U91(isBagKind(V1),V1)	(95)
U102(tt,V1)	→	U103(isBag(V1))	(5)
isBagKind(union(V1,V2))	→	U41(isBagKind(V1),V2)	(89)
U23(tt,V1,V2)	→	U24(isBagKind(V2),V1,V2)	(40)
U26(tt)	→	tt	(53)
U42(tt)	→	tt	(62)
U82(tt,V1,V2)	→	U83(isBinKind(V2),V1,V2)	(76)
U92(tt,V1)	→	U93(isBag(V1))	(82)
isBag(singl(V1))	→	U11(isBinKind(V1),V1)	(85)
U101(tt,V1)	→	U102(isBagKind(V1),V1)	(4)
U72(tt,V1,V2)	→	U73(isBinKind(V2),V1,V2)	(70)
U11(tt,V1)	→	U12(isBinKind(V1),V1)	(7)
U52(tt,V1)	→	U53(isBin(V1))	(64)
U22(tt,V1,V2)	→	U23(isBagKind(V2),V1,V2)	(35)
isBagKind(singl(V1))	→	U31(isBinKind(V1))	(88)
isBinKind(sum(V1))	→	U161(isBagKind(V1))	(103)
U31(tt)	→	tt	(60)
U41(tt,V2)	→	U42(isBagKind(V2))	(61)
U83(tt,V1,V2)	→	U84(isBinKind(V2),V1,V2)	(77)
U142(tt)	→	tt	(15)
U161(tt)	→	tt	(17)
U91(tt,V1)	→	U92(isBagKind(V1),V1)	(81)
U76(tt)	→	tt	(74)
U132(tt)	→	tt	(13)
isBinKind(0(V1))	→	U111(isBinKind(V1))	(98)
isBinKind(plus(V1,V2))	→	U141(isBinKind(V1),V2)	(101)
U86(tt)	→	tt	(80)
U53(tt)	→	tt	(65)
U62(tt,V1)	→	U63(isBin(V1))	(67)
U63(tt)	→	tt	(68)
isBin(0(V1))	→	U51(isBinKind(V1),V1)	(91)
U151(tt)	→	tt	(16)
isBinKind(z)	→	tt	(97)
U73(tt,V1,V2)	→	U74(isBinKind(V2),V1,V2)	(71)

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

sum^#(union(A,B))

→

U271^#(isBag(A),A,B)

(308)

and the rules

union(X,empty)	→	X	(1)
union(empty,X)	→	X	(2)
0(z)	→	z	(3)
U161(tt)	→	tt	(17)
U171(tt,X)	→	U172(isBinKind(X))	(18)
U172(tt)	→	z	(19)
U181(tt,X,Y)	→	U182(isBinKind(X),X,Y)	(20)
U182(tt,X,Y)	→	U183(isBin(Y),X,Y)	(21)
U183(tt,X,Y)	→	U184(isBinKind(Y),X,Y)	(22)
U184(tt,X,Y)	→	0(mult(X,Y))	(23)
U191(tt,X,Y)	→	U192(isBinKind(X),X,Y)	(24)
U192(tt,X,Y)	→	U193(isBin(Y),X,Y)	(25)
U193(tt,X,Y)	→	U194(isBinKind(Y),X,Y)	(26)
U194(tt,X,Y)	→	plus(0(mult(X,Y)),Y)	(27)
U201(tt,X)	→	U202(isBinKind(X),X)	(28)
U202(tt,X)	→	X	(29)
U211(tt,X,Y)	→	U212(isBinKind(X),X,Y)	(31)
U212(tt,X,Y)	→	U213(isBin(Y),X,Y)	(32)
U213(tt,X,Y)	→	U214(isBinKind(Y),X,Y)	(33)
U214(tt,X,Y)	→	0(plus(X,Y))	(34)
U221(tt,X,Y)	→	U222(isBinKind(X),X,Y)	(36)
U222(tt,X,Y)	→	U223(isBin(Y),X,Y)	(37)
U223(tt,X,Y)	→	U224(isBinKind(Y),X,Y)	(38)
U224(tt,X,Y)	→	1(plus(X,Y))	(39)
U231(tt,X,Y)	→	U232(isBinKind(X),X,Y)	(41)
U232(tt,X,Y)	→	U233(isBin(Y),X,Y)	(42)
U233(tt,X,Y)	→	U234(isBinKind(Y),X,Y)	(43)
U234(tt,X,Y)	→	0(plus(plus(X,Y),1(z)))	(44)
U241(tt,X)	→	U242(isBinKind(X),X)	(46)
U242(tt,X)	→	X	(47)
U251(tt,A,B)	→	U252(isBagKind(A),A,B)	(49)
U252(tt,A,B)	→	U253(isBag(B),A,B)	(50)
U253(tt,A,B)	→	U254(isBagKind(B),A,B)	(51)
U254(tt,A,B)	→	mult(prod(A),prod(B))	(52)
U261(tt,X)	→	U262(isBinKind(X),X)	(54)
U262(tt,X)	→	X	(55)
U271(tt,A,B)	→	U272(isBagKind(A),A,B)	(56)
U272(tt,A,B)	→	U273(isBag(B),A,B)	(57)
U273(tt,A,B)	→	U274(isBagKind(B),A,B)	(58)
U274(tt,A,B)	→	plus(sum(A),sum(B))	(59)
U52(tt,V1)	→	U53(isBin(V1))	(64)
U91(tt,V1)	→	U92(isBagKind(V1),V1)	(81)
isBag(empty)	→	tt	(84)
isBag(singl(V1))	→	U11(isBinKind(V1),V1)	(85)
isBag(union(V1,V2))	→	U21(isBagKind(V1),V1,V2)	(86)
isBagKind(empty)	→	tt	(87)
isBagKind(singl(V1))	→	U31(isBinKind(V1))	(88)
isBagKind(union(V1,V2))	→	U41(isBagKind(V1),V2)	(89)
isBin(z)	→	tt	(90)
isBin(0(V1))	→	U51(isBinKind(V1),V1)	(91)
isBin(1(V1))	→	U61(isBinKind(V1),V1)	(92)
isBin(mult(V1,V2))	→	U71(isBinKind(V1),V1,V2)	(93)
isBin(plus(V1,V2))	→	U81(isBinKind(V1),V1,V2)	(94)
isBin(prod(V1))	→	U91(isBagKind(V1),V1)	(95)
isBin(sum(V1))	→	U101(isBagKind(V1),V1)	(96)
isBinKind(z)	→	tt	(97)
isBinKind(0(V1))	→	U111(isBinKind(V1))	(98)
isBinKind(1(V1))	→	U121(isBinKind(V1))	(99)
isBinKind(mult(V1,V2))	→	U131(isBinKind(V1),V2)	(100)
isBinKind(plus(V1,V2))	→	U141(isBinKind(V1),V2)	(101)
isBinKind(prod(V1))	→	U151(isBagKind(V1))	(102)
isBinKind(sum(V1))	→	U161(isBagKind(V1))	(103)
mult(z,X)	→	U171(isBin(X),X)	(104)
mult(0(X),Y)	→	U181(isBin(X),X,Y)	(105)
mult(1(X),Y)	→	U191(isBin(X),X,Y)	(106)
plus(z,X)	→	U201(isBin(X),X)	(107)
plus(0(X),0(Y))	→	U211(isBin(X),X,Y)	(108)
plus(0(X),1(Y))	→	U221(isBin(X),X,Y)	(109)
plus(1(X),1(Y))	→	U231(isBin(X),X,Y)	(110)
prod(empty)	→	1(z)	(111)
prod(singl(X))	→	U241(isBin(X),X)	(112)
prod(union(A,B))	→	U251(isBag(A),A,B)	(113)
sum(empty)	→	0(z)	(114)
sum(singl(X))	→	U261(isBin(X),X)	(115)
sum(union(A,B))	→	U271(isBag(A),A,B)	(116)
mult(mult(z,X),ext)	→	mult(U171(isBin(X),X),ext)	(333)
mult(mult(0(X),Y),ext)	→	mult(U181(isBin(X),X,Y),ext)	(334)
mult(mult(1(X),Y),ext)	→	mult(U191(isBin(X),X,Y),ext)	(335)
plus(plus(z,X),ext)	→	plus(U201(isBin(X),X),ext)	(336)
plus(plus(0(X),0(Y)),ext)	→	plus(U211(isBin(X),X,Y),ext)	(337)
plus(plus(0(X),1(Y)),ext)	→	plus(U221(isBin(X),X,Y),ext)	(338)
plus(plus(1(X),1(Y)),ext)	→	plus(U231(isBin(X),X,Y),ext)	(339)
union(union(X,empty),ext)	→	union(X,ext)	(340)
union(union(empty,X),ext)	→	union(X,ext)	(341)

could be deleted.

1.1.2.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 3^rd component contains the pair

U182^#(tt,X,Y)	→	U183^#(isBin(Y),X,Y)	(148)
U183^#(tt,X,Y)	→	U184^#(isBinKind(Y),X,Y)	(150)
U184^#(tt,X,Y)	→	mult^#(X,Y)	(153)
mult^#(0(X),Y)	→	U181^#(isBin(X),X,Y)	(289)
U181^#(tt,X,Y)	→	U182^#(isBinKind(X),X,Y)	(146)
mult^#(1(X),Y)	→	U191^#(isBin(X),X,Y)	(291)
U191^#(tt,X,Y)	→	U192^#(isBinKind(X),X,Y)	(154)
U192^#(tt,X,Y)	→	U193^#(isBin(Y),X,Y)	(156)
U193^#(tt,X,Y)	→	U194^#(isBinKind(Y),X,Y)	(158)
U194^#(tt,X,Y)	→	mult^#(X,Y)	(162)
mult^#(mult(z,X),ext)	→	mult^#(U171(isBin(X),X),ext)	(310)
mult^#(mult(0(X),Y),ext)	→	mult^#(U181(isBin(X),X,Y),ext)	(313)
mult^#(mult(0(X),Y),ext)	→	U181^#(isBin(X),X,Y)	(314)
mult^#(mult(1(X),Y),ext)	→	mult^#(U191(isBin(X),X,Y),ext)	(316)
mult^#(mult(1(X),Y),ext)	→	U191^#(isBin(X),X,Y)	(317)
mult^#(mult(x,y),z')	→	mult^#(y,z')	(129)
mult^#(x,y)	→	mult^#(y,x)	(123)
mult^#(mult(x,y),z')	→	mult^#(x,mult(y,z'))	(126)

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₂
[U184^#(x₁, x₂, x₃)]	=	1 · x₃ + 1 · x₂ + 1 · x₁ · x₂ · x₃
[tt]	=	1
[0(x₁)]	=	1 · x₁
[U181(x₁, x₂, x₃)]	=	1 · x₃ + 1 · x₂ + 1 · x₁ · x₂ · x₃
[isBin(x₁)]	=	1
[U193^#(x₁, x₂, x₃)]	=	1 · x₃ + 1 · x₂ + 1 · x₂ · x₃
[U194^#(x₁, x₂, x₃)]	=	1 · x₃ + 1 · x₂ + 1 · x₂ · x₃
[isBinKind(x₁)]	=	1
[1(x₁)]	=	1 + 1 · x₁
[U191^#(x₁, x₂, x₃)]	=	1 + 1 · x₃ + 1 · x₂ · x₃ + 1 · x₁ · x₂
[U192^#(x₁, x₂, x₃)]	=	1 + 1 · x₃ + 1 · x₁ · x₂ + 1 · x₁ · x₂ · x₃
[z]	=	0
[U171(x₁, x₂)]	=	0
[U181^#(x₁, x₂, x₃)]	=	1 · x₃ + 1 · x₂ · x₃ + 1 · x₁ · x₂
[U182^#(x₁, x₂, x₃)]	=	1 · x₃ + 1 · x₂ · x₃ + 1 · x₁ · x₂
[U183^#(x₁, x₂, x₃)]	=	1 · x₃ + 1 · x₂ + 1 · x₁ · x₂ · x₃
[U191(x₁, x₂, x₃)]	=	1 · x₃ + 1 · x₂ + 1 · x₂ · x₃ + 1 · x₁ · x₃
[U193(x₁, x₂, x₃)]	=	1 · x₃ + 1 · x₂ · x₃ + 1 · x₁ · x₃ + 1 · x₁ · x₂
[U194(x₁, x₂, x₃)]	=	1 · x₃ + 1 · x₂ + 1 · x₂ · x₃ + 1 · x₁ · x₃
[U232(x₁, x₂, x₃)]	=	1 + 1 · x₂ + 1 · x₁ + 1 · x₁ · x₃
[U233(x₁, x₂, x₃)]	=	1 + 1 · x₃ + 1 · x₂ + 1 · x₁
[U86(x₁)]	=	1 · x₁ · x₁
[U92(x₁, x₂)]	=	1
[U93(x₁)]	=	1
[isBag(x₁)]	=	1 · x₁
[U72(x₁, x₂, x₃)]	=	1
[U73(x₁, x₂, x₃)]	=	1
[U61(x₁, x₂)]	=	1
[U71(x₁, x₂, x₃)]	=	1
[prod(x₁)]	=	0
[U91(x₁, x₂)]	=	1
[isBagKind(x₁)]	=	1 · x₁ · x₁
[U51(x₁, x₂)]	=	1
[sum(x₁)]	=	0
[U101(x₁, x₂)]	=	1
[plus(x₁, x₂)]	=	1 · x₂ + 1 · x₁
[U81(x₁, x₂, x₃)]	=	1
[U231(x₁, x₂, x₃)]	=	1 + 1 · x₃ + 1 · x₂ + 1 · x₁
[U75(x₁, x₂)]	=	1
[U76(x₁)]	=	1 · x₁ · x₁
[U13(x₁)]	=	1 · x₁ · x₁
[U161(x₁)]	=	1
[U131(x₁, x₂)]	=	1 · x₁
[U151(x₁)]	=	1
[U121(x₁)]	=	1 · x₁ · x₁
[U111(x₁)]	=	1
[U141(x₁, x₂)]	=	1
[U74(x₁, x₂, x₃)]	=	1
[U103(x₁)]	=	1
[U53(x₁)]	=	1 · x₁ · x₁
[U41(x₁, x₂)]	=	1 · x₁
[U42(x₁)]	=	1
[U132(x₁)]	=	1 · x₁ · x₁
[U142(x₁)]	=	1 · x₁
[U102(x₁, x₂)]	=	1
[U172(x₁)]	=	0
[U224(x₁, x₂, x₃)]	=	1 + 1 · x₃ + 1 · x₂
[U26(x₁)]	=	1
[U31(x₁)]	=	1
[U182(x₁, x₂, x₃)]	=	1 · x₃ + 1 · x₂ + 1 · x₂ · x₃
[U234(x₁, x₂, x₃)]	=	1 + 1 · x₃ + 1 · x₂ + 1 · x₁
[U201(x₁, x₂)]	=	1 · x₂
[U202(x₁, x₂)]	=	1 · x₂
[U183(x₁, x₂, x₃)]	=	1 · x₃ + 1 · x₂ + 1 · x₁ · x₂ · x₃
[U214(x₁, x₂, x₃)]	=	1 · x₃ + 1 · x₂
[singl(x₁)]	=	1
[U11(x₁, x₂)]	=	1
[empty]	=	1
[union(x₁, x₂)]	=	1 · x₁
[U21(x₁, x₂, x₃)]	=	1 · x₂
[U25(x₁, x₂)]	=	1 · x₁
[U62(x₁, x₂)]	=	1
[U63(x₁)]	=	1
[U221(x₁, x₂, x₃)]	=	1 + 1 · x₃ + 1 · x₁ · x₂
[U222(x₁, x₂, x₃)]	=	1 + 1 · x₁ · x₃ + 1 · x₁ · x₂
[U223(x₁, x₂, x₃)]	=	1 + 1 · x₃ + 1 · x₂
[U211(x₁, x₂, x₃)]	=	1 · x₃ + 1 · x₂
[U12(x₁, x₂)]	=	1
[U85(x₁, x₂)]	=	1
[U184(x₁, x₂, x₃)]	=	1 · x₃ + 1 · x₂ + 1 · x₁ · x₂ · x₃
[U83(x₁, x₂, x₃)]	=	1
[U84(x₁, x₂, x₃)]	=	1
[U24(x₁, x₂, x₃)]	=	1 · x₂
[U82(x₁, x₂, x₃)]	=	1
[U52(x₁, x₂)]	=	1
[U192(x₁, x₂, x₃)]	=	1 · x₃ + 1 · x₂ + 1 · x₂ · x₃ + 1 · x₁ · x₃
[U23(x₁, x₂, x₃)]	=	1 · x₂
[U212(x₁, x₂, x₃)]	=	1 · x₃ + 1 · x₁ · x₂
[U213(x₁, x₂, x₃)]	=	1 · x₃ + 1 · x₂
[U22(x₁, x₂, x₃)]	=	1 · x₂

together with the usable rules

There are 107 ruless (increase limit for explicit display).

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

mult^#(mult(1(X),Y),ext)	→	mult^#(U191(isBin(X),X,Y),ext)	(316)
U192^#(tt,X,Y)	→	U193^#(isBin(Y),X,Y)	(156)

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)	→	U181^#(isBin(X),X,Y)	(289)
U181^#(tt,X,Y)	→	U182^#(isBinKind(X),X,Y)	(146)
U182^#(tt,X,Y)	→	U183^#(isBin(Y),X,Y)	(148)
U183^#(tt,X,Y)	→	U184^#(isBinKind(Y),X,Y)	(150)
U184^#(tt,X,Y)	→	mult^#(X,Y)	(153)
mult^#(mult(z,X),ext)	→	mult^#(U171(isBin(X),X),ext)	(310)
mult^#(mult(0(X),Y),ext)	→	mult^#(U181(isBin(X),X,Y),ext)	(313)
mult^#(mult(0(X),Y),ext)	→	U181^#(isBin(X),X,Y)	(314)
mult^#(mult(x,y),z')	→	mult^#(y,z')	(129)
mult^#(x,y)	→	mult^#(y,x)	(123)
mult^#(mult(x,y),z')	→	mult^#(x,mult(y,z'))	(126)

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₂
[U184^#(x₁, x₂, x₃)]	=	1 · x₃ + 1 · x₂ + 1 · x₁ · x₂ · x₃
[tt]	=	1
[z]	=	0
[U171(x₁, x₂)]	=	0
[isBin(x₁)]	=	1
[0(x₁)]	=	1 + 1 · x₁
[U181(x₁, x₂, x₃)]	=	1 + 1 · x₃ + 1 · x₂ + 1 · x₂ · x₃
[U181^#(x₁, x₂, x₃)]	=	1 · x₃ + 1 · x₂ · x₃ + 1 · x₁ · x₂
[U182^#(x₁, x₂, x₃)]	=	1 · x₃ + 1 · x₁ · x₂ + 1 · x₁ · x₂ · x₃
[U183^#(x₁, x₂, x₃)]	=	1 · x₃ + 1 · x₂ + 1 · x₂ · x₃
[isBinKind(x₁)]	=	1
[1(x₁)]	=	1 + 1 · x₁
[U191(x₁, x₂, x₃)]	=	1 + 1 · x₃ + 1 · x₂ + 1 · x₂ · x₃ + 1 · x₁ · x₃
[U24(x₁, x₂, x₃)]	=	1 + 1 · x₂
[U25(x₁, x₂)]	=	1 · x₁
[isBag(x₁)]	=	1 + 1 · x₁
[U213(x₁, x₂, x₃)]	=	1 + 1 · x₂ + 1 · x₁ · x₃
[U214(x₁, x₂, x₃)]	=	1 + 1 · x₃ + 1 · x₂
[U182(x₁, x₂, x₃)]	=	1 · x₃ + 1 · x₁ + 1 · x₂ · x₃ + 1 · x₁ · x₂
[U201(x₁, x₂)]	=	1 · x₂
[U202(x₁, x₂)]	=	1 · x₁ · x₂
[U83(x₁, x₂, x₃)]	=	1
[U84(x₁, x₂, x₃)]	=	1
[U183(x₁, x₂, x₃)]	=	1 + 1 · x₃ + 1 · x₁ · x₂ + 1 · x₁ · x₂ · x₃
[U184(x₁, x₂, x₃)]	=	1 + 1 · x₂ · x₃ + 1 · x₁ · x₃ + 1 · x₁ · x₂
[U81(x₁, x₂, x₃)]	=	1
[U82(x₁, x₂, x₃)]	=	1
[U74(x₁, x₂, x₃)]	=	1 · x₁
[U75(x₁, x₂)]	=	1 · x₁
[U53(x₁)]	=	1 · x₁ · x₁
[U11(x₁, x₂)]	=	1 + 1 · x₁
[U12(x₁, x₂)]	=	1 + 1 · x₁
[U76(x₁)]	=	1 · x₁
[sum(x₁)]	=	0
[U161(x₁)]	=	1
[isBagKind(x₁)]	=	1
[U131(x₁, x₂)]	=	1 · x₁
[prod(x₁)]	=	0
[U151(x₁)]	=	1
[U121(x₁)]	=	1 · x₁ · x₁
[U111(x₁)]	=	1
[plus(x₁, x₂)]	=	1 · x₂ + 1 · x₁
[U141(x₁, x₂)]	=	1
[singl(x₁)]	=	1
[empty]	=	1
[union(x₁, x₂)]	=	1 · x₁
[U21(x₁, x₂, x₃)]	=	1 + 1 · x₂
[U51(x₁, x₂)]	=	1
[U52(x₁, x₂)]	=	1
[U72(x₁, x₂, x₃)]	=	1
[U73(x₁, x₂, x₃)]	=	1 · x₁
[U221(x₁, x₂, x₃)]	=	1 + 1 · x₃ + 1 · x₂ + 1 · x₁
[U222(x₁, x₂, x₃)]	=	1 + 1 · x₃ + 1 · x₂ + 1 · x₁
[U92(x₁, x₂)]	=	1
[U93(x₁)]	=	1
[U223(x₁, x₂, x₃)]	=	1 + 1 · x₃ + 1 · x₁ + 1 · x₁ · x₂
[U224(x₁, x₂, x₃)]	=	1 + 1 · x₃ + 1 · x₂
[U23(x₁, x₂, x₃)]	=	1 + 1 · x₂
[U61(x₁, x₂)]	=	1 · x₁
[U71(x₁, x₂, x₃)]	=	1 · x₁
[U91(x₁, x₂)]	=	1 · x₁
[U101(x₁, x₂)]	=	1
[U85(x₁, x₂)]	=	1 · x₁
[U86(x₁)]	=	1
[U42(x₁)]	=	1
[U192(x₁, x₂, x₃)]	=	1 + 1 · x₃ + 1 · x₂ + 1 · x₂ · x₃ + 1 · x₁ · x₃
[U193(x₁, x₂, x₃)]	=	1 + 1 · x₃ + 1 · x₂ + 1 · x₂ · x₃ + 1 · x₁ · x₃
[U232(x₁, x₂, x₃)]	=	1 + 1 · x₃ + 1 · x₂ + 1 · x₁
[U233(x₁, x₂, x₃)]	=	1 + 1 · x₂ + 1 · x₁ + 1 · x₁ · x₃
[U103(x₁)]	=	1
[U62(x₁, x₂)]	=	1
[U63(x₁)]	=	1
[U172(x₁)]	=	0
[U13(x₁)]	=	1
[U194(x₁, x₂, x₃)]	=	1 · x₃ + 1 · x₁ + 1 · x₁ · x₃ + 1 · x₁ · x₂ + 1 · x₁ · x₂ · x₃
[U142(x₁)]	=	1 · x₁ · x₁
[U211(x₁, x₂, x₃)]	=	1 + 1 · x₂ + 1 · x₁ · x₃
[U212(x₁, x₂, x₃)]	=	1 · x₃ + 1 · x₂ + 1 · x₁
[U26(x₁)]	=	1
[U31(x₁)]	=	1
[U22(x₁, x₂, x₃)]	=	1 · x₂ + 1 · x₁
[U234(x₁, x₂, x₃)]	=	1 + 1 · x₃ + 1 · x₂ + 1 · x₁
[U102(x₁, x₂)]	=	1
[U231(x₁, x₂, x₃)]	=	1 + 1 · x₃ + 1 · x₂ + 1 · x₁
[U41(x₁, x₂)]	=	1 · x₁
[U132(x₁)]	=	1 · x₁

together with the usable rules

There are 107 ruless (increase limit for explicit display).

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

mult^#(mult(0(X),Y),ext)	→	U181^#(isBin(X),X,Y)	(314)
mult^#(0(X),Y)	→	U181^#(isBin(X),X,Y)	(289)

could be deleted.

1.1.3.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^#(U171(isBin(X),X),ext)	(310)
mult^#(mult(0(X),Y),ext)	→	mult^#(U181(isBin(X),X,Y),ext)	(313)
mult^#(mult(x,y),z')	→	mult^#(y,z')	(129)
mult^#(x,y)	→	mult^#(y,x)	(123)
mult^#(mult(x,y),z')	→	mult^#(x,mult(y,z'))	(126)

1.1.3.1.1.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₂)]	=	1 + 1 · x₁ + 1 · x₂
[z]	=	0
[U171(x₁, x₂)]	=	1 + 1 · x₂
[isBin(x₁)]	=	0
[0(x₁)]	=	3
[U181(x₁, x₂, x₃)]	=	3
[U172(x₁)]	=	0
[tt]	=	0
[U132(x₁)]	=	3
[U81(x₁, x₂, x₃)]	=	3 + 3 · x₂ + 3 · x₃
[U82(x₁, x₂, x₃)]	=	3 + 3 · x₂ + 3 · x₃
[isBinKind(x₁)]	=	0
[U221(x₁, x₂, x₃)]	=	3
[U222(x₁, x₂, x₃)]	=	3
[U51(x₁, x₂)]	=	3 + 3 · x₂
[U52(x₁, x₂)]	=	3 + 3 · x₂
[U194(x₁, x₂, x₃)]	=	3 + 1 · x₃
[plus(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[isBagKind(x₁)]	=	0
[empty]	=	0
[singl(x₁)]	=	0
[U31(x₁)]	=	3
[union(x₁, x₂)]	=	0
[U41(x₁, x₂)]	=	3 + 3 · x₂
[U63(x₁)]	=	3
[U101(x₁, x₂)]	=	3 + 3 · x₂
[U102(x₁, x₂)]	=	3 + 3 · x₂
[U91(x₁, x₂)]	=	3 + 3 · x₂
[U92(x₁, x₂)]	=	3 + 3 · x₂
[U121(x₁)]	=	3
[U93(x₁)]	=	3
[U232(x₁, x₂, x₃)]	=	3
[U233(x₁, x₂, x₃)]	=	3
[U21(x₁, x₂, x₃)]	=	3 + 3 · x₂ + 3 · x₃
[U22(x₁, x₂, x₃)]	=	3 + 3 · x₂ + 3 · x₃
[U201(x₁, x₂)]	=	1 · x₂
[U202(x₁, x₂)]	=	1 · x₂
[U151(x₁)]	=	3
[U224(x₁, x₂, x₃)]	=	2
[1(x₁)]	=	2
[U74(x₁, x₂, x₃)]	=	3 + 3 · x₂ + 3 · x₃
[U75(x₁, x₂)]	=	3 + 3 · x₂
[U71(x₁, x₂, x₃)]	=	3 + 3 · x₂ + 3 · x₃
[U72(x₁, x₂, x₃)]	=	3 + 3 · x₂ + 3 · x₃
[U83(x₁, x₂, x₃)]	=	3 + 3 · x₂ + 3 · x₃
[U84(x₁, x₂, x₃)]	=	3 + 3 · x₂ + 3 · x₃
[U73(x₁, x₂, x₃)]	=	3 + 3 · x₂ + 3 · x₃
[U131(x₁, x₂)]	=	3 + 3 · x₂
[U13(x₁)]	=	3
[U193(x₁, x₂, x₃)]	=	3 + 1 · x₃
[U191(x₁, x₂, x₃)]	=	3 + 1 · x₃
[U223(x₁, x₂, x₃)]	=	3
[U12(x₁, x₂)]	=	3 + 3 · x₂
[U182(x₁, x₂, x₃)]	=	3
[U183(x₁, x₂, x₃)]	=	3
[U184(x₁, x₂, x₃)]	=	3
[U111(x₁)]	=	3
[U25(x₁, x₂)]	=	3 + 3 · x₂
[U26(x₁)]	=	3
[isBag(x₁)]	=	0
[U234(x₁, x₂, x₃)]	=	3
[U24(x₁, x₂, x₃)]	=	3 + 3 · x₂ + 3 · x₃
[U192(x₁, x₂, x₃)]	=	3 + 1 · x₃
[sum(x₁)]	=	0
[U161(x₁)]	=	3
[prod(x₁)]	=	0
[U141(x₁, x₂)]	=	3 + 3 · x₂
[U85(x₁, x₂)]	=	3 + 3 · x₂
[U86(x₁)]	=	3
[U211(x₁, x₂, x₃)]	=	3
[U231(x₁, x₂, x₃)]	=	3
[U53(x₁)]	=	3
[U142(x₁)]	=	3
[U11(x₁, x₂)]	=	3 + 3 · x₂
[U214(x₁, x₂, x₃)]	=	3
[U103(x₁)]	=	3
[U23(x₁, x₂, x₃)]	=	3 + 3 · x₂ + 3 · x₃
[U61(x₁, x₂)]	=	3 + 3 · x₂
[U62(x₁, x₂)]	=	3 + 3 · x₂
[U212(x₁, x₂, x₃)]	=	3
[U213(x₁, x₂, x₃)]	=	3
[U76(x₁)]	=	3
[U42(x₁)]	=	3

together with the usable rules

U172(tt)	→	z	(19)
0(z)	→	z	(3)
U221(tt,X,Y)	→	U222(isBinKind(X),X,Y)	(36)
U194(tt,X,Y)	→	plus(0(mult(X,Y)),Y)	(27)
U171(tt,X)	→	U172(isBinKind(X))	(18)
U232(tt,X,Y)	→	U233(isBin(Y),X,Y)	(42)
U201(tt,X)	→	U202(isBinKind(X),X)	(28)
U224(tt,X,Y)	→	1(plus(X,Y))	(39)
U193(tt,X,Y)	→	U194(isBinKind(Y),X,Y)	(26)
mult(0(X),Y)	→	U181(isBin(X),X,Y)	(105)
mult(z,X)	→	U171(isBin(X),X)	(104)
mult(mult(1(X),Y),ext)	→	mult(U191(isBin(X),X,Y),ext)	(335)
mult(1(X),Y)	→	U191(isBin(X),X,Y)	(106)
mult(mult(z,X),ext)	→	mult(U171(isBin(X),X),ext)	(333)
mult(mult(0(X),Y),ext)	→	mult(U181(isBin(X),X,Y),ext)	(334)
U223(tt,X,Y)	→	U224(isBinKind(Y),X,Y)	(38)
U222(tt,X,Y)	→	U223(isBin(Y),X,Y)	(37)
U182(tt,X,Y)	→	U183(isBin(Y),X,Y)	(21)
U183(tt,X,Y)	→	U184(isBinKind(Y),X,Y)	(22)
U184(tt,X,Y)	→	0(mult(X,Y))	(23)
U234(tt,X,Y)	→	0(plus(plus(X,Y),1(z)))	(44)
U233(tt,X,Y)	→	U234(isBinKind(Y),X,Y)	(43)
U191(tt,X,Y)	→	U192(isBinKind(X),X,Y)	(24)
U192(tt,X,Y)	→	U193(isBin(Y),X,Y)	(25)
plus(0(X),1(Y))	→	U221(isBin(X),X,Y)	(109)
plus(plus(0(X),0(Y)),ext)	→	plus(U211(isBin(X),X,Y),ext)	(337)
plus(plus(0(X),1(Y)),ext)	→	plus(U221(isBin(X),X,Y),ext)	(338)
plus(1(X),1(Y))	→	U231(isBin(X),X,Y)	(110)
plus(z,X)	→	U201(isBin(X),X)	(107)
plus(plus(1(X),1(Y)),ext)	→	plus(U231(isBin(X),X,Y),ext)	(339)
plus(0(X),0(Y))	→	U211(isBin(X),X,Y)	(108)
plus(plus(z,X),ext)	→	plus(U201(isBin(X),X),ext)	(336)
U214(tt,X,Y)	→	0(plus(X,Y))	(34)
U231(tt,X,Y)	→	U232(isBinKind(X),X,Y)	(41)
U202(tt,X)	→	X	(29)
U211(tt,X,Y)	→	U212(isBinKind(X),X,Y)	(31)
U213(tt,X,Y)	→	U214(isBinKind(Y),X,Y)	(33)
U181(tt,X,Y)	→	U182(isBinKind(X),X,Y)	(20)
U212(tt,X,Y)	→	U213(isBin(Y),X,Y)	(32)
mult(x,y)	→	mult(y,x)	(117)
mult(mult(x,y),z')	→	mult(x,mult(y,z'))	(120)
plus(plus(x,y),z')	→	plus(x,plus(y,z'))	(121)
plus(x,y)	→	plus(y,x)	(118)

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

mult^#(mult(x,y),z')	→	mult^#(y,z')	(129)
mult^#(mult(0(X),Y),ext)	→	mult^#(U181(isBin(X),X,Y),ext)	(313)

could be deleted.

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₂)]	=	1 · x₁ + 1 · x₂
[mult(x₁, x₂)]	=	2 + 1 · x₁ + 1 · x₂
[z]	=	0
[U171(x₁, x₂)]	=	1 · x₂
[isBin(x₁)]	=	2 + 3 · x₁
[U52(x₁, x₂)]	=	2 · x₁
[tt]	=	2
[U53(x₁)]	=	2
[U151(x₁)]	=	3
[U121(x₁)]	=	3
[U142(x₁)]	=	3
[U92(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[U93(x₁)]	=	2 + 1 · x₁
[isBag(x₁)]	=	2 · x₁
[U182(x₁, x₂, x₃)]	=	1
[U183(x₁, x₂, x₃)]	=	0
[U141(x₁, x₂)]	=	3 + 3 · x₂
[isBinKind(x₁)]	=	0
[U102(x₁, x₂)]	=	2 · x₂
[U103(x₁)]	=	1 · x₁
[U85(x₁, x₂)]	=	3 + 1 · x₁ + 3 · x₂
[U86(x₁)]	=	2 + 1 · x₁
[U213(x₁, x₂, x₃)]	=	0
[U214(x₁, x₂, x₃)]	=	0
[U51(x₁, x₂)]	=	2 + 2 · x₁
[U73(x₁, x₂, x₃)]	=	1 · x₁ + 3 · x₂ + 3 · x₃
[U74(x₁, x₂, x₃)]	=	3 · x₁ + 3 · x₂ + 3 · x₃
[U211(x₁, x₂, x₃)]	=	0
[U212(x₁, x₂, x₃)]	=	0
[U222(x₁, x₂, x₃)]	=	0
[U223(x₁, x₂, x₃)]	=	0
[U234(x₁, x₂, x₃)]	=	0
[0(x₁)]	=	0
[plus(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[1(x₁)]	=	0
[U91(x₁, x₂)]	=	2 + 3 · x₁ + 2 · x₂
[isBagKind(x₁)]	=	2
[U194(x₁, x₂, x₃)]	=	1 · x₃
[U76(x₁)]	=	2 + 1 · x₁
[U161(x₁)]	=	3
[U24(x₁, x₂, x₃)]	=	1 + 2 · x₃
[U25(x₁, x₂)]	=	1 + 2 · x₂
[U81(x₁, x₂, x₃)]	=	2 + 3 · x₁ + 3 · x₂ + 3 · x₃
[U82(x₁, x₂, x₃)]	=	2 + 2 · x₁ + 3 · x₂ + 3 · x₃
[U63(x₁)]	=	2
[U111(x₁)]	=	3
[U41(x₁, x₂)]	=	3 + 3 · x₂
[U42(x₁)]	=	3
[U181(x₁, x₂, x₃)]	=	1
[U61(x₁, x₂)]	=	2 · x₁
[U62(x₁, x₂)]	=	2 · x₁
[U101(x₁, x₂)]	=	2 · x₂
[U13(x₁)]	=	1 · x₁
[U31(x₁)]	=	3
[singl(x₁)]	=	2 · x₁
[U11(x₁, x₂)]	=	3 · x₂
[empty]	=	2
[union(x₁, x₂)]	=	3 + 1 · x₂
[U21(x₁, x₂, x₃)]	=	1 + 2 · x₃
[U83(x₁, x₂, x₃)]	=	2 · x₁ + 3 · x₂ + 3 · x₃
[U72(x₁, x₂, x₃)]	=	1 · x₁ + 3 · x₂ + 3 · x₃
[U193(x₁, x₂, x₃)]	=	1 · x₃
[U202(x₁, x₂)]	=	1 · x₂
[U71(x₁, x₂, x₃)]	=	2 + 2 · x₁ + 3 · x₂ + 3 · x₃
[prod(x₁)]	=	3 + 2 · x₁
[sum(x₁)]	=	1 · x₁
[U84(x₁, x₂, x₃)]	=	2 + 2 · x₁ + 3 · x₂ + 3 · x₃
[U75(x₁, x₂)]	=	2 + 1 · x₁ + 3 · x₂
[U26(x₁)]	=	1 · x₁
[U22(x₁, x₂, x₃)]	=	1 + 2 · x₃
[U23(x₁, x₂, x₃)]	=	1 + 2 · x₃
[U184(x₁, x₂, x₃)]	=	0
[U232(x₁, x₂, x₃)]	=	0
[U233(x₁, x₂, x₃)]	=	0
[U224(x₁, x₂, x₃)]	=	0
[U172(x₁)]	=	0
[U221(x₁, x₂, x₃)]	=	0
[U231(x₁, x₂, x₃)]	=	0
[U201(x₁, x₂)]	=	1 · x₂
[U192(x₁, x₂, x₃)]	=	2 + 1 · x₃
[U12(x₁, x₂)]	=	2 · x₁ + 3 · x₂
[U191(x₁, x₂, x₃)]	=	2 + 1 · x₃
[U131(x₁, x₂)]	=	3 + 3 · x₂
[U132(x₁)]	=	3

together with the usable rules

U182(tt,X,Y)	→	U183(isBin(Y),X,Y)	(21)
U213(tt,X,Y)	→	U214(isBinKind(Y),X,Y)	(33)
U211(tt,X,Y)	→	U212(isBinKind(X),X,Y)	(31)
U222(tt,X,Y)	→	U223(isBin(Y),X,Y)	(37)
U234(tt,X,Y)	→	0(plus(plus(X,Y),1(z)))	(44)
U194(tt,X,Y)	→	plus(0(mult(X,Y)),Y)	(27)
U181(tt,X,Y)	→	U182(isBinKind(X),X,Y)	(20)
U193(tt,X,Y)	→	U194(isBinKind(Y),X,Y)	(26)
U202(tt,X)	→	X	(29)
U183(tt,X,Y)	→	U184(isBinKind(Y),X,Y)	(22)
U232(tt,X,Y)	→	U233(isBin(Y),X,Y)	(42)
0(z)	→	z	(3)
U223(tt,X,Y)	→	U224(isBinKind(Y),X,Y)	(38)
U171(tt,X)	→	U172(isBinKind(X))	(18)
plus(0(X),1(Y))	→	U221(isBin(X),X,Y)	(109)
plus(plus(0(X),0(Y)),ext)	→	plus(U211(isBin(X),X,Y),ext)	(337)
plus(plus(0(X),1(Y)),ext)	→	plus(U221(isBin(X),X,Y),ext)	(338)
plus(1(X),1(Y))	→	U231(isBin(X),X,Y)	(110)
plus(z,X)	→	U201(isBin(X),X)	(107)
plus(plus(1(X),1(Y)),ext)	→	plus(U231(isBin(X),X,Y),ext)	(339)
plus(0(X),0(Y))	→	U211(isBin(X),X,Y)	(108)
plus(plus(z,X),ext)	→	plus(U201(isBin(X),X),ext)	(336)
U201(tt,X)	→	U202(isBinKind(X),X)	(28)
U221(tt,X,Y)	→	U222(isBinKind(X),X,Y)	(36)
U192(tt,X,Y)	→	U193(isBin(Y),X,Y)	(25)
U191(tt,X,Y)	→	U192(isBinKind(X),X,Y)	(24)
U184(tt,X,Y)	→	0(mult(X,Y))	(23)
U224(tt,X,Y)	→	1(plus(X,Y))	(39)
mult(0(X),Y)	→	U181(isBin(X),X,Y)	(105)
mult(z,X)	→	U171(isBin(X),X)	(104)
mult(mult(1(X),Y),ext)	→	mult(U191(isBin(X),X,Y),ext)	(335)
mult(1(X),Y)	→	U191(isBin(X),X,Y)	(106)
mult(mult(z,X),ext)	→	mult(U171(isBin(X),X),ext)	(333)
mult(mult(0(X),Y),ext)	→	mult(U181(isBin(X),X,Y),ext)	(334)
U233(tt,X,Y)	→	U234(isBinKind(Y),X,Y)	(43)
U172(tt)	→	z	(19)
U231(tt,X,Y)	→	U232(isBinKind(X),X,Y)	(41)
U214(tt,X,Y)	→	0(plus(X,Y))	(34)
U212(tt,X,Y)	→	U213(isBin(Y),X,Y)	(32)
plus(plus(x,y),z')	→	plus(x,plus(y,z'))	(121)
plus(x,y)	→	plus(y,x)	(118)
mult(x,y)	→	mult(y,x)	(117)
mult(mult(x,y),z')	→	mult(x,mult(y,z'))	(120)

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

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

→

mult^#(U171(isBin(X),X),ext)

(310)

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

U212^#(tt,X,Y)	→	U213^#(isBin(Y),X,Y)	(169)
U213^#(tt,X,Y)	→	U214^#(isBinKind(Y),X,Y)	(171)
U214^#(tt,X,Y)	→	plus^#(X,Y)	(174)
plus^#(0(X),0(Y))	→	U211^#(isBin(X),X,Y)	(295)
U211^#(tt,X,Y)	→	U212^#(isBinKind(X),X,Y)	(167)
plus^#(0(X),1(Y))	→	U221^#(isBin(X),X,Y)	(297)
U221^#(tt,X,Y)	→	U222^#(isBinKind(X),X,Y)	(177)
U222^#(tt,X,Y)	→	U223^#(isBin(Y),X,Y)	(179)
U223^#(tt,X,Y)	→	U224^#(isBinKind(Y),X,Y)	(181)
U224^#(tt,X,Y)	→	plus^#(X,Y)	(183)
plus^#(1(X),1(Y))	→	U231^#(isBin(X),X,Y)	(299)
U231^#(tt,X,Y)	→	U232^#(isBinKind(X),X,Y)	(186)
U232^#(tt,X,Y)	→	U233^#(isBin(Y),X,Y)	(188)
U233^#(tt,X,Y)	→	U234^#(isBinKind(Y),X,Y)	(190)
U234^#(tt,X,Y)	→	plus^#(plus(X,Y),1(z))	(193)
plus^#(plus(z,X),ext)	→	plus^#(U201(isBin(X),X),ext)	(319)
plus^#(plus(0(X),0(Y)),ext)	→	plus^#(U211(isBin(X),X,Y),ext)	(322)
plus^#(plus(0(X),0(Y)),ext)	→	U211^#(isBin(X),X,Y)	(323)
plus^#(plus(0(X),1(Y)),ext)	→	plus^#(U221(isBin(X),X,Y),ext)	(325)
plus^#(plus(0(X),1(Y)),ext)	→	U221^#(isBin(X),X,Y)	(326)
plus^#(plus(1(X),1(Y)),ext)	→	plus^#(U231(isBin(X),X,Y),ext)	(328)
plus^#(plus(1(X),1(Y)),ext)	→	U231^#(isBin(X),X,Y)	(329)
plus^#(plus(x,y),z')	→	plus^#(y,z')	(130)
plus^#(x,y)	→	plus^#(y,x)	(124)
plus^#(plus(x,y),z')	→	plus^#(x,plus(y,z'))	(127)
U234^#(tt,X,Y)	→	plus^#(X,Y)	(194)

1.1.4 AC Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the naturals

[U214^#(x₁, x₂, x₃)]	=	1 · x₂ + 1 · x₃
[tt]	=	0
[plus^#(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[plus(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[0(x₁)]	=	1 · x₁
[1(x₁)]	=	1 + 1 · x₁
[U221^#(x₁, x₂, x₃)]	=	1 + 1 · x₂ + 1 · x₃
[isBin(x₁)]	=	0
[U222^#(x₁, x₂, x₃)]	=	1 + 1 · x₂ + 1 · x₃
[isBinKind(x₁)]	=	0
[U231^#(x₁, x₂, x₃)]	=	1 + 1 · x₂ + 1 · x₃
[U212^#(x₁, x₂, x₃)]	=	1 · x₂ + 1 · x₃
[U213^#(x₁, x₂, x₃)]	=	1 · x₂ + 1 · x₃
[U211^#(x₁, x₂, x₃)]	=	1 · x₂ + 1 · x₃
[U223^#(x₁, x₂, x₃)]	=	1 + 1 · x₂ + 1 · x₃
[U224^#(x₁, x₂, x₃)]	=	1 · x₂ + 1 · x₃
[U232^#(x₁, x₂, x₃)]	=	1 + 1 · x₂ + 1 · x₃
[U233^#(x₁, x₂, x₃)]	=	1 + 1 · x₂ + 1 · x₃
[U221(x₁, x₂, x₃)]	=	1 + 1 · x₂ + 1 · x₃
[U211(x₁, x₂, x₃)]	=	1 · x₂ + 1 · x₃
[z]	=	0
[U201(x₁, x₂)]	=	1 · x₂
[U234^#(x₁, x₂, x₃)]	=	1 + 1 · x₂ + 1 · x₃
[U231(x₁, x₂, x₃)]	=	1 + 1 · x₂ + 1 · x₃
[U224(x₁, x₂, x₃)]	=	1 + 1 · x₂ + 1 · x₃
[U234(x₁, x₂, x₃)]	=	1 + 1 · x₂ + 1 · x₃
[U41(x₁, x₂)]	=	3 + 3 · x₂
[U42(x₁)]	=	3
[isBagKind(x₁)]	=	0
[U75(x₁, x₂)]	=	3 + 3 · x₂
[U76(x₁)]	=	3
[U86(x₁)]	=	3
[U21(x₁, x₂, x₃)]	=	3 + 3 · x₂ + 3 · x₃
[U22(x₁, x₂, x₃)]	=	3 + 3 · x₂ + 3 · x₃
[U23(x₁, x₂, x₃)]	=	3 + 3 · x₂ + 3 · x₃
[U26(x₁)]	=	3
[U111(x₁)]	=	3
[U151(x₁)]	=	3
[U81(x₁, x₂, x₃)]	=	3 + 3 · x₂ + 3 · x₃
[U82(x₁, x₂, x₃)]	=	3 + 3 · x₂ + 3 · x₃
[U92(x₁, x₂)]	=	3 + 3 · x₂
[U93(x₁)]	=	3
[isBag(x₁)]	=	0
[U103(x₁)]	=	3
[U161(x₁)]	=	3
[U132(x₁)]	=	3
[empty]	=	0
[union(x₁, x₂)]	=	0
[singl(x₁)]	=	0
[U11(x₁, x₂)]	=	3 + 3 · x₂
[U212(x₁, x₂, x₃)]	=	1 · x₂ + 1 · x₃
[U213(x₁, x₂, x₃)]	=	1 · x₂ + 1 · x₃
[U121(x₁)]	=	3
[U131(x₁, x₂)]	=	3 + 3 · x₂
[U232(x₁, x₂, x₃)]	=	1 + 1 · x₂ + 1 · x₃
[U233(x₁, x₂, x₃)]	=	1 + 1 · x₂ + 1 · x₃
[mult(x₁, x₂)]	=	0
[prod(x₁)]	=	0
[sum(x₁)]	=	0
[U141(x₁, x₂)]	=	3 + 3 · x₂
[U101(x₁, x₂)]	=	3 + 3 · x₂
[U102(x₁, x₂)]	=	3 + 3 · x₂
[U142(x₁)]	=	3
[U71(x₁, x₂, x₃)]	=	3 + 3 · x₂ + 3 · x₃
[U72(x₁, x₂, x₃)]	=	3 + 3 · x₂ + 3 · x₃
[U83(x₁, x₂, x₃)]	=	3 + 3 · x₂ + 3 · x₃
[U214(x₁, x₂, x₃)]	=	1 · x₂ + 1 · x₃
[U53(x₁)]	=	3
[U202(x₁, x₂)]	=	1 · x₂
[U223(x₁, x₂, x₃)]	=	1 + 1 · x₂ + 1 · x₃
[U31(x₁)]	=	3
[U61(x₁, x₂)]	=	3 + 3 · x₂
[U91(x₁, x₂)]	=	3 + 3 · x₂
[U51(x₁, x₂)]	=	3 + 3 · x₂
[U73(x₁, x₂, x₃)]	=	3 + 3 · x₂ + 3 · x₃
[U74(x₁, x₂, x₃)]	=	3 + 3 · x₂ + 3 · x₃
[U24(x₁, x₂, x₃)]	=	3 + 3 · x₂ + 3 · x₃
[U222(x₁, x₂, x₃)]	=	1 + 1 · x₂ + 1 · x₃
[U12(x₁, x₂)]	=	3 + 3 · x₂
[U85(x₁, x₂)]	=	3 + 3 · x₂
[U13(x₁)]	=	3
[U63(x₁)]	=	3
[U84(x₁, x₂, x₃)]	=	3 + 3 · x₂ + 3 · x₃
[U25(x₁, x₂)]	=	3 + 3 · x₂
[U62(x₁, x₂)]	=	3 + 3 · x₂
[U52(x₁, x₂)]	=	3 + 3 · x₂

together with the usable rules

U224(tt,X,Y)	→	1(plus(X,Y))	(39)
U234(tt,X,Y)	→	0(plus(plus(X,Y),1(z)))	(44)
0(z)	→	z	(3)
U212(tt,X,Y)	→	U213(isBin(Y),X,Y)	(32)
U232(tt,X,Y)	→	U233(isBin(Y),X,Y)	(42)
U211(tt,X,Y)	→	U212(isBinKind(X),X,Y)	(31)
U213(tt,X,Y)	→	U214(isBinKind(Y),X,Y)	(33)
U201(tt,X)	→	U202(isBinKind(X),X)	(28)
U223(tt,X,Y)	→	U224(isBinKind(Y),X,Y)	(38)
U221(tt,X,Y)	→	U222(isBinKind(X),X,Y)	(36)
plus(z,X)	→	U201(isBin(X),X)	(107)
plus(0(X),1(Y))	→	U221(isBin(X),X,Y)	(109)
plus(plus(1(X),1(Y)),ext)	→	plus(U231(isBin(X),X,Y),ext)	(339)
plus(0(X),0(Y))	→	U211(isBin(X),X,Y)	(108)
plus(plus(0(X),0(Y)),ext)	→	plus(U211(isBin(X),X,Y),ext)	(337)
plus(plus(z,X),ext)	→	plus(U201(isBin(X),X),ext)	(336)
plus(plus(0(X),1(Y)),ext)	→	plus(U221(isBin(X),X,Y),ext)	(338)
plus(1(X),1(Y))	→	U231(isBin(X),X,Y)	(110)
U233(tt,X,Y)	→	U234(isBinKind(Y),X,Y)	(43)
U222(tt,X,Y)	→	U223(isBin(Y),X,Y)	(37)
U231(tt,X,Y)	→	U232(isBinKind(X),X,Y)	(41)
U214(tt,X,Y)	→	0(plus(X,Y))	(34)
U202(tt,X)	→	X	(29)
plus(plus(x,y),z')	→	plus(x,plus(y,z'))	(121)
plus(x,y)	→	plus(y,x)	(118)

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

plus^#(1(X),1(Y))	→	U231^#(isBin(X),X,Y)	(299)
U223^#(tt,X,Y)	→	U224^#(isBinKind(Y),X,Y)	(181)
plus^#(plus(1(X),1(Y)),ext)	→	plus^#(U231(isBin(X),X,Y),ext)	(328)
U234^#(tt,X,Y)	→	plus^#(X,Y)	(194)
plus^#(plus(1(X),1(Y)),ext)	→	U231^#(isBin(X),X,Y)	(329)

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^#(0(X),0(Y))	→	U211^#(isBin(X),X,Y)	(295)
U211^#(tt,X,Y)	→	U212^#(isBinKind(X),X,Y)	(167)
U212^#(tt,X,Y)	→	U213^#(isBin(Y),X,Y)	(169)
U213^#(tt,X,Y)	→	U214^#(isBinKind(Y),X,Y)	(171)
U214^#(tt,X,Y)	→	plus^#(X,Y)	(174)
plus^#(plus(z,X),ext)	→	plus^#(U201(isBin(X),X),ext)	(319)
plus^#(plus(0(X),0(Y)),ext)	→	plus^#(U211(isBin(X),X,Y),ext)	(322)
plus^#(plus(0(X),0(Y)),ext)	→	U211^#(isBin(X),X,Y)	(323)
plus^#(plus(0(X),1(Y)),ext)	→	plus^#(U221(isBin(X),X,Y),ext)	(325)
plus^#(plus(x,y),z')	→	plus^#(y,z')	(130)
plus^#(x,y)	→	plus^#(y,x)	(124)
plus^#(plus(x,y),z')	→	plus^#(x,plus(y,z'))	(127)

1.1.4.1.1 AC Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the naturals

[U214^#(x₁, x₂, x₃)]	=	2 · x₂ + 2 · x₃
[tt]	=	0
[plus^#(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[plus(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[0(x₁)]	=	1 + 1 · x₁
[U211(x₁, x₂, x₃)]	=	1 + 1 · x₂ + 1 · x₃
[isBin(x₁)]	=	0
[z]	=	0
[U201(x₁, x₂)]	=	1 · x₂
[U212^#(x₁, x₂, x₃)]	=	2 · x₂ + 2 · x₃
[U213^#(x₁, x₂, x₃)]	=	2 · x₂ + 2 · x₃
[U211^#(x₁, x₂, x₃)]	=	2 · x₂ + 2 · x₃
[1(x₁)]	=	1 + 1 · x₁
[U221(x₁, x₂, x₃)]	=	1 + 1 · x₂ + 1 · x₃
[isBinKind(x₁)]	=	0
[U222(x₁, x₂, x₃)]	=	1 + 1 · x₂ + 1 · x₃
[U131(x₁, x₂)]	=	3 + 3 · x₂
[U132(x₁)]	=	3
[U202(x₁, x₂)]	=	1 · x₂
[U101(x₁, x₂)]	=	3 + 3 · x₂
[U102(x₁, x₂)]	=	3 + 3 · x₂
[isBagKind(x₁)]	=	0
[U62(x₁, x₂)]	=	3 + 3 · x₂
[U63(x₁)]	=	3
[U74(x₁, x₂, x₃)]	=	3 + 3 · x₂ + 3 · x₃
[U75(x₁, x₂)]	=	3 + 3 · x₂
[U51(x₁, x₂)]	=	3 + 3 · x₂
[U52(x₁, x₂)]	=	3 + 3 · x₂
[U85(x₁, x₂)]	=	3 + 3 · x₂
[U86(x₁)]	=	3
[U41(x₁, x₂)]	=	3 + 3 · x₂
[U42(x₁)]	=	3
[U26(x₁)]	=	3
[U234(x₁, x₂, x₃)]	=	2 + 1 · x₂ + 1 · x₃
[U91(x₁, x₂)]	=	3 + 3 · x₂
[U92(x₁, x₂)]	=	3 + 3 · x₂
[U161(x₁)]	=	3
[U213(x₁, x₂, x₃)]	=	1 + 1 · x₂ + 1 · x₃
[U214(x₁, x₂, x₃)]	=	1 + 1 · x₂ + 1 · x₃
[U24(x₁, x₂, x₃)]	=	3 + 3 · x₂ + 3 · x₃
[U25(x₁, x₂)]	=	3 + 3 · x₂
[isBag(x₁)]	=	0
[U53(x₁)]	=	3
[U121(x₁)]	=	3
[U212(x₁, x₂, x₃)]	=	1 + 1 · x₂ + 1 · x₃
[U142(x₁)]	=	3
[U111(x₁)]	=	3
[U61(x₁, x₂)]	=	3 + 3 · x₂
[U71(x₁, x₂, x₃)]	=	3 + 3 · x₂ + 3 · x₃
[U72(x₁, x₂, x₃)]	=	3 + 3 · x₂ + 3 · x₃
[U141(x₁, x₂)]	=	3 + 3 · x₂
[empty]	=	0
[union(x₁, x₂)]	=	0
[U21(x₁, x₂, x₃)]	=	3 + 3 · x₂ + 3 · x₃
[singl(x₁)]	=	0
[U11(x₁, x₂)]	=	3 + 3 · x₂
[U12(x₁, x₂)]	=	3 + 3 · x₂
[U13(x₁)]	=	3
[U83(x₁, x₂, x₃)]	=	3 + 3 · x₂ + 3 · x₃
[U84(x₁, x₂, x₃)]	=	3 + 3 · x₂ + 3 · x₃
[U151(x₁)]	=	3
[U223(x₁, x₂, x₃)]	=	1 + 1 · x₂ + 1 · x₃
[U23(x₁, x₂, x₃)]	=	3 + 3 · x₂ + 3 · x₃
[U233(x₁, x₂, x₃)]	=	2 + 1 · x₂ + 1 · x₃
[U73(x₁, x₂, x₃)]	=	3 + 3 · x₂ + 3 · x₃
[U31(x₁)]	=	3
[U103(x₁)]	=	3
[U82(x₁, x₂, x₃)]	=	3 + 3 · x₂ + 3 · x₃
[U224(x₁, x₂, x₃)]	=	1 + 1 · x₂ + 1 · x₃
[U93(x₁)]	=	3
[U76(x₁)]	=	3
[U231(x₁, x₂, x₃)]	=	2 + 1 · x₂ + 1 · x₃
[U232(x₁, x₂, x₃)]	=	2 + 1 · x₂ + 1 · x₃
[mult(x₁, x₂)]	=	0
[prod(x₁)]	=	0
[sum(x₁)]	=	0
[U22(x₁, x₂, x₃)]	=	3 + 3 · x₂ + 3 · x₃
[U81(x₁, x₂, x₃)]	=	3 + 3 · x₂ + 3 · x₃

together with the usable rules

U221(tt,X,Y)	→	U222(isBinKind(X),X,Y)	(36)
U201(tt,X)	→	U202(isBinKind(X),X)	(28)
U234(tt,X,Y)	→	0(plus(plus(X,Y),1(z)))	(44)
U213(tt,X,Y)	→	U214(isBinKind(Y),X,Y)	(33)
U212(tt,X,Y)	→	U213(isBin(Y),X,Y)	(32)
U222(tt,X,Y)	→	U223(isBin(Y),X,Y)	(37)
U233(tt,X,Y)	→	U234(isBinKind(Y),X,Y)	(43)
U224(tt,X,Y)	→	1(plus(X,Y))	(39)
U231(tt,X,Y)	→	U232(isBinKind(X),X,Y)	(41)
U214(tt,X,Y)	→	0(plus(X,Y))	(34)
plus(z,X)	→	U201(isBin(X),X)	(107)
plus(0(X),1(Y))	→	U221(isBin(X),X,Y)	(109)
plus(plus(1(X),1(Y)),ext)	→	plus(U231(isBin(X),X,Y),ext)	(339)
plus(0(X),0(Y))	→	U211(isBin(X),X,Y)	(108)
plus(plus(0(X),0(Y)),ext)	→	plus(U211(isBin(X),X,Y),ext)	(337)
plus(plus(z,X),ext)	→	plus(U201(isBin(X),X),ext)	(336)
plus(plus(0(X),1(Y)),ext)	→	plus(U221(isBin(X),X,Y),ext)	(338)
plus(1(X),1(Y))	→	U231(isBin(X),X,Y)	(110)
U232(tt,X,Y)	→	U233(isBin(Y),X,Y)	(42)
0(z)	→	z	(3)
U202(tt,X)	→	X	(29)
U211(tt,X,Y)	→	U212(isBinKind(X),X,Y)	(31)
U223(tt,X,Y)	→	U224(isBinKind(Y),X,Y)	(38)
plus(plus(x,y),z')	→	plus(x,plus(y,z'))	(121)
plus(x,y)	→	plus(y,x)	(118)

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

plus^#(plus(0(X),0(Y)),ext)	→	plus^#(U211(isBin(X),X,Y),ext)	(322)
plus^#(plus(0(X),0(Y)),ext)	→	U211^#(isBin(X),X,Y)	(323)
plus^#(plus(0(X),1(Y)),ext)	→	plus^#(U221(isBin(X),X,Y),ext)	(325)
plus^#(0(X),0(Y))	→	U211^#(isBin(X),X,Y)	(295)

could be deleted.

1.1.4.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

plus^#(plus(x,y),z')	→	plus^#(y,z')	(130)
plus^#(plus(z,X),ext)	→	plus^#(U201(isBin(X),X),ext)	(319)
plus^#(x,y)	→	plus^#(y,x)	(124)
plus^#(plus(x,y),z')	→	plus^#(x,plus(y,z'))	(127)

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₂)]	=	1 · x₁ + 1 · x₂
[plus(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[z]	=	0
[U201(x₁, x₂)]	=	1 + 1 · x₂
[isBin(x₁)]	=	1 + 1 · x₁
[tt]	=	1
[U202(x₁, x₂)]	=	1 · x₂
[isBinKind(x₁)]	=	0
[U74(x₁, x₂, x₃)]	=	1 + 3 · x₁ + 1 · x₂
[U75(x₁, x₂)]	=	1 + 1 · x₁
[U93(x₁)]	=	1 · x₁
[U82(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂
[U83(x₁, x₂, x₃)]	=	1 · x₂
[U51(x₁, x₂)]	=	2 + 2 · x₁
[U52(x₁, x₂)]	=	2 · x₁
[U12(x₁, x₂)]	=	2 + 2 · x₁
[U13(x₁)]	=	2
[U103(x₁)]	=	1 · x₁
[U26(x₁)]	=	1
[U151(x₁)]	=	3
[U102(x₁, x₂)]	=	1 · x₂
[isBag(x₁)]	=	1 · x₁
[U61(x₁, x₂)]	=	2 + 2 · x₁
[U62(x₁, x₂)]	=	3 + 3 · x₁
[U231(x₁, x₂, x₃)]	=	3
[U232(x₁, x₂, x₃)]	=	3
[U111(x₁)]	=	3
[U233(x₁, x₂, x₃)]	=	2
[U234(x₁, x₂, x₃)]	=	1
[U101(x₁, x₂)]	=	2 · x₁ + 1 · x₂
[isBagKind(x₁)]	=	0
[U63(x₁)]	=	1
[U121(x₁)]	=	3
[U53(x₁)]	=	1
[U213(x₁, x₂, x₃)]	=	2
[U214(x₁, x₂, x₃)]	=	2
[U223(x₁, x₂, x₃)]	=	2
[U224(x₁, x₂, x₃)]	=	2
[U161(x₁)]	=	3
[1(x₁)]	=	1
[sum(x₁)]	=	3 + 2 · x₁
[U81(x₁, x₂, x₃)]	=	1 · x₂
[mult(x₁, x₂)]	=	2 + 2 · x₁ + 2 · x₂
[U71(x₁, x₂, x₃)]	=	1 + 1 · x₂
[prod(x₁)]	=	2 + 2 · x₁
[U91(x₁, x₂)]	=	3 + 3 · x₁ + 1 · x₂
[0(x₁)]	=	1
[U86(x₁)]	=	1
[U142(x₁)]	=	3
[U211(x₁, x₂, x₃)]	=	2
[U212(x₁, x₂, x₃)]	=	2
[U24(x₁, x₂, x₃)]	=	1 · x₁
[U25(x₁, x₂)]	=	1
[empty]	=	2
[union(x₁, x₂)]	=	2 + 2 · x₁ + 2 · x₂
[U21(x₁, x₂, x₃)]	=	0
[singl(x₁)]	=	3 + 2 · x₁
[U11(x₁, x₂)]	=	2 + 2 · x₁
[U221(x₁, x₂, x₃)]	=	2
[U72(x₁, x₂, x₃)]	=	1 + 3 · x₁ + 1 · x₂
[U131(x₁, x₂)]	=	3 + 3 · x₂
[U141(x₁, x₂)]	=	3 + 3 · x₂
[U42(x₁)]	=	3
[U76(x₁)]	=	1
[U22(x₁, x₂, x₃)]	=	0
[U23(x₁, x₂, x₃)]	=	1 · x₁
[U132(x₁)]	=	3
[U92(x₁, x₂)]	=	1 · x₂
[U222(x₁, x₂, x₃)]	=	2
[U41(x₁, x₂)]	=	3 + 3 · x₂
[U31(x₁)]	=	3
[U85(x₁, x₂)]	=	1 · x₁
[U73(x₁, x₂, x₃)]	=	3 + 1 · x₁ + 1 · x₂
[U84(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂

together with the usable rules

U201(tt,X)	→	U202(isBinKind(X),X)	(28)
U231(tt,X,Y)	→	U232(isBinKind(X),X,Y)	(41)
U233(tt,X,Y)	→	U234(isBinKind(Y),X,Y)	(43)
U213(tt,X,Y)	→	U214(isBinKind(Y),X,Y)	(33)
U223(tt,X,Y)	→	U224(isBinKind(Y),X,Y)	(38)
U202(tt,X)	→	X	(29)
U224(tt,X,Y)	→	1(plus(X,Y))	(39)
U211(tt,X,Y)	→	U212(isBinKind(X),X,Y)	(31)
0(z)	→	z	(3)
plus(z,X)	→	U201(isBin(X),X)	(107)
plus(0(X),1(Y))	→	U221(isBin(X),X,Y)	(109)
plus(plus(1(X),1(Y)),ext)	→	plus(U231(isBin(X),X,Y),ext)	(339)
plus(0(X),0(Y))	→	U211(isBin(X),X,Y)	(108)
plus(plus(0(X),0(Y)),ext)	→	plus(U211(isBin(X),X,Y),ext)	(337)
plus(plus(z,X),ext)	→	plus(U201(isBin(X),X),ext)	(336)
plus(plus(0(X),1(Y)),ext)	→	plus(U221(isBin(X),X,Y),ext)	(338)
plus(1(X),1(Y))	→	U231(isBin(X),X,Y)	(110)
U214(tt,X,Y)	→	0(plus(X,Y))	(34)
U222(tt,X,Y)	→	U223(isBin(Y),X,Y)	(37)
U221(tt,X,Y)	→	U222(isBinKind(X),X,Y)	(36)
U232(tt,X,Y)	→	U233(isBin(Y),X,Y)	(42)
U212(tt,X,Y)	→	U213(isBin(Y),X,Y)	(32)
U234(tt,X,Y)	→	0(plus(plus(X,Y),1(z)))	(44)
plus(plus(x,y),z')	→	plus(x,plus(y,z'))	(121)
plus(x,y)	→	plus(y,x)	(118)

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

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

→

plus^#(y,z')

(130)

could be deleted.

1.1.4.1.1.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₂)]	=	1 + 1 · x₁ + 1 · x₂
[z]	=	0
[U201(x₁, x₂)]	=	1 · x₂
[isBin(x₁)]	=	0
[isBag(x₁)]	=	0
[empty]	=	0
[tt]	=	0
[union(x₁, x₂)]	=	0
[U21(x₁, x₂, x₃)]	=	3 + 3 · x₂ + 3 · x₃
[isBagKind(x₁)]	=	0
[singl(x₁)]	=	0
[U11(x₁, x₂)]	=	3 + 3 · x₂
[isBinKind(x₁)]	=	0
[U41(x₁, x₂)]	=	3 + 3 · x₂
[U42(x₁)]	=	3
[U23(x₁, x₂, x₃)]	=	3 + 3 · x₂ + 3 · x₃
[U24(x₁, x₂, x₃)]	=	3 + 3 · x₂ + 3 · x₃
[U72(x₁, x₂, x₃)]	=	3 + 3 · x₂ + 3 · x₃
[U73(x₁, x₂, x₃)]	=	3 + 3 · x₂ + 3 · x₃
[U22(x₁, x₂, x₃)]	=	3 + 3 · x₂ + 3 · x₃
[U13(x₁)]	=	3
[U202(x₁, x₂)]	=	1 · x₂
[U214(x₁, x₂, x₃)]	=	0
[0(x₁)]	=	0
[1(x₁)]	=	0
[U61(x₁, x₂)]	=	3 + 3 · x₂
[sum(x₁)]	=	0
[U101(x₁, x₂)]	=	3 + 3 · x₂
[U81(x₁, x₂, x₃)]	=	3 + 3 · x₂ + 3 · x₃
[mult(x₁, x₂)]	=	0
[U71(x₁, x₂, x₃)]	=	3 + 3 · x₂ + 3 · x₃
[prod(x₁)]	=	0
[U91(x₁, x₂)]	=	3 + 3 · x₂
[U51(x₁, x₂)]	=	3 + 3 · x₂
[U221(x₁, x₂, x₃)]	=	1
[U222(x₁, x₂, x₃)]	=	1
[U231(x₁, x₂, x₃)]	=	0
[U232(x₁, x₂, x₃)]	=	0
[U103(x₁)]	=	3
[U25(x₁, x₂)]	=	3 + 3 · x₂
[U31(x₁)]	=	3
[U26(x₁)]	=	3
[U224(x₁, x₂, x₃)]	=	0
[U132(x₁)]	=	3
[U102(x₁, x₂)]	=	3 + 3 · x₂
[U211(x₁, x₂, x₃)]	=	1
[U212(x₁, x₂, x₃)]	=	1
[U53(x₁)]	=	3
[U223(x₁, x₂, x₃)]	=	1
[U62(x₁, x₂)]	=	3 + 3 · x₂
[U63(x₁)]	=	3
[U121(x₁)]	=	3
[U131(x₁, x₂)]	=	3 + 3 · x₂
[U151(x₁)]	=	3
[U161(x₁)]	=	3
[U111(x₁)]	=	3
[U141(x₁, x₂)]	=	3 + 3 · x₂
[U82(x₁, x₂, x₃)]	=	3 + 3 · x₂ + 3 · x₃
[U83(x₁, x₂, x₃)]	=	3 + 3 · x₂ + 3 · x₃
[U142(x₁)]	=	3
[U84(x₁, x₂, x₃)]	=	3 + 3 · x₂ + 3 · x₃
[U233(x₁, x₂, x₃)]	=	0
[U85(x₁, x₂)]	=	3 + 3 · x₂
[U86(x₁)]	=	3
[U92(x₁, x₂)]	=	3 + 3 · x₂
[U213(x₁, x₂, x₃)]	=	0
[U12(x₁, x₂)]	=	3 + 3 · x₂
[U74(x₁, x₂, x₃)]	=	3 + 3 · x₂ + 3 · x₃
[U75(x₁, x₂)]	=	3 + 3 · x₂
[U93(x₁)]	=	3
[U234(x₁, x₂, x₃)]	=	0
[U52(x₁, x₂)]	=	3 + 3 · x₂
[U76(x₁)]	=	3

together with the usable rules

U201(tt,X)	→	U202(isBinKind(X),X)	(28)
U214(tt,X,Y)	→	0(plus(X,Y))	(34)
U221(tt,X,Y)	→	U222(isBinKind(X),X,Y)	(36)
U231(tt,X,Y)	→	U232(isBinKind(X),X,Y)	(41)
U224(tt,X,Y)	→	1(plus(X,Y))	(39)
U211(tt,X,Y)	→	U212(isBinKind(X),X,Y)	(31)
U222(tt,X,Y)	→	U223(isBin(Y),X,Y)	(37)
U232(tt,X,Y)	→	U233(isBin(Y),X,Y)	(42)
U213(tt,X,Y)	→	U214(isBinKind(Y),X,Y)	(33)
U202(tt,X)	→	X	(29)
plus(z,X)	→	U201(isBin(X),X)	(107)
plus(0(X),1(Y))	→	U221(isBin(X),X,Y)	(109)
plus(plus(1(X),1(Y)),ext)	→	plus(U231(isBin(X),X,Y),ext)	(339)
plus(0(X),0(Y))	→	U211(isBin(X),X,Y)	(108)
plus(plus(0(X),0(Y)),ext)	→	plus(U211(isBin(X),X,Y),ext)	(337)
plus(plus(z,X),ext)	→	plus(U201(isBin(X),X),ext)	(336)
plus(plus(0(X),1(Y)),ext)	→	plus(U221(isBin(X),X,Y),ext)	(338)
plus(1(X),1(Y))	→	U231(isBin(X),X,Y)	(110)
U212(tt,X,Y)	→	U213(isBin(Y),X,Y)	(32)
U223(tt,X,Y)	→	U224(isBinKind(Y),X,Y)	(38)
U234(tt,X,Y)	→	0(plus(plus(X,Y),1(z)))	(44)
0(z)	→	z	(3)
U233(tt,X,Y)	→	U234(isBinKind(Y),X,Y)	(43)
plus(plus(x,y),z')	→	plus(x,plus(y,z'))	(121)
plus(x,y)	→	plus(y,x)	(118)

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

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

→

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

(319)

could be deleted.

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

U102^#(tt,V1)	→	isBag^#(V1)	(135)
isBag^#(singl(V1))	→	U11^#(isBinKind(V1),V1)	(255)
U11^#(tt,V1)	→	U12^#(isBinKind(V1),V1)	(136)
U12^#(tt,V1)	→	isBin^#(V1)	(139)
isBin^#(0(V1))	→	U51^#(isBinKind(V1),V1)	(263)
U51^#(tt,V1)	→	U52^#(isBinKind(V1),V1)	(223)
U52^#(tt,V1)	→	isBin^#(V1)	(226)
isBin^#(1(V1))	→	U61^#(isBinKind(V1),V1)	(265)
U61^#(tt,V1)	→	U62^#(isBinKind(V1),V1)	(227)
U62^#(tt,V1)	→	isBin^#(V1)	(230)
isBin^#(mult(V1,V2))	→	U71^#(isBinKind(V1),V1,V2)	(267)
U71^#(tt,V1,V2)	→	U72^#(isBinKind(V1),V1,V2)	(231)
U72^#(tt,V1,V2)	→	U73^#(isBinKind(V2),V1,V2)	(233)
U73^#(tt,V1,V2)	→	U74^#(isBinKind(V2),V1,V2)	(235)
U74^#(tt,V1,V2)	→	U75^#(isBin(V1),V2)	(237)
U75^#(tt,V2)	→	isBin^#(V2)	(240)
isBin^#(plus(V1,V2))	→	U81^#(isBinKind(V1),V1,V2)	(269)
U81^#(tt,V1,V2)	→	U82^#(isBinKind(V1),V1,V2)	(241)
U82^#(tt,V1,V2)	→	U83^#(isBinKind(V2),V1,V2)	(243)
U83^#(tt,V1,V2)	→	U84^#(isBinKind(V2),V1,V2)	(245)
U84^#(tt,V1,V2)	→	U85^#(isBin(V1),V2)	(247)
U85^#(tt,V2)	→	isBin^#(V2)	(250)
isBin^#(prod(V1))	→	U91^#(isBagKind(V1),V1)	(271)
U91^#(tt,V1)	→	U92^#(isBagKind(V1),V1)	(251)
U92^#(tt,V1)	→	isBag^#(V1)	(254)
isBag^#(union(V1,V2))	→	U21^#(isBagKind(V1),V1,V2)	(257)
U21^#(tt,V1,V2)	→	U22^#(isBagKind(V1),V1,V2)	(165)
U22^#(tt,V1,V2)	→	U23^#(isBagKind(V2),V1,V2)	(175)
U23^#(tt,V1,V2)	→	U24^#(isBagKind(V2),V1,V2)	(184)
U24^#(tt,V1,V2)	→	U25^#(isBag(V1),V2)	(195)
U25^#(tt,V2)	→	isBag^#(V2)	(200)
U24^#(tt,V1,V2)	→	isBag^#(V1)	(196)
isBin^#(sum(V1))	→	U101^#(isBagKind(V1),V1)	(273)
U101^#(tt,V1)	→	U102^#(isBagKind(V1),V1)	(132)
U84^#(tt,V1,V2)	→	isBin^#(V1)	(248)
U74^#(tt,V1,V2)	→	isBin^#(V1)	(238)

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₁)]	=	2 + 3 · x₁
[U61(x₁, x₂)]	=	2 + 1 · x₁ + 2 · x₂
[isBinKind(x₁)]	=	1 · x₁
[sum(x₁)]	=	1 + 3 · x₁
[U101(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[isBagKind(x₁)]	=	1 · x₁
[mult(x₁, x₂)]	=	1 + 3 · x₁ + 3 · x₂
[U131(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[U103(x₁)]	=	1 · x₁
[tt]	=	2
[isBag(x₁)]	=	1 + 1 · x₁
[empty]	=	2
[U81(x₁, x₂, x₃)]	=	1 · x₁ + 2 · x₂ + 3 · x₃
[U82(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 3 · x₃
[U25(x₁, x₂)]	=	2 + 1 · x₁ + 1 · x₂
[U26(x₁)]	=	2 + 1 · x₁
[U71(x₁, x₂, x₃)]	=	1 + 1 · x₁ + 2 · x₂ + 3 · x₃
[U72(x₁, x₂, x₃)]	=	2 + 1 · x₁ + 1 · x₂ + 3 · x₃
[prod(x₁)]	=	2 + 3 · x₁
[U151(x₁)]	=	2 + 1 · x₁
[U74(x₁, x₂, x₃)]	=	2 + 1 · x₁ + 1 · x₂ + 1 · x₃
[U75(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[plus(x₁, x₂)]	=	2 + 3 · x₁ + 3 · x₂
[U62(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[U84(x₁, x₂, x₃)]	=	2 + 1 · x₁ + 1 · x₂ + 1 · x₃
[U85(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[U141(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[U142(x₁)]	=	2 + 1 · x₁
[U12(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[U13(x₁)]	=	1 · x₁
[U86(x₁)]	=	1 · x₁
[U24(x₁, x₂, x₃)]	=	2 + 1 · x₁ + 1 · x₂ + 1 · x₃
[U93(x₁)]	=	1 · x₁
[U111(x₁)]	=	1 · x₁
[U121(x₁)]	=	1 · x₁
[union(x₁, x₂)]	=	1 + 3 · x₁ + 3 · x₂
[U21(x₁, x₂, x₃)]	=	1 · x₁ + 2 · x₂ + 3 · x₃
[U22(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 3 · x₃
[U76(x₁)]	=	2 + 1 · x₁
[U132(x₁)]	=	2 + 1 · x₁
[U51(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[U52(x₁, x₂)]	=	2 + 1 · x₁ + 1 · x₂
[z]	=	2
[U91(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[U102(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[U41(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[U23(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 2 · x₃
[U42(x₁)]	=	2 · x₁
[U83(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 2 · x₃
[U92(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[singl(x₁)]	=	3 · x₁
[U11(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[U73(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 2 · x₃
[U53(x₁)]	=	2 + 1 · x₁
[U31(x₁)]	=	1 · x₁
[U161(x₁)]	=	2 · x₁
[0(x₁)]	=	3 + 3 · x₁
[U63(x₁)]	=	2 + 1 · x₁
[U24^#(x₁, x₂, x₃)]	=	2 + 1 · x₁ + 1 · x₂ + 1 · x₃
[isBag^#(x₁)]	=	1 · x₁
[U102^#(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[U12^#(x₁, x₂)]	=	2 + 1 · x₁ + 1 · x₂
[isBin^#(x₁)]	=	1 · x₁
[U11^#(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[U83^#(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 2 · x₃
[U84^#(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 1 · x₃
[U85^#(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[U25^#(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[U72^#(x₁, x₂, x₃)]	=	2 + 1 · x₁ + 1 · x₂ + 3 · x₃
[U73^#(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 2 · x₃
[U51^#(x₁, x₂)]	=	2 + 1 · x₁ + 2 · x₂
[U91^#(x₁, x₂)]	=	2 + 1 · x₁ + 2 · x₂
[U92^#(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[U61^#(x₁, x₂)]	=	2 + 1 · x₁ + 2 · x₂
[U62^#(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[U21^#(x₁, x₂, x₃)]	=	1 · x₁ + 2 · x₂ + 3 · x₃
[U22^#(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 3 · x₃
[U75^#(x₁, x₂)]	=	2 + 1 · x₁ + 1 · x₂
[U23^#(x₁, x₂, x₃)]	=	2 + 1 · x₁ + 1 · x₂ + 2 · x₃
[U81^#(x₁, x₂, x₃)]	=	1 · x₁ + 2 · x₂ + 3 · x₃
[U82^#(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 3 · x₃
[U52^#(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[U74^#(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 1 · x₃
[U101^#(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[U71^#(x₁, x₂, x₃)]	=	1 · x₁ + 2 · x₂ + 3 · x₃

together with the usable rules

isBin(1(V1))	→	U61(isBinKind(V1),V1)	(92)
isBin(sum(V1))	→	U101(isBagKind(V1),V1)	(96)
isBinKind(mult(V1,V2))	→	U131(isBinKind(V1),V2)	(100)
U103(tt)	→	tt	(6)
isBag(empty)	→	tt	(84)
U81(tt,V1,V2)	→	U82(isBinKind(V1),V1,V2)	(75)
U25(tt,V2)	→	U26(isBag(V2))	(48)
U71(tt,V1,V2)	→	U72(isBinKind(V1),V1,V2)	(69)
isBinKind(prod(V1))	→	U151(isBagKind(V1))	(102)
U74(tt,V1,V2)	→	U75(isBin(V1),V2)	(72)
isBin(plus(V1,V2))	→	U81(isBinKind(V1),V1,V2)	(94)
U61(tt,V1)	→	U62(isBinKind(V1),V1)	(66)
isBagKind(empty)	→	tt	(87)
U84(tt,V1,V2)	→	U85(isBin(V1),V2)	(78)
U141(tt,V2)	→	U142(isBinKind(V2))	(14)
U12(tt,V1)	→	U13(isBin(V1))	(9)
U85(tt,V2)	→	U86(isBin(V2))	(79)
U24(tt,V1,V2)	→	U25(isBag(V1),V2)	(45)
U93(tt)	→	tt	(83)
U111(tt)	→	tt	(8)
U121(tt)	→	tt	(10)
isBag(union(V1,V2))	→	U21(isBagKind(V1),V1,V2)	(86)
U21(tt,V1,V2)	→	U22(isBagKind(V1),V1,V2)	(30)
U75(tt,V2)	→	U76(isBin(V2))	(73)
U131(tt,V2)	→	U132(isBinKind(V2))	(12)
U51(tt,V1)	→	U52(isBinKind(V1),V1)	(63)
isBinKind(1(V1))	→	U121(isBinKind(V1))	(99)
isBin(z)	→	tt	(90)
U13(tt)	→	tt	(11)
isBin(mult(V1,V2))	→	U71(isBinKind(V1),V1,V2)	(93)
isBin(prod(V1))	→	U91(isBagKind(V1),V1)	(95)
U102(tt,V1)	→	U103(isBag(V1))	(5)
isBagKind(union(V1,V2))	→	U41(isBagKind(V1),V2)	(89)
U23(tt,V1,V2)	→	U24(isBagKind(V2),V1,V2)	(40)
U26(tt)	→	tt	(53)
U42(tt)	→	tt	(62)
U82(tt,V1,V2)	→	U83(isBinKind(V2),V1,V2)	(76)
U92(tt,V1)	→	U93(isBag(V1))	(82)
isBag(singl(V1))	→	U11(isBinKind(V1),V1)	(85)
U101(tt,V1)	→	U102(isBagKind(V1),V1)	(4)
U72(tt,V1,V2)	→	U73(isBinKind(V2),V1,V2)	(70)
U11(tt,V1)	→	U12(isBinKind(V1),V1)	(7)
U52(tt,V1)	→	U53(isBin(V1))	(64)
U22(tt,V1,V2)	→	U23(isBagKind(V2),V1,V2)	(35)
isBagKind(singl(V1))	→	U31(isBinKind(V1))	(88)
isBinKind(sum(V1))	→	U161(isBagKind(V1))	(103)
U31(tt)	→	tt	(60)
U41(tt,V2)	→	U42(isBagKind(V2))	(61)
U83(tt,V1,V2)	→	U84(isBinKind(V2),V1,V2)	(77)
U142(tt)	→	tt	(15)
U161(tt)	→	tt	(17)
U91(tt,V1)	→	U92(isBagKind(V1),V1)	(81)
U76(tt)	→	tt	(74)
U132(tt)	→	tt	(13)
isBinKind(0(V1))	→	U111(isBinKind(V1))	(98)
isBinKind(plus(V1,V2))	→	U141(isBinKind(V1),V2)	(101)
U86(tt)	→	tt	(80)
U53(tt)	→	tt	(65)
U62(tt,V1)	→	U63(isBin(V1))	(67)
U63(tt)	→	tt	(68)
isBin(0(V1))	→	U51(isBinKind(V1),V1)	(91)
U151(tt)	→	tt	(16)
isBinKind(z)	→	tt	(97)
U73(tt,V1,V2)	→	U74(isBinKind(V2),V1,V2)	(71)

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

U24^#(tt,V1,V2)	→	isBag^#(V1)	(196)
U102^#(tt,V1)	→	isBag^#(V1)	(135)
U12^#(tt,V1)	→	isBin^#(V1)	(139)
U83^#(tt,V1,V2)	→	U84^#(isBinKind(V2),V1,V2)	(245)
U85^#(tt,V2)	→	isBin^#(V2)	(250)
U25^#(tt,V2)	→	isBag^#(V2)	(200)
U72^#(tt,V1,V2)	→	U73^#(isBinKind(V2),V1,V2)	(233)
isBin^#(0(V1))	→	U51^#(isBinKind(V1),V1)	(263)
U91^#(tt,V1)	→	U92^#(isBagKind(V1),V1)	(251)
U61^#(tt,V1)	→	U62^#(isBinKind(V1),V1)	(227)
U21^#(tt,V1,V2)	→	U22^#(isBagKind(V1),V1,V2)	(165)
U75^#(tt,V2)	→	isBin^#(V2)	(240)
U23^#(tt,V1,V2)	→	U24^#(isBagKind(V2),V1,V2)	(184)
U81^#(tt,V1,V2)	→	U82^#(isBinKind(V1),V1,V2)	(241)
U51^#(tt,V1)	→	U52^#(isBinKind(V1),V1)	(223)
U74^#(tt,V1,V2)	→	isBin^#(V1)	(238)
isBin^#(sum(V1))	→	U101^#(isBagKind(V1),V1)	(273)
U24^#(tt,V1,V2)	→	U25^#(isBag(V1),V2)	(195)
U101^#(tt,V1)	→	U102^#(isBagKind(V1),V1)	(132)
isBag^#(union(V1,V2))	→	U21^#(isBagKind(V1),V1,V2)	(257)
U52^#(tt,V1)	→	isBin^#(V1)	(226)
U92^#(tt,V1)	→	isBag^#(V1)	(254)
U73^#(tt,V1,V2)	→	U74^#(isBinKind(V2),V1,V2)	(235)
isBin^#(1(V1))	→	U61^#(isBinKind(V1),V1)	(265)
isBag^#(singl(V1))	→	U11^#(isBinKind(V1),V1)	(255)
U84^#(tt,V1,V2)	→	U85^#(isBin(V1),V2)	(247)
isBin^#(prod(V1))	→	U91^#(isBagKind(V1),V1)	(271)
isBin^#(plus(V1,V2))	→	U81^#(isBinKind(V1),V1,V2)	(269)
U82^#(tt,V1,V2)	→	U83^#(isBinKind(V2),V1,V2)	(243)
U62^#(tt,V1)	→	isBin^#(V1)	(230)
U84^#(tt,V1,V2)	→	isBin^#(V1)	(248)
isBin^#(mult(V1,V2))	→	U71^#(isBinKind(V1),V1,V2)	(267)

and the rules

There are 112 ruless (increase limit for explicit display).

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

U131^#(tt,V2)	→	isBinKind^#(V2)	(141)
isBinKind^#(0(V1))	→	isBinKind^#(V1)	(276)
isBinKind^#(1(V1))	→	isBinKind^#(V1)	(278)
isBinKind^#(mult(V1,V2))	→	U131^#(isBinKind(V1),V2)	(279)
isBinKind^#(mult(V1,V2))	→	isBinKind^#(V1)	(280)
isBinKind^#(plus(V1,V2))	→	U141^#(isBinKind(V1),V2)	(281)
U141^#(tt,V2)	→	isBinKind^#(V2)	(143)
isBinKind^#(plus(V1,V2))	→	isBinKind^#(V1)	(282)
isBinKind^#(prod(V1))	→	isBagKind^#(V1)	(284)
isBagKind^#(singl(V1))	→	isBinKind^#(V1)	(260)
isBinKind^#(sum(V1))	→	isBagKind^#(V1)	(286)
isBagKind^#(union(V1,V2))	→	U41^#(isBagKind(V1),V2)	(261)
U41^#(tt,V2)	→	isBagKind^#(V2)	(222)
isBagKind^#(union(V1,V2))	→	isBagKind^#(V1)	(262)

1.1.6 AC Monotonic Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the naturals

[U142(x₁)]	=	1 · x₁
[tt]	=	2
[U42(x₁)]	=	1 · x₁
[isBinKind(x₁)]	=	2 · x₁
[mult(x₁, x₂)]	=	2 + 3 · x₁ + 3 · x₂
[U131(x₁, x₂)]	=	2 · x₁ + 3 · x₂
[U161(x₁)]	=	2 · x₁
[U132(x₁)]	=	2 + 1 · x₁
[1(x₁)]	=	3 · x₁
[U121(x₁)]	=	2 · x₁
[prod(x₁)]	=	3 + 2 · x₁
[U151(x₁)]	=	2 · x₁
[isBagKind(x₁)]	=	2 + 2 · x₁
[empty]	=	1
[U141(x₁, x₂)]	=	1 · x₁ + 3 · x₂
[0(x₁)]	=	2 + 2 · x₁
[U111(x₁)]	=	1 · x₁
[plus(x₁, x₂)]	=	1 · x₁ + 3 · x₂
[union(x₁, x₂)]	=	3 + 2 · x₁ + 3 · x₂
[U41(x₁, x₂)]	=	2 · x₁ + 3 · x₂
[singl(x₁)]	=	3 · x₁
[U31(x₁)]	=	2 · x₁
[sum(x₁)]	=	3 + 3 · x₁
[z]	=	2
[U141^#(x₁, x₂)]	=	1 · x₁ + 3 · x₂
[isBinKind^#(x₁)]	=	2 · x₁
[isBagKind^#(x₁)]	=	3 · x₁
[U41^#(x₁, x₂)]	=	2 · x₁ + 3 · x₂
[U131^#(x₁, x₂)]	=	2 · x₁ + 3 · x₂

together with the usable rules

U142(tt)	→	tt	(15)
U42(tt)	→	tt	(62)
isBinKind(mult(V1,V2))	→	U131(isBinKind(V1),V2)	(100)
U161(tt)	→	tt	(17)
U131(tt,V2)	→	U132(isBinKind(V2))	(12)
isBinKind(1(V1))	→	U121(isBinKind(V1))	(99)
isBinKind(prod(V1))	→	U151(isBagKind(V1))	(102)
isBagKind(empty)	→	tt	(87)
U132(tt)	→	tt	(13)
U141(tt,V2)	→	U142(isBinKind(V2))	(14)
isBinKind(0(V1))	→	U111(isBinKind(V1))	(98)
isBinKind(plus(V1,V2))	→	U141(isBinKind(V1),V2)	(101)
isBagKind(union(V1,V2))	→	U41(isBagKind(V1),V2)	(89)
U111(tt)	→	tt	(8)
U121(tt)	→	tt	(10)
isBagKind(singl(V1))	→	U31(isBinKind(V1))	(88)
isBinKind(sum(V1))	→	U161(isBagKind(V1))	(103)
U31(tt)	→	tt	(60)
isBinKind(z)	→	tt	(97)
U151(tt)	→	tt	(16)
U41(tt,V2)	→	U42(isBagKind(V2))	(61)

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

U141^#(tt,V2)	→	isBinKind^#(V2)	(143)
isBinKind^#(prod(V1))	→	isBagKind^#(V1)	(284)
U41^#(tt,V2)	→	isBagKind^#(V2)	(222)
isBagKind^#(union(V1,V2))	→	isBagKind^#(V1)	(262)
isBinKind^#(0(V1))	→	isBinKind^#(V1)	(276)
isBinKind^#(1(V1))	→	isBinKind^#(V1)	(278)
isBinKind^#(plus(V1,V2))	→	isBinKind^#(V1)	(282)
isBinKind^#(sum(V1))	→	isBagKind^#(V1)	(286)
isBinKind^#(plus(V1,V2))	→	U141^#(isBinKind(V1),V2)	(281)
U131^#(tt,V2)	→	isBinKind^#(V2)	(141)
isBinKind^#(mult(V1,V2))	→	isBinKind^#(V1)	(280)
isBinKind^#(mult(V1,V2))	→	U131^#(isBinKind(V1),V2)	(279)
isBagKind^#(singl(V1))	→	isBinKind^#(V1)	(260)
isBagKind^#(union(V1,V2))	→	U41^#(isBagKind(V1),V2)	(261)

and the rules

There are 122 ruless (increase limit for explicit display).

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)	(332)
union^#(union(X,empty),ext)	→	union^#(X,ext)	(331)
union^#(union(x,y),z')	→	union^#(y,z')	(131)
union^#(x,y)	→	union^#(y,x)	(125)
union^#(union(x,y),z')	→	union^#(x,union(y,z'))	(128)

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)	(340)
union(union(empty,X),ext)	→	union(X,ext)	(341)
union(union(x,y),z')	→	union(x,union(y,z'))	(122)
union(x,y)	→	union(y,x)	(119)

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

union^#(union(empty,X),ext)	→	union^#(X,ext)	(332)
union^#(union(X,empty),ext)	→	union^#(X,ext)	(331)

and the rules

There are 125 ruless (increase limit for explicit display).

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)	(117)
plus(x,y)	→	plus(y,x)	(118)
union(x,y)	→	union(y,x)	(119)
mult(mult(x,y),z')	→	mult(x,mult(y,z'))	(120)
plus(plus(x,y),z')	→	plus(x,plus(y,z'))	(121)
union(union(x,y),z')	→	union(x,union(y,z'))	(122)

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

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

→

union^#(y,z')

(131)

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.