AbsoluteValueFn - Sigma Knowledge base Browser

appearance as argument number 1

s__documentation(s__AbsoluteValueFn__m,s__ChineseLanguage,'"(AbsoluteValueFn ?NUMBER)的值时 RealNumber ?NUMBER 的绝对值。"')	chinese_format.kif 2224-2225
s__documentation(s__AbsoluteValueFn__m,s__EnglishLanguage,'"The value of (AbsoluteValueFn ?NUMBER) is the absolute value of the RealNumber ?NUMBER."')	Merge.kif 4592-4593
s__domain(s__AbsoluteValueFn__m,n__1,s__RealNumber)	Merge.kif 4589-4589	The number 1 argument of absolute value is an instance of real number
s__instance(s__TotalValuedRelation,s__SetOrClass) s__instance(s__AbsoluteValueFn__m,s__TotalValuedRelation)	Merge.kif 4588-4588	Absolute value is an instance of total valued relation
s__instance(s__UnaryFunction,s__SetOrClass) s__instance(s__AbsoluteValueFn__m,s__UnaryFunction)	Merge.kif 4587-4587	Absolute value is an instance of unary function
s__lexicon(s__AbsoluteValueFn__m,s__LexNoun,'"abs"')	engineering.kif 133-133
s__lexicon(s__AbsoluteValueFn__m,s__LexNoun,'"absolute value"')	engineering.kif 134-134
s__range(s__AbsoluteValueFn__m,s__NonnegativeRealNumber)	Merge.kif 4590-4590	The range of absolute value is an instance of nonnegative real number

appearance as argument number 2

s__format(s__ChineseLanguage,s__AbsoluteValueFn__m,'"%1 的绝对值"')	chinese_format.kif 688-688
s__format(s__EnglishLanguage,s__AbsoluteValueFn__m,'"the absolute value of %1"')	english_format.kif 693-693
s__termFormat(s__ChineseLanguage,s__AbsoluteValueFn__m,'"绝对值"')	domainEnglishFormat.kif 5163-5163
s__termFormat(s__ChineseLanguage,s__AbsoluteValueFn__m,'"绝对值函数"')	chinese_format.kif 689-689
s__termFormat(s__ChineseTraditionalLanguage,s__AbsoluteValueFn__m,'"絕對值"')	domainEnglishFormat.kif 5162-5162
s__termFormat(s__EnglishLanguage,s__AbsoluteValueFn__m,'"absolute value"')	domainEnglishFormat.kif 5161-5161

antecedent

( ! [V__NUMBER1,V__NUMBER2] :
   (((((s__AbsoluteValueFn(V__NUMBER1)
           = V__NUMBER2)
         &
         s__instance(V__NUMBER1,s__RealNumber) &
         s__instance(V__NUMBER2,s__RealNumber))
       =>
       ((s__instance(V__NUMBER1,s__NonnegativeRealNumber) &
           (V__NUMBER1 = V__NUMBER2))
         |
         (s__instance(V__NUMBER1,s__NegativeRealNumber) &
           (V__NUMBER2 = s__SubtractionFn(n__0,V__NUMBER1)))))
   &
   (((s__instance(V__NUMBER1,s__NonnegativeRealNumber) &
         (V__NUMBER1 = V__NUMBER2))
       |
       (s__instance(V__NUMBER1,s__NegativeRealNumber) &
         (V__NUMBER2 = s__SubtractionFn(n__0,V__NUMBER1))))
   =>
   ((s__AbsoluteValueFn(V__NUMBER1)
     = V__NUMBER2)
   &
   s__instance(V__NUMBER1,s__RealNumber) &
   s__instance(V__NUMBER2,s__RealNumber))))
)
)

Merge.kif 4595-4606