( ! [V__LIST3,V__LIST1,V__LIST2] :
(((s__instance(V__LIST3,s__List) &
s__instance(V__LIST1,s__List) &
s__instance(V__LIST2,s__List))
=>
(((((V__LIST3 = s__ListConcatenateFn(V__LIST1,V__LIST2))
&
~((V__LIST1 = s__NullList))
&
~((V__LIST2 = s__NullList)))
=>
( ! [V__NUMBER1, V__NUMBER2] :
(((s__lessThanOrEqualTo(V__NUMBER1,s__ListLengthFn(V__LIST1))
&
s__lessThanOrEqualTo(V__NUMBER2,s__ListLengthFn(V__LIST2))
&
s__instance(V__NUMBER1,s__PositiveInteger) &
s__instance(V__NUMBER2,s__PositiveInteger))
=>
(((s__ListOrderFn(V__LIST3,V__NUMBER1)
= s__ListOrderFn(V__LIST1,V__NUMBER1))
&
(s__ListOrderFn(V__LIST3,s__AdditionFn(s__ListLengthFn(V__LIST1)
,V__NUMBER2))
= s__ListOrderFn(V__LIST2,V__NUMBER2))))))))
&
(( ! [V__NUMBER1, V__NUMBER2] :
(((s__lessThanOrEqualTo(V__NUMBER1,s__ListLengthFn(V__LIST1))
&
s__lessThanOrEqualTo(V__NUMBER2,s__ListLengthFn(V__LIST2))
&
s__instance(V__NUMBER1,s__PositiveInteger) &
s__instance(V__NUMBER2,s__PositiveInteger))
=>
(((s__ListOrderFn(V__LIST3,V__NUMBER1)
= s__ListOrderFn(V__LIST1,V__NUMBER1))
&
(s__ListOrderFn(V__LIST3,s__AdditionFn(s__ListLengthFn(V__LIST1)
,V__NUMBER2))
= s__ListOrderFn(V__LIST2,V__NUMBER2)))))))
=>
((V__LIST3 = s__ListConcatenateFn(V__LIST1,V__LIST2))
&
~((V__LIST1 = s__NullList))
&
~((V__LIST2 = s__NullList)))))))
)
)
|
Merge.kif 2979-2995 |
A list is equal to the list composed of another list and a third list and the other list is not equal to null list and the third list is not equal to null list if and only if for all a positive integer and another positive integer |
( ! [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 285-306 |
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 |
( ! [V__NUMBER1,V__NUMBER2,V__NUMBER] :
(((s__instance(V__NUMBER1,s__Integer) &
s__instance(V__NUMBER2,s__Integer) &
s__instance(V__NUMBER,s__Integer))
=>
((((s__RemainderFn(V__NUMBER1,V__NUMBER2)
= V__NUMBER)
=>
(s__AdditionFn(s__MultiplicationFn(s__FloorFn(s__DivisionFn(V__NUMBER1,V__NUMBER2))
,V__NUMBER2)
,V__NUMBER)
= V__NUMBER1))
&
((s__AdditionFn(s__MultiplicationFn(s__FloorFn(s__DivisionFn(V__NUMBER1,V__NUMBER2))
,V__NUMBER2)
,V__NUMBER)
= V__NUMBER1)
=>
(s__RemainderFn(V__NUMBER1,V__NUMBER2)
= V__NUMBER)))))
)
)
|
Merge.kif 4908-4910 |
An integer mod another integer is equal to a third integer if and only if (the largest integer less than or equal to the integer and the other integer and the other integer and the third integer) is equal to the integer |
( ! [V__DEGREE,V__OBJ1,V__OBJ2,V__MAGDEGREE,V__AREA,V__DIRECTION] :
(((s__instance(V__DEGREE,s__Number) &
s__instance(V__DEGREE,s__PlaneAngleMeasure) &
s__instance(V__OBJ1,s__Physical) &
s__instance(V__OBJ2,s__Physical) &
s__instance(V__MAGDEGREE,s__Number) &
s__instance(V__MAGDEGREE,s__PlaneAngleMeasure) &
s__instance(V__AREA,s__GeographicArea) &
s__instance(V__DIRECTION,s__DirectionalAttribute))
=>
(((s__courseWRTMagneticNorth(V__OBJ1,V__OBJ2,V__MAGDEGREE)
&
s__partlyLocated(V__OBJ1,V__AREA)
&
s__partlyLocated(V__OBJ2,V__AREA)
&
s__magneticVariation(V__AREA,V__DEGREE,V__DIRECTION))
=>
(( ? [V__DIFFDEGREE, V__TRUEDEGREE] :
((s__instance(V__DIFFDEGREE,s__Number) &
s__instance(V__TRUEDEGREE,s__PlaneAngleMeasure) &
((((V__DIRECTION = s__East) &
(V__DIFFDEGREE = s__AdditionFn(V__MAGDEGREE,V__DEGREE)))
=>
(s__courseWRTTrueNorth(V__OBJ1,V__OBJ2,V__TRUEDEGREE)))
&
(((V__DIRECTION = s__West) &
(V__DIFFDEGREE = s__SubtractionFn(V__MAGDEGREE,V__DEGREE)))
=>
(s__courseWRTTrueNorth(V__OBJ1,V__OBJ2,V__TRUEDEGREE)))))))))))
)
)
|
Geography.kif 3675-3692 |
|
( ! [V__SUM,V__NUMBER1,V__NUMBER2,V__ARC1,V__PATH,V__ARC2] :
(((s__instance(V__SUM,s__Number) &
s__instance(V__NUMBER1,s__Number) &
s__instance(V__NUMBER2,s__Number) &
s__instance(V__ARC1,s__GraphArc) &
s__instance(V__PATH,s__GraphPath) &
s__instance(V__ARC2,s__GraphArc))
=>
((((s__PathWeightFn(V__PATH)
= V__SUM)
&
s__graphPart(V__ARC1,V__PATH)
&
s__graphPart(V__ARC2,V__PATH)
&
s__arcWeight(V__ARC1,V__NUMBER1)
&
s__arcWeight(V__ARC2,V__NUMBER2)
&
( ! [V__ARC3] :
((s__instance(V__ARC3,s__GraphElement) =>
((s__graphPart(V__ARC3,V__PATH)
=>
(((V__ARC3 = V__ARC1)
|
(V__ARC3 = V__ARC2)))))))))
=>
((s__PathWeightFn(V__PATH)
= s__AdditionFn(V__NUMBER1,V__NUMBER2))))))
)
)
|
Merge.kif 5727-5740 |
|
( ! [V__SUM,V__NUMBER1,V__SUBPATH,V__ARC1,V__PATH] :
(((s__instance(V__SUM,s__Number) &
s__instance(V__NUMBER1,s__Number) &
s__instance(V__SUBPATH,s__GraphPath) &
s__instance(V__ARC1,s__GraphArc) &
s__instance(V__PATH,s__GraphPath))
=>
((((s__PathWeightFn(V__PATH)
= V__SUM)
&
s__subGraph(V__SUBPATH,V__PATH)
&
s__graphPart(V__ARC1,V__PATH)
&
s__arcWeight(V__ARC1,V__NUMBER1)
&
( ! [V__ARC2] :
((s__instance(V__ARC2,s__GraphElement) =>
((s__graphPart(V__ARC2,V__PATH)
=>
((s__graphPart(V__ARC2,V__SUBPATH)
|
(V__ARC2 = V__ARC1)))))))))
=>
((V__SUM = s__AdditionFn(s__PathWeightFn(V__SUBPATH)
,V__NUMBER1))))))
)
)
|
Merge.kif 5713-5725 |
|
( ! [V__A,V__L] :
(((s__instance(V__A,s__Number) &
s__instance(V__L,s__List))
=>
((((V__A = s__ListSumFn(V__L))
&
s__greaterThan(s__ListLengthFn(V__L)
,n__1))
=>
((V__A = s__AdditionFn(s__FirstFn(V__L)
,s__ListSumFn(s__SubListFn(n__2,s__ListLengthFn(V__L)
,V__L))))))))
)
)
|
Merge.kif 3149-3159 |
|
( ! [V__OUT,V__IN,V__S,V__PIVOT,V__LEN,V__NEW,V__N] :
(((s__instance(V__OUT,s__SymbolicString) &
s__instance(V__IN,s__SymbolicString) &
s__instance(V__S,s__SymbolicString) &
s__instance(V__PIVOT,s__Integer) &
s__instance(V__LEN,s__NonnegativeInteger) &
s__instance(V__NEW,s__NonnegativeInteger) &
s__instance(V__N,s__NonnegativeInteger))
=>
((((V__OUT = s__ReverseFn(V__IN))
&
(V__LEN = s__StringLengthFn(V__IN))
&
s__greaterThan(V__LEN,n__1)
&
s__greaterThan(V__N,n__0)
&
s__lessThan(V__N,V__LEN)
&
(V__PIVOT = s__CeilingFn(s__DivisionFn(s__SubtractionFn(V__LEN,n__1)
,n__2)))
&
(V__NEW = s__AdditionFn(s__SubtractionFn(V__PIVOT,V__N)
,V__PIVOT))
&
(V__S = s__SubstringFn(V__IN,V__N,s__AdditionFn(n__1,V__N))))
=>
((V__S = s__SubstringFn(V__OUT,V__NEW,s__AdditionFn(n__1,V__NEW)))))))
)
)
|
Media.kif 3038-3059 |
|
( ! [V__R,V__S,V__E,V__L] :
(((s__instance(V__R,s__List) &
s__instance(V__S,s__Integer) &
s__instance(V__E,s__Integer) &
s__instance(V__L,s__List))
=>
((((V__R = s__SubListFn(V__S,V__E,V__L))
&
s__greaterThan(s__SubtractionFn(V__E,V__S)
,n__1))
=>
((V__R = s__ListConcatenateFn(s__ListFn__1Fn(s__ListOrderFn(V__L,V__S))
,s__SubListFn(s__AdditionFn(n__1,V__S)
,V__E,V__L)))))))
)
)
|
Merge.kif 3085-3097 |
|
( ! [V__VA,V__L,V__M] :
(((s__instance(V__VA,s__Number) &
s__instance(V__L,s__List) &
s__instance(V__M,s__Number))
=>
((((V__VA = s__VarianceAverageFn(V__M,V__L))
&
s__greaterThan(s__ListLengthFn(V__L)
,n__1))
=>
((V__VA = s__AdditionFn(s__VarianceAverageFn(V__M,s__ListOrderFn(V__L,n__1))
,s__VarianceAverageFn(V__M,s__SubListFn(n__2,s__ListLengthFn(V__L)
,V__L))))))))
)
)
|
Weather.kif 1452-1464 |
|
( ! [V__LAND,V__WATER,V__AREA,V__UNIT] :
(((s__instance(V__LAND,s__RealNumber) &
s__instance(V__WATER,s__RealNumber) &
s__instance(V__AREA,s__GeographicArea))
=>
(((s__instance(V__UNIT,s__UnitOfArea) &
s__landAreaOnly(V__AREA,s__MeasureFn(V__LAND,V__UNIT))
&
s__waterAreaOnly(V__AREA,s__MeasureFn(V__WATER,V__UNIT)))
=>
(s__totalArea(V__AREA,s__MeasureFn(s__AdditionFn(V__LAND,V__WATER)
,V__UNIT))))))
)
)
|
Geography.kif 562-567 |
|
( ! [V__LENGTH1,V__LENGTH2,V__AREA,V__LENGTH,V__UNIT] :
(((s__instance(V__LENGTH1,s__RealNumber) &
s__instance(V__LENGTH2,s__RealNumber) &
s__instance(V__AREA,s__GeographicArea) &
s__instance(V__LENGTH,s__RealNumber))
=>
(((s__totalLengthOfHighwaySystem(V__AREA,s__MeasureFn(V__LENGTH,V__UNIT))
&
s__lengthOfPavedHighway(V__AREA,s__MeasureFn(V__LENGTH1,V__UNIT))
&
s__lengthOfUnpavedHighway(V__AREA,s__MeasureFn(V__LENGTH2,V__UNIT))
&
s__instance(V__UNIT,s__UnitOfLength))
=>
(s__totalLengthOfHighwaySystem(V__AREA,s__MeasureFn(s__AdditionFn(V__LENGTH1,V__LENGTH2)
,V__UNIT))))))
)
)
|
Transportation.kif 510-517 |
|
( ! [V__LENGTH1,V__LENGTH2,V__AREA,V__LENGTH] :
(((s__instance(V__LENGTH1,s__Number) &
s__instance(V__LENGTH1,s__LengthMeasure) &
s__instance(V__LENGTH2,s__Number) &
s__instance(V__LENGTH2,s__LengthMeasure) &
s__instance(V__AREA,s__GeographicArea) &
s__instance(V__LENGTH,s__Number) &
s__instance(V__LENGTH,s__LengthMeasure))
=>
(((s__totalLengthOfHighwaySystem(V__AREA,V__LENGTH)
&
s__lengthOfPavedHighway(V__AREA,V__LENGTH1)
&
s__lengthOfUnpavedHighway(V__AREA,V__LENGTH2))
=>
((V__LENGTH = s__AdditionFn(V__LENGTH1,V__LENGTH2))))))
)
)
|
Transportation.kif 503-508 |
|
( ! [V__COMPOUND2,V__COMPOUND1] :
(((s__instance(V__COMPOUND2,s__CompoundSubstance) &
s__instance(V__COMPOUND1,s__CompoundSubstance))
=>
((s__conjugate(V__COMPOUND1,V__COMPOUND2)
=>
(( ? [V__NUMBER1, V__NUMBER2] :
((s__instance(V__NUMBER1,s__PositiveInteger) &
s__instance(V__NUMBER2,s__PositiveInteger) &
(s__protonNumber(V__COMPOUND1,V__NUMBER1)
&
s__protonNumber(V__COMPOUND2,V__NUMBER2)
&
((V__NUMBER1 = s__AdditionFn(V__NUMBER2,n__1))
|
(V__NUMBER2 = s__AdditionFn(V__NUMBER1,n__1)))))))))))
)
)
|
Mid-level-ontology.kif 6122-6130 |
|
( ! [V__TIME2,V__TIME1] :
(((s__instance(V__TIME2,s__Number) &
s__instance(V__TIME2,s__TimePosition) &
s__instance(V__TIME1,s__Number) &
s__instance(V__TIME1,s__TimePosition))
=>
(((s__RelativeTimeFn(V__TIME1,s__CentralTimeZone) = V__TIME2)
=>
((V__TIME2 = s__AdditionFn(V__TIME1,s__MeasureFn(n__6,s__HourDuration)))))))
)
)
|
Merge.kif 16407-16409 |
|
( ! [V__TIME2,V__TIME1] :
(((s__instance(V__TIME2,s__Number) &
s__instance(V__TIME2,s__TimePosition) &
s__instance(V__TIME1,s__Number) &
s__instance(V__TIME1,s__TimePosition))
=>
(((s__RelativeTimeFn(V__TIME1,s__EasternTimeZone) = V__TIME2)
=>
((V__TIME2 = s__AdditionFn(V__TIME1,s__MeasureFn(n__5,s__HourDuration)))))))
)
)
|
Merge.kif 16415-16417 |
|
( ! [V__TIME2,V__TIME1] :
(((s__instance(V__TIME2,s__Number) &
s__instance(V__TIME2,s__TimePosition) &
s__instance(V__TIME1,s__Number) &
s__instance(V__TIME1,s__TimePosition))
=>
(((s__RelativeTimeFn(V__TIME1,s__MountainTimeZone) = V__TIME2)
=>
((V__TIME2 = s__AdditionFn(V__TIME1,s__MeasureFn(n__7,s__HourDuration)))))))
)
)
|
Merge.kif 16399-16401 |
|
( ! [V__TIME2,V__TIME1] :
(((s__instance(V__TIME2,s__Number) &
s__instance(V__TIME2,s__TimePosition) &
s__instance(V__TIME1,s__Number) &
s__instance(V__TIME1,s__TimePosition))
=>
(((s__RelativeTimeFn(V__TIME1,s__PacificTimeZone) = V__TIME2)
=>
((V__TIME2 = s__AdditionFn(V__TIME1,s__MeasureFn(n__8,s__HourDuration)))))))
)
)
|
Merge.kif 16388-16393 |
|
( ! [V__1,V__LIST,V__T1,V__T2,V__N] :
(((s__instance(V__1,s__Number) &
s__instance(V__T1,s__TimeInterval) &
s__instance(V__T2,s__TimeInterval) &
s__instance(V__N,s__Number) &
s__instance(V__N,s__List))
=>
((s__instance(V__LIST,s__ConsecutiveTimeIntervalList) =>
(((V__T1 = s__ListOrderFn(V__N,V__LIST))
&
(V__T2 = s__ListOrderFn(s__AdditionFn(V__N,V__1)
,V__LIST))
&
(s__BeginFn(V__T2)
= s__EndFn(V__T1)))))))
)
)
|
Weather.kif 1934-1943 |
|
