[STATEMENT]
lemma set_mode_types_preserved:
  assumes "w \<in> set_mode_locs element_ptr"
  assumes "h \<turnstile> w \<rightarrow>\<^sub>h h'"
  shows "type_wf h = type_wf h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. type_wf h = type_wf h'
[PROOF STEP]
apply(unfold type_wf_impl)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ShadowRootClass.type_wf h = ShadowRootClass.type_wf h'
[PROOF STEP]
using assms(1) type_wf_preserved[OF writes_singleton2 assms(2)]
[PROOF STATE]
proof (prove)
using this:
w \<in> set_mode_locs element_ptr
\<lbrakk>\<And>h h' wa. \<lbrakk>wa \<in> {w}; h \<turnstile> wa \<rightarrow>\<^sub>h h'\<rbrakk> \<Longrightarrow> \<forall>object_ptr. preserved (get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t object_ptr RObject.nothing) h h'; \<And>h h' wa. \<lbrakk>wa \<in> {w}; h \<turnstile> wa \<rightarrow>\<^sub>h h'\<rbrakk> \<Longrightarrow> \<forall>node_ptr. preserved (get_M\<^sub>N\<^sub>o\<^sub>d\<^sub>e node_ptr RNode.nothing) h h'; \<And>h h' wa. \<lbrakk>wa \<in> {w}; h \<turnstile> wa \<rightarrow>\<^sub>h h'\<rbrakk> \<Longrightarrow> \<forall>element_ptr. preserved (get_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t element_ptr RElement.nothing) h h'; \<And>h h' wa. \<lbrakk>wa \<in> {w}; h \<turnstile> wa \<rightarrow>\<^sub>h h'\<rbrakk> \<Longrightarrow> \<forall>character_data_ptr. preserved (get_M\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a character_data_ptr RCharacterData.nothing) h h'; \<And>h h' wa. \<lbrakk>wa \<in> {w}; h \<turnstile> wa \<rightarrow>\<^sub>h h'\<rbrakk> \<Longrightarrow> \<forall>document_ptr. preserved (get_M\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t document_ptr RDocument.nothing) h h'; \<And>h h' wa. \<lbrakk>wa \<in> {w}; h \<turnstile> wa \<rightarrow>\<^sub>h h'\<rbrakk> \<Longrightarrow> \<forall>shadow_root_ptr. preserved (get_M\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t shadow_root_ptr RShadowRoot.nothing) h h'\<rbrakk> \<Longrightarrow> ShadowRootClass.type_wf h = ShadowRootClass.type_wf h'

goal (1 subgoal):
 1. ShadowRootClass.type_wf h = ShadowRootClass.type_wf h'
[PROOF STEP]
by(auto simp add: all_args_def set_mode_locs_def split: if_splits)