theory CSpace_I

lemma next_trancl_split_tt:
  assumes p1: "m \<turnstile> x \<leadsto>\<^sup>+ y"
  and     p2: "m \<turnstile> x \<leadsto>\<^sup>+ p"
  and     nm: "\<not> m \<turnstile> p \<leadsto>\<^sup>* y"
  shows "m \<turnstile> y \<leadsto>\<^sup>* p" using p2 p1 nm proof induct case base thus ?case by (clarsimp dest!: tranclD) (drule (1)  next_single_value, simp) next case (step q r) show ?case proof (cases "q = y") case True thus ?thesis using step by fastforce next case False have "m \<turnstile> y \<leadsto>\<^sup>* q" proof (rule step.hyps) have "\<not> m \<turnstile> q \<leadsto>\<^sup>+ y" by (rule neg_next_rtrancl_trancl) fact+ thus "\<not> m \<turnstile> q \<leadsto>\<^sup>* y" using False by (clarsimp dest!: rtranclD) qed fact+ thus ?thesis by (rule rtrancl_into_rtrancl) fact+ qed qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<turnstile> y \<leadsto>\<^sup>* p proof (prove)
using this:
m \<turnstile> x \<leadsto>\<^sup>+ p
m \<turnstile> x \<leadsto>\<^sup>+ y
(p, y) \<notin> (mdb_next_rel m)\<^sup>*

goal (1 subgoal):
 1. m \<turnstile> y \<leadsto>\<^sup>* p proof (state)
goal (2 subgoals):
 1. \<And>ya. \<lbrakk>m \<turnstile> x \<leadsto> ya; m \<turnstile> x \<leadsto>\<^sup>+ y; (ya, y) \<notin> (mdb_next_rel m)\<^sup>*\<rbrakk> \<Longrightarrow> m \<turnstile> y \<leadsto>\<^sup>* ya
 2. \<And>ya z. \<lbrakk>m \<turnstile> x \<leadsto>\<^sup>+ ya; m \<turnstile> ya \<leadsto> z; \<lbrakk>m \<turnstile> x \<leadsto>\<^sup>+ y; (ya, y) \<notin> (mdb_next_rel m)\<^sup>*\<rbrakk> \<Longrightarrow> m \<turnstile> y \<leadsto>\<^sup>* ya; m \<turnstile> x \<leadsto>\<^sup>+ y; (z, y) \<notin> (mdb_next_rel m)\<^sup>*\<rbrakk> \<Longrightarrow> m \<turnstile> y \<leadsto>\<^sup>* z proof (state)
this:
m \<turnstile> x \<leadsto> y_
m \<turnstile> x \<leadsto>\<^sup>+ y
(y_, y) \<notin> (mdb_next_rel m)\<^sup>*

goal (2 subgoals):
 1. \<And>ya. \<lbrakk>m \<turnstile> x \<leadsto> ya; m \<turnstile> x \<leadsto>\<^sup>+ y; (ya, y) \<notin> (mdb_next_rel m)\<^sup>*\<rbrakk> \<Longrightarrow> m \<turnstile> y \<leadsto>\<^sup>* ya
 2. \<And>ya z. \<lbrakk>m \<turnstile> x \<leadsto>\<^sup>+ ya; m \<turnstile> ya \<leadsto> z; \<lbrakk>m \<turnstile> x \<leadsto>\<^sup>+ y; (ya, y) \<notin> (mdb_next_rel m)\<^sup>*\<rbrakk> \<Longrightarrow> m \<turnstile> y \<leadsto>\<^sup>* ya; m \<turnstile> x \<leadsto>\<^sup>+ y; (z, y) \<notin> (mdb_next_rel m)\<^sup>*\<rbrakk> \<Longrightarrow> m \<turnstile> y \<leadsto>\<^sup>* z proof (prove)
using this:
m \<turnstile> x \<leadsto> y_
m \<turnstile> x \<leadsto>\<^sup>+ y
(y_, y) \<notin> (mdb_next_rel m)\<^sup>*

goal (1 subgoal):
 1. m \<turnstile> y \<leadsto>\<^sup>* y_ proof (state)
this:
m \<turnstile> y \<leadsto>\<^sup>* y_

goal (1 subgoal):
 1. \<And>ya z. \<lbrakk>m \<turnstile> x \<leadsto>\<^sup>+ ya; m \<turnstile> ya \<leadsto> z; \<lbrakk>m \<turnstile> x \<leadsto>\<^sup>+ y; (ya, y) \<notin> (mdb_next_rel m)\<^sup>*\<rbrakk> \<Longrightarrow> m \<turnstile> y \<leadsto>\<^sup>* ya; m \<turnstile> x \<leadsto>\<^sup>+ y; (z, y) \<notin> (mdb_next_rel m)\<^sup>*\<rbrakk> \<Longrightarrow> m \<turnstile> y \<leadsto>\<^sup>* z proof (state)
goal (1 subgoal):
 1. \<And>ya z. \<lbrakk>m \<turnstile> x \<leadsto>\<^sup>+ ya; m \<turnstile> ya \<leadsto> z; \<lbrakk>m \<turnstile> x \<leadsto>\<^sup>+ y; (ya, y) \<notin> (mdb_next_rel m)\<^sup>*\<rbrakk> \<Longrightarrow> m \<turnstile> y \<leadsto>\<^sup>* ya; m \<turnstile> x \<leadsto>\<^sup>+ y; (z, y) \<notin> (mdb_next_rel m)\<^sup>*\<rbrakk> \<Longrightarrow> m \<turnstile> y \<leadsto>\<^sup>* z proof (state)
