Re: [isabelle] nested multiset ordering?



I've only glanced at the paper briefly, so I'm probably wrong, but the
multi-set ordering in HOL4 (
https://github.com/HOL-Theorem-Prover/HOL/blob/master/src/bag/bagScript.sml#L2224)
looks similar. Then again, the comment there says it was "taken from [an]
Isabelle development", so is probably something you have seen before. In
particular, perhaps it doesn't cover the nested version you asked for.

On Sun, Sep 28, 2014 at 4:19 PM, Lawrence Paulson <lp15 at cam.ac.uk> wrote:

> I wonder whether anybody is aware of a formalisation (in any system) of
> the nested multiset ordering, as described in the classic paper "Proving
> Termination With Multiset Orderings”?
>
> http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.145.8728
>
> There is, I believe, a connection with the ordinal epsilon-0.
>
> Larry Paulson
>
>
>
>



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.