Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/Transformed_CSR_04/Ex15_Luc98_GM)

The rewrite relation of the following TRS is considered.

a__and(true,X)	→	mark(X)	(1)
a__and(false,Y)	→	false	(2)
a__if(true,X,Y)	→	mark(X)	(3)
a__if(false,X,Y)	→	mark(Y)	(4)
a__add(0,X)	→	mark(X)	(5)
a__add(s(X),Y)	→	s(add(X,Y))	(6)
a__first(0,X)	→	nil	(7)
a__first(s(X),cons(Y,Z))	→	cons(Y,first(X,Z))	(8)
a__from(X)	→	cons(X,from(s(X)))	(9)
mark(and(X1,X2))	→	a__and(mark(X1),X2)	(10)
mark(if(X1,X2,X3))	→	a__if(mark(X1),X2,X3)	(11)
mark(add(X1,X2))	→	a__add(mark(X1),X2)	(12)
mark(first(X1,X2))	→	a__first(mark(X1),mark(X2))	(13)
mark(from(X))	→	a__from(X)	(14)
mark(true)	→	true	(15)
mark(false)	→	false	(16)
mark(0)	→	0	(17)
mark(s(X))	→	s(X)	(18)
mark(nil)	→	nil	(19)
mark(cons(X1,X2))	→	cons(X1,X2)	(20)
a__and(X1,X2)	→	and(X1,X2)	(21)
a__if(X1,X2,X3)	→	if(X1,X2,X3)	(22)
a__add(X1,X2)	→	add(X1,X2)	(23)
a__first(X1,X2)	→	first(X1,X2)	(24)
a__from(X)	→	from(X)	(25)

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__and^#(true,z0)

→

