Models

For a subsorted signature Sigma the  subsorted models are ordinary many-sorted models for Sigma^# that satisfy the following properties (which can be formalized as a set of conditional axioms):

• Embedding functions are total and 1-1; projection functions are partial, and 1-1 when defined.
• The embedding of a sort into itself is the identity function.
• All compositions of embedding functions between the same two sorts are equal functions.
• Embedding followed by projection is identity; projection followed by embedding is included in identity.
• Membership in a subsort holds just when the projection to the subsort is defined.
• Embedding is compatible with those functions and predicates that are in the overloading relations.