theory Ctac

lemma call_ceqv_hoarep_gen:
  assumes mod: "\<forall>s. \<Gamma>\<turnstile>\<^bsub>/F s\<^esub> (P s) Call f (Q s),(A s)"
  assumes ieq: "\<And>s. rewrite_xf xf s v i i'"
  and    ceqv: "\<And>t t' s'. ceqv \<Gamma> xf v (r t s') t' (c t s') (c' t s')"
  and     xf:  "\<And>s t. xf s = v \<Longrightarrow> i' s \<in> P (x s) \<longrightarrow> t \<in> Q (x s) \<or> t \<in> A (x s) \<Longrightarrow> xf (r s t) = v"
  shows   "ceqv \<Gamma> xf v t t' (call i f r c) (call i' f r c')" apply (rule ceqvI) apply (rule iffI) apply (erule exec_call_Normal_elim) apply (drule ceqvD1[OF _ _ ceqv]) apply (simp add: rewrite_xfD[OF ieq]) apply (erule xf) apply (frule (1) hoarep_exec_call_body[OF mod], fastforce) apply (erule exec_call) apply (simp add: rewrite_xfD[OF ieq]) apply assumption apply (clarsimp simp: rewrite_xfD[OF ieq] elim!: exec_callAbrupt) apply (clarsimp simp: rewrite_xfD[OF ieq] elim!: exec_callFault) apply (clarsimp simp: rewrite_xfD[OF ieq] elim!: exec_callStuck) apply (clarsimp simp: rewrite_xfD[OF ieq] elim!: exec_callUndefined) apply (erule exec_call_Normal_elim) apply (drule ceqvD2 [OF _ _ ceqv]) apply (erule xf) apply (frule (1) hoarep_exec_call_body[OF mod], fastforce) apply (erule exec_call) apply (simp add: rewrite_xfD[OF ieq]) apply assumption apply (clarsimp simp: rewrite_xfD[OF ieq] elim!: exec_callAbrupt) apply (clarsimp simp: rewrite_xfD[OF ieq] elim!: exec_callFault) apply (clarsimp simp: rewrite_xfD[OF ieq] elim!: exec_callStuck) apply (clarsimp simp: rewrite_xfD[OF ieq] elim!: exec_callUndefined) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ceqv \<Gamma> xf v t t' (call i f r c) (call i' f r c') proof (prove)
