| NegativeRealNumber(Numero Real negativo)
| |
| 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 | Numero Real negativo e' uma sub-classe de Numero Real |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1892-1892 | O conceito Numero Real e' completamente decomposto em Numero Real negativo + Numero Real nao-negativo |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1986-1986 | Inteiro negativo e' uma sub-classe de Numero Real negativo |
| 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 | Numero Real e' uma instancia de Numero Real negativo Numero Real e' menos que 0 Numero Real e' uma instancia de Numero Real |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5206-5208 |
|
| consequent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4769-4780 | O valor absoluto de Numero Real e' igual a Numero Real nao-negativo Numero Real e' uma instancia de Numero Real Numero Real nao-negativo e' uma instancia de Numero Real Numero Real e' uma instancia de Numero Real nao-negativo Numero Real e' igual a Numero Real nao-negativo Numero Real e' uma instancia de Numero Real negativo Numero Real nao-negativo e' igual a (0.0 + Numero Real) |
|
|
|