theory TcbQueue_C

lemma tcbDequeue_update0:
  assumes in_queue: "tcbp \<in> set queue"
  and    valid_ntfn: "\<forall>t\<in>set queue. tcb_at' t s" "distinct queue"
  and    queue_rel: "tcb_queue_relation tn tp mp queue qprev qhead"
  and prev_not_queue: "ctcb_ptr_to_tcb_ptr qprev \<notin> set queue"
  and       cs_tcb: "mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb"
  and            f: "\<And>v f g. tn (tn_update f v) = f (tn v) \<and> tp (tp_update g v) = g (tp v)
                           \<and> tn (tp_update f v) = tn v \<and> tp (tn_update g v) = tp v"
  shows "tcb_queue_relation tn tp
          (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb))))
            (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp))
            (remove1 tcbp queue)
            (if tcb_ptr_to_ctcb_ptr tcbp = qhead then tp tcb else qprev)
            (if tcb_ptr_to_ctcb_ptr tcbp = qhead then tn tcb else qhead)"
  (is "tcb_queue_relation tn tp ?mp (remove1 tcbp queue) (?qprev qprev qhead) (?qhead qhead)") using queue_rel valid_ntfn prev_not_queue in_queue proof (induct queue arbitrary: qprev qhead) case Nil thus ?case by simp next case (Cons tcb' tcbs qprev' qhead') have "tcbp = tcb' \<or> tcbp \<in> set tcbs" using Cons.prems by simp thus ?case proof assume tcbp: "tcbp = tcb'" hence qp: "qprev' = tp tcb" and qh: "qhead' = tcb_ptr_to_ctcb_ptr tcb'" using Cons.prems cs_tcb by auto from Cons.prems have tq: "tcb_queue_relation tn tp mp tcbs (tcb_ptr_to_ctcb_ptr tcb') (tn tcb)" using Cons.prems cs_tcb tcbp by clarsimp note ind_prems = Cons.prems note ind_hyp   = Cons.hyps show ?thesis proof (cases tcbs) case Nil thus ?thesis using Cons.prems tcbp cs_tcb by clarsimp next case (Cons tcbs_hd tcbss) have nnull: "tn tcb \<noteq> NULL" using tq proof (rule tcb_queue_relation_next_not_NULL) from ind_prems show "\<forall>t\<in>set tcbs. tcb_at' t s"
          and "distinct tcbs" by simp_all show "tcbs \<noteq> []" using Cons by simp qed from Cons ind_prems have "tcbs_hd \<notin> set tcbss" by simp hence mpeq: "\<And>p. p \<in> tcb_ptr_to_ctcb_ptr ` set tcbss \<Longrightarrow> ?mp p = mp p" using tq cs_tcb tcbp Cons nnull ind_prems apply - apply (subst upd_unless_null_cong_helper, assumption, clarsimp)+ apply simp done have "tcb_ptr_to_ctcb_ptr tcbp \<noteq> tn tcb \<and> tcb_ptr_to_ctcb_ptr tcbp \<noteq> tp tcb
        \<and> tn tcb \<noteq> tp tcb" using tq cs_tcb ind_prems nnull apply - apply (drule (5) tcb_queue_relation_ptr_rel) apply clarsimp done hence "?mp (tcb_ptr_to_ctcb_ptr tcbs_hd) = Some (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb))))" using qp qh tq cs_tcb tcbp Cons nnull by (simp add: upd_unless_null_def) thus ?thesis using qp qh tq cs_tcb tcbp Cons nnull apply (simp (no_asm) add: tcbp Cons split del: if_split) apply (subst tcb_queue_relation_cong [OF refl refl refl mpeq]) apply assumption apply (clarsimp simp: f) done qed next assume inset: "tcbp \<in> set tcbs" hence  tcbp: "tcbp \<noteq> tcb'" using Cons.prems by clarsimp obtain tcb2 where cs_tcb2: "mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcb2"
      and rel2: "tcb_queue_relation tn tp mp tcbs (tcb_ptr_to_ctcb_ptr tcb') (tn tcb2)"
      and qh: "qhead' = tcb_ptr_to_ctcb_ptr tcb'"
      and qp: "qprev' = tp tcb2" using Cons.prems by clarsimp have nnull: "tcb_ptr_to_ctcb_ptr tcb' \<noteq> NULL" using Cons.prems apply - apply (erule (1) tcb_queue_relation_not_NULL') apply simp done have ih: "tcb_queue_relation tn tp ?mp (remove1 tcbp tcbs)
                                     (?qprev (tcb_ptr_to_ctcb_ptr tcb') (tn tcb2))
                                     (?qhead (tn tcb2))" using rel2 proof (rule Cons.hyps) from Cons.prems show "\<forall>t\<in>set tcbs. tcb_at' t s"
        and "distinct tcbs"
        and "ctcb_ptr_to_tcb_ptr (tcb_ptr_to_ctcb_ptr tcb') \<notin> set tcbs" by simp_all qed fact have tcb_next: "tn tcb \<noteq> tcb_ptr_to_ctcb_ptr tcb'" using Cons.prems tcb_queue_next_prev[OF Cons.prems(1), OF _ _ cs_tcb cs_tcb2]
            tcbp qp[symmetric] by auto show ?thesis using tcbp proof (cases "tn tcb2 = tcb_ptr_to_ctcb_ptr tcbp") case True hence tcb_prev: "tp tcb = tcb_ptr_to_ctcb_ptr tcb'" using Cons.prems cs_tcb2 cs_tcb not_sym [OF tcbp] apply - apply (subst tcb_queue_next_prev [symmetric], assumption+) apply simp apply simp apply simp apply (rule not_sym [OF tcbp]) apply simp done hence "?mp (tcb_ptr_to_ctcb_ptr tcb') = Some (tn_update (\<lambda>_. tn tcb) tcb2)" using tcb_next nnull cs_tcb2 unfolding upd_unless_null_def by simp thus ?thesis using tcbp cs_tcb qh qp True ih tcb_prev by (simp add: inj_eq f) next case False hence tcb_prev: "tp tcb \<noteq> tcb_ptr_to_ctcb_ptr tcb'" using Cons.prems cs_tcb2 cs_tcb not_sym [OF tcbp] apply - apply (subst tcb_queue_next_prev [symmetric], assumption+) apply simp apply simp apply simp apply (rule not_sym [OF tcbp]) apply simp done hence "?mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcb2" using tcb_next nnull cs_tcb2 unfolding upd_unless_null_def by simp thus ?thesis using tcbp cs_tcb qh qp False ih tcb_prev by (simp add: inj_eq) qed qed qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp queue) (if tcb_ptr_to_ctcb_ptr tcbp = qhead then tp tcb else qprev) (if tcb_ptr_to_ctcb_ptr tcbp = qhead then tn tcb else qhead) proof (prove)
using this:
tcb_queue_relation tn tp mp queue qprev qhead
\<forall>t\<in>set queue. tcb_at' t s
distinct queue
ctcb_ptr_to_tcb_ptr qprev \<notin> set queue
tcbp \<in> set queue

goal (1 subgoal):
 1. tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp queue) (if tcb_ptr_to_ctcb_ptr tcbp = qhead then tp tcb else qprev) (if tcb_ptr_to_ctcb_ptr tcbp = qhead then tn tcb else qhead) proof (state)
goal (2 subgoals):
 1. \<And>qprev qhead. \<lbrakk>tcb_queue_relation tn tp mp [] qprev qhead; \<forall>t\<in>set []. tcb_at' t s; distinct []; ctcb_ptr_to_tcb_ptr qprev \<notin> set []; tcbp \<in> set []\<rbrakk> \<Longrightarrow> tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp []) (if tcb_ptr_to_ctcb_ptr tcbp = qhead then tp tcb else qprev) (if tcb_ptr_to_ctcb_ptr tcbp = qhead then tn tcb else qhead)
 2. \<And>x1 queue qprev qhead. \<lbrakk>\<And>qprev qhead. \<lbrakk>tcb_queue_relation tn tp mp queue qprev qhead; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; ctcb_ptr_to_tcb_ptr qprev \<notin> set queue; tcbp \<in> set queue\<rbrakk> \<Longrightarrow> tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp queue) (if tcb_ptr_to_ctcb_ptr tcbp = qhead then tp tcb else qprev) (if tcb_ptr_to_ctcb_ptr tcbp = qhead then tn tcb else qhead); tcb_queue_relation tn tp mp (x1 # queue) qprev qhead; \<forall>t\<in>set (x1 # queue). tcb_at' t s; distinct (x1 # queue); ctcb_ptr_to_tcb_ptr qprev \<notin> set (x1 # queue); tcbp \<in> set (x1 # queue)\<rbrakk> \<Longrightarrow> tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp (x1 # queue)) (if tcb_ptr_to_ctcb_ptr tcbp = qhead then tp tcb else qprev) (if tcb_ptr_to_ctcb_ptr tcbp = qhead then tn tcb else qhead) proof (state)
this:
tcb_queue_relation tn tp mp [] qprev qhead
\<forall>t\<in>set []. tcb_at' t s
distinct []
ctcb_ptr_to_tcb_ptr qprev \<notin> set []
tcbp \<in> set []

goal (2 subgoals):
 1. \<And>qprev qhead. \<lbrakk>tcb_queue_relation tn tp mp [] qprev qhead; \<forall>t\<in>set []. tcb_at' t s; distinct []; ctcb_ptr_to_tcb_ptr qprev \<notin> set []; tcbp \<in> set []\<rbrakk> \<Longrightarrow> tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp []) (if tcb_ptr_to_ctcb_ptr tcbp = qhead then tp tcb else qprev) (if tcb_ptr_to_ctcb_ptr tcbp = qhead then tn tcb else qhead)
 2. \<And>x1 queue qprev qhead. \<lbrakk>\<And>qprev qhead. \<lbrakk>tcb_queue_relation tn tp mp queue qprev qhead; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; ctcb_ptr_to_tcb_ptr qprev \<notin> set queue; tcbp \<in> set queue\<rbrakk> \<Longrightarrow> tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp queue) (if tcb_ptr_to_ctcb_ptr tcbp = qhead then tp tcb else qprev) (if tcb_ptr_to_ctcb_ptr tcbp = qhead then tn tcb else qhead); tcb_queue_relation tn tp mp (x1 # queue) qprev qhead; \<forall>t\<in>set (x1 # queue). tcb_at' t s; distinct (x1 # queue); ctcb_ptr_to_tcb_ptr qprev \<notin> set (x1 # queue); tcbp \<in> set (x1 # queue)\<rbrakk> \<Longrightarrow> tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp (x1 # queue)) (if tcb_ptr_to_ctcb_ptr tcbp = qhead then tp tcb else qprev) (if tcb_ptr_to_ctcb_ptr tcbp = qhead then tn tcb else qhead) proof (prove)
using this:
tcb_queue_relation tn tp mp [] qprev qhead
\<forall>t\<in>set []. tcb_at' t s
distinct []
ctcb_ptr_to_tcb_ptr qprev \<notin> set []
tcbp \<in> set []

goal (1 subgoal):
 1. tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp []) (if tcb_ptr_to_ctcb_ptr tcbp = qhead then tp tcb else qprev) (if tcb_ptr_to_ctcb_ptr tcbp = qhead then tn tcb else qhead) proof (state)
