Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/PEANO_complete-noand_Z)

The rewrite relation of the following TRS is considered.

U11(tt,V1,V2)	→	U12(isNatKind(activate(V1)),activate(V1),activate(V2))	(1)
U12(tt,V1,V2)	→	U13(isNatKind(activate(V2)),activate(V1),activate(V2))	(2)
U13(tt,V1,V2)	→	U14(isNatKind(activate(V2)),activate(V1),activate(V2))	(3)
U14(tt,V1,V2)	→	U15(isNat(activate(V1)),activate(V2))	(4)
U15(tt,V2)	→	U16(isNat(activate(V2)))	(5)
U16(tt)	→	tt	(6)
U21(tt,V1)	→	U22(isNatKind(activate(V1)),activate(V1))	(7)
U22(tt,V1)	→	U23(isNat(activate(V1)))	(8)
U23(tt)	→	tt	(9)
U31(tt,V2)	→	U32(isNatKind(activate(V2)))	(10)
U32(tt)	→	tt	(11)
U41(tt)	→	tt	(12)
U51(tt,N)	→	U52(isNatKind(activate(N)),activate(N))	(13)
U52(tt,N)	→	activate(N)	(14)
U61(tt,M,N)	→	U62(isNatKind(activate(M)),activate(M),activate(N))	(15)
U62(tt,M,N)	→	U63(isNat(activate(N)),activate(M),activate(N))	(16)
U63(tt,M,N)	→	U64(isNatKind(activate(N)),activate(M),activate(N))	(17)
U64(tt,M,N)	→	s(plus(activate(N),activate(M)))	(18)
isNat(n__0)	→	tt	(19)
isNat(n__plus(V1,V2))	→	U11(isNatKind(activate(V1)),activate(V1),activate(V2))	(20)
isNat(n__s(V1))	→	U21(isNatKind(activate(V1)),activate(V1))	(21)
isNatKind(n__0)	→	tt	(22)
isNatKind(n__plus(V1,V2))	→	U31(isNatKind(activate(V1)),activate(V2))	(23)
isNatKind(n__s(V1))	→	U41(isNatKind(activate(V1)))	(24)
plus(N,0)	→	U51(isNat(N),N)	(25)
plus(N,s(M))	→	U61(isNat(M),M,N)	(26)
0	→	n__0	(27)
plus(X1,X2)	→	n__plus(X1,X2)	(28)
s(X)	→	n__s(X)	(29)
activate(n__0)	→	0	(30)
activate(n__plus(X1,X2))	→	plus(X1,X2)	(31)
activate(n__s(X))	→	s(X)	(32)
activate(X)	→	X	(33)

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,V1,V2)	→	isNatKind^#(activate(V2))	(34)
plus^#(N,s(M))	→	U61^#(isNat(M),M,N)	(35)
U21^#(tt,V1)	→	activate^#(V1)	(36)
U15^#(tt,V2)	→	isNat^#(activate(V2))	(37)
U22^#(tt,V1)	→	activate^#(V1)	(38)
isNat^#(n__s(V1))	→	isNatKind^#(activate(V1))	(39)
activate^#(n__s(X))	→	s^#(X)	(40)
U63^#(tt,M,N)	→	activate^#(N)	(41)
U63^#(tt,M,N)	→	U64^#(isNatKind(activate(N)),activate(M),activate(N))	(42)
U14^#(tt,V1,V2)	→	isNat^#(activate(V1))	(43)
isNat^#(n__s(V1))	→	activate^#(V1)	(44)
U62^#(tt,M,N)	→	activate^#(N)	(45)
U61^#(tt,M,N)	→	activate^#(N)	(46)
isNat^#(n__s(V1))	→	activate^#(V1)	(44)
U14^#(tt,V1,V2)	→	activate^#(V2)	(47)
U14^#(tt,V1,V2)	→	activate^#(V1)	(48)
U13^#(tt,V1,V2)	→	activate^#(V2)	(49)
U11^#(tt,V1,V2)	→	activate^#(V1)	(50)
U63^#(tt,M,N)	→	isNatKind^#(activate(N))	(51)
U51^#(tt,N)	→	U52^#(isNatKind(activate(N)),activate(N))	(52)
U11^#(tt,V1,V2)	→	U12^#(isNatKind(activate(V1)),activate(V1),activate(V2))	(53)
U13^#(tt,V1,V2)	→	isNatKind^#(activate(V2))	(54)
U61^#(tt,M,N)	→	U62^#(isNatKind(activate(M)),activate(M),activate(N))	(55)
U63^#(tt,M,N)	→	activate^#(M)	(56)
U62^#(tt,M,N)	→	activate^#(N)	(45)
isNatKind^#(n__plus(V1,V2))	→	U31^#(isNatKind(activate(V1)),activate(V2))	(57)
U51^#(tt,N)	→	activate^#(N)	(58)
isNatKind^#(n__s(V1))	→	isNatKind^#(activate(V1))	(59)
U13^#(tt,V1,V2)	→	activate^#(V1)	(60)
U64^#(tt,M,N)	→	s^#(plus(activate(N),activate(M)))	(61)
isNat^#(n__plus(V1,V2))	→	activate^#(V1)	(62)
U61^#(tt,M,N)	→	activate^#(M)	(63)
isNat^#(n__plus(V1,V2))	→	isNatKind^#(activate(V1))	(64)
U64^#(tt,M,N)	→	activate^#(N)	(65)
isNat^#(n__s(V1))	→	U21^#(isNatKind(activate(V1)),activate(V1))	(66)
U61^#(tt,M,N)	→	activate^#(M)	(63)
isNatKind^#(n__s(V1))	→	activate^#(V1)	(67)
U31^#(tt,V2)	→	U32^#(isNatKind(activate(V2)))	(68)
U64^#(tt,M,N)	→	activate^#(M)	(69)
U13^#(tt,V1,V2)	→	activate^#(V2)	(49)
isNatKind^#(n__plus(V1,V2))	→	isNatKind^#(activate(V1))	(70)
U11^#(tt,V1,V2)	→	activate^#(V1)	(50)
U21^#(tt,V1)	→	activate^#(V1)	(36)
U62^#(tt,M,N)	→	activate^#(M)	(71)
U62^#(tt,M,N)	→	U63^#(isNat(activate(N)),activate(M),activate(N))	(72)
isNat^#(n__plus(V1,V2))	→	activate^#(V1)	(62)
plus^#(N,0)	→	U51^#(isNat(N),N)	(73)
U51^#(tt,N)	→	isNatKind^#(activate(N))	(74)
U63^#(tt,M,N)	→	activate^#(N)	(41)
isNatKind^#(n__s(V1))	→	U41^#(isNatKind(activate(V1)))	(75)
U22^#(tt,V1)	→	U23^#(isNat(activate(V1)))	(76)
U31^#(tt,V2)	→	activate^#(V2)	(77)
U14^#(tt,V1,V2)	→	U15^#(isNat(activate(V1)),activate(V2))	(78)
U12^#(tt,V1,V2)	→	activate^#(V2)	(79)
plus^#(N,s(M))	→	isNat^#(M)	(80)
U22^#(tt,V1)	→	isNat^#(activate(V1))	(81)
U21^#(tt,V1)	→	isNatKind^#(activate(V1))	(82)
isNat^#(n__plus(V1,V2))	→	U11^#(isNatKind(activate(V1)),activate(V1),activate(V2))	(83)
U15^#(tt,V2)	→	U16^#(isNat(activate(V2)))	(84)
U21^#(tt,V1)	→	U22^#(isNatKind(activate(V1)),activate(V1))	(85)
U11^#(tt,V1,V2)	→	isNatKind^#(activate(V1))	(86)
activate^#(n__plus(X1,X2))	→	plus^#(X1,X2)	(87)
U31^#(tt,V2)	→	isNatKind^#(activate(V2))	(88)
activate^#(n__0)	→	0^#	(89)
U11^#(tt,V1,V2)	→	activate^#(V2)	(90)
isNat^#(n__plus(V1,V2))	→	activate^#(V2)	(91)
U61^#(tt,M,N)	→	isNatKind^#(activate(M))	(92)
U15^#(tt,V2)	→	activate^#(V2)	(93)
plus^#(N,0)	→	isNat^#(N)	(94)
isNatKind^#(n__plus(V1,V2))	→	activate^#(V2)	(95)
U12^#(tt,V1,V2)	→	activate^#(V2)	(79)
U64^#(tt,M,N)	→	plus^#(activate(N),activate(M))	(96)
U12^#(tt,V1,V2)	→	U13^#(isNatKind(activate(V2)),activate(V1),activate(V2))	(97)
U13^#(tt,V1,V2)	→	U14^#(isNatKind(activate(V2)),activate(V1),activate(V2))	(98)
U51^#(tt,N)	→	activate^#(N)	(58)
isNatKind^#(n__plus(V1,V2))	→	activate^#(V1)	(99)
U12^#(tt,V1,V2)	→	activate^#(V1)	(100)
U62^#(tt,M,N)	→	isNat^#(activate(N))	(101)
U52^#(tt,N)	→	activate^#(N)	(102)

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

