Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/AG01/#3.37)

The rewrite relation of the following TRS is considered.

not(true) → false (1)
not(false) → true (2)
evenodd(x,0) → not(evenodd(x,s(0))) (3)
evenodd(0,s(0)) → false (4)
evenodd(s(x),s(0)) → evenodd(x,0) (5)
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 3. This is shown by the following automaton.