Registry · Lemma VII.L22 tau-effective formalized

VII.L22 — Bounded Witness Form Check

BWF verification: every bounded witness is τ-finite, NF-addressed, and finitely terminating.

Book VII Part 1 Ch. 9

Dependency Graph

Depends on (1)

VII.D15

Lean Formalization

Module: TauLib.BookVII.Meta.Saturation

Symbol: Tau.BookVII.Meta.Saturation.bounded_witness_form_check