Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/PEANO_complete_noand_GM)

The rewrite relation of the following TRS is considered.

a__U11(tt,V1,V2)	→	a__U12(a__isNatKind(V1),V1,V2)	(1)
a__U12(tt,V1,V2)	→	a__U13(a__isNatKind(V2),V1,V2)	(2)
a__U13(tt,V1,V2)	→	a__U14(a__isNatKind(V2),V1,V2)	(3)
a__U14(tt,V1,V2)	→	a__U15(a__isNat(V1),V2)	(4)
a__U15(tt,V2)	→	a__U16(a__isNat(V2))	(5)
a__U16(tt)	→	tt	(6)
a__U21(tt,V1)	→	a__U22(a__isNatKind(V1),V1)	(7)
a__U22(tt,V1)	→	a__U23(a__isNat(V1))	(8)
a__U23(tt)	→	tt	(9)
a__U31(tt,V2)	→	a__U32(a__isNatKind(V2))	(10)
a__U32(tt)	→	tt	(11)
a__U41(tt)	→	tt	(12)
a__U51(tt,N)	→	a__U52(a__isNatKind(N),N)	(13)
a__U52(tt,N)	→	mark(N)	(14)
a__U61(tt,M,N)	→	a__U62(a__isNatKind(M),M,N)	(15)
a__U62(tt,M,N)	→	a__U63(a__isNat(N),M,N)	(16)
a__U63(tt,M,N)	→	a__U64(a__isNatKind(N),M,N)	(17)
a__U64(tt,M,N)	→	s(a__plus(mark(N),mark(M)))	(18)
a__isNat(0)	→	tt	(19)
a__isNat(plus(V1,V2))	→	a__U11(a__isNatKind(V1),V1,V2)	(20)
a__isNat(s(V1))	→	a__U21(a__isNatKind(V1),V1)	(21)
a__isNatKind(0)	→	tt	(22)
a__isNatKind(plus(V1,V2))	→	a__U31(a__isNatKind(V1),V2)	(23)
a__isNatKind(s(V1))	→	a__U41(a__isNatKind(V1))	(24)
a__plus(N,0)	→	a__U51(a__isNat(N),N)	(25)
a__plus(N,s(M))	→	a__U61(a__isNat(M),M,N)	(26)
mark(U11(X1,X2,X3))	→	a__U11(mark(X1),X2,X3)	(27)
mark(U12(X1,X2,X3))	→	a__U12(mark(X1),X2,X3)	(28)
mark(isNatKind(X))	→	a__isNatKind(X)	(29)
mark(U13(X1,X2,X3))	→	a__U13(mark(X1),X2,X3)	(30)
mark(U14(X1,X2,X3))	→	a__U14(mark(X1),X2,X3)	(31)
mark(U15(X1,X2))	→	a__U15(mark(X1),X2)	(32)
mark(isNat(X))	→	a__isNat(X)	(33)
mark(U16(X))	→	a__U16(mark(X))	(34)
mark(U21(X1,X2))	→	a__U21(mark(X1),X2)	(35)
mark(U22(X1,X2))	→	a__U22(mark(X1),X2)	(36)
mark(U23(X))	→	a__U23(mark(X))	(37)
mark(U31(X1,X2))	→	a__U31(mark(X1),X2)	(38)
mark(U32(X))	→	a__U32(mark(X))	(39)
mark(U41(X))	→	a__U41(mark(X))	(40)
mark(U51(X1,X2))	→	a__U51(mark(X1),X2)	(41)
mark(U52(X1,X2))	→	a__U52(mark(X1),X2)	(42)
mark(U61(X1,X2,X3))	→	a__U61(mark(X1),X2,X3)	(43)
mark(U62(X1,X2,X3))	→	a__U62(mark(X1),X2,X3)	(44)
mark(U63(X1,X2,X3))	→	a__U63(mark(X1),X2,X3)	(45)
mark(U64(X1,X2,X3))	→	a__U64(mark(X1),X2,X3)	(46)
mark(plus(X1,X2))	→	a__plus(mark(X1),mark(X2))	(47)
mark(tt)	→	tt	(48)
mark(s(X))	→	s(mark(X))	(49)
mark(0)	→	0	(50)
a__U11(X1,X2,X3)	→	U11(X1,X2,X3)	(51)
a__U12(X1,X2,X3)	→	U12(X1,X2,X3)	(52)
a__isNatKind(X)	→	isNatKind(X)	(53)
a__U13(X1,X2,X3)	→	U13(X1,X2,X3)	(54)
a__U14(X1,X2,X3)	→	U14(X1,X2,X3)	(55)
a__U15(X1,X2)	→	U15(X1,X2)	(56)
a__isNat(X)	→	isNat(X)	(57)
a__U16(X)	→	U16(X)	(58)
a__U21(X1,X2)	→	U21(X1,X2)	(59)
a__U22(X1,X2)	→	U22(X1,X2)	(60)
a__U23(X)	→	U23(X)	(61)
a__U31(X1,X2)	→	U31(X1,X2)	(62)
a__U32(X)	→	U32(X)	(63)
a__U41(X)	→	U41(X)	(64)
a__U51(X1,X2)	→	U51(X1,X2)	(65)
a__U52(X1,X2)	→	U52(X1,X2)	(66)
a__U61(X1,X2,X3)	→	U61(X1,X2,X3)	(67)
a__U62(X1,X2,X3)	→	U62(X1,X2,X3)	(68)
a__U63(X1,X2,X3)	→	U63(X1,X2,X3)	(69)
a__U64(X1,X2,X3)	→	U64(X1,X2,X3)	(70)
a__plus(X1,X2)	→	plus(X1,X2)	(71)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by ttt2 @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

