kings-crown/FVELER_Isabelle huggingface dataset:
theory Types_H

lemma bifNumNodes_bifUntypedObjIsDeviceList_update [simp]:
  "bifNumNodes (bifUntypedObjIsDeviceList_update f v) = bifNumNodes v" by (cases v) simp

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

lemma bifNumNodes_bifITCNodeSizeBits_update [simp]:
  "bifNumNodes (bifITCNodeSizeBits_update f v) = bifNumNodes v" by (cases v) simp

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

lemma bifNumNodes_bifNumDeviceRegions_update [simp]:
  "bifNumNodes (bifNumDeviceRegions_update f v) = bifNumNodes v" by (cases v) simp

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

lemma bifNumNodes_bifDeviceRegions_update [simp]:
  "bifNumNodes (bifDeviceRegions_update f v) = bifNumNodes v" by (cases v) simp

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

lemma bifNumIOPTLevels_bifNodeID_update [simp]:
  "bifNumIOPTLevels (bifNodeID_update f v) = bifNumIOPTLevels v" by (cases v) simp

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

lemma bifNumIOPTLevels_bifNumIOPTLevels_update [simp]:
  "bifNumIOPTLevels (bifNumIOPTLevels_update f v) = f (bifNumIOPTLevels v)" by (cases v) simp

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

lemma bifNumIOPTLevels_bifIPCBufVPtr_update [simp]:
  "bifNumIOPTLevels (bifIPCBufVPtr_update f v) = bifNumIOPTLevels v" by (cases v) simp

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

lemma bifNumIOPTLevels_bifNullCaps_update [simp]:
  "bifNumIOPTLevels (bifNullCaps_update f v) = bifNumIOPTLevels v" by (cases v) simp

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

lemma bifNumIOPTLevels_bifSharedFrameCaps_update [simp]:
  "bifNumIOPTLevels (bifSharedFrameCaps_update f v) = bifNumIOPTLevels v" by (cases v) simp

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

lemma bifNumIOPTLevels_bifUIFrameCaps_update [simp]:
  "bifNumIOPTLevels (bifUIFrameCaps_update f v) = bifNumIOPTLevels v" by (cases v) simp

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

lemma bifNumIOPTLevels_bifUIPDCaps_update [simp]:
  "bifNumIOPTLevels (bifUIPDCaps_update f v) = bifNumIOPTLevels v" by (cases v) simp

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

lemma bifNumIOPTLevels_bifUIPTCaps_update [simp]:
  "bifNumIOPTLevels (bifUIPTCaps_update f v) = bifNumIOPTLevels v" by (cases v) simp

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

lemma bifNumIOPTLevels_bifUntypedObjCaps_update [simp]:
  "bifNumIOPTLevels (bifUntypedObjCaps_update f v) = bifNumIOPTLevels v" by (cases v) simp

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

lemma bifNumIOPTLevels_bifUntypedObjPAddrs_update [simp]:
  "bifNumIOPTLevels (bifUntypedObjPAddrs_update f v) = bifNumIOPTLevels v" by (cases v) simp

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

lemma bifNumIOPTLevels_bifUntypedObjSizeBits_update [simp]:
  "bifNumIOPTLevels (bifUntypedObjSizeBits_update f v) = bifNumIOPTLevels v" by (cases v) simp

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

lemma bifNumIOPTLevels_bifUntypedObjIsDeviceList_update [simp]:
  "bifNumIOPTLevels (bifUntypedObjIsDeviceList_update f v) = bifNumIOPTLevels v" by (cases v) simp

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

lemma bifNumIOPTLevels_bifITCNodeSizeBits_update [simp]:
  "bifNumIOPTLevels (bifITCNodeSizeBits_update f v) = bifNumIOPTLevels v" by (cases v) simp

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

lemma bifNumIOPTLevels_bifNumDeviceRegions_update [simp]:
  "bifNumIOPTLevels (bifNumDeviceRegions_update f v) = bifNumIOPTLevels v" by (cases v) simp

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

lemma bifNumIOPTLevels_bifDeviceRegions_update [simp]:
  "bifNumIOPTLevels (bifDeviceRegions_update f v) = bifNumIOPTLevels v" by (cases v) simp

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

lemma bifIPCBufVPtr_bifNodeID_update [simp]:
  "bifIPCBufVPtr (bifNodeID_update f v) = bifIPCBufVPtr v" by (cases v) simp

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

lemma bifIPCBufVPtr_bifNumNodes_update [simp]:
  "bifIPCBufVPtr (bifNumNodes_update f v) = bifIPCBufVPtr v" by (cases v) simp

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

