theory CSpace_I

lemma getObject_cte_det:
  "(r::cte,s') \<in> fst (getObject p s) \<Longrightarrow> fst (getObject p s) = {(r,s)} \<and> s' = s" apply (clarsimp simp add: getObject_def bind_def get_def gets_def
                            return_def loadObject_cte split_def) apply (clarsimp split: kernel_object.split_asm if_split_asm option.split_asm
                   simp: in_monad typeError_def alignError_def magnitudeCheck_def) apply (simp_all add: bind_def return_def assert_opt_def split_def
                            alignCheck_def is_aligned_mask[symmetric]
                            unless_def when_def magnitudeCheck_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (r, s') \<in> fst (getObject p s) \<Longrightarrow> fst (getObject p s) = {(r, s)} \<and> s' = s proof (prove)
goal (1 subgoal):
 1. \<And>a b ba. \<lbrakk>((a, b), ba) \<in> fst (assert_opt (fst (lookupAround2 p (ksPSpace s))) s); (r, s') \<in> fst ((case b of KOTCB tcb \<Rightarrow> do alignCheck (fst (fst ((a, b), ba))) (objBits tcb);
magnitudeCheck (fst (fst ((a, b), ba))) (snd (fst (lookupAround2 p (fst (ksPSpace s, s)), snd (ksPSpace s, s)))) (objBits tcb);
if p - fst (fst ((a, b), ba)) = tcbVTableSlot << objBits undefined then \<lambda>s. ({(tcbVTable tcb, s)}, False) else if p - fst (fst ((a, b), ba)) = tcbCTableSlot << objBits undefined then \<lambda>s. ({(tcbCTable tcb, s)}, False) else if p - fst (fst ((a, b), ba)) = tcbReplySlot << objBits undefined then \<lambda>s. ({(tcbReply tcb, s)}, False) else if p - fst (fst ((a, b), ba)) = tcbCallerSlot << objBits undefined then \<lambda>s. ({(tcbCaller tcb, s)}, False) else if p - fst (fst ((a, b), ba)) = tcbIPCBufferSlot << objBits undefined then \<lambda>s. ({(tcbIPCBufferFrame tcb, s)}, False) else fail
od | KOCTE cte \<Rightarrow> do unless (p = fst (fst ((a, b), ba))) $ haskell_fail [];
alignCheck p (objBits cte);
magnitudeCheck p (snd (fst (lookupAround2 p (fst (ksPSpace s, s)), snd (ksPSpace s, s)))) (objBits cte);
return cte
od | _ \<Rightarrow> typeError [] (snd (fst ((a, b), ba)))) ba)\<rbrakk> \<Longrightarrow> (\<Union>x\<in>fst (assert_opt (fst (lookupAround2 p (ksPSpace s))) s). fst ((case snd (fst x) of KOTCB tcb \<Rightarrow> do alignCheck (fst (fst x)) (objBits tcb);
magnitudeCheck (fst (fst x)) (snd (fst (lookupAround2 p (fst (ksPSpace s, s)), snd (ksPSpace s, s)))) (objBits tcb);
if p - fst (fst x) = tcbVTableSlot << objBits undefined then \<lambda>s. ({(tcbVTable tcb, s)}, False) else if p - fst (fst x) = tcbCTableSlot << objBits undefined then \<lambda>s. ({(tcbCTable tcb, s)}, False) else if p - fst (fst x) = tcbReplySlot << objBits undefined then \<lambda>s. ({(tcbReply tcb, s)}, False) else if p - fst (fst x) = tcbCallerSlot << objBits undefined then \<lambda>s. ({(tcbCaller tcb, s)}, False) else if p - fst (fst x) = tcbIPCBufferSlot << objBits undefined then \<lambda>s. ({(tcbIPCBufferFrame tcb, s)}, False) else fail
od | KOCTE cte \<Rightarrow> do unless (p = fst (fst x)) $ haskell_fail [];
alignCheck p (objBits cte);
magnitudeCheck p (snd (fst (lookupAround2 p (fst (ksPSpace s, s)), snd (ksPSpace s, s)))) (objBits cte);
return cte
od | _ \<Rightarrow> typeError [] (snd (fst x))) (snd x))) = {(r, s)} \<and> s' = s proof (prove)
goal (12 subgoals):
 1. \<And>a x6. \<lbrakk>fst (lookupAround2 p (ksPSpace s)) = Some (a, KOTCB x6); p - a = tcbVTableSlot << objBits undefined; snd (lookupAround2 p (ksPSpace s)) = None; is_aligned a (objBits x6); s' = s; r = tcbVTable x6\<rbrakk> \<Longrightarrow> (\<Union>x\<in>fst (return (a, KOTCB x6) s). fst ((case snd (fst x) of KOTCB tcb \<Rightarrow> do alignCheck (fst (fst x)) (objBits tcb);
magnitudeCheck (fst (fst x)) (snd (fst (lookupAround2 p (fst (ksPSpace s, s)), snd (ksPSpace s, s)))) (objBits tcb);
if p - fst (fst x) = tcbVTableSlot << objBits undefined then \<lambda>s. ({(tcbVTable tcb, s)}, False) else if p - fst (fst x) = tcbCTableSlot << objBits undefined then \<lambda>s. ({(tcbCTable tcb, s)}, False) else if p - fst (fst x) = tcbReplySlot << objBits undefined then \<lambda>s. ({(tcbReply tcb, s)}, False) else if p - fst (fst x) = tcbCallerSlot << objBits undefined then \<lambda>s. ({(tcbCaller tcb, s)}, False) else if p - fst (fst x) = tcbIPCBufferSlot << objBits undefined then \<lambda>s. ({(tcbIPCBufferFrame tcb, s)}, False) else fail
od | KOCTE cte \<Rightarrow> do unless (p = fst (fst x)) $ haskell_fail [];
alignCheck p (objBits cte);
magnitudeCheck p (snd (fst (lookupAround2 p (fst (ksPSpace s, s)), snd (ksPSpace s, s)))) (objBits cte);
return cte
od | _ \<Rightarrow> typeError [] (snd (fst x))) (snd x))) = {(tcbVTable x6, s)}
 2. \<And>a x6 x2. \<lbrakk>fst (lookupAround2 p (ksPSpace s)) = Some (a, KOTCB x6); p - a = tcbVTableSlot << objBits undefined; snd (lookupAround2 p (ksPSpace s)) = Some x2; is_aligned a (objBits x6); \<not> x2 - a < 2 ^ objBits x6; r = tcbVTable x6; s' = s\<rbrakk> \<Longrightarrow> (\<Union>x\<in>fst (return (a, KOTCB x6) s). fst ((case snd (fst x) of KOTCB tcb \<Rightarrow> do alignCheck (fst (fst x)) (objBits tcb);
