[STATEMENT]
lemma devBC_some[simp]: assumes "\<parallel>nid\<parallel>\<^bsub>t n\<^esub>" shows "devBC t n nid n = Some nid"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. devBC t n nid n = Some nid
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. devBC t n nid n = Some nid
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<parallel>nid\<parallel>\<^bsub>t n\<^esub>
[PROOF STEP]
have "(n, nid)\<in> his t n nid"
[PROOF STATE]
proof (prove)
using this:
\<parallel>nid\<parallel>\<^bsub>t n\<^esub>

goal (1 subgoal):
 1. (n, nid) \<in> his t n nid
[PROOF STEP]
using his.intros(1)
[PROOF STATE]
proof (prove)
using this:
\<parallel>nid\<parallel>\<^bsub>t n\<^esub>
\<parallel>?nid\<parallel>\<^bsub>?t ?n\<^esub> \<Longrightarrow> (?n, ?nid) \<in> his ?t ?n ?nid

goal (1 subgoal):
 1. (n, nid) \<in> his t n nid
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(n, nid) \<in> his t n nid

goal (1 subgoal):
 1. devBC t n nid n = Some nid
[PROOF STEP]
hence "devBC t n nid n = (Some (THE nid'. (n, nid')\<in>his t n nid))"
[PROOF STATE]
proof (prove)
using this:
(n, nid) \<in> his t n nid

goal (1 subgoal):
 1. devBC t n nid n = Some (THE nid'. (n, nid') \<in> his t n nid)
[PROOF STEP]
using devBC_def
[PROOF STATE]
proof (prove)
using this:
(n, nid) \<in> his t n nid
devBC ?t ?n ?nid ?n' \<equiv> if \<exists>nid'. (?n', nid') \<in> his ?t ?n ?nid then Some (THE nid'. (?n', nid') \<in> his ?t ?n ?nid) else None

goal (1 subgoal):
 1. devBC t n nid n = Some (THE nid'. (n, nid') \<in> his t n nid)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
devBC t n nid n = Some (THE nid'. (n, nid') \<in> his t n nid)

goal (1 subgoal):
 1. devBC t n nid n = Some nid
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
devBC t n nid n = Some (THE nid'. (n, nid') \<in> his t n nid)

goal (1 subgoal):
 1. devBC t n nid n = Some nid
[PROOF STEP]
have "(THE nid'. (n, nid')\<in>his t n nid) = nid"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (THE nid'. (n, nid') \<in> his t n nid) = nid
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (n, nid) \<in> his t n nid
 2. \<And>nid'. (n, nid') \<in> his t n nid \<Longrightarrow> nid' = nid
[PROOF STEP]
from \<open>(n, nid)\<in> his t n nid\<close>
[PROOF STATE]
proof (chain)
picking this:
(n, nid) \<in> his t n nid
[PROOF STEP]
show "(n, nid)\<in> his t n nid"
[PROOF STATE]
proof (prove)
using this:
(n, nid) \<in> his t n nid

goal (1 subgoal):
 1. (n, nid) \<in> his t n nid
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(n, nid) \<in> his t n nid

goal (1 subgoal):
 1. \<And>nid'. (n, nid') \<in> his t n nid \<Longrightarrow> nid' = nid
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>nid'. (n, nid') \<in> his t n nid \<Longrightarrow> nid' = nid
[PROOF STEP]
fix nid'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>nid'. (n, nid') \<in> his t n nid \<Longrightarrow> nid' = nid
[PROOF STEP]
assume "(n, nid') \<in> his t n nid"
[PROOF STATE]
proof (state)
this:
(n, nid') \<in> his t n nid

goal (1 subgoal):
 1. \<And>nid'. (n, nid') \<in> his t n nid \<Longrightarrow> nid' = nid
[PROOF STEP]
thus "nid' = nid"
[PROOF STATE]
proof (prove)
using this:
(n, nid') \<in> his t n nid

goal (1 subgoal):
 1. nid' = nid
[PROOF STEP]
using his_determ_base
[PROOF STATE]
proof (prove)
using this:
(n, nid') \<in> his t n nid
(?n, ?nid') \<in> his ?t ?n ?nid \<Longrightarrow> ?nid' = ?nid

goal (1 subgoal):
 1. nid' = nid
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
nid' = nid

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(THE nid'. (n, nid') \<in> his t n nid) = nid

goal (1 subgoal):
 1. devBC t n nid n = Some nid
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
devBC t n nid n = Some (THE nid'. (n, nid') \<in> his t n nid)
(THE nid'. (n, nid') \<in> his t n nid) = nid
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
devBC t n nid n = Some (THE nid'. (n, nid') \<in> his t n nid)
(THE nid'. (n, nid') \<in> his t n nid) = nid

goal (1 subgoal):
 1. devBC t n nid n = Some nid
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
devBC t n nid n = Some nid

goal:
No subgoals!
[PROOF STEP]
qed