-- ========================================================================
--      Proof Scores for facts to be used for Invariant verifications
-- ========================================================================

-- ========================================================================
require abp-factTbu
require abp-constLitl
require genCases

-- ========================================================================
mod! CEQpd {pr(BOOL)
pred _=_if_ : Bool Bool Bool .
eq (B1:Bool = B2:Bool if B3:Bool) = (B3 implies (B1 = B2)) .
}

-- ========================================================================
-- proof scores for fact (rs-1)-(rs-4) on RsCh in the FACTtbu module
-- ========================================================================

-- ========================================================================
--> (rs-1) 
--  eq 0g(B1:Bit,RSC:RsCh) and 1g(B2:Bit,RSC) = 0g(B1,RSC) .
-- proof score with induction of the length of RSC
open (RSchPred + CONST-LITL + GENcases) .
-- induction base: RSC=empB
red ((0g(b1,empB) and 1g(b2,empB)) = 0g(b1,empB)) .
-- induction step
-- induction hypothesis
eq 0g(B1:Bit,rsc1) and 1g(B2:Bit,rsc1) = 0g(B1,rsc1) .
-- step check
[Bit RsCh < Val]
eq v(B1:Bit,B2:Bit,B3:Bit,RSC:RsCh) = 
    ((0g(B1,B3 RSC) and 1g(B2,B3 RSC)) = 0g(B1,B3 RSC)) .
red check([(t;f),(t;f),(t;f),rsc1]) .
close
--> q.e.d.

-- ========================================================================
--> (rs-2) 
--  eq (0g(B:Bit,RSC1:RsCh) and 0g(B,RSC2:RsCh) and 0g(B,RSC1 RSC2))
--   = (0g(B,RSC1) and 0g(B,RSC2)) .
-- proof score with induction of the length of RSC1
open (RSchPred + CONST-LITL + GENcases) .
-- induction base: RSC=empB
red ((0g(b1,empB) and 0g(b1,rsc2) and 0g(b1,empB rsc2))
    = (0g(b1,empB) and 0g(b1,rsc2))) .
-- induction step:
-- induction hypothesis
eq (0g(B:Bit,rsc1) and 0g(B,rsc2) and 0g(B,rsc1 rsc2))
    = (0g(B,rsc1) and 0g(B,rsc2)) .
-- step check
[Bit RsCh < Val]
eq v(B1:Bit,B2:Bit,RSC1:RsCh,RSC2:RsCh) = 
   ((0g(B1,B2 RSC1) and 0g(B1,RSC2) and 0g(B1,(B2 RSC1) RSC2))
     = (0g(B1,B2 RSC1) and 0g(B1,RSC2))) .
red check([(t;f),(t;f),rsc1,rsc2]) .
close
--> q.e.d.

-- ========================================================================
--> (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)) .
-- proof score with induction of the length of RSC1
open (RSchPred + CONST-LITL + GENcases) .
-- induction base: RSC=empB
red (0g(b1,empB) and 1g(b1,rsc2) and 1g(b1,empB rsc2))
        = (0g(b1,empB) and 1g(b1,rsc2)) .
-- induction hypothesis
eq (0g(B:Bit,rsc1) and 1g(B,rsc2) and 1g(B,rsc1 rsc2))
   = (0g(B,rsc1) and 1g(B,rsc2)) .
-- induction step
[Bit RsCh < Val]
eq v(B1:Bit,B2:Bit,RSC1:RsCh,RSC2:RsCh) = 
   ((0g(B1,B2 RSC1) and 1g(B1,RSC2) and 1g(B1,(B2 RSC1) RSC2))
     = (0g(B1,B2 RSC1) and 1g(B1,RSC2))) .
red check([(t;f),(t;f),rsc1,rsc2]) .
close
--> q.e.d.

