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

Formal Language: 



KB Term:  Term intersection
English Word: 

  inList

Sigma KEE - inList
inList

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


s__documentation(s__inList__m,s__ChineseLanguage,'"这是类似 Listelementinstance。 (inList ?OBJ ?LIST) 的意思是 ?OBJ 是在 ?LIST List 里。例如: (inList Tuesday (ListFn Monday Tuesday Wednesday)) 是真的"')

chinese_format.kif 1973-1975
s__documentation(s__inList__m,s__EnglishLanguage,'"The analog of element and instance for Lists. (inList ?OBJ ?LIST) means that ?OBJ is in the List ?LIST. For example, (inList Tuesday (ListFn Monday Tuesday Wednesday)) would be true."')

Merge.kif 3037-3039
s__domain(s__inList__m,n__1,s__Entity)

Merge.kif 3034-3034 The number 1 argument of in list is an instance of entity
s__domain(s__inList__m,n__2,s__List)

Merge.kif 3035-3035 The number 2 argument of in list is an instance of list
s__instance(s__inList__m,s__AsymmetricRelation)

s__instance(s__AsymmetricRelation,s__Class)

Merge.kif 3032-3032 in list is an instance of asymmetric relation
s__instance(s__inList__m,s__BinaryPredicate)

s__instance(s__BinaryPredicate,s__Class)

Merge.kif 3030-3030 in list is an instance of binary predicate
s__instance(s__IrreflexiveRelation,s__Class)

s__instance(s__inList__m,s__IrreflexiveRelation)

Merge.kif 3031-3031 in list is an instance of irreflexive relation
s__instance(s__inList__m,s__PartialValuedRelation)

s__instance(s__PartialValuedRelation,s__Class)

Merge.kif 3033-3033 in list is an instance of partial valued relation

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


s__format(s__ChineseLanguage,s__inList__m,'"%1 %n 是 %2 的 member"')

chinese_format.kif 131-131
s__format(s__EnglishLanguage,s__inList__m,'"%1 is %n a member of %2"')

english_format.kif 132-132
s__subrelation(s__albumTrack__m,s__inList__m)

Music.kif 330-330 album track is a subrelation of in list
s__termFormat(s__ChineseLanguage,s__inList__m,'"在列表中"')

domainEnglishFormat.kif 30180-30180
s__termFormat(s__ChineseLanguage,s__inList__m,'"在列表内"')

chinese_format.kif 132-132
s__termFormat(s__ChineseTraditionalLanguage,s__inList__m,'"在列表中"')

domainEnglishFormat.kif 30179-30179
s__termFormat(s__EnglishLanguage,s__inList__m,'"in list"')

domainEnglishFormat.kif 30178-30178

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


( ! [V__A,V__L,V__N] :
   (((s__instance(V__A,s__RealNumber) &
         s__instance(V__L,s__List))
       =>
       ((((V__A = s__AverageFn(V__L))
           &
           s__inList(V__N,V__L))
       =>
       (s__instance(V__N,s__Number)))))
)
)

Merge.kif 3210-3214
( ! [V__SPEED,V__TIME,V__PLACE,V__SPEEDLIST] :
   (((s__instance(V__SPEED,s__FunctionQuantity) &
         s__instance(V__TIME,s__TimeInterval) &
         s__instance(V__PLACE,s__GeographicArea) &
         s__instance(V__SPEEDLIST,s__List))
       =>
       ((((V__SPEEDLIST = s__Mean3SecondWindSpeedListFn(V__PLACE,V__TIME))
           &
           s__inList(V__SPEED,V__SPEEDLIST))
       =>
       (( ? [V__TIMELIST, V__INT] :
           ((s__instance(V__TIMELIST,s__ConsecutiveTimeIntervalList) &
               s__instance(V__INT,s__TimeInterval) &
               ((V__TIMELIST = s__TimeIntervalListFn(V__TIME,s__MeasureFn(n__3,s__SecondDuration)))
               &
               s__inList(V__INT,V__TIMELIST)
             &
             (V__SPEED = s__Mean3SecondWindSpeedFn(V__PLACE,V__INT))))))))))
)
)

Weather.kif 1998-2010
( ! [V__SPEED,V__TIME,V__PLACE,V__SPEEDLIST] :
   (((s__instance(V__TIME,s__TimeInterval) &
         s__instance(V__PLACE,s__GeographicArea) &
         s__instance(V__SPEEDLIST,s__List))
       =>
       ((((V__SPEEDLIST = s__Mean3SecondWindSpeedListFn(V__PLACE,V__TIME))
           &
           s__inList(V__SPEED,V__SPEEDLIST))
       =>
       (s__instance(V__SPEED,s__FunctionQuantity)))))
)
)

Weather.kif 1991-1996
( ! [V__ROW5,V__ROW3,V__ATTR,V__ROW4,V__ROW2,V__CLASS] :
   (((s__instance(V__ROW5,s__Attribute) &
         s__instance(V__ROW3,s__Attribute) &
         s__instance(V__ROW4,s__Attribute) &
         s__instance(V__ROW2,s__Attribute) &
         s__subclass(V__CLASS,s__Attribute) &
         s__instance(V__CLASS,s__Class))
       =>
       (((s__exhaustiveAttribute__5(V__CLASS,V__ROW2,V__ROW3,V__ROW4,V__ROW5)
           &
           s__inList(V__ATTR,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5)))
     =>
     (s__instance(V__ATTR,V__CLASS)))))
)
)

( ! [V__ATTR,V__ROW2,V__CLASS] :
   (((s__instance(V__ROW2,s__Attribute) &
         s__subclass(V__CLASS,s__Attribute) &
         s__instance(V__CLASS,s__Class))
       =>
       (((s__exhaustiveAttribute__2(V__CLASS,V__ROW2)
           &
           s__inList(V__ATTR,s__ListFn__1Fn(V__ROW2)))
     =>
     (s__instance(V__ATTR,V__CLASS)))))
)
)

( ! [V__ROW5,V__ROW6,V__ROW3,V__ATTR,V__ROW4,V__ROW2,V__CLASS] :
   (((s__instance(V__ROW5,s__Attribute) &
         s__instance(V__ROW6,s__Attribute) &
         s__instance(V__ROW3,s__Attribute) &
         s__instance(V__ROW4,s__Attribute) &
         s__instance(V__ROW2,s__Attribute) &
         s__subclass(V__CLASS,s__Attribute) &
         s__instance(V__CLASS,s__Class))
       =>
       (((s__exhaustiveAttribute__6(V__CLASS,V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
           &
           s__inList(V__ATTR,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)))
     =>
     (s__instance(V__ATTR,V__CLASS)))))
)
)

( ! [V__ROW3,V__ATTR,V__ROW4,V__ROW2,V__CLASS] :
   (((s__instance(V__ROW3,s__Attribute) &
         s__instance(V__ROW4,s__Attribute) &
         s__instance(V__ROW2,s__Attribute) &
         s__subclass(V__CLASS,s__Attribute) &
         s__instance(V__CLASS,s__Class))
       =>
       (((s__exhaustiveAttribute__4(V__CLASS,V__ROW2,V__ROW3,V__ROW4)
           &
           s__inList(V__ATTR,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4)))
     =>
     (s__instance(V__ATTR,V__CLASS)))))
)
)

( ! [V__ROW3,V__ATTR,V__ROW2,V__CLASS] :
   (((s__instance(V__ROW3,s__Attribute) &
         s__instance(V__ROW2,s__Attribute) &
         s__subclass(V__CLASS,s__Attribute) &
         s__instance(V__CLASS,s__Class))
       =>
       (((s__exhaustiveAttribute__3(V__CLASS,V__ROW2,V__ROW3)
           &
           s__inList(V__ATTR,s__ListFn__2Fn(V__ROW2,V__ROW3)))
     =>
     (s__instance(V__ATTR,V__CLASS)))))
)
)

Merge.kif 504-508
( ! [V__ROW5,V__ROW6,V__ROW3,V__ATTR,V__ROW4,V__ROW2,V__CLASS] :
   (((s__instance(V__ROW5,s__Attribute) &
         s__instance(V__ROW6,s__Attribute) &
         s__instance(V__ROW3,s__Attribute) &
         s__instance(V__ROW4,s__Attribute) &
         s__instance(V__ROW2,s__Attribute) &
         s__subclass(V__CLASS,s__Attribute))
       =>
       (((s__exhaustiveAttribute__6(V__CLASS,V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
           &
           s__inList(V__ATTR,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)))
     =>
     (s__instance(V__ATTR,s__Attribute)))))
)
)

( ! [V__ROW5,V__ROW3,V__ATTR,V__ROW4,V__ROW2,V__CLASS] :
   (((s__instance(V__ROW5,s__Attribute) &
         s__instance(V__ROW3,s__Attribute) &
         s__instance(V__ROW4,s__Attribute) &
         s__instance(V__ROW2,s__Attribute) &
         s__subclass(V__CLASS,s__Attribute))
       =>
       (((s__exhaustiveAttribute__5(V__CLASS,V__ROW2,V__ROW3,V__ROW4,V__ROW5)
           &
           s__inList(V__ATTR,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5)))
     =>
     (s__instance(V__ATTR,s__Attribute)))))
)
)

( ! [V__ATTR,V__ROW2,V__CLASS] :
   (((s__instance(V__ROW2,s__Attribute) &
         s__subclass(V__CLASS,s__Attribute))
       =>
       (((s__exhaustiveAttribute__2(V__CLASS,V__ROW2)
           &
           s__inList(V__ATTR,s__ListFn__1Fn(V__ROW2)))
     =>
     (s__instance(V__ATTR,s__Attribute)))))
)
)

( ! [V__ROW3,V__ATTR,V__ROW4,V__ROW2,V__CLASS] :
   (((s__instance(V__ROW3,s__Attribute) &
         s__instance(V__ROW4,s__Attribute) &
         s__instance(V__ROW2,s__Attribute) &
         s__subclass(V__CLASS,s__Attribute))
       =>
       (((s__exhaustiveAttribute__4(V__CLASS,V__ROW2,V__ROW3,V__ROW4)
           &
           s__inList(V__ATTR,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4)))
     =>
     (s__instance(V__ATTR,s__Attribute)))))
)
)

( ! [V__ROW3,V__ATTR,V__ROW2,V__CLASS] :
   (((s__instance(V__ROW3,s__Attribute) &
         s__instance(V__ROW2,s__Attribute) &
         s__subclass(V__CLASS,s__Attribute))
       =>
       (((s__exhaustiveAttribute__3(V__CLASS,V__ROW2,V__ROW3)
           &
           s__inList(V__ATTR,s__ListFn__2Fn(V__ROW2,V__ROW3)))
     =>
     (s__instance(V__ATTR,s__Attribute)))))
)
)