a__U11^#(tt,V1,V2)	→	a__isNatKind^#(V1)	(72)
a__U11^#(tt,V1,V2)	→	a__U12^#(a__isNatKind(V1),V1,V2)	(73)
a__U12^#(tt,V1,V2)	→	a__isNatKind^#(V2)	(74)
a__U12^#(tt,V1,V2)	→	a__U13^#(a__isNatKind(V2),V1,V2)	(75)
a__U13^#(tt,V1,V2)	→	a__isNatKind^#(V2)	(76)
a__U13^#(tt,V1,V2)	→	a__U14^#(a__isNatKind(V2),V1,V2)	(77)
a__U14^#(tt,V1,V2)	→	a__isNat^#(V1)	(78)
a__U14^#(tt,V1,V2)	→	a__U15^#(a__isNat(V1),V2)	(79)
a__U15^#(tt,V2)	→	a__isNat^#(V2)	(80)
a__U15^#(tt,V2)	→	a__U16^#(a__isNat(V2))	(81)
a__U21^#(tt,V1)	→	a__isNatKind^#(V1)	(82)
a__U21^#(tt,V1)	→	a__U22^#(a__isNatKind(V1),V1)	(83)
a__U22^#(tt,V1)	→	a__isNat^#(V1)	(84)
a__U22^#(tt,V1)	→	a__U23^#(a__isNat(V1))	(85)
a__U31^#(tt,V2)	→	a__isNatKind^#(V2)	(86)
a__U31^#(tt,V2)	→	a__U32^#(a__isNatKind(V2))	(87)
a__U51^#(tt,N)	→	a__isNatKind^#(N)	(88)
a__U51^#(tt,N)	→	a__U52^#(a__isNatKind(N),N)	(89)
a__U52^#(tt,N)	→	mark^#(N)	(90)
a__U61^#(tt,M,N)	→	a__isNatKind^#(M)	(91)
a__U61^#(tt,M,N)	→	a__U62^#(a__isNatKind(M),M,N)	(92)
a__U62^#(tt,M,N)	→	a__isNat^#(N)	(93)
a__U62^#(tt,M,N)	→	a__U63^#(a__isNat(N),M,N)	(94)
a__U63^#(tt,M,N)	→	a__isNatKind^#(N)	(95)
a__U63^#(tt,M,N)	→	a__U64^#(a__isNatKind(N),M,N)	(96)
a__U64^#(tt,M,N)	→	mark^#(M)	(97)
a__U64^#(tt,M,N)	→	mark^#(N)	(98)
a__U64^#(tt,M,N)	→	a__plus^#(mark(N),mark(M))	(99)
a__isNat^#(plus(V1,V2))	→	a__isNatKind^#(V1)	(100)
a__isNat^#(plus(V1,V2))	→	a__U11^#(a__isNatKind(V1),V1,V2)	(101)
a__isNat^#(s(V1))	→	a__isNatKind^#(V1)	(102)
a__isNat^#(s(V1))	→	a__U21^#(a__isNatKind(V1),V1)	(103)
a__isNatKind^#(plus(V1,V2))	→	a__isNatKind^#(V1)	(104)
a__isNatKind^#(plus(V1,V2))	→	a__U31^#(a__isNatKind(V1),V2)	(105)
a__isNatKind^#(s(V1))	→	a__isNatKind^#(V1)	(106)
a__isNatKind^#(s(V1))	→	a__U41^#(a__isNatKind(V1))	(107)
a__plus^#(N,0)	→	a__isNat^#(N)	(108)
a__plus^#(N,0)	→	a__U51^#(a__isNat(N),N)	(109)
a__plus^#(N,s(M))	→	a__isNat^#(M)	(110)
a__plus^#(N,s(M))	→	a__U61^#(a__isNat(M),M,N)	(111)
mark^#(U11(X1,X2,X3))	→	mark^#(X1)	(112)
mark^#(U11(X1,X2,X3))	→	a__U11^#(mark(X1),X2,X3)	(113)
mark^#(U12(X1,X2,X3))	→	mark^#(X1)	(114)
mark^#(U12(X1,X2,X3))	→	a__U12^#(mark(X1),X2,X3)	(115)
mark^#(isNatKind(X))	→	a__isNatKind^#(X)	(116)
mark^#(U13(X1,X2,X3))	→	mark^#(X1)	(117)
mark^#(U13(X1,X2,X3))	→	a__U13^#(mark(X1),X2,X3)	(118)
mark^#(U14(X1,X2,X3))	→	mark^#(X1)	(119)
mark^#(U14(X1,X2,X3))	→	a__U14^#(mark(X1),X2,X3)	(120)
mark^#(U15(X1,X2))	→	mark^#(X1)	(121)
mark^#(U15(X1,X2))	→	a__U15^#(mark(X1),X2)	(122)
mark^#(isNat(X))	→	a__isNat^#(X)	(123)
mark^#(U16(X))	→	mark^#(X)	(124)
mark^#(U16(X))	→	a__U16^#(mark(X))	(125)
mark^#(U21(X1,X2))	→	mark^#(X1)	(126)
mark^#(U21(X1,X2))	→	a__U21^#(mark(X1),X2)	(127)
mark^#(U22(X1,X2))	→	mark^#(X1)	(128)
mark^#(U22(X1,X2))	→	a__U22^#(mark(X1),X2)	(129)
mark^#(U23(X))	→	mark^#(X)	(130)
mark^#(U23(X))	→	a__U23^#(mark(X))	(131)
mark^#(U31(X1,X2))	→	mark^#(X1)	(132)
mark^#(U31(X1,X2))	→	a__U31^#(mark(X1),X2)	(133)
mark^#(U32(X))	→	mark^#(X)	(134)
mark^#(U32(X))	→	a__U32^#(mark(X))	(135)
mark^#(U41(X))	→	mark^#(X)	(136)
mark^#(U41(X))	→	a__U41^#(mark(X))	(137)
mark^#(U51(X1,X2))	→	mark^#(X1)	(138)
mark^#(U51(X1,X2))	→	a__U51^#(mark(X1),X2)	(139)
mark^#(U52(X1,X2))	→	mark^#(X1)	(140)
mark^#(U52(X1,X2))	→	a__U52^#(mark(X1),X2)	(141)
mark^#(U61(X1,X2,X3))	→	mark^#(X1)	(142)
mark^#(U61(X1,X2,X3))	→	a__U61^#(mark(X1),X2,X3)	(143)
mark^#(U62(X1,X2,X3))	→	mark^#(X1)	(144)
mark^#(U62(X1,X2,X3))	→	a__U62^#(mark(X1),X2,X3)	(145)
mark^#(U63(X1,X2,X3))	→	mark^#(X1)	(146)
mark^#(U63(X1,X2,X3))	→	a__U63^#(mark(X1),X2,X3)	(147)
mark^#(U64(X1,X2,X3))	→	mark^#(X1)	(148)
mark^#(U64(X1,X2,X3))	→	a__U64^#(mark(X1),X2,X3)	(149)
mark^#(plus(X1,X2))	→	mark^#(X2)	(150)
mark^#(plus(X1,X2))	→	mark^#(X1)	(151)
mark^#(plus(X1,X2))	→	a__plus^#(mark(X1),mark(X2))	(152)
mark^#(s(X))	→	mark^#(X)	(153)

1.1 Dependency Graph Processor

The dependency pairs are split into 3 components.

The 1^st component contains the pair

