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

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.