3. 14 FUNF (Replacement by the Definition Formula)


This rule is used for citing the definition formula. Examples are listed below.

Example 1  a1 : Put f(x)=g(x) and u(x) ;
a2 : g(h(a)) and u(h(a)) by .... ;
........
a3 : f(h(a)) by FUNF (a1,a2) ;
Example 2  a1 : Put f(x)=g(x) and u(x) ;
a2 : f([a=b]) by .... ;
........
a3 : g([a=b]) and u([a=b]) by FUNF (a1,a2) ;

In such ways, if a formula can be formed by substituting a certain value to either side of the definition formula, another formula can be constructed by inserting that value into the other side of the formula in the same way. In fact, the definition formulas without put are also acceptable for citation. It is because the system memorizes each formula by a table of formulas; however, formula a1 above memorizes such a formula as indicated below.

(All x) ([f(x)=g(x) and u(x)])

Let us list some examples next.

Example 3  a1 : (All x) ([f(x)=g(x)]) by ... ;
a2 : f(a) by ..... ;
........
a3 : g(a) by FUNF (a1,a2) ;

Further, the rule FUNF also is not necessary. For example 3, if we write the following of a3 as below, it becomes a substitution.

a3 : [f(a)=g(a)] by ALS (a1) ;
a4 : g(a) by SUBST (a2,a3) ;

FUNF is an abbreviation of Function-Form.