theory GraphRefine

lemma simpl_to_graph_induct_proof:
  assumes Suc: "\<And>S' n'. n' \<ge> n
    \<Longrightarrow> simpl_to_graph SGamma GGamma gf nn com (Suc n') (S' # S) P I inp_eqs out_eqs
    \<Longrightarrow> simpl_to_graph SGamma GGamma gf nn com n' (S' # S) P I inp_eqs out_eqs"
  shows "simpl_to_graph SGamma GGamma gf nn com n (({tr} \<times> UNIV) # S) P I inp_eqs out_eqs" proof - obtain M where M_def:
    "M = (\<lambda>n1 tr1. {(n', n'', tr'). tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}
        \<and> (\<exists>sst gst gf'. tr' n'' = Some (com, Normal sst) \<and> tr n' = Some [(nn, gst, gf')]
            \<and> inp_eqs gst sst \<and> sst \<in> P \<and> sst \<in> I
            \<and> (tr, restrict_map tr' {..n''}) \<in> suffix_tuple_closure_inter (set S)
            \<and> restrict_map tr' {..n1} = restrict_map tr1 {..n1}
            \<and> n' \<ge> n \<and> n'' \<ge> n \<and> n'' \<ge> n1)})" by auto have induct_ge: "\<And>S' m n'. m \<ge> n \<longrightarrow> simpl_to_graph SGamma GGamma gf nn com m (S' # S) P I inp_eqs out_eqs
    \<Longrightarrow> m \<ge> n'
    \<Longrightarrow> n' \<ge> n \<longrightarrow> simpl_to_graph SGamma GGamma gf nn com n' (S' # S) P I inp_eqs out_eqs" apply (erule(1) inc_induct) apply clarsimp apply (erule(1) Suc) done hence ge: "\<And>S' m n'. simpl_to_graph SGamma GGamma gf nn com m (S' # S) P I inp_eqs out_eqs
    \<Longrightarrow> m \<ge> n' \<Longrightarrow> n' \<ge> n
    \<Longrightarrow> simpl_to_graph SGamma GGamma gf nn com n' (S' # S) P I inp_eqs out_eqs" by auto have terminating_case: "\<And>i j orig_tr' n1 tr1. (i, j, orig_tr') \<in> M n1 tr1
      \<Longrightarrow> tr \<in> exec_trace GGamma gf
      \<Longrightarrow> \<forall>v' \<in> M n1 tr1. fst v' > i \<longrightarrow> ((j, orig_tr'), snd v') \<notin> extend_rel
      \<Longrightarrow> \<exists>tr'. tr' \<in> c_trace SGamma
            \<and> restrict_map tr' {..j} = restrict_map orig_tr' {..j}
            \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr')" apply (cut_tac n'="min i j" and m="Suc (max i j)"
            and S'="{tr} \<times> {restrict_map orig_tr' {..j}}" in ge) apply (clarsimp simp: M_def simpl_to_graph_def suffix_tuple_closure_inter_insert) apply (erule_tac x=n' in allE, erule_tac x=n'' in allE, erule_tac x=tr' in allE) apply (simp add: Suc_le_eq) apply (drule(1) restrict_map_eq_Some_le) apply simp apply simp apply (clarsimp simp: M_def) apply (clarsimp simp: M_def) apply (erule_tac n''=j and tr'=orig_tr' in simpl_to_graphD,
      (rule conjI | assumption | simp)+) apply (simp add: suffix_tuple_closure_inter_insert) apply (metis min.idem) apply simp done have infinite_case:
    "\<And>v' n1 tr1. \<forall>v \<in> M n1 tr1. \<exists>v' \<in> M n1 tr1. fst v' > fst v \<and> (snd v, snd v') \<in> extend_rel
        \<Longrightarrow> tr \<in> exec_trace GGamma gf
        \<Longrightarrow> v' \<in> M n1 tr1
        \<Longrightarrow> \<exists>tr'. trace_end tr = None
            \<and> restrict_map tr' {.. n1} = restrict_map tr1 {.. n1}
            \<and> trace_end tr' = None
            \<and> tr' \<in> c_trace SGamma" apply (drule extensible_traces_to_infinite_trace_choice[where
          trace=snd and m=fst, rotated]) apply (rule ballI, drule(1) bspec) apply fastforce apply (erule exE, rename_tac tr') apply (rule_tac x=tr' in exI) apply (rule conjI) apply (rule trace_end_None_ge_seq) apply (auto simp add: exec_trace_def)[1] apply clarsimp apply (drule_tac x=i in spec) apply (clarsimp simp: M_def) apply (blast intro: less_imp_le) apply (clarsimp simp: c_trace_def) apply (rule conjI) apply (drule_tac x=0 in spec) apply (clarsimp simp: M_def) apply (drule_tac i=n1 in restrict_map_eq_mono[rotated], assumption)+ apply simp apply (rule trace_prefixes_to_trace) apply clarsimp apply (drule_tac x=i in spec) apply (clarsimp simp: M_def) apply (blast intro: less_imp_le) done show ?thesis apply (clarsimp simp: simpl_to_graph_def suffix_tuple_closure_inter_insert) apply (case_tac "(\<forall>v \<in> M n'' tr'. \<exists>v' \<in> M n'' tr'. fst v' > fst v \<and> (snd v, snd v') \<in> extend_rel)") apply (drule(1) infinite_case) apply (fastforce simp add: M_def) apply (fastforce simp: trace_end_match_def) apply clarsimp apply (frule(1) terminating_case, simp) apply (clarify, rename_tac soln_tr', rule_tac x=soln_tr' in exI) apply (clarsimp simp: M_def) apply (drule_tac i=n'' in restrict_map_eq_mono[rotated], assumption)+ apply simp done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. simpl_to_graph SGamma GGamma gf nn com n ({tr} \<times> UNIV # S) P I inp_eqs out_eqs proof (state)
goal (1 subgoal):
 1. simpl_to_graph SGamma GGamma gf nn com n ({tr} \<times> UNIV # S) P I inp_eqs out_eqs proof (prove)
goal (1 subgoal):
 1. (\<And>M. M = (\<lambda>n1 tr1. {(n', n'', tr'). tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y} \<and> (\<exists>sst gst gf'. tr' n'' = Some (com, Normal sst) \<and> tr n' = Some [(nn, gst, gf')] \<and> inp_eqs gst sst \<and> sst \<in> P \<and> sst \<in> I \<and> (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set S) \<and> tr'|\<^bsub>{..n1}\<^esub> = tr1|\<^bsub>{..n1}\<^esub> \<and> n \<le> n' \<and> n \<le> n'' \<and> n1 \<le> n'')}) \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
M = (\<lambda>n1 tr1. {(n', n'', tr'). tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y} \<and> (\<exists>sst gst gf'. tr' n'' = Some (com, Normal sst) \<and> tr n' = Some [(nn, gst, gf')] \<and> inp_eqs gst sst \<and> sst \<in> P \<and> sst \<in> I \<and> (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set S) \<and> tr'|\<^bsub>{..n1}\<^esub> = tr1|\<^bsub>{..n1}\<^esub> \<and> n \<le> n' \<and> n \<le> n'' \<and> n1 \<le> n'')})

goal (1 subgoal):
 1. simpl_to_graph SGamma GGamma gf nn com n ({tr} \<times> UNIV # S) P I inp_eqs out_eqs proof (prove)
goal (1 subgoal):
 1. \<And>S' m n'. \<lbrakk>n \<le> m \<longrightarrow> simpl_to_graph SGamma GGamma gf nn com m (S' # S) P I inp_eqs out_eqs; n' \<le> m\<rbrakk> \<Longrightarrow> n \<le> n' \<longrightarrow> simpl_to_graph SGamma GGamma gf nn com n' (S' # S) P I inp_eqs out_eqs proof (prove)
goal (1 subgoal):
 1. \<And>S' m n' na. \<lbrakk>n \<le> m \<longrightarrow> simpl_to_graph SGamma GGamma gf nn com m (S' # S) P I inp_eqs out_eqs; n' \<le> na; na < m; n \<le> Suc na \<longrightarrow> simpl_to_graph SGamma GGamma gf nn com (Suc na) (S' # S) P I inp_eqs out_eqs\<rbrakk> \<Longrightarrow> n \<le> na \<longrightarrow> simpl_to_graph SGamma GGamma gf nn com na (S' # S) P I inp_eqs out_eqs proof (prove)
goal (1 subgoal):
 1. \<And>S' m n' na. \<lbrakk>simpl_to_graph SGamma GGamma gf nn com m (S' # S) P I inp_eqs out_eqs; n' \<le> na; na < m; simpl_to_graph SGamma GGamma gf nn com (Suc na) (S' # S) P I inp_eqs out_eqs; n \<le> na\<rbrakk> \<Longrightarrow> simpl_to_graph SGamma GGamma gf nn com na (S' # S) P I inp_eqs out_eqs proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrakk>n \<le> ?m \<longrightarrow> simpl_to_graph SGamma GGamma gf nn com ?m (?S' # S) P I inp_eqs out_eqs; ?n' \<le> ?m\<rbrakk> \<Longrightarrow> n \<le> ?n' \<longrightarrow> simpl_to_graph SGamma GGamma gf nn com ?n' (?S' # S) P I inp_eqs out_eqs

goal (1 subgoal):
 1. simpl_to_graph SGamma GGamma gf nn com n ({tr} \<times> UNIV # S) P I inp_eqs out_eqs proof (prove)
using this:
\<lbrakk>n \<le> ?m \<longrightarrow> simpl_to_graph SGamma GGamma gf nn com ?m (?S' # S) P I inp_eqs out_eqs; ?n' \<le> ?m\<rbrakk> \<Longrightarrow> n \<le> ?n' \<longrightarrow> simpl_to_graph SGamma GGamma gf nn com ?n' (?S' # S) P I inp_eqs out_eqs

goal (1 subgoal):
 1. \<And>S' m n'. \<lbrakk>simpl_to_graph SGamma GGamma gf nn com m (S' # S) P I inp_eqs out_eqs; n' \<le> m; n \<le> n'\<rbrakk> \<Longrightarrow> simpl_to_graph SGamma GGamma gf nn com n' (S' # S) P I inp_eqs out_eqs proof (state)
this:
\<lbrakk>simpl_to_graph SGamma GGamma gf nn com ?m (?S' # S) P I inp_eqs out_eqs; ?n' \<le> ?m; n \<le> ?n'\<rbrakk> \<Longrightarrow> simpl_to_graph SGamma GGamma gf nn com ?n' (?S' # S) P I inp_eqs out_eqs

goal (1 subgoal):
 1. simpl_to_graph SGamma GGamma gf nn com n ({tr} \<times> UNIV # S) P I inp_eqs out_eqs proof (prove)
goal (1 subgoal):
 1. \<And>i j orig_tr' n1 tr1. \<lbrakk>(i, j, orig_tr') \<in> M n1 tr1; tr \<in> exec_trace GGamma gf; \<forall>v'\<in>M n1 tr1. i < fst v' \<longrightarrow> ((j, orig_tr'), snd v') \<notin> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>}\<rbrakk> \<Longrightarrow> \<exists>tr'. tr' \<in> c_trace SGamma \<and> tr'|\<^bsub>{..j}\<^esub> = orig_tr'|\<^bsub>{..j}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr') proof (prove)
goal (4 subgoals):
 1. \<And>i j orig_tr' n1 tr1. \<lbrakk>(i, j, orig_tr') \<in> M n1 tr1; tr \<in> exec_trace GGamma gf; \<forall>v'\<in>M n1 tr1. i < fst v' \<longrightarrow> ((j, orig_tr'), snd v') \<notin> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>}\<rbrakk> \<Longrightarrow> simpl_to_graph SGamma GGamma gf nn com (Suc (max i j)) ({tr} \<times> {orig_tr'|\<^bsub>{..j}\<^esub>} # S) P I inp_eqs out_eqs
 2. \<And>i j orig_tr' n1 tr1. \<lbrakk>(i, j, orig_tr') \<in> M n1 tr1; tr \<in> exec_trace GGamma gf; \<forall>v'\<in>M n1 tr1. i < fst v' \<longrightarrow> ((j, orig_tr'), snd v') \<notin> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>}\<rbrakk> \<Longrightarrow> min i j \<le> Suc (max i j)
 3. \<And>i j orig_tr' n1 tr1. \<lbrakk>(i, j, orig_tr') \<in> M n1 tr1; tr \<in> exec_trace GGamma gf; \<forall>v'\<in>M n1 tr1. i < fst v' \<longrightarrow> ((j, orig_tr'), snd v') \<notin> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>}\<rbrakk> \<Longrightarrow> n \<le> min i j
 4. \<And>i j orig_tr' n1 tr1. \<lbrakk>(i, j, orig_tr') \<in> M n1 tr1; tr \<in> exec_trace GGamma gf; \<forall>v'\<in>M n1 tr1. i < fst v' \<longrightarrow> ((j, orig_tr'), snd v') \<notin> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>}; simpl_to_graph SGamma GGamma gf nn com (min i j) ({tr} \<times> {orig_tr'|\<^bsub>{..j}\<^esub>} # S) P I inp_eqs out_eqs\<rbrakk> \<Longrightarrow> \<exists>tr'. tr' \<in> c_trace SGamma \<and> tr'|\<^bsub>{..j}\<^esub> = orig_tr'|\<^bsub>{..j}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr') proof (prove)
goal (4 subgoals):
 1. \<And>i j orig_tr' n1 tr1 gst sst n' gf' tr' n'' ssta gsta gf'a k. \<lbrakk>tr \<in> exec_trace GGamma gf; \<forall>a aa b. b \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y} \<and> (\<exists>sst. b aa = Some (com, Normal sst) \<and> (\<exists>gst. (\<exists>gf'. tr a = Some [(nn, gst, gf')]) \<and> inp_eqs gst sst \<and> sst \<in> P \<and> sst \<in> I \<and> (tr, b|\<^bsub>{..aa}\<^esub>) \<in> suffix_tuple_closure_inter (set S) \<and> b|\<^bsub>{..n1}\<^esub> = tr1|\<^bsub>{..n1}\<^esub> \<and> n \<le> a \<and> n \<le> aa \<and> n1 \<le> aa)) \<longrightarrow> i < a \<longrightarrow> j < aa \<longrightarrow> orig_tr'|\<^bsub>{..j}\<^esub> \<noteq> b|\<^bsub>{..j}\<^esub>; orig_tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; orig_tr' j = Some (com, Normal ssta); tr i = Some [(nn, gsta, gf'a)]; inp_eqs gsta ssta; ssta \<in> P; ssta \<in> I; (tr, orig_tr'|\<^bsub>{..j}\<^esub>) \<in> suffix_tuple_closure_inter (set S); orig_tr'|\<^bsub>{..n1}\<^esub> = tr1|\<^bsub>{..n1}\<^esub>; n \<le> i; n \<le> j; n1 \<le> j; tr n' = Some [(nn, gst, gf')]; sst \<in> P; sst \<in> I; inp_eqs gst sst; Suc (max i j) \<le> n'; Suc (max i j) \<le> n''; tr'|\<^bsub>{..min n'' k}\<^esub> = orig_tr'|\<^bsub>{..j}\<^esub>; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set S); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (com, Normal sst)\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'')
 2. \<And>i j orig_tr' n1 tr1. \<lbrakk>(i, j, orig_tr') \<in> M n1 tr1; tr \<in> exec_trace GGamma gf; \<forall>v'\<in>M n1 tr1. i < fst v' \<longrightarrow> ((j, orig_tr'), snd v') \<notin> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>}\<rbrakk> \<Longrightarrow> min i j \<le> Suc (max i j)
 3. \<And>i j orig_tr' n1 tr1. \<lbrakk>(i, j, orig_tr') \<in> M n1 tr1; tr \<in> exec_trace GGamma gf; \<forall>v'\<in>M n1 tr1. i < fst v' \<longrightarrow> ((j, orig_tr'), snd v') \<notin> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>}\<rbrakk> \<Longrightarrow> n \<le> min i j
 4. \<And>i j orig_tr' n1 tr1. \<lbrakk>(i, j, orig_tr') \<in> M n1 tr1; tr \<in> exec_trace GGamma gf; \<forall>v'\<in>M n1 tr1. i < fst v' \<longrightarrow> ((j, orig_tr'), snd v') \<notin> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>}; simpl_to_graph SGamma GGamma gf nn com (min i j) ({tr} \<times> {orig_tr'|\<^bsub>{..j}\<^esub>} # S) P I inp_eqs out_eqs\<rbrakk> \<Longrightarrow> \<exists>tr'. tr' \<in> c_trace SGamma \<and> tr'|\<^bsub>{..j}\<^esub> = orig_tr'|\<^bsub>{..j}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr') proof (prove)
goal (4 subgoals):
 1. \<And>i j orig_tr' n1 tr1 gst sst n' gf' tr' n'' ssta gsta gf'a k. \<lbrakk>tr \<in> exec_trace GGamma gf; orig_tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; orig_tr' j = Some (com, Normal ssta); tr i = Some [(nn, gsta, gf'a)]; inp_eqs gsta ssta; ssta \<in> P; ssta \<in> I; (tr, orig_tr'|\<^bsub>{..j}\<^esub>) \<in> suffix_tuple_closure_inter (set S); orig_tr'|\<^bsub>{..n1}\<^esub> = tr1|\<^bsub>{..n1}\<^esub>; n \<le> i; n \<le> j; n1 \<le> j; tr n' = Some [(nn, gst, gf')]; sst \<in> P; sst \<in> I; inp_eqs gst sst; Suc (max i j) \<le> n'; Suc (max i j) \<le> n''; tr'|\<^bsub>{..min n'' k}\<^esub> = orig_tr'|\<^bsub>{..j}\<^esub>; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set S); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (com, Normal sst); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y} \<and> (\<exists>sst. tr' n'' = Some (com, Normal sst) \<and> (\<exists>gst. (\<exists>gf'. tr n' = Some [(nn, gst, gf')]) \<and> inp_eqs gst sst \<and> sst \<in> P \<and> sst \<in> I \<and> (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set S) \<and> tr'|\<^bsub>{..n1}\<^esub> = tr1|\<^bsub>{..n1}\<^esub> \<and> n \<le> n' \<and> n \<le> n'' \<and> n1 \<le> n'')) \<longrightarrow> i < n' \<longrightarrow> j < n'' \<longrightarrow> orig_tr'|\<^bsub>{..j}\<^esub> \<noteq> tr'|\<^bsub>{..j}\<^esub>\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'')
 2. \<And>i j orig_tr' n1 tr1. \<lbrakk>(i, j, orig_tr') \<in> M n1 tr1; tr \<in> exec_trace GGamma gf; \<forall>v'\<in>M n1 tr1. i < fst v' \<longrightarrow> ((j, orig_tr'), snd v') \<notin> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>}\<rbrakk> \<Longrightarrow> min i j \<le> Suc (max i j)
 3. \<And>i j orig_tr' n1 tr1. \<lbrakk>(i, j, orig_tr') \<in> M n1 tr1; tr \<in> exec_trace GGamma gf; \<forall>v'\<in>M n1 tr1. i < fst v' \<longrightarrow> ((j, orig_tr'), snd v') \<notin> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>}\<rbrakk> \<Longrightarrow> n \<le> min i j
 4. \<And>i j orig_tr' n1 tr1. \<lbrakk>(i, j, orig_tr') \<in> M n1 tr1; tr \<in> exec_trace GGamma gf; \<forall>v'\<in>M n1 tr1. i < fst v' \<longrightarrow> ((j, orig_tr'), snd v') \<notin> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>}; simpl_to_graph SGamma GGamma gf nn com (min i j) ({tr} \<times> {orig_tr'|\<^bsub>{..j}\<^esub>} # S) P I inp_eqs out_eqs\<rbrakk> \<Longrightarrow> \<exists>tr'. tr' \<in> c_trace SGamma \<and> tr'|\<^bsub>{..j}\<^esub> = orig_tr'|\<^bsub>{..j}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr') proof (prove)
goal (4 subgoals):
 1. \<And>i j orig_tr' n1 tr1 gst sst n' gf' tr' n'' ssta gsta gf'a k. \<lbrakk>tr \<in> exec_trace GGamma gf; orig_tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; orig_tr' j = Some (com, Normal ssta); tr i = Some [(nn, gsta, gf'a)]; inp_eqs gsta ssta; ssta \<in> P; ssta \<in> I; (tr, orig_tr'|\<^bsub>{..j}\<^esub>) \<in> suffix_tuple_closure_inter (set S); orig_tr'|\<^bsub>{..n1}\<^esub> = tr1|\<^bsub>{..n1}\<^esub>; n \<le> i; n \<le> j; n1 \<le> j; tr n' = Some [(nn, gst, gf')]; sst \<in> P; sst \<in> I; inp_eqs gst sst; i < n' \<and> j < n'; i < n'' \<and> j < n''; tr'|\<^bsub>{..min n'' k}\<^esub> = orig_tr'|\<^bsub>{..j}\<^esub>; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set S); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (com, Normal sst); tr'|\<^bsub>{..n1}\<^esub> = tr1|\<^bsub>{..n1}\<^esub> \<longrightarrow> orig_tr'|\<^bsub>{..j}\<^esub> \<noteq> tr'|\<^bsub>{..j}\<^esub>\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'')
 2. \<And>i j orig_tr' n1 tr1. \<lbrakk>(i, j, orig_tr') \<in> M n1 tr1; tr \<in> exec_trace GGamma gf; \<forall>v'\<in>M n1 tr1. i < fst v' \<longrightarrow> ((j, orig_tr'), snd v') \<notin> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>}\<rbrakk> \<Longrightarrow> min i j \<le> Suc (max i j)
 3. \<And>i j orig_tr' n1 tr1. \<lbrakk>(i, j, orig_tr') \<in> M n1 tr1; tr \<in> exec_trace GGamma gf; \<forall>v'\<in>M n1 tr1. i < fst v' \<longrightarrow> ((j, orig_tr'), snd v') \<notin> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>}\<rbrakk> \<Longrightarrow> n \<le> min i j
 4. \<And>i j orig_tr' n1 tr1. \<lbrakk>(i, j, orig_tr') \<in> M n1 tr1; tr \<in> exec_trace GGamma gf; \<forall>v'\<in>M n1 tr1. i < fst v' \<longrightarrow> ((j, orig_tr'), snd v') \<notin> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>}; simpl_to_graph SGamma GGamma gf nn com (min i j) ({tr} \<times> {orig_tr'|\<^bsub>{..j}\<^esub>} # S) P I inp_eqs out_eqs\<rbrakk> \<Longrightarrow> \<exists>tr'. tr' \<in> c_trace SGamma \<and> tr'|\<^bsub>{..j}\<^esub> = orig_tr'|\<^bsub>{..j}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr') proof (prove)
goal (4 subgoals):
 1. \<And>i j orig_tr' n1 tr1 gst sst n' gf' tr' n'' ssta gsta gf'a k. \<lbrakk>tr \<in> exec_trace GGamma gf; orig_tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; orig_tr' j = Some (com, Normal ssta); tr i = Some [(nn, gsta, gf'a)]; inp_eqs gsta ssta; ssta \<in> P; ssta \<in> I; (tr, orig_tr'|\<^bsub>{..j}\<^esub>) \<in> suffix_tuple_closure_inter (set S); orig_tr'|\<^bsub>{..n1}\<^esub> = tr1|\<^bsub>{..n1}\<^esub>; n \<le> i; n \<le> j; n1 \<le> j; tr n' = Some [(nn, gst, gf')]; sst \<in> P; sst \<in> I; inp_eqs gst sst; i < n' \<and> j < n'; i < n'' \<and> j < n''; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set S); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (com, Normal sst); tr'|\<^bsub>{..n1}\<^esub> = tr1|\<^bsub>{..n1}\<^esub> \<longrightarrow> orig_tr'|\<^bsub>{..j}\<^esub> \<noteq> tr'|\<^bsub>{..j}\<^esub>; j \<le> min n'' k \<and> (\<forall>k\<le>j. tr'|\<^bsub>{..k}\<^esub> = orig_tr'|\<^bsub>{..k}\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'')
 2. \<And>i j orig_tr' n1 tr1. \<lbrakk>(i, j, orig_tr') \<in> M n1 tr1; tr \<in> exec_trace GGamma gf; \<forall>v'\<in>M n1 tr1. i < fst v' \<longrightarrow> ((j, orig_tr'), snd v') \<notin> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>}\<rbrakk> \<Longrightarrow> min i j \<le> Suc (max i j)
 3. \<And>i j orig_tr' n1 tr1. \<lbrakk>(i, j, orig_tr') \<in> M n1 tr1; tr \<in> exec_trace GGamma gf; \<forall>v'\<in>M n1 tr1. i < fst v' \<longrightarrow> ((j, orig_tr'), snd v') \<notin> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>}\<rbrakk> \<Longrightarrow> n \<le> min i j
 4. \<And>i j orig_tr' n1 tr1. \<lbrakk>(i, j, orig_tr') \<in> M n1 tr1; tr \<in> exec_trace GGamma gf; \<forall>v'\<in>M n1 tr1. i < fst v' \<longrightarrow> ((j, orig_tr'), snd v') \<notin> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>}; simpl_to_graph SGamma GGamma gf nn com (min i j) ({tr} \<times> {orig_tr'|\<^bsub>{..j}\<^esub>} # S) P I inp_eqs out_eqs\<rbrakk> \<Longrightarrow> \<exists>tr'. tr' \<in> c_trace SGamma \<and> tr'|\<^bsub>{..j}\<^esub> = orig_tr'|\<^bsub>{..j}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr') proof (prove)
goal (3 subgoals):
 1. \<And>i j orig_tr' n1 tr1. \<lbrakk>(i, j, orig_tr') \<in> M n1 tr1; tr \<in> exec_trace GGamma gf; \<forall>v'\<in>M n1 tr1. i < fst v' \<longrightarrow> ((j, orig_tr'), snd v') \<notin> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>}\<rbrakk> \<Longrightarrow> min i j \<le> Suc (max i j)
 2. \<And>i j orig_tr' n1 tr1. \<lbrakk>(i, j, orig_tr') \<in> M n1 tr1; tr \<in> exec_trace GGamma gf; \<forall>v'\<in>M n1 tr1. i < fst v' \<longrightarrow> ((j, orig_tr'), snd v') \<notin> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>}\<rbrakk> \<Longrightarrow> n \<le> min i j
 3. \<And>i j orig_tr' n1 tr1. \<lbrakk>(i, j, orig_tr') \<in> M n1 tr1; tr \<in> exec_trace GGamma gf; \<forall>v'\<in>M n1 tr1. i < fst v' \<longrightarrow> ((j, orig_tr'), snd v') \<notin> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>}; simpl_to_graph SGamma GGamma gf nn com (min i j) ({tr} \<times> {orig_tr'|\<^bsub>{..j}\<^esub>} # S) P I inp_eqs out_eqs\<rbrakk> \<Longrightarrow> \<exists>tr'. tr' \<in> c_trace SGamma \<and> tr'|\<^bsub>{..j}\<^esub> = orig_tr'|\<^bsub>{..j}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr') proof (prove)
goal (2 subgoals):
 1. \<And>i j orig_tr' n1 tr1. \<lbrakk>(i, j, orig_tr') \<in> M n1 tr1; tr \<in> exec_trace GGamma gf; \<forall>v'\<in>M n1 tr1. i < fst v' \<longrightarrow> ((j, orig_tr'), snd v') \<notin> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>}\<rbrakk> \<Longrightarrow> n \<le> min i j
 2. \<And>i j orig_tr' n1 tr1. \<lbrakk>(i, j, orig_tr') \<in> M n1 tr1; tr \<in> exec_trace GGamma gf; \<forall>v'\<in>M n1 tr1. i < fst v' \<longrightarrow> ((j, orig_tr'), snd v') \<notin> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>}; simpl_to_graph SGamma GGamma gf nn com (min i j) ({tr} \<times> {orig_tr'|\<^bsub>{..j}\<^esub>} # S) P I inp_eqs out_eqs\<rbrakk> \<Longrightarrow> \<exists>tr'. tr' \<in> c_trace SGamma \<and> tr'|\<^bsub>{..j}\<^esub> = orig_tr'|\<^bsub>{..j}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr') proof (prove)
goal (1 subgoal):
 1. \<And>i j orig_tr' n1 tr1. \<lbrakk>(i, j, orig_tr') \<in> M n1 tr1; tr \<in> exec_trace GGamma gf; \<forall>v'\<in>M n1 tr1. i < fst v' \<longrightarrow> ((j, orig_tr'), snd v') \<notin> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>}; simpl_to_graph SGamma GGamma gf nn com (min i j) ({tr} \<times> {orig_tr'|\<^bsub>{..j}\<^esub>} # S) P I inp_eqs out_eqs\<rbrakk> \<Longrightarrow> \<exists>tr'. tr' \<in> c_trace SGamma \<and> tr'|\<^bsub>{..j}\<^esub> = orig_tr'|\<^bsub>{..j}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr') proof (prove)
goal (1 subgoal):
 1. \<And>i j orig_tr' n1 tr1 sst gst gf'. \<lbrakk>tr \<in> exec_trace GGamma gf; \<forall>a aa b. b \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y} \<and> (\<exists>sst. b aa = Some (com, Normal sst) \<and> (\<exists>gst. (\<exists>gf'. tr a = Some [(nn, gst, gf')]) \<and> inp_eqs gst sst \<and> sst \<in> P \<and> sst \<in> I \<and> (tr, b|\<^bsub>{..aa}\<^esub>) \<in> suffix_tuple_closure_inter (set S) \<and> b|\<^bsub>{..n1}\<^esub> = tr1|\<^bsub>{..n1}\<^esub> \<and> n \<le> a \<and> n \<le> aa \<and> n1 \<le> aa)) \<longrightarrow> i < a \<longrightarrow> j < aa \<longrightarrow> orig_tr'|\<^bsub>{..j}\<^esub> \<noteq> b|\<^bsub>{..j}\<^esub>; simpl_to_graph SGamma GGamma gf nn com (min i j) ({(tr, orig_tr'|\<^bsub>{..j}\<^esub>)} # S) P I inp_eqs out_eqs; orig_tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; orig_tr' j = Some (com, Normal sst); tr i = Some [(nn, gst, gf')]; inp_eqs gst sst; sst \<in> P; sst \<in> I; (tr, orig_tr'|\<^bsub>{..j}\<^esub>) \<in> suffix_tuple_closure_inter (set S); orig_tr'|\<^bsub>{..n1}\<^esub> = tr1|\<^bsub>{..n1}\<^esub>; n \<le> i; n \<le> j; n1 \<le> j\<rbrakk> \<Longrightarrow> \<exists>tr'. tr' \<in> c_trace SGamma \<and> tr'|\<^bsub>{..j}\<^esub> = orig_tr'|\<^bsub>{..j}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr') proof (prove)
goal (2 subgoals):
 1. \<And>i j orig_tr' n1 tr1 sst gst gf'. \<lbrakk>tr \<in> exec_trace GGamma gf; \<forall>a aa b. b \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y} \<and> (\<exists>sst. b aa = Some (com, Normal sst) \<and> (\<exists>gst. (\<exists>gf'. tr a = Some [(nn, gst, gf')]) \<and> inp_eqs gst sst \<and> sst \<in> P \<and> sst \<in> I \<and> (tr, b|\<^bsub>{..aa}\<^esub>) \<in> suffix_tuple_closure_inter (set S) \<and> b|\<^bsub>{..n1}\<^esub> = tr1|\<^bsub>{..n1}\<^esub> \<and> n \<le> a \<and> n \<le> aa \<and> n1 \<le> aa)) \<longrightarrow> i < a \<longrightarrow> j < aa \<longrightarrow> orig_tr'|\<^bsub>{..j}\<^esub> \<noteq> b|\<^bsub>{..j}\<^esub>; orig_tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; orig_tr' j = Some (com, Normal sst); tr i = Some [(nn, gst, gf')]; inp_eqs gst sst; sst \<in> P; sst \<in> I; (tr, orig_tr'|\<^bsub>{..j}\<^esub>) \<in> suffix_tuple_closure_inter (set S); orig_tr'|\<^bsub>{..n1}\<^esub> = tr1|\<^bsub>{..n1}\<^esub>; n \<le> i; n \<le> j; n1 \<le> j\<rbrakk> \<Longrightarrow> (tr, orig_tr'|\<^bsub>{..j}\<^esub>) \<in> suffix_tuple_closure_inter (insert {(tr, orig_tr'|\<^bsub>{..j}\<^esub>)} (set S))
 2. \<And>i j orig_tr' n1 tr1 sst gst gf'. \<lbrakk>tr \<in> exec_trace GGamma gf; \<forall>a aa b. b \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y} \<and> (\<exists>sst. b aa = Some (com, Normal sst) \<and> (\<exists>gst. (\<exists>gf'. tr a = Some [(nn, gst, gf')]) \<and> inp_eqs gst sst \<and> sst \<in> P \<and> sst \<in> I \<and> (tr, b|\<^bsub>{..aa}\<^esub>) \<in> suffix_tuple_closure_inter (set S) \<and> b|\<^bsub>{..n1}\<^esub> = tr1|\<^bsub>{..n1}\<^esub> \<and> n \<le> a \<and> n \<le> aa \<and> n1 \<le> aa)) \<longrightarrow> i < a \<longrightarrow> j < aa \<longrightarrow> orig_tr'|\<^bsub>{..j}\<^esub> \<noteq> b|\<^bsub>{..j}\<^esub>; orig_tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; orig_tr' j = Some (com, Normal sst); tr i = Some [(nn, gst, gf')]; inp_eqs gst sst; sst \<in> P; sst \<in> I; (tr, orig_tr'|\<^bsub>{..j}\<^esub>) \<in> suffix_tuple_closure_inter (set S); orig_tr'|\<^bsub>{..n1}\<^esub> = tr1|\<^bsub>{..n1}\<^esub>; n \<le> i; n \<le> j; n1 \<le> j\<rbrakk> \<Longrightarrow> orig_tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y} \<and> orig_tr' j = Some (com, Normal sst) proof (prove)
goal (2 subgoals):
 1. \<And>i j orig_tr' n1 tr1 sst gst gf'. \<lbrakk>tr \<in> exec_trace GGamma gf; \<forall>a aa b. b \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y} \<and> (\<exists>sst. b aa = Some (com, Normal sst) \<and> (\<exists>gst. (\<exists>gf'. tr a = Some [(nn, gst, gf')]) \<and> inp_eqs gst sst \<and> sst \<in> P \<and> sst \<in> I \<and> (tr, b|\<^bsub>{..aa}\<^esub>) \<in> suffix_tuple_closure_inter (set S) \<and> b|\<^bsub>{..n1}\<^esub> = tr1|\<^bsub>{..n1}\<^esub> \<and> n \<le> a \<and> n \<le> aa \<and> n1 \<le> aa)) \<longrightarrow> i < a \<longrightarrow> j < aa \<longrightarrow> orig_tr'|\<^bsub>{..j}\<^esub> \<noteq> b|\<^bsub>{..j}\<^esub>; orig_tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; orig_tr' j = Some (com, Normal sst); tr i = Some [(nn, gst, gf')]; inp_eqs gst sst; sst \<in> P; sst \<in> I; (tr, orig_tr'|\<^bsub>{..j}\<^esub>) \<in> suffix_tuple_closure_inter (set S); orig_tr'|\<^bsub>{..n1}\<^esub> = tr1|\<^bsub>{..n1}\<^esub>; n \<le> i; n \<le> j; n1 \<le> j\<rbrakk> \<Longrightarrow> \<exists>k. orig_tr'|\<^bsub>{..min j k}\<^esub> = orig_tr'|\<^bsub>{..j}\<^esub>
 2. \<And>i j orig_tr' n1 tr1 sst gst gf'. \<lbrakk>tr \<in> exec_trace GGamma gf; \<forall>a aa b. b \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y} \<and> (\<exists>sst. b aa = Some (com, Normal sst) \<and> (\<exists>gst. (\<exists>gf'. tr a = Some [(nn, gst, gf')]) \<and> inp_eqs gst sst \<and> sst \<in> P \<and> sst \<in> I \<and> (tr, b|\<^bsub>{..aa}\<^esub>) \<in> suffix_tuple_closure_inter (set S) \<and> b|\<^bsub>{..n1}\<^esub> = tr1|\<^bsub>{..n1}\<^esub> \<and> n \<le> a \<and> n \<le> aa \<and> n1 \<le> aa)) \<longrightarrow> i < a \<longrightarrow> j < aa \<longrightarrow> orig_tr'|\<^bsub>{..j}\<^esub> \<noteq> b|\<^bsub>{..j}\<^esub>; orig_tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; orig_tr' j = Some (com, Normal sst); tr i = Some [(nn, gst, gf')]; inp_eqs gst sst; sst \<in> P; sst \<in> I; (tr, orig_tr'|\<^bsub>{..j}\<^esub>) \<in> suffix_tuple_closure_inter (set S); orig_tr'|\<^bsub>{..n1}\<^esub> = tr1|\<^bsub>{..n1}\<^esub>; n \<le> i; n \<le> j; n1 \<le> j\<rbrakk> \<Longrightarrow> orig_tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y} \<and> orig_tr' j = Some (com, Normal sst) proof (prove)
goal (1 subgoal):
 1. \<And>i j orig_tr' n1 tr1 sst gst gf'. \<lbrakk>tr \<in> exec_trace GGamma gf; \<forall>a aa b. b \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y} \<and> (\<exists>sst. b aa = Some (com, Normal sst) \<and> (\<exists>gst. (\<exists>gf'. tr a = Some [(nn, gst, gf')]) \<and> inp_eqs gst sst \<and> sst \<in> P \<and> sst \<in> I \<and> (tr, b|\<^bsub>{..aa}\<^esub>) \<in> suffix_tuple_closure_inter (set S) \<and> b|\<^bsub>{..n1}\<^esub> = tr1|\<^bsub>{..n1}\<^esub> \<and> n \<le> a \<and> n \<le> aa \<and> n1 \<le> aa)) \<longrightarrow> i < a \<longrightarrow> j < aa \<longrightarrow> orig_tr'|\<^bsub>{..j}\<^esub> \<noteq> b|\<^bsub>{..j}\<^esub>; orig_tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; orig_tr' j = Some (com, Normal sst); tr i = Some [(nn, gst, gf')]; inp_eqs gst sst; sst \<in> P; sst \<in> I; (tr, orig_tr'|\<^bsub>{..j}\<^esub>) \<in> suffix_tuple_closure_inter (set S); orig_tr'|\<^bsub>{..n1}\<^esub> = tr1|\<^bsub>{..n1}\<^esub>; n \<le> i; n \<le> j; n1 \<le> j\<rbrakk> \<Longrightarrow> orig_tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y} \<and> orig_tr' j = Some (com, Normal sst) proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrakk>(?i, ?j, ?orig_tr') \<in> M ?n1.0 ?tr1.0; tr \<in> exec_trace GGamma gf; \<forall>v'\<in>M ?n1.0 ?tr1.0. ?i < fst v' \<longrightarrow> ((?j, ?orig_tr'), snd v') \<notin> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>}\<rbrakk> \<Longrightarrow> \<exists>tr'. tr' \<in> c_trace SGamma \<and> tr'|\<^bsub>{..?j}\<^esub> = ?orig_tr'|\<^bsub>{..?j}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr')

goal (1 subgoal):
 1. simpl_to_graph SGamma GGamma gf nn com n ({tr} \<times> UNIV # S) P I inp_eqs out_eqs proof (prove)
goal (1 subgoal):
 1. \<And>v' n1 tr1. \<lbrakk>\<forall>v\<in>M n1 tr1. \<exists>v'\<in>M n1 tr1. fst v < fst v' \<and> (snd v, snd v') \<in> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>}; tr \<in> exec_trace GGamma gf; v' \<in> M n1 tr1\<rbrakk> \<Longrightarrow> \<exists>tr'. trace_end tr = None \<and> tr'|\<^bsub>{..n1}\<^esub> = tr1|\<^bsub>{..n1}\<^esub> \<and> trace_end tr' = None \<and> tr' \<in> c_trace SGamma proof (prove)
goal (2 subgoals):
 1. \<And>v' n1 tr1. \<lbrakk>\<forall>v\<in>M n1 tr1. \<exists>v'\<in>M n1 tr1. fst v < fst v' \<and> (snd v, snd v') \<in> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>}; tr \<in> exec_trace GGamma gf\<rbrakk> \<Longrightarrow> \<forall>x\<in>M n1 tr1. \<exists>y. (snd x, snd y) \<in> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>} \<and> y \<in> M n1 tr1 \<and> fst x < fst y
 2. \<And>v' n1 tr1. \<lbrakk>\<forall>v\<in>M n1 tr1. \<exists>v'\<in>M n1 tr1. fst v < fst v' \<and> (snd v, snd v') \<in> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>}; tr \<in> exec_trace GGamma gf; \<exists>tr. \<forall>i. \<exists>y\<in>M n1 tr1. \<exists>j. i < fst y \<and> i < fst (snd y) \<and> (snd y, j, tr) \<in> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>}\<rbrakk> \<Longrightarrow> \<exists>tr'. trace_end tr = None \<and> tr'|\<^bsub>{..n1}\<^esub> = tr1|\<^bsub>{..n1}\<^esub> \<and> trace_end tr' = None \<and> tr' \<in> c_trace SGamma proof (prove)
