theory GraphRefine

lemma exec_via_trace:
  "Gamma \<turnstile> \<langle>com, Normal s\<rangle> \<Rightarrow> xs
    = (\<exists>tr \<in> c_trace Gamma. tr 0 = Some (com, Normal s)
        \<and> option_map exec_final_step (trace_end tr) = Some xs)" proof - have dom_If: "\<And>n f. dom (\<lambda>i. if i \<le> n then Some (f i) else None) = {..n}" by (auto split: if_split_asm) have end_If: "\<And>n f. trace_end (\<lambda>i. if i \<le> n then Some (f i) else None) = Some (f n)" apply (simp add: trace_end_def dom_If) apply (subst Max_eqI, simp+) apply (rule_tac x="Suc n" in exI, simp) done show ?thesis unfolding c_trace_def apply safe apply (clarsimp simp: relpowp_fun_conv dest!: exec_impl_steps rtranclp_imp_relpowp) apply (rule_tac x="\<lambda>i. if i \<le> n then Some (f i) else None" in bexI) apply (simp add: end_If exec_final_step_def split: xstate.split_asm) apply (simp add: nat_trace_rel_def) apply (clarsimp simp: linorder_not_le less_Suc_eq) apply (simp add: final_def split: xstate.split_asm) apply (drule(1) trace_end_SomeD) apply clarsimp apply (subgoal_tac "rtranclp (step Gamma) (the (tr 0)) (the (tr n))") apply (clarsimp simp: final_def) apply (auto simp: exec_final_step_def dest: steps_Skip_impl_exec steps_Throw_impl_exec)[1] apply (simp add: rtranclp_power relpowp_fun_conv) apply (rule_tac x=n in exI) apply (rule_tac x="the o tr" in exI) apply (frule(1) trace_None_dom_eq) apply (clarsimp simp: nat_trace_rel_def) apply (subgoal_tac "i \<in> dom tr \<and> Suc i \<in> dom tr") apply clarify apply metis apply (drule(1) eqset_imp_iff[THEN iffD1, rotated, OF domI])+ apply simp done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Gamma\<turnstile> \<langle>com,Normal s\<rangle> \<Rightarrow> xs = (\<exists>tr\<in>c_trace Gamma. tr 0 = Some (com, Normal s) \<and> map_option exec_final_step (trace_end tr) = Some xs) proof (state)
goal (1 subgoal):
 1. Gamma\<turnstile> \<langle>com,Normal s\<rangle> \<Rightarrow> xs = (\<exists>tr\<in>c_trace Gamma. tr 0 = Some (com, Normal s) \<and> map_option exec_final_step (trace_end tr) = Some xs) proof (prove)
goal (1 subgoal):
 1. \<And>n f. dom (\<lambda>i. if i \<le> n then Some (f i) else None) = {..n} proof (state)
this:
dom (\<lambda>i. if i \<le> ?n then Some (?f i) else None) = {..?n}

goal (1 subgoal):
 1. Gamma\<turnstile> \<langle>com,Normal s\<rangle> \<Rightarrow> xs = (\<exists>tr\<in>c_trace Gamma. tr 0 = Some (com, Normal s) \<and> map_option exec_final_step (trace_end tr) = Some xs) proof (prove)
goal (1 subgoal):
 1. \<And>n f. trace_end (\<lambda>i. if i \<le> n then Some (f i) else None) = Some (f n) proof (prove)
goal (1 subgoal):
 1. \<And>n f. ((\<exists>na. \<not> na \<le> n) \<longrightarrow> f (Max {..n}) = f n) \<and> (\<exists>na. \<not> na \<le> n) proof (prove)
goal (1 subgoal):
 1. \<And>n. \<exists>na. \<not> na \<le> n proof (prove)
goal:
No subgoals! proof (state)
this:
trace_end (\<lambda>i. if i \<le> ?n1 then Some (?f1 i) else None) = Some (?f1 ?n1)

goal (1 subgoal):
 1. Gamma\<turnstile> \<langle>com,Normal s\<rangle> \<Rightarrow> xs = (\<exists>tr\<in>c_trace Gamma. tr 0 = Some (com, Normal s) \<and> map_option exec_final_step (trace_end tr) = Some xs) proof (prove)
goal (1 subgoal):
 1. Gamma\<turnstile> \<langle>com,Normal s\<rangle> \<Rightarrow> xs = (\<exists>tr\<in>c_trace Gamma. tr 0 = Some (com, Normal s) \<and> map_option exec_final_step (trace_end tr) = Some xs) proof (prove)
goal (1 subgoal):
 1. Gamma\<turnstile> \<langle>com,Normal s\<rangle> \<Rightarrow> xs = (\<exists>tr\<in>nat_trace_rel (Not \<circ> final) {(x, y). Gamma\<turnstile> x \<rightarrow> y}. tr 0 = Some (com, Normal s) \<and> map_option exec_final_step (trace_end tr) = Some xs) proof (prove)
goal (2 subgoals):
 1. Gamma\<turnstile> \<langle>com,Normal s\<rangle> \<Rightarrow> xs \<Longrightarrow> \<exists>tr\<in>nat_trace_rel (Not \<circ> final) {(x, y). Gamma\<turnstile> x \<rightarrow> y}. tr 0 = Some (com, Normal s) \<and> map_option exec_final_step (trace_end tr) = Some xs
 2. \<And>tr a b. \<lbrakk>tr \<in> nat_trace_rel (Not \<circ> final) {(x, y). Gamma\<turnstile> x \<rightarrow> y}; tr 0 = Some (com, Normal s); trace_end tr = Some (a, b); xs = exec_final_step (a, b)\<rbrakk> \<Longrightarrow> Gamma\<turnstile> \<langle>com,Normal s\<rangle> \<Rightarrow> exec_final_step (a, b) proof (prove)
goal (2 subgoals):
 1. \<And>c' t' n f. \<lbrakk>case xs of Abrupt x \<Rightarrow> if Normal s = xs then c' = SKIP \<and> t' = xs else c' = THROW \<and> t' = Normal x | _ \<Rightarrow> c' = SKIP \<and> t' = xs; f 0 = (com, Normal s); f n = (c', t'); \<forall>i<n. Gamma\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> \<exists>tr\<in>nat_trace_rel (Not \<circ> final) {(x, y). Gamma\<turnstile> x \<rightarrow> y}. tr 0 = Some (com, Normal s) \<and> (\<exists>a b. trace_end tr = Some (a, b) \<and> exec_final_step (a, b) = xs)
 2. \<And>tr a b. \<lbrakk>tr \<in> nat_trace_rel (Not \<circ> final) {(x, y). Gamma\<turnstile> x \<rightarrow> y}; tr 0 = Some (com, Normal s); trace_end tr = Some (a, b); xs = exec_final_step (a, b)\<rbrakk> \<Longrightarrow> Gamma\<turnstile> \<langle>com,Normal s\<rangle> \<Rightarrow> exec_final_step (a, b) proof (prove)
goal (3 subgoals):
 1. \<And>c' t' n f. \<lbrakk>case xs of Abrupt x \<Rightarrow> if Normal s = xs then c' = SKIP \<and> t' = xs else c' = THROW \<and> t' = Normal x | _ \<Rightarrow> c' = SKIP \<and> t' = xs; f 0 = (com, Normal s); f n = (c', t'); \<forall>i<n. Gamma\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> (if 0 \<le> n then Some (f 0) else None) = Some (com, Normal s) \<and> (\<exists>a b. trace_end (\<lambda>i. if i \<le> n then Some (f i) else None) = Some (a, b) \<and> exec_final_step (a, b) = xs)
 2. \<And>c' t' n f. \<lbrakk>case xs of Abrupt x \<Rightarrow> if Normal s = xs then c' = SKIP \<and> t' = xs else c' = THROW \<and> t' = Normal x | _ \<Rightarrow> c' = SKIP \<and> t' = xs; f 0 = (com, Normal s); f n = (c', t'); \<forall>i<n. Gamma\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> (\<lambda>i. if i \<le> n then Some (f i) else None) \<in> nat_trace_rel (Not \<circ> final) {(x, y). Gamma\<turnstile> x \<rightarrow> y}
 3. \<And>tr a b. \<lbrakk>tr \<in> nat_trace_rel (Not \<circ> final) {(x, y). Gamma\<turnstile> x \<rightarrow> y}; tr 0 = Some (com, Normal s); trace_end tr = Some (a, b); xs = exec_final_step (a, b)\<rbrakk> \<Longrightarrow> Gamma\<turnstile> \<langle>com,Normal s\<rangle> \<Rightarrow> exec_final_step (a, b) proof (prove)
