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.