Re: [isabelle] Integer Division


On Fri, 2008-12-12 at 09:23 +0100, Jens Doll wrote: 
> I will have to teach my algorithm to solve the inequality
> " EX (i::int). r - 2*i <= 1" ,

this (again) falls within the scope of Presburger arithmetic, and is
handled automatically by Isabelle:

lemma "EX (i::int). r - 2*i <= 1"
  by presburger


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.