U+2A64 "⩤" Z Notation Domain Antirestriction Unicode Character

U+2A64 "⩤" Z Notation Domain Antirestriction is a mathematical symbol used in the Z notation formal specification language to represent the operation of domain antirestriction, also known as domain subtraction. This operator, when applied to a relation, removes from that relation all ordered pairs whose first element belongs to a specified set, effectively resulting in a new relation that contains only those pairs where the domain element is not in that set. It is visually similar to a less-than or equal sign with a vertical stroke on the left, and it serves as a precise tool for specifying constraints and data transformations in formal methods for software and systems engineering.