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, 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>&#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>
-