magnitudeCheck (fst (fst x)) (snd (fst (lookupAround2 p (fst (ksPSpace s, s)), snd (ksPSpace s, s)))) (objBits tcb);
if p - fst (fst x) = tcbVTableSlot << objBits undefined then \<lambda>s. ({(tcbVTable tcb, s)}, False) else if p - fst (fst x) = tcbCTableSlot << objBits undefined then \<lambda>s. ({(tcbCTable tcb, s)}, False) else if p - fst (fst x) = tcbReplySlot << objBits undefined then \<lambda>s. ({(tcbReply tcb, s)}, False) else if p - fst (fst x) = tcbCallerSlot << objBits undefined then \<lambda>s. ({(tcbCaller tcb, s)}, False) else if p - fst (fst x) = tcbIPCBufferSlot << objBits undefined then \<lambda>s. ({(tcbIPCBufferFrame tcb, s)}, False) else fail
od | KOCTE cte \<Rightarrow> do unless (p = fst (fst x)) $ haskell_fail [];
alignCheck p (objBits cte);
magnitudeCheck p (snd (fst (lookupAround2 p (fst (ksPSpace s, s)), snd (ksPSpace s, s)))) (objBits cte);
return cte
od | _ \<Rightarrow> typeError [] (snd (fst x))) (snd x))) = {(tcbVTable x6, s)}
 3. \<And>a x6. \<lbrakk>fst (lookupAround2 p (ksPSpace s)) = Some (a, KOTCB x6); tcbCTableSlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined; p - a = tcbCTableSlot << objBits undefined; snd (lookupAround2 p (ksPSpace s)) = None; is_aligned a (objBits x6); s' = s; r = tcbCTable x6\<rbrakk> \<Longrightarrow> (\<Union>x\<in>fst (return (a, KOTCB x6) s). fst ((case snd (fst x) of KOTCB tcb \<Rightarrow> do alignCheck (fst (fst x)) (objBits tcb);
