Select language: english | cesky | deutsch | italiano | simplified chinese | traditional chinese | hindi Concept: English word: Home

# list fn (ListFn)

A Function that takes any number of arguments and returns the List containing those arguments in exactly the same order.

## Ontology

SUMO / BASE-ONTOLOGY

## Class(es)

 class

inheritable relation

function
 variable arity relation

list fn

## Coordinate term(s)

assignment fn  greatest common divisor fn  least common multiple fn  contrary attribute  disjoint decomposition  disjoint relation  exhaustive attribute  exhaustive decomposition  holds  partition

## Axioms (27)

```(=>
(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 is equal to list2,
• then if list1 is equal to "()" and list2 is equal to "()", then for all number holds: "numberth element of "()"" is equal to "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)))))```

If and ? are disjoint and rel is a member of "()", then rel is an instance of relation.
```(=>
(and
(disjointRelation @ROW)
(inList
?REL
(ListFn @ROW)))
(instance ?REL Relation))```

If and ? are disjoint and rel1 is a member of "()" and rel2 is a member of "()" and rel1 %&has number argument(s), then rel2 %&has number argument(s).
```(=>
(and
(disjointRelation @ROW)
(inList
?REL1
(ListFn @ROW))
(inList
?REL2
(ListFn @ROW))
(valence ?REL1 ?NUMBER))
(valence ?REL2 ?NUMBER))```

If and ? are disjoint and rel1 is a member of "()" and rel2 is a member of "()" and rel1 is not equal to rel2 and rel1() holds, then rel2() doesn't hold.
```(=>
(and
(disjointRelation @ROW1)
(inList
?REL1
(ListFn @ROW1))
(inList
?REL2
(ListFn @ROW1))
(not
(equal ?REL1 ?REL2))
(holds ?REL1 @ROW2))
(not
(holds ?REL2 @ROW2)))```

```(=>
(contraryAttribute @ROW)
(=>
(inList
?ELEMENT
(ListFn @ROW))
(instance ?ELEMENT Attribute)))```

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

```(=>
(exhaustiveAttribute ?CLASS @ROW)
(=>
(inList
?ATTR
(ListFn @ROW))
(instance ?ATTR Attribute)))```

```(=>
(exhaustiveAttribute ?CLASS @ROW)
(forall
(?OBJ)
(=>
(instance ?ATTR1 ?CLASS)
(exists
(?ATTR2)
(and
(inList
?ATTR2
(ListFn @ROW))
(equal ?ATTR1 ?ATTR2))))))```

```(=>
(exhaustiveDecomposition @ROW)
(=>
(inList
?ELEMENT
(ListFn @ROW))
(instance ?ELEMENT Class)))```

```(=>
(disjointDecomposition @ROW)
(=>
(inList
?ELEMENT
(ListFn @ROW))
(instance ?ELEMENT Class)))```

