Exercise logic.propositional.dnf
Description
Proposition to DNF
Derivation
Final term is not finished~(~(T /\ ~F /\ ((~(~T /\ T) /\ ~(~T /\ T) /\ ~~(T /\ q)) || (~(~T /\ T) /\ ~(~T /\ T) /\ ~r)) /\ ~~(T /\ ~q /\ ~~T /\ ~~p /\ ~q /\ ~~(p /\ ~q /\ T /\ T) /\ p /\ ~~(p /\ ~q) /\ T)) /\ ~(T /\ ~F /\ ((~(~T /\ T) /\ ~(~T /\ T) /\ ~~(T /\ q)) || (~(~T /\ T) /\ ~(~T /\ T) /\ ~r)) /\ ~~(T /\ ~q /\ ~~T /\ ~~p /\ ~q /\ ~~(p /\ ~q /\ T /\ T) /\ p /\ ~~(p /\ ~q) /\ T)))
⇒ logic.propositional.idempand~~(T /\ ~F /\ ((~(~T /\ T) /\ ~(~T /\ T) /\ ~~(T /\ q)) || (~(~T /\ T) /\ ~(~T /\ T) /\ ~r)) /\ ~~(T /\ ~q /\ ~~T /\ ~~p /\ ~q /\ ~~(p /\ ~q /\ T /\ T) /\ p /\ ~~(p /\ ~q) /\ T))
⇒ logic.propositional.truezeroand~~(~F /\ ((~(~T /\ T) /\ ~(~T /\ T) /\ ~~(T /\ q)) || (~(~T /\ T) /\ ~(~T /\ T) /\ ~r)) /\ ~~(T /\ ~q /\ ~~T /\ ~~p /\ ~q /\ ~~(p /\ ~q /\ T /\ T) /\ p /\ ~~(p /\ ~q) /\ T))
⇒ logic.propositional.idempand~~(~F /\ ((~(~T /\ T) /\ ~~(T /\ q)) || (~(~T /\ T) /\ ~(~T /\ T) /\ ~r)) /\ ~~(T /\ ~q /\ ~~T /\ ~~p /\ ~q /\ ~~(p /\ ~q /\ T /\ T) /\ p /\ ~~(p /\ ~q) /\ T))
⇒ logic.propositional.compland~~(~F /\ ((~F /\ ~~(T /\ q)) || (~(~T /\ T) /\ ~(~T /\ T) /\ ~r)) /\ ~~(T /\ ~q /\ ~~T /\ ~~p /\ ~q /\ ~~(p /\ ~q /\ T /\ T) /\ p /\ ~~(p /\ ~q) /\ T))
⇒ logic.propositional.idempand~~(~F /\ ((~F /\ ~~(T /\ q)) || (~(~T /\ T) /\ ~r)) /\ ~~(T /\ ~q /\ ~~T /\ ~~p /\ ~q /\ ~~(p /\ ~q /\ T /\ T) /\ p /\ ~~(p /\ ~q) /\ T))
⇒ logic.propositional.compland~~(~F /\ ((~F /\ ~~(T /\ q)) || (~F /\ ~r)) /\ ~~(T /\ ~q /\ ~~T /\ ~~p /\ ~q /\ ~~(p /\ ~q /\ T /\ T) /\ p /\ ~~(p /\ ~q) /\ T))
⇒ logic.propositional.notfalse~~(T /\ ((~F /\ ~~(T /\ q)) || (~F /\ ~r)) /\ ~~(T /\ ~q /\ ~~T /\ ~~p /\ ~q /\ ~~(p /\ ~q /\ T /\ T) /\ p /\ ~~(p /\ ~q) /\ T))
⇒ logic.propositional.truezeroand~~(((~F /\ ~~(T /\ q)) || (~F /\ ~r)) /\ ~~(T /\ ~q /\ ~~T /\ ~~p /\ ~q /\ ~~(p /\ ~q /\ T /\ T) /\ p /\ ~~(p /\ ~q) /\ T))
⇒ logic.propositional.notfalse~~(((T /\ ~~(T /\ q)) || (~F /\ ~r)) /\ ~~(T /\ ~q /\ ~~T /\ ~~p /\ ~q /\ ~~(p /\ ~q /\ T /\ T) /\ p /\ ~~(p /\ ~q) /\ T))
⇒ logic.propositional.notfalse~~(((T /\ ~~(T /\ q)) || (T /\ ~r)) /\ ~~(T /\ ~q /\ ~~T /\ ~~p /\ ~q /\ ~~(p /\ ~q /\ T /\ T) /\ p /\ ~~(p /\ ~q) /\ T))
⇒ logic.propositional.notnot~~(((T /\ ~~(T /\ q)) || (T /\ ~r)) /\ T /\ ~q /\ ~~T /\ ~~p /\ ~q /\ ~~(p /\ ~q /\ T /\ T) /\ p /\ ~~(p /\ ~q) /\ T)
⇒ logic.propositional.truezeroand~~(((T /\ ~~(T /\ q)) || (T /\ ~r)) /\ ~q /\ ~~T /\ ~~p /\ ~q /\ ~~(p /\ ~q /\ T /\ T) /\ p /\ ~~(p /\ ~q) /\ T)
⇒ logic.propositional.truezeroand~~(((T /\ ~~(T /\ q)) || (T /\ ~r)) /\ ~q /\ ~~T /\ ~~p /\ ~q /\ ~~(p /\ ~q /\ T /\ T) /\ p /\ ~~(p /\ ~q))
⇒ logic.propositional.notnot~~(((T /\ ~~(T /\ q)) || (T /\ ~r)) /\ ~q /\ T /\ ~~p /\ ~q /\ ~~(p /\ ~q /\ T /\ T) /\ p /\ ~~(p /\ ~q))
⇒ logic.propositional.truezeroand~~(((T /\ ~~(T /\ q)) || (T /\ ~r)) /\ ~q /\ ~~p /\ ~q /\ ~~(p /\ ~q /\ T /\ T) /\ p /\ ~~(p /\ ~q))
⇒ logic.propositional.notnot~~(((T /\ ~~(T /\ q)) || (T /\ ~r)) /\ ~q /\ p /\ ~q /\ ~~(p /\ ~q /\ T /\ T) /\ p /\ ~~(p /\ ~q))
⇒ logic.propositional.notnot~~(((T /\ ~~(T /\ q)) || (T /\ ~r)) /\ ~q /\ p /\ ~q /\ p /\ ~q /\ T /\ T /\ p /\ ~~(p /\ ~q))
⇒ logic.propositional.idempand~~(((T /\ ~~(T /\ q)) || (T /\ ~r)) /\ ~q /\ p /\ ~q /\ T /\ T /\ p /\ ~~(p /\ ~q))
⇒ logic.propositional.idempand~~(((T /\ ~~(T /\ q)) || (T /\ ~r)) /\ ~q /\ p /\ ~q /\ T /\ p /\ ~~(p /\ ~q))
⇒ logic.propositional.truezeroand~~(((T /\ ~~(T /\ q)) || (T /\ ~r)) /\ ~q /\ p /\ ~q /\ p /\ ~~(p /\ ~q))
⇒ logic.propositional.idempand~~(((T /\ ~~(T /\ q)) || (T /\ ~r)) /\ ~q /\ p /\ ~~(p /\ ~q))
⇒ logic.propositional.notnot~~(((T /\ ~~(T /\ q)) || (T /\ ~r)) /\ ~q /\ p /\ p /\ ~q)
⇒ logic.propositional.idempand~~(((T /\ ~~(T /\ q)) || (T /\ ~r)) /\ ~q /\ p /\ ~q)
⇒ logic.propositional.truezeroand~~((~~(T /\ q) || (T /\ ~r)) /\ ~q /\ p /\ ~q)
⇒ logic.propositional.notnot~~(((T /\ q) || (T /\ ~r)) /\ ~q /\ p /\ ~q)
⇒ logic.propositional.truezeroand~~((q || (T /\ ~r)) /\ ~q /\ p /\ ~q)
⇒ logic.propositional.truezeroand~~((q || ~r) /\ ~q /\ p /\ ~q)
⇒ logic.propositional.andoveror~~(((q /\ ~q) || (~r /\ ~q)) /\ p /\ ~q)
⇒ logic.propositional.compland~~((F || (~r /\ ~q)) /\ p /\ ~q)
⇒ logic.propositional.falsezeroor~~(~r /\ ~q /\ p /\ ~q)
⇒ logic.propositional.gendemorganand~(~~r || ~~q || ~p || ~~q)
⇒ logic.propositional.notnot~(r || ~~q || ~p || ~~q)
⇒ logic.propositional.notnot~(r || q || ~p || ~~q)
⇒ logic.propositional.notnot~(r || q || ~p || q)