Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/LISTUTILITIES_nokinds_GM)

The rewrite relation of the following TRS is considered.

Property / Task

Answer / Result

Proof (by NaTT @ termCOMP 2023)

1 Dependency Pair Transformation

There are 124 ruless (increase limit for explicit display).

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

• The 1^st component contains the pair

  There are 124 ruless (increase limit for explicit display).

  1.1.1 Reduction Pair Processor with Usable Rules

  Using the Max-polynomial interpretation

  [U21(x1, x2)]	=	max(x1 + 0, x2 + 0, 0)
  [a__U82#(x1, x2)]	=	max(x1 + 0, x2 + 0, 0)
  [a__U71#(x1, x2)]	=	max(x1 + 0, x2 + 0, 0)
  [U11(x1, x2, x3)]	=	max(x1 + 3, x2 + 2, x3 + 1, 0)
  [s(x1)]	=	x1 + 0
  [a__U31#(x1, x2)]	=	max(x1 + 52063, x2 + 0, 0)
  [a__head#(x1)]	=	x1 + 52064
  [a__natsFrom#(x1)]	=	x1 + 0
  [isPLNat(x1)]	=	x1 + 0
  [a__snd#(x1)]	=	x1 + 0
  [a__afterNth(x1, x2)]	=	max(x1 + 6, x2 + 5, 0)
  [U91(x1, x2)]	=	max(x1 + 49661, x2 + 49660, 0)
  [a__U82(x1, x2)]	=	max(x1 + 0, x2 + 0, 0)
  [take(x1, x2)]	=	max(x1 + 3578, x2 + 0, 0)
  [U71(x1, x2)]	=	max(x1 + 0, x2 + 0, 0)
  [and(x1, x2)]	=	max(x1 + 0, x2 + 0, 0)
  [U101(x1, x2, x3)]	=	max(x1 + 0, x2 + 3578, x3 + 0, 0)
  [pair(x1, x2)]	=	max(x1 + 0, x2 + 0, 0)
  [fst(x1)]	=	x1 + 0
  [natsFrom(x1)]	=	x1 + 0
  [a__snd(x1)]	=	x1 + 1
  [a__U51#(x1, x2, x3)]	=	max(x1 + 52075, x2 + 52073, x3 + 52071, 0)
  [splitAt(x1, x2)]	=	max(x1 + 0, x2 + 0, 0)
  [a__U11#(x1, x2, x3)]	=	max(x1 + 3, x2 + 0, x3 + 0, 0)
  [a__U31(x1, x2)]	=	max(x1 + 52066, x2 + 52062, 0)
  [a__U51(x1, x2, x3)]	=	max(x1 + 52076, x2 + 52074, x3 + 52072, 0)
  [a__U81(x1,...,x4)]	=	max(x1 + 0, x2 + 0, x3 + 0, x4 + 0, 0)
  [a__take#(x1, x2)]	=	max(x1 + 0, x2 + 0, 0)
  [isNatural(x1)]	=	x1 + 0
  [a__U41(x1, x2)]	=	max(x1 + 0, x2 + 0, 0)
  [a__U21#(x1, x2)]	=	max(x1 + 0, x2 + 0, 0)
  [a__U81#(x1,...,x4)]	=	max(x1 + 0, x2 + 0, x3 + 0, x4 + 0, 0)
  [a__U61#(x1, x2)]	=	max(x1 + 0, x2 + 0, 0)
  [a__fst(x1)]	=	x1 + 0
  [tail(x1)]	=	x1 + 49662
  [a__natsFrom(x1)]	=	x1 + 0
  [mark#(x1)]	=	x1 + 0
  [0]	=	43731
  [a__and#(x1, x2)]	=	max(x2 + 0, 0)
  [a__isLNat(x1)]	=	x1 + 0
  [a__U21(x1, x2)]	=	max(x1 + 0, x2 + 0, 0)
  [a__U91(x1, x2)]	=	max(x1 + 49661, x2 + 49660, 0)
  [sel(x1, x2)]	=	max(x1 + 52077, x2 + 52079, 0)
  [afterNth(x1, x2)]	=	max(x1 + 6, x2 + 5, 0)
  [nil]	=	1
  [a__splitAt(x1, x2)]	=	max(x1 + 0, x2 + 0, 0)
  [isLNat(x1)]	=	x1 + 0
  [a__sel#(x1, x2)]	=	max(x1 + 52076, x2 + 52078, 0)
  [mark(x1)]	=	x1 + 0
  [a__isLNat#(x1)]	=	x1 + 0
  [a__U101#(x1, x2, x3)]	=	max(x1 + 0, x2 + 0, x3 + 0, 0)
  [a__U11(x1, x2, x3)]	=	max(x1 + 3, x2 + 2, x3 + 1, 0)
  [a__sel(x1, x2)]	=	max(x1 + 52077, x2 + 52079, 0)
  [a__isPLNat(x1)]	=	x1 + 0
  [U61(x1, x2)]	=	max(x1 + 1, x2 + 0, 0)
  [U31(x1, x2)]	=	max(x1 + 52066, x2 + 52062, 0)
  [a__U71(x1, x2)]	=	max(x1 + 0, x2 + 0, 0)
  [a__isPLNat#(x1)]	=	x1 + 0
  [head(x1)]	=	x1 + 52067
  [a__afterNth#(x1, x2)]	=	max(x1 + 5, x2 + 4, 0)
  [a__splitAt#(x1, x2)]	=	max(x1 + 0, x2 + 0, 0)
  [cons(x1, x2)]	=	max(x1 + 0, x2 + 0, 0)
  [a__U61(x1, x2)]	=	max(x1 + 1, x2 + 0, 0)
  [snd(x1)]	=	x1 + 1
  [a__take(x1, x2)]	=	max(x1 + 3578, x2 + 0, 0)
  [U81(x1,...,x4)]	=	max(x1 + 0, x2 + 0, x3 + 0, x4 + 0, 0)
  [a__U41#(x1, x2)]	=	max(x1 + 0, x2 + 0, 0)
  [U82(x1, x2)]	=	max(x1 + 0, x2 + 0, 0)
  [tt]	=	1
  [a__isNatural(x1)]	=	x1 + 0
  [a__isNatural#(x1)]	=	x1 + 0
  [a__fst#(x1)]	=	x1 + 0
  [U51(x1, x2, x3)]	=	max(x1 + 52076, x2 + 52074, x3 + 52072, 0)
  [a__and(x1, x2)]	=	max(x1 + 0, x2 + 0, 0)
  [a__tail(x1)]	=	x1 + 49662
  [U41(x1, x2)]	=	max(x1 + 0, x2 + 0, 0)
  [a__tail#(x1)]	=	x1 + 49661
  [a__U101(x1, x2, x3)]	=	max(x1 + 0, x2 + 3578, x3 + 0, 0)
  [a__U91#(x1, x2)]	=	max(x1 + 49660, x2 + 49659, 0)
  [a__head(x1)]	=	x1 + 52067

  together with the usable rules

  a__isLNat(cons(V1,V2))	→	a__and(a__isNatural(V1),isLNat(V2))	(18)
  mark(U71(X1,X2))	→	a__U71(mark(X1),X2)	(50)
  a__U71(X1,X2)	→	U71(X1,X2)	(80)
  a__U31(tt,N)	→	mark(N)	(4)
  a__head(cons(N,XS))	→	a__U31(a__and(a__isNatural(N),isLNat(XS)),N)	(15)
  a__U71(tt,XS)	→	pair(nil,mark(XS))	(8)
  mark(and(X1,X2))	→	a__and(mark(X1),X2)	(54)
  a__U101(tt,N,XS)	→	a__fst(a__splitAt(mark(N),mark(XS)))	(1)
  a__head(X)	→	head(X)	(77)
  a__U21(tt,X)	→	mark(X)	(3)
  a__isLNat(nil)	→	tt	(16)
  a__isLNat(snd(V1))	→	a__isPLNat(V1)	(21)
  a__take(N,XS)	→	a__U101(a__and(a__isNatural(N),isLNat(XS)),N,XS)	(36)
  a__fst(X)	→	fst(X)	(68)
  a__isNatural(X)	→	isNatural(X)	(85)
  a__isNatural(s(V1))	→	a__isNatural(V1)	(26)
  mark(s(X))	→	s(mark(X))	(63)
  a__isLNat(fst(V1))	→	a__isPLNat(V1)	(19)
  a__snd(pair(X,Y))	→	a__U61(a__and(a__isLNat(X),isLNat(Y)),Y)	(32)
  a__isLNat(afterNth(V1,V2))	→	a__and(a__isNatural(V1),isLNat(V2))	(17)
  mark(sel(X1,X2))	→	a__sel(mark(X1),mark(X2))	(60)
  a__isNatural(sel(V1,V2))	→	a__and(a__isNatural(V1),isLNat(V2))	(27)
  a__isPLNat(X)	→	isPLNat(X)	(87)
  a__and(X1,X2)	→	and(X1,X2)	(84)
  a__splitAt(s(N),cons(X,XS))	→	a__U81(a__and(a__isNatural(N),and(isNatural(X),isLNat(XS))),N,X,XS)	(34)
  a__isLNat(tail(V1))	→	a__isLNat(V1)	(22)
  a__isPLNat(pair(V1,V2))	→	a__and(a__isLNat(V1),isLNat(V2))	(28)
  mark(nil)	→	nil	(65)
  mark(U41(X1,X2))	→	a__U41(mark(X1),X2)	(44)
  a__U41(tt,N)	→	cons(mark(N),natsFrom(s(N)))	(5)
  a__U21(X1,X2)	→	U21(X1,X2)	(72)
  a__splitAt(0,XS)	→	a__U71(a__isLNat(XS),XS)	(33)
  mark(pair(X1,X2))	→	pair(mark(X1),mark(X2))	(64)
  a__U82(pair(YS,ZS),X)	→	pair(cons(mark(X),YS),mark(ZS))	(10)
  mark(splitAt(X1,X2))	→	a__splitAt(mark(X1),mark(X2))	(39)
  a__U61(tt,Y)	→	mark(Y)	(7)
  a__tail(X)	→	tail(X)	(88)
  a__isLNat(natsFrom(V1))	→	a__isNatural(V1)	(20)
  a__isNatural(head(V1))	→	a__isLNat(V1)	(25)
  mark(U61(X1,X2))	→	a__U61(mark(X1),X2)	(49)
  mark(U82(X1,X2))	→	a__U82(mark(X1),X2)	(52)
  a__natsFrom(N)	→	a__U41(a__isNatural(N),N)	(30)
  mark(cons(X1,X2))	→	cons(mark(X1),X2)	(62)
  a__fst(pair(X,Y))	→	a__U21(a__and(a__isLNat(X),isLNat(Y)),X)	(14)
  a__U82(X1,X2)	→	U82(X1,X2)	(82)
  a__take(X1,X2)	→	take(X1,X2)	(89)
  mark(isLNat(X))	→	a__isLNat(X)	(56)
  a__U61(X1,X2)	→	U61(X1,X2)	(79)
  a__sel(N,XS)	→	a__U51(a__and(a__isNatural(N),isLNat(XS)),N,XS)	(31)
  a__afterNth(N,XS)	→	a__U11(a__and(a__isNatural(N),isLNat(XS)),N,XS)	(12)
  a__splitAt(X1,X2)	→	splitAt(X1,X2)	(69)
  mark(natsFrom(X))	→	a__natsFrom(mark(X))	(45)
  a__afterNth(X1,X2)	→	afterNth(X1,X2)	(78)
  a__U81(X1,X2,X3,X4)	→	U81(X1,X2,X3,X4)	(81)
  a__isLNat(take(V1,V2))	→	a__and(a__isNatural(V1),isLNat(V2))	(23)
  a__U11(X1,X2,X3)	→	U11(X1,X2,X3)	(70)
  a__isNatural(0)	→	tt	(24)
  a__U51(X1,X2,X3)	→	U51(X1,X2,X3)	(76)
  mark(isPLNat(X))	→	a__isPLNat(X)	(57)
  a__U91(tt,XS)	→	mark(XS)	(11)
  a__U81(tt,N,X,XS)	→	a__U82(a__splitAt(mark(N),mark(XS)),X)	(9)
  a__and(tt,X)	→	mark(X)	(13)
  mark(U81(X1,X2,X3,X4))	→	a__U81(mark(X1),X2,X3,X4)	(51)
  a__sel(X1,X2)	→	sel(X1,X2)	(90)
  mark(U11(X1,X2,X3))	→	a__U11(mark(X1),X2,X3)	(40)
  a__U101(X1,X2,X3)	→	U101(X1,X2,X3)	(67)
  mark(isNatural(X))	→	a__isNatural(X)	(55)
  mark(take(X1,X2))	→	a__take(mark(X1),mark(X2))	(59)
  a__U51(tt,N,XS)	→	a__head(a__afterNth(mark(N),mark(XS)))	(6)
  mark(fst(X))	→	a__fst(mark(X))	(38)
  mark(tt)	→	tt	(61)
  mark(tail(X))	→	a__tail(mark(X))	(58)
  a__U41(X1,X2)	→	U41(X1,X2)	(74)
  a__natsFrom(X)	→	natsFrom(X)	(75)
  mark(afterNth(X1,X2))	→	a__afterNth(mark(X1),mark(X2))	(48)
  a__snd(X)	→	snd(X)	(71)
  mark(U91(X1,X2))	→	a__U91(mark(X1),X2)	(53)
  mark(head(X))	→	a__head(mark(X))	(47)
  a__U31(X1,X2)	→	U31(X1,X2)	(73)
  mark(U101(X1,X2,X3))	→	a__U101(mark(X1),X2,X3)	(37)
  mark(snd(X))	→	a__snd(mark(X))	(41)
  mark(U21(X1,X2))	→	a__U21(mark(X1),X2)	(42)
  mark(U51(X1,X2,X3))	→	a__U51(mark(X1),X2,X3)	(46)
  mark(0)	→	0	(66)
  a__U91(X1,X2)	→	U91(X1,X2)	(83)
  a__tail(cons(N,XS))	→	a__U91(a__and(a__isNatural(N),isLNat(XS)),XS)	(35)
  a__isPLNat(splitAt(V1,V2))	→	a__and(a__isNatural(V1),isLNat(V2))	(29)
  mark(U31(X1,X2))	→	a__U31(mark(X1),X2)	(43)
  a__isLNat(X)	→	isLNat(X)	(86)
  a__U11(tt,N,XS)	→	a__snd(a__splitAt(mark(N),mark(XS)))	(2)

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

  a__isLNat#(snd(V1))	→	a__isPLNat#(V1)	(163)
  mark#(afterNth(X1,X2))	→	mark#(X1)	(162)
  a__afterNth#(N,XS)	→	a__isNatural#(N)	(152)
  a__U51#(tt,N,XS)	→	a__head#(a__afterNth(mark(N),mark(XS)))	(150)
  mark#(U51(X1,X2,X3))	→	a__U51#(mark(X1),X2,X3)	(149)
  mark#(sel(X1,X2))	→	mark#(X2)	(146)
  a__afterNth#(N,XS)	→	a__U11#(a__and(a__isNatural(N),isLNat(XS)),N,XS)	(204)
  a__head#(cons(N,XS))	→	a__and#(a__isNatural(N),isLNat(XS))	(143)
  mark#(U91(X1,X2))	→	mark#(X1)	(141)
  mark#(U61(X1,X2))	→	mark#(X1)	(140)
  mark#(afterNth(X1,X2))	→	a__afterNth#(mark(X1),mark(X2))	(139)
  mark#(snd(X))	→	a__snd#(mark(X))	(199)
  mark#(sel(X1,X2))	→	a__sel#(mark(X1),mark(X2))	(138)
  mark#(head(X))	→	mark#(X)	(198)
  mark#(take(X1,X2))	→	mark#(X1)	(197)
  a__sel#(N,XS)	→	a__U51#(a__and(a__isNatural(N),isLNat(XS)),N,XS)	(135)
  a__isLNat#(afterNth(V1,V2))	→	a__isNatural#(V1)	(134)
  mark#(afterNth(X1,X2))	→	mark#(X2)	(192)
  a__tail#(cons(N,XS))	→	a__isNatural#(N)	(133)
  a__tail#(cons(N,XS))	→	a__U91#(a__and(a__isNatural(N),isLNat(XS)),XS)	(132)
  mark#(U51(X1,X2,X3))	→	mark#(X1)	(131)
  a__isLNat#(take(V1,V2))	→	a__isNatural#(V1)	(130)
  a__U51#(tt,N,XS)	→	a__afterNth#(mark(N),mark(XS))	(188)
  mark#(snd(X))	→	mark#(X)	(187)
  mark#(U11(X1,X2,X3))	→	mark#(X1)	(127)
  a__afterNth#(N,XS)	→	a__and#(a__isNatural(N),isLNat(XS))	(125)
  a__head#(cons(N,XS))	→	a__U31#(a__and(a__isNatural(N),isLNat(XS)),N)	(186)
  a__sel#(N,XS)	→	a__isNatural#(N)	(123)
  mark#(U31(X1,X2))	→	mark#(X1)	(122)
  mark#(tail(X))	→	a__tail#(mark(X))	(184)
  a__sel#(N,XS)	→	a__and#(a__isNatural(N),isLNat(XS))	(117)
  a__U51#(tt,N,XS)	→	mark#(XS)	(181)
  a__U91#(tt,XS)	→	mark#(XS)	(112)
  a__isNatural#(head(V1))	→	a__isLNat#(V1)	(111)
  mark#(U91(X1,X2))	→	a__U91#(mark(X1),X2)	(180)
  mark#(tail(X))	→	mark#(X)	(179)
  mark#(U31(X1,X2))	→	a__U31#(mark(X1),X2)	(176)
  a__isLNat#(afterNth(V1,V2))	→	a__and#(a__isNatural(V1),isLNat(V2))	(106)
  a__U51#(tt,N,XS)	→	mark#(N)	(173)
  a__head#(cons(N,XS))	→	a__isNatural#(N)	(170)
  a__isNatural#(sel(V1,V2))	→	a__isNatural#(V1)	(171)
  mark#(sel(X1,X2))	→	mark#(X1)	(101)
  a__isNatural#(sel(V1,V2))	→	a__and#(a__isNatural(V1),isLNat(V2))	(169)
  a__tail#(cons(N,XS))	→	a__and#(a__isNatural(N),isLNat(XS))	(168)
  a__isLNat#(tail(V1))	→	a__isLNat#(V1)	(165)
  mark#(head(X))	→	a__head#(mark(X))	(164)

  could be deleted.

  1.1.1.1 Dependency Graph Processor

  The dependency pairs are split into 2 components.

  • The 1^st component contains the pair

    a__isLNat#(cons(V1,V2))	→	a__and#(a__isNatural(V1),isLNat(V2))	(113)
    mark#(U71(X1,X2))	→	mark#(X1)	(195)
    mark#(U71(X1,X2))	→	a__U71#(mark(X1),X2)	(206)
    a__U71#(tt,XS)	→	mark#(XS)	(121)
    mark#(and(X1,X2))	→	mark#(X1)	(100)
    mark#(and(X1,X2))	→	a__and#(mark(X1),X2)	(104)
    a__U101#(tt,N,XS)	→	mark#(XS)	(118)
    a__U101#(tt,N,XS)	→	mark#(N)	(115)
    a__U101#(tt,N,XS)	→	a__splitAt#(mark(N),mark(XS))	(155)
    a__U101#(tt,N,XS)	→	a__fst#(a__splitAt(mark(N),mark(XS)))	(124)
    a__U21#(tt,X)	→	mark#(X)	(137)
    a__take#(N,XS)	→	a__and#(a__isNatural(N),isLNat(XS))	(157)
    a__take#(N,XS)	→	a__U101#(a__and(a__isNatural(N),isLNat(XS)),N,XS)	(191)
    mark#(s(X))	→	mark#(X)	(209)
    a__isLNat#(fst(V1))	→	a__isPLNat#(V1)	(208)
    a__snd#(pair(X,Y))	→	a__isLNat#(X)	(148)
    a__snd#(pair(X,Y))	→	a__and#(a__isLNat(X),isLNat(Y))	(193)
    a__snd#(pair(X,Y))	→	a__U61#(a__and(a__isLNat(X),isLNat(Y)),Y)	(105)
    a__splitAt#(s(N),cons(X,XS))	→	a__and#(a__isNatural(N),and(isNatural(X),isLNat(XS)))	(128)
    a__splitAt#(s(N),cons(X,XS))	→	a__U81#(a__and(a__isNatural(N),and(isNatural(X),isLNat(XS))),N,X,XS)	(153)
    a__isPLNat#(pair(V1,V2))	→	a__isLNat#(V1)	(183)
    a__isPLNat#(pair(V1,V2))	→	a__and#(a__isLNat(V1),isLNat(V2))	(92)
    mark#(U41(X1,X2))	→	mark#(X1)	(194)
    mark#(U41(X1,X2))	→	a__U41#(mark(X1),X2)	(182)
    a__U41#(tt,N)	→	mark#(N)	(96)
    a__splitAt#(0,XS)	→	a__isLNat#(XS)	(154)
    a__splitAt#(0,XS)	→	a__U71#(a__isLNat(XS),XS)	(142)
    mark#(pair(X1,X2))	→	mark#(X2)	(212)
    mark#(pair(X1,X2))	→	mark#(X1)	(151)
    a__U82#(pair(YS,ZS),X)	→	mark#(ZS)	(144)
    a__U82#(pair(YS,ZS),X)	→	mark#(X)	(201)
    mark#(splitAt(X1,X2))	→	mark#(X2)	(136)
    mark#(splitAt(X1,X2))	→	mark#(X1)	(114)
    mark#(splitAt(X1,X2))	→	a__splitAt#(mark(X1),mark(X2))	(116)
    a__U61#(tt,Y)	→	mark#(Y)	(108)
    mark#(U61(X1,X2))	→	a__U61#(mark(X1),X2)	(147)
    mark#(U82(X1,X2))	→	mark#(X1)	(196)
    mark#(U82(X1,X2))	→	a__U82#(mark(X1),X2)	(126)
    a__natsFrom#(N)	→	a__U41#(a__isNatural(N),N)	(178)
    mark#(cons(X1,X2))	→	mark#(X1)	(172)
    a__fst#(pair(X,Y))	→	a__isLNat#(X)	(190)
    a__fst#(pair(X,Y))	→	a__and#(a__isLNat(X),isLNat(Y))	(158)
    a__fst#(pair(X,Y))	→	a__U21#(a__and(a__isLNat(X),isLNat(Y)),X)	(119)
    mark#(isLNat(X))	→	a__isLNat#(X)	(185)
    mark#(natsFrom(X))	→	mark#(X)	(110)
    mark#(natsFrom(X))	→	a__natsFrom#(mark(X))	(160)
    a__isLNat#(take(V1,V2))	→	a__and#(a__isNatural(V1),isLNat(V2))	(213)
    mark#(isPLNat(X))	→	a__isPLNat#(X)	(161)
    a__U81#(tt,N,X,XS)	→	mark#(XS)	(109)
    a__U81#(tt,N,X,XS)	→	mark#(N)	(98)
    a__U81#(tt,N,X,XS)	→	a__splitAt#(mark(N),mark(XS))	(145)
    a__U81#(tt,N,X,XS)	→	a__U82#(a__splitAt(mark(N),mark(XS)),X)	(177)
    a__and#(tt,X)	→	mark#(X)	(93)
    mark#(U81(X1,X2,X3,X4))	→	mark#(X1)	(99)
    mark#(U81(X1,X2,X3,X4))	→	a__U81#(mark(X1),X2,X3,X4)	(102)
    mark#(U11(X1,X2,X3))	→	a__U11#(mark(X1),X2,X3)	(167)
    mark#(take(X1,X2))	→	mark#(X2)	(103)
    mark#(take(X1,X2))	→	a__take#(mark(X1),mark(X2))	(95)
    mark#(fst(X))	→	mark#(X)	(159)
    mark#(fst(X))	→	a__fst#(mark(X))	(94)
    mark#(U101(X1,X2,X3))	→	mark#(X1)	(189)
    mark#(U101(X1,X2,X3))	→	a__U101#(mark(X1),X2,X3)	(214)
    mark#(U21(X1,X2))	→	mark#(X1)	(207)
    mark#(U21(X1,X2))	→	a__U21#(mark(X1),X2)	(156)
    a__isPLNat#(splitAt(V1,V2))	→	a__and#(a__isNatural(V1),isLNat(V2))	(166)
    a__U11#(tt,N,XS)	→	mark#(XS)	(210)
    a__U11#(tt,N,XS)	→	mark#(N)	(200)
    a__U11#(tt,N,XS)	→	a__splitAt#(mark(N),mark(XS))	(91)
    a__U11#(tt,N,XS)	→	a__snd#(a__splitAt(mark(N),mark(XS)))	(202)

    1.1.1.1.1 Reduction Pair Processor with Usable Rules

    Using the Max-polynomial interpretation

    [U21(x1, x2)]	=	max(x1 + 837, x2 + 6720, 0)
    [a__U82#(x1, x2)]	=	max(x1 + 0, x2 + 25829, 0)
    [a__U71#(x1, x2)]	=	max(x2 + 26672, 0)
    [U11(x1, x2, x3)]	=	max(x1 + 70095, x2 + 70094, x3 + 70092, 0)
    [s(x1)]	=	x1 + 0
    [a__U31#(x1, x2)]	=	max(0)
    [a__head#(x1)]	=	52064
    [a__natsFrom#(x1)]	=	x1 + 14184
    [isPLNat(x1)]	=	13333
    [a__snd#(x1)]	=	x1 + 13332
    [a__afterNth(x1, x2)]	=	max(x1 + 83429, x2 + 83428, 0)
    [U91(x1, x2)]	=	max(x2 + 0, 0)
    [a__U82(x1, x2)]	=	max(x1 + 0, x2 + 26674, 0)
    [take(x1, x2)]	=	max(x1 + 72043, x2 + 72042, 0)
    [U71(x1, x2)]	=	max(x1 + 846, x2 + 13337, 0)
    [and(x1, x2)]	=	max(x1 + 0, x2 + 0, 0)
    [U101(x1, x2, x3)]	=	max(x1 + 58709, x2 + 58708, x3 + 19217, 0)
    [pair(x1, x2)]	=	max(x1 + 842, x2 + 13337, 0)
    [fst(x1)]	=	x1 + 5878
    [natsFrom(x1)]	=	x1 + 14180
    [a__snd(x1)]	=	x1 + 43419
    [a__U51#(x1, x2, x3)]	=	max(0)
    [splitAt(x1, x2)]	=	max(x1 + 26673, x2 + 13339, 0)
    [a__U11#(x1, x2, x3)]	=	max(x2 + 83429, x3 + 83428, 0)
    [a__U31(x1, x2)]	=	max(x1 + 52805, x2 + 52804, 0)
    [a__U51(x1, x2, x3)]	=	max(x1 + 149568, x2 + 149567, x3 + 149566, 0)
    [a__U81(x1,...,x4)]	=	max(x1 + 13340, x2 + 26673, x3 + 26674, x4 + 13339, 0)
    [a__take#(x1, x2)]	=	max(x1 + 40007, x2 + 40007, 0)
    [isNatural(x1)]	=	13333
    [a__U41(x1, x2)]	=	max(x1 + 847, x2 + 14180, 0)
    [a__U21#(x1, x2)]	=	max(x1 + 843, x2 + 14174, 0)
    [a__U81#(x1,...,x4)]	=	max(x1 + 13338, x2 + 26674, x3 + 40010, x4 + 26672, 0)
    [a__U61#(x1, x2)]	=	max(x2 + 13337, 0)
    [a__fst(x1)]	=	x1 + 5878
    [tail(x1)]	=	x1 + 10473
    [a__natsFrom(x1)]	=	x1 + 14180
    [mark#(x1)]	=	x1 + 13336
    [0]	=	26356
    [a__and#(x1, x2)]	=	max(x1 + 845, x2 + 13336, 0)
    [a__isLNat(x1)]	=	13333
    [a__U21(x1, x2)]	=	max(x1 + 837, x2 + 6720, 0)
    [a__U91(x1, x2)]	=	max(x2 + 0, 0)
    [sel(x1, x2)]	=	max(x1 + 162901, x2 + 162902, 0)
    [afterNth(x1, x2)]	=	max(x1 + 83429, x2 + 83428, 0)
    [nil]	=	12496
    [a__splitAt(x1, x2)]	=	max(x1 + 26673, x2 + 13339, 0)
    [isLNat(x1)]	=	13333
    [a__sel#(x1, x2)]	=	max(0)
    [mark(x1)]	=	x1 + 0
    [a__isLNat#(x1)]	=	26669
    [a__U101#(x1, x2, x3)]	=	max(x2 + 40006, x3 + 26674, 0)
    [a__U11(x1, x2, x3)]	=	max(x1 + 70095, x2 + 70094, x3 + 70092, 0)
    [a__sel(x1, x2)]	=	max(x1 + 162901, x2 + 162902, 0)
    [a__isPLNat(x1)]	=	13333
    [U61(x1, x2)]	=	max(x1 + 30928, x2 + 30929, 0)
    [U31(x1, x2)]	=	max(x1 + 52805, x2 + 52804, 0)
    [a__U71(x1, x2)]	=	max(x1 + 846, x2 + 13337, 0)
    [a__isPLNat#(x1)]	=	26669
    [head(x1)]	=	x1 + 66138
    [a__afterNth#(x1, x2)]	=	max(0)
    [a__splitAt#(x1, x2)]	=	max(x1 + 26674, x2 + 26672, 0)
    [cons(x1, x2)]	=	max(x1 + 13339, x2 + 0, 0)
    [a__U61(x1, x2)]	=	max(x1 + 30928, x2 + 30929, 0)
    [snd(x1)]	=	x1 + 43419
    [a__take(x1, x2)]	=	max(x1 + 72043, x2 + 72042, 0)
    [U81(x1,...,x4)]	=	max(x1 + 13340, x2 + 26673, x3 + 26674, x4 + 13339, 0)
    [a__U41#(x1, x2)]	=	max(x2 + 14183, 0)
    [U82(x1, x2)]	=	max(x1 + 0, x2 + 26674, 0)
    [tt]	=	12492
    [a__isNatural(x1)]	=	13333
    [a__isNatural#(x1)]	=	0
    [a__fst#(x1)]	=	x1 + 13333
    [U51(x1, x2, x3)]	=	max(x1 + 149568, x2 + 149567, x3 + 149566, 0)
    [a__and(x1, x2)]	=	max(x1 + 0, x2 + 0, 0)
    [a__tail(x1)]	=	x1 + 10473
    [U41(x1, x2)]	=	max(x1 + 847, x2 + 14180, 0)
    [a__tail#(x1)]	=	49661
    [a__U101(x1, x2, x3)]	=	max(x1 + 58709, x2 + 58708, x3 + 19217, 0)
    [a__U91#(x1, x2)]	=	max(0)
    [a__head(x1)]	=	x1 + 66138

    together with the usable rules

    a__isLNat(cons(V1,V2))	→	a__and(a__isNatural(V1),isLNat(V2))	(18)
    mark(U71(X1,X2))	→	a__U71(mark(X1),X2)	(50)
    a__U71(X1,X2)	→	U71(X1,X2)	(80)
    a__U31(tt,N)	→	mark(N)	(4)
    a__head(cons(N,XS))	→	a__U31(a__and(a__isNatural(N),isLNat(XS)),N)	(15)
    a__U71(tt,XS)	→	pair(nil,mark(XS))	(8)
    mark(and(X1,X2))	→	a__and(mark(X1),X2)	(54)
    a__U101(tt,N,XS)	→	a__fst(a__splitAt(mark(N),mark(XS)))	(1)
    a__head(X)	→	head(X)	(77)
    a__U21(tt,X)	→	mark(X)	(3)
    a__isLNat(nil)	→	tt	(16)
    a__isLNat(snd(V1))	→	a__isPLNat(V1)	(21)
    a__take(N,XS)	→	a__U101(a__and(a__isNatural(N),isLNat(XS)),N,XS)	(36)
    a__fst(X)	→	fst(X)	(68)
    a__isNatural(X)	→	isNatural(X)	(85)
    a__isNatural(s(V1))	→	a__isNatural(V1)	(26)
    mark(s(X))	→	s(mark(X))	(63)
    a__isLNat(fst(V1))	→	a__isPLNat(V1)	(19)
    a__snd(pair(X,Y))	→	a__U61(a__and(a__isLNat(X),isLNat(Y)),Y)	(32)
    a__isLNat(afterNth(V1,V2))	→	a__and(a__isNatural(V1),isLNat(V2))	(17)
    mark(sel(X1,X2))	→	a__sel(mark(X1),mark(X2))	(60)
    a__isNatural(sel(V1,V2))	→	a__and(a__isNatural(V1),isLNat(V2))	(27)
    a__isPLNat(X)	→	isPLNat(X)	(87)
    a__and(X1,X2)	→	and(X1,X2)	(84)
    a__splitAt(s(N),cons(X,XS))	→	a__U81(a__and(a__isNatural(N),and(isNatural(X),isLNat(XS))),N,X,XS)	(34)
    a__isLNat(tail(V1))	→	a__isLNat(V1)	(22)
    a__isPLNat(pair(V1,V2))	→	a__and(a__isLNat(V1),isLNat(V2))	(28)
    mark(nil)	→	nil	(65)
    mark(U41(X1,X2))	→	a__U41(mark(X1),X2)	(44)
    a__U41(tt,N)	→	cons(mark(N),natsFrom(s(N)))	(5)
    a__U21(X1,X2)	→	U21(X1,X2)	(72)
    a__splitAt(0,XS)	→	a__U71(a__isLNat(XS),XS)	(33)
    mark(pair(X1,X2))	→	pair(mark(X1),mark(X2))	(64)
    a__U82(pair(YS,ZS),X)	→	pair(cons(mark(X),YS),mark(ZS))	(10)
    mark(splitAt(X1,X2))	→	a__splitAt(mark(X1),mark(X2))	(39)
    a__U61(tt,Y)	→	mark(Y)	(7)
    a__tail(X)	→	tail(X)	(88)
    a__isLNat(natsFrom(V1))	→	a__isNatural(V1)	(20)
    a__isNatural(head(V1))	→	a__isLNat(V1)	(25)
    mark(U61(X1,X2))	→	a__U61(mark(X1),X2)	(49)
    mark(U82(X1,X2))	→	a__U82(mark(X1),X2)	(52)
    a__natsFrom(N)	→	a__U41(a__isNatural(N),N)	(30)
    mark(cons(X1,X2))	→	cons(mark(X1),X2)	(62)
    a__fst(pair(X,Y))	→	a__U21(a__and(a__isLNat(X),isLNat(Y)),X)	(14)
    a__U82(X1,X2)	→	U82(X1,X2)	(82)
    a__take(X1,X2)	→	take(X1,X2)	(89)
    mark(isLNat(X))	→	a__isLNat(X)	(56)
    a__U61(X1,X2)	→	U61(X1,X2)	(79)
    a__sel(N,XS)	→	a__U51(a__and(a__isNatural(N),isLNat(XS)),N,XS)	(31)
    a__afterNth(N,XS)	→	a__U11(a__and(a__isNatural(N),isLNat(XS)),N,XS)	(12)
    a__splitAt(X1,X2)	→	splitAt(X1,X2)	(69)
    mark(natsFrom(X))	→	a__natsFrom(mark(X))	(45)
    a__afterNth(X1,X2)	→	afterNth(X1,X2)	(78)
    a__U81(X1,X2,X3,X4)	→	U81(X1,X2,X3,X4)	(81)
    a__isLNat(take(V1,V2))	→	a__and(a__isNatural(V1),isLNat(V2))	(23)
    a__U11(X1,X2,X3)	→	U11(X1,X2,X3)	(70)
    a__isNatural(0)	→	tt	(24)
    a__U51(X1,X2,X3)	→	U51(X1,X2,X3)	(76)
    mark(isPLNat(X))	→	a__isPLNat(X)	(57)
    a__U91(tt,XS)	→	mark(XS)	(11)
    a__U81(tt,N,X,XS)	→	a__U82(a__splitAt(mark(N),mark(XS)),X)	(9)
    a__and(tt,X)	→	mark(X)	(13)
    mark(U81(X1,X2,X3,X4))	→	a__U81(mark(X1),X2,X3,X4)	(51)
    a__sel(X1,X2)	→	sel(X1,X2)	(90)
    mark(U11(X1,X2,X3))	→	a__U11(mark(X1),X2,X3)	(40)
    a__U101(X1,X2,X3)	→	U101(X1,X2,X3)	(67)
    mark(isNatural(X))	→	a__isNatural(X)	(55)
    mark(take(X1,X2))	→	a__take(mark(X1),mark(X2))	(59)
    a__U51(tt,N,XS)	→	a__head(a__afterNth(mark(N),mark(XS)))	(6)
    mark(fst(X))	→	a__fst(mark(X))	(38)
    mark(tt)	→	tt	(61)
    mark(tail(X))	→	a__tail(mark(X))	(58)
    a__U41(X1,X2)	→	U41(X1,X2)	(74)
    a__natsFrom(X)	→	natsFrom(X)	(75)
    mark(afterNth(X1,X2))	→	a__afterNth(mark(X1),mark(X2))	(48)
    a__snd(X)	→	snd(X)	(71)
    mark(U91(X1,X2))	→	a__U91(mark(X1),X2)	(53)
    mark(head(X))	→	a__head(mark(X))	(47)
    a__U31(X1,X2)	→	U31(X1,X2)	(73)
    mark(U101(X1,X2,X3))	→	a__U101(mark(X1),X2,X3)	(37)
    mark(snd(X))	→	a__snd(mark(X))	(41)
    mark(U21(X1,X2))	→	a__U21(mark(X1),X2)	(42)
    mark(U51(X1,X2,X3))	→	a__U51(mark(X1),X2,X3)	(46)
    mark(0)	→	0	(66)
    a__U91(X1,X2)	→	U91(X1,X2)	(83)
    a__tail(cons(N,XS))	→	a__U91(a__and(a__isNatural(N),isLNat(XS)),XS)	(35)
    a__isPLNat(splitAt(V1,V2))	→	a__and(a__isNatural(V1),isLNat(V2))	(29)
    mark(U31(X1,X2))	→	a__U31(mark(X1),X2)	(43)
    a__isLNat(X)	→	isLNat(X)	(86)
    a__U11(tt,N,XS)	→	a__snd(a__splitAt(mark(N),mark(XS)))	(2)

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

    mark#(U71(X1,X2))	→	mark#(X1)	(195)
    mark#(U71(X1,X2))	→	a__U71#(mark(X1),X2)	(206)
    a__U71#(tt,XS)	→	mark#(XS)	(121)
    a__U101#(tt,N,XS)	→	mark#(XS)	(118)
    a__U101#(tt,N,XS)	→	mark#(N)	(115)
    a__U101#(tt,N,XS)	→	a__splitAt#(mark(N),mark(XS))	(155)
    a__U21#(tt,X)	→	mark#(X)	(137)
    a__take#(N,XS)	→	a__and#(a__isNatural(N),isLNat(XS))	(157)
    a__take#(N,XS)	→	a__U101#(a__and(a__isNatural(N),isLNat(XS)),N,XS)	(191)
    a__snd#(pair(X,Y))	→	a__U61#(a__and(a__isLNat(X),isLNat(Y)),Y)	(105)
    a__splitAt#(s(N),cons(X,XS))	→	a__and#(a__isNatural(N),and(isNatural(X),isLNat(XS)))	(128)
    mark#(U41(X1,X2))	→	mark#(X1)	(194)
    mark#(U41(X1,X2))	→	a__U41#(mark(X1),X2)	(182)
    a__U41#(tt,N)	→	mark#(N)	(96)
    a__splitAt#(0,XS)	→	a__isLNat#(XS)	(154)
    mark#(pair(X1,X2))	→	mark#(X2)	(212)
    mark#(pair(X1,X2))	→	mark#(X1)	(151)
    a__U82#(pair(YS,ZS),X)	→	mark#(ZS)	(144)
    a__U82#(pair(YS,ZS),X)	→	mark#(X)	(201)
    mark#(splitAt(X1,X2))	→	mark#(X2)	(136)
    mark#(splitAt(X1,X2))	→	mark#(X1)	(114)
    mark#(splitAt(X1,X2))	→	a__splitAt#(mark(X1),mark(X2))	(116)
    a__U61#(tt,Y)	→	mark#(Y)	(108)
    mark#(U61(X1,X2))	→	a__U61#(mark(X1),X2)	(147)
    mark#(U82(X1,X2))	→	a__U82#(mark(X1),X2)	(126)
    a__natsFrom#(N)	→	a__U41#(a__isNatural(N),N)	(178)
    mark#(cons(X1,X2))	→	mark#(X1)	(172)
    a__fst#(pair(X,Y))	→	a__isLNat#(X)	(190)
    a__fst#(pair(X,Y))	→	a__and#(a__isLNat(X),isLNat(Y))	(158)
    a__fst#(pair(X,Y))	→	a__U21#(a__and(a__isLNat(X),isLNat(Y)),X)	(119)
    mark#(natsFrom(X))	→	mark#(X)	(110)
    mark#(natsFrom(X))	→	a__natsFrom#(mark(X))	(160)
    a__U81#(tt,N,X,XS)	→	mark#(XS)	(109)
    a__U81#(tt,N,X,XS)	→	mark#(N)	(98)
    a__U81#(tt,N,X,XS)	→	a__U82#(a__splitAt(mark(N),mark(XS)),X)	(177)
    mark#(U81(X1,X2,X3,X4))	→	mark#(X1)	(99)
    mark#(take(X1,X2))	→	mark#(X2)	(103)
    mark#(take(X1,X2))	→	a__take#(mark(X1),mark(X2))	(95)
    mark#(fst(X))	→	mark#(X)	(159)
    mark#(fst(X))	→	a__fst#(mark(X))	(94)
    mark#(U101(X1,X2,X3))	→	mark#(X1)	(189)
    mark#(U101(X1,X2,X3))	→	a__U101#(mark(X1),X2,X3)	(214)
    mark#(U21(X1,X2))	→	mark#(X1)	(207)
    mark#(U21(X1,X2))	→	a__U21#(mark(X1),X2)	(156)
    a__U11#(tt,N,XS)	→	mark#(XS)	(210)
    a__U11#(tt,N,XS)	→	mark#(N)	(200)
    a__U11#(tt,N,XS)	→	a__splitAt#(mark(N),mark(XS))	(91)
    a__U11#(tt,N,XS)	→	a__snd#(a__splitAt(mark(N),mark(XS)))	(202)

    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

      a__isLNat#(cons(V1,V2))	→	a__and#(a__isNatural(V1),isLNat(V2))	(113)
      mark#(and(X1,X2))	→	mark#(X1)	(100)
      mark#(and(X1,X2))	→	a__and#(mark(X1),X2)	(104)
      mark#(s(X))	→	mark#(X)	(209)
      a__isLNat#(fst(V1))	→	a__isPLNat#(V1)	(208)
      a__isPLNat#(pair(V1,V2))	→	a__isLNat#(V1)	(183)
      a__isPLNat#(pair(V1,V2))	→	a__and#(a__isLNat(V1),isLNat(V2))	(92)
      mark#(U82(X1,X2))	→	mark#(X1)	(196)
      mark#(isLNat(X))	→	a__isLNat#(X)	(185)
      a__isLNat#(take(V1,V2))	→	a__and#(a__isNatural(V1),isLNat(V2))	(213)
      mark#(isPLNat(X))	→	a__isPLNat#(X)	(161)
      a__and#(tt,X)	→	mark#(X)	(93)
      a__isPLNat#(splitAt(V1,V2))	→	a__and#(a__isNatural(V1),isLNat(V2))	(166)

      1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

      Using the Max-polynomial interpretation

      [U21(x1, x2)]	=	x2 + 15663
      [a__U82#(x1, x2)]	=	0
      [a__U71#(x1, x2)]	=	0
      [U11(x1, x2, x3)]	=	x1 + x3 + 16283
      [s(x1)]	=	x1 + 1
      [a__U31#(x1, x2)]	=	2
      [a__head#(x1)]	=	2
      [a__natsFrom#(x1)]	=	0
      [isPLNat(x1)]	=	x1 + 56387
      [a__snd#(x1)]	=	0
      [a__afterNth(x1, x2)]	=	16281
      [U91(x1, x2)]	=	14047
      [a__U82(x1, x2)]	=	15668
      [take(x1, x2)]	=	x2 + 15657
      [U71(x1, x2)]	=	x2 + 2
      [and(x1, x2)]	=	x1 + x2 + 15664
      [U101(x1, x2, x3)]	=	x1 + x2 + 15658
      [pair(x1, x2)]	=	x1 + x2 + 13209
      [fst(x1)]	=	x1 + 15659
      [natsFrom(x1)]	=	52892
      [a__snd(x1)]	=	16283
      [a__U51#(x1, x2, x3)]	=	0
      [splitAt(x1, x2)]	=	x1 + x2 + 1
      [a__U11#(x1, x2, x3)]	=	0
      [a__U31(x1, x2)]	=	4385
      [a__U51(x1, x2, x3)]	=	x1 + 4382
      [a__U81(x1,...,x4)]	=	x2 + x4 + 15667
      [a__take#(x1, x2)]	=	0
      [isNatural(x1)]	=	x1 + 40720
      [a__U41(x1, x2)]	=	68558
      [a__U21#(x1, x2)]	=	0
      [a__U81#(x1,...,x4)]	=	1
      [a__U61#(x1, x2)]	=	0
      [a__fst(x1)]	=	31324
      [tail(x1)]	=	x1 + 14043
      [a__natsFrom(x1)]	=	68557
      [mark#(x1)]	=	x1 + 0
      [0]	=	8907
      [a__and#(x1, x2)]	=	x2 + 15655
      [a__isLNat(x1)]	=	56385
      [a__U21(x1, x2)]	=	x1 + 15662
      [a__U91(x1, x2)]	=	x1 + x2 + 14046
      [sel(x1, x2)]	=	x1 + x2 + 4379
      [afterNth(x1, x2)]	=	x2 + 616
      [nil]	=	0
      [a__splitAt(x1, x2)]	=	15666
      [isLNat(x1)]	=	x1 + 40720
      [a__sel#(x1, x2)]	=	2
      [mark(x1)]	=	x1 + 15664
      [a__isLNat#(x1)]	=	x1 + 40719
      [a__U101#(x1, x2, x3)]	=	0
      [a__U11(x1, x2, x3)]	=	16282
      [a__sel(x1, x2)]	=	20044
      [a__isPLNat(x1)]	=	x1 + 56386
      [U61(x1, x2)]	=	x2 + 15663
      [U31(x1, x2)]	=	x1 + 4386
      [a__U71(x1, x2)]	=	15667
      [a__isPLNat#(x1)]	=	x1 + 56375
      [head(x1)]	=	4385
      [a__afterNth#(x1, x2)]	=	2
      [a__splitAt#(x1, x2)]	=	0
      [cons(x1, x2)]	=	x2 + 15667
      [a__U61(x1, x2)]	=	x1 + 15662
      [snd(x1)]	=	x1 + 48
      [a__take(x1, x2)]	=	31322
      [U81(x1,...,x4)]	=	x1 + x3 + 15668
      [a__U41#(x1, x2)]	=	0
      [U82(x1, x2)]	=	x1 + x2 + 15669
      [tt]	=	1
      [a__isNatural(x1)]	=	56386
      [a__isNatural#(x1)]	=	2
      [a__fst#(x1)]	=	0
      [U51(x1, x2, x3)]	=	x2 + x3 + 4383
      [a__and(x1, x2)]	=	15663
      [a__tail(x1)]	=	29708
      [U41(x1, x2)]	=	68559
      [a__tail#(x1)]	=	2
      [a__U101(x1, x2, x3)]	=	x2 + x3 + 31323
      [a__U91#(x1, x2)]	=	2
      [a__head(x1)]	=	4384

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

      a__isLNat#(cons(V1,V2))	→	a__and#(a__isNatural(V1),isLNat(V2))	(113)
      mark#(and(X1,X2))	→	mark#(X1)	(100)
      mark#(and(X1,X2))	→	a__and#(mark(X1),X2)	(104)
      mark#(s(X))	→	mark#(X)	(209)
      a__isLNat#(fst(V1))	→	a__isPLNat#(V1)	(208)
      a__isPLNat#(pair(V1,V2))	→	a__isLNat#(V1)	(183)
      a__isPLNat#(pair(V1,V2))	→	a__and#(a__isLNat(V1),isLNat(V2))	(92)
      mark#(U82(X1,X2))	→	mark#(X1)	(196)
      mark#(isLNat(X))	→	a__isLNat#(X)	(185)
      a__isLNat#(take(V1,V2))	→	a__and#(a__isNatural(V1),isLNat(V2))	(213)
      mark#(isPLNat(X))	→	a__isPLNat#(X)	(161)
      a__and#(tt,X)	→	mark#(X)	(93)
      a__isPLNat#(splitAt(V1,V2))	→	a__and#(a__isNatural(V1),isLNat(V2))	(166)

      could be deleted.

      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__splitAt#(s(N),cons(X,XS))	→	a__U81#(a__and(a__isNatural(N),and(isNatural(X),isLNat(XS))),N,X,XS)	(153)
      a__U81#(tt,N,X,XS)	→	a__splitAt#(mark(N),mark(XS))	(145)

      1.1.1.1.1.1.2 Reduction Pair Processor with Usable Rules

      Using the argument filter

      π(a__U71#)	=	1
      π(a__snd#)	=	1
      π(and)	=	2
      π(a__U11#)	=	1
      π(a__sel#)	=	2
      π(mark)	=	1
      π(a__isNatural#)	=	1
      π(a__and)	=	2

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

      prec(U21)	=	7		status(U21)	=	[]		list-extension(U21)	=	Lex
      prec(a__U82#)	=	0		status(a__U82#)	=	[1, 2]		list-extension(a__U82#)	=	Lex
      prec(U11)	=	2		status(U11)	=	[]		list-extension(U11)	=	Lex
      prec(s)	=	13		status(s)	=	[1]		list-extension(s)	=	Lex
      prec(a__U31#)	=	0		status(a__U31#)	=	[2, 1]		list-extension(a__U31#)	=	Lex
      prec(a__head#)	=	0		status(a__head#)	=	[]		list-extension(a__head#)	=	Lex
      prec(a__natsFrom#)	=	0		status(a__natsFrom#)	=	[]		list-extension(a__natsFrom#)	=	Lex
      prec(isPLNat)	=	11		status(isPLNat)	=	[1]		list-extension(isPLNat)	=	Lex
      prec(a__afterNth)	=	3		status(a__afterNth)	=	[]		list-extension(a__afterNth)	=	Lex
      prec(U91)	=	0		status(U91)	=	[]		list-extension(U91)	=	Lex
      prec(a__U82)	=	2		status(a__U82)	=	[]		list-extension(a__U82)	=	Lex
      prec(take)	=	14		status(take)	=	[]		list-extension(take)	=	Lex
      prec(U71)	=	1		status(U71)	=	[1]		list-extension(U71)	=	Lex
      prec(U101)	=	13		status(U101)	=	[]		list-extension(U101)	=	Lex
      prec(pair)	=	1		status(pair)	=	[]		list-extension(pair)	=	Lex
      prec(fst)	=	12		status(fst)	=	[]		list-extension(fst)	=	Lex
      prec(natsFrom)	=	15		status(natsFrom)	=	[]		list-extension(natsFrom)	=	Lex
      prec(a__snd)	=	1		status(a__snd)	=	[]		list-extension(a__snd)	=	Lex
      prec(a__U51#)	=	0		status(a__U51#)	=	[1, 2, 3]		list-extension(a__U51#)	=	Lex
      prec(splitAt)	=	4		status(splitAt)	=	[]		list-extension(splitAt)	=	Lex
      prec(a__U31)	=	0		status(a__U31)	=	[2]		list-extension(a__U31)	=	Lex
      prec(a__U51)	=	6		status(a__U51)	=	[]		list-extension(a__U51)	=	Lex
      prec(a__U81)	=	3		status(a__U81)	=	[1, 3, 4]		list-extension(a__U81)	=	Lex
      prec(a__take#)	=	0		status(a__take#)	=	[2]		list-extension(a__take#)	=	Lex
      prec(isNatural)	=	10		status(isNatural)	=	[]		list-extension(isNatural)	=	Lex
      prec(a__U41)	=	14		status(a__U41)	=	[2]		list-extension(a__U41)	=	Lex
      prec(a__U21#)	=	0		status(a__U21#)	=	[1, 2]		list-extension(a__U21#)	=	Lex
      prec(a__U81#)	=	12		status(a__U81#)	=	[2]		list-extension(a__U81#)	=	Lex
      prec(a__U61#)	=	0		status(a__U61#)	=	[1, 2]		list-extension(a__U61#)	=	Lex
      prec(a__fst)	=	12		status(a__fst)	=	[]		list-extension(a__fst)	=	Lex
      prec(tail)	=	9		status(tail)	=	[1]		list-extension(tail)	=	Lex
      prec(a__natsFrom)	=	15		status(a__natsFrom)	=	[]		list-extension(a__natsFrom)	=	Lex
      prec(mark#)	=	0		status(mark#)	=	[]		list-extension(mark#)	=	Lex
      prec(0)	=	8		status(0)	=	[]		list-extension(0)	=	Lex
      prec(a__and#)	=	0		status(a__and#)	=	[2, 1]		list-extension(a__and#)	=	Lex
      prec(a__isLNat)	=	9		status(a__isLNat)	=	[]		list-extension(a__isLNat)	=	Lex
      prec(a__U21)	=	7		status(a__U21)	=	[]		list-extension(a__U21)	=	Lex
      prec(a__U91)	=	0		status(a__U91)	=	[]		list-extension(a__U91)	=	Lex
      prec(sel)	=	9		status(sel)	=	[1]		list-extension(sel)	=	Lex
      prec(afterNth)	=	3		status(afterNth)	=	[]		list-extension(afterNth)	=	Lex
      prec(nil)	=	7		status(nil)	=	[]		list-extension(nil)	=	Lex
      prec(a__splitAt)	=	4		status(a__splitAt)	=	[]		list-extension(a__splitAt)	=	Lex
      prec(isLNat)	=	9		status(isLNat)	=	[]		list-extension(isLNat)	=	Lex
      prec(a__isLNat#)	=	0		status(a__isLNat#)	=	[]		list-extension(a__isLNat#)	=	Lex
      prec(a__U101#)	=	0		status(a__U101#)	=	[2, 3]		list-extension(a__U101#)	=	Lex
      prec(a__U11)	=	2		status(a__U11)	=	[]		list-extension(a__U11)	=	Lex
      prec(a__sel)	=	9		status(a__sel)	=	[1]		list-extension(a__sel)	=	Lex
      prec(a__isPLNat)	=	11		status(a__isPLNat)	=	[1]		list-extension(a__isPLNat)	=	Lex
      prec(U61)	=	0		status(U61)	=	[1]		list-extension(U61)	=	Lex
      prec(U31)	=	0		status(U31)	=	[2]		list-extension(U31)	=	Lex
      prec(a__U71)	=	1		status(a__U71)	=	[1]		list-extension(a__U71)	=	Lex
      prec(a__isPLNat#)	=	0		status(a__isPLNat#)	=	[]		list-extension(a__isPLNat#)	=	Lex
      prec(head)	=	1		status(head)	=	[]		list-extension(head)	=	Lex
      prec(a__afterNth#)	=	0		status(a__afterNth#)	=	[2, 1]		list-extension(a__afterNth#)	=	Lex
      prec(a__splitAt#)	=	12		status(a__splitAt#)	=	[1]		list-extension(a__splitAt#)	=	Lex
      prec(cons)	=	13		status(cons)	=	[1]		list-extension(cons)	=	Lex
      prec(a__U61)	=	0		status(a__U61)	=	[1]		list-extension(a__U61)	=	Lex
      prec(snd)	=	1		status(snd)	=	[]		list-extension(snd)	=	Lex
      prec(a__take)	=	14		status(a__take)	=	[]		list-extension(a__take)	=	Lex
      prec(U81)	=	3		status(U81)	=	[1, 3, 4]		list-extension(U81)	=	Lex
      prec(a__U41#)	=	0		status(a__U41#)	=	[1, 2]		list-extension(a__U41#)	=	Lex
      prec(U82)	=	2		status(U82)	=	[]		list-extension(U82)	=	Lex
      prec(tt)	=	11		status(tt)	=	[]		list-extension(tt)	=	Lex
      prec(a__isNatural)	=	10		status(a__isNatural)	=	[]		list-extension(a__isNatural)	=	Lex
      prec(a__fst#)	=	0		status(a__fst#)	=	[]		list-extension(a__fst#)	=	Lex
      prec(U51)	=	6		status(U51)	=	[]		list-extension(U51)	=	Lex
      prec(a__tail)	=	9		status(a__tail)	=	[1]		list-extension(a__tail)	=	Lex
      prec(U41)	=	14		status(U41)	=	[2]		list-extension(U41)	=	Lex
      prec(a__tail#)	=	0		status(a__tail#)	=	[]		list-extension(a__tail#)	=	Lex
      prec(a__U101)	=	13		status(a__U101)	=	[]		list-extension(a__U101)	=	Lex
      prec(a__U91#)	=	0		status(a__U91#)	=	[2, 1]		list-extension(a__U91#)	=	Lex
      prec(a__head)	=	1		status(a__head)	=	[]		list-extension(a__head)	=	Lex

      and the following Max-polynomial interpretation

      [U21(x1, x2)]	=	max(x2 + 9, 0)
      [a__U82#(x1, x2)]	=	x1 + x2 + 0
      [U11(x1, x2, x3)]	=	max(x1 + 16, x3 + 15, 0)
      [s(x1)]	=	x1 + 0
      [a__U31#(x1, x2)]	=	x1 + x2 + 1
      [a__head#(x1)]	=	1
      [a__natsFrom#(x1)]	=	1
      [isPLNat(x1)]	=	x1 + 3
      [a__afterNth(x1, x2)]	=	max(x2 + 20, 0)
      [U91(x1, x2)]	=	max(x2 + 12, 0)
      [a__U82(x1, x2)]	=	max(x1 + 0, x2 + 17, 0)
      [take(x1, x2)]	=	x1 + x2 + 20
      [U71(x1, x2)]	=	max(x1 + 8, x2 + 10, 0)
      [U101(x1, x2, x3)]	=	max(x1 + 14, x2 + 15, x3 + 20, 0)
      [pair(x1, x2)]	=	max(x1 + 6, x2 + 4, 0)
      [fst(x1)]	=	x1 + 4
      [natsFrom(x1)]	=	x1 + 20
      [a__snd(x1)]	=	x1 + 4
      [a__U51#(x1, x2, x3)]	=	x1 + x2 + x3 + 1
      [splitAt(x1, x2)]	=	max(x2 + 10, 0)
      [a__U31(x1, x2)]	=	max(x2 + 12, 0)
      [a__U51(x1, x2, x3)]	=	max(x1 + 44, x3 + 43, 0)
      [a__U81(x1,...,x4)]	=	max(x1 + 0, x3 + 18, x4 + 10, 0)
      [a__take#(x1, x2)]	=	x2 + 1
      [isNatural(x1)]	=	x1 + 21
      [a__U41(x1, x2)]	=	max(x2 + 20, 0)
      [a__U21#(x1, x2)]	=	x1 + x2 + 1
      [a__U81#(x1,...,x4)]	=	max(x2 + 0, 0)
      [a__U61#(x1, x2)]	=	x1 + x2 + 1
      [a__fst(x1)]	=	x1 + 4
      [tail(x1)]	=	x1 + 22
      [a__natsFrom(x1)]	=	x1 + 20
      [mark#(x1)]	=	1
      [0]	=	9
      [a__and#(x1, x2)]	=	max(x1 + 1, x2 + 1, 0)
      [a__isLNat(x1)]	=	x1 + 2
      [a__U21(x1, x2)]	=	max(x2 + 9, 0)
      [a__U91(x1, x2)]	=	max(x2 + 12, 0)
      [sel(x1, x2)]	=	x1 + x2 + 47
      [afterNth(x1, x2)]	=	max(x2 + 20, 0)
      [nil]	=	2
      [a__splitAt(x1, x2)]	=	max(x2 + 10, 0)
      [isLNat(x1)]	=	x1 + 2
      [a__isLNat#(x1)]	=	1
      [a__U101#(x1, x2, x3)]	=	x2 + x3 + 1
      [a__U11(x1, x2, x3)]	=	max(x1 + 16, x3 + 15, 0)
      [a__sel(x1, x2)]	=	x1 + x2 + 47
      [a__isPLNat(x1)]	=	x1 + 3
      [U61(x1, x2)]	=	max(x1 + 1, x2 + 2, 0)
      [U31(x1, x2)]	=	max(x2 + 12, 0)
      [a__U71(x1, x2)]	=	max(x1 + 8, x2 + 10, 0)
      [a__isPLNat#(x1)]	=	1
      [head(x1)]	=	x1 + 22
      [a__afterNth#(x1, x2)]	=	x1 + x2 + 1
      [a__splitAt#(x1, x2)]	=	max(x1 + 0, 0)
      [cons(x1, x2)]	=	max(x1 + 11, x2 + 0, 0)
      [a__U61(x1, x2)]	=	max(x1 + 1, x2 + 2, 0)
      [snd(x1)]	=	x1 + 4
      [a__take(x1, x2)]	=	x1 + x2 + 20
      [U81(x1,...,x4)]	=	max(x1 + 0, x3 + 18, x4 + 10, 0)
      [a__U41#(x1, x2)]	=	x1 + x2 + 1
      [U82(x1, x2)]	=	max(x1 + 0, x2 + 17, 0)
      [tt]	=	1
      [a__isNatural(x1)]	=	x1 + 21
      [a__fst#(x1)]	=	1
      [U51(x1, x2, x3)]	=	max(x1 + 44, x3 + 43, 0)
      [a__tail(x1)]	=	x1 + 22
      [U41(x1, x2)]	=	max(x2 + 20, 0)
      [a__tail#(x1)]	=	1
      [a__U101(x1, x2, x3)]	=	max(x1 + 14, x2 + 15, x3 + 20, 0)
      [a__U91#(x1, x2)]	=	x1 + x2 + 1
      [a__head(x1)]	=	x1 + 22

      together with the usable rules

      a__isLNat(cons(V1,V2))	→	a__and(a__isNatural(V1),isLNat(V2))	(18)
      mark(U71(X1,X2))	→	a__U71(mark(X1),X2)	(50)
      a__U71(X1,X2)	→	U71(X1,X2)	(80)
      a__U31(tt,N)	→	mark(N)	(4)
      a__head(cons(N,XS))	→	a__U31(a__and(a__isNatural(N),isLNat(XS)),N)	(15)
      a__U71(tt,XS)	→	pair(nil,mark(XS))	(8)
      mark(and(X1,X2))	→	a__and(mark(X1),X2)	(54)
      a__U101(tt,N,XS)	→	a__fst(a__splitAt(mark(N),mark(XS)))	(1)
      a__head(X)	→	head(X)	(77)
      a__U21(tt,X)	→	mark(X)	(3)
      a__isLNat(nil)	→	tt	(16)
      a__isLNat(snd(V1))	→	a__isPLNat(V1)	(21)
      a__take(N,XS)	→	a__U101(a__and(a__isNatural(N),isLNat(XS)),N,XS)	(36)
      a__fst(X)	→	fst(X)	(68)
      a__isNatural(X)	→	isNatural(X)	(85)
      a__isNatural(s(V1))	→	a__isNatural(V1)	(26)
      mark(s(X))	→	s(mark(X))	(63)
      a__isLNat(fst(V1))	→	a__isPLNat(V1)	(19)
      a__snd(pair(X,Y))	→	a__U61(a__and(a__isLNat(X),isLNat(Y)),Y)	(32)
      a__isLNat(afterNth(V1,V2))	→	a__and(a__isNatural(V1),isLNat(V2))	(17)
      mark(sel(X1,X2))	→	a__sel(mark(X1),mark(X2))	(60)
      a__isNatural(sel(V1,V2))	→	a__and(a__isNatural(V1),isLNat(V2))	(27)
      a__isPLNat(X)	→	isPLNat(X)	(87)
      a__and(X1,X2)	→	and(X1,X2)	(84)
      a__splitAt(s(N),cons(X,XS))	→	a__U81(a__and(a__isNatural(N),and(isNatural(X),isLNat(XS))),N,X,XS)	(34)
      a__isLNat(tail(V1))	→	a__isLNat(V1)	(22)
      a__isPLNat(pair(V1,V2))	→	a__and(a__isLNat(V1),isLNat(V2))	(28)
      mark(nil)	→	nil	(65)
      mark(U41(X1,X2))	→	a__U41(mark(X1),X2)	(44)
      a__U41(tt,N)	→	cons(mark(N),natsFrom(s(N)))	(5)
      a__U21(X1,X2)	→	U21(X1,X2)	(72)
      a__splitAt(0,XS)	→	a__U71(a__isLNat(XS),XS)	(33)
      mark(pair(X1,X2))	→	pair(mark(X1),mark(X2))	(64)
      a__U82(pair(YS,ZS),X)	→	pair(cons(mark(X),YS),mark(ZS))	(10)
      mark(splitAt(X1,X2))	→	a__splitAt(mark(X1),mark(X2))	(39)
      a__U61(tt,Y)	→	mark(Y)	(7)
      a__tail(X)	→	tail(X)	(88)
      a__isLNat(natsFrom(V1))	→	a__isNatural(V1)	(20)
      a__isNatural(head(V1))	→	a__isLNat(V1)	(25)
      mark(U61(X1,X2))	→	a__U61(mark(X1),X2)	(49)
      mark(U82(X1,X2))	→	a__U82(mark(X1),X2)	(52)
      a__natsFrom(N)	→	a__U41(a__isNatural(N),N)	(30)
      mark(cons(X1,X2))	→	cons(mark(X1),X2)	(62)
      a__fst(pair(X,Y))	→	a__U21(a__and(a__isLNat(X),isLNat(Y)),X)	(14)
      a__U82(X1,X2)	→	U82(X1,X2)	(82)
      a__take(X1,X2)	→	take(X1,X2)	(89)
      mark(isLNat(X))	→	a__isLNat(X)	(56)
      a__U61(X1,X2)	→	U61(X1,X2)	(79)
      a__sel(N,XS)	→	a__U51(a__and(a__isNatural(N),isLNat(XS)),N,XS)	(31)
      a__afterNth(N,XS)	→	a__U11(a__and(a__isNatural(N),isLNat(XS)),N,XS)	(12)
      a__splitAt(X1,X2)	→	splitAt(X1,X2)	(69)
      mark(natsFrom(X))	→	a__natsFrom(mark(X))	(45)
      a__afterNth(X1,X2)	→	afterNth(X1,X2)	(78)
      a__U81(X1,X2,X3,X4)	→	U81(X1,X2,X3,X4)	(81)
      a__isLNat(take(V1,V2))	→	a__and(a__isNatural(V1),isLNat(V2))	(23)
      a__U11(X1,X2,X3)	→	U11(X1,X2,X3)	(70)
      a__isNatural(0)	→	tt	(24)
      a__U51(X1,X2,X3)	→	U51(X1,X2,X3)	(76)
      mark(isPLNat(X))	→	a__isPLNat(X)	(57)
      a__U91(tt,XS)	→	mark(XS)	(11)
      a__U81(tt,N,X,XS)	→	a__U82(a__splitAt(mark(N),mark(XS)),X)	(9)
      a__and(tt,X)	→	mark(X)	(13)
      mark(U81(X1,X2,X3,X4))	→	a__U81(mark(X1),X2,X3,X4)	(51)
      a__sel(X1,X2)	→	sel(X1,X2)	(90)
      mark(U11(X1,X2,X3))	→	a__U11(mark(X1),X2,X3)	(40)
      a__U101(X1,X2,X3)	→	U101(X1,X2,X3)	(67)
      mark(isNatural(X))	→	a__isNatural(X)	(55)
      mark(take(X1,X2))	→	a__take(mark(X1),mark(X2))	(59)
      a__U51(tt,N,XS)	→	a__head(a__afterNth(mark(N),mark(XS)))	(6)
      mark(fst(X))	→	a__fst(mark(X))	(38)
      mark(tt)	→	tt	(61)
      mark(tail(X))	→	a__tail(mark(X))	(58)
      a__U41(X1,X2)	→	U41(X1,X2)	(74)
      a__natsFrom(X)	→	natsFrom(X)	(75)
      mark(afterNth(X1,X2))	→	a__afterNth(mark(X1),mark(X2))	(48)
      a__snd(X)	→	snd(X)	(71)
      mark(U91(X1,X2))	→	a__U91(mark(X1),X2)	(53)
      mark(head(X))	→	a__head(mark(X))	(47)
      a__U31(X1,X2)	→	U31(X1,X2)	(73)
      mark(U101(X1,X2,X3))	→	a__U101(mark(X1),X2,X3)	(37)
      mark(snd(X))	→	a__snd(mark(X))	(41)
      mark(U21(X1,X2))	→	a__U21(mark(X1),X2)	(42)
      mark(U51(X1,X2,X3))	→	a__U51(mark(X1),X2,X3)	(46)
      mark(0)	→	0	(66)
      a__U91(X1,X2)	→	U91(X1,X2)	(83)
      a__tail(cons(N,XS))	→	a__U91(a__and(a__isNatural(N),isLNat(XS)),XS)	(35)
      a__isPLNat(splitAt(V1,V2))	→	a__and(a__isNatural(V1),isLNat(V2))	(29)
      mark(U31(X1,X2))	→	a__U31(mark(X1),X2)	(43)
      a__isLNat(X)	→	isLNat(X)	(86)
      a__U11(tt,N,XS)	→	a__snd(a__splitAt(mark(N),mark(XS)))	(2)

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

      a__splitAt#(s(N),cons(X,XS))

      →

      a__U81#(a__and(a__isNatural(N),and(isNatural(X),isLNat(XS))),N,X,XS)

      (153)

      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__isNatural#(s(V1))

    →

    a__isNatural#(V1)

    (211)

    1.1.1.1.2 Reduction Pair Processor with Usable Rules

    Using the Max-polynomial interpretation

    [U21(x1, x2)]	=	x2 + 1
    [a__U82#(x1, x2)]	=	0
    [a__U71#(x1, x2)]	=	0
    [U11(x1, x2, x3)]	=	5579
    [s(x1)]	=	x1 + 6310
    [a__U31#(x1, x2)]	=	2
    [a__head#(x1)]	=	2
    [a__natsFrom#(x1)]	=	0
    [isPLNat(x1)]	=	15269
    [a__snd#(x1)]	=	0
    [a__afterNth(x1, x2)]	=	x2 + 4171
    [U91(x1, x2)]	=	x2 + 1
    [a__U82(x1, x2)]	=	2
    [take(x1, x2)]	=	x1 + 6264
    [U71(x1, x2)]	=	x2 + 5
    [and(x1, x2)]	=	x2 + 4
    [U101(x1, x2, x3)]	=	x3 + 6
    [pair(x1, x2)]	=	x1 + 1
    [fst(x1)]	=	4
    [natsFrom(x1)]	=	199
    [a__snd(x1)]	=	15266
    [a__U51#(x1, x2, x3)]	=	0
    [splitAt(x1, x2)]	=	x2 + 2
    [a__U11#(x1, x2, x3)]	=	0
    [a__U31(x1, x2)]	=	x1 + 1
    [a__U51(x1, x2, x3)]	=	x1 + x2 + 0
    [a__U81(x1,...,x4)]	=	x1 + x2 + x4 + 0
    [a__take#(x1, x2)]	=	0
    [isNatural(x1)]	=	x1 + 5436
    [a__U41(x1, x2)]	=	x1 + 4
    [a__U21#(x1, x2)]	=	0
    [a__U81#(x1,...,x4)]	=	0
    [a__U61#(x1, x2)]	=	0
    [a__fst(x1)]	=	x1 + 5
    [tail(x1)]	=	4601
    [a__natsFrom(x1)]	=	204
    [mark#(x1)]	=	0
    [0]	=	8
    [a__and#(x1, x2)]	=	15655
    [a__isLNat(x1)]	=	15267
    [a__U21(x1, x2)]	=	x1 + 2
    [a__U91(x1, x2)]	=	x1 + 2
    [sel(x1, x2)]	=	x1 + 3
    [afterNth(x1, x2)]	=	4172
    [nil]	=	10
    [a__splitAt(x1, x2)]	=	x1 + x2 + 1
    [isLNat(x1)]	=	x1 + 15262
    [a__sel#(x1, x2)]	=	2
    [mark(x1)]	=	x1 + 4
    [a__isLNat#(x1)]	=	40719
    [a__U101#(x1, x2, x3)]	=	0
    [a__U11(x1, x2, x3)]	=	x1 + x3 + 0
    [a__sel(x1, x2)]	=	x2 + 4
    [a__isPLNat(x1)]	=	x1 + 15268
    [U61(x1, x2)]	=	x2 + 3
    [U31(x1, x2)]	=	2
    [a__U71(x1, x2)]	=	10
    [a__isPLNat#(x1)]	=	56375
    [head(x1)]	=	15263
    [a__afterNth#(x1, x2)]	=	2
    [a__splitAt#(x1, x2)]	=	0
    [cons(x1, x2)]	=	x1 + x2 + 1
    [a__U61(x1, x2)]	=	x1 + 2
    [snd(x1)]	=	x1 + 15261
    [a__take(x1, x2)]	=	x2 + 6265
    [U81(x1,...,x4)]	=	x3 + 15783
    [a__U41#(x1, x2)]	=	0
    [U82(x1, x2)]	=	x1 + x2 + 31850
    [tt]	=	1
    [a__isNatural(x1)]	=	15268
    [a__isNatural#(x1)]	=	x1 + 2
    [a__fst#(x1)]	=	0
    [U51(x1, x2, x3)]	=	x3 + 8924
    [a__and(x1, x2)]	=	x2 + 3
    [a__tail(x1)]	=	x1 + 4602
    [U41(x1, x2)]	=	3
    [a__tail#(x1)]	=	2
    [a__U101(x1, x2, x3)]	=	x1 + x2 + 7
    [a__U91#(x1, x2)]	=	2
    [a__head(x1)]	=	x1 + 15264

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

    a__isNatural#(s(V1))

    →

    a__isNatural#(V1)

    (211)

    could be deleted.

    1.1.1.1.2.1 Dependency Graph Processor

    The dependency pairs are split into 0 components.