kings-crown/FVELER_Isabelle huggingface dataset:
theory Types_H

lemma bifITCNodeSizeBits_bifNumIOPTLevels_update [simp]:
  "bifITCNodeSizeBits (bifNumIOPTLevels_update f v) = bifITCNodeSizeBits v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bifITCNodeSizeBits (bifNumIOPTLevels_update f v) = bifITCNodeSizeBits v
theory Types_H

lemma bifITCNodeSizeBits_bifIPCBufVPtr_update [simp]:
  "bifITCNodeSizeBits (bifIPCBufVPtr_update f v) = bifITCNodeSizeBits v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bifITCNodeSizeBits (bifIPCBufVPtr_update f v) = bifITCNodeSizeBits v
theory Types_H

lemma bifITCNodeSizeBits_bifNullCaps_update [simp]:
  "bifITCNodeSizeBits (bifNullCaps_update f v) = bifITCNodeSizeBits v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bifITCNodeSizeBits (bifNullCaps_update f v) = bifITCNodeSizeBits v
theory Types_H

lemma bifITCNodeSizeBits_bifSharedFrameCaps_update [simp]:
  "bifITCNodeSizeBits (bifSharedFrameCaps_update f v) = bifITCNodeSizeBits v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bifITCNodeSizeBits (bifSharedFrameCaps_update f v) = bifITCNodeSizeBits v
theory Types_H

lemma bifITCNodeSizeBits_bifUIFrameCaps_update [simp]:
  "bifITCNodeSizeBits (bifUIFrameCaps_update f v) = bifITCNodeSizeBits v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bifITCNodeSizeBits (bifUIFrameCaps_update f v) = bifITCNodeSizeBits v
theory Types_H

lemma bifITCNodeSizeBits_bifUIPDCaps_update [simp]:
  "bifITCNodeSizeBits (bifUIPDCaps_update f v) = bifITCNodeSizeBits v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bifITCNodeSizeBits (bifUIPDCaps_update f v) = bifITCNodeSizeBits v
theory Types_H

lemma bifITCNodeSizeBits_bifUIPTCaps_update [simp]:
  "bifITCNodeSizeBits (bifUIPTCaps_update f v) = bifITCNodeSizeBits v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bifITCNodeSizeBits (bifUIPTCaps_update f v) = bifITCNodeSizeBits v
theory Types_H

lemma bifITCNodeSizeBits_bifUntypedObjCaps_update [simp]:
  "bifITCNodeSizeBits (bifUntypedObjCaps_update f v) = bifITCNodeSizeBits v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bifITCNodeSizeBits (bifUntypedObjCaps_update f v) = bifITCNodeSizeBits v
theory Types_H

lemma bifITCNodeSizeBits_bifUntypedObjPAddrs_update [simp]:
  "bifITCNodeSizeBits (bifUntypedObjPAddrs_update f v) = bifITCNodeSizeBits v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bifITCNodeSizeBits (bifUntypedObjPAddrs_update f v) = bifITCNodeSizeBits v
theory Types_H

lemma bifITCNodeSizeBits_bifUntypedObjSizeBits_update [simp]:
  "bifITCNodeSizeBits (bifUntypedObjSizeBits_update f v) = bifITCNodeSizeBits v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bifITCNodeSizeBits (bifUntypedObjSizeBits_update f v) = bifITCNodeSizeBits v
theory Types_H

lemma bifITCNodeSizeBits_bifUntypedObjIsDeviceList_update [simp]:
  "bifITCNodeSizeBits (bifUntypedObjIsDeviceList_update f v) = bifITCNodeSizeBits v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bifITCNodeSizeBits (bifUntypedObjIsDeviceList_update f v) = bifITCNodeSizeBits v
theory Types_H

lemma bifITCNodeSizeBits_bifITCNodeSizeBits_update [simp]:
  "bifITCNodeSizeBits (bifITCNodeSizeBits_update f v) = f (bifITCNodeSizeBits v)" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bifITCNodeSizeBits (bifITCNodeSizeBits_update f v) = f (bifITCNodeSizeBits v)
