The representation built by rep has 2n+1 constructors. rev preserves that count, and abs traverses it once. Their three linear bounds add to Θ(n+1) total time, improving the direct quadratic reversal. The correctness equations for representation, reversal and abstraction compose to the required reversed list.