Theorems · Definition · logic and foundations

StateTransition.evalInduction

{σ : Type u_2} →
  {f : σ → Option σ} →
    {b : σ} →
      {C : σ → Sort u_1} →
        {a : σ} →
          b ∈ StateTransition.eval f a →
            ((a : σ) → b ∈ StateTransition.eval f a → ((a' : σ) → f a = some a' → C a') → C a) → C a

(co-)Induction principle for eval. If a property C holds of any point a evaluating to b which is either terminal (meaning a = b) or where the next point also satisfies C, then it holds of any point where eval f a evaluates to b. This formalizes the notion that if eval f a evaluates to b then it reaches terminal state b in finitely many steps.

Defined in

Mathlib.Computability.StateTransition

Cited by

2 results in Mathlib

Foundations

Depth 20 from the axioms · uses propext, Classical.choice, Quot.sound