NullList - Sigma Knowledge base Browser

appearance as argument number 1

(instance NullList List)	Merge.kif 3028-3028	Null list is an instance of list
(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 3030-3032	Null list is an instance of list

appearance as argument number 2

(termFormat EnglishLanguage NullList "null list")	domainEnglishFormat.kif 41420-41420
(termFormat ChineseTraditionalLanguage NullList "空列表")	domainEnglishFormat.kif 41421-41421
(termFormat ChineseLanguage NullList "空列表")	domainEnglishFormat.kif 41422-41422

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 3194-3213	If All of the following hold: (1) equal X, the list composed of Y, and Z (2) equal Y and null list (3) equal Z and null list (4) W is less than or equal to length of Y (5) V is less than or equal to length of Z (6) W is an instance of positive integer (7) V is an instance of positive integer, then equal U element of X and U element of Y and equal (length of Y and V)th element of X and T element of Z
(=> (and (instance ?LIST List) (not (equal ?LIST NullList))) (equal (FirstFn ?LIST) (ListOrderFn ?LIST 1)))	Merge.kif 3343-3348	If X is an instance of list and equal X and null list, then equal the first of X and 1th element of X

consequent

(=>
    (and
        (equal ?R
            (SubListFn ?S ?E ?L))
        (equal
            (SubtractionFn ?E ?S) 0))
    (equal ?R NullList))

If equal X and the sub-list from Y to Z of W and equal (Z and Y) and 0, then equal X and null list