Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/MYNAT_nokinds-noand_Z)

The rewrite relation of the following TRS is considered.

U11(tt,V2)	→	U12(isNat(activate(V2)))	(1)
U12(tt)	→	tt	(2)
U21(tt)	→	tt	(3)
U31(tt,V2)	→	U32(isNat(activate(V2)))	(4)
U32(tt)	→	tt	(5)
U41(tt,N)	→	activate(N)	(6)
U51(tt,M,N)	→	U52(isNat(activate(N)),activate(M),activate(N))	(7)
U52(tt,M,N)	→	s(plus(activate(N),activate(M)))	(8)
U61(tt)	→	0	(9)
U71(tt,M,N)	→	U72(isNat(activate(N)),activate(M),activate(N))	(10)
U72(tt,M,N)	→	plus(x(activate(N),activate(M)),activate(N))	(11)
isNat(n__0)	→	tt	(12)
isNat(n__plus(V1,V2))	→	U11(isNat(activate(V1)),activate(V2))	(13)
isNat(n__s(V1))	→	U21(isNat(activate(V1)))	(14)
isNat(n__x(V1,V2))	→	U31(isNat(activate(V1)),activate(V2))	(15)
plus(N,0)	→	U41(isNat(N),N)	(16)
plus(N,s(M))	→	U51(isNat(M),M,N)	(17)
x(N,0)	→	U61(isNat(N))	(18)
x(N,s(M))	→	U71(isNat(M),M,N)	(19)
0	→	n__0	(20)
plus(X1,X2)	→	n__plus(X1,X2)	(21)
s(X)	→	n__s(X)	(22)
x(X1,X2)	→	n__x(X1,X2)	(23)
activate(n__0)	→	0	(24)
activate(n__plus(X1,X2))	→	plus(X1,X2)	(25)
activate(n__s(X))	→	s(X)	(26)
activate(n__x(X1,X2))	→	x(X1,X2)	(27)
activate(X)	→	X	(28)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by NaTT @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

isNat^#(n__plus(V1,V2))	→	U11^#(isNat(activate(V1)),activate(V2))	(29)
isNat^#(n__x(V1,V2))	→	isNat^#(activate(V1))	(30)
plus^#(N,s(M))	→	isNat^#(M)	(31)
U11^#(tt,V2)	→	U12^#(isNat(activate(V2)))	(32)
U31^#(tt,V2)	→	U32^#(isNat(activate(V2)))	(33)
isNat^#(n__x(V1,V2))	→	U31^#(isNat(activate(V1)),activate(V2))	(34)
U52^#(tt,M,N)	→	activate^#(M)	(35)
U11^#(tt,V2)	→	activate^#(V2)	(36)
U31^#(tt,V2)	→	isNat^#(activate(V2))	(37)
U31^#(tt,V2)	→	activate^#(V2)	(38)
U52^#(tt,M,N)	→	s^#(plus(activate(N),activate(M)))	(39)
U61^#(tt)	→	0^#	(40)
U52^#(tt,M,N)	→	activate^#(N)	(41)
isNat^#(n__s(V1))	→	U21^#(isNat(activate(V1)))	(42)
U72^#(tt,M,N)	→	activate^#(N)	(43)
U72^#(tt,M,N)	→	activate^#(N)	(43)
U71^#(tt,M,N)	→	activate^#(N)	(44)
U71^#(tt,M,N)	→	isNat^#(activate(N))	(45)
isNat^#(n__x(V1,V2))	→	activate^#(V2)	(46)
activate^#(n__0)	→	0^#	(47)
x^#(N,s(M))	→	isNat^#(M)	(48)
isNat^#(n__s(V1))	→	isNat^#(activate(V1))	(49)
x^#(N,s(M))	→	U71^#(isNat(M),M,N)	(50)
x^#(N,0)	→	U61^#(isNat(N))	(51)
U71^#(tt,M,N)	→	activate^#(M)	(52)
U51^#(tt,M,N)	→	activate^#(M)	(53)
U72^#(tt,M,N)	→	plus^#(x(activate(N),activate(M)),activate(N))	(54)
U52^#(tt,M,N)	→	plus^#(activate(N),activate(M))	(55)
U72^#(tt,M,N)	→	activate^#(M)	(56)
plus^#(N,0)	→	U41^#(isNat(N),N)	(57)
isNat^#(n__plus(V1,V2))	→	activate^#(V2)	(58)
isNat^#(n__x(V1,V2))	→	activate^#(V1)	(59)
plus^#(N,s(M))	→	U51^#(isNat(M),M,N)	(60)
U71^#(tt,M,N)	→	U72^#(isNat(activate(N)),activate(M),activate(N))	(61)
plus^#(N,0)	→	isNat^#(N)	(62)
activate^#(n__x(X1,X2))	→	x^#(X1,X2)	(63)
U51^#(tt,M,N)	→	U52^#(isNat(activate(N)),activate(M),activate(N))	(64)
activate^#(n__s(X))	→	s^#(X)	(65)
U51^#(tt,M,N)	→	activate^#(N)	(66)
U71^#(tt,M,N)	→	activate^#(N)	(44)
U11^#(tt,V2)	→	isNat^#(activate(V2))	(67)
U51^#(tt,M,N)	→	activate^#(N)	(66)
activate^#(n__plus(X1,X2))	→	plus^#(X1,X2)	(68)
isNat^#(n__plus(V1,V2))	→	isNat^#(activate(V1))	(69)
U41^#(tt,N)	→	activate^#(N)	(70)
U72^#(tt,M,N)	→	x^#(activate(N),activate(M))	(71)
isNat^#(n__s(V1))	→	activate^#(V1)	(72)
isNat^#(n__plus(V1,V2))	→	activate^#(V1)	(73)
x^#(N,0)	→	isNat^#(N)	(74)
U51^#(tt,M,N)	→	isNat^#(activate(N))	(75)

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

