ListOrderFn - Sigma Knowledge base Browser

appearance as argument number 1

s__documentation(s__ListOrderFn__m,s__ChineseLanguage,'(ListOrderFn ?LIST ?NUMBER) 表示在 ?LIST List 第?NUMBER个位置的项目。例如： (ListOrderFn (ListFn Monday Tuesday Wednesday) 2) 交出的值会是 Tuesday。')	Merge.kif 3157-3159
s__documentation(s__ListOrderFn__m,s__EnglishLanguage,'(ListOrderFn ?LIST ?NUMBER) denotes the item that is in the ?NUMBER position in the List ?LIST. For example, (ListOrderFn (ListFn Monday Tuesday Wednesday) 2) would return the value Tuesday.')	Merge.kif 3153-3156
s__domain(s__ListOrderFn__m,1,s__List)	Merge.kif 3150-3150	The number 1 argument of list order is an instance of list
s__domain(s__ListOrderFn__m,2,s__PositiveInteger)	Merge.kif 3151-3151	The number 2 argument of list order is an instance of positive integer
s__instance(s__ListOrderFn__m,s__BinaryFunction) s__instance(s__BinaryFunction,s__SetOrClass)	Merge.kif 3148-3148	List order is an instance of binary function
s__instance(s__ListOrderFn__m,s__PartialValuedRelation) s__instance(s__PartialValuedRelation,s__SetOrClass)	Merge.kif 3149-3149	List order is an instance of partial valued relation
s__range(s__ListOrderFn__m,s__Entity)	Merge.kif 3152-3152	The range of list order is an instance of entity

appearance as argument number 2

s__format(s__ChineseLanguage,s__ListOrderFn__m,'%1 的第 %2 几个元素')	chinese_format.kif 263-263
s__format(s__EnglishLanguage,s__ListOrderFn__m,'%2th element of %1')	english_format.kif 160-160
s__format(s__FrenchLanguage,s__ListOrderFn__m,'%2th �lement de %1')	french_format.kif 150-150
s__format(s__ItalianLanguage,s__ListOrderFn__m,'%2th elemento di %1')	relations-it.txt 169-169
s__format(s__PortugueseLanguage,s__ListOrderFn__m,'%2th elemento de %1')	portuguese_format.kif 102-102
s__format(s__ar__m,s__ListOrderFn__m,'%2 عُنْصُر من %1')	arabic_format.kif 98-98
s__format(s__cz__m,s__ListOrderFn__m,'%2th element of %1')	relations-cz.txt 159-159
s__format(s__de__m,s__ListOrderFn__m,'%2te mitglied von %1')	relations-de.txt 338-338
s__format(s__hi__m,s__ListOrderFn__m,'%1 kaa ghaTaka sankhyaa %2')	relations-hindi.txt 207-207
s__format(s__tg__m,s__ListOrderFn__m,'%2th elemento ng %1')	relations-tg.txt 337-337
s__termFormat(s__ChineseLanguage,s__ListOrderFn__m,'找出表列顺序的函数')	chinese_format.kif 264-264	"找出表列顺序的函数" is the printable form of list order in ChineseLanguage
s__termFormat(s__EnglishLanguage,s__ListOrderFn__m,'list order')	domainEnglishFormat.kif 6201-6201	"list order" is the printable form of list order in english language
s__termFormat(s__ar__m,s__ListOrderFn__m,'«عُنْصُر من»')	arabic_format.kif 548-548	"«عُنْصُر من»" is the printable form of list order in ar
s__termFormat(s__tg__m,s__ListOrderFn__m,'tungkulin ng talaan utos1')	relations-tg.txt 338-338	"tungkulin ng talaan utos1" is the printable form of list order in tg

antecedent

