BinaryNumber | *documentation* Elements from the number system with base 2. Every BinaryNumber is expressed as a sequence of the digits 1 *and* 0 | |

**is a kind of** RealNumber | |

RealNumber | **has axiom** (=> (*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)))))
| |

**has axiom** (=> (*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)))))
| |

**has axiom** (=> (*instance* ?NUMBER *ImaginaryNumber*) (*instance* ?NUMBER (*RelativeComplementFn* Number RealNumber)))
| |

**is first ***domain* of *AbsoluteValueFn* | |

**is first ***domain* of *ArcCosineFn* | |

**is first ***domain* of *ArcSineFn* | |

**is first ***domain* of *ArcTangentFn* | |

**is first ***domain* of *CeilingFn* | |

**is first ***domain* of *DenominatorFn* | |

**is first ***domain* of *FloorFn* | |

**is first ***domain* of *IntegerSquareRootFn* | |

**is first ***domain* of *LogFn* | |

**is first ***domain* of *MeasureFn* | |

**is first ***domain* of *NumeratorFn* | |

**is first ***domain* of *SignumFn* | |

**is first ***domain* of *SquareRootFn* | |

**is partitioned into** NegativeRealNumber, NonnegativeRealNumber | |

Quantity | **is second ***domain* of *AdditionFn* | |

**is second ***domain* of *DivisionFn* | |

**is second ***domain* of *greaterThan* | |

**is second ***domain* of *greaterThanOrEqualTo* | |

**is second ***domain* of *lessThan* | |

**is second ***domain* of *lessThanOrEqualTo* | |

**is second ***domain* of *MaxFn* | |

**is second ***domain* of *MinFn* | |

**is second ***domain* of *MultiplicationFn* | |

**is second ***domain* of *RemainderFn* | |

**is second ***domain* of *SubtractionFn* | |

Abstract | **is ***disjoint* from Physical | |