U51^#(tt,M,N)	→	isNat^#(activate(N))	(75)
x^#(N,0)	→	isNat^#(N)	(74)
U71^#(tt,M,N)	→	activate^#(M)	(52)
isNat^#(n__plus(V1,V2))	→	activate^#(V1)	(73)
x^#(N,s(M))	→	U71^#(isNat(M),M,N)	(50)
isNat^#(n__s(V1))	→	isNat^#(activate(V1))	(49)
isNat^#(n__s(V1))	→	activate^#(V1)	(72)
x^#(N,s(M))	→	isNat^#(M)	(48)
U72^#(tt,M,N)	→	x^#(activate(N),activate(M))	(71)
isNat^#(n__x(V1,V2))	→	activate^#(V2)	(46)
U41^#(tt,N)	→	activate^#(N)	(70)
U71^#(tt,M,N)	→	isNat^#(activate(N))	(45)
isNat^#(n__plus(V1,V2))	→	isNat^#(activate(V1))	(69)
U71^#(tt,M,N)	→	activate^#(N)	(44)
activate^#(n__plus(X1,X2))	→	plus^#(X1,X2)	(68)
U51^#(tt,M,N)	→	activate^#(N)	(66)
U11^#(tt,V2)	→	isNat^#(activate(V2))	(67)
U71^#(tt,M,N)	→	activate^#(N)	(44)
U72^#(tt,M,N)	→	activate^#(N)	(43)
U72^#(tt,M,N)	→	activate^#(N)	(43)
U51^#(tt,M,N)	→	activate^#(N)	(66)
U51^#(tt,M,N)	→	U52^#(isNat(activate(N)),activate(M),activate(N))	(64)
U52^#(tt,M,N)	→	activate^#(N)	(41)
activate^#(n__x(X1,X2))	→	x^#(X1,X2)	(63)
plus^#(N,0)	→	isNat^#(N)	(62)
U31^#(tt,V2)	→	activate^#(V2)	(38)
U71^#(tt,M,N)	→	U72^#(isNat(activate(N)),activate(M),activate(N))	(61)
plus^#(N,s(M))	→	U51^#(isNat(M),M,N)	(60)
U31^#(tt,V2)	→	isNat^#(activate(V2))	(37)
isNat^#(n__x(V1,V2))	→	activate^#(V1)	(59)
isNat^#(n__plus(V1,V2))	→	activate^#(V2)	(58)
U11^#(tt,V2)	→	activate^#(V2)	(36)
plus^#(N,0)	→	U41^#(isNat(N),N)	(57)
U52^#(tt,M,N)	→	activate^#(M)	(35)
isNat^#(n__x(V1,V2))	→	U31^#(isNat(activate(V1)),activate(V2))	(34)
U72^#(tt,M,N)	→	activate^#(M)	(56)
U52^#(tt,M,N)	→	plus^#(activate(N),activate(M))	(55)
U72^#(tt,M,N)	→	plus^#(x(activate(N),activate(M)),activate(N))	(54)
plus^#(N,s(M))	→	isNat^#(M)	(31)
isNat^#(n__x(V1,V2))	→	isNat^#(activate(V1))	(30)
isNat^#(n__plus(V1,V2))	→	U11^#(isNat(activate(V1)),activate(V2))	(29)
U51^#(tt,M,N)	→	activate^#(M)	(53)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[0^#]	=	0
[U72^#(x₁, x₂, x₃)]	=	max(x₂ + 18590, x₃ + 0, 0)
[U32^#(x₁)]	=	0
[U21(x₁)]	=	0
[U11(x₁, x₂)]	=	max(0)
[s(x₁)]	=	x₁ + 0
[isNat^#(x₁)]	=	x₁ + 0
[activate(x₁)]	=	x₁ + 0
[U71(x₁, x₂, x₃)]	=	max(x₁ + 1, x₂ + 18590, x₃ + 0, 0)
[plus^#(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[activate^#(x₁)]	=	x₁ + 0
[U72(x₁, x₂, x₃)]	=	max(x₂ + 18590, x₃ + 0, 0)
[U52^#(x₁, x₂, x₃)]	=	max(x₂ + 0, x₃ + 0, 0)
[U12(x₁)]	=	0
[x(x₁, x₂)]	=	max(x₁ + 0, x₂ + 18590, 0)
[n__s(x₁)]	=	x₁ + 0
[U12^#(x₁)]	=	0
[0]	=	17776
[x^#(x₁, x₂)]	=	max(x₁ + 0, x₂ + 18590, 0)
[s^#(x₁)]	=	0
[n__plus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[U32(x₁)]	=	0
[n__0]	=	17776
[isNat(x₁)]	=	1
[n__x(x₁, x₂)]	=	max(x₁ + 0, x₂ + 18590, 0)
[U52(x₁, x₂, x₃)]	=	max(x₂ + 0, x₃ + 0, 0)
[plus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[U61(x₁)]	=	17776
[U51^#(x₁, x₂, x₃)]	=	max(x₂ + 0, x₃ + 0, 0)
[U11^#(x₁, x₂)]	=	max(x₂ + 0, 0)
[U31(x₁, x₂)]	=	max(0)
[U41^#(x₁, x₂)]	=	max(x₁ + 17775, x₂ + 0, 0)
[U21^#(x₁)]	=	0
[tt]	=	0
[U71^#(x₁, x₂, x₃)]	=	max(x₁ + 12457, x₂ + 18590, x₃ + 0, 0)
[U51(x₁, x₂, x₃)]	=	max(x₂ + 0, x₃ + 0, 0)
[U41(x₁, x₂)]	=	max(x₂ + 0, 0)
[U31^#(x₁, x₂)]	=	max(x₁ + 1, x₂ + 5023, 0)
[U61^#(x₁)]	=	0

together with the usable rules

x(N,0)	→	U61(isNat(N))	(18)
U31(tt,V2)	→	U32(isNat(activate(V2)))	(4)
isNat(n__x(V1,V2))	→	U31(isNat(activate(V1)),activate(V2))	(15)
U52(tt,M,N)	→	s(plus(activate(N),activate(M)))	(8)
U11(tt,V2)	→	U12(isNat(activate(V2)))	(1)
U21(tt)	→	tt	(3)
plus(N,0)	→	U41(isNat(N),N)	(16)
plus(X1,X2)	→	n__plus(X1,X2)	(21)
activate(n__s(X))	→	s(X)	(26)
x(N,s(M))	→	U71(isNat(M),M,N)	(19)
plus(N,s(M))	→	U51(isNat(M),M,N)	(17)
activate(n__x(X1,X2))	→	x(X1,X2)	(27)
s(X)	→	n__s(X)	(22)
activate(X)	→	X	(28)
U32(tt)	→	tt	(5)
U71(tt,M,N)	→	U72(isNat(activate(N)),activate(M),activate(N))	(10)
U51(tt,M,N)	→	U52(isNat(activate(N)),activate(M),activate(N))	(7)
0	→	n__0	(20)
activate(n__plus(X1,X2))	→	plus(X1,X2)	(25)
isNat(n__s(V1))	→	U21(isNat(activate(V1)))	(14)
isNat(n__0)	→	tt	(12)
x(X1,X2)	→	n__x(X1,X2)	(23)
activate(n__0)	→	0	(24)
U72(tt,M,N)	→	plus(x(activate(N),activate(M)),activate(N))	(11)
U61(tt)	→	0	(9)
isNat(n__plus(V1,V2))	→	U11(isNat(activate(V1)),activate(V2))	(13)
U41(tt,N)	→	activate(N)	(6)
U12(tt)	→	tt	(2)

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

U71^#(tt,M,N)	→	activate^#(M)	(52)
x^#(N,s(M))	→	isNat^#(M)	(48)
isNat^#(n__x(V1,V2))	→	activate^#(V2)	(46)
U31^#(tt,V2)	→	activate^#(V2)	(38)
U31^#(tt,V2)	→	isNat^#(activate(V2))	(37)
isNat^#(n__x(V1,V2))	→	U31^#(isNat(activate(V1)),activate(V2))	(34)
U72^#(tt,M,N)	→	activate^#(M)	(56)

could be deleted.

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

x^#(N,0)	→	isNat^#(N)	(74)
isNat^#(n__x(V1,V2))	→	activate^#(V1)	(59)
isNat^#(n__x(V1,V2))	→	isNat^#(activate(V1))	(30)
U52^#(tt,M,N)	→	activate^#(M)	(35)
U52^#(tt,M,N)	→	activate^#(N)	(41)
U52^#(tt,M,N)	→	plus^#(activate(N),activate(M))	(55)
U11^#(tt,V2)	→	activate^#(V2)	(36)
U11^#(tt,V2)	→	isNat^#(activate(V2))	(67)
plus^#(N,0)	→	isNat^#(N)	(62)
plus^#(N,0)	→	U41^#(isNat(N),N)	(57)
x^#(N,s(M))	→	U71^#(isNat(M),M,N)	(50)
plus^#(N,s(M))	→	isNat^#(M)	(31)
plus^#(N,s(M))	→	U51^#(isNat(M),M,N)	(60)
activate^#(n__x(X1,X2))	→	x^#(X1,X2)	(63)
U71^#(tt,M,N)	→	activate^#(N)	(44)
U71^#(tt,M,N)	→	activate^#(N)	(44)
U71^#(tt,M,N)	→	isNat^#(activate(N))	(45)
U71^#(tt,M,N)	→	U72^#(isNat(activate(N)),activate(M),activate(N))	(61)
U51^#(tt,M,N)	→	activate^#(N)	(66)
U51^#(tt,M,N)	→	activate^#(M)	(53)
U51^#(tt,M,N)	→	activate^#(N)	(66)
U51^#(tt,M,N)	→	isNat^#(activate(N))	(75)
U51^#(tt,M,N)	→	U52^#(isNat(activate(N)),activate(M),activate(N))	(64)
activate^#(n__plus(X1,X2))	→	plus^#(X1,X2)	(68)
isNat^#(n__s(V1))	→	activate^#(V1)	(72)
isNat^#(n__s(V1))	→	isNat^#(activate(V1))	(49)
U72^#(tt,M,N)	→	activate^#(N)	(43)
U72^#(tt,M,N)	→	activate^#(N)	(43)
U72^#(tt,M,N)	→	x^#(activate(N),activate(M))	(71)
U72^#(tt,M,N)	→	plus^#(x(activate(N),activate(M)),activate(N))	(54)
isNat^#(n__plus(V1,V2))	→	activate^#(V2)	(58)
isNat^#(n__plus(V1,V2))	→	activate^#(V1)	(73)
isNat^#(n__plus(V1,V2))	→	isNat^#(activate(V1))	(69)
isNat^#(n__plus(V1,V2))	→	U11^#(isNat(activate(V1)),activate(V2))	(29)
U41^#(tt,N)	→	activate^#(N)	(70)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[0^#]	=	0
[U72^#(x₁, x₂, x₃)]	=	max(x₂ + 9, x₃ + 3, 0)
[U32^#(x₁)]	=	0
[U21(x₁)]	=	0
[U11(x₁, x₂)]	=	max(0)
[s(x₁)]	=	x₁ + 0
[isNat^#(x₁)]	=	x₁ + 2
[activate(x₁)]	=	x₁ + 0
[U71(x₁, x₂, x₃)]	=	max(x₁ + 4, x₂ + 7, x₃ + 1, 0)
[plus^#(x₁, x₂)]	=	max(x₁ + 2, x₂ + 2, 0)
[activate^#(x₁)]	=	x₁ + 2
[U72(x₁, x₂, x₃)]	=	max(x₁ + 1, x₂ + 7, x₃ + 1, 0)
[U52^#(x₁, x₂, x₃)]	=	max(x₂ + 2, x₃ + 2, 0)
[U12(x₁)]	=	0
[x(x₁, x₂)]	=	max(x₁ + 1, x₂ + 7, 0)
[n__s(x₁)]	=	x₁ + 0
[U12^#(x₁)]	=	0
[0]	=	3
[x^#(x₁, x₂)]	=	max(x₁ + 3, x₂ + 9, 0)
[s^#(x₁)]	=	0
[n__plus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[U32(x₁)]	=	0
[n__0]	=	3
[isNat(x₁)]	=	3
[n__x(x₁, x₂)]	=	max(x₁ + 1, x₂ + 7, 0)
[U52(x₁, x₂, x₃)]	=	max(x₂ + 0, x₃ + 0, 0)
[plus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[U61(x₁)]	=	7
[U51^#(x₁, x₂, x₃)]	=	max(x₂ + 2, x₃ + 2, 0)
[U11^#(x₁, x₂)]	=	max(x₂ + 2, 0)
[U31(x₁, x₂)]	=	max(0)
[U41^#(x₁, x₂)]	=	max(x₁ + 1, x₂ + 2, 0)
[U21^#(x₁)]	=	0
[tt]	=	0
[U71^#(x₁, x₂, x₃)]	=	max(x₁ + 1, x₂ + 9, x₃ + 3, 0)
[U51(x₁, x₂, x₃)]	=	max(x₂ + 0, x₃ + 0, 0)
[U41(x₁, x₂)]	=	max(x₂ + 0, 0)
[U31^#(x₁, x₂)]	=	max(x₁ + 1, x₂ + 5023, 0)
[U61^#(x₁)]	=	0

together with the usable rules

x(N,0)	→	U61(isNat(N))	(18)
U31(tt,V2)	→	U32(isNat(activate(V2)))	(4)
isNat(n__x(V1,V2))	→	U31(isNat(activate(V1)),activate(V2))	(15)
U52(tt,M,N)	→	s(plus(activate(N),activate(M)))	(8)
U11(tt,V2)	→	U12(isNat(activate(V2)))	(1)
U21(tt)	→	tt	(3)
plus(N,0)	→	U41(isNat(N),N)	(16)
plus(X1,X2)	→	n__plus(X1,X2)	(21)
activate(n__s(X))	→	s(X)	(26)
x(N,s(M))	→	U71(isNat(M),M,N)	(19)
plus(N,s(M))	→	U51(isNat(M),M,N)	(17)
activate(n__x(X1,X2))	→	x(X1,X2)	(27)
s(X)	→	n__s(X)	(22)
activate(X)	→	X	(28)
U32(tt)	→	tt	(5)
U71(tt,M,N)	→	U72(isNat(activate(N)),activate(M),activate(N))	(10)
U51(tt,M,N)	→	U52(isNat(activate(N)),activate(M),activate(N))	(7)
0	→	n__0	(20)
activate(n__plus(X1,X2))	→	plus(X1,X2)	(25)
isNat(n__s(V1))	→	U21(isNat(activate(V1)))	(14)
isNat(n__0)	→	tt	(12)
x(X1,X2)	→	n__x(X1,X2)	(23)
activate(n__0)	→	0	(24)
U72(tt,M,N)	→	plus(x(activate(N),activate(M)),activate(N))	(11)
U61(tt)	→	0	(9)
isNat(n__plus(V1,V2))	→	U11(isNat(activate(V1)),activate(V2))	(13)
U41(tt,N)	→	activate(N)	(6)
U12(tt)	→	tt	(2)

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

x^#(N,0)	→	isNat^#(N)	(74)
isNat^#(n__x(V1,V2))	→	activate^#(V1)	(59)
isNat^#(n__x(V1,V2))	→	isNat^#(activate(V1))	(30)
U71^#(tt,M,N)	→	activate^#(N)	(44)
U71^#(tt,M,N)	→	activate^#(N)	(44)
U71^#(tt,M,N)	→	isNat^#(activate(N))	(45)
U72^#(tt,M,N)	→	activate^#(N)	(43)
U72^#(tt,M,N)	→	activate^#(N)	(43)

could be deleted.

1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

U52^#(tt,M,N)	→	activate^#(M)	(35)
U52^#(tt,M,N)	→	activate^#(N)	(41)
U52^#(tt,M,N)	→	plus^#(activate(N),activate(M))	(55)
U11^#(tt,V2)	→	activate^#(V2)	(36)
U11^#(tt,V2)	→	isNat^#(activate(V2))	(67)
plus^#(N,0)	→	isNat^#(N)	(62)
plus^#(N,0)	→	U41^#(isNat(N),N)	(57)
x^#(N,s(M))	→	U71^#(isNat(M),M,N)	(50)
plus^#(N,s(M))	→	isNat^#(M)	(31)
plus^#(N,s(M))	→	U51^#(isNat(M),M,N)	(60)
activate^#(n__x(X1,X2))	→	x^#(X1,X2)	(63)
U71^#(tt,M,N)	→	U72^#(isNat(activate(N)),activate(M),activate(N))	(61)
U51^#(tt,M,N)	→	activate^#(N)	(66)
U51^#(tt,M,N)	→	activate^#(M)	(53)
U51^#(tt,M,N)	→	activate^#(N)	(66)
U51^#(tt,M,N)	→	isNat^#(activate(N))	(75)
U51^#(tt,M,N)	→	U52^#(isNat(activate(N)),activate(M),activate(N))	(64)
activate^#(n__plus(X1,X2))	→	plus^#(X1,X2)	(68)
isNat^#(n__s(V1))	→	activate^#(V1)	(72)
isNat^#(n__s(V1))	→	isNat^#(activate(V1))	(49)
U72^#(tt,M,N)	→	x^#(activate(N),activate(M))	(71)
U72^#(tt,M,N)	→	plus^#(x(activate(N),activate(M)),activate(N))	(54)
isNat^#(n__plus(V1,V2))	→	activate^#(V2)	(58)
isNat^#(n__plus(V1,V2))	→	activate^#(V1)	(73)
isNat^#(n__plus(V1,V2))	→	isNat^#(activate(V1))	(69)
isNat^#(n__plus(V1,V2))	→	U11^#(isNat(activate(V1)),activate(V2))	(29)
U41^#(tt,N)	→	activate^#(N)	(70)

1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[0^#]	=	0
[U72^#(x₁, x₂, x₃)]	=	max(x₁ + 3580, x₃ + 3583, 0)
[U32^#(x₁)]	=	0
[U21(x₁)]	=	0
[U11(x₁, x₂)]	=	max(0)
[s(x₁)]	=	x₁ + 0
[isNat^#(x₁)]	=	x₁ + 0
[activate(x₁)]	=	x₁ + 0
[U71(x₁, x₂, x₃)]	=	max(x₃ + 3583, 0)
[plus^#(x₁, x₂)]	=	max(x₁ + 0, x₂ + 2, 0)
[activate^#(x₁)]	=	x₁ + 0
[U72(x₁, x₂, x₃)]	=	max(x₃ + 3583, 0)
[U52^#(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 2, x₃ + 0, 0)
[U12(x₁)]	=	0
[x(x₁, x₂)]	=	max(x₁ + 3583, 0)
[n__s(x₁)]	=	x₁ + 0
[U12^#(x₁)]	=	0
[0]	=	3471
[x^#(x₁, x₂)]	=	max(x₁ + 3583, 0)
[s^#(x₁)]	=	0
[n__plus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 1725, 0)
[U32(x₁)]	=	0
[n__0]	=	3471
[isNat(x₁)]	=	2
[n__x(x₁, x₂)]	=	max(x₁ + 3583, 0)
[U52(x₁, x₂, x₃)]	=	max(x₁ + 153, x₂ + 1725, x₃ + 0, 0)
[plus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 1725, 0)
[U61(x₁)]	=	3471
[U51^#(x₁, x₂, x₃)]	=	max(x₂ + 2, x₃ + 0, 0)
[U11^#(x₁, x₂)]	=	max(x₁ + 1722, x₂ + 713, 0)
[U31(x₁, x₂)]	=	max(x₁ + 0, 0)
[U41^#(x₁, x₂)]	=	max(x₁ + 3471, x₂ + 0, 0)
[U21^#(x₁)]	=	0
[tt]	=	0
[U71^#(x₁, x₂, x₃)]	=	max(x₁ + 3581, x₃ + 3583, 0)
[U51(x₁, x₂, x₃)]	=	max(x₂ + 1725, x₃ + 0, 0)
[U41(x₁, x₂)]	=	max(x₂ + 0, 0)
[U31^#(x₁, x₂)]	=	max(0)
[U61^#(x₁)]	=	0

together with the usable rules

x(N,0)	→	U61(isNat(N))	(18)
U31(tt,V2)	→	U32(isNat(activate(V2)))	(4)
isNat(n__x(V1,V2))	→	U31(isNat(activate(V1)),activate(V2))	(15)
U52(tt,M,N)	→	s(plus(activate(N),activate(M)))	(8)
U11(tt,V2)	→	U12(isNat(activate(V2)))	(1)
U21(tt)	→	tt	(3)
plus(N,0)	→	U41(isNat(N),N)	(16)
plus(X1,X2)	→	n__plus(X1,X2)	(21)
activate(n__s(X))	→	s(X)	(26)
x(N,s(M))	→	U71(isNat(M),M,N)	(19)
plus(N,s(M))	→	U51(isNat(M),M,N)	(17)
activate(n__x(X1,X2))	→	x(X1,X2)	(27)
s(X)	→	n__s(X)	(22)
activate(X)	→	X	(28)
U32(tt)	→	tt	(5)
U71(tt,M,N)	→	U72(isNat(activate(N)),activate(M),activate(N))	(10)
U51(tt,M,N)	→	U52(isNat(activate(N)),activate(M),activate(N))	(7)
0	→	n__0	(20)
activate(n__plus(X1,X2))	→	plus(X1,X2)	(25)
isNat(n__s(V1))	→	U21(isNat(activate(V1)))	(14)
isNat(n__0)	→	tt	(12)
x(X1,X2)	→	n__x(X1,X2)	(23)
activate(n__0)	→	0	(24)
U72(tt,M,N)	→	plus(x(activate(N),activate(M)),activate(N))	(11)
U61(tt)	→	0	(9)
isNat(n__plus(V1,V2))	→	U11(isNat(activate(V1)),activate(V2))	(13)
U41(tt,N)	→	activate(N)	(6)
U12(tt)	→	tt	(2)

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

U52^#(tt,M,N)	→	activate^#(M)	(35)
U11^#(tt,V2)	→	activate^#(V2)	(36)
U11^#(tt,V2)	→	isNat^#(activate(V2))	(67)
plus^#(N,s(M))	→	isNat^#(M)	(31)
U51^#(tt,M,N)	→	activate^#(M)	(53)
isNat^#(n__plus(V1,V2))	→	activate^#(V2)	(58)
isNat^#(n__plus(V1,V2))	→	U11^#(isNat(activate(V1)),activate(V2))	(29)

could be deleted.

1.1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

U52^#(tt,M,N)	→	activate^#(N)	(41)
U52^#(tt,M,N)	→	plus^#(activate(N),activate(M))	(55)
plus^#(N,0)	→	isNat^#(N)	(62)
plus^#(N,0)	→	U41^#(isNat(N),N)	(57)
x^#(N,s(M))	→	U71^#(isNat(M),M,N)	(50)
plus^#(N,s(M))	→	U51^#(isNat(M),M,N)	(60)
activate^#(n__x(X1,X2))	→	x^#(X1,X2)	(63)
U71^#(tt,M,N)	→	U72^#(isNat(activate(N)),activate(M),activate(N))	(61)
U51^#(tt,M,N)	→	activate^#(N)	(66)
U51^#(tt,M,N)	→	activate^#(N)	(66)
U51^#(tt,M,N)	→	isNat^#(activate(N))	(75)
U51^#(tt,M,N)	→	U52^#(isNat(activate(N)),activate(M),activate(N))	(64)
activate^#(n__plus(X1,X2))	→	plus^#(X1,X2)	(68)
isNat^#(n__s(V1))	→	activate^#(V1)	(72)
isNat^#(n__s(V1))	→	isNat^#(activate(V1))	(49)
U72^#(tt,M,N)	→	x^#(activate(N),activate(M))	(71)
U72^#(tt,M,N)	→	plus^#(x(activate(N),activate(M)),activate(N))	(54)
isNat^#(n__plus(V1,V2))	→	activate^#(V1)	(73)
isNat^#(n__plus(V1,V2))	→	isNat^#(activate(V1))	(69)
U41^#(tt,N)	→	activate^#(N)	(70)

1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the argument filter

π(isNat^#)	=	1
π(activate)	=	1
π(plus^#)	=	1
π(activate^#)	=	1
π(U52^#)	=	3
π(U12)	=	1
π(U32)	=	1
π(U61)	=	1
π(U51^#)	=	3
π(U41^#)	=	2
π(U31^#)	=	1

in combination with the following Weighted Path Order with the following precedence and status

prec(0^#)	=	0	status(0^#)	=	[]	list-extension(0^#)	=	Lex
prec(U72^#)	=	7	status(U72^#)	=	[3, 2]	list-extension(U72^#)	=	Lex
prec(U32^#)	=	0	status(U32^#)	=	[]	list-extension(U32^#)	=	Lex
prec(U21)	=	3	status(U21)	=	[]	list-extension(U21)	=	Lex
prec(U11)	=	3	status(U11)	=	[]	list-extension(U11)	=	Lex
prec(s)	=	4	status(s)	=	[1]	list-extension(s)	=	Lex
prec(U71)	=	7	status(U71)	=	[3, 2, 1]	list-extension(U71)	=	Lex
prec(U72)	=	7	status(U72)	=	[3, 2, 1]	list-extension(U72)	=	Lex
prec(x)	=	7	status(x)	=	[1, 2]	list-extension(x)	=	Lex
prec(n__s)	=	4	status(n__s)	=	[1]	list-extension(n__s)	=	Lex
prec(U12^#)	=	0	status(U12^#)	=	[]	list-extension(U12^#)	=	Lex
prec(0)	=	2	status(0)	=	[]	list-extension(0)	=	Lex
prec(x^#)	=	7	status(x^#)	=	[1, 2]	list-extension(x^#)	=	Lex
prec(s^#)	=	0	status(s^#)	=	[]	list-extension(s^#)	=	Lex
prec(n__plus)	=	6	status(n__plus)	=	[2, 1]	list-extension(n__plus)	=	Lex
prec(n__0)	=	2	status(n__0)	=	[]	list-extension(n__0)	=	Lex
prec(isNat)	=	3	status(isNat)	=	[]	list-extension(isNat)	=	Lex
prec(n__x)	=	7	status(n__x)	=	[1, 2]	list-extension(n__x)	=	Lex
prec(U52)	=	6	status(U52)	=	[2, 3, 1]	list-extension(U52)	=	Lex
prec(plus)	=	6	status(plus)	=	[2, 1]	list-extension(plus)	=	Lex
prec(U11^#)	=	0	status(U11^#)	=	[]	list-extension(U11^#)	=	Lex
prec(U31)	=	3	status(U31)	=	[]	list-extension(U31)	=	Lex
prec(U21^#)	=	0	status(U21^#)	=	[]	list-extension(U21^#)	=	Lex
prec(tt)	=	3	status(tt)	=	[]	list-extension(tt)	=	Lex
prec(U71^#)	=	7	status(U71^#)	=	[3, 2, 1]	list-extension(U71^#)	=	Lex
prec(U51)	=	6	status(U51)	=	[2, 3, 1]	list-extension(U51)	=	Lex
prec(U41)	=	0	status(U41)	=	[1, 2]	list-extension(U41)	=	Lex
prec(U61^#)	=	0	status(U61^#)	=	[]	list-extension(U61^#)	=	Lex

and the following Max-polynomial interpretation

[0^#]	=	0
[U72^#(x₁, x₂, x₃)]	=	max(x₂ + 0, x₃ + 0, 0)
[U32^#(x₁)]	=	0
[U21(x₁)]	=	0
[U11(x₁, x₂)]	=	max(0)
[s(x₁)]	=	x₁ + 0
[U71(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 0, 0)
[U72(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 0, 0)
[x(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[n__s(x₁)]	=	x₁ + 0
[U12^#(x₁)]	=	0
[0]	=	0
[x^#(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[s^#(x₁)]	=	0
[n__plus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[n__0]	=	0
[isNat(x₁)]	=	0
[n__x(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[U52(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 0, 0)
[plus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[U11^#(x₁, x₂)]	=	max(0)
[U31(x₁, x₂)]	=	max(0)
[U21^#(x₁)]	=	0
[tt]	=	0
[U71^#(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 0, 0)
[U51(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 0, 0)
[U41(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[U61^#(x₁)]	=	0

together with the usable rules

x(N,0)	→	U61(isNat(N))	(18)
U31(tt,V2)	→	U32(isNat(activate(V2)))	(4)
isNat(n__x(V1,V2))	→	U31(isNat(activate(V1)),activate(V2))	(15)
U52(tt,M,N)	→	s(plus(activate(N),activate(M)))	(8)
U11(tt,V2)	→	U12(isNat(activate(V2)))	(1)
U21(tt)	→	tt	(3)
plus(N,0)	→	U41(isNat(N),N)	(16)
plus(X1,X2)	→	n__plus(X1,X2)	(21)
activate(n__s(X))	→	s(X)	(26)
x(N,s(M))	→	U71(isNat(M),M,N)	(19)
plus(N,s(M))	→	U51(isNat(M),M,N)	(17)
activate(n__x(X1,X2))	→	x(X1,X2)	(27)
s(X)	→	n__s(X)	(22)
activate(X)	→	X	(28)
U32(tt)	→	tt	(5)
U71(tt,M,N)	→	U72(isNat(activate(N)),activate(M),activate(N))	(10)
U51(tt,M,N)	→	U52(isNat(activate(N)),activate(M),activate(N))	(7)
0	→	n__0	(20)
activate(n__plus(X1,X2))	→	plus(X1,X2)	(25)
isNat(n__s(V1))	→	U21(isNat(activate(V1)))	(14)
isNat(n__0)	→	tt	(12)
x(X1,X2)	→	n__x(X1,X2)	(23)
activate(n__0)	→	0	(24)
U72(tt,M,N)	→	plus(x(activate(N),activate(M)),activate(N))	(11)
U61(tt)	→	0	(9)
isNat(n__plus(V1,V2))	→	U11(isNat(activate(V1)),activate(V2))	(13)
U41(tt,N)	→	activate(N)	(6)
U12(tt)	→	tt	(2)

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

x^#(N,s(M))	→	U71^#(isNat(M),M,N)	(50)
U71^#(tt,M,N)	→	U72^#(isNat(activate(N)),activate(M),activate(N))	(61)
activate^#(n__plus(X1,X2))	→	plus^#(X1,X2)	(68)
isNat^#(n__s(V1))	→	activate^#(V1)	(72)
isNat^#(n__s(V1))	→	isNat^#(activate(V1))	(49)
isNat^#(n__plus(V1,V2))	→	activate^#(V1)	(73)
isNat^#(n__plus(V1,V2))	→	isNat^#(activate(V1))	(69)

could be deleted.

1.1.1.1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

U52^#(tt,M,N)	→	plus^#(activate(N),activate(M))	(55)
plus^#(N,s(M))	→	U51^#(isNat(M),M,N)	(60)
U51^#(tt,M,N)	→	U52^#(isNat(activate(N)),activate(M),activate(N))	(64)

1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the argument filter

π(isNat^#)	=	1
π(activate)	=	1
π(activate^#)	=	1
π(U12)	=	1
π(U32)	=	1
π(U61)	=	1
π(U41^#)	=	2
π(U31^#)	=	1

in combination with the following Weighted Path Order with the following precedence and status

prec(0^#)	=	0	status(0^#)	=	[]	list-extension(0^#)	=	Lex
prec(U72^#)	=	7	status(U72^#)	=	[3, 2]	list-extension(U72^#)	=	Lex
prec(U32^#)	=	0	status(U32^#)	=	[]	list-extension(U32^#)	=	Lex
prec(U21)	=	2	status(U21)	=	[]	list-extension(U21)	=	Lex
prec(U11)	=	2	status(U11)	=	[]	list-extension(U11)	=	Lex
prec(s)	=	3	status(s)	=	[1]	list-extension(s)	=	Lex
prec(U71)	=	7	status(U71)	=	[3, 2, 1]	list-extension(U71)	=	Lex
prec(plus^#)	=	4	status(plus^#)	=	[2, 1]	list-extension(plus^#)	=	Lex
prec(U72)	=	7	status(U72)	=	[3, 2, 1]	list-extension(U72)	=	Lex
prec(U52^#)	=	4	status(U52^#)	=	[2, 3]	list-extension(U52^#)	=	Lex
prec(x)	=	7	status(x)	=	[1, 2]	list-extension(x)	=	Lex
prec(n__s)	=	3	status(n__s)	=	[1]	list-extension(n__s)	=	Lex
prec(U12^#)	=	0	status(U12^#)	=	[]	list-extension(U12^#)	=	Lex
prec(0)	=	1	status(0)	=	[]	list-extension(0)	=	Lex
prec(x^#)	=	7	status(x^#)	=	[1, 2]	list-extension(x^#)	=	Lex
prec(s^#)	=	0	status(s^#)	=	[]	list-extension(s^#)	=	Lex
prec(n__plus)	=	6	status(n__plus)	=	[2, 1]	list-extension(n__plus)	=	Lex
prec(n__0)	=	1	status(n__0)	=	[]	list-extension(n__0)	=	Lex
prec(isNat)	=	2	status(isNat)	=	[]	list-extension(isNat)	=	Lex
prec(n__x)	=	7	status(n__x)	=	[1, 2]	list-extension(n__x)	=	Lex
prec(U52)	=	6	status(U52)	=	[2, 3, 1]	list-extension(U52)	=	Lex
prec(plus)	=	6	status(plus)	=	[2, 1]	list-extension(plus)	=	Lex
prec(U51^#)	=	4	status(U51^#)	=	[2, 3]	list-extension(U51^#)	=	Lex
prec(U11^#)	=	0	status(U11^#)	=	[]	list-extension(U11^#)	=	Lex
prec(U31)	=	2	status(U31)	=	[]	list-extension(U31)	=	Lex
prec(U21^#)	=	0	status(U21^#)	=	[]	list-extension(U21^#)	=	Lex
prec(tt)	=	2	status(tt)	=	[]	list-extension(tt)	=	Lex
prec(U71^#)	=	7	status(U71^#)	=	[3, 2, 1]	list-extension(U71^#)	=	Lex
prec(U51)	=	6	status(U51)	=	[2, 3, 1]	list-extension(U51)	=	Lex
prec(U41)	=	0	status(U41)	=	[1, 2]	list-extension(U41)	=	Lex
prec(U61^#)	=	0	status(U61^#)	=	[]	list-extension(U61^#)	=	Lex

and the following Max-polynomial interpretation

[0^#]	=	0
[U72^#(x₁, x₂, x₃)]	=	max(x₂ + 0, x₃ + 0, 0)
[U32^#(x₁)]	=	0
[U21(x₁)]	=	0
[U11(x₁, x₂)]	=	max(0)
[s(x₁)]	=	x₁ + 0
[U71(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 0, 0)
[plus^#(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[U72(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 0, 0)
[U52^#(x₁, x₂, x₃)]	=	max(x₂ + 0, x₃ + 0, 0)
[x(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[n__s(x₁)]	=	x₁ + 0
[U12^#(x₁)]	=	0
[0]	=	0
[x^#(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[s^#(x₁)]	=	0
[n__plus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[n__0]	=	0
[isNat(x₁)]	=	0
[n__x(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[U52(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 0, 0)
[plus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[U51^#(x₁, x₂, x₃)]	=	max(x₂ + 0, x₃ + 0, 0)
[U11^#(x₁, x₂)]	=	max(0)
[U31(x₁, x₂)]	=	max(0)
[U21^#(x₁)]	=	0
[tt]	=	0
[U71^#(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 0, 0)
[U51(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 0, 0)
[U41(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[U61^#(x₁)]	=	0

together with the usable rules

x(N,0)	→	U61(isNat(N))	(18)
U31(tt,V2)	→	U32(isNat(activate(V2)))	(4)
isNat(n__x(V1,V2))	→	U31(isNat(activate(V1)),activate(V2))	(15)
U52(tt,M,N)	→	s(plus(activate(N),activate(M)))	(8)
U11(tt,V2)	→	U12(isNat(activate(V2)))	(1)
U21(tt)	→	tt	(3)
plus(N,0)	→	U41(isNat(N),N)	(16)
plus(X1,X2)	→	n__plus(X1,X2)	(21)
activate(n__s(X))	→	s(X)	(26)
x(N,s(M))	→	U71(isNat(M),M,N)	(19)
plus(N,s(M))	→	U51(isNat(M),M,N)	(17)
activate(n__x(X1,X2))	→	x(X1,X2)	(27)
s(X)	→	n__s(X)	(22)
activate(X)	→	X	(28)
U32(tt)	→	tt	(5)
U71(tt,M,N)	→	U72(isNat(activate(N)),activate(M),activate(N))	(10)
U51(tt,M,N)	→	U52(isNat(activate(N)),activate(M),activate(N))	(7)
0	→	n__0	(20)
activate(n__plus(X1,X2))	→	plus(X1,X2)	(25)
isNat(n__s(V1))	→	U21(isNat(activate(V1)))	(14)
isNat(n__0)	→	tt	(12)
x(X1,X2)	→	n__x(X1,X2)	(23)
activate(n__0)	→	0	(24)
U72(tt,M,N)	→	plus(x(activate(N),activate(M)),activate(N))	(11)
U61(tt)	→	0	(9)
isNat(n__plus(V1,V2))	→	U11(isNat(activate(V1)),activate(V2))	(13)
U41(tt,N)	→	activate(N)	(6)
U12(tt)	→	tt	(2)

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

plus^#(N,s(M))

→

U51^#(isNat(M),M,N)

(60)

could be deleted.

1.1.1.1.1.1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.