theory SimplRewrite

lemma gabi_simulation:
  "\<lbrakk> G \<turnstile> \<langle>c, xs\<rangle> \<Rightarrow> xs';
        guards_adjust_by_invariant S T c c';
        xs \<in> xstate_inv_set (S \<inter> T); context_gabi S G G' \<rbrakk>
    \<Longrightarrow> G' \<turnstile> \<langle>c', xs\<rangle> \<Rightarrow> xs' \<and> xs' \<in> xstate_inv_set S" proof (induct arbitrary: c' T rule: exec.induct) case (Call proc bdy s t) show ?case using Call.prems Call.hyps by - (gs_case \<open>drule_tac x=proc in spec\<close> g_def: context_gabi_def) next case (CallUndefined proc s t) show ?case using CallUndefined.prems CallUndefined.hyps by - (gs_case \<open>drule_tac x=proc in spec\<close> g_def: context_gabi_def) next case (WhileTrue s S c s' t) show ?case using WhileTrue.prems WhileTrue.hyps by - (gs_case \<open>(erule_tac x=UNIV in meta_allE)+\<close>) qed gs_simple_cases

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>G\<turnstile> \<langle>c,xs\<rangle> \<Rightarrow> xs'; guards_adjust_by_invariant S T c c'; xs \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',xs\<rangle> \<Rightarrow> xs' \<and> xs' \<in> xstate_inv_set S proof (state)
goal (20 subgoals):
 1. \<And>s c' T. \<lbrakk>guards_adjust_by_invariant S T SKIP c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> Normal s \<and> Normal s \<in> xstate_inv_set S
 2. \<And>s g c t f c' T. \<lbrakk>s \<in> g; G\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> t; \<And>c' T. \<lbrakk>guards_adjust_by_invariant S T c c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S; guards_adjust_by_invariant S T (Guard f g c) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S
 3. \<And>s g f c c' T. \<lbrakk>s \<notin> g; guards_adjust_by_invariant S T (Guard f g c) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> Fault f \<and> Fault f \<in> xstate_inv_set S
 4. \<And>c f c' T. \<lbrakk>guards_adjust_by_invariant S T c c'; Fault f \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Fault f\<rangle> \<Rightarrow> Fault f \<and> Fault f \<in> xstate_inv_set S
 5. \<And>f s c' T. \<lbrakk>guards_adjust_by_invariant S T (Basic f) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> Normal (f s) \<and> Normal (f s) \<in> xstate_inv_set S
 6. \<And>s t r c' T. \<lbrakk>(s, t) \<in> r; guards_adjust_by_invariant S T (Spec r) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> Normal t \<and> Normal t \<in> xstate_inv_set S
 7. \<And>s r c' T. \<lbrakk>\<forall>t. (s, t) \<notin> r; guards_adjust_by_invariant S T (Spec r) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> Stuck \<and> Stuck \<in> xstate_inv_set S
 8. \<And>c\<^sub>1 s s' c\<^sub>2 t c' T. \<lbrakk>G\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> s'; \<And>c' T. \<lbrakk>guards_adjust_by_invariant S T c\<^sub>1 c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> s' \<and> s' \<in> xstate_inv_set S; G\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> t; \<And>c' T. \<lbrakk>guards_adjust_by_invariant S T c\<^sub>2 c'; s' \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',s'\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S; guards_adjust_by_invariant S T (c\<^sub>1;;
c\<^sub>2) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S
 9. \<And>s b c\<^sub>1 t c\<^sub>2 c' T. \<lbrakk>s \<in> b; G\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>c' T. \<lbrakk>guards_adjust_by_invariant S T c\<^sub>1 c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S; guards_adjust_by_invariant S T (Cond b c\<^sub>1 c\<^sub>2) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S
 10. \<And>s b c\<^sub>2 t c\<^sub>1 c' T. \<lbrakk>s \<notin> b; G\<turnstile> \<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> t; \<And>c' T. \<lbrakk>guards_adjust_by_invariant S T c\<^sub>2 c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S; guards_adjust_by_invariant S T (Cond b c\<^sub>1 c\<^sub>2) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S