lemma bifIPCBufVPtr_bifNumIOPTLevels_update [simp]:
  "bifIPCBufVPtr (bifNumIOPTLevels_update f v) = bifIPCBufVPtr v" by (cases v) simp

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

lemma bifIPCBufVPtr_bifIPCBufVPtr_update [simp]:
  "bifIPCBufVPtr (bifIPCBufVPtr_update f v) = f (bifIPCBufVPtr v)" by (cases v) simp

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

lemma bifIPCBufVPtr_bifNullCaps_update [simp]:
  "bifIPCBufVPtr (bifNullCaps_update f v) = bifIPCBufVPtr v" by (cases v) simp

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

lemma bifIPCBufVPtr_bifSharedFrameCaps_update [simp]:
  "bifIPCBufVPtr (bifSharedFrameCaps_update f v) = bifIPCBufVPtr v" by (cases v) simp

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

lemma bifIPCBufVPtr_bifUIFrameCaps_update [simp]:
  "bifIPCBufVPtr (bifUIFrameCaps_update f v) = bifIPCBufVPtr v" by (cases v) simp

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

lemma bifIPCBufVPtr_bifUIPDCaps_update [simp]:
  "bifIPCBufVPtr (bifUIPDCaps_update f v) = bifIPCBufVPtr v" by (cases v) simp

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

lemma bifIPCBufVPtr_bifUIPTCaps_update [simp]:
  "bifIPCBufVPtr (bifUIPTCaps_update f v) = bifIPCBufVPtr v" by (cases v) simp

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

lemma bifIPCBufVPtr_bifUntypedObjCaps_update [simp]:
  "bifIPCBufVPtr (bifUntypedObjCaps_update f v) = bifIPCBufVPtr v" by (cases v) simp

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

lemma bifIPCBufVPtr_bifUntypedObjPAddrs_update [simp]:
  "bifIPCBufVPtr (bifUntypedObjPAddrs_update f v) = bifIPCBufVPtr v" by (cases v) simp

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

lemma bifIPCBufVPtr_bifUntypedObjSizeBits_update [simp]:
  "bifIPCBufVPtr (bifUntypedObjSizeBits_update f v) = bifIPCBufVPtr v" by (cases v) simp

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

lemma bifIPCBufVPtr_bifUntypedObjIsDeviceList_update [simp]:
  "bifIPCBufVPtr (bifUntypedObjIsDeviceList_update f v) = bifIPCBufVPtr v" by (cases v) simp

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

lemma bifIPCBufVPtr_bifITCNodeSizeBits_update [simp]:
  "bifIPCBufVPtr (bifITCNodeSizeBits_update f v) = bifIPCBufVPtr v" by (cases v) simp

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

lemma bifIPCBufVPtr_bifNumDeviceRegions_update [simp]:
  "bifIPCBufVPtr (bifNumDeviceRegions_update f v) = bifIPCBufVPtr v" by (cases v) simp

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

lemma bifIPCBufVPtr_bifDeviceRegions_update [simp]:
  "bifIPCBufVPtr (bifDeviceRegions_update f v) = bifIPCBufVPtr v" by (cases v) simp

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

lemma bifNullCaps_bifNodeID_update [simp]:
  "bifNullCaps (bifNodeID_update f v) = bifNullCaps v" by (cases v) simp

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

lemma bifNullCaps_bifNumNodes_update [simp]:
  "bifNullCaps (bifNumNodes_update f v) = bifNullCaps v" by (cases v) simp

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

lemma bifNullCaps_bifNumIOPTLevels_update [simp]:
  "bifNullCaps (bifNumIOPTLevels_update f v) = bifNullCaps v" by (cases v) simp

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

lemma bifNullCaps_bifIPCBufVPtr_update [simp]:
  "bifNullCaps (bifIPCBufVPtr_update f v) = bifNullCaps v" by (cases v) simp

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

lemma bifNullCaps_bifNullCaps_update [simp]:
  "bifNullCaps (bifNullCaps_update f v) = f (bifNullCaps v)" by (cases v) simp

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

lemma bifNullCaps_bifSharedFrameCaps_update [simp]:
  "bifNullCaps (bifSharedFrameCaps_update f v) = bifNullCaps v" by (cases v) simp

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

lemma bifNullCaps_bifUIFrameCaps_update [simp]:
  "bifNullCaps (bifUIFrameCaps_update f v) = bifNullCaps v" by (cases v) simp

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

lemma bifNullCaps_bifUIPDCaps_update [simp]:
  "bifNullCaps (bifUIPDCaps_update f v) = bifNullCaps v" by (cases v) simp

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

