3Dgeo1
description: This CD defines symbols for 3-dimensional Euclidean geometry
type: Library
comment: This document is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. The copyright holder grants you permission to redistribute this document freely as a verbatim copy. Furthermore, the copyright holder permits you to develop any derived work from this document provided that the following conditions are met. a) The derived work acknowledges the fact that it is derived from this document, and maintains a prominent reference in the work to the original source. b) The fact that the derived work is not the original OpenMath document is stated prominently in the derived work. Moreover if both this document and the derived work are Content Dictionaries then the derived work must include a different CDName element, chosen so that it cannot be confused with any works adopted by the OpenMath Society. In particular, if there is a Content Dictionary Group whose name is, for example, `math' containing Content Dictionaries named `math1', `math2' etc., then you should not name a derived Content Dictionary `mathN' where N is an integer. However you are free to name it `private_mathN' or some such. This is because the names `mathN' may be used by the OpenMath Society for future extensions. c) The derived work is distributed under terms that allow the compilation of derived works, but keep paragraphs a) and b) intact. The simplest way to do this is to distribute the derived work under the OpenMath license, but this is not a requirement. If you have questions about this license please contact the OpenMath society at http://www.openmath.org.

circle
description: The symbol is used to indicate a circle in 3-dimensional Euclidean geometry by a variable. The circle may (but need not) be subject to constraints. The symbol takes the variable as the first argument and the constraints as further arguments.
example: Application
  arguments: Literal
    value: The circle c with center at A and passing through the point B is given by:
  arguments: Application
    arguments: Variable
      name: c
    operator: circle
  operator: Example
type: Symbol

endpoints
description: The symbol is used to indicate the set of the two endpoints of a segment in 3-dimensional Euclidean geometry by a variable. The symbol takes the variable as the first argument and the segment as second argument.
example: Application
  arguments: Literal
    value: The set E of the two endpoints of a segment s is given by:
  arguments: Application
    arguments: Variable
      name: E
    operator: endpoints
  operator: Example
type: Symbol

line
description: The symbol is used to indicate a line of 3-dimensional Euclidean geometry by a variable. The line may (but need not) be subject to constraints. The symbol takes the variable as the first argument and the constraints as further arguments.
example: Application
  arguments: Literal
    value: Given points A and B in 3-dimensional space, a line l through A and B is defined by:
  arguments: Application
    arguments: Variable
      name: l
    operator: line
  operator: Example
type: Symbol

midpoint
description: The symbol is used to indicate the midpoint of a segment in 3-dimensional Euclidean geometry by a variable. The symbol takes the variable as the first argument and the segment as second argument.
example: Application
  arguments: Literal
    value: The midpoint M of the segment s is given by
  arguments: Application
    arguments: Variable
      name: M
    operator: midpoint
  operator: Example
type: Symbol

plane
description: The symbol is used to indicate a plane in 3-dimensional Euclidean geometry by a variable. The plane may (but need not) be subject to constraints. The symbol takes the variable as the first argument and the constraints as further arguments.
example: Application
  arguments: Literal
    value: Given points A, B and C in 3-dimensional space, a plane p through A, B and C is defined by:
  arguments: Application
    arguments: Variable
      name: p
    operator: plane
  operator: Example
type: Symbol

point
description: The symbol is used to indicate a point of 3-dimensional Euclidean geometry by a variable. The point may (but need not) be subject to constraints. The symbol takes the variable as the first argument and the constraints as further arguments.
example: Application
  arguments: Literal
    value: Given two lines l and m, a point A on l and m is defined by:
  arguments: Application
    arguments: Variable
      name: A
    operator: point
  operator: Example
type: Symbol

segment
description: The symbol is used to indicate a segment of a line in 3-dimensional Euclidean geometry by a variable. The segment is contained in the affine part of the line. The symbol takes the variable as the first argument and the endpoints as second and third arguments.
example: Application
  arguments: Literal
    value: The segment s with endpoints A and B is given by
  arguments: Application
    arguments: Variable
      name: s
    operator: segment
  operator: Example
type: Symbol

sphere
description: The symbol is used to indicate a sphere in 3-dimensional Euclidean geometry by a variable. The sphere may (but need not) be subject to constraints. The symbol takes the variable as the first argument and the constraints as further arguments.
example: Application
  arguments: Literal
    value: The sphere s with center at A and passing through the point B is given by:
  arguments: Application
    arguments: Variable
      name: s
    operator: sphere
  operator: Example
type: Symbol

3Dgeo2
description: This CD defines symbols for 3-dimensional Euclidean geometry
type: Library
comment: This document is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. The copyright holder grants you permission to redistribute this document freely as a verbatim copy. Furthermore, the copyright holder permits you to develop any derived work from this document provided that the following conditions are met. a) The derived work acknowledges the fact that it is derived from this document, and maintains a prominent reference in the work to the original source. b) The fact that the derived work is not the original OpenMath document is stated prominently in the derived work. Moreover if both this document and the derived work are Content Dictionaries then the derived work must include a different CDName element, chosen so that it cannot be confused with any works adopted by the OpenMath Society. In particular, if there is a Content Dictionary Group whose name is, for example, `math' containing Content Dictionaries named `math1', `math2' etc., then you should not name a derived Content Dictionary `mathN' where N is an integer. However you are free to name it `private_mathN' or some such. This is because the names `mathN' may be used by the OpenMath Society for future extensions. c) The derived work is distributed under terms that allow the compilation of derived works, but keep paragraphs a) and b) intact. The simplest way to do this is to distribute the derived work under the OpenMath license, but this is not a requirement. If you have questions about this license please contact the OpenMath society at http://www.openmath.org.

are on line
description: The symbol is a boolean n-ary function. Its arguments should be points. When applied to a sequence of points in 3-dimensional Euclidean space, its evaluated to true if and only if there is a line on which all arguments lie.
example: Application
  arguments: Literal
    value: This example states that the points A, B, C, and D are collinear.
  arguments: Application
    arguments: Variable
      name: A
    operator: are on line
  operator: Example
type: Symbol

are on plane
description: The symbol is a boolean n-ary function. Its arguments should be points. When applied to a sequence of points in 3-dimensional Euclidean space, its evaluated to true if and only if there is a plane on which all arguments lie.
example: Application
  arguments: Literal
    value: This example states that the points A, B, C, and D are coplanar.
  arguments: Application
    arguments: Variable
      name: A
    operator: are on plane
  operator: Example
type: Symbol

circle center
description: The statement that a circle in 3-dimensional Euclidean space has a given point as center. Takes the circle as first argument and the point as second argument.
example: Application
  arguments: Literal
    value: The circle c with center at A and passing through the point B is given by:
  arguments: Application
    arguments: Variable
      name: c
    operator: circle
  operator: Example
type: Symbol

incident
description: The symbol represents the logical incidence function which is a binary function taking arguments representing geometric objects like points and lines and returning a boolean value. It is true if and only if the first argument is incident to the second.
example: Application
  arguments: Literal
    value: That a point A is incident to a line l is given by:
  arguments: Application
    arguments: Variable
      name: A
    operator: incident
  operator: Example
type: Symbol

is midpoint
description: The statement that one point is the midpoint of two others.
example: Application
  arguments: Literal
    value: This example states that C is the midpoint of A and B.
  arguments: Application
    arguments: Variable
      name: C
    operator: is midpoint
  operator: Example
type: Symbol

line parallel
description: The symbol represents a binary boolean function with input two lines or segments. Its value is true whenever the first argument is parallel to the second.
example: Application
  arguments: Literal
    value: This example states that the lines l and m are parallel.
  arguments: Application
    arguments: Variable
      name: l
    operator: line parallel
  operator: Example
type: Symbol

normal
description: The symbol represents a binary boolean function with a line as first argument and a plane as second argument. Its value is true whenever the first argument is normal to the second.
example: Application
  arguments: Literal
    value: This example states that the line l is normal to the plane p.
  arguments: Application
    arguments: Variable
      name: l
    operator: normal
  operator: Example
type: Symbol

perpendicular
description: The symbol represents a binary boolean function with input two lines or segments. Its value is true whenever the first argument is perpendicular to the second.
example: Application
  arguments: Literal
    value: This example states that the lines l and m are perpendicular.
  arguments: Application
    arguments: Variable
      name: l
    operator: perpendicular
  operator: Example
type: Symbol

plane parallel
description: The symbol represents a binary boolean function with input two planes. Its value is true whenever the first argument is parallel to the second.
example: Application
  arguments: Literal
    value: This example states that the planes m and n are parallel.
  arguments: Application
    arguments: Variable
      name: m
    operator: plane parallel
  operator: Example
type: Symbol

sphere center
description: The statement that a sphere in 3-dimensional Euclidean space has a given point as center. Takes the sphere as first argument and the point as second argument.
example: Application
  arguments: Literal
    value: The sphere s with center at A and passing through the point B is given by:
  arguments: Application
    arguments: Variable
      name: s
    operator: sphere
  operator: Example
type: Symbol

FundamentalPhysicalConstants1
description: This CD defines symbols which represent five fundamental physical constants and the Planck units that they define.
type: Library
comment: This document is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. The copyright holder grants you permission to redistribute this document freely as a verbatim copy. Furthermore, the copyright holder permits you to develop any derived work from this document provided that the following conditions are met. a) The derived work acknowledges the fact that it is derived from this document, and maintains a prominent reference in the work to the original source. b) The fact that the derived work is not the original OpenMath document is stated prominently in the derived work. Moreover if both this document and the derived work are Content Dictionaries then the derived work must include a different CDName element, chosen so that it cannot be confused with any works adopted by the OpenMath Society. In particular, if there is a Content Dictionary Group whose name is, for example, `math' containing Content Dictionaries named `math1', `math2' etc., then you should not name a derived Content Dictionary `mathN' where N is an integer. However you are free to name it `private_mathN' or some such. This is because the names `mathN' may be used by the OpenMath Society for future extensions. c) The derived work is distributed under terms that allow the compilation of derived works, but keep paragraphs a) and b) intact. The simplest way to do this is to distribute the derived work under the OpenMath license, but this is not a requirement. If you have questions about this license please contact the OpenMath society at http://www.openmath.org. Author: Joseph B. Collins (2009), Naval Research Laboratory, Washington, DC. Copyright Notice: This is a work of the U.S. Government and is not subject to copyright protection in the United States. Foreign copyrights may apply.

Boltzmann constant
commented property: k ~ 1.3806504*10^(-23) joule kelvin^-1
description: The Boltzmann constant relates energy at the particle level with temperature observed at the bulk level via the ideal gas law, pV = NkT. By measurement it is found to be approximately equal to 1.3806504(24)*10^(-23) joule per kelvin. It is commonly represented with the short, italic symbol, "k".
formal property: Application
  arguments: Boltzmann constant
  arguments: Application
    arguments: Application
      operator: bigfloat
    operator: times
  operator: approx
type: ConstantSymbol

Coulomb constant
commented property: k ~ 1.3806504*10^(-23) joule kelvin^-1
description: The value of the Coulomb constant is implied by international definitions of the speed of light and the vacuum permeability. By definition, its exact value is equal to (299,792,458)^2 * 10^-7 N m^2 C^-2. It is commonly represented with the short, italic symbol, "k" subscripted with the upright letter "e".
formal property: Application
  arguments: Coulomb constant
  arguments: Application
    arguments: Application
      operator: bigfloat
    operator: times
  operator: approx
type: ConstantSymbol

Planck charge
commented property: q_P = sqrt(h-bar*c*4*pi*eps0)
commented property: q_P ~ 1.875545870(47) * 10^−18 coulomb
description: The Planck charge is defined to be sqrt(h-bar*c*4*pi*eps0). Its value derived from measurement is 1.875545870(47) * 10^−18 coulomb. It is commonly represented with the short, italic symbol, "q", subscripted with an upright capital "P".
formal property: Application
  arguments: Planck charge
  arguments: Application
    arguments: Application
      operator: bigfloat
    arguments: coulomb
    operator: times
  operator: eq
type: ConstantSymbol

Planck constant
commented property: Planck constant ~ 6.62606896 * 10^–34 J s
description: This symbol represents the fundamental constant equal to the ratio of the energy of a photon to its frequency. By measurement it is found to be approximately equal to 6.62606896(33)*10^(-34) J s [CODATA 2006]. It is commonly represented with the short, italic symbol, "h".
formal property: Application
  arguments: Planck constant
  arguments: Application
    arguments: Application
      operator: bigfloat
    arguments: joule
    operator: times
  operator: approx
type: ConstantSymbol

Planck length
commented property: l_P = sqrt(h-bar*G/(c^3))
commented property: l_P ~ 1.616252(81) * 10^−35 metre
description: The Planck length is defined to be sqrt(h-bar*G/(c^3)). Its value derived from measurement is 1.616252(81) * 10^−35 metre. It is commonly represented with the short, italic symbol, "l", subscripted with an upright capital "P".
formal property: Application
  arguments: Planck length
  arguments: Application
    arguments: Application
      operator: bigfloat
    arguments: metre
    operator: times
  operator: eq
type: ConstantSymbol

Planck mass
commented property: m_P = sqrt(h-bar*c/G)
commented property: m_P ~ 2.17644(11) * 10^−8 kilogram
description: The Planck mass is defined to be sqrt(h-bar*c/G). Its value derived from measurement is 2.17644(11) * 10^−8 kilogram. It is commonly represented with the short, italic symbol, "m", subscripted with an upright capital "P".
formal property: Application
  arguments: Planck mass
  arguments: Application
    arguments: Application
      operator: bigfloat
    arguments: kilogram
    operator: times
  operator: eq
type: ConstantSymbol

Planck temperature
commented property: l_P = sqrt(h-bar*c^5/(G*k^3))
commented property: l_P ~ 1.416785(71) × 10^32 kelvin
description: The Planck temperature is defined to be sqrt(h-bar*c^5/(G*k^3)). Its value derived from measurement is 1.416785(71) × 10^32 kelvin. It is commonly represented with the short, italic symbol, "T", subscripted with an upright capital "P".
formal property: Application
  arguments: Boltzmann constant
  arguments: Application
    arguments: Application
      operator: bigfloat
    operator: times
  operator: eq
type: ConstantSymbol

Planck time
commented property: t_P = sqrt(h-bar*G/(c^5))
commented property: t_P ~ 5.39124(27) * 10^−44 second
description: The Planck time is defined to be sqrt(h-bar*G/(c^5)). Its value derived from measurement is 5.39124(27) * 10^−44 second. It is commonly represented with the short, italic symbol, "t", subscripted with an upright capital "P".
formal property: Application
  arguments: Planck time
  arguments: Application
    arguments: Application
      operator: bigfloat
    arguments: second
    operator: times
  operator: eq
type: ConstantSymbol

gravitational constant
commented property: G ~ 6.6742(10)*10^-11 newton metre^2 per kilogram^2
description: This symbol represents the constant of proportionality in Newton's law of universal gravitation. By measurement it is found to be approximately equal to 6.6742(10)*10^-11 newton metre^2 per kilogram^2. It is commonly represented with the short, italic symbol, "G".
formal property: Application
  arguments: gravitational constant
  arguments: Application
    arguments: Application
      operator: bigfloat
    arguments: newton
    operator: times
  operator: approx
type: ConstantSymbol

reduced Planck constant
commented property: reduced Planck constant = h/(2*pi)
description: This symbol represents the Planck constant divided by 2*pi. It is commonly represented with the short, italic symbol, h with a horizontal bar ("h-bar"), Unicode: U+210F , HTML: ℏ.
formal property: Application
  arguments: reduced Planck constant
  arguments: Application
    arguments: Planck constant
    operator: divide
  operator: eq
type: ConstantSymbol

speed of light
commented property: The speed of light is 299,792,458 metre per second
description: This symbol represents the speed of light in a vacuum. Its value is implied by the definition of the metre [17th CGPM (1983)]. Consequently, the speed of light is defined to be exactly 299,792,458 metre per second (in the SI). It is commonly represented with the short, italic symbol, "c".
formal property: Application
  arguments: speed of light
  arguments: Application
    arguments: Literal
      value: 299792458
    operator: times
  operator: eq
type: ConstantSymbol

SIUsed OffSystemMeasuredUnits1
description: This CD defines symbols to represent units that are off-system with respect to the SI system of units, but are retained for use with the SI. Each unit is determined by experimental measurement. (DRAFT INTERNATIONAL STANDARD ISO/DIS 80000-1 - "Quantities and units", 2008).
type: Library
comment: This document is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. The copyright holder grants you permission to redistribute this document freely as a verbatim copy. Furthermore, the copyright holder permits you to develop any derived work from this document provided that the following conditions are met. a) The derived work acknowledges the fact that it is derived from this document, and maintains a prominent reference in the work to the original source. b) The fact that the derived work is not the original OpenMath document is stated prominently in the derived work. Moreover if both this document and the derived work are Content Dictionaries then the derived work must include a different CDName element, chosen so that it cannot be confused with any works adopted by the OpenMath Society. In particular, if there is a Content Dictionary Group whose name is, for example, `math' containing Content Dictionaries named `math1', `math2' etc., then you should not name a derived Content Dictionary `mathN' where N is an integer. However you are free to name it `private_mathN' or some such. This is because the names `mathN' may be used by the OpenMath Society for future extensions. c) The derived work is distributed under terms that allow the compilation of derived works, but keep paragraphs a) and b) intact. The simplest way to do this is to distribute the derived work under the OpenMath license, but this is not a requirement. If you have questions about this license please contact the OpenMath society at http://www.openmath.org. Author: Joseph B. Collins (2009), Naval Research Laboratory, Washington, DC. Copyright Notice: This is a work of the U.S. Government and is not subject to copyright protection in the United States. Foreign copyrights may apply.

astronomical unit
commented property: 1 astronomical unit ~ 1.49597870691 * 10^11 metre
description: This symbol represents the measure of one astronomical unit of distance. It has the short symbol form, "ua". It is the mean distance between the sun and the earth. Its measured value is 1 ua = 1.49597870691(6) * 10^11 m [DRAFT INTERNATIONAL STANDARD ISO/DIS 80000-1, International Organization for Standardization, 2008]
formal property: Application
  arguments: Application
    arguments: Literal
      value: 1
    arguments: astronomical unit
    operator: times
  arguments: Application
    arguments: Application
      operator: bigfloat
    arguments: metre
    operator: times
  operator: approx
type: Symbol

dalton
commented property: 1 dalton ~ 1.660538782 * 10^–27 kilogram
description: This symbol represents the measure of one dalton of mass. It has the short symbol form, "Da". The dalton is one-twelth the mass of an atom of Carbon-12 at rest and in its ground state. Its measured value is 1 Da = 1.660538782(83) * 10^–27 kg [CODATA 2006]
formal property: Application
  arguments: Application
    arguments: Literal
      value: 1
    arguments: dalton
    operator: times
  arguments: Application
    arguments: Application
      operator: bigfloat
    arguments: kilogram
    operator: times
  operator: approx
type: Symbol

electronvolt
commented property: 1 electronvolt = 1.602176487 * 10^–19 joule
description: This symbol represents the measure of one electronvolt of energy. It has the short symbol form, "eV". It is the kinetic energy acquired by an electron in passing through a potential difference of 1 volt in a vacuum. Its measured value is 1 eV = 1.602176487(40) * 10^–19 J [CODATA 2006]
formal property: Application
  arguments: Application
    arguments: Literal
      value: 1
    arguments: electronvolt
    operator: times
  arguments: Application
    arguments: Application
      operator: bigfloat
    arguments: joule
    operator: times
  operator: approx
type: Symbol

SIUsed OffSystemUnits1
description: This CD defines symbols to represent units that are off-system with respect to the SI system of units, but are retained for use with the SI. (DRAFT INTERNATIONAL STANDARD ISO/DIS 80000-1 - "Quantities and units", 2008).
type: Library
comment: This document is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. The copyright holder grants you permission to redistribute this document freely as a verbatim copy. Furthermore, the copyright holder permits you to develop any derived work from this document provided that the following conditions are met. a) The derived work acknowledges the fact that it is derived from this document, and maintains a prominent reference in the work to the original source. b) The fact that the derived work is not the original OpenMath document is stated prominently in the derived work. Moreover if both this document and the derived work are Content Dictionaries then the derived work must include a different CDName element, chosen so that it cannot be confused with any works adopted by the OpenMath Society. In particular, if there is a Content Dictionary Group whose name is, for example, `math' containing Content Dictionaries named `math1', `math2' etc., then you should not name a derived Content Dictionary `mathN' where N is an integer. However you are free to name it `private_mathN' or some such. This is because the names `mathN' may be used by the OpenMath Society for future extensions. c) The derived work is distributed under terms that allow the compilation of derived works, but keep paragraphs a) and b) intact. The simplest way to do this is to distribute the derived work under the OpenMath license, but this is not a requirement. If you have questions about this license please contact the OpenMath society at http://www.openmath.org. Author: Joseph B. Collins (2009), Naval Research Laboratory, Washington, DC. Copyright Notice: This is a work of the U.S. Government and is not subject to copyright protection in the United States. Foreign copyrights may apply.

bel
commented property: 1 bel = (ln(10))/2 neper
description: This symbol represents the dimensionless measure of one bel. It has the short symbol form, "B".
formal property: Application
  arguments: Application
    arguments: Literal
      value: 1
    arguments: bel
    operator: times
  arguments: Application
    arguments: Application
      operator: divide
    arguments: neper
    operator: times
  operator: eq
type: Symbol

day
commented property: 1 day = 24 hour
description: This symbol represents the measure of one day of time. It has the short symbol form, "d".
formal property: Application
  arguments: Application
    arguments: Literal
      value: 1
    arguments: day
    operator: times
  arguments: Application
    arguments: Literal
      value: 24
    arguments: hour
    operator: times
  operator: eq
type: Symbol

degree of arc
commented property: 1 degree of arc = pi/180 radian
description: This symbol represents the angular measure of one degree of arc. It has the short symbol form of the degree symbol, a superscript circle, Unicode: U+00B0 or HTML: °.
formal property: Application
  arguments: Application
    arguments: Literal
      value: 1
    arguments: degree of arc
    operator: times
  arguments: Application
    arguments: Application
      operator: divide
    arguments: radian
    operator: times
  operator: eq
type: Symbol

hour
commented property: 1 hour = 60 minute
description: This symbol represents the measure of one hour of time. It has the short symbol form, "h".
formal property: Application
  arguments: Application
    arguments: Literal
      value: 1
    arguments: hour
    operator: times
  arguments: Application
    arguments: Literal
      value: 60
    arguments: minute
    operator: times
  operator: eq
type: Symbol

litre
commented property: 1 litre = 1 decimetre^3
description: This symbol represents the volume measure of one litre. It has the short symbol form, "l" or "L".
formal property: Application
  arguments: Application
    arguments: Literal
      value: 1
    arguments: litre
    operator: times
  arguments: Application
    arguments: Application
      operator: times
    operator: power
  operator: eq
type: Symbol

minute
commented property: 1 minute = 60 seconds
description: This symbol represents the measure of one minute of time. It has the short symbol form, "min".
formal property: Application
  arguments: Application
    arguments: Literal
      value: 1
    arguments: minute
    operator: times
  arguments: Application
    arguments: Literal
      value: 60
    arguments: second
    operator: times
  operator: eq
type: Symbol

minute of arc
commented property: 1 minute of arc = 1/60 degree of arc
description: This symbol represents the angular measure of one minute of arc. It has the short symbol form, "'".
formal property: Application
  arguments: Application
    arguments: Literal
      value: 1
    arguments: minute of arc
    operator: times
  arguments: Application
    arguments: degree of arc
    operator: divide
  operator: eq
type: Symbol

neper
commented property: 1 neper = ln(e) = 1
description: This symbol represents the dimensionless measure of one neper, the natural unit for representing logarithms of ratios of field amplitudes, such as voltage or pressure. It has the short symbol form, "Np".
formal property: Application
  arguments: Application
    arguments: Literal
      value: 1
    arguments: neper
    operator: times
  arguments: Application
    arguments: http://www.openmath.org/cd/nums1#e
    operator: log
  arguments: Literal
    value: 1
  operator: eq
type: Symbol

second of arc
commented property: 1 second of arc = 1/60 minute of arc
description: This symbol represents the angular measure of one second of arc. It has the short symbol form, '"'.
formal property: Application
  arguments: Application
    arguments: Literal
      value: 1
    arguments: second of arc
    operator: times
  arguments: Application
    arguments: minute of arc
    operator: divide
  operator: eq
type: Symbol

tonne
commented property: 1 tonne = 1000 kilogram
description: This symbol represents the mass measure of one tonne. It has the short symbol form, "t".
formal property: Application
  arguments: Application
    arguments: Literal
      value: 1
    arguments: tonne
    operator: times
  arguments: Application
    arguments: Literal
      value: 1000
    arguments: kilogram
    operator: times
  operator: eq
type: Symbol

SI BaseQuantities
description: This CD defines symbols which represent the seven base quantities of the SI (Syst\'{e}me International) system of quantities for describing quantity dimensions. (DRAFT INTERNATIONAL STANDARD ISO/DIS 80000-1 - "Quantities and units", 2008)
type: Library
comment: This document is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. The copyright holder grants you permission to redistribute this document freely as a verbatim copy. Furthermore, the copyright holder permits you to develop any derived work from this document provided that the following conditions are met. a) The derived work acknowledges the fact that it is derived from this document, and maintains a prominent reference in the work to the original source. b) The fact that the derived work is not the original OpenMath document is stated prominently in the derived work. Moreover if both this document and the derived work are Content Dictionaries then the derived work must include a different CDName element, chosen so that it cannot be confused with any works adopted by the OpenMath Society. In particular, if there is a Content Dictionary Group whose name is, for example, `math' containing Content Dictionaries named `math1', `math2' etc., then you should not name a derived Content Dictionary `mathN' where N is an integer. However you are free to name it `private_mathN' or some such. This is because the names `mathN' may be used by the OpenMath Society for future extensions. c) The derived work is distributed under terms that allow the compilation of derived works, but keep paragraphs a) and b) intact. The simplest way to do this is to distribute the derived work under the OpenMath license, but this is not a requirement. If you have questions about this license please contact the OpenMath society at http://www.openmath.org. Author: Joseph B. Collins (2009), Naval Research Laboratory, Washington, DC. Copyright Notice: This is a work of the U.S. Government and is not subject to copyright protection in the United States. Foreign copyrights may apply.

amount-of-substance
description: This symbol represents the SI base quantity of amount of substance. It has the short symbol form, "N".
type: ConstantSymbol

current
description: This symbol represents the SI base quantity of electrical current. It has the short symbol form, "I".
type: ConstantSymbol

length
description: This symbol represents the SI base quantity of length. It has the short symbol form, "L".
type: ConstantSymbol

luminous-intensity
description: This symbol represents the SI base quantity of luminous intensity. It has the short symbol form, "J".
type: ConstantSymbol

mass
description: This symbol represents the SI base quantity of mass. It has the short symbol form, "M".
type: ConstantSymbol

one
description: This symbol represents the proposed SI base quantity of dimension one, or the dimensionless quantity. It has the short symbol form, "1".
type: ConstantSymbol

temperature
description: This symbol represents the SI base quantity of thermodynamic temperature. It has the short symbol form, "\Theta;".
type: ConstantSymbol

time
description: This symbol represents the SI base quantity of time. It has the short symbol form, "T".
type: ConstantSymbol

SI BaseUnits1
description: This CD defines symbols to represent the seven base units of the SI (Syst\'eme International) system of units. (DRAFT INTERNATIONAL STANDARD ISO/DIS 80000-1 - "Quantities and units", 2008). Each unit refers to a corresponding base quantity in SI_BaseQuantities.ocd.
type: Library
comment: This document is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. The copyright holder grants you permission to redistribute this document freely as a verbatim copy. Furthermore, the copyright holder permits you to develop any derived work from this document provided that the following conditions are met. a) The derived work acknowledges the fact that it is derived from this document, and maintains a prominent reference in the work to the original source. b) The fact that the derived work is not the original OpenMath document is stated prominently in the derived work. Moreover if both this document and the derived work are Content Dictionaries then the derived work must include a different CDName element, chosen so that it cannot be confused with any works adopted by the OpenMath Society. In particular, if there is a Content Dictionary Group whose name is, for example, `math' containing Content Dictionaries named `math1', `math2' etc., then you should not name a derived Content Dictionary `mathN' where N is an integer. However you are free to name it `private_mathN' or some such. This is because the names `mathN' may be used by the OpenMath Society for future extensions. c) The derived work is distributed under terms that allow the compilation of derived works, but keep paragraphs a) and b) intact. The simplest way to do this is to distribute the derived work under the OpenMath license, but this is not a requirement. If you have questions about this license please contact the OpenMath society at http://www.openmath.org. Author: Joseph B. Collins (2009), Naval Research Laboratory, Washington, DC. Copyright Notice: This is a work of the U.S. Government and is not subject to copyright protection in the United States. Foreign copyrights may apply.

ampere
commented property: This is a base unit for the SI system. It is defined physically as that constant electric current which, if maintained in two parallel conductors of infinite length, of negligible circular cross-section, and placed 1 metre apart in vacuum, would produce between these conductors a force equal to 2 × 10–7 newton per metre of length [9th CGPM (1948)].
commented property: ampere = unit(current)
description: This symbol represents the measure of one ampere, the standard SI unit of measure for quantities of electric current. It has the short symbol form, "A", in upright roman font.
formal property: Application
  arguments: ampere
  arguments: Application
    arguments: current
    operator: unit
  operator: eq
type: ConstantSymbol

candela
commented property: This is a base unit for the SI system. It is defined physically as the luminous intensity, in a given direction, of a source that emits monochromatic radiation of frequency 540×10^12 hertz and that has a radiant intensity in that direction of 1/683 watt per steradian [16th CGPM (1979)].
commented property: candela = unit(luminous intensity)
description: This symbol represents the measure of one candela, the standard SI unit measure for quantities of luminous intensity. It has the short symbol form, "cd", in upright roman font.
formal property: Application
  arguments: candela
  arguments: Application
    arguments: luminous intensity
    operator: unit
  operator: eq
type: ConstantSymbol

kelvin
commented property: This is a base unit for the SI system. It is defined physically as equal to the fraction 1/273.16 of the thermodynamic temperature of the triple point of water [International Temperature Scale of 1990, ITS-90, adopted by CIPM in 1989]. The isotopic composition of the water is defined by Vienna Standard Mean Ocean Water.
commented property: kelvin = unit(temperature)
description: This symbol represents the measure of one kelvin, the standard SI unit of measure for quantities of thermodynamic temperature. It has the short symbol form, "K", in upright roman font.
formal property: Application
  arguments: kelvin
  arguments: Application
    arguments: temperature
    operator: unit
  operator: eq
type: ConstantSymbol

kilogram
commented property: This is a base unit for the SI system. It is defined physically as the mass of the International Prototype Kilogram stored at the International Bureau of Weights and Measures (BIPM) in in Sèvres, France [3rd CGPM (1901)]. A proposal is pending to redefine the standard mass in terms of natural constants.
commented property: kilogram = unit(mass)
description: This symbol represents the measure of one kilogram of mass, the standard SI unit of measure for quantities of mass. It has the short symbol form, "kg", in upright roman font.
formal property: Application
  arguments: kilogram
  arguments: Application
    arguments: mass
    operator: unit
  operator: eq
type: ConstantSymbol

metre
commented property: This is a base unit for the SI system. It is defined physically as the length of the path travelled by light in vacuum during a time interval of 1/299 792 458 of a second. This definition was provided in 1983 by the seventeenth General Conference on Weights and Measures (CGPM) [17th CGPM (1983)].
commented property: metre = unit(length)
description: This symbol represents the measure of one metre of length, the standard SI unit of measure for quantities of length or physical distance. It has the short symbol form, "m", in upright roman font.
formal property: Application
  arguments: metre
  arguments: Application
    arguments: length
    operator: unit
  operator: eq
type: ConstantSymbol

mole
commented property: This is a base unit for the SI system. It is defined physically as the amount of substance of a system which contains as many "elemental entities" as there are atoms in 12 grams of carbon-12 [14th CGPM (1971)].
commented property: mole = unit(amount of substance)
description: This symbol represents the measure of one mole, the standard SI unit measure for quantities of amount of substance. It has the short symbol form, "mol", in upright roman font.
formal property: Application
  arguments: mole
  arguments: Application
    arguments: amount of substance
    operator: unit
  operator: eq
type: ConstantSymbol

one
commented property: one = unit(one) = 1
description: This symbol represents the dimensionless unit corresponding to the dimensionless quantity dimension. It has the short symbol form, "1".
formal property: Application
  arguments: one
  arguments: Application
    arguments: one
    operator: unit
  operator: eqs
type: ConstantSymbol

second
commented property: This is a base unit for the SI system. It is defined physically as the duration of 9,192,631,770 periods of the radiation corresponding to the transition between the two hyperfine levels of the ground state of the caesium 133 atom [13th CGPM (1967)]. This definition refers to a caesium atom at rest at a temperature of 0 kelvin (absolute zero). The ground state is defined at zero magnetic field [1997 meeting of the BIPM].
commented property: second = unit(time)
description: This symbol represents the measure of one second of time, the standard SI unit of measure for quantities of time. It has the short symbol form, "s", in upright roman font.
formal property: Application
  arguments: second
  arguments: Application
    arguments: time
    operator: unit
  operator: eq
type: ConstantSymbol

SI DerivedQuantities1
type: Library
comment: This document is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. The copyright holder grants you permission to redistribute this document freely as a verbatim copy. Furthermore, the copyright holder permits you to develop any derived work from this document provided that the following conditions are met. a) The derived work acknowledges the fact that it is derived from this document, and maintains a prominent reference in the work to the original source. b) The fact that the derived work is not the original OpenMath document is stated prominently in the derived work. Moreover if both this document and the derived work are Content Dictionaries then the derived work must include a different CDName element, chosen so that it cannot be confused with any works adopted by the OpenMath Society. In particular, if there is a Content Dictionary Group whose name is, for example, `math' containing Content Dictionaries named `math1', `math2' etc., then you should not name a derived Content Dictionary `mathN' where N is an integer. However you are free to name it `private_mathN' or some such. This is because the names `mathN' may be used by the OpenMath Society for future extensions. c) The derived work is distributed under terms that allow the compilation of derived works, but keep paragraphs a) and b) intact. The simplest way to do this is to distribute the derived work under the OpenMath license, but this is not a requirement. If you have questions about this license please contact the OpenMath society at http://www.openmath.org. Author: Joseph B. Collins (2009), Naval Research Laboratory, Washington, DC. Copyright Notice: This is a work of the U.S. Government and is not subject to copyright protection in the United States. Foreign copyrights may apply.

Celsius temperature
commented property: dim(Celsius temperature) = temperature
commented property: num(Celsius temperature) + 273.15 = num(temperature)
description: This symbol represents the physical quantity of Celsius temperature. A variable representing an arbitrary quantity of temperature is commonly represented with the italic, upper case letter, "T".
formal property: Application
  arguments: Application
    arguments: Celsius temperature
    operator: dim
  arguments: temperature
  operator: eq
