Function I-Upper-Bound

Binary-Relation, Function, Relation, Set
Domain: Integer-Range
Range: Integer
Arity: 2
Documentation: (I-UPPER-BOUND r) denotes the integer upper bound of range r.

Frame References to I-Upper-Bound:

In class Minute-Number@Simple-Time:

I-Upper-Bound: 59

In class Month-Number@Simple-Time:

I-Upper-Bound: 12

In class Hour-Number@Simple-Time:

I-Upper-Bound: 23

In class Day-Number@Simple-Time:

I-Upper-Bound: 31

In class Integer-Range:


Slot-Cardinality: 1

Implication Axioms mentioning I-Upper-Bound:

(=> (Integer-Range ?Class)
    (Forall (?I)
            (=> (Instance-Of ?I ?Class)
                (And (=< (I-Lower-Bound ?Class) ?I)
                     (=< ?I (I-Upper-Bound ?Class))))))

Equivalence Axioms mentioning I-Upper-Bound:

(<=> (Integer-Range ?Class)
     (And (Class ?Class)
          (Subclass-Of ?Class Integer)
          (Value-Cardinality ?Class I-Lower-Bound 1)
          (Value-Cardinality ?Class I-Upper-Bound 1)
          (Forall (?I)
                  (=> (Instance-Of ?I ?Class)
                      (And (=< (I-Lower-Bound ?Class) ?I)
                           (=< ?I (I-Upper-Bound ?Class)))))))