Merge.kif 498-502
( ! [V__S,V__U,V__E,V__CO,V__L] :
   (((s__subclass(V__S,s__Substance) &
         s__instance(V__U,s__UnitOfMass) &
         s__instance(V__CO,s__CorpuscularObject) &
         s__instance(V__L,s__List))
       =>
       (((s__inList(V__E,V__L)
           &
           (V__L = s__AmountsFn(V__S,V__CO,V__U)))
       =>
       (s__instance(V__E,s__RationalNumber)))))
)
)

Merge.kif 7368-7373
( ! [V__RESULTS,V__ITEM] :
   (((s__inList(V__ITEM,V__RESULTS)
       &
       s__instance(V__RESULTS,s__SRPResults))
     =>
     (( ? [V__SRP] :
         ((s__instance(V__SRP,s__SearchResultsPage) &
             s__component(V__RESULTS,V__SRP))))))
)
)

UXExperimentalTerms.kif 2701-2708
( ! [V__RESULTS,V__ITEM] :
   (((s__inList(V__ITEM,V__RESULTS)
       &
       s__instance(V__RESULTS,s__SRPResults))
     =>
     ((s__instance(V__ITEM,s__WebListing) |
         s__instance(V__ITEM,s__WebPage))))
   )
)

UXExperimentalTerms.kif 2693-2699
( ! [V__TIME,V__Time,V__LIST] :
   (((s__instance(V__LIST,s__ConsecutiveTimeIntervalList) &
         s__inList(V__TIME,V__LIST))
     =>
     (s__instance(V__Time,s__TimeInterval)))
   )
)

Weather.kif 1928-1932
( ! [V__LIST,V__M] :
   (((s__instance(V__LIST,s__MeasuringList) &
         s__inList(V__M,V__LIST))
     =>
     (s__instance(V__M,s__Measuring)))
   )
)

Weather.kif 1715-1719
( ! [V__R,V__LIST] :
   (((s__instance(V__LIST,s__MeasuringResultList) &
         s__inList(V__R,V__LIST))
     =>
     (s__instance(V__R,s__PhysicalQuantity)))
   )
)

Weather.kif 1783-1787
( ! [V__LIST,V__M] :
   (((s__instance(V__LIST,s__MeasuringSurfaceWindSpeedList) &
         s__inList(V__M,V__LIST))
     =>
     (s__instance(V__M,s__SurfaceWindSpeedMeasuring)))
   )
)

Weather.kif 1749-1753
( ! [V__LIST,V__NUM] :
   (((s__instance(V__LIST,s__NumberList) &
         s__inList(V__NUM,V__LIST))
     =>
     (s__instance(V__NUM,s__Number)))
   )
)

Weather.kif 1818-1822
( ! [V__AGENT,V__OBJ,V__ROW2] :
   (((s__instance(V__AGENT,s__CognitiveAgent) &
         s__instance(V__ROW2,s__Agent))
       =>
       (((s__instance(s__enemy__m,s__IntentionalRelation) &
             s__enemy(V__AGENT,V__ROW2)
           &
           s__inList(V__OBJ,s__ListFn__1Fn(V__ROW2)))
     =>
     (s__inScopeOfInterest(V__AGENT,V__OBJ)))))
)
)

( ! [V__AGENT,V__OBJ,V__ROW2] :
   (((s__instance(V__AGENT,s__CognitiveAgent) &
         s__instance(V__ROW2,s__CognitiveAgent))
       =>
       (((s__instance(s__approves__m,s__IntentionalRelation) &
             s__approves(V__AGENT,V__ROW2)
           &
           s__inList(V__OBJ,s__ListFn__1Fn(V__ROW2)))
     =>
     (s__inScopeOfInterest(V__AGENT,V__OBJ)))))
)
)

( ! [V__AGENT,V__OBJ,V__ROW2] :
   (((s__instance(V__AGENT,s__Human) &
         s__instance(V__ROW2,s__Human))
       =>
       (((s__instance(s__domesticPartner__m,s__IntentionalRelation) &
             s__domesticPartner(V__AGENT,V__ROW2)
           &
           s__inList(V__OBJ,s__ListFn__1Fn(V__ROW2)))
     =>
     (s__inScopeOfInterest(V__AGENT,V__OBJ)))))
)
)

( ! [V__AGENT,V__OBJ,V__ROW3,V__ROW2] :
   (((s__instance(V__AGENT,s__CognitiveAgent) &
         s__instance(V__ROW3,s__Formula) &
         s__instance(V__ROW2,s__Formula))
       =>
       (((s__instance(s__prefers__m,s__IntentionalRelation) &
             s__prefers(V__AGENT,V__ROW2,V__ROW3)
           &
           s__inList(V__OBJ,s__ListFn__2Fn(V__ROW2,V__ROW3)))
     =>
     (s__inScopeOfInterest(V__AGENT,V__OBJ)))))
)
)

( ! [V__AGENT,V__OBJ,V__ROW2] :
   ((s__instance(V__AGENT,s__CognitiveAgent) =>
       (((s__instance(s__inScopeOfInterest__m,s__IntentionalRelation) &
             s__inScopeOfInterest(V__AGENT,V__ROW2)
           &
           s__inList(V__OBJ,s__ListFn__1Fn(V__ROW2)))
     =>
     (s__inScopeOfInterest(V__AGENT,V__OBJ)))))
)
)

( ! [V__AGENT,V__OBJ,V__ROW2] :
   (((s__instance(V__AGENT,s__CognitiveAgent) &
         s__instance(V__ROW2,s__Formula))
       =>
       (((s__instance(s__considers__m,s__IntentionalRelation) &
             s__considers(V__AGENT,V__ROW2)
           &
           s__inList(V__OBJ,s__ListFn__1Fn(V__ROW2)))
     =>
     (s__inScopeOfInterest(V__AGENT,V__OBJ)))))
)
)

( ! [V__AGENT,V__OBJ,V__ROW2] :
   (((s__instance(V__AGENT,s__CognitiveAgent) &
         s__instance(V__ROW2,s__Physical))
       =>
       (((s__instance(s__needs__m,s__IntentionalRelation) &
             s__needs(V__AGENT,V__ROW2)
           &
           s__inList(V__OBJ,s__ListFn__1Fn(V__ROW2)))
     =>
     (s__inScopeOfInterest(V__AGENT,V__OBJ)))))
)
)

( ! [V__AGENT,V__OBJ,V__ROW2] :
   (((s__instance(V__AGENT,s__CognitiveAgent) &
         s__instance(V__ROW2,s__Formula))
       =>
       (((s__instance(s__knows__m,s__IntentionalRelation) &
             s__knows(V__AGENT,V__ROW2)
           &
           s__inList(V__OBJ,s__ListFn__1Fn(V__ROW2)))
     =>
     (s__inScopeOfInterest(V__AGENT,V__OBJ)))))
)
)

( ! [V__AGENT,V__OBJ,V__ROW2] :
   (((s__instance(V__AGENT,s__CognitiveAgent) &
         s__subclass(V__ROW2,s__IntentionalProcess))
       =>
       (((s__instance(s__enjoys__m,s__IntentionalRelation) &
             s__enjoys(V__AGENT,V__ROW2)
           &
           s__inList(V__OBJ,s__ListFn__1Fn(V__ROW2)))
     =>
     (s__inScopeOfInterest(V__AGENT,V__OBJ)))))
)
)

( ! [V__AGENT,V__OBJ,V__ROW2] :
   (((s__instance(V__AGENT,s__CognitiveAgent) &
         s__instance(V__ROW2,s__Object))
       =>
       (((s__instance(s__dislikes__m,s__IntentionalRelation) &
             s__dislikes(V__AGENT,V__ROW2)
           &
           s__inList(V__OBJ,s__ListFn__1Fn(V__ROW2)))
     =>
     (s__inScopeOfInterest(V__AGENT,V__OBJ)))))
)
)

( ! [V__AGENT,V__OBJ,V__ROW2] :
   (((s__instance(V__AGENT,s__ServiceProcess) &
         s__instance(V__AGENT,s__CognitiveAgent) &
         s__instance(V__ROW2,s__CognitiveAgent))
       =>
       (((s__instance(s__serviceRecipient__m,s__IntentionalRelation) &
             s__serviceRecipient(V__AGENT,V__ROW2)
           &
           s__inList(V__OBJ,s__ListFn__1Fn(V__ROW2)))
     =>
     (s__inScopeOfInterest(V__AGENT,V__OBJ)))))
)
)

( ! [V__AGENT,V__OBJ,V__ROW2] :
   (((s__instance(V__AGENT,s__Human) &
         s__instance(V__ROW2,s__Human))
       =>
       (((s__instance(s__cohabitant__m,s__IntentionalRelation) &
             s__cohabitant(V__AGENT,V__ROW2)
           &
           s__inList(V__OBJ,s__ListFn__1Fn(V__ROW2)))
     =>
     (s__inScopeOfInterest(V__AGENT,V__OBJ)))))
)
)

( ! [V__AGENT,V__OBJ,V__ROW2] :
   (((s__instance(V__AGENT,s__CognitiveAgent) &
         s__instance(V__ROW2,s__Formula))
       =>
       (((s__instance(s__doubts__m,s__IntentionalRelation) &
             s__doubts(V__AGENT,V__ROW2)
           &
           s__inList(V__OBJ,s__ListFn__1Fn(V__ROW2)))
     =>
     (s__inScopeOfInterest(V__AGENT,V__OBJ)))))
)
)

( ! [V__AGENT,V__OBJ,V__ROW2] :
   ((s__instance(V__AGENT,s__CognitiveAgent) =>
       (((s__instance(s__lacks__m,s__IntentionalRelation) &
             s__lacks(V__AGENT,V__ROW2)
           &
           s__inList(V__OBJ,s__ListFn__1Fn(V__ROW2)))
     =>
     (s__inScopeOfInterest(V__AGENT,V__OBJ)))))
)
)

( ! [V__AGENT,V__OBJ,V__ROW2] :
   (((s__instance(V__AGENT,s__CognitiveAgent) &
         s__instance(V__ROW2,s__Physical))
       =>
       (((s__instance(s__wants__m,s__IntentionalRelation) &
             s__wants(V__AGENT,V__ROW2)
           &
           s__inList(V__OBJ,s__ListFn__1Fn(V__ROW2)))
     =>
     (s__inScopeOfInterest(V__AGENT,V__OBJ)))))
)
)

( ! [V__AGENT,V__OBJ,V__ROW2] :
   (((s__instance(V__AGENT,s__CognitiveAgent) &
         s__instance(V__ROW2,s__Formula))
       =>
       (((s__instance(s__desires__m,s__IntentionalRelation) &
             s__desires(V__AGENT,V__ROW2)
           &
           s__inList(V__OBJ,s__ListFn__1Fn(V__ROW2)))
     =>
     (s__inScopeOfInterest(V__AGENT,V__OBJ)))))
)
)

( ! [V__AGENT,V__OBJ,V__ROW2] :
   (((s__instance(V__AGENT,s__Human) &
         s__instance(V__ROW2,s__Human))
       =>
       (((s__instance(s__friend__m,s__IntentionalRelation) &
             s__friend(V__AGENT,V__ROW2)
           &
           s__inList(V__OBJ,s__ListFn__1Fn(V__ROW2)))
     =>
     (s__inScopeOfInterest(V__AGENT,V__OBJ)))))
)
)

