diff options
Diffstat (limited to 'Master/texmf-dist/source/latex/stex/schema/rnc/omdoc/arith1.omdoc')
-rw-r--r-- | Master/texmf-dist/source/latex/stex/schema/rnc/omdoc/arith1.omdoc | 1672 |
1 files changed, 1672 insertions, 0 deletions
diff --git a/Master/texmf-dist/source/latex/stex/schema/rnc/omdoc/arith1.omdoc b/Master/texmf-dist/source/latex/stex/schema/rnc/omdoc/arith1.omdoc new file mode 100644 index 00000000000..d7aa94849ff --- /dev/null +++ b/Master/texmf-dist/source/latex/stex/schema/rnc/omdoc/arith1.omdoc @@ -0,0 +1,1672 @@ +<?xml version="1.0" encoding="utf-8"?> + +<omdoc xml:id="arith1-omdoc" version="1.3" + modules="CD" + xmlns:dc="http://purl.org/dc/elements/1.1/" + xmlns:cc="http://creativecommons.org/ns" + xmlns:om="http://www.openmath.org/OpenMath" + xmlns:m="http://www.w3.org/1998/Math/MathML" + xmlns:o="http://omdoc.org/ns" + xmlns:xh="http://www.w3.org/1999/xhtml" + xmlns="http://omdoc.org/ns"> + +<metadata> + <dc:title>The OpenMath Content Dictionary arith1.ocd in OMDoc form</dc:title> + <dc:creator role="trl">Michael Kohlhase</dc:creator> + <dc:creator role="ant">The OpenMath Society</dc:creator> + <dc:date action="updated">2004-07-13</dc:date> + <dc:source>Derived from the OpenMath CD http://www.openmath.org/cd/arith1.ocd.</dc:source> + <dc:type>Text</dc:type> + <dc:format>application/omdoc+xml</dc:format> + <dc:rights> + <xh:p>Copyright (c) 2000-2002 Michael Kohlhase; + This OMDoc content dictionary is released under the OpenMath license: + http://monet.nag.co.uk/openmath/cdfiles/license.html + </xh:p> + </dc:rights> + <dc:description><xh:p>This CD defines symbols for common arithmetic functions.</xh:p></dc:description> +</metadata> + +<theory xml:id="arith1"> + <imports from="integer1.omdoc#integer1"/> + <imports from="interval1.omdoc#interval1"/> + <imports from="fns1.omdoc#fns1"/> + <imports from="relation1.omdoc#relation1"/> + +<symbol name="lcm" xml:id="lcm"> + <metadata> + <dc:description> + <xh:p>The symbol to represent the n-ary function to return the + <term cd="arith1" name="lcm" role="definiens">least common multiple</term> of its arguments. + </xh:p> + </dc:description> + <dc:description xml:lang="de"> + <xh:p> + Das Symbol f"ur das <term cd="arith1" name="lcm" role="definiens">kleinste + gemeinsame Vielfache</term> (als n-aere Funktion). + </xh:p> + </dc:description> + <dc:subject>lcm</dc:subject> + <dc:subject xml:lang="de">kgV</dc:subject> + </metadata> + <type system="sts.omdoc#sts"> + <OMOBJ xmlns="http://www.openmath.org/OpenMath"> + <OMA> + <OMS name="mapsto" cd="sts"/> + <OMA> + <OMS name="nassoc" cd="sts"/> + <OMV name="SemiGroup"/> + </OMA> + <OMV name="SemiGroup"/> + </OMA> + </OMOBJ> + </type> +</symbol> + + <notation> + <prototype> + <om:OMS cd="arith1" name="lcm"/> + </prototype> + <prototype> + <m:csymbol cd="arith1">lcm</m:csymbol> + </prototype> + <rendering xml:lang="en"> + <m:mo>lcm</m:mo> + </rendering> + <rendering xml:lang="de"> + <m:mo>kgV</m:mo> + </rendering> + </notation> + +<theory xml:id="arith1-lcm"> +<imports from="alg1.omdoc#alg1"/> +<imports from="logic1.omdoc#logic1"/> +<imports from="quant1.omdoc#quant1"/> +<imports from="set1.omdoc#set1"/> +<imports from="transc1.omdoc#transc1"/> + +<assertion xml:id="lcm-prop-1" type="lemma"> + <CMP> + <xh:p> + <OMOBJ xmlns="http://www.openmath.org/OpenMath"> + <OMR href="lcm-prop-1.O"/></OMOBJ> + for all integers <OMOBJ xmlns="http://www.openmath.org/OpenMath"><OMV name="a"/></OMOBJ> and + <OMOBJ xmlns="http://www.openmath.org/OpenMath"><OMV name="b"/></OMOBJ>. + </xh:p> + </CMP> + <CMP xml:lang="de"> + <xh:p> + <OMOBJ xmlns="http://www.openmath.org/OpenMath"><OMR + href="lcm-prop-1.O"/></OMOBJ> fuer alle ganzen Zahlen <OMOBJ + xmlns="http://www.openmath.org/OpenMath"><OMV name="a"/></OMOBJ> und <OMOBJ + xmlns="http://www.openmath.org/OpenMath"><OMV name="a"/></OMOBJ>. + </xh:p> + </CMP> + <FMP> + <OMOBJ xmlns="http://www.openmath.org/OpenMath"> + <OMA id="lcm-prop-1.O"> + <OMS cd="relation1" name="eq"/> + <OMA><OMS cd="arith1" name="lcm"/><OMV name="a"/><OMV name="b"/></OMA> + <OMA> + <OMS cd="arith1" name="divide"/> + <OMA><OMS cd="arith1" name="times"/><OMV name="a"/><OMV name="b"/></OMA> + <OMA><OMS cd="arith1" name="gcd"/><OMV name="a"/><OMV name="b"/></OMA> + </OMA> + </OMA> + </OMOBJ> + </FMP> +</assertion> + +<assertion xml:id="lcm-prop-3" type="lemma"> + <CMP> + <xh:p> + For all integers a,b there is no <OMOBJ + xmlns="http://www.openmath.org/OpenMath"><OMR href="#lcm-prop-3.1"/></OMOBJ> such + that <OMOBJ xmlns="http://www.openmath.org/OpenMath"><OMR + href="lcm-prop-3.2"/></OMOBJ> and <OMOBJ + xmlns="http://www.openmath.org/OpenMath"><OMR href="#lcm-prop-3.3"/></OMOBJ> and + <OMOBJ xmlns="http://www.openmath.org/OpenMath"><OMR + href="lcm-prop-3.4"/></OMOBJ>. + </xh:p> + </CMP> + <CMP xml:lang="de"> + <xh:p> + Fuer alle ganzen Zahlen a,b gibt es kein <OMOBJ + xmlns="http://www.openmath.org/OpenMath"><OMR href="#lcm-prop-3.1"/></OMOBJ> mit + <OMOBJ xmlns="http://www.openmath.org/OpenMath"><OMR + href="lcm-prop-3.2"/></OMOBJ> und <OMOBJ + xmlns="http://www.openmath.org/OpenMath"><OMR href="#lcm-prop-3.3"/></OMOBJ> und + <OMOBJ xmlns="http://www.openmath.org/OpenMath"><OMR + href="lcm-prop-3.4"/></OMOBJ>. + </xh:p> + </CMP> + <FMP> + <OMOBJ xmlns="http://www.openmath.org/OpenMath"> + <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="not"/> + <OMBIND> + <OMS cd="quant1" name="exists"/> + <OMBVAR> + <OMV name="c"/> + </OMBVAR> + <OMA> + <OMS cd="logic1" name="and"/> + <OMA id="lcm-prop-3.1"> + <OMS cd="relation1" name="gt"/> + <OMV name="c"/> + <OMI>0</OMI> + </OMA> + <OMA id="lcm-prop-3.2"> + <OMS cd="integer1" name="factorof"/> + <OMV name="a"/> + <OMV name="c"/> + </OMA> + <OMA id="lcm-prop-3.3"> + <OMS cd="integer1" name="factorof"/> + <OMV name="b"/> + <OMV name="c"/> + </OMA> + <OMA id="lcm-prop-3.4"> + <OMS cd="relation1" name="lt"/> + <OMV name="c"/> + <OMA> + <OMS cd="arith1" name="lcm"/> + <OMV name="a"/> + <OMV name="b"/> + </OMA> + </OMA> + </OMA> + </OMBIND> + </OMA> + </OMA> + </OMBIND> + </OMOBJ> + </FMP> +</assertion> +</theory> + +<symbol name="gcd" xml:id="gcd"> + <metadata> + <dc:description> + <xh:p> + The symbol to represent the n-ary function to return the gcd (greatest + common divisor) of its arguments. + </xh:p> + </dc:description> +</metadata> +<type system="sts.omdoc#sts"> + <OMOBJ xmlns="http://www.openmath.org/OpenMath"> + <OMA> + <OMS name="mapsto" cd="sts"/> + <OMA> + <OMS name="nassoc" cd="sts"/> + <OMV name="SemiGroup"/> + </OMA> + <OMV name="SemiGroup"/> + </OMA> + </OMOBJ> + </type> +</symbol> + + <notation> + <prototype> + <om:OMS cd="arith1" name="gcd"/> + </prototype> + <prototype> + <m:csymbol cd="arith1">gcd</m:csymbol> + </prototype> + <rendering xml:lang="en"> + <m:mo>gcd</m:mo> + </rendering> + <rendering xml:lang="de"> + <m:mo>ggT</m:mo> + </rendering> + </notation> + +<theory xml:id="arith1-gcd"> +<imports from="alg1.omdoc#alg1"/> +<imports from="logic1.omdoc#logic1"/> +<imports from="quant1.omdoc#quant1"/> +<imports from="set1.omdoc#set1"/> +<imports from="transc1.omdoc#transc1"/> + +<assertion xml:id="gcd-prop-1" type="lemma"> + <CMP> + <xh:p> + For all integers a,b there is no c + such that <OMOBJ xmlns="http://www.openmath.org/OpenMath"><OMR href="#gcd-prop-1.1"/></OMOBJ> and + <OMOBJ xmlns="http://www.openmath.org/OpenMath"><OMR href="#gcd-prop-1.2"/></OMOBJ> but + <OMOBJ xmlns="http://www.openmath.org/OpenMath"><OMR href="#gcd-prop-1.3"/></OMOBJ>. + + Note that this implies that + <OMOBJ xmlns="http://www.openmath.org/OpenMath"> + <OMA> + <OMS cd="relation1" name="gt"/> + <OMA><OMS cd="arith1" name="gcd"/><OMV name="a"/><OMV name="b"/></OMA> + <OMI>0</OMI> + </OMA> + </OMOBJ>. + </xh:p> +</CMP> +<FMP> + <OMOBJ xmlns="http://www.openmath.org/OpenMath"> + <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="not"/> + <OMBIND> + <OMS cd="quant1" name="exists"/> + <OMBVAR> + <OMV name="c"/> + </OMBVAR> + <OMA> + <OMS cd="logic1" name="and"/> + <OMA id="gcd-prop-1.1"> + <OMS cd="set1" name="in"/> + <OMA> + <OMS cd="arith1" name="divide"/> + <OMV name="a"/> + <OMV name="c"/> + </OMA> + <OMS cd="setname1" name="Z"/> + </OMA> + <OMA id="gcd-prop-1.2"> + <OMS cd="set1" name="in"/> + <OMA> + <OMS cd="arith1" name="divide"/> + <OMV name="b"/> + <OMV name="c"/> + </OMA> + <OMS cd="setname1" name="Z"/> + </OMA> + <OMA id="gcd-prop-1.3"> + <OMS cd="relation1" name="gt"/> + <OMV name="c"/> + <OMA> + <OMS cd="arith1" name="gcd"/> + <OMV name="a"/> + <OMV name="b"/> + </OMA> + </OMA> + </OMA> + </OMBIND> + </OMA> + </OMA> + </OMBIND> + </OMOBJ> +</FMP> +</assertion> + +<example xml:id="gcd-ex-3" type="for" for="#gcd"> + <CMP> + <xh:p> + <OMOBJ xmlns="http://www.openmath.org/OpenMath"><OMR href="#gcd-ex-3.1"/></OMOBJ> + </xh:p> + </CMP> + <OMOBJ xmlns="http://www.openmath.org/OpenMath"> + <OMA id="gcd-ex-3.1"> + <OMS cd="relation1" name="eq"/> + <OMA> + <OMS cd="arith1" name="gcd"/> + <OMI> 6 </OMI> + <OMI> 9 </OMI> + </OMA> + <OMI> 3 </OMI> + </OMA> + </OMOBJ> +</example> +</theory> + +<symbol name="plus" xml:id="plus"> + <metadata> + <dc:description><xh:p>The symbol representing an n-ary commutative function plus.</xh:p></dc:description> + <dc:subject>plus</dc:subject> + </metadata> + <type system="sts.omdoc#sts"> + <OMOBJ xmlns="http://www.openmath.org/OpenMath"> + <OMA> + <OMS name="mapsto" cd="sts"/> + <OMA> + <OMS name="nassoc" cd="sts"/> + <OMV name="AbelianSemiGroup"/> + </OMA> + <OMV name="AbelianSemiGroup"/> + </OMA> + </OMOBJ> + </type> +</symbol> + + <notation> + <prototype> + <om:OMA> + <om:OMS cd="arith1" name="plus" o:cr="fun"/> + <exprlist name="args"> + <expr name="arg"/> + </exprlist> + </om:OMA> + </prototype> + <prototype> + <m:apply> + <m:csymbol cd="arith1" o:cr="fun">plus</m:csymbol> + <exprlist name="args"> + <expr name="arg"/> + </exprlist> + </m:apply> + </prototype> + <rendering> + <m:mrow> + <m:mo o:egroup="fence" fence="true">(</m:mo> + <iterate name="args" precedence="500"> + <separator><m:mo o:cr="fun">+</m:mo></separator> + <render name="arg"/> + </iterate> + <m:mo o:egroup="fence" fence="true">)</m:mo> + </m:mrow> + </rendering> + </notation> + <notation> + <prototype> + <om:OMS cd="arith1" name="plus"/> + </prototype> + <prototype> + <m:csymbol cd="arith1">plus</m:csymbol> + </prototype> + <rendering> + <m:mo>+</m:mo> + </rendering> + </notation> + +<theory xml:id="arith1-plus"> +<imports from="alg1.omdoc#alg1"/> +<imports from="logic1.omdoc#logic1"/> +<imports from="quant1.omdoc#quant1"/> +<imports from="set1.omdoc#set1"/> +<imports from="transc1.omdoc#transc1"/> + +<assertion xml:id="plus-prop-1" type="lemma"> + <CMP><xh:p>For all <OMOBJ xmlns="http://www.openmath.org/OpenMath"><OMV name="a"/></OMOBJ> and <OMOBJ xmlns="http://www.openmath.org/OpenMath"><OMV name="b"/></OMOBJ>, + <OMOBJ xmlns="http://www.openmath.org/OpenMath"><OMR href="#plus-prop-1.1"/></OMOBJ> + </xh:p></CMP> + <FMP> + <OMOBJ xmlns="http://www.openmath.org/OpenMath"> + <OMBIND> + <OMS cd="quant1" name="forall"/> + <OMBVAR> + <OMV name="a"/> + <OMV name="b"/> + </OMBVAR> + <OMA id="plus-prop-1.1"> + <OMS cd="relation1" name="eq"/> + <OMA> + <OMS cd="arith1" name="plus"/> + <OMV name="a"/> + <OMV name="b"/> + </OMA> + <OMA> + <OMS cd="arith1" name="plus"/> + <OMV name="b"/> + <OMV name="a"/> + </OMA> + </OMA> + </OMBIND> + </OMOBJ> + </FMP> +</assertion> +</theory> + +<symbol name="unary_minus" xml:id="unary_minus"> + <metadata> + <dc:description><xh:p> This symbol denotes unary minus, i.e. the additive inverse.</xh:p></dc:description><dc:subject>unary minus</dc:subject></metadata> + <type system="sts.omdoc#sts"> + <OMOBJ xmlns="http://www.openmath.org/OpenMath"> + <OMA> + <OMS name="mapsto" cd="sts"/> + <OMV name="AbelianGroup"/> + <OMV name="AbelianGroup"/> + </OMA> + </OMOBJ> + </type> +</symbol> + + <notation> + <prototype> + <om:OMA> + <om:OMS cd="arith1" name="unary_minus" o:cr="fun"/> + <expr name="arg"/> + </om:OMA> + </prototype> + <prototype> + <m:apply> + <m:csymbol cd="arith1" o:cr="fun">unary_minus</m:csymbol> + <expr name="arg"/> + </m:apply> + </prototype> + <rendering> + <m:mrow> + <m:mo o:cr="fun">-</m:mo> + <m:mo o:egroup="fence" fence="true">(</m:mo> + <render name="arg"/> + <m:mo o:egroup="fence" fence="true">)</m:mo> + </m:mrow> + </rendering> + </notation> + <notation> + <prototype> + <om:OMS cd="arith1" name="unary_minus"/> + </prototype> + <prototype> + <m:csymbol cd="arith1">unary_minus</m:csymbol> + </prototype> + <rendering> + <m:mo>-</m:mo> + </rendering> + </notation> + +<theory xml:id="arith1-uminus"> +<imports from="alg1.omdoc#alg1"/> +<imports from="logic1.omdoc#logic1"/> +<imports from="quant1.omdoc#quant1"/> +<imports from="set1.omdoc#set1"/> +<imports from="transc1.omdoc#transc1"/> + +<assertion xml:id="unary_minus-prop-1" type="lemma"> + <CMP><xh:p><OMOBJ xmlns="http://www.openmath.org/OpenMath"><OMR href="#unary_minus-prop-1.1"/></OMOBJ> for all + <OMOBJ xmlns="http://www.openmath.org/OpenMath"><OMV name="a"/></OMOBJ>. + </xh:p></CMP> + <FMP> + <OMOBJ xmlns="http://www.openmath.org/OpenMath"> + <OMBIND> + <OMS cd="quant1" name="forall"/> + <OMBVAR> + <OMV name="a"/> + </OMBVAR> + <OMA id="unary_minus-prop-1.1"> + <OMS cd="relation1" name="eq"/> + <OMA> + <OMS cd="arith1" name="plus"/> + <OMV name="a"/> + <OMA> + <OMS cd="arith1" name="unary_minus"/> + <OMV name="a"/> + </OMA> + </OMA> + <OMS cd="alg1" name="zero"/> + </OMA> + </OMBIND> + </OMOBJ> + </FMP> +</assertion> +</theory> + + +<symbol name="minus" xml:id="minus"> + <metadata> + <dc:description><xh:p> The symbol representing a binary minus function. This is equivalent to + adding the additive inverse. + </xh:p></dc:description> +</metadata> +<type system="sts.omdoc#sts"> + <OMOBJ xmlns="http://www.openmath.org/OpenMath"> + <OMA> + <OMS name="mapsto" cd="sts"/> + <OMV name="AbelianGroup"/> + <OMV name="AbelianGroup"/> + <OMV name="AbelianGroup"/> + </OMA> + </OMOBJ> + </type> +</symbol> + <notation> + <prototype> + <om:OMA> + <om:OMS cd="arith1" name="minus" o:cr="fun"/> + <expr name="arg1"/> + <expr name="arg2"/> + </om:OMA> + </prototype> + <prototype> + <m:apply> + <m:csymbol cd="arith1" o:cr="fun">minus</m:csymbol> + <expr name="arg1"/> + <expr name="arg2"/> + </m:apply> + </prototype> + <rendering> + <m:mrow> + <m:mo o:egroup="fence" fence="true">(</m:mo> + <render name="arg1" precedence="500"/> + <m:mo o:cr="fun">-</m:mo> + <render name="arg2" precedence="500"/> + <m:mo o:egroup="fence" fence="true">)</m:mo> + </m:mrow> + </rendering> + </notation> + <notation> + <prototype> + <om:OMS cd="arith1" name="minus"/> + </prototype> + <prototype> + <m:csymbol cd="arith1">minus</m:csymbol> + </prototype> + <rendering> + <m:mo>-</m:mo> + </rendering> + </notation> + +<theory xml:id="arith1-minus"> +<imports from="alg1.omdoc#alg1"/> +<imports from="logic1.omdoc#logic1"/> +<imports from="quant1.omdoc#quant1"/> +<imports from="set1.omdoc#set1"/> +<imports from="transc1.omdoc#transc1"/> + + +<assertion xml:id="minus-prop-1" type="lemma"> + <CMP><xh:p> + For all <OMOBJ xmlns="http://www.openmath.org/OpenMath"><OMV name="a"/></OMOBJ> and <OMOBJ xmlns="http://www.openmath.org/OpenMath"><OMV name="b"/></OMOBJ>, + <OMOBJ xmlns="http://www.openmath.org/OpenMath"><OMR href="#minus-prop-1.1"/></OMOBJ>. + </xh:p></CMP> + <FMP> + <OMOBJ xmlns="http://www.openmath.org/OpenMath"> + <OMBIND> + <OMS cd="quant1" name="forall"/> + <OMBVAR> + <OMV name="a"/> + <OMV name="b"/> + </OMBVAR> + <OMA id="minus-prop-1.1"> + <OMS cd="relation1" name="eq"/> + <OMA> + <OMS cd="arith1" name="minus"/> + <OMV name="a"/> + <OMV name="b"/> + </OMA> + <OMA> + <OMS cd="arith1" name="plus"/> + <OMV name="a"/> + <OMA> + <OMS cd="arith1" name="unary_minus"/> + <OMV name="b"/> + </OMA> + </OMA> + </OMA> + </OMBIND> + </OMOBJ> + </FMP> +</assertion> +</theory> + +<symbol name="times" xml:id="times"> + <metadata> + <dc:description><xh:p> The symbol representing an n-ary multiplication function.</xh:p></dc:description><dc:subject>times</dc:subject></metadata> + <type system="sts.omdoc#sts"> + <OMOBJ xmlns="http://www.openmath.org/OpenMath"> + <OMA> + <OMS name="mapsto" cd="sts"/> + <OMA> + <OMS name="nassoc" cd="sts"/> + <OMV name="SemiGroup"/> + </OMA> + <OMV name="SemiGroup"/> + </OMA> + </OMOBJ> + </type> +</symbol> + + <notation> + <prototype> + <om:OMS cd="arith1" name="times"/> + </prototype> + <prototype> + <m:csymbol cd="arith1">times</m:csymbol> + </prototype> + <rendering> + <m:mo></m:mo> + </rendering> + </notation> + <notation> + <prototype> + <om:OMA> + <om:OMS cd="arith1" name="times" o:cr="fun"/> + <exprlist name="args"> + <expr name="arg"/> + </exprlist> + </om:OMA> + </prototype> + <prototype> + <m:apply> + <m:csymbol cd="arith1" o:cr="fun">times</m:csymbol> + <exprlist name="args"> + <expr name="arg"/> + </exprlist> + </m:apply> + </prototype> + <rendering> + <m:mrow> + <m:mo o:egroup="fence" fence="true">(</m:mo> + <iterate name="args" precedence="400"> + <separator> + <m:mo o:cr="fun"></m:mo> + </separator> + <render name="arg"/> + </iterate> + <m:mo o:egroup="fence" fence="true">)</m:mo> + </m:mrow> + </rendering> + </notation> + +<theory xml:id="arith1-times"> +<imports from="alg1.omdoc#alg1"/> +<imports from="logic1.omdoc#logic1"/> +<imports from="quant1.omdoc#quant1"/> +<imports from="set1.omdoc#set1"/> +<imports from="transc1.omdoc#transc1"/> +<imports from="linalg2.omdoc#linalg2"/> + +<example xml:id="times-ex-1" type="for" for="#times"> + <OMOBJ xmlns="http://www.openmath.org/OpenMath" style="display:block"> + <OMA> + <OMS cd="relation1" name="eq"/> + <OMA> + <OMS cd="arith1" name="times"/> + <OMA> + <OMS cd="linalg2" name="matrix"/> + <OMA> + <OMS cd="linalg2" name="matrixrow"/> + <OMI> 1 </OMI> + <OMI> 2 </OMI> + </OMA> + <OMA> + <OMS cd="linalg2" name="matrixrow"/> + <OMI> 3 </OMI> + <OMI> 4 </OMI> + </OMA> + </OMA> + <OMA> + <OMS cd="linalg2" name="matrix"/> + <OMA> + <OMS cd="linalg2" name="matrixrow"/> + <OMI> 5 </OMI> + <OMI> 6 </OMI> + </OMA> + <OMA> + <OMS cd="linalg2" name="matrixrow"/> + <OMI> 7 </OMI> + <OMI> 8 </OMI> + </OMA> + </OMA> + </OMA> + <OMA> + <OMS cd="linalg2" name="matrix"/> + <OMA> + <OMS cd="linalg2" name="matrixrow"/> + <OMI> 19 </OMI> + <OMI> 20 </OMI> + </OMA> + <OMA> + <OMS cd="linalg2" name="matrixrow"/> + <OMI> 43 </OMI> + <OMI> 50 </OMI> + </OMA> + </OMA> + </OMA> + </OMOBJ> +</example> + +<assertion xml:id="times-prop-2" type="lemma"> + <CMP><xh:p> for all <OMOBJ xmlns="http://www.openmath.org/OpenMath"><OMV name="a"/></OMOBJ> and <OMOBJ xmlns="http://www.openmath.org/OpenMath"><OMV name="b"/></OMOBJ>, + <OMOBJ xmlns="http://www.openmath.org/OpenMath"><OMR href="#times-prop-2.1"/></OMOBJ> and + <OMOBJ xmlns="http://www.openmath.org/OpenMath"><OMR href="#times-prop-2.2"/></OMOBJ>. + </xh:p></CMP> + <FMP> + <OMOBJ xmlns="http://www.openmath.org/OpenMath"> + <OMBIND> + <OMS cd="quant1" name="forall"/> + <OMBVAR> + <OMV name="a"/> + <OMV name="b"/> + </OMBVAR> + <OMA> + <OMS cd="logic1" name="and"/> + <OMA id="times-prop-2.1"> + <OMS cd="relation1" name="eq"/> + <OMA> + <OMS cd="arith1" name="times"/> + <OMV name="a"/> + <OMS cd="alg1" name="zero"/> + </OMA> + <OMS cd="alg1" name="zero"/> + </OMA> + <OMA id="times-prop-2.2"> + <OMS cd="relation1" name="eq"/> + <OMA> + <OMS cd="arith1" name="times"/> + <OMV name="a"/> + <OMV name="b"/> + </OMA> + <OMA> + <OMS cd="arith1" name="plus"/> + <OMA> + <OMS cd="arith1" name="times"/> + <OMV name="a"/> + <OMA> + <OMS cd="arith1" name="minus"/> + <OMV name="b"/> + <OMS cd="alg1" name="one"/> + </OMA> + </OMA> + <OMV name="a"/> + </OMA> + </OMA> + </OMA> + </OMBIND> + </OMOBJ> + </FMP> +</assertion> +<assertion xml:id="times-prop-4" type="lemma"> + <CMP><xh:p>For all <OMOBJ xmlns="http://www.openmath.org/OpenMath"><OMV name="a"/></OMOBJ>, + <OMOBJ xmlns="http://www.openmath.org/OpenMath"><OMV name="b"/></OMOBJ>, + and <OMOBJ xmlns="http://www.openmath.org/OpenMath"><OMV name="a"/></OMOBJ>, we + have + <OMOBJ xmlns="http://www.openmath.org/OpenMath"><OMR href="#times-prop-4.1"/></OMOBJ>. + </xh:p></CMP> + <FMP> + <OMOBJ xmlns="http://www.openmath.org/OpenMath"> + <OMBIND> + <OMS cd="quant1" name="forall"/> + <OMBVAR> + <OMV name="a"/> + <OMV name="b"/> + <OMV name="c"/> + </OMBVAR> + <OMA id="times-prop-4.1"> + <OMS cd="relation1" name="eq"/> + <OMA> + <OMS cd="arith1" name="times"/> + <OMV name="a"/> + <OMA> + <OMS cd="arith1" name="plus"/> + <OMV name="b"/> + <OMV name="c"/> + </OMA> + </OMA> + <OMA> + <OMS cd="arith1" name="plus"/> + <OMA> + <OMS cd="arith1" name="times"/> + <OMV name="a"/> + <OMV name="b"/> + </OMA> + <OMA> + <OMS cd="arith1" name="times"/> + <OMV name="a"/> + <OMV name="c"/> + </OMA> + </OMA> + </OMA> + </OMBIND> + </OMOBJ> + </FMP> +</assertion> +</theory> + +<symbol name="divide" xml:id="divide"> +<metadata> +<dc:description><xh:p> + This symbol represents a (binary) division function denoting the first argument + right-divided by the second, i.e. divide(a,b)=a*inverse(b). It is the + inverse of the multiplication function defined by the symbol times in this CD. +</xh:p></dc:description> +</metadata> +<type system="sts.omdoc#sts"> + <OMOBJ xmlns="http://www.openmath.org/OpenMath"> + <OMA> + <OMS name="mapsto" cd="sts"/> + <OMV name="AbelianGroup"/> + <OMV name="AbelianGroup"/> + <OMV name="AbelianGroup"/> + </OMA> + </OMOBJ> + </type> +</symbol> + <notation> + <prototype> + <om:OMS cd="arith1" name="divide"/> + </prototype> + <prototype> + <m:csymbol cd="arith1">divide</m:csymbol> + </prototype> + <rendering> + <m:mo>/</m:mo> + </rendering> + </notation> + <notation> + <prototype> + <om:OMA> + <om:OMS cd="arith1" name="divide"/> + <expr name="arg1"/> + <expr name="arg2"/> + </om:OMA> + </prototype> + <prototype> + <m:apply> + <m:csymbol cd="arith1">divide</m:csymbol> + <expr name="arg1"/> + <expr name="arg2"/> + </m:apply> + </prototype> + <rendering> + <m:mfrac> + <render name="arg1"/> + <render name="arg2"/> + </m:mfrac> + </rendering> + </notation> + +<theory xml:id="arith1-divide"> +<imports from="alg1.omdoc#alg1"/> +<imports from="logic1.omdoc#logic1"/> +<imports from="quant1.omdoc#quant1"/> +<imports from="set1.omdoc#set1"/> +<imports from="transc1.omdoc#transc1"/> + +<assertion xml:id="divide-prop-1" type="lemma"> + <CMP><xh:p>If <OMOBJ xmlns="http://www.openmath.org/OpenMath"><OMR href="#divide-prop-1.1"/></OMOBJ> then + <OMOBJ xmlns="http://www.openmath.org/OpenMath"><OMR href="#divide-prop-1.2"/></OMOBJ>. + </xh:p></CMP> + <FMP> + <OMOBJ xmlns="http://www.openmath.org/OpenMath"> + <OMBIND> + <OMS cd="quant1" name="forall"/> + <OMBVAR> + <OMV name="a"/> + </OMBVAR> + <OMA> + <OMS cd="logic1" name="implies"/> + <OMA id="divide-prop-1.1"> + <OMS cd="relation1" name="neq"/> + <OMV name="a"/> + <OMS cd="alg1" name="zero"/> + </OMA> + <OMA id="divide-prop-1.2"> + <OMS cd="relation1" name="eq"/> + <OMA> + <OMS cd="arith1" name="divide"/> + <OMV name="a"/> + <OMV name="a"/> + </OMA> + <OMS cd="alg1" name="one"/> + </OMA> + </OMA> + </OMBIND> + </OMOBJ> + </FMP> +</assertion> +</theory> + +<symbol name="power" xml:id="power"> +<metadata> +<dc:description><xh:p> + This symbol represents a power function. The first argument is raised + to the power of the second argument. When the second argument is not + an integer, powering is defined in terms of exponentials and + logarithms for the complex and real numbers. + This operator can represent general powering. +</xh:p></dc:description> +</metadata> +<type system="sts.omdoc#sts"> + <OMOBJ xmlns="http://www.openmath.org/OpenMath"> + <OMA> + <OMS name="mapsto" cd="sts"/> + <OMS name="NumericalValue" cd="sts"/> + <OMS name="NumericalValue" cd="sts"/> + <OMS name="NumericalValue" cd="sts"/> + </OMA> + </OMOBJ> + </type> +</symbol> + + <notation> + <prototype> + <om:OMS cd="arith1" name="power"/> + </prototype> + <prototype> + <m:csymbol cd="arith1">power</m:csymbol> + </prototype> + <rendering> + <m:mo>power</m:mo> + </rendering> + </notation> + <notation> + <prototype> + <om:OMA> + <om:OMS cd="arith1" name="power"/> + <expr name="arg1"/> + <expr name="arg2"/> + </om:OMA> + </prototype> + <prototype> + <m:apply> + <m:csymbol cd="arith1">power</m:csymbol> + <expr name="arg1"/> + <expr name="arg2"/> + </m:apply> + </prototype> + <rendering> + <m:msup> + <render name="arg1"/> + <render name="arg2"/> + </m:msup> + </rendering> + </notation> + +<theory xml:id="arith1-power"> +<imports from="alg1.omdoc#alg1"/> +<imports from="logic1.omdoc#logic1"/> +<imports from="quant1.omdoc#quant1"/> +<imports from="set1.omdoc#set1"/> +<imports from="transc1.omdoc#transc1"/> +<imports from="linalg2.omdoc#linalg2"/> +<imports from="nums1.omdoc#nums1"/> + +<assertion xml:id="power-prop-1" type="lemma"> + <CMP><xh:p><OMOBJ xmlns="http://www.openmath.org/OpenMath"><OMR href="#power-prop-1.1"/></OMOBJ> implies + <OMOBJ xmlns="http://www.openmath.org/OpenMath"><OMR href="#power-prop-1.2"/></OMOBJ>. + </xh:p></CMP> + <FMP> + <OMOBJ xmlns="http://www.openmath.org/OpenMath"> + <OMA> + <OMS cd="logic1" name="implies"/> + <OMA id="power-prop-1.1"> + <OMS cd="set1" name="in"/> + <OMV name="x"/> + <OMS cd="setname1" name="C"/> + </OMA> + <OMA id="power-prop-1.2"> + <OMS cd="relation1" name="eq"/> + <OMA> + <OMS name="power" cd="arith1"/> + <OMV name="x"/> + <OMV name="a"/> + </OMA> + <OMA> + <OMS name="exp" cd="transc1"/> + <OMA> + <OMS name="times" cd="arith1"/> + <OMV name="a"/> + <OMA> + <OMS name="ln" cd="transc1"/> + <OMV name="x"/> + </OMA> + </OMA> + </OMA> + </OMA> + </OMA> + </OMOBJ> + </FMP> +</assertion> +<assertion xml:id="power-prop-3" type="lemma"> + <CMP><xh:p>If <OMOBJ xmlns="http://www.openmath.org/OpenMath"><OMV name="n"/></OMOBJ> is an integer then + <OMOBJ xmlns="http://www.openmath.org/OpenMath"><OMR href="#power-prop-3.1"/></OMOBJ> and + <OMOBJ xmlns="http://www.openmath.org/OpenMath"><OMR href="#power-prop-3.2"/></OMOBJ>. + </xh:p></CMP> + <FMP> + <OMOBJ xmlns="http://www.openmath.org/OpenMath"> + <OMA> + <OMS cd="logic1" name="implies"/> + <OMA> + <OMS cd="set1" name="in"/> + <OMV name="n"/> + <OMS cd="setname1" name="Z"/> + </OMA> + <OMA> + <OMS cd="logic1" name="and"/> + <OMA id="power-prop-3.1"> + <OMS cd="relation1" name="eq"/> + <OMA> + <OMS cd="arith1" name="power"/> + <OMV name="x"/> + <OMI>0</OMI> + </OMA> + <OMS cd="alg1" name="one"/> + </OMA> + <OMA id="power-prop-3.2"> + <OMS cd="relation1" name="eq"/> + <OMA> + <OMS cd="arith1" name="power"/> + <OMV name="x"/> + <OMV name="n"/> + </OMA> + <OMA> + <OMS cd="arith1" name="times"/> + <OMV name="x"/> + <OMA> + <OMS cd="arith1" name="power"/> + <OMV name="x"/> + <OMA> + <OMS cd="arith1" name="minus"/> + <OMV name="n"/> + <OMI>1</OMI> + </OMA> + </OMA> + </OMA> + </OMA> + </OMA> + </OMA> + </OMOBJ> + </FMP> +</assertion> + + <example xml:id="power-ex-5" type="for" for="#power"> + <OMOBJ xmlns="http://www.openmath.org/OpenMath" style="display:block"> + <OMA> + <OMS cd="relation1" name="eq"/> + <OMA> + <OMS cd="arith1" name="power"/> + <OMA> + <OMS cd="linalg2" name="matrix"/> + <OMA> + <OMS cd="linalg2" name="matrixrow"/> + <OMI> 1 </OMI> + <OMI> 2 </OMI> + </OMA> + <OMA> + <OMS cd="linalg2" name="matrixrow"/> + <OMI> 3 </OMI> + <OMI> 4 </OMI> + </OMA> + </OMA> + <OMI>3</OMI> + </OMA> + <OMA> + <OMS cd="linalg2" name="matrix"/> + <OMA> + <OMS cd="linalg2" name="matrixrow"/> + <OMI> 37 </OMI> + <OMI> 54 </OMI> + </OMA> + <OMA> + <OMS cd="linalg2" name="matrixrow"/> + <OMI> 81 </OMI> + <OMI> 118 </OMI> + </OMA> + </OMA> + </OMA> + </OMOBJ> +</example> + +<example xml:id="power-ex-6" type="for" for="#power"> + <OMOBJ xmlns="http://www.openmath.org/OpenMath"> + <OMA> + <OMS cd="relation1" name="eq"/> + <OMA> + <OMS cd="arith1" name="power"/> + <OMS cd="nums1" name="e"/> + <OMA> + <OMS cd="arith1" name="times"/> + <OMS cd="nums1" name="i"/> + <OMS cd="nums1" name="pi"/> + </OMA> + </OMA> + <OMA> + <OMS cd="arith1" name="unary_minus"/> + <OMS cd="alg1" name="one"/> + </OMA> + </OMA> + </OMOBJ> +</example> +</theory> + +<symbol name="abs" xml:id="abs"> +<metadata> +<dc:description><xh:p> + A unary operator which represents the absolute value of its + argument. The argument should be numerically valued. + In the complex case this is often referred to as the modulus. +</xh:p></dc:description> +</metadata> +<type system="sts.omdoc#sts"> + <OMOBJ xmlns="http://www.openmath.org/OpenMath"> + <OMA> + <OMS name="mapsto" cd="sts"/> + <OMS name="C" cd="setname1"/> + <OMS name="R" cd="setname1"/> + </OMA> + </OMOBJ> + </type> +</symbol> + + <notation> + <prototype> + <om:OMS cd="arith1" name="abs"/> + </prototype> + <prototype> + <m:csymbol cd="arith1">abs</m:csymbol> + </prototype> + <rendering> + <m:mo>abs</m:mo> + </rendering> + </notation> + <notation> + <prototype> + <om:OMA> + <om:OMS cd="arith1" name="abs" o:cr="fun"/> + <expr name="arg"/> + </om:OMA> + </prototype> + <prototype> + <m:apply> + <m:csymbol cd="arith1">abs</m:csymbol> + <expr name="arg"/> + </m:apply> + </prototype> + <rendering> + <m:mrow><m:mo>|</m:mo><render name="arg"/><m:mo>|</m:mo></m:mrow> + </rendering> + </notation> + +<theory xml:id="arith1-abs"> +<imports from="alg1.omdoc#alg1"/> +<imports from="logic1.omdoc#logic1"/> +<imports from="quant1.omdoc#quant1"/> +<imports from="set1.omdoc#set1"/> +<imports from="transc1.omdoc#transc1"/> + +<assertion xml:id="abs-prop-1" type="lemma"> + <CMP><xh:p>For all <OMOBJ xmlns="http://www.openmath.org/OpenMath"><OMV name="x"/></OMOBJ> and + <OMOBJ xmlns="http://www.openmath.org/OpenMath"><OMV name="y"/></OMOBJ> we + have <OMOBJ xmlns="http://www.openmath.org/OpenMath"><OMR + href="abs-prop-1.1"/></OMOBJ>. + </xh:p></CMP> + <FMP> + <OMOBJ xmlns="http://www.openmath.org/OpenMath"> + <OMBIND> + <OMS cd="quant1" name="forall"/> + <OMBVAR> + <OMV name="x"/> + <OMV name="y"/> + </OMBVAR> + <OMA id="abs-prop-1.1"> + <OMS cd="relation1" name="geq"/> + <OMA> + <OMS cd="arith1" name="plus"/> + <OMA> + <OMS cd="arith1" name="abs"/> + <OMV name="x"/> + </OMA> + <OMA> + <OMS cd="arith1" name="abs"/> + <OMV name="y"/> + </OMA> + </OMA> + <OMA> + <OMS cd="arith1" name="abs"/> + <OMA> + <OMS cd="arith1" name="plus"/> + <OMV name="x"/> + <OMV name="y"/> + </OMA> + </OMA> + </OMA> + </OMBIND> + </OMOBJ> + </FMP> +</assertion> +</theory> + + +<symbol name="root" xml:id="root"> +<metadata> +<dc:description><xh:p> + A binary operator which represents its first argument "lowered" to its + n'th root where n is the second argument. This is the inverse of the operation + represented by the power symbol defined in this CD. + + Care should be taken as to the precise meaning of this operator, in particular + which root is represented, however it is here to represent the general notion of + taking n'th roots. As inferred by the signature relevant to this symbol, the + function represented by this symbol is the single valued function, the specific + root returned is the one indicated by the first CMP. Note also that the converse + of the second CMP is not valid in general. +</xh:p></dc:description> +</metadata> +<type system="sts.omdoc#sts"> + <OMOBJ xmlns="http://www.openmath.org/OpenMath"> + <OMA> + <OMS name="mapsto" cd="sts"/> + <OMS name="NumericalValue" cd="sts"/> + <OMS name="NumericalValue" cd="sts"/> + <OMS name="NumericalValue" cd="sts"/> + </OMA> + </OMOBJ> +</type> +</symbol> + <notation> + <prototype> + <om:OMA> + <om:OMS cd="arith1" name="root"/> + <expr name="arg"/> + <expr name="n"/> + </om:OMA> + </prototype> + <prototype> + <m:apply> + <m:csymbol cd="arith1">root</m:csymbol> + <expr name="arg"/> + <expr name="n"/> + </m:apply> + </prototype> + <rendering> + <m:mroot> + <render name="arg"/> + <render name="n"/> + </m:mroot> + </rendering> + </notation> + <notation> + <prototype> + <om:OMS cd="arith1" name="root"/> + </prototype> + <prototype> + <m:csymbol cd="arith1">root</m:csymbol> + </prototype> + <rendering> + <m:mo>√</m:mo> + </rendering> + </notation> + +<theory xml:id="arith1-root"> +<imports from="alg1.omdoc#alg1"/> +<imports from="logic1.omdoc#logic1"/> +<imports from="quant1.omdoc#quant1"/> +<imports from="set1.omdoc#set1"/> +<imports from="transc1.omdoc#transc1"/> + + +<assertion xml:id="root-prop-1" type="lemma"> + <CMP><xh:p> <OMOBJ xmlns="http://www.openmath.org/OpenMath"><OMR href="#root-prop-1.1"/></OMOBJ> implies + <OMOBJ xmlns="http://www.openmath.org/OpenMath"><OMR href="#root-prop-1.2"/></OMOBJ>. + </xh:p></CMP> + <FMP> + <OMOBJ xmlns="http://www.openmath.org/OpenMath"> + <OMA> + <OMS cd="logic1" name="implies"/> + <OMA id="root-prop-1.1"> + <OMS cd="set1" name="in"/> + <OMV name="x"/> + <OMS cd="setname1" name="C"/> + </OMA> + <OMA id="root-prop-1.2"> + <OMS cd="relation1" name="eq"/> + <OMA> + <OMS cd="arith1" name="root"/> + <OMV name="x"/> + <OMV name="n"/> + </OMA> + <OMA> + <OMS name="exp" cd="transc1"/> + <OMA> + <OMS name="divide" cd="arith1"/> + <OMA> + <OMS name="ln" cd="transc1"/> + <OMV name="x"/> + </OMA> + <OMV name="n"/> + </OMA> + </OMA> + </OMA> + </OMA> + </OMOBJ> + </FMP> +</assertion> +<assertion xml:id="root-prop-3" type="lemma"> + <CMP><xh:p> + For all <OMOBJ xmlns="http://www.openmath.org/OpenMath"><OMV + name="a"/></OMOBJ> and <OMOBJ xmlns="http://www.openmath.org/OpenMath"><OMV + name="n"/></OMOBJ> + <OMOBJ xmlns="http://www.openmath.org/OpenMath"><OMR href="#root-prop-3.1"/></OMOBJ> (if the root exists!). + </xh:p></CMP> + <FMP> + <OMOBJ xmlns="http://www.openmath.org/OpenMath"> + <OMBIND> + <OMS cd="quant1" name="forall"/> + <OMBVAR> + <OMV name="a"/> + <OMV name="n"/> + </OMBVAR> + <OMA id="root-prop-3.1"> + <OMS cd="relation1" name="eq"/> + <OMA> + <OMS cd="arith1" name="power"/> + <OMA> + <OMS cd="arith1" name="root"/> + <OMV name="a"/> + <OMV name="n"/> + </OMA> + <OMV name="n"/> + </OMA> + <OMV name="a"/> + </OMA> + </OMBIND> + </OMOBJ> + </FMP> +</assertion> +</theory> + +<symbol name="sum" xml:id="sum"> +<metadata> +<dc:description><xh:p> + An operator taking two arguments, the first being the range of summation, + e.g. an integral interval, the second being the function to be + summed. Note that the sum may be over an infinite interval. +</xh:p></dc:description> +</metadata> +<type system="sts.omdoc#sts"> + <OMOBJ xmlns="http://www.openmath.org/OpenMath"> + <OMA> + <OMS name="mapsto" cd="sts"/> + <OMV name="IntegerRange"/> + <OMA> + <OMS name="mapsto" cd="sts"/> + <OMS name="Z" cd="setname1"/> + <OMV name="AbelianMonoid"/> + </OMA> + <OMV name="AbelianMonoid"/> + </OMA> + </OMOBJ> + </type> +</symbol> + + <notation> + <prototype> + <om:OMA> + <om:OMS cd="arith1" name="sum" o:cr="fun"/> + <om:OMA> + <om:OMS cd="interval1" name="integer_interval"/> + <expr name="low"/> + <expr name="high"/> + </om:OMA> + <om:OMBIND> + <om:OMS cd="fns1" name="lambda"/> + <om:OMBVAR><expr name="var"/></om:OMBVAR> + <expr name="scope"/> + </om:OMBIND> + </om:OMA> + </prototype> + <prototype> + <m:apply> + <m:csymbol cd="arith1" o:cr="fun">sum</m:csymbol> + <m:apply> + <m:csymbol cd="interval1">integer_interval</m:csymbol> + <expr name="low"/> + <expr name="high"/> + </m:apply> + <m:bind> + <m:csymbol cd="fns1">lambda</m:csymbol> + <m:bvar><expr name="var"/></m:bvar> + <expr name="scope"/> + </m:bind> + </m:apply> + </prototype> + <rendering> + <m:mrow> + <m:munderover> + <m:mo o:cr="fun">∑</m:mo> + <m:mrow> + <render name="var"/> + <m:mo>=</m:mo> + <render name="low"/> + </m:mrow> + <render name="high"/> + </m:munderover> + <render name="scope"/> + </m:mrow> + </rendering> + </notation> + +<!-- not over an interval --> + <notation> + <prototype> + <om:OMA> + <om:OMS cd="arith1" name="sum" o:cr="fun"/> + <expr name="range"/> + <om:OMBIND> + <om:OMS cd="fns1" name="lambda"/> + <om:OMBVAR><expr name="var"/></om:OMBVAR> + <expr name="scope"/> + </om:OMBIND> + </om:OMA> + </prototype> + <prototype> + <m:apply> + <m:csymbol cd="arith1" o:cr="fun">sum</m:csymbol> + <expr name="range"/> + <m:bind> + <m:csymbol cd="fns1">lambda</m:csymbol> + <m:bvar><expr name="var"/></m:bvar> + <expr name="scope"/> + </m:bind> + </m:apply> + </prototype> + <rendering> + <m:mrow> + <m:munder> + <m:mo o:cr="fun">∑</m:mo> + <m:mrow><render name="var"/><m:mo>∈</m:mo><render name="range"/></m:mrow> + </m:munder> + <render name="scope"/> + </m:mrow> + </rendering> + </notation> + + <notation> + <prototype> + <om:OMS cd="arith1" name="sum"/> + </prototype> + <prototype> + <m:csymbol cd="arith1">sum</m:csymbol> + </prototype> + <rendering> + <m:mo>∑</m:mo> + </rendering> + </notation> + + +<theory xml:id="sum-ex.theory"> +<imports xml:id="sum-ex-imports-fns1" from="fns1.omdoc#fns1"/> +<imports xml:id="sum-ex-imports-interval1" from="interval1.omdoc#interval1"/> + +<example xml:id="sum-ex-1" type="for" for="#sum"> + <CMP><xh:p> + This represents the summation of the reciprocals of all the integers between + <OMOBJ xmlns="http://www.openmath.org/OpenMath"><OMI>1</OMI></OMOBJ> and + <OMOBJ xmlns="http://www.openmath.org/OpenMath"><OMI>10</OMI></OMOBJ> + inclusive. + </xh:p></CMP> + <OMOBJ xmlns="http://www.openmath.org/OpenMath"> + <OMA> + <OMS cd="arith1" name="sum"/> + <OMA> + <OMS cd="interval1" name="integer_interval"/> + <OMI> 1 </OMI> + <OMI> 10 </OMI> + </OMA> + <OMBIND> + <OMS cd="fns1" name="lambda"/> + <OMBVAR> + <OMV name="x"/> + </OMBVAR> + <OMA> + <OMS cd="arith1" name="divide"/> + <OMI> 1 </OMI> + <OMV name="x"/> + </OMA> + </OMBIND> + </OMA> + </OMOBJ> +</example> +</theory> + +<symbol name="product" xml:id="product"> +<metadata> +<dc:description><xh:p> + An operator taking two arguments, the first being the range of multiplication + e.g. an integral interval, the second being the function to + be multiplied. Note that the product may be over an infinite interval. +</xh:p></dc:description> +</metadata> +<type system="sts.omdoc#sts"> + <OMOBJ xmlns="http://www.openmath.org/OpenMath"> + <OMA> + <OMS name="mapsto" cd="sts"/> + <OMV name="IntegerRange"/> + <OMA> + <OMS name="mapsto" cd="sts"/> + <OMS name="Z" cd="setname1"/> + <OMV name="AbelianMonoid"/> + </OMA> + <OMV name="AbelianMonoid"/> + </OMA> + </OMOBJ> + </type> +</symbol> + + <notation> + <prototype> + <om:OMA> + <om:OMS cd="arith1" name="product" o:cr="fun"/> + <om:OMA> + <om:OMS cd="interval1" name="integer_interval"/> + <expr name="low"/> + <expr name="high"/> + </om:OMA> + <om:OMBIND> + <om:OMS cd="fns1" name="lambda"/> + <om:OMBVAR><expr name="var"/></om:OMBVAR> + <expr name="scope"/> + </om:OMBIND> + </om:OMA> + </prototype> + <prototype> + <m:apply> + <m:csymbol cd="arith1" o:cr="fun">product</m:csymbol> + <m:apply> + <m:csymbol cd="interval1">integer_interval</m:csymbol> + <expr name="low"/> + <expr name="high"/> + </m:apply> + <m:bind> + <m:csymbol cd="fns1">lambda</m:csymbol> + <m:bvar><expr name="var"/></m:bvar> + <expr name="scope"/> + </m:bind> + </m:apply> + </prototype> + <rendering> + <m:mrow> + <m:munderover> + <m:mo o:cr="fun">∏</m:mo> + <m:mrow> + <render name="var"/> + <m:mo>=</m:mo> + <render name="low"/> + </m:mrow> + <render name="high"/> + </m:munderover> + <render name="scope"/> + </m:mrow> + </rendering> + </notation> + <notation> + <prototype> + <om:OMS cd="arith1" name="product"/> + </prototype> + <prototype> + <m:csymbol cd="arith1">product</m:csymbol> + </prototype> + <rendering> + <m:mo>∏</m:mo> + </rendering> + </notation> + +<theory xml:id="product-ex.theory"> + <imports xml:id="product-ex-imports-interval1" from="interval1.omdoc#interval1"/> + <imports xml:id="product-ex-imports-fns1" from="fns1.omdoc#fns1"/> +<example xml:id="product-ex-1" type="for" for="#product"> + <CMP><xh:p> + This represents the statement that the + <term cd="integer1" name="factorial">factorial</term> of n is equal to the + <term cd="arith1" name="product">product</term> + of all the integers between 1 and n inclusive. + </xh:p></CMP> + <OMOBJ xmlns="http://www.openmath.org/OpenMath"> + <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> +</example> +</theory> +</theory> + + +</omdoc> + |