theory SimplRewrite

lemma exec_statefn_simulates_While_lemma:
  assumes sim: "exec_statefn_simulates f C
        {s. f s \<in> S \<and> (f s \<in> com_initial_guards b \<or> f s \<notin> f ` (- T))} a b"
  assumes eq: "\<And>s. \<lbrakk> f s \<in> S; f s \<in> com_initial_guards b \<or> f s \<notin> f ` (- T) \<rbrakk>
    \<Longrightarrow> s \<in> C = (f s \<in> C')"
  assumes subs: "com_final_guards UNIV b \<subseteq> S"
  shows "\<lbrakk> \<Gamma> \<turnstile> \<langle>bdy, xs\<rangle> \<Rightarrow> t \<rbrakk>
            \<Longrightarrow> \<forall>s. bdy = While C a \<and> xs = Normal s \<and> f s \<in> S
                \<longrightarrow> (map_option (add_statefn (inv f)) o \<Gamma>)
                         \<turnstile> \<langle>While C' b, Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t
                   \<or> (\<exists>ft. (map_option (add_statefn (inv f)) o \<Gamma>)
                         \<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft)
                   \<or> (\<exists>t' \<in> - T. (map_option (add_statefn (inv f)) o \<Gamma>)
                         \<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'))" apply (induct rule: exec.induct, simp_all) apply clarsimp apply (rule ccontr) apply (frule exec_While_not_in_state_lemma, simp) apply (drule(1) eq[rotated]) apply (drule(1) exec_statefn_simulatesD[OF _ sim]) apply (simp add: o_def) apply (elim disjE exE) apply (case_tac s', simp_all) apply (blast intro: exec.WhileTrue
                 exec_in_final_guards[THEN subsetD[OF subs]])[1] apply (erule exec.cases, simp_all)[1] apply (blast intro: exec.WhileTrue)[1] apply (erule exec.cases, simp_all)[1] apply (blast intro: exec.WhileTrue) apply (erule exec.cases, simp_all)[1] apply (blast intro: exec.WhileTrue)[1] apply (case_tac s', simp_all) apply (blast intro: exec.WhileTrue) apply (erule exec.cases, simp_all)[1] apply (blast intro: exec.WhileTrue) apply (erule exec.cases, simp_all) apply (blast intro: exec.WhileTrue) apply (erule exec.cases, simp_all)[1] apply (blast intro: exec.WhileTrue) apply (clarsimp simp: Bex_def exec_in_final_guards[THEN subsetD[OF subs]]) apply (drule_tac \<Gamma>="map_option (add_statefn (inv f)) \<circ> \<Gamma>"
             in exec_not_in_initial_guards) apply (clarsimp simp: o_def) apply (blast intro: exec.WhileTrue exec.WhileFalse) apply clarsimp apply (rule ccontr, frule exec_While_not_in_state_lemma, simp) apply (cut_tac s=s in eq) apply (auto intro: exec.WhileFalse) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>bdy,xs\<rangle> \<Rightarrow> t \<Longrightarrow> \<forall>s. bdy = While C a \<and> xs = Normal s \<and> f s \<in> S \<longrightarrow> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t \<or> (\<exists>ft. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')) proof (prove)
goal (2 subgoals):
 1. \<And>s ba c s' t. \<lbrakk>s \<in> ba; \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> s'; c = While C a \<and> f s \<in> S \<longrightarrow> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f s' \<or> (\<exists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')); \<Gamma>\<turnstile> \<langle>While ba c,s'\<rangle> \<Rightarrow> t; \<forall>s. ba = C \<and> c = a \<and> s' = Normal s \<and> f s \<in> S \<longrightarrow> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t \<or> (\<exists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'))\<rbrakk> \<Longrightarrow> ba = C \<and> c = a \<and> f s \<in> S \<longrightarrow> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t \<or> (\<exists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'))
 2. \<And>s ba c. s \<notin> ba \<Longrightarrow> ba = C \<and> c = a \<and> f s \<in> S \<longrightarrow> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f s) \<or> (\<exists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')) proof (prove)
goal (2 subgoals):
 1. \<And>s s' t. \<lbrakk>s \<in> C; \<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>While C a,s'\<rangle> \<Rightarrow> t; \<forall>s. s' = Normal s \<and> f s \<in> S \<longrightarrow> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t \<or> (\<exists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')); f s \<in> S; \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t; \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')\<rbrakk> \<Longrightarrow> \<exists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft
 2. \<And>s ba c. s \<notin> ba \<Longrightarrow> ba = C \<and> c = a \<and> f s \<in> S \<longrightarrow> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f s) \<or> (\<exists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')) proof (prove)
goal (2 subgoals):
 1. \<And>s s' t. \<lbrakk>s \<in> C; \<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>While C a,s'\<rangle> \<Rightarrow> t; \<forall>s. s' = Normal s \<and> f s \<in> S \<longrightarrow> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t \<or> (\<exists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')); f s \<in> S; \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t; \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'); \<nexists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft\<rbrakk> \<Longrightarrow> False
 2. \<And>s ba c. s \<notin> ba \<Longrightarrow> ba = C \<and> c = a \<and> f s \<in> S \<longrightarrow> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f s) \<or> (\<exists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')) proof (prove)
goal (2 subgoals):
 1. \<And>s s' t. \<lbrakk>s \<in> C; \<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>While C a,s'\<rangle> \<Rightarrow> t; \<forall>s. s' = Normal s \<and> f s \<in> S \<longrightarrow> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t \<or> (\<exists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')); f s \<in> S; \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t; \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'); \<nexists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; f s \<in> com_initial_guards b \<or> f s \<notin> f ` (- T)\<rbrakk> \<Longrightarrow> False
 2. \<And>s ba c. s \<notin> ba \<Longrightarrow> ba = C \<and> c = a \<and> f s \<in> S \<longrightarrow> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f s) \<or> (\<exists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')) proof (prove)
goal (2 subgoals):
 1. \<And>s s' t. \<lbrakk>s \<in> C; \<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>While C a,s'\<rangle> \<Rightarrow> t; \<forall>s. s' = Normal s \<and> f s \<in> S \<longrightarrow> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t \<or> (\<exists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')); f s \<in> S; \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t; \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'); \<nexists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; (s \<in> C) = (f s \<in> C')\<rbrakk> \<Longrightarrow> False
 2. \<And>s ba c. s \<notin> ba \<Longrightarrow> ba = C \<and> c = a \<and> f s \<in> S \<longrightarrow> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f s) \<or> (\<exists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')) proof (prove)
goal (2 subgoals):
 1. \<And>s s' t. \<lbrakk>s \<in> C; \<Gamma>\<turnstile> \<langle>While C a,s'\<rangle> \<Rightarrow> t; \<forall>s. s' = Normal s \<and> f s \<in> S \<longrightarrow> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t \<or> (\<exists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')); f s \<in> S; \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t; \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'); \<nexists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; (s \<in> C) = (f s \<in> C'); (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f s' \<or> (\<exists>ft. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- {s. f s \<in> S \<and> (f s \<in> com_initial_guards b \<or> f s \<notin> f ` (- T))}. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'))\<rbrakk> \<Longrightarrow> False
 2. \<And>s ba c. s \<notin> ba \<Longrightarrow> ba = C \<and> c = a \<and> f s \<in> S \<longrightarrow> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f s) \<or> (\<exists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')) proof (prove)
goal (2 subgoals):
 1. \<And>s s' t. \<lbrakk>f s \<in> C'; \<Gamma>\<turnstile> \<langle>While C a,s'\<rangle> \<Rightarrow> t; \<forall>s. s' = Normal s \<and> f s \<in> S \<longrightarrow> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t \<or> (\<exists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')); f s \<in> S; \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t; \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'); \<forall>ft. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s \<in> C; (\<lambda>x. map_option (add_statefn (inv f)) (\<Gamma> x))\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f s' \<or> (\<exists>ft. (\<lambda>x. map_option (add_statefn (inv f)) (\<Gamma> x))\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- {s. f s \<in> S \<and> (f s \<in> com_initial_guards b \<or> f s \<notin> f ` (- T))}. (\<lambda>x. map_option (add_statefn (inv f)) (\<Gamma> x))\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'))\<rbrakk> \<Longrightarrow> False
 2. \<And>s ba c. s \<notin> ba \<Longrightarrow> ba = C \<and> c = a \<and> f s \<in> S \<longrightarrow> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f s) \<or> (\<exists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')) proof (prove)
goal (4 subgoals):
 1. \<And>s s' t. \<lbrakk>f s \<in> C'; \<Gamma>\<turnstile> \<langle>While C a,s'\<rangle> \<Rightarrow> t; \<forall>s. s' = Normal s \<and> f s \<in> S \<longrightarrow> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t \<or> (\<exists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')); f s \<in> S; \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t; \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'); \<forall>ft. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s \<in> C; (\<lambda>x. map_option (add_statefn (inv f)) (\<Gamma> x))\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f s'\<rbrakk> \<Longrightarrow> False
 2. \<And>s s' t ft. \<lbrakk>f s \<in> C'; \<Gamma>\<turnstile> \<langle>While C a,s'\<rangle> \<Rightarrow> t; \<forall>s. s' = Normal s \<and> f s \<in> S \<longrightarrow> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t \<or> (\<exists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')); f s \<in> S; \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t; \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'); \<forall>ft. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s \<in> C; (\<lambda>x. map_option (add_statefn (inv f)) (\<Gamma> x))\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Fault ft\<rbrakk> \<Longrightarrow> False
 3. \<And>s s' t. \<lbrakk>f s \<in> C'; \<Gamma>\<turnstile> \<langle>While C a,s'\<rangle> \<Rightarrow> t; \<forall>s. s' = Normal s \<and> f s \<in> S \<longrightarrow> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t \<or> (\<exists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')); f s \<in> S; \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t; \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'); \<forall>ft. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s \<in> C; \<exists>t'\<in>- {s. f s \<in> S \<and> (f s \<in> com_initial_guards b \<or> f s \<notin> f ` (- T))}. (\<lambda>x. map_option (add_statefn (inv f)) (\<Gamma> x))\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')\<rbrakk> \<Longrightarrow> False
 4. \<And>s ba c. s \<notin> ba \<Longrightarrow> ba = C \<and> c = a \<and> f s \<in> S \<longrightarrow> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f s) \<or> (\<exists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')) proof (prove)
goal (7 subgoals):
 1. \<And>s s' t x1. \<lbrakk>f s \<in> C'; \<Gamma>\<turnstile> \<langle>While C a,Normal x1\<rangle> \<Rightarrow> t; f x1 \<in> S \<longrightarrow> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f x1)\<rangle> \<Rightarrow> add_statefn_xstate f t \<or> (\<exists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f x1)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f x1)\<rangle> \<Rightarrow> Normal (f t')); f s \<in> S; \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t; \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'); \<forall>ft. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s \<in> C; (\<lambda>x. map_option (add_statefn (inv f)) (\<Gamma> x))\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Normal (f x1); s' = Normal x1\<rbrakk> \<Longrightarrow> False
 2. \<And>s s' t x2. \<lbrakk>f s \<in> C'; \<Gamma>\<turnstile> \<langle>While C a,Abrupt x2\<rangle> \<Rightarrow> t; f s \<in> S; \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t; \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'); \<forall>ft. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s \<in> C; (\<lambda>x. map_option (add_statefn (inv f)) (\<Gamma> x))\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Abrupt (f x2); s' = Abrupt x2\<rbrakk> \<Longrightarrow> False
 3. \<And>s s' t x3. \<lbrakk>f s \<in> C'; \<Gamma>\<turnstile> \<langle>While C a,Fault x3\<rangle> \<Rightarrow> t; f s \<in> S; \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t; \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'); \<forall>ft. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s \<in> C; (\<lambda>x. map_option (add_statefn (inv f)) (\<Gamma> x))\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Fault x3; s' = Fault x3\<rbrakk> \<Longrightarrow> False
 4. \<And>s s' t. \<lbrakk>f s \<in> C'; \<Gamma>\<turnstile> \<langle>While C a,Stuck\<rangle> \<Rightarrow> t; f s \<in> S; \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t; \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'); \<forall>ft. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s \<in> C; (\<lambda>x. map_option (add_statefn (inv f)) (\<Gamma> x))\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Stuck; s' = Stuck\<rbrakk> \<Longrightarrow> False
 5. \<And>s s' t ft. \<lbrakk>f s \<in> C'; \<Gamma>\<turnstile> \<langle>While C a,s'\<rangle> \<Rightarrow> t; \<forall>s. s' = Normal s \<and> f s \<in> S \<longrightarrow> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t \<or> (\<exists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')); f s \<in> S; \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t; \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'); \<forall>ft. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s \<in> C; (\<lambda>x. map_option (add_statefn (inv f)) (\<Gamma> x))\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Fault ft\<rbrakk> \<Longrightarrow> False
 6. \<And>s s' t. \<lbrakk>f s \<in> C'; \<Gamma>\<turnstile> \<langle>While C a,s'\<rangle> \<Rightarrow> t; \<forall>s. s' = Normal s \<and> f s \<in> S \<longrightarrow> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t \<or> (\<exists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')); f s \<in> S; \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t; \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'); \<forall>ft. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s \<in> C; \<exists>t'\<in>- {s. f s \<in> S \<and> (f s \<in> com_initial_guards b \<or> f s \<notin> f ` (- T))}. (\<lambda>x. map_option (add_statefn (inv f)) (\<Gamma> x))\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')\<rbrakk> \<Longrightarrow> False
 7. \<And>s ba c. s \<notin> ba \<Longrightarrow> ba = C \<and> c = a \<and> f s \<in> S \<longrightarrow> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f s) \<or> (\<exists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')) proof (prove)
goal (6 subgoals):
 1. \<And>s s' t x2. \<lbrakk>f s \<in> C'; \<Gamma>\<turnstile> \<langle>While C a,Abrupt x2\<rangle> \<Rightarrow> t; f s \<in> S; \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t; \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'); \<forall>ft. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s \<in> C; (\<lambda>x. map_option (add_statefn (inv f)) (\<Gamma> x))\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Abrupt (f x2); s' = Abrupt x2\<rbrakk> \<Longrightarrow> False
 2. \<And>s s' t x3. \<lbrakk>f s \<in> C'; \<Gamma>\<turnstile> \<langle>While C a,Fault x3\<rangle> \<Rightarrow> t; f s \<in> S; \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t; \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'); \<forall>ft. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s \<in> C; (\<lambda>x. map_option (add_statefn (inv f)) (\<Gamma> x))\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Fault x3; s' = Fault x3\<rbrakk> \<Longrightarrow> False
 3. \<And>s s' t. \<lbrakk>f s \<in> C'; \<Gamma>\<turnstile> \<langle>While C a,Stuck\<rangle> \<Rightarrow> t; f s \<in> S; \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t; \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'); \<forall>ft. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s \<in> C; (\<lambda>x. map_option (add_statefn (inv f)) (\<Gamma> x))\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Stuck; s' = Stuck\<rbrakk> \<Longrightarrow> False
 4. \<And>s s' t ft. \<lbrakk>f s \<in> C'; \<Gamma>\<turnstile> \<langle>While C a,s'\<rangle> \<Rightarrow> t; \<forall>s. s' = Normal s \<and> f s \<in> S \<longrightarrow> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t \<or> (\<exists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')); f s \<in> S; \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t; \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'); \<forall>ft. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s \<in> C; (\<lambda>x. map_option (add_statefn (inv f)) (\<Gamma> x))\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Fault ft\<rbrakk> \<Longrightarrow> False
 5. \<And>s s' t. \<lbrakk>f s \<in> C'; \<Gamma>\<turnstile> \<langle>While C a,s'\<rangle> \<Rightarrow> t; \<forall>s. s' = Normal s \<and> f s \<in> S \<longrightarrow> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t \<or> (\<exists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')); f s \<in> S; \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t; \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'); \<forall>ft. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s \<in> C; \<exists>t'\<in>- {s. f s \<in> S \<and> (f s \<in> com_initial_guards b \<or> f s \<notin> f ` (- T))}. (\<lambda>x. map_option (add_statefn (inv f)) (\<Gamma> x))\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')\<rbrakk> \<Longrightarrow> False
 6. \<And>s ba c. s \<notin> ba \<Longrightarrow> ba = C \<and> c = a \<and> f s \<in> S \<longrightarrow> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f s) \<or> (\<exists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')) proof (prove)
goal (6 subgoals):
 1. \<And>s s' t x2 c sa. \<lbrakk>f s \<in> C'; f s \<in> S; \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Abrupt (f sa); \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'); \<forall>ft. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s \<in> C; (\<lambda>x. map_option (add_statefn (inv f)) (\<Gamma> x))\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Abrupt (f sa); s' = Abrupt sa; While C a = c; x2 = sa; t = Abrupt sa\<rbrakk> \<Longrightarrow> False
 2. \<And>s s' t x3. \<lbrakk>f s \<in> C'; \<Gamma>\<turnstile> \<langle>While C a,Fault x3\<rangle> \<Rightarrow> t; f s \<in> S; \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t; \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'); \<forall>ft. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s \<in> C; (\<lambda>x. map_option (add_statefn (inv f)) (\<Gamma> x))\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Fault x3; s' = Fault x3\<rbrakk> \<Longrightarrow> False
 3. \<And>s s' t. \<lbrakk>f s \<in> C'; \<Gamma>\<turnstile> \<langle>While C a,Stuck\<rangle> \<Rightarrow> t; f s \<in> S; \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t; \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'); \<forall>ft. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s \<in> C; (\<lambda>x. map_option (add_statefn (inv f)) (\<Gamma> x))\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Stuck; s' = Stuck\<rbrakk> \<Longrightarrow> False
 4. \<And>s s' t ft. \<lbrakk>f s \<in> C'; \<Gamma>\<turnstile> \<langle>While C a,s'\<rangle> \<Rightarrow> t; \<forall>s. s' = Normal s \<and> f s \<in> S \<longrightarrow> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t \<or> (\<exists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')); f s \<in> S; \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t; \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'); \<forall>ft. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s \<in> C; (\<lambda>x. map_option (add_statefn (inv f)) (\<Gamma> x))\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Fault ft\<rbrakk> \<Longrightarrow> False
 5. \<And>s s' t. \<lbrakk>f s \<in> C'; \<Gamma>\<turnstile> \<langle>While C a,s'\<rangle> \<Rightarrow> t; \<forall>s. s' = Normal s \<and> f s \<in> S \<longrightarrow> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t \<or> (\<exists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')); f s \<in> S; \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t; \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'); \<forall>ft. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s \<in> C; \<exists>t'\<in>- {s. f s \<in> S \<and> (f s \<in> com_initial_guards b \<or> f s \<notin> f ` (- T))}. (\<lambda>x. map_option (add_statefn (inv f)) (\<Gamma> x))\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')\<rbrakk> \<Longrightarrow> False
 6. \<And>s ba c. s \<notin> ba \<Longrightarrow> ba = C \<and> c = a \<and> f s \<in> S \<longrightarrow> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f s) \<or> (\<exists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')) proof (prove)
goal (5 subgoals):
 1. \<And>s s' t x3. \<lbrakk>f s \<in> C'; \<Gamma>\<turnstile> \<langle>While C a,Fault x3\<rangle> \<Rightarrow> t; f s \<in> S; \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t; \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'); \<forall>ft. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s \<in> C; (\<lambda>x. map_option (add_statefn (inv f)) (\<Gamma> x))\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Fault x3; s' = Fault x3\<rbrakk> \<Longrightarrow> False
 2. \<And>s s' t. \<lbrakk>f s \<in> C'; \<Gamma>\<turnstile> \<langle>While C a,Stuck\<rangle> \<Rightarrow> t; f s \<in> S; \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t; \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'); \<forall>ft. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s \<in> C; (\<lambda>x. map_option (add_statefn (inv f)) (\<Gamma> x))\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Stuck; s' = Stuck\<rbrakk> \<Longrightarrow> False
 3. \<And>s s' t ft. \<lbrakk>f s \<in> C'; \<Gamma>\<turnstile> \<langle>While C a,s'\<rangle> \<Rightarrow> t; \<forall>s. s' = Normal s \<and> f s \<in> S \<longrightarrow> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t \<or> (\<exists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')); f s \<in> S; \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t; \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'); \<forall>ft. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s \<in> C; (\<lambda>x. map_option (add_statefn (inv f)) (\<Gamma> x))\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Fault ft\<rbrakk> \<Longrightarrow> False
 4. \<And>s s' t. \<lbrakk>f s \<in> C'; \<Gamma>\<turnstile> \<langle>While C a,s'\<rangle> \<Rightarrow> t; \<forall>s. s' = Normal s \<and> f s \<in> S \<longrightarrow> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t \<or> (\<exists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')); f s \<in> S; \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t; \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'); \<forall>ft. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s \<in> C; \<exists>t'\<in>- {s. f s \<in> S \<and> (f s \<in> com_initial_guards b \<or> f s \<notin> f ` (- T))}. (\<lambda>x. map_option (add_statefn (inv f)) (\<Gamma> x))\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')\<rbrakk> \<Longrightarrow> False
 5. \<And>s ba c. s \<notin> ba \<Longrightarrow> ba = C \<and> c = a \<and> f s \<in> S \<longrightarrow> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f s) \<or> (\<exists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')) proof (prove)
goal (5 subgoals):
 1. \<And>s s' t x3 c fa. \<lbrakk>f s \<in> C'; f s \<in> S; \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'); \<forall>ft. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s \<in> C; (\<lambda>x. map_option (add_statefn (inv f)) (\<Gamma> x))\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Fault fa; s' = Fault fa; While C a = c; x3 = fa; t = Fault fa\<rbrakk> \<Longrightarrow> False
 2. \<And>s s' t. \<lbrakk>f s \<in> C'; \<Gamma>\<turnstile> \<langle>While C a,Stuck\<rangle> \<Rightarrow> t; f s \<in> S; \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t; \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'); \<forall>ft. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s \<in> C; (\<lambda>x. map_option (add_statefn (inv f)) (\<Gamma> x))\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Stuck; s' = Stuck\<rbrakk> \<Longrightarrow> False
 3. \<And>s s' t ft. \<lbrakk>f s \<in> C'; \<Gamma>\<turnstile> \<langle>While C a,s'\<rangle> \<Rightarrow> t; \<forall>s. s' = Normal s \<and> f s \<in> S \<longrightarrow> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t \<or> (\<exists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')); f s \<in> S; \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t; \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'); \<forall>ft. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s \<in> C; (\<lambda>x. map_option (add_statefn (inv f)) (\<Gamma> x))\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Fault ft\<rbrakk> \<Longrightarrow> False
 4. \<And>s s' t. \<lbrakk>f s \<in> C'; \<Gamma>\<turnstile> \<langle>While C a,s'\<rangle> \<Rightarrow> t; \<forall>s. s' = Normal s \<and> f s \<in> S \<longrightarrow> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t \<or> (\<exists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')); f s \<in> S; \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t; \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'); \<forall>ft. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s \<in> C; \<exists>t'\<in>- {s. f s \<in> S \<and> (f s \<in> com_initial_guards b \<or> f s \<notin> f ` (- T))}. (\<lambda>x. map_option (add_statefn (inv f)) (\<Gamma> x))\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')\<rbrakk> \<Longrightarrow> False
 5. \<And>s ba c. s \<notin> ba \<Longrightarrow> ba = C \<and> c = a \<and> f s \<in> S \<longrightarrow> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f s) \<or> (\<exists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')) proof (prove)
goal (4 subgoals):
 1. \<And>s s' t. \<lbrakk>f s \<in> C'; \<Gamma>\<turnstile> \<langle>While C a,Stuck\<rangle> \<Rightarrow> t; f s \<in> S; \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t; \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'); \<forall>ft. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s \<in> C; (\<lambda>x. map_option (add_statefn (inv f)) (\<Gamma> x))\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Stuck; s' = Stuck\<rbrakk> \<Longrightarrow> False
 2. \<And>s s' t ft. \<lbrakk>f s \<in> C'; \<Gamma>\<turnstile> \<langle>While C a,s'\<rangle> \<Rightarrow> t; \<forall>s. s' = Normal s \<and> f s \<in> S \<longrightarrow> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t \<or> (\<exists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')); f s \<in> S; \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t; \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'); \<forall>ft. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s \<in> C; (\<lambda>x. map_option (add_statefn (inv f)) (\<Gamma> x))\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Fault ft\<rbrakk> \<Longrightarrow> False
 3. \<And>s s' t. \<lbrakk>f s \<in> C'; \<Gamma>\<turnstile> \<langle>While C a,s'\<rangle> \<Rightarrow> t; \<forall>s. s' = Normal s \<and> f s \<in> S \<longrightarrow> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t \<or> (\<exists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')); f s \<in> S; \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t; \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'); \<forall>ft. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s \<in> C; \<exists>t'\<in>- {s. f s \<in> S \<and> (f s \<in> com_initial_guards b \<or> f s \<notin> f ` (- T))}. (\<lambda>x. map_option (add_statefn (inv f)) (\<Gamma> x))\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')\<rbrakk> \<Longrightarrow> False
 4. \<And>s ba c. s \<notin> ba \<Longrightarrow> ba = C \<and> c = a \<and> f s \<in> S \<longrightarrow> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f s) \<or> (\<exists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')) proof (prove)
goal (4 subgoals):
 1. \<And>s s' t c. \<lbrakk>f s \<in> C'; f s \<in> S; \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Stuck; \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'); \<forall>ft. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s \<in> C; (\<lambda>x. map_option (add_statefn (inv f)) (\<Gamma> x))\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Stuck; s' = Stuck; While C a = c; t = Stuck\<rbrakk> \<Longrightarrow> False
 2. \<And>s s' t ft. \<lbrakk>f s \<in> C'; \<Gamma>\<turnstile> \<langle>While C a,s'\<rangle> \<Rightarrow> t; \<forall>s. s' = Normal s \<and> f s \<in> S \<longrightarrow> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t \<or> (\<exists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')); f s \<in> S; \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t; \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'); \<forall>ft. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s \<in> C; (\<lambda>x. map_option (add_statefn (inv f)) (\<Gamma> x))\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Fault ft\<rbrakk> \<Longrightarrow> False
 3. \<And>s s' t. \<lbrakk>f s \<in> C'; \<Gamma>\<turnstile> \<langle>While C a,s'\<rangle> \<Rightarrow> t; \<forall>s. s' = Normal s \<and> f s \<in> S \<longrightarrow> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t \<or> (\<exists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')); f s \<in> S; \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t; \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'); \<forall>ft. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s \<in> C; \<exists>t'\<in>- {s. f s \<in> S \<and> (f s \<in> com_initial_guards b \<or> f s \<notin> f ` (- T))}. (\<lambda>x. map_option (add_statefn (inv f)) (\<Gamma> x))\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')\<rbrakk> \<Longrightarrow> False
 4. \<And>s ba c. s \<notin> ba \<Longrightarrow> ba = C \<and> c = a \<and> f s \<in> S \<longrightarrow> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f s) \<or> (\<exists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')) proof (prove)
goal (3 subgoals):
 1. \<And>s s' t ft. \<lbrakk>f s \<in> C'; \<Gamma>\<turnstile> \<langle>While C a,s'\<rangle> \<Rightarrow> t; \<forall>s. s' = Normal s \<and> f s \<in> S \<longrightarrow> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t \<or> (\<exists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')); f s \<in> S; \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t; \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'); \<forall>ft. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s \<in> C; (\<lambda>x. map_option (add_statefn (inv f)) (\<Gamma> x))\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Fault ft\<rbrakk> \<Longrightarrow> False
 2. \<And>s s' t. \<lbrakk>f s \<in> C'; \<Gamma>\<turnstile> \<langle>While C a,s'\<rangle> \<Rightarrow> t; \<forall>s. s' = Normal s \<and> f s \<in> S \<longrightarrow> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t \<or> (\<exists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')); f s \<in> S; \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t; \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'); \<forall>ft. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s \<in> C; \<exists>t'\<in>- {s. f s \<in> S \<and> (f s \<in> com_initial_guards b \<or> f s \<notin> f ` (- T))}. (\<lambda>x. map_option (add_statefn (inv f)) (\<Gamma> x))\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')\<rbrakk> \<Longrightarrow> False
 3. \<And>s ba c. s \<notin> ba \<Longrightarrow> ba = C \<and> c = a \<and> f s \<in> S \<longrightarrow> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f s) \<or> (\<exists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')) proof (prove)
goal (6 subgoals):
 1. \<And>s s' t ft x1. \<lbrakk>f s \<in> C'; \<Gamma>\<turnstile> \<langle>While C a,Normal x1\<rangle> \<Rightarrow> t; f x1 \<in> S \<longrightarrow> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f x1)\<rangle> \<Rightarrow> add_statefn_xstate f t \<or> (\<exists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f x1)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f x1)\<rangle> \<Rightarrow> Normal (f t')); f s \<in> S; \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t; \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'); \<forall>ft. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s \<in> C; (\<lambda>x. map_option (add_statefn (inv f)) (\<Gamma> x))\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s' = Normal x1\<rbrakk> \<Longrightarrow> False
 2. \<And>s s' t ft x2. \<lbrakk>f s \<in> C'; \<Gamma>\<turnstile> \<langle>While C a,Abrupt x2\<rangle> \<Rightarrow> t; f s \<in> S; \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t; \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'); \<forall>ft. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s \<in> C; (\<lambda>x. map_option (add_statefn (inv f)) (\<Gamma> x))\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s' = Abrupt x2\<rbrakk> \<Longrightarrow> False
 3. \<And>s s' t ft x3. \<lbrakk>f s \<in> C'; \<Gamma>\<turnstile> \<langle>While C a,Fault x3\<rangle> \<Rightarrow> t; f s \<in> S; \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t; \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'); \<forall>ft. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s \<in> C; (\<lambda>x. map_option (add_statefn (inv f)) (\<Gamma> x))\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s' = Fault x3\<rbrakk> \<Longrightarrow> False
 4. \<And>s s' t ft. \<lbrakk>f s \<in> C'; \<Gamma>\<turnstile> \<langle>While C a,Stuck\<rangle> \<Rightarrow> t; f s \<in> S; \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t; \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'); \<forall>ft. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s \<in> C; (\<lambda>x. map_option (add_statefn (inv f)) (\<Gamma> x))\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s' = Stuck\<rbrakk> \<Longrightarrow> False
 5. \<And>s s' t. \<lbrakk>f s \<in> C'; \<Gamma>\<turnstile> \<langle>While C a,s'\<rangle> \<Rightarrow> t; \<forall>s. s' = Normal s \<and> f s \<in> S \<longrightarrow> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t \<or> (\<exists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')); f s \<in> S; \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t; \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'); \<forall>ft. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s \<in> C; \<exists>t'\<in>- {s. f s \<in> S \<and> (f s \<in> com_initial_guards b \<or> f s \<notin> f ` (- T))}. (\<lambda>x. map_option (add_statefn (inv f)) (\<Gamma> x))\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')\<rbrakk> \<Longrightarrow> False
 6. \<And>s ba c. s \<notin> ba \<Longrightarrow> ba = C \<and> c = a \<and> f s \<in> S \<longrightarrow> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f s) \<or> (\<exists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')) proof (prove)
goal (5 subgoals):
 1. \<And>s s' t ft x2. \<lbrakk>f s \<in> C'; \<Gamma>\<turnstile> \<langle>While C a,Abrupt x2\<rangle> \<Rightarrow> t; f s \<in> S; \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t; \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'); \<forall>ft. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s \<in> C; (\<lambda>x. map_option (add_statefn (inv f)) (\<Gamma> x))\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s' = Abrupt x2\<rbrakk> \<Longrightarrow> False
 2. \<And>s s' t ft x3. \<lbrakk>f s \<in> C'; \<Gamma>\<turnstile> \<langle>While C a,Fault x3\<rangle> \<Rightarrow> t; f s \<in> S; \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t; \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'); \<forall>ft. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s \<in> C; (\<lambda>x. map_option (add_statefn (inv f)) (\<Gamma> x))\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s' = Fault x3\<rbrakk> \<Longrightarrow> False
 3. \<And>s s' t ft. \<lbrakk>f s \<in> C'; \<Gamma>\<turnstile> \<langle>While C a,Stuck\<rangle> \<Rightarrow> t; f s \<in> S; \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t; \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'); \<forall>ft. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s \<in> C; (\<lambda>x. map_option (add_statefn (inv f)) (\<Gamma> x))\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s' = Stuck\<rbrakk> \<Longrightarrow> False
 4. \<And>s s' t. \<lbrakk>f s \<in> C'; \<Gamma>\<turnstile> \<langle>While C a,s'\<rangle> \<Rightarrow> t; \<forall>s. s' = Normal s \<and> f s \<in> S \<longrightarrow> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t \<or> (\<exists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')); f s \<in> S; \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t; \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'); \<forall>ft. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s \<in> C; \<exists>t'\<in>- {s. f s \<in> S \<and> (f s \<in> com_initial_guards b \<or> f s \<notin> f ` (- T))}. (\<lambda>x. map_option (add_statefn (inv f)) (\<Gamma> x))\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')\<rbrakk> \<Longrightarrow> False
 5. \<And>s ba c. s \<notin> ba \<Longrightarrow> ba = C \<and> c = a \<and> f s \<in> S \<longrightarrow> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f s) \<or> (\<exists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')) proof (prove)
goal (5 subgoals):
 1. \<And>s s' t ft x2 c sa. \<lbrakk>f s \<in> C'; f s \<in> S; \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Abrupt (f sa); \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'); \<forall>ft. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s \<in> C; (\<lambda>x. map_option (add_statefn (inv f)) (\<Gamma> x))\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s' = Abrupt sa; While C a = c; x2 = sa; t = Abrupt sa\<rbrakk> \<Longrightarrow> False
 2. \<And>s s' t ft x3. \<lbrakk>f s \<in> C'; \<Gamma>\<turnstile> \<langle>While C a,Fault x3\<rangle> \<Rightarrow> t; f s \<in> S; \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t; \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'); \<forall>ft. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s \<in> C; (\<lambda>x. map_option (add_statefn (inv f)) (\<Gamma> x))\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s' = Fault x3\<rbrakk> \<Longrightarrow> False
 3. \<And>s s' t ft. \<lbrakk>f s \<in> C'; \<Gamma>\<turnstile> \<langle>While C a,Stuck\<rangle> \<Rightarrow> t; f s \<in> S; \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t; \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'); \<forall>ft. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s \<in> C; (\<lambda>x. map_option (add_statefn (inv f)) (\<Gamma> x))\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s' = Stuck\<rbrakk> \<Longrightarrow> False
 4. \<And>s s' t. \<lbrakk>f s \<in> C'; \<Gamma>\<turnstile> \<langle>While C a,s'\<rangle> \<Rightarrow> t; \<forall>s. s' = Normal s \<and> f s \<in> S \<longrightarrow> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t \<or> (\<exists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')); f s \<in> S; \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t; \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'); \<forall>ft. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s \<in> C; \<exists>t'\<in>- {s. f s \<in> S \<and> (f s \<in> com_initial_guards b \<or> f s \<notin> f ` (- T))}. (\<lambda>x. map_option (add_statefn (inv f)) (\<Gamma> x))\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')\<rbrakk> \<Longrightarrow> False
 5. \<And>s ba c. s \<notin> ba \<Longrightarrow> ba = C \<and> c = a \<and> f s \<in> S \<longrightarrow> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f s) \<or> (\<exists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')) proof (prove)
goal (4 subgoals):
 1. \<And>s s' t ft x3. \<lbrakk>f s \<in> C'; \<Gamma>\<turnstile> \<langle>While C a,Fault x3\<rangle> \<Rightarrow> t; f s \<in> S; \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t; \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'); \<forall>ft. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s \<in> C; (\<lambda>x. map_option (add_statefn (inv f)) (\<Gamma> x))\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s' = Fault x3\<rbrakk> \<Longrightarrow> False
 2. \<And>s s' t ft. \<lbrakk>f s \<in> C'; \<Gamma>\<turnstile> \<langle>While C a,Stuck\<rangle> \<Rightarrow> t; f s \<in> S; \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t; \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'); \<forall>ft. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s \<in> C; (\<lambda>x. map_option (add_statefn (inv f)) (\<Gamma> x))\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s' = Stuck\<rbrakk> \<Longrightarrow> False
 3. \<And>s s' t. \<lbrakk>f s \<in> C'; \<Gamma>\<turnstile> \<langle>While C a,s'\<rangle> \<Rightarrow> t; \<forall>s. s' = Normal s \<and> f s \<in> S \<longrightarrow> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t \<or> (\<exists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')); f s \<in> S; \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t; \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'); \<forall>ft. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s \<in> C; \<exists>t'\<in>- {s. f s \<in> S \<and> (f s \<in> com_initial_guards b \<or> f s \<notin> f ` (- T))}. (\<lambda>x. map_option (add_statefn (inv f)) (\<Gamma> x))\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')\<rbrakk> \<Longrightarrow> False
 4. \<And>s ba c. s \<notin> ba \<Longrightarrow> ba = C \<and> c = a \<and> f s \<in> S \<longrightarrow> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f s) \<or> (\<exists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')) proof (prove)
goal (4 subgoals):
 1. \<And>s s' t ft x3 c fa. \<lbrakk>f s \<in> C'; f s \<in> S; \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'); \<forall>ft. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s \<in> C; (\<lambda>x. map_option (add_statefn (inv f)) (\<Gamma> x))\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s' = Fault fa; While C a = c; x3 = fa; t = Fault fa\<rbrakk> \<Longrightarrow> False
 2. \<And>s s' t ft. \<lbrakk>f s \<in> C'; \<Gamma>\<turnstile> \<langle>While C a,Stuck\<rangle> \<Rightarrow> t; f s \<in> S; \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t; \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'); \<forall>ft. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s \<in> C; (\<lambda>x. map_option (add_statefn (inv f)) (\<Gamma> x))\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s' = Stuck\<rbrakk> \<Longrightarrow> False
 3. \<And>s s' t. \<lbrakk>f s \<in> C'; \<Gamma>\<turnstile> \<langle>While C a,s'\<rangle> \<Rightarrow> t; \<forall>s. s' = Normal s \<and> f s \<in> S \<longrightarrow> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t \<or> (\<exists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')); f s \<in> S; \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t; \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'); \<forall>ft. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s \<in> C; \<exists>t'\<in>- {s. f s \<in> S \<and> (f s \<in> com_initial_guards b \<or> f s \<notin> f ` (- T))}. (\<lambda>x. map_option (add_statefn (inv f)) (\<Gamma> x))\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')\<rbrakk> \<Longrightarrow> False
 4. \<And>s ba c. s \<notin> ba \<Longrightarrow> ba = C \<and> c = a \<and> f s \<in> S \<longrightarrow> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f s) \<or> (\<exists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')) proof (prove)
goal (3 subgoals):
 1. \<And>s s' t ft. \<lbrakk>f s \<in> C'; \<Gamma>\<turnstile> \<langle>While C a,Stuck\<rangle> \<Rightarrow> t; f s \<in> S; \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t; \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'); \<forall>ft. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s \<in> C; (\<lambda>x. map_option (add_statefn (inv f)) (\<Gamma> x))\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s' = Stuck\<rbrakk> \<Longrightarrow> False
 2. \<And>s s' t. \<lbrakk>f s \<in> C'; \<Gamma>\<turnstile> \<langle>While C a,s'\<rangle> \<Rightarrow> t; \<forall>s. s' = Normal s \<and> f s \<in> S \<longrightarrow> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t \<or> (\<exists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')); f s \<in> S; \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t; \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'); \<forall>ft. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s \<in> C; \<exists>t'\<in>- {s. f s \<in> S \<and> (f s \<in> com_initial_guards b \<or> f s \<notin> f ` (- T))}. (\<lambda>x. map_option (add_statefn (inv f)) (\<Gamma> x))\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')\<rbrakk> \<Longrightarrow> False
 3. \<And>s ba c. s \<notin> ba \<Longrightarrow> ba = C \<and> c = a \<and> f s \<in> S \<longrightarrow> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f s) \<or> (\<exists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')) proof (prove)
goal (3 subgoals):
 1. \<And>s s' t ft c. \<lbrakk>f s \<in> C'; f s \<in> S; \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Stuck; \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'); \<forall>ft. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s \<in> C; (\<lambda>x. map_option (add_statefn (inv f)) (\<Gamma> x))\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s' = Stuck; While C a = c; t = Stuck\<rbrakk> \<Longrightarrow> False
 2. \<And>s s' t. \<lbrakk>f s \<in> C'; \<Gamma>\<turnstile> \<langle>While C a,s'\<rangle> \<Rightarrow> t; \<forall>s. s' = Normal s \<and> f s \<in> S \<longrightarrow> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t \<or> (\<exists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')); f s \<in> S; \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t; \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'); \<forall>ft. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s \<in> C; \<exists>t'\<in>- {s. f s \<in> S \<and> (f s \<in> com_initial_guards b \<or> f s \<notin> f ` (- T))}. (\<lambda>x. map_option (add_statefn (inv f)) (\<Gamma> x))\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')\<rbrakk> \<Longrightarrow> False
 3. \<And>s ba c. s \<notin> ba \<Longrightarrow> ba = C \<and> c = a \<and> f s \<in> S \<longrightarrow> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f s) \<or> (\<exists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')) proof (prove)
goal (2 subgoals):
 1. \<And>s s' t. \<lbrakk>f s \<in> C'; \<Gamma>\<turnstile> \<langle>While C a,s'\<rangle> \<Rightarrow> t; \<forall>s. s' = Normal s \<and> f s \<in> S \<longrightarrow> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t \<or> (\<exists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')); f s \<in> S; \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t; \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'); \<forall>ft. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s \<in> C; \<exists>t'\<in>- {s. f s \<in> S \<and> (f s \<in> com_initial_guards b \<or> f s \<notin> f ` (- T))}. (\<lambda>x. map_option (add_statefn (inv f)) (\<Gamma> x))\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')\<rbrakk> \<Longrightarrow> False
 2. \<And>s ba c. s \<notin> ba \<Longrightarrow> ba = C \<and> c = a \<and> f s \<in> S \<longrightarrow> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f s) \<or> (\<exists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')) proof (prove)
goal (2 subgoals):
 1. \<And>s s' t x xa. \<lbrakk>f s \<in> C'; \<Gamma>\<turnstile> \<langle>While C a,s'\<rangle> \<Rightarrow> t; \<forall>s. s' = Normal s \<and> f s \<in> S \<longrightarrow> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t \<or> (\<exists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>x. x \<notin> T \<and> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f x)); f s \<in> S; \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t; \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'); \<forall>ft. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s \<in> C; (\<lambda>x. map_option (add_statefn (inv f)) (\<Gamma> x))\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Normal (f xa); f xa \<notin> com_initial_guards b; f x = f xa; xa \<notin> T\<rbrakk> \<Longrightarrow> False
 2. \<And>s ba c. s \<notin> ba \<Longrightarrow> ba = C \<and> c = a \<and> f s \<in> S \<longrightarrow> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f s) \<or> (\<exists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')) proof (prove)
goal (2 subgoals):
 1. \<And>s s' t x xa. \<lbrakk>f s \<in> C'; \<Gamma>\<turnstile> \<langle>While C a,s'\<rangle> \<Rightarrow> t; \<forall>s. s' = Normal s \<and> f s \<in> S \<longrightarrow> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t \<or> (\<exists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>x. x \<notin> T \<and> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f x)); f s \<in> S; \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t; \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'); \<forall>ft. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s \<in> C; (\<lambda>x. map_option (add_statefn (inv f)) (\<Gamma> x))\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Normal (f xa); f x = f xa; xa \<notin> T; \<exists>ft. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b,Normal (f xa)\<rangle> \<Rightarrow> Fault ft\<rbrakk> \<Longrightarrow> False
 2. \<And>s ba c. s \<notin> ba \<Longrightarrow> ba = C \<and> c = a \<and> f s \<in> S \<longrightarrow> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f s) \<or> (\<exists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')) proof (prove)
goal (2 subgoals):
 1. \<And>s s' t x xa ft. \<lbrakk>f s \<in> C'; \<Gamma>\<turnstile> \<langle>While C a,s'\<rangle> \<Rightarrow> t; \<forall>s. s' = Normal s \<and> f s \<in> S \<longrightarrow> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t \<or> (\<exists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>x. x \<notin> T \<and> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f x)); f s \<in> S; \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t; \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'); \<forall>ft. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; s \<in> C; (\<lambda>x. map_option (add_statefn (inv f)) (\<Gamma> x))\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Normal (f xa); f x = f xa; xa \<notin> T; (\<lambda>x. map_option (add_statefn (inv f)) (\<Gamma> x))\<turnstile> \<langle>b,Normal (f xa)\<rangle> \<Rightarrow> Fault ft\<rbrakk> \<Longrightarrow> False
 2. \<And>s ba c. s \<notin> ba \<Longrightarrow> ba = C \<and> c = a \<and> f s \<in> S \<longrightarrow> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f s) \<or> (\<exists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')) proof (prove)
goal (1 subgoal):
 1. \<And>s ba c. s \<notin> ba \<Longrightarrow> ba = C \<and> c = a \<and> f s \<in> S \<longrightarrow> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f s) \<or> (\<exists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>s \<notin> C; f s \<in> S; \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f s); \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')\<rbrakk> \<Longrightarrow> \<exists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>s \<notin> C; f s \<in> S; \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f s); \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'); \<nexists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; f s \<in> com_initial_guards b \<or> f s \<notin> f ` (- T)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>s \<notin> C; f s \<in> S; \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f s); \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'); \<nexists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; f s \<in> com_initial_guards b \<or> f s \<notin> f ` (- T)\<rbrakk> \<Longrightarrow> f s \<in> S
 2. \<And>s. \<lbrakk>s \<notin> C; f s \<in> S; \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f s); \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'); \<nexists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; f s \<in> com_initial_guards b \<or> f s \<notin> f ` (- T)\<rbrakk> \<Longrightarrow> f s \<in> com_initial_guards b \<or> f s \<notin> f ` (- T)
 3. \<And>s. \<lbrakk>s \<notin> C; f s \<in> S; \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f s); \<forall>t'\<in>- T. \<not> (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'); \<nexists>ft. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft; f s \<in> com_initial_guards b \<or> f s \<notin> f ` (- T); (s \<in> C) = (f s \<in> C')\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!