this:
m \<turnstile> x \<leadsto>\<^sup>+ q
m \<turnstile> q \<leadsto> r
\<lbrakk>m \<turnstile> x \<leadsto>\<^sup>+ y; (q, y) \<notin> (mdb_next_rel m)\<^sup>*\<rbrakk> \<Longrightarrow> m \<turnstile> y \<leadsto>\<^sup>* q
m \<turnstile> x \<leadsto>\<^sup>+ y
(r, y) \<notin> (mdb_next_rel m)\<^sup>*

goal (1 subgoal):
 1. \<And>ya z. \<lbrakk>m \<turnstile> x \<leadsto>\<^sup>+ ya; m \<turnstile> ya \<leadsto> z; \<lbrakk>m \<turnstile> x \<leadsto>\<^sup>+ y; (ya, y) \<notin> (mdb_next_rel m)\<^sup>*\<rbrakk> \<Longrightarrow> m \<turnstile> y \<leadsto>\<^sup>* ya; m \<turnstile> x \<leadsto>\<^sup>+ y; (z, y) \<notin> (mdb_next_rel m)\<^sup>*\<rbrakk> \<Longrightarrow> m \<turnstile> y \<leadsto>\<^sup>* z proof (prove)
goal (1 subgoal):
 1. m \<turnstile> y \<leadsto>\<^sup>* r proof (state)
goal (2 subgoals):
 1. q = y \<Longrightarrow> m \<turnstile> y \<leadsto>\<^sup>* r
 2. q \<noteq> y \<Longrightarrow> m \<turnstile> y \<leadsto>\<^sup>* r proof (state)
this:
q = y

goal (2 subgoals):
 1. q = y \<Longrightarrow> m \<turnstile> y \<leadsto>\<^sup>* r
 2. q \<noteq> y \<Longrightarrow> m \<turnstile> y \<leadsto>\<^sup>* r proof (prove)
using this:
q = y

goal (1 subgoal):
 1. m \<turnstile> y \<leadsto>\<^sup>* r proof (prove)
using this:
q = y
m \<turnstile> x \<leadsto>\<^sup>+ q
m \<turnstile> q \<leadsto> r
\<lbrakk>m \<turnstile> x \<leadsto>\<^sup>+ y; (q, y) \<notin> (mdb_next_rel m)\<^sup>*\<rbrakk> \<Longrightarrow> m \<turnstile> y \<leadsto>\<^sup>* q
m \<turnstile> x \<leadsto>\<^sup>+ y
(r, y) \<notin> (mdb_next_rel m)\<^sup>*

goal (1 subgoal):
 1. m \<turnstile> y \<leadsto>\<^sup>* r proof (state)
this:
m \<turnstile> y \<leadsto>\<^sup>* r

goal (1 subgoal):
 1. q \<noteq> y \<Longrightarrow> m \<turnstile> y \<leadsto>\<^sup>* r proof (state)
goal (1 subgoal):
 1. q \<noteq> y \<Longrightarrow> m \<turnstile> y \<leadsto>\<^sup>* r proof (state)
this:
q \<noteq> y

goal (1 subgoal):
 1. q \<noteq> y \<Longrightarrow> m \<turnstile> y \<leadsto>\<^sup>* r proof (prove)
goal (1 subgoal):
 1. m \<turnstile> y \<leadsto>\<^sup>* q proof (state)
goal (2 subgoals):
 1. m \<turnstile> x \<leadsto>\<^sup>+ y
 2. (q, y) \<notin> (mdb_next_rel m)\<^sup>* proof (prove)
goal (1 subgoal):
 1. (q, y) \<notin> (mdb_next_rel m)\<^sup>+ proof (state)
this:
(q, y) \<notin> (mdb_next_rel m)\<^sup>+

goal (2 subgoals):
 1. m \<turnstile> x \<leadsto>\<^sup>+ y
 2. (q, y) \<notin> (mdb_next_rel m)\<^sup>* proof (prove)
using this:
(q, y) \<notin> (mdb_next_rel m)\<^sup>+

goal (1 subgoal):
 1. (q, y) \<notin> (mdb_next_rel m)\<^sup>* proof (prove)
using this:
(q, y) \<notin> (mdb_next_rel m)\<^sup>+
q \<noteq> y

goal (1 subgoal):
 1. (q, y) \<notin> (mdb_next_rel m)\<^sup>* proof (state)
this:
(q, y) \<notin> (mdb_next_rel m)\<^sup>*

goal (1 subgoal):
 1. m \<turnstile> x \<leadsto>\<^sup>+ y proof (state)
this:
m \<turnstile> y \<leadsto>\<^sup>* q

goal (1 subgoal):
 1. q \<noteq> y \<Longrightarrow> m \<turnstile> y \<leadsto>\<^sup>* r proof (prove)
using this:
m \<turnstile> y \<leadsto>\<^sup>* q

goal (1 subgoal):
 1. m \<turnstile> y \<leadsto>\<^sup>* r proof (state)
this:
m \<turnstile> y \<leadsto>\<^sup>* r

goal:
No subgoals! proof (state)
this:
m \<turnstile> y \<leadsto>\<^sup>* r

goal:
No subgoals!