A total of 20 subgoals... proof (state)
this:
G proc = Some bdy
G\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> t
\<lbrakk>guards_adjust_by_invariant S ?T bdy ?c'; Normal s \<in> xstate_inv_set (S \<inter> ?T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>?c',Normal s\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S
guards_adjust_by_invariant S T (Call proc) c'
Normal s \<in> xstate_inv_set (S \<inter> T)
context_gabi S G G'

goal (20 subgoals):
 1. \<And>s c' T. \<lbrakk>guards_adjust_by_invariant S T SKIP c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> Normal s \<and> Normal s \<in> xstate_inv_set S
 2. \<And>s g c t f c' T. \<lbrakk>s \<in> g; G\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> t; \<And>c' T. \<lbrakk>guards_adjust_by_invariant S T c c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S; guards_adjust_by_invariant S T (Guard f g c) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S
 3. \<And>s g f c c' T. \<lbrakk>s \<notin> g; guards_adjust_by_invariant S T (Guard f g c) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> Fault f \<and> Fault f \<in> xstate_inv_set S
 4. \<And>c f c' T. \<lbrakk>guards_adjust_by_invariant S T c c'; Fault f \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Fault f\<rangle> \<Rightarrow> Fault f \<and> Fault f \<in> xstate_inv_set S
 5. \<And>f s c' T. \<lbrakk>guards_adjust_by_invariant S T (Basic f) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> Normal (f s) \<and> Normal (f s) \<in> xstate_inv_set S
 6. \<And>s t r c' T. \<lbrakk>(s, t) \<in> r; guards_adjust_by_invariant S T (Spec r) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> Normal t \<and> Normal t \<in> xstate_inv_set S
 7. \<And>s r c' T. \<lbrakk>\<forall>t. (s, t) \<notin> r; guards_adjust_by_invariant S T (Spec r) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> Stuck \<and> Stuck \<in> xstate_inv_set S
 8. \<And>c\<^sub>1 s s' c\<^sub>2 t c' T. \<lbrakk>G\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> s'; \<And>c' T. \<lbrakk>guards_adjust_by_invariant S T c\<^sub>1 c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> s' \<and> s' \<in> xstate_inv_set S; G\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> t; \<And>c' T. \<lbrakk>guards_adjust_by_invariant S T c\<^sub>2 c'; s' \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',s'\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S; guards_adjust_by_invariant S T (c\<^sub>1;;
c\<^sub>2) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S
 9. \<And>s b c\<^sub>1 t c\<^sub>2 c' T. \<lbrakk>s \<in> b; G\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>c' T. \<lbrakk>guards_adjust_by_invariant S T c\<^sub>1 c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S; guards_adjust_by_invariant S T (Cond b c\<^sub>1 c\<^sub>2) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S
 10. \<And>s b c\<^sub>2 t c\<^sub>1 c' T. \<lbrakk>s \<notin> b; G\<turnstile> \<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> t; \<And>c' T. \<lbrakk>guards_adjust_by_invariant S T c\<^sub>2 c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S; guards_adjust_by_invariant S T (Cond b c\<^sub>1 c\<^sub>2) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S
A total of 20 subgoals... proof (prove)
goal (1 subgoal):
 1. G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S proof (prove)
using this:
guards_adjust_by_invariant S T (Call proc) c'
Normal s \<in> xstate_inv_set (S \<inter> T)
context_gabi S G G'
G proc = Some bdy
G\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> t
\<lbrakk>guards_adjust_by_invariant S ?T bdy ?c'; Normal s \<in> xstate_inv_set (S \<inter> ?T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>?c',Normal s\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S

goal (1 subgoal):
 1. G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S proof (state)
this:
G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S

