Formalization of Nested Multisets, Hereditary Multisets, and Syntactic Ordinals

Title:	Formalization of Nested Multisets, Hereditary Multisets, and Syntactic Ordinals
Authors:	Jasmin Christian Blanchette (j /dot/ c /dot/ blanchette /at/ vu /dot/ nl), Mathias Fleury (fleury /at/ mpi-inf /dot/ mpg /dot/ de) and Dmitriy Traytel
Submission date:	2016-11-12
Abstract:	This Isabelle/HOL formalization introduces a nested multiset datatype and defines Dershowitz and Manna's nested multiset order. The order is proved well founded and linear. By removing one constructor, we transform the nested multisets into hereditary multisets. These are isomorphic to the syntactic ordinals—the ordinals can be recursively expressed in Cantor normal form. Addition, subtraction, multiplication, and linear orders are provided on this type.
BibTeX:	@article{Nested_Multisets_Ordinals-AFP, author = {Jasmin Christian Blanchette and Mathias Fleury and Dmitriy Traytel}, title = {Formalization of Nested Multisets, Hereditary Multisets, and Syntactic Ordinals}, journal = {Archive of Formal Proofs}, month = nov, year = 2016, note = {\url{http://isa-afp.org/entries/Nested_Multisets_Ordinals.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Depends on:	List-Index, Ordinal
Used by:	Functional_Ordered_Resolution_Prover, Lambda_Free_KBOs, Ordered_Resolution_Prover
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.