OpenMath Content Dictionary: setname2

Canonical URL:

http://www.openmath.org/cd/setname2.ocd

CD File:

setname2.ocd

CD as XML Encoded OpenMath:

setname2.omcd

Defines:

A, AlgebraicExtension, Boolean, GFp, GFpn, H, QuotientField, Zm

Date:

2000-02-02

Version:

3

Review Date:

2003-04-01

Status:

experimental

Uses CD:

alg1, arith1, logic1, polyu, quant1, relation1, setname1, set1, sts

This CD defines some common sets of mathematics.

Written by J.H. Davenport on 1999-04-18.
Revised to add Zm, GFp, GFpn on 1999-11-09.
Revised to add QuotientField and A on 1999-11-19.
AlgebraicExtension added 2003-09-16

Boolean

Description:

This symbol represents the set of Booleans. That is the truth values, true and false.

Commented Mathematical property (CMP):

for all b in the booleans | (there exists an nb in the booleans | nb not= b implies nb = not b)

Formal Mathematical property (FMP):

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
  <OMBIND>
    <OMS cd="quant1" name="forall"/>
    <OMBVAR>
      <OMV name="b"/>
    </OMBVAR>
    <OMA>
      <OMS cd="logic1" name="implies"/>
      <OMA>
	<OMS cd="set1" name="in"/>
	<OMV name="b"/>
	<OMS cd="setname2" name="Boolean"/>
      </OMA>
      <OMBIND>
        <OMS cd="quant1" name="exists"/>
	<OMBVAR>
	  <OMV name="nb"/>
	</OMBVAR>
	<OMA>
	  <OMS cd="logic1" name="and"/>
	  <OMA>
	    <OMS cd="set1" name="in"/>
	    <OMV name="nb"/>
	    <OMS cd="setname2" name="Boolean"/>
	  </OMA>
	  <OMA>
	    <OMS cd="relation1" name="neq"/>
	    <OMV name="nb"/>
	    <OMV name="b"/>
	  </OMA>
	  <OMA>
	    <OMS cd="relation1" name="eq"/>
	    <OMV name="nb"/>
	    <OMA>
	      <OMS cd="logic1" name="not"/>
  	      <OMV name="b"/>
	    </OMA>
	 </OMA>
	</OMA>
      </OMBIND>
    </OMA>
  </OMBIND>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <bind><csymbol cd="quant1">forall</csymbol>
  <bvar><ci>b</ci></bvar>
  <apply><csymbol cd="logic1">implies</csymbol>
   <apply><csymbol cd="set1">in</csymbol><ci>b</ci><csymbol cd="setname2">Boolean</csymbol></apply>
   <bind><csymbol cd="quant1">exists</csymbol>
    <bvar><ci>nb</ci></bvar>
    <apply><csymbol cd="logic1">and</csymbol>
     <apply><csymbol cd="set1">in</csymbol><ci>nb</ci><csymbol cd="setname2">Boolean</csymbol></apply>
     <apply><csymbol cd="relation1">neq</csymbol><ci>nb</ci><ci>b</ci></apply>
     <apply><csymbol cd="relation1">eq</csymbol>
      <ci>nb</ci>
      <apply><csymbol cd="logic1">not</csymbol><ci>b</ci></apply>
     </apply>
    </apply>
   </bind>
  </apply>
 </bind>
</math>

Prefix

forall [ b ] . (implies (in ( b, Boolean) , exists [ nb ] . (and (in ( nb, Boolean) , neq ( nb, b) , eq ( nb, not ( b) ) ) ) ) )

Popcorn

quant1.forall[$b -> set1.in($b, setname2.Boolean) ==> quant1.exists[$nb -> set1.in($nb, setname2.Boolean) and $nb != $b and $nb = not($b)]]

Rendered Presentation MathML

$$\forall \hspace{0.17em}b.b\in \mathrm{Boolean}\Rightarrow \exists \hspace{0.17em}\mathrm{nb}.\mathrm{nb}\in \mathrm{Boolean}\wedge \mathrm{nb}\ne b\wedge \mathrm{nb}=\neg b$$

Signatures:

sts

A

Description:

This symbol represents the set of algebraic numbers.

Commented Mathematical property (CMP):

The algebraic numbers are a proper subset of the reals

