On 10/04/13 05:46, Cris Perdue wrote: > I think this systematizes the approach that leads to using x != 0 ==> recip x > * > x = 1 as a specification for reciprocal, or Konrad's example with DIV and MOD. > Hopefully I am not missing something here.
Taking definedness to the level Freek is discussing would, I think, not let you prove that x DIV 0 = x DIV 0 at least if you were in the "meta-world" where you were paying attention to the D(..) predicate. It's problems like this that set off alarms with many. More examples: - should (x DIV 0) * 0 = 0 be a theorem? - should (x DIV 0) + 1 > x DIV 0 be a theorem? Michael
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ Precog is a next-generation analytics platform capable of advanced analytics on semi-structured data. The platform includes APIs for building apps and a phenomenal toolset for data science. Developers can use our toolset for easy data analysis & visualization. Get a free account! http://www2.precog.com/precogplatform/slashdotnewsletter
_______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
