Browsing Interface : Welcome guest : log in
Home |  Graph |  ]  KB:  Language:   

Formal Language: 



KB Term:  Term intersection
English Word: 

Sigma KEE - ListOrderFn
ListOrderFn

appearance as argument number 1
-------------------------


s__documentation(s__ListOrderFn__m,s__ChineseLanguage,'(ListOrderFn ?LIST ?NUMBER) 表示在 ?LIST List 第?NUMBER个位置的项目。例如: (ListOrderFn (ListFn Monday Tuesday Wednesday) 2) 交出的值会是 Tuesday。')

Merge.kif 3157-3159
s__documentation(s__ListOrderFn__m,s__EnglishLanguage,'(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.')

Merge.kif 3153-3156
s__domain(s__ListOrderFn__m,1,s__List)

Merge.kif 3150-3150 The number 1 argument of list order is an instance of list
s__domain(s__ListOrderFn__m,2,s__PositiveInteger)

Merge.kif 3151-3151 The number 2 argument of list order is an instance of positive integer
s__instance(s__ListOrderFn__m,s__BinaryFunction)

s__instance(s__BinaryFunction,s__SetOrClass)

Merge.kif 3148-3148 List order is an instance of binary function
s__instance(s__ListOrderFn__m,s__PartialValuedRelation)

s__instance(s__PartialValuedRelation,s__SetOrClass)

Merge.kif 3149-3149 List order is an instance of partial valued relation
s__range(s__ListOrderFn__m,s__Entity)

Merge.kif 3152-3152 The range of list order is an instance of entity

appearance as argument number 2
-------------------------


s__format(s__ChineseLanguage,s__ListOrderFn__m,'%1 的第 %2 几个元素')

chinese_format.kif 263-263
s__format(s__EnglishLanguage,s__ListOrderFn__m,'%2th element of %1')

english_format.kif 160-160
s__format(s__FrenchLanguage,s__ListOrderFn__m,'%2th �lement de %1')

french_format.kif 150-150
s__format(s__ItalianLanguage,s__ListOrderFn__m,'%2th elemento di %1')

relations-it.txt 169-169
s__format(s__PortugueseLanguage,s__ListOrderFn__m,'%2th elemento de %1')

portuguese_format.kif 102-102
s__format(s__ar__m,s__ListOrderFn__m,'%2 عُنْصُر من %1')

arabic_format.kif 98-98
s__format(s__cz__m,s__ListOrderFn__m,'%2th element of %1')

relations-cz.txt 159-159
s__format(s__de__m,s__ListOrderFn__m,'%2te mitglied von %1')

relations-de.txt 338-338
s__format(s__hi__m,s__ListOrderFn__m,'%1 kaa ghaTaka sankhyaa %2')

relations-hindi.txt 207-207
s__format(s__tg__m,s__ListOrderFn__m,'%2th elemento ng %1')

relations-tg.txt 337-337
s__termFormat(s__ChineseLanguage,s__ListOrderFn__m,'找出表列顺序的函数')

chinese_format.kif 264-264 "找出表列顺序的函数" is the printable form of list order in ChineseLanguage
s__termFormat(s__EnglishLanguage,s__ListOrderFn__m,'list order')

domainEnglishFormat.kif 6201-6201 "list order" is the printable form of list order in english language
s__termFormat(s__ar__m,s__ListOrderFn__m,'«عُنْصُر من»')

arabic_format.kif 548-548 "«عُنْصُر من»" is the printable form of list order in ar
s__termFormat(s__tg__m,s__ListOrderFn__m,'tungkulin ng talaan utos1')

relations-tg.txt 338-338 "tungkulin ng talaan utos1" is the printable form of list order in tg

antecedent
-------------------------


( ! [V__ARG,V__ARGS1,V__X,V__Y] :
   ((s__exactCardinality(s__contraryAttribute__m,V__ARG,1)
     &
     s__instance(s__contraryAttribute__m,s__Predicate) &
     s__contraryAttribute_1(V__ARGS1)
   &
   (V__X = s__ListOrderFn(s__ListFn_1(V__ARGS1)
  ,V__ARG))
&
(V__Y = s__ListOrderFn(s__ListFn_1(V__ARGS1)
,V__ARG)))
=>
(V__X = V__Y))
)

Media.kif 2108-2115
( ! [V__ARG,V__ARGS1,V__X] :
   ((s__exactCardinality(s__contraryAttribute__m,V__ARG,1)
     &
     s__instance(s__contraryAttribute__m,s__Predicate) &
     s__contraryAttribute_1(V__ARGS1)
   &
   (V__X = s__ListOrderFn(s__ListFn_1(V__ARGS1)
  ,V__ARG)))
=>
(~ (? [V__Y] :
((V__Y = s__ListOrderFn(s__ListFn_1(V__ARGS1)
  ,V__ARG))
&
(~ (V__X = V__Y))))))
)

Media.kif 2095-2105
( ! [V__DIRECTION,V__ROW1,V__NUM] :
   ((s__instance(s__LatitudeFn_2(V__DIRECTION,V__ROW1)
    ,s__Region) &
     (s__ListOrderFn(s__ListFn_1(V__ROW1)
    ,1)
   = s__MeasureFn(V__NUM,s__AngularDegree)))
=>
lesseq(V__NUM,90))
)

Geography.kif 427-431
( ! [V__DIRECTION,V__ROW1,V__NUM] :
   ((s__instance(s__LongitudeFn_2(V__DIRECTION,V__ROW1)
    ,s__Region) &
     (s__ListOrderFn(s__ListFn_1(V__ROW1)
    ,1)
   = s__MeasureFn(V__NUM,s__AngularDegree)))
=>
lesseq(V__NUM,180))
)

Geography.kif 467-471
( ! [V__ROW1,V__Process1,V__Process2,V__Number1,V__Number2] :
   ((s__processList_1(V__ROW1)
     &
     s__inList(V__Process1,s__ListFn_1(V__ROW1))
&
s__inList(V__Process2,s__ListFn_1(V__ROW1))
&
(s__ListOrderFn(s__ListFn_1(V__ROW1)
,V__Number1)
= V__Process1)
&
(s__ListOrderFn(s__ListFn_1(V__ROW1)
,V__Number2)
= V__Process2)
&
less(V__Number1,V__Number2))
=>
s__earlier(s__WhenFn(V__Process1)
,s__WhenFn(V__Process2)))
)

QoSontology.kif 692-700
  • If the list of processes @ROW and ?Process1 is a member of (@ROW) and ?Process2 is a member of (@ROW) and ?Number1th element of (@ROW) is equal to ?Process1 and ?Number2th element of (@ROW) is equal to ?Process2 and ?Number1 is less than ?Number2,
  • then the time of existence of ?Process1 happens earlier than the time of existence of ?Process2
( ! [V__USER,V__LIST,V__ACCESSING1,V__ACCESSING2,V__INDEX1,V__INDEX2] :
   ((s__viewedItemList(V__USER,V__LIST)
     &
     s__instance(V__ACCESSING1,s__AccessingWebPage) &
     s__instance(V__ACCESSING2,s__AccessingWebPage) &
     s__instance(V__INDEX1,s__PositiveInteger) &
     s__instance(V__INDEX2,s__PositiveInteger) &
     (s__ListOrderFn(V__LIST,V__INDEX1)
     = V__ACCESSING1)
   &
   (s__ListOrderFn(V__LIST,V__INDEX2)
   = V__ACCESSING2)
&
greater(V__INDEX1,V__INDEX2))
=>
s__earlier(s__WhenFn(V__ACCESSING2)
,s__WhenFn(V__ACCESSING1)))
)

UXExperimentalTerms.kif 990-1006

consequent
-------------------------


( ! [V__ROW1] :
   ((s__instance(s__parent__m,s__TotalValuedRelation) &
       s__instance(s__parent__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__parent__m,s__Relation) &
         s__valence(s__parent__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__parent__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__parent(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__protonNumber__m,s__TotalValuedRelation) &
       s__instance(s__protonNumber__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__protonNumber__m,s__Relation) &
         s__valence(s__protonNumber__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__protonNumber__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__protonNumber(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__lineMeasure__m,s__TotalValuedRelation) &
       s__instance(s__lineMeasure__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__lineMeasure__m,s__Relation) &
         s__valence(s__lineMeasure__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__lineMeasure__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__lineMeasure(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__earlier__m,s__TotalValuedRelation) &
       s__instance(s__earlier__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__earlier__m,s__Relation) &
         s__valence(s__earlier__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__earlier__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__earlier(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__conclusion__m,s__TotalValuedRelation) &
       s__instance(s__conclusion__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__conclusion__m,s__Relation) &
         s__valence(s__conclusion__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__conclusion__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__conclusion(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__coordinates__m,s__TotalValuedRelation) &
       s__instance(s__coordinates__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__coordinates__m,s__Relation) &
         s__valence(s__coordinates__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__coordinates__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__coordinates(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__subCollection__m,s__TotalValuedRelation) &
       s__instance(s__subCollection__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__subCollection__m,s__Relation) &
         s__valence(s__subCollection__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__subCollection__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__subCollection(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__meetsTemporally__m,s__TotalValuedRelation) &
       s__instance(s__meetsTemporally__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__meetsTemporally__m,s__Relation) &
         s__valence(s__meetsTemporally__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__meetsTemporally__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__meetsTemporally(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__subrelation__m,s__TotalValuedRelation) &
       s__instance(s__subrelation__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__subrelation__m,s__Relation) &
         s__valence(s__subrelation__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__subrelation__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__subrelation(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(greater__m,s__TotalValuedRelation) &
       s__instance(greater__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(greater__m,s__Relation) &
         s__valence(greater__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(greater__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   greater(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__subAttribute__m,s__TotalValuedRelation) &
       s__instance(s__subAttribute__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__subAttribute__m,s__Relation) &
         s__valence(s__subAttribute__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__subAttribute__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__subAttribute(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__subclass__m,s__TotalValuedRelation) &
       s__instance(s__subclass__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__subclass__m,s__Relation) &
         s__valence(s__subclass__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__subclass__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__subclass(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__larger__m,s__TotalValuedRelation) &
       s__instance(s__larger__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__larger__m,s__Relation) &
         s__valence(s__larger__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__larger__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__larger(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__maximumPayloadCapacity__m,s__TotalValuedRelation) &
       s__instance(s__maximumPayloadCapacity__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__maximumPayloadCapacity__m,s__Relation) &
         s__valence(s__maximumPayloadCapacity__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__maximumPayloadCapacity__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__maximumPayloadCapacity(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(lesseq__m,s__TotalValuedRelation) &
       s__instance(lesseq__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(lesseq__m,s__Relation) &
         s__valence(lesseq__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(lesseq__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   lesseq(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__partlyLocated__m,s__TotalValuedRelation) &
       s__instance(s__partlyLocated__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__partlyLocated__m,s__Relation) &
         s__valence(s__partlyLocated__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__partlyLocated__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__partlyLocated(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(greatereq__m,s__TotalValuedRelation) &
       s__instance(greatereq__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(greatereq__m,s__Relation) &
         s__valence(greatereq__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(greatereq__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   greatereq(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__moves__m,s__TotalValuedRelation) &
       s__instance(s__moves__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__moves__m,s__Relation) &
         s__valence(s__moves__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__moves__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__moves(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__beforeOrEqual__m,s__TotalValuedRelation) &
       s__instance(s__beforeOrEqual__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__beforeOrEqual__m,s__Relation) &
         s__valence(s__beforeOrEqual__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__beforeOrEqual__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__beforeOrEqual(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__eventLocated__m,s__TotalValuedRelation) &
       s__instance(s__eventLocated__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__eventLocated__m,s__Relation) &
         s__valence(s__eventLocated__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__eventLocated__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__eventLocated(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__smaller__m,s__TotalValuedRelation) &
       s__instance(s__smaller__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__smaller__m,s__Relation) &
         s__valence(s__smaller__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__smaller__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__smaller(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__diameter__m,s__TotalValuedRelation) &
       s__instance(s__diameter__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__diameter__m,s__Relation) &
         s__valence(s__diameter__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__diameter__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__diameter(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__electronNumber__m,s__TotalValuedRelation) &
       s__instance(s__electronNumber__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__electronNumber__m,s__Relation) &
         s__valence(s__electronNumber__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__electronNumber__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__electronNumber(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__personTransportCapability__m,s__TotalValuedRelation) &
       s__instance(s__personTransportCapability__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__personTransportCapability__m,s__Relation) &
         s__valence(s__personTransportCapability__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__personTransportCapability__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__personTransportCapability(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__abstractPart__m,s__TotalValuedRelation) &
       s__instance(s__abstractPart__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__abstractPart__m,s__Relation) &
         s__valence(s__abstractPart__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__abstractPart__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__abstractPart(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__transactionAmount__m,s__TotalValuedRelation) &
       s__instance(s__transactionAmount__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__transactionAmount__m,s__Relation) &
         s__valence(s__transactionAmount__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__transactionAmount__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__transactionAmount(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__time__m,s__TotalValuedRelation) &
       s__instance(s__time__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__time__m,s__Relation) &
         s__valence(s__time__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__time__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__time(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__caliber__m,s__TotalValuedRelation) &
       s__instance(s__caliber__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__caliber__m,s__Relation) &
         s__valence(s__caliber__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__caliber__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__caliber(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__graphPart__m,s__TotalValuedRelation) &
       s__instance(s__graphPart__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__graphPart__m,s__Relation) &
         s__valence(s__graphPart__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__graphPart__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__graphPart(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__geometricPart__m,s__TotalValuedRelation) &
       s__instance(s__geometricPart__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__geometricPart__m,s__Relation) &
         s__valence(s__geometricPart__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__geometricPart__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__geometricPart(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__changesLocation__m,s__TotalValuedRelation) &
       s__instance(s__changesLocation__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__changesLocation__m,s__Relation) &
         s__valence(s__changesLocation__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__changesLocation__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__changesLocation(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__temporalPart__m,s__TotalValuedRelation) &
       s__instance(s__temporalPart__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__temporalPart__m,s__Relation) &
         s__valence(s__temporalPart__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__temporalPart__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__temporalPart(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__path__m,s__TotalValuedRelation) &
       s__instance(s__path__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__path__m,s__Relation) &
         s__valence(s__path__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__path__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__path(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__premise__m,s__TotalValuedRelation) &
       s__instance(s__premise__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__premise__m,s__Relation) &
         s__valence(s__premise__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__premise__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__premise(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__subsumesContentClass__m,s__TotalValuedRelation) &
       s__instance(s__subsumesContentClass__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__subsumesContentClass__m,s__Relation) &
         s__valence(s__subsumesContentClass__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__subsumesContentClass__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__subsumesContentClass(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__subProcess__m,s__TotalValuedRelation) &
       s__instance(s__subProcess__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__subProcess__m,s__Relation) &
         s__valence(s__subProcess__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__subProcess__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__subProcess(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__radius__m,s__TotalValuedRelation) &
       s__instance(s__radius__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__radius__m,s__Relation) &
         s__valence(s__radius__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__radius__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__radius(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__subsumesContentInstance__m,s__TotalValuedRelation) &
       s__instance(s__subsumesContentInstance__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__subsumesContentInstance__m,s__Relation) &
         s__valence(s__subsumesContentInstance__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__subsumesContentInstance__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__subsumesContentInstance(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__contestParticipant__m,s__TotalValuedRelation) &
       s__instance(s__contestParticipant__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__contestParticipant__m,s__Relation) &
         s__valence(s__contestParticipant__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__contestParticipant__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__contestParticipant(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__stringLength__m,s__TotalValuedRelation) &
       s__instance(s__stringLength__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__stringLength__m,s__Relation) &
         s__valence(s__stringLength__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__stringLength__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__stringLength(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__subList__m,s__TotalValuedRelation) &
       s__instance(s__subList__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__subList__m,s__Relation) &
         s__valence(s__subList__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__subList__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__subList(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__angularMeasure__m,s__TotalValuedRelation) &
       s__instance(s__angularMeasure__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__angularMeasure__m,s__Relation) &
         s__valence(s__angularMeasure__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__angularMeasure__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__angularMeasure(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__subLanguage__m,s__TotalValuedRelation) &
       s__instance(s__subLanguage__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__subLanguage__m,s__Relation) &
         s__valence(s__subLanguage__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__subLanguage__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__subLanguage(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__duration__m,s__TotalValuedRelation) &
       s__instance(s__duration__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__duration__m,s__Relation) &
         s__valence(s__duration__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__duration__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__duration(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__initialList__m,s__TotalValuedRelation) &
       s__instance(s__initialList__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__initialList__m,s__Relation) &
         s__valence(s__initialList__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__initialList__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__initialList(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__subString__m,s__TotalValuedRelation) &
       s__instance(s__subString__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__subString__m,s__Relation) &
         s__valence(s__subString__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__subString__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__subString(V__ROW1,V__ITEM))))))
)

Merge.kif 2308-2325 ?REL is an instance of total valued relation and ?REL is an instance of predicate if and only if there exists ?VALENCE such that ?REL is an instance of relation and ?REL %&has ?VALENCE argument(s) and
  • if for all ?NUMBER, ?ELEMENT and ?CLASS
    • 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 (@ROW),
    • then ?ELEMENT is an instance of ?CLASS
    ,
  • then there exists ?ITEM such that ?REL @ROW and ?ITEM
( ! [V__LIST1,V__AVERAGE,V__LASTPLACE] :
   (s__average(V__LIST1,V__AVERAGE)
   <=>
   (? [V__LIST2] :
     ((s__ListLengthFn(V__LIST2)
       = s__ListLengthFn(V__LIST1))
   &
   (s__ListOrderFn(V__LIST2,1)
   = s__ListOrderFn(V__LIST1,1))
&
(! [V__ITEMFROM2] :
(s__inList(V__ITEMFROM2,V__LIST2)
=>
(? [V__POSITION,V__POSITIONMINUSONE,V__ITEMFROM1,V__PRIORFROM2] :
   (greater(V__POSITION,1)
     &
     lesseq(V__POSITION,s__ListLengthFn(V__LIST2))
   &
   (s__ListOrderFn(V__LIST2,V__ITEMFROM2)
   = V__POSITION)
&
s__inList(V__ITEMFROM1,V__LIST1)
&
(V__POSITION = s__ListOrderFn(V__LIST1,V__ITEMFROM1))
&
s__inList(V__PRIORFROM2,V__LIST2)
&
(V__POSITIONMINUSONE = minus(V__POSITION,1))
&
(V__POSITIONMINUSONE = s__ListOrderFn(V__LIST2,V__PRIORFROM2))
&
(V__ITEMFROM2 = plus(V__ITEMFROM1,V__PRIORFROM2))))))
&
(V__LASTPLACE = s__ListLengthFn(V__LIST2))
&
(V__AVERAGE = divide(s__ListOrderFn(V__LIST2,V__LASTPLACE)
,V__LASTPLACE)))))
)

People.kif 285-306 ?AVERAGE is an average of ?LIST1 if and only if there exists ?LIST2 such that length of ?LIST2 is equal to length of ?LIST1 and 1th element of ?LIST2 is equal to 1th element of ?LIST1 and for all ?ITEMFROM2
  • if ?ITEMFROM2 is a member of ?LIST2,
  • then there exist ?POSITION, ?POSITIONMINUSONE,, , ?ITEMFROM1 and ?PRIORFROM2 such that ?POSITION is greater than 1 and ?POSITION is less than or equal to length of ?LIST2 and ?ITEMFROM2th element of ?LIST2 is equal to ?POSITION and ?ITEMFROM1 is a member of ?LIST1 and ?POSITION is equal to ?ITEMFROM1th element of ?LIST1 and ?PRIORFROM2 is a member of ?LIST2 and ?POSITIONMINUSONE is equal to (?POSITION and 1) and ?POSITIONMINUSONE is equal to ?PRIORFROM2th element of ?LIST2 and ?ITEMFROM2 is equal to (?ITEMFROM1 and ?PRIORFROM2)
and ?LASTPLACE is equal to length of ?LIST2 and ?AVERAGE is equal to ?LASTPLACEth element of ?LIST2 and ?LASTPLACE
( ! [V__LIST,V__ITEM] :
   ((s__LastFn(V__LIST)
     = V__ITEM)
   <=>
   (? [V__NUMBER] :
     ((s__ListLengthFn(V__LIST)
       = V__NUMBER)
     &
     (s__ListOrderFn(V__LIST,V__NUMBER)
     = V__ITEM))))
)

Mid-level-ontology.kif 6342-6347 The last of ?LIST is equal to ?ITEM if and only if there exists ?NUMBER such that length of ?LIST is equal to ?NUMBER and ?NUMBERth element of ?LIST is equal to ?ITEM
( ! [V__NUMBER,V__CLASS,V__ROW1] :
   ((s__domain(s__contraryAttribute__m,V__NUMBER,V__CLASS)
     &
     s__instance(s__contraryAttribute__m,s__Predicate) &
     s__contraryAttribute_1(V__ROW1))
=>
s__instance(s__ListOrderFn(s__ListFn_1(V__ROW1)
,V__NUMBER)
,V__CLASS))
)

Merge.kif 3173-3178
( ! [V__NUMBER,V__CLASS,V__ROW1] :
   ((s__domainSubclass(s__contraryAttribute__m,V__NUMBER,V__CLASS)
     &
     s__instance(s__contraryAttribute__m,s__Predicate) &
     s__contraryAttribute_1(V__ROW1))
=>
s__subclass(s__ListOrderFn(s__ListFn_1(V__ROW1)
,V__NUMBER)
,V__CLASS))
)

Merge.kif 3180-3185
( ! [V__ARG,V__ARGS1,V__X] :
   ((s__exactCardinality(s__contraryAttribute__m,V__ARG,1)
     &
     s__instance(s__contraryAttribute__m,s__Predicate) &
     s__contraryAttribute_1(V__ARGS1)
   &
   (V__X = s__ListOrderFn(s__ListFn_1(V__ARGS1)
  ,V__ARG)))
=>
(~ (? [V__Y] :
((V__Y = s__ListOrderFn(s__ListFn_1(V__ARGS1)
  ,V__ARG))
&
(~ (V__X = V__Y))))))
)

Media.kif 2095-2105
( ! [V__ARG] :
   ((s__exactCardinality(s__contraryAttribute__m,V__ARG,1)
     &
     s__instance(s__contraryAttribute__m,s__Predicate))
   =>
   (? [V__X,V__ARGS1] :
     (s__contraryAttribute_1(V__ARGS1)
     &
     (V__X = s__ListOrderFn(s__ListFn_1(V__ARGS1)
    ,V__ARG))
&
(~ (? [V__Y] :
     ((V__Y = s__ListOrderFn(s__ListFn_1(V__ARGS1)
      ,V__ARG))
   &
   (~ (V__X = V__Y))))))))
)

Media.kif 2077-2092
  • If there can be 1 values to argument ?ARG of ?REL and ?REL is an instance of predicate,
  • then there exist ?X and @ARGS such that ?REL @ARGS and ?X is equal to ?ARGth element of (@ARGS) and there doesn't exist ?Y such that ?Y is equal to ?ARGth element of (@ARGS) and ?X is not equal to ?Y
( ! [V__ARG,V__COUNT,V__ARGS1,V__EL] :
   ((s__exactCardinality(s__contraryAttribute__m,V__ARG,V__COUNT)
     &
     s__instance(s__contraryAttribute__m,s__Predicate))
   =>
   (? [V__S] :
     (s__instance(V__S,s__SetOrClass) &
       ((s__contraryAttribute_1(V__ARGS1)
         &
         (V__EL = s__ListOrderFn(s__ListFn_1(V__ARGS1)
        ,V__ARG)))
   =>
   (s__instance(V__EL,V__S)
   &
   (s__CardinalityFn(V__S)
   = V__COUNT))))))
)

Media.kif 2134-2147
( ! [V__LIST] :
   ((s__instance(V__LIST,s__List) &
       (~ (V__LIST = s__NullList__m)))
       =>
       (s__FirstFn(V__LIST)
       = s__ListOrderFn(V__LIST,1)))
)

Mid-level-ontology.kif 6356-6361
( ! [V__SEO,V__PAGE,V__BEFORE,V__AFTER] :
   ((s__instance(V__SEO,s__SEO) &
       s__patient(V__SEO,V__PAGE))
   =>
   s__hasPurpose(V__SEO,'(? [V__SRPRESULT_BEFORE,V__SRPRESULT_AFTER,V__BM1,V__BM2] : (s__instance(V__SRPRESULT_BEFORE,s__SRPResults) & s__instance(V__SRPRESULT_AFTER,s__SRPResult) & (V__PAGE = s__ListOrderFn(V__SRPRESULT_BEFORE,V__BEFORE)) & (V__PAGE = s__ListOrderFn(V__SRPRESULT_AFTER,V__AFTER)) & s__instance(V__BM1,s__BestMatchAlgorithm) & s__instance(V__BM2,s__BestMatchAlgorithm) & s__earlier(s__WhenFn(V__BM1),s__WhenFn(V__BM2)) & s__earlier(s__WhenFn(V__SEO),s__WhenFn(V__BM2)) & s__earlier(s__WhenFn(V__BM1),s__WhenFn(V__SEO)) & greater(V__BEFORE,V__AFTER)))'))
)

UXExperimentalTerms.kif 2596-2612
( ! [V__ARG,V__COUNT,V__ARGS1,V__EL] :
   ((s__maxCardinality(s__contraryAttribute__m,V__ARG,V__COUNT)
     &
     s__instance(s__contraryAttribute__m,s__Predicate))
   =>
   (? [V__S] :
     (s__instance(V__S,s__SetOrClass) &
       ((s__contraryAttribute_1(V__ARGS1)
         &
         (V__EL = s__ListOrderFn(s__ListFn_1(V__ARGS1)
        ,V__ARG)))
   =>
   (s__instance(V__EL,V__S)
   &
   lesseq(s__CardinalityFn(V__S)
  ,V__COUNT))))))
)

Media.kif 2205-2218
( ! [V__ARG,V__COUNT,V__ARGS1,V__EL] :
   ((s__minCardinality(s__contraryAttribute__m,V__ARG,V__COUNT)
     &
     s__instance(s__contraryAttribute__m,s__Predicate))
   =>
   (? [V__S] :
     (s__instance(V__S,s__SetOrClass) &
       ((s__contraryAttribute_1(V__ARGS1)
         &
         (V__EL = s__ListOrderFn(s__ListFn_1(V__ARGS1)
        ,V__ARG)))
   =>
   (s__instance(V__EL,V__S)
   &
   greatereq(s__CardinalityFn(V__S)
  ,V__COUNT))))))
)

Media.kif 2170-2183
( ! [V__ROW1,V__NUMBER1,V__NUMBER2,V__OBJ] :
   (s__contraryAttribute_1(V__ROW1)
   =>
   (! [V__ATTR1,V__ATTR2] :
     (((V__ATTR1 = s__ListOrderFn(s__ListFn_1(V__ROW1)
        ,V__NUMBER1))
     &
     (V__ATTR2 = s__ListOrderFn(s__ListFn_1(V__ROW1)
    ,V__NUMBER2))
&
(~ (V__NUMBER1 = V__NUMBER2)))
=>
(s__property(V__OBJ,V__ATTR1)
=>
(~ s__property(V__OBJ,V__ATTR2))))))
)

Merge.kif 526-536
( ! [V__LIST1,V__LIST2,V__ROW11,V__ROW21] :
   ((V__LIST1 = V__LIST2)
     =>
     (((V__LIST1 = s__ListFn_1(V__ROW11))
       &
       (V__LIST2 = s__ListFn_1(V__ROW21)))
   =>
   (! [V__NUMBER] :
     (s__ListOrderFn(s__ListFn_1(V__ROW11)
    ,V__NUMBER)
   = s__ListOrderFn(s__ListFn_1(V__ROW21)
,V__NUMBER)))))
)

Merge.kif 326-333
  • If ?LIST1 is equal to ?LIST2,
  • then
    • if ?LIST1 is equal to (@ROW1) and ?LIST2 is equal to (@ROW2),
    • then for all ?NUMBER ?NUMBERth element of (@ROW1) is equal to ?NUMBERth element of (@ROW2)
( ! [V__REL,V__ARG,V__COUNT,V__EL,V__ARGS1] :
   (s__exactCardinality(V__REL,V__ARG,V__COUNT)
   =>
   (s__CardinalityFn(s__KappaFn(V__EL,'(V__REL(V__ARGS1) & (V__EL = s__ListOrderFn(s__ListFn_1(V__ARGS1),V__ARG)))'))
= V__COUNT))
)

Media.kif 2123-2131
  • If there can be ?COUNT values to argument ?ARG of ?REL,
  • then the number of instances in the class described by ?EL is equal to ?COUNT
( ! [V__ATTRCLASS,V__ROW1] :
   (s__exhaustiveAttribute_2(V__ATTRCLASS,V__ROW1)
   =>
   (~ (? [V__EL] :
       (s__instance(V__EL,V__ATTRCLASS)
       &
       (~ (? [V__ATTR,V__NUMBER] :
           ((V__EL = V__ATTR)
             &
             (V__ATTR = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))))))))
)

Merge.kif 568-580
  • If @ROW are all the attributes of ?ATTRCLASS,
  • then there doesn't exist ?EL such that ?EL is an instance of ?ATTRCLASS and there don't exist ?ATTR and ?NUMBER such that ?EL is equal to ?ATTR and ?ATTR is equal to ?NUMBERth element of (@ROW)
( ! [V__ITEM,V__LIST] :
   (s__inList(V__ITEM,V__LIST)
   =>
   (? [V__NUMBER] :
     (s__ListOrderFn(V__LIST,V__NUMBER)
     = V__ITEM)))
)

Merge.kif 3294-3297
  • If ?ITEM is a member of ?LIST,
  • then there exists ?NUMBER such that ?NUMBERth element of ?LIST is equal to ?ITEM
( ! [V__LIST] :
   (s__instance(V__LIST,s__UniqueList) =>
     (! [V__NUMBER1,V__NUMBER2] :
       ((s__ListOrderFn(V__LIST,V__NUMBER1)
         = s__ListOrderFn(V__LIST,V__NUMBER2))
     =>
     (V__NUMBER1 = V__NUMBER2))))
)

Merge.kif 3081-3086
( ! [V__REL,V__ARG,V__COUNT,V__EL,V__ARGS1] :
   (s__maxCardinality(V__REL,V__ARG,V__COUNT)
   =>
   lesseq(s__CardinalityFn(s__KappaFn(V__EL,'(V__REL(V__ARGS1) & (V__EL = s__ListOrderFn(s__ListFn_1(V__ARGS1),V__ARG)))'))
,V__COUNT))
)

Media.kif 2194-2202
  • If there can be at most ?COUNT values to argument ?ARG of ?REL,
  • then the number of instances in the class described by ?EL is less than or equal to ?COUNT
( ! [V__REL,V__ARG,V__COUNT,V__EL,V__ARGS1] :
   (s__minCardinality(V__REL,V__ARG,V__COUNT)
   =>
   greatereq(s__CardinalityFn(s__KappaFn(V__EL,'(V__REL(V__ARGS1) & (V__EL = s__ListOrderFn(s__ListFn_1(V__ARGS1),V__ARG)))'))
,V__COUNT))
)

Media.kif 2158-2166
  • If there are at least ?COUNT values to argument ?ARG of ?REL,
  • then the number of instances in the class described by ?EL is greater than or equal to ?COUNT

statement
-------------------------


No TPTP formula. May not be expressible in strict first order. Merge.kif 3219-3223 For all @ROW and ?ITEM length of (@ROW and ?ITEM)th element of (@ROW and ?ITEM) is equal to ?ITEM


Show full definition with tree view
Show simplified definition (without tree view)
Show simplified definition (with tree view)



Sigma web home      Suggested Upper Merged Ontology (SUMO) web home
Sigma version 2.99c (>= 2017/11/20) is open source software produced by Articulate Software and its partners