-- ========================================================================
--            EX-QLOCK Proof score for invariant properties
--                the first verification condition 
-- ========================================================================

-- ========================================================================
require qlock-genCheck

-- ========================================================================
mod! Q-INV-1-genCheck {ex(Q-INV-1)
op ck : -> IndTr . eq ck = check([`s:ExState]) .
}

-- ========================================================================
open Q-INV-1-genCheck .
pr(INV) 
eq p-iinv = inv1 inv2 inv3 . 
eq p^t = mx .
red ck .
close

-- ========================================================================
eof