Email Gateway (Aug 22 2022 at 18:54): Email Gateway (Aug 22 2022 at 18:54):From: Joachim Breitner <joachim@cis.upenn.edu>
Hi,
just a guess from the side lines, but when you define functions with
function (and not fun), you usually want to follow up with
termination by <termination_proof>
Only after termination of the equations is proven will the equations
you used be available as lemmas, and hence be picked up by
sledgehammer.
The problem in this case is that at least NextState is _not_
terminating, so using a function here seems wrong. In fact, your
function seems to be calculating no the _next_ state, but rather the
_final_ state.
Cheers,
Joachim
signature.asc
Last updated: Nov 21 2024 at 12:39 UTC