Knowledge base Browser

appearance as argument number 1

(documentation ListOrderFn EnglishLanguage "(list order ?LIST ?NUMBER) denotes the item that is in the ?NUMBER position in the list ?LIST. For example, (list order (list Monday Tuesday Wednesday) 2) would return the value Tuesday.")	Merge.kif 2421-2424
(domain ListOrderFn 1 List)	Merge.kif 2418-2418	The number 1 argument of list order is an instance of list
(domain ListOrderFn 2 PositiveInteger)	Merge.kif 2419-2419	The number 2 argument of list order is an instance of positive integer
(instance ListOrderFn BinaryFunction)	Merge.kif 2416-2416	List order is an instance of binary function
(instance ListOrderFn PartialValuedRelation)	Merge.kif 2417-2417	List order is an instance of partial valued relation
(range ListOrderFn Entity)	Merge.kif 2420-2420	The range of list order is an instance of entity

appearance as argument number 2

(format EnglishLanguage ListOrderFn "%2th element of %1")	english_format.kif 148-148
(termFormat EnglishLanguage ListOrderFn "list order")	domainEnglishFormat.kif 5578-5578	term format english language, list order and "list order"

antecedent

(=> (and (exactCardinality ?REL ?ARG 1) (?REL @ARGS) (equal ?X (ListOrderFn (ListFn @ARGS) ?ARG)) (equal ?Y (ListOrderFn (ListFn @ARGS) ?ARG))) (equal ?X ?Y))	Media.kif 1854-1860	If exactCardinality a relation, a positive integer and 1 and relation @ARGS and entity is equal to positive integerth element of (@ARGS) and a entity is equal to positive integerth element of (@ARGS) then entity is equal to entity
(=> (and (exactCardinality ?REL ?ARG 1) (?REL @ARGS) (equal ?X (ListOrderFn (ListFn @ARGS) ?ARG))) (not (exists (?Y) (and (equal ?Y (ListOrderFn (ListFn @ARGS) ?ARG)) (not (equal ?X ?Y))))))	Media.kif 1842-1851	If exactCardinality a relation, a positive integer and 1 and relation @ARGS and entity is equal to positive integerth element of (@ARGS) then there doesn't exist a entity so that entity is equal to positive integerth element of (@ARGS) and entity is not equal to entity
(=> (and (instance (LatitudeFn ?DIRECTION @ROW) Region) (equal (ListOrderFn (ListFn @ROW) 1) (MeasureFn ?NUM AngularDegree))) (lessThanOrEqualTo ?NUM 90))	Geography.kif 427-431	If latitude a directional attribute and @ROW is an instance of region and 1th element of (@ROW) is equal to a real number angular degree(s) then real number is less than or equal to 90
(=> (and (instance (LongitudeFn ?DIRECTION @ROW) Region) (equal (ListOrderFn (ListFn @ROW) 1) (MeasureFn ?NUM AngularDegree))) (lessThanOrEqualTo ?NUM 180))	Geography.kif 467-471	If longitude a directional attribute and @ROW is an instance of region and 1th element of (@ROW) is equal to a real number angular degree(s) then real number is less than or equal to 180
(=> (and (instance ?LIST1 List) (instance ?LIST2 List) (forall (?NUMBER) (equal (ListOrderFn ?LIST1 ?NUMBER) (ListOrderFn ?LIST2 ?NUMBER)))) (equal ?LIST1 ?LIST2))	Merge.kif 2426-2432	If a list is an instance of list and list is an instance of list and for all a positive integer positive integerth element of list is equal to positive integerth element of list then list is equal to list
(=> (and (processList @ROW) (inList ?Process1 (ListFn @ROW)) (inList ?Process2 (ListFn @ROW)) (equal (ListOrderFn (ListFn @ROW) ?Number1) ?Process1) (equal (ListOrderFn (ListFn @ROW) ?Number2) ?Process2) (lessThan ?Number1 ?Number2)) (earlier (WhenFn ?Process1) (WhenFn ?Process2)))	QoSontology.kif 597-605	If process list @ROW and a physical is a member of (@ROW) and physical is a member of (@ROW) and a positive integerth element of (@ROW) is equal to physical and positive integerth element of (@ROW) is equal to physical and positive integer is less than positive integer then the time of existence of physical happens earlier than the time of existence of physical

consequent

