summaryrefslogtreecommitdiff
path: root/Master/texmf-dist/source/latex/stex/schema/rnc/omdoc/arith1.omdoc
diff options
context:
space:
mode:
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.omdoc1672
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>&#x2208;</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>
+