( ! [V__ARG,V__ARGS1,V__X,V__Y] : ((s__exactCardinality(s__contraryAttribute__m,V__ARG,1) & s__instance(s__contraryAttribute__m,s__Predicate) & s__contraryAttribute_1(V__ARGS1) & (V__X = s__ListOrderFn(s__ListFn_1(V__ARGS1) ,V__ARG)) & (V__Y = s__ListOrderFn(s__ListFn_1(V__ARGS1) ,V__ARG))) => (V__X = V__Y)) )	Media.kif 2108-2115	If there can be 1 values to argument ?ARG of ?REL and ?REL is an instance of predicate and ?REL @ARGS and ?X is equal to ?ARGth element of (@ARGS) and ?Y is equal to ?ARGth element of (@ARGS), then ?X is equal to ?Y
( ! [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	If there can be 1 values to argument ?ARG of ?REL and ?REL is an instance of predicate and ?REL @ARGS and ?X is equal to ?ARGth element of (@ARGS), then there doesn't exist ?Y such that ?Y is equal to ?ARGth element of (@ARGS) and ?X is not equal to ?Y
( ! [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	If the region ?DIRECTION of @ROW is an instance of region and 1th element of (@ROW) is equal to ?NUM angular degree(s), then ?NUM is less than or equal to 90
( ! [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	If the meridian at @ROW ?DIRECTION is an instance of region and 1th element of (@ROW) is equal to ?NUM angular degree(s), then ?NUM is less than or equal to 180
( ! [V__ROW1,V__Process1,V__Process2,V__Number1,V__Number2] : ((s__processList_1(V__ROW1) & s__inList(V__Process1,s__ListFn_1(V__ROW1)) & s__inList(V__Process2,s__ListFn_1(V__ROW1)) & (s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__Number1) = V__Process1) & (s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__Number2) = V__Process2) & less(V__Number1,V__Number2)) => s__earlier(s__WhenFn(V__Process1) ,s__WhenFn(V__Process2))) )	QoSontology.kif 692-700	If the list of processes @ROW and ?Process1 is a member of (@ROW) and ?Process2 is a member of (@ROW) and ?Number1th element of (@ROW) is equal to ?Process1 and ?Number2th element of (@ROW) is equal to ?Process2 and ?Number1 is less than ?Number2, then the time of existence of ?Process1 happens earlier than the time of existence of ?Process2
( ! [V__USER,V__LIST,V__ACCESSING1,V__ACCESSING2,V__INDEX1,V__INDEX2] : ((s__viewedItemList(V__USER,V__LIST) & s__instance(V__ACCESSING1,s__AccessingWebPage) & s__instance(V__ACCESSING2,s__AccessingWebPage) & s__instance(V__INDEX1,s__PositiveInteger) & s__instance(V__INDEX2,s__PositiveInteger) & (s__ListOrderFn(V__LIST,V__INDEX1) = V__ACCESSING1) & (s__ListOrderFn(V__LIST,V__INDEX2) = V__ACCESSING2) & greater(V__INDEX1,V__INDEX2)) => s__earlier(s__WhenFn(V__ACCESSING2) ,s__WhenFn(V__ACCESSING1))) )	UXExperimentalTerms.kif 990-1006	If %2 is the list of items viewed by 1 and ?ACCESSING1 is an instance of AccessingWebPage and ?ACCESSING2 is an instance of AccessingWebPage and ?INDEX1 is an instance of positive integer and ?INDEX2 is an instance of positive integer and ?INDEX1th element of ?LIST is equal to ?ACCESSING1 and ?INDEX2th element of ?LIST is equal to ?ACCESSING2 and ?INDEX1 is greater than ?INDEX2, then the time of existence of ?ACCESSING2 happens earlier than the time of existence of ?ACCESSING1

consequent

( ! [V__ROW1] : ((s__instance(s__parent__m,s__TotalValuedRelation) & s__instance(s__parent__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__parent__m,s__Relation) & s__valence(s__parent__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__parent__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__parent(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__protonNumber__m,s__TotalValuedRelation) & s__instance(s__protonNumber__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__protonNumber__m,s__Relation) & s__valence(s__protonNumber__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__protonNumber__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__protonNumber(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__lineMeasure__m,s__TotalValuedRelation) & s__instance(s__lineMeasure__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__lineMeasure__m,s__Relation) & s__valence(s__lineMeasure__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__lineMeasure__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__lineMeasure(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__earlier__m,s__TotalValuedRelation) & s__instance(s__earlier__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__earlier__m,s__Relation) & s__valence(s__earlier__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__earlier__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__earlier(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__conclusion__m,s__TotalValuedRelation) & s__instance(s__conclusion__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__conclusion__m,s__Relation) & s__valence(s__conclusion__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__conclusion__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__conclusion(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__coordinates__m,s__TotalValuedRelation) & s__instance(s__coordinates__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__coordinates__m,s__Relation) & s__valence(s__coordinates__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__coordinates__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__coordinates(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__subCollection__m,s__TotalValuedRelation) & s__instance(s__subCollection__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__subCollection__m,s__Relation) & s__valence(s__subCollection__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__subCollection__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__subCollection(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__meetsTemporally__m,s__TotalValuedRelation) & s__instance(s__meetsTemporally__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__meetsTemporally__m,s__Relation) & s__valence(s__meetsTemporally__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__meetsTemporally__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__meetsTemporally(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__subrelation__m,s__TotalValuedRelation) & s__instance(s__subrelation__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__subrelation__m,s__Relation) & s__valence(s__subrelation__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__subrelation__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__subrelation(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(greater__m,s__TotalValuedRelation) & s__instance(greater__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(greater__m,s__Relation) & s__valence(greater__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(greater__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : greater(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__subAttribute__m,s__TotalValuedRelation) & s__instance(s__subAttribute__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__subAttribute__m,s__Relation) & s__valence(s__subAttribute__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__subAttribute__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__subAttribute(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__subclass__m,s__TotalValuedRelation) & s__instance(s__subclass__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__subclass__m,s__Relation) & s__valence(s__subclass__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__subclass__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__subclass(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__larger__m,s__TotalValuedRelation) & s__instance(s__larger__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__larger__m,s__Relation) & s__valence(s__larger__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__larger__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__larger(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__maximumPayloadCapacity__m,s__TotalValuedRelation) & s__instance(s__maximumPayloadCapacity__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__maximumPayloadCapacity__m,s__Relation) & s__valence(s__maximumPayloadCapacity__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__maximumPayloadCapacity__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__maximumPayloadCapacity(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(lesseq__m,s__TotalValuedRelation) & s__instance(lesseq__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(lesseq__m,s__Relation) & s__valence(lesseq__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(lesseq__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : lesseq(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__partlyLocated__m,s__TotalValuedRelation) & s__instance(s__partlyLocated__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__partlyLocated__m,s__Relation) & s__valence(s__partlyLocated__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__partlyLocated__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__partlyLocated(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(greatereq__m,s__TotalValuedRelation) & s__instance(greatereq__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(greatereq__m,s__Relation) & s__valence(greatereq__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(greatereq__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : greatereq(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__moves__m,s__TotalValuedRelation) & s__instance(s__moves__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__moves__m,s__Relation) & s__valence(s__moves__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__moves__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__moves(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__beforeOrEqual__m,s__TotalValuedRelation) & s__instance(s__beforeOrEqual__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__beforeOrEqual__m,s__Relation) & s__valence(s__beforeOrEqual__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__beforeOrEqual__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__beforeOrEqual(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__eventLocated__m,s__TotalValuedRelation) & s__instance(s__eventLocated__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__eventLocated__m,s__Relation) & s__valence(s__eventLocated__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__eventLocated__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__eventLocated(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__smaller__m,s__TotalValuedRelation) & s__instance(s__smaller__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__smaller__m,s__Relation) & s__valence(s__smaller__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__smaller__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__smaller(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__diameter__m,s__TotalValuedRelation) & s__instance(s__diameter__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__diameter__m,s__Relation) & s__valence(s__diameter__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__diameter__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__diameter(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__electronNumber__m,s__TotalValuedRelation) & s__instance(s__electronNumber__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__electronNumber__m,s__Relation) & s__valence(s__electronNumber__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__electronNumber__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__electronNumber(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__personTransportCapability__m,s__TotalValuedRelation) & s__instance(s__personTransportCapability__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__personTransportCapability__m,s__Relation) & s__valence(s__personTransportCapability__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__personTransportCapability__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__personTransportCapability(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__abstractPart__m,s__TotalValuedRelation) & s__instance(s__abstractPart__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__abstractPart__m,s__Relation) & s__valence(s__abstractPart__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__abstractPart__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__abstractPart(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__transactionAmount__m,s__TotalValuedRelation) & s__instance(s__transactionAmount__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__transactionAmount__m,s__Relation) & s__valence(s__transactionAmount__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__transactionAmount__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__transactionAmount(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__time__m,s__TotalValuedRelation) & s__instance(s__time__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__time__m,s__Relation) & s__valence(s__time__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__time__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__time(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__caliber__m,s__TotalValuedRelation) & s__instance(s__caliber__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__caliber__m,s__Relation) & s__valence(s__caliber__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__caliber__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__caliber(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__graphPart__m,s__TotalValuedRelation) & s__instance(s__graphPart__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__graphPart__m,s__Relation) & s__valence(s__graphPart__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__graphPart__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__graphPart(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__geometricPart__m,s__TotalValuedRelation) & s__instance(s__geometricPart__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__geometricPart__m,s__Relation) & s__valence(s__geometricPart__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__geometricPart__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__geometricPart(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__changesLocation__m,s__TotalValuedRelation) & s__instance(s__changesLocation__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__changesLocation__m,s__Relation) & s__valence(s__changesLocation__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__changesLocation__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__changesLocation(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__temporalPart__m,s__TotalValuedRelation) & s__instance(s__temporalPart__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__temporalPart__m,s__Relation) & s__valence(s__temporalPart__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__temporalPart__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__temporalPart(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__path__m,s__TotalValuedRelation) & s__instance(s__path__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__path__m,s__Relation) & s__valence(s__path__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__path__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__path(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__premise__m,s__TotalValuedRelation) & s__instance(s__premise__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__premise__m,s__Relation) & s__valence(s__premise__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__premise__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__premise(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__subsumesContentClass__m,s__TotalValuedRelation) & s__instance(s__subsumesContentClass__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__subsumesContentClass__m,s__Relation) & s__valence(s__subsumesContentClass__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__subsumesContentClass__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__subsumesContentClass(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__subProcess__m,s__TotalValuedRelation) & s__instance(s__subProcess__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__subProcess__m,s__Relation) & s__valence(s__subProcess__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__subProcess__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__subProcess(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__radius__m,s__TotalValuedRelation) & s__instance(s__radius__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__radius__m,s__Relation) & s__valence(s__radius__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__radius__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__radius(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__subsumesContentInstance__m,s__TotalValuedRelation) & s__instance(s__subsumesContentInstance__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__subsumesContentInstance__m,s__Relation) & s__valence(s__subsumesContentInstance__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__subsumesContentInstance__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__subsumesContentInstance(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__contestParticipant__m,s__TotalValuedRelation) & s__instance(s__contestParticipant__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__contestParticipant__m,s__Relation) & s__valence(s__contestParticipant__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__contestParticipant__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__contestParticipant(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__stringLength__m,s__TotalValuedRelation) & s__instance(s__stringLength__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__stringLength__m,s__Relation) & s__valence(s__stringLength__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__stringLength__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__stringLength(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__subList__m,s__TotalValuedRelation) & s__instance(s__subList__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__subList__m,s__Relation) & s__valence(s__subList__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__subList__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__subList(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__angularMeasure__m,s__TotalValuedRelation) & s__instance(s__angularMeasure__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__angularMeasure__m,s__Relation) & s__valence(s__angularMeasure__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__angularMeasure__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__angularMeasure(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__subLanguage__m,s__TotalValuedRelation) & s__instance(s__subLanguage__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__subLanguage__m,s__Relation) & s__valence(s__subLanguage__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__subLanguage__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__subLanguage(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__duration__m,s__TotalValuedRelation) & s__instance(s__duration__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__duration__m,s__Relation) & s__valence(s__duration__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__duration__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__duration(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__initialList__m,s__TotalValuedRelation) & s__instance(s__initialList__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__initialList__m,s__Relation) & s__valence(s__initialList__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__initialList__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__initialList(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__subString__m,s__TotalValuedRelation) & s__instance(s__subString__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__subString__m,s__Relation) & s__valence(s__subString__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__subString__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__subString(V__ROW1,V__ITEM)))))) )	Merge.kif 2308-2325	?REL is an instance of total valued relation and ?REL is an instance of predicate if and only if there exists ?VALENCE such that ?REL is an instance of relation and ?REL %&has ?VALENCE argument(s) and if for all ?NUMBER, ?ELEMENT and ?CLASS if ?NUMBER is less than ?VALENCE and the number ?NUMBER argument of ?REL is an instance of ?CLASS and ?ELEMENT is equal to ?NUMBERth element of (@ROW), then ?ELEMENT is an instance of ?CLASS , then there exists ?ITEM such that ?REL @ROW and ?ITEM
( ! [V__LIST1,V__AVERAGE,V__LASTPLACE] : (s__average(V__LIST1,V__AVERAGE) <=> (? [V__LIST2] : ((s__ListLengthFn(V__LIST2) = s__ListLengthFn(V__LIST1)) & (s__ListOrderFn(V__LIST2,1) = s__ListOrderFn(V__LIST1,1)) & (! [V__ITEMFROM2] : (s__inList(V__ITEMFROM2,V__LIST2) => (? [V__POSITION,V__POSITIONMINUSONE,V__ITEMFROM1,V__PRIORFROM2] : (greater(V__POSITION,1) & lesseq(V__POSITION,s__ListLengthFn(V__LIST2)) & (s__ListOrderFn(V__LIST2,V__ITEMFROM2) = V__POSITION) & s__inList(V__ITEMFROM1,V__LIST1) & (V__POSITION = s__ListOrderFn(V__LIST1,V__ITEMFROM1)) & s__inList(V__PRIORFROM2,V__LIST2) & (V__POSITIONMINUSONE = minus(V__POSITION,1)) & (V__POSITIONMINUSONE = s__ListOrderFn(V__LIST2,V__PRIORFROM2)) & (V__ITEMFROM2 = plus(V__ITEMFROM1,V__PRIORFROM2)))))) & (V__LASTPLACE = s__ListLengthFn(V__LIST2)) & (V__AVERAGE = divide(s__ListOrderFn(V__LIST2,V__LASTPLACE) ,V__LASTPLACE))))) )	People.kif 285-306	?AVERAGE is an average of ?LIST1 if and only if there exists ?LIST2 such that length of ?LIST2 is equal to length of ?LIST1 and 1th element of ?LIST2 is equal to 1th element of ?LIST1 and for all ?ITEMFROM2 if ?ITEMFROM2 is a member of ?LIST2, then there exist ?POSITION, ?POSITIONMINUSONE,, , ?ITEMFROM1 and ?PRIORFROM2 such that ?POSITION is greater than 1 and ?POSITION is less than or equal to length of ?LIST2 and ?ITEMFROM2th element of ?LIST2 is equal to ?POSITION and ?ITEMFROM1 is a member of ?LIST1 and ?POSITION is equal to ?ITEMFROM1th element of ?LIST1 and ?PRIORFROM2 is a member of ?LIST2 and ?POSITIONMINUSONE is equal to (?POSITION and 1) and ?POSITIONMINUSONE is equal to ?PRIORFROM2th element of ?LIST2 and ?ITEMFROM2 is equal to (?ITEMFROM1 and ?PRIORFROM2) and ?LASTPLACE is equal to length of ?LIST2 and ?AVERAGE is equal to ?LASTPLACEth element of ?LIST2 and ?LASTPLACE
( ! [V__LIST,V__ITEM] : ((s__LastFn(V__LIST) = V__ITEM) <=> (? [V__NUMBER] : ((s__ListLengthFn(V__LIST) = V__NUMBER) & (s__ListOrderFn(V__LIST,V__NUMBER) = V__ITEM)))) )	Mid-level-ontology.kif 6342-6347	The last of ?LIST is equal to ?ITEM if and only if there exists ?NUMBER such that length of ?LIST is equal to ?NUMBER and ?NUMBERth element of ?LIST is equal to ?ITEM
( ! [V__NUMBER,V__CLASS,V__ROW1] : ((s__domain(s__contraryAttribute__m,V__NUMBER,V__CLASS) & s__instance(s__contraryAttribute__m,s__Predicate) & s__contraryAttribute_1(V__ROW1)) => s__instance(s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER) ,V__CLASS)) )	Merge.kif 3173-3178	If the number ?NUMBER argument of ?REL is an instance of ?CLASS and ?REL is an instance of predicate and ?REL @ROW, then ?NUMBERth element of (@ROW) is an instance of ?CLASS
( ! [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	If the number ?NUMBER argument of ?REL is a subclass of ?CLASS and ?REL is an instance of predicate and ?REL @ROW, then ?NUMBERth element of (@ROW) is a subclass of ?CLASS
( ! [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	If there can be 1 values to argument ?ARG of ?REL and ?REL is an instance of predicate and ?REL @ARGS and ?X is equal to ?ARGth element of (@ARGS), then there doesn't exist ?Y such that ?Y is equal to ?ARGth element of (@ARGS) and ?X is not equal to ?Y
( ! [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	If there can be ?COUNT values to argument ?ARG of ?REL and ?REL is an instance of predicate, then there exists ?S such that ?S is an instance of set or class and if ?REL @ARGS and ?EL is equal to ?ARGth element of (@ARGS), then ?EL is an instance of ?S and the number of instances in ?S is equal to ?COUNT
( ! [V__LIST] : ((s__instance(V__LIST,s__List) & (~ (V__LIST = s__NullList__m))) => (s__FirstFn(V__LIST) = s__ListOrderFn(V__LIST,1))) )	Mid-level-ontology.kif 6356-6361	If ?LIST is an instance of list and ?LIST is not equal to null list, then the first of ?LIST is equal to 1th element of ?LIST
( ! [V__SEO,V__PAGE,V__BEFORE,V__AFTER] : ((s__instance(V__SEO,s__SEO) & s__patient(V__SEO,V__PAGE)) => s__hasPurpose(V__SEO,'(? [V__SRPRESULT_BEFORE,V__SRPRESULT_AFTER,V__BM1,V__BM2] : (s__instance(V__SRPRESULT_BEFORE,s__SRPResults) & s__instance(V__SRPRESULT_AFTER,s__SRPResult) & (V__PAGE = s__ListOrderFn(V__SRPRESULT_BEFORE,V__BEFORE)) & (V__PAGE = s__ListOrderFn(V__SRPRESULT_AFTER,V__AFTER)) & s__instance(V__BM1,s__BestMatchAlgorithm) & s__instance(V__BM2,s__BestMatchAlgorithm) & s__earlier(s__WhenFn(V__BM1),s__WhenFn(V__BM2)) & s__earlier(s__WhenFn(V__SEO),s__WhenFn(V__BM2)) & s__earlier(s__WhenFn(V__BM1),s__WhenFn(V__SEO)) & greater(V__BEFORE,V__AFTER)))')) )	UXExperimentalTerms.kif 2596-2612	If ?SEO is an instance of search engine optimization and ?PAGE is a patient of ?SEO, then ?SEO has purpose there exist ?SRPRESULT_BEFORE, ?SRPRESULT_AFTER,, , ?BM1 and ?BM2 such that ?SRPRESULT_BEFORE is an instance of search results and ?SRPRESULT_AFTER is an instance of SRPResult and ?PAGE is equal to ?BEFOREth element of ?SRPRESULT_BEFORE and ?PAGE is equal to ?AFTERth element of ?SRPRESULT_AFTER and ?BM1 is an instance of best match sort and ?BM2 is an instance of best match sort and the time of existence of ?BM1 happens earlier than the time of existence of ?BM2 and the time of existence of ?SEO happens earlier than the time of existence of ?BM2 and the time of existence of ?BM1 happens earlier than the time of existence of ?SEO and ?BEFORE is greater than ?AFTER
( ! [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	If there can be at most ?COUNT values to argument ?ARG of ?REL and ?REL is an instance of predicate, then there exists ?S such that ?S is an instance of set or class and if ?REL @ARGS and ?EL is equal to ?ARGth element of (@ARGS), then ?EL is an instance of ?S and the number of instances in ?S is less than or equal to ?COUNT
( ! [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	If there are at least ?COUNT values to argument ?ARG of ?REL and ?REL is an instance of predicate, then there exists ?S such that ?S is an instance of set or class and if ?REL @ARGS and ?EL is equal to ?ARGth element of (@ARGS), then ?EL is an instance of ?S and the number of instances in ?S is greater than or equal to ?COUNT
( ! [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	If @ROW is the opposite of , then for all ?ATTR1 and ?ATTR2 if ?ATTR1 is equal to ?NUMBER1th element of (@ROW) and ?ATTR2 is equal to ?NUMBER2th element of (@ROW) and ?NUMBER1 is not equal to ?NUMBER2, then if ?OBJ has an attribute ?ATTR1, then ?OBJ has not an attribute ?ATTR2
( ! [V__LIST1,V__LIST2,V__ROW11,V__ROW21] : ((V__LIST1 = V__LIST2) => (((V__LIST1 = s__ListFn_1(V__ROW11)) & (V__LIST2 = s__ListFn_1(V__ROW21))) => (! [V__NUMBER] : (s__ListOrderFn(s__ListFn_1(V__ROW11) ,V__NUMBER) = s__ListOrderFn(s__ListFn_1(V__ROW21) ,V__NUMBER))))) )	Merge.kif 326-333	If ?LIST1 is equal to ?LIST2, then if ?LIST1 is equal to (@ROW1) and ?LIST2 is equal to (@ROW2), then for all ?NUMBER ?NUMBERth element of (@ROW1) is equal to ?NUMBERth element of (@ROW2)
( ! [V__REL,V__ARG,V__COUNT,V__EL,V__ARGS1] : (s__exactCardinality(V__REL,V__ARG,V__COUNT) => (s__CardinalityFn(s__KappaFn(V__EL,'(V__REL(V__ARGS1) & (V__EL = s__ListOrderFn(s__ListFn_1(V__ARGS1),V__ARG)))')) = V__COUNT)) )	Media.kif 2123-2131	If there can be ?COUNT values to argument ?ARG of ?REL, then the number of instances in the class described by ?EL is equal to ?COUNT
( ! [V__ATTRCLASS,V__ROW1] : (s__exhaustiveAttribute_2(V__ATTRCLASS,V__ROW1) => (~ (? [V__EL] : (s__instance(V__EL,V__ATTRCLASS) & (~ (? [V__ATTR,V__NUMBER] : ((V__EL = V__ATTR) & (V__ATTR = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))))))))) )	Merge.kif 568-580	If @ROW are all the attributes of ?ATTRCLASS, then there doesn't exist ?EL such that ?EL is an instance of ?ATTRCLASS and there don't exist ?ATTR and ?NUMBER such that ?EL is equal to ?ATTR and ?ATTR is equal to ?NUMBERth element of (@ROW)
( ! [V__ITEM,V__LIST] : (s__inList(V__ITEM,V__LIST) => (? [V__NUMBER] : (s__ListOrderFn(V__LIST,V__NUMBER) = V__ITEM))) )	Merge.kif 3294-3297	If ?ITEM is a member of ?LIST, then there exists ?NUMBER such that ?NUMBERth element of ?LIST is equal to ?ITEM
( ! [V__LIST] : (s__instance(V__LIST,s__UniqueList) => (! [V__NUMBER1,V__NUMBER2] : ((s__ListOrderFn(V__LIST,V__NUMBER1) = s__ListOrderFn(V__LIST,V__NUMBER2)) => (V__NUMBER1 = V__NUMBER2)))) )	Merge.kif 3081-3086	If ?LIST is an instance of unique list, then for all ?NUMBER1 and ?NUMBER2 if ?NUMBER1th element of ?LIST is equal to ?NUMBER2th element of ?LIST, then ?NUMBER1 is equal to ?NUMBER2
( ! [V__REL,V__ARG,V__COUNT,V__EL,V__ARGS1] : (s__maxCardinality(V__REL,V__ARG,V__COUNT) => lesseq(s__CardinalityFn(s__KappaFn(V__EL,'(V__REL(V__ARGS1) & (V__EL = s__ListOrderFn(s__ListFn_1(V__ARGS1),V__ARG)))')) ,V__COUNT)) )	Media.kif 2194-2202	If there can be at most ?COUNT values to argument ?ARG of ?REL, then the number of instances in the class described by ?EL is less than or equal to ?COUNT
( ! [V__REL,V__ARG,V__COUNT,V__EL,V__ARGS1] : (s__minCardinality(V__REL,V__ARG,V__COUNT) => greatereq(s__CardinalityFn(s__KappaFn(V__EL,'(V__REL(V__ARGS1) & (V__EL = s__ListOrderFn(s__ListFn_1(V__ARGS1),V__ARG)))')) ,V__COUNT)) )	Media.kif 2158-2166	If there are at least ?COUNT values to argument ?ARG of ?REL, then the number of instances in the class described by ?EL is greater than or equal to ?COUNT

statement

No TPTP formula. May not be expressible in strict first order.

Merge.kif 3219-3223

For all @ROW and ?ITEM length of (@ROW and ?ITEM)th element of (@ROW and ?ITEM) is equal to ?ITEM

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

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

KB Term:			Term intersection

English Word: