NullList
|
|
appearance as argument number 1 |
(documentation NullList ChineseLanguage "这是一个没有项目的 List,NullList 的独特之处是因为 List 是可以延伸,也就是说俩个含有相同项目以相同顺序排列的列表是一样的。") | chinese_format.kif 1960-1961 | |
(documentation NullList EnglishLanguage "The List that has no items. The uniqueness of NullList follows from the extensionality of Lists, i.e. the fact that two Lists with the same items in the same order are identical.") | Merge.kif 2920-2922 | |
(documentation NullList JapaneseLanguage "項目のない List 。NullList の一意性は、 Lists の拡張性、すなわち、同じ順序で同じ項目を持つ2つの List が同じであるという事実。") | japanese_format.kif 592-593 | |
(instance NullList List) | Merge.kif 2918-2918 |
appearance as argument number 2 |
(termFormat ChineseLanguage NullList "空列表") | domainEnglishFormat.kif 41423-41423 | |
(termFormat ChineseTraditionalLanguage NullList "空列表") | domainEnglishFormat.kif 41422-41422 | |
(termFormat EnglishLanguage NullList "null list") | domainEnglishFormat.kif 41421-41421 |
antecedent |
(=> (and (equal ?LIST3 (ListConcatenateFn ?LIST1 ?LIST2)) (not (equal ?LIST1 NullList)) (not (equal ?LIST2 NullList)) (lessThanOrEqualTo ?NUMBER1 (ListLengthFn ?LIST1)) (lessThanOrEqualTo ?NUMBER2 (ListLengthFn ?LIST2)) (instance ?NUMBER1 PositiveInteger) (instance ?NUMBER2 PositiveInteger)) (and (equal (ListOrderFn ?LIST3 ?NUMBER1) (ListOrderFn ?LIST1 ?NUMBER1)) (equal (ListOrderFn ?LIST3 (AdditionFn (ListLengthFn ?LIST1) ?NUMBER2)) (ListOrderFn ?LIST2 ?NUMBER2)))) |
Merge.kif 3084-3103 | |
(=> (and (instance ?LIST List) (not (equal ?LIST NullList))) (equal (FirstFn ?LIST) (ListOrderFn ?LIST 1))) |
Merge.kif 3233-3238 |
consequent |
(=> (and (equal ?R (SubListFn ?S ?E ?L)) (equal (SubtractionFn ?E ?S) 0)) (equal ?R NullList)) |
Merge.kif 3171-3178 |