why3doc index index
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
Generated by why3doc 0.87.3