ag-gipp/GoUldI

<math 
  xmlns="http://www.w3.org/1998/Math/MathML" display="block" alttext="for-all x for-all y upper P left-parenthesis x comma y right-parenthesis left right double arrow for-all y for-all x upper P left-parenthesis x comma y right-parenthesis">
  <semantics>
    <mrow data-semantic-type="relseq" data-semantic-role="arrow" data-semantic-id="45" data-semantic-children="44,34" data-semantic-content="10">
      <mrow data-semantic-type="appl" data-semantic-role="prefix function" data-semantic-id="44" data-semantic-children="0,42" data-semantic-content="43" data-semantic-parent="45">
        <mi mathvariant="normal" data-semantic-type="prefixop" data-semantic-role="prefix function" data-semantic-font="normal" data-semantic-id="0" data-semantic-parent="44">∀
          <!-- ∀ -->
        </mi>
        <mo data-semantic-type="punctuation" data-semantic-role="application" data-semantic-id="43" data-semantic-parent="44" data-semantic-added="true" data-semantic-operator="appl">⁡</mo>
        <mrow data-semantic-type="infixop" data-semantic-role="implicit" data-semantic-id="42" data-semantic-children="1,40" data-semantic-content="41" data-semantic-parent="44">
          <mi data-semantic-type="identifier" data-semantic-role="latinletter" data-semantic-font="italic" data-semantic-id="1" data-semantic-parent="42">x</mi>
          <mspace width="thinmathspace"/>
          <mo data-semantic-type="operator" data-semantic-role="multiplication" data-semantic-id="41" data-semantic-parent="42" data-semantic-added="true" data-semantic-operator="infixop,⁢">⁢</mo>
          <mrow data-semantic-type="appl" data-semantic-role="prefix function" data-semantic-id="40" data-semantic-children="2,38" data-semantic-content="39" data-semantic-parent="42">
            <mi mathvariant="normal" data-semantic-type="prefixop" data-semantic-role="prefix function" data-semantic-font="normal" data-semantic-id="2" data-semantic-parent="40">∀
              <!-- ∀ -->
            </mi>
            <mo data-semantic-type="punctuation" data-semantic-role="application" data-semantic-id="39" data-semantic-parent="40" data-semantic-added="true" data-semantic-operator="appl">⁡</mo>
            <mrow data-semantic-type="infixop" data-semantic-role="implicit" data-semantic-id="38" data-semantic-children="3,36" data-semantic-content="37" data-semantic-parent="40">
              <mi data-semantic-type="identifier" data-semantic-role="latinletter" data-semantic-font="italic" data-semantic-id="3" data-semantic-parent="38">y</mi>
              <mspace width="thinmathspace"/>
              <mo data-semantic-type="operator" data-semantic-role="multiplication" data-semantic-id="37" data-semantic-parent="38" data-semantic-added="true" data-semantic-operator="infixop,⁢">⁢</mo>
              <mrow data-semantic-type="appl" data-semantic-role="simple function" data-semantic-id="36" data-semantic-children="4,22" data-semantic-content="35,4" data-semantic-parent="38">
                <mi data-semantic-type="identifier" data-semantic-role="simple function" data-semantic-font="italic" data-semantic-id="4" data-semantic-parent="36" data-semantic-operator="appl">P</mi>
                <mo data-semantic-type="punctuation" data-semantic-role="application" data-semantic-id="35" data-semantic-parent="36" data-semantic-added="true" data-semantic-operator="appl">⁡</mo>
                <mrow data-semantic-type="fenced" data-semantic-role="leftright" data-semantic-id="22" data-semantic-children="21" data-semantic-content="5,9" data-semantic-parent="36">
                  <mo stretchy="false" data-semantic-type="fence" data-semantic-role="open" data-semantic-id="5" data-semantic-parent="22" data-semantic-operator="fenced">(</mo>
                  <mrow data-semantic-type="punctuated" data-semantic-role="sequence" data-semantic-id="21" data-semantic-children="6,7,8" data-semantic-content="7" data-semantic-parent="22">
                    <mi data-semantic-type="identifier" data-semantic-role="latinletter" data-semantic-font="italic" data-semantic-id="6" data-semantic-parent="21">x</mi>
                    <mo data-semantic-type="punctuation" data-semantic-role="comma" data-semantic-id="7" data-semantic-parent="21" data-semantic-operator="punctuated">,</mo>
                    <mi data-semantic-type="identifier" data-semantic-role="latinletter" data-semantic-font="italic" data-semantic-id="8" data-semantic-parent="21">y</mi>
                  </mrow>
                  <mo stretchy="false" data-semantic-type="fence" data-semantic-role="close" data-semantic-id="9" data-semantic-parent="22" data-semantic-operator="fenced">)</mo>
                </mrow>
              </mrow>
            </mrow>
          </mrow>
        </mrow>
      </mrow>
      <mo stretchy="false" data-semantic-type="relation" data-semantic-role="arrow" data-semantic-id="10" data-semantic-parent="45" data-semantic-operator="relseq,⇔">⇔
        <!-- ⇔ -->
      </mo>
      <mrow data-semantic-type="appl" data-semantic-role="prefix function" data-semantic-id="34" data-semantic-children="11,32" data-semantic-content="33" data-semantic-parent="45">
        <mi mathvariant="normal" data-semantic-type="prefixop" data-semantic-role="prefix function" data-semantic-font="normal" data-semantic-id="11" data-semantic-parent="34">∀
          <!-- ∀ -->
        </mi>
        <mo data-semantic-type="punctuation" data-semantic-role="application" data-semantic-id="33" data-semantic-parent="34" data-semantic-added="true" data-semantic-operator="appl">⁡</mo>
        <mrow data-semantic-type="infixop" data-semantic-role="implicit" data-semantic-id="32" data-semantic-children="12,30" data-semantic-content="31" data-semantic-parent="34">
          <mi data-semantic-type="identifier" data-semantic-role="latinletter" data-semantic-font="italic" data-semantic-id="12" data-semantic-parent="32">y</mi>
          <mspace width="thinmathspace"/>
          <mo data-semantic-type="operator" data-semantic-role="multiplication" data-semantic-id="31" data-semantic-parent="32" data-semantic-added="true" data-semantic-operator="infixop,⁢">⁢</mo>
          <mrow data-semantic-type="appl" data-semantic-role="prefix function" data-semantic-id="30" data-semantic-children="13,28" data-semantic-content="29" data-semantic-parent="32">
            <mi mathvariant="normal" data-semantic-type="prefixop" data-semantic-role="prefix function" data-semantic-font="normal" data-semantic-id="13" data-semantic-parent="30">∀
              <!-- ∀ -->
            </mi>
            <mo data-semantic-type="punctuation" data-semantic-role="application" data-semantic-id="29" data-semantic-parent="30" data-semantic-added="true" data-semantic-operator="appl">⁡</mo>
            <mrow data-semantic-type="infixop" data-semantic-role="implicit" data-semantic-id="28" data-semantic-children="14,26" data-semantic-content="27" data-semantic-parent="30">
              <mi data-semantic-type="identifier" data-semantic-role="latinletter" data-semantic-font="italic" data-semantic-id="14" data-semantic-parent="28">x</mi>
              <mspace width="thinmathspace"/>
              <mo data-semantic-type="operator" data-semantic-role="multiplication" data-semantic-id="27" data-semantic-parent="28" data-semantic-added="true" data-semantic-operator="infixop,⁢">⁢</mo>
              <mrow data-semantic-type="appl" data-semantic-role="simple function" data-semantic-id="26" data-semantic-children="15,24" data-semantic-content="25,15" data-semantic-parent="28">
                <mi data-semantic-type="identifier" data-semantic-role="simple function" data-semantic-font="italic" data-semantic-id="15" data-semantic-parent="26" data-semantic-operator="appl">P</mi>
                <mo data-semantic-type="punctuation" data-semantic-role="application" data-semantic-id="25" data-semantic-parent="26" data-semantic-added="true" data-semantic-operator="appl">⁡</mo>
                <mrow data-semantic-type="fenced" data-semantic-role="leftright" data-semantic-id="24" data-semantic-children="23" data-semantic-content="16,20" data-semantic-parent="26">
                  <mo stretchy="false" data-semantic-type="fence" data-semantic-role="open" data-semantic-id="16" data-semantic-parent="24" data-semantic-operator="fenced">(</mo>
                  <mrow data-semantic-type="punctuated" data-semantic-role="sequence" data-semantic-id="23" data-semantic-children="17,18,19" data-semantic-content="18" data-semantic-parent="24">
                    <mi data-semantic-type="identifier" data-semantic-role="latinletter" data-semantic-font="italic" data-semantic-id="17" data-semantic-parent="23">x</mi>
                    <mo data-semantic-type="punctuation" data-semantic-role="comma" data-semantic-id="18" data-semantic-parent="23" data-semantic-operator="punctuated">,</mo>
                    <mi data-semantic-type="identifier" data-semantic-role="latinletter" data-semantic-font="italic" data-semantic-id="19" data-semantic-parent="23">y</mi>
                  </mrow>
                  <mo stretchy="false" data-semantic-type="fence" data-semantic-role="close" data-semantic-id="20" data-semantic-parent="24" data-semantic-operator="fenced">)</mo>
                </mrow>
              </mrow>
            </mrow>
          </mrow>
        </mrow>
      </mrow>
    </mrow>
    <annotation encoding="application/x-tex">\forall x\,\forall y\,P(x,y)\Leftrightarrow \forall y\,\forall x\,P(x,y)</annotation>
  </semantics>
</math>