[Why3-club] variant's and inlining

[Jean-Jacques Levy]

Dear Why3 folks,

here is a small termination problem which I cannot solve. Pls help!

Thanks -JJ-
———————————
Termination proved for g’, but not proved for g and g’’ !!

module Test
  use import int.Int
  use import int.EuclideanDivision
  
let p x = mod x 2 = 0

(* ———— *)
let rec f e =
requires {0 <= e}
variant {e}
  if e = 0 then 1 else g (e - 1)

with g e =
requires {0 <= e}
variant {e}
  if e = 0 then 1 else 
  if p e then f e else g (e - 1)

(* ———— *)
let rec g' e =
requires {0 <= e}
variant {e}
  if e = 0 then 1 else
  if p e then if e = 0 then 1 else g' (e - 1)
  else g' (e-1)

(* ———— *)
let rec g'' e =
requires {0 <= e}
variant {e}
  let f e =
  requires {0 <= e}
  if e = 0 then 1 else g'' (e - 1)  in
  
  if e = 0 then 1 else 
  if p e then f e else g'' (e-1)

end


_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club