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, 0 insertions, 1672 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 deleted file mode 100644 index d7aa94849ff..00000000000 --- a/Master/texmf-dist/source/latex/stex/schema/rnc/omdoc/arith1.omdoc +++ /dev/null @@ -1,1672 +0,0 @@ -<?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> - |