[Why3-club] cannot prove termination

Jean-Christophe Filliâtre Jean-Christophe.Filliatre at lri.fr
Wed Nov 13 08:00:10 CET 2013

Hi Cláudio,

> I guess the question is more: What type structures can Why3 easily
> deduce termination for?

Why3 looks for a lexicographic order of arguments that guarantees a
structural descent over algebraic data types.

In your case, there is a structural descent in the first recursive call
(on both arguments) but no in the second recursive call (no descent at
all, on either argument).

You have no other choice than switching to a program function (with "let
rec") and using a variant.

PS: Note that the pattern matching in your function f is not exhaustive;
cases A, C _ and C _, A are missing.


More information about the Why3-club mailing list