[STATEMENT]
lemma disjoint: "(res ts c) \<sqinter> (clm ts c) = \<emptyset>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. res ts c \<sqinter> clm ts c = bot
[PROOF STEP]
using Rep_traffic res_def clm_def
[PROOF STATE]
proof (prove)
using this:
Rep_traffic ?x \<in> {ts. (\<forall>c. fst (snd ts) c \<sqinter> fst (snd (snd ts)) c = bot) \<and> (\<forall>c. 1 \<le> |fst (snd ts) c|) \<and> (\<forall>c. |fst (snd ts) c| \<le> 2) \<and> (\<forall>c. |fst (snd (snd ts)) c| \<le> 1) \<and> (\<forall>c. |fst (snd ts) c| + |fst (snd (snd ts)) c| \<le> 2) \<and> (\<forall>c. fst (snd (snd ts)) c \<noteq> bot \<longrightarrow> (\<exists>n. Rep_nat_int (fst (snd ts) c) \<union> Rep_nat_int (fst (snd (snd ts)) c) = {n, n + 1})) \<and> (\<forall>c. 0 < fst (snd (snd (snd (snd ts)))) c) \<and> (\<forall>c. 0 < snd (snd (snd (snd (snd ts)))) c)}
res ?ts \<equiv> fst (snd (Rep_traffic ?ts))
clm ?ts \<equiv> fst (snd (snd (Rep_traffic ?ts)))

goal (1 subgoal):
 1. res ts c \<sqinter> clm ts c = bot
[PROOF STEP]
by auto


[STATEMENT]
lemma atLeastOneRes: "1 \<le> |res ts c|"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<le> |res ts c|
[PROOF STEP]
using Rep_traffic  res_def
[PROOF STATE]
proof (prove)
using this:
Rep_traffic ?x \<in> {ts. (\<forall>c. fst (snd ts) c \<sqinter> fst (snd (snd ts)) c = bot) \<and> (\<forall>c. 1 \<le> |fst (snd ts) c|) \<and> (\<forall>c. |fst (snd ts) c| \<le> 2) \<and> (\<forall>c. |fst (snd (snd ts)) c| \<le> 1) \<and> (\<forall>c. |fst (snd ts) c| + |fst (snd (snd ts)) c| \<le> 2) \<and> (\<forall>c. fst (snd (snd ts)) c \<noteq> bot \<longrightarrow> (\<exists>n. Rep_nat_int (fst (snd ts) c) \<union> Rep_nat_int (fst (snd (snd ts)) c) = {n, n + 1})) \<and> (\<forall>c. 0 < fst (snd (snd (snd (snd ts)))) c) \<and> (\<forall>c. 0 < snd (snd (snd (snd (snd ts)))) c)}
res ?ts \<equiv> fst (snd (Rep_traffic ?ts))

goal (1 subgoal):
 1. 1 \<le> |res ts c|
[PROOF STEP]
by auto


[STATEMENT]
lemma atMostTwoRes:" |res ts c| \<le> 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. |res ts c| \<le> 2
[PROOF STEP]
using Rep_traffic  res_def
[PROOF STATE]
proof (prove)
using this:
Rep_traffic ?x \<in> {ts. (\<forall>c. fst (snd ts) c \<sqinter> fst (snd (snd ts)) c = bot) \<and> (\<forall>c. 1 \<le> |fst (snd ts) c|) \<and> (\<forall>c. |fst (snd ts) c| \<le> 2) \<and> (\<forall>c. |fst (snd (snd ts)) c| \<le> 1) \<and> (\<forall>c. |fst (snd ts) c| + |fst (snd (snd ts)) c| \<le> 2) \<and> (\<forall>c. fst (snd (snd ts)) c \<noteq> bot \<longrightarrow> (\<exists>n. Rep_nat_int (fst (snd ts) c) \<union> Rep_nat_int (fst (snd (snd ts)) c) = {n, n + 1})) \<and> (\<forall>c. 0 < fst (snd (snd (snd (snd ts)))) c) \<and> (\<forall>c. 0 < snd (snd (snd (snd (snd ts)))) c)}
res ?ts \<equiv> fst (snd (Rep_traffic ?ts))

goal (1 subgoal):
 1. |res ts c| \<le> 2
[PROOF STEP]
by auto


[STATEMENT]
lemma  atMostOneClm: "|clm ts c| \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. |clm ts c| \<le> 1
[PROOF STEP]
using Rep_traffic  clm_def
[PROOF STATE]
proof (prove)
using this:
Rep_traffic ?x \<in> {ts. (\<forall>c. fst (snd ts) c \<sqinter> fst (snd (snd ts)) c = bot) \<and> (\<forall>c. 1 \<le> |fst (snd ts) c|) \<and> (\<forall>c. |fst (snd ts) c| \<le> 2) \<and> (\<forall>c. |fst (snd (snd ts)) c| \<le> 1) \<and> (\<forall>c. |fst (snd ts) c| + |fst (snd (snd ts)) c| \<le> 2) \<and> (\<forall>c. fst (snd (snd ts)) c \<noteq> bot \<longrightarrow> (\<exists>n. Rep_nat_int (fst (snd ts) c) \<union> Rep_nat_int (fst (snd (snd ts)) c) = {n, n + 1})) \<and> (\<forall>c. 0 < fst (snd (snd (snd (snd ts)))) c) \<and> (\<forall>c. 0 < snd (snd (snd (snd (snd ts)))) c)}
clm ?ts \<equiv> fst (snd (snd (Rep_traffic ?ts)))

goal (1 subgoal):
 1. |clm ts c| \<le> 1
[PROOF STEP]
by auto


[STATEMENT]
lemma atMostTwoLanes: "|res ts c| +|clm ts c| \<le> 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. |res ts c| + |clm ts c| \<le> 2
[PROOF STEP]
using Rep_traffic  res_def clm_def
[PROOF STATE]
proof (prove)
using this:
Rep_traffic ?x \<in> {ts. (\<forall>c. fst (snd ts) c \<sqinter> fst (snd (snd ts)) c = bot) \<and> (\<forall>c. 1 \<le> |fst (snd ts) c|) \<and> (\<forall>c. |fst (snd ts) c| \<le> 2) \<and> (\<forall>c. |fst (snd (snd ts)) c| \<le> 1) \<and> (\<forall>c. |fst (snd ts) c| + |fst (snd (snd ts)) c| \<le> 2) \<and> (\<forall>c. fst (snd (snd ts)) c \<noteq> bot \<longrightarrow> (\<exists>n. Rep_nat_int (fst (snd ts) c) \<union> Rep_nat_int (fst (snd (snd ts)) c) = {n, n + 1})) \<and> (\<forall>c. 0 < fst (snd (snd (snd (snd ts)))) c) \<and> (\<forall>c. 0 < snd (snd (snd (snd (snd ts)))) c)}
res ?ts \<equiv> fst (snd (Rep_traffic ?ts))
clm ?ts \<equiv> fst (snd (snd (Rep_traffic ?ts)))

goal (1 subgoal):
 1. |res ts c| + |clm ts c| \<le> 2
[PROOF STEP]
by auto


[STATEMENT]
lemma  consecutiveRes:" |res ts  c| =2 \<longrightarrow> (\<exists>n . Rep_nat_int (res ts c) = {n,n+1})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. |res ts c| = 2 \<longrightarrow> (\<exists>n. Rep_nat_int (res ts c) = {n, n + 1})
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. |res ts c| = 2 \<Longrightarrow> \<exists>n. Rep_nat_int (res ts c) = {n, n + 1}
[PROOF STEP]
assume assump:"|res ts  c| =2"
[PROOF STATE]
proof (state)
this:
|res ts c| = 2

goal (1 subgoal):
 1. |res ts c| = 2 \<Longrightarrow> \<exists>n. Rep_nat_int (res ts c) = {n, n + 1}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
|res ts c| = 2
[PROOF STEP]
have not_empty:"(res ts c) \<noteq> \<emptyset>"
[PROOF STATE]
proof (prove)
using this:
|res ts c| = 2

goal (1 subgoal):
 1. res ts c \<noteq> bot
[PROOF STEP]
by (simp add: card_non_empty_geq_one)
[PROOF STATE]
proof (state)
this:
res ts c \<noteq> bot

goal (1 subgoal):
 1. |res ts c| = 2 \<Longrightarrow> \<exists>n. Rep_nat_int (res ts c) = {n, n + 1}
[PROOF STEP]
from assump and card_seq
[PROOF STATE]
proof (chain)
picking this:
|res ts c| = 2
\<forall>i. |i| = ?x \<longrightarrow> Rep_nat_int i = {} \<or> (\<exists>n. Rep_nat_int i = {n..n + (?x - 1)})
[PROOF STEP]
have "Rep_nat_int (res ts  c) = {} \<or> (\<exists>n . Rep_nat_int (res ts c) = {n,n+1})"
[PROOF STATE]
proof (prove)
using this:
|res ts c| = 2
\<forall>i. |i| = ?x \<longrightarrow> Rep_nat_int i = {} \<or> (\<exists>n. Rep_nat_int i = {n..n + (?x - 1)})

goal (1 subgoal):
 1. Rep_nat_int (res ts c) = {} \<or> (\<exists>n. Rep_nat_int (res ts c) = {n, n + 1})
[PROOF STEP]
by (metis add_diff_cancel_left' atLeastAtMost_singleton insert_is_Un nat_int.un_consec_seq
        one_add_one order_refl)
[PROOF STATE]
proof (state)
this:
Rep_nat_int (res ts c) = {} \<or> (\<exists>n. Rep_nat_int (res ts c) = {n, n + 1})

goal (1 subgoal):
 1. |res ts c| = 2 \<Longrightarrow> \<exists>n. Rep_nat_int (res ts c) = {n, n + 1}
[PROOF STEP]
with assump
[PROOF STATE]
proof (chain)
picking this:
|res ts c| = 2
Rep_nat_int (res ts c) = {} \<or> (\<exists>n. Rep_nat_int (res ts c) = {n, n + 1})
[PROOF STEP]
show "(\<exists>n . Rep_nat_int (res ts c) = {n,n+1})"
[PROOF STATE]
proof (prove)
using this:
|res ts c| = 2
Rep_nat_int (res ts c) = {} \<or> (\<exists>n. Rep_nat_int (res ts c) = {n, n + 1})

goal (1 subgoal):
 1. \<exists>n. Rep_nat_int (res ts c) = {n, n + 1}
[PROOF STEP]
using Rep_nat_int_inject bot_nat_int.rep_eq card_non_empty_geq_one
[PROOF STATE]
proof (prove)
using this:
|res ts c| = 2
Rep_nat_int (res ts c) = {} \<or> (\<exists>n. Rep_nat_int (res ts c) = {n, n + 1})
(Rep_nat_int ?x = Rep_nat_int ?y) = (?x = ?y)
Rep_nat_int bot = {}
(?i \<noteq> bot) = (1 \<le> |?i|)