( ! [V__AGENT,V__OBJ,V__ROW2] :
   (((s__instance(V__AGENT,s__CognitiveAgent) &
         s__instance(V__ROW2,s__Formula))
       =>
       (((s__instance(s__believes__m,s__IntentionalRelation) &
             s__believes(V__AGENT,V__ROW2)
           &
           s__inList(V__OBJ,s__ListFn__1Fn(V__ROW2)))
     =>
     (s__inScopeOfInterest(V__AGENT,V__OBJ)))))
)
)

( ! [V__AGENT,V__OBJ,V__ROW2] :
   (((s__instance(V__AGENT,s__CognitiveAgent) &
         s__instance(V__ROW2,s__Formula))
       =>
       (((s__instance(s__disapproves__m,s__IntentionalRelation) &
             s__disapproves(V__AGENT,V__ROW2)
           &
           s__inList(V__OBJ,s__ListFn__1Fn(V__ROW2)))
     =>
     (s__inScopeOfInterest(V__AGENT,V__OBJ)))))
)
)

( ! [V__AGENT,V__OBJ,V__ROW2] :
   (((s__instance(V__AGENT,s__ServiceProcess) &
         s__instance(V__AGENT,s__CognitiveAgent) &
         s__instance(V__ROW2,s__CognitiveAgent))
       =>
       (((s__instance(s__serviceProvider__m,s__IntentionalRelation) &
             s__serviceProvider(V__AGENT,V__ROW2)
           &
           s__inList(V__OBJ,s__ListFn__1Fn(V__ROW2)))
     =>
     (s__inScopeOfInterest(V__AGENT,V__OBJ)))))
)
)

Merge.kif 2618-2623
( ! [V__PLACE,V__LIST,V__M] :
   (((s__instance(V__PLACE,s__GeographicArea) &
         s__instance(V__LIST,s__MeasuringList) &
         s__instance(V__M,s__Process))
       =>
       (((s__locationMeasuringList(V__LIST,V__PLACE)
           &
           s__inList(V__M,V__LIST))
       =>
       ((s__instance(V__M,s__Measuring) &
           s__eventLocated(V__M,V__PLACE))))))
)
)

Weather.kif 1768-1774
( ! [V__LIST,V__M,V__DUR] :
   (((s__instance(V__LIST,s__MeasuringList) &
         s__instance(V__M,s__Physical) &
         s__instance(V__DUR,s__TimeDuration))
       =>
       (((s__measuringListInterval(V__LIST,V__DUR)
           &
           s__inList(V__M,V__LIST))
       =>
       (s__duration(s__WhenFn(V__M)
      ,V__DUR)))))
)
)

Weather.kif 1859-1863
( ! [V__OBJ1,V__OBJ2,V__ROW3,V__ROW4,V__ROW2,V__ATTR1,V__ATTR2] :
   (((s__instance(V__OBJ1,s__Object) &
         s__instance(V__OBJ2,s__Object) &
         s__instance(V__ROW3,s__Attribute) &
         s__instance(V__ROW4,s__Attribute) &
         s__instance(V__ROW2,s__Attribute) &
         s__instance(V__ATTR1,s__PositionalAttribute) &
         s__instance(V__ATTR2,s__PositionalAttribute))
       =>
       (((s__orientation(V__OBJ1,V__OBJ2,V__ATTR1)
           &
           s__contraryAttribute__3(V__ROW2,V__ROW3,V__ROW4)
         &
         s__inList(V__ATTR1,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4))
     &
     s__inList(V__ATTR2,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4))
&
~((V__ATTR1 = V__ATTR2)))
=>
(~(s__orientation(V__OBJ1,V__OBJ2,V__ATTR2))))))
)
)

( ! [V__ROW5,V__OBJ1,V__ROW6,V__OBJ2,V__ROW3,V__ROW4,V__ROW2,V__ATTR1,V__ATTR2] :
   (((s__instance(V__ROW5,s__Attribute) &
         s__instance(V__OBJ1,s__Object) &
         s__instance(V__ROW6,s__Attribute) &
         s__instance(V__OBJ2,s__Object) &
         s__instance(V__ROW3,s__Attribute) &
         s__instance(V__ROW4,s__Attribute) &
         s__instance(V__ROW2,s__Attribute) &
         s__instance(V__ATTR1,s__PositionalAttribute) &
         s__instance(V__ATTR2,s__PositionalAttribute))
       =>
       (((s__orientation(V__OBJ1,V__OBJ2,V__ATTR1)
           &
           s__contraryAttribute__5(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
         &
         s__inList(V__ATTR1,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6))
     &
     s__inList(V__ATTR2,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6))
&
~((V__ATTR1 = V__ATTR2)))
=>
(~(s__orientation(V__OBJ1,V__OBJ2,V__ATTR2))))))
)
)

( ! [V__ROW5,V__OBJ1,V__OBJ2,V__ROW3,V__ROW4,V__ROW2,V__ATTR1,V__ATTR2] :
   (((s__instance(V__ROW5,s__Attribute) &
         s__instance(V__OBJ1,s__Object) &
         s__instance(V__OBJ2,s__Object) &
         s__instance(V__ROW3,s__Attribute) &
         s__instance(V__ROW4,s__Attribute) &
         s__instance(V__ROW2,s__Attribute) &
         s__instance(V__ATTR1,s__PositionalAttribute) &
         s__instance(V__ATTR2,s__PositionalAttribute))
       =>
       (((s__orientation(V__OBJ1,V__OBJ2,V__ATTR1)
           &
           s__contraryAttribute__4(V__ROW2,V__ROW3,V__ROW4,V__ROW5)
         &
         s__inList(V__ATTR1,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5))
     &
     s__inList(V__ATTR2,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5))
&
~((V__ATTR1 = V__ATTR2)))
=>
(~(s__orientation(V__OBJ1,V__OBJ2,V__ATTR2))))))
)
)

( ! [V__OBJ1,V__OBJ2,V__ROW3,V__ROW2,V__ATTR1,V__ATTR2] :
   (((s__instance(V__OBJ1,s__Object) &
         s__instance(V__OBJ2,s__Object) &
         s__instance(V__ROW3,s__Attribute) &
         s__instance(V__ROW2,s__Attribute) &
         s__instance(V__ATTR1,s__PositionalAttribute) &
         s__instance(V__ATTR2,s__PositionalAttribute))
       =>
       (((s__orientation(V__OBJ1,V__OBJ2,V__ATTR1)
           &
           s__contraryAttribute__2(V__ROW2,V__ROW3)
         &
         s__inList(V__ATTR1,s__ListFn__2Fn(V__ROW2,V__ROW3))
     &
     s__inList(V__ATTR2,s__ListFn__2Fn(V__ROW2,V__ROW3))
&
~((V__ATTR1 = V__ATTR2)))
=>
(~(s__orientation(V__OBJ1,V__OBJ2,V__ATTR2))))))
)
)

( ! [V__OBJ1,V__OBJ2,V__ROW2,V__ATTR1,V__ATTR2] :
   (((s__instance(V__OBJ1,s__Object) &
         s__instance(V__OBJ2,s__Object) &
         s__instance(V__ROW2,s__Attribute) &
         s__instance(V__ATTR1,s__PositionalAttribute) &
         s__instance(V__ATTR2,s__PositionalAttribute))
       =>
       (((s__orientation(V__OBJ1,V__OBJ2,V__ATTR1)
           &
           s__contraryAttribute__1(V__ROW2)
         &
         s__inList(V__ATTR1,s__ListFn__1Fn(V__ROW2))
     &
     s__inList(V__ATTR2,s__ListFn__1Fn(V__ROW2))
&
~((V__ATTR1 = V__ATTR2)))
=>
(~(s__orientation(V__OBJ1,V__OBJ2,V__ATTR2))))))
)
)

Merge.kif 16256-16264
( ! [V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__Process1,V__ROW2,V__Process2,V__Number1,V__Number2] :
   (((s__instance(V__Process1,s__Physical) &
         s__instance(V__Process2,s__Physical) &
         s__instance(V__Number1,s__PositiveInteger) &
         s__instance(V__Number2,s__PositiveInteger))
       =>
       (((s__processList__5(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
           &
           s__inList(V__Process1,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6))
       &
       s__inList(V__Process2,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6))
   &
   (s__ListOrderFn(s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
  ,V__Number1)
= V__Process1)
&
(s__ListOrderFn(s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
,V__Number2)
= V__Process2)
&
s__lessThan(V__Number1,V__Number2))
=>
(s__earlier(s__WhenFn(V__Process1)
,s__WhenFn(V__Process2))))))
)
)

( ! [V__Process1,V__ROW2,V__Process2,V__Number1,V__Number2] :
   (((s__instance(V__Process1,s__Physical) &
         s__instance(V__Process2,s__Physical) &
         s__instance(V__Number1,s__PositiveInteger) &
         s__instance(V__Number2,s__PositiveInteger))
       =>
       (((s__processList__1(V__ROW2)
           &
           s__inList(V__Process1,s__ListFn__1Fn(V__ROW2))
       &
       s__inList(V__Process2,s__ListFn__1Fn(V__ROW2))
   &
   (s__ListOrderFn(s__ListFn__1Fn(V__ROW2)
  ,V__Number1)
= V__Process1)
&
(s__ListOrderFn(s__ListFn__1Fn(V__ROW2)
,V__Number2)
= V__Process2)
&
s__lessThan(V__Number1,V__Number2))
=>
(s__earlier(s__WhenFn(V__Process1)
,s__WhenFn(V__Process2))))))
)
)

( ! [V__ROW3,V__ROW4,V__Process1,V__ROW2,V__Process2,V__Number1,V__Number2] :
   (((s__instance(V__Process1,s__Physical) &
         s__instance(V__Process2,s__Physical) &
         s__instance(V__Number1,s__PositiveInteger) &
         s__instance(V__Number2,s__PositiveInteger))
       =>
       (((s__processList__3(V__ROW2,V__ROW3,V__ROW4)
           &
           s__inList(V__Process1,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4))
       &
       s__inList(V__Process2,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4))
   &
   (s__ListOrderFn(s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
  ,V__Number1)
= V__Process1)
&
(s__ListOrderFn(s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
,V__Number2)
= V__Process2)
&
s__lessThan(V__Number1,V__Number2))
=>
(s__earlier(s__WhenFn(V__Process1)
,s__WhenFn(V__Process2))))))
)
)