Formal Mathematical property (FMP):

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
  <OMA>
    <OMS cd="set1" name="prsubset"/>
    <OMS cd="setname2" name="A"/>
    <OMS cd="setname1" name="R"/>
  </OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="set1">prsubset</csymbol>
  <csymbol cd="setname2">A</csymbol>
  <csymbol cd="setname1">R</csymbol>
 </apply>
</math>

Prefix

prsubset (A, R)

Popcorn

set1.prsubset(setname2.A, setname1.R)

Rendered Presentation MathML

$$A\subset \mathbb{R}$$

Commented Mathematical property (CMP):

The rationals are a proper subset of the algebraic numbers

Formal Mathematical property (FMP):

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
  <OMA>
    <OMS cd="set1" name="prsubset"/>
    <OMS cd="setname1" name="Q"/>
    <OMS cd="setname2" name="A"/>
  </OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="set1">prsubset</csymbol>
  <csymbol cd="setname1">Q</csymbol>
  <csymbol cd="setname2">A</csymbol>
 </apply>
</math>

Prefix

prsubset (Q, A)

Popcorn

set1.prsubset(setname1.Q, setname2.A)

Rendered Presentation MathML

$$\mathbb{Q}\subset A$$

Signatures:

sts

Zm

Description:

This symbol represents the set of integers modulo m, where m is not necessarily a prime. It takes one argument, the integer m.

Commented Mathematical property (CMP):

for all x in the integers modulo m | there exists an n such that n is an integer and n <= m and x^n = x

Formal Mathematical property (FMP):

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
  <OMBIND>
    <OMS cd="quant1" name="forall"/>
    <OMBVAR>
      <OMV name="x"/>
    </OMBVAR>
    <OMA>
      <OMS cd="logic1" name="implies"/>
      <OMA>
        <OMS cd="set1" name="in"/>
	<OMV name="x"/>
	<OMA>
	  <OMS cd="setname2" name="Zm"/>
	  <OMV name="m"/>
	</OMA>
      </OMA>
      <OMBIND>
        <OMS cd="quant1" name="exists"/>
	<OMBVAR>
	  <OMV name="n"/>
	</OMBVAR>
	<OMA>
	  <OMS cd="logic1" name="and"/>
	  <OMA>
	    <OMS cd="set1" name="in"/>
	    <OMV name="n"/>
	    <OMS cd="setname1" name="Z"/>
	  </OMA>
	  <OMA>
	    <OMS cd="relation1" name="leq"/>
	    <OMV name="n"/>
	    <OMV name="m"/>
	  </OMA>
	  <OMA>
	    <OMS cd="relation1" name="eq"/>
	    <OMA>
	      <OMS cd="arith1" name="power"/>
	      <OMV name="x"/>
	      <OMV name="n"/>
	    </OMA>
	    <OMV name="x"/>
	  </OMA>
	</OMA>
      </OMBIND>
    </OMA>
  </OMBIND>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <bind><csymbol cd="quant1">forall</csymbol>
  <bvar><ci>x</ci></bvar>
  <apply><csymbol cd="logic1">implies</csymbol>
   <apply><csymbol cd="set1">in</csymbol>
    <ci>x</ci>
    <apply><csymbol cd="setname2">Zm</csymbol><ci>m</ci></apply>
   </apply>
   <bind><csymbol cd="quant1">exists</csymbol>
    <bvar><ci>n</ci></bvar>
    <apply><csymbol cd="logic1">and</csymbol>
     <apply><csymbol cd="set1">in</csymbol><ci>n</ci><csymbol cd="setname1">Z</csymbol></apply>
     <apply><csymbol cd="relation1">leq</csymbol><ci>n</ci><ci>m</ci></apply>
     <apply><csymbol cd="relation1">eq</csymbol>
      <apply><csymbol cd="arith1">power</csymbol><ci>x</ci><ci>n</ci></apply>
      <ci>x</ci>
     </apply>
    </apply>
   </bind>
  </apply>
 </bind>
</math>

Prefix

forall [ x ] . (implies (in ( x, Zm ( m) ) , exists [ n ] . (and (in ( n, Z) , leq ( n, m) , eq (power ( x, n) , x) ) ) ) )

Popcorn

quant1.forall[$x -> set1.in($x, setname2.Zm($m)) ==> quant1.exists[$n -> set1.in($n, setname1.Z) and $n <= $m and $x ^ $n = $x]]

