The problem occurs in those DB subterms that the recursive function does
not see as protected by a binder. For example:
abstract "X" ty (1 (g (y\ h1 X))) ->
x\ 1 (g (y\ h1 `2) ->
x\ x (g (y\ y x))
So there is a capture at the top that was not envisioned by the method.
These "unprotected DBs" are to be incremented to account for the new
lambda that will wrap the resulting term.
The problem occurs in those DB subterms that the recursive function does not see as protected by a binder. For example:
abstract "X" ty (
1 (g (y\ h1 X))) -> x\1 (g (y\ h1 `2) -> x\ x (g (y\ y x))So there is a capture at the top that was not envisioned by the method. These "unprotected DBs" are to be incremented to account for the new lambda that will wrap the resulting term.
This commit addresses issue #82.