c(mark^#(z0))

(27)

originates from

a__and(true,z0)

→

mark(z0)

(26)

a__and^#(false,z0)

→

(29)

originates from

a__and(false,z0)

→

false

(28)

a__and^#(z0,z1)

→

(31)

originates from

a__and(z0,z1)

→

and(z0,z1)

(30)

a__if^#(true,z0,z1)

→

c3(mark^#(z0))

(33)

originates from

a__if(true,z0,z1)

→

mark(z0)

(32)

a__if^#(false,z0,z1)

→

c4(mark^#(z1))

(35)

originates from

a__if(false,z0,z1)

→

mark(z1)

(34)

a__if^#(z0,z1,z2)

→

(37)

originates from

a__if(z0,z1,z2)

→

if(z0,z1,z2)

(36)

a__add^#(0,z0)

→

c6(mark^#(z0))

(39)

originates from

a__add(0,z0)

→

mark(z0)

(38)

a__add^#(s(z0),z1)

→

(41)

originates from

a__add(s(z0),z1)

→

s(add(z0,z1))

(40)

a__add^#(z0,z1)

→

(43)

originates from

a__add(z0,z1)

→

add(z0,z1)

(42)

a__first^#(0,z0)

→

(45)

originates from

a__first(0,z0)

→

nil

(44)

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

→

c10

(47)

originates from

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

→

cons(z1,first(z0,z2))

(46)

a__first^#(z0,z1)

→

c11

(49)

originates from

a__first(z0,z1)

→

first(z0,z1)

(48)

a__from^#(z0)

→

c12

(51)

originates from

a__from(z0)

→

cons(z0,from(s(z0)))

(50)

a__from^#(z0)

→

c13

(53)

originates from

a__from(z0)

→

from(z0)

(52)

mark^#(and(z0,z1))

→

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

(55)

originates from

mark(and(z0,z1))

→

a__and(mark(z0),z1)

(54)

mark^#(if(z0,z1,z2))

→

c15(a__if^#(mark(z0),z1,z2),mark^#(z0))

(57)

originates from

mark(if(z0,z1,z2))

→

a__if(mark(z0),z1,z2)

(56)

mark^#(add(z0,z1))

→

c16(a__add^#(mark(z0),z1),mark^#(z0))

(59)

originates from

mark(add(z0,z1))

→

a__add(mark(z0),z1)

(58)

mark^#(first(z0,z1))

→

c17(a__first^#(mark(z0),mark(z1)),mark^#(z0),mark^#(z1))

(61)

originates from

mark(first(z0,z1))

→

a__first(mark(z0),mark(z1))

(60)

mark^#(from(z0))

→

c18(a__from^#(z0))

(63)

originates from

mark(from(z0))

→

a__from(z0)

(62)

mark^#(true)

→

c19

(64)

originates from

mark(true)

→

true

(15)

mark^#(false)

→

c20

(65)

originates from

mark(false)

→

false

(16)

mark^#(0)

→

c21

(66)

originates from

mark(0)

→

(17)

mark^#(s(z0))

→

c22

(68)

originates from

mark(s(z0))

→

s(z0)

(67)

mark^#(nil)

→

c23

(69)

originates from

mark(nil)

→

nil

(19)

mark^#(cons(z0,z1))

→

c24

(71)

originates from

mark(cons(z0,z1))

→

cons(z0,z1)

(70)

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

a__and^#(true,z0)

a__and^#(false,z0)

a__and^#(z0,z1)

a__if^#(true,z0,z1)

a__if^#(false,z0,z1)

a__if^#(z0,z1,z2)

a__add^#(0,z0)

a__add^#(s(z0),z1)

a__add^#(z0,z1)

a__first^#(0,z0)

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

a__first^#(z0,z1)

a__from^#(z0)

mark^#(and(z0,z1))

mark^#(if(z0,z1,z2))

mark^#(add(z0,z1))

mark^#(first(z0,z1))

mark^#(from(z0))

mark^#(true)

mark^#(false)

mark^#(0)

mark^#(s(z0))

mark^#(nil)

mark^#(cons(z0,z1))

1.1 Rule Shifting

The rules

a__from^#(z0)	→	c12	(51)
a__from^#(z0)	→	c13	(53)
mark^#(and(z0,z1))	→	c14(a__and^#(mark(z0),z1),mark^#(z0))	(55)
mark^#(if(z0,z1,z2))	→	c15(a__if^#(mark(z0),z1,z2),mark^#(z0))	(57)

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

[c(x₁)]	=	1 · x₁ + 0
[c1]	=	0
[c2]	=	0
[c3(x₁)]	=	1 · x₁ + 0
[c4(x₁)]	=	1 · x₁ + 0
[c5]	=	0
[c6(x₁)]	=	1 · x₁ + 0
[c7]	=	0
[c8]	=	0
[c9]	=	0
[c10]	=	0
[c11]	=	0
[c12]	=	0
[c13]	=	0
[c14(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c15(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c16(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c17(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃
[c18(x₁)]	=	1 · x₁ + 0
[c19]	=	0
[c20]	=	0
[c21]	=	0
[c22]	=	0
[c23]	=	0
[c24]	=	0
[a__and(x₁, x₂)]	=	3 + 3 · x₂
[a__if(x₁, x₂, x₃)]	=	3 + 3 · x₂ + 3 · x₃
[a__add(x₁, x₂)]	=	3 + 3 · x₂
[a__first(x₁, x₂)]	=	3 + 3 · x₁ + 3 · x₂
[a__from(x₁)]	=	3 + 3 · x₁
[mark(x₁)]	=	3 · x₁ + 0
[a__and^#(x₁, x₂)]	=	1 · x₂ + 0
[a__if^#(x₁, x₂, x₃)]	=	1 · x₂ + 0 + 1 · x₃
[a__add^#(x₁, x₂)]	=	1 · x₂ + 0
[a__first^#(x₁, x₂)]	=	0
[a__from^#(x₁)]	=	2 + 1 · x₁
[mark^#(x₁)]	=	1 · x₁ + 0
[and(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[if(x₁, x₂, x₃)]	=	1 + 1 · x₁ + 1 · x₂ + 1 · x₃
[add(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[first(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[from(x₁)]	=	2 + 1 · x₁
[true]	=	0
[false]	=	0
[0]	=	0
[s(x₁)]	=	0
[nil]	=	0
[cons(x₁, x₂)]	=	1 · x₁ + 0

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

a__and^#(true,z0)	→	c(mark^#(z0))	(27)
a__and^#(false,z0)	→	c1	(29)
a__and^#(z0,z1)	→	c2	(31)
a__if^#(true,z0,z1)	→	c3(mark^#(z0))	(33)
a__if^#(false,z0,z1)	→	c4(mark^#(z1))	(35)
a__if^#(z0,z1,z2)	→	c5	(37)
a__add^#(0,z0)	→	c6(mark^#(z0))	(39)
a__add^#(s(z0),z1)	→	c7	(41)
a__add^#(z0,z1)	→	c8	(43)
a__first^#(0,z0)	→	c9	(45)
a__first^#(s(z0),cons(z1,z2))	→	c10	(47)
a__first^#(z0,z1)	→	c11	(49)
a__from^#(z0)	→	c12	(51)
a__from^#(z0)	→	c13	(53)
mark^#(and(z0,z1))	→	c14(a__and^#(mark(z0),z1),mark^#(z0))	(55)
mark^#(if(z0,z1,z2))	→	c15(a__if^#(mark(z0),z1,z2),mark^#(z0))	(57)
mark^#(add(z0,z1))	→	c16(a__add^#(mark(z0),z1),mark^#(z0))	(59)
mark^#(first(z0,z1))	→	c17(a__first^#(mark(z0),mark(z1)),mark^#(z0),mark^#(z1))	(61)
mark^#(from(z0))	→	c18(a__from^#(z0))	(63)
mark^#(true)	→	c19	(64)
mark^#(false)	→	c20	(65)
mark^#(0)	→	c21	(66)
mark^#(s(z0))	→	c22	(68)
mark^#(nil)	→	c23	(69)
mark^#(cons(z0,z1))	→	c24	(71)

1.1.1 Rule Shifting

The rules

a__add^#(0,z0)	→	c6(mark^#(z0))	(39)
a__add^#(s(z0),z1)	→	c7	(41)
a__add^#(z0,z1)	→	c8	(43)
mark^#(first(z0,z1))	→	c17(a__first^#(mark(z0),mark(z1)),mark^#(z0),mark^#(z1))	(61)
mark^#(true)	→	c19	(64)
mark^#(false)	→	c20	(65)
mark^#(0)	→	c21	(66)
mark^#(s(z0))	→	c22	(68)
mark^#(nil)	→	c23	(69)
mark^#(cons(z0,z1))	→	c24	(71)

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

[c(x₁)]	=	1 · x₁ + 0
[c1]	=	0
[c2]	=	0
[c3(x₁)]	=	1 · x₁ + 0
[c4(x₁)]	=	1 · x₁ + 0
[c5]	=	0
[c6(x₁)]	=	1 · x₁ + 0
[c7]	=	0
[c8]	=	0
[c9]	=	0
[c10]	=	0
[c11]	=	0
[c12]	=	0
[c13]	=	0
[c14(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c15(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c16(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c17(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃
[c18(x₁)]	=	1 · x₁ + 0
[c19]	=	0
[c20]	=	0
[c21]	=	0
[c22]	=	0
[c23]	=	0
[c24]	=	0
[a__and(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[a__if(x₁, x₂, x₃)]	=	1 + 1 · x₁ + 1 · x₂ + 1 · x₃
[a__add(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[a__first(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[a__from(x₁)]	=	1 + 1 · x₁
[mark(x₁)]	=	1 · x₁ + 0
[a__and^#(x₁, x₂)]	=	1 · x₂ + 0
[a__if^#(x₁, x₂, x₃)]	=	1 · x₂ + 0 + 1 · x₃
[a__add^#(x₁, x₂)]	=	1 + 1 · x₂
[a__first^#(x₁, x₂)]	=	0
[a__from^#(x₁)]	=	1 + 1 · x₁
[mark^#(x₁)]	=	1 · x₁ + 0
[and(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[if(x₁, x₂, x₃)]	=	1 + 1 · x₁ + 1 · x₂ + 1 · x₃
[add(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[first(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[from(x₁)]	=	1 + 1 · x₁
[true]	=	1
[false]	=	1
[0]	=	1
[s(x₁)]	=	1 + 1 · x₁
[nil]	=	1
[cons(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂

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

a__and^#(true,z0)	→	c(mark^#(z0))	(27)
a__and^#(false,z0)	→	c1	(29)
a__and^#(z0,z1)	→	c2	(31)
a__if^#(true,z0,z1)	→	c3(mark^#(z0))	(33)
a__if^#(false,z0,z1)	→	c4(mark^#(z1))	(35)
a__if^#(z0,z1,z2)	→	c5	(37)
a__add^#(0,z0)	→	c6(mark^#(z0))	(39)
a__add^#(s(z0),z1)	→	c7	(41)
a__add^#(z0,z1)	→	c8	(43)
a__first^#(0,z0)	→	c9	(45)
a__first^#(s(z0),cons(z1,z2))	→	c10	(47)
a__first^#(z0,z1)	→	c11	(49)
a__from^#(z0)	→	c12	(51)
a__from^#(z0)	→	c13	(53)
mark^#(and(z0,z1))	→	c14(a__and^#(mark(z0),z1),mark^#(z0))	(55)
mark^#(if(z0,z1,z2))	→	c15(a__if^#(mark(z0),z1,z2),mark^#(z0))	(57)
mark^#(add(z0,z1))	→	c16(a__add^#(mark(z0),z1),mark^#(z0))	(59)
mark^#(first(z0,z1))	→	c17(a__first^#(mark(z0),mark(z1)),mark^#(z0),mark^#(z1))	(61)
mark^#(from(z0))	→	c18(a__from^#(z0))	(63)
mark^#(true)	→	c19	(64)
mark^#(false)	→	c20	(65)
mark^#(0)	→	c21	(66)
mark^#(s(z0))	→	c22	(68)
mark^#(nil)	→	c23	(69)
mark^#(cons(z0,z1))	→	c24	(71)

1.1.1.1 Rule Shifting

The rules

mark^#(add(z0,z1))	→	c16(a__add^#(mark(z0),z1),mark^#(z0))	(59)
mark^#(from(z0))	→	c18(a__from^#(z0))	(63)

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

[c(x₁)]	=	1 · x₁ + 0
[c1]	=	0
[c2]	=	0
[c3(x₁)]	=	1 · x₁ + 0
[c4(x₁)]	=	1 · x₁ + 0
[c5]	=	0
[c6(x₁)]	=	1 · x₁ + 0
[c7]	=	0
[c8]	=	0
[c9]	=	0
[c10]	=	0
[c11]	=	0
[c12]	=	0
[c13]	=	0
[c14(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c15(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c16(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c17(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃
[c18(x₁)]	=	1 · x₁ + 0
[c19]	=	0
[c20]	=	0
[c21]	=	0
[c22]	=	0
[c23]	=	0
[c24]	=	0
[a__and(x₁, x₂)]	=	1 · x₁ + 0 + 3 · x₂
[a__if(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 3 · x₂ + 3 · x₃
[a__add(x₁, x₂)]	=	3 + 1 · x₁ + 3 · x₂
[a__first(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[a__from(x₁)]	=	2 + 3 · x₁
[mark(x₁)]	=	3 · x₁ + 0
[a__and^#(x₁, x₂)]	=	1 · x₂ + 0
[a__if^#(x₁, x₂, x₃)]	=	1 · x₂ + 0 + 1 · x₃
[a__add^#(x₁, x₂)]	=	1 · x₂ + 0
[a__first^#(x₁, x₂)]	=	0
[a__from^#(x₁)]	=	1 · x₁ + 0
[mark^#(x₁)]	=	1 · x₁ + 0
[and(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[if(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃
[add(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[first(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[from(x₁)]	=	1 + 1 · x₁
[true]	=	0
[false]	=	0
[0]	=	0
[s(x₁)]	=	1 + 1 · x₁
[nil]	=	0
[cons(x₁, x₂)]	=	1 · x₁ + 0

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

a__and^#(true,z0)	→	c(mark^#(z0))	(27)
a__and^#(false,z0)	→	c1	(29)
a__and^#(z0,z1)	→	c2	(31)
a__if^#(true,z0,z1)	→	c3(mark^#(z0))	(33)
a__if^#(false,z0,z1)	→	c4(mark^#(z1))	(35)
a__if^#(z0,z1,z2)	→	c5	(37)
a__add^#(0,z0)	→	c6(mark^#(z0))	(39)
a__add^#(s(z0),z1)	→	c7	(41)
a__add^#(z0,z1)	→	c8	(43)
a__first^#(0,z0)	→	c9	(45)
a__first^#(s(z0),cons(z1,z2))	→	c10	(47)
a__first^#(z0,z1)	→	c11	(49)
a__from^#(z0)	→	c12	(51)
a__from^#(z0)	→	c13	(53)
mark^#(and(z0,z1))	→	c14(a__and^#(mark(z0),z1),mark^#(z0))	(55)
mark^#(if(z0,z1,z2))	→	c15(a__if^#(mark(z0),z1,z2),mark^#(z0))	(57)
mark^#(add(z0,z1))	→	c16(a__add^#(mark(z0),z1),mark^#(z0))	(59)
mark^#(first(z0,z1))	→	c17(a__first^#(mark(z0),mark(z1)),mark^#(z0),mark^#(z1))	(61)
mark^#(from(z0))	→	c18(a__from^#(z0))	(63)
mark^#(true)	→	c19	(64)
mark^#(false)	→	c20	(65)
mark^#(0)	→	c21	(66)
mark^#(s(z0))	→	c22	(68)
mark^#(nil)	→	c23	(69)
mark^#(cons(z0,z1))	→	c24	(71)

1.1.1.1.1 Rule Shifting

The rules

a__and^#(true,z0)	→	c(mark^#(z0))	(27)
a__and^#(false,z0)	→	c1	(29)
a__and^#(z0,z1)	→	c2	(31)
a__if^#(true,z0,z1)	→	c3(mark^#(z0))	(33)
a__if^#(false,z0,z1)	→	c4(mark^#(z1))	(35)
a__if^#(z0,z1,z2)	→	c5	(37)

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

[c(x₁)]	=	1 · x₁ + 0
[c1]	=	0
[c2]	=	0
[c3(x₁)]	=	1 · x₁ + 0
[c4(x₁)]	=	1 · x₁ + 0
[c5]	=	0
[c6(x₁)]	=	1 · x₁ + 0
[c7]	=	0
[c8]	=	0
[c9]	=	0
[c10]	=	0
[c11]	=	0
[c12]	=	0
[c13]	=	0
[c14(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c15(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c16(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c17(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃
[c18(x₁)]	=	1 · x₁ + 0
[c19]	=	0
[c20]	=	0
[c21]	=	0
[c22]	=	0
[c23]	=	0
[c24]	=	0
[a__and(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[a__if(x₁, x₂, x₃)]	=	1 + 1 · x₁ + 1 · x₂ + 1 · x₃
[a__add(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[a__first(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[a__from(x₁)]	=	1 + 1 · x₁
[mark(x₁)]	=	1 · x₁ + 0
[a__and^#(x₁, x₂)]	=	1 + 1 · x₂
[a__if^#(x₁, x₂, x₃)]	=	1 + 1 · x₂ + 1 · x₃
[a__add^#(x₁, x₂)]	=	1 + 1 · x₂
[a__first^#(x₁, x₂)]	=	0
[a__from^#(x₁)]	=	1 + 1 · x₁
[mark^#(x₁)]	=	1 · x₁ + 0
[and(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[if(x₁, x₂, x₃)]	=	1 + 1 · x₁ + 1 · x₂ + 1 · x₃
[add(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[first(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[from(x₁)]	=	1 + 1 · x₁
[true]	=	1
[false]	=	1
[0]	=	1
[s(x₁)]	=	1 + 1 · x₁
[nil]	=	1
[cons(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂

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

a__and^#(true,z0)	→	c(mark^#(z0))	(27)
a__and^#(false,z0)	→	c1	(29)
a__and^#(z0,z1)	→	c2	(31)
a__if^#(true,z0,z1)	→	c3(mark^#(z0))	(33)
a__if^#(false,z0,z1)	→	c4(mark^#(z1))	(35)
a__if^#(z0,z1,z2)	→	c5	(37)
a__add^#(0,z0)	→	c6(mark^#(z0))	(39)
a__add^#(s(z0),z1)	→	c7	(41)
a__add^#(z0,z1)	→	c8	(43)
a__first^#(0,z0)	→	c9	(45)
a__first^#(s(z0),cons(z1,z2))	→	c10	(47)
a__first^#(z0,z1)	→	c11	(49)
a__from^#(z0)	→	c12	(51)
a__from^#(z0)	→	c13	(53)
mark^#(and(z0,z1))	→	c14(a__and^#(mark(z0),z1),mark^#(z0))	(55)
mark^#(if(z0,z1,z2))	→	c15(a__if^#(mark(z0),z1,z2),mark^#(z0))	(57)
mark^#(add(z0,z1))	→	c16(a__add^#(mark(z0),z1),mark^#(z0))	(59)
mark^#(first(z0,z1))	→	c17(a__first^#(mark(z0),mark(z1)),mark^#(z0),mark^#(z1))	(61)
mark^#(from(z0))	→	c18(a__from^#(z0))	(63)
mark^#(true)	→	c19	(64)
mark^#(false)	→	c20	(65)
mark^#(0)	→	c21	(66)
mark^#(s(z0))	→	c22	(68)
mark^#(nil)	→	c23	(69)
mark^#(cons(z0,z1))	→	c24	(71)

1.1.1.1.1.1 Rule Shifting

The rules

a__first^#(0,z0)	→	c9	(45)
a__first^#(s(z0),cons(z1,z2))	→	c10	(47)
a__first^#(z0,z1)	→	c11	(49)

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

[c(x₁)]	=	1 · x₁ + 0
[c1]	=	0
[c2]	=	0
[c3(x₁)]	=	1 · x₁ + 0
[c4(x₁)]	=	1 · x₁ + 0
[c5]	=	0
[c6(x₁)]	=	1 · x₁ + 0
[c7]	=	0
[c8]	=	0
[c9]	=	0
[c10]	=	0
[c11]	=	0
[c12]	=	0
[c13]	=	0
[c14(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c15(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c16(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c17(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃
[c18(x₁)]	=	1 · x₁ + 0
[c19]	=	0
[c20]	=	0
[c21]	=	0
[c22]	=	0
[c23]	=	0
[c24]	=	0
[a__and(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[a__if(x₁, x₂, x₃)]	=	1 + 1 · x₁ + 1 · x₂ + 1 · x₃
[a__add(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[a__first(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[a__from(x₁)]	=	1 + 1 · x₁
[mark(x₁)]	=	1 · x₁ + 0
[a__and^#(x₁, x₂)]	=	1 + 1 · x₂
[a__if^#(x₁, x₂, x₃)]	=	1 + 1 · x₂ + 1 · x₃
[a__add^#(x₁, x₂)]	=	1 + 1 · x₂
[a__first^#(x₁, x₂)]	=	1
[a__from^#(x₁)]	=	1 + 1 · x₁
[mark^#(x₁)]	=	1 · x₁ + 0
[and(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[if(x₁, x₂, x₃)]	=	1 + 1 · x₁ + 1 · x₂ + 1 · x₃
[add(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[first(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[from(x₁)]	=	1 + 1 · x₁
[true]	=	1
[false]	=	1
[0]	=	1
[s(x₁)]	=	1 + 1 · x₁
[nil]	=	1
[cons(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂

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

a__and^#(true,z0)	→	c(mark^#(z0))	(27)
a__and^#(false,z0)	→	c1	(29)
a__and^#(z0,z1)	→	c2	(31)
a__if^#(true,z0,z1)	→	c3(mark^#(z0))	(33)
a__if^#(false,z0,z1)	→	c4(mark^#(z1))	(35)
a__if^#(z0,z1,z2)	→	c5	(37)
a__add^#(0,z0)	→	c6(mark^#(z0))	(39)
a__add^#(s(z0),z1)	→	c7	(41)
a__add^#(z0,z1)	→	c8	(43)
a__first^#(0,z0)	→	c9	(45)
a__first^#(s(z0),cons(z1,z2))	→	c10	(47)
a__first^#(z0,z1)	→	c11	(49)
a__from^#(z0)	→	c12	(51)
a__from^#(z0)	→	c13	(53)
mark^#(and(z0,z1))	→	c14(a__and^#(mark(z0),z1),mark^#(z0))	(55)
mark^#(if(z0,z1,z2))	→	c15(a__if^#(mark(z0),z1,z2),mark^#(z0))	(57)
mark^#(add(z0,z1))	→	c16(a__add^#(mark(z0),z1),mark^#(z0))	(59)
mark^#(first(z0,z1))	→	c17(a__first^#(mark(z0),mark(z1)),mark^#(z0),mark^#(z1))	(61)
mark^#(from(z0))	→	c18(a__from^#(z0))	(63)
mark^#(true)	→	c19	(64)
mark^#(false)	→	c20	(65)
mark^#(0)	→	c21	(66)
mark^#(s(z0))	→	c22	(68)
mark^#(nil)	→	c23	(69)
mark^#(cons(z0,z1))	→	c24	(71)

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).