Method test_bool_biimplication

tests/test_z3_ported.py:525–529

(p == q) == And(Implies(p,q), Implies(q,p))

(self, kernel)

        assert prove(claim)

    def test_bool_biimplication(self, kernel):
        """(p == q) == And(Implies(p,q), Implies(q,p))"""
        p, q = Bools("p q")
        claim = ForAll([p, q], (p == q) == And(Implies(p, q), Implies(q, p)))
        assert prove(claim)

    def test_modus_ponens(self, kernel):
        """If p and p => q, then q."""