*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 | |