theory TcbQueue_C

lemma tcb_queue_relation_ptr_rel:
  assumes   tq: "tcb_queue_relation getNext getPrev mp queue qprev qhead"
  and valid_ep: "\<forall>t\<in>set queue. tcb_at' t s" "distinct queue"
  and   cs_tcb: "mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb"
  and prev_not_queue: "ctcb_ptr_to_tcb_ptr qprev \<notin> set queue"
  and in_queue: "tcbp \<in> set queue"
  shows "tcb_ptr_to_ctcb_ptr tcbp \<noteq> getNext tcb \<and> tcb_ptr_to_ctcb_ptr tcbp \<noteq> getPrev tcb
         \<and> (getNext tcb \<noteq> NULL \<longrightarrow> getNext tcb \<noteq> getPrev tcb)" using tq valid_ep in_queue cs_tcb prev_not_queue apply - apply (frule (3) tcb_queueD) apply (frule (2) tcb_queue_relation_not_NULL') apply (simp split: if_split_asm) apply (rule not_sym) apply (rule notI) apply simp apply (clarsimp simp: inj_eq distinct_conv_nth) apply (intro conjI impI) apply (clarsimp simp: inj_eq distinct_conv_nth) apply (rule not_sym) apply clarsimp apply clarsimp apply (clarsimp simp: inj_eq) apply (intro conjI impI) apply (clarsimp simp: distinct_conv_nth) apply (erule_tac s = "queue ! Suc n" in subst) apply (clarsimp simp: distinct_conv_nth) apply clarsimp apply (case_tac "na = Suc n") apply hypsubst apply (clarsimp simp: distinct_conv_nth) apply (clarsimp simp: distinct_conv_nth) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_ptr_to_ctcb_ptr tcbp \<noteq> getNext tcb \<and> tcb_ptr_to_ctcb_ptr tcbp \<noteq> getPrev tcb \<and> (getNext tcb \<noteq> NULL \<longrightarrow> getNext tcb \<noteq> getPrev tcb) proof (prove)
using this:
tcb_queue_relation getNext getPrev mp queue qprev qhead
\<forall>t\<in>set queue. tcb_at' t s
distinct queue
tcbp \<in> set queue
mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb
ctcb_ptr_to_tcb_ptr qprev \<notin> set queue

