Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/MYNAT_nokinds_Z)

The rewrite relation of the following TRS is considered.

U11(tt,N)	→	activate(N)	(1)
U21(tt,M,N)	→	s(plus(activate(N),activate(M)))	(2)
U31(tt)	→	0	(3)
U41(tt,M,N)	→	plus(x(activate(N),activate(M)),activate(N))	(4)
and(tt,X)	→	activate(X)	(5)
isNat(n__0)	→	tt	(6)
isNat(n__plus(V1,V2))	→	and(isNat(activate(V1)),n__isNat(activate(V2)))	(7)
isNat(n__s(V1))	→	isNat(activate(V1))	(8)
isNat(n__x(V1,V2))	→	and(isNat(activate(V1)),n__isNat(activate(V2)))	(9)
plus(N,0)	→	U11(isNat(N),N)	(10)
plus(N,s(M))	→	U21(and(isNat(M),n__isNat(N)),M,N)	(11)
x(N,0)	→	U31(isNat(N))	(12)
x(N,s(M))	→	U41(and(isNat(M),n__isNat(N)),M,N)	(13)
0	→	n__0	(14)
plus(X1,X2)	→	n__plus(X1,X2)	(15)
isNat(X)	→	n__isNat(X)	(16)
s(X)	→	n__s(X)	(17)
x(X1,X2)	→	n__x(X1,X2)	(18)
activate(n__0)	→	0	(19)
activate(n__plus(X1,X2))	→	plus(X1,X2)	(20)
activate(n__isNat(X))	→	isNat(X)	(21)
activate(n__s(X))	→	s(X)	(22)
activate(n__x(X1,X2))	→	x(X1,X2)	(23)
activate(X)	→	X	(24)

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.

U21^#(tt,M,N)	→	plus^#(activate(N),activate(M))	(25)
U31^#(tt)	→	0^#	(26)
U41^#(tt,M,N)	→	activate^#(N)	(27)
U41^#(tt,M,N)	→	activate^#(N)	(27)
x^#(N,s(M))	→	and^#(isNat(M),n__isNat(N))	(28)
plus^#(N,s(M))	→	and^#(isNat(M),n__isNat(N))	(29)
isNat^#(n__x(V1,V2))	→	isNat^#(activate(V1))	(30)
isNat^#(n__x(V1,V2))	→	activate^#(V2)	(31)
plus^#(N,0)	→	isNat^#(N)	(32)
plus^#(N,0)	→	U11^#(isNat(N),N)	(33)
plus^#(N,s(M))	→	U21^#(and(isNat(M),n__isNat(N)),M,N)	(34)
isNat^#(n__s(V1))	→	isNat^#(activate(V1))	(35)
plus^#(N,s(M))	→	isNat^#(M)	(36)
U11^#(tt,N)	→	activate^#(N)	(37)
and^#(tt,X)	→	activate^#(X)	(38)
isNat^#(n__plus(V1,V2))	→	isNat^#(activate(V1))	(39)
x^#(N,s(M))	→	isNat^#(M)	(40)
isNat^#(n__x(V1,V2))	→	activate^#(V1)	(41)
U41^#(tt,M,N)	→	plus^#(x(activate(N),activate(M)),activate(N))	(42)
x^#(N,s(M))	→	U41^#(and(isNat(M),n__isNat(N)),M,N)	(43)
activate^#(n__isNat(X))	→	isNat^#(X)	(44)
isNat^#(n__plus(V1,V2))	→	activate^#(V2)	(45)
U41^#(tt,M,N)	→	x^#(activate(N),activate(M))	(46)
activate^#(n__0)	→	0^#	(47)
x^#(N,0)	→	isNat^#(N)	(48)
isNat^#(n__s(V1))	→	activate^#(V1)	(49)
isNat^#(n__plus(V1,V2))	→	and^#(isNat(activate(V1)),n__isNat(activate(V2)))	(50)
activate^#(n__s(X))	→	s^#(X)	(51)
U41^#(tt,M,N)	→	activate^#(M)	(52)
isNat^#(n__plus(V1,V2))	→	activate^#(V1)	(53)
x^#(N,0)	→	U31^#(isNat(N))	(54)
U21^#(tt,M,N)	→	activate^#(N)	(55)
U21^#(tt,M,N)	→	s^#(plus(activate(N),activate(M)))	(56)
isNat^#(n__x(V1,V2))	→	and^#(isNat(activate(V1)),n__isNat(activate(V2)))	(57)
activate^#(n__x(X1,X2))	→	x^#(X1,X2)	(58)
U21^#(tt,M,N)	→	activate^#(M)	(59)
activate^#(n__plus(X1,X2))	→	plus^#(X1,X2)	(60)

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