goal (1 subgoal):
 1. \<exists>n. Rep_nat_int (res ts c) = {n, n + 1}
[PROOF STEP]
by (metis not_empty)
[PROOF STATE]
proof (state)
this:
\<exists>n. Rep_nat_int (res ts c) = {n, n + 1}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma clmNextRes :
  "(clm ts c) \<noteq> \<emptyset> \<longrightarrow> (\<exists> n. Rep_nat_int(res ts c) \<union> Rep_nat_int(clm ts c) = {n, n+1})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. clm ts c \<noteq> bot \<longrightarrow> (\<exists>n. Rep_nat_int (res ts c) \<union> Rep_nat_int (clm ts c) = {n, n + 1})
[PROOF STEP]
using Rep_traffic res_def clm_def
[PROOF STATE]
proof (prove)
using this:
Rep_traffic ?x \<in> {ts. (\<forall>c. fst (snd ts) c \<sqinter> fst (snd (snd ts)) c = bot) \<and> (\<forall>c. 1 \<le> |fst (snd ts) c|) \<and> (\<forall>c. |fst (snd ts) c| \<le> 2) \<and> (\<forall>c. |fst (snd (snd ts)) c| \<le> 1) \<and> (\<forall>c. |fst (snd ts) c| + |fst (snd (snd ts)) c| \<le> 2) \<and> (\<forall>c. fst (snd (snd ts)) c \<noteq> bot \<longrightarrow> (\<exists>n. Rep_nat_int (fst (snd ts) c) \<union> Rep_nat_int (fst (snd (snd ts)) c) = {n, n + 1})) \<and> (\<forall>c. 0 < fst (snd (snd (snd (snd ts)))) c) \<and> (\<forall>c. 0 < snd (snd (snd (snd (snd ts)))) c)}
res ?ts \<equiv> fst (snd (Rep_traffic ?ts))
clm ?ts \<equiv> fst (snd (snd (Rep_traffic ?ts)))

goal (1 subgoal):
 1. clm ts c \<noteq> bot \<longrightarrow> (\<exists>n. Rep_nat_int (res ts c) \<union> Rep_nat_int (clm ts c) = {n, n + 1})
[PROOF STEP]
by auto


[STATEMENT]
lemma psGeZero:"\<forall>c. (physical_size ts c > 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>c. 0 < physical_size ts c
[PROOF STEP]
using Rep_traffic physical_size_def
[PROOF STATE]
proof (prove)
using this:
Rep_traffic ?x \<in> {ts. (\<forall>c. fst (snd ts) c \<sqinter> fst (snd (snd ts)) c = bot) \<and> (\<forall>c. 1 \<le> |fst (snd ts) c|) \<and> (\<forall>c. |fst (snd ts) c| \<le> 2) \<and> (\<forall>c. |fst (snd (snd ts)) c| \<le> 1) \<and> (\<forall>c. |fst (snd ts) c| + |fst (snd (snd ts)) c| \<le> 2) \<and> (\<forall>c. fst (snd (snd ts)) c \<noteq> bot \<longrightarrow> (\<exists>n. Rep_nat_int (fst (snd ts) c) \<union> Rep_nat_int (fst (snd (snd ts)) c) = {n, n + 1})) \<and> (\<forall>c. 0 < fst (snd (snd (snd (snd ts)))) c) \<and> (\<forall>c. 0 < snd (snd (snd (snd (snd ts)))) c)}
physical_size ?ts \<equiv> fst (snd (snd (snd (snd (Rep_traffic ?ts)))))

goal (1 subgoal):
 1. \<forall>c. 0 < physical_size ts c
[PROOF STEP]
by auto


[STATEMENT]
lemma sdGeZero:"\<forall>c. (braking_distance ts c > 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>c. 0 < braking_distance ts c
[PROOF STEP]
using Rep_traffic braking_distance_def
[PROOF STATE]
proof (prove)
using this:
Rep_traffic ?x \<in> {ts. (\<forall>c. fst (snd ts) c \<sqinter> fst (snd (snd ts)) c = bot) \<and> (\<forall>c. 1 \<le> |fst (snd ts) c|) \<and> (\<forall>c. |fst (snd ts) c| \<le> 2) \<and> (\<forall>c. |fst (snd (snd ts)) c| \<le> 1) \<and> (\<forall>c. |fst (snd ts) c| + |fst (snd (snd ts)) c| \<le> 2) \<and> (\<forall>c. fst (snd (snd ts)) c \<noteq> bot \<longrightarrow> (\<exists>n. Rep_nat_int (fst (snd ts) c) \<union> Rep_nat_int (fst (snd (snd ts)) c) = {n, n + 1})) \<and> (\<forall>c. 0 < fst (snd (snd (snd (snd ts)))) c) \<and> (\<forall>c. 0 < snd (snd (snd (snd (snd ts)))) c)}
braking_distance ?ts \<equiv> snd (snd (snd (snd (snd (Rep_traffic ?ts)))))

goal (1 subgoal):
 1. \<forall>c. 0 < braking_distance ts c
[PROOF STEP]
by auto


[STATEMENT]
lemma clm_consec_res:
"(clm ts) c \<noteq> \<emptyset> \<longrightarrow> consec (clm ts c) (res ts c) \<or> consec (res ts c) (clm ts c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. clm ts c \<noteq> bot \<longrightarrow> consec (clm ts c) (res ts c) \<or> consec (res ts c) (clm ts c)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. clm ts c \<noteq> bot \<Longrightarrow> consec (clm ts c) (res ts c) \<or> consec (res ts c) (clm ts c)
[PROOF STEP]
assume assm:"clm ts c \<noteq>\<emptyset>"
[PROOF STATE]
proof (state)
this:
clm ts c \<noteq> bot

goal (1 subgoal):
 1. clm ts c \<noteq> bot \<Longrightarrow> consec (clm ts c) (res ts c) \<or> consec (res ts c) (clm ts c)
[PROOF STEP]
hence adj:"(\<exists> n. Rep_nat_int(res ts c) \<union> Rep_nat_int(clm ts c) = {n, n+1})"
[PROOF STATE]
proof (prove)
using this:
clm ts c \<noteq> bot

goal (1 subgoal):
 1. \<exists>n. Rep_nat_int (res ts c) \<union> Rep_nat_int (clm ts c) = {n, n + 1}
[PROOF STEP]
using clmNextRes
[PROOF STATE]
proof (prove)
using this:
clm ts c \<noteq> bot
clm ?ts ?c \<noteq> bot \<longrightarrow> (\<exists>n. Rep_nat_int (res ?ts ?c) \<union> Rep_nat_int (clm ?ts ?c) = {n, n + 1})

goal (1 subgoal):
 1. \<exists>n. Rep_nat_int (res ts c) \<union> Rep_nat_int (clm ts c) = {n, n + 1}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>n. Rep_nat_int (res ts c) \<union> Rep_nat_int (clm ts c) = {n, n + 1}

goal (1 subgoal):
 1. clm ts c \<noteq> bot \<Longrightarrow> consec (clm ts c) (res ts c) \<or> consec (res ts c) (clm ts c)
[PROOF STEP]
obtain n where n_def:"Rep_nat_int(res ts c)\<union>Rep_nat_int(clm ts c) = {n, n+1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>n. Rep_nat_int (res ts c) \<union> Rep_nat_int (clm ts c) = {n, n + 1} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using adj
[PROOF STATE]
proof (prove)
using this:
\<exists>n. Rep_nat_int (res ts c) \<union> Rep_nat_int (clm ts c) = {n, n + 1}