goal (1 subgoal):
 1. tcb_ptr_to_ctcb_ptr tcbp \<noteq> getNext tcb \<and> tcb_ptr_to_ctcb_ptr tcbp \<noteq> getPrev tcb \<and> (getNext tcb \<noteq> NULL \<longrightarrow> getNext tcb \<noteq> getPrev tcb) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_queue_relation getNext getPrev mp queue qprev qhead; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; tcbp \<in> set queue; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; ctcb_ptr_to_tcb_ptr qprev \<notin> set queue\<rbrakk> \<Longrightarrow> tcb_ptr_to_ctcb_ptr tcbp \<noteq> getNext tcb \<and> tcb_ptr_to_ctcb_ptr tcbp \<noteq> getPrev tcb \<and> (getNext tcb \<noteq> NULL \<longrightarrow> getNext tcb \<noteq> getPrev tcb) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_queue_relation getNext getPrev mp queue qprev qhead; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; tcbp \<in> set queue; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; ctcb_ptr_to_tcb_ptr qprev \<notin> set queue; (if tcbp = hd queue then getPrev tcb = qprev else \<exists>n<length queue - 1. getPrev tcb = tcb_ptr_to_ctcb_ptr (queue ! n) \<and> tcbp = queue ! Suc n) \<and> (if tcbp = last queue then getNext tcb = NULL else \<exists>n<length queue - 1. tcbp = queue ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n))\<rbrakk> \<Longrightarrow> tcb_ptr_to_ctcb_ptr tcbp \<noteq> getNext tcb \<and> tcb_ptr_to_ctcb_ptr tcbp \<noteq> getPrev tcb \<and> (getNext tcb \<noteq> NULL \<longrightarrow> getNext tcb \<noteq> getPrev tcb) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_queue_relation getNext getPrev mp queue qprev qhead; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; tcbp \<in> set queue; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; ctcb_ptr_to_tcb_ptr qprev \<notin> set queue; (if tcbp = hd queue then getPrev tcb = qprev else \<exists>n<length queue - 1. getPrev tcb = tcb_ptr_to_ctcb_ptr (queue ! n) \<and> tcbp = queue ! Suc n) \<and> (if tcbp = last queue then getNext tcb = NULL else \<exists>n<length queue - 1. tcbp = queue ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n)); tcb_ptr_to_ctcb_ptr tcbp \<noteq> NULL\<rbrakk> \<Longrightarrow> tcb_ptr_to_ctcb_ptr tcbp \<noteq> getNext tcb \<and> tcb_ptr_to_ctcb_ptr tcbp \<noteq> getPrev tcb \<and> (getNext tcb \<noteq> NULL \<longrightarrow> getNext tcb \<noteq> getPrev tcb) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>tcb_ptr_to_ctcb_ptr (hd queue) \<noteq> NULL; tcb_queue_relation getNext getPrev mp queue qprev qhead; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; hd queue \<in> set queue; mp (tcb_ptr_to_ctcb_ptr (hd queue)) = Some tcb; ctcb_ptr_to_tcb_ptr qprev \<notin> set queue; tcbp = hd queue; last queue = hd queue; getPrev tcb = qprev \<and> getNext tcb = NULL\<rbrakk> \<Longrightarrow> tcb_ptr_to_ctcb_ptr (hd queue) \<noteq> qprev
 2. \<lbrakk>tcb_ptr_to_ctcb_ptr (last queue) \<noteq> NULL; tcb_queue_relation getNext getPrev mp queue qprev qhead; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; last queue \<in> set queue; mp (tcb_ptr_to_ctcb_ptr (last queue)) = Some tcb; ctcb_ptr_to_tcb_ptr qprev \<notin> set queue; tcbp = last queue; last queue \<noteq> hd queue; (\<exists>n<length queue - Suc 0. getPrev tcb = tcb_ptr_to_ctcb_ptr (queue ! n) \<and> last queue = queue ! Suc n) \<and> getNext tcb = NULL\<rbrakk> \<Longrightarrow> tcb_ptr_to_ctcb_ptr (last queue) \<noteq> getPrev tcb
 3. \<lbrakk>tcb_ptr_to_ctcb_ptr (hd queue) \<noteq> NULL; tcb_queue_relation getNext getPrev mp queue qprev qhead; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; hd queue \<in> set queue; mp (tcb_ptr_to_ctcb_ptr (hd queue)) = Some tcb; ctcb_ptr_to_tcb_ptr qprev \<notin> set queue; hd queue \<noteq> last queue; tcbp = hd queue; getPrev tcb = qprev \<and> (\<exists>n<length queue - Suc 0. hd queue = queue ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n))\<rbrakk> \<Longrightarrow> tcb_ptr_to_ctcb_ptr (hd queue) \<noteq> getNext tcb \<and> tcb_ptr_to_ctcb_ptr (hd queue) \<noteq> qprev \<and> (getNext tcb \<noteq> NULL \<longrightarrow> getNext tcb \<noteq> qprev)
 4. \<lbrakk>tcb_ptr_to_ctcb_ptr tcbp \<noteq> NULL; tcb_queue_relation getNext getPrev mp queue qprev qhead; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; tcbp \<in> set queue; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; ctcb_ptr_to_tcb_ptr qprev \<notin> set queue; tcbp \<noteq> last queue; tcbp \<noteq> hd queue; (\<exists>n<length queue - Suc 0. getPrev tcb = tcb_ptr_to_ctcb_ptr (queue ! n) \<and> tcbp = queue ! Suc n) \<and> (\<exists>n<length queue - Suc 0. tcbp = queue ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n))\<rbrakk> \<Longrightarrow> tcb_ptr_to_ctcb_ptr tcbp \<noteq> getNext tcb \<and> tcb_ptr_to_ctcb_ptr tcbp \<noteq> getPrev tcb \<and> (getNext tcb \<noteq> NULL \<longrightarrow> getNext tcb \<noteq> getPrev tcb) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>tcb_ptr_to_ctcb_ptr (hd queue) \<noteq> NULL; tcb_queue_relation getNext getPrev mp queue qprev qhead; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; hd queue \<in> set queue; mp (tcb_ptr_to_ctcb_ptr (hd queue)) = Some tcb; ctcb_ptr_to_tcb_ptr qprev \<notin> set queue; tcbp = hd queue; last queue = hd queue; getPrev tcb = qprev \<and> getNext tcb = NULL\<rbrakk> \<Longrightarrow> qprev \<noteq> tcb_ptr_to_ctcb_ptr (hd queue)
 2. \<lbrakk>tcb_ptr_to_ctcb_ptr (last queue) \<noteq> NULL; tcb_queue_relation getNext getPrev mp queue qprev qhead; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; last queue \<in> set queue; mp (tcb_ptr_to_ctcb_ptr (last queue)) = Some tcb; ctcb_ptr_to_tcb_ptr qprev \<notin> set queue; tcbp = last queue; last queue \<noteq> hd queue; (\<exists>n<length queue - Suc 0. getPrev tcb = tcb_ptr_to_ctcb_ptr (queue ! n) \<and> last queue = queue ! Suc n) \<and> getNext tcb = NULL\<rbrakk> \<Longrightarrow> tcb_ptr_to_ctcb_ptr (last queue) \<noteq> getPrev tcb
 3. \<lbrakk>tcb_ptr_to_ctcb_ptr (hd queue) \<noteq> NULL; tcb_queue_relation getNext getPrev mp queue qprev qhead; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; hd queue \<in> set queue; mp (tcb_ptr_to_ctcb_ptr (hd queue)) = Some tcb; ctcb_ptr_to_tcb_ptr qprev \<notin> set queue; hd queue \<noteq> last queue; tcbp = hd queue; getPrev tcb = qprev \<and> (\<exists>n<length queue - Suc 0. hd queue = queue ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n))\<rbrakk> \<Longrightarrow> tcb_ptr_to_ctcb_ptr (hd queue) \<noteq> getNext tcb \<and> tcb_ptr_to_ctcb_ptr (hd queue) \<noteq> qprev \<and> (getNext tcb \<noteq> NULL \<longrightarrow> getNext tcb \<noteq> qprev)
 4. \<lbrakk>tcb_ptr_to_ctcb_ptr tcbp \<noteq> NULL; tcb_queue_relation getNext getPrev mp queue qprev qhead; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; tcbp \<in> set queue; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; ctcb_ptr_to_tcb_ptr qprev \<notin> set queue; tcbp \<noteq> last queue; tcbp \<noteq> hd queue; (\<exists>n<length queue - Suc 0. getPrev tcb = tcb_ptr_to_ctcb_ptr (queue ! n) \<and> tcbp = queue ! Suc n) \<and> (\<exists>n<length queue - Suc 0. tcbp = queue ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n))\<rbrakk> \<Longrightarrow> tcb_ptr_to_ctcb_ptr tcbp \<noteq> getNext tcb \<and> tcb_ptr_to_ctcb_ptr tcbp \<noteq> getPrev tcb \<and> (getNext tcb \<noteq> NULL \<longrightarrow> getNext tcb \<noteq> getPrev tcb) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>tcb_ptr_to_ctcb_ptr (hd queue) \<noteq> NULL; tcb_queue_relation getNext getPrev mp queue qprev qhead; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; hd queue \<in> set queue; mp (tcb_ptr_to_ctcb_ptr (hd queue)) = Some tcb; ctcb_ptr_to_tcb_ptr qprev \<notin> set queue; tcbp = hd queue; last queue = hd queue; getPrev tcb = qprev \<and> getNext tcb = NULL; qprev = tcb_ptr_to_ctcb_ptr (hd queue)\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>tcb_ptr_to_ctcb_ptr (last queue) \<noteq> NULL; tcb_queue_relation getNext getPrev mp queue qprev qhead; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; last queue \<in> set queue; mp (tcb_ptr_to_ctcb_ptr (last queue)) = Some tcb; ctcb_ptr_to_tcb_ptr qprev \<notin> set queue; tcbp = last queue; last queue \<noteq> hd queue; (\<exists>n<length queue - Suc 0. getPrev tcb = tcb_ptr_to_ctcb_ptr (queue ! n) \<and> last queue = queue ! Suc n) \<and> getNext tcb = NULL\<rbrakk> \<Longrightarrow> tcb_ptr_to_ctcb_ptr (last queue) \<noteq> getPrev tcb
 3. \<lbrakk>tcb_ptr_to_ctcb_ptr (hd queue) \<noteq> NULL; tcb_queue_relation getNext getPrev mp queue qprev qhead; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; hd queue \<in> set queue; mp (tcb_ptr_to_ctcb_ptr (hd queue)) = Some tcb; ctcb_ptr_to_tcb_ptr qprev \<notin> set queue; hd queue \<noteq> last queue; tcbp = hd queue; getPrev tcb = qprev \<and> (\<exists>n<length queue - Suc 0. hd queue = queue ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n))\<rbrakk> \<Longrightarrow> tcb_ptr_to_ctcb_ptr (hd queue) \<noteq> getNext tcb \<and> tcb_ptr_to_ctcb_ptr (hd queue) \<noteq> qprev \<and> (getNext tcb \<noteq> NULL \<longrightarrow> getNext tcb \<noteq> qprev)
 4. \<lbrakk>tcb_ptr_to_ctcb_ptr tcbp \<noteq> NULL; tcb_queue_relation getNext getPrev mp queue qprev qhead; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; tcbp \<in> set queue; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; ctcb_ptr_to_tcb_ptr qprev \<notin> set queue; tcbp \<noteq> last queue; tcbp \<noteq> hd queue; (\<exists>n<length queue - Suc 0. getPrev tcb = tcb_ptr_to_ctcb_ptr (queue ! n) \<and> tcbp = queue ! Suc n) \<and> (\<exists>n<length queue - Suc 0. tcbp = queue ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n))\<rbrakk> \<Longrightarrow> tcb_ptr_to_ctcb_ptr tcbp \<noteq> getNext tcb \<and> tcb_ptr_to_ctcb_ptr tcbp \<noteq> getPrev tcb \<and> (getNext tcb \<noteq> NULL \<longrightarrow> getNext tcb \<noteq> getPrev tcb) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>tcb_ptr_to_ctcb_ptr (last queue) \<noteq> NULL; tcb_queue_relation getNext getPrev mp queue qprev qhead; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; last queue \<in> set queue; mp (tcb_ptr_to_ctcb_ptr (last queue)) = Some tcb; ctcb_ptr_to_tcb_ptr qprev \<notin> set queue; tcbp = last queue; last queue \<noteq> hd queue; (\<exists>n<length queue - Suc 0. getPrev tcb = tcb_ptr_to_ctcb_ptr (queue ! n) \<and> last queue = queue ! Suc n) \<and> getNext tcb = NULL\<rbrakk> \<Longrightarrow> tcb_ptr_to_ctcb_ptr (last queue) \<noteq> getPrev tcb
 2. \<lbrakk>tcb_ptr_to_ctcb_ptr (hd queue) \<noteq> NULL; tcb_queue_relation getNext getPrev mp queue qprev qhead; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; hd queue \<in> set queue; mp (tcb_ptr_to_ctcb_ptr (hd queue)) = Some tcb; ctcb_ptr_to_tcb_ptr qprev \<notin> set queue; hd queue \<noteq> last queue; tcbp = hd queue; getPrev tcb = qprev \<and> (\<exists>n<length queue - Suc 0. hd queue = queue ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n))\<rbrakk> \<Longrightarrow> tcb_ptr_to_ctcb_ptr (hd queue) \<noteq> getNext tcb \<and> tcb_ptr_to_ctcb_ptr (hd queue) \<noteq> qprev \<and> (getNext tcb \<noteq> NULL \<longrightarrow> getNext tcb \<noteq> qprev)
 3. \<lbrakk>tcb_ptr_to_ctcb_ptr tcbp \<noteq> NULL; tcb_queue_relation getNext getPrev mp queue qprev qhead; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; tcbp \<in> set queue; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; ctcb_ptr_to_tcb_ptr qprev \<notin> set queue; tcbp \<noteq> last queue; tcbp \<noteq> hd queue; (\<exists>n<length queue - Suc 0. getPrev tcb = tcb_ptr_to_ctcb_ptr (queue ! n) \<and> tcbp = queue ! Suc n) \<and> (\<exists>n<length queue - Suc 0. tcbp = queue ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n))\<rbrakk> \<Longrightarrow> tcb_ptr_to_ctcb_ptr tcbp \<noteq> getNext tcb \<and> tcb_ptr_to_ctcb_ptr tcbp \<noteq> getPrev tcb \<and> (getNext tcb \<noteq> NULL \<longrightarrow> getNext tcb \<noteq> getPrev tcb) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>tcb_ptr_to_ctcb_ptr (hd queue) \<noteq> NULL; tcb_queue_relation getNext getPrev mp queue qprev qhead; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; hd queue \<in> set queue; mp (tcb_ptr_to_ctcb_ptr (hd queue)) = Some tcb; ctcb_ptr_to_tcb_ptr qprev \<notin> set queue; hd queue \<noteq> last queue; tcbp = hd queue; getPrev tcb = qprev \<and> (\<exists>n<length queue - Suc 0. hd queue = queue ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n))\<rbrakk> \<Longrightarrow> tcb_ptr_to_ctcb_ptr (hd queue) \<noteq> getNext tcb \<and> tcb_ptr_to_ctcb_ptr (hd queue) \<noteq> qprev \<and> (getNext tcb \<noteq> NULL \<longrightarrow> getNext tcb \<noteq> qprev)
 2. \<lbrakk>tcb_ptr_to_ctcb_ptr tcbp \<noteq> NULL; tcb_queue_relation getNext getPrev mp queue qprev qhead; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; tcbp \<in> set queue; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; ctcb_ptr_to_tcb_ptr qprev \<notin> set queue; tcbp \<noteq> last queue; tcbp \<noteq> hd queue; (\<exists>n<length queue - Suc 0. getPrev tcb = tcb_ptr_to_ctcb_ptr (queue ! n) \<and> tcbp = queue ! Suc n) \<and> (\<exists>n<length queue - Suc 0. tcbp = queue ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n))\<rbrakk> \<Longrightarrow> tcb_ptr_to_ctcb_ptr tcbp \<noteq> getNext tcb \<and> tcb_ptr_to_ctcb_ptr tcbp \<noteq> getPrev tcb \<and> (getNext tcb \<noteq> NULL \<longrightarrow> getNext tcb \<noteq> getPrev tcb) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>tcb_ptr_to_ctcb_ptr (hd queue) \<noteq> NULL; tcb_queue_relation getNext getPrev mp queue qprev qhead; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; hd queue \<in> set queue; mp (tcb_ptr_to_ctcb_ptr (hd queue)) = Some tcb; ctcb_ptr_to_tcb_ptr qprev \<notin> set queue; hd queue \<noteq> last queue; tcbp = hd queue; getPrev tcb = qprev \<and> (\<exists>n<length queue - Suc 0. hd queue = queue ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n))\<rbrakk> \<Longrightarrow> tcb_ptr_to_ctcb_ptr (hd queue) \<noteq> getNext tcb
 2. \<lbrakk>tcb_ptr_to_ctcb_ptr (hd queue) \<noteq> NULL; tcb_queue_relation getNext getPrev mp queue qprev qhead; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; hd queue \<in> set queue; mp (tcb_ptr_to_ctcb_ptr (hd queue)) = Some tcb; ctcb_ptr_to_tcb_ptr qprev \<notin> set queue; hd queue \<noteq> last queue; tcbp = hd queue; getPrev tcb = qprev \<and> (\<exists>n<length queue - Suc 0. hd queue = queue ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n))\<rbrakk> \<Longrightarrow> tcb_ptr_to_ctcb_ptr (hd queue) \<noteq> qprev
 3. \<lbrakk>tcb_ptr_to_ctcb_ptr (hd queue) \<noteq> NULL; tcb_queue_relation getNext getPrev mp queue qprev qhead; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; hd queue \<in> set queue; mp (tcb_ptr_to_ctcb_ptr (hd queue)) = Some tcb; ctcb_ptr_to_tcb_ptr qprev \<notin> set queue; hd queue \<noteq> last queue; tcbp = hd queue; getPrev tcb = qprev \<and> (\<exists>n<length queue - Suc 0. hd queue = queue ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n)); getNext tcb \<noteq> NULL\<rbrakk> \<Longrightarrow> getNext tcb \<noteq> qprev
 4. \<lbrakk>tcb_ptr_to_ctcb_ptr tcbp \<noteq> NULL; tcb_queue_relation getNext getPrev mp queue qprev qhead; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; tcbp \<in> set queue; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; ctcb_ptr_to_tcb_ptr qprev \<notin> set queue; tcbp \<noteq> last queue; tcbp \<noteq> hd queue; (\<exists>n<length queue - Suc 0. getPrev tcb = tcb_ptr_to_ctcb_ptr (queue ! n) \<and> tcbp = queue ! Suc n) \<and> (\<exists>n<length queue - Suc 0. tcbp = queue ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n))\<rbrakk> \<Longrightarrow> tcb_ptr_to_ctcb_ptr tcbp \<noteq> getNext tcb \<and> tcb_ptr_to_ctcb_ptr tcbp \<noteq> getPrev tcb \<and> (getNext tcb \<noteq> NULL \<longrightarrow> getNext tcb \<noteq> getPrev tcb) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>tcb_ptr_to_ctcb_ptr (hd queue) \<noteq> NULL; tcb_queue_relation getNext getPrev mp queue qprev qhead; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; hd queue \<in> set queue; mp (tcb_ptr_to_ctcb_ptr (hd queue)) = Some tcb; ctcb_ptr_to_tcb_ptr qprev \<notin> set queue; hd queue \<noteq> last queue; tcbp = hd queue; getPrev tcb = qprev \<and> (\<exists>n<length queue - Suc 0. hd queue = queue ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n))\<rbrakk> \<Longrightarrow> tcb_ptr_to_ctcb_ptr (hd queue) \<noteq> qprev
 2. \<lbrakk>tcb_ptr_to_ctcb_ptr (hd queue) \<noteq> NULL; tcb_queue_relation getNext getPrev mp queue qprev qhead; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; hd queue \<in> set queue; mp (tcb_ptr_to_ctcb_ptr (hd queue)) = Some tcb; ctcb_ptr_to_tcb_ptr qprev \<notin> set queue; hd queue \<noteq> last queue; tcbp = hd queue; getPrev tcb = qprev \<and> (\<exists>n<length queue - Suc 0. hd queue = queue ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n)); getNext tcb \<noteq> NULL\<rbrakk> \<Longrightarrow> getNext tcb \<noteq> qprev
 3. \<lbrakk>tcb_ptr_to_ctcb_ptr tcbp \<noteq> NULL; tcb_queue_relation getNext getPrev mp queue qprev qhead; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; tcbp \<in> set queue; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; ctcb_ptr_to_tcb_ptr qprev \<notin> set queue; tcbp \<noteq> last queue; tcbp \<noteq> hd queue; (\<exists>n<length queue - Suc 0. getPrev tcb = tcb_ptr_to_ctcb_ptr (queue ! n) \<and> tcbp = queue ! Suc n) \<and> (\<exists>n<length queue - Suc 0. tcbp = queue ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n))\<rbrakk> \<Longrightarrow> tcb_ptr_to_ctcb_ptr tcbp \<noteq> getNext tcb \<and> tcb_ptr_to_ctcb_ptr tcbp \<noteq> getPrev tcb \<and> (getNext tcb \<noteq> NULL \<longrightarrow> getNext tcb \<noteq> getPrev tcb) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>tcb_ptr_to_ctcb_ptr (hd queue) \<noteq> NULL; tcb_queue_relation getNext getPrev mp queue qprev qhead; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; hd queue \<in> set queue; mp (tcb_ptr_to_ctcb_ptr (hd queue)) = Some tcb; ctcb_ptr_to_tcb_ptr qprev \<notin> set queue; hd queue \<noteq> last queue; tcbp = hd queue; getPrev tcb = qprev \<and> (\<exists>n<length queue - Suc 0. hd queue = queue ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n))\<rbrakk> \<Longrightarrow> qprev \<noteq> tcb_ptr_to_ctcb_ptr (hd queue)
 2. \<lbrakk>tcb_ptr_to_ctcb_ptr (hd queue) \<noteq> NULL; tcb_queue_relation getNext getPrev mp queue qprev qhead; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; hd queue \<in> set queue; mp (tcb_ptr_to_ctcb_ptr (hd queue)) = Some tcb; ctcb_ptr_to_tcb_ptr qprev \<notin> set queue; hd queue \<noteq> last queue; tcbp = hd queue; getPrev tcb = qprev \<and> (\<exists>n<length queue - Suc 0. hd queue = queue ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n)); getNext tcb \<noteq> NULL\<rbrakk> \<Longrightarrow> getNext tcb \<noteq> qprev
 3. \<lbrakk>tcb_ptr_to_ctcb_ptr tcbp \<noteq> NULL; tcb_queue_relation getNext getPrev mp queue qprev qhead; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; tcbp \<in> set queue; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; ctcb_ptr_to_tcb_ptr qprev \<notin> set queue; tcbp \<noteq> last queue; tcbp \<noteq> hd queue; (\<exists>n<length queue - Suc 0. getPrev tcb = tcb_ptr_to_ctcb_ptr (queue ! n) \<and> tcbp = queue ! Suc n) \<and> (\<exists>n<length queue - Suc 0. tcbp = queue ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n))\<rbrakk> \<Longrightarrow> tcb_ptr_to_ctcb_ptr tcbp \<noteq> getNext tcb \<and> tcb_ptr_to_ctcb_ptr tcbp \<noteq> getPrev tcb \<and> (getNext tcb \<noteq> NULL \<longrightarrow> getNext tcb \<noteq> getPrev tcb) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>tcb_ptr_to_ctcb_ptr (hd queue) \<noteq> NULL; tcb_queue_relation getNext getPrev mp queue qprev qhead; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; hd queue \<in> set queue; mp (tcb_ptr_to_ctcb_ptr (hd queue)) = Some tcb; ctcb_ptr_to_tcb_ptr qprev \<notin> set queue; hd queue \<noteq> last queue; tcbp = hd queue; getPrev tcb = qprev \<and> (\<exists>n<length queue - Suc 0. hd queue = queue ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n)); getNext tcb \<noteq> NULL\<rbrakk> \<Longrightarrow> getNext tcb \<noteq> qprev
 2. \<lbrakk>tcb_ptr_to_ctcb_ptr tcbp \<noteq> NULL; tcb_queue_relation getNext getPrev mp queue qprev qhead; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; tcbp \<in> set queue; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; ctcb_ptr_to_tcb_ptr qprev \<notin> set queue; tcbp \<noteq> last queue; tcbp \<noteq> hd queue; (\<exists>n<length queue - Suc 0. getPrev tcb = tcb_ptr_to_ctcb_ptr (queue ! n) \<and> tcbp = queue ! Suc n) \<and> (\<exists>n<length queue - Suc 0. tcbp = queue ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n))\<rbrakk> \<Longrightarrow> tcb_ptr_to_ctcb_ptr tcbp \<noteq> getNext tcb \<and> tcb_ptr_to_ctcb_ptr tcbp \<noteq> getPrev tcb \<and> (getNext tcb \<noteq> NULL \<longrightarrow> getNext tcb \<noteq> getPrev tcb) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_ptr_to_ctcb_ptr tcbp \<noteq> NULL; tcb_queue_relation getNext getPrev mp queue qprev qhead; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; tcbp \<in> set queue; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; ctcb_ptr_to_tcb_ptr qprev \<notin> set queue; tcbp \<noteq> last queue; tcbp \<noteq> hd queue; (\<exists>n<length queue - Suc 0. getPrev tcb = tcb_ptr_to_ctcb_ptr (queue ! n) \<and> tcbp = queue ! Suc n) \<and> (\<exists>n<length queue - Suc 0. tcbp = queue ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n))\<rbrakk> \<Longrightarrow> tcb_ptr_to_ctcb_ptr tcbp \<noteq> getNext tcb \<and> tcb_ptr_to_ctcb_ptr tcbp \<noteq> getPrev tcb \<and> (getNext tcb \<noteq> NULL \<longrightarrow> getNext tcb \<noteq> getPrev tcb) proof (prove)