formal property: Application
  arguments: Application
    arguments: Application
      arguments: Celsius temperature
      operator: num
    arguments: Literal
      value: 273.15
    operator: plus
  operator: eq
type: ConstantSymbol

absorbed dose
commented property: dim(absorbed dose) = dim(energy/mass)
description: This symbol represents the physical quantity of absorbed dose of ionizing radiation. A variable representing an arbitrary quantity of absorbed dose is commonly represented with the italic, upper case letter, "D".
formal property: Application
  arguments: Application
    arguments: absorbed dose
    operator: dim
  arguments: Application
    arguments: Application
      operator: divide
    operator: dim
  operator: eq
type: ConstantSymbol

angle
commented property: dim(angle) = one
description: This symbol represents the quantity of a geometric planar angle. A variable representing an arbitrary quantity of angle is commonly represented with the italic, lower case greek variable, e.g., "\theta;".
formal property: Application
  arguments: Application
    arguments: angle
    operator: dim
  arguments: one
  operator: eq
type: ConstantSymbol

area
commented property: dim(area) = length*length
description: This symbol represents the physical quantity of area.
formal property: Application
  arguments: Application
    arguments: area
    operator: dim
  arguments: Application
    arguments: length
    operator: times
  operator: eq
type: ConstantSymbol

capacitance
commented property: dim(capacitance) = dim(charge/voltage) = current^2*time^4/(mass*length^2)
description: This symbol represents the physical quantity of electric capacitance. A variable representing an arbitrary quantity of capacitance is commonly represented with the italic, upper case letter, "C".
formal property: Application
  arguments: Application
    arguments: capacitance
    operator: dim
  arguments: Application
    arguments: Application
      operator: divide
    operator: dim
  arguments: Application
    operator: divide
  operator: eqs
type: ConstantSymbol

catalytic activity
commented property: dim(catalytic activity) = (amount of substance)/time
description: This symbol represents the physical quantity of catalytic activity, an amount of catalyst that effects a rate of catalytic conversion of an amount of substance.
formal property: Application
  arguments: Application
    arguments: catalytic activity
    operator: dim
  arguments: Application
    arguments: amount of substance
    arguments: time
    operator: divide
  operator: eq
type: ConstantSymbol

charge
commented property: dim(charge) = current*time
description: This symbol represents the physical quantity of electric charge. A variable representing an arbitrary quantity of charge is commonly represented with the italic, upper case letter, "Q".
formal property: Application
  arguments: Application
    arguments: charge
    operator: dim
  arguments: Application
    arguments: current
    arguments: time
    operator: times
  operator: eq
type: ConstantSymbol

concentration
commented property: dim(concentration) = (amount of substance)/length^3
description: This symbol represents the physical quantity of concentration, the amount of a substance in a volume.
formal property: Application
  arguments: Application
    arguments: concentration
    operator: dim
  arguments: Application
    arguments: amount of substance
    operator: divide
  operator: eq
type: ConstantSymbol

conductance
commented property: dim(conductance) = dim(current/voltage) = current^2*time^3/(mass*length^2)
description: This symbol represents the physical quantity of electrical conductance, the inverse of resistance. A variable representing an arbitrary quantity of conductance is commonly represented with the italic, upper case letter, "G" or "S".
formal property: Application
  arguments: Application
    arguments: conductance
    operator: dim
  arguments: Application
    arguments: Application
      operator: divide
    operator: dim
  arguments: Application
    operator: divide
  operator: eqs
type: ConstantSymbol

density
commented property: dim(density) = mass/(length^3)
description: This symbol represents the physical quantity of volumic mass density.
formal property: Application
  arguments: Application
    arguments: density
    operator: dim
  arguments: Application
    arguments: mass
    operator: divide
  operator: eq
type: ConstantSymbol

energy
commented property: dim(energy) = dim(force)*length = mass*length^2/(time^2)
description: This symbol represents the physical quantity of energy. A variable representing an arbitrary quantity of energy is commonly represented with the italic, upper case letter, "E".
formal property: Application
  arguments: Application
    arguments: energy
    operator: dim
  arguments: Application
    arguments: Application
      operator: dim
    arguments: length
    operator: times
  arguments: Application
    operator: divide
  operator: eqs
type: ConstantSymbol

entropy
commented property: dim(entropy) = dim(energy/temperature)
description: This symbol represents the physical quantity of entropy, a measure of the disorder of a system.
formal property: Application
  arguments: Application
    arguments: entropy
    operator: dim
  arguments: Application
    arguments: Application
      operator: divide
    operator: dim
  operator: eq
type: ConstantSymbol

equivalent dose
commented property: dim(equivalent dose) = dim(energy/mass)
description: This symbol represents the physical quantity of equivalent dose of ionizing radiation. Equivalent dose is similar to absorbed dose but is weighted to reflect differing biological effects and different radiation types. A variable representing an arbitrary quantity of equivalent dose is commonly represented with the italic, upper case letter, "H".
formal property: Application
  arguments: Application
    arguments: equivalent dose
    operator: dim
  arguments: Application
    arguments: Application
      operator: divide
    operator: dim
  operator: eq
type: ConstantSymbol

force
commented property: dim(force) = mass*length/(time^2)
description: This symbol represents the physical quantity of force. A variable representing an arbitrary quantity of force is commonly represented with the italic, upper case letter, "F".
formal property: Application
  arguments: Application
    arguments: force
    operator: dim
  arguments: Application
    arguments: Application
      operator: times
    operator: divide
  operator: eq
type: ConstantSymbol

frequency
commented property: dim(frequency) = one/time
description: This symbol represents the physical quantity of frequency. A variable representing an arbitrary quantity of frequency is commonly represented with the italic, lower case greek variable, "\omega;".
formal property: Application
  arguments: Application
    arguments: frequency
    operator: dim
  arguments: Application
    arguments: one
    arguments: time
    operator: divide
  operator: eq
type: ConstantSymbol

heat
commented property: dim(heat) = dim(energy) = mass*length^2/(time^2)
description: This symbol represents the physical quantity of energy that is transferred from one object to another due to a difference in temperature.
formal property: Application
  arguments: Application
    arguments: heat
    operator: dim
  arguments: Application
    arguments: energy
    operator: dim
  arguments: Application
    operator: divide
  operator: eqs
type: ConstantSymbol

illuminance
commented property: dim(illuminance) = dim(luminous flux)/(length^2) = (luminous intensity)/(length^2)
description: This symbol represents the physical quantity of illuminance. A variable representing an arbitrary quantity of illuminance is commonly represented with the italic, upper case letter, "E".
formal property: Application
  arguments: Application
    arguments: illuminance
    operator: dim
  arguments: Application
    arguments: Application
      operator: dim
    operator: divide
  arguments: Application
    arguments: luminous intensity
    operator: divide
  operator: eqs
type: ConstantSymbol

inductance
commented property: dim(inductance) = dim(voltage)*time/current = mass*length^2/(current^2*time^2)
description: This symbol represents the physical quantity of electrical inductance. A variable representing an arbitrary quantity of inductance is commonly represented with the italic, upper case letter, "L".
formal property: Application
  arguments: Application
    arguments: inductance
    operator: dim
  arguments: Application
    arguments: Application
      operator: times
    arguments: current
    operator: divide
  arguments: Application
    operator: divide
  operator: eqs
type: ConstantSymbol

luminous flux
commented property: dim(luminous flux) = (luminous intensity)*dim(solid angle) = (luminous intensity)
description: This symbol represents the physical quantity of luminous flux. A variable representing an arbitrary quantity of luminous flux is commonly represented with the italic, upper case letter, "Φv" (\phi; sub V).
formal property: Application
  arguments: Application
    arguments: luminous flux
    operator: dim
  arguments: Application
    arguments: luminous intensity
    operator: times
  operator: eqs
type: ConstantSymbol

magnetic flux
commented property: dim(magnetic flux) = dim(energy/current) = mass*length^2/(current*time^2)
description: This symbol represents the physical quantity of magnetic flux. A variable representing an arbitrary quantity of magnetic flux is commonly represented with the italic, upper case greek letter, "\Phi;".
formal property: Application
  arguments: Application
    arguments: magnetic flux
    operator: dim
  arguments: Application
    arguments: Application
      operator: divide
    operator: dim
  arguments: Application
    operator: divide
  operator: eqs
type: ConstantSymbol

magnetic flux density
commented property: dim(magnetic flux density) = dim(magnetic flux)/(length^2) = mass/(current*time^2)
description: This symbol represents the physical quantity of magnetic flux density. A variable representing an arbitrary quantity of magnetic flux density is commonly represented with the italic, upper case letter, "B".
formal property: Application
  arguments: Application
    arguments: magnetic flux density
    operator: dim
  arguments: Application
    arguments: Application
      operator: dim
    operator: divide
  arguments: Application
    arguments: mass
    operator: divide
  operator: eqs
type: ConstantSymbol

moment of force
commented property: dim(moment of force) = length*dim(force) = mass*length^2/(time^2)
description: This symbol represents the physical quantity of force.
formal property: Application
  arguments: Application
    arguments: moment of force
    operator: dim
  arguments: Application
    arguments: length
    operator: times
  arguments: Application
    operator: divide
  operator: eqs
type: ConstantSymbol

momentum
commented property: dim(momentum) = mass*length/time
description: This symbol represents the physical quantity of momentum.
formal property: Application
  arguments: Application
    arguments: momentum
    operator: dim
  arguments: Application
    arguments: Application
      operator: times
    arguments: time
    operator: divide
  operator: eq
type: ConstantSymbol

power
commented property: dim(power) = dim(energy)/time = mass*length^2/(time^3)
description: This symbol represents the physical quantity of power, or energy divided by time. A variable representing an arbitrary quantity of power is commonly represented with the italic, upper case letter, "P".
formal property: Application
  arguments: Application
    arguments: power
    operator: dim
  arguments: Application
    arguments: Application
      operator: dim
    arguments: time
    operator: divide
  arguments: Application
    operator: divide
  operator: eqs
type: ConstantSymbol

pressure
commented property: dim(pressure) = dim(force)/dim(area) = mass/(length*time*time)
description: This symbol represents the physical quantity of pressure. A variable representing an arbitrary quantity of pressure is commonly represented with the italic, lower case letter, "p".
formal property: Application
  arguments: Application
    arguments: pressure
    operator: dim
  arguments: Application
    arguments: Application
      operator: dim
    operator: divide
  arguments: Application
    arguments: mass
    operator: divide
  operator: eqs
type: ConstantSymbol

radioactivity
commented property: dim(radioactivity) = dim(1/time)
description: This symbol represents the physical quantity of radio nuclide activity, or radioactivity. A variable representing an arbitrary quantity of radioactivity is commonly represented with the italic, upper case letter, "A".
formal property: Application
  arguments: Application
    arguments: radioactivity
    operator: dim
  arguments: Application
    arguments: Literal
      value: 1
    arguments: time
    operator: divide
  operator: eq
type: ConstantSymbol

resistance
commented property: dim(resistance) = dim(voltage/current) = mass*length^2/(current^2*time^3)
description: This symbol represents the physical quantity of electrical resistance, the resistance that an electrical circuit has to electrical current. A variable representing an arbitrary quantity of electrical resistance is commonly represented with the italic, upper case letter, "R".
formal property: Application
  arguments: Application
    arguments: resistance
    operator: dim
  arguments: Application
    arguments: Application
      operator: divide
    operator: dim
  arguments: Application
    operator: divide
  operator: eqs
type: ConstantSymbol

solid angle
commented property: dim(solid angle) = one
description: This symbol represents the quantity of a two dimensional, geometric solid angle. A variable representing an arbitrary quantity of solid angle is commonly represented with the italic, upper case greek variable, "\Omega;".
formal property: Application
  arguments: Application
    arguments: solid angle
    operator: dim
  arguments: one
  operator: eq
type: ConstantSymbol

speed
commented property: dim(speed) = length/time
description: This symbol represents the physical quantity of speed. It is the size of the derivative of position with respect to time.
formal property: Application
  arguments: Application
    arguments: speed
    operator: dim
  arguments: Application
    arguments: length
    arguments: time
    operator: divide
  operator: eq
type: ConstantSymbol

voltage
commented property: dim(voltage) = dim(energy/charge) = mass*length^2/(current*time^3)
description: This symbol represents the physical quantity of voltage or electric tension. A variable representing an arbitrary quantity of voltage is commonly represented with the italic, upper case letter, "V".
formal property: Application
  arguments: Application
    arguments: voltage
    operator: dim
  arguments: Application
    arguments: Application
      operator: divide
    operator: dim
  arguments: Application
    operator: divide
  operator: eqs
type: ConstantSymbol

volume
commented property: dim(volume) = length^3
description: This symbol represents the physical quantity of volume. It has the short symbol form, "V".
formal property: Application
  arguments: Application
    arguments: volume
    operator: dim
  arguments: Application
    arguments: length
    operator: power
  operator: eq
type: ConstantSymbol

SI NamedDerivedUnits1
description: 2010-08-25 This CD defines symbols to represent the names of named derived units the SI (Syst\'eme International) system of units. (DRAFT INTERNATIONAL STANDARD ISO/DIS 80000-1 - "Quantities and units", 2008). Each unit refers to a corresponding derived quantity in SI_DerivedQuantities.ocd.
type: Library
comment: This document is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. The copyright holder grants you permission to redistribute this document freely as a verbatim copy. Furthermore, the copyright holder permits you to develop any derived work from this document provided that the following conditions are met. a) The derived work acknowledges the fact that it is derived from this document, and maintains a prominent reference in the work to the original source. b) The fact that the derived work is not the original OpenMath document is stated prominently in the derived work. Moreover if both this document and the derived work are Content Dictionaries then the derived work must include a different CDName element, chosen so that it cannot be confused with any works adopted by the OpenMath Society. In particular, if there is a Content Dictionary Group whose name is, for example, `math' containing Content Dictionaries named `math1', `math2' etc., then you should not name a derived Content Dictionary `mathN' where N is an integer. However you are free to name it `private_mathN' or some such. This is because the names `mathN' may be used by the OpenMath Society for future extensions. c) The derived work is distributed under terms that allow the compilation of derived works, but keep paragraphs a) and b) intact. The simplest way to do this is to distribute the derived work under the OpenMath license, but this is not a requirement. If you have questions about this license please contact the OpenMath society at http://www.openmath.org. Author: Joseph B. Collins (2009), Naval Research Laboratory, Washington, DC. Copyright Notice: This is a work of the U.S. Government and is not subject to copyright protection in the United States. Foreign copyrights may apply.

becquerel
commented property: unit(becquerel) = 1/(second)
description: This symbol represents an SI unit of radio nuclide activity, or radioactivity. A becquerel of activity represents one nuclear decay event per second. It has the short symbol form, "Bq".
type: ConstantSymbol

coulomb
commented property: unit(coulomb) = ampere*second
description: This symbol represents an SI unit of electric charge. It has the short symbol form, "C".
type: ConstantSymbol

degree-Celsius
commented property: unit(degree Celsius) = unit(kelvin)
description: This symbol represents an SI unit of Celsius temperature. It has the short symbol form, "ºC".
type: ConstantSymbol

farad
commented property: unit(farad) = unit(coulomb/volt)
description: This symbol represents an SI unit of electric capacitance. It has the short symbol form, "F".
type: ConstantSymbol

gram
commented property: gram = kilogram/1000
description: This symbol represents one gram. This unit is implied by the incorporation of the prefix "kilo" in the base unit standard, kilogram. Since SI prefixes may not, by SI standard, be presented by prepending to "kilogram", the gram is introduced for the application of prefixes. By itself, gram should not appear in SI compliant presentation. It has the short symbol form, "g".
type: ConstantSymbol

gray
commented property: unit(gray) = unit(joule/kilogram)
description: This symbol represents an SI unit of absorbed dose of ionizing, radiation. A gray of absorbed dose represents one joule of energy absorbed per kilogram of mass. It has the short symbol form, "Gy".
type: ConstantSymbol

henry
commented property: unit(henry) = unit(volt*second/ampere)
description: This symbol represents an SI unit of electrical inductance. It has the short symbol form, "H".
type: ConstantSymbol

hertz
commented property: unit(hertz) = one/second
description: This symbol represents an SI unit of frequency. It has the short symbol form, "Hz".
type: ConstantSymbol

joule
commented property: unit(joule) = unit(newton)*metre
description: This symbol represents an SI unit of energy. It has the short symbol form, "J".
type: ConstantSymbol

katal
commented property: unit(katal) = mole/second
description: This symbol represents an SI unit of equivalent dose of catalytic activity. A katal of catalytic activity represents the amount of catalyst to effect one mole of catalytic conversion per second. It has the short symbol form, "kat".
type: ConstantSymbol

lumen
commented property: unit(lumen) = unit(candela*steradian)
description: This symbol represents an SI unit of luminous flux. It has the short symbol form, "lm".
type: ConstantSymbol

lux
commented property: unit(lux) = unit(lumen/(metre^2))
description: This symbol represents an SI unit of illuminance. It has the short symbol form, "lx".
type: ConstantSymbol

newton
commented property: unit(newton) = kilogram*metre/second^2
description: This symbol represents an SI unit of force. It has the short symbol form, "N".
type: ConstantSymbol

ohm
commented property: unit(ohm) = unit(volt/ampere)
description: This symbol represents an SI unit of electrical resistance. It has the short symbol form, "\Omega;".
type: ConstantSymbol

pascal
commented property: unit(pascal) = unit(newton)/length^2
description: This symbol represents an SI unit of pressure. It has the short symbol form, "Pa".
type: ConstantSymbol

radian
commented property: This is a dimensionless derived unit for the SI system. It is the angle subtended at the center of a circular arc with length the same as the radius of the corresponding circle.
commented property: unit(radian) = 1
description: This symbol represents one radian, the natural unit of measure for angle. It has the short symbol form, "rad".
type: ConstantSymbol

siemens
commented property: unit(siemens) = unit(ampere/volt)
description: This symbol represents an SI unit of electrical conductance. It is not plural. It has the short symbol form, "S".
type: ConstantSymbol

sievert
commented property: unit(sievert) = unit(joule/kilogram)
description: This symbol represents an SI unit of equivalent dose of ionizing, radiation. A sievert of equivalent dose represents one joule of biologically damaging energy absorbed per kilogram of mass. It has the short symbol form, "Sv".
type: ConstantSymbol

steradian
commented property: One steradian is defined as the solid angle subtended at the center of a sphere of radius r by a part of the surface of the sphere having an area r*r.
commented property: unit(steradian) = 1
description: This symbol represents one steradian, the natural unit of measure for solid angle. It has the short symbol form, "sr".
type: ConstantSymbol

tesla
commented property: unit(tesla) = unit(weber)/(metre^2)
description: This symbol represents an SI unit of magnetic flux density. It has the short symbol form, "T".
type: ConstantSymbol

volt
commented property: unit(volt) = unit(joule/coulomb)
description: This symbol represents an SI unit of voltage or electric tension. It has the short symbol form, "V".
type: ConstantSymbol

watt
commented property: unit(watt) = unit(joule)/second
description: This symbol represents an SI unit of power, a joule per second. It has the short symbol form, "W".
type: ConstantSymbol

weber
commented property: unit(weber) = unit(joule/ampere)
description: This symbol represents an SI unit of magnetic flux. It has the short symbol form, "Wb".
type: ConstantSymbol

SI functions1
description: This CD defines symbols for functions applied to SI quantities and units.
type: Library
comment: This document is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. The copyright holder grants you permission to redistribute this document freely as a verbatim copy. Furthermore, the copyright holder permits you to develop any derived work from this document provided that the following conditions are met. a) The derived work acknowledges the fact that it is derived from this document, and maintains a prominent reference in the work to the original source. b) The fact that the derived work is not the original OpenMath document is stated prominently in the derived work. Moreover if both this document and the derived work are Content Dictionaries then the derived work must include a different CDName element, chosen so that it cannot be confused with any works adopted by the OpenMath Society. In particular, if there is a Content Dictionary Group whose name is, for example, `math' containing Content Dictionaries named `math1', `math2' etc., then you should not name a derived Content Dictionary `mathN' where N is an integer. However you are free to name it `private_mathN' or some such. This is because the names `mathN' may be used by the OpenMath Society for future extensions. c) The derived work is distributed under terms that allow the compilation of derived works, but keep paragraphs a) and b) intact. The simplest way to do this is to distribute the derived work under the OpenMath license, but this is not a requirement. If you have questions about this license please contact the OpenMath society at http://www.openmath.org. Author: Joseph B. Collins (2009), Naval Research Laboratory, Washington, DC. Copyright Notice: This is a work of the U.S. Government and is not subject to copyright protection in the United States. Foreign copyrights may apply.

dim
commented property: For named SI derived quantities and named units, the value returned by the dim operator shall be defined for each case.
commented property: The dim operator acts as the identity operation when applied to an SI base quantity.
commented property: The dim operator applied to a multiplicative inverse of a quantity is equal to the multiplicative inverse of the dim operator applied to the same quantity.
commented property: The dim operator applied to a product is equal to the associative product of the dim operator applied to the individual factors.
commented property: The dim operator applied to a product is equal to the commutative product of the dim operator applied to the factors.
commented property: The dim operator returns a value of one when applied to a dimensionless quantity or number.
commented property: The dim operator returns the corresponding SI base quantity when applied to an SI base unit.
description: The symbol to represent the function that returns the physical dimension of its argument in terms of products of powers of SI base quantities. The dim operation may be meaningfully applied to SI quantities, SI units, and numbers without physical dimension.
type: ApplicationSymbol

kind
description: The symbol to represent the function to return the kind of a quantity. The value of this function is referred to, but not defined in the SI. Its value, kind(Q) for a given quantity, Q, is left to the user to assign.
type: ApplicationSymbol

num
commented property: The num operator applied to an SI base quantity or unit returns the value one.
commented property: The num operator may be applied to any physical quantity.
commented property: The quantity num(Q)*unit(Q), may replace any quantity, Q, in a set of physical relations, if all such quantities in the set of relations are so replaced. The quantity num(Q)*unit(Q) is not always the same as Q, however dim(Q) = dim(num(Q)*unit(Q)).
description: The symbol to represent the function to return the numerical value of a quantity in terms of a product of powers of SI base units.
type: ApplicationSymbol

unit
commented property: The unit operator applied to a multiplicative inverse of a quantity is equal to the multiplicative inverse of the unit operator applied to the same quantity.
commented property: The unit operator applied to a product is equal to the associative product of the unit operator applied to the factors.
commented property: The unit operator applied to a product is equal to the commutative product of the unit operator applied to the factors.
commented property: The unit operator applied to an SI base quantity returns the corresponding SI base unit.
commented property: The unit operator applied to an SI base unit or SI coherent unit acts as the identity operator, returning that unit.
commented property: The unit operator applied to any derived quantity is equal to the unit operator applied to the result of applying the dim operator to the same quantity, i.e., unit(Q) = unit(dim(Q)).
commented property: The unit operator may be applied to any physical quantity.
commented property: The unit operator returns a value of one when applied to a dimensionless quantity or number.
description: The symbol to represent the function that returns the units of its argument in terms of a product of powers of SI base units.
type: ApplicationSymbol

aggregate cats
description: A CD of basic aggregate category constructors. This CD holds constructors of individual instances of the categories, with defining properties of the categories.
type: Library
comment: This document is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. The copyright holder grants you permission to redistribute this document freely as a verbatim copy. Furthermore, the copyright holder permits you to develop any derived work from this document provided that the following conditions are met. a) The derived work acknowledges the fact that it is derived from this document, and maintains a prominent reference in the work to the original source. b) The fact that the derived work is not the original OpenMath document is stated prominently in the derived work. Moreover if both this document and the derived work are Content Dictionaries then the derived work must include a different CDName element, chosen so that it cannot be confused with any works adopted by the OpenMath Society. In particular, if there is a Content Dictionary Group whose name is, for example, `math' containing Content Dictionaries named `math1', `math2' etc., then you should not name a derived Content Dictionary `mathN' where N is an integer. However you are free to name it `private_mathN' or some such. This is because the names `mathN' may be used by the OpenMath Society for future extensions. c) The derived work is distributed under terms that allow the compilation of derived works, but keep paragraphs a) and b) intact. The simplest way to do this is to distribute the derived work under the OpenMath license, but this is not a requirement. If you have questions about this license please contact the OpenMath society at http://www.openmath.org.

aggregateType
description: This symbol represents a generic type for aggregates (or collections of objects.
type: Symbol

continuousSetType
commented property: continuous set type has set type
description: This symbol represents the type of continuous sets.
formal property: Application
  arguments: continuousSetType
  arguments: setType
  operator: has
type: Symbol

discreteSetType
commented property: discrete set type does not have continuous set type or piecewise continuous set type
commented property: discrete set type has set type
description: This symbol represents the type of discrete sets.
formal property: Application
  arguments: discreteSetType
  arguments: setType
  operator: has
formal property: Application
  arguments: Application
    arguments: discreteSetType
    arguments: continuousSetType
    operator: has
  operator: not
type: Symbol

finiteSetType
commented property: finite set type has set type
description: This symbol represents the type of finite sets.
formal property: Application
  arguments: finiteSetType
  arguments: setType
  operator: has
type: Symbol

infiniteSetType
commented property: infinite set type does not have finite set type
commented property: infinite set type has set type
description: This symbol represents the type of infinite sets.
formal property: Application
  arguments: infiniteSetType
  arguments: setType
  operator: has
type: Symbol

multisetType
commented property: multisetType is an aggregate type
description: This symbol represents the type of multisets.
formal property: Application
  arguments: multisetType
  arguments: aggregateType
  operator: has
type: Symbol

non continuousSetType
commented property: non-continuous set type does not have continuous set type
commented property: non-continuous set type has set type
description: This symbol represents the type of non-continuous sets.
formal property: Application
  arguments: non continuousSetType
  arguments: setType
  operator: has
formal property: Application
  arguments: Application
    arguments: non continuousSetType
    arguments: continuousSetType
    operator: has
  operator: not
type: Symbol

piecewiseContinuousSetType
commented property: piecewise continuous set type has set type
description: This symbol represents the type of piecewise continuous sets.
formal property: Application
  arguments: piecewiseContinuousSetType
  arguments: setType
  operator: has
type: Symbol

setType
commented property: setType is an aggregate type
description: This symbol represents the type of sets.
formal property: Application
  arguments: setType
  arguments: aggregateType
  operator: has
type: Symbol

alg1
description: A CD of basic algebraic concepts At present this CD only holds definitions of zero and one. They are deliberately defined here without specifying any particular structure (e.g. a group) to which they correspond.
type: Library
comment: This document is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. The copyright holder grants you permission to redistribute this document freely as a verbatim copy. Furthermore, the copyright holder permits you to develop any derived work from this document provided that the following conditions are met. a) The derived work acknowledges the fact that it is derived from this document, and maintains a prominent reference in the work to the original source. b) The fact that the derived work is not the original OpenMath document is stated prominently in the derived work. Moreover if both this document and the derived work are Content Dictionaries then the derived work must include a different CDName element, chosen so that it cannot be confused with any works adopted by the OpenMath Society. In particular, if there is a Content Dictionary Group whose name is, for example, `math' containing Content Dictionaries named `math1', `math2' etc., then you should not name a derived Content Dictionary `mathN' where N is an integer. However you are free to name it `private_mathN' or some such. This is because the names `mathN' may be used by the OpenMath Society for future extensions. c) The derived work is distributed under terms that allow the compilation of derived works, but keep paragraphs a) and b) intact. The simplest way to do this is to distribute the derived work under the OpenMath license, but this is not a requirement. If you have questions about this license please contact the OpenMath society at http://www.openmath.org.

one
commented property: The one of the integers is 1
commented property: for all a | 1 * a = a
commented property: for all a | a * 1 = a
description: This symbol represents the multiplicative identity element.
formal property: Binding
  binder: forall
  body: Application
    arguments: Application
      arguments: one
      operator: times
    arguments: Variable
      name: a
    operator: eq
  variables: Variable
    name: a
formal property: Binding
  binder: forall
  body: Application
    arguments: Application
      arguments: Variable
        name: a
      arguments: one
      operator: times
    arguments: Variable
      name: a
    operator: eq
  variables: Variable
    name: a
formal property: Binding
  binder: forall
  body: Application
    arguments: Application
      arguments: Application
        operator: in
      operator: and
    arguments: Application
      operator: eq
    operator: implies
  variables: Variable
    name: x
type: ConstantSymbol

zero
commented property: The zero of the integers is 0
commented property: for all a | 0 * a = 0
commented property: for all a | a + 0 = a
description: This symbol represents the additive identity element.
formal property: Binding
  binder: forall
  body: Application
    arguments: Application
      arguments: Application
        operator: in
      operator: and
    arguments: Application
      operator: eq
    operator: implies
  variables: Variable
    name: x
formal property: Binding
  binder: forall
  body: Application
    arguments: Application
      arguments: Variable
        name: a
      arguments: zero
      operator: plus
    arguments: Variable
      name: a
    operator: eq
  variables: Variable
    name: a
formal property: Binding
  binder: forall
  body: Application
    arguments: Application
      arguments: zero
      operator: times
    arguments: zero
    operator: eq
  variables: Variable
    name: a
type: ConstantSymbol

altenc
description: A CD of alternative encoding symbols This CD is motivated in part by a desire to maintain compatibility with the MathML semantics element, In order for it to be possible for OpenMath to express symbols in an alternative encoding (this facilitates the exact translation and representation of objects) we use the OpenMath attribution nodes (which performs a similar role to the MathML semantics nodes). The formats and descriptions of common syntaxes are held in this CD; at present this only includes LaTeX and MathML.
type: Library
comment: Alternative encodings in OpenMath are dealt with by using OMATTR symbols together with the alternative encoding placed in a string. The string encoding must be valid XML, and so non-XML valid characters must themselves be encoded as suggested in "Draft of the OpenMath Standard". For alternative encodings to be represented in OpenMath, one must define a symbol to describe the encoding.
comment: This document is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. The copyright holder grants you permission to redistribute this document freely as a verbatim copy. Furthermore, the copyright holder permits you to develop any derived work from this document provided that the following conditions are met. a) The derived work acknowledges the fact that it is derived from this document, and maintains a prominent reference in the work to the original source. b) The fact that the derived work is not the original OpenMath document is stated prominently in the derived work. Moreover if both this document and the derived work are Content Dictionaries then the derived work must include a different CDName element, chosen so that it cannot be confused with any works adopted by the OpenMath Society. In particular, if there is a Content Dictionary Group whose name is, for example, `math' containing Content Dictionaries named `math1', `math2' etc., then you should not name a derived Content Dictionary `mathN' where N is an integer. However you are free to name it `private_mathN' or some such. This is because the names `mathN' may be used by the OpenMath Society for future extensions. c) The derived work is distributed under terms that allow the compilation of derived works, but keep paragraphs a) and b) intact. The simplest way to do this is to distribute the derived work under the OpenMath license, but this is not a requirement. If you have questions about this license please contact the OpenMath society at http://www.openmath.org.

LaTeX encoding
description: A symbol which heads a piece of LaTeX encoding in an attribution.
example: Application
  arguments: Attribution
    arguments: AttributionPair
      attribute key: LaTeX encoding
      attribute value: Literal
        value: \sin(1.5)
    target: Application
      arguments: Literal
        value: 1.5
      operator: sin
  operator: Example
type: Symbol
type: AttributionSymbol

MathML encoding
description: A symbol which heads a piece of MathML encoding in an attribution. The MathML encoding is an XML encoding, and the details may be found at: http://www.w3.org/Math/Overview.html
example: Application
  arguments: Attribution
    arguments: AttributionPair
      attribute key: LaTeX encoding
      attribute value: Literal
        value: \sin(1.5)
    target: Application
      arguments: Literal
        value: 1.5
      operator: sin
  operator: Example
example: Application
  arguments: Attribution
    arguments: AttributionPair
      attribute key: MathML encoding
      attribute value: Foreign
        encoding: MathML-Presentaion
        value: 3
    target: Application
      arguments: Literal
        value: 1
      operator: plus
  operator: Example
type: Symbol
type: AttributionSymbol

arith1
description: This CD defines symbols for common arithmetic functions.
type: Library
comment: This document is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. The copyright holder grants you permission to redistribute this document freely as a verbatim copy. Furthermore, the copyright holder permits you to develop any derived work from this document provided that the following conditions are met. a) The derived work acknowledges the fact that it is derived from this document, and maintains a prominent reference in the work to the original source. b) The fact that the derived work is not the original OpenMath document is stated prominently in the derived work. Moreover if both this document and the derived work are Content Dictionaries then the derived work must include a different CDName element, chosen so that it cannot be confused with any works adopted by the OpenMath Society. In particular, if there is a Content Dictionary Group whose name is, for example, `math' containing Content Dictionaries named `math1', `math2' etc., then you should not name a derived Content Dictionary `mathN' where N is an integer. However you are free to name it `private_mathN' or some such. This is because the names `mathN' may be used by the OpenMath Society for future extensions. c) The derived work is distributed under terms that allow the compilation of derived works, but keep paragraphs a) and b) intact. The simplest way to do this is to distribute the derived work under the OpenMath license, but this is not a requirement. If you have questions about this license please contact the OpenMath society at http://www.openmath.org.

abs
commented property: for all x,y | abs(x) + abs(y) >= abs(x+y)
description: 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.
formal property: Binding
  binder: forall
  body: Application
    arguments: Application
      arguments: Application
        operator: abs
      operator: plus
    arguments: Application
      operator: abs
    operator: geq
  variables: Variable
    name: x
  variables: Variable
    name: y
type: ApplicationSymbol

divide
commented property: whenever not(a=0) then a/a = 1
description: 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.
formal property: Binding
  binder: forall
  body: Application
    arguments: Application
      arguments: Variable
        name: a
      arguments: zero
      operator: neq
    arguments: Application
      operator: eq
    operator: implies
  variables: Variable
    name: a
type: ApplicationSymbol

gcd
commented property: for all integers a,b | There does not exist a c such that a/c is an Integer and b/c is an Integer and c > gcd(a,b). Note that this implies that gcd(a,b) > 0
description: The symbol to represent the n-ary function to return the gcd (greatest common divisor) of its arguments.
example: Application
  arguments: Literal
    value: gcd(6,9) = 3
  arguments: Application
    arguments: Application
      operator: gcd
    operator: eq
  operator: Example
formal property: Binding
  binder: forall
  body: Application
    arguments: Application
      arguments: Application
        operator: in
      operator: and
    arguments: Application
      operator: not
    operator: implies
  variables: Variable
    name: a
  variables: Variable
    name: b
type: ApplicationSymbol

lcm
commented property: for all integers a,b | There does not exist a c>0 such that c/a is an Integer and c/b is an Integer and lcm(a,b) > c.
commented property: lcm(a,b) = a*b/gcd(a,b)
description: The symbol to represent the n-ary function to return the least common multiple of its arguments.
formal property: Application
  arguments: Application
    arguments: Variable
      name: a
    arguments: Variable
      name: b
    operator: lcm
  arguments: Application
    arguments: Application
      operator: times
    operator: divide
  operator: eq
formal property: Binding
  binder: forall
  body: Application
    arguments: Application
      arguments: Application
        operator: in
      operator: and
    arguments: Application
      operator: not
    operator: implies
  variables: Variable
    name: a
  variables: Variable
    name: b
type: ApplicationSymbol

minus
commented property: for all a,b | a - b = a + (-b)
description: The symbol representing a binary minus function. This is equivalent to adding the additive inverse.
formal property: Binding
  binder: forall
  body: Application
    arguments: Application
      arguments: Variable
        name: a
      operator: minus
    arguments: Application
      operator: plus
    operator: eq
  variables: Variable
    name: a
  variables: Variable
    name: b
type: ApplicationSymbol

plus
commented property: for all a,b | a + b = b + a
description: The symbol representing an n-ary commutative function plus.
formal property: Binding
  binder: forall
  body: Application
    arguments: Application
      arguments: Variable
        name: a
      operator: plus
    arguments: Application
      operator: plus
    operator: eq
  variables: Variable
    name: a
  variables: Variable
    name: b
type: ApplicationSymbol

power
commented property: if n is an integer then x^0 = 1, x^n = x * x^(n-1)
commented property: x\in C implies x^a = exp(a ln x)
description: 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.
example: Application
  arguments: Application
    arguments: Application
      operator: power
    arguments: Application
      operator: matrix
    operator: eq
  operator: Example
example: Application
  arguments: Application
    arguments: Application
      arguments: http://www.openmath.org/cd/nums1#e
      operator: power
    arguments: Application
      operator: unary minus
    operator: eq
  operator: Example
formal property: Application
  arguments: Application
    arguments: Variable
      name: x
    arguments: http://www.openmath.org/cd/setname1#C
    operator: in
  arguments: Application
    arguments: Application
      operator: power
    operator: eq
  operator: implies
formal property: Application
  arguments: Application
    arguments: Variable
      name: n
    arguments: http://www.openmath.org/cd/setname1#Z
    operator: in
  arguments: Application
    arguments: Application
      operator: eq
    operator: and
  operator: implies
type: ApplicationSymbol

product
description: 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.
example: Application
  arguments: Literal
    value: This represents the statement that the factorial of n is equal to the product of all the integers between 1 and n inclusive.
  arguments: Application
    arguments: Application
      operator: factorial
    operator: eq
  operator: Example
type: ApplicationSymbol

root
commented property: for all a,n | power(root(a,n),n) = a (if the root exists!)
commented property: x\in C implies root(x,n) = exp(ln(x)/n)
description: 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.
formal property: Application
  arguments: Application
    arguments: Variable
      name: x
    arguments: http://www.openmath.org/cd/setname1#C
    operator: in
  arguments: Application
    arguments: Application
      operator: root
    operator: eq
  operator: implies
formal property: Binding
  binder: forall
  body: Application
    arguments: Application
      arguments: Application
        operator: root
      operator: power
    arguments: Variable
      name: a
    operator: eq
  variables: Variable
    name: a
  variables: Variable
    name: n
type: ApplicationSymbol

sum
description: 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.
example: Application
  arguments: Literal
    value: This represents the summation of the reciprocals of all the integers between 1 and 10 inclusive.
  arguments: Application
    arguments: Application
      operator: integer interval
    operator: sum
  operator: Example
type: ApplicationSymbol

times
commented property: for all a,b | a * 0 = 0 and a * b = a * (b - 1) + a
commented property: for all a,b,c | a*(b+c) = a*b + a*c
description: The symbol representing an n-ary multiplication function.
example: Application
  arguments: Application
    arguments: Application
      operator: times
    arguments: Application
      operator: matrix
    operator: eq
  operator: Example
formal property: Binding
  binder: forall
  body: Application
    arguments: Application
      arguments: Application
        operator: times
      arguments: zero
      operator: eq
    arguments: Application
      operator: eq
    operator: and
  variables: Variable
    name: a
  variables: Variable
    name: b
formal property: Binding
  binder: forall
  body: Application
    arguments: Application
      arguments: Variable
        name: a
      operator: times
    arguments: Application
      operator: plus
    operator: eq
  variables: Variable
    name: a
  variables: Variable
    name: b
  variables: Variable
    name: c
type: ApplicationSymbol

unary minus
commented property: for all a | a + (-a) = 0
description: This symbol denotes unary minus, i.e. the additive inverse.
formal property: Binding
  binder: forall
  body: Application
    arguments: Application
      arguments: Variable
        name: a
      operator: plus
    arguments: zero
    operator: eq
  variables: Variable
    name: a
type: ApplicationSymbol

arith2
description: Further to the basic arithmetic functions, we define some more common arithmetic operations. This includes a commutative times which exhibits the use of inheritance within the CD's.
type: Library
comment: This document is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. The copyright holder grants you permission to redistribute this document freely as a verbatim copy. Furthermore, the copyright holder permits you to develop any derived work from this document provided that the following conditions are met. a) The derived work acknowledges the fact that it is derived from this document, and maintains a prominent reference in the work to the original source. b) The fact that the derived work is not the original OpenMath document is stated prominently in the derived work. Moreover if both this document and the derived work are Content Dictionaries then the derived work must include a different CDName element, chosen so that it cannot be confused with any works adopted by the OpenMath Society. In particular, if there is a Content Dictionary Group whose name is, for example, `math' containing Content Dictionaries named `math1', `math2' etc., then you should not name a derived Content Dictionary `mathN' where N is an integer. However you are free to name it `private_mathN' or some such. This is because the names `mathN' may be used by the OpenMath Society for future extensions. c) The derived work is distributed under terms that allow the compilation of derived works, but keep paragraphs a) and b) intact. The simplest way to do this is to distribute the derived work under the OpenMath license, but this is not a requirement. If you have questions about this license please contact the OpenMath society at http://www.openmath.org.

inverse
commented property: inverse(inverse(a))=a
description: A unary operator which represents the inverse of an element of a set. This symbol could be used to represent additive or multiplicative inverses.
formal property: Binding
  binder: forall
  body: Application
    arguments: Application
      arguments: Application
        operator: inverse
      operator: inverse
    arguments: Variable
      name: a
    operator: eq
  variables: Variable
    name: a
type: ApplicationSymbol

times
commented property: for all a,b | a * b = b * a
description: The symbol representing an n-ary multiplication function inheriting from the times in arith1, but with the extra property that here it must be commutative.
formal property: Binding
  binder: forall
  body: Application
    arguments: Application
      arguments: Variable
        name: a
      operator: times
    arguments: Application
      operator: times
    operator: eq
  variables: Variable
    name: a
  variables: Variable
    name: b
type: ApplicationSymbol

arith3
description: Extended GCD
type: Library

extended gcd
description: The symbol represents the n-ary function, a_1,...,a_n to return a list consisting of the gcd (greatest common divisor) of its arguments, together with n elements x_1,...,x_n such that gcd(a_1,...,a_n)=x_1 a_1+...+x_n a_n
example: Application
  arguments: Application
    arguments: Application
      operator: extended gcd
    arguments: Application
      operator: list
    operator: extended gcd
  operator: Example
type: Symbol

asymp1
description: This CD provides a representation of various asymptotic set constructors (O, \Omega, etc.) The constructors represent sets of functions : R -> R.
type: Library
comment: This document is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. The copyright holder grants you permission to redistribute this document freely as a verbatim copy. Furthermore, the copyright holder permits you to develop any derived work from this document provided that the following conditions are met. a) The derived work acknowledges the fact that it is derived from this document, and maintains a prominent reference in the work to the original source. b) The fact that the derived work is not the original OpenMath document is stated prominently in the derived work. Moreover if both this document and the derived work are Content Dictionaries then the derived work must include a different CDName element, chosen so that it cannot be confused with any works adopted by the OpenMath Society. In particular, if there is a Content Dictionary Group whose name is, for example, `math' containing Content Dictionaries named `math1', `math2' etc., then you should not name a derived Content Dictionary `mathN' where N is an integer. However you are free to name it `private_mathN' or some such. This is because the names `mathN' may be used by the OpenMath Society for future extensions. c) The derived work is distributed under terms that allow the compilation of derived works, but keep paragraphs a) and b) intact. The simplest way to do this is to distribute the derived work under the OpenMath license, but this is not a requirement. If you have questions about this license please contact the OpenMath society at http://www.openmath.org.

http://www.openmath.org/cd/asymp1#O
commented property: O(g) = { f:reals -> reals | exists c in positive reals and M in the naturals such that forall n geq M. |f(n)| leq c*g(n)}
description: The O symbol represents a unary function which constructs a set of certain functions of type reals to reals. The condition f(n)=O(g(n)) is intended to express an upper bound condition on f.
formal property: Application
  arguments: Application
    arguments: Variable
      name: g
    operator: http://www.openmath.org/cd/asymp1#O
  arguments: Application
    arguments: Application
      operator: function set
    operator: suchthat
  operator: eq
type: Symbol

Omega
commented property: f(x) is Omega(g(x)) if and only if it is not true that f(x) is O(g(x))
description: The Omega symbol represents a unary function which constructs a set of certain functions of type reals to positive reals. The Omega symbol represents a set of functions such that for any function in the set Omega(g(x)), f(x); it is not true that f(x) is in O(g(x)).
formal property: Application
  arguments: Application
    arguments: Variable
      name: g
    operator: Omega
  arguments: Application
    arguments: Application
      operator: function set
    operator: suchthat
  operator: eq
type: Symbol

asymptotic
commented property: f(x) is asymptotic g(x) if and only if the limit as x tends to infinity of f(x)/g(x) = 1
description: The asymptotic symbol represents a binary relation between two functions of type reals to reals. The asymptotic relation between two functions returns true if the two functions have the same rate of growth and more precisely there ratio approaches 1 as the variable approaches infinity. Formally we say that f(x) is asymptotic to g(x) if and only if the limit as x tends to infinity of f(x)/g(x) = 1.
formal property: Application
  arguments: Application
    arguments: Variable
      name: f
    arguments: Variable
      name: g
    operator: asymptotic
  arguments: Application
    arguments: Application
      operator: limit
    arguments: one
    operator: eq
  operator: equivalent
type: Symbol

http://www.openmath.org/cd/asymp1#o
commented property: o(g) = {f : reals -> reals | the limit as x tends to infinity of f(x)/g(x) is 0}
description: The o symbol represents a unary function which constructs a set of certain functions of type reals to positive reals. The condition f(n) = o(g(n)) is intended to express a lower bouund condition on f. Formally we say that f(n) = o(g(n)) if and only if the limit as n tends to infinity of f(n)/g(n) exists and is equal to 0.
formal property: Application
  arguments: Application
    arguments: Variable
      name: g
    operator: http://www.openmath.org/cd/asymp1#o
  arguments: Application
    arguments: Application
      operator: function set
    operator: suchthat
  operator: eq
type: Symbol

omega
commented property: f(x) = omega(g(x)) if and only if there is an epsilon > 0 and an infinite sequence x_1, x_2, x_3, ... such that for all j then abs(f(x_j)) > epsilon * g(x_j).
commented property: f(x) is omega(g(x)) if and only if it is not true that f(x) is o(g(x))
description: The omega symbol represents a unary function which constructs a set of certain functions of type reals to positive reals. The omega symbol represents a set of functions such that for any function in the set omega(g(x)), f(x); it is not true that f(x) is in o(g(x)). Formally we say that f(x) = omega(g(x)) if and only if there is an epsilon > 0 and an infinite sequence x_1, x_2, x_3, ... such that for all j then abs(f(x_j)) > epsilon * g(x_j).
formal property: Application
  arguments: Application
    arguments: Variable
      name: g
    operator: omega
  arguments: Application
    arguments: Application
      operator: function set
    operator: suchthat
  operator: eq
formal property: Application
  arguments: Application
    arguments: Variable
      name: f
    arguments: Application
      operator: omega
    operator: in
  arguments: Binding
    binder: exists
    body: Application
      operator: and
    variables: Variable
      name: epsilon
  operator: equivalent
type: Symbol

theta
commented property: f(x) = theta(g(x)) if and only if there are constants c_1 not= 0 and c_2 not= 0 and x_0 such that for all x > x_0 it is true that c_1*g(x) < f(x) < c_2*g(x)
description: The theta symbol represents a unary function which constructs a set of certain functions of type reals to positive reals. The theta symbol represents a set of functions which all have the same 'rate of growth'. Formally we say that f(x) = theta(g(x)) if and only if there are constants c_1 not= 0 and c_2 not= 0 and x_0 such that for all x > x_0 it is true that c_1*g(x) < f(x) < c_2*g(x).
formal property: Application
  arguments: Application
    arguments: Variable
      name: g
    operator: theta
  arguments: Application
    arguments: Application
      operator: function set
    operator: suchthat
  operator: eq
type: Symbol

bigfloat1
description: This CD provides a common representation of "bigfloats" in a mantissa/ radix/exponent format. There is a further version, which provides an opportunity to state a precision (only required in a different radix). No operations are defined here -- see arith and alg.
type: Library
comment: This document is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. The copyright holder grants you permission to redistribute this document freely as a verbatim copy. Furthermore, the copyright holder permits you to develop any derived work from this document provided that the following conditions are met. a) The derived work acknowledges the fact that it is derived from this document, and maintains a prominent reference in the work to the original source. b) The fact that the derived work is not the original OpenMath document is stated prominently in the derived work. Moreover if both this document and the derived work are Content Dictionaries then the derived work must include a different CDName element, chosen so that it cannot be confused with any works adopted by the OpenMath Society. In particular, if there is a Content Dictionary Group whose name is, for example, `math' containing Content Dictionaries named `math1', `math2' etc., then you should not name a derived Content Dictionary `mathN' where N is an integer. However you are free to name it `private_mathN' or some such. This is because the names `mathN' may be used by the OpenMath Society for future extensions. c) The derived work is distributed under terms that allow the compilation of derived works, but keep paragraphs a) and b) intact. The simplest way to do this is to distribute the derived work under the OpenMath license, but this is not a requirement. If you have questions about this license please contact the OpenMath society at http://www.openmath.org.
comment: Written by James Davenport on 1999-07-13. bigfloatprec added 1999-07-21.

bigfloat
commented property: bigfloat(m,r,e)=m*r^e
description: The bigfloat constructor takes three arguments, a mantissa, a base and the exponent.
formal property: Application
  arguments: Application
    arguments: Variable
      name: m
    arguments: Variable
      name: r
    operator: bigfloat
  arguments: Application
    arguments: Variable
      name: m
    operator: times
  operator: eq
type: ApplicationSymbol

bigfloatprec
commented property: bigfloatprec(f,r,p)=f However, if converted to radix r, only p digits in that radix are significant. This usually means that it originated in radix r, and has since (e.g. for display purposes) been converted into its current radix. For exposition, f = m*r^e.
description: The bigfloat "with precision specified in (another) radix" constructor. Takes 3 arguments, the first argument is a floating point number constructed with the bigfloat constructor, the second is the new radix, whilst the third specifies how many digits are significant.
formal property: Application
  arguments: Application
    arguments: Application
      operator: bigfloat
    arguments: Variable
      name: r
    operator: bigfloatprec
  arguments: Application
    arguments: Variable
      name: m
    operator: bigfloat
  operator: eq
type: ApplicationSymbol

calculus1
description: This CD is intended to be compatible with the calculus operations in Content MathML. Integration is just for the univariate case and is either definite or indefinite.
type: Library
comment: This document is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. The copyright holder grants you permission to redistribute this document freely as a verbatim copy. Furthermore, the copyright holder permits you to develop any derived work from this document provided that the following conditions are met. a) The derived work acknowledges the fact that it is derived from this document, and maintains a prominent reference in the work to the original source. b) The fact that the derived work is not the original OpenMath document is stated prominently in the derived work. Moreover if both this document and the derived work are Content Dictionaries then the derived work must include a different CDName element, chosen so that it cannot be confused with any works adopted by the OpenMath Society. In particular, if there is a Content Dictionary Group whose name is, for example, `math' containing Content Dictionaries named `math1', `math2' etc., then you should not name a derived Content Dictionary `mathN' where N is an integer. However you are free to name it `private_mathN' or some such. This is because the names `mathN' may be used by the OpenMath Society for future extensions. c) The derived work is distributed under terms that allow the compilation of derived works, but keep paragraphs a) and b) intact. The simplest way to do this is to distribute the derived work under the OpenMath license, but this is not a requirement. If you have questions about this license please contact the OpenMath society at http://www.openmath.org.

defint
commented property: for all a < b < c | integral over [a,c] = integral over [a,b] + integral over [b,c]
commented property: for all a,b | integral from a to b = -integral from b to a
description: This symbol is used to represent definite integration of unary functions. It takes two arguments; the first being the range (e.g. a set) of integration, and the second the function.
example: Application
  arguments: Literal
    value: An example to represent the definite integration of sin(x) between the points -1.0 and 1.0.
  arguments: Application
    arguments: Application
      operator: ordered interval
    operator: defint
  operator: Example
example: Application
  arguments: Literal
    value: An example to represent the definite integration of f(x), for x in the set C:
  arguments: Application
    arguments: Variable
      name: C
    operator: defint
  operator: Example
formal property: Binding
  binder: forall
  body: Application
    arguments: Application
      arguments: Application
        operator: ordered interval
      operator: defint
    arguments: Application
      operator: unary minus
    operator: eq
  variables: Variable
    name: a
  variables: Variable
    name: b
formal property: Binding
  binder: forall
  body: Application
    arguments: Application
      arguments: Application
        operator: lt
      operator: and
    arguments: Application
      operator: eq
    operator: implies
  variables: Variable
    name: a
  variables: Variable
    name: b
  variables: Variable
    name: c
type: ApplicationSymbol

diff
commented property: diff(lambda y:a(y) * b(y))(x) = diff(lambda y:a(y))(x) * b(x) + a(x) * diff(lambda y:b(y))(x)
commented property: diff(lambda y:a(y) + b(y))(x) = diff(lambda y:a(y))(x) + diff(lambda y:b(y))(x)
description: This symbol is used to express ordinary differentiation of a unary function. The single argument is the unary function.
example: Application
  arguments: Literal
    value: This represents the equation: derivative(x + 1.0) = 1.0
  arguments: Application
    arguments: Application
    operator: eq
  operator: Example
formal property: Application
  arguments: Application
    arguments: Variable
      name: x
    operator: Application
      arguments: Binding
        binder: lambda
      operator: diff
  arguments: Application
    arguments: Application
    operator: plus
  operator: eq
formal property: Application
  arguments: Application
    arguments: Variable
      name: x
    operator: Application
      arguments: Binding
        binder: lambda
      operator: diff
  arguments: Application
    arguments: Application
      operator: times
    operator: plus
  operator: eq
type: ApplicationSymbol

int
commented property: application of integrate followed by differentiate is the identity function, that is: diff(lambda y:integral(lambda z:f(z))(y)) = f
description: This symbol is used to represent indefinite integration of unary functions. The argument is the unary function.
example: Application
  arguments: Literal
    value: An example which represents the equation: integral(x +-> sin(x)) w.r.t. x = x +-> -cos(x)
  arguments: Application
    arguments: Application
      operator: int
    operator: eq
  operator: Example
formal property: Application
  arguments: Application
    arguments: Binding
      binder: lambda
      body: Application
    operator: diff
  arguments: Variable
    name: f
  operator: eq
type: ApplicationSymbol

nthdiff
description: This symbol is used to express the nth-iterated ordinary differentiation of a unary function. The first argument is n, and the second the unary function.
formal property: Application
  arguments: Application
    arguments: zero
    arguments: Variable
      name: f
    operator: nthdiff
  arguments: Variable
    name: f
  operator: eq
formal property: Application
  arguments: Application
    arguments: Application
      operator: plus
    arguments: Variable
      name: f
    operator: nthdiff
  arguments: Application
    arguments: Application
      operator: nthdiff
    operator: diff
  operator: eq
type: ApplicationSymbol

nthpartialdiff
commented property: \frac{\partial^{n+m}}{\partial x^n\partial y^m} f(x,y,z) = \frac{\partial^n}{\partial x^n}(\frac{\partial^m}{\partial y^m}(f(x,y,z)))
description: This symbol is used to express the nth-iterated partial differentiation of a function of more than one variable. It has three arguments, the first is a list of positive integers which index the variables of the function, the second is a list of integers which specify the order of differentiation with respect to the corresponding variable, the third argument is the function. Application of the symbol should be taken as meaning the following: differentiation of the third argument with respect to the variables indexed by the first argument. The orders of differentiation are specified by the second argument, in the following manner: The i'th element of the second argument is the order of differentiation of the variable indexed by the i'th element of the first argument.
formal property: Application
  arguments: Application
    arguments: Application
      operator: list
    arguments: Application
      operator: list
    operator: nthpartialdiff
  arguments: Application
    arguments: Application
      operator: list
    operator: nthpartialdiff
  operator: eq
type: Symbol

partialdiff
description: This symbol is used to express partial differentiation of a function of more than one variable. It has two arguments, the first is a list of integers which index the variables of the function, the second is the function.
example: Application
  arguments: Literal
    value: An example to represent the equation: \partial^2{xyz}/ \partial{x}\partial{z} = y
  arguments: Application
    arguments: Application
    operator: eq
  operator: Example
type: ApplicationSymbol

partialdiffdegree
description: This symbol is used to express partial differentiation of a function of more than one variable. It has three arguments, the first is a list of integers which give the degrees by which the function is differentiated by the corresponding variable. The second is the total degree (which should therefore be the sum of the values in the first list, but may be given symbolically). The third is the function.
example: Application
  arguments: Literal
    value: An example to represent the equation: \partial^2{xyz}/ \partial{x}\partial{z} = y
  arguments: Application
    arguments: Application
    operator: eq
  operator: Example
type: ApplicationSymbol

calculus2
description: This CD provides a vocabulary for talking about integrals.
type: Library
comment: This document is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. The copyright holder grants you permission to redistribute this document freely as a verbatim copy. Furthermore, the copyright holder permits you to develop any derived work from this document provided that the following conditions are met. a) The derived work acknowledges the fact that it is derived from this document, and maintains a prominent reference in the work to the original source. b) The fact that the derived work is not the original OpenMath document is stated prominently in the derived work. Moreover if both this document and the derived work are Content Dictionaries then the derived work must include a different CDName element, chosen so that it cannot be confused with any works adopted by the OpenMath Society. In particular, if there is a Content Dictionary Group whose name is, for example, `math' containing Content Dictionaries named `math1', `math2' etc., then you should not name a derived Content Dictionary `mathN' where N is an integer. However you are free to name it `private_mathN' or some such. This is because the names `mathN' may be used by the OpenMath Society for future extensions. c) The derived work is distributed under terms that allow the compilation of derived works, but keep paragraphs a) and b) intact. The simplest way to do this is to distribute the derived work under the OpenMath license, but this is not a requirement. If you have questions about this license please contact the OpenMath society at http://www.openmath.org.

integrand
description: This symbol represents the integrand of the integral.
example: Application
  arguments: Application
    arguments: Application
      operator: integrand
    arguments: Application
      operator: sin
    operator: eq
  operator: Example
type: Symbol

variable of integration
description: This symbol represents the variable with respect to which an integral is calculated.
example: Application
  arguments: Application
    arguments: Application
      operator: variable of integration
    arguments: Variable
      name: x
    operator: eq
  operator: Example
type: Symbol

cc
description: CC Type Attribution for OM Initial version: O. Caprotti (May 20, 1999) Revised: O. Caprotti (Aug 20, 1999), split-up so that it uses symbols from lc, omtypes.
type: Library
comment: This document is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. The copyright holder grants you permission to redistribute this document freely as a verbatim copy. Furthermore, the copyright holder permits you to develop any derived work from this document provided that the following conditions are met. a) The derived work acknowledges the fact that it is derived from this document, and maintains a prominent reference in the work to the original source. b) The fact that the derived work is not the original OpenMath document is stated prominently in the derived work. Moreover if both this document and the derived work are Content Dictionaries then the derived work must include a different CDName element, chosen so that it cannot be confused with any works adopted by the OpenMath Society. In particular, if there is a Content Dictionary Group whose name is, for example, `math' containing Content Dictionaries named `math1', `math2' etc., then you should not name a derived Content Dictionary `mathN' where N is an integer. However you are free to name it `private_mathN' or some such. This is because the names `mathN' may be used by the OpenMath Society for future extensions. c) The derived work is distributed under terms that allow the compilation of derived works, but keep paragraphs a) and b) intact. The simplest way to do this is to distribute the derived work under the OpenMath license, but this is not a requirement. If you have questions about this license please contact the OpenMath society at http://www.openmath.org.

type
description: Attribution tag to denote type-judgement
type: Symbol
type: SemanticAttributionSymbol

typecoerce
description: Attribution tag to denote type-judgement with coercion
type: SemanticAttributionSymbol

coercions
description: Coercion Functions among OM Types Initial version: O. Caprotti
type: Library
comment: This document is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. The copyright holder grants you permission to redistribute this document freely as a verbatim copy. Furthermore, the copyright holder permits you to develop any derived work from this document provided that the following conditions are met. a) The derived work acknowledges the fact that it is derived from this document, and maintains a prominent reference in the work to the original source. b) The fact that the derived work is not the original OpenMath document is stated prominently in the derived work. Moreover if both this document and the derived work are Content Dictionaries then the derived work must include a different CDName element, chosen so that it cannot be confused with any works adopted by the OpenMath Society. In particular, if there is a Content Dictionary Group whose name is, for example, `math' containing Content Dictionaries named `math1', `math2' etc., then you should not name a derived Content Dictionary `mathN' where N is an integer. However you are free to name it `private_mathN' or some such. This is because the names `mathN' may be used by the OpenMath Society for future extensions. c) The derived work is distributed under terms that allow the compilation of derived works, but keep paragraphs a) and b) intact. The simplest way to do this is to distribute the derived work under the OpenMath license, but this is not a requirement. If you have questions about this license please contact the OpenMath society at http://www.openmath.org.

int2flt
description: The function that converts an integer to a float.
example: Application
  arguments: Attribution
    arguments: AttributionPair
      attribute key: type
      attribute value: float
    target: Application
      arguments: Literal
        value: 1
      operator: int2flt
  arguments: Literal
    value: is well-typed object.
  operator: Example
type: ApplicationSymbol

combinat1
description: This CD defines some basic combinatorics definitions.
type: Library
comment: This document is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. The copyright holder grants you permission to redistribute this document freely as a verbatim copy. Furthermore, the copyright holder permits you to develop any derived work from this document provided that the following conditions are met. a) The derived work acknowledges the fact that it is derived from this document, and maintains a prominent reference in the work to the original source. b) The fact that the derived work is not the original OpenMath document is stated prominently in the derived work. Moreover if both this document and the derived work are Content Dictionaries then the derived work must include a different CDName element, chosen so that it cannot be confused with any works adopted by the OpenMath Society. In particular, if there is a Content Dictionary Group whose name is, for example, `math' containing Content Dictionaries named `math1', `math2' etc., then you should not name a derived Content Dictionary `mathN' where N is an integer. However you are free to name it `private_mathN' or some such. This is because the names `mathN' may be used by the OpenMath Society for future extensions. c) The derived work is distributed under terms that allow the compilation of derived works, but keep paragraphs a) and b) intact. The simplest way to do this is to distribute the derived work under the OpenMath license, but this is not a requirement. If you have questions about this license please contact the OpenMath society at http://www.openmath.org.
comment: Written by S. Dalmas (INRIA Sophia Antipolis) for the Esprit OpenMath project.

Bell
commented property: Bell(n) = the sum from k=0 to n of Stirling2(n,k)
description: The Bell numbers: Bell(n) is the total number of possible partitions of a set of n elements.
example: Application
  arguments: Application
    arguments: Application
      operator: Bell
    arguments: Literal
      value: 877
    operator: eq
  operator: Example
formal property: Application
  arguments: Application
    arguments: Variable
      name: n
    operator: Bell
  arguments: Application
    arguments: Application
      operator: integer interval
    operator: sum
  operator: eq
type: ApplicationSymbol

Fibonacci
commented property: Fibonacci(0) = 0, Fibonacci(1) = 1, and Fibonacci(n + 1) = Fibonacci(n) + Fibonacci(n - 1)
description: The Fibonacci numbers, defined by the linear recurrence: Fibonacci(0) = 0, Fibonacci(1) = 1, and Fibonacci(n + 1) = Fibonacci(n) + Fibonacci(n - 1). Note that some authors define Fibonacci(0) = 1.
example: Application
  arguments: Application
    arguments: Application
      operator: Fibonacci
    arguments: Literal
      value: 55
    operator: eq
  operator: Example
formal property: Application
  arguments: Application
    arguments: Application
      arguments: zero
      operator: Fibonacci
    arguments: zero
    operator: eq
  arguments: Application
    arguments: Application
      operator: Fibonacci
    arguments: one
    operator: eq
  arguments: Application
    operator: eq
  operator: and
type: ApplicationSymbol

Stirling1
commented property: Stirling1(n,m) = the sum k=0 to n-m of (-1)^k * binomial(n-1+k, n-m+k) * binomial(2n-m,n-m-k) * Stirling2(n,m)
description: The Stirling numbers of the first kind. (-1)^(n-m)*Stirling1(n,m) is the number of permutations of n symbols which have exactly m cycles. Note that there are a few slightly different definitions of these numbers.
example: Application
  arguments: Application
    arguments: Application
      operator: Stirling1
    arguments: Literal
      value: -9450
    operator: eq
  operator: Example
formal property: Application
  arguments: Application
    arguments: Variable
      name: n
    arguments: Variable
      name: m
    operator: Stirling1
  arguments: Application
    arguments: Application
      operator: integer interval
    operator: sum
  operator: eq
type: ApplicationSymbol

Stirling2
commented property: Stirling2(n,m) = 1/m! * the sum from k=0 to m of (-1)^(m-k) * binomial(m,k) * k^n
description: The Stirling numbers of the second kind. Stirling2(n, m) is the number of partitions of a set with n elements into m non empty subsets. Note that there are a few slightly different definitions of these numbers.
example: Application
  arguments: Application
    arguments: Application
      operator: Stirling2
    arguments: Literal
      value: 301
    operator: eq
  operator: Example
formal property: Application
  arguments: Application
    arguments: Variable
      name: n
    arguments: Variable
      name: m
    operator: Stirling2
  arguments: Application
    arguments: Application
      operator: divide
    operator: times
  operator: eq
type: ApplicationSymbol

binomial
commented property: binomial(n,m) = n!/(m!*(n-m)!)
description: The binomial coefficients. binomial(n, m) is the number of ways of choosing m objects from a collection of n distinct objects without regard to the order.
example: Application
  arguments: Application
    arguments: Application
      operator: binomial
    arguments: Literal
      value: 6
    operator: eq
  operator: Example
formal property: Application
  arguments: Application
    arguments: Variable
      name: n
    arguments: Variable
      name: m
    operator: binomial
  arguments: Application
    arguments: Application
      operator: factorial
    operator: divide
  operator: eq
type: ApplicationSymbol

multinomial
commented property: multinomial(n, n1, ... nk) is equal to n!/(n1!*n2! ...*nk!) where n=n1+...+nk
description: The multinomial coefficient, multinomial(n, n1, ... nk) is the number of ways of choosing ni objects of type i (i from 1 to k) without regard to order, in such a way that the total number of objects chosen is n. multinomial(n, n1, ... nk) is equal to n!/(n1!*n2! ...*nk!).
example: Application
  arguments: Application
    arguments: Application
      operator: multinomial
    arguments: Literal
      value: 560
    operator: eq
  operator: Example
formal property: Application
  arguments: Application
    arguments: Application
      arguments: multinomial
      operator: apply to list
    arguments: Application
      operator: divide
    operator: eq
  arguments: Application
    arguments: Application
      operator: vector selector
    operator: eq
  arguments: Application
    operator: eq
  operator: and
type: ApplicationSymbol

complex1
description: This CD is intended to be `compatible' with the MathML view of operations on and constructors for complex numbers.
type: Library
comment: This document is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. The copyright holder grants you permission to redistribute this document freely as a verbatim copy. Furthermore, the copyright holder permits you to develop any derived work from this document provided that the following conditions are met. a) The derived work acknowledges the fact that it is derived from this document, and maintains a prominent reference in the work to the original source. b) The fact that the derived work is not the original OpenMath document is stated prominently in the derived work. Moreover if both this document and the derived work are Content Dictionaries then the derived work must include a different CDName element, chosen so that it cannot be confused with any works adopted by the OpenMath Society. In particular, if there is a Content Dictionary Group whose name is, for example, `math' containing Content Dictionaries named `math1', `math2' etc., then you should not name a derived Content Dictionary `mathN' where N is an integer. However you are free to name it `private_mathN' or some such. This is because the names `mathN' may be used by the OpenMath Society for future extensions. c) The derived work is distributed under terms that allow the compilation of derived works, but keep paragraphs a) and b) intact. The simplest way to do this is to distribute the derived work under the OpenMath license, but this is not a requirement. If you have questions about this license please contact the OpenMath society at http://www.openmath.org.

argument
commented property: for all r,a | argument(complex_polar(r,a)=a)
commented property: the argument of x+i*y = arctan(y,x) (two-argument arctan from transc2)
commented property: the argument of x+i*y = arctan(y/x) (if x is positive)
description: This symbol represents the unary function which returns the argument of a complex number, viz. the angle which a straight line drawn from the number to zero makes with the Real line (measured anti-clockwise). The argument to the symbol is the complex number whos argument is being taken.
formal property: Binding
  binder: forall
  body: Application
    arguments: Application
      arguments: Application
        operator: complex polar
      operator: argument
    arguments: Variable
      name: a
    operator: eq
  variables: Variable
    name: r
  variables: Variable
    name: a
formal property: Application
  arguments: Application
    arguments: Variable
      name: x
    arguments: zero
    operator: gt
  arguments: Application
    arguments: Application
      operator: argument
    operator: eq
  operator: implies
formal property: Application
  arguments: Application
    arguments: Application
      operator: complex cartesian
    operator: argument
  arguments: Application
    arguments: Variable
      name: y
    operator: arctan
  operator: eq
type: ApplicationSymbol

complex cartesian
commented property: for all x,y | complex_cartesian(x,y) = x + iy
description: This symbol represents a constructor function for complex numbers specified as the Cartesian coordinates of the relevant point on the complex plane. It takes two arguments, the first is a number x to denote the real part and the second a number y to denote the imaginary part of the complex number x + i y. (Where i is the square root of -1.)
formal property: Binding
  binder: forall
  body: Application
    arguments: Application
      arguments: Variable
        name: x
      operator: complex cartesian
    arguments: Application
      operator: plus
    operator: eq
  variables: Variable
    name: x
  variables: Variable
    name: y
type: ApplicationSymbol

complex polar
commented property: for all r,a | complex_polar(r,a) = r*e^(a*i)
commented property: for all x | if a is a real number and k is an integer then complex_polar(x,a) = complex_polar(x,a+2*pi*k)
commented property: for all x,y,r,a | (r sin a = y and r cos a = x) implies (complex_polar(r,a) = complex_cartesian(x,y)
description: This symbol represents a constructor function for complex numbers specified as the polar coordinates of the relevant point on the complex plane. It takes two arguments, the first is a nonnegative number r to denote the magnitude and the second a number theta (given in radians) to denote the argument of the complex number r e^(i theta). (i and e are defined as in this CD).
example: Application
  arguments: Literal
    value: i = complex_polar(1,pi/2)
  arguments: Application
    arguments: http://www.openmath.org/cd/nums1#i
    operator: eq
  operator: Example
formal property: Binding
  binder: forall
  body: Application
    arguments: Application
      arguments: Variable
        name: r
      operator: complex polar
    arguments: Application
      operator: times
    operator: eq
  variables: Variable
    name: r
  variables: Variable
    name: a
formal property: Binding
  binder: forall
  body: Application
    arguments: Application
      arguments: Application
        operator: eq
      operator: and
    arguments: Application
      operator: eq
    operator: implies
  variables: Variable
    name: x
  variables: Variable
    name: y
  variables: Variable
    name: r
  variables: Variable
    name: a
formal property: Binding
  binder: forall
  body: Application
    arguments: Application
      arguments: Application
        operator: in
      operator: and
    arguments: Application
      operator: eq
    operator: implies
  variables: Variable
    name: x
type: ApplicationSymbol

conjugate
commented property: if a is a complex number then (conjugate(a) + a) is a real number
description: A unary operator representing the complex conjugate of its argument.
formal property: Application
  arguments: Application
    arguments: Variable
      name: a
    arguments: http://www.openmath.org/cd/setname1#C
    operator: in
  arguments: Application
    arguments: Application
      operator: plus
    arguments: http://www.openmath.org/cd/setname1#R
    operator: in
  operator: implies
type: ApplicationSymbol

imaginary
commented property: for all x,y | y = imaginary(x+iy)
description: This represents the imaginary part of a complex number
formal property: Binding
  binder: forall
  body: Application
    arguments: Variable
      name: y
    arguments: Application
      operator: imaginary
    operator: eq
  variables: Variable
    name: x
  variables: Variable
    name: y
type: ApplicationSymbol

real
commented property: for all x,y | x = real(x+iy)
description: This represents the real part of a complex number
formal property: Binding
  binder: forall
  body: Application
    arguments: Variable
      name: x
    arguments: Application
      operator: real
    operator: eq
  variables: Variable
    name: x
  variables: Variable
    name: y
type: ApplicationSymbol

dimensions1
description: This CD defines symbols which represent basic physical dimensions.
type: Library
comment: This document is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. The copyright holder grants you permission to redistribute this document freely as a verbatim copy. Furthermore, the copyright holder permits you to develop any derived work from this document provided that the following conditions are met. a) The derived work acknowledges the fact that it is derived from this document, and maintains a prominent reference in the work to the original source. b) The fact that the derived work is not the original OpenMath document is stated prominently in the derived work. Moreover if both this document and the derived work are Content Dictionaries then the derived work must include a different CDName element, chosen so that it cannot be confused with any works adopted by the OpenMath Society. In particular, if there is a Content Dictionary Group whose name is, for example, `math' containing Content Dictionaries named `math1', `math2' etc., then you should not name a derived Content Dictionary `mathN' where N is an integer. However you are free to name it `private_mathN' or some such. This is because the names `mathN' may be used by the OpenMath Society for future extensions. c) The derived work is distributed under terms that allow the compilation of derived works, but keep paragraphs a) and b) intact. The simplest way to do this is to distribute the derived work under the OpenMath license, but this is not a requirement. If you have questions about this license please contact the OpenMath society at http://www.openmath.org.

acceleration
commented property: acceleration = length/(time^2)
description: This symbol represents the acceleration physical dimension. It is the second derivative of distance with respect to time.
formal property: Application
  arguments: acceleration
  arguments: Application
    arguments: length
    operator: divide
  operator: eq
type: Symbol

area
commented property: area = length*length
description: This symbol represents the area physical dimension.
formal property: Application
  arguments: area
  arguments: Application
    arguments: length
    operator: times
  operator: eq
type: Symbol

charge
commented property: charge = current/voltage
description: This symbol represents the charge physical dimension.
type: Symbol

concentration
commented property: concentration = mass/length^3
description: This symbol represents the concentration physical dimension, it is the amount of a substance in a volume.
type: Symbol

current
commented property: current = voltage*charge
description: This symbol represents the current physical dimension.
type: Symbol

density
commented property: density = mass/volume
description: This symbol represents the density physical dimension, it is the mass per unit volume.
formal property: Application
  arguments: density
  arguments: Application
    arguments: mass
    arguments: volume
    operator: divide
  operator: eq
type: Symbol

displacement
description: This symbol represents the spatial difference between two points. The direction of the displacement is taken into account as well as the distance between the points.
type: ConstantSymbol

energy
commented property: energy = force*length
commented property: energy = mass*length^2/time^2
description: This symbol represents the energy physical dimension.
formal property: Application
  arguments: energy
  arguments: Application
    arguments: force
    arguments: length
    operator: times
  operator: eq
type: Symbol

force
commented property: force = mass*length/time^2
description: This symbol represents the force physical dimension.
formal property: Application
  arguments: force
  arguments: Application
    arguments: mass
    arguments: acceleration
    operator: times
  operator: eq
type: Symbol

length
description: This symbol represents the length physical dimension.
type: Symbol

mass
description: This symbol represents the mass physical dimension.
type: Symbol

momentum
commented property: momentum = mass*velocity
description: This symbol represents the momentum physical dimension, it is mass times velocity.
formal property: Application
  arguments: momentun
  arguments: Application
    arguments: mass
    arguments: velocity
    operator: times
  operator: eq
type: Symbol

power
commented property: power = energy/time
description: This symbol represents the power physical dimension, it is energy per time.
formal property: Application
  arguments: power
  arguments: Application
    arguments: energy
    arguments: time
    operator: divide
  operator: eq
type: Symbol

pressure
commented property: pressure = force/area
description: This symbol represents the pressure physical dimension.
formal property: Application
  arguments: pressure
  arguments: Application
    arguments: force
    arguments: area
    operator: divide
  operator: eq
type: Symbol

resistance
commented property: resistance = voltage/current
description: This symbol represents the resistance physical dimension, it is the resistance that an electrical circuit has to flow of charge.
type: Symbol

speed
commented property: speed = length/time
description: This symbol represents the speed physical dimension. It is the size of the derivative of distance with respect to time.
formal property: Application
  arguments: speed
  arguments: Application
    arguments: length
    arguments: time
    operator: divide
  operator: eq
type: Symbol

temperature
description: This symbol represents the temperature physical dimension.
type: Symbol

time
description: This symbol represents the time physical dimension. Note that the main units for time are defined in the units_time1 CD.
type: Symbol

velocity
commented property: speed is the Euclidean norm of velocity
commented property: velocity = displacement/second
description: This symbol represents the velocity physical dimension. It is the derivative of (vector) distance with respect to time.
formal property: Application
  arguments: speed
  arguments: Application
    arguments: velocity
    operator: Euclidean norm
  operator: eq
type: Symbol

voltage
commented property: voltage = current/charge
description: This symbol represents the voltage physical dimension.
type: Symbol

volume
commented property: volume = length*length*length
description: This symbol represents the volume physical dimension.
formal property: Application
  arguments: volume
  arguments: Application
    arguments: length
    operator: times
  operator: eq
type: Symbol

directives1
description: The primal objective of OpenMath objects is to represent mathematical expressions. In this Content Dictionary another objective is addressed, namely to express an action related to a mathematical expression. Such a request for an action is generally referred to as a query. The specific queries are called directives. In this CD we define some. An entity (software) carrying out the query is referred to as a service. The service might return an OpenMath object. To formalize this object, we also introduce the symbol response in this CD. amc 2004-03-18: added the directive explore. amc 2004-03-24: removed redundancies.
type: Library

decide
commented property: The response to the decide query is logically equivalent to the truth of the argument.
description: This symbol is a function with one argument, which should be a clause. When applied to a clause, it asks whether the clause holds.
example: Application
  arguments: Literal
    value: The question if sin(Pi) is equal to zero can be phrased as follows.
  arguments: Application
    arguments: Application
      operator: eq
    operator: decide
  operator: Example
formal property: Application
  arguments: Application
    arguments: Application
      operator: decide
    operator: response
  arguments: Variable
    name: P
  operator: equivalent
type: Symbol

disprove
commented property: Asking to disprove C amounts to asking for a proof that C does not hold. (In other words, this symbol is completely redundant, even in multi-valued logic.***)
description: This symbol is a function with one argument, which should be a clause. When applied to a clause C, it asks for a proof of that C does not hold.
formal property: Application
  arguments: Application
    arguments: Variable
      name: C
    operator: disprove
  arguments: Application
    arguments: Application
      operator: not
    operator: prove
  operator: eq
type: Symbol

evaluate
description: This symbol is a function with one argument, which should be a mathematical expression. When applied to a mathematical expression, it asks for an evaluation or simplification of the expression. The evaluation or simplification to be carried out by a service is a simpler mathematical expression (in some definition of complexity of objects) which is equal to the argument.
example: Application
  arguments: Literal
    value: The value of sin(Pi) is zero. The expression below asks for sin(Pi) to be evaluated, and so a service receiving the object is supposed to return zero.
  arguments: Application
    arguments: Application
      operator: sin
    operator: evaluate
  operator: Example
type: Symbol

evaluate to type
commented property: The type of the responded object should be equal to the specification, that is the second argument of the evaluate_to_type.
description: This symbol is a function with two arguments, which should be a mathematical expression and a type. When applied to a mathematical expression E and a type T, it asks for an evaluation or simplification of E to a mathematical expression of type T.
example: Application
  arguments: Literal
    value: The value of (7*6)/2 is a natural number. The expression below asks for this integer.
  arguments: Application
    arguments: Application
      operator: divide
    arguments: http://www.openmath.org/cd/setname1#N
    operator: evaluate
  operator: Example
formal property: Attribution
  arguments: AttributionPair
    attribute key: type
    attribute value: Variable
      name: T
  target: Application
    arguments: Application
      arguments: Variable
        name: x
      operator: evaluate to type
    operator: response
type: Symbol

explore
commented property: A response R should satisfy the requirement that R implies the assertion.
description: This symbol is a unary function whose argument should be a mathematical assertion. When applied to an assertion A, it asks for conditions under which the assertion holds.
example: Application
  arguments: Literal
    value: Given the Pappos configuration P, the Pappos thesis T asserts that three points of the configuration are collinear. A conceivable answer to the explore directive with the assertion that in configuration P the thesis T holds, is a nondegeneracy condition that makes the assertion valid.
  operator: Example
formal property: Application
  arguments: Application
    arguments: Application
      operator: explore
    operator: response
  arguments: Variable
    name: A
  operator: implies
type: Symbol

find
commented property: The body of argument with the binder x replaced by the response should be a true statement.
description: This symbol is a binder, whose body should be a clause. When bound to a variable (or list of variables) x with body P(x), it asks for a mathematical expression A such that P(A) holds.
example: Application
  arguments: Literal
    value: Searching for a real number x such that sin(x) = 0
  arguments: Binding
    binder: find
    body: Application
      operator: and
    variables: Variable
      name: x
  arguments: Literal
    value: is to be compared to asking for an inverse of x:
  arguments: Application
    operator: evaluate to type
  operator: Example
formal property: Application
  arguments: Application
    arguments: Binding
      binder: find
      body: Variable
        name: P
    operator: response
  operator: Variable
    name: P
type: Symbol

look up
description: This symbol is a function with one argument, which should be a mathematical expression. When applied to a mathematical expression, it asks for mathematical expressions related to the argument. If the argument is a single OpenMath symbol, the service might respond by the list of all properties in the CD containing the argument. Alternatively, the service can provide a list of CDs which use the CD in which the argument occurs. Another service might return all documents in which the symbol occurs. If the argument is a more complicated object, the same services could be called for, but then with all OpenMath symbols occurring in the argument instead of the single one.
example: Application
  arguments: Literal
    value: Looking up sin is expressed as follows:
  arguments: Application
    arguments: sin
    operator: look up
  operator: Example
type: Symbol

prove
description: This symbol is a function with one argument, which should be a clause. When applied to a clause C, it asks for a proof of C.
type: Symbol

prove in theory
description: This symbol is a function with two arguments, the first of which should be a clause and the second of which should be a symbol indicating a logic theory. When applied to arguments C, T, it asks for a proof of C in theory T.
type: Symbol

response
description: This symbol is a function of one argument, which should be a query. When applied to a query, it refers to the response a service might give. It will mainly be used in this CD to express formal mathematical properties of queries.
type: Symbol

ecc
description: Extended Calculus of Constructions Primitives Initial version: O. Caprotti (July 1, 1999) Revised: O. Caprotti (September 8, 1999)
type: Library
comment: This document is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. The copyright holder grants you permission to redistribute this document freely as a verbatim copy. Furthermore, the copyright holder permits you to develop any derived work from this document provided that the following conditions are met. a) The derived work acknowledges the fact that it is derived from this document, and maintains a prominent reference in the work to the original source. b) The fact that the derived work is not the original OpenMath document is stated prominently in the derived work. Moreover if both this document and the derived work are Content Dictionaries then the derived work must include a different CDName element, chosen so that it cannot be confused with any works adopted by the OpenMath Society. In particular, if there is a Content Dictionary Group whose name is, for example, `math' containing Content Dictionaries named `math1', `math2' etc., then you should not name a derived Content Dictionary `mathN' where N is an integer. However you are free to name it `private_mathN' or some such. This is because the names `mathN' may be used by the OpenMath Society for future extensions. c) The derived work is distributed under terms that allow the compilation of derived works, but keep paragraphs a) and b) intact. The simplest way to do this is to distribute the derived work under the OpenMath license, but this is not a requirement. If you have questions about this license please contact the OpenMath society at http://www.openmath.org.

Pair
description: The pairing constructor. It takes two OpenMath objects as first element and second element of the pair, and a third optional OpenMath object that represents the type of the pair.
example: Application
  arguments: Application
    arguments: Literal
      value: 0
    arguments: Literal
      value: 1
    operator: Pair
  operator: Example
type: ApplicationSymbol

PairProj1
description: The first projection function that extracts the first component of a Pair. It satisfies the sigma-reduction rule.
example: Application
  arguments: Application
    arguments: Application
      operator: PairProj1
    arguments: Literal
      value: 0
    operator: eq
  operator: Example
type: ApplicationSymbol

PairProj2
description: The second projection function that extracts the second component of a Pair. It satisfies sigma-reduction rule.
example: Application
  arguments: Application
    arguments: Application
      operator: PairProj2
    arguments: Literal
      value: 1
    operator: eq
  operator: Example
type: ApplicationSymbol

SigmaType
description: The binder symbol used to construct the type of Cartesian products. The (either plain or attributed) variables might occur in the body \OM\ object.
type: BinderSymbol

Tuple
description: The n-ary tupling constructor when n>2. The arguments are the element of the tuple. Tuple objects can also be constructed by successive nesting of Pair.
example: Application
  arguments: Application
    arguments: Application
      operator: Pair
    arguments: Application
      operator: Tuple
    operator: eq
  operator: Example
type: ApplicationSymbol

type
description: Attribution tag to denote type-judgement
type: Symbol
type: SemanticAttributionSymbol

typecoerce
description: Attribution tag to denote type-judgement with coercion
type: SemanticAttributionSymbol

equations1
description: Symbols to provide a vocabulary for talking about properties of (systems of) equations.
type: Library
comment: This document is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. The copyright holder grants you permission to redistribute this document freely as a verbatim copy. Furthermore, the copyright holder permits you to develop any derived work from this document provided that the following conditions are met. a) The derived work acknowledges the fact that it is derived from this document, and maintains a prominent reference in the work to the original source. b) The fact that the derived work is not the original OpenMath document is stated prominently in the derived work. Moreover if both this document and the derived work are Content Dictionaries then the derived work must include a different CDName element, chosen so that it cannot be confused with any works adopted by the OpenMath Society. In particular, if there is a Content Dictionary Group whose name is, for example, `math' containing Content Dictionaries named `math1', `math2' etc., then you should not name a derived Content Dictionary `mathN' where N is an integer. However you are free to name it `private_mathN' or some such. This is because the names `mathN' may be used by the OpenMath Society for future extensions. c) The derived work is distributed under terms that allow the compilation of derived works, but keep paragraphs a) and b) intact. The simplest way to do this is to distribute the derived work under the OpenMath license, but this is not a requirement. If you have questions about this license please contact the OpenMath society at http://www.openmath.org.

dense
description: A predicate to indicate that an equation or system of equations is dense.
example: Application
  arguments: Application
    arguments: Variable
      name: eqns
    operator: dense
  operator: Example
type: Symbol

linear
description: A predicate to indicate that an equation or system of equations is linear, i.e. is expressed in terms of constants and first order terms.
example: Application
  arguments: Application
    arguments: Application
      operator: plus
    operator: linear
  operator: Example
type: Symbol

non linear
description: A predicate to indicate that an equation or system of equations is non-linear, i.e. contains terms of order greater than 1.
example: Application
  arguments: Application
    arguments: Application
      operator: power
    operator: non linear
  operator: Example
type: Symbol

sparse
description: A predicate to indicate that an equation or system of equations is sparse.
example: Application
  arguments: Application
    arguments: Variable
      name: eqns
    operator: sparse
  operator: Example
type: Symbol

error
type: Library
comment: This document is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. The copyright holder grants you permission to redistribute this document freely as a verbatim copy. Furthermore, the copyright holder permits you to develop any derived work from this document provided that the following conditions are met. a) The derived work acknowledges the fact that it is derived from this document, and maintains a prominent reference in the work to the original source. b) The fact that the derived work is not the original OpenMath document is stated prominently in the derived work. Moreover if both this document and the derived work are Content Dictionaries then the derived work must include a different CDName element, chosen so that it cannot be confused with any works adopted by the OpenMath Society. In particular, if there is a Content Dictionary Group whose name is, for example, `math' containing Content Dictionaries named `math1', `math2' etc., then you should not name a derived Content Dictionary `mathN' where N is an integer. However you are free to name it `private_mathN' or some such. This is because the names `mathN' may be used by the OpenMath Society for future extensions. c) The derived work is distributed under terms that allow the compilation of derived works, but keep paragraphs a) and b) intact. The simplest way to do this is to distribute the derived work under the OpenMath license, but this is not a requirement. If you have questions about this license please contact the OpenMath society at http://www.openmath.org.

unexpected symbol
description: This symbol represents the error which is raised when an application reads a symbol which is not present in the mentioned content dictionary. When receiving such a symbol, the application should act as if it had received the OpenMath error object constructed from unexpected_symbol and the unexpected symbol as in the example below.
example: Application
  arguments: Literal
    value: The application received a mistyped symbol
  arguments: Error
    arguments: plurse
    symbol: unexpected symbol
  operator: Example
type: ErrorSymbol

unhandled symbol
description: This symbol represents the error which is raised when an application reads a symbol which is present in the mentioned content dictionary, but which it has not implemented. When receiving such a symbol, the application should act as if it had received the OpenMath error object constructed from unhandled_symbol and the unhandled symbol as in the example below.
example: Application
  arguments: Literal
    value: The application does not implement the Complex numbers:
  arguments: Error
    arguments: http://www.openmath.org/cd/setname1#C
    symbol: unhandled symbol
  operator: Example
type: ErrorSymbol

unsupported CD
description: This symbol represents the error which is raised when an application reads a symbol where the mentioned content dictionary is not present. When receiving such a symbol, the application should act as if it had received the OpenMath error object constructed from unsupported_CD and the symbol from the unsupported Content Dictionary as in the example below.
example: Application
  arguments: Literal
    value: The application does not know about the CD specfun1
  arguments: Error
    arguments: BesselJ
    symbol: unsupported CD
  operator: Example
type: ErrorSymbol

expint
description: This content dictionary contains symbols to describe the Exponential integral and associated functions.
type: Library
comment: This document is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. The copyright holder grants you permission to redistribute this document freely as a verbatim copy. Furthermore, the copyright holder permits you to develop any derived work from this document provided that the following conditions are met. a) The derived work acknowledges the fact that it is derived from this document, and maintains a prominent reference in the work to the original source. b) The fact that the derived work is not the original OpenMath document is stated prominently in the derived work. Moreover if both this document and the derived work are Content Dictionaries then the derived work must include a different CDName element, chosen so that it cannot be confused with any works adopted by the OpenMath Society. In particular, if there is a Content Dictionary Group whose name is, for example, `math' containing Content Dictionaries named `math1', `math2' etc., then you should not name a derived Content Dictionary `mathN' where N is an integer. However you are free to name it `private_mathN' or some such. This is because the names `mathN' may be used by the OpenMath Society for future extensions. c) The derived work is distributed under terms that allow the compilation of derived works, but keep paragraphs a) and b) intact. The simplest way to do this is to distribute the derived work under the OpenMath license, but this is not a requirement. If you have questions about this license please contact the OpenMath society at http://www.openmath.org.

http://www.openmath.org/cd/expint#E
description: The symbol E defines the generalised exponential integral as in Abramovitz & Stegun equation 5.1.4. This is an ordinary integral: $$E_n(z)=\int_1^{-\infty}\frac{e^{-zt}}{t^n} dt\qquad(\Re z>0)$$ which is then extended by analytic continuation (this latter is not currently represented in the FMPs) to the complex plane slit along the negative real axis. Note that OpenMath's definition is curried, i.e. E(n) is a function.
formal property: Application
  arguments: Application
    arguments: Application
      operator: real
    arguments: zero
    operator: gt
  arguments: Application
    arguments: Application
    operator: eq
  operator: implies
type: Symbol

Ei
description: The symbol Ei defines the basic exponential integral as in Abramovitz & Stegun equation 5.1.2. This is a Cauchy principal value integral: $$Ei(x)=\int_{-\infty}^x\frac{e^t}t dt\qquad(x>0)$$ which is then extended by analytic continuation (this latter is not currently represented in the FMPs) to the complex plane slit along the negative real axis
formal property: Application
  arguments: Application
    arguments: Variable
      name: x
    arguments: zero
    operator: gt
  arguments: Application
    arguments: Application
      operator: Ei
    operator: eq
  operator: implies
type: Symbol

li
description: The symbol li defines the basic logarithmic integral as in Abramovitz & Stegun equation 5.1.2. This is a Cauchy principal value integral: $$li(x)=\int_0^x\frac1{\ln t}t dt\qquad(x>1)$$ which is then extended by analytic continuation (this latter is not currently represented in the FMPs) to the complex plane slit along the negative real axis
formal property: Application
  arguments: Application
    arguments: Variable
      name: x
    arguments: one
    operator: gt
  arguments: Application
    arguments: Application
      operator: li
    operator: eq
  operator: implies
type: Symbol

field1
description: A CD of basic functions for field theory
type: Library
comment: Written by Arjeh M. Cohen 2004-02-26

addition
description: This symbols represents a unary function, whose argument should be a field. It returns the addition map on the field. We allow for the map to be n-ary.
example: Application
  arguments: Literal
    value: The identity field(R,+,0,-,*,1,inv) is +.
  arguments: Application
    arguments: Application
      operator: identity
    operator: eq
  operator: Example
type: Symbol

additive group
description: This symbol is a unary function, whose argument should be a field S. When applied to S its value is the monoid underlying S.
example: Application
  arguments: Application
    arguments: Application
      operator: additive group
    arguments: Application
      operator: group
    operator: eq
  operator: Example
type: Symbol

carrier
description: This symbol represents a unary function, whose argument should be a field S (for instance constructed by field). When applied to S, its value should be the set of elements of S.
example: Application
  arguments: Literal
    value: The carrier of field(R,+,0,-,*,1,inv) is R.
  arguments: Application
    arguments: Application
      operator: carrier
    operator: eq
  operator: Example
type: Symbol

expression
description: This symbol is a function with two arguments. Its first argument should be a field. The second should be an arithmetic expression A, whose operators are times, plus, minus, unary_minus, and power, and whose leaves are members of the carrier of G. When applied to G and A, it denotes the element (of G) that is the element obtained from the leaves of A by applying the operations of G instead of those from the CD arith1 according to A. Here multiplication, addition, subtraction, minus, and power take over the roles of times, plus, minus, unary_minus, and power, respectively. Also, an integer m occurring in A will be interpreted as a member of G by interpreting it as the sum of m copies of the identity element, the symbol alg1.one will be interpreted as the identity, and the symbol alg1.zero will be interpreted as the zero of G.
example: Application
  arguments: Application
    arguments: Application
      operator: expression
    arguments: Literal
      value: 18
    operator: eq
  operator: Example
type: Symbol

field
description: This symbol is a constructor for fields. It takes seven arguments R, a, o, n, m, e, i: which are, respectively, a set R to specify the elements in the field, a binary operation a on R, an element o of R, and a unary operation n on R such that [R,a,o,n] is a commutative group, a binary operation m on R, an element e of R, and a map from R - {o} to itself such that [R,m,e] is a monoid and such that [R - {o},m',e,i] is a group, where m' is the restriction of m to R -{o}.
example: Application
  arguments: Literal
    value: This example represents the field of rational numbers. The field addition is binary addition, the field multiplication is binary multiplication.
  arguments: Application
    arguments: http://www.openmath.org/cd/setname1#Q
    arguments: plus
    operator: field
  operator: Example
type: Symbol

identity
description: This symbols represents a unary function, whose argument should be a field. It returns the identity element of the field.
example: Application
  arguments: Literal
    value: The identity field(R,+,0,-,*,1,inv) is 1.
  arguments: Application
    arguments: Application
      operator: identity
    operator: eq
  operator: Example
type: Symbol

inverse
description: This symbol represents a unary function, whose argument should be a field S. It returns the map sending a nonzero element of S to its multiplicative inverse.
example: Application
  arguments: Literal
    value: The inverse of field(R,+,0,-,*,1,inv) is inv.
  arguments: Application
    arguments: Application
      operator: inverse
    operator: eq
  operator: Example
type: Symbol

is commutative
commented property: If is_commutative(G) then for all a,b in carrier(G) a*b = b*a
description: The unary boolean function whose value is true iff the argument is a commutative field.
formal property: Application
  arguments: Application
    arguments: Variable
      name: G
    operator: is commutative
  arguments: Binding
    binder: forall
    body: Application
      operator: implies
    variables: Variable
      name: a
  operator: implies
type: Symbol

is subfield
commented property: If is_subfield(G,H) then H is a nonempty set of elements of the carrier of G and H is closed under multiplication and taking inverses.
description: The binary boolean function whose value is true iff the second argument is a subfield of the second.
type: Symbol

minus
description: This symbol represents a unary function, whose argument should be a field S. It returns the map sending an element of S to its additive inverse.
example: Application
  arguments: Literal
    value: The minus of field(R,+,0,-,*,1,inv) is -.
  arguments: Application
    arguments: Application
      operator: minus
    operator: eq
  operator: Example
type: Symbol

multiplication
description: This symbol represents a unary function, whose argument should be a field S. It returns the multiplication map on the field. We allow for the map to be n-ary.
example: Application
  arguments: Literal
    value: The multiplication of field(R,+,0,-,*,1,inv) is *.
  arguments: Application
    arguments: Application
      operator: multiplication
    operator: eq
  operator: Example
type: Symbol

multiplicative group
description: This symbol is a unary function, whose argument should be a field S. When applied to S its value is the multiplicative group on the nonzero elements of S.
example: Application
  arguments: Application
    arguments: Application
      operator: multiplicative group
    arguments: Application
      operator: group
    operator: eq
  operator: Example
type: Symbol

power
description: This is a symbol with two or three arguments. Its first argument should be an element g of a field and the second argument should be an integer. The optional third argument is the field G containing g. It denotes the element g^k in G.
example: Application
  arguments: Application
    arguments: Application
      operator: power
    arguments: Literal
      value: 9
    operator: eq
  operator: Example
type: Symbol

subfield
description: This symbol is a constructor symbol with one or two arguments. The first argument is a list or set, D, of field elements. The optional second argument is the field G containing D. It denotes the subfield of G generated by D.
example: Application
  arguments: Application
    arguments: Variable
      name: D
    arguments: Variable
      name: G
    operator: subfield
  operator: Example
example: Application
  arguments: Literal
    value: This example represents the subfield of the multiplicative field of the nonzero reals generated by the constants Pi and E:
  arguments: Application
    arguments: Application
      operator: list
    operator: subfield
  operator: Example
type: Symbol

subtraction
description: This symbols represents a unary function, whose argument should be a field. It returns the binary operation of subtraction on the field.
example: Application
  arguments: Literal
    value: The subtraction of field(R,+,0,-,*,1,inv) is the map sending the pair (r,s) of elements of R to r-s.
  arguments: Application
    arguments: Application
      operator: subtraction
    operator: eq
  operator: Example
type: Symbol

zero
description: This symbols represents a unary function, whose argument should be a field. It returns the zero element of the field.
example: Application
  arguments: Literal
    value: The identity field(R,+,0,-,*,1,inv) is 0.
  arguments: Application
    arguments: Application
      operator: zero
    operator: eq
  operator: Example
type: Symbol

field2
description: Basic functions for homomorphisms in field theory
type: Library
comment: Initiated by Arjeh M. Cohen 2004-03-05

conjugation
commented property: conjugation(M,x) (y) = x * y * x^ {-1}.
description: This symbol is a function with two arguments, which should be a field M and a nonzero element x of M. When applied to M and x, it denotes conjugation on M by x.
formal property: Binding
  binder: forall
  body: Application
    arguments: Application
      arguments: Variable
        name: y
      operator: Application
        operator: conjugation
    arguments: Application
      operator: expression
    operator: eq
  variables: Variable
    name: M
  variables: Variable
    name: x
  variables: Variable
    name: y
type: Symbol

is automorphism
commented property: If is_automorphism(M,f) then is_isomorphism(M,M,f)
description: This symbol is a boolean function with two arguments. The first is a field M, the second is a map f from the element set of M to the element set of M. When applied to M and f, it denotes a field automorphism f of M.
example: Application
  arguments: Application
    arguments: Variable
      name: M
    arguments: Variable
      name: f
    operator: is automorphism
  operator: Example
formal property: Application
  arguments: Application
    arguments: Variable
      name: M
    arguments: Variable
      name: f
    operator: is automorphism
  arguments: Application
    arguments: Variable
      name: M
    operator: is isomorphism
  operator: implies
type: Symbol

is endomorphism
commented property: If is_endomorphism(M,f) then is_homomorphism(M,M,f)
description: This symbol is a boolean function with two arguments. The first argument is a field M, the second is a map f from the element set of M to the element set of M. When applied to M and f, it denotes that f is a field endomorphism from M to M.
example: Application
  arguments: Application
    arguments: Variable
      name: M
    arguments: Variable
      name: f
    operator: is endomorphism
  operator: Example
formal property: Application
  arguments: Application
    arguments: Variable
      name: M
    arguments: Variable
      name: f
    operator: is endomorphism
  arguments: Application
    arguments: Variable
      name: M
    operator: is homomorphism
  operator: implies
type: Symbol

is homomorphism
commented property: If is_homomorphism(M,N,f) then, for each pair of elements x, y of M, we have f(x * y) = f(x) * f(y).
description: This symbol is a boolean function with three arguments. The first and arguments are fields M, N, the third is a map f from the element set of M to the element set of N. When applied to M, N, and f, it denotes that f is a field homomorphism from M to N.
example: Application
  arguments: Application
    arguments: Variable
      name: M
    arguments: Variable
      name: N
    operator: is homomorphism
  operator: Example
formal property: Application
  arguments: Application
    arguments: Variable
      name: M
    arguments: Variable
      name: N
    operator: is homomorphism
  arguments: Binding
    binder: forall
    body: Application
      operator: implies
    variables: Variable
      name: x
  operator: implies
type: Symbol

is isomorphism
description: This symbol is a boolean function with three arguments. The first and arguments are fields M, N, the third is a map f from the element set of M to the element set of N. When applied to M, N, and f, it denotes that f is a field isomorphism from M to N. This means that f is a homomorphism from M to N, that f is bijective, and that its inverse is a homomorphism from N to M.
example: Application
  arguments: Application
    arguments: Variable
      name: M
    arguments: Variable
      name: N
    operator: is isomorphism
  operator: Example
type: Symbol

isomorphic
description: This symbol is a Boolean function with n arguments, n at least 2, which are fields. When applied to M_1, ..., M_n, it denotes the fact that there is an isomorphism from each M_i to each M_j.
example: Application
  arguments: Application
    arguments: Variable
      name: M
    arguments: Variable
      name: N
    operator: isomorphic
  operator: Example
type: Symbol

left multiplication
commented property: left_multiplication(M,x) (y) = x * y.
description: This symbol is a function with two arguments, which should be a field M and an element x of M. When applied to M and x, it denotes left multiplication on M by x.
formal property: Binding
  binder: forall
  body: Application
    arguments: Application
      arguments: Variable
        name: y
      operator: Application
        operator: left multiplication
    arguments: Application
      operator: multiplication
    operator: eq
  variables: Variable
    name: M
  variables: Variable
    name: x
  variables: Variable
    name: y
type: Symbol

right multiplication
commented property: right_multiplication(M,x) (y) = y * x.
description: This symbol is a function with two arguments, which should be a field M and an element x of M. When applied to M and x, it denotes right multiplication on M by x.
formal property: Binding
  binder: forall
  body: Application
    arguments: Application
      arguments: Variable
        name: y
      operator: Application
        operator: right multiplication
    arguments: Application
      operator: multiplication
    operator: eq
  variables: Variable
    name: M
  variables: Variable
    name: x
  variables: Variable
    name: y
type: Symbol

field3
description: A CD of functions for basic constructions in field theory.
type: Library
comment: Written by Arjeh M. Cohen 2004-02-25

field by poly
description: This symbol is a binary function whose first argument is a univariate polynomial ring R over a field, and whose second argument is an irreducible polynomial f in this polynomial ring R. So, when applied to R and f, the function has value the quotient ring R/(f).
example: Application
  arguments: Literal
    value: The finite field GF(2)[X]/(X^2+X+1) is represented by
  arguments: Application
    operator: Application
      operator: field by poly
  arguments: Literal
    value: or by
  arguments: Application
    operator: field by poly
  operator: Example
type: Symbol

fraction field
description: This is a unary function. Its argument should be a domain (as in CD ring4). It denotes the fraction field of the domain.
example: Application
  arguments: Literal
    value: The rationals equals fraction_field(Integers)
  arguments: Application
    arguments: http://www.openmath.org/cd/fieldname1#Q
    operator: eq
  operator: Example
type: Symbol

free field
description: This symbol represents a binary function. The first argument should be a natural number p which is zero or a prime number, the second argument a list or a set L. When evaluated on such arguments p and L, the function represents the field of rational functions in L over the rationals if p = 0 and over the field of integers mod p if p is a prime.
example: Application
  arguments: Literal
    value: The rational function field Q(a,b) in the indeterminates a, b is
  arguments: Application
    arguments: Literal
      value: 0
    operator: free field
  operator: Example
type: Symbol

field4
description: A CD of functions for morphisms of fields.
type: Library
comment: Written by Arjeh M. Cohen 2004-07-07

automorphism group
description: This is a function with a single argument which must be a field. It refers to the automorphism group of its argument.
type: Symbol

field by poly map
description: Same as quotient_by_poly_map in CD ring5, except that R and the quotient ring R[X]/(f) are fields (so f is irreducible in R[X]).
example: Application
  arguments: Literal
    value: An element aX + b of the finite field GF(3)[X]/(X^2+1) is represented by
  arguments: Application
    arguments: Application
      operator: DMP
    operator: Application
      operator: field by poly map
  operator: Example
type: Symbol

field by poly vector
commented property: later
description: This symbol is a binary function. Its first argument should be a field_by_poly(R,f). Its second argument should be a list L of elements of F, the coefficient field of the univariate polynomial ring R = F[X]. The length of the list L should be equal to the degree d of f. When applied to R and L, it represents the element L[0] + L[1] x + L[2] x^2 + ... + L[d-1] ^(d-1) of R/(f), where x stands for the image of x under the natural quotient map R -> R/(f). If the first argument is a field_by_conway(p,n), defined in the CD finfield1, then the same interpretation holds, where R and f are respectively poly_ring_d(GFp(p),1) and conway_polynomial(p,n).
example: Application
  arguments: Literal
    value: The element x+1 of the Conway field of order 4:
  arguments: Application
    arguments: Application
      operator: field by conway
    operator: field by poly vector
  operator: Example
type: Symbol

homomorphism by generators
description: This is a function with three arguments the first two of which must be fields F and K. The third argument should be a set or a list L of ordered pairs (lists of length 2). Each pair [x,y] from L consists of an element x from F and an element y from K. when applied to F, K, and L, the symbol represents the homomorphism from F to K that maps the first entry x of each pair [x,y] to the second entry y of the same pair.
type: Symbol

fieldname1
description: A CD of functions for basic constructions in field theory.
type: Library
comment: Written by Arjeh M. Cohen 2004-02-25

http://www.openmath.org/cd/fieldname1#C
commented property: The field of complex numbers is (C, +,0,-,*,1,/), where +,-,*,/ are the standard arithmetic operations.
description: This is a symbol representing the field of complex numbers.
formal property: Application
  arguments: http://www.openmath.org/cd/fieldname1#C
  arguments: Application
    arguments: http://www.openmath.org/cd/setname1#C
    arguments: plus
    operator: field
  operator: eq
type: Symbol

http://www.openmath.org/cd/fieldname1#Q
commented property: The carrier set of this field is the set of rational numbers.
commented property: The field of rational numbers is (Q, +,0,-,*,1,/), where +,-,*,/ are the standard arithmetic operations.
description: This is a symbol representing the field of rational numbers.
example: Application
  arguments: Application
    arguments: http://www.openmath.org/cd/fieldname1#Q
    arguments: Application
      operator: field
    operator: eq
  operator: Example
formal property: Application
  arguments: http://www.openmath.org/cd/fieldname1#Q
  arguments: Application
    arguments: http://www.openmath.org/cd/setname1#Q
    arguments: plus
    operator: field
  operator: eq
formal property: Application
  arguments: Application
    arguments: http://www.openmath.org/cd/fieldname1#Q
    operator: carrier
  arguments: http://www.openmath.org/cd/setname1#Q
  operator: eq
type: Symbol

http://www.openmath.org/cd/fieldname1#R
commented property: The field of real numbers is (R, +,0,-,*,1,/), where +,-,*,/ are the standard arithmetic operations.
description: This is a symbol representing the field of real numbers.
formal property: Application
  arguments: http://www.openmath.org/cd/fieldname1#R
  arguments: Application
    arguments: http://www.openmath.org/cd/setname1#R
    arguments: plus
    operator: field
  operator: eq
type: Symbol

finfield1
description: A CD to instantiate finite fields.
type: Library
comment: Built by Arjeh M. Cohen 2003-02-25. The information on Conway polynomials is largely taken from Frank Luebeck.

conway polynomial
description: This symbol represents a binary function. Its arguments should be a prime number p and a positive integer n. Before defining which of the possible f(X) is the Conway polynomial we introduce an ordering of the (univariate) polynomials of degree n over GF(p). Here the coefficients of the polynomials are taken in {0, ..., p-1}, the indeterminate is X. Let g(X) = g_nX^n + ... + g_0 and h(X) = h_nX^n + ... + h_0. Then we define g < h if and only if there is an index k with g_i = h_i for i > k and (-1)^{n-k} g_k < (-1)^{n-k} h_k. The Conway polynomial f_{p,n}(X) for GF(p^n) is defined recursively as the smallest polynomial of degree n with respect to this ordering such that: 1) f_{p,n}(X) is monic, 2) f_{p,n}(X) is primitive, that is, it is irreducible and its zeros are generators of the (cyclic) multiplicative group of GF(p^n), 3) for each proper divisor m of n we have that f_{p,m}(X^{(p^n-1) / (p^m-1)})= 0 mod f_{p,n}(X); that is, the ((p^n-1) / (p^m-1))-th power of a zero of f_{p,n}(X) is a zero of f_{p,m}(X).
example: Application
  arguments: Literal
    value: Some Conway polynomials for p = 2.
  arguments: Application
    arguments: Application
      operator: conway polynomial
    operator: eq
  arguments: Application
    operator: eq
  arguments: Application
    operator: eq
  operator: Example
type: Symbol
comment: The existence of these polynomials can be shown with the Chinese Remainder Theorem, see W. Nickel, Endliche Koerper in dem gruppentheoretischen Programmsystem GAP, Diploma thesis, RWTH Aachen (1988) Conway polynomials were defined by R. Parker. Their purpose is to provide a standard notation for elements in a finite field GF(p^n) with p^n elements, p being a prime. This is for example used within computer algebra systems to have data of finite field elements which can easily be ported between different programs. The Conway polynomials are also used in data bases like the Modular Atlas character tables, this was the original motivation for their definition. The computation method of computing the minimal polynomials of all compatible elements was rediscovered in L.S.Heath and N.A.Loehr, New algorithms for generating Conway polynomials over finite fields, Proceedings of the Tenth Annual ACM-SIAM Symposium on Discrete Algorithms (Baltimore, MD, 1999), 429--437, ACM, New York (1999) There are basically two methods to compute Conway polynomials. The first is to run through all polynomials of degree n over GF(p) with respect to the ordering defined above and to check the necessary conditions (for primitivity one has to check that for each proper (maximal) divisor k of p^n-1 we have that f_{p,n}(X) does not divide X^k-1). The second possibility is to take any representation of GF(p^n) and to enumerate all elements in that field which fulfill the compatibility condition 3. above. Then check for each of these elements if it is primitive and if yes compute its minimal polynomial over GF(p). The smallest polynomial found this way is the Conway polynomial. Both methods were used by R. Parker to compute a long list of Conway polynomials. These are available in computer algebra systems like GAP or Magma and they are used in several other programs, like the MeatAxe.

discrete log
commented property: later
description: This symbol represents a binary function. The first argument is the base b, a primitive element of a finite field F. The second argument is a nonzero element x in F. It returns the smallest nonnegative integer i such that x=b^i.
type: Symbol

field by conway
description: This symbol represents a binary function. The first argument should be a prime number p, the second argument a positive integer n. This symbol returns the field GF(q)[X]/ (C(X)), where q = p^n, X is an indeterminate, C(X) is the Conway polynomial f_{n,p}(X), and (C(X)) is the ideal in the polynomial ring GF(q)[X] generated by C(X).
type: Symbol

is primitive
description: This symbol represents a binary Boolean function. The first argument should be a finite field, the second a an element of that field. When applied to such arguments, the value represented is true if the second argument is a primitive element of the field, that is, a generator of the multiplicative group of the field.
type: Symbol

is primitive poly
description: This symbol is a Boolean-valued function with two arguments, the first of which should be a prime number p, and the second of which should be a polynomial with coefficients in GF(p). When applied to p and f, this symbol represents the value true if and only if f is a primitive polynomial, that is, f is irreducible over GF(p), so GF(p)[X]/(f) is a finite field of order p^n, where n is the degree of f, and the image of X in GF(p)[X]/(f) is a generator of the (cyclic) multiplicative group of GF(p)[X]/(f).
type: Symbol

minimal polynomial
description: This symbol represents a function with one or two arguments. Its first argument should be an element x of a finite field F. The second argument should be a subfield K of F. It returns the minimal polynomial of x over K. If there is only one argument, K defaults to the prime subfield of F.
example: Application
  operator: Example
type: Symbol

primitive element
description: This symbol has one or two arguments. If there is only one argument, it must be a prime power q. The optional second argument is a polynomial m which is primitive over the prime subfield of GF(q). This symbol returns a primitive element for GF(q) with minimal polynomial m. If there is only one argument, then the minimal polynomial is assumed to be the conway polynomial for GF(q).
type: Symbol

fns1
description: This CD is intended to be `compatible' with the corresponding elements in Content MathML. In this CD we give a set of functions concerning functions themselves. Functions can be constructed from expressions via a lambda expression. Also there are basic function functions like compose, etc.
type: Library
comment: This document is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. The copyright holder grants you permission to redistribute this document freely as a verbatim copy. Furthermore, the copyright holder permits you to develop any derived work from this document provided that the following conditions are met. a) The derived work acknowledges the fact that it is derived from this document, and maintains a prominent reference in the work to the original source. b) The fact that the derived work is not the original OpenMath document is stated prominently in the derived work. Moreover if both this document and the derived work are Content Dictionaries then the derived work must include a different CDName element, chosen so that it cannot be confused with any works adopted by the OpenMath Society. In particular, if there is a Content Dictionary Group whose name is, for example, `math' containing Content Dictionaries named `math1', `math2' etc., then you should not name a derived Content Dictionary `mathN' where N is an integer. However you are free to name it `private_mathN' or some such. This is because the names `mathN' may be used by the OpenMath Society for future extensions. c) The derived work is distributed under terms that allow the compilation of derived works, but keep paragraphs a) and b) intact. The simplest way to do this is to distribute the derived work under the OpenMath license, but this is not a requirement. If you have questions about this license please contact the OpenMath society at http://www.openmath.org.

domain
commented property: x is in the domain of f if and only if there exists a y in the range of f and f(x) = y
description: This symbol denotes the domain of a given function, which is the set of values it is defined over.
formal property: Application
  arguments: Application
    arguments: Variable
      name: x
    arguments: Application
      operator: domain
    operator: in
  arguments: Binding
    binder: exists
    body: Application
      operator: and
    variables: Variable
      name: y
  operator: equivalent
type: ApplicationSymbol

domainofapplication
description: Deprecated. This symbol was intended to model MathML domainofapplication but as defined it is a synonym for domain. In MathML3, MathML compatibility is defined to use the new restriction symbol.
type: ApplicationSymbol

identity
commented property: for all x | identity(x)=x
description: The identity function, it takes one argument and returns the same value.
formal property: Binding
  binder: forall
  body: Application
    arguments: Application
      arguments: Variable
        name: x
      operator: identity
    arguments: Variable
      name: x
    operator: eq
  variables: Variable
    name: x
type: ApplicationSymbol

image
commented property: x in the domain of f implies f(x) is in the image f
description: This symbol denotes the image of a given function, which is the set of values the domain of the given function maps to.
formal property: Application
  arguments: Application
    arguments: Variable
      name: x
    arguments: Application
      operator: domain
    operator: in
  arguments: Application
    arguments: Application
    operator: in
  operator: implies
type: ApplicationSymbol

inverse
commented property: (inverse(f))(f(x)) = x if f is injective, that is (for all x,y | f(x) = f(y) implies x=y) implies (inverse(f))(f(z)) = z
commented property: f(inverse(f(y))=y if f is defined at inverse(f)(y) that is, if there exists an x s.t. inverse(f)(y) = x then this implies f(inverse(f)(y)) = y
description: This symbol is used to describe the inverse of its argument (a function). This inverse may only be partially defined because the function may not have been surjective. If the function is not surjective the inverse function is ill-defined without further stipulations. No assumptions are made on the semantics of this inverse.
formal property: Application
  arguments: Binding
    binder: forall
    body: Application
      arguments: Application
        operator: eq
      operator: implies
    variables: Variable
      name: x
    variables: Variable
      name: y
  arguments: Application
    arguments: Application
    operator: eq
  operator: implies
formal property: Application
  arguments: Binding
    binder: exists
    body: Application
      arguments: Application
      operator: eq
    variables: Variable
      name: x
  arguments: Application
    arguments: Application
    operator: eq
  operator: implies
type: ApplicationSymbol

lambda
description: This symbol is used to represent anonymous functions as lambda expansions. It is used in a binder that takes two further arguments, the first of which is a list of variables, and the second of which is an expression, and it forms the function which is the lambda extraction of the expression
example: Application
  arguments: Literal
    value: An example to show the connection between curried and uncurried applications of a binary function f (lambda(x,y).(f))(a,b)= (lambda(x).((lambda(y).(f))(b)))(a)
  arguments: Binding
    binder: forall
    body: Application
      operator: eq
    variables: Variable
      name: a
  operator: Example
type: BinderSymbol

left compose
commented property: for all f,g,x | left_compose(f,g)(x) = f(g(x))
description: This symbol represents the function which forms the left-composition of its two (function) arguments.
formal property: Binding
  binder: forall
  body: Application
    arguments: Application
      arguments: Variable
        name: x
      operator: Application
        operator: left compose
    arguments: Application
      operator: Variable
        name: f
    operator: eq
  variables: Variable
    name: f
  variables: Variable
    name: g
  variables: Variable
    name: x
type: ApplicationSymbol

left inverse
description: This symbol is used to describe the left inverse of its argument (a function). This inverse may only be partially defined because the function may not have been surjective. If the function is not surjective the left inverse function is ill-defined without further stipulations. No other assumptions are made on the semantics of this left inverse.
type: ApplicationSymbol

range
commented property: the range of f is a subset of the image of f
description: This symbol denotes the range of a function, that is a set that the function will map to. The single argument should be the function whos range is being queried. It should be noted that this is not necessarily equal to the image, it is merely required to contain the image.
formal property: Application
  arguments: Application
    arguments: Variable
      name: f
    operator: range
  arguments: Application
    arguments: Variable
      name: f
    operator: image
  operator: subset
type: ApplicationSymbol

restriction
description: restriction takes two arguments, a function f, and a set S, which should be a subset of domain(f) and returns the function f restricted to S.
formal property: Application
  arguments: Application
    arguments: Application
      operator: restriction
    operator: domain
  arguments: Variable
    name: S
  operator: eq
formal property: Application
  arguments: Application
    arguments: Variable
      name: f
    arguments: Application
      operator: domain
    operator: restriction
  arguments: Variable
    name: f
  operator: eq
type: ApplicationSymbol

right inverse
description: This symbol is used to describe the right inverse of its argument (a function). This inverse may only be partially defined because the function may not have been surjective. If the function is not surjective the right inverse function is ill-defined without further stipulations. No other assumptions are made on the semantics of this right inverse.
type: ApplicationSymbol

fns2
description: This CD holds further functions concerning functions themselves. A particularly interesting function is apply_to_list which applies an nary function to all the elements in a specified list. For example, such a function can be used to form sums and products in conjunction with plus and times respectively.
type: Library
comment: This document is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. The copyright holder grants you permission to redistribute this document freely as a verbatim copy. Furthermore, the copyright holder permits you to develop any derived work from this document provided that the following conditions are met. a) The derived work acknowledges the fact that it is derived from this document, and maintains a prominent reference in the work to the original source. b) The fact that the derived work is not the original OpenMath document is stated prominently in the derived work. Moreover if both this document and the derived work are Content Dictionaries then the derived work must include a different CDName element, chosen so that it cannot be confused with any works adopted by the OpenMath Society. In particular, if there is a Content Dictionary Group whose name is, for example, `math' containing Content Dictionaries named `math1', `math2' etc., then you should not name a derived Content Dictionary `mathN' where N is an integer. However you are free to name it `private_mathN' or some such. This is because the names `mathN' may be used by the OpenMath Society for future extensions. c) The derived work is distributed under terms that allow the compilation of derived works, but keep paragraphs a) and b) intact. The simplest way to do this is to distribute the derived work under the OpenMath license, but this is not a requirement. If you have questions about this license please contact the OpenMath society at http://www.openmath.org.

apply to list
description: This symbol is used to denote the repeated application of an n-ary function on the elements of a given list. For example when used with plus or times this can represent sums and products. The symbol takes two arguments; the first of which is the n-ary function, the second a list.
example: Application
  arguments: Literal
    value: For all n 1 + 2 + ... + n = n(n+1)/2.
  arguments: Binding
    binder: forall
    body: Application
      operator: eq
    variables: Variable
      name: n
  operator: Example
example: Application
  arguments: Literal
    value: One may form a set in the following way. This gives the set {1^2, 2^2, ... , 10^2 }
  arguments: Application
    arguments: set
    operator: apply to list
  operator: Example
type: ApplicationSymbol

kernel
commented property: x in the kernal of f implies that f(x) = 0
description: This symbol denotes the kernel of a given function. This may be defined as the subset of the range of the given function which maps to the identity element of the image of the given function, however no semantics are assumed. The kernel of a function is also known as the null space of the function.
formal property: Application
  arguments: Application
    arguments: Variable
      name: x
    arguments: Application
      operator: kernel
    operator: in
  arguments: Application
    arguments: Application
    arguments: zero
    operator: eq
  operator: implies
type: ApplicationSymbol

predicate on list
description: This symbol is used to denote the chains of application or a binary predicate typified by a < b < c. In particular it is used to support the usage in MathML, where transative relations are classed as nary, but the underlying OpenMath symbols are binary. The symbol takes two arguments; the first of which is the binary predicate, the second a list. It is true if every application of the predicate on a pair of elements of the list, taken in order, returns true, otherwise it is false.
example: Application
  arguments: Literal
    value: a < b < c.
  arguments: Application
    arguments: lt
    operator: predicate on list
  operator: Example
formal property: Application
  arguments: Application
    arguments: Variable
      name: p
    arguments: nil
    operator: predicate on list
  arguments: true
  operator: eq
formal property: Application
  arguments: Application
    arguments: Variable
      name: p
    arguments: Application
      operator: append
    operator: predicate on list
  arguments: true
  operator: eq
formal property: Application
  arguments: Application
    arguments: Variable
      name: p
    arguments: Application
      operator: append
    operator: predicate on list
  arguments: Application
    arguments: Application
    operator: and
  operator: eq
type: ApplicationSymbol

right compose
commented property: right_compose(f,g)(x) = g(f(x))
description: This symbol represents a function forming the right-composition of its two functional arguments.
formal property: Binding
  binder: forall
  body: Application
    arguments: Application
      arguments: Variable
        name: x
      operator: Application
        operator: right compose
    arguments: Application
      operator: Variable
        name: g
    operator: eq
  variables: Variable
    name: f
  variables: Variable
    name: g
  variables: Variable
    name: x
type: ApplicationSymbol

fns3
description: Symbols to make statements about properties of a function
description: This CD holds further functions concerning functions themselves. A particularly interesting function is function which constructs a function with given domain and range.
type: Library
comment: This document is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. The copyright holder grants you permission to redistribute this document freely as a verbatim copy. Furthermore, the copyright holder permits you to develop any derived work from this document provided that the following conditions are met. a) The derived work acknowledges the fact that it is derived from this document, and maintains a prominent reference in the work to the original source. b) The fact that the derived work is not the original OpenMath document is stated prominently in the derived work. Moreover if both this document and the derived work are Content Dictionaries then the derived work must include a different CDName element, chosen so that it cannot be confused with any works adopted by the OpenMath Society. In particular, if there is a Content Dictionary Group whose name is, for example, `math' containing Content Dictionaries named `math1', `math2' etc., then you should not name a derived Content Dictionary `mathN' where N is an integer. However you are free to name it `private_mathN' or some such. This is because the names `mathN' may be used by the OpenMath Society for future extensions. c) The derived work is distributed under terms that allow the compilation of derived works, but keep paragraphs a) and b) intact. The simplest way to do this is to distribute the derived work under the OpenMath license, but this is not a requirement. If you have questions about this license please contact the OpenMath society at http://www.openmath.org.

continuous
description: A predicate to indicate that a function is continuous everywhere.
example: Application
  arguments: Application
    arguments: sin
    operator: continuous
  operator: Example
type: Symbol

continuous on
description: A predicate to indicate that a function is continuous over a particular region or range.
example: Application
  arguments: Literal
    value: 1/x is continuous on the real interval [1,10]
  arguments: Application
    arguments: Binding
      binder: lambda
    operator: continuous on
  operator: Example
type: Symbol

differentiable
description: A predicate to indicate that a function is differentiable over its whole domain.
example: Application
  arguments: Application
    arguments: sin
    operator: differentiable
  operator: Example
type: Symbol

differentiable on
description: A predicate to indicate that a function is differentiable on a region.
example: Application
  arguments: Application
    arguments: sin
    arguments: http://www.openmath.org/cd/setnames1#R
    operator: differentiable on
  operator: Example
type: Symbol

function
commented property: The domain of the function f constructed this way is the first argument
commented property: The range of the function f constructed this way is the second argument
description: This symbol denotes a function constructor. When aplied to at least two arguments, which are sets, the first argument is the domain and the second the range of the function. When applied to at least three arguments, the first two of which are stes and the third of which is a lambda expression, the third argument gives the function specification.
example: Application
  arguments: Literal
    value: The following object defines a function from the natural numbers into the integers specificied by the fact that n maps to n(n+1)/2.
  arguments: Application
    arguments: http://www.openmath.org/cd/setname1#N
    arguments: http://www.openmath.org/cd/setname1#Z
    operator: function
  operator: Example
formal property: Application
  arguments: Application
    arguments: Application
      operator: function
    operator: domain
  arguments: Variable
    name: X
  operator: eq
formal property: Application
  arguments: Application
    arguments: Application
      operator: function
    operator: range
  arguments: Variable
    name: Y
  operator: eq
type: Symbol

piecewise continuous
description: A predicate to indicate that a function is piecewise continuous everywhere, i.e. continuous at all but a finite number of points in its domain.
example: Application
  arguments: Literal
    value: 1/x is continuous everywhere except x=0.
  arguments: Application
    arguments: Binding
      binder: lambda
    operator: piecewise continuous
  operator: Example
type: Symbol

piecewise continuous on
description: A predicate to indicate that a function is continuous at all but a finite number of points in a region.
example: Application
  arguments: Literal
    value: tan is piecewise continuous over the real interval [0,pi]
  arguments: Application
    arguments: tan
    operator: piecewise continuous on
  operator: Example
type: Symbol

specification
description: This symbol denotes the specification of a function. It is a unary function. When aplied to its argument, which should be a function applied to three arguments, it returns the third argument of the function, that is, the function specification.
example: Application
  arguments: Literal
    value: The following object defines a function from the natural numbers into the integers specificied by the fact that n maps to n(n+1)/2.
  arguments: Application
    arguments: Application
      operator: specification
    operator: eq
  operator: Example
formal property: Application
  arguments: Application
    arguments: Application
      arguments: http://www.openmath.org/cd/setname1#N
      operator: function
    operator: specification
  arguments: Variable
    name: f
  operator: eq
type: Symbol

freealg1
description: This CD defines elements of a free algebra.
type: Library

times
description: Multiplication in the free algebra.
type: Symbol

gen hyperbolic1
description: This CD contains a symbol to represent the generalised hyperbolic function, and facts relating it to other functions.
type: Library
comment: This document is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. The copyright holder grants you permission to redistribute this document freely as a verbatim copy. Furthermore, the copyright holder permits you to develop any derived work from this document provided that the following conditions are met. a) The derived work acknowledges the fact that it is derived from this document, and maintains a prominent reference in the work to the original source. b) The fact that the derived work is not the original OpenMath document is stated prominently in the derived work. Moreover if both this document and the derived work are Content Dictionaries then the derived work must include a different CDName element, chosen so that it cannot be confused with any works adopted by the OpenMath Society. In particular, if there is a Content Dictionary Group whose name is, for example, `math' containing Content Dictionaries named `math1', `math2' etc., then you should not name a derived Content Dictionary `mathN' where N is an integer. However you are free to name it `private_mathN' or some such. This is because the names `mathN' may be used by the OpenMath Society for future extensions. c) The derived work is distributed under terms that allow the compilation of derived works, but keep paragraphs a) and b) intact. The simplest way to do this is to distribute the derived work under the OpenMath license, but this is not a requirement. If you have questions about this license please contact the OpenMath society at http://www.openmath.org.

generalised hyperbolic
commented property: for all z \in C F^1_{1,0} (z) = e^z
commented property: for all z \in C F^{-1}_{2,-1} (z) = sin(z)
commented property: for all z \in C F^{-1}_{2,0} (z) = cos(z)
commented property: for all z \in C F^{1}_{2,0} (z) = cosh(z)
commented property: for all z \in C F^{1}_{2,1} (z) = sinh(z)
commented property: for complex \alpha, integral n and r an integer between 0 and r (inclusive) (F^\alpha_{n,r})(x) = \Sigma^\infty_{k=0}{\frac{\alpha^k}{(nk+r)!}x^{nk+r}}
description: This symbol represents the generalised hyperbolic function as recorded by Riccati. It is intended to be applied in the curried form, that is, the symbol should be applied to three arguments in order to return a function which should be applied to one argument. The generalised hyperbolic function may be defined as an infinite sum as in the first CMP/FMP .
formal property: Application
  arguments: Application
    arguments: Application
      operator: in
    arguments: Application
      operator: in
    operator: and
  arguments: Application
    arguments: Application
    operator: eq
  operator: implies
formal property: Binding
  binder: forall
  body: Application
    arguments: Application
      arguments: Variable
        name: z
      arguments: http://www.openmath.org/cd/setname1#C
      operator: in
    arguments: Application
      operator: eq
    operator: implies
  variables: Variable
    name: z
formal property: Binding
  binder: forall
  body: Application
    arguments: Application
      arguments: Variable
        name: z
      arguments: http://www.openmath.org/cd/setname1#C
      operator: in
    arguments: Application
      operator: eq
    operator: implies
  variables: Variable
    name: z
formal property: Binding
  binder: forall
  body: Application
    arguments: Application
      arguments: Variable
        name: z
      arguments: http://www.openmath.org/cd/setname1#C
      operator: in
    arguments: Application
      operator: eq
    operator: implies
  variables: Variable
    name: z
formal property: Binding
  binder: forall
  body: Application
    arguments: Application
      arguments: Variable
        name: z
      arguments: http://www.openmath.org/cd/setname1#C
      operator: in
    arguments: Application
      operator: eq
    operator: implies
  variables: Variable
    name: z
formal property: Binding
  binder: forall
  body: Application
    arguments: Application
      arguments: Variable
        name: z
      arguments: http://www.openmath.org/cd/setname1#C
      operator: in
    arguments: Application
      operator: eq
    operator: implies
  variables: Variable
    name: z
type: Symbol

generic alg cats
description: A CD of generic algebraic categories. This CD holds information relating to the heirarchical sturcture of the algebraic category system.
type: Library
comment: This document is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. The copyright holder grants you permission to redistribute this document freely as a verbatim copy. Furthermore, the copyright holder permits you to develop any derived work from this document provided that the following conditions are met. a) The derived work acknowledges the fact that it is derived from this document, and maintains a prominent reference in the work to the original source. b) The fact that the derived work is not the original OpenMath document is stated prominently in the derived work. Moreover if both this document and the derived work are Content Dictionaries then the derived work must include a different CDName element, chosen so that it cannot be confused with any works adopted by the OpenMath Society. In particular, if there is a Content Dictionary Group whose name is, for example, `math' containing Content Dictionaries named `math1', `math2' etc., then you should not name a derived Content Dictionary `mathN' where N is an integer. However you are free to name it `private_mathN' or some such. This is because the names `mathN' may be used by the OpenMath Society for future extensions. c) The derived work is distributed under terms that allow the compilation of derived works, but keep paragraphs a) and b) intact. The simplest way to do this is to distribute the derived work under the OpenMath license, but this is not a requirement. If you have questions about this license please contact the OpenMath society at http://www.openmath.org.

Abelian group
commented property: An Abelian group is a group
description: This Symbol represents the generic category of Abelian group.
formal property: Application
  arguments: Abelian group
  arguments: group
  operator: has
type: Symbol

Abelian monoid
commented property: An Abelian monoid is a monoid
description: This Symbol represents the generic category of Abelian monoid.
formal property: Application
  arguments: Abelian monoid
  arguments: monoid
  operator: has
type: Symbol

Abelian semigroup
commented property: An Abelian semigroup is a semigroup
description: This Symbol represents the generic category of Abelian semigroup.
formal property: Application
  arguments: Abelian semigroup
  arguments: semigroup
  operator: has
type: Symbol

Euclidean domain
commented property: A Euclidean domain is a ring
description: This Symbol represents the generic category of Euclidean domain.
formal property: Application
  arguments: Euclidean domain
  arguments: ring
  operator: has
type: Symbol

field
commented property: A field is a ring
commented property: A field is an Abelian group under +
description: This Symbol represents the generic category of field.
formal property: Application
  arguments: Application
    arguments: Variable
      name: F
    arguments: field
    operator: in
  arguments: Application
    arguments: Application
      operator: Abelian group
    arguments: Abelian group
    operator: in
  operator: implies
formal property: Application
  arguments: field
  arguments: ring
  operator: has
type: Symbol

group
commented property: A group is a monoid
description: This Symbol represents the generic category of group.
formal property: Application
  arguments: group
  arguments: monoid
  operator: has
type: Symbol

groupoid
description: This Symbol represents the generic category of groupoid.
type: Symbol

integral domain
commented property: An integral domain is a ring
description: This Symbol represents the generic category of integral domain.
formal property: Application
  arguments: integral domain
  arguments: ring
  operator: has
type: Symbol

monoid
commented property: A monoid is a groupoid
description: This Symbol represents the generic category of monoid.
formal property: Application
  arguments: monoid
  arguments: groupoid
  operator: has
type: Symbol

non commutative ring
commented property: A non-commutative ring is a ring
description: This Symbol represents the generic category of non-commutative ring.
formal property: Application
  arguments: non commutative ring
  arguments: ring
  operator: has
type: Symbol

ordered Abelian group
commented property: An ordered Abelian group is an Abelian group
commented property: An ordered Abelian group is an ordered group
description: This Symbol represents the generic category of ordered Abelian group.
formal property: Application
  arguments: ordered Abelian group
  arguments: Abelian group
  operator: has
formal property: Application
  arguments: ordered Abelian group
  arguments: ordered group
  operator: has
type: Symbol

ordered Abelian monoid
commented property: An ordered Abelian monoid is an Abelian monoid
commented property: An ordered Abelian monoid is an ordered monoid
description: This Symbol represents the generic category of ordered Abelian monoid.
formal property: Application
  arguments: ordered Abelian monoid
  arguments: Abelian monoid
  operator: has
formal property: Application
  arguments: ordered Abelian monoid
  arguments: ordered monoid
  operator: has
type: Symbol

ordered group
commented property: An ordered group is a group
description: This Symbol represents the generic category of ordered group.
formal property: Application
  arguments: ordered group
  arguments: group
  operator: has
type: Symbol

ordered monoid
commented property: An ordered monoid is a monoid
description: This Symbol represents the generic category of ordered monoid.
formal property: Application
  arguments: ordered monoid
  arguments: monoid
  operator: has
type: Symbol

ordered ring
commented property: An ordered ring is a ring
description: This Symbol represents the generic category of ordered ring.
formal property: Application
  arguments: ordered ring
  arguments: ring
  operator: has
type: Symbol

ring
commented property: A ring is a group under addition
commented property: A ring is a ringoid
commented property: A ring is a semigroup under multiplication
description: This Symbol represents the generic category of ring.
formal property: Application
  arguments: ring
  arguments: ringoid
  operator: has
formal property: Application
  arguments: Application
    arguments: Variable
      name: R
    arguments: ring
    operator: in
  arguments: Application
    arguments: Application
      operator: group
    arguments: group
    operator: in
  operator: implies
formal property: Application
  arguments: Application
    arguments: Variable
      name: R
    arguments: ring
    operator: in
  arguments: Application
    arguments: Application
      operator: semigroup
    arguments: semigroup
    operator: in
  operator: implies
type: Symbol

ringoid
description: This symbol represents the generic category of ringoid.
type: Symbol

semigroup
commented property: A semigroup is a groupoid
description: This Symbol represents the generic category of semigroup.
formal property: Application
  arguments: semigroup
  arguments: groupoid
  operator: has
type: Symbol

gp1
description: A CD of functions for group theory
type: Library
comment: This document is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. The copyright holder grants you permission to redistribute this document freely as a verbatim copy. Furthermore, the copyright holder permits you to develop any derived work from this document provided that the following conditions are met. a) The derived work acknowledges the fact that it is derived from this document, and maintains a prominent reference in the work to the original source. b) The fact that the derived work is not the original OpenMath document is stated prominently in the derived work. Moreover if both this document and the derived work are Content Dictionaries then the derived work must include a different CDName element, chosen so that it cannot be confused with any works adopted by the OpenMath Society. In particular, if there is a Content Dictionary Group whose name is, for example, `math' containing Content Dictionaries named `math1', `math2' etc., then you should not name a derived Content Dictionary `mathN' where N is an integer. However you are free to name it `private_mathN' or some such. This is because the names `mathN' may be used by the OpenMath Society for future extensions. c) The derived work is distributed under terms that allow the compilation of derived works, but keep paragraphs a) and b) intact. The simplest way to do this is to distribute the derived work under the OpenMath license, but this is not a requirement. If you have questions about this license please contact the OpenMath society at http://www.openmath.org.
comment: Written by A. Solomon on 1998-11-19 Modified by David Carlisle 1998-04-28 This is the old version of group1. It is now deprecated in facour of the Cds in the riaca_algebra CD group.

character table
description: This is the constructor for a character table. Usage: CharacterTable(centralizer_primes, centralizer_indices, classnames, power_map, irreducibles_matrix) If G has n conjugacy classes then: * centralizer_primes is of the form [p1, .., pk] i < j implies that pi < pj and the pi are precisely the primes which divide the order of some centralizer of a conjugacy class * centralizer_indices is of the form [[i11, ...,i1k] ... [in1,...ink]] so the centralizer of class 1 has order p1^i11 ... pk^i1k etc * classnames is a list of n strings which name the conjugacy classes in line with the convention used in the Atlas of Finite Groups * power_map is of the form [list1, ..., listk] where listi[j] is the name of the class where elements of class j go when raised to the power pi. * irreducibles_matrix: rows correspond to irreducible characters, columns are conjugacy classes. Entries are the value of an element of the column's conjugacy class under the character of the row.
type: ApplicationSymbol

character table of group
description: Refers to the character table of its argument which must be a group.
type: ApplicationSymbol

conjugacy class
commented property: The conjugacy class in G with respect to h = {g^(-1) h g | g in G}
description: The binary function whose value is the set of elements which are conjugate to the second argument in the first.
formal property: Application
  arguments: Application
    arguments: Variable
      name: G
    arguments: Variable
      name: h
    operator: conjugacy class
  arguments: Application
    arguments: Application
      operator: element set
    operator: suchthat
  operator: eq
type: ApplicationSymbol