goal (1 subgoal):
 1. xf t = v \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i f r c,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>call i' f r c',Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>call i f r c,Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i' f r c',Normal t\<rangle> \<Rightarrow> t'
 2. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>call i' f r c',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i f r c,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (6 subgoals):
 1. \<And>bdy t'a. \<lbrakk>xf t = v; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i t)\<rangle> \<Rightarrow> Normal t'a; \<Gamma>\<turnstile> \<langle>c t t'a,Normal (r t t'a)\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i' f r c',Normal t\<rangle> \<Rightarrow> t'
 2. \<And>bdy t'a. \<lbrakk>xf t = v; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i t)\<rangle> \<Rightarrow> Abrupt t'a; t' = Abrupt (r t t'a)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i' f r c',Normal t\<rangle> \<Rightarrow> t'
 3. \<And>bdy fa. \<lbrakk>xf t = v; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i t)\<rangle> \<Rightarrow> Fault fa; t' = Fault fa\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i' f r c',Normal t\<rangle> \<Rightarrow> t'
 4. \<And>bdy. \<lbrakk>xf t = v; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i t)\<rangle> \<Rightarrow> Stuck; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i' f r c',Normal t\<rangle> \<Rightarrow> t'
 5. \<lbrakk>xf t = v; \<Gamma> f = None; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i' f r c',Normal t\<rangle> \<Rightarrow> t'
 6. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>call i' f r c',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i f r c,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (7 subgoals):
 1. \<And>bdy t'. \<lbrakk>xf t = v; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i t)\<rangle> \<Rightarrow> Normal t'\<rbrakk> \<Longrightarrow> xf (r t t') = v
 2. \<And>bdy t'a. \<lbrakk>xf t = v; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i t)\<rangle> \<Rightarrow> Normal t'a; \<Gamma>\<turnstile> \<langle>c' t t'a,Normal (r t t'a)\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i' f r c',Normal t\<rangle> \<Rightarrow> t'
 3. \<And>bdy t'a. \<lbrakk>xf t = v; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i t)\<rangle> \<Rightarrow> Abrupt t'a; t' = Abrupt (r t t'a)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i' f r c',Normal t\<rangle> \<Rightarrow> t'
 4. \<And>bdy fa. \<lbrakk>xf t = v; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i t)\<rangle> \<Rightarrow> Fault fa; t' = Fault fa\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i' f r c',Normal t\<rangle> \<Rightarrow> t'
 5. \<And>bdy. \<lbrakk>xf t = v; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i t)\<rangle> \<Rightarrow> Stuck; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i' f r c',Normal t\<rangle> \<Rightarrow> t'
 6. \<lbrakk>xf t = v; \<Gamma> f = None; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i' f r c',Normal t\<rangle> \<Rightarrow> t'
 7. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>call i' f r c',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i f r c,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (7 subgoals):
 1. \<And>bdy t'. \<lbrakk>xf t = v; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i' t)\<rangle> \<Rightarrow> Normal t'\<rbrakk> \<Longrightarrow> xf (r t t') = v
 2. \<And>bdy t'a. \<lbrakk>xf t = v; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i t)\<rangle> \<Rightarrow> Normal t'a; \<Gamma>\<turnstile> \<langle>c' t t'a,Normal (r t t'a)\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i' f r c',Normal t\<rangle> \<Rightarrow> t'
 3. \<And>bdy t'a. \<lbrakk>xf t = v; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i t)\<rangle> \<Rightarrow> Abrupt t'a; t' = Abrupt (r t t'a)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i' f r c',Normal t\<rangle> \<Rightarrow> t'
 4. \<And>bdy fa. \<lbrakk>xf t = v; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i t)\<rangle> \<Rightarrow> Fault fa; t' = Fault fa\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i' f r c',Normal t\<rangle> \<Rightarrow> t'
 5. \<And>bdy. \<lbrakk>xf t = v; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i t)\<rangle> \<Rightarrow> Stuck; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i' f r c',Normal t\<rangle> \<Rightarrow> t'
 6. \<lbrakk>xf t = v; \<Gamma> f = None; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i' f r c',Normal t\<rangle> \<Rightarrow> t'
 7. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>call i' f r c',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i f r c,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (7 subgoals):
 1. \<And>bdy t'. \<lbrakk>\<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i' t)\<rangle> \<Rightarrow> Normal t'\<rbrakk> \<Longrightarrow> i' t \<in> P (x t) \<longrightarrow> t' \<in> Q (x t) \<or> t' \<in> A (x t)
 2. \<And>bdy t'a. \<lbrakk>xf t = v; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i t)\<rangle> \<Rightarrow> Normal t'a; \<Gamma>\<turnstile> \<langle>c' t t'a,Normal (r t t'a)\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i' f r c',Normal t\<rangle> \<Rightarrow> t'
 3. \<And>bdy t'a. \<lbrakk>xf t = v; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i t)\<rangle> \<Rightarrow> Abrupt t'a; t' = Abrupt (r t t'a)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i' f r c',Normal t\<rangle> \<Rightarrow> t'
 4. \<And>bdy fa. \<lbrakk>xf t = v; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i t)\<rangle> \<Rightarrow> Fault fa; t' = Fault fa\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i' f r c',Normal t\<rangle> \<Rightarrow> t'
 5. \<And>bdy. \<lbrakk>xf t = v; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i t)\<rangle> \<Rightarrow> Stuck; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i' f r c',Normal t\<rangle> \<Rightarrow> t'
 6. \<lbrakk>xf t = v; \<Gamma> f = None; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i' f r c',Normal t\<rangle> \<Rightarrow> t'
 7. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>call i' f r c',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i f r c,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (6 subgoals):
 1. \<And>bdy t'a. \<lbrakk>xf t = v; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i t)\<rangle> \<Rightarrow> Normal t'a; \<Gamma>\<turnstile> \<langle>c' t t'a,Normal (r t t'a)\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i' f r c',Normal t\<rangle> \<Rightarrow> t'
 2. \<And>bdy t'a. \<lbrakk>xf t = v; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i t)\<rangle> \<Rightarrow> Abrupt t'a; t' = Abrupt (r t t'a)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i' f r c',Normal t\<rangle> \<Rightarrow> t'
 3. \<And>bdy fa. \<lbrakk>xf t = v; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i t)\<rangle> \<Rightarrow> Fault fa; t' = Fault fa\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i' f r c',Normal t\<rangle> \<Rightarrow> t'
 4. \<And>bdy. \<lbrakk>xf t = v; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i t)\<rangle> \<Rightarrow> Stuck; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i' f r c',Normal t\<rangle> \<Rightarrow> t'
 5. \<lbrakk>xf t = v; \<Gamma> f = None; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i' f r c',Normal t\<rangle> \<Rightarrow> t'
 6. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>call i' f r c',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i f r c,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (7 subgoals):
 1. \<And>bdy t'a. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>bdy,Normal (i t)\<rangle> \<Rightarrow> Normal t'a; \<Gamma>\<turnstile> \<langle>c' t t'a,Normal (r t t'a)\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>bdy,Normal (i' t)\<rangle> \<Rightarrow> Normal (?t34 bdy t'a)
 2. \<And>bdy t'a. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>bdy,Normal (i t)\<rangle> \<Rightarrow> Normal t'a; \<Gamma>\<turnstile> \<langle>c' t t'a,Normal (r t t'a)\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>c' t (?t34 bdy t'a),Normal (r t (?t34 bdy t'a))\<rangle> \<Rightarrow> t'
 3. \<And>bdy t'a. \<lbrakk>xf t = v; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i t)\<rangle> \<Rightarrow> Abrupt t'a; t' = Abrupt (r t t'a)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i' f r c',Normal t\<rangle> \<Rightarrow> t'
 4. \<And>bdy fa. \<lbrakk>xf t = v; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i t)\<rangle> \<Rightarrow> Fault fa; t' = Fault fa\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i' f r c',Normal t\<rangle> \<Rightarrow> t'
 5. \<And>bdy. \<lbrakk>xf t = v; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i t)\<rangle> \<Rightarrow> Stuck; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i' f r c',Normal t\<rangle> \<Rightarrow> t'
 6. \<lbrakk>xf t = v; \<Gamma> f = None; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i' f r c',Normal t\<rangle> \<Rightarrow> t'
 7. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>call i' f r c',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i f r c,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (6 subgoals):
 1. \<And>bdy t'a. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>bdy,Normal (i t)\<rangle> \<Rightarrow> Normal t'a; \<Gamma>\<turnstile> \<langle>c' t t'a,Normal (r t t'a)\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>c' t t'a,Normal (r t t'a)\<rangle> \<Rightarrow> t'
 2. \<And>bdy t'a. \<lbrakk>xf t = v; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i t)\<rangle> \<Rightarrow> Abrupt t'a; t' = Abrupt (r t t'a)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i' f r c',Normal t\<rangle> \<Rightarrow> t'
 3. \<And>bdy fa. \<lbrakk>xf t = v; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i t)\<rangle> \<Rightarrow> Fault fa; t' = Fault fa\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i' f r c',Normal t\<rangle> \<Rightarrow> t'
 4. \<And>bdy. \<lbrakk>xf t = v; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i t)\<rangle> \<Rightarrow> Stuck; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i' f r c',Normal t\<rangle> \<Rightarrow> t'
 5. \<lbrakk>xf t = v; \<Gamma> f = None; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i' f r c',Normal t\<rangle> \<Rightarrow> t'
 6. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>call i' f r c',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i f r c,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (5 subgoals):
 1. \<And>bdy t'a. \<lbrakk>xf t = v; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i t)\<rangle> \<Rightarrow> Abrupt t'a; t' = Abrupt (r t t'a)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i' f r c',Normal t\<rangle> \<Rightarrow> t'
 2. \<And>bdy fa. \<lbrakk>xf t = v; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i t)\<rangle> \<Rightarrow> Fault fa; t' = Fault fa\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i' f r c',Normal t\<rangle> \<Rightarrow> t'
 3. \<And>bdy. \<lbrakk>xf t = v; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i t)\<rangle> \<Rightarrow> Stuck; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i' f r c',Normal t\<rangle> \<Rightarrow> t'
 4. \<lbrakk>xf t = v; \<Gamma> f = None; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i' f r c',Normal t\<rangle> \<Rightarrow> t'
 5. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>call i' f r c',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i f r c,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (4 subgoals):
 1. \<And>bdy fa. \<lbrakk>xf t = v; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i t)\<rangle> \<Rightarrow> Fault fa; t' = Fault fa\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i' f r c',Normal t\<rangle> \<Rightarrow> t'
 2. \<And>bdy. \<lbrakk>xf t = v; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i t)\<rangle> \<Rightarrow> Stuck; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i' f r c',Normal t\<rangle> \<Rightarrow> t'
 3. \<lbrakk>xf t = v; \<Gamma> f = None; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i' f r c',Normal t\<rangle> \<Rightarrow> t'
 4. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>call i' f r c',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i f r c,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (3 subgoals):
 1. \<And>bdy. \<lbrakk>xf t = v; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i t)\<rangle> \<Rightarrow> Stuck; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i' f r c',Normal t\<rangle> \<Rightarrow> t'
 2. \<lbrakk>xf t = v; \<Gamma> f = None; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i' f r c',Normal t\<rangle> \<Rightarrow> t'
 3. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>call i' f r c',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i f r c,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>xf t = v; \<Gamma> f = None; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i' f r c',Normal t\<rangle> \<Rightarrow> t'
 2. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>call i' f r c',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i f r c,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>call i' f r c',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i f r c,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (5 subgoals):
 1. \<And>bdy t'a. \<lbrakk>xf t = v; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i' t)\<rangle> \<Rightarrow> Normal t'a; \<Gamma>\<turnstile> \<langle>c' t t'a,Normal (r t t'a)\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i f r c,Normal t\<rangle> \<Rightarrow> t'
 2. \<And>bdy t'a. \<lbrakk>xf t = v; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i' t)\<rangle> \<Rightarrow> Abrupt t'a; t' = Abrupt (r t t'a)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i f r c,Normal t\<rangle> \<Rightarrow> t'
 3. \<And>bdy fa. \<lbrakk>xf t = v; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i' t)\<rangle> \<Rightarrow> Fault fa; t' = Fault fa\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i f r c,Normal t\<rangle> \<Rightarrow> t'
 4. \<And>bdy. \<lbrakk>xf t = v; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i' t)\<rangle> \<Rightarrow> Stuck; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i f r c,Normal t\<rangle> \<Rightarrow> t'
 5. \<lbrakk>xf t = v; \<Gamma> f = None; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i f r c,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (6 subgoals):
 1. \<And>bdy t'. \<lbrakk>xf t = v; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i' t)\<rangle> \<Rightarrow> Normal t'\<rbrakk> \<Longrightarrow> xf (r t t') = v
 2. \<And>bdy t'a. \<lbrakk>xf t = v; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i' t)\<rangle> \<Rightarrow> Normal t'a; \<Gamma>\<turnstile> \<langle>c t t'a,Normal (r t t'a)\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i f r c,Normal t\<rangle> \<Rightarrow> t'
 3. \<And>bdy t'a. \<lbrakk>xf t = v; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i' t)\<rangle> \<Rightarrow> Abrupt t'a; t' = Abrupt (r t t'a)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i f r c,Normal t\<rangle> \<Rightarrow> t'
 4. \<And>bdy fa. \<lbrakk>xf t = v; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i' t)\<rangle> \<Rightarrow> Fault fa; t' = Fault fa\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i f r c,Normal t\<rangle> \<Rightarrow> t'
 5. \<And>bdy. \<lbrakk>xf t = v; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i' t)\<rangle> \<Rightarrow> Stuck; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i f r c,Normal t\<rangle> \<Rightarrow> t'
 6. \<lbrakk>xf t = v; \<Gamma> f = None; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i f r c,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (6 subgoals):
 1. \<And>bdy t'. \<lbrakk>\<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i' t)\<rangle> \<Rightarrow> Normal t'\<rbrakk> \<Longrightarrow> i' t \<in> P (x t) \<longrightarrow> t' \<in> Q (x t) \<or> t' \<in> A (x t)
 2. \<And>bdy t'a. \<lbrakk>xf t = v; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i' t)\<rangle> \<Rightarrow> Normal t'a; \<Gamma>\<turnstile> \<langle>c t t'a,Normal (r t t'a)\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i f r c,Normal t\<rangle> \<Rightarrow> t'
 3. \<And>bdy t'a. \<lbrakk>xf t = v; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i' t)\<rangle> \<Rightarrow> Abrupt t'a; t' = Abrupt (r t t'a)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i f r c,Normal t\<rangle> \<Rightarrow> t'
 4. \<And>bdy fa. \<lbrakk>xf t = v; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i' t)\<rangle> \<Rightarrow> Fault fa; t' = Fault fa\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i f r c,Normal t\<rangle> \<Rightarrow> t'
 5. \<And>bdy. \<lbrakk>xf t = v; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i' t)\<rangle> \<Rightarrow> Stuck; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i f r c,Normal t\<rangle> \<Rightarrow> t'
 6. \<lbrakk>xf t = v; \<Gamma> f = None; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i f r c,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (5 subgoals):
 1. \<And>bdy t'a. \<lbrakk>xf t = v; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i' t)\<rangle> \<Rightarrow> Normal t'a; \<Gamma>\<turnstile> \<langle>c t t'a,Normal (r t t'a)\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i f r c,Normal t\<rangle> \<Rightarrow> t'
 2. \<And>bdy t'a. \<lbrakk>xf t = v; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i' t)\<rangle> \<Rightarrow> Abrupt t'a; t' = Abrupt (r t t'a)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i f r c,Normal t\<rangle> \<Rightarrow> t'
 3. \<And>bdy fa. \<lbrakk>xf t = v; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i' t)\<rangle> \<Rightarrow> Fault fa; t' = Fault fa\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i f r c,Normal t\<rangle> \<Rightarrow> t'
 4. \<And>bdy. \<lbrakk>xf t = v; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i' t)\<rangle> \<Rightarrow> Stuck; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i f r c,Normal t\<rangle> \<Rightarrow> t'
 5. \<lbrakk>xf t = v; \<Gamma> f = None; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i f r c,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (6 subgoals):
 1. \<And>bdy t'a. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>bdy,Normal (i' t)\<rangle> \<Rightarrow> Normal t'a; \<Gamma>\<turnstile> \<langle>c t t'a,Normal (r t t'a)\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>bdy,Normal (i t)\<rangle> \<Rightarrow> Normal (?t87 bdy t'a)
 2. \<And>bdy t'a. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>bdy,Normal (i' t)\<rangle> \<Rightarrow> Normal t'a; \<Gamma>\<turnstile> \<langle>c t t'a,Normal (r t t'a)\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>c t (?t87 bdy t'a),Normal (r t (?t87 bdy t'a))\<rangle> \<Rightarrow> t'
 3. \<And>bdy t'a. \<lbrakk>xf t = v; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i' t)\<rangle> \<Rightarrow> Abrupt t'a; t' = Abrupt (r t t'a)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i f r c,Normal t\<rangle> \<Rightarrow> t'
 4. \<And>bdy fa. \<lbrakk>xf t = v; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i' t)\<rangle> \<Rightarrow> Fault fa; t' = Fault fa\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i f r c,Normal t\<rangle> \<Rightarrow> t'
 5. \<And>bdy. \<lbrakk>xf t = v; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i' t)\<rangle> \<Rightarrow> Stuck; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i f r c,Normal t\<rangle> \<Rightarrow> t'
 6. \<lbrakk>xf t = v; \<Gamma> f = None; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i f r c,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (5 subgoals):
 1. \<And>bdy t'a. \<lbrakk>xf t = v; \<Gamma>\<turnstile> \<langle>bdy,Normal (i' t)\<rangle> \<Rightarrow> Normal t'a; \<Gamma>\<turnstile> \<langle>c t t'a,Normal (r t t'a)\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>c t t'a,Normal (r t t'a)\<rangle> \<Rightarrow> t'
 2. \<And>bdy t'a. \<lbrakk>xf t = v; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i' t)\<rangle> \<Rightarrow> Abrupt t'a; t' = Abrupt (r t t'a)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i f r c,Normal t\<rangle> \<Rightarrow> t'
 3. \<And>bdy fa. \<lbrakk>xf t = v; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i' t)\<rangle> \<Rightarrow> Fault fa; t' = Fault fa\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i f r c,Normal t\<rangle> \<Rightarrow> t'
 4. \<And>bdy. \<lbrakk>xf t = v; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i' t)\<rangle> \<Rightarrow> Stuck; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i f r c,Normal t\<rangle> \<Rightarrow> t'
 5. \<lbrakk>xf t = v; \<Gamma> f = None; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i f r c,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (4 subgoals):
 1. \<And>bdy t'a. \<lbrakk>xf t = v; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i' t)\<rangle> \<Rightarrow> Abrupt t'a; t' = Abrupt (r t t'a)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i f r c,Normal t\<rangle> \<Rightarrow> t'
 2. \<And>bdy fa. \<lbrakk>xf t = v; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i' t)\<rangle> \<Rightarrow> Fault fa; t' = Fault fa\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i f r c,Normal t\<rangle> \<Rightarrow> t'
 3. \<And>bdy. \<lbrakk>xf t = v; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i' t)\<rangle> \<Rightarrow> Stuck; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i f r c,Normal t\<rangle> \<Rightarrow> t'
 4. \<lbrakk>xf t = v; \<Gamma> f = None; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i f r c,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (3 subgoals):
 1. \<And>bdy fa. \<lbrakk>xf t = v; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i' t)\<rangle> \<Rightarrow> Fault fa; t' = Fault fa\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i f r c,Normal t\<rangle> \<Rightarrow> t'
 2. \<And>bdy. \<lbrakk>xf t = v; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i' t)\<rangle> \<Rightarrow> Stuck; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i f r c,Normal t\<rangle> \<Rightarrow> t'
 3. \<lbrakk>xf t = v; \<Gamma> f = None; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i f r c,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (2 subgoals):
 1. \<And>bdy. \<lbrakk>xf t = v; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (i' t)\<rangle> \<Rightarrow> Stuck; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i f r c,Normal t\<rangle> \<Rightarrow> t'
 2. \<lbrakk>xf t = v; \<Gamma> f = None; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i f r c,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>xf t = v; \<Gamma> f = None; t' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i f r c,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal:
No subgoals!