Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/MYNAT_complete_FR)

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(n__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(n__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)
isNat(X)	→	n__isNat(X)	(32)
activate(n__0)	→	0	(33)
activate(n__plus(X1,X2))	→	plus(activate(X1),activate(X2))	(34)
activate(n__isNatKind(X))	→	isNatKind(X)	(35)
activate(n__s(X))	→	s(activate(X))	(36)
activate(n__x(X1,X2))	→	x(activate(X1),activate(X2))	(37)
activate(n__and(X1,X2))	→	and(activate(X1),X2)	(38)
activate(n__isNat(X))	→	isNat(X)	(39)
activate(X)	→	X	(40)

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

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

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

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[0^#]	=	0
[U32^#(x₁, x₂)]	=	max(x₂ + 1, 0)
[isNatKind(x₁)]	=	x₁ + 0
[U21(x₁, x₂)]	=	max(0)
[U11(x₁, x₂, x₃)]	=	max(0)
[s(x₁)]	=	x₁ + 0
[isNat^#(x₁)]	=	x₁ + 0
[activate(x₁)]	=	x₁ + 0
[U71(x₁, x₂, x₃)]	=	max(x₂ + 3, x₃ + 27860, 0)
[n__isNatKind(x₁)]	=	x₁ + 0
[and(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[plus^#(x₁, x₂)]	=	max(x₁ + 0, x₂ + 1, 0)
[activate^#(x₁)]	=	x₁ + 0
[U13^#(x₁)]	=	0
[U12(x₁, x₂)]	=	max(0)
[U33^#(x₁)]	=	0
[x(x₁, x₂)]	=	max(x₁ + 27860, x₂ + 3, 0)
[n__s(x₁)]	=	x₁ + 0
[U12^#(x₁, x₂)]	=	max(x₂ + 1, 0)
[0]	=	0
[x^#(x₁, x₂)]	=	max(x₁ + 27860, x₂ + 3, 0)
[s^#(x₁)]	=	0
[n__isNat(x₁)]	=	x₁ + 0
[n__plus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 2, 0)
[U32(x₁, x₂)]	=	max(x₁ + 1, 0)
[U33(x₁)]	=	0
[n__0]	=	0
[isNat(x₁)]	=	x₁ + 0
[n__x(x₁, x₂)]	=	max(x₁ + 27860, x₂ + 3, 0)
[plus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 2, 0)
[U61(x₁)]	=	3
[U51^#(x₁, x₂, x₃)]	=	max(x₂ + 1, x₃ + 0, 0)
[U11^#(x₁, x₂, x₃)]	=	max(x₂ + 0, x₃ + 2, 0)
[U31(x₁, x₂, x₃)]	=	max(x₂ + 4, 0)
[U41^#(x₁, x₂)]	=	max(x₂ + 0, 0)
[U21^#(x₁, x₂)]	=	max(x₂ + 0, 0)
[U22^#(x₁)]	=	0
[tt]	=	0
[n__and(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[U71^#(x₁, x₂, x₃)]	=	max(x₁ + 3, x₂ + 3, x₃ + 27860, 0)
[U13(x₁)]	=	0
[U22(x₁)]	=	0
[U51(x₁, x₂, x₃)]	=	max(x₂ + 2, x₃ + 0, 0)
[isNatKind^#(x₁)]	=	x₁ + 0
[U41(x₁, x₂)]	=	max(x₂ + 0, 0)
[U31^#(x₁, x₂, x₃)]	=	max(x₂ + 27860, x₃ + 2, 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__s(X))	→	s(activate(X))	(36)
0	→	n__0	(26)
isNatKind(n__plus(V1,V2))	→	and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))	(19)
isNat(X)	→	n__isNat(X)	(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__plus(X1,X2))	→	plus(activate(X1),activate(X2))	(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__0)	→	0	(33)
U51(tt,M,N)	→	s(plus(activate(N),activate(M)))	(10)
activate(n__isNat(X))	→	isNat(X)	(39)
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(n__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(n__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	(40)
U31(tt,V1,V2)	→	U32(isNat(activate(V1)),activate(V2))	(6)
activate(n__and(X1,X2))	→	and(activate(X1),X2)	(38)
activate(n__x(X1,X2))	→	x(activate(X1),activate(X2))	(37)
activate(n__isNatKind(X))	→	isNatKind(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

x^#(N,0)	→	and^#(isNat(N),n__isNatKind(N))	(118)
isNat^#(n__x(V1,V2))	→	isNatKind^#(activate(V1))	(84)
activate^#(n__plus(X1,X2))	→	activate^#(X2)	(85)
x^#(N,s(M))	→	and^#(and(isNat(M),n__isNatKind(M)),n__and(n__isNat(N),n__isNatKind(N)))	(83)
isNat^#(n__plus(V1,V2))	→	activate^#(V2)	(74)
isNat^#(n__x(V1,V2))	→	activate^#(V2)	(79)
x^#(N,s(M))	→	and^#(isNat(M),n__isNatKind(M))	(78)
U31^#(tt,V1,V2)	→	activate^#(V1)	(77)
isNat^#(n__x(V1,V2))	→	activate^#(V2)	(79)
isNat^#(n__plus(V1,V2))	→	activate^#(V2)	(74)
plus^#(N,s(M))	→	isNat^#(M)	(73)
U12^#(tt,V2)	→	activate^#(V2)	(111)
isNat^#(n__plus(V1,V2))	→	and^#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))	(70)
U32^#(tt,V2)	→	isNat^#(activate(V2))	(108)
isNatKind^#(n__plus(V1,V2))	→	and^#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))	(69)
U71^#(tt,M,N)	→	activate^#(N)	(97)
U31^#(tt,V1,V2)	→	isNat^#(activate(V1))	(68)
U31^#(tt,V1,V2)	→	activate^#(V2)	(66)
isNatKind^#(n__x(V1,V2))	→	and^#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))	(106)
isNat^#(n__x(V1,V2))	→	and^#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))	(65)
x^#(N,s(M))	→	isNat^#(M)	(104)
x^#(N,0)	→	isNat^#(N)	(105)
isNat^#(n__x(V1,V2))	→	activate^#(V1)	(53)
isNatKind^#(n__plus(V1,V2))	→	activate^#(V2)	(102)
activate^#(n__x(X1,X2))	→	activate^#(X1)	(61)
U71^#(tt,M,N)	→	activate^#(M)	(101)
U11^#(tt,V1,V2)	→	activate^#(V2)	(57)
U11^#(tt,V1,V2)	→	U12^#(isNat(activate(V1)),activate(V2))	(54)
plus^#(N,s(M))	→	and^#(isNat(M),n__isNatKind(M))	(98)
isNat^#(n__x(V1,V2))	→	activate^#(V1)	(53)
U71^#(tt,M,N)	→	activate^#(N)	(97)
isNatKind^#(n__x(V1,V2))	→	activate^#(V1)	(96)
U32^#(tt,V2)	→	activate^#(V2)	(50)
isNatKind^#(n__x(V1,V2))	→	isNatKind^#(activate(V1))	(91)
U51^#(tt,M,N)	→	activate^#(M)	(48)
U31^#(tt,V1,V2)	→	U32^#(isNat(activate(V1)),activate(V2))	(90)
isNatKind^#(n__x(V1,V2))	→	activate^#(V2)	(46)
activate^#(n__x(X1,X2))	→	activate^#(X2)	(88)
U12^#(tt,V2)	→	isNat^#(activate(V2))	(41)

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)	(100)
U21^#(tt,V1)	→	isNat^#(activate(V1))	(45)
isNat^#(n__plus(V1,V2))	→	activate^#(V1)	(75)
isNat^#(n__plus(V1,V2))	→	activate^#(V1)	(75)
isNat^#(n__plus(V1,V2))	→	isNatKind^#(activate(V1))	(112)
isNat^#(n__plus(V1,V2))	→	U11^#(and(isNatKind(activate(V1)),n__isNatKind(activate(V2))),activate(V1),activate(V2))	(56)
U11^#(tt,V1,V2)	→	activate^#(V1)	(51)
U11^#(tt,V1,V2)	→	isNat^#(activate(V1))	(93)
isNat^#(n__s(V1))	→	activate^#(V1)	(72)
isNat^#(n__s(V1))	→	activate^#(V1)	(72)
isNat^#(n__s(V1))	→	isNatKind^#(activate(V1))	(107)
isNat^#(n__s(V1))	→	U21^#(isNatKind(activate(V1)),activate(V1))	(63)
activate^#(n__s(X))	→	activate^#(X)	(82)
isNatKind^#(n__plus(V1,V2))	→	activate^#(V1)	(62)
isNatKind^#(n__plus(V1,V2))	→	isNatKind^#(activate(V1))	(58)
activate^#(n__plus(X1,X2))	→	activate^#(X1)	(55)
activate^#(n__plus(X1,X2))	→	plus^#(activate(X1),activate(X2))	(52)
plus^#(N,0)	→	isNat^#(N)	(47)
plus^#(N,0)	→	and^#(isNat(N),n__isNatKind(N))	(76)
plus^#(N,0)	→	U41^#(and(isNat(N),n__isNatKind(N)),N)	(95)
U51^#(tt,M,N)	→	activate^#(N)	(49)
U51^#(tt,M,N)	→	plus^#(activate(N),activate(M))	(64)
activate^#(n__isNat(X))	→	isNat^#(X)	(60)
isNatKind^#(n__s(V1))	→	activate^#(V1)	(99)
isNatKind^#(n__s(V1))	→	isNatKind^#(activate(V1))	(92)
x^#(N,s(M))	→	U71^#(and(and(isNat(M),n__isNatKind(M)),n__and(n__isNat(N),n__isNatKind(N))),M,N)	(43)
U71^#(tt,M,N)	→	x^#(activate(N),activate(M))	(86)
U71^#(tt,M,N)	→	plus^#(x(activate(N),activate(M)),activate(N))	(71)
plus^#(N,s(M))	→	and^#(and(isNat(M),n__isNatKind(M)),n__and(n__isNat(N),n__isNatKind(N)))	(109)
plus^#(N,s(M))	→	U51^#(and(and(isNat(M),n__isNatKind(M)),n__and(n__isNat(N),n__isNatKind(N))),M,N)	(87)
U41^#(tt,N)	→	activate^#(N)	(115)
and^#(tt,X)	→	activate^#(X)	(81)
activate^#(n__and(X1,X2))	→	activate^#(X1)	(67)
activate^#(n__and(X1,X2))	→	and^#(activate(X1),X2)	(114)
activate^#(n__x(X1,X2))	→	x^#(activate(X1),activate(X2))	(94)
activate^#(n__isNatKind(X))	→	isNatKind^#(X)	(116)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the argument filter

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

and the following Max-polynomial interpretation

[0^#]	=	0
[U32^#(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[U11(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 0, 0)
[s(x₁)]	=	x₁ + 0
[isNat^#(x₁)]	=	x₁ + 0
[U71(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 0, 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, x₂ + 0, 0)
[U33^#(x₁)]	=	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)
[n__plus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[U33(x₁)]	=	0
[n__0]	=	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, x₂ + 0, x₃ + 0, 0)
[U11^#(x₁, x₂, x₃)]	=	max(x₂ + 0, 0)
[U41^#(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[U21^#(x₁, x₂)]	=	max(x₂ + 0, 0)
[tt]	=	0
[n__and(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[U71^#(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 0, 0)
[U13(x₁)]	=	0
[U51(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, 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__s(X))	→	s(activate(X))	(36)
0	→	n__0	(26)
isNatKind(n__plus(V1,V2))	→	and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))	(19)
isNat(X)	→	n__isNat(X)	(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__plus(X1,X2))	→	plus(activate(X1),activate(X2))	(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__0)	→	0	(33)
U51(tt,M,N)	→	s(plus(activate(N),activate(M)))	(10)
activate(n__isNat(X))	→	isNat(X)	(39)
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(n__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(n__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	(40)
U31(tt,V1,V2)	→	U32(isNat(activate(V1)),activate(V2))	(6)
activate(n__and(X1,X2))	→	and(activate(X1),X2)	(38)
activate(n__x(X1,X2))	→	x(activate(X1),activate(X2))	(37)
activate(n__isNatKind(X))	→	isNatKind(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

U21^#(tt,V1)	→	activate^#(V1)	(100)
U21^#(tt,V1)	→	isNat^#(activate(V1))	(45)
isNat^#(n__plus(V1,V2))	→	activate^#(V1)	(75)
isNat^#(n__plus(V1,V2))	→	activate^#(V1)	(75)
isNat^#(n__plus(V1,V2))	→	isNatKind^#(activate(V1))	(112)
isNat^#(n__plus(V1,V2))	→	U11^#(and(isNatKind(activate(V1)),n__isNatKind(activate(V2))),activate(V1),activate(V2))	(56)
U11^#(tt,V1,V2)	→	isNat^#(activate(V1))	(93)
isNat^#(n__s(V1))	→	activate^#(V1)	(72)
isNat^#(n__s(V1))	→	activate^#(V1)	(72)
isNat^#(n__s(V1))	→	isNatKind^#(activate(V1))	(107)
isNat^#(n__s(V1))	→	U21^#(isNatKind(activate(V1)),activate(V1))	(63)
activate^#(n__s(X))	→	activate^#(X)	(82)
isNatKind^#(n__plus(V1,V2))	→	activate^#(V1)	(62)
isNatKind^#(n__plus(V1,V2))	→	isNatKind^#(activate(V1))	(58)
activate^#(n__plus(X1,X2))	→	activate^#(X1)	(55)
activate^#(n__plus(X1,X2))	→	plus^#(activate(X1),activate(X2))	(52)
plus^#(N,0)	→	isNat^#(N)	(47)
plus^#(N,0)	→	and^#(isNat(N),n__isNatKind(N))	(76)
plus^#(N,0)	→	U41^#(and(isNat(N),n__isNatKind(N)),N)	(95)
U51^#(tt,M,N)	→	activate^#(N)	(49)
U51^#(tt,M,N)	→	plus^#(activate(N),activate(M))	(64)
activate^#(n__isNat(X))	→	isNat^#(X)	(60)
isNatKind^#(n__s(V1))	→	activate^#(V1)	(99)
isNatKind^#(n__s(V1))	→	isNatKind^#(activate(V1))	(92)
x^#(N,s(M))	→	U71^#(and(and(isNat(M),n__isNatKind(M)),n__and(n__isNat(N),n__isNatKind(N))),M,N)	(43)
U71^#(tt,M,N)	→	x^#(activate(N),activate(M))	(86)
U71^#(tt,M,N)	→	plus^#(x(activate(N),activate(M)),activate(N))	(71)
plus^#(N,s(M))	→	and^#(and(isNat(M),n__isNatKind(M)),n__and(n__isNat(N),n__isNatKind(N)))	(109)
plus^#(N,s(M))	→	U51^#(and(and(isNat(M),n__isNatKind(M)),n__and(n__isNat(N),n__isNatKind(N))),M,N)	(87)
U41^#(tt,N)	→	activate^#(N)	(115)
activate^#(n__and(X1,X2))	→	activate^#(X1)	(67)
activate^#(n__and(X1,X2))	→	and^#(activate(X1),X2)	(114)
activate^#(n__x(X1,X2))	→	x^#(activate(X1),activate(X2))	(94)
activate^#(n__isNatKind(X))	→	isNatKind^#(X)	(116)

could be deleted.

1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.