OpenMath Content Dictionary: integer1

Canonical URL:
http://www.openmath.org/cd/integer1.ocd
CD File:
integer1.ocd
CD as XML Encoded OpenMath:
integer1.omcd
Defines:
factorial, factorof, quotient, remainder
Date:
2001-03-12
Version:
2
Review Date:
2003-04-01
Status:
official
Uses CD:
logic1, quant1, set1, arith1, setname1, relation1, fns1, alg1, interval1

This CD holds a collection of basic integer functions.

This CD is intended to be `compatible' with the corresponding elements in Content MathML.


factorof

This is the binary OpenMath operator that is used to indicate the mathematical relationship a "is a factor of" b, where a is the first argument and b is the second. This relationship is true if and only if b mod a = 0.

Commented Mathematical property (CMP):
b is a factor of a iff remainder of a divided by b = 0
Formal Mathematical property (FMP):
<OMOBJ>
    <OMA>
      <OMS cd="logic1" name="implies"/>
      <OMA>
        <OMS cd="integer1" name="factorof"/>
	<OMV name="b"/>
	<OMV name="a"/>
      </OMA>
      <OMA>
        <OMS cd="relation1" name="eq"/>
	<OMA>
	  <OMS cd="integer1" name="remainder"/>
	  <OMV name="a"/>
	  <OMV name="b"/>
	</OMA>
	<OMS cd="alg1" name="zero"/>
      </OMA>
    </OMA>
  </OMOBJ>

implies (factorof ( b, a) , eq (remainder ( a, b) , zero) )

Signatures:
sts


[Next: factorial] [Last: remainder] [Top]

factorial

The symbol to represent a unary factorial function on non-negative integers.

Commented Mathematical property (CMP):
factorial n = product [1..n]
Formal Mathematical property (FMP):
<OMOBJ>
    <OMA>
      <OMS cd="relation1" name="eq"/>
      <OMA>
        <OMS cd="integer1" name="factorial"/>
        <OMV name="n"/>
      </OMA>
      <OMA>
        <OMS cd="arith1" name="product"/>
          <OMA>
            <OMS cd="interval1" name="integer_interval"/>
            <OMI> 1 </OMI>
            <OMV name="n"/>
          </OMA>
        <OMBIND>
          <OMS cd="fns1" name="lambda"/>
            <OMBVAR>
              <OMV name="i"/>
            </OMBVAR>
            <OMV name="i"/>
        </OMBIND>
      </OMA>
    </OMA>
  </OMOBJ>

eq (factorial ( n) , product (integer_interval ( 1 , n) , lambda [ i ] . ( i) ) )

Signatures:
sts


[Next: quotient] [Previous: factorof] [Top]

quotient

The symbol to represent the integer (binary) division operator. That is, for integers a and b, quotient(a,b) denotes q such that a=b*q+r, with |r| less than |b| and a*r positive.

Commented Mathematical property (CMP):
for all a,b with a,b Integers | a = b * quotient(a,b) + remainder(a,b) and abs(remainder(a,b)) is less than abs(b) and a*remainder(a,b) >= 0
Formal Mathematical property (FMP):
<OMOBJ>
     <OMBIND>
       <OMS cd="quant1" name="forall"/>
       <OMBVAR>
         <OMV name="a"/>
         <OMV name="b"/>
       </OMBVAR>
       <OMA>
         <OMS cd="logic1" name="implies"/>
         <OMA>
           <OMS cd="logic1" name="and"/>
           <OMA>
             <OMS cd="set1" name="in"/>
             <OMV name="a"/>
             <OMS cd="setname1" name="Z"/>
           </OMA>
           <OMA>
             <OMS cd="set1" name="in"/>
             <OMV name="b"/>
             <OMS cd="setname1" name="Z"/>
           </OMA>
         </OMA>
         <OMA>
	   <OMS cd="logic1" name="and"/>
	   <OMA>
             <OMS cd="relation1" name="eq"/>
             <OMV name="a"/>
             <OMA>
               <OMS cd="arith1" name="plus"/>
               <OMA>
                 <OMS cd="arith1" name="times"/>
                 <OMV name="b"/>
                 <OMA>
                   <OMS cd="integer1" name="quotient"/>
                   <OMV name="a"/>
                   <OMV name="b"/>
                 </OMA>
               </OMA>
               <OMA>
                 <OMS cd="integer1" name="remainder"/>
                 <OMV name="a"/>
                 <OMV name="b"/>
               </OMA>
             </OMA>
           </OMA>
           <OMA>
             <OMS cd="relation1" name="lt"/>
             <OMA>
               <OMS cd="arith1" name="abs"/>
               <OMA>
                 <OMS cd="integer1" name="remainder"/>
                 <OMV name="a"/>
                 <OMV name="b"/>
               </OMA>
             </OMA>
             <OMA>
               <OMS cd="arith1" name="abs"/>
               <OMV name="b"/>
             </OMA>
           </OMA>
           <OMA>
             <OMS cd="relation1" name="geq"/>
             <OMA>
               <OMS cd="arith1" name="times"/>
               <OMV name="a"/>
	       <OMA>
	         <OMS cd="integer1" name="remainder"/>
		 <OMV name="a"/>
		 <OMV name="b"/>
	       </OMA>
             </OMA>
             <OMS cd="alg1" name="zero"/>
           </OMA>
         </OMA>
       </OMA>
     </OMBIND>
   </OMOBJ>

forall [ a b ] . (implies (and (in ( a, Z) , in ( b, Z) ) , and (eq ( a, plus (times ( b, quotient ( a, b) ) , remainder ( a, b) ) ) , lt (abs (remainder ( a, b) ) , abs ( b) ) , geq (times ( a, remainder ( a, b) ) , zero) ) ) )

Signatures:
sts


[Next: remainder] [Previous: factorial] [Top]

remainder

The symbol to represent the integer remainder after (binary) division. For integers a and b, remainder(a,b) denotes r such that a=b*q+r, with |r| less than |b| and a*r positive.

Commented Mathematical property (CMP):
for all a,b with a,b Integers | a = b * quotient(a,b) + remainder(a,b) and abs(remainder(a,b)) is less than abs(b) and a*remainder(a,b) >= 0
Formal Mathematical property (FMP):
<OMOBJ>
     <OMBIND>
       <OMS cd="quant1" name="forall"/>
       <OMBVAR>
         <OMV name="a"/>
         <OMV name="b"/>
       </OMBVAR>
       <OMA>
         <OMS cd="logic1" name="implies"/>
         <OMA>
           <OMS cd="logic1" name="and"/>
           <OMA>
             <OMS cd="set1" name="in"/>
             <OMV name="a"/>
             <OMS cd="setname1" name="Z"/>
           </OMA>
           <OMA>
             <OMS cd="set1" name="in"/>
             <OMV name="b"/>
             <OMS cd="setname1" name="Z"/>
           </OMA>
         </OMA>
         <OMA>
	   <OMS cd="logic1" name="and"/>
	   <OMA>
             <OMS cd="relation1" name="eq"/>
             <OMV name="a"/>
             <OMA>
               <OMS cd="arith1" name="plus"/>
               <OMA>
                 <OMS cd="arith1" name="times"/>
                 <OMV name="b"/>
                 <OMA>
                   <OMS cd="integer1" name="quotient"/>
                   <OMV name="a"/>
                   <OMV name="b"/>
                 </OMA>
               </OMA>
               <OMA>
                 <OMS cd="integer1" name="remainder"/>
                 <OMV name="a"/>
                 <OMV name="b"/>
               </OMA>
             </OMA>
           </OMA>
           <OMA>
             <OMS cd="relation1" name="lt"/>
             <OMA>
               <OMS cd="arith1" name="abs"/>
               <OMA>
                 <OMS cd="integer1" name="remainder"/>
                 <OMV name="a"/>
                 <OMV name="b"/>
               </OMA>
             </OMA>
             <OMA>
               <OMS cd="arith1" name="abs"/>
               <OMV name="b"/>
             </OMA>
           </OMA>
           <OMA>
             <OMS cd="relation1" name="geq"/>
             <OMA>
               <OMS cd="arith1" name="times"/>
               <OMV name="a"/>
	       <OMA>
	         <OMS cd="integer1" name="remainder"/>
		 <OMV name="a"/>
		 <OMV name="b"/>
	       </OMA>
             </OMA>
             <OMS cd="alg1" name="zero"/>
           </OMA>
         </OMA>
       </OMA>
     </OMBIND>
   </OMOBJ>

forall [ a b ] . (implies (and (in ( a, Z) , in ( b, Z) ) , and (eq ( a, plus (times ( b, quotient ( a, b) ) , remainder ( a, b) ) ) , lt (abs (remainder ( a, b) ) , abs ( b) ) , geq (times ( a, remainder ( a, b) ) , zero) ) ) )

Signatures:
sts


[First: factorof] [Previous: quotient] [Top]