kings-crown/FVELER_Isabelle huggingface dataset:
theory Structures_H

lemma tcbFaultHandler_tcbVTable_update [simp]:
  "tcbFaultHandler (tcbVTable_update f v) = tcbFaultHandler v" by (cases v) simp

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

lemma tcbFaultHandler_tcbReply_update [simp]:
  "tcbFaultHandler (tcbReply_update f v) = tcbFaultHandler v" by (cases v) simp

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

lemma tcbFaultHandler_tcbCaller_update [simp]:
  "tcbFaultHandler (tcbCaller_update f v) = tcbFaultHandler v" by (cases v) simp

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

lemma tcbFaultHandler_tcbIPCBufferFrame_update [simp]:
  "tcbFaultHandler (tcbIPCBufferFrame_update f v) = tcbFaultHandler v" by (cases v) simp

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

lemma tcbFaultHandler_tcbDomain_update [simp]:
  "tcbFaultHandler (tcbDomain_update f v) = tcbFaultHandler v" by (cases v) simp

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

lemma tcbFaultHandler_tcbState_update [simp]:
  "tcbFaultHandler (tcbState_update f v) = tcbFaultHandler v" by (cases v) simp

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

lemma tcbFaultHandler_tcbMCP_update [simp]:
  "tcbFaultHandler (tcbMCP_update f v) = tcbFaultHandler v" by (cases v) simp

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

lemma tcbFaultHandler_tcbPriority_update [simp]:
  "tcbFaultHandler (tcbPriority_update f v) = tcbFaultHandler v" by (cases v) simp

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

lemma tcbFaultHandler_tcbQueued_update [simp]:
  "tcbFaultHandler (tcbQueued_update f v) = tcbFaultHandler v" by (cases v) simp

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

lemma tcbFaultHandler_tcbFault_update [simp]:
  "tcbFaultHandler (tcbFault_update f v) = tcbFaultHandler v" by (cases v) simp

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

lemma tcbFaultHandler_tcbTimeSlice_update [simp]:
  "tcbFaultHandler (tcbTimeSlice_update f v) = tcbFaultHandler v" by (cases v) simp

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

lemma tcbFaultHandler_tcbIPCBuffer_update [simp]:
  "tcbFaultHandler (tcbIPCBuffer_update f v) = tcbFaultHandler v" by (cases v) simp

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

lemma tcbFaultHandler_tcbBoundNotification_update [simp]:
  "tcbFaultHandler (tcbBoundNotification_update f v) = tcbFaultHandler v" by (cases v) simp

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

lemma tcbFaultHandler_tcbArch_update [simp]:
  "tcbFaultHandler (tcbArch_update f v) = tcbFaultHandler v" by (cases v) simp

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

lemma tcbIPCBuffer_tcbCTable_update [simp]:
  "tcbIPCBuffer (tcbCTable_update f v) = tcbIPCBuffer v" by (cases v) simp

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

lemma tcbIPCBuffer_tcbVTable_update [simp]:
  "tcbIPCBuffer (tcbVTable_update f v) = tcbIPCBuffer v" by (cases v) simp

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

lemma tcbIPCBuffer_tcbReply_update [simp]:
  "tcbIPCBuffer (tcbReply_update f v) = tcbIPCBuffer v" by (cases v) simp

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

lemma tcbIPCBuffer_tcbCaller_update [simp]:
  "tcbIPCBuffer (tcbCaller_update f v) = tcbIPCBuffer v" by (cases v) simp

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

lemma tcbIPCBuffer_tcbIPCBufferFrame_update [simp]:
  "tcbIPCBuffer (tcbIPCBufferFrame_update f v) = tcbIPCBuffer v" by (cases v) simp

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

lemma tcbIPCBuffer_tcbDomain_update [simp]:
  "tcbIPCBuffer (tcbDomain_update f v) = tcbIPCBuffer v" by (cases v) simp

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

lemma tcbIPCBuffer_tcbState_update [simp]:
  "tcbIPCBuffer (tcbState_update f v) = tcbIPCBuffer v" by (cases v) simp

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

lemma tcbIPCBuffer_tcbMCP_update [simp]:
  "tcbIPCBuffer (tcbMCP_update f v) = tcbIPCBuffer v" by (cases v) simp

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

lemma tcbIPCBuffer_tcbPriority_update [simp]:
  "tcbIPCBuffer (tcbPriority_update f v) = tcbIPCBuffer v" by (cases v) simp

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

lemma tcbIPCBuffer_tcbQueued_update [simp]:
  "tcbIPCBuffer (tcbQueued_update f v) = tcbIPCBuffer v" by (cases v) simp

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

lemma tcbIPCBuffer_tcbFault_update [simp]:
  "tcbIPCBuffer (tcbFault_update f v) = tcbIPCBuffer v" by (cases v) simp

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

lemma tcbIPCBuffer_tcbTimeSlice_update [simp]:
  "tcbIPCBuffer (tcbTimeSlice_update f v) = tcbIPCBuffer v" by (cases v) simp

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

lemma tcbIPCBuffer_tcbFaultHandler_update [simp]:
  "tcbIPCBuffer (tcbFaultHandler_update f v) = tcbIPCBuffer v" by (cases v) simp

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

lemma tcbIPCBuffer_tcbIPCBuffer_update [simp]:
  "tcbIPCBuffer (tcbIPCBuffer_update f v) = f (tcbIPCBuffer v)" by (cases v) simp

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

lemma tcbIPCBuffer_tcbBoundNotification_update [simp]:
  "tcbIPCBuffer (tcbBoundNotification_update f v) = tcbIPCBuffer v" by (cases v) simp

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

lemma tcbIPCBuffer_tcbArch_update [simp]:
  "tcbIPCBuffer (tcbArch_update f v) = tcbIPCBuffer v" by (cases v) simp

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

lemma tcbBoundNotification_tcbCTable_update [simp]:
  "tcbBoundNotification (tcbCTable_update f v) = tcbBoundNotification v" by (cases v) simp

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

lemma tcbBoundNotification_tcbVTable_update [simp]:
  "tcbBoundNotification (tcbVTable_update f v) = tcbBoundNotification v" by (cases v) simp

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

lemma tcbBoundNotification_tcbReply_update [simp]:
  "tcbBoundNotification (tcbReply_update f v) = tcbBoundNotification v" by (cases v) simp

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

lemma tcbBoundNotification_tcbIPCBufferFrame_update [simp]:
  "tcbBoundNotification (tcbIPCBufferFrame_update f v) = tcbBoundNotification v" by (cases v) simp

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

lemma tcbBoundNotification_tcbDomain_update [simp]:
  "tcbBoundNotification (tcbDomain_update f v) = tcbBoundNotification v" by (cases v) simp

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

lemma tcbBoundNotification_tcbState_update [simp]:
  "tcbBoundNotification (tcbState_update f v) = tcbBoundNotification v" by (cases v) simp

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

lemma tcbBoundNotification_tcbMCP_update [simp]:
  "tcbBoundNotification (tcbMCP_update f v) = tcbBoundNotification v" by (cases v) simp

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

lemma tcbBoundNotification_tcbQueued_update [simp]:
  "tcbBoundNotification (tcbQueued_update f v) = tcbBoundNotification v" by (cases v) simp

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

lemma tcbBoundNotification_tcbFault_update [simp]:
  "tcbBoundNotification (tcbFault_update f v) = tcbBoundNotification v" by (cases v) simp

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

lemma tcbBoundNotification_tcbTimeSlice_update [simp]:
  "tcbBoundNotification (tcbTimeSlice_update f v) = tcbBoundNotification v" by (cases v) simp

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

lemma tcbBoundNotification_tcbFaultHandler_update [simp]:
  "tcbBoundNotification (tcbFaultHandler_update f v) = tcbBoundNotification v" by (cases v) simp

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

lemma tcbBoundNotification_tcbIPCBuffer_update [simp]:
  "tcbBoundNotification (tcbIPCBuffer_update f v) = tcbBoundNotification v" by (cases v) simp

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

lemma tcbBoundNotification_tcbBoundNotification_update [simp]:
  "tcbBoundNotification (tcbBoundNotification_update f v) = f (tcbBoundNotification v)" by (cases v) simp

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

lemma tcbBoundNotification_tcbArch_update [simp]:
  "tcbBoundNotification (tcbArch_update f v) = tcbBoundNotification v" by (cases v) simp

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

lemma tcbArch_tcbCTable_update [simp]:
  "tcbArch (tcbCTable_update f v) = tcbArch v" by (cases v) simp

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

lemma tcbArch_tcbVTable_update [simp]:
  "tcbArch (tcbVTable_update f v) = tcbArch v" by (cases v) simp

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

lemma tcbArch_tcbReply_update [simp]:
  "tcbArch (tcbReply_update f v) = tcbArch v" by (cases v) simp

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

lemma tcbArch_tcbCaller_update [simp]:
  "tcbArch (tcbCaller_update f v) = tcbArch v" by (cases v) simp

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

lemma tcbArch_tcbIPCBufferFrame_update [simp]:
  "tcbArch (tcbIPCBufferFrame_update f v) = tcbArch v" by (cases v) simp

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

lemma tcbArch_tcbDomain_update [simp]:
  "tcbArch (tcbDomain_update f v) = tcbArch v" by (cases v) simp

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

lemma tcbArch_tcbState_update [simp]:
  "tcbArch (tcbState_update f v) = tcbArch v" by (cases v) simp

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

lemma tcbArch_tcbMCP_update [simp]:
  "tcbArch (tcbMCP_update f v) = tcbArch v" by (cases v) simp

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

lemma tcbArch_tcbPriority_update [simp]:
  "tcbArch (tcbPriority_update f v) = tcbArch v" by (cases v) simp

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

lemma tcbArch_tcbQueued_update [simp]:
  "tcbArch (tcbQueued_update f v) = tcbArch v" by (cases v) simp

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

lemma tcbArch_tcbTimeSlice_update [simp]:
  "tcbArch (tcbTimeSlice_update f v) = tcbArch v" by (cases v) simp

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

lemma tcbArch_tcbFaultHandler_update [simp]:
  "tcbArch (tcbFaultHandler_update f v) = tcbArch v" by (cases v) simp

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

lemma tcbArch_tcbIPCBuffer_update [simp]:
  "tcbArch (tcbIPCBuffer_update f v) = tcbArch v" by (cases v) simp

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

lemma tcbArch_tcbBoundNotification_update [simp]:
  "tcbArch (tcbBoundNotification_update f v) = tcbArch v" by (cases v) simp

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

lemma tcbArch_tcbArch_update [simp]:
  "tcbArch (tcbArch_update f v) = f (tcbArch v)" by (cases v) simp

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

lemma intStateIRQNode_intStateIRQNode_update [simp]:
  "intStateIRQNode (intStateIRQNode_update f v) = f (intStateIRQNode v)" by (cases v) simp

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

lemma intStateIRQTable_intStateIRQNode_update [simp]:
  "intStateIRQTable (intStateIRQNode_update f v) = intStateIRQTable v" by (cases v) simp

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

lemma intStateIRQTable_intStateIRQTable_update [simp]:
  "intStateIRQTable (intStateIRQTable_update f v) = f (intStateIRQTable v)" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. intStateIRQTable (intStateIRQTable_update f v) = f (intStateIRQTable v)
theory ArchStateData_H

lemma armKSASIDTable_armKSASIDTable_update [simp]:
  "armKSASIDTable (armKSASIDTable_update f v) = f (armKSASIDTable v)" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. armKSASIDTable (armKSASIDTable_update f v) = f (armKSASIDTable v)
theory ArchStateData_H

lemma armKSASIDTable_armKSHWASIDTable_update [simp]:
  "armKSASIDTable (armKSHWASIDTable_update f v) = armKSASIDTable v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. armKSASIDTable (armKSHWASIDTable_update f v) = armKSASIDTable v
theory ArchStateData_H

lemma armKSASIDTable_armKSNextASID_update [simp]:
  "armKSASIDTable (armKSNextASID_update f v) = armKSASIDTable v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. armKSASIDTable (armKSNextASID_update f v) = armKSASIDTable v
theory ArchStateData_H

lemma armKSASIDTable_armKSASIDMap_update [simp]:
  "armKSASIDTable (armKSASIDMap_update f v) = armKSASIDTable v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. armKSASIDTable (armKSASIDMap_update f v) = armKSASIDTable v
theory ArchStateData_H

lemma armKSASIDTable_armKSGlobalPD_update [simp]:
  "armKSASIDTable (armKSGlobalPD_update f v) = armKSASIDTable v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. armKSASIDTable (armKSGlobalPD_update f v) = armKSASIDTable v
theory ArchStateData_H

lemma armKSASIDTable_armKSKernelVSpace_update [simp]:
  "armKSASIDTable (armKSKernelVSpace_update f v) = armKSASIDTable v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. armKSASIDTable (armKSKernelVSpace_update f v) = armKSASIDTable v
theory ArchStateData_H

lemma armKSHWASIDTable_armKSASIDTable_update [simp]:
  "armKSHWASIDTable (armKSASIDTable_update f v) = armKSHWASIDTable v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. armKSHWASIDTable (armKSASIDTable_update f v) = armKSHWASIDTable v
theory ArchStateData_H

lemma armKSHWASIDTable_armKSHWASIDTable_update [simp]:
  "armKSHWASIDTable (armKSHWASIDTable_update f v) = f (armKSHWASIDTable v)" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. armKSHWASIDTable (armKSHWASIDTable_update f v) = f (armKSHWASIDTable v)
theory ArchStateData_H

lemma armKSHWASIDTable_armKSNextASID_update [simp]:
  "armKSHWASIDTable (armKSNextASID_update f v) = armKSHWASIDTable v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. armKSHWASIDTable (armKSNextASID_update f v) = armKSHWASIDTable v
theory ArchStateData_H

lemma armKSHWASIDTable_armKSASIDMap_update [simp]:
  "armKSHWASIDTable (armKSASIDMap_update f v) = armKSHWASIDTable v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. armKSHWASIDTable (armKSASIDMap_update f v) = armKSHWASIDTable v
