[STATEMENT]
lemma simulation_\<tau>Runs_table1:
  assumes bisim: "s1 \<approx> s2"
  and run1: "trsys1.\<tau>Runs_table s1 stlsss1"
  shows "\<exists>stlsss2. trsys2.\<tau>Runs_table s2 stlsss2 \<and> tllist_all2 (\<lambda>(tl1, s1'') (tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (rel_option bisim) stlsss1 stlsss2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>stlsss2. trsys2.\<tau>Runs_table s2 stlsss2 \<and> tllist_all2 (\<lambda>(tl1, s1'') (tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (rel_option bisim) stlsss1 stlsss2
[PROOF STEP]
proof(intro exI conjI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. trsys2.\<tau>Runs_table s2 ?stlsss2.0
 2. tllist_all2 (\<lambda>(tl1, s1'') (tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (rel_option bisim) stlsss1 ?stlsss2.0
[PROOF STEP]
let ?P = "\<lambda>(s2 :: 's2) (stlsss1 :: ('tl1 \<times> 's1, 's1 option) tllist) (tl2, s2'').
    \<exists>s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> s2' -2-tl2\<rightarrow> s2'' \<and> \<not> \<tau>move2 s2' tl2 s2'' \<and> snd (thd stlsss1) \<approx> s2'' \<and> fst (thd stlsss1) \<sim> tl2"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. trsys2.\<tau>Runs_table s2 ?stlsss2.0
 2. tllist_all2 (\<lambda>(tl1, s1'') (tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (rel_option bisim) stlsss1 ?stlsss2.0
[PROOF STEP]
define tls1_to_tls2 where "tls1_to_tls2 s2 stlsss1 = unfold_tllist
      (\<lambda>(s2, stlsss1). is_TNil stlsss1)
      (\<lambda>(s2, stlsss1). map_option (\<lambda>s1'. SOME s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> (\<forall>tl s2''. \<not> s2' -2-tl\<rightarrow> s2'') \<and> s1' \<approx> s2') (terminal stlsss1))
      (\<lambda>(s2, stlsss1). let (tl2, s2'') = Eps (?P s2 stlsss1) in (tl2, s2''))
      (\<lambda>(s2, stlsss1). let (tl2, s2'') = Eps (?P s2 stlsss1) in (s2'', ttl stlsss1))
      (s2, stlsss1)"
    for s2 stlsss1
[PROOF STATE]
proof (state)
this:
tls1_to_tls2 ?s2.0 ?stlsss1.0 = unfold_tllist (\<lambda>(s2, stlsss1). is_TNil stlsss1) (\<lambda>(s2, stlsss1). map_option (\<lambda>s1'. SOME s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> (\<forall>tl s2''. \<not> s2' -2-tl\<rightarrow> s2'') \<and> s1' \<approx> s2') (terminal stlsss1)) (\<lambda>(s2, stlsss1). let (tl2, s2'') = SOME (tl2, s2''). \<exists>s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> s2' -2-tl2\<rightarrow> s2'' \<and> \<not> \<tau>move2 s2' tl2 s2'' \<and> snd (thd stlsss1) \<approx> s2'' \<and> fst (thd stlsss1) \<sim> tl2 in (tl2, s2'')) (\<lambda>(s2, stlsss1). let (tl2, s2'') = SOME (tl2, s2''). \<exists>s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> s2' -2-tl2\<rightarrow> s2'' \<and> \<not> \<tau>move2 s2' tl2 s2'' \<and> snd (thd stlsss1) \<approx> s2'' \<and> fst (thd stlsss1) \<sim> tl2 in (s2'', ttl stlsss1)) (?s2.0, ?stlsss1.0)

goal (2 subgoals):
 1. trsys2.\<tau>Runs_table s2 ?stlsss2.0
 2. tllist_all2 (\<lambda>(tl1, s1'') (tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (rel_option bisim) stlsss1 ?stlsss2.0
[PROOF STEP]
have [simp]:
    "\<And>s2 stlsss1. is_TNil (tls1_to_tls2 s2 stlsss1) \<longleftrightarrow> is_TNil stlsss1"
    "\<And>s2 stlsss1. is_TNil stlsss1 \<Longrightarrow> terminal (tls1_to_tls2 s2 stlsss1) = map_option (\<lambda>s1'. SOME s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> (\<forall>tl s2''. \<not> s2' -2-tl\<rightarrow> s2'') \<and> s1' \<approx> s2') (terminal stlsss1)"
    "\<And>s2 stlsss1. \<not> is_TNil stlsss1 \<Longrightarrow> thd (tls1_to_tls2 s2 stlsss1) = (let (tl2, s2'') = Eps (?P s2 stlsss1) in (tl2, s2''))"
    "\<And>s2 stlsss1. \<not> is_TNil stlsss1 \<Longrightarrow> ttl (tls1_to_tls2 s2 stlsss1) = (let (tl2, s2'') = Eps (?P s2 stlsss1) in tls1_to_tls2 s2'' (ttl stlsss1))"
    "\<And>s2 os1. tls1_to_tls2 s2 (TNil os1) = 
               TNil (map_option (\<lambda>s1'. SOME s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> (\<forall>tl s2''. \<not> s2' -2-tl\<rightarrow> s2'') \<and> s1' \<approx> s2') os1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<And>s2 stlsss1. is_TNil (tls1_to_tls2 s2 stlsss1) = is_TNil stlsss1) &&& (\<And>s2 stlsss1. is_TNil stlsss1 \<Longrightarrow> terminal (tls1_to_tls2 s2 stlsss1) = map_option (\<lambda>s1'. SOME s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> (\<forall>tl s2''. \<not> s2' -2-tl\<rightarrow> s2'') \<and> s1' \<approx> s2') (terminal stlsss1))) &&& (\<And>s2 stlsss1. \<not> is_TNil stlsss1 \<Longrightarrow> thd (tls1_to_tls2 s2 stlsss1) = (let (tl2, s2'') = SOME (tl2, s2''). \<exists>s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> s2' -2-tl2\<rightarrow> s2'' \<and> \<not> \<tau>move2 s2' tl2 s2'' \<and> snd (thd stlsss1) \<approx> s2'' \<and> fst (thd stlsss1) \<sim> tl2 in (tl2, s2''))) &&& (\<And>s2 stlsss1. \<not> is_TNil stlsss1 \<Longrightarrow> ttl (tls1_to_tls2 s2 stlsss1) = (let (tl2, s2'') = SOME (tl2, s2''). \<exists>s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> s2' -2-tl2\<rightarrow> s2'' \<and> \<not> \<tau>move2 s2' tl2 s2'' \<and> snd (thd stlsss1) \<approx> s2'' \<and> fst (thd stlsss1) \<sim> tl2 in tls1_to_tls2 s2'' (ttl stlsss1))) &&& (\<And>s2 os1. tls1_to_tls2 s2 (TNil os1) = TNil (map_option (\<lambda>s1'. SOME s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> (\<forall>tl s2''. \<not> s2' -2-tl\<rightarrow> s2'') \<and> s1' \<approx> s2') os1))
[PROOF STEP]
by(simp_all add: tls1_to_tls2_def split_beta)
[PROOF STATE]
proof (state)
this:
is_TNil (tls1_to_tls2 ?s2.0 ?stlsss1.0) = is_TNil ?stlsss1.0
is_TNil ?stlsss1.0 \<Longrightarrow> terminal (tls1_to_tls2 ?s2.0 ?stlsss1.0) = map_option (\<lambda>s1'. SOME s2'. ?s2.0 -\<tau>2\<rightarrow>* s2' \<and> (\<forall>tl s2''. \<not> s2' -2-tl\<rightarrow> s2'') \<and> s1' \<approx> s2') (terminal ?stlsss1.0)
\<not> is_TNil ?stlsss1.0 \<Longrightarrow> thd (tls1_to_tls2 ?s2.0 ?stlsss1.0) = (let (tl2, s2'') = SOME (tl2, s2''). \<exists>s2'. ?s2.0 -\<tau>2\<rightarrow>* s2' \<and> s2' -2-tl2\<rightarrow> s2'' \<and> \<not> \<tau>move2 s2' tl2 s2'' \<and> snd (thd ?stlsss1.0) \<approx> s2'' \<and> fst (thd ?stlsss1.0) \<sim> tl2 in (tl2, s2''))
\<not> is_TNil ?stlsss1.0 \<Longrightarrow> ttl (tls1_to_tls2 ?s2.0 ?stlsss1.0) = (let (tl2, s2'') = SOME (tl2, s2''). \<exists>s2'. ?s2.0 -\<tau>2\<rightarrow>* s2' \<and> s2' -2-tl2\<rightarrow> s2'' \<and> \<not> \<tau>move2 s2' tl2 s2'' \<and> snd (thd ?stlsss1.0) \<approx> s2'' \<and> fst (thd ?stlsss1.0) \<sim> tl2 in tls1_to_tls2 s2'' (ttl ?stlsss1.0))
tls1_to_tls2 ?s2.0 (TNil ?os1.0) = TNil (map_option (\<lambda>s1'. SOME s2'. ?s2.0 -\<tau>2\<rightarrow>* s2' \<and> (\<forall>tl s2''. \<not> s2' -2-tl\<rightarrow> s2'') \<and> s1' \<approx> s2') ?os1.0)

goal (2 subgoals):
 1. trsys2.\<tau>Runs_table s2 ?stlsss2.0
 2. tllist_all2 (\<lambda>(tl1, s1'') (tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (rel_option bisim) stlsss1 ?stlsss2.0
[PROOF STEP]
have [simp]:
    "\<And>s2 s1 s1' tl1 s1'' stlsss1. 
     tls1_to_tls2 s2 (TCons (tl1, s1'') stlsss1) =
     (let (tl2, s2'') = SOME (tl2, s2''). \<exists>s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> s2' -2-tl2\<rightarrow> s2'' \<and> 
                             \<not> \<tau>move2 s2' tl2 s2'' \<and> s1'' \<approx> s2'' \<and> tl1 \<sim> tl2
      in TCons (tl2, s2'') (tls1_to_tls2 s2'' stlsss1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s2 s1 s1' tl1 s1'' stlsss1. tls1_to_tls2 s2 (TCons (tl1, s1'') stlsss1) = (let (tl2, s2'') = SOME (tl2, s2''). \<exists>s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> s2' -2-tl2\<rightarrow> s2'' \<and> \<not> \<tau>move2 s2' tl2 s2'' \<and> s1'' \<approx> s2'' \<and> tl1 \<sim> tl2 in TCons (tl2, s2'') (tls1_to_tls2 s2'' stlsss1))
[PROOF STEP]
by(rule tllist.expand)(simp_all add: split_beta)
[PROOF STATE]
proof (state)
this:
tls1_to_tls2 ?s2.0 (TCons (?tl1.0, ?s1'') ?stlsss1.0) = (let (tl2, s2'') = SOME (tl2, s2''). \<exists>s2'. ?s2.0 -\<tau>2\<rightarrow>* s2' \<and> s2' -2-tl2\<rightarrow> s2'' \<and> \<not> \<tau>move2 s2' tl2 s2'' \<and> ?s1'' \<approx> s2'' \<and> ?tl1.0 \<sim> tl2 in TCons (tl2, s2'') (tls1_to_tls2 s2'' ?stlsss1.0))

goal (2 subgoals):
 1. trsys2.\<tau>Runs_table s2 ?stlsss2.0
 2. tllist_all2 (\<lambda>(tl1, s1'') (tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (rel_option bisim) stlsss1 ?stlsss2.0
[PROOF STEP]
from bisim run1
[PROOF STATE]
proof (chain)
picking this:
s1 \<approx> s2
trsys1.\<tau>Runs_table s1 stlsss1
[PROOF STEP]
show "trsys2.\<tau>Runs_table s2 (tls1_to_tls2 s2 stlsss1)"
[PROOF STATE]
proof (prove)
using this:
s1 \<approx> s2
trsys1.\<tau>Runs_table s1 stlsss1

goal (1 subgoal):
 1. trsys2.\<tau>Runs_table s2 (tls1_to_tls2 s2 stlsss1)
[PROOF STEP]
proof(coinduction arbitrary: s2 s1 stlsss1)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s2 s1 stlsss1. \<lbrakk>s1 \<approx> s2; trsys1.\<tau>Runs_table s1 stlsss1\<rbrakk> \<Longrightarrow> (\<exists>s s'. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil \<lfloor>s'\<rfloor> \<and> s -\<tau>2\<rightarrow>* s' \<and> (\<forall>x xa. \<not> s' -2-x\<rightarrow> xa)) \<or> (\<exists>s. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil None \<and> s -\<tau>2\<rightarrow> \<infinity>) \<or> (\<exists>s s' s'' tls tl. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TCons (tl, s'') tls \<and> s -\<tau>2\<rightarrow>* s' \<and> s' -2-tl\<rightarrow> s'' \<and> \<not> \<tau>move2 s' tl s'' \<and> ((\<exists>s2 s1 stlsss1. s'' = s2 \<and> tls = tls1_to_tls2 s2 stlsss1 \<and> s1 \<approx> s2 \<and> trsys1.\<tau>Runs_table s1 stlsss1) \<or> trsys2.\<tau>Runs_table s'' tls))
[PROOF STEP]
case (\<tau>Runs_table s2 s1 stlsss1)
[PROOF STATE]
proof (state)
this:
s1 \<approx> s2
trsys1.\<tau>Runs_table s1 stlsss1

goal (1 subgoal):
 1. \<And>s2 s1 stlsss1. \<lbrakk>s1 \<approx> s2; trsys1.\<tau>Runs_table s1 stlsss1\<rbrakk> \<Longrightarrow> (\<exists>s s'. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil \<lfloor>s'\<rfloor> \<and> s -\<tau>2\<rightarrow>* s' \<and> (\<forall>x xa. \<not> s' -2-x\<rightarrow> xa)) \<or> (\<exists>s. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil None \<and> s -\<tau>2\<rightarrow> \<infinity>) \<or> (\<exists>s s' s'' tls tl. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TCons (tl, s'') tls \<and> s -\<tau>2\<rightarrow>* s' \<and> s' -2-tl\<rightarrow> s'' \<and> \<not> \<tau>move2 s' tl s'' \<and> ((\<exists>s2 s1 stlsss1. s'' = s2 \<and> tls = tls1_to_tls2 s2 stlsss1 \<and> s1 \<approx> s2 \<and> trsys1.\<tau>Runs_table s1 stlsss1) \<or> trsys2.\<tau>Runs_table s'' tls))
[PROOF STEP]
note bisim = \<open>s1 \<approx> s2\<close>
      and run1 = \<open>trsys1.\<tau>Runs_table s1 stlsss1\<close>
[PROOF STATE]
proof (state)
this:
s1 \<approx> s2
trsys1.\<tau>Runs_table s1 stlsss1

goal (1 subgoal):
 1. \<And>s2 s1 stlsss1. \<lbrakk>s1 \<approx> s2; trsys1.\<tau>Runs_table s1 stlsss1\<rbrakk> \<Longrightarrow> (\<exists>s s'. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil \<lfloor>s'\<rfloor> \<and> s -\<tau>2\<rightarrow>* s' \<and> (\<forall>x xa. \<not> s' -2-x\<rightarrow> xa)) \<or> (\<exists>s. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil None \<and> s -\<tau>2\<rightarrow> \<infinity>) \<or> (\<exists>s s' s'' tls tl. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TCons (tl, s'') tls \<and> s -\<tau>2\<rightarrow>* s' \<and> s' -2-tl\<rightarrow> s'' \<and> \<not> \<tau>move2 s' tl s'' \<and> ((\<exists>s2 s1 stlsss1. s'' = s2 \<and> tls = tls1_to_tls2 s2 stlsss1 \<and> s1 \<approx> s2 \<and> trsys1.\<tau>Runs_table s1 stlsss1) \<or> trsys2.\<tau>Runs_table s'' tls))
[PROOF STEP]
from run1
[PROOF STATE]
proof (chain)
picking this:
trsys1.\<tau>Runs_table s1 stlsss1
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
trsys1.\<tau>Runs_table s1 stlsss1

goal (1 subgoal):
 1. (\<exists>s s'. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil \<lfloor>s'\<rfloor> \<and> s -\<tau>2\<rightarrow>* s' \<and> (\<forall>x xa. \<not> s' -2-x\<rightarrow> xa)) \<or> (\<exists>s. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil None \<and> s -\<tau>2\<rightarrow> \<infinity>) \<or> (\<exists>s s' s'' tls tl. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TCons (tl, s'') tls \<and> s -\<tau>2\<rightarrow>* s' \<and> s' -2-tl\<rightarrow> s'' \<and> \<not> \<tau>move2 s' tl s'' \<and> ((\<exists>s2 s1 stlsss1. s'' = s2 \<and> tls = tls1_to_tls2 s2 stlsss1 \<and> s1 \<approx> s2 \<and> trsys1.\<tau>Runs_table s1 stlsss1) \<or> trsys2.\<tau>Runs_table s'' tls))
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>s'. \<lbrakk>stlsss1 = TNil \<lfloor>s'\<rfloor>; s1 -\<tau>1\<rightarrow>* s'; \<And>tl s''. \<not> s' -1-tl\<rightarrow> s''\<rbrakk> \<Longrightarrow> (\<exists>s s'. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil \<lfloor>s'\<rfloor> \<and> s -\<tau>2\<rightarrow>* s' \<and> (\<forall>x xa. \<not> s' -2-x\<rightarrow> xa)) \<or> (\<exists>s. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil None \<and> s -\<tau>2\<rightarrow> \<infinity>) \<or> (\<exists>s s' s'' tls tl. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TCons (tl, s'') tls \<and> s -\<tau>2\<rightarrow>* s' \<and> s' -2-tl\<rightarrow> s'' \<and> \<not> \<tau>move2 s' tl s'' \<and> ((\<exists>s2 s1 stlsss1. s'' = s2 \<and> tls = tls1_to_tls2 s2 stlsss1 \<and> s1 \<approx> s2 \<and> trsys1.\<tau>Runs_table s1 stlsss1) \<or> trsys2.\<tau>Runs_table s'' tls))
 2. \<lbrakk>stlsss1 = TNil None; s1 -\<tau>1\<rightarrow> \<infinity>\<rbrakk> \<Longrightarrow> (\<exists>s s'. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil \<lfloor>s'\<rfloor> \<and> s -\<tau>2\<rightarrow>* s' \<and> (\<forall>x xa. \<not> s' -2-x\<rightarrow> xa)) \<or> (\<exists>s. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil None \<and> s -\<tau>2\<rightarrow> \<infinity>) \<or> (\<exists>s s' s'' tls tl. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TCons (tl, s'') tls \<and> s -\<tau>2\<rightarrow>* s' \<and> s' -2-tl\<rightarrow> s'' \<and> \<not> \<tau>move2 s' tl s'' \<and> ((\<exists>s2 s1 stlsss1. s'' = s2 \<and> tls = tls1_to_tls2 s2 stlsss1 \<and> s1 \<approx> s2 \<and> trsys1.\<tau>Runs_table s1 stlsss1) \<or> trsys2.\<tau>Runs_table s'' tls))
 3. \<And>s' s'' tls tl. \<lbrakk>stlsss1 = TCons (tl, s'') tls; s1 -\<tau>1\<rightarrow>* s'; s' -1-tl\<rightarrow> s''; \<not> \<tau>move1 s' tl s''; trsys1.\<tau>Runs_table s'' tls\<rbrakk> \<Longrightarrow> (\<exists>s s'. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil \<lfloor>s'\<rfloor> \<and> s -\<tau>2\<rightarrow>* s' \<and> (\<forall>x xa. \<not> s' -2-x\<rightarrow> xa)) \<or> (\<exists>s. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil None \<and> s -\<tau>2\<rightarrow> \<infinity>) \<or> (\<exists>s s' s'' tls tl. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TCons (tl, s'') tls \<and> s -\<tau>2\<rightarrow>* s' \<and> s' -2-tl\<rightarrow> s'' \<and> \<not> \<tau>move2 s' tl s'' \<and> ((\<exists>s2 s1 stlsss1. s'' = s2 \<and> tls = tls1_to_tls2 s2 stlsss1 \<and> s1 \<approx> s2 \<and> trsys1.\<tau>Runs_table s1 stlsss1) \<or> trsys2.\<tau>Runs_table s'' tls))
[PROOF STEP]
case (Terminate s1')
[PROOF STATE]
proof (state)
this:
stlsss1 = TNil \<lfloor>s1'\<rfloor>
s1 -\<tau>1\<rightarrow>* s1'
\<not> s1' -1-?tl1\<rightarrow> ?s''1

goal (3 subgoals):
 1. \<And>s'. \<lbrakk>stlsss1 = TNil \<lfloor>s'\<rfloor>; s1 -\<tau>1\<rightarrow>* s'; \<And>tl s''. \<not> s' -1-tl\<rightarrow> s''\<rbrakk> \<Longrightarrow> (\<exists>s s'. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil \<lfloor>s'\<rfloor> \<and> s -\<tau>2\<rightarrow>* s' \<and> (\<forall>x xa. \<not> s' -2-x\<rightarrow> xa)) \<or> (\<exists>s. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil None \<and> s -\<tau>2\<rightarrow> \<infinity>) \<or> (\<exists>s s' s'' tls tl. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TCons (tl, s'') tls \<and> s -\<tau>2\<rightarrow>* s' \<and> s' -2-tl\<rightarrow> s'' \<and> \<not> \<tau>move2 s' tl s'' \<and> ((\<exists>s2 s1 stlsss1. s'' = s2 \<and> tls = tls1_to_tls2 s2 stlsss1 \<and> s1 \<approx> s2 \<and> trsys1.\<tau>Runs_table s1 stlsss1) \<or> trsys2.\<tau>Runs_table s'' tls))
 2. \<lbrakk>stlsss1 = TNil None; s1 -\<tau>1\<rightarrow> \<infinity>\<rbrakk> \<Longrightarrow> (\<exists>s s'. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil \<lfloor>s'\<rfloor> \<and> s -\<tau>2\<rightarrow>* s' \<and> (\<forall>x xa. \<not> s' -2-x\<rightarrow> xa)) \<or> (\<exists>s. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil None \<and> s -\<tau>2\<rightarrow> \<infinity>) \<or> (\<exists>s s' s'' tls tl. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TCons (tl, s'') tls \<and> s -\<tau>2\<rightarrow>* s' \<and> s' -2-tl\<rightarrow> s'' \<and> \<not> \<tau>move2 s' tl s'' \<and> ((\<exists>s2 s1 stlsss1. s'' = s2 \<and> tls = tls1_to_tls2 s2 stlsss1 \<and> s1 \<approx> s2 \<and> trsys1.\<tau>Runs_table s1 stlsss1) \<or> trsys2.\<tau>Runs_table s'' tls))
 3. \<And>s' s'' tls tl. \<lbrakk>stlsss1 = TCons (tl, s'') tls; s1 -\<tau>1\<rightarrow>* s'; s' -1-tl\<rightarrow> s''; \<not> \<tau>move1 s' tl s''; trsys1.\<tau>Runs_table s'' tls\<rbrakk> \<Longrightarrow> (\<exists>s s'. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil \<lfloor>s'\<rfloor> \<and> s -\<tau>2\<rightarrow>* s' \<and> (\<forall>x xa. \<not> s' -2-x\<rightarrow> xa)) \<or> (\<exists>s. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil None \<and> s -\<tau>2\<rightarrow> \<infinity>) \<or> (\<exists>s s' s'' tls tl. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TCons (tl, s'') tls \<and> s -\<tau>2\<rightarrow>* s' \<and> s' -2-tl\<rightarrow> s'' \<and> \<not> \<tau>move2 s' tl s'' \<and> ((\<exists>s2 s1 stlsss1. s'' = s2 \<and> tls = tls1_to_tls2 s2 stlsss1 \<and> s1 \<approx> s2 \<and> trsys1.\<tau>Runs_table s1 stlsss1) \<or> trsys2.\<tau>Runs_table s'' tls))
