[STATEMENT]
lemma clock_simTrans:
  assumes tC: "t \<in> Clock.jkbpC"
      and ec: "clock_simAbs ec = Clock.sim_equiv_class a t"
  shows "clock_simAbs ` set (clock_simTrans a ec)
      = { Clock.sim_equiv_class a (t' \<leadsto> s)
          |t' s. t' \<leadsto> s \<in> Clock.jkbpC \<and> clock_jview a t' = clock_jview a t }"
(*<*) (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. clock_simAbs ` set (local.clock_simTrans a ec) = rel_ext (\<lambda>uu_. \<exists>t' s. uu_ = Clock.sim_equiv_class a (t' \<leadsto> s) \<and> t' \<leadsto> s \<in> Clock.jkbpC \<and> clock_jview a t' = clock_jview a t)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. clock_simAbs ` set (local.clock_simTrans a ec) \<subseteq> rel_ext (\<lambda>uu_. \<exists>t' s. uu_ = Clock.sim_equiv_class a (t' \<leadsto> s) \<and> t' \<leadsto> s \<in> Clock.jkbpC \<and> clock_jview a t' = clock_jview a t)
 2. rel_ext (\<lambda>uu_. \<exists>t' s. uu_ = Clock.sim_equiv_class a (t' \<leadsto> s) \<and> t' \<leadsto> s \<in> Clock.jkbpC \<and> clock_jview a t' = clock_jview a t) \<subseteq> clock_simAbs ` set (local.clock_simTrans a ec)
[PROOF STEP]
note image_cong_simp [cong del]
[PROOF STATE]
proof (state)
this:
\<lbrakk>?M = ?N; \<And>x. x \<in> ?N =simp=> ?f x = ?g x\<rbrakk> \<Longrightarrow> ?f ` ?M = ?g ` ?N

goal (2 subgoals):
 1. clock_simAbs ` set (local.clock_simTrans a ec) \<subseteq> rel_ext (\<lambda>uu_. \<exists>t' s. uu_ = Clock.sim_equiv_class a (t' \<leadsto> s) \<and> t' \<leadsto> s \<in> Clock.jkbpC \<and> clock_jview a t' = clock_jview a t)
 2. rel_ext (\<lambda>uu_. \<exists>t' s. uu_ = Clock.sim_equiv_class a (t' \<leadsto> s) \<and> t' \<leadsto> s \<in> Clock.jkbpC \<and> clock_jview a t' = clock_jview a t) \<subseteq> clock_simAbs ` set (local.clock_simTrans a ec)
[PROOF STEP]
show "?lhs \<subseteq> ?rhs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. clock_simAbs ` set (local.clock_simTrans a ec) \<subseteq> rel_ext (\<lambda>uu_. \<exists>t' s. uu_ = Clock.sim_equiv_class a (t' \<leadsto> s) \<and> t' \<leadsto> s \<in> Clock.jkbpC \<and> clock_jview a t' = clock_jview a t)
[PROOF STEP]
unfolding clock_simTrans_def clock_mkSuccs_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. clock_simAbs ` set (case ec of (Y, X) \<Rightarrow> let X' = local.clock_trans Y X; Y' = local.clock_trans Y Y in map (\<lambda>obs. (Y', ODList.filter (\<lambda>s. envObs a s = obs) Y')) (map (envObs a) (toList X'))) \<subseteq> rel_ext (\<lambda>uu_. \<exists>t' s. uu_ = Clock.sim_equiv_class a (t' \<leadsto> s) \<and> t' \<leadsto> s \<in> Clock.jkbpC \<and> clock_jview a t' = clock_jview a t)
[PROOF STEP]
using clock_trans_common[OF tC ec] clock_trans_agent[OF tC ec]
[PROOF STATE]
proof (prove)
using this:
toSet (local.clock_trans (fst ec) (fst ec)) = rel_ext (\<lambda>uu_. \<exists>t' s. uu_ = s \<and> t' \<leadsto> s \<in> Clock.jkbpC \<and> tLength t' = tLength t)
toSet (local.clock_trans (fst ec) (snd ec)) = rel_ext (\<lambda>uu_. \<exists>t' s. uu_ = s \<and> t' \<leadsto> s \<in> Clock.jkbpC \<and> clock_jview a t' = clock_jview a t)

goal (1 subgoal):
 1. clock_simAbs ` set (case ec of (Y, X) \<Rightarrow> let X' = local.clock_trans Y X; Y' = local.clock_trans Y Y in map (\<lambda>obs. (Y', ODList.filter (\<lambda>s. envObs a s = obs) Y')) (map (envObs a) (toList X'))) \<subseteq> rel_ext (\<lambda>uu_. \<exists>t' s. uu_ = Clock.sim_equiv_class a (t' \<leadsto> s) \<and> t' \<leadsto> s \<in> Clock.jkbpC \<and> clock_jview a t' = clock_jview a t)
[PROOF STEP]
apply (clarsimp simp: toSet_def[symmetric] clock_simAbs_def Let_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>uu_ uua_ xa t'. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t)\<rbrakk> \<Longrightarrow> \<exists>t' s. rel_ext (\<lambda>uu_. \<exists>s. uu_ = (rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t), s) \<and> (\<exists>t'. t' \<leadsto> s \<in> Clock.jkbpC \<and> tLength t' = tLength t) \<and> envObs a s = envObs a xa) = clock_sim ` rel_ext (\<lambda>t'a. t'a \<in> Clock.jkbpC \<and> tLength t'a = Suc (tLength t') \<and> envObs a (tLast t'a) = envObs a s) \<and> t' \<leadsto> s \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)
[PROOF STEP]
apply (rule_tac x=t' in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>uu_ uua_ xa t'. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t)\<rbrakk> \<Longrightarrow> \<exists>s. rel_ext (\<lambda>uu_. \<exists>s. uu_ = (rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t), s) \<and> (\<exists>t'. t' \<leadsto> s \<in> Clock.jkbpC \<and> tLength t' = tLength t) \<and> envObs a s = envObs a xa) = clock_sim ` rel_ext (\<lambda>t'a. t'a \<in> Clock.jkbpC \<and> tLength t'a = Suc (tLength t') \<and> envObs a (tLast t'a) = envObs a s) \<and> t' \<leadsto> s \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)
[PROOF STEP]
apply (rule_tac x=xa in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>uu_ uua_ xa t'. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t)\<rbrakk> \<Longrightarrow> rel_ext (\<lambda>uu_. \<exists>s. uu_ = (rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t), s) \<and> (\<exists>t'. t' \<leadsto> s \<in> Clock.jkbpC \<and> tLength t' = tLength t) \<and> envObs a s = envObs a xa) = clock_sim ` rel_ext (\<lambda>t'a. t'a \<in> Clock.jkbpC \<and> tLength t'a = Suc (tLength t') \<and> envObs a (tLast t'a) = envObs a xa) \<and> t' \<leadsto> xa \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)
[PROOF STEP]
apply (clarsimp simp: clock_sim_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>uu_ uua_ xa t'. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t)\<rbrakk> \<Longrightarrow> rel_ext (\<lambda>uu_. \<exists>s. uu_ = (rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t), s) \<and> (\<exists>t'. t' \<leadsto> s \<in> Clock.jkbpC \<and> tLength t' = tLength t) \<and> envObs a s = envObs a xa) = (\<lambda>t. (clock_commonAbs t, tLast t)) ` rel_ext (\<lambda>t'. t' \<in> Clock.jkbpC \<and> tLength t' = Suc (tLength t) \<and> envObs a (tLast t') = envObs a xa)
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>uu_ uua_ xa t' aa b s t'a. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); envObs a s = envObs a xa; t'a \<leadsto> s \<in> Clock.jkbpC; tLength t'a = tLength t\<rbrakk> \<Longrightarrow> (rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t), s) \<in> (\<lambda>t. (clock_commonAbs t, tLast t)) ` rel_ext (\<lambda>t'. t' \<in> Clock.jkbpC \<and> tLength t' = Suc (tLength t) \<and> envObs a (tLast t') = envObs a xa)
 2. \<And>uu_ uua_ xa t' aa b ta. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); ta \<in> Clock.jkbpC; tLength ta = Suc (tLength t); envObs a (tLast ta) = envObs a xa\<rbrakk> \<Longrightarrow> \<exists>s. (clock_commonAbs ta, tLast ta) = (rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t), s) \<and> (\<exists>t'. t' \<leadsto> s \<in> Clock.jkbpC \<and> tLength t' = tLength t) \<and> envObs a s = envObs a xa
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>uu_ uua_ xa t' s t'a. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); envObs a s = envObs a xa; t'a \<leadsto> s \<in> Clock.jkbpC; tLength t'a = tLength t\<rbrakk> \<Longrightarrow> (rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t), s) \<in> (\<lambda>t. (clock_commonAbs t, tLast t)) ` rel_ext (\<lambda>t'. t' \<in> Clock.jkbpC \<and> tLength t' = Suc (tLength t) \<and> envObs a (tLast t') = envObs a xa)
 2. \<And>uu_ uua_ xa t' aa b ta. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); ta \<in> Clock.jkbpC; tLength ta = Suc (tLength t); envObs a (tLast ta) = envObs a xa\<rbrakk> \<Longrightarrow> \<exists>s. (clock_commonAbs ta, tLast ta) = (rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t), s) \<and> (\<exists>t'. t' \<leadsto> s \<in> Clock.jkbpC \<and> tLength t' = tLength t) \<and> envObs a s = envObs a xa
[PROOF STEP]
apply (rule_tac x="t'a \<leadsto> s" in image_eqI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>uu_ uua_ xa t' s t'a. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); envObs a s = envObs a xa; t'a \<leadsto> s \<in> Clock.jkbpC; tLength t'a = tLength t\<rbrakk> \<Longrightarrow> (rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t), s) = (clock_commonAbs (t'a \<leadsto> s), tLast (t'a \<leadsto> s))
 2. \<And>uu_ uua_ xa t' s t'a. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); envObs a s = envObs a xa; t'a \<leadsto> s \<in> Clock.jkbpC; tLength t'a = tLength t\<rbrakk> \<Longrightarrow> t'a \<leadsto> s \<in> rel_ext (\<lambda>t'. t' \<in> Clock.jkbpC \<and> tLength t' = Suc (tLength t) \<and> envObs a (tLast t') = envObs a xa)
 3. \<And>uu_ uua_ xa t' aa b ta. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); ta \<in> Clock.jkbpC; tLength ta = Suc (tLength t); envObs a (tLast ta) = envObs a xa\<rbrakk> \<Longrightarrow> \<exists>s. (clock_commonAbs ta, tLast ta) = (rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t), s) \<and> (\<exists>t'. t' \<leadsto> s \<in> Clock.jkbpC \<and> tLength t' = tLength t) \<and> envObs a s = envObs a xa