-- ========================================================================
--> (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)) .
-- proof score with induction on the length of RSC1
-- induction base: RSC=empB
open (RSchPred + CONST-LITL + GENcases + CEQpd) .
-- already proved equation (1)
eq 0g(B1:Bit,RSC:RsCh) and 1g(B2:Bit,RSC) = 0g(B1,RSC) .
[Bit RsCh < Val]
eq v(B1:Bit,B2:Bit,RSC1:RsCh,RSC2:RsCh) = 
    (1g(B1,RSC1) and 0g(B2,RSC2) and 1g(B1,RSC1 RSC2)) = 
    (1g(B1,RSC1) and 0g(B2,RSC2)) if (B1 = not(B2)) .
red check([(t;f),(t;f),empB,rsc2]) .
close
-- induction step: rsc1 implies (B rsc1)
open (RSchPred + CONST-LITL + GENcases + CEQpd) .
-- already proved equation (2)
eq (0g(B:Bit,RSC1:RsCh) and 0g(B,RSC2:RsCh) and 0g(B,RSC1 RSC2))
       = (0g(B,RSC1) and 0g(B,RSC2)) .
-- induction hypothesis
ceq (1g(B1:Bit,rsc1) and 0g(B2:Bit,rsc2) and 1g(B1,rsc1 rsc2))
     = (1g(B1,rsc1) and 0g(B2,rsc2)) if (B1 = not(B2)) .
-- check
[Bit RsCh < Val]
eq v(B1:Bit,B2:Bit,B3:Bit,RSC1:RsCh,RSC2:RsCh) = 
    (1g(B1,B3 RSC1) and 0g(B2,RSC2) and 1g(B1,(B3 RSC1) RSC2)) = 
    (1g(B1,B3 RSC1) and 0g(B2,RSC2)) if (B1 = not(B2)) .
red check([(t;f),(t;f),(t;f),rsc1,rsc2]) .
close
--> q.e.d.

-- ========================================================================
--  proof scores for fact (sr-1)-(sr-4) on SrCh in the FACTtbu module
-- ========================================================================

-- ========================================================================
--> (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) .
-- proof score with induction on the length of RSC1
open (SRchPred + CONST-LITL + GENcases) .
-- induction base:
red ((0g(bn1,empBN) and 0g(bn1,src2) and 0g(bn1,empBN src2))
      = (0g(bn1,empBN) and 0g(bn1,src2))) .

-- induction step: src1 implies (bn1 src1)
-- induction hypothesis
eq (0g(BN:Bnp,src1) and 0g(BN,SRC2:SrCh) and 0g(BN,src1 SRC2))
      = (0g(BN,src1) and 0g(BN,SRC2)) .
-- step check
[Bit Nn Bnp SrCh < Val]
eq v(BN1:Bnp,BN2:Bnp,SRC1:SrCh,SRC2:SrCh) =
    ((0g(BN1,BN2 SRC1) and 0g(BN1,SRC2) and 0g(BN1,(BN2 SRC1) SRC2))
     = (0g(BN1,BN2 SRC1) and 0g(BN1,SRC2))) .
red check([(bn1),(bn1;bn3),src1,src2]) .
close
--> q.e.d.

-- ========================================================================
--> (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) .
-- proof score with induction on the length of RSC1
open (SRchPred + CONST-LITL + GENcases) .
-- induction base: SRC1=empBN
red ((0g(bn1,empBN) and 1g(bn1,src2) and 1g(bn1,empBN src2))
     = (0g(bn1,empBN) and 1g(bn1,src2))) .
-- induction step: src1 implies (bn1 src1)
-- induction hypothesis
eq (0g(BN:Bnp,src1) and 1g(BN,SRC2:SrCh) and 1g(BN,src1 SRC2))
      = (0g(BN,src1) and 1g(BN,SRC2)) .
-- step check
[Bnp SrCh < Val]
eq v(BN1:Bnp,BN2:Bnp,SRC1:SrCh,SRC2:SrCh) =
    ((0g(BN1,BN2 SRC1) and 1g(BN1,SRC2) and 1g(BN1,(BN2 SRC1) SRC2))
     = (0g(BN1,BN2 SRC1) and 1g(BN1,SRC2))) .
red check([(bn1),(bn1;bn3),src1,src2]) .
close
--> q.e.d.

