Registry · Definition VII.D15 tau-effective formalized

VII.D15 — Bounded Witness Form

Claim φ is in BWF if finite witness w exists (τ-finite with NF-address) certifying φ and terminating in finitely many kernel-axiom steps.

Book VII Part 1 Ch. 9

Dependency Graph

Depended on by (2)

VII.L22 VII.T07

Lean Formalization

Module: TauLib.BookVII.Meta.Registers

Symbol: Tau.BookVII.Meta.Registers.BoundedWitnessForm