-- ========================================================================
--             ABP Proof score for invariant properties
--                the first verification condition 
-- ========================================================================

-- ========================================================================
require abp-genCheck

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

-- ========================================================================
open ABP-INV-1-genCheck .
pr(IINV) 
eq p-iinv = iinv2 . 
eq p^t = ft .
red ck .
close

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

-- the above proof score just checks 
--     (cj(ft sr rs,`s:PreState) implies cj(ft,`s:PreState))