theory SimplRewrite

lemma exec_statefn_simulates_Seq:
  "\<lbrakk> exec_statefn_simulates f S {s. f s \<in> com_initial_guards d} a b;
       exec_statefn_simulates f UNIV T c d \<rbrakk>
        \<Longrightarrow> exec_statefn_simulates f S T (a ;; c) (b ;; d)" apply (rule exec_statefn_simulatesI) apply (erule exec.cases, simp_all) apply clarsimp apply (drule(2) exec_statefn_simulatesD) apply (elim disjE exE) apply (case_tac s', simp_all)[1] apply (drule(1) exec_statefn_simulatesD, simp) apply (auto intro: exec.Seq)[1] apply ((force elim: exec.Seq exec.cases notE)+)[4] apply clarsimp apply (rule ccontr, frule_tac \<Gamma>="map_option (add_statefn (inv f)) \<circ> \<Gamma>"
            in exec_not_in_initial_guards, clarsimp) apply (blast intro: exec.Seq) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>exec_statefn_simulates f S {s. f s \<in> com_initial_guards d} a b; exec_statefn_simulates f UNIV T c d\<rbrakk> \<Longrightarrow> exec_statefn_simulates f S T (a;;
c) (b;;
d) proof (prove)
goal (1 subgoal):
 1. \<And>s \<Gamma> t. \<lbrakk>exec_statefn_simulates f S {s. f s \<in> com_initial_guards d} a b; exec_statefn_simulates f UNIV T c d; s \<in> S; \<Gamma>\<turnstile> \<langle>a;;
c,Normal s\<rangle> \<Rightarrow> t\<rbrakk> \<Longrightarrow> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t \<or> (\<exists>ft. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')) proof (prove)
goal (1 subgoal):
 1. \<And>s \<Gamma> t c\<^sub>1 sa s' ta. \<lbrakk>exec_statefn_simulates f S {s. f s \<in> com_initial_guards d} c\<^sub>1 b; exec_statefn_simulates f UNIV T c d; sa \<in> S; a = c\<^sub>1; s = sa; t = ta; \<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal sa\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>c,s'\<rangle> \<Rightarrow> ta\<rbrakk> \<Longrightarrow> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> add_statefn_xstate f ta \<or> (\<exists>ft. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> Normal (f t')) proof (prove)
goal (1 subgoal):
 1. \<And>\<Gamma> sa s' ta. \<lbrakk>exec_statefn_simulates f S {s. f s \<in> com_initial_guards d} a b; exec_statefn_simulates f UNIV T c d; sa \<in> S; \<Gamma>\<turnstile> \<langle>a,Normal sa\<rangle> \<Rightarrow> s'; \<Gamma>\<turnstile> \<langle>c,s'\<rangle> \<Rightarrow> ta; \<not> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> add_statefn_xstate f ta; \<forall>t'\<in>- T. \<not> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> Normal (f t')\<rbrakk> \<Longrightarrow> \<exists>ft. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> Fault ft proof (prove)
goal (1 subgoal):
 1. \<And>\<Gamma> sa s' ta. \<lbrakk>exec_statefn_simulates f S {s. f s \<in> com_initial_guards d} a b; exec_statefn_simulates f UNIV T c d; sa \<in> S; \<Gamma>\<turnstile> \<langle>c,s'\<rangle> \<Rightarrow> ta; \<not> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> add_statefn_xstate f ta; \<forall>t'\<in>- T. \<not> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> Normal (f t'); (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b,Normal (f sa)\<rangle> \<Rightarrow> add_statefn_xstate f s' \<or> (\<exists>ft. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b,Normal (f sa)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- {s. f s \<in> com_initial_guards d}. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b,Normal (f sa)\<rangle> \<Rightarrow> Normal (f t'))\<rbrakk> \<Longrightarrow> \<exists>ft. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> Fault ft proof (prove)
goal (3 subgoals):
 1. \<And>\<Gamma> sa s' ta. \<lbrakk>exec_statefn_simulates f S {s. f s \<in> com_initial_guards d} a b; exec_statefn_simulates f UNIV T c d; sa \<in> S; \<Gamma>\<turnstile> \<langle>c,s'\<rangle> \<Rightarrow> ta; \<not> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> add_statefn_xstate f ta; \<forall>t'\<in>- T. \<not> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> Normal (f t'); (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b,Normal (f sa)\<rangle> \<Rightarrow> add_statefn_xstate f s'\<rbrakk> \<Longrightarrow> \<exists>ft. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> Fault ft
 2. \<And>\<Gamma> sa s' ta ft. \<lbrakk>exec_statefn_simulates f S {s. f s \<in> com_initial_guards d} a b; exec_statefn_simulates f UNIV T c d; sa \<in> S; \<Gamma>\<turnstile> \<langle>c,s'\<rangle> \<Rightarrow> ta; \<not> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> add_statefn_xstate f ta; \<forall>t'\<in>- T. \<not> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> Normal (f t'); (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b,Normal (f sa)\<rangle> \<Rightarrow> Fault ft\<rbrakk> \<Longrightarrow> \<exists>ft. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> Fault ft
 3. \<And>\<Gamma> sa s' ta. \<lbrakk>exec_statefn_simulates f S {s. f s \<in> com_initial_guards d} a b; exec_statefn_simulates f UNIV T c d; sa \<in> S; \<Gamma>\<turnstile> \<langle>c,s'\<rangle> \<Rightarrow> ta; \<not> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> add_statefn_xstate f ta; \<forall>t'\<in>- T. \<not> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> Normal (f t'); \<exists>t'\<in>- {s. f s \<in> com_initial_guards d}. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b,Normal (f sa)\<rangle> \<Rightarrow> Normal (f t')\<rbrakk> \<Longrightarrow> \<exists>ft. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> Fault ft proof (prove)
