Part A ports, one for one, the 67 checks of the verification function in the figure program deposited with the article. Part B checks the worked examples stated in the article text. Part C checks the decibel conversion and input parsing. The checks reproduce stated examples; they do not prove the general theorems.