Exercise relationalgebra.cnf

Description
To conjunctive normal form

Strategy

<label name="tocnf">
  <let>
    <decl var="3">
      <orelse>
        <sequence>
          <orelse>
            <label name="step1">
              <let>
                <decl var="1">
                  <orelse>
                    <choice>
                      <rule name="relationalgebra.remcompl"/>
                      <rule name="relationalgebra.remredunexprs"/>
                      <rule name="relationalgebra.doublenegation"/>
                      <rule name="relationalgebra.idempotencyor"/>
                      <rule name="relationalgebra.idempotencyand"/>
                      <rule name="relationalgebra.absorp"/>
                      <rule name="relationalgebra.absorpcompl"/>
                      <rule name="relationalgebra.invoverunion"/>
                      <rule name="relationalgebra.invoverintersect"/>
                      <rule name="relationalgebra.invovercomp"/>
                      <rule name="relationalgebra.invoveradd"/>
                      <rule name="relationalgebra.invovernot"/>
                      <rule name="relationalgebra.doubleinv"/>
                      <fail/>
                    </choice>
                    <sequence>
                      <rule name="navigator.down"/>
                      <succeed/>
                      <let>
                        <decl var="2">
                          <choice>
                            <var var="1"/>
                            <sequence>
                              <rule name="navigator.right"/>
                              <succeed/>
                              <var var="2"/>
                            </sequence>
                          </choice>
                        </decl>
                        <var var="2"/>
                      </let>
                      <orelse>
                        <rule name="navigator.up"/>
                        <succeed/>
                      </orelse>
                    </sequence>
                  </orelse>
                </decl>
                <var var="1"/>
              </let>
            </label>
            <label name="step2">
              <let>
                <decl var="1">
                  <orelse>
                    <choice>
                      <rule name="relationalgebra.compoverunion"/>
                      <rule name="relationalgebra.addoverintersec"/>
                      <rule name="relationalgebra.demorganor"/>
                      <rule name="relationalgebra.demorganand"/>
                      <rule name="relationalgebra.notovercomp"/>
                      <rule name="relationalgebra.notoveradd"/>
                      <fail/>
                    </choice>
                    <sequence>
                      <rule name="navigator.down"/>
                      <succeed/>
                      <let>
                        <decl var="2">
                          <choice>
                            <var var="1"/>
                            <sequence>
                              <rule name="navigator.right"/>
                              <succeed/>
                              <var var="2"/>
                            </sequence>
                          </choice>
                        </decl>
                        <var var="2"/>
                      </let>
                      <orelse>
                        <rule name="navigator.up"/>
                        <succeed/>
                      </orelse>
                    </sequence>
                  </orelse>
                </decl>
                <var var="1"/>
              </let>
            </label>
            <label name="step3">
              <let>
                <decl var="1">
                  <choice>
                    <rule name="relationalgebra.unionoverintersec"/>
                    <sequence>
                      <rule name="navigator.down"/>
                      <succeed/>
                      <let>
                        <decl var="2">
                          <choice>
                            <var var="1"/>
                            <sequence>
                              <rule name="navigator.right"/>
                              <succeed/>
                              <var var="2"/>
                            </sequence>
                          </choice>
                        </decl>
                        <var var="2"/>
                      </let>
                      <orelse>
                        <rule name="navigator.up"/>
                        <succeed/>
                      </orelse>
                    </sequence>
                  </choice>
                </decl>
                <var var="1"/>
              </let>
            </label>
          </orelse>
          <var var="3"/>
        </sequence>
        <succeed/>
      </orelse>
    </decl>
    <var var="3"/>
  </let>
</label>

Locations