When you start describing the semantics of the recurrence extracted for fast reverse, you have a bunch of notation that is completely undefined. You need to explain what is going on here. It might be possible to give a higher-level description, and avoid the details of the general size-based denotational semantics.
When you start describing the semantics of the recurrence extracted for fast reverse, you have a bunch of notation that is completely undefined. You need to explain what is going on here. It might be possible to give a higher-level description, and avoid the details of the general size-based denotational semantics.