magnitudeCheck (fst (fst x)) (snd (fst (lookupAround2 p (fst (ksPSpace s, s)), snd (ksPSpace s, s)))) (objBits tcb);
if p - fst (fst x) = tcbVTableSlot << objBits undefined then \<lambda>s. ({(tcbVTable tcb, s)}, False) else if p - fst (fst x) = tcbCTableSlot << objBits undefined then \<lambda>s. ({(tcbCTable tcb, s)}, False) else if p - fst (fst x) = tcbReplySlot << objBits undefined then \<lambda>s. ({(tcbReply tcb, s)}, False) else if p - fst (fst x) = tcbCallerSlot << objBits undefined then \<lambda>s. ({(tcbCaller tcb, s)}, False) else if p - fst (fst x) = tcbIPCBufferSlot << objBits undefined then \<lambda>s. ({(tcbIPCBufferFrame tcb, s)}, False) else fail
od | KOCTE cte \<Rightarrow> do unless (p = fst (fst x)) $ haskell_fail [];
alignCheck p (objBits cte);
magnitudeCheck p (snd (fst (lookupAround2 p (fst (ksPSpace s, s)), snd (ksPSpace s, s)))) (objBits cte);
return cte
od | _ \<Rightarrow> typeError [] (snd (fst x))) (snd x))) = {(tcbCTable x6, s)}
 4. \<And>a x6 x2. \<lbrakk>fst (lookupAround2 p (ksPSpace s)) = Some (a, KOTCB x6); tcbCTableSlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined; p - a = tcbCTableSlot << objBits undefined; snd (lookupAround2 p (ksPSpace s)) = Some x2; is_aligned a (objBits x6); \<not> x2 - a < 2 ^ objBits x6; r = tcbCTable x6; s' = s\<rbrakk> \<Longrightarrow> (\<Union>x\<in>fst (return (a, KOTCB x6) s). fst ((case snd (fst x) of KOTCB tcb \<Rightarrow> do alignCheck (fst (fst x)) (objBits tcb);
magnitudeCheck (fst (fst x)) (snd (fst (lookupAround2 p (fst (ksPSpace s, s)), snd (ksPSpace s, s)))) (objBits tcb);
if p - fst (fst x) = tcbVTableSlot << objBits undefined then \<lambda>s. ({(tcbVTable tcb, s)}, False) else if p - fst (fst x) = tcbCTableSlot << objBits undefined then \<lambda>s. ({(tcbCTable tcb, s)}, False) else if p - fst (fst x) = tcbReplySlot << objBits undefined then \<lambda>s. ({(tcbReply tcb, s)}, False) else if p - fst (fst x) = tcbCallerSlot << objBits undefined then \<lambda>s. ({(tcbCaller tcb, s)}, False) else if p - fst (fst x) = tcbIPCBufferSlot << objBits undefined then \<lambda>s. ({(tcbIPCBufferFrame tcb, s)}, False) else fail
od | KOCTE cte \<Rightarrow> do unless (p = fst (fst x)) $ haskell_fail [];
alignCheck p (objBits cte);
magnitudeCheck p (snd (fst (lookupAround2 p (fst (ksPSpace s, s)), snd (ksPSpace s, s)))) (objBits cte);
return cte
od | _ \<Rightarrow> typeError [] (snd (fst x))) (snd x))) = {(tcbCTable x6, s)}
 5. \<And>a x6. \<lbrakk>fst (lookupAround2 p (ksPSpace s)) = Some (a, KOTCB x6); tcbReplySlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined; tcbReplySlot << objBits undefined \<noteq> tcbCTableSlot << objBits undefined; p - a = tcbReplySlot << objBits undefined; snd (lookupAround2 p (ksPSpace s)) = None; is_aligned a (objBits x6); s' = s; r = tcbReply x6\<rbrakk> \<Longrightarrow> (\<Union>x\<in>fst (return (a, KOTCB x6) s). fst ((case snd (fst x) of KOTCB tcb \<Rightarrow> do alignCheck (fst (fst x)) (objBits tcb);
