kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchStateData_H

lemma armKSGlobalPD_armKSHWASIDTable_update [simp]:
  "armKSGlobalPD (armKSHWASIDTable_update f v) = armKSGlobalPD v" by (cases v) simp

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

lemma armKSGlobalPD_armKSNextASID_update [simp]:
  "armKSGlobalPD (armKSNextASID_update f v) = armKSGlobalPD v" by (cases v) simp

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

lemma armKSGlobalPD_armKSASIDMap_update [simp]:
  "armKSGlobalPD (armKSASIDMap_update f v) = armKSGlobalPD v" by (cases v) simp

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

lemma armKSGlobalPD_armKSGlobalPD_update [simp]:
  "armKSGlobalPD (armKSGlobalPD_update f v) = f (armKSGlobalPD v)" by (cases v) simp

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

lemma armKSGlobalPD_armKSGlobalPTs_update [simp]:
  "armKSGlobalPD (armKSGlobalPTs_update f v) = armKSGlobalPD v" by (cases v) simp

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

lemma armKSGlobalPD_armKSKernelVSpace_update [simp]:
  "armKSGlobalPD (armKSKernelVSpace_update f v) = armKSGlobalPD v" by (cases v) simp

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

lemma armKSGlobalPTs_armKSASIDTable_update [simp]:
  "armKSGlobalPTs (armKSASIDTable_update f v) = armKSGlobalPTs v" by (cases v) simp

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

lemma armKSGlobalPTs_armKSNextASID_update [simp]:
  "armKSGlobalPTs (armKSNextASID_update f v) = armKSGlobalPTs v" by (cases v) simp

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

lemma armKSGlobalPTs_armKSASIDMap_update [simp]:
  "armKSGlobalPTs (armKSASIDMap_update f v) = armKSGlobalPTs v" by (cases v) simp

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

lemma armKSGlobalPTs_armKSGlobalPD_update [simp]:
  "armKSGlobalPTs (armKSGlobalPD_update f v) = armKSGlobalPTs v" by (cases v) simp

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

lemma armKSGlobalPTs_armKSGlobalPTs_update [simp]:
  "armKSGlobalPTs (armKSGlobalPTs_update f v) = f (armKSGlobalPTs v)" by (cases v) simp

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

lemma armKSGlobalPTs_armKSKernelVSpace_update [simp]:
  "armKSGlobalPTs (armKSKernelVSpace_update f v) = armKSGlobalPTs v" by (cases v) simp

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

lemma armKSKernelVSpace_armKSHWASIDTable_update [simp]:
  "armKSKernelVSpace (armKSHWASIDTable_update f v) = armKSKernelVSpace v" by (cases v) simp

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

lemma armKSKernelVSpace_armKSNextASID_update [simp]:
  "armKSKernelVSpace (armKSNextASID_update f v) = armKSKernelVSpace v" by (cases v) simp

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

lemma armKSKernelVSpace_armKSASIDMap_update [simp]:
  "armKSKernelVSpace (armKSASIDMap_update f v) = armKSKernelVSpace v" by (cases v) simp

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

lemma armKSKernelVSpace_armKSGlobalPD_update [simp]:
  "armKSKernelVSpace (armKSGlobalPD_update f v) = armKSKernelVSpace v" by (cases v) simp

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

lemma armKSKernelVSpace_armKSGlobalPTs_update [simp]:
  "armKSKernelVSpace (armKSGlobalPTs_update f v) = armKSKernelVSpace v" by (cases v) simp

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

