--- layout: fc_discuss_archives title: Message 18 from Frama-C-discuss on July 2009 ---
On Christoph Weber's request I forward the following mail: ----------------------------- Hello, I am exploring the possibilitys of lemmas to assist proofs. As I allready mentioned before, I cannot proof the lemma (mean) you provided with any prover. It seems to me, that the division within prevents a solution. For example the following: /*@ lemma test1 : \forall int x; x/1 == x; */ /*@ lemma test2 : \forall int x; x/x == 1; */ The computations would result in unknowns. I would like to know if this is a general problem and if there is a way to circumvent it. Sincerely Christoph