this:
tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp []) (if tcb_ptr_to_ctcb_ptr tcbp = qhead then tp tcb else qprev) (if tcb_ptr_to_ctcb_ptr tcbp = qhead then tn tcb else qhead)

goal (1 subgoal):
 1. \<And>x1 queue qprev qhead. \<lbrakk>\<And>qprev qhead. \<lbrakk>tcb_queue_relation tn tp mp queue qprev qhead; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; ctcb_ptr_to_tcb_ptr qprev \<notin> set queue; tcbp \<in> set queue\<rbrakk> \<Longrightarrow> tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp queue) (if tcb_ptr_to_ctcb_ptr tcbp = qhead then tp tcb else qprev) (if tcb_ptr_to_ctcb_ptr tcbp = qhead then tn tcb else qhead); tcb_queue_relation tn tp mp (x1 # queue) qprev qhead; \<forall>t\<in>set (x1 # queue). tcb_at' t s; distinct (x1 # queue); ctcb_ptr_to_tcb_ptr qprev \<notin> set (x1 # queue); tcbp \<in> set (x1 # queue)\<rbrakk> \<Longrightarrow> tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp (x1 # queue)) (if tcb_ptr_to_ctcb_ptr tcbp = qhead then tp tcb else qprev) (if tcb_ptr_to_ctcb_ptr tcbp = qhead then tn tcb else qhead) proof (state)
goal (1 subgoal):
 1. \<And>x1 queue qprev qhead. \<lbrakk>\<And>qprev qhead. \<lbrakk>tcb_queue_relation tn tp mp queue qprev qhead; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; ctcb_ptr_to_tcb_ptr qprev \<notin> set queue; tcbp \<in> set queue\<rbrakk> \<Longrightarrow> tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp queue) (if tcb_ptr_to_ctcb_ptr tcbp = qhead then tp tcb else qprev) (if tcb_ptr_to_ctcb_ptr tcbp = qhead then tn tcb else qhead); tcb_queue_relation tn tp mp (x1 # queue) qprev qhead; \<forall>t\<in>set (x1 # queue). tcb_at' t s; distinct (x1 # queue); ctcb_ptr_to_tcb_ptr qprev \<notin> set (x1 # queue); tcbp \<in> set (x1 # queue)\<rbrakk> \<Longrightarrow> tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp (x1 # queue)) (if tcb_ptr_to_ctcb_ptr tcbp = qhead then tp tcb else qprev) (if tcb_ptr_to_ctcb_ptr tcbp = qhead then tn tcb else qhead) proof (state)
this:
\<lbrakk>tcb_queue_relation tn tp mp tcbs ?qprev ?qhead; \<forall>t\<in>set tcbs. tcb_at' t s; distinct tcbs; ctcb_ptr_to_tcb_ptr ?qprev \<notin> set tcbs; tcbp \<in> set tcbs\<rbrakk> \<Longrightarrow> tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp tcbs) (if tcb_ptr_to_ctcb_ptr tcbp = ?qhead then tp tcb else ?qprev) (if tcb_ptr_to_ctcb_ptr tcbp = ?qhead then tn tcb else ?qhead)
tcb_queue_relation tn tp mp (tcb' # tcbs) qprev' qhead'
\<forall>t\<in>set (tcb' # tcbs). tcb_at' t s
distinct (tcb' # tcbs)
ctcb_ptr_to_tcb_ptr qprev' \<notin> set (tcb' # tcbs)
tcbp \<in> set (tcb' # tcbs)

goal (1 subgoal):
 1. \<And>x1 queue qprev qhead. \<lbrakk>\<And>qprev qhead. \<lbrakk>tcb_queue_relation tn tp mp queue qprev qhead; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; ctcb_ptr_to_tcb_ptr qprev \<notin> set queue; tcbp \<in> set queue\<rbrakk> \<Longrightarrow> tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp queue) (if tcb_ptr_to_ctcb_ptr tcbp = qhead then tp tcb else qprev) (if tcb_ptr_to_ctcb_ptr tcbp = qhead then tn tcb else qhead); tcb_queue_relation tn tp mp (x1 # queue) qprev qhead; \<forall>t\<in>set (x1 # queue). tcb_at' t s; distinct (x1 # queue); ctcb_ptr_to_tcb_ptr qprev \<notin> set (x1 # queue); tcbp \<in> set (x1 # queue)\<rbrakk> \<Longrightarrow> tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp (x1 # queue)) (if tcb_ptr_to_ctcb_ptr tcbp = qhead then tp tcb else qprev) (if tcb_ptr_to_ctcb_ptr tcbp = qhead then tn tcb else qhead) proof (prove)
goal (1 subgoal):
 1. tcbp = tcb' \<or> tcbp \<in> set tcbs proof (prove)
using this:
tcb_queue_relation tn tp mp (tcb' # tcbs) qprev' qhead'
\<forall>t\<in>set (tcb' # tcbs). tcb_at' t s
distinct (tcb' # tcbs)
ctcb_ptr_to_tcb_ptr qprev' \<notin> set (tcb' # tcbs)
tcbp \<in> set (tcb' # tcbs)

goal (1 subgoal):
 1. tcbp = tcb' \<or> tcbp \<in> set tcbs proof (state)
this:
tcbp = tcb' \<or> tcbp \<in> set tcbs

goal (1 subgoal):
 1. \<And>x1 queue qprev qhead. \<lbrakk>\<And>qprev qhead. \<lbrakk>tcb_queue_relation tn tp mp queue qprev qhead; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; ctcb_ptr_to_tcb_ptr qprev \<notin> set queue; tcbp \<in> set queue\<rbrakk> \<Longrightarrow> tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp queue) (if tcb_ptr_to_ctcb_ptr tcbp = qhead then tp tcb else qprev) (if tcb_ptr_to_ctcb_ptr tcbp = qhead then tn tcb else qhead); tcb_queue_relation tn tp mp (x1 # queue) qprev qhead; \<forall>t\<in>set (x1 # queue). tcb_at' t s; distinct (x1 # queue); ctcb_ptr_to_tcb_ptr qprev \<notin> set (x1 # queue); tcbp \<in> set (x1 # queue)\<rbrakk> \<Longrightarrow> tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp (x1 # queue)) (if tcb_ptr_to_ctcb_ptr tcbp = qhead then tp tcb else qprev) (if tcb_ptr_to_ctcb_ptr tcbp = qhead then tn tcb else qhead) proof (prove)
using this:
tcbp = tcb' \<or> tcbp \<in> set tcbs

goal (1 subgoal):
 1. tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp (tcb' # tcbs)) (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tp tcb else qprev') (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tn tcb else qhead') proof (state)
goal (2 subgoals):
 1. tcbp = tcb' \<Longrightarrow> tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp (tcb' # tcbs)) (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tp tcb else qprev') (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tn tcb else qhead')
 2. tcbp \<in> set tcbs \<Longrightarrow> tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp (tcb' # tcbs)) (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tp tcb else qprev') (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tn tcb else qhead') proof (state)
this:
tcbp = tcb'

goal (2 subgoals):
 1. tcbp = tcb' \<Longrightarrow> tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp (tcb' # tcbs)) (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tp tcb else qprev') (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tn tcb else qhead')
 2. tcbp \<in> set tcbs \<Longrightarrow> tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp (tcb' # tcbs)) (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tp tcb else qprev') (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tn tcb else qhead') proof (prove)
using this:
tcbp = tcb'

goal (1 subgoal):
 1. qprev' = tp tcb &&& qhead' = tcb_ptr_to_ctcb_ptr tcb' proof (prove)
using this:
tcbp = tcb'
tcb_queue_relation tn tp mp (tcb' # tcbs) qprev' qhead'
\<forall>t\<in>set (tcb' # tcbs). tcb_at' t s
distinct (tcb' # tcbs)
ctcb_ptr_to_tcb_ptr qprev' \<notin> set (tcb' # tcbs)
tcbp \<in> set (tcb' # tcbs)
mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb

goal (1 subgoal):
 1. qprev' = tp tcb &&& qhead' = tcb_ptr_to_ctcb_ptr tcb' proof (state)
this:
qprev' = tp tcb
qhead' = tcb_ptr_to_ctcb_ptr tcb'

goal (2 subgoals):
 1. tcbp = tcb' \<Longrightarrow> tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp (tcb' # tcbs)) (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tp tcb else qprev') (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tn tcb else qhead')
 2. tcbp \<in> set tcbs \<Longrightarrow> tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp (tcb' # tcbs)) (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tp tcb else qprev') (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tn tcb else qhead') proof (chain)
picking this:
tcb_queue_relation tn tp mp (tcb' # tcbs) qprev' qhead'
\<forall>t\<in>set (tcb' # tcbs). tcb_at' t s
distinct (tcb' # tcbs)
ctcb_ptr_to_tcb_ptr qprev' \<notin> set (tcb' # tcbs)
tcbp \<in> set (tcb' # tcbs) proof (prove)
using this:
tcb_queue_relation tn tp mp (tcb' # tcbs) qprev' qhead'
\<forall>t\<in>set (tcb' # tcbs). tcb_at' t s
distinct (tcb' # tcbs)
ctcb_ptr_to_tcb_ptr qprev' \<notin> set (tcb' # tcbs)
tcbp \<in> set (tcb' # tcbs)

goal (1 subgoal):
 1. tcb_queue_relation tn tp mp tcbs (tcb_ptr_to_ctcb_ptr tcb') (tn tcb) proof (prove)
using this:
tcb_queue_relation tn tp mp (tcb' # tcbs) qprev' qhead'
\<forall>t\<in>set (tcb' # tcbs). tcb_at' t s
distinct (tcb' # tcbs)
ctcb_ptr_to_tcb_ptr qprev' \<notin> set (tcb' # tcbs)
tcbp \<in> set (tcb' # tcbs)
tcb_queue_relation tn tp mp (tcb' # tcbs) qprev' qhead'
\<forall>t\<in>set (tcb' # tcbs). tcb_at' t s
distinct (tcb' # tcbs)
ctcb_ptr_to_tcb_ptr qprev' \<notin> set (tcb' # tcbs)
tcbp \<in> set (tcb' # tcbs)
mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb
tcbp = tcb'

goal (1 subgoal):
 1. tcb_queue_relation tn tp mp tcbs (tcb_ptr_to_ctcb_ptr tcb') (tn tcb) proof (state)
this:
tcb_queue_relation tn tp mp tcbs (tcb_ptr_to_ctcb_ptr tcb') (tn tcb)

goal (2 subgoals):
 1. tcbp = tcb' \<Longrightarrow> tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp (tcb' # tcbs)) (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tp tcb else qprev') (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tn tcb else qhead')
 2. tcbp \<in> set tcbs \<Longrightarrow> tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp (tcb' # tcbs)) (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tp tcb else qprev') (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tn tcb else qhead') proof (state)
this:
tcb_queue_relation tn tp mp (tcb' # tcbs) qprev' qhead'
\<forall>t\<in>set (tcb' # tcbs). tcb_at' t s
distinct (tcb' # tcbs)
ctcb_ptr_to_tcb_ptr qprev' \<notin> set (tcb' # tcbs)
tcbp \<in> set (tcb' # tcbs)

goal (2 subgoals):
 1. tcbp = tcb' \<Longrightarrow> tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp (tcb' # tcbs)) (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tp tcb else qprev') (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tn tcb else qhead')
 2. tcbp \<in> set tcbs \<Longrightarrow> tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp (tcb' # tcbs)) (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tp tcb else qprev') (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tn tcb else qhead') proof (state)
this:
\<lbrakk>tcb_queue_relation tn tp mp tcbs ?qprev ?qhead; \<forall>t\<in>set tcbs. tcb_at' t s; distinct tcbs; ctcb_ptr_to_tcb_ptr ?qprev \<notin> set tcbs; tcbp \<in> set tcbs\<rbrakk> \<Longrightarrow> tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp tcbs) (if tcb_ptr_to_ctcb_ptr tcbp = ?qhead then tp tcb else ?qprev) (if tcb_ptr_to_ctcb_ptr tcbp = ?qhead then tn tcb else ?qhead)

goal (2 subgoals):
 1. tcbp = tcb' \<Longrightarrow> tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp (tcb' # tcbs)) (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tp tcb else qprev') (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tn tcb else qhead')
 2. tcbp \<in> set tcbs \<Longrightarrow> tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp (tcb' # tcbs)) (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tp tcb else qprev') (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tn tcb else qhead') proof (prove)
goal (1 subgoal):
 1. tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp (tcb' # tcbs)) (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tp tcb else qprev') (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tn tcb else qhead') proof (state)
goal (2 subgoals):
 1. tcbs = [] \<Longrightarrow> tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp (tcb' # tcbs)) (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tp tcb else qprev') (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tn tcb else qhead')
 2. \<And>a list. tcbs = a # list \<Longrightarrow> tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp (tcb' # tcbs)) (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tp tcb else qprev') (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tn tcb else qhead') proof (state)
this:
tcbs = []

goal (2 subgoals):
 1. tcbs = [] \<Longrightarrow> tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp (tcb' # tcbs)) (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tp tcb else qprev') (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tn tcb else qhead')
 2. \<And>a list. tcbs = a # list \<Longrightarrow> tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp (tcb' # tcbs)) (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tp tcb else qprev') (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tn tcb else qhead') proof (prove)
using this:
tcbs = []

goal (1 subgoal):
 1. tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp (tcb' # tcbs)) (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tp tcb else qprev') (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tn tcb else qhead') proof (prove)
using this:
tcbs = []
tcb_queue_relation tn tp mp (tcb' # tcbs) qprev' qhead'
\<forall>t\<in>set (tcb' # tcbs). tcb_at' t s
distinct (tcb' # tcbs)
ctcb_ptr_to_tcb_ptr qprev' \<notin> set (tcb' # tcbs)
tcbp \<in> set (tcb' # tcbs)
tcbp = tcb'
mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb

goal (1 subgoal):
 1. tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp (tcb' # tcbs)) (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tp tcb else qprev') (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tn tcb else qhead') proof (state)
this:
tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp (tcb' # tcbs)) (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tp tcb else qprev') (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tn tcb else qhead')

goal (1 subgoal):
 1. \<And>a list. tcbs = a # list \<Longrightarrow> tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp (tcb' # tcbs)) (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tp tcb else qprev') (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tn tcb else qhead') proof (state)
goal (1 subgoal):
 1. \<And>a list. tcbs = a # list \<Longrightarrow> tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp (tcb' # tcbs)) (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tp tcb else qprev') (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tn tcb else qhead') proof (state)
this:
tcbs = tcbs_hd # tcbss

goal (1 subgoal):
 1. \<And>a list. tcbs = a # list \<Longrightarrow> tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp (tcb' # tcbs)) (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tp tcb else qprev') (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tn tcb else qhead') proof (prove)
goal (1 subgoal):
 1. tn tcb \<noteq> NULL proof (prove)
using this:
tcb_queue_relation tn tp mp tcbs (tcb_ptr_to_ctcb_ptr tcb') (tn tcb)

goal (1 subgoal):
 1. tn tcb \<noteq> NULL proof (state)
goal (3 subgoals):
 1. \<forall>t\<in>set tcbs. tcb_at' t ?s
 2. distinct tcbs
 3. tcbs \<noteq> [] proof (chain)
picking this:
tcb_queue_relation tn tp mp (tcb' # tcbs) qprev' qhead'
\<forall>t\<in>set (tcb' # tcbs). tcb_at' t s
distinct (tcb' # tcbs)
ctcb_ptr_to_tcb_ptr qprev' \<notin> set (tcb' # tcbs)
tcbp \<in> set (tcb' # tcbs) proof (prove)
using this:
tcb_queue_relation tn tp mp (tcb' # tcbs) qprev' qhead'
\<forall>t\<in>set (tcb' # tcbs). tcb_at' t s
distinct (tcb' # tcbs)
ctcb_ptr_to_tcb_ptr qprev' \<notin> set (tcb' # tcbs)
tcbp \<in> set (tcb' # tcbs)

goal (1 subgoal):
 1. \<forall>t\<in>set tcbs. tcb_at' t s &&& distinct tcbs proof (state)
this:
\<forall>t\<in>set tcbs. tcb_at' t s
distinct tcbs

goal (1 subgoal):
 1. tcbs \<noteq> [] proof (prove)
goal (1 subgoal):
 1. tcbs \<noteq> [] proof (prove)
using this:
tcbs = tcbs_hd # tcbss

goal (1 subgoal):
 1. tcbs \<noteq> [] proof (state)
this:
tcbs \<noteq> []

goal:
No subgoals! proof (state)
this:
tn tcb \<noteq> NULL

goal (1 subgoal):
 1. \<And>a list. tcbs = a # list \<Longrightarrow> tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp (tcb' # tcbs)) (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tp tcb else qprev') (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tn tcb else qhead') proof (chain)
picking this:
tcbs = tcbs_hd # tcbss
tcb_queue_relation tn tp mp (tcb' # tcbs) qprev' qhead'
\<forall>t\<in>set (tcb' # tcbs). tcb_at' t s
distinct (tcb' # tcbs)
ctcb_ptr_to_tcb_ptr qprev' \<notin> set (tcb' # tcbs)
tcbp \<in> set (tcb' # tcbs) proof (prove)
using this:
tcbs = tcbs_hd # tcbss
tcb_queue_relation tn tp mp (tcb' # tcbs) qprev' qhead'
\<forall>t\<in>set (tcb' # tcbs). tcb_at' t s
distinct (tcb' # tcbs)
ctcb_ptr_to_tcb_ptr qprev' \<notin> set (tcb' # tcbs)
tcbp \<in> set (tcb' # tcbs)

goal (1 subgoal):
 1. tcbs_hd \<notin> set tcbss proof (state)
this:
tcbs_hd \<notin> set tcbss

goal (1 subgoal):
 1. \<And>a list. tcbs = a # list \<Longrightarrow> tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp (tcb' # tcbs)) (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tp tcb else qprev') (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tn tcb else qhead') proof (prove)
using this:
tcbs_hd \<notin> set tcbss

goal (1 subgoal):
 1. \<And>p. p \<in> tcb_ptr_to_ctcb_ptr ` set tcbss \<Longrightarrow> upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp) p = mp p proof (prove)
using this:
tcbs_hd \<notin> set tcbss
tcb_queue_relation tn tp mp tcbs (tcb_ptr_to_ctcb_ptr tcb') (tn tcb)
mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb
tcbp = tcb'
tcbs = tcbs_hd # tcbss
tn tcb \<noteq> NULL
tcb_queue_relation tn tp mp (tcb' # tcbs) qprev' qhead'
\<forall>t\<in>set (tcb' # tcbs). tcb_at' t s
distinct (tcb' # tcbs)
ctcb_ptr_to_tcb_ptr qprev' \<notin> set (tcb' # tcbs)
tcbp \<in> set (tcb' # tcbs)

goal (1 subgoal):
 1. \<And>p. p \<in> tcb_ptr_to_ctcb_ptr ` set tcbss \<Longrightarrow> upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp) p = mp p proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>p \<in> tcb_ptr_to_ctcb_ptr ` set tcbss; tcbs_hd \<notin> set tcbss; tcb_queue_relation tn tp mp tcbs (tcb_ptr_to_ctcb_ptr tcb') (tn tcb); mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; tcbp = tcb'; tcbs = tcbs_hd # tcbss; tn tcb \<noteq> NULL; tcb_queue_relation tn tp mp (tcb' # tcbs) qprev' qhead'; \<forall>t\<in>set (tcb' # tcbs). tcb_at' t s; distinct (tcb' # tcbs); ctcb_ptr_to_tcb_ptr qprev' \<notin> set (tcb' # tcbs); tcbp \<in> set (tcb' # tcbs)\<rbrakk> \<Longrightarrow> upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp) p = mp p proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>p \<in> tcb_ptr_to_ctcb_ptr ` set tcbss; tcbs_hd \<notin> set tcbss; tcb_queue_relation tn tp mp tcbs (tcb_ptr_to_ctcb_ptr tcb') (tn tcb); mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; tcbp = tcb'; tcbs = tcbs_hd # tcbss; tn tcb \<noteq> NULL; tcb_queue_relation tn tp mp (tcb' # tcbs) qprev' qhead'; \<forall>t\<in>set (tcb' # tcbs). tcb_at' t s; distinct (tcb' # tcbs); ctcb_ptr_to_tcb_ptr qprev' \<notin> set (tcb' # tcbs); tcbp \<in> set (tcb' # tcbs)\<rbrakk> \<Longrightarrow> mp p = mp p proof (prove)
goal:
No subgoals! proof (state)
this:
?p \<in> tcb_ptr_to_ctcb_ptr ` set tcbss \<Longrightarrow> upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp) ?p = mp ?p

goal (1 subgoal):
 1. \<And>a list. tcbs = a # list \<Longrightarrow> tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp (tcb' # tcbs)) (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tp tcb else qprev') (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tn tcb else qhead') proof (prove)
goal (1 subgoal):
 1. tcb_ptr_to_ctcb_ptr tcbp \<noteq> tn tcb \<and> tcb_ptr_to_ctcb_ptr tcbp \<noteq> tp tcb \<and> tn tcb \<noteq> tp tcb proof (prove)
using this:
tcb_queue_relation tn tp mp tcbs (tcb_ptr_to_ctcb_ptr tcb') (tn tcb)
mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb
tcb_queue_relation tn tp mp (tcb' # tcbs) qprev' qhead'
\<forall>t\<in>set (tcb' # tcbs). tcb_at' t s
distinct (tcb' # tcbs)
ctcb_ptr_to_tcb_ptr qprev' \<notin> set (tcb' # tcbs)
tcbp \<in> set (tcb' # tcbs)
tn tcb \<noteq> NULL

goal (1 subgoal):
 1. tcb_ptr_to_ctcb_ptr tcbp \<noteq> tn tcb \<and> tcb_ptr_to_ctcb_ptr tcbp \<noteq> tp tcb \<and> tn tcb \<noteq> tp tcb proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_queue_relation tn tp mp tcbs (tcb_ptr_to_ctcb_ptr tcb') (tn tcb); mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; tcb_queue_relation tn tp mp (tcb' # tcbs) qprev' qhead'; \<forall>t\<in>set (tcb' # tcbs). tcb_at' t s; distinct (tcb' # tcbs); ctcb_ptr_to_tcb_ptr qprev' \<notin> set (tcb' # tcbs); tcbp \<in> set (tcb' # tcbs); tn tcb \<noteq> NULL\<rbrakk> \<Longrightarrow> tcb_ptr_to_ctcb_ptr tcbp \<noteq> tn tcb \<and> tcb_ptr_to_ctcb_ptr tcbp \<noteq> tp tcb \<and> tn tcb \<noteq> tp tcb proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_queue_relation tn tp mp tcbs (tcb_ptr_to_ctcb_ptr tcb') (tn tcb); mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; \<forall>t\<in>set (tcb' # tcbs). tcb_at' t s; distinct (tcb' # tcbs); ctcb_ptr_to_tcb_ptr qprev' \<notin> set (tcb' # tcbs); tcbp \<in> set (tcb' # tcbs); tn tcb \<noteq> NULL; tcb_ptr_to_ctcb_ptr tcbp \<noteq> tn tcb \<and> tcb_ptr_to_ctcb_ptr tcbp \<noteq> tp tcb \<and> (tn tcb \<noteq> NULL \<longrightarrow> tn tcb \<noteq> tp tcb)\<rbrakk> \<Longrightarrow> tcb_ptr_to_ctcb_ptr tcbp \<noteq> tn tcb \<and> tcb_ptr_to_ctcb_ptr tcbp \<noteq> tp tcb \<and> tn tcb \<noteq> tp tcb proof (prove)
goal:
No subgoals! proof (state)
this:
tcb_ptr_to_ctcb_ptr tcbp \<noteq> tn tcb \<and> tcb_ptr_to_ctcb_ptr tcbp \<noteq> tp tcb \<and> tn tcb \<noteq> tp tcb

goal (1 subgoal):
 1. \<And>a list. tcbs = a # list \<Longrightarrow> tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp (tcb' # tcbs)) (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tp tcb else qprev') (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tn tcb else qhead') proof (prove)
using this:
tcb_ptr_to_ctcb_ptr tcbp \<noteq> tn tcb \<and> tcb_ptr_to_ctcb_ptr tcbp \<noteq> tp tcb \<and> tn tcb \<noteq> tp tcb

goal (1 subgoal):
 1. upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp) (tcb_ptr_to_ctcb_ptr tcbs_hd) = Some (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) proof (prove)
using this:
tcb_ptr_to_ctcb_ptr tcbp \<noteq> tn tcb \<and> tcb_ptr_to_ctcb_ptr tcbp \<noteq> tp tcb \<and> tn tcb \<noteq> tp tcb
qprev' = tp tcb
qhead' = tcb_ptr_to_ctcb_ptr tcb'
tcb_queue_relation tn tp mp tcbs (tcb_ptr_to_ctcb_ptr tcb') (tn tcb)
mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb
tcbp = tcb'
tcbs = tcbs_hd # tcbss
tn tcb \<noteq> NULL

goal (1 subgoal):
 1. upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp) (tcb_ptr_to_ctcb_ptr tcbs_hd) = Some (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) proof (state)
this:
upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp) (tcb_ptr_to_ctcb_ptr tcbs_hd) = Some (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb))))

goal (1 subgoal):
 1. \<And>a list. tcbs = a # list \<Longrightarrow> tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp (tcb' # tcbs)) (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tp tcb else qprev') (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tn tcb else qhead') proof (prove)
using this:
upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp) (tcb_ptr_to_ctcb_ptr tcbs_hd) = Some (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb))))

goal (1 subgoal):
 1. tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp (tcb' # tcbs)) (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tp tcb else qprev') (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tn tcb else qhead') proof (prove)
using this:
upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp) (tcb_ptr_to_ctcb_ptr tcbs_hd) = Some (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb))))
qprev' = tp tcb
qhead' = tcb_ptr_to_ctcb_ptr tcb'
tcb_queue_relation tn tp mp tcbs (tcb_ptr_to_ctcb_ptr tcb') (tn tcb)
mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb
tcbp = tcb'
tcbs = tcbs_hd # tcbss
tn tcb \<noteq> NULL

goal (1 subgoal):
 1. tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp (tcb' # tcbs)) (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tp tcb else qprev') (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tn tcb else qhead') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp) (tcb_ptr_to_ctcb_ptr tcbs_hd) = Some (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))); qprev' = tp tcb; qhead' = tcb_ptr_to_ctcb_ptr tcb'; tcb_queue_relation tn tp mp tcbs (tcb_ptr_to_ctcb_ptr tcb') (tn tcb); mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; tcbp = tcb'; tcbs = tcbs_hd # tcbss; tn tcb \<noteq> NULL\<rbrakk> \<Longrightarrow> (if tcb_ptr_to_ctcb_ptr tcb' = qhead' then tn tcb else qhead') = tcb_ptr_to_ctcb_ptr tcbs_hd \<and> (\<exists>tcba. upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp) (if tcb_ptr_to_ctcb_ptr tcb' = qhead' then tn tcb else qhead') = Some tcba \<and> tp tcba = (if tcb_ptr_to_ctcb_ptr tcb' = qhead' then tp tcb else qprev') \<and> tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) tcbss (if tcb_ptr_to_ctcb_ptr tcb' = qhead' then tn tcb else qhead') (tn tcba)) proof (prove)
goal (2 subgoals):
 1. \<And>tcba p. \<lbrakk>upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp) (tcb_ptr_to_ctcb_ptr tcbs_hd) = Some (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))); qprev' = tp tcb; qhead' = tcb_ptr_to_ctcb_ptr tcb'; tcb_queue_relation tn tp mp tcbs (tcb_ptr_to_ctcb_ptr tcb') (tn tcb); mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; tcbp = tcb'; tcbs = tcbs_hd # tcbss; tn tcb \<noteq> NULL; p \<in> tcb_ptr_to_ctcb_ptr ` set tcbss\<rbrakk> \<Longrightarrow> p \<in> tcb_ptr_to_ctcb_ptr ` set tcbss
 2. \<lbrakk>upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp) (tcb_ptr_to_ctcb_ptr tcbs_hd) = Some (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))); qprev' = tp tcb; qhead' = tcb_ptr_to_ctcb_ptr tcb'; tcb_queue_relation tn tp mp tcbs (tcb_ptr_to_ctcb_ptr tcb') (tn tcb); mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; tcbp = tcb'; tcbs = tcbs_hd # tcbss; tn tcb \<noteq> NULL\<rbrakk> \<Longrightarrow> (if tcb_ptr_to_ctcb_ptr tcb' = qhead' then tn tcb else qhead') = tcb_ptr_to_ctcb_ptr tcbs_hd \<and> (\<exists>tcba. upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp) (if tcb_ptr_to_ctcb_ptr tcb' = qhead' then tn tcb else qhead') = Some tcba \<and> tp tcba = (if tcb_ptr_to_ctcb_ptr tcb' = qhead' then tp tcb else qprev') \<and> tcb_queue_relation tn tp mp tcbss (if tcb_ptr_to_ctcb_ptr tcb' = qhead' then tn tcb else qhead') (tn tcba)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp) (tcb_ptr_to_ctcb_ptr tcbs_hd) = Some (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))); qprev' = tp tcb; qhead' = tcb_ptr_to_ctcb_ptr tcb'; tcb_queue_relation tn tp mp tcbs (tcb_ptr_to_ctcb_ptr tcb') (tn tcb); mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; tcbp = tcb'; tcbs = tcbs_hd # tcbss; tn tcb \<noteq> NULL\<rbrakk> \<Longrightarrow> (if tcb_ptr_to_ctcb_ptr tcb' = qhead' then tn tcb else qhead') = tcb_ptr_to_ctcb_ptr tcbs_hd \<and> (\<exists>tcba. upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp) (if tcb_ptr_to_ctcb_ptr tcb' = qhead' then tn tcb else qhead') = Some tcba \<and> tp tcba = (if tcb_ptr_to_ctcb_ptr tcb' = qhead' then tp tcb else qprev') \<and> tcb_queue_relation tn tp mp tcbss (if tcb_ptr_to_ctcb_ptr tcb' = qhead' then tn tcb else qhead') (tn tcba)) proof (prove)
goal:
No subgoals! proof (state)
this:
tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp (tcb' # tcbs)) (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tp tcb else qprev') (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tn tcb else qhead')

goal:
No subgoals! proof (state)
this:
tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp (tcb' # tcbs)) (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tp tcb else qprev') (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tn tcb else qhead')

goal (1 subgoal):
 1. tcbp \<in> set tcbs \<Longrightarrow> tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp (tcb' # tcbs)) (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tp tcb else qprev') (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tn tcb else qhead') proof (state)
goal (1 subgoal):
 1. tcbp \<in> set tcbs \<Longrightarrow> tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp (tcb' # tcbs)) (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tp tcb else qprev') (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tn tcb else qhead') proof (state)
this:
tcbp \<in> set tcbs

goal (1 subgoal):
 1. tcbp \<in> set tcbs \<Longrightarrow> tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp (tcb' # tcbs)) (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tp tcb else qprev') (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tn tcb else qhead') proof (prove)
using this:
tcbp \<in> set tcbs

goal (1 subgoal):
 1. tcbp \<noteq> tcb' proof (prove)
using this:
tcbp \<in> set tcbs
tcb_queue_relation tn tp mp (tcb' # tcbs) qprev' qhead'
\<forall>t\<in>set (tcb' # tcbs). tcb_at' t s
distinct (tcb' # tcbs)
ctcb_ptr_to_tcb_ptr qprev' \<notin> set (tcb' # tcbs)
tcbp \<in> set (tcb' # tcbs)

goal (1 subgoal):
 1. tcbp \<noteq> tcb' proof (state)
this:
tcbp \<noteq> tcb'

goal (1 subgoal):
 1. tcbp \<in> set tcbs \<Longrightarrow> tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp (tcb' # tcbs)) (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tp tcb else qprev') (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tn tcb else qhead') proof (prove)
goal (1 subgoal):
 1. (\<And>tcb2. \<lbrakk>mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcb2; tcb_queue_relation tn tp mp tcbs (tcb_ptr_to_ctcb_ptr tcb') (tn tcb2); qhead' = tcb_ptr_to_ctcb_ptr tcb'; qprev' = tp tcb2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (prove)
using this:
tcb_queue_relation tn tp mp (tcb' # tcbs) qprev' qhead'
\<forall>t\<in>set (tcb' # tcbs). tcb_at' t s
distinct (tcb' # tcbs)
ctcb_ptr_to_tcb_ptr qprev' \<notin> set (tcb' # tcbs)
tcbp \<in> set (tcb' # tcbs)

goal (1 subgoal):
 1. (\<And>tcb2. \<lbrakk>mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcb2; tcb_queue_relation tn tp mp tcbs (tcb_ptr_to_ctcb_ptr tcb') (tn tcb2); qhead' = tcb_ptr_to_ctcb_ptr tcb'; qprev' = tp tcb2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcb2
tcb_queue_relation tn tp mp tcbs (tcb_ptr_to_ctcb_ptr tcb') (tn tcb2)
qhead' = tcb_ptr_to_ctcb_ptr tcb'
qprev' = tp tcb2

goal (1 subgoal):
 1. tcbp \<in> set tcbs \<Longrightarrow> tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp (tcb' # tcbs)) (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tp tcb else qprev') (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tn tcb else qhead') proof (prove)
goal (1 subgoal):
 1. tcb_ptr_to_ctcb_ptr tcb' \<noteq> NULL proof (prove)
using this:
tcb_queue_relation tn tp mp (tcb' # tcbs) qprev' qhead'
\<forall>t\<in>set (tcb' # tcbs). tcb_at' t s
distinct (tcb' # tcbs)
ctcb_ptr_to_tcb_ptr qprev' \<notin> set (tcb' # tcbs)
tcbp \<in> set (tcb' # tcbs)

goal (1 subgoal):
 1. tcb_ptr_to_ctcb_ptr tcb' \<noteq> NULL proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_queue_relation tn tp mp (tcb' # tcbs) qprev' qhead'; \<forall>t\<in>set (tcb' # tcbs). tcb_at' t s; distinct (tcb' # tcbs); ctcb_ptr_to_tcb_ptr qprev' \<notin> set (tcb' # tcbs); tcbp \<in> set (tcb' # tcbs)\<rbrakk> \<Longrightarrow> tcb_ptr_to_ctcb_ptr tcb' \<noteq> NULL proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>t\<in>set (tcb' # tcbs). tcb_at' t s; distinct (tcb' # tcbs); ctcb_ptr_to_tcb_ptr qprev' \<notin> set (tcb' # tcbs); tcbp \<in> set (tcb' # tcbs)\<rbrakk> \<Longrightarrow> tcb' \<in> set (tcb' # tcbs) proof (prove)
goal:
No subgoals! proof (state)
this:
tcb_ptr_to_ctcb_ptr tcb' \<noteq> NULL

goal (1 subgoal):
 1. tcbp \<in> set tcbs \<Longrightarrow> tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp (tcb' # tcbs)) (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tp tcb else qprev') (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tn tcb else qhead') proof (prove)
goal (1 subgoal):
 1. tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp tcbs) (if tcb_ptr_to_ctcb_ptr tcbp = tn tcb2 then tp tcb else tcb_ptr_to_ctcb_ptr tcb') (if tcb_ptr_to_ctcb_ptr tcbp = tn tcb2 then tn tcb else tn tcb2) proof (prove)
using this:
tcb_queue_relation tn tp mp tcbs (tcb_ptr_to_ctcb_ptr tcb') (tn tcb2)

goal (1 subgoal):
 1. tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp tcbs) (if tcb_ptr_to_ctcb_ptr tcbp = tn tcb2 then tp tcb else tcb_ptr_to_ctcb_ptr tcb') (if tcb_ptr_to_ctcb_ptr tcbp = tn tcb2 then tn tcb else tn tcb2) proof (state)
goal (4 subgoals):
 1. \<forall>t\<in>set tcbs. tcb_at' t s
 2. distinct tcbs
 3. ctcb_ptr_to_tcb_ptr (tcb_ptr_to_ctcb_ptr tcb') \<notin> set tcbs
 4. tcbp \<in> set tcbs proof (chain)
picking this:
tcb_queue_relation tn tp mp (tcb' # tcbs) qprev' qhead'
\<forall>t\<in>set (tcb' # tcbs). tcb_at' t s
distinct (tcb' # tcbs)
ctcb_ptr_to_tcb_ptr qprev' \<notin> set (tcb' # tcbs)
tcbp \<in> set (tcb' # tcbs) proof (prove)
using this:
tcb_queue_relation tn tp mp (tcb' # tcbs) qprev' qhead'
\<forall>t\<in>set (tcb' # tcbs). tcb_at' t s
distinct (tcb' # tcbs)
ctcb_ptr_to_tcb_ptr qprev' \<notin> set (tcb' # tcbs)
tcbp \<in> set (tcb' # tcbs)

goal (1 subgoal):
 1. \<forall>t\<in>set tcbs. tcb_at' t s &&& distinct tcbs &&& ctcb_ptr_to_tcb_ptr (tcb_ptr_to_ctcb_ptr tcb') \<notin> set tcbs proof (state)
this:
\<forall>t\<in>set tcbs. tcb_at' t s
distinct tcbs
ctcb_ptr_to_tcb_ptr (tcb_ptr_to_ctcb_ptr tcb') \<notin> set tcbs

goal (1 subgoal):
 1. tcbp \<in> set tcbs proof (state)
this:
tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp tcbs) (if tcb_ptr_to_ctcb_ptr tcbp = tn tcb2 then tp tcb else tcb_ptr_to_ctcb_ptr tcb') (if tcb_ptr_to_ctcb_ptr tcbp = tn tcb2 then tn tcb else tn tcb2)

goal (1 subgoal):
 1. tcbp \<in> set tcbs \<Longrightarrow> tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp (tcb' # tcbs)) (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tp tcb else qprev') (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tn tcb else qhead') proof (prove)
goal (1 subgoal):
 1. tn tcb \<noteq> tcb_ptr_to_ctcb_ptr tcb' proof (prove)
using this:
tcb_queue_relation tn tp mp (tcb' # tcbs) qprev' qhead'
\<forall>t\<in>set (tcb' # tcbs). tcb_at' t s
distinct (tcb' # tcbs)
ctcb_ptr_to_tcb_ptr qprev' \<notin> set (tcb' # tcbs)
tcbp \<in> set (tcb' # tcbs)
\<lbrakk>\<forall>t\<in>set (tcb' # tcbs). tcb_at' t ?s; distinct (tcb' # tcbs); tcbp \<in> set (tcb' # tcbs); tcb' \<in> set (tcb' # tcbs); ctcb_ptr_to_tcb_ptr qprev' \<notin> set (tcb' # tcbs); tcbp \<noteq> tcb'\<rbrakk> \<Longrightarrow> (tn tcb = tcb_ptr_to_ctcb_ptr tcb') = (tp tcb2 = tcb_ptr_to_ctcb_ptr tcbp)
tcbp \<noteq> tcb'
tp tcb2 = qprev'

goal (1 subgoal):
 1. tn tcb \<noteq> tcb_ptr_to_ctcb_ptr tcb' proof (state)
this:
tn tcb \<noteq> tcb_ptr_to_ctcb_ptr tcb'

goal (1 subgoal):
 1. tcbp \<in> set tcbs \<Longrightarrow> tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp (tcb' # tcbs)) (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tp tcb else qprev') (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tn tcb else qhead') proof (prove)
goal (1 subgoal):
 1. tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp (tcb' # tcbs)) (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tp tcb else qprev') (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tn tcb else qhead') proof (prove)
using this:
tcbp \<noteq> tcb'

goal (1 subgoal):
 1. tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp (tcb' # tcbs)) (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tp tcb else qprev') (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tn tcb else qhead') proof (state)
goal (2 subgoals):
 1. \<lbrakk>tcbp \<noteq> tcb'; tn tcb2 = tcb_ptr_to_ctcb_ptr tcbp\<rbrakk> \<Longrightarrow> tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp (tcb' # tcbs)) (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tp tcb else qprev') (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tn tcb else qhead')
 2. \<lbrakk>tcbp \<noteq> tcb'; tn tcb2 \<noteq> tcb_ptr_to_ctcb_ptr tcbp\<rbrakk> \<Longrightarrow> tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp (tcb' # tcbs)) (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tp tcb else qprev') (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tn tcb else qhead') proof (state)
this:
tn tcb2 = tcb_ptr_to_ctcb_ptr tcbp

goal (2 subgoals):
 1. \<lbrakk>tcbp \<noteq> tcb'; tn tcb2 = tcb_ptr_to_ctcb_ptr tcbp\<rbrakk> \<Longrightarrow> tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp (tcb' # tcbs)) (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tp tcb else qprev') (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tn tcb else qhead')
 2. \<lbrakk>tcbp \<noteq> tcb'; tn tcb2 \<noteq> tcb_ptr_to_ctcb_ptr tcbp\<rbrakk> \<Longrightarrow> tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp (tcb' # tcbs)) (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tp tcb else qprev') (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tn tcb else qhead') proof (prove)
using this:
tn tcb2 = tcb_ptr_to_ctcb_ptr tcbp

goal (1 subgoal):
 1. tp tcb = tcb_ptr_to_ctcb_ptr tcb' proof (prove)
using this:
tn tcb2 = tcb_ptr_to_ctcb_ptr tcbp
tcb_queue_relation tn tp mp (tcb' # tcbs) qprev' qhead'
\<forall>t\<in>set (tcb' # tcbs). tcb_at' t s
distinct (tcb' # tcbs)
ctcb_ptr_to_tcb_ptr qprev' \<notin> set (tcb' # tcbs)
tcbp \<in> set (tcb' # tcbs)
mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcb2
mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb
tcb' \<noteq> tcbp

goal (1 subgoal):
 1. tp tcb = tcb_ptr_to_ctcb_ptr tcb' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tn tcb2 = tcb_ptr_to_ctcb_ptr tcbp; tcb_queue_relation tn tp mp (tcb' # tcbs) qprev' qhead'; \<forall>t\<in>set (tcb' # tcbs). tcb_at' t s; distinct (tcb' # tcbs); ctcb_ptr_to_tcb_ptr qprev' \<notin> set (tcb' # tcbs); tcbp \<in> set (tcb' # tcbs); mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcb2; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; tcb' \<noteq> tcbp\<rbrakk> \<Longrightarrow> tp tcb = tcb_ptr_to_ctcb_ptr tcb' proof (prove)
goal (5 subgoals):
 1. \<lbrakk>tn tcb2 = tcb_ptr_to_ctcb_ptr tcbp; tcb_queue_relation tn tp mp (tcb' # tcbs) qprev' qhead'; \<forall>t\<in>set (tcb' # tcbs). tcb_at' t s; distinct (tcb' # tcbs); ctcb_ptr_to_tcb_ptr qprev' \<notin> set (tcb' # tcbs); tcbp \<in> set (tcb' # tcbs); mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcb2; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; tcb' \<noteq> tcbp\<rbrakk> \<Longrightarrow> tcb' \<in> set (tcb' # tcbs)
 2. \<lbrakk>tn tcb2 = tcb_ptr_to_ctcb_ptr tcbp; tcb_queue_relation tn tp mp (tcb' # tcbs) qprev' qhead'; \<forall>t\<in>set (tcb' # tcbs). tcb_at' t s; distinct (tcb' # tcbs); ctcb_ptr_to_tcb_ptr qprev' \<notin> set (tcb' # tcbs); tcbp \<in> set (tcb' # tcbs); mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcb2; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; tcb' \<noteq> tcbp\<rbrakk> \<Longrightarrow> tcbp \<in> set (tcb' # tcbs)
 3. \<lbrakk>tn tcb2 = tcb_ptr_to_ctcb_ptr tcbp; tcb_queue_relation tn tp mp (tcb' # tcbs) qprev' qhead'; \<forall>t\<in>set (tcb' # tcbs). tcb_at' t s; distinct (tcb' # tcbs); ctcb_ptr_to_tcb_ptr qprev' \<notin> set (tcb' # tcbs); tcbp \<in> set (tcb' # tcbs); mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcb2; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; tcb' \<noteq> tcbp\<rbrakk> \<Longrightarrow> ctcb_ptr_to_tcb_ptr qprev' \<notin> set (tcb' # tcbs)
 4. \<lbrakk>tn tcb2 = tcb_ptr_to_ctcb_ptr tcbp; tcb_queue_relation tn tp mp (tcb' # tcbs) qprev' qhead'; \<forall>t\<in>set (tcb' # tcbs). tcb_at' t s; distinct (tcb' # tcbs); ctcb_ptr_to_tcb_ptr qprev' \<notin> set (tcb' # tcbs); tcbp \<in> set (tcb' # tcbs); mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcb2; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; tcb' \<noteq> tcbp\<rbrakk> \<Longrightarrow> tcb' \<noteq> tcbp
 5. \<lbrakk>tn tcb2 = tcb_ptr_to_ctcb_ptr tcbp; tcb_queue_relation tn tp mp (tcb' # tcbs) qprev' qhead'; \<forall>t\<in>set (tcb' # tcbs). tcb_at' t s; distinct (tcb' # tcbs); ctcb_ptr_to_tcb_ptr qprev' \<notin> set (tcb' # tcbs); tcbp \<in> set (tcb' # tcbs); mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcb2; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; tcb' \<noteq> tcbp\<rbrakk> \<Longrightarrow> tn tcb2 = tcb_ptr_to_ctcb_ptr tcbp proof (prove)
goal (4 subgoals):
 1. \<lbrakk>tn tcb2 = tcb_ptr_to_ctcb_ptr tcbp; tcb_queue_relation tn tp mp (tcb' # tcbs) qprev' qhead'; \<forall>t\<in>set (tcb' # tcbs). tcb_at' t s; distinct (tcb' # tcbs); ctcb_ptr_to_tcb_ptr qprev' \<notin> set (tcb' # tcbs); tcbp \<in> set (tcb' # tcbs); mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcb2; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; tcb' \<noteq> tcbp\<rbrakk> \<Longrightarrow> tcbp \<in> set (tcb' # tcbs)
 2. \<lbrakk>tn tcb2 = tcb_ptr_to_ctcb_ptr tcbp; tcb_queue_relation tn tp mp (tcb' # tcbs) qprev' qhead'; \<forall>t\<in>set (tcb' # tcbs). tcb_at' t s; distinct (tcb' # tcbs); ctcb_ptr_to_tcb_ptr qprev' \<notin> set (tcb' # tcbs); tcbp \<in> set (tcb' # tcbs); mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcb2; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; tcb' \<noteq> tcbp\<rbrakk> \<Longrightarrow> ctcb_ptr_to_tcb_ptr qprev' \<notin> set (tcb' # tcbs)
 3. \<lbrakk>tn tcb2 = tcb_ptr_to_ctcb_ptr tcbp; tcb_queue_relation tn tp mp (tcb' # tcbs) qprev' qhead'; \<forall>t\<in>set (tcb' # tcbs). tcb_at' t s; distinct (tcb' # tcbs); ctcb_ptr_to_tcb_ptr qprev' \<notin> set (tcb' # tcbs); tcbp \<in> set (tcb' # tcbs); mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcb2; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; tcb' \<noteq> tcbp\<rbrakk> \<Longrightarrow> tcb' \<noteq> tcbp
 4. \<lbrakk>tn tcb2 = tcb_ptr_to_ctcb_ptr tcbp; tcb_queue_relation tn tp mp (tcb' # tcbs) qprev' qhead'; \<forall>t\<in>set (tcb' # tcbs). tcb_at' t s; distinct (tcb' # tcbs); ctcb_ptr_to_tcb_ptr qprev' \<notin> set (tcb' # tcbs); tcbp \<in> set (tcb' # tcbs); mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcb2; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; tcb' \<noteq> tcbp\<rbrakk> \<Longrightarrow> tn tcb2 = tcb_ptr_to_ctcb_ptr tcbp proof (prove)
goal (3 subgoals):
 1. \<lbrakk>tn tcb2 = tcb_ptr_to_ctcb_ptr tcbp; tcb_queue_relation tn tp mp (tcb' # tcbs) qprev' qhead'; \<forall>t\<in>set (tcb' # tcbs). tcb_at' t s; distinct (tcb' # tcbs); ctcb_ptr_to_tcb_ptr qprev' \<notin> set (tcb' # tcbs); tcbp \<in> set (tcb' # tcbs); mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcb2; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; tcb' \<noteq> tcbp\<rbrakk> \<Longrightarrow> ctcb_ptr_to_tcb_ptr qprev' \<notin> set (tcb' # tcbs)
 2. \<lbrakk>tn tcb2 = tcb_ptr_to_ctcb_ptr tcbp; tcb_queue_relation tn tp mp (tcb' # tcbs) qprev' qhead'; \<forall>t\<in>set (tcb' # tcbs). tcb_at' t s; distinct (tcb' # tcbs); ctcb_ptr_to_tcb_ptr qprev' \<notin> set (tcb' # tcbs); tcbp \<in> set (tcb' # tcbs); mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcb2; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; tcb' \<noteq> tcbp\<rbrakk> \<Longrightarrow> tcb' \<noteq> tcbp
 3. \<lbrakk>tn tcb2 = tcb_ptr_to_ctcb_ptr tcbp; tcb_queue_relation tn tp mp (tcb' # tcbs) qprev' qhead'; \<forall>t\<in>set (tcb' # tcbs). tcb_at' t s; distinct (tcb' # tcbs); ctcb_ptr_to_tcb_ptr qprev' \<notin> set (tcb' # tcbs); tcbp \<in> set (tcb' # tcbs); mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcb2; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; tcb' \<noteq> tcbp\<rbrakk> \<Longrightarrow> tn tcb2 = tcb_ptr_to_ctcb_ptr tcbp proof (prove)
goal (2 subgoals):
 1. \<lbrakk>tn tcb2 = tcb_ptr_to_ctcb_ptr tcbp; tcb_queue_relation tn tp mp (tcb' # tcbs) qprev' qhead'; \<forall>t\<in>set (tcb' # tcbs). tcb_at' t s; distinct (tcb' # tcbs); ctcb_ptr_to_tcb_ptr qprev' \<notin> set (tcb' # tcbs); tcbp \<in> set (tcb' # tcbs); mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcb2; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; tcb' \<noteq> tcbp\<rbrakk> \<Longrightarrow> tcb' \<noteq> tcbp
 2. \<lbrakk>tn tcb2 = tcb_ptr_to_ctcb_ptr tcbp; tcb_queue_relation tn tp mp (tcb' # tcbs) qprev' qhead'; \<forall>t\<in>set (tcb' # tcbs). tcb_at' t s; distinct (tcb' # tcbs); ctcb_ptr_to_tcb_ptr qprev' \<notin> set (tcb' # tcbs); tcbp \<in> set (tcb' # tcbs); mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcb2; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; tcb' \<noteq> tcbp\<rbrakk> \<Longrightarrow> tn tcb2 = tcb_ptr_to_ctcb_ptr tcbp proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tn tcb2 = tcb_ptr_to_ctcb_ptr tcbp; tcb_queue_relation tn tp mp (tcb' # tcbs) qprev' qhead'; \<forall>t\<in>set (tcb' # tcbs). tcb_at' t s; distinct (tcb' # tcbs); ctcb_ptr_to_tcb_ptr qprev' \<notin> set (tcb' # tcbs); tcbp \<in> set (tcb' # tcbs); mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcb2; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; tcb' \<noteq> tcbp\<rbrakk> \<Longrightarrow> tn tcb2 = tcb_ptr_to_ctcb_ptr tcbp proof (prove)
goal:
No subgoals! proof (state)
this:
tp tcb = tcb_ptr_to_ctcb_ptr tcb'

goal (2 subgoals):
 1. \<lbrakk>tcbp \<noteq> tcb'; tn tcb2 = tcb_ptr_to_ctcb_ptr tcbp\<rbrakk> \<Longrightarrow> tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp (tcb' # tcbs)) (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tp tcb else qprev') (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tn tcb else qhead')
 2. \<lbrakk>tcbp \<noteq> tcb'; tn tcb2 \<noteq> tcb_ptr_to_ctcb_ptr tcbp\<rbrakk> \<Longrightarrow> tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp (tcb' # tcbs)) (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tp tcb else qprev') (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tn tcb else qhead') proof (prove)
using this:
tp tcb = tcb_ptr_to_ctcb_ptr tcb'

goal (1 subgoal):
 1. upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp) (tcb_ptr_to_ctcb_ptr tcb') = Some (tn_update (\<lambda>_. tn tcb) tcb2) proof (prove)
using this:
tp tcb = tcb_ptr_to_ctcb_ptr tcb'
tn tcb \<noteq> tcb_ptr_to_ctcb_ptr tcb'
tcb_ptr_to_ctcb_ptr tcb' \<noteq> NULL
mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcb2

goal (1 subgoal):
 1. upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp) (tcb_ptr_to_ctcb_ptr tcb') = Some (tn_update (\<lambda>_. tn tcb) tcb2) proof (prove)
using this:
tp tcb = tcb_ptr_to_ctcb_ptr tcb'
tn tcb \<noteq> tcb_ptr_to_ctcb_ptr tcb'
tcb_ptr_to_ctcb_ptr tcb' \<noteq> NULL
mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcb2

goal (1 subgoal):
 1. (if tn tcb = NULL then if tp tcb = NULL then mp else mp(tp tcb \<mapsto> tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) else (if tp tcb = NULL then mp else mp(tp tcb \<mapsto> tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))))(tn tcb \<mapsto> tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb))))) (tcb_ptr_to_ctcb_ptr tcb') = Some (tn_update (\<lambda>_. tn tcb) tcb2) proof (state)
this:
upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp) (tcb_ptr_to_ctcb_ptr tcb') = Some (tn_update (\<lambda>_. tn tcb) tcb2)

goal (2 subgoals):
 1. \<lbrakk>tcbp \<noteq> tcb'; tn tcb2 = tcb_ptr_to_ctcb_ptr tcbp\<rbrakk> \<Longrightarrow> tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp (tcb' # tcbs)) (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tp tcb else qprev') (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tn tcb else qhead')
 2. \<lbrakk>tcbp \<noteq> tcb'; tn tcb2 \<noteq> tcb_ptr_to_ctcb_ptr tcbp\<rbrakk> \<Longrightarrow> tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp (tcb' # tcbs)) (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tp tcb else qprev') (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tn tcb else qhead') proof (prove)
using this:
upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp) (tcb_ptr_to_ctcb_ptr tcb') = Some (tn_update (\<lambda>_. tn tcb) tcb2)

goal (1 subgoal):
 1. tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp (tcb' # tcbs)) (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tp tcb else qprev') (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tn tcb else qhead') proof (prove)
using this:
upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp) (tcb_ptr_to_ctcb_ptr tcb') = Some (tn_update (\<lambda>_. tn tcb) tcb2)
tcbp \<noteq> tcb'
mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb
qhead' = tcb_ptr_to_ctcb_ptr tcb'
qprev' = tp tcb2
tn tcb2 = tcb_ptr_to_ctcb_ptr tcbp
tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp tcbs) (if tcb_ptr_to_ctcb_ptr tcbp = tn tcb2 then tp tcb else tcb_ptr_to_ctcb_ptr tcb') (if tcb_ptr_to_ctcb_ptr tcbp = tn tcb2 then tn tcb else tn tcb2)
tp tcb = tcb_ptr_to_ctcb_ptr tcb'

goal (1 subgoal):
 1. tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp (tcb' # tcbs)) (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tp tcb else qprev') (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tn tcb else qhead') proof (state)
this:
tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp (tcb' # tcbs)) (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tp tcb else qprev') (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tn tcb else qhead')

goal (1 subgoal):
 1. \<lbrakk>tcbp \<noteq> tcb'; tn tcb2 \<noteq> tcb_ptr_to_ctcb_ptr tcbp\<rbrakk> \<Longrightarrow> tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp (tcb' # tcbs)) (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tp tcb else qprev') (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tn tcb else qhead') proof (state)
goal (1 subgoal):
 1. \<lbrakk>tcbp \<noteq> tcb'; tn tcb2 \<noteq> tcb_ptr_to_ctcb_ptr tcbp\<rbrakk> \<Longrightarrow> tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp (tcb' # tcbs)) (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tp tcb else qprev') (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tn tcb else qhead') proof (state)
this:
tn tcb2 \<noteq> tcb_ptr_to_ctcb_ptr tcbp

goal (1 subgoal):
 1. \<lbrakk>tcbp \<noteq> tcb'; tn tcb2 \<noteq> tcb_ptr_to_ctcb_ptr tcbp\<rbrakk> \<Longrightarrow> tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp (tcb' # tcbs)) (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tp tcb else qprev') (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tn tcb else qhead') proof (prove)
using this:
tn tcb2 \<noteq> tcb_ptr_to_ctcb_ptr tcbp

goal (1 subgoal):
 1. tp tcb \<noteq> tcb_ptr_to_ctcb_ptr tcb' proof (prove)
using this:
tn tcb2 \<noteq> tcb_ptr_to_ctcb_ptr tcbp
tcb_queue_relation tn tp mp (tcb' # tcbs) qprev' qhead'
\<forall>t\<in>set (tcb' # tcbs). tcb_at' t s
distinct (tcb' # tcbs)
ctcb_ptr_to_tcb_ptr qprev' \<notin> set (tcb' # tcbs)
tcbp \<in> set (tcb' # tcbs)
mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcb2
mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb
tcb' \<noteq> tcbp

goal (1 subgoal):
 1. tp tcb \<noteq> tcb_ptr_to_ctcb_ptr tcb' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tn tcb2 \<noteq> tcb_ptr_to_ctcb_ptr tcbp; tcb_queue_relation tn tp mp (tcb' # tcbs) qprev' qhead'; \<forall>t\<in>set (tcb' # tcbs). tcb_at' t s; distinct (tcb' # tcbs); ctcb_ptr_to_tcb_ptr qprev' \<notin> set (tcb' # tcbs); tcbp \<in> set (tcb' # tcbs); mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcb2; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; tcb' \<noteq> tcbp\<rbrakk> \<Longrightarrow> tp tcb \<noteq> tcb_ptr_to_ctcb_ptr tcb' proof (prove)
goal (5 subgoals):
 1. \<lbrakk>tn tcb2 \<noteq> tcb_ptr_to_ctcb_ptr tcbp; tcb_queue_relation tn tp mp (tcb' # tcbs) qprev' qhead'; \<forall>t\<in>set (tcb' # tcbs). tcb_at' t s; distinct (tcb' # tcbs); ctcb_ptr_to_tcb_ptr qprev' \<notin> set (tcb' # tcbs); tcbp \<in> set (tcb' # tcbs); mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcb2; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; tcb' \<noteq> tcbp\<rbrakk> \<Longrightarrow> tcb' \<in> set (tcb' # tcbs)
 2. \<lbrakk>tn tcb2 \<noteq> tcb_ptr_to_ctcb_ptr tcbp; tcb_queue_relation tn tp mp (tcb' # tcbs) qprev' qhead'; \<forall>t\<in>set (tcb' # tcbs). tcb_at' t s; distinct (tcb' # tcbs); ctcb_ptr_to_tcb_ptr qprev' \<notin> set (tcb' # tcbs); tcbp \<in> set (tcb' # tcbs); mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcb2; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; tcb' \<noteq> tcbp\<rbrakk> \<Longrightarrow> tcbp \<in> set (tcb' # tcbs)
 3. \<lbrakk>tn tcb2 \<noteq> tcb_ptr_to_ctcb_ptr tcbp; tcb_queue_relation tn tp mp (tcb' # tcbs) qprev' qhead'; \<forall>t\<in>set (tcb' # tcbs). tcb_at' t s; distinct (tcb' # tcbs); ctcb_ptr_to_tcb_ptr qprev' \<notin> set (tcb' # tcbs); tcbp \<in> set (tcb' # tcbs); mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcb2; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; tcb' \<noteq> tcbp\<rbrakk> \<Longrightarrow> ctcb_ptr_to_tcb_ptr qprev' \<notin> set (tcb' # tcbs)
 4. \<lbrakk>tn tcb2 \<noteq> tcb_ptr_to_ctcb_ptr tcbp; tcb_queue_relation tn tp mp (tcb' # tcbs) qprev' qhead'; \<forall>t\<in>set (tcb' # tcbs). tcb_at' t s; distinct (tcb' # tcbs); ctcb_ptr_to_tcb_ptr qprev' \<notin> set (tcb' # tcbs); tcbp \<in> set (tcb' # tcbs); mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcb2; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; tcb' \<noteq> tcbp\<rbrakk> \<Longrightarrow> tcb' \<noteq> tcbp
 5. \<lbrakk>tn tcb2 \<noteq> tcb_ptr_to_ctcb_ptr tcbp; tcb_queue_relation tn tp mp (tcb' # tcbs) qprev' qhead'; \<forall>t\<in>set (tcb' # tcbs). tcb_at' t s; distinct (tcb' # tcbs); ctcb_ptr_to_tcb_ptr qprev' \<notin> set (tcb' # tcbs); tcbp \<in> set (tcb' # tcbs); mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcb2; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; tcb' \<noteq> tcbp\<rbrakk> \<Longrightarrow> tn tcb2 \<noteq> tcb_ptr_to_ctcb_ptr tcbp proof (prove)
goal (4 subgoals):
 1. \<lbrakk>tn tcb2 \<noteq> tcb_ptr_to_ctcb_ptr tcbp; tcb_queue_relation tn tp mp (tcb' # tcbs) qprev' qhead'; \<forall>t\<in>set (tcb' # tcbs). tcb_at' t s; distinct (tcb' # tcbs); ctcb_ptr_to_tcb_ptr qprev' \<notin> set (tcb' # tcbs); tcbp \<in> set (tcb' # tcbs); mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcb2; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; tcb' \<noteq> tcbp\<rbrakk> \<Longrightarrow> tcbp \<in> set (tcb' # tcbs)
 2. \<lbrakk>tn tcb2 \<noteq> tcb_ptr_to_ctcb_ptr tcbp; tcb_queue_relation tn tp mp (tcb' # tcbs) qprev' qhead'; \<forall>t\<in>set (tcb' # tcbs). tcb_at' t s; distinct (tcb' # tcbs); ctcb_ptr_to_tcb_ptr qprev' \<notin> set (tcb' # tcbs); tcbp \<in> set (tcb' # tcbs); mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcb2; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; tcb' \<noteq> tcbp\<rbrakk> \<Longrightarrow> ctcb_ptr_to_tcb_ptr qprev' \<notin> set (tcb' # tcbs)
 3. \<lbrakk>tn tcb2 \<noteq> tcb_ptr_to_ctcb_ptr tcbp; tcb_queue_relation tn tp mp (tcb' # tcbs) qprev' qhead'; \<forall>t\<in>set (tcb' # tcbs). tcb_at' t s; distinct (tcb' # tcbs); ctcb_ptr_to_tcb_ptr qprev' \<notin> set (tcb' # tcbs); tcbp \<in> set (tcb' # tcbs); mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcb2; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; tcb' \<noteq> tcbp\<rbrakk> \<Longrightarrow> tcb' \<noteq> tcbp
 4. \<lbrakk>tn tcb2 \<noteq> tcb_ptr_to_ctcb_ptr tcbp; tcb_queue_relation tn tp mp (tcb' # tcbs) qprev' qhead'; \<forall>t\<in>set (tcb' # tcbs). tcb_at' t s; distinct (tcb' # tcbs); ctcb_ptr_to_tcb_ptr qprev' \<notin> set (tcb' # tcbs); tcbp \<in> set (tcb' # tcbs); mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcb2; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; tcb' \<noteq> tcbp\<rbrakk> \<Longrightarrow> tn tcb2 \<noteq> tcb_ptr_to_ctcb_ptr tcbp proof (prove)
goal (3 subgoals):
 1. \<lbrakk>tn tcb2 \<noteq> tcb_ptr_to_ctcb_ptr tcbp; tcb_queue_relation tn tp mp (tcb' # tcbs) qprev' qhead'; \<forall>t\<in>set (tcb' # tcbs). tcb_at' t s; distinct (tcb' # tcbs); ctcb_ptr_to_tcb_ptr qprev' \<notin> set (tcb' # tcbs); tcbp \<in> set (tcb' # tcbs); mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcb2; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; tcb' \<noteq> tcbp\<rbrakk> \<Longrightarrow> ctcb_ptr_to_tcb_ptr qprev' \<notin> set (tcb' # tcbs)
 2. \<lbrakk>tn tcb2 \<noteq> tcb_ptr_to_ctcb_ptr tcbp; tcb_queue_relation tn tp mp (tcb' # tcbs) qprev' qhead'; \<forall>t\<in>set (tcb' # tcbs). tcb_at' t s; distinct (tcb' # tcbs); ctcb_ptr_to_tcb_ptr qprev' \<notin> set (tcb' # tcbs); tcbp \<in> set (tcb' # tcbs); mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcb2; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; tcb' \<noteq> tcbp\<rbrakk> \<Longrightarrow> tcb' \<noteq> tcbp
 3. \<lbrakk>tn tcb2 \<noteq> tcb_ptr_to_ctcb_ptr tcbp; tcb_queue_relation tn tp mp (tcb' # tcbs) qprev' qhead'; \<forall>t\<in>set (tcb' # tcbs). tcb_at' t s; distinct (tcb' # tcbs); ctcb_ptr_to_tcb_ptr qprev' \<notin> set (tcb' # tcbs); tcbp \<in> set (tcb' # tcbs); mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcb2; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; tcb' \<noteq> tcbp\<rbrakk> \<Longrightarrow> tn tcb2 \<noteq> tcb_ptr_to_ctcb_ptr tcbp proof (prove)
goal (2 subgoals):
 1. \<lbrakk>tn tcb2 \<noteq> tcb_ptr_to_ctcb_ptr tcbp; tcb_queue_relation tn tp mp (tcb' # tcbs) qprev' qhead'; \<forall>t\<in>set (tcb' # tcbs). tcb_at' t s; distinct (tcb' # tcbs); ctcb_ptr_to_tcb_ptr qprev' \<notin> set (tcb' # tcbs); tcbp \<in> set (tcb' # tcbs); mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcb2; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; tcb' \<noteq> tcbp\<rbrakk> \<Longrightarrow> tcb' \<noteq> tcbp
 2. \<lbrakk>tn tcb2 \<noteq> tcb_ptr_to_ctcb_ptr tcbp; tcb_queue_relation tn tp mp (tcb' # tcbs) qprev' qhead'; \<forall>t\<in>set (tcb' # tcbs). tcb_at' t s; distinct (tcb' # tcbs); ctcb_ptr_to_tcb_ptr qprev' \<notin> set (tcb' # tcbs); tcbp \<in> set (tcb' # tcbs); mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcb2; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; tcb' \<noteq> tcbp\<rbrakk> \<Longrightarrow> tn tcb2 \<noteq> tcb_ptr_to_ctcb_ptr tcbp proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tn tcb2 \<noteq> tcb_ptr_to_ctcb_ptr tcbp; tcb_queue_relation tn tp mp (tcb' # tcbs) qprev' qhead'; \<forall>t\<in>set (tcb' # tcbs). tcb_at' t s; distinct (tcb' # tcbs); ctcb_ptr_to_tcb_ptr qprev' \<notin> set (tcb' # tcbs); tcbp \<in> set (tcb' # tcbs); mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcb2; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; tcb' \<noteq> tcbp\<rbrakk> \<Longrightarrow> tn tcb2 \<noteq> tcb_ptr_to_ctcb_ptr tcbp proof (prove)
goal:
No subgoals! proof (state)
this:
tp tcb \<noteq> tcb_ptr_to_ctcb_ptr tcb'

goal (1 subgoal):
 1. \<lbrakk>tcbp \<noteq> tcb'; tn tcb2 \<noteq> tcb_ptr_to_ctcb_ptr tcbp\<rbrakk> \<Longrightarrow> tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp (tcb' # tcbs)) (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tp tcb else qprev') (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tn tcb else qhead') proof (prove)
using this:
tp tcb \<noteq> tcb_ptr_to_ctcb_ptr tcb'

goal (1 subgoal):
 1. upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp) (tcb_ptr_to_ctcb_ptr tcb') = Some tcb2 proof (prove)
using this:
tp tcb \<noteq> tcb_ptr_to_ctcb_ptr tcb'
tn tcb \<noteq> tcb_ptr_to_ctcb_ptr tcb'
tcb_ptr_to_ctcb_ptr tcb' \<noteq> NULL
mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcb2

goal (1 subgoal):
 1. upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp) (tcb_ptr_to_ctcb_ptr tcb') = Some tcb2 proof (prove)
using this:
tp tcb \<noteq> tcb_ptr_to_ctcb_ptr tcb'
tn tcb \<noteq> tcb_ptr_to_ctcb_ptr tcb'
tcb_ptr_to_ctcb_ptr tcb' \<noteq> NULL
mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcb2

goal (1 subgoal):
 1. (if tn tcb = NULL then if tp tcb = NULL then mp else mp(tp tcb \<mapsto> tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) else (if tp tcb = NULL then mp else mp(tp tcb \<mapsto> tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))))(tn tcb \<mapsto> tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb))))) (tcb_ptr_to_ctcb_ptr tcb') = Some tcb2 proof (state)
this:
upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp) (tcb_ptr_to_ctcb_ptr tcb') = Some tcb2

goal (1 subgoal):
 1. \<lbrakk>tcbp \<noteq> tcb'; tn tcb2 \<noteq> tcb_ptr_to_ctcb_ptr tcbp\<rbrakk> \<Longrightarrow> tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp (tcb' # tcbs)) (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tp tcb else qprev') (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tn tcb else qhead') proof (prove)
using this:
upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp) (tcb_ptr_to_ctcb_ptr tcb') = Some tcb2

goal (1 subgoal):
 1. tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp (tcb' # tcbs)) (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tp tcb else qprev') (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tn tcb else qhead') proof (prove)
using this:
upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp) (tcb_ptr_to_ctcb_ptr tcb') = Some tcb2
tcbp \<noteq> tcb'
mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb
qhead' = tcb_ptr_to_ctcb_ptr tcb'
qprev' = tp tcb2
tn tcb2 \<noteq> tcb_ptr_to_ctcb_ptr tcbp
tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp tcbs) (if tcb_ptr_to_ctcb_ptr tcbp = tn tcb2 then tp tcb else tcb_ptr_to_ctcb_ptr tcb') (if tcb_ptr_to_ctcb_ptr tcbp = tn tcb2 then tn tcb else tn tcb2)
tp tcb \<noteq> tcb_ptr_to_ctcb_ptr tcb'

goal (1 subgoal):
 1. tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp (tcb' # tcbs)) (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tp tcb else qprev') (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tn tcb else qhead') proof (state)
this:
tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp (tcb' # tcbs)) (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tp tcb else qprev') (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tn tcb else qhead')

goal:
No subgoals! proof (state)
this:
tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp (tcb' # tcbs)) (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tp tcb else qprev') (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tn tcb else qhead')

goal:
No subgoals! proof (state)
this:
tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp (tcb' # tcbs)) (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tp tcb else qprev') (if tcb_ptr_to_ctcb_ptr tcbp = qhead' then tn tcb else qhead')

goal:
No subgoals!