On Multiset Ordering

Grzegorz Bancerek. "On Multiset Ordering." Formalized Mathematics 24.2 (2016): 95-106. <http://eudml.org/doc/287159>.

@article{GrzegorzBancerek2016,
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].},
author = {Grzegorz Bancerek},
journal = {Formalized Mathematics},
keywords = {ordering; Dershowitz-Manna ordering},
language = {eng},
number = {2},
pages = {95-106},
title = {On Multiset Ordering},
url = {http://eudml.org/doc/287159},
volume = {24},
year = {2016},
}

TY - JOUR
AU - Grzegorz Bancerek
TI - On Multiset Ordering
JO - Formalized Mathematics
PY - 2016
VL - 24
IS - 2
SP - 95
EP - 106
AB - 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].
LA - eng
KW - ordering; Dershowitz-Manna ordering
UR - http://eudml.org/doc/287159
ER -