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 4626-4628 | |
(domain AdditionFn 1 RealNumber) | Merge.kif 4622-4622 | The number 1 argument of addition is an instance of real number |
(domain AdditionFn 2 RealNumber) | Merge.kif 4623-4623 | The number 2 argument of addition is an instance of real number |
(identityElement AdditionFn 0) | Merge.kif 5201-5201 | 0 is an identity element of addition |
(instance AdditionFn AssociativeFunction) | Merge.kif 4618-4618 | Addition is an instance of associative function |
(instance AdditionFn BinaryFunction) | Merge.kif 4617-4617 | Addition is an instance of binary function |
(instance AdditionFn CommutativeFunction) | Merge.kif 4619-4619 | Addition is an instance of commutative function |
(instance AdditionFn TotalValuedRelation) | Merge.kif 4621-4621 | Addition is an instance of total valued relation |
(range AdditionFn RealNumber) | Merge.kif 4624-4624 | The range of addition is an instance of real number |
appearance as argument number 2 |
![]() |
(format ChineseLanguage AdditionFn "(%*[+])") | chinese_format.kif 682-682 | |
(format EnglishLanguage AdditionFn "(%*[+])") | english_format.kif 684-684 | |
(termFormat ChineseLanguage AdditionFn "加成") | domainEnglishFormat.kif 5427-5427 | |
(termFormat ChineseLanguage AdditionFn "加法函数") | chinese_format.kif 683-683 | |
(termFormat ChineseTraditionalLanguage AdditionFn "加成") | domainEnglishFormat.kif 5426-5426 | |
(termFormat EnglishLanguage AdditionFn "addition") | domainEnglishFormat.kif 5425-5425 |
antecedent |
![]() |
consequent |
![]() |
statement |
![]() |
(forall (?NUMBER) (equal (SuccessorFn ?NUMBER) (AdditionFn ?NUMBER 1))) |
Merge.kif 4630-4631 | For all an integer (the integer+1) is equal to (the integer and 1) |
![]() |
![]() |