lemma bifNullCaps_bifUIPTCaps_update [simp]:
  "bifNullCaps (bifUIPTCaps_update f v) = bifNullCaps v" by (cases v) simp

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

lemma bifNullCaps_bifUntypedObjCaps_update [simp]:
  "bifNullCaps (bifUntypedObjCaps_update f v) = bifNullCaps v" by (cases v) simp

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

lemma bifNullCaps_bifUntypedObjPAddrs_update [simp]:
  "bifNullCaps (bifUntypedObjPAddrs_update f v) = bifNullCaps v" by (cases v) simp

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

lemma bifNullCaps_bifUntypedObjSizeBits_update [simp]:
  "bifNullCaps (bifUntypedObjSizeBits_update f v) = bifNullCaps v" by (cases v) simp

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

lemma bifNullCaps_bifUntypedObjIsDeviceList_update [simp]:
  "bifNullCaps (bifUntypedObjIsDeviceList_update f v) = bifNullCaps v" by (cases v) simp

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

lemma bifNullCaps_bifNumDeviceRegions_update [simp]:
  "bifNullCaps (bifNumDeviceRegions_update f v) = bifNullCaps v" by (cases v) simp

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

lemma bifNullCaps_bifDeviceRegions_update [simp]:
  "bifNullCaps (bifDeviceRegions_update f v) = bifNullCaps v" by (cases v) simp

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

lemma bifSharedFrameCaps_bifNodeID_update [simp]:
  "bifSharedFrameCaps (bifNodeID_update f v) = bifSharedFrameCaps v" by (cases v) simp

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

lemma bifSharedFrameCaps_bifNumNodes_update [simp]:
  "bifSharedFrameCaps (bifNumNodes_update f v) = bifSharedFrameCaps v" by (cases v) simp

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

lemma bifSharedFrameCaps_bifNumIOPTLevels_update [simp]:
  "bifSharedFrameCaps (bifNumIOPTLevels_update f v) = bifSharedFrameCaps v" by (cases v) simp

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

lemma bifSharedFrameCaps_bifIPCBufVPtr_update [simp]:
  "bifSharedFrameCaps (bifIPCBufVPtr_update f v) = bifSharedFrameCaps v" by (cases v) simp

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

lemma bifSharedFrameCaps_bifNullCaps_update [simp]:
  "bifSharedFrameCaps (bifNullCaps_update f v) = bifSharedFrameCaps v" by (cases v) simp

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

lemma bifSharedFrameCaps_bifSharedFrameCaps_update [simp]:
  "bifSharedFrameCaps (bifSharedFrameCaps_update f v) = f (bifSharedFrameCaps v)" by (cases v) simp

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

lemma bifSharedFrameCaps_bifUIFrameCaps_update [simp]:
  "bifSharedFrameCaps (bifUIFrameCaps_update f v) = bifSharedFrameCaps v" by (cases v) simp

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

lemma bifSharedFrameCaps_bifUIPDCaps_update [simp]:
  "bifSharedFrameCaps (bifUIPDCaps_update f v) = bifSharedFrameCaps v" by (cases v) simp

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

lemma bifSharedFrameCaps_bifUIPTCaps_update [simp]:
  "bifSharedFrameCaps (bifUIPTCaps_update f v) = bifSharedFrameCaps v" by (cases v) simp

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

lemma bifSharedFrameCaps_bifUntypedObjPAddrs_update [simp]:
  "bifSharedFrameCaps (bifUntypedObjPAddrs_update f v) = bifSharedFrameCaps v" by (cases v) simp

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

lemma bifSharedFrameCaps_bifUntypedObjSizeBits_update [simp]:
  "bifSharedFrameCaps (bifUntypedObjSizeBits_update f v) = bifSharedFrameCaps v" by (cases v) simp

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

lemma bifSharedFrameCaps_bifUntypedObjIsDeviceList_update [simp]:
  "bifSharedFrameCaps (bifUntypedObjIsDeviceList_update f v) = bifSharedFrameCaps v" by (cases v) simp

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

lemma bifSharedFrameCaps_bifNumDeviceRegions_update [simp]:
  "bifSharedFrameCaps (bifNumDeviceRegions_update f v) = bifSharedFrameCaps v" by (cases v) simp

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

lemma bifSharedFrameCaps_bifDeviceRegions_update [simp]:
  "bifSharedFrameCaps (bifDeviceRegions_update f v) = bifSharedFrameCaps v" by (cases v) simp

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

lemma bifUIFrameCaps_bifNodeID_update [simp]:
  "bifUIFrameCaps (bifNodeID_update f v) = bifUIFrameCaps v" by (cases v) simp

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

