= Finite-injury priority construction
A finite-injury priority construction orders countably many requirements so that each has finitely many predecessors. A strategy may discard lower-priority strategies' current witnesses and restraints when it acts. If each requirement acts finitely often after its last such initialization, induction on priority shows that every requirement is injured only finitely often and eventually has a stable strategy. The <Friedberg–Muchnik theorem> is a central example.
Back to article page
