kings-crown/FVELER_Isabelle huggingface dataset:
theory Types_H

lemma bifUIPDCaps_bifUntypedObjPAddrs_update [simp]:
  "bifUIPDCaps (bifUntypedObjPAddrs_update f v) = bifUIPDCaps v" by (cases v) simp

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

lemma bifUIPDCaps_bifUntypedObjSizeBits_update [simp]:
  "bifUIPDCaps (bifUntypedObjSizeBits_update f v) = bifUIPDCaps v" by (cases v) simp

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

lemma bifUIPDCaps_bifUntypedObjIsDeviceList_update [simp]:
  "bifUIPDCaps (bifUntypedObjIsDeviceList_update f v) = bifUIPDCaps v" by (cases v) simp

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

lemma bifUIPDCaps_bifITCNodeSizeBits_update [simp]:
  "bifUIPDCaps (bifITCNodeSizeBits_update f v) = bifUIPDCaps v" by (cases v) simp

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

lemma bifUIPDCaps_bifNumDeviceRegions_update [simp]:
  "bifUIPDCaps (bifNumDeviceRegions_update f v) = bifUIPDCaps v" by (cases v) simp

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

lemma bifUIPDCaps_bifDeviceRegions_update [simp]:
  "bifUIPDCaps (bifDeviceRegions_update f v) = bifUIPDCaps v" by (cases v) simp

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

lemma bifUIPTCaps_bifNodeID_update [simp]:
  "bifUIPTCaps (bifNodeID_update f v) = bifUIPTCaps v" by (cases v) simp

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

lemma bifUIPTCaps_bifNumNodes_update [simp]:
  "bifUIPTCaps (bifNumNodes_update f v) = bifUIPTCaps v" by (cases v) simp

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

lemma bifUIPTCaps_bifNumIOPTLevels_update [simp]:
  "bifUIPTCaps (bifNumIOPTLevels_update f v) = bifUIPTCaps v" by (cases v) simp

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

lemma bifUIPTCaps_bifIPCBufVPtr_update [simp]:
  "bifUIPTCaps (bifIPCBufVPtr_update f v) = bifUIPTCaps v" by (cases v) simp

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

lemma bifUIPTCaps_bifNullCaps_update [simp]:
  "bifUIPTCaps (bifNullCaps_update f v) = bifUIPTCaps v" by (cases v) simp

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

lemma bifUIPTCaps_bifSharedFrameCaps_update [simp]:
  "bifUIPTCaps (bifSharedFrameCaps_update f v) = bifUIPTCaps v" by (cases v) simp

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

lemma bifUIPTCaps_bifUIFrameCaps_update [simp]:
  "bifUIPTCaps (bifUIFrameCaps_update f v) = bifUIPTCaps v" by (cases v) simp

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

lemma bifUIPTCaps_bifUIPDCaps_update [simp]:
  "bifUIPTCaps (bifUIPDCaps_update f v) = bifUIPTCaps v" by (cases v) simp

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

lemma bifUIPTCaps_bifUIPTCaps_update [simp]:
  "bifUIPTCaps (bifUIPTCaps_update f v) = f (bifUIPTCaps v)" by (cases v) simp

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

lemma bifUIPTCaps_bifUntypedObjCaps_update [simp]:
  "bifUIPTCaps (bifUntypedObjCaps_update f v) = bifUIPTCaps v" by (cases v) simp

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

lemma bifUIPTCaps_bifUntypedObjPAddrs_update [simp]:
  "bifUIPTCaps (bifUntypedObjPAddrs_update f v) = bifUIPTCaps v" by (cases v) simp

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

lemma bifUIPTCaps_bifUntypedObjSizeBits_update [simp]:
  "bifUIPTCaps (bifUntypedObjSizeBits_update f v) = bifUIPTCaps v" by (cases v) simp

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

lemma bifUIPTCaps_bifUntypedObjIsDeviceList_update [simp]:
  "bifUIPTCaps (bifUntypedObjIsDeviceList_update f v) = bifUIPTCaps v" by (cases v) simp

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

lemma bifUIPTCaps_bifITCNodeSizeBits_update [simp]:
  "bifUIPTCaps (bifITCNodeSizeBits_update f v) = bifUIPTCaps v" by (cases v) simp

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

lemma bifUIPTCaps_bifNumDeviceRegions_update [simp]:
  "bifUIPTCaps (bifNumDeviceRegions_update f v) = bifUIPTCaps v" by (cases v) simp

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

lemma bifUIPTCaps_bifDeviceRegions_update [simp]:
  "bifUIPTCaps (bifDeviceRegions_update f v) = bifUIPTCaps v" by (cases v) simp

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

