Constraint Generalization

Core Concept

Given proven constraints on individual paths, synthesize new constraints that hold across composed paths. This skill moves from "validation" (rejecting bad paths) to "generation" (creating better paths).

Example: If path A proves outputs are even, and path B proves outputs are positive, the composed path AB proves outputs are both even AND positive.

Why Constraint Generalization?

Without it, constraints are lost during composition:

nav_even = @late_nav([ALL, pred(iseven)])      # proves: even
nav_positive = @late_nav([ALL, pred(x > 0)])   # proves: positive