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

Formal Language: 



KB Term:  Term intersection
English Word: 

Sigma KEE - ListFn
ListFn

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


s__documentation(s__ListFn__m,s__ChineseLanguage,'这是一个可以接受任何数量的参数,然后交出含有跟哪些参数完全 相同顺序的 Function。')

Merge.kif 3110-3111
s__documentation(s__ListFn__m,s__EnglishLanguage,'A Function that takes any number of arguments and returns the List containing those arguments in exactly the same order.')

Merge.kif 3108-3109
s__domain(s__ListFn__m,1,s__Entity)

Merge.kif 3105-3105 The number 1 argument of list is an instance of entity
s__instance(s__Function,s__SetOrClass)

s__instance(s__ListFn__m,s__Function)

Merge.kif 3103-3103 List is an instance of function
s__instance(s__VariableArityRelation,s__SetOrClass)

s__instance(s__ListFn__m,s__VariableArityRelation)

Merge.kif 3104-3104 List is an instance of variable arity relation
s__range(s__ListFn__m,s__List)

Merge.kif 3107-3107 The range of list is an instance of list

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


s__format(s__ChineseLanguage,s__ListFn__m,'(%*[,])')

chinese_format.kif 261-261
s__format(s__EnglishLanguage,s__ListFn__m,'(%*[,])')

english_format.kif 159-159
s__format(s__FrenchLanguage,s__ListFn__m,'(%*[,])')

french_format.kif 149-149
s__format(s__ItalianLanguage,s__ListFn__m,'(%*[,]')

relations-it.txt 167-167
s__format(s__PortugueseLanguage,s__ListFn__m,'(%*[,])')

portuguese_format.kif 101-101
s__format(s__ar__m,s__ListFn__m,'(%*[])')

arabic_format.kif 97-97
s__format(s__cz__m,s__ListFn__m,'(%*[,])')

relations-cz.txt 158-158
s__format(s__de__m,s__ListFn__m,'(%*[,])')

relations-de.txt 336-336
s__format(s__hi__m,s__ListFn__m,'(%*[,]')

relations-hindi.txt 206-206
s__format(s__tg__m,s__ListFn__m,'(%*[,]')

relations-tg.txt 333-333
s__termFormat(s__ChineseLanguage,s__ListFn__m,'表列函数')

chinese_format.kif 262-262 "表列函数" is the printable form of list in ChineseLanguage
s__termFormat(s__EnglishLanguage,s__ListFn__m,'list')

domainEnglishFormat.kif 6199-6199 "list" is the printable form of list in english language
s__termFormat(s__ar__m,s__ListFn__m,'«قائمة»')

arabic_format.kif 547-547 "«قائمة»" is the printable form of list in ar
s__termFormat(s__tg__m,s__ListFn__m,'tungkulin ng talaan')

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

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


( ! [V__ROW11,V__ROW21] :
   ((s__contraryAttribute_1(V__ROW11)
     &
     s__identicalListItems(s__ListFn_1(V__ROW11)
  ,s__ListFn_1(V__ROW21)))
=>
s__contraryAttribute_1(V__ROW21))
)

Merge.kif 520-524
( ! [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__AGENT,V__ROW1,V__OBJ] :
   ((s__instance(s__needs__m,s__IntentionalRelation) &
       s__needs(V__AGENT,V__ROW1)
     &
     s__inList(V__OBJ,s__ListFn_1(V__ROW1)))
=>
s__inScopeOfInterest(V__AGENT,V__OBJ))
)

( ! [V__AGENT,V__ROW1,V__OBJ] :
   ((s__instance(s__enemy__m,s__IntentionalRelation) &
       s__enemy(V__AGENT,V__ROW1)
     &
     s__inList(V__OBJ,s__ListFn_1(V__ROW1)))
=>
s__inScopeOfInterest(V__AGENT,V__OBJ))
)

( ! [V__AGENT,V__ROW1,V__OBJ] :
   ((s__instance(s__disapproves__m,s__IntentionalRelation) &
       s__disapproves(V__AGENT,V__ROW1)
     &
     s__inList(V__OBJ,s__ListFn_1(V__ROW1)))
=>
s__inScopeOfInterest(V__AGENT,V__OBJ))
)

( ! [V__AGENT,V__ROW1,V__OBJ] :
   ((s__instance(s__dislikes__m,s__IntentionalRelation) &
       s__dislikes(V__AGENT,V__ROW1)
     &
     s__inList(V__OBJ,s__ListFn_1(V__ROW1)))
=>
s__inScopeOfInterest(V__AGENT,V__OBJ))
)