( ! [V__ROW3,V__Process1,V__ROW2,V__Process2,V__Number1,V__Number2] :
   (((s__instance(V__Process1,s__Physical) &
         s__instance(V__Process2,s__Physical) &
         s__instance(V__Number1,s__PositiveInteger) &
         s__instance(V__Number2,s__PositiveInteger))
       =>
       (((s__processList__2(V__ROW2,V__ROW3)
           &
           s__inList(V__Process1,s__ListFn__2Fn(V__ROW2,V__ROW3))
       &
       s__inList(V__Process2,s__ListFn__2Fn(V__ROW2,V__ROW3))
   &
   (s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
  ,V__Number1)
= V__Process1)
&
(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__Number2)
= V__Process2)
&
s__lessThan(V__Number1,V__Number2))
=>
(s__earlier(s__WhenFn(V__Process1)
,s__WhenFn(V__Process2))))))
)
)

( ! [V__ROW5,V__ROW3,V__ROW4,V__Process1,V__ROW2,V__Process2,V__Number1,V__Number2] :
   (((s__instance(V__Process1,s__Physical) &
         s__instance(V__Process2,s__Physical) &
         s__instance(V__Number1,s__PositiveInteger) &
         s__instance(V__Number2,s__PositiveInteger))
       =>
       (((s__processList__4(V__ROW2,V__ROW3,V__ROW4,V__ROW5)
           &
           s__inList(V__Process1,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5))
       &
       s__inList(V__Process2,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5))
   &
   (s__ListOrderFn(s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5)
  ,V__Number1)
= V__Process1)
&
(s__ListOrderFn(s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5)
,V__Number2)
= V__Process2)
&
s__lessThan(V__Number1,V__Number2))
=>
(s__earlier(s__WhenFn(V__Process1)
,s__WhenFn(V__Process2))))))
)
)

QoSontology.kif 692-708
( ! [V__USER,V__ACCESSING,V__LIST] :
   (((s__instance(V__USER,s__Agent) &
         s__instance(V__ACCESSING,s__Process) &
         s__instance(V__LIST,s__List))
       =>
       (((s__viewedItemList(V__USER,V__LIST)
           &
           s__inList(V__ACCESSING,V__LIST))
       =>
       ((s__instance(V__ACCESSING,s__AccessingWebPage) &
           s__agent(V__ACCESSING,V__USER)
         &
         ( ? [V__DEST] :
           ((s__instance(V__DEST,s__WebPage) &
               s__destination(V__ACCESSING,s__WebPage)))))))))
)
)

UXExperimentalTerms.kif 961-971
( ! [V__LIST,V__ITEM] :
   ((s__instance(V__LIST,s__List) =>
       ((s__inList(V__ITEM,V__LIST)
         =>
         (( ? [V__NUMBER] :
             ((s__instance(V__NUMBER,s__PositiveInteger) &
                 (s__ListOrderFn(V__LIST,V__NUMBER)
                 = V__ITEM))))))))
)
)

Merge.kif 3041-3044

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


( ! [V__LASTPLACE,V__LIST1,V__AVERAGE] :
   (((s__instance(V__LASTPLACE,s__PositiveInteger) &
         s__instance(V__LIST1,s__List) &
         s__instance(V__AVERAGE,s__RealNumber))
       =>
       (((s__average(V__LIST1,V__AVERAGE)
           =>
           ( ? [V__LIST2] :
             ((s__instance(V__LIST2,s__List) &
                 ((s__ListLengthFn(V__LIST2)
                   = s__ListLengthFn(V__LIST1))
               &
               (s__ListOrderFn(V__LIST2,n__1)
               = s__ListOrderFn(V__LIST1,n__1))
           &
           ( ! [V__ITEMFROM2] :
             ((s__instance(V__ITEMFROM2,s__PositiveInteger) =>
                 ((s__inList(V__ITEMFROM2,V__LIST2)
                   =>
                   (( ? [V__POSITION, V__POSITIONMINUSONE, V__ITEMFROM1, V__PRIORFROM2] :
                       ((s__instance(V__POSITION,s__Number) &
                           s__instance(V__POSITIONMINUSONE,s__Number) &
                           s__instance(V__ITEMFROM1,s__PositiveInteger) &
                           s__instance(V__PRIORFROM2,s__PositiveInteger) &
                           (s__greaterThan(V__POSITION,n__1)
                           &
                           s__lessThanOrEqualTo(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 = s__SubtractionFn(V__POSITION,n__1))
             &
             (V__POSITIONMINUSONE = s__ListOrderFn(V__LIST2,V__PRIORFROM2))
           &
           (V__ITEMFROM2 = s__AdditionFn(V__ITEMFROM1,V__PRIORFROM2))))))))))))
&
(V__LASTPLACE = s__ListLengthFn(V__LIST2))
&
(V__AVERAGE = s__DivisionFn(s__ListOrderFn(V__LIST2,V__LASTPLACE)
,V__LASTPLACE)))))))
&
(( ? [V__LIST2] :
((s__instance(V__LIST2,s__List) &
((s__ListLengthFn(V__LIST2)
= s__ListLengthFn(V__LIST1))
&
(s__ListOrderFn(V__LIST2,n__1)
= s__ListOrderFn(V__LIST1,n__1))
&
( ! [V__ITEMFROM2] :
((s__instance(V__ITEMFROM2,s__PositiveInteger) =>
((s__inList(V__ITEMFROM2,V__LIST2)
=>
(( ? [V__POSITION, V__POSITIONMINUSONE, V__ITEMFROM1, V__PRIORFROM2] :
((s__instance(V__POSITION,s__Number) &
s__instance(V__POSITIONMINUSONE,s__Number) &
s__instance(V__ITEMFROM1,s__PositiveInteger) &
s__instance(V__PRIORFROM2,s__PositiveInteger) &
(s__greaterThan(V__POSITION,n__1)
&
s__lessThanOrEqualTo(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 = s__SubtractionFn(V__POSITION,n__1))
&
(V__POSITIONMINUSONE = s__ListOrderFn(V__LIST2,V__PRIORFROM2))
&
(V__ITEMFROM2 = s__AdditionFn(V__ITEMFROM1,V__PRIORFROM2))))))))))))
&
(V__LASTPLACE = s__ListLengthFn(V__LIST2))
&
(V__AVERAGE = s__DivisionFn(s__ListOrderFn(V__LIST2,V__LASTPLACE)
,V__LASTPLACE))))))
=>
s__average(V__LIST1,V__AVERAGE)))))
)
)

People.kif 289-310 A real number is an average of a list if and only if there exists another list such that length of the other list is equal to length of the list and 1th element of the other list is equal to 1th element of the list and for all a positive integer and a fourth positive integer is equal to length of the other list and the real number is equal to the fourth positive integerth element of the other list and the fourth positive integer
No TPTP formula. May not be expressible in strict first order. People.kif 415-446 The female life expectancy at birth of a geopolitical area and the year an integer is equal to a real number if and only if there exists a list such that the list is an instance of list and length of the list is an instance of another integer and for all the listITEM and the real number is an average of the list
No TPTP formula. May not be expressible in strict first order. People.kif 327-357 The life expectancy at birth of a geopolitical area and the year an integer is equal to a real number if and only if there exists a list such that the list is an instance of list and length of the list is an instance of another integer and for all the listITEM and the real number is an average of the list
No TPTP formula. May not be expressible in strict first order. People.kif 371-402 The male life expectancy at birth of a geopolitical area and the year an integer is equal to a real number if and only if there exists a list such that the list is an instance of list and length of the list is an instance of another integer and for all the listITEM and the real number is an average of the list
( ! [V__P,V__A] :
   (((s__instance(V__P,s__CognitiveAgent) &
         s__instance(V__A,s__Album))
       =>
       ((s__albumArtist(V__A,V__P)
         =>
         (( ? [V__R, V__M] :
             ((s__instance(V__M,s__Process) &
                 (s__instance(V__R,s__Recording) &
                   s__inList(V__R,V__A)
                 &
                 s__record(V__R,V__M)
               &
               s__agent(V__M,V__P)))))))))
)
)

Music.kif 278-285
( ! [V__N2,V__S,V__SI,V__U,V__CO,V__N] :
   (((s__instance(V__N2,s__RealNumber) &
         s__subclass(V__S,s__Substance) &
         s__instance(V__S,s__Class) &
         s__instance(V__SI,s__Object) &
         s__instance(V__U,s__UnitOfMass) &
         s__instance(V__CO,s__CorpuscularObject) &
         s__instance(V__N,s__RealNumber))
       =>
       (((s__amount(V__S,V__CO,s__MeasureFn(V__N,V__U))
         &
         s__instance(V__SI,V__S)
       &
       s__measure(V__SI,s__MeasureFn(V__N2,V__U))
   &
   s__part(V__SI,V__CO))
=>
(( ? [V__L] :
   ((s__instance(V__L,s__List) &
       (s__inList(s__MeasureFn(V__N2,V__U)
      ,V__L)
     &
     (V__L = s__AmountsFn(V__S,V__CO,V__U))
   &
   (V__N = s__ListSumFn(V__L))))))))))
)
)

Merge.kif 7382-7397
( ! [V__A,V__D,V__X,V__DS] :
   (((s__instance(V__A,s__Album) &
         s__subclass(V__D,s__DataStorageDevice) &
         s__instance(V__D,s__DataStorageDevice) &
         s__instance(V__D,s__Class) &
         s__subclass(V__DS,s__DataStorageDevice))
       =>
       ((((V__D = s__AlbumCopiesFn(V__A,V__DS))
           &
           s__instance(V__X,V__D))
       =>
       (( ! [V__S] :
           ((s__instance(V__S,s__Object) =>
               ((s__inList(V__S,V__A)
                 =>
                 (( ? [V__C] :
                     ((s__instance(V__C,s__ContentBearingObject) &
                         (s__copy(V__C,V__S)
                         &
                         s__stored(V__C,V__D)))))))))))))))
)
)

Music.kif 931-941
( ! [V__SPEED,V__TIME,V__PLACE,V__SPEEDLIST] :
   (((s__instance(V__SPEED,s__FunctionQuantity) &
         s__instance(V__TIME,s__TimeInterval) &
         s__instance(V__PLACE,s__GeographicArea) &
         s__instance(V__SPEEDLIST,s__List))
       =>
       ((((V__SPEEDLIST = s__Mean3SecondWindSpeedListFn(V__PLACE,V__TIME))
           &
           s__inList(V__SPEED,V__SPEEDLIST))
       =>
       (( ? [V__TIMELIST, V__INT] :
           ((s__instance(V__TIMELIST,s__ConsecutiveTimeIntervalList) &
               s__instance(V__INT,s__TimeInterval) &
               ((V__TIMELIST = s__TimeIntervalListFn(V__TIME,s__MeasureFn(n__3,s__SecondDuration)))
               &
               s__inList(V__INT,V__TIMELIST)
             &
             (V__SPEED = s__Mean3SecondWindSpeedFn(V__PLACE,V__INT))))))))))
)
)

Weather.kif 1998-2010
( ! [V__OBJ,V__NUM,V__PART] :
   (((s__instance(V__OBJ,s__DigitalDataStorageDevice) &
         s__part(V__PART,V__OBJ)
       &
       s__instance(V__PART,s__DigitalData))
     =>
     (( ? [V__SCHEME, V__LIST] :
         ((s__instance(V__SCHEME,s__CodeMap) &
             s__instance(V__LIST,s__List) &
             (s__codeMapping(V__SCHEME,V__PART,V__NUM)
             &
             s__represents(V__LIST,V__SCHEME)
           &
           (s__inList(V__NUM,V__LIST)
           =>
           (s__instance(V__NUM,s__BinaryNumber)))))))))
)
)

