You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
To solve freshness constraints (i.e., x \notin free_evars \phi), the freshness manager should not expand all conditions. One option for the optimization could be the following:
Deconstruct the goal into a list of subgoals for the metavariables. For example, x \notin \phi $ \psi could be deconstructed to x \notin \phi and x \notin \psi.
Solve the subgoals by using the fact that the metavariables are included in the freshness manager (by using the index_of tactic).
The text was updated successfully, but these errors were encountered:
To solve freshness constraints (i.e.,
x \notin free_evars \phi
), the freshness manager should not expand all conditions. One option for the optimization could be the following:x \notin \phi $ \psi
could be deconstructed tox \notin \phi
andx \notin \psi
.index_of
tactic).The text was updated successfully, but these errors were encountered: