theory CCorresLemmas

lemma ccorres_While_Normal_helper:
  assumes setter_inv:
    "\<Gamma> \<turnstile> {s'. \<exists>rv s. G rv s s'} setter {s'. \<exists>rv s. G rv s s' \<and> (cond_xf s' \<noteq> 0 \<longrightarrow> Cnd rv s s')}"
  assumes body_inv: "\<Gamma> \<turnstile> {s'. \<exists>rv s. G rv s s' \<and> Cnd rv s s'} B {s'. \<exists>rv s. G rv s s'}"
  shows "\<Gamma> \<turnstile> ({s'. \<exists>rv s. G rv s s' \<and> (cond_xf s' \<noteq> 0 \<longrightarrow> Cnd rv s s')})
             While {s'. cond_xf s' \<noteq> 0} (Seq B setter)
             {s'. \<exists>rv s. G rv s s'}" apply (insert assms) apply (rule hoare_complete) apply (simp add: cvalid_def HoarePartialDef.valid_def) apply (intro allI) apply (rename_tac xstate xstate') apply (rule impI) apply (case_tac "\<not> isNormal xstate") apply fastforce apply (simp add: isNormal_def) apply (elim exE) apply (simp add: image_def) apply (erule exec_While_final_inv''[where C="{s'. cond_xf s' \<noteq> 0}" and B="B;; setter"]; clarsimp) apply (frule intermediate_Normal_state[OF _ _ body_inv]) apply fastforce apply clarsimp apply (rename_tac inter_t) apply (frule hoarep_exec[OF _ _ body_inv, rotated], fastforce) apply (frule_tac s=inter_t in hoarep_exec[rotated 2], fastforce+)[1] apply (metis (mono_tags, lifting) HoarePartial.SeqSwap empty_iff exec_abrupt mem_Collect_eq) apply (metis (mono_tags, lifting) HoarePartial.SeqSwap exec_stuck mem_Collect_eq) apply (metis (mono_tags, lifting) HoarePartial.SeqSwap empty_iff exec_fault mem_Collect_eq) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s' \<and> (cond_xf s' \<noteq> (0::'f) \<longrightarrow> Cnd rv s s')} While {s'. cond_xf s' \<noteq> (0::'f)} (B;;
