From the negative formulas of some equalities, or equal signs, EQ (equality) guides the single equality (the negative formula of equal signs).
Example 1 a1 : [a=b] by .... ;
a2 : [b=c] by .... ;
a3 : [a=c] by EQ (a1, a2) ;
Example 2 a1 : [v=v] by EQ ;
Example 3 a1 : [f(a)=G] by .... ;
a2 : [f(a)=K(b)] by ... ;
a3 : [G=t] by .... ;
a4 : [t=K(b)] by EQ (a1,a2,a3) ;
Example 4 a1 : not [a=Q] by .... ;
a2 : [Q=D] by .... ;
a3 : [a=C] by .... ;
a4 : not [C=D] by EQ (a1,a2,a3) ;
Formulas that are cited, or concluded, all take either this form [...=...], or not[...=...]. Computers classify equal variables (or formulas), and they record any unequal relationships between these groups. Also, computers judge to see if the last conclusion formula gets to be guided from those records (Yuji Takahashi, a research graduate thought of this simple judgment of algorithm that connects equal things). Arguments of EQ can either be 0 or optional numbers. In addition, the fact that (All x)(f(x)) and (All y) (f(y)) are judged identically are the same with other cases of rules.
Except for example 2, others can also be guided by the later introduced SUBST. For instance, saying that a1, a2, and a3 are the same, example 4 can be guided without using EQ as it is stated below.
Therefore, except for example 2, the EQ rule is also not necessary.