PSPACE ⊆ NPSPACE

⚠️ Unreviewed by Bolton

Deterministic polynomial space is contained in nondeterministic polynomial space.

This direction is immediate: a deterministic decider is a nondeterministic one whose two transition functions agree, so each DSPACE level embeds in the corresponding NSPACE level. The converse is Savitch's theorem — see NPSPACESubsetPSPACE.

theorem Complexity.PSPACE_subset_NPSPACE : PSPACE ⊆ NPSPACE

PSPACE ⊆ NPSPACE: every deterministic space-bounded decider is a nondeterministic one, level by level.