Full-graph verdict

This is justified by Propositions prop:D0 and prop:nolift. It continues the J2 stop of XIV-J, the B1 stop of XV-B, and the C0 stop of XV-C Jverdict,XVB,XVC. It is not an obstruction: no exhaustive class is defined and no incompatibility is proved. It is not a construction: no map on ${\mathcal{P}}_{\mathrm{int}}$ is defined. The admission (eq:admission) is unasserted, and “not admitted” is not “nonexistent” Jadmission.