Registry · Theorem I.T03 established formalized

I.T03 — Composition Associativity

Program composition is associative. A THEOREM, not an axiom: proved via normalization confluence (NF-Confluence Theorem).

Book I Part 3 Ch. 13

Dependency Graph

Depends on (1)

I.D14

Depended on by (3)

I.D79 I.P24 I.X02

Lean Formalization

Module: TauLib.BookI.Denotation.ProgramMonoid

Symbol: Tau.Denotation.comp_assoc