Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/Frederiksen_Others/thetrickSize)

The relative rewrite relation R/S is considered where R is the following TRS

lt0(Nil,Cons(x',xs))	→	True	(1)
lt0(Cons(x',xs'),Cons(x,xs))	→	lt0(xs',xs)	(2)
g(x,Nil)	→	Cons(Nil,Cons(Nil,Cons(Nil,Cons(Nil,Nil))))	(3)
f(x,Nil)	→	Cons(Nil,Cons(Nil,Cons(Nil,Cons(Nil,Nil))))	(4)
notEmpty(Cons(x,xs))	→	True	(5)
notEmpty(Nil)	→	False	(6)
lt0(x,Nil)	→	False	(7)
g(x,Cons(x',xs))	→	g[Ite][False][Ite](lt0(x,Cons(Nil,Nil)),x,Cons(x',xs))	(8)
f(x,Cons(x',xs))	→	f[Ite][False][Ite](lt0(x,Cons(Nil,Nil)),x,Cons(x',xs))	(9)
number4(n)	→	Cons(Nil,Cons(Nil,Cons(Nil,Cons(Nil,Nil))))	(10)
goal(x,y)	→	Cons(f(x,y),Cons(g(x,y),Nil))	(11)

and S is the following TRS.

g[Ite][False][Ite](False,Cons(x,xs),y)	→	g(xs,Cons(Cons(Nil,Nil),y))	(12)
g[Ite][False][Ite](True,x',Cons(x,xs))	→	g(x',xs)	(13)
f[Ite][False][Ite](False,Cons(x,xs),y)	→	f(xs,Cons(Cons(Nil,Nil),y))	(14)
f[Ite][False][Ite](True,x',Cons(x,xs))	→	f(x',xs)	(15)

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:

lt0^#(Nil,Cons(z0,z1))

→

(17)

originates from

lt0(Nil,Cons(z0,z1))

→

True

(16)

lt0^#(Cons(z0,z1),Cons(z2,z3))

→

c5(lt0^#(z1,z3))

(19)

originates from

lt0(Cons(z0,z1),Cons(z2,z3))

→

lt0(z1,z3)

(18)

lt0^#(z0,Nil)

→

(21)

originates from

lt0(z0,Nil)

→

False

(20)

g^#(z0,Nil)

→

(23)

originates from

g(z0,Nil)

→

Cons(Nil,Cons(Nil,Cons(Nil,Cons(Nil,Nil))))

(22)

g^#(z0,Cons(z1,z2))

→

c8(g[Ite][False][Ite]^#(lt0(z0,Cons(Nil,Nil)),z0,Cons(z1,z2)),lt0^#(z0,Cons(Nil,Nil)))

(25)

originates from

g(z0,Cons(z1,z2))

→

g[Ite][False][Ite](lt0(z0,Cons(Nil,Nil)),z0,Cons(z1,z2))

(24)

f^#(z0,Nil)

→

(27)

originates from

f(z0,Nil)

→

Cons(Nil,Cons(Nil,Cons(Nil,Cons(Nil,Nil))))

(26)

f^#(z0,Cons(z1,z2))

→

c10(f[Ite][False][Ite]^#(lt0(z0,Cons(Nil,Nil)),z0,Cons(z1,z2)),lt0^#(z0,Cons(Nil,Nil)))

(29)

originates from

f(z0,Cons(z1,z2))

→

f[Ite][False][Ite](lt0(z0,Cons(Nil,Nil)),z0,Cons(z1,z2))

(28)

notEmpty^#(Cons(z0,z1))

→

c11

(31)

originates from

notEmpty(Cons(z0,z1))

→

True

(30)

notEmpty^#(Nil)

→

c12

(32)

originates from

notEmpty(Nil)

→

False

(6)

number4^#(z0)

→

c13

(34)

originates from

number4(z0)

→

Cons(Nil,Cons(Nil,Cons(Nil,Cons(Nil,Nil))))

(33)

goal^#(z0,z1)

→

c14(f^#(z0,z1),g^#(z0,z1))

(36)

originates from

goal(z0,z1)

→

Cons(f(z0,z1),Cons(g(z0,z1),Nil))

(35)

g[Ite][False][Ite]^#(False,Cons(z0,z1),z2)

→

c(g^#(z1,Cons(Cons(Nil,Nil),z2)))

(38)

originates from

g[Ite][False][Ite](False,Cons(z0,z1),z2)

→

g(z1,Cons(Cons(Nil,Nil),z2))

(37)

g[Ite][False][Ite]^#(True,z0,Cons(z1,z2))

→

c1(g^#(z0,z2))

(40)

originates from

g[Ite][False][Ite](True,z0,Cons(z1,z2))

→

g(z0,z2)

(39)

f[Ite][False][Ite]^#(False,Cons(z0,z1),z2)

→

c2(f^#(z1,Cons(Cons(Nil,Nil),z2)))

(42)

originates from

f[Ite][False][Ite](False,Cons(z0,z1),z2)

→

f(z1,Cons(Cons(Nil,Nil),z2))

(41)

f[Ite][False][Ite]^#(True,z0,Cons(z1,z2))

→

c3(f^#(z0,z2))

(44)

originates from

f[Ite][False][Ite](True,z0,Cons(z1,z2))

→

f(z0,z2)

(43)

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

g[Ite][False][Ite]^#(False,Cons(z0,z1),z2)

g[Ite][False][Ite]^#(True,z0,Cons(z1,z2))

f[Ite][False][Ite]^#(False,Cons(z0,z1),z2)

f[Ite][False][Ite]^#(True,z0,Cons(z1,z2))

lt0^#(Nil,Cons(z0,z1))

lt0^#(Cons(z0,z1),Cons(z2,z3))

lt0^#(z0,Nil)

g^#(z0,Nil)

g^#(z0,Cons(z1,z2))

f^#(z0,Nil)

f^#(z0,Cons(z1,z2))

notEmpty^#(Cons(z0,z1))

notEmpty^#(Nil)

number4^#(z0)

goal^#(z0,z1)

1.1 Usable Rules

We remove the following rules since they are not usable.

g[Ite][False][Ite](False,Cons(z0,z1),z2)	→	g(z1,Cons(Cons(Nil,Nil),z2))	(37)
g[Ite][False][Ite](True,z0,Cons(z1,z2))	→	g(z0,z2)	(39)
f[Ite][False][Ite](False,Cons(z0,z1),z2)	→	f(z1,Cons(Cons(Nil,Nil),z2))	(41)
f[Ite][False][Ite](True,z0,Cons(z1,z2))	→	f(z0,z2)	(43)
g(z0,Nil)	→	Cons(Nil,Cons(Nil,Cons(Nil,Cons(Nil,Nil))))	(22)
g(z0,Cons(z1,z2))	→	g[Ite][False][Ite](lt0(z0,Cons(Nil,Nil)),z0,Cons(z1,z2))	(24)
f(z0,Nil)	→	Cons(Nil,Cons(Nil,Cons(Nil,Cons(Nil,Nil))))	(26)
f(z0,Cons(z1,z2))	→	f[Ite][False][Ite](lt0(z0,Cons(Nil,Nil)),z0,Cons(z1,z2))	(28)
notEmpty(Cons(z0,z1))	→	True	(30)
notEmpty(Nil)	→	False	(6)
number4(z0)	→	Cons(Nil,Cons(Nil,Cons(Nil,Cons(Nil,Nil))))	(33)
goal(z0,z1)	→	Cons(f(z0,z1),Cons(g(z0,z1),Nil))	(35)

1.1.1 Rule Shifting

The rules

notEmpty^#(Cons(z0,z1))	→	c11	(31)
notEmpty^#(Nil)	→	c12	(32)

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

[c(x₁)]	=	1 · x₁ + 0
[c1(x₁)]	=	1 · x₁ + 0
[c2(x₁)]	=	1 · x₁ + 0
[c3(x₁)]	=	1 · x₁ + 0
[c4]	=	0
[c5(x₁)]	=	1 · x₁ + 0
[c6]	=	0
[c7]	=	0
[c8(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c9]	=	0
[c10(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c11]	=	0
[c12]	=	0
[c13]	=	0
[c14(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[lt0(x₁, x₂)]	=	1 + 1 · x₁
[g[Ite][False][Ite]^#(x₁, x₂, x₃)]	=	1 · x₃ + 0
[f[Ite][False][Ite]^#(x₁, x₂, x₃)]	=	1 · x₃ + 0
[lt0^#(x₁, x₂)]	=	0
[g^#(x₁, x₂)]	=	0
[f^#(x₁, x₂)]	=	0
[notEmpty^#(x₁)]	=	1 + 1 · x₁
[number4^#(x₁)]	=	0
[goal^#(x₁, x₂)]	=	0
[Nil]	=	0
[Cons(x₁, x₂)]	=	0
[True]	=	1
[False]	=	1

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

g[Ite][False][Ite]^#(False,Cons(z0,z1),z2)	→	c(g^#(z1,Cons(Cons(Nil,Nil),z2)))	(38)
g[Ite][False][Ite]^#(True,z0,Cons(z1,z2))	→	c1(g^#(z0,z2))	(40)
f[Ite][False][Ite]^#(False,Cons(z0,z1),z2)	→	c2(f^#(z1,Cons(Cons(Nil,Nil),z2)))	(42)
f[Ite][False][Ite]^#(True,z0,Cons(z1,z2))	→	c3(f^#(z0,z2))	(44)
lt0^#(Nil,Cons(z0,z1))	→	c4	(17)
lt0^#(Cons(z0,z1),Cons(z2,z3))	→	c5(lt0^#(z1,z3))	(19)
lt0^#(z0,Nil)	→	c6	(21)
g^#(z0,Nil)	→	c7	(23)
g^#(z0,Cons(z1,z2))	→	c8(g[Ite][False][Ite]^#(lt0(z0,Cons(Nil,Nil)),z0,Cons(z1,z2)),lt0^#(z0,Cons(Nil,Nil)))	(25)
f^#(z0,Nil)	→	c9	(27)
f^#(z0,Cons(z1,z2))	→	c10(f[Ite][False][Ite]^#(lt0(z0,Cons(Nil,Nil)),z0,Cons(z1,z2)),lt0^#(z0,Cons(Nil,Nil)))	(29)
notEmpty^#(Cons(z0,z1))	→	c11	(31)
notEmpty^#(Nil)	→	c12	(32)
number4^#(z0)	→	c13	(34)
goal^#(z0,z1)	→	c14(f^#(z0,z1),g^#(z0,z1))	(36)

1.1.1.1 Rule Shifting

The rules

goal^#(z0,z1)

→

c14(f^#(z0,z1),g^#(z0,z1))

(36)

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

[c(x₁)]	=	1 · x₁ + 0
[c1(x₁)]	=	1 · x₁ + 0
[c2(x₁)]	=	1 · x₁ + 0
[c3(x₁)]	=	1 · x₁ + 0
[c4]	=	0
[c5(x₁)]	=	1 · x₁ + 0
[c6]	=	0
[c7]	=	0
[c8(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c9]	=	0
[c10(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c11]	=	0
[c12]	=	0
[c13]	=	0
[c14(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[lt0(x₁, x₂)]	=	1 + 1 · x₁
[g[Ite][False][Ite]^#(x₁, x₂, x₃)]	=	1 · x₃ + 0
[f[Ite][False][Ite]^#(x₁, x₂, x₃)]	=	1 · x₃ + 0
[lt0^#(x₁, x₂)]	=	0
[g^#(x₁, x₂)]	=	0
[f^#(x₁, x₂)]	=	0
[notEmpty^#(x₁)]	=	0
[number4^#(x₁)]	=	0
[goal^#(x₁, x₂)]	=	1
[Nil]	=	0
[Cons(x₁, x₂)]	=	0
[True]	=	1
[False]	=	1

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

g[Ite][False][Ite]^#(False,Cons(z0,z1),z2)	→	c(g^#(z1,Cons(Cons(Nil,Nil),z2)))	(38)
g[Ite][False][Ite]^#(True,z0,Cons(z1,z2))	→	c1(g^#(z0,z2))	(40)
f[Ite][False][Ite]^#(False,Cons(z0,z1),z2)	→	c2(f^#(z1,Cons(Cons(Nil,Nil),z2)))	(42)
f[Ite][False][Ite]^#(True,z0,Cons(z1,z2))	→	c3(f^#(z0,z2))	(44)
lt0^#(Nil,Cons(z0,z1))	→	c4	(17)
lt0^#(Cons(z0,z1),Cons(z2,z3))	→	c5(lt0^#(z1,z3))	(19)
lt0^#(z0,Nil)	→	c6	(21)
g^#(z0,Nil)	→	c7	(23)
g^#(z0,Cons(z1,z2))	→	c8(g[Ite][False][Ite]^#(lt0(z0,Cons(Nil,Nil)),z0,Cons(z1,z2)),lt0^#(z0,Cons(Nil,Nil)))	(25)
f^#(z0,Nil)	→	c9	(27)
f^#(z0,Cons(z1,z2))	→	c10(f[Ite][False][Ite]^#(lt0(z0,Cons(Nil,Nil)),z0,Cons(z1,z2)),lt0^#(z0,Cons(Nil,Nil)))	(29)
notEmpty^#(Cons(z0,z1))	→	c11	(31)
notEmpty^#(Nil)	→	c12	(32)
number4^#(z0)	→	c13	(34)
goal^#(z0,z1)	→	c14(f^#(z0,z1),g^#(z0,z1))	(36)

1.1.1.1.1 Rule Shifting

The rules

number4^#(z0)

→

c13

(34)

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

[c(x₁)]	=	1 · x₁ + 0
[c1(x₁)]	=	1 · x₁ + 0
[c2(x₁)]	=	1 · x₁ + 0
[c3(x₁)]	=	1 · x₁ + 0
[c4]	=	0
[c5(x₁)]	=	1 · x₁ + 0
[c6]	=	0
[c7]	=	0
[c8(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c9]	=	0
[c10(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c11]	=	0
[c12]	=	0
[c13]	=	0
[c14(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[lt0(x₁, x₂)]	=	1 + 1 · x₁
[g[Ite][False][Ite]^#(x₁, x₂, x₃)]	=	1 · x₃ + 0
[f[Ite][False][Ite]^#(x₁, x₂, x₃)]	=	1 · x₃ + 0
[lt0^#(x₁, x₂)]	=	0
[g^#(x₁, x₂)]	=	0
[f^#(x₁, x₂)]	=	0
[notEmpty^#(x₁)]	=	0
[number4^#(x₁)]	=	1
[goal^#(x₁, x₂)]	=	0
[Nil]	=	0
[Cons(x₁, x₂)]	=	0
[True]	=	1
[False]	=	1

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

g[Ite][False][Ite]^#(False,Cons(z0,z1),z2)	→	c(g^#(z1,Cons(Cons(Nil,Nil),z2)))	(38)
g[Ite][False][Ite]^#(True,z0,Cons(z1,z2))	→	c1(g^#(z0,z2))	(40)
f[Ite][False][Ite]^#(False,Cons(z0,z1),z2)	→	c2(f^#(z1,Cons(Cons(Nil,Nil),z2)))	(42)
f[Ite][False][Ite]^#(True,z0,Cons(z1,z2))	→	c3(f^#(z0,z2))	(44)
lt0^#(Nil,Cons(z0,z1))	→	c4	(17)
lt0^#(Cons(z0,z1),Cons(z2,z3))	→	c5(lt0^#(z1,z3))	(19)
lt0^#(z0,Nil)	→	c6	(21)
g^#(z0,Nil)	→	c7	(23)
g^#(z0,Cons(z1,z2))	→	c8(g[Ite][False][Ite]^#(lt0(z0,Cons(Nil,Nil)),z0,Cons(z1,z2)),lt0^#(z0,Cons(Nil,Nil)))	(25)
f^#(z0,Nil)	→	c9	(27)
f^#(z0,Cons(z1,z2))	→	c10(f[Ite][False][Ite]^#(lt0(z0,Cons(Nil,Nil)),z0,Cons(z1,z2)),lt0^#(z0,Cons(Nil,Nil)))	(29)
notEmpty^#(Cons(z0,z1))	→	c11	(31)
notEmpty^#(Nil)	→	c12	(32)
number4^#(z0)	→	c13	(34)
goal^#(z0,z1)	→	c14(f^#(z0,z1),g^#(z0,z1))	(36)

1.1.1.1.1.1 Rule Shifting

The rules

g^#(z0,Nil)

→

(23)

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

[c(x₁)]	=	1 · x₁ + 0
[c1(x₁)]	=	1 · x₁ + 0
[c2(x₁)]	=	1 · x₁ + 0
[c3(x₁)]	=	1 · x₁ + 0
[c4]	=	0
[c5(x₁)]	=	1 · x₁ + 0
[c6]	=	0
[c7]	=	0
[c8(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c9]	=	0
[c10(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c11]	=	0
[c12]	=	0
[c13]	=	0
[c14(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[lt0(x₁, x₂)]	=	1 + 1 · x₁
[g[Ite][False][Ite]^#(x₁, x₂, x₃)]	=	1 + 1 · x₃
[f[Ite][False][Ite]^#(x₁, x₂, x₃)]	=	1 · x₃ + 0
[lt0^#(x₁, x₂)]	=	0
[g^#(x₁, x₂)]	=	1
[f^#(x₁, x₂)]	=	0
[notEmpty^#(x₁)]	=	0
[number4^#(x₁)]	=	0
[goal^#(x₁, x₂)]	=	1
[Nil]	=	0
[Cons(x₁, x₂)]	=	0
[True]	=	1
[False]	=	1

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

g[Ite][False][Ite]^#(False,Cons(z0,z1),z2)	→	c(g^#(z1,Cons(Cons(Nil,Nil),z2)))	(38)
g[Ite][False][Ite]^#(True,z0,Cons(z1,z2))	→	c1(g^#(z0,z2))	(40)
f[Ite][False][Ite]^#(False,Cons(z0,z1),z2)	→	c2(f^#(z1,Cons(Cons(Nil,Nil),z2)))	(42)
f[Ite][False][Ite]^#(True,z0,Cons(z1,z2))	→	c3(f^#(z0,z2))	(44)
lt0^#(Nil,Cons(z0,z1))	→	c4	(17)
lt0^#(Cons(z0,z1),Cons(z2,z3))	→	c5(lt0^#(z1,z3))	(19)
lt0^#(z0,Nil)	→	c6	(21)
g^#(z0,Nil)	→	c7	(23)
g^#(z0,Cons(z1,z2))	→	c8(g[Ite][False][Ite]^#(lt0(z0,Cons(Nil,Nil)),z0,Cons(z1,z2)),lt0^#(z0,Cons(Nil,Nil)))	(25)
f^#(z0,Nil)	→	c9	(27)
f^#(z0,Cons(z1,z2))	→	c10(f[Ite][False][Ite]^#(lt0(z0,Cons(Nil,Nil)),z0,Cons(z1,z2)),lt0^#(z0,Cons(Nil,Nil)))	(29)
notEmpty^#(Cons(z0,z1))	→	c11	(31)
notEmpty^#(Nil)	→	c12	(32)
number4^#(z0)	→	c13	(34)
goal^#(z0,z1)	→	c14(f^#(z0,z1),g^#(z0,z1))	(36)

1.1.1.1.1.1.1 Rule Shifting

The rules

f^#(z0,Nil)

→

(27)

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

[c(x₁)]	=	1 · x₁ + 0
[c1(x₁)]	=	1 · x₁ + 0
[c2(x₁)]	=	1 · x₁ + 0
[c3(x₁)]	=	1 · x₁ + 0
[c4]	=	0
[c5(x₁)]	=	1 · x₁ + 0
[c6]	=	0
[c7]	=	0
[c8(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c9]	=	0
[c10(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c11]	=	0
[c12]	=	0
[c13]	=	0
[c14(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[lt0(x₁, x₂)]	=	1 + 1 · x₁
[g[Ite][False][Ite]^#(x₁, x₂, x₃)]	=	1 · x₃ + 0
[f[Ite][False][Ite]^#(x₁, x₂, x₃)]	=	1 + 1 · x₃
[lt0^#(x₁, x₂)]	=	0
[g^#(x₁, x₂)]	=	0
[f^#(x₁, x₂)]	=	1
[notEmpty^#(x₁)]	=	0
[number4^#(x₁)]	=	0
[goal^#(x₁, x₂)]	=	1
[Nil]	=	0
[Cons(x₁, x₂)]	=	0
[True]	=	1
[False]	=	1

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

g[Ite][False][Ite]^#(False,Cons(z0,z1),z2)	→	c(g^#(z1,Cons(Cons(Nil,Nil),z2)))	(38)
g[Ite][False][Ite]^#(True,z0,Cons(z1,z2))	→	c1(g^#(z0,z2))	(40)
f[Ite][False][Ite]^#(False,Cons(z0,z1),z2)	→	c2(f^#(z1,Cons(Cons(Nil,Nil),z2)))	(42)
f[Ite][False][Ite]^#(True,z0,Cons(z1,z2))	→	c3(f^#(z0,z2))	(44)
lt0^#(Nil,Cons(z0,z1))	→	c4	(17)
lt0^#(Cons(z0,z1),Cons(z2,z3))	→	c5(lt0^#(z1,z3))	(19)
lt0^#(z0,Nil)	→	c6	(21)
g^#(z0,Nil)	→	c7	(23)
g^#(z0,Cons(z1,z2))	→	c8(g[Ite][False][Ite]^#(lt0(z0,Cons(Nil,Nil)),z0,Cons(z1,z2)),lt0^#(z0,Cons(Nil,Nil)))	(25)
f^#(z0,Nil)	→	c9	(27)
f^#(z0,Cons(z1,z2))	→	c10(f[Ite][False][Ite]^#(lt0(z0,Cons(Nil,Nil)),z0,Cons(z1,z2)),lt0^#(z0,Cons(Nil,Nil)))	(29)
notEmpty^#(Cons(z0,z1))	→	c11	(31)
notEmpty^#(Nil)	→	c12	(32)
number4^#(z0)	→	c13	(34)
goal^#(z0,z1)	→	c14(f^#(z0,z1),g^#(z0,z1))	(36)

1.1.1.1.1.1.1.1 Rule Shifting

The rules

f^#(z0,Cons(z1,z2))

→

c10(f[Ite][False][Ite]^#(lt0(z0,Cons(Nil,Nil)),z0,Cons(z1,z2)),lt0^#(z0,Cons(Nil,Nil)))

(29)

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

[c(x₁)]	=	1 · x₁ + 0
[c1(x₁)]	=	1 · x₁ + 0
[c2(x₁)]	=	1 · x₁ + 0
[c3(x₁)]	=	1 · x₁ + 0
[c4]	=	0
[c5(x₁)]	=	1 · x₁ + 0
[c6]	=	0
[c7]	=	0
[c8(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c9]	=	0
[c10(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c11]	=	0
[c12]	=	0
[c13]	=	0
[c14(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[lt0(x₁, x₂)]	=	0
[g[Ite][False][Ite]^#(x₁, x₂, x₃)]	=	0
[f[Ite][False][Ite]^#(x₁, x₂, x₃)]	=	2 + 3 · x₂ + 2 · x₃
[lt0^#(x₁, x₂)]	=	0
[g^#(x₁, x₂)]	=	0
[f^#(x₁, x₂)]	=	3 + 3 · x₁ + 2 · x₂
[notEmpty^#(x₁)]	=	0
[number4^#(x₁)]	=	0
[goal^#(x₁, x₂)]	=	3 + 3 · x₁ + 2 · x₂
[Nil]	=	0
[Cons(x₁, x₂)]	=	2 + 1 · x₂
[True]	=	0
[False]	=	0

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

g[Ite][False][Ite]^#(False,Cons(z0,z1),z2)	→	c(g^#(z1,Cons(Cons(Nil,Nil),z2)))	(38)
g[Ite][False][Ite]^#(True,z0,Cons(z1,z2))	→	c1(g^#(z0,z2))	(40)
f[Ite][False][Ite]^#(False,Cons(z0,z1),z2)	→	c2(f^#(z1,Cons(Cons(Nil,Nil),z2)))	(42)
f[Ite][False][Ite]^#(True,z0,Cons(z1,z2))	→	c3(f^#(z0,z2))	(44)
lt0^#(Nil,Cons(z0,z1))	→	c4	(17)
lt0^#(Cons(z0,z1),Cons(z2,z3))	→	c5(lt0^#(z1,z3))	(19)
lt0^#(z0,Nil)	→	c6	(21)
g^#(z0,Nil)	→	c7	(23)
g^#(z0,Cons(z1,z2))	→	c8(g[Ite][False][Ite]^#(lt0(z0,Cons(Nil,Nil)),z0,Cons(z1,z2)),lt0^#(z0,Cons(Nil,Nil)))	(25)
f^#(z0,Nil)	→	c9	(27)
f^#(z0,Cons(z1,z2))	→	c10(f[Ite][False][Ite]^#(lt0(z0,Cons(Nil,Nil)),z0,Cons(z1,z2)),lt0^#(z0,Cons(Nil,Nil)))	(29)
notEmpty^#(Cons(z0,z1))	→	c11	(31)
notEmpty^#(Nil)	→	c12	(32)
number4^#(z0)	→	c13	(34)
goal^#(z0,z1)	→	c14(f^#(z0,z1),g^#(z0,z1))	(36)

1.1.1.1.1.1.1.1.1 Rule Shifting

The rules

g^#(z0,Cons(z1,z2))

→

c8(g[Ite][False][Ite]^#(lt0(z0,Cons(Nil,Nil)),z0,Cons(z1,z2)),lt0^#(z0,Cons(Nil,Nil)))

(25)

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

[c(x₁)]	=	1 · x₁ + 0
[c1(x₁)]	=	1 · x₁ + 0
[c2(x₁)]	=	1 · x₁ + 0
[c3(x₁)]	=	1 · x₁ + 0
[c4]	=	0
[c5(x₁)]	=	1 · x₁ + 0
[c6]	=	0
[c7]	=	0
[c8(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c9]	=	0
[c10(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c11]	=	0
[c12]	=	0
[c13]	=	0
[c14(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[lt0(x₁, x₂)]	=	0
[g[Ite][False][Ite]^#(x₁, x₂, x₃)]	=	3 · x₂ + 0 + 2 · x₃
[f[Ite][False][Ite]^#(x₁, x₂, x₃)]	=	0
[lt0^#(x₁, x₂)]	=	0
[g^#(x₁, x₂)]	=	1 + 3 · x₁ + 2 · x₂
[f^#(x₁, x₂)]	=	0
[notEmpty^#(x₁)]	=	0
[number4^#(x₁)]	=	0
[goal^#(x₁, x₂)]	=	1 + 3 · x₁ + 2 · x₂
[Nil]	=	0
[Cons(x₁, x₂)]	=	2 + 1 · x₂
[True]	=	0
[False]	=	0

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

g[Ite][False][Ite]^#(False,Cons(z0,z1),z2)	→	c(g^#(z1,Cons(Cons(Nil,Nil),z2)))	(38)
g[Ite][False][Ite]^#(True,z0,Cons(z1,z2))	→	c1(g^#(z0,z2))	(40)
f[Ite][False][Ite]^#(False,Cons(z0,z1),z2)	→	c2(f^#(z1,Cons(Cons(Nil,Nil),z2)))	(42)
f[Ite][False][Ite]^#(True,z0,Cons(z1,z2))	→	c3(f^#(z0,z2))	(44)
lt0^#(Nil,Cons(z0,z1))	→	c4	(17)
lt0^#(Cons(z0,z1),Cons(z2,z3))	→	c5(lt0^#(z1,z3))	(19)
lt0^#(z0,Nil)	→	c6	(21)
g^#(z0,Nil)	→	c7	(23)
g^#(z0,Cons(z1,z2))	→	c8(g[Ite][False][Ite]^#(lt0(z0,Cons(Nil,Nil)),z0,Cons(z1,z2)),lt0^#(z0,Cons(Nil,Nil)))	(25)
f^#(z0,Nil)	→	c9	(27)
f^#(z0,Cons(z1,z2))	→	c10(f[Ite][False][Ite]^#(lt0(z0,Cons(Nil,Nil)),z0,Cons(z1,z2)),lt0^#(z0,Cons(Nil,Nil)))	(29)
notEmpty^#(Cons(z0,z1))	→	c11	(31)
notEmpty^#(Nil)	→	c12	(32)
number4^#(z0)	→	c13	(34)
goal^#(z0,z1)	→	c14(f^#(z0,z1),g^#(z0,z1))	(36)

1.1.1.1.1.1.1.1.1.1 Rule Shifting

The rules

lt0^#(Nil,Cons(z0,z1))	→	c4	(17)
lt0^#(Cons(z0,z1),Cons(z2,z3))	→	c5(lt0^#(z1,z3))	(19)

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

[c(x₁)]	=	1 · x₁ + 0
[c1(x₁)]	=	1 · x₁ + 0
[c2(x₁)]	=	1 · x₁ + 0
[c3(x₁)]	=	1 · x₁ + 0
[c4]	=	0
[c5(x₁)]	=	1 · x₁ + 0
[c6]	=	0
[c7]	=	0
[c8(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c9]	=	0
[c10(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c11]	=	0
[c12]	=	0
[c13]	=	0
[c14(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[lt0(x₁, x₂)]	=	0
[g[Ite][False][Ite]^#(x₁, x₂, x₃)]	=	1 · x₂ · x₃ + 0 + 1 · x₂ · x₂
[f[Ite][False][Ite]^#(x₁, x₂, x₃)]	=	1 · x₂ · x₃ + 0 + 1 · x₂ · x₂
[lt0^#(x₁, x₂)]	=	1 · x₁ + 0
[g^#(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₁ · x₂ + 1 · x₁ · x₁
[f^#(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₁ · x₂ + 1 · x₁ · x₁
[notEmpty^#(x₁)]	=	0
[number4^#(x₁)]	=	0
[goal^#(x₁, x₂)]	=	1 + 2 · x₁ + 2 · x₂ + 1 · x₂ · x₂ + 2 · x₁ · x₂ + 2 · x₁ · x₁
[Nil]	=	1
[Cons(x₁, x₂)]	=	1 + 1 · x₂
[True]	=	0
[False]	=	0

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

g[Ite][False][Ite]^#(False,Cons(z0,z1),z2)	→	c(g^#(z1,Cons(Cons(Nil,Nil),z2)))	(38)
g[Ite][False][Ite]^#(True,z0,Cons(z1,z2))	→	c1(g^#(z0,z2))	(40)
f[Ite][False][Ite]^#(False,Cons(z0,z1),z2)	→	c2(f^#(z1,Cons(Cons(Nil,Nil),z2)))	(42)
f[Ite][False][Ite]^#(True,z0,Cons(z1,z2))	→	c3(f^#(z0,z2))	(44)
lt0^#(Nil,Cons(z0,z1))	→	c4	(17)
lt0^#(Cons(z0,z1),Cons(z2,z3))	→	c5(lt0^#(z1,z3))	(19)
lt0^#(z0,Nil)	→	c6	(21)
g^#(z0,Nil)	→	c7	(23)
g^#(z0,Cons(z1,z2))	→	c8(g[Ite][False][Ite]^#(lt0(z0,Cons(Nil,Nil)),z0,Cons(z1,z2)),lt0^#(z0,Cons(Nil,Nil)))	(25)
f^#(z0,Nil)	→	c9	(27)
f^#(z0,Cons(z1,z2))	→	c10(f[Ite][False][Ite]^#(lt0(z0,Cons(Nil,Nil)),z0,Cons(z1,z2)),lt0^#(z0,Cons(Nil,Nil)))	(29)
notEmpty^#(Cons(z0,z1))	→	c11	(31)
notEmpty^#(Nil)	→	c12	(32)
number4^#(z0)	→	c13	(34)
goal^#(z0,z1)	→	c14(f^#(z0,z1),g^#(z0,z1))	(36)

1.1.1.1.1.1.1.1.1.1.1 Rule Shifting

The rules

lt0^#(z0,Nil)

→

(21)

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

[c(x₁)]	=	1 · x₁ + 0
[c1(x₁)]	=	1 · x₁ + 0
[c2(x₁)]	=	1 · x₁ + 0
[c3(x₁)]	=	1 · x₁ + 0
[c4]	=	0
[c5(x₁)]	=	1 · x₁ + 0
[c6]	=	0
[c7]	=	0
[c8(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c9]	=	0
[c10(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c11]	=	0
[c12]	=	0
[c13]	=	0
[c14(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[lt0(x₁, x₂)]	=	0
[g[Ite][False][Ite]^#(x₁, x₂, x₃)]	=	1 · x₂ + 0 + 1 · x₃ · x₃ + 2 · x₂ · x₃ + 1 · x₂ · x₂
[f[Ite][False][Ite]^#(x₁, x₂, x₃)]	=	1 · x₃ + 0 + 1 · x₂ · x₂
[lt0^#(x₁, x₂)]	=	1
[g^#(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂ · x₂ + 2 · x₁ · x₂ + 1 · x₁ · x₁
[f^#(x₁, x₂)]	=	1 + 1 · x₂ + 1 · x₁ · x₁
[notEmpty^#(x₁)]	=	0
[number4^#(x₁)]	=	0
[goal^#(x₁, x₂)]	=	2 + 2 · x₁ + 1 · x₂ + 1 · x₂ · x₂ + 2 · x₁ · x₂ + 2 · x₁ · x₁
[Nil]	=	0
[Cons(x₁, x₂)]	=	2 + 1 · x₂
[True]	=	0
[False]	=	0

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

g[Ite][False][Ite]^#(False,Cons(z0,z1),z2)	→	c(g^#(z1,Cons(Cons(Nil,Nil),z2)))	(38)
g[Ite][False][Ite]^#(True,z0,Cons(z1,z2))	→	c1(g^#(z0,z2))	(40)
f[Ite][False][Ite]^#(False,Cons(z0,z1),z2)	→	c2(f^#(z1,Cons(Cons(Nil,Nil),z2)))	(42)
f[Ite][False][Ite]^#(True,z0,Cons(z1,z2))	→	c3(f^#(z0,z2))	(44)
lt0^#(Nil,Cons(z0,z1))	→	c4	(17)
lt0^#(Cons(z0,z1),Cons(z2,z3))	→	c5(lt0^#(z1,z3))	(19)
lt0^#(z0,Nil)	→	c6	(21)
g^#(z0,Nil)	→	c7	(23)
g^#(z0,Cons(z1,z2))	→	c8(g[Ite][False][Ite]^#(lt0(z0,Cons(Nil,Nil)),z0,Cons(z1,z2)),lt0^#(z0,Cons(Nil,Nil)))	(25)
f^#(z0,Nil)	→	c9	(27)
f^#(z0,Cons(z1,z2))	→	c10(f[Ite][False][Ite]^#(lt0(z0,Cons(Nil,Nil)),z0,Cons(z1,z2)),lt0^#(z0,Cons(Nil,Nil)))	(29)
notEmpty^#(Cons(z0,z1))	→	c11	(31)
notEmpty^#(Nil)	→	c12	(32)
number4^#(z0)	→	c13	(34)
goal^#(z0,z1)	→	c14(f^#(z0,z1),g^#(z0,z1))	(36)

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