setter) {s'. \<exists>rv s. G rv s s'} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s'} setter {s'. \<exists>rv s. G rv s s' \<and> (cond_xf s' \<noteq> (0::'f) \<longrightarrow> Cnd rv s s')}; \<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s' \<and> Cnd rv s s'} B {s'. \<exists>rv s. G rv s s'}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s' \<and> (cond_xf s' \<noteq> (0::'f) \<longrightarrow> Cnd rv s s')} While {s'. cond_xf s' \<noteq> (0::'f)} (B;;
setter) {s'. \<exists>rv s. G rv s s'} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s'} setter {s'. \<exists>rv s. G rv s s' \<and> (cond_xf s' \<noteq> (0::'f) \<longrightarrow> Cnd rv s s')}; \<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s' \<and> Cnd rv s s'} B {s'. \<exists>rv s. G rv s s'}\<rbrakk> \<Longrightarrow> \<Gamma>\<Turnstile>\<^bsub>/{}\<^esub> {s'. \<exists>rv s. G rv s s' \<and> (cond_xf s' \<noteq> (0::'f) \<longrightarrow> Cnd rv s s')} While {s'. cond_xf s' \<noteq> (0::'f)} (B;;
setter) {s'. \<exists>rv s. G rv s s'},{} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s'} setter {s'. \<exists>rv s. G rv s s' \<and> (cond_xf s' \<noteq> (0::'f) \<longrightarrow> Cnd rv s s')}; \<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s' \<and> Cnd rv s s'} B {s'. \<exists>rv s. G rv s s'}\<rbrakk> \<Longrightarrow> \<forall>s t. \<Gamma>\<turnstile> \<langle>While {s'. cond_xf s' \<noteq> (0::'f)} (B;;
setter),s\<rangle> \<Rightarrow> t \<longrightarrow> s \<in> Normal ` {s'. \<exists>rv s. G rv s s' \<and> (cond_xf s' \<noteq> (0::'f) \<longrightarrow> Cnd rv s s')} \<longrightarrow> t \<in> Normal ` {s'. \<exists>rv s. G rv s s'} proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>\<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s'} setter {s'. \<exists>rv s. G rv s s' \<and> (cond_xf s' \<noteq> (0::'f) \<longrightarrow> Cnd rv s s')}; \<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s' \<and> Cnd rv s s'} B {s'. \<exists>rv s. G rv s s'}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While {s'. cond_xf s' \<noteq> (0::'f)} (B;;
setter),s\<rangle> \<Rightarrow> t \<longrightarrow> s \<in> Normal ` {s'. \<exists>rv s. G rv s s' \<and> (cond_xf s' \<noteq> (0::'f) \<longrightarrow> Cnd rv s s')} \<longrightarrow> t \<in> Normal ` {s'. \<exists>rv s. G rv s s'} proof (prove)
goal (1 subgoal):
 1. \<And>xstate xstate'. \<lbrakk>\<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s'} setter {s'. \<exists>rv s. G rv s s' \<and> (cond_xf s' \<noteq> (0::'f) \<longrightarrow> Cnd rv s s')}; \<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s' \<and> Cnd rv s s'} B {s'. \<exists>rv s. G rv s s'}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>While {s'. cond_xf s' \<noteq> (0::'f)} (B;;
setter),xstate\<rangle> \<Rightarrow> xstate' \<longrightarrow> xstate \<in> Normal ` {s'. \<exists>rv s. G rv s s' \<and> (cond_xf s' \<noteq> (0::'f) \<longrightarrow> Cnd rv s s')} \<longrightarrow> xstate' \<in> Normal ` {s'. \<exists>rv s. G rv s s'} proof (prove)
goal (1 subgoal):
 1. \<And>xstate xstate'. \<lbrakk>\<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s'} setter {s'. \<exists>rv s. G rv s s' \<and> (cond_xf s' \<noteq> (0::'f) \<longrightarrow> Cnd rv s s')}; \<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s' \<and> Cnd rv s s'} B {s'. \<exists>rv s. G rv s s'}; \<Gamma>\<turnstile> \<langle>While {s'. cond_xf s' \<noteq> (0::'f)} (B;;
setter),xstate\<rangle> \<Rightarrow> xstate'\<rbrakk> \<Longrightarrow> xstate \<in> Normal ` {s'. \<exists>rv s. G rv s s' \<and> (cond_xf s' \<noteq> (0::'f) \<longrightarrow> Cnd rv s s')} \<longrightarrow> xstate' \<in> Normal ` {s'. \<exists>rv s. G rv s s'} proof (prove)
goal (2 subgoals):
 1. \<And>xstate xstate'. \<lbrakk>\<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s'} setter {s'. \<exists>rv s. G rv s s' \<and> (cond_xf s' \<noteq> (0::'f) \<longrightarrow> Cnd rv s s')}; \<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s' \<and> Cnd rv s s'} B {s'. \<exists>rv s. G rv s s'}; \<Gamma>\<turnstile> \<langle>While {s'. cond_xf s' \<noteq> (0::'f)} (B;;
setter),xstate\<rangle> \<Rightarrow> xstate'; \<not> isNormal xstate\<rbrakk> \<Longrightarrow> xstate \<in> Normal ` {s'. \<exists>rv s. G rv s s' \<and> (cond_xf s' \<noteq> (0::'f) \<longrightarrow> Cnd rv s s')} \<longrightarrow> xstate' \<in> Normal ` {s'. \<exists>rv s. G rv s s'}
 2. \<And>xstate xstate'. \<lbrakk>\<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s'} setter {s'. \<exists>rv s. G rv s s' \<and> (cond_xf s' \<noteq> (0::'f) \<longrightarrow> Cnd rv s s')}; \<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s' \<and> Cnd rv s s'} B {s'. \<exists>rv s. G rv s s'}; \<Gamma>\<turnstile> \<langle>While {s'. cond_xf s' \<noteq> (0::'f)} (B;;
setter),xstate\<rangle> \<Rightarrow> xstate'; \<not> \<not> isNormal xstate\<rbrakk> \<Longrightarrow> xstate \<in> Normal ` {s'. \<exists>rv s. G rv s s' \<and> (cond_xf s' \<noteq> (0::'f) \<longrightarrow> Cnd rv s s')} \<longrightarrow> xstate' \<in> Normal ` {s'. \<exists>rv s. G rv s s'} proof (prove)
goal (1 subgoal):
 1. \<And>xstate xstate'. \<lbrakk>\<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s'} setter {s'. \<exists>rv s. G rv s s' \<and> (cond_xf s' \<noteq> (0::'f) \<longrightarrow> Cnd rv s s')}; \<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s' \<and> Cnd rv s s'} B {s'. \<exists>rv s. G rv s s'}; \<Gamma>\<turnstile> \<langle>While {s'. cond_xf s' \<noteq> (0::'f)} (B;;
setter),xstate\<rangle> \<Rightarrow> xstate'; \<not> \<not> isNormal xstate\<rbrakk> \<Longrightarrow> xstate \<in> Normal ` {s'. \<exists>rv s. G rv s s' \<and> (cond_xf s' \<noteq> (0::'f) \<longrightarrow> Cnd rv s s')} \<longrightarrow> xstate' \<in> Normal ` {s'. \<exists>rv s. G rv s s'} proof (prove)
goal (1 subgoal):
 1. \<And>xstate xstate'. \<lbrakk>\<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s'} setter {s'. \<exists>rv s. G rv s s' \<and> (cond_xf s' \<noteq> (0::'f) \<longrightarrow> Cnd rv s s')}; \<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s' \<and> Cnd rv s s'} B {s'. \<exists>rv s. G rv s s'}; \<Gamma>\<turnstile> \<langle>While {s'. cond_xf s' \<noteq> (0::'f)} (B;;
setter),xstate\<rangle> \<Rightarrow> xstate'; \<exists>s. xstate = Normal s\<rbrakk> \<Longrightarrow> xstate \<in> Normal ` {s'. \<exists>rv s. G rv s s' \<and> (cond_xf s' \<noteq> (0::'f) \<longrightarrow> Cnd rv s s')} \<longrightarrow> xstate' \<in> Normal ` {s'. \<exists>rv s. G rv s s'} proof (prove)
goal (1 subgoal):
 1. \<And>xstate xstate' s. \<lbrakk>\<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s'} setter {s'. \<exists>rv s. G rv s s' \<and> (cond_xf s' \<noteq> (0::'f) \<longrightarrow> Cnd rv s s')}; \<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s' \<and> Cnd rv s s'} B {s'. \<exists>rv s. G rv s s'}; \<Gamma>\<turnstile> \<langle>While {s'. cond_xf s' \<noteq> (0::'f)} (B;;
setter),xstate\<rangle> \<Rightarrow> xstate'; xstate = Normal s\<rbrakk> \<Longrightarrow> xstate \<in> Normal ` {s'. \<exists>rv s. G rv s s' \<and> (cond_xf s' \<noteq> (0::'f) \<longrightarrow> Cnd rv s s')} \<longrightarrow> xstate' \<in> Normal ` {s'. \<exists>rv s. G rv s s'} proof (prove)
goal (1 subgoal):
 1. \<And>xstate xstate' s. \<lbrakk>\<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s'} setter {s'. \<exists>rv s. G rv s s' \<and> (cond_xf s' \<noteq> (0::'f) \<longrightarrow> Cnd rv s s')}; \<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s' \<and> Cnd rv s s'} B {s'. \<exists>rv s. G rv s s'}; \<Gamma>\<turnstile> \<langle>While {s'. cond_xf s' \<noteq> (0::'f)} (B;;
setter),Normal s\<rangle> \<Rightarrow> xstate'; xstate = Normal s\<rbrakk> \<Longrightarrow> (\<exists>rv sa. G rv sa s \<and> (cond_xf s \<noteq> (0::'f) \<longrightarrow> Cnd rv sa s)) \<longrightarrow> (\<exists>x. (\<exists>rv s. G rv s x) \<and> xstate' = Normal x) proof (prove)
goal (4 subgoals):
 1. \<And>t t' t'' rv sa. \<lbrakk>\<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s'} setter {s'. \<exists>rv s. G rv s s' \<and> (cond_xf s' \<noteq> (0::'f) \<longrightarrow> Cnd rv s s')}; \<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s' \<and> Cnd rv s s'} B {s'. \<exists>rv s. G rv s s'}; cond_xf t \<noteq> (0::'f); \<Gamma>\<turnstile> \<langle>B;;