-- ========================================================================
--> (sr-3)
--  ceq (0g(BN1:Bnp,SRC:SrCh) and 1g(BN2:Bnp,SRC)) = 0g(BN1,SRC) 
--      if ((BN2 = (s BN1)) or (BN1 = (p BN2))) .
-- proof score with induction on the length of SRC
-- induction base: SRC=empBN
open (SRchPred + CONST-LITL + GENcases + CEQpd) .
-- induction base: SRC=empBN
[Bnp SrCh < Val]
eq v(BN1:Bnp,BN2:Bnp,SRC:SrCh) =
    (0g(BN1,SRC) and 1g(BN2,SRC)) = 0g(BN1,SRC) 
    if ((BN2 = (s BN1)) or (BN1 = (p BN2))) .
red check([bn1,(bn1;bn2),empBN]) .
close
-- induction step: src1 implies (bn1 src1)
mod! IS-sr-3{ex(SRchPred + CONST-LITL + GENcases + CEQpd)
-- induction hypothesis
ceq (0g(BN1:Bnp,src1) and 1g(BN2:Bnp,src1)) = 0g(BN1,src1) 
    if ((BN2 = (s BN1)) or (BN1 = (p BN2))) .
-- check
[Bnp SrCh < Val]
eq v(BN1:Bnp,BN2:Bnp,BN3:Bnp,SRC:SrCh) =
    (0g(BN1,BN3 SRC) and 1g(BN2,BN3 SRC)) = 0g(BN1,BN3 SRC) 
     if ((BN2 = (s BN1)) or (BN1 = (p BN2))) .
}
select IS-sr-3 .
:goal{eq check([bn1,(bn1;bn2),(bn1;bn2;bn3),src1]) = $ .}
:ctf{eq bn2 = p bn1 .}
:ctf{eq bn2 = s bn1 .}
:ctf{eq bn1 = p bn2 .}
--> q.e.d.

-- ========================================================================
--> (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)) .
-- proof score with induction on the length of SRC1
-- induction base: SRC1=empBN
mod! IB-sr-4 {ex(SRchPred + CONST-LITL + GENcases + CEQpd) .
-- proved fact (sr-3')
ceq (0g(BN1:Bnp,SRC:SrCh) and 1g(BN2:Bnp,SRC)) = 0g(BN1,SRC) 
     if ((BN2 = (s BN1)) or (BN1 = (p BN2))) .
-- induction base: SRC=empBN
[Bnp SrCh < Val]
eq v(BN1:Bnp,SRC1:SrCh,BN2:Bnp,SRC2:SrCh) =
    (1g(BN1,SRC1) and 0g(BN2,SRC2) and 1g(BN1,SRC1 SRC2)) =
    (1g(BN1,SRC1) and 0g(BN2,SRC2))
    if (BN2 = (p BN1)) . 
}
select IB-sr-4 .
:goal{eq check([bn1,empBN,(bn1;bn2),src2]) = $ .}
:ctf{eq bn2 = p bn1 .}
-- q.e.d.
-- induction step: src implies (bn1 src1)
mod! IS-sr-4 {ex(SRchPred + CONST-LITL + GENcases + CEQpd)
-- already proved fact (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) .
-- induction hypothesis
ceq (1g(BN1:Bnp,src1) and 0g(BN2:Bnp,SRC2:SrCh) 
                            and 1g(BN1,src1 SRC2)) = 
    (1g(BN1,src1) and 0g(BN2,SRC2)) if (BN2 = (p BN1)) .
-- check
[Bnp SrCh < Val]
eq v(BN1:Bnp,SRC1:SrCh,BN2:Bnp,SRC2:SrCh,BN3:Bnp) =
    (1g(BN1,BN3 SRC1) and 0g(BN2,SRC2) and 1g(BN1,(BN3 SRC1) SRC2)) =
    (1g(BN1,BN3 SRC1) and 0g(BN2,SRC2))
    if (BN2 = (p BN1)) .
}
select IS-sr-4 .
:goal{eq check([bn1,src1,(bn1;bn2),src2,(bn1;bn2;bn3)]) = $ .}
:ctf{eq bn2 = p bn1 .}
:ctf{eq bn3 = p bn1 .}
--> q.e.d.

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