Join GitHub today
GitHub is home to over 40 million developers working together to host and review code, manage projects, and build software together.Sign up
Induction in the presence of mutually recursive functions #5
Imandra cannot generally synthesize induction schemes for mutually recursive functions, a lot of of the times in the presence of mutually recursive functions, induction would just never work.
Users can provide induction schemes manually (using a custom functional induction scheme), but usually it's much better (if possible) to write in a style that doesn't require mutual recursion (especially in higher order position)