kings-crown/FVELER_Isabelle huggingface dataset:
theory Structures_H

lemma ntfnObj_ntfnBoundTCB_update [simp]:
  "ntfnObj (ntfnBoundTCB_update f v) = ntfnObj v" by (cases v) simp

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

lemma ntfnBoundTCB_ntfnObj_update [simp]:
  "ntfnBoundTCB (ntfnObj_update f v) = ntfnBoundTCB v" by (cases v) simp

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

lemma ntfnBoundTCB_ntfnBoundTCB_update [simp]:
  "ntfnBoundTCB (ntfnBoundTCB_update f v) = f (ntfnBoundTCB v)" by (cases v) simp

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

lemma mdbNext_mdbNext_update [simp]:
  "mdbNext (mdbNext_update f v) = f (mdbNext v)" by (cases v) simp

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

lemma mdbNext_mdbPrev_update [simp]:
  "mdbNext (mdbPrev_update f v) = mdbNext v" by (cases v) simp

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

lemma mdbNext_mdbRevocable_update [simp]:
  "mdbNext (mdbRevocable_update f v) = mdbNext v" by (cases v) simp

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

lemma mdbNext_mdbFirstBadged_update [simp]:
  "mdbNext (mdbFirstBadged_update f v) = mdbNext v" by (cases v) simp

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

lemma mdbPrev_mdbNext_update [simp]:
  "mdbPrev (mdbNext_update f v) = mdbPrev v" by (cases v) simp

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

lemma mdbPrev_mdbPrev_update [simp]:
  "mdbPrev (mdbPrev_update f v) = f (mdbPrev v)" by (cases v) simp

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

lemma mdbPrev_mdbRevocable_update [simp]:
  "mdbPrev (mdbRevocable_update f v) = mdbPrev v" by (cases v) simp

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

lemma mdbPrev_mdbFirstBadged_update [simp]:
  "mdbPrev (mdbFirstBadged_update f v) = mdbPrev v" by (cases v) simp

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

lemma mdbRevocable_mdbNext_update [simp]:
  "mdbRevocable (mdbNext_update f v) = mdbRevocable v" by (cases v) simp

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

lemma mdbRevocable_mdbPrev_update [simp]:
  "mdbRevocable (mdbPrev_update f v) = mdbRevocable v" by (cases v) simp

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

lemma mdbRevocable_mdbRevocable_update [simp]:
  "mdbRevocable (mdbRevocable_update f v) = f (mdbRevocable v)" by (cases v) simp

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

lemma mdbRevocable_mdbFirstBadged_update [simp]:
  "mdbRevocable (mdbFirstBadged_update f v) = mdbRevocable v" by (cases v) simp

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

lemma mdbFirstBadged_mdbNext_update [simp]:
  "mdbFirstBadged (mdbNext_update f v) = mdbFirstBadged v" by (cases v) simp

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

lemma mdbFirstBadged_mdbPrev_update [simp]:
  "mdbFirstBadged (mdbPrev_update f v) = mdbFirstBadged v" by (cases v) simp

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

lemma mdbFirstBadged_mdbRevocable_update [simp]:
  "mdbFirstBadged (mdbRevocable_update f v) = mdbFirstBadged v" by (cases v) simp

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

lemma cteCap_cteMDBNode_update [simp]:
  "cteCap (cteMDBNode_update f v) = cteCap v" by (cases v) simp

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

lemma cteMDBNode_cteCap_update [simp]:
  "cteMDBNode (cteCap_update f v) = cteMDBNode v" by (cases v) simp

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

lemma cteMDBNode_cteMDBNode_update [simp]:
  "cteMDBNode (cteMDBNode_update f v) = f (cteMDBNode v)" by (cases v) simp

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

lemma tcbCTable_tcbCTable_update [simp]:
  "tcbCTable (tcbCTable_update f v) = f (tcbCTable v)" by (cases v) simp

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

lemma tcbCTable_tcbVTable_update [simp]:
  "tcbCTable (tcbVTable_update f v) = tcbCTable v" by (cases v) simp

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

lemma tcbCTable_tcbReply_update [simp]:
  "tcbCTable (tcbReply_update f v) = tcbCTable v" by (cases v) simp

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