goal (19 subgoals):
 1. \<And>s c' T. \<lbrakk>guards_adjust_by_invariant S T SKIP c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> Normal s \<and> Normal s \<in> xstate_inv_set S
 2. \<And>s g c t f c' T. \<lbrakk>s \<in> g; G\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> t; \<And>c' T. \<lbrakk>guards_adjust_by_invariant S T c c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S; guards_adjust_by_invariant S T (Guard f g c) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S
 3. \<And>s g f c c' T. \<lbrakk>s \<notin> g; guards_adjust_by_invariant S T (Guard f g c) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> Fault f \<and> Fault f \<in> xstate_inv_set S
 4. \<And>c f c' T. \<lbrakk>guards_adjust_by_invariant S T c c'; Fault f \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Fault f\<rangle> \<Rightarrow> Fault f \<and> Fault f \<in> xstate_inv_set S
 5. \<And>f s c' T. \<lbrakk>guards_adjust_by_invariant S T (Basic f) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> Normal (f s) \<and> Normal (f s) \<in> xstate_inv_set S
 6. \<And>s t r c' T. \<lbrakk>(s, t) \<in> r; guards_adjust_by_invariant S T (Spec r) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> Normal t \<and> Normal t \<in> xstate_inv_set S
 7. \<And>s r c' T. \<lbrakk>\<forall>t. (s, t) \<notin> r; guards_adjust_by_invariant S T (Spec r) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> Stuck \<and> Stuck \<in> xstate_inv_set S
 8. \<And>c\<^sub>1 s s' c\<^sub>2 t c' T. \<lbrakk>G\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> s'; \<And>c' T. \<lbrakk>guards_adjust_by_invariant S T c\<^sub>1 c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> s' \<and> s' \<in> xstate_inv_set S; G\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> t; \<And>c' T. \<lbrakk>guards_adjust_by_invariant S T c\<^sub>2 c'; s' \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',s'\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S; guards_adjust_by_invariant S T (c\<^sub>1;;
c\<^sub>2) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S
 9. \<And>s b c\<^sub>1 t c\<^sub>2 c' T. \<lbrakk>s \<in> b; G\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>c' T. \<lbrakk>guards_adjust_by_invariant S T c\<^sub>1 c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S; guards_adjust_by_invariant S T (Cond b c\<^sub>1 c\<^sub>2) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S
 10. \<And>s b c\<^sub>2 t c\<^sub>1 c' T. \<lbrakk>s \<notin> b; G\<turnstile> \<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> t; \<And>c' T. \<lbrakk>guards_adjust_by_invariant S T c\<^sub>2 c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S; guards_adjust_by_invariant S T (Cond b c\<^sub>1 c\<^sub>2) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S
A total of 19 subgoals... proof (state)
goal (19 subgoals):
 1. \<And>s c' T. \<lbrakk>guards_adjust_by_invariant S T SKIP c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> Normal s \<and> Normal s \<in> xstate_inv_set S
 2. \<And>s g c t f c' T. \<lbrakk>s \<in> g; G\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> t; \<And>c' T. \<lbrakk>guards_adjust_by_invariant S T c c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S; guards_adjust_by_invariant S T (Guard f g c) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S
 3. \<And>s g f c c' T. \<lbrakk>s \<notin> g; guards_adjust_by_invariant S T (Guard f g c) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> Fault f \<and> Fault f \<in> xstate_inv_set S
 4. \<And>c f c' T. \<lbrakk>guards_adjust_by_invariant S T c c'; Fault f \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Fault f\<rangle> \<Rightarrow> Fault f \<and> Fault f \<in> xstate_inv_set S
 5. \<And>f s c' T. \<lbrakk>guards_adjust_by_invariant S T (Basic f) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> Normal (f s) \<and> Normal (f s) \<in> xstate_inv_set S
 6. \<And>s t r c' T. \<lbrakk>(s, t) \<in> r; guards_adjust_by_invariant S T (Spec r) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> Normal t \<and> Normal t \<in> xstate_inv_set S
 7. \<And>s r c' T. \<lbrakk>\<forall>t. (s, t) \<notin> r; guards_adjust_by_invariant S T (Spec r) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> Stuck \<and> Stuck \<in> xstate_inv_set S
 8. \<And>c\<^sub>1 s s' c\<^sub>2 t c' T. \<lbrakk>G\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> s'; \<And>c' T. \<lbrakk>guards_adjust_by_invariant S T c\<^sub>1 c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> s' \<and> s' \<in> xstate_inv_set S; G\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> t; \<And>c' T. \<lbrakk>guards_adjust_by_invariant S T c\<^sub>2 c'; s' \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',s'\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S; guards_adjust_by_invariant S T (c\<^sub>1;;
c\<^sub>2) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S
 9. \<And>s b c\<^sub>1 t c\<^sub>2 c' T. \<lbrakk>s \<in> b; G\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>c' T. \<lbrakk>guards_adjust_by_invariant S T c\<^sub>1 c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S; guards_adjust_by_invariant S T (Cond b c\<^sub>1 c\<^sub>2) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S
 10. \<And>s b c\<^sub>2 t c\<^sub>1 c' T. \<lbrakk>s \<notin> b; G\<turnstile> \<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> t; \<And>c' T. \<lbrakk>guards_adjust_by_invariant S T c\<^sub>2 c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S; guards_adjust_by_invariant S T (Cond b c\<^sub>1 c\<^sub>2) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S
A total of 19 subgoals... proof (state)
this:
G proc = None
guards_adjust_by_invariant S T (Call proc) t
Normal s \<in> xstate_inv_set (S \<inter> T)
context_gabi S G G'

goal (19 subgoals):
 1. \<And>s c' T. \<lbrakk>guards_adjust_by_invariant S T SKIP c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> Normal s \<and> Normal s \<in> xstate_inv_set S
 2. \<And>s g c t f c' T. \<lbrakk>s \<in> g; G\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> t; \<And>c' T. \<lbrakk>guards_adjust_by_invariant S T c c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S; guards_adjust_by_invariant S T (Guard f g c) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S
 3. \<And>s g f c c' T. \<lbrakk>s \<notin> g; guards_adjust_by_invariant S T (Guard f g c) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> Fault f \<and> Fault f \<in> xstate_inv_set S
 4. \<And>c f c' T. \<lbrakk>guards_adjust_by_invariant S T c c'; Fault f \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Fault f\<rangle> \<Rightarrow> Fault f \<and> Fault f \<in> xstate_inv_set S
 5. \<And>f s c' T. \<lbrakk>guards_adjust_by_invariant S T (Basic f) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> Normal (f s) \<and> Normal (f s) \<in> xstate_inv_set S
 6. \<And>s t r c' T. \<lbrakk>(s, t) \<in> r; guards_adjust_by_invariant S T (Spec r) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> Normal t \<and> Normal t \<in> xstate_inv_set S
 7. \<And>s r c' T. \<lbrakk>\<forall>t. (s, t) \<notin> r; guards_adjust_by_invariant S T (Spec r) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> Stuck \<and> Stuck \<in> xstate_inv_set S
 8. \<And>c\<^sub>1 s s' c\<^sub>2 t c' T. \<lbrakk>G\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> s'; \<And>c' T. \<lbrakk>guards_adjust_by_invariant S T c\<^sub>1 c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> s' \<and> s' \<in> xstate_inv_set S; G\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> t; \<And>c' T. \<lbrakk>guards_adjust_by_invariant S T c\<^sub>2 c'; s' \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',s'\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S; guards_adjust_by_invariant S T (c\<^sub>1;;
c\<^sub>2) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S
 9. \<And>s b c\<^sub>1 t c\<^sub>2 c' T. \<lbrakk>s \<in> b; G\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>c' T. \<lbrakk>guards_adjust_by_invariant S T c\<^sub>1 c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S; guards_adjust_by_invariant S T (Cond b c\<^sub>1 c\<^sub>2) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S
 10. \<And>s b c\<^sub>2 t c\<^sub>1 c' T. \<lbrakk>s \<notin> b; G\<turnstile> \<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> t; \<And>c' T. \<lbrakk>guards_adjust_by_invariant S T c\<^sub>2 c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S; guards_adjust_by_invariant S T (Cond b c\<^sub>1 c\<^sub>2) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S
A total of 19 subgoals... proof (prove)
goal (1 subgoal):
 1. G'\<turnstile> \<langle>t,Normal s\<rangle> \<Rightarrow> Stuck \<and> Stuck \<in> xstate_inv_set S proof (prove)
using this:
guards_adjust_by_invariant S T (Call proc) t
Normal s \<in> xstate_inv_set (S \<inter> T)
context_gabi S G G'
G proc = None

goal (1 subgoal):
 1. G'\<turnstile> \<langle>t,Normal s\<rangle> \<Rightarrow> Stuck \<and> Stuck \<in> xstate_inv_set S proof (state)
this:
G'\<turnstile> \<langle>t,Normal s\<rangle> \<Rightarrow> Stuck \<and> Stuck \<in> xstate_inv_set S

