Module Z3.Proof

val is_true : Expr.expr -> bool
val is_asserted : Expr.expr -> bool
val is_goal : Expr.expr -> bool
val is_oeq : Expr.expr -> bool
val is_modus_ponens : Expr.expr -> bool
val is_reflexivity : Expr.expr -> bool
val is_symmetry : Expr.expr -> bool
val is_transitivity : Expr.expr -> bool
val is_Transitivity_star : Expr.expr -> bool
val is_monotonicity : Expr.expr -> bool
val is_quant_intro : Expr.expr -> bool
val is_distributivity : Expr.expr -> bool
val is_and_elimination : Expr.expr -> bool
val is_or_elimination : Expr.expr -> bool
val is_rewrite : Expr.expr -> bool
val is_rewrite_star : Expr.expr -> bool
val is_pull_quant : Expr.expr -> bool
val is_push_quant : Expr.expr -> bool
val is_elim_unused_vars : Expr.expr -> bool
val is_der : Expr.expr -> bool
val is_quant_inst : Expr.expr -> bool
val is_hypothesis : Expr.expr -> bool
val is_lemma : Expr.expr -> bool
val is_unit_resolution : Expr.expr -> bool
val is_iff_true : Expr.expr -> bool
val is_iff_false : Expr.expr -> bool
val is_commutativity : Expr.expr -> bool
val is_def_axiom : Expr.expr -> bool
val is_def_intro : Expr.expr -> bool
val is_apply_def : Expr.expr -> bool
val is_iff_oeq : Expr.expr -> bool
val is_nnf_pos : Expr.expr -> bool
val is_nnf_neg : Expr.expr -> bool
val is_skolemize : Expr.expr -> bool
val is_modus_ponens_oeq : Expr.expr -> bool
val is_theory_lemma : Expr.expr -> bool