Proof Labs

Interactive theorem companion

Proof Labs

See the mechanism, predict the next proof state, then open the formal justification.

Each lab keeps one mathematical visual in the foreground. The example explains the current step; the formal argument proves it for every case.

Chapter 1 · Finite-State Automata

Theorem 1 Subset construction Synchronize every NFA run with one deterministic subset.

Chapter 2 · Regular Languages and Decision Problems

Theorem 2 ε-removal Compile free paths into ordinary symbol transitions. Theorem 3 Kleene equivalence Follow the constructive cycle between automata and expressions. Theorem 4 Closure of regular languages Read every closure property as an automaton compiler. Theorem 5 Small model property Delete a repeated-state loop from a shortest accepting run. Theorem 6 Myhill–Nerode Turn indistinguishable futures into the canonical DFA.

Chapter 3 · Automata over Infinite Words

Theorem 7 Basic ω-regular closure Alternate recurring obligations in Büchi intersection. Theorem 8 Büchi–expression equivalence Cut an accepting run into a finite prefix and recurring loops.

Chapter 4 · Complementation of ω-Regular Languages

Lemma Ramsey decomposition Slice any ω-word, periodic or not, into a prefix and repeating V-blocks. Theorem 9 Büchi complementation Partition all infinite words into saturated class products.