[PROOF STEP]
let ?P = "\<lambda>s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> (\<forall>tl2 s2''. \<not> s2' -2-tl2\<rightarrow> s2'') \<and> s1' \<approx> s2'"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>s'. \<lbrakk>stlsss1 = TNil \<lfloor>s'\<rfloor>; s1 -\<tau>1\<rightarrow>* s'; \<And>tl s''. \<not> s' -1-tl\<rightarrow> s''\<rbrakk> \<Longrightarrow> (\<exists>s s'. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil \<lfloor>s'\<rfloor> \<and> s -\<tau>2\<rightarrow>* s' \<and> (\<forall>x xa. \<not> s' -2-x\<rightarrow> xa)) \<or> (\<exists>s. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil None \<and> s -\<tau>2\<rightarrow> \<infinity>) \<or> (\<exists>s s' s'' tls tl. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TCons (tl, s'') tls \<and> s -\<tau>2\<rightarrow>* s' \<and> s' -2-tl\<rightarrow> s'' \<and> \<not> \<tau>move2 s' tl s'' \<and> ((\<exists>s2 s1 stlsss1. s'' = s2 \<and> tls = tls1_to_tls2 s2 stlsss1 \<and> s1 \<approx> s2 \<and> trsys1.\<tau>Runs_table s1 stlsss1) \<or> trsys2.\<tau>Runs_table s'' tls))
 2. \<lbrakk>stlsss1 = TNil None; s1 -\<tau>1\<rightarrow> \<infinity>\<rbrakk> \<Longrightarrow> (\<exists>s s'. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil \<lfloor>s'\<rfloor> \<and> s -\<tau>2\<rightarrow>* s' \<and> (\<forall>x xa. \<not> s' -2-x\<rightarrow> xa)) \<or> (\<exists>s. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil None \<and> s -\<tau>2\<rightarrow> \<infinity>) \<or> (\<exists>s s' s'' tls tl. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TCons (tl, s'') tls \<and> s -\<tau>2\<rightarrow>* s' \<and> s' -2-tl\<rightarrow> s'' \<and> \<not> \<tau>move2 s' tl s'' \<and> ((\<exists>s2 s1 stlsss1. s'' = s2 \<and> tls = tls1_to_tls2 s2 stlsss1 \<and> s1 \<approx> s2 \<and> trsys1.\<tau>Runs_table s1 stlsss1) \<or> trsys2.\<tau>Runs_table s'' tls))
 3. \<And>s' s'' tls tl. \<lbrakk>stlsss1 = TCons (tl, s'') tls; s1 -\<tau>1\<rightarrow>* s'; s' -1-tl\<rightarrow> s''; \<not> \<tau>move1 s' tl s''; trsys1.\<tau>Runs_table s'' tls\<rbrakk> \<Longrightarrow> (\<exists>s s'. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil \<lfloor>s'\<rfloor> \<and> s -\<tau>2\<rightarrow>* s' \<and> (\<forall>x xa. \<not> s' -2-x\<rightarrow> xa)) \<or> (\<exists>s. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil None \<and> s -\<tau>2\<rightarrow> \<infinity>) \<or> (\<exists>s s' s'' tls tl. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TCons (tl, s'') tls \<and> s -\<tau>2\<rightarrow>* s' \<and> s' -2-tl\<rightarrow> s'' \<and> \<not> \<tau>move2 s' tl s'' \<and> ((\<exists>s2 s1 stlsss1. s'' = s2 \<and> tls = tls1_to_tls2 s2 stlsss1 \<and> s1 \<approx> s2 \<and> trsys1.\<tau>Runs_table s1 stlsss1) \<or> trsys2.\<tau>Runs_table s'' tls))
[PROOF STEP]
from simulation_silents1[OF bisim \<open>s1 -\<tau>1\<rightarrow>* s1'\<close>]
[PROOF STATE]
proof (chain)
picking this:
\<exists>s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> s1' \<approx> s2'
[PROOF STEP]
obtain s2' where "s2 -\<tau>2\<rightarrow>* s2'" and "s1' \<approx> s2'"
[PROOF STATE]
proof (prove)
using this:
\<exists>s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> s1' \<approx> s2'

goal (1 subgoal):
 1. (\<And>s2'. \<lbrakk>s2 -\<tau>2\<rightarrow>* s2'; s1' \<approx> s2'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
s2 -\<tau>2\<rightarrow>* s2'
s1' \<approx> s2'

goal (3 subgoals):
 1. \<And>s'. \<lbrakk>stlsss1 = TNil \<lfloor>s'\<rfloor>; s1 -\<tau>1\<rightarrow>* s'; \<And>tl s''. \<not> s' -1-tl\<rightarrow> s''\<rbrakk> \<Longrightarrow> (\<exists>s s'. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil \<lfloor>s'\<rfloor> \<and> s -\<tau>2\<rightarrow>* s' \<and> (\<forall>x xa. \<not> s' -2-x\<rightarrow> xa)) \<or> (\<exists>s. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil None \<and> s -\<tau>2\<rightarrow> \<infinity>) \<or> (\<exists>s s' s'' tls tl. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TCons (tl, s'') tls \<and> s -\<tau>2\<rightarrow>* s' \<and> s' -2-tl\<rightarrow> s'' \<and> \<not> \<tau>move2 s' tl s'' \<and> ((\<exists>s2 s1 stlsss1. s'' = s2 \<and> tls = tls1_to_tls2 s2 stlsss1 \<and> s1 \<approx> s2 \<and> trsys1.\<tau>Runs_table s1 stlsss1) \<or> trsys2.\<tau>Runs_table s'' tls))
 2. \<lbrakk>stlsss1 = TNil None; s1 -\<tau>1\<rightarrow> \<infinity>\<rbrakk> \<Longrightarrow> (\<exists>s s'. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil \<lfloor>s'\<rfloor> \<and> s -\<tau>2\<rightarrow>* s' \<and> (\<forall>x xa. \<not> s' -2-x\<rightarrow> xa)) \<or> (\<exists>s. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil None \<and> s -\<tau>2\<rightarrow> \<infinity>) \<or> (\<exists>s s' s'' tls tl. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TCons (tl, s'') tls \<and> s -\<tau>2\<rightarrow>* s' \<and> s' -2-tl\<rightarrow> s'' \<and> \<not> \<tau>move2 s' tl s'' \<and> ((\<exists>s2 s1 stlsss1. s'' = s2 \<and> tls = tls1_to_tls2 s2 stlsss1 \<and> s1 \<approx> s2 \<and> trsys1.\<tau>Runs_table s1 stlsss1) \<or> trsys2.\<tau>Runs_table s'' tls))
 3. \<And>s' s'' tls tl. \<lbrakk>stlsss1 = TCons (tl, s'') tls; s1 -\<tau>1\<rightarrow>* s'; s' -1-tl\<rightarrow> s''; \<not> \<tau>move1 s' tl s''; trsys1.\<tau>Runs_table s'' tls\<rbrakk> \<Longrightarrow> (\<exists>s s'. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil \<lfloor>s'\<rfloor> \<and> s -\<tau>2\<rightarrow>* s' \<and> (\<forall>x xa. \<not> s' -2-x\<rightarrow> xa)) \<or> (\<exists>s. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil None \<and> s -\<tau>2\<rightarrow> \<infinity>) \<or> (\<exists>s s' s'' tls tl. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TCons (tl, s'') tls \<and> s -\<tau>2\<rightarrow>* s' \<and> s' -2-tl\<rightarrow> s'' \<and> \<not> \<tau>move2 s' tl s'' \<and> ((\<exists>s2 s1 stlsss1. s'' = s2 \<and> tls = tls1_to_tls2 s2 stlsss1 \<and> s1 \<approx> s2 \<and> trsys1.\<tau>Runs_table s1 stlsss1) \<or> trsys2.\<tau>Runs_table s'' tls))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
s2 -\<tau>2\<rightarrow>* s2'
s1' \<approx> s2'

goal (3 subgoals):
 1. \<And>s'. \<lbrakk>stlsss1 = TNil \<lfloor>s'\<rfloor>; s1 -\<tau>1\<rightarrow>* s'; \<And>tl s''. \<not> s' -1-tl\<rightarrow> s''\<rbrakk> \<Longrightarrow> (\<exists>s s'. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil \<lfloor>s'\<rfloor> \<and> s -\<tau>2\<rightarrow>* s' \<and> (\<forall>x xa. \<not> s' -2-x\<rightarrow> xa)) \<or> (\<exists>s. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil None \<and> s -\<tau>2\<rightarrow> \<infinity>) \<or> (\<exists>s s' s'' tls tl. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TCons (tl, s'') tls \<and> s -\<tau>2\<rightarrow>* s' \<and> s' -2-tl\<rightarrow> s'' \<and> \<not> \<tau>move2 s' tl s'' \<and> ((\<exists>s2 s1 stlsss1. s'' = s2 \<and> tls = tls1_to_tls2 s2 stlsss1 \<and> s1 \<approx> s2 \<and> trsys1.\<tau>Runs_table s1 stlsss1) \<or> trsys2.\<tau>Runs_table s'' tls))
 2. \<lbrakk>stlsss1 = TNil None; s1 -\<tau>1\<rightarrow> \<infinity>\<rbrakk> \<Longrightarrow> (\<exists>s s'. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil \<lfloor>s'\<rfloor> \<and> s -\<tau>2\<rightarrow>* s' \<and> (\<forall>x xa. \<not> s' -2-x\<rightarrow> xa)) \<or> (\<exists>s. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil None \<and> s -\<tau>2\<rightarrow> \<infinity>) \<or> (\<exists>s s' s'' tls tl. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TCons (tl, s'') tls \<and> s -\<tau>2\<rightarrow>* s' \<and> s' -2-tl\<rightarrow> s'' \<and> \<not> \<tau>move2 s' tl s'' \<and> ((\<exists>s2 s1 stlsss1. s'' = s2 \<and> tls = tls1_to_tls2 s2 stlsss1 \<and> s1 \<approx> s2 \<and> trsys1.\<tau>Runs_table s1 stlsss1) \<or> trsys2.\<tau>Runs_table s'' tls))
 3. \<And>s' s'' tls tl. \<lbrakk>stlsss1 = TCons (tl, s'') tls; s1 -\<tau>1\<rightarrow>* s'; s' -1-tl\<rightarrow> s''; \<not> \<tau>move1 s' tl s''; trsys1.\<tau>Runs_table s'' tls\<rbrakk> \<Longrightarrow> (\<exists>s s'. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil \<lfloor>s'\<rfloor> \<and> s -\<tau>2\<rightarrow>* s' \<and> (\<forall>x xa. \<not> s' -2-x\<rightarrow> xa)) \<or> (\<exists>s. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil None \<and> s -\<tau>2\<rightarrow> \<infinity>) \<or> (\<exists>s s' s'' tls tl. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TCons (tl, s'') tls \<and> s -\<tau>2\<rightarrow>* s' \<and> s' -2-tl\<rightarrow> s'' \<and> \<not> \<tau>move2 s' tl s'' \<and> ((\<exists>s2 s1 stlsss1. s'' = s2 \<and> tls = tls1_to_tls2 s2 stlsss1 \<and> s1 \<approx> s2 \<and> trsys1.\<tau>Runs_table s1 stlsss1) \<or> trsys2.\<tau>Runs_table s'' tls))
[PROOF STEP]
from no_move1_to_no_move2[OF \<open>s1' \<approx> s2'\<close> \<open>\<And>tl1 s1''. \<not> s1' -1-tl1\<rightarrow> s1''\<close>]
[PROOF STATE]
proof (chain)
picking this:
\<exists>s2'a. s2' -\<tau>2\<rightarrow>* s2'a \<and> (\<forall>tl2 s2''. \<not> s2'a -2-tl2\<rightarrow> s2'') \<and> s1' \<approx> s2'a
[PROOF STEP]
obtain s2'' where "s2' -\<tau>2\<rightarrow>* s2''" and "s1' \<approx> s2''" 
        and "\<And>tl2 s2'''. \<not> s2'' -2-tl2\<rightarrow> s2'''"
[PROOF STATE]
proof (prove)
using this:
\<exists>s2'a. s2' -\<tau>2\<rightarrow>* s2'a \<and> (\<forall>tl2 s2''. \<not> s2'a -2-tl2\<rightarrow> s2'') \<and> s1' \<approx> s2'a

