Method test_contrapositive_proof

tests/test_z3_ported.py:507–511

(p => q) => (Not(q) => Not(p))

(self, kernel)

        assert prove(claim)

    def test_contrapositive_proof(self, kernel):
        """(p => q) => (Not(q) => Not(p))"""
        p, q = Bools("p q")
        claim = ForAll([p, q], Implies(Implies(p, q), Implies(Not(q), Not(p))))
        assert prove(claim)

    def test_excluded_middle(self, kernel):
        """p ∨ ¬p is always true."""