TreeView Knowledge Base Browser

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

Show simplified definition (without tree view)
Show simplified definition (with tree view)

KB Term:			Term intersection

English Word: