Browsing Interface : Welcome guest : log in
|
Browsing Interface : Welcome guest : log in |
[
Home |
Graph |
LogLearn |
Editor |
]
KB:
Language:
Formal Language:
|
| FloorFn |
| appearance as argument number 1 |
|
| (instance FloorFn UnaryFunction) | Merge.kif 4938-4938 | Floor is an instance of unary function |
| (instance FloorFn TotalValuedRelation) | Merge.kif 4939-4939 | Floor is an instance of total valued relation |
| (domain FloorFn 1 RealNumber) | Merge.kif 4940-4940 | The number 1 argument of floor is an instance of real number |
| (range FloorFn Integer) | Merge.kif 4941-4941 | The range of floor is an instance of integer |
| (documentation FloorFn EnglishLanguage "(FloorFn ?NUMBER) returns the largest Integer less than or equal to the RealNumber ?NUMBER.") | Merge.kif 4943-4944 | The range of floor is an instance of integer |
| appearance as argument number 2 |
|
|
| (termFormat EnglishLanguage FloorFn "floor") | domainEnglishFormat.kif 24256-24256 | |
| (termFormat ChineseTraditionalLanguage FloorFn "地板") | domainEnglishFormat.kif 24257-24257 | |
| (termFormat ChineseLanguage FloorFn "地板") | domainEnglishFormat.kif 24258-24258 | |
| (format EnglishLanguage FloorFn "the largest integer less than or equal to %1") | english_format.kif 700-700 |
| antecedent |
|
|
| (=> (and (not (equal ?NUMBER2 0)) (equal (AdditionFn (MultiplicationFn (FloorFn (DivisionFn ?NUMBER1 ?NUMBER2)) ?NUMBER2) ?NUMBER) ?NUMBER1)) (equal (RemainderFn ?NUMBER1 ?NUMBER2) ?NUMBER)) |
Merge.kif 5229-5240 | If equal X and 0 and equal (the largest integer less than or equal to Y and X and X and Z) and Y, then equal Y mod X and Z |
| consequent |
|
|
| (=> (and (equal (RemainderFn ?NUMBER1 ?NUMBER2) ?NUMBER) (not (equal ?NUMBER2 0))) (equal (AdditionFn (MultiplicationFn (FloorFn (DivisionFn ?NUMBER1 ?NUMBER2)) ?NUMBER2) ?NUMBER) ?NUMBER1)) |
Merge.kif 5216-5227 | If equal X mod Y and Z and equal Y and 0, then equal (the largest integer less than or equal to X and Y and Y and Z) and X |
|