goal (2 subgoals):
 1. \<And>v' n1 tr1 x. \<lbrakk>tr \<in> exec_trace GGamma gf; x \<in> M n1 tr1; \<exists>v'\<in>M n1 tr1. fst x < fst v' \<and> (snd x, snd v') \<in> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>}\<rbrakk> \<Longrightarrow> \<exists>y. (snd x, snd y) \<in> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>} \<and> y \<in> M n1 tr1 \<and> fst x < fst y
 2. \<And>v' n1 tr1. \<lbrakk>\<forall>v\<in>M n1 tr1. \<exists>v'\<in>M n1 tr1. fst v < fst v' \<and> (snd v, snd v') \<in> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>}; tr \<in> exec_trace GGamma gf; \<exists>tr. \<forall>i. \<exists>y\<in>M n1 tr1. \<exists>j. i < fst y \<and> i < fst (snd y) \<and> (snd y, j, tr) \<in> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>}\<rbrakk> \<Longrightarrow> \<exists>tr'. trace_end tr = None \<and> tr'|\<^bsub>{..n1}\<^esub> = tr1|\<^bsub>{..n1}\<^esub> \<and> trace_end tr' = None \<and> tr' \<in> c_trace SGamma proof (prove)
goal (1 subgoal):
 1. \<And>v' n1 tr1. \<lbrakk>\<forall>v\<in>M n1 tr1. \<exists>v'\<in>M n1 tr1. fst v < fst v' \<and> (snd v, snd v') \<in> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>}; tr \<in> exec_trace GGamma gf; \<exists>tr. \<forall>i. \<exists>y\<in>M n1 tr1. \<exists>j. i < fst y \<and> i < fst (snd y) \<and> (snd y, j, tr) \<in> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>}\<rbrakk> \<Longrightarrow> \<exists>tr'. trace_end tr = None \<and> tr'|\<^bsub>{..n1}\<^esub> = tr1|\<^bsub>{..n1}\<^esub> \<and> trace_end tr' = None \<and> tr' \<in> c_trace SGamma proof (prove)
goal (1 subgoal):
 1. \<And>v' n1 tr1 tr'. \<lbrakk>\<forall>v\<in>M n1 tr1. \<exists>v'\<in>M n1 tr1. fst v < fst v' \<and> (snd v, snd v') \<in> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>}; tr \<in> exec_trace GGamma gf; \<forall>i. \<exists>y\<in>M n1 tr1. \<exists>j. i < fst y \<and> i < fst (snd y) \<and> (snd y, j, tr') \<in> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>}\<rbrakk> \<Longrightarrow> \<exists>tr'. trace_end tr = None \<and> tr'|\<^bsub>{..n1}\<^esub> = tr1|\<^bsub>{..n1}\<^esub> \<and> trace_end tr' = None \<and> tr' \<in> c_trace SGamma proof (prove)
goal (1 subgoal):
 1. \<And>v' n1 tr1 tr'. \<lbrakk>\<forall>v\<in>M n1 tr1. \<exists>v'\<in>M n1 tr1. fst v < fst v' \<and> (snd v, snd v') \<in> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>}; tr \<in> exec_trace GGamma gf; \<forall>i. \<exists>y\<in>M n1 tr1. \<exists>j. i < fst y \<and> i < fst (snd y) \<and> (snd y, j, tr') \<in> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>}\<rbrakk> \<Longrightarrow> trace_end tr = None \<and> tr'|\<^bsub>{..n1}\<^esub> = tr1|\<^bsub>{..n1}\<^esub> \<and> trace_end tr' = None \<and> tr' \<in> c_trace SGamma proof (prove)
goal (2 subgoals):
 1. \<And>v' n1 tr1 tr'. \<lbrakk>\<forall>v\<in>M n1 tr1. \<exists>v'\<in>M n1 tr1. fst v < fst v' \<and> (snd v, snd v') \<in> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>}; tr \<in> exec_trace GGamma gf; \<forall>i. \<exists>y\<in>M n1 tr1. \<exists>j. i < fst y \<and> i < fst (snd y) \<and> (snd y, j, tr') \<in> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>}\<rbrakk> \<Longrightarrow> trace_end tr = None
 2. \<And>v' n1 tr1 tr'. \<lbrakk>\<forall>v\<in>M n1 tr1. \<exists>v'\<in>M n1 tr1. fst v < fst v' \<and> (snd v, snd v') \<in> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>}; tr \<in> exec_trace GGamma gf; \<forall>i. \<exists>y\<in>M n1 tr1. \<exists>j. i < fst y \<and> i < fst (snd y) \<and> (snd y, j, tr') \<in> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>}\<rbrakk> \<Longrightarrow> tr'|\<^bsub>{..n1}\<^esub> = tr1|\<^bsub>{..n1}\<^esub> \<and> trace_end tr' = None \<and> tr' \<in> c_trace SGamma proof (prove)
goal (3 subgoals):
 1. \<And>v' n1 tr1 tr'. \<lbrakk>\<forall>v\<in>M n1 tr1. \<exists>v'\<in>M n1 tr1. fst v < fst v' \<and> (snd v, snd v') \<in> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>}; tr \<in> exec_trace GGamma gf; \<forall>i. \<exists>y\<in>M n1 tr1. \<exists>j. i < fst y \<and> i < fst (snd y) \<and> (snd y, j, tr') \<in> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>}\<rbrakk> \<Longrightarrow> tr \<in> nat_trace_rel (?c31 v' n1 tr1 tr') (?R31 v' n1 tr1 tr')
 2. \<And>v' n1 tr1 tr'. \<lbrakk>\<forall>v\<in>M n1 tr1. \<exists>v'\<in>M n1 tr1. fst v < fst v' \<and> (snd v, snd v') \<in> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>}; tr \<in> exec_trace GGamma gf; \<forall>i. \<exists>y\<in>M n1 tr1. \<exists>j. i < fst y \<and> i < fst (snd y) \<and> (snd y, j, tr') \<in> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>}\<rbrakk> \<Longrightarrow> \<forall>i. \<exists>j\<ge>i. tr j \<noteq> None
 3. \<And>v' n1 tr1 tr'. \<lbrakk>\<forall>v\<in>M n1 tr1. \<exists>v'\<in>M n1 tr1. fst v < fst v' \<and> (snd v, snd v') \<in> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>}; tr \<in> exec_trace GGamma gf; \<forall>i. \<exists>y\<in>M n1 tr1. \<exists>j. i < fst y \<and> i < fst (snd y) \<and> (snd y, j, tr') \<in> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>}\<rbrakk> \<Longrightarrow> tr'|\<^bsub>{..n1}\<^esub> = tr1|\<^bsub>{..n1}\<^esub> \<and> trace_end tr' = None \<and> tr' \<in> c_trace SGamma proof (prove)
goal (2 subgoals):
 1. \<And>v' n1 tr1 tr'. \<lbrakk>\<forall>v\<in>M n1 tr1. \<exists>v'\<in>M n1 tr1. fst v < fst v' \<and> (snd v, snd v') \<in> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>}; tr \<in> exec_trace GGamma gf; \<forall>i. \<exists>y\<in>M n1 tr1. \<exists>j. i < fst y \<and> i < fst (snd y) \<and> (snd y, j, tr') \<in> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>}\<rbrakk> \<Longrightarrow> \<forall>i. \<exists>j\<ge>i. tr j \<noteq> None
 2. \<And>v' n1 tr1 tr'. \<lbrakk>\<forall>v\<in>M n1 tr1. \<exists>v'\<in>M n1 tr1. fst v < fst v' \<and> (snd v, snd v') \<in> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>}; tr \<in> exec_trace GGamma gf; \<forall>i. \<exists>y\<in>M n1 tr1. \<exists>j. i < fst y \<and> i < fst (snd y) \<and> (snd y, j, tr') \<in> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>}\<rbrakk> \<Longrightarrow> tr'|\<^bsub>{..n1}\<^esub> = tr1|\<^bsub>{..n1}\<^esub> \<and> trace_end tr' = None \<and> tr' \<in> c_trace SGamma proof (prove)
