Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/hoca/dfs-flatten)

The rewrite relation of the following TRS is considered.

revApp#2(Nil,x16) → x16 (1)
revApp#2(Cons(x6,x4),x2) → revApp#2(x4,Cons(x6,x2)) (2)
dfsAcc#3(Leaf(x8),x16) → Cons(x8,x16) (3)
dfsAcc#3(Node(x6,x4),x2) → dfsAcc#3(x4,dfsAcc#3(x6,x2)) (4)
main(x1) → revApp#2(dfsAcc#3(x1,Nil),Nil) (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 2. This is shown by the following automaton.