Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/MYNAT_complete_GM)

The rewrite relation of the following TRS is considered.

a__U11(tt,V1,V2)	→	a__U12(a__isNat(V1),V2)	(1)
a__U12(tt,V2)	→	a__U13(a__isNat(V2))	(2)
a__U13(tt)	→	tt	(3)
a__U21(tt,V1)	→	a__U22(a__isNat(V1))	(4)
a__U22(tt)	→	tt	(5)
a__U31(tt,V1,V2)	→	a__U32(a__isNat(V1),V2)	(6)
a__U32(tt,V2)	→	a__U33(a__isNat(V2))	(7)
a__U33(tt)	→	tt	(8)
a__U41(tt,N)	→	mark(N)	(9)
a__U51(tt,M,N)	→	s(a__plus(mark(N),mark(M)))	(10)
a__U61(tt)	→	0	(11)
a__U71(tt,M,N)	→	a__plus(a__x(mark(N),mark(M)),mark(N))	(12)
a__and(tt,X)	→	mark(X)	(13)
a__isNat(0)	→	tt	(14)
a__isNat(plus(V1,V2))	→	a__U11(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2)	(15)
a__isNat(s(V1))	→	a__U21(a__isNatKind(V1),V1)	(16)
a__isNat(x(V1,V2))	→	a__U31(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2)	(17)
a__isNatKind(0)	→	tt	(18)
a__isNatKind(plus(V1,V2))	→	a__and(a__isNatKind(V1),isNatKind(V2))	(19)
a__isNatKind(s(V1))	→	a__isNatKind(V1)	(20)
a__isNatKind(x(V1,V2))	→	a__and(a__isNatKind(V1),isNatKind(V2))	(21)
a__plus(N,0)	→	a__U41(a__and(a__isNat(N),isNatKind(N)),N)	(22)
a__plus(N,s(M))	→	a__U51(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N)	(23)
a__x(N,0)	→	a__U61(a__and(a__isNat(N),isNatKind(N)))	(24)
a__x(N,s(M))	→	a__U71(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N)	(25)
mark(U11(X1,X2,X3))	→	a__U11(mark(X1),X2,X3)	(26)
mark(U12(X1,X2))	→	a__U12(mark(X1),X2)	(27)
mark(isNat(X))	→	a__isNat(X)	(28)
mark(U13(X))	→	a__U13(mark(X))	(29)
mark(U21(X1,X2))	→	a__U21(mark(X1),X2)	(30)
mark(U22(X))	→	a__U22(mark(X))	(31)
mark(U31(X1,X2,X3))	→	a__U31(mark(X1),X2,X3)	(32)
mark(U32(X1,X2))	→	a__U32(mark(X1),X2)	(33)
mark(U33(X))	→	a__U33(mark(X))	(34)
mark(U41(X1,X2))	→	a__U41(mark(X1),X2)	(35)
mark(U51(X1,X2,X3))	→	a__U51(mark(X1),X2,X3)	(36)
mark(plus(X1,X2))	→	a__plus(mark(X1),mark(X2))	(37)
mark(U61(X))	→	a__U61(mark(X))	(38)
mark(U71(X1,X2,X3))	→	a__U71(mark(X1),X2,X3)	(39)
mark(x(X1,X2))	→	a__x(mark(X1),mark(X2))	(40)
mark(and(X1,X2))	→	a__and(mark(X1),X2)	(41)
mark(isNatKind(X))	→	a__isNatKind(X)	(42)
mark(tt)	→	tt	(43)
mark(s(X))	→	s(mark(X))	(44)
mark(0)	→	0	(45)
a__U11(X1,X2,X3)	→	U11(X1,X2,X3)	(46)
a__U12(X1,X2)	→	U12(X1,X2)	(47)
a__isNat(X)	→	isNat(X)	(48)
a__U13(X)	→	U13(X)	(49)
a__U21(X1,X2)	→	U21(X1,X2)	(50)
a__U22(X)	→	U22(X)	(51)
a__U31(X1,X2,X3)	→	U31(X1,X2,X3)	(52)
a__U32(X1,X2)	→	U32(X1,X2)	(53)
a__U33(X)	→	U33(X)	(54)
a__U41(X1,X2)	→	U41(X1,X2)	(55)
a__U51(X1,X2,X3)	→	U51(X1,X2,X3)	(56)
a__plus(X1,X2)	→	plus(X1,X2)	(57)
a__U61(X)	→	U61(X)	(58)
a__U71(X1,X2,X3)	→	U71(X1,X2,X3)	(59)
a__x(X1,X2)	→	x(X1,X2)	(60)
a__and(X1,X2)	→	and(X1,X2)	(61)
a__isNatKind(X)	→	isNatKind(X)	(62)

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.

a__U12^#(tt,V2)	→	a__isNat^#(V2)	(63)
a__U32^#(tt,V2)	→	a__U33^#(a__isNat(V2))	(64)
a__U71^#(tt,M,N)	→	a__plus^#(a__x(mark(N),mark(M)),mark(N))	(65)
mark^#(U22(X))	→	mark^#(X)	(66)
a__isNatKind^#(plus(V1,V2))	→	a__and^#(a__isNatKind(V1),isNatKind(V2))	(67)
mark^#(U71(X1,X2,X3))	→	mark^#(X1)	(68)
a__isNatKind^#(s(V1))	→	a__isNatKind^#(V1)	(69)
a__x^#(N,s(M))	→	a__isNat^#(M)	(70)
mark^#(U21(X1,X2))	→	mark^#(X1)	(71)
a__isNatKind^#(x(V1,V2))	→	a__isNatKind^#(V1)	(72)
a__U51^#(tt,M,N)	→	a__plus^#(mark(N),mark(M))	(73)
mark^#(isNat(X))	→	a__isNat^#(X)	(74)
mark^#(U51(X1,X2,X3))	→	mark^#(X1)	(75)
a__U51^#(tt,M,N)	→	mark^#(N)	(76)
a__isNat^#(s(V1))	→	a__isNatKind^#(V1)	(77)
a__isNat^#(s(V1))	→	a__U21^#(a__isNatKind(V1),V1)	(78)
mark^#(U33(X))	→	mark^#(X)	(79)
a__isNat^#(x(V1,V2))	→	a__U31^#(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2)	(80)
a__x^#(N,s(M))	→	a__U71^#(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N)	(81)
mark^#(U41(X1,X2))	→	mark^#(X1)	(82)
mark^#(U12(X1,X2))	→	a__U12^#(mark(X1),X2)	(83)
a__plus^#(N,0)	→	a__and^#(a__isNat(N),isNatKind(N))	(84)
a__isNatKind^#(plus(V1,V2))	→	a__isNatKind^#(V1)	(85)
a__x^#(N,s(M))	→	a__and^#(a__isNat(M),isNatKind(M))	(86)
mark^#(U32(X1,X2))	→	mark^#(X1)	(87)
mark^#(U61(X))	→	a__U61^#(mark(X))	(88)
mark^#(and(X1,X2))	→	mark^#(X1)	(89)
mark^#(plus(X1,X2))	→	mark^#(X1)	(90)
mark^#(U33(X))	→	a__U33^#(mark(X))	(91)
a__U11^#(tt,V1,V2)	→	a__U12^#(a__isNat(V1),V2)	(92)
a__x^#(N,0)	→	a__isNat^#(N)	(93)
mark^#(U51(X1,X2,X3))	→	a__U51^#(mark(X1),X2,X3)	(94)
a__x^#(N,0)	→	a__and^#(a__isNat(N),isNatKind(N))	(95)
a__U21^#(tt,V1)	→	a__U22^#(a__isNat(V1))	(96)
a__isNat^#(plus(V1,V2))	→	a__U11^#(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2)	(97)
mark^#(U71(X1,X2,X3))	→	a__U71^#(mark(X1),X2,X3)	(98)
mark^#(U11(X1,X2,X3))	→	mark^#(X1)	(99)
mark^#(plus(X1,X2))	→	mark^#(X2)	(100)
a__U71^#(tt,M,N)	→	mark^#(N)	(101)
a__isNat^#(plus(V1,V2))	→	a__and^#(a__isNatKind(V1),isNatKind(V2))	(102)
a__plus^#(N,0)	→	a__isNat^#(N)	(103)
a__U21^#(tt,V1)	→	a__isNat^#(V1)	(104)
mark^#(U61(X))	→	mark^#(X)	(105)
a__isNat^#(x(V1,V2))	→	a__and^#(a__isNatKind(V1),isNatKind(V2))	(106)
a__U71^#(tt,M,N)	→	a__x^#(mark(N),mark(M))	(107)
mark^#(s(X))	→	mark^#(X)	(108)
a__U51^#(tt,M,N)	→	mark^#(M)	(109)
a__plus^#(N,s(M))	→	a__U51^#(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N)	(110)
a__and^#(tt,X)	→	mark^#(X)	(111)
mark^#(isNatKind(X))	→	a__isNatKind^#(X)	(112)
a__x^#(N,s(M))	→	a__and^#(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N)))	(113)
mark^#(plus(X1,X2))	→	a__plus^#(mark(X1),mark(X2))	(114)
mark^#(U31(X1,X2,X3))	→	a__U31^#(mark(X1),X2,X3)	(115)
a__U71^#(tt,M,N)	→	mark^#(N)	(101)
a__isNatKind^#(x(V1,V2))	→	a__and^#(a__isNatKind(V1),isNatKind(V2))	(116)
mark^#(U41(X1,X2))	→	a__U41^#(mark(X1),X2)	(117)
a__U32^#(tt,V2)	→	a__isNat^#(V2)	(118)
mark^#(U31(X1,X2,X3))	→	mark^#(X1)	(119)
a__plus^#(N,s(M))	→	a__isNat^#(M)	(120)
a__x^#(N,0)	→	a__U61^#(a__and(a__isNat(N),isNatKind(N)))	(121)
mark^#(U22(X))	→	a__U22^#(mark(X))	(122)
a__plus^#(N,s(M))	→	a__and^#(a__isNat(M),isNatKind(M))	(123)
mark^#(U12(X1,X2))	→	mark^#(X1)	(124)
mark^#(x(X1,X2))	→	a__x^#(mark(X1),mark(X2))	(125)
a__U71^#(tt,M,N)	→	mark^#(M)	(126)
mark^#(x(X1,X2))	→	mark^#(X2)	(127)
a__isNat^#(x(V1,V2))	→	a__isNatKind^#(V1)	(128)
a__plus^#(N,s(M))	→	a__and^#(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N)))	(129)
mark^#(U11(X1,X2,X3))	→	a__U11^#(mark(X1),X2,X3)	(130)
mark^#(U21(X1,X2))	→	a__U21^#(mark(X1),X2)	(131)
a__U41^#(tt,N)	→	mark^#(N)	(132)
a__U31^#(tt,V1,V2)	→	a__isNat^#(V1)	(133)
mark^#(U13(X))	→	a__U13^#(mark(X))	(134)
a__U11^#(tt,V1,V2)	→	a__isNat^#(V1)	(135)
a__U12^#(tt,V2)	→	a__U13^#(a__isNat(V2))	(136)
a__plus^#(N,0)	→	a__U41^#(a__and(a__isNat(N),isNatKind(N)),N)	(137)
mark^#(and(X1,X2))	→	a__and^#(mark(X1),X2)	(138)
a__U31^#(tt,V1,V2)	→	a__U32^#(a__isNat(V1),V2)	(139)
mark^#(U13(X))	→	mark^#(X)	(140)
a__isNat^#(plus(V1,V2))	→	a__isNatKind^#(V1)	(141)
mark^#(U32(X1,X2))	→	a__U32^#(mark(X1),X2)	(142)
mark^#(x(X1,X2))	→	mark^#(X1)	(143)

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

mark^#(x(X1,X2))	→	mark^#(X1)	(143)
a__isNat^#(plus(V1,V2))	→	a__isNatKind^#(V1)	(141)
mark^#(U32(X1,X2))	→	a__U32^#(mark(X1),X2)	(142)
a__plus^#(N,s(M))	→	a__U51^#(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N)	(110)
mark^#(s(X))	→	mark^#(X)	(108)
a__U51^#(tt,M,N)	→	mark^#(M)	(109)
mark^#(U13(X))	→	mark^#(X)	(140)
a__isNat^#(x(V1,V2))	→	a__and^#(a__isNatKind(V1),isNatKind(V2))	(106)
a__U71^#(tt,M,N)	→	a__x^#(mark(N),mark(M))	(107)
mark^#(U61(X))	→	mark^#(X)	(105)
a__U21^#(tt,V1)	→	a__isNat^#(V1)	(104)
a__U31^#(tt,V1,V2)	→	a__U32^#(a__isNat(V1),V2)	(139)
a__isNat^#(plus(V1,V2))	→	a__and^#(a__isNatKind(V1),isNatKind(V2))	(102)
a__plus^#(N,0)	→	a__isNat^#(N)	(103)
a__U71^#(tt,M,N)	→	mark^#(N)	(101)
mark^#(plus(X1,X2))	→	mark^#(X2)	(100)
mark^#(U11(X1,X2,X3))	→	mark^#(X1)	(99)
mark^#(and(X1,X2))	→	a__and^#(mark(X1),X2)	(138)
mark^#(U71(X1,X2,X3))	→	a__U71^#(mark(X1),X2,X3)	(98)
a__plus^#(N,0)	→	a__U41^#(a__and(a__isNat(N),isNatKind(N)),N)	(137)
a__isNat^#(plus(V1,V2))	→	a__U11^#(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2)	(97)
a__x^#(N,0)	→	a__and^#(a__isNat(N),isNatKind(N))	(95)
a__U11^#(tt,V1,V2)	→	a__isNat^#(V1)	(135)
mark^#(U51(X1,X2,X3))	→	a__U51^#(mark(X1),X2,X3)	(94)
a__x^#(N,0)	→	a__isNat^#(N)	(93)
a__U31^#(tt,V1,V2)	→	a__isNat^#(V1)	(133)
a__U41^#(tt,N)	→	mark^#(N)	(132)
a__U11^#(tt,V1,V2)	→	a__U12^#(a__isNat(V1),V2)	(92)
mark^#(U21(X1,X2))	→	a__U21^#(mark(X1),X2)	(131)
mark^#(U11(X1,X2,X3))	→	a__U11^#(mark(X1),X2,X3)	(130)
a__plus^#(N,s(M))	→	a__and^#(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N)))	(129)
mark^#(plus(X1,X2))	→	mark^#(X1)	(90)
mark^#(and(X1,X2))	→	mark^#(X1)	(89)
a__isNat^#(x(V1,V2))	→	a__isNatKind^#(V1)	(128)
mark^#(U32(X1,X2))	→	mark^#(X1)	(87)
a__U71^#(tt,M,N)	→	mark^#(M)	(126)
mark^#(x(X1,X2))	→	mark^#(X2)	(127)
mark^#(x(X1,X2))	→	a__x^#(mark(X1),mark(X2))	(125)
a__x^#(N,s(M))	→	a__and^#(a__isNat(M),isNatKind(M))	(86)
a__isNatKind^#(plus(V1,V2))	→	a__isNatKind^#(V1)	(85)
a__plus^#(N,0)	→	a__and^#(a__isNat(N),isNatKind(N))	(84)
mark^#(U12(X1,X2))	→	mark^#(X1)	(124)
mark^#(U12(X1,X2))	→	a__U12^#(mark(X1),X2)	(83)
mark^#(U41(X1,X2))	→	mark^#(X1)	(82)
a__plus^#(N,s(M))	→	a__and^#(a__isNat(M),isNatKind(M))	(123)
a__isNat^#(x(V1,V2))	→	a__U31^#(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2)	(80)
a__x^#(N,s(M))	→	a__U71^#(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N)	(81)
mark^#(U33(X))	→	mark^#(X)	(79)
a__isNat^#(s(V1))	→	a__U21^#(a__isNatKind(V1),V1)	(78)
a__isNat^#(s(V1))	→	a__isNatKind^#(V1)	(77)
a__U51^#(tt,M,N)	→	mark^#(N)	(76)
mark^#(U51(X1,X2,X3))	→	mark^#(X1)	(75)
mark^#(isNat(X))	→	a__isNat^#(X)	(74)
a__plus^#(N,s(M))	→	a__isNat^#(M)	(120)
mark^#(U31(X1,X2,X3))	→	mark^#(X1)	(119)
a__isNatKind^#(x(V1,V2))	→	a__isNatKind^#(V1)	(72)
a__U51^#(tt,M,N)	→	a__plus^#(mark(N),mark(M))	(73)
a__U32^#(tt,V2)	→	a__isNat^#(V2)	(118)
mark^#(U41(X1,X2))	→	a__U41^#(mark(X1),X2)	(117)
a__isNatKind^#(x(V1,V2))	→	a__and^#(a__isNatKind(V1),isNatKind(V2))	(116)
mark^#(U21(X1,X2))	→	mark^#(X1)	(71)
mark^#(U31(X1,X2,X3))	→	a__U31^#(mark(X1),X2,X3)	(115)
a__U71^#(tt,M,N)	→	mark^#(N)	(101)
a__x^#(N,s(M))	→	a__isNat^#(M)	(70)
a__isNatKind^#(s(V1))	→	a__isNatKind^#(V1)	(69)
mark^#(plus(X1,X2))	→	a__plus^#(mark(X1),mark(X2))	(114)
mark^#(U71(X1,X2,X3))	→	mark^#(X1)	(68)
a__isNatKind^#(plus(V1,V2))	→	a__and^#(a__isNatKind(V1),isNatKind(V2))	(67)
a__x^#(N,s(M))	→	a__and^#(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N)))	(113)
mark^#(isNatKind(X))	→	a__isNatKind^#(X)	(112)
mark^#(U22(X))	→	mark^#(X)	(66)
a__U71^#(tt,M,N)	→	a__plus^#(a__x(mark(N),mark(M)),mark(N))	(65)
a__U12^#(tt,V2)	→	a__isNat^#(V2)	(63)
a__and^#(tt,X)	→	mark^#(X)	(111)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a__isNatKind^#(x₁)]	=	0
[isNatKind(x₁)]	=	0
[a__plus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 21654, 0)
[U21(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[a__U71^#(x₁, x₂, x₃)]	=	max(x₂ + 22758, x₃ + 22756, 0)
[U11(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 15452, 0)
[s(x₁)]	=	x₁ + 0
[a__U31^#(x₁, x₂, x₃)]	=	max(0)
[a__U33^#(x₁)]	=	0
[a__U33(x₁)]	=	x₁ + 5600
[a__isNat^#(x₁)]	=	0
[U71(x₁, x₂, x₃)]	=	max(x₁ + 21653, x₂ + 22758, x₃ + 22756, 0)
[and(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[a__U13^#(x₁)]	=	0
[a__U51^#(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 0, 0)
[a__x^#(x₁, x₂)]	=	max(x₁ + 22756, x₂ + 22758, 0)
[a__U22(x₁)]	=	x₁ + 0
[a__U11^#(x₁, x₂, x₃)]	=	max(0)
[a__U31(x₁, x₂, x₃)]	=	max(x₁ + 22758, x₂ + 22756, x₃ + 22757, 0)
[a__U51(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 21654, x₃ + 0, 0)
[a__x(x₁, x₂)]	=	max(x₁ + 22756, x₂ + 22758, 0)
[U12(x₁, x₂)]	=	max(x₁ + 0, x₂ + 6132, 0)
[a__U41(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[x(x₁, x₂)]	=	max(x₁ + 22756, x₂ + 22758, 0)
[a__U12^#(x₁, x₂)]	=	max(0)
[a__U21^#(x₁, x₂)]	=	max(0)
[a__U61^#(x₁)]	=	0
[a__plus^#(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[mark^#(x₁)]	=	x₁ + 0
[0]	=	14098
[a__and^#(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[a__U21(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[a__U32(x₁, x₂)]	=	max(x₁ + 1, x₂ + 21174, 0)
[mark(x₁)]	=	x₁ + 0
[a__U11(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 15452, 0)
[U32(x₁, x₂)]	=	max(x₁ + 1, x₂ + 21174, 0)
[U33(x₁)]	=	x₁ + 5600
[a__U12(x₁, x₂)]	=	max(x₁ + 0, x₂ + 6132, 0)
[isNat(x₁)]	=	x₁ + 0
[plus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 21654, 0)
[U61(x₁)]	=	x₁ + 14098
[a__U22^#(x₁)]	=	0
[a__U13(x₁)]	=	x₁ + 6132
[U31(x₁, x₂, x₃)]	=	max(x₁ + 22758, x₂ + 22756, x₃ + 22757, 0)
[a__U71(x₁, x₂, x₃)]	=	max(x₁ + 21653, x₂ + 22758, x₃ + 22756, 0)
[a__U61(x₁)]	=	x₁ + 14098
[a__U41^#(x₁, x₂)]	=	max(x₂ + 0, 0)
[tt]	=	0
[a__isNat(x₁)]	=	x₁ + 0
[U13(x₁)]	=	x₁ + 6132
[a__isNatKind(x₁)]	=	0
[U22(x₁)]	=	x₁ + 0
[U51(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 21654, x₃ + 0, 0)
[a__and(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[U41(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[a__U32^#(x₁, x₂)]	=	max(0)

together with the usable rules

a__isNatKind(0)	→	tt	(18)
a__U21(X1,X2)	→	U21(X1,X2)	(50)
a__U21(tt,V1)	→	a__U22(a__isNat(V1))	(4)
a__isNat(plus(V1,V2))	→	a__U11(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2)	(15)
a__U33(tt)	→	tt	(8)
a__U33(X)	→	U33(X)	(54)
a__U11(tt,V1,V2)	→	a__U12(a__isNat(V1),V2)	(1)
a__U13(tt)	→	tt	(3)
a__isNat(s(V1))	→	a__U21(a__isNatKind(V1),V1)	(16)
a__isNatKind(x(V1,V2))	→	a__and(a__isNatKind(V1),isNatKind(V2))	(21)
mark(U51(X1,X2,X3))	→	a__U51(mark(X1),X2,X3)	(36)
mark(U11(X1,X2,X3))	→	a__U11(mark(X1),X2,X3)	(26)
a__isNatKind(plus(V1,V2))	→	a__and(a__isNatKind(V1),isNatKind(V2))	(19)
mark(U31(X1,X2,X3))	→	a__U31(mark(X1),X2,X3)	(32)
a__isNat(x(V1,V2))	→	a__U31(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2)	(17)
a__x(X1,X2)	→	x(X1,X2)	(60)
mark(U12(X1,X2))	→	a__U12(mark(X1),X2)	(27)
mark(U33(X))	→	a__U33(mark(X))	(34)
a__plus(N,0)	→	a__U41(a__and(a__isNat(N),isNatKind(N)),N)	(22)
mark(isNat(X))	→	a__isNat(X)	(28)
mark(s(X))	→	s(mark(X))	(44)
a__U22(tt)	→	tt	(5)
mark(U32(X1,X2))	→	a__U32(mark(X1),X2)	(33)
a__U51(tt,M,N)	→	s(a__plus(mark(N),mark(M)))	(10)
mark(U71(X1,X2,X3))	→	a__U71(mark(X1),X2,X3)	(39)
a__U32(tt,V2)	→	a__U33(a__isNat(V2))	(7)
a__isNatKind(s(V1))	→	a__isNatKind(V1)	(20)
a__x(N,s(M))	→	a__U71(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N)	(25)
a__U13(X)	→	U13(X)	(49)
a__U31(X1,X2,X3)	→	U31(X1,X2,X3)	(52)
mark(U21(X1,X2))	→	a__U21(mark(X1),X2)	(30)
a__isNatKind(X)	→	isNatKind(X)	(62)
a__isNat(0)	→	tt	(14)
a__U51(X1,X2,X3)	→	U51(X1,X2,X3)	(56)
mark(U22(X))	→	a__U22(mark(X))	(31)
a__U71(tt,M,N)	→	a__plus(a__x(mark(N),mark(M)),mark(N))	(12)
mark(0)	→	0	(45)
a__plus(N,s(M))	→	a__U51(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N)	(23)
a__x(N,0)	→	a__U61(a__and(a__isNat(N),isNatKind(N)))	(24)
a__plus(X1,X2)	→	plus(X1,X2)	(57)
a__U61(tt)	→	0	(11)
a__U41(tt,N)	→	mark(N)	(9)
a__and(tt,X)	→	mark(X)	(13)
a__U22(X)	→	U22(X)	(51)
mark(x(X1,X2))	→	a__x(mark(X1),mark(X2))	(40)
a__U41(X1,X2)	→	U41(X1,X2)	(55)
a__U71(X1,X2,X3)	→	U71(X1,X2,X3)	(59)
a__U31(tt,V1,V2)	→	a__U32(a__isNat(V1),V2)	(6)
mark(U61(X))	→	a__U61(mark(X))	(38)
a__and(X1,X2)	→	and(X1,X2)	(61)
a__U61(X)	→	U61(X)	(58)
a__isNat(X)	→	isNat(X)	(48)
a__U32(X1,X2)	→	U32(X1,X2)	(53)
a__U12(X1,X2)	→	U12(X1,X2)	(47)
mark(plus(X1,X2))	→	a__plus(mark(X1),mark(X2))	(37)
mark(and(X1,X2))	→	a__and(mark(X1),X2)	(41)
mark(isNatKind(X))	→	a__isNatKind(X)	(42)
a__U11(X1,X2,X3)	→	U11(X1,X2,X3)	(46)
mark(U41(X1,X2))	→	a__U41(mark(X1),X2)	(35)
mark(U13(X))	→	a__U13(mark(X))	(29)
mark(tt)	→	tt	(43)
a__U12(tt,V2)	→	a__U13(a__isNat(V2))	(2)

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

mark^#(x(X1,X2))	→	mark^#(X1)	(143)
mark^#(U32(X1,X2))	→	a__U32^#(mark(X1),X2)	(142)
mark^#(U13(X))	→	mark^#(X)	(140)
mark^#(U61(X))	→	mark^#(X)	(105)
a__plus^#(N,0)	→	a__isNat^#(N)	(103)
a__U71^#(tt,M,N)	→	mark^#(N)	(101)
mark^#(plus(X1,X2))	→	mark^#(X2)	(100)
a__x^#(N,0)	→	a__and^#(a__isNat(N),isNatKind(N))	(95)
a__x^#(N,0)	→	a__isNat^#(N)	(93)
mark^#(U11(X1,X2,X3))	→	a__U11^#(mark(X1),X2,X3)	(130)
mark^#(U32(X1,X2))	→	mark^#(X1)	(87)
a__U71^#(tt,M,N)	→	mark^#(M)	(126)
mark^#(x(X1,X2))	→	mark^#(X2)	(127)
a__x^#(N,s(M))	→	a__and^#(a__isNat(M),isNatKind(M))	(86)
mark^#(U12(X1,X2))	→	a__U12^#(mark(X1),X2)	(83)
mark^#(U33(X))	→	mark^#(X)	(79)
mark^#(U31(X1,X2,X3))	→	mark^#(X1)	(119)
mark^#(U31(X1,X2,X3))	→	a__U31^#(mark(X1),X2,X3)	(115)
a__U71^#(tt,M,N)	→	mark^#(N)	(101)
a__x^#(N,s(M))	→	a__isNat^#(M)	(70)
mark^#(U71(X1,X2,X3))	→	mark^#(X1)	(68)
a__x^#(N,s(M))	→	a__and^#(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N)))	(113)

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__U21^#(tt,V1)	→	a__isNat^#(V1)	(104)
a__isNat^#(plus(V1,V2))	→	a__isNatKind^#(V1)	(141)
a__isNat^#(plus(V1,V2))	→	a__and^#(a__isNatKind(V1),isNatKind(V2))	(102)
a__isNat^#(plus(V1,V2))	→	a__U11^#(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2)	(97)
a__U11^#(tt,V1,V2)	→	a__isNat^#(V1)	(135)
a__U11^#(tt,V1,V2)	→	a__U12^#(a__isNat(V1),V2)	(92)
a__isNat^#(s(V1))	→	a__isNatKind^#(V1)	(77)
a__isNat^#(s(V1))	→	a__U21^#(a__isNatKind(V1),V1)	(78)
a__isNatKind^#(x(V1,V2))	→	a__isNatKind^#(V1)	(72)
a__isNatKind^#(x(V1,V2))	→	a__and^#(a__isNatKind(V1),isNatKind(V2))	(116)
mark^#(U51(X1,X2,X3))	→	mark^#(X1)	(75)
mark^#(U51(X1,X2,X3))	→	a__U51^#(mark(X1),X2,X3)	(94)
mark^#(U11(X1,X2,X3))	→	mark^#(X1)	(99)
a__isNatKind^#(plus(V1,V2))	→	a__isNatKind^#(V1)	(85)
a__isNatKind^#(plus(V1,V2))	→	a__and^#(a__isNatKind(V1),isNatKind(V2))	(67)
a__isNat^#(x(V1,V2))	→	a__isNatKind^#(V1)	(128)
a__isNat^#(x(V1,V2))	→	a__and^#(a__isNatKind(V1),isNatKind(V2))	(106)
a__isNat^#(x(V1,V2))	→	a__U31^#(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2)	(80)
mark^#(U12(X1,X2))	→	mark^#(X1)	(124)
a__plus^#(N,0)	→	a__and^#(a__isNat(N),isNatKind(N))	(84)
a__plus^#(N,0)	→	a__U41^#(a__and(a__isNat(N),isNatKind(N)),N)	(137)
mark^#(isNat(X))	→	a__isNat^#(X)	(74)
mark^#(s(X))	→	mark^#(X)	(108)
a__U51^#(tt,M,N)	→	mark^#(M)	(109)
a__U51^#(tt,M,N)	→	mark^#(N)	(76)
a__U51^#(tt,M,N)	→	a__plus^#(mark(N),mark(M))	(73)
mark^#(U71(X1,X2,X3))	→	a__U71^#(mark(X1),X2,X3)	(98)
a__U32^#(tt,V2)	→	a__isNat^#(V2)	(118)
a__isNatKind^#(s(V1))	→	a__isNatKind^#(V1)	(69)
a__x^#(N,s(M))	→	a__U71^#(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N)	(81)
mark^#(U21(X1,X2))	→	mark^#(X1)	(71)
mark^#(U21(X1,X2))	→	a__U21^#(mark(X1),X2)	(131)
mark^#(U22(X))	→	mark^#(X)	(66)
a__U71^#(tt,M,N)	→	a__x^#(mark(N),mark(M))	(107)
a__U71^#(tt,M,N)	→	a__plus^#(a__x(mark(N),mark(M)),mark(N))	(65)
a__plus^#(N,s(M))	→	a__isNat^#(M)	(120)
a__plus^#(N,s(M))	→	a__and^#(a__isNat(M),isNatKind(M))	(123)
a__plus^#(N,s(M))	→	a__and^#(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N)))	(129)
a__plus^#(N,s(M))	→	a__U51^#(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N)	(110)
a__U41^#(tt,N)	→	mark^#(N)	(132)
a__and^#(tt,X)	→	mark^#(X)	(111)
mark^#(x(X1,X2))	→	a__x^#(mark(X1),mark(X2))	(125)
a__U31^#(tt,V1,V2)	→	a__isNat^#(V1)	(133)
a__U31^#(tt,V1,V2)	→	a__U32^#(a__isNat(V1),V2)	(139)
mark^#(plus(X1,X2))	→	mark^#(X1)	(90)
mark^#(plus(X1,X2))	→	a__plus^#(mark(X1),mark(X2))	(114)
mark^#(and(X1,X2))	→	mark^#(X1)	(89)
mark^#(and(X1,X2))	→	a__and^#(mark(X1),X2)	(138)
mark^#(isNatKind(X))	→	a__isNatKind^#(X)	(112)
mark^#(U41(X1,X2))	→	mark^#(X1)	(82)
mark^#(U41(X1,X2))	→	a__U41^#(mark(X1),X2)	(117)
a__U12^#(tt,V2)	→	a__isNat^#(V2)	(63)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a__isNatKind^#(x₁)]	=	0
[isNatKind(x₁)]	=	0
[a__plus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 1, 0)
[U21(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[a__U71^#(x₁, x₂, x₃)]	=	max(x₂ + 4, x₃ + 2, 0)
[U11(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 1, 0)
[s(x₁)]	=	x₁ + 0
[a__U31^#(x₁, x₂, x₃)]	=	max(0)
[a__U33^#(x₁)]	=	0
[a__U33(x₁)]	=	x₁ + 2
[a__isNat^#(x₁)]	=	0
[U71(x₁, x₂, x₃)]	=	max(x₂ + 4, x₃ + 2, 0)
[and(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[a__U13^#(x₁)]	=	0
[a__U51^#(x₁, x₂, x₃)]	=	max(x₂ + 1, x₃ + 0, 0)
[a__x^#(x₁, x₂)]	=	max(x₁ + 2, x₂ + 4, 0)
[a__U22(x₁)]	=	x₁ + 0
[a__U11^#(x₁, x₂, x₃)]	=	max(0)
[a__U31(x₁, x₂, x₃)]	=	max(x₁ + 4, x₂ + 2, x₃ + 3, 0)
[a__U51(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 1, x₃ + 0, 0)
[a__x(x₁, x₂)]	=	max(x₁ + 2, x₂ + 4, 0)
[U12(x₁, x₂)]	=	max(x₁ + 0, x₂ + 1, 0)
[a__U41(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[x(x₁, x₂)]	=	max(x₁ + 2, x₂ + 4, 0)
[a__U12^#(x₁, x₂)]	=	max(0)
[a__U21^#(x₁, x₂)]	=	max(0)
[a__U61^#(x₁)]	=	0
[a__plus^#(x₁, x₂)]	=	max(x₁ + 0, x₂ + 1, 0)
[mark^#(x₁)]	=	x₁ + 0
[0]	=	2
[a__and^#(x₁, x₂)]	=	max(x₂ + 0, 0)
[a__U21(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[a__U32(x₁, x₂)]	=	max(x₁ + 1, x₂ + 2, 0)
[mark(x₁)]	=	x₁ + 0
[a__U11(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 1, 0)
[U32(x₁, x₂)]	=	max(x₁ + 1, x₂ + 2, 0)
[U33(x₁)]	=	x₁ + 2
[a__U12(x₁, x₂)]	=	max(x₁ + 0, x₂ + 1, 0)
[isNat(x₁)]	=	x₁ + 0
[plus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 1, 0)
[U61(x₁)]	=	2
[a__U22^#(x₁)]	=	0
[a__U13(x₁)]	=	x₁ + 1
[U31(x₁, x₂, x₃)]	=	max(x₁ + 4, x₂ + 2, x₃ + 3, 0)
[a__U71(x₁, x₂, x₃)]	=	max(x₂ + 4, x₃ + 2, 0)
[a__U61(x₁)]	=	2
[a__U41^#(x₁, x₂)]	=	max(x₂ + 0, 0)
[tt]	=	0
[a__isNat(x₁)]	=	x₁ + 0
[U13(x₁)]	=	x₁ + 1
[a__isNatKind(x₁)]	=	0
[U22(x₁)]	=	x₁ + 0
[U51(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 1, x₃ + 0, 0)
[a__and(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[U41(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[a__U32^#(x₁, x₂)]	=	max(0)

together with the usable rules

a__isNatKind(0)	→	tt	(18)
a__U21(X1,X2)	→	U21(X1,X2)	(50)
a__U21(tt,V1)	→	a__U22(a__isNat(V1))	(4)
a__isNat(plus(V1,V2))	→	a__U11(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2)	(15)
a__U33(tt)	→	tt	(8)
a__U33(X)	→	U33(X)	(54)
a__U11(tt,V1,V2)	→	a__U12(a__isNat(V1),V2)	(1)
a__U13(tt)	→	tt	(3)
a__isNat(s(V1))	→	a__U21(a__isNatKind(V1),V1)	(16)
a__isNatKind(x(V1,V2))	→	a__and(a__isNatKind(V1),isNatKind(V2))	(21)
mark(U51(X1,X2,X3))	→	a__U51(mark(X1),X2,X3)	(36)
mark(U11(X1,X2,X3))	→	a__U11(mark(X1),X2,X3)	(26)
a__isNatKind(plus(V1,V2))	→	a__and(a__isNatKind(V1),isNatKind(V2))	(19)
mark(U31(X1,X2,X3))	→	a__U31(mark(X1),X2,X3)	(32)
a__isNat(x(V1,V2))	→	a__U31(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2)	(17)
a__x(X1,X2)	→	x(X1,X2)	(60)
mark(U12(X1,X2))	→	a__U12(mark(X1),X2)	(27)
mark(U33(X))	→	a__U33(mark(X))	(34)
a__plus(N,0)	→	a__U41(a__and(a__isNat(N),isNatKind(N)),N)	(22)
mark(isNat(X))	→	a__isNat(X)	(28)
mark(s(X))	→	s(mark(X))	(44)
a__U22(tt)	→	tt	(5)
mark(U32(X1,X2))	→	a__U32(mark(X1),X2)	(33)
a__U51(tt,M,N)	→	s(a__plus(mark(N),mark(M)))	(10)
mark(U71(X1,X2,X3))	→	a__U71(mark(X1),X2,X3)	(39)
a__U32(tt,V2)	→	a__U33(a__isNat(V2))	(7)
a__isNatKind(s(V1))	→	a__isNatKind(V1)	(20)
a__x(N,s(M))	→	a__U71(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N)	(25)
a__U13(X)	→	U13(X)	(49)
a__U31(X1,X2,X3)	→	U31(X1,X2,X3)	(52)
mark(U21(X1,X2))	→	a__U21(mark(X1),X2)	(30)
a__isNatKind(X)	→	isNatKind(X)	(62)
a__isNat(0)	→	tt	(14)
a__U51(X1,X2,X3)	→	U51(X1,X2,X3)	(56)
mark(U22(X))	→	a__U22(mark(X))	(31)
a__U71(tt,M,N)	→	a__plus(a__x(mark(N),mark(M)),mark(N))	(12)
mark(0)	→	0	(45)
a__plus(N,s(M))	→	a__U51(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N)	(23)
a__x(N,0)	→	a__U61(a__and(a__isNat(N),isNatKind(N)))	(24)
a__plus(X1,X2)	→	plus(X1,X2)	(57)
a__U61(tt)	→	0	(11)
a__U41(tt,N)	→	mark(N)	(9)
a__and(tt,X)	→	mark(X)	(13)
a__U22(X)	→	U22(X)	(51)
mark(x(X1,X2))	→	a__x(mark(X1),mark(X2))	(40)
a__U41(X1,X2)	→	U41(X1,X2)	(55)
a__U71(X1,X2,X3)	→	U71(X1,X2,X3)	(59)
a__U31(tt,V1,V2)	→	a__U32(a__isNat(V1),V2)	(6)
mark(U61(X))	→	a__U61(mark(X))	(38)
a__and(X1,X2)	→	and(X1,X2)	(61)
a__U61(X)	→	U61(X)	(58)
a__isNat(X)	→	isNat(X)	(48)
a__U32(X1,X2)	→	U32(X1,X2)	(53)
a__U12(X1,X2)	→	U12(X1,X2)	(47)
mark(plus(X1,X2))	→	a__plus(mark(X1),mark(X2))	(37)
mark(and(X1,X2))	→	a__and(mark(X1),X2)	(41)
mark(isNatKind(X))	→	a__isNatKind(X)	(42)
a__U11(X1,X2,X3)	→	U11(X1,X2,X3)	(46)
mark(U41(X1,X2))	→	a__U41(mark(X1),X2)	(35)
mark(U13(X))	→	a__U13(mark(X))	(29)
mark(tt)	→	tt	(43)
a__U12(tt,V2)	→	a__U13(a__isNat(V2))	(2)

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

a__plus^#(N,0)	→	a__and^#(a__isNat(N),isNatKind(N))	(84)
a__U51^#(tt,M,N)	→	mark^#(M)	(109)
a__plus^#(N,s(M))	→	a__isNat^#(M)	(120)
a__plus^#(N,s(M))	→	a__and^#(a__isNat(M),isNatKind(M))	(123)

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

a__U21^#(tt,V1)	→	a__isNat^#(V1)	(104)
a__isNat^#(plus(V1,V2))	→	a__isNatKind^#(V1)	(141)
a__isNat^#(plus(V1,V2))	→	a__and^#(a__isNatKind(V1),isNatKind(V2))	(102)
a__isNat^#(plus(V1,V2))	→	a__U11^#(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2)	(97)
a__U11^#(tt,V1,V2)	→	a__isNat^#(V1)	(135)
a__U11^#(tt,V1,V2)	→	a__U12^#(a__isNat(V1),V2)	(92)
a__isNat^#(s(V1))	→	a__isNatKind^#(V1)	(77)
a__isNat^#(s(V1))	→	a__U21^#(a__isNatKind(V1),V1)	(78)
a__isNatKind^#(x(V1,V2))	→	a__isNatKind^#(V1)	(72)
a__isNatKind^#(x(V1,V2))	→	a__and^#(a__isNatKind(V1),isNatKind(V2))	(116)
mark^#(U51(X1,X2,X3))	→	mark^#(X1)	(75)
mark^#(U51(X1,X2,X3))	→	a__U51^#(mark(X1),X2,X3)	(94)
mark^#(U11(X1,X2,X3))	→	mark^#(X1)	(99)
a__isNatKind^#(plus(V1,V2))	→	a__isNatKind^#(V1)	(85)
a__isNatKind^#(plus(V1,V2))	→	a__and^#(a__isNatKind(V1),isNatKind(V2))	(67)
a__isNat^#(x(V1,V2))	→	a__isNatKind^#(V1)	(128)
a__isNat^#(x(V1,V2))	→	a__and^#(a__isNatKind(V1),isNatKind(V2))	(106)
a__isNat^#(x(V1,V2))	→	a__U31^#(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2)	(80)
mark^#(U12(X1,X2))	→	mark^#(X1)	(124)
a__plus^#(N,0)	→	a__U41^#(a__and(a__isNat(N),isNatKind(N)),N)	(137)
mark^#(isNat(X))	→	a__isNat^#(X)	(74)
mark^#(s(X))	→	mark^#(X)	(108)
a__U51^#(tt,M,N)	→	mark^#(N)	(76)
a__U51^#(tt,M,N)	→	a__plus^#(mark(N),mark(M))	(73)
mark^#(U71(X1,X2,X3))	→	a__U71^#(mark(X1),X2,X3)	(98)
a__U32^#(tt,V2)	→	a__isNat^#(V2)	(118)
a__isNatKind^#(s(V1))	→	a__isNatKind^#(V1)	(69)
a__x^#(N,s(M))	→	a__U71^#(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N)	(81)
mark^#(U21(X1,X2))	→	mark^#(X1)	(71)
mark^#(U21(X1,X2))	→	a__U21^#(mark(X1),X2)	(131)
mark^#(U22(X))	→	mark^#(X)	(66)
a__U71^#(tt,M,N)	→	a__x^#(mark(N),mark(M))	(107)
a__U71^#(tt,M,N)	→	a__plus^#(a__x(mark(N),mark(M)),mark(N))	(65)
a__plus^#(N,s(M))	→	a__and^#(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N)))	(129)
a__plus^#(N,s(M))	→	a__U51^#(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N)	(110)
a__U41^#(tt,N)	→	mark^#(N)	(132)
a__and^#(tt,X)	→	mark^#(X)	(111)
mark^#(x(X1,X2))	→	a__x^#(mark(X1),mark(X2))	(125)
a__U31^#(tt,V1,V2)	→	a__isNat^#(V1)	(133)
a__U31^#(tt,V1,V2)	→	a__U32^#(a__isNat(V1),V2)	(139)
mark^#(plus(X1,X2))	→	mark^#(X1)	(90)
mark^#(plus(X1,X2))	→	a__plus^#(mark(X1),mark(X2))	(114)
mark^#(and(X1,X2))	→	mark^#(X1)	(89)
mark^#(and(X1,X2))	→	a__and^#(mark(X1),X2)	(138)
mark^#(isNatKind(X))	→	a__isNatKind^#(X)	(112)
mark^#(U41(X1,X2))	→	mark^#(X1)	(82)
mark^#(U41(X1,X2))	→	a__U41^#(mark(X1),X2)	(117)
a__U12^#(tt,V2)	→	a__isNat^#(V2)	(63)

1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a__isNatKind^#(x₁)]	=	1
[isNatKind(x₁)]	=	0
[a__plus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 2, 0)
[U21(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[a__U71^#(x₁, x₂, x₃)]	=	max(x₂ + 6, x₃ + 4, 0)
[U11(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 1, 0)
[s(x₁)]	=	x₁ + 0
[a__U31^#(x₁, x₂, x₃)]	=	max(x₂ + 3, x₃ + 3, 0)
[a__U33^#(x₁)]	=	0
[a__U33(x₁)]	=	x₁ + 3
[a__isNat^#(x₁)]	=	x₁ + 1
[U71(x₁, x₂, x₃)]	=	max(x₂ + 5, x₃ + 3, 0)
[and(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[a__U13^#(x₁)]	=	0
[a__U51^#(x₁, x₂, x₃)]	=	max(x₂ + 3, x₃ + 1, 0)
[a__x^#(x₁, x₂)]	=	max(x₁ + 4, x₂ + 6, 0)
[a__U22(x₁)]	=	x₁ + 0
[a__U11^#(x₁, x₂, x₃)]	=	max(x₂ + 1, x₃ + 2, 0)
[a__U31(x₁, x₂, x₃)]	=	max(x₁ + 5, x₂ + 3, x₃ + 4, 0)
[a__U51(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 2, x₃ + 0, 0)
[a__x(x₁, x₂)]	=	max(x₁ + 3, x₂ + 5, 0)
[U12(x₁, x₂)]	=	max(x₁ + 0, x₂ + 1, 0)
[a__U41(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[x(x₁, x₂)]	=	max(x₁ + 3, x₂ + 5, 0)
[a__U12^#(x₁, x₂)]	=	max(x₂ + 2, 0)
[a__U21^#(x₁, x₂)]	=	max(x₂ + 1, 0)
[a__U61^#(x₁)]	=	0
[a__plus^#(x₁, x₂)]	=	max(x₁ + 1, x₂ + 3, 0)
[mark^#(x₁)]	=	x₁ + 1
[0]	=	1
[a__and^#(x₁, x₂)]	=	max(x₂ + 1, 0)
[a__U21(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[a__U32(x₁, x₂)]	=	max(x₁ + 2, x₂ + 3, 0)
[mark(x₁)]	=	x₁ + 0
[a__U11(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 1, 0)
[U32(x₁, x₂)]	=	max(x₁ + 2, x₂ + 3, 0)
[U33(x₁)]	=	x₁ + 3
[a__U12(x₁, x₂)]	=	max(x₁ + 0, x₂ + 1, 0)
[isNat(x₁)]	=	x₁ + 0
[plus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 2, 0)
[U61(x₁)]	=	3
[a__U22^#(x₁)]	=	0
[a__U13(x₁)]	=	x₁ + 1
[U31(x₁, x₂, x₃)]	=	max(x₁ + 5, x₂ + 3, x₃ + 4, 0)
[a__U71(x₁, x₂, x₃)]	=	max(x₂ + 5, x₃ + 3, 0)
[a__U61(x₁)]	=	3
[a__U41^#(x₁, x₂)]	=	max(x₂ + 1, 0)
[tt]	=	0
[a__isNat(x₁)]	=	x₁ + 0
[U13(x₁)]	=	x₁ + 1
[a__isNatKind(x₁)]	=	0
[U22(x₁)]	=	x₁ + 0
[U51(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 2, x₃ + 0, 0)
[a__and(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[U41(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[a__U32^#(x₁, x₂)]	=	max(x₂ + 2, 0)

together with the usable rules

a__isNatKind(0)	→	tt	(18)
a__U21(X1,X2)	→	U21(X1,X2)	(50)
a__U21(tt,V1)	→	a__U22(a__isNat(V1))	(4)
a__isNat(plus(V1,V2))	→	a__U11(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2)	(15)
a__U33(tt)	→	tt	(8)
a__U33(X)	→	U33(X)	(54)
a__U11(tt,V1,V2)	→	a__U12(a__isNat(V1),V2)	(1)
a__U13(tt)	→	tt	(3)
a__isNat(s(V1))	→	a__U21(a__isNatKind(V1),V1)	(16)
a__isNatKind(x(V1,V2))	→	a__and(a__isNatKind(V1),isNatKind(V2))	(21)
mark(U51(X1,X2,X3))	→	a__U51(mark(X1),X2,X3)	(36)
mark(U11(X1,X2,X3))	→	a__U11(mark(X1),X2,X3)	(26)
a__isNatKind(plus(V1,V2))	→	a__and(a__isNatKind(V1),isNatKind(V2))	(19)
mark(U31(X1,X2,X3))	→	a__U31(mark(X1),X2,X3)	(32)
a__isNat(x(V1,V2))	→	a__U31(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2)	(17)
a__x(X1,X2)	→	x(X1,X2)	(60)
mark(U12(X1,X2))	→	a__U12(mark(X1),X2)	(27)
mark(U33(X))	→	a__U33(mark(X))	(34)
a__plus(N,0)	→	a__U41(a__and(a__isNat(N),isNatKind(N)),N)	(22)
mark(isNat(X))	→	a__isNat(X)	(28)
mark(s(X))	→	s(mark(X))	(44)
a__U22(tt)	→	tt	(5)
mark(U32(X1,X2))	→	a__U32(mark(X1),X2)	(33)
a__U51(tt,M,N)	→	s(a__plus(mark(N),mark(M)))	(10)
mark(U71(X1,X2,X3))	→	a__U71(mark(X1),X2,X3)	(39)
a__U32(tt,V2)	→	a__U33(a__isNat(V2))	(7)
a__isNatKind(s(V1))	→	a__isNatKind(V1)	(20)
a__x(N,s(M))	→	a__U71(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N)	(25)
a__U13(X)	→	U13(X)	(49)
a__U31(X1,X2,X3)	→	U31(X1,X2,X3)	(52)
mark(U21(X1,X2))	→	a__U21(mark(X1),X2)	(30)
a__isNatKind(X)	→	isNatKind(X)	(62)
a__isNat(0)	→	tt	(14)
a__U51(X1,X2,X3)	→	U51(X1,X2,X3)	(56)
mark(U22(X))	→	a__U22(mark(X))	(31)
a__U71(tt,M,N)	→	a__plus(a__x(mark(N),mark(M)),mark(N))	(12)
mark(0)	→	0	(45)
a__plus(N,s(M))	→	a__U51(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N)	(23)
a__x(N,0)	→	a__U61(a__and(a__isNat(N),isNatKind(N)))	(24)
a__plus(X1,X2)	→	plus(X1,X2)	(57)
a__U61(tt)	→	0	(11)
a__U41(tt,N)	→	mark(N)	(9)
a__and(tt,X)	→	mark(X)	(13)
a__U22(X)	→	U22(X)	(51)
mark(x(X1,X2))	→	a__x(mark(X1),mark(X2))	(40)
a__U41(X1,X2)	→	U41(X1,X2)	(55)
a__U71(X1,X2,X3)	→	U71(X1,X2,X3)	(59)
a__U31(tt,V1,V2)	→	a__U32(a__isNat(V1),V2)	(6)
mark(U61(X))	→	a__U61(mark(X))	(38)
a__and(X1,X2)	→	and(X1,X2)	(61)
a__U61(X)	→	U61(X)	(58)
a__isNat(X)	→	isNat(X)	(48)
a__U32(X1,X2)	→	U32(X1,X2)	(53)
a__U12(X1,X2)	→	U12(X1,X2)	(47)
mark(plus(X1,X2))	→	a__plus(mark(X1),mark(X2))	(37)
mark(and(X1,X2))	→	a__and(mark(X1),X2)	(41)
mark(isNatKind(X))	→	a__isNatKind(X)	(42)
a__U11(X1,X2,X3)	→	U11(X1,X2,X3)	(46)
mark(U41(X1,X2))	→	a__U41(mark(X1),X2)	(35)
mark(U13(X))	→	a__U13(mark(X))	(29)
mark(tt)	→	tt	(43)
a__U12(tt,V2)	→	a__U13(a__isNat(V2))	(2)

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

a__isNat^#(plus(V1,V2))	→	a__isNatKind^#(V1)	(141)
a__isNat^#(plus(V1,V2))	→	a__and^#(a__isNatKind(V1),isNatKind(V2))	(102)
a__isNat^#(x(V1,V2))	→	a__isNatKind^#(V1)	(128)
a__isNat^#(x(V1,V2))	→	a__and^#(a__isNatKind(V1),isNatKind(V2))	(106)
a__isNat^#(x(V1,V2))	→	a__U31^#(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2)	(80)
a__U32^#(tt,V2)	→	a__isNat^#(V2)	(118)
a__U31^#(tt,V1,V2)	→	a__isNat^#(V1)	(133)
a__U31^#(tt,V1,V2)	→	a__U32^#(a__isNat(V1),V2)	(139)
a__U12^#(tt,V2)	→	a__isNat^#(V2)	(63)

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

a__U21^#(tt,V1)	→	a__isNat^#(V1)	(104)
a__isNat^#(plus(V1,V2))	→	a__U11^#(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2)	(97)
a__U11^#(tt,V1,V2)	→	a__isNat^#(V1)	(135)
a__isNat^#(s(V1))	→	a__isNatKind^#(V1)	(77)
a__isNat^#(s(V1))	→	a__U21^#(a__isNatKind(V1),V1)	(78)
a__isNatKind^#(x(V1,V2))	→	a__isNatKind^#(V1)	(72)
a__isNatKind^#(x(V1,V2))	→	a__and^#(a__isNatKind(V1),isNatKind(V2))	(116)
mark^#(U51(X1,X2,X3))	→	mark^#(X1)	(75)
mark^#(U51(X1,X2,X3))	→	a__U51^#(mark(X1),X2,X3)	(94)
mark^#(U11(X1,X2,X3))	→	mark^#(X1)	(99)
a__isNatKind^#(plus(V1,V2))	→	a__isNatKind^#(V1)	(85)
a__isNatKind^#(plus(V1,V2))	→	a__and^#(a__isNatKind(V1),isNatKind(V2))	(67)
mark^#(U12(X1,X2))	→	mark^#(X1)	(124)
a__plus^#(N,0)	→	a__U41^#(a__and(a__isNat(N),isNatKind(N)),N)	(137)
mark^#(isNat(X))	→	a__isNat^#(X)	(74)
mark^#(s(X))	→	mark^#(X)	(108)
a__U51^#(tt,M,N)	→	mark^#(N)	(76)
a__U51^#(tt,M,N)	→	a__plus^#(mark(N),mark(M))	(73)
mark^#(U71(X1,X2,X3))	→	a__U71^#(mark(X1),X2,X3)	(98)
a__isNatKind^#(s(V1))	→	a__isNatKind^#(V1)	(69)
a__x^#(N,s(M))	→	a__U71^#(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N)	(81)
mark^#(U21(X1,X2))	→	mark^#(X1)	(71)
mark^#(U21(X1,X2))	→	a__U21^#(mark(X1),X2)	(131)
mark^#(U22(X))	→	mark^#(X)	(66)
a__U71^#(tt,M,N)	→	a__x^#(mark(N),mark(M))	(107)
a__U71^#(tt,M,N)	→	a__plus^#(a__x(mark(N),mark(M)),mark(N))	(65)
a__plus^#(N,s(M))	→	a__and^#(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N)))	(129)
a__plus^#(N,s(M))	→	a__U51^#(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N)	(110)
a__U41^#(tt,N)	→	mark^#(N)	(132)
a__and^#(tt,X)	→	mark^#(X)	(111)
mark^#(x(X1,X2))	→	a__x^#(mark(X1),mark(X2))	(125)
mark^#(plus(X1,X2))	→	mark^#(X1)	(90)
mark^#(plus(X1,X2))	→	a__plus^#(mark(X1),mark(X2))	(114)
mark^#(and(X1,X2))	→	mark^#(X1)	(89)
mark^#(and(X1,X2))	→	a__and^#(mark(X1),X2)	(138)
mark^#(isNatKind(X))	→	a__isNatKind^#(X)	(112)
mark^#(U41(X1,X2))	→	mark^#(X1)	(82)
mark^#(U41(X1,X2))	→	a__U41^#(mark(X1),X2)	(117)

1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a__isNatKind^#(x₁)]	=	32294
[isNatKind(x₁)]	=	1
[a__plus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 8, 0)
[U21(x₁, x₂)]	=	max(x₁ + 2, 0)
[a__U71^#(x₁, x₂, x₃)]	=	max(x₁ + 32297, x₃ + 51803, 0)
[U11(x₁, x₂, x₃)]	=	max(x₁ + 2, 0)
[s(x₁)]	=	x₁ + 0
[a__U31^#(x₁, x₂, x₃)]	=	max(0)
[a__U33^#(x₁)]	=	0
[a__U33(x₁)]	=	1
[a__isNat^#(x₁)]	=	32295
[U71(x₁, x₂, x₃)]	=	max(x₁ + 5, x₃ + 19510, 0)
[and(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[a__U13^#(x₁)]	=	0
[a__U51^#(x₁, x₂, x₃)]	=	max(x₁ + 32294, x₂ + 32297, x₃ + 32293, 0)
[a__x^#(x₁, x₂)]	=	max(x₁ + 51803, 0)
[a__U22(x₁)]	=	x₁ + 0
[a__U11^#(x₁, x₂, x₃)]	=	max(x₁ + 32294, 0)
[a__U31(x₁, x₂, x₃)]	=	max(x₁ + 2, 0)
[a__U51(x₁, x₂, x₃)]	=	max(x₁ + 1, x₂ + 8, x₃ + 0, 0)
[a__x(x₁, x₂)]	=	max(x₁ + 19510, 0)
[U12(x₁, x₂)]	=	max(x₁ + 0, 0)
[a__U41(x₁, x₂)]	=	max(x₁ + 5108, x₂ + 0, 0)
[x(x₁, x₂)]	=	max(x₁ + 19510, 0)
[a__U12^#(x₁, x₂)]	=	max(0)
[a__U21^#(x₁, x₂)]	=	max(x₁ + 32294, 0)
[a__U61^#(x₁)]	=	0
[a__plus^#(x₁, x₂)]	=	max(x₁ + 32293, x₂ + 32297, 0)
[mark^#(x₁)]	=	x₁ + 32293
[0]	=	12579
[a__and^#(x₁, x₂)]	=	max(x₂ + 32293, 0)
[a__U21(x₁, x₂)]	=	max(x₁ + 2, 0)
[a__U32(x₁, x₂)]	=	max(x₁ + 0, 0)
[mark(x₁)]	=	x₁ + 0
[a__U11(x₁, x₂, x₃)]	=	max(x₁ + 2, 0)
[U32(x₁, x₂)]	=	max(x₁ + 0, 0)
[U33(x₁)]	=	1
[a__U12(x₁, x₂)]	=	max(x₁ + 0, 0)
[isNat(x₁)]	=	3
[plus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 8, 0)
[U61(x₁)]	=	12579
[a__U22^#(x₁)]	=	0
[a__U13(x₁)]	=	1
[U31(x₁, x₂, x₃)]	=	max(x₁ + 2, 0)
[a__U71(x₁, x₂, x₃)]	=	max(x₁ + 5, x₃ + 19510, 0)
[a__U61(x₁)]	=	12579
[a__U41^#(x₁, x₂)]	=	max(x₂ + 32293, 0)
[tt]	=	1
[a__isNat(x₁)]	=	3
[U13(x₁)]	=	1
[a__isNatKind(x₁)]	=	1
[U22(x₁)]	=	x₁ + 0
[U51(x₁, x₂, x₃)]	=	max(x₁ + 1, x₂ + 8, x₃ + 0, 0)
[a__and(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[U41(x₁, x₂)]	=	max(x₁ + 5108, x₂ + 0, 0)
[a__U32^#(x₁, x₂)]	=	max(0)

together with the usable rules

a__isNatKind(0)	→	tt	(18)
a__U21(X1,X2)	→	U21(X1,X2)	(50)
a__U21(tt,V1)	→	a__U22(a__isNat(V1))	(4)
a__isNat(plus(V1,V2))	→	a__U11(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2)	(15)
a__U33(tt)	→	tt	(8)
a__U33(X)	→	U33(X)	(54)
a__U11(tt,V1,V2)	→	a__U12(a__isNat(V1),V2)	(1)
a__U13(tt)	→	tt	(3)
a__isNat(s(V1))	→	a__U21(a__isNatKind(V1),V1)	(16)
a__isNatKind(x(V1,V2))	→	a__and(a__isNatKind(V1),isNatKind(V2))	(21)
mark(U51(X1,X2,X3))	→	a__U51(mark(X1),X2,X3)	(36)
mark(U11(X1,X2,X3))	→	a__U11(mark(X1),X2,X3)	(26)
a__isNatKind(plus(V1,V2))	→	a__and(a__isNatKind(V1),isNatKind(V2))	(19)
mark(U31(X1,X2,X3))	→	a__U31(mark(X1),X2,X3)	(32)
a__isNat(x(V1,V2))	→	a__U31(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2)	(17)
a__x(X1,X2)	→	x(X1,X2)	(60)
mark(U12(X1,X2))	→	a__U12(mark(X1),X2)	(27)
mark(U33(X))	→	a__U33(mark(X))	(34)
a__plus(N,0)	→	a__U41(a__and(a__isNat(N),isNatKind(N)),N)	(22)
mark(isNat(X))	→	a__isNat(X)	(28)
mark(s(X))	→	s(mark(X))	(44)
a__U22(tt)	→	tt	(5)
mark(U32(X1,X2))	→	a__U32(mark(X1),X2)	(33)
a__U51(tt,M,N)	→	s(a__plus(mark(N),mark(M)))	(10)
mark(U71(X1,X2,X3))	→	a__U71(mark(X1),X2,X3)	(39)
a__U32(tt,V2)	→	a__U33(a__isNat(V2))	(7)
a__isNatKind(s(V1))	→	a__isNatKind(V1)	(20)
a__x(N,s(M))	→	a__U71(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N)	(25)
a__U13(X)	→	U13(X)	(49)
a__U31(X1,X2,X3)	→	U31(X1,X2,X3)	(52)
mark(U21(X1,X2))	→	a__U21(mark(X1),X2)	(30)
a__isNatKind(X)	→	isNatKind(X)	(62)
a__isNat(0)	→	tt	(14)
a__U51(X1,X2,X3)	→	U51(X1,X2,X3)	(56)
mark(U22(X))	→	a__U22(mark(X))	(31)
a__U71(tt,M,N)	→	a__plus(a__x(mark(N),mark(M)),mark(N))	(12)
mark(0)	→	0	(45)
a__plus(N,s(M))	→	a__U51(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N)	(23)
a__x(N,0)	→	a__U61(a__and(a__isNat(N),isNatKind(N)))	(24)
a__plus(X1,X2)	→	plus(X1,X2)	(57)
a__U61(tt)	→	0	(11)
a__U41(tt,N)	→	mark(N)	(9)
a__and(tt,X)	→	mark(X)	(13)
a__U22(X)	→	U22(X)	(51)
mark(x(X1,X2))	→	a__x(mark(X1),mark(X2))	(40)
a__U41(X1,X2)	→	U41(X1,X2)	(55)
a__U71(X1,X2,X3)	→	U71(X1,X2,X3)	(59)
a__U31(tt,V1,V2)	→	a__U32(a__isNat(V1),V2)	(6)
mark(U61(X))	→	a__U61(mark(X))	(38)
a__and(X1,X2)	→	and(X1,X2)	(61)
a__U61(X)	→	U61(X)	(58)
a__isNat(X)	→	isNat(X)	(48)
a__U32(X1,X2)	→	U32(X1,X2)	(53)
a__U12(X1,X2)	→	U12(X1,X2)	(47)
mark(plus(X1,X2))	→	a__plus(mark(X1),mark(X2))	(37)
mark(and(X1,X2))	→	a__and(mark(X1),X2)	(41)
mark(isNatKind(X))	→	a__isNatKind(X)	(42)
a__U11(X1,X2,X3)	→	U11(X1,X2,X3)	(46)
mark(U41(X1,X2))	→	a__U41(mark(X1),X2)	(35)
mark(U13(X))	→	a__U13(mark(X))	(29)
mark(tt)	→	tt	(43)
a__U12(tt,V2)	→	a__U13(a__isNat(V2))	(2)

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

a__isNat^#(s(V1))	→	a__isNatKind^#(V1)	(77)
mark^#(U51(X1,X2,X3))	→	mark^#(X1)	(75)
mark^#(U11(X1,X2,X3))	→	mark^#(X1)	(99)
mark^#(isNat(X))	→	a__isNat^#(X)	(74)
mark^#(U21(X1,X2))	→	mark^#(X1)	(71)
mark^#(U21(X1,X2))	→	a__U21^#(mark(X1),X2)	(131)
a__plus^#(N,s(M))	→	a__and^#(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N)))	(129)
mark^#(U41(X1,X2))	→	mark^#(X1)	(82)

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

a__U21^#(tt,V1)	→	a__isNat^#(V1)	(104)
a__isNat^#(plus(V1,V2))	→	a__U11^#(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2)	(97)
a__U11^#(tt,V1,V2)	→	a__isNat^#(V1)	(135)
a__isNat^#(s(V1))	→	a__U21^#(a__isNatKind(V1),V1)	(78)

1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a__isNatKind^#(x₁)]	=	0
[isNatKind(x₁)]	=	4448
[a__plus(x₁, x₂)]	=	4449
[U21(x₁, x₂)]	=	4449
[a__U71^#(x₁, x₂, x₃)]	=	0
[U11(x₁, x₂, x₃)]	=	4449
[s(x₁)]	=	x₁ + 2
[a__U31^#(x₁, x₂, x₃)]	=	0
[a__U33^#(x₁)]	=	0
[a__U33(x₁)]	=	4450
[a__isNat^#(x₁)]	=	x₁ + 0
[U71(x₁, x₂, x₃)]	=	4449
[and(x₁, x₂)]	=	2
[a__U13^#(x₁)]	=	0
[a__U51^#(x₁, x₂, x₃)]	=	0
[a__x^#(x₁, x₂)]	=	0
[a__U22(x₁)]	=	4449
[a__U11^#(x₁, x₂, x₃)]	=	x₂ + 1
[a__U31(x₁, x₂, x₃)]	=	4448
[a__U51(x₁, x₂, x₃)]	=	4450
[a__x(x₁, x₂)]	=	4447
[U12(x₁, x₂)]	=	4450
[a__U41(x₁, x₂)]	=	4450
[x(x₁, x₂)]	=	x₁ + 4448
[a__U12^#(x₁, x₂)]	=	0
[a__U21^#(x₁, x₂)]	=	x₂ + 1
[a__U61^#(x₁)]	=	0
[a__plus^#(x₁, x₂)]	=	0
[mark^#(x₁)]	=	0
[0]	=	4449
[a__and^#(x₁, x₂)]	=	0
[a__U21(x₁, x₂)]	=	x₂ + 4448
[a__U32(x₁, x₂)]	=	x₂ + 4449
[mark(x₁)]	=	4446
[a__U11(x₁, x₂, x₃)]	=	x₂ + x₃ + 4448
[U32(x₁, x₂)]	=	x₁ + 4450
[U33(x₁)]	=	x₁ + 4451
[a__U12(x₁, x₂)]	=	4449
[isNat(x₁)]	=	4448
[plus(x₁, x₂)]	=	x₁ + 4450
[U61(x₁)]	=	x₁ + 4449
[a__U22^#(x₁)]	=	0
[a__U13(x₁)]	=	4450
[U31(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 4449
[a__U71(x₁, x₂, x₃)]	=	x₂ + 4448
[a__U61(x₁)]	=	4448
[a__U41^#(x₁, x₂)]	=	0
[tt]	=	4451
[a__isNat(x₁)]	=	4447
[U13(x₁)]	=	x₁ + 4451
[a__isNatKind(x₁)]	=	4447
[U22(x₁)]	=	4450
[U51(x₁, x₂, x₃)]	=	4451
[a__and(x₁, x₂)]	=	1
[U41(x₁, x₂)]	=	4451
[a__U32^#(x₁, x₂)]	=	0

having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the pairs

a__U21^#(tt,V1)	→	a__isNat^#(V1)	(104)
a__isNat^#(plus(V1,V2))	→	a__U11^#(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2)	(97)
a__U11^#(tt,V1,V2)	→	a__isNat^#(V1)	(135)
a__isNat^#(s(V1))	→	a__U21^#(a__isNatKind(V1),V1)	(78)

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

a__isNatKind^#(x(V1,V2))	→	a__isNatKind^#(V1)	(72)
a__isNatKind^#(x(V1,V2))	→	a__and^#(a__isNatKind(V1),isNatKind(V2))	(116)
mark^#(U51(X1,X2,X3))	→	a__U51^#(mark(X1),X2,X3)	(94)
a__isNatKind^#(plus(V1,V2))	→	a__isNatKind^#(V1)	(85)
a__isNatKind^#(plus(V1,V2))	→	a__and^#(a__isNatKind(V1),isNatKind(V2))	(67)
mark^#(U12(X1,X2))	→	mark^#(X1)	(124)
a__plus^#(N,0)	→	a__U41^#(a__and(a__isNat(N),isNatKind(N)),N)	(137)
mark^#(s(X))	→	mark^#(X)	(108)
a__U51^#(tt,M,N)	→	mark^#(N)	(76)
a__U51^#(tt,M,N)	→	a__plus^#(mark(N),mark(M))	(73)
mark^#(U71(X1,X2,X3))	→	a__U71^#(mark(X1),X2,X3)	(98)
a__isNatKind^#(s(V1))	→	a__isNatKind^#(V1)	(69)
a__x^#(N,s(M))	→	a__U71^#(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N)	(81)
mark^#(U22(X))	→	mark^#(X)	(66)
a__U71^#(tt,M,N)	→	a__x^#(mark(N),mark(M))	(107)
a__U71^#(tt,M,N)	→	a__plus^#(a__x(mark(N),mark(M)),mark(N))	(65)
a__plus^#(N,s(M))	→	a__U51^#(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N)	(110)
a__U41^#(tt,N)	→	mark^#(N)	(132)
a__and^#(tt,X)	→	mark^#(X)	(111)
mark^#(x(X1,X2))	→	a__x^#(mark(X1),mark(X2))	(125)
mark^#(plus(X1,X2))	→	mark^#(X1)	(90)
mark^#(plus(X1,X2))	→	a__plus^#(mark(X1),mark(X2))	(114)
mark^#(and(X1,X2))	→	mark^#(X1)	(89)
mark^#(and(X1,X2))	→	a__and^#(mark(X1),X2)	(138)
mark^#(isNatKind(X))	→	a__isNatKind^#(X)	(112)
mark^#(U41(X1,X2))	→	a__U41^#(mark(X1),X2)	(117)

1.1.1.1.1.1.1.1.1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a__isNatKind^#(x₁)]	=	x₁ + 1
[isNatKind(x₁)]	=	x₁ + 2
[a__plus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 2, 0)
[U21(x₁, x₂)]	=	max(x₁ + 1, x₂ + 4, 0)
[a__U71^#(x₁, x₂, x₃)]	=	max(x₂ + 4, x₃ + 2, 0)
[U11(x₁, x₂, x₃)]	=	max(x₁ + 1, x₂ + 4, x₃ + 3, 0)
[s(x₁)]	=	x₁ + 0
[a__U31^#(x₁, x₂, x₃)]	=	max(0)
[a__U33^#(x₁)]	=	0
[a__U33(x₁)]	=	x₁ + 1
[a__isNat^#(x₁)]	=	32295
[U71(x₁, x₂, x₃)]	=	max(x₂ + 4, x₃ + 2, 0)
[and(x₁, x₂)]	=	max(x₁ + 0, x₂ + 2, 0)
[a__U13^#(x₁)]	=	0
[a__U51^#(x₁, x₂, x₃)]	=	max(x₃ + 0, 0)
[a__x^#(x₁, x₂)]	=	max(x₁ + 2, x₂ + 4, 0)
[a__U22(x₁)]	=	x₁ + 0
[a__U11^#(x₁, x₂, x₃)]	=	max(0)
[a__U31(x₁, x₂, x₃)]	=	max(x₁ + 4, x₃ + 8, 0)
[a__U51(x₁, x₂, x₃)]	=	max(x₂ + 2, x₃ + 0, 0)
[a__x(x₁, x₂)]	=	max(x₁ + 2, x₂ + 4, 0)
[U12(x₁, x₂)]	=	max(x₁ + 0, x₂ + 1, 0)
[a__U41(x₁, x₂)]	=	max(x₂ + 0, 0)
[x(x₁, x₂)]	=	max(x₁ + 2, x₂ + 4, 0)
[a__U12^#(x₁, x₂)]	=	max(0)
[a__U21^#(x₁, x₂)]	=	max(0)
[a__U61^#(x₁)]	=	0
[a__plus^#(x₁, x₂)]	=	max(x₁ + 0, 0)
[mark^#(x₁)]	=	x₁ + 0
[0]	=	1
[a__and^#(x₁, x₂)]	=	max(x₂ + 0, 0)
[a__U21(x₁, x₂)]	=	max(x₁ + 1, x₂ + 4, 0)
[a__U32(x₁, x₂)]	=	max(x₂ + 5, 0)
[mark(x₁)]	=	x₁ + 0
[a__U11(x₁, x₂, x₃)]	=	max(x₁ + 1, x₂ + 4, x₃ + 3, 0)
[U32(x₁, x₂)]	=	max(x₂ + 5, 0)
[U33(x₁)]	=	x₁ + 1
[a__U12(x₁, x₂)]	=	max(x₁ + 0, x₂ + 1, 0)
[isNat(x₁)]	=	x₁ + 4
[plus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 2, 0)
[U61(x₁)]	=	1
[a__U22^#(x₁)]	=	0
[a__U13(x₁)]	=	2
[U31(x₁, x₂, x₃)]	=	max(x₁ + 4, x₃ + 8, 0)
[a__U71(x₁, x₂, x₃)]	=	max(x₂ + 4, x₃ + 2, 0)
[a__U61(x₁)]	=	1
[a__U41^#(x₁, x₂)]	=	max(x₂ + 0, 0)
[tt]	=	2
[a__isNat(x₁)]	=	x₁ + 4
[U13(x₁)]	=	2
[a__isNatKind(x₁)]	=	x₁ + 2
[U22(x₁)]	=	x₁ + 0
[U51(x₁, x₂, x₃)]	=	max(x₂ + 2, x₃ + 0, 0)
[a__and(x₁, x₂)]	=	max(x₁ + 0, x₂ + 2, 0)
[U41(x₁, x₂)]	=	max(x₂ + 0, 0)
[a__U32^#(x₁, x₂)]	=	max(0)

together with the usable rules

a__isNatKind(0)	→	tt	(18)
a__U21(X1,X2)	→	U21(X1,X2)	(50)
a__U21(tt,V1)	→	a__U22(a__isNat(V1))	(4)
a__isNat(plus(V1,V2))	→	a__U11(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2)	(15)
a__U33(tt)	→	tt	(8)
a__U33(X)	→	U33(X)	(54)
a__U11(tt,V1,V2)	→	a__U12(a__isNat(V1),V2)	(1)
a__U13(tt)	→	tt	(3)
a__isNat(s(V1))	→	a__U21(a__isNatKind(V1),V1)	(16)
a__isNatKind(x(V1,V2))	→	a__and(a__isNatKind(V1),isNatKind(V2))	(21)
mark(U51(X1,X2,X3))	→	a__U51(mark(X1),X2,X3)	(36)
mark(U11(X1,X2,X3))	→	a__U11(mark(X1),X2,X3)	(26)
a__isNatKind(plus(V1,V2))	→	a__and(a__isNatKind(V1),isNatKind(V2))	(19)
mark(U31(X1,X2,X3))	→	a__U31(mark(X1),X2,X3)	(32)
a__isNat(x(V1,V2))	→	a__U31(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2)	(17)
a__x(X1,X2)	→	x(X1,X2)	(60)
mark(U12(X1,X2))	→	a__U12(mark(X1),X2)	(27)
mark(U33(X))	→	a__U33(mark(X))	(34)
a__plus(N,0)	→	a__U41(a__and(a__isNat(N),isNatKind(N)),N)	(22)
mark(isNat(X))	→	a__isNat(X)	(28)
mark(s(X))	→	s(mark(X))	(44)
a__U22(tt)	→	tt	(5)
mark(U32(X1,X2))	→	a__U32(mark(X1),X2)	(33)
a__U51(tt,M,N)	→	s(a__plus(mark(N),mark(M)))	(10)
mark(U71(X1,X2,X3))	→	a__U71(mark(X1),X2,X3)	(39)
a__U32(tt,V2)	→	a__U33(a__isNat(V2))	(7)
a__isNatKind(s(V1))	→	a__isNatKind(V1)	(20)
a__x(N,s(M))	→	a__U71(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N)	(25)
a__U13(X)	→	U13(X)	(49)
a__U31(X1,X2,X3)	→	U31(X1,X2,X3)	(52)
mark(U21(X1,X2))	→	a__U21(mark(X1),X2)	(30)
a__isNatKind(X)	→	isNatKind(X)	(62)
a__isNat(0)	→	tt	(14)
a__U51(X1,X2,X3)	→	U51(X1,X2,X3)	(56)
mark(U22(X))	→	a__U22(mark(X))	(31)
a__U71(tt,M,N)	→	a__plus(a__x(mark(N),mark(M)),mark(N))	(12)
mark(0)	→	0	(45)
a__plus(N,s(M))	→	a__U51(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N)	(23)
a__x(N,0)	→	a__U61(a__and(a__isNat(N),isNatKind(N)))	(24)
a__plus(X1,X2)	→	plus(X1,X2)	(57)
a__U61(tt)	→	0	(11)
a__U41(tt,N)	→	mark(N)	(9)
a__and(tt,X)	→	mark(X)	(13)
a__U22(X)	→	U22(X)	(51)
mark(x(X1,X2))	→	a__x(mark(X1),mark(X2))	(40)
a__U41(X1,X2)	→	U41(X1,X2)	(55)
a__U71(X1,X2,X3)	→	U71(X1,X2,X3)	(59)
a__U31(tt,V1,V2)	→	a__U32(a__isNat(V1),V2)	(6)
mark(U61(X))	→	a__U61(mark(X))	(38)
a__and(X1,X2)	→	and(X1,X2)	(61)
a__U61(X)	→	U61(X)	(58)
a__isNat(X)	→	isNat(X)	(48)
a__U32(X1,X2)	→	U32(X1,X2)	(53)
a__U12(X1,X2)	→	U12(X1,X2)	(47)
mark(plus(X1,X2))	→	a__plus(mark(X1),mark(X2))	(37)
mark(and(X1,X2))	→	a__and(mark(X1),X2)	(41)
mark(isNatKind(X))	→	a__isNatKind(X)	(42)
a__U11(X1,X2,X3)	→	U11(X1,X2,X3)	(46)
mark(U41(X1,X2))	→	a__U41(mark(X1),X2)	(35)
mark(U13(X))	→	a__U13(mark(X))	(29)
mark(tt)	→	tt	(43)
a__U12(tt,V2)	→	a__U13(a__isNat(V2))	(2)

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

a__isNatKind^#(x(V1,V2))	→	a__isNatKind^#(V1)	(72)
a__isNatKind^#(x(V1,V2))	→	a__and^#(a__isNatKind(V1),isNatKind(V2))	(116)
a__isNatKind^#(plus(V1,V2))	→	a__and^#(a__isNatKind(V1),isNatKind(V2))	(67)
mark^#(and(X1,X2))	→	a__and^#(mark(X1),X2)	(138)
mark^#(isNatKind(X))	→	a__isNatKind^#(X)	(112)

could be deleted.

1.1.1.1.1.1.1.1.1.1.2.1 Dependency Graph Processor

The dependency pairs are split into 2 components.

The 1^st component contains the pair

a__isNatKind^#(plus(V1,V2))	→	a__isNatKind^#(V1)	(85)
a__isNatKind^#(s(V1))	→	a__isNatKind^#(V1)	(69)

1.1.1.1.1.1.1.1.1.1.2.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a__isNatKind^#(x₁)]	=	x₁ + 2
[isNatKind(x₁)]	=	43587
[a__plus(x₁, x₂)]	=	43588
[U21(x₁, x₂)]	=	43588
[a__U71^#(x₁, x₂, x₃)]	=	2
[U11(x₁, x₂, x₃)]	=	43588
[s(x₁)]	=	x₁ + 2
[a__U31^#(x₁, x₂, x₃)]	=	0
[a__U33^#(x₁)]	=	0
[a__U33(x₁)]	=	43589
[a__isNat^#(x₁)]	=	0
[U71(x₁, x₂, x₃)]	=	43588
[and(x₁, x₂)]	=	x₁ + 43585
[a__U13^#(x₁)]	=	0
[a__U51^#(x₁, x₂, x₃)]	=	0
[a__x^#(x₁, x₂)]	=	0
[a__U22(x₁)]	=	43588
[a__U11^#(x₁, x₂, x₃)]	=	1
[a__U31(x₁, x₂, x₃)]	=	x₁ + 3
[a__U51(x₁, x₂, x₃)]	=	43589
[a__x(x₁, x₂)]	=	43586
[U12(x₁, x₂)]	=	43589
[a__U41(x₁, x₂)]	=	x₁ + 5
[x(x₁, x₂)]	=	43587
[a__U12^#(x₁, x₂)]	=	0
[a__U21^#(x₁, x₂)]	=	1
[a__U61^#(x₁)]	=	0
[a__plus^#(x₁, x₂)]	=	0
[mark^#(x₁)]	=	2
[0]	=	43588
[a__and^#(x₁, x₂)]	=	2
[a__U21(x₁, x₂)]	=	43587
[a__U32(x₁, x₂)]	=	x₁ + 8
[mark(x₁)]	=	43585
[a__U11(x₁, x₂, x₃)]	=	x₂ + x₃ + 43587
[U32(x₁, x₂)]	=	x₂ + 9
[U33(x₁)]	=	x₁ + 43590
[a__U12(x₁, x₂)]	=	x₂ + 43588
[isNat(x₁)]	=	x₁ + 43587
[plus(x₁, x₂)]	=	x₁ + 43589
[U61(x₁)]	=	x₁ + 43588
[a__U22^#(x₁)]	=	0
[a__U13(x₁)]	=	43589
[U31(x₁, x₂, x₃)]	=	x₃ + 4
[a__U71(x₁, x₂, x₃)]	=	43587
[a__U61(x₁)]	=	43587
[a__U41^#(x₁, x₂)]	=	0
[tt]	=	43590
[a__isNat(x₁)]	=	43586
[U13(x₁)]	=	x₁ + 43590
[a__isNatKind(x₁)]	=	43586
[U22(x₁)]	=	43589
[U51(x₁, x₂, x₃)]	=	43590
[a__and(x₁, x₂)]	=	43584
[U41(x₁, x₂)]	=	6
[a__U32^#(x₁, x₂)]	=	0

having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the pairs

a__isNatKind^#(plus(V1,V2))	→	a__isNatKind^#(V1)	(85)
a__isNatKind^#(s(V1))	→	a__isNatKind^#(V1)	(69)

could be deleted.

1.1.1.1.1.1.1.1.1.1.2.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 2^nd component contains the pair

mark^#(U51(X1,X2,X3))	→	a__U51^#(mark(X1),X2,X3)	(94)
mark^#(U12(X1,X2))	→	mark^#(X1)	(124)
a__plus^#(N,0)	→	a__U41^#(a__and(a__isNat(N),isNatKind(N)),N)	(137)
mark^#(s(X))	→	mark^#(X)	(108)
a__U51^#(tt,M,N)	→	mark^#(N)	(76)
a__U51^#(tt,M,N)	→	a__plus^#(mark(N),mark(M))	(73)
mark^#(U71(X1,X2,X3))	→	a__U71^#(mark(X1),X2,X3)	(98)
a__x^#(N,s(M))	→	a__U71^#(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N)	(81)
mark^#(U22(X))	→	mark^#(X)	(66)
a__U71^#(tt,M,N)	→	a__x^#(mark(N),mark(M))	(107)
a__U71^#(tt,M,N)	→	a__plus^#(a__x(mark(N),mark(M)),mark(N))	(65)
a__plus^#(N,s(M))	→	a__U51^#(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N)	(110)
a__U41^#(tt,N)	→	mark^#(N)	(132)
mark^#(x(X1,X2))	→	a__x^#(mark(X1),mark(X2))	(125)
mark^#(plus(X1,X2))	→	mark^#(X1)	(90)
mark^#(plus(X1,X2))	→	a__plus^#(mark(X1),mark(X2))	(114)
mark^#(and(X1,X2))	→	mark^#(X1)	(89)
mark^#(U41(X1,X2))	→	a__U41^#(mark(X1),X2)	(117)

1.1.1.1.1.1.1.1.1.1.2.1.2 Reduction Pair Processor with Usable Rules

Using the argument filter

π(a__isNatKind^#)	=	1
π(a__U33^#)	=	1
π(a__U51^#)	=	3
π(a__plus^#)	=	1
π(mark^#)	=	1
π(a__and^#)	=	2
π(mark)	=	1
π(a__U41^#)	=	2
π(a__U32^#)	=	1

in combination with the following Weighted Path Order with the following precedence and status

prec(isNatKind)	=	5	status(isNatKind)	=	[1]	list-extension(isNatKind)	=	Lex
prec(a__plus)	=	9	status(a__plus)	=	[1, 2]	list-extension(a__plus)	=	Lex
prec(U21)	=	3	status(U21)	=	[2, 1]	list-extension(U21)	=	Lex
prec(a__U71^#)	=	10	status(a__U71^#)	=	[3, 2]	list-extension(a__U71^#)	=	Lex
prec(U11)	=	8	status(U11)	=	[2]	list-extension(U11)	=	Lex
prec(s)	=	5	status(s)	=	[1]	list-extension(s)	=	Lex
prec(a__U31^#)	=	0	status(a__U31^#)	=	[1, 3, 2]	list-extension(a__U31^#)	=	Lex
prec(a__U33)	=	6	status(a__U33)	=	[]	list-extension(a__U33)	=	Lex
prec(a__isNat^#)	=	0	status(a__isNat^#)	=	[]	list-extension(a__isNat^#)	=	Lex
prec(U71)	=	10	status(U71)	=	[3, 2, 1]	list-extension(U71)	=	Lex
prec(and)	=	0	status(and)	=	[1, 2]	list-extension(and)	=	Lex
prec(a__U13^#)	=	0	status(a__U13^#)	=	[]	list-extension(a__U13^#)	=	Lex
prec(a__x^#)	=	10	status(a__x^#)	=	[1, 2]	list-extension(a__x^#)	=	Lex
prec(a__U22)	=	2	status(a__U22)	=	[1]	list-extension(a__U22)	=	Lex
prec(a__U11^#)	=	0	status(a__U11^#)	=	[2, 3, 1]	list-extension(a__U11^#)	=	Lex
prec(a__U31)	=	0	status(a__U31)	=	[2, 3, 1]	list-extension(a__U31)	=	Lex
prec(a__U51)	=	9	status(a__U51)	=	[3, 2, 1]	list-extension(a__U51)	=	Lex
prec(a__x)	=	10	status(a__x)	=	[1, 2]	list-extension(a__x)	=	Lex
prec(U12)	=	7	status(U12)	=	[1]	list-extension(U12)	=	Lex
prec(a__U41)	=	1	status(a__U41)	=	[2, 1]	list-extension(a__U41)	=	Lex
prec(x)	=	10	status(x)	=	[1, 2]	list-extension(x)	=	Lex
prec(a__U12^#)	=	0	status(a__U12^#)	=	[2, 1]	list-extension(a__U12^#)	=	Lex
prec(a__U21^#)	=	0	status(a__U21^#)	=	[2, 1]	list-extension(a__U21^#)	=	Lex
prec(a__U61^#)	=	0	status(a__U61^#)	=	[]	list-extension(a__U61^#)	=	Lex
prec(0)	=	11	status(0)	=	[]	list-extension(0)	=	Lex
prec(a__U21)	=	3	status(a__U21)	=	[2, 1]	list-extension(a__U21)	=	Lex
prec(a__U32)	=	6	status(a__U32)	=	[]	list-extension(a__U32)	=	Lex
prec(a__U11)	=	8	status(a__U11)	=	[2]	list-extension(a__U11)	=	Lex
prec(U32)	=	6	status(U32)	=	[]	list-extension(U32)	=	Lex
prec(U33)	=	6	status(U33)	=	[]	list-extension(U33)	=	Lex
prec(a__U12)	=	7	status(a__U12)	=	[1]	list-extension(a__U12)	=	Lex
prec(isNat)	=	3	status(isNat)	=	[1]	list-extension(isNat)	=	Lex
prec(plus)	=	9	status(plus)	=	[1, 2]	list-extension(plus)	=	Lex
prec(U61)	=	11	status(U61)	=	[]	list-extension(U61)	=	Lex
prec(a__U22^#)	=	0	status(a__U22^#)	=	[]	list-extension(a__U22^#)	=	Lex
prec(a__U13)	=	6	status(a__U13)	=	[]	list-extension(a__U13)	=	Lex
prec(U31)	=	0	status(U31)	=	[2, 3, 1]	list-extension(U31)	=	Lex
prec(a__U71)	=	10	status(a__U71)	=	[3, 2, 1]	list-extension(a__U71)	=	Lex
prec(a__U61)	=	11	status(a__U61)	=	[]	list-extension(a__U61)	=	Lex
prec(tt)	=	6	status(tt)	=	[]	list-extension(tt)	=	Lex
prec(a__isNat)	=	3	status(a__isNat)	=	[1]	list-extension(a__isNat)	=	Lex
prec(U13)	=	6	status(U13)	=	[]	list-extension(U13)	=	Lex
prec(a__isNatKind)	=	5	status(a__isNatKind)	=	[1]	list-extension(a__isNatKind)	=	Lex
prec(U22)	=	2	status(U22)	=	[1]	list-extension(U22)	=	Lex
prec(U51)	=	9	status(U51)	=	[3, 2, 1]	list-extension(U51)	=	Lex
prec(a__and)	=	0	status(a__and)	=	[1, 2]	list-extension(a__and)	=	Lex
prec(U41)	=	1	status(U41)	=	[2, 1]	list-extension(U41)	=	Lex

and the following Max-polynomial interpretation

[isNatKind(x₁)]	=	x₁ + 0
[a__plus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[U21(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[a__U71^#(x₁, x₂, x₃)]	=	max(x₂ + 0, x₃ + 0, 0)
[U11(x₁, x₂, x₃)]	=	max(x₂ + 0, 0)
[s(x₁)]	=	x₁ + 0
[a__U31^#(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 0, 0)
[a__U33(x₁)]	=	0
[a__isNat^#(x₁)]	=	0
[U71(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 0, 0)
[and(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[a__U13^#(x₁)]	=	0
[a__x^#(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[a__U22(x₁)]	=	x₁ + 0
[a__U11^#(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 0, 0)
[a__U31(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 0, 0)
[a__U51(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 0, 0)
[a__x(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[U12(x₁, x₂)]	=	max(x₁ + 0, 0)
[a__U41(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[x(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[a__U12^#(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[a__U21^#(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[a__U61^#(x₁)]	=	0
[0]	=	0
[a__U21(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[a__U32(x₁, x₂)]	=	max(0)
[a__U11(x₁, x₂, x₃)]	=	max(x₂ + 0, 0)
[U32(x₁, x₂)]	=	max(0)
[U33(x₁)]	=	0
[a__U12(x₁, x₂)]	=	max(x₁ + 0, 0)
[isNat(x₁)]	=	x₁ + 0
[plus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[U61(x₁)]	=	0
[a__U22^#(x₁)]	=	0
[a__U13(x₁)]	=	0
[U31(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 0, 0)
[a__U71(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 0, 0)
[a__U61(x₁)]	=	0
[tt]	=	0
[a__isNat(x₁)]	=	x₁ + 0
[U13(x₁)]	=	0
[a__isNatKind(x₁)]	=	x₁ + 0
[U22(x₁)]	=	x₁ + 0
[U51(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 0, 0)
[a__and(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[U41(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)

together with the usable rules

a__isNatKind(0)	→	tt	(18)
a__U21(X1,X2)	→	U21(X1,X2)	(50)
a__U21(tt,V1)	→	a__U22(a__isNat(V1))	(4)
a__isNat(plus(V1,V2))	→	a__U11(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2)	(15)
a__U33(tt)	→	tt	(8)
a__U33(X)	→	U33(X)	(54)
a__U11(tt,V1,V2)	→	a__U12(a__isNat(V1),V2)	(1)
a__U13(tt)	→	tt	(3)
a__isNat(s(V1))	→	a__U21(a__isNatKind(V1),V1)	(16)
a__isNatKind(x(V1,V2))	→	a__and(a__isNatKind(V1),isNatKind(V2))	(21)
mark(U51(X1,X2,X3))	→	a__U51(mark(X1),X2,X3)	(36)
mark(U11(X1,X2,X3))	→	a__U11(mark(X1),X2,X3)	(26)
a__isNatKind(plus(V1,V2))	→	a__and(a__isNatKind(V1),isNatKind(V2))	(19)
mark(U31(X1,X2,X3))	→	a__U31(mark(X1),X2,X3)	(32)
a__isNat(x(V1,V2))	→	a__U31(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2)	(17)
a__x(X1,X2)	→	x(X1,X2)	(60)
mark(U12(X1,X2))	→	a__U12(mark(X1),X2)	(27)
mark(U33(X))	→	a__U33(mark(X))	(34)
a__plus(N,0)	→	a__U41(a__and(a__isNat(N),isNatKind(N)),N)	(22)
mark(isNat(X))	→	a__isNat(X)	(28)
mark(s(X))	→	s(mark(X))	(44)
a__U22(tt)	→	tt	(5)
mark(U32(X1,X2))	→	a__U32(mark(X1),X2)	(33)
a__U51(tt,M,N)	→	s(a__plus(mark(N),mark(M)))	(10)
mark(U71(X1,X2,X3))	→	a__U71(mark(X1),X2,X3)	(39)
a__U32(tt,V2)	→	a__U33(a__isNat(V2))	(7)
a__isNatKind(s(V1))	→	a__isNatKind(V1)	(20)
a__x(N,s(M))	→	a__U71(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N)	(25)
a__U13(X)	→	U13(X)	(49)
a__U31(X1,X2,X3)	→	U31(X1,X2,X3)	(52)
mark(U21(X1,X2))	→	a__U21(mark(X1),X2)	(30)
a__isNatKind(X)	→	isNatKind(X)	(62)
a__isNat(0)	→	tt	(14)
a__U51(X1,X2,X3)	→	U51(X1,X2,X3)	(56)
mark(U22(X))	→	a__U22(mark(X))	(31)
a__U71(tt,M,N)	→	a__plus(a__x(mark(N),mark(M)),mark(N))	(12)
mark(0)	→	0	(45)
a__plus(N,s(M))	→	a__U51(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N)	(23)
a__x(N,0)	→	a__U61(a__and(a__isNat(N),isNatKind(N)))	(24)
a__plus(X1,X2)	→	plus(X1,X2)	(57)
a__U61(tt)	→	0	(11)
a__U41(tt,N)	→	mark(N)	(9)
a__and(tt,X)	→	mark(X)	(13)
a__U22(X)	→	U22(X)	(51)
mark(x(X1,X2))	→	a__x(mark(X1),mark(X2))	(40)
a__U41(X1,X2)	→	U41(X1,X2)	(55)
a__U71(X1,X2,X3)	→	U71(X1,X2,X3)	(59)
a__U31(tt,V1,V2)	→	a__U32(a__isNat(V1),V2)	(6)
mark(U61(X))	→	a__U61(mark(X))	(38)
a__and(X1,X2)	→	and(X1,X2)	(61)
a__U61(X)	→	U61(X)	(58)
a__isNat(X)	→	isNat(X)	(48)
a__U32(X1,X2)	→	U32(X1,X2)	(53)
a__U12(X1,X2)	→	U12(X1,X2)	(47)
mark(plus(X1,X2))	→	a__plus(mark(X1),mark(X2))	(37)
mark(and(X1,X2))	→	a__and(mark(X1),X2)	(41)
mark(isNatKind(X))	→	a__isNatKind(X)	(42)
a__U11(X1,X2,X3)	→	U11(X1,X2,X3)	(46)
mark(U41(X1,X2))	→	a__U41(mark(X1),X2)	(35)
mark(U13(X))	→	a__U13(mark(X))	(29)
mark(tt)	→	tt	(43)
a__U12(tt,V2)	→	a__U13(a__isNat(V2))	(2)

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

mark^#(U51(X1,X2,X3))	→	a__U51^#(mark(X1),X2,X3)	(94)
mark^#(U12(X1,X2))	→	mark^#(X1)	(124)
mark^#(s(X))	→	mark^#(X)	(108)
mark^#(U71(X1,X2,X3))	→	a__U71^#(mark(X1),X2,X3)	(98)
a__x^#(N,s(M))	→	a__U71^#(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N)	(81)
mark^#(U22(X))	→	mark^#(X)	(66)
mark^#(plus(X1,X2))	→	mark^#(X1)	(90)
mark^#(plus(X1,X2))	→	a__plus^#(mark(X1),mark(X2))	(114)
mark^#(and(X1,X2))	→	mark^#(X1)	(89)
mark^#(U41(X1,X2))	→	a__U41^#(mark(X1),X2)	(117)

could be deleted.

1.1.1.1.1.1.1.1.1.1.2.1.2.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

a__U51^#(tt,M,N)	→	a__plus^#(mark(N),mark(M))	(73)
a__plus^#(N,s(M))	→	a__U51^#(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N)	(110)

1.1.1.1.1.1.1.1.1.1.2.1.2.1.1 Reduction Pair Processor with Usable Rules

Using the argument filter

π(a__isNatKind^#)	=	1
π(a__U33^#)	=	1
π(a__U51^#)	=	2
π(a__plus^#)	=	2
π(mark^#)	=	1
π(a__and^#)	=	2
π(mark)	=	1
π(a__U41^#)	=	2
π(a__U32^#)	=	1

in combination with the following Weighted Path Order with the following precedence and status

prec(isNatKind)	=	4	status(isNatKind)	=	[1]	list-extension(isNatKind)	=	Lex
prec(a__plus)	=	9	status(a__plus)	=	[1, 2]	list-extension(a__plus)	=	Lex
prec(U21)	=	3	status(U21)	=	[2, 1]	list-extension(U21)	=	Lex
prec(a__U71^#)	=	10	status(a__U71^#)	=	[3, 2]	list-extension(a__U71^#)	=	Lex
prec(U11)	=	8	status(U11)	=	[2]	list-extension(U11)	=	Lex
prec(s)	=	4	status(s)	=	[1]	list-extension(s)	=	Lex
prec(a__U31^#)	=	0	status(a__U31^#)	=	[1, 3, 2]	list-extension(a__U31^#)	=	Lex
prec(a__U33)	=	6	status(a__U33)	=	[]	list-extension(a__U33)	=	Lex
prec(a__isNat^#)	=	0	status(a__isNat^#)	=	[]	list-extension(a__isNat^#)	=	Lex
prec(U71)	=	10	status(U71)	=	[3, 2, 1]	list-extension(U71)	=	Lex
prec(and)	=	0	status(and)	=	[1, 2]	list-extension(and)	=	Lex
prec(a__U13^#)	=	0	status(a__U13^#)	=	[]	list-extension(a__U13^#)	=	Lex
prec(a__x^#)	=	10	status(a__x^#)	=	[1, 2]	list-extension(a__x^#)	=	Lex
prec(a__U22)	=	2	status(a__U22)	=	[1]	list-extension(a__U22)	=	Lex
prec(a__U11^#)	=	0	status(a__U11^#)	=	[2, 3, 1]	list-extension(a__U11^#)	=	Lex
prec(a__U31)	=	0	status(a__U31)	=	[2, 3, 1]	list-extension(a__U31)	=	Lex
prec(a__U51)	=	9	status(a__U51)	=	[3, 2, 1]	list-extension(a__U51)	=	Lex
prec(a__x)	=	10	status(a__x)	=	[1, 2]	list-extension(a__x)	=	Lex
prec(U12)	=	7	status(U12)	=	[1]	list-extension(U12)	=	Lex
prec(a__U41)	=	1	status(a__U41)	=	[2, 1]	list-extension(a__U41)	=	Lex
prec(x)	=	10	status(x)	=	[1, 2]	list-extension(x)	=	Lex
prec(a__U12^#)	=	0	status(a__U12^#)	=	[2, 1]	list-extension(a__U12^#)	=	Lex
prec(a__U21^#)	=	0	status(a__U21^#)	=	[2, 1]	list-extension(a__U21^#)	=	Lex
prec(a__U61^#)	=	0	status(a__U61^#)	=	[]	list-extension(a__U61^#)	=	Lex
prec(0)	=	11	status(0)	=	[]	list-extension(0)	=	Lex
prec(a__U21)	=	3	status(a__U21)	=	[2, 1]	list-extension(a__U21)	=	Lex
prec(a__U32)	=	6	status(a__U32)	=	[]	list-extension(a__U32)	=	Lex
prec(a__U11)	=	8	status(a__U11)	=	[2]	list-extension(a__U11)	=	Lex
prec(U32)	=	6	status(U32)	=	[]	list-extension(U32)	=	Lex
prec(U33)	=	6	status(U33)	=	[]	list-extension(U33)	=	Lex
prec(a__U12)	=	7	status(a__U12)	=	[1]	list-extension(a__U12)	=	Lex
prec(isNat)	=	3	status(isNat)	=	[1]	list-extension(isNat)	=	Lex
prec(plus)	=	9	status(plus)	=	[1, 2]	list-extension(plus)	=	Lex
prec(U61)	=	11	status(U61)	=	[]	list-extension(U61)	=	Lex
prec(a__U22^#)	=	0	status(a__U22^#)	=	[]	list-extension(a__U22^#)	=	Lex
prec(a__U13)	=	6	status(a__U13)	=	[]	list-extension(a__U13)	=	Lex
prec(U31)	=	0	status(U31)	=	[2, 3, 1]	list-extension(U31)	=	Lex
prec(a__U71)	=	10	status(a__U71)	=	[3, 2, 1]	list-extension(a__U71)	=	Lex
prec(a__U61)	=	11	status(a__U61)	=	[]	list-extension(a__U61)	=	Lex
prec(tt)	=	6	status(tt)	=	[]	list-extension(tt)	=	Lex
prec(a__isNat)	=	3	status(a__isNat)	=	[1]	list-extension(a__isNat)	=	Lex
prec(U13)	=	6	status(U13)	=	[]	list-extension(U13)	=	Lex
prec(a__isNatKind)	=	4	status(a__isNatKind)	=	[1]	list-extension(a__isNatKind)	=	Lex
prec(U22)	=	2	status(U22)	=	[1]	list-extension(U22)	=	Lex
prec(U51)	=	9	status(U51)	=	[3, 2, 1]	list-extension(U51)	=	Lex
prec(a__and)	=	0	status(a__and)	=	[1, 2]	list-extension(a__and)	=	Lex
prec(U41)	=	1	status(U41)	=	[2, 1]	list-extension(U41)	=	Lex

and the following Max-polynomial interpretation

[isNatKind(x₁)]	=	x₁ + 0
[a__plus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[U21(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[a__U71^#(x₁, x₂, x₃)]	=	max(x₂ + 0, x₃ + 0, 0)
[U11(x₁, x₂, x₃)]	=	max(x₂ + 0, 0)
[s(x₁)]	=	x₁ + 0
[a__U31^#(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 0, 0)
[a__U33(x₁)]	=	0
[a__isNat^#(x₁)]	=	0
[U71(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 0, 0)
[and(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[a__U13^#(x₁)]	=	0
[a__x^#(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[a__U22(x₁)]	=	x₁ + 0
[a__U11^#(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 0, 0)
[a__U31(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 0, 0)
[a__U51(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 0, 0)
[a__x(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[U12(x₁, x₂)]	=	max(x₁ + 0, 0)
[a__U41(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[x(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[a__U12^#(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[a__U21^#(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[a__U61^#(x₁)]	=	0
[0]	=	0
[a__U21(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[a__U32(x₁, x₂)]	=	max(0)
[a__U11(x₁, x₂, x₃)]	=	max(x₂ + 0, 0)
[U32(x₁, x₂)]	=	max(0)
[U33(x₁)]	=	0
[a__U12(x₁, x₂)]	=	max(x₁ + 0, 0)
[isNat(x₁)]	=	x₁ + 0
[plus(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[U61(x₁)]	=	0
[a__U22^#(x₁)]	=	0
[a__U13(x₁)]	=	0
[U31(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 0, 0)
[a__U71(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 0, 0)
[a__U61(x₁)]	=	0
[tt]	=	0
[a__isNat(x₁)]	=	x₁ + 0
[U13(x₁)]	=	0
[a__isNatKind(x₁)]	=	x₁ + 0
[U22(x₁)]	=	x₁ + 0
[U51(x₁, x₂, x₃)]	=	max(x₁ + 0, x₂ + 0, x₃ + 0, 0)
[a__and(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[U41(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)

together with the usable rules

a__isNatKind(0)	→	tt	(18)
a__U21(X1,X2)	→	U21(X1,X2)	(50)
a__U21(tt,V1)	→	a__U22(a__isNat(V1))	(4)
a__isNat(plus(V1,V2))	→	a__U11(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2)	(15)
a__U33(tt)	→	tt	(8)
a__U33(X)	→	U33(X)	(54)
a__U11(tt,V1,V2)	→	a__U12(a__isNat(V1),V2)	(1)
a__U13(tt)	→	tt	(3)
a__isNat(s(V1))	→	a__U21(a__isNatKind(V1),V1)	(16)
a__isNatKind(x(V1,V2))	→	a__and(a__isNatKind(V1),isNatKind(V2))	(21)
mark(U51(X1,X2,X3))	→	a__U51(mark(X1),X2,X3)	(36)
mark(U11(X1,X2,X3))	→	a__U11(mark(X1),X2,X3)	(26)
a__isNatKind(plus(V1,V2))	→	a__and(a__isNatKind(V1),isNatKind(V2))	(19)
mark(U31(X1,X2,X3))	→	a__U31(mark(X1),X2,X3)	(32)
a__isNat(x(V1,V2))	→	a__U31(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2)	(17)
a__x(X1,X2)	→	x(X1,X2)	(60)
mark(U12(X1,X2))	→	a__U12(mark(X1),X2)	(27)
mark(U33(X))	→	a__U33(mark(X))	(34)
a__plus(N,0)	→	a__U41(a__and(a__isNat(N),isNatKind(N)),N)	(22)
mark(isNat(X))	→	a__isNat(X)	(28)
mark(s(X))	→	s(mark(X))	(44)
a__U22(tt)	→	tt	(5)
mark(U32(X1,X2))	→	a__U32(mark(X1),X2)	(33)
a__U51(tt,M,N)	→	s(a__plus(mark(N),mark(M)))	(10)
mark(U71(X1,X2,X3))	→	a__U71(mark(X1),X2,X3)	(39)
a__U32(tt,V2)	→	a__U33(a__isNat(V2))	(7)
a__isNatKind(s(V1))	→	a__isNatKind(V1)	(20)
a__x(N,s(M))	→	a__U71(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N)	(25)
a__U13(X)	→	U13(X)	(49)
a__U31(X1,X2,X3)	→	U31(X1,X2,X3)	(52)
mark(U21(X1,X2))	→	a__U21(mark(X1),X2)	(30)
a__isNatKind(X)	→	isNatKind(X)	(62)
a__isNat(0)	→	tt	(14)
a__U51(X1,X2,X3)	→	U51(X1,X2,X3)	(56)
mark(U22(X))	→	a__U22(mark(X))	(31)
a__U71(tt,M,N)	→	a__plus(a__x(mark(N),mark(M)),mark(N))	(12)
mark(0)	→	0	(45)
a__plus(N,s(M))	→	a__U51(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N)	(23)
a__x(N,0)	→	a__U61(a__and(a__isNat(N),isNatKind(N)))	(24)
a__plus(X1,X2)	→	plus(X1,X2)	(57)
a__U61(tt)	→	0	(11)
a__U41(tt,N)	→	mark(N)	(9)
a__and(tt,X)	→	mark(X)	(13)
a__U22(X)	→	U22(X)	(51)
mark(x(X1,X2))	→	a__x(mark(X1),mark(X2))	(40)
a__U41(X1,X2)	→	U41(X1,X2)	(55)
a__U71(X1,X2,X3)	→	U71(X1,X2,X3)	(59)
a__U31(tt,V1,V2)	→	a__U32(a__isNat(V1),V2)	(6)
mark(U61(X))	→	a__U61(mark(X))	(38)
a__and(X1,X2)	→	and(X1,X2)	(61)
a__U61(X)	→	U61(X)	(58)
a__isNat(X)	→	isNat(X)	(48)
a__U32(X1,X2)	→	U32(X1,X2)	(53)
a__U12(X1,X2)	→	U12(X1,X2)	(47)
mark(plus(X1,X2))	→	a__plus(mark(X1),mark(X2))	(37)
mark(and(X1,X2))	→	a__and(mark(X1),X2)	(41)
mark(isNatKind(X))	→	a__isNatKind(X)	(42)
a__U11(X1,X2,X3)	→	U11(X1,X2,X3)	(46)
mark(U41(X1,X2))	→	a__U41(mark(X1),X2)	(35)
mark(U13(X))	→	a__U13(mark(X))	(29)
mark(tt)	→	tt	(43)
a__U12(tt,V2)	→	a__U13(a__isNat(V2))	(2)

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

a__plus^#(N,s(M))

→

a__U51^#(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N)

(110)

could be deleted.

1.1.1.1.1.1.1.1.1.1.2.1.2.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.