| NonnegativeRealNumber(非負実数)
| |
| appearance as argument number 1 |
|
|
| (documentation NonnegativeRealNumber ChineseLanguage "这是一个大于或等于零的 RealNumber。") | chinese_format.kif 1745-1745 | |
| (documentation NonnegativeRealNumber EnglishLanguage "A RealNumber that is greater than or equal to zero.") | Merge.kif 1934-1935 | |
| (documentation NonnegativeRealNumber JapaneseLanguage "ゼロ 以上の RealNumber 。") | japanese_format.kif 353-353 | |
| (externalImage NonnegativeRealNumber "http://upload.wikimedia.org/wikipedia/ commons/ d/ dc/ Reelle_Zahlengerade_mit_Konstanten.png") | pictureList.kif 11501-11501 | |
| (externalImage NonnegativeRealNumber "http://upload.wikimedia.org/wikipedia/ commons/ f/ fd/ Recta_real_entero_o_decimal_exacto.png") | pictureList.kif 10147-10147 | |
| (subclass NonnegativeRealNumber RealNumber) | Merge.kif 1932-1932 | 非負実数 は 実数 の subclass では |
| appearance as argument number 2 |
|
|
| appearance as argument number 3 |
|
|
| antecedent |
|
|
| (<=> (instance ?NUMBER NonnegativeRealNumber) (and (greaterThanOrEqualTo ?NUMBER 0) (instance ?NUMBER RealNumber))) |
Merge.kif 1937-1941 | 実数 は 非負実数 の instance では 実数 は 0 greater では 実数 は 実数 の instance では |
| (=> (instance ?NUMBER NonnegativeRealNumber) (or (equal (SignumFn ?NUMBER) 1) (equal (SignumFn ?NUMBER) 0))) |
Merge.kif 5223-5227 |
| 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 4796-4807 | equal 実数 の absolute value and 非負実数 実数 は 実数 の instance では 非負実数 は 実数 の instance では 実数 は 非負実数 の instance では equal 実数 and 非負実数 実数 は 負の実数 の instance では equal 非負実数 and (0.0 + 実数) |
|
|
|