goal (1 subgoal):
 1. \<And>n na. \<lbrakk>tcb_ptr_to_ctcb_ptr (queue ! na) \<noteq> NULL; tcb_queue_relation getNext getPrev mp queue qprev qhead; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; mp (tcb_ptr_to_ctcb_ptr (queue ! na)) = Some tcb; ctcb_ptr_to_tcb_ptr qprev \<notin> set queue; queue ! na \<noteq> last queue; queue ! na \<noteq> hd queue; n < length queue - Suc 0; na < length queue - Suc 0; getPrev tcb = tcb_ptr_to_ctcb_ptr (queue ! n); tcbp = queue ! na; queue ! Suc n = queue ! na; getNext tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc na)\<rbrakk> \<Longrightarrow> queue ! na \<noteq> queue ! Suc na \<and> queue ! na \<noteq> queue ! n \<and> (tcb_ptr_to_ctcb_ptr (queue ! Suc na) \<noteq> NULL \<longrightarrow> queue ! Suc na \<noteq> queue ! n) proof (prove)
goal (3 subgoals):
 1. \<And>n na. \<lbrakk>tcb_ptr_to_ctcb_ptr (queue ! na) \<noteq> NULL; tcb_queue_relation getNext getPrev mp queue qprev qhead; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; mp (tcb_ptr_to_ctcb_ptr (queue ! na)) = Some tcb; ctcb_ptr_to_tcb_ptr qprev \<notin> set queue; queue ! na \<noteq> last queue; queue ! na \<noteq> hd queue; n < length queue - Suc 0; na < length queue - Suc 0; getPrev tcb = tcb_ptr_to_ctcb_ptr (queue ! n); tcbp = queue ! na; queue ! Suc n = queue ! na; getNext tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc na)\<rbrakk> \<Longrightarrow> queue ! na \<noteq> queue ! Suc na
 2. \<And>n na. \<lbrakk>tcb_ptr_to_ctcb_ptr (queue ! na) \<noteq> NULL; tcb_queue_relation getNext getPrev mp queue qprev qhead; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; mp (tcb_ptr_to_ctcb_ptr (queue ! na)) = Some tcb; ctcb_ptr_to_tcb_ptr qprev \<notin> set queue; queue ! na \<noteq> last queue; queue ! na \<noteq> hd queue; n < length queue - Suc 0; na < length queue - Suc 0; getPrev tcb = tcb_ptr_to_ctcb_ptr (queue ! n); tcbp = queue ! na; queue ! Suc n = queue ! na; getNext tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc na)\<rbrakk> \<Longrightarrow> queue ! na \<noteq> queue ! n
 3. \<And>n na. \<lbrakk>tcb_ptr_to_ctcb_ptr (queue ! na) \<noteq> NULL; tcb_queue_relation getNext getPrev mp queue qprev qhead; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; mp (tcb_ptr_to_ctcb_ptr (queue ! na)) = Some tcb; ctcb_ptr_to_tcb_ptr qprev \<notin> set queue; queue ! na \<noteq> last queue; queue ! na \<noteq> hd queue; n < length queue - Suc 0; na < length queue - Suc 0; getPrev tcb = tcb_ptr_to_ctcb_ptr (queue ! n); tcbp = queue ! na; queue ! Suc n = queue ! na; getNext tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc na); tcb_ptr_to_ctcb_ptr (queue ! Suc na) \<noteq> NULL\<rbrakk> \<Longrightarrow> queue ! Suc na \<noteq> queue ! n proof (prove)
