[isabelle] nested multiset ordering?

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