SUMO   View all facts   Glossary   Help
Entity > Abstract > Class > Relation > Function > BinaryFunction > CommutativeFunction
Next BinaryFunction: DayFn    Up: BinaryFunction    Previous BinaryFunction: AssociativeFunction   

CommutativeFunction comparison table
Subject documentation have axiom have identityElement
AdditionFnIf ?NUMBER1 and ?NUMBER2 are Numbers, then (AdditionFn ?NUMBER1 ?NUMBER2) is the arithmetical sum of these numbers
(<=>
    (equal (RemainderFn ?NUMBER1 ?NUMBER2) ?NUMBER)
    (equal (AdditionFn (MultiplicationFn (FloorFn (DivisionFn ?NUMBER1 ?NUMBER2)) ?NUMBER2) ?NUMBER) ?NUMBER1))
0
MaxFn(MaxFn ?NUMBER1 ?NUMBER2) is the largest of ?NUMBER1 and ?NUMBER2. In cases where ?NUMBER1 is equal to ?NUMBER2, MaxFn returns one of its arguments
(=>
    (equal (MaxFn ?NUMBER1 ?NUMBER2) ?NUMBER)
    (or
       (and
          (equal ?NUMBER ?NUMBER1)
          (greaterThan ?NUMBER1 ?NUMBER2))
       (and
          (equal ?NUMBER ?NUMBER2)
          (greaterThan ?NUMBER2 ?NUMBER1))
       (and
          (equal ?NUMBER ?NUMBER1)
          (equal ?NUMBER ?NUMBER2))))
 
MinFn(MinFn ?NUMBER1 ?NUMBER2) is the smallest of ?NUMBER1 and ?NUMBER2. In cases where ?NUMBER1 is equal to ?NUMBER2, MinFn returns one of its arguments
(=>
    (equal (MinFn ?NUMBER1 ?NUMBER2) ?NUMBER)
    (or
       (and
          (equal ?NUMBER ?NUMBER1)
          (lessThan ?NUMBER1 ?NUMBER2))
       (and
          (equal ?NUMBER ?NUMBER2)
          (lessThan ?NUMBER2 ?NUMBER1))
       (and
          (equal ?NUMBER ?NUMBER1)
          (equal ?NUMBER ?NUMBER2))))
 
MultiplicationFnIf ?NUMBER1 and ?NUMBER2 are Numbers, then (MultiplicationFn ?NUMBER1 ?NUMBER2) is the arithmetical product of these numbers
(equal
 	(MeasureFn ?NUMBER YearDuration)
 	(MeasureFn (MultiplicationFn ?NUMBER 365) DayDuration))
1

Next BinaryFunction: DayFn    Up: BinaryFunction    Previous BinaryFunction: AssociativeFunction