Method test_nat_nonneg

tests/test_z3_semantic.py:417–419

(self, kernel)

        assert _try_prove(Implies(And(x <= y, y <= x), x == y))

    def test_nat_nonneg(self, kernel):
        n = Nat("n")
        assert _try_prove(n >= NatVal(0))

    def test_nat_succ_pos(self, kernel):
        n = Nat("n")