declare group
commented property: A group is closed under its operation. A groups operation is associative. A group has an identity element. Every element of a group has an inverse.
description: This symbol is a constructor for groups. It takes four arguments in the following order; a set to specify the elements in the group, a binary operation to specify the group operation, a unary operation to specify inverses of group elements and an element to specify the identity. Both the binary and unary operations should act on elements of the set and return an element of the set.
example: Application
  arguments: Literal
    value: This example represents the group which has as elements all positive and negative even numbers, the group operation is binary addition, inverses are the negative of the element and the identity is the zero element.
  arguments: Application
    arguments: Application
      operator: suchthat
    arguments: plus
    operator: declare group
  operator: Example
formal property: Application
  arguments: Application
    arguments: Variable
      name: G
    arguments: Application
      operator: declare group
    operator: eq
  arguments: Application
    arguments: Application
      operator: implies
    operator: and
  operator: implies
type: ApplicationSymbol

derived subgroup
commented property: d in the derived subgroup of G implies there exist x,y in G such that d=x y x^(-1) y^(-1)
description: The unary function whose value is the subgroup of argument generated by all products of the form xyx^-1y^-1.
formal property: Application
  arguments: Application
    arguments: Variable
      name: d
    arguments: Application
      operator: element set
    operator: in
  arguments: Binding
    binder: exists
    body: Application
      operator: and
    variables: Variable
      name: x
  operator: implies
type: ApplicationSymbol

element set
description: The unary function which returns the set of elements of a group.
type: ApplicationSymbol

group
description: The n-ary function Group. The group generated by its arguments. The arguments must have a natural group operation associated with them.
type: ApplicationSymbol

is abelian
commented property: If is_abelian(G) then for all a,b in element_set(G) a*b = b*a
description: The unary boolean function whose value is true iff the argument is an abelian group
formal property: Application
  arguments: Application
    arguments: Variable
      name: G
    operator: is abelian
  arguments: Binding
    binder: forall
    body: Application
      operator: implies
    variables: Variable
      name: a
  operator: implies
type: ApplicationSymbol

is normal
commented property: is_normal(G,H) implies that for all g in G and h in H then g^-1*h*g is in H
description: If G, H are the group arguments, then IsNormal(G,H) returns true precisely when G is normal in H. That is, g^-1*h*g is defined and contained in H for all h in H and g in G.
formal property: Application
  arguments: Application
    arguments: Variable
      name: G
    arguments: Variable
      name: H
    operator: is normal
  arguments: Binding
    binder: forall
    body: Application
      operator: and
    variables: Variable
      name: g
  operator: implies
type: ApplicationSymbol

is subgroup
commented property: A is a subgroup of B implies element_set(A) is a subset of element_set(B)
description: The binary function whose value is true if the second argument is a subgroup of the first.
formal property: Application
  arguments: Application
    arguments: Variable
      name: B
    arguments: Variable
      name: A
    operator: is subgroup
  arguments: Application
    arguments: Application
      operator: element set
    operator: subset
  operator: implies
type: ApplicationSymbol

normal closure
commented property: n in the normal closure (A,B) implies there exists a in A and b in B s.t. n = b^(-1) a b
description: The binary function whose value is the set of conjugates of the elements of the second group by elements of the first, where multiplication between them is defined.
formal property: Application
  arguments: Application
    arguments: Variable
      name: n
    arguments: Application
      operator: normal closure
    operator: in
  arguments: Binding
    binder: exists
    body: Application
      operator: and
    variables: Variable
      name: a
  operator: implies
type: ApplicationSymbol

quotient group
description: The binary function whose value is the factor group of the first argument by the second, assuming the second is normal in the first.
type: ApplicationSymbol

right transversal
description: The binary function whose value is a set of representatives for the right cosets of the second argument as a subgroup of the first.
type: ApplicationSymbol

sylow subgroup
description: The largest p-subgroup of the argument (up to conjugacy).
type: ApplicationSymbol

graph1
description: This CD defines symbols for handling directed and undirected graphs. Authored by Hans Cuypers and Erik Postma. This version is edited by amc; bugfix JHD after Robbins.
type: Library

arrowset
description: This symbol represents the set of arrows of a directed graph. It takes one argument, the directed graph.
example: Application
  arguments: Literal
    value: The arrow set of the loop consists of one loop.
  arguments: Application
    arguments: Application
      operator: arrowset
    operator: eq
  operator: Example
type: Symbol

digraph
description: This symbol refers to a digraph. It has two arguments. The first is the set of vertices, the second is the set of arrows. Arrows are represented by lists of length two, where a list represents the arrow from the first element to the second.
example: Application
  arguments: Literal
    value: The two-sided infinite directed path.
  arguments: Application
    arguments: http://www.openmath.org/cd/setname1#Z
    operator: digraph
  operator: Example
type: Symbol

edgeset
commented property: Every edge in an undirected graph Gamma is a subset of the vertex set of size two.
description: This symbol represents the set of edges of an undirected graph. It takes one argument, the undirected graph.
example: Application
  arguments: Literal
    value: Given a graph Gamma and two of its vertices v and w, this predicate asserts that they are adjacent.
  arguments: Application
    arguments: Application
      operator: set
    operator: in
  operator: Example
formal property: Binding
  binder: forall
  body: Application
    arguments: Application
      arguments: Variable
        name: e
      operator: in
    arguments: Application
      operator: and
    operator: implies
  variables: Variable
    name: e
  variables: Variable
    name: Gamma
type: Symbol

graph
description: This symbol represents an undirected graph. It takes two arguments: the vertex set of the graph and the edge set. The vertices can be arbitrary OpenMath objects. Each edge should be a set consisting of two vertices.
example: Application
  arguments: Literal
    value: A path of length 2.
  arguments: Application
    arguments: Application
      operator: set
    operator: graph
  operator: Example
type: Symbol

source
description: Given an arrow, this symbol refers to the vertex where the arrow starts. It takes one argument, the arrow.
example: Application
  arguments: Literal
    value: The arrow [a, b] starts at a.
  arguments: Application
    arguments: Application
      operator: source
    operator: eq
  operator: Example
type: Symbol

target
description: Given an arrow, this symbol refers to the vertex the arrow points to. It takes one argument, the arrow.
example: Application
  arguments: Literal
    value: The arrow [a, b] points to b.
  arguments: Application
    arguments: Application
      operator: target
    operator: eq
  operator: Example
type: Symbol

vertexset
description: This symbol represents the vertex set of a (directed or undirected) graph. It takes one argument, the graph.
example: Application
  arguments: Literal
    value: If Gamma is a graph, the following function tests whether its argument v is a vertex of Gamma.
  arguments: Binding
    binder: lambda
    body: Application
      operator: in
    variables: Variable
      name: v
  operator: Example
type: Symbol

graph2
description: This CD defines symbols for handling directed and undirected graphs. Authored by Arjeh---to be merged with version of Erik Postma.
type: Library

automorphism group
description: This symbol is a unary function whose argument is an undirected graph. When applied to an undirected graph G, it represents the automorphism group of G. The resulting automorphism group is represented as a permutation group on the vertices of the graph G.
example: Application
  arguments: Literal
    value: The automorphism group of a path of length 2 (on three nodes) is the permutation group of order two interchanging the two end nodes.
  arguments: Application
    arguments: Application
      operator: automorphism group
    operator: eq
  operator: Example
type: Symbol

is automorphism
commented property: If is_automorphism(M,f) then is_isomorphism(M,M,f)
description: This symbol is a boolean function with two arguments. The first is a graph M, the second is a map f from the element set of M to the element set of M. When applied to M and f, it denotes a graph automorphism f of M.
example: Application
  arguments: Application
    arguments: Variable
      name: M
    arguments: Variable
      name: f
    operator: is automorphism
  operator: Example
formal property: Application
  arguments: Application
    arguments: Variable
      name: M
    arguments: Variable
      name: f
    operator: is automorphism
  arguments: Application
    arguments: Variable
      name: M
    operator: is isomorphism
  operator: implies
type: Symbol

is endomorphism
commented property: If is_endomorphism(M,f) then is_homomorphism(M,M,f)
description: This symbol is a boolean function with two arguments. The first argument is a graph M, the second is a map f from the element set of M to the element set of M. When applied to M and f, it denotes that f is a graph endomorphism from M to M.
example: Application
  arguments: Application
    arguments: Variable
      name: M
    arguments: Variable
      name: f
    operator: is endomorphism
  operator: Example
formal property: Application
  arguments: Application
    arguments: Variable
      name: M
    arguments: Variable
      name: f
    operator: is endomorphism
  arguments: Application
    arguments: Variable
      name: M
    operator: is homomorphism
  operator: implies
type: Symbol

is homomorphism
commented property: If is_homomorphism(M,N,f) then, for each pair of vertices x, y of M, we have if {x,y} is an edge of M, then {f(x), f(y)} is an edge of N.
description: This symbol is a boolean function with three arguments. The first and arguments are graphs M, N, the third is a map f from the vertex set of M to the vertex set of N. When applied to M, N, and f, it denotes that f is a graph homomorphism from M to N.
formal property: Application
  arguments: Application
    arguments: Variable
      name: M
    arguments: Variable
      name: N
    operator: is homomorphism
  arguments: Binding
    binder: forall
    body: Application
      operator: implies
    variables: Variable
      name: x
  operator: implies
type: Symbol

is isomorphism
description: This symbol is a boolean function with three arguments. The first and arguments are graphs M, N, the third is a map f from the element set of M to the element set of N. When applied to M, N, and f, it denotes that f is a graph isomorphism from M to N. This means that f is a homomorphism from M to N, that f is bijective, and that its inverse is a homomorphism from N to M.
example: Application
  arguments: Application
    arguments: Variable
      name: M
    arguments: Variable
      name: N
    operator: is isomorphism
  operator: Example
type: Symbol

isomorphic
description: This symbol is a Boolean function with n arguments, n at least 2, which are graphs. When applied to M_1, ..., M_n, it denotes the fact that there is an isomorphism from each M_i to each M_j.
example: Application
  arguments: Application
    arguments: Variable
      name: M
    arguments: Variable
      name: N
    operator: isomorphic
  operator: Example
type: Symbol

group1
description: A CD of basic functions for group theory
type: Library
comment: Written by A. Solomon on 1998-11-19 Modified by David Carlisle 1998-04-28 Severely edited by Arjeh M. Cohen in 2003

carrier
description: This symbol represents a unary function, whose argument should be a group G (for instance constructed by group). When applied to G, its value should be the set of elements of G.
example: Application
  arguments: Literal
    value: The carrier of group(G,*,e,inverse) is G.
  arguments: Application
    arguments: Application
      operator: carrier
    operator: eq
  operator: Example
type: Symbol

expression
description: This symbol is a function with two arguments. Its first argument should be a group. The second should be an arithmetic expression A, whose operators are times and power, and whose leaves are members of the carrier of G. When applied to G and A, it denotes the element (of G) that is obtained from the leaves of A by applying the multiplication and the power map of G instead of the times and power from the CD arith1 appearing in A. The symbol alg1.one occurring in A will be interpreted as the identity of G.
example: Application
  arguments: Application
    arguments: Application
      operator: expression
    arguments: Literal
      value: 9
    operator: eq
  operator: Example
type: Symbol

group
commented property: A group is closed under its operation. A groups operation is associative. A group has an identity element. Every element of a group has an inverse.
description: This symbol is a constructor for groups. It takes four arguments in the following order: a set to specify the elements in the group, a binary operation to specify the group operation, an element to specify the identity, and a unary operation to specify inverses of group elements. Both the binary and unary operations should act on elements of the set and return an element of the set.
example: Application
  arguments: Literal
    value: This example represents the group which has as elements all positive and negative even numbers, the group operation is binary addition, inverses are the negative of the element and the identity is the zero element.
  arguments: Application
    arguments: Application
      operator: suchthat
    arguments: plus
    operator: group
  operator: Example
formal property: Application
  arguments: Application
    arguments: Variable
      name: G
    arguments: Application
      operator: group
    operator: eq
  arguments: Application
    arguments: Application
      operator: implies
    operator: and
  operator: implies
type: Symbol

identity
description: This symbols represents a unary function, whose argument should be a group. It returns the identity element of the group.
example: Application
  arguments: Literal
    value: The identity of group(G,*,e,inverse) is e.
  arguments: Application
    arguments: Application
      operator: identity
    operator: eq
  operator: Example
type: Symbol

inversion
description: This symbol represents a unary function, whose argument should be a group G. It returns the map sending an element of G to its inverse.
example: Application
  arguments: Literal
    value: The inversion of group(G,*,e,inverse) is inverse.
  arguments: Application
    arguments: Application
      operator: inversion
    operator: eq
  operator: Example
type: Symbol

is commutative
commented property: If is_commutative(G) then for all a,b in carrier(G) a*b = b*a
description: The unary boolean function whose value is true iff the argument is a commutative group.
formal property: Application
  arguments: Application
    arguments: Variable
      name: G
    operator: is commutative
  arguments: Binding
    binder: forall
    body: Application
      operator: implies
    variables: Variable
      name: a
  operator: implies
type: Symbol

is normal
commented property: is_normal(G,H) implies that for all g in G and h in H then inverse(g)*h*g is in H.
description: If G, H are the group arguments, then IsNormal(G,H) returns true precisely when H is normal in G. That is, inverse(g)*h*g is defined and contained in H for all h in H and g in G.
formal property: Application
  arguments: Application
    arguments: Variable
      name: G
    arguments: Variable
      name: H
    operator: is normal
  arguments: Binding
    binder: forall
    body: Application
      operator: and
    variables: Variable
      name: g
  operator: implies
type: Symbol

is subgroup
commented property: If is_subgroup(G,H) then H is a nonempty set of elements of G and H is closed under multiplication and taking inverses.
description: The binary boolean function whose value is true iff the second argument is a subgroup of the second.
type: Symbol

monoid
description: This symbol is a unary function, whose argument should be a group G. When applied to G its value is the monoid underlying G.
example: Application
  arguments: Application
    arguments: Variable
      name: G
    operator: monoid
  operator: Example
type: Symbol

multiplication
description: This symbol represents a unary function, whose argument should be a group G. It returns the multiplication map on G. We allow for the map to be n-ary.
example: Application
  arguments: Literal
    value: The multiplication of group(G,*,inverse,e) is *.
  arguments: Application
    arguments: Application
      operator: multiplication
    operator: eq
  operator: Example
type: Symbol

normal closure
commented property: n in the normal closure (A,B) implies there exists a in A and b in B s.t. n = b^(-1) a b
description: The binary function whose value is the set of conjugates of the elements of the second group by elements of the first, where multiplication between them is defined.
formal property: Application
  arguments: Application
    arguments: Variable
      name: n
    arguments: Application
      operator: normal closure
    operator: in
  arguments: Binding
    binder: exists
    body: Application
      operator: and
    variables: Variable
      name: a
  operator: implies
type: Symbol

power
description: This is a symbol with three arguments. The first argument is a group G. Its second argument is an element g of G and the third argument is an integer k. It denotes the element g^k in G.
example: Application
  arguments: Application
    arguments: Application
      operator: power
    arguments: Literal
      value: 6
    operator: eq
  operator: Example
type: Symbol

subgroup
description: This symbol is a constructor symbol with one or two arguments. The first argument is a list or set, D, of group elements. The optional second argument is the group G containing D. It denotes the subgroup of G generated by D.
example: Application
  arguments: Application
    arguments: Variable
      name: D
    arguments: Variable
      name: G
    operator: subgroup
  operator: Example
example: Application
  arguments: Literal
    value: This example represents the subgroup of the multiplicative group of the nonzero reals generated by the constants Pi and E:
  arguments: Application
    arguments: Application
      operator: list
    operator: subgroup
  operator: Example
type: Symbol

group2
description: A CD of functions like homomorphisms for groups
type: Library
comment: Written by Arjeh M. Cohen 2004-02-20. Edited AMC 2004-03-02

conjugation
commented property: conjugation(M,x) (y) = x * y * x^ {-1}.
description: This symbol is a function with two arguments, which should be a group M and an element x of M. When applied to M and x, it denotes conjugation on M by x.
formal property: Binding
  binder: forall
  body: Application
    arguments: Application
      arguments: Variable
        name: y
      operator: Application
        operator: conjugation
    arguments: Application
      operator: expression
    operator: eq
  variables: Variable
    name: M
  variables: Variable
    name: x
  variables: Variable
    name: y
type: Symbol

is automorphism
commented property: If is_automorphism(M,f) then is_isomorphism(M,M,f)
description: This symbol is a boolean function with two arguments. The first is a group M, the second is a map f from the element set of M to the element set of M. When applied to M and f, it denotes a group automorphism f of M.
example: Application
  arguments: Application
    arguments: Variable
      name: M
    arguments: Variable
      name: f
    operator: is automorphism
  operator: Example
formal property: Application
  arguments: Application
    arguments: Variable
      name: M
    arguments: Variable
      name: f
    operator: is automorphism
  arguments: Application
    arguments: Variable
      name: M
    operator: is isomorphism
  operator: implies
type: Symbol

is endomorphism
commented property: If is_endomorphism(M,f) then is_homomorphism(M,M,f)
description: This symbol is a boolean function with two arguments. The first argument is a group M, the second is a map f from the element set of M to the element set of M. When applied to M and f, it denotes that f is a group endomorphism from M to M.
example: Application
  arguments: Application
    arguments: Variable
      name: M
    arguments: Variable
      name: f
    operator: is endomorphism
  operator: Example
formal property: Application
  arguments: Application
    arguments: Variable
      name: M
    arguments: Variable
      name: f
    operator: is endomorphism
  arguments: Application
    arguments: Variable
      name: M
    operator: is homomorphism
  operator: implies
type: Symbol

is homomorphism
commented property: If is_homomorphism(M,N,f) then, for each pair of elements x, y of M, we have f(x * y) = f(x) * f(y).
description: This symbol is a boolean function with three arguments. The first two arguments are groups M, N, the third is a map f from the element set of M to the element set of N. When applied to M, N, and f, it denotes that f is a group homomorphism from M to N.
example: Application
  arguments: Application
    arguments: Variable
      name: M
    arguments: Variable
      name: N
    operator: is homomorphism
  operator: Example
formal property: Application
  arguments: Application
    arguments: Variable
      name: M
    arguments: Variable
      name: N
    operator: is homomorphism
  arguments: Binding
    binder: forall
    body: Application
      operator: implies
    variables: Variable
      name: x
  operator: implies
type: Symbol

is isomorphism
description: This symbol is a boolean function with three arguments. The first and arguments are groups M, N, the third is a map f from the element set of M to the element set of N. When applied to M, N, and f, it denotes that f is a group isomorphism from M to N. This means that f is a homomorphism from M to N, that f is bijective, and that its inverse is a homomorphism from N to M.
example: Application
  arguments: Application
    arguments: Variable
      name: M
    arguments: Variable
      name: N
    operator: is isomorphism
  operator: Example
type: Symbol

isomorphic
description: This symbol is a Boolean function with n arguments, n at least 2, which are groups. When applied to M_1, ..., M_n, it denotes the fact that there is an isomorphism from each M_i to each M_j.
example: Application
  arguments: Application
    arguments: Variable
      name: M
    arguments: Variable
      name: N
    operator: isomorphic
  operator: Example
type: Symbol

left multiplication
commented property: left_multiplication(M,x) (y) = x * y.
description: This symbol is a function with two arguments, which should be a group M and an element x of M. When applied to M and x, it denotes left multiplication on M by x.
formal property: Binding
  binder: forall
  body: Application
    arguments: Application
      arguments: Variable
        name: y
      operator: Application
        operator: left multiplication
    arguments: Application
      operator: multiplication
    operator: eq
  variables: Variable
    name: M
  variables: Variable
    name: x
  variables: Variable
    name: y
type: Symbol

right inverse multiplication
commented property: right_inverse_multiplication(M,x) (y) = y * x^(-1).
description: This symbol is a function with two arguments, which should be a group M and an element x of M. When applied to M and x, it denotes right multiplication on M by the inverse of x.
formal property: Binding
  binder: forall
  body: Application
    arguments: Application
      arguments: Variable
        name: y
      operator: Application
        operator: right inverse multiplication
    arguments: Application
      operator: multiplication
    operator: eq
  variables: Variable
    name: M
  variables: Variable
    name: x
  variables: Variable
    name: y
type: Symbol

right multiplication
commented property: right_multiplication(M,x) (y) = y * x.
description: This symbol is a function with two arguments, which should be a group M and an element x of M. When applied to M and x, it denotes right multiplication on M by x.
formal property: Binding
  binder: forall
  body: Application
    arguments: Application
      arguments: Variable
        name: y
      operator: Application
        operator: right multiplication
    arguments: Application
      operator: multiplication
    operator: eq
  variables: Variable
    name: M
  variables: Variable
    name: x
  variables: Variable
    name: y
type: Symbol

group3
description: A CD of group constructions
type: Library
comment: Written by Arjeh M. Cohen 2004-02-20.

GL
description: This symbol is a function with one argument, which should be a vector space or a module V. When applied to V it represents the group of all invertible linear transformations of V.
type: Symbol

GLn
description: This symbol is a function with two arguments. The first should be a positive integer n, the second a field F. When applied to n and F it represents the group of all invertible linear transformations of the vector space over F of dimension n.
type: Symbol

SL
description: This symbol is a function with one argument, which should be a a module V over a commutative ring. When applied to V it represents the group of all invertible linear transformations of V of determinant 1.
type: Symbol

SLn
description: This symbol is a function with two arguments. The first should be a positive integer n, the second a field F. When applied to n and F it represents the group of all invertible linear transformations of the vector space over F of dimension n having determinant 1.
type: Symbol

alternating group
description: This symbol is a function with one argument, which should be a set X. When applied to a set X it represents the group of all even permutations on X .
type: Symbol

alternatingn
description: This symbol is a function with one argument, which should be a natural number n. When applied to n it represents the group of all even permutations on the set {1,2, ...,n}.
type: Symbol

automorphism group
description: This is a function with a single argument which must be a group. It refers to the automorphism group of its argument.
type: Symbol

center
commented property: d is in the center of G if and only if for all g in G we have g d= d g.
description: This symbols represents a unary function whose argument should be a group G. Its value is the biggest subgroup of G all of whose elements commute with all elements of G.
formal property: Application
  arguments: Application
    arguments: Variable
      name: d
    arguments: Application
      operator: center
    operator: in
  arguments: Binding
    binder: forall
    body: Application
      operator: implies
    variables: Variable
      name: g
  operator: equivalent
type: Symbol

centralizer
commented property: d is in the centralizer of g in G if and only if g d= d g.
description: This symbols represents a binary function whose first argument should be a group G and whose second argument should be an element g or a list of elements L of the group G. Its value is the subgroup of G of all elements commuting with g or, if the second argument is a list, all elements of L.
formal property: Application
  arguments: Application
    arguments: Variable
      name: d
    arguments: Application
      operator: centralizer
    operator: in
  arguments: Application
    arguments: Application
      operator: in
    operator: and
  operator: equivalent
type: Symbol

derived subgroup
commented property: d in the derived subgroup of G if and only if there exist lists x,y of elements of G of equal length such that d is the product x_1 y_1 x_1^(-1) y_1^(-1) ... x_n y_n x_n^(-1) y_n^(-1).
description: The unary function whose value is the subgroup of argument generated by all products of the form xyx^-1y^-1.
formal property: Application
  arguments: Application
    arguments: Variable
      name: d
    arguments: Application
      operator: derived subgroup
    operator: in
  arguments: Binding
    binder: exists
    body: Application
      operator: and
    variables: Variable
      name: x
  operator: equivalent
type: Symbol

direct power
description: This is a binary function whose first argument should be a group G and whose second argument should be a natural number n. It refers to the direct product of n copies of G.
type: Symbol

direct product
description: This is an n-ary function whose arguments must be groups. It refers to the direct product of its arguments.
type: Symbol

free group
description: This symbol represents a unary function. The argument is a list or a set. When evaluated on such an argument, the function represents the free group generated by the entries of the list or set.
example: Application
  arguments: Literal
    value: The free group on the letters a, b:
  arguments: Application
    arguments: Application
      operator: list
    operator: free group
  operator: Example
type: Symbol

invertibles
description: This symbol is a function with one argument, which should be a monoid M. When applied to M it represents the group of all invertible elements of M.
type: Symbol

normalizer
commented property: d is in the normalizer of X in G if and only if g X= X g.
description: This symbols represents a binary function whose first argument should be a group G and whose second argument should be a set of elements or a subgroup L of the group G. Its value is the subgroup of G of all elements normalizing L.
formal property: Application
  arguments: Application
    arguments: Variable
      name: d
    arguments: Application
      operator: normalizer
    operator: in
  arguments: Application
    arguments: Application
      operator: in
    operator: and
  operator: equivalent
type: Symbol

quotient group
description: The binary function whose value is the factor group of the first argument by the second, assuming the second is normal in the first.
type: Symbol

sylow subgroup
description: This symbol represents a binary function with two arguments, the first is a group G and the second a prime number p. When applied to G and p, it represents a Sylow p-subgroup of G (which is unique up to conjugacy in G).
type: Symbol

symmetric group
description: This symbol is a function with one argument, which should be a set X. When applied to a set X it represents the group of all permutations on X .
type: Symbol

symmetric groupn
commented property: The carrier set of symmetric_groupn(k) consists of all permutations with support in the integers {1,...,k}.
description: This symbol is a function with one argument, which should be a natural number n. When applied to n it represents the group of all permutations on the set {1,2,... ,n}.
formal property: Application
  arguments: Application
    arguments: Application
      operator: symmetric groupn
    operator: carrier
  arguments: Application
    arguments: Variable
      name: n
    operator: permutationsn
  operator: eq
type: Symbol

group4
description: A CD of sets constructed from groups
type: Library
comment: Written by Arjeh M. Cohen 2004-03-02. Edited AMC 2004-03-05

are conjugate
commented property: x and y are conjugate if and only if there is h in G such that x = h y h^(-1).
description: This symbol represents a boolean ternary function whose first argument is a group G and whose second and third arguments are elements x and y of G. Its value on G, x, and y is true if and only if x and y are conjugate in G.
formal property: Application
  arguments: Application
    arguments: Variable
      name: G
    arguments: Variable
      name: x
    operator: are conjugate
  arguments: Binding
    binder: exists
    body: Application
      operator: and
    variables: Variable
      name: h
  operator: equivalent
type: Symbol

conjugacy class
commented property: The conjugacy class in G of h is the subset {g^(-1) h g | g in G} of G.
description: This symbol represents a binary function, whose first argument is a group G and whose second argument is an element x of G. Its value on G and x is the set of elements which are conjugate to x in G.
formal property: Application
  arguments: Application
    arguments: Variable
      name: G
    arguments: Variable
      name: h
    operator: conjugacy class
  arguments: Application
    arguments: Application
      operator: carrier
    operator: suchthat
  operator: eq
type: Symbol

conjugacy class representatives
description: This symbol represents a unary function whose argument should be a group. Its value on a group is a set of representatives of the conjugacy classes of that group.
type: Symbol

conjugacy classes
description: This symbol represents a unary function whose argument should be a group. Its value on a group is the set of conjugacy classes of that group.
type: Symbol

left coset
description: This symbol represents a ternary function whose first argument is a group G, whose second argument is a subgroup H of G, and whose third argument is an element x of G. Its value on G, H, and x is the left coset of H in G containing x, that is, the set x H.
type: Symbol

left coset representative
description: This symbol represents a quaternary function whose first argument is a group G, whose second argument is a subgroup H of G, whose third argument is left_transversal T of H in G, and whose fourth argument is an element of G. It assigns to G, H, T, g the element of t of T representing the left coset of H containing g, that is, t H = g H .
type: Symbol

left cosets
description: The binary function whose value is the set of left cosets of the second argument in the first.
type: Symbol

left transversal
description: The binary function whose value is a set of representatives for the left cosets of the second argument as a subgroup of the first.
type: Symbol

right coset
description: This symbol represents a ternary function whose first argument is a group G, whose second argument is a subgroup H of G, and whose third argument is an element x of G. Its value on G, H, and x is the right coset of H in G containing x, that is, the set H x.
type: Symbol

right coset representative
description: This symbol represents a quaternary function whose first argument is a group G, whose second argument is a subgroup H of G, whose third argument is right_transversal T of H in G, and whose fourth argument is an element of G. It assigns to G, H, T, g the element of t of T representing the right coset of H containing g, that is, H t = H g.
type: Symbol

right cosets
description: The binary function whose value is the set of right cosets of the second argument in the first.
type: Symbol

right transversal
description: The binary function whose value is a set of representatives for the right cosets of the second argument as a subgroup of the first.
type: Symbol

group5
description: A CD of functions for relating group elements to their images in quotients.
type: Library
comment: The left and right quotients have a natural group structure if and only if H is a normal subgroup of G.
comment: Written by Arjeh M. Cohen 2004-07-07

homomorphism by generators
description: This is a function with three arguments the first two of which must be groups F and K. The third argument should be a set or a list L of ordered pairs (lists of length 2). Each pair [x,y] from L consists of an element x from F and an element y from K. When applied to F, K, and L, the symbol represents the group homomorphism from F to K that maps the first entry x of each pair [x,y] to the second entry y of the same pair.
type: Symbol

left quotient map
commented property: The image of an element x is the right coset of x with respect to H.
description: This symbol is a binary function whose first argument is a group G and whose second argument is an subgroup H of G. When applied to G and H, its value is the natural quotient map from G to the quotient group G/H, sending x to the right coset Hx of G.
formal property: Application
  arguments: Application
    arguments: Variable
      name: x
    operator: Application
      arguments: Variable
        name: G
      operator: left quotient map
  arguments: Application
    arguments: Variable
      name: G
    operator: right coset
  operator: eq
type: Symbol

right quotient map
commented property: The image of an element x is the left coset of x with respect to H.
description: This symbol is a binary function whose first argument is a group G and whose second argument is an subgroup H of G. When applied to G and H, its value is the natural quotient map from G to the quotient group G/H, sending x to the left coset xH of G.
formal property: Application
  arguments: Application
    arguments: Variable
      name: x
    operator: Application
      arguments: Variable
        name: G
      operator: right quotient map
  arguments: Application
    arguments: Variable
      name: G
    operator: left coset
  operator: eq
type: Symbol

groupname1
description: Well known groups in group theory
type: Library
comment: Written by Arjeh M. Cohen 2003-04-15

cyclic group
description: This symbol is a function with one argument, which should be a natural number n. When applied to n it represents the cyclic group of order n.
type: Symbol

dihedral group
commented property: The dihedral group of order 2n is isomorphic to the group generated by a, b with presentation a^2 = b^n = 1 and a b a = b^(-1).
description: This symbol is a function with one argument, which should be a positive integer n. When applied to n it represents the dihedral group of order 2n. This is the group of all isometries (including reflections) of the regular n-gon in the plane.
formal property: Application
  arguments: Application
    arguments: Variable
      name: n
    operator: dihedral group
  arguments: Application
    arguments: Application
      operator: free group
    operator: quotient group
  operator: isomorphic
type: Symbol

generalized quaternion group
description: This symbol is a function with one argument, which should be a positive integer. When applied to n it represents the generalized quaternion group of order 4n. This is the group with three generators a, b, and c and relations c = a^2 = b^n, c*a = a*c , b*c = c*b, a*b = b*a*c, and c^2 = 1.
type: Symbol

quaternion group
commented property: The center of Q has order 2.
commented property: The derived subgroup of Q coincides with the center of Q.
commented property: The quaternion group is isomorphic to the group generated by a, b with presentation a^2 = b^2 = aba^(-1)b^(-1) and a^4 = 1.
description: This symbol represents the quaternion group of order 8.
formal property: Application
  arguments: quaternion group
  arguments: Application
    arguments: Application
      operator: free group
    operator: quotient group
  operator: isomorphic
type: Symbol

hypergeo0
description: This CD defines some basic hypergeometric integrals and symbols necessary to define hypergeometric functions. These functions are described in the following books. (1) Handbook of Mathematical Functions, Abramowitz, Stegun (2) Higher transcendental functions. Vol. III. Krieger Publishing Co., Inc., Melbourne, Fla., 1981, Erdlyi, Arthur; Magnus, Wilhelm; Oberhettinger, Fritz; Tricomi, Francesco G. (3) From Gauss to Painleve, Vieweg, Katsunori Iwasaki, Hironobu Kimura, Shun Shimomura, Masaaki Yoshida
type: Library

beta
commented property: beta(p,q)=\frac{gamma(p)gamma(q)}{gamma(p+q)}(p,q \not\in Z_{<=0})
description: Euler's beta function
example: Application
  arguments: Literal
    value: beta(p,q)=\int_0^1 t^{p-1} (1-t)^{q-1} dt (Re(p),Re(q)>0)
  arguments: Application
    arguments: Application
      operator: and
    operator: implies
  operator: Example
formal property: Application
  arguments: Application
    arguments: Application
      operator: notin
    arguments: Application
      operator: notin
    operator: and
  arguments: Application
    arguments: Application
      operator: times
    operator: divide
  operator: implies
type: Symbol

gamma
commented property: gamma(z)=\int_0^{+\infty} t^{z-1} e^{-z} dt (Re(z)>0)
description: Euler's gamma function
example: Application
  arguments: Literal
    value: gamma(n) = (n-1)! (n \in N)
  arguments: Application
    arguments: Application
      operator: in
    operator: implies
  operator: Example
formal property: Application
  arguments: Application
    arguments: Application
      operator: real
    arguments: Literal
      value: 0
    operator: gt
  arguments: Application
    arguments: Application
      operator: gamma
    operator: eq
  operator: implies
type: Symbol

pochhammer
commented property: pochhammer(a,n) = gamma(a+n)/gamma(a)
description: Pochhammer symbol
example: Application
  arguments: Literal
    value: pochhammer(a,n) = \prod_0^{n-1} (a+i)
  arguments: Application
    arguments: Application
      operator: pochhammer
    operator: eq
  operator: Example
formal property: Application
  arguments: Application
    arguments: Variable
      name: alpha
    arguments: Variable
      name: n
    operator: pochhammer
  arguments: Application
    arguments: Application
      operator: gamma
    operator: divide
  operator: eq
type: Symbol

hypergeo1
description: This CD defines the Gauss hypergeometric function, confluent hypergeometric functions, and generalized hypergeometric functions in one variable. These functions are described in the following books. (1) Handbook of Mathematical Functions, Abramowitz, Stegun (2) Higher transcendental functions. Vol. III. Krieger Publishing Co., Inc., Melbourne, Fla., 1981, Erdlyi, Arthur; Magnus, Wilhelm; Oberhettinger, Fritz; Tricomi, Francesco G. (3) From Gauss to Painleve, Vieweg, Katsunori Iwasaki, Hironobu Kimura, Shun Shimomura, Masaaki Yoshida.
type: Library

hypergeometric0F1
commented property: hypergeometric0F1(;a;z) =\sum_{n=0}^{+\infty} \frac{1}{pochhammer(a,n)pochhammer(1,n)} z^n
description: Hypergeometric function {}_0 F_1.
formal property: Application
  arguments: Application
    arguments: Variable
      name: a
    arguments: Variable
      name: z
    operator: hypergeometric0F1
  arguments: Application
    arguments: Application
      operator: integer interval
    operator: sum
  operator: eq
