Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/Transformed_CSR_04/Ex1_GL02a_GM)

The rewrite relation of the following TRS is considered.

a__eq(0,0)	→	true	(1)
a__eq(s(X),s(Y))	→	a__eq(X,Y)	(2)
a__eq(X,Y)	→	false	(3)
a__inf(X)	→	cons(X,inf(s(X)))	(4)
a__take(0,X)	→	nil	(5)
a__take(s(X),cons(Y,L))	→	cons(Y,take(X,L))	(6)
a__length(nil)	→	0	(7)
a__length(cons(X,L))	→	s(length(L))	(8)
mark(eq(X1,X2))	→	a__eq(X1,X2)	(9)
mark(inf(X))	→	a__inf(mark(X))	(10)
mark(take(X1,X2))	→	a__take(mark(X1),mark(X2))	(11)
mark(length(X))	→	a__length(mark(X))	(12)
mark(0)	→	0	(13)
mark(true)	→	true	(14)
mark(s(X))	→	s(X)	(15)
mark(false)	→	false	(16)
mark(cons(X1,X2))	→	cons(X1,X2)	(17)
mark(nil)	→	nil	(18)
a__eq(X1,X2)	→	eq(X1,X2)	(19)
a__inf(X)	→	inf(X)	(20)
a__take(X1,X2)	→	take(X1,X2)	(21)
a__length(X)	→	length(X)	(22)

The evaluation strategy is innermost.

Property / Task

Determine bounds on the runtime complexity.

Answer / Result

An upperbound for the complexity is O(n).

Proof (by AProVE @ termCOMP 2023)

1 Dependency Tuples

We get the following set of dependency tuples:

a__eq^#(0,0)

→

(23)

originates from

a__eq(0,0)

→

true

(1)

a__eq^#(s(z0),s(z1))

→