Media.kif 801-812
( ! [V__WH,V__SWH,V__WW] :
   (((s__instance(V__WH,s__LengthMeasure) &
         s__instance(V__SWH,s__RealNumber))
       =>
       (((s__instance(V__WW,s__WaterWave) &
             s__waveHeight(V__WW,V__WH))
         =>
         (( ? [V__LIST, V__WA, V__U] :
             ((s__instance(V__LIST,s__List) &
                 (s__inList(V__WH,V__LIST)
                 &
                 s__instance(V__WA,s__WaterArea) &
                 s__eventLocated(V__WW,V__WA)
               &
               s__instance(V__U,s__LengthMeasure) &
               s__significantWaveHeight(V__WA,s__WhenFn(V__WW)
            ,s__MeasureFn(V__SWH,V__U))
         &
         (V__SWH = s__MultiplicationFn(n__4,s__StandardDeviationFn(V__LIST)))))))))))
)
)

Weather.kif 1531-1546
( ! [V__LIST,V__AVERAGE] :
   (((s__instance(V__LIST,s__List) &
         s__instance(V__AVERAGE,s__RealNumber))
       =>
       ((s__average(V__LIST,V__AVERAGE)
         =>
         (( ! [V__LISTITEM] :
             ((s__inList(V__LISTITEM,V__LIST)
               =>
               (s__instance(V__LISTITEM,s__RealNumber)))))))))
)
)

Merge.kif 5171-5176
( ! [V__ELEMENT,V__ROW3,V__ROW2] :
   (((s__instance(V__ROW3,s__Attribute) &
         s__instance(V__ROW2,s__Attribute))
       =>
       ((s__contraryAttribute__2(V__ROW2,V__ROW3)
         =>
         ((s__inList(V__ELEMENT,s__ListFn__2Fn(V__ROW2,V__ROW3))
         =>
         (s__instance(V__ELEMENT,s__Attribute)))))))
)
)

( ! [V__ROW5,V__ELEMENT,V__ROW3,V__ROW4,V__ROW2] :
   (((s__instance(V__ROW5,s__Attribute) &
         s__instance(V__ROW3,s__Attribute) &
         s__instance(V__ROW4,s__Attribute) &
         s__instance(V__ROW2,s__Attribute))
       =>
       ((s__contraryAttribute__4(V__ROW2,V__ROW3,V__ROW4,V__ROW5)
         =>
         ((s__inList(V__ELEMENT,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5))
         =>
         (s__instance(V__ELEMENT,s__Attribute)))))))
)
)

( ! [V__ROW5,V__ROW6,V__ELEMENT,V__ROW3,V__ROW4,V__ROW2] :
   (((s__instance(V__ROW5,s__Attribute) &
         s__instance(V__ROW6,s__Attribute) &
         s__instance(V__ROW3,s__Attribute) &
         s__instance(V__ROW4,s__Attribute) &
         s__instance(V__ROW2,s__Attribute))
       =>
       ((s__contraryAttribute__5(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
         =>
         ((s__inList(V__ELEMENT,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6))
         =>
         (s__instance(V__ELEMENT,s__Attribute)))))))
)
)

( ! [V__ELEMENT,V__ROW3,V__ROW4,V__ROW2] :
   (((s__instance(V__ROW3,s__Attribute) &
         s__instance(V__ROW4,s__Attribute) &
         s__instance(V__ROW2,s__Attribute))
       =>
       ((s__contraryAttribute__3(V__ROW2,V__ROW3,V__ROW4)
         =>
         ((s__inList(V__ELEMENT,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4))
         =>
         (s__instance(V__ELEMENT,s__Attribute)))))))
)
)

( ! [V__ELEMENT,V__ROW2] :
   ((s__instance(V__ROW2,s__Attribute) =>
       ((s__contraryAttribute__1(V__ROW2)
         =>
         ((s__inList(V__ELEMENT,s__ListFn__1Fn(V__ROW2))
         =>
         (s__instance(V__ELEMENT,s__Attribute)))))))
)
)

Merge.kif 463-467
( ! [V__ROW3,V__ROW4,V__ROW2,V__CLASS] :
   (((s__instance(V__ROW3,s__Class) &
         s__instance(V__ROW4,s__Class) &
         s__instance(V__ROW2,s__Class) &
         s__instance(V__CLASS,s__Class))
       =>
       ((s__disjointDecomposition__4(V__CLASS,V__ROW2,V__ROW3,V__ROW4)
         =>
         (( ! [V__ITEM] :
             ((s__instance(V__ITEM,s__Class) =>
                 ((s__inList(V__ITEM,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4))
                 =>
                 (s__subclass(V__ITEM,V__CLASS)))))))))))
)
)

( ! [V__ROW3,V__ROW2,V__CLASS] :
   (((s__instance(V__ROW3,s__Class) &
         s__instance(V__ROW2,s__Class) &
         s__instance(V__CLASS,s__Class))
       =>
       ((s__disjointDecomposition__3(V__CLASS,V__ROW2,V__ROW3)
         =>
         (( ! [V__ITEM] :
             ((s__instance(V__ITEM,s__Class) =>
                 ((s__inList(V__ITEM,s__ListFn__2Fn(V__ROW2,V__ROW3))
                 =>
                 (s__subclass(V__ITEM,V__CLASS)))))))))))
)
)

( ! [V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__CLASS] :
   (((s__instance(V__ROW5,s__Class) &
         s__instance(V__ROW6,s__Class) &
         s__instance(V__ROW3,s__Class) &
         s__instance(V__ROW4,s__Class) &
         s__instance(V__ROW2,s__Class) &
         s__instance(V__CLASS,s__Class))
       =>
       ((s__disjointDecomposition__6(V__CLASS,V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
         =>
         (( ! [V__ITEM] :
             ((s__instance(V__ITEM,s__Class) =>
                 ((s__inList(V__ITEM,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6))
                 =>
                 (s__subclass(V__ITEM,V__CLASS)))))))))))
)
)

( ! [V__ROW5,V__ROW3,V__ROW4,V__ROW2,V__CLASS] :
   (((s__instance(V__ROW5,s__Class) &
         s__instance(V__ROW3,s__Class) &
         s__instance(V__ROW4,s__Class) &
         s__instance(V__ROW2,s__Class) &
         s__instance(V__CLASS,s__Class))
       =>
       ((s__disjointDecomposition__5(V__CLASS,V__ROW2,V__ROW3,V__ROW4,V__ROW5)
         =>
         (( ! [V__ITEM] :
             ((s__instance(V__ITEM,s__Class) =>
                 ((s__inList(V__ITEM,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5))
                 =>
                 (s__subclass(V__ITEM,V__CLASS)))))))))))
)
)

( ! [V__ROW2,V__CLASS] :
   (((s__instance(V__ROW2,s__Class) &
         s__instance(V__CLASS,s__Class))
       =>
       ((s__disjointDecomposition__2(V__CLASS,V__ROW2)
         =>
         (( ! [V__ITEM] :
             ((s__instance(V__ITEM,s__Class) =>
                 ((s__inList(V__ITEM,s__ListFn__1Fn(V__ROW2))
                 =>
                 (s__subclass(V__ITEM,V__CLASS)))))))))))
)
)

Merge.kif 2879-2884
( ! [V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__CLASS] :
   (((s__instance(V__ROW5,s__Class) &
         s__instance(V__ROW6,s__Class) &
         s__instance(V__ROW3,s__Class) &
         s__instance(V__ROW4,s__Class) &
         s__instance(V__ROW2,s__Class) &
         s__instance(V__CLASS,s__Class))
       =>
       ((s__disjointDecomposition__6(V__CLASS,V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
         =>
         (( ! [V__ITEM1, V__ITEM2] :
             (((s__instance(V__ITEM1,s__Class) &
                   s__instance(V__ITEM2,s__Class))
                 =>
                 (((s__inList(V__ITEM1,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6))
                   &
                   s__inList(V__ITEM2,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6))
               &
               ~((V__ITEM1 = V__ITEM2)))
             =>
             (s__disjoint(V__ITEM1,V__ITEM2)))))))))))
)
)

( ! [V__ROW2,V__CLASS] :
   (((s__instance(V__ROW2,s__Class) &
         s__instance(V__CLASS,s__Class))
       =>
       ((s__disjointDecomposition__2(V__CLASS,V__ROW2)
         =>
         (( ! [V__ITEM1, V__ITEM2] :
             (((s__instance(V__ITEM1,s__Class) &
                   s__instance(V__ITEM2,s__Class))
                 =>
                 (((s__inList(V__ITEM1,s__ListFn__1Fn(V__ROW2))
                   &
                   s__inList(V__ITEM2,s__ListFn__1Fn(V__ROW2))
               &
               ~((V__ITEM1 = V__ITEM2)))
             =>
             (s__disjoint(V__ITEM1,V__ITEM2)))))))))))
)
)

( ! [V__ROW3,V__ROW2,V__CLASS] :
   (((s__instance(V__ROW3,s__Class) &
         s__instance(V__ROW2,s__Class) &
         s__instance(V__CLASS,s__Class))
       =>
       ((s__disjointDecomposition__3(V__CLASS,V__ROW2,V__ROW3)
         =>
         (( ! [V__ITEM1, V__ITEM2] :
             (((s__instance(V__ITEM1,s__Class) &
                   s__instance(V__ITEM2,s__Class))
                 =>
                 (((s__inList(V__ITEM1,s__ListFn__2Fn(V__ROW2,V__ROW3))
                   &
                   s__inList(V__ITEM2,s__ListFn__2Fn(V__ROW2,V__ROW3))
               &
               ~((V__ITEM1 = V__ITEM2)))
             =>
             (s__disjoint(V__ITEM1,V__ITEM2)))))))))))
)
)

( ! [V__ROW5,V__ROW3,V__ROW4,V__ROW2,V__CLASS] :
   (((s__instance(V__ROW5,s__Class) &
         s__instance(V__ROW3,s__Class) &
         s__instance(V__ROW4,s__Class) &
         s__instance(V__ROW2,s__Class) &
         s__instance(V__CLASS,s__Class))
       =>
       ((s__disjointDecomposition__5(V__CLASS,V__ROW2,V__ROW3,V__ROW4,V__ROW5)
         =>
         (( ! [V__ITEM1, V__ITEM2] :
             (((s__instance(V__ITEM1,s__Class) &
                   s__instance(V__ITEM2,s__Class))
                 =>
                 (((s__inList(V__ITEM1,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5))
                   &
                   s__inList(V__ITEM2,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5))
               &
               ~((V__ITEM1 = V__ITEM2)))
             =>
             (s__disjoint(V__ITEM1,V__ITEM2)))))))))))
)
)

