chapter ‹Generated by Lem from ‹semantics/namespace.lem›.› theory "NamespaceAuxiliary" imports Main "HOL-Library.Datatype_Records" "LEM.Lem_pervasives" "LEM.Lem_set_extra" "Namespace" begin ― ‹‹**************************************************›› ― ‹‹ ›› ― ‹‹ Termination Proofs ›› ― ‹‹ ›› ― ‹‹**************************************************›› termination nsMap by lexicographic_order end