Registry · Lemma VII.L32 conjectural formalized

VII.L32 — OR3+OR4 Narrowing

Diagonal-free + NF-addressable force NF-address structure compatible with self-description, entailing axioms K0-K4.

Book VII Part 2 Ch. 29

Dependency Graph

Depends on (1)

VII.D37

Lean Formalization

Module: TauLib.BookVII.Meta.Saturation

Symbol: Tau.BookVII.Meta.Saturation.or34_narrowing