Rendered Presentation MathML

$$\forall \hspace{0.17em}x.x\in {\mathbb{Z}}_m\Rightarrow \exists \hspace{0.17em}n.n\in \mathbb{Z}\wedge n\le m\wedge x^n=x$$

Example:

The integers mod 12:

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
  <OMA>
    <OMS name="Zm" cd="setname2"/>
    <OMI> 12 </OMI>
  </OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML"><apply><csymbol cd="setname2">Zm</csymbol><cn>12</cn></apply></math>

Prefix

Zm ( 12 )

Popcorn

setname2.Zm(12)

Rendered Presentation MathML

$${\mathbb{Z}}_{12}$$

Example:

The integers mod m:

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
  <OMA>
    <OMS name="Zm" cd="setname2"/>
    <OMV name="m"/>
  </OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML"><apply><csymbol cd="setname2">Zm</csymbol><ci>m</ci></apply></math>

Prefix

Zm ( m)

Popcorn

setname2.Zm($m)

Rendered Presentation MathML

$${\mathbb{Z}}_m$$

Example:

4*5=8 in Z mod 12

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
  <OMA>
    <OMS name="eq" cd="relation1"/>
    <OMA>
      <OMS name="times" cd="arith1"/>
      <OMATTR>
        <OMATP>
          <OMS name="type" cd="sts"/>
          <OMA>
            <OMS name="Zm" cd="setname2"/>
            <OMI> 12 </OMI>
          </OMA>
        </OMATP>
        <OMI> 4 </OMI> 
      </OMATTR>
      <OMATTR>
        <OMATP>
          <OMS name="type" cd="sts"/>
          <OMA>
            <OMS name="Zm" cd="setname2"/>
            <OMI> 12 </OMI>
          </OMA>
        </OMATP>
        <OMI> 5 </OMI> 
      </OMATTR>
    </OMA>
    <OMATTR>
      <OMATP>
        <OMS name="type" cd="sts"/>
        <OMA>
          <OMS name="Zm" cd="setname2"/>
          <OMI> 12 </OMI>
        </OMA>
      </OMATP>
      <OMI> 8 </OMI> 
    </OMATTR>
  </OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="relation1">eq</csymbol>
  <apply><csymbol cd="arith1">times</csymbol>
   <semantics>
    <cn>4</cn>
    <annotation-xml cd="sts" encoding="type"><apply><csymbol cd="setname2">Zm</csymbol><cn>12</cn></apply></annotation-xml>
   </semantics>
   <semantics>
    <cn>5</cn>
    <annotation-xml cd="sts" encoding="type"><apply><csymbol cd="setname2">Zm</csymbol><cn>12</cn></apply></annotation-xml>
   </semantics>
  </apply>
  <semantics>
   <cn>8</cn>
   <annotation-xml cd="sts" encoding="type"><apply><csymbol cd="setname2">Zm</csymbol><cn>12</cn></apply></annotation-xml>
  </semantics>
 </apply>
</math>

Prefix

eq (times (Attrib([ type Zm ( 12 ) ], 4 ) , Attrib([ type Zm ( 12 ) ], 5 ) ) , Attrib([ type Zm ( 12 ) ], 8 ) )

Popcorn

4{sts.type -> setname2.Zm(12)} * 5{sts.type -> setname2.Zm(12)} = 8{sts.type -> setname2.Zm(12)}

Rendered Presentation MathML

$$45=8$$

Signatures:

sts

GFp

Description:

This symbol represents the finite field of integers modulo p, where p is a prime.

Commented Mathematical property (CMP):

x^p = x mod p