goal (1 subgoal):
 1. (\<And>s2''. \<lbrakk>s2' -\<tau>2\<rightarrow>* s2''; s1' \<approx> s2''; \<And>tl2 s2'''. \<not> s2'' -2-tl2\<rightarrow> s2'''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
s2' -\<tau>2\<rightarrow>* s2''
s1' \<approx> s2''
\<not> s2'' -2-?tl2.1\<rightarrow> ?s2'''1

goal (3 subgoals):
 1. \<And>s'. \<lbrakk>stlsss1 = TNil \<lfloor>s'\<rfloor>; s1 -\<tau>1\<rightarrow>* s'; \<And>tl s''. \<not> s' -1-tl\<rightarrow> s''\<rbrakk> \<Longrightarrow> (\<exists>s s'. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil \<lfloor>s'\<rfloor> \<and> s -\<tau>2\<rightarrow>* s' \<and> (\<forall>x xa. \<not> s' -2-x\<rightarrow> xa)) \<or> (\<exists>s. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil None \<and> s -\<tau>2\<rightarrow> \<infinity>) \<or> (\<exists>s s' s'' tls tl. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TCons (tl, s'') tls \<and> s -\<tau>2\<rightarrow>* s' \<and> s' -2-tl\<rightarrow> s'' \<and> \<not> \<tau>move2 s' tl s'' \<and> ((\<exists>s2 s1 stlsss1. s'' = s2 \<and> tls = tls1_to_tls2 s2 stlsss1 \<and> s1 \<approx> s2 \<and> trsys1.\<tau>Runs_table s1 stlsss1) \<or> trsys2.\<tau>Runs_table s'' tls))
 2. \<lbrakk>stlsss1 = TNil None; s1 -\<tau>1\<rightarrow> \<infinity>\<rbrakk> \<Longrightarrow> (\<exists>s s'. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil \<lfloor>s'\<rfloor> \<and> s -\<tau>2\<rightarrow>* s' \<and> (\<forall>x xa. \<not> s' -2-x\<rightarrow> xa)) \<or> (\<exists>s. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil None \<and> s -\<tau>2\<rightarrow> \<infinity>) \<or> (\<exists>s s' s'' tls tl. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TCons (tl, s'') tls \<and> s -\<tau>2\<rightarrow>* s' \<and> s' -2-tl\<rightarrow> s'' \<and> \<not> \<tau>move2 s' tl s'' \<and> ((\<exists>s2 s1 stlsss1. s'' = s2 \<and> tls = tls1_to_tls2 s2 stlsss1 \<and> s1 \<approx> s2 \<and> trsys1.\<tau>Runs_table s1 stlsss1) \<or> trsys2.\<tau>Runs_table s'' tls))
 3. \<And>s' s'' tls tl. \<lbrakk>stlsss1 = TCons (tl, s'') tls; s1 -\<tau>1\<rightarrow>* s'; s' -1-tl\<rightarrow> s''; \<not> \<tau>move1 s' tl s''; trsys1.\<tau>Runs_table s'' tls\<rbrakk> \<Longrightarrow> (\<exists>s s'. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil \<lfloor>s'\<rfloor> \<and> s -\<tau>2\<rightarrow>* s' \<and> (\<forall>x xa. \<not> s' -2-x\<rightarrow> xa)) \<or> (\<exists>s. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil None \<and> s -\<tau>2\<rightarrow> \<infinity>) \<or> (\<exists>s s' s'' tls tl. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TCons (tl, s'') tls \<and> s -\<tau>2\<rightarrow>* s' \<and> s' -2-tl\<rightarrow> s'' \<and> \<not> \<tau>move2 s' tl s'' \<and> ((\<exists>s2 s1 stlsss1. s'' = s2 \<and> tls = tls1_to_tls2 s2 stlsss1 \<and> s1 \<approx> s2 \<and> trsys1.\<tau>Runs_table s1 stlsss1) \<or> trsys2.\<tau>Runs_table s'' tls))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
s2 -\<tau>2\<rightarrow>* s2'
s1' \<approx> s2'
s2' -\<tau>2\<rightarrow>* s2''
s1' \<approx> s2''
\<not> s2'' -2-?tl2.1\<rightarrow> ?s2'''1
[PROOF STEP]
have "?P s2''"
[PROOF STATE]
proof (prove)
using this:
s2 -\<tau>2\<rightarrow>* s2'
s1' \<approx> s2'
s2' -\<tau>2\<rightarrow>* s2''
s1' \<approx> s2''
\<not> s2'' -2-?tl2.1\<rightarrow> ?s2'''1

goal (1 subgoal):
 1. s2 -\<tau>2\<rightarrow>* s2'' \<and> (\<forall>tl2 s2''a. \<not> s2'' -2-tl2\<rightarrow> s2''a) \<and> s1' \<approx> s2''
[PROOF STEP]
by(blast intro: rtranclp_trans)
[PROOF STATE]
proof (state)
this:
s2 -\<tau>2\<rightarrow>* s2'' \<and> (\<forall>tl2 s2''a. \<not> s2'' -2-tl2\<rightarrow> s2''a) \<and> s1' \<approx> s2''

goal (3 subgoals):
 1. \<And>s'. \<lbrakk>stlsss1 = TNil \<lfloor>s'\<rfloor>; s1 -\<tau>1\<rightarrow>* s'; \<And>tl s''. \<not> s' -1-tl\<rightarrow> s''\<rbrakk> \<Longrightarrow> (\<exists>s s'. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil \<lfloor>s'\<rfloor> \<and> s -\<tau>2\<rightarrow>* s' \<and> (\<forall>x xa. \<not> s' -2-x\<rightarrow> xa)) \<or> (\<exists>s. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil None \<and> s -\<tau>2\<rightarrow> \<infinity>) \<or> (\<exists>s s' s'' tls tl. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TCons (tl, s'') tls \<and> s -\<tau>2\<rightarrow>* s' \<and> s' -2-tl\<rightarrow> s'' \<and> \<not> \<tau>move2 s' tl s'' \<and> ((\<exists>s2 s1 stlsss1. s'' = s2 \<and> tls = tls1_to_tls2 s2 stlsss1 \<and> s1 \<approx> s2 \<and> trsys1.\<tau>Runs_table s1 stlsss1) \<or> trsys2.\<tau>Runs_table s'' tls))
 2. \<lbrakk>stlsss1 = TNil None; s1 -\<tau>1\<rightarrow> \<infinity>\<rbrakk> \<Longrightarrow> (\<exists>s s'. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil \<lfloor>s'\<rfloor> \<and> s -\<tau>2\<rightarrow>* s' \<and> (\<forall>x xa. \<not> s' -2-x\<rightarrow> xa)) \<or> (\<exists>s. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil None \<and> s -\<tau>2\<rightarrow> \<infinity>) \<or> (\<exists>s s' s'' tls tl. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TCons (tl, s'') tls \<and> s -\<tau>2\<rightarrow>* s' \<and> s' -2-tl\<rightarrow> s'' \<and> \<not> \<tau>move2 s' tl s'' \<and> ((\<exists>s2 s1 stlsss1. s'' = s2 \<and> tls = tls1_to_tls2 s2 stlsss1 \<and> s1 \<approx> s2 \<and> trsys1.\<tau>Runs_table s1 stlsss1) \<or> trsys2.\<tau>Runs_table s'' tls))
 3. \<And>s' s'' tls tl. \<lbrakk>stlsss1 = TCons (tl, s'') tls; s1 -\<tau>1\<rightarrow>* s'; s' -1-tl\<rightarrow> s''; \<not> \<tau>move1 s' tl s''; trsys1.\<tau>Runs_table s'' tls\<rbrakk> \<Longrightarrow> (\<exists>s s'. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil \<lfloor>s'\<rfloor> \<and> s -\<tau>2\<rightarrow>* s' \<and> (\<forall>x xa. \<not> s' -2-x\<rightarrow> xa)) \<or> (\<exists>s. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil None \<and> s -\<tau>2\<rightarrow> \<infinity>) \<or> (\<exists>s s' s'' tls tl. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TCons (tl, s'') tls \<and> s -\<tau>2\<rightarrow>* s' \<and> s' -2-tl\<rightarrow> s'' \<and> \<not> \<tau>move2 s' tl s'' \<and> ((\<exists>s2 s1 stlsss1. s'' = s2 \<and> tls = tls1_to_tls2 s2 stlsss1 \<and> s1 \<approx> s2 \<and> trsys1.\<tau>Runs_table s1 stlsss1) \<or> trsys2.\<tau>Runs_table s'' tls))
[PROOF STEP]
hence "?P (Eps ?P)"
[PROOF STATE]
proof (prove)
using this:
s2 -\<tau>2\<rightarrow>* s2'' \<and> (\<forall>tl2 s2''a. \<not> s2'' -2-tl2\<rightarrow> s2''a) \<and> s1' \<approx> s2''

goal (1 subgoal):
 1. s2 -\<tau>2\<rightarrow>* (SOME s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> (\<forall>tl2 s2''. \<not> s2' -2-tl2\<rightarrow> s2'') \<and> s1' \<approx> s2') \<and> (\<forall>tl2 s2''. \<not> (SOME s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> (\<forall>tl2 s2''. \<not> s2' -2-tl2\<rightarrow> s2'') \<and> s1' \<approx> s2') -2-tl2\<rightarrow> s2'') \<and> s1' \<approx> (SOME s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> (\<forall>tl2 s2''. \<not> s2' -2-tl2\<rightarrow> s2'') \<and> s1' \<approx> s2')
[PROOF STEP]
by(rule someI)
[PROOF STATE]
proof (state)
this:
s2 -\<tau>2\<rightarrow>* (SOME s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> (\<forall>tl2 s2''. \<not> s2' -2-tl2\<rightarrow> s2'') \<and> s1' \<approx> s2') \<and> (\<forall>tl2 s2''. \<not> (SOME s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> (\<forall>tl2 s2''. \<not> s2' -2-tl2\<rightarrow> s2'') \<and> s1' \<approx> s2') -2-tl2\<rightarrow> s2'') \<and> s1' \<approx> (SOME s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> (\<forall>tl2 s2''. \<not> s2' -2-tl2\<rightarrow> s2'') \<and> s1' \<approx> s2')

goal (3 subgoals):
 1. \<And>s'. \<lbrakk>stlsss1 = TNil \<lfloor>s'\<rfloor>; s1 -\<tau>1\<rightarrow>* s'; \<And>tl s''. \<not> s' -1-tl\<rightarrow> s''\<rbrakk> \<Longrightarrow> (\<exists>s s'. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil \<lfloor>s'\<rfloor> \<and> s -\<tau>2\<rightarrow>* s' \<and> (\<forall>x xa. \<not> s' -2-x\<rightarrow> xa)) \<or> (\<exists>s. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil None \<and> s -\<tau>2\<rightarrow> \<infinity>) \<or> (\<exists>s s' s'' tls tl. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TCons (tl, s'') tls \<and> s -\<tau>2\<rightarrow>* s' \<and> s' -2-tl\<rightarrow> s'' \<and> \<not> \<tau>move2 s' tl s'' \<and> ((\<exists>s2 s1 stlsss1. s'' = s2 \<and> tls = tls1_to_tls2 s2 stlsss1 \<and> s1 \<approx> s2 \<and> trsys1.\<tau>Runs_table s1 stlsss1) \<or> trsys2.\<tau>Runs_table s'' tls))
 2. \<lbrakk>stlsss1 = TNil None; s1 -\<tau>1\<rightarrow> \<infinity>\<rbrakk> \<Longrightarrow> (\<exists>s s'. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil \<lfloor>s'\<rfloor> \<and> s -\<tau>2\<rightarrow>* s' \<and> (\<forall>x xa. \<not> s' -2-x\<rightarrow> xa)) \<or> (\<exists>s. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil None \<and> s -\<tau>2\<rightarrow> \<infinity>) \<or> (\<exists>s s' s'' tls tl. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TCons (tl, s'') tls \<and> s -\<tau>2\<rightarrow>* s' \<and> s' -2-tl\<rightarrow> s'' \<and> \<not> \<tau>move2 s' tl s'' \<and> ((\<exists>s2 s1 stlsss1. s'' = s2 \<and> tls = tls1_to_tls2 s2 stlsss1 \<and> s1 \<approx> s2 \<and> trsys1.\<tau>Runs_table s1 stlsss1) \<or> trsys2.\<tau>Runs_table s'' tls))
 3. \<And>s' s'' tls tl. \<lbrakk>stlsss1 = TCons (tl, s'') tls; s1 -\<tau>1\<rightarrow>* s'; s' -1-tl\<rightarrow> s''; \<not> \<tau>move1 s' tl s''; trsys1.\<tau>Runs_table s'' tls\<rbrakk> \<Longrightarrow> (\<exists>s s'. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil \<lfloor>s'\<rfloor> \<and> s -\<tau>2\<rightarrow>* s' \<and> (\<forall>x xa. \<not> s' -2-x\<rightarrow> xa)) \<or> (\<exists>s. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil None \<and> s -\<tau>2\<rightarrow> \<infinity>) \<or> (\<exists>s s' s'' tls tl. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TCons (tl, s'') tls \<and> s -\<tau>2\<rightarrow>* s' \<and> s' -2-tl\<rightarrow> s'' \<and> \<not> \<tau>move2 s' tl s'' \<and> ((\<exists>s2 s1 stlsss1. s'' = s2 \<and> tls = tls1_to_tls2 s2 stlsss1 \<and> s1 \<approx> s2 \<and> trsys1.\<tau>Runs_table s1 stlsss1) \<or> trsys2.\<tau>Runs_table s'' tls))
[PROOF STEP]
hence ?Terminate
[PROOF STATE]
proof (prove)
using this:
s2 -\<tau>2\<rightarrow>* (SOME s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> (\<forall>tl2 s2''. \<not> s2' -2-tl2\<rightarrow> s2'') \<and> s1' \<approx> s2') \<and> (\<forall>tl2 s2''. \<not> (SOME s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> (\<forall>tl2 s2''. \<not> s2' -2-tl2\<rightarrow> s2'') \<and> s1' \<approx> s2') -2-tl2\<rightarrow> s2'') \<and> s1' \<approx> (SOME s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> (\<forall>tl2 s2''. \<not> s2' -2-tl2\<rightarrow> s2'') \<and> s1' \<approx> s2')

goal (1 subgoal):
 1. \<exists>s s'. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil \<lfloor>s'\<rfloor> \<and> s -\<tau>2\<rightarrow>* s' \<and> (\<forall>x xa. \<not> s' -2-x\<rightarrow> xa)
[PROOF STEP]
using \<open>stlsss1 = TNil \<lfloor>s1'\<rfloor>\<close>
[PROOF STATE]
proof (prove)
using this:
s2 -\<tau>2\<rightarrow>* (SOME s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> (\<forall>tl2 s2''. \<not> s2' -2-tl2\<rightarrow> s2'') \<and> s1' \<approx> s2') \<and> (\<forall>tl2 s2''. \<not> (SOME s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> (\<forall>tl2 s2''. \<not> s2' -2-tl2\<rightarrow> s2'') \<and> s1' \<approx> s2') -2-tl2\<rightarrow> s2'') \<and> s1' \<approx> (SOME s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> (\<forall>tl2 s2''. \<not> s2' -2-tl2\<rightarrow> s2'') \<and> s1' \<approx> s2')
stlsss1 = TNil \<lfloor>s1'\<rfloor>

goal (1 subgoal):
 1. \<exists>s s'. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil \<lfloor>s'\<rfloor> \<and> s -\<tau>2\<rightarrow>* s' \<and> (\<forall>x xa. \<not> s' -2-x\<rightarrow> xa)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>s s'. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil \<lfloor>s'\<rfloor> \<and> s -\<tau>2\<rightarrow>* s' \<and> (\<forall>x xa. \<not> s' -2-x\<rightarrow> xa)

goal (3 subgoals):
 1. \<And>s'. \<lbrakk>stlsss1 = TNil \<lfloor>s'\<rfloor>; s1 -\<tau>1\<rightarrow>* s'; \<And>tl s''. \<not> s' -1-tl\<rightarrow> s''\<rbrakk> \<Longrightarrow> (\<exists>s s'. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil \<lfloor>s'\<rfloor> \<and> s -\<tau>2\<rightarrow>* s' \<and> (\<forall>x xa. \<not> s' -2-x\<rightarrow> xa)) \<or> (\<exists>s. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil None \<and> s -\<tau>2\<rightarrow> \<infinity>) \<or> (\<exists>s s' s'' tls tl. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TCons (tl, s'') tls \<and> s -\<tau>2\<rightarrow>* s' \<and> s' -2-tl\<rightarrow> s'' \<and> \<not> \<tau>move2 s' tl s'' \<and> ((\<exists>s2 s1 stlsss1. s'' = s2 \<and> tls = tls1_to_tls2 s2 stlsss1 \<and> s1 \<approx> s2 \<and> trsys1.\<tau>Runs_table s1 stlsss1) \<or> trsys2.\<tau>Runs_table s'' tls))
 2. \<lbrakk>stlsss1 = TNil None; s1 -\<tau>1\<rightarrow> \<infinity>\<rbrakk> \<Longrightarrow> (\<exists>s s'. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil \<lfloor>s'\<rfloor> \<and> s -\<tau>2\<rightarrow>* s' \<and> (\<forall>x xa. \<not> s' -2-x\<rightarrow> xa)) \<or> (\<exists>s. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil None \<and> s -\<tau>2\<rightarrow> \<infinity>) \<or> (\<exists>s s' s'' tls tl. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TCons (tl, s'') tls \<and> s -\<tau>2\<rightarrow>* s' \<and> s' -2-tl\<rightarrow> s'' \<and> \<not> \<tau>move2 s' tl s'' \<and> ((\<exists>s2 s1 stlsss1. s'' = s2 \<and> tls = tls1_to_tls2 s2 stlsss1 \<and> s1 \<approx> s2 \<and> trsys1.\<tau>Runs_table s1 stlsss1) \<or> trsys2.\<tau>Runs_table s'' tls))
 3. \<And>s' s'' tls tl. \<lbrakk>stlsss1 = TCons (tl, s'') tls; s1 -\<tau>1\<rightarrow>* s'; s' -1-tl\<rightarrow> s''; \<not> \<tau>move1 s' tl s''; trsys1.\<tau>Runs_table s'' tls\<rbrakk> \<Longrightarrow> (\<exists>s s'. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil \<lfloor>s'\<rfloor> \<and> s -\<tau>2\<rightarrow>* s' \<and> (\<forall>x xa. \<not> s' -2-x\<rightarrow> xa)) \<or> (\<exists>s. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil None \<and> s -\<tau>2\<rightarrow> \<infinity>) \<or> (\<exists>s s' s'' tls tl. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TCons (tl, s'') tls \<and> s -\<tau>2\<rightarrow>* s' \<and> s' -2-tl\<rightarrow> s'' \<and> \<not> \<tau>move2 s' tl s'' \<and> ((\<exists>s2 s1 stlsss1. s'' = s2 \<and> tls = tls1_to_tls2 s2 stlsss1 \<and> s1 \<approx> s2 \<and> trsys1.\<tau>Runs_table s1 stlsss1) \<or> trsys2.\<tau>Runs_table s'' tls))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>s s'. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil \<lfloor>s'\<rfloor> \<and> s -\<tau>2\<rightarrow>* s' \<and> (\<forall>x xa. \<not> s' -2-x\<rightarrow> xa)

goal (1 subgoal):
 1. (\<exists>s s'. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil \<lfloor>s'\<rfloor> \<and> s -\<tau>2\<rightarrow>* s' \<and> (\<forall>x xa. \<not> s' -2-x\<rightarrow> xa)) \<or> (\<exists>s. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil None \<and> s -\<tau>2\<rightarrow> \<infinity>) \<or> (\<exists>s s' s'' tls tl. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TCons (tl, s'') tls \<and> s -\<tau>2\<rightarrow>* s' \<and> s' -2-tl\<rightarrow> s'' \<and> \<not> \<tau>move2 s' tl s'' \<and> ((\<exists>s2 s1 stlsss1. s'' = s2 \<and> tls = tls1_to_tls2 s2 stlsss1 \<and> s1 \<approx> s2 \<and> trsys1.\<tau>Runs_table s1 stlsss1) \<or> trsys2.\<tau>Runs_table s'' tls))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(\<exists>s s'. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil \<lfloor>s'\<rfloor> \<and> s -\<tau>2\<rightarrow>* s' \<and> (\<forall>x xa. \<not> s' -2-x\<rightarrow> xa)) \<or> (\<exists>s. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil None \<and> s -\<tau>2\<rightarrow> \<infinity>) \<or> (\<exists>s s' s'' tls tl. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TCons (tl, s'') tls \<and> s -\<tau>2\<rightarrow>* s' \<and> s' -2-tl\<rightarrow> s'' \<and> \<not> \<tau>move2 s' tl s'' \<and> ((\<exists>s2 s1 stlsss1. s'' = s2 \<and> tls = tls1_to_tls2 s2 stlsss1 \<and> s1 \<approx> s2 \<and> trsys1.\<tau>Runs_table s1 stlsss1) \<or> trsys2.\<tau>Runs_table s'' tls))

goal (2 subgoals):
 1. \<lbrakk>stlsss1 = TNil None; s1 -\<tau>1\<rightarrow> \<infinity>\<rbrakk> \<Longrightarrow> (\<exists>s s'. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil \<lfloor>s'\<rfloor> \<and> s -\<tau>2\<rightarrow>* s' \<and> (\<forall>x xa. \<not> s' -2-x\<rightarrow> xa)) \<or> (\<exists>s. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil None \<and> s -\<tau>2\<rightarrow> \<infinity>) \<or> (\<exists>s s' s'' tls tl. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TCons (tl, s'') tls \<and> s -\<tau>2\<rightarrow>* s' \<and> s' -2-tl\<rightarrow> s'' \<and> \<not> \<tau>move2 s' tl s'' \<and> ((\<exists>s2 s1 stlsss1. s'' = s2 \<and> tls = tls1_to_tls2 s2 stlsss1 \<and> s1 \<approx> s2 \<and> trsys1.\<tau>Runs_table s1 stlsss1) \<or> trsys2.\<tau>Runs_table s'' tls))
 2. \<And>s' s'' tls tl. \<lbrakk>stlsss1 = TCons (tl, s'') tls; s1 -\<tau>1\<rightarrow>* s'; s' -1-tl\<rightarrow> s''; \<not> \<tau>move1 s' tl s''; trsys1.\<tau>Runs_table s'' tls\<rbrakk> \<Longrightarrow> (\<exists>s s'. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil \<lfloor>s'\<rfloor> \<and> s -\<tau>2\<rightarrow>* s' \<and> (\<forall>x xa. \<not> s' -2-x\<rightarrow> xa)) \<or> (\<exists>s. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil None \<and> s -\<tau>2\<rightarrow> \<infinity>) \<or> (\<exists>s s' s'' tls tl. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TCons (tl, s'') tls \<and> s -\<tau>2\<rightarrow>* s' \<and> s' -2-tl\<rightarrow> s'' \<and> \<not> \<tau>move2 s' tl s'' \<and> ((\<exists>s2 s1 stlsss1. s'' = s2 \<and> tls = tls1_to_tls2 s2 stlsss1 \<and> s1 \<approx> s2 \<and> trsys1.\<tau>Runs_table s1 stlsss1) \<or> trsys2.\<tau>Runs_table s'' tls))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>stlsss1 = TNil None; s1 -\<tau>1\<rightarrow> \<infinity>\<rbrakk> \<Longrightarrow> (\<exists>s s'. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil \<lfloor>s'\<rfloor> \<and> s -\<tau>2\<rightarrow>* s' \<and> (\<forall>x xa. \<not> s' -2-x\<rightarrow> xa)) \<or> (\<exists>s. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil None \<and> s -\<tau>2\<rightarrow> \<infinity>) \<or> (\<exists>s s' s'' tls tl. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TCons (tl, s'') tls \<and> s -\<tau>2\<rightarrow>* s' \<and> s' -2-tl\<rightarrow> s'' \<and> \<not> \<tau>move2 s' tl s'' \<and> ((\<exists>s2 s1 stlsss1. s'' = s2 \<and> tls = tls1_to_tls2 s2 stlsss1 \<and> s1 \<approx> s2 \<and> trsys1.\<tau>Runs_table s1 stlsss1) \<or> trsys2.\<tau>Runs_table s'' tls))
 2. \<And>s' s'' tls tl. \<lbrakk>stlsss1 = TCons (tl, s'') tls; s1 -\<tau>1\<rightarrow>* s'; s' -1-tl\<rightarrow> s''; \<not> \<tau>move1 s' tl s''; trsys1.\<tau>Runs_table s'' tls\<rbrakk> \<Longrightarrow> (\<exists>s s'. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil \<lfloor>s'\<rfloor> \<and> s -\<tau>2\<rightarrow>* s' \<and> (\<forall>x xa. \<not> s' -2-x\<rightarrow> xa)) \<or> (\<exists>s. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil None \<and> s -\<tau>2\<rightarrow> \<infinity>) \<or> (\<exists>s s' s'' tls tl. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TCons (tl, s'') tls \<and> s -\<tau>2\<rightarrow>* s' \<and> s' -2-tl\<rightarrow> s'' \<and> \<not> \<tau>move2 s' tl s'' \<and> ((\<exists>s2 s1 stlsss1. s'' = s2 \<and> tls = tls1_to_tls2 s2 stlsss1 \<and> s1 \<approx> s2 \<and> trsys1.\<tau>Runs_table s1 stlsss1) \<or> trsys2.\<tau>Runs_table s'' tls))
[PROOF STEP]
case Diverge
[PROOF STATE]
proof (state)
this:
stlsss1 = TNil None
s1 -\<tau>1\<rightarrow> \<infinity>

goal (2 subgoals):
 1. \<lbrakk>stlsss1 = TNil None; s1 -\<tau>1\<rightarrow> \<infinity>\<rbrakk> \<Longrightarrow> (\<exists>s s'. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil \<lfloor>s'\<rfloor> \<and> s -\<tau>2\<rightarrow>* s' \<and> (\<forall>x xa. \<not> s' -2-x\<rightarrow> xa)) \<or> (\<exists>s. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil None \<and> s -\<tau>2\<rightarrow> \<infinity>) \<or> (\<exists>s s' s'' tls tl. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TCons (tl, s'') tls \<and> s -\<tau>2\<rightarrow>* s' \<and> s' -2-tl\<rightarrow> s'' \<and> \<not> \<tau>move2 s' tl s'' \<and> ((\<exists>s2 s1 stlsss1. s'' = s2 \<and> tls = tls1_to_tls2 s2 stlsss1 \<and> s1 \<approx> s2 \<and> trsys1.\<tau>Runs_table s1 stlsss1) \<or> trsys2.\<tau>Runs_table s'' tls))
 2. \<And>s' s'' tls tl. \<lbrakk>stlsss1 = TCons (tl, s'') tls; s1 -\<tau>1\<rightarrow>* s'; s' -1-tl\<rightarrow> s''; \<not> \<tau>move1 s' tl s''; trsys1.\<tau>Runs_table s'' tls\<rbrakk> \<Longrightarrow> (\<exists>s s'. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil \<lfloor>s'\<rfloor> \<and> s -\<tau>2\<rightarrow>* s' \<and> (\<forall>x xa. \<not> s' -2-x\<rightarrow> xa)) \<or> (\<exists>s. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil None \<and> s -\<tau>2\<rightarrow> \<infinity>) \<or> (\<exists>s s' s'' tls tl. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TCons (tl, s'') tls \<and> s -\<tau>2\<rightarrow>* s' \<and> s' -2-tl\<rightarrow> s'' \<and> \<not> \<tau>move2 s' tl s'' \<and> ((\<exists>s2 s1 stlsss1. s'' = s2 \<and> tls = tls1_to_tls2 s2 stlsss1 \<and> s1 \<approx> s2 \<and> trsys1.\<tau>Runs_table s1 stlsss1) \<or> trsys2.\<tau>Runs_table s'' tls))
[PROOF STEP]
with \<tau>diverge_bisim_inv[OF bisim]
[PROOF STATE]
proof (chain)
picking this:
s1 -\<tau>1\<rightarrow> \<infinity> = s2 -\<tau>2\<rightarrow> \<infinity>
stlsss1 = TNil None
s1 -\<tau>1\<rightarrow> \<infinity>
[PROOF STEP]
have ?Diverge
[PROOF STATE]
proof (prove)
using this:
s1 -\<tau>1\<rightarrow> \<infinity> = s2 -\<tau>2\<rightarrow> \<infinity>
stlsss1 = TNil None
s1 -\<tau>1\<rightarrow> \<infinity>

goal (1 subgoal):
 1. \<exists>s. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil None \<and> s -\<tau>2\<rightarrow> \<infinity>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>s. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil None \<and> s -\<tau>2\<rightarrow> \<infinity>

goal (2 subgoals):
 1. \<lbrakk>stlsss1 = TNil None; s1 -\<tau>1\<rightarrow> \<infinity>\<rbrakk> \<Longrightarrow> (\<exists>s s'. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil \<lfloor>s'\<rfloor> \<and> s -\<tau>2\<rightarrow>* s' \<and> (\<forall>x xa. \<not> s' -2-x\<rightarrow> xa)) \<or> (\<exists>s. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil None \<and> s -\<tau>2\<rightarrow> \<infinity>) \<or> (\<exists>s s' s'' tls tl. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TCons (tl, s'') tls \<and> s -\<tau>2\<rightarrow>* s' \<and> s' -2-tl\<rightarrow> s'' \<and> \<not> \<tau>move2 s' tl s'' \<and> ((\<exists>s2 s1 stlsss1. s'' = s2 \<and> tls = tls1_to_tls2 s2 stlsss1 \<and> s1 \<approx> s2 \<and> trsys1.\<tau>Runs_table s1 stlsss1) \<or> trsys2.\<tau>Runs_table s'' tls))
 2. \<And>s' s'' tls tl. \<lbrakk>stlsss1 = TCons (tl, s'') tls; s1 -\<tau>1\<rightarrow>* s'; s' -1-tl\<rightarrow> s''; \<not> \<tau>move1 s' tl s''; trsys1.\<tau>Runs_table s'' tls\<rbrakk> \<Longrightarrow> (\<exists>s s'. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil \<lfloor>s'\<rfloor> \<and> s -\<tau>2\<rightarrow>* s' \<and> (\<forall>x xa. \<not> s' -2-x\<rightarrow> xa)) \<or> (\<exists>s. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil None \<and> s -\<tau>2\<rightarrow> \<infinity>) \<or> (\<exists>s s' s'' tls tl. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TCons (tl, s'') tls \<and> s -\<tau>2\<rightarrow>* s' \<and> s' -2-tl\<rightarrow> s'' \<and> \<not> \<tau>move2 s' tl s'' \<and> ((\<exists>s2 s1 stlsss1. s'' = s2 \<and> tls = tls1_to_tls2 s2 stlsss1 \<and> s1 \<approx> s2 \<and> trsys1.\<tau>Runs_table s1 stlsss1) \<or> trsys2.\<tau>Runs_table s'' tls))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>s. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil None \<and> s -\<tau>2\<rightarrow> \<infinity>

goal (1 subgoal):
 1. (\<exists>s s'. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil \<lfloor>s'\<rfloor> \<and> s -\<tau>2\<rightarrow>* s' \<and> (\<forall>x xa. \<not> s' -2-x\<rightarrow> xa)) \<or> (\<exists>s. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil None \<and> s -\<tau>2\<rightarrow> \<infinity>) \<or> (\<exists>s s' s'' tls tl. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TCons (tl, s'') tls \<and> s -\<tau>2\<rightarrow>* s' \<and> s' -2-tl\<rightarrow> s'' \<and> \<not> \<tau>move2 s' tl s'' \<and> ((\<exists>s2 s1 stlsss1. s'' = s2 \<and> tls = tls1_to_tls2 s2 stlsss1 \<and> s1 \<approx> s2 \<and> trsys1.\<tau>Runs_table s1 stlsss1) \<or> trsys2.\<tau>Runs_table s'' tls))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<exists>s s'. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil \<lfloor>s'\<rfloor> \<and> s -\<tau>2\<rightarrow>* s' \<and> (\<forall>x xa. \<not> s' -2-x\<rightarrow> xa)) \<or> (\<exists>s. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil None \<and> s -\<tau>2\<rightarrow> \<infinity>) \<or> (\<exists>s s' s'' tls tl. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TCons (tl, s'') tls \<and> s -\<tau>2\<rightarrow>* s' \<and> s' -2-tl\<rightarrow> s'' \<and> \<not> \<tau>move2 s' tl s'' \<and> ((\<exists>s2 s1 stlsss1. s'' = s2 \<and> tls = tls1_to_tls2 s2 stlsss1 \<and> s1 \<approx> s2 \<and> trsys1.\<tau>Runs_table s1 stlsss1) \<or> trsys2.\<tau>Runs_table s'' tls))

goal (1 subgoal):
 1. \<And>s' s'' tls tl. \<lbrakk>stlsss1 = TCons (tl, s'') tls; s1 -\<tau>1\<rightarrow>* s'; s' -1-tl\<rightarrow> s''; \<not> \<tau>move1 s' tl s''; trsys1.\<tau>Runs_table s'' tls\<rbrakk> \<Longrightarrow> (\<exists>s s'. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil \<lfloor>s'\<rfloor> \<and> s -\<tau>2\<rightarrow>* s' \<and> (\<forall>x xa. \<not> s' -2-x\<rightarrow> xa)) \<or> (\<exists>s. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil None \<and> s -\<tau>2\<rightarrow> \<infinity>) \<or> (\<exists>s s' s'' tls tl. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TCons (tl, s'') tls \<and> s -\<tau>2\<rightarrow>* s' \<and> s' -2-tl\<rightarrow> s'' \<and> \<not> \<tau>move2 s' tl s'' \<and> ((\<exists>s2 s1 stlsss1. s'' = s2 \<and> tls = tls1_to_tls2 s2 stlsss1 \<and> s1 \<approx> s2 \<and> trsys1.\<tau>Runs_table s1 stlsss1) \<or> trsys2.\<tau>Runs_table s'' tls))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s' s'' tls tl. \<lbrakk>stlsss1 = TCons (tl, s'') tls; s1 -\<tau>1\<rightarrow>* s'; s' -1-tl\<rightarrow> s''; \<not> \<tau>move1 s' tl s''; trsys1.\<tau>Runs_table s'' tls\<rbrakk> \<Longrightarrow> (\<exists>s s'. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil \<lfloor>s'\<rfloor> \<and> s -\<tau>2\<rightarrow>* s' \<and> (\<forall>x xa. \<not> s' -2-x\<rightarrow> xa)) \<or> (\<exists>s. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil None \<and> s -\<tau>2\<rightarrow> \<infinity>) \<or> (\<exists>s s' s'' tls tl. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TCons (tl, s'') tls \<and> s -\<tau>2\<rightarrow>* s' \<and> s' -2-tl\<rightarrow> s'' \<and> \<not> \<tau>move2 s' tl s'' \<and> ((\<exists>s2 s1 stlsss1. s'' = s2 \<and> tls = tls1_to_tls2 s2 stlsss1 \<and> s1 \<approx> s2 \<and> trsys1.\<tau>Runs_table s1 stlsss1) \<or> trsys2.\<tau>Runs_table s'' tls))
[PROOF STEP]
case (Proceed s1' s1'' stlsss1' tl1)
[PROOF STATE]
proof (state)
this:
stlsss1 = TCons (tl1, s1'') stlsss1'
s1 -\<tau>1\<rightarrow>* s1'
s1' -1-tl1\<rightarrow> s1''
\<not> \<tau>move1 s1' tl1 s1''
trsys1.\<tau>Runs_table s1'' stlsss1'

goal (1 subgoal):
 1. \<And>s' s'' tls tl. \<lbrakk>stlsss1 = TCons (tl, s'') tls; s1 -\<tau>1\<rightarrow>* s'; s' -1-tl\<rightarrow> s''; \<not> \<tau>move1 s' tl s''; trsys1.\<tau>Runs_table s'' tls\<rbrakk> \<Longrightarrow> (\<exists>s s'. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil \<lfloor>s'\<rfloor> \<and> s -\<tau>2\<rightarrow>* s' \<and> (\<forall>x xa. \<not> s' -2-x\<rightarrow> xa)) \<or> (\<exists>s. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil None \<and> s -\<tau>2\<rightarrow> \<infinity>) \<or> (\<exists>s s' s'' tls tl. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TCons (tl, s'') tls \<and> s -\<tau>2\<rightarrow>* s' \<and> s' -2-tl\<rightarrow> s'' \<and> \<not> \<tau>move2 s' tl s'' \<and> ((\<exists>s2 s1 stlsss1. s'' = s2 \<and> tls = tls1_to_tls2 s2 stlsss1 \<and> s1 \<approx> s2 \<and> trsys1.\<tau>Runs_table s1 stlsss1) \<or> trsys2.\<tau>Runs_table s'' tls))
[PROOF STEP]
let ?P = "\<lambda>(tl2, s2''). \<exists>s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> s2' -2-tl2\<rightarrow> s2'' \<and> \<not> \<tau>move2 s2' tl2 s2'' \<and> s1'' \<approx> s2'' \<and> tl1 \<sim> tl2"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s' s'' tls tl. \<lbrakk>stlsss1 = TCons (tl, s'') tls; s1 -\<tau>1\<rightarrow>* s'; s' -1-tl\<rightarrow> s''; \<not> \<tau>move1 s' tl s''; trsys1.\<tau>Runs_table s'' tls\<rbrakk> \<Longrightarrow> (\<exists>s s'. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil \<lfloor>s'\<rfloor> \<and> s -\<tau>2\<rightarrow>* s' \<and> (\<forall>x xa. \<not> s' -2-x\<rightarrow> xa)) \<or> (\<exists>s. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil None \<and> s -\<tau>2\<rightarrow> \<infinity>) \<or> (\<exists>s s' s'' tls tl. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TCons (tl, s'') tls \<and> s -\<tau>2\<rightarrow>* s' \<and> s' -2-tl\<rightarrow> s'' \<and> \<not> \<tau>move2 s' tl s'' \<and> ((\<exists>s2 s1 stlsss1. s'' = s2 \<and> tls = tls1_to_tls2 s2 stlsss1 \<and> s1 \<approx> s2 \<and> trsys1.\<tau>Runs_table s1 stlsss1) \<or> trsys2.\<tau>Runs_table s'' tls))
[PROOF STEP]
from simulation_silents1[OF bisim \<open>s1 -\<tau>1\<rightarrow>* s1'\<close>]
[PROOF STATE]
proof (chain)
picking this:
\<exists>s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> s1' \<approx> s2'
[PROOF STEP]
obtain s2' where "s2 -\<tau>2\<rightarrow>* s2'" and "s1' \<approx> s2'"
[PROOF STATE]
proof (prove)
using this:
\<exists>s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> s1' \<approx> s2'

goal (1 subgoal):
 1. (\<And>s2'. \<lbrakk>s2 -\<tau>2\<rightarrow>* s2'; s1' \<approx> s2'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
s2 -\<tau>2\<rightarrow>* s2'
s1' \<approx> s2'

goal (1 subgoal):
 1. \<And>s' s'' tls tl. \<lbrakk>stlsss1 = TCons (tl, s'') tls; s1 -\<tau>1\<rightarrow>* s'; s' -1-tl\<rightarrow> s''; \<not> \<tau>move1 s' tl s''; trsys1.\<tau>Runs_table s'' tls\<rbrakk> \<Longrightarrow> (\<exists>s s'. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil \<lfloor>s'\<rfloor> \<and> s -\<tau>2\<rightarrow>* s' \<and> (\<forall>x xa. \<not> s' -2-x\<rightarrow> xa)) \<or> (\<exists>s. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil None \<and> s -\<tau>2\<rightarrow> \<infinity>) \<or> (\<exists>s s' s'' tls tl. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TCons (tl, s'') tls \<and> s -\<tau>2\<rightarrow>* s' \<and> s' -2-tl\<rightarrow> s'' \<and> \<not> \<tau>move2 s' tl s'' \<and> ((\<exists>s2 s1 stlsss1. s'' = s2 \<and> tls = tls1_to_tls2 s2 stlsss1 \<and> s1 \<approx> s2 \<and> trsys1.\<tau>Runs_table s1 stlsss1) \<or> trsys2.\<tau>Runs_table s'' tls))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
s2 -\<tau>2\<rightarrow>* s2'
s1' \<approx> s2'

goal (1 subgoal):
 1. \<And>s' s'' tls tl. \<lbrakk>stlsss1 = TCons (tl, s'') tls; s1 -\<tau>1\<rightarrow>* s'; s' -1-tl\<rightarrow> s''; \<not> \<tau>move1 s' tl s''; trsys1.\<tau>Runs_table s'' tls\<rbrakk> \<Longrightarrow> (\<exists>s s'. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil \<lfloor>s'\<rfloor> \<and> s -\<tau>2\<rightarrow>* s' \<and> (\<forall>x xa. \<not> s' -2-x\<rightarrow> xa)) \<or> (\<exists>s. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil None \<and> s -\<tau>2\<rightarrow> \<infinity>) \<or> (\<exists>s s' s'' tls tl. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TCons (tl, s'') tls \<and> s -\<tau>2\<rightarrow>* s' \<and> s' -2-tl\<rightarrow> s'' \<and> \<not> \<tau>move2 s' tl s'' \<and> ((\<exists>s2 s1 stlsss1. s'' = s2 \<and> tls = tls1_to_tls2 s2 stlsss1 \<and> s1 \<approx> s2 \<and> trsys1.\<tau>Runs_table s1 stlsss1) \<or> trsys2.\<tau>Runs_table s'' tls))
[PROOF STEP]
from simulation1[OF \<open>s1' \<approx> s2'\<close> \<open>s1' -1-tl1\<rightarrow> s1''\<close> \<open>\<not> \<tau>move1 s1' tl1 s1''\<close>]
[PROOF STATE]
proof (chain)
picking this:
\<exists>s2'a s2'' tl2. s2' -\<tau>2\<rightarrow>* s2'a \<and> s2'a -2-tl2\<rightarrow> s2'' \<and> \<not> \<tau>move2 s2'a tl2 s2'' \<and> s1'' \<approx> s2'' \<and> tl1 \<sim> tl2
[PROOF STEP]
obtain s2'' s2''' tl2 where "s2' -\<tau>2\<rightarrow>* s2''"
        and "s2'' -2-tl2\<rightarrow> s2'''" and "\<not> \<tau>move2 s2'' tl2 s2'''"
        and "s1'' \<approx> s2'''" and "tl1 \<sim> tl2"
[PROOF STATE]
proof (prove)
using this:
\<exists>s2'a s2'' tl2. s2' -\<tau>2\<rightarrow>* s2'a \<and> s2'a -2-tl2\<rightarrow> s2'' \<and> \<not> \<tau>move2 s2'a tl2 s2'' \<and> s1'' \<approx> s2'' \<and> tl1 \<sim> tl2

goal (1 subgoal):
 1. (\<And>s2'' tl2 s2'''. \<lbrakk>s2' -\<tau>2\<rightarrow>* s2''; s2'' -2-tl2\<rightarrow> s2'''; \<not> \<tau>move2 s2'' tl2 s2'''; s1'' \<approx> s2'''; tl1 \<sim> tl2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
s2' -\<tau>2\<rightarrow>* s2''
s2'' -2-tl2\<rightarrow> s2'''
\<not> \<tau>move2 s2'' tl2 s2'''
s1'' \<approx> s2'''
tl1 \<sim> tl2

goal (1 subgoal):
 1. \<And>s' s'' tls tl. \<lbrakk>stlsss1 = TCons (tl, s'') tls; s1 -\<tau>1\<rightarrow>* s'; s' -1-tl\<rightarrow> s''; \<not> \<tau>move1 s' tl s''; trsys1.\<tau>Runs_table s'' tls\<rbrakk> \<Longrightarrow> (\<exists>s s'. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil \<lfloor>s'\<rfloor> \<and> s -\<tau>2\<rightarrow>* s' \<and> (\<forall>x xa. \<not> s' -2-x\<rightarrow> xa)) \<or> (\<exists>s. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil None \<and> s -\<tau>2\<rightarrow> \<infinity>) \<or> (\<exists>s s' s'' tls tl. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TCons (tl, s'') tls \<and> s -\<tau>2\<rightarrow>* s' \<and> s' -2-tl\<rightarrow> s'' \<and> \<not> \<tau>move2 s' tl s'' \<and> ((\<exists>s2 s1 stlsss1. s'' = s2 \<and> tls = tls1_to_tls2 s2 stlsss1 \<and> s1 \<approx> s2 \<and> trsys1.\<tau>Runs_table s1 stlsss1) \<or> trsys2.\<tau>Runs_table s'' tls))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
s2 -\<tau>2\<rightarrow>* s2'
s1' \<approx> s2'
s2' -\<tau>2\<rightarrow>* s2''
s2'' -2-tl2\<rightarrow> s2'''
\<not> \<tau>move2 s2'' tl2 s2'''
s1'' \<approx> s2'''
tl1 \<sim> tl2
[PROOF STEP]
have "?P (tl2, s2''')"
[PROOF STATE]
proof (prove)
using this:
s2 -\<tau>2\<rightarrow>* s2'
s1' \<approx> s2'
s2' -\<tau>2\<rightarrow>* s2''
s2'' -2-tl2\<rightarrow> s2'''
\<not> \<tau>move2 s2'' tl2 s2'''
s1'' \<approx> s2'''
tl1 \<sim> tl2

goal (1 subgoal):
 1. case (tl2, s2''') of (tl2, s2'') \<Rightarrow> \<exists>s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> s2' -2-tl2\<rightarrow> s2'' \<and> \<not> \<tau>move2 s2' tl2 s2'' \<and> s1'' \<approx> s2'' \<and> tl1 \<sim> tl2
[PROOF STEP]
by(blast intro: rtranclp_trans)
[PROOF STATE]
proof (state)
this:
case (tl2, s2''') of (tl2, s2'') \<Rightarrow> \<exists>s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> s2' -2-tl2\<rightarrow> s2'' \<and> \<not> \<tau>move2 s2' tl2 s2'' \<and> s1'' \<approx> s2'' \<and> tl1 \<sim> tl2

goal (1 subgoal):
 1. \<And>s' s'' tls tl. \<lbrakk>stlsss1 = TCons (tl, s'') tls; s1 -\<tau>1\<rightarrow>* s'; s' -1-tl\<rightarrow> s''; \<not> \<tau>move1 s' tl s''; trsys1.\<tau>Runs_table s'' tls\<rbrakk> \<Longrightarrow> (\<exists>s s'. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil \<lfloor>s'\<rfloor> \<and> s -\<tau>2\<rightarrow>* s' \<and> (\<forall>x xa. \<not> s' -2-x\<rightarrow> xa)) \<or> (\<exists>s. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil None \<and> s -\<tau>2\<rightarrow> \<infinity>) \<or> (\<exists>s s' s'' tls tl. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TCons (tl, s'') tls \<and> s -\<tau>2\<rightarrow>* s' \<and> s' -2-tl\<rightarrow> s'' \<and> \<not> \<tau>move2 s' tl s'' \<and> ((\<exists>s2 s1 stlsss1. s'' = s2 \<and> tls = tls1_to_tls2 s2 stlsss1 \<and> s1 \<approx> s2 \<and> trsys1.\<tau>Runs_table s1 stlsss1) \<or> trsys2.\<tau>Runs_table s'' tls))
[PROOF STEP]
hence "?P (Eps ?P)"
[PROOF STATE]
proof (prove)
using this:
case (tl2, s2''') of (tl2, s2'') \<Rightarrow> \<exists>s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> s2' -2-tl2\<rightarrow> s2'' \<and> \<not> \<tau>move2 s2' tl2 s2'' \<and> s1'' \<approx> s2'' \<and> tl1 \<sim> tl2

goal (1 subgoal):
 1. case SOME (tl2, s2''). \<exists>s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> s2' -2-tl2\<rightarrow> s2'' \<and> \<not> \<tau>move2 s2' tl2 s2'' \<and> s1'' \<approx> s2'' \<and> tl1 \<sim> tl2 of (tl2, s2'') \<Rightarrow> \<exists>s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> s2' -2-tl2\<rightarrow> s2'' \<and> \<not> \<tau>move2 s2' tl2 s2'' \<and> s1'' \<approx> s2'' \<and> tl1 \<sim> tl2
[PROOF STEP]
by(rule someI)
[PROOF STATE]
proof (state)
this:
case SOME (tl2, s2''). \<exists>s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> s2' -2-tl2\<rightarrow> s2'' \<and> \<not> \<tau>move2 s2' tl2 s2'' \<and> s1'' \<approx> s2'' \<and> tl1 \<sim> tl2 of (tl2, s2'') \<Rightarrow> \<exists>s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> s2' -2-tl2\<rightarrow> s2'' \<and> \<not> \<tau>move2 s2' tl2 s2'' \<and> s1'' \<approx> s2'' \<and> tl1 \<sim> tl2

goal (1 subgoal):
 1. \<And>s' s'' tls tl. \<lbrakk>stlsss1 = TCons (tl, s'') tls; s1 -\<tau>1\<rightarrow>* s'; s' -1-tl\<rightarrow> s''; \<not> \<tau>move1 s' tl s''; trsys1.\<tau>Runs_table s'' tls\<rbrakk> \<Longrightarrow> (\<exists>s s'. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil \<lfloor>s'\<rfloor> \<and> s -\<tau>2\<rightarrow>* s' \<and> (\<forall>x xa. \<not> s' -2-x\<rightarrow> xa)) \<or> (\<exists>s. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil None \<and> s -\<tau>2\<rightarrow> \<infinity>) \<or> (\<exists>s s' s'' tls tl. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TCons (tl, s'') tls \<and> s -\<tau>2\<rightarrow>* s' \<and> s' -2-tl\<rightarrow> s'' \<and> \<not> \<tau>move2 s' tl s'' \<and> ((\<exists>s2 s1 stlsss1. s'' = s2 \<and> tls = tls1_to_tls2 s2 stlsss1 \<and> s1 \<approx> s2 \<and> trsys1.\<tau>Runs_table s1 stlsss1) \<or> trsys2.\<tau>Runs_table s'' tls))