goal (2 subgoals):
 1. \<And>c' t' n f. \<lbrakk>case xs of Abrupt x \<Rightarrow> if Normal s = xs then c' = SKIP \<and> t' = xs else c' = THROW \<and> t' = Normal x | _ \<Rightarrow> c' = SKIP \<and> t' = xs; f 0 = (com, Normal s); f n = (c', t'); \<forall>i<n. Gamma\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> (\<lambda>i. if i \<le> n then Some (f i) else None) \<in> nat_trace_rel (Not \<circ> final) {(x, y). Gamma\<turnstile> x \<rightarrow> y}
 2. \<And>tr a b. \<lbrakk>tr \<in> nat_trace_rel (Not \<circ> final) {(x, y). Gamma\<turnstile> x \<rightarrow> y}; tr 0 = Some (com, Normal s); trace_end tr = Some (a, b); xs = exec_final_step (a, b)\<rbrakk> \<Longrightarrow> Gamma\<turnstile> \<langle>com,Normal s\<rangle> \<Rightarrow> exec_final_step (a, b) proof (prove)
goal (2 subgoals):
 1. \<And>c' t' n f. \<lbrakk>case xs of Abrupt x \<Rightarrow> if Normal s = xs then c' = SKIP \<and> t' = xs else c' = THROW \<and> t' = Normal x | _ \<Rightarrow> c' = SKIP \<and> t' = xs; f 0 = (com, Normal s); f n = (c', t'); \<forall>i<n. Gamma\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> \<forall>na\<le>n. \<not> Suc na \<le> n \<longrightarrow> (\<forall>a b. f na \<noteq> (a, b)) \<or> final (f na)
 2. \<And>tr a b. \<lbrakk>tr \<in> nat_trace_rel (Not \<circ> final) {(x, y). Gamma\<turnstile> x \<rightarrow> y}; tr 0 = Some (com, Normal s); trace_end tr = Some (a, b); xs = exec_final_step (a, b)\<rbrakk> \<Longrightarrow> Gamma\<turnstile> \<langle>com,Normal s\<rangle> \<Rightarrow> exec_final_step (a, b) proof (prove)