theory Types_H

lemma bifITCNodeSizeBits_bifNumDeviceRegions_update [simp]:
  "bifITCNodeSizeBits (bifNumDeviceRegions_update f v) = bifITCNodeSizeBits v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bifITCNodeSizeBits (bifNumDeviceRegions_update f v) = bifITCNodeSizeBits v
theory Types_H

lemma bifITCNodeSizeBits_bifDeviceRegions_update [simp]:
  "bifITCNodeSizeBits (bifDeviceRegions_update f v) = bifITCNodeSizeBits v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bifITCNodeSizeBits (bifDeviceRegions_update f v) = bifITCNodeSizeBits v
theory Types_H

lemma bifNumDeviceRegions_bifNodeID_update [simp]:
  "bifNumDeviceRegions (bifNodeID_update f v) = bifNumDeviceRegions v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bifNumDeviceRegions (bifNodeID_update f v) = bifNumDeviceRegions v
theory Types_H

lemma bifNumDeviceRegions_bifNumNodes_update [simp]:
  "bifNumDeviceRegions (bifNumNodes_update f v) = bifNumDeviceRegions v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bifNumDeviceRegions (bifNumNodes_update f v) = bifNumDeviceRegions v
theory Types_H

lemma bifNumDeviceRegions_bifNumIOPTLevels_update [simp]:
  "bifNumDeviceRegions (bifNumIOPTLevels_update f v) = bifNumDeviceRegions v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bifNumDeviceRegions (bifNumIOPTLevels_update f v) = bifNumDeviceRegions v
theory Types_H

lemma bifNumDeviceRegions_bifIPCBufVPtr_update [simp]:
  "bifNumDeviceRegions (bifIPCBufVPtr_update f v) = bifNumDeviceRegions v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bifNumDeviceRegions (bifIPCBufVPtr_update f v) = bifNumDeviceRegions v
theory Types_H

lemma bifNumDeviceRegions_bifNullCaps_update [simp]:
  "bifNumDeviceRegions (bifNullCaps_update f v) = bifNumDeviceRegions v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bifNumDeviceRegions (bifNullCaps_update f v) = bifNumDeviceRegions v
theory Types_H

lemma bifNumDeviceRegions_bifSharedFrameCaps_update [simp]:
  "bifNumDeviceRegions (bifSharedFrameCaps_update f v) = bifNumDeviceRegions v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bifNumDeviceRegions (bifSharedFrameCaps_update f v) = bifNumDeviceRegions v
theory Types_H

lemma bifNumDeviceRegions_bifUIFrameCaps_update [simp]:
  "bifNumDeviceRegions (bifUIFrameCaps_update f v) = bifNumDeviceRegions v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bifNumDeviceRegions (bifUIFrameCaps_update f v) = bifNumDeviceRegions v
theory Types_H

lemma bifNumDeviceRegions_bifUIPDCaps_update [simp]:
  "bifNumDeviceRegions (bifUIPDCaps_update f v) = bifNumDeviceRegions v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bifNumDeviceRegions (bifUIPDCaps_update f v) = bifNumDeviceRegions v
theory Types_H

lemma bifNumDeviceRegions_bifUIPTCaps_update [simp]:
  "bifNumDeviceRegions (bifUIPTCaps_update f v) = bifNumDeviceRegions v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bifNumDeviceRegions (bifUIPTCaps_update f v) = bifNumDeviceRegions v
theory Types_H

lemma bifNumDeviceRegions_bifUntypedObjCaps_update [simp]:
  "bifNumDeviceRegions (bifUntypedObjCaps_update f v) = bifNumDeviceRegions v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bifNumDeviceRegions (bifUntypedObjCaps_update f v) = bifNumDeviceRegions v
theory Types_H

lemma bifNumDeviceRegions_bifUntypedObjSizeBits_update [simp]:
  "bifNumDeviceRegions (bifUntypedObjSizeBits_update f v) = bifNumDeviceRegions v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bifNumDeviceRegions (bifUntypedObjSizeBits_update f v) = bifNumDeviceRegions v
theory Types_H