U52^#(tt,N)	→	activate^#(N)	(102)
U62^#(tt,M,N)	→	isNat^#(activate(N))	(101)
isNat^#(n__plus(V1,V2))	→	activate^#(V1)	(62)
U62^#(tt,M,N)	→	activate^#(M)	(71)
U62^#(tt,M,N)	→	U63^#(isNat(activate(N)),activate(M),activate(N))	(72)
U12^#(tt,V1,V2)	→	activate^#(V1)	(100)
U11^#(tt,V1,V2)	→	activate^#(V1)	(50)
U21^#(tt,V1)	→	activate^#(V1)	(36)
isNatKind^#(n__plus(V1,V2))	→	isNatKind^#(activate(V1))	(70)
isNatKind^#(n__plus(V1,V2))	→	activate^#(V1)	(99)
U64^#(tt,M,N)	→	activate^#(M)	(69)
U13^#(tt,V1,V2)	→	activate^#(V2)	(49)
isNatKind^#(n__s(V1))	→	activate^#(V1)	(67)
U61^#(tt,M,N)	→	activate^#(M)	(63)
U51^#(tt,N)	→	activate^#(N)	(58)
isNat^#(n__s(V1))	→	U21^#(isNatKind(activate(V1)),activate(V1))	(66)
U13^#(tt,V1,V2)	→	U14^#(isNatKind(activate(V2)),activate(V1),activate(V2))	(98)
U64^#(tt,M,N)	→	activate^#(N)	(65)
U12^#(tt,V1,V2)	→	U13^#(isNatKind(activate(V2)),activate(V1),activate(V2))	(97)
isNat^#(n__plus(V1,V2))	→	isNatKind^#(activate(V1))	(64)
U64^#(tt,M,N)	→	plus^#(activate(N),activate(M))	(96)
U61^#(tt,M,N)	→	activate^#(M)	(63)
U12^#(tt,V1,V2)	→	activate^#(V2)	(79)
isNat^#(n__plus(V1,V2))	→	activate^#(V1)	(62)
isNatKind^#(n__plus(V1,V2))	→	activate^#(V2)	(95)
plus^#(N,0)	→	isNat^#(N)	(94)
U15^#(tt,V2)	→	activate^#(V2)	(93)
U13^#(tt,V1,V2)	→	activate^#(V1)	(60)
U61^#(tt,M,N)	→	isNatKind^#(activate(M))	(92)
isNat^#(n__plus(V1,V2))	→	activate^#(V2)	(91)
isNatKind^#(n__s(V1))	→	isNatKind^#(activate(V1))	(59)
U51^#(tt,N)	→	activate^#(N)	(58)
isNatKind^#(n__plus(V1,V2))	→	U31^#(isNatKind(activate(V1)),activate(V2))	(57)
U11^#(tt,V1,V2)	→	activate^#(V2)	(90)
U62^#(tt,M,N)	→	activate^#(N)	(45)
U31^#(tt,V2)	→	isNatKind^#(activate(V2))	(88)
activate^#(n__plus(X1,X2))	→	plus^#(X1,X2)	(87)
U63^#(tt,M,N)	→	activate^#(M)	(56)
U61^#(tt,M,N)	→	U62^#(isNatKind(activate(M)),activate(M),activate(N))	(55)
U13^#(tt,V1,V2)	→	isNatKind^#(activate(V2))	(54)
U11^#(tt,V1,V2)	→	isNatKind^#(activate(V1))	(86)
U11^#(tt,V1,V2)	→	U12^#(isNatKind(activate(V1)),activate(V1),activate(V2))	(53)
U51^#(tt,N)	→	U52^#(isNatKind(activate(N)),activate(N))	(52)
U21^#(tt,V1)	→	U22^#(isNatKind(activate(V1)),activate(V1))	(85)
U11^#(tt,V1,V2)	→	activate^#(V1)	(50)
U63^#(tt,M,N)	→	isNatKind^#(activate(N))	(51)
U13^#(tt,V1,V2)	→	activate^#(V2)	(49)
U14^#(tt,V1,V2)	→	activate^#(V1)	(48)
U14^#(tt,V1,V2)	→	activate^#(V2)	(47)
isNat^#(n__s(V1))	→	activate^#(V1)	(44)
U61^#(tt,M,N)	→	activate^#(N)	(46)
isNat^#(n__plus(V1,V2))	→	U11^#(isNatKind(activate(V1)),activate(V1),activate(V2))	(83)
U62^#(tt,M,N)	→	activate^#(N)	(45)
U21^#(tt,V1)	→	isNatKind^#(activate(V1))	(82)
U22^#(tt,V1)	→	isNat^#(activate(V1))	(81)
U14^#(tt,V1,V2)	→	isNat^#(activate(V1))	(43)
isNat^#(n__s(V1))	→	activate^#(V1)	(44)
plus^#(N,s(M))	→	isNat^#(M)	(80)
U12^#(tt,V1,V2)	→	activate^#(V2)	(79)
U14^#(tt,V1,V2)	→	U15^#(isNat(activate(V1)),activate(V2))	(78)
U63^#(tt,M,N)	→	U64^#(isNatKind(activate(N)),activate(M),activate(N))	(42)
U31^#(tt,V2)	→	activate^#(V2)	(77)
U63^#(tt,M,N)	→	activate^#(N)	(41)
isNat^#(n__s(V1))	→	isNatKind^#(activate(V1))	(39)
U22^#(tt,V1)	→	activate^#(V1)	(38)
U63^#(tt,M,N)	→	activate^#(N)	(41)
U51^#(tt,N)	→	isNatKind^#(activate(N))	(74)
U15^#(tt,V2)	→	isNat^#(activate(V2))	(37)
U21^#(tt,V1)	→	activate^#(V1)	(36)
plus^#(N,s(M))	→	U61^#(isNat(M),M,N)	(35)
U12^#(tt,V1,V2)	→	isNatKind^#(activate(V2))	(34)
plus^#(N,0)	→	U51^#(isNat(N),N)	(73)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[0^#]	=	0
[U32^#(x₁)]	=	0
[isNatKind(x₁)]	=	2
[U16(x₁)]	=	7
[U21(x₁, x₂)]	=	x₁ + 0
[U11(x₁, x₂, x₃)]	=	x₂ + 2
[U64(x₁, x₂, x₃)]	=	x₂ + x₃ + 0
[s(x₁)]	=	x₁ + 0
[isNat^#(x₁)]	=	x₁ + 2
[activate(x₁)]	=	x₁ + 0
[plus^#(x₁, x₂)]	=	x₁ + x₂ + 2
[activate^#(x₁)]	=	x₁ + 2
[U23^#(x₁)]	=	0
[U23(x₁)]	=	1
[U63(x₁, x₂, x₃)]	=	x₂ + x₃ + 0
[U13^#(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 0
[U52^#(x₁, x₂)]	=	x₂ + 3
[U12(x₁, x₂, x₃)]	=	x₃ + 3
[U16^#(x₁)]	=	0
[n__s(x₁)]	=	x₁ + 0
[U12^#(x₁, x₂, x₃)]	=	x₂ + x₃ + 2
[U62^#(x₁, x₂, x₃)]	=	x₂ + x₃ + 2
[0]	=	21097
[U14^#(x₁, x₂, x₃)]	=	x₂ + x₃ + 2
[s^#(x₁)]	=	0
[U62(x₁, x₂, x₃)]	=	x₂ + x₃ + 0
[n__plus(x₁, x₂)]	=	x₁ + x₂ + 0
[U63^#(x₁, x₂, x₃)]	=	x₂ + x₃ + 2
[U15^#(x₁, x₂)]	=	x₂ + 2
[U32(x₁)]	=	x₁ + 0
[n__0]	=	21097
[U14(x₁, x₂, x₃)]	=	5
[isNat(x₁)]	=	1
[U52(x₁, x₂)]	=	x₁ + x₂ + 0
[U15(x₁, x₂)]	=	6
[U61(x₁, x₂, x₃)]	=	x₂ + x₃ + 0
[plus(x₁, x₂)]	=	x₁ + x₂ + 0
[U51^#(x₁, x₂)]	=	x₂ + 4
[U11^#(x₁, x₂, x₃)]	=	x₂ + x₃ + 2
[U64^#(x₁, x₂, x₃)]	=	x₂ + x₃ + 2
[U31(x₁, x₂)]	=	2
[U41^#(x₁)]	=	0
[U21^#(x₁, x₂)]	=	x₂ + 2
[U22^#(x₁, x₂)]	=	x₂ + 2
[tt]	=	2
[U13(x₁, x₂, x₃)]	=	x₁ + 2
[U22(x₁, x₂)]	=	3
[U51(x₁, x₂)]	=	x₂ + 2
[isNatKind^#(x₁)]	=	x₁ + 2
[U41(x₁)]	=	x₁ + 0
[U31^#(x₁, x₂)]	=	x₂ + 2
[U61^#(x₁, x₂, x₃)]	=	x₂ + x₃ + 2

together with the usable rules

U64(tt,M,N)	→	s(plus(activate(N),activate(M)))	(18)
U61(tt,M,N)	→	U62(isNatKind(activate(M)),activate(M),activate(N))	(15)
U62(tt,M,N)	→	U63(isNat(activate(N)),activate(M),activate(N))	(16)
plus(N,s(M))	→	U61(isNat(M),M,N)	(26)
activate(n__s(X))	→	s(X)	(32)
U63(tt,M,N)	→	U64(isNatKind(activate(N)),activate(M),activate(N))	(17)
0	→	n__0	(27)
isNatKind(n__0)	→	tt	(22)
plus(X1,X2)	→	n__plus(X1,X2)	(28)
activate(X)	→	X	(33)
U31(tt,V2)	→	U32(isNatKind(activate(V2)))	(10)
plus(N,0)	→	U51(isNat(N),N)	(25)
activate(n__0)	→	0	(30)
U52(tt,N)	→	activate(N)	(14)
activate(n__plus(X1,X2))	→	plus(X1,X2)	(31)
U41(tt)	→	tt	(12)
isNatKind(n__plus(V1,V2))	→	U31(isNatKind(activate(V1)),activate(V2))	(23)
isNatKind(n__s(V1))	→	U41(isNatKind(activate(V1)))	(24)
U32(tt)	→	tt	(11)
U51(tt,N)	→	U52(isNatKind(activate(N)),activate(N))	(13)
s(X)	→	n__s(X)	(29)

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

U52^#(tt,N)	→	activate^#(N)	(102)
U51^#(tt,N)	→	activate^#(N)	(58)
plus^#(N,0)	→	isNat^#(N)	(94)
U51^#(tt,N)	→	activate^#(N)	(58)
U51^#(tt,N)	→	U52^#(isNatKind(activate(N)),activate(N))	(52)
U51^#(tt,N)	→	isNatKind^#(activate(N))	(74)
plus^#(N,0)	→	U51^#(isNat(N),N)	(73)

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

U64^#(tt,M,N)	→	activate^#(M)	(69)
U64^#(tt,M,N)	→	activate^#(N)	(65)
U64^#(tt,M,N)	→	plus^#(activate(N),activate(M))	(96)
U14^#(tt,V1,V2)	→	activate^#(V2)	(47)
U14^#(tt,V1,V2)	→	activate^#(V1)	(48)
U14^#(tt,V1,V2)	→	isNat^#(activate(V1))	(43)
U14^#(tt,V1,V2)	→	U15^#(isNat(activate(V1)),activate(V2))	(78)
U61^#(tt,M,N)	→	activate^#(N)	(46)
U61^#(tt,M,N)	→	activate^#(M)	(63)
U61^#(tt,M,N)	→	activate^#(M)	(63)
U61^#(tt,M,N)	→	isNatKind^#(activate(M))	(92)
U61^#(tt,M,N)	→	U62^#(isNatKind(activate(M)),activate(M),activate(N))	(55)
U22^#(tt,V1)	→	activate^#(V1)	(38)
U22^#(tt,V1)	→	isNat^#(activate(V1))	(81)
U11^#(tt,V1,V2)	→	activate^#(V2)	(90)
U11^#(tt,V1,V2)	→	activate^#(V1)	(50)
U11^#(tt,V1,V2)	→	activate^#(V1)	(50)
U11^#(tt,V1,V2)	→	isNatKind^#(activate(V1))	(86)
U11^#(tt,V1,V2)	→	U12^#(isNatKind(activate(V1)),activate(V1),activate(V2))	(53)
U13^#(tt,V1,V2)	→	activate^#(V2)	(49)
U13^#(tt,V1,V2)	→	activate^#(V1)	(60)
U13^#(tt,V1,V2)	→	activate^#(V2)	(49)
U13^#(tt,V1,V2)	→	isNatKind^#(activate(V2))	(54)
U13^#(tt,V1,V2)	→	U14^#(isNatKind(activate(V2)),activate(V1),activate(V2))	(98)
U62^#(tt,M,N)	→	activate^#(N)	(45)
U62^#(tt,M,N)	→	activate^#(M)	(71)
U62^#(tt,M,N)	→	activate^#(N)	(45)
U62^#(tt,M,N)	→	isNat^#(activate(N))	(101)
U62^#(tt,M,N)	→	U63^#(isNat(activate(N)),activate(M),activate(N))	(72)
isNat^#(n__s(V1))	→	activate^#(V1)	(44)
isNat^#(n__s(V1))	→	activate^#(V1)	(44)
isNat^#(n__s(V1))	→	isNatKind^#(activate(V1))	(39)
isNat^#(n__s(V1))	→	U21^#(isNatKind(activate(V1)),activate(V1))	(66)
plus^#(N,s(M))	→	isNat^#(M)	(80)
plus^#(N,s(M))	→	U61^#(isNat(M),M,N)	(35)
U63^#(tt,M,N)	→	activate^#(N)	(41)
U63^#(tt,M,N)	→	activate^#(M)	(56)
U63^#(tt,M,N)	→	activate^#(N)	(41)
U63^#(tt,M,N)	→	isNatKind^#(activate(N))	(51)
U63^#(tt,M,N)	→	U64^#(isNatKind(activate(N)),activate(M),activate(N))	(42)
U15^#(tt,V2)	→	activate^#(V2)	(93)
U15^#(tt,V2)	→	isNat^#(activate(V2))	(37)
U31^#(tt,V2)	→	activate^#(V2)	(77)
U31^#(tt,V2)	→	isNatKind^#(activate(V2))	(88)
U21^#(tt,V1)	→	activate^#(V1)	(36)
U21^#(tt,V1)	→	activate^#(V1)	(36)
U21^#(tt,V1)	→	isNatKind^#(activate(V1))	(82)
U21^#(tt,V1)	→	U22^#(isNatKind(activate(V1)),activate(V1))	(85)
isNat^#(n__plus(V1,V2))	→	activate^#(V2)	(91)
isNat^#(n__plus(V1,V2))	→	activate^#(V1)	(62)
isNat^#(n__plus(V1,V2))	→	activate^#(V1)	(62)
isNat^#(n__plus(V1,V2))	→	isNatKind^#(activate(V1))	(64)
isNat^#(n__plus(V1,V2))	→	U11^#(isNatKind(activate(V1)),activate(V1),activate(V2))	(83)
activate^#(n__plus(X1,X2))	→	plus^#(X1,X2)	(87)
isNatKind^#(n__plus(V1,V2))	→	activate^#(V2)	(95)
isNatKind^#(n__plus(V1,V2))	→	activate^#(V1)	(99)
isNatKind^#(n__plus(V1,V2))	→	isNatKind^#(activate(V1))	(70)
isNatKind^#(n__plus(V1,V2))	→	U31^#(isNatKind(activate(V1)),activate(V2))	(57)
isNatKind^#(n__s(V1))	→	activate^#(V1)	(67)
isNatKind^#(n__s(V1))	→	isNatKind^#(activate(V1))	(59)
U12^#(tt,V1,V2)	→	activate^#(V2)	(79)
U12^#(tt,V1,V2)	→	activate^#(V1)	(100)
U12^#(tt,V1,V2)	→	activate^#(V2)	(79)
U12^#(tt,V1,V2)	→	isNatKind^#(activate(V2))	(34)
U12^#(tt,V1,V2)	→	U13^#(isNatKind(activate(V2)),activate(V1),activate(V2))	(97)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[0^#]	=	0
[U32^#(x₁)]	=	0
[isNatKind(x₁)]	=	2
[U16(x₁)]	=	7
[U21(x₁, x₂)]	=	x₁ + 0
[U11(x₁, x₂, x₃)]	=	x₂ + 2
[U64(x₁, x₂, x₃)]	=	x₂ + x₃ + 28482
[s(x₁)]	=	x₁ + 6
[isNat^#(x₁)]	=	x₁ + 2
[activate(x₁)]	=	x₁ + 0
[plus^#(x₁, x₂)]	=	x₁ + x₂ + 1
[activate^#(x₁)]	=	x₁ + 2
[U23^#(x₁)]	=	0
[U23(x₁)]	=	1
[U63(x₁, x₂, x₃)]	=	x₂ + x₃ + 28482
[U13^#(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 3
[U52^#(x₁, x₂)]	=	x₂ + 3
[U12(x₁, x₂, x₃)]	=	x₃ + 3
[U16^#(x₁)]	=	0
[n__s(x₁)]	=	x₁ + 6
[U12^#(x₁, x₂, x₃)]	=	x₂ + x₃ + 6
[U62^#(x₁, x₂, x₃)]	=	x₂ + x₃ + 5
[0]	=	31274
[U14^#(x₁, x₂, x₃)]	=	x₂ + x₃ + 4
[s^#(x₁)]	=	0
[U62(x₁, x₂, x₃)]	=	x₂ + x₃ + 28482
[n__plus(x₁, x₂)]	=	x₁ + x₂ + 28476
[U63^#(x₁, x₂, x₃)]	=	x₂ + x₃ + 4
[U15^#(x₁, x₂)]	=	x₂ + 3
[U32(x₁)]	=	x₁ + 0
[n__0]	=	31274
[U14(x₁, x₂, x₃)]	=	5
[isNat(x₁)]	=	1
[U52(x₁, x₂)]	=	x₁ + x₂ + 0
[U15(x₁, x₂)]	=	6
[U61(x₁, x₂, x₃)]	=	x₂ + x₃ + 28482
[plus(x₁, x₂)]	=	x₁ + x₂ + 28476
[U51^#(x₁, x₂)]	=	4
[U11^#(x₁, x₂, x₃)]	=	x₂ + x₃ + 7
[U64^#(x₁, x₂, x₃)]	=	x₂ + x₃ + 3
[U31(x₁, x₂)]	=	2
[U41^#(x₁)]	=	0
[U21^#(x₁, x₂)]	=	x₂ + 4
[U22^#(x₁, x₂)]	=	x₂ + 3
[tt]	=	2
[U13(x₁, x₂, x₃)]	=	x₁ + 2
[U22(x₁, x₂)]	=	3
[U51(x₁, x₂)]	=	x₂ + 2
[isNatKind^#(x₁)]	=	x₁ + 3
[U41(x₁)]	=	x₁ + 0
[U31^#(x₁, x₂)]	=	x₂ + 4
[U61^#(x₁, x₂, x₃)]	=	x₂ + x₃ + 6

together with the usable rules

U64(tt,M,N)	→	s(plus(activate(N),activate(M)))	(18)
U61(tt,M,N)	→	U62(isNatKind(activate(M)),activate(M),activate(N))	(15)
U62(tt,M,N)	→	U63(isNat(activate(N)),activate(M),activate(N))	(16)
plus(N,s(M))	→	U61(isNat(M),M,N)	(26)
activate(n__s(X))	→	s(X)	(32)
U63(tt,M,N)	→	U64(isNatKind(activate(N)),activate(M),activate(N))	(17)
0	→	n__0	(27)
isNatKind(n__0)	→	tt	(22)
plus(X1,X2)	→	n__plus(X1,X2)	(28)
activate(X)	→	X	(33)
U31(tt,V2)	→	U32(isNatKind(activate(V2)))	(10)
plus(N,0)	→	U51(isNat(N),N)	(25)
activate(n__0)	→	0	(30)
U52(tt,N)	→	activate(N)	(14)
activate(n__plus(X1,X2))	→	plus(X1,X2)	(31)
U41(tt)	→	tt	(12)
isNatKind(n__plus(V1,V2))	→	U31(isNatKind(activate(V1)),activate(V2))	(23)
isNatKind(n__s(V1))	→	U41(isNatKind(activate(V1)))	(24)
U32(tt)	→	tt	(11)
U51(tt,N)	→	U52(isNatKind(activate(N)),activate(N))	(13)
s(X)	→	n__s(X)	(29)

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

U64^#(tt,M,N)	→	activate^#(M)	(69)
U64^#(tt,M,N)	→	activate^#(N)	(65)
U64^#(tt,M,N)	→	plus^#(activate(N),activate(M))	(96)
U14^#(tt,V1,V2)	→	activate^#(V2)	(47)
U14^#(tt,V1,V2)	→	activate^#(V1)	(48)
U14^#(tt,V1,V2)	→	isNat^#(activate(V1))	(43)
U14^#(tt,V1,V2)	→	U15^#(isNat(activate(V1)),activate(V2))	(78)
U61^#(tt,M,N)	→	activate^#(N)	(46)
U61^#(tt,M,N)	→	activate^#(M)	(63)
U61^#(tt,M,N)	→	activate^#(M)	(63)
U61^#(tt,M,N)	→	isNatKind^#(activate(M))	(92)
U61^#(tt,M,N)	→	U62^#(isNatKind(activate(M)),activate(M),activate(N))	(55)
U22^#(tt,V1)	→	activate^#(V1)	(38)
U22^#(tt,V1)	→	isNat^#(activate(V1))	(81)
U11^#(tt,V1,V2)	→	activate^#(V2)	(90)
U11^#(tt,V1,V2)	→	activate^#(V1)	(50)
U11^#(tt,V1,V2)	→	activate^#(V1)	(50)
U11^#(tt,V1,V2)	→	isNatKind^#(activate(V1))	(86)
U11^#(tt,V1,V2)	→	U12^#(isNatKind(activate(V1)),activate(V1),activate(V2))	(53)
U13^#(tt,V1,V2)	→	activate^#(V2)	(49)
U13^#(tt,V1,V2)	→	activate^#(V1)	(60)
U13^#(tt,V1,V2)	→	activate^#(V2)	(49)
U13^#(tt,V1,V2)	→	isNatKind^#(activate(V2))	(54)
U13^#(tt,V1,V2)	→	U14^#(isNatKind(activate(V2)),activate(V1),activate(V2))	(98)
U62^#(tt,M,N)	→	activate^#(N)	(45)
U62^#(tt,M,N)	→	activate^#(M)	(71)
U62^#(tt,M,N)	→	activate^#(N)	(45)
U62^#(tt,M,N)	→	isNat^#(activate(N))	(101)
U62^#(tt,M,N)	→	U63^#(isNat(activate(N)),activate(M),activate(N))	(72)
isNat^#(n__s(V1))	→	activate^#(V1)	(44)
isNat^#(n__s(V1))	→	activate^#(V1)	(44)
isNat^#(n__s(V1))	→	isNatKind^#(activate(V1))	(39)
isNat^#(n__s(V1))	→	U21^#(isNatKind(activate(V1)),activate(V1))	(66)
plus^#(N,s(M))	→	isNat^#(M)	(80)
plus^#(N,s(M))	→	U61^#(isNat(M),M,N)	(35)
U63^#(tt,M,N)	→	activate^#(N)	(41)
U63^#(tt,M,N)	→	activate^#(M)	(56)
U63^#(tt,M,N)	→	activate^#(N)	(41)
U63^#(tt,M,N)	→	isNatKind^#(activate(N))	(51)
U63^#(tt,M,N)	→	U64^#(isNatKind(activate(N)),activate(M),activate(N))	(42)
U15^#(tt,V2)	→	activate^#(V2)	(93)
U15^#(tt,V2)	→	isNat^#(activate(V2))	(37)
U31^#(tt,V2)	→	activate^#(V2)	(77)
U31^#(tt,V2)	→	isNatKind^#(activate(V2))	(88)
U21^#(tt,V1)	→	activate^#(V1)	(36)
U21^#(tt,V1)	→	activate^#(V1)	(36)
U21^#(tt,V1)	→	isNatKind^#(activate(V1))	(82)
U21^#(tt,V1)	→	U22^#(isNatKind(activate(V1)),activate(V1))	(85)
isNat^#(n__plus(V1,V2))	→	activate^#(V2)	(91)
isNat^#(n__plus(V1,V2))	→	activate^#(V1)	(62)
isNat^#(n__plus(V1,V2))	→	activate^#(V1)	(62)
isNat^#(n__plus(V1,V2))	→	isNatKind^#(activate(V1))	(64)
isNat^#(n__plus(V1,V2))	→	U11^#(isNatKind(activate(V1)),activate(V1),activate(V2))	(83)
activate^#(n__plus(X1,X2))	→	plus^#(X1,X2)	(87)
isNatKind^#(n__plus(V1,V2))	→	activate^#(V2)	(95)
isNatKind^#(n__plus(V1,V2))	→	activate^#(V1)	(99)
isNatKind^#(n__plus(V1,V2))	→	isNatKind^#(activate(V1))	(70)
isNatKind^#(n__plus(V1,V2))	→	U31^#(isNatKind(activate(V1)),activate(V2))	(57)
isNatKind^#(n__s(V1))	→	activate^#(V1)	(67)
isNatKind^#(n__s(V1))	→	isNatKind^#(activate(V1))	(59)
U12^#(tt,V1,V2)	→	activate^#(V2)	(79)
U12^#(tt,V1,V2)	→	activate^#(V1)	(100)
U12^#(tt,V1,V2)	→	activate^#(V2)	(79)
U12^#(tt,V1,V2)	→	isNatKind^#(activate(V2))	(34)
U12^#(tt,V1,V2)	→	U13^#(isNatKind(activate(V2)),activate(V1),activate(V2))	(97)

could be deleted.

1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.