kings-crown/FVELER_Isabelle huggingface dataset:
theory Structures_H

lemma tcbDomain_tcbDomain_update [simp]:
  "tcbDomain (tcbDomain_update f v) = f (tcbDomain v)" by (cases v) simp

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

lemma tcbDomain_tcbState_update [simp]:
  "tcbDomain (tcbState_update f v) = tcbDomain v" by (cases v) simp

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

lemma tcbDomain_tcbMCP_update [simp]:
  "tcbDomain (tcbMCP_update f v) = tcbDomain v" by (cases v) simp

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

lemma tcbDomain_tcbPriority_update [simp]:
  "tcbDomain (tcbPriority_update f v) = tcbDomain v" by (cases v) simp

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

lemma tcbDomain_tcbQueued_update [simp]:
  "tcbDomain (tcbQueued_update f v) = tcbDomain v" by (cases v) simp

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

lemma tcbDomain_tcbFault_update [simp]:
  "tcbDomain (tcbFault_update f v) = tcbDomain v" by (cases v) simp

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

lemma tcbDomain_tcbTimeSlice_update [simp]:
  "tcbDomain (tcbTimeSlice_update f v) = tcbDomain v" by (cases v) simp

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

lemma tcbDomain_tcbFaultHandler_update [simp]:
  "tcbDomain (tcbFaultHandler_update f v) = tcbDomain v" by (cases v) simp

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

lemma tcbDomain_tcbIPCBuffer_update [simp]:
  "tcbDomain (tcbIPCBuffer_update f v) = tcbDomain v" by (cases v) simp

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

lemma tcbDomain_tcbBoundNotification_update [simp]:
  "tcbDomain (tcbBoundNotification_update f v) = tcbDomain v" by (cases v) simp

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

lemma tcbDomain_tcbArch_update [simp]:
  "tcbDomain (tcbArch_update f v) = tcbDomain v" by (cases v) simp

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

lemma tcbState_tcbCTable_update [simp]:
  "tcbState (tcbCTable_update f v) = tcbState v" by (cases v) simp

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

lemma tcbState_tcbVTable_update [simp]:
  "tcbState (tcbVTable_update f v) = tcbState v" by (cases v) simp

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

lemma tcbState_tcbReply_update [simp]:
  "tcbState (tcbReply_update f v) = tcbState v" by (cases v) simp

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

lemma tcbState_tcbCaller_update [simp]:
  "tcbState (tcbCaller_update f v) = tcbState v" by (cases v) simp

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

lemma tcbState_tcbIPCBufferFrame_update [simp]:
  "tcbState (tcbIPCBufferFrame_update f v) = tcbState v" by (cases v) simp

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

lemma tcbState_tcbDomain_update [simp]:
  "tcbState (tcbDomain_update f v) = tcbState v" by (cases v) simp

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

lemma tcbState_tcbMCP_update [simp]:
  "tcbState (tcbMCP_update f v) = tcbState v" by (cases v) simp

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

lemma tcbState_tcbPriority_update [simp]:
  "tcbState (tcbPriority_update f v) = tcbState v" by (cases v) simp

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

lemma tcbState_tcbQueued_update [simp]:
  "tcbState (tcbQueued_update f v) = tcbState v" by (cases v) simp

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

lemma tcbState_tcbFault_update [simp]:
  "tcbState (tcbFault_update f v) = tcbState v" by (cases v) simp

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

lemma tcbState_tcbTimeSlice_update [simp]:
  "tcbState (tcbTimeSlice_update f v) = tcbState v" by (cases v) simp

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

lemma tcbState_tcbFaultHandler_update [simp]:
  "tcbState (tcbFaultHandler_update f v) = tcbState v" by (cases v) simp

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

lemma tcbState_tcbIPCBuffer_update [simp]:
  "tcbState (tcbIPCBuffer_update f v) = tcbState v" by (cases v) simp

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

lemma tcbState_tcbBoundNotification_update [simp]:
  "tcbState (tcbBoundNotification_update f v) = tcbState v" by (cases v) simp

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

lemma tcbState_tcbArch_update [simp]:
  "tcbState (tcbArch_update f v) = tcbState v" by (cases v) simp

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

