/*
*/

Input I1 is bool
Output O1 is bool


req1: Globally, it is always the case that "O1" holds