ListFn |
appearance as argument number 1 |
(documentation ListFn ChineseLanguage "这是一个可以接受任何数量的参数,然后交出含有跟哪些参数完全 相同顺序的 Function。") | chinese_format.kif 1962-1963 | |
(documentation ListFn EnglishLanguage "A Function that takes any number of arguments and returns the List containing those arguments in exactly the same order.") | Merge.kif 2938-2939 | |
(documentation ListFn JapaneseLanguage "任意の数の引数を受け取り、それらの引数を含む List を まったく同じ順序で返す Function。") | japanese_format.kif 594-595 | |
(domain ListFn 1 Entity) | Merge.kif 2934-2934 | The number 1 argument of list is an instance of entity |
(instance ListFn Function) | Merge.kif 2932-2932 | List is an instance of function |
(instance ListFn VariableArityRelation) | Merge.kif 2933-2933 | List is an instance of variable arity relation |
(range ListFn List) | Merge.kif 2936-2936 | The range of list is an instance of list |
appearance as argument number 2 |
(format ChineseLanguage ListFn "(%*[,])") | chinese_format.kif 261-261 | |
(format EnglishLanguage ListFn "(%*[,])") | english_format.kif 266-266 | |
(format FrenchLanguage ListFn "(%*[,])") | french_format.kif 149-149 | |
(format ItalianLanguage ListFn "(%*[,]") | relations-it.txt 167-167 | |
(format JapaneseLanguage ListFn "(%*[,])") | japanese_format.kif 1977-1977 | |
(format PortugueseLanguage ListFn "(%*[,])") | portuguese_format.kif 101-101 | |
(format cz ListFn "(%*[,])") | relations-cz.txt 158-158 | |
(format de ListFn "(%*[,])") | relations-de.txt 336-336 | |
(format hi ListFn "(%*[,]") | relations-hindi.txt 206-206 | |
(format ro ListFn "(%*[,])") | relations-ro.kif 168-168 | |
(format sv ListFn "(%*[,])") | relations-sv.txt 155-155 | |
(format tg ListFn "(%*[,]") | relations-tg.txt 333-333 | |
(termFormat ChineseLanguage ListFn "名单") | domainEnglishFormat.kif 34719-34719 | |
(termFormat ChineseLanguage ListFn "表列函数") | chinese_format.kif 262-262 | |
(termFormat ChineseTraditionalLanguage ListFn "名單") | domainEnglishFormat.kif 34718-34718 | |
(termFormat EnglishLanguage ListFn "list") | domainEnglishFormat.kif 34717-34717 | |
(termFormat de ListFn "ListeFn") | terms-de.txt 107-107 | |
(termFormat tg ListFn "tungkulin ng talaan") | relations-tg.txt 334-334 |
antecedent |
consequent |
(=> (and (domain ?REL ?NUMBER ?CLASS) (instance ?REL Predicate) (?REL @ROW)) (instance (ListOrderFn (ListFn @ROW) ?NUMBER) ?CLASS)) |
Merge.kif 2999-3004 |
|
(=> (and (domainSubclass ?REL ?NUMBER ?CLASS) (instance ?REL Predicate) (?REL @ROW)) (subclass (ListOrderFn (ListFn @ROW) ?NUMBER) ?CLASS)) |
Merge.kif 3006-3011 |
|
(=> (and (equal (GreatestCommonDivisorFn @ROW) ?NUMBER) (not (equal ?NUMBER 0))) (forall (?ELEMENT) (=> (inList ?ELEMENT (ListFn @ROW)) (equal (RemainderFn ?ELEMENT ?NUMBER) 0)))) |
Merge.kif 4862-4873 |
|
(=> (and (equal (GreatestCommonDivisorFn @ROW) ?NUMBER) (not (equal ?NUMBER 0))) (not (exists (?GREATER) (and (greaterThan ?GREATER ?NUMBER) (forall (?ELEMENT) (=> (inList ?ELEMENT (ListFn @ROW)) (equal (RemainderFn ?ELEMENT ?GREATER) 0))))))) |
Merge.kif 4875-4889 |
|
(=> (and (equal (LeastCommonMultipleFn @ROW) ?NUMBER) (not (equal ?NUMBER 0))) (forall (?ELEMENT) (=> (inList ?ELEMENT (ListFn @ROW)) (equal (RemainderFn ?NUMBER ?ELEMENT) 0)))) |
Merge.kif 4947-4957 |
|
(=> (and (equal (LeastCommonMultipleFn @ROW) ?NUMBER) (not (equal ?NUMBER 0))) (not (exists (?LESS) (and (lessThan ?LESS ?NUMBER) (forall (?ELEMENT) (=> (inList ?ELEMENT (ListFn @ROW)) (equal (RemainderFn ?LESS ?ELEMENT) 0))))))) |
Merge.kif 4959-4973 |
|
(=> (and (equal ?LIST1 ?LIST2) (equal ?LIST1 (ListFn @ROW1)) (equal ?LIST2 (ListFn @ROW2))) (equal (ListOrderFn (ListFn @ROW1) ?NUMBER) (ListOrderFn (ListFn @ROW2) ?NUMBER))) |
Merge.kif 295-302 |
|
(=> (and (equal ?R (SubListFn ?S ?E ?L)) (equal (SubtractionFn ?E ?S) 1)) (equal ?R (ListFn (ListOrderFn ?L ?S)))) |
Merge.kif 3180-3189 |
|
(=> (and (equal ?R (SubListFn ?S ?E ?L)) (greaterThan (SubtractionFn ?E ?S) 1)) (equal ?R (ListConcatenateFn (ListFn (ListOrderFn ?L ?S)) (SubListFn (AdditionFn 1 ?S) ?E ?L)))) |
Merge.kif 3191-3203 |
|
(=> (and (exactCardinality ?REL ?ARG 1) (instance ?REL Predicate) (?REL @ARGS) (equal ?X (ListOrderFn (ListFn @ARGS) ?ARG))) (not (exists (?Y) (and (equal ?Y (ListOrderFn (ListFn @ARGS) ?ARG)) (not (equal ?X ?Y)))))) |
Media.kif 2093-2103 |
|
(=> (and (exactCardinality ?REL ?ARG 1) (instance ?REL Predicate)) (exists (?X @ARGS) (and (?REL @ARGS) (equal ?X (ListOrderFn (ListFn @ARGS) ?ARG)) (not (exists (?Y) (and (equal ?Y (ListOrderFn (ListFn @ARGS) ?ARG)) (not (equal ?X ?Y)))))))) |
Media.kif 2075-2090 |
|
(=> (and (exactCardinality ?REL ?ARG ?COUNT) (instance ?REL Predicate)) (exists (?S ?EL @ARGS) (and (instance ?S SetOrClass) (=> (and (?REL @ARGS) (equal ?EL (ListOrderFn (ListFn @ARGS) ?ARG))) (and (instance ?EL ?S) (equal (CardinalityFn ?S) ?COUNT)))))) |
Media.kif 2137-2150 |
|
(=> (and (maxCardinality ?REL ?ARG ?COUNT) (instance ?REL Predicate)) (exists (?S ?EL @ARGS) (and (instance ?S SetOrClass) (=> (and (?REL @ARGS) (equal ?EL (ListOrderFn (ListFn @ARGS) ?ARG))) (and (instance ?EL ?S) (lessThanOrEqualTo (CardinalityFn ?S) ?COUNT)))))) |
Media.kif 2210-2223 |
|
(=> (and (minCardinality ?REL ?ARG ?COUNT) (instance ?REL Predicate)) (exists (?S ?EL @ARGS) (and (instance ?S SetOrClass) (=> (and (?REL @ARGS) (equal ?EL (ListOrderFn (ListFn @ARGS) ?ARG))) (and (instance ?EL ?S) (greaterThanOrEqualTo (CardinalityFn ?S) ?COUNT)))))) |
Media.kif 2174-2187 |
|
(=> (and (valence ?REL ?NUMBER) (instance ?REL Predicate)) (forall (@ROW) (=> (?REL @ROW) (equal (ListLengthFn (ListFn @ROW)) ?NUMBER)))) |
Merge.kif 3049-3056 |
|
(=> (contraryAttribute @ROW) (=> (inList ?ELEMENT (ListFn @ROW)) (instance ?ELEMENT Attribute))) |
Merge.kif 464-468 |
|
(=> (disjointDecomposition ?CLASS @ROW) (forall (?ITEM) (=> (inList ?ITEM (ListFn @ROW)) (subclass ?ITEM ?CLASS)))) |
Merge.kif 2951-2956 |
|
(=> (disjointDecomposition ?CLASS @ROW) (forall (?ITEM1 ?ITEM2) (=> (and (inList ?ITEM1 (ListFn @ROW)) (inList ?ITEM2 (ListFn @ROW)) (not (equal ?ITEM1 ?ITEM2))) (disjoint ?ITEM1 ?ITEM2)))) |
Merge.kif 2958-2967 |
|
(=> (disjointDecomposition @ROW) (=> (inList ?ELEMENT (ListFn @ROW)) (instance ?ELEMENT Class))) |
Merge.kif 574-578 |
|
(=> (equal (GreatestCommonDivisorFn @ROW) ?NUMBER) (=> (inList ?ELEMENT (ListFn @ROW)) (instance ?ELEMENT Number))) |
Merge.kif 4855-4860 |
|
(=> (equal (LeastCommonMultipleFn @ROW) ?NUMBER) (=> (inList ?ELEMENT (ListFn @ROW)) (instance ?ELEMENT Number))) |
Merge.kif 4940-4945 |
|
(=> (exactCardinality ?REL ?ARG ?COUNT) (exists (?EL @ARGS) (equal (CardinalityFn (KappaFn ?EL (and (?REL @ARGS) (equal ?EL (ListOrderFn (ListFn @ARGS) ?ARG))))) ?COUNT))) |
Media.kif 2125-2134 |
|
(=> (exhaustiveAttribute ?ATTRCLASS @ROW) (not (exists (?EL) (and (instance ?EL ?ATTRCLASS) (not (exists (?ATTR ?NUMBER) (and (equal ?EL ?ATTR) (equal ?ATTR (ListOrderFn (ListFn @ROW) ?NUMBER))))))))) |
Merge.kif 519-531 |
|
(=> (exhaustiveAttribute ?CLASS @ROW) (forall (?ATTR1) (=> (instance ?ATTR1 ?CLASS) (exists (?ATTR2) (and (inList ?ATTR2 (ListFn @ROW)) (equal ?ATTR1 ?ATTR2)))))) |
Merge.kif 509-517 |
|
(=> (exhaustiveDecomposition ?CLASS @ROW) (forall (?OBJ) (=> (instance ?OBJ ?CLASS) (exists (?ITEM) (and (inList ?ITEM (ListFn @ROW)) (instance ?OBJ ?ITEM)))))) |
Merge.kif 2941-2949 |
|
Display limited to 25 items. Show next 25 | ||
Display limited to 25 items. Show next 25 |
statement |
(forall (@ROW ?ITEM) (equal (ListLengthFn (ListFn @ROW ?ITEM)) (SuccessorFn (ListLengthFn (ListFn @ROW))))) |
Merge.kif 3038-3041 | For all @ROW and another entity length of (@ROW and the other entity) is equal to (length of (@ROW)+1) |
(forall (@ROW ?ITEM) (equal (ListOrderFn (ListFn @ROW ?ITEM) (ListLengthFn (ListFn @ROW ?ITEM))) ?ITEM)) |
Merge.kif 3043-3047 | For all @ROW and another entity length of (@ROW and the other entity)th element of (@ROW and the other entity) is equal to the other entity |
(forall (@ROW ?ITEM) (initialList (ListFn @ROW) (ListFn @ROW ?ITEM))) |
Merge.kif 3316-3317 | For all @ROW and another entity (@ROW) starts (@ROW and the other entity) |