Formal Mathematical property (FMP):

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
  <OMA>
    <OMS name="eq" cd="relation1"/>
    <OMA>
      <OMS name="power" cd="arith1"/>
      <OMATTR>
        <OMATP>
          <OMS name="type" cd="sts"/>
          <OMA>
            <OMS name="GFp" cd="setname2"/>
            <OMV name="p"/>
          </OMA>
        </OMATP>
       <OMV name="x"/>
      </OMATTR>
      <OMV name="p"/>
    </OMA>
    <OMATTR>
      <OMATP>
        <OMS name="type" cd="sts"/>
        <OMA>
          <OMS name="GFp" cd="setname2"/>
          <OMV name="p"/>
        </OMA>
      </OMATP>
      <OMV name="x"/>
    </OMATTR>
  </OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="relation1">eq</csymbol>
  <apply><csymbol cd="arith1">power</csymbol>
   <semantics>
    <ci>x</ci>
    <annotation-xml cd="sts" encoding="type"><apply><csymbol cd="setname2">GFp</csymbol><ci>p</ci></apply></annotation-xml>
   </semantics>
   <ci>p</ci>
  </apply>
  <semantics>
   <ci>x</ci>
   <annotation-xml cd="sts" encoding="type"><apply><csymbol cd="setname2">GFp</csymbol><ci>p</ci></apply></annotation-xml>
  </semantics>
 </apply>
</math>

Prefix

eq (power (Attrib([ type GFp ( p) ], x) , p) , Attrib([ type GFp ( p) ], x) )

Popcorn

$x{sts.type -> setname2.GFp($p)} ^ $p = $x{sts.type -> setname2.GFp($p)}

Rendered Presentation MathML

$$x^p=x$$

Signatures:

sts

GFpn

Description:

This symbol represents the finite field with p^n elements, where p is a prime.

Example:

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
  <OMA>
    <OMS name="eq" cd="relation1"/>
    <OMA>
      <OMS name="GFp" cd="setname2"/>
      <OMV name="p"/>
    </OMA>
    <OMA>
      <OMS name="GFpn" cd="setname2"/>
      <OMV name="p"/>
      <OMS name="one" cd="alg1"/>
    </OMA>
  </OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="relation1">eq</csymbol>
  <apply><csymbol cd="setname2">GFp</csymbol><ci>p</ci></apply>
  <apply><csymbol cd="setname2">GFpn</csymbol><ci>p</ci><csymbol cd="alg1">one</csymbol></apply>
 </apply>
</math>

Prefix

eq (GFp ( p) , GFpn ( p, one) )

Popcorn

setname2.GFp($p) = setname2.GFpn($p, alg1.one)

Rendered Presentation MathML

$${\mathbb{GF}}_p={\mathbb{GF}}_{p^1}$$

Signatures:

sts

QuotientField

Description:

This symbol represents the quotient field of any integral domain.

Example:

The rationals equals QuotientField(Integers)

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
<OMA>
  <OMS cd="relation1" name="eq"/>
  <OMS cd="setname1" name="Q"/>
  <OMA>
    <OMS cd="setname2" name="QuotientField"/>
    <OMS cd="setname1" name="Z"/>
  </OMA>
</OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="relation1">eq</csymbol>
  <csymbol cd="setname1">Q</csymbol>
  <apply><csymbol cd="setname2">QuotientField</csymbol><csymbol cd="setname1">Z</csymbol></apply>
 </apply>
</math>

Prefix

eq (Q, QuotientField (Z) )

Popcorn

setname1.Q = setname2.QuotientField(setname1.Z)

Rendered Presentation MathML

$$\mathbb{Q}=\mathrm{QuotientField}\left(\mathbb{Z}\right)$$

Commented Mathematical property (CMP):

R is a field iff QuotientField(R)=R

Formal Mathematical property (FMP):

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
  <OMA>
    <OMS name="equivalent" cd="logic1"/>
    <OMA>
      <OMS name="in" cd="set1"/>
      <OMV name="R"/>
      <OMA>
        <OMS name="structure" cd="sts"/>
        <OMV name="Field"/>
      </OMA>
    </OMA>
    <OMA>
      <OMS name="eq" cd="relation1"/>
      <OMA>
        <OMS name="QuotientField" cd="setname2"/>
        <OMV name="R"/>
      </OMA>
      <OMV name="R"/>
    </OMA>
  </OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="logic1">equivalent</csymbol>
  <apply><csymbol cd="set1">in</csymbol>
   <ci>R</ci>
   <apply><csymbol cd="sts">structure</csymbol><ci>Field</ci></apply>
  </apply>
  <apply><csymbol cd="relation1">eq</csymbol>
   <apply><csymbol cd="setname2">QuotientField</csymbol><ci>R</ci></apply>
   <ci>R</ci>
  </apply>
 </apply>
</math>

Prefix

equivalent (in ( R, structure ( Field) ) , eq (QuotientField ( R) , R) )

Popcorn

logic1.equivalent(set1.in($R, sts.structure($Field)), setname2.QuotientField($R) = $R)

Rendered Presentation MathML

$$R\in \mathrm{structure}\left(\mathrm{Field}\right)\equiv (\mathrm{QuotientField}\left(R\right)=R)$$

Signatures:

sts

AlgebraicExtension

Description:

This symbol represents an algebraic extension of any integral domain.

Example:

The complex numbers are the extension of the reals by a root of x^2+1

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
<OMA>
  <OMS cd="relation1" name="eq"/>
  <OMS cd="setname1" name="C"/>
  <OMA>
    <OMS cd="setname2" name="AlgebraicExtension"/>
    <OMS cd="setname1" name="R"/>
    <OMA>
      <OMS cd="polyu" name="poly_u_rep"/>
      <OMV name="x"/>
      <OMA>
        <OMS cd="polyu" name="term"/> 
	<OMI> 2 </OMI>
	<OMI> 1 </OMI>
      </OMA>
      <OMA>
        <OMS cd="polyu" name="term"/> 
	<OMI> 0 </OMI>
	<OMI> 1 </OMI>
      </OMA>
    </OMA>
  </OMA>
</OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="relation1">eq</csymbol>
  <csymbol cd="setname1">C</csymbol>
  <apply><csymbol cd="setname2">AlgebraicExtension</csymbol>
   <csymbol cd="setname1">R</csymbol>
   <apply><csymbol cd="polyu">poly_u_rep</csymbol>
    <ci>x</ci>
    <apply><csymbol cd="polyu">term</csymbol><cn>2</cn><cn>1</cn></apply>
    <apply><csymbol cd="polyu">term</csymbol><cn>0</cn><cn>1</cn></apply>
   </apply>
  </apply>
 </apply>
</math>

Prefix

eq (C, AlgebraicExtension (R, poly_u_rep ( x, term ( 2 , 1 ) , term ( 0 , 1 ) ) ) )

Popcorn

setname1.C = setname2.AlgebraicExtension(setname1.R, polyu.poly_u_rep($x, polyu.term(2, 1), polyu.term(0, 1)))

Rendered Presentation MathML

$$\mathbb{C}=\mathrm{AlgebraicExtension}(\mathbb{R},\mathrm{poly\_u\_rep}(x,\mathrm{term}(2,1),\mathrm{term}(0,1)))$$

Signatures:

sts

H

Description:

This symbol represents the set of quaternions.

Commented Mathematical property (CMP):

1 is a quaternion and there exists i,j,k s.t. i,j,k are quaternions and i^2 = j^2 = k^2 = ijk = -1 with abs(i) not = abs(j) not = abs(k) not = 1 implies for all q, q a quaternion implies there exists r_0, r_1, r_2, r_3 reals s.t. q = r_0 + r_1*i + r_2*j + r_3*k

Formal Mathematical property (FMP):

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
  <OMA>
    <OMS cd="logic1" name="and"/>
    <OMA>
      <OMS cd="set1" name="in"/>
      <OMS cd="alg1" name="one"/>
      <OMS cd="setname2" name="H"/>
    </OMA>
    <OMBIND>
      <OMS cd="quant1" name="exists"/>
      <OMBVAR>
        <OMV name="i"/>
        <OMV name="j"/>
        <OMV name="k"/>
      </OMBVAR>
      <OMA>
	<OMS cd="logic1" name="and"/>
	<OMA>
	  <OMS cd="set1" name="in"/>
	  <OMV name="i"/>
	  <OMS cd="setname2" name="H"/>
	</OMA>
	<OMA>
	  <OMS cd="set1" name="in"/>
	  <OMV name="j"/>
	  <OMS cd="setname2" name="H"/>
	</OMA>
	<OMA>
	  <OMS cd="set1" name="in"/>
	  <OMV name="k"/>
	  <OMS cd="setname2" name="H"/>
	</OMA>
	<OMA>
	  <OMS cd="relation1" name="eq"/>
	  <OMA>
	    <OMS cd="arith1" name="power"/>
	    <OMV name="i"/>
	    <OMI> 2 </OMI>
	  </OMA>
	  <OMA>
	    <OMS cd="arith1" name="unary_minus"/>
	    <OMS cd="alg1" name="one"/>
	  </OMA>
	</OMA>
	<OMA>
	  <OMS cd="relation1" name="eq"/>
	  <OMA>
	    <OMS cd="arith1" name="power"/>
	    <OMV name="j"/>
	    <OMI> 2 </OMI>
	  </OMA>
	  <OMA>
	    <OMS cd="arith1" name="unary_minus"/>
	    <OMS cd="alg1" name="one"/>
	  </OMA>
	</OMA>
	<OMA>
	  <OMS cd="relation1" name="eq"/>
	  <OMA>
	    <OMS cd="arith1" name="power"/>
	    <OMV name="k"/>
	    <OMI> 2 </OMI>
	  </OMA>
	  <OMA>
	    <OMS cd="arith1" name="unary_minus"/>
	    <OMS cd="alg1" name="one"/>
	  </OMA>
	</OMA>
	<OMA>
	  <OMS cd="relation1" name="eq"/>
	  <OMA>
	    <OMS cd="arith1" name="times"/>
	    <OMV name="i"/>
	    <OMV name="j"/>
	    <OMV name="k"/>
	  </OMA>
	  <OMA>
	    <OMS cd="arith1" name="unary_minus"/>
	    <OMS cd="alg1" name="one"/>
	  </OMA>
	</OMA>
	<OMA>
	  <OMS cd="relation1" name="neq"/>
	  <OMA>
	    <OMS cd="arith1" name="abs"/>
	    <OMV name="i"/>
	  </OMA>
	  <OMS cd="alg1" name="one"/>
	</OMA>
	<OMA>
	  <OMS cd="relation1" name="neq"/>
	  <OMA>
	    <OMS cd="arith1" name="abs"/>
	    <OMV name="j"/>
	  </OMA>
	  <OMS cd="alg1" name="one"/>
	</OMA>
	<OMA>
	  <OMS cd="relation1" name="neq"/>
	  <OMA>
	    <OMS cd="arith1" name="abs"/>
	    <OMV name="k"/>
	  </OMA>
	  <OMS cd="alg1" name="one"/>
	</OMA>
	<OMBIND>
	  <OMS cd="quant1" name="forall"/>
	  <OMBVAR>
	    <OMV name="q"/>
	  </OMBVAR>
	  <OMA>
	    <OMS cd="logic1" name="implies"/>
	    <OMA>
	      <OMS cd="set1" name="in"/>
	      <OMV name="q"/>
	      <OMS cd="setname2" name="H"/>
	    </OMA>
	    <OMBIND>
	      <OMS cd="quant1" name="exists"/>
	      <OMBVAR>
	        <OMV name="r0"/>
	        <OMV name="r1"/>
	        <OMV name="r2"/>
	        <OMV name="r3"/>
	      </OMBVAR>
	      <OMA>
		<OMS cd="logic1" name="and"/>
		<OMA>
		  <OMS cd="set1" name="in"/>
		  <OMV name="r0"/>
		  <OMS cd="setname1" name="R"/>
		</OMA>
		<OMA>
		  <OMS cd="set1" name="in"/>
		  <OMV name="r1"/>
		  <OMS cd="setname1" name="R"/>
		</OMA>
		<OMA>
		  <OMS cd="set1" name="in"/>
		  <OMV name="r2"/>
		  <OMS cd="setname1" name="R"/>
		</OMA>
		<OMA>
		  <OMS cd="set1" name="in"/>
		  <OMV name="r3"/>
		  <OMS cd="setname1" name="R"/>
		</OMA>
	        <OMA>
	          <OMS cd="relation1" name="eq"/>
		  <OMV name="q"/>
		  <OMA>
		    <OMS cd="arith1" name="plus"/>
		    <OMV name="r0"/>
		    <OMA>
		      <OMS cd="arith1" name="times"/>
		      <OMV name="r1"/>
		      <OMV name="i"/>
		    </OMA>
		    <OMA>
		      <OMS cd="arith1" name="times"/>
		      <OMV name="r2"/>
		      <OMV name="j"/>
		    </OMA>
		    <OMA>
		      <OMS cd="arith1" name="times"/>
		      <OMV name="r3"/>
		      <OMV name="k"/>
		    </OMA>
		  </OMA>
	        </OMA>
	      </OMA>
	    </OMBIND>
	  </OMA>
	</OMBIND>
      </OMA>
    </OMBIND>
  </OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="logic1">and</csymbol>
  <apply><csymbol cd="set1">in</csymbol>
   <csymbol cd="alg1">one</csymbol>
   <csymbol cd="setname2">H</csymbol>
  </apply>
  <bind><csymbol cd="quant1">exists</csymbol>
   <bvar><ci>i</ci></bvar>
   <bvar><ci>j</ci></bvar>
   <bvar><ci>k</ci></bvar>
   <apply><csymbol cd="logic1">and</csymbol>
    <apply><csymbol cd="set1">in</csymbol><ci>i</ci><csymbol cd="setname2">H</csymbol></apply>
    <apply><csymbol cd="set1">in</csymbol><ci>j</ci><csymbol cd="setname2">H</csymbol></apply>
    <apply><csymbol cd="set1">in</csymbol><ci>k</ci><csymbol cd="setname2">H</csymbol></apply>
    <apply><csymbol cd="relation1">eq</csymbol>
     <apply><csymbol cd="arith1">power</csymbol><ci>i</ci><cn>2</cn></apply>
     <apply><csymbol cd="arith1">unary_minus</csymbol><csymbol cd="alg1">one</csymbol></apply>
    </apply>
    <apply><csymbol cd="relation1">eq</csymbol>
     <apply><csymbol cd="arith1">power</csymbol><ci>j</ci><cn>2</cn></apply>
     <apply><csymbol cd="arith1">unary_minus</csymbol><csymbol cd="alg1">one</csymbol></apply>
    </apply>
    <apply><csymbol cd="relation1">eq</csymbol>
     <apply><csymbol cd="arith1">power</csymbol><ci>k</ci><cn>2</cn></apply>
     <apply><csymbol cd="arith1">unary_minus</csymbol><csymbol cd="alg1">one</csymbol></apply>
    </apply>
    <apply><csymbol cd="relation1">eq</csymbol>
     <apply><csymbol cd="arith1">times</csymbol><ci>i</ci><ci>j</ci><ci>k</ci></apply>
     <apply><csymbol cd="arith1">unary_minus</csymbol><csymbol cd="alg1">one</csymbol></apply>
    </apply>
    <apply><csymbol cd="relation1">neq</csymbol>
     <apply><csymbol cd="arith1">abs</csymbol><ci>i</ci></apply>
     <csymbol cd="alg1">one</csymbol>
    </apply>
    <apply><csymbol cd="relation1">neq</csymbol>
     <apply><csymbol cd="arith1">abs</csymbol><ci>j</ci></apply>
     <csymbol cd="alg1">one</csymbol>
    </apply>
    <apply><csymbol cd="relation1">neq</csymbol>
     <apply><csymbol cd="arith1">abs</csymbol><ci>k</ci></apply>
     <csymbol cd="alg1">one</csymbol>
    </apply>
    <bind><csymbol cd="quant1">forall</csymbol>
     <bvar><ci>q</ci></bvar>
     <apply><csymbol cd="logic1">implies</csymbol>
      <apply><csymbol cd="set1">in</csymbol><ci>q</ci><csymbol cd="setname2">H</csymbol></apply>
      <bind><csymbol cd="quant1">exists</csymbol>
       <bvar><ci>r0</ci></bvar>
       <bvar><ci>r1</ci></bvar>
       <bvar><ci>r2</ci></bvar>
       <bvar><ci>r3</ci></bvar>
       <apply><csymbol cd="logic1">and</csymbol>
        <apply><csymbol cd="set1">in</csymbol><ci>r0</ci><csymbol cd="setname1">R</csymbol></apply>
        <apply><csymbol cd="set1">in</csymbol><ci>r1</ci><csymbol cd="setname1">R</csymbol></apply>
        <apply><csymbol cd="set1">in</csymbol><ci>r2</ci><csymbol cd="setname1">R</csymbol></apply>
        <apply><csymbol cd="set1">in</csymbol><ci>r3</ci><csymbol cd="setname1">R</csymbol></apply>
        <apply><csymbol cd="relation1">eq</csymbol>
         <ci>q</ci>
         <apply><csymbol cd="arith1">plus</csymbol>
          <ci>r0</ci>
          <apply><csymbol cd="arith1">times</csymbol><ci>r1</ci><ci>i</ci></apply>
          <apply><csymbol cd="arith1">times</csymbol><ci>r2</ci><ci>j</ci></apply>
          <apply><csymbol cd="arith1">times</csymbol><ci>r3</ci><ci>k</ci></apply>
         </apply>
        </apply>
       </apply>
      </bind>
     </apply>
    </bind>
   </apply>
  </bind>
 </apply>
