proof

P40 Safety-case leaves

Lean spine source

Declarations: P40_unsupported_leaf_blocks_root

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 P40_unsupported_leaf_blocks_root
    {n : Nat} {supported : Fin n → Prop} {requiresLeaf : Fin n → Fin n → Prop}
    {leaf root : Fin n}
    (h : requiresLeaf leaf root)
    (hunsup : ¬ supported leaf) :
    ¬ FiniteProvenDef supported requiresLeaf root := fun hp => hunsup (hp leaf h)