## 3. 11 EQ (Guiding Out the Equalities)

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.

a4 : not [a=D] by SUBST (a1 ,a2) ;
a5 : not [C=D] by SUBST (a4 ,a3) ;
Therefore, except for example 2, the EQ rule is also not necessary.