In the analysis of rev (either version), you prematurely argue that the cost
of the recursive call is 1. That argument can only be carried out in the
semantics, but you do it in the syntax. I'm afraid we cannot do that. It
obviously highlights the need for additional syntactic reasoning rules, and
maybe that is (ought to be) one the goals of this thesis: identify syntactic
reasoning (rules, equations, etc.) that are true in any semantics, and hence
we can apply to the syntax.
In the analysis of rev (either version), you prematurely argue that the cost of the recursive call is 1. That argument can only be carried out in the semantics, but you do it in the syntax. I'm afraid we cannot do that. It obviously highlights the need for additional syntactic reasoning rules, and maybe that is (ought to be) one the goals of this thesis: identify syntactic reasoning (rules, equations, etc.) that are true in any semantics, and hence we can apply to the syntax.