BinaryNumber
|
|
appearance as argument number 1 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1755-1756 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2005-2006 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 364-365 | |
No TPTP formula. May not be expressible in strict first order. | pictureList.kif 4962-4962 | |
No TPTP formula. May not be expressible in strict first order. | pictureList.kif 4864-4864 | |
No TPTP formula. May not be expressible in strict first order. | pictureList.kif 4963-4963 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2003-2003 | Binary number is a subclass of real number |
appearance as argument number 2 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 873-873 | |
No TPTP formula. May not be expressible in strict first order. | english_format.kif 948-948 | |
No TPTP formula. May not be expressible in strict first order. | french_format.kif 549-549 | |
No TPTP formula. May not be expressible in strict first order. | terms-hindi.txt 79-79 | |
No TPTP formula. May not be expressible in strict first order. | terms-it.txt 82-82 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2234-2234 | |
No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 501-501 | |
No TPTP formula. May not be expressible in strict first order. | terms-cz.txt 116-116 | |
No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 570-570 | |
No TPTP formula. May not be expressible in strict first order. | terms-tg.txt 83-83 |
consequent |
No TPTP formula. May not be expressible in strict first order. | Media.kif 801-812 |
|