 SUMO   View all facts   Glossary   Help Entity > Abstract > Class > Relation > Function > BinaryFunction > AssociativeFunction > DivisionFn
Next AssociativeFunctionMaxFn    UpAssociativeFunction, RelationExtendedToQuantities    Previous AssociativeFunctionAdditionFn  DivisionFn subject fact
 DivisionFn documentation If ?NUMBER1 and ?NUMBER2 are Numbers, then (DivisionFn ?NUMBER1 ?NUMBER2) is the result of dividing ?NUMBER1 by ?NUMBER2. An exception occurs when ?NUMBER1 = 1, in which case (DivisionFn ?NUMBER1 ?NUMBER2) is the reciprocal of ?NUMBER2 has axiom `(<=> (equal (RemainderFn ?NUMBER1 ?NUMBER2) ?NUMBER) (equal (AdditionFn (MultiplicationFn (FloorFn (DivisionFn ?NUMBER1 ?NUMBER2)) ?NUMBER2) ?NUMBER) ?NUMBER1))` has axiom `(=> (instance ?NUMBER RationalNumber) (exists (?INT1 ?INT2) (and (instance ?INT1 Integer) (instance ?INT2 Integer) (equal ?NUMBER (DivisionFn ?INT1 ?INT2)))))` has axiom `(equal (TangentFn ?DEGREE) (DivisionFn (SineFn ?DEGREE) (CosineFn ?DEGREE)))` has axiom `(equal (MeasureFn ?NUMBER Cup) (MeasureFn (DivisionFn ?NUMBER 2) Pint))` has axiom `(equal (MeasureFn ?NUMBER Ounce) (MeasureFn (DivisionFn ?NUMBER 8) Cup)) ` has axiom `(equal (MeasureFn ?NUMBER Pint) (MeasureFn (DivisionFn ?NUMBER 2) Quart)) ` has axiom `(equal (MeasureFn ?NUMBER Quart) (MeasureFn (DivisionFn ?NUMBER 4) UnitedStatesGallon)) ` has axiom `(equal (MeasureFn ?NUMBER AngularDegree) (MeasureFn (MultiplicationFn ?NUMBER (DivisionFn Pi 180)) Radian))` has domain1 Quantity has domain2 Quantity has identityElement 1 has range Quantity is an instance of AssociativeFunction is an instance of RelationExtendedToQuantities BinaryFunction is first domain of distributes is first domain of identityElement is second domain of distributes Relation is first domain of domain is first domain of domainSubclass is first domain of holds is first domain of subrelation is first domain of valence is second domain of subrelation Class is third domain of domain is third domain of domainSubclass Abstract is disjoint from Physical  Next AssociativeFunctionMaxFn    UpAssociativeFunction, RelationExtendedToQuantities    Previous AssociativeFunctionAdditionFn