(=> (and (equal (MeasureFn ?NUMBER ?UNIT) ?QUANT) (subclass ?UNIT ?QUANTTYPE) (not (equal ?QUANTTYPE UnitOfMeasure))) (subclass ?QUANT ?QUANTTYPE))
(=> (and (instance ?DECREASE Decreasing) (patient ?DECREASE ?OBJ)) (exists (?UNIT ?QUANT1 ?QUANT2) (and (holdsDuring (ImmediatePastFn (WhenFn ?DECREASE)) (equal (MeasureFn ?OBJ ?UNIT) ?QUANT1)) (holdsDuring (ImmediateFutureFn (WhenFn ?DECREASE)) (equal (MeasureFn ?OBJ ?UNIT) ?QUANT2)) (lessThan ?QUANT2 ?QUANT1))))
(=> (and (instance ?FUNCTION RelationExtendedToQuantities) (instance ?FUNCTION BinaryFunction) (instance ?NUMBER1 RealNumber) (instance ?NUMBER2 RealNumber) (equal (AssignmentFn ?FUNCTION ?NUMBER1 ?NUMBER2) ?VALUE)) (forall (?UNIT) (=> (instance ?UNIT UnitOfMeasure) (equal (AssignmentFn ?FUNCTION (MeasureFn ?NUMBER1 ?UNIT) (MeasureFn ?NUMBER2 ?UNIT)) (MeasureFn ?VALUE ?UNIT)))))
(=> (and (instance ?INCREASE Increasing) (patient ?INCREASE ?OBJ)) (exists (?UNIT ?QUANT1 ?QUANT2) (and (holdsDuring (ImmediatePastFn (WhenFn ?INCREASE)) (equal (MeasureFn ?OBJ ?UNIT) ?QUANT1)) (holdsDuring (ImmediateFutureFn (WhenFn ?INCREASE)) (equal (MeasureFn ?OBJ ?UNIT) ?QUANT2)) (greaterThan ?QUANT2 ?QUANT1))))
(=> (and (instance ?MEAS Measuring) (agent ?MEAS ?AGENT) (patient ?MEAS ?OBJ)) (exists (?QUANT ?UNIT) (holdsDuring (ImmediateFutureFn (WhenFn ?MEAS)) (knows ?AGENT (measure ?OBJ (MeasureFn ?QUANT ?UNIT))))))
(=> (and (instance ?REL RelationExtendedToQuantities) (instance ?REL BinaryRelation) (instance ?NUMBER1 RealNumber) (instance ?NUMBER2 RealNumber) (holds ?REL ?NUMBER1 ?NUMBER2)) (forall (?UNIT) (=> (instance ?UNIT UnitOfMeasure) (holds ?REL (MeasureFn ?NUMBER1 ?UNIT) (MeasureFn ?NUMBER2 ?UNIT)))))
(=> (larger ?OBJ1 ?OBJ2) (forall (?QUANT1 ?QUANT2) (=> (and (measure ?OBJ1 (MeasureFn ?QUANT1 LengthMeasure)) (measure ?OBJ2 (MeasureFn ?QUANT2 LengthMeasure))) (greaterThan ?QUANT1 ?QUANT2))))
(equal (MagnitudeFn (MeasureFn ?NUMBER ?UNIT)) ?NUMBER)
(equal (MeasureFn ?NUMBER GigaHertz) (MeasureFn (MultiplicationFn ?NUMBER 1.0E9) Hertz))
(equal (MeasureFn ?NUMBER Amu) (MeasureFn (MultiplicationFn ?NUMBER 1.6605402E-27) Kilogram))
(equal (MeasureFn ?NUMBER Angstrom) (MeasureFn (MultiplicationFn ?NUMBER 1.0E-10) Meter))
(equal (MeasureFn ?NUMBER BritishThermalUnit) (MeasureFn (MultiplicationFn ?NUMBER 1055.05585262) Joule))
(equal (MeasureFn ?NUMBER Byte) (MeasureFn (MultiplicationFn ?NUMBER 8) Bit))
(equal (MeasureFn ?NUMBER Calorie) (MeasureFn (MultiplicationFn ?NUMBER 4.1868) Joule))
(equal (MeasureFn ?NUMBER Celsius) (MeasureFn (SubtractionFn ?NUMBER 273.15) Kelvin))
(equal (MeasureFn ?NUMBER Centimeter) (MeasureFn (MultiplicationFn ?NUMBER 0.01) Meter))
(equal (MeasureFn ?NUMBER CentUnitedStates) (MeasureFn (MultiplicationFn ?NUMBER .01) DollarUnitedStates))
(equal (MeasureFn ?NUMBER Cup) (MeasureFn (DivisionFn ?NUMBER 2) Pint))
(equal (MeasureFn ?NUMBER ElectronVolt) (MeasureFn (MultiplicationFn ?NUMBER 1.60217733E-19) Joule))
(equal (MeasureFn ?NUMBER Foot) (MeasureFn (MultiplicationFn ?NUMBER 0.3048) Meter))
(equal (MeasureFn ?NUMBER Inch) (MeasureFn (MultiplicationFn ?NUMBER 0.0254) Meter))
(equal (MeasureFn ?NUMBER KiloByte) (MeasureFn (MultiplicationFn ?NUMBER 1024) Byte))
(equal (MeasureFn ?NUMBER MegaByte) (MeasureFn (MultiplicationFn ?NUMBER 1024) KiloByte))
(equal (MeasureFn ?NUMBER MegaHertz) (MeasureFn (MultiplicationFn ?NUMBER 1.0E6) Hertz))
(equal (MeasureFn ?NUMBER Mile) (MeasureFn (MultiplicationFn ?NUMBER 1609.344) Meter))
(equal (MeasureFn ?NUMBER MinuteDuration) (MeasureFn (MultiplicationFn ?NUMBER 60) SecondDuration))
(equal (MeasureFn ?NUMBER Ounce) (MeasureFn (DivisionFn ?NUMBER 8) Cup))
(equal (MeasureFn ?NUMBER Pint) (MeasureFn (DivisionFn ?NUMBER 2) Quart))
(equal (MeasureFn ?NUMBER Pound) (MeasureFn (MultiplicationFn ?NUMBER 0.45359237) Kilogram))
(equal (MeasureFn ?NUMBER PoundForce) (MeasureFn (MultiplicationFn ?NUMBER 4.448222) Newton))
(equal (MeasureFn ?NUMBER Quart) (MeasureFn (DivisionFn ?NUMBER 4) UnitedStatesGallon))
(equal (MeasureFn ?NUMBER Rankine) (MeasureFn (MultiplicationFn ?NUMBER 1.8) Kelvin))
(equal (MeasureFn ?NUMBER Slug) (MeasureFn (MultiplicationFn ?NUMBER 14.59390) Kilogram))
(equal (MeasureFn ?NUMBER UnitedKingdomGallon) (MeasureFn (MultiplicationFn ?NUMBER 4.54609) Liter))
(equal (MeasureFn ?NUMBER UnitedStatesGallon) (MeasureFn (MultiplicationFn ?NUMBER 3.785411784) Liter))
(equal (MeasureFn ?NUMBER AngularDegree) (MeasureFn (MultiplicationFn ?NUMBER (DivisionFn Pi 180)) Radian))
(equal (MeasureFn ?NUMBER DayDuration) (MeasureFn (MultiplicationFn ?NUMBER 24) HourDuration))
(equal (MeasureFn ?NUMBER Gram) (MeasureFn (MultiplicationFn ?NUMBER 0.001) Kilogram))
(equal (MeasureFn ?NUMBER HourDuration) (MeasureFn (MultiplicationFn ?NUMBER 60) MinuteDuration))
(equal (MeasureFn ?NUMBER Kilogram) (MeasureFn (MultiplicationFn ?NUMBER 1000) Gram))
(equal (MeasureFn ?NUMBER KiloHertz) (MeasureFn (MultiplicationFn ?NUMBER 1000) Hertz))
(equal (MeasureFn ?NUMBER Kilometer) (MeasureFn (MultiplicationFn ?NUMBER 1000) Meter))
(equal (MeasureFn ?NUMBER KiloWatt) (MeasureFn (MultiplicationFn ?NUMBER 1000) Watt))
(equal (MeasureFn ?NUMBER MegaOhm) (MeasureFn (MultiplicationFn ?NUMBER 1.0E6) Ohm))
(equal (MeasureFn ?NUMBER MegaPascal) (MeasureFn (MultiplicationFn ?NUMBER 1.0E6) Pascal))
(equal (MeasureFn ?NUMBER MicroOhm) (MeasureFn (MultiplicationFn ?NUMBER 0.000001) Ohm))
(equal (MeasureFn ?NUMBER MicroVolt) (MeasureFn (MultiplicationFn ?NUMBER 0.000001) Volt))
(equal (MeasureFn ?NUMBER MilliAmpere) (MeasureFn (MultiplicationFn ?NUMBER .001) Ampere))
(equal (MeasureFn ?NUMBER MilliVolt) (MeasureFn (MultiplicationFn ?NUMBER .001) Volt))
(equal (MeasureFn ?NUMBER NanoAmpere) (MeasureFn (MultiplicationFn ?NUMBER 1.0E-9) Ampere))
(equal (MeasureFn ?NUMBER NanoSecond) (MeasureFn (MultiplicationFn ?NUMBER 1.0E-9) Second))
(equal (MeasureFn ?NUMBER PicoAmpere) (MeasureFn (MultiplicationFn ?NUMBER 1.0E-12) Ampere))
(equal (MeasureFn ?NUMBER PicoSecond) (MeasureFn (MultiplicationFn ?NUMBER 1.0E-12) SecondDuration))
(equal (MeasureFn ?NUMBER YearDuration) (MeasureFn (MultiplicationFn ?NUMBER 365) DayDuration))
Next BinaryFunction: MereologicalDifferenceFn Up: BinaryFunction Previous BinaryFunction: LogFn