[Why3-club] cannot prove termination

Cláudio Amaral coa at dcc.fc.up.pt
Tue Nov 12 23:13:21 CET 2013


Hello, all!

I have a function like the following and why3 cannot prove its termination.
I can make it a 'let rec', but I would like to know more about this issue
and if it is possible to change something to enable the termination proof.

Cheers
Cláudio

module Example

  use import list.List
  type t =
    | A
    | C t t
  type r =
    | D
    | E

  function f (ts1: list t) (ts2: list t) (s: r) : r =
  match (ts1,ts2) with
  | (Nil, Nil) -> s
  | (Nil, Cons _ _) -> D
  | (Cons _ _, Nil) -> D
  | (Cons x xs, Cons y ys) ->
    match (x,y) with
    | (A, A) -> f xs ys s
    | (C xx xxs, C yy yys) ->
         f (Cons xx (Cons xxs xs)) (Cons yy (Cons yys ys)) s
    end
  end

end
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/why3-club/attachments/20131112/89d987de/attachment.html>


More information about the Why3-club mailing list