lemma bifNumDeviceRegions_bifUntypedObjIsDeviceList_update [simp]:
  "bifNumDeviceRegions (bifUntypedObjIsDeviceList_update f v) = bifNumDeviceRegions v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bifNumDeviceRegions (bifUntypedObjIsDeviceList_update f v) = bifNumDeviceRegions v
theory Types_H

lemma bifNumDeviceRegions_bifITCNodeSizeBits_update [simp]:
  "bifNumDeviceRegions (bifITCNodeSizeBits_update f v) = bifNumDeviceRegions v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bifNumDeviceRegions (bifITCNodeSizeBits_update f v) = bifNumDeviceRegions v
theory Types_H

lemma bifNumDeviceRegions_bifNumDeviceRegions_update [simp]:
  "bifNumDeviceRegions (bifNumDeviceRegions_update f v) = f (bifNumDeviceRegions v)" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bifNumDeviceRegions (bifNumDeviceRegions_update f v) = f (bifNumDeviceRegions v)
theory Types_H

lemma bifNumDeviceRegions_bifDeviceRegions_update [simp]:
  "bifNumDeviceRegions (bifDeviceRegions_update f v) = bifNumDeviceRegions v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bifNumDeviceRegions (bifDeviceRegions_update f v) = bifNumDeviceRegions v
theory Types_H

lemma bifDeviceRegions_bifNodeID_update [simp]:
  "bifDeviceRegions (bifNodeID_update f v) = bifDeviceRegions v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bifDeviceRegions (bifNodeID_update f v) = bifDeviceRegions v
theory Types_H

lemma bifDeviceRegions_bifNumNodes_update [simp]:
  "bifDeviceRegions (bifNumNodes_update f v) = bifDeviceRegions v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bifDeviceRegions (bifNumNodes_update f v) = bifDeviceRegions v
theory Types_H

lemma bifDeviceRegions_bifNumIOPTLevels_update [simp]:
  "bifDeviceRegions (bifNumIOPTLevels_update f v) = bifDeviceRegions v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bifDeviceRegions (bifNumIOPTLevels_update f v) = bifDeviceRegions v
theory Types_H

lemma bifDeviceRegions_bifIPCBufVPtr_update [simp]:
  "bifDeviceRegions (bifIPCBufVPtr_update f v) = bifDeviceRegions v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bifDeviceRegions (bifIPCBufVPtr_update f v) = bifDeviceRegions v
theory Types_H

lemma bifDeviceRegions_bifNullCaps_update [simp]:
  "bifDeviceRegions (bifNullCaps_update f v) = bifDeviceRegions v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bifDeviceRegions (bifNullCaps_update f v) = bifDeviceRegions v
theory Types_H

lemma bifDeviceRegions_bifSharedFrameCaps_update [simp]:
  "bifDeviceRegions (bifSharedFrameCaps_update f v) = bifDeviceRegions v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bifDeviceRegions (bifSharedFrameCaps_update f v) = bifDeviceRegions v
theory Types_H

lemma bifDeviceRegions_bifUIFrameCaps_update [simp]:
  "bifDeviceRegions (bifUIFrameCaps_update f v) = bifDeviceRegions v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bifDeviceRegions (bifUIFrameCaps_update f v) = bifDeviceRegions v
theory Types_H

lemma bifDeviceRegions_bifUIPDCaps_update [simp]:
  "bifDeviceRegions (bifUIPDCaps_update f v) = bifDeviceRegions v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bifDeviceRegions (bifUIPDCaps_update f v) = bifDeviceRegions v
theory Types_H

lemma bifDeviceRegions_bifUIPTCaps_update [simp]:
  "bifDeviceRegions (bifUIPTCaps_update f v) = bifDeviceRegions v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bifDeviceRegions (bifUIPTCaps_update f v) = bifDeviceRegions v
theory Types_H

lemma bifDeviceRegions_bifUntypedObjCaps_update [simp]:
  "bifDeviceRegions (bifUntypedObjCaps_update f v) = bifDeviceRegions v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bifDeviceRegions (bifUntypedObjCaps_update f v) = bifDeviceRegions v
theory Types_H

lemma bifDeviceRegions_bifUntypedObjPAddrs_update [simp]:
  "bifDeviceRegions (bifUntypedObjPAddrs_update f v) = bifDeviceRegions v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bifDeviceRegions (bifUntypedObjPAddrs_update f v) = bifDeviceRegions v
theory Types_H

lemma bifDeviceRegions_bifUntypedObjSizeBits_update [simp]:
  "bifDeviceRegions (bifUntypedObjSizeBits_update f v) = bifDeviceRegions v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bifDeviceRegions (bifUntypedObjSizeBits_update f v) = bifDeviceRegions v
theory Types_H

lemma bifDeviceRegions_bifUntypedObjIsDeviceList_update [simp]:
  "bifDeviceRegions (bifUntypedObjIsDeviceList_update f v) = bifDeviceRegions v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bifDeviceRegions (bifUntypedObjIsDeviceList_update f v) = bifDeviceRegions v
theory Types_H

lemma bifDeviceRegions_bifITCNodeSizeBits_update [simp]:
  "bifDeviceRegions (bifITCNodeSizeBits_update f v) = bifDeviceRegions v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bifDeviceRegions (bifITCNodeSizeBits_update f v) = bifDeviceRegions v
theory Types_H

lemma bifDeviceRegions_bifNumDeviceRegions_update [simp]:
  "bifDeviceRegions (bifNumDeviceRegions_update f v) = bifDeviceRegions v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bifDeviceRegions (bifNumDeviceRegions_update f v) = bifDeviceRegions v
theory Types_H

lemma bifDeviceRegions_bifDeviceRegions_update [simp]:
  "bifDeviceRegions (bifDeviceRegions_update f v) = f (bifDeviceRegions v)" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bifDeviceRegions (bifDeviceRegions_update f v) = f (bifDeviceRegions v)
theory Types_H

lemma initFreeMemory_initFreeMemory_update [simp]:
  "initFreeMemory (initFreeMemory_update f v) = f (initFreeMemory v)" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. initFreeMemory (initFreeMemory_update f v) = f (initFreeMemory v)
theory Types_H

lemma initFreeMemory_initSlotPosCur_update [simp]:
  "initFreeMemory (initSlotPosCur_update f v) = initFreeMemory v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. initFreeMemory (initSlotPosCur_update f v) = initFreeMemory v
theory Types_H

lemma initFreeMemory_initSlotPosMax_update [simp]:
  "initFreeMemory (initSlotPosMax_update f v) = initFreeMemory v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. initFreeMemory (initSlotPosMax_update f v) = initFreeMemory v
theory Types_H

lemma initFreeMemory_initBootInfo_update [simp]:
  "initFreeMemory (initBootInfo_update f v) = initFreeMemory v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. initFreeMemory (initBootInfo_update f v) = initFreeMemory v
theory Types_H

lemma initFreeMemory_initVPtrOffset_update [simp]:
  "initFreeMemory (initVPtrOffset_update f v) = initFreeMemory v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. initFreeMemory (initVPtrOffset_update f v) = initFreeMemory v
theory Types_H

lemma initFreeMemory_initBootInfoFrame_update [simp]:
  "initFreeMemory (initBootInfoFrame_update f v) = initFreeMemory v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. initFreeMemory (initBootInfoFrame_update f v) = initFreeMemory v
theory Types_H

lemma initSlotPosCur_initFreeMemory_update [simp]:
  "initSlotPosCur (initFreeMemory_update f v) = initSlotPosCur v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. initSlotPosCur (initFreeMemory_update f v) = initSlotPosCur v
theory Types_H

lemma initSlotPosCur_initSlotPosCur_update [simp]:
  "initSlotPosCur (initSlotPosCur_update f v) = f (initSlotPosCur v)" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. initSlotPosCur (initSlotPosCur_update f v) = f (initSlotPosCur v)
theory Types_H

lemma initSlotPosCur_initSlotPosMax_update [simp]:
  "initSlotPosCur (initSlotPosMax_update f v) = initSlotPosCur v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. initSlotPosCur (initSlotPosMax_update f v) = initSlotPosCur v
