ListFn - Sigma Knowledge base Browser

appearance as argument number 1

s__documentation(s__ListFn__m,s__ChineseLanguage,'这是一个可以接受任何数量的参数，然后交出含有跟哪些参数完全相同顺序的 Function。')	Merge.kif 3110-3111
s__documentation(s__ListFn__m,s__EnglishLanguage,'A Function that takes any number of arguments and returns the List containing those arguments in exactly the same order.')	Merge.kif 3108-3109
s__domain(s__ListFn__m,1,s__Entity)	Merge.kif 3105-3105	The number 1 argument of list is an instance of entity
s__instance(s__Function,s__SetOrClass) s__instance(s__ListFn__m,s__Function)	Merge.kif 3103-3103	List is an instance of function
s__instance(s__VariableArityRelation,s__SetOrClass) s__instance(s__ListFn__m,s__VariableArityRelation)	Merge.kif 3104-3104	List is an instance of variable arity relation
s__range(s__ListFn__m,s__List)	Merge.kif 3107-3107	The range of list is an instance of list

appearance as argument number 2

s__format(s__ChineseLanguage,s__ListFn__m,'(%*[,])')	chinese_format.kif 261-261
s__format(s__EnglishLanguage,s__ListFn__m,'(%*[,])')	english_format.kif 159-159
s__format(s__FrenchLanguage,s__ListFn__m,'(%*[,])')	french_format.kif 149-149
s__format(s__ItalianLanguage,s__ListFn__m,'(%*[,]')	relations-it.txt 167-167
s__format(s__PortugueseLanguage,s__ListFn__m,'(%*[,])')	portuguese_format.kif 101-101
s__format(s__ar__m,s__ListFn__m,'(%*[])')	arabic_format.kif 97-97
s__format(s__cz__m,s__ListFn__m,'(%*[,])')	relations-cz.txt 158-158
s__format(s__de__m,s__ListFn__m,'(%*[,])')	relations-de.txt 336-336
s__format(s__hi__m,s__ListFn__m,'(%*[,]')	relations-hindi.txt 206-206
s__format(s__tg__m,s__ListFn__m,'(%*[,]')	relations-tg.txt 333-333
s__termFormat(s__ChineseLanguage,s__ListFn__m,'表列函数')	chinese_format.kif 262-262	"表列函数" is the printable form of list in ChineseLanguage
s__termFormat(s__EnglishLanguage,s__ListFn__m,'list')	domainEnglishFormat.kif 6199-6199	"list" is the printable form of list in english language
s__termFormat(s__ar__m,s__ListFn__m,'«قائمة»')	arabic_format.kif 547-547	"«قائمة»" is the printable form of list in ar
s__termFormat(s__tg__m,s__ListFn__m,'tungkulin ng talaan')	relations-tg.txt 334-334	"tungkulin ng talaan" is the printable form of list in tg

antecedent

