Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/MYNAT_complete_Z)

The rewrite relation of the following TRS is considered.

U11(tt,V1,V2)	→	U12(isNat(activate(V1)),activate(V2))	(1)
U12(tt,V2)	→	U13(isNat(activate(V2)))	(2)
U13(tt)	→	tt	(3)
U21(tt,V1)	→	U22(isNat(activate(V1)))	(4)
U22(tt)	→	tt	(5)
U31(tt,V1,V2)	→	U32(isNat(activate(V1)),activate(V2))	(6)
U32(tt,V2)	→	U33(isNat(activate(V2)))	(7)
U33(tt)	→	tt	(8)
U41(tt,N)	→	activate(N)	(9)
U51(tt,M,N)	→	s(plus(activate(N),activate(M)))	(10)
U61(tt)	→	0	(11)
U71(tt,M,N)	→	plus(x(activate(N),activate(M)),activate(N))	(12)
and(tt,X)	→	activate(X)	(13)
isNat(n__0)	→	tt	(14)
isNat(n__plus(V1,V2))	→	U11(and(isNatKind(activate(V1)),n__isNatKind(activate(V2))),activate(V1),activate(V2))	(15)
isNat(n__s(V1))	→	U21(isNatKind(activate(V1)),activate(V1))	(16)
isNat(n__x(V1,V2))	→	U31(and(isNatKind(activate(V1)),n__isNatKind(activate(V2))),activate(V1),activate(V2))	(17)
isNatKind(n__0)	→	tt	(18)
isNatKind(n__plus(V1,V2))	→	and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))	(19)
isNatKind(n__s(V1))	→	isNatKind(activate(V1))	(20)
isNatKind(n__x(V1,V2))	→	and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))	(21)
plus(N,0)	→	U41(and(isNat(N),n__isNatKind(N)),N)	(22)
plus(N,s(M))	→	U51(and(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N))),M,N)	(23)
x(N,0)	→	U61(and(isNat(N),n__isNatKind(N)))	(24)
x(N,s(M))	→	U71(and(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N))),M,N)	(25)
0	→	n__0	(26)
plus(X1,X2)	→	n__plus(X1,X2)	(27)
isNatKind(X)	→	n__isNatKind(X)	(28)
s(X)	→	n__s(X)	(29)
x(X1,X2)	→	n__x(X1,X2)	(30)
and(X1,X2)	→	n__and(X1,X2)	(31)
activate(n__0)	→	0	(32)
activate(n__plus(X1,X2))	→	plus(X1,X2)	(33)
activate(n__isNatKind(X))	→	isNatKind(X)	(34)
activate(n__s(X))	→	s(X)	(35)
activate(n__x(X1,X2))	→	x(X1,X2)	(36)
activate(n__and(X1,X2))	→	and(X1,X2)	(37)
activate(X)	→	X	(38)

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.

U12^#(tt,V2)	→	isNat^#(activate(V2))	(39)
plus^#(N,0)	→	isNat^#(N)	(40)
x^#(N,s(M))	→	isNat^#(M)	(41)
U32^#(tt,V2)	→	activate^#(V2)	(42)
U11^#(tt,V1,V2)	→	U12^#(isNat(activate(V1)),activate(V2))	(43)
isNat^#(n__x(V1,V2))	→	and^#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))	(44)
plus^#(N,0)	→	and^#(isNat(N),n__isNatKind(N))	(45)
plus^#(N,0)	→	U41^#(and(isNat(N),n__isNatKind(N)),N)	(46)
U51^#(tt,M,N)	→	plus^#(activate(N),activate(M))	(47)
isNat^#(n__plus(V1,V2))	→	activate^#(V1)	(48)
isNat^#(n__x(V1,V2))	→	isNatKind^#(activate(V1))	(49)
isNatKind^#(n__plus(V1,V2))	→	and^#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))	(50)
isNat^#(n__plus(V1,V2))	→	and^#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))	(51)
isNat^#(n__x(V1,V2))	→	activate^#(V1)	(52)
isNat^#(n__plus(V1,V2))	→	activate^#(V1)	(48)
isNat^#(n__plus(V1,V2))	→	activate^#(V2)	(53)
isNatKind^#(n__x(V1,V2))	→	and^#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))	(54)
isNatKind^#(n__x(V1,V2))	→	activate^#(V2)	(55)
U51^#(tt,M,N)	→	activate^#(N)	(56)
U31^#(tt,V1,V2)	→	U32^#(isNat(activate(V1)),activate(V2))	(57)
isNatKind^#(n__x(V1,V2))	→	isNatKind^#(activate(V1))	(58)
isNatKind^#(n__plus(V1,V2))	→	activate^#(V1)	(59)
U11^#(tt,V1,V2)	→	isNat^#(activate(V1))	(60)
activate^#(n__plus(X1,X2))	→	plus^#(X1,X2)	(61)
isNat^#(n__x(V1,V2))	→	activate^#(V2)	(62)
x^#(N,0)	→	U61^#(and(isNat(N),n__isNatKind(N)))	(63)
U31^#(tt,V1,V2)	→	activate^#(V2)	(64)
U41^#(tt,N)	→	activate^#(N)	(65)
activate^#(n__x(X1,X2))	→	x^#(X1,X2)	(66)
isNat^#(n__plus(V1,V2))	→	activate^#(V2)	(53)
U71^#(tt,M,N)	→	activate^#(M)	(67)
isNat^#(n__plus(V1,V2))	→	U11^#(and(isNatKind(activate(V1)),n__isNatKind(activate(V2))),activate(V1),activate(V2))	(68)
U71^#(tt,M,N)	→	activate^#(N)	(69)
U21^#(tt,V1)	→	isNat^#(activate(V1))	(70)
isNat^#(n__x(V1,V2))	→	U31^#(and(isNatKind(activate(V1)),n__isNatKind(activate(V2))),activate(V1),activate(V2))	(71)
U11^#(tt,V1,V2)	→	activate^#(V2)	(72)
U61^#(tt)	→	0^#	(73)
isNatKind^#(n__s(V1))	→	isNatKind^#(activate(V1))	(74)
U21^#(tt,V1)	→	activate^#(V1)	(75)
isNatKind^#(n__plus(V1,V2))	→	activate^#(V2)	(76)
x^#(N,0)	→	and^#(isNat(N),n__isNatKind(N))	(77)
isNat^#(n__s(V1))	→	U21^#(isNatKind(activate(V1)),activate(V1))	(78)
x^#(N,s(M))	→	isNat^#(N)	(79)
activate^#(n__0)	→	0^#	(80)
isNat^#(n__x(V1,V2))	→	activate^#(V2)	(62)
U71^#(tt,M,N)	→	activate^#(N)	(69)
plus^#(N,s(M))	→	isNat^#(N)	(81)
U31^#(tt,V1,V2)	→	isNat^#(activate(V1))	(82)
U51^#(tt,M,N)	→	activate^#(M)	(83)
and^#(tt,X)	→	activate^#(X)	(84)
isNat^#(n__s(V1))	→	activate^#(V1)	(85)
U32^#(tt,V2)	→	U33^#(isNat(activate(V2)))	(86)
isNat^#(n__plus(V1,V2))	→	isNatKind^#(activate(V1))	(87)
activate^#(n__and(X1,X2))	→	and^#(X1,X2)	(88)
activate^#(n__isNatKind(X))	→	isNatKind^#(X)	(89)
isNat^#(n__s(V1))	→	activate^#(V1)	(85)
x^#(N,s(M))	→	and^#(isNat(M),n__isNatKind(M))	(90)
U71^#(tt,M,N)	→	x^#(activate(N),activate(M))	(91)
U32^#(tt,V2)	→	isNat^#(activate(V2))	(92)
x^#(N,s(M))	→	and^#(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N)))	(93)
isNatKind^#(n__x(V1,V2))	→	activate^#(V1)	(94)
plus^#(N,s(M))	→	and^#(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N)))	(95)
isNatKind^#(n__s(V1))	→	activate^#(V1)	(96)
plus^#(N,s(M))	→	isNat^#(M)	(97)
isNat^#(n__s(V1))	→	isNatKind^#(activate(V1))	(98)
x^#(N,s(M))	→	U71^#(and(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N))),M,N)	(99)
U11^#(tt,V1,V2)	→	activate^#(V1)	(100)
U51^#(tt,M,N)	→	s^#(plus(activate(N),activate(M)))	(101)
U71^#(tt,M,N)	→	plus^#(x(activate(N),activate(M)),activate(N))	(102)
plus^#(N,s(M))	→	U51^#(and(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N))),M,N)	(103)
U12^#(tt,V2)	→	activate^#(V2)	(104)
U21^#(tt,V1)	→	U22^#(isNat(activate(V1)))	(105)
U12^#(tt,V2)	→	U13^#(isNat(activate(V2)))	(106)
isNatKind^#(n__plus(V1,V2))	→	isNatKind^#(activate(V1))	(107)
U31^#(tt,V1,V2)	→	activate^#(V1)	(108)
x^#(N,0)	→	isNat^#(N)	(109)
activate^#(n__s(X))	→	s^#(X)	(110)
isNat^#(n__x(V1,V2))	→	activate^#(V1)	(52)
plus^#(N,s(M))	→	and^#(isNat(M),n__isNatKind(M))	(111)

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

