AmountsFn |
appearance as argument number 1 |
(documentation AmountsFn EnglishLanguage "A List of all the MassMeasures of instances of a type of Substance found in an Object.") | Merge.kif 7574-7576 | |
(domain AmountsFn 2 CorpuscularObject) | Merge.kif 7578-7578 | 域 AmountsFn, 2 and CorpuscularObject |
(domain AmountsFn 3 UnitOfMass) | Merge.kif 7579-7579 | 域 AmountsFn, 3 and UnitOfMass |
(domainSubclass AmountsFn 1 Substance) | Merge.kif 7577-7577 | 域子類 AmountsFn, 1 and Substance |
(instance AmountsFn BinaryFunction) | Merge.kif 7573-7573 | 例 AmountsFn and BinaryFunction |
(range AmountsFn List) | Merge.kif 7580-7580 | 範圍 AmountsFn and List |
appearance as argument number 2 |
(termFormat EnglishLanguage AmountsFn "Amounts fn") | domainEnglishFormat.kif 64441-64441 |
antecedent |
(=> (and (inList ?E ?L) (equal ?L (AmountsFn ?S ?CO ?U))) (instance ?E RationalNumber)) |
Merge.kif 7582-7587 |
|
consequent |
(=> (and (amount ?S ?CO (MeasureFn ?N ?U)) (instance ?SI ?S) (measure ?SI (MeasureFn ?N2 ?U)) (part ?SI ?CO)) (exists (?L) (and (inList (MeasureFn ?N2 ?U) ?L) (equal ?L (AmountsFn ?S ?CO ?U)) (equal ?N (ListSumFn ?L))))) |
Merge.kif 7596-7611 |
|