603 lemma sec_kill: 

   604   "valid (Kill p p' # s) \<Longrightarrow> sectxt_of_obj (Kill p p' # s) = sectxt_of_obj s"

   605 by (auto dest!:sec_others)

   606 

   607 lemma sec_ptrace:

   608   "valid (Ptrace p p' # s) \<Longrightarrow> sectxt_of_obj (Ptrace p p' # s) = sectxt_of_obj s"

   609 by (auto dest!:sec_others)

   610 

   611 lemma sec_exit:

   612   "valid (Exit p # s) \<Longrightarrow> sectxt_of_obj (Exit p # s) = sectxt_of_obj s"

   613 by (auto dest!:sec_others)

   614 

   615 lemma sec_readfile:

   616   "valid (ReadFile p fd # s) \<Longrightarrow> sectxt_of_obj (ReadFile p fd # s) = sectxt_of_obj s"

   617 by (auto dest!:sec_others)

   618 

   619 lemma sec_writefile:

   620   "valid (WriteFile p fd # s) \<Longrightarrow> sectxt_of_obj (WriteFile p fd # s) = sectxt_of_obj s"

   621 by (auto dest!:sec_others)

   622 

   623 lemma sec_closefd:

   624   "valid (CloseFd p fd # s) \<Longrightarrow> sectxt_of_obj (CloseFd p fd # s) = sectxt_of_obj s"

   625 by (auto dest!:sec_others)

   626 

   627 lemma sec_unlink:

   628   "valid (UnLink p f # s) \<Longrightarrow> sectxt_of_obj (UnLink p f # s) = sectxt_of_obj s"

   629 by (auto dest!:sec_others)

   630 

   631 lemma sec_Rmdir:

   632   "valid (Rmdir p f # s) \<Longrightarrow> sectxt_of_obj (Rmdir p f # s) = sectxt_of_obj s"

   633 by (auto dest!:sec_others)

   634 

   635 lemma sec_truncate:

   636   "valid (Truncate p f len # s) \<Longrightarrow> sectxt_of_obj (Truncate p f len # s) = sectxt_of_obj s"

   637 by (auto dest!:sec_others)

   638 

   639 lemma sec_recvmsg:

   640   "valid (RecvMsg p q m # s) \<Longrightarrow> sectxt_of_obj (RecvMsg p q m # s) = sectxt_of_obj s"

   641 by (auto dest!:sec_others)

   642 

   643 lemma sec_removemsgq:

   644   "valid (RemoveMsgq p q # s) \<Longrightarrow> sectxt_of_obj (RemoveMsgq p q # s) = sectxt_of_obj s"

   645 by (auto dest!:sec_others)

   646 

   647 lemma sec_attach:

   648   "valid (Attach p h flag # s) \<Longrightarrow> sectxt_of_obj (Attach p h flag # s) = sectxt_of_obj s"

   649 by (auto dest!:sec_others)

   650 

   651 lemma sec_detach:

   652   "valid (Detach p h # s) \<Longrightarrow> sectxt_of_obj (Detach p h # s) = sectxt_of_obj s"

   653 by (auto dest!:sec_others)

   654 

   655 lemma sec_deleteshm:

   656   "valid (DeleteShM p h # s) \<Longrightarrow> sectxt_of_obj (DeleteShM p h # s) = sectxt_of_obj s"

   657 by (auto dest!:sec_others)

   658 

   659 lemma sec_bind:

   660   "valid (Bind p fd addr # s) \<Longrightarrow> sectxt_of_obj (Bind p fd addr # s) = sectxt_of_obj s"

   661 by (auto dest!:sec_others)

   662 

   663 lemma sec_connect:

   664   "valid (Connect p fd addr # s) \<Longrightarrow> sectxt_of_obj (Connect p fd addr # s) = sectxt_of_obj s"

   665 by (auto dest!:sec_others)

   666 

   667 lemma sec_listen:

   668   "valid (Listen p fd # s) \<Longrightarrow> sectxt_of_obj (Listen p fd # s) = sectxt_of_obj s"

   669 by (auto dest!:sec_others)

   670 

   671 lemma sec_sendsock:

   672   "valid (SendSock p fd # s) \<Longrightarrow> sectxt_of_obj (SendSock p fd # s) = sectxt_of_obj s"

   673 by (auto dest!:sec_others)

   674 

   675 lemma sec_recvsock:

   676   "valid (RecvSock p fd # s) \<Longrightarrow> sectxt_of_obj (RecvSock p fd # s) = sectxt_of_obj s"

   677 by (auto dest!:sec_others)

   678 

   679 lemma sec_shutdown:

   680   "valid (Shutdown p fd how # s) \<Longrightarrow> sectxt_of_obj (Shutdown p fd how # s) = sectxt_of_obj s"

   681 by (auto dest!:sec_others)

   682