lie4 xu4 han2 shu4 (ListOrderFn)

(ListOrderFn list number) denotes the item that is in the number position in the List list. For example, (ListOrderFn (ListFn Monday Tuesday Wednesday) 2) would return the value Tuesday.

Ontology

SUMO / BASE-ONTOLOGY

Class(es)

zhong3 lei4

ke3 ji4 cheng2 guan1 xi4

er4 yuan2 han2 shu4

lie4 xu4 han2 shu4

Coordinate term(s)

jia1 fa3 han2 shu4 ri4 han2 shu4 mi4 du4 han2 shu4 chu2 fa3 han2 shu4 wen2 ben3 ban3 ben3 han2 shu4 zhi3 shu4 han2 shu4 tu2 lu4 jing4 han2 shu4 xiao3 shi2 han2 shu4 jiao1 ji2 han2 shu4 jian1 ge2 han2 shu4 zhong3 lei4 miao2 shu4 han2 shu4 lie4 jie2 han2 shu4 dui4 shu4 han2 shu4 zui4 da4 zhi2 han2 shu4 zui4 da4 liang4 lu4 jing4 han2 shu4 ce4 liang4 han2 shu4 bu4 fen5 zheng3 ti1 cha4 yi4 han2 shu4 bu4 fen5 zheng3 ti1 jiao1 ji2 han2 shu4 bu4 fen5 zheng3 ti1 jia1 zong1 han2 shu4 zui4 xiao3 zhi2 han2 shu4 zui4 xiao3 liang4 lu4 jing4 han2 shu4 fen1 zhong1 han2 shu4 yue4 fen4 han2 shu4 cheng2 fa3 han2 shu4 qi1 kan1 yi1 qi1 han2 shu4 zhou1 qi1 xing4 shi2 ju4 han2 shu4 guan1 xi4 hu4 bu3 han2 shu4 xiang4 dui4 shi2 jian1 han2 shu4 yu2 shu4 han2 shu4 miao3 zhong1 han2 shu4 xi4 lie4 yi1 juan4 han2 shu4 su4 du4 han2 shu4 jian3 fa3 han2 shu4 shi2 jian1 dan1 wei4 han2 shu4 shi2 jian1 li4 cheng2 han2 shu4 lian2 ji2 han2 shu4 wei4 zhi4 han2 shu4

Type restrictions

shi2 ti3 ListOrderFn(xu4 lie4, zheng4 zheng3 shu4)

Related WordNet synsets

See more related synsets on a separate page.

Axioms (16)

if obj1 deng3 yu1 obj2,
then if obj1 deng3 yu1 ""()" de5 di4 er4 yuan2 su4" and obj2 deng3 yu1 ""()" de5 di4 er4 yuan2 su4" and "()" deng3 yu1 "()", then () (bu2) cheng2 li4s if and only if () (bu2) cheng2 li4s

(=>
      (equal ?OBJ1 ?OBJ2)
      (=>
            (and
                  (equal
                        ?OBJ1
                        (ListOrderFn
                              (ListFn @ROW1)
                              ?NUMBER))
                  (equal
                        ?OBJ2
                        (ListOrderFn
                              (ListFn @ROW2)
                              ?NUMBER))
                  (equal
                        (ListFn @ROW1)
                        (ListFn @ROW2)))
            (<=>
                  (holds @ROW1)
                  (holds @ROW2))))

if list1 deng3 yu1 list2,
then if list1 deng3 yu1 "()" and list2 deng3 yu1 "()", then for all number holds: ""()" de5 di4 er4 yuan2 su4" deng3 yu1 ""()" de5 di4 er4 yuan2 su4"

(=>
      (equal ?LIST1 ?LIST2)
      (=>
            (and
                  (equal
                        ?LIST1
                        (ListFn @ROW1))
                  (equal
                        ?LIST2
                        (ListFn @ROW2)))
            (forall
                  (?NUMBER)
                  (equal
                        (ListOrderFn
                              (ListFn @ROW1)
                              ?NUMBER)
                        (ListOrderFn
                              (ListFn @ROW2)
                              ?NUMBER)))))

if dui4 li4 yu1 ?,
then for all attr1,attr2 holds:
- if attr1 deng3 yu1 ""()" de5 di4 er4 yuan2 su4" and attr2 deng3 yu1 ""()" de5 di4 er4 yuan2 su4" and number1 deng3 yu1 number2,
- then if obj you3 shu3 xing4 attr1, then obj you3 shu3 xing4 attr2

(=>
      (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))))))

rel shi4 quan2 zhi2 guan1 xi4 de5 shi2 li4 if and only if there exists valence so_that_not rel shi4 guan1 xi4 de5 shi2 li4 and rel %&有論元(s) valence and

if for all number,element,class holds: if number xiao3 yu1 valence and rel de5 lun4 yuan2 number shi4 class de5 shi2 li4 and element deng3 yu1 ""()" de5 di4 er4 yuan2 su4", then element shi4 class de5 shi2 li4,
then there exists item so_that_not rel(,item) (bu2) cheng2 li4s

(<=>
      (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)
                              (holds ?REL @ROW ?ITEM))))))

if list shi4 xu4 lie4 de5 shi2 li4,
then there exists number1 so_that_not there exists item1 so_that_not "list de5 di4 er4 yuan2 su4" deng3 yu1 item1 and for all number2 holds: if number2 shi4 zheng4 zheng3 shu4 de5 shi2 li4 and number2 xiao3 yu1 number1, then there exists item2 so_that_not "list de5 di4 er4 yuan2 su4" deng3 yu1 item2

(=>
      (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))))))))

list shi4 wei2 yi1 xu4 lie4 de5 shi2 li4 if and only if for all number1,number2 holds: if "list de5 di4 er4 yuan2 su4" deng3 yu1 "list de5 di4 er4 yuan2 su4", then number1 deng3 yu1 number2.

