{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,10]],"date-time":"2026-01-10T02:06:19Z","timestamp":1768010779887,"version":"3.49.0"},"reference-count":16,"publisher":"Walter de Gruyter GmbH","issue":"2","license":[{"start":{"date-parts":[[2016,6,1]],"date-time":"2016-06-01T00:00:00Z","timestamp":1464739200000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by-sa\/3.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016,6,1]]},"abstract":"<jats:title>Summary<\/jats:title>\n               <jats:p>Formalization of a part of [11]. Unfortunately, not all is possible to be formalized. Namely, in the paper there is a mistake in the proof of Lemma 3. It states that there exists <jats:italic>x<\/jats:italic> \u2208 <jats:italic>M<\/jats:italic>\n                  <jats:sub>1<\/jats:sub> such that <jats:italic>M<\/jats:italic>\n                  <jats:sub>1<\/jats:sub>(<jats:italic>x<\/jats:italic>) &gt; <jats:italic>N<\/jats:italic>\n                  <jats:sub>1<\/jats:sub>(<jats:italic>x<\/jats:italic>) and (\u2200<jats:italic>y<\/jats:italic> \u2208 <jats:italic>N<\/jats:italic>\n                  <jats:sub>1<\/jats:sub>)<jats:italic>x<\/jats:italic> \u2280 <jats:italic>y<\/jats:italic>. It should be <jats:italic>M<\/jats:italic>\n                  <jats:sub>1<\/jats:sub>(<jats:italic>x<\/jats:italic>) \u2a7e <jats:italic>N<\/jats:italic>\n                  <jats:sub>1<\/jats:sub>(<jats:italic>x<\/jats:italic>). Nevertheless we do not know whether <jats:italic>x<\/jats:italic> \u2208 <jats:italic>N<\/jats:italic>\n                  <jats:sub>1<\/jats:sub> or not and cannot prove the contradiction. In the article we referred to [8], [9] and [10].<\/jats:p>","DOI":"10.1515\/forma-2016-0008","type":"journal-article","created":{"date-parts":[[2016,12,12]],"date-time":"2016-12-12T10:01:46Z","timestamp":1481536906000},"page":"95-106","source":"Crossref","is-referenced-by-count":1,"title":["On Multiset Ordering"],"prefix":"10.1515","volume":"24","author":[{"given":"Grzegorz","family":"Bancerek","sequence":"first","affiliation":[{"name":"Association of Mizar Users, Bia\u0142ystok, Poland"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"374","published-online":{"date-parts":[[2016,12,8]]},"reference":[{"key":"2021040619221012368_j_forma-2016-0008_ref_001_w2aab2b8c11b1b7b1ab1ab1Aa","unstructured":"[1] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41\u201346, 1990."},{"key":"2021040619221012368_j_forma-2016-0008_ref_002_w2aab2b8c11b1b7b1ab1ab2Aa","unstructured":"[2] Grzegorz Bancerek. Reduction relations. Formalized Mathematics, 5(4):469\u2013478, 1996."},{"key":"2021040619221012368_j_forma-2016-0008_ref_003_w2aab2b8c11b1b7b1ab1ab3Aa","unstructured":"[3] Grzegorz Bancerek. K\u00f6nig\u2019s lemma. Formalized Mathematics, 2(3):397\u2013402, 1991."},{"key":"2021040619221012368_j_forma-2016-0008_ref_004_w2aab2b8c11b1b7b1ab1ab4Aa","unstructured":"[4] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107\u2013114, 1990."},{"key":"2021040619221012368_j_forma-2016-0008_ref_005_w2aab2b8c11b1b7b1ab1ab5Aa","unstructured":"[5] Czes\u0142aw Byli\u0144ski. Finite sequences and tuples of elements of a non-empty sets. Formalized Mathematics, 1(3):529\u2013536, 1990."},{"key":"2021040619221012368_j_forma-2016-0008_ref_006_w2aab2b8c11b1b7b1ab1ab6Aa","unstructured":"[6] Czes\u0142aw Byli\u0144ski. Functions and their basic properties. Formalized Mathematics, 1(1): 55\u201365, 1990."},{"key":"2021040619221012368_j_forma-2016-0008_ref_007_w2aab2b8c11b1b7b1ab1ab7Aa","unstructured":"[7] Czes\u0142aw Byli\u0144ski. Some basic properties of sets. Formalized Mathematics, 1(1):47\u201353, 1990."},{"key":"2021040619221012368_j_forma-2016-0008_ref_008_w2aab2b8c11b1b7b1ab1ab8Aa","doi-asserted-by":"crossref","unstructured":"[8] Nachum Dershowitz. Orderings for term-rewriting systems. Theoretical Computer Science, 17(3):279\u2013301, 1982. doi:10.1016\/0304-3975(82)90026-3.","DOI":"10.1016\/0304-3975(82)90026-3"},{"key":"2021040619221012368_j_forma-2016-0008_ref_009_w2aab2b8c11b1b7b1ab1ab9Aa","doi-asserted-by":"crossref","unstructured":"[9] Nachum Dershowitz and Zohar Manna. Proving termination with multiset orderings. Communications of the ACM, 22(8):465\u2013476, 1979. doi:10.1145\/359138.359142.","DOI":"10.1145\/359138.359142"},{"key":"2021040619221012368_j_forma-2016-0008_ref_010_w2aab2b8c11b1b7b1ab1ac10Aa","doi-asserted-by":"crossref","unstructured":"[10] Gerard Huet and Derek C. Oppen. Equations and rewrite rules: A survey. Technical report, Stanford, CA, USA, 1980.","DOI":"10.1016\/B978-0-12-115350-2.50017-8"},{"key":"2021040619221012368_j_forma-2016-0008_ref_011_w2aab2b8c11b1b7b1ab1ac11Aa","doi-asserted-by":"crossref","unstructured":"[11] Jean-Pierre Jouannaud and Pierre Lescanne. On multiset ordering. Information Processing Letters, 15(2):57\u201363, 1982. doi:10.1016\/0020-0190(82)90107-7.","DOI":"10.1016\/0020-0190(82)90107-7"},{"key":"2021040619221012368_j_forma-2016-0008_ref_012_w2aab2b8c11b1b7b1ab1ac12Aa","unstructured":"[12] Robert Milewski. Natural numbers. Formalized Mathematics, 7(1):19\u201322, 1998."},{"key":"2021040619221012368_j_forma-2016-0008_ref_013_w2aab2b8c11b1b7b1ab1ac13Aa","doi-asserted-by":"crossref","unstructured":"[13] Eliza Niewiadomska and Adam Grabowski. Introduction to formal preference spaces. Formalized Mathematics, 21(3):223\u2013233, 2013. doi:10.2478\/forma-2013-0024.","DOI":"10.2478\/forma-2013-0024"},{"key":"2021040619221012368_j_forma-2016-0008_ref_014_w2aab2b8c11b1b7b1ab1ac14Aa","unstructured":"[14] Andrzej Trybulec. Binary operations applied to functions. Formalized Mathematics, 1 (2):329\u2013334, 1990."},{"key":"2021040619221012368_j_forma-2016-0008_ref_015_w2aab2b8c11b1b7b1ab1ac15Aa","unstructured":"[15] Wojciech A. Trybulec. Non-contiguous substrings and one-to-one finite sequences. Formalized Mathematics, 1(3):569\u2013573, 1990."},{"key":"2021040619221012368_j_forma-2016-0008_ref_016_w2aab2b8c11b1b7b1ab1ac16Aa","unstructured":"[16] Wojciech A. Trybulec and Grzegorz Bancerek. Kuratowski \u2013 Zorn lemma. Formalized Mathematics, 1(2):387\u2013393, 1990."}],"container-title":["Formalized Mathematics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/content.sciendo.com\/view\/journals\/forma\/24\/2\/article-p95.xml","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/www.sciendo.com\/article\/10.1515\/forma-2016-0008","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,7]],"date-time":"2021-04-07T00:26:16Z","timestamp":1617755176000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.sciendo.com\/article\/10.1515\/forma-2016-0008"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,6,1]]},"references-count":16,"journal-issue":{"issue":"2","published-online":{"date-parts":[[2016,12,8]]},"published-print":{"date-parts":[[2016,6,1]]}},"alternative-id":["10.1515\/forma-2016-0008"],"URL":"https:\/\/doi.org\/10.1515\/forma-2016-0008","relation":{},"ISSN":["1898-9934","1426-2630"],"issn-type":[{"value":"1898-9934","type":"electronic"},{"value":"1426-2630","type":"print"}],"subject":[],"published":{"date-parts":[[2016,6,1]]}}}