SubtractionFn |
appearance as argument number 1 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 2216-2219 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4730-4734 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 880-883 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4726-4726 | The number 1 argument of subtraction is an instance of real number |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4727-4727 | The number 2 argument of subtraction is an instance of real number |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5296-5296 | 0 is an identity element of subtraction |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4723-4723 | Subtraction is an instance of binary function |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4725-4725 | Subtraction is an instance of total valued relation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4728-4728 | The range of subtraction is an instance of real number |
appearance as argument number 2 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 684-684 | |
No TPTP formula. May not be expressible in strict first order. | english_format.kif 686-686 | |
No TPTP formula. May not be expressible in strict first order. | french_format.kif 415-415 | |
No TPTP formula. May not be expressible in strict first order. | relations-it.txt 285-285 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2132-2132 | |
No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 367-367 | |
No TPTP formula. May not be expressible in strict first order. | relations-cz.txt 424-424 | |
No TPTP formula. May not be expressible in strict first order. | relations-de.txt 891-891 | |
No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 322-322 | |
No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 437-437 | |
No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 459-459 | |
No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 477-477 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 55854-55854 | |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 685-685 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 55853-55853 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 55852-55852 |
antecedent |
consequent |
statement |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7012-7014 | A real number celsius degree(s) is equal to (the real number and 32.0) and 1.8 fahrenheit degree(s) |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7008-7010 | A real number celsius degree(s) is equal to (the real number and 273.15) kelvin degree(s) |
No TPTP formula. May not be expressible in strict first order. | Military.kif 933-946 | The reaching military age annually male of a geopolitical area and a year is equal to the number of instances in the class described by a symbolic string |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4736-4737 | For all an integer (the integer+2) is equal to (the integer and 1) |