goal (2 subgoals):
 1. \<And>n na. \<lbrakk>tcb_ptr_to_ctcb_ptr (queue ! na) \<noteq> NULL; tcb_queue_relation getNext getPrev mp queue qprev qhead; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; mp (tcb_ptr_to_ctcb_ptr (queue ! na)) = Some tcb; ctcb_ptr_to_tcb_ptr qprev \<notin> set queue; queue ! na \<noteq> last queue; queue ! na \<noteq> hd queue; n < length queue - Suc 0; na < length queue - Suc 0; getPrev tcb = tcb_ptr_to_ctcb_ptr (queue ! n); tcbp = queue ! na; queue ! Suc n = queue ! na; getNext tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc na)\<rbrakk> \<Longrightarrow> queue ! na \<noteq> queue ! n
 2. \<And>n na. \<lbrakk>tcb_ptr_to_ctcb_ptr (queue ! na) \<noteq> NULL; tcb_queue_relation getNext getPrev mp queue qprev qhead; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; mp (tcb_ptr_to_ctcb_ptr (queue ! na)) = Some tcb; ctcb_ptr_to_tcb_ptr qprev \<notin> set queue; queue ! na \<noteq> last queue; queue ! na \<noteq> hd queue; n < length queue - Suc 0; na < length queue - Suc 0; getPrev tcb = tcb_ptr_to_ctcb_ptr (queue ! n); tcbp = queue ! na; queue ! Suc n = queue ! na; getNext tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc na); tcb_ptr_to_ctcb_ptr (queue ! Suc na) \<noteq> NULL\<rbrakk> \<Longrightarrow> queue ! Suc na \<noteq> queue ! n proof (prove)