( ! [V__ROW3,V__ROW4,V__ROW2,V__CLASS] :
   (((s__instance(V__ROW3,s__Class) &
         s__instance(V__ROW4,s__Class) &
         s__instance(V__ROW2,s__Class) &
         s__instance(V__CLASS,s__Class))
       =>
       ((s__disjointDecomposition__4(V__CLASS,V__ROW2,V__ROW3,V__ROW4)
         =>
         (( ! [V__ITEM1, V__ITEM2] :
             (((s__instance(V__ITEM1,s__Class) &
                   s__instance(V__ITEM2,s__Class))
                 =>
                 (((s__inList(V__ITEM1,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4))
                   &
                   s__inList(V__ITEM2,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4))
               &
               ~((V__ITEM1 = V__ITEM2)))
             =>
             (s__disjoint(V__ITEM1,V__ITEM2)))))))))))
)
)

Merge.kif 2886-2895
( ! [V__ELEMENT,V__ROW2] :
   ((s__instance(V__ROW2,s__Class) =>
       ((s__disjointDecomposition__1(V__ROW2)
         =>
         ((s__inList(V__ELEMENT,s__ListFn__1Fn(V__ROW2))
         =>
         (s__instance(V__ELEMENT,s__Class)))))))
)
)

( ! [V__ROW5,V__ROW6,V__ELEMENT,V__ROW3,V__ROW4,V__ROW2] :
   (((s__instance(V__ROW5,s__Class) &
         s__instance(V__ROW6,s__Class) &
         s__instance(V__ROW3,s__Class) &
         s__instance(V__ROW4,s__Class) &
         s__instance(V__ROW2,s__Class))
       =>
       ((s__disjointDecomposition__5(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
         =>
         ((s__inList(V__ELEMENT,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6))
         =>
         (s__instance(V__ELEMENT,s__Class)))))))
)
)

( ! [V__ELEMENT,V__ROW3,V__ROW2] :
   (((s__instance(V__ROW3,s__Class) &
         s__instance(V__ROW2,s__Class))
       =>
       ((s__disjointDecomposition__2(V__ROW2,V__ROW3)
         =>
         ((s__inList(V__ELEMENT,s__ListFn__2Fn(V__ROW2,V__ROW3))
         =>
         (s__instance(V__ELEMENT,s__Class)))))))
)
)

( ! [V__ELEMENT,V__ROW3,V__ROW4,V__ROW2] :
   (((s__instance(V__ROW3,s__Class) &
         s__instance(V__ROW4,s__Class) &
         s__instance(V__ROW2,s__Class))
       =>
       ((s__disjointDecomposition__3(V__ROW2,V__ROW3,V__ROW4)
         =>
         ((s__inList(V__ELEMENT,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4))
         =>
         (s__instance(V__ELEMENT,s__Class)))))))
)
)

( ! [V__ROW5,V__ELEMENT,V__ROW3,V__ROW4,V__ROW2] :
   (((s__instance(V__ROW5,s__Class) &
         s__instance(V__ROW3,s__Class) &
         s__instance(V__ROW4,s__Class) &
         s__instance(V__ROW2,s__Class))
       =>
       ((s__disjointDecomposition__4(V__ROW2,V__ROW3,V__ROW4,V__ROW5)
         =>
         ((s__inList(V__ELEMENT,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5))
         =>
         (s__instance(V__ELEMENT,s__Class)))))))
)
)

Merge.kif 575-579
( ! [V__ELEMENT,V__ROW2,V__NUMBER] :
   (((s__instance(V__ROW2,s__Integer) &
         s__instance(V__NUMBER,s__Integer))
       =>
       (((s__GreatestCommonDivisorFn__1Fn(V__ROW2)
           = V__NUMBER)
         =>
         ((s__inList(V__ELEMENT,s__ListFn__1Fn(V__ROW2))
         =>
         (s__instance(V__ELEMENT,s__Number)))))))
)
)

( ! [V__ELEMENT,V__ROW3,V__ROW2,V__NUMBER] :
   (((s__instance(V__ROW3,s__Integer) &
         s__instance(V__ROW2,s__Integer) &
         s__instance(V__NUMBER,s__Integer))
       =>
       (((s__GreatestCommonDivisorFn__2Fn(V__ROW2,V__ROW3)
           = V__NUMBER)
         =>
         ((s__inList(V__ELEMENT,s__ListFn__2Fn(V__ROW2,V__ROW3))
         =>
         (s__instance(V__ELEMENT,s__Number)))))))
)
)

( ! [V__ROW5,V__ELEMENT,V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   (((s__instance(V__ROW5,s__Integer) &
         s__instance(V__ROW3,s__Integer) &
         s__instance(V__ROW4,s__Integer) &
         s__instance(V__ROW2,s__Integer) &
         s__instance(V__NUMBER,s__Integer))
       =>
       (((s__GreatestCommonDivisorFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5)
           = V__NUMBER)
         =>
         ((s__inList(V__ELEMENT,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5))
         =>
         (s__instance(V__ELEMENT,s__Number)))))))
)
)

( ! [V__ROW5,V__ROW6,V__ELEMENT,V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   (((s__instance(V__ROW5,s__Integer) &
         s__instance(V__ROW6,s__Integer) &
         s__instance(V__ROW3,s__Integer) &
         s__instance(V__ROW4,s__Integer) &
         s__instance(V__ROW2,s__Integer) &
         s__instance(V__NUMBER,s__Integer))
       =>
       (((s__GreatestCommonDivisorFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
           = V__NUMBER)
         =>
         ((s__inList(V__ELEMENT,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6))
         =>
         (s__instance(V__ELEMENT,s__Number)))))))
)
)

( ! [V__ELEMENT,V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   (((s__instance(V__ROW3,s__Integer) &
         s__instance(V__ROW4,s__Integer) &
         s__instance(V__ROW2,s__Integer) &
         s__instance(V__NUMBER,s__Integer))
       =>
       (((s__GreatestCommonDivisorFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
           = V__NUMBER)
         =>
         ((s__inList(V__ELEMENT,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4))
         =>
         (s__instance(V__ELEMENT,s__Number)))))))
)
)

Merge.kif 4716-4721
( ! [V__ROW5,V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   (((s__instance(V__ROW5,s__Integer) &
         s__instance(V__ROW3,s__Integer) &
         s__instance(V__ROW4,s__Integer) &
         s__instance(V__ROW2,s__Integer) &
         s__instance(V__NUMBER,s__Integer))
       =>
       (((s__GreatestCommonDivisorFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5)
           = V__NUMBER)
         =>
         (( ! [V__ELEMENT] :
             ((s__instance(V__ELEMENT,s__Integer) =>
                 ((s__inList(V__ELEMENT,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5))
                 =>
                 ((s__RemainderFn(V__ELEMENT,V__NUMBER)
                   = n__0)))))))))))
)
)

( ! [V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   (((s__instance(V__ROW5,s__Integer) &
         s__instance(V__ROW6,s__Integer) &
         s__instance(V__ROW3,s__Integer) &
         s__instance(V__ROW4,s__Integer) &
         s__instance(V__ROW2,s__Integer) &
         s__instance(V__NUMBER,s__Integer))
       =>
       (((s__GreatestCommonDivisorFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
           = V__NUMBER)
         =>
         (( ! [V__ELEMENT] :
             ((s__instance(V__ELEMENT,s__Integer) =>
                 ((s__inList(V__ELEMENT,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6))
                 =>
                 ((s__RemainderFn(V__ELEMENT,V__NUMBER)
                   = n__0)))))))))))
)
)

( ! [V__ROW3,V__ROW2,V__NUMBER] :
   (((s__instance(V__ROW3,s__Integer) &
         s__instance(V__ROW2,s__Integer) &
         s__instance(V__NUMBER,s__Integer))
       =>
       (((s__GreatestCommonDivisorFn__2Fn(V__ROW2,V__ROW3)
           = V__NUMBER)
         =>
         (( ! [V__ELEMENT] :
             ((s__instance(V__ELEMENT,s__Integer) =>
                 ((s__inList(V__ELEMENT,s__ListFn__2Fn(V__ROW2,V__ROW3))
                 =>
                 ((s__RemainderFn(V__ELEMENT,V__NUMBER)
                   = n__0)))))))))))
)
)

( ! [V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   (((s__instance(V__ROW3,s__Integer) &
         s__instance(V__ROW4,s__Integer) &
         s__instance(V__ROW2,s__Integer) &
         s__instance(V__NUMBER,s__Integer))
       =>
       (((s__GreatestCommonDivisorFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
           = V__NUMBER)
         =>
         (( ! [V__ELEMENT] :
             ((s__instance(V__ELEMENT,s__Integer) =>
                 ((s__inList(V__ELEMENT,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4))
                 =>
                 ((s__RemainderFn(V__ELEMENT,V__NUMBER)
                   = n__0)))))))))))
)
)

( ! [V__ROW2,V__NUMBER] :
   (((s__instance(V__ROW2,s__Integer) &
         s__instance(V__NUMBER,s__Integer))
       =>
       (((s__GreatestCommonDivisorFn__1Fn(V__ROW2)
           = V__NUMBER)
         =>
         (( ! [V__ELEMENT] :
             ((s__instance(V__ELEMENT,s__Integer) =>
                 ((s__inList(V__ELEMENT,s__ListFn__1Fn(V__ROW2))
                 =>
                 ((s__RemainderFn(V__ELEMENT,V__NUMBER)
                   = n__0)))))))))))
)
)

Merge.kif 4723-4728
( ! [V__ROW3,V__ROW2,V__NUMBER] :
   (((s__instance(V__ROW3,s__Integer) &
         s__instance(V__ROW2,s__Integer) &
         s__instance(V__NUMBER,s__Integer))
       =>
       (((s__GreatestCommonDivisorFn__2Fn(V__ROW2,V__ROW3)
           = V__NUMBER)
         =>
         (~(( ? [V__GREATER] :
               ((s__instance(V__GREATER,s__Integer) &
                   (s__greaterThan(V__GREATER,V__NUMBER)
                   &
                   ( ! [V__ELEMENT] :
                     ((s__instance(V__ELEMENT,s__Integer) =>
                         ((s__inList(V__ELEMENT,s__ListFn__2Fn(V__ROW2,V__ROW3))
                         =>
                         ((s__RemainderFn(V__ELEMENT,V__GREATER)
                           = n__0))))))))))))))))
)
)

( ! [V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   (((s__instance(V__ROW3,s__Integer) &
         s__instance(V__ROW4,s__Integer) &
         s__instance(V__ROW2,s__Integer) &
         s__instance(V__NUMBER,s__Integer))
       =>
       (((s__GreatestCommonDivisorFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
           = V__NUMBER)
         =>
         (~(( ? [V__GREATER] :
               ((s__instance(V__GREATER,s__Integer) &
                   (s__greaterThan(V__GREATER,V__NUMBER)
                   &
                   ( ! [V__ELEMENT] :
                     ((s__instance(V__ELEMENT,s__Integer) =>
                         ((s__inList(V__ELEMENT,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4))
                         =>
                         ((s__RemainderFn(V__ELEMENT,V__GREATER)
                           = n__0))))))))))))))))
)
)