type: Symbol

hypergeometric1F1
commented property: hypergeometric1F1(a,b;z) =\sum_{n=0}^{+\infty} \frac{pochhammer(a,n)}{pochhammer(1,n)pochhammer(b,n)} z^n
description: Kummer's confluent hypergeometric function.
formal property: Application
  arguments: Application
    arguments: Variable
      name: a
    arguments: Variable
      name: b
    operator: hypergeometric1F1
  arguments: Application
    arguments: Application
      operator: integer interval
    operator: sum
  operator: eq
type: Symbol

hypergeometric2F1
commented property: hypergeometric2F1(a,b,c;z) =\sum_{n=0}^{+\infty} \frac{pochhammer(a,n)pochhammer(b,n)}{pochhammer(c,n)pochhammer(1,n)} z^n
description: The Gauss hypergeometric function. This function has a branch cut on [1,+infinity).
example: Application
  arguments: Literal
    value: z (1-z) d^2 F/dz^2 + (c - (a+b+1) z) d F/dz - a b F = 0
  arguments: Application
    arguments: Application
      operator: minus
    operator: eq
  operator: Example
formal property: Application
  arguments: Application
    arguments: Variable
      name: a
    arguments: Variable
      name: b
    operator: hypergeometric2F1
  arguments: Application
    arguments: Application
      operator: integer interval
    operator: sum
  operator: eq
type: Symbol

hypergeometric pFq
commented property: hypergeometric_pFq(a,b;z) =\sum_{n=0}^{+\infty} \frac{\Pi_i pochhammer(a_i,n)}{\Pi_i pochhammer(b_i,n)pochhammer(1,n)} z^n
description: Generalized hypergeometric function. This function has a branch cut on [1,+infinity).
formal property: Application
  arguments: Application
    arguments: Variable
      name: a
    arguments: Variable
      name: b
    operator: hypergeometric pFq
  arguments: Application
    arguments: Application
      operator: integer interval
    operator: sum
  operator: eq
type: Symbol

hypergeon0
description: This CD defines some supplementary symbols necessary for hypergeon1 and hypergeon2 (hypergeometric series of n variables). These symbols may be included in CD's linalg, logic, poly, and set.
type: Library

cartesian product n
commented property: $ Z^m \times Z^n = Z^{m+n} $
description: the cartesian product of n copies of the first argument. Binary function.
formal property: Application
  arguments: Application
    arguments: Application
      arguments: http://www.openmath.org/cd/setname1#Z
      operator: cartesian product n
    arguments: Application
      operator: cartesian product n
    operator: cartesian product
  arguments: Application
    arguments: http://www.openmath.org/cd/setname1#Z
    operator: cartesian product n
  operator: eq
type: Symbol

kernel
commented property: $\kernel(D,A) = \{ x \in D | A x = 0 \}$
description: It returns the kernel of the map defined by a matrix in a specified domain.
formal property: Application
  arguments: Application
    arguments: Variable
      name: d
    arguments: Variable
      name: a
    operator: kernel
  arguments: Application
    arguments: Variable
      name: d
    operator: suchthat
  operator: eq
type: Symbol

minus part
commented property: $u = u_{+} - u_{-}$
description: The argument is a vector. It replaces positive elements in the vector to zero and negative elements to their absolute values.
formal property: Application
  arguments: Variable
    name: u
  arguments: Application
    arguments: Application
      operator: plus part
    operator: sub
  operator: eq
type: Symbol

multi power
commented property: $x^e = \prod_{i=1}^n x_i ^ {e_i}$
description: multi_power is for using the multi-index notation.
formal property: Application
  arguments: Application
    arguments: Variable
      name: x
    arguments: Variable
      name: e
    operator: multi power
  arguments: Application
    arguments: Application
      operator: integer interval
    operator: product
  operator: eq
type: Symbol

plus part
description: The argument is a vector. It replaces negative elements in the vector to zero.
type: Symbol

where
commented property: $x^n=x x x \where{n=3}$
description: The word "where" is often used in mathematical expressions to set variables or to say side conditions. CDname logic1.implies can be used for these purposes, but "where" will be more intuitive and more friendly expression for authors.
formal property: Application
  arguments: Binding
    binder: lambda
    body: Application
      arguments: Application
        operator: power
      operator: eq
    variables: Variable
      name: n
  arguments: Application
    arguments: Variable
      name: n
    operator: eq
  operator: where
type: Symbol

icc
description: ICC Typing Attributes for OM Initial version: O. Caprotti (July 1, 1999)
type: Library
comment: Revised by W.A. Naylor on 2000-02-02 to reflect the name change of setname, also adding CDUses.
comment: This document is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. The copyright holder grants you permission to redistribute this document freely as a verbatim copy. Furthermore, the copyright holder permits you to develop any derived work from this document provided that the following conditions are met. a) The derived work acknowledges the fact that it is derived from this document, and maintains a prominent reference in the work to the original source. b) The fact that the derived work is not the original OpenMath document is stated prominently in the derived work. Moreover if both this document and the derived work are Content Dictionaries then the derived work must include a different CDName element, chosen so that it cannot be confused with any works adopted by the OpenMath Society. In particular, if there is a Content Dictionary Group whose name is, for example, `math' containing Content Dictionaries named `math1', `math2' etc., then you should not name a derived Content Dictionary `mathN' where N is an integer. However you are free to name it `private_mathN' or some such. This is because the names `mathN' may be used by the OpenMath Society for future extensions. c) The derived work is distributed under terms that allow the compilation of derived works, but keep paragraphs a) and b) intact. The simplest way to do this is to distribute the derived work under the OpenMath license, but this is not a requirement. If you have questions about this license please contact the OpenMath society at http://www.openmath.org.

IndType
description: Constructor for Inductive Types. Takes arguments the constructor functions for the inhabitants of the type and their signatures.
example: Application
  arguments: Application
    arguments: Attribution
      target: Literal
        value: 0
    arguments: Attribution
      target: succ
    operator: IndType
  arguments: Literal
    value: is the defining mathematical property for the symbolic type nat of the inductively defined natural numbers with 0 and succ as constructor functions.
  operator: Example
type: ApplicationSymbol

type
description: Attribution tag to denote type-judgement
type: Symbol
type: SemanticAttributionSymbol

typecoerce
description: Attribution tag to denote type-judgement with coercion
type: SemanticAttributionSymbol

indnat
description: Inductive definition of natural numbers Initial version: O.C (Jan. 2000)
type: Library
comment: This document is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. The copyright holder grants you permission to redistribute this document freely as a verbatim copy. Furthermore, the copyright holder permits you to develop any derived work from this document provided that the following conditions are met. a) The derived work acknowledges the fact that it is derived from this document, and maintains a prominent reference in the work to the original source. b) The fact that the derived work is not the original OpenMath document is stated prominently in the derived work. Moreover if both this document and the derived work are Content Dictionaries then the derived work must include a different CDName element, chosen so that it cannot be confused with any works adopted by the OpenMath Society. In particular, if there is a Content Dictionary Group whose name is, for example, `math' containing Content Dictionaries named `math1', `math2' etc., then you should not name a derived Content Dictionary `mathN' where N is an integer. However you are free to name it `private_mathN' or some such. This is because the names `mathN' may be used by the OpenMath Society for future extensions. c) The derived work is distributed under terms that allow the compilation of derived works, but keep paragraphs a) and b) intact. The simplest way to do this is to distribute the derived work under the OpenMath license, but this is not a requirement. If you have questions about this license please contact the OpenMath society at http://www.openmath.org.

indNat
description: Attribution tag to denote the type of inductively defined natural numbers. It is also denoted as setname1:N.
type: ConstantSymbol

plus
description: Addition of natural numbers defined recursively by using the successor.
example: Application
  arguments: Application
    arguments: Application
      operator: plus
    arguments: Application
      operator: succ
    operator: eq
  operator: Example
type: ApplicationSymbol

succ
description: Successor function on the natural number. Constructor for the inductively defined natural numbers. Takes argument a a natural number and returns a natural number.
type: ApplicationSymbol

times
description: Multiplication of natural numbers defined recursively by using the successor and plus.
example: Application
  arguments: Application
    arguments: Application
      operator: times
    arguments: Application
      operator: plus
    operator: eq
  operator: Example
type: ApplicationSymbol

zero
description: The natural number 0, also constant base function for the inductive definition of the type of natural numbers
type: ConstantSymbol