activate^#(n__plus(X1,X2))	→	plus^#(X1,X2)	(60)
and^#(tt,X)	→	activate^#(X)	(38)
U21^#(tt,M,N)	→	activate^#(M)	(59)
U11^#(tt,N)	→	activate^#(N)	(37)
plus^#(N,s(M))	→	isNat^#(M)	(36)
activate^#(n__x(X1,X2))	→	x^#(X1,X2)	(58)
isNat^#(n__s(V1))	→	isNat^#(activate(V1))	(35)
plus^#(N,s(M))	→	U21^#(and(isNat(M),n__isNat(N)),M,N)	(34)
isNat^#(n__x(V1,V2))	→	and^#(isNat(activate(V1)),n__isNat(activate(V2)))	(57)
plus^#(N,0)	→	U11^#(isNat(N),N)	(33)
U21^#(tt,M,N)	→	activate^#(N)	(55)
plus^#(N,0)	→	isNat^#(N)	(32)
isNat^#(n__plus(V1,V2))	→	activate^#(V1)	(53)
U41^#(tt,M,N)	→	activate^#(M)	(52)
isNat^#(n__x(V1,V2))	→	activate^#(V2)	(31)
isNat^#(n__x(V1,V2))	→	isNat^#(activate(V1))	(30)
plus^#(N,s(M))	→	and^#(isNat(M),n__isNat(N))	(29)
isNat^#(n__s(V1))	→	activate^#(V1)	(49)
isNat^#(n__plus(V1,V2))	→	and^#(isNat(activate(V1)),n__isNat(activate(V2)))	(50)
x^#(N,0)	→	isNat^#(N)	(48)
x^#(N,s(M))	→	and^#(isNat(M),n__isNat(N))	(28)
U41^#(tt,M,N)	→	x^#(activate(N),activate(M))	(46)
isNat^#(n__plus(V1,V2))	→	activate^#(V2)	(45)
activate^#(n__isNat(X))	→	isNat^#(X)	(44)
x^#(N,s(M))	→	U41^#(and(isNat(M),n__isNat(N)),M,N)	(43)
U41^#(tt,M,N)	→	activate^#(N)	(27)
U41^#(tt,M,N)	→	plus^#(x(activate(N),activate(M)),activate(N))	(42)
isNat^#(n__x(V1,V2))	→	activate^#(V1)	(41)
x^#(N,s(M))	→	isNat^#(M)	(40)
U41^#(tt,M,N)	→	activate^#(N)	(27)
U21^#(tt,M,N)	→	plus^#(activate(N),activate(M))	(25)
isNat^#(n__plus(V1,V2))	→	isNat^#(activate(V1))	(39)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[0^#]	=	0
[U21(x₁, x₂, x₃)]	=	max(x₂ + 841, x₃ + 0, 0)
[U11(x₁, x₂)]	=	max(x₂ + 0, 0)
[s(x₁)]	=	x₁ + 0
[isNat^#(x₁)]	=	x₁ + 0
[activate(x₁)]	=	x₁ + 0
[and(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[plus^#(x₁, x₂)]	=	max(x₁ + 0, x₂ + 841, 0)
[activate^#(x₁)]	=	x₁ + 0
[x(x₁, x₂)]	=	max(x₁ + 841, x₂ + 0, 0)
[n__s(x₁)]	=	x₁ + 0
[0]	=	842
[x^#(x₁, x₂)]	=	max(x₁ + 841, x₂ + 0, 0)
[s^#(x₁)]	=	0
[n__isNat(x₁)]	=	x₁ + 0
[n__plus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 841, 0)
[n__0]	=	842
[isNat(x₁)]	=	x₁ + 0
[n__x(x₁, x₂)]	=	max(x₁ + 841, x₂ + 0, 0)
[plus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 841, 0)
[U11^#(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[U31(x₁)]	=	842
[U41^#(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 841, 0)
[U21^#(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 841, x₃ + 0, 0)
[tt]	=	842
[U41(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 841, 0)
[U31^#(x₁)]	=	0
[and^#(x₁, x₂)]	=	max(x₂ + 0, 0)

together with the usable rules

x(X1,X2)	→	n__x(X1,X2)	(18)
U41(tt,M,N)	→	plus(x(activate(N),activate(M)),activate(N))	(4)
plus(X1,X2)	→	n__plus(X1,X2)	(15)
isNat(n__s(V1))	→	isNat(activate(V1))	(8)
U11(tt,N)	→	activate(N)	(1)
U31(tt)	→	0	(3)
isNat(X)	→	n__isNat(X)	(16)
activate(n__isNat(X))	→	isNat(X)	(21)
activate(n__0)	→	0	(19)
s(X)	→	n__s(X)	(17)
activate(n__s(X))	→	s(X)	(22)
and(tt,X)	→	activate(X)	(5)
plus(N,0)	→	U11(isNat(N),N)	(10)
isNat(n__plus(V1,V2))	→	and(isNat(activate(V1)),n__isNat(activate(V2)))	(7)
activate(n__plus(X1,X2))	→	plus(X1,X2)	(20)
0	→	n__0	(14)
x(N,0)	→	U31(isNat(N))	(12)
activate(n__x(X1,X2))	→	x(X1,X2)	(23)
activate(X)	→	X	(24)
plus(N,s(M))	→	U21(and(isNat(M),n__isNat(N)),M,N)	(11)
isNat(n__x(V1,V2))	→	and(isNat(activate(V1)),n__isNat(activate(V2)))	(9)
x(N,s(M))	→	U41(and(isNat(M),n__isNat(N)),M,N)	(13)
isNat(n__0)	→	tt	(6)
U21(tt,M,N)	→	s(plus(activate(N),activate(M)))	(2)

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

U21^#(tt,M,N)	→	activate^#(M)	(59)
plus^#(N,s(M))	→	isNat^#(M)	(36)
isNat^#(n__x(V1,V2))	→	isNat^#(activate(V1))	(30)
isNat^#(n__plus(V1,V2))	→	and^#(isNat(activate(V1)),n__isNat(activate(V2)))	(50)
x^#(N,0)	→	isNat^#(N)	(48)
x^#(N,s(M))	→	and^#(isNat(M),n__isNat(N))	(28)
isNat^#(n__plus(V1,V2))	→	activate^#(V2)	(45)
U41^#(tt,M,N)	→	activate^#(N)	(27)
isNat^#(n__x(V1,V2))	→	activate^#(V1)	(41)
U41^#(tt,M,N)	→	activate^#(N)	(27)

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

U41^#(tt,M,N)	→	activate^#(M)	(52)
U41^#(tt,M,N)	→	x^#(activate(N),activate(M))	(46)
U41^#(tt,M,N)	→	plus^#(x(activate(N),activate(M)),activate(N))	(42)
isNat^#(n__s(V1))	→	activate^#(V1)	(49)
isNat^#(n__s(V1))	→	isNat^#(activate(V1))	(35)
U11^#(tt,N)	→	activate^#(N)	(37)
activate^#(n__isNat(X))	→	isNat^#(X)	(44)
and^#(tt,X)	→	activate^#(X)	(38)
plus^#(N,0)	→	isNat^#(N)	(32)
plus^#(N,0)	→	U11^#(isNat(N),N)	(33)
isNat^#(n__plus(V1,V2))	→	activate^#(V1)	(53)
isNat^#(n__plus(V1,V2))	→	isNat^#(activate(V1))	(39)
activate^#(n__plus(X1,X2))	→	plus^#(X1,X2)	(60)
activate^#(n__x(X1,X2))	→	x^#(X1,X2)	(58)
plus^#(N,s(M))	→	and^#(isNat(M),n__isNat(N))	(29)
plus^#(N,s(M))	→	U21^#(and(isNat(M),n__isNat(N)),M,N)	(34)
isNat^#(n__x(V1,V2))	→	activate^#(V2)	(31)
isNat^#(n__x(V1,V2))	→	and^#(isNat(activate(V1)),n__isNat(activate(V2)))	(57)
x^#(N,s(M))	→	isNat^#(M)	(40)
x^#(N,s(M))	→	U41^#(and(isNat(M),n__isNat(N)),M,N)	(43)
U21^#(tt,M,N)	→	activate^#(N)	(55)
U21^#(tt,M,N)	→	plus^#(activate(N),activate(M))	(25)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[0^#]	=	0
[U21(x₁, x₂, x₃)]	=	max(x₂ + 1, x₃ + 0, 0)
[U11(x₁, x₂)]	=	max(x₂ + 0, 0)
[s(x₁)]	=	x₁ + 0
[isNat^#(x₁)]	=	x₁ + 41635
[activate(x₁)]	=	x₁ + 0
[and(x₁, x₂)]	=	max(x₂ + 0, 0)
[plus^#(x₁, x₂)]	=	max(x₁ + 41635, x₂ + 35325, 0)
[activate^#(x₁)]	=	x₁ + 41635
[x(x₁, x₂)]	=	max(x₁ + 3155, x₂ + 3155, 0)
[n__s(x₁)]	=	x₁ + 0
[0]	=	3154
[x^#(x₁, x₂)]	=	max(x₁ + 44790, x₂ + 44790, 0)
[s^#(x₁)]	=	0
[n__isNat(x₁)]	=	x₁ + 0
[n__plus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 1, 0)
[n__0]	=	3154
[isNat(x₁)]	=	x₁ + 0
[n__x(x₁, x₂)]	=	max(x₁ + 3155, x₂ + 3155, 0)
[plus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 1, 0)
[U11^#(x₁, x₂)]	=	max(x₁ + 38480, x₂ + 41635, 0)
[U31(x₁)]	=	x₁ + 3155
[U41^#(x₁, x₂, x₃)]	=	max(x₁ + 44790, x₂ + 44790, x₃ + 44790, 0)
[U21^#(x₁, x₂, x₃)]	=	max(x₁ + 41634, x₂ + 35325, x₃ + 41635, 0)
[tt]	=	3154
[U41(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 3155, x₃ + 3155, 0)
[U31^#(x₁)]	=	0
[and^#(x₁, x₂)]	=	max(x₁ + 35324, x₂ + 41635, 0)

together with the usable rules

x(X1,X2)	→	n__x(X1,X2)	(18)
U41(tt,M,N)	→	plus(x(activate(N),activate(M)),activate(N))	(4)
plus(X1,X2)	→	n__plus(X1,X2)	(15)
isNat(n__s(V1))	→	isNat(activate(V1))	(8)
U11(tt,N)	→	activate(N)	(1)
U31(tt)	→	0	(3)
isNat(X)	→	n__isNat(X)	(16)
activate(n__isNat(X))	→	isNat(X)	(21)
activate(n__0)	→	0	(19)
s(X)	→	n__s(X)	(17)
activate(n__s(X))	→	s(X)	(22)
and(tt,X)	→	activate(X)	(5)
plus(N,0)	→	U11(isNat(N),N)	(10)
isNat(n__plus(V1,V2))	→	and(isNat(activate(V1)),n__isNat(activate(V2)))	(7)
activate(n__plus(X1,X2))	→	plus(X1,X2)	(20)
0	→	n__0	(14)
x(N,0)	→	U31(isNat(N))	(12)
activate(n__x(X1,X2))	→	x(X1,X2)	(23)
activate(X)	→	X	(24)
plus(N,s(M))	→	U21(and(isNat(M),n__isNat(N)),M,N)	(11)
isNat(n__x(V1,V2))	→	and(isNat(activate(V1)),n__isNat(activate(V2)))	(9)
x(N,s(M))	→	U41(and(isNat(M),n__isNat(N)),M,N)	(13)
isNat(n__0)	→	tt	(6)
U21(tt,M,N)	→	s(plus(activate(N),activate(M)))	(2)

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

U41^#(tt,M,N)	→	activate^#(M)	(52)
isNat^#(n__x(V1,V2))	→	activate^#(V2)	(31)
isNat^#(n__x(V1,V2))	→	and^#(isNat(activate(V1)),n__isNat(activate(V2)))	(57)
x^#(N,s(M))	→	isNat^#(M)	(40)

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

U41^#(tt,M,N)	→	x^#(activate(N),activate(M))	(46)
U41^#(tt,M,N)	→	plus^#(x(activate(N),activate(M)),activate(N))	(42)
isNat^#(n__s(V1))	→	activate^#(V1)	(49)
isNat^#(n__s(V1))	→	isNat^#(activate(V1))	(35)
U11^#(tt,N)	→	activate^#(N)	(37)
activate^#(n__isNat(X))	→	isNat^#(X)	(44)
and^#(tt,X)	→	activate^#(X)	(38)
plus^#(N,0)	→	isNat^#(N)	(32)
plus^#(N,0)	→	U11^#(isNat(N),N)	(33)
isNat^#(n__plus(V1,V2))	→	activate^#(V1)	(53)
isNat^#(n__plus(V1,V2))	→	isNat^#(activate(V1))	(39)
activate^#(n__plus(X1,X2))	→	plus^#(X1,X2)	(60)
activate^#(n__x(X1,X2))	→	x^#(X1,X2)	(58)
plus^#(N,s(M))	→	and^#(isNat(M),n__isNat(N))	(29)
plus^#(N,s(M))	→	U21^#(and(isNat(M),n__isNat(N)),M,N)	(34)
x^#(N,s(M))	→	U41^#(and(isNat(M),n__isNat(N)),M,N)	(43)
U21^#(tt,M,N)	→	activate^#(N)	(55)
U21^#(tt,M,N)	→	plus^#(activate(N),activate(M))	(25)

1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the argument filter

π(activate)	=	1
π(and)	=	2
π(s^#)	=	1
π(n__isNat)	=	1
π(isNat)	=	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(U21)	=	5	status(U21)	=	[3, 2, 1]	list-extension(U21)	=	Lex
prec(U11)	=	4	status(U11)	=	[1, 2]	list-extension(U11)	=	Lex
prec(s)	=	4	status(s)	=	[1]	list-extension(s)	=	Lex
prec(isNat^#)	=	3	status(isNat^#)	=	[1]	list-extension(isNat^#)	=	Lex
prec(plus^#)	=	3	status(plus^#)	=	[1]	list-extension(plus^#)	=	Lex
prec(activate^#)	=	3	status(activate^#)	=	[1]	list-extension(activate^#)	=	Lex
prec(x)	=	6	status(x)	=	[1, 2]	list-extension(x)	=	Lex
prec(n__s)	=	4	status(n__s)	=	[1]	list-extension(n__s)	=	Lex
prec(0)	=	2	status(0)	=	[]	list-extension(0)	=	Lex
prec(x^#)	=	6	status(x^#)	=	[1, 2]	list-extension(x^#)	=	Lex
prec(n__plus)	=	5	status(n__plus)	=	[1, 2]	list-extension(n__plus)	=	Lex
prec(n__0)	=	2	status(n__0)	=	[]	list-extension(n__0)	=	Lex
prec(n__x)	=	6	status(n__x)	=	[1, 2]	list-extension(n__x)	=	Lex
prec(plus)	=	5	status(plus)	=	[1, 2]	list-extension(plus)	=	Lex
prec(U11^#)	=	3	status(U11^#)	=	[2]	list-extension(U11^#)	=	Lex
prec(U31)	=	2	status(U31)	=	[1]	list-extension(U31)	=	Lex
prec(U41^#)	=	6	status(U41^#)	=	[3, 2, 1]	list-extension(U41^#)	=	Lex
prec(U21^#)	=	3	status(U21^#)	=	[3]	list-extension(U21^#)	=	Lex
prec(tt)	=	1	status(tt)	=	[]	list-extension(tt)	=	Lex
prec(U41)	=	6	status(U41)	=	[3, 2, 1]	list-extension(U41)	=	Lex
prec(U31^#)	=	0	status(U31^#)	=	[]	list-extension(U31^#)	=	Lex
prec(and^#)	=	3	status(and^#)	=	[2]	list-extension(and^#)	=	Lex

and the following Max-polynomial interpretation

[0^#]	=	0
[U21(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 0, 0)
[U11(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[s(x₁)]	=	x₁ + 0
[isNat^#(x₁)]	=	x₁ + 0
[plus^#(x₁, x₂)]	=	max(x₁ + 0, 0)
[activate^#(x₁)]	=	x₁ + 0
[x(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[n__s(x₁)]	=	x₁ + 0
[0]	=	0
[x^#(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[n__plus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[n__0]	=	0
[n__x(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[plus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[U11^#(x₁, x₂)]	=	max(x₂ + 0, 0)
[U31(x₁)]	=	x₁ + 0
[U41^#(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 0, 0)
[U21^#(x₁, x₂, x₃)]	=	max(x₃ + 0, 0)
[tt]	=	0
[U41(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 0, 0)
[U31^#(x₁)]	=	0
[and^#(x₁, x₂)]	=	max(x₂ + 0, 0)

together with the usable rules

x(X1,X2)	→	n__x(X1,X2)	(18)
U41(tt,M,N)	→	plus(x(activate(N),activate(M)),activate(N))	(4)
plus(X1,X2)	→	n__plus(X1,X2)	(15)
isNat(n__s(V1))	→	isNat(activate(V1))	(8)
U11(tt,N)	→	activate(N)	(1)
U31(tt)	→	0	(3)
isNat(X)	→	n__isNat(X)	(16)
activate(n__isNat(X))	→	isNat(X)	(21)
activate(n__0)	→	0	(19)
s(X)	→	n__s(X)	(17)
activate(n__s(X))	→	s(X)	(22)
and(tt,X)	→	activate(X)	(5)
plus(N,0)	→	U11(isNat(N),N)	(10)
isNat(n__plus(V1,V2))	→	and(isNat(activate(V1)),n__isNat(activate(V2)))	(7)
activate(n__plus(X1,X2))	→	plus(X1,X2)	(20)
0	→	n__0	(14)
x(N,0)	→	U31(isNat(N))	(12)
activate(n__x(X1,X2))	→	x(X1,X2)	(23)
activate(X)	→	X	(24)
plus(N,s(M))	→	U21(and(isNat(M),n__isNat(N)),M,N)	(11)
isNat(n__x(V1,V2))	→	and(isNat(activate(V1)),n__isNat(activate(V2)))	(9)
x(N,s(M))	→	U41(and(isNat(M),n__isNat(N)),M,N)	(13)
isNat(n__0)	→	tt	(6)
U21(tt,M,N)	→	s(plus(activate(N),activate(M)))	(2)

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

U41^#(tt,M,N)	→	x^#(activate(N),activate(M))	(46)
U41^#(tt,M,N)	→	plus^#(x(activate(N),activate(M)),activate(N))	(42)
isNat^#(n__s(V1))	→	activate^#(V1)	(49)
isNat^#(n__s(V1))	→	isNat^#(activate(V1))	(35)
isNat^#(n__plus(V1,V2))	→	activate^#(V1)	(53)
isNat^#(n__plus(V1,V2))	→	isNat^#(activate(V1))	(39)
activate^#(n__plus(X1,X2))	→	plus^#(X1,X2)	(60)
activate^#(n__x(X1,X2))	→	x^#(X1,X2)	(58)
x^#(N,s(M))	→	U41^#(and(isNat(M),n__isNat(N)),M,N)	(43)

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

plus^#(N,s(M))	→	U21^#(and(isNat(M),n__isNat(N)),M,N)	(34)
U21^#(tt,M,N)	→	plus^#(activate(N),activate(M))	(25)

1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the argument filter

π(activate)	=	1
π(and)	=	2
π(s^#)	=	1
π(n__isNat)	=	1
π(isNat)	=	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(U21)	=	5	status(U21)	=	[3, 2, 1]	list-extension(U21)	=	Lex
prec(U11)	=	4	status(U11)	=	[1, 2]	list-extension(U11)	=	Lex
prec(s)	=	4	status(s)	=	[1]	list-extension(s)	=	Lex
prec(isNat^#)	=	3	status(isNat^#)	=	[1]	list-extension(isNat^#)	=	Lex
prec(plus^#)	=	0	status(plus^#)	=	[2]	list-extension(plus^#)	=	Lex
prec(activate^#)	=	3	status(activate^#)	=	[1]	list-extension(activate^#)	=	Lex
prec(x)	=	6	status(x)	=	[1, 2]	list-extension(x)	=	Lex
prec(n__s)	=	4	status(n__s)	=	[1]	list-extension(n__s)	=	Lex
prec(0)	=	2	status(0)	=	[]	list-extension(0)	=	Lex
prec(x^#)	=	6	status(x^#)	=	[1, 2]	list-extension(x^#)	=	Lex
prec(n__plus)	=	5	status(n__plus)	=	[1, 2]	list-extension(n__plus)	=	Lex
prec(n__0)	=	2	status(n__0)	=	[]	list-extension(n__0)	=	Lex
prec(n__x)	=	6	status(n__x)	=	[1, 2]	list-extension(n__x)	=	Lex
prec(plus)	=	5	status(plus)	=	[1, 2]	list-extension(plus)	=	Lex
prec(U11^#)	=	3	status(U11^#)	=	[2]	list-extension(U11^#)	=	Lex
prec(U31)	=	2	status(U31)	=	[1]	list-extension(U31)	=	Lex
prec(U41^#)	=	6	status(U41^#)	=	[3, 2, 1]	list-extension(U41^#)	=	Lex
prec(U21^#)	=	0	status(U21^#)	=	[2]	list-extension(U21^#)	=	Lex
prec(tt)	=	1	status(tt)	=	[]	list-extension(tt)	=	Lex
prec(U41)	=	6	status(U41)	=	[3, 2, 1]	list-extension(U41)	=	Lex
prec(U31^#)	=	0	status(U31^#)	=	[]	list-extension(U31^#)	=	Lex
prec(and^#)	=	3	status(and^#)	=	[2]	list-extension(and^#)	=	Lex

and the following Max-polynomial interpretation

[0^#]	=	0
[U21(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 0, 0)
[U11(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[s(x₁)]	=	x₁ + 0
[isNat^#(x₁)]	=	x₁ + 0
[plus^#(x₁, x₂)]	=	max(x₂ + 0, 0)
[activate^#(x₁)]	=	x₁ + 0
[x(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[n__s(x₁)]	=	x₁ + 0
[0]	=	0
[x^#(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[n__plus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[n__0]	=	0
[n__x(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[plus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[U11^#(x₁, x₂)]	=	max(x₂ + 0, 0)
[U31(x₁)]	=	x₁ + 0
[U41^#(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 0, 0)
[U21^#(x₁, x₂, x₃)]	=	max(x₂ + 0, 0)
[tt]	=	0
[U41(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 0, 0)
[U31^#(x₁)]	=	0
[and^#(x₁, x₂)]	=	max(x₂ + 0, 0)

together with the usable rules

x(X1,X2)	→	n__x(X1,X2)	(18)
U41(tt,M,N)	→	plus(x(activate(N),activate(M)),activate(N))	(4)
plus(X1,X2)	→	n__plus(X1,X2)	(15)
isNat(n__s(V1))	→	isNat(activate(V1))	(8)
U11(tt,N)	→	activate(N)	(1)
U31(tt)	→	0	(3)
isNat(X)	→	n__isNat(X)	(16)
activate(n__isNat(X))	→	isNat(X)	(21)
activate(n__0)	→	0	(19)
s(X)	→	n__s(X)	(17)
activate(n__s(X))	→	s(X)	(22)
and(tt,X)	→	activate(X)	(5)
plus(N,0)	→	U11(isNat(N),N)	(10)
isNat(n__plus(V1,V2))	→	and(isNat(activate(V1)),n__isNat(activate(V2)))	(7)
activate(n__plus(X1,X2))	→	plus(X1,X2)	(20)
0	→	n__0	(14)
x(N,0)	→	U31(isNat(N))	(12)
activate(n__x(X1,X2))	→	x(X1,X2)	(23)
activate(X)	→	X	(24)
plus(N,s(M))	→	U21(and(isNat(M),n__isNat(N)),M,N)	(11)
isNat(n__x(V1,V2))	→	and(isNat(activate(V1)),n__isNat(activate(V2)))	(9)
x(N,s(M))	→	U41(and(isNat(M),n__isNat(N)),M,N)	(13)
isNat(n__0)	→	tt	(6)
U21(tt,M,N)	→	s(plus(activate(N),activate(M)))	(2)

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

plus^#(N,s(M))

→

U21^#(and(isNat(M),n__isNat(N)),M,N)

(34)

could be deleted.

1.1.1.1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.