[PROOF STEP]
apply (clarsimp simp: Let_def Set.image_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>uu_ uua_ xa t' s t'a. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); envObs a s = envObs a xa; t'a \<leadsto> s \<in> Clock.jkbpC; tLength t'a = tLength t\<rbrakk> \<Longrightarrow> rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t) = rel_ext (\<lambda>y. \<exists>x. (\<exists>ta eact aact. x = ta \<leadsto> envTrans eact aact (tLast ta) \<and> ta \<in> Clock.jkbpCn (tLength t) \<and> eact \<in> set (envAction (tLast ta)) \<and> (\<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t)) ta a))) \<and> y = tLast x)
 2. \<And>uu_ uua_ xa t' s t'a. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); envObs a s = envObs a xa; t'a \<leadsto> s \<in> Clock.jkbpC; tLength t'a = tLength t\<rbrakk> \<Longrightarrow> t'a \<leadsto> s \<in> rel_ext (\<lambda>t'. t' \<in> Clock.jkbpC \<and> tLength t' = Suc (tLength t) \<and> envObs a (tLast t') = envObs a xa)
 3. \<And>uu_ uua_ xa t' aa b ta. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); ta \<in> Clock.jkbpC; tLength ta = Suc (tLength t); envObs a (tLast ta) = envObs a xa\<rbrakk> \<Longrightarrow> \<exists>s. (clock_commonAbs ta, tLast ta) = (rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t), s) \<and> (\<exists>t'. t' \<leadsto> s \<in> Clock.jkbpC \<and> tLength t' = tLength t) \<and> envObs a s = envObs a xa
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>uu_ uua_ xa t' s t'a x t'b. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); envObs a s = envObs a xa; t'a \<leadsto> s \<in> Clock.jkbpC; tLength t'a = tLength t; t'b \<leadsto> x \<in> Clock.jkbpC; tLength t'b = tLength t\<rbrakk> \<Longrightarrow> \<exists>xa. (\<exists>ta eact aact. xa = ta \<leadsto> envTrans eact aact (tLast ta) \<and> ta \<in> Clock.jkbpCn (tLength t) \<and> eact \<in> set (envAction (tLast ta)) \<and> (\<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t)) ta a))) \<and> x = tLast xa
 2. \<And>uu_ uua_ xa t' s t'a x xb ta eact aact. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); envObs a s = envObs a xa; t'a \<leadsto> s \<in> Clock.jkbpC; tLength t'a = tLength t; ta \<in> Clock.jkbpCn (tLength t); eact \<in> set (envAction (tLast ta)); \<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t)) ta a)\<rbrakk> \<Longrightarrow> \<exists>t'. t' \<leadsto> tLast (ta \<leadsto> envTrans eact aact (tLast ta)) \<in> Clock.jkbpC \<and> tLength t' = tLength t
 3. \<And>uu_ uua_ xa t' s t'a. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); envObs a s = envObs a xa; t'a \<leadsto> s \<in> Clock.jkbpC; tLength t'a = tLength t\<rbrakk> \<Longrightarrow> tLength (t'a \<leadsto> s) = Suc (tLength t)
 4. \<And>uu_ uua_ xa t' s t'a. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); envObs a s = envObs a xa; t'a \<leadsto> s \<in> Clock.jkbpC; tLength t'a = tLength t\<rbrakk> \<Longrightarrow> envObs a (tLast (t'a \<leadsto> s)) = envObs a xa
 5. \<And>uu_ uua_ xa t' aa b ta. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); ta \<in> Clock.jkbpC; tLength ta = Suc (tLength t); envObs a (tLast ta) = envObs a xa\<rbrakk> \<Longrightarrow> \<exists>s. (clock_commonAbs ta, tLast ta) = (rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t), s) \<and> (\<exists>t'. t' \<leadsto> s \<in> Clock.jkbpC \<and> tLength t' = tLength t) \<and> envObs a s = envObs a xa
[PROOF STEP]
apply (rule_tac x="t'b \<leadsto> x" in exI)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>uu_ uua_ xa t' s t'a x t'b. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); envObs a s = envObs a xa; t'a \<leadsto> s \<in> Clock.jkbpC; tLength t'a = tLength t; t'b \<leadsto> x \<in> Clock.jkbpC; tLength t'b = tLength t\<rbrakk> \<Longrightarrow> (\<exists>ta eact aact. t'b \<leadsto> x = ta \<leadsto> envTrans eact aact (tLast ta) \<and> ta \<in> Clock.jkbpCn (tLength t) \<and> eact \<in> set (envAction (tLast ta)) \<and> (\<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t)) ta a))) \<and> x = tLast (t'b \<leadsto> x)
 2. \<And>uu_ uua_ xa t' s t'a x xb ta eact aact. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); envObs a s = envObs a xa; t'a \<leadsto> s \<in> Clock.jkbpC; tLength t'a = tLength t; ta \<in> Clock.jkbpCn (tLength t); eact \<in> set (envAction (tLast ta)); \<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t)) ta a)\<rbrakk> \<Longrightarrow> \<exists>t'. t' \<leadsto> tLast (ta \<leadsto> envTrans eact aact (tLast ta)) \<in> Clock.jkbpC \<and> tLength t' = tLength t
 3. \<And>uu_ uua_ xa t' s t'a. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); envObs a s = envObs a xa; t'a \<leadsto> s \<in> Clock.jkbpC; tLength t'a = tLength t\<rbrakk> \<Longrightarrow> tLength (t'a \<leadsto> s) = Suc (tLength t)
 4. \<And>uu_ uua_ xa t' s t'a. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); envObs a s = envObs a xa; t'a \<leadsto> s \<in> Clock.jkbpC; tLength t'a = tLength t\<rbrakk> \<Longrightarrow> envObs a (tLast (t'a \<leadsto> s)) = envObs a xa
 5. \<And>uu_ uua_ xa t' aa b ta. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); ta \<in> Clock.jkbpC; tLength ta = Suc (tLength t); envObs a (tLast ta) = envObs a xa\<rbrakk> \<Longrightarrow> \<exists>s. (clock_commonAbs ta, tLast ta) = (rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t), s) \<and> (\<exists>t'. t' \<leadsto> s \<in> Clock.jkbpC \<and> tLength t' = tLength t) \<and> envObs a s = envObs a xa
[PROOF STEP]
apply (clarsimp simp: Let_def Set.image_def)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>uu_ uua_ xa t' s t'a x t'b. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); envObs a s = envObs a xa; t'a \<leadsto> s \<in> Clock.jkbpC; tLength t'a = tLength t; t'b \<leadsto> x \<in> Clock.jkbpC; tLength t'b = tLength t\<rbrakk> \<Longrightarrow> \<exists>eact aact. x = envTrans eact aact (tLast t'b) \<and> t'b \<in> Clock.jkbpCn (tLength t) \<and> eact \<in> set (envAction (tLast t'b)) \<and> (\<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t)) t'b a))
 2. \<And>uu_ uua_ xa t' s t'a x xb ta eact aact. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); envObs a s = envObs a xa; t'a \<leadsto> s \<in> Clock.jkbpC; tLength t'a = tLength t; ta \<in> Clock.jkbpCn (tLength t); eact \<in> set (envAction (tLast ta)); \<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t)) ta a)\<rbrakk> \<Longrightarrow> \<exists>t'. t' \<leadsto> tLast (ta \<leadsto> envTrans eact aact (tLast ta)) \<in> Clock.jkbpC \<and> tLength t' = tLength t
 3. \<And>uu_ uua_ xa t' s t'a. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); envObs a s = envObs a xa; t'a \<leadsto> s \<in> Clock.jkbpC; tLength t'a = tLength t\<rbrakk> \<Longrightarrow> tLength (t'a \<leadsto> s) = Suc (tLength t)
 4. \<And>uu_ uua_ xa t' s t'a. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); envObs a s = envObs a xa; t'a \<leadsto> s \<in> Clock.jkbpC; tLength t'a = tLength t\<rbrakk> \<Longrightarrow> envObs a (tLast (t'a \<leadsto> s)) = envObs a xa
 5. \<And>uu_ uua_ xa t' aa b ta. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); ta \<in> Clock.jkbpC; tLength ta = Suc (tLength t); envObs a (tLast ta) = envObs a xa\<rbrakk> \<Longrightarrow> \<exists>s. (clock_commonAbs ta, tLast ta) = (rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t), s) \<and> (\<exists>t'. t' \<leadsto> s \<in> Clock.jkbpC \<and> tLength t' = tLength t) \<and> envObs a s = envObs a xa
[PROOF STEP]
apply (drule_tac t="t'b \<leadsto> x" in Clock.jkbpC_tLength_inv[OF _ refl])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>uu_ uua_ xa t' s t'a x t'b. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); envObs a s = envObs a xa; t'a \<leadsto> s \<in> Clock.jkbpC; tLength t'a = tLength t; tLength t'b = tLength t; t'b \<leadsto> x \<in> Clock.jkbpCn (tLength (t'b \<leadsto> x))\<rbrakk> \<Longrightarrow> \<exists>eact aact. x = envTrans eact aact (tLast t'b) \<and> t'b \<in> Clock.jkbpCn (tLength t) \<and> eact \<in> set (envAction (tLast t'b)) \<and> (\<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t)) t'b a))
 2. \<And>uu_ uua_ xa t' s t'a x xb ta eact aact. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); envObs a s = envObs a xa; t'a \<leadsto> s \<in> Clock.jkbpC; tLength t'a = tLength t; ta \<in> Clock.jkbpCn (tLength t); eact \<in> set (envAction (tLast ta)); \<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t)) ta a)\<rbrakk> \<Longrightarrow> \<exists>t'. t' \<leadsto> tLast (ta \<leadsto> envTrans eact aact (tLast ta)) \<in> Clock.jkbpC \<and> tLength t' = tLength t
 3. \<And>uu_ uua_ xa t' s t'a. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); envObs a s = envObs a xa; t'a \<leadsto> s \<in> Clock.jkbpC; tLength t'a = tLength t\<rbrakk> \<Longrightarrow> tLength (t'a \<leadsto> s) = Suc (tLength t)
 4. \<And>uu_ uua_ xa t' s t'a. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); envObs a s = envObs a xa; t'a \<leadsto> s \<in> Clock.jkbpC; tLength t'a = tLength t\<rbrakk> \<Longrightarrow> envObs a (tLast (t'a \<leadsto> s)) = envObs a xa
 5. \<And>uu_ uua_ xa t' aa b ta. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); ta \<in> Clock.jkbpC; tLength ta = Suc (tLength t); envObs a (tLast ta) = envObs a xa\<rbrakk> \<Longrightarrow> \<exists>s. (clock_commonAbs ta, tLast ta) = (rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t), s) \<and> (\<exists>t'. t' \<leadsto> s \<in> Clock.jkbpC \<and> tLength t' = tLength t) \<and> envObs a s = envObs a xa
[PROOF STEP]
apply (auto simp: Let_def)[1]
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>uu_ uua_ xa t' s t'a x xb ta eact aact. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); envObs a s = envObs a xa; t'a \<leadsto> s \<in> Clock.jkbpC; tLength t'a = tLength t; ta \<in> Clock.jkbpCn (tLength t); eact \<in> set (envAction (tLast ta)); \<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t)) ta a)\<rbrakk> \<Longrightarrow> \<exists>t'. t' \<leadsto> tLast (ta \<leadsto> envTrans eact aact (tLast ta)) \<in> Clock.jkbpC \<and> tLength t' = tLength t
 2. \<And>uu_ uua_ xa t' s t'a. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); envObs a s = envObs a xa; t'a \<leadsto> s \<in> Clock.jkbpC; tLength t'a = tLength t\<rbrakk> \<Longrightarrow> tLength (t'a \<leadsto> s) = Suc (tLength t)
 3. \<And>uu_ uua_ xa t' s t'a. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); envObs a s = envObs a xa; t'a \<leadsto> s \<in> Clock.jkbpC; tLength t'a = tLength t\<rbrakk> \<Longrightarrow> envObs a (tLast (t'a \<leadsto> s)) = envObs a xa
 4. \<And>uu_ uua_ xa t' aa b ta. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); ta \<in> Clock.jkbpC; tLength ta = Suc (tLength t); envObs a (tLast ta) = envObs a xa\<rbrakk> \<Longrightarrow> \<exists>s. (clock_commonAbs ta, tLast ta) = (rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t), s) \<and> (\<exists>t'. t' \<leadsto> s \<in> Clock.jkbpC \<and> tLength t' = tLength t) \<and> envObs a s = envObs a xa
[PROOF STEP]
apply (rule_tac x="ta" in exI)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>uu_ uua_ xa t' s t'a x xb ta eact aact. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); envObs a s = envObs a xa; t'a \<leadsto> s \<in> Clock.jkbpC; tLength t'a = tLength t; ta \<in> Clock.jkbpCn (tLength t); eact \<in> set (envAction (tLast ta)); \<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t)) ta a)\<rbrakk> \<Longrightarrow> ta \<leadsto> tLast (ta \<leadsto> envTrans eact aact (tLast ta)) \<in> Clock.jkbpC \<and> tLength ta = tLength t
 2. \<And>uu_ uua_ xa t' s t'a. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); envObs a s = envObs a xa; t'a \<leadsto> s \<in> Clock.jkbpC; tLength t'a = tLength t\<rbrakk> \<Longrightarrow> tLength (t'a \<leadsto> s) = Suc (tLength t)
 3. \<And>uu_ uua_ xa t' s t'a. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); envObs a s = envObs a xa; t'a \<leadsto> s \<in> Clock.jkbpC; tLength t'a = tLength t\<rbrakk> \<Longrightarrow> envObs a (tLast (t'a \<leadsto> s)) = envObs a xa
 4. \<And>uu_ uua_ xa t' aa b ta. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); ta \<in> Clock.jkbpC; tLength ta = Suc (tLength t); envObs a (tLast ta) = envObs a xa\<rbrakk> \<Longrightarrow> \<exists>s. (clock_commonAbs ta, tLast ta) = (rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t), s) \<and> (\<exists>t'. t' \<leadsto> s \<in> Clock.jkbpC \<and> tLength t' = tLength t) \<and> envObs a s = envObs a xa
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>uu_ uua_ xa t' s t'a ta eact aact. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); envObs a s = envObs a xa; t'a \<leadsto> s \<in> Clock.jkbpC; tLength t'a = tLength t; ta \<in> Clock.jkbpCn (tLength t); eact \<in> set (envAction (tLast ta)); \<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t)) ta a)\<rbrakk> \<Longrightarrow> ta \<leadsto> envTrans eact aact (tLast ta) \<in> Clock.jkbpC
 2. \<And>uu_ uua_ xa t' s t'a. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); envObs a s = envObs a xa; t'a \<leadsto> s \<in> Clock.jkbpC; tLength t'a = tLength t\<rbrakk> \<Longrightarrow> tLength (t'a \<leadsto> s) = Suc (tLength t)
 3. \<And>uu_ uua_ xa t' s t'a. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); envObs a s = envObs a xa; t'a \<leadsto> s \<in> Clock.jkbpC; tLength t'a = tLength t\<rbrakk> \<Longrightarrow> envObs a (tLast (t'a \<leadsto> s)) = envObs a xa
 4. \<And>uu_ uua_ xa t' aa b ta. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); ta \<in> Clock.jkbpC; tLength ta = Suc (tLength t); envObs a (tLast ta) = envObs a xa\<rbrakk> \<Longrightarrow> \<exists>s. (clock_commonAbs ta, tLast ta) = (rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t), s) \<and> (\<exists>t'. t' \<leadsto> s \<in> Clock.jkbpC \<and> tLength t' = tLength t) \<and> envObs a s = envObs a xa
[PROOF STEP]
apply (rule Clock.jkbpCn_jkbpC_inc[where n="Suc (tLength t)"])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>uu_ uua_ xa t' s t'a ta eact aact. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); envObs a s = envObs a xa; t'a \<leadsto> s \<in> Clock.jkbpC; tLength t'a = tLength t; ta \<in> Clock.jkbpCn (tLength t); eact \<in> set (envAction (tLast ta)); \<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t)) ta a)\<rbrakk> \<Longrightarrow> ta \<leadsto> envTrans eact aact (tLast ta) \<in> Clock.jkbpCn (Suc (tLength t))
 2. \<And>uu_ uua_ xa t' s t'a. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); envObs a s = envObs a xa; t'a \<leadsto> s \<in> Clock.jkbpC; tLength t'a = tLength t\<rbrakk> \<Longrightarrow> tLength (t'a \<leadsto> s) = Suc (tLength t)
 3. \<And>uu_ uua_ xa t' s t'a. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); envObs a s = envObs a xa; t'a \<leadsto> s \<in> Clock.jkbpC; tLength t'a = tLength t\<rbrakk> \<Longrightarrow> envObs a (tLast (t'a \<leadsto> s)) = envObs a xa
 4. \<And>uu_ uua_ xa t' aa b ta. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); ta \<in> Clock.jkbpC; tLength ta = Suc (tLength t); envObs a (tLast ta) = envObs a xa\<rbrakk> \<Longrightarrow> \<exists>s. (clock_commonAbs ta, tLast ta) = (rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t), s) \<and> (\<exists>t'. t' \<leadsto> s \<in> Clock.jkbpC \<and> tLength t' = tLength t) \<and> envObs a s = envObs a xa
[PROOF STEP]
apply (auto simp: Let_def)[3]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>uu_ uua_ xa t' aa b ta. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); ta \<in> Clock.jkbpC; tLength ta = Suc (tLength t); envObs a (tLast ta) = envObs a xa\<rbrakk> \<Longrightarrow> \<exists>s. (clock_commonAbs ta, tLast ta) = (rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t), s) \<and> (\<exists>t'. t' \<leadsto> s \<in> Clock.jkbpC \<and> tLength t' = tLength t) \<and> envObs a s = envObs a xa
[PROOF STEP]
apply (rule_tac x="tLast ta" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>uu_ uua_ xa t' aa b ta. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); ta \<in> Clock.jkbpC; tLength ta = Suc (tLength t); envObs a (tLast ta) = envObs a xa\<rbrakk> \<Longrightarrow> (clock_commonAbs ta, tLast ta) = (rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t), tLast ta) \<and> (\<exists>t'. t' \<leadsto> tLast ta \<in> Clock.jkbpC \<and> tLength t' = tLength t) \<and> envObs a (tLast ta) = envObs a xa
[PROOF STEP]
apply (clarsimp simp: Let_def Set.image_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>uu_ uua_ xa t' ta. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); ta \<in> Clock.jkbpC; tLength ta = Suc (tLength t); envObs a (tLast ta) = envObs a xa\<rbrakk> \<Longrightarrow> rel_ext (\<lambda>y. \<exists>x. (\<exists>ta eact aact. x = ta \<leadsto> envTrans eact aact (tLast ta) \<and> ta \<in> Clock.jkbpCn (tLength t) \<and> eact \<in> set (envAction (tLast ta)) \<and> (\<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t)) ta a))) \<and> y = tLast x) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t) \<and> (\<exists>t'. t' \<leadsto> tLast ta \<in> Clock.jkbpC \<and> tLength t' = tLength t)
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>uu_ uua_ xa t' ta x xb taa eact aact. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); ta \<in> Clock.jkbpC; tLength ta = Suc (tLength t); envObs a (tLast ta) = envObs a xa; taa \<in> Clock.jkbpCn (tLength t); eact \<in> set (envAction (tLast taa)); \<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t)) taa a)\<rbrakk> \<Longrightarrow> \<exists>t'. t' \<leadsto> tLast (taa \<leadsto> envTrans eact aact (tLast taa)) \<in> Clock.jkbpC \<and> tLength t' = tLength t
 2. \<And>uu_ uua_ xa t' ta x t'a. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); ta \<in> Clock.jkbpC; tLength ta = Suc (tLength t); envObs a (tLast ta) = envObs a xa; t'a \<leadsto> x \<in> Clock.jkbpC; tLength t'a = tLength t\<rbrakk> \<Longrightarrow> \<exists>xa. (\<exists>ta eact aact. xa = ta \<leadsto> envTrans eact aact (tLast ta) \<and> ta \<in> Clock.jkbpCn (tLength t) \<and> eact \<in> set (envAction (tLast ta)) \<and> (\<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t)) ta a))) \<and> x = tLast xa
 3. \<And>uu_ uua_ xa t' ta. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); ta \<in> Clock.jkbpC; tLength ta = Suc (tLength t); envObs a (tLast ta) = envObs a xa\<rbrakk> \<Longrightarrow> \<exists>t'. t' \<leadsto> tLast ta \<in> Clock.jkbpC \<and> tLength t' = tLength t