goal (2 subgoals):
 1. \<And>n na. \<lbrakk>tcb_ptr_to_ctcb_ptr (queue ! na) \<noteq> NULL; tcb_queue_relation getNext getPrev mp queue qprev qhead; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; mp (tcb_ptr_to_ctcb_ptr (queue ! na)) = Some tcb; ctcb_ptr_to_tcb_ptr qprev \<notin> set queue; queue ! na \<noteq> last queue; queue ! na \<noteq> hd queue; n < length queue - Suc 0; na < length queue - Suc 0; getPrev tcb = tcb_ptr_to_ctcb_ptr (queue ! n); tcbp = queue ! na; getNext tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc na)\<rbrakk> \<Longrightarrow> queue ! Suc n \<noteq> queue ! n
 2. \<And>n na. \<lbrakk>tcb_ptr_to_ctcb_ptr (queue ! na) \<noteq> NULL; tcb_queue_relation getNext getPrev mp queue qprev qhead; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; mp (tcb_ptr_to_ctcb_ptr (queue ! na)) = Some tcb; ctcb_ptr_to_tcb_ptr qprev \<notin> set queue; queue ! na \<noteq> last queue; queue ! na \<noteq> hd queue; n < length queue - Suc 0; na < length queue - Suc 0; getPrev tcb = tcb_ptr_to_ctcb_ptr (queue ! n); tcbp = queue ! na; queue ! Suc n = queue ! na; getNext tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc na); tcb_ptr_to_ctcb_ptr (queue ! Suc na) \<noteq> NULL\<rbrakk> \<Longrightarrow> queue ! Suc na \<noteq> queue ! n proof (prove)
