Guarded command grammar and finite histories

Assertion (iii) is deliberately conditional on the displayed preservation property. This paper does not manufacture the native three-to-six certificate from an unspecified matrix or chart. The supplied VIII-A record describes one accepted event on the reference cone; VIII-B describes fixed-deficit packet instances; VIII-C describes their guarded composition CheungVIIIA,CheungVIIIB,CheungVIIIC. Those documentary statements are not extra hypotheses hidden inside the proof.