[PROOF STEP]
hence ?Proceed
[PROOF STATE]
proof (prove)
using this:
case SOME (tl2, s2''). \<exists>s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> s2' -2-tl2\<rightarrow> s2'' \<and> \<not> \<tau>move2 s2' tl2 s2'' \<and> s1'' \<approx> s2'' \<and> tl1 \<sim> tl2 of (tl2, s2'') \<Rightarrow> \<exists>s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> s2' -2-tl2\<rightarrow> s2'' \<and> \<not> \<tau>move2 s2' tl2 s2'' \<and> s1'' \<approx> s2'' \<and> tl1 \<sim> tl2

goal (1 subgoal):
 1. \<exists>s s' s'' tls tl. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TCons (tl, s'') tls \<and> s -\<tau>2\<rightarrow>* s' \<and> s' -2-tl\<rightarrow> s'' \<and> \<not> \<tau>move2 s' tl s'' \<and> ((\<exists>s2 s1 stlsss1. s'' = s2 \<and> tls = tls1_to_tls2 s2 stlsss1 \<and> s1 \<approx> s2 \<and> trsys1.\<tau>Runs_table s1 stlsss1) \<or> trsys2.\<tau>Runs_table s'' tls)
[PROOF STEP]
using \<open>stlsss1 = TCons (tl1, s1'') stlsss1'\<close> \<open>trsys1.\<tau>Runs_table s1'' stlsss1'\<close>
[PROOF STATE]
proof (prove)
using this:
case SOME (tl2, s2''). \<exists>s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> s2' -2-tl2\<rightarrow> s2'' \<and> \<not> \<tau>move2 s2' tl2 s2'' \<and> s1'' \<approx> s2'' \<and> tl1 \<sim> tl2 of (tl2, s2'') \<Rightarrow> \<exists>s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> s2' -2-tl2\<rightarrow> s2'' \<and> \<not> \<tau>move2 s2' tl2 s2'' \<and> s1'' \<approx> s2'' \<and> tl1 \<sim> tl2
stlsss1 = TCons (tl1, s1'') stlsss1'
trsys1.\<tau>Runs_table s1'' stlsss1'

goal (1 subgoal):
 1. \<exists>s s' s'' tls tl. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TCons (tl, s'') tls \<and> s -\<tau>2\<rightarrow>* s' \<and> s' -2-tl\<rightarrow> s'' \<and> \<not> \<tau>move2 s' tl s'' \<and> ((\<exists>s2 s1 stlsss1. s'' = s2 \<and> tls = tls1_to_tls2 s2 stlsss1 \<and> s1 \<approx> s2 \<and> trsys1.\<tau>Runs_table s1 stlsss1) \<or> trsys2.\<tau>Runs_table s'' tls)
[PROOF STEP]
by auto blast
[PROOF STATE]
proof (state)
this:
\<exists>s s' s'' tls tl. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TCons (tl, s'') tls \<and> s -\<tau>2\<rightarrow>* s' \<and> s' -2-tl\<rightarrow> s'' \<and> \<not> \<tau>move2 s' tl s'' \<and> ((\<exists>s2 s1 stlsss1. s'' = s2 \<and> tls = tls1_to_tls2 s2 stlsss1 \<and> s1 \<approx> s2 \<and> trsys1.\<tau>Runs_table s1 stlsss1) \<or> trsys2.\<tau>Runs_table s'' tls)

