ListSumFn |
appearance as argument number 1 |
(documentation ListSumFn EnglishLanguage "The sum of all the numbers in a List.") | Merge.kif 3242-3242 | |
(domain ListSumFn 1 List) | Merge.kif 3240-3240 | Die Zahl 1 Argument von ListSumFn ist ein fall von List %n{nicht} |
(instance ListSumFn UnaryFunction) | Merge.kif 3239-3239 | ListSumFn ist ein fall von UnaryFunction %n{nicht} |
(range ListSumFn RealNumber) | Merge.kif 3241-3241 | bildbereich von ListSumFn ist ein fall von RealNumber {nicht} |
appearance as argument number 2 |
(format EnglishLanguage ListSumFn "the sum of %1") | Merge.kif 3243-3243 | |
(termFormat EnglishLanguage ListSumFn "sum of elements") | Merge.kif 3244-3244 |
antecedent |
(=> (and (equal ?A (ListSumFn ?L)) (equal 1 (ListLengthFn ?L))) (equal ?A (ListOrderFn ?L 1))) |
Merge.kif 3252-3256 |
|
(=> (and (equal ?A (ListSumFn ?L)) (greaterThan (ListLengthFn ?L) 1)) (equal ?A (AdditionFn (FirstFn ?L) (ListSumFn (SubListFn 2 (ListLengthFn ?L) ?L))))) |
Merge.kif 3258-3268 |
|
consequent |