Zvolte jazyk: english | cesky | deutsch | italiano | simplified chinese | traditional chinese | hindi Koncept: Anglické slovo: Hlavní stránka

# list order fn (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.

## Ontologie

SUMO / BASE-ONTOLOGY

## Class(es)

 třída

inheritable relation

binární funkce

list order fn

## Související termín(y)

addition fn  day fn  density fn  division fn  edition fn  exponentiation fn  graph path fn  hour fn  intersection fn  interval fn  kappa fn  list concatenate fn  log fn  max fn  maximal weighted path fn  measure fn  mereological difference fn  mereological product fn  mereological sum fn  min fn  minimal weighted path fn  minute fn  month fn  multiplication fn  periodical issue fn  recurrent time interval fn  relative complement fn  relative time fn  remainder fn  second fn  series volume fn  speed fn  subtraction fn  temporal composition fn  time interval fn  union fn  where fn

## Related WordNet synsets

See more related synsets on a separate page.

## Axiomy (16)

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

• jestliže list1 se rovná list2,
• potom jestliže list1 se rovná "()" a list2 se rovná "()", potom pro všechny number platí: "numberth element of "()"" se rovná "numberth element of "()""
• .
```(=>
(equal ?LIST1 ?LIST2)
(=>
(and
(equal
?LIST1
(ListFn @ROW1))
(equal
?LIST2
(ListFn @ROW2)))
(forall
(?NUMBER)
(equal
(ListOrderFn
(ListFn @ROW1)
?NUMBER)
(ListOrderFn
(ListFn @ROW2)
?NUMBER)))))```

```(=>
(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 je instancí třídy úplná relace tehdy a jen tehdy pokud existuje valence tak, že rel je instancí třídy relace a rel has valence argument(s) a
• jestliže pro všechny number,element,class platí: jestliže number je menší než valence a numberth argument of rel je an instance of class a element se rovná "numberth element of "()"", potom element je instancí třídy class,
• potom existuje item tak, že rel(,item) holds
• .
```(<=>
(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))))))```

```(=>
(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 je instancí třídy seznam bez duplicit tehdy a jen tehdy pokud pro všechny number1,number2 platí: jestliže "number1th element of list" se rovná "number2th element of list", potom number1 se rovná number2.
```(<=>
(instance ?LIST UniqueList)
(forall
(?NUMBER1 ?NUMBER2)
(=>
(equal
(ListOrderFn ?LIST ?NUMBER1)
(ListOrderFn ?LIST ?NUMBER2))
(equal ?NUMBER1 ?NUMBER2))))```

Jestliže list1 je instancí třídy seznam a list2 je instancí třídy seznam a pro všechny number platí: "numberth element of list1" se rovná "numberth element of list2", potom list1 se rovná list2.
```(=>
(and
(instance ?LIST1 List)
(instance ?LIST2 List)
(forall
(?NUMBER)
(equal
(ListOrderFn ?LIST1 ?NUMBER)
(ListOrderFn ?LIST2 ?NUMBER))))
(equal ?LIST1 ?LIST2))```

Jestliže numberth argument of rel je an instance of class a rel() holds, potom "numberth element of "()"" je instancí třídy class.
```(=>
(and
(domain ?REL ?NUMBER ?CLASS)
(holds ?REL @ROW))
(instance
(ListOrderFn
(ListFn @ROW)
?NUMBER)
?CLASS))```

Jestliže numberth argument of rel je a subclass of class a rel() holds, potom "numberth element of "()"" je podtřídou class.
```(=>
(and
(domainSubclass ?REL ?NUMBER ?CLASS)
(holds ?REL @ROW))
(subclass
(ListOrderFn
(ListFn @ROW)
?NUMBER)
?CLASS))```

Jestliže "length of list" se rovná number1, potom pro všechny number2 platí: existuje item tak, že "number2th element of list" se rovná item tehdy a jen tehdy pokud number2 je menší než nebo roven number1.
```(=>
(equal
(ListLengthFn ?LIST)
?NUMBER1)
(forall
(?NUMBER2)
(<=>
(exists
(?ITEM)
(equal
(ListOrderFn ?LIST ?NUMBER2)
?ITEM))
(lessThanOrEqualTo ?NUMBER2 ?NUMBER1))))```

""length of "(,item)""th element of "(,item)"" se rovná item.
```(equal
(ListOrderFn
(ListFn @ROW ?ITEM)
(ListLengthFn
(ListFn @ROW ?ITEM)))
?ITEM)```

Jestliže "length of list1" se rovná number, potom existuje list2 tak, že list1 starts list2 a "(number+1)" se rovná "length of list2" a ""(number+1)"th element of list2" se rovná item.
```(=>
(equal
(ListLengthFn ?LIST1)
?NUMBER)
(exists
(?LIST2)
(and
(initialList ?LIST1 ?LIST2)
(equal
(SuccessorFn ?NUMBER)
(ListLengthFn ?LIST2))
(equal
(ListOrderFn
?LIST2
(SuccessorFn ?NUMBER))
?ITEM))))```

list3 se rovná "list concatenate fn(list1,list2)" tehdy a jen tehdy pokud pro všechny number1,number2 platí: jestliže number1 je menší než nebo roven "length of list1" a number2 je menší než nebo roven "length of list2" a number1 je instancí třídy kladné celé číslo a number2 je instancí třídy kladné celé číslo, potom "number1th element of list3" se rovná "number1th element of list1" a ""("length of list1"+number2)"th element of list3" se rovná "number2th element of list2".
```(<=>
(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
(ListLengthFn ?LIST1)
?NUMBER2))
(ListOrderFn ?LIST2 ?NUMBER2))))))```

item je a member of list tehdy a jen tehdy pokud existuje number tak, že "numberth element of list" se rovná item.
```(<=>
(inList ?ITEM ?LIST)
(exists
(?NUMBER)
(equal
(ListOrderFn ?LIST ?NUMBER)
?ITEM)))```

• jestliže list1 je a sublist of list2,
• potom existuje number3 tak, že pro všechny item platí: jestliže item je a member of list1, potom existují number1,number2 tak, že "number1th element of list1" se rovná item a "number2th element of list2" se rovná item a number2 se rovná "(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

• jestliže list1 starts list2,
• potom pro všechny number1,number2 platí: jestliže "length of list1" se rovná number1 a number2 je menší než nebo roven number1, potom "number2th element of list1" se rovná "number2th element of list2"
• .
```(=>
(initialList ?LIST1 ?LIST2)
(forall
(?NUMBER1 ?NUMBER2)
(=>
(and
(equal
(ListLengthFn ?LIST1)
?NUMBER1)
(lessThanOrEqualTo ?NUMBER2 ?NUMBER1))
(equal
(ListOrderFn ?LIST1 ?NUMBER2)
(ListOrderFn ?LIST2 ?NUMBER2)))))```