-- ========================================================================
--        QLOCK Proof Scores for a (p leads-to q) property
--               the first verification condition 
-- ========================================================================

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

-- ========================================================================
mod! Q-PQ-1-genCheck {
ex(Q-PQ-1 + GENstTerm + CONSTandLITL)
op ck : -> IndTr .
eq ck = check
(
 [(g("_%_")[(g("_$_")[empQ,(g("lb[_]:__")[b1,rs,as])]),
            (b1;b2)]),SS:ExState,CC:Bool]
        || 
 [(g("_%_")[(g("_$_")[(b1 & q),(g("lb[_]:__")[(b1;b2),rs,as])]),
            (b1;b2;b3)]),SS,CC]
        ||
 [(g("_%_")[(g("_$_")[(b1 & q),(g("lb[_]:__")[b1,ws,as])]),
            (b1;b2)]),SS,CC]
        ||
 [(g("_%_")[(g("_$_")[(b1 & q),(g("lb[_]:__")[(b1;b2),cs,as])]),
            (b1;b2;b3)]),SS,CC]
) .
}
-- ========================================================================
-- Generate&Check-T1
open Q-PQ-1-genCheck .
pr(QLOCKsys1)
red ck .
close

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

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

 [(g("_%_")[(g("_$_")[empQ,(g("lb[_]:__")[b1,rs,as])]),
            (b1;b2)]),SS:ExState,CC:Bool]
        || 
 [(g("_%_")[(g("_$_")[(b1 & q),(g("lb[_]:__")[(b1;b2),rs,as])]),
            (b1;b2;b3)]),SS,CC]
        ||
 [(g("_%_")[(g("_$_")[(b1 & q),(g("lb[_]:__")[b1,ws,as])]),
            (b1;b2;b3)]),SS,CC]
        ||
 [(g("_%_")[(g("_$_")[(b1 & q),(g("lb[_]:__")[(b1;b2),cs,as])]),
            (b1;b2;b3)]),SS,CC]
=red=>
(
    [ (((empQ $ ((lb [ b1 ] : rs) as)) % b1) , SS , CC) ] || 
    [ (((empQ $ ((lb [ b1 ] : rs) as)) % b2) , SS , CC) ] || 

[ ((((b1 & q) $ ((lb [ b1 ] : rs) as)) % b1) , SS , CC) ] || 
[ ((((b1 & q) $ ((lb [ b2 ] : rs) as)) % b1) , SS , CC) ] || 
[ ((((b1 & q) $ ((lb [ b1 ] : rs) as)) % b2) , SS , CC) ] || 
[ ((((b1 & q) $ ((lb [ b2 ] : rs) as)) % b2) , SS , CC) ] || 
[ ((((b1 & q) $ ((lb [ b1 ] : rs) as)) % b3) , SS , CC) ] || 
[ ((((b1 & q) $ ((lb [ b2 ] : rs) as)) % b3) , SS , CC) ] || 

[ ((((b1 & q) $ ((lb [ b1 ] : ws) as)) % b1) , SS , CC) ] || 
[ ((((b1 & q) $ ((lb [ b1 ] : ws) as)) % b2) , SS , CC) ] || 

[ ((((b1 & q) $ ((lb [ b1 ] : cs) as)) % b1) , SS , CC) ] || 
[ ((((b1 & q) $ ((lb [ b2 ] : cs) as)) % b1) , SS , CC) ] || 
[ ((((b1 & q) $ ((lb [ b1 ] : cs) as)) % b2) , SS , CC) ] || 
[ ((((b1 & q) $ ((lb [ b2 ] : cs) as)) % b2) , SS , CC) ] || 
[ ((((b1 & q) $ ((lb [ b1 ] : cs) as)) % b3) , SS , CC) ] || 
[ ((((b1 & q) $ ((lb [ b2 ] : cs) as)) % b3) , SS , CC) ])

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