lemma UserData_singleton [simp]:
  "(v = UserData) = True" "(UserData = v) = True" by (cases v, simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (v = UserData) = True &&& (UserData = v) = True
theory PSpaceStorable_H

lemma UserDataDevice_singleton [simp]:
  "(v = UserDataDevice) = True" "(UserDataDevice = v) = True" by (cases v, simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (v = UserDataDevice) = True &&& (UserDataDevice = v) = True
theory ArchRetypeDecls_H

lemma makePoolFrame_makePoolFrame_update [simp]:
  "makePoolFrame (makePoolFrame_update f v) = f (makePoolFrame v)" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. makePoolFrame (makePoolFrame_update f v) = f (makePoolFrame v)
theory ArchRetypeDecls_H

lemma makePoolFrame_makePoolSlot_update [simp]:
  "makePoolFrame (makePoolSlot_update f v) = makePoolFrame v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. makePoolFrame (makePoolSlot_update f v) = makePoolFrame v
theory ArchRetypeDecls_H

lemma makePoolFrame_makePoolParent_update [simp]:
  "makePoolFrame (makePoolParent_update f v) = makePoolFrame v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. makePoolFrame (makePoolParent_update f v) = makePoolFrame v
theory ArchRetypeDecls_H

lemma makePoolSlot_makePoolFrame_update [simp]:
  "makePoolSlot (makePoolFrame_update f v) = makePoolSlot v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. makePoolSlot (makePoolFrame_update f v) = makePoolSlot v
theory ArchRetypeDecls_H

lemma makePoolSlot_makePoolSlot_update [simp]:
  "makePoolSlot (makePoolSlot_update f v) = f (makePoolSlot v)" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. makePoolSlot (makePoolSlot_update f v) = f (makePoolSlot v)
theory ArchRetypeDecls_H

lemma makePoolSlot_makePoolParent_update [simp]:
  "makePoolSlot (makePoolParent_update f v) = makePoolSlot v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. makePoolSlot (makePoolParent_update f v) = makePoolSlot v
theory ArchRetypeDecls_H

lemma makePoolSlot_makePoolBase_update [simp]:
  "makePoolSlot (makePoolBase_update f v) = makePoolSlot v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. makePoolSlot (makePoolBase_update f v) = makePoolSlot v
theory ArchRetypeDecls_H

lemma makePoolParent_makePoolFrame_update [simp]:
  "makePoolParent (makePoolFrame_update f v) = makePoolParent v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. makePoolParent (makePoolFrame_update f v) = makePoolParent v
theory ArchRetypeDecls_H

lemma makePoolParent_makePoolSlot_update [simp]:
  "makePoolParent (makePoolSlot_update f v) = makePoolParent v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. makePoolParent (makePoolSlot_update f v) = makePoolParent v
theory ArchRetypeDecls_H

lemma makePoolParent_makePoolParent_update [simp]:
  "makePoolParent (makePoolParent_update f v) = f (makePoolParent v)" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. makePoolParent (makePoolParent_update f v) = f (makePoolParent v)
theory ArchRetypeDecls_H

lemma makePoolParent_makePoolBase_update [simp]:
  "makePoolParent (makePoolBase_update f v) = makePoolParent v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. makePoolParent (makePoolBase_update f v) = makePoolParent v
theory ArchRetypeDecls_H

lemma makePoolBase_makePoolFrame_update [simp]:
  "makePoolBase (makePoolFrame_update f v) = makePoolBase v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. makePoolBase (makePoolFrame_update f v) = makePoolBase v
theory ArchRetypeDecls_H

lemma makePoolBase_makePoolSlot_update [simp]:
  "makePoolBase (makePoolSlot_update f v) = makePoolBase v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. makePoolBase (makePoolSlot_update f v) = makePoolBase v
theory ArchRetypeDecls_H

lemma makePoolBase_makePoolParent_update [simp]:
  "makePoolBase (makePoolParent_update f v) = makePoolBase v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. makePoolBase (makePoolParent_update f v) = makePoolBase v
theory ArchRetypeDecls_H

lemma makePoolBase_makePoolBase_update [simp]:
  "makePoolBase (makePoolBase_update f v) = f (makePoolBase v)" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. makePoolBase (makePoolBase_update f v) = f (makePoolBase v)
theory ArchRetypeDecls_H

lemma assignASID_assignASID_update [simp]:
  "assignASID (assignASID_update f v) = f (assignASID v)" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. assignASID (assignASID_update f v) = f (assignASID v)
theory ArchRetypeDecls_H

lemma assignASID_assignASIDCTSlot_update [simp]:
  "assignASID (assignASIDCTSlot_update f v) = assignASID v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. assignASID (assignASIDCTSlot_update f v) = assignASID v
theory ArchRetypeDecls_H

lemma assignASIDPool_assignASID_update [simp]:
  "assignASIDPool (assignASID_update f v) = assignASIDPool v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. assignASIDPool (assignASID_update f v) = assignASIDPool v
theory ArchRetypeDecls_H

lemma assignASIDPool_assignASIDPool_update [simp]:
  "assignASIDPool (assignASIDPool_update f v) = f (assignASIDPool v)" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. assignASIDPool (assignASIDPool_update f v) = f (assignASIDPool v)
theory ArchRetypeDecls_H

lemma assignASIDPool_assignASIDCTSlot_update [simp]:
  "assignASIDPool (assignASIDCTSlot_update f v) = assignASIDPool v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. assignASIDPool (assignASIDCTSlot_update f v) = assignASIDPool v
theory ArchRetypeDecls_H

lemma assignASIDCTSlot_assignASID_update [simp]:
  "assignASIDCTSlot (assignASID_update f v) = assignASIDCTSlot v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. assignASIDCTSlot (assignASID_update f v) = assignASIDCTSlot v
theory ArchRetypeDecls_H

lemma assignASIDCTSlot_assignASIDPool_update [simp]:
  "assignASIDCTSlot (assignASIDPool_update f v) = assignASIDCTSlot v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. assignASIDCTSlot (assignASIDPool_update f v) = assignASIDCTSlot v
theory ArchRetypeDecls_H

lemma assignASIDCTSlot_assignASIDCTSlot_update [simp]:
  "assignASIDCTSlot (assignASIDCTSlot_update f v) = f (assignASIDCTSlot v)" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. assignASIDCTSlot (assignASIDCTSlot_update f v) = f (assignASIDCTSlot v)
theory ArchRetypeDecls_H

lemma issueHandlerIRQ_issueHandlerIRQ_update [simp]:
  "issueHandlerIRQ (issueHandlerIRQ_update f v) = f (issueHandlerIRQ v)" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. issueHandlerIRQ (issueHandlerIRQ_update f v) = f (issueHandlerIRQ v)
theory ArchRetypeDecls_H

lemma issueHandlerIRQ_issueHandlerSlot_update [simp]:
  "issueHandlerIRQ (issueHandlerSlot_update f v) = issueHandlerIRQ v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. issueHandlerIRQ (issueHandlerSlot_update f v) = issueHandlerIRQ v
theory ArchRetypeDecls_H

lemma issueHandlerIRQ_issueHandlerControllerSlot_update [simp]:
  "issueHandlerIRQ (issueHandlerControllerSlot_update f v) = issueHandlerIRQ v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. issueHandlerIRQ (issueHandlerControllerSlot_update f v) = issueHandlerIRQ v
theory ArchRetypeDecls_H

lemma issueHandlerIRQ_issueHandlerTrigger_update [simp]:
  "issueHandlerIRQ (issueHandlerTrigger_update f v) = issueHandlerIRQ v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. issueHandlerIRQ (issueHandlerTrigger_update f v) = issueHandlerIRQ v
theory ArchRetypeDecls_H

lemma issueHandlerSlot_issueHandlerIRQ_update [simp]:
  "issueHandlerSlot (issueHandlerIRQ_update f v) = issueHandlerSlot v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. issueHandlerSlot (issueHandlerIRQ_update f v) = issueHandlerSlot v
theory ArchRetypeDecls_H

lemma issueHandlerSlot_issueHandlerSlot_update [simp]:
  "issueHandlerSlot (issueHandlerSlot_update f v) = f (issueHandlerSlot v)" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. issueHandlerSlot (issueHandlerSlot_update f v) = f (issueHandlerSlot v)
theory ArchRetypeDecls_H

lemma issueHandlerSlot_issueHandlerTrigger_update [simp]:
  "issueHandlerSlot (issueHandlerTrigger_update f v) = issueHandlerSlot v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. issueHandlerSlot (issueHandlerTrigger_update f v) = issueHandlerSlot v
theory ArchRetypeDecls_H

lemma issueHandlerControllerSlot_issueHandlerIRQ_update [simp]:
  "issueHandlerControllerSlot (issueHandlerIRQ_update f v) = issueHandlerControllerSlot v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. issueHandlerControllerSlot (issueHandlerIRQ_update f v) = issueHandlerControllerSlot v
theory ArchRetypeDecls_H

lemma issueHandlerControllerSlot_issueHandlerSlot_update [simp]:
  "issueHandlerControllerSlot (issueHandlerSlot_update f v) = issueHandlerControllerSlot v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. issueHandlerControllerSlot (issueHandlerSlot_update f v) = issueHandlerControllerSlot v
theory ArchRetypeDecls_H

lemma issueHandlerControllerSlot_issueHandlerControllerSlot_update [simp]:
  "issueHandlerControllerSlot (issueHandlerControllerSlot_update f v) = f (issueHandlerControllerSlot v)" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. issueHandlerControllerSlot (issueHandlerControllerSlot_update f v) = f (issueHandlerControllerSlot v)
theory ArchRetypeDecls_H

lemma issueHandlerControllerSlot_issueHandlerTrigger_update [simp]:
  "issueHandlerControllerSlot (issueHandlerTrigger_update f v) = issueHandlerControllerSlot v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. issueHandlerControllerSlot (issueHandlerTrigger_update f v) = issueHandlerControllerSlot v
theory ArchRetypeDecls_H

lemma issueHandlerTrigger_issueHandlerIRQ_update [simp]:
  "issueHandlerTrigger (issueHandlerIRQ_update f v) = issueHandlerTrigger v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. issueHandlerTrigger (issueHandlerIRQ_update f v) = issueHandlerTrigger v
theory ArchRetypeDecls_H

lemma issueHandlerTrigger_issueHandlerControllerSlot_update [simp]:
  "issueHandlerTrigger (issueHandlerControllerSlot_update f v) = issueHandlerTrigger v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. issueHandlerTrigger (issueHandlerControllerSlot_update f v) = issueHandlerTrigger v
theory ArchRetypeDecls_H

lemma issueHandlerTrigger_issueHandlerTrigger_update [simp]:
  "issueHandlerTrigger (issueHandlerTrigger_update f v) = f (issueHandlerTrigger v)" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. issueHandlerTrigger (issueHandlerTrigger_update f v) = f (issueHandlerTrigger v)
theory Invocations_H

lemma retypeSource_retypeSource_update [simp]:
  "retypeSource (retypeSource_update f v) = f (retypeSource v)" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. retypeSource (retypeSource_update f v) = f (retypeSource v)
theory Invocations_H

lemma retypeSource_retypeResetUntyped_update [simp]:
  "retypeSource (retypeResetUntyped_update f v) = retypeSource v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. retypeSource (retypeResetUntyped_update f v) = retypeSource v
theory Invocations_H

lemma retypeSource_retypeRegionBase_update [simp]:
  "retypeSource (retypeRegionBase_update f v) = retypeSource v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. retypeSource (retypeRegionBase_update f v) = retypeSource v
theory Invocations_H

lemma retypeSource_retypeFreeRegionBase_update [simp]:
  "retypeSource (retypeFreeRegionBase_update f v) = retypeSource v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. retypeSource (retypeFreeRegionBase_update f v) = retypeSource v
theory Invocations_H

lemma retypeSource_retypeNewType_update [simp]:
  "retypeSource (retypeNewType_update f v) = retypeSource v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. retypeSource (retypeNewType_update f v) = retypeSource v
theory Invocations_H

lemma retypeSource_retypeNewSizeBits_update [simp]:
  "retypeSource (retypeNewSizeBits_update f v) = retypeSource v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. retypeSource (retypeNewSizeBits_update f v) = retypeSource v
theory Invocations_H

lemma retypeSource_retypeSlots_update [simp]:
  "retypeSource (retypeSlots_update f v) = retypeSource v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. retypeSource (retypeSlots_update f v) = retypeSource v
theory Invocations_H

lemma retypeResetUntyped_retypeSource_update [simp]:
  "retypeResetUntyped (retypeSource_update f v) = retypeResetUntyped v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. retypeResetUntyped (retypeSource_update f v) = retypeResetUntyped v
theory Invocations_H

lemma retypeResetUntyped_retypeResetUntyped_update [simp]:
  "retypeResetUntyped (retypeResetUntyped_update f v) = f (retypeResetUntyped v)" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. retypeResetUntyped (retypeResetUntyped_update f v) = f (retypeResetUntyped v)
theory Invocations_H

lemma retypeResetUntyped_retypeRegionBase_update [simp]:
  "retypeResetUntyped (retypeRegionBase_update f v) = retypeResetUntyped v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. retypeResetUntyped (retypeRegionBase_update f v) = retypeResetUntyped v
theory Invocations_H

lemma retypeResetUntyped_retypeFreeRegionBase_update [simp]:
  "retypeResetUntyped (retypeFreeRegionBase_update f v) = retypeResetUntyped v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. retypeResetUntyped (retypeFreeRegionBase_update f v) = retypeResetUntyped v
theory Invocations_H

lemma retypeResetUntyped_retypeSlots_update [simp]:
  "retypeResetUntyped (retypeSlots_update f v) = retypeResetUntyped v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. retypeResetUntyped (retypeSlots_update f v) = retypeResetUntyped v
theory Invocations_H

lemma retypeResetUntyped_retypeIsDevice_update [simp]:
  "retypeResetUntyped (retypeIsDevice_update f v) = retypeResetUntyped v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. retypeResetUntyped (retypeIsDevice_update f v) = retypeResetUntyped v
theory Invocations_H

lemma retypeRegionBase_retypeSource_update [simp]:
  "retypeRegionBase (retypeSource_update f v) = retypeRegionBase v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. retypeRegionBase (retypeSource_update f v) = retypeRegionBase v
theory Invocations_H

lemma retypeRegionBase_retypeResetUntyped_update [simp]:
  "retypeRegionBase (retypeResetUntyped_update f v) = retypeRegionBase v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. retypeRegionBase (retypeResetUntyped_update f v) = retypeRegionBase v
theory Invocations_H

lemma retypeRegionBase_retypeRegionBase_update [simp]:
  "retypeRegionBase (retypeRegionBase_update f v) = f (retypeRegionBase v)" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. retypeRegionBase (retypeRegionBase_update f v) = f (retypeRegionBase v)
theory Invocations_H

lemma retypeRegionBase_retypeFreeRegionBase_update [simp]:
  "retypeRegionBase (retypeFreeRegionBase_update f v) = retypeRegionBase v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. retypeRegionBase (retypeFreeRegionBase_update f v) = retypeRegionBase v
theory Invocations_H

lemma retypeRegionBase_retypeNewType_update [simp]:
  "retypeRegionBase (retypeNewType_update f v) = retypeRegionBase v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. retypeRegionBase (retypeNewType_update f v) = retypeRegionBase v
theory Invocations_H

lemma retypeRegionBase_retypeNewSizeBits_update [simp]:
  "retypeRegionBase (retypeNewSizeBits_update f v) = retypeRegionBase v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. retypeRegionBase (retypeNewSizeBits_update f v) = retypeRegionBase v
theory Invocations_H

lemma retypeRegionBase_retypeSlots_update [simp]:
  "retypeRegionBase (retypeSlots_update f v) = retypeRegionBase v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. retypeRegionBase (retypeSlots_update f v) = retypeRegionBase v
theory Invocations_H

lemma retypeRegionBase_retypeIsDevice_update [simp]:
  "retypeRegionBase (retypeIsDevice_update f v) = retypeRegionBase v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. retypeRegionBase (retypeIsDevice_update f v) = retypeRegionBase v
theory Invocations_H

lemma retypeFreeRegionBase_retypeResetUntyped_update [simp]:
  "retypeFreeRegionBase (retypeResetUntyped_update f v) = retypeFreeRegionBase v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. retypeFreeRegionBase (retypeResetUntyped_update f v) = retypeFreeRegionBase v
theory Invocations_H

lemma retypeFreeRegionBase_retypeRegionBase_update [simp]:
  "retypeFreeRegionBase (retypeRegionBase_update f v) = retypeFreeRegionBase v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. retypeFreeRegionBase (retypeRegionBase_update f v) = retypeFreeRegionBase v
theory Invocations_H

lemma retypeFreeRegionBase_retypeFreeRegionBase_update [simp]:
  "retypeFreeRegionBase (retypeFreeRegionBase_update f v) = f (retypeFreeRegionBase v)" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. retypeFreeRegionBase (retypeFreeRegionBase_update f v) = f (retypeFreeRegionBase v)
theory Invocations_H

lemma retypeFreeRegionBase_retypeNewType_update [simp]:
  "retypeFreeRegionBase (retypeNewType_update f v) = retypeFreeRegionBase v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. retypeFreeRegionBase (retypeNewType_update f v) = retypeFreeRegionBase v
theory Invocations_H

lemma retypeFreeRegionBase_retypeNewSizeBits_update [simp]:
  "retypeFreeRegionBase (retypeNewSizeBits_update f v) = retypeFreeRegionBase v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. retypeFreeRegionBase (retypeNewSizeBits_update f v) = retypeFreeRegionBase v
theory Invocations_H

lemma retypeFreeRegionBase_retypeSlots_update [simp]:
  "retypeFreeRegionBase (retypeSlots_update f v) = retypeFreeRegionBase v" by (cases v) simp

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