Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/Transformed_CSR_04/Ex1_Zan97_GM)

The rewrite relation of the following TRS is considered.

a__g(X) → a__h(X) (1)
a__c → d (2)
a__h(d) → a__g(c) (3)
mark(g(X)) → a__g(X) (4)
mark(h(X)) → a__h(X) (5)
mark(c) → a__c (6)
mark(d) → d (7)
a__g(X) → g(X) (8)
a__h(X) → h(X) (9)
a__c → c (10)
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.