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].
@article{bwmeta1.element.doi-10_1515_forma-2016-0008,
author = {Grzegorz Bancerek},
title = {On Multiset Ordering},
journal = {Formalized Mathematics},
volume = {24},
year = {2016},
pages = {95-106},
zbl = {1352.06004},
language = {en},
url = {http://dml.mathdoc.fr/item/bwmeta1.element.doi-10_1515_forma-2016-0008}
}
Grzegorz Bancerek. On Multiset Ordering. Formalized Mathematics, Tome 24 (2016) pp. 95-106. http://gdmltest.u-ga.fr/item/bwmeta1.element.doi-10_1515_forma-2016-0008/