<abstract xmlns="http://www.w3.org/1999/xhtml"><p>Binary representation of integers <xref ref-type="bibr" rid="j_forma-2018-0020_ref_005_w2aab3b7b2b1b6b1ab1ab5Aa">[5]</xref>, <xref ref-type="bibr" rid="j_forma-2018-0020_ref_003_w2aab3b7b2b1b6b1ab1ab3Aa">[3]</xref> and arithmetic operations on them have already been introduced in Mizar Mathematical Library <xref ref-type="bibr" rid="j_forma-2018-0020_ref_008_w2aab3b7b2b1b6b1ab1ab8Aa">[8</xref>, <xref ref-type="bibr" rid="j_forma-2018-0020_ref_007_w2aab3b7b2b1b6b1ab1ab7Aa">7</xref>, <xref ref-type="bibr" rid="j_forma-2018-0020_ref_006_w2aab3b7b2b1b6b1ab1ab6Aa">6</xref>, <xref ref-type="bibr" rid="j_forma-2018-0020_ref_004_w2aab3b7b2b1b6b1ab1ab4Aa">4</xref>]. However, these articles formalize the notion of integers as mapped into a certain length tuple of boolean values.</p><p>In this article we formalize, by means of Mizar system <xref ref-type="bibr" rid="j_forma-2018-0020_ref_002_w2aab3b7b2b1b6b1ab1ab2Aa">[2]</xref>, <xref ref-type="bibr" rid="j_forma-2018-0020_ref_001_w2aab3b7b2b1b6b1ab1ab1Aa">[1]</xref>, the binary representation of natural numbers which maps ℕ into bitstreams.</p></abstract>

Binary representation of integers [5], [3] and arithmetic operations on them have already been introduced in Mizar Mathematical Library [8, 7, 6, 4]. However, these articles formalize the notion of integers as mapped into a certain length tuple of boolean values.In this article we formalize, by means of Mizar system [2], [1], the binary representation of natural numbers which maps ℕ into bitstreams.

Binary Representation of Natural Numbers

Formalized Mathematics

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 3.0 License.

{"article-title":"Binary Representation of Natural Numbers"}

Binary representation of integers [5], [3] and arithmetic operations on them have already been introduced in Mizar Mathematical Library [8, 7, 6, 4]. However,...

Binary Representation of Natural Numbers

Publié en ligne: 23 févr. 2019

Pages: 223 - 229

Accepté: 29 sept. 2018

DOI: https://doi.org/10.2478/forma-2018-0020

Mots clés
algorithms

© 2018 Hiroyuki Okazaki, published by Sciendo

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 3.0 License.

Binary Representation of Natural Numbers

Publié en ligne: 23 févr. 2019

Pages: 223 - 229

Accepté: 29 sept. 2018

DOI: https://doi.org/10.2478/forma-2018-0020

Mots clésalgorithms

© 2018 Hiroyuki Okazaki, published by Sciendo

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 3.0 License.

Mots clés
algorithms