次序列 (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.

Ontology

SUMO / BASE-ONTOLOGY

Class(es)

種類

可繼承關係

二元述詞

偏序關係

次序列

Subrelation(s)

初始化序列

Coordinate term(s)

弧線重量作者先於或同時肇因次類肇因公民封閉於相連的包含訊息共生複製日期降低可能性發展期形式無交集分配文字說明持續時間較早編者元素雇用相等等同關係於利用以...語言表達面對家族關係完成次數圖部分大於大於或等於有意圖有技巧在...期間為真須使...為真有權使...為真洞同一元素串列中在注意範圍中增加可能性獨立或然率居住抑制初始化序列實例倒序非反射於... 大於小於小於或等於位於物質測量時段相接情態屬性時段重疊雙親部分偏序於... 部分位於路徑長擁有先決條件避免特性出版範圍範圍次種類提及反射於... SUMO內部相關概念兄弟姊妹小於開始次屬性次聚集次圖次歷程次命題次種類次關係包含訊息種類包含訊息實例續接屬性封閉續接屬性時間部分時間全序於... 三分法使用（結合）價人造物版本

Type restrictions

subList(序列, 序列)

Axioms (2)

if list1 是 list2 的次序列,
then for all item holds: if item 是 list1 的一成員, then item 是 list2 的一成員

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

if list1 是 list2 的次序列,
then there exists number3 so that for all item holds: if item 是 list1 的一成員, then there exist number1,number2 so that "list1 的第二元素" 等於 item and "list2 的第二元素" 等於 item and number2 等於 "(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))))))))