lemma tcbCTable_tcbCaller_update [simp]:
  "tcbCTable (tcbCaller_update f v) = tcbCTable v" by (cases v) simp

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

lemma tcbCTable_tcbIPCBufferFrame_update [simp]:
  "tcbCTable (tcbIPCBufferFrame_update f v) = tcbCTable v" by (cases v) simp

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

lemma tcbCTable_tcbDomain_update [simp]:
  "tcbCTable (tcbDomain_update f v) = tcbCTable v" by (cases v) simp

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

lemma tcbCTable_tcbState_update [simp]:
  "tcbCTable (tcbState_update f v) = tcbCTable v" by (cases v) simp

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

lemma tcbCTable_tcbMCP_update [simp]:
  "tcbCTable (tcbMCP_update f v) = tcbCTable v" by (cases v) simp

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

lemma tcbCTable_tcbPriority_update [simp]:
  "tcbCTable (tcbPriority_update f v) = tcbCTable v" by (cases v) simp

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

lemma tcbCTable_tcbQueued_update [simp]:
  "tcbCTable (tcbQueued_update f v) = tcbCTable v" by (cases v) simp

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

lemma tcbCTable_tcbFault_update [simp]:
  "tcbCTable (tcbFault_update f v) = tcbCTable v" by (cases v) simp

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

lemma tcbCTable_tcbTimeSlice_update [simp]:
  "tcbCTable (tcbTimeSlice_update f v) = tcbCTable v" by (cases v) simp

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

lemma tcbCTable_tcbFaultHandler_update [simp]:
  "tcbCTable (tcbFaultHandler_update f v) = tcbCTable v" by (cases v) simp

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

lemma tcbCTable_tcbIPCBuffer_update [simp]:
  "tcbCTable (tcbIPCBuffer_update f v) = tcbCTable v" by (cases v) simp

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

lemma tcbCTable_tcbBoundNotification_update [simp]:
  "tcbCTable (tcbBoundNotification_update f v) = tcbCTable v" by (cases v) simp

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

lemma tcbCTable_tcbArch_update [simp]:
  "tcbCTable (tcbArch_update f v) = tcbCTable v" by (cases v) simp

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

lemma tcbVTable_tcbCTable_update [simp]:
  "tcbVTable (tcbCTable_update f v) = tcbVTable v" by (cases v) simp

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

lemma tcbVTable_tcbVTable_update [simp]:
  "tcbVTable (tcbVTable_update f v) = f (tcbVTable v)" by (cases v) simp

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

lemma tcbVTable_tcbReply_update [simp]:
  "tcbVTable (tcbReply_update f v) = tcbVTable v" by (cases v) simp

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

lemma tcbVTable_tcbCaller_update [simp]:
  "tcbVTable (tcbCaller_update f v) = tcbVTable v" by (cases v) simp

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

lemma tcbVTable_tcbIPCBufferFrame_update [simp]:
  "tcbVTable (tcbIPCBufferFrame_update f v) = tcbVTable v" by (cases v) simp

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

lemma tcbVTable_tcbState_update [simp]:
  "tcbVTable (tcbState_update f v) = tcbVTable v" by (cases v) simp

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

lemma tcbVTable_tcbMCP_update [simp]:
  "tcbVTable (tcbMCP_update f v) = tcbVTable v" by (cases v) simp

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

lemma tcbVTable_tcbPriority_update [simp]:
  "tcbVTable (tcbPriority_update f v) = tcbVTable v" by (cases v) simp

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

lemma tcbVTable_tcbQueued_update [simp]:
  "tcbVTable (tcbQueued_update f v) = tcbVTable v" by (cases v) simp

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

lemma tcbVTable_tcbTimeSlice_update [simp]:
  "tcbVTable (tcbTimeSlice_update f v) = tcbVTable v" by (cases v) simp

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

lemma tcbVTable_tcbFaultHandler_update [simp]:
  "tcbVTable (tcbFaultHandler_update f v) = tcbVTable v" by (cases v) simp

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

lemma tcbVTable_tcbIPCBuffer_update [simp]:
  "tcbVTable (tcbIPCBuffer_update f v) = tcbVTable v" by (cases v) simp

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

lemma tcbVTable_tcbBoundNotification_update [simp]:
  "tcbVTable (tcbBoundNotification_update f v) = tcbVTable v" by (cases v) simp

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

