Exercise logic.propositional.dnf.unicode

Description
Proposition to DNF (unicode support)

Strategy

<label name="dnf">
  <let>
    <decl var="5">
      <orelse>
        <sequence>
          <choice>
            <label name="orrules">
              <choice>
                <rule name="logic.propositional.falsezeroor"/>
                <rule name="logic.propositional.truezeroor"/>
                <rule name="logic.propositional.idempor"/>
                <rule name="logic.propositional.absorpor"/>
                <rule name="logic.propositional.complor"/>
                <fail/>
              </choice>
            </label>
            <let>
              <decl var="3">
                <choice>
                  <sequence>
                    <rule name="check"/>
                    <orelse>
                      <label name="simplify">
                        <let>
                          <decl var="1">
                            <preference>
                              <choice>
                                <label name="orrules">
                                  <choice>
                                    <rule name="logic.propositional.falsezeroor"/>
                                    <rule name="logic.propositional.truezeroor"/>
                                    <rule name="logic.propositional.idempor"/>
                                    <rule name="logic.propositional.absorpor"/>
                                    <rule name="logic.propositional.complor"/>
                                    <fail/>
                                  </choice>
                                </label>
                                <label name="andrules">
                                  <choice>
                                    <rule name="logic.propositional.falsezeroand"/>
                                    <rule name="logic.propositional.truezeroand"/>
                                    <rule name="logic.propositional.idempand"/>
                                    <rule name="logic.propositional.absorpand"/>
                                    <rule name="logic.propositional.compland"/>
                                    <fail/>
                                  </choice>
                                </label>
                                <rule name="logic.propositional.nottrue"/>
                                <rule name="logic.propositional.notfalse"/>
                                <rule name="logic.propositional.notnot"/>
                                <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>
                            </preference>
                          </decl>
                          <var var="1"/>
                        </let>
                      </label>
                      <preference>
                        <label name="specialsort" removed="true">
                          <let>
                            <decl var="1">
                              <choice>
                                <rule name="complor.sort"/>
                                <rule name="compland.sort"/>
                                <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>
                        <label name="specialdistrnot">
                          <let>
                            <decl var="1">
                              <choice>
                                <sequence>
                                  <rule name="check"/>
                                  <rule name="logic.propositional.oroverand"/>
                                </sequence>
                                <sequence>
                                  <rule name="check"/>
                                  <rule name="logic.propositional.andoveror"/>
                                </sequence>
                                <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>
                        <label name="specialdemorgannot">
                          <let>
                            <decl var="1">
                              <choice>
                                <sequence>
                                  <rule name="check"/>
                                  <preference>
                                    <rule name="logic.propositional.gendemorganor"/>
                                    <rule name="logic.propositional.demorganor"/>
                                  </preference>
                                </sequence>
                                <sequence>
                                  <rule name="check"/>
                                  <preference>
                                    <rule name="logic.propositional.gendemorganand"/>
                                    <rule name="logic.propositional.demorganand"/>
                                  </preference>
                                </sequence>
                                <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>
                      </preference>
                      <preference>
                        <label name="eliminateimplequiv">
                          <preference>
                            <let>
                              <decl var="1">
                                <choice>
                                  <rule name="logic.propositional.defimpl"/>
                                  <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>
                            <let>
                              <decl var="1">
                                <preference>
                                  <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>
                                  <rule name="logic.propositional.defequiv"/>
                                </preference>
                              </decl>
                              <var var="1"/>
                            </let>
                          </preference>
                        </label>
                        <label name="demorgan">
                          <let>
                            <decl var="1">
                              <choice>
                                <preference>
                                  <rule name="logic.propositional.gendemorganor"/>
                                  <rule name="logic.propositional.demorganor"/>
                                </preference>
                                <preference>
                                  <rule name="logic.propositional.gendemorganand"/>
                                  <rule name="logic.propositional.demorganand"/>
                                </preference>
                                <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>
                      </preference>
                      <label name="distrand">
                        <let>
                          <decl var="1">
                            <preference>
                              <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>
                              <rule name="logic.propositional.genandoveror"/>
                              <rule name="logic.propositional.andoveror"/>
                            </preference>
                          </decl>
                          <var var="1"/>
                        </let>
                      </label>
                    </orelse>
                  </sequence>
                  <sequence>
                    <rule name="check"/>
                    <rule name="navigator.down"/>
                    <succeed/>
                    <let>
                      <decl var="4">
                        <choice>
                          <var var="3"/>
                          <sequence>
                            <rule name="navigator.right"/>
                            <succeed/>
                            <var var="4"/>
                          </sequence>
                        </choice>
                      </decl>
                      <var var="4"/>
                    </let>
                    <orelse>
                      <rule name="navigator.up"/>
                      <succeed/>
                    </orelse>
                  </sequence>
                </choice>
              </decl>
              <var var="3"/>
            </let>
          </choice>
          <var var="5"/>
        </sequence>
        <succeed/>
      </orelse>
    </decl>
    <var var="5"/>
  </let>
</label>

Locations