(documentation exhaustiveDecomposition ChineseLanguage "C Class 的 exhaustiveDecomposition 是C的一组子类别， 而C的每一个实例就是这个组内其中一个子类别的一个实例。按： 这并不一定是意会着这个组的单元都不相交 （可参考 partition  一个 partition 是一个已列举尽 不相交的掏空成分。 ") 
chinese_format.kif 15111514 

(documentation exhaustiveDecomposition EnglishLanguage "An exhaustiveDecomposition of a Class C is a set of subclasses of C such that every instance of C is an instance of one of the subclasses in the set. Note: this does not necessarily mean that the elements of the set are disjoint (see partition  a partition is a disjoint exhaustive decomposition).") 
Merge.kif 552556 

(domain exhaustiveDecomposition 1 Class) 
Merge.kif 548548 
The number 1 argument of exhaustive decomposition is an instance of class 
(domain exhaustiveDecomposition 2 Class) 
Merge.kif 549549 
The number 2 argument of exhaustive decomposition is an instance of class 
(instance exhaustiveDecomposition Predicate) 
Merge.kif 546546 
exhaustive decomposition is an instance of predicate 
(instance exhaustiveDecomposition VariableArityRelation) 
Merge.kif 547547 
exhaustive decomposition is an instance of variable arity relation 
(relatedInternalConcept exhaustiveDecomposition partition) 
Merge.kif 550550 
exhaustive decomposition is internally related to partition 