magnitudeCheck (fst (fst x)) (snd (fst (lookupAround2 p (fst (ksPSpace s, s)), snd (ksPSpace s, s)))) (objBits tcb);
if p - fst (fst x) = tcbVTableSlot << objBits undefined then \<lambda>s. ({(tcbVTable tcb, s)}, False) else if p - fst (fst x) = tcbCTableSlot << objBits undefined then \<lambda>s. ({(tcbCTable tcb, s)}, False) else if p - fst (fst x) = tcbReplySlot << objBits undefined then \<lambda>s. ({(tcbReply tcb, s)}, False) else if p - fst (fst x) = tcbCallerSlot << objBits undefined then \<lambda>s. ({(tcbCaller tcb, s)}, False) else if p - fst (fst x) = tcbIPCBufferSlot << objBits undefined then \<lambda>s. ({(tcbIPCBufferFrame tcb, s)}, False) else fail
od | KOCTE cte \<Rightarrow> do unless (p = fst (fst x)) $ haskell_fail [];
alignCheck p (objBits cte);
magnitudeCheck p (snd (fst (lookupAround2 p (fst (ksPSpace s, s)), snd (ksPSpace s, s)))) (objBits cte);
return cte
od | _ \<Rightarrow> typeError [] (snd (fst x))) (snd x))) = {(tcbReply x6, s)}
 6. \<And>a x6 x2. \<lbrakk>fst (lookupAround2 p (ksPSpace s)) = Some (a, KOTCB x6); tcbReplySlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined; tcbReplySlot << objBits undefined \<noteq> tcbCTableSlot << objBits undefined; p - a = tcbReplySlot << objBits undefined; snd (lookupAround2 p (ksPSpace s)) = Some x2; is_aligned a (objBits x6); \<not> x2 - a < 2 ^ objBits x6; r = tcbReply x6; s' = s\<rbrakk> \<Longrightarrow> (\<Union>x\<in>fst (return (a, KOTCB x6) s). fst ((case snd (fst x) of KOTCB tcb \<Rightarrow> do alignCheck (fst (fst x)) (objBits tcb);
magnitudeCheck (fst (fst x)) (snd (fst (lookupAround2 p (fst (ksPSpace s, s)), snd (ksPSpace s, s)))) (objBits tcb);
if p - fst (fst x) = tcbVTableSlot << objBits undefined then \<lambda>s. ({(tcbVTable tcb, s)}, False) else if p - fst (fst x) = tcbCTableSlot << objBits undefined then \<lambda>s. ({(tcbCTable tcb, s)}, False) else if p - fst (fst x) = tcbReplySlot << objBits undefined then \<lambda>s. ({(tcbReply tcb, s)}, False) else if p - fst (fst x) = tcbCallerSlot << objBits undefined then \<lambda>s. ({(tcbCaller tcb, s)}, False) else if p - fst (fst x) = tcbIPCBufferSlot << objBits undefined then \<lambda>s. ({(tcbIPCBufferFrame tcb, s)}, False) else fail
od | KOCTE cte \<Rightarrow> do unless (p = fst (fst x)) $ haskell_fail [];
alignCheck p (objBits cte);
magnitudeCheck p (snd (fst (lookupAround2 p (fst (ksPSpace s, s)), snd (ksPSpace s, s)))) (objBits cte);
return cte
od | _ \<Rightarrow> typeError [] (snd (fst x))) (snd x))) = {(tcbReply x6, s)}
 7. \<And>a x6. \<lbrakk>fst (lookupAround2 p (ksPSpace s)) = Some (a, KOTCB x6); tcbCallerSlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined; tcbCallerSlot << objBits undefined \<noteq> tcbCTableSlot << objBits undefined; tcbCallerSlot << objBits undefined \<noteq> tcbReplySlot << objBits undefined; p - a = tcbCallerSlot << objBits undefined; snd (lookupAround2 p (ksPSpace s)) = None; is_aligned a (objBits x6); s' = s; r = tcbCaller x6\<rbrakk> \<Longrightarrow> (\<Union>x\<in>fst (return (a, KOTCB x6) s). fst ((case snd (fst x) of KOTCB tcb \<Rightarrow> do alignCheck (fst (fst x)) (objBits tcb);
magnitudeCheck (fst (fst x)) (snd (fst (lookupAround2 p (fst (ksPSpace s, s)), snd (ksPSpace s, s)))) (objBits tcb);
if p - fst (fst x) = tcbVTableSlot << objBits undefined then \<lambda>s. ({(tcbVTable tcb, s)}, False) else if p - fst (fst x) = tcbCTableSlot << objBits undefined then \<lambda>s. ({(tcbCTable tcb, s)}, False) else if p - fst (fst x) = tcbReplySlot << objBits undefined then \<lambda>s. ({(tcbReply tcb, s)}, False) else if p - fst (fst x) = tcbCallerSlot << objBits undefined then \<lambda>s. ({(tcbCaller tcb, s)}, False) else if p - fst (fst x) = tcbIPCBufferSlot << objBits undefined then \<lambda>s. ({(tcbIPCBufferFrame tcb, s)}, False) else fail
od | KOCTE cte \<Rightarrow> do unless (p = fst (fst x)) $ haskell_fail [];
alignCheck p (objBits cte);
magnitudeCheck p (snd (fst (lookupAround2 p (fst (ksPSpace s, s)), snd (ksPSpace s, s)))) (objBits cte);
return cte
od | _ \<Rightarrow> typeError [] (snd (fst x))) (snd x))) = {(tcbCaller x6, s)}
 8. \<And>a x6 x2. \<lbrakk>fst (lookupAround2 p (ksPSpace s)) = Some (a, KOTCB x6); tcbCallerSlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined; tcbCallerSlot << objBits undefined \<noteq> tcbCTableSlot << objBits undefined; tcbCallerSlot << objBits undefined \<noteq> tcbReplySlot << objBits undefined; p - a = tcbCallerSlot << objBits undefined; snd (lookupAround2 p (ksPSpace s)) = Some x2; is_aligned a (objBits x6); \<not> x2 - a < 2 ^ objBits x6; r = tcbCaller x6; s' = s\<rbrakk> \<Longrightarrow> (\<Union>x\<in>fst (return (a, KOTCB x6) s). fst ((case snd (fst x) of KOTCB tcb \<Rightarrow> do alignCheck (fst (fst x)) (objBits tcb);
magnitudeCheck (fst (fst x)) (snd (fst (lookupAround2 p (fst (ksPSpace s, s)), snd (ksPSpace s, s)))) (objBits tcb);
if p - fst (fst x) = tcbVTableSlot << objBits undefined then \<lambda>s. ({(tcbVTable tcb, s)}, False) else if p - fst (fst x) = tcbCTableSlot << objBits undefined then \<lambda>s. ({(tcbCTable tcb, s)}, False) else if p - fst (fst x) = tcbReplySlot << objBits undefined then \<lambda>s. ({(tcbReply tcb, s)}, False) else if p - fst (fst x) = tcbCallerSlot << objBits undefined then \<lambda>s. ({(tcbCaller tcb, s)}, False) else if p - fst (fst x) = tcbIPCBufferSlot << objBits undefined then \<lambda>s. ({(tcbIPCBufferFrame tcb, s)}, False) else fail
od | KOCTE cte \<Rightarrow> do unless (p = fst (fst x)) $ haskell_fail [];
alignCheck p (objBits cte);
magnitudeCheck p (snd (fst (lookupAround2 p (fst (ksPSpace s, s)), snd (ksPSpace s, s)))) (objBits cte);
return cte
od | _ \<Rightarrow> typeError [] (snd (fst x))) (snd x))) = {(tcbCaller x6, s)}
 9. \<And>a x6. \<lbrakk>fst (lookupAround2 p (ksPSpace s)) = Some (a, KOTCB x6); tcbIPCBufferSlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined; tcbIPCBufferSlot << objBits undefined \<noteq> tcbCTableSlot << objBits undefined; tcbIPCBufferSlot << objBits undefined \<noteq> tcbReplySlot << objBits undefined; tcbIPCBufferSlot << objBits undefined \<noteq> tcbCallerSlot << objBits undefined; p - a = tcbIPCBufferSlot << objBits undefined; snd (lookupAround2 p (ksPSpace s)) = None; is_aligned a (objBits x6); s' = s; r = tcbIPCBufferFrame x6\<rbrakk> \<Longrightarrow> (\<Union>x\<in>fst (return (a, KOTCB x6) s). fst ((case snd (fst x) of KOTCB tcb \<Rightarrow> do alignCheck (fst (fst x)) (objBits tcb);
