-- ========================================================================
--             facts to be used for verifications
-- ========================================================================

-- ========================================================================
require qlock-prop

-- ========================================================================
mod! FACTtbu {pr(STATEfuns-pq)
-- necessary fact about #aq
eq #aq(Q:Qu & A1:Aid,A2:Aid) = if (A1 = A2) then (s 0) + #aq(Q,A2) 
                               else #aq(Q,A2) fi .
-- for Nat
eq [NatGt1]: ((N:Nat.PNAT = 0) and (N > 0)) = false .
ceq [NatGt2]: (s N1:Nat.PNAT > N2:Nat.PNAT) = true if N1 > N2 .
eq ((N:Nat.PNAT = 0) and (N = s 0)) = false .

-- about laga
ceq ((laga(AS:Aobs,A:Aid) = L1:Label) and 
     (laga(AS,A) = L2:Label)) = false
    if not(L1 = L2) .

-- about #daq
ceq #daq((Q:Qu & A1:Aid),A2:Aid) = #daq(Q,A2) if not(A1 = A2) .
}

-- ========================================================================
provide qlock-factTbu

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