Fix: Kernel Substitution Fresh ID Generation
Substituting in the presence of bound variables produces dubious results when the fresh ID is not calculated properly.
Consider the following lambda formula
val L = x_1 => \forall x. P(x)
Expected:
L(y) = \forall x. P(x)
L(f(x)) = \forall x. P(x)
Actual:
L(y) = \forall x. P(x)
L(f(x)) = \forall x_1. P(f(x))
During substitution, on reaching the quantifier, the variable x
is spotted as occurring in the substitution x_1 => f(x)
, and based on the discovered set of free variables {x}
, is renamed to x_1
, leading to the substitution above.
PR adds substitution keys, in this case {x_1}
to the free variable pool for renaming, leading to correct results.
Also added a test to account for this.