sub list (subList)

(subList list1 list2) means that list1 is a sublist of list2, i.e. every element of list1 is an element of list2 and the elements that are common to both Lists have the same order in both Lists.

Ontologie

SUMO / BASE-ONTOLOGY

Class(es)

třída

inheritable relation

binární predikát
is instance of

relace částečné uspořádání
is instance of

sub list

Subrelation(s)

initial list

Související termín(y)

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 initial list instance inverse irreflexive on larger less than less than or equal to located material measure meets temporally modal attribute overlaps temporally parent part 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 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

Typy argumentů

subList(seznam, seznam)

Axiomy (2)

jestliže list1 je a sublist of list2,
potom pro všechny item platí: jestliže item je a member of list1, potom item je a member of list2

(=>
      (subList ?LIST1 ?LIST2)
      (forall
            (?ITEM)
            (=>
                  (inList ?ITEM ?LIST1)
                  (inList ?ITEM ?LIST2))))

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
                                          (AdditionFn ?NUMBER1 ?NUMBER3))))))))