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

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

-- ========================================================================
mod! FACTtbu {pr(ABPpred)

-- 0g 1g on Rsch
-- (rs-1)
eq 0g(B1:Bit,RSC:RsCh) and 1g(B2:Bit,RSC) = 0g(B1,RSC) .

-- (rs-22)
eq 0g(B:Bit,RSC1:RsCh) and 0g(B,RSC2:RsCh) and 0g(B,RSC1 RSC2)
   = 0g(B,RSC1) and 0g(B,RSC2) .

-- (rs-3)
eq 0g(B:Bit,RSC1:RsCh) and 1g(B,RSC2:RsCh) and 1g(B,RSC1 RSC2)
   = 0g(B,RSC1) and 1g(B,RSC2) .

-- (rs-4)
ceq 1g(B1:Bit,RSC1:RsCh) and 0g(B2:Bit,RSC2:RsCh) and 1g(B1,RSC1 RSC2)
    = 1g(B1,RSC1) and 0g(B2,RSC2) if (B1 = not(B2)) .

-- 0g 1g SrCh
-- (sr-1)
 eq 0g(BN:Bnp,SRC1:SrCh) and 0g(BN,SRC2:SrCh) and 0g(BN,SRC1 SRC2) = 
    0g(BN,SRC1) and 0g(BN,SRC2) .

-- (sr-2)
eq 0g(BN:Bnp,SRC1:SrCh) and 1g(BN,SRC2:SrCh) and 1g(BN,SRC1 SRC2) = 
   0g(BN,SRC1) and 1g(BN,SRC2) .

-- (sr-3)
ceq (0g(BN1:Bnp,SRC:SrCh) and 1g(BN2:Bnp,SRC)) = 0g(BN1,SRC) 
    if ((BN2 = (s BN1)) or (BN1 = (p BN2))) .

-- (sr-4)
ceq 1g(BN1:Bnp,SRC1:SrCh) and 0g(BN2:Bnp,SRC2:SrCh) and 1g(BN1,SRC1 SRC2) = 
    1g(BN1,SRC1) and 0g(BN2,SRC2) if (BN2 = p(BN1)) .
    
-- NnSeq
eq (N:Nn NS1:NnSeq = N:Nn NS2:NnSeq) = (NS1 = NS2) .

}
-- ========================================================================
provide abp-factTbu

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