lemma tcbVTable_tcbArch_update [simp]:
  "tcbVTable (tcbArch_update f v) = tcbVTable v" by (cases v) simp

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

lemma tcbReply_tcbCTable_update [simp]:
  "tcbReply (tcbCTable_update f v) = tcbReply v" by (cases v) simp

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

lemma tcbReply_tcbVTable_update [simp]:
  "tcbReply (tcbVTable_update f v) = tcbReply v" by (cases v) simp

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

lemma tcbReply_tcbReply_update [simp]:
  "tcbReply (tcbReply_update f v) = f (tcbReply v)" by (cases v) simp

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

lemma tcbReply_tcbCaller_update [simp]:
  "tcbReply (tcbCaller_update f v) = tcbReply v" by (cases v) simp

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

lemma tcbReply_tcbIPCBufferFrame_update [simp]:
  "tcbReply (tcbIPCBufferFrame_update f v) = tcbReply v" by (cases v) simp

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

lemma tcbReply_tcbDomain_update [simp]:
  "tcbReply (tcbDomain_update f v) = tcbReply v" by (cases v) simp

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

lemma tcbReply_tcbState_update [simp]:
  "tcbReply (tcbState_update f v) = tcbReply v" by (cases v) simp

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

lemma tcbReply_tcbMCP_update [simp]:
  "tcbReply (tcbMCP_update f v) = tcbReply v" by (cases v) simp

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

lemma tcbReply_tcbQueued_update [simp]:
  "tcbReply (tcbQueued_update f v) = tcbReply v" by (cases v) simp

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

lemma tcbReply_tcbFault_update [simp]:
  "tcbReply (tcbFault_update f v) = tcbReply v" by (cases v) simp

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

lemma tcbReply_tcbTimeSlice_update [simp]:
  "tcbReply (tcbTimeSlice_update f v) = tcbReply v" by (cases v) simp

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

lemma tcbReply_tcbIPCBuffer_update [simp]:
  "tcbReply (tcbIPCBuffer_update f v) = tcbReply v" by (cases v) simp

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

lemma tcbReply_tcbBoundNotification_update [simp]:
  "tcbReply (tcbBoundNotification_update f v) = tcbReply v" by (cases v) simp

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

lemma tcbReply_tcbArch_update [simp]:
  "tcbReply (tcbArch_update f v) = tcbReply v" by (cases v) simp

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

lemma tcbCaller_tcbCTable_update [simp]:
  "tcbCaller (tcbCTable_update f v) = tcbCaller v" by (cases v) simp

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

lemma tcbCaller_tcbVTable_update [simp]:
  "tcbCaller (tcbVTable_update f v) = tcbCaller v" by (cases v) simp

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

lemma tcbCaller_tcbReply_update [simp]:
  "tcbCaller (tcbReply_update f v) = tcbCaller v" by (cases v) simp

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

lemma tcbCaller_tcbCaller_update [simp]:
  "tcbCaller (tcbCaller_update f v) = f (tcbCaller v)" by (cases v) simp

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

lemma tcbCaller_tcbIPCBufferFrame_update [simp]:
  "tcbCaller (tcbIPCBufferFrame_update f v) = tcbCaller v" by (cases v) simp

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

lemma tcbCaller_tcbDomain_update [simp]:
  "tcbCaller (tcbDomain_update f v) = tcbCaller v" by (cases v) simp

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

lemma tcbCaller_tcbState_update [simp]:
  "tcbCaller (tcbState_update f v) = tcbCaller v" by (cases v) simp

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

lemma tcbCaller_tcbMCP_update [simp]:
  "tcbCaller (tcbMCP_update f v) = tcbCaller v" by (cases v) simp

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

lemma tcbCaller_tcbPriority_update [simp]:
  "tcbCaller (tcbPriority_update f v) = tcbCaller v" by (cases v) simp

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

lemma tcbCaller_tcbQueued_update [simp]:
  "tcbCaller (tcbQueued_update f v) = tcbCaller v" by (cases v) simp

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

lemma tcbCaller_tcbFault_update [simp]:
  "tcbCaller (tcbFault_update f v) = tcbCaller v" by (cases v) simp

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

