Function VALUE-CARDINALITY

The VALUE-CARDINALITY of a binary-relation with respect to a given domain instance is the number of range-elements to which the relation maps the domain-element. For a function (single-valued relation), the VALUE-CARDINALITY is 1 on all domain instances for which the function is defined. It is 0 for those instances outside the exact domain of the function.

VALUE-CARDINALITY may be used within the definition of a class to specify a slot cardinality if its first argument is the class's instance variable.

Arity: 3
Axioms:
(Nth-Domain Value-Cardinality 3 Nonnegative-Integer)

(Nth-Domain Value-Cardinality 2 Binary-Relation)

(=> (Value-Cardinality ?Instance ?Binary-Relation ?N)
    (= ?N
       (Cardinality (Setofall ?Y
                              (Holds ?Binary-Relation ?Instance ?Y)))))

Notes: