OpenMath Content Dictionary: relation3

Canonical URL:

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

CD Base:

http://www.openmath.org/cd

CD File:

relation3.ocd

CD as XML Encoded OpenMath:

relation3.omcd

Defines:

class, is_equivalence, is_relation, is_symmetric, is_transitive, classes, equivalence_closure, is_reflexive, reflexive_closure, symmetric_closure, transitive_closure

Date:

2001-03-12

Version:

2

Review Date:

2003-04-01

Status:

official

Uses CD:

arith1, logic1, nums1, set1, relation1

This CD holds the basic equivalence relation notions.

is_relation

Description:

This symbol is a boolean function of two arguments, S and R. The first argument should be a set. When applied to S and R, the function returns true if and only if the second argument is a subset of the Cartesian product of S with itself.

Commented Mathematical property (CMP):

R a subset of S x S if and only if is_relation (S,R).

Formal Mathematical property (FMP):

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
<OMA><OMS cd="logic1" name="equivalent"/>
     <OMA><OMS cd="set1" name="subset"/>
          <OMV name="R"/>
          <OMA><OMS cd="set1" name="cartesian_product"/>
               <OMV name="S"/>
          </OMA>
     </OMA>
     <OMA><OMS cd="relation3" name="is_relation"/>
          <OMV name="S"/>
          <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">subset</csymbol>
   <ci>R</ci>
   <apply><csymbol cd="set1">cartesian_product</csymbol><ci>S</ci></apply>
  </apply>
  <apply><csymbol cd="relation3">is_relation</csymbol><ci>S</ci><ci>R</ci></apply>
 </apply>
</math>

Prefix

equivalent (subset ( R, cartesian_product ( S) ) , is_relation ( S, R) )

Popcorn

logic1.equivalent(set1.subset($R, set1.cartesian_product($S)), relation3.is_relation($S, $R))

Rendered Presentation MathML

$$R\subset S\equiv \mathrm{is\_relation}(S,R)$$

Signatures:

sts

equivalence_closure

Description:

This symbol represents a binary function whose first argument is a set S, whose second argument is a relation R on S. When applied to S and R, it represents the smallest equivalence relation (with respect to inclusion) on S containing R.

Signatures:

sts

transitive_closure

Description:

This symbol represents a binary function whose first argument is a set S, whose second argument is a relation R on S. When applied to S and R, it represents the smallest transitive relation (with respect to inclusion) on S containing R.

Signatures:

sts

reflexive_closure

Description:

This symbol represents a binary function whose first argument is a set S, whose second argument is a relation R on S. When applied to S and R, it represents the smallest reflexive relation (with respect to inclusion) on S containing R.

Signatures:

sts

symmetric_closure

Description:

This symbol represents a binary function whose first argument is a set S, whose second argument is a relation R on S. When applied to S and R, it represents the smallest symmetric relation (with respect to inclusion) on S containing R.

Signatures:

sts

is_transitive

Description:

This symbol represents the boolean binary function which returns true if and only if the second argument is a transitive relation on the first.

Commented Mathematical property (CMP):

R is transitive on S if and only if, for all a,b,c in S with (a,b) in R and (b,c) in R, wehave (a,c) in R.

Formal Mathematical property (FMP):

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
<OMA><OMS cd="logic1" name="equivalent"/>
     <OMA><OMS cd="relation3" name="is_transitive"/>
          <OMV name="S"/>    <OMV name="R"/>
     </OMA>
     <OMBIND><OMS cd="quant1" name="forall"/>
          <OMBVAR> <OMV name="a"/> <OMV name="b"/><OMV name="c"/>
          </OMBVAR>
          <OMA><OMS cd="logic1" name="implies"/>
               <OMA><OMS cd="logic1" name="and"/>
                    <OMA><OMS cd="set1" name="in"/>
                         <OMV name="a"/>
                         <OMV name="S"/>
                    </OMA>
                    <OMA><OMS cd="set1" name="in"/>
                         <OMV name="b"/>
                         <OMV name="S"/>
                    </OMA>
                    <OMA><OMS cd="set1" name="in"/>
                         <OMV name="c"/>
                         <OMV name="S"/>
                    </OMA>
                    <OMA><OMS cd="set1" name="in"/>
                         <OMA><OMS cd="list1" name="list"/>
                              <OMV name="a"/>  <OMV name="b"/>
                         </OMA>
                         <OMV name="R"/>
                    </OMA>
                    <OMA><OMS cd="set1" name="in"/>
                         <OMA><OMS cd="list1" name="list"/>
                              <OMV name="b"/>  <OMV name="c"/>
                         </OMA>
                         <OMV name="R"/>
                    </OMA>
               </OMA>
               <OMA><OMS cd="set1" name="in"/>
                    <OMA><OMS cd="list1" name="list"/>
                         <OMV name="a"/>  <OMV name="c"/>
                    </OMA>
                    <OMV name="R"/>
               </OMA>
          </OMA>
    </OMBIND>
</OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="logic1">equivalent</csymbol>
  <apply><csymbol cd="relation3">is_transitive</csymbol><ci>S</ci><ci>R</ci></apply>
  <bind><csymbol cd="quant1">forall</csymbol>
   <bvar><ci>a</ci></bvar>
   <bvar><ci>b</ci></bvar>
   <bvar><ci>c</ci></bvar>
   <apply><csymbol cd="logic1">implies</csymbol>
    <apply><csymbol cd="logic1">and</csymbol>
     <apply><csymbol cd="set1">in</csymbol><ci>a</ci><ci>S</ci></apply>
     <apply><csymbol cd="set1">in</csymbol><ci>b</ci><ci>S</ci></apply>
     <apply><csymbol cd="set1">in</csymbol><ci>c</ci><ci>S</ci></apply>
     <apply><csymbol cd="set1">in</csymbol>
      <apply><csymbol cd="list1">list</csymbol><ci>a</ci><ci>b</ci></apply>
      <ci>R</ci>
     </apply>
     <apply><csymbol cd="set1">in</csymbol>
      <apply><csymbol cd="list1">list</csymbol><ci>b</ci><ci>c</ci></apply>
      <ci>R</ci>
     </apply>
    </apply>
    <apply><csymbol cd="set1">in</csymbol>
     <apply><csymbol cd="list1">list</csymbol><ci>a</ci><ci>c</ci></apply>
     <ci>R</ci>
    </apply>
   </apply>
  </bind>
 </apply>
</math>

Prefix

equivalent (is_transitive ( S, R) , forall [ a b c ] . (implies (and (in ( a, S) , in ( b, S) , in ( c, S) , in (list ( a, b) , R) , in (list ( b, c) , R) ) , in (list ( a, c) , R) ) ) )

Popcorn

logic1.equivalent(relation3.is_transitive($S, $R), quant1.forall[$a, $b, $c -> set1.in($a, $S) and set1.in($b, $S) and set1.in($c, $S) and set1.in([$a , $b], $R) and set1.in([$b , $c], $R) ==> set1.in([$a , $c], $R)])

Rendered Presentation MathML

$$\mathrm{is\_transitive}(S,R)\equiv \forall \hspace{0.17em}a,b,c.a\in S\wedge b\in S\wedge c\in S\wedge (a,b)\in R\wedge (b,c)\in R\Rightarrow (a,c)\in R$$

Signatures:

sts

is_reflexive

Description:

This symbol represents the boolean binary function which returns true if and only if the second argument is a reflexive relation on the first.

Commented Mathematical property (CMP):

is_reflexive(S,R) if and only if, for all, a in S, we have (a,a) in R.

Formal Mathematical property (FMP):

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
<OMA><OMS cd="logic1" name="equivalent"/>
     <OMA><OMS cd="relation3" name="is_reflexive"/>
          <OMV name="S"/>    <OMV name="R"/>
     </OMA>
     <OMBIND><OMS cd="quant1" name="forall"/>
          <OMBVAR> <OMV name="a"/>
          </OMBVAR>
          <OMA><OMS cd="logic1" name="implies"/>
               <OMA><OMS cd="set1" name="in"/>
                    <OMV name="a"/>
                    <OMV name="S"/>
              </OMA>
              <OMA><OMS cd="set1" name="set"/>
                   <OMA><OMS cd="list1" name="list"/>
                        <OMV name="a"/>  <OMV name="a"/>
                   </OMA>
                   <OMV name="R"/>
              </OMA>
         </OMA>
    </OMBIND>
</OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="logic1">equivalent</csymbol>
  <apply><csymbol cd="relation3">is_reflexive</csymbol><ci>S</ci><ci>R</ci></apply>
  <bind><csymbol cd="quant1">forall</csymbol>
   <bvar><ci>a</ci></bvar>
   <apply><csymbol cd="logic1">implies</csymbol>
    <apply><csymbol cd="set1">in</csymbol><ci>a</ci><ci>S</ci></apply>
    <apply><csymbol cd="set1">set</csymbol>
     <apply><csymbol cd="list1">list</csymbol><ci>a</ci><ci>a</ci></apply>
     <ci>R</ci>
    </apply>
   </apply>
  </bind>
 </apply>
</math>

Prefix

equivalent (is_reflexive ( S, R) , forall [ a ] . (implies (in ( a, S) , set (list ( a, a) , R) ) ) )

Popcorn

logic1.equivalent(relation3.is_reflexive($S, $R), quant1.forall[$a -> set1.in($a, $S) ==> {[$a , $a] , $R}])

Rendered Presentation MathML

$$\mathrm{is\_reflexive}(S,R)\equiv \forall \hspace{0.17em}a.a\in S\Rightarrow \{(a,a),R\}$$

Signatures:

sts

is_symmetric

Description:

This symbol represents the boolean binary function which returns true if and only if the second argument is a symmetric relation on the first.

Commented Mathematical property (CMP):

is_symmetric(S,R) if and only if, for all a, b in S with (a,b) in R, we have (b,a) in R.

Formal Mathematical property (FMP):

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
<OMA><OMS cd="logic1" name="equivalent"/>
     <OMA><OMS cd="relation3" name="is_symmetric"/>
          <OMV name="S"/>    <OMV name="R"/>
     </OMA>
     <OMBIND><OMS cd="quant1" name="forall"/>
          <OMBVAR> <OMV name="a"/> <OMV name="b"/>
          </OMBVAR>
          <OMA><OMS cd="logic1" name="implies"/>
               <OMA><OMS cd="logic1" name="and"/>
                    <OMA><OMS cd="set1" name="in"/>
                         <OMV name="a"/>
                         <OMV name="S"/>
                    </OMA>
                    <OMA><OMS cd="set1" name="in"/>
                         <OMV name="b"/>
                         <OMV name="S"/>
                    </OMA>
                    <OMA><OMS cd="set1" name="in"/>
                         <OMA><OMS cd="list1" name="list"/>
                              <OMV name="a"/>  <OMV name="b"/>
                         </OMA>
                         <OMV name="R"/>
                    </OMA>
               </OMA>
               <OMA><OMS cd="set1" name="in"/>
                    <OMA><OMS cd="list1" name="list"/>
                         <OMV name="b"/>  <OMV name="a"/>
                    </OMA>
                    <OMV name="R"/>
               </OMA>
          </OMA>
    </OMBIND>
</OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="logic1">equivalent</csymbol>
  <apply><csymbol cd="relation3">is_symmetric</csymbol><ci>S</ci><ci>R</ci></apply>
  <bind><csymbol cd="quant1">forall</csymbol>
   <bvar><ci>a</ci></bvar>
   <bvar><ci>b</ci></bvar>
   <apply><csymbol cd="logic1">implies</csymbol>
    <apply><csymbol cd="logic1">and</csymbol>
     <apply><csymbol cd="set1">in</csymbol><ci>a</ci><ci>S</ci></apply>
     <apply><csymbol cd="set1">in</csymbol><ci>b</ci><ci>S</ci></apply>
     <apply><csymbol cd="set1">in</csymbol>
      <apply><csymbol cd="list1">list</csymbol><ci>a</ci><ci>b</ci></apply>
      <ci>R</ci>
     </apply>
    </apply>
    <apply><csymbol cd="set1">in</csymbol>
     <apply><csymbol cd="list1">list</csymbol><ci>b</ci><ci>a</ci></apply>
     <ci>R</ci>
    </apply>
   </apply>
  </bind>
 </apply>
</math>

Prefix

equivalent (is_symmetric ( S, R) , forall [ a b ] . (implies (and (in ( a, S) , in ( b, S) , in (list ( a, b) , R) ) , in (list ( b, a) , R) ) ) )

Popcorn

logic1.equivalent(relation3.is_symmetric($S, $R), quant1.forall[$a, $b -> set1.in($a, $S) and set1.in($b, $S) and set1.in([$a , $b], $R) ==> set1.in([$b , $a], $R)])

Rendered Presentation MathML

$$\mathrm{is\_symmetric}(S,R)\equiv \forall \hspace{0.17em}a,b.a\in S\wedge b\in S\wedge (a,b)\in R\Rightarrow (b,a)\in R$$

Signatures:

sts

is_equivalence

Description:

This symbol represents the boolean binary function which returns true if and only if the second argument is a symmetric relation on the first.

Commented Mathematical property (CMP):

R is an equivalence relation on S if and only if R is a symmetric, reflexive, transitive relation on S.

Formal Mathematical property (FMP):

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
<OMA><OMS cd="logic1" name="equivalent"/>
     <OMA><OMS cd="relation3" name="is_symmetric"/>
          <OMV name="S"/>    <OMV name="R"/>
     </OMA>
     <OMA><OMS cd="logic1" name="and"/>
          <OMA><OMS cd="relation3" name="is_relation"/>
               <OMV name="S"/>    <OMV name="R"/>
          </OMA>
          <OMA><OMS cd="relation3" name="is_symmetric"/>
               <OMV name="S"/>    <OMV name="R"/>
          </OMA>
          <OMA><OMS cd="relation3" name="is_reflexive"/>
               <OMV name="S"/>    <OMV name="R"/>
          </OMA>
          <OMA><OMS cd="relation3" name="is_transitive"/>
               <OMV name="S"/>    <OMV name="R"/>
          </OMA>
     </OMA>
</OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="logic1">equivalent</csymbol>
  <apply><csymbol cd="relation3">is_symmetric</csymbol><ci>S</ci><ci>R</ci></apply>
  <apply><csymbol cd="logic1">and</csymbol>
   <apply><csymbol cd="relation3">is_relation</csymbol><ci>S</ci><ci>R</ci></apply>
   <apply><csymbol cd="relation3">is_symmetric</csymbol><ci>S</ci><ci>R</ci></apply>
   <apply><csymbol cd="relation3">is_reflexive</csymbol><ci>S</ci><ci>R</ci></apply>
   <apply><csymbol cd="relation3">is_transitive</csymbol><ci>S</ci><ci>R</ci></apply>
  </apply>
 </apply>
</math>

Prefix

equivalent (is_symmetric ( S, R) , and (is_relation ( S, R) , is_symmetric ( S, R) , is_reflexive ( S, R) , is_transitive ( S, R) ) )

Popcorn

logic1.equivalent(relation3.is_symmetric($S, $R), relation3.is_relation($S, $R) and relation3.is_symmetric($S, $R) and relation3.is_reflexive($S, $R) and relation3.is_transitive($S, $R))

Rendered Presentation MathML

$$\mathrm{is\_symmetric}(S,R)\equiv (\mathrm{is\_relation}(S,R)\wedge \mathrm{is\_symmetric}(S,R)\wedge \mathrm{is\_reflexive}(S,R)\wedge \mathrm{is\_transitive}(S,R))$$

Signatures:

sts

class

Description:

This symbol represents a ternary function whose first argument is a set S, whose second argument is a relation R on S, and whose third argument is an element a of S. When applied to S, R, and a, it represents the set of all elements in S related to a by R, that is, the set {b in S | (a,b) in R}.

Commented Mathematical property (CMP):

class(S,R,a) = {b in S | (a,b) in R}.

Formal Mathematical property (FMP):

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
<OMA><OMS cd="relation1" name="eq"/>
     <OMA><OMS cd="relation3" name="class"/>
          <OMV name="S"/>    <OMV name="R"/> <OMV name="a"/>
     </OMA>
     <OMA><OMS cd="set1" name="suchthat"/>
          <OMV name="S"/>
          <OMBIND><OMS cd="fns1" name="lambda"/>
               <OMBVAR> <OMV name="b"/></OMBVAR>
               <OMA><OMS cd="set1" name="in"/>
                    <OMA><OMS cd="list1" name="list"/>
                         <OMV name="a"/>  <OMV name="b"/>
                    </OMA>
                    <OMV name="R"/>
               </OMA>
          </OMBIND>
     </OMA>
</OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="relation1">eq</csymbol>
  <apply><csymbol cd="relation3">class</csymbol><ci>S</ci><ci>R</ci><ci>a</ci></apply>
  <apply><csymbol cd="set1">suchthat</csymbol>
   <ci>S</ci>
   <bind><csymbol cd="fns1">lambda</csymbol>
    <bvar><ci>b</ci></bvar>
    <apply><csymbol cd="set1">in</csymbol>
     <apply><csymbol cd="list1">list</csymbol><ci>a</ci><ci>b</ci></apply>
     <ci>R</ci>
    </apply>
   </bind>
  </apply>
 </apply>
</math>

Prefix

eq (class ( S, R, a) , suchthat ( S, lambda [ b] . (in (list ( a, b) , R) ) ) )

Popcorn

relation3.class($S, $R, $a) = set1.suchthat($S, fns1.lambda[$b -> set1.in([$a , $b], $R)])

Rendered Presentation MathML

$$\mathrm{class}(S,R,a)=\left\{b\in S\right|(a,b)\in R\}$$

Signatures:

sts

classes

Description:

This symbol represents a binary function whose first argument is a set S, whose second argument is a relation R on S. When applied to S and R, it represents the set of all elements in S of the form class(S,R,a) for a in S.

Commented Mathematical property (CMP):

The classes of an equivalence relation R on S partition S.

Formal Mathematical property (FMP):

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
<OMA><OMS cd="logic1" name="implies"/>
     <OMA><OMS cd="relation3" name="is_equivalence"/>
          <OMV name="S"/>    <OMV name="R"/> 
     </OMA>
     <OMBIND><OMS cd="quant1" name="forall"/>
          <OMBVAR> <OMV name="a"/> <OMV name="b"/></OMBVAR>
          <OMA><OMS cd="logic1" name="implies"/>
               <OMA><OMS cd="set1" name="in"/>
                    <OMA><OMS cd="list1" name="list"/>
                         <OMV name="a"/>  <OMV name="b"/>
                    </OMA>
                    <OMA><OMS cd="set1" name="cartesian_product"/>
                         <OMV name="S"/>  <OMV name="S"/>
                    </OMA>
               </OMA>
               <OMA><OMS cd="logic1" name="or"/>
                    <OMA><OMS cd="relation1" name="eq"/>
                         <OMA><OMS cd="set1" name="intersect"/>
                              <OMA><OMS cd="relation3" name="class"/>
                                   <OMV name="S"/><OMV name="R"/><OMV name="a"/>
                              </OMA>
                              <OMA><OMS cd="relation3" name="class"/>
                                   <OMV name="S"/>  <OMV name="R"/>  <OMV name="b"/>
                              </OMA>
                         </OMA>
                         <OMS cd="set1" name="emptyset"/>
                    </OMA>

                    <OMA><OMS cd="relation1" name="eq"/>
                         <OMA><OMS cd="relation3" name="class"/>
                              <OMV name="S"/><OMV name="R"/><OMV name="a"/>
                         </OMA>
                         <OMA><OMS cd="relation3" name="class"/>
                              <OMV name="S"/>  <OMV name="R"/>  <OMV name="b"/>
                         </OMA>
                    </OMA>
               </OMA>
          </OMA>
     </OMBIND>
 </OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="logic1">implies</csymbol>
  <apply><csymbol cd="relation3">is_equivalence</csymbol><ci>S</ci><ci>R</ci></apply>
  <bind><csymbol cd="quant1">forall</csymbol>
   <bvar><ci>a</ci></bvar>
   <bvar><ci>b</ci></bvar>
   <apply><csymbol cd="logic1">implies</csymbol>
    <apply><csymbol cd="set1">in</csymbol>
     <apply><csymbol cd="list1">list</csymbol><ci>a</ci><ci>b</ci></apply>
     <apply><csymbol cd="set1">cartesian_product</csymbol><ci>S</ci><ci>S</ci></apply>
    </apply>
    <apply><csymbol cd="logic1">or</csymbol>
     <apply><csymbol cd="relation1">eq</csymbol>
      <apply><csymbol cd="set1">intersect</csymbol>
       <apply><csymbol cd="relation3">class</csymbol><ci>S</ci><ci>R</ci><ci>a</ci></apply>
       <apply><csymbol cd="relation3">class</csymbol><ci>S</ci><ci>R</ci><ci>b</ci></apply>
      </apply>
      <csymbol cd="set1">emptyset</csymbol>
     </apply>
     <apply><csymbol cd="relation1">eq</csymbol>
      <apply><csymbol cd="relation3">class</csymbol><ci>S</ci><ci>R</ci><ci>a</ci></apply>
      <apply><csymbol cd="relation3">class</csymbol><ci>S</ci><ci>R</ci><ci>b</ci></apply>
     </apply>
    </apply>
   </apply>
  </bind>
 </apply>