( ! [V__ROW11,V__ROW21] : ((s__contraryAttribute_1(V__ROW11) & s__identicalListItems(s__ListFn_1(V__ROW11) ,s__ListFn_1(V__ROW21))) => s__contraryAttribute_1(V__ROW21)) )	Merge.kif 520-524	If @ROW1 is the opposite of and (@ROW2) is an identical list items of (@ROW1), then @ROW2 is the opposite of
( ! [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__AGENT,V__ROW1,V__OBJ] : ((s__instance(s__needs__m,s__IntentionalRelation) & s__needs(V__AGENT,V__ROW1) & s__inList(V__OBJ,s__ListFn_1(V__ROW1))) => s__inScopeOfInterest(V__AGENT,V__OBJ)) ) ( ! [V__AGENT,V__ROW1,V__OBJ] : ((s__instance(s__enemy__m,s__IntentionalRelation) & s__enemy(V__AGENT,V__ROW1) & s__inList(V__OBJ,s__ListFn_1(V__ROW1))) => s__inScopeOfInterest(V__AGENT,V__OBJ)) ) ( ! [V__AGENT,V__ROW1,V__OBJ] : ((s__instance(s__disapproves__m,s__IntentionalRelation) & s__disapproves(V__AGENT,V__ROW1) & s__inList(V__OBJ,s__ListFn_1(V__ROW1))) => s__inScopeOfInterest(V__AGENT,V__OBJ)) ) ( ! [V__AGENT,V__ROW1,V__OBJ] : ((s__instance(s__dislikes__m,s__IntentionalRelation) & s__dislikes(V__AGENT,V__ROW1) & s__inList(V__OBJ,s__ListFn_1(V__ROW1))) => s__inScopeOfInterest(V__AGENT,V__OBJ)) ) ( ! [V__AGENT,V__ROW1,V__OBJ] : ((s__instance(s__facebookFriend__m,s__IntentionalRelation) & s__facebookFriend(V__AGENT,V__ROW1) & s__inList(V__OBJ,s__ListFn_1(V__ROW1))) => s__inScopeOfInterest(V__AGENT,V__OBJ)) ) ( ! [V__AGENT,V__ROW1,V__OBJ] : ((s__instance(s__wants__m,s__IntentionalRelation) & s__wants(V__AGENT,V__ROW1) & s__inList(V__OBJ,s__ListFn_1(V__ROW1))) => s__inScopeOfInterest(V__AGENT,V__OBJ)) ) ( ! [V__AGENT,V__ROW1,V__OBJ] : ((s__instance(s__cohabitant__m,s__IntentionalRelation) & s__cohabitant(V__AGENT,V__ROW1) & s__inList(V__OBJ,s__ListFn_1(V__ROW1))) => s__inScopeOfInterest(V__AGENT,V__OBJ)) ) ( ! [V__AGENT,V__ROW1,V__OBJ] : ((s__instance(s__serviceRecipient__m,s__IntentionalRelation) & s__serviceRecipient(V__AGENT,V__ROW1) & s__inList(V__OBJ,s__ListFn_1(V__ROW1))) => s__inScopeOfInterest(V__AGENT,V__OBJ)) ) ( ! [V__AGENT,V__ROW1,V__OBJ] : ((s__instance(s__serviceProvider__m,s__IntentionalRelation) & s__serviceProvider(V__AGENT,V__ROW1) & s__inList(V__OBJ,s__ListFn_1(V__ROW1))) => s__inScopeOfInterest(V__AGENT,V__OBJ)) ) ( ! [V__AGENT,V__ROW1,V__OBJ] : ((s__instance(s__desires__m,s__IntentionalRelation) & s__desires(V__AGENT,V__ROW1) & s__inList(V__OBJ,s__ListFn_1(V__ROW1))) => s__inScopeOfInterest(V__AGENT,V__OBJ)) ) ( ! [V__AGENT,V__ROW1,V__OBJ] : ((s__instance(s__knows__m,s__IntentionalRelation) & s__knows(V__AGENT,V__ROW1) & s__inList(V__OBJ,s__ListFn_1(V__ROW1))) => s__inScopeOfInterest(V__AGENT,V__OBJ)) ) ( ! [V__AGENT,V__ROW1,V__OBJ] : ((s__instance(s__inScopeOfInterest__m,s__IntentionalRelation) & s__inScopeOfInterest(V__AGENT,V__ROW1) & s__inList(V__OBJ,s__ListFn_1(V__ROW1))) => s__inScopeOfInterest(V__AGENT,V__OBJ)) ) ( ! [V__AGENT,V__ROW1,V__OBJ] : ((s__instance(s__domesticPartner__m,s__IntentionalRelation) & s__domesticPartner(V__AGENT,V__ROW1) & s__inList(V__OBJ,s__ListFn_1(V__ROW1))) => s__inScopeOfInterest(V__AGENT,V__OBJ)) ) ( ! [V__AGENT,V__ROW1,V__OBJ] : ((s__instance(s__doubts__m,s__IntentionalRelation) & s__doubts(V__AGENT,V__ROW1) & s__inList(V__OBJ,s__ListFn_1(V__ROW1))) => s__inScopeOfInterest(V__AGENT,V__OBJ)) ) ( ! [V__AGENT,V__ROW1,V__OBJ] : ((s__instance(s__considers__m,s__IntentionalRelation) & s__considers(V__AGENT,V__ROW1) & s__inList(V__OBJ,s__ListFn_1(V__ROW1))) => s__inScopeOfInterest(V__AGENT,V__OBJ)) ) ( ! [V__AGENT,V__ROW1,V__OBJ] : ((s__instance(s__follows__m,s__IntentionalRelation) & s__follows(V__AGENT,V__ROW1) & s__inList(V__OBJ,s__ListFn_1(V__ROW1))) => s__inScopeOfInterest(V__AGENT,V__OBJ)) ) ( ! [V__AGENT,V__ROW1,V__OBJ] : ((s__instance(s__friend__m,s__IntentionalRelation) & s__friend(V__AGENT,V__ROW1) & s__inList(V__OBJ,s__ListFn_1(V__ROW1))) => s__inScopeOfInterest(V__AGENT,V__OBJ)) ) ( ! [V__AGENT,V__ROW1,V__OBJ] : ((s__instance(s__believes__m,s__IntentionalRelation) & s__believes(V__AGENT,V__ROW1) & s__inList(V__OBJ,s__ListFn_1(V__ROW1))) => s__inScopeOfInterest(V__AGENT,V__OBJ)) ) ( ! [V__AGENT,V__ROW1,V__OBJ] : ((s__instance(s__connectedInSocialNetwork__m,s__IntentionalRelation) & s__connectedInSocialNetwork(V__AGENT,V__ROW1) & s__inList(V__OBJ,s__ListFn_1(V__ROW1))) => s__inScopeOfInterest(V__AGENT,V__OBJ)) )	Merge.kif 2836-2841	If ?REL is an instance of intentional relation and ?REL ?AGENT and @ROW and ?OBJ is a member of (@ROW), then ?AGENT is interested in ?OBJ
( ! [V__OBJ1,V__OBJ2,V__ATTR1,V__ROW1,V__ATTR2] : ((s__orientation(V__OBJ1,V__OBJ2,V__ATTR1) & s__contraryAttribute_1(V__ROW1) & s__inList(V__ATTR1,s__ListFn_1(V__ROW1)) & s__inList(V__ATTR2,s__ListFn_1(V__ROW1)) & (~ (V__ATTR1 = V__ATTR2))) => (~ s__orientation(V__OBJ1,V__OBJ2,V__ATTR2))) )	Merge.kif 17100-17108	If ?OBJ1 is ?ATTR1 to ?OBJ2 and @ROW is the opposite of and ?ATTR1 is a member of (@ROW) and ?ATTR2 is a member of (@ROW) and ?ATTR1 is not equal to ?ATTR2, then ?OBJ1 is not ?ATTR2 to ?OBJ2
( ! [V__ROW1,V__Process1,V__Process2,V__Number1,V__Number2] : ((s__processList_1(V__ROW1) & s__inList(V__Process1,s__ListFn_1(V__ROW1)) & s__inList(V__Process2,s__ListFn_1(V__ROW1)) & (s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__Number1) = V__Process1) & (s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__Number2) = V__Process2) & less(V__Number1,V__Number2)) => s__earlier(s__WhenFn(V__Process1) ,s__WhenFn(V__Process2))) )	QoSontology.kif 692-700	If the list of processes @ROW and ?Process1 is a member of (@ROW) and ?Process2 is a member of (@ROW) and ?Number1th element of (@ROW) is equal to ?Process1 and ?Number2th element of (@ROW) is equal to ?Process2 and ?Number1 is less than ?Number2, then the time of existence of ?Process1 happens earlier than the time of existence of ?Process2