setter,Normal t\<rangle> \<Rightarrow> Normal t'; \<Gamma>\<turnstile> \<langle>While {s'. cond_xf s' \<noteq> (0::'f)} (B;;
setter),Normal t'\<rangle> \<Rightarrow> t''; G rv sa t; Cnd rv sa t; \<forall>rv s. G rv s t' \<longrightarrow> cond_xf t' \<noteq> (0::'f) \<and> \<not> Cnd rv s t'\<rbrakk> \<Longrightarrow> \<exists>x. (\<exists>rv s. G rv s x) \<and> t'' = Normal x
 2. \<And>t t' rv sa. \<lbrakk>\<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s'} setter {s'. \<exists>rv s. G rv s s' \<and> (cond_xf s' \<noteq> (0::'f) \<longrightarrow> Cnd rv s s')}; \<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s' \<and> Cnd rv s s'} B {s'. \<exists>rv s. G rv s s'}; cond_xf t \<noteq> (0::'f); \<Gamma>\<turnstile> \<langle>B;;
setter,Normal t\<rangle> \<Rightarrow> Abrupt t'; G rv sa t; Cnd rv sa t\<rbrakk> \<Longrightarrow> False
 3. \<And>t rv sa. \<lbrakk>\<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s'} setter {s'. \<exists>rv s. G rv s s' \<and> (cond_xf s' \<noteq> (0::'f) \<longrightarrow> Cnd rv s s')}; \<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s' \<and> Cnd rv s s'} B {s'. \<exists>rv s. G rv s s'}; cond_xf t \<noteq> (0::'f); \<Gamma>\<turnstile> \<langle>B;;
setter,Normal t\<rangle> \<Rightarrow> Stuck; G rv sa t; Cnd rv sa t\<rbrakk> \<Longrightarrow> False
 4. \<And>t f rv sa. \<lbrakk>\<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s'} setter {s'. \<exists>rv s. G rv s s' \<and> (cond_xf s' \<noteq> (0::'f) \<longrightarrow> Cnd rv s s')}; \<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s' \<and> Cnd rv s s'} B {s'. \<exists>rv s. G rv s s'}; cond_xf t \<noteq> (0::'f); \<Gamma>\<turnstile> \<langle>B;;
setter,Normal t\<rangle> \<Rightarrow> Fault f; G rv sa t; Cnd rv sa t\<rbrakk> \<Longrightarrow> False proof (prove)
goal (5 subgoals):
 1. \<And>t t' t'' rv sa. \<lbrakk>\<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s'} setter {s'. \<exists>rv s. G rv s s' \<and> (cond_xf s' \<noteq> (0::'f) \<longrightarrow> Cnd rv s s')}; \<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s' \<and> Cnd rv s s'} B {s'. \<exists>rv s. G rv s s'}; cond_xf t \<noteq> (0::'f); \<Gamma>\<turnstile> \<langle>B;;
