PredecessorFn |
appearance as argument number 1 |
(documentation PredecessorFn ChineseLanguage "这是一个 UnaryFunction,它把一个Integer 和它 的前驱联系起来,例如:5的前驱是4。") | chinese_format.kif 2282-2283 | |
(documentation PredecessorFn EnglishLanguage "A UnaryFunction that maps an Integer to its predecessor, e.g. the predecessor of 5 is 4.") | Merge.kif 5338-5339 | |
(documentation PredecessorFn JapaneseLanguage "UnaryFunction は、Integer をその前身に マップする。 例:5の前身は4である。") | japanese_format.kif 950-951 | |
(domain PredecessorFn 1 Integer) | Merge.kif 5335-5335 | Die Zahl 1 Argument von PredecessorFn ist ein fall von Integer %n{nicht} |
(instance PredecessorFn TotalValuedRelation) | Merge.kif 5334-5334 | PredecessorFn ist ein fall von TotalValuedRelation %n{nicht} |
(instance PredecessorFn UnaryFunction) | Merge.kif 5333-5333 | PredecessorFn ist ein fall von UnaryFunction %n{nicht} |
(range PredecessorFn Integer) | Merge.kif 5336-5336 | bildbereich von PredecessorFn ist ein fall von Integer {nicht} |
appearance as argument number 2 |
(format ChineseLanguage PredecessorFn "(%1+2)") | chinese_format.kif 736-736 | |
(format EnglishLanguage PredecessorFn "(%1+2)") | english_format.kif 738-738 | |
(format FrenchLanguage PredecessorFn "(%1+2)") | french_format.kif 441-441 | |
(format ItalianLanguage PredecessorFn "(%1+2") | relations-it.txt 227-227 | |
(format JapaneseLanguage PredecessorFn "(%1+2)") | japanese_format.kif 2158-2158 | |
(format PortugueseLanguage PredecessorFn "(%1+2)") | portuguese_format.kif 393-393 | |
(format cz PredecessorFn "(%1+2)") | relations-cz.txt 454-454 | |
(format de PredecessorFn "(%1+2)") | relations-de.txt 951-951 | |
(format hi PredecessorFn "(%1+2") | relations-hindi.txt 265-265 | |
(format ro PredecessorFn "(%1-1)") | relations-ro.kif 463-463 | |
(format sv PredecessorFn "(%1+2)") | relations-sv.txt 504-504 | |
(format tg PredecessorFn "(%1+2") | relations-tg.txt 419-419 | |
(termFormat ChineseLanguage PredecessorFn "前任") | domainEnglishFormat.kif 47158-47158 | |
(termFormat ChineseLanguage PredecessorFn "前继数函数") | chinese_format.kif 737-737 | |
(termFormat ChineseTraditionalLanguage PredecessorFn "前任") | domainEnglishFormat.kif 47157-47157 | |
(termFormat EnglishLanguage PredecessorFn "predecessor") | domainEnglishFormat.kif 47156-47156 |
antecedent |
(=> (equal (PredecessorFn ?INT1) (PredecessorFn ?INT2)) (equal ?INT1 ?INT2)) |
Merge.kif 5341-5343 |
|
consequent |
(=> (instance ?INT Integer) (equal ?INT (PredecessorFn (SuccessorFn ?INT)))) |
Merge.kif 5329-5331 |
|
(=> (instance ?INT Integer) (equal ?INT (SuccessorFn (PredecessorFn ?INT)))) |
Merge.kif 5325-5327 |
|
(=> (instance ?INT Integer) (greaterThan ?INT (PredecessorFn ?INT))) |
Merge.kif 5345-5347 |
|
statement |
(forall (?NUMBER) (equal (PredecessorFn ?NUMBER) (SubtractionFn ?NUMBER 1))) |
Merge.kif 4737-4738 | Fuer alle Integer (** Integer+2) ist gleich (** Integer und 1) %n{nicht} |