plus^#(N,s(M))	→	and^#(isNat(M),n__isNatKind(M))	(111)
isNat^#(n__x(V1,V2))	→	activate^#(V1)	(52)
U71^#(tt,M,N)	→	activate^#(N)	(69)
isNat^#(n__x(V1,V2))	→	activate^#(V2)	(62)
isNat^#(n__s(V1))	→	U21^#(isNatKind(activate(V1)),activate(V1))	(78)
x^#(N,s(M))	→	isNat^#(N)	(79)
x^#(N,0)	→	and^#(isNat(N),n__isNatKind(N))	(77)
x^#(N,0)	→	isNat^#(N)	(109)
U21^#(tt,V1)	→	activate^#(V1)	(75)
isNatKind^#(n__plus(V1,V2))	→	activate^#(V2)	(76)
isNatKind^#(n__s(V1))	→	isNatKind^#(activate(V1))	(74)
U11^#(tt,V1,V2)	→	activate^#(V2)	(72)
U31^#(tt,V1,V2)	→	activate^#(V1)	(108)
isNat^#(n__x(V1,V2))	→	U31^#(and(isNatKind(activate(V1)),n__isNatKind(activate(V2))),activate(V1),activate(V2))	(71)
isNatKind^#(n__plus(V1,V2))	→	isNatKind^#(activate(V1))	(107)
U21^#(tt,V1)	→	isNat^#(activate(V1))	(70)
U71^#(tt,M,N)	→	activate^#(N)	(69)
isNat^#(n__plus(V1,V2))	→	U11^#(and(isNatKind(activate(V1)),n__isNatKind(activate(V2))),activate(V1),activate(V2))	(68)
U12^#(tt,V2)	→	activate^#(V2)	(104)
U71^#(tt,M,N)	→	activate^#(M)	(67)
plus^#(N,s(M))	→	U51^#(and(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N))),M,N)	(103)
U71^#(tt,M,N)	→	plus^#(x(activate(N),activate(M)),activate(N))	(102)
isNat^#(n__plus(V1,V2))	→	activate^#(V2)	(53)
activate^#(n__x(X1,X2))	→	x^#(X1,X2)	(66)
U11^#(tt,V1,V2)	→	activate^#(V1)	(100)
x^#(N,s(M))	→	U71^#(and(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N))),M,N)	(99)
U41^#(tt,N)	→	activate^#(N)	(65)
U31^#(tt,V1,V2)	→	activate^#(V2)	(64)
isNat^#(n__s(V1))	→	isNatKind^#(activate(V1))	(98)
isNat^#(n__x(V1,V2))	→	activate^#(V2)	(62)
isNatKind^#(n__s(V1))	→	activate^#(V1)	(96)
plus^#(N,s(M))	→	isNat^#(M)	(97)
plus^#(N,s(M))	→	and^#(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N)))	(95)
activate^#(n__plus(X1,X2))	→	plus^#(X1,X2)	(61)
U11^#(tt,V1,V2)	→	isNat^#(activate(V1))	(60)
isNatKind^#(n__plus(V1,V2))	→	activate^#(V1)	(59)
isNatKind^#(n__x(V1,V2))	→	activate^#(V1)	(94)
isNatKind^#(n__x(V1,V2))	→	isNatKind^#(activate(V1))	(58)
U31^#(tt,V1,V2)	→	U32^#(isNat(activate(V1)),activate(V2))	(57)
x^#(N,s(M))	→	and^#(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N)))	(93)
isNatKind^#(n__x(V1,V2))	→	activate^#(V2)	(55)
U51^#(tt,M,N)	→	activate^#(N)	(56)
isNatKind^#(n__x(V1,V2))	→	and^#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))	(54)
isNat^#(n__plus(V1,V2))	→	activate^#(V2)	(53)
U32^#(tt,V2)	→	isNat^#(activate(V2))	(92)
isNat^#(n__plus(V1,V2))	→	activate^#(V1)	(48)
isNat^#(n__x(V1,V2))	→	activate^#(V1)	(52)
isNat^#(n__plus(V1,V2))	→	and^#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))	(51)
U71^#(tt,M,N)	→	x^#(activate(N),activate(M))	(91)
isNatKind^#(n__plus(V1,V2))	→	and^#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))	(50)
x^#(N,s(M))	→	and^#(isNat(M),n__isNatKind(M))	(90)
isNat^#(n__s(V1))	→	activate^#(V1)	(85)
isNat^#(n__plus(V1,V2))	→	activate^#(V1)	(48)
isNat^#(n__x(V1,V2))	→	isNatKind^#(activate(V1))	(49)
activate^#(n__isNatKind(X))	→	isNatKind^#(X)	(89)
activate^#(n__and(X1,X2))	→	and^#(X1,X2)	(88)
isNat^#(n__plus(V1,V2))	→	isNatKind^#(activate(V1))	(87)
U51^#(tt,M,N)	→	plus^#(activate(N),activate(M))	(47)
isNat^#(n__s(V1))	→	activate^#(V1)	(85)
plus^#(N,0)	→	U41^#(and(isNat(N),n__isNatKind(N)),N)	(46)
plus^#(N,0)	→	and^#(isNat(N),n__isNatKind(N))	(45)
and^#(tt,X)	→	activate^#(X)	(84)
isNat^#(n__x(V1,V2))	→	and^#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))	(44)
U11^#(tt,V1,V2)	→	U12^#(isNat(activate(V1)),activate(V2))	(43)
U51^#(tt,M,N)	→	activate^#(M)	(83)
U31^#(tt,V1,V2)	→	isNat^#(activate(V1))	(82)
U32^#(tt,V2)	→	activate^#(V2)	(42)
x^#(N,s(M))	→	isNat^#(M)	(41)
plus^#(N,0)	→	isNat^#(N)	(40)
U12^#(tt,V2)	→	isNat^#(activate(V2))	(39)
plus^#(N,s(M))	→	isNat^#(N)	(81)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[0^#]	=	0
[U32^#(x₁, x₂)]	=	max(x₂ + 0, 0)
[isNatKind(x₁)]	=	x₁ + 0
[U21(x₁, x₂)]	=	max(x₁ + 0, 0)
[U11(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, 0)
[s(x₁)]	=	x₁ + 0
[isNat^#(x₁)]	=	x₁ + 0
[activate(x₁)]	=	x₁ + 0
[U71(x₁, x₂, x₃)]	=	max(x₂ + 0, x₃ + 1, 0)
[n__isNatKind(x₁)]	=	x₁ + 0
[and(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[plus^#(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[activate^#(x₁)]	=	x₁ + 0
[U13^#(x₁)]	=	0
[U12(x₁, x₂)]	=	max(x₁ + 0, 0)
[U33^#(x₁)]	=	0
[x(x₁, x₂)]	=	max(x₁ + 1, x₂ + 0, 0)
[n__s(x₁)]	=	x₁ + 0
[U12^#(x₁, x₂)]	=	max(x₂ + 0, 0)
[0]	=	12331
[x^#(x₁, x₂)]	=	max(x₁ + 1, x₂ + 0, 0)
[s^#(x₁)]	=	0
[n__plus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[U32(x₁, x₂)]	=	max(x₂ + 0, 0)
[U33(x₁)]	=	x₁ + 0
[n__0]	=	12331
[isNat(x₁)]	=	x₁ + 0
[n__x(x₁, x₂)]	=	max(x₁ + 1, x₂ + 0, 0)
[plus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[U61(x₁)]	=	12331
[U51^#(x₁, x₂, x₃)]	=	max(x₂ + 0, x₃ + 0, 0)
[U11^#(x₁, x₂, x₃)]	=	max(x₂ + 0, x₃ + 0, 0)
[U31(x₁, x₂, x₃)]	=	max(x₃ + 0, 0)
[U41^#(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[U21^#(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[U22^#(x₁)]	=	0
[tt]	=	1
[n__and(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[U71^#(x₁, x₂, x₃)]	=	max(x₂ + 0, x₃ + 1, 0)
[U13(x₁)]	=	1
[U22(x₁)]	=	1
[U51(x₁, x₂, x₃)]	=	max(x₂ + 0, x₃ + 0, 0)
[isNatKind^#(x₁)]	=	x₁ + 0
[U41(x₁, x₂)]	=	max(x₂ + 0, 0)
[U31^#(x₁, x₂, x₃)]	=	max(x₂ + 0, x₃ + 0, 0)
[and^#(x₁, x₂)]	=	max(x₂ + 0, 0)
[U61^#(x₁)]	=	0

together with the usable rules

isNatKind(n__0)	→	tt	(18)
U21(tt,V1)	→	U22(isNat(activate(V1)))	(4)
isNat(n__plus(V1,V2))	→	U11(and(isNatKind(activate(V1)),n__isNatKind(activate(V2))),activate(V1),activate(V2))	(15)
U33(tt)	→	tt	(8)
U11(tt,V1,V2)	→	U12(isNat(activate(V1)),activate(V2))	(1)
U13(tt)	→	tt	(3)
isNat(n__s(V1))	→	U21(isNatKind(activate(V1)),activate(V1))	(16)
isNatKind(n__x(V1,V2))	→	and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))	(21)
activate(n__x(X1,X2))	→	x(X1,X2)	(36)
0	→	n__0	(26)
isNatKind(n__plus(V1,V2))	→	and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))	(19)
activate(n__0)	→	0	(32)
isNat(n__x(V1,V2))	→	U31(and(isNatKind(activate(V1)),n__isNatKind(activate(V2))),activate(V1),activate(V2))	(17)
plus(X1,X2)	→	n__plus(X1,X2)	(27)
activate(n__isNatKind(X))	→	isNatKind(X)	(34)
plus(N,0)	→	U41(and(isNat(N),n__isNatKind(N)),N)	(22)
isNatKind(X)	→	n__isNatKind(X)	(28)
U22(tt)	→	tt	(5)
activate(n__plus(X1,X2))	→	plus(X1,X2)	(33)
U51(tt,M,N)	→	s(plus(activate(N),activate(M)))	(10)
U32(tt,V2)	→	U33(isNat(activate(V2)))	(7)
isNatKind(n__s(V1))	→	isNatKind(activate(V1))	(20)
x(N,s(M))	→	U71(and(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N))),M,N)	(25)
x(X1,X2)	→	n__x(X1,X2)	(30)
isNat(n__0)	→	tt	(14)
and(X1,X2)	→	n__and(X1,X2)	(31)
U71(tt,M,N)	→	plus(x(activate(N),activate(M)),activate(N))	(12)
plus(N,s(M))	→	U51(and(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N))),M,N)	(23)
x(N,0)	→	U61(and(isNat(N),n__isNatKind(N)))	(24)
U61(tt)	→	0	(11)
U41(tt,N)	→	activate(N)	(9)
and(tt,X)	→	activate(X)	(13)
U31(tt,V1,V2)	→	U32(isNat(activate(V1)),activate(V2))	(6)
activate(X)	→	X	(38)
activate(n__and(X1,X2))	→	and(X1,X2)	(37)
activate(n__s(X))	→	s(X)	(35)
s(X)	→	n__s(X)	(29)
U12(tt,V2)	→	U13(isNat(activate(V2)))	(2)

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

isNat^#(n__x(V1,V2))	→	activate^#(V1)	(52)
U71^#(tt,M,N)	→	activate^#(N)	(69)
x^#(N,s(M))	→	isNat^#(N)	(79)
x^#(N,0)	→	and^#(isNat(N),n__isNatKind(N))	(77)
x^#(N,0)	→	isNat^#(N)	(109)
U71^#(tt,M,N)	→	activate^#(N)	(69)
isNatKind^#(n__x(V1,V2))	→	activate^#(V1)	(94)
isNatKind^#(n__x(V1,V2))	→	isNatKind^#(activate(V1))	(58)
x^#(N,s(M))	→	and^#(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N)))	(93)
isNat^#(n__x(V1,V2))	→	activate^#(V1)	(52)
isNat^#(n__x(V1,V2))	→	isNatKind^#(activate(V1))	(49)

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

U21^#(tt,V1)	→	activate^#(V1)	(75)
U21^#(tt,V1)	→	isNat^#(activate(V1))	(70)
isNat^#(n__plus(V1,V2))	→	activate^#(V2)	(53)
isNat^#(n__plus(V1,V2))	→	activate^#(V1)	(48)
isNat^#(n__plus(V1,V2))	→	activate^#(V2)	(53)
isNat^#(n__plus(V1,V2))	→	activate^#(V1)	(48)
isNat^#(n__plus(V1,V2))	→	isNatKind^#(activate(V1))	(87)
isNat^#(n__plus(V1,V2))	→	and^#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))	(51)
isNat^#(n__plus(V1,V2))	→	U11^#(and(isNatKind(activate(V1)),n__isNatKind(activate(V2))),activate(V1),activate(V2))	(68)
U11^#(tt,V1,V2)	→	activate^#(V2)	(72)
U11^#(tt,V1,V2)	→	activate^#(V1)	(100)
U11^#(tt,V1,V2)	→	isNat^#(activate(V1))	(60)
U11^#(tt,V1,V2)	→	U12^#(isNat(activate(V1)),activate(V2))	(43)
isNat^#(n__s(V1))	→	activate^#(V1)	(85)
isNat^#(n__s(V1))	→	activate^#(V1)	(85)
isNat^#(n__s(V1))	→	isNatKind^#(activate(V1))	(98)
isNat^#(n__s(V1))	→	U21^#(isNatKind(activate(V1)),activate(V1))	(78)
isNatKind^#(n__x(V1,V2))	→	activate^#(V2)	(55)
isNatKind^#(n__x(V1,V2))	→	and^#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))	(54)
activate^#(n__x(X1,X2))	→	x^#(X1,X2)	(66)
isNatKind^#(n__plus(V1,V2))	→	activate^#(V2)	(76)
isNatKind^#(n__plus(V1,V2))	→	activate^#(V1)	(59)
isNatKind^#(n__plus(V1,V2))	→	isNatKind^#(activate(V1))	(107)
isNatKind^#(n__plus(V1,V2))	→	and^#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))	(50)
isNat^#(n__x(V1,V2))	→	activate^#(V2)	(62)
isNat^#(n__x(V1,V2))	→	activate^#(V2)	(62)
isNat^#(n__x(V1,V2))	→	and^#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))	(44)
isNat^#(n__x(V1,V2))	→	U31^#(and(isNatKind(activate(V1)),n__isNatKind(activate(V2))),activate(V1),activate(V2))	(71)
activate^#(n__isNatKind(X))	→	isNatKind^#(X)	(89)
plus^#(N,0)	→	isNat^#(N)	(40)
plus^#(N,0)	→	and^#(isNat(N),n__isNatKind(N))	(45)
plus^#(N,0)	→	U41^#(and(isNat(N),n__isNatKind(N)),N)	(46)
activate^#(n__plus(X1,X2))	→	plus^#(X1,X2)	(61)
U51^#(tt,M,N)	→	activate^#(M)	(83)
U51^#(tt,M,N)	→	activate^#(N)	(56)
U51^#(tt,M,N)	→	plus^#(activate(N),activate(M))	(47)
U32^#(tt,V2)	→	activate^#(V2)	(42)
U32^#(tt,V2)	→	isNat^#(activate(V2))	(92)
isNatKind^#(n__s(V1))	→	activate^#(V1)	(96)
isNatKind^#(n__s(V1))	→	isNatKind^#(activate(V1))	(74)
x^#(N,s(M))	→	isNat^#(M)	(41)
x^#(N,s(M))	→	and^#(isNat(M),n__isNatKind(M))	(90)
x^#(N,s(M))	→	U71^#(and(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N))),M,N)	(99)
U71^#(tt,M,N)	→	activate^#(M)	(67)
U71^#(tt,M,N)	→	x^#(activate(N),activate(M))	(91)
U71^#(tt,M,N)	→	plus^#(x(activate(N),activate(M)),activate(N))	(102)
plus^#(N,s(M))	→	isNat^#(N)	(81)
plus^#(N,s(M))	→	isNat^#(M)	(97)
plus^#(N,s(M))	→	and^#(isNat(M),n__isNatKind(M))	(111)
plus^#(N,s(M))	→	and^#(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N)))	(95)
plus^#(N,s(M))	→	U51^#(and(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N))),M,N)	(103)
U41^#(tt,N)	→	activate^#(N)	(65)
and^#(tt,X)	→	activate^#(X)	(84)
U31^#(tt,V1,V2)	→	activate^#(V2)	(64)
U31^#(tt,V1,V2)	→	activate^#(V1)	(108)
U31^#(tt,V1,V2)	→	isNat^#(activate(V1))	(82)
U31^#(tt,V1,V2)	→	U32^#(isNat(activate(V1)),activate(V2))	(57)
activate^#(n__and(X1,X2))	→	and^#(X1,X2)	(88)
U12^#(tt,V2)	→	activate^#(V2)	(104)
U12^#(tt,V2)	→	isNat^#(activate(V2))	(39)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[0^#]	=	0
[U32^#(x₁, x₂)]	=	max(x₂ + 2, 0)
[isNatKind(x₁)]	=	x₁ + 0
[U21(x₁, x₂)]	=	max(x₁ + 0, 0)
[U11(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, 0)
[s(x₁)]	=	x₁ + 0
[isNat^#(x₁)]	=	x₁ + 2
[activate(x₁)]	=	x₁ + 0
[U71(x₁, x₂, x₃)]	=	max(x₂ + 0, x₃ + 1, 0)
[n__isNatKind(x₁)]	=	x₁ + 0
[and(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[plus^#(x₁, x₂)]	=	max(x₁ + 2, x₂ + 2, 0)
[activate^#(x₁)]	=	x₁ + 2
[U13^#(x₁)]	=	0
[U12(x₁, x₂)]	=	max(x₁ + 0, 0)
[U33^#(x₁)]	=	0
[x(x₁, x₂)]	=	max(x₁ + 1, x₂ + 0, 0)
[n__s(x₁)]	=	x₁ + 0
[U12^#(x₁, x₂)]	=	max(x₂ + 2, 0)
[0]	=	15944
[x^#(x₁, x₂)]	=	max(x₁ + 3, x₂ + 2, 0)
[s^#(x₁)]	=	0
[n__plus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[U32(x₁, x₂)]	=	max(x₂ + 0, 0)
[U33(x₁)]	=	x₁ + 0
[n__0]	=	15944
[isNat(x₁)]	=	x₁ + 0
[n__x(x₁, x₂)]	=	max(x₁ + 1, x₂ + 0, 0)
[plus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[U61(x₁)]	=	15944
[U51^#(x₁, x₂, x₃)]	=	max(x₁ + 2, x₂ + 2, x₃ + 2, 0)
[U11^#(x₁, x₂, x₃)]	=	max(x₁ + 2, x₂ + 2, x₃ + 2, 0)
[U31(x₁, x₂, x₃)]	=	max(x₃ + 0, 0)
[U41^#(x₁, x₂)]	=	max(x₁ + 2, x₂ + 2, 0)
[U21^#(x₁, x₂)]	=	max(x₁ + 1, x₂ + 2, 0)
[U22^#(x₁)]	=	0
[tt]	=	2
[n__and(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[U71^#(x₁, x₂, x₃)]	=	max(x₂ + 2, x₃ + 3, 0)
[U13(x₁)]	=	2
[U22(x₁)]	=	2
[U51(x₁, x₂, x₃)]	=	max(x₂ + 0, x₃ + 0, 0)
[isNatKind^#(x₁)]	=	x₁ + 2
[U41(x₁, x₂)]	=	max(x₂ + 0, 0)
[U31^#(x₁, x₂, x₃)]	=	max(x₁ + 1, x₂ + 3, x₃ + 2, 0)
[and^#(x₁, x₂)]	=	max(x₂ + 2, 0)
[U61^#(x₁)]	=	0

together with the usable rules

isNatKind(n__0)	→	tt	(18)
U21(tt,V1)	→	U22(isNat(activate(V1)))	(4)
isNat(n__plus(V1,V2))	→	U11(and(isNatKind(activate(V1)),n__isNatKind(activate(V2))),activate(V1),activate(V2))	(15)
U33(tt)	→	tt	(8)
U11(tt,V1,V2)	→	U12(isNat(activate(V1)),activate(V2))	(1)
U13(tt)	→	tt	(3)
isNat(n__s(V1))	→	U21(isNatKind(activate(V1)),activate(V1))	(16)
isNatKind(n__x(V1,V2))	→	and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))	(21)
activate(n__x(X1,X2))	→	x(X1,X2)	(36)
0	→	n__0	(26)
isNatKind(n__plus(V1,V2))	→	and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))	(19)
activate(n__0)	→	0	(32)
isNat(n__x(V1,V2))	→	U31(and(isNatKind(activate(V1)),n__isNatKind(activate(V2))),activate(V1),activate(V2))	(17)
plus(X1,X2)	→	n__plus(X1,X2)	(27)
activate(n__isNatKind(X))	→	isNatKind(X)	(34)
plus(N,0)	→	U41(and(isNat(N),n__isNatKind(N)),N)	(22)
isNatKind(X)	→	n__isNatKind(X)	(28)
U22(tt)	→	tt	(5)
activate(n__plus(X1,X2))	→	plus(X1,X2)	(33)
U51(tt,M,N)	→	s(plus(activate(N),activate(M)))	(10)
U32(tt,V2)	→	U33(isNat(activate(V2)))	(7)
isNatKind(n__s(V1))	→	isNatKind(activate(V1))	(20)
x(N,s(M))	→	U71(and(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N))),M,N)	(25)
x(X1,X2)	→	n__x(X1,X2)	(30)
isNat(n__0)	→	tt	(14)
and(X1,X2)	→	n__and(X1,X2)	(31)
U71(tt,M,N)	→	plus(x(activate(N),activate(M)),activate(N))	(12)
plus(N,s(M))	→	U51(and(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N))),M,N)	(23)
x(N,0)	→	U61(and(isNat(N),n__isNatKind(N)))	(24)
U61(tt)	→	0	(11)
U41(tt,N)	→	activate(N)	(9)
and(tt,X)	→	activate(X)	(13)
U31(tt,V1,V2)	→	U32(isNat(activate(V1)),activate(V2))	(6)
activate(X)	→	X	(38)
activate(n__and(X1,X2))	→	and(X1,X2)	(37)
activate(n__s(X))	→	s(X)	(35)
s(X)	→	n__s(X)	(29)
U12(tt,V2)	→	U13(isNat(activate(V2)))	(2)

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

U31^#(tt,V1,V2)	→	activate^#(V1)	(108)
U31^#(tt,V1,V2)	→	isNat^#(activate(V1))	(82)

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

U21^#(tt,V1)	→	activate^#(V1)	(75)
U21^#(tt,V1)	→	isNat^#(activate(V1))	(70)
isNat^#(n__plus(V1,V2))	→	activate^#(V2)	(53)
isNat^#(n__plus(V1,V2))	→	activate^#(V1)	(48)
isNat^#(n__plus(V1,V2))	→	activate^#(V2)	(53)
isNat^#(n__plus(V1,V2))	→	activate^#(V1)	(48)
isNat^#(n__plus(V1,V2))	→	isNatKind^#(activate(V1))	(87)
isNat^#(n__plus(V1,V2))	→	and^#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))	(51)
isNat^#(n__plus(V1,V2))	→	U11^#(and(isNatKind(activate(V1)),n__isNatKind(activate(V2))),activate(V1),activate(V2))	(68)
U11^#(tt,V1,V2)	→	activate^#(V2)	(72)
U11^#(tt,V1,V2)	→	activate^#(V1)	(100)
U11^#(tt,V1,V2)	→	isNat^#(activate(V1))	(60)
U11^#(tt,V1,V2)	→	U12^#(isNat(activate(V1)),activate(V2))	(43)
isNat^#(n__s(V1))	→	activate^#(V1)	(85)
isNat^#(n__s(V1))	→	activate^#(V1)	(85)
isNat^#(n__s(V1))	→	isNatKind^#(activate(V1))	(98)
isNat^#(n__s(V1))	→	U21^#(isNatKind(activate(V1)),activate(V1))	(78)
isNatKind^#(n__x(V1,V2))	→	activate^#(V2)	(55)
isNatKind^#(n__x(V1,V2))	→	and^#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))	(54)
activate^#(n__x(X1,X2))	→	x^#(X1,X2)	(66)
isNatKind^#(n__plus(V1,V2))	→	activate^#(V2)	(76)
isNatKind^#(n__plus(V1,V2))	→	activate^#(V1)	(59)
isNatKind^#(n__plus(V1,V2))	→	isNatKind^#(activate(V1))	(107)
isNatKind^#(n__plus(V1,V2))	→	and^#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))	(50)
isNat^#(n__x(V1,V2))	→	activate^#(V2)	(62)
isNat^#(n__x(V1,V2))	→	activate^#(V2)	(62)
isNat^#(n__x(V1,V2))	→	and^#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))	(44)
isNat^#(n__x(V1,V2))	→	U31^#(and(isNatKind(activate(V1)),n__isNatKind(activate(V2))),activate(V1),activate(V2))	(71)
activate^#(n__isNatKind(X))	→	isNatKind^#(X)	(89)
plus^#(N,0)	→	isNat^#(N)	(40)
plus^#(N,0)	→	and^#(isNat(N),n__isNatKind(N))	(45)
plus^#(N,0)	→	U41^#(and(isNat(N),n__isNatKind(N)),N)	(46)
activate^#(n__plus(X1,X2))	→	plus^#(X1,X2)	(61)
U51^#(tt,M,N)	→	activate^#(M)	(83)
U51^#(tt,M,N)	→	activate^#(N)	(56)
U51^#(tt,M,N)	→	plus^#(activate(N),activate(M))	(47)
U32^#(tt,V2)	→	activate^#(V2)	(42)
U32^#(tt,V2)	→	isNat^#(activate(V2))	(92)
isNatKind^#(n__s(V1))	→	activate^#(V1)	(96)
isNatKind^#(n__s(V1))	→	isNatKind^#(activate(V1))	(74)
x^#(N,s(M))	→	isNat^#(M)	(41)
x^#(N,s(M))	→	and^#(isNat(M),n__isNatKind(M))	(90)
x^#(N,s(M))	→	U71^#(and(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N))),M,N)	(99)
U71^#(tt,M,N)	→	activate^#(M)	(67)
U71^#(tt,M,N)	→	x^#(activate(N),activate(M))	(91)
U71^#(tt,M,N)	→	plus^#(x(activate(N),activate(M)),activate(N))	(102)
plus^#(N,s(M))	→	isNat^#(N)	(81)
plus^#(N,s(M))	→	isNat^#(M)	(97)
plus^#(N,s(M))	→	and^#(isNat(M),n__isNatKind(M))	(111)
plus^#(N,s(M))	→	and^#(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N)))	(95)
plus^#(N,s(M))	→	U51^#(and(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N))),M,N)	(103)
U41^#(tt,N)	→	activate^#(N)	(65)
and^#(tt,X)	→	activate^#(X)	(84)
U31^#(tt,V1,V2)	→	activate^#(V2)	(64)
U31^#(tt,V1,V2)	→	U32^#(isNat(activate(V1)),activate(V2))	(57)
activate^#(n__and(X1,X2))	→	and^#(X1,X2)	(88)
U12^#(tt,V2)	→	activate^#(V2)	(104)
U12^#(tt,V2)	→	isNat^#(activate(V2))	(39)

1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[0^#]	=	0
[U32^#(x₁, x₂)]	=	max(x₂ + 3, 0)
[isNatKind(x₁)]	=	x₁ + 0
[U21(x₁, x₂)]	=	max(x₁ + 1, x₂ + 2, 0)
[U11(x₁, x₂, x₃)]	=	max(x₁ + 5, x₃ + 8, 0)
[s(x₁)]	=	x₁ + 0
[isNat^#(x₁)]	=	x₁ + 2
[activate(x₁)]	=	x₁ + 0
[U71(x₁, x₂, x₃)]	=	max(x₂ + 5, x₃ + 4, 0)
[n__isNatKind(x₁)]	=	x₁ + 0
[and(x₁, x₂)]	=	max(x₂ + 0, 0)
[plus^#(x₁, x₂)]	=	max(x₁ + 2, x₂ + 5, 0)
[activate^#(x₁)]	=	x₁ + 2
[U13^#(x₁)]	=	0
[U12(x₁, x₂)]	=	max(x₁ + 5, x₂ + 8, 0)
[U33^#(x₁)]	=	0
[x(x₁, x₂)]	=	max(x₁ + 4, x₂ + 5, 0)
[n__s(x₁)]	=	x₁ + 0
[U12^#(x₁, x₂)]	=	max(x₂ + 4, 0)
[0]	=	8856
[x^#(x₁, x₂)]	=	max(x₁ + 6, x₂ + 7, 0)
[s^#(x₁)]	=	0
[n__plus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 4, 0)
[U32(x₁, x₂)]	=	max(0)
[U33(x₁)]	=	0
[n__0]	=	8856
[isNat(x₁)]	=	x₁ + 4
[n__x(x₁, x₂)]	=	max(x₁ + 4, x₂ + 5, 0)
[plus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 4, 0)
[U61(x₁)]	=	8861
[U51^#(x₁, x₂, x₃)]	=	max(x₂ + 5, x₃ + 2, 0)
[U11^#(x₁, x₂, x₃)]	=	max(x₁ + 3, x₂ + 2, x₃ + 5, 0)
[U31(x₁, x₂, x₃)]	=	max(x₁ + 10, 0)
[U41^#(x₁, x₂)]	=	max(x₁ + 1, x₂ + 2, 0)
[U21^#(x₁, x₂)]	=	max(x₁ + 1, x₂ + 2, 0)
[U22^#(x₁)]	=	0
[tt]	=	2
[n__and(x₁, x₂)]	=	max(x₂ + 0, 0)
[U71^#(x₁, x₂, x₃)]	=	max(x₂ + 7, x₃ + 6, 0)
[U13(x₁)]	=	8
[U22(x₁)]	=	4
[U51(x₁, x₂, x₃)]	=	max(x₂ + 4, x₃ + 0, 0)
[isNatKind^#(x₁)]	=	x₁ + 2
[U41(x₁, x₂)]	=	max(x₂ + 0, 0)
[U31^#(x₁, x₂, x₃)]	=	max(x₃ + 5, 0)
[and^#(x₁, x₂)]	=	max(x₂ + 2, 0)
[U61^#(x₁)]	=	0

together with the usable rules

isNatKind(n__0)	→	tt	(18)
U13(tt)	→	tt	(3)
isNatKind(n__x(V1,V2))	→	and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))	(21)
activate(n__x(X1,X2))	→	x(X1,X2)	(36)
0	→	n__0	(26)
isNatKind(n__plus(V1,V2))	→	and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))	(19)
activate(n__0)	→	0	(32)
plus(X1,X2)	→	n__plus(X1,X2)	(27)
activate(n__isNatKind(X))	→	isNatKind(X)	(34)
plus(N,0)	→	U41(and(isNat(N),n__isNatKind(N)),N)	(22)
isNatKind(X)	→	n__isNatKind(X)	(28)
U22(tt)	→	tt	(5)
activate(n__plus(X1,X2))	→	plus(X1,X2)	(33)
U51(tt,M,N)	→	s(plus(activate(N),activate(M)))	(10)
isNatKind(n__s(V1))	→	isNatKind(activate(V1))	(20)
x(N,s(M))	→	U71(and(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N))),M,N)	(25)
x(X1,X2)	→	n__x(X1,X2)	(30)
isNat(n__0)	→	tt	(14)
and(X1,X2)	→	n__and(X1,X2)	(31)
U71(tt,M,N)	→	plus(x(activate(N),activate(M)),activate(N))	(12)
plus(N,s(M))	→	U51(and(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N))),M,N)	(23)
x(N,0)	→	U61(and(isNat(N),n__isNatKind(N)))	(24)
U61(tt)	→	0	(11)
U41(tt,N)	→	activate(N)	(9)
and(tt,X)	→	activate(X)	(13)
activate(X)	→	X	(38)
activate(n__and(X1,X2))	→	and(X1,X2)	(37)
activate(n__s(X))	→	s(X)	(35)
s(X)	→	n__s(X)	(29)
U12(tt,V2)	→	U13(isNat(activate(V2)))	(2)

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

isNat^#(n__plus(V1,V2))	→	activate^#(V2)	(53)
isNat^#(n__plus(V1,V2))	→	activate^#(V2)	(53)
isNat^#(n__plus(V1,V2))	→	and^#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))	(51)
U11^#(tt,V1,V2)	→	activate^#(V2)	(72)
U11^#(tt,V1,V2)	→	U12^#(isNat(activate(V1)),activate(V2))	(43)
isNatKind^#(n__x(V1,V2))	→	activate^#(V2)	(55)
isNatKind^#(n__x(V1,V2))	→	and^#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))	(54)
isNatKind^#(n__plus(V1,V2))	→	activate^#(V2)	(76)
isNatKind^#(n__plus(V1,V2))	→	and^#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))	(50)
isNat^#(n__x(V1,V2))	→	activate^#(V2)	(62)
isNat^#(n__x(V1,V2))	→	activate^#(V2)	(62)
isNat^#(n__x(V1,V2))	→	and^#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))	(44)
isNat^#(n__x(V1,V2))	→	U31^#(and(isNatKind(activate(V1)),n__isNatKind(activate(V2))),activate(V1),activate(V2))	(71)
U51^#(tt,M,N)	→	activate^#(M)	(83)
U32^#(tt,V2)	→	activate^#(V2)	(42)
U32^#(tt,V2)	→	isNat^#(activate(V2))	(92)
x^#(N,s(M))	→	isNat^#(M)	(41)
x^#(N,s(M))	→	and^#(isNat(M),n__isNatKind(M))	(90)
U71^#(tt,M,N)	→	activate^#(M)	(67)
plus^#(N,s(M))	→	isNat^#(M)	(97)
plus^#(N,s(M))	→	and^#(isNat(M),n__isNatKind(M))	(111)
U31^#(tt,V1,V2)	→	activate^#(V2)	(64)
U31^#(tt,V1,V2)	→	U32^#(isNat(activate(V1)),activate(V2))	(57)
U12^#(tt,V2)	→	activate^#(V2)	(104)
U12^#(tt,V2)	→	isNat^#(activate(V2))	(39)

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

U21^#(tt,V1)	→	activate^#(V1)	(75)
U21^#(tt,V1)	→	isNat^#(activate(V1))	(70)
isNat^#(n__plus(V1,V2))	→	activate^#(V1)	(48)
isNat^#(n__plus(V1,V2))	→	activate^#(V1)	(48)
isNat^#(n__plus(V1,V2))	→	isNatKind^#(activate(V1))	(87)
isNat^#(n__plus(V1,V2))	→	U11^#(and(isNatKind(activate(V1)),n__isNatKind(activate(V2))),activate(V1),activate(V2))	(68)
U11^#(tt,V1,V2)	→	activate^#(V1)	(100)
U11^#(tt,V1,V2)	→	isNat^#(activate(V1))	(60)
isNat^#(n__s(V1))	→	activate^#(V1)	(85)
isNat^#(n__s(V1))	→	activate^#(V1)	(85)
isNat^#(n__s(V1))	→	isNatKind^#(activate(V1))	(98)
isNat^#(n__s(V1))	→	U21^#(isNatKind(activate(V1)),activate(V1))	(78)
activate^#(n__x(X1,X2))	→	x^#(X1,X2)	(66)
isNatKind^#(n__plus(V1,V2))	→	activate^#(V1)	(59)
isNatKind^#(n__plus(V1,V2))	→	isNatKind^#(activate(V1))	(107)
activate^#(n__isNatKind(X))	→	isNatKind^#(X)	(89)
plus^#(N,0)	→	isNat^#(N)	(40)
plus^#(N,0)	→	and^#(isNat(N),n__isNatKind(N))	(45)
plus^#(N,0)	→	U41^#(and(isNat(N),n__isNatKind(N)),N)	(46)
activate^#(n__plus(X1,X2))	→	plus^#(X1,X2)	(61)
U51^#(tt,M,N)	→	activate^#(N)	(56)
U51^#(tt,M,N)	→	plus^#(activate(N),activate(M))	(47)
isNatKind^#(n__s(V1))	→	activate^#(V1)	(96)
isNatKind^#(n__s(V1))	→	isNatKind^#(activate(V1))	(74)
x^#(N,s(M))	→	U71^#(and(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N))),M,N)	(99)
U71^#(tt,M,N)	→	x^#(activate(N),activate(M))	(91)
U71^#(tt,M,N)	→	plus^#(x(activate(N),activate(M)),activate(N))	(102)
plus^#(N,s(M))	→	isNat^#(N)	(81)
plus^#(N,s(M))	→	and^#(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N)))	(95)
plus^#(N,s(M))	→	U51^#(and(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N))),M,N)	(103)
U41^#(tt,N)	→	activate^#(N)	(65)
and^#(tt,X)	→	activate^#(X)	(84)
activate^#(n__and(X1,X2))	→	and^#(X1,X2)	(88)

1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the argument filter

π(U32^#)	=	2
π(isNat^#)	=	1
π(activate)	=	1
π(and)	=	2
π(activate^#)	=	1
π(U33^#)	=	1
π(U32)	=	2
π(n__and)	=	2
π(U41)	=	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(isNatKind)	=	1	status(isNatKind)	=	[1]	list-extension(isNatKind)	=	Lex
prec(U21)	=	4	status(U21)	=	[1, 2]	list-extension(U21)	=	Lex
prec(U11)	=	3	status(U11)	=	[3]	list-extension(U11)	=	Lex
prec(s)	=	3	status(s)	=	[1]	list-extension(s)	=	Lex
prec(U71)	=	7	status(U71)	=	[2, 3, 1]	list-extension(U71)	=	Lex
prec(n__isNatKind)	=	1	status(n__isNatKind)	=	[1]	list-extension(n__isNatKind)	=	Lex
prec(plus^#)	=	3	status(plus^#)	=	[1]	list-extension(plus^#)	=	Lex
prec(U13^#)	=	0	status(U13^#)	=	[]	list-extension(U13^#)	=	Lex
prec(U12)	=	3	status(U12)	=	[2]	list-extension(U12)	=	Lex
prec(x)	=	7	status(x)	=	[2, 1]	list-extension(x)	=	Lex
prec(n__s)	=	3	status(n__s)	=	[1]	list-extension(n__s)	=	Lex
prec(U12^#)	=	0	status(U12^#)	=	[2, 1]	list-extension(U12^#)	=	Lex
prec(0)	=	0	status(0)	=	[]	list-extension(0)	=	Lex
prec(x^#)	=	7	status(x^#)	=	[2, 1]	list-extension(x^#)	=	Lex
prec(s^#)	=	0	status(s^#)	=	[]	list-extension(s^#)	=	Lex
prec(n__plus)	=	4	status(n__plus)	=	[2, 1]	list-extension(n__plus)	=	Lex
prec(U33)	=	5	status(U33)	=	[1]	list-extension(U33)	=	Lex
prec(n__0)	=	0	status(n__0)	=	[]	list-extension(n__0)	=	Lex
prec(isNat)	=	3	status(isNat)	=	[]	list-extension(isNat)	=	Lex
prec(n__x)	=	7	status(n__x)	=	[2, 1]	list-extension(n__x)	=	Lex
prec(plus)	=	4	status(plus)	=	[2, 1]	list-extension(plus)	=	Lex
prec(U61)	=	0	status(U61)	=	[1]	list-extension(U61)	=	Lex
prec(U51^#)	=	3	status(U51^#)	=	[3]	list-extension(U51^#)	=	Lex
prec(U11^#)	=	2	status(U11^#)	=	[2]	list-extension(U11^#)	=	Lex
prec(U31)	=	3	status(U31)	=	[1, 2, 3]	list-extension(U31)	=	Lex
prec(U41^#)	=	2	status(U41^#)	=	[1, 2]	list-extension(U41^#)	=	Lex
prec(U21^#)	=	2	status(U21^#)	=	[2, 1]	list-extension(U21^#)	=	Lex
prec(U22^#)	=	0	status(U22^#)	=	[]	list-extension(U22^#)	=	Lex
prec(tt)	=	1	status(tt)	=	[]	list-extension(tt)	=	Lex
prec(U71^#)	=	7	status(U71^#)	=	[2, 3, 1]	list-extension(U71^#)	=	Lex
prec(U13)	=	3	status(U13)	=	[]	list-extension(U13)	=	Lex
prec(U22)	=	1	status(U22)	=	[]	list-extension(U22)	=	Lex
prec(U51)	=	4	status(U51)	=	[2, 3, 1]	list-extension(U51)	=	Lex
prec(isNatKind^#)	=	0	status(isNatKind^#)	=	[1]	list-extension(isNatKind^#)	=	Lex
prec(U31^#)	=	0	status(U31^#)	=	[3, 2, 1]	list-extension(U31^#)	=	Lex
prec(U61^#)	=	0	status(U61^#)	=	[]	list-extension(U61^#)	=	Lex

and the following Max-polynomial interpretation

[0^#]	=	0
[isNatKind(x₁)]	=	x₁ + 0
[U21(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[U11(x₁, x₂, x₃)]	=	max(x₃ + 0, 0)
[s(x₁)]	=	x₁ + 0
[U71(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 0, 0)
[n__isNatKind(x₁)]	=	x₁ + 0
[plus^#(x₁, x₂)]	=	max(x₁ + 0, 0)
[U13^#(x₁)]	=	0
[U12(x₁, x₂)]	=	max(x₂ + 0, 0)
[x(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[n__s(x₁)]	=	x₁ + 0
[U12^#(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 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)
[U33(x₁)]	=	x₁ + 0
[n__0]	=	0
[isNat(x₁)]	=	0
[n__x(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[plus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[U61(x₁)]	=	x₁ + 0
[U51^#(x₁, x₂, x₃)]	=	max(x₃ + 0, 0)
[U11^#(x₁, x₂, x₃)]	=	max(x₂ + 0, 0)
[U31(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 0, 0)
[U41^#(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[U21^#(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[U22^#(x₁)]	=	0
[tt]	=	0
[U71^#(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 0, 0)
[U13(x₁)]	=	0
[U22(x₁)]	=	0
[U51(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 0, 0)
[isNatKind^#(x₁)]	=	x₁ + 0
[U31^#(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 0, 0)
[U61^#(x₁)]	=	0

together with the usable rules

isNatKind(n__0)	→	tt	(18)
isNatKind(n__x(V1,V2))	→	and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))	(21)
activate(n__x(X1,X2))	→	x(X1,X2)	(36)
0	→	n__0	(26)
isNatKind(n__plus(V1,V2))	→	and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))	(19)
activate(n__0)	→	0	(32)
plus(X1,X2)	→	n__plus(X1,X2)	(27)
activate(n__isNatKind(X))	→	isNatKind(X)	(34)
plus(N,0)	→	U41(and(isNat(N),n__isNatKind(N)),N)	(22)
isNatKind(X)	→	n__isNatKind(X)	(28)
activate(n__plus(X1,X2))	→	plus(X1,X2)	(33)
U51(tt,M,N)	→	s(plus(activate(N),activate(M)))	(10)
isNatKind(n__s(V1))	→	isNatKind(activate(V1))	(20)
x(N,s(M))	→	U71(and(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N))),M,N)	(25)
x(X1,X2)	→	n__x(X1,X2)	(30)
and(X1,X2)	→	n__and(X1,X2)	(31)
U71(tt,M,N)	→	plus(x(activate(N),activate(M)),activate(N))	(12)
plus(N,s(M))	→	U51(and(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N))),M,N)	(23)
x(N,0)	→	U61(and(isNat(N),n__isNatKind(N)))	(24)
U61(tt)	→	0	(11)
U41(tt,N)	→	activate(N)	(9)
and(tt,X)	→	activate(X)	(13)
activate(X)	→	X	(38)
activate(n__and(X1,X2))	→	and(X1,X2)	(37)
activate(n__s(X))	→	s(X)	(35)
s(X)	→	n__s(X)	(29)

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

U21^#(tt,V1)	→	activate^#(V1)	(75)
U21^#(tt,V1)	→	isNat^#(activate(V1))	(70)
isNat^#(n__plus(V1,V2))	→	activate^#(V1)	(48)
isNat^#(n__plus(V1,V2))	→	activate^#(V1)	(48)
isNat^#(n__plus(V1,V2))	→	isNatKind^#(activate(V1))	(87)
isNat^#(n__plus(V1,V2))	→	U11^#(and(isNatKind(activate(V1)),n__isNatKind(activate(V2))),activate(V1),activate(V2))	(68)
U11^#(tt,V1,V2)	→	activate^#(V1)	(100)
U11^#(tt,V1,V2)	→	isNat^#(activate(V1))	(60)
isNat^#(n__s(V1))	→	activate^#(V1)	(85)
isNat^#(n__s(V1))	→	activate^#(V1)	(85)
isNat^#(n__s(V1))	→	isNatKind^#(activate(V1))	(98)
isNat^#(n__s(V1))	→	U21^#(isNatKind(activate(V1)),activate(V1))	(78)
isNatKind^#(n__plus(V1,V2))	→	activate^#(V1)	(59)
isNatKind^#(n__plus(V1,V2))	→	isNatKind^#(activate(V1))	(107)
activate^#(n__isNatKind(X))	→	isNatKind^#(X)	(89)
plus^#(N,0)	→	isNat^#(N)	(40)
plus^#(N,0)	→	and^#(isNat(N),n__isNatKind(N))	(45)
plus^#(N,0)	→	U41^#(and(isNat(N),n__isNatKind(N)),N)	(46)
activate^#(n__plus(X1,X2))	→	plus^#(X1,X2)	(61)
U51^#(tt,M,N)	→	activate^#(N)	(56)
isNatKind^#(n__s(V1))	→	activate^#(V1)	(96)
isNatKind^#(n__s(V1))	→	isNatKind^#(activate(V1))	(74)
x^#(N,s(M))	→	U71^#(and(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N))),M,N)	(99)
U71^#(tt,M,N)	→	x^#(activate(N),activate(M))	(91)
U71^#(tt,M,N)	→	plus^#(x(activate(N),activate(M)),activate(N))	(102)
plus^#(N,s(M))	→	isNat^#(N)	(81)
plus^#(N,s(M))	→	and^#(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N)))	(95)
U41^#(tt,N)	→	activate^#(N)	(65)

could be deleted.

1.1.1.1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.

The 1^st component contains the pair

U51^#(tt,M,N)	→	plus^#(activate(N),activate(M))	(47)
plus^#(N,s(M))	→	U51^#(and(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N))),M,N)	(103)

1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the argument filter

π(U32^#)	=	2
π(isNat^#)	=	1
π(activate)	=	1
π(and)	=	2
π(activate^#)	=	1
π(U33^#)	=	1
π(U32)	=	2
π(n__and)	=	2
π(U41)	=	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(isNatKind)	=	1	status(isNatKind)	=	[1]	list-extension(isNatKind)	=	Lex
prec(U21)	=	4	status(U21)	=	[1, 2]	list-extension(U21)	=	Lex
prec(U11)	=	3	status(U11)	=	[3]	list-extension(U11)	=	Lex
prec(s)	=	3	status(s)	=	[1]	list-extension(s)	=	Lex
prec(U71)	=	7	status(U71)	=	[2, 3, 1]	list-extension(U71)	=	Lex
prec(n__isNatKind)	=	1	status(n__isNatKind)	=	[1]	list-extension(n__isNatKind)	=	Lex
prec(plus^#)	=	1	status(plus^#)	=	[2]	list-extension(plus^#)	=	Lex
prec(U13^#)	=	0	status(U13^#)	=	[]	list-extension(U13^#)	=	Lex
prec(U12)	=	3	status(U12)	=	[2]	list-extension(U12)	=	Lex
prec(x)	=	7	status(x)	=	[2, 1]	list-extension(x)	=	Lex
prec(n__s)	=	3	status(n__s)	=	[1]	list-extension(n__s)	=	Lex
prec(U12^#)	=	0	status(U12^#)	=	[2, 1]	list-extension(U12^#)	=	Lex
prec(0)	=	0	status(0)	=	[]	list-extension(0)	=	Lex
prec(x^#)	=	7	status(x^#)	=	[2, 1]	list-extension(x^#)	=	Lex
prec(s^#)	=	0	status(s^#)	=	[]	list-extension(s^#)	=	Lex
prec(n__plus)	=	4	status(n__plus)	=	[2, 1]	list-extension(n__plus)	=	Lex
prec(U33)	=	5	status(U33)	=	[1]	list-extension(U33)	=	Lex
prec(n__0)	=	0	status(n__0)	=	[]	list-extension(n__0)	=	Lex
prec(isNat)	=	3	status(isNat)	=	[]	list-extension(isNat)	=	Lex
prec(n__x)	=	7	status(n__x)	=	[2, 1]	list-extension(n__x)	=	Lex
prec(plus)	=	4	status(plus)	=	[2, 1]	list-extension(plus)	=	Lex
prec(U61)	=	0	status(U61)	=	[1]	list-extension(U61)	=	Lex
prec(U51^#)	=	2	status(U51^#)	=	[2]	list-extension(U51^#)	=	Lex
prec(U11^#)	=	2	status(U11^#)	=	[2]	list-extension(U11^#)	=	Lex
prec(U31)	=	3	status(U31)	=	[1, 2, 3]	list-extension(U31)	=	Lex
prec(U41^#)	=	2	status(U41^#)	=	[1, 2]	list-extension(U41^#)	=	Lex
prec(U21^#)	=	2	status(U21^#)	=	[2, 1]	list-extension(U21^#)	=	Lex
prec(U22^#)	=	0	status(U22^#)	=	[]	list-extension(U22^#)	=	Lex
prec(tt)	=	1	status(tt)	=	[]	list-extension(tt)	=	Lex
prec(U71^#)	=	7	status(U71^#)	=	[2, 3, 1]	list-extension(U71^#)	=	Lex
prec(U13)	=	3	status(U13)	=	[]	list-extension(U13)	=	Lex
prec(U22)	=	1	status(U22)	=	[]	list-extension(U22)	=	Lex
prec(U51)	=	4	status(U51)	=	[2, 3, 1]	list-extension(U51)	=	Lex
prec(isNatKind^#)	=	0	status(isNatKind^#)	=	[1]	list-extension(isNatKind^#)	=	Lex
prec(U31^#)	=	0	status(U31^#)	=	[3, 2, 1]	list-extension(U31^#)	=	Lex
prec(U61^#)	=	0	status(U61^#)	=	[]	list-extension(U61^#)	=	Lex

and the following Max-polynomial interpretation

[0^#]	=	0
[isNatKind(x₁)]	=	x₁ + 0
[U21(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[U11(x₁, x₂, x₃)]	=	max(x₃ + 0, 0)
[s(x₁)]	=	x₁ + 0
[U71(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 0, 0)
[n__isNatKind(x₁)]	=	x₁ + 0
[plus^#(x₁, x₂)]	=	max(x₂ + 0, 0)
[U13^#(x₁)]	=	0
[U12(x₁, x₂)]	=	max(x₂ + 0, 0)
[x(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[n__s(x₁)]	=	x₁ + 0
[U12^#(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 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)
[U33(x₁)]	=	x₁ + 0
[n__0]	=	0
[isNat(x₁)]	=	0
[n__x(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[plus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[U61(x₁)]	=	x₁ + 0
[U51^#(x₁, x₂, x₃)]	=	max(x₂ + 0, 0)
[U11^#(x₁, x₂, x₃)]	=	max(x₂ + 0, 0)
[U31(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 0, 0)
[U41^#(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[U21^#(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[U22^#(x₁)]	=	0
[tt]	=	0
[U71^#(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 0, 0)
[U13(x₁)]	=	0
[U22(x₁)]	=	0
[U51(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 0, 0)
[isNatKind^#(x₁)]	=	x₁ + 0
[U31^#(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 0, 0)
[U61^#(x₁)]	=	0

together with the usable rules

isNatKind(n__0)	→	tt	(18)
isNatKind(n__x(V1,V2))	→	and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))	(21)
activate(n__x(X1,X2))	→	x(X1,X2)	(36)
0	→	n__0	(26)
isNatKind(n__plus(V1,V2))	→	and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))	(19)
activate(n__0)	→	0	(32)
plus(X1,X2)	→	n__plus(X1,X2)	(27)
activate(n__isNatKind(X))	→	isNatKind(X)	(34)
plus(N,0)	→	U41(and(isNat(N),n__isNatKind(N)),N)	(22)
isNatKind(X)	→	n__isNatKind(X)	(28)
activate(n__plus(X1,X2))	→	plus(X1,X2)	(33)
U51(tt,M,N)	→	s(plus(activate(N),activate(M)))	(10)
isNatKind(n__s(V1))	→	isNatKind(activate(V1))	(20)
x(N,s(M))	→	U71(and(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N))),M,N)	(25)
x(X1,X2)	→	n__x(X1,X2)	(30)
and(X1,X2)	→	n__and(X1,X2)	(31)
U71(tt,M,N)	→	plus(x(activate(N),activate(M)),activate(N))	(12)
plus(N,s(M))	→	U51(and(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N))),M,N)	(23)
x(N,0)	→	U61(and(isNat(N),n__isNatKind(N)))	(24)
U61(tt)	→	0	(11)
U41(tt,N)	→	activate(N)	(9)
and(tt,X)	→	activate(X)	(13)
activate(X)	→	X	(38)
activate(n__and(X1,X2))	→	and(X1,X2)	(37)
activate(n__s(X))	→	s(X)	(35)
s(X)	→	n__s(X)	(29)

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

U51^#(tt,M,N)	→	plus^#(activate(N),activate(M))	(47)
plus^#(N,s(M))	→	U51^#(and(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N))),M,N)	(103)

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.

The 2^nd component contains the pair

and^#(tt,X)	→	activate^#(X)	(84)
activate^#(n__and(X1,X2))	→	and^#(X1,X2)	(88)

1.1.1.1.1.1.1.1.1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[0^#]	=	0
[U32^#(x₁, x₂)]	=	2
[isNatKind(x₁)]	=	18254
[U21(x₁, x₂)]	=	18250
[U11(x₁, x₂, x₃)]	=	18250
[s(x₁)]	=	18254
[isNat^#(x₁)]	=	3
[activate(x₁)]	=	18253
[U71(x₁, x₂, x₃)]	=	x₁ + 0
[n__isNatKind(x₁)]	=	18255
[and(x₁, x₂)]	=	x₁ + x₂ + 0
[plus^#(x₁, x₂)]	=	3
[activate^#(x₁)]	=	x₁ + 3
[U13^#(x₁)]	=	0
[U12(x₁, x₂)]	=	18250
[U33^#(x₁)]	=	0
[x(x₁, x₂)]	=	x₁ + 18254
[n__s(x₁)]	=	45388
[U12^#(x₁, x₂)]	=	2
[0]	=	18256
[x^#(x₁, x₂)]	=	3
[s^#(x₁)]	=	0
[n__plus(x₁, x₂)]	=	x₁ + 18252
[U32(x₁, x₂)]	=	18250
[U33(x₁)]	=	18250
[n__0]	=	18257
[isNat(x₁)]	=	x₁ + 1
[n__x(x₁, x₂)]	=	35788
[plus(x₁, x₂)]	=	18251
[U61(x₁)]	=	18255
[U51^#(x₁, x₂, x₃)]	=	2
[U11^#(x₁, x₂, x₃)]	=	3
[U31(x₁, x₂, x₃)]	=	18250
[U41^#(x₁, x₂)]	=	3
[U21^#(x₁, x₂)]	=	3
[U22^#(x₁)]	=	0
[tt]	=	18250
[n__and(x₁, x₂)]	=	x₁ + x₂ + 2
[U71^#(x₁, x₂, x₃)]	=	3
[U13(x₁)]	=	18250
[U22(x₁)]	=	18250
[U51(x₁, x₂, x₃)]	=	18253
[isNatKind^#(x₁)]	=	3
[U41(x₁, x₂)]	=	x₂ + 18252
[U31^#(x₁, x₂, x₃)]	=	1
[and^#(x₁, x₂)]	=	x₂ + 4
[U61^#(x₁)]	=	0

together with the usable rules

U21(tt,V1)	→	U22(isNat(activate(V1)))	(4)
isNat(n__plus(V1,V2))	→	U11(and(isNatKind(activate(V1)),n__isNatKind(activate(V2))),activate(V1),activate(V2))	(15)
U33(tt)	→	tt	(8)
U11(tt,V1,V2)	→	U12(isNat(activate(V1)),activate(V2))	(1)
U13(tt)	→	tt	(3)
isNat(n__s(V1))	→	U21(isNatKind(activate(V1)),activate(V1))	(16)
isNat(n__x(V1,V2))	→	U31(and(isNatKind(activate(V1)),n__isNatKind(activate(V2))),activate(V1),activate(V2))	(17)
U22(tt)	→	tt	(5)
U32(tt,V2)	→	U33(isNat(activate(V2)))	(7)
isNat(n__0)	→	tt	(14)
U31(tt,V1,V2)	→	U32(isNat(activate(V1)),activate(V2))	(6)
U12(tt,V2)	→	U13(isNat(activate(V2)))	(2)

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

and^#(tt,X)	→	activate^#(X)	(84)
activate^#(n__and(X1,X2))	→	and^#(X1,X2)	(88)

could be deleted.

1.1.1.1.1.1.1.1.1.1.2.1 Dependency Graph Processor

The dependency pairs are split into 0 components.