goal (2 subgoals):
 1. \<And>c' t' n f. \<lbrakk>case xs of Abrupt x \<Rightarrow> if Normal s = xs then c' = SKIP \<and> t' = xs else c' = THROW \<and> t' = Normal x | _ \<Rightarrow> c' = SKIP \<and> t' = xs; f 0 = (com, Normal s); f n = (c', t'); \<forall>i<n. Gamma\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> final (c', t')
 2. \<And>tr a b. \<lbrakk>tr \<in> nat_trace_rel (Not \<circ> final) {(x, y). Gamma\<turnstile> x \<rightarrow> y}; tr 0 = Some (com, Normal s); trace_end tr = Some (a, b); xs = exec_final_step (a, b)\<rbrakk> \<Longrightarrow> Gamma\<turnstile> \<langle>com,Normal s\<rangle> \<Rightarrow> exec_final_step (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>tr a b. \<lbrakk>tr \<in> nat_trace_rel (Not \<circ> final) {(x, y). Gamma\<turnstile> x \<rightarrow> y}; tr 0 = Some (com, Normal s); trace_end tr = Some (a, b); xs = exec_final_step (a, b)\<rbrakk> \<Longrightarrow> Gamma\<turnstile> \<langle>com,Normal s\<rangle> \<Rightarrow> exec_final_step (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>tr a b. \<lbrakk>tr \<in> nat_trace_rel (Not \<circ> final) {(x, y). Gamma\<turnstile> x \<rightarrow> y}; tr 0 = Some (com, Normal s); xs = exec_final_step (a, b); \<exists>n. tr n = Some (a, b) \<and> tr (Suc n) = None \<and> \<not> (Not \<circ> final) (a, b)\<rbrakk> \<Longrightarrow> Gamma\<turnstile> \<langle>com,Normal s\<rangle> \<Rightarrow> exec_final_step (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>tr a b n. \<lbrakk>tr \<in> nat_trace_rel (Not \<circ> final) {(x, y). Gamma\<turnstile> x \<rightarrow> y}; tr 0 = Some (com, Normal s); xs = exec_final_step (a, b); tr n = Some (a, b); tr (Suc n) = None; final (a, b)\<rbrakk> \<Longrightarrow> Gamma\<turnstile> \<langle>com,Normal s\<rangle> \<Rightarrow> exec_final_step (a, b) proof (prove)
goal (2 subgoals):
 1. \<And>tr a b n. \<lbrakk>tr \<in> nat_trace_rel (Not \<circ> final) {(x, y). Gamma\<turnstile> x \<rightarrow> y}; tr 0 = Some (com, Normal s); xs = exec_final_step (a, b); tr n = Some (a, b); tr (Suc n) = None; final (a, b); Gamma\<turnstile> the (tr 0) \<rightarrow>\<^sup>* the (tr n)\<rbrakk> \<Longrightarrow> Gamma\<turnstile> \<langle>com,Normal s\<rangle> \<Rightarrow> exec_final_step (a, b)
 2. \<And>tr a b n. \<lbrakk>tr \<in> nat_trace_rel (Not \<circ> final) {(x, y). Gamma\<turnstile> x \<rightarrow> y}; tr 0 = Some (com, Normal s); xs = exec_final_step (a, b); tr n = Some (a, b); tr (Suc n) = None; final (a, b)\<rbrakk> \<Longrightarrow> Gamma\<turnstile> the (tr 0) \<rightarrow>\<^sup>* the (tr n) proof (prove)
goal (2 subgoals):
 1. \<And>tr a b n. \<lbrakk>tr \<in> nat_trace_rel (Not \<circ> final) {(x, y). Gamma\<turnstile> x \<rightarrow> y}; tr 0 = Some (com, Normal s); xs = exec_final_step (a, b); tr n = Some (a, b); tr (Suc n) = None; a = SKIP \<or> a = THROW \<and> (\<exists>s. b = Normal s); Gamma\<turnstile> (com, Normal s) \<rightarrow>\<^sup>* (a, b)\<rbrakk> \<Longrightarrow> Gamma\<turnstile> \<langle>com,Normal s\<rangle> \<Rightarrow> exec_final_step (a, b)
 2. \<And>tr a b n. \<lbrakk>tr \<in> nat_trace_rel (Not \<circ> final) {(x, y). Gamma\<turnstile> x \<rightarrow> y}; tr 0 = Some (com, Normal s); xs = exec_final_step (a, b); tr n = Some (a, b); tr (Suc n) = None; final (a, b)\<rbrakk> \<Longrightarrow> Gamma\<turnstile> the (tr 0) \<rightarrow>\<^sup>* the (tr n) proof (prove)
goal (1 subgoal):
 1. \<And>tr a b n. \<lbrakk>tr \<in> nat_trace_rel (Not \<circ> final) {(x, y). Gamma\<turnstile> x \<rightarrow> y}; tr 0 = Some (com, Normal s); xs = exec_final_step (a, b); tr n = Some (a, b); tr (Suc n) = None; final (a, b)\<rbrakk> \<Longrightarrow> Gamma\<turnstile> the (tr 0) \<rightarrow>\<^sup>* the (tr n) proof (prove)
goal (1 subgoal):
 1. \<And>tr a b n. \<lbrakk>tr \<in> nat_trace_rel (Not \<circ> final) {(x, y). Gamma\<turnstile> x \<rightarrow> y}; tr 0 = Some (com, Normal s); xs = exec_final_step (a, b); tr n = Some (a, b); tr (Suc n) = None; final (a, b)\<rbrakk> \<Longrightarrow> \<exists>n f. f 0 = (com, Normal s) \<and> f n = (a, b) \<and> (\<forall>i<n. Gamma\<turnstile> f i \<rightarrow> f (Suc i)) proof (prove)
goal (1 subgoal):
 1. \<And>tr a b n. \<lbrakk>tr \<in> nat_trace_rel (Not \<circ> final) {(x, y). Gamma\<turnstile> x \<rightarrow> y}; tr 0 = Some (com, Normal s); xs = exec_final_step (a, b); tr n = Some (a, b); tr (Suc n) = None; final (a, b)\<rbrakk> \<Longrightarrow> \<exists>f. f 0 = (com, Normal s) \<and> f n = (a, b) \<and> (\<forall>i<n. Gamma\<turnstile> f i \<rightarrow> f (Suc i)) proof (prove)
goal (1 subgoal):
 1. \<And>tr a b n. \<lbrakk>tr \<in> nat_trace_rel (Not \<circ> final) {(x, y). Gamma\<turnstile> x \<rightarrow> y}; tr 0 = Some (com, Normal s); xs = exec_final_step (a, b); tr n = Some (a, b); tr (Suc n) = None; final (a, b)\<rbrakk> \<Longrightarrow> (the \<circ> tr) 0 = (com, Normal s) \<and> (the \<circ> tr) n = (a, b) \<and> (\<forall>i<n. Gamma\<turnstile> (the \<circ> tr) i \<rightarrow> (the \<circ> tr) (Suc i)) proof (prove)
goal (1 subgoal):
 1. \<And>tr a b n. \<lbrakk>tr \<in> nat_trace_rel (Not \<circ> final) {(x, y). Gamma\<turnstile> x \<rightarrow> y}; tr 0 = Some (com, Normal s); xs = exec_final_step (a, b); tr n = Some (a, b); tr (Suc n) = None; final (a, b); \<exists>n'\<le>Suc n. dom tr = {..<n'}\<rbrakk> \<Longrightarrow> (the \<circ> tr) 0 = (com, Normal s) \<and> (the \<circ> tr) n = (a, b) \<and> (\<forall>i<n. Gamma\<turnstile> (the \<circ> tr) i \<rightarrow> (the \<circ> tr) (Suc i)) proof (prove)
goal (1 subgoal):
 1. \<And>tr a b n n' i. \<lbrakk>\<forall>n. (tr n = None \<longrightarrow> tr (Suc n) = None) \<and> ((\<exists>a b. tr (Suc n) = Some (a, b)) \<longrightarrow> Gamma\<turnstile> the (tr n) \<rightarrow> the (tr (Suc n))) \<and> ((\<exists>a b. tr n = Some (a, b)) \<and> \<not> final (the (tr n)) \<longrightarrow> (\<exists>a b. tr (Suc n) = Some (a, b))); tr 0 = Some (com, Normal s); xs = exec_final_step (a, b); tr n = Some (a, b); tr (Suc n) = None; final (a, b); n' \<le> Suc n; dom tr = {..<n'}; i < n\<rbrakk> \<Longrightarrow> Gamma\<turnstile> the (tr i) \<rightarrow> the (tr (Suc i)) proof (prove)
goal (2 subgoals):
 1. \<And>tr a b n n' i. \<lbrakk>\<forall>n. (tr n = None \<longrightarrow> tr (Suc n) = None) \<and> ((\<exists>a b. tr (Suc n) = Some (a, b)) \<longrightarrow> Gamma\<turnstile> the (tr n) \<rightarrow> the (tr (Suc n))) \<and> ((\<exists>a b. tr n = Some (a, b)) \<and> \<not> final (the (tr n)) \<longrightarrow> (\<exists>a b. tr (Suc n) = Some (a, b))); tr 0 = Some (com, Normal s); xs = exec_final_step (a, b); tr n = Some (a, b); tr (Suc n) = None; final (a, b); n' \<le> Suc n; dom tr = {..<n'}; i < n; i \<in> dom tr \<and> Suc i \<in> dom tr\<rbrakk> \<Longrightarrow> Gamma\<turnstile> the (tr i) \<rightarrow> the (tr (Suc i))
 2. \<And>tr a b n n' i. \<lbrakk>\<forall>n. (tr n = None \<longrightarrow> tr (Suc n) = None) \<and> ((\<exists>a b. tr (Suc n) = Some (a, b)) \<longrightarrow> Gamma\<turnstile> the (tr n) \<rightarrow> the (tr (Suc n))) \<and> ((\<exists>a b. tr n = Some (a, b)) \<and> \<not> final (the (tr n)) \<longrightarrow> (\<exists>a b. tr (Suc n) = Some (a, b))); tr 0 = Some (com, Normal s); xs = exec_final_step (a, b); tr n = Some (a, b); tr (Suc n) = None; final (a, b); n' \<le> Suc n; dom tr = {..<n'}; i < n\<rbrakk> \<Longrightarrow> i \<in> dom tr \<and> Suc i \<in> dom tr proof (prove)
goal (2 subgoals):
 1. \<And>tr a b n n' i aa ba ab bb. \<lbrakk>\<forall>n. (tr n = None \<longrightarrow> tr (Suc n) = None) \<and> ((\<exists>a b. tr (Suc n) = Some (a, b)) \<longrightarrow> Gamma\<turnstile> the (tr n) \<rightarrow> the (tr (Suc n))) \<and> ((\<exists>a b. tr n = Some (a, b)) \<and> \<not> final (the (tr n)) \<longrightarrow> (\<exists>a b. tr (Suc n) = Some (a, b))); tr 0 = Some (com, Normal s); xs = exec_final_step (a, b); tr n = Some (a, b); tr (Suc n) = None; final (a, b); n' \<le> Suc n; dom tr = {..<n'}; i < n; tr i = Some (aa, ba); tr (Suc i) = Some (ab, bb)\<rbrakk> \<Longrightarrow> Gamma\<turnstile> the (tr i) \<rightarrow> the (tr (Suc i))
 2. \<And>tr a b n n' i. \<lbrakk>\<forall>n. (tr n = None \<longrightarrow> tr (Suc n) = None) \<and> ((\<exists>a b. tr (Suc n) = Some (a, b)) \<longrightarrow> Gamma\<turnstile> the (tr n) \<rightarrow> the (tr (Suc n))) \<and> ((\<exists>a b. tr n = Some (a, b)) \<and> \<not> final (the (tr n)) \<longrightarrow> (\<exists>a b. tr (Suc n) = Some (a, b))); tr 0 = Some (com, Normal s); xs = exec_final_step (a, b); tr n = Some (a, b); tr (Suc n) = None; final (a, b); n' \<le> Suc n; dom tr = {..<n'}; i < n\<rbrakk> \<Longrightarrow> i \<in> dom tr \<and> Suc i \<in> dom tr proof (prove)
goal (1 subgoal):
 1. \<And>tr a b n n' i. \<lbrakk>\<forall>n. (tr n = None \<longrightarrow> tr (Suc n) = None) \<and> ((\<exists>a b. tr (Suc n) = Some (a, b)) \<longrightarrow> Gamma\<turnstile> the (tr n) \<rightarrow> the (tr (Suc n))) \<and> ((\<exists>a b. tr n = Some (a, b)) \<and> \<not> final (the (tr n)) \<longrightarrow> (\<exists>a b. tr (Suc n) = Some (a, b))); tr 0 = Some (com, Normal s); xs = exec_final_step (a, b); tr n = Some (a, b); tr (Suc n) = None; final (a, b); n' \<le> Suc n; dom tr = {..<n'}; i < n\<rbrakk> \<Longrightarrow> i \<in> dom tr \<and> Suc i \<in> dom tr proof (prove)
goal (1 subgoal):
 1. \<And>tr a b n n' i. \<lbrakk>\<forall>n. (tr n = None \<longrightarrow> tr (Suc n) = None) \<and> ((\<exists>a b. tr (Suc n) = Some (a, b)) \<longrightarrow> Gamma\<turnstile> the (tr n) \<rightarrow> the (tr (Suc n))) \<and> ((\<exists>a b. tr n = Some (a, b)) \<and> \<not> final (the (tr n)) \<longrightarrow> (\<exists>a b. tr (Suc n) = Some (a, b))); xs = exec_final_step (a, b); tr (Suc n) = None; final (a, b); n' \<le> Suc n; dom tr = {..<n'}; i < n; 0 \<in> {..<n'}; n \<in> {..<n'}\<rbrakk> \<Longrightarrow> i \<in> dom tr \<and> Suc i \<in> dom tr proof (prove)
goal:
No subgoals! proof (state)
this:
Gamma\<turnstile> \<langle>com,Normal s\<rangle> \<Rightarrow> xs = (\<exists>tr\<in>c_trace Gamma. tr 0 = Some (com, Normal s) \<and> map_option exec_final_step (trace_end tr) = Some xs)

goal:
No subgoals!