Exercise logic.propositional.proof.unicode

Description
Prove two propositions equivalent (unicode support)

Strategy

<label name="proofequivalent">
  <sequence>
    <let>
      <decl var="5">
        <orelse>
          <sequence>
            <orelse>
              <let>
                <decl var="1">
                  <choice>
                    <rule name="top-is-not"/>
                    <rule name="top-is-equiv"/>
                    <rule name="top-is-impl"/>
                    <orelse>
                      <rule name="top-is-and"/>
                      <rule name="top-is-and.com"/>
                    </orelse>
                    <orelse>
                      <rule name="top-is-or"/>
                      <rule name="top-is-or.com"/>
                    </orelse>
                    <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>
              <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">
                              <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>
                        </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>
              <sequence>
                <let>
                  <decl var="3">
                    <orelse>
                      <sequence>
                        <let>
                          <decl var="1">
                            <choice>
                              <rule name="command.common-literal-special"/>
                              <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>
                        <var var="3"/>
                      </sequence>
                      <succeed/>
                    </orelse>
                  </decl>
                  <var var="3"/>
                </let>
                <let>
                  <decl var="1">
                    <choice>
                      <rule name="andoveror.inv.common-literal"/>
                      <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="3">
                    <orelse>
                      <sequence>
                        <let>
                          <decl var="1">
                            <choice>
                              <rule name="andoveror.inv.common-literal"/>
                              <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>
                        <var var="3"/>
                      </sequence>
                      <succeed/>
                    </orelse>
                  </decl>
                  <var var="3"/>
                </let>
                <let>
                  <decl var="3">
                    <orelse>
                      <sequence>
                        <let>
                          <decl var="1">
                            <choice>
                              <rule name="top-is-and"/>
                              <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>
                        <var var="3"/>
                      </sequence>
                      <succeed/>
                    </orelse>
                  </decl>
                  <var var="3"/>
                </let>
              </sequence>
              <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>
              <sequence>
                <rule name="is-dnf"/>
                <let>
                  <decl var="3">
                    <orelse>
                      <sequence>
                        <let>
                          <decl var="1">
                            <choice>
                              <rule name="command.common-literal"/>
                              <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>
                        <var var="3"/>
                      </sequence>
                      <succeed/>
                    </orelse>
                  </decl>
                  <var var="3"/>
                </let>
                <let>
                  <decl var="1">
                    <choice>
                      <rule name="andoveror.inv.common-literal"/>
                      <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="3">
                    <orelse>
                      <sequence>
                        <let>
                          <decl var="1">
                            <choice>
                              <rule name="andoveror.inv.common-literal"/>
                              <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>
                        <var var="3"/>
                      </sequence>
                      <succeed/>
                    </orelse>
                  </decl>
                  <var var="3"/>
                </let>
                <let>
                  <decl var="3">
                    <orelse>
                      <sequence>
                        <let>
                          <decl var="1">
                            <choice>
                              <rule name="top-is-and"/>
                              <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>
                        <var var="3"/>
                      </sequence>
                      <succeed/>
                    </orelse>
                  </decl>
                  <var var="3"/>
                </let>
              </sequence>
            </orelse>
            <var var="5"/>
          </sequence>
          <succeed/>
        </orelse>
      </decl>
      <var var="5"/>
    </let>
    <rule name="is-dnf"/>
    <let>
      <decl var="6">
        <orelse>
          <sequence>
            <orelse>
              <let>
                <decl var="1">
                  <choice>
                    <rule name="top-is-not"/>
                    <rule name="top-is-equiv"/>
                    <rule name="top-is-impl"/>
                    <orelse>
                      <rule name="top-is-and"/>
                      <rule name="top-is-and.com"/>
                    </orelse>
                    <orelse>
                      <rule name="top-is-or"/>
                      <rule name="top-is-or.com"/>
                    </orelse>
                    <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">
                  <choice>
                    <rule name="logic.propositional.idempor"/>
                    <rule name="logic.propositional.idempand"/>
                    <rule name="absorpor-subset"/>
                    <rule name="logic.propositional.complor"/>
                    <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="4">
                  <orelse>
                    <sequence>
                      <rule name="check"/>
                      <rule name="navigator.down"/>
                      <succeed/>
                      <let>
                        <decl var="3">
                          <choice>
                            <let>
                              <decl var="1">
                                <choice>
                                  <sequence>
                                    <rule name="check"/>
                                    <rule name="check"/>
                                    <rule name="introtrueleft"/>
                                    <rule name="introcompl"/>
                                    <rule name="logic.propositional.andoveror"/>
                                  </sequence>
                                  <sequence>
                                    <rule name="check"/>
                                    <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>
                            <sequence>
                              <rule name="navigator.right"/>
                              <succeed/>
                              <var var="3"/>
                            </sequence>
                          </choice>
                        </decl>
                        <var var="3"/>
                      </let>
                      <orelse>
                        <rule name="navigator.up"/>
                        <succeed/>
                      </orelse>
                    </sequence>
                    <sequence>
                      <rule name="navigator.down"/>
                      <succeed/>
                      <let>
                        <decl var="5">
                          <choice>
                            <var var="4"/>
                            <sequence>
                              <rule name="navigator.right"/>
                              <succeed/>
                              <var var="5"/>
                            </sequence>
                          </choice>
                        </decl>
                        <var var="5"/>
                      </let>
                      <orelse>
                        <rule name="navigator.up"/>
                        <succeed/>
                      </orelse>
                    </sequence>
                  </orelse>
                </decl>
                <var var="4"/>
              </let>
            </orelse>
            <var var="6"/>
          </sequence>
          <succeed/>
        </orelse>
      </decl>
      <var var="6"/>
    </let>
  </sequence>
</label>

Locations