Registry · Lemma I.L02 established formalized

I.L02 — NF-Confluence

Normalization of programs is confluent: any two reduction paths yield the same normal form. Proved via termination + local confluence + Newman's Lemma.

Book I Part 3 Ch. 13

Dependency Graph

Depends on (2)

I.D14 I.T01

Depended on by (3)

I.D79 I.T37 I.T46

Lean Formalization

Module: TauLib.BookI.Denotation.ProgramMonoid

Symbol: Tau.Denotation.nf_confluence