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

-- ========================================================================
require qlock-genCheck
require qlock-genStTerm
require qlock-constAndLitl

-- ========================================================================
mod! Q-INV-2-genCheck {ex(Q-INV-2 + GENstTerm + CONSTandLITL)
op ck : -> IndTr .
eq ck = check
(
 [(g("_%_")[(g("_$_")[q,empty]),a1])]
      ||
 [(g("_%_")[(g("_$_")[empQ,(g("lb[_]:__")[a1,(rs;ws;cs),as])]),a2])]
      || 
 [(g("_%_")[(g("_$_")[(a1 & q),(g("lb[_]:__")[a2,(rs;ws;cs),as])]),a3])]
) .
}

-- ========================================================================
open Q-INV-2-genCheck .
pr(INIT + INV)
eq p-init = init .
eq p-iinv = inv1 inv2 inv3 .
red ck .
close

-- ========================================================================
eof 
** end of file
** the system reads the input file until this key word
** the text after this is comment and not be read by the system

-- ========================================================================

 [(g("_%_")[(g("_$_")[q,empty]),a1])]
      ||
 [(g("_%_")[(g("_$_")[empQ,(g("lb[_]:__")[a1,(rs;ws;cs),as])]),a2])]
      || 
 [(g("_%_")[(g("_$_")[(a1 & q),(g("lb[_]:__")[a2,(rs;ws;cs),as])]),a3])]
=red=>
[ ((q $ empty) % a1) ] || 
[ ((empQ $ ((lb [ a1 ] : rs) as)) % a2) ] || 
[ ((empQ $ ((lb [ a1 ] : ws) as)) % a2) ] || 
[ ((empQ $ ((lb [ a1 ] : cs) as)) % a2) ] || 
[ (((a1 & q) $ ((lb [ a2 ] : rs) as)) % a3) ] || 
[ (((a1 & q) $ ((lb [ a2 ] : ws) as)) % a3) ] || 
[ (((a1 & q) $ ((lb [ a2 ] : cs) as)) % a3) ]

-- ========================================================================