 SUMO   View all facts   Glossary   Help Entity > Abstract > Class > Relation > BinaryRelation > UnaryFunction > FloorFn
Next UnaryFunctionFutureFn    UpUnaryFunction    Previous UnaryFunctionExtensionFn  FloorFn subject fact
 FloorFn documentation (FloorFn ?NUMBER) returns the largest Integer less than or equal to the RealNumber ?NUMBER has axiom `(<=> (equal (RemainderFn ?NUMBER1 ?NUMBER2) ?NUMBER) (equal (AdditionFn (MultiplicationFn (FloorFn (DivisionFn ?NUMBER1 ?NUMBER2)) ?NUMBER2) ?NUMBER) ?NUMBER1))` has axiom `(=> (equal (FloorFn ?NUMBER) ?INT) (not (exists (?OTHERINT) (and (instance ?OTHERINT Integer) (lessThanOrEqualTo ?OTHERINT ?NUMBER) (greaterThan ?OTHERINT ?INT)))))` has axiom `(=> (equal (RoundFn ?NUMBER1) ?NUMBER2) (or (=> (lessThan (SubtractionFn ?NUMBER1 (FloorFn ?NUMBER1)) .5) (equal ?NUMBER2 (FloorFn ?NUMBER1))) (=> (greaterThanOrEqualTo (SubtractionFn ?NUMBER1 (FloorFn ?NUMBER1)) .5) (equal ?NUMBER2 (CeilingFn ?NUMBER1)))))` has domain1 RealNumber has range Integer is an instance of UnaryFunction BinaryRelation is first domain of DomainFn is first domain of equivalenceRelationOn is first domain of inverse is first domain of irreflexiveOn is first domain of partialOrderingOn is first domain of RangeFn is first domain of reflexiveOn is first domain of totalOrderingOn is first domain of trichotomizingOn is second domain of inverse Function is first domain of AssignmentFn is first domain of closedOn is first domain of range is first domain of rangeSubclass Class is third domain of domain is third domain of domainSubclass Abstract is disjoint from Physical  Next UnaryFunctionFutureFn    UpUnaryFunction    Previous UnaryFunctionExtensionFn