lemma bifUntypedObjCaps_bifNodeID_update [simp]:
  "bifUntypedObjCaps (bifNodeID_update f v) = bifUntypedObjCaps v" by (cases v) simp

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

lemma bifUntypedObjCaps_bifNumNodes_update [simp]:
  "bifUntypedObjCaps (bifNumNodes_update f v) = bifUntypedObjCaps v" by (cases v) simp

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

lemma bifUntypedObjCaps_bifIPCBufVPtr_update [simp]:
  "bifUntypedObjCaps (bifIPCBufVPtr_update f v) = bifUntypedObjCaps v" by (cases v) simp

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

lemma bifUntypedObjCaps_bifNullCaps_update [simp]:
  "bifUntypedObjCaps (bifNullCaps_update f v) = bifUntypedObjCaps v" by (cases v) simp

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

lemma bifUntypedObjCaps_bifSharedFrameCaps_update [simp]:
  "bifUntypedObjCaps (bifSharedFrameCaps_update f v) = bifUntypedObjCaps v" by (cases v) simp

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

lemma bifUntypedObjCaps_bifUIFrameCaps_update [simp]:
  "bifUntypedObjCaps (bifUIFrameCaps_update f v) = bifUntypedObjCaps v" by (cases v) simp

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

lemma bifUntypedObjCaps_bifUIPDCaps_update [simp]:
  "bifUntypedObjCaps (bifUIPDCaps_update f v) = bifUntypedObjCaps v" by (cases v) simp

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

lemma bifUntypedObjCaps_bifUIPTCaps_update [simp]:
  "bifUntypedObjCaps (bifUIPTCaps_update f v) = bifUntypedObjCaps v" by (cases v) simp

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

lemma bifUntypedObjCaps_bifUntypedObjCaps_update [simp]:
  "bifUntypedObjCaps (bifUntypedObjCaps_update f v) = f (bifUntypedObjCaps v)" by (cases v) simp

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

lemma bifUntypedObjCaps_bifUntypedObjPAddrs_update [simp]:
  "bifUntypedObjCaps (bifUntypedObjPAddrs_update f v) = bifUntypedObjCaps v" by (cases v) simp

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

lemma bifUntypedObjCaps_bifUntypedObjSizeBits_update [simp]:
  "bifUntypedObjCaps (bifUntypedObjSizeBits_update f v) = bifUntypedObjCaps v" by (cases v) simp

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

lemma bifUntypedObjCaps_bifUntypedObjIsDeviceList_update [simp]:
  "bifUntypedObjCaps (bifUntypedObjIsDeviceList_update f v) = bifUntypedObjCaps v" by (cases v) simp

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

lemma bifUntypedObjCaps_bifITCNodeSizeBits_update [simp]:
  "bifUntypedObjCaps (bifITCNodeSizeBits_update f v) = bifUntypedObjCaps v" by (cases v) simp

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

lemma bifUntypedObjCaps_bifDeviceRegions_update [simp]:
  "bifUntypedObjCaps (bifDeviceRegions_update f v) = bifUntypedObjCaps v" by (cases v) simp

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

lemma bifUntypedObjPAddrs_bifNodeID_update [simp]:
  "bifUntypedObjPAddrs (bifNodeID_update f v) = bifUntypedObjPAddrs v" by (cases v) simp

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

lemma bifUntypedObjPAddrs_bifNumNodes_update [simp]:
  "bifUntypedObjPAddrs (bifNumNodes_update f v) = bifUntypedObjPAddrs v" by (cases v) simp

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

lemma bifUntypedObjPAddrs_bifNumIOPTLevels_update [simp]:
  "bifUntypedObjPAddrs (bifNumIOPTLevels_update f v) = bifUntypedObjPAddrs v" by (cases v) simp

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

lemma bifUntypedObjPAddrs_bifIPCBufVPtr_update [simp]:
  "bifUntypedObjPAddrs (bifIPCBufVPtr_update f v) = bifUntypedObjPAddrs v" by (cases v) simp

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

lemma bifUntypedObjPAddrs_bifNullCaps_update [simp]:
  "bifUntypedObjPAddrs (bifNullCaps_update f v) = bifUntypedObjPAddrs v" by (cases v) simp

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

lemma bifUntypedObjPAddrs_bifSharedFrameCaps_update [simp]:
  "bifUntypedObjPAddrs (bifSharedFrameCaps_update f v) = bifUntypedObjPAddrs v" by (cases v) simp

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

lemma bifUntypedObjPAddrs_bifUIPDCaps_update [simp]:
  "bifUntypedObjPAddrs (bifUIPDCaps_update f v) = bifUntypedObjPAddrs v" by (cases v) simp

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