goal (2 subgoals):
 1. \<And>n1 tr1 tr' i. \<lbrakk>\<forall>v\<in>M n1 tr1. \<exists>v'\<in>M n1 tr1. fst v < fst v' \<and> (case snd v of (i, tr) \<Rightarrow> \<lambda>(j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>) (snd v'); tr \<in> exec_trace GGamma gf; \<forall>i. \<exists>y\<in>M n1 tr1. i < fst y \<and> i < fst (snd y) \<and> (\<exists>j. (case snd y of (i, tr) \<Rightarrow> \<lambda>(j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>) (j, tr'))\<rbrakk> \<Longrightarrow> \<exists>j\<ge>i. \<exists>y. tr j = Some y
 2. \<And>v' n1 tr1 tr'. \<lbrakk>\<forall>v\<in>M n1 tr1. \<exists>v'\<in>M n1 tr1. fst v < fst v' \<and> (snd v, snd v') \<in> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>}; tr \<in> exec_trace GGamma gf; \<forall>i. \<exists>y\<in>M n1 tr1. \<exists>j. i < fst y \<and> i < fst (snd y) \<and> (snd y, j, tr') \<in> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>}\<rbrakk> \<Longrightarrow> tr'|\<^bsub>{..n1}\<^esub> = tr1|\<^bsub>{..n1}\<^esub> \<and> trace_end tr' = None \<and> tr' \<in> c_trace SGamma proof (prove)
goal (2 subgoals):
 1. \<And>n1 tr1 tr' i. \<lbrakk>\<forall>v\<in>M n1 tr1. \<exists>v'\<in>M n1 tr1. fst v < fst v' \<and> (case snd v of (i, tr) \<Rightarrow> \<lambda>(j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>) (snd v'); tr \<in> exec_trace GGamma gf; \<exists>y\<in>M n1 tr1. i < fst y \<and> i < fst (snd y) \<and> (\<exists>j. (case snd y of (i, tr) \<Rightarrow> \<lambda>(j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>) (j, tr'))\<rbrakk> \<Longrightarrow> \<exists>j\<ge>i. \<exists>y. tr j = Some y
 2. \<And>v' n1 tr1 tr'. \<lbrakk>\<forall>v\<in>M n1 tr1. \<exists>v'\<in>M n1 tr1. fst v < fst v' \<and> (snd v, snd v') \<in> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>}; tr \<in> exec_trace GGamma gf; \<forall>i. \<exists>y\<in>M n1 tr1. \<exists>j. i < fst y \<and> i < fst (snd y) \<and> (snd y, j, tr') \<in> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>}\<rbrakk> \<Longrightarrow> tr'|\<^bsub>{..n1}\<^esub> = tr1|\<^bsub>{..n1}\<^esub> \<and> trace_end tr' = None \<and> tr' \<in> c_trace SGamma proof (prove)
goal (2 subgoals):
 1. \<And>n1 tr1 tr' i a aa b sst gst gf' x. \<lbrakk>\<forall>a aa b. b \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y} \<and> (\<exists>sst. b aa = Some (com, Normal sst) \<and> (\<exists>gst. (\<exists>gf'. tr a = Some [(nn, gst, gf')]) \<and> inp_eqs gst sst \<and> sst \<in> P \<and> sst \<in> I \<and> (tr, b|\<^bsub>{..aa}\<^esub>) \<in> suffix_tuple_closure_inter (set S) \<and> b|\<^bsub>{..n1}\<^esub> = tr1|\<^bsub>{..n1}\<^esub> \<and> n \<le> a \<and> n \<le> aa \<and> n1 \<le> aa)) \<longrightarrow> (\<exists>ab ac ba. ba \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y} \<and> (\<exists>sst. ba ac = Some (com, Normal sst) \<and> (\<exists>gst. (\<exists>gf'. tr ab = Some [(nn, gst, gf')]) \<and> inp_eqs gst sst \<and> sst \<in> P \<and> sst \<in> I \<and> (tr, ba|\<^bsub>{..ac}\<^esub>) \<in> suffix_tuple_closure_inter (set S) \<and> ba|\<^bsub>{..n1}\<^esub> = tr1|\<^bsub>{..n1}\<^esub> \<and> n \<le> ab \<and> n \<le> ac \<and> n1 \<le> ac)) \<and> a < ab \<and> aa < ac \<and> b|\<^bsub>{..aa}\<^esub> = ba|\<^bsub>{..aa}\<^esub>); tr \<in> exec_trace GGamma gf; b \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; i < a; b aa = Some (com, Normal sst); i < aa; tr a = Some [(nn, gst, gf')]; b|\<^bsub>{..aa}\<^esub> = tr'|\<^bsub>{..aa}\<^esub>; aa < x; inp_eqs gst sst; sst \<in> P; sst \<in> I; (tr, tr'|\<^bsub>{..aa}\<^esub>) \<in> suffix_tuple_closure_inter (set S); b|\<^bsub>{..n1}\<^esub> = tr1|\<^bsub>{..n1}\<^esub>; n \<le> a; n \<le> aa; n1 \<le> aa\<rbrakk> \<Longrightarrow> \<exists>j\<ge>i. \<exists>y. tr j = Some y
 2. \<And>v' n1 tr1 tr'. \<lbrakk>\<forall>v\<in>M n1 tr1. \<exists>v'\<in>M n1 tr1. fst v < fst v' \<and> (snd v, snd v') \<in> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>}; tr \<in> exec_trace GGamma gf; \<forall>i. \<exists>y\<in>M n1 tr1. \<exists>j. i < fst y \<and> i < fst (snd y) \<and> (snd y, j, tr') \<in> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>}\<rbrakk> \<Longrightarrow> tr'|\<^bsub>{..n1}\<^esub> = tr1|\<^bsub>{..n1}\<^esub> \<and> trace_end tr' = None \<and> tr' \<in> c_trace SGamma proof (prove)
goal (1 subgoal):
 1. \<And>v' n1 tr1 tr'. \<lbrakk>\<forall>v\<in>M n1 tr1. \<exists>v'\<in>M n1 tr1. fst v < fst v' \<and> (snd v, snd v') \<in> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>}; tr \<in> exec_trace GGamma gf; \<forall>i. \<exists>y\<in>M n1 tr1. \<exists>j. i < fst y \<and> i < fst (snd y) \<and> (snd y, j, tr') \<in> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>}\<rbrakk> \<Longrightarrow> tr'|\<^bsub>{..n1}\<^esub> = tr1|\<^bsub>{..n1}\<^esub> \<and> trace_end tr' = None \<and> tr' \<in> c_trace SGamma proof (prove)
goal (1 subgoal):
 1. \<And>n1 tr1 tr'. \<lbrakk>\<forall>v\<in>M n1 tr1. \<exists>v'\<in>M n1 tr1. fst v < fst v' \<and> (case snd v of (i, tr) \<Rightarrow> \<lambda>(j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>) (snd v'); tr \<in> exec_trace GGamma gf; \<forall>i. \<exists>y\<in>M n1 tr1. i < fst y \<and> i < fst (snd y) \<and> (\<exists>j. (case snd y of (i, tr) \<Rightarrow> \<lambda>(j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>) (j, tr'))\<rbrakk> \<Longrightarrow> tr'|\<^bsub>{..n1}\<^esub> = tr1|\<^bsub>{..n1}\<^esub> \<and> trace_end tr' = None \<and> tr' \<in> nat_trace_rel (Not \<circ> final) {(x, y). SGamma\<turnstile> x \<rightarrow> y} proof (prove)
goal (2 subgoals):
 1. \<And>n1 tr1 tr'. \<lbrakk>\<forall>v\<in>M n1 tr1. \<exists>v'\<in>M n1 tr1. fst v < fst v' \<and> (case snd v of (i, tr) \<Rightarrow> \<lambda>(j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>) (snd v'); tr \<in> exec_trace GGamma gf; \<forall>i. \<exists>y\<in>M n1 tr1. i < fst y \<and> i < fst (snd y) \<and> (\<exists>j. (case snd y of (i, tr) \<Rightarrow> \<lambda>(j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>) (j, tr'))\<rbrakk> \<Longrightarrow> tr'|\<^bsub>{..n1}\<^esub> = tr1|\<^bsub>{..n1}\<^esub>
 2. \<And>n1 tr1 tr'. \<lbrakk>\<forall>v\<in>M n1 tr1. \<exists>v'\<in>M n1 tr1. fst v < fst v' \<and> (case snd v of (i, tr) \<Rightarrow> \<lambda>(j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>) (snd v'); tr \<in> exec_trace GGamma gf; \<forall>i. \<exists>y\<in>M n1 tr1. i < fst y \<and> i < fst (snd y) \<and> (\<exists>j. (case snd y of (i, tr) \<Rightarrow> \<lambda>(j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>) (j, tr'))\<rbrakk> \<Longrightarrow> trace_end tr' = None \<and> tr' \<in> nat_trace_rel (Not \<circ> final) {(x, y). SGamma\<turnstile> x \<rightarrow> y} proof (prove)
goal (2 subgoals):
 1. \<And>n1 tr1 tr'. \<lbrakk>\<forall>v\<in>M n1 tr1. \<exists>v'\<in>M n1 tr1. fst v < fst v' \<and> (case snd v of (i, tr) \<Rightarrow> \<lambda>(j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>) (snd v'); tr \<in> exec_trace GGamma gf; \<exists>y\<in>M n1 tr1. 0 < fst y \<and> 0 < fst (snd y) \<and> (\<exists>j. (case snd y of (i, tr) \<Rightarrow> \<lambda>(j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>) (j, tr'))\<rbrakk> \<Longrightarrow> tr'|\<^bsub>{..n1}\<^esub> = tr1|\<^bsub>{..n1}\<^esub>
 2. \<And>n1 tr1 tr'. \<lbrakk>\<forall>v\<in>M n1 tr1. \<exists>v'\<in>M n1 tr1. fst v < fst v' \<and> (case snd v of (i, tr) \<Rightarrow> \<lambda>(j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>) (snd v'); tr \<in> exec_trace GGamma gf; \<forall>i. \<exists>y\<in>M n1 tr1. i < fst y \<and> i < fst (snd y) \<and> (\<exists>j. (case snd y of (i, tr) \<Rightarrow> \<lambda>(j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>) (j, tr'))\<rbrakk> \<Longrightarrow> trace_end tr' = None \<and> tr' \<in> nat_trace_rel (Not \<circ> final) {(x, y). SGamma\<turnstile> x \<rightarrow> y} proof (prove)
goal (2 subgoals):
 1. \<And>n1 tr1 tr' a aa b sst gst gf' x. \<lbrakk>\<forall>a aa b. b \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y} \<and> (\<exists>sst. b aa = Some (com, Normal sst) \<and> (\<exists>gst. (\<exists>gf'. tr a = Some [(nn, gst, gf')]) \<and> inp_eqs gst sst \<and> sst \<in> P \<and> sst \<in> I \<and> (tr, b|\<^bsub>{..aa}\<^esub>) \<in> suffix_tuple_closure_inter (set S) \<and> b|\<^bsub>{..n1}\<^esub> = tr1|\<^bsub>{..n1}\<^esub> \<and> n \<le> a \<and> n \<le> aa \<and> n1 \<le> aa)) \<longrightarrow> (\<exists>ab ac ba. ba \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y} \<and> (\<exists>sst. ba ac = Some (com, Normal sst) \<and> (\<exists>gst. (\<exists>gf'. tr ab = Some [(nn, gst, gf')]) \<and> inp_eqs gst sst \<and> sst \<in> P \<and> sst \<in> I \<and> (tr, ba|\<^bsub>{..ac}\<^esub>) \<in> suffix_tuple_closure_inter (set S) \<and> ba|\<^bsub>{..n1}\<^esub> = tr1|\<^bsub>{..n1}\<^esub> \<and> n \<le> ab \<and> n \<le> ac \<and> n1 \<le> ac)) \<and> a < ab \<and> aa < ac \<and> b|\<^bsub>{..aa}\<^esub> = ba|\<^bsub>{..aa}\<^esub>); tr \<in> exec_trace GGamma gf; b \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; 0 < a; b aa = Some (com, Normal sst); 0 < aa; tr a = Some [(nn, gst, gf')]; b|\<^bsub>{..aa}\<^esub> = tr'|\<^bsub>{..aa}\<^esub>; aa < x; inp_eqs gst sst; sst \<in> P; sst \<in> I; (tr, tr'|\<^bsub>{..aa}\<^esub>) \<in> suffix_tuple_closure_inter (set S); b|\<^bsub>{..n1}\<^esub> = tr1|\<^bsub>{..n1}\<^esub>; n \<le> a; n \<le> aa; n1 \<le> aa\<rbrakk> \<Longrightarrow> tr'|\<^bsub>{..n1}\<^esub> = tr1|\<^bsub>{..n1}\<^esub>
 2. \<And>n1 tr1 tr'. \<lbrakk>\<forall>v\<in>M n1 tr1. \<exists>v'\<in>M n1 tr1. fst v < fst v' \<and> (case snd v of (i, tr) \<Rightarrow> \<lambda>(j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>) (snd v'); tr \<in> exec_trace GGamma gf; \<forall>i. \<exists>y\<in>M n1 tr1. i < fst y \<and> i < fst (snd y) \<and> (\<exists>j. (case snd y of (i, tr) \<Rightarrow> \<lambda>(j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>) (j, tr'))\<rbrakk> \<Longrightarrow> trace_end tr' = None \<and> tr' \<in> nat_trace_rel (Not \<circ> final) {(x, y). SGamma\<turnstile> x \<rightarrow> y} proof (prove)
goal (2 subgoals):
 1. \<And>n1 tr1 tr' a aa b sst gst gf' x. \<lbrakk>\<forall>a aa b. b \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y} \<and> (\<exists>sst. b aa = Some (com, Normal sst) \<and> (\<exists>gst. (\<exists>gf'. tr a = Some [(nn, gst, gf')]) \<and> inp_eqs gst sst \<and> sst \<in> P \<and> sst \<in> I \<and> (tr, b|\<^bsub>{..aa}\<^esub>) \<in> suffix_tuple_closure_inter (set S) \<and> b|\<^bsub>{..n1}\<^esub> = tr1|\<^bsub>{..n1}\<^esub> \<and> n \<le> a \<and> n \<le> aa \<and> n1 \<le> aa)) \<longrightarrow> (\<exists>ab ac ba. ba \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y} \<and> (\<exists>sst. ba ac = Some (com, Normal sst) \<and> (\<exists>gst. (\<exists>gf'. tr ab = Some [(nn, gst, gf')]) \<and> inp_eqs gst sst \<and> sst \<in> P \<and> sst \<in> I \<and> (tr, ba|\<^bsub>{..ac}\<^esub>) \<in> suffix_tuple_closure_inter (set S) \<and> ba|\<^bsub>{..n1}\<^esub> = tr1|\<^bsub>{..n1}\<^esub> \<and> n \<le> ab \<and> n \<le> ac \<and> n1 \<le> ac)) \<and> a < ab \<and> aa < ac \<and> b|\<^bsub>{..aa}\<^esub> = ba|\<^bsub>{..aa}\<^esub>); tr \<in> exec_trace GGamma gf; b \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; 0 < a; b aa = Some (com, Normal sst); 0 < aa; tr a = Some [(nn, gst, gf')]; aa < x; inp_eqs gst sst; sst \<in> P; sst \<in> I; (tr, tr'|\<^bsub>{..aa}\<^esub>) \<in> suffix_tuple_closure_inter (set S); b|\<^bsub>{..n1}\<^esub> = tr1|\<^bsub>{..n1}\<^esub>; n \<le> a; n \<le> aa; n1 \<le> aa; b|\<^bsub>{..n1}\<^esub> = tr'|\<^bsub>{..n1}\<^esub>\<rbrakk> \<Longrightarrow> tr'|\<^bsub>{..n1}\<^esub> = tr1|\<^bsub>{..n1}\<^esub>
 2. \<And>n1 tr1 tr'. \<lbrakk>\<forall>v\<in>M n1 tr1. \<exists>v'\<in>M n1 tr1. fst v < fst v' \<and> (case snd v of (i, tr) \<Rightarrow> \<lambda>(j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>) (snd v'); tr \<in> exec_trace GGamma gf; \<forall>i. \<exists>y\<in>M n1 tr1. i < fst y \<and> i < fst (snd y) \<and> (\<exists>j. (case snd y of (i, tr) \<Rightarrow> \<lambda>(j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>) (j, tr'))\<rbrakk> \<Longrightarrow> trace_end tr' = None \<and> tr' \<in> nat_trace_rel (Not \<circ> final) {(x, y). SGamma\<turnstile> x \<rightarrow> y} proof (prove)
goal (1 subgoal):
 1. \<And>n1 tr1 tr'. \<lbrakk>\<forall>v\<in>M n1 tr1. \<exists>v'\<in>M n1 tr1. fst v < fst v' \<and> (case snd v of (i, tr) \<Rightarrow> \<lambda>(j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>) (snd v'); tr \<in> exec_trace GGamma gf; \<forall>i. \<exists>y\<in>M n1 tr1. i < fst y \<and> i < fst (snd y) \<and> (\<exists>j. (case snd y of (i, tr) \<Rightarrow> \<lambda>(j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>) (j, tr'))\<rbrakk> \<Longrightarrow> trace_end tr' = None \<and> tr' \<in> nat_trace_rel (Not \<circ> final) {(x, y). SGamma\<turnstile> x \<rightarrow> y} proof (prove)
goal (1 subgoal):
 1. \<And>n1 tr1 tr'. \<lbrakk>\<forall>v\<in>M n1 tr1. \<exists>v'\<in>M n1 tr1. fst v < fst v' \<and> (case snd v of (i, tr) \<Rightarrow> \<lambda>(j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>) (snd v'); tr \<in> exec_trace GGamma gf; \<forall>i. \<exists>y\<in>M n1 tr1. i < fst y \<and> i < fst (snd y) \<and> (\<exists>j. (case snd y of (i, tr) \<Rightarrow> \<lambda>(j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>) (j, tr'))\<rbrakk> \<Longrightarrow> \<forall>i. \<exists>j tr k. i \<le> j \<and> tr j \<noteq> None \<and> ((j, tr), k, tr') \<in> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>} \<and> tr \<in> nat_trace_rel (?c120 n1 tr1 tr') {(x, y). SGamma\<turnstile> x \<rightarrow> y} proof (prove)
goal (1 subgoal):
 1. \<And>n1 tr1 tr' i. \<lbrakk>\<forall>v\<in>M n1 tr1. \<exists>v'\<in>M n1 tr1. fst v < fst v' \<and> (case snd v of (i, tr) \<Rightarrow> \<lambda>(j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>) (snd v'); tr \<in> exec_trace GGamma gf; \<forall>i. \<exists>y\<in>M n1 tr1. i < fst y \<and> i < fst (snd y) \<and> (\<exists>j. (case snd y of (i, tr) \<Rightarrow> \<lambda>(j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>) (j, tr'))\<rbrakk> \<Longrightarrow> \<exists>j\<ge>i. \<exists>tr. (\<exists>a b. tr j = Some (a, b)) \<and> Ex ((<) j) \<and> tr|\<^bsub>{..j}\<^esub> = tr'|\<^bsub>{..j}\<^esub> \<and> tr \<in> nat_trace_rel (?c120 n1 tr1 tr') {(x, y). SGamma\<turnstile> x \<rightarrow> y} proof (prove)
goal (1 subgoal):
 1. \<And>n1 tr1 tr' i. \<lbrakk>\<forall>v\<in>M n1 tr1. \<exists>v'\<in>M n1 tr1. fst v < fst v' \<and> (case snd v of (i, tr) \<Rightarrow> \<lambda>(j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>) (snd v'); tr \<in> exec_trace GGamma gf; \<exists>y\<in>M n1 tr1. i < fst y \<and> i < fst (snd y) \<and> (\<exists>j. (case snd y of (i, tr) \<Rightarrow> \<lambda>(j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>) (j, tr'))\<rbrakk> \<Longrightarrow> \<exists>j\<ge>i. \<exists>tr. (\<exists>a b. tr j = Some (a, b)) \<and> Ex ((<) j) \<and> tr|\<^bsub>{..j}\<^esub> = tr'|\<^bsub>{..j}\<^esub> \<and> tr \<in> nat_trace_rel (?c120 n1 tr1 tr') {(x, y). SGamma\<turnstile> x \<rightarrow> y} proof (prove)
goal (1 subgoal):
 1. \<And>n1 tr1 tr' i a aa b sst gst gf' x. \<lbrakk>\<forall>a aa b. b \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y} \<and> (\<exists>sst. b aa = Some (com, Normal sst) \<and> (\<exists>gst. (\<exists>gf'. tr a = Some [(nn, gst, gf')]) \<and> inp_eqs gst sst \<and> sst \<in> P \<and> sst \<in> I \<and> (tr, b|\<^bsub>{..aa}\<^esub>) \<in> suffix_tuple_closure_inter (set S) \<and> b|\<^bsub>{..n1}\<^esub> = tr1|\<^bsub>{..n1}\<^esub> \<and> n \<le> a \<and> n \<le> aa \<and> n1 \<le> aa)) \<longrightarrow> (\<exists>ab ac ba. ba \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y} \<and> (\<exists>sst. ba ac = Some (com, Normal sst) \<and> (\<exists>gst. (\<exists>gf'. tr ab = Some [(nn, gst, gf')]) \<and> inp_eqs gst sst \<and> sst \<in> P \<and> sst \<in> I \<and> (tr, ba|\<^bsub>{..ac}\<^esub>) \<in> suffix_tuple_closure_inter (set S) \<and> ba|\<^bsub>{..n1}\<^esub> = tr1|\<^bsub>{..n1}\<^esub> \<and> n \<le> ab \<and> n \<le> ac \<and> n1 \<le> ac)) \<and> a < ab \<and> aa < ac \<and> b|\<^bsub>{..aa}\<^esub> = ba|\<^bsub>{..aa}\<^esub>); tr \<in> exec_trace GGamma gf; b \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; i < a; b aa = Some (com, Normal sst); i < aa; tr a = Some [(nn, gst, gf')]; b|\<^bsub>{..aa}\<^esub> = tr'|\<^bsub>{..aa}\<^esub>; aa < x; inp_eqs gst sst; sst \<in> P; sst \<in> I; (tr, tr'|\<^bsub>{..aa}\<^esub>) \<in> suffix_tuple_closure_inter (set S); b|\<^bsub>{..n1}\<^esub> = tr1|\<^bsub>{..n1}\<^esub>; n \<le> a; n \<le> aa; n1 \<le> aa\<rbrakk> \<Longrightarrow> \<exists>j\<ge>i. \<exists>tr. (\<exists>a b. tr j = Some (a, b)) \<and> Ex ((<) j) \<and> tr|\<^bsub>{..j}\<^esub> = tr'|\<^bsub>{..j}\<^esub> \<and> tr \<in> nat_trace_rel (?c120 n1 tr1 tr') {(x, y). SGamma\<turnstile> x \<rightarrow> y} proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrakk>\<forall>v\<in>M ?n1.0 ?tr1.0. \<exists>v'\<in>M ?n1.0 ?tr1.0. fst v < fst v' \<and> (snd v, snd v') \<in> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>}; tr \<in> exec_trace GGamma gf; ?v' \<in> M ?n1.0 ?tr1.0\<rbrakk> \<Longrightarrow> \<exists>tr'. trace_end tr = None \<and> tr'|\<^bsub>{..?n1.0}\<^esub> = ?tr1.0|\<^bsub>{..?n1.0}\<^esub> \<and> trace_end tr' = None \<and> tr' \<in> c_trace SGamma

goal (1 subgoal):
 1. simpl_to_graph SGamma GGamma gf nn com n ({tr} \<times> UNIV # S) P I inp_eqs out_eqs proof (prove)
goal (1 subgoal):
 1. simpl_to_graph SGamma GGamma gf nn com n ({tr} \<times> UNIV # S) P I inp_eqs out_eqs proof (prove)
goal (1 subgoal):
 1. \<And>gst sst n' gf' tr' n''. \<lbrakk>tr n' = Some [(nn, gst, gf')]; sst \<in> P; sst \<in> I; inp_eqs gst sst; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma gf; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set S); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (com, Normal sst)\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'') proof (prove)
goal (2 subgoals):
 1. \<And>gst sst n' gf' tr' n''. \<lbrakk>tr n' = Some [(nn, gst, gf')]; sst \<in> P; sst \<in> I; inp_eqs gst sst; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma gf; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set S); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (com, Normal sst); \<forall>v\<in>M n'' tr'. \<exists>v'\<in>M n'' tr'. fst v < fst v' \<and> (snd v, snd v') \<in> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>}\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'')
 2. \<And>gst sst n' gf' tr' n''. \<lbrakk>tr n' = Some [(nn, gst, gf')]; sst \<in> P; sst \<in> I; inp_eqs gst sst; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma gf; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set S); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (com, Normal sst); \<not> (\<forall>v\<in>M n'' tr'. \<exists>v'\<in>M n'' tr'. fst v < fst v' \<and> (snd v, snd v') \<in> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>})\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'') proof (prove)
goal (3 subgoals):
 1. \<And>gst sst n' gf' tr' n''. \<lbrakk>tr n' = Some [(nn, gst, gf')]; sst \<in> P; sst \<in> I; inp_eqs gst sst; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma gf; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set S); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (com, Normal sst)\<rbrakk> \<Longrightarrow> ?v'31 gst sst n' gf' tr' n'' \<in> M n'' tr'
 2. \<And>gst sst n' gf' tr' n''. \<lbrakk>tr n' = Some [(nn, gst, gf')]; sst \<in> P; sst \<in> I; inp_eqs gst sst; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma gf; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set S); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (com, Normal sst); \<exists>tr'a. trace_end tr = None \<and> tr'a|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end tr'a = None \<and> tr'a \<in> c_trace SGamma\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'')
 3. \<And>gst sst n' gf' tr' n''. \<lbrakk>tr n' = Some [(nn, gst, gf')]; sst \<in> P; sst \<in> I; inp_eqs gst sst; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma gf; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set S); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (com, Normal sst); \<not> (\<forall>v\<in>M n'' tr'. \<exists>v'\<in>M n'' tr'. fst v < fst v' \<and> (snd v, snd v') \<in> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>})\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'') proof (prove)
goal (2 subgoals):
 1. \<And>gst sst n' gf' tr' n''. \<lbrakk>tr n' = Some [(nn, gst, gf')]; sst \<in> P; sst \<in> I; inp_eqs gst sst; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma gf; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set S); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (com, Normal sst); \<exists>tr'a. trace_end tr = None \<and> tr'a|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end tr'a = None \<and> tr'a \<in> c_trace SGamma\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'')
 2. \<And>gst sst n' gf' tr' n''. \<lbrakk>tr n' = Some [(nn, gst, gf')]; sst \<in> P; sst \<in> I; inp_eqs gst sst; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma gf; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set S); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (com, Normal sst); \<not> (\<forall>v\<in>M n'' tr'. \<exists>v'\<in>M n'' tr'. fst v < fst v' \<and> (snd v, snd v') \<in> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>})\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'') proof (prove)
goal (1 subgoal):
 1. \<And>gst sst n' gf' tr' n''. \<lbrakk>tr n' = Some [(nn, gst, gf')]; sst \<in> P; sst \<in> I; inp_eqs gst sst; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma gf; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set S); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (com, Normal sst); \<not> (\<forall>v\<in>M n'' tr'. \<exists>v'\<in>M n'' tr'. fst v < fst v' \<and> (snd v, snd v') \<in> {((i, tr), j, tr'). i < j \<and> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub>})\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'') proof (prove)
goal (1 subgoal):
 1. \<And>gst sst n' gf' tr' n'' a aa b. \<lbrakk>tr n' = Some [(nn, gst, gf')]; sst \<in> P; sst \<in> I; inp_eqs gst sst; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma gf; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set S); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (com, Normal sst); (a, aa, b) \<in> M n'' tr'; \<forall>v'\<in>M n'' tr'. a < fst v' \<longrightarrow> \<not> (case snd v' of (j, tr') \<Rightarrow> aa < j \<and> b|\<^bsub>{..aa}\<^esub> = tr'|\<^bsub>{..aa}\<^esub>)\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'') proof (prove)
goal (1 subgoal):
 1. \<And>gst sst n' gf' tr' n'' a aa b. \<lbrakk>tr n' = Some [(nn, gst, gf')]; sst \<in> P; sst \<in> I; inp_eqs gst sst; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma gf; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set S); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (com, Normal sst); (a, aa, b) \<in> M n'' tr'; \<forall>v'\<in>M n'' tr'. a < fst v' \<longrightarrow> \<not> (case snd v' of (j, tr') \<Rightarrow> aa < j \<and> b|\<^bsub>{..aa}\<^esub> = tr'|\<^bsub>{..aa}\<^esub>); \<exists>tr'. tr' \<in> c_trace SGamma \<and> tr'|\<^bsub>{..aa}\<^esub> = b|\<^bsub>{..aa}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr')\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'') proof (prove)
goal (1 subgoal):
 1. \<And>gst sst n' gf' tr' n'' a aa b soln_tr'. \<lbrakk>tr n' = Some [(nn, gst, gf')]; sst \<in> P; sst \<in> I; inp_eqs gst sst; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma gf; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set S); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (com, Normal sst); (a, aa, b) \<in> M n'' tr'; \<forall>v'\<in>M n'' tr'. a < fst v' \<longrightarrow> \<not> (case snd v' of (j, tr') \<Rightarrow> aa < j \<and> b|\<^bsub>{..aa}\<^esub> = tr'|\<^bsub>{..aa}\<^esub>); soln_tr' \<in> c_trace SGamma; soln_tr'|\<^bsub>{..aa}\<^esub> = b|\<^bsub>{..aa}\<^esub>; trace_end_match out_eqs I (trace_end tr) (trace_end soln_tr')\<rbrakk> \<Longrightarrow> soln_tr' \<in> c_trace SGamma \<and> soln_tr'|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end soln_tr') proof (prove)
goal (1 subgoal):
 1. \<And>gst sst n' gf' tr' n'' a aa b soln_tr' ssta gsta gf'a. \<lbrakk>tr n' = Some [(nn, gst, gf')]; sst \<in> P; sst \<in> I; inp_eqs gst sst; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma gf; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set S); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (com, Normal sst); \<forall>ab ac ba. ba \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y} \<and> (\<exists>sst. ba ac = Some (com, Normal sst) \<and> (\<exists>gst. (\<exists>gf'. tr ab = Some [(nn, gst, gf')]) \<and> inp_eqs gst sst \<and> sst \<in> P \<and> sst \<in> I \<and> (tr, ba|\<^bsub>{..ac}\<^esub>) \<in> suffix_tuple_closure_inter (set S) \<and> ba|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> n \<le> ab \<and> n \<le> ac \<and> n'' \<le> ac)) \<longrightarrow> a < ab \<longrightarrow> aa < ac \<longrightarrow> b|\<^bsub>{..aa}\<^esub> \<noteq> ba|\<^bsub>{..aa}\<^esub>; soln_tr' \<in> c_trace SGamma; soln_tr'|\<^bsub>{..aa}\<^esub> = b|\<^bsub>{..aa}\<^esub>; trace_end_match out_eqs I (trace_end tr) (trace_end soln_tr'); b \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; b aa = Some (com, Normal ssta); tr a = Some [(nn, gsta, gf'a)]; inp_eqs gsta ssta; ssta \<in> P; ssta \<in> I; (tr, b|\<^bsub>{..aa}\<^esub>) \<in> suffix_tuple_closure_inter (set S); b|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub>; n \<le> a; n'' \<le> aa\<rbrakk> \<Longrightarrow> soln_tr'|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> proof (prove)
goal (1 subgoal):
 1. \<And>gst sst n' gf' tr' n'' a aa b soln_tr' ssta gsta gf'a. \<lbrakk>tr n' = Some [(nn, gst, gf')]; sst \<in> P; sst \<in> I; inp_eqs gst sst; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma gf; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set S); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (com, Normal sst); \<forall>ab ac ba. ba \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y} \<and> (\<exists>sst. ba ac = Some (com, Normal sst) \<and> (\<exists>gst. (\<exists>gf'. tr ab = Some [(nn, gst, gf')]) \<and> inp_eqs gst sst \<and> sst \<in> P \<and> sst \<in> I \<and> (tr, ba|\<^bsub>{..ac}\<^esub>) \<in> suffix_tuple_closure_inter (set S) \<and> ba|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> n \<le> ab \<and> n \<le> ac \<and> n'' \<le> ac)) \<longrightarrow> a < ab \<longrightarrow> aa < ac \<longrightarrow> b|\<^bsub>{..aa}\<^esub> \<noteq> ba|\<^bsub>{..aa}\<^esub>; soln_tr' \<in> c_trace SGamma; trace_end_match out_eqs I (trace_end tr) (trace_end soln_tr'); b \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; b aa = Some (com, Normal ssta); tr a = Some [(nn, gsta, gf'a)]; inp_eqs gsta ssta; ssta \<in> P; ssta \<in> I; (tr, b|\<^bsub>{..aa}\<^esub>) \<in> suffix_tuple_closure_inter (set S); b|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub>; n \<le> a; n'' \<le> aa; soln_tr'|\<^bsub>{..n''}\<^esub> = b|\<^bsub>{..n''}\<^esub>\<rbrakk> \<Longrightarrow> soln_tr'|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> proof (prove)
goal:
No subgoals! proof (state)
this:
simpl_to_graph SGamma GGamma gf nn com n ({tr} \<times> UNIV # S) P I inp_eqs out_eqs

goal:
No subgoals!