AdditionFn |
appearance as argument number 1 |
(documentation AdditionFn ChineseLanguage "如果 ?NUMBER1 和 ?NUMBER2 是 Number,那么 (AdditionFn ?NUMBER1 ?NUMBER2)就是这些数字的算术和。") | chinese_format.kif 2214-2215 | |
(documentation AdditionFn EnglishLanguage "If ?NUMBER1 and ?NUMBER2 are Numbers, then (AdditionFn ?NUMBER1 ?NUMBER2) is the arithmetical sum of these numbers.") | Merge.kif 4717-4719 | |
(documentation AdditionFn JapaneseLanguage "?NUMBER1 と ?NUMBER2 が Number の場合、 (AdditionFn ?NUMBER1 ?NUMBER2) はこれらの数値の算術合計である。") | japanese_format.kif 878-879 | |
(domain AdditionFn 1 RealNumber) | Merge.kif 4713-4713 | Le nombre 1 argument de AdditionFn est une instance de nombre r�el |
(domain AdditionFn 2 RealNumber) | Merge.kif 4714-4714 | Le nombre 2 argument de AdditionFn est une instance de nombre r�el |
(identityElement AdditionFn 0) | Merge.kif 5296-5296 | 0 est un AdditionFn |
(instance AdditionFn AssociativeFunction) | Merge.kif 4709-4709 | AdditionFn est une instance de fonction associative |
(instance AdditionFn BinaryFunction) | Merge.kif 4708-4708 | AdditionFn est une instance de fonction binaire |
(instance AdditionFn CommutativeFunction) | Merge.kif 4710-4710 | AdditionFn est une instance de function commutative |
(instance AdditionFn TotalValuedRelation) | Merge.kif 4712-4712 | AdditionFn est une instance de relation total |
(range AdditionFn RealNumber) | Merge.kif 4715-4715 | Le domaine de AdditionFn est une instance de nombre r�el |
appearance as argument number 2 |
(format ChineseLanguage AdditionFn "(%*[+])") | chinese_format.kif 682-682 | |
(format EnglishLanguage AdditionFn "(%*[+])") | english_format.kif 684-684 | |
(format FrenchLanguage AdditionFn "(%*[+])") | french_format.kif 414-414 | |
(format ItalianLanguage AdditionFn "(%*[+]") | relations-it.txt 20-20 | |
(format JapaneseLanguage AdditionFn "(%*[+])") | japanese_format.kif 2131-2131 | |
(format PortugueseLanguage AdditionFn "(%*[+])") | portuguese_format.kif 366-366 | |
(format cz AdditionFn "(%*[+])") | relations-cz.txt 423-423 | |
(format de AdditionFn "(%*[+])") | relations-de.txt 889-889 | |
(format hi AdditionFn "(%*[+]") | relations-hindi.txt 65-65 | |
(format ro AdditionFn "(%*[+])") | relations-ro.kif 436-436 | |
(format sv AdditionFn "(%*[+])") | relations-sv.txt 458-458 | |
(format tg AdditionFn "(%*[+]") | relations-cb.txt 54-54 | |
(termFormat ChineseLanguage AdditionFn "加成") | domainEnglishFormat.kif 5422-5422 | |
(termFormat ChineseLanguage AdditionFn "加法函数") | chinese_format.kif 683-683 | |
(termFormat ChineseTraditionalLanguage AdditionFn "加成") | domainEnglishFormat.kif 5421-5421 | |
(termFormat EnglishLanguage AdditionFn "addition") | domainEnglishFormat.kif 5420-5420 | |
(termFormat tg AdditionFn "tungkulin ng pagsasama") | relations-tg.txt 57-57 |
antecedent |
consequent |
statement |
(forall (?NUMBER) (equal (SuccessorFn ?NUMBER) (AdditionFn ?NUMBER 1))) |
Merge.kif 4721-4722 | Nombre entier ( nombre entier+1) est nombre entier + 1) |