lemma bifUntypedObjPAddrs_bifUIPTCaps_update [simp]:
  "bifUntypedObjPAddrs (bifUIPTCaps_update f v) = bifUntypedObjPAddrs v" by (cases v) simp

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

lemma bifUntypedObjPAddrs_bifUntypedObjPAddrs_update [simp]:
  "bifUntypedObjPAddrs (bifUntypedObjPAddrs_update f v) = f (bifUntypedObjPAddrs v)" by (cases v) simp

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

lemma bifUntypedObjPAddrs_bifUntypedObjIsDeviceList_update [simp]:
  "bifUntypedObjPAddrs (bifUntypedObjIsDeviceList_update f v) = bifUntypedObjPAddrs v" by (cases v) simp

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

lemma bifUntypedObjPAddrs_bifITCNodeSizeBits_update [simp]:
  "bifUntypedObjPAddrs (bifITCNodeSizeBits_update f v) = bifUntypedObjPAddrs v" by (cases v) simp

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

lemma bifUntypedObjPAddrs_bifNumDeviceRegions_update [simp]:
  "bifUntypedObjPAddrs (bifNumDeviceRegions_update f v) = bifUntypedObjPAddrs v" by (cases v) simp

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

lemma bifUntypedObjPAddrs_bifDeviceRegions_update [simp]:
  "bifUntypedObjPAddrs (bifDeviceRegions_update f v) = bifUntypedObjPAddrs v" by (cases v) simp

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

lemma bifUntypedObjSizeBits_bifNodeID_update [simp]:
  "bifUntypedObjSizeBits (bifNodeID_update f v) = bifUntypedObjSizeBits v" by (cases v) simp

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

lemma bifUntypedObjSizeBits_bifNumIOPTLevels_update [simp]:
  "bifUntypedObjSizeBits (bifNumIOPTLevels_update f v) = bifUntypedObjSizeBits v" by (cases v) simp

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

lemma bifUntypedObjSizeBits_bifIPCBufVPtr_update [simp]:
  "bifUntypedObjSizeBits (bifIPCBufVPtr_update f v) = bifUntypedObjSizeBits v" by (cases v) simp

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

lemma bifUntypedObjSizeBits_bifNullCaps_update [simp]:
  "bifUntypedObjSizeBits (bifNullCaps_update f v) = bifUntypedObjSizeBits v" by (cases v) simp

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

lemma bifUntypedObjSizeBits_bifSharedFrameCaps_update [simp]:
  "bifUntypedObjSizeBits (bifSharedFrameCaps_update f v) = bifUntypedObjSizeBits v" by (cases v) simp

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

lemma bifUntypedObjSizeBits_bifUIFrameCaps_update [simp]:
  "bifUntypedObjSizeBits (bifUIFrameCaps_update f v) = bifUntypedObjSizeBits v" by (cases v) simp

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

lemma bifUntypedObjSizeBits_bifUIPDCaps_update [simp]:
  "bifUntypedObjSizeBits (bifUIPDCaps_update f v) = bifUntypedObjSizeBits v" by (cases v) simp

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

lemma bifUntypedObjSizeBits_bifUIPTCaps_update [simp]:
  "bifUntypedObjSizeBits (bifUIPTCaps_update f v) = bifUntypedObjSizeBits v" by (cases v) simp

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

lemma bifUntypedObjSizeBits_bifUntypedObjCaps_update [simp]:
  "bifUntypedObjSizeBits (bifUntypedObjCaps_update f v) = bifUntypedObjSizeBits v" by (cases v) simp

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

lemma bifUntypedObjSizeBits_bifUntypedObjPAddrs_update [simp]:
  "bifUntypedObjSizeBits (bifUntypedObjPAddrs_update f v) = bifUntypedObjSizeBits v" by (cases v) simp

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

lemma bifUntypedObjSizeBits_bifUntypedObjSizeBits_update [simp]:
  "bifUntypedObjSizeBits (bifUntypedObjSizeBits_update f v) = f (bifUntypedObjSizeBits v)" by (cases v) simp

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

lemma bifUntypedObjSizeBits_bifUntypedObjIsDeviceList_update [simp]:
  "bifUntypedObjSizeBits (bifUntypedObjIsDeviceList_update f v) = bifUntypedObjSizeBits v" by (cases v) simp

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

lemma bifUntypedObjSizeBits_bifITCNodeSizeBits_update [simp]:
  "bifUntypedObjSizeBits (bifITCNodeSizeBits_update f v) = bifUntypedObjSizeBits v" by (cases v) simp

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