consequent

( ! [V__ROW1] : ((s__instance(s__parent__m,s__TotalValuedRelation) & s__instance(s__parent__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__parent__m,s__Relation) & s__valence(s__parent__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__parent__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__parent(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__protonNumber__m,s__TotalValuedRelation) & s__instance(s__protonNumber__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__protonNumber__m,s__Relation) & s__valence(s__protonNumber__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__protonNumber__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__protonNumber(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__lineMeasure__m,s__TotalValuedRelation) & s__instance(s__lineMeasure__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__lineMeasure__m,s__Relation) & s__valence(s__lineMeasure__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__lineMeasure__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__lineMeasure(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__earlier__m,s__TotalValuedRelation) & s__instance(s__earlier__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__earlier__m,s__Relation) & s__valence(s__earlier__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__earlier__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__earlier(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__conclusion__m,s__TotalValuedRelation) & s__instance(s__conclusion__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__conclusion__m,s__Relation) & s__valence(s__conclusion__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__conclusion__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__conclusion(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__coordinates__m,s__TotalValuedRelation) & s__instance(s__coordinates__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__coordinates__m,s__Relation) & s__valence(s__coordinates__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__coordinates__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__coordinates(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__subCollection__m,s__TotalValuedRelation) & s__instance(s__subCollection__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__subCollection__m,s__Relation) & s__valence(s__subCollection__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__subCollection__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__subCollection(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__meetsTemporally__m,s__TotalValuedRelation) & s__instance(s__meetsTemporally__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__meetsTemporally__m,s__Relation) & s__valence(s__meetsTemporally__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__meetsTemporally__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__meetsTemporally(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__subrelation__m,s__TotalValuedRelation) & s__instance(s__subrelation__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__subrelation__m,s__Relation) & s__valence(s__subrelation__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__subrelation__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__subrelation(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(greater__m,s__TotalValuedRelation) & s__instance(greater__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(greater__m,s__Relation) & s__valence(greater__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(greater__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : greater(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__subAttribute__m,s__TotalValuedRelation) & s__instance(s__subAttribute__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__subAttribute__m,s__Relation) & s__valence(s__subAttribute__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__subAttribute__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__subAttribute(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__subclass__m,s__TotalValuedRelation) & s__instance(s__subclass__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__subclass__m,s__Relation) & s__valence(s__subclass__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__subclass__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__subclass(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__larger__m,s__TotalValuedRelation) & s__instance(s__larger__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__larger__m,s__Relation) & s__valence(s__larger__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__larger__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__larger(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__maximumPayloadCapacity__m,s__TotalValuedRelation) & s__instance(s__maximumPayloadCapacity__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__maximumPayloadCapacity__m,s__Relation) & s__valence(s__maximumPayloadCapacity__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__maximumPayloadCapacity__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__maximumPayloadCapacity(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(lesseq__m,s__TotalValuedRelation) & s__instance(lesseq__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(lesseq__m,s__Relation) & s__valence(lesseq__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(lesseq__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : lesseq(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__partlyLocated__m,s__TotalValuedRelation) & s__instance(s__partlyLocated__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__partlyLocated__m,s__Relation) & s__valence(s__partlyLocated__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__partlyLocated__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__partlyLocated(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(greatereq__m,s__TotalValuedRelation) & s__instance(greatereq__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(greatereq__m,s__Relation) & s__valence(greatereq__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(greatereq__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : greatereq(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__moves__m,s__TotalValuedRelation) & s__instance(s__moves__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__moves__m,s__Relation) & s__valence(s__moves__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__moves__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__moves(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__beforeOrEqual__m,s__TotalValuedRelation) & s__instance(s__beforeOrEqual__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__beforeOrEqual__m,s__Relation) & s__valence(s__beforeOrEqual__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__beforeOrEqual__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__beforeOrEqual(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__eventLocated__m,s__TotalValuedRelation) & s__instance(s__eventLocated__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__eventLocated__m,s__Relation) & s__valence(s__eventLocated__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__eventLocated__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__eventLocated(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__smaller__m,s__TotalValuedRelation) & s__instance(s__smaller__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__smaller__m,s__Relation) & s__valence(s__smaller__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__smaller__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__smaller(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__diameter__m,s__TotalValuedRelation) & s__instance(s__diameter__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__diameter__m,s__Relation) & s__valence(s__diameter__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__diameter__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__diameter(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__electronNumber__m,s__TotalValuedRelation) & s__instance(s__electronNumber__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__electronNumber__m,s__Relation) & s__valence(s__electronNumber__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__electronNumber__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__electronNumber(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__personTransportCapability__m,s__TotalValuedRelation) & s__instance(s__personTransportCapability__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__personTransportCapability__m,s__Relation) & s__valence(s__personTransportCapability__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__personTransportCapability__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__personTransportCapability(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__abstractPart__m,s__TotalValuedRelation) & s__instance(s__abstractPart__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__abstractPart__m,s__Relation) & s__valence(s__abstractPart__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__abstractPart__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__abstractPart(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__transactionAmount__m,s__TotalValuedRelation) & s__instance(s__transactionAmount__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__transactionAmount__m,s__Relation) & s__valence(s__transactionAmount__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__transactionAmount__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__transactionAmount(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__time__m,s__TotalValuedRelation) & s__instance(s__time__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__time__m,s__Relation) & s__valence(s__time__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__time__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__time(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__caliber__m,s__TotalValuedRelation) & s__instance(s__caliber__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__caliber__m,s__Relation) & s__valence(s__caliber__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__caliber__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__caliber(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__graphPart__m,s__TotalValuedRelation) & s__instance(s__graphPart__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__graphPart__m,s__Relation) & s__valence(s__graphPart__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__graphPart__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__graphPart(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__geometricPart__m,s__TotalValuedRelation) & s__instance(s__geometricPart__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__geometricPart__m,s__Relation) & s__valence(s__geometricPart__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__geometricPart__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__geometricPart(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__changesLocation__m,s__TotalValuedRelation) & s__instance(s__changesLocation__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__changesLocation__m,s__Relation) & s__valence(s__changesLocation__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__changesLocation__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__changesLocation(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__temporalPart__m,s__TotalValuedRelation) & s__instance(s__temporalPart__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__temporalPart__m,s__Relation) & s__valence(s__temporalPart__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__temporalPart__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__temporalPart(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__path__m,s__TotalValuedRelation) & s__instance(s__path__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__path__m,s__Relation) & s__valence(s__path__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__path__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__path(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__premise__m,s__TotalValuedRelation) & s__instance(s__premise__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__premise__m,s__Relation) & s__valence(s__premise__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__premise__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__premise(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__subsumesContentClass__m,s__TotalValuedRelation) & s__instance(s__subsumesContentClass__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__subsumesContentClass__m,s__Relation) & s__valence(s__subsumesContentClass__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__subsumesContentClass__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__subsumesContentClass(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__subProcess__m,s__TotalValuedRelation) & s__instance(s__subProcess__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__subProcess__m,s__Relation) & s__valence(s__subProcess__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__subProcess__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__subProcess(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__radius__m,s__TotalValuedRelation) & s__instance(s__radius__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__radius__m,s__Relation) & s__valence(s__radius__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__radius__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__radius(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__subsumesContentInstance__m,s__TotalValuedRelation) & s__instance(s__subsumesContentInstance__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__subsumesContentInstance__m,s__Relation) & s__valence(s__subsumesContentInstance__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__subsumesContentInstance__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__subsumesContentInstance(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__contestParticipant__m,s__TotalValuedRelation) & s__instance(s__contestParticipant__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__contestParticipant__m,s__Relation) & s__valence(s__contestParticipant__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__contestParticipant__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__contestParticipant(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__stringLength__m,s__TotalValuedRelation) & s__instance(s__stringLength__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__stringLength__m,s__Relation) & s__valence(s__stringLength__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__stringLength__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__stringLength(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__subList__m,s__TotalValuedRelation) & s__instance(s__subList__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__subList__m,s__Relation) & s__valence(s__subList__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__subList__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__subList(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__angularMeasure__m,s__TotalValuedRelation) & s__instance(s__angularMeasure__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__angularMeasure__m,s__Relation) & s__valence(s__angularMeasure__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__angularMeasure__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__angularMeasure(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__subLanguage__m,s__TotalValuedRelation) & s__instance(s__subLanguage__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__subLanguage__m,s__Relation) & s__valence(s__subLanguage__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__subLanguage__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__subLanguage(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__duration__m,s__TotalValuedRelation) & s__instance(s__duration__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__duration__m,s__Relation) & s__valence(s__duration__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__duration__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__duration(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__initialList__m,s__TotalValuedRelation) & s__instance(s__initialList__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__initialList__m,s__Relation) & s__valence(s__initialList__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__initialList__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__initialList(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__subString__m,s__TotalValuedRelation) & s__instance(s__subString__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__subString__m,s__Relation) & s__valence(s__subString__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__subString__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__subString(V__ROW1,V__ITEM)))))) )	Merge.kif 2308-2325	?REL is an instance of total valued relation and ?REL is an instance of predicate if and only if there exists ?VALENCE such that ?REL is an instance of relation and ?REL %&has ?VALENCE argument(s) and if for all ?NUMBER, ?ELEMENT and ?CLASS if ?NUMBER is less than ?VALENCE and the number ?NUMBER argument of ?REL is an instance of ?CLASS and ?ELEMENT is equal to ?NUMBERth element of (@ROW), then ?ELEMENT is an instance of ?CLASS , then there exists ?ITEM such that ?REL @ROW and ?ITEM
( ! [V__ROW1,V__ELEMENT] : (s__GreatestCommonDivisorFn_1(V__ROW1) => (s__inList(V__ELEMENT,s__ListFn_1(V__ROW1)) => s__instance(V__ELEMENT,s__Number))) )	Merge.kif 4984-4989	If the greatest common divisor of @ROW, then if ?ELEMENT is a member of (@ROW), then ?ELEMENT is an instance of number
( ! [V__ROW1,V__ELEMENT] : (s__LeastCommonMultipleFn_1(V__ROW1) => (s__inList(V__ELEMENT,s__ListFn_1(V__ROW1)) => s__instance(V__ELEMENT,s__Number))) )	Merge.kif 5063-5068	If the least common multiple of @ROW, then if ?ELEMENT is a member of (@ROW), then ?ELEMENT is an instance of number
( ! [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__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__NUMBER] : ((s__valence(s__contraryAttribute__m,V__NUMBER) & s__instance(s__contraryAttribute__m,s__Predicate)) => (! [V__ROW1] : (s__contraryAttribute_1(V__ROW1) => (s__ListLengthFn(s__ListFn_1(V__ROW1)) = V__NUMBER)))) )	Merge.kif 3225-3232	If ?REL %&has ?NUMBER argument(s) and ?REL is an instance of predicate, then for all @ROW if ?REL @ROW, then length of (@ROW) is equal to ?NUMBER
( ! [V__ROW1,V__ELEMENT] : (s__contraryAttribute_1(V__ROW1) => (s__inList(V__ELEMENT,s__ListFn_1(V__ROW1)) => s__instance(V__ELEMENT,s__Attribute))) )	Merge.kif 514-518	If @ROW is the opposite of , then if ?ELEMENT is a member of (@ROW), then ?ELEMENT is an instance of attribute
( ! [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__CLASS,V__ROW1] : (s__disjointDecomposition_2(V__CLASS,V__ROW1) => (! [V__ITEM] : (s__inList(V__ITEM,s__ListFn_1(V__ROW1)) => s__subclass(V__ITEM,V__CLASS)))) )	Merge.kif 3123-3128	If ?CLASS is disjointly decomposed into @ROW, then for all ?ITEM if ?ITEM is a member of (@ROW), then ?ITEM is a subclass of ?CLASS
( ! [V__CLASS,V__ROW1] : (s__disjointDecomposition_2(V__CLASS,V__ROW1) => (! [V__ITEM1,V__ITEM2] : ((s__inList(V__ITEM1,s__ListFn_1(V__ROW1)) & s__inList(V__ITEM2,s__ListFn_1(V__ROW1)) & (~ (V__ITEM1 = V__ITEM2))) => s__disjoint(V__ITEM1,V__ITEM2)))) )	Merge.kif 3130-3139	If ?CLASS is disjointly decomposed into @ROW, then for all ?ITEM1 and ?ITEM2 if ?ITEM1 is a member of (@ROW) and ?ITEM2 is a member of (@ROW) and ?ITEM1 is not equal to ?ITEM2, then ?ITEM1 is disjoint from ?ITEM2
( ! [V__ROW1,V__ELEMENT] : (s__disjointDecomposition_1(V__ROW1) => (s__inList(V__ELEMENT,s__ListFn_1(V__ROW1)) => s__instance(V__ELEMENT,s__Class))) )	Merge.kif 614-618	If @ROW is disjointly decomposed into @ROW, then if ?ELEMENT is a member of (@ROW), then ?ELEMENT is an instance of class
( ! [V__ROW1,V__NUMBER] : ((s__GreatestCommonDivisorFn_1(V__ROW1) = V__NUMBER) => (! [V__ELEMENT] : (s__inList(V__ELEMENT,s__ListFn_1(V__ROW1)) => (s__RemainderFn(V__ELEMENT,V__NUMBER) = 0)))) )	Merge.kif 4991-4996	If the greatest common divisor of @ROW is equal to ?NUMBER, then for all ?ELEMENT if ?ELEMENT is a member of (@ROW), then ?ELEMENT mod ?NUMBER is equal to 0
( ! [V__ROW1,V__NUMBER] : ((s__GreatestCommonDivisorFn_1(V__ROW1) = V__NUMBER) => (~ (? [V__GREATER] : (greater(V__GREATER,V__NUMBER) & (! [V__ELEMENT] : (s__inList(V__ELEMENT,s__ListFn_1(V__ROW1)) => (s__RemainderFn(V__ELEMENT,V__GREATER) = 0))))))) )	Merge.kif 4998-5006	If the greatest common divisor of @ROW is equal to ?NUMBER, then there doesn't exist ?GREATER such that ?GREATER is greater than ?NUMBER and for all ?ELEMENT if ?ELEMENT is a member of (@ROW), then ?ELEMENT mod ?GREATER is equal to 0
( ! [V__ROW1,V__NUMBER] : ((s__LeastCommonMultipleFn_1(V__ROW1) = V__NUMBER) => (! [V__ELEMENT] : (s__inList(V__ELEMENT,s__ListFn_1(V__ROW1)) => (s__RemainderFn(V__NUMBER,V__ELEMENT) = 0)))) )	Merge.kif 5070-5075	If the least common multiple of @ROW is equal to ?NUMBER, then for all ?ELEMENT if ?ELEMENT is a member of (@ROW), then ?NUMBER mod ?ELEMENT is equal to 0
( ! [V__ROW1,V__NUMBER] : ((s__LeastCommonMultipleFn_1(V__ROW1) = V__NUMBER) => (~ (? [V__LESS] : (less(V__LESS,V__NUMBER) & (! [V__ELEMENT] : (s__inList(V__ELEMENT,s__ListFn_1(V__ROW1)) => (s__RemainderFn(V__LESS,V__ELEMENT) = 0))))))) )	Merge.kif 5077-5085	If the least common multiple of @ROW is equal to ?NUMBER, then there doesn't exist ?LESS such that ?LESS is less than ?NUMBER and for all ?ELEMENT if ?ELEMENT is a member of (@ROW), then ?LESS mod ?ELEMENT is equal to 0
( ! [V__LIST1,V__LIST2,V__ROW11,V__ROW21] : ((V__LIST1 = V__LIST2) => (((V__LIST1 = s__ListFn_1(V__ROW11)) & (V__LIST2 = s__ListFn_1(V__ROW21))) => (! [V__NUMBER] : (s__ListOrderFn(s__ListFn_1(V__ROW11) ,V__NUMBER) = s__ListOrderFn(s__ListFn_1(V__ROW21) ,V__NUMBER))))) )	Merge.kif 326-333	If ?LIST1 is equal to ?LIST2, then if ?LIST1 is equal to (@ROW1) and ?LIST2 is equal to (@ROW2), then for all ?NUMBER ?NUMBERth element of (@ROW1) is equal to ?NUMBERth element of (@ROW2)
( ! [V__REL,V__ARG,V__COUNT,V__EL,V__ARGS1] : (s__exactCardinality(V__REL,V__ARG,V__COUNT) => (s__CardinalityFn(s__KappaFn(V__EL,'(V__REL(V__ARGS1) & (V__EL = s__ListOrderFn(s__ListFn_1(V__ARGS1),V__ARG)))')) = V__COUNT)) )	Media.kif 2123-2131	If there can be ?COUNT values to argument ?ARG of ?REL, then the number of instances in the class described by ?EL is equal to ?COUNT
( ! [V__ATTRCLASS,V__ROW1] : (s__exhaustiveAttribute_2(V__ATTRCLASS,V__ROW1) => (~ (? [V__EL] : (s__instance(V__EL,V__ATTRCLASS) & (~ (? [V__ATTR,V__NUMBER] : ((V__EL = V__ATTR) & (V__ATTR = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))))))))) )	Merge.kif 568-580	If @ROW are all the attributes of ?ATTRCLASS, then there doesn't exist ?EL such that ?EL is an instance of ?ATTRCLASS and there don't exist ?ATTR and ?NUMBER such that ?EL is equal to ?ATTR and ?ATTR is equal to ?NUMBERth element of (@ROW)
( ! [V__CLASS,V__ROW1,V__ATTR] : (s__exhaustiveAttribute_2(V__CLASS,V__ROW1) => (s__inList(V__ATTR,s__ListFn_1(V__ROW1)) => s__instance(V__ATTR,s__Attribute))) )	Merge.kif 552-556	If @ROW are all the attributes of ?CLASS, then if ?ATTR is a member of (@ROW), then ?ATTR is an instance of attribute
( ! [V__CLASS,V__ROW1] : (s__exhaustiveAttribute_2(V__CLASS,V__ROW1) => (! [V__ATTR1] : (s__instance(V__ATTR1,V__CLASS) => (? [V__ATTR2] : (s__inList(V__ATTR2,s__ListFn_1(V__ROW1)) & (V__ATTR1 = V__ATTR2)))))) )	Merge.kif 558-566	If @ROW are all the attributes of ?CLASS, then for all ?ATTR1 if ?ATTR1 is an instance of ?CLASS, then there exists ?ATTR2 such that ?ATTR2 is a member of (@ROW) and ?ATTR1 is equal to ?ATTR2

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25

statement

No TPTP formula. May not be expressible in strict first order.	Merge.kif 3214-3217	For all @ROW and ?ITEM length of (@ROW and ?ITEM) is equal to (length of (@ROW)+1)
No TPTP formula. May not be expressible in strict first order.	Merge.kif 3219-3223	For all @ROW and ?ITEM length of (@ROW and ?ITEM)th element of (@ROW and ?ITEM) is equal to ?ITEM
(! [V__ROW1,V__ITEM] : s__initialList(s__ListFn_1(V__ROW1) ,s__ListFn_2(V__ROW1,V__ITEM)))	Merge.kif 3372-3373	For all @ROW and ?ITEM (@ROW) starts (@ROW and ?ITEM)

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

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

KB Term:			Term intersection

English Word: