proof

P27 Successor invariant chain

Lean spine source

Declarations: P27_successor_invariant_chain

From the machine-checked spine in formal/ (Mathlib + spine imports). Not self-contained for Lean 4 Web — use the repo or a local lake build.

theorem P27_successor_invariant_chain
    (P : System → Prop)
    {A B : System}
    (h0 : P A)
    (hstep : ∀ X Y, Successor X Y → P X → P Y)
    (hchain : SuccessorChain A B) :
    P B := by
  induction hchain with
  | refl A => exact h0
  | step hsucc _ ih => exact ih (hstep _ _ hsucc h0)