lemma bifUntypedObjSizeBits_bifNumDeviceRegions_update [simp]:
  "bifUntypedObjSizeBits (bifNumDeviceRegions_update f v) = bifUntypedObjSizeBits v" by (cases v) simp

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

lemma bifUntypedObjSizeBits_bifDeviceRegions_update [simp]:
  "bifUntypedObjSizeBits (bifDeviceRegions_update f v) = bifUntypedObjSizeBits v" by (cases v) simp

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

lemma bifUntypedObjIsDeviceList_bifNodeID_update [simp]:
  "bifUntypedObjIsDeviceList (bifNodeID_update f v) = bifUntypedObjIsDeviceList v" by (cases v) simp

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

lemma bifUntypedObjIsDeviceList_bifNumNodes_update [simp]:
  "bifUntypedObjIsDeviceList (bifNumNodes_update f v) = bifUntypedObjIsDeviceList v" by (cases v) simp

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

lemma bifUntypedObjIsDeviceList_bifNumIOPTLevels_update [simp]:
  "bifUntypedObjIsDeviceList (bifNumIOPTLevels_update f v) = bifUntypedObjIsDeviceList v" by (cases v) simp

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

lemma bifUntypedObjIsDeviceList_bifIPCBufVPtr_update [simp]:
  "bifUntypedObjIsDeviceList (bifIPCBufVPtr_update f v) = bifUntypedObjIsDeviceList v" by (cases v) simp

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

lemma bifUntypedObjIsDeviceList_bifNullCaps_update [simp]:
  "bifUntypedObjIsDeviceList (bifNullCaps_update f v) = bifUntypedObjIsDeviceList v" by (cases v) simp

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

lemma bifUntypedObjIsDeviceList_bifSharedFrameCaps_update [simp]:
  "bifUntypedObjIsDeviceList (bifSharedFrameCaps_update f v) = bifUntypedObjIsDeviceList v" by (cases v) simp

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

lemma bifUntypedObjIsDeviceList_bifUIFrameCaps_update [simp]:
  "bifUntypedObjIsDeviceList (bifUIFrameCaps_update f v) = bifUntypedObjIsDeviceList v" by (cases v) simp

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

lemma bifUntypedObjIsDeviceList_bifUIPDCaps_update [simp]:
  "bifUntypedObjIsDeviceList (bifUIPDCaps_update f v) = bifUntypedObjIsDeviceList v" by (cases v) simp

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

lemma bifUntypedObjIsDeviceList_bifUntypedObjCaps_update [simp]:
  "bifUntypedObjIsDeviceList (bifUntypedObjCaps_update f v) = bifUntypedObjIsDeviceList v" by (cases v) simp

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

lemma bifUntypedObjIsDeviceList_bifUntypedObjPAddrs_update [simp]:
  "bifUntypedObjIsDeviceList (bifUntypedObjPAddrs_update f v) = bifUntypedObjIsDeviceList v" by (cases v) simp

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

lemma bifUntypedObjIsDeviceList_bifUntypedObjSizeBits_update [simp]:
  "bifUntypedObjIsDeviceList (bifUntypedObjSizeBits_update f v) = bifUntypedObjIsDeviceList v" by (cases v) simp

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

lemma bifUntypedObjIsDeviceList_bifUntypedObjIsDeviceList_update [simp]:
  "bifUntypedObjIsDeviceList (bifUntypedObjIsDeviceList_update f v) = f (bifUntypedObjIsDeviceList v)" by (cases v) simp

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

lemma bifUntypedObjIsDeviceList_bifITCNodeSizeBits_update [simp]:
  "bifUntypedObjIsDeviceList (bifITCNodeSizeBits_update f v) = bifUntypedObjIsDeviceList v" by (cases v) simp

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

lemma bifUntypedObjIsDeviceList_bifNumDeviceRegions_update [simp]:
  "bifUntypedObjIsDeviceList (bifNumDeviceRegions_update f v) = bifUntypedObjIsDeviceList v" by (cases v) simp

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

lemma bifUntypedObjIsDeviceList_bifDeviceRegions_update [simp]:
  "bifUntypedObjIsDeviceList (bifDeviceRegions_update f v) = bifUntypedObjIsDeviceList v" by (cases v) simp

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

lemma bifITCNodeSizeBits_bifNodeID_update [simp]:
  "bifITCNodeSizeBits (bifNodeID_update f v) = bifITCNodeSizeBits v" by (cases v) simp

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

lemma bifITCNodeSizeBits_bifNumNodes_update [simp]:
  "bifITCNodeSizeBits (bifNumNodes_update f v) = bifITCNodeSizeBits v" by (cases v) simp

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