Function Value-Cardinality

Arity: 3
Documentation:
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.

Notes:

Instance-Of: Function, Relation, Set

Axioms for Value-Cardinality:

(Nth-Domain Value-Cardinality 3 Nonnegative-Integer)

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


Implication Axioms mentioning Value-Cardinality:

(=> (= (Slot-Cardinality ?Domain-Class ?Binary-Relation) ?N)
    (=> (Instance-Of ?Instance ?Domain-Class)
        (= (Value-Cardinality ?Instance ?Binary-Relation) ?N)))

(=> (Minimum-Value-Cardinality ?Instance ?Binary-Relation ?N)
    (>= (Value-Cardinality ?Instance ?Binary-Relation) ?N))

(=> (Maximum-Value-Cardinality ?Instance ?Binary-Relation ?N)
    (=< (Value-Cardinality ?Instance ?Binary-Relation) ?N))

(=> (Has-At-Least@Ol-User%Slot-Constraint-Sugar ?Instance
                  ?Binary-Relation
                  ?N)
    (>= (Value-Cardinality ?Instance ?Binary-Relation) ?N))

(=> (Has-At-Most@Ol-User%Slot-Constraint-Sugar ?Instance
                 ?Binary-Relation
                 ?N)
    (=< (Value-Cardinality ?Instance ?Binary-Relation) ?N))


Equivalence Axioms mentioning Value-Cardinality:

(<=> (Minimum-Value-Cardinality ?Instance ?Binary-Relation ?N)
     (And (Binary-Relation ?Binary-Relation)
          (Nonnegative-Integer ?N)
          (>= (Value-Cardinality ?Instance ?Binary-Relation) ?N)))

(<=> (Maximum-Value-Cardinality ?Instance ?Binary-Relation ?N)
     (And (Binary-Relation ?Binary-Relation)
          (Nonnegative-Integer ?N)
          (=< (Value-Cardinality ?Instance ?Binary-Relation) ?N)))

(<=> (Slot-Cardinality ?Domain-Class ?Binary-Relation)
     (=> (Instance-Of ?Instance ?Domain-Class)
         (= (Value-Cardinality ?Instance ?Binary-Relation) ?N)))

(<=> (Minimum-Slot-Cardinality ?Domain-Class ?Relation ?N)
     (=> (Instance-Of ?Instance ?Domain-Class)
         (>= (Value-Cardinality ?Instance ?Relation) ?N)))

(<=> (Maximum-Slot-Cardinality ?Domain-Class ?Relation ?N)
     (=> (Instance-Of ?Instance ?Domain-Class)
         (=< (Value-Cardinality ?Instance ?Relation) ?N)))


Axioms mentioning Value-Cardinality:

(= (Value-Cardinality ?Instance ?Binary-Relation) 1)

(>= (Value-Cardinality ?Instance ?Binary-Relation) 1)