Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/MYNAT_nokinds_FR)

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(activate(X1),activate(X2))	(20)
activate(n__isNat(X))	→	isNat(X)	(21)
activate(n__s(X))	→	s(activate(X))	(22)
activate(n__x(X1,X2))	→	x(activate(X1),activate(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)
and^#(tt,X)	→	activate^#(X)	(26)
U11^#(tt,N)	→	activate^#(N)	(27)
U41^#(tt,M,N)	→	activate^#(N)	(28)
U41^#(tt,M,N)	→	activate^#(M)	(29)
isNat^#(n__s(V1))	→	activate^#(V1)	(30)
U41^#(tt,M,N)	→	plus^#(x(activate(N),activate(M)),activate(N))	(31)
x^#(N,s(M))	→	and^#(isNat(M),n__isNat(N))	(32)
U41^#(tt,M,N)	→	activate^#(N)	(28)
plus^#(N,s(M))	→	and^#(isNat(M),n__isNat(N))	(33)
isNat^#(n__x(V1,V2))	→	isNat^#(activate(V1))	(34)
isNat^#(n__x(V1,V2))	→	activate^#(V2)	(35)
isNat^#(n__plus(V1,V2))	→	isNat^#(activate(V1))	(36)
isNat^#(n__plus(V1,V2))	→	and^#(isNat(activate(V1)),n__isNat(activate(V2)))	(37)
plus^#(N,s(M))	→	U21^#(and(isNat(M),n__isNat(N)),M,N)	(38)
activate^#(n__s(X))	→	activate^#(X)	(39)
plus^#(N,s(M))	→	isNat^#(M)	(40)
activate^#(n__s(X))	→	s^#(activate(X))	(41)
isNat^#(n__plus(V1,V2))	→	activate^#(V1)	(42)
activate^#(n__plus(X1,X2))	→	plus^#(activate(X1),activate(X2))	(43)
x^#(N,s(M))	→	isNat^#(M)	(44)
U41^#(tt,M,N)	→	x^#(activate(N),activate(M))	(45)
isNat^#(n__x(V1,V2))	→	activate^#(V1)	(46)
activate^#(n__isNat(X))	→	isNat^#(X)	(47)
x^#(N,s(M))	→	U41^#(and(isNat(M),n__isNat(N)),M,N)	(48)
plus^#(N,0)	→	isNat^#(N)	(49)
activate^#(n__plus(X1,X2))	→	activate^#(X2)	(50)
U31^#(tt)	→	0^#	(51)
plus^#(N,0)	→	U11^#(isNat(N),N)	(52)
activate^#(n__x(X1,X2))	→	activate^#(X2)	(53)
activate^#(n__0)	→	0^#	(54)
x^#(N,0)	→	isNat^#(N)	(55)
isNat^#(n__plus(V1,V2))	→	activate^#(V2)	(56)
isNat^#(n__s(V1))	→	isNat^#(activate(V1))	(57)
activate^#(n__plus(X1,X2))	→	activate^#(X1)	(58)
activate^#(n__x(X1,X2))	→	activate^#(X1)	(59)
U21^#(tt,M,N)	→	activate^#(N)	(60)
U21^#(tt,M,N)	→	s^#(plus(activate(N),activate(M)))	(61)
isNat^#(n__x(V1,V2))	→	and^#(isNat(activate(V1)),n__isNat(activate(V2)))	(62)
activate^#(n__x(X1,X2))	→	x^#(activate(X1),activate(X2))	(63)
U21^#(tt,M,N)	→	activate^#(M)	(64)
x^#(N,0)	→	U31^#(isNat(N))	(65)

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

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

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[0^#]	=	0
[U21(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 4, x₃ + 0, 0)
[U11(x₁, x₂)]	=	max(x₂ + 0, 0)
[s(x₁)]	=	x₁ + 0
[isNat^#(x₁)]	=	x₁ + 2
[activate(x₁)]	=	x₁ + 0
[and(x₁, x₂)]	=	max(x₂ + 0, 0)
[plus^#(x₁, x₂)]	=	max(x₁ + 2, x₂ + 4, 0)
[activate^#(x₁)]	=	x₁ + 2
[x(x₁, x₂)]	=	max(x₁ + 31116, x₂ + 31117, 0)
[n__s(x₁)]	=	x₁ + 0
[0]	=	17069
[x^#(x₁, x₂)]	=	max(x₁ + 31118, x₂ + 31119, 0)
[s^#(x₁)]	=	0
[n__isNat(x₁)]	=	x₁ + 0
[n__plus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 4, 0)
[n__0]	=	17069
[isNat(x₁)]	=	x₁ + 0
[n__x(x₁, x₂)]	=	max(x₁ + 31116, x₂ + 31117, 0)
[plus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 4, 0)
[U11^#(x₁, x₂)]	=	max(x₁ + 2, x₂ + 2, 0)
[U31(x₁)]	=	17069
[U41^#(x₁, x₂, x₃)]	=	max(x₁ + 31117, x₂ + 31119, x₃ + 31118, 0)
[U21^#(x₁, x₂, x₃)]	=	max(x₁ + 2, x₂ + 4, x₃ + 2, 0)
[tt]	=	3
[U41(x₁, x₂, x₃)]	=	max(x₁ + 1, x₂ + 31117, x₃ + 31116, 0)
[U31^#(x₁)]	=	0
[and^#(x₁, x₂)]	=	max(x₁ + 1, x₂ + 2, 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(activate(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(activate(X1),activate(X2))	(20)
0	→	n__0	(14)
x(N,0)	→	U31(isNat(N))	(12)
activate(n__x(X1,X2))	→	x(activate(X1),activate(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)	(64)
plus^#(N,s(M))	→	isNat^#(M)	(40)
isNat^#(n__x(V1,V2))	→	and^#(isNat(activate(V1)),n__isNat(activate(V2)))	(62)
isNat^#(n__plus(V1,V2))	→	and^#(isNat(activate(V1)),n__isNat(activate(V2)))	(37)
activate^#(n__x(X1,X2))	→	activate^#(X1)	(59)
isNat^#(n__plus(V1,V2))	→	activate^#(V2)	(56)
isNat^#(n__x(V1,V2))	→	activate^#(V2)	(35)
isNat^#(n__x(V1,V2))	→	isNat^#(activate(V1))	(34)
x^#(N,0)	→	isNat^#(N)	(55)
activate^#(n__x(X1,X2))	→	activate^#(X2)	(53)
U41^#(tt,M,N)	→	activate^#(N)	(28)
x^#(N,s(M))	→	and^#(isNat(M),n__isNat(N))	(32)
activate^#(n__plus(X1,X2))	→	activate^#(X2)	(50)
U41^#(tt,M,N)	→	activate^#(M)	(29)
U41^#(tt,M,N)	→	activate^#(N)	(28)
isNat^#(n__x(V1,V2))	→	activate^#(V1)	(46)
x^#(N,s(M))	→	isNat^#(M)	(44)

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)	→	x^#(activate(N),activate(M))	(45)
U41^#(tt,M,N)	→	plus^#(x(activate(N),activate(M)),activate(N))	(31)
isNat^#(n__s(V1))	→	activate^#(V1)	(30)
isNat^#(n__s(V1))	→	isNat^#(activate(V1))	(57)
U11^#(tt,N)	→	activate^#(N)	(27)
activate^#(n__isNat(X))	→	isNat^#(X)	(47)
activate^#(n__s(X))	→	activate^#(X)	(39)
and^#(tt,X)	→	activate^#(X)	(26)
plus^#(N,0)	→	isNat^#(N)	(49)
plus^#(N,0)	→	U11^#(isNat(N),N)	(52)
isNat^#(n__plus(V1,V2))	→	activate^#(V1)	(42)
isNat^#(n__plus(V1,V2))	→	isNat^#(activate(V1))	(36)
activate^#(n__plus(X1,X2))	→	activate^#(X1)	(58)
activate^#(n__plus(X1,X2))	→	plus^#(activate(X1),activate(X2))	(43)
activate^#(n__x(X1,X2))	→	x^#(activate(X1),activate(X2))	(63)
plus^#(N,s(M))	→	and^#(isNat(M),n__isNat(N))	(33)
plus^#(N,s(M))	→	U21^#(and(isNat(M),n__isNat(N)),M,N)	(38)
x^#(N,s(M))	→	U41^#(and(isNat(M),n__isNat(N)),M,N)	(48)
U21^#(tt,M,N)	→	activate^#(N)	(60)
U21^#(tt,M,N)	→	plus^#(activate(N),activate(M))	(25)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the argument filter

π(U11)	=	2
π(isNat^#)	=	1
π(activate)	=	1
π(and)	=	2
π(plus^#)	=	1
π(activate^#)	=	1
π(s^#)	=	1
π(n__isNat)	=	1
π(isNat)	=	1
π(U11^#)	=	2
π(U21^#)	=	3
π(and^#)	=	2

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

and the following Max-polynomial interpretation

[0^#]	=	0
[U21(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 0, 0)
[s(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)
[U31(x₁)]	=	x₁ + 0
[U41^#(x₁, x₂, x₃)]	=	max(x₂ + 0, x₃ + 0, 0)
[tt]	=	0
[U41(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 0, 0)
[U31^#(x₁)]	=	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(activate(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(activate(X1),activate(X2))	(20)
0	→	n__0	(14)
x(N,0)	→	U31(isNat(N))	(12)
activate(n__x(X1,X2))	→	x(activate(X1),activate(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

isNat^#(n__s(V1))	→	activate^#(V1)	(30)
isNat^#(n__s(V1))	→	isNat^#(activate(V1))	(57)
activate^#(n__s(X))	→	activate^#(X)	(39)
isNat^#(n__plus(V1,V2))	→	activate^#(V1)	(42)
isNat^#(n__plus(V1,V2))	→	isNat^#(activate(V1))	(36)
activate^#(n__plus(X1,X2))	→	activate^#(X1)	(58)
activate^#(n__plus(X1,X2))	→	plus^#(activate(X1),activate(X2))	(43)
x^#(N,s(M))	→	U41^#(and(isNat(M),n__isNat(N)),M,N)	(48)

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

plus^#(N,s(M))	→	U21^#(and(isNat(M),n__isNat(N)),M,N)	(38)
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

π(U11)	=	2
π(isNat^#)	=	1
π(activate)	=	1
π(and)	=	2
π(activate^#)	=	1
π(s^#)	=	1
π(n__isNat)	=	1
π(isNat)	=	1
π(U11^#)	=	2
π(and^#)	=	2

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)	=	3	status(U21)	=	[3, 2, 1]	list-extension(U21)	=	Lex
prec(s)	=	1	status(s)	=	[1]	list-extension(s)	=	Lex
prec(plus^#)	=	2	status(plus^#)	=	[1, 2]	list-extension(plus^#)	=	Lex
prec(x)	=	8	status(x)	=	[2, 1]	list-extension(x)	=	Lex
prec(n__s)	=	1	status(n__s)	=	[1]	list-extension(n__s)	=	Lex
prec(0)	=	0	status(0)	=	[]	list-extension(0)	=	Lex
prec(x^#)	=	8	status(x^#)	=	[2, 1]	list-extension(x^#)	=	Lex
prec(n__plus)	=	3	status(n__plus)	=	[1, 2]	list-extension(n__plus)	=	Lex
prec(n__0)	=	0	status(n__0)	=	[]	list-extension(n__0)	=	Lex
prec(n__x)	=	8	status(n__x)	=	[2, 1]	list-extension(n__x)	=	Lex
prec(plus)	=	3	status(plus)	=	[1, 2]	list-extension(plus)	=	Lex
prec(U31)	=	0	status(U31)	=	[1]	list-extension(U31)	=	Lex
prec(U41^#)	=	8	status(U41^#)	=	[2, 3]	list-extension(U41^#)	=	Lex
prec(U21^#)	=	2	status(U21^#)	=	[3, 2, 1]	list-extension(U21^#)	=	Lex
prec(tt)	=	0	status(tt)	=	[]	list-extension(tt)	=	Lex
prec(U41)	=	8	status(U41)	=	[2, 3, 1]	list-extension(U41)	=	Lex
prec(U31^#)	=	0	status(U31^#)	=	[]	list-extension(U31^#)	=	Lex

and the following Max-polynomial interpretation

[0^#]	=	0
[U21(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 0, 0)
[s(x₁)]	=	x₁ + 0
[plus^#(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 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)
[U31(x₁)]	=	x₁ + 0
[U41^#(x₁, x₂, x₃)]	=	max(x₂ + 0, x₃ + 0, 0)
[U21^#(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 0, 0)
[tt]	=	0
[U41(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 0, 0)
[U31^#(x₁)]	=	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(activate(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(activate(X1),activate(X2))	(20)
0	→	n__0	(14)
x(N,0)	→	U31(isNat(N))	(12)
activate(n__x(X1,X2))	→	x(activate(X1),activate(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

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

could be deleted.

1.1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.