## 2.9 Simple Put Sentences

As introduced before, this is a simple replacement of names or functions.
Further, a logical proposition is included in functions. A simple put sentence
is written in one sentence with a line saying<simple.put. line>.
That general form is such:

<label>:put <general.function.form>=<general.formula>;
This<general.function.form>can be<name>.

For example,
AB : Put f(x)=Nat(x) and GT(1, x);
C4 : Put 2= P1(1);
a3 : Put Commutative(S) (p)=(All x)
(All y)(S(x) and S(y) imp[p (x, y)=p(y,x)]);

D4 : Put add3(x, y, z)=Add (Add(x,y), z);
When there is a simple put sentence, the system does mainly two things.
One of them is to register the names that are newly defined to a name table.
From the example above, name f from formula AB, name 2 from formula C4,
name Commutative from formula a3, and name add3 from formula D4 are registered
to a name table. Furthermore, new names go to the left side of the equalities
which come behind the Put. New names must not appear to the right side
of the equalities. Namely, new names that emerge at the right side of the
equalities must already be registered to a name table at that point.

The second job that the system performs is to register new names to
a formula table (udirect), and make it so that they can be cited by labels
later. From the example above, let us indicate what kinds of formulas get
registered to a formula table. For each label,

AB : (All x)([f(x)=Nat(x)and GT(1,x)])
C4 : [2=P1(1)]
a3 : (All S)(All p)([Commutative (S)(p)=(All x)(All y)(S(x)and S(y)imp[p(x,y)=p(y,x)])])
D4 : (All x)(All y)(All z)([add3(x,y,z)=Add(Add(x,y),z)])
Therefore, the arguments on the left side of the function form all become
bound variables and the whole formula becomes quantitized. Such formulas
as C4 which does not have an argument will not have all the symbols attached
to it; the equalities formulas will only be enclosed by Japanese quotation
marks. Therefore, when citing put sentences, one needs to be careful because
formulas that were changed as above will be used, instead of the original
formulas that start with Put.