--- layout: fc_discuss_archives title: Message 37 from Frama-C-discuss on June 2014 ---
Thanks for the experiment with different provers. I have reformulated the assertions as lemmas as suggested and run the Coq prover on the example, but also this one is not able to prove the lemmas. As for the second axiom: I have learned that if one defines a function one has to ensure that the function value exists (for total functions) and that it is unique. It was not there in my first attempts but I have seen it somewhere so I thought I may help the prover. Frank