setter,Normal t\<rangle> \<Rightarrow> Normal t'; \<Gamma>\<turnstile> \<langle>While {s'. cond_xf s' \<noteq> (0::'f)} (B;;
setter),Normal t'\<rangle> \<Rightarrow> t''; G rv sa t; Cnd rv sa t; \<forall>rv s. G rv s t' \<longrightarrow> cond_xf t' \<noteq> (0::'f) \<and> \<not> Cnd rv s t'\<rbrakk> \<Longrightarrow> t \<in> {s'. \<exists>rv s. G rv s s' \<and> Cnd rv s s'}
 2. \<And>t t' t'' rv sa. \<lbrakk>\<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s'} setter {s'. \<exists>rv s. G rv s s' \<and> (cond_xf s' \<noteq> (0::'f) \<longrightarrow> Cnd rv s s')}; \<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s' \<and> Cnd rv s s'} B {s'. \<exists>rv s. G rv s s'}; cond_xf t \<noteq> (0::'f); \<Gamma>\<turnstile> \<langle>B;;
setter,Normal t\<rangle> \<Rightarrow> Normal t'; \<Gamma>\<turnstile> \<langle>While {s'. cond_xf s' \<noteq> (0::'f)} (B;;
setter),Normal t'\<rangle> \<Rightarrow> t''; G rv sa t; Cnd rv sa t; \<forall>rv s. G rv s t' \<longrightarrow> cond_xf t' \<noteq> (0::'f) \<and> \<not> Cnd rv s t'; \<exists>t'a. \<Gamma>\<turnstile> \<langle>B,Normal t\<rangle> \<Rightarrow> Normal t'a \<and> \<Gamma>\<turnstile> \<langle>setter,Normal t'a\<rangle> \<Rightarrow> Normal t'\<rbrakk> \<Longrightarrow> \<exists>x. (\<exists>rv s. G rv s x) \<and> t'' = Normal x
 3. \<And>t t' rv sa. \<lbrakk>\<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s'} setter {s'. \<exists>rv s. G rv s s' \<and> (cond_xf s' \<noteq> (0::'f) \<longrightarrow> Cnd rv s s')}; \<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s' \<and> Cnd rv s s'} B {s'. \<exists>rv s. G rv s s'}; cond_xf t \<noteq> (0::'f); \<Gamma>\<turnstile> \<langle>B;;
setter,Normal t\<rangle> \<Rightarrow> Abrupt t'; G rv sa t; Cnd rv sa t\<rbrakk> \<Longrightarrow> False
 4. \<And>t rv sa. \<lbrakk>\<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s'} setter {s'. \<exists>rv s. G rv s s' \<and> (cond_xf s' \<noteq> (0::'f) \<longrightarrow> Cnd rv s s')}; \<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s' \<and> Cnd rv s s'} B {s'. \<exists>rv s. G rv s s'}; cond_xf t \<noteq> (0::'f); \<Gamma>\<turnstile> \<langle>B;;
setter,Normal t\<rangle> \<Rightarrow> Stuck; G rv sa t; Cnd rv sa t\<rbrakk> \<Longrightarrow> False
 5. \<And>t f rv sa. \<lbrakk>\<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s'} setter {s'. \<exists>rv s. G rv s s' \<and> (cond_xf s' \<noteq> (0::'f) \<longrightarrow> Cnd rv s s')}; \<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s' \<and> Cnd rv s s'} B {s'. \<exists>rv s. G rv s s'}; cond_xf t \<noteq> (0::'f); \<Gamma>\<turnstile> \<langle>B;;
setter,Normal t\<rangle> \<Rightarrow> Fault f; G rv sa t; Cnd rv sa t\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>t t' t'' rv sa. \<lbrakk>\<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s'} setter {s'. \<exists>rv s. G rv s s' \<and> (cond_xf s' \<noteq> (0::'f) \<longrightarrow> Cnd rv s s')}; \<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s' \<and> Cnd rv s s'} B {s'. \<exists>rv s. G rv s s'}; cond_xf t \<noteq> (0::'f); \<Gamma>\<turnstile> \<langle>B;;
setter,Normal t\<rangle> \<Rightarrow> Normal t'; \<Gamma>\<turnstile> \<langle>While {s'. cond_xf s' \<noteq> (0::'f)} (B;;
setter),Normal t'\<rangle> \<Rightarrow> t''; G rv sa t; Cnd rv sa t; \<forall>rv s. G rv s t' \<longrightarrow> cond_xf t' \<noteq> (0::'f) \<and> \<not> Cnd rv s t'; \<exists>t'a. \<Gamma>\<turnstile> \<langle>B,Normal t\<rangle> \<Rightarrow> Normal t'a \<and> \<Gamma>\<turnstile> \<langle>setter,Normal t'a\<rangle> \<Rightarrow> Normal t'\<rbrakk> \<Longrightarrow> \<exists>x. (\<exists>rv s. G rv s x) \<and> t'' = Normal x
 2. \<And>t t' rv sa. \<lbrakk>\<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s'} setter {s'. \<exists>rv s. G rv s s' \<and> (cond_xf s' \<noteq> (0::'f) \<longrightarrow> Cnd rv s s')}; \<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s' \<and> Cnd rv s s'} B {s'. \<exists>rv s. G rv s s'}; cond_xf t \<noteq> (0::'f); \<Gamma>\<turnstile> \<langle>B;;
setter,Normal t\<rangle> \<Rightarrow> Abrupt t'; G rv sa t; Cnd rv sa t\<rbrakk> \<Longrightarrow> False
 3. \<And>t rv sa. \<lbrakk>\<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s'} setter {s'. \<exists>rv s. G rv s s' \<and> (cond_xf s' \<noteq> (0::'f) \<longrightarrow> Cnd rv s s')}; \<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s' \<and> Cnd rv s s'} B {s'. \<exists>rv s. G rv s s'}; cond_xf t \<noteq> (0::'f); \<Gamma>\<turnstile> \<langle>B;;
setter,Normal t\<rangle> \<Rightarrow> Stuck; G rv sa t; Cnd rv sa t\<rbrakk> \<Longrightarrow> False
 4. \<And>t f rv sa. \<lbrakk>\<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s'} setter {s'. \<exists>rv s. G rv s s' \<and> (cond_xf s' \<noteq> (0::'f) \<longrightarrow> Cnd rv s s')}; \<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s' \<and> Cnd rv s s'} B {s'. \<exists>rv s. G rv s s'}; cond_xf t \<noteq> (0::'f); \<Gamma>\<turnstile> \<langle>B;;
setter,Normal t\<rangle> \<Rightarrow> Fault f; G rv sa t; Cnd rv sa t\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>t t' t'' rv sa t'a. \<lbrakk>\<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s'} setter {s'. \<exists>rv s. G rv s s' \<and> (cond_xf s' \<noteq> (0::'f) \<longrightarrow> Cnd rv s s')}; \<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s' \<and> Cnd rv s s'} B {s'. \<exists>rv s. G rv s s'}; cond_xf t \<noteq> (0::'f); \<Gamma>\<turnstile> \<langle>B;;
setter,Normal t\<rangle> \<Rightarrow> Normal t'; \<Gamma>\<turnstile> \<langle>While {s'. cond_xf s' \<noteq> (0::'f)} (B;;
setter),Normal t'\<rangle> \<Rightarrow> t''; G rv sa t; Cnd rv sa t; \<forall>rv s. G rv s t' \<longrightarrow> cond_xf t' \<noteq> (0::'f) \<and> \<not> Cnd rv s t'; \<Gamma>\<turnstile> \<langle>B,Normal t\<rangle> \<Rightarrow> Normal t'a; \<Gamma>\<turnstile> \<langle>setter,Normal t'a\<rangle> \<Rightarrow> Normal t'\<rbrakk> \<Longrightarrow> \<exists>x. (\<exists>rv s. G rv s x) \<and> t'' = Normal x
 2. \<And>t t' rv sa. \<lbrakk>\<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s'} setter {s'. \<exists>rv s. G rv s s' \<and> (cond_xf s' \<noteq> (0::'f) \<longrightarrow> Cnd rv s s')}; \<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s' \<and> Cnd rv s s'} B {s'. \<exists>rv s. G rv s s'}; cond_xf t \<noteq> (0::'f); \<Gamma>\<turnstile> \<langle>B;;
setter,Normal t\<rangle> \<Rightarrow> Abrupt t'; G rv sa t; Cnd rv sa t\<rbrakk> \<Longrightarrow> False
 3. \<And>t rv sa. \<lbrakk>\<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s'} setter {s'. \<exists>rv s. G rv s s' \<and> (cond_xf s' \<noteq> (0::'f) \<longrightarrow> Cnd rv s s')}; \<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s' \<and> Cnd rv s s'} B {s'. \<exists>rv s. G rv s s'}; cond_xf t \<noteq> (0::'f); \<Gamma>\<turnstile> \<langle>B;;
setter,Normal t\<rangle> \<Rightarrow> Stuck; G rv sa t; Cnd rv sa t\<rbrakk> \<Longrightarrow> False
 4. \<And>t f rv sa. \<lbrakk>\<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s'} setter {s'. \<exists>rv s. G rv s s' \<and> (cond_xf s' \<noteq> (0::'f) \<longrightarrow> Cnd rv s s')}; \<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s' \<and> Cnd rv s s'} B {s'. \<exists>rv s. G rv s s'}; cond_xf t \<noteq> (0::'f); \<Gamma>\<turnstile> \<langle>B;;
setter,Normal t\<rangle> \<Rightarrow> Fault f; G rv sa t; Cnd rv sa t\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>t t' t'' rv sa inter_t. \<lbrakk>\<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s'} setter {s'. \<exists>rv s. G rv s s' \<and> (cond_xf s' \<noteq> (0::'f) \<longrightarrow> Cnd rv s s')}; \<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s' \<and> Cnd rv s s'} B {s'. \<exists>rv s. G rv s s'}; cond_xf t \<noteq> (0::'f); \<Gamma>\<turnstile> \<langle>B;;
setter,Normal t\<rangle> \<Rightarrow> Normal t'; \<Gamma>\<turnstile> \<langle>While {s'. cond_xf s' \<noteq> (0::'f)} (B;;
setter),Normal t'\<rangle> \<Rightarrow> t''; G rv sa t; Cnd rv sa t; \<forall>rv s. G rv s t' \<longrightarrow> cond_xf t' \<noteq> (0::'f) \<and> \<not> Cnd rv s t'; \<Gamma>\<turnstile> \<langle>B,Normal t\<rangle> \<Rightarrow> Normal inter_t; \<Gamma>\<turnstile> \<langle>setter,Normal inter_t\<rangle> \<Rightarrow> Normal t'\<rbrakk> \<Longrightarrow> \<exists>x. (\<exists>rv s. G rv s x) \<and> t'' = Normal x
 2. \<And>t t' rv sa. \<lbrakk>\<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s'} setter {s'. \<exists>rv s. G rv s s' \<and> (cond_xf s' \<noteq> (0::'f) \<longrightarrow> Cnd rv s s')}; \<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s' \<and> Cnd rv s s'} B {s'. \<exists>rv s. G rv s s'}; cond_xf t \<noteq> (0::'f); \<Gamma>\<turnstile> \<langle>B;;