(<=>
      (instance ?LIST UniqueList)
      (forall
            (?NUMBER1 ?NUMBER2)
            (=>
                  (equal
                        (ListOrderFn ?LIST ?NUMBER1)
                        (ListOrderFn ?LIST ?NUMBER2))
                  (equal ?NUMBER1 ?NUMBER2))))

If list1 shi4 xu4 lie4 de5 shi2 li4 and list2 shi4 xu4 lie4 de5 shi2 li4 and for all number holds: "list1 de5 di4 er4 yuan2 su4" deng3 yu1 "list2 de5 di4 er4 yuan2 su4", then list1 deng3 yu1 list2.

(=>
      (and
            (instance ?LIST1 List)
            (instance ?LIST2 List)
            (forall
                  (?NUMBER)
                  (equal
                        (ListOrderFn ?LIST1 ?NUMBER)
                        (ListOrderFn ?LIST2 ?NUMBER))))
      (equal ?LIST1 ?LIST2))

If rel de5 lun4 yuan2 number shi4 class de5 shi2 li4 and rel() (bu2) cheng2 li4s, then ""()" de5 di4 er4 yuan2 su4" shi4 class de5 shi2 li4.

(=>
      (and
            (domain ?REL ?NUMBER ?CLASS)
            (holds ?REL @ROW))
      (instance
            (ListOrderFn
                  (ListFn @ROW)
                  ?NUMBER)
            ?CLASS))

If rel de5 lun4 yuan2 number shi4 class de5 ci4 zhong3 lei4 and rel() (bu2) cheng2 li4s, then ""()" de5 di4 er4 yuan2 su4" shi4 class de5 ci4 zhong3 lei4.

(=>
      (and
            (domainSubclass ?REL ?NUMBER ?CLASS)
            (holds ?REL @ROW))
      (subclass
            (ListOrderFn
                  (ListFn @ROW)
                  ?NUMBER)
            ?CLASS))

If "list de5 chang2 du4" deng3 yu1 number1, then for all number2 holds: there exists item so_that_not "list de5 di4 er4 yuan2 su4" deng3 yu1 item if and only if number2 小於或等於 number1.

(=>
      (equal
            (ListLengthFn ?LIST)
            ?NUMBER1)
      (forall
            (?NUMBER2)
            (<=>
                  (exists
                        (?ITEM)
                        (equal
                              (ListOrderFn ?LIST ?NUMBER2)
                              ?ITEM))
                  (lessThanOrEqualTo ?NUMBER2 ?NUMBER1))))

""(,item)" de5 di4 er4 yuan2 su4" deng3 yu1 item.

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

If "list1 de5 chang2 du4" deng3 yu1 number, then there exists list2 so_that_not list1 (mei2chu1 shi3 hua4not(s) list2 and "(number+1)" deng3 yu1 "list2 de5 chang2 du4" and "list2 de5 di4 er4 yuan2 su4" deng3 yu1 item.

(=>
      (equal
            (ListLengthFn ?LIST1)
            ?NUMBER)
      (exists
            (?LIST2)
            (and
                  (initialList ?LIST1 ?LIST2)
                  (equal
                        (SuccessorFn ?NUMBER)
                        (ListLengthFn ?LIST2))
                  (equal
                        (ListOrderFn
                              ?LIST2
                              (SuccessorFn ?NUMBER))
                        ?ITEM))))

list3 deng3 yu1 "list1 he2 list2 zu3 cheng2 de5 xu4 lie4" if and only if for all number1,number2 holds: if number1 小於或等於 "list1 de5 chang2 du4" and number2 小於或等於 "list2 de5 chang2 du4" and number1 shi4 zheng4 zheng3 shu4 de5 shi2 li4 and number2 shi4 zheng4 zheng3 shu4 de5 shi2 li4, then "list3 de5 di4 er4 yuan2 su4" deng3 yu1 "list1 de5 di4 er4 yuan2 su4" and "list3 de5 di4 er4 yuan2 su4" deng3 yu1 "list2 de5 di4 er4 yuan2 su4".

(<=>
      (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))))))

item shi4 list de5 yi1 cheng2 yuan2 if and only if there exists number so_that_not "list de5 di4 er4 yuan2 su4" deng3 yu1 item.

(<=>
      (inList ?ITEM ?LIST)
      (exists
            (?NUMBER)
            (equal
                  (ListOrderFn ?LIST ?NUMBER)
                  ?ITEM)))

if list1 shi4 list2 de5 ci4 xu4 lie4,
then there exists number3 so_that_not for all item holds: if item shi4 list1 de5 yi1 cheng2 yuan2, then there exist number1,number2 so_that_not "list1 de5 di4 er4 yuan2 su4" deng3 yu1 item and "list2 de5 di4 er4 yuan2 su4" deng3 yu1 item and number2 deng3 yu1 "(number1+number3)"

(=>
      (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))))))))

if list1 (mei2chu1 shi3 hua4not(s) list2,
then for all number1,number2 holds: if "list1 de5 chang2 du4" deng3 yu1 number1 and number2 小於或等於 number1, then "list1 de5 di4 er4 yuan2 su4" deng3 yu1 "list2 de5 di4 er4 yuan2 su4"

(=>
      (initialList ?LIST1 ?LIST2)
      (forall
            (?NUMBER1 ?NUMBER2)
            (=>
                  (and
                        (equal
                              (ListLengthFn ?LIST1)
                              ?NUMBER1)
                        (lessThanOrEqualTo ?NUMBER2 ?NUMBER1))
                  (equal
                        (ListOrderFn ?LIST1 ?NUMBER2)
                        (ListOrderFn ?LIST2 ?NUMBER2)))))