theory ArchStateData_H

lemma armKSHWASIDTable_armKSGlobalPD_update [simp]:
  "armKSHWASIDTable (armKSGlobalPD_update f v) = armKSHWASIDTable v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. armKSHWASIDTable (armKSGlobalPD_update f v) = armKSHWASIDTable v
theory ArchStateData_H

lemma armKSHWASIDTable_armKSGlobalPTs_update [simp]:
  "armKSHWASIDTable (armKSGlobalPTs_update f v) = armKSHWASIDTable v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. armKSHWASIDTable (armKSGlobalPTs_update f v) = armKSHWASIDTable v
theory ArchStateData_H

lemma armKSHWASIDTable_armKSKernelVSpace_update [simp]:
  "armKSHWASIDTable (armKSKernelVSpace_update f v) = armKSHWASIDTable v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. armKSHWASIDTable (armKSKernelVSpace_update f v) = armKSHWASIDTable v
theory ArchStateData_H

lemma armKSNextASID_armKSASIDTable_update [simp]:
  "armKSNextASID (armKSASIDTable_update f v) = armKSNextASID v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. armKSNextASID (armKSASIDTable_update f v) = armKSNextASID v
theory ArchStateData_H

lemma armKSNextASID_armKSHWASIDTable_update [simp]:
  "armKSNextASID (armKSHWASIDTable_update f v) = armKSNextASID v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. armKSNextASID (armKSHWASIDTable_update f v) = armKSNextASID v
theory ArchStateData_H

lemma armKSNextASID_armKSNextASID_update [simp]:
  "armKSNextASID (armKSNextASID_update f v) = f (armKSNextASID v)" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. armKSNextASID (armKSNextASID_update f v) = f (armKSNextASID v)
theory ArchStateData_H

lemma armKSNextASID_armKSASIDMap_update [simp]:
  "armKSNextASID (armKSASIDMap_update f v) = armKSNextASID v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. armKSNextASID (armKSASIDMap_update f v) = armKSNextASID v
theory ArchStateData_H

lemma armKSNextASID_armKSGlobalPD_update [simp]:
  "armKSNextASID (armKSGlobalPD_update f v) = armKSNextASID v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. armKSNextASID (armKSGlobalPD_update f v) = armKSNextASID v
theory ArchStateData_H

lemma armKSNextASID_armKSGlobalPTs_update [simp]:
  "armKSNextASID (armKSGlobalPTs_update f v) = armKSNextASID v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. armKSNextASID (armKSGlobalPTs_update f v) = armKSNextASID v
theory ArchStateData_H

lemma armKSNextASID_armKSKernelVSpace_update [simp]:
  "armKSNextASID (armKSKernelVSpace_update f v) = armKSNextASID v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. armKSNextASID (armKSKernelVSpace_update f v) = armKSNextASID v
theory ArchStateData_H

lemma armKSASIDMap_armKSASIDTable_update [simp]:
  "armKSASIDMap (armKSASIDTable_update f v) = armKSASIDMap v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. armKSASIDMap (armKSASIDTable_update f v) = armKSASIDMap v
theory ArchStateData_H

lemma armKSASIDMap_armKSHWASIDTable_update [simp]:
  "armKSASIDMap (armKSHWASIDTable_update f v) = armKSASIDMap v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. armKSASIDMap (armKSHWASIDTable_update f v) = armKSASIDMap v
theory ArchStateData_H

lemma armKSASIDMap_armKSASIDMap_update [simp]:
  "armKSASIDMap (armKSASIDMap_update f v) = f (armKSASIDMap v)" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. armKSASIDMap (armKSASIDMap_update f v) = f (armKSASIDMap v)
theory ArchStateData_H

lemma armKSASIDMap_armKSGlobalPD_update [simp]:
  "armKSASIDMap (armKSGlobalPD_update f v) = armKSASIDMap v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. armKSASIDMap (armKSGlobalPD_update f v) = armKSASIDMap v
theory ArchStateData_H

lemma armKSASIDMap_armKSGlobalPTs_update [simp]:
  "armKSASIDMap (armKSGlobalPTs_update f v) = armKSASIDMap v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. armKSASIDMap (armKSGlobalPTs_update f v) = armKSASIDMap v
theory ArchStateData_H

lemma armKSASIDMap_armKSKernelVSpace_update [simp]:
  "armKSASIDMap (armKSKernelVSpace_update f v) = armKSASIDMap v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. armKSASIDMap (armKSKernelVSpace_update f v) = armKSASIDMap v
theory ArchStateData_H

lemma armKSGlobalPD_armKSASIDTable_update [simp]:
  "armKSGlobalPD (armKSASIDTable_update f v) = armKSGlobalPD v" by (cases v) simp

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