(<=> (average ?LIST1 ?AVERAGE) (exists (?LIST2) (and (equal (ListLengthFn ?LIST2) (ListLengthFn ?LIST1)) (equal (ListOrderFn ?LIST2 1) (ListOrderFn ?LIST1 1)) (forall (?ITEMFROM2) (=> (inList ?ITEMFROM2 ?LIST2) (exists (?POSITION ?POSITIONMINUSONE ?ITEMFROM1 ?PRIORFROM2) (and (greaterThan ?POSITION 1) (lessThanOrEqualTo ?POSITION (ListLengthFn ?LIST2)) (equal (ListOrderFn ?LIST2 ?ITEMFROM2) ?POSITION) (inList ?ITEMFROM1 ?LIST1) (equal ?POSITION (ListOrderFn ?LIST1 ?ITEMFROM1)) (inList ?PRIORFROM2 ?LIST2) (equal ?POSITIONMINUSONE (SubtractionFn ?POSITION 1)) (equal ?POSITIONMINUSONE (ListOrderFn ?LIST2 ?PRIORFROM2)) (equal ?ITEMFROM2 (AdditionFn ?ITEMFROM1 ?PRIORFROM2)))))) (equal ?LASTPLACE (ListLengthFn ?LIST2)) (equal ?AVERAGE (DivisionFn (ListOrderFn ?LIST2 ?LASTPLACE) ?LASTPLACE)))))	People.kif 286-307	A real number is an average of a list if and only if there exists list so that length of list is equal to length of list and 1th element of list is equal to 1th element of list and for all a positive integer if positive integer is a member of list then there exist a quantity quantityMINUSONE, positive integer and and a positive integer so that quantity is greater than 1 and quantity is less than or equal to length of list and positive integerth element of list is equal to quantity and positive integer is a member of list and quantity is equal to positive integerth element of list and positive integer is a member of list and quantityMINUSONE is equal to ( quantity and 1) and quantityMINUSONE is equal to positive integerth element of list and positive integer is equal to ( positive integer and positive integer) and a positive integer is equal to length of list and real number is equal to positive integerth element of list and positive integer
(<=> (equal (LastFn ?LIST) ?ITEM) (exists (?NUMBER) (and (equal (ListLengthFn ?LIST) ?NUMBER) (equal (ListOrderFn ?LIST ?NUMBER) ?ITEM))))	Mid-level-ontology.kif 4061-4066	The last of a list is equal to an entity if and only if there exists a positive integer so that length of list is equal to positive integer and positive integerth element of list is equal to entity
(<=> (equal ?LIST3 (ListConcatenateFn ?LIST1 ?LIST2)) (forall (?NUMBER1 ?NUMBER2) (=> (and (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 2511-2522	A list is equal to the list composed of list and a list if and only if for all a positive integer and positive integer if positive integer is less than or equal to length of list and positive integer is less than or equal to length of list and positive integer is an instance of positive integer and positive integer is an instance of positive integer then positive integerth element of list is equal to positive integerth element of list and (length of list and positive integer)th element of list is equal to positive integerth element of list
(<=> (instance ?REL TotalValuedRelation) (exists (?VALENCE) (and (instance ?REL Relation) (valence ?REL ?VALENCE) (=> (forall (?NUMBER ?ELEMENT ?CLASS) (=> (and (lessThan ?NUMBER ?VALENCE) (domain ?REL ?NUMBER ?CLASS) (equal ?ELEMENT (ListOrderFn (ListFn @ROW) ?NUMBER))) (instance ?ELEMENT ?CLASS))) (exists (?ITEM) (?REL @ROW ?ITEM))))))	Merge.kif 1776-1791	A relation is an instance of total valued relation if and only if there exists a positive integer so that relation is an instance of relation and relation %&has positive integer argument(s) and if for all positive integer an entity and and a set or class if positive integer is less than positive integer and the number positive integer argument of relation is an instance of set or class and entity is equal to positive integerth element of (@ROW) then entity is an instance of set or class then there exists a entity so that relation @ROW and entity
(=> (and (domain ?REL ?NUMBER ?CLASS) (?REL @ROW)) (instance (ListOrderFn (ListFn @ROW) ?NUMBER) ?CLASS))	Merge.kif 2434-2438	If the number a positive integer argument of a relation is an instance of a set or class and relation @ROW then positive integerth element of (@ROW) is an instance of set or class
(=> (and (domainSubclass ?REL ?NUMBER ?CLASS) (?REL @ROW)) (subclass (ListOrderFn (ListFn @ROW) ?NUMBER) ?CLASS))	Merge.kif 2440-2444	If the number a positive integer argument of a relation is a subclass of a set or class and relation @ROW then positive integerth element of (@ROW) is a subclass of set or class
(=> (and (equal (ListLengthFn ?LIST) ?NUMBER1) (instance ?LIST List) (not (equal ?LIST NullList)) (instance ?NUMBER1 PositiveInteger)) (forall (?NUMBER2) (<=> (exists (?ITEM) (and (equal (ListOrderFn ?LIST ?NUMBER2) ?ITEM) (inList ?ITEM ?LIST))) (lessThanOrEqualTo ?NUMBER2 ?NUMBER1))))	Merge.kif 2455-2468	If length of a list is equal to a nonnegative integer and list is an instance of list and list is not equal to null list and nonnegative integer is an instance of positive integer then for all a positive integer there exists an entity so that positive integerth element of list is equal to entity and entity is a member of list if and only if positive integer is less than or equal to nonnegative integer
(=> (and (equal (ListLengthFn ?LIST1) ?NUMBER) (instance ?LIST List) (not (equal ?LIST NullList)) (instance ?NUMBER1 PositiveInteger)) (exists (?LIST2 ?ITEM) (and (initialList ?LIST1 ?LIST2) (equal (SuccessorFn ?NUMBER) (ListLengthFn ?LIST2)) (equal (ListOrderFn ?LIST2 (SuccessorFn ?NUMBER)) ?ITEM))))	Merge.kif 2488-2499	If length of a list is equal to a nonnegative integer and list is an instance of list and list is not equal to null list and nonnegative integer1 is an instance of positive integer then there exist list2 and entity so that list starts list2 and ( nonnegative integer+1) is equal to length of list2 and ( nonnegative integer+1)th element of list2 is equal to entity
(=> (and (exactCardinality ?REL ?ARG 1) (?REL @ARGS) (equal ?X (ListOrderFn (ListFn @ARGS) ?ARG))) (not (exists (?Y) (and (equal ?Y (ListOrderFn (ListFn @ARGS) ?ARG)) (not (equal ?X ?Y))))))	Media.kif 1842-1851	If exactCardinality a relation, a positive integer and 1 and relation @ARGS and entity is equal to positive integerth element of (@ARGS) then there doesn't exist a entity so that entity is equal to positive integerth element of (@ARGS) and entity is not equal to entity
(=> (and (instance ?LIST List) (not (equal ?LIST NullList))) (equal (FirstFn ?LIST) (ListOrderFn ?LIST 1)))	Mid-level-ontology.kif 4075-4080	If a list is an instance of list and list is not equal to null list then the first of list is equal to 1th element of list
(=> (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 447-457	If @ROW is opposed to then for all an attribute and attribute if attribute is equal to a positive integerth element of (@ROW) and attribute is equal to positive integerth element of (@ROW) and positive integer is not equal to positive integer then if entity has an attribute attribute then entity has not an attribute attribute
(=> (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 282-289	If a list is equal to list then if list is equal to (@ROW1) and list is equal to (@ROW2) then for all a positive integer positive integerth element of (@ROW1) is equal to positive integerth element of (@ROW2)
(=> (exactCardinality ?REL ?ARG 1) (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 1826-1839	If exactCardinality a relation, a positive integer and 1 then there exist an entity and @ARGS so that relation @ARGS and entity is equal to positive integerth element of (@ARGS) and there doesn't exist a entity so that entity is equal to positive integerth element of (@ARGS) and entity is not equal to entity
(=> (exactCardinality ?REL ?ARG ?COUNT) (equal (CardinalityFn (KappaFn ?EL (and (?REL @ARGS) (equal ?EL (ListOrderFn (ListFn @ARGS) ?ARG))))) ?COUNT))	Media.kif 1868-1876	If exactCardinality a relation, a positive integer and an integer then the number of instances in the class described by ?EL is equal to integer
(=> (exactCardinality ?REL ?ARG ?COUNT) (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 1879-1890	If exactCardinality a relation, a positive integer and an integer then there exists a set or class so that set or class is an instance of set or class and if relation @ARGS and entity is equal to positive integerth element of (@ARGS) then entity is an instance of set or class and the number of instances in set or class is equal to integer
(=> (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 484-496	If exhaustive attribute a attribute and @ROW then there doesn't exist an entity so that entity is an instance of a attribute and there don't exist entity and a positive integer so that entity is equal to entity and entity is equal to positive integerth element of (@ROW)
(=> (inList ?ITEM ?LIST) (exists (?NUMBER) (equal (ListOrderFn ?LIST ?NUMBER) ?ITEM)))	Merge.kif 2533-2536	If an entity is a member of a list then there exists a positive integer so that positive integerth element of list is equal to entity
(=> (initialList ?LIST1 ?LIST2) (forall (?NUMBER1 ?NUMBER2) (=> (and (equal (ListLengthFn ?LIST1) ?NUMBER1) (lessThanOrEqualTo ?NUMBER2 ?NUMBER1)) (equal (ListOrderFn ?LIST1 ?NUMBER2) (ListOrderFn ?LIST2 ?NUMBER2)))))	Merge.kif 2577-2584	If a list starts list then for all a nonnegative integer and a positive integer if length of list is equal to nonnegative integer and positive integer is less than or equal to nonnegative integer then positive integerth element of list is equal to positive integerth element of list
(=> (instance ?LIST List) (exists (?NUMBER1) (exists (?ITEM1) (and (not (equal (ListOrderFn ?LIST ?NUMBER1) ?ITEM1)) (forall (?NUMBER2) (=> (and (instance ?NUMBER2 PositiveInteger) (lessThan ?NUMBER2 ?NUMBER1)) (exists (?ITEM2) (equal (ListOrderFn ?LIST ?NUMBER2) ?ITEM2))))))))	Merge.kif 2341-2353	If a list is an instance of list then there exists a positive integer so that there exists an entity so that positive integerth element of list is not equal to entity and for all positive integer if positive integer is an instance of positive integer and positive integer is less than positive integer then there exists entity so that positive integerth element of list is equal to entity
(=> (instance ?LIST UniqueList) (forall (?NUMBER1 ?NUMBER2) (=> (equal (ListOrderFn ?LIST ?NUMBER1) (ListOrderFn ?LIST ?NUMBER2)) (equal ?NUMBER1 ?NUMBER2))))	Merge.kif 2361-2366	If a list is an instance of unique list then for all a positive integer and positive integer if positive integerth element of list is equal to positive integerth element of list then positive integer is equal to positive integer
(=> (maxCardinality ?REL ?ARG ?COUNT) (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 1946-1957	If maxCardinality a relation, a positive integer and an integer then there exists a set or class so that set or class is an instance of set or class and if relation @ARGS and entity is equal to positive integerth element of (@ARGS) then entity is an instance of set or class and the number of instances in set or class is less than or equal to integer
(=> (maxCardinality ?REL ?ARG ?COUNT) (lessThanOrEqualTo (CardinalityFn (KappaFn ?EL (and (?REL @ARGS) (equal ?EL (ListOrderFn (ListFn @ARGS) ?ARG))))) ?COUNT))	Media.kif 1935-1943	If maxCardinality a relation, a positive integer and an integer then the number of instances in the class described by ?EL is less than or equal to integer
(=> (minCardinality ?REL ?ARG ?COUNT) (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 1913-1924	If minCardinality a relation, a positive integer and an integer then there exists a set or class so that set or class is an instance of set or class and if relation @ARGS and entity is equal to positive integerth element of (@ARGS) then entity is an instance of set or class and the number of instances in set or class is greater than or equal to integer
(=> (minCardinality ?REL ?ARG ?COUNT) (greaterThanOrEqualTo (CardinalityFn (KappaFn ?EL (and (?REL @ARGS) (equal ?EL (ListOrderFn (ListFn @ARGS) ?ARG))))) ?COUNT))	Media.kif 1901-1909	If minCardinality a relation, a positive integer and an integer then the number of instances in the class described by ?EL is greater than or equal to integer
(=> (subList ?LIST1 ?LIST2) (exists (?NUMBER3) (forall (?ITEM) (=> (inList ?ITEM ?LIST1) (exists (?NUMBER1 ?NUMBER2) (and (equal (ListOrderFn ?LIST1 ?NUMBER1) ?ITEM) (equal (ListOrderFn ?LIST2 ?NUMBER2) ?ITEM) (equal ?NUMBER2 (AdditionFn ?NUMBER1 ?NUMBER3))))))))	Merge.kif 2557-2567	If a list is a sublist of list then there exists a quantity so that for all an entity if entity is a member of list then there exist a positive integer and positive integer so that positive integerth element of list is equal to entity and positive integerth element of list is equal to entity and positive integer is equal to ( positive integer and quantity)

Display limited to 25 items. Show next 25

statement

(forall (@ROW ?ITEM)
    (equal
        (ListOrderFn
            (ListFn @ROW ?ITEM)
            (ListLengthFn
                (ListFn @ROW ?ITEM))) ?ITEM))

Merge.kif 2475-2479

For all @ROW and entity length of (@ROW and entity)th element of (@ROW and entity) is equal to entity

Show full definition with tree view
Show simplified definition (without tree view)
Show simplified definition (with tree view)

Sigma web home SUMO web home
Sigma version 2.8b (2010/03/15) is open source software produced by Articulate Software and its partners

KB Term:

English Word: