Is there a way to disable termination checks for recursive predicate definitions that I know to be logically consistent?

Question

Is there a way to disable termination checks for recursive predicate definitions that I know to be logically consistent?

Answer

Well, first of all, be careful about thinking things like “I know this to be logically consistent”. Verifiers exist to check our human tendency to hand-wave over questionable assumptions.

That said, you can do something like this:

predicate P(x: int, terminationFiction: int)
  decreases terminationFiction
{
  assume 0 < terminationFiction;
  P(x, terminationFiction - 1)
}

That may cause some quantification triggering problems and may need an axiom like

forall x,j,k:int :: P(x, j) == P(x, k)

It can also help to manually instantiate an axiom to avoid triggering issues: declare the axiom like this:

lemma {:axiom} PSynonym(x: int, j: int, k: int)
  ensures P(x, j) == P(x, k)

and then call the lemma as needed.