Dear Caballero:
Your information is very exciting for me. For me, you are the first man who derived the division by zero and division by zero calculus as the outputs of a computer. Meanwhile, I am writing some book on the division by zero calculus. I would like to include the very important information in my book. How will be the sentences? On February 16, 2019 Professor H. Okumura introduced the surprising news in Research Gate: José Manuel Rodríguez Caballero Added an answer In the proof assistant Isabelle/HOL we have x/0 = 0 for each number x. This is advantageous in order to simplify the proofs. You can download this proof assistant here: https://isabelle.in.tum.de/ J.M.R. Caballero kindly showed surprisingly several examples by the system that tan (π /2) = 0, log 0 = 0, exp (1/ x) (x = 0) = 1, and others. It seems that the division by zero calculus was implimented to the computer system already. If it is possible, I would like to refer to more details with precise information. Implimented?! With deep thanks, Sincerely yours, Saburou Saitoh 2019.3.3.11.02
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info