Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/SK90/2.30)

The rewrite relation of the following TRS is considered.

not(x)	→	xor(x,true)	(1)
implies(x,y)	→	xor(and(x,y),xor(x,true))	(2)
or(x,y)	→	xor(and(x,y),xor(x,y))	(3)
=(x,y)	→	xor(x,xor(y,true))	(4)

The evaluation strategy is innermost.

Property / Task

Determine bounds on the runtime complexity.

Answer / Result

An upperbound for the complexity is O(1).

Proof (by AProVE @ termCOMP 2023)

1 Dependency Tuples

We get the following set of dependency tuples:

not^#(z0)

→

(6)

originates from

not(z0)

→

xor(z0,true)

(5)

implies^#(z0,z1)

→

(8)

originates from

implies(z0,z1)

→

xor(and(z0,z1),xor(z0,true))

(7)

or^#(z0,z1)

→

(10)

originates from

or(z0,z1)

→

xor(and(z0,z1),xor(z0,z1))

(9)

=^#(z0,z1)

→

(12)

originates from

=(z0,z1)

→

xor(z0,xor(z1,true))

(11)

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

not^#(z0)

implies^#(z0,z1)

or^#(z0,z1)

=^#(z0,z1)

1.1 Usable Rules

We remove the following rules since they are not usable.

not(z0)	→	xor(z0,true)	(5)
implies(z0,z1)	→	xor(and(z0,z1),xor(z0,true))	(7)
or(z0,z1)	→	xor(and(z0,z1),xor(z0,z1))	(9)
=(z0,z1)	→	xor(z0,xor(z1,true))	(11)

1.1.1 Rule Shifting

The rules

implies^#(z0,z1)	→	c1	(8)
=^#(z0,z1)	→	c3	(12)

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

[c]	=	0
[c1]	=	0
[c2]	=	0
[c3]	=	0
[not^#(x₁)]	=	0
[implies^#(x₁, x₂)]	=	1
[or^#(x₁, x₂)]	=	0
[=^#(x₁, x₂)]	=	1

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

not^#(z0)	→	c	(6)
implies^#(z0,z1)	→	c1	(8)
or^#(z0,z1)	→	c2	(10)
=^#(z0,z1)	→	c3	(12)

1.1.1.1 Rule Shifting

The rules

or^#(z0,z1)

→

(10)

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

[c]	=	0
[c1]	=	0
[c2]	=	0
[c3]	=	0
[not^#(x₁)]	=	0
[implies^#(x₁, x₂)]	=	0
[or^#(x₁, x₂)]	=	1
[=^#(x₁, x₂)]	=	0

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

not^#(z0)	→	c	(6)
implies^#(z0,z1)	→	c1	(8)
or^#(z0,z1)	→	c2	(10)
=^#(z0,z1)	→	c3	(12)

1.1.1.1.1 Rule Shifting

The rules

not^#(z0)

→

(6)

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

[c]	=	0
[c1]	=	0
[c2]	=	0
[c3]	=	0
[not^#(x₁)]	=	1
[implies^#(x₁, x₂)]	=	0
[or^#(x₁, x₂)]	=	0
[=^#(x₁, x₂)]	=	0

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

not^#(z0)	→	c	(6)
implies^#(z0,z1)	→	c1	(8)
or^#(z0,z1)	→	c2	(10)
=^#(z0,z1)	→	c3	(12)

1.1.1.1.1.1 R is empty

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