6.3 Predicate Definition

We will first explain the predicate definition. For instance, considering
k and l as natural numbers, let us assume that we want to define k as a
factor of l. This is a predicate. Let us assume that we also want to define
such that k is a factor of l. This has a form similar to a binomial calculation
unit; however, it has two variables of k and l. The following shows how
to write the definition for this case.

definition

let k,l be Nat;

pred k is_factor_of l

means

:FACTOR:

ex t being Nat st l=k·t

The Nat in let k,l be Nat indicates that the mode of k and l is a natural
number. :FACTOR: is a label and this is used for citation later. The labels
in the definition are put between the colons. When the abstract file is
made by pulling it out of here, it will be changed to def with numbers.
Labels of normal theorems will be changed to simple numbers. Also, ·
in k·t symbolizes multiplication.

As a result, a predicate of k is_factor_of l means ex t being
Nat st l=k·t.