magnitudeCheck (fst (fst x)) (snd (fst (lookupAround2 p (fst (ksPSpace s, s)), snd (ksPSpace s, s)))) (objBits tcb);
if p - fst (fst x) = tcbVTableSlot << objBits undefined then \<lambda>s. ({(tcbVTable tcb, s)}, False) else if p - fst (fst x) = tcbCTableSlot << objBits undefined then \<lambda>s. ({(tcbCTable tcb, s)}, False) else if p - fst (fst x) = tcbReplySlot << objBits undefined then \<lambda>s. ({(tcbReply tcb, s)}, False) else if p - fst (fst x) = tcbCallerSlot << objBits undefined then \<lambda>s. ({(tcbCaller tcb, s)}, False) else if p - fst (fst x) = tcbIPCBufferSlot << objBits undefined then \<lambda>s. ({(tcbIPCBufferFrame tcb, s)}, False) else fail
od | KOCTE cte \<Rightarrow> do unless (p = fst (fst x)) $ haskell_fail [];
alignCheck p (objBits cte);
magnitudeCheck p (snd (fst (lookupAround2 p (fst (ksPSpace s, s)), snd (ksPSpace s, s)))) (objBits cte);
return cte
od | _ \<Rightarrow> typeError [] (snd (fst x))) (snd x))) = {(tcbIPCBufferFrame x6, s)}
 10. \<And>a x6 x2. \<lbrakk>fst (lookupAround2 p (ksPSpace s)) = Some (a, KOTCB x6); tcbIPCBufferSlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined; tcbIPCBufferSlot << objBits undefined \<noteq> tcbCTableSlot << objBits undefined; tcbIPCBufferSlot << objBits undefined \<noteq> tcbReplySlot << objBits undefined; tcbIPCBufferSlot << objBits undefined \<noteq> tcbCallerSlot << objBits undefined; p - a = tcbIPCBufferSlot << objBits undefined; snd (lookupAround2 p (ksPSpace s)) = Some x2; is_aligned a (objBits x6); \<not> x2 - a < 2 ^ objBits x6; r = tcbIPCBufferFrame x6; s' = s\<rbrakk> \<Longrightarrow> (\<Union>x\<in>fst (return (a, KOTCB x6) s). fst ((case snd (fst x) of KOTCB tcb \<Rightarrow> do alignCheck (fst (fst x)) (objBits tcb);
magnitudeCheck (fst (fst x)) (snd (fst (lookupAround2 p (fst (ksPSpace s, s)), snd (ksPSpace s, s)))) (objBits tcb);
if p - fst (fst x) = tcbVTableSlot << objBits undefined then \<lambda>s. ({(tcbVTable tcb, s)}, False) else if p - fst (fst x) = tcbCTableSlot << objBits undefined then \<lambda>s. ({(tcbCTable tcb, s)}, False) else if p - fst (fst x) = tcbReplySlot << objBits undefined then \<lambda>s. ({(tcbReply tcb, s)}, False) else if p - fst (fst x) = tcbCallerSlot << objBits undefined then \<lambda>s. ({(tcbCaller tcb, s)}, False) else if p - fst (fst x) = tcbIPCBufferSlot << objBits undefined then \<lambda>s. ({(tcbIPCBufferFrame tcb, s)}, False) else fail
od | KOCTE cte \<Rightarrow> do unless (p = fst (fst x)) $ haskell_fail [];
alignCheck p (objBits cte);
magnitudeCheck p (snd (fst (lookupAround2 p (fst (ksPSpace s, s)), snd (ksPSpace s, s)))) (objBits cte);
return cte
od | _ \<Rightarrow> typeError [] (snd (fst x))) (snd x))) = {(tcbIPCBufferFrame x6, s)}
A total of 12 subgoals... proof (prove)
goal:
No subgoals!