theory Types_H

lemma initSlotPosCur_initBootInfo_update [simp]:
  "initSlotPosCur (initBootInfo_update f v) = initSlotPosCur v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. initSlotPosCur (initBootInfo_update f v) = initSlotPosCur v
theory Types_H

lemma initSlotPosCur_initVPtrOffset_update [simp]:
  "initSlotPosCur (initVPtrOffset_update f v) = initSlotPosCur v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. initSlotPosCur (initVPtrOffset_update f v) = initSlotPosCur v
theory Types_H

lemma initSlotPosCur_initBootInfoFrame_update [simp]:
  "initSlotPosCur (initBootInfoFrame_update f v) = initSlotPosCur v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. initSlotPosCur (initBootInfoFrame_update f v) = initSlotPosCur v
theory Types_H

lemma initSlotPosMax_initFreeMemory_update [simp]:
  "initSlotPosMax (initFreeMemory_update f v) = initSlotPosMax v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. initSlotPosMax (initFreeMemory_update f v) = initSlotPosMax v
theory Types_H

lemma initSlotPosMax_initSlotPosCur_update [simp]:
  "initSlotPosMax (initSlotPosCur_update f v) = initSlotPosMax v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. initSlotPosMax (initSlotPosCur_update f v) = initSlotPosMax v
theory Types_H

lemma initSlotPosMax_initBootInfo_update [simp]:
  "initSlotPosMax (initBootInfo_update f v) = initSlotPosMax v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. initSlotPosMax (initBootInfo_update f v) = initSlotPosMax v
theory Types_H

lemma initSlotPosMax_initVPtrOffset_update [simp]:
  "initSlotPosMax (initVPtrOffset_update f v) = initSlotPosMax v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. initSlotPosMax (initVPtrOffset_update f v) = initSlotPosMax v
theory Types_H

lemma initSlotPosMax_initBootInfoFrame_update [simp]:
  "initSlotPosMax (initBootInfoFrame_update f v) = initSlotPosMax v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. initSlotPosMax (initBootInfoFrame_update f v) = initSlotPosMax v
theory Types_H

lemma initBootInfo_initFreeMemory_update [simp]:
  "initBootInfo (initFreeMemory_update f v) = initBootInfo v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. initBootInfo (initFreeMemory_update f v) = initBootInfo v
theory Types_H

lemma initBootInfo_initSlotPosCur_update [simp]:
  "initBootInfo (initSlotPosCur_update f v) = initBootInfo v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. initBootInfo (initSlotPosCur_update f v) = initBootInfo v
theory Types_H

lemma initBootInfo_initSlotPosMax_update [simp]:
  "initBootInfo (initSlotPosMax_update f v) = initBootInfo v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. initBootInfo (initSlotPosMax_update f v) = initBootInfo v
theory Types_H

lemma initBootInfo_initBootInfo_update [simp]:
  "initBootInfo (initBootInfo_update f v) = f (initBootInfo v)" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. initBootInfo (initBootInfo_update f v) = f (initBootInfo v)
theory Types_H

lemma initBootInfo_initVPtrOffset_update [simp]:
  "initBootInfo (initVPtrOffset_update f v) = initBootInfo v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. initBootInfo (initVPtrOffset_update f v) = initBootInfo v
theory Types_H

lemma initBootInfo_initBootInfoFrame_update [simp]:
  "initBootInfo (initBootInfoFrame_update f v) = initBootInfo v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. initBootInfo (initBootInfoFrame_update f v) = initBootInfo v
theory Types_H

lemma initVPtrOffset_initFreeMemory_update [simp]:
  "initVPtrOffset (initFreeMemory_update f v) = initVPtrOffset v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. initVPtrOffset (initFreeMemory_update f v) = initVPtrOffset v
theory Types_H

lemma initVPtrOffset_initSlotPosCur_update [simp]:
  "initVPtrOffset (initSlotPosCur_update f v) = initVPtrOffset v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. initVPtrOffset (initSlotPosCur_update f v) = initVPtrOffset v
