NegativeRealNumber(负实数) |
appearance as argument number 1 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1747-1747 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1945-1946 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 355-355 | |
No TPTP formula. May not be expressible in strict first order. | pictureList.kif 10145-10145 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1943-1943 | 负实数 是 实数 的 subclass |
appearance as argument number 2 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1892-1892 | 实数 详尽无遗地 partition 成 负实数 和 非负实数 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1986-1986 | 负整数 是 负实数 的 subclass |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 865-865 | |
No TPTP formula. May not be expressible in strict first order. | english_format.kif 932-932 | |
No TPTP formula. May not be expressible in strict first order. | french_format.kif 541-541 | |
No TPTP formula. May not be expressible in strict first order. | terms-hindi.txt 71-71 | |
No TPTP formula. May not be expressible in strict first order. | terms-it.txt 74-74 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2226-2226 | |
No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 493-493 | |
No TPTP formula. May not be expressible in strict first order. | terms-cz.txt 108-108 | |
No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 562-562 | |
No TPTP formula. May not be expressible in strict first order. | terms-tg.txt 75-75 |
antecedent |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1948-1952 | 实数 是 负实数 的 instance 若且唯若 那个 实数 是 lessThan 0 和 那个 实数 是 实数 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5205-5207 |
consequent |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4768-4779 | 实数 的绝对值 equal 非负实数 和 那个 实数 是 实数 的 instance 和 那个 非负实数 是 实数 的 instance 若且唯若 那个 实数 是 非负实数 的 instance 和 那个 实数 equal 那个 非负实数 或 那个 实数 是 负实数 的 instance 和 那个 非负实数 equal (0.0 和 那个 实数) |