Function prove_invariant 

pub fn prove_invariant(
    init: &ProofExpr,
    trans: &dyn Fn(u32) -> ProofExpr,
    property: &dyn Fn(u32) -> ProofExpr,
    k: u32,
) -> InductionOutcome

k-induction: prove property is an invariant of the transition system.

• Base: for each j < k, init ∧ path(j) ∧ ¬property(j) is certified-UNSAT (no violation in the first k steps; a SAT here is a genuine counterexample).
• Step: property(0..k) ∧ trans(0..k) ∧ ¬property(k) is certified-UNSAT (the property is k-inductive).

Both certified ⇒ InductionOutcome::Proven for the unbounded system.