Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/Frederiksen_Glenstrup/lte)

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

lte(Cons(x',xs'),Cons(x,xs))	→	lte(xs',xs)	(1)
lte(Cons(x,xs),Nil)	→	False	(2)
even(Cons(x,Nil))	→	False	(3)
even(Cons(x',Cons(x,xs)))	→	even(xs)	(4)
notEmpty(Cons(x,xs))	→	True	(5)
notEmpty(Nil)	→	False	(6)
lte(Nil,y)	→	True	(7)
even(Nil)	→	True	(8)
goal(x,y)	→	and(lte(x,y),even(x))	(9)

and S is the following TRS.

and(False,False)	→	False	(10)
and(True,False)	→	False	(11)
and(False,True)	→	False	(12)
and(True,True)	→	True	(13)

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:

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

→

c4(lte^#(z1,z3))

(15)

originates from

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

→

lte(z1,z3)

(14)

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

→

(17)

originates from

lte(Cons(z0,z1),Nil)

→

False

(16)

lte^#(Nil,z0)

→

(19)

originates from

lte(Nil,z0)

→

True

(18)

even^#(Cons(z0,Nil))

→

(21)

originates from

even(Cons(z0,Nil))

→

False

(20)

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

→

c8(even^#(z2))

(23)

originates from

even(Cons(z0,Cons(z1,z2)))

→

even(z2)

(22)

even^#(Nil)

→

(24)

originates from

even(Nil)

→

True

(8)

notEmpty^#(Cons(z0,z1))

→

c10

(26)

originates from

notEmpty(Cons(z0,z1))

→

True

(25)

notEmpty^#(Nil)

→

c11

(27)

originates from

notEmpty(Nil)

→

False

(6)

goal^#(z0,z1)

→

c12(and^#(lte(z0,z1),even(z0)),lte^#(z0,z1),even^#(z0))

(29)

originates from

goal(z0,z1)

→

and(lte(z0,z1),even(z0))

(28)

and^#(False,False)

→

(30)

originates from

and(False,False)

→

False

(10)

and^#(True,False)

→

(31)

originates from

and(True,False)

→

False

(11)

and^#(False,True)

→

(32)

originates from

and(False,True)

→

False

(12)

and^#(True,True)

→

(33)

originates from

and(True,True)

→

True

(13)

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

and^#(False,False)

and^#(True,False)

and^#(False,True)

and^#(True,True)

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

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

lte^#(Nil,z0)

even^#(Cons(z0,Nil))

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

even^#(Nil)

notEmpty^#(Cons(z0,z1))

notEmpty^#(Nil)

goal^#(z0,z1)

1.1 Usable Rules

We remove the following rules since they are not usable.

and(False,False)	→	False	(10)
and(True,False)	→	False	(11)
and(False,True)	→	False	(12)
and(True,True)	→	True	(13)
notEmpty(Cons(z0,z1))	→	True	(25)
notEmpty(Nil)	→	False	(6)
goal(z0,z1)	→	and(lte(z0,z1),even(z0))	(28)

1.1.1 Rule Shifting

The rules

lte^#(Cons(z0,z1),Cons(z2,z3))	→	c4(lte^#(z1,z3))	(15)
lte^#(Cons(z0,z1),Nil)	→	c5	(17)
even^#(Cons(z0,Nil))	→	c7	(21)
even^#(Cons(z0,Cons(z1,z2)))	→	c8(even^#(z2))	(23)
even^#(Nil)	→	c9	(24)
notEmpty^#(Cons(z0,z1))	→	c10	(26)
notEmpty^#(Nil)	→	c11	(27)
goal^#(z0,z1)	→	c12(and^#(lte(z0,z1),even(z0)),lte^#(z0,z1),even^#(z0))	(29)

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

[c]	=	0
[c1]	=	0
[c2]	=	0
[c3]	=	0
[c4(x₁)]	=	1 · x₁ + 0
[c5]	=	0
[c6]	=	0
[c7]	=	0
[c8(x₁)]	=	1 · x₁ + 0
[c9]	=	0
[c10]	=	0
[c11]	=	0
[c12(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃
[lte(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[even(x₁)]	=	1 + 1 · x₁
[and^#(x₁, x₂)]	=	0
[lte^#(x₁, x₂)]	=	1 · x₂ + 0
[even^#(x₁)]	=	1 · x₁ + 0
[notEmpty^#(x₁)]	=	1 · x₁ + 0
[goal^#(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[Cons(x₁, x₂)]	=	1 + 1 · x₂
[Nil]	=	1
[False]	=	1
[True]	=	1

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

and^#(False,False)	→	c	(30)
and^#(True,False)	→	c1	(31)
and^#(False,True)	→	c2	(32)
and^#(True,True)	→	c3	(33)
lte^#(Cons(z0,z1),Cons(z2,z3))	→	c4(lte^#(z1,z3))	(15)
lte^#(Cons(z0,z1),Nil)	→	c5	(17)
lte^#(Nil,z0)	→	c6	(19)
even^#(Cons(z0,Nil))	→	c7	(21)
even^#(Cons(z0,Cons(z1,z2)))	→	c8(even^#(z2))	(23)
even^#(Nil)	→	c9	(24)
notEmpty^#(Cons(z0,z1))	→	c10	(26)
notEmpty^#(Nil)	→	c11	(27)
goal^#(z0,z1)	→	c12(and^#(lte(z0,z1),even(z0)),lte^#(z0,z1),even^#(z0))	(29)

1.1.1.1 Rule Shifting

The rules

lte^#(Nil,z0)

→

(19)

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

[c]	=	0
[c1]	=	0
[c2]	=	0
[c3]	=	0
[c4(x₁)]	=	1 · x₁ + 0
[c5]	=	0
[c6]	=	0
[c7]	=	0
[c8(x₁)]	=	1 · x₁ + 0
[c9]	=	0
[c10]	=	0
[c11]	=	0
[c12(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₂ + 1 · x₃
[lte(x₁, x₂)]	=	1 · x₁ + 0
[even(x₁)]	=	1 + 1 · x₁
[and^#(x₁, x₂)]	=	0
[lte^#(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[even^#(x₁)]	=	1
[notEmpty^#(x₁)]	=	0
[goal^#(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[Cons(x₁, x₂)]	=	1 + 1 · x₂
[Nil]	=	1
[False]	=	1
[True]	=	1

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

and^#(False,False)	→	c	(30)
and^#(True,False)	→	c1	(31)
and^#(False,True)	→	c2	(32)
and^#(True,True)	→	c3	(33)
lte^#(Cons(z0,z1),Cons(z2,z3))	→	c4(lte^#(z1,z3))	(15)
lte^#(Cons(z0,z1),Nil)	→	c5	(17)
lte^#(Nil,z0)	→	c6	(19)
even^#(Cons(z0,Nil))	→	c7	(21)
even^#(Cons(z0,Cons(z1,z2)))	→	c8(even^#(z2))	(23)
even^#(Nil)	→	c9	(24)
notEmpty^#(Cons(z0,z1))	→	c10	(26)
notEmpty^#(Nil)	→	c11	(27)
goal^#(z0,z1)	→	c12(and^#(lte(z0,z1),even(z0)),lte^#(z0,z1),even^#(z0))	(29)

1.1.1.1.1 R is empty

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