(* 1 *) CacheState[#1] = Exclusive &&
        CacheState[#2] <> Invalid

(* 2 *) Exgntd = False &&
        MemData <> AuxData

(* 3 *) CacheState[#1] <> Invalid &&
        CacheData[#1] <> AuxData

(* 4 *) Chan2Cmd[#2] = Gnts &&
        CacheState[#1] = Exclusive

(* 5 *) Chan2Cmd[#1] = Gnte &&
        CacheState[#2] <> Invalid

(* 6 *) Chan2Cmd[#1] = Gnts &&
        Chan2Data[#1] <> AuxData

(* 7 *) Chan2Cmd[#1] = Gnte &&
        Chan2Data[#1] <> AuxData

(* 8 *) Exgntd = False &&
        CacheState[#1] = Exclusive

(* 9 *) Chan2Cmd[#1] = Gnte &&
        Chan2Cmd[#2] = Gnts

(* 10 *) CacheState[#1] <> Invalid &&
         Shrset[#1] = False

(* 11 *) Chan2Cmd[#1] = Gnte &&
         Chan2Cmd[#2] = Gnte

(* 12 *) Chan2Cmd[#1] = Gnts &&
         CacheState[#1] = Exclusive

(* 13 *) Chan2Cmd[#1] = Gnte &&
         CacheState[#1] = Exclusive

(* 14 *) Chan3Cmd[#1] = Invack &&
         CacheState[#1] = Exclusive

(* 15 *) Exgntd = False &&
         Chan2Cmd[#1] = Gnte

(* 16 *) Chan2Cmd[#1] = Gnts &&
         Shrset[#1] = False

(* 17 *) Chan3Cmd[#1] = Invack &&
         CacheState[#1] <> Invalid

(* 18 *) Chan2Cmd[#1] = Gnte &&
         Shrset[#1] = False

(* 19 *) Chan2Cmd[#1] = Gnte &&
         Chan3Cmd[#1] = Invack

(* 20 *) Chan2Cmd[#1] = Gnts &&
         Chan3Cmd[#1] = Invack

(* 21 *) Chan3Cmd[#1] = Invack &&
         Shrset[#1] = False

(* 22 *) Exgntd = False &&
         Curcmd = Reqs &&
         Chan3Cmd[#1] = Invack

(* 23 *) Chan2Cmd[#1] = Inv &&
         Shrset[#1] = False

(* 24 *) Curcmd = Empty &&
         Chan3Cmd[#1] = Invack

(* 25 *) Exgntd = False &&
         Curcmd = Reqs &&
         Chan2Cmd[#1] = Inv

(* 26 *) Invset[#1] = True &&
         Shrset[#1] = False

(* 27 *) Chan2Cmd[#1] = Inv &&
         Chan3Cmd[#1] = Invack

(* 28 *) Curcmd = Empty &&
         Chan2Cmd[#1] = Inv

(* 29 *) Chan3Cmd[#1] = Invack &&
         Invset[#1] = True

(* 30 *) Chan2Cmd[#1] = Inv &&
         Invset[#1] = True

(* 31 *) Exgntd = True &&
         Curcmd = Reqs &&
         Chan2Cmd[#1] = Inv &&
         Chan3Cmd[#2] = Invack

(* 32 *) Exgntd = True &&
         Curcmd = Reqs &&
         Chan3Cmd[#1] = Invack &&
         Chan3Cmd[#2] = Invack

(* 33 *) Chan2Cmd[#1] = Gnte &&
         Chan3Cmd[#2] = Invack

(* 34 *) Chan3Cmd[#2] = Invack &&
         CacheState[#1] = Exclusive

(* 35 *) Exgntd = True &&
         Curcmd <> Empty &&
         Chan3Cmd[#1] = Invack &&
         Chan3Data[#1] <> AuxData

(* 36 *) Exgntd = True &&
         Curcmd = Reqs &&
         Chan2Cmd[#1] = Empty &&
         Chan3Cmd[#2] = Invack &&
         Invset[#1] = True

(* 37 *) Exgntd = True &&
         Curcmd = Reqs &&
         Chan2Cmd[#1] = Inv &&
         Chan2Cmd[#2] = Inv &&
         Chan3Cmd[#2] = Empty

(* 38 *) Chan2Cmd[#1] = Gnte &&
         Chan2Cmd[#2] = Inv

(* 39 *) Chan2Cmd[#2] = Inv &&
         CacheState[#1] = Exclusive

(* 40 *) Exgntd = True &&
         Curcmd <> Empty &&
         Chan2Cmd[#1] = Inv &&
         Chan3Cmd[#1] = Empty &&
         Chan3Data[#1] <> AuxData &&
         CacheData[#1] <> AuxData

(* 41 *) Exgntd = True &&
         Curcmd <> Empty &&
         Chan2Cmd[#1] = Inv &&
         Chan3Cmd[#1] = Empty &&
         Chan3Data[#1] <> AuxData &&
         CacheState[#1] <> Exclusive

(* 42 *) Exgntd = True &&
         Curcmd = Reqs &&
         Chan2Cmd[#1] = Empty &&
         Chan2Cmd[#2] = Inv &&
         Chan3Cmd[#2] = Empty &&
         Invset[#1] = True

(* 43 *) Exgntd = True &&
         Chan2Cmd[#1] = Gnts

(* 44 *) Chan2Cmd[#1] = Gnte &&
         Invset[#2] = True

(* 45 *) CacheState[#1] = Exclusive &&
         Invset[#2] = True

(* 46 *) Exgntd = True &&
         Curcmd = Reqe &&
         Chan2Cmd[#1] = Empty &&
         Chan3Cmd[#1] = Empty &&
         Chan3Data[#1] <> AuxData &&
         CacheData[#1] <> AuxData &&
         Invset[#1] = True

(* 47 *) Exgntd = True &&
         Curcmd = Reqs &&
         Chan2Cmd[#1] = Empty &&
         Chan3Cmd[#1] = Empty &&
         Chan3Data[#1] <> AuxData &&
         CacheData[#1] <> AuxData &&
         Invset[#1] = True

(* 48 *) Exgntd = True &&
         Curcmd = Reqe &&
         Chan2Cmd[#1] = Empty &&
         Chan3Cmd[#1] = Empty &&
         Chan3Data[#1] <> AuxData &&
         CacheState[#1] <> Exclusive &&
         Invset[#1] = True

(* 49 *) Exgntd = True &&
         Curcmd = Reqs &&
         Chan2Cmd[#1] = Empty &&
         Chan3Cmd[#1] = Empty &&
         Chan3Data[#1] <> AuxData &&
         CacheState[#1] <> Exclusive &&
         Invset[#1] = True

(* 50 *) Exgntd = True &&
         Curcmd = Reqs &&
         Chan2Cmd[#1] = Empty &&
         Chan2Cmd[#2] = Empty &&
         Chan3Cmd[#2] = Empty &&
         Invset[#1] = True &&
         Invset[#2] = True

(* 51 *) Chan2Cmd[#1] = Gnte &&
         Shrset[#2] = True

(* 52 *) CacheState[#1] = Exclusive &&
         Shrset[#2] = True

(* 53 *) Exgntd = True &&
         Curcmd = Empty &&
         Chan1Cmd[#1] = Reqe &&
         Chan2Cmd[#1] = Empty &&
         Chan3Cmd[#1] = Empty &&
         Chan3Data[#1] <> AuxData &&
         CacheData[#1] <> AuxData &&
         Shrset[#1] = True

(* 54 *) Exgntd = True &&
         Curcmd = Empty &&
         Chan1Cmd[#1] = Reqs &&
         Chan2Cmd[#1] = Empty &&
         Chan3Cmd[#1] = Empty &&
         Chan3Data[#1] <> AuxData &&
         CacheData[#1] <> AuxData &&
         Shrset[#1] = True

(* 55 *) Exgntd = True &&
         Curcmd = Empty &&
         Chan1Cmd[#1] = Reqe &&
         Chan2Cmd[#1] = Empty &&
         Chan3Cmd[#1] = Empty &&
         Chan3Data[#1] <> AuxData &&
         CacheState[#1] <> Exclusive &&
         Shrset[#1] = True

(* 56 *) Exgntd = True &&
         Curcmd = Empty &&
         Chan1Cmd[#1] = Reqs &&
         Chan2Cmd[#1] = Empty &&
         Chan3Cmd[#1] = Empty &&
         Chan3Data[#1] <> AuxData &&
         CacheState[#1] <> Exclusive &&
         Shrset[#1] = True

(* 57 *) Exgntd = True &&
         Curcmd = Empty &&
         Chan1Cmd[#1] = Reqs &&
         Chan2Cmd[#1] = Empty &&
         Chan2Cmd[#2] = Empty &&
         Chan3Cmd[#2] = Empty &&
         Shrset[#1] = True &&
         Shrset[#2] = True

(* 58 *) Exgntd = True &&
         Curcmd = Empty &&
         Chan1Cmd[#1] = Empty &&
         Chan2Cmd[#1] = Empty &&
         Chan3Cmd[#1] = Empty &&
         Chan3Data[#1] <> AuxData &&
         CacheState[#1] <> Exclusive &&
         CacheData[#1] <> AuxData &&
         Shrset[#1] = True

(* 59 *) Exgntd = True &&
         Curcmd = Empty &&
         Chan1Cmd[#1] = Empty &&
         Chan2Cmd[#1] = Empty &&
         Chan3Cmd[#1] = Empty &&
         Chan3Data[#1] <> AuxData &&
         CacheState[#1] <> Exclusive &&
         Shrset[#1] = True

(* 60 *) Exgntd = True &&
         Curcmd = Empty &&
         Chan1Cmd[#1] = Empty &&
         Chan2Cmd[#1] = Empty &&
         Chan2Cmd[#2] = Empty &&
         Chan3Cmd[#2] = Empty &&
         CacheState[#1] = Invalid &&
         Shrset[#1] = True &&
         Shrset[#2] = True

(* 61 *) Exgntd = True &&
         Curcmd = Empty &&
         Chan1Cmd[#3] = Reqs &&
         Chan2Cmd[#1] = Empty &&
         Chan2Cmd[#2] = Empty &&
         Chan3Cmd[#2] = Empty &&
         Shrset[#1] = True &&
         Shrset[#2] = True

(* 62 *) Exgntd = True &&
         Curcmd = Empty &&
         Chan1Cmd[#3] = Empty &&
         Chan2Cmd[#1] = Empty &&
         Chan2Cmd[#2] = Empty &&
         Chan3Cmd[#2] = Empty &&
         CacheState[#3] = Invalid &&
         Shrset[#1] = True &&
         Shrset[#2] = True