{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,25]],"date-time":"2026-02-25T20:40:36Z","timestamp":1772052036120,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540005681","type":"print"},{"value":"9783540364696","type":"electronic"}],"license":[{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-36469-2_13","type":"book-chapter","created":{"date-parts":[[2007,10,27]],"date-time":"2007-10-27T03:02:41Z","timestamp":1193454161000},"page":"162-174","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":15,"title":["On the Integrity of a Repository of Formalized Mathematics"],"prefix":"10.1007","author":[{"given":"Piotr","family":"Rudnicki","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrzej","family":"Trybulec","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2003,1,30]]},"reference":[{"key":"13_CR1","first-page":"91","volume":"1","author":"Grzegorz Bancerek","year":"1990","unstructured":"Grzegorz Bancerek.The ordinal numbers.Formalized Mathematics,1(1 ):91\u201396, 1990.","journal-title":"Formalized Mathematics"},{"issue":"3","key":"13_CR2","first-page":"589","volume":"1","author":"G. Bancerek","year":"1990","unstructured":"Grzegorz Bancerek. K\u00f6nig\u2019s theorem.Formalized Mathematics,1(3 ):589\u2013593, 1990.","journal-title":"Formalized Mathematics"},{"issue":"4","key":"13_CR3","first-page":"547","volume":"2","author":"Grzegorz Bancerek.Cartesian product of functions","year":"1991","unstructured":"Grzegorz Bancerek.Cartesian product of functions.Formalized Mathematics, 2(4 ):547\u2013552,1991.","journal-title":"Formalized Mathematics"},{"key":"13_CR4","first-page":"469","volume":"5","author":"Grzegorz Bancerek.Reduction relations","year":"1996","unstructured":"Grzegorz Bancerek.Reduction relations.Formalized Mathematics,5(4 ):469\u2013478, 1996.","journal-title":"Formalized Mathematics"},{"issue":"1","key":"13_CR5","first-page":"111","volume":"9","author":"Grzegorz Bancerek","year":"2001","unstructured":"Grzegorz Bancerek.Continuous lattices of maps between T 0 spaces.Formalized Mathematics,9(1 ):111\u2013117,2001.","journal-title":"Formalized Mathematics"},{"issue":"1","key":"13_CR6","first-page":"107","volume":"1","author":"G. Bancerek","year":"1990","unstructured":"Grzegorz Bancerek and Krzysztof Hryniewiecki.Segments of natural numbers and finite sequences.Formalized Mathematics,1(1 ):107\u2013114,1990.","journal-title":"Formalized Mathematics"},{"key":"13_CR7","unstructured":"Czes\u0142aw Byli\u0144ski.Some basic properties of sets.Formalized Mathematics,1(1 ):47\u201353,1990."},{"key":"13_CR8","unstructured":"Czes\u0142aw Byli\u0144ski.Functions from a set to a set.Formalized Mathematics ,1(1 ):153\u2013164,1990."},{"key":"13_CR9","unstructured":"Czes\u0142aw Byli\u0144ski.Finite sequences and tuples of elements of a non-empty sets. Formalized Mathematics,1(3 ):529\u2013536,1990."},{"issue":"3","key":"13_CR10","first-page":"427","volume":"6","author":"B. Czes\u0142aw","year":"1997","unstructured":"Czes\u0142aw Byli\u0144ski and Piotr Rudnicki.Bounding boxes for compact sets in \u23092. Formalized Mathematics ,6(3 ):427\u2013440,1997.","journal-title":"Formalized Mathematics"},{"key":"13_CR11","unstructured":"Agata Darmochwa\u0142.The Euclidean space.Formalized Mathematics,2(4 ):599\u2013603, 1991."},{"issue":"3","key":"13_CR12","first-page":"607","volume":"1","author":"S. Kanas","year":"1990","unstructured":"Stanis\u0142awa Kanas, Adam Lecko, and Mariusz Startek. Metric spaces. Formalized Mathematics,1(3 ):607\u2013610,1990.","journal-title":"Formalized Mathematics"},{"issue":"1","key":"13_CR13","first-page":"145","volume":"6","author":"Artur Korni\u0142owicz","year":"1997","unstructured":"Artur Korni\u0142owicz.Cartesian products of relations and relational structures.For-malized Mathematics,6(1 ):145\u2013152,1997.","journal-title":"For-malized Mathematics"},{"issue":"3","key":"13_CR14","first-page":"477","volume":"1","author":"Kotowicz Jaros\u0142aw","year":"1990","unstructured":"Jaros\u0142aw Kotowicz.Convergent real sequences.Upper and lower bound of sets of real numbers.Formalized Mathematics,1(3 ):477\u2013481,1990.","journal-title":"Formalized Mathematics"},{"key":"13_CR15","unstructured":"Mizar Manuals .\nhttp:\/\/mizar.org\/project\/bibliography.html\n\n."},{"issue":"1","key":"13_CR16","first-page":"115","volume":"7","author":"Y. Nakamura","year":"1998","unstructured":"Yatsuka Nakamura and Adam Grabowski.Bounding boxes for special sequences in \u23092.Formalized Mathematics,7(1 ):115\u2013121,1998.","journal-title":"Formalized Mathematics"},{"issue":"3","key":"13_CR17","first-page":"297","volume":"5","author":"Y. Nakamura","year":"1996","unstructured":"Yatsuka Nakamura and Piotr Rudnicki.Vertex sequences induced by chains.For-malized Mathematics,5(3 ):297\u2013304,1996.","journal-title":"For-malized Mathematics"},{"issue":"1","key":"13_CR18","first-page":"9","volume":"2","author":"A. Naumowicz","year":"2002","unstructured":"Adam Naumowicz and Czes\u0142aw Byli\u0144ski.Basic Elements of Computer Algebra in Mizar.Mechanized Mathematics and Its Applications,2 (1):9\u201316,2002.","journal-title":"Mechanized Mathematics and Its Applications"},{"issue":"1","key":"13_CR19","first-page":"223","volume":"1","author":"B. Padlewska","year":"1990","unstructured":"Beata Padlewska and Agata Darmochwa\u0142.Topological spaces and continuous func-tions.Formalized Mathematics,1(1 ):223\u2013230,1990.","journal-title":"Formalized Mathematics"},{"key":"13_CR20","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1006\/jsco.2001.0456","volume":"32","author":"P. Rudnicki","year":"2001","unstructured":"P. Rudnicki, Ch. Schwarzweller and A. Trybulec.Commutative Algebra in the Mizar System.Journal of Symbolic Computation,32 :143\u2013169,2001.","journal-title":"Journal of Symbolic Computation"},{"issue":"3-4","key":"13_CR21","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1023\/A:1006218513245","volume":"23","author":"P. Rudnicki","year":"1999","unstructured":"Piotr Rudnicki and Andrzej Trybulec.On equivalents of well-foundedness.Journal of Automated Reasoning ,23 (3-4):197\u2013234,1999.","journal-title":"Journal of Automated Reasoning"},{"key":"13_CR22","unstructured":"Piotr Rudnicki and Andrzej Trybulec.Mathematical Knowledge Management in Mizar.1st Int.Workshop on MKM ,Sept.24\u201326,2001, \nhttp:\/\/www.risc.uni-linz.ac.at\/institute\/conferences\/MKM2001\n\n."},{"issue":"1","key":"13_CR23","first-page":"93","volume":"5","author":"A. Sakowicz","year":"1996","unstructured":"Agnieszka Sakowicz, Jaros\u0142aw Gryko, and Adam Grabowski. Sequences in\u2309n\ntFormalized Mathematics,5(1 ):93\u201396,1996.","journal-title":"Formalized Mathematics"},{"issue":"1","key":"13_CR24","first-page":"9","volume":"1","author":"Trybulec Andrzej","year":"1990","unstructured":"Andrzej Trybulec.Tarski Grothendieck set theory.Formalized Mathematics , 1(1 ):9\u201311,1990.","journal-title":"Formalized Mathematics"},{"issue":"3","key":"13_CR25","first-page":"569","volume":"1","author":"W. A. Trybulec","year":"1990","unstructured":"Wojciech A. Trybulec.Non-contiguous substrings and one-to-one.nite sequences. Formalized Mathematics,1(3 ):569\u2013573,1990.","journal-title":"Formalized Mathematics"},{"issue":"4","key":"13_CR26","first-page":"825","volume":"9","author":"T. Tsunetou","year":"2001","unstructured":"Tetsuya Tsunetou, Grzegorz Bancerek, and Yatsuka Nakamura. Zero-Based Finite Sequences. Formalized Mathematics,9(4):825\u2013829,2001.","journal-title":"Formalized Mathematics"},{"key":"13_CR27","unstructured":"Freek Wiedijk.Mizar:An Impression.\nhttp:\/\/www.cs.kun.nl\/~freek\/notes\n\n."}],"container-title":["Lecture Notes in Computer Science","Mathematical Knowledge Management"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36469-2_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,10]],"date-time":"2020-01-10T06:19:02Z","timestamp":1578637142000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36469-2_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540005681","9783540364696"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/3-540-36469-2_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2003]]},"assertion":[{"value":"30 January 2003","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}