This feature checks that an equation is not applied to itself. This means
that the focus of the rule application must not be one side of an equation
that is the instantiation of the first if-formula. If the rule application is
admissible, zero is returned.