kings-crown/FVELER_Isabelle huggingface dataset:
theory HaskellLib_H

lemma show_simp_away[simp]: "S @ show t = S" by (simp add: show_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. S @ show t = S
theory HaskellLib_H

lemma finite_surj_type:
  "\<lbrakk> (\<forall>x. \<exists>y. (x :: 'b) = f (y :: 'a)); finite (UNIV :: 'a set) \<rbrakk> \<Longrightarrow> finite (UNIV :: 'b set)" apply (erule finite_surj) apply safe apply (erule allE) apply safe apply (erule image_eqI) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x. \<exists>y. x = f y; finite UNIV\<rbrakk> \<Longrightarrow> finite UNIV proof (prove)
goal (1 subgoal):
 1. \<forall>x. \<exists>y. x = f y \<Longrightarrow> UNIV \<subseteq> range ?f proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>x. \<exists>y. x = f y; x \<in> UNIV\<rbrakk> \<Longrightarrow> x \<in> range ?f proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> UNIV; \<exists>y. ?x3 x = f y\<rbrakk> \<Longrightarrow> x \<in> range ?f proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> UNIV; ?x3 x = f y\<rbrakk> \<Longrightarrow> x \<in> range ?f proof (prove)
goal (1 subgoal):
 1. \<And>x y. x \<in> UNIV \<Longrightarrow> y \<in> UNIV proof (prove)
goal:
No subgoals!
theory HaskellLib_H

lemma finite_finite[simp]: "finite (s :: ('a :: finite) set)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. finite s
theory HaskellLib_H

lemma finite_inv_card_less:
   "(card (UNIV - insert (a :: ('a :: finite)) s) < card (UNIV - s)) = (a \<notin> s)" by (simp add: finite_inv_card_less')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (card (UNIV - insert a s) < card (UNIV - s)) = (a \<notin> s)
theory HaskellLib_H

lemma "[(x,1) . x \<leftarrow> [0..10]] = [(x,1) | x \<leftarrow> [0..10]]" by (rule refl)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. map (\<lambda>x. (x, 1::'a)) [0..10] = map (\<lambda>x. (x, 1::'a)) [0..10]
theory HaskellLib_H

lemma ohaskell_assert_wp[wp]:
  "\<lblot>\<lambda>s. Q \<longrightarrow> P () s\<rblot> ohaskell_assert Q [] \<lblot>P\<rblot>" apply (clarsimp simp: ohaskell_assert_def) apply (intro conjI; wpsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lblot>\<lambda>s. Q \<longrightarrow> P () s\<rblot> ohaskell_assert Q [] \<lblot>P\<rblot> proof (prove)
goal (1 subgoal):
 1. (Q \<longrightarrow> \<lblot>P ()\<rblot> oreturn () \<lblot>P\<rblot>) \<and> (\<not> Q \<longrightarrow> \<lblot>\<lambda>s. True\<rblot> ofail \<lblot>P\<rblot>) proof (prove)
goal:
No subgoals!
theory HaskellLib_H

lemma ohaskell_assert_sp:
  "\<lblot>P\<rblot> ohaskell_assert Q [] \<lblot>\<lambda>_ s. P s \<and> Q\<rblot>" apply (clarsimp simp: ohaskell_assert_def) apply (intro conjI; wpsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lblot>P\<rblot> ohaskell_assert Q [] \<lblot>\<lambda>_ s. P s \<and> Q\<rblot> proof (prove)
goal (1 subgoal):
 1. (Q \<longrightarrow> \<lblot>P\<rblot> oreturn () \<lblot>\<lambda>_. P\<rblot>) \<and> (\<not> Q \<longrightarrow> \<lblot>P\<rblot> ofail \<lblot>\<lambda>_ s. False\<rblot>) proof (prove)
goal:
No subgoals!
theory HaskellLib_H

lemma gets_the_ohaskell_assert:
  "gets_the (ohaskell_assert P []) = assert P" by (clarsimp simp: ohaskell_assert_def split: if_splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. gets_the (ohaskell_assert P []) = assert P
theory Hardware_H

lemma armPageCacheable_armPageCacheable_update [simp]:
  "armPageCacheable (armPageCacheable_update f v) = f (armPageCacheable v)" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. armPageCacheable (armPageCacheable_update f v) = f (armPageCacheable v)
theory Hardware_H

lemma armPageCacheable_armParityEnabled_update [simp]:
  "armPageCacheable (armParityEnabled_update f v) = armPageCacheable v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. armPageCacheable (armParityEnabled_update f v) = armPageCacheable v
theory Hardware_H

lemma armPageCacheable_armExecuteNever_update [simp]:
  "armPageCacheable (armExecuteNever_update f v) = armPageCacheable v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. armPageCacheable (armExecuteNever_update f v) = armPageCacheable v
theory Hardware_H

lemma armParityEnabled_armPageCacheable_update [simp]:
  "armParityEnabled (armPageCacheable_update f v) = armParityEnabled v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. armParityEnabled (armPageCacheable_update f v) = armParityEnabled v
theory Hardware_H

lemma armParityEnabled_armParityEnabled_update [simp]:
  "armParityEnabled (armParityEnabled_update f v) = f (armParityEnabled v)" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. armParityEnabled (armParityEnabled_update f v) = f (armParityEnabled v)
theory Hardware_H

lemma armParityEnabled_armExecuteNever_update [simp]:
  "armParityEnabled (armExecuteNever_update f v) = armParityEnabled v" by (cases v) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. armParityEnabled (armExecuteNever_update f v) = armParityEnabled v
theory Hardware_H

lemma armExecuteNever_armParityEnabled_update [simp]:
  "armExecuteNever (armParityEnabled_update f v) = armExecuteNever v" by (cases v) simp

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

lemma capAllowWrite_capAllowWrite_update [simp]:
  "capAllowWrite (capAllowWrite_update f v) = f (capAllowWrite v)" by (cases v) simp

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

lemma capAllowWrite_capAllowRead_update [simp]:
  "capAllowWrite (capAllowRead_update f v) = capAllowWrite v" by (cases v) simp

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

lemma capAllowWrite_capAllowGrant_update [simp]:
  "capAllowWrite (capAllowGrant_update f v) = capAllowWrite v" by (cases v) simp

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

lemma capAllowWrite_capAllowGrantReply_update [simp]:
  "capAllowWrite (capAllowGrantReply_update f v) = capAllowWrite v" by (cases v) simp

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

lemma capAllowRead_capAllowRead_update [simp]:
  "capAllowRead (capAllowRead_update f v) = f (capAllowRead v)" by (cases v) simp

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

lemma capAllowRead_capAllowGrant_update [simp]:
  "capAllowRead (capAllowGrant_update f v) = capAllowRead v" by (cases v) simp

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

lemma capAllowRead_capAllowGrantReply_update [simp]:
  "capAllowRead (capAllowGrantReply_update f v) = capAllowRead v" by (cases v) simp

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

lemma capAllowGrant_capAllowWrite_update [simp]:
  "capAllowGrant (capAllowWrite_update f v) = capAllowGrant v" by (cases v) simp

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

lemma capAllowGrant_capAllowRead_update [simp]:
  "capAllowGrant (capAllowRead_update f v) = capAllowGrant v" by (cases v) simp

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

lemma capAllowGrant_capAllowGrant_update [simp]:
  "capAllowGrant (capAllowGrant_update f v) = f (capAllowGrant v)" by (cases v) simp

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

lemma capAllowGrant_capAllowGrantReply_update [simp]:
  "capAllowGrant (capAllowGrantReply_update f v) = capAllowGrant v" by (cases v) simp

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

lemma capAllowGrantReply_capAllowWrite_update [simp]:
  "capAllowGrantReply (capAllowWrite_update f v) = capAllowGrantReply v" by (cases v) simp

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

lemma capAllowGrantReply_capAllowRead_update [simp]:
  "capAllowGrantReply (capAllowRead_update f v) = capAllowGrantReply v" by (cases v) simp

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

lemma capAllowGrantReply_capAllowGrant_update [simp]:
  "capAllowGrantReply (capAllowGrant_update f v) = capAllowGrantReply v" by (cases v) simp

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

lemma capAllowGrantReply_capAllowGrantReply_update [simp]:
  "capAllowGrantReply (capAllowGrantReply_update f v) = f (capAllowGrantReply v)" by (cases v) simp

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

lemma msgLength_msgLength_update [simp]:
  "msgLength (msgLength_update f v) = f (msgLength v)" by (cases v) simp

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

lemma msgLength_msgExtraCaps_update [simp]:
  "msgLength (msgExtraCaps_update f v) = msgLength v" by (cases v) simp

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

lemma msgLength_msgCapsUnwrapped_update [simp]:
  "msgLength (msgCapsUnwrapped_update f v) = msgLength v" by (cases v) simp

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

lemma msgLength_msgLabel_update [simp]:
  "msgLength (msgLabel_update f v) = msgLength v" by (cases v) simp

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

lemma msgExtraCaps_msgLength_update [simp]:
  "msgExtraCaps (msgLength_update f v) = msgExtraCaps v" by (cases v) simp

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

lemma msgExtraCaps_msgExtraCaps_update [simp]:
  "msgExtraCaps (msgExtraCaps_update f v) = f (msgExtraCaps v)" by (cases v) simp

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

lemma msgExtraCaps_msgCapsUnwrapped_update [simp]:
  "msgExtraCaps (msgCapsUnwrapped_update f v) = msgExtraCaps v" by (cases v) simp

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

lemma msgExtraCaps_msgLabel_update [simp]:
  "msgExtraCaps (msgLabel_update f v) = msgExtraCaps v" by (cases v) simp

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

lemma msgCapsUnwrapped_msgLength_update [simp]:
  "msgCapsUnwrapped (msgLength_update f v) = msgCapsUnwrapped v" by (cases v) simp

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

lemma msgCapsUnwrapped_msgExtraCaps_update [simp]:
  "msgCapsUnwrapped (msgExtraCaps_update f v) = msgCapsUnwrapped v" by (cases v) simp

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

lemma msgCapsUnwrapped_msgCapsUnwrapped_update [simp]:
  "msgCapsUnwrapped (msgCapsUnwrapped_update f v) = f (msgCapsUnwrapped v)" by (cases v) simp

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

lemma msgCapsUnwrapped_msgLabel_update [simp]:
  "msgCapsUnwrapped (msgLabel_update f v) = msgCapsUnwrapped v" by (cases v) simp

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

lemma msgLabel_msgLength_update [simp]:
  "msgLabel (msgLength_update f v) = msgLabel v" by (cases v) simp

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

lemma msgLabel_msgExtraCaps_update [simp]:
  "msgLabel (msgExtraCaps_update f v) = msgLabel v" by (cases v) simp

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

lemma msgLabel_msgCapsUnwrapped_update [simp]:
  "msgLabel (msgCapsUnwrapped_update f v) = msgLabel v" by (cases v) simp

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

lemma msgLabel_msgLabel_update [simp]:
  "msgLabel (msgLabel_update f v) = f (msgLabel v)" by (cases v) simp

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

lemma ctReceiveRoot_ctReceiveIndex_update [simp]:
  "ctReceiveRoot (ctReceiveIndex_update f v) = ctReceiveRoot v" by (cases v) simp

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

lemma ctReceiveRoot_ctReceiveDepth_update [simp]:
  "ctReceiveRoot (ctReceiveDepth_update f v) = ctReceiveRoot v" by (cases v) simp

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

lemma ctReceiveIndex_ctReceiveRoot_update [simp]:
  "ctReceiveIndex (ctReceiveRoot_update f v) = ctReceiveIndex v" by (cases v) simp

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

lemma ctReceiveIndex_ctReceiveIndex_update [simp]:
  "ctReceiveIndex (ctReceiveIndex_update f v) = f (ctReceiveIndex v)" by (cases v) simp

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

lemma ctReceiveIndex_ctReceiveDepth_update [simp]:
  "ctReceiveIndex (ctReceiveDepth_update f v) = ctReceiveIndex v" by (cases v) simp

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

lemma ctReceiveDepth_ctReceiveRoot_update [simp]:
  "ctReceiveDepth (ctReceiveRoot_update f v) = ctReceiveDepth v" by (cases v) simp

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

lemma ctReceiveDepth_ctReceiveIndex_update [simp]:
  "ctReceiveDepth (ctReceiveIndex_update f v) = ctReceiveDepth v" by (cases v) simp

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

lemma ctReceiveDepth_ctReceiveDepth_update [simp]:
  "ctReceiveDepth (ctReceiveDepth_update f v) = f (ctReceiveDepth v)" by (cases v) simp

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

lemma bidrBasePAddr_bidrBasePAddr_update [simp]:
  "bidrBasePAddr (bidrBasePAddr_update f v) = f (bidrBasePAddr v)" by (cases v) simp

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

lemma bidrBasePAddr_bidrFrameSizeBits_update [simp]:
  "bidrBasePAddr (bidrFrameSizeBits_update f v) = bidrBasePAddr v" by (cases v) simp

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

lemma bidrBasePAddr_bidrFrameCaps_update [simp]:
  "bidrBasePAddr (bidrFrameCaps_update f v) = bidrBasePAddr v" by (cases v) simp

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

lemma bidrFrameSizeBits_bidrBasePAddr_update [simp]:
  "bidrFrameSizeBits (bidrBasePAddr_update f v) = bidrFrameSizeBits v" by (cases v) simp

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

lemma bidrFrameSizeBits_bidrFrameSizeBits_update [simp]:
  "bidrFrameSizeBits (bidrFrameSizeBits_update f v) = f (bidrFrameSizeBits v)" by (cases v) simp

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

lemma bidrFrameSizeBits_bidrFrameCaps_update [simp]:
  "bidrFrameSizeBits (bidrFrameCaps_update f v) = bidrFrameSizeBits v" by (cases v) simp

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

lemma bidrFrameCaps_bidrBasePAddr_update [simp]:
  "bidrFrameCaps (bidrBasePAddr_update f v) = bidrFrameCaps v" by (cases v) simp

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

lemma bidrFrameCaps_bidrFrameCaps_update [simp]:
  "bidrFrameCaps (bidrFrameCaps_update f v) = f (bidrFrameCaps v)" by (cases v) simp

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

lemma bifNodeID_bifNodeID_update [simp]:
  "bifNodeID (bifNodeID_update f v) = f (bifNodeID v)" by (cases v) simp

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

lemma bifNodeID_bifNumNodes_update [simp]:
  "bifNodeID (bifNumNodes_update f v) = bifNodeID v" by (cases v) simp

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

lemma bifNodeID_bifNumIOPTLevels_update [simp]:
  "bifNodeID (bifNumIOPTLevels_update f v) = bifNodeID v" by (cases v) simp

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

lemma bifNodeID_bifIPCBufVPtr_update [simp]:
  "bifNodeID (bifIPCBufVPtr_update f v) = bifNodeID v" by (cases v) simp

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

lemma bifNodeID_bifNullCaps_update [simp]:
  "bifNodeID (bifNullCaps_update f v) = bifNodeID v" by (cases v) simp

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

lemma bifNodeID_bifSharedFrameCaps_update [simp]:
  "bifNodeID (bifSharedFrameCaps_update f v) = bifNodeID v" by (cases v) simp

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

lemma bifNodeID_bifUIPDCaps_update [simp]:
  "bifNodeID (bifUIPDCaps_update f v) = bifNodeID v" by (cases v) simp

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

lemma bifNodeID_bifUIPTCaps_update [simp]:
  "bifNodeID (bifUIPTCaps_update f v) = bifNodeID v" by (cases v) simp

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

lemma bifNodeID_bifUntypedObjPAddrs_update [simp]:
  "bifNodeID (bifUntypedObjPAddrs_update f v) = bifNodeID v" by (cases v) simp

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

lemma bifNodeID_bifUntypedObjSizeBits_update [simp]:
  "bifNodeID (bifUntypedObjSizeBits_update f v) = bifNodeID v" by (cases v) simp

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

lemma bifNodeID_bifUntypedObjIsDeviceList_update [simp]:
  "bifNodeID (bifUntypedObjIsDeviceList_update f v) = bifNodeID v" by (cases v) simp

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

lemma bifNodeID_bifNumDeviceRegions_update [simp]:
  "bifNodeID (bifNumDeviceRegions_update f v) = bifNodeID v" by (cases v) simp

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

lemma bifNodeID_bifDeviceRegions_update [simp]:
  "bifNodeID (bifDeviceRegions_update f v) = bifNodeID v" by (cases v) simp

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

lemma bifNumNodes_bifNodeID_update [simp]:
  "bifNumNodes (bifNodeID_update f v) = bifNumNodes v" by (cases v) simp

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

lemma bifNumNodes_bifNumNodes_update [simp]:
  "bifNumNodes (bifNumNodes_update f v) = f (bifNumNodes v)" by (cases v) simp

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

lemma bifNumNodes_bifNumIOPTLevels_update [simp]:
  "bifNumNodes (bifNumIOPTLevels_update f v) = bifNumNodes v" by (cases v) simp

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

lemma bifNumNodes_bifIPCBufVPtr_update [simp]:
  "bifNumNodes (bifIPCBufVPtr_update f v) = bifNumNodes v" by (cases v) simp

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

lemma bifNumNodes_bifNullCaps_update [simp]:
  "bifNumNodes (bifNullCaps_update f v) = bifNumNodes v" by (cases v) simp

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

lemma bifNumNodes_bifSharedFrameCaps_update [simp]:
  "bifNumNodes (bifSharedFrameCaps_update f v) = bifNumNodes v" by (cases v) simp

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

lemma bifNumNodes_bifUIFrameCaps_update [simp]:
  "bifNumNodes (bifUIFrameCaps_update f v) = bifNumNodes v" by (cases v) simp

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

lemma bifNumNodes_bifUIPDCaps_update [simp]:
  "bifNumNodes (bifUIPDCaps_update f v) = bifNumNodes v" by (cases v) simp

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

lemma bifNumNodes_bifUIPTCaps_update [simp]:
  "bifNumNodes (bifUIPTCaps_update f v) = bifNumNodes v" by (cases v) simp

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

lemma bifNumNodes_bifUntypedObjCaps_update [simp]:
  "bifNumNodes (bifUntypedObjCaps_update f v) = bifNumNodes v" by (cases v) simp

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

lemma bifNumNodes_bifUntypedObjPAddrs_update [simp]:
  "bifNumNodes (bifUntypedObjPAddrs_update f v) = bifNumNodes v" by (cases v) simp

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