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 (
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”?
> 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