On Multiset Ordering

Autor: Grzegorz Bancerek
Rok vydání: 2016
Předmět:
Zdroj: Formalized Mathematics, Vol 24, Iss 2, Pp 95-106 (2016)
ISSN: 1898-9934
1426-2630
DOI: 10.1515/forma-2016-0008
Popis: Summary 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 ∈ M 1 such that M 1(x) > N 1(x) and (∀y ∈ N 1)x ⊀ y. It should be M 1(x) ⩾ N 1(x). Nevertheless we do not know whether x ∈ N 1 or not and cannot prove the contradiction. In the article we referred to [8], [9] and [10].
Databáze: OpenAIRE