( ! [V__ROW2,V__NUMBER] :
   (((s__instance(V__ROW2,s__Integer) &
         s__instance(V__NUMBER,s__Integer))
       =>
       (((s__GreatestCommonDivisorFn__1Fn(V__ROW2)
           = V__NUMBER)
         =>
         (~(( ? [V__GREATER] :
               ((s__instance(V__GREATER,s__Integer) &
                   (s__greaterThan(V__GREATER,V__NUMBER)
                   &
                   ( ! [V__ELEMENT] :
                     ((s__instance(V__ELEMENT,s__Integer) =>
                         ((s__inList(V__ELEMENT,s__ListFn__1Fn(V__ROW2))
                         =>
                         ((s__RemainderFn(V__ELEMENT,V__GREATER)
                           = n__0))))))))))))))))
)
)

( ! [V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   (((s__instance(V__ROW5,s__Integer) &
         s__instance(V__ROW6,s__Integer) &
         s__instance(V__ROW3,s__Integer) &
         s__instance(V__ROW4,s__Integer) &
         s__instance(V__ROW2,s__Integer) &
         s__instance(V__NUMBER,s__Integer))
       =>
       (((s__GreatestCommonDivisorFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
           = V__NUMBER)
         =>
         (~(( ? [V__GREATER] :
               ((s__instance(V__GREATER,s__Integer) &
                   (s__greaterThan(V__GREATER,V__NUMBER)
                   &
                   ( ! [V__ELEMENT] :
                     ((s__instance(V__ELEMENT,s__Integer) =>
                         ((s__inList(V__ELEMENT,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6))
                         =>
                         ((s__RemainderFn(V__ELEMENT,V__GREATER)
                           = n__0))))))))))))))))
)
)

( ! [V__ROW5,V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   (((s__instance(V__ROW5,s__Integer) &
         s__instance(V__ROW3,s__Integer) &
         s__instance(V__ROW4,s__Integer) &
         s__instance(V__ROW2,s__Integer) &
         s__instance(V__NUMBER,s__Integer))
       =>
       (((s__GreatestCommonDivisorFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5)
           = V__NUMBER)
         =>
         (~(( ? [V__GREATER] :
               ((s__instance(V__GREATER,s__Integer) &
                   (s__greaterThan(V__GREATER,V__NUMBER)
                   &
                   ( ! [V__ELEMENT] :
                     ((s__instance(V__ELEMENT,s__Integer) =>
                         ((s__inList(V__ELEMENT,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5))
                         =>
                         ((s__RemainderFn(V__ELEMENT,V__GREATER)
                           = n__0))))))))))))))))
)
)

Merge.kif 4730-4738
( ! [V__ELEMENT,V__ROW3,V__ROW2,V__NUMBER] :
   (((s__instance(V__ROW3,s__Integer) &
         s__instance(V__ROW2,s__Integer) &
         s__instance(V__NUMBER,s__Integer))
       =>
       (((s__LeastCommonMultipleFn__2Fn(V__ROW2,V__ROW3)
           = V__NUMBER)
         =>
         ((s__inList(V__ELEMENT,s__ListFn__2Fn(V__ROW2,V__ROW3))
         =>
         (s__instance(V__ELEMENT,s__Number)))))))
)
)

( ! [V__ROW5,V__ROW6,V__ELEMENT,V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   (((s__instance(V__ROW5,s__Integer) &
         s__instance(V__ROW6,s__Integer) &
         s__instance(V__ROW3,s__Integer) &
         s__instance(V__ROW4,s__Integer) &
         s__instance(V__ROW2,s__Integer) &
         s__instance(V__NUMBER,s__Integer))
       =>
       (((s__LeastCommonMultipleFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
           = V__NUMBER)
         =>
         ((s__inList(V__ELEMENT,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6))
         =>
         (s__instance(V__ELEMENT,s__Number)))))))
)
)

( ! [V__ELEMENT,V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   (((s__instance(V__ROW3,s__Integer) &
         s__instance(V__ROW4,s__Integer) &
         s__instance(V__ROW2,s__Integer) &
         s__instance(V__NUMBER,s__Integer))
       =>
       (((s__LeastCommonMultipleFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
           = V__NUMBER)
         =>
         ((s__inList(V__ELEMENT,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4))
         =>
         (s__instance(V__ELEMENT,s__Number)))))))
)
)

( ! [V__ROW5,V__ELEMENT,V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   (((s__instance(V__ROW5,s__Integer) &
         s__instance(V__ROW3,s__Integer) &
         s__instance(V__ROW4,s__Integer) &
         s__instance(V__ROW2,s__Integer) &
         s__instance(V__NUMBER,s__Integer))
       =>
       (((s__LeastCommonMultipleFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5)
           = V__NUMBER)
         =>
         ((s__inList(V__ELEMENT,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5))
         =>
         (s__instance(V__ELEMENT,s__Number)))))))
)
)

( ! [V__ELEMENT,V__ROW2,V__NUMBER] :
   (((s__instance(V__ROW2,s__Integer) &
         s__instance(V__NUMBER,s__Integer))
       =>
       (((s__LeastCommonMultipleFn__1Fn(V__ROW2)
           = V__NUMBER)
         =>
         ((s__inList(V__ELEMENT,s__ListFn__1Fn(V__ROW2))
         =>
         (s__instance(V__ELEMENT,s__Number)))))))
)
)

Merge.kif 4789-4794
( ! [V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   (((s__instance(V__ROW3,s__Integer) &
         s__instance(V__ROW4,s__Integer) &
         s__instance(V__ROW2,s__Integer) &
         s__instance(V__NUMBER,s__Integer))
       =>
       (((s__LeastCommonMultipleFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
           = V__NUMBER)
         =>
         (( ! [V__ELEMENT] :
             ((s__instance(V__ELEMENT,s__Integer) =>
                 ((s__inList(V__ELEMENT,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4))
                 =>
                 ((s__RemainderFn(V__NUMBER,V__ELEMENT)
                   = n__0)))))))))))
)
)

( ! [V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   (((s__instance(V__ROW5,s__Integer) &
         s__instance(V__ROW6,s__Integer) &
         s__instance(V__ROW3,s__Integer) &
         s__instance(V__ROW4,s__Integer) &
         s__instance(V__ROW2,s__Integer) &
         s__instance(V__NUMBER,s__Integer))
       =>
       (((s__LeastCommonMultipleFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
           = V__NUMBER)
         =>
         (( ! [V__ELEMENT] :
             ((s__instance(V__ELEMENT,s__Integer) =>
                 ((s__inList(V__ELEMENT,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6))
                 =>
                 ((s__RemainderFn(V__NUMBER,V__ELEMENT)
                   = n__0)))))))))))
)
)

( ! [V__ROW3,V__ROW2,V__NUMBER] :
   (((s__instance(V__ROW3,s__Integer) &
         s__instance(V__ROW2,s__Integer) &
         s__instance(V__NUMBER,s__Integer))
       =>
       (((s__LeastCommonMultipleFn__2Fn(V__ROW2,V__ROW3)
           = V__NUMBER)
         =>
         (( ! [V__ELEMENT] :
             ((s__instance(V__ELEMENT,s__Integer) =>
                 ((s__inList(V__ELEMENT,s__ListFn__2Fn(V__ROW2,V__ROW3))
                 =>
                 ((s__RemainderFn(V__NUMBER,V__ELEMENT)
                   = n__0)))))))))))
)
)

( ! [V__ROW2,V__NUMBER] :
   (((s__instance(V__ROW2,s__Integer) &
         s__instance(V__NUMBER,s__Integer))
       =>
       (((s__LeastCommonMultipleFn__1Fn(V__ROW2)
           = V__NUMBER)
         =>
         (( ! [V__ELEMENT] :
             ((s__instance(V__ELEMENT,s__Integer) =>
                 ((s__inList(V__ELEMENT,s__ListFn__1Fn(V__ROW2))
                 =>
                 ((s__RemainderFn(V__NUMBER,V__ELEMENT)
                   = n__0)))))))))))
)
)

( ! [V__ROW5,V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   (((s__instance(V__ROW5,s__Integer) &
         s__instance(V__ROW3,s__Integer) &
         s__instance(V__ROW4,s__Integer) &
         s__instance(V__ROW2,s__Integer) &
         s__instance(V__NUMBER,s__Integer))
       =>
       (((s__LeastCommonMultipleFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5)
           = V__NUMBER)
         =>
         (( ! [V__ELEMENT] :
             ((s__instance(V__ELEMENT,s__Integer) =>
                 ((s__inList(V__ELEMENT,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5))
                 =>
                 ((s__RemainderFn(V__NUMBER,V__ELEMENT)
                   = n__0)))))))))))
)
)

Merge.kif 4796-4801
( ! [V__ROW2,V__NUMBER] :
   (((s__instance(V__ROW2,s__Integer) &
         s__instance(V__NUMBER,s__Integer))
       =>
       (((s__LeastCommonMultipleFn__1Fn(V__ROW2)
           = V__NUMBER)
         =>
         (~(( ? [V__LESS] :
               ((s__instance(V__LESS,s__Integer) &
                   (s__lessThan(V__LESS,V__NUMBER)
                   &
                   ( ! [V__ELEMENT] :
                     ((s__instance(V__ELEMENT,s__Integer) =>
                         ((s__inList(V__ELEMENT,s__ListFn__1Fn(V__ROW2))
                         =>
                         ((s__RemainderFn(V__LESS,V__ELEMENT)
                           = n__0))))))))))))))))
)
)

( ! [V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   (((s__instance(V__ROW3,s__Integer) &
         s__instance(V__ROW4,s__Integer) &
         s__instance(V__ROW2,s__Integer) &
         s__instance(V__NUMBER,s__Integer))
       =>
       (((s__LeastCommonMultipleFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
           = V__NUMBER)
         =>
         (~(( ? [V__LESS] :
               ((s__instance(V__LESS,s__Integer) &
                   (s__lessThan(V__LESS,V__NUMBER)
                   &
                   ( ! [V__ELEMENT] :
                     ((s__instance(V__ELEMENT,s__Integer) =>
                         ((s__inList(V__ELEMENT,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4))
                         =>
                         ((s__RemainderFn(V__LESS,V__ELEMENT)
                           = n__0))))))))))))))))
)
)

( ! [V__ROW3,V__ROW2,V__NUMBER] :
   (((s__instance(V__ROW3,s__Integer) &
         s__instance(V__ROW2,s__Integer) &
         s__instance(V__NUMBER,s__Integer))
       =>
       (((s__LeastCommonMultipleFn__2Fn(V__ROW2,V__ROW3)
           = V__NUMBER)
         =>
         (~(( ? [V__LESS] :
               ((s__instance(V__LESS,s__Integer) &
                   (s__lessThan(V__LESS,V__NUMBER)
                   &
                   ( ! [V__ELEMENT] :
                     ((s__instance(V__ELEMENT,s__Integer) =>
                         ((s__inList(V__ELEMENT,s__ListFn__2Fn(V__ROW2,V__ROW3))
                         =>
                         ((s__RemainderFn(V__LESS,V__ELEMENT)
                           = n__0))))))))))))))))
)
)