lemma tcbMCP_tcbCTable_update [simp]:
  "tcbMCP (tcbCTable_update f v) = tcbMCP v" by (cases v) simp

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

lemma tcbMCP_tcbVTable_update [simp]:
  "tcbMCP (tcbVTable_update f v) = tcbMCP v" by (cases v) simp

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

lemma tcbMCP_tcbReply_update [simp]:
  "tcbMCP (tcbReply_update f v) = tcbMCP v" by (cases v) simp

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

lemma tcbMCP_tcbCaller_update [simp]:
  "tcbMCP (tcbCaller_update f v) = tcbMCP v" by (cases v) simp

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

lemma tcbMCP_tcbIPCBufferFrame_update [simp]:
  "tcbMCP (tcbIPCBufferFrame_update f v) = tcbMCP v" by (cases v) simp

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

lemma tcbMCP_tcbDomain_update [simp]:
  "tcbMCP (tcbDomain_update f v) = tcbMCP v" by (cases v) simp

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

lemma tcbMCP_tcbState_update [simp]:
  "tcbMCP (tcbState_update f v) = tcbMCP v" by (cases v) simp

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

lemma tcbMCP_tcbMCP_update [simp]:
  "tcbMCP (tcbMCP_update f v) = f (tcbMCP v)" by (cases v) simp

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

lemma tcbMCP_tcbPriority_update [simp]:
  "tcbMCP (tcbPriority_update f v) = tcbMCP v" by (cases v) simp

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

lemma tcbMCP_tcbQueued_update [simp]:
  "tcbMCP (tcbQueued_update f v) = tcbMCP v" by (cases v) simp

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

lemma tcbMCP_tcbFault_update [simp]:
  "tcbMCP (tcbFault_update f v) = tcbMCP v" by (cases v) simp

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

lemma tcbMCP_tcbTimeSlice_update [simp]:
  "tcbMCP (tcbTimeSlice_update f v) = tcbMCP v" by (cases v) simp

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

lemma tcbMCP_tcbFaultHandler_update [simp]:
  "tcbMCP (tcbFaultHandler_update f v) = tcbMCP v" by (cases v) simp

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

lemma tcbMCP_tcbIPCBuffer_update [simp]:
  "tcbMCP (tcbIPCBuffer_update f v) = tcbMCP v" by (cases v) simp

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

lemma tcbMCP_tcbBoundNotification_update [simp]:
  "tcbMCP (tcbBoundNotification_update f v) = tcbMCP v" by (cases v) simp

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

lemma tcbMCP_tcbArch_update [simp]:
  "tcbMCP (tcbArch_update f v) = tcbMCP v" by (cases v) simp

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

lemma tcbPriority_tcbCTable_update [simp]:
  "tcbPriority (tcbCTable_update f v) = tcbPriority v" by (cases v) simp

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

lemma tcbPriority_tcbVTable_update [simp]:
  "tcbPriority (tcbVTable_update f v) = tcbPriority v" by (cases v) simp

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

lemma tcbPriority_tcbReply_update [simp]:
  "tcbPriority (tcbReply_update f v) = tcbPriority v" by (cases v) simp

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

lemma tcbPriority_tcbCaller_update [simp]:
  "tcbPriority (tcbCaller_update f v) = tcbPriority v" by (cases v) simp

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

lemma tcbPriority_tcbIPCBufferFrame_update [simp]:
  "tcbPriority (tcbIPCBufferFrame_update f v) = tcbPriority v" by (cases v) simp

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

lemma tcbPriority_tcbDomain_update [simp]:
  "tcbPriority (tcbDomain_update f v) = tcbPriority v" by (cases v) simp

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

lemma tcbPriority_tcbState_update [simp]:
  "tcbPriority (tcbState_update f v) = tcbPriority v" by (cases v) simp

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

lemma tcbPriority_tcbMCP_update [simp]:
  "tcbPriority (tcbMCP_update f v) = tcbPriority v" by (cases v) simp

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

lemma tcbPriority_tcbPriority_update [simp]:
  "tcbPriority (tcbPriority_update f v) = f (tcbPriority v)" by (cases v) simp

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

