[Why3-club] cannot prove termination
coa at dcc.fc.up.pt
Tue Nov 12 23:13:21 CET 2013
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.
use import list.List
type t =
| C t t
type r =
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
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Why3-club