goal (6 subgoals):
 1. \<And>\<Gamma> sa s' ta x1. \<lbrakk>exec_statefn_simulates f S {s. f s \<in> com_initial_guards d} a b; exec_statefn_simulates f UNIV T c d; sa \<in> S; \<Gamma>\<turnstile> \<langle>c,Normal x1\<rangle> \<Rightarrow> ta; \<not> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> add_statefn_xstate f ta; \<forall>t'\<in>- T. \<not> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> Normal (f t'); (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b,Normal (f sa)\<rangle> \<Rightarrow> Normal (f x1); s' = Normal x1\<rbrakk> \<Longrightarrow> \<exists>ft. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> Fault ft
 2. \<And>\<Gamma> sa s' ta x2. \<lbrakk>exec_statefn_simulates f S {s. f s \<in> com_initial_guards d} a b; exec_statefn_simulates f UNIV T c d; sa \<in> S; \<Gamma>\<turnstile> \<langle>c,Abrupt x2\<rangle> \<Rightarrow> ta; \<not> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> add_statefn_xstate f ta; \<forall>t'\<in>- T. \<not> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> Normal (f t'); (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b,Normal (f sa)\<rangle> \<Rightarrow> Abrupt (f x2); s' = Abrupt x2\<rbrakk> \<Longrightarrow> \<exists>ft. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> Fault ft
 3. \<And>\<Gamma> sa s' ta x3. \<lbrakk>exec_statefn_simulates f S {s. f s \<in> com_initial_guards d} a b; exec_statefn_simulates f UNIV T c d; sa \<in> S; \<Gamma>\<turnstile> \<langle>c,Fault x3\<rangle> \<Rightarrow> ta; \<not> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> add_statefn_xstate f ta; \<forall>t'\<in>- T. \<not> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> Normal (f t'); (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b,Normal (f sa)\<rangle> \<Rightarrow> Fault x3; s' = Fault x3\<rbrakk> \<Longrightarrow> \<exists>ft. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> Fault ft
 4. \<And>\<Gamma> sa s' ta. \<lbrakk>exec_statefn_simulates f S {s. f s \<in> com_initial_guards d} a b; exec_statefn_simulates f UNIV T c d; sa \<in> S; \<Gamma>\<turnstile> \<langle>c,Stuck\<rangle> \<Rightarrow> ta; \<not> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> add_statefn_xstate f ta; \<forall>t'\<in>- T. \<not> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> Normal (f t'); (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b,Normal (f sa)\<rangle> \<Rightarrow> Stuck; s' = Stuck\<rbrakk> \<Longrightarrow> \<exists>ft. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> Fault ft
 5. \<And>\<Gamma> sa s' ta ft. \<lbrakk>exec_statefn_simulates f S {s. f s \<in> com_initial_guards d} a b; exec_statefn_simulates f UNIV T c d; sa \<in> S; \<Gamma>\<turnstile> \<langle>c,s'\<rangle> \<Rightarrow> ta; \<not> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> add_statefn_xstate f ta; \<forall>t'\<in>- T. \<not> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> Normal (f t'); (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b,Normal (f sa)\<rangle> \<Rightarrow> Fault ft\<rbrakk> \<Longrightarrow> \<exists>ft. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> Fault ft
 6. \<And>\<Gamma> sa s' ta. \<lbrakk>exec_statefn_simulates f S {s. f s \<in> com_initial_guards d} a b; exec_statefn_simulates f UNIV T c d; sa \<in> S; \<Gamma>\<turnstile> \<langle>c,s'\<rangle> \<Rightarrow> ta; \<not> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> add_statefn_xstate f ta; \<forall>t'\<in>- T. \<not> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> Normal (f t'); \<exists>t'\<in>- {s. f s \<in> com_initial_guards d}. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b,Normal (f sa)\<rangle> \<Rightarrow> Normal (f t')\<rbrakk> \<Longrightarrow> \<exists>ft. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> Fault ft proof (prove)
goal (6 subgoals):
 1. \<And>\<Gamma> sa s' ta x1. \<lbrakk>exec_statefn_simulates f S {s. f s \<in> com_initial_guards d} a b; exec_statefn_simulates f UNIV T c d; sa \<in> S; \<not> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> add_statefn_xstate f ta; \<forall>t'\<in>- T. \<not> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> Normal (f t'); (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b,Normal (f sa)\<rangle> \<Rightarrow> Normal (f x1); s' = Normal x1; (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>d,Normal (f x1)\<rangle> \<Rightarrow> add_statefn_xstate f ta \<or> (\<exists>ft. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>d,Normal (f x1)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>d,Normal (f x1)\<rangle> \<Rightarrow> Normal (f t'))\<rbrakk> \<Longrightarrow> \<exists>ft. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> Fault ft
 2. \<And>\<Gamma> sa s' ta x2. \<lbrakk>exec_statefn_simulates f S {s. f s \<in> com_initial_guards d} a b; exec_statefn_simulates f UNIV T c d; sa \<in> S; \<Gamma>\<turnstile> \<langle>c,Abrupt x2\<rangle> \<Rightarrow> ta; \<not> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> add_statefn_xstate f ta; \<forall>t'\<in>- T. \<not> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> Normal (f t'); (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b,Normal (f sa)\<rangle> \<Rightarrow> Abrupt (f x2); s' = Abrupt x2\<rbrakk> \<Longrightarrow> \<exists>ft. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> Fault ft
 3. \<And>\<Gamma> sa s' ta x3. \<lbrakk>exec_statefn_simulates f S {s. f s \<in> com_initial_guards d} a b; exec_statefn_simulates f UNIV T c d; sa \<in> S; \<Gamma>\<turnstile> \<langle>c,Fault x3\<rangle> \<Rightarrow> ta; \<not> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> add_statefn_xstate f ta; \<forall>t'\<in>- T. \<not> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> Normal (f t'); (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b,Normal (f sa)\<rangle> \<Rightarrow> Fault x3; s' = Fault x3\<rbrakk> \<Longrightarrow> \<exists>ft. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> Fault ft
 4. \<And>\<Gamma> sa s' ta. \<lbrakk>exec_statefn_simulates f S {s. f s \<in> com_initial_guards d} a b; exec_statefn_simulates f UNIV T c d; sa \<in> S; \<Gamma>\<turnstile> \<langle>c,Stuck\<rangle> \<Rightarrow> ta; \<not> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> add_statefn_xstate f ta; \<forall>t'\<in>- T. \<not> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> Normal (f t'); (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b,Normal (f sa)\<rangle> \<Rightarrow> Stuck; s' = Stuck\<rbrakk> \<Longrightarrow> \<exists>ft. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> Fault ft
 5. \<And>\<Gamma> sa s' ta ft. \<lbrakk>exec_statefn_simulates f S {s. f s \<in> com_initial_guards d} a b; exec_statefn_simulates f UNIV T c d; sa \<in> S; \<Gamma>\<turnstile> \<langle>c,s'\<rangle> \<Rightarrow> ta; \<not> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> add_statefn_xstate f ta; \<forall>t'\<in>- T. \<not> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> Normal (f t'); (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b,Normal (f sa)\<rangle> \<Rightarrow> Fault ft\<rbrakk> \<Longrightarrow> \<exists>ft. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> Fault ft
 6. \<And>\<Gamma> sa s' ta. \<lbrakk>exec_statefn_simulates f S {s. f s \<in> com_initial_guards d} a b; exec_statefn_simulates f UNIV T c d; sa \<in> S; \<Gamma>\<turnstile> \<langle>c,s'\<rangle> \<Rightarrow> ta; \<not> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> add_statefn_xstate f ta; \<forall>t'\<in>- T. \<not> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> Normal (f t'); \<exists>t'\<in>- {s. f s \<in> com_initial_guards d}. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b,Normal (f sa)\<rangle> \<Rightarrow> Normal (f t')\<rbrakk> \<Longrightarrow> \<exists>ft. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> Fault ft proof (prove)
goal (5 subgoals):
 1. \<And>\<Gamma> sa s' ta x2. \<lbrakk>exec_statefn_simulates f S {s. f s \<in> com_initial_guards d} a b; exec_statefn_simulates f UNIV T c d; sa \<in> S; \<Gamma>\<turnstile> \<langle>c,Abrupt x2\<rangle> \<Rightarrow> ta; \<not> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> add_statefn_xstate f ta; \<forall>t'\<in>- T. \<not> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> Normal (f t'); (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b,Normal (f sa)\<rangle> \<Rightarrow> Abrupt (f x2); s' = Abrupt x2\<rbrakk> \<Longrightarrow> \<exists>ft. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> Fault ft
 2. \<And>\<Gamma> sa s' ta x3. \<lbrakk>exec_statefn_simulates f S {s. f s \<in> com_initial_guards d} a b; exec_statefn_simulates f UNIV T c d; sa \<in> S; \<Gamma>\<turnstile> \<langle>c,Fault x3\<rangle> \<Rightarrow> ta; \<not> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> add_statefn_xstate f ta; \<forall>t'\<in>- T. \<not> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> Normal (f t'); (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b,Normal (f sa)\<rangle> \<Rightarrow> Fault x3; s' = Fault x3\<rbrakk> \<Longrightarrow> \<exists>ft. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> Fault ft
 3. \<And>\<Gamma> sa s' ta. \<lbrakk>exec_statefn_simulates f S {s. f s \<in> com_initial_guards d} a b; exec_statefn_simulates f UNIV T c d; sa \<in> S; \<Gamma>\<turnstile> \<langle>c,Stuck\<rangle> \<Rightarrow> ta; \<not> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> add_statefn_xstate f ta; \<forall>t'\<in>- T. \<not> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> Normal (f t'); (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b,Normal (f sa)\<rangle> \<Rightarrow> Stuck; s' = Stuck\<rbrakk> \<Longrightarrow> \<exists>ft. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> Fault ft
 4. \<And>\<Gamma> sa s' ta ft. \<lbrakk>exec_statefn_simulates f S {s. f s \<in> com_initial_guards d} a b; exec_statefn_simulates f UNIV T c d; sa \<in> S; \<Gamma>\<turnstile> \<langle>c,s'\<rangle> \<Rightarrow> ta; \<not> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> add_statefn_xstate f ta; \<forall>t'\<in>- T. \<not> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> Normal (f t'); (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b,Normal (f sa)\<rangle> \<Rightarrow> Fault ft\<rbrakk> \<Longrightarrow> \<exists>ft. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> Fault ft
 5. \<And>\<Gamma> sa s' ta. \<lbrakk>exec_statefn_simulates f S {s. f s \<in> com_initial_guards d} a b; exec_statefn_simulates f UNIV T c d; sa \<in> S; \<Gamma>\<turnstile> \<langle>c,s'\<rangle> \<Rightarrow> ta; \<not> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> add_statefn_xstate f ta; \<forall>t'\<in>- T. \<not> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> Normal (f t'); \<exists>t'\<in>- {s. f s \<in> com_initial_guards d}. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b,Normal (f sa)\<rangle> \<Rightarrow> Normal (f t')\<rbrakk> \<Longrightarrow> \<exists>ft. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> Fault ft proof (prove)
goal (1 subgoal):
 1. \<And>\<Gamma> sa s' ta. \<lbrakk>exec_statefn_simulates f S {s. f s \<in> com_initial_guards d} a b; exec_statefn_simulates f UNIV T c d; sa \<in> S; \<Gamma>\<turnstile> \<langle>c,s'\<rangle> \<Rightarrow> ta; \<not> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> add_statefn_xstate f ta; \<forall>t'\<in>- T. \<not> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> Normal (f t'); \<exists>t'\<in>- {s. f s \<in> com_initial_guards d}. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b,Normal (f sa)\<rangle> \<Rightarrow> Normal (f t')\<rbrakk> \<Longrightarrow> \<exists>ft. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> Fault ft proof (prove)
goal (1 subgoal):
 1. \<And>\<Gamma> sa s' ta t'. \<lbrakk>exec_statefn_simulates f S {s. f s \<in> com_initial_guards d} a b; exec_statefn_simulates f UNIV T c d; sa \<in> S; \<Gamma>\<turnstile> \<langle>c,s'\<rangle> \<Rightarrow> ta; \<not> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> add_statefn_xstate f ta; \<forall>t'\<in>- T. \<not> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> Normal (f t'); (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b,Normal (f sa)\<rangle> \<Rightarrow> Normal (f t'); \<forall>ft. \<not> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> Fault ft\<rbrakk> \<Longrightarrow> f t' \<in> com_initial_guards d proof (prove)
goal (1 subgoal):
 1. \<And>\<Gamma> sa s' ta t' ft. \<lbrakk>exec_statefn_simulates f S {s. f s \<in> com_initial_guards d} a b; exec_statefn_simulates f UNIV T c d; sa \<in> S; \<Gamma>\<turnstile> \<langle>c,s'\<rangle> \<Rightarrow> ta; \<not> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> add_statefn_xstate f ta; \<forall>t'\<in>- T. \<not> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> Normal (f t'); (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b,Normal (f sa)\<rangle> \<Rightarrow> Normal (f t'); \<forall>ft. \<not> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b;;
d,Normal (f sa)\<rangle> \<Rightarrow> Fault ft; f t' \<notin> com_initial_guards d; (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>d,Normal (f t')\<rangle> \<Rightarrow> Fault ft\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!