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 2871-2872 | |
(domain ListFn 1 Entity) | Merge.kif 2867-2867 | The number 1 argument of list is an instance of entity |
(instance ListFn Function) | Merge.kif 2865-2865 | List is an instance of function |
(instance ListFn VariableArityRelation) | Merge.kif 2866-2866 | List is an instance of variable arity relation |
(range ListFn List) | Merge.kif 2869-2869 | 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 | |
(termFormat ChineseLanguage ListFn "名单") | domainEnglishFormat.kif 34668-34668 | |
(termFormat ChineseLanguage ListFn "表列函数") | chinese_format.kif 262-262 | |
(termFormat ChineseTraditionalLanguage ListFn "名單") | domainEnglishFormat.kif 34667-34667 | |
(termFormat EnglishLanguage ListFn "list") | domainEnglishFormat.kif 34666-34666 |
antecedent |
![]() |
consequent |
![]() |
(=> (and (domain ?REL ?NUMBER ?CLASS) (instance ?REL Predicate) (?REL @ROW)) (instance (ListOrderFn (ListFn @ROW) ?NUMBER) ?CLASS)) |
Merge.kif 2932-2937 |
|
(=> (and (domainSubclass ?REL ?NUMBER ?CLASS) (instance ?REL Predicate) (?REL @ROW)) (subclass (ListOrderFn (ListFn @ROW) ?NUMBER) ?CLASS)) |
Merge.kif 2939-2944 |
|
(=> (and (equal (GreatestCommonDivisorFn @ROW) ?NUMBER) (not (equal ?NUMBER 0))) (forall (?ELEMENT) (=> (inList ?ELEMENT (ListFn @ROW)) (equal (RemainderFn ?ELEMENT ?NUMBER) 0)))) |
Merge.kif 4771-4782 |
|
(=> (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 4784-4798 |
|
(=> (and (equal (LeastCommonMultipleFn @ROW) ?NUMBER) (not (equal ?NUMBER 0))) (forall (?ELEMENT) (=> (inList ?ELEMENT (ListFn @ROW)) (equal (RemainderFn ?NUMBER ?ELEMENT) 0)))) |
Merge.kif 4856-4866 |
|
(=> (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 4868-4882 |
|
(=> (and (equal ?R (SubListFn ?S ?E ?L)) (equal (SubtractionFn ?E ?S) 1)) (equal ?R (ListFn (ListOrderFn ?L ?S)))) |
Merge.kif 3113-3122 |
|
(=> (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 3124-3136 |
|
(=> (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 2091-2101 |
|
(=> (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 2073-2088 |
|
(=> (and (exactCardinality ?REL ?ARG ?COUNT) (instance ?REL Predicate)) (exists (?S) (and (instance ?S SetOrClass) (=> (and (?REL @ARGS) (equal ?EL (ListOrderFn (ListFn @ARGS) ?ARG))) (and (instance ?EL ?S) (equal (CardinalityFn ?S) ?COUNT)))))) |
Media.kif 2130-2143 |
|
(=> (and (maxCardinality ?REL ?ARG ?COUNT) (instance ?REL Predicate)) (exists (?S) (and (instance ?S SetOrClass) (=> (and (?REL @ARGS) (equal ?EL (ListOrderFn (ListFn @ARGS) ?ARG))) (and (instance ?EL ?S) (lessThanOrEqualTo (CardinalityFn ?S) ?COUNT)))))) |
Media.kif 2201-2214 |
|
(=> (and (minCardinality ?REL ?ARG ?COUNT) (instance ?REL Predicate)) (exists (?S) (and (instance ?S SetOrClass) (=> (and (?REL @ARGS) (equal ?EL (ListOrderFn (ListFn @ARGS) ?ARG))) (and (instance ?EL ?S) (greaterThanOrEqualTo (CardinalityFn ?S) ?COUNT)))))) |
Media.kif 2166-2179 |
|
(=> (and (valence ?REL ?NUMBER) (instance ?REL Predicate)) (forall (@ROW) (=> (?REL @ROW) (equal (ListLengthFn (ListFn @ROW)) ?NUMBER)))) |
Merge.kif 2982-2989 |
|
(=> (contraryAttribute @ROW) (=> (inList ?ELEMENT (ListFn @ROW)) (instance ?ELEMENT Attribute))) |
Merge.kif 462-466 |
|
(=> (contraryAttribute @ROW) (forall (?ATTR1 ?ATTR2) (=> (and (equal ?ATTR1 (ListOrderFn (ListFn @ROW) ?NUMBER1)) (equal ?ATTR2 (ListOrderFn (ListFn @ROW) ?NUMBER2)) (not (equal ?NUMBER1 ?NUMBER2))) (=> (property ?OBJ ?ATTR1) (not (property ?OBJ ?ATTR2)))))) |
Merge.kif 474-484 |
|
(=> (disjointDecomposition ?CLASS @ROW) (forall (?ITEM) (=> (inList ?ITEM (ListFn @ROW)) (subclass ?ITEM ?CLASS)))) |
Merge.kif 2884-2889 |
|
(=> (disjointDecomposition ?CLASS @ROW) (forall (?ITEM1 ?ITEM2) (=> (and (inList ?ITEM1 (ListFn @ROW)) (inList ?ITEM2 (ListFn @ROW)) (not (equal ?ITEM1 ?ITEM2))) (disjoint ?ITEM1 ?ITEM2)))) |
Merge.kif 2891-2900 |
|
(=> (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 4764-4769 |
|
(=> (equal (LeastCommonMultipleFn @ROW) ?NUMBER) (=> (inList ?ELEMENT (ListFn @ROW)) (instance ?ELEMENT Number))) |
Merge.kif 4849-4854 |
|
(=> (equal ?LIST1 ?LIST2) (=> (and (equal ?LIST1 (ListFn @ROW1)) (equal ?LIST2 (ListFn @ROW2))) (forall (?NUMBER) (equal (ListOrderFn (ListFn @ROW1) ?NUMBER) (ListOrderFn (ListFn @ROW2) ?NUMBER))))) |
Merge.kif 293-300 |
|
(=> (exactCardinality ?REL ?ARG ?COUNT) (equal (CardinalityFn (KappaFn ?EL (and (?REL @ARGS) (equal ?EL (ListOrderFn (ListFn @ARGS) ?ARG))))) ?COUNT)) |
Media.kif 2119-2127 |
|
(=> (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 |
|
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 2971-2974 | 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 2976-2980 | 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 3250-3251 | For all @ROW and another entity (@ROW) starts (@ROW and the other entity) |
![]() |
![]() |