goal (18 subgoals):
 1. \<And>s c' T. \<lbrakk>guards_adjust_by_invariant S T SKIP c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> Normal s \<and> Normal s \<in> xstate_inv_set S
 2. \<And>s g c t f c' T. \<lbrakk>s \<in> g; G\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> t; \<And>c' T. \<lbrakk>guards_adjust_by_invariant S T c c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S; guards_adjust_by_invariant S T (Guard f g c) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S
 3. \<And>s g f c c' T. \<lbrakk>s \<notin> g; guards_adjust_by_invariant S T (Guard f g c) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> Fault f \<and> Fault f \<in> xstate_inv_set S
 4. \<And>c f c' T. \<lbrakk>guards_adjust_by_invariant S T c c'; Fault f \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Fault f\<rangle> \<Rightarrow> Fault f \<and> Fault f \<in> xstate_inv_set S
 5. \<And>f s c' T. \<lbrakk>guards_adjust_by_invariant S T (Basic f) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> Normal (f s) \<and> Normal (f s) \<in> xstate_inv_set S
 6. \<And>s t r c' T. \<lbrakk>(s, t) \<in> r; guards_adjust_by_invariant S T (Spec r) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> Normal t \<and> Normal t \<in> xstate_inv_set S
 7. \<And>s r c' T. \<lbrakk>\<forall>t. (s, t) \<notin> r; guards_adjust_by_invariant S T (Spec r) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> Stuck \<and> Stuck \<in> xstate_inv_set S
 8. \<And>c\<^sub>1 s s' c\<^sub>2 t c' T. \<lbrakk>G\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> s'; \<And>c' T. \<lbrakk>guards_adjust_by_invariant S T c\<^sub>1 c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> s' \<and> s' \<in> xstate_inv_set S; G\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> t; \<And>c' T. \<lbrakk>guards_adjust_by_invariant S T c\<^sub>2 c'; s' \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',s'\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S; guards_adjust_by_invariant S T (c\<^sub>1;;
c\<^sub>2) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S
 9. \<And>s b c\<^sub>1 t c\<^sub>2 c' T. \<lbrakk>s \<in> b; G\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>c' T. \<lbrakk>guards_adjust_by_invariant S T c\<^sub>1 c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S; guards_adjust_by_invariant S T (Cond b c\<^sub>1 c\<^sub>2) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S
 10. \<And>s b c\<^sub>2 t c\<^sub>1 c' T. \<lbrakk>s \<notin> b; G\<turnstile> \<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> t; \<And>c' T. \<lbrakk>guards_adjust_by_invariant S T c\<^sub>2 c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S; guards_adjust_by_invariant S T (Cond b c\<^sub>1 c\<^sub>2) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S
A total of 18 subgoals... proof (state)
goal (18 subgoals):
 1. \<And>s c' T. \<lbrakk>guards_adjust_by_invariant S T SKIP c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> Normal s \<and> Normal s \<in> xstate_inv_set S
 2. \<And>s g c t f c' T. \<lbrakk>s \<in> g; G\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> t; \<And>c' T. \<lbrakk>guards_adjust_by_invariant S T c c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S; guards_adjust_by_invariant S T (Guard f g c) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S
 3. \<And>s g f c c' T. \<lbrakk>s \<notin> g; guards_adjust_by_invariant S T (Guard f g c) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> Fault f \<and> Fault f \<in> xstate_inv_set S
 4. \<And>c f c' T. \<lbrakk>guards_adjust_by_invariant S T c c'; Fault f \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Fault f\<rangle> \<Rightarrow> Fault f \<and> Fault f \<in> xstate_inv_set S
 5. \<And>f s c' T. \<lbrakk>guards_adjust_by_invariant S T (Basic f) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> Normal (f s) \<and> Normal (f s) \<in> xstate_inv_set S
 6. \<And>s t r c' T. \<lbrakk>(s, t) \<in> r; guards_adjust_by_invariant S T (Spec r) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> Normal t \<and> Normal t \<in> xstate_inv_set S
 7. \<And>s r c' T. \<lbrakk>\<forall>t. (s, t) \<notin> r; guards_adjust_by_invariant S T (Spec r) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> Stuck \<and> Stuck \<in> xstate_inv_set S
 8. \<And>c\<^sub>1 s s' c\<^sub>2 t c' T. \<lbrakk>G\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> s'; \<And>c' T. \<lbrakk>guards_adjust_by_invariant S T c\<^sub>1 c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> s' \<and> s' \<in> xstate_inv_set S; G\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> t; \<And>c' T. \<lbrakk>guards_adjust_by_invariant S T c\<^sub>2 c'; s' \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',s'\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S; guards_adjust_by_invariant S T (c\<^sub>1;;