integer1
description: This CD holds a collection of basic integer functions. This CD is intended to be `compatible' with the corresponding elements in Content MathML.
type: Library
comment: This document is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. The copyright holder grants you permission to redistribute this document freely as a verbatim copy. Furthermore, the copyright holder permits you to develop any derived work from this document provided that the following conditions are met. a) The derived work acknowledges the fact that it is derived from this document, and maintains a prominent reference in the work to the original source. b) The fact that the derived work is not the original OpenMath document is stated prominently in the derived work. Moreover if both this document and the derived work are Content Dictionaries then the derived work must include a different CDName element, chosen so that it cannot be confused with any works adopted by the OpenMath Society. In particular, if there is a Content Dictionary Group whose name is, for example, `math' containing Content Dictionaries named `math1', `math2' etc., then you should not name a derived Content Dictionary `mathN' where N is an integer. However you are free to name it `private_mathN' or some such. This is because the names `mathN' may be used by the OpenMath Society for future extensions. c) The derived work is distributed under terms that allow the compilation of derived works, but keep paragraphs a) and b) intact. The simplest way to do this is to distribute the derived work under the OpenMath license, but this is not a requirement. If you have questions about this license please contact the OpenMath society at http://www.openmath.org.

factorial
commented property: factorial n = product [1..n]
description: The symbol to represent a unary factorial function on non-negative integers.
formal property: Application
  arguments: Application
    arguments: Variable
      name: n
    operator: factorial
  arguments: Application
    arguments: Application
      operator: integer interval
    operator: product
  operator: eq
type: ApplicationSymbol

factorof
commented property: b is a factor of a iff remainder of a divided by b = 0
description: This is the binary OpenMath operator that is used to indicate the mathematical relationship a "is a factor of" b, where a is the first argument and b is the second. This relationship is true if and only if b mod a = 0.
formal property: Application
  arguments: Application
    arguments: Variable
      name: b
    arguments: Variable
      name: a
    operator: factorof
  arguments: Application
    arguments: Application
      operator: remainder
    arguments: zero
    operator: eq
  operator: implies
type: ApplicationSymbol

quotient
commented property: for all a,b with a,b Integers | a = b * quotient(a,b) + remainder(a,b) and abs(remainder(a,b)) is less than abs(b) and a*remainder(a,b) >= 0
description: The symbol to represent the integer (binary) division operator. That is, for integers a and b, quotient(a,b) denotes q such that a=b*q+r, with |r| less than |b| and a*r positive.
formal property: Binding
  binder: forall
  body: Application
    arguments: Application
      arguments: Application
        operator: in
      operator: and
    arguments: Application
      operator: and
    operator: implies
  variables: Variable
    name: a
  variables: Variable
    name: b
type: ApplicationSymbol

remainder
commented property: for all a,b with a,b Integers | a = b * quotient(a,b) + remainder(a,b) and abs(remainder(a,b)) is less than abs(b) and a*remainder(a,b) >= 0
description: The symbol to represent the integer remainder after (binary) division. For integers a and b, remainder(a,b) denotes r such that a=b*q+r, with |r| less than |b| and a*r positive.
formal property: Binding
  binder: forall
  body: Application
    arguments: Application
      arguments: Application
        operator: in
      operator: and
    arguments: Application
      operator: and
    operator: implies
  variables: Variable
    name: a
  variables: Variable
    name: b
type: ApplicationSymbol

integer2
description: This CD holds a collection of basic modular arithmetic for integers.
type: Library

class
description: This symbol represents a bivariate function, whose arguments should be integers. If a, m are integers, then class(a,m) denotes the residue class a mod m in setname2.Zm.
type: Symbol

divides
commented property: For two integers a and b, the number a divides b if and only, in the magma Z with multiplication, a is a left divisor of b.
description: This symbol represents a bivariate Boolean function, whose arguments should be integers. When applied to integers a and b, it denotes the property that a divides b.
formal property: Application
  arguments: Application
    arguments: Variable
      name: a
    arguments: Variable
      name: b
    operator: divides
  arguments: Application
    arguments: Application
      operator: magma
    operator: left divides
  operator: equivalent
type: Symbol

eqmod
description: This symbol represents a Boolean valued trivariate function, whose arguments should be integers. When applied to integers a, b, m, it denotes the Boolean evalue of the assertion that a and b are equal modulo m.
type: Symbol

euler
description: This symbol denotes the univariate Euler totient function. If m is an integer, then euler(m) denotes the order of the multiplicative group of invertible elements in the residue class ring Z/mZ.
type: Symbol

modulo relation
description: This symbol represents a univariate function, whose argument should be an integer. When applied to an integer m, it denotes the equivalence relation of being equal modulo m on Z.
type: Symbol

neqmod
description: This symbol represents a Boolean valued trivariate function, whose arguments should be integers. When applied to integers a, b, m, it denotes the Boolean evalue of the assertion that a and b are not equal modulo m.
type: Symbol

ord
description: This symbol denotes a binary function. Its first argument shoud be a prime number p, the second an integer n. When applied to p and n, it represents the highest power of p occurring in a factorization of n.
example: Application
  arguments: Literal
    value: There are two factors 2 in 60:
  arguments: Application
    arguments: Application
      operator: ord
    operator: ord
  operator: Example
type: Symbol

interval1
description: This CD holds symbols which describe both discrete and continuous 1-dimensional intervals (with open/closed end points). There is also an oriented_interval, for use in integration
type: Library
comment: This document is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. The copyright holder grants you permission to redistribute this document freely as a verbatim copy. Furthermore, the copyright holder permits you to develop any derived work from this document provided that the following conditions are met. a) The derived work acknowledges the fact that it is derived from this document, and maintains a prominent reference in the work to the original source. b) The fact that the derived work is not the original OpenMath document is stated prominently in the derived work. Moreover if both this document and the derived work are Content Dictionaries then the derived work must include a different CDName element, chosen so that it cannot be confused with any works adopted by the OpenMath Society. In particular, if there is a Content Dictionary Group whose name is, for example, `math' containing Content Dictionaries named `math1', `math2' etc., then you should not name a derived Content Dictionary `mathN' where N is an integer. However you are free to name it `private_mathN' or some such. This is because the names `mathN' may be used by the OpenMath Society for future extensions. c) The derived work is distributed under terms that allow the compilation of derived works, but keep paragraphs a) and b) intact. The simplest way to do this is to distribute the derived work under the OpenMath license, but this is not a requirement. If you have questions about this license please contact the OpenMath society at http://www.openmath.org.

integer interval
description: A symbol to denote a discrete 1 dimensional interval from the first argument to the second (inclusive), where the discretisation occurs at unit intervals. The arguments are the start and the end points of the interval in that order.
example: Application
  arguments: Literal
    value: The integer interval 1, 2, ..., 10.
  arguments: Application
    arguments: Literal
      value: 1
    operator: integer interval
  operator: Example
formal property: Application
  arguments: Application
    arguments: Variable
      name: n
    arguments: Application
      operator: integer interval
    operator: in
  arguments: Application
    arguments: Application
      operator: in
    operator: and
  operator: equivalent
type: ApplicationSymbol

interval
description: A symbol to denote a continuous 1-dimensional interval without any information about the character of the end points (used in definite integration). The arguments are the start and the end points of the interval in that order.
example: Application
  arguments: Literal
    value: The interval 1.0, ..., 10.0.
  arguments: Application
    arguments: Literal
      value: 1.0
    operator: interval
  operator: Example
formal property: Application
  arguments: Application
    arguments: Variable
      name: a
    arguments: Variable
      name: b
    operator: interval
  arguments: Application
    arguments: Variable
      name: a
    operator: interval cc
  operator: subset
formal property: Application
  arguments: Application
    arguments: Variable
      name: a
    arguments: Variable
      name: b
    operator: interval oo
  arguments: Application
    arguments: Variable
      name: a
    operator: interval
  operator: subset
type: ApplicationSymbol

interval cc
description: A symbol to denote a continuous 1-dimensional interval with both end points included in the interval. The arguments are the start and the end points of the interval in that order.
example: Application
  arguments: Literal
    value: The continuous closed interval [1,10].
  arguments: Application
    arguments: Literal
      value: 1
    operator: interval cc
  operator: Example
formal property: Application
  arguments: Application
    arguments: Variable
      name: x
    arguments: Application
      operator: interval cc
    operator: in
  arguments: Application
    arguments: Application
      operator: in
    operator: and
  operator: equivalent
type: ApplicationSymbol

interval co
description: A symbol to denote a continuous 1-dimensional interval with the first point included in the interval, but the last excluded. The arguments are the start and the end points of the interval in that order.
example: Application
  arguments: Literal
    value: The continuous interval closed at the lower bound and open at the higher bound [1,10).
  arguments: Application
    arguments: Literal
      value: 1
    operator: interval co
  operator: Example
formal property: Application
  arguments: Application
    arguments: Variable
      name: x
    arguments: Application
      operator: interval co
    operator: in
  arguments: Application
    arguments: Application
      operator: in
    operator: and
  operator: equivalent
type: ApplicationSymbol

interval oc
description: A symbol to denote a continuous 1-dimensional interval with the first point excluded from the interval, but the last included. The arguments are the start and the end points of the interval in that order.
example: Application
  arguments: Literal
    value: The continuous interval open at the lower bound and closed at the higher bound (1,10].
  arguments: Application
    arguments: Literal
      value: 1
    operator: interval oc
  operator: Example
formal property: Application
  arguments: Application
    arguments: Variable
      name: x
    arguments: Application
      operator: interval oc
    operator: in
  arguments: Application
    arguments: Application
      operator: in
    operator: and
  operator: equivalent
type: ApplicationSymbol

interval oo
description: A symbol to denote a continuous 1-dimensional interval with both end points excluded from the interval. The arguments are the start and the end points of the interval in that order.
example: Application
  arguments: Literal
    value: The continuous open interval (1,10).
  arguments: Application
    arguments: Literal
      value: 1
    operator: interval oo
  operator: Example
formal property: Application
  arguments: Application
    arguments: Variable
      name: x
    arguments: Application
      operator: interval oo
    operator: in
  arguments: Application
    arguments: Application
      operator: in
    operator: and
  operator: equivalent
type: ApplicationSymbol

oriented interval
description: A symbol to denote a continuous 1-dimensional interval without any information about the character of the end points (used in definite integration). The arguments are the start and the end points of the integration, in either order.
example: Application
  arguments: Application
    arguments: Application
      operator: defintint
    arguments: Application
      operator: minus
    operator: eq
  operator: Example
type: ApplicationSymbol

interval types
description: A CD of basic interval type constructors. This CD holds constructors of individual instances of the different types of intervals.
type: Library
comment: This document is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. The copyright holder grants you permission to redistribute this document freely as a verbatim copy. Furthermore, the copyright holder permits you to develop any derived work from this document provided that the following conditions are met. a) The derived work acknowledges the fact that it is derived from this document, and maintains a prominent reference in the work to the original source. b) The fact that the derived work is not the original OpenMath document is stated prominently in the derived work. Moreover if both this document and the derived work are Content Dictionaries then the derived work must include a different CDName element, chosen so that it cannot be confused with any works adopted by the OpenMath Society. In particular, if there is a Content Dictionary Group whose name is, for example, `math' containing Content Dictionaries named `math1', `math2' etc., then you should not name a derived Content Dictionary `mathN' where N is an integer. However you are free to name it `private_mathN' or some such. This is because the names `mathN' may be used by the OpenMath Society for future extensions. c) The derived work is distributed under terms that allow the compilation of derived works, but keep paragraphs a) and b) intact. The simplest way to do this is to distribute the derived work under the OpenMath license, but this is not a requirement. If you have questions about this license please contact the OpenMath society at http://www.openmath.org.
comment: maybe we should also include some 'complex interval' symbols, could have cartesian varieties, i.e. 'square', as well as polar varieties, i.e. 'round'

algebraicIntervalType
commented property: algebraic interval type has continuous set type
commented property: algebraic interval type has real interval type
description: This symbol represents the type of algebraic intervals.
formal property: Application
  arguments: algebraicIntervalType
  arguments: realIntervalType
  operator: has
formal property: Application
  arguments: algebraicIntervalType
  arguments: continuousSetType
  operator: has
type: Symbol

integerIntervalType
commented property: integer interval type has discrete set type
commented property: integer interval type has rational interval type
description: This symbol represents the type of integer intervals.
formal property: Application
  arguments: integerIntervalType
  arguments: rationalIntervalType
  operator: has
formal property: Application
  arguments: integerIntervalType
  arguments: discreteSetType
  operator: has
type: Symbol

intervalType
commented property: interval type has set type
description: This symbol represents the type of intervals.
formal property: Application
  arguments: intervalType
  arguments: setType
  operator: has
type: Symbol

rationalIntervalType
commented property: rational interval type has algebraic interval type
commented property: rational interval type has continuous set type
description: This symbol represents the type of rational intervals.
formal property: Application
  arguments: rationalIntervalType
  arguments: algebraicIntervalType
  operator: has
formal property: Application
  arguments: rationalIntervalType
  arguments: continuousSetType
  operator: has
type: Symbol

realIntervalType
commented property: real interval type has continuous set type
commented property: real interval type has interval type
description: This symbol represents the type of real intervals.
formal property: Application
  arguments: realIntervalType
  arguments: intervalType
  operator: has
formal property: Application
  arguments: realIntervalType
  arguments: continuousSetType
  operator: has
type: Symbol

intpath1
description: This CD defines symbols to express pathes for integration for complex integral in one variable. Our pathes lie in the one dimensional complex projective space = the Riemann sphere. These pathes are sufficiently rich to express most pathes of integrations in the complex special function theory in one variables. The theory of twisted cycles ([1] and [2]) answers to the question of telling the exact space of cycles (pathes) defined by symbols in this CD. Our symbols are enough to express integral pathes when integrand functions are solutions of ordinary differential equations with polynomial coefficients. The details will be discussed in a separate paper. [1] P.Deligne, Equation differentiel dans le champ complex, Springer Lecture Note in Mathematics, 163. [2] K.Matsumoto, H.Majima, N.Takayama, Quadratic relations for confluent hypergeometric functions. Tohoku Mathematical Journal 52 (2000), 489--514.
type: Library

circle
description: The symbol circle(c,r) is the circle in the Riemann sphere of which center is c and the radius is r. The direction of the circle is the counter clockwise. When the center is intpath1.infty, the radius should be given in the standard coordinate t=1/z at the infinity.
example: Application
  arguments: Literal
    value: The residue of 1/z is equal to 2 pi sqrt(-1).
  arguments: Application
    arguments: Application
      operator: times
    operator: eq
  operator: Example
type: Symbol

circle with starting point
description: The symbol circle_with_starting_point(c,r,z0) is the circle in the Riemann sphere of which center is c and the radius is r. The direction of the circle is the counter clockwise and the staring point is z0.
example: Application
  arguments: Literal
    value: The integral representation of the beta function B(p,q) by the twisted cycle is as follows.
  arguments: Application
    arguments: Application
      operator: and
    operator: implies
  operator: Example
type: Symbol

closed path
description: The symbol closed_path(start_end,points_in, points_out) is a closed path with the starting point "start_end". The direction of the path is counter clockwise. It contains the set of points "points_in" in the inside of the path. The winding number of the path for each point in the set points_in is 1. The path is zero homotope in the space (P^1 - points_in).
type: Symbol

infty
description: The infty on the Riemann sphere. When the coordinate of the complex plane is z, we call t=1/z the standard coordinate around the infinity of the Riemann sphere.
type: Symbol

path in sector
description: The symbol path_in_sector(c,t1,t2) is an outgoing path in a sufficiently small sector with the center c and the angles t1 and t2. The path starts from the point c and it is sufficiently short. When the center is intpath1.infty, the angle should be given in the coordinate t=1/z.
example: Application
  arguments: Literal
    value: The Airy integral is expressed as follows.
  arguments: Application
    arguments: Application
      operator: plus
    operator: defint
  operator: Example
type: Symbol

path in sector2
description: The symbol path_in_sector2(c,t1,t2,z0) is an outgoing path in the sector with the center c and the angles t1 and t2. The path is the segment from the point c to the point z0 which lies in the sector.
type: Symbol

segment
description: The symbol segment(a,b) is the segment from the point a to the point b in the complex plane. If the arguments are sectors given by path_in_sector, it means the segment from a point in the circular border of the sector to a point in the circular border of the another sector.
example: Application
  arguments: Literal
    value: The beta function B(p,q) [Re(p)>0, Re(q)>0] is defined by the following integral.
  arguments: Application
    arguments: Application
      operator: segment
    operator: defint
  operator: Example
type: Symbol

lc
description: Lambda Calculus Initial version: O. Caprotti
type: Library
comment: This document is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. The copyright holder grants you permission to redistribute this document freely as a verbatim copy. Furthermore, the copyright holder permits you to develop any derived work from this document provided that the following conditions are met. a) The derived work acknowledges the fact that it is derived from this document, and maintains a prominent reference in the work to the original source. b) The fact that the derived work is not the original OpenMath document is stated prominently in the derived work. Moreover if both this document and the derived work are Content Dictionaries then the derived work must include a different CDName element, chosen so that it cannot be confused with any works adopted by the OpenMath Society. In particular, if there is a Content Dictionary Group whose name is, for example, `math' containing Content Dictionaries named `math1', `math2' etc., then you should not name a derived Content Dictionary `mathN' where N is an integer. However you are free to name it `private_mathN' or some such. This is because the names `mathN' may be used by the OpenMath Society for future extensions. c) The derived work is distributed under terms that allow the compilation of derived works, but keep paragraphs a) and b) intact. The simplest way to do this is to distribute the derived work under the OpenMath license, but this is not a requirement. If you have questions about this license please contact the OpenMath society at http://www.openmath.org.

Lambda
description: The abstraction constructor. It is followed by a list of variables and an OpenMath object.
type: ApplicationSymbol

PiType
description: The type constructor of dependant function space. It binds the (type-attributed) variables in the body, that is an OpenMath object.
example: Application
  operator: Example
type: ApplicationSymbol

mapsto
description: The type constructor of non-dependant function space. The first n-1 children denote the types of the arguments, the last denotes the return type. Contrary to sts:mapsto, arguments cannot be variables but have to be OpenMath objects that map to ground OpenMath terms (they contain no variables).
type: ApplicationSymbol

type
description: Attribution tag to denote type-judgement
type: SemanticAttributionSymbol

typecoerce
description: Attribution tag to denote type-judgement with coercion
type: SemanticAttributionSymbol

limit1
description: This CD holds the basic notion of the limits of unary functions whilst its variable tend (either from above, below or both sides) to a particular value.
type: Library
comment: This document is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. The copyright holder grants you permission to redistribute this document freely as a verbatim copy. Furthermore, the copyright holder permits you to develop any derived work from this document provided that the following conditions are met. a) The derived work acknowledges the fact that it is derived from this document, and maintains a prominent reference in the work to the original source. b) The fact that the derived work is not the original OpenMath document is stated prominently in the derived work. Moreover if both this document and the derived work are Content Dictionaries then the derived work must include a different CDName element, chosen so that it cannot be confused with any works adopted by the OpenMath Society. In particular, if there is a Content Dictionary Group whose name is, for example, `math' containing Content Dictionaries named `math1', `math2' etc., then you should not name a derived Content Dictionary `mathN' where N is an integer. However you are free to name it `private_mathN' or some such. This is because the names `mathN' may be used by the OpenMath Society for future extensions. c) The derived work is distributed under terms that allow the compilation of derived works, but keep paragraphs a) and b) intact. The simplest way to do this is to distribute the derived work under the OpenMath license, but this is not a requirement. If you have questions about this license please contact the OpenMath society at http://www.openmath.org.

above
description: This symbol is used within a limit construct to show the limit is being approached from above. It takes no arguments.
example: Application
  arguments: Literal
    value: The limit of sin(x) as x tends to 0 from above
  arguments: Application
    arguments: Literal
      value: 0
    arguments: above
    operator: limit
  operator: Example
type: ConstantSymbol

below
description: This symbol is used within a limit construct to show the limit is being approached from below. It takes no arguments.
example: Application
  arguments: Literal
    value: The limit of sin(x) as x tends to 0 from below
  arguments: Application
    arguments: Literal
      value: 0
    arguments: below
    operator: limit
  operator: Example
type: ConstantSymbol

both sides
description: This symbol is used within a limit construct to show the limit is being approached from both sides. It takes no arguments.
example: Application
  arguments: Literal
    value: The limit of sin(x) as x tends to 0 from either direction
  arguments: Application
    arguments: Literal
      value: 0
    arguments: both sides
    operator: limit
  operator: Example
type: ConstantSymbol

limit
description: This symbol is used to denote the limit of a unary function. It takes 3 arguments: the limiting value of the argument, the method of approach (either null, above, below or both_sides) and the function.
example: Application
  arguments: Literal
    value: The limit of sin(x) as x tends to 0
  arguments: Application
    arguments: Literal
      value: 0
    arguments: both sides
    operator: limit
  operator: Example
type: ApplicationSymbol

null
description: This symbol is used within a limit construct to avoid specifying the method of approach to the limit. It takes no arguments.
example: Application
  arguments: Literal
    value: The limit of sin(x) as x tends to 0
  arguments: Application
    arguments: Literal
      value: 0
    arguments: null
    operator: limit
  operator: Example
type: ConstantSymbol

linalg1
description: Operations on Matrices (independent of the matrix representation).
type: Library
comment: This document is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. The copyright holder grants you permission to redistribute this document freely as a verbatim copy. Furthermore, the copyright holder permits you to develop any derived work from this document provided that the following conditions are met. a) The derived work acknowledges the fact that it is derived from this document, and maintains a prominent reference in the work to the original source. b) The fact that the derived work is not the original OpenMath document is stated prominently in the derived work. Moreover if both this document and the derived work are Content Dictionaries then the derived work must include a different CDName element, chosen so that it cannot be confused with any works adopted by the OpenMath Society. In particular, if there is a Content Dictionary Group whose name is, for example, `math' containing Content Dictionaries named `math1', `math2' etc., then you should not name a derived Content Dictionary `mathN' where N is an integer. However you are free to name it `private_mathN' or some such. This is because the names `mathN' may be used by the OpenMath Society for future extensions. c) The derived work is distributed under terms that allow the compilation of derived works, but keep paragraphs a) and b) intact. The simplest way to do this is to distribute the derived work under the OpenMath license, but this is not a requirement. If you have questions about this license please contact the OpenMath society at http://www.openmath.org.

determinant
commented property: The determinant of an identity matrix is 1
description: This symbol denotes the unary function which returns the determinant of its argument, the argument should be a square matrix.
formal property: Application
  arguments: Application
    arguments: Application
      operator: implies
    arguments: Application
      operator: implies
    operator: and
  arguments: Application
    arguments: Application
      operator: determinant
    arguments: one
    operator: eq
  operator: implies
type: ApplicationSymbol

matrix selector
description: This symbol represents the function which allows individual entries to be selected from a matrix. It takes three arguments, the first is the index of the row and the second is the index of the column of the required element, the third argument is the matrix in question. The indexing is one based, i.e. the element in the top left hand corner is indexed by (1,1).
example: Application
  arguments: Literal
    value: Representation of a specification of selection of the top left hand entry to the matrix M.
  arguments: Application
    arguments: Literal
      value: 1
    operator: matrix selector
  operator: Example
type: ApplicationSymbol

outerproduct
commented property: outerproduct(a,b)_{i,j} = a_i * b_j
description: This symbol represents the outer product function. It takes two vector arguments and returns a matrix. It is defined as follows: if we write the {i,j}'th element of the matrix to be returned as m_{i,j}, then: m_{i,j}=a_i * b_j where a_i,b_j are the i'th and j'th elements of a, b respectively.
formal property: Application
  arguments: Application
    arguments: Variable
      name: i
    arguments: Variable
      name: j
    operator: matrix selector
  arguments: Application
    arguments: Application
      operator: vector selector
    operator: times
  operator: eq
type: ApplicationSymbol

scalarproduct
commented property: a.b = |a| * |b| * cos(\theta), where \theta is the angle between the two vectors that is |atan(a_2/a_1)-atan(b_2/b_1)|. N.B. The FMP displays the two dimensional case only.
description: This symbol represents the scalar product function. It takes two vector arguments and returns a scalar value. The scalar product of two vectors a, b is defined as |a| * |b| * cos(\theta), where \theta is the angle between the two vectors and |.| is a euclidean size function. Note that the scalar product is often referred to as the dot product.
formal property: Application
  arguments: Application
    arguments: Variable
      name: a
    arguments: Variable
      name: b
    operator: scalarproduct
  arguments: Application
    arguments: Application
      operator: root
    operator: times
  operator: eq
type: ApplicationSymbol

transpose
description: This symbol represents a unary function that denotes the transpose of the given matrix or vector
example: Application
  arguments: Literal
    value: A representation of the equation transpose matrix([0,1],[2,3]) = matrix([0,2],[1,3]) N.B. in this example the row oriented view of matrix construction is being assumed.
  arguments: Application
    arguments: Application
      operator: transpose
    operator: eq
  operator: Example
type: ApplicationSymbol

vector selector
description: This symbol represents the function which allows individual entries to be selected from a vector, or a matrixrow. It takes two arguments. The first argument is the position in the vector (or matrixrow) of the required entry, the second argument is the vector (or matrixrow) in question. The indexing is one based, i.e. the first element is indexed by one.
example: Application
  arguments: Literal
    value: Representation of a specification of selection of the second element of the specific vector [3,6,9]. N.B. in this example the row oriented view of vector construction is being assumed
  arguments: Application
    arguments: Literal
      value: 2
    operator: vector selector
  operator: Example
example: Application
  arguments: Literal
    value: Representation of a specification of selection of the second element of the specific matrixrow [0,1,0]. N.B. in this example the row oriented view of matrixrow construction is being assumed
  arguments: Application
    arguments: Literal
      value: 2
    operator: vector selector
  operator: Example
type: ApplicationSymbol

vectorproduct
commented property: if we write a as [a_1,a_2,a_3] and b as [b_1,b_2,b_3] then the vector product denoted a x b = [a_2b_3 - a_3b_2 , a_3b_1 - a_1b_3 , a_1b_2 - a_2b_1]
description: This symbol represents the vector product function. It takes two three dimensional vector arguments and returns a three dimensional vector. It is defined as follows: if we write a as [a_1,a_2,a_3] and b as [b_1,b_2,b_3] then the vector product denoted a x b = [a_2b_3 - a_3b_2 , a_3b_1 - a_1b_3 , a_1b_2 - a_2b_1]. Note that the vector product is often referred to as the cross product.
formal property: Application
  arguments: Application
    arguments: Variable
      name: A
    arguments: Variable
      name: B
    operator: vectorproduct
  arguments: Application
    arguments: Application
      operator: minus
    operator: and
  operator: eq
type: ApplicationSymbol

linalg2
description: This CD treats matrices and vectors in a row oriented fashion (using matrixrow's).
type: Library
comment: This document is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. The copyright holder grants you permission to redistribute this document freely as a verbatim copy. Furthermore, the copyright holder permits you to develop any derived work from this document provided that the following conditions are met. a) The derived work acknowledges the fact that it is derived from this document, and maintains a prominent reference in the work to the original source. b) The fact that the derived work is not the original OpenMath document is stated prominently in the derived work. Moreover if both this document and the derived work are Content Dictionaries then the derived work must include a different CDName element, chosen so that it cannot be confused with any works adopted by the OpenMath Society. In particular, if there is a Content Dictionary Group whose name is, for example, `math' containing Content Dictionaries named `math1', `math2' etc., then you should not name a derived Content Dictionary `mathN' where N is an integer. However you are free to name it `private_mathN' or some such. This is because the names `mathN' may be used by the OpenMath Society for future extensions. c) The derived work is distributed under terms that allow the compilation of derived works, but keep paragraphs a) and b) intact. The simplest way to do this is to distribute the derived work under the OpenMath license, but this is not a requirement. If you have questions about this license please contact the OpenMath society at http://www.openmath.org.

matrix
description: This symbol is an n-ary matrix constructor which requires matrixrow's as arguments. It is used to represent matrices.
example: Application
  arguments: Literal
    value: Representation of a 2x2 identity matrix
  arguments: Application
    arguments: Application
      operator: matrixrow
    operator: matrix
  operator: Example
type: ApplicationSymbol

matrixrow
description: This symbol is an n-ary constructor used to represent rows of matrices. Its arguments should be members of a ring.
example: Application
  arguments: Literal
    value: Representation of a row of a matrix of length two containing the integers [1,0]
  arguments: Application
    arguments: Literal
      value: 1
    operator: matrixrow
  operator: Example
type: ApplicationSymbol

vector
description: This symbol represents an n-ary function used to construct (or describe) vectors. Vectors in this CD are considered to be row vectors and must therefore be transposed to be considered as column vectors.
example: Application
  arguments: Literal
    value: An example of vector using n arguments. The specific vector constructed in this example is [3,6,9].
  arguments: Application
    arguments: Literal
      value: 3
    operator: vector
  operator: Example
type: ApplicationSymbol

linalg3
description: This CD treats matrices and vectors in a column oriented fashion (using matrixcolumn's).
type: Library
comment: This document is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. The copyright holder grants you permission to redistribute this document freely as a verbatim copy. Furthermore, the copyright holder permits you to develop any derived work from this document provided that the following conditions are met. a) The derived work acknowledges the fact that it is derived from this document, and maintains a prominent reference in the work to the original source. b) The fact that the derived work is not the original OpenMath document is stated prominently in the derived work. Moreover if both this document and the derived work are Content Dictionaries then the derived work must include a different CDName element, chosen so that it cannot be confused with any works adopted by the OpenMath Society. In particular, if there is a Content Dictionary Group whose name is, for example, `math' containing Content Dictionaries named `math1', `math2' etc., then you should not name a derived Content Dictionary `mathN' where N is an integer. However you are free to name it `private_mathN' or some such. This is because the names `mathN' may be used by the OpenMath Society for future extensions. c) The derived work is distributed under terms that allow the compilation of derived works, but keep paragraphs a) and b) intact. The simplest way to do this is to distribute the derived work under the OpenMath license, but this is not a requirement. If you have questions about this license please contact the OpenMath society at http://www.openmath.org.

matrix
description: This symbol is an n-ary matrix constructor which requires matrixcolumn's as arguments. It is used to represent matrices.
example: Application
  arguments: Literal
    value: Representation of a 2x2 identity matrix
  arguments: Application
    arguments: Application
      operator: matrixcolumn
    operator: matrix
  operator: Example
type: ApplicationSymbol

matrixcolumn
description: This symbol is an n-ary constructor used to represent columns of matrices. Its arguments should be members of a ring.
example: Application
  arguments: Literal
    value: Representation of a column of a matrix of length two containing the integers [1,0]
  arguments: Application
    arguments: Literal
      value: 1
    operator: matrixcolumn
  operator: Example
type: ApplicationSymbol

vector
description: This symbol represents an n-ary function used to construct (or describe) vectors. Vectors in this CD are considered to be column vectors, and must therefore be transposed to be considered as row vectors.
example: Application
  arguments: Literal
    value: An example of vector using n arguments. The specific vector constructed in this example is transpose of [3,6,9].
  arguments: Application
    arguments: Literal
      value: 3
    operator: vector
  operator: Example
type: ApplicationSymbol

linalg4
description: This CD defines symbols for basic linear algebra. Regardless of the way of forming vectors and matrices, this CD deals with eigenvalues, eigenvectors and related concepts.
type: Library
comment: This document is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. The copyright holder grants you permission to redistribute this document freely as a verbatim copy. Furthermore, the copyright holder permits you to develop any derived work from this document provided that the following conditions are met. a) The derived work acknowledges the fact that it is derived from this document, and maintains a prominent reference in the work to the original source. b) The fact that the derived work is not the original OpenMath document is stated prominently in the derived work. Moreover if both this document and the derived work are Content Dictionaries then the derived work must include a different CDName element, chosen so that it cannot be confused with any works adopted by the OpenMath Society. In particular, if there is a Content Dictionary Group whose name is, for example, `math' containing Content Dictionaries named `math1', `math2' etc., then you should not name a derived Content Dictionary `mathN' where N is an integer. However you are free to name it `private_mathN' or some such. This is because the names `mathN' may be used by the OpenMath Society for future extensions. c) The derived work is distributed under terms that allow the compilation of derived works, but keep paragraphs a) and b) intact. The simplest way to do this is to distribute the derived work under the OpenMath license, but this is not a requirement. If you have questions about this license please contact the OpenMath society at http://www.openmath.org.

characteristic eqn
commented property: p(eigenvalue(A,i)) = det(A-eigenvalue(A,i)I) = 0 where p is the characteristic equation of A
description: This symbol represents the polynomial which appears in the left hand side of the characteristic equation of a matrix. It takes one argument which should be the matrix. A definition of the characteristic equation is given in Elementary Linear Algebra, Stanley I. Grossman in Definition 2 of chapter 6, page 535.
formal property: Application
  arguments: Application
    arguments: Application
      operator: Application
        operator: characteristic eqn
    arguments: zero
    operator: eq
  arguments: Application
    arguments: Application
      operator: determinant
    arguments: zero
    operator: eq
  operator: and
type: ApplicationSymbol

columncount
description: This symbol represents the function which takes one matrix argument and returns the number of columns in that matrix.
example: Application
  arguments: Literal
    value: Specification of the number of columns in the matrix: [[1 2] [3 4] [5 6]]
  arguments: Application
    arguments: Application
      operator: matrix
    operator: columncount
  operator: Example
type: ApplicationSymbol

eigenvalue
commented property: A*eigenvector(A,i) = eigenvalue(A,i)*eigenvector(A,i)
description: This symbol represents the eigenvalue of a matrix. It takes two arguments the first should be the matrix, the second should be an index to specify the eigenvalue. The ordering imposed on the eigenvalues is first on the modulus of the value, and second on the argument of the value. A definition of eigenvalue is given in Elementary Linear Algebra, Stanley I. Grossman in Definition 1 of chapter 6, page 533.
formal property: Application
  arguments: Application
    arguments: Variable
      name: A
    arguments: Application
      operator: eigenvector
    operator: times
  arguments: Application
    arguments: Application
      operator: eigenvalue
    operator: times
  operator: eq
type: ApplicationSymbol

eigenvector
commented property: A*eigenvector(A) = eigenvalue(A)*eigenvector(A)
description: This symbol represents the eigenvector of a matrix. It takes two arguments the first should be the matrix, the second should be an index to specify which eigenvalue this eigenvector should be paired with. The ordering is as given in the eigenvalue symbol. A definition of eigenvector is given in Elementary Linear Algebra, Stanley I. Grossman in Definition 1 of chapter 6, page 533.
formal property: Application
  arguments: Application
    arguments: Variable
      name: A
    arguments: Application
      operator: eigenvector
    operator: times
  arguments: Application
    arguments: Application
      operator: eigenvalue
    operator: times
  operator: eq
type: ApplicationSymbol

rank
commented property: the rank of an nxn identity matrix is n
description: This symbol represents the function which takes one matrix argument and returns the number of linearly independent rows (or columns) of that matrix.
formal property: Application
  arguments: Application
    arguments: Application
      operator: identity
    operator: rank
  arguments: Variable
    name: n
  operator: eq
type: ApplicationSymbol

rowcount
description: This symbol represents the function which takes one matrix argument and returns the number of rows in that matrix.
example: Application
  arguments: Literal
    value: Specification of the number of rows in the matrix: [[1 2] [3 4] [5 6]]
  arguments: Application
    arguments: Application
      operator: matrix
    operator: rowcount
  operator: Example
type: ApplicationSymbol

size
description: This symbol represents the function which takes one vector argument and returns the length of that vector.
example: Application
  arguments: Literal
    value: the length of the vector [1,2,3] = 3
  arguments: Application
    arguments: Application
      operator: size
    operator: eq
  operator: Example
type: ApplicationSymbol

linalg5
description: This CD contains symbols which represent a number of special types of matrix.
type: Library
comment: This document is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. The copyright holder grants you permission to redistribute this document freely as a verbatim copy. Furthermore, the copyright holder permits you to develop any derived work from this document provided that the following conditions are met. a) The derived work acknowledges the fact that it is derived from this document, and maintains a prominent reference in the work to the original source. b) The fact that the derived work is not the original OpenMath document is stated prominently in the derived work. Moreover if both this document and the derived work are Content Dictionaries then the derived work must include a different CDName element, chosen so that it cannot be confused with any works adopted by the OpenMath Society. In particular, if there is a Content Dictionary Group whose name is, for example, `math' containing Content Dictionaries named `math1', `math2' etc., then you should not name a derived Content Dictionary `mathN' where N is an integer. However you are free to name it `private_mathN' or some such. This is because the names `mathN' may be used by the OpenMath Society for future extensions. c) The derived work is distributed under terms that allow the compilation of derived works, but keep paragraphs a) and b) intact. The simplest way to do this is to distribute the derived work under the OpenMath license, but this is not a requirement. If you have questions about this license please contact the OpenMath society at http://www.openmath.org.

Hermitian
commented property: The complex conjugate of a Hermitian matrix equals its transpose
commented property: The diagonal elements of a Hermitian matrix will be real
description: This symbol represents a Hermitian matrix, it takes one argument. The argument should be a vector of vectors of values which determine the upper triangle of the matrix. The lower triangle of the matrix is specified by the following relation: M^* = transpose(M), were M^* denotes the matrix consisting of all the complex conjugates of M.
example: Application
  arguments: Literal
    value: An example to describe the Hermitian matrix: [[1+i , 2+2i] [2-2i, 3+3i]]
  arguments: Application
    arguments: Application
      operator: vector
    operator: Hermitian
  operator: Example
formal property: Application
  arguments: Application
    arguments: Variable
      name: i
    arguments: Variable
      name: i
    operator: matrix selector
  arguments: http://www.openmath.org/cd/setname1#R
  operator: in
type: ApplicationSymbol

anti-Hermitian
commented property: The complex conjugate of an anti-Hermitian matrix equals minus its transpose
commented property: an anti-hermitian matrix will have zero on the diagonal
description: This symbol represents an anti-Hermitian matrix, it takes one argument. The argument should be a vector of vectors of values which determine the upper triangle of the matrix. The lower triangle of the matrix is specified by the following relation: - M^* = transpose(M), were M^* denotes the matrix consisting of all the complex conjugates of M. This rules implies that the main diagonal is zero, therefore the argument should not include it.
example: Application
  arguments: Literal
    value: An example to describe the anti-Hermitian matrix: [[0 , 1+i] [-1+i , 0 ]]
  arguments: Application
    arguments: Application
      operator: vector
    operator: anti-Hermitian
  operator: Example
formal property: Application
  arguments: Application
    arguments: Variable
      name: i
    arguments: Variable
      name: i
    operator: matrix selector
  arguments: zero
  operator: eq
type: ApplicationSymbol

banded
description: This symbol represents a (p,q) banded matrix, it takes one argument. A (p,q) banded matrix should always be square. The lower non-zero subdiagonal is the first element of the argument, whilst the highest non-zero super-diagonal is given by the last element of the argument. The argument determines the band of possibly non-zero entries which are positioned around the diagonal. It should be a vector of vectors, we note that they will not all be the same length, however the length of the vectors determine p and q. The longest element specifies the diagonal of the matrix and hence the size of the matrix. Every element not in the band is zero.
example: Application
  arguments: Literal
    value: A specification of the (2,1) banded matrix: [ [1 2 3 0 0] [4 5 6 7 0] [0 8 9 10 11] [0 0 12 13 14] [0 0 0 15 16]]
  arguments: Application
    arguments: Application
      operator: vector
    operator: banded
  operator: Example
type: ApplicationSymbol

constant
commented property: the rank of a non-zero constant matrix = 1
description: This symbol represents a matrix which has all entries of the same value. It takes two arguments, the first is the size of the matrix, the second is the constant which determines every element.
formal property: Application
  arguments: Application
    arguments: Variable
      name: v
    arguments: zero
    operator: neq
  arguments: Application
    arguments: Application
      operator: rank
    arguments: one
    operator: eq
  operator: implies
type: ApplicationSymbol

diagonal matrix
commented property: given a diagonal matrix, it is equal to its transpose
description: This symbol denotes an n_ary function which is used to construct an (nxn) diagonal matrix, that is a matrix where every non-diagonal element is zero, the diagonal elements are equal to the n arguments.
example: Application
  arguments: Literal
    value: The diagonal matrix with diagonal elements [1,2,3]
  arguments: Application
    arguments: Literal
      value: 1
    operator: diagonal matrix
  operator: Example
type: ApplicationSymbol

identity
commented property: for all M | identity(rowcount M) * M = M * identity(columncount M) = M
description: This symbol denotes a unary function which is used to construct an (nxn) identity matrix where n is the single positive integral argument.
example: Application
  arguments: Literal
    value: A representation of the 2x2 identity matrix [[1,0],[0,1]]
  arguments: Application
    arguments: Literal
      value: 2
    operator: identity
  operator: Example
formal property: Binding
  binder: forall
  body: Application
    arguments: Application
      arguments: Application
        operator: times
      operator: eq
    arguments: Application
      operator: eq
    operator: and
  variables: Variable
    name: M
type: ApplicationSymbol

lower-Hessenberg
commented property: the transpose of a lower-Hessenberg matrix is upper-Hessenberg
description: This symbol represents a lower-Hessenberg matrix, it takes one argument, the argument is a vector of vectors representing the non-zero elements. The first element of the argument specifies the value of the first super-diagonal, the subsequent elements specify the value of the diagonal and subsequent subdiagonals, all other elements are zero.
example: Application
  arguments: Literal
    value: A specification of a lower-Hessenberg matrix of dimension 5: [[1 2 0 0 0] [3 4 5 0 0] [6 7 8 9 0] [0 10 11 12 13] [0 0 14 15 16]]
  arguments: Application
    arguments: Application
      operator: vector
    operator: lower-Hessenberg
  operator: Example
formal property: Application
  arguments: Application
    arguments: Application
      operator: lower-Hessenberg
    operator: transpose
  arguments: Application
    arguments: Variable
      name: VV2
    operator: upper-Hessenberg
  operator: eq
type: ApplicationSymbol

lower-triangular
commented property: the product of two lower-triangular matrices is lower-triangular
description: This symbol represents a lower-triangular matrix, it takes one argument. The argument should be a vector of vectors of elements of the matrix.
example: Application
  arguments: Literal
    value: An example to describe the lower triangular matrix: [[1,0,0] [2,3,0] [4,5,6]]
  arguments: Application
    arguments: Application
      operator: vector
    operator: lower-triangular
  operator: Example
formal property: Application
  arguments: Application
    arguments: Variable
      name: VV1
    operator: lower-triangular
  arguments: Application
    arguments: Application
      operator: lower-triangular
    operator: times
  operator: eq
type: ApplicationSymbol

scalar
commented property: the scalar matrix of size n, where the scalar multiple is s = s * identity(n)
description: This symbol represents a matrix which is a scalar constant times the identity matrix. It should take two arguments, the first specifes the number of rows and columns in the matrix respectively and the third specifies the scalar multiplier.
example: Application
  arguments: Application
    arguments: Literal
      value: 4
    arguments: Literal
      value: 1.5
    operator: scalar
  operator: Example
formal property: Application
  arguments: Application
    arguments: Variable
      name: n
    arguments: Variable
      name: s
    operator: scalar
  arguments: Application
    arguments: Variable
      name: s
    operator: times
  operator: eq
type: ApplicationSymbol

skew-symmetric
commented property: The elements on the diagonal of a skew-symmetric matrix are zero
commented property: for a skew-symmetric matrix M, M = - transpose M
description: This symbol represents a skew-symmetric matrix, it takes one argument. The argument should be a vector of vectors of elements of the matrix. For j>i the ij'th element of the matrix is the (j-i+1)'th element of the i'th element of the argument. This determines the elements above the diagonal of the matrix, the elements below the diagonal of the matrix must conform to the rule M = - transpose M. This rule implies that the elements on the diagonal must be equal to 0, therefore we do not include these in the argument.
example: Application
  arguments: Literal
    value: An example to represent the skew-symmetric matrix: [[ 0, 2, 3, 4] [-2, 0, 6, 7] [-3,-6, 0, 9] [-4,-7,-9, 0]]
  arguments: Application
    arguments: Application
      operator: vector
    operator: skew-symmetric
  operator: Example
formal property: Application
  arguments: Application
    arguments: Variable
      name: i
    arguments: Variable
      name: i
    operator: matrix selector
  arguments: zero
  operator: eq
formal property: Application
  arguments: Application
    arguments: Variable
      name: VV
    operator: skew-symmetric
  arguments: Application
    arguments: Application
      operator: transpose
    operator: unary minus
  operator: eq
type: ApplicationSymbol

symmetric
commented property: for a symmetric matrix M, M = transpose M
commented property: the dimension of a symmetric matrix = the length of the vector which defines it
commented property: the sum of a symmetric matrix and its transpose is symmetric
description: This symbol represents a symmetric matrix, it takes one argument. The argument should be a vector of vectors of elements of the matrix. For j>=i the ij'th element of the matrix is the (j-i+1)'th element of the i'th element of the argument. This determines the upper triangle of the matrix, the lower triangle is specified by the rule M = transpose M.
example: Application
  arguments: Literal
    value: An example to represent the symmetric matrix: [[1,2,3,4] [2,5,6,7] [3,6,8,9] [4,7,9,10]]
  arguments: Application
    arguments: Application
      operator: vector
    operator: symmetric
  operator: Example
formal property: Application
  arguments: Application
    arguments: Application
      operator: symmetric
    arguments: Application
      operator: transpose
    operator: plus
  arguments: Application
    arguments: Variable
      name: VV2
    operator: symmetric
  operator: eq
formal property: Application
  arguments: Application
    arguments: Variable
      name: VV
    operator: symmetric
  arguments: Application
    arguments: Application
      operator: symmetric
    operator: transpose
  operator: eq
formal property: Application
  arguments: Application
    arguments: Application
      operator: symmetric
    operator: rowcount
  arguments: Application
    arguments: Variable
      name: VV
    operator: size
  operator: eq
type: ApplicationSymbol

tridiagonal
commented property: The product of two tridiagonal matrices is tridiagonal
commented property: a tridiagonal matrix is a (1,1) banded matrix
description: This symbol represents a tridiagonal matrix, it takes one argument which should be a vector of vectors which should have three elements. These should be vectors representing the sub-diagonal, the diagonal and the super-diagonal in that order.
formal property: Application
  arguments: Application
    arguments: Application
      operator: size
    arguments: Literal
      value: 3
    operator: eq
  arguments: Application
    arguments: Application
      operator: size
    operator: eq
  arguments: Application
    operator: eq
  operator: and
formal property: Application
  arguments: Application
    arguments: Application
      operator: tridiagonal
    arguments: Application
      operator: tridiagonal
    operator: times
  arguments: Application
    arguments: Variable
      name: VV3
    operator: tridiagonal
  operator: eq
type: ApplicationSymbol

upper-Hessenberg
commented property: the transpose of an upper-Hessenberg matrix is lower-Hessenberg
description: This symbol represents an upper-Hessenberg matrix, it takes one argument, the argument is a vector of vectors representing the non-zero elements. The first element of the argument specifies the value of the first subdiagonal, the subsequent elements specify the value of the diagonal and subsequent super-diagonals, all other elements are zero.
example: Application
  arguments: Literal
    value: A specification of an upper-Hessenberg matrix of dimension 5: [[1 2 3 0 0] [4 5 6 7 0] [0 8 9 10 11] [0 0 12 13 14] [0 0 0 15 16]]
  arguments: Application
    arguments: Application
      operator: vector
    operator: upper-Hessenberg
  operator: Example
formal property: Application
  arguments: Application
    arguments: Application
      operator: upper-Hessenberg
    operator: transpose
  arguments: Application
    arguments: Variable
      name: VV2
    operator: lower-Hessenberg
  operator: eq
type: ApplicationSymbol

upper-triangular
commented property: the product of two upper-triangular matrices is upper-triangular
description: This symbol represents an upper-triangular matrix, it takes one argument. The argument should be a vector of vectors of elements of the matrix.
example: Application
  arguments: Literal
    value: An example to describe the upper triangular matrix: [[1,2,3] [0,4,5] [0,0,6]]
  arguments: Application
    arguments: Application
      operator: vector
    operator: upper-triangular
  operator: Example
formal property: Application
  arguments: Application
    arguments: Variable
      name: VV1
    operator: upper-triangular
  arguments: Application
    arguments: Application
      operator: upper-triangular
    operator: times
  operator: eq
type: ApplicationSymbol

zero
commented property: for all M | zero(rowcount M,rowcount M) * M = M * zero(columncount M,columncount M) = zero(rowcount M,columncount M)
commented property: for all M | M + zero(rowcount M,columncount M) = M
description: This symbol denotes a function with two integral arguments m,n which is used to construct an (mxn) zero matrix.
example: Application
  arguments: Literal
    value: A representation of the 2x2 zero matrix [[0,0],[0,0]]
  arguments: Application
    arguments: Literal
      value: 2
    operator: zero
  operator: Example
formal property: Binding
  binder: forall
  body: Application
    arguments: Application
      arguments: Variable
        name: M
      operator: plus
    arguments: Variable
      name: M
    operator: eq
  variables: Variable
    name: M
formal property: Binding
  binder: forall
  body: Application
    arguments: Application
      arguments: Application
        operator: times
      operator: eq
    arguments: Application
      operator: eq
    operator: and
  variables: Variable
    name: M
type: ApplicationSymbol

linalg6
description: Symbols for describing sparse matrices
description: This CD contains symbols for the construction of some new matrices from old ones.
type: Library
comment: This document is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. The copyright holder grants you permission to redistribute this document freely as a verbatim copy. Furthermore, the copyright holder permits you to develop any derived work from this document provided that the following conditions are met. a) The derived work acknowledges the fact that it is derived from this document, and maintains a prominent reference in the work to the original source. b) The fact that the derived work is not the original OpenMath document is stated prominently in the derived work. Moreover if both this document and the derived work are Content Dictionaries then the derived work must include a different CDName element, chosen so that it cannot be confused with any works adopted by the OpenMath Society. In particular, if there is a Content Dictionary Group whose name is, for example, `math' containing Content Dictionaries named `math1', `math2' etc., then you should not name a derived Content Dictionary `mathN' where N is an integer. However you are free to name it `private_mathN' or some such. This is because the names `mathN' may be used by the OpenMath Society for future extensions. c) The derived work is distributed under terms that allow the compilation of derived works, but keep paragraphs a) and b) intact. The simplest way to do this is to distribute the derived work under the OpenMath license, but this is not a requirement. If you have questions about this license please contact the OpenMath society at http://www.openmath.org.

matrix tensor
commented property: If A is an m x r matrix B is an n x s matrix, then their Kronecker product is the m n x rs matrix whose i + (k-1) m, j + (l-1) n entry is A_{i,j} B_{k,l},
description: This symbol denotes a n-nary function which is used to construct the tensor product matrix of its arguments, which must be matrices.
formal property: Application
  arguments: Application
    arguments: Application
      operator: eq
    arguments: Application
      operator: eq
    operator: and
  arguments: Application
    arguments: Application
      operator: matrix selector
    operator: eq
  operator: implies
type: Symbol

nonZeroRowSparseMatrix
description: This symbol may be used for representing matrices, it is designed for efficiently representing sparse matrices where every row has at least one non-zero entry. This is an n+1 ary symbol, where n is the number of rows in the matrix. The first argument must be the number of columns in the matrix, every following argument of the symbol must be an application of a sparseMatrixRow symbol which has arguments which are sparseMatrixElement2, one sparseMatrixElement2 element for each row in the matrix, in the order in which they occur in the matrix. Any non-specified entry is implicitly zero.
example: Application
  arguments: Literal
    value: The matrix $$ \left ( \begin{array}{ccccc} 5&0&0&0&0\\ 0&0&2&0&0\\ 1&0&0&0&0\\ 0&0&0&0&1 \end{array}\right ) $$ may be represented as:
  arguments: Application
    arguments: Literal
      value: 5
    operator: nonZeroRowSparseMatrix
  operator: Example
type: Symbol

nonZeroRowSparseMatrix01
description: This symbol may be used to represent matrices which have no zero rows, and for which every row is in Z_2 efficiently. The first argument is the number of columns in the matrix, the following arguments are sparseMatrixRow elements where the arguments are sparseMatrixElement4 elements. Any non-specified entry is implicitly zero.
example: Application
  arguments: Literal
    value: The matrix $$ \left ( \begin{array}{ccccc} 1&0&0&0&1\\ 0&0&1&0&0\\ 0&0&0&1&0\\ 0&0&0&0&1 \end{array}\right ) $$ may be represented as:
  arguments: Application
    arguments: Literal
      value: 5
    operator: nonZeroRowSparseMatrix01
  operator: Example
type: Symbol

sparseMatrix
description: This symbol may be used for representing matrices, it is designed for efficiently representing sparse matrices. The symbol is n+2 ary, where the first argument is the number of rows in the matrix, the second argument is the number of columns in the matrix and n is the number of non-zero entries. The following arguments must be applications of the symbol sparseMatrixElement1. Any non-specified entry is implicitly zero.
example: Application
  arguments: Literal
    value: The matrix $$ \left ( \begin{array}{ccccc} 5&0&0&0&0\\ 0&0&6&0&0\\ 0&0&0&0&0\\ 0&0&0&0&1 \end{array}\right ) $$ may be represented as:
  arguments: Application
    arguments: Literal
      value: 4
    operator: sparseMatrix
  operator: Example
type: Symbol

sparseMatrix01
description: This symbol may be used for representing matrices which have all entries in the modular field Z_2, i.e. 1 or 0. It allows efficient representation of sparse matrices, more so than the 'sparseMatrix' symbol, since the value of the entries with values of 1 need not be stored, only their positions. The symbol is n+2 ary, where the first argument is the number of rows in the matrix, the second argument is the number of columns in the matrix. The following arguments are sparseMatrixElement3 elements described in this content dictionary. Any non-specified entry is implicitly zero.
example: Application
  arguments: Literal
    value: The matrix $$ \left ( \begin{array}{ccccc} 1&0&0&0&0\\ 0&0&1&0&0\\ 0&0&0&0&0\\ 0&0&0&0&1 \end{array}\right ) $$ may be represented as:
  arguments: Application
    arguments: Literal
      value: 4
    operator: sparseMatrix01
  operator: Example
type: Symbol

sparseMatrixElement1
description: This symbol may be used to represent a non-zero element of a sparse matrix in the following way. It takes three arguments, the first of which represents the column index, the second of which represents the row index and the third represents the value. The indexing is one based; that is an element in the top left position of the matrix will have first and second indices of 1,1 respectively. Applications of this symbol will be expected as arguments of the symbol sparseMatrix in this content dictionary.
type: Symbol

sparseMatrixElement2
description: This symbol may be used to represent a non-zero element of a sparse matrix in the following way. It takes two arguments, the first of which represents the column index, the second of which represents the value of the element. The row index is deduced from the index of the sparseMatrixRow symbols of which applications of this symbol are arguments. Applications of this symbol occur as arguments of arguments of the symbol nonZeroRowSparseMatrix only.
type: Symbol

sparseMatrixElement3
description: This symbol may be used to represent a non-zero element of a sparse matrix over Z_2 in the following way. The first and second arguments are the column and row indices of the non-zero elements respectively i.e. elements with value 1. Applications of this symbol occur as arguments of arguments of the symbol sparseMatrix01 only.
type: Symbol

sparseMatrixElement4
description: This symbol may be used to represent a non-zero element of a sparse matrix over Z_2 in the following way. The single argument is the column index of non-zero elements of the matrix, i.e. elements with value 1. Applications of this symbol occur as arguments of arguments of the symbol nonZeroRowSparseMatrix01 only.
type: Symbol

sparseMatrixRow
description: This symbol may be used to represent rows of sparse matrices, it is a fairly general symbol in that it may be used to represent rows of any type of sparse matrix from this CD. However the particular type of sparse matrix must have as elements symbols of the corresponding type, as described in that symbols description.
type: Symbol

vector tensor
description: This symbol denotes a n-nary function which is used to construct the tensor product vector of its arguments, which must be vectors.
type: Symbol

linalg7
description: A CD of structured vectors
description: This CD contains symbols for the construction of matrices from lists.
type: Library
comment: This document is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. The copyright holder grants you permission to redistribute this document freely as a verbatim copy. Furthermore, the copyright holder permits you to develop any derived work from this document provided that the following conditions are met. a) The derived work acknowledges the fact that it is derived from this document, and maintains a prominent reference in the work to the original source. b) The fact that the derived work is not the original OpenMath document is stated prominently in the derived work. Moreover if both this document and the derived work are Content Dictionaries then the derived work must include a different CDName element, chosen so that it cannot be confused with any works adopted by the OpenMath Society. In particular, if there is a Content Dictionary Group whose name is, for example, `math' containing Content Dictionaries named `math1', `math2' etc., then you should not name a derived Content Dictionary `mathN' where N is an integer. However you are free to name it `private_mathN' or some such. This is because the names `mathN' may be used by the OpenMath Society for future extensions. c) The derived work is distributed under terms that allow the compilation of derived works, but keep paragraphs a) and b) intact. The simplest way to do this is to distribute the derived work under the OpenMath license, but this is not a requirement. If you have questions about this license please contact the OpenMath society at http://www.openmath.org.

constant
commented property: If V is a constant vector of length n, with constant value c and i is in the integral interval [1,n] then V.i = c
description: The constant symbol represents the constant vector. It takes two parameters, the length (dimension) of the vector and the constant value, which all the elements are equal to.
formal property: Application
  arguments: Application
    arguments: Variable
      name: i
    arguments: Application
      operator: integer interval
    operator: in
  arguments: Application
    arguments: Application
      operator: vector selector
    operator: eq
  operator: implies
type: Symbol

list to matrix
description: This symbol denotes a binary function. Its first argument must be a ring R, its second argument must be list L of lists of equal lengths whose entries belong to the ring R, up to ring1.expression. When applied to R and L it represents the matrix whose i,j entry consists of the j-th entry from the list L[i]. In particular, the matrix has length(L) rows and length(L[1]) columns.
type: Symbol

list to vector
description: This symbol denotes a binary function. Its first argument must be a ring R, its second argument must be list L with entries belonging to the ring R, up to ring1.expression. When applied to R and L it represents the vector of the same length as the list L whose i-th coordinate is L[i] (or ring1.expression(L[i])).
type: Symbol

sparse
description: The sparse symbol is a constructor for sparse vectors, it is (n+1)-ary, where the first parameter is the length (dimension) of the vector, and every following parameter specifies a possibly non-zero element in the following way. The parameter is a list which should have length two. The first element in the list is the position (one based), whilst the second element in the list is the value. Every other element of the vector is implicitly zero.
example: Application
  arguments: Literal
    value: This example shows a representation of the sparse matrix $$\left (\begin{array}[c]1\\0\\0\\0\\0\end{array}\right$$
  arguments: Application
    arguments: Application
      operator: list
    operator: sparse
  operator: Example
type: Symbol

zero
commented property: If M is an n*m matrix and V is a zero vector of length m then V*M = V2 where V2 is a zero vector of length n
commented property: If M is an n*m matrix and V is a zero vector of length n then M*V = V2 where V2 is a zero vector of length m
commented property: If V is a zero vector of length n and V2 is a vector of length n then V+V2 = V2+V = V2
commented property: If V is a zero vector of length n and i is in the integral interval [1,n] then V.i = 0
description: The zero symbol represents the zero vector, it takes one parameter which should be the length (dimension in some terminology) of the vector.
formal property: Binding
  binder: forall
  body: Application
    arguments: Application
      arguments: Application
        operator: eq
      operator: and
    arguments: Application
      operator: eq
    operator: implies
formal property: Binding
  binder: forall
  body: Application
    arguments: Application
      arguments: Application
        operator: eq
      operator: and
    arguments: Application
      operator: eq
    operator: implies
formal property: Binding
  binder: forall
  body: Application
    arguments: Application
      arguments: Application
        operator: size
      operator: eq
    arguments: Application
      operator: and
    operator: implies
formal property: Application
  arguments: Application
    arguments: Variable
      name: i
    arguments: Application
      operator: integer interval
    operator: in
  arguments: Application
    arguments: Application
      operator: vector selector
    arguments: zero
    operator: eq
  operator: implies
type: Symbol

list1
description: This CD is intended to be `compatible' with MathML list constructs.
description: This CD is intended to be `compatible' with MathML list constructs. A.M. Cohen slightly edited the description of the suchthat symbol (eq, "the set" replaced by "a set X").
type: Library
comment: This document is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. The copyright holder grants you permission to redistribute this document freely as a verbatim copy. Furthermore, the copyright holder permits you to develop any derived work from this document provided that the following conditions are met. a) The derived work acknowledges the fact that it is derived from this document, and maintains a prominent reference in the work to the original source. b) The fact that the derived work is not the original OpenMath document is stated prominently in the derived work. Moreover if both this document and the derived work are Content Dictionaries then the derived work must include a different CDName element, chosen so that it cannot be confused with any works adopted by the OpenMath Society. In particular, if there is a Content Dictionary Group whose name is, for example, `math' containing Content Dictionaries named `math1', `math2' etc., then you should not name a derived Content Dictionary `mathN' where N is an integer. However you are free to name it `private_mathN' or some such. This is because the names `mathN' may be used by the OpenMath Society for future extensions. c) The derived work is distributed under terms that allow the compilation of derived works, but keep paragraphs a) and b) intact. The simplest way to do this is to distribute the derived work under the OpenMath license, but this is not a requirement. If you have questions about this license please contact the OpenMath society at http://www.openmath.org.

list
description: This symbol denotes the list construct which is an n-ary function. The list entries must be given explicitly.
example: Application
  arguments: Literal
    value: The list 3, 6, 9.
  arguments: Application
    operator: list
  operator: Example
type: Symbol