a__plus^#(N,0)	→	a__U51^#(a__isNat(N),N)	(109)
a__U51^#(tt,N)	→	a__U52^#(a__isNatKind(N),N)	(89)
a__U52^#(tt,N)	→	mark^#(N)	(90)
mark^#(U11(X1,X2,X3))	→	mark^#(X1)	(112)
mark^#(U12(X1,X2,X3))	→	mark^#(X1)	(114)
mark^#(U13(X1,X2,X3))	→	mark^#(X1)	(117)
mark^#(U14(X1,X2,X3))	→	mark^#(X1)	(119)
mark^#(U15(X1,X2))	→	mark^#(X1)	(121)
mark^#(U16(X))	→	mark^#(X)	(124)
mark^#(U21(X1,X2))	→	mark^#(X1)	(126)
mark^#(U22(X1,X2))	→	mark^#(X1)	(128)
mark^#(U23(X))	→	mark^#(X)	(130)
mark^#(U31(X1,X2))	→	mark^#(X1)	(132)
mark^#(U32(X))	→	mark^#(X)	(134)
mark^#(U41(X))	→	mark^#(X)	(136)
mark^#(U51(X1,X2))	→	mark^#(X1)	(138)
mark^#(U51(X1,X2))	→	a__U51^#(mark(X1),X2)	(139)
mark^#(U52(X1,X2))	→	mark^#(X1)	(140)
mark^#(U52(X1,X2))	→	a__U52^#(mark(X1),X2)	(141)
mark^#(U61(X1,X2,X3))	→	mark^#(X1)	(142)
mark^#(U61(X1,X2,X3))	→	a__U61^#(mark(X1),X2,X3)	(143)
a__U61^#(tt,M,N)	→	a__U62^#(a__isNatKind(M),M,N)	(92)
a__U62^#(tt,M,N)	→	a__U63^#(a__isNat(N),M,N)	(94)
a__U63^#(tt,M,N)	→	a__U64^#(a__isNatKind(N),M,N)	(96)
a__U64^#(tt,M,N)	→	mark^#(M)	(97)
mark^#(U62(X1,X2,X3))	→	mark^#(X1)	(144)
mark^#(U62(X1,X2,X3))	→	a__U62^#(mark(X1),X2,X3)	(145)
mark^#(U63(X1,X2,X3))	→	mark^#(X1)	(146)
mark^#(U63(X1,X2,X3))	→	a__U63^#(mark(X1),X2,X3)	(147)
mark^#(U64(X1,X2,X3))	→	mark^#(X1)	(148)
mark^#(U64(X1,X2,X3))	→	a__U64^#(mark(X1),X2,X3)	(149)
a__U64^#(tt,M,N)	→	mark^#(N)	(98)
mark^#(plus(X1,X2))	→	mark^#(X2)	(150)
mark^#(plus(X1,X2))	→	mark^#(X1)	(151)
mark^#(plus(X1,X2))	→	a__plus^#(mark(X1),mark(X2))	(152)
a__plus^#(N,s(M))	→	a__U61^#(a__isNat(M),M,N)	(111)
mark^#(s(X))	→	mark^#(X)	(153)
a__U64^#(tt,M,N)	→	a__plus^#(mark(N),mark(M))	(99)

1.1.1 Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the arctic semiring over the integers