theory Types_H

lemma initVPtrOffset_initSlotPosMax_update [simp]:
  "initVPtrOffset (initSlotPosMax_update f v) = initVPtrOffset v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. initVPtrOffset (initSlotPosMax_update f v) = initVPtrOffset v
theory Types_H

lemma initVPtrOffset_initBootInfo_update [simp]:
  "initVPtrOffset (initBootInfo_update f v) = initVPtrOffset v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. initVPtrOffset (initBootInfo_update f v) = initVPtrOffset v
theory Types_H

lemma initVPtrOffset_initVPtrOffset_update [simp]:
  "initVPtrOffset (initVPtrOffset_update f v) = f (initVPtrOffset v)" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. initVPtrOffset (initVPtrOffset_update f v) = f (initVPtrOffset v)
theory Types_H

lemma initVPtrOffset_initBootInfoFrame_update [simp]:
  "initVPtrOffset (initBootInfoFrame_update f v) = initVPtrOffset v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. initVPtrOffset (initBootInfoFrame_update f v) = initVPtrOffset v
theory Types_H

lemma initBootInfoFrame_initFreeMemory_update [simp]:
  "initBootInfoFrame (initFreeMemory_update f v) = initBootInfoFrame v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. initBootInfoFrame (initFreeMemory_update f v) = initBootInfoFrame v
theory Types_H

lemma initBootInfoFrame_initSlotPosCur_update [simp]:
  "initBootInfoFrame (initSlotPosCur_update f v) = initBootInfoFrame v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. initBootInfoFrame (initSlotPosCur_update f v) = initBootInfoFrame v
theory Types_H

lemma initBootInfoFrame_initBootInfo_update [simp]:
  "initBootInfoFrame (initBootInfo_update f v) = initBootInfoFrame v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. initBootInfoFrame (initBootInfo_update f v) = initBootInfoFrame v
theory Types_H

lemma initBootInfoFrame_initVPtrOffset_update [simp]:
  "initBootInfoFrame (initVPtrOffset_update f v) = initBootInfoFrame v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. initBootInfoFrame (initVPtrOffset_update f v) = initBootInfoFrame v
theory Types_H

lemma initBootInfoFrame_initBootInfoFrame_update [simp]:
  "initBootInfoFrame (initBootInfoFrame_update f v) = f (initBootInfoFrame v)" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. initBootInfoFrame (initBootInfoFrame_update f v) = f (initBootInfoFrame v)
theory ArchFault_H

lemma vmFaultAddress_vmFaultAddress_update [simp]:
  "vmFaultAddress (vmFaultAddress_update f v) = f (vmFaultAddress v)" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. vmFaultAddress (vmFaultAddress_update f v) = f (vmFaultAddress v)
theory ArchFault_H

lemma vmFaultAddress_vmFaultArchData_update [simp]:
  "vmFaultAddress (vmFaultArchData_update f v) = vmFaultAddress v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. vmFaultAddress (vmFaultArchData_update f v) = vmFaultAddress v
theory ArchFault_H

lemma vmFaultArchData_vmFaultAddress_update [simp]:
  "vmFaultArchData (vmFaultAddress_update f v) = vmFaultArchData v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. vmFaultArchData (vmFaultAddress_update f v) = vmFaultArchData v
theory ArchFault_H

lemma vmFaultArchData_vmFaultArchData_update [simp]:
  "vmFaultArchData (vmFaultArchData_update f v) = f (vmFaultArchData v)" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. vmFaultArchData (vmFaultArchData_update f v) = f (vmFaultArchData v)
theory ArchStructures_H

lemma atcbContext_atcbContext_update [simp]:
  "atcbContext (atcbContext_update f v) = f (atcbContext v)" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. atcbContext (atcbContext_update f v) = f (atcbContext v)
theory Structures_H

lemma ntfnObj_ntfnObj_update [simp]:
  "ntfnObj (ntfnObj_update f v) = f (ntfnObj v)" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ntfnObj (ntfnObj_update f v) = f (ntfnObj v)