lemma tcbCaller_tcbTimeSlice_update [simp]:
  "tcbCaller (tcbTimeSlice_update f v) = tcbCaller v" by (cases v) simp

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

lemma tcbCaller_tcbFaultHandler_update [simp]:
  "tcbCaller (tcbFaultHandler_update f v) = tcbCaller v" by (cases v) simp

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

lemma tcbCaller_tcbBoundNotification_update [simp]:
  "tcbCaller (tcbBoundNotification_update f v) = tcbCaller v" by (cases v) simp

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

lemma tcbCaller_tcbArch_update [simp]:
  "tcbCaller (tcbArch_update f v) = tcbCaller v" by (cases v) simp

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

lemma tcbIPCBufferFrame_tcbCTable_update [simp]:
  "tcbIPCBufferFrame (tcbCTable_update f v) = tcbIPCBufferFrame v" by (cases v) simp

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

lemma tcbIPCBufferFrame_tcbVTable_update [simp]:
  "tcbIPCBufferFrame (tcbVTable_update f v) = tcbIPCBufferFrame v" by (cases v) simp

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

lemma tcbIPCBufferFrame_tcbReply_update [simp]:
  "tcbIPCBufferFrame (tcbReply_update f v) = tcbIPCBufferFrame v" by (cases v) simp

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

lemma tcbIPCBufferFrame_tcbCaller_update [simp]:
  "tcbIPCBufferFrame (tcbCaller_update f v) = tcbIPCBufferFrame v" by (cases v) simp

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

lemma tcbIPCBufferFrame_tcbDomain_update [simp]:
  "tcbIPCBufferFrame (tcbDomain_update f v) = tcbIPCBufferFrame v" by (cases v) simp

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

lemma tcbIPCBufferFrame_tcbState_update [simp]:
  "tcbIPCBufferFrame (tcbState_update f v) = tcbIPCBufferFrame v" by (cases v) simp

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

lemma tcbIPCBufferFrame_tcbMCP_update [simp]:
  "tcbIPCBufferFrame (tcbMCP_update f v) = tcbIPCBufferFrame v" by (cases v) simp

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

lemma tcbIPCBufferFrame_tcbPriority_update [simp]:
  "tcbIPCBufferFrame (tcbPriority_update f v) = tcbIPCBufferFrame v" by (cases v) simp

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

lemma tcbIPCBufferFrame_tcbQueued_update [simp]:
  "tcbIPCBufferFrame (tcbQueued_update f v) = tcbIPCBufferFrame v" by (cases v) simp

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

lemma tcbIPCBufferFrame_tcbTimeSlice_update [simp]:
  "tcbIPCBufferFrame (tcbTimeSlice_update f v) = tcbIPCBufferFrame v" by (cases v) simp

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

lemma tcbIPCBufferFrame_tcbFaultHandler_update [simp]:
  "tcbIPCBufferFrame (tcbFaultHandler_update f v) = tcbIPCBufferFrame v" by (cases v) simp

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

lemma tcbIPCBufferFrame_tcbIPCBuffer_update [simp]:
  "tcbIPCBufferFrame (tcbIPCBuffer_update f v) = tcbIPCBufferFrame v" by (cases v) simp

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

lemma tcbIPCBufferFrame_tcbBoundNotification_update [simp]:
  "tcbIPCBufferFrame (tcbBoundNotification_update f v) = tcbIPCBufferFrame v" by (cases v) simp

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

lemma tcbIPCBufferFrame_tcbArch_update [simp]:
  "tcbIPCBufferFrame (tcbArch_update f v) = tcbIPCBufferFrame v" by (cases v) simp

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

lemma tcbDomain_tcbVTable_update [simp]:
  "tcbDomain (tcbVTable_update f v) = tcbDomain v" by (cases v) simp

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

lemma tcbDomain_tcbReply_update [simp]:
  "tcbDomain (tcbReply_update f v) = tcbDomain v" by (cases v) simp

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

lemma tcbDomain_tcbCaller_update [simp]:
  "tcbDomain (tcbCaller_update f v) = tcbDomain v" by (cases v) simp

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

lemma tcbDomain_tcbIPCBufferFrame_update [simp]:
  "tcbDomain (tcbIPCBufferFrame_update f v) = tcbDomain v" by (cases v) simp

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