</math>

Prefix

implies (is_equivalence ( S, R) , forall [ a b] . (implies (in (list ( a, b) , cartesian_product ( S, S) ) , or (eq (intersect (class ( S, R, a) , class ( S, R, b) ) , emptyset) , eq (class ( S, R, a) , class ( S, R, b) ) ) ) ) )

Popcorn

relation3.is_equivalence($S, $R) ==> quant1.forall[$a, $b -> set1.in([$a , $b], set1.cartesian_product($S, $S)) ==> set1.intersect(relation3.class($S, $R, $a), relation3.class($S, $R, $b)) = set1.emptyset > relation3.class($S, $R, $a) = relation3.class($S, $R, $b)]

Rendered Presentation MathML

$$\mathrm{is\_equivalence}(S,R)\Rightarrow \forall \hspace{0.17em}a,b.(a,b)\in S\times S\Rightarrow (\mathrm{class}(S,R,a)\cap \mathrm{class}(S,R,b)=\varnothing )\vee (\mathrm{class}(S,R,a)=\mathrm{class}(S,R,b))$$

Commented Mathematical property (CMP):

The classes of a reflexive relation R on S cover S, as a in S belongs to class(S,R,a).

Formal Mathematical property (FMP):

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
<OMA><OMS cd="logic1" name="implies"/>
     <OMA><OMS cd="relation3" name="is_reflexive"/>
          <OMV name="S"/>    <OMV name="R"/> 
     </OMA>
     <OMBIND><OMS cd="quant1" name="forall"/>
          <OMBVAR> <OMV name="a"/></OMBVAR>
          <OMA><OMS cd="logic1" name="implies"/>
               <OMA><OMS cd="set1" name="in"/>
                    <OMV name="a"/> <OMV name="S"/> 
               </OMA>
               <OMA><OMS cd="set1" name="in"/>
                    <OMV name="a"/>
                    <OMA><OMS cd="relation3" name="class"/>
                         <OMV name="S"/><OMV name="R"/><OMV name="a"/>
                    </OMA>
               </OMA>
          </OMA>
     </OMBIND>
 </OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="logic1">implies</csymbol>
  <apply><csymbol cd="relation3">is_reflexive</csymbol><ci>S</ci><ci>R</ci></apply>
  <bind><csymbol cd="quant1">forall</csymbol>
   <bvar><ci>a</ci></bvar>
   <apply><csymbol cd="logic1">implies</csymbol>
    <apply><csymbol cd="set1">in</csymbol><ci>a</ci><ci>S</ci></apply>
    <apply><csymbol cd="set1">in</csymbol>
     <ci>a</ci>
     <apply><csymbol cd="relation3">class</csymbol><ci>S</ci><ci>R</ci><ci>a</ci></apply>
    </apply>
   </apply>
  </bind>
 </apply>
</math>

Prefix

implies (is_reflexive ( S, R) , forall [ a] . (implies (in ( a, S) , in ( a, class ( S, R, a) ) ) ) )

Popcorn

relation3.is_reflexive($S, $R) ==> quant1.forall[$a -> set1.in($a, $S) ==> set1.in($a, relation3.class($S, $R, $a))]

Rendered Presentation MathML

$$\mathrm{is\_reflexive}(S,R)\Rightarrow \forall \hspace{0.17em}a.a\in S\Rightarrow a\in \mathrm{class}(S,R,a)$$

Signatures:

sts