( ! [V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   (((s__instance(V__ROW5,s__Integer) &
         s__instance(V__ROW6,s__Integer) &
         s__instance(V__ROW3,s__Integer) &
         s__instance(V__ROW4,s__Integer) &
         s__instance(V__ROW2,s__Integer) &
         s__instance(V__NUMBER,s__Integer))
       =>
       (((s__LeastCommonMultipleFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
           = V__NUMBER)
         =>
         (~(( ? [V__LESS] :
               ((s__instance(V__LESS,s__Integer) &
                   (s__lessThan(V__LESS,V__NUMBER)
                   &
                   ( ! [V__ELEMENT] :
                     ((s__instance(V__ELEMENT,s__Integer) =>
                         ((s__inList(V__ELEMENT,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6))
                         =>
                         ((s__RemainderFn(V__LESS,V__ELEMENT)
                           = n__0))))))))))))))))
)
)

( ! [V__ROW5,V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   (((s__instance(V__ROW5,s__Integer) &
         s__instance(V__ROW3,s__Integer) &
         s__instance(V__ROW4,s__Integer) &
         s__instance(V__ROW2,s__Integer) &
         s__instance(V__NUMBER,s__Integer))
       =>
       (((s__LeastCommonMultipleFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5)
           = V__NUMBER)
         =>
         (~(( ? [V__LESS] :
               ((s__instance(V__LESS,s__Integer) &
                   (s__lessThan(V__LESS,V__NUMBER)
                   &
                   ( ! [V__ELEMENT] :
                     ((s__instance(V__ELEMENT,s__Integer) =>
                         ((s__inList(V__ELEMENT,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5))
                         =>
                         ((s__RemainderFn(V__LESS,V__ELEMENT)
                           = n__0))))))))))))))))
)
)

Merge.kif 4803-4811
( ! [V__TIME,V__LIST,V__INT,V__DUR] :
   (((s__instance(V__TIME,s__TimeInterval) &
         s__instance(V__LIST,s__ConsecutiveTimeIntervalList) &
         s__instance(V__INT,s__TimeInterval) &
         s__instance(V__DUR,s__TimeDuration))
       =>
       (((V__LIST = s__TimeIntervalListFn(V__TIME,V__DUR))
         =>
         (((s__BeginFn(V__TIME)
             = s__BeginFn(s__FirstFn(V__LIST)))
       &
       s__inList(V__INT,V__LIST)
     &
     s__duration(V__INT,V__DUR))))))
)
)

Weather.kif 1965-1973
( ! [V__LIST,V__X] :
   (((s__instance(V__LIST,s__List) &
         s__instance(V__X,s__Number))
       =>
       (((V__X = s__MaxValueFn(V__LIST))
         =>
         (~(( ? [V__Y] :
               ((s__instance(V__Y,s__Quantity) &
                   (s__inList(V__Y,V__LIST)
                   &
                   s__greaterThan(V__Y,V__X))))))))))
)
)

Weather.kif 1684-1691
( ! [V__ROW5,V__ROW3,V__ROW4,V__ROW2,V__CLASS] :
   (((s__instance(V__ROW5,s__Attribute) &
         s__instance(V__ROW3,s__Attribute) &
         s__instance(V__ROW4,s__Attribute) &
         s__instance(V__ROW2,s__Attribute) &
         s__subclass(V__CLASS,s__Attribute) &
         s__instance(V__CLASS,s__Class))
       =>
       ((s__exhaustiveAttribute__5(V__CLASS,V__ROW2,V__ROW3,V__ROW4,V__ROW5)
         =>
         (( ! [V__ATTR1] :
             ((s__instance(V__ATTR1,V__CLASS)
               =>
               (( ? [V__ATTR2] :
                   ((s__inList(V__ATTR2,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5))
                   &
                   (V__ATTR1 = V__ATTR2))))))))))))
)
)

( ! [V__ROW3,V__ROW2,V__CLASS] :
   (((s__instance(V__ROW3,s__Attribute) &
         s__instance(V__ROW2,s__Attribute) &
         s__subclass(V__CLASS,s__Attribute) &
         s__instance(V__CLASS,s__Class))
       =>
       ((s__exhaustiveAttribute__3(V__CLASS,V__ROW2,V__ROW3)
         =>
         (( ! [V__ATTR1] :
             ((s__instance(V__ATTR1,V__CLASS)
               =>
               (( ? [V__ATTR2] :
                   ((s__inList(V__ATTR2,s__ListFn__2Fn(V__ROW2,V__ROW3))
                   &
                   (V__ATTR1 = V__ATTR2))))))))))))
)
)

( ! [V__ROW3,V__ROW4,V__ROW2,V__CLASS] :
   (((s__instance(V__ROW3,s__Attribute) &
         s__instance(V__ROW4,s__Attribute) &
         s__instance(V__ROW2,s__Attribute) &
         s__subclass(V__CLASS,s__Attribute) &
         s__instance(V__CLASS,s__Class))
       =>
       ((s__exhaustiveAttribute__4(V__CLASS,V__ROW2,V__ROW3,V__ROW4)
         =>
         (( ! [V__ATTR1] :
             ((s__instance(V__ATTR1,V__CLASS)
               =>
               (( ? [V__ATTR2] :
                   ((s__inList(V__ATTR2,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4))
                   &
                   (V__ATTR1 = V__ATTR2))))))))))))
)
)

( ! [V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__CLASS] :
   (((s__instance(V__ROW5,s__Attribute) &
         s__instance(V__ROW6,s__Attribute) &
         s__instance(V__ROW3,s__Attribute) &
         s__instance(V__ROW4,s__Attribute) &
         s__instance(V__ROW2,s__Attribute) &
         s__subclass(V__CLASS,s__Attribute) &
         s__instance(V__CLASS,s__Class))
       =>
       ((s__exhaustiveAttribute__6(V__CLASS,V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
         =>
         (( ! [V__ATTR1] :
             ((s__instance(V__ATTR1,V__CLASS)
               =>
               (( ? [V__ATTR2] :
                   ((s__inList(V__ATTR2,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6))
                   &
                   (V__ATTR1 = V__ATTR2))))))))))))
)
)

( ! [V__ROW2,V__CLASS] :
   (((s__instance(V__ROW2,s__Attribute) &
         s__subclass(V__CLASS,s__Attribute) &
         s__instance(V__CLASS,s__Class))
       =>
       ((s__exhaustiveAttribute__2(V__CLASS,V__ROW2)
         =>
         (( ! [V__ATTR1] :
             ((s__instance(V__ATTR1,V__CLASS)
               =>
               (( ? [V__ATTR2] :
                   ((s__inList(V__ATTR2,s__ListFn__1Fn(V__ROW2))
                   &
                   (V__ATTR1 = V__ATTR2))))))))))))
)
)

Merge.kif 510-518
( ! [V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__CLASS] :
   (((s__instance(V__ROW5,s__Class) &
         s__instance(V__ROW6,s__Class) &
         s__instance(V__ROW3,s__Class) &
         s__instance(V__ROW4,s__Class) &
         s__instance(V__ROW2,s__Class) &
         s__instance(V__CLASS,s__Class))
       =>
       ((s__exhaustiveDecomposition__6(V__CLASS,V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
         =>
         (( ! [V__OBJ] :
             ((s__instance(V__OBJ,V__CLASS)
               =>
               (( ? [V__ITEM] :
                   ((s__instance(V__ITEM,s__Class) &
                       (s__inList(V__ITEM,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6))
                     &
                     s__instance(V__OBJ,V__ITEM)))))))))))))
)
)

( ! [V__ROW5,V__ROW3,V__ROW4,V__ROW2,V__CLASS] :
   (((s__instance(V__ROW5,s__Class) &
         s__instance(V__ROW3,s__Class) &
         s__instance(V__ROW4,s__Class) &
         s__instance(V__ROW2,s__Class) &
         s__instance(V__CLASS,s__Class))
       =>
       ((s__exhaustiveDecomposition__5(V__CLASS,V__ROW2,V__ROW3,V__ROW4,V__ROW5)
         =>
         (( ! [V__OBJ] :
             ((s__instance(V__OBJ,V__CLASS)
               =>
               (( ? [V__ITEM] :
                   ((s__instance(V__ITEM,s__Class) &
                       (s__inList(V__ITEM,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5))
                     &
                     s__instance(V__OBJ,V__ITEM)))))))))))))
)
)

( ! [V__ROW3,V__ROW4,V__ROW2,V__CLASS] :
   (((s__instance(V__ROW3,s__Class) &
         s__instance(V__ROW4,s__Class) &
         s__instance(V__ROW2,s__Class) &
         s__instance(V__CLASS,s__Class))
       =>
       ((s__exhaustiveDecomposition__4(V__CLASS,V__ROW2,V__ROW3,V__ROW4)
         =>
         (( ! [V__OBJ] :
             ((s__instance(V__OBJ,V__CLASS)
               =>
               (( ? [V__ITEM] :
                   ((s__instance(V__ITEM,s__Class) &
                       (s__inList(V__ITEM,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4))
                     &
                     s__instance(V__OBJ,V__ITEM)))))))))))))
)
)

( ! [V__ROW3,V__ROW2,V__CLASS] :
   (((s__instance(V__ROW3,s__Class) &
         s__instance(V__ROW2,s__Class) &
         s__instance(V__CLASS,s__Class))
       =>
       ((s__exhaustiveDecomposition__3(V__CLASS,V__ROW2,V__ROW3)
         =>
         (( ! [V__OBJ] :
             ((s__instance(V__OBJ,V__CLASS)
               =>
               (( ? [V__ITEM] :
                   ((s__instance(V__ITEM,s__Class) &
                       (s__inList(V__ITEM,s__ListFn__2Fn(V__ROW2,V__ROW3))
                     &
                     s__instance(V__OBJ,V__ITEM)))))))))))))
)
)

( ! [V__ROW2,V__CLASS] :
   (((s__instance(V__ROW2,s__Class) &
         s__instance(V__CLASS,s__Class))
       =>
       ((s__exhaustiveDecomposition__2(V__CLASS,V__ROW2)
         =>
         (( ! [V__OBJ] :
             ((s__instance(V__OBJ,V__CLASS)
               =>
               (( ? [V__ITEM] :
                   ((s__instance(V__ITEM,s__Class) &
                       (s__inList(V__ITEM,s__ListFn__1Fn(V__ROW2))
                     &
                     s__instance(V__OBJ,V__ITEM)))))))))))))
)
)

Merge.kif 2869-2877

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25


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

Show without tree


Sigma web home      Suggested Upper Merged Ontology (SUMO) web home
Sigma version 3.0 is open source software produced by Articulate Software and its partners