| NonnegativeRealNumber
| |
| appearance as argument number 1 |
|
|
| (documentation NonnegativeRealNumber ChineseLanguage "这是一个大于或等于零的 RealNumber。") | Merge.kif 1996-1996 | |
| (documentation NonnegativeRealNumber EnglishLanguage "A RealNumber that is greater than or equal to zero.") | Merge.kif 1994-1995 | |
| (externalImage NonnegativeRealNumber "http://upload.wikimedia.org/wikipedia/ commons/ d/ dc/ Reelle_Zahlengerade_mit_Konstanten.png") | pictureList.kif 11535-11535 | |
| (externalImage NonnegativeRealNumber "http://upload.wikimedia.org/wikipedia/ commons/ f/ fd/ Recta_real_entero_o_decimal_exacto.png") | pictureList.kif 10170-10170 | |
| (subclass NonnegativeRealNumber RealNumber) | Merge.kif 1993-1993 |
| appearance as argument number 2 |
|
|
| (range AbsoluteValueFn NonnegativeRealNumber) | Merge.kif 4918-4918 | |
| (subclass NonnegativeInteger NonnegativeRealNumber) | Merge.kif 2048-2048 | |
| (subclass PositiveRealNumber NonnegativeRealNumber) | Merge.kif 2004-2004 | |
| (termFormat ChineseLanguage NonnegativeRealNumber "非负实数") | chinese_format.kif 863-863 | |
| (termFormat EnglishLanguage NonnegativeRealNumber "nonnegative real number") | english_format.kif 650-650 | |
| (termFormat JapaneseLanguage NonnegativeRealNumber "非負実数") | english_format.kif 651-651 |
| appearance as argument number 3 |
|
|
| (domain cloudCoverFraction 2 NonnegativeRealNumber) | Weather.kif 483-483 | |
| (domain incomeDistributionByGiniIndex 2 NonnegativeRealNumber) | Economy.kif 1296-1296 | |
| (domain incomeDistributionByGiniIndexInPeriod 2 NonnegativeRealNumber) | Economy.kif 1281-1281 | |
| (domain laborForceTotal 2 NonnegativeRealNumber) | Economy.kif 1372-1372 | |
| (domain laborForceTotalInPeriod 2 NonnegativeRealNumber) | Economy.kif 1362-1362 | |
| (domain overcastDaysInPeriod 3 NonnegativeRealNumber) | Weather.kif 566-566 | |
| (domain relativeHumidity 2 NonnegativeRealNumber) | Weather.kif 637-637 | |
| (domain slopeGradient 2 NonnegativeRealNumber) | Geography.kif 1616-1616 | |
| (partition RealNumber NegativeRealNumber NonnegativeRealNumber) | Merge.kif 1960-1960 |
| antecedent |
|
|
| (<=> (instance ?NUMBER NonnegativeRealNumber) (and (greaterThanOrEqualTo ?NUMBER 0) (instance ?NUMBER RealNumber))) |
Merge.kif 1998-2002 | |
| (=> (instance ?NUMBER NonnegativeRealNumber) (or (equal (SignumFn ?NUMBER) 1) (equal (SignumFn ?NUMBER) 0))) |
Merge.kif 5316-5320 |
| 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 ?NUMBER1))))) |
Merge.kif 4924-4935 |
|
|
|