lemma bifUIFrameCaps_bifNumNodes_update [simp]:
  "bifUIFrameCaps (bifNumNodes_update f v) = bifUIFrameCaps v" by (cases v) simp

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

lemma bifUIFrameCaps_bifNumIOPTLevels_update [simp]:
  "bifUIFrameCaps (bifNumIOPTLevels_update f v) = bifUIFrameCaps v" by (cases v) simp

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

lemma bifUIFrameCaps_bifNullCaps_update [simp]:
  "bifUIFrameCaps (bifNullCaps_update f v) = bifUIFrameCaps v" by (cases v) simp

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

lemma bifUIFrameCaps_bifSharedFrameCaps_update [simp]:
  "bifUIFrameCaps (bifSharedFrameCaps_update f v) = bifUIFrameCaps v" by (cases v) simp

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

lemma bifUIFrameCaps_bifUIFrameCaps_update [simp]:
  "bifUIFrameCaps (bifUIFrameCaps_update f v) = f (bifUIFrameCaps v)" by (cases v) simp

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

lemma bifUIFrameCaps_bifUIPDCaps_update [simp]:
  "bifUIFrameCaps (bifUIPDCaps_update f v) = bifUIFrameCaps v" by (cases v) simp

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

lemma bifUIFrameCaps_bifUIPTCaps_update [simp]:
  "bifUIFrameCaps (bifUIPTCaps_update f v) = bifUIFrameCaps v" by (cases v) simp

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

lemma bifUIFrameCaps_bifUntypedObjCaps_update [simp]:
  "bifUIFrameCaps (bifUntypedObjCaps_update f v) = bifUIFrameCaps v" by (cases v) simp

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

lemma bifUIFrameCaps_bifUntypedObjPAddrs_update [simp]:
  "bifUIFrameCaps (bifUntypedObjPAddrs_update f v) = bifUIFrameCaps v" by (cases v) simp

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

lemma bifUIFrameCaps_bifUntypedObjSizeBits_update [simp]:
  "bifUIFrameCaps (bifUntypedObjSizeBits_update f v) = bifUIFrameCaps v" by (cases v) simp

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

lemma bifUIFrameCaps_bifUntypedObjIsDeviceList_update [simp]:
  "bifUIFrameCaps (bifUntypedObjIsDeviceList_update f v) = bifUIFrameCaps v" by (cases v) simp

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

lemma bifUIFrameCaps_bifITCNodeSizeBits_update [simp]:
  "bifUIFrameCaps (bifITCNodeSizeBits_update f v) = bifUIFrameCaps v" by (cases v) simp

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

lemma bifUIFrameCaps_bifNumDeviceRegions_update [simp]:
  "bifUIFrameCaps (bifNumDeviceRegions_update f v) = bifUIFrameCaps v" by (cases v) simp

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

lemma bifUIFrameCaps_bifDeviceRegions_update [simp]:
  "bifUIFrameCaps (bifDeviceRegions_update f v) = bifUIFrameCaps v" by (cases v) simp

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

lemma bifUIPDCaps_bifNodeID_update [simp]:
  "bifUIPDCaps (bifNodeID_update f v) = bifUIPDCaps v" by (cases v) simp

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

lemma bifUIPDCaps_bifNumIOPTLevels_update [simp]:
  "bifUIPDCaps (bifNumIOPTLevels_update f v) = bifUIPDCaps v" by (cases v) simp

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

lemma bifUIPDCaps_bifIPCBufVPtr_update [simp]:
  "bifUIPDCaps (bifIPCBufVPtr_update f v) = bifUIPDCaps v" by (cases v) simp

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

lemma bifUIPDCaps_bifSharedFrameCaps_update [simp]:
  "bifUIPDCaps (bifSharedFrameCaps_update f v) = bifUIPDCaps v" by (cases v) simp

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

lemma bifUIPDCaps_bifUIFrameCaps_update [simp]:
  "bifUIPDCaps (bifUIFrameCaps_update f v) = bifUIPDCaps v" by (cases v) simp

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

lemma bifUIPDCaps_bifUIPDCaps_update [simp]:
  "bifUIPDCaps (bifUIPDCaps_update f v) = f (bifUIPDCaps v)" by (cases v) simp

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

lemma bifUIPDCaps_bifUIPTCaps_update [simp]:
  "bifUIPDCaps (bifUIPTCaps_update f v) = bifUIPDCaps v" by (cases v) simp

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

lemma bifUIPDCaps_bifUntypedObjCaps_update [simp]:
  "bifUIPDCaps (bifUntypedObjCaps_update f v) = bifUIPDCaps v" by (cases v) simp

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