initial list (initialList)

(initialList list1 list2) means that list1 is a subList of list2 and (ListOrderFn list1 number) returns the same value as (ListOrderFn list2 number) for all of the values of number over which (ListOrderFn list1 number) is defined.

Ontology

SUMO / BASE-ONTOLOGY

Class(es)

Classe

inheritable relation

PredicatoBinario

initial list

Superrelation(s)

sub list

initial list

Coordinate term(s)

arc weight authors before or equal causes causes subclass citizen closed on connected contains information cooccur copy date decreases likelihood developmental form disjoint distributes documentation duration earlier editor element employs equal equivalence relation on exploits expressed in language faces family relation finishes frequency graph part greater than greater than or equal to has purpose has skill holds during holds obligation holds right hole identity element in list in scope of interest increases likelihood independent probability inhabits inhibits instance inverse irreflexive on larger less than less than or equal to material measure meets temporally modal attribute overlaps temporally parent partial ordering on partly located path length possesses precondition prevents property publishes range range subclass refers reflexive on related internal concept sibling smaller starts sub attribute sub collection sub graph sub list sub process sub proposition subclass subrelation subsumes content class subsumes content instance successor attribute successor attribute closure temporal part time total ordering on trichotomizing on uses valence version

Axioms (3)

Se "lunghezza di list1" is uguale a number, allora esiste list2 tale che list1 inizias list2 e "(number+1" is uguale a "lunghezza di list2" e ""(number+1"th elemento di list2" is uguale a item.

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

se list1 inizias list2,
allora per ogni number1,number2 vale: se "lunghezza di list1" is uguale a number1 e number2 é minore o uguale a number1, allora "number2th elemento di list1" is uguale a "number2th elemento di list2"

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

"(" inizias "(,item".

(initialList
      (ListFn @ROW)
      (ListFn @ROW ?ITEM))