Manuscript XI-G@1 · XI-G.tex · section · f029bbcd
Scope of the obstruction
G3: the wavefront alternative › Scope of the obstruction · lines 1324–1331
Gate 3 ends at Proved obstructed. The constructed branch is characterized by (eq:criterion) and not instantiated; the unresolved branch does not arise, because the extension criterion is discharged by Lemma lem:decay.