[STATEMENT]
lemma recvOFriend_eqButUID:
assumes "step s a = (ou, s')"
and "reach s"
and "a = COMact (comReceiveCreateOFriend AID cp UID uID') \<or> a = COMact (comReceiveDeleteOFriend AID cp UID uID')"
and "uID' \<notin> UIDs AID'"
shows "eqButUID s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqButUID s s'
[PROOF STEP]
using assms reach_distinct_friends_reqs(4)
[PROOF STATE]
proof (prove)
using this:
step s a = (ou, s')
reach s
a = COMact (comReceiveCreateOFriend AID cp UID uID') \<or> a = COMact (comReceiveDeleteOFriend AID cp UID uID')
uID' \<notin> UIDs AID'
reach ?s \<Longrightarrow> distinct (recvOuterFriendIDs ?s ?uid)

goal (1 subgoal):
 1. eqButUID s s'
[PROOF STEP]
unfolding eqButUID_def eqButUIDf_def
[PROOF STATE]
proof (prove)
using this:
step s a = (ou, s')
reach s
a = COMact (comReceiveCreateOFriend AID cp UID uID') \<or> a = COMact (comReceiveDeleteOFriend AID cp UID uID')
uID' \<notin> UIDs AID'
reach ?s \<Longrightarrow> distinct (recvOuterFriendIDs ?s ?uid)

goal (1 subgoal):
 1. admin s = admin s' \<and> pendingUReqs s = pendingUReqs s' \<and> userReq s = userReq s' \<and> userIDs s = userIDs s' \<and> user s = user s' \<and> pass s = pass s' \<and> pendingFReqs s = pendingFReqs s' \<and> friendReq s = friendReq s' \<and> friendIDs s = friendIDs s' \<and> postIDs s = postIDs s' \<and> admin s = admin s' \<and> post s = post s' \<and> vis s = vis s' \<and> owner s = owner s' \<and> pendingSApiReqs s = pendingSApiReqs s' \<and> sApiReq s = sApiReq s' \<and> serverApiIDs s = serverApiIDs s' \<and> serverPass s = serverPass s' \<and> outerPostIDs s = outerPostIDs s' \<and> outerPost s = outerPost s' \<and> outerVis s = outerVis s' \<and> outerOwner s = outerOwner s' \<and> sentOuterFriendIDs s = sentOuterFriendIDs s' \<and> (\<forall>uid. if uid \<in> UIDs AID' then recvOuterFriendIDs s uid = recvOuterFriendIDs s' uid else eqButUIDl (recvOuterFriendIDs s uid) (recvOuterFriendIDs s' uid)) \<and> pendingCApiReqs s = pendingCApiReqs s' \<and> cApiReq s = cApiReq s' \<and> clientApiIDs s = clientApiIDs s' \<and> clientPass s = clientPass s' \<and> sharedWith s = sharedWith s'
[PROOF STEP]
by (auto simp: com_defs remove1_idem remove1_append)