## 3. 13 EQPT (Replacement of Identity)

This means that if two formulas accord with each other, two new formulas
made the same way by those two are also equal to each other. Let us look
at examples.

Example 1 a1 : [a=b] by .... ;

......
a2 : [f(a)=f(b)] by EQPT (a1) ;
Example 2 a1 : [f(a)=g(b) and D] by .... ;

......
a2 : [t(f(a)) or g(b) and D=t(g(b) and D) or f(a)] by EQPT (a1) ;
That is, for example 1, because a is equal to b, f(a) and f(b) which
are made in the similar way are also equal to each other.

Computers make sure if the conclusion formula is the formula of equal
signs. Using only the left side of the formula to make a formula such as
[left side of the formula = left side of the formula] in order to confirm
if the desired conclusion formula can be acquired by substituting the cited
formula into it. Namely, example 1 is the same with writing such as below.

a1 : [a=b] by .... ;
a1.1 : [f(a)=f(a)] by EQ ;
a2 : [f(a)=f(b)] by SUBST (a1.1,a1) ;
Therefore, EQPT also is not a necessary rule; however, if we have it,
we will be able to save one minute and the demonstration will be simpler.

Further, EQPT is an abbreviation of Equality-Put.