setter,Normal t\<rangle> \<Rightarrow> Abrupt t'; G rv sa t; Cnd rv sa t\<rbrakk> \<Longrightarrow> False
 3. \<And>t rv sa. \<lbrakk>\<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s'} setter {s'. \<exists>rv s. G rv s s' \<and> (cond_xf s' \<noteq> (0::'f) \<longrightarrow> Cnd rv s s')}; \<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s' \<and> Cnd rv s s'} B {s'. \<exists>rv s. G rv s s'}; cond_xf t \<noteq> (0::'f); \<Gamma>\<turnstile> \<langle>B;;
setter,Normal t\<rangle> \<Rightarrow> Stuck; G rv sa t; Cnd rv sa t\<rbrakk> \<Longrightarrow> False
 4. \<And>t f rv sa. \<lbrakk>\<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s'} setter {s'. \<exists>rv s. G rv s s' \<and> (cond_xf s' \<noteq> (0::'f) \<longrightarrow> Cnd rv s s')}; \<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s' \<and> Cnd rv s s'} B {s'. \<exists>rv s. G rv s s'}; cond_xf t \<noteq> (0::'f); \<Gamma>\<turnstile> \<langle>B;;
setter,Normal t\<rangle> \<Rightarrow> Fault f; G rv sa t; Cnd rv sa t\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>t t' t'' rv sa inter_t. \<lbrakk>\<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s'} setter {s'. \<exists>rv s. G rv s s' \<and> (cond_xf s' \<noteq> (0::'f) \<longrightarrow> Cnd rv s s')}; \<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s' \<and> Cnd rv s s'} B {s'. \<exists>rv s. G rv s s'}; cond_xf t \<noteq> (0::'f); \<Gamma>\<turnstile> \<langle>B;;
setter,Normal t\<rangle> \<Rightarrow> Normal t'; \<Gamma>\<turnstile> \<langle>While {s'. cond_xf s' \<noteq> (0::'f)} (B;;
setter),Normal t'\<rangle> \<Rightarrow> t''; G rv sa t; Cnd rv sa t; \<forall>rv s. G rv s t' \<longrightarrow> cond_xf t' \<noteq> (0::'f) \<and> \<not> Cnd rv s t'; \<Gamma>\<turnstile> \<langle>B,Normal t\<rangle> \<Rightarrow> Normal inter_t; \<Gamma>\<turnstile> \<langle>setter,Normal inter_t\<rangle> \<Rightarrow> Normal t'; (\<exists>f\<in>{}. Normal inter_t = Fault f) \<or> (\<exists>t'\<in>{s'. \<exists>rv s. G rv s s'}. Normal inter_t = Normal t') \<or> (\<exists>t'\<in>{}. Normal inter_t = Abrupt t')\<rbrakk> \<Longrightarrow> \<exists>x. (\<exists>rv s. G rv s x) \<and> t'' = Normal x
 2. \<And>t t' rv sa. \<lbrakk>\<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s'} setter {s'. \<exists>rv s. G rv s s' \<and> (cond_xf s' \<noteq> (0::'f) \<longrightarrow> Cnd rv s s')}; \<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s' \<and> Cnd rv s s'} B {s'. \<exists>rv s. G rv s s'}; cond_xf t \<noteq> (0::'f); \<Gamma>\<turnstile> \<langle>B;;
