Define , a test. Then let be a state vector for input.
Following the application of the assignment, the output is
So counts as True every possible input to the assignment that gives an output satisfying . So is the most general possible precondition making the tripple correct.