lemma tcbPriority_tcbQueued_update [simp]:
  "tcbPriority (tcbQueued_update f v) = tcbPriority v" by (cases v) simp

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

lemma tcbPriority_tcbFault_update [simp]:
  "tcbPriority (tcbFault_update f v) = tcbPriority v" by (cases v) simp

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

lemma tcbPriority_tcbTimeSlice_update [simp]:
  "tcbPriority (tcbTimeSlice_update f v) = tcbPriority v" by (cases v) simp

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

lemma tcbPriority_tcbFaultHandler_update [simp]:
  "tcbPriority (tcbFaultHandler_update f v) = tcbPriority v" by (cases v) simp

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

lemma tcbPriority_tcbIPCBuffer_update [simp]:
  "tcbPriority (tcbIPCBuffer_update f v) = tcbPriority v" by (cases v) simp

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

lemma tcbPriority_tcbBoundNotification_update [simp]:
  "tcbPriority (tcbBoundNotification_update f v) = tcbPriority v" by (cases v) simp

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

lemma tcbPriority_tcbArch_update [simp]:
  "tcbPriority (tcbArch_update f v) = tcbPriority v" by (cases v) simp

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

lemma tcbQueued_tcbCTable_update [simp]:
  "tcbQueued (tcbCTable_update f v) = tcbQueued v" by (cases v) simp

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

lemma tcbQueued_tcbVTable_update [simp]:
  "tcbQueued (tcbVTable_update f v) = tcbQueued v" by (cases v) simp

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

lemma tcbQueued_tcbCaller_update [simp]:
  "tcbQueued (tcbCaller_update f v) = tcbQueued v" by (cases v) simp

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

lemma tcbQueued_tcbIPCBufferFrame_update [simp]:
  "tcbQueued (tcbIPCBufferFrame_update f v) = tcbQueued v" by (cases v) simp

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

lemma tcbQueued_tcbDomain_update [simp]:
  "tcbQueued (tcbDomain_update f v) = tcbQueued v" by (cases v) simp

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

lemma tcbQueued_tcbState_update [simp]:
  "tcbQueued (tcbState_update f v) = tcbQueued v" by (cases v) simp

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

lemma tcbQueued_tcbMCP_update [simp]:
  "tcbQueued (tcbMCP_update f v) = tcbQueued v" by (cases v) simp

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

lemma tcbQueued_tcbQueued_update [simp]:
  "tcbQueued (tcbQueued_update f v) = f (tcbQueued v)" by (cases v) simp

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

lemma tcbQueued_tcbFault_update [simp]:
  "tcbQueued (tcbFault_update f v) = tcbQueued v" by (cases v) simp

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

lemma tcbQueued_tcbTimeSlice_update [simp]:
  "tcbQueued (tcbTimeSlice_update f v) = tcbQueued v" by (cases v) simp

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

lemma tcbQueued_tcbFaultHandler_update [simp]:
  "tcbQueued (tcbFaultHandler_update f v) = tcbQueued v" by (cases v) simp

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

lemma tcbQueued_tcbIPCBuffer_update [simp]:
  "tcbQueued (tcbIPCBuffer_update f v) = tcbQueued v" by (cases v) simp

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

lemma tcbQueued_tcbBoundNotification_update [simp]:
  "tcbQueued (tcbBoundNotification_update f v) = tcbQueued v" by (cases v) simp

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

lemma tcbQueued_tcbArch_update [simp]:
  "tcbQueued (tcbArch_update f v) = tcbQueued v" by (cases v) simp

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

lemma tcbFault_tcbCTable_update [simp]:
  "tcbFault (tcbCTable_update f v) = tcbFault v" by (cases v) simp

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

lemma tcbFault_tcbVTable_update [simp]:
  "tcbFault (tcbVTable_update f v) = tcbFault v" by (cases v) simp

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

lemma tcbFault_tcbReply_update [simp]:
  "tcbFault (tcbReply_update f v) = tcbFault v" by (cases v) simp

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

lemma tcbFault_tcbCaller_update [simp]:
  "tcbFault (tcbCaller_update f v) = tcbFault v" by (cases v) simp

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

