Exercise logic.propositional.dnf
Description
Proposition to DNF
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
Location | Label |
[] | dnf |
[0] | ...orrules |
[0,0] | ......logic.propositional.falsezeroor |
[1,0] | ......logic.propositional.truezeroor |
[2,0] | ......logic.propositional.idempor |
[3,0] | ......logic.propositional.absorpor |
[4,0] | ......logic.propositional.complor |
[1] | ...simplify |
[0,1] | ......orrules |
[0,0,1] | .........logic.propositional.falsezeroor |
[1,0,1] | .........logic.propositional.truezeroor |
[2,0,1] | .........logic.propositional.idempor |
[3,0,1] | .........logic.propositional.absorpor |
[4,0,1] | .........logic.propositional.complor |
[1,1] | ......andrules |
[0,1,1] | .........logic.propositional.falsezeroand |
[1,1,1] | .........logic.propositional.truezeroand |
[2,1,1] | .........logic.propositional.idempand |
[3,1,1] | .........logic.propositional.absorpand |
[4,1,1] | .........logic.propositional.compland |
[2,1] | ......logic.propositional.nottrue |
[3,1] | ......logic.propositional.notfalse |
[4,1] | ......logic.propositional.notnot |
[2] | ...specialsort |
[0,2] | ......complor.sort |
[1,2] | ......compland.sort |
[3] | ...specialdistrnot |
[0,3] | ......logic.propositional.oroverand |
[1,3] | ......logic.propositional.andoveror |
[4] | ...specialdemorgannot |
[0,4] | ......logic.propositional.gendemorganor |
[1,4] | ......logic.propositional.demorganor |
[2,4] | ......logic.propositional.gendemorganand |
[3,4] | ......logic.propositional.demorganand |
[5] | ...eliminateimplequiv |
[0,5] | ......logic.propositional.defimpl |
[1,5] | ......logic.propositional.defequiv |
[6] | ...demorgan |
[0,6] | ......logic.propositional.gendemorganor |
[1,6] | ......logic.propositional.demorganor |
[2,6] | ......logic.propositional.gendemorganand |
[3,6] | ......logic.propositional.demorganand |
[7] | ...distrand |
[0,7] | ......logic.propositional.genandoveror |
[1,7] | ......logic.propositional.andoveror |