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.