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

### License

BSD License

### Topics

- Logic/Rewriting

### Session Nested_Multisets_Ordinals

- Multiset_More
- Signed_Multiset
- Nested_Multiset
- Hereditary_Multiset
- Signed_Hereditary_Multiset
- Syntactic_Ordinal
- Signed_Syntactic_Ordinal
- Syntactic_Ordinal_Bridge
- McCarthy_91
- Hydra_Battle
- Goodstein_Sequence
- Unary_PCF

### Depends on

- List Index
- Countable Ordinals

### Used by

- Combinatorial Design Theory
- Formalization of Timely Dataflow’s Progress Tracking Protocol
- Practical Algebraic Calculus Checker
- A Verified Functional Implementation of Bachmair and Ganzinger’s Ordered Resolution Prover
- Formalization of Bachmair and Ganzinger’s Ordered Resolution Prover
- Formalization of Knuth–Bendix Orders for Lambda-Free Higher-Order Terms
- Formalization of Recursive Path Orders for Lambda-Free Higher-Order Terms

### Auto-related entries

- Clique is not solvable by monotone circuits of polynomial size
- Extensions to the Comprehensive Framework for Saturation Theorem Proving
- Formalization of Concurrent Revisions

## Cite

×

Nested_Multisets_Ordinals-AFP

    @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   = {November},
      year    = {2016},
      note    = {\url{https://isa-afp.org/entries/Nested_Multisets_Ordinals.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1