<abstract xmlns="http://www.w3.org/1999/xhtml">Formalization of a part of <xref ref-type="bibr" rid="j_forma-2016-0008_ref_011_w2aab2b8c11b1b7b1ab1ac11Aa">[11]</xref>. 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 <italic>x</italic> ∈ <italic>M</italic>1 such that <italic>M</italic>1(<italic>x</italic>) > <italic>N</italic>1(<italic>x</italic>) and (∀<italic>y</italic> ∈ <italic>N</italic>1)<italic>x</italic> ⊀ <italic>y</italic>. It should be <italic>M</italic>1(<italic>x</italic>) ⩾ <italic>N</italic>1(<italic>x</italic>). Nevertheless we do not know whether <italic>x</italic> ∈ <italic>N</italic>1 or not and cannot prove the contradiction. In the article we referred to <xref ref-type="bibr" rid="j_forma-2016-0008_ref_008_w2aab2b8c11b1b7b1ab1ab8Aa">[8]</xref>, <xref ref-type="bibr" rid="j_forma-2016-0008_ref_009_w2aab2b8c11b1b7b1ab1ab9Aa">[9]</xref> and <xref ref-type="bibr" rid="j_forma-2016-0008_ref_010_w2aab2b8c11b1b7b1ab1ac10Aa">[10]</xref>.</abstract>

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 x ∈ M1 such that M1(x) > N1(x) and (∀y ∈ N1)x ⊀ y. It should be M1(x) ⩾ N1(x). Nevertheless we do not know whether x ∈ N1 or not and cannot prove the contradiction. In the article we referred to [8], [9] and [10].

On Multiset Ordering

Formalized Mathematics

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

{"article-title":"On Multiset Ordering"}

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...

On Multiset Ordering

Online veröffentlicht: 08. Dez. 2016

Seitenbereich: 95 - 106

Eingereicht: 31. Dez. 2015

DOI: https://doi.org/10.1515/forma-2016-0008

Schlüsselwörter
ordering, Dershowitz-Manna ordering

© 2016 Grzegorz Bancerek, published by De Gruyter Open

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

On Multiset Ordering

Online veröffentlicht: 08. Dez. 2016

Seitenbereich: 95 - 106

Eingereicht: 31. Dez. 2015

DOI: https://doi.org/10.1515/forma-2016-0008

Schlüsselwörterordering, Dershowitz-Manna ordering

© 2016 Grzegorz Bancerek, published by De Gruyter Open

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

Schlüsselwörter
ordering, Dershowitz-Manna ordering