lemma tcbFault_tcbIPCBufferFrame_update [simp]:
  "tcbFault (tcbIPCBufferFrame_update f v) = tcbFault v" by (cases v) simp

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

lemma tcbFault_tcbDomain_update [simp]:
  "tcbFault (tcbDomain_update f v) = tcbFault v" by (cases v) simp

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

lemma tcbFault_tcbState_update [simp]:
  "tcbFault (tcbState_update f v) = tcbFault v" by (cases v) simp

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

lemma tcbFault_tcbMCP_update [simp]:
  "tcbFault (tcbMCP_update f v) = tcbFault v" by (cases v) simp

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

lemma tcbFault_tcbPriority_update [simp]:
  "tcbFault (tcbPriority_update f v) = tcbFault v" by (cases v) simp

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

lemma tcbFault_tcbQueued_update [simp]:
  "tcbFault (tcbQueued_update f v) = tcbFault v" by (cases v) simp

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

lemma tcbFault_tcbFault_update [simp]:
  "tcbFault (tcbFault_update f v) = f (tcbFault v)" by (cases v) simp

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

lemma tcbFault_tcbTimeSlice_update [simp]:
  "tcbFault (tcbTimeSlice_update f v) = tcbFault v" by (cases v) simp

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

lemma tcbFault_tcbFaultHandler_update [simp]:
  "tcbFault (tcbFaultHandler_update f v) = tcbFault v" by (cases v) simp

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

lemma tcbFault_tcbIPCBuffer_update [simp]:
  "tcbFault (tcbIPCBuffer_update f v) = tcbFault v" by (cases v) simp

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

lemma tcbFault_tcbBoundNotification_update [simp]:
  "tcbFault (tcbBoundNotification_update f v) = tcbFault v" by (cases v) simp

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

lemma tcbFault_tcbArch_update [simp]:
  "tcbFault (tcbArch_update f v) = tcbFault v" by (cases v) simp

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

lemma tcbTimeSlice_tcbCTable_update [simp]:
  "tcbTimeSlice (tcbCTable_update f v) = tcbTimeSlice v" by (cases v) simp

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

lemma tcbTimeSlice_tcbVTable_update [simp]:
  "tcbTimeSlice (tcbVTable_update f v) = tcbTimeSlice v" by (cases v) simp

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

lemma tcbTimeSlice_tcbReply_update [simp]:
  "tcbTimeSlice (tcbReply_update f v) = tcbTimeSlice v" by (cases v) simp

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

lemma tcbTimeSlice_tcbCaller_update [simp]:
  "tcbTimeSlice (tcbCaller_update f v) = tcbTimeSlice v" by (cases v) simp

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

lemma tcbTimeSlice_tcbDomain_update [simp]:
  "tcbTimeSlice (tcbDomain_update f v) = tcbTimeSlice v" by (cases v) simp

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

lemma tcbTimeSlice_tcbMCP_update [simp]:
  "tcbTimeSlice (tcbMCP_update f v) = tcbTimeSlice v" by (cases v) simp

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

lemma tcbTimeSlice_tcbPriority_update [simp]:
  "tcbTimeSlice (tcbPriority_update f v) = tcbTimeSlice v" by (cases v) simp

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

lemma tcbTimeSlice_tcbQueued_update [simp]:
  "tcbTimeSlice (tcbQueued_update f v) = tcbTimeSlice v" by (cases v) simp

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

lemma tcbTimeSlice_tcbFault_update [simp]:
  "tcbTimeSlice (tcbFault_update f v) = tcbTimeSlice v" by (cases v) simp

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

lemma tcbTimeSlice_tcbTimeSlice_update [simp]:
  "tcbTimeSlice (tcbTimeSlice_update f v) = f (tcbTimeSlice v)" by (cases v) simp

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

lemma tcbTimeSlice_tcbFaultHandler_update [simp]:
  "tcbTimeSlice (tcbFaultHandler_update f v) = tcbTimeSlice v" by (cases v) simp

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

lemma tcbFaultHandler_tcbCTable_update [simp]:
  "tcbFaultHandler (tcbCTable_update f v) = tcbFaultHandler v" by (cases v) simp

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