[a__U61(x₁, x₂, x₃)]	=	0 · x₁ + 0 · x₂ + 6 · x₃ + -∞
[a__U13(x₁, x₂, x₃)]	=	0 · x₁ + 0 · x₂ + 0 · x₃ + 0
[a__U51(x₁, x₂)]	=	6 · x₁ + 1 · x₂ + 0
[a__U16(x₁)]	=	0 · x₁ + -∞
[a__U11(x₁, x₂, x₃)]	=	0 · x₁ + 4 · x₂ + 0 · x₃ + -∞
[a__U12(x₁, x₂, x₃)]	=	0 · x₁ + 0 · x₂ + 0 · x₃ + -∞
[a__U52(x₁, x₂)]	=	0 · x₁ + 1 · x₂ + -∞
[a__U64(x₁, x₂, x₃)]	=	0 · x₁ + 0 · x₂ + 6 · x₃ + -∞
[U23(x₁)]	=	0 · x₁ + 0
[U11(x₁, x₂, x₃)]	=	0 · x₁ + 4 · x₂ + 0 · x₃ + -∞
[a__U61^#(x₁, x₂, x₃)]	=	0 · x₁ + 0 · x₂ + 6 · x₃ + -∞
[isNat(x₁)]	=	0 · x₁ + -∞
[a__U62(x₁, x₂, x₃)]	=	0 · x₁ + 0 · x₂ + 6 · x₃ + 0
[mark(x₁)]	=	0 · x₁ + -∞
[a__U51^#(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + -∞
[U12(x₁, x₂, x₃)]	=	0 · x₁ + 0 · x₂ + 0 · x₃ + -∞
[U21(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + -∞
[a__plus(x₁, x₂)]	=	6 · x₁ + 0 · x₂ + -∞
[isNatKind(x₁)]	=	0 · x₁ + -∞
[a__U63^#(x₁, x₂, x₃)]	=	0 · x₁ + 0 · x₂ + 6 · x₃ + 0
[U63(x₁, x₂, x₃)]	=	0 · x₁ + 0 · x₂ + 6 · x₃ + 0
[a__U14(x₁, x₂, x₃)]	=	0 · x₁ + 0 · x₂ + 0 · x₃ + 0
[a__U62^#(x₁, x₂, x₃)]	=	0 · x₁ + 0 · x₂ + 6 · x₃ + 0
[U16(x₁)]	=	0 · x₁ + -∞
[a__U22(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + -∞
[tt]	=	0
[U41(x₁)]	=	0 · x₁ + -∞
[a__U15(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + -∞
[a__U63(x₁, x₂, x₃)]	=	0 · x₁ + 0 · x₂ + 6 · x₃ + 0
[plus(x₁, x₂)]	=	6 · x₁ + 0 · x₂ + -∞
[U14(x₁, x₂, x₃)]	=	0 · x₁ + 0 · x₂ + 0 · x₃ + 0
[mark^#(x₁)]	=	0 · x₁ + 0
[a__U41(x₁)]	=	0 · x₁ + -∞
[U15(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + -∞
[a__U31(x₁, x₂)]	=	4 · x₁ + 0 · x₂ + -∞
[U64(x₁, x₂, x₃)]	=	0 · x₁ + 0 · x₂ + 6 · x₃ + -∞
[s(x₁)]	=	0 · x₁ + -∞
[0]	=	0
[a__U23(x₁)]	=	0 · x₁ + 0
[a__U21(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + -∞
[a__U32(x₁)]	=	0 · x₁ + 0
[U51(x₁, x₂)]	=	6 · x₁ + 1 · x₂ + 0
[a__plus^#(x₁, x₂)]	=	6 · x₁ + 0 · x₂ + 0
[a__isNat(x₁)]	=	0 · x₁ + -∞
[U32(x₁)]	=	0 · x₁ + 0
[a__U52^#(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + 0
[U31(x₁, x₂)]	=	4 · x₁ + 0 · x₂ + -∞
[U52(x₁, x₂)]	=	0 · x₁ + 1 · x₂ + -∞
[U61(x₁, x₂, x₃)]	=	0 · x₁ + 0 · x₂ + 6 · x₃ + -∞
[a__U64^#(x₁, x₂, x₃)]	=	0 · x₁ + 0 · x₂ + 6 · x₃ + 0
[U22(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + -∞
[U13(x₁, x₂, x₃)]	=	0 · x₁ + 0 · x₂ + 0 · x₃ + 0
[U62(x₁, x₂, x₃)]	=	0 · x₁ + 0 · x₂ + 6 · x₃ + 0
[a__isNatKind(x₁)]	=	0 · x₁ + -∞

together with the usable rules

a__U11(tt,V1,V2)	→	a__U12(a__isNatKind(V1),V1,V2)	(1)
a__U12(tt,V1,V2)	→	a__U13(a__isNatKind(V2),V1,V2)	(2)
a__U13(tt,V1,V2)	→	a__U14(a__isNatKind(V2),V1,V2)	(3)
a__U14(tt,V1,V2)	→	a__U15(a__isNat(V1),V2)	(4)
a__U15(tt,V2)	→	a__U16(a__isNat(V2))	(5)
a__U16(tt)	→	tt	(6)
a__U21(tt,V1)	→	a__U22(a__isNatKind(V1),V1)	(7)
a__U22(tt,V1)	→	a__U23(a__isNat(V1))	(8)
a__U23(tt)	→	tt	(9)
a__U31(tt,V2)	→	a__U32(a__isNatKind(V2))	(10)
a__U32(tt)	→	tt	(11)
a__U41(tt)	→	tt	(12)
a__U51(tt,N)	→	a__U52(a__isNatKind(N),N)	(13)
a__U52(tt,N)	→	mark(N)	(14)
a__U61(tt,M,N)	→	a__U62(a__isNatKind(M),M,N)	(15)
a__U62(tt,M,N)	→	a__U63(a__isNat(N),M,N)	(16)
a__U63(tt,M,N)	→	a__U64(a__isNatKind(N),M,N)	(17)
a__U64(tt,M,N)	→	s(a__plus(mark(N),mark(M)))	(18)
a__isNat(0)	→	tt	(19)
a__isNat(plus(V1,V2))	→	a__U11(a__isNatKind(V1),V1,V2)	(20)
a__isNat(s(V1))	→	a__U21(a__isNatKind(V1),V1)	(21)
a__isNatKind(0)	→	tt	(22)
a__isNatKind(plus(V1,V2))	→	a__U31(a__isNatKind(V1),V2)	(23)
a__isNatKind(s(V1))	→	a__U41(a__isNatKind(V1))	(24)
a__plus(N,0)	→	a__U51(a__isNat(N),N)	(25)
a__plus(N,s(M))	→	a__U61(a__isNat(M),M,N)	(26)
mark(U11(X1,X2,X3))	→	a__U11(mark(X1),X2,X3)	(27)
mark(U12(X1,X2,X3))	→	a__U12(mark(X1),X2,X3)	(28)
mark(isNatKind(X))	→	a__isNatKind(X)	(29)
mark(U13(X1,X2,X3))	→	a__U13(mark(X1),X2,X3)	(30)
mark(U14(X1,X2,X3))	→	a__U14(mark(X1),X2,X3)	(31)
mark(U15(X1,X2))	→	a__U15(mark(X1),X2)	(32)
mark(isNat(X))	→	a__isNat(X)	(33)
mark(U16(X))	→	a__U16(mark(X))	(34)
mark(U21(X1,X2))	→	a__U21(mark(X1),X2)	(35)
mark(U22(X1,X2))	→	a__U22(mark(X1),X2)	(36)
mark(U23(X))	→	a__U23(mark(X))	(37)
mark(U31(X1,X2))	→	a__U31(mark(X1),X2)	(38)
mark(U32(X))	→	a__U32(mark(X))	(39)
mark(U41(X))	→	a__U41(mark(X))	(40)
mark(U51(X1,X2))	→	a__U51(mark(X1),X2)	(41)
mark(U52(X1,X2))	→	a__U52(mark(X1),X2)	(42)
mark(U61(X1,X2,X3))	→	a__U61(mark(X1),X2,X3)	(43)
mark(U62(X1,X2,X3))	→	a__U62(mark(X1),X2,X3)	(44)
mark(U63(X1,X2,X3))	→	a__U63(mark(X1),X2,X3)	(45)
mark(U64(X1,X2,X3))	→	a__U64(mark(X1),X2,X3)	(46)
mark(plus(X1,X2))	→	a__plus(mark(X1),mark(X2))	(47)
mark(tt)	→	tt	(48)
mark(s(X))	→	s(mark(X))	(49)
mark(0)	→	0	(50)
a__U11(X1,X2,X3)	→	U11(X1,X2,X3)	(51)
a__U12(X1,X2,X3)	→	U12(X1,X2,X3)	(52)
a__isNatKind(X)	→	isNatKind(X)	(53)
a__U13(X1,X2,X3)	→	U13(X1,X2,X3)	(54)
a__U14(X1,X2,X3)	→	U14(X1,X2,X3)	(55)
a__U15(X1,X2)	→	U15(X1,X2)	(56)
a__isNat(X)	→	isNat(X)	(57)
a__U16(X)	→	U16(X)	(58)
a__U21(X1,X2)	→	U21(X1,X2)	(59)
a__U22(X1,X2)	→	U22(X1,X2)	(60)
a__U23(X)	→	U23(X)	(61)
a__U31(X1,X2)	→	U31(X1,X2)	(62)
a__U32(X)	→	U32(X)	(63)
a__U41(X)	→	U41(X)	(64)
a__U51(X1,X2)	→	U51(X1,X2)	(65)
a__U52(X1,X2)	→	U52(X1,X2)	(66)
a__U61(X1,X2,X3)	→	U61(X1,X2,X3)	(67)
a__U62(X1,X2,X3)	→	U62(X1,X2,X3)	(68)
a__U63(X1,X2,X3)	→	U63(X1,X2,X3)	(69)
a__U64(X1,X2,X3)	→	U64(X1,X2,X3)	(70)
a__plus(X1,X2)	→	plus(X1,X2)	(71)

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

a__plus^#(N,0)	→	a__U51^#(a__isNat(N),N)	(109)
mark^#(U51(X1,X2))	→	a__U51^#(mark(X1),X2)	(139)

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

a__plus^#(N,s(M))	→	a__U61^#(a__isNat(M),M,N)	(111)
a__U61^#(tt,M,N)	→	a__U62^#(a__isNatKind(M),M,N)	(92)
a__U62^#(tt,M,N)	→	a__U63^#(a__isNat(N),M,N)	(94)
a__U63^#(tt,M,N)	→	a__U64^#(a__isNatKind(N),M,N)	(96)
a__U64^#(tt,M,N)	→	mark^#(M)	(97)
mark^#(U11(X1,X2,X3))	→	mark^#(X1)	(112)
mark^#(U12(X1,X2,X3))	→	mark^#(X1)	(114)
mark^#(U13(X1,X2,X3))	→	mark^#(X1)	(117)
mark^#(U14(X1,X2,X3))	→	mark^#(X1)	(119)
mark^#(U15(X1,X2))	→	mark^#(X1)	(121)
mark^#(U16(X))	→	mark^#(X)	(124)
mark^#(U21(X1,X2))	→	mark^#(X1)	(126)
mark^#(U22(X1,X2))	→	mark^#(X1)	(128)
mark^#(U23(X))	→	mark^#(X)	(130)
mark^#(U31(X1,X2))	→	mark^#(X1)	(132)
mark^#(U32(X))	→	mark^#(X)	(134)
mark^#(U41(X))	→	mark^#(X)	(136)
mark^#(U51(X1,X2))	→	mark^#(X1)	(138)
mark^#(U52(X1,X2))	→	mark^#(X1)	(140)
mark^#(U52(X1,X2))	→	a__U52^#(mark(X1),X2)	(141)
a__U52^#(tt,N)	→	mark^#(N)	(90)
mark^#(U61(X1,X2,X3))	→	mark^#(X1)	(142)
mark^#(U61(X1,X2,X3))	→	a__U61^#(mark(X1),X2,X3)	(143)
mark^#(U62(X1,X2,X3))	→	mark^#(X1)	(144)
mark^#(U62(X1,X2,X3))	→	a__U62^#(mark(X1),X2,X3)	(145)
mark^#(U63(X1,X2,X3))	→	mark^#(X1)	(146)
mark^#(U63(X1,X2,X3))	→	a__U63^#(mark(X1),X2,X3)	(147)
mark^#(U64(X1,X2,X3))	→	mark^#(X1)	(148)
mark^#(U64(X1,X2,X3))	→	a__U64^#(mark(X1),X2,X3)	(149)
a__U64^#(tt,M,N)	→	mark^#(N)	(98)
mark^#(plus(X1,X2))	→	mark^#(X2)	(150)
mark^#(plus(X1,X2))	→	mark^#(X1)	(151)
mark^#(plus(X1,X2))	→	a__plus^#(mark(X1),mark(X2))	(152)
mark^#(s(X))	→	mark^#(X)	(153)
a__U64^#(tt,M,N)	→	a__plus^#(mark(N),mark(M))	(99)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the arctic semiring over the integers

[a__U61(x₁, x₂, x₃)]	=	2 · x₁ + 2 · x₂ + 3 · x₃ + 0
[a__U13(x₁, x₂, x₃)]	=	0 · x₁ + 0 · x₂ + 0 · x₃ + 0
[a__U51(x₁, x₂)]	=	1 · x₁ + 0 · x₂ + -∞
[a__U16(x₁)]	=	0 · x₁ + 0
[a__U11(x₁, x₂, x₃)]	=	0 · x₁ + 3 · x₂ + 0 · x₃ + 0
[a__U12(x₁, x₂, x₃)]	=	0 · x₁ + 0 · x₂ + 0 · x₃ + -∞
[a__U52(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + -∞
[a__U64(x₁, x₂, x₃)]	=	0 · x₁ + 2 · x₂ + 3 · x₃ + 0
[U23(x₁)]	=	0 · x₁ + -∞
[U11(x₁, x₂, x₃)]	=	0 · x₁ + 3 · x₂ + 0 · x₃ + 0
[a__U61^#(x₁, x₂, x₃)]	=	6 · x₁ + 6 · x₂ + 7 · x₃ + 0
[isNat(x₁)]	=	0 · x₁ + 0
[a__U62(x₁, x₂, x₃)]	=	2 · x₁ + 2 · x₂ + 3 · x₃ + 0
[mark(x₁)]	=	0 · x₁ + -∞
[U12(x₁, x₂, x₃)]	=	0 · x₁ + 0 · x₂ + 0 · x₃ + -∞
[U21(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + 0
[a__plus(x₁, x₂)]	=	3 · x₁ + 2 · x₂ + 0
[isNatKind(x₁)]	=	-∞ · x₁ + 0
[a__U63^#(x₁, x₂, x₃)]	=	6 · x₁ + 6 · x₂ + 7 · x₃ + 0
[U63(x₁, x₂, x₃)]	=	2 · x₁ + 2 · x₂ + 3 · x₃ + 0
[a__U14(x₁, x₂, x₃)]	=	0 · x₁ + 0 · x₂ + 0 · x₃ + -∞
[U16(x₁)]	=	0 · x₁ + 0
[a__U62^#(x₁, x₂, x₃)]	=	6 · x₁ + 6 · x₂ + 7 · x₃ + 0
[a__U22(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + 0
[tt]	=	0
[U41(x₁)]	=	0 · x₁ + 0
[a__U15(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + -∞
[a__U63(x₁, x₂, x₃)]	=	2 · x₁ + 2 · x₂ + 3 · x₃ + 0
[plus(x₁, x₂)]	=	3 · x₁ + 2 · x₂ + 0
[U14(x₁, x₂, x₃)]	=	0 · x₁ + 0 · x₂ + 0 · x₃ + -∞
[mark^#(x₁)]	=	4 · x₁ + -∞
[a__U41(x₁)]	=	0 · x₁ + 0
[U15(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + -∞
[a__U31(x₁, x₂)]	=	0 · x₁ + -∞ · x₂ + 0
[U64(x₁, x₂, x₃)]	=	0 · x₁ + 2 · x₂ + 3 · x₃ + 0
[s(x₁)]	=	0 · x₁ + 0
[0]	=	0
[a__U23(x₁)]	=	0 · x₁ + -∞
[a__U21(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + 0
[a__U32(x₁)]	=	0 · x₁ + 0
[U51(x₁, x₂)]	=	1 · x₁ + 0 · x₂ + -∞
[a__plus^#(x₁, x₂)]	=	7 · x₁ + 6 · x₂ + -∞
[a__isNat(x₁)]	=	0 · x₁ + 0
[a__U52^#(x₁, x₂)]	=	0 · x₁ + 4 · x₂ + -∞
[U32(x₁)]	=	0 · x₁ + 0
[U31(x₁, x₂)]	=	0 · x₁ + -∞ · x₂ + 0
[U52(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + -∞
[U61(x₁, x₂, x₃)]	=	2 · x₁ + 2 · x₂ + 3 · x₃ + 0
[a__U64^#(x₁, x₂, x₃)]	=	-∞ · x₁ + 6 · x₂ + 7 · x₃ + -∞
[U22(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + 0
[U13(x₁, x₂, x₃)]	=	0 · x₁ + 0 · x₂ + 0 · x₃ + 0
[U62(x₁, x₂, x₃)]	=	2 · x₁ + 2 · x₂ + 3 · x₃ + 0
[a__isNatKind(x₁)]	=	-∞ · x₁ + 0

together with the usable rules

a__U11(tt,V1,V2)	→	a__U12(a__isNatKind(V1),V1,V2)	(1)
a__U12(tt,V1,V2)	→	a__U13(a__isNatKind(V2),V1,V2)	(2)
a__U13(tt,V1,V2)	→	a__U14(a__isNatKind(V2),V1,V2)	(3)
a__U14(tt,V1,V2)	→	a__U15(a__isNat(V1),V2)	(4)
a__U15(tt,V2)	→	a__U16(a__isNat(V2))	(5)
a__U16(tt)	→	tt	(6)
a__U21(tt,V1)	→	a__U22(a__isNatKind(V1),V1)	(7)
a__U22(tt,V1)	→	a__U23(a__isNat(V1))	(8)
a__U23(tt)	→	tt	(9)
a__U31(tt,V2)	→	a__U32(a__isNatKind(V2))	(10)
a__U32(tt)	→	tt	(11)
a__U41(tt)	→	tt	(12)
a__U51(tt,N)	→	a__U52(a__isNatKind(N),N)	(13)
a__U52(tt,N)	→	mark(N)	(14)
a__U61(tt,M,N)	→	a__U62(a__isNatKind(M),M,N)	(15)
a__U62(tt,M,N)	→	a__U63(a__isNat(N),M,N)	(16)
a__U63(tt,M,N)	→	a__U64(a__isNatKind(N),M,N)	(17)
a__U64(tt,M,N)	→	s(a__plus(mark(N),mark(M)))	(18)
a__isNat(0)	→	tt	(19)
a__isNat(plus(V1,V2))	→	a__U11(a__isNatKind(V1),V1,V2)	(20)
a__isNat(s(V1))	→	a__U21(a__isNatKind(V1),V1)	(21)
a__isNatKind(0)	→	tt	(22)
a__isNatKind(plus(V1,V2))	→	a__U31(a__isNatKind(V1),V2)	(23)
a__isNatKind(s(V1))	→	a__U41(a__isNatKind(V1))	(24)
a__plus(N,0)	→	a__U51(a__isNat(N),N)	(25)
a__plus(N,s(M))	→	a__U61(a__isNat(M),M,N)	(26)
mark(U11(X1,X2,X3))	→	a__U11(mark(X1),X2,X3)	(27)
mark(U12(X1,X2,X3))	→	a__U12(mark(X1),X2,X3)	(28)
mark(isNatKind(X))	→	a__isNatKind(X)	(29)
mark(U13(X1,X2,X3))	→	a__U13(mark(X1),X2,X3)	(30)
mark(U14(X1,X2,X3))	→	a__U14(mark(X1),X2,X3)	(31)
mark(U15(X1,X2))	→	a__U15(mark(X1),X2)	(32)
mark(isNat(X))	→	a__isNat(X)	(33)
mark(U16(X))	→	a__U16(mark(X))	(34)
mark(U21(X1,X2))	→	a__U21(mark(X1),X2)	(35)
mark(U22(X1,X2))	→	a__U22(mark(X1),X2)	(36)
mark(U23(X))	→	a__U23(mark(X))	(37)
mark(U31(X1,X2))	→	a__U31(mark(X1),X2)	(38)
mark(U32(X))	→	a__U32(mark(X))	(39)
mark(U41(X))	→	a__U41(mark(X))	(40)
mark(U51(X1,X2))	→	a__U51(mark(X1),X2)	(41)
mark(U52(X1,X2))	→	a__U52(mark(X1),X2)	(42)
mark(U61(X1,X2,X3))	→	a__U61(mark(X1),X2,X3)	(43)
mark(U62(X1,X2,X3))	→	a__U62(mark(X1),X2,X3)	(44)
mark(U63(X1,X2,X3))	→	a__U63(mark(X1),X2,X3)	(45)
mark(U64(X1,X2,X3))	→	a__U64(mark(X1),X2,X3)	(46)
mark(plus(X1,X2))	→	a__plus(mark(X1),mark(X2))	(47)
mark(tt)	→	tt	(48)
mark(s(X))	→	s(mark(X))	(49)
mark(0)	→	0	(50)
a__U11(X1,X2,X3)	→	U11(X1,X2,X3)	(51)
a__U12(X1,X2,X3)	→	U12(X1,X2,X3)	(52)
a__isNatKind(X)	→	isNatKind(X)	(53)
a__U13(X1,X2,X3)	→	U13(X1,X2,X3)	(54)
a__U14(X1,X2,X3)	→	U14(X1,X2,X3)	(55)
a__U15(X1,X2)	→	U15(X1,X2)	(56)
a__isNat(X)	→	isNat(X)	(57)
a__U16(X)	→	U16(X)	(58)
a__U21(X1,X2)	→	U21(X1,X2)	(59)
a__U22(X1,X2)	→	U22(X1,X2)	(60)
a__U23(X)	→	U23(X)	(61)
a__U31(X1,X2)	→	U31(X1,X2)	(62)
a__U32(X)	→	U32(X)	(63)
a__U41(X)	→	U41(X)	(64)
a__U51(X1,X2)	→	U51(X1,X2)	(65)
a__U52(X1,X2)	→	U52(X1,X2)	(66)
a__U61(X1,X2,X3)	→	U61(X1,X2,X3)	(67)
a__U62(X1,X2,X3)	→	U62(X1,X2,X3)	(68)
a__U63(X1,X2,X3)	→	U63(X1,X2,X3)	(69)
a__U64(X1,X2,X3)	→	U64(X1,X2,X3)	(70)
a__plus(X1,X2)	→	plus(X1,X2)	(71)

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

a__U64^#(tt,M,N)	→	mark^#(M)	(97)
mark^#(U51(X1,X2))	→	mark^#(X1)	(138)
mark^#(U61(X1,X2,X3))	→	mark^#(X1)	(142)
mark^#(U62(X1,X2,X3))	→	mark^#(X1)	(144)
mark^#(U63(X1,X2,X3))	→	mark^#(X1)	(146)
a__U64^#(tt,M,N)	→	mark^#(N)	(98)
mark^#(plus(X1,X2))	→	mark^#(X2)	(150)
mark^#(plus(X1,X2))	→	mark^#(X1)	(151)

could be deleted.

1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.

The 1^st component contains the pair

mark^#(U64(X1,X2,X3))	→	mark^#(X1)	(148)
mark^#(U11(X1,X2,X3))	→	mark^#(X1)	(112)
mark^#(U12(X1,X2,X3))	→	mark^#(X1)	(114)
mark^#(U13(X1,X2,X3))	→	mark^#(X1)	(117)
mark^#(U14(X1,X2,X3))	→	mark^#(X1)	(119)
mark^#(U15(X1,X2))	→	mark^#(X1)	(121)
mark^#(U16(X))	→	mark^#(X)	(124)
mark^#(U21(X1,X2))	→	mark^#(X1)	(126)
mark^#(U22(X1,X2))	→	mark^#(X1)	(128)
mark^#(U23(X))	→	mark^#(X)	(130)
mark^#(U31(X1,X2))	→	mark^#(X1)	(132)
mark^#(U32(X))	→	mark^#(X)	(134)
mark^#(U41(X))	→	mark^#(X)	(136)
mark^#(U52(X1,X2))	→	mark^#(X1)	(140)
mark^#(U52(X1,X2))	→	a__U52^#(mark(X1),X2)	(141)
a__U52^#(tt,N)	→	mark^#(N)	(90)
mark^#(s(X))	→	mark^#(X)	(153)

1.1.1.1.1.1.1 Subterm Criterion Processor

We use the projection

π(mark^#)	=	1
π(a__U52^#)	=	2

and remove the pairs:

mark^#(U64(X1,X2,X3))	→	mark^#(X1)	(148)
mark^#(U11(X1,X2,X3))	→	mark^#(X1)	(112)
mark^#(U12(X1,X2,X3))	→	mark^#(X1)	(114)
mark^#(U13(X1,X2,X3))	→	mark^#(X1)	(117)
mark^#(U14(X1,X2,X3))	→	mark^#(X1)	(119)
mark^#(U15(X1,X2))	→	mark^#(X1)	(121)
mark^#(U16(X))	→	mark^#(X)	(124)
mark^#(U21(X1,X2))	→	mark^#(X1)	(126)
mark^#(U22(X1,X2))	→	mark^#(X1)	(128)
mark^#(U23(X))	→	mark^#(X)	(130)
mark^#(U31(X1,X2))	→	mark^#(X1)	(132)
mark^#(U32(X))	→	mark^#(X)	(134)
mark^#(U41(X))	→	mark^#(X)	(136)
mark^#(U52(X1,X2))	→	mark^#(X1)	(140)
mark^#(U52(X1,X2))	→	a__U52^#(mark(X1),X2)	(141)
mark^#(s(X))	→	mark^#(X)	(153)

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

a__plus^#(N,s(M))	→	a__U61^#(a__isNat(M),M,N)	(111)
a__U61^#(tt,M,N)	→	a__U62^#(a__isNatKind(M),M,N)	(92)
a__U62^#(tt,M,N)	→	a__U63^#(a__isNat(N),M,N)	(94)
a__U63^#(tt,M,N)	→	a__U64^#(a__isNatKind(N),M,N)	(96)
a__U64^#(tt,M,N)	→	a__plus^#(mark(N),mark(M))	(99)

1.1.1.1.1.1.2 Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the rationals with delta = 1/64

[a__U61(x₁, x₂, x₃)]	=	0 · x₁ + 3 · x₂ + 1 · x₃ + 1/2
[a__U13(x₁, x₂, x₃)]	=	0 · x₁ + 0 · x₂ + 0 · x₃ + 0
[a__U51(x₁, x₂)]	=	0 · x₁ + 1 · x₂ + 0
[a__U16(x₁)]	=	0 · x₁ + 0
[a__U11(x₁, x₂, x₃)]	=	0 · x₁ + 0 · x₂ + 0 · x₃ + 0
[a__U12(x₁, x₂, x₃)]	=	0 · x₁ + 0 · x₂ + 0 · x₃ + 0
[a__U52(x₁, x₂)]	=	0 · x₁ + 1 · x₂ + 0
[a__U64(x₁, x₂, x₃)]	=	0 · x₁ + 3 · x₂ + 1 · x₃ + 1/2
[U23(x₁)]	=	0 · x₁ + 0
[U11(x₁, x₂, x₃)]	=	0 · x₁ + 0 · x₂ + 0 · x₃ + 0
[a__U61^#(x₁, x₂, x₃)]	=	0 · x₁ + 2 · x₂ + 1 · x₃ + 1
[isNat(x₁)]	=	3 · x₁ + 0
[a__U62(x₁, x₂, x₃)]	=	0 · x₁ + 3 · x₂ + 1 · x₃ + 1/2
[mark(x₁)]	=	1 · x₁ + 0
[U12(x₁, x₂, x₃)]	=	0 · x₁ + 0 · x₂ + 0 · x₃ + 0
[U21(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + 3/2
[a__plus(x₁, x₂)]	=	1 · x₁ + 3 · x₂ + 0
[isNatKind(x₁)]	=	0 · x₁ + 1
[a__U63^#(x₁, x₂, x₃)]	=	0 · x₁ + 2 · x₂ + 1 · x₃ + 1/2
[U63(x₁, x₂, x₃)]	=	0 · x₁ + 3 · x₂ + 1 · x₃ + 1/2
[a__U14(x₁, x₂, x₃)]	=	0 · x₁ + 0 · x₂ + 0 · x₃ + 0
[U16(x₁)]	=	0 · x₁ + 0
[a__U62^#(x₁, x₂, x₃)]	=	1/2 · x₁ + 2 · x₂ + 1 · x₃ + 1/2
[a__U22(x₁, x₂)]	=	1/2 · x₁ + 0 · x₂ + 1
[tt]	=	0
[U41(x₁)]	=	0 · x₁ + 0
[a__U15(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + 0
[a__U63(x₁, x₂, x₃)]	=	0 · x₁ + 3 · x₂ + 1 · x₃ + 1/2
[plus(x₁, x₂)]	=	1 · x₁ + 3 · x₂ + 0
[U14(x₁, x₂, x₃)]	=	0 · x₁ + 0 · x₂ + 0 · x₃ + 0
[a__U41(x₁)]	=	0 · x₁ + 0
[U15(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + 0
[a__U31(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + 0
[U64(x₁, x₂, x₃)]	=	0 · x₁ + 3 · x₂ + 1 · x₃ + 1/2
[s(x₁)]	=	1 · x₁ + 1/2
[0]	=	2
[a__U23(x₁)]	=	0 · x₁ + 0
[a__U21(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + 3/2
[a__U32(x₁)]	=	0 · x₁ + 0
[U51(x₁, x₂)]	=	0 · x₁ + 1 · x₂ + 0
[a__plus^#(x₁, x₂)]	=	1 · x₁ + 2 · x₂ + 1/2
[a__isNat(x₁)]	=	3 · x₁ + 0
[U32(x₁)]	=	0 · x₁ + 0
[U31(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + 0
[U52(x₁, x₂)]	=	0 · x₁ + 1 · x₂ + 0
[U61(x₁, x₂, x₃)]	=	0 · x₁ + 3 · x₂ + 1 · x₃ + 1/2
[a__U64^#(x₁, x₂, x₃)]	=	0 · x₁ + 2 · x₂ + 1 · x₃ + 1/2
[U22(x₁, x₂)]	=	1/2 · x₁ + 0 · x₂ + 1
[U13(x₁, x₂, x₃)]	=	0 · x₁ + 0 · x₂ + 0 · x₃ + 0
[U62(x₁, x₂, x₃)]	=	0 · x₁ + 3 · x₂ + 1 · x₃ + 1/2
[a__isNatKind(x₁)]	=	0 · x₁ + 1

together with the usable rules

a__U11(tt,V1,V2)	→	a__U12(a__isNatKind(V1),V1,V2)	(1)
a__U12(tt,V1,V2)	→	a__U13(a__isNatKind(V2),V1,V2)	(2)
a__U13(tt,V1,V2)	→	a__U14(a__isNatKind(V2),V1,V2)	(3)
a__U14(tt,V1,V2)	→	a__U15(a__isNat(V1),V2)	(4)
a__U15(tt,V2)	→	a__U16(a__isNat(V2))	(5)
a__U16(tt)	→	tt	(6)
a__U21(tt,V1)	→	a__U22(a__isNatKind(V1),V1)	(7)
a__U22(tt,V1)	→	a__U23(a__isNat(V1))	(8)
a__U23(tt)	→	tt	(9)
a__U31(tt,V2)	→	a__U32(a__isNatKind(V2))	(10)
a__U32(tt)	→	tt	(11)
a__U41(tt)	→	tt	(12)
a__U51(tt,N)	→	a__U52(a__isNatKind(N),N)	(13)
a__U52(tt,N)	→	mark(N)	(14)
a__U61(tt,M,N)	→	a__U62(a__isNatKind(M),M,N)	(15)
a__U62(tt,M,N)	→	a__U63(a__isNat(N),M,N)	(16)
a__U63(tt,M,N)	→	a__U64(a__isNatKind(N),M,N)	(17)
a__U64(tt,M,N)	→	s(a__plus(mark(N),mark(M)))	(18)
a__isNat(0)	→	tt	(19)
a__isNat(plus(V1,V2))	→	a__U11(a__isNatKind(V1),V1,V2)	(20)
a__isNat(s(V1))	→	a__U21(a__isNatKind(V1),V1)	(21)
a__isNatKind(0)	→	tt	(22)
a__isNatKind(plus(V1,V2))	→	a__U31(a__isNatKind(V1),V2)	(23)
a__isNatKind(s(V1))	→	a__U41(a__isNatKind(V1))	(24)
a__plus(N,0)	→	a__U51(a__isNat(N),N)	(25)
a__plus(N,s(M))	→	a__U61(a__isNat(M),M,N)	(26)
mark(U11(X1,X2,X3))	→	a__U11(mark(X1),X2,X3)	(27)
mark(U12(X1,X2,X3))	→	a__U12(mark(X1),X2,X3)	(28)
mark(isNatKind(X))	→	a__isNatKind(X)	(29)
mark(U13(X1,X2,X3))	→	a__U13(mark(X1),X2,X3)	(30)
mark(U14(X1,X2,X3))	→	a__U14(mark(X1),X2,X3)	(31)
mark(U15(X1,X2))	→	a__U15(mark(X1),X2)	(32)
mark(isNat(X))	→	a__isNat(X)	(33)
mark(U16(X))	→	a__U16(mark(X))	(34)
mark(U21(X1,X2))	→	a__U21(mark(X1),X2)	(35)
mark(U22(X1,X2))	→	a__U22(mark(X1),X2)	(36)
mark(U23(X))	→	a__U23(mark(X))	(37)
mark(U31(X1,X2))	→	a__U31(mark(X1),X2)	(38)
mark(U32(X))	→	a__U32(mark(X))	(39)
mark(U41(X))	→	a__U41(mark(X))	(40)
mark(U51(X1,X2))	→	a__U51(mark(X1),X2)	(41)
mark(U52(X1,X2))	→	a__U52(mark(X1),X2)	(42)
mark(U61(X1,X2,X3))	→	a__U61(mark(X1),X2,X3)	(43)
mark(U62(X1,X2,X3))	→	a__U62(mark(X1),X2,X3)	(44)
mark(U63(X1,X2,X3))	→	a__U63(mark(X1),X2,X3)	(45)
mark(U64(X1,X2,X3))	→	a__U64(mark(X1),X2,X3)	(46)
mark(plus(X1,X2))	→	a__plus(mark(X1),mark(X2))	(47)
mark(tt)	→	tt	(48)
mark(s(X))	→	s(mark(X))	(49)
mark(0)	→	0	(50)
a__U11(X1,X2,X3)	→	U11(X1,X2,X3)	(51)
a__U12(X1,X2,X3)	→	U12(X1,X2,X3)	(52)
a__isNatKind(X)	→	isNatKind(X)	(53)
a__U13(X1,X2,X3)	→	U13(X1,X2,X3)	(54)
a__U14(X1,X2,X3)	→	U14(X1,X2,X3)	(55)
a__U15(X1,X2)	→	U15(X1,X2)	(56)
a__isNat(X)	→	isNat(X)	(57)
a__U16(X)	→	U16(X)	(58)
a__U21(X1,X2)	→	U21(X1,X2)	(59)
a__U22(X1,X2)	→	U22(X1,X2)	(60)
a__U23(X)	→	U23(X)	(61)
a__U31(X1,X2)	→	U31(X1,X2)	(62)
a__U32(X)	→	U32(X)	(63)
a__U41(X)	→	U41(X)	(64)
a__U51(X1,X2)	→	U51(X1,X2)	(65)
a__U52(X1,X2)	→	U52(X1,X2)	(66)
a__U61(X1,X2,X3)	→	U61(X1,X2,X3)	(67)
a__U62(X1,X2,X3)	→	U62(X1,X2,X3)	(68)
a__U63(X1,X2,X3)	→	U63(X1,X2,X3)	(69)
a__U64(X1,X2,X3)	→	U64(X1,X2,X3)	(70)
a__plus(X1,X2)	→	plus(X1,X2)	(71)

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

a__plus^#(N,s(M))

→

a__U61^#(a__isNat(M),M,N)

(111)

could be deleted.

1.1.1.1.1.1.2.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 2^nd component contains the pair

a__U11^#(tt,V1,V2)	→	a__U12^#(a__isNatKind(V1),V1,V2)	(73)
a__U12^#(tt,V1,V2)	→	a__U13^#(a__isNatKind(V2),V1,V2)	(75)
a__U13^#(tt,V1,V2)	→	a__U14^#(a__isNatKind(V2),V1,V2)	(77)
a__U14^#(tt,V1,V2)	→	a__isNat^#(V1)	(78)
a__isNat^#(plus(V1,V2))	→	a__U11^#(a__isNatKind(V1),V1,V2)	(101)
a__isNat^#(s(V1))	→	a__U21^#(a__isNatKind(V1),V1)	(103)
a__U21^#(tt,V1)	→	a__U22^#(a__isNatKind(V1),V1)	(83)
a__U22^#(tt,V1)	→	a__isNat^#(V1)	(84)
a__U14^#(tt,V1,V2)	→	a__U15^#(a__isNat(V1),V2)	(79)
a__U15^#(tt,V2)	→	a__isNat^#(V2)	(80)

1.1.2 Size-Change Termination

Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.

a__U11^#(tt,V1,V2)	→	a__U12^#(a__isNatKind(V1),V1,V2)	(73)

3	≥	3
2	≥	2
a__U12^#(tt,V1,V2)	→	a__U13^#(a__isNatKind(V2),V1,V2)	(75)

3	≥	3
2	≥	2
a__U13^#(tt,V1,V2)	→	a__U14^#(a__isNatKind(V2),V1,V2)	(77)

3	≥	3
2	≥	2
a__U14^#(tt,V1,V2)	→	a__isNat^#(V1)	(78)

2	≥	1
a__isNat^#(plus(V1,V2))	→	a__U11^#(a__isNatKind(V1),V1,V2)	(101)

1	>	3
1	>	2
a__isNat^#(s(V1))	→	a__U21^#(a__isNatKind(V1),V1)	(103)

1	>	2
a__U21^#(tt,V1)	→	a__U22^#(a__isNatKind(V1),V1)	(83)

2	≥	2
a__U22^#(tt,V1)	→	a__isNat^#(V1)	(84)

2	≥	1
a__U14^#(tt,V1,V2)	→	a__U15^#(a__isNat(V1),V2)	(79)

3	≥	2
a__U15^#(tt,V2)	→	a__isNat^#(V2)	(80)

2	≥	1

As there is no critical graph in the transitive closure, there are no infinite chains.

The 3^rd component contains the pair

a__isNatKind^#(plus(V1,V2))	→	a__isNatKind^#(V1)	(104)
a__isNatKind^#(plus(V1,V2))	→	a__U31^#(a__isNatKind(V1),V2)	(105)
a__U31^#(tt,V2)	→	a__isNatKind^#(V2)	(86)
a__isNatKind^#(s(V1))	→	a__isNatKind^#(V1)	(106)

1.1.3 Size-Change Termination

Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.

a__isNatKind^#(plus(V1,V2))	→	a__isNatKind^#(V1)	(104)

1	>	1
a__isNatKind^#(plus(V1,V2))	→	a__U31^#(a__isNatKind(V1),V2)	(105)

1	>	2
a__U31^#(tt,V2)	→	a__isNatKind^#(V2)	(86)

2	≥	1
a__isNatKind^#(s(V1))	→	a__isNatKind^#(V1)	(106)

1	>	1

As there is no critical graph in the transitive closure, there are no infinite chains.