pi
and rho
determine an atom of concept T
uniquely, you can write:<label>
is the name of the rule. It can be a single word or a string (enclosed by double brackets). It is followed by a colon (:
) to distinguish the label from the concept that follows.<Concept>
is the name of the Concept for atoms of which the rule specifies an identity<Concept>
. This is enforced by the type system.e
is both univalent and total, e<>e~
equals e;e~
, and the rule is equivalent to:e
is univalent but not total, you should use the IDENT
statement (or the rule that it implements), because that also works when an e
is not populated.