|
|
   NegativeRealNumber
|
|
|
| appearance as argument number 1 |
|
|
| (documentation NegativeRealNumber ChineseLanguage "这是一个小于零的 RealNumber。") | chinese_format.kif 1747-1747 | |
| (documentation NegativeRealNumber EnglishLanguage "A RealNumber that is less than zero.") | Merge.kif 1885-1886 | |
| (externalImage NegativeRealNumber "http://upload.wikimedia.org/wikipedia/ commons/ 0/ 09/ Number-line.gif") | pictureList.kif 10155-10155 | |
| (subclass NegativeRealNumber RealNumber) | Merge.kif 1883-1883 | subclass NegativeRealNumber and RealNumber |
| appearance as argument number 2 |
|
|
| (partition RealNumber NegativeRealNumber NonnegativeRealNumber) | Merge.kif 1832-1832 | partition RealNumber, NegativeRealNumber and NonnegativeRealNumber |
| (subclass NegativeInteger NegativeRealNumber) | Merge.kif 1926-1926 | subclass NegativeInteger and NegativeRealNumber |
| (termFormat ChineseLanguage NegativeRealNumber "负实数") | chinese_format.kif 865-865 | |
| (termFormat EnglishLanguage NegativeRealNumber "negative real number") | english_format.kif 932-932 |
| antecedent |
|
|
| (<=> (instance ?NUMBER NegativeRealNumber) (and (lessThan ?NUMBER 0) (instance ?NUMBER RealNumber))) |
Merge.kif 1888-1892 | instance RealNumber and NegativeRealNumber lessThan RealNumber and 0 instance RealNumber and RealNumber |
| (=> (instance ?NUMBER NegativeRealNumber) (equal (SignumFn ?NUMBER) -1)) |
Merge.kif 5105-5107 |
|
| consequent |
|
|
| (<=> (and (equal (AbsoluteValueFn ?NUMBER1) ?NUMBER2) (instance ?NUMBER1 RealNumber) (instance ?NUMBER2 RealNumber)) (or (and (instance ?NUMBER1 NonnegativeRealNumber) (equal ?NUMBER1 ?NUMBER2)) (and (instance ?NUMBER1 NegativeRealNumber) (equal ?NUMBER2 (SubtractionFn 0.0 ?NUMBER1))))) |
Merge.kif 4672-4683 | equal AbsoluteValueFn RealNumber and NonnegativeRealNumber instance RealNumber and RealNumber instance NonnegativeRealNumber and RealNumber instance RealNumber and NonnegativeRealNumber equal RealNumber and NonnegativeRealNumber instance RealNumber and NegativeRealNumber equal NonnegativeRealNumber and SubtractionFn 0.0 and RealNumber |
|
|
|