( ! [V__AGENT,V__ROW1,V__OBJ] :
   ((s__instance(s__facebookFriend__m,s__IntentionalRelation) &
       s__facebookFriend(V__AGENT,V__ROW1)
     &
     s__inList(V__OBJ,s__ListFn_1(V__ROW1)))
=>
s__inScopeOfInterest(V__AGENT,V__OBJ))
)

( ! [V__AGENT,V__ROW1,V__OBJ] :
   ((s__instance(s__wants__m,s__IntentionalRelation) &
       s__wants(V__AGENT,V__ROW1)
     &
     s__inList(V__OBJ,s__ListFn_1(V__ROW1)))
=>
s__inScopeOfInterest(V__AGENT,V__OBJ))
)

( ! [V__AGENT,V__ROW1,V__OBJ] :
   ((s__instance(s__cohabitant__m,s__IntentionalRelation) &
       s__cohabitant(V__AGENT,V__ROW1)
     &
     s__inList(V__OBJ,s__ListFn_1(V__ROW1)))
=>
s__inScopeOfInterest(V__AGENT,V__OBJ))
)

( ! [V__AGENT,V__ROW1,V__OBJ] :
   ((s__instance(s__serviceRecipient__m,s__IntentionalRelation) &
       s__serviceRecipient(V__AGENT,V__ROW1)
     &
     s__inList(V__OBJ,s__ListFn_1(V__ROW1)))
=>
s__inScopeOfInterest(V__AGENT,V__OBJ))
)

( ! [V__AGENT,V__ROW1,V__OBJ] :
   ((s__instance(s__serviceProvider__m,s__IntentionalRelation) &
       s__serviceProvider(V__AGENT,V__ROW1)
     &
     s__inList(V__OBJ,s__ListFn_1(V__ROW1)))
=>
s__inScopeOfInterest(V__AGENT,V__OBJ))
)

( ! [V__AGENT,V__ROW1,V__OBJ] :
   ((s__instance(s__desires__m,s__IntentionalRelation) &
       s__desires(V__AGENT,V__ROW1)
     &
     s__inList(V__OBJ,s__ListFn_1(V__ROW1)))
=>
s__inScopeOfInterest(V__AGENT,V__OBJ))
)

( ! [V__AGENT,V__ROW1,V__OBJ] :
   ((s__instance(s__knows__m,s__IntentionalRelation) &
       s__knows(V__AGENT,V__ROW1)
     &
     s__inList(V__OBJ,s__ListFn_1(V__ROW1)))
=>
s__inScopeOfInterest(V__AGENT,V__OBJ))
)

( ! [V__AGENT,V__ROW1,V__OBJ] :
   ((s__instance(s__inScopeOfInterest__m,s__IntentionalRelation) &
       s__inScopeOfInterest(V__AGENT,V__ROW1)
     &
     s__inList(V__OBJ,s__ListFn_1(V__ROW1)))
=>
s__inScopeOfInterest(V__AGENT,V__OBJ))
)

( ! [V__AGENT,V__ROW1,V__OBJ] :
   ((s__instance(s__domesticPartner__m,s__IntentionalRelation) &
       s__domesticPartner(V__AGENT,V__ROW1)
     &
     s__inList(V__OBJ,s__ListFn_1(V__ROW1)))
=>
s__inScopeOfInterest(V__AGENT,V__OBJ))
)

( ! [V__AGENT,V__ROW1,V__OBJ] :
   ((s__instance(s__doubts__m,s__IntentionalRelation) &
       s__doubts(V__AGENT,V__ROW1)
     &
     s__inList(V__OBJ,s__ListFn_1(V__ROW1)))
=>
s__inScopeOfInterest(V__AGENT,V__OBJ))
)

( ! [V__AGENT,V__ROW1,V__OBJ] :
   ((s__instance(s__considers__m,s__IntentionalRelation) &
       s__considers(V__AGENT,V__ROW1)
     &
     s__inList(V__OBJ,s__ListFn_1(V__ROW1)))
=>
s__inScopeOfInterest(V__AGENT,V__OBJ))
)

( ! [V__AGENT,V__ROW1,V__OBJ] :
   ((s__instance(s__follows__m,s__IntentionalRelation) &
       s__follows(V__AGENT,V__ROW1)
     &
     s__inList(V__OBJ,s__ListFn_1(V__ROW1)))
=>
s__inScopeOfInterest(V__AGENT,V__OBJ))
)

( ! [V__AGENT,V__ROW1,V__OBJ] :
   ((s__instance(s__friend__m,s__IntentionalRelation) &
       s__friend(V__AGENT,V__ROW1)
     &
     s__inList(V__OBJ,s__ListFn_1(V__ROW1)))
=>
s__inScopeOfInterest(V__AGENT,V__OBJ))
)

( ! [V__AGENT,V__ROW1,V__OBJ] :
   ((s__instance(s__believes__m,s__IntentionalRelation) &
       s__believes(V__AGENT,V__ROW1)
     &
     s__inList(V__OBJ,s__ListFn_1(V__ROW1)))
=>
s__inScopeOfInterest(V__AGENT,V__OBJ))
)

( ! [V__AGENT,V__ROW1,V__OBJ] :
   ((s__instance(s__connectedInSocialNetwork__m,s__IntentionalRelation) &
       s__connectedInSocialNetwork(V__AGENT,V__ROW1)
     &
     s__inList(V__OBJ,s__ListFn_1(V__ROW1)))
=>
s__inScopeOfInterest(V__AGENT,V__OBJ))
)

Merge.kif 2836-2841
( ! [V__OBJ1,V__OBJ2,V__ATTR1,V__ROW1,V__ATTR2] :
   ((s__orientation(V__OBJ1,V__OBJ2,V__ATTR1)
     &
     s__contraryAttribute_1(V__ROW1)
   &
   s__inList(V__ATTR1,s__ListFn_1(V__ROW1))
&
s__inList(V__ATTR2,s__ListFn_1(V__ROW1))
&
(~ (V__ATTR1 = V__ATTR2)))
=>
(~ s__orientation(V__OBJ1,V__OBJ2,V__ATTR2)))
)

Merge.kif 17100-17108
  • If ?OBJ1 is ?ATTR1 to ?OBJ2 and @ROW is the opposite of and ?ATTR1 is a member of (@ROW) and ?ATTR2 is a member of (@ROW) and ?ATTR1 is not equal to ?ATTR2,
  • then ?OBJ1 is not ?ATTR2 to ?OBJ2
( ! [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

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__ROW1,V__ELEMENT] :
   (s__GreatestCommonDivisorFn_1(V__ROW1)
   =>
   (s__inList(V__ELEMENT,s__ListFn_1(V__ROW1))
=>
s__instance(V__ELEMENT,s__Number)))
)

Merge.kif 4984-4989
( ! [V__ROW1,V__ELEMENT] :
   (s__LeastCommonMultipleFn_1(V__ROW1)
   =>
   (s__inList(V__ELEMENT,s__ListFn_1(V__ROW1))
=>
s__instance(V__ELEMENT,s__Number)))
)

Merge.kif 5063-5068
( ! [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__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__NUMBER] :
   ((s__valence(s__contraryAttribute__m,V__NUMBER)
     &
     s__instance(s__contraryAttribute__m,s__Predicate))
   =>
   (! [V__ROW1] :
     (s__contraryAttribute_1(V__ROW1)
     =>
     (s__ListLengthFn(s__ListFn_1(V__ROW1))
   = V__NUMBER))))
)

Merge.kif 3225-3232
( ! [V__ROW1,V__ELEMENT] :
   (s__contraryAttribute_1(V__ROW1)
   =>
   (s__inList(V__ELEMENT,s__ListFn_1(V__ROW1))
=>
s__instance(V__ELEMENT,s__Attribute)))
)

Merge.kif 514-518
( ! [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__CLASS,V__ROW1] :
   (s__disjointDecomposition_2(V__CLASS,V__ROW1)
   =>
   (! [V__ITEM] :
     (s__inList(V__ITEM,s__ListFn_1(V__ROW1))
   =>
   s__subclass(V__ITEM,V__CLASS))))
)

Merge.kif 3123-3128
( ! [V__CLASS,V__ROW1] :
   (s__disjointDecomposition_2(V__CLASS,V__ROW1)
   =>
   (! [V__ITEM1,V__ITEM2] :
     ((s__inList(V__ITEM1,s__ListFn_1(V__ROW1))
     &
     s__inList(V__ITEM2,s__ListFn_1(V__ROW1))
&
(~ (V__ITEM1 = V__ITEM2)))
=>
s__disjoint(V__ITEM1,V__ITEM2))))
)

Merge.kif 3130-3139
( ! [V__ROW1,V__ELEMENT] :
   (s__disjointDecomposition_1(V__ROW1)
   =>
   (s__inList(V__ELEMENT,s__ListFn_1(V__ROW1))
=>
s__instance(V__ELEMENT,s__Class)))
)

Merge.kif 614-618
( ! [V__ROW1,V__NUMBER] :
   ((s__GreatestCommonDivisorFn_1(V__ROW1)
     = V__NUMBER)
   =>
   (! [V__ELEMENT] :
     (s__inList(V__ELEMENT,s__ListFn_1(V__ROW1))
   =>
   (s__RemainderFn(V__ELEMENT,V__NUMBER)
   = 0))))
)

Merge.kif 4991-4996
  • If the greatest common divisor of @ROW is equal to ?NUMBER,
  • then for all ?ELEMENT
    • if ?ELEMENT is a member of (@ROW),
    • then ?ELEMENT mod ?NUMBER is equal to 0
( ! [V__ROW1,V__NUMBER] :
   ((s__GreatestCommonDivisorFn_1(V__ROW1)
     = V__NUMBER)
   =>
   (~ (? [V__GREATER] :
       (greater(V__GREATER,V__NUMBER)
         &
         (! [V__ELEMENT] :
           (s__inList(V__ELEMENT,s__ListFn_1(V__ROW1))
         =>
         (s__RemainderFn(V__ELEMENT,V__GREATER)
         = 0)))))))
)

Merge.kif 4998-5006
  • If the greatest common divisor of @ROW is equal to ?NUMBER,
  • then there doesn't exist ?GREATER such that ?GREATER is greater than ?NUMBER and for all ?ELEMENT
    • if ?ELEMENT is a member of (@ROW),
    • then ?ELEMENT mod ?GREATER is equal to 0
( ! [V__ROW1,V__NUMBER] :
   ((s__LeastCommonMultipleFn_1(V__ROW1)
     = V__NUMBER)
   =>
   (! [V__ELEMENT] :
     (s__inList(V__ELEMENT,s__ListFn_1(V__ROW1))
   =>
   (s__RemainderFn(V__NUMBER,V__ELEMENT)
   = 0))))
)

Merge.kif 5070-5075
  • If the least common multiple of @ROW is equal to ?NUMBER,
  • then for all ?ELEMENT
    • if ?ELEMENT is a member of (@ROW),
    • then ?NUMBER mod ?ELEMENT is equal to 0
( ! [V__ROW1,V__NUMBER] :
   ((s__LeastCommonMultipleFn_1(V__ROW1)
     = V__NUMBER)
   =>
   (~ (? [V__LESS] :
       (less(V__LESS,V__NUMBER)
         &
         (! [V__ELEMENT] :
           (s__inList(V__ELEMENT,s__ListFn_1(V__ROW1))
         =>
         (s__RemainderFn(V__LESS,V__ELEMENT)
         = 0)))))))
)

Merge.kif 5077-5085
  • If the least common multiple of @ROW is equal to ?NUMBER,
  • then there doesn't exist ?LESS such that ?LESS is less than ?NUMBER and for all ?ELEMENT
    • if ?ELEMENT is a member of (@ROW),
    • then ?LESS mod ?ELEMENT is equal to 0
( ! [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__CLASS,V__ROW1,V__ATTR] :
   (s__exhaustiveAttribute_2(V__CLASS,V__ROW1)
   =>
   (s__inList(V__ATTR,s__ListFn_1(V__ROW1))
=>
s__instance(V__ATTR,s__Attribute)))
)

Merge.kif 552-556
( ! [V__CLASS,V__ROW1] :
   (s__exhaustiveAttribute_2(V__CLASS,V__ROW1)
   =>
   (! [V__ATTR1] :
     (s__instance(V__ATTR1,V__CLASS)
     =>
     (? [V__ATTR2] :
       (s__inList(V__ATTR2,s__ListFn_1(V__ROW1))
     &
     (V__ATTR1 = V__ATTR2))))))
)

Merge.kif 558-566
  • If @ROW are all the attributes of ?CLASS,
  • then for all ?ATTR1
    • if ?ATTR1 is an instance of ?CLASS,
    • then there exists ?ATTR2 such that ?ATTR2 is a member of (@ROW) and ?ATTR1 is equal to ?ATTR2

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25

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


No TPTP formula. May not be expressible in strict first order. Merge.kif 3214-3217 For all @ROW and ?ITEM length of (@ROW and ?ITEM) is equal to (length of (@ROW)+1)
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
(! [V__ROW1,V__ITEM] :
   s__initialList(s__ListFn_1(V__ROW1)
,s__ListFn_2(V__ROW1,V__ITEM)))

Merge.kif 3372-3373 For all @ROW and ?ITEM (@ROW) starts (@ROW and ?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