c\<^sub>2) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S
 9. \<And>s b c\<^sub>1 t c\<^sub>2 c' T. \<lbrakk>s \<in> b; G\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>c' T. \<lbrakk>guards_adjust_by_invariant S T c\<^sub>1 c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S; guards_adjust_by_invariant S T (Cond b c\<^sub>1 c\<^sub>2) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S
 10. \<And>s b c\<^sub>2 t c\<^sub>1 c' T. \<lbrakk>s \<notin> b; G\<turnstile> \<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> t; \<And>c' T. \<lbrakk>guards_adjust_by_invariant S T c\<^sub>2 c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S; guards_adjust_by_invariant S T (Cond b c\<^sub>1 c\<^sub>2) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S
A total of 18 subgoals... proof (state)
this:
s \<in> S
G\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> s'
\<lbrakk>guards_adjust_by_invariant S ?T c ?c'; Normal s \<in> xstate_inv_set (S \<inter> ?T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>?c',Normal s\<rangle> \<Rightarrow> s' \<and> s' \<in> xstate_inv_set S
G\<turnstile> \<langle>While S c,s'\<rangle> \<Rightarrow> t
\<lbrakk>guards_adjust_by_invariant S ?T (While S c) ?c'; s' \<in> xstate_inv_set (S \<inter> ?T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>?c',s'\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S
guards_adjust_by_invariant S T (While S c) c'
Normal s \<in> xstate_inv_set (S \<inter> T)
context_gabi S G G'

goal (18 subgoals):
 1. \<And>s c' T. \<lbrakk>guards_adjust_by_invariant S T SKIP c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> Normal s \<and> Normal s \<in> xstate_inv_set S
 2. \<And>s g c t f c' T. \<lbrakk>s \<in> g; G\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> t; \<And>c' T. \<lbrakk>guards_adjust_by_invariant S T c c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S; guards_adjust_by_invariant S T (Guard f g c) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S
 3. \<And>s g f c c' T. \<lbrakk>s \<notin> g; guards_adjust_by_invariant S T (Guard f g c) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> Fault f \<and> Fault f \<in> xstate_inv_set S
 4. \<And>c f c' T. \<lbrakk>guards_adjust_by_invariant S T c c'; Fault f \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Fault f\<rangle> \<Rightarrow> Fault f \<and> Fault f \<in> xstate_inv_set S
 5. \<And>f s c' T. \<lbrakk>guards_adjust_by_invariant S T (Basic f) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> Normal (f s) \<and> Normal (f s) \<in> xstate_inv_set S
 6. \<And>s t r c' T. \<lbrakk>(s, t) \<in> r; guards_adjust_by_invariant S T (Spec r) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> Normal t \<and> Normal t \<in> xstate_inv_set S
 7. \<And>s r c' T. \<lbrakk>\<forall>t. (s, t) \<notin> r; guards_adjust_by_invariant S T (Spec r) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> Stuck \<and> Stuck \<in> xstate_inv_set S
 8. \<And>c\<^sub>1 s s' c\<^sub>2 t c' T. \<lbrakk>G\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> s'; \<And>c' T. \<lbrakk>guards_adjust_by_invariant S T c\<^sub>1 c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> s' \<and> s' \<in> xstate_inv_set S; G\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> t; \<And>c' T. \<lbrakk>guards_adjust_by_invariant S T c\<^sub>2 c'; s' \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',s'\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S; guards_adjust_by_invariant S T (c\<^sub>1;;
c\<^sub>2) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S
 9. \<And>s b c\<^sub>1 t c\<^sub>2 c' T. \<lbrakk>s \<in> b; G\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>c' T. \<lbrakk>guards_adjust_by_invariant S T c\<^sub>1 c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S; guards_adjust_by_invariant S T (Cond b c\<^sub>1 c\<^sub>2) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S
 10. \<And>s b c\<^sub>2 t c\<^sub>1 c' T. \<lbrakk>s \<notin> b; G\<turnstile> \<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> t; \<And>c' T. \<lbrakk>guards_adjust_by_invariant S T c\<^sub>2 c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S; guards_adjust_by_invariant S T (Cond b c\<^sub>1 c\<^sub>2) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S
A total of 18 subgoals... proof (prove)
goal (1 subgoal):
 1. G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S proof (prove)
using this:
guards_adjust_by_invariant S T (While S c) c'
Normal s \<in> xstate_inv_set (S \<inter> T)
context_gabi S G G'
s \<in> S
G\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> s'
\<lbrakk>guards_adjust_by_invariant S ?T c ?c'; Normal s \<in> xstate_inv_set (S \<inter> ?T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>?c',Normal s\<rangle> \<Rightarrow> s' \<and> s' \<in> xstate_inv_set S
G\<turnstile> \<langle>While S c,s'\<rangle> \<Rightarrow> t
\<lbrakk>guards_adjust_by_invariant S ?T (While S c) ?c'; s' \<in> xstate_inv_set (S \<inter> ?T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>?c',s'\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S

goal (1 subgoal):
 1. G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S proof (state)
this:
G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S

goal (17 subgoals):
 1. \<And>s c' T. \<lbrakk>guards_adjust_by_invariant S T SKIP c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> Normal s \<and> Normal s \<in> xstate_inv_set S
 2. \<And>s g c t f c' T. \<lbrakk>s \<in> g; G\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> t; \<And>c' T. \<lbrakk>guards_adjust_by_invariant S T c c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S; guards_adjust_by_invariant S T (Guard f g c) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S
 3. \<And>s g f c c' T. \<lbrakk>s \<notin> g; guards_adjust_by_invariant S T (Guard f g c) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> Fault f \<and> Fault f \<in> xstate_inv_set S
 4. \<And>c f c' T. \<lbrakk>guards_adjust_by_invariant S T c c'; Fault f \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Fault f\<rangle> \<Rightarrow> Fault f \<and> Fault f \<in> xstate_inv_set S
 5. \<And>f s c' T. \<lbrakk>guards_adjust_by_invariant S T (Basic f) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> Normal (f s) \<and> Normal (f s) \<in> xstate_inv_set S
 6. \<And>s t r c' T. \<lbrakk>(s, t) \<in> r; guards_adjust_by_invariant S T (Spec r) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> Normal t \<and> Normal t \<in> xstate_inv_set S
 7. \<And>s r c' T. \<lbrakk>\<forall>t. (s, t) \<notin> r; guards_adjust_by_invariant S T (Spec r) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> Stuck \<and> Stuck \<in> xstate_inv_set S
 8. \<And>c\<^sub>1 s s' c\<^sub>2 t c' T. \<lbrakk>G\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> s'; \<And>c' T. \<lbrakk>guards_adjust_by_invariant S T c\<^sub>1 c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> s' \<and> s' \<in> xstate_inv_set S; G\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> t; \<And>c' T. \<lbrakk>guards_adjust_by_invariant S T c\<^sub>2 c'; s' \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',s'\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S; guards_adjust_by_invariant S T (c\<^sub>1;;
c\<^sub>2) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S
 9. \<And>s b c\<^sub>1 t c\<^sub>2 c' T. \<lbrakk>s \<in> b; G\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; \<And>c' T. \<lbrakk>guards_adjust_by_invariant S T c\<^sub>1 c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S; guards_adjust_by_invariant S T (Cond b c\<^sub>1 c\<^sub>2) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S
 10. \<And>s b c\<^sub>2 t c\<^sub>1 c' T. \<lbrakk>s \<notin> b; G\<turnstile> \<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> t; \<And>c' T. \<lbrakk>guards_adjust_by_invariant S T c\<^sub>2 c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S; guards_adjust_by_invariant S T (Cond b c\<^sub>1 c\<^sub>2) c'; Normal s \<in> xstate_inv_set (S \<inter> T); context_gabi S G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c',Normal s\<rangle> \<Rightarrow> t \<and> t \<in> xstate_inv_set S
A total of 17 subgoals...