Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/SK90/2.44)

The rewrite relation of the following TRS is considered.

del(.(x,.(y,z)))	→	f(=(x,y),x,y,z)	(1)
f(true,x,y,z)	→	del(.(y,z))	(2)
f(false,x,y,z)	→	.(x,del(.(y,z)))	(3)
=(nil,nil)	→	true	(4)
=(.(x,y),nil)	→	false	(5)
=(nil,.(y,z))	→	false	(6)
=(.(x,y),.(u,v))	→	and(=(x,u),=(y,v))	(7)

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:

del^#(.(z0,.(z1,z2)))

→

c(f^#(=(z0,z1),z0,z1,z2),=^#(z0,z1))

(9)

originates from

del(.(z0,.(z1,z2)))

→

f(=(z0,z1),z0,z1,z2)

(8)

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

→

c1(del^#(.(z1,z2)))

(11)

originates from

f(true,z0,z1,z2)

→

del(.(z1,z2))

(10)

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

→

c2(del^#(.(z1,z2)))

(13)

originates from

f(false,z0,z1,z2)

→

.(z0,del(.(z1,z2)))

(12)

=^#(nil,nil)

→

(14)

originates from

=(nil,nil)

→

true

(4)

=^#(.(z0,z1),nil)

→

(16)

originates from

=(.(z0,z1),nil)

→

false

(15)

=^#(nil,.(z0,z1))

→

(18)

originates from

=(nil,.(z0,z1))

→

false

(17)

=^#(.(z0,z1),.(u,v))

→

c6(=^#(z0,u),=^#(z1,v))

(20)

originates from

=(.(z0,z1),.(u,v))

→

and(=(z0,u),=(z1,v))

(19)

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

del^#(.(z0,.(z1,z2)))

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

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

=^#(nil,nil)

=^#(.(z0,z1),nil)

=^#(nil,.(z0,z1))

=^#(.(z0,z1),.(u,v))

1.1 Usable Rules

We remove the following rules since they are not usable.

del(.(z0,.(z1,z2)))	→	f(=(z0,z1),z0,z1,z2)	(8)
f(true,z0,z1,z2)	→	del(.(z1,z2))	(10)
f(false,z0,z1,z2)	→	.(z0,del(.(z1,z2)))	(12)

1.1.1 Rule Shifting

The rules

del^#(.(z0,.(z1,z2)))

→

c(f^#(=(z0,z1),z0,z1,z2),=^#(z0,z1))

(9)

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

[c(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c1(x₁)]	=	1 · x₁ + 0
[c2(x₁)]	=	1 · x₁ + 0
[c3]	=	0
[c4]	=	0
[c5]	=	0
[c6(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[=(x₁, x₂)]	=	1
[del^#(x₁)]	=	1 · x₁ + 0
[f^#(x₁,...,x₄)]	=	1 + 1 · x₄
[=^#(x₁, x₂)]	=	0
[nil]	=	1
[true]	=	1
[.(x₁, x₂)]	=	1 + 1 · x₂
[false]	=	1
[u]	=	1
[v]	=	1
[and(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂

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

del^#(.(z0,.(z1,z2)))	→	c(f^#(=(z0,z1),z0,z1,z2),=^#(z0,z1))	(9)
f^#(true,z0,z1,z2)	→	c1(del^#(.(z1,z2)))	(11)
f^#(false,z0,z1,z2)	→	c2(del^#(.(z1,z2)))	(13)
=^#(nil,nil)	→	c3	(14)
=^#(.(z0,z1),nil)	→	c4	(16)
=^#(nil,.(z0,z1))	→	c5	(18)
=^#(.(z0,z1),.(u,v))	→	c6(=^#(z0,u),=^#(z1,v))	(20)

1.1.1.1 Rule Shifting

The rules

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

→

c1(del^#(.(z1,z2)))

(11)

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

[c(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c1(x₁)]	=	1 · x₁ + 0
[c2(x₁)]	=	1 · x₁ + 0
[c3]	=	0
[c4]	=	0
[c5]	=	0
[c6(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[=(x₁, x₂)]	=	1 · x₁ + 0
[del^#(x₁)]	=	1 · x₁ + 0
[f^#(x₁,...,x₄)]	=	1 · x₁ + 0 + 1 · x₃ + 1 · x₄
[=^#(x₁, x₂)]	=	0
[nil]	=	1
[true]	=	1
[.(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[false]	=	0
[u]	=	1
[v]	=	1
[and(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂

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

del^#(.(z0,.(z1,z2)))	→	c(f^#(=(z0,z1),z0,z1,z2),=^#(z0,z1))	(9)
f^#(true,z0,z1,z2)	→	c1(del^#(.(z1,z2)))	(11)
f^#(false,z0,z1,z2)	→	c2(del^#(.(z1,z2)))	(13)
=^#(nil,nil)	→	c3	(14)
=^#(.(z0,z1),nil)	→	c4	(16)
=^#(nil,.(z0,z1))	→	c5	(18)
=^#(.(z0,z1),.(u,v))	→	c6(=^#(z0,u),=^#(z1,v))	(20)
=(.(z0,z1),nil)	→	false	(15)
=(nil,.(z0,z1))	→	false	(17)
=(.(z0,z1),.(u,v))	→	and(=(z0,u),=(z1,v))	(19)
=(nil,nil)	→	true	(4)

1.1.1.1.1 Rule Shifting

The rules

=^#(.(z0,z1),nil)	→	c4	(16)
=^#(.(z0,z1),.(u,v))	→	c6(=^#(z0,u),=^#(z1,v))	(20)

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

[c(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c1(x₁)]	=	1 · x₁ + 0
[c2(x₁)]	=	1 · x₁ + 0
[c3]	=	0
[c4]	=	0
[c5]	=	0
[c6(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[=(x₁, x₂)]	=	3 + 3 · x₁ + 3 · x₂
[del^#(x₁)]	=	1 · x₁ + 0
[f^#(x₁,...,x₄)]	=	3 + 1 · x₃ + 1 · x₄
[=^#(x₁, x₂)]	=	1 · x₁ + 0
[nil]	=	0
[true]	=	2
[.(x₁, x₂)]	=	3 + 1 · x₁ + 1 · x₂
[false]	=	0
[u]	=	3
[v]	=	0
[and(x₁, x₂)]	=	0

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

del^#(.(z0,.(z1,z2)))	→	c(f^#(=(z0,z1),z0,z1,z2),=^#(z0,z1))	(9)
f^#(true,z0,z1,z2)	→	c1(del^#(.(z1,z2)))	(11)
f^#(false,z0,z1,z2)	→	c2(del^#(.(z1,z2)))	(13)
=^#(nil,nil)	→	c3	(14)
=^#(.(z0,z1),nil)	→	c4	(16)
=^#(nil,.(z0,z1))	→	c5	(18)
=^#(.(z0,z1),.(u,v))	→	c6(=^#(z0,u),=^#(z1,v))	(20)

1.1.1.1.1.1 Rule Shifting

The rules

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

→

c2(del^#(.(z1,z2)))

(13)

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

[c(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c1(x₁)]	=	1 · x₁ + 0
[c2(x₁)]	=	1 · x₁ + 0
[c3]	=	0
[c4]	=	0
[c5]	=	0
[c6(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[=(x₁, x₂)]	=	1 + 1 · x₁
[del^#(x₁)]	=	1 · x₁ + 0
[f^#(x₁,...,x₄)]	=	1 + 1 · x₁ + 1 · x₃ + 1 · x₄
[=^#(x₁, x₂)]	=	0
[nil]	=	1
[true]	=	1
[.(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[false]	=	1
[u]	=	1
[v]	=	1
[and(x₁, x₂)]	=	0

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

del^#(.(z0,.(z1,z2)))	→	c(f^#(=(z0,z1),z0,z1,z2),=^#(z0,z1))	(9)
f^#(true,z0,z1,z2)	→	c1(del^#(.(z1,z2)))	(11)
f^#(false,z0,z1,z2)	→	c2(del^#(.(z1,z2)))	(13)
=^#(nil,nil)	→	c3	(14)
=^#(.(z0,z1),nil)	→	c4	(16)
=^#(nil,.(z0,z1))	→	c5	(18)
=^#(.(z0,z1),.(u,v))	→	c6(=^#(z0,u),=^#(z1,v))	(20)
=(.(z0,z1),nil)	→	false	(15)
=(nil,.(z0,z1))	→	false	(17)
=(.(z0,z1),.(u,v))	→	and(=(z0,u),=(z1,v))	(19)
=(nil,nil)	→	true	(4)

1.1.1.1.1.1.1 Rule Shifting

The rules

=^#(nil,nil)	→	c3	(14)
=^#(nil,.(z0,z1))	→	c5	(18)

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

[c(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c1(x₁)]	=	1 · x₁ + 0
[c2(x₁)]	=	1 · x₁ + 0
[c3]	=	0
[c4]	=	0
[c5]	=	0
[c6(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[=(x₁, x₂)]	=	1 + 1 · x₂
[del^#(x₁)]	=	1 · x₁ + 0
[f^#(x₁,...,x₄)]	=	1 · x₃ + 0 + 1 · x₄
[=^#(x₁, x₂)]	=	1 · x₁ + 0
[nil]	=	1
[true]	=	1
[.(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[false]	=	1
[u]	=	0
[v]	=	1
[and(x₁, x₂)]	=	0

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

del^#(.(z0,.(z1,z2)))	→	c(f^#(=(z0,z1),z0,z1,z2),=^#(z0,z1))	(9)
f^#(true,z0,z1,z2)	→	c1(del^#(.(z1,z2)))	(11)
f^#(false,z0,z1,z2)	→	c2(del^#(.(z1,z2)))	(13)
=^#(nil,nil)	→	c3	(14)
=^#(.(z0,z1),nil)	→	c4	(16)
=^#(nil,.(z0,z1))	→	c5	(18)
=^#(.(z0,z1),.(u,v))	→	c6(=^#(z0,u),=^#(z1,v))	(20)

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