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

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

-- ========================================================================
mod! ABP-INV-2-genCheck {ex(ABP-INV-2 + INIT + IINV)
op ck : -> IndTr .
eq ck = check([init]) .}
** init = [(sBit: f)(sNn: 0)(srCh: empBN)(rBit: f)(rNns: empN)(rsCh: empB)]

-- ========================================================================
open ABP-INV-2-genCheck .
eq p-init = init .
eq p-iinv = iinv1 iinv2 .
red ck .
close

-- ========================================================================
eof 
** end of file

-- the above proof score just checks 
--                        cj(iinv1 iinv2,init)