Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/SK90/2.31)

The rewrite relation of the following TRS is considered.

not(true)	→	false	(1)
not(false)	→	true	(2)
odd(0)	→	false	(3)
odd(s(x))	→	not(odd(x))	(4)
+(x,0)	→	x	(5)
+(x,s(y))	→	s(+(x,y))	(6)
+(s(x),y)	→	s(+(x,y))	(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 Bounds

The given TRS is match-(raise)-bounded by 2. This is shown by the following automaton.

final states:

{0, 1, 2, 3}

transitions:

true₀	→	0
false₀	→	0
0₀	→	0
s₀(0)	→	0
not₀(0)	→	1
odd₀(0)	→	2
+₀(0,0)	→	3
false₁	→	1
true₁	→	1
false₁	→	2
odd₁(0)	→	4
not₁(4)	→	2
+₁(0,0)	→	5
s₁(5)	→	3
false₁	→	4
not₁(4)	→	4
s₁(5)	→	5
true₂	→	2
true₂	→	4
false₂	→	2
false₂	→	4
0	→	3
0	→	5