## 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.