goal (1 subgoal):
 1. \<And>s' s'' tls tl. \<lbrakk>stlsss1 = TCons (tl, s'') tls; s1 -\<tau>1\<rightarrow>* s'; s' -1-tl\<rightarrow> s''; \<not> \<tau>move1 s' tl s''; trsys1.\<tau>Runs_table s'' tls\<rbrakk> \<Longrightarrow> (\<exists>s s'. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil \<lfloor>s'\<rfloor> \<and> s -\<tau>2\<rightarrow>* s' \<and> (\<forall>x xa. \<not> s' -2-x\<rightarrow> xa)) \<or> (\<exists>s. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil None \<and> s -\<tau>2\<rightarrow> \<infinity>) \<or> (\<exists>s s' s'' tls tl. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TCons (tl, s'') tls \<and> s -\<tau>2\<rightarrow>* s' \<and> s' -2-tl\<rightarrow> s'' \<and> \<not> \<tau>move2 s' tl s'' \<and> ((\<exists>s2 s1 stlsss1. s'' = s2 \<and> tls = tls1_to_tls2 s2 stlsss1 \<and> s1 \<approx> s2 \<and> trsys1.\<tau>Runs_table s1 stlsss1) \<or> trsys2.\<tau>Runs_table s'' tls))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>s s' s'' tls tl. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TCons (tl, s'') tls \<and> s -\<tau>2\<rightarrow>* s' \<and> s' -2-tl\<rightarrow> s'' \<and> \<not> \<tau>move2 s' tl s'' \<and> ((\<exists>s2 s1 stlsss1. s'' = s2 \<and> tls = tls1_to_tls2 s2 stlsss1 \<and> s1 \<approx> s2 \<and> trsys1.\<tau>Runs_table s1 stlsss1) \<or> trsys2.\<tau>Runs_table s'' tls)

goal (1 subgoal):
 1. (\<exists>s s'. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil \<lfloor>s'\<rfloor> \<and> s -\<tau>2\<rightarrow>* s' \<and> (\<forall>x xa. \<not> s' -2-x\<rightarrow> xa)) \<or> (\<exists>s. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil None \<and> s -\<tau>2\<rightarrow> \<infinity>) \<or> (\<exists>s s' s'' tls tl. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TCons (tl, s'') tls \<and> s -\<tau>2\<rightarrow>* s' \<and> s' -2-tl\<rightarrow> s'' \<and> \<not> \<tau>move2 s' tl s'' \<and> ((\<exists>s2 s1 stlsss1. s'' = s2 \<and> tls = tls1_to_tls2 s2 stlsss1 \<and> s1 \<approx> s2 \<and> trsys1.\<tau>Runs_table s1 stlsss1) \<or> trsys2.\<tau>Runs_table s'' tls))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<exists>s s'. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil \<lfloor>s'\<rfloor> \<and> s -\<tau>2\<rightarrow>* s' \<and> (\<forall>x xa. \<not> s' -2-x\<rightarrow> xa)) \<or> (\<exists>s. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil None \<and> s -\<tau>2\<rightarrow> \<infinity>) \<or> (\<exists>s s' s'' tls tl. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TCons (tl, s'') tls \<and> s -\<tau>2\<rightarrow>* s' \<and> s' -2-tl\<rightarrow> s'' \<and> \<not> \<tau>move2 s' tl s'' \<and> ((\<exists>s2 s1 stlsss1. s'' = s2 \<and> tls = tls1_to_tls2 s2 stlsss1 \<and> s1 \<approx> s2 \<and> trsys1.\<tau>Runs_table s1 stlsss1) \<or> trsys2.\<tau>Runs_table s'' tls))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<exists>s s'. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil \<lfloor>s'\<rfloor> \<and> s -\<tau>2\<rightarrow>* s' \<and> (\<forall>x xa. \<not> s' -2-x\<rightarrow> xa)) \<or> (\<exists>s. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TNil None \<and> s -\<tau>2\<rightarrow> \<infinity>) \<or> (\<exists>s s' s'' tls tl. s2 = s \<and> tls1_to_tls2 s2 stlsss1 = TCons (tl, s'') tls \<and> s -\<tau>2\<rightarrow>* s' \<and> s' -2-tl\<rightarrow> s'' \<and> \<not> \<tau>move2 s' tl s'' \<and> ((\<exists>s2 s1 stlsss1. s'' = s2 \<and> tls = tls1_to_tls2 s2 stlsss1 \<and> s1 \<approx> s2 \<and> trsys1.\<tau>Runs_table s1 stlsss1) \<or> trsys2.\<tau>Runs_table s'' tls))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
trsys2.\<tau>Runs_table s2 (tls1_to_tls2 s2 stlsss1)