rel is an instance of total valued relation if and only if there exists valence so that rel is an instance of relation and rel %&has valence argument(s) and
• if for all number,element,class holds: if number is less than valence and the number number argument of rel is an instance of class and element is equal to "numberth element of "()"", then element is an instance of class,
• then there exists item so that 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))))))```

If rel is an instance of intentional relation and rel(agent,) holds and obj is a member of "()", then agent is interested in obj.
```(=>
(and
(instance ?REL IntentionalRelation)
(holds ?REL ?AGENT @ROW)
(inList
?OBJ
(ListFn @ROW)))
(inScopeOfInterest ?AGENT ?OBJ))```

• if class is covered by ,
• then for all obj holds: if obj is an instance of class, then there exists item so that item is a member of "()" and obj is an instance of item
• .
```(=>
(exhaustiveDecomposition ?CLASS @ROW)
(forall
(?OBJ)
(=>
(instance ?OBJ ?CLASS)
(exists
(?ITEM)
(and
(inList
?ITEM
(ListFn @ROW))
(instance ?OBJ ?ITEM))))))```

• if class is disjointly decomposed into ,
• then for all item holds: if item is a member of "()", then item is a subclass of class
• .
```(=>
(disjointDecomposition ?CLASS @ROW)
(forall
(?ITEM)
(=>
(inList
?ITEM
(ListFn @ROW))
(subclass ?ITEM ?CLASS))))```

• if class is disjointly decomposed into ,
• then for all item1,item2 holds: if item1 is a member of "()" and item2 is a member of "()" and item1 is not equal to item2, then item1 is disjoint from item2
• .
```(=>
(disjointDecomposition ?CLASS @ROW)
(forall
(?ITEM1 ?ITEM2)
(=>
(and
(inList
?ITEM1
(ListFn @ROW))
(inList
?ITEM2
(ListFn @ROW))
(not
(equal ?ITEM1 ?ITEM2)))
(disjoint ?ITEM1 ?ITEM2))))```

If the number number argument of rel is an instance of class and rel() holds, then "numberth element of "()"" is an instance of class.
```(=>
(and
(domain ?REL ?NUMBER ?CLASS)
(holds ?REL @ROW))
(instance
(ListOrderFn
(ListFn @ROW)
?NUMBER)
?CLASS))```

If the number number argument of rel is a subclass of class and rel() holds, then "numberth element of "()"" is a subclass of class.
```(=>
(and
(domainSubclass ?REL ?NUMBER ?CLASS)
(holds ?REL @ROW))
(subclass
(ListOrderFn
(ListFn @ROW)
?NUMBER)
?CLASS))```

"length of "(,item)"" is equal to "("length of "()""+1)".
```(equal
(ListLengthFn
(ListFn @ROW ?ITEM))
(SuccessorFn
(ListLengthFn
(ListFn @ROW))))```

""length of "(,item)""th element of "(,item)"" is equal to item.
```(equal
(ListOrderFn
(ListFn @ROW ?ITEM)
(ListLengthFn
(ListFn @ROW ?ITEM)))
?ITEM)```

```(=>
(valence ?REL ?NUMBER)
(forall
(@ROW)
(=>
(holds ?REL @ROW)
(equal
(ListLengthFn
(ListFn @ROW))
?NUMBER))))```

"()" starts "(,item)".
```(initialList
(ListFn @ROW)
(ListFn @ROW ?ITEM))```

• if "the greatest common divisor of " is equal to number,
• then for all element holds: if element is a member of "()", then "element mod number" is equal to
• .
```(=>
(equal
(GreatestCommonDivisorFn @ROW)
?NUMBER)
(forall
(?ELEMENT)
(=>
(inList
?ELEMENT
(ListFn @ROW))
(equal
(RemainderFn ?ELEMENT ?NUMBER)
0))))```

• if "the greatest common divisor of " is equal to number,
• then there doesn't exist greater so that greater is greater than number and for all element holds: if element is a member of "()", then "element mod greater" is equal to
• .
```(=>
(equal
(GreatestCommonDivisorFn @ROW)
?NUMBER)
(not
(exists
(?GREATER)
(and
(greaterThan ?GREATER ?NUMBER)
(forall
(?ELEMENT)
(=>
(inList
?ELEMENT
(ListFn @ROW))
(equal
(RemainderFn ?ELEMENT ?GREATER)
0)))))))```

• if "the least common multiple of " is equal to number,
• then for all element holds: if element is a member of "()", then "number mod element" is equal to
• .
```(=>
(equal
(LeastCommonMultipleFn @ROW)
?NUMBER)
(forall
(?ELEMENT)
(=>
(inList
?ELEMENT
(ListFn @ROW))
(equal
(RemainderFn ?NUMBER ?ELEMENT)
0))))```

• if "the least common multiple of " is equal to number,
• then there doesn't exist less so that less is less than number and for all element holds: if element is a member of "()", then "less mod element" is equal to
• .
```(=>
(equal
(LeastCommonMultipleFn @ROW)
?NUMBER)
(not
(exists
(?LESS)
(and
(lessThan ?LESS ?NUMBER)
(forall
(?ELEMENT)
(=>
(inList
?ELEMENT
(ListFn @ROW))
(equal
(RemainderFn ?LESS ?ELEMENT)
0)))))))```

If obj1 is attr1 to obj2 and is opposed to ? and attr1 is a member of "()" and attr2 is a member of "()" and attr1 is not equal to attr2, then obj1 is not attr2 to obj2.
```(=>
(and
(orientation ?OBJ1 ?OBJ2 ?ATTR1)
(contraryAttribute @ROW)
(inList
?ATTR1
(ListFn @ROW))
(inList
?ATTR2
(ListFn @ROW))
(not
(equal ?ATTR1 ?ATTR2)))
(not
(orientation ?OBJ1 ?OBJ2 ?ATTR2)))```