309     \<forall> p. e \<noteq> Exit p; 

   309     \<forall> p. e \<noteq> Exit p; 

   310     \<forall> p fd. e \<noteq> CloseFd p fd;

   310     \<forall> p fd. e \<noteq> CloseFd p fd;

   311     \<forall> p f. e \<noteq> UnLink p f;

   311     \<forall> p f. e \<noteq> UnLink p f;

   312     \<forall> p d. e \<noteq> Rmdir p d;

   312     \<forall> p d. e \<noteq> Rmdir p d;

   313     \<forall> p d inum. e \<noteq> Mkdir p d inum;

   313     \<forall> p d inum. e \<noteq> Mkdir p d inum;

   315     \<forall> p q. e \<noteq> CreateMsgq p q;

   314     \<forall> p q. e \<noteq> CreateMsgq p q;

   316     \<forall> p q m. e \<noteq> SendMsg p q m;

   315     \<forall> p q m. e \<noteq> SendMsg p q m;

   317     \<forall> p q m. e \<noteq> RecvMsg p q m;

   316     \<forall> p q m. e \<noteq> RecvMsg p q m;

   318     \<forall> p q. e \<noteq> RemoveMsgq p q;

   317     \<forall> p q. e \<noteq> RemoveMsgq p q;

   319     \<forall> p af st fd inum. e \<noteq> CreateSock p af st fd inum;

   318     \<forall> p af st fd inum. e \<noteq> CreateSock p af st fd inum;