Exercise logic.propositional.cnf.unicode
Description
Proposition to CNF (unicode support)
Derivation
Final term is not finished
F ∨ ((¬(r ↔ r) ∨ ¬T ∨ ¬r) ∧ T)
⇒ logic.propositional.nottrueF ∨ ((¬(r ↔ r) ∨ F ∨ ¬r) ∧ T)
⇒ logic.propositional.falsezeroorF ∨ ((¬(r ↔ r) ∨ ¬r) ∧ T)
⇒ logic.propositional.defequivF ∨ ((¬((r ∧ r) ∨ (¬r ∧ ¬r)) ∨ ¬r) ∧ T)
⇒ logic.propositional.idempandF ∨ ((¬(r ∨ (¬r ∧ ¬r)) ∨ ¬r) ∧ T)
⇒ logic.propositional.idempandF ∨ ((¬(r ∨ ¬r) ∨ ¬r) ∧ T)
⇒ logic.propositional.complorF ∨ ((¬T ∨ ¬r) ∧ T)
⇒ logic.propositional.nottrueF ∨ ((F ∨ ¬r) ∧ T)
⇒ logic.propositional.falsezeroorF ∨ (¬r ∧ T)