setter,Normal t\<rangle> \<Rightarrow> Abrupt t'; G rv sa t; Cnd rv sa t\<rbrakk> \<Longrightarrow> False
 3. \<And>t rv sa. \<lbrakk>\<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s'} setter {s'. \<exists>rv s. G rv s s' \<and> (cond_xf s' \<noteq> (0::'f) \<longrightarrow> Cnd rv s s')}; \<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s' \<and> Cnd rv s s'} B {s'. \<exists>rv s. G rv s s'}; cond_xf t \<noteq> (0::'f); \<Gamma>\<turnstile> \<langle>B;;
setter,Normal t\<rangle> \<Rightarrow> Stuck; G rv sa t; Cnd rv sa t\<rbrakk> \<Longrightarrow> False
 4. \<And>t f rv sa. \<lbrakk>\<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s'} setter {s'. \<exists>rv s. G rv s s' \<and> (cond_xf s' \<noteq> (0::'f) \<longrightarrow> Cnd rv s s')}; \<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s' \<and> Cnd rv s s'} B {s'. \<exists>rv s. G rv s s'}; cond_xf t \<noteq> (0::'f); \<Gamma>\<turnstile> \<langle>B;;
setter,Normal t\<rangle> \<Rightarrow> Fault f; G rv sa t; Cnd rv sa t\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>t t' rv sa. \<lbrakk>\<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s'} setter {s'. \<exists>rv s. G rv s s' \<and> (cond_xf s' \<noteq> (0::'f) \<longrightarrow> Cnd rv s s')}; \<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s' \<and> Cnd rv s s'} B {s'. \<exists>rv s. G rv s s'}; cond_xf t \<noteq> (0::'f); \<Gamma>\<turnstile> \<langle>B;;
setter,Normal t\<rangle> \<Rightarrow> Abrupt t'; G rv sa t; Cnd rv sa t\<rbrakk> \<Longrightarrow> False
 2. \<And>t rv sa. \<lbrakk>\<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s'} setter {s'. \<exists>rv s. G rv s s' \<and> (cond_xf s' \<noteq> (0::'f) \<longrightarrow> Cnd rv s s')}; \<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s' \<and> Cnd rv s s'} B {s'. \<exists>rv s. G rv s s'}; cond_xf t \<noteq> (0::'f); \<Gamma>\<turnstile> \<langle>B;;
setter,Normal t\<rangle> \<Rightarrow> Stuck; G rv sa t; Cnd rv sa t\<rbrakk> \<Longrightarrow> False
 3. \<And>t f rv sa. \<lbrakk>\<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s'} setter {s'. \<exists>rv s. G rv s s' \<and> (cond_xf s' \<noteq> (0::'f) \<longrightarrow> Cnd rv s s')}; \<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s' \<and> Cnd rv s s'} B {s'. \<exists>rv s. G rv s s'}; cond_xf t \<noteq> (0::'f); \<Gamma>\<turnstile> \<langle>B;;
setter,Normal t\<rangle> \<Rightarrow> Fault f; G rv sa t; Cnd rv sa t\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>t rv sa. \<lbrakk>\<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s'} setter {s'. \<exists>rv s. G rv s s' \<and> (cond_xf s' \<noteq> (0::'f) \<longrightarrow> Cnd rv s s')}; \<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s' \<and> Cnd rv s s'} B {s'. \<exists>rv s. G rv s s'}; cond_xf t \<noteq> (0::'f); \<Gamma>\<turnstile> \<langle>B;;
setter,Normal t\<rangle> \<Rightarrow> Stuck; G rv sa t; Cnd rv sa t\<rbrakk> \<Longrightarrow> False
 2. \<And>t f rv sa. \<lbrakk>\<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s'} setter {s'. \<exists>rv s. G rv s s' \<and> (cond_xf s' \<noteq> (0::'f) \<longrightarrow> Cnd rv s s')}; \<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s' \<and> Cnd rv s s'} B {s'. \<exists>rv s. G rv s s'}; cond_xf t \<noteq> (0::'f); \<Gamma>\<turnstile> \<langle>B;;
setter,Normal t\<rangle> \<Rightarrow> Fault f; G rv sa t; Cnd rv sa t\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>t f rv sa. \<lbrakk>\<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s'} setter {s'. \<exists>rv s. G rv s s' \<and> (cond_xf s' \<noteq> (0::'f) \<longrightarrow> Cnd rv s s')}; \<Gamma>\<turnstile> {s'. \<exists>rv s. G rv s s' \<and> Cnd rv s s'} B {s'. \<exists>rv s. G rv s s'}; cond_xf t \<noteq> (0::'f); \<Gamma>\<turnstile> \<langle>B;;
setter,Normal t\<rangle> \<Rightarrow> Fault f; G rv sa t; Cnd rv sa t\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!