[PROOF STEP]
apply (rule_tac x="taa" in exI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>uu_ uua_ xa t' ta x xb taa eact aact. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); ta \<in> Clock.jkbpC; tLength ta = Suc (tLength t); envObs a (tLast ta) = envObs a xa; taa \<in> Clock.jkbpCn (tLength t); eact \<in> set (envAction (tLast taa)); \<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t)) taa a)\<rbrakk> \<Longrightarrow> taa \<leadsto> tLast (taa \<leadsto> envTrans eact aact (tLast taa)) \<in> Clock.jkbpC \<and> tLength taa = tLength t
 2. \<And>uu_ uua_ xa t' ta x t'a. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); ta \<in> Clock.jkbpC; tLength ta = Suc (tLength t); envObs a (tLast ta) = envObs a xa; t'a \<leadsto> x \<in> Clock.jkbpC; tLength t'a = tLength t\<rbrakk> \<Longrightarrow> \<exists>xa. (\<exists>ta eact aact. xa = ta \<leadsto> envTrans eact aact (tLast ta) \<and> ta \<in> Clock.jkbpCn (tLength t) \<and> eact \<in> set (envAction (tLast ta)) \<and> (\<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t)) ta a))) \<and> x = tLast xa
 3. \<And>uu_ uua_ xa t' ta. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); ta \<in> Clock.jkbpC; tLength ta = Suc (tLength t); envObs a (tLast ta) = envObs a xa\<rbrakk> \<Longrightarrow> \<exists>t'. t' \<leadsto> tLast ta \<in> Clock.jkbpC \<and> tLength t' = tLength t
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>uu_ uua_ xa t' ta taa eact aact. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); ta \<in> Clock.jkbpC; tLength ta = Suc (tLength t); envObs a (tLast ta) = envObs a xa; taa \<in> Clock.jkbpCn (tLength t); eact \<in> set (envAction (tLast taa)); \<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t)) taa a)\<rbrakk> \<Longrightarrow> taa \<leadsto> envTrans eact aact (tLast taa) \<in> Clock.jkbpC
 2. \<And>uu_ uua_ xa t' ta x t'a. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); ta \<in> Clock.jkbpC; tLength ta = Suc (tLength t); envObs a (tLast ta) = envObs a xa; t'a \<leadsto> x \<in> Clock.jkbpC; tLength t'a = tLength t\<rbrakk> \<Longrightarrow> \<exists>xa. (\<exists>ta eact aact. xa = ta \<leadsto> envTrans eact aact (tLast ta) \<and> ta \<in> Clock.jkbpCn (tLength t) \<and> eact \<in> set (envAction (tLast ta)) \<and> (\<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t)) ta a))) \<and> x = tLast xa
 3. \<And>uu_ uua_ xa t' ta. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); ta \<in> Clock.jkbpC; tLength ta = Suc (tLength t); envObs a (tLast ta) = envObs a xa\<rbrakk> \<Longrightarrow> \<exists>t'. t' \<leadsto> tLast ta \<in> Clock.jkbpC \<and> tLength t' = tLength t
[PROOF STEP]
apply (rule Clock.jkbpCn_jkbpC_inc[where n="Suc (tLength t)"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>uu_ uua_ xa t' ta taa eact aact. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); ta \<in> Clock.jkbpC; tLength ta = Suc (tLength t); envObs a (tLast ta) = envObs a xa; taa \<in> Clock.jkbpCn (tLength t); eact \<in> set (envAction (tLast taa)); \<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t)) taa a)\<rbrakk> \<Longrightarrow> taa \<leadsto> envTrans eact aact (tLast taa) \<in> Clock.jkbpCn (Suc (tLength t))
 2. \<And>uu_ uua_ xa t' ta x t'a. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); ta \<in> Clock.jkbpC; tLength ta = Suc (tLength t); envObs a (tLast ta) = envObs a xa; t'a \<leadsto> x \<in> Clock.jkbpC; tLength t'a = tLength t\<rbrakk> \<Longrightarrow> \<exists>xa. (\<exists>ta eact aact. xa = ta \<leadsto> envTrans eact aact (tLast ta) \<and> ta \<in> Clock.jkbpCn (tLength t) \<and> eact \<in> set (envAction (tLast ta)) \<and> (\<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t)) ta a))) \<and> x = tLast xa
 3. \<And>uu_ uua_ xa t' ta. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); ta \<in> Clock.jkbpC; tLength ta = Suc (tLength t); envObs a (tLast ta) = envObs a xa\<rbrakk> \<Longrightarrow> \<exists>t'. t' \<leadsto> tLast ta \<in> Clock.jkbpC \<and> tLength t' = tLength t
[PROOF STEP]
apply (auto simp: Let_def)[1]
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>uu_ uua_ xa t' ta x t'a. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); ta \<in> Clock.jkbpC; tLength ta = Suc (tLength t); envObs a (tLast ta) = envObs a xa; t'a \<leadsto> x \<in> Clock.jkbpC; tLength t'a = tLength t\<rbrakk> \<Longrightarrow> \<exists>xa. (\<exists>ta eact aact. xa = ta \<leadsto> envTrans eact aact (tLast ta) \<and> ta \<in> Clock.jkbpCn (tLength t) \<and> eact \<in> set (envAction (tLast ta)) \<and> (\<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t)) ta a))) \<and> x = tLast xa
 2. \<And>uu_ uua_ xa t' ta. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); ta \<in> Clock.jkbpC; tLength ta = Suc (tLength t); envObs a (tLast ta) = envObs a xa\<rbrakk> \<Longrightarrow> \<exists>t'. t' \<leadsto> tLast ta \<in> Clock.jkbpC \<and> tLength t' = tLength t
[PROOF STEP]
apply (drule_tac t="t'a \<leadsto> x" in Clock.jkbpC_tLength_inv[OF _ refl])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>uu_ uua_ xa t' ta x t'a. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); ta \<in> Clock.jkbpC; tLength ta = Suc (tLength t); envObs a (tLast ta) = envObs a xa; tLength t'a = tLength t; t'a \<leadsto> x \<in> Clock.jkbpCn (tLength (t'a \<leadsto> x))\<rbrakk> \<Longrightarrow> \<exists>xa. (\<exists>ta eact aact. xa = ta \<leadsto> envTrans eact aact (tLast ta) \<and> ta \<in> Clock.jkbpCn (tLength t) \<and> eact \<in> set (envAction (tLast ta)) \<and> (\<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t)) ta a))) \<and> x = tLast xa
 2. \<And>uu_ uua_ xa t' ta. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); ta \<in> Clock.jkbpC; tLength ta = Suc (tLength t); envObs a (tLast ta) = envObs a xa\<rbrakk> \<Longrightarrow> \<exists>t'. t' \<leadsto> tLast ta \<in> Clock.jkbpC \<and> tLength t' = tLength t
[PROOF STEP]
apply (rule_tac x="t'a \<leadsto> x" in exI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>uu_ uua_ xa t' ta x t'a. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); ta \<in> Clock.jkbpC; tLength ta = Suc (tLength t); envObs a (tLast ta) = envObs a xa; tLength t'a = tLength t; t'a \<leadsto> x \<in> Clock.jkbpCn (tLength (t'a \<leadsto> x))\<rbrakk> \<Longrightarrow> (\<exists>ta eact aact. t'a \<leadsto> x = ta \<leadsto> envTrans eact aact (tLast ta) \<and> ta \<in> Clock.jkbpCn (tLength t) \<and> eact \<in> set (envAction (tLast ta)) \<and> (\<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t)) ta a))) \<and> x = tLast (t'a \<leadsto> x)
 2. \<And>uu_ uua_ xa t' ta. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); ta \<in> Clock.jkbpC; tLength ta = Suc (tLength t); envObs a (tLast ta) = envObs a xa\<rbrakk> \<Longrightarrow> \<exists>t'. t' \<leadsto> tLast ta \<in> Clock.jkbpC \<and> tLength t' = tLength t
[PROOF STEP]
apply (auto simp: Let_def)[1]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>uu_ uua_ xa t' ta. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); ta \<in> Clock.jkbpC; tLength ta = Suc (tLength t); envObs a (tLast ta) = envObs a xa\<rbrakk> \<Longrightarrow> \<exists>t'. t' \<leadsto> tLast ta \<in> Clock.jkbpC \<and> tLength t' = tLength t
[PROOF STEP]
apply (drule_tac t="ta" in Clock.jkbpC_tLength_inv)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>uu_ uua_ xa t' ta. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); tLength ta = Suc (tLength t); envObs a (tLast ta) = envObs a xa\<rbrakk> \<Longrightarrow> tLength ta = ?n189 uu_ uua_ xa t' ta
 2. \<And>uu_ uua_ xa t' ta. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); tLength ta = Suc (tLength t); envObs a (tLast ta) = envObs a xa; ta \<in> Clock.jkbpCn (?n189 uu_ uua_ xa t' ta)\<rbrakk> \<Longrightarrow> \<exists>t'. t' \<leadsto> tLast ta \<in> Clock.jkbpC \<and> tLength t' = tLength t
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>uu_ uua_ xa t' ta. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); tLength ta = Suc (tLength t); envObs a (tLast ta) = envObs a xa; ta \<in> Clock.jkbpCn (Suc (tLength t))\<rbrakk> \<Longrightarrow> \<exists>t'. t' \<leadsto> tLast ta \<in> Clock.jkbpC \<and> tLength t' = tLength t
[PROOF STEP]
apply (clarsimp simp: Let_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>uu_ uua_ xa t' ta eact aact. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); envObs a (envTrans eact aact (tLast ta)) = envObs a xa; ta \<in> Clock.jkbpCn (tLength t); eact \<in> set (envAction (tLast ta)); \<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t)) ta a)\<rbrakk> \<Longrightarrow> \<exists>t'. t' \<leadsto> envTrans eact aact (tLast ta) \<in> Clock.jkbpC \<and> tLength t' = tLength t
[PROOF STEP]
apply (rule_tac x="ta" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>uu_ uua_ xa t' ta eact aact. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); envObs a (envTrans eact aact (tLast ta)) = envObs a xa; ta \<in> Clock.jkbpCn (tLength t); eact \<in> set (envAction (tLast ta)); \<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t)) ta a)\<rbrakk> \<Longrightarrow> ta \<leadsto> envTrans eact aact (tLast ta) \<in> Clock.jkbpC \<and> tLength ta = tLength t
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>uu_ uua_ xa t' ta eact aact. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); envObs a (envTrans eact aact (tLast ta)) = envObs a xa; ta \<in> Clock.jkbpCn (tLength t); eact \<in> set (envAction (tLast ta)); \<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t)) ta a)\<rbrakk> \<Longrightarrow> ta \<leadsto> envTrans eact aact (tLast ta) \<in> Clock.jkbpC
[PROOF STEP]
apply (rule Clock.jkbpCn_jkbpC_inc[where n="Suc (tLength t)"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>uu_ uua_ xa t' ta eact aact. \<lbrakk>toSet (local.clock_trans uua_ uua_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans uua_ uu_) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); ec = (uua_, uu_); t' \<leadsto> xa \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); envObs a (envTrans eact aact (tLast ta)) = envObs a xa; ta \<in> Clock.jkbpCn (tLength t); eact \<in> set (envAction (tLast ta)); \<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t)) ta a)\<rbrakk> \<Longrightarrow> ta \<leadsto> envTrans eact aact (tLast ta) \<in> Clock.jkbpCn (Suc (tLength t))
[PROOF STEP]
apply (auto simp: Let_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
clock_simAbs ` set (local.clock_simTrans a ec) \<subseteq> rel_ext (\<lambda>uu_. \<exists>t' s. uu_ = Clock.sim_equiv_class a (t' \<leadsto> s) \<and> t' \<leadsto> s \<in> Clock.jkbpC \<and> clock_jview a t' = clock_jview a t)

goal (1 subgoal):
 1. rel_ext (\<lambda>uu_. \<exists>t' s. uu_ = Clock.sim_equiv_class a (t' \<leadsto> s) \<and> t' \<leadsto> s \<in> Clock.jkbpC \<and> clock_jview a t' = clock_jview a t) \<subseteq> clock_simAbs ` set (local.clock_simTrans a ec)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rel_ext (\<lambda>uu_. \<exists>t' s. uu_ = Clock.sim_equiv_class a (t' \<leadsto> s) \<and> t' \<leadsto> s \<in> Clock.jkbpC \<and> clock_jview a t' = clock_jview a t) \<subseteq> clock_simAbs ` set (local.clock_simTrans a ec)
[PROOF STEP]
show "?rhs \<subseteq> ?lhs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_ext (\<lambda>uu_. \<exists>t' s. uu_ = Clock.sim_equiv_class a (t' \<leadsto> s) \<and> t' \<leadsto> s \<in> Clock.jkbpC \<and> clock_jview a t' = clock_jview a t) \<subseteq> clock_simAbs ` set (local.clock_simTrans a ec)
[PROOF STEP]
unfolding clock_simTrans_def Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_ext (\<lambda>uu_. \<exists>t' s. uu_ = Clock.sim_equiv_class a (t' \<leadsto> s) \<and> t' \<leadsto> s \<in> Clock.jkbpC \<and> clock_jview a t' = clock_jview a t) \<subseteq> clock_simAbs ` set (case ec of (Y, X) \<Rightarrow> map (\<lambda>obs. clock_mkSuccs (envObs a) obs (local.clock_trans Y Y)) (map (envObs a) (toList (local.clock_trans Y X))))
[PROOF STEP]
apply (cases ec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa b. ec = (aa, b) \<Longrightarrow> rel_ext (\<lambda>uu_. \<exists>t' s. uu_ = Clock.sim_equiv_class a (t' \<leadsto> s) \<and> t' \<leadsto> s \<in> Clock.jkbpC \<and> clock_jview a t' = clock_jview a t) \<subseteq> clock_simAbs ` set (case ec of (Y, X) \<Rightarrow> map (\<lambda>obs. clock_mkSuccs (envObs a) obs (local.clock_trans Y Y)) (map (envObs a) (toList (local.clock_trans Y X))))
[PROOF STEP]
using clock_trans_common[OF tC ec] clock_trans_agent[OF tC ec]
[PROOF STATE]
proof (prove)
using this:
toSet (local.clock_trans (fst ec) (fst ec)) = rel_ext (\<lambda>uu_. \<exists>t' s. uu_ = s \<and> t' \<leadsto> s \<in> Clock.jkbpC \<and> tLength t' = tLength t)
toSet (local.clock_trans (fst ec) (snd ec)) = rel_ext (\<lambda>uu_. \<exists>t' s. uu_ = s \<and> t' \<leadsto> s \<in> Clock.jkbpC \<and> clock_jview a t' = clock_jview a t)

goal (1 subgoal):
 1. \<And>aa b. ec = (aa, b) \<Longrightarrow> rel_ext (\<lambda>uu_. \<exists>t' s. uu_ = Clock.sim_equiv_class a (t' \<leadsto> s) \<and> t' \<leadsto> s \<in> Clock.jkbpC \<and> clock_jview a t' = clock_jview a t) \<subseteq> clock_simAbs ` set (case ec of (Y, X) \<Rightarrow> map (\<lambda>obs. clock_mkSuccs (envObs a) obs (local.clock_trans Y Y)) (map (envObs a) (toList (local.clock_trans Y X))))
[PROOF STEP]
apply (clarsimp simp: toSet_def[symmetric] Set.image_def clock_simAbs_def
                simp del: split_paired_Ex)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa b t' s. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t)\<rbrakk> \<Longrightarrow> \<exists>x. (\<exists>xa. (\<exists>t'. t' \<leadsto> xa \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)) \<and> x = clock_mkSuccs (envObs a) (envObs a xa) (local.clock_trans aa aa)) \<and> rel_ext (\<lambda>y. \<exists>x. x \<in> Clock.jkbpC \<and> tLength x = Suc (tLength t) \<and> envObs a (tLast x) = envObs a s \<and> y = clock_sim x) = rel_ext (\<lambda>uu_. \<exists>s. uu_ = (toSet (fst x), s) \<and> s \<in> toSet (snd x))
[PROOF STEP]
apply (rule_tac x="clock_mkSuccs (envObs a) (envObs a s) (clock_trans aa aa)" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa b t' s. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t)\<rbrakk> \<Longrightarrow> (\<exists>x. (\<exists>t'. t' \<leadsto> x \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)) \<and> clock_mkSuccs (envObs a) (envObs a s) (local.clock_trans aa aa) = clock_mkSuccs (envObs a) (envObs a x) (local.clock_trans aa aa)) \<and> rel_ext (\<lambda>y. \<exists>x. x \<in> Clock.jkbpC \<and> tLength x = Suc (tLength t) \<and> envObs a (tLast x) = envObs a s \<and> y = clock_sim x) = rel_ext (\<lambda>uu_. \<exists>sa. uu_ = (toSet (fst (clock_mkSuccs (envObs a) (envObs a s) (local.clock_trans aa aa))), sa) \<and> sa \<in> toSet (snd (clock_mkSuccs (envObs a) (envObs a s) (local.clock_trans aa aa))))
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>aa b t' s. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t)\<rbrakk> \<Longrightarrow> \<exists>x. (\<exists>t'. t' \<leadsto> x \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)) \<and> clock_mkSuccs (envObs a) (envObs a s) (local.clock_trans aa aa) = clock_mkSuccs (envObs a) (envObs a x) (local.clock_trans aa aa)
 2. \<And>aa b t' s aaa ba x. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); x \<in> Clock.jkbpC; tLength x = Suc (tLength t); envObs a (tLast x) = envObs a s; (aaa, ba) = clock_sim x\<rbrakk> \<Longrightarrow> \<exists>sa. (aaa, ba) = (toSet (fst (clock_mkSuccs (envObs a) (envObs a s) (local.clock_trans aa aa))), sa) \<and> sa \<in> toSet (snd (clock_mkSuccs (envObs a) (envObs a s) (local.clock_trans aa aa)))
 3. \<And>aa b t' s aaa ba sa. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); sa \<in> toSet (snd (clock_mkSuccs (envObs a) (envObs a s) (local.clock_trans aa aa)))\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> Clock.jkbpC \<and> tLength x = Suc (tLength t) \<and> envObs a (tLast x) = envObs a s \<and> (toSet (fst (clock_mkSuccs (envObs a) (envObs a s) (local.clock_trans aa aa))), sa) = clock_sim x
[PROOF STEP]
apply auto[1]
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa b t' s aaa ba x. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); x \<in> Clock.jkbpC; tLength x = Suc (tLength t); envObs a (tLast x) = envObs a s; (aaa, ba) = clock_sim x\<rbrakk> \<Longrightarrow> \<exists>sa. (aaa, ba) = (toSet (fst (clock_mkSuccs (envObs a) (envObs a s) (local.clock_trans aa aa))), sa) \<and> sa \<in> toSet (snd (clock_mkSuccs (envObs a) (envObs a s) (local.clock_trans aa aa)))
 2. \<And>aa b t' s aaa ba sa. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); sa \<in> toSet (snd (clock_mkSuccs (envObs a) (envObs a s) (local.clock_trans aa aa)))\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> Clock.jkbpC \<and> tLength x = Suc (tLength t) \<and> envObs a (tLast x) = envObs a s \<and> (toSet (fst (clock_mkSuccs (envObs a) (envObs a s) (local.clock_trans aa aa))), sa) = clock_sim x
[PROOF STEP]
apply (rule_tac x="tLast x" in exI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa b t' s aaa ba x. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); x \<in> Clock.jkbpC; tLength x = Suc (tLength t); envObs a (tLast x) = envObs a s; (aaa, ba) = clock_sim x\<rbrakk> \<Longrightarrow> (aaa, ba) = (toSet (fst (clock_mkSuccs (envObs a) (envObs a s) (local.clock_trans aa aa))), tLast x) \<and> tLast x \<in> toSet (snd (clock_mkSuccs (envObs a) (envObs a s) (local.clock_trans aa aa)))
 2. \<And>aa b t' s aaa ba sa. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); sa \<in> toSet (snd (clock_mkSuccs (envObs a) (envObs a s) (local.clock_trans aa aa)))\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> Clock.jkbpC \<and> tLength x = Suc (tLength t) \<and> envObs a (tLast x) = envObs a s \<and> (toSet (fst (clock_mkSuccs (envObs a) (envObs a s) (local.clock_trans aa aa))), sa) = clock_sim x
[PROOF STEP]
apply (clarsimp simp: clock_trans_common[OF tC ec] clock_mkSuccs_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa b t' s aaa ba x. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); x \<in> Clock.jkbpC; tLength x = Suc (tLength t); envObs a (tLast x) = envObs a s; (aaa, ba) = clock_sim x\<rbrakk> \<Longrightarrow> clock_sim x = (rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t), tLast x) \<and> (\<exists>t'. t' \<leadsto> tLast x \<in> Clock.jkbpC \<and> tLength t' = tLength t)
 2. \<And>aa b t' s aaa ba sa. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); sa \<in> toSet (snd (clock_mkSuccs (envObs a) (envObs a s) (local.clock_trans aa aa)))\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> Clock.jkbpC \<and> tLength x = Suc (tLength t) \<and> envObs a (tLast x) = envObs a s \<and> (toSet (fst (clock_mkSuccs (envObs a) (envObs a s) (local.clock_trans aa aa))), sa) = clock_sim x
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>aa b t' s aaa ba x. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); x \<in> Clock.jkbpC; tLength x = Suc (tLength t); envObs a (tLast x) = envObs a s; (aaa, ba) = clock_sim x\<rbrakk> \<Longrightarrow> clock_sim x = (rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t), tLast x)
 2. \<And>aa b t' s aaa ba x. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); x \<in> Clock.jkbpC; tLength x = Suc (tLength t); envObs a (tLast x) = envObs a s; (aaa, ba) = clock_sim x\<rbrakk> \<Longrightarrow> \<exists>t'. t' \<leadsto> tLast x \<in> Clock.jkbpC \<and> tLength t' = tLength t
 3. \<And>aa b t' s aaa ba sa. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); sa \<in> toSet (snd (clock_mkSuccs (envObs a) (envObs a s) (local.clock_trans aa aa)))\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> Clock.jkbpC \<and> tLength x = Suc (tLength t) \<and> envObs a (tLast x) = envObs a s \<and> (toSet (fst (clock_mkSuccs (envObs a) (envObs a s) (local.clock_trans aa aa))), sa) = clock_sim x
[PROOF STEP]
apply (clarsimp simp: clock_sim_def simp del: Clock.jkbpCn.simps)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>aa b t' s x. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); x \<in> Clock.jkbpC; tLength x = Suc (tLength t); envObs a (tLast x) = envObs a s\<rbrakk> \<Longrightarrow> tLast ` Clock.jkbpCn (Suc (tLength t)) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t)
 2. \<And>aa b t' s aaa ba x. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); x \<in> Clock.jkbpC; tLength x = Suc (tLength t); envObs a (tLast x) = envObs a s; (aaa, ba) = clock_sim x\<rbrakk> \<Longrightarrow> \<exists>t'. t' \<leadsto> tLast x \<in> Clock.jkbpC \<and> tLength t' = tLength t
 3. \<And>aa b t' s aaa ba sa. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); sa \<in> toSet (snd (clock_mkSuccs (envObs a) (envObs a s) (local.clock_trans aa aa)))\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> Clock.jkbpC \<and> tLength x = Suc (tLength t) \<and> envObs a (tLast x) = envObs a s \<and> (toSet (fst (clock_mkSuccs (envObs a) (envObs a s) (local.clock_trans aa aa))), sa) = clock_sim x
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>aa b t' s x. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); x \<in> Clock.jkbpC; tLength x = Suc (tLength t); envObs a (tLast x) = envObs a s\<rbrakk> \<Longrightarrow> tLast ` Clock.jkbpCn (Suc (tLength t)) \<subseteq> rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t)
 2. \<And>aa b t' s x. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); x \<in> Clock.jkbpC; tLength x = Suc (tLength t); envObs a (tLast x) = envObs a s\<rbrakk> \<Longrightarrow> rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t) \<subseteq> tLast ` Clock.jkbpCn (Suc (tLength t))
 3. \<And>aa b t' s aaa ba x. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); x \<in> Clock.jkbpC; tLength x = Suc (tLength t); envObs a (tLast x) = envObs a s; (aaa, ba) = clock_sim x\<rbrakk> \<Longrightarrow> \<exists>t'. t' \<leadsto> tLast x \<in> Clock.jkbpC \<and> tLength t' = tLength t
 4. \<And>aa b t' s aaa ba sa. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); sa \<in> toSet (snd (clock_mkSuccs (envObs a) (envObs a s) (local.clock_trans aa aa)))\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> Clock.jkbpC \<and> tLength x = Suc (tLength t) \<and> envObs a (tLast x) = envObs a s \<and> (toSet (fst (clock_mkSuccs (envObs a) (envObs a s) (local.clock_trans aa aa))), sa) = clock_sim x
[PROOF STEP]
apply (clarsimp simp: Let_def)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>aa b t' s x ta eact aact. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); x \<in> Clock.jkbpC; tLength x = Suc (tLength t); envObs a (tLast x) = envObs a s; ta \<in> Clock.jkbpCn (tLength t); eact \<in> set (envAction (tLast ta)); \<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t)) ta a)\<rbrakk> \<Longrightarrow> \<exists>t'. t' \<leadsto> envTrans eact aact (tLast ta) \<in> Clock.jkbpC \<and> tLength t' = tLength t
 2. \<And>aa b t' s x. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); x \<in> Clock.jkbpC; tLength x = Suc (tLength t); envObs a (tLast x) = envObs a s\<rbrakk> \<Longrightarrow> rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t) \<subseteq> tLast ` Clock.jkbpCn (Suc (tLength t))
 3. \<And>aa b t' s aaa ba x. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); x \<in> Clock.jkbpC; tLength x = Suc (tLength t); envObs a (tLast x) = envObs a s; (aaa, ba) = clock_sim x\<rbrakk> \<Longrightarrow> \<exists>t'. t' \<leadsto> tLast x \<in> Clock.jkbpC \<and> tLength t' = tLength t
 4. \<And>aa b t' s aaa ba sa. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); sa \<in> toSet (snd (clock_mkSuccs (envObs a) (envObs a s) (local.clock_trans aa aa)))\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> Clock.jkbpC \<and> tLength x = Suc (tLength t) \<and> envObs a (tLast x) = envObs a s \<and> (toSet (fst (clock_mkSuccs (envObs a) (envObs a s) (local.clock_trans aa aa))), sa) = clock_sim x
[PROOF STEP]
apply (rule_tac x="ta" in exI)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>aa b t' s x ta eact aact. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); x \<in> Clock.jkbpC; tLength x = Suc (tLength t); envObs a (tLast x) = envObs a s; ta \<in> Clock.jkbpCn (tLength t); eact \<in> set (envAction (tLast ta)); \<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t)) ta a)\<rbrakk> \<Longrightarrow> ta \<leadsto> envTrans eact aact (tLast ta) \<in> Clock.jkbpC \<and> tLength ta = tLength t
 2. \<And>aa b t' s x. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); x \<in> Clock.jkbpC; tLength x = Suc (tLength t); envObs a (tLast x) = envObs a s\<rbrakk> \<Longrightarrow> rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t) \<subseteq> tLast ` Clock.jkbpCn (Suc (tLength t))
 3. \<And>aa b t' s aaa ba x. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); x \<in> Clock.jkbpC; tLength x = Suc (tLength t); envObs a (tLast x) = envObs a s; (aaa, ba) = clock_sim x\<rbrakk> \<Longrightarrow> \<exists>t'. t' \<leadsto> tLast x \<in> Clock.jkbpC \<and> tLength t' = tLength t
 4. \<And>aa b t' s aaa ba sa. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); sa \<in> toSet (snd (clock_mkSuccs (envObs a) (envObs a s) (local.clock_trans aa aa)))\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> Clock.jkbpC \<and> tLength x = Suc (tLength t) \<and> envObs a (tLast x) = envObs a s \<and> (toSet (fst (clock_mkSuccs (envObs a) (envObs a s) (local.clock_trans aa aa))), sa) = clock_sim x
[PROOF STEP]
apply (simp add: Let_def)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>aa b t' s x ta eact aact. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); x \<in> Clock.jkbpC; tLength x = Suc (tLength t); envObs a (tLast x) = envObs a s; ta \<in> Clock.jkbpCn (tLength t); eact \<in> set (envAction (tLast ta)); \<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t)) ta a)\<rbrakk> \<Longrightarrow> ta \<leadsto> envTrans eact aact (tLast ta) \<in> Clock.jkbpC
 2. \<And>aa b t' s x. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); x \<in> Clock.jkbpC; tLength x = Suc (tLength t); envObs a (tLast x) = envObs a s\<rbrakk> \<Longrightarrow> rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t) \<subseteq> tLast ` Clock.jkbpCn (Suc (tLength t))
 3. \<And>aa b t' s aaa ba x. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); x \<in> Clock.jkbpC; tLength x = Suc (tLength t); envObs a (tLast x) = envObs a s; (aaa, ba) = clock_sim x\<rbrakk> \<Longrightarrow> \<exists>t'. t' \<leadsto> tLast x \<in> Clock.jkbpC \<and> tLength t' = tLength t
 4. \<And>aa b t' s aaa ba sa. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); sa \<in> toSet (snd (clock_mkSuccs (envObs a) (envObs a s) (local.clock_trans aa aa)))\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> Clock.jkbpC \<and> tLength x = Suc (tLength t) \<and> envObs a (tLast x) = envObs a s \<and> (toSet (fst (clock_mkSuccs (envObs a) (envObs a s) (local.clock_trans aa aa))), sa) = clock_sim x
[PROOF STEP]
apply (rule Clock.jkbpCn_jkbpC_inc[where n="Suc (tLength t)"])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>aa b t' s x ta eact aact. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); x \<in> Clock.jkbpC; tLength x = Suc (tLength t); envObs a (tLast x) = envObs a s; ta \<in> Clock.jkbpCn (tLength t); eact \<in> set (envAction (tLast ta)); \<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t)) ta a)\<rbrakk> \<Longrightarrow> ta \<leadsto> envTrans eact aact (tLast ta) \<in> Clock.jkbpCn (Suc (tLength t))
 2. \<And>aa b t' s x. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); x \<in> Clock.jkbpC; tLength x = Suc (tLength t); envObs a (tLast x) = envObs a s\<rbrakk> \<Longrightarrow> rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t) \<subseteq> tLast ` Clock.jkbpCn (Suc (tLength t))
 3. \<And>aa b t' s aaa ba x. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); x \<in> Clock.jkbpC; tLength x = Suc (tLength t); envObs a (tLast x) = envObs a s; (aaa, ba) = clock_sim x\<rbrakk> \<Longrightarrow> \<exists>t'. t' \<leadsto> tLast x \<in> Clock.jkbpC \<and> tLength t' = tLength t
 4. \<And>aa b t' s aaa ba sa. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); sa \<in> toSet (snd (clock_mkSuccs (envObs a) (envObs a s) (local.clock_trans aa aa)))\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> Clock.jkbpC \<and> tLength x = Suc (tLength t) \<and> envObs a (tLast x) = envObs a s \<and> (toSet (fst (clock_mkSuccs (envObs a) (envObs a s) (local.clock_trans aa aa))), sa) = clock_sim x
[PROOF STEP]
apply (clarsimp simp: Let_def)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>aa b t' s x ta eact aact. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); x \<in> Clock.jkbpC; tLength x = Suc (tLength t); envObs a (tLast x) = envObs a s; ta \<in> Clock.jkbpCn (tLength t); eact \<in> set (envAction (tLast ta)); \<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t)) ta a)\<rbrakk> \<Longrightarrow> \<exists>eacta aacta. envTrans eact aact (tLast ta) = envTrans eacta aacta (tLast ta) \<and> eacta \<in> set (envAction (tLast ta)) \<and> (\<forall>a. aacta a \<in> set (jAction (Clock.MCn (tLength t)) ta a))
 2. \<And>aa b t' s x. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); x \<in> Clock.jkbpC; tLength x = Suc (tLength t); envObs a (tLast x) = envObs a s\<rbrakk> \<Longrightarrow> rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t) \<subseteq> tLast ` Clock.jkbpCn (Suc (tLength t))
 3. \<And>aa b t' s aaa ba x. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); x \<in> Clock.jkbpC; tLength x = Suc (tLength t); envObs a (tLast x) = envObs a s; (aaa, ba) = clock_sim x\<rbrakk> \<Longrightarrow> \<exists>t'. t' \<leadsto> tLast x \<in> Clock.jkbpC \<and> tLength t' = tLength t
 4. \<And>aa b t' s aaa ba sa. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); sa \<in> toSet (snd (clock_mkSuccs (envObs a) (envObs a s) (local.clock_trans aa aa)))\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> Clock.jkbpC \<and> tLength x = Suc (tLength t) \<and> envObs a (tLast x) = envObs a s \<and> (toSet (fst (clock_mkSuccs (envObs a) (envObs a s) (local.clock_trans aa aa))), sa) = clock_sim x
[PROOF STEP]
apply (rule_tac x=eact in exI)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>aa b t' s x ta eact aact. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); x \<in> Clock.jkbpC; tLength x = Suc (tLength t); envObs a (tLast x) = envObs a s; ta \<in> Clock.jkbpCn (tLength t); eact \<in> set (envAction (tLast ta)); \<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t)) ta a)\<rbrakk> \<Longrightarrow> \<exists>aacta. envTrans eact aact (tLast ta) = envTrans eact aacta (tLast ta) \<and> eact \<in> set (envAction (tLast ta)) \<and> (\<forall>a. aacta a \<in> set (jAction (Clock.MCn (tLength t)) ta a))
 2. \<And>aa b t' s x. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); x \<in> Clock.jkbpC; tLength x = Suc (tLength t); envObs a (tLast x) = envObs a s\<rbrakk> \<Longrightarrow> rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t) \<subseteq> tLast ` Clock.jkbpCn (Suc (tLength t))
 3. \<And>aa b t' s aaa ba x. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); x \<in> Clock.jkbpC; tLength x = Suc (tLength t); envObs a (tLast x) = envObs a s; (aaa, ba) = clock_sim x\<rbrakk> \<Longrightarrow> \<exists>t'. t' \<leadsto> tLast x \<in> Clock.jkbpC \<and> tLength t' = tLength t
 4. \<And>aa b t' s aaa ba sa. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); sa \<in> toSet (snd (clock_mkSuccs (envObs a) (envObs a s) (local.clock_trans aa aa)))\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> Clock.jkbpC \<and> tLength x = Suc (tLength t) \<and> envObs a (tLast x) = envObs a s \<and> (toSet (fst (clock_mkSuccs (envObs a) (envObs a s) (local.clock_trans aa aa))), sa) = clock_sim x
[PROOF STEP]
apply (rule_tac x=aact in exI)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>aa b t' s x ta eact aact. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); x \<in> Clock.jkbpC; tLength x = Suc (tLength t); envObs a (tLast x) = envObs a s; ta \<in> Clock.jkbpCn (tLength t); eact \<in> set (envAction (tLast ta)); \<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t)) ta a)\<rbrakk> \<Longrightarrow> envTrans eact aact (tLast ta) = envTrans eact aact (tLast ta) \<and> eact \<in> set (envAction (tLast ta)) \<and> (\<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t)) ta a))
 2. \<And>aa b t' s x. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); x \<in> Clock.jkbpC; tLength x = Suc (tLength t); envObs a (tLast x) = envObs a s\<rbrakk> \<Longrightarrow> rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t) \<subseteq> tLast ` Clock.jkbpCn (Suc (tLength t))
 3. \<And>aa b t' s aaa ba x. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); x \<in> Clock.jkbpC; tLength x = Suc (tLength t); envObs a (tLast x) = envObs a s; (aaa, ba) = clock_sim x\<rbrakk> \<Longrightarrow> \<exists>t'. t' \<leadsto> tLast x \<in> Clock.jkbpC \<and> tLength t' = tLength t
 4. \<And>aa b t' s aaa ba sa. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); sa \<in> toSet (snd (clock_mkSuccs (envObs a) (envObs a s) (local.clock_trans aa aa)))\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> Clock.jkbpC \<and> tLength x = Suc (tLength t) \<and> envObs a (tLast x) = envObs a s \<and> (toSet (fst (clock_mkSuccs (envObs a) (envObs a s) (local.clock_trans aa aa))), sa) = clock_sim x
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>aa b t' s x. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); x \<in> Clock.jkbpC; tLength x = Suc (tLength t); envObs a (tLast x) = envObs a s\<rbrakk> \<Longrightarrow> rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t) \<subseteq> tLast ` Clock.jkbpCn (Suc (tLength t))
 2. \<And>aa b t' s aaa ba x. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); x \<in> Clock.jkbpC; tLength x = Suc (tLength t); envObs a (tLast x) = envObs a s; (aaa, ba) = clock_sim x\<rbrakk> \<Longrightarrow> \<exists>t'. t' \<leadsto> tLast x \<in> Clock.jkbpC \<and> tLength t' = tLength t
 3. \<And>aa b t' s aaa ba sa. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); sa \<in> toSet (snd (clock_mkSuccs (envObs a) (envObs a s) (local.clock_trans aa aa)))\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> Clock.jkbpC \<and> tLength x = Suc (tLength t) \<and> envObs a (tLast x) = envObs a s \<and> (toSet (fst (clock_mkSuccs (envObs a) (envObs a s) (local.clock_trans aa aa))), sa) = clock_sim x
[PROOF STEP]
apply (clarsimp simp: Let_def Set.image_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>aa b t' s x xa t'a. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); x \<in> Clock.jkbpC; tLength x = Suc (tLength t); envObs a (tLast x) = envObs a s; t'a \<leadsto> xa \<in> Clock.jkbpC; tLength t'a = tLength t\<rbrakk> \<Longrightarrow> \<exists>x. (\<exists>ta eact aact. x = ta \<leadsto> envTrans eact aact (tLast ta) \<and> ta \<in> Clock.jkbpCn (tLength t) \<and> eact \<in> set (envAction (tLast ta)) \<and> (\<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t)) ta a))) \<and> xa = tLast x
 2. \<And>aa b t' s aaa ba x. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); x \<in> Clock.jkbpC; tLength x = Suc (tLength t); envObs a (tLast x) = envObs a s; (aaa, ba) = clock_sim x\<rbrakk> \<Longrightarrow> \<exists>t'. t' \<leadsto> tLast x \<in> Clock.jkbpC \<and> tLength t' = tLength t
 3. \<And>aa b t' s aaa ba sa. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); sa \<in> toSet (snd (clock_mkSuccs (envObs a) (envObs a s) (local.clock_trans aa aa)))\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> Clock.jkbpC \<and> tLength x = Suc (tLength t) \<and> envObs a (tLast x) = envObs a s \<and> (toSet (fst (clock_mkSuccs (envObs a) (envObs a s) (local.clock_trans aa aa))), sa) = clock_sim x
[PROOF STEP]
apply (drule_tac t="t'a \<leadsto> xa" in Clock.jkbpC_tLength_inv[OF _ refl])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>aa b t' s x xa t'a. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); x \<in> Clock.jkbpC; tLength x = Suc (tLength t); envObs a (tLast x) = envObs a s; tLength t'a = tLength t; t'a \<leadsto> xa \<in> Clock.jkbpCn (tLength (t'a \<leadsto> xa))\<rbrakk> \<Longrightarrow> \<exists>x. (\<exists>ta eact aact. x = ta \<leadsto> envTrans eact aact (tLast ta) \<and> ta \<in> Clock.jkbpCn (tLength t) \<and> eact \<in> set (envAction (tLast ta)) \<and> (\<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t)) ta a))) \<and> xa = tLast x
 2. \<And>aa b t' s aaa ba x. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); x \<in> Clock.jkbpC; tLength x = Suc (tLength t); envObs a (tLast x) = envObs a s; (aaa, ba) = clock_sim x\<rbrakk> \<Longrightarrow> \<exists>t'. t' \<leadsto> tLast x \<in> Clock.jkbpC \<and> tLength t' = tLength t
 3. \<And>aa b t' s aaa ba sa. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); sa \<in> toSet (snd (clock_mkSuccs (envObs a) (envObs a s) (local.clock_trans aa aa)))\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> Clock.jkbpC \<and> tLength x = Suc (tLength t) \<and> envObs a (tLast x) = envObs a s \<and> (toSet (fst (clock_mkSuccs (envObs a) (envObs a s) (local.clock_trans aa aa))), sa) = clock_sim x
[PROOF STEP]
apply (rule_tac x="t'a \<leadsto> xa" in exI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>aa b t' s x xa t'a. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); x \<in> Clock.jkbpC; tLength x = Suc (tLength t); envObs a (tLast x) = envObs a s; tLength t'a = tLength t; t'a \<leadsto> xa \<in> Clock.jkbpCn (tLength (t'a \<leadsto> xa))\<rbrakk> \<Longrightarrow> (\<exists>ta eact aact. t'a \<leadsto> xa = ta \<leadsto> envTrans eact aact (tLast ta) \<and> ta \<in> Clock.jkbpCn (tLength t) \<and> eact \<in> set (envAction (tLast ta)) \<and> (\<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t)) ta a))) \<and> xa = tLast (t'a \<leadsto> xa)
 2. \<And>aa b t' s aaa ba x. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); x \<in> Clock.jkbpC; tLength x = Suc (tLength t); envObs a (tLast x) = envObs a s; (aaa, ba) = clock_sim x\<rbrakk> \<Longrightarrow> \<exists>t'. t' \<leadsto> tLast x \<in> Clock.jkbpC \<and> tLength t' = tLength t
 3. \<And>aa b t' s aaa ba sa. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); sa \<in> toSet (snd (clock_mkSuccs (envObs a) (envObs a s) (local.clock_trans aa aa)))\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> Clock.jkbpC \<and> tLength x = Suc (tLength t) \<and> envObs a (tLast x) = envObs a s \<and> (toSet (fst (clock_mkSuccs (envObs a) (envObs a s) (local.clock_trans aa aa))), sa) = clock_sim x
[PROOF STEP]
apply (auto simp: Let_def)[1]
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa b t' s aaa ba x. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); x \<in> Clock.jkbpC; tLength x = Suc (tLength t); envObs a (tLast x) = envObs a s; (aaa, ba) = clock_sim x\<rbrakk> \<Longrightarrow> \<exists>t'. t' \<leadsto> tLast x \<in> Clock.jkbpC \<and> tLength t' = tLength t
 2. \<And>aa b t' s aaa ba sa. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); sa \<in> toSet (snd (clock_mkSuccs (envObs a) (envObs a s) (local.clock_trans aa aa)))\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> Clock.jkbpC \<and> tLength x = Suc (tLength t) \<and> envObs a (tLast x) = envObs a s \<and> (toSet (fst (clock_mkSuccs (envObs a) (envObs a s) (local.clock_trans aa aa))), sa) = clock_sim x
[PROOF STEP]
apply (drule_tac t="x" in Clock.jkbpC_tLength_inv[OF _ refl])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa b t' s aaa ba x. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); tLength x = Suc (tLength t); envObs a (tLast x) = envObs a s; (aaa, ba) = clock_sim x; x \<in> Clock.jkbpCn (tLength x)\<rbrakk> \<Longrightarrow> \<exists>t'. t' \<leadsto> tLast x \<in> Clock.jkbpC \<and> tLength t' = tLength t
 2. \<And>aa b t' s aaa ba sa. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); sa \<in> toSet (snd (clock_mkSuccs (envObs a) (envObs a s) (local.clock_trans aa aa)))\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> Clock.jkbpC \<and> tLength x = Suc (tLength t) \<and> envObs a (tLast x) = envObs a s \<and> (toSet (fst (clock_mkSuccs (envObs a) (envObs a s) (local.clock_trans aa aa))), sa) = clock_sim x
[PROOF STEP]
apply (simp only: Let_def Clock.jkbpCn.simps)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa b t' s aaa ba x. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); tLength x = Suc (tLength t); envObs a (tLast x) = envObs a s; (aaa, ba) = clock_sim x; x \<in> rel_ext (\<lambda>uu_. \<exists>ta eact aact. uu_ = ta \<leadsto> envTrans eact aact (tLast ta) \<and> ta \<in> Clock.jkbpCn (tLength t) \<and> eact \<in> set (envAction (tLast ta)) \<and> (\<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t)) ta a)))\<rbrakk> \<Longrightarrow> \<exists>t'. t' \<leadsto> tLast x \<in> Clock.jkbpC \<and> tLength t' = tLength t
 2. \<And>aa b t' s aaa ba sa. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); sa \<in> toSet (snd (clock_mkSuccs (envObs a) (envObs a s) (local.clock_trans aa aa)))\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> Clock.jkbpC \<and> tLength x = Suc (tLength t) \<and> envObs a (tLast x) = envObs a s \<and> (toSet (fst (clock_mkSuccs (envObs a) (envObs a s) (local.clock_trans aa aa))), sa) = clock_sim x
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa b t' s aaa ba x ta eact aact. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); tLength (ta \<leadsto> envTrans eact aact (tLast ta)) = Suc (tLength t); envObs a (tLast (ta \<leadsto> envTrans eact aact (tLast ta))) = envObs a s; (aaa, ba) = clock_sim (ta \<leadsto> envTrans eact aact (tLast ta)); ta \<in> Clock.jkbpCn (tLength t); eact \<in> set (envAction (tLast ta)); \<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t)) ta a)\<rbrakk> \<Longrightarrow> \<exists>t'. t' \<leadsto> tLast (ta \<leadsto> envTrans eact aact (tLast ta)) \<in> Clock.jkbpC \<and> tLength t' = tLength t
 2. \<And>aa b t' s aaa ba sa. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); sa \<in> toSet (snd (clock_mkSuccs (envObs a) (envObs a s) (local.clock_trans aa aa)))\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> Clock.jkbpC \<and> tLength x = Suc (tLength t) \<and> envObs a (tLast x) = envObs a s \<and> (toSet (fst (clock_mkSuccs (envObs a) (envObs a s) (local.clock_trans aa aa))), sa) = clock_sim x
[PROOF STEP]
apply (rule_tac x="ta" in exI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa b t' s aaa ba x ta eact aact. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); tLength (ta \<leadsto> envTrans eact aact (tLast ta)) = Suc (tLength t); envObs a (tLast (ta \<leadsto> envTrans eact aact (tLast ta))) = envObs a s; (aaa, ba) = clock_sim (ta \<leadsto> envTrans eact aact (tLast ta)); ta \<in> Clock.jkbpCn (tLength t); eact \<in> set (envAction (tLast ta)); \<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t)) ta a)\<rbrakk> \<Longrightarrow> ta \<leadsto> tLast (ta \<leadsto> envTrans eact aact (tLast ta)) \<in> Clock.jkbpC \<and> tLength ta = tLength t
 2. \<And>aa b t' s aaa ba sa. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); sa \<in> toSet (snd (clock_mkSuccs (envObs a) (envObs a s) (local.clock_trans aa aa)))\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> Clock.jkbpC \<and> tLength x = Suc (tLength t) \<and> envObs a (tLast x) = envObs a s \<and> (toSet (fst (clock_mkSuccs (envObs a) (envObs a s) (local.clock_trans aa aa))), sa) = clock_sim x
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa b t' s aaa ba ta eact aact. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); envObs a (envTrans eact aact (tLast ta)) = envObs a s; (aaa, ba) = clock_sim (ta \<leadsto> envTrans eact aact (tLast ta)); ta \<in> Clock.jkbpCn (tLength t); eact \<in> set (envAction (tLast ta)); \<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t)) ta a)\<rbrakk> \<Longrightarrow> ta \<leadsto> envTrans eact aact (tLast ta) \<in> Clock.jkbpC
 2. \<And>aa b t' s aaa ba sa. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); sa \<in> toSet (snd (clock_mkSuccs (envObs a) (envObs a s) (local.clock_trans aa aa)))\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> Clock.jkbpC \<and> tLength x = Suc (tLength t) \<and> envObs a (tLast x) = envObs a s \<and> (toSet (fst (clock_mkSuccs (envObs a) (envObs a s) (local.clock_trans aa aa))), sa) = clock_sim x
[PROOF STEP]
apply (rule Clock.jkbpCn_jkbpC_inc[where n="Suc (tLength t)"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa b t' s aaa ba ta eact aact. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); envObs a (envTrans eact aact (tLast ta)) = envObs a s; (aaa, ba) = clock_sim (ta \<leadsto> envTrans eact aact (tLast ta)); ta \<in> Clock.jkbpCn (tLength t); eact \<in> set (envAction (tLast ta)); \<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t)) ta a)\<rbrakk> \<Longrightarrow> ta \<leadsto> envTrans eact aact (tLast ta) \<in> Clock.jkbpCn (Suc (tLength t))
 2. \<And>aa b t' s aaa ba sa. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); sa \<in> toSet (snd (clock_mkSuccs (envObs a) (envObs a s) (local.clock_trans aa aa)))\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> Clock.jkbpC \<and> tLength x = Suc (tLength t) \<and> envObs a (tLast x) = envObs a s \<and> (toSet (fst (clock_mkSuccs (envObs a) (envObs a s) (local.clock_trans aa aa))), sa) = clock_sim x
[PROOF STEP]
apply (auto simp: Let_def)[1]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa b t' s aaa ba sa. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); sa \<in> toSet (snd (clock_mkSuccs (envObs a) (envObs a s) (local.clock_trans aa aa)))\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> Clock.jkbpC \<and> tLength x = Suc (tLength t) \<and> envObs a (tLast x) = envObs a s \<and> (toSet (fst (clock_mkSuccs (envObs a) (envObs a s) (local.clock_trans aa aa))), sa) = clock_sim x
[PROOF STEP]
apply (clarsimp simp: clock_trans_common[OF tC ec] clock_mkSuccs_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa b t' s sa t'a. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); envObs a sa = envObs a s; t'a \<leadsto> sa \<in> Clock.jkbpC; tLength t'a = tLength t\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> Clock.jkbpC \<and> tLength x = Suc (tLength t) \<and> envObs a (tLast x) = envObs a s \<and> (rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t), sa) = clock_sim x
[PROOF STEP]
apply (rule_tac x="t'a \<leadsto> sa" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa b t' s sa t'a. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); envObs a sa = envObs a s; t'a \<leadsto> sa \<in> Clock.jkbpC; tLength t'a = tLength t\<rbrakk> \<Longrightarrow> t'a \<leadsto> sa \<in> Clock.jkbpC \<and> tLength (t'a \<leadsto> sa) = Suc (tLength t) \<and> envObs a (tLast (t'a \<leadsto> sa)) = envObs a s \<and> (rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t), sa) = clock_sim (t'a \<leadsto> sa)
[PROOF STEP]
apply (clarsimp simp: clock_sim_def Let_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa b t' s sa t'a. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); envObs a sa = envObs a s; t'a \<leadsto> sa \<in> Clock.jkbpC; tLength t'a = tLength t\<rbrakk> \<Longrightarrow> rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t) = tLast ` rel_ext (\<lambda>uu_. \<exists>ta eact aact. uu_ = ta \<leadsto> envTrans eact aact (tLast ta) \<and> ta \<in> Clock.jkbpCn (tLength t) \<and> eact \<in> set (envAction (tLast ta)) \<and> (\<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t)) ta a)))
[PROOF STEP]
(* FIXME similar to above *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa b t' s sa t'a. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); envObs a sa = envObs a s; t'a \<leadsto> sa \<in> Clock.jkbpC; tLength t'a = tLength t\<rbrakk> \<Longrightarrow> rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t) = tLast ` rel_ext (\<lambda>uu_. \<exists>ta eact aact. uu_ = ta \<leadsto> envTrans eact aact (tLast ta) \<and> ta \<in> Clock.jkbpCn (tLength t) \<and> eact \<in> set (envAction (tLast ta)) \<and> (\<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t)) ta a)))
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa b t' s sa t'a. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); envObs a sa = envObs a s; t'a \<leadsto> sa \<in> Clock.jkbpC; tLength t'a = tLength t\<rbrakk> \<Longrightarrow> rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t) \<subseteq> tLast ` rel_ext (\<lambda>uu_. \<exists>ta eact aact. uu_ = ta \<leadsto> envTrans eact aact (tLast ta) \<and> ta \<in> Clock.jkbpCn (tLength t) \<and> eact \<in> set (envAction (tLast ta)) \<and> (\<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t)) ta a)))
 2. \<And>aa b t' s sa t'a. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); envObs a sa = envObs a s; t'a \<leadsto> sa \<in> Clock.jkbpC; tLength t'a = tLength t\<rbrakk> \<Longrightarrow> tLast ` rel_ext (\<lambda>uu_. \<exists>ta eact aact. uu_ = ta \<leadsto> envTrans eact aact (tLast ta) \<and> ta \<in> Clock.jkbpCn (tLength t) \<and> eact \<in> set (envAction (tLast ta)) \<and> (\<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t)) ta a))) \<subseteq> rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t)
