(* 1 *) CacheState_home = CACHE_E &&
        CacheState[#1] = CACHE_E

(* 2 *) CacheState[#1] = CACHE_E &&
        CacheState[#2] = CACHE_E

(* 3 *) Dir_Dirty = False &&
        CacheState[#1] = CACHE_E

(* 4 *) UniMsg_Cmd_home = UNI_PutX &&
        CacheState[#1] = CACHE_E

(* 5 *) Home <> #1 &&
        CacheState_home = CACHE_E &&
        UniMsg_Cmd[#1] = UNI_PutX

(* 6 *) Home <> #1 &&
        CacheState[#2] = CACHE_E &&
        UniMsg_Cmd[#1] = UNI_PutX

(* 7 *) InvMarked_home = True

(* 8 *) UniMsg_Cmd_home = UNI_Put &&
        CacheState[#1] = CACHE_E

(* 9 *) Home <> #1 &&
        Dir_Dirty = False &&
        UniMsg_Cmd[#1] = UNI_PutX

(* 10 *) WbMsg_Cmd = WB_Wb &&
         CacheState[#1] = CACHE_E

(* 11 *) ShWbMsg_Cmd = SHWB_ShWb &&
         ShWbMsg_Proc = Home

(* 12 *) ShWbMsg_Cmd = SHWB_ShWb &&
         CacheState[#1] = CACHE_E

(* 13 *) Home <> #1 &&
         UniMsg_Cmd_home = UNI_PutX &&
         UniMsg_Cmd[#1] = UNI_PutX

(* 14 *) CacheState_home = CACHE_E &&
         Dir_HeadVld = True

(* 15 *) Home <> #1 &&
         Home <> #2 &&
         UniMsg_Cmd[#1] = UNI_PutX &&
         UniMsg_Cmd[#2] = UNI_PutX

(* 16 *) Home <> #1 &&
         UniMsg_Cmd_home = UNI_Put &&
         UniMsg_Cmd[#1] = UNI_PutX

(* 17 *) Home <> #1 &&
         WbMsg_Cmd = WB_Wb &&
         UniMsg_Cmd[#1] = UNI_PutX

(* 18 *) Home <> #1 &&
         ShWbMsg_Cmd = SHWB_ShWb &&
         UniMsg_Cmd[#1] = UNI_PutX

(* 19 *) UniMsg_Cmd_home = UNI_PutX &&
         Dir_HeadVld = False

(* 20 *) UniMsg_Cmd_home = UNI_PutX &&
         Dir_Dirty = False

(* 21 *) Home <> #1 &&
         CacheState[#1] = CACHE_E &&
         UniMsg_Cmd[#1] = UNI_PutX

(* 22 *) UniMsg_Cmd_home = UNI_Put &&
         Dir_HeadVld = False

(* 23 *) UniMsg_Cmd_home = UNI_Put &&
         Dir_Dirty = False

(* 24 *) Dir_HeadVld = False &&
         WbMsg_Cmd = WB_Wb

(* 25 *) Dir_Dirty = False &&
         WbMsg_Cmd = WB_Wb

(* 26 *) Dir_HeadVld = False &&
         ShWbMsg_Cmd = SHWB_ShWb

(* 27 *) Dir_Dirty = False &&
         ShWbMsg_Cmd = SHWB_ShWb

(* 28 *) UniMsg_Cmd_home = UNI_PutX &&
         WbMsg_Cmd = WB_Wb

(* 29 *) UniMsg_Cmd_home = UNI_PutX &&
         ShWbMsg_Cmd = SHWB_ShWb

(* 30 *) UniMsg_Cmd_home = UNI_Put &&
         WbMsg_Cmd = WB_Wb

(* 31 *) UniMsg_Cmd_home = UNI_Put &&
         ShWbMsg_Cmd = SHWB_ShWb

(* 32 *) WbMsg_Cmd = WB_Wb &&
         ShWbMsg_Cmd = SHWB_ShWb

(* 33 *) Home <> #1 &&
         Dir_HeadVld = False &&
         CacheState[#1] = CACHE_E

(* 34 *) CacheState_home = CACHE_E &&
         Dir_Dirty = False

(* 35 *) ProcCmd_home = NODE_Get &&
         Dir_Local = True

(* 36 *) Home <> #1 &&
         Dir_HeadVld = False &&
         UniMsg_Cmd[#1] = UNI_PutX

(* 37 *) CacheState_home = CACHE_I &&
         Dir_Local = True &&
         Dir_Dirty = True