goal (1 subgoal):
 1. tllist_all2 (\<lambda>(tl1, s1'') (tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (rel_option bisim) stlsss1 (unfold_tllist (\<lambda>(s2, y). is_TNil y) (\<lambda>(s2, stlsss1). map_option (\<lambda>s1'. SOME s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> (\<forall>tl s2''. \<not> s2' -2-tl\<rightarrow> s2'') \<and> s1' \<approx> s2') (terminal stlsss1)) (\<lambda>(s2, stlsss1). let (x, y) = SOME (tl2, s2''). \<exists>s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> s2' -2-tl2\<rightarrow> s2'' \<and> \<not> \<tau>move2 s2' tl2 s2'' \<and> snd (thd stlsss1) \<approx> s2'' \<and> fst (thd stlsss1) \<sim> tl2 in (x, y)) (\<lambda>(s2, stlsss1). let (tl2, s2'') = SOME (tl2, s2''). \<exists>s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> s2' -2-tl2\<rightarrow> s2'' \<and> \<not> \<tau>move2 s2' tl2 s2'' \<and> snd (thd stlsss1) \<approx> s2'' \<and> fst (thd stlsss1) \<sim> tl2 in (s2'', ttl stlsss1)) (s2, stlsss1))
[PROOF STEP]
let ?Tlsim = "\<lambda>(tl1, s1'') (tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2''"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. tllist_all2 (\<lambda>(tl1, s1'') (tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (rel_option bisim) stlsss1 (unfold_tllist (\<lambda>(s2, y). is_TNil y) (\<lambda>(s2, stlsss1). map_option (\<lambda>s1'. SOME s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> (\<forall>tl s2''. \<not> s2' -2-tl\<rightarrow> s2'') \<and> s1' \<approx> s2') (terminal stlsss1)) (\<lambda>(s2, stlsss1). let (x, y) = SOME (tl2, s2''). \<exists>s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> s2' -2-tl2\<rightarrow> s2'' \<and> \<not> \<tau>move2 s2' tl2 s2'' \<and> snd (thd stlsss1) \<approx> s2'' \<and> fst (thd stlsss1) \<sim> tl2 in (x, y)) (\<lambda>(s2, stlsss1). let (tl2, s2'') = SOME (tl2, s2''). \<exists>s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> s2' -2-tl2\<rightarrow> s2'' \<and> \<not> \<tau>move2 s2' tl2 s2'' \<and> snd (thd stlsss1) \<approx> s2'' \<and> fst (thd stlsss1) \<sim> tl2 in (s2'', ttl stlsss1)) (s2, stlsss1))
[PROOF STEP]
let ?Bisim = "rel_option bisim"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. tllist_all2 (\<lambda>(tl1, s1'') (tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (rel_option bisim) stlsss1 (unfold_tllist (\<lambda>(s2, y). is_TNil y) (\<lambda>(s2, stlsss1). map_option (\<lambda>s1'. SOME s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> (\<forall>tl s2''. \<not> s2' -2-tl\<rightarrow> s2'') \<and> s1' \<approx> s2') (terminal stlsss1)) (\<lambda>(s2, stlsss1). let (x, y) = SOME (tl2, s2''). \<exists>s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> s2' -2-tl2\<rightarrow> s2'' \<and> \<not> \<tau>move2 s2' tl2 s2'' \<and> snd (thd stlsss1) \<approx> s2'' \<and> fst (thd stlsss1) \<sim> tl2 in (x, y)) (\<lambda>(s2, stlsss1). let (tl2, s2'') = SOME (tl2, s2''). \<exists>s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> s2' -2-tl2\<rightarrow> s2'' \<and> \<not> \<tau>move2 s2' tl2 s2'' \<and> snd (thd stlsss1) \<approx> s2'' \<and> fst (thd stlsss1) \<sim> tl2 in (s2'', ttl stlsss1)) (s2, stlsss1))
[PROOF STEP]
from run1 bisim
[PROOF STATE]
proof (chain)
picking this:
trsys1.\<tau>Runs_table s1 stlsss1
s1 \<approx> s2
[PROOF STEP]
show "tllist_all2 ?Tlsim ?Bisim stlsss1 (tls1_to_tls2 s2 stlsss1)"
[PROOF STATE]
proof (prove)
using this:
trsys1.\<tau>Runs_table s1 stlsss1
s1 \<approx> s2

goal (1 subgoal):
 1. tllist_all2 (\<lambda>(tl1, s1'') (tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (rel_option bisim) stlsss1 (tls1_to_tls2 s2 stlsss1)
[PROOF STEP]
proof(coinduction arbitrary: s1 s2 stlsss1)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s1 s2 stlsss1. \<lbrakk>trsys1.\<tau>Runs_table s1 stlsss1; s1 \<approx> s2\<rbrakk> \<Longrightarrow> is_TNil stlsss1 = is_TNil (tls1_to_tls2 s2 stlsss1) \<and> (is_TNil stlsss1 \<longrightarrow> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> rel_option bisim (terminal stlsss1) (terminal (tls1_to_tls2 s2 stlsss1))) \<and> (\<not> is_TNil stlsss1 \<longrightarrow> \<not> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> (case thd stlsss1 of (tl1, s1'') \<Rightarrow> \<lambda>(tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (thd (tls1_to_tls2 s2 stlsss1)) \<and> ((\<exists>s1 s2a stlsss1a. ttl stlsss1 = stlsss1a \<and> ttl (tls1_to_tls2 s2 stlsss1) = tls1_to_tls2 s2a stlsss1a \<and> trsys1.\<tau>Runs_table s1 stlsss1a \<and> s1 \<approx> s2a) \<or> tllist_all2 (\<lambda>(tl1, s1'') (tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (rel_option bisim) (ttl stlsss1) (ttl (tls1_to_tls2 s2 stlsss1))))
[PROOF STEP]
case (tllist_all2 s1 s2 stlsss1)
[PROOF STATE]
proof (state)
this:
trsys1.\<tau>Runs_table s1 stlsss1
s1 \<approx> s2

goal (1 subgoal):
 1. \<And>s1 s2 stlsss1. \<lbrakk>trsys1.\<tau>Runs_table s1 stlsss1; s1 \<approx> s2\<rbrakk> \<Longrightarrow> is_TNil stlsss1 = is_TNil (tls1_to_tls2 s2 stlsss1) \<and> (is_TNil stlsss1 \<longrightarrow> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> rel_option bisim (terminal stlsss1) (terminal (tls1_to_tls2 s2 stlsss1))) \<and> (\<not> is_TNil stlsss1 \<longrightarrow> \<not> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> (case thd stlsss1 of (tl1, s1'') \<Rightarrow> \<lambda>(tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (thd (tls1_to_tls2 s2 stlsss1)) \<and> ((\<exists>s1 s2a stlsss1a. ttl stlsss1 = stlsss1a \<and> ttl (tls1_to_tls2 s2 stlsss1) = tls1_to_tls2 s2a stlsss1a \<and> trsys1.\<tau>Runs_table s1 stlsss1a \<and> s1 \<approx> s2a) \<or> tllist_all2 (\<lambda>(tl1, s1'') (tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (rel_option bisim) (ttl stlsss1) (ttl (tls1_to_tls2 s2 stlsss1))))
[PROOF STEP]
note Runs = \<open>trsys1.\<tau>Runs_table s1 stlsss1\<close> and bisim = \<open>s1 \<approx> s2\<close>
[PROOF STATE]
proof (state)
this:
trsys1.\<tau>Runs_table s1 stlsss1
s1 \<approx> s2

goal (1 subgoal):
 1. \<And>s1 s2 stlsss1. \<lbrakk>trsys1.\<tau>Runs_table s1 stlsss1; s1 \<approx> s2\<rbrakk> \<Longrightarrow> is_TNil stlsss1 = is_TNil (tls1_to_tls2 s2 stlsss1) \<and> (is_TNil stlsss1 \<longrightarrow> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> rel_option bisim (terminal stlsss1) (terminal (tls1_to_tls2 s2 stlsss1))) \<and> (\<not> is_TNil stlsss1 \<longrightarrow> \<not> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> (case thd stlsss1 of (tl1, s1'') \<Rightarrow> \<lambda>(tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (thd (tls1_to_tls2 s2 stlsss1)) \<and> ((\<exists>s1 s2a stlsss1a. ttl stlsss1 = stlsss1a \<and> ttl (tls1_to_tls2 s2 stlsss1) = tls1_to_tls2 s2a stlsss1a \<and> trsys1.\<tau>Runs_table s1 stlsss1a \<and> s1 \<approx> s2a) \<or> tllist_all2 (\<lambda>(tl1, s1'') (tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (rel_option bisim) (ttl stlsss1) (ttl (tls1_to_tls2 s2 stlsss1))))
[PROOF STEP]
from Runs
[PROOF STATE]
proof (chain)
picking this:
trsys1.\<tau>Runs_table s1 stlsss1
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
trsys1.\<tau>Runs_table s1 stlsss1

goal (1 subgoal):
 1. is_TNil stlsss1 = is_TNil (tls1_to_tls2 s2 stlsss1) \<and> (is_TNil stlsss1 \<longrightarrow> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> rel_option bisim (terminal stlsss1) (terminal (tls1_to_tls2 s2 stlsss1))) \<and> (\<not> is_TNil stlsss1 \<longrightarrow> \<not> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> (case thd stlsss1 of (tl1, s1'') \<Rightarrow> \<lambda>(tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (thd (tls1_to_tls2 s2 stlsss1)) \<and> ((\<exists>s1 s2 stlsss1. ttl stlsss1 = stlsss1 \<and> ttl (tls1_to_tls2 s2 stlsss1) = tls1_to_tls2 s2 stlsss1 \<and> trsys1.\<tau>Runs_table s1 stlsss1 \<and> s1 \<approx> s2) \<or> tllist_all2 (\<lambda>(tl1, s1'') (tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (rel_option bisim) (ttl stlsss1) (ttl (tls1_to_tls2 s2 stlsss1))))
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>s'. \<lbrakk>stlsss1 = TNil \<lfloor>s'\<rfloor>; s1 -\<tau>1\<rightarrow>* s'; \<And>tl s''. \<not> s' -1-tl\<rightarrow> s''\<rbrakk> \<Longrightarrow> is_TNil stlsss1 = is_TNil (tls1_to_tls2 s2 stlsss1) \<and> (is_TNil stlsss1 \<longrightarrow> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> rel_option bisim (terminal stlsss1) (terminal (tls1_to_tls2 s2 stlsss1))) \<and> (\<not> is_TNil stlsss1 \<longrightarrow> \<not> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> (case thd stlsss1 of (tl1, s1'') \<Rightarrow> \<lambda>(tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (thd (tls1_to_tls2 s2 stlsss1)) \<and> ((\<exists>s1 s2 stlsss1. ttl stlsss1 = stlsss1 \<and> ttl (tls1_to_tls2 s2 stlsss1) = tls1_to_tls2 s2 stlsss1 \<and> trsys1.\<tau>Runs_table s1 stlsss1 \<and> s1 \<approx> s2) \<or> tllist_all2 (\<lambda>(tl1, s1'') (tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (rel_option bisim) (ttl stlsss1) (ttl (tls1_to_tls2 s2 stlsss1))))
 2. \<lbrakk>stlsss1 = TNil None; s1 -\<tau>1\<rightarrow> \<infinity>\<rbrakk> \<Longrightarrow> is_TNil stlsss1 = is_TNil (tls1_to_tls2 s2 stlsss1) \<and> (is_TNil stlsss1 \<longrightarrow> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> rel_option bisim (terminal stlsss1) (terminal (tls1_to_tls2 s2 stlsss1))) \<and> (\<not> is_TNil stlsss1 \<longrightarrow> \<not> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> (case thd stlsss1 of (tl1, s1'') \<Rightarrow> \<lambda>(tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (thd (tls1_to_tls2 s2 stlsss1)) \<and> ((\<exists>s1 s2 stlsss1. ttl stlsss1 = stlsss1 \<and> ttl (tls1_to_tls2 s2 stlsss1) = tls1_to_tls2 s2 stlsss1 \<and> trsys1.\<tau>Runs_table s1 stlsss1 \<and> s1 \<approx> s2) \<or> tllist_all2 (\<lambda>(tl1, s1'') (tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (rel_option bisim) (ttl stlsss1) (ttl (tls1_to_tls2 s2 stlsss1))))
 3. \<And>s' s'' tls tl. \<lbrakk>stlsss1 = TCons (tl, s'') tls; s1 -\<tau>1\<rightarrow>* s'; s' -1-tl\<rightarrow> s''; \<not> \<tau>move1 s' tl s''; trsys1.\<tau>Runs_table s'' tls\<rbrakk> \<Longrightarrow> is_TNil stlsss1 = is_TNil (tls1_to_tls2 s2 stlsss1) \<and> (is_TNil stlsss1 \<longrightarrow> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> rel_option bisim (terminal stlsss1) (terminal (tls1_to_tls2 s2 stlsss1))) \<and> (\<not> is_TNil stlsss1 \<longrightarrow> \<not> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> (case thd stlsss1 of (tl1, s1'') \<Rightarrow> \<lambda>(tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (thd (tls1_to_tls2 s2 stlsss1)) \<and> ((\<exists>s1 s2 stlsss1. ttl stlsss1 = stlsss1 \<and> ttl (tls1_to_tls2 s2 stlsss1) = tls1_to_tls2 s2 stlsss1 \<and> trsys1.\<tau>Runs_table s1 stlsss1 \<and> s1 \<approx> s2) \<or> tllist_all2 (\<lambda>(tl1, s1'') (tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (rel_option bisim) (ttl stlsss1) (ttl (tls1_to_tls2 s2 stlsss1))))
[PROOF STEP]
case (Terminate s1')
[PROOF STATE]
proof (state)
this:
stlsss1 = TNil \<lfloor>s1'\<rfloor>
s1 -\<tau>1\<rightarrow>* s1'
\<not> s1' -1-?tl1\<rightarrow> ?s''1

goal (3 subgoals):
 1. \<And>s'. \<lbrakk>stlsss1 = TNil \<lfloor>s'\<rfloor>; s1 -\<tau>1\<rightarrow>* s'; \<And>tl s''. \<not> s' -1-tl\<rightarrow> s''\<rbrakk> \<Longrightarrow> is_TNil stlsss1 = is_TNil (tls1_to_tls2 s2 stlsss1) \<and> (is_TNil stlsss1 \<longrightarrow> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> rel_option bisim (terminal stlsss1) (terminal (tls1_to_tls2 s2 stlsss1))) \<and> (\<not> is_TNil stlsss1 \<longrightarrow> \<not> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> (case thd stlsss1 of (tl1, s1'') \<Rightarrow> \<lambda>(tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (thd (tls1_to_tls2 s2 stlsss1)) \<and> ((\<exists>s1 s2 stlsss1. ttl stlsss1 = stlsss1 \<and> ttl (tls1_to_tls2 s2 stlsss1) = tls1_to_tls2 s2 stlsss1 \<and> trsys1.\<tau>Runs_table s1 stlsss1 \<and> s1 \<approx> s2) \<or> tllist_all2 (\<lambda>(tl1, s1'') (tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (rel_option bisim) (ttl stlsss1) (ttl (tls1_to_tls2 s2 stlsss1))))
 2. \<lbrakk>stlsss1 = TNil None; s1 -\<tau>1\<rightarrow> \<infinity>\<rbrakk> \<Longrightarrow> is_TNil stlsss1 = is_TNil (tls1_to_tls2 s2 stlsss1) \<and> (is_TNil stlsss1 \<longrightarrow> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> rel_option bisim (terminal stlsss1) (terminal (tls1_to_tls2 s2 stlsss1))) \<and> (\<not> is_TNil stlsss1 \<longrightarrow> \<not> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> (case thd stlsss1 of (tl1, s1'') \<Rightarrow> \<lambda>(tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (thd (tls1_to_tls2 s2 stlsss1)) \<and> ((\<exists>s1 s2 stlsss1. ttl stlsss1 = stlsss1 \<and> ttl (tls1_to_tls2 s2 stlsss1) = tls1_to_tls2 s2 stlsss1 \<and> trsys1.\<tau>Runs_table s1 stlsss1 \<and> s1 \<approx> s2) \<or> tllist_all2 (\<lambda>(tl1, s1'') (tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (rel_option bisim) (ttl stlsss1) (ttl (tls1_to_tls2 s2 stlsss1))))
 3. \<And>s' s'' tls tl. \<lbrakk>stlsss1 = TCons (tl, s'') tls; s1 -\<tau>1\<rightarrow>* s'; s' -1-tl\<rightarrow> s''; \<not> \<tau>move1 s' tl s''; trsys1.\<tau>Runs_table s'' tls\<rbrakk> \<Longrightarrow> is_TNil stlsss1 = is_TNil (tls1_to_tls2 s2 stlsss1) \<and> (is_TNil stlsss1 \<longrightarrow> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> rel_option bisim (terminal stlsss1) (terminal (tls1_to_tls2 s2 stlsss1))) \<and> (\<not> is_TNil stlsss1 \<longrightarrow> \<not> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> (case thd stlsss1 of (tl1, s1'') \<Rightarrow> \<lambda>(tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (thd (tls1_to_tls2 s2 stlsss1)) \<and> ((\<exists>s1 s2 stlsss1. ttl stlsss1 = stlsss1 \<and> ttl (tls1_to_tls2 s2 stlsss1) = tls1_to_tls2 s2 stlsss1 \<and> trsys1.\<tau>Runs_table s1 stlsss1 \<and> s1 \<approx> s2) \<or> tllist_all2 (\<lambda>(tl1, s1'') (tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (rel_option bisim) (ttl stlsss1) (ttl (tls1_to_tls2 s2 stlsss1))))
[PROOF STEP]
let ?P = "\<lambda>s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> (\<forall>tl2 s2''. \<not> s2' -2-tl2\<rightarrow> s2'') \<and> s1' \<approx> s2'"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>s'. \<lbrakk>stlsss1 = TNil \<lfloor>s'\<rfloor>; s1 -\<tau>1\<rightarrow>* s'; \<And>tl s''. \<not> s' -1-tl\<rightarrow> s''\<rbrakk> \<Longrightarrow> is_TNil stlsss1 = is_TNil (tls1_to_tls2 s2 stlsss1) \<and> (is_TNil stlsss1 \<longrightarrow> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> rel_option bisim (terminal stlsss1) (terminal (tls1_to_tls2 s2 stlsss1))) \<and> (\<not> is_TNil stlsss1 \<longrightarrow> \<not> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> (case thd stlsss1 of (tl1, s1'') \<Rightarrow> \<lambda>(tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (thd (tls1_to_tls2 s2 stlsss1)) \<and> ((\<exists>s1 s2 stlsss1. ttl stlsss1 = stlsss1 \<and> ttl (tls1_to_tls2 s2 stlsss1) = tls1_to_tls2 s2 stlsss1 \<and> trsys1.\<tau>Runs_table s1 stlsss1 \<and> s1 \<approx> s2) \<or> tllist_all2 (\<lambda>(tl1, s1'') (tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (rel_option bisim) (ttl stlsss1) (ttl (tls1_to_tls2 s2 stlsss1))))
 2. \<lbrakk>stlsss1 = TNil None; s1 -\<tau>1\<rightarrow> \<infinity>\<rbrakk> \<Longrightarrow> is_TNil stlsss1 = is_TNil (tls1_to_tls2 s2 stlsss1) \<and> (is_TNil stlsss1 \<longrightarrow> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> rel_option bisim (terminal stlsss1) (terminal (tls1_to_tls2 s2 stlsss1))) \<and> (\<not> is_TNil stlsss1 \<longrightarrow> \<not> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> (case thd stlsss1 of (tl1, s1'') \<Rightarrow> \<lambda>(tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (thd (tls1_to_tls2 s2 stlsss1)) \<and> ((\<exists>s1 s2 stlsss1. ttl stlsss1 = stlsss1 \<and> ttl (tls1_to_tls2 s2 stlsss1) = tls1_to_tls2 s2 stlsss1 \<and> trsys1.\<tau>Runs_table s1 stlsss1 \<and> s1 \<approx> s2) \<or> tllist_all2 (\<lambda>(tl1, s1'') (tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (rel_option bisim) (ttl stlsss1) (ttl (tls1_to_tls2 s2 stlsss1))))
 3. \<And>s' s'' tls tl. \<lbrakk>stlsss1 = TCons (tl, s'') tls; s1 -\<tau>1\<rightarrow>* s'; s' -1-tl\<rightarrow> s''; \<not> \<tau>move1 s' tl s''; trsys1.\<tau>Runs_table s'' tls\<rbrakk> \<Longrightarrow> is_TNil stlsss1 = is_TNil (tls1_to_tls2 s2 stlsss1) \<and> (is_TNil stlsss1 \<longrightarrow> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> rel_option bisim (terminal stlsss1) (terminal (tls1_to_tls2 s2 stlsss1))) \<and> (\<not> is_TNil stlsss1 \<longrightarrow> \<not> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> (case thd stlsss1 of (tl1, s1'') \<Rightarrow> \<lambda>(tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (thd (tls1_to_tls2 s2 stlsss1)) \<and> ((\<exists>s1 s2 stlsss1. ttl stlsss1 = stlsss1 \<and> ttl (tls1_to_tls2 s2 stlsss1) = tls1_to_tls2 s2 stlsss1 \<and> trsys1.\<tau>Runs_table s1 stlsss1 \<and> s1 \<approx> s2) \<or> tllist_all2 (\<lambda>(tl1, s1'') (tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (rel_option bisim) (ttl stlsss1) (ttl (tls1_to_tls2 s2 stlsss1))))
[PROOF STEP]
from simulation_silents1[OF bisim \<open>s1 -\<tau>1\<rightarrow>* s1'\<close>]
[PROOF STATE]
proof (chain)
picking this:
\<exists>s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> s1' \<approx> s2'
[PROOF STEP]
obtain s2' where "s2 -\<tau>2\<rightarrow>* s2'" and "s1' \<approx> s2'"
[PROOF STATE]
proof (prove)
using this:
\<exists>s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> s1' \<approx> s2'

goal (1 subgoal):
 1. (\<And>s2'. \<lbrakk>s2 -\<tau>2\<rightarrow>* s2'; s1' \<approx> s2'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
s2 -\<tau>2\<rightarrow>* s2'
s1' \<approx> s2'

goal (3 subgoals):
 1. \<And>s'. \<lbrakk>stlsss1 = TNil \<lfloor>s'\<rfloor>; s1 -\<tau>1\<rightarrow>* s'; \<And>tl s''. \<not> s' -1-tl\<rightarrow> s''\<rbrakk> \<Longrightarrow> is_TNil stlsss1 = is_TNil (tls1_to_tls2 s2 stlsss1) \<and> (is_TNil stlsss1 \<longrightarrow> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> rel_option bisim (terminal stlsss1) (terminal (tls1_to_tls2 s2 stlsss1))) \<and> (\<not> is_TNil stlsss1 \<longrightarrow> \<not> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> (case thd stlsss1 of (tl1, s1'') \<Rightarrow> \<lambda>(tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (thd (tls1_to_tls2 s2 stlsss1)) \<and> ((\<exists>s1 s2 stlsss1. ttl stlsss1 = stlsss1 \<and> ttl (tls1_to_tls2 s2 stlsss1) = tls1_to_tls2 s2 stlsss1 \<and> trsys1.\<tau>Runs_table s1 stlsss1 \<and> s1 \<approx> s2) \<or> tllist_all2 (\<lambda>(tl1, s1'') (tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (rel_option bisim) (ttl stlsss1) (ttl (tls1_to_tls2 s2 stlsss1))))
 2. \<lbrakk>stlsss1 = TNil None; s1 -\<tau>1\<rightarrow> \<infinity>\<rbrakk> \<Longrightarrow> is_TNil stlsss1 = is_TNil (tls1_to_tls2 s2 stlsss1) \<and> (is_TNil stlsss1 \<longrightarrow> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> rel_option bisim (terminal stlsss1) (terminal (tls1_to_tls2 s2 stlsss1))) \<and> (\<not> is_TNil stlsss1 \<longrightarrow> \<not> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> (case thd stlsss1 of (tl1, s1'') \<Rightarrow> \<lambda>(tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (thd (tls1_to_tls2 s2 stlsss1)) \<and> ((\<exists>s1 s2 stlsss1. ttl stlsss1 = stlsss1 \<and> ttl (tls1_to_tls2 s2 stlsss1) = tls1_to_tls2 s2 stlsss1 \<and> trsys1.\<tau>Runs_table s1 stlsss1 \<and> s1 \<approx> s2) \<or> tllist_all2 (\<lambda>(tl1, s1'') (tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (rel_option bisim) (ttl stlsss1) (ttl (tls1_to_tls2 s2 stlsss1))))
 3. \<And>s' s'' tls tl. \<lbrakk>stlsss1 = TCons (tl, s'') tls; s1 -\<tau>1\<rightarrow>* s'; s' -1-tl\<rightarrow> s''; \<not> \<tau>move1 s' tl s''; trsys1.\<tau>Runs_table s'' tls\<rbrakk> \<Longrightarrow> is_TNil stlsss1 = is_TNil (tls1_to_tls2 s2 stlsss1) \<and> (is_TNil stlsss1 \<longrightarrow> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> rel_option bisim (terminal stlsss1) (terminal (tls1_to_tls2 s2 stlsss1))) \<and> (\<not> is_TNil stlsss1 \<longrightarrow> \<not> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> (case thd stlsss1 of (tl1, s1'') \<Rightarrow> \<lambda>(tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (thd (tls1_to_tls2 s2 stlsss1)) \<and> ((\<exists>s1 s2 stlsss1. ttl stlsss1 = stlsss1 \<and> ttl (tls1_to_tls2 s2 stlsss1) = tls1_to_tls2 s2 stlsss1 \<and> trsys1.\<tau>Runs_table s1 stlsss1 \<and> s1 \<approx> s2) \<or> tllist_all2 (\<lambda>(tl1, s1'') (tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (rel_option bisim) (ttl stlsss1) (ttl (tls1_to_tls2 s2 stlsss1))))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
s2 -\<tau>2\<rightarrow>* s2'
s1' \<approx> s2'

goal (3 subgoals):
 1. \<And>s'. \<lbrakk>stlsss1 = TNil \<lfloor>s'\<rfloor>; s1 -\<tau>1\<rightarrow>* s'; \<And>tl s''. \<not> s' -1-tl\<rightarrow> s''\<rbrakk> \<Longrightarrow> is_TNil stlsss1 = is_TNil (tls1_to_tls2 s2 stlsss1) \<and> (is_TNil stlsss1 \<longrightarrow> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> rel_option bisim (terminal stlsss1) (terminal (tls1_to_tls2 s2 stlsss1))) \<and> (\<not> is_TNil stlsss1 \<longrightarrow> \<not> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> (case thd stlsss1 of (tl1, s1'') \<Rightarrow> \<lambda>(tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (thd (tls1_to_tls2 s2 stlsss1)) \<and> ((\<exists>s1 s2 stlsss1. ttl stlsss1 = stlsss1 \<and> ttl (tls1_to_tls2 s2 stlsss1) = tls1_to_tls2 s2 stlsss1 \<and> trsys1.\<tau>Runs_table s1 stlsss1 \<and> s1 \<approx> s2) \<or> tllist_all2 (\<lambda>(tl1, s1'') (tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (rel_option bisim) (ttl stlsss1) (ttl (tls1_to_tls2 s2 stlsss1))))
 2. \<lbrakk>stlsss1 = TNil None; s1 -\<tau>1\<rightarrow> \<infinity>\<rbrakk> \<Longrightarrow> is_TNil stlsss1 = is_TNil (tls1_to_tls2 s2 stlsss1) \<and> (is_TNil stlsss1 \<longrightarrow> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> rel_option bisim (terminal stlsss1) (terminal (tls1_to_tls2 s2 stlsss1))) \<and> (\<not> is_TNil stlsss1 \<longrightarrow> \<not> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> (case thd stlsss1 of (tl1, s1'') \<Rightarrow> \<lambda>(tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (thd (tls1_to_tls2 s2 stlsss1)) \<and> ((\<exists>s1 s2 stlsss1. ttl stlsss1 = stlsss1 \<and> ttl (tls1_to_tls2 s2 stlsss1) = tls1_to_tls2 s2 stlsss1 \<and> trsys1.\<tau>Runs_table s1 stlsss1 \<and> s1 \<approx> s2) \<or> tllist_all2 (\<lambda>(tl1, s1'') (tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (rel_option bisim) (ttl stlsss1) (ttl (tls1_to_tls2 s2 stlsss1))))
 3. \<And>s' s'' tls tl. \<lbrakk>stlsss1 = TCons (tl, s'') tls; s1 -\<tau>1\<rightarrow>* s'; s' -1-tl\<rightarrow> s''; \<not> \<tau>move1 s' tl s''; trsys1.\<tau>Runs_table s'' tls\<rbrakk> \<Longrightarrow> is_TNil stlsss1 = is_TNil (tls1_to_tls2 s2 stlsss1) \<and> (is_TNil stlsss1 \<longrightarrow> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> rel_option bisim (terminal stlsss1) (terminal (tls1_to_tls2 s2 stlsss1))) \<and> (\<not> is_TNil stlsss1 \<longrightarrow> \<not> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> (case thd stlsss1 of (tl1, s1'') \<Rightarrow> \<lambda>(tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (thd (tls1_to_tls2 s2 stlsss1)) \<and> ((\<exists>s1 s2 stlsss1. ttl stlsss1 = stlsss1 \<and> ttl (tls1_to_tls2 s2 stlsss1) = tls1_to_tls2 s2 stlsss1 \<and> trsys1.\<tau>Runs_table s1 stlsss1 \<and> s1 \<approx> s2) \<or> tllist_all2 (\<lambda>(tl1, s1'') (tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (rel_option bisim) (ttl stlsss1) (ttl (tls1_to_tls2 s2 stlsss1))))
[PROOF STEP]
from no_move1_to_no_move2[OF \<open>s1' \<approx> s2'\<close> \<open>\<And>tl1 s1''. \<not> s1' -1-tl1\<rightarrow> s1''\<close>]
[PROOF STATE]
proof (chain)
picking this:
\<exists>s2'a. s2' -\<tau>2\<rightarrow>* s2'a \<and> (\<forall>tl2 s2''. \<not> s2'a -2-tl2\<rightarrow> s2'') \<and> s1' \<approx> s2'a
[PROOF STEP]
obtain s2'' where "s2' -\<tau>2\<rightarrow>* s2''" and "s1' \<approx> s2''"
        and "\<And>tl2 s2'''. \<not> s2'' -2-tl2\<rightarrow> s2'''"
[PROOF STATE]
proof (prove)
using this:
\<exists>s2'a. s2' -\<tau>2\<rightarrow>* s2'a \<and> (\<forall>tl2 s2''. \<not> s2'a -2-tl2\<rightarrow> s2'') \<and> s1' \<approx> s2'a

goal (1 subgoal):
 1. (\<And>s2''. \<lbrakk>s2' -\<tau>2\<rightarrow>* s2''; s1' \<approx> s2''; \<And>tl2 s2'''. \<not> s2'' -2-tl2\<rightarrow> s2'''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
s2' -\<tau>2\<rightarrow>* s2''
s1' \<approx> s2''
\<not> s2'' -2-?tl2.1\<rightarrow> ?s2'''1

goal (3 subgoals):
 1. \<And>s'. \<lbrakk>stlsss1 = TNil \<lfloor>s'\<rfloor>; s1 -\<tau>1\<rightarrow>* s'; \<And>tl s''. \<not> s' -1-tl\<rightarrow> s''\<rbrakk> \<Longrightarrow> is_TNil stlsss1 = is_TNil (tls1_to_tls2 s2 stlsss1) \<and> (is_TNil stlsss1 \<longrightarrow> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> rel_option bisim (terminal stlsss1) (terminal (tls1_to_tls2 s2 stlsss1))) \<and> (\<not> is_TNil stlsss1 \<longrightarrow> \<not> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> (case thd stlsss1 of (tl1, s1'') \<Rightarrow> \<lambda>(tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (thd (tls1_to_tls2 s2 stlsss1)) \<and> ((\<exists>s1 s2 stlsss1. ttl stlsss1 = stlsss1 \<and> ttl (tls1_to_tls2 s2 stlsss1) = tls1_to_tls2 s2 stlsss1 \<and> trsys1.\<tau>Runs_table s1 stlsss1 \<and> s1 \<approx> s2) \<or> tllist_all2 (\<lambda>(tl1, s1'') (tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (rel_option bisim) (ttl stlsss1) (ttl (tls1_to_tls2 s2 stlsss1))))
 2. \<lbrakk>stlsss1 = TNil None; s1 -\<tau>1\<rightarrow> \<infinity>\<rbrakk> \<Longrightarrow> is_TNil stlsss1 = is_TNil (tls1_to_tls2 s2 stlsss1) \<and> (is_TNil stlsss1 \<longrightarrow> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> rel_option bisim (terminal stlsss1) (terminal (tls1_to_tls2 s2 stlsss1))) \<and> (\<not> is_TNil stlsss1 \<longrightarrow> \<not> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> (case thd stlsss1 of (tl1, s1'') \<Rightarrow> \<lambda>(tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (thd (tls1_to_tls2 s2 stlsss1)) \<and> ((\<exists>s1 s2 stlsss1. ttl stlsss1 = stlsss1 \<and> ttl (tls1_to_tls2 s2 stlsss1) = tls1_to_tls2 s2 stlsss1 \<and> trsys1.\<tau>Runs_table s1 stlsss1 \<and> s1 \<approx> s2) \<or> tllist_all2 (\<lambda>(tl1, s1'') (tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (rel_option bisim) (ttl stlsss1) (ttl (tls1_to_tls2 s2 stlsss1))))
 3. \<And>s' s'' tls tl. \<lbrakk>stlsss1 = TCons (tl, s'') tls; s1 -\<tau>1\<rightarrow>* s'; s' -1-tl\<rightarrow> s''; \<not> \<tau>move1 s' tl s''; trsys1.\<tau>Runs_table s'' tls\<rbrakk> \<Longrightarrow> is_TNil stlsss1 = is_TNil (tls1_to_tls2 s2 stlsss1) \<and> (is_TNil stlsss1 \<longrightarrow> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> rel_option bisim (terminal stlsss1) (terminal (tls1_to_tls2 s2 stlsss1))) \<and> (\<not> is_TNil stlsss1 \<longrightarrow> \<not> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> (case thd stlsss1 of (tl1, s1'') \<Rightarrow> \<lambda>(tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (thd (tls1_to_tls2 s2 stlsss1)) \<and> ((\<exists>s1 s2 stlsss1. ttl stlsss1 = stlsss1 \<and> ttl (tls1_to_tls2 s2 stlsss1) = tls1_to_tls2 s2 stlsss1 \<and> trsys1.\<tau>Runs_table s1 stlsss1 \<and> s1 \<approx> s2) \<or> tllist_all2 (\<lambda>(tl1, s1'') (tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (rel_option bisim) (ttl stlsss1) (ttl (tls1_to_tls2 s2 stlsss1))))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
s2 -\<tau>2\<rightarrow>* s2'
s1' \<approx> s2'
s2' -\<tau>2\<rightarrow>* s2''
s1' \<approx> s2''
\<not> s2'' -2-?tl2.1\<rightarrow> ?s2'''1
[PROOF STEP]
have "?P s2''"
[PROOF STATE]
proof (prove)
using this:
s2 -\<tau>2\<rightarrow>* s2'
s1' \<approx> s2'
s2' -\<tau>2\<rightarrow>* s2''
s1' \<approx> s2''
\<not> s2'' -2-?tl2.1\<rightarrow> ?s2'''1

goal (1 subgoal):
 1. s2 -\<tau>2\<rightarrow>* s2'' \<and> (\<forall>tl2 s2''a. \<not> s2'' -2-tl2\<rightarrow> s2''a) \<and> s1' \<approx> s2''
[PROOF STEP]
by(blast intro: rtranclp_trans)
[PROOF STATE]
proof (state)
this:
s2 -\<tau>2\<rightarrow>* s2'' \<and> (\<forall>tl2 s2''a. \<not> s2'' -2-tl2\<rightarrow> s2''a) \<and> s1' \<approx> s2''

goal (3 subgoals):
 1. \<And>s'. \<lbrakk>stlsss1 = TNil \<lfloor>s'\<rfloor>; s1 -\<tau>1\<rightarrow>* s'; \<And>tl s''. \<not> s' -1-tl\<rightarrow> s''\<rbrakk> \<Longrightarrow> is_TNil stlsss1 = is_TNil (tls1_to_tls2 s2 stlsss1) \<and> (is_TNil stlsss1 \<longrightarrow> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> rel_option bisim (terminal stlsss1) (terminal (tls1_to_tls2 s2 stlsss1))) \<and> (\<not> is_TNil stlsss1 \<longrightarrow> \<not> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> (case thd stlsss1 of (tl1, s1'') \<Rightarrow> \<lambda>(tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (thd (tls1_to_tls2 s2 stlsss1)) \<and> ((\<exists>s1 s2 stlsss1. ttl stlsss1 = stlsss1 \<and> ttl (tls1_to_tls2 s2 stlsss1) = tls1_to_tls2 s2 stlsss1 \<and> trsys1.\<tau>Runs_table s1 stlsss1 \<and> s1 \<approx> s2) \<or> tllist_all2 (\<lambda>(tl1, s1'') (tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (rel_option bisim) (ttl stlsss1) (ttl (tls1_to_tls2 s2 stlsss1))))
 2. \<lbrakk>stlsss1 = TNil None; s1 -\<tau>1\<rightarrow> \<infinity>\<rbrakk> \<Longrightarrow> is_TNil stlsss1 = is_TNil (tls1_to_tls2 s2 stlsss1) \<and> (is_TNil stlsss1 \<longrightarrow> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> rel_option bisim (terminal stlsss1) (terminal (tls1_to_tls2 s2 stlsss1))) \<and> (\<not> is_TNil stlsss1 \<longrightarrow> \<not> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> (case thd stlsss1 of (tl1, s1'') \<Rightarrow> \<lambda>(tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (thd (tls1_to_tls2 s2 stlsss1)) \<and> ((\<exists>s1 s2 stlsss1. ttl stlsss1 = stlsss1 \<and> ttl (tls1_to_tls2 s2 stlsss1) = tls1_to_tls2 s2 stlsss1 \<and> trsys1.\<tau>Runs_table s1 stlsss1 \<and> s1 \<approx> s2) \<or> tllist_all2 (\<lambda>(tl1, s1'') (tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (rel_option bisim) (ttl stlsss1) (ttl (tls1_to_tls2 s2 stlsss1))))
 3. \<And>s' s'' tls tl. \<lbrakk>stlsss1 = TCons (tl, s'') tls; s1 -\<tau>1\<rightarrow>* s'; s' -1-tl\<rightarrow> s''; \<not> \<tau>move1 s' tl s''; trsys1.\<tau>Runs_table s'' tls\<rbrakk> \<Longrightarrow> is_TNil stlsss1 = is_TNil (tls1_to_tls2 s2 stlsss1) \<and> (is_TNil stlsss1 \<longrightarrow> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> rel_option bisim (terminal stlsss1) (terminal (tls1_to_tls2 s2 stlsss1))) \<and> (\<not> is_TNil stlsss1 \<longrightarrow> \<not> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> (case thd stlsss1 of (tl1, s1'') \<Rightarrow> \<lambda>(tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (thd (tls1_to_tls2 s2 stlsss1)) \<and> ((\<exists>s1 s2 stlsss1. ttl stlsss1 = stlsss1 \<and> ttl (tls1_to_tls2 s2 stlsss1) = tls1_to_tls2 s2 stlsss1 \<and> trsys1.\<tau>Runs_table s1 stlsss1 \<and> s1 \<approx> s2) \<or> tllist_all2 (\<lambda>(tl1, s1'') (tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (rel_option bisim) (ttl stlsss1) (ttl (tls1_to_tls2 s2 stlsss1))))
[PROOF STEP]
hence "?P (Eps ?P)"
[PROOF STATE]
proof (prove)
using this:
s2 -\<tau>2\<rightarrow>* s2'' \<and> (\<forall>tl2 s2''a. \<not> s2'' -2-tl2\<rightarrow> s2''a) \<and> s1' \<approx> s2''

goal (1 subgoal):
 1. s2 -\<tau>2\<rightarrow>* (SOME s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> (\<forall>tl2 s2''. \<not> s2' -2-tl2\<rightarrow> s2'') \<and> s1' \<approx> s2') \<and> (\<forall>tl2 s2''. \<not> (SOME s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> (\<forall>tl2 s2''. \<not> s2' -2-tl2\<rightarrow> s2'') \<and> s1' \<approx> s2') -2-tl2\<rightarrow> s2'') \<and> s1' \<approx> (SOME s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> (\<forall>tl2 s2''. \<not> s2' -2-tl2\<rightarrow> s2'') \<and> s1' \<approx> s2')
[PROOF STEP]
by(rule someI)
[PROOF STATE]
proof (state)
this:
s2 -\<tau>2\<rightarrow>* (SOME s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> (\<forall>tl2 s2''. \<not> s2' -2-tl2\<rightarrow> s2'') \<and> s1' \<approx> s2') \<and> (\<forall>tl2 s2''. \<not> (SOME s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> (\<forall>tl2 s2''. \<not> s2' -2-tl2\<rightarrow> s2'') \<and> s1' \<approx> s2') -2-tl2\<rightarrow> s2'') \<and> s1' \<approx> (SOME s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> (\<forall>tl2 s2''. \<not> s2' -2-tl2\<rightarrow> s2'') \<and> s1' \<approx> s2')

goal (3 subgoals):
 1. \<And>s'. \<lbrakk>stlsss1 = TNil \<lfloor>s'\<rfloor>; s1 -\<tau>1\<rightarrow>* s'; \<And>tl s''. \<not> s' -1-tl\<rightarrow> s''\<rbrakk> \<Longrightarrow> is_TNil stlsss1 = is_TNil (tls1_to_tls2 s2 stlsss1) \<and> (is_TNil stlsss1 \<longrightarrow> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> rel_option bisim (terminal stlsss1) (terminal (tls1_to_tls2 s2 stlsss1))) \<and> (\<not> is_TNil stlsss1 \<longrightarrow> \<not> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> (case thd stlsss1 of (tl1, s1'') \<Rightarrow> \<lambda>(tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (thd (tls1_to_tls2 s2 stlsss1)) \<and> ((\<exists>s1 s2 stlsss1. ttl stlsss1 = stlsss1 \<and> ttl (tls1_to_tls2 s2 stlsss1) = tls1_to_tls2 s2 stlsss1 \<and> trsys1.\<tau>Runs_table s1 stlsss1 \<and> s1 \<approx> s2) \<or> tllist_all2 (\<lambda>(tl1, s1'') (tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (rel_option bisim) (ttl stlsss1) (ttl (tls1_to_tls2 s2 stlsss1))))
 2. \<lbrakk>stlsss1 = TNil None; s1 -\<tau>1\<rightarrow> \<infinity>\<rbrakk> \<Longrightarrow> is_TNil stlsss1 = is_TNil (tls1_to_tls2 s2 stlsss1) \<and> (is_TNil stlsss1 \<longrightarrow> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> rel_option bisim (terminal stlsss1) (terminal (tls1_to_tls2 s2 stlsss1))) \<and> (\<not> is_TNil stlsss1 \<longrightarrow> \<not> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> (case thd stlsss1 of (tl1, s1'') \<Rightarrow> \<lambda>(tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (thd (tls1_to_tls2 s2 stlsss1)) \<and> ((\<exists>s1 s2 stlsss1. ttl stlsss1 = stlsss1 \<and> ttl (tls1_to_tls2 s2 stlsss1) = tls1_to_tls2 s2 stlsss1 \<and> trsys1.\<tau>Runs_table s1 stlsss1 \<and> s1 \<approx> s2) \<or> tllist_all2 (\<lambda>(tl1, s1'') (tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (rel_option bisim) (ttl stlsss1) (ttl (tls1_to_tls2 s2 stlsss1))))
 3. \<And>s' s'' tls tl. \<lbrakk>stlsss1 = TCons (tl, s'') tls; s1 -\<tau>1\<rightarrow>* s'; s' -1-tl\<rightarrow> s''; \<not> \<tau>move1 s' tl s''; trsys1.\<tau>Runs_table s'' tls\<rbrakk> \<Longrightarrow> is_TNil stlsss1 = is_TNil (tls1_to_tls2 s2 stlsss1) \<and> (is_TNil stlsss1 \<longrightarrow> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> rel_option bisim (terminal stlsss1) (terminal (tls1_to_tls2 s2 stlsss1))) \<and> (\<not> is_TNil stlsss1 \<longrightarrow> \<not> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> (case thd stlsss1 of (tl1, s1'') \<Rightarrow> \<lambda>(tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (thd (tls1_to_tls2 s2 stlsss1)) \<and> ((\<exists>s1 s2 stlsss1. ttl stlsss1 = stlsss1 \<and> ttl (tls1_to_tls2 s2 stlsss1) = tls1_to_tls2 s2 stlsss1 \<and> trsys1.\<tau>Runs_table s1 stlsss1 \<and> s1 \<approx> s2) \<or> tllist_all2 (\<lambda>(tl1, s1'') (tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (rel_option bisim) (ttl stlsss1) (ttl (tls1_to_tls2 s2 stlsss1))))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
s2 -\<tau>2\<rightarrow>* (SOME s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> (\<forall>tl2 s2''. \<not> s2' -2-tl2\<rightarrow> s2'') \<and> s1' \<approx> s2') \<and> (\<forall>tl2 s2''. \<not> (SOME s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> (\<forall>tl2 s2''. \<not> s2' -2-tl2\<rightarrow> s2'') \<and> s1' \<approx> s2') -2-tl2\<rightarrow> s2'') \<and> s1' \<approx> (SOME s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> (\<forall>tl2 s2''. \<not> s2' -2-tl2\<rightarrow> s2'') \<and> s1' \<approx> s2')

goal (1 subgoal):
 1. is_TNil stlsss1 = is_TNil (tls1_to_tls2 s2 stlsss1) \<and> (is_TNil stlsss1 \<longrightarrow> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> rel_option bisim (terminal stlsss1) (terminal (tls1_to_tls2 s2 stlsss1))) \<and> (\<not> is_TNil stlsss1 \<longrightarrow> \<not> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> (case thd stlsss1 of (tl1, s1'') \<Rightarrow> \<lambda>(tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (thd (tls1_to_tls2 s2 stlsss1)) \<and> ((\<exists>s1 s2 stlsss1. ttl stlsss1 = stlsss1 \<and> ttl (tls1_to_tls2 s2 stlsss1) = tls1_to_tls2 s2 stlsss1 \<and> trsys1.\<tau>Runs_table s1 stlsss1 \<and> s1 \<approx> s2) \<or> tllist_all2 (\<lambda>(tl1, s1'') (tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (rel_option bisim) (ttl stlsss1) (ttl (tls1_to_tls2 s2 stlsss1))))
[PROOF STEP]
using \<open>stlsss1 = TNil \<lfloor>s1'\<rfloor>\<close> bisim
[PROOF STATE]
proof (prove)
using this:
s2 -\<tau>2\<rightarrow>* (SOME s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> (\<forall>tl2 s2''. \<not> s2' -2-tl2\<rightarrow> s2'') \<and> s1' \<approx> s2') \<and> (\<forall>tl2 s2''. \<not> (SOME s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> (\<forall>tl2 s2''. \<not> s2' -2-tl2\<rightarrow> s2'') \<and> s1' \<approx> s2') -2-tl2\<rightarrow> s2'') \<and> s1' \<approx> (SOME s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> (\<forall>tl2 s2''. \<not> s2' -2-tl2\<rightarrow> s2'') \<and> s1' \<approx> s2')
stlsss1 = TNil \<lfloor>s1'\<rfloor>
s1 \<approx> s2

goal (1 subgoal):
 1. is_TNil stlsss1 = is_TNil (tls1_to_tls2 s2 stlsss1) \<and> (is_TNil stlsss1 \<longrightarrow> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> rel_option bisim (terminal stlsss1) (terminal (tls1_to_tls2 s2 stlsss1))) \<and> (\<not> is_TNil stlsss1 \<longrightarrow> \<not> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> (case thd stlsss1 of (tl1, s1'') \<Rightarrow> \<lambda>(tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (thd (tls1_to_tls2 s2 stlsss1)) \<and> ((\<exists>s1 s2 stlsss1. ttl stlsss1 = stlsss1 \<and> ttl (tls1_to_tls2 s2 stlsss1) = tls1_to_tls2 s2 stlsss1 \<and> trsys1.\<tau>Runs_table s1 stlsss1 \<and> s1 \<approx> s2) \<or> tllist_all2 (\<lambda>(tl1, s1'') (tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (rel_option bisim) (ttl stlsss1) (ttl (tls1_to_tls2 s2 stlsss1))))
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
is_TNil stlsss1 = is_TNil (tls1_to_tls2 s2 stlsss1) \<and> (is_TNil stlsss1 \<longrightarrow> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> rel_option bisim (terminal stlsss1) (terminal (tls1_to_tls2 s2 stlsss1))) \<and> (\<not> is_TNil stlsss1 \<longrightarrow> \<not> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> (case thd stlsss1 of (tl1, s1'') \<Rightarrow> \<lambda>(tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (thd (tls1_to_tls2 s2 stlsss1)) \<and> ((\<exists>s1 s2 stlsss1. ttl stlsss1 = stlsss1 \<and> ttl (tls1_to_tls2 s2 stlsss1) = tls1_to_tls2 s2 stlsss1 \<and> trsys1.\<tau>Runs_table s1 stlsss1 \<and> s1 \<approx> s2) \<or> tllist_all2 (\<lambda>(tl1, s1'') (tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (rel_option bisim) (ttl stlsss1) (ttl (tls1_to_tls2 s2 stlsss1))))

goal (2 subgoals):
 1. \<lbrakk>stlsss1 = TNil None; s1 -\<tau>1\<rightarrow> \<infinity>\<rbrakk> \<Longrightarrow> is_TNil stlsss1 = is_TNil (tls1_to_tls2 s2 stlsss1) \<and> (is_TNil stlsss1 \<longrightarrow> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> rel_option bisim (terminal stlsss1) (terminal (tls1_to_tls2 s2 stlsss1))) \<and> (\<not> is_TNil stlsss1 \<longrightarrow> \<not> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> (case thd stlsss1 of (tl1, s1'') \<Rightarrow> \<lambda>(tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (thd (tls1_to_tls2 s2 stlsss1)) \<and> ((\<exists>s1 s2 stlsss1. ttl stlsss1 = stlsss1 \<and> ttl (tls1_to_tls2 s2 stlsss1) = tls1_to_tls2 s2 stlsss1 \<and> trsys1.\<tau>Runs_table s1 stlsss1 \<and> s1 \<approx> s2) \<or> tllist_all2 (\<lambda>(tl1, s1'') (tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (rel_option bisim) (ttl stlsss1) (ttl (tls1_to_tls2 s2 stlsss1))))
 2. \<And>s' s'' tls tl. \<lbrakk>stlsss1 = TCons (tl, s'') tls; s1 -\<tau>1\<rightarrow>* s'; s' -1-tl\<rightarrow> s''; \<not> \<tau>move1 s' tl s''; trsys1.\<tau>Runs_table s'' tls\<rbrakk> \<Longrightarrow> is_TNil stlsss1 = is_TNil (tls1_to_tls2 s2 stlsss1) \<and> (is_TNil stlsss1 \<longrightarrow> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> rel_option bisim (terminal stlsss1) (terminal (tls1_to_tls2 s2 stlsss1))) \<and> (\<not> is_TNil stlsss1 \<longrightarrow> \<not> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> (case thd stlsss1 of (tl1, s1'') \<Rightarrow> \<lambda>(tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (thd (tls1_to_tls2 s2 stlsss1)) \<and> ((\<exists>s1 s2 stlsss1. ttl stlsss1 = stlsss1 \<and> ttl (tls1_to_tls2 s2 stlsss1) = tls1_to_tls2 s2 stlsss1 \<and> trsys1.\<tau>Runs_table s1 stlsss1 \<and> s1 \<approx> s2) \<or> tllist_all2 (\<lambda>(tl1, s1'') (tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (rel_option bisim) (ttl stlsss1) (ttl (tls1_to_tls2 s2 stlsss1))))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>stlsss1 = TNil None; s1 -\<tau>1\<rightarrow> \<infinity>\<rbrakk> \<Longrightarrow> is_TNil stlsss1 = is_TNil (tls1_to_tls2 s2 stlsss1) \<and> (is_TNil stlsss1 \<longrightarrow> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> rel_option bisim (terminal stlsss1) (terminal (tls1_to_tls2 s2 stlsss1))) \<and> (\<not> is_TNil stlsss1 \<longrightarrow> \<not> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> (case thd stlsss1 of (tl1, s1'') \<Rightarrow> \<lambda>(tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (thd (tls1_to_tls2 s2 stlsss1)) \<and> ((\<exists>s1 s2 stlsss1. ttl stlsss1 = stlsss1 \<and> ttl (tls1_to_tls2 s2 stlsss1) = tls1_to_tls2 s2 stlsss1 \<and> trsys1.\<tau>Runs_table s1 stlsss1 \<and> s1 \<approx> s2) \<or> tllist_all2 (\<lambda>(tl1, s1'') (tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (rel_option bisim) (ttl stlsss1) (ttl (tls1_to_tls2 s2 stlsss1))))
 2. \<And>s' s'' tls tl. \<lbrakk>stlsss1 = TCons (tl, s'') tls; s1 -\<tau>1\<rightarrow>* s'; s' -1-tl\<rightarrow> s''; \<not> \<tau>move1 s' tl s''; trsys1.\<tau>Runs_table s'' tls\<rbrakk> \<Longrightarrow> is_TNil stlsss1 = is_TNil (tls1_to_tls2 s2 stlsss1) \<and> (is_TNil stlsss1 \<longrightarrow> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> rel_option bisim (terminal stlsss1) (terminal (tls1_to_tls2 s2 stlsss1))) \<and> (\<not> is_TNil stlsss1 \<longrightarrow> \<not> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> (case thd stlsss1 of (tl1, s1'') \<Rightarrow> \<lambda>(tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (thd (tls1_to_tls2 s2 stlsss1)) \<and> ((\<exists>s1 s2 stlsss1. ttl stlsss1 = stlsss1 \<and> ttl (tls1_to_tls2 s2 stlsss1) = tls1_to_tls2 s2 stlsss1 \<and> trsys1.\<tau>Runs_table s1 stlsss1 \<and> s1 \<approx> s2) \<or> tllist_all2 (\<lambda>(tl1, s1'') (tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (rel_option bisim) (ttl stlsss1) (ttl (tls1_to_tls2 s2 stlsss1))))
[PROOF STEP]
case (Proceed s1' s1'' stlsss1' tl1)
[PROOF STATE]
proof (state)
this:
stlsss1 = TCons (tl1, s1'') stlsss1'
s1 -\<tau>1\<rightarrow>* s1'
s1' -1-tl1\<rightarrow> s1''
\<not> \<tau>move1 s1' tl1 s1''
trsys1.\<tau>Runs_table s1'' stlsss1'

goal (2 subgoals):
 1. \<lbrakk>stlsss1 = TNil None; s1 -\<tau>1\<rightarrow> \<infinity>\<rbrakk> \<Longrightarrow> is_TNil stlsss1 = is_TNil (tls1_to_tls2 s2 stlsss1) \<and> (is_TNil stlsss1 \<longrightarrow> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> rel_option bisim (terminal stlsss1) (terminal (tls1_to_tls2 s2 stlsss1))) \<and> (\<not> is_TNil stlsss1 \<longrightarrow> \<not> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> (case thd stlsss1 of (tl1, s1'') \<Rightarrow> \<lambda>(tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (thd (tls1_to_tls2 s2 stlsss1)) \<and> ((\<exists>s1 s2 stlsss1. ttl stlsss1 = stlsss1 \<and> ttl (tls1_to_tls2 s2 stlsss1) = tls1_to_tls2 s2 stlsss1 \<and> trsys1.\<tau>Runs_table s1 stlsss1 \<and> s1 \<approx> s2) \<or> tllist_all2 (\<lambda>(tl1, s1'') (tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (rel_option bisim) (ttl stlsss1) (ttl (tls1_to_tls2 s2 stlsss1))))
 2. \<And>s' s'' tls tl. \<lbrakk>stlsss1 = TCons (tl, s'') tls; s1 -\<tau>1\<rightarrow>* s'; s' -1-tl\<rightarrow> s''; \<not> \<tau>move1 s' tl s''; trsys1.\<tau>Runs_table s'' tls\<rbrakk> \<Longrightarrow> is_TNil stlsss1 = is_TNil (tls1_to_tls2 s2 stlsss1) \<and> (is_TNil stlsss1 \<longrightarrow> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> rel_option bisim (terminal stlsss1) (terminal (tls1_to_tls2 s2 stlsss1))) \<and> (\<not> is_TNil stlsss1 \<longrightarrow> \<not> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> (case thd stlsss1 of (tl1, s1'') \<Rightarrow> \<lambda>(tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (thd (tls1_to_tls2 s2 stlsss1)) \<and> ((\<exists>s1 s2 stlsss1. ttl stlsss1 = stlsss1 \<and> ttl (tls1_to_tls2 s2 stlsss1) = tls1_to_tls2 s2 stlsss1 \<and> trsys1.\<tau>Runs_table s1 stlsss1 \<and> s1 \<approx> s2) \<or> tllist_all2 (\<lambda>(tl1, s1'') (tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (rel_option bisim) (ttl stlsss1) (ttl (tls1_to_tls2 s2 stlsss1))))
[PROOF STEP]
from simulation_silents1[OF bisim \<open>s1 -\<tau>1\<rightarrow>* s1'\<close>]
[PROOF STATE]
proof (chain)
picking this:
\<exists>s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> s1' \<approx> s2'
[PROOF STEP]
obtain s2' where "s2 -\<tau>2\<rightarrow>* s2'" and "s1' \<approx> s2'"
[PROOF STATE]
proof (prove)
using this:
\<exists>s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> s1' \<approx> s2'

goal (1 subgoal):
 1. (\<And>s2'. \<lbrakk>s2 -\<tau>2\<rightarrow>* s2'; s1' \<approx> s2'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
s2 -\<tau>2\<rightarrow>* s2'
s1' \<approx> s2'

goal (2 subgoals):
 1. \<lbrakk>stlsss1 = TNil None; s1 -\<tau>1\<rightarrow> \<infinity>\<rbrakk> \<Longrightarrow> is_TNil stlsss1 = is_TNil (tls1_to_tls2 s2 stlsss1) \<and> (is_TNil stlsss1 \<longrightarrow> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> rel_option bisim (terminal stlsss1) (terminal (tls1_to_tls2 s2 stlsss1))) \<and> (\<not> is_TNil stlsss1 \<longrightarrow> \<not> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> (case thd stlsss1 of (tl1, s1'') \<Rightarrow> \<lambda>(tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (thd (tls1_to_tls2 s2 stlsss1)) \<and> ((\<exists>s1 s2 stlsss1. ttl stlsss1 = stlsss1 \<and> ttl (tls1_to_tls2 s2 stlsss1) = tls1_to_tls2 s2 stlsss1 \<and> trsys1.\<tau>Runs_table s1 stlsss1 \<and> s1 \<approx> s2) \<or> tllist_all2 (\<lambda>(tl1, s1'') (tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (rel_option bisim) (ttl stlsss1) (ttl (tls1_to_tls2 s2 stlsss1))))
 2. \<And>s' s'' tls tl. \<lbrakk>stlsss1 = TCons (tl, s'') tls; s1 -\<tau>1\<rightarrow>* s'; s' -1-tl\<rightarrow> s''; \<not> \<tau>move1 s' tl s''; trsys1.\<tau>Runs_table s'' tls\<rbrakk> \<Longrightarrow> is_TNil stlsss1 = is_TNil (tls1_to_tls2 s2 stlsss1) \<and> (is_TNil stlsss1 \<longrightarrow> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> rel_option bisim (terminal stlsss1) (terminal (tls1_to_tls2 s2 stlsss1))) \<and> (\<not> is_TNil stlsss1 \<longrightarrow> \<not> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> (case thd stlsss1 of (tl1, s1'') \<Rightarrow> \<lambda>(tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (thd (tls1_to_tls2 s2 stlsss1)) \<and> ((\<exists>s1 s2 stlsss1. ttl stlsss1 = stlsss1 \<and> ttl (tls1_to_tls2 s2 stlsss1) = tls1_to_tls2 s2 stlsss1 \<and> trsys1.\<tau>Runs_table s1 stlsss1 \<and> s1 \<approx> s2) \<or> tllist_all2 (\<lambda>(tl1, s1'') (tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (rel_option bisim) (ttl stlsss1) (ttl (tls1_to_tls2 s2 stlsss1))))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
s2 -\<tau>2\<rightarrow>* s2'
s1' \<approx> s2'

goal (2 subgoals):
 1. \<lbrakk>stlsss1 = TNil None; s1 -\<tau>1\<rightarrow> \<infinity>\<rbrakk> \<Longrightarrow> is_TNil stlsss1 = is_TNil (tls1_to_tls2 s2 stlsss1) \<and> (is_TNil stlsss1 \<longrightarrow> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> rel_option bisim (terminal stlsss1) (terminal (tls1_to_tls2 s2 stlsss1))) \<and> (\<not> is_TNil stlsss1 \<longrightarrow> \<not> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> (case thd stlsss1 of (tl1, s1'') \<Rightarrow> \<lambda>(tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (thd (tls1_to_tls2 s2 stlsss1)) \<and> ((\<exists>s1 s2 stlsss1. ttl stlsss1 = stlsss1 \<and> ttl (tls1_to_tls2 s2 stlsss1) = tls1_to_tls2 s2 stlsss1 \<and> trsys1.\<tau>Runs_table s1 stlsss1 \<and> s1 \<approx> s2) \<or> tllist_all2 (\<lambda>(tl1, s1'') (tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (rel_option bisim) (ttl stlsss1) (ttl (tls1_to_tls2 s2 stlsss1))))
 2. \<And>s' s'' tls tl. \<lbrakk>stlsss1 = TCons (tl, s'') tls; s1 -\<tau>1\<rightarrow>* s'; s' -1-tl\<rightarrow> s''; \<not> \<tau>move1 s' tl s''; trsys1.\<tau>Runs_table s'' tls\<rbrakk> \<Longrightarrow> is_TNil stlsss1 = is_TNil (tls1_to_tls2 s2 stlsss1) \<and> (is_TNil stlsss1 \<longrightarrow> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> rel_option bisim (terminal stlsss1) (terminal (tls1_to_tls2 s2 stlsss1))) \<and> (\<not> is_TNil stlsss1 \<longrightarrow> \<not> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> (case thd stlsss1 of (tl1, s1'') \<Rightarrow> \<lambda>(tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (thd (tls1_to_tls2 s2 stlsss1)) \<and> ((\<exists>s1 s2 stlsss1. ttl stlsss1 = stlsss1 \<and> ttl (tls1_to_tls2 s2 stlsss1) = tls1_to_tls2 s2 stlsss1 \<and> trsys1.\<tau>Runs_table s1 stlsss1 \<and> s1 \<approx> s2) \<or> tllist_all2 (\<lambda>(tl1, s1'') (tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (rel_option bisim) (ttl stlsss1) (ttl (tls1_to_tls2 s2 stlsss1))))
[PROOF STEP]
from simulation1[OF \<open>s1' \<approx> s2'\<close> \<open>s1' -1-tl1\<rightarrow> s1''\<close> \<open>\<not> \<tau>move1 s1' tl1 s1''\<close>]
[PROOF STATE]
proof (chain)
picking this:
\<exists>s2'a s2'' tl2. s2' -\<tau>2\<rightarrow>* s2'a \<and> s2'a -2-tl2\<rightarrow> s2'' \<and> \<not> \<tau>move2 s2'a tl2 s2'' \<and> s1'' \<approx> s2'' \<and> tl1 \<sim> tl2
[PROOF STEP]
obtain s2'' s2''' tl2 where "s2' -\<tau>2\<rightarrow>* s2''"
        and "s2'' -2-tl2\<rightarrow> s2'''" and "\<not> \<tau>move2 s2'' tl2 s2'''"
        and "s1'' \<approx> s2'''" and "tl1 \<sim> tl2"
[PROOF STATE]
proof (prove)
using this:
\<exists>s2'a s2'' tl2. s2' -\<tau>2\<rightarrow>* s2'a \<and> s2'a -2-tl2\<rightarrow> s2'' \<and> \<not> \<tau>move2 s2'a tl2 s2'' \<and> s1'' \<approx> s2'' \<and> tl1 \<sim> tl2

goal (1 subgoal):
 1. (\<And>s2'' tl2 s2'''. \<lbrakk>s2' -\<tau>2\<rightarrow>* s2''; s2'' -2-tl2\<rightarrow> s2'''; \<not> \<tau>move2 s2'' tl2 s2'''; s1'' \<approx> s2'''; tl1 \<sim> tl2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
s2' -\<tau>2\<rightarrow>* s2''
s2'' -2-tl2\<rightarrow> s2'''
\<not> \<tau>move2 s2'' tl2 s2'''
s1'' \<approx> s2'''
tl1 \<sim> tl2

goal (2 subgoals):
 1. \<lbrakk>stlsss1 = TNil None; s1 -\<tau>1\<rightarrow> \<infinity>\<rbrakk> \<Longrightarrow> is_TNil stlsss1 = is_TNil (tls1_to_tls2 s2 stlsss1) \<and> (is_TNil stlsss1 \<longrightarrow> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> rel_option bisim (terminal stlsss1) (terminal (tls1_to_tls2 s2 stlsss1))) \<and> (\<not> is_TNil stlsss1 \<longrightarrow> \<not> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> (case thd stlsss1 of (tl1, s1'') \<Rightarrow> \<lambda>(tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (thd (tls1_to_tls2 s2 stlsss1)) \<and> ((\<exists>s1 s2 stlsss1. ttl stlsss1 = stlsss1 \<and> ttl (tls1_to_tls2 s2 stlsss1) = tls1_to_tls2 s2 stlsss1 \<and> trsys1.\<tau>Runs_table s1 stlsss1 \<and> s1 \<approx> s2) \<or> tllist_all2 (\<lambda>(tl1, s1'') (tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (rel_option bisim) (ttl stlsss1) (ttl (tls1_to_tls2 s2 stlsss1))))
 2. \<And>s' s'' tls tl. \<lbrakk>stlsss1 = TCons (tl, s'') tls; s1 -\<tau>1\<rightarrow>* s'; s' -1-tl\<rightarrow> s''; \<not> \<tau>move1 s' tl s''; trsys1.\<tau>Runs_table s'' tls\<rbrakk> \<Longrightarrow> is_TNil stlsss1 = is_TNil (tls1_to_tls2 s2 stlsss1) \<and> (is_TNil stlsss1 \<longrightarrow> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> rel_option bisim (terminal stlsss1) (terminal (tls1_to_tls2 s2 stlsss1))) \<and> (\<not> is_TNil stlsss1 \<longrightarrow> \<not> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> (case thd stlsss1 of (tl1, s1'') \<Rightarrow> \<lambda>(tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (thd (tls1_to_tls2 s2 stlsss1)) \<and> ((\<exists>s1 s2 stlsss1. ttl stlsss1 = stlsss1 \<and> ttl (tls1_to_tls2 s2 stlsss1) = tls1_to_tls2 s2 stlsss1 \<and> trsys1.\<tau>Runs_table s1 stlsss1 \<and> s1 \<approx> s2) \<or> tllist_all2 (\<lambda>(tl1, s1'') (tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (rel_option bisim) (ttl stlsss1) (ttl (tls1_to_tls2 s2 stlsss1))))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
s2 -\<tau>2\<rightarrow>* s2'
s1' \<approx> s2'
s2' -\<tau>2\<rightarrow>* s2''
s2'' -2-tl2\<rightarrow> s2'''
\<not> \<tau>move2 s2'' tl2 s2'''
s1'' \<approx> s2'''
tl1 \<sim> tl2
[PROOF STEP]
have "?P s2 stlsss1 (tl2, s2''')"
[PROOF STATE]
proof (prove)
using this:
s2 -\<tau>2\<rightarrow>* s2'
s1' \<approx> s2'
s2' -\<tau>2\<rightarrow>* s2''
s2'' -2-tl2\<rightarrow> s2'''
\<not> \<tau>move2 s2'' tl2 s2'''
s1'' \<approx> s2'''
tl1 \<sim> tl2

goal (1 subgoal):
 1. case (tl2, s2''') of (tl2, s2'') \<Rightarrow> \<exists>s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> s2' -2-tl2\<rightarrow> s2'' \<and> \<not> \<tau>move2 s2' tl2 s2'' \<and> snd (thd stlsss1) \<approx> s2'' \<and> fst (thd stlsss1) \<sim> tl2
[PROOF STEP]
using \<open>stlsss1 = TCons (tl1, s1'') stlsss1'\<close>
[PROOF STATE]
proof (prove)
using this:
s2 -\<tau>2\<rightarrow>* s2'
s1' \<approx> s2'
s2' -\<tau>2\<rightarrow>* s2''
s2'' -2-tl2\<rightarrow> s2'''
\<not> \<tau>move2 s2'' tl2 s2'''
s1'' \<approx> s2'''
tl1 \<sim> tl2
stlsss1 = TCons (tl1, s1'') stlsss1'

goal (1 subgoal):
 1. case (tl2, s2''') of (tl2, s2'') \<Rightarrow> \<exists>s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> s2' -2-tl2\<rightarrow> s2'' \<and> \<not> \<tau>move2 s2' tl2 s2'' \<and> snd (thd stlsss1) \<approx> s2'' \<and> fst (thd stlsss1) \<sim> tl2
[PROOF STEP]
by(auto intro: rtranclp_trans)
[PROOF STATE]
proof (state)
this:
case (tl2, s2''') of (tl2, s2'') \<Rightarrow> \<exists>s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> s2' -2-tl2\<rightarrow> s2'' \<and> \<not> \<tau>move2 s2' tl2 s2'' \<and> snd (thd stlsss1) \<approx> s2'' \<and> fst (thd stlsss1) \<sim> tl2

goal (2 subgoals):
 1. \<lbrakk>stlsss1 = TNil None; s1 -\<tau>1\<rightarrow> \<infinity>\<rbrakk> \<Longrightarrow> is_TNil stlsss1 = is_TNil (tls1_to_tls2 s2 stlsss1) \<and> (is_TNil stlsss1 \<longrightarrow> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> rel_option bisim (terminal stlsss1) (terminal (tls1_to_tls2 s2 stlsss1))) \<and> (\<not> is_TNil stlsss1 \<longrightarrow> \<not> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> (case thd stlsss1 of (tl1, s1'') \<Rightarrow> \<lambda>(tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (thd (tls1_to_tls2 s2 stlsss1)) \<and> ((\<exists>s1 s2 stlsss1. ttl stlsss1 = stlsss1 \<and> ttl (tls1_to_tls2 s2 stlsss1) = tls1_to_tls2 s2 stlsss1 \<and> trsys1.\<tau>Runs_table s1 stlsss1 \<and> s1 \<approx> s2) \<or> tllist_all2 (\<lambda>(tl1, s1'') (tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (rel_option bisim) (ttl stlsss1) (ttl (tls1_to_tls2 s2 stlsss1))))
 2. \<And>s' s'' tls tl. \<lbrakk>stlsss1 = TCons (tl, s'') tls; s1 -\<tau>1\<rightarrow>* s'; s' -1-tl\<rightarrow> s''; \<not> \<tau>move1 s' tl s''; trsys1.\<tau>Runs_table s'' tls\<rbrakk> \<Longrightarrow> is_TNil stlsss1 = is_TNil (tls1_to_tls2 s2 stlsss1) \<and> (is_TNil stlsss1 \<longrightarrow> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> rel_option bisim (terminal stlsss1) (terminal (tls1_to_tls2 s2 stlsss1))) \<and> (\<not> is_TNil stlsss1 \<longrightarrow> \<not> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> (case thd stlsss1 of (tl1, s1'') \<Rightarrow> \<lambda>(tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (thd (tls1_to_tls2 s2 stlsss1)) \<and> ((\<exists>s1 s2 stlsss1. ttl stlsss1 = stlsss1 \<and> ttl (tls1_to_tls2 s2 stlsss1) = tls1_to_tls2 s2 stlsss1 \<and> trsys1.\<tau>Runs_table s1 stlsss1 \<and> s1 \<approx> s2) \<or> tllist_all2 (\<lambda>(tl1, s1'') (tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (rel_option bisim) (ttl stlsss1) (ttl (tls1_to_tls2 s2 stlsss1))))
[PROOF STEP]
hence "?P s2 stlsss1 (Eps (?P s2 stlsss1))"
[PROOF STATE]
proof (prove)
using this:
case (tl2, s2''') of (tl2, s2'') \<Rightarrow> \<exists>s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> s2' -2-tl2\<rightarrow> s2'' \<and> \<not> \<tau>move2 s2' tl2 s2'' \<and> snd (thd stlsss1) \<approx> s2'' \<and> fst (thd stlsss1) \<sim> tl2

goal (1 subgoal):
 1. case SOME (tl2, s2''). \<exists>s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> s2' -2-tl2\<rightarrow> s2'' \<and> \<not> \<tau>move2 s2' tl2 s2'' \<and> snd (thd stlsss1) \<approx> s2'' \<and> fst (thd stlsss1) \<sim> tl2 of (tl2, s2'') \<Rightarrow> \<exists>s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> s2' -2-tl2\<rightarrow> s2'' \<and> \<not> \<tau>move2 s2' tl2 s2'' \<and> snd (thd stlsss1) \<approx> s2'' \<and> fst (thd stlsss1) \<sim> tl2
[PROOF STEP]
by(rule someI)
[PROOF STATE]
proof (state)
this:
case SOME (tl2, s2''). \<exists>s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> s2' -2-tl2\<rightarrow> s2'' \<and> \<not> \<tau>move2 s2' tl2 s2'' \<and> snd (thd stlsss1) \<approx> s2'' \<and> fst (thd stlsss1) \<sim> tl2 of (tl2, s2'') \<Rightarrow> \<exists>s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> s2' -2-tl2\<rightarrow> s2'' \<and> \<not> \<tau>move2 s2' tl2 s2'' \<and> snd (thd stlsss1) \<approx> s2'' \<and> fst (thd stlsss1) \<sim> tl2

goal (2 subgoals):
 1. \<lbrakk>stlsss1 = TNil None; s1 -\<tau>1\<rightarrow> \<infinity>\<rbrakk> \<Longrightarrow> is_TNil stlsss1 = is_TNil (tls1_to_tls2 s2 stlsss1) \<and> (is_TNil stlsss1 \<longrightarrow> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> rel_option bisim (terminal stlsss1) (terminal (tls1_to_tls2 s2 stlsss1))) \<and> (\<not> is_TNil stlsss1 \<longrightarrow> \<not> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> (case thd stlsss1 of (tl1, s1'') \<Rightarrow> \<lambda>(tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (thd (tls1_to_tls2 s2 stlsss1)) \<and> ((\<exists>s1 s2 stlsss1. ttl stlsss1 = stlsss1 \<and> ttl (tls1_to_tls2 s2 stlsss1) = tls1_to_tls2 s2 stlsss1 \<and> trsys1.\<tau>Runs_table s1 stlsss1 \<and> s1 \<approx> s2) \<or> tllist_all2 (\<lambda>(tl1, s1'') (tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (rel_option bisim) (ttl stlsss1) (ttl (tls1_to_tls2 s2 stlsss1))))
 2. \<And>s' s'' tls tl. \<lbrakk>stlsss1 = TCons (tl, s'') tls; s1 -\<tau>1\<rightarrow>* s'; s' -1-tl\<rightarrow> s''; \<not> \<tau>move1 s' tl s''; trsys1.\<tau>Runs_table s'' tls\<rbrakk> \<Longrightarrow> is_TNil stlsss1 = is_TNil (tls1_to_tls2 s2 stlsss1) \<and> (is_TNil stlsss1 \<longrightarrow> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> rel_option bisim (terminal stlsss1) (terminal (tls1_to_tls2 s2 stlsss1))) \<and> (\<not> is_TNil stlsss1 \<longrightarrow> \<not> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> (case thd stlsss1 of (tl1, s1'') \<Rightarrow> \<lambda>(tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (thd (tls1_to_tls2 s2 stlsss1)) \<and> ((\<exists>s1 s2 stlsss1. ttl stlsss1 = stlsss1 \<and> ttl (tls1_to_tls2 s2 stlsss1) = tls1_to_tls2 s2 stlsss1 \<and> trsys1.\<tau>Runs_table s1 stlsss1 \<and> s1 \<approx> s2) \<or> tllist_all2 (\<lambda>(tl1, s1'') (tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (rel_option bisim) (ttl stlsss1) (ttl (tls1_to_tls2 s2 stlsss1))))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
case SOME (tl2, s2''). \<exists>s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> s2' -2-tl2\<rightarrow> s2'' \<and> \<not> \<tau>move2 s2' tl2 s2'' \<and> snd (thd stlsss1) \<approx> s2'' \<and> fst (thd stlsss1) \<sim> tl2 of (tl2, s2'') \<Rightarrow> \<exists>s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> s2' -2-tl2\<rightarrow> s2'' \<and> \<not> \<tau>move2 s2' tl2 s2'' \<and> snd (thd stlsss1) \<approx> s2'' \<and> fst (thd stlsss1) \<sim> tl2

goal (1 subgoal):
 1. is_TNil stlsss1 = is_TNil (tls1_to_tls2 s2 stlsss1) \<and> (is_TNil stlsss1 \<longrightarrow> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> rel_option bisim (terminal stlsss1) (terminal (tls1_to_tls2 s2 stlsss1))) \<and> (\<not> is_TNil stlsss1 \<longrightarrow> \<not> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> (case thd stlsss1 of (tl1, s1'') \<Rightarrow> \<lambda>(tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (thd (tls1_to_tls2 s2 stlsss1)) \<and> ((\<exists>s1 s2 stlsss1. ttl stlsss1 = stlsss1 \<and> ttl (tls1_to_tls2 s2 stlsss1) = tls1_to_tls2 s2 stlsss1 \<and> trsys1.\<tau>Runs_table s1 stlsss1 \<and> s1 \<approx> s2) \<or> tllist_all2 (\<lambda>(tl1, s1'') (tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (rel_option bisim) (ttl stlsss1) (ttl (tls1_to_tls2 s2 stlsss1))))
[PROOF STEP]
using \<open>stlsss1 = TCons (tl1, s1'') stlsss1'\<close> \<open>trsys1.\<tau>Runs_table s1'' stlsss1'\<close> bisim
[PROOF STATE]
proof (prove)
using this:
case SOME (tl2, s2''). \<exists>s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> s2' -2-tl2\<rightarrow> s2'' \<and> \<not> \<tau>move2 s2' tl2 s2'' \<and> snd (thd stlsss1) \<approx> s2'' \<and> fst (thd stlsss1) \<sim> tl2 of (tl2, s2'') \<Rightarrow> \<exists>s2'. s2 -\<tau>2\<rightarrow>* s2' \<and> s2' -2-tl2\<rightarrow> s2'' \<and> \<not> \<tau>move2 s2' tl2 s2'' \<and> snd (thd stlsss1) \<approx> s2'' \<and> fst (thd stlsss1) \<sim> tl2
stlsss1 = TCons (tl1, s1'') stlsss1'
trsys1.\<tau>Runs_table s1'' stlsss1'
s1 \<approx> s2

goal (1 subgoal):
 1. is_TNil stlsss1 = is_TNil (tls1_to_tls2 s2 stlsss1) \<and> (is_TNil stlsss1 \<longrightarrow> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> rel_option bisim (terminal stlsss1) (terminal (tls1_to_tls2 s2 stlsss1))) \<and> (\<not> is_TNil stlsss1 \<longrightarrow> \<not> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> (case thd stlsss1 of (tl1, s1'') \<Rightarrow> \<lambda>(tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (thd (tls1_to_tls2 s2 stlsss1)) \<and> ((\<exists>s1 s2 stlsss1. ttl stlsss1 = stlsss1 \<and> ttl (tls1_to_tls2 s2 stlsss1) = tls1_to_tls2 s2 stlsss1 \<and> trsys1.\<tau>Runs_table s1 stlsss1 \<and> s1 \<approx> s2) \<or> tllist_all2 (\<lambda>(tl1, s1'') (tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (rel_option bisim) (ttl stlsss1) (ttl (tls1_to_tls2 s2 stlsss1))))
[PROOF STEP]
by auto blast
[PROOF STATE]
proof (state)
this:
is_TNil stlsss1 = is_TNil (tls1_to_tls2 s2 stlsss1) \<and> (is_TNil stlsss1 \<longrightarrow> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> rel_option bisim (terminal stlsss1) (terminal (tls1_to_tls2 s2 stlsss1))) \<and> (\<not> is_TNil stlsss1 \<longrightarrow> \<not> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> (case thd stlsss1 of (tl1, s1'') \<Rightarrow> \<lambda>(tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (thd (tls1_to_tls2 s2 stlsss1)) \<and> ((\<exists>s1 s2 stlsss1. ttl stlsss1 = stlsss1 \<and> ttl (tls1_to_tls2 s2 stlsss1) = tls1_to_tls2 s2 stlsss1 \<and> trsys1.\<tau>Runs_table s1 stlsss1 \<and> s1 \<approx> s2) \<or> tllist_all2 (\<lambda>(tl1, s1'') (tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (rel_option bisim) (ttl stlsss1) (ttl (tls1_to_tls2 s2 stlsss1))))

goal (1 subgoal):
 1. \<lbrakk>stlsss1 = TNil None; s1 -\<tau>1\<rightarrow> \<infinity>\<rbrakk> \<Longrightarrow> is_TNil stlsss1 = is_TNil (tls1_to_tls2 s2 stlsss1) \<and> (is_TNil stlsss1 \<longrightarrow> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> rel_option bisim (terminal stlsss1) (terminal (tls1_to_tls2 s2 stlsss1))) \<and> (\<not> is_TNil stlsss1 \<longrightarrow> \<not> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> (case thd stlsss1 of (tl1, s1'') \<Rightarrow> \<lambda>(tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (thd (tls1_to_tls2 s2 stlsss1)) \<and> ((\<exists>s1 s2 stlsss1. ttl stlsss1 = stlsss1 \<and> ttl (tls1_to_tls2 s2 stlsss1) = tls1_to_tls2 s2 stlsss1 \<and> trsys1.\<tau>Runs_table s1 stlsss1 \<and> s1 \<approx> s2) \<or> tllist_all2 (\<lambda>(tl1, s1'') (tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (rel_option bisim) (ttl stlsss1) (ttl (tls1_to_tls2 s2 stlsss1))))
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
is_TNil stlsss1 = is_TNil (tls1_to_tls2 s2 stlsss1) \<and> (is_TNil stlsss1 \<longrightarrow> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> rel_option bisim (terminal stlsss1) (terminal (tls1_to_tls2 s2 stlsss1))) \<and> (\<not> is_TNil stlsss1 \<longrightarrow> \<not> is_TNil (tls1_to_tls2 s2 stlsss1) \<longrightarrow> (case thd stlsss1 of (tl1, s1'') \<Rightarrow> \<lambda>(tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (thd (tls1_to_tls2 s2 stlsss1)) \<and> ((\<exists>s1 s2 stlsss1. ttl stlsss1 = stlsss1 \<and> ttl (tls1_to_tls2 s2 stlsss1) = tls1_to_tls2 s2 stlsss1 \<and> trsys1.\<tau>Runs_table s1 stlsss1 \<and> s1 \<approx> s2) \<or> tllist_all2 (\<lambda>(tl1, s1'') (tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (rel_option bisim) (ttl stlsss1) (ttl (tls1_to_tls2 s2 stlsss1))))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
tllist_all2 (\<lambda>(tl1, s1'') (tl2, s2''). tl1 \<sim> tl2 \<and> s1'' \<approx> s2'') (rel_option bisim) stlsss1 (tls1_to_tls2 s2 stlsss1)

goal:
No subgoals!
[PROOF STEP]
qed