goal (1 subgoal):
 1. (\<And>n. Rep_nat_int (res ts c) \<union> Rep_nat_int (clm ts c) = {n, n + 1} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Rep_nat_int (res ts c) \<union> Rep_nat_int (clm ts c) = {n, n + 1}

goal (1 subgoal):
 1. clm ts c \<noteq> bot \<Longrightarrow> consec (clm ts c) (res ts c) \<or> consec (res ts c) (clm ts c)
[PROOF STEP]
have disj:"res ts c \<sqinter> clm ts c = \<emptyset>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. res ts c \<sqinter> clm ts c = bot
[PROOF STEP]
using disjoint
[PROOF STATE]
proof (prove)
using this:
res ?ts ?c \<sqinter> clm ?ts ?c = bot

goal (1 subgoal):
 1. res ts c \<sqinter> clm ts c = bot
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
res ts c \<sqinter> clm ts c = bot

goal (1 subgoal):
 1. clm ts c \<noteq> bot \<Longrightarrow> consec (clm ts c) (res ts c) \<or> consec (res ts c) (clm ts c)
[PROOF STEP]
from n_def and disj
[PROOF STATE]
proof (chain)
picking this:
Rep_nat_int (res ts c) \<union> Rep_nat_int (clm ts c) = {n, n + 1}
res ts c \<sqinter> clm ts c = bot
[PROOF STEP]
have "(n \<^bold>\<in> res ts c \<and> n \<^bold>\<notin> clm ts c) \<or> (n \<^bold>\<in> clm ts c \<and> n \<^bold>\<notin> res ts c)"
[PROOF STATE]
proof (prove)
using this:
Rep_nat_int (res ts c) \<union> Rep_nat_int (clm ts c) = {n, n + 1}
res ts c \<sqinter> clm ts c = bot

goal (1 subgoal):
 1. n \<^bold>\<in> res ts c \<and> n \<^bold>\<notin> clm ts c \<or> n \<^bold>\<in> clm ts c \<and> n \<^bold>\<notin> res ts c
[PROOF STEP]
by (metis UnE bot_nat_int.rep_eq disjoint_insert(1) el.rep_eq inf_nat_int.rep_eq
          insertI1 insert_absorb not_in.rep_eq)
[PROOF STATE]
proof (state)
this:
n \<^bold>\<in> res ts c \<and> n \<^bold>\<notin> clm ts c \<or> n \<^bold>\<in> clm ts c \<and> n \<^bold>\<notin> res ts c

goal (1 subgoal):
 1. clm ts c \<noteq> bot \<Longrightarrow> consec (clm ts c) (res ts c) \<or> consec (res ts c) (clm ts c)
[PROOF STEP]
thus "consec (clm ts c) (res ts c) \<or> consec (res ts c) (clm ts c)"
[PROOF STATE]
proof (prove)
using this:
n \<^bold>\<in> res ts c \<and> n \<^bold>\<notin> clm ts c \<or> n \<^bold>\<in> clm ts c \<and> n \<^bold>\<notin> res ts c

goal (1 subgoal):
 1. consec (clm ts c) (res ts c) \<or> consec (res ts c) (clm ts c)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n \<^bold>\<in> res ts c \<and> n \<^bold>\<notin> clm ts c \<Longrightarrow> consec (clm ts c) (res ts c) \<or> consec (res ts c) (clm ts c)
 2. n \<^bold>\<in> clm ts c \<and> n \<^bold>\<notin> res ts c \<Longrightarrow> consec (clm ts c) (res ts c) \<or> consec (res ts c) (clm ts c)
[PROOF STEP]
assume n_in_res: "n \<^bold>\<in> res ts c \<and>  n \<^bold>\<notin> clm ts c"
[PROOF STATE]
proof (state)
this:
n \<^bold>\<in> res ts c \<and> n \<^bold>\<notin> clm ts c

goal (2 subgoals):
 1. n \<^bold>\<in> res ts c \<and> n \<^bold>\<notin> clm ts c \<Longrightarrow> consec (clm ts c) (res ts c) \<or> consec (res ts c) (clm ts c)
 2. n \<^bold>\<in> clm ts c \<and> n \<^bold>\<notin> res ts c \<Longrightarrow> consec (clm ts c) (res ts c) \<or> consec (res ts c) (clm ts c)
[PROOF STEP]
hence suc_n_in_clm:"n+1 \<^bold>\<in> clm ts c"
[PROOF STATE]
proof (prove)
using this:
n \<^bold>\<in> res ts c \<and> n \<^bold>\<notin> clm ts c

goal (1 subgoal):
 1. n + 1 \<^bold>\<in> clm ts c
[PROOF STEP]
by (metis UnCI assm el.rep_eq in_not_in_iff1 insert_iff n_def non_empty_elem_in
          singletonD)
[PROOF STATE]
proof (state)
this:
n + 1 \<^bold>\<in> clm ts c

goal (2 subgoals):
 1. n \<^bold>\<in> res ts c \<and> n \<^bold>\<notin> clm ts c \<Longrightarrow> consec (clm ts c) (res ts c) \<or> consec (res ts c) (clm ts c)
 2. n \<^bold>\<in> clm ts c \<and> n \<^bold>\<notin> res ts c \<Longrightarrow> consec (clm ts c) (res ts c) \<or> consec (res ts c) (clm ts c)
[PROOF STEP]
have "Rep_nat_int (res ts c) \<noteq> {n, n + 1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_nat_int (res ts c) \<noteq> {n, n + 1}
[PROOF STEP]
by (metis assm disj n_def inf_absorb1 inf_commute less_eq_nat_int.rep_eq
          sup.cobounded2)
[PROOF STATE]
proof (state)
this:
Rep_nat_int (res ts c) \<noteq> {n, n + 1}

goal (2 subgoals):
 1. n \<^bold>\<in> res ts c \<and> n \<^bold>\<notin> clm ts c \<Longrightarrow> consec (clm ts c) (res ts c) \<or> consec (res ts c) (clm ts c)
 2. n \<^bold>\<in> clm ts c \<and> n \<^bold>\<notin> res ts c \<Longrightarrow> consec (clm ts c) (res ts c) \<or> consec (res ts c) (clm ts c)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Rep_nat_int (res ts c) \<noteq> {n, n + 1}
[PROOF STEP]
have suc_n_not_in_res:"n+1 \<^bold>\<notin> res ts c"
[PROOF STATE]
proof (prove)
using this:
Rep_nat_int (res ts c) \<noteq> {n, n + 1}

goal (1 subgoal):
 1. n + 1 \<^bold>\<notin> res ts c
[PROOF STEP]
using n_def n_in_res nat_int.el.rep_eq nat_int.not_in.rep_eq
[PROOF STATE]
proof (prove)
using this:
Rep_nat_int (res ts c) \<noteq> {n, n + 1}
Rep_nat_int (res ts c) \<union> Rep_nat_int (clm ts c) = {n, n + 1}
n \<^bold>\<in> res ts c \<and> n \<^bold>\<notin> clm ts c
(?x \<^bold>\<in> ?xa) = (?x \<in> Rep_nat_int ?xa)
(?x \<^bold>\<notin> ?xa) = (?x \<notin> Rep_nat_int ?xa)

goal (1 subgoal):
 1. n + 1 \<^bold>\<notin> res ts c
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n + 1 \<^bold>\<notin> res ts c

goal (2 subgoals):
 1. n \<^bold>\<in> res ts c \<and> n \<^bold>\<notin> clm ts c \<Longrightarrow> consec (clm ts c) (res ts c) \<or> consec (res ts c) (clm ts c)
 2. n \<^bold>\<in> clm ts c \<and> n \<^bold>\<notin> res ts c \<Longrightarrow> consec (clm ts c) (res ts c) \<or> consec (res ts c) (clm ts c)
[PROOF STEP]
from n_in_res
[PROOF STATE]
proof (chain)
picking this:
n \<^bold>\<in> res ts c \<and> n \<^bold>\<notin> clm ts c
[PROOF STEP]
have n_not_in_clm:"n \<^bold>\<notin> clm ts c"
[PROOF STATE]
proof (prove)
using this:
n \<^bold>\<in> res ts c \<and> n \<^bold>\<notin> clm ts c

goal (1 subgoal):
 1. n \<^bold>\<notin> clm ts c
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
n \<^bold>\<notin> clm ts c

goal (2 subgoals):
 1. n \<^bold>\<in> res ts c \<and> n \<^bold>\<notin> clm ts c \<Longrightarrow> consec (clm ts c) (res ts c) \<or> consec (res ts c) (clm ts c)
 2. n \<^bold>\<in> clm ts c \<and> n \<^bold>\<notin> res ts c \<Longrightarrow> consec (clm ts c) (res ts c) \<or> consec (res ts c) (clm ts c)
[PROOF STEP]
have max:"nat_int.maximum (res ts c) = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. maximum (res ts c) = n
[PROOF STEP]
using n_in_res suc_n_not_in_res nat_int.el.rep_eq nat_int.not_in.rep_eq n_def
        nat_int.maximum_in nat_int.non_empty_elem_in inf_sup_aci(4)
[PROOF STATE]
proof (prove)
using this:
n \<^bold>\<in> res ts c \<and> n \<^bold>\<notin> clm ts c
n + 1 \<^bold>\<notin> res ts c
(?x \<^bold>\<in> ?xa) = (?x \<in> Rep_nat_int ?xa)
(?x \<^bold>\<notin> ?xa) = (?x \<notin> Rep_nat_int ?xa)
Rep_nat_int (res ts c) \<union> Rep_nat_int (clm ts c) = {n, n + 1}
?i \<noteq> bot \<longrightarrow> maximum ?i \<^bold>\<in> ?i
(?i \<noteq> bot) = (\<exists>n. n \<^bold>\<in> ?i)
?x \<sqinter> (?x \<sqinter> ?y) = ?x \<sqinter> ?y

goal (1 subgoal):
 1. maximum (res ts c) = n
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
maximum (res ts c) = n

goal (2 subgoals):
 1. n \<^bold>\<in> res ts c \<and> n \<^bold>\<notin> clm ts c \<Longrightarrow> consec (clm ts c) (res ts c) \<or> consec (res ts c) (clm ts c)
 2. n \<^bold>\<in> clm ts c \<and> n \<^bold>\<notin> res ts c \<Longrightarrow> consec (clm ts c) (res ts c) \<or> consec (res ts c) (clm ts c)
[PROOF STEP]
have min:"nat_int.minimum (clm ts c) = n+1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. minimum (clm ts c) = n + 1
[PROOF STEP]
using suc_n_in_clm n_not_in_clm nat_int.el.rep_eq nat_int.not_in.rep_eq
        n_def nat_int.minimum_in nat_int.non_empty_elem_in
[PROOF STATE]
proof (prove)
using this:
n + 1 \<^bold>\<in> clm ts c
n \<^bold>\<notin> clm ts c
(?x \<^bold>\<in> ?xa) = (?x \<in> Rep_nat_int ?xa)
(?x \<^bold>\<notin> ?xa) = (?x \<notin> Rep_nat_int ?xa)
Rep_nat_int (res ts c) \<union> Rep_nat_int (clm ts c) = {n, n + 1}
?i \<noteq> bot \<longrightarrow> minimum ?i \<^bold>\<in> ?i
(?i \<noteq> bot) = (\<exists>n. n \<^bold>\<in> ?i)

goal (1 subgoal):
 1. minimum (clm ts c) = n + 1
[PROOF STEP]
using inf_sup_aci(4)
        not_in.rep_eq
[PROOF STATE]
proof (prove)
using this:
n + 1 \<^bold>\<in> clm ts c
n \<^bold>\<notin> clm ts c
(?x \<^bold>\<in> ?xa) = (?x \<in> Rep_nat_int ?xa)
(?x \<^bold>\<notin> ?xa) = (?x \<notin> Rep_nat_int ?xa)
Rep_nat_int (res ts c) \<union> Rep_nat_int (clm ts c) = {n, n + 1}
?i \<noteq> bot \<longrightarrow> minimum ?i \<^bold>\<in> ?i
(?i \<noteq> bot) = (\<exists>n. n \<^bold>\<in> ?i)
?x \<sqinter> (?x \<sqinter> ?y) = ?x \<sqinter> ?y
(?x \<^bold>\<notin> ?xa) = (?x \<notin> Rep_nat_int ?xa)

goal (1 subgoal):
 1. minimum (clm ts c) = n + 1
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
minimum (clm ts c) = n + 1

goal (2 subgoals):
 1. n \<^bold>\<in> res ts c \<and> n \<^bold>\<notin> clm ts c \<Longrightarrow> consec (clm ts c) (res ts c) \<or> consec (res ts c) (clm ts c)
 2. n \<^bold>\<in> clm ts c \<and> n \<^bold>\<notin> res ts c \<Longrightarrow> consec (clm ts c) (res ts c) \<or> consec (res ts c) (clm ts c)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. consec (clm ts c) (res ts c) \<or> consec (res ts c) (clm ts c)
[PROOF STEP]
using assm max min n_in_res nat_int.consec_def nat_int.non_empty_elem_in
[PROOF STATE]
proof (prove)
using this:
clm ts c \<noteq> bot
maximum (res ts c) = n
minimum (clm ts c) = n + 1
n \<^bold>\<in> res ts c \<and> n \<^bold>\<notin> clm ts c
consec ?i ?j \<equiv> ?i \<noteq> bot \<and> ?j \<noteq> bot \<and> maximum ?i + 1 = minimum ?j
(?i \<noteq> bot) = (\<exists>n. n \<^bold>\<in> ?i)

goal (1 subgoal):
 1. consec (clm ts c) (res ts c) \<or> consec (res ts c) (clm ts c)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
consec (clm ts c) (res ts c) \<or> consec (res ts c) (clm ts c)

goal (1 subgoal):
 1. n \<^bold>\<in> clm ts c \<and> n \<^bold>\<notin> res ts c \<Longrightarrow> consec (clm ts c) (res ts c) \<or> consec (res ts c) (clm ts c)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n \<^bold>\<in> clm ts c \<and> n \<^bold>\<notin> res ts c \<Longrightarrow> consec (clm ts c) (res ts c) \<or> consec (res ts c) (clm ts c)
[PROOF STEP]
assume n_in_clm: "n \<^bold>\<in> clm ts c \<and> n \<^bold>\<notin> res ts c "
[PROOF STATE]
proof (state)
this:
n \<^bold>\<in> clm ts c \<and> n \<^bold>\<notin> res ts c

goal (1 subgoal):
 1. n \<^bold>\<in> clm ts c \<and> n \<^bold>\<notin> res ts c \<Longrightarrow> consec (clm ts c) (res ts c) \<or> consec (res ts c) (clm ts c)
[PROOF STEP]
have suc_n_in_res:"n+1 \<^bold>\<in> res ts c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n + 1 \<^bold>\<in> res ts c
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> n + 1 \<^bold>\<in> res ts c \<Longrightarrow> False
[PROOF STEP]
assume "\<not>n+1 \<^bold>\<in> res ts c"
[PROOF STATE]
proof (state)
this:
\<not> n + 1 \<^bold>\<in> res ts c

goal (1 subgoal):
 1. \<not> n + 1 \<^bold>\<in> res ts c \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> n + 1 \<^bold>\<in> res ts c
[PROOF STEP]
have "n \<^bold>\<in> res ts c "
[PROOF STATE]
proof (prove)
using this:
\<not> n + 1 \<^bold>\<in> res ts c

goal (1 subgoal):
 1. n \<^bold>\<in> res ts c
[PROOF STEP]
by (metis Int_insert_right_if0 One_nat_def Suc_leI add.right_neutral add_Suc_right
            atMostTwoRes el.rep_eq inf_bot_right inf_sup_absorb insert_not_empty le_antisym
            n_def one_add_one order.not_eq_order_implies_strict singleton traffic.atLeastOneRes
            traffic.consecutiveRes)
[PROOF STATE]
proof (state)
this:
n \<^bold>\<in> res ts c

goal (1 subgoal):
 1. \<not> n + 1 \<^bold>\<in> res ts c \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n \<^bold>\<in> res ts c
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
n \<^bold>\<in> res ts c

goal (1 subgoal):
 1. False
[PROOF STEP]
using n_in_clm
[PROOF STATE]
proof (prove)
using this:
n \<^bold>\<in> res ts c
n \<^bold>\<in> clm ts c \<and> n \<^bold>\<notin> res ts c

goal (1 subgoal):
 1. False
[PROOF STEP]
using nat_int.el.rep_eq nat_int.not_in.rep_eq
[PROOF STATE]
proof (prove)
using this:
n \<^bold>\<in> res ts c
n \<^bold>\<in> clm ts c \<and> n \<^bold>\<notin> res ts c
(?x \<^bold>\<in> ?xa) = (?x \<in> Rep_nat_int ?xa)
(?x \<^bold>\<notin> ?xa) = (?x \<notin> Rep_nat_int ?xa)

goal (1 subgoal):
 1. False
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
n + 1 \<^bold>\<in> res ts c

goal (1 subgoal):
 1. n \<^bold>\<in> clm ts c \<and> n \<^bold>\<notin> res ts c \<Longrightarrow> consec (clm ts c) (res ts c) \<or> consec (res ts c) (clm ts c)
[PROOF STEP]
have max:"nat_int.maximum (clm ts c) = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. maximum (clm ts c) = n
[PROOF STEP]
by (metis Rep_nat_int_inverse assm n_in_clm card_non_empty_geq_one
          le_antisym nat_int.in_singleton nat_int.maximum_in singleton traffic.atMostOneClm)
[PROOF STATE]
proof (state)
this:
maximum (clm ts c) = n

goal (1 subgoal):
 1. n \<^bold>\<in> clm ts c \<and> n \<^bold>\<notin> res ts c \<Longrightarrow> consec (clm ts c) (res ts c) \<or> consec (res ts c) (clm ts c)
[PROOF STEP]
have min:"nat_int.minimum (res ts c) = n+1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. minimum (res ts c) = n + 1
[PROOF STEP]
by (metis Int_insert_right_if0 Int_insert_right_if1 Rep_nat_int_inverse
          bot_nat_int.rep_eq el.rep_eq in_not_in_iff1 in_singleton inf_nat_int.rep_eq
          inf_sup_absorb insert_not_empty inter_empty1 minimum_in n_def
          n_in_clm suc_n_in_res)
[PROOF STATE]
proof (state)
this:
minimum (res ts c) = n + 1

goal (1 subgoal):
 1. n \<^bold>\<in> clm ts c \<and> n \<^bold>\<notin> res ts c \<Longrightarrow> consec (clm ts c) (res ts c) \<or> consec (res ts c) (clm ts c)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
minimum (res ts c) = n + 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
minimum (res ts c) = n + 1

goal (1 subgoal):
 1. consec (clm ts c) (res ts c) \<or> consec (res ts c) (clm ts c)
[PROOF STEP]
using assm max min nat_int.consec_def nat_int.non_empty_elem_in
        suc_n_in_res
[PROOF STATE]
proof (prove)
using this:
minimum (res ts c) = n + 1
clm ts c \<noteq> bot
maximum (clm ts c) = n
minimum (res ts c) = n + 1
consec ?i ?j \<equiv> ?i \<noteq> bot \<and> ?j \<noteq> bot \<and> maximum ?i + 1 = minimum ?j
(?i \<noteq> bot) = (\<exists>n. n \<^bold>\<in> ?i)
n + 1 \<^bold>\<in> res ts c

goal (1 subgoal):
 1. consec (clm ts c) (res ts c) \<or> consec (res ts c) (clm ts c)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
consec (clm ts c) (res ts c) \<or> consec (res ts c) (clm ts c)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
consec (clm ts c) (res ts c) \<or> consec (res ts c) (clm ts c)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma evolve_trans:"(ts0 \<^bold>\<leadsto> ts1) \<Longrightarrow> (ts1 \<^bold>\<leadsto> ts2) \<Longrightarrow> (ts0 \<^bold>\<leadsto> ts2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ts0 \<^bold>\<leadsto> ts1; ts1 \<^bold>\<leadsto> ts2\<rbrakk> \<Longrightarrow> ts0 \<^bold>\<leadsto> ts2
[PROOF STEP]
proof (induction rule:evolve.induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>ts. ts \<^bold>\<leadsto> ts2 \<Longrightarrow> ts \<^bold>\<leadsto> ts2
 2. \<And>ts ts' ts''. \<lbrakk>\<exists>c f.  ts \<^bold>\<midarrow> dyn(c,f) \<^bold>\<rightarrow> ts'; ts' \<^bold>\<leadsto> ts''; ts'' \<^bold>\<leadsto> ts2 \<Longrightarrow> ts' \<^bold>\<leadsto> ts2; ts'' \<^bold>\<leadsto> ts2\<rbrakk> \<Longrightarrow> ts \<^bold>\<leadsto> ts2
 3. \<And>ts ts' ts''. \<lbrakk>\<exists>x\<ge>0.  ts \<^bold>\<midarrow> x \<^bold>\<rightarrow> ts'; ts' \<^bold>\<leadsto> ts''; ts'' \<^bold>\<leadsto> ts2 \<Longrightarrow> ts' \<^bold>\<leadsto> ts2; ts'' \<^bold>\<leadsto> ts2\<rbrakk> \<Longrightarrow> ts \<^bold>\<leadsto> ts2
[PROOF STEP]
case (refl ts)
[PROOF STATE]
proof (state)
this:
ts \<^bold>\<leadsto> ts2

goal (3 subgoals):
 1. \<And>ts. ts \<^bold>\<leadsto> ts2 \<Longrightarrow> ts \<^bold>\<leadsto> ts2
 2. \<And>ts ts' ts''. \<lbrakk>\<exists>c f.  ts \<^bold>\<midarrow> dyn(c,f) \<^bold>\<rightarrow> ts'; ts' \<^bold>\<leadsto> ts''; ts'' \<^bold>\<leadsto> ts2 \<Longrightarrow> ts' \<^bold>\<leadsto> ts2; ts'' \<^bold>\<leadsto> ts2\<rbrakk> \<Longrightarrow> ts \<^bold>\<leadsto> ts2
 3. \<And>ts ts' ts''. \<lbrakk>\<exists>x\<ge>0.  ts \<^bold>\<midarrow> x \<^bold>\<rightarrow> ts'; ts' \<^bold>\<leadsto> ts''; ts'' \<^bold>\<leadsto> ts2 \<Longrightarrow> ts' \<^bold>\<leadsto> ts2; ts'' \<^bold>\<leadsto> ts2\<rbrakk> \<Longrightarrow> ts \<^bold>\<leadsto> ts2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ts \<^bold>\<leadsto> ts2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
ts \<^bold>\<leadsto> ts2

goal (1 subgoal):
 1. ts \<^bold>\<leadsto> ts2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ts \<^bold>\<leadsto> ts2

goal (2 subgoals):
 1. \<And>ts ts' ts''. \<lbrakk>\<exists>c f.  ts \<^bold>\<midarrow> dyn(c,f) \<^bold>\<rightarrow> ts'; ts' \<^bold>\<leadsto> ts''; ts'' \<^bold>\<leadsto> ts2 \<Longrightarrow> ts' \<^bold>\<leadsto> ts2; ts'' \<^bold>\<leadsto> ts2\<rbrakk> \<Longrightarrow> ts \<^bold>\<leadsto> ts2
 2. \<And>ts ts' ts''. \<lbrakk>\<exists>x\<ge>0.  ts \<^bold>\<midarrow> x \<^bold>\<rightarrow> ts'; ts' \<^bold>\<leadsto> ts''; ts'' \<^bold>\<leadsto> ts2 \<Longrightarrow> ts' \<^bold>\<leadsto> ts2; ts'' \<^bold>\<leadsto> ts2\<rbrakk> \<Longrightarrow> ts \<^bold>\<leadsto> ts2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ts ts' ts''. \<lbrakk>\<exists>c f.  ts \<^bold>\<midarrow> dyn(c,f) \<^bold>\<rightarrow> ts'; ts' \<^bold>\<leadsto> ts''; ts'' \<^bold>\<leadsto> ts2 \<Longrightarrow> ts' \<^bold>\<leadsto> ts2; ts'' \<^bold>\<leadsto> ts2\<rbrakk> \<Longrightarrow> ts \<^bold>\<leadsto> ts2
 2. \<And>ts ts' ts''. \<lbrakk>\<exists>x\<ge>0.  ts \<^bold>\<midarrow> x \<^bold>\<rightarrow> ts'; ts' \<^bold>\<leadsto> ts''; ts'' \<^bold>\<leadsto> ts2 \<Longrightarrow> ts' \<^bold>\<leadsto> ts2; ts'' \<^bold>\<leadsto> ts2\<rbrakk> \<Longrightarrow> ts \<^bold>\<leadsto> ts2
[PROOF STEP]
case (drive ts ts' ts'')
[PROOF STATE]
proof (state)
this:
\<exists>x\<ge>0.  ts \<^bold>\<midarrow> x \<^bold>\<rightarrow> ts'
ts' \<^bold>\<leadsto> ts''
ts'' \<^bold>\<leadsto> ts2 \<Longrightarrow> ts' \<^bold>\<leadsto> ts2
ts'' \<^bold>\<leadsto> ts2

goal (2 subgoals):
 1. \<And>ts ts' ts''. \<lbrakk>\<exists>c f.  ts \<^bold>\<midarrow> dyn(c,f) \<^bold>\<rightarrow> ts'; ts' \<^bold>\<leadsto> ts''; ts'' \<^bold>\<leadsto> ts2 \<Longrightarrow> ts' \<^bold>\<leadsto> ts2; ts'' \<^bold>\<leadsto> ts2\<rbrakk> \<Longrightarrow> ts \<^bold>\<leadsto> ts2
 2. \<And>ts ts' ts''. \<lbrakk>\<exists>x\<ge>0.  ts \<^bold>\<midarrow> x \<^bold>\<rightarrow> ts'; ts' \<^bold>\<leadsto> ts''; ts'' \<^bold>\<leadsto> ts2 \<Longrightarrow> ts' \<^bold>\<leadsto> ts2; ts'' \<^bold>\<leadsto> ts2\<rbrakk> \<Longrightarrow> ts \<^bold>\<leadsto> ts2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>x\<ge>0.  ts \<^bold>\<midarrow> x \<^bold>\<rightarrow> ts'
ts' \<^bold>\<leadsto> ts''
ts'' \<^bold>\<leadsto> ts2 \<Longrightarrow> ts' \<^bold>\<leadsto> ts2
ts'' \<^bold>\<leadsto> ts2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<exists>x\<ge>0.  ts \<^bold>\<midarrow> x \<^bold>\<rightarrow> ts'
ts' \<^bold>\<leadsto> ts''
ts'' \<^bold>\<leadsto> ts2 \<Longrightarrow> ts' \<^bold>\<leadsto> ts2
ts'' \<^bold>\<leadsto> ts2

goal (1 subgoal):
 1. ts \<^bold>\<leadsto> ts2
[PROOF STEP]
by (metis evolve.drive)
[PROOF STATE]
proof (state)
this:
ts \<^bold>\<leadsto> ts2

goal (1 subgoal):
 1. \<And>ts ts' ts''. \<lbrakk>\<exists>c f.  ts \<^bold>\<midarrow> dyn(c,f) \<^bold>\<rightarrow> ts'; ts' \<^bold>\<leadsto> ts''; ts'' \<^bold>\<leadsto> ts2 \<Longrightarrow> ts' \<^bold>\<leadsto> ts2; ts'' \<^bold>\<leadsto> ts2\<rbrakk> \<Longrightarrow> ts \<^bold>\<leadsto> ts2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ts ts' ts''. \<lbrakk>\<exists>c f.  ts \<^bold>\<midarrow> dyn(c,f) \<^bold>\<rightarrow> ts'; ts' \<^bold>\<leadsto> ts''; ts'' \<^bold>\<leadsto> ts2 \<Longrightarrow> ts' \<^bold>\<leadsto> ts2; ts'' \<^bold>\<leadsto> ts2\<rbrakk> \<Longrightarrow> ts \<^bold>\<leadsto> ts2
[PROOF STEP]
case (change ts ts' ts'')
[PROOF STATE]
proof (state)
this:
\<exists>c f.  ts \<^bold>\<midarrow> dyn(c,f) \<^bold>\<rightarrow> ts'
ts' \<^bold>\<leadsto> ts''
ts'' \<^bold>\<leadsto> ts2 \<Longrightarrow> ts' \<^bold>\<leadsto> ts2
ts'' \<^bold>\<leadsto> ts2

goal (1 subgoal):
 1. \<And>ts ts' ts''. \<lbrakk>\<exists>c f.  ts \<^bold>\<midarrow> dyn(c,f) \<^bold>\<rightarrow> ts'; ts' \<^bold>\<leadsto> ts''; ts'' \<^bold>\<leadsto> ts2 \<Longrightarrow> ts' \<^bold>\<leadsto> ts2; ts'' \<^bold>\<leadsto> ts2\<rbrakk> \<Longrightarrow> ts \<^bold>\<leadsto> ts2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>c f.  ts \<^bold>\<midarrow> dyn(c,f) \<^bold>\<rightarrow> ts'
ts' \<^bold>\<leadsto> ts''
ts'' \<^bold>\<leadsto> ts2 \<Longrightarrow> ts' \<^bold>\<leadsto> ts2
ts'' \<^bold>\<leadsto> ts2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<exists>c f.  ts \<^bold>\<midarrow> dyn(c,f) \<^bold>\<rightarrow> ts'
ts' \<^bold>\<leadsto> ts''
ts'' \<^bold>\<leadsto> ts2 \<Longrightarrow> ts' \<^bold>\<leadsto> ts2
ts'' \<^bold>\<leadsto> ts2

goal (1 subgoal):
 1. ts \<^bold>\<leadsto> ts2
[PROOF STEP]
by (metis evolve.change)
[PROOF STATE]
proof (state)
this:
ts \<^bold>\<leadsto> ts2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma abs_trans:" (ts1 \<^bold>\<Rightarrow> ts2) \<Longrightarrow>(ts0 \<^bold>\<Rightarrow> ts1) \<Longrightarrow> (ts0 \<^bold>\<Rightarrow> ts2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ts1 \<^bold>\<Rightarrow> ts2; ts0 \<^bold>\<Rightarrow> ts1\<rbrakk> \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts2
[PROOF STEP]
proof (induction  rule:abstract.induct    )
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts1
 2. \<And>ts' ts''. \<lbrakk>ts1 \<^bold>\<Rightarrow> ts'; ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'; ts' \<^bold>\<leadsto> ts''; ts0 \<^bold>\<Rightarrow> ts1\<rbrakk> \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts''
 3. \<And>ts' ts''. \<lbrakk>ts1 \<^bold>\<Rightarrow> ts'; ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'; \<exists>c n. ts' \<^bold>\<midarrow>c( c, n ) \<^bold>\<rightarrow> ts''; ts0 \<^bold>\<Rightarrow> ts1\<rbrakk> \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts''
 4. \<And>ts' ts''. \<lbrakk>ts1 \<^bold>\<Rightarrow> ts'; ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'; \<exists>c. ts' \<^bold>\<midarrow>wdc( c ) \<^bold>\<rightarrow> ts''; ts0 \<^bold>\<Rightarrow> ts1\<rbrakk> \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts''
 5. \<And>ts' ts''. \<lbrakk>ts1 \<^bold>\<Rightarrow> ts'; ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'; \<exists>c. ts' \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts''; ts0 \<^bold>\<Rightarrow> ts1\<rbrakk> \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts''
 6. \<And>ts' ts''. \<lbrakk>ts1 \<^bold>\<Rightarrow> ts'; ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'; \<exists>c n. ts' \<^bold>\<midarrow>wdr( c, n ) \<^bold>\<rightarrow> ts''; ts0 \<^bold>\<Rightarrow> ts1\<rbrakk> \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts''
[PROOF STEP]
case refl
[PROOF STATE]
proof (state)
this:
ts0 \<^bold>\<Rightarrow> ts1

goal (6 subgoals):
 1. ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts1
 2. \<And>ts' ts''. \<lbrakk>ts1 \<^bold>\<Rightarrow> ts'; ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'; ts' \<^bold>\<leadsto> ts''; ts0 \<^bold>\<Rightarrow> ts1\<rbrakk> \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts''
 3. \<And>ts' ts''. \<lbrakk>ts1 \<^bold>\<Rightarrow> ts'; ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'; \<exists>c n. ts' \<^bold>\<midarrow>c( c, n ) \<^bold>\<rightarrow> ts''; ts0 \<^bold>\<Rightarrow> ts1\<rbrakk> \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts''
 4. \<And>ts' ts''. \<lbrakk>ts1 \<^bold>\<Rightarrow> ts'; ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'; \<exists>c. ts' \<^bold>\<midarrow>wdc( c ) \<^bold>\<rightarrow> ts''; ts0 \<^bold>\<Rightarrow> ts1\<rbrakk> \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts''
 5. \<And>ts' ts''. \<lbrakk>ts1 \<^bold>\<Rightarrow> ts'; ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'; \<exists>c. ts' \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts''; ts0 \<^bold>\<Rightarrow> ts1\<rbrakk> \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts''
 6. \<And>ts' ts''. \<lbrakk>ts1 \<^bold>\<Rightarrow> ts'; ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'; \<exists>c n. ts' \<^bold>\<midarrow>wdr( c, n ) \<^bold>\<rightarrow> ts''; ts0 \<^bold>\<Rightarrow> ts1\<rbrakk> \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts''
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ts0 \<^bold>\<Rightarrow> ts1
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
ts0 \<^bold>\<Rightarrow> ts1

goal (1 subgoal):
 1. ts0 \<^bold>\<Rightarrow> ts1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ts0 \<^bold>\<Rightarrow> ts1

goal (5 subgoals):
 1. \<And>ts' ts''. \<lbrakk>ts1 \<^bold>\<Rightarrow> ts'; ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'; ts' \<^bold>\<leadsto> ts''; ts0 \<^bold>\<Rightarrow> ts1\<rbrakk> \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts''
 2. \<And>ts' ts''. \<lbrakk>ts1 \<^bold>\<Rightarrow> ts'; ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'; \<exists>c n. ts' \<^bold>\<midarrow>c( c, n ) \<^bold>\<rightarrow> ts''; ts0 \<^bold>\<Rightarrow> ts1\<rbrakk> \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts''
 3. \<And>ts' ts''. \<lbrakk>ts1 \<^bold>\<Rightarrow> ts'; ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'; \<exists>c. ts' \<^bold>\<midarrow>wdc( c ) \<^bold>\<rightarrow> ts''; ts0 \<^bold>\<Rightarrow> ts1\<rbrakk> \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts''
 4. \<And>ts' ts''. \<lbrakk>ts1 \<^bold>\<Rightarrow> ts'; ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'; \<exists>c. ts' \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts''; ts0 \<^bold>\<Rightarrow> ts1\<rbrakk> \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts''
 5. \<And>ts' ts''. \<lbrakk>ts1 \<^bold>\<Rightarrow> ts'; ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'; \<exists>c n. ts' \<^bold>\<midarrow>wdr( c, n ) \<^bold>\<rightarrow> ts''; ts0 \<^bold>\<Rightarrow> ts1\<rbrakk> \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts''
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>ts' ts''. \<lbrakk>ts1 \<^bold>\<Rightarrow> ts'; ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'; ts' \<^bold>\<leadsto> ts''; ts0 \<^bold>\<Rightarrow> ts1\<rbrakk> \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts''
 2. \<And>ts' ts''. \<lbrakk>ts1 \<^bold>\<Rightarrow> ts'; ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'; \<exists>c n. ts' \<^bold>\<midarrow>c( c, n ) \<^bold>\<rightarrow> ts''; ts0 \<^bold>\<Rightarrow> ts1\<rbrakk> \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts''
 3. \<And>ts' ts''. \<lbrakk>ts1 \<^bold>\<Rightarrow> ts'; ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'; \<exists>c. ts' \<^bold>\<midarrow>wdc( c ) \<^bold>\<rightarrow> ts''; ts0 \<^bold>\<Rightarrow> ts1\<rbrakk> \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts''
 4. \<And>ts' ts''. \<lbrakk>ts1 \<^bold>\<Rightarrow> ts'; ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'; \<exists>c. ts' \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts''; ts0 \<^bold>\<Rightarrow> ts1\<rbrakk> \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts''
 5. \<And>ts' ts''. \<lbrakk>ts1 \<^bold>\<Rightarrow> ts'; ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'; \<exists>c n. ts' \<^bold>\<midarrow>wdr( c, n ) \<^bold>\<rightarrow> ts''; ts0 \<^bold>\<Rightarrow> ts1\<rbrakk> \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts''
[PROOF STEP]
case (evolve ts' ts'')
[PROOF STATE]
proof (state)
this:
ts1 \<^bold>\<Rightarrow> ts'
ts' \<^bold>\<leadsto> ts''
ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'
ts0 \<^bold>\<Rightarrow> ts1

goal (5 subgoals):
 1. \<And>ts' ts''. \<lbrakk>ts1 \<^bold>\<Rightarrow> ts'; ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'; ts' \<^bold>\<leadsto> ts''; ts0 \<^bold>\<Rightarrow> ts1\<rbrakk> \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts''
 2. \<And>ts' ts''. \<lbrakk>ts1 \<^bold>\<Rightarrow> ts'; ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'; \<exists>c n. ts' \<^bold>\<midarrow>c( c, n ) \<^bold>\<rightarrow> ts''; ts0 \<^bold>\<Rightarrow> ts1\<rbrakk> \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts''
 3. \<And>ts' ts''. \<lbrakk>ts1 \<^bold>\<Rightarrow> ts'; ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'; \<exists>c. ts' \<^bold>\<midarrow>wdc( c ) \<^bold>\<rightarrow> ts''; ts0 \<^bold>\<Rightarrow> ts1\<rbrakk> \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts''
 4. \<And>ts' ts''. \<lbrakk>ts1 \<^bold>\<Rightarrow> ts'; ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'; \<exists>c. ts' \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts''; ts0 \<^bold>\<Rightarrow> ts1\<rbrakk> \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts''
 5. \<And>ts' ts''. \<lbrakk>ts1 \<^bold>\<Rightarrow> ts'; ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'; \<exists>c n. ts' \<^bold>\<midarrow>wdr( c, n ) \<^bold>\<rightarrow> ts''; ts0 \<^bold>\<Rightarrow> ts1\<rbrakk> \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts''
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ts1 \<^bold>\<Rightarrow> ts'
ts' \<^bold>\<leadsto> ts''
ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'
ts0 \<^bold>\<Rightarrow> ts1
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
ts1 \<^bold>\<Rightarrow> ts'
ts' \<^bold>\<leadsto> ts''
ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'
ts0 \<^bold>\<Rightarrow> ts1

goal (1 subgoal):
 1. ts0 \<^bold>\<Rightarrow> ts''
[PROOF STEP]
using traffic.evolve
[PROOF STATE]
proof (prove)
using this:
ts1 \<^bold>\<Rightarrow> ts'
ts' \<^bold>\<leadsto> ts''
ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'
ts0 \<^bold>\<Rightarrow> ts1
\<lbrakk>?ts \<^bold>\<Rightarrow> ?ts'; ?ts' \<^bold>\<leadsto> ?ts''\<rbrakk> \<Longrightarrow> ?ts \<^bold>\<Rightarrow> ?ts''

goal (1 subgoal):
 1. ts0 \<^bold>\<Rightarrow> ts''
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ts0 \<^bold>\<Rightarrow> ts''

goal (4 subgoals):
 1. \<And>ts' ts''. \<lbrakk>ts1 \<^bold>\<Rightarrow> ts'; ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'; \<exists>c n. ts' \<^bold>\<midarrow>c( c, n ) \<^bold>\<rightarrow> ts''; ts0 \<^bold>\<Rightarrow> ts1\<rbrakk> \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts''
 2. \<And>ts' ts''. \<lbrakk>ts1 \<^bold>\<Rightarrow> ts'; ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'; \<exists>c. ts' \<^bold>\<midarrow>wdc( c ) \<^bold>\<rightarrow> ts''; ts0 \<^bold>\<Rightarrow> ts1\<rbrakk> \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts''
 3. \<And>ts' ts''. \<lbrakk>ts1 \<^bold>\<Rightarrow> ts'; ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'; \<exists>c. ts' \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts''; ts0 \<^bold>\<Rightarrow> ts1\<rbrakk> \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts''
 4. \<And>ts' ts''. \<lbrakk>ts1 \<^bold>\<Rightarrow> ts'; ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'; \<exists>c n. ts' \<^bold>\<midarrow>wdr( c, n ) \<^bold>\<rightarrow> ts''; ts0 \<^bold>\<Rightarrow> ts1\<rbrakk> \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts''
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>ts' ts''. \<lbrakk>ts1 \<^bold>\<Rightarrow> ts'; ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'; \<exists>c n. ts' \<^bold>\<midarrow>c( c, n ) \<^bold>\<rightarrow> ts''; ts0 \<^bold>\<Rightarrow> ts1\<rbrakk> \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts''
 2. \<And>ts' ts''. \<lbrakk>ts1 \<^bold>\<Rightarrow> ts'; ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'; \<exists>c. ts' \<^bold>\<midarrow>wdc( c ) \<^bold>\<rightarrow> ts''; ts0 \<^bold>\<Rightarrow> ts1\<rbrakk> \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts''
 3. \<And>ts' ts''. \<lbrakk>ts1 \<^bold>\<Rightarrow> ts'; ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'; \<exists>c. ts' \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts''; ts0 \<^bold>\<Rightarrow> ts1\<rbrakk> \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts''
 4. \<And>ts' ts''. \<lbrakk>ts1 \<^bold>\<Rightarrow> ts'; ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'; \<exists>c n. ts' \<^bold>\<midarrow>wdr( c, n ) \<^bold>\<rightarrow> ts''; ts0 \<^bold>\<Rightarrow> ts1\<rbrakk> \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts''
[PROOF STEP]
case (cr_clm ts' ts'')
[PROOF STATE]
proof (state)
this:
ts1 \<^bold>\<Rightarrow> ts'
\<exists>c n. ts' \<^bold>\<midarrow>c( c, n ) \<^bold>\<rightarrow> ts''
ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'
ts0 \<^bold>\<Rightarrow> ts1

goal (4 subgoals):
 1. \<And>ts' ts''. \<lbrakk>ts1 \<^bold>\<Rightarrow> ts'; ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'; \<exists>c n. ts' \<^bold>\<midarrow>c( c, n ) \<^bold>\<rightarrow> ts''; ts0 \<^bold>\<Rightarrow> ts1\<rbrakk> \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts''
 2. \<And>ts' ts''. \<lbrakk>ts1 \<^bold>\<Rightarrow> ts'; ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'; \<exists>c. ts' \<^bold>\<midarrow>wdc( c ) \<^bold>\<rightarrow> ts''; ts0 \<^bold>\<Rightarrow> ts1\<rbrakk> \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts''
 3. \<And>ts' ts''. \<lbrakk>ts1 \<^bold>\<Rightarrow> ts'; ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'; \<exists>c. ts' \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts''; ts0 \<^bold>\<Rightarrow> ts1\<rbrakk> \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts''
 4. \<And>ts' ts''. \<lbrakk>ts1 \<^bold>\<Rightarrow> ts'; ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'; \<exists>c n. ts' \<^bold>\<midarrow>wdr( c, n ) \<^bold>\<rightarrow> ts''; ts0 \<^bold>\<Rightarrow> ts1\<rbrakk> \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts''
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ts1 \<^bold>\<Rightarrow> ts'
\<exists>c n. ts' \<^bold>\<midarrow>c( c, n ) \<^bold>\<rightarrow> ts''
ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'
ts0 \<^bold>\<Rightarrow> ts1
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
ts1 \<^bold>\<Rightarrow> ts'
\<exists>c n. ts' \<^bold>\<midarrow>c( c, n ) \<^bold>\<rightarrow> ts''
ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'
ts0 \<^bold>\<Rightarrow> ts1

goal (1 subgoal):
 1. ts0 \<^bold>\<Rightarrow> ts''
[PROOF STEP]
using traffic.cr_clm
[PROOF STATE]
proof (prove)
using this:
ts1 \<^bold>\<Rightarrow> ts'
\<exists>c n. ts' \<^bold>\<midarrow>c( c, n ) \<^bold>\<rightarrow> ts''
ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'
ts0 \<^bold>\<Rightarrow> ts1
\<lbrakk>?ts \<^bold>\<Rightarrow> ?ts'; \<exists>c n. ?ts' \<^bold>\<midarrow>c( c, n ) \<^bold>\<rightarrow> ?ts''\<rbrakk> \<Longrightarrow> ?ts \<^bold>\<Rightarrow> ?ts''

goal (1 subgoal):
 1. ts0 \<^bold>\<Rightarrow> ts''
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ts0 \<^bold>\<Rightarrow> ts''

goal (3 subgoals):
 1. \<And>ts' ts''. \<lbrakk>ts1 \<^bold>\<Rightarrow> ts'; ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'; \<exists>c. ts' \<^bold>\<midarrow>wdc( c ) \<^bold>\<rightarrow> ts''; ts0 \<^bold>\<Rightarrow> ts1\<rbrakk> \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts''
 2. \<And>ts' ts''. \<lbrakk>ts1 \<^bold>\<Rightarrow> ts'; ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'; \<exists>c. ts' \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts''; ts0 \<^bold>\<Rightarrow> ts1\<rbrakk> \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts''
 3. \<And>ts' ts''. \<lbrakk>ts1 \<^bold>\<Rightarrow> ts'; ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'; \<exists>c n. ts' \<^bold>\<midarrow>wdr( c, n ) \<^bold>\<rightarrow> ts''; ts0 \<^bold>\<Rightarrow> ts1\<rbrakk> \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts''
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>ts' ts''. \<lbrakk>ts1 \<^bold>\<Rightarrow> ts'; ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'; \<exists>c. ts' \<^bold>\<midarrow>wdc( c ) \<^bold>\<rightarrow> ts''; ts0 \<^bold>\<Rightarrow> ts1\<rbrakk> \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts''
 2. \<And>ts' ts''. \<lbrakk>ts1 \<^bold>\<Rightarrow> ts'; ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'; \<exists>c. ts' \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts''; ts0 \<^bold>\<Rightarrow> ts1\<rbrakk> \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts''
 3. \<And>ts' ts''. \<lbrakk>ts1 \<^bold>\<Rightarrow> ts'; ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'; \<exists>c n. ts' \<^bold>\<midarrow>wdr( c, n ) \<^bold>\<rightarrow> ts''; ts0 \<^bold>\<Rightarrow> ts1\<rbrakk> \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts''
[PROOF STEP]
case (wd_clm ts' ts'')
[PROOF STATE]
proof (state)
this:
ts1 \<^bold>\<Rightarrow> ts'
\<exists>c. ts' \<^bold>\<midarrow>wdc( c ) \<^bold>\<rightarrow> ts''
ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'
ts0 \<^bold>\<Rightarrow> ts1

goal (3 subgoals):
 1. \<And>ts' ts''. \<lbrakk>ts1 \<^bold>\<Rightarrow> ts'; ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'; \<exists>c. ts' \<^bold>\<midarrow>wdc( c ) \<^bold>\<rightarrow> ts''; ts0 \<^bold>\<Rightarrow> ts1\<rbrakk> \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts''
 2. \<And>ts' ts''. \<lbrakk>ts1 \<^bold>\<Rightarrow> ts'; ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'; \<exists>c. ts' \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts''; ts0 \<^bold>\<Rightarrow> ts1\<rbrakk> \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts''
 3. \<And>ts' ts''. \<lbrakk>ts1 \<^bold>\<Rightarrow> ts'; ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'; \<exists>c n. ts' \<^bold>\<midarrow>wdr( c, n ) \<^bold>\<rightarrow> ts''; ts0 \<^bold>\<Rightarrow> ts1\<rbrakk> \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts''
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ts1 \<^bold>\<Rightarrow> ts'
\<exists>c. ts' \<^bold>\<midarrow>wdc( c ) \<^bold>\<rightarrow> ts''
ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'
ts0 \<^bold>\<Rightarrow> ts1
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
ts1 \<^bold>\<Rightarrow> ts'
\<exists>c. ts' \<^bold>\<midarrow>wdc( c ) \<^bold>\<rightarrow> ts''
ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'
ts0 \<^bold>\<Rightarrow> ts1

goal (1 subgoal):
 1. ts0 \<^bold>\<Rightarrow> ts''
[PROOF STEP]
using traffic.wd_clm
[PROOF STATE]
proof (prove)
using this:
ts1 \<^bold>\<Rightarrow> ts'
\<exists>c. ts' \<^bold>\<midarrow>wdc( c ) \<^bold>\<rightarrow> ts''
ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'
ts0 \<^bold>\<Rightarrow> ts1
\<lbrakk>?ts \<^bold>\<Rightarrow> ?ts'; \<exists>c. ?ts' \<^bold>\<midarrow>wdc( c ) \<^bold>\<rightarrow> ?ts''\<rbrakk> \<Longrightarrow> ?ts \<^bold>\<Rightarrow> ?ts''

goal (1 subgoal):
 1. ts0 \<^bold>\<Rightarrow> ts''
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ts0 \<^bold>\<Rightarrow> ts''

goal (2 subgoals):
 1. \<And>ts' ts''. \<lbrakk>ts1 \<^bold>\<Rightarrow> ts'; ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'; \<exists>c. ts' \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts''; ts0 \<^bold>\<Rightarrow> ts1\<rbrakk> \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts''
 2. \<And>ts' ts''. \<lbrakk>ts1 \<^bold>\<Rightarrow> ts'; ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'; \<exists>c n. ts' \<^bold>\<midarrow>wdr( c, n ) \<^bold>\<rightarrow> ts''; ts0 \<^bold>\<Rightarrow> ts1\<rbrakk> \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts''
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ts' ts''. \<lbrakk>ts1 \<^bold>\<Rightarrow> ts'; ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'; \<exists>c. ts' \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts''; ts0 \<^bold>\<Rightarrow> ts1\<rbrakk> \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts''
 2. \<And>ts' ts''. \<lbrakk>ts1 \<^bold>\<Rightarrow> ts'; ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'; \<exists>c n. ts' \<^bold>\<midarrow>wdr( c, n ) \<^bold>\<rightarrow> ts''; ts0 \<^bold>\<Rightarrow> ts1\<rbrakk> \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts''
[PROOF STEP]
case (cr_res ts' ts'')
[PROOF STATE]
proof (state)
this:
ts1 \<^bold>\<Rightarrow> ts'
\<exists>c. ts' \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts''
ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'
ts0 \<^bold>\<Rightarrow> ts1

goal (2 subgoals):
 1. \<And>ts' ts''. \<lbrakk>ts1 \<^bold>\<Rightarrow> ts'; ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'; \<exists>c. ts' \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts''; ts0 \<^bold>\<Rightarrow> ts1\<rbrakk> \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts''
 2. \<And>ts' ts''. \<lbrakk>ts1 \<^bold>\<Rightarrow> ts'; ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'; \<exists>c n. ts' \<^bold>\<midarrow>wdr( c, n ) \<^bold>\<rightarrow> ts''; ts0 \<^bold>\<Rightarrow> ts1\<rbrakk> \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts''
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ts1 \<^bold>\<Rightarrow> ts'
\<exists>c. ts' \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts''
ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'
ts0 \<^bold>\<Rightarrow> ts1
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
ts1 \<^bold>\<Rightarrow> ts'
\<exists>c. ts' \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts''
ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'
ts0 \<^bold>\<Rightarrow> ts1

goal (1 subgoal):
 1. ts0 \<^bold>\<Rightarrow> ts''
[PROOF STEP]
using traffic.cr_res
[PROOF STATE]
proof (prove)
using this:
ts1 \<^bold>\<Rightarrow> ts'
\<exists>c. ts' \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts''
ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'
ts0 \<^bold>\<Rightarrow> ts1
\<lbrakk>?ts \<^bold>\<Rightarrow> ?ts'; \<exists>c. ?ts' \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ?ts''\<rbrakk> \<Longrightarrow> ?ts \<^bold>\<Rightarrow> ?ts''

goal (1 subgoal):
 1. ts0 \<^bold>\<Rightarrow> ts''
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ts0 \<^bold>\<Rightarrow> ts''

goal (1 subgoal):
 1. \<And>ts' ts''. \<lbrakk>ts1 \<^bold>\<Rightarrow> ts'; ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'; \<exists>c n. ts' \<^bold>\<midarrow>wdr( c, n ) \<^bold>\<rightarrow> ts''; ts0 \<^bold>\<Rightarrow> ts1\<rbrakk> \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts''
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ts' ts''. \<lbrakk>ts1 \<^bold>\<Rightarrow> ts'; ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'; \<exists>c n. ts' \<^bold>\<midarrow>wdr( c, n ) \<^bold>\<rightarrow> ts''; ts0 \<^bold>\<Rightarrow> ts1\<rbrakk> \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts''
[PROOF STEP]
case (wd_res ts' ts'')
[PROOF STATE]
proof (state)
this:
ts1 \<^bold>\<Rightarrow> ts'
\<exists>c n. ts' \<^bold>\<midarrow>wdr( c, n ) \<^bold>\<rightarrow> ts''
ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'
ts0 \<^bold>\<Rightarrow> ts1

goal (1 subgoal):
 1. \<And>ts' ts''. \<lbrakk>ts1 \<^bold>\<Rightarrow> ts'; ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'; \<exists>c n. ts' \<^bold>\<midarrow>wdr( c, n ) \<^bold>\<rightarrow> ts''; ts0 \<^bold>\<Rightarrow> ts1\<rbrakk> \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts''
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ts1 \<^bold>\<Rightarrow> ts'
\<exists>c n. ts' \<^bold>\<midarrow>wdr( c, n ) \<^bold>\<rightarrow> ts''
ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'
ts0 \<^bold>\<Rightarrow> ts1
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
ts1 \<^bold>\<Rightarrow> ts'
\<exists>c n. ts' \<^bold>\<midarrow>wdr( c, n ) \<^bold>\<rightarrow> ts''
ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'
ts0 \<^bold>\<Rightarrow> ts1

goal (1 subgoal):
 1. ts0 \<^bold>\<Rightarrow> ts''
[PROOF STEP]
using traffic.wd_res
[PROOF STATE]
proof (prove)
using this:
ts1 \<^bold>\<Rightarrow> ts'
\<exists>c n. ts' \<^bold>\<midarrow>wdr( c, n ) \<^bold>\<rightarrow> ts''
ts0 \<^bold>\<Rightarrow> ts1 \<Longrightarrow> ts0 \<^bold>\<Rightarrow> ts'
ts0 \<^bold>\<Rightarrow> ts1
\<lbrakk>?ts \<^bold>\<Rightarrow> ?ts'; \<exists>c n. ?ts' \<^bold>\<midarrow>wdr( c, n ) \<^bold>\<rightarrow> ?ts''\<rbrakk> \<Longrightarrow> ?ts \<^bold>\<Rightarrow> ?ts''

goal (1 subgoal):
 1. ts0 \<^bold>\<Rightarrow> ts''
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ts0 \<^bold>\<Rightarrow> ts''

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma create_res_subseteq1:"(ts \<^bold>\<midarrow>r(c)\<^bold>\<rightarrow> ts') \<longrightarrow> res ts c \<sqsubseteq> res ts' c "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ts \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts' \<longrightarrow> res ts c \<le> res ts' c
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ts \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts' \<Longrightarrow> res ts c \<le> res ts' c
[PROOF STEP]
assume assm:"(ts \<^bold>\<midarrow>r(c)\<^bold>\<rightarrow> ts')"
[PROOF STATE]
proof (state)
this:
ts \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts'

goal (1 subgoal):
 1. ts \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts' \<Longrightarrow> res ts c \<le> res ts' c
[PROOF STEP]
hence "res ts' c = res ts c \<squnion> clm ts c"
[PROOF STATE]
proof (prove)
using this:
ts \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts'

goal (1 subgoal):
 1. res ts' c = res ts c \<squnion> clm ts c
[PROOF STEP]
using create_reservation_def
[PROOF STATE]
proof (prove)
using this:
ts \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts'
?ts \<^bold>\<midarrow>r( ?c ) \<^bold>\<rightarrow> ?ts' \<equiv> pos ?ts' = pos ?ts \<and> res ?ts' = (res ?ts)(?c := res ?ts ?c \<squnion> clm ?ts ?c) \<and> dyn ?ts' = dyn ?ts \<and> clm ?ts' = (clm ?ts)(?c := bot) \<and> physical_size ?ts' = physical_size ?ts \<and> braking_distance ?ts' = braking_distance ?ts

goal (1 subgoal):
 1. res ts' c = res ts c \<squnion> clm ts c
[PROOF STEP]
using fun_upd_apply
[PROOF STATE]
proof (prove)
using this:
ts \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts'
?ts \<^bold>\<midarrow>r( ?c ) \<^bold>\<rightarrow> ?ts' \<equiv> pos ?ts' = pos ?ts \<and> res ?ts' = (res ?ts)(?c := res ?ts ?c \<squnion> clm ?ts ?c) \<and> dyn ?ts' = dyn ?ts \<and> clm ?ts' = (clm ?ts)(?c := bot) \<and> physical_size ?ts' = physical_size ?ts \<and> braking_distance ?ts' = braking_distance ?ts
(?f(?x := ?y)) ?z = (if ?z = ?x then ?y else ?f ?z)

goal (1 subgoal):
 1. res ts' c = res ts c \<squnion> clm ts c
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
res ts' c = res ts c \<squnion> clm ts c

goal (1 subgoal):
 1. ts \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts' \<Longrightarrow> res ts c \<le> res ts' c
[PROOF STEP]
thus "res ts c \<sqsubseteq> res ts' c"
[PROOF STATE]
proof (prove)
using this:
res ts' c = res ts c \<squnion> clm ts c

goal (1 subgoal):
 1. res ts c \<le> res ts' c
[PROOF STEP]
by (metis (no_types, lifting) Un_commute clm_consec_res  nat_int.un_subset2
        nat_int.union_def nat_int.chop_subset1 nat_int.nchop_def)
[PROOF STATE]
proof (state)
this:
res ts c \<le> res ts' c

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma create_res_subseteq2:"(ts \<^bold>\<midarrow>r(c)\<^bold>\<rightarrow> ts') \<longrightarrow> clm ts c \<sqsubseteq> res ts' c "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ts \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts' \<longrightarrow> clm ts c \<le> res ts' c
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ts \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts' \<Longrightarrow> clm ts c \<le> res ts' c
[PROOF STEP]
assume assm:"(ts \<^bold>\<midarrow>r(c)\<^bold>\<rightarrow> ts')"
[PROOF STATE]
proof (state)
this:
ts \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts'

goal (1 subgoal):
 1. ts \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts' \<Longrightarrow> clm ts c \<le> res ts' c
[PROOF STEP]
hence "res ts' c = res ts c \<squnion> clm ts c"
[PROOF STATE]
proof (prove)
using this:
ts \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts'

goal (1 subgoal):
 1. res ts' c = res ts c \<squnion> clm ts c
[PROOF STEP]
using create_reservation_def
[PROOF STATE]
proof (prove)
using this:
ts \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts'
?ts \<^bold>\<midarrow>r( ?c ) \<^bold>\<rightarrow> ?ts' \<equiv> pos ?ts' = pos ?ts \<and> res ?ts' = (res ?ts)(?c := res ?ts ?c \<squnion> clm ?ts ?c) \<and> dyn ?ts' = dyn ?ts \<and> clm ?ts' = (clm ?ts)(?c := bot) \<and> physical_size ?ts' = physical_size ?ts \<and> braking_distance ?ts' = braking_distance ?ts

goal (1 subgoal):
 1. res ts' c = res ts c \<squnion> clm ts c
[PROOF STEP]
using fun_upd_apply
[PROOF STATE]
proof (prove)
using this:
ts \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts'
?ts \<^bold>\<midarrow>r( ?c ) \<^bold>\<rightarrow> ?ts' \<equiv> pos ?ts' = pos ?ts \<and> res ?ts' = (res ?ts)(?c := res ?ts ?c \<squnion> clm ?ts ?c) \<and> dyn ?ts' = dyn ?ts \<and> clm ?ts' = (clm ?ts)(?c := bot) \<and> physical_size ?ts' = physical_size ?ts \<and> braking_distance ?ts' = braking_distance ?ts
(?f(?x := ?y)) ?z = (if ?z = ?x then ?y else ?f ?z)

goal (1 subgoal):
 1. res ts' c = res ts c \<squnion> clm ts c
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
res ts' c = res ts c \<squnion> clm ts c

goal (1 subgoal):
 1. ts \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts' \<Longrightarrow> clm ts c \<le> res ts' c
[PROOF STEP]
thus "clm ts c \<sqsubseteq> res ts' c"
[PROOF STATE]
proof (prove)
using this:
res ts' c = res ts c \<squnion> clm ts c

goal (1 subgoal):
 1. clm ts c \<le> res ts' c
[PROOF STEP]
by (metis Un_commute clm_consec_res disjoint inf_le1 nat_int.un_subset1 nat_int.un_subset2
        nat_int.union_def)
[PROOF STATE]
proof (state)
this:
clm ts c \<le> res ts' c

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma create_res_subseteq1_neq:"(ts \<^bold>\<midarrow>r(d)\<^bold>\<rightarrow> ts') \<and> d \<noteq>c \<longrightarrow> res ts c = res ts' c "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ts \<^bold>\<midarrow>r( d ) \<^bold>\<rightarrow> ts') \<and> d \<noteq> c \<longrightarrow> res ts c = res ts' c
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (ts \<^bold>\<midarrow>r( d ) \<^bold>\<rightarrow> ts') \<and> d \<noteq> c \<Longrightarrow> res ts c = res ts' c
[PROOF STEP]
assume assm:"(ts \<^bold>\<midarrow>r(d)\<^bold>\<rightarrow> ts') \<and> d \<noteq>c"
[PROOF STATE]
proof (state)
this:
(ts \<^bold>\<midarrow>r( d ) \<^bold>\<rightarrow> ts') \<and> d \<noteq> c

goal (1 subgoal):
 1. (ts \<^bold>\<midarrow>r( d ) \<^bold>\<rightarrow> ts') \<and> d \<noteq> c \<Longrightarrow> res ts c = res ts' c
[PROOF STEP]
thus "res ts c = res ts' c"
[PROOF STATE]
proof (prove)
using this:
(ts \<^bold>\<midarrow>r( d ) \<^bold>\<rightarrow> ts') \<and> d \<noteq> c

goal (1 subgoal):
 1. res ts c = res ts' c
[PROOF STEP]
using create_reservation_def
[PROOF STATE]
proof (prove)
using this:
(ts \<^bold>\<midarrow>r( d ) \<^bold>\<rightarrow> ts') \<and> d \<noteq> c
?ts \<^bold>\<midarrow>r( ?c ) \<^bold>\<rightarrow> ?ts' \<equiv> pos ?ts' = pos ?ts \<and> res ?ts' = (res ?ts)(?c := res ?ts ?c \<squnion> clm ?ts ?c) \<and> dyn ?ts' = dyn ?ts \<and> clm ?ts' = (clm ?ts)(?c := bot) \<and> physical_size ?ts' = physical_size ?ts \<and> braking_distance ?ts' = braking_distance ?ts

goal (1 subgoal):
 1. res ts c = res ts' c
[PROOF STEP]
using fun_upd_apply
[PROOF STATE]
proof (prove)
using this:
(ts \<^bold>\<midarrow>r( d ) \<^bold>\<rightarrow> ts') \<and> d \<noteq> c
?ts \<^bold>\<midarrow>r( ?c ) \<^bold>\<rightarrow> ?ts' \<equiv> pos ?ts' = pos ?ts \<and> res ?ts' = (res ?ts)(?c := res ?ts ?c \<squnion> clm ?ts ?c) \<and> dyn ?ts' = dyn ?ts \<and> clm ?ts' = (clm ?ts)(?c := bot) \<and> physical_size ?ts' = physical_size ?ts \<and> braking_distance ?ts' = braking_distance ?ts
(?f(?x := ?y)) ?z = (if ?z = ?x then ?y else ?f ?z)

goal (1 subgoal):
 1. res ts c = res ts' c
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
res ts c = res ts' c

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma create_res_subseteq2_neq:"(ts \<^bold>\<midarrow>r(d)\<^bold>\<rightarrow> ts') \<and> d \<noteq>c \<longrightarrow> clm ts c= clm ts' c "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ts \<^bold>\<midarrow>r( d ) \<^bold>\<rightarrow> ts') \<and> d \<noteq> c \<longrightarrow> clm ts c = clm ts' c
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (ts \<^bold>\<midarrow>r( d ) \<^bold>\<rightarrow> ts') \<and> d \<noteq> c \<Longrightarrow> clm ts c = clm ts' c
[PROOF STEP]
assume assm:"(ts \<^bold>\<midarrow>r(d)\<^bold>\<rightarrow> ts') \<and> d \<noteq>c"
[PROOF STATE]
proof (state)
this:
(ts \<^bold>\<midarrow>r( d ) \<^bold>\<rightarrow> ts') \<and> d \<noteq> c

goal (1 subgoal):
 1. (ts \<^bold>\<midarrow>r( d ) \<^bold>\<rightarrow> ts') \<and> d \<noteq> c \<Longrightarrow> clm ts c = clm ts' c
[PROOF STEP]
thus "clm ts c =  clm ts' c"
[PROOF STATE]
proof (prove)
using this:
(ts \<^bold>\<midarrow>r( d ) \<^bold>\<rightarrow> ts') \<and> d \<noteq> c

goal (1 subgoal):
 1. clm ts c = clm ts' c
[PROOF STEP]
using create_reservation_def
[PROOF STATE]
proof (prove)
using this:
(ts \<^bold>\<midarrow>r( d ) \<^bold>\<rightarrow> ts') \<and> d \<noteq> c
?ts \<^bold>\<midarrow>r( ?c ) \<^bold>\<rightarrow> ?ts' \<equiv> pos ?ts' = pos ?ts \<and> res ?ts' = (res ?ts)(?c := res ?ts ?c \<squnion> clm ?ts ?c) \<and> dyn ?ts' = dyn ?ts \<and> clm ?ts' = (clm ?ts)(?c := bot) \<and> physical_size ?ts' = physical_size ?ts \<and> braking_distance ?ts' = braking_distance ?ts

goal (1 subgoal):
 1. clm ts c = clm ts' c
[PROOF STEP]
using fun_upd_apply
[PROOF STATE]
proof (prove)
using this:
(ts \<^bold>\<midarrow>r( d ) \<^bold>\<rightarrow> ts') \<and> d \<noteq> c
?ts \<^bold>\<midarrow>r( ?c ) \<^bold>\<rightarrow> ?ts' \<equiv> pos ?ts' = pos ?ts \<and> res ?ts' = (res ?ts)(?c := res ?ts ?c \<squnion> clm ?ts ?c) \<and> dyn ?ts' = dyn ?ts \<and> clm ?ts' = (clm ?ts)(?c := bot) \<and> physical_size ?ts' = physical_size ?ts \<and> braking_distance ?ts' = braking_distance ?ts
(?f(?x := ?y)) ?z = (if ?z = ?x then ?y else ?f ?z)

goal (1 subgoal):
 1. clm ts c = clm ts' c
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
clm ts c = clm ts' c

goal:
No subgoals!
[PROOF STEP]
qed