goal (1 subgoal):
 1. \<And>n na. \<lbrakk>tcb_ptr_to_ctcb_ptr (queue ! na) \<noteq> NULL; tcb_queue_relation getNext getPrev mp queue qprev qhead; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; mp (tcb_ptr_to_ctcb_ptr (queue ! na)) = Some tcb; ctcb_ptr_to_tcb_ptr qprev \<notin> set queue; queue ! na \<noteq> last queue; queue ! na \<noteq> hd queue; n < length queue - Suc 0; na < length queue - Suc 0; getPrev tcb = tcb_ptr_to_ctcb_ptr (queue ! n); tcbp = queue ! na; queue ! Suc n = queue ! na; getNext tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc na); tcb_ptr_to_ctcb_ptr (queue ! Suc na) \<noteq> NULL\<rbrakk> \<Longrightarrow> queue ! Suc na \<noteq> queue ! n proof (prove)
goal (1 subgoal):
 1. \<And>n na. \<lbrakk>tcb_ptr_to_ctcb_ptr (queue ! na) \<noteq> NULL; tcb_queue_relation getNext getPrev mp queue qprev qhead; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; mp (tcb_ptr_to_ctcb_ptr (queue ! na)) = Some tcb; ctcb_ptr_to_tcb_ptr qprev \<notin> set queue; queue ! na \<noteq> last queue; queue ! na \<noteq> hd queue; n < length queue - Suc 0; na < length queue - Suc 0; getPrev tcb = tcb_ptr_to_ctcb_ptr (queue ! n); tcbp = queue ! na; queue ! Suc n = queue ! na; getNext tcb = tcb_ptr_to_ctcb_ptr (queue ! n); tcb_ptr_to_ctcb_ptr (queue ! n) \<noteq> NULL; queue ! Suc na = queue ! n\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>n na. \<lbrakk>tcb_ptr_to_ctcb_ptr (queue ! na) \<noteq> NULL; tcb_queue_relation getNext getPrev mp queue qprev qhead; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; mp (tcb_ptr_to_ctcb_ptr (queue ! na)) = Some tcb; ctcb_ptr_to_tcb_ptr qprev \<notin> set queue; queue ! na \<noteq> last queue; queue ! na \<noteq> hd queue; n < length queue - Suc 0; na < length queue - Suc 0; getPrev tcb = tcb_ptr_to_ctcb_ptr (queue ! n); tcbp = queue ! na; queue ! Suc n = queue ! na; getNext tcb = tcb_ptr_to_ctcb_ptr (queue ! n); tcb_ptr_to_ctcb_ptr (queue ! n) \<noteq> NULL; queue ! Suc na = queue ! n; na = Suc n\<rbrakk> \<Longrightarrow> False
 2. \<And>n na. \<lbrakk>tcb_ptr_to_ctcb_ptr (queue ! na) \<noteq> NULL; tcb_queue_relation getNext getPrev mp queue qprev qhead; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; mp (tcb_ptr_to_ctcb_ptr (queue ! na)) = Some tcb; ctcb_ptr_to_tcb_ptr qprev \<notin> set queue; queue ! na \<noteq> last queue; queue ! na \<noteq> hd queue; n < length queue - Suc 0; na < length queue - Suc 0; getPrev tcb = tcb_ptr_to_ctcb_ptr (queue ! n); tcbp = queue ! na; queue ! Suc n = queue ! na; getNext tcb = tcb_ptr_to_ctcb_ptr (queue ! n); tcb_ptr_to_ctcb_ptr (queue ! n) \<noteq> NULL; queue ! Suc na = queue ! n; na \<noteq> Suc n\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>n na. \<lbrakk>tcb_ptr_to_ctcb_ptr (queue ! Suc n) \<noteq> NULL; tcb_queue_relation getNext getPrev mp queue qprev qhead; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; mp (tcb_ptr_to_ctcb_ptr (queue ! Suc n)) = Some tcb; ctcb_ptr_to_tcb_ptr qprev \<notin> set queue; queue ! Suc n \<noteq> last queue; queue ! Suc n \<noteq> hd queue; n < length queue - Suc 0; Suc n < length queue - Suc 0; getPrev tcb = tcb_ptr_to_ctcb_ptr (queue ! n); tcbp = queue ! Suc n; getNext tcb = tcb_ptr_to_ctcb_ptr (queue ! n); tcb_ptr_to_ctcb_ptr (queue ! n) \<noteq> NULL; queue ! Suc (Suc n) = queue ! n\<rbrakk> \<Longrightarrow> False
 2. \<And>n na. \<lbrakk>tcb_ptr_to_ctcb_ptr (queue ! na) \<noteq> NULL; tcb_queue_relation getNext getPrev mp queue qprev qhead; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; mp (tcb_ptr_to_ctcb_ptr (queue ! na)) = Some tcb; ctcb_ptr_to_tcb_ptr qprev \<notin> set queue; queue ! na \<noteq> last queue; queue ! na \<noteq> hd queue; n < length queue - Suc 0; na < length queue - Suc 0; getPrev tcb = tcb_ptr_to_ctcb_ptr (queue ! n); tcbp = queue ! na; queue ! Suc n = queue ! na; getNext tcb = tcb_ptr_to_ctcb_ptr (queue ! n); tcb_ptr_to_ctcb_ptr (queue ! n) \<noteq> NULL; queue ! Suc na = queue ! n; na \<noteq> Suc n\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>n na. \<lbrakk>tcb_ptr_to_ctcb_ptr (queue ! na) \<noteq> NULL; tcb_queue_relation getNext getPrev mp queue qprev qhead; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; mp (tcb_ptr_to_ctcb_ptr (queue ! na)) = Some tcb; ctcb_ptr_to_tcb_ptr qprev \<notin> set queue; queue ! na \<noteq> last queue; queue ! na \<noteq> hd queue; n < length queue - Suc 0; na < length queue - Suc 0; getPrev tcb = tcb_ptr_to_ctcb_ptr (queue ! n); tcbp = queue ! na; queue ! Suc n = queue ! na; getNext tcb = tcb_ptr_to_ctcb_ptr (queue ! n); tcb_ptr_to_ctcb_ptr (queue ! n) \<noteq> NULL; queue ! Suc na = queue ! n; na \<noteq> Suc n\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!