Method test_excluded_middle

tests/test_z3_ported.py:513–517

p ∨ ¬p is always true.

(self, kernel)

        assert prove(claim)

    def test_excluded_middle(self, kernel):
        """p ∨ ¬p is always true."""
        p = Bool("p")
        claim = ForAll([p], Or(p, Not(p)))
        assert prove(claim)

    def test_xor_definition(self, kernel):
        """Xor(p,q) == And(Or(p,q), Not(And(p,q)))"""