[PROOF STEP]
apply (clarsimp simp: Set.image_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa b t' s sa t'a x t'b. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); envObs a sa = envObs a s; t'a \<leadsto> sa \<in> Clock.jkbpC; tLength t'a = tLength t; t'b \<leadsto> x \<in> Clock.jkbpC; tLength t'b = tLength t\<rbrakk> \<Longrightarrow> \<exists>xa. (\<exists>ta eact aact. xa = ta \<leadsto> envTrans eact aact (tLast ta) \<and> ta \<in> Clock.jkbpCn (tLength t) \<and> eact \<in> set (envAction (tLast ta)) \<and> (\<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t)) ta a))) \<and> x = tLast xa
 2. \<And>aa b t' s sa t'a. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); envObs a sa = envObs a s; t'a \<leadsto> sa \<in> Clock.jkbpC; tLength t'a = tLength t\<rbrakk> \<Longrightarrow> tLast ` rel_ext (\<lambda>uu_. \<exists>ta eact aact. uu_ = ta \<leadsto> envTrans eact aact (tLast ta) \<and> ta \<in> Clock.jkbpCn (tLength t) \<and> eact \<in> set (envAction (tLast ta)) \<and> (\<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t)) ta a))) \<subseteq> rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t)
[PROOF STEP]
apply (rule_tac x="t'b \<leadsto> x" in exI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa b t' s sa t'a x t'b. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); envObs a sa = envObs a s; t'a \<leadsto> sa \<in> Clock.jkbpC; tLength t'a = tLength t; t'b \<leadsto> x \<in> Clock.jkbpC; tLength t'b = tLength t\<rbrakk> \<Longrightarrow> (\<exists>ta eact aact. t'b \<leadsto> x = ta \<leadsto> envTrans eact aact (tLast ta) \<and> ta \<in> Clock.jkbpCn (tLength t) \<and> eact \<in> set (envAction (tLast ta)) \<and> (\<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t)) ta a))) \<and> x = tLast (t'b \<leadsto> x)
 2. \<And>aa b t' s sa t'a. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); envObs a sa = envObs a s; t'a \<leadsto> sa \<in> Clock.jkbpC; tLength t'a = tLength t\<rbrakk> \<Longrightarrow> tLast ` rel_ext (\<lambda>uu_. \<exists>ta eact aact. uu_ = ta \<leadsto> envTrans eact aact (tLast ta) \<and> ta \<in> Clock.jkbpCn (tLength t) \<and> eact \<in> set (envAction (tLast ta)) \<and> (\<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t)) ta a))) \<subseteq> rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t)
[PROOF STEP]
apply (drule_tac t="t'b \<leadsto> x" in Clock.jkbpC_tLength_inv[OF _ refl])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa b t' s sa t'a x t'b. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); envObs a sa = envObs a s; t'a \<leadsto> sa \<in> Clock.jkbpC; tLength t'a = tLength t; tLength t'b = tLength t; t'b \<leadsto> x \<in> Clock.jkbpCn (tLength (t'b \<leadsto> x))\<rbrakk> \<Longrightarrow> (\<exists>ta eact aact. t'b \<leadsto> x = ta \<leadsto> envTrans eact aact (tLast ta) \<and> ta \<in> Clock.jkbpCn (tLength t) \<and> eact \<in> set (envAction (tLast ta)) \<and> (\<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t)) ta a))) \<and> x = tLast (t'b \<leadsto> x)
 2. \<And>aa b t' s sa t'a. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); envObs a sa = envObs a s; t'a \<leadsto> sa \<in> Clock.jkbpC; tLength t'a = tLength t\<rbrakk> \<Longrightarrow> tLast ` rel_ext (\<lambda>uu_. \<exists>ta eact aact. uu_ = ta \<leadsto> envTrans eact aact (tLast ta) \<and> ta \<in> Clock.jkbpCn (tLength t) \<and> eact \<in> set (envAction (tLast ta)) \<and> (\<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t)) ta a))) \<subseteq> rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t)
[PROOF STEP]
apply (auto simp: Let_def)[1]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa b t' s sa t'a. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); envObs a sa = envObs a s; t'a \<leadsto> sa \<in> Clock.jkbpC; tLength t'a = tLength t\<rbrakk> \<Longrightarrow> tLast ` rel_ext (\<lambda>uu_. \<exists>ta eact aact. uu_ = ta \<leadsto> envTrans eact aact (tLast ta) \<and> ta \<in> Clock.jkbpCn (tLength t) \<and> eact \<in> set (envAction (tLast ta)) \<and> (\<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t)) ta a))) \<subseteq> rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t)
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa b t' s sa t'a ta eact aact. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); envObs a sa = envObs a s; t'a \<leadsto> sa \<in> Clock.jkbpC; tLength t'a = tLength t; ta \<in> Clock.jkbpCn (tLength t); eact \<in> set (envAction (tLast ta)); \<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t)) ta a)\<rbrakk> \<Longrightarrow> \<exists>t'. t' \<leadsto> envTrans eact aact (tLast ta) \<in> Clock.jkbpC \<and> tLength t' = tLength t
[PROOF STEP]
apply (rule_tac x="ta" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa b t' s sa t'a ta eact aact. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); envObs a sa = envObs a s; t'a \<leadsto> sa \<in> Clock.jkbpC; tLength t'a = tLength t; ta \<in> Clock.jkbpCn (tLength t); eact \<in> set (envAction (tLast ta)); \<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t)) ta a)\<rbrakk> \<Longrightarrow> ta \<leadsto> envTrans eact aact (tLast ta) \<in> Clock.jkbpC \<and> tLength ta = tLength t
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa b t' s sa t'a ta eact aact. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); envObs a sa = envObs a s; t'a \<leadsto> sa \<in> Clock.jkbpC; tLength t'a = tLength t; ta \<in> Clock.jkbpCn (tLength t); eact \<in> set (envAction (tLast ta)); \<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t)) ta a)\<rbrakk> \<Longrightarrow> ta \<leadsto> envTrans eact aact (tLast ta) \<in> Clock.jkbpC
[PROOF STEP]
apply (rule Clock.jkbpCn_jkbpC_inc[where n="Suc (tLength t)"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa b t' s sa t'a ta eact aact. \<lbrakk>ec = (aa, b); toSet (local.clock_trans aa aa) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t); toSet (local.clock_trans aa b) = rel_ext (\<lambda>uu_. \<exists>t'. t' \<leadsto> uu_ \<in> Clock.jkbpC \<and> tLength t' = tLength t \<and> envObs a (tLast t') = envObs a (tLast t)); t' \<leadsto> s \<in> Clock.jkbpC; tLength t' = tLength t; envObs a (tLast t') = envObs a (tLast t); envObs a sa = envObs a s; t'a \<leadsto> sa \<in> Clock.jkbpC; tLength t'a = tLength t; ta \<in> Clock.jkbpCn (tLength t); eact \<in> set (envAction (tLast ta)); \<forall>a. aact a \<in> set (jAction (Clock.MCn (tLength t)) ta a)\<rbrakk> \<Longrightarrow> ta \<leadsto> envTrans eact aact (tLast ta) \<in> Clock.jkbpCn (Suc (tLength t))
[PROOF STEP]
apply (auto simp: Let_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
rel_ext (\<lambda>uu_. \<exists>t' s. uu_ = Clock.sim_equiv_class a (t' \<leadsto> s) \<and> t' \<leadsto> s \<in> Clock.jkbpC \<and> clock_jview a t' = clock_jview a t) \<subseteq> clock_simAbs ` set (local.clock_simTrans a ec)

goal:
No subgoals!
[PROOF STEP]
qed