</math>

Prefix

and (in (one, H) , exists [ i j k ] . (and (in ( i, H) , in ( j, H) , in ( k, H) , eq (power ( i, 2 ) , unary_minus (one) ) , eq (power ( j, 2 ) , unary_minus (one) ) , eq (power ( k, 2 ) , unary_minus (one) ) , eq (times ( i, j, k) , unary_minus (one) ) , neq (abs ( i) , one) , neq (abs ( j) , one) , neq (abs ( k) , one) , forall [ q ] . (implies (in ( q, H) , exists [ r0 r1 r2 r3 ] . (and (in ( r0, R) , in ( r1, R) , in ( r2, R) , in ( r3, R) , eq ( q, plus ( r0, times ( r1, i) , times ( r2, j) , times ( r3, k) ) ) ) ) ) ) ) ) )

Popcorn

set1.in(alg1.one, setname2.H) and quant1.exists[$i, $j, $k -> set1.in($i, setname2.H) and set1.in($j, setname2.H) and set1.in($k, setname2.H) and $i ^ 2 = -(alg1.one) and $j ^ 2 = -(alg1.one) and $k ^ 2 = -(alg1.one) and $i * $j * $k = -(alg1.one) and arith1.abs($i) != alg1.one and arith1.abs($j) != alg1.one and arith1.abs($k) != alg1.one and quant1.forall[$q -> set1.in($q, setname2.H) ==> quant1.exists[$r0, $r1, $r2, $r3 -> set1.in($r0, setname1.R) and set1.in($r1, setname1.R) and set1.in($r2, setname1.R) and set1.in($r3, setname1.R) and $q = $r0 + $r1 * $i + $r2 * $j + $r3 * $k]]]