c1(a__eq^#(z0,z1))

(25)

originates from

a__eq(s(z0),s(z1))

→

a__eq(z0,z1)

(24)

a__eq^#(z0,z1)

→

(27)

originates from

a__eq(z0,z1)

→

false

(26)

a__eq^#(z0,z1)

→

(29)

originates from

a__eq(z0,z1)

→

eq(z0,z1)

(28)

a__inf^#(z0)

→

(31)

originates from

a__inf(z0)

→

cons(z0,inf(s(z0)))

(30)

a__inf^#(z0)

→

(33)

originates from

a__inf(z0)

→

inf(z0)

(32)

a__take^#(0,z0)

→

(35)

originates from

a__take(0,z0)

→

nil

(34)

a__take^#(s(z0),cons(z1,z2))

→

(37)

originates from

a__take(s(z0),cons(z1,z2))

→

cons(z1,take(z0,z2))

(36)

a__take^#(z0,z1)

→

(39)

originates from

a__take(z0,z1)

→

take(z0,z1)

(38)

a__length^#(nil)

→

(40)

originates from

a__length(nil)

→

(7)

a__length^#(cons(z0,z1))

→

c10

(42)

originates from

a__length(cons(z0,z1))

→

s(length(z1))

(41)

a__length^#(z0)

→

c11

(44)

originates from

a__length(z0)

→

length(z0)

(43)

mark^#(eq(z0,z1))

→

c12(a__eq^#(z0,z1))

(46)

originates from

mark(eq(z0,z1))

→

a__eq(z0,z1)

(45)

mark^#(inf(z0))

→

c13(a__inf^#(mark(z0)),mark^#(z0))

(48)

originates from

mark(inf(z0))

→

a__inf(mark(z0))

(47)

mark^#(take(z0,z1))

→

c14(a__take^#(mark(z0),mark(z1)),mark^#(z0),mark^#(z1))

(50)

originates from

mark(take(z0,z1))

→

a__take(mark(z0),mark(z1))

(49)

mark^#(length(z0))

→

c15(a__length^#(mark(z0)),mark^#(z0))

(52)

originates from

mark(length(z0))

→

a__length(mark(z0))

(51)

mark^#(0)

→

c16

(53)

originates from

mark(0)

→

(13)

mark^#(true)

→

c17

(54)

originates from

mark(true)

→

true

(14)

mark^#(s(z0))

→

c18

(56)

originates from

mark(s(z0))

→

s(z0)

(55)

mark^#(false)

→

c19

(57)

originates from

mark(false)

→

false

(16)

mark^#(cons(z0,z1))

→

c20

(59)

originates from

mark(cons(z0,z1))

→

cons(z0,z1)

(58)

mark^#(nil)

→

c21

(60)

originates from

mark(nil)

→

nil

(18)

Moreover, we add the following terms to the innermost strategy.

a__eq^#(0,0)

a__eq^#(s(z0),s(z1))

a__eq^#(z0,z1)

a__inf^#(z0)

a__take^#(0,z0)

a__take^#(s(z0),cons(z1,z2))

a__take^#(z0,z1)

a__length^#(nil)

a__length^#(cons(z0,z1))

a__length^#(z0)

mark^#(eq(z0,z1))

mark^#(inf(z0))

mark^#(take(z0,z1))

mark^#(length(z0))

mark^#(0)

mark^#(true)

mark^#(s(z0))

mark^#(false)

mark^#(cons(z0,z1))

mark^#(nil)

1.1 Rule Shifting

The rules

mark^#(inf(z0))	→	c13(a__inf^#(mark(z0)),mark^#(z0))	(48)
mark^#(take(z0,z1))	→	c14(a__take^#(mark(z0),mark(z1)),mark^#(z0),mark^#(z1))	(50)
mark^#(length(z0))	→	c15(a__length^#(mark(z0)),mark^#(z0))	(52)
mark^#(false)	→	c19	(57)
mark^#(cons(z0,z1))	→	c20	(59)

are strictly oriented by the following linear polynomial interpretation over the naturals

[c]	=	0
[c1(x₁)]	=	1 · x₁ + 0
[c2]	=	0
[c3]	=	0
[c4]	=	0
[c5]	=	0
[c6]	=	0
[c7]	=	0
[c8]	=	0
[c9]	=	0
[c10]	=	0
[c11]	=	0
[c12(x₁)]	=	1 · x₁ + 0
[c13(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c14(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃
[c15(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c16]	=	0
[c17]	=	0
[c18]	=	0
[c19]	=	0
[c20]	=	0
[c21]	=	0
[a__eq(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[a__inf(x₁)]	=	1 + 1 · x₁
[a__take(x₁, x₂)]	=	1 + 1 · x₂
[a__length(x₁)]	=	1 + 1 · x₁
[mark(x₁)]	=	1 + 1 · x₁
[a__eq^#(x₁, x₂)]	=	0
[a__inf^#(x₁)]	=	0
[a__take^#(x₁, x₂)]	=	0
[a__length^#(x₁)]	=	0
[mark^#(x₁)]	=	1 · x₁ + 0
[eq(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[inf(x₁)]	=	1 + 1 · x₁
[take(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[length(x₁)]	=	1 + 1 · x₁
[0]	=	0
[true]	=	0
[s(x₁)]	=	0
[false]	=	1
[cons(x₁, x₂)]	=	1 + 1 · x₁
[nil]	=	0

which has the intended complexity. Here, only the following usable rules have been considered:

a__eq^#(0,0)	→	c	(23)
a__eq^#(s(z0),s(z1))	→	c1(a__eq^#(z0,z1))	(25)
a__eq^#(z0,z1)	→	c2	(27)
a__eq^#(z0,z1)	→	c3	(29)
a__inf^#(z0)	→	c4	(31)
a__inf^#(z0)	→	c5	(33)
a__take^#(0,z0)	→	c6	(35)
a__take^#(s(z0),cons(z1,z2))	→	c7	(37)
a__take^#(z0,z1)	→	c8	(39)
a__length^#(nil)	→	c9	(40)
a__length^#(cons(z0,z1))	→	c10	(42)
a__length^#(z0)	→	c11	(44)
mark^#(eq(z0,z1))	→	c12(a__eq^#(z0,z1))	(46)
mark^#(inf(z0))	→	c13(a__inf^#(mark(z0)),mark^#(z0))	(48)
mark^#(take(z0,z1))	→	c14(a__take^#(mark(z0),mark(z1)),mark^#(z0),mark^#(z1))	(50)
mark^#(length(z0))	→	c15(a__length^#(mark(z0)),mark^#(z0))	(52)
mark^#(0)	→	c16	(53)
mark^#(true)	→	c17	(54)
mark^#(s(z0))	→	c18	(56)
mark^#(false)	→	c19	(57)
mark^#(cons(z0,z1))	→	c20	(59)
mark^#(nil)	→	c21	(60)

1.1.1 Rule Shifting

The rules

a__inf^#(z0)	→	c4	(31)
a__inf^#(z0)	→	c5	(33)
mark^#(true)	→	c17	(54)
mark^#(s(z0))	→	c18	(56)

are strictly oriented by the following linear polynomial interpretation over the naturals

[c]	=	0
[c1(x₁)]	=	1 · x₁ + 0
[c2]	=	0
[c3]	=	0
[c4]	=	0
[c5]	=	0
[c6]	=	0
[c7]	=	0
[c8]	=	0
[c9]	=	0
[c10]	=	0
[c11]	=	0
[c12(x₁)]	=	1 · x₁ + 0
[c13(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c14(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃
[c15(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c16]	=	0
[c17]	=	0
[c18]	=	0
[c19]	=	0
[c20]	=	0
[c21]	=	0
[a__eq(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[a__inf(x₁)]	=	1 + 1 · x₁
[a__take(x₁, x₂)]	=	1 + 1 · x₂
[a__length(x₁)]	=	1 + 1 · x₁
[mark(x₁)]	=	1 + 1 · x₁
[a__eq^#(x₁, x₂)]	=	0
[a__inf^#(x₁)]	=	1
[a__take^#(x₁, x₂)]	=	0
[a__length^#(x₁)]	=	0
[mark^#(x₁)]	=	1 · x₁ + 0
[eq(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[inf(x₁)]	=	1 + 1 · x₁
[take(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[length(x₁)]	=	1 + 1 · x₁
[0]	=	0
[true]	=	1
[s(x₁)]	=	1
[false]	=	1
[cons(x₁, x₂)]	=	1 + 1 · x₁
[nil]	=	0

which has the intended complexity. Here, only the following usable rules have been considered:

a__eq^#(0,0)	→	c	(23)
a__eq^#(s(z0),s(z1))	→	c1(a__eq^#(z0,z1))	(25)
a__eq^#(z0,z1)	→	c2	(27)
a__eq^#(z0,z1)	→	c3	(29)
a__inf^#(z0)	→	c4	(31)
a__inf^#(z0)	→	c5	(33)
a__take^#(0,z0)	→	c6	(35)
a__take^#(s(z0),cons(z1,z2))	→	c7	(37)
a__take^#(z0,z1)	→	c8	(39)
a__length^#(nil)	→	c9	(40)
a__length^#(cons(z0,z1))	→	c10	(42)
a__length^#(z0)	→	c11	(44)
mark^#(eq(z0,z1))	→	c12(a__eq^#(z0,z1))	(46)
mark^#(inf(z0))	→	c13(a__inf^#(mark(z0)),mark^#(z0))	(48)
mark^#(take(z0,z1))	→	c14(a__take^#(mark(z0),mark(z1)),mark^#(z0),mark^#(z1))	(50)
mark^#(length(z0))	→	c15(a__length^#(mark(z0)),mark^#(z0))	(52)
mark^#(0)	→	c16	(53)
mark^#(true)	→	c17	(54)
mark^#(s(z0))	→	c18	(56)
mark^#(false)	→	c19	(57)
mark^#(cons(z0,z1))	→	c20	(59)
mark^#(nil)	→	c21	(60)

1.1.1.1 Rule Shifting

The rules

a__eq^#(0,0)	→	c	(23)
a__eq^#(s(z0),s(z1))	→	c1(a__eq^#(z0,z1))	(25)
mark^#(0)	→	c16	(53)

are strictly oriented by the following linear polynomial interpretation over the naturals

[c]	=	0
[c1(x₁)]	=	1 · x₁ + 0
[c2]	=	0
[c3]	=	0
[c4]	=	0
[c5]	=	0
[c6]	=	0
[c7]	=	0
[c8]	=	0
[c9]	=	0
[c10]	=	0
[c11]	=	0
[c12(x₁)]	=	1 · x₁ + 0
[c13(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c14(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃
[c15(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c16]	=	0
[c17]	=	0
[c18]	=	0
[c19]	=	0
[c20]	=	0
[c21]	=	0
[a__eq(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[a__inf(x₁)]	=	1 + 1 · x₁
[a__take(x₁, x₂)]	=	1 + 1 · x₂
[a__length(x₁)]	=	1 + 1 · x₁
[mark(x₁)]	=	1 + 1 · x₁
[a__eq^#(x₁, x₂)]	=	1 · x₁ + 0
[a__inf^#(x₁)]	=	1
[a__take^#(x₁, x₂)]	=	0
[a__length^#(x₁)]	=	0
[mark^#(x₁)]	=	1 · x₁ + 0
[eq(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[inf(x₁)]	=	1 + 1 · x₁
[take(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[length(x₁)]	=	1 · x₁ + 0
[0]	=	1
[true]	=	1
[s(x₁)]	=	1 + 1 · x₁
[false]	=	1
[cons(x₁, x₂)]	=	1 + 1 · x₁
[nil]	=	0

which has the intended complexity. Here, only the following usable rules have been considered:

a__eq^#(0,0)	→	c	(23)
a__eq^#(s(z0),s(z1))	→	c1(a__eq^#(z0,z1))	(25)
a__eq^#(z0,z1)	→	c2	(27)
a__eq^#(z0,z1)	→	c3	(29)
a__inf^#(z0)	→	c4	(31)
a__inf^#(z0)	→	c5	(33)
a__take^#(0,z0)	→	c6	(35)
a__take^#(s(z0),cons(z1,z2))	→	c7	(37)
a__take^#(z0,z1)	→	c8	(39)
a__length^#(nil)	→	c9	(40)
a__length^#(cons(z0,z1))	→	c10	(42)
a__length^#(z0)	→	c11	(44)
mark^#(eq(z0,z1))	→	c12(a__eq^#(z0,z1))	(46)
mark^#(inf(z0))	→	c13(a__inf^#(mark(z0)),mark^#(z0))	(48)
mark^#(take(z0,z1))	→	c14(a__take^#(mark(z0),mark(z1)),mark^#(z0),mark^#(z1))	(50)
mark^#(length(z0))	→	c15(a__length^#(mark(z0)),mark^#(z0))	(52)
mark^#(0)	→	c16	(53)
mark^#(true)	→	c17	(54)
mark^#(s(z0))	→	c18	(56)
mark^#(false)	→	c19	(57)
mark^#(cons(z0,z1))	→	c20	(59)
mark^#(nil)	→	c21	(60)

1.1.1.1.1 Rule Shifting

The rules

a__length^#(nil)	→	c9	(40)
a__length^#(cons(z0,z1))	→	c10	(42)
a__length^#(z0)	→	c11	(44)

are strictly oriented by the following linear polynomial interpretation over the naturals

[c]	=	0
[c1(x₁)]	=	1 · x₁ + 0
[c2]	=	0
[c3]	=	0
[c4]	=	0
[c5]	=	0
[c6]	=	0
[c7]	=	0
[c8]	=	0
[c9]	=	0
[c10]	=	0
[c11]	=	0
[c12(x₁)]	=	1 · x₁ + 0
[c13(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c14(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃
[c15(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c16]	=	0
[c17]	=	0
[c18]	=	0
[c19]	=	0
[c20]	=	0
[c21]	=	0
[a__eq(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[a__inf(x₁)]	=	1 + 1 · x₁
[a__take(x₁, x₂)]	=	1 + 1 · x₂
[a__length(x₁)]	=	1 + 1 · x₁
[mark(x₁)]	=	1 + 1 · x₁
[a__eq^#(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[a__inf^#(x₁)]	=	1
[a__take^#(x₁, x₂)]	=	0
[a__length^#(x₁)]	=	1
[mark^#(x₁)]	=	1 · x₁ + 0
[eq(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[inf(x₁)]	=	1 + 1 · x₁
[take(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[length(x₁)]	=	1 + 1 · x₁
[0]	=	1
[true]	=	1
[s(x₁)]	=	1 + 1 · x₁
[false]	=	1
[cons(x₁, x₂)]	=	1 + 1 · x₁
[nil]	=	0

which has the intended complexity. Here, only the following usable rules have been considered:

a__eq^#(0,0)	→	c	(23)
a__eq^#(s(z0),s(z1))	→	c1(a__eq^#(z0,z1))	(25)
a__eq^#(z0,z1)	→	c2	(27)
a__eq^#(z0,z1)	→	c3	(29)
a__inf^#(z0)	→	c4	(31)
a__inf^#(z0)	→	c5	(33)
a__take^#(0,z0)	→	c6	(35)
a__take^#(s(z0),cons(z1,z2))	→	c7	(37)
a__take^#(z0,z1)	→	c8	(39)
a__length^#(nil)	→	c9	(40)
a__length^#(cons(z0,z1))	→	c10	(42)
a__length^#(z0)	→	c11	(44)
mark^#(eq(z0,z1))	→	c12(a__eq^#(z0,z1))	(46)
mark^#(inf(z0))	→	c13(a__inf^#(mark(z0)),mark^#(z0))	(48)
mark^#(take(z0,z1))	→	c14(a__take^#(mark(z0),mark(z1)),mark^#(z0),mark^#(z1))	(50)
mark^#(length(z0))	→	c15(a__length^#(mark(z0)),mark^#(z0))	(52)
mark^#(0)	→	c16	(53)
mark^#(true)	→	c17	(54)
mark^#(s(z0))	→	c18	(56)
mark^#(false)	→	c19	(57)
mark^#(cons(z0,z1))	→	c20	(59)
mark^#(nil)	→	c21	(60)

1.1.1.1.1.1 Rule Shifting

The rules

mark^#(eq(z0,z1))	→	c12(a__eq^#(z0,z1))	(46)
mark^#(nil)	→	c21	(60)

are strictly oriented by the following linear polynomial interpretation over the naturals

[c]	=	0
[c1(x₁)]	=	1 · x₁ + 0
[c2]	=	0
[c3]	=	0
[c4]	=	0
[c5]	=	0
[c6]	=	0
[c7]	=	0
[c8]	=	0
[c9]	=	0
[c10]	=	0
[c11]	=	0
[c12(x₁)]	=	1 · x₁ + 0
[c13(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c14(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃
[c15(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c16]	=	0
[c17]	=	0
[c18]	=	0
[c19]	=	0
[c20]	=	0
[c21]	=	0
[a__eq(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[a__inf(x₁)]	=	1 + 1 · x₁
[a__take(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[a__length(x₁)]	=	1 + 1 · x₁
[mark(x₁)]	=	1 + 1 · x₁
[a__eq^#(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[a__inf^#(x₁)]	=	1
[a__take^#(x₁, x₂)]	=	0
[a__length^#(x₁)]	=	1
[mark^#(x₁)]	=	1 · x₁ + 0
[eq(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[inf(x₁)]	=	1 + 1 · x₁
[take(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[length(x₁)]	=	1 + 1 · x₁
[0]	=	1
[true]	=	1
[s(x₁)]	=	1 + 1 · x₁
[false]	=	1
[cons(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[nil]	=	1

which has the intended complexity. Here, only the following usable rules have been considered:

a__eq^#(0,0)	→	c	(23)
a__eq^#(s(z0),s(z1))	→	c1(a__eq^#(z0,z1))	(25)
a__eq^#(z0,z1)	→	c2	(27)
a__eq^#(z0,z1)	→	c3	(29)
a__inf^#(z0)	→	c4	(31)
a__inf^#(z0)	→	c5	(33)
a__take^#(0,z0)	→	c6	(35)
a__take^#(s(z0),cons(z1,z2))	→	c7	(37)
a__take^#(z0,z1)	→	c8	(39)
a__length^#(nil)	→	c9	(40)
a__length^#(cons(z0,z1))	→	c10	(42)
a__length^#(z0)	→	c11	(44)
mark^#(eq(z0,z1))	→	c12(a__eq^#(z0,z1))	(46)
mark^#(inf(z0))	→	c13(a__inf^#(mark(z0)),mark^#(z0))	(48)
mark^#(take(z0,z1))	→	c14(a__take^#(mark(z0),mark(z1)),mark^#(z0),mark^#(z1))	(50)
mark^#(length(z0))	→	c15(a__length^#(mark(z0)),mark^#(z0))	(52)
mark^#(0)	→	c16	(53)
mark^#(true)	→	c17	(54)
mark^#(s(z0))	→	c18	(56)
mark^#(false)	→	c19	(57)
mark^#(cons(z0,z1))	→	c20	(59)
mark^#(nil)	→	c21	(60)

1.1.1.1.1.1.1 Rule Shifting

The rules

a__eq^#(z0,z1)	→	c2	(27)
a__eq^#(z0,z1)	→	c3	(29)

are strictly oriented by the following linear polynomial interpretation over the naturals

[c]	=	0
[c1(x₁)]	=	1 · x₁ + 0
[c2]	=	0
[c3]	=	0
[c4]	=	0
[c5]	=	0
[c6]	=	0
[c7]	=	0
[c8]	=	0
[c9]	=	0
[c10]	=	0
[c11]	=	0
[c12(x₁)]	=	1 · x₁ + 0
[c13(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c14(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃
[c15(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c16]	=	0
[c17]	=	0
[c18]	=	0
[c19]	=	0
[c20]	=	0
[c21]	=	0
[a__eq(x₁, x₂)]	=	3 + 3 · x₁ + 3 · x₂
[a__inf(x₁)]	=	3
[a__take(x₁, x₂)]	=	3
[a__length(x₁)]	=	3 + 3 · x₁
[mark(x₁)]	=	3 · x₁ + 0
[a__eq^#(x₁, x₂)]	=	3
[a__inf^#(x₁)]	=	0
[a__take^#(x₁, x₂)]	=	0
[a__length^#(x₁)]	=	0
[mark^#(x₁)]	=	2 · x₁ + 0
[eq(x₁, x₂)]	=	2 + 1 · x₁ + 1 · x₂
[inf(x₁)]	=	1 + 1 · x₁
[take(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[length(x₁)]	=	1 · x₁ + 0
[0]	=	0
[true]	=	3
[s(x₁)]	=	0
[false]	=	3
[cons(x₁, x₂)]	=	1 · x₁ + 0
[nil]	=	0

which has the intended complexity. Here, only the following usable rules have been considered:

a__eq^#(0,0)	→	c	(23)
a__eq^#(s(z0),s(z1))	→	c1(a__eq^#(z0,z1))	(25)
a__eq^#(z0,z1)	→	c2	(27)
a__eq^#(z0,z1)	→	c3	(29)
a__inf^#(z0)	→	c4	(31)
a__inf^#(z0)	→	c5	(33)
a__take^#(0,z0)	→	c6	(35)
a__take^#(s(z0),cons(z1,z2))	→	c7	(37)
a__take^#(z0,z1)	→	c8	(39)
a__length^#(nil)	→	c9	(40)
a__length^#(cons(z0,z1))	→	c10	(42)
a__length^#(z0)	→	c11	(44)
mark^#(eq(z0,z1))	→	c12(a__eq^#(z0,z1))	(46)
mark^#(inf(z0))	→	c13(a__inf^#(mark(z0)),mark^#(z0))	(48)
mark^#(take(z0,z1))	→	c14(a__take^#(mark(z0),mark(z1)),mark^#(z0),mark^#(z1))	(50)
mark^#(length(z0))	→	c15(a__length^#(mark(z0)),mark^#(z0))	(52)
mark^#(0)	→	c16	(53)
mark^#(true)	→	c17	(54)
mark^#(s(z0))	→	c18	(56)
mark^#(false)	→	c19	(57)
mark^#(cons(z0,z1))	→	c20	(59)
mark^#(nil)	→	c21	(60)

1.1.1.1.1.1.1.1 Rule Shifting

The rules

a__take^#(0,z0)	→	c6	(35)
a__take^#(s(z0),cons(z1,z2))	→	c7	(37)
a__take^#(z0,z1)	→	c8	(39)

are strictly oriented by the following linear polynomial interpretation over the naturals

[c]	=	0
[c1(x₁)]	=	1 · x₁ + 0
[c2]	=	0
[c3]	=	0
[c4]	=	0
[c5]	=	0
[c6]	=	0
[c7]	=	0
[c8]	=	0
[c9]	=	0
[c10]	=	0
[c11]	=	0
[c12(x₁)]	=	1 · x₁ + 0
[c13(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c14(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃
[c15(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c16]	=	0
[c17]	=	0
[c18]	=	0
[c19]	=	0
[c20]	=	0
[c21]	=	0
[a__eq(x₁, x₂)]	=	1
[a__inf(x₁)]	=	1 + 1 · x₁
[a__take(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[a__length(x₁)]	=	1 + 1 · x₁
[mark(x₁)]	=	1 · x₁ + 0
[a__eq^#(x₁, x₂)]	=	1
[a__inf^#(x₁)]	=	1
[a__take^#(x₁, x₂)]	=	1
[a__length^#(x₁)]	=	1
[mark^#(x₁)]	=	1 · x₁ + 0
[eq(x₁, x₂)]	=	1
[inf(x₁)]	=	1 + 1 · x₁
[take(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[length(x₁)]	=	1 + 1 · x₁
[0]	=	1
[true]	=	1
[s(x₁)]	=	1
[false]	=	1
[cons(x₁, x₂)]	=	1 + 1 · x₁
[nil]	=	1

which has the intended complexity. Here, only the following usable rules have been considered:

a__eq^#(0,0)	→	c	(23)
a__eq^#(s(z0),s(z1))	→	c1(a__eq^#(z0,z1))	(25)
a__eq^#(z0,z1)	→	c2	(27)
a__eq^#(z0,z1)	→	c3	(29)
a__inf^#(z0)	→	c4	(31)
a__inf^#(z0)	→	c5	(33)
a__take^#(0,z0)	→	c6	(35)
a__take^#(s(z0),cons(z1,z2))	→	c7	(37)
a__take^#(z0,z1)	→	c8	(39)
a__length^#(nil)	→	c9	(40)
a__length^#(cons(z0,z1))	→	c10	(42)
a__length^#(z0)	→	c11	(44)
mark^#(eq(z0,z1))	→	c12(a__eq^#(z0,z1))	(46)
mark^#(inf(z0))	→	c13(a__inf^#(mark(z0)),mark^#(z0))	(48)
mark^#(take(z0,z1))	→	c14(a__take^#(mark(z0),mark(z1)),mark^#(z0),mark^#(z1))	(50)
mark^#(length(z0))	→	c15(a__length^#(mark(z0)),mark^#(z0))	(52)
mark^#(0)	→	c16	(53)
mark^#(true)	→	c17	(54)
mark^#(s(z0))	→	c18	(56)
mark^#(false)	→	c19	(57)
mark^#(cons(z0,z1))	→	c20	(59)
mark^#(nil)	→	c21	(60)

1.1.1.1.1.1.1.1.1 R is empty

There are no rules in the TRS R. Hence, R/S has complexity O(1).