Rendered Presentation MathML

$$1\in \mathbb{H}\wedge \exists \hspace{0.17em}i,j,k.i\in \mathbb{H}\wedge j\in \mathbb{H}\wedge k\in \mathbb{H}\wedge i^2=-1\wedge j^2=-1\wedge k^2=-1\wedge ijk=-1\wedge \left|i\right|\ne 1\wedge \left|j\right|\ne 1\wedge \left|k\right|\ne 1\wedge \forall \hspace{0.17em}q.q\in \mathbb{H}\Rightarrow \exists \hspace{0.17em}{r}_0,r_1,r_2,r_3.r_0\in \mathbb{R}\wedge r_1\in \mathbb{R}\wedge r_2\in \mathbb{R}\wedge r_3\in \mathbb{R}\wedge q=r_0+r_{1}i+r_{2}j+r_{3}k$$

Example:

There exists a,b in the quaternions s.t. a*b neq b*a

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
  <OMBIND>
    <OMS cd="quant1" name="exists"/>
    <OMBVAR>
      <OMV name="a"/>
      <OMV name="b"/>
    </OMBVAR>
    <OMA>
      <OMS cd="relation1" name="neq"/>
      <OMA>
        <OMS cd="arith1" name="times"/>
	<OMV name="a"/>
	<OMV name="b"/>
      </OMA>
      <OMA>
        <OMS cd="arith1" name="times"/>
	<OMV name="b"/>
	<OMV name="a"/>
      </OMA>
    </OMA>
  </OMBIND>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <bind><csymbol cd="quant1">exists</csymbol>
  <bvar><ci>a</ci></bvar>
  <bvar><ci>b</ci></bvar>
  <apply><csymbol cd="relation1">neq</csymbol>
   <apply><csymbol cd="arith1">times</csymbol><ci>a</ci><ci>b</ci></apply>
   <apply><csymbol cd="arith1">times</csymbol><ci>b</ci><ci>a</ci></apply>
  </apply>
 </bind>
</math>

Prefix

exists [ a b ] . (neq (times ( a, b) , times ( b, a) ) )

Popcorn

quant1.exists[$a, $b -> $a * $b != $b * $a]

Rendered Presentation MathML

$$\exists \hspace{0.17em}a,b.ab\ne ba$$

Signatures:

sts