[STATEMENT]
lemma eqButUID_step_\<gamma>_out:
assumes ss1: "eqButUID s s1"
and step: "step s a = (ou,s')" and step1: "step s1 a = (ou1,s1')"
(*and sT: "reachNT s" and s1: "reachNT s1"*)
and \<gamma>: "\<gamma> (Trans s a ou s')"
and os1: "\<not>open s1"
and \<phi>: "\<phi> (Trans s1 a ou1 s1') \<longleftrightarrow> \<phi> (Trans s a ou s')"
shows "ou = ou1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ou = ou1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ou = ou1
[PROOF STEP]
obtain uid sa com_act where uid_a: "(userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID)
                                      \<or> a = COMact com_act \<or> a = Sact sa"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>uid com_act sa. userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<gamma> UID_UIDs
[PROOF STATE]
proof (prove)
using this:
\<gamma> (Trans s a ou s')
UID \<notin> UIDs AID

goal (1 subgoal):
 1. (\<And>uid com_act sa. userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa

goal (1 subgoal):
 1. ou = ou1
[PROOF STEP]
note simps = eqButUID_not_UID eqButUID_stateSelectors r_defs s_defs c_defs com_defs l_defs u_defs d_defs
[PROOF STATE]
proof (state)
this:
\<lbrakk>eqButUID ?s ?s1.0; ?uid \<noteq> UID\<rbrakk> \<Longrightarrow> sentOuterFriendIDs ?s ?uid = sentOuterFriendIDs ?s1.0 ?uid
eqButUID ?s ?s1.0 \<Longrightarrow> admin ?s = admin ?s1.0
eqButUID ?s ?s1.0 \<Longrightarrow> pendingUReqs ?s = pendingUReqs ?s1.0
eqButUID ?s ?s1.0 \<Longrightarrow> userReq ?s = userReq ?s1.0
eqButUID ?s ?s1.0 \<Longrightarrow> userIDs ?s = userIDs ?s1.0
eqButUID ?s ?s1.0 \<Longrightarrow> user ?s = user ?s1.0
eqButUID ?s ?s1.0 \<Longrightarrow> pass ?s = pass ?s1.0
eqButUID ?s ?s1.0 \<Longrightarrow> pendingFReqs ?s = pendingFReqs ?s1.0
eqButUID ?s ?s1.0 \<Longrightarrow> friendReq ?s = friendReq ?s1.0
eqButUID ?s ?s1.0 \<Longrightarrow> friendIDs ?s = friendIDs ?s1.0
eqButUID ?s ?s1.0 \<Longrightarrow> postIDs ?s = postIDs ?s1.0
eqButUID ?s ?s1.0 \<Longrightarrow> post ?s = post ?s1.0
eqButUID ?s ?s1.0 \<Longrightarrow> vis ?s = vis ?s1.0
eqButUID ?s ?s1.0 \<Longrightarrow> owner ?s = owner ?s1.0
eqButUID ?s ?s1.0 \<Longrightarrow> pendingSApiReqs ?s = pendingSApiReqs ?s1.0
eqButUID ?s ?s1.0 \<Longrightarrow> sApiReq ?s = sApiReq ?s1.0
eqButUID ?s ?s1.0 \<Longrightarrow> serverApiIDs ?s = serverApiIDs ?s1.0
eqButUID ?s ?s1.0 \<Longrightarrow> serverPass ?s = serverPass ?s1.0
eqButUID ?s ?s1.0 \<Longrightarrow> outerPostIDs ?s = outerPostIDs ?s1.0
eqButUID ?s ?s1.0 \<Longrightarrow> outerPost ?s = outerPost ?s1.0
eqButUID ?s ?s1.0 \<Longrightarrow> outerVis ?s = outerVis ?s1.0
eqButUID ?s ?s1.0 \<Longrightarrow> outerOwner ?s = outerOwner ?s1.0
eqButUID ?s ?s1.0 \<Longrightarrow> eqButUIDf (sentOuterFriendIDs ?s) (sentOuterFriendIDs ?s1.0)
eqButUID ?s ?s1.0 \<Longrightarrow> recvOuterFriendIDs ?s = recvOuterFriendIDs ?s1.0
eqButUID ?s ?s1.0 \<Longrightarrow> pendingCApiReqs ?s = pendingCApiReqs ?s1.0
eqButUID ?s ?s1.0 \<Longrightarrow> cApiReq ?s = cApiReq ?s1.0
eqButUID ?s ?s1.0 \<Longrightarrow> clientApiIDs ?s = clientApiIDs ?s1.0
eqButUID ?s ?s1.0 \<Longrightarrow> clientPass ?s = clientPass ?s1.0
eqButUID ?s ?s1.0 \<Longrightarrow> sharedWith ?s = sharedWith ?s1.0
eqButUID ?s ?s1.0 \<Longrightarrow> IDsOK ?s = IDsOK ?s1.0
readNUReq ?s ?uID ?p ?uID' \<equiv> userReq ?s ?uID'
e_readNUReq ?s ?uID ?p ?uID' \<equiv> IDsOK ?s [?uID] [] [] [] \<and> pass ?s ?uID = ?p \<and> ?uID = admin ?s \<and> ?uID' \<in>\<in> pendingUReqs ?s
readUser ?s ?uID ?p ?uID' \<equiv> nameUser (user ?s ?uID')
e_readUser ?s ?uID ?p ?uID' \<equiv> IDsOK ?s [?uID, ?uID'] [] [] [] \<and> pass ?s ?uID = ?p
readAmIAdmin ?s ?uID ?p \<equiv> ?uID = admin ?s
e_readAmIAdmin ?s ?uID ?p \<equiv> IDsOK ?s [?uID] [] [] [] \<and> pass ?s ?uID = ?p
readPost ?s ?uID ?p ?pID \<equiv> post ?s ?pID
e_readPost ?s ?uID ?p ?pID \<equiv> IDsOK ?s [?uID] [?pID] [] [] \<and> pass ?s ?uID = ?p \<and> (owner ?s ?pID = ?uID \<or> ?uID \<in>\<in> friendIDs ?s (owner ?s ?pID) \<or> vis ?s ?pID = PublicV)
readOwnerPost ?s ?uID ?p ?pID \<equiv> owner ?s ?pID
e_readOwnerPost ?s ?uID ?p ?pID \<equiv> IDsOK ?s [?uID] [?pID] [] [] \<and> pass ?s ?uID = ?p \<and> (admin ?s = ?uID \<or> owner ?s ?pID = ?uID \<or> ?uID \<in>\<in> friendIDs ?s (owner ?s ?pID) \<or> vis ?s ?pID = PublicV)
readVisPost ?s ?uID ?p ?pID \<equiv> vis ?s ?pID
e_readVisPost ?s ?uID ?p ?pID \<equiv> IDsOK ?s [?uID] [?pID] [] [] \<and> pass ?s ?uID = ?p \<and> (admin ?s = ?uID \<or> owner ?s ?pID = ?uID \<or> ?uID \<in>\<in> friendIDs ?s (owner ?s ?pID) \<or> vis ?s ?pID = PublicV)
readOPost ?s ?uID ?p ?aID ?pID \<equiv> outerPost ?s ?aID ?pID
e_readOPost ?s ?uID ?p ?aID ?pID \<equiv> IDsOK ?s [?uID] [] [(?aID, [?pID])] [] \<and> pass ?s ?uID = ?p \<and> (admin ?s = ?uID \<or> (?aID, outerOwner ?s ?aID ?pID) \<in>\<in> recvOuterFriendIDs ?s ?uID \<or> outerVis ?s ?aID ?pID = PublicV)
readOwnerOPost ?s ?uID ?p ?aID ?pID \<equiv> outerOwner ?s ?aID ?pID
e_readOwnerOPost ?s ?uID ?p ?aID ?pID \<equiv> IDsOK ?s [?uID] [] [(?aID, [?pID])] [] \<and> pass ?s ?uID = ?p \<and> (admin ?s = ?uID \<or> (?aID, outerOwner ?s ?aID ?pID) \<in>\<in> recvOuterFriendIDs ?s ?uID \<or> outerVis ?s ?aID ?pID = PublicV)
readVisOPost ?s ?uID ?p ?aID ?pID \<equiv> outerVis ?s ?aID ?pID
e_readVisOPost ?s ?uID ?p ?aID ?pID \<equiv> let post = outerPost ?s ?aID ?pID in IDsOK ?s [?uID] [] [(?aID, [?pID])] [] \<and> pass ?s ?uID = ?p \<and> (admin ?s = ?uID \<or> (?aID, outerOwner ?s ?aID ?pID) \<in>\<in> recvOuterFriendIDs ?s ?uID \<or> outerVis ?s ?aID ?pID = PublicV)
readFriendReqToMe ?s ?uID ?p ?uID' \<equiv> friendReq ?s ?uID' ?uID
e_readFriendReqToMe ?s ?uID ?p ?uID' \<equiv> IDsOK ?s [?uID, ?uID'] [] [] [] \<and> pass ?s ?uID = ?p \<and> ?uID' \<in>\<in> pendingFReqs ?s ?uID
readFriendReqFromMe ?s ?uID ?p ?uID' \<equiv> friendReq ?s ?uID ?uID'
e_readFriendReqFromMe ?s ?uID ?p ?uID' \<equiv> IDsOK ?s [?uID, ?uID'] [] [] [] \<and> pass ?s ?uID = ?p \<and> ?uID \<in>\<in> pendingFReqs ?s ?uID'
readSApiReq ?s ?uID ?p ?uID' \<equiv> sApiReq ?s ?uID'
e_readSApiReq ?s ?uID ?p ?uID' \<equiv> IDsOK ?s [?uID] [] [] [] \<and> pass ?s ?uID = ?p \<and> ?uID = admin ?s \<and> ?uID' \<in>\<in> pendingSApiReqs ?s
readCApiReq ?s ?uID ?p ?uID' \<equiv> cApiReq ?s ?uID'
e_readCApiReq ?s ?uID ?p ?uID' \<equiv> IDsOK ?s [?uID] [] [] [] \<and> pass ?s ?uID = ?p \<and> ?uID = admin ?s \<and> ?uID' \<in>\<in> pendingCApiReqs ?s
e_startSys ?s ?uID ?p \<equiv> userIDs ?s = []
startSys ?s ?uID ?p \<equiv> ?s\<lparr>admin := ?uID, userIDs := [?uID], user := (user ?s)(?uID := emptyUser), pass := (pass ?s)(?uID := ?p)\<rparr>
e_createNUReq ?s ?uID ?requestInfo \<equiv> admin ?s \<in>\<in> userIDs ?s \<and> ?uID \<notin> set (userIDs ?s) \<and> ?uID \<notin> set (pendingUReqs ?s)
createNUReq ?s ?uID ?reqInfo \<equiv> ?s\<lparr>pendingUReqs := pendingUReqs ?s ## ?uID, userReq := (userReq ?s)(?uID := ?reqInfo)\<rparr>
e_createUser ?s ?uID ?p ?uID' ?p' \<equiv> IDsOK ?s [?uID] [] [] [] \<and> pass ?s ?uID = ?p \<and> ?uID = admin ?s \<and> ?uID' \<in>\<in> pendingUReqs ?s
createUser ?s ?uID ?p ?uID' ?p' \<equiv> ?s\<lparr>userIDs := ?uID' # userIDs ?s, user := (user ?s)(?uID' := emptyUser), pass := (pass ?s)(?uID' := ?p'), pendingUReqs := remove1 ?uID' (pendingUReqs ?s), userReq := (userReq ?s)(?uID := emptyRequestInfo)\<rparr>
e_createPost ?s ?uID ?p ?pID \<equiv> IDsOK ?s [?uID] [] [] [] \<and> pass ?s ?uID = ?p \<and> ?pID \<notin> set (postIDs ?s)
createPost ?s ?uID ?p ?pID \<equiv> ?s\<lparr>postIDs := ?pID # postIDs ?s, post := (post ?s)(?pID := emptyPost), owner := (owner ?s)(?pID := ?uID)\<rparr>
e_createFriendReq ?s ?uID ?p ?uID' ?req \<equiv> IDsOK ?s [?uID, ?uID'] [] [] [] \<and> pass ?s ?uID = ?p \<and> ?uID \<notin> set (pendingFReqs ?s ?uID') \<and> ?uID \<notin> set (friendIDs ?s ?uID')
createFriendReq ?s ?uID ?p ?uID' ?req \<equiv> let pfr = pendingFReqs ?s in ?s\<lparr>pendingFReqs := pfr(?uID' := pfr ?uID' ## ?uID), friendReq := fun_upd2 (friendReq ?s) ?uID ?uID' ?req\<rparr>
e_createFriend ?s ?uID ?p ?uID' \<equiv> IDsOK ?s [?uID, ?uID'] [] [] [] \<and> pass ?s ?uID = ?p \<and> ?uID' \<in>\<in> pendingFReqs ?s ?uID
createFriend ?s ?uID ?p ?uID' \<equiv> let fr = friendIDs ?s; pfr = pendingFReqs ?s in ?s\<lparr>friendIDs := fr(?uID := fr ?uID ## ?uID', ?uID' := fr ?uID' ## ?uID), pendingFReqs := pfr(?uID := remove1 ?uID' (pfr ?uID), ?uID' := remove1 ?uID (pfr ?uID')), friendReq := fun_upd2 (fun_upd2 (friendReq ?s) ?uID' ?uID emptyRequestInfo) ?uID ?uID' emptyRequestInfo\<rparr>
sendServerReq ?s ?uID ?p ?aID ?reqInfo \<equiv> ((?aID, ?reqInfo), ?s\<lparr>pendingSApiReqs := pendingSApiReqs ?s ## ?aID, sApiReq := (sApiReq ?s)(?aID := ?reqInfo)\<rparr>)
e_sendServerReq ?s ?uID ?p ?aID ?reqInfo \<equiv> IDsOK ?s [?uID] [] [] [] \<and> pass ?s ?uID = ?p \<and> ?uID = admin ?s \<and> ?aID \<notin> set (pendingSApiReqs ?s)
receiveClientReq ?s ?aID ?reqInfo \<equiv> ?s\<lparr>pendingCApiReqs := pendingCApiReqs ?s ## ?aID, cApiReq := (cApiReq ?s)(?aID := ?reqInfo)\<rparr>
e_receiveClientReq ?s ?aID ?reqInfo \<equiv> ?aID \<notin> set (pendingCApiReqs ?s) \<and> admin ?s \<in>\<in> userIDs ?s
connectClient ?s ?uID ?p ?aID ?cp \<equiv> ((?aID, ?cp), ?s\<lparr>clientApiIDs := ?aID # clientApiIDs ?s, clientPass := (clientPass ?s)(?aID := ?cp), pendingCApiReqs := remove1 ?aID (pendingCApiReqs ?s), cApiReq := (cApiReq ?s)(?aID := emptyRequestInfo)\<rparr>)
e_connectClient ?s ?uID ?p ?aID ?cp \<equiv> IDsOK ?s [?uID] [] [] [] \<and> pass ?s ?uID = ?p \<and> ?uID = admin ?s \<and> ?aID \<in>\<in> pendingCApiReqs ?s \<and> ?aID \<notin> set (clientApiIDs ?s)
connectServer ?s ?aID ?sp \<equiv> ?s\<lparr>serverApiIDs := ?aID # serverApiIDs ?s, serverPass := (serverPass ?s)(?aID := ?sp), pendingSApiReqs := remove1 ?aID (pendingSApiReqs ?s), sApiReq := (sApiReq ?s)(?aID := emptyRequestInfo)\<rparr>
e_connectServer ?s ?aID ?sp \<equiv> ?aID \<in>\<in> pendingSApiReqs ?s \<and> ?aID \<notin> set (serverApiIDs ?s)
receivePost ?s ?aID ?sp ?pID ?pst ?uID ?vs \<equiv> let opIDs = outerPostIDs ?s in ?s\<lparr>outerPostIDs := opIDs(?aID := List.insert ?pID (opIDs ?aID)), outerPost := fun_upd2 (outerPost ?s) ?aID ?pID ?pst, outerOwner := fun_upd2 (outerOwner ?s) ?aID ?pID ?uID, outerVis := fun_upd2 (outerVis ?s) ?aID ?pID ?vs\<rparr>
e_receivePost ?s ?aID ?sp ?pID ?nt ?uID ?vs \<equiv> IDsOK ?s [] [] [(?aID, [])] [] \<and> serverPass ?s ?aID = ?sp
sendPost ?s ?uID ?p ?aID ?pID \<equiv> ((?aID, clientPass ?s ?aID, ?pID, post ?s ?pID, owner ?s ?pID, vis ?s ?pID), ?s\<lparr>sharedWith := (sharedWith ?s)(?pID := insert2 ?aID True (sharedWith ?s ?pID))\<rparr>)
e_sendPost ?s ?uID ?p ?aID ?pID \<equiv> IDsOK ?s [?uID] [?pID] [] [?aID] \<and> pass ?s ?uID = ?p \<and> ?uID = admin ?s \<and> ?aID \<in>\<in> clientApiIDs ?s
receiveCreateOFriend ?s ?saID ?sp ?uID ?uID' \<equiv> let ofr = recvOuterFriendIDs ?s in ?s\<lparr>recvOuterFriendIDs := ofr(?uID' := ofr ?uID' ## (?saID, ?uID))\<rparr>
e_receiveCreateOFriend ?s ?saID ?sp ?uID ?uID' \<equiv> IDsOK ?s [] [] [(?saID, [])] [] \<and> serverPass ?s ?saID = ?sp \<and> (?saID, ?uID) \<notin> set (recvOuterFriendIDs ?s ?uID')
sendCreateOFriend ?s ?uID ?p ?aID ?uID' \<equiv> let ofr = sentOuterFriendIDs ?s in ((?aID, clientPass ?s ?aID, ?uID, ?uID'), ?s\<lparr>sentOuterFriendIDs := ofr(?uID := ofr ?uID ## (?aID, ?uID'))\<rparr>)
e_sendCreateOFriend ?s ?uID ?p ?caID ?uID' \<equiv> IDsOK ?s [?uID] [] [] [?caID] \<and> pass ?s ?uID = ?p \<and> (?caID, ?uID') \<notin> set (sentOuterFriendIDs ?s ?uID)
receiveDeleteOFriend ?s ?saID ?sp ?uID ?uID' \<equiv> let ofr = recvOuterFriendIDs ?s in ?s\<lparr>recvOuterFriendIDs := ofr(?uID' := remove1 (?saID, ?uID) (ofr ?uID'))\<rparr>
e_receiveDeleteOFriend ?s ?saID ?sp ?uID ?uID' \<equiv> IDsOK ?s [] [] [(?saID, [])] [] \<and> serverPass ?s ?saID = ?sp \<and> (?saID, ?uID) \<in>\<in> recvOuterFriendIDs ?s ?uID'
sendDeleteOFriend ?s ?uID ?p ?aID ?uID' \<equiv> let ofr = sentOuterFriendIDs ?s in ((?aID, clientPass ?s ?aID, ?uID, ?uID'), ?s\<lparr>sentOuterFriendIDs := ofr(?uID := remove1 (?aID, ?uID') (ofr ?uID))\<rparr>)
e_sendDeleteOFriend ?s ?uID ?p ?caID ?uID' \<equiv> IDsOK ?s [?uID] [] [] [?caID] \<and> pass ?s ?uID = ?p \<and> (?caID, ?uID') \<in>\<in> sentOuterFriendIDs ?s ?uID
listPendingUReqs ?s ?uID ?p \<equiv> pendingUReqs ?s
e_listPendingUReqs ?s ?uID ?p \<equiv> IDsOK ?s [?uID] [] [] [] \<and> pass ?s ?uID = ?p \<and> ?uID = admin ?s
listAllUsers ?s ?uID ?p \<equiv> userIDs ?s
e_listAllUsers ?s ?uID ?p \<equiv> IDsOK ?s [?uID] [] [] [] \<and> pass ?s ?uID = ?p
listFriends ?s ?uID ?p ?uID' \<equiv> friendIDs ?s ?uID'
e_listFriends ?s ?uID ?p ?uID' \<equiv> IDsOK ?s [?uID, ?uID'] [] [] [] \<and> pass ?s ?uID = ?p \<and> (?uID = ?uID' \<or> ?uID \<in>\<in> friendIDs ?s ?uID')
listSentOuterFriends ?s ?uID ?p ?uID' \<equiv> sentOuterFriendIDs ?s ?uID'
e_listSentOuterFriends ?s ?uID ?p ?uID' \<equiv> IDsOK ?s [?uID, ?uID'] [] [] [] \<and> pass ?s ?uID = ?p \<and> (?uID = ?uID' \<or> ?uID \<in>\<in> friendIDs ?s ?uID')
listRecvOuterFriends ?s ?uID ?p \<equiv> recvOuterFriendIDs ?s ?uID
e_listRecvOuterFriends ?s ?uID ?p \<equiv> IDsOK ?s [?uID] [] [] [] \<and> pass ?s ?uID = ?p
listInnerPosts ?s ?uID ?p \<equiv> cmap (\<lambda>pID. if vis ?s pID \<noteq> FriendV \<or> ?uID \<in>\<in> friendIDs ?s (owner ?s pID) \<or> ?uID = owner ?s pID then [(owner ?s pID, pID)] else []) (postIDs ?s)
e_listInnerPosts ?s ?uID ?p \<equiv> IDsOK ?s [?uID] [] [] [] \<and> pass ?s ?uID = ?p
listOuterPosts ?s ?uID ?p \<equiv> cmap (\<lambda>saID. cmap (\<lambda>pID. if outerVis ?s saID pID = PublicV \<or> (saID, outerOwner ?s saID pID) \<in>\<in> recvOuterFriendIDs ?s ?uID then [(saID, pID)] else []) (outerPostIDs ?s saID)) (serverApiIDs ?s)
e_listOuterPosts ?s ?uID ?p \<equiv> IDsOK ?s [?uID] [] [] [] \<and> pass ?s ?uID = ?p
listClientsPost ?s ?uID ?p ?pID \<equiv> sharedWith ?s ?pID
e_listClientsPost ?s ?uID ?p ?pID \<equiv> IDsOK ?s [?uID] [?pID] [] [] \<and> pass ?s ?uID = ?p \<and> ?uID = admin ?s
listPendingSApiReqs ?s ?uID ?p \<equiv> pendingSApiReqs ?s
e_listPendingSApiReqs ?s ?uID ?p \<equiv> IDsOK ?s [?uID] [] [] [] \<and> pass ?s ?uID = ?p \<and> ?uID = admin ?s
listServerAPIs ?s ?uID ?p \<equiv> serverApiIDs ?s
e_listServerAPIs ?s ?uID ?p \<equiv> IDsOK ?s [?uID] [] [] [] \<and> pass ?s ?uID = ?p \<and> ?uID = admin ?s
listPendingCApiReqs ?s ?uID ?p \<equiv> pendingCApiReqs ?s
e_listPendingCApiReqs ?s ?uID ?p \<equiv> IDsOK ?s [?uID] [] [] [] \<and> pass ?s ?uID = ?p \<and> ?uID = admin ?s
listClientAPIs ?s ?uID ?p \<equiv> clientApiIDs ?s
e_listClientAPIs ?s ?uID ?p \<equiv> IDsOK ?s [?uID] [] [] [] \<and> pass ?s ?uID = ?p \<and> ?uID = admin ?s
e_updateUser ?s ?uID ?p ?p' ?name ?info \<equiv> IDsOK ?s [?uID] [] [] [] \<and> pass ?s ?uID = ?p
updateUser ?s ?uID ?p ?p' ?name ?info \<equiv> ?s\<lparr>user := (user ?s)(?uID := Usr ?name ?info), pass := (pass ?s)(?uID := ?p')\<rparr>
e_updatePost ?s ?uID ?p ?pID ?pst \<equiv> IDsOK ?s [?uID] [?pID] [] [] \<and> pass ?s ?uID = ?p \<and> owner ?s ?pID = ?uID
updatePost ?s ?uID ?p ?pID ?pst \<equiv> let sW = sharedWith ?s in ?s\<lparr>post := (post ?s)(?pID := ?pst), sharedWith := sW(?pID := map (\<lambda>(aID, uu_). (aID, False)) (sW ?pID))\<rparr>
e_updateVisPost ?s ?uID ?p ?pID ?vs \<equiv> IDsOK ?s [?uID] [?pID] [] [] \<and> pass ?s ?uID = ?p \<and> owner ?s ?pID = ?uID \<and> ?vs \<in> {FriendV, PublicV}
updateVisPost ?s ?uID ?p ?pID ?vs \<equiv> ?s\<lparr>vis := (vis ?s)(?pID := ?vs)\<rparr>
e_deleteFriend ?s ?uID ?p ?uID' \<equiv> IDsOK ?s [?uID, ?uID'] [] [] [] \<and> pass ?s ?uID = ?p \<and> ?uID' \<in>\<in> friendIDs ?s ?uID
deleteFriend ?s ?uID ?p ?uID' \<equiv> let fr = friendIDs ?s in ?s\<lparr>friendIDs := fr(?uID := removeAll ?uID' (fr ?uID), ?uID' := removeAll ?uID (fr ?uID'))\<rparr>

goal (1 subgoal):
 1. ou = ou1
[PROOF STEP]
note facts = ss1 step step1 uid_a
[PROOF STATE]
proof (state)
this:
eqButUID s s1
step s a = (ou, s')
step s1 a = (ou1, s1')
userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa

goal (1 subgoal):
 1. ou = ou1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ou = ou1
[PROOF STEP]
proof (cases a)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>x1. a = Sact x1 \<Longrightarrow> ou = ou1
 2. \<And>x2. a = Cact x2 \<Longrightarrow> ou = ou1
 3. \<And>x3. a = Dact x3 \<Longrightarrow> ou = ou1
 4. \<And>x4. a = Uact x4 \<Longrightarrow> ou = ou1
 5. \<And>x5. a = Ract x5 \<Longrightarrow> ou = ou1
 6. \<And>x6. a = Lact x6 \<Longrightarrow> ou = ou1
 7. \<And>x7. a = COMact x7 \<Longrightarrow> ou = ou1
[PROOF STEP]
case (Ract ra)
[PROOF STATE]
proof (state)
this:
a = Ract ra

goal (7 subgoals):
 1. \<And>x1. a = Sact x1 \<Longrightarrow> ou = ou1
 2. \<And>x2. a = Cact x2 \<Longrightarrow> ou = ou1
 3. \<And>x3. a = Dact x3 \<Longrightarrow> ou = ou1
 4. \<And>x4. a = Uact x4 \<Longrightarrow> ou = ou1
 5. \<And>x5. a = Ract x5 \<Longrightarrow> ou = ou1
 6. \<And>x6. a = Lact x6 \<Longrightarrow> ou = ou1
 7. \<And>x7. a = COMact x7 \<Longrightarrow> ou = ou1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a = Ract ra
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a = Ract ra

goal (1 subgoal):
 1. ou = ou1
[PROOF STEP]
using facts
[PROOF STATE]
proof (prove)
using this:
a = Ract ra
eqButUID s s1
step s a = (ou, s')
step s1 a = (ou1, s1')
userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa

goal (1 subgoal):
 1. ou = ou1
[PROOF STEP]
by (cases ra) (auto simp add: simps)
[PROOF STATE]
proof (state)
this:
ou = ou1

goal (6 subgoals):
 1. \<And>x1. a = Sact x1 \<Longrightarrow> ou = ou1
 2. \<And>x2. a = Cact x2 \<Longrightarrow> ou = ou1
 3. \<And>x3. a = Dact x3 \<Longrightarrow> ou = ou1
 4. \<And>x4. a = Uact x4 \<Longrightarrow> ou = ou1
 5. \<And>x6. a = Lact x6 \<Longrightarrow> ou = ou1
 6. \<And>x7. a = COMact x7 \<Longrightarrow> ou = ou1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>x1. a = Sact x1 \<Longrightarrow> ou = ou1
 2. \<And>x2. a = Cact x2 \<Longrightarrow> ou = ou1
 3. \<And>x3. a = Dact x3 \<Longrightarrow> ou = ou1
 4. \<And>x4. a = Uact x4 \<Longrightarrow> ou = ou1
 5. \<And>x6. a = Lact x6 \<Longrightarrow> ou = ou1
 6. \<And>x7. a = COMact x7 \<Longrightarrow> ou = ou1
[PROOF STEP]
case (Sact sa)
[PROOF STATE]
proof (state)
this:
a = Sact sa

goal (6 subgoals):
 1. \<And>x1. a = Sact x1 \<Longrightarrow> ou = ou1
 2. \<And>x2. a = Cact x2 \<Longrightarrow> ou = ou1
 3. \<And>x3. a = Dact x3 \<Longrightarrow> ou = ou1
 4. \<And>x4. a = Uact x4 \<Longrightarrow> ou = ou1
 5. \<And>x6. a = Lact x6 \<Longrightarrow> ou = ou1
 6. \<And>x7. a = COMact x7 \<Longrightarrow> ou = ou1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a = Sact sa
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a = Sact sa

goal (1 subgoal):
 1. ou = ou1
[PROOF STEP]
using facts
[PROOF STATE]
proof (prove)
using this:
a = Sact sa
eqButUID s s1
step s a = (ou, s')
step s1 a = (ou1, s1')
userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa__

goal (1 subgoal):
 1. ou = ou1
[PROOF STEP]
by (cases sa) (auto simp add: simps)
[PROOF STATE]
proof (state)
this:
ou = ou1

goal (5 subgoals):
 1. \<And>x2. a = Cact x2 \<Longrightarrow> ou = ou1
 2. \<And>x3. a = Dact x3 \<Longrightarrow> ou = ou1
 3. \<And>x4. a = Uact x4 \<Longrightarrow> ou = ou1
 4. \<And>x6. a = Lact x6 \<Longrightarrow> ou = ou1
 5. \<And>x7. a = COMact x7 \<Longrightarrow> ou = ou1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>x2. a = Cact x2 \<Longrightarrow> ou = ou1
 2. \<And>x3. a = Dact x3 \<Longrightarrow> ou = ou1
 3. \<And>x4. a = Uact x4 \<Longrightarrow> ou = ou1
 4. \<And>x6. a = Lact x6 \<Longrightarrow> ou = ou1
 5. \<And>x7. a = COMact x7 \<Longrightarrow> ou = ou1
[PROOF STEP]
case (Cact ca)
[PROOF STATE]
proof (state)
this:
a = Cact ca

goal (5 subgoals):
 1. \<And>x2. a = Cact x2 \<Longrightarrow> ou = ou1
 2. \<And>x3. a = Dact x3 \<Longrightarrow> ou = ou1
 3. \<And>x4. a = Uact x4 \<Longrightarrow> ou = ou1
 4. \<And>x6. a = Lact x6 \<Longrightarrow> ou = ou1
 5. \<And>x7. a = COMact x7 \<Longrightarrow> ou = ou1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a = Cact ca
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a = Cact ca

goal (1 subgoal):
 1. ou = ou1
[PROOF STEP]
using facts
[PROOF STATE]
proof (prove)
using this:
a = Cact ca
eqButUID s s1
step s a = (ou, s')
step s1 a = (ou1, s1')
userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa

goal (1 subgoal):
 1. ou = ou1
[PROOF STEP]
by (cases ca) (auto simp add: simps)
[PROOF STATE]
proof (state)
this:
ou = ou1

goal (4 subgoals):
 1. \<And>x3. a = Dact x3 \<Longrightarrow> ou = ou1
 2. \<And>x4. a = Uact x4 \<Longrightarrow> ou = ou1
 3. \<And>x6. a = Lact x6 \<Longrightarrow> ou = ou1
 4. \<And>x7. a = COMact x7 \<Longrightarrow> ou = ou1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x3. a = Dact x3 \<Longrightarrow> ou = ou1
 2. \<And>x4. a = Uact x4 \<Longrightarrow> ou = ou1
 3. \<And>x6. a = Lact x6 \<Longrightarrow> ou = ou1
 4. \<And>x7. a = COMact x7 \<Longrightarrow> ou = ou1
[PROOF STEP]
case (COMact ca)
[PROOF STATE]
proof (state)
this:
a = COMact ca

goal (4 subgoals):
 1. \<And>x3. a = Dact x3 \<Longrightarrow> ou = ou1
 2. \<And>x4. a = Uact x4 \<Longrightarrow> ou = ou1
 3. \<And>x6. a = Lact x6 \<Longrightarrow> ou = ou1
 4. \<And>x7. a = COMact x7 \<Longrightarrow> ou = ou1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a = COMact ca
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a = COMact ca

goal (1 subgoal):
 1. ou = ou1
[PROOF STEP]
using facts
[PROOF STATE]
proof (prove)
using this:
a = COMact ca
eqButUID s s1
step s a = (ou, s')
step s1 a = (ou1, s1')
userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa

goal (1 subgoal):
 1. ou = ou1
[PROOF STEP]
proof (cases ca)
[PROOF STATE]
proof (state)
goal (10 subgoals):
 1. \<And>x11 x12 x13 x14. \<lbrakk>a = COMact ca; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; ca = comSendServerReq x11 x12 x13 x14\<rbrakk> \<Longrightarrow> ou = ou1
 2. \<And>x21 x22. \<lbrakk>a = COMact ca; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; ca = comReceiveClientReq x21 x22\<rbrakk> \<Longrightarrow> ou = ou1
 3. \<And>x31 x32 x33 x34. \<lbrakk>a = COMact ca; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; ca = comConnectClient x31 x32 x33 x34\<rbrakk> \<Longrightarrow> ou = ou1
 4. \<And>x41 x42. \<lbrakk>a = COMact ca; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; ca = comConnectServer x41 x42\<rbrakk> \<Longrightarrow> ou = ou1
 5. \<And>x51 x52 x53 x54 x55 x56. \<lbrakk>a = COMact ca; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; ca = comReceivePost x51 x52 x53 x54 x55 x56\<rbrakk> \<Longrightarrow> ou = ou1
 6. \<And>x61 x62 x63 x64. \<lbrakk>a = COMact ca; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; ca = comSendPost x61 x62 x63 x64\<rbrakk> \<Longrightarrow> ou = ou1
 7. \<And>x71 x72 x73 x74. \<lbrakk>a = COMact ca; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; ca = comReceiveCreateOFriend x71 x72 x73 x74\<rbrakk> \<Longrightarrow> ou = ou1
 8. \<And>x81 x82 x83 x84. \<lbrakk>a = COMact ca; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; ca = comSendCreateOFriend x81 x82 x83 x84\<rbrakk> \<Longrightarrow> ou = ou1
 9. \<And>x91 x92 x93 x94. \<lbrakk>a = COMact ca; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; ca = comReceiveDeleteOFriend x91 x92 x93 x94\<rbrakk> \<Longrightarrow> ou = ou1
 10. \<And>x101 x102 x103 x104. \<lbrakk>a = COMact ca; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; ca = comSendDeleteOFriend x101 x102 x103 x104\<rbrakk> \<Longrightarrow> ou = ou1
[PROOF STEP]
case (comSendCreateOFriend uID p aID uID')
[PROOF STATE]
proof (state)
this:
ca = comSendCreateOFriend uID p aID uID'

goal (10 subgoals):
 1. \<And>x11 x12 x13 x14. \<lbrakk>a = COMact ca; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; ca = comSendServerReq x11 x12 x13 x14\<rbrakk> \<Longrightarrow> ou = ou1
 2. \<And>x21 x22. \<lbrakk>a = COMact ca; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; ca = comReceiveClientReq x21 x22\<rbrakk> \<Longrightarrow> ou = ou1
 3. \<And>x31 x32 x33 x34. \<lbrakk>a = COMact ca; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; ca = comConnectClient x31 x32 x33 x34\<rbrakk> \<Longrightarrow> ou = ou1
 4. \<And>x41 x42. \<lbrakk>a = COMact ca; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; ca = comConnectServer x41 x42\<rbrakk> \<Longrightarrow> ou = ou1
 5. \<And>x51 x52 x53 x54 x55 x56. \<lbrakk>a = COMact ca; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; ca = comReceivePost x51 x52 x53 x54 x55 x56\<rbrakk> \<Longrightarrow> ou = ou1
 6. \<And>x61 x62 x63 x64. \<lbrakk>a = COMact ca; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; ca = comSendPost x61 x62 x63 x64\<rbrakk> \<Longrightarrow> ou = ou1
 7. \<And>x71 x72 x73 x74. \<lbrakk>a = COMact ca; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; ca = comReceiveCreateOFriend x71 x72 x73 x74\<rbrakk> \<Longrightarrow> ou = ou1
 8. \<And>x81 x82 x83 x84. \<lbrakk>a = COMact ca; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; ca = comSendCreateOFriend x81 x82 x83 x84\<rbrakk> \<Longrightarrow> ou = ou1
 9. \<And>x91 x92 x93 x94. \<lbrakk>a = COMact ca; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; ca = comReceiveDeleteOFriend x91 x92 x93 x94\<rbrakk> \<Longrightarrow> ou = ou1
 10. \<And>x101 x102 x103 x104. \<lbrakk>a = COMact ca; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; ca = comSendDeleteOFriend x101 x102 x103 x104\<rbrakk> \<Longrightarrow> ou = ou1
[PROOF STEP]
with facts \<phi>
[PROOF STATE]
proof (chain)
picking this:
eqButUID s s1
step s a = (ou, s')
step s1 a = (ou1, s1')
userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa
\<phi> (Trans s1 a ou1 s1') = \<phi> (Trans s a ou s')
ca = comSendCreateOFriend uID p aID uID'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eqButUID s s1
step s a = (ou, s')
step s1 a = (ou1, s1')
userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa
\<phi> (Trans s1 a ou1 s1') = \<phi> (Trans s a ou s')
ca = comSendCreateOFriend uID p aID uID'

goal (1 subgoal):
 1. ou = ou1
[PROOF STEP]
using COMact eqButUID_sentOuterFriends_UIDs[OF ss1]
[PROOF STATE]
proof (prove)
using this:
eqButUID s s1
step s a = (ou, s')
step s1 a = (ou1, s1')
userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa
\<phi> (Trans s1 a ou1 s1') = \<phi> (Trans s a ou s')
ca = comSendCreateOFriend uID p aID uID'
a = COMact ca
?uid' \<in> UIDs ?aid \<Longrightarrow> ((?aid, ?uid') \<in>\<in> sentOuterFriendIDs s UID) = ((?aid, ?uid') \<in>\<in> sentOuterFriendIDs s1 UID)

goal (1 subgoal):
 1. ou = ou1
[PROOF STEP]
by (cases "uID = UID") (auto simp: simps)
[PROOF STATE]
proof (state)
this:
ou = ou1

goal (9 subgoals):
 1. \<And>x11 x12 x13 x14. \<lbrakk>a = COMact ca; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; ca = comSendServerReq x11 x12 x13 x14\<rbrakk> \<Longrightarrow> ou = ou1
 2. \<And>x21 x22. \<lbrakk>a = COMact ca; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; ca = comReceiveClientReq x21 x22\<rbrakk> \<Longrightarrow> ou = ou1
 3. \<And>x31 x32 x33 x34. \<lbrakk>a = COMact ca; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; ca = comConnectClient x31 x32 x33 x34\<rbrakk> \<Longrightarrow> ou = ou1
 4. \<And>x41 x42. \<lbrakk>a = COMact ca; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; ca = comConnectServer x41 x42\<rbrakk> \<Longrightarrow> ou = ou1
 5. \<And>x51 x52 x53 x54 x55 x56. \<lbrakk>a = COMact ca; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; ca = comReceivePost x51 x52 x53 x54 x55 x56\<rbrakk> \<Longrightarrow> ou = ou1
 6. \<And>x61 x62 x63 x64. \<lbrakk>a = COMact ca; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; ca = comSendPost x61 x62 x63 x64\<rbrakk> \<Longrightarrow> ou = ou1
 7. \<And>x71 x72 x73 x74. \<lbrakk>a = COMact ca; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; ca = comReceiveCreateOFriend x71 x72 x73 x74\<rbrakk> \<Longrightarrow> ou = ou1
 8. \<And>x91 x92 x93 x94. \<lbrakk>a = COMact ca; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; ca = comReceiveDeleteOFriend x91 x92 x93 x94\<rbrakk> \<Longrightarrow> ou = ou1
 9. \<And>x101 x102 x103 x104. \<lbrakk>a = COMact ca; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; ca = comSendDeleteOFriend x101 x102 x103 x104\<rbrakk> \<Longrightarrow> ou = ou1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. \<And>x11 x12 x13 x14. \<lbrakk>a = COMact ca; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; ca = comSendServerReq x11 x12 x13 x14\<rbrakk> \<Longrightarrow> ou = ou1
 2. \<And>x21 x22. \<lbrakk>a = COMact ca; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; ca = comReceiveClientReq x21 x22\<rbrakk> \<Longrightarrow> ou = ou1
 3. \<And>x31 x32 x33 x34. \<lbrakk>a = COMact ca; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; ca = comConnectClient x31 x32 x33 x34\<rbrakk> \<Longrightarrow> ou = ou1
 4. \<And>x41 x42. \<lbrakk>a = COMact ca; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; ca = comConnectServer x41 x42\<rbrakk> \<Longrightarrow> ou = ou1
 5. \<And>x51 x52 x53 x54 x55 x56. \<lbrakk>a = COMact ca; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; ca = comReceivePost x51 x52 x53 x54 x55 x56\<rbrakk> \<Longrightarrow> ou = ou1
 6. \<And>x61 x62 x63 x64. \<lbrakk>a = COMact ca; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; ca = comSendPost x61 x62 x63 x64\<rbrakk> \<Longrightarrow> ou = ou1
 7. \<And>x71 x72 x73 x74. \<lbrakk>a = COMact ca; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; ca = comReceiveCreateOFriend x71 x72 x73 x74\<rbrakk> \<Longrightarrow> ou = ou1
 8. \<And>x91 x92 x93 x94. \<lbrakk>a = COMact ca; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; ca = comReceiveDeleteOFriend x91 x92 x93 x94\<rbrakk> \<Longrightarrow> ou = ou1
 9. \<And>x101 x102 x103 x104. \<lbrakk>a = COMact ca; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; ca = comSendDeleteOFriend x101 x102 x103 x104\<rbrakk> \<Longrightarrow> ou = ou1
[PROOF STEP]
case (comSendDeleteOFriend uID p aID uID')
[PROOF STATE]
proof (state)
this:
ca = comSendDeleteOFriend uID p aID uID'

goal (9 subgoals):
 1. \<And>x11 x12 x13 x14. \<lbrakk>a = COMact ca; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; ca = comSendServerReq x11 x12 x13 x14\<rbrakk> \<Longrightarrow> ou = ou1
 2. \<And>x21 x22. \<lbrakk>a = COMact ca; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; ca = comReceiveClientReq x21 x22\<rbrakk> \<Longrightarrow> ou = ou1
 3. \<And>x31 x32 x33 x34. \<lbrakk>a = COMact ca; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; ca = comConnectClient x31 x32 x33 x34\<rbrakk> \<Longrightarrow> ou = ou1
 4. \<And>x41 x42. \<lbrakk>a = COMact ca; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; ca = comConnectServer x41 x42\<rbrakk> \<Longrightarrow> ou = ou1
 5. \<And>x51 x52 x53 x54 x55 x56. \<lbrakk>a = COMact ca; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; ca = comReceivePost x51 x52 x53 x54 x55 x56\<rbrakk> \<Longrightarrow> ou = ou1
 6. \<And>x61 x62 x63 x64. \<lbrakk>a = COMact ca; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; ca = comSendPost x61 x62 x63 x64\<rbrakk> \<Longrightarrow> ou = ou1
 7. \<And>x71 x72 x73 x74. \<lbrakk>a = COMact ca; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; ca = comReceiveCreateOFriend x71 x72 x73 x74\<rbrakk> \<Longrightarrow> ou = ou1
 8. \<And>x91 x92 x93 x94. \<lbrakk>a = COMact ca; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; ca = comReceiveDeleteOFriend x91 x92 x93 x94\<rbrakk> \<Longrightarrow> ou = ou1
 9. \<And>x101 x102 x103 x104. \<lbrakk>a = COMact ca; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; ca = comSendDeleteOFriend x101 x102 x103 x104\<rbrakk> \<Longrightarrow> ou = ou1
[PROOF STEP]
with facts \<phi>
[PROOF STATE]
proof (chain)
picking this:
eqButUID s s1
step s a = (ou, s')
step s1 a = (ou1, s1')
userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa
\<phi> (Trans s1 a ou1 s1') = \<phi> (Trans s a ou s')
ca = comSendDeleteOFriend uID p aID uID'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eqButUID s s1
step s a = (ou, s')
step s1 a = (ou1, s1')
userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa
\<phi> (Trans s1 a ou1 s1') = \<phi> (Trans s a ou s')
ca = comSendDeleteOFriend uID p aID uID'

goal (1 subgoal):
 1. ou = ou1
[PROOF STEP]
using COMact eqButUID_sentOuterFriends_UIDs[OF ss1]
[PROOF STATE]
proof (prove)
using this:
eqButUID s s1
step s a = (ou, s')
step s1 a = (ou1, s1')
userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa
\<phi> (Trans s1 a ou1 s1') = \<phi> (Trans s a ou s')
ca = comSendDeleteOFriend uID p aID uID'
a = COMact ca
?uid' \<in> UIDs ?aid \<Longrightarrow> ((?aid, ?uid') \<in>\<in> sentOuterFriendIDs s UID) = ((?aid, ?uid') \<in>\<in> sentOuterFriendIDs s1 UID)

goal (1 subgoal):
 1. ou = ou1
[PROOF STEP]
by (cases "uID = UID") (auto simp: simps)
[PROOF STATE]
proof (state)
this:
ou = ou1

goal (8 subgoals):
 1. \<And>x11 x12 x13 x14. \<lbrakk>a = COMact ca; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; ca = comSendServerReq x11 x12 x13 x14\<rbrakk> \<Longrightarrow> ou = ou1
 2. \<And>x21 x22. \<lbrakk>a = COMact ca; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; ca = comReceiveClientReq x21 x22\<rbrakk> \<Longrightarrow> ou = ou1
 3. \<And>x31 x32 x33 x34. \<lbrakk>a = COMact ca; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; ca = comConnectClient x31 x32 x33 x34\<rbrakk> \<Longrightarrow> ou = ou1
 4. \<And>x41 x42. \<lbrakk>a = COMact ca; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; ca = comConnectServer x41 x42\<rbrakk> \<Longrightarrow> ou = ou1
 5. \<And>x51 x52 x53 x54 x55 x56. \<lbrakk>a = COMact ca; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; ca = comReceivePost x51 x52 x53 x54 x55 x56\<rbrakk> \<Longrightarrow> ou = ou1
 6. \<And>x61 x62 x63 x64. \<lbrakk>a = COMact ca; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; ca = comSendPost x61 x62 x63 x64\<rbrakk> \<Longrightarrow> ou = ou1
 7. \<And>x71 x72 x73 x74. \<lbrakk>a = COMact ca; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; ca = comReceiveCreateOFriend x71 x72 x73 x74\<rbrakk> \<Longrightarrow> ou = ou1
 8. \<And>x91 x92 x93 x94. \<lbrakk>a = COMact ca; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; ca = comReceiveDeleteOFriend x91 x92 x93 x94\<rbrakk> \<Longrightarrow> ou = ou1
[PROOF STEP]
qed (auto simp: simps)
[PROOF STATE]
proof (state)
this:
ou = ou1

goal (3 subgoals):
 1. \<And>x3. a = Dact x3 \<Longrightarrow> ou = ou1
 2. \<And>x4. a = Uact x4 \<Longrightarrow> ou = ou1
 3. \<And>x6. a = Lact x6 \<Longrightarrow> ou = ou1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x3. a = Dact x3 \<Longrightarrow> ou = ou1
 2. \<And>x4. a = Uact x4 \<Longrightarrow> ou = ou1
 3. \<And>x6. a = Lact x6 \<Longrightarrow> ou = ou1
[PROOF STEP]
case (Lact la)
[PROOF STATE]
proof (state)
this:
a = Lact la

goal (3 subgoals):
 1. \<And>x3. a = Dact x3 \<Longrightarrow> ou = ou1
 2. \<And>x4. a = Uact x4 \<Longrightarrow> ou = ou1
 3. \<And>x6. a = Lact x6 \<Longrightarrow> ou = ou1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a = Lact la
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a = Lact la

goal (1 subgoal):
 1. ou = ou1
[PROOF STEP]
using facts
[PROOF STATE]
proof (prove)
using this:
a = Lact la
eqButUID s s1
step s a = (ou, s')
step s1 a = (ou1, s1')
userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa

goal (1 subgoal):
 1. ou = ou1
[PROOF STEP]
proof (cases la)
[PROOF STATE]
proof (state)
goal (12 subgoals):
 1. \<And>x11 x12. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lPendingUReqs x11 x12\<rbrakk> \<Longrightarrow> ou = ou1
 2. \<And>x21 x22. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lAllUsers x21 x22\<rbrakk> \<Longrightarrow> ou = ou1
 3. \<And>x31 x32 x33. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lFriends x31 x32 x33\<rbrakk> \<Longrightarrow> ou = ou1
 4. \<And>x41 x42 x43. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lSentOuterFriends x41 x42 x43\<rbrakk> \<Longrightarrow> ou = ou1
 5. \<And>x51 x52. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lRecvOuterFriends x51 x52\<rbrakk> \<Longrightarrow> ou = ou1
 6. \<And>x61 x62. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lInnerPosts x61 x62\<rbrakk> \<Longrightarrow> ou = ou1
 7. \<And>x71 x72. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lOuterPosts x71 x72\<rbrakk> \<Longrightarrow> ou = ou1
 8. \<And>x81 x82 x83. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lClientsPost x81 x82 x83\<rbrakk> \<Longrightarrow> ou = ou1
 9. \<And>x91 x92. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lPendingSApiReqs x91 x92\<rbrakk> \<Longrightarrow> ou = ou1
 10. \<And>x101 x102. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lServerAPIs x101 x102\<rbrakk> \<Longrightarrow> ou = ou1
A total of 12 subgoals...
[PROOF STEP]
case (lSentOuterFriends uID p uID')
[PROOF STATE]
proof (state)
this:
la = lSentOuterFriends uID p uID'

goal (12 subgoals):
 1. \<And>x11 x12. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lPendingUReqs x11 x12\<rbrakk> \<Longrightarrow> ou = ou1
 2. \<And>x21 x22. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lAllUsers x21 x22\<rbrakk> \<Longrightarrow> ou = ou1
 3. \<And>x31 x32 x33. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lFriends x31 x32 x33\<rbrakk> \<Longrightarrow> ou = ou1
 4. \<And>x41 x42 x43. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lSentOuterFriends x41 x42 x43\<rbrakk> \<Longrightarrow> ou = ou1
 5. \<And>x51 x52. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lRecvOuterFriends x51 x52\<rbrakk> \<Longrightarrow> ou = ou1
 6. \<And>x61 x62. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lInnerPosts x61 x62\<rbrakk> \<Longrightarrow> ou = ou1
 7. \<And>x71 x72. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lOuterPosts x71 x72\<rbrakk> \<Longrightarrow> ou = ou1
 8. \<And>x81 x82 x83. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lClientsPost x81 x82 x83\<rbrakk> \<Longrightarrow> ou = ou1
 9. \<And>x91 x92. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lPendingSApiReqs x91 x92\<rbrakk> \<Longrightarrow> ou = ou1
 10. \<And>x101 x102. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lServerAPIs x101 x102\<rbrakk> \<Longrightarrow> ou = ou1
A total of 12 subgoals...
[PROOF STEP]
with Lact facts os1
[PROOF STATE]
proof (chain)
picking this:
a = Lact la
eqButUID s s1
step s a = (ou, s')
step s1 a = (ou1, s1')
userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa
\<not> open s1
la = lSentOuterFriends uID p uID'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a = Lact la
eqButUID s s1
step s a = (ou, s')
step s1 a = (ou1, s1')
userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa
\<not> open s1
la = lSentOuterFriends uID p uID'

goal (1 subgoal):
 1. ou = ou1
[PROOF STEP]
by (cases "uID' = UID") (auto simp: simps open_def)
[PROOF STATE]
proof (state)
this:
ou = ou1

goal (11 subgoals):
 1. \<And>x11 x12. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lPendingUReqs x11 x12\<rbrakk> \<Longrightarrow> ou = ou1
 2. \<And>x21 x22. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lAllUsers x21 x22\<rbrakk> \<Longrightarrow> ou = ou1
 3. \<And>x31 x32 x33. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lFriends x31 x32 x33\<rbrakk> \<Longrightarrow> ou = ou1
 4. \<And>x51 x52. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lRecvOuterFriends x51 x52\<rbrakk> \<Longrightarrow> ou = ou1
 5. \<And>x61 x62. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lInnerPosts x61 x62\<rbrakk> \<Longrightarrow> ou = ou1
 6. \<And>x71 x72. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lOuterPosts x71 x72\<rbrakk> \<Longrightarrow> ou = ou1
 7. \<And>x81 x82 x83. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lClientsPost x81 x82 x83\<rbrakk> \<Longrightarrow> ou = ou1
 8. \<And>x91 x92. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lPendingSApiReqs x91 x92\<rbrakk> \<Longrightarrow> ou = ou1
 9. \<And>x101 x102. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lServerAPIs x101 x102\<rbrakk> \<Longrightarrow> ou = ou1
 10. \<And>x111 x112. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lPendingCApiReqs x111 x112\<rbrakk> \<Longrightarrow> ou = ou1
A total of 11 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (11 subgoals):
 1. \<And>x11 x12. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lPendingUReqs x11 x12\<rbrakk> \<Longrightarrow> ou = ou1
 2. \<And>x21 x22. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lAllUsers x21 x22\<rbrakk> \<Longrightarrow> ou = ou1
 3. \<And>x31 x32 x33. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lFriends x31 x32 x33\<rbrakk> \<Longrightarrow> ou = ou1
 4. \<And>x51 x52. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lRecvOuterFriends x51 x52\<rbrakk> \<Longrightarrow> ou = ou1
 5. \<And>x61 x62. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lInnerPosts x61 x62\<rbrakk> \<Longrightarrow> ou = ou1
 6. \<And>x71 x72. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lOuterPosts x71 x72\<rbrakk> \<Longrightarrow> ou = ou1
 7. \<And>x81 x82 x83. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lClientsPost x81 x82 x83\<rbrakk> \<Longrightarrow> ou = ou1
 8. \<And>x91 x92. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lPendingSApiReqs x91 x92\<rbrakk> \<Longrightarrow> ou = ou1
 9. \<And>x101 x102. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lServerAPIs x101 x102\<rbrakk> \<Longrightarrow> ou = ou1
 10. \<And>x111 x112. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lPendingCApiReqs x111 x112\<rbrakk> \<Longrightarrow> ou = ou1
A total of 11 subgoals...
[PROOF STEP]
case (lInnerPosts uid p)
[PROOF STATE]
proof (state)
this:
la = lInnerPosts uid p

goal (11 subgoals):
 1. \<And>x11 x12. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid__ \<and> uid__ \<in> UIDs AID \<and> uid__ \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lPendingUReqs x11 x12\<rbrakk> \<Longrightarrow> ou = ou1
 2. \<And>x21 x22. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid__ \<and> uid__ \<in> UIDs AID \<and> uid__ \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lAllUsers x21 x22\<rbrakk> \<Longrightarrow> ou = ou1
 3. \<And>x31 x32 x33. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid__ \<and> uid__ \<in> UIDs AID \<and> uid__ \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lFriends x31 x32 x33\<rbrakk> \<Longrightarrow> ou = ou1
 4. \<And>x51 x52. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid__ \<and> uid__ \<in> UIDs AID \<and> uid__ \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lRecvOuterFriends x51 x52\<rbrakk> \<Longrightarrow> ou = ou1
 5. \<And>x61 x62. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid__ \<and> uid__ \<in> UIDs AID \<and> uid__ \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lInnerPosts x61 x62\<rbrakk> \<Longrightarrow> ou = ou1
 6. \<And>x71 x72. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid__ \<and> uid__ \<in> UIDs AID \<and> uid__ \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lOuterPosts x71 x72\<rbrakk> \<Longrightarrow> ou = ou1
 7. \<And>x81 x82 x83. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid__ \<and> uid__ \<in> UIDs AID \<and> uid__ \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lClientsPost x81 x82 x83\<rbrakk> \<Longrightarrow> ou = ou1
 8. \<And>x91 x92. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid__ \<and> uid__ \<in> UIDs AID \<and> uid__ \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lPendingSApiReqs x91 x92\<rbrakk> \<Longrightarrow> ou = ou1
 9. \<And>x101 x102. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid__ \<and> uid__ \<in> UIDs AID \<and> uid__ \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lServerAPIs x101 x102\<rbrakk> \<Longrightarrow> ou = ou1
 10. \<And>x111 x112. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid__ \<and> uid__ \<in> UIDs AID \<and> uid__ \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lPendingCApiReqs x111 x112\<rbrakk> \<Longrightarrow> ou = ou1
A total of 11 subgoals...
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
la = lInnerPosts uid p
[PROOF STEP]
have o: "\<And>nid. owner s nid = owner s1 nid"
                and n: "\<And>nid. post s nid = post s1 nid"
                and nids: "postIDs s = postIDs s1"
                and vis: "vis s = vis s1"
                and fu: "\<And>uid'. friendIDs s uid' = friendIDs s1 uid'"
                and e: "e_listInnerPosts s uid p \<longleftrightarrow> e_listInnerPosts s1 uid p"
[PROOF STATE]
proof (prove)
using this:
la = lInnerPosts uid p

goal (1 subgoal):
 1. ((\<And>nid. owner s nid = owner s1 nid) &&& (\<And>nid. post s nid = post s1 nid) &&& postIDs s = postIDs s1) &&& vis s = vis s1 &&& (\<And>uid'. friendIDs s uid' = friendIDs s1 uid') &&& e_listInnerPosts s uid p = e_listInnerPosts s1 uid p
[PROOF STEP]
using ss1
[PROOF STATE]
proof (prove)
using this:
la = lInnerPosts uid p
eqButUID s s1

goal (1 subgoal):
 1. ((\<And>nid. owner s nid = owner s1 nid) &&& (\<And>nid. post s nid = post s1 nid) &&& postIDs s = postIDs s1) &&& vis s = vis s1 &&& (\<And>uid'. friendIDs s uid' = friendIDs s1 uid') &&& e_listInnerPosts s uid p = e_listInnerPosts s1 uid p
[PROOF STEP]
unfolding eqButUID_def l_defs
[PROOF STATE]
proof (prove)
using this:
la = lInnerPosts uid p
admin s = admin s1 \<and> pendingUReqs s = pendingUReqs s1 \<and> userReq s = userReq s1 \<and> userIDs s = userIDs s1 \<and> user s = user s1 \<and> pass s = pass s1 \<and> pendingFReqs s = pendingFReqs s1 \<and> friendReq s = friendReq s1 \<and> friendIDs s = friendIDs s1 \<and> postIDs s = postIDs s1 \<and> admin s = admin s1 \<and> post s = post s1 \<and> vis s = vis s1 \<and> owner s = owner s1 \<and> pendingSApiReqs s = pendingSApiReqs s1 \<and> sApiReq s = sApiReq s1 \<and> serverApiIDs s = serverApiIDs s1 \<and> serverPass s = serverPass s1 \<and> outerPostIDs s = outerPostIDs s1 \<and> outerPost s = outerPost s1 \<and> outerVis s = outerVis s1 \<and> outerOwner s = outerOwner s1 \<and> eqButUIDf (sentOuterFriendIDs s) (sentOuterFriendIDs s1) \<and> recvOuterFriendIDs s = recvOuterFriendIDs s1 \<and> pendingCApiReqs s = pendingCApiReqs s1 \<and> cApiReq s = cApiReq s1 \<and> clientApiIDs s = clientApiIDs s1 \<and> clientPass s = clientPass s1 \<and> sharedWith s = sharedWith s1

goal (1 subgoal):
 1. ((\<And>nid. owner s nid = owner s1 nid) &&& (\<And>nid. post s nid = post s1 nid) &&& postIDs s = postIDs s1) &&& vis s = vis s1 &&& (\<And>uid'. friendIDs s uid' = friendIDs s1 uid') &&& (IDsOK s [uid] [] [] [] \<and> pass s uid = p) = (IDsOK s1 [uid] [] [] [] \<and> pass s1 uid = p)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
owner s ?nid = owner s1 ?nid
post s ?nid = post s1 ?nid
postIDs s = postIDs s1
vis s = vis s1
friendIDs s ?uid' = friendIDs s1 ?uid'
e_listInnerPosts s uid p = e_listInnerPosts s1 uid p

goal (11 subgoals):
 1. \<And>x11 x12. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid__ \<and> uid__ \<in> UIDs AID \<and> uid__ \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lPendingUReqs x11 x12\<rbrakk> \<Longrightarrow> ou = ou1
 2. \<And>x21 x22. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid__ \<and> uid__ \<in> UIDs AID \<and> uid__ \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lAllUsers x21 x22\<rbrakk> \<Longrightarrow> ou = ou1
 3. \<And>x31 x32 x33. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid__ \<and> uid__ \<in> UIDs AID \<and> uid__ \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lFriends x31 x32 x33\<rbrakk> \<Longrightarrow> ou = ou1
 4. \<And>x51 x52. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid__ \<and> uid__ \<in> UIDs AID \<and> uid__ \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lRecvOuterFriends x51 x52\<rbrakk> \<Longrightarrow> ou = ou1
 5. \<And>x61 x62. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid__ \<and> uid__ \<in> UIDs AID \<and> uid__ \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lInnerPosts x61 x62\<rbrakk> \<Longrightarrow> ou = ou1
 6. \<And>x71 x72. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid__ \<and> uid__ \<in> UIDs AID \<and> uid__ \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lOuterPosts x71 x72\<rbrakk> \<Longrightarrow> ou = ou1
 7. \<And>x81 x82 x83. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid__ \<and> uid__ \<in> UIDs AID \<and> uid__ \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lClientsPost x81 x82 x83\<rbrakk> \<Longrightarrow> ou = ou1
 8. \<And>x91 x92. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid__ \<and> uid__ \<in> UIDs AID \<and> uid__ \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lPendingSApiReqs x91 x92\<rbrakk> \<Longrightarrow> ou = ou1
 9. \<And>x101 x102. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid__ \<and> uid__ \<in> UIDs AID \<and> uid__ \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lServerAPIs x101 x102\<rbrakk> \<Longrightarrow> ou = ou1
 10. \<And>x111 x112. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid__ \<and> uid__ \<in> UIDs AID \<and> uid__ \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lPendingCApiReqs x111 x112\<rbrakk> \<Longrightarrow> ou = ou1
A total of 11 subgoals...
[PROOF STEP]
have "listInnerPosts s uid p = listInnerPosts s1 uid p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. listInnerPosts s uid p = listInnerPosts s1 uid p
[PROOF STEP]
unfolding listInnerPosts_def o n nids vis fu
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmap (\<lambda>pID. if vis s1 pID \<noteq> FriendV \<or> uid \<in>\<in> friendIDs s1 (owner s1 pID) \<or> uid = owner s1 pID then [(owner s1 pID, pID)] else []) (postIDs s1) = cmap (\<lambda>pID. if vis s1 pID \<noteq> FriendV \<or> uid \<in>\<in> friendIDs s1 (owner s1 pID) \<or> uid = owner s1 pID then [(owner s1 pID, pID)] else []) (postIDs s1)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
listInnerPosts s uid p = listInnerPosts s1 uid p

goal (11 subgoals):
 1. \<And>x11 x12. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid__ \<and> uid__ \<in> UIDs AID \<and> uid__ \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lPendingUReqs x11 x12\<rbrakk> \<Longrightarrow> ou = ou1
 2. \<And>x21 x22. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid__ \<and> uid__ \<in> UIDs AID \<and> uid__ \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lAllUsers x21 x22\<rbrakk> \<Longrightarrow> ou = ou1
 3. \<And>x31 x32 x33. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid__ \<and> uid__ \<in> UIDs AID \<and> uid__ \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lFriends x31 x32 x33\<rbrakk> \<Longrightarrow> ou = ou1
 4. \<And>x51 x52. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid__ \<and> uid__ \<in> UIDs AID \<and> uid__ \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lRecvOuterFriends x51 x52\<rbrakk> \<Longrightarrow> ou = ou1
 5. \<And>x61 x62. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid__ \<and> uid__ \<in> UIDs AID \<and> uid__ \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lInnerPosts x61 x62\<rbrakk> \<Longrightarrow> ou = ou1
 6. \<And>x71 x72. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid__ \<and> uid__ \<in> UIDs AID \<and> uid__ \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lOuterPosts x71 x72\<rbrakk> \<Longrightarrow> ou = ou1
 7. \<And>x81 x82 x83. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid__ \<and> uid__ \<in> UIDs AID \<and> uid__ \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lClientsPost x81 x82 x83\<rbrakk> \<Longrightarrow> ou = ou1
 8. \<And>x91 x92. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid__ \<and> uid__ \<in> UIDs AID \<and> uid__ \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lPendingSApiReqs x91 x92\<rbrakk> \<Longrightarrow> ou = ou1
 9. \<And>x101 x102. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid__ \<and> uid__ \<in> UIDs AID \<and> uid__ \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lServerAPIs x101 x102\<rbrakk> \<Longrightarrow> ou = ou1
 10. \<And>x111 x112. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid__ \<and> uid__ \<in> UIDs AID \<and> uid__ \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lPendingCApiReqs x111 x112\<rbrakk> \<Longrightarrow> ou = ou1
A total of 11 subgoals...
[PROOF STEP]
with e
[PROOF STATE]
proof (chain)
picking this:
e_listInnerPosts s uid p = e_listInnerPosts s1 uid p
listInnerPosts s uid p = listInnerPosts s1 uid p
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
e_listInnerPosts s uid p = e_listInnerPosts s1 uid p
listInnerPosts s uid p = listInnerPosts s1 uid p

goal (1 subgoal):
 1. ou = ou1
[PROOF STEP]
using Lact lInnerPosts step step1
[PROOF STATE]
proof (prove)
using this:
e_listInnerPosts s uid p = e_listInnerPosts s1 uid p
listInnerPosts s uid p = listInnerPosts s1 uid p
a = Lact la
la = lInnerPosts uid p
step s a = (ou, s')
step s1 a = (ou1, s1')

goal (1 subgoal):
 1. ou = ou1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ou = ou1

goal (10 subgoals):
 1. \<And>x11 x12. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid__ \<and> uid__ \<in> UIDs AID \<and> uid__ \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lPendingUReqs x11 x12\<rbrakk> \<Longrightarrow> ou = ou1
 2. \<And>x21 x22. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid__ \<and> uid__ \<in> UIDs AID \<and> uid__ \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lAllUsers x21 x22\<rbrakk> \<Longrightarrow> ou = ou1
 3. \<And>x31 x32 x33. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid__ \<and> uid__ \<in> UIDs AID \<and> uid__ \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lFriends x31 x32 x33\<rbrakk> \<Longrightarrow> ou = ou1
 4. \<And>x51 x52. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid__ \<and> uid__ \<in> UIDs AID \<and> uid__ \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lRecvOuterFriends x51 x52\<rbrakk> \<Longrightarrow> ou = ou1
 5. \<And>x71 x72. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid__ \<and> uid__ \<in> UIDs AID \<and> uid__ \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lOuterPosts x71 x72\<rbrakk> \<Longrightarrow> ou = ou1
 6. \<And>x81 x82 x83. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid__ \<and> uid__ \<in> UIDs AID \<and> uid__ \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lClientsPost x81 x82 x83\<rbrakk> \<Longrightarrow> ou = ou1
 7. \<And>x91 x92. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid__ \<and> uid__ \<in> UIDs AID \<and> uid__ \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lPendingSApiReqs x91 x92\<rbrakk> \<Longrightarrow> ou = ou1
 8. \<And>x101 x102. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid__ \<and> uid__ \<in> UIDs AID \<and> uid__ \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lServerAPIs x101 x102\<rbrakk> \<Longrightarrow> ou = ou1
 9. \<And>x111 x112. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid__ \<and> uid__ \<in> UIDs AID \<and> uid__ \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lPendingCApiReqs x111 x112\<rbrakk> \<Longrightarrow> ou = ou1
 10. \<And>x121 x122. \<lbrakk>a = Lact la; eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); userOfA a = Some uid__ \<and> uid__ \<in> UIDs AID \<and> uid__ \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa; la = lClientAPIs x121 x122\<rbrakk> \<Longrightarrow> ou = ou1
[PROOF STEP]
qed (auto simp add: simps)
[PROOF STATE]
proof (state)
this:
ou = ou1

goal (2 subgoals):
 1. \<And>x3. a = Dact x3 \<Longrightarrow> ou = ou1
 2. \<And>x4. a = Uact x4 \<Longrightarrow> ou = ou1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x3. a = Dact x3 \<Longrightarrow> ou = ou1
 2. \<And>x4. a = Uact x4 \<Longrightarrow> ou = ou1
[PROOF STEP]
case (Uact ua)
[PROOF STATE]
proof (state)
this:
a = Uact ua

goal (2 subgoals):
 1. \<And>x3. a = Dact x3 \<Longrightarrow> ou = ou1
 2. \<And>x4. a = Uact x4 \<Longrightarrow> ou = ou1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a = Uact ua
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a = Uact ua

goal (1 subgoal):
 1. ou = ou1
[PROOF STEP]
using facts
[PROOF STATE]
proof (prove)
using this:
a = Uact ua
eqButUID s s1
step s a = (ou, s')
step s1 a = (ou1, s1')
userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa

goal (1 subgoal):
 1. ou = ou1
[PROOF STEP]
by (cases ua) (auto simp add: simps)
[PROOF STATE]
proof (state)
this:
ou = ou1

goal (1 subgoal):
 1. \<And>x3. a = Dact x3 \<Longrightarrow> ou = ou1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x3. a = Dact x3 \<Longrightarrow> ou = ou1
[PROOF STEP]
case (Dact da)
[PROOF STATE]
proof (state)
this:
a = Dact da

goal (1 subgoal):
 1. \<And>x3. a = Dact x3 \<Longrightarrow> ou = ou1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a = Dact da
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a = Dact da

goal (1 subgoal):
 1. ou = ou1
[PROOF STEP]
using facts
[PROOF STATE]
proof (prove)
using this:
a = Dact da
eqButUID s s1
step s a = (ou, s')
step s1 a = (ou1, s1')
userOfA a = Some uid \<and> uid \<in> UIDs AID \<and> uid \<noteq> UID \<or> a = COMact com_act \<or> a = Sact sa

goal (1 subgoal):
 1. ou = ou1
[PROOF STEP]
by (cases da) (auto simp add: simps)
[PROOF STATE]
proof (state)
this:
ou = ou1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ou = ou1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma step_open_\<phi>:
assumes "step s a = (ou, s')"
and "open s \<noteq> open s'"
shows "\<phi> (Trans s a ou s')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> (Trans s a ou s')
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
step s a = (ou, s')
open s \<noteq> open s'

goal (1 subgoal):
 1. \<phi> (Trans s a ou s')
[PROOF STEP]
by (elim open_step_cases) (auto simp: open_def)


[STATEMENT]
lemma step_sendOFriend_eqButUID:
assumes "step s a = (ou, s')"
and "reach s"
and "uID' \<notin> UIDs aID"
and "a = COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<or>
     a = COMact (comSendDeleteOFriend UID (pass s UID) aID uID')"
shows "eqButUID s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqButUID s s'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
step s a = (ou, s')
reach s
uID' \<notin> UIDs aID
a = COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<or> a = COMact (comSendDeleteOFriend UID (pass s UID) aID uID')

goal (1 subgoal):
 1. eqButUID s s'
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>step s a = (ou, s'); reach s; uID' \<notin> UIDs aID; a = COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<or> a = COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); ?P4\<rbrakk> \<Longrightarrow> eqButUID s s'
 2. \<lbrakk>step s a = (ou, s'); reach s; uID' \<notin> UIDs aID; a = COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<or> a = COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); \<not> ?P4\<rbrakk> \<Longrightarrow> eqButUID s s'
[PROOF STEP]
assume "\<phi> (Trans s a ou s')"
[PROOF STATE]
proof (state)
this:
\<phi> (Trans s a ou s')

goal (2 subgoals):
 1. \<lbrakk>step s a = (ou, s'); reach s; uID' \<notin> UIDs aID; a = COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<or> a = COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); ?P4\<rbrakk> \<Longrightarrow> eqButUID s s'
 2. \<lbrakk>step s a = (ou, s'); reach s; uID' \<notin> UIDs aID; a = COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<or> a = COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); \<not> ?P4\<rbrakk> \<Longrightarrow> eqButUID s s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<phi> (Trans s a ou s')
[PROOF STEP]
show "eqButUID s s'"
[PROOF STATE]
proof (prove)
using this:
\<phi> (Trans s a ou s')

goal (1 subgoal):
 1. eqButUID s s'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<phi> (Trans s a ou s')
step s a = (ou, s')
reach s
uID' \<notin> UIDs aID
a = COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<or> a = COMact (comSendDeleteOFriend UID (pass s UID) aID uID')

goal (1 subgoal):
 1. eqButUID s s'
[PROOF STEP]
proof (cases rule: \<phi>E)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>p aIDa uID'a. \<lbrakk>uID' \<notin> UIDs aID; a = COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<or> a = COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); a = COMact (comSendCreateOFriend UID p aIDa uID'a); ou \<noteq> outErr; f (Trans s a ou s') = FrVal aIDa uID'a True; uID'a \<notin> UIDs aIDa\<rbrakk> \<Longrightarrow> eqButUID s s'
 2. \<And>p aIDa uID'a. \<lbrakk>uID' \<notin> UIDs aID; a = COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<or> a = COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); a = COMact (comSendDeleteOFriend UID p aIDa uID'a); ou \<noteq> outErr; f (Trans s a ou s') = FrVal aIDa uID'a False; uID'a \<notin> UIDs aIDa\<rbrakk> \<Longrightarrow> eqButUID s s'
 3. \<And>uid p uid'. \<lbrakk>uID' \<notin> UIDs aID; a = COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<or> a = COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); a = Cact (cFriend uid p uid'); ou = outOK; p = pass s uid; uid \<in> UIDs AID \<and> uid' = UID \<or> uid = UID \<and> uid' \<in> UIDs AID; open s'; \<not> open s; f (Trans s a ou s') = OVal True\<rbrakk> \<Longrightarrow> eqButUID s s'
 4. \<And>uid p uid'. \<lbrakk>uID' \<notin> UIDs aID; a = COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<or> a = COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); a = Dact (dFriend uid p uid'); ou = outOK; p = pass s uid; uid \<in> UIDs AID \<and> uid' = UID \<or> uid = UID \<and> uid' \<in> UIDs AID; open s; \<not> open s'; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> eqButUID s s'
[PROOF STEP]
case (Friend p aid uid')
[PROOF STATE]
proof (state)
this:
a = COMact (comSendCreateOFriend UID p aid uid')
ou \<noteq> outErr
f (Trans s a ou s') = FrVal aid uid' True
uid' \<notin> UIDs aid

goal (4 subgoals):
 1. \<And>p aIDa uID'a. \<lbrakk>uID' \<notin> UIDs aID; a = COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<or> a = COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); a = COMact (comSendCreateOFriend UID p aIDa uID'a); ou \<noteq> outErr; f (Trans s a ou s') = FrVal aIDa uID'a True; uID'a \<notin> UIDs aIDa\<rbrakk> \<Longrightarrow> eqButUID s s'
 2. \<And>p aIDa uID'a. \<lbrakk>uID' \<notin> UIDs aID; a = COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<or> a = COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); a = COMact (comSendDeleteOFriend UID p aIDa uID'a); ou \<noteq> outErr; f (Trans s a ou s') = FrVal aIDa uID'a False; uID'a \<notin> UIDs aIDa\<rbrakk> \<Longrightarrow> eqButUID s s'
 3. \<And>uid p uid'. \<lbrakk>uID' \<notin> UIDs aID; a = COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<or> a = COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); a = Cact (cFriend uid p uid'); ou = outOK; p = pass s uid; uid \<in> UIDs AID \<and> uid' = UID \<or> uid = UID \<and> uid' \<in> UIDs AID; open s'; \<not> open s; f (Trans s a ou s') = OVal True\<rbrakk> \<Longrightarrow> eqButUID s s'
 4. \<And>uid p uid'. \<lbrakk>uID' \<notin> UIDs aID; a = COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<or> a = COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); a = Dact (dFriend uid p uid'); ou = outOK; p = pass s uid; uid \<in> UIDs AID \<and> uid' = UID \<or> uid = UID \<and> uid' \<in> UIDs AID; open s; \<not> open s'; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> eqButUID s s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a = COMact (comSendCreateOFriend UID p aid uid')
ou \<noteq> outErr
f (Trans s a ou s') = FrVal aid uid' True
uid' \<notin> UIDs aid
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a = COMact (comSendCreateOFriend UID p aid uid')
ou \<noteq> outErr
f (Trans s a ou s') = FrVal aid uid' True
uid' \<notin> UIDs aid

goal (1 subgoal):
 1. eqButUID s s'
[PROOF STEP]
using assms eqButUID_sentOuterFriendIDs_cong[of s s]
[PROOF STATE]
proof (prove)
using this:
a = COMact (comSendCreateOFriend UID p aid uid')
ou \<noteq> outErr
f (Trans s a ou s') = FrVal aid uid' True
uid' \<notin> UIDs aid
step s a = (ou, s')
reach s
uID' \<notin> UIDs aID
a = COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<or> a = COMact (comSendDeleteOFriend UID (pass s UID) aID uID')
\<lbrakk>eqButUID s s; ?uid' \<notin> UIDs ?aid\<rbrakk> \<Longrightarrow> eqButUID (s\<lparr>sentOuterFriendIDs := (sentOuterFriendIDs s)(UID := sentOuterFriendIDs s UID ## (?aid, ?uid'))\<rparr>) s
\<lbrakk>eqButUID s s; ?uid' \<notin> UIDs ?aid\<rbrakk> \<Longrightarrow> eqButUID s (s\<lparr>sentOuterFriendIDs := (sentOuterFriendIDs s)(UID := sentOuterFriendIDs s UID ## (?aid, ?uid'))\<rparr>)
\<lbrakk>eqButUID s s; ?uid' \<notin> UIDs ?aid\<rbrakk> \<Longrightarrow> eqButUID s (s\<lparr>sentOuterFriendIDs := (sentOuterFriendIDs s)(UID := remove1 (?aid, ?uid') (sentOuterFriendIDs s UID))\<rparr>)
\<lbrakk>eqButUID s s; ?uid' \<notin> UIDs ?aid\<rbrakk> \<Longrightarrow> eqButUID (s\<lparr>sentOuterFriendIDs := (sentOuterFriendIDs s)(UID := remove1 (?aid, ?uid') (sentOuterFriendIDs s UID))\<rparr>) s

goal (1 subgoal):
 1. eqButUID s s'
[PROOF STEP]
by (auto split: prod.splits simp: com_defs)
[PROOF STATE]
proof (state)
this:
eqButUID s s'

goal (3 subgoals):
 1. \<And>p aIDa uID'a. \<lbrakk>uID' \<notin> UIDs aID; a = COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<or> a = COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); a = COMact (comSendDeleteOFriend UID p aIDa uID'a); ou \<noteq> outErr; f (Trans s a ou s') = FrVal aIDa uID'a False; uID'a \<notin> UIDs aIDa\<rbrakk> \<Longrightarrow> eqButUID s s'
 2. \<And>uid p uid'. \<lbrakk>uID' \<notin> UIDs aID; a = COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<or> a = COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); a = Cact (cFriend uid p uid'); ou = outOK; p = pass s uid; uid \<in> UIDs AID \<and> uid' = UID \<or> uid = UID \<and> uid' \<in> UIDs AID; open s'; \<not> open s; f (Trans s a ou s') = OVal True\<rbrakk> \<Longrightarrow> eqButUID s s'
 3. \<And>uid p uid'. \<lbrakk>uID' \<notin> UIDs aID; a = COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<or> a = COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); a = Dact (dFriend uid p uid'); ou = outOK; p = pass s uid; uid \<in> UIDs AID \<and> uid' = UID \<or> uid = UID \<and> uid' \<in> UIDs AID; open s; \<not> open s'; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> eqButUID s s'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>p aIDa uID'a. \<lbrakk>uID' \<notin> UIDs aID; a = COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<or> a = COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); a = COMact (comSendDeleteOFriend UID p aIDa uID'a); ou \<noteq> outErr; f (Trans s a ou s') = FrVal aIDa uID'a False; uID'a \<notin> UIDs aIDa\<rbrakk> \<Longrightarrow> eqButUID s s'
 2. \<And>uid p uid'. \<lbrakk>uID' \<notin> UIDs aID; a = COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<or> a = COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); a = Cact (cFriend uid p uid'); ou = outOK; p = pass s uid; uid \<in> UIDs AID \<and> uid' = UID \<or> uid = UID \<and> uid' \<in> UIDs AID; open s'; \<not> open s; f (Trans s a ou s') = OVal True\<rbrakk> \<Longrightarrow> eqButUID s s'
 3. \<And>uid p uid'. \<lbrakk>uID' \<notin> UIDs aID; a = COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<or> a = COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); a = Dact (dFriend uid p uid'); ou = outOK; p = pass s uid; uid \<in> UIDs AID \<and> uid' = UID \<or> uid = UID \<and> uid' \<in> UIDs AID; open s; \<not> open s'; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> eqButUID s s'
[PROOF STEP]
case (Unfriend p aid uid')
[PROOF STATE]
proof (state)
this:
a = COMact (comSendDeleteOFriend UID p aid uid')
ou \<noteq> outErr
f (Trans s a ou s') = FrVal aid uid' False
uid' \<notin> UIDs aid

goal (3 subgoals):
 1. \<And>p aIDa uID'a. \<lbrakk>uID' \<notin> UIDs aID; a = COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<or> a = COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); a = COMact (comSendDeleteOFriend UID p aIDa uID'a); ou \<noteq> outErr; f (Trans s a ou s') = FrVal aIDa uID'a False; uID'a \<notin> UIDs aIDa\<rbrakk> \<Longrightarrow> eqButUID s s'
 2. \<And>uid p uid'. \<lbrakk>uID' \<notin> UIDs aID; a = COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<or> a = COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); a = Cact (cFriend uid p uid'); ou = outOK; p = pass s uid; uid \<in> UIDs AID \<and> uid' = UID \<or> uid = UID \<and> uid' \<in> UIDs AID; open s'; \<not> open s; f (Trans s a ou s') = OVal True\<rbrakk> \<Longrightarrow> eqButUID s s'
 3. \<And>uid p uid'. \<lbrakk>uID' \<notin> UIDs aID; a = COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<or> a = COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); a = Dact (dFriend uid p uid'); ou = outOK; p = pass s uid; uid \<in> UIDs AID \<and> uid' = UID \<or> uid = UID \<and> uid' \<in> UIDs AID; open s; \<not> open s'; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> eqButUID s s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a = COMact (comSendDeleteOFriend UID p aid uid')
ou \<noteq> outErr
f (Trans s a ou s') = FrVal aid uid' False
uid' \<notin> UIDs aid
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a = COMact (comSendDeleteOFriend UID p aid uid')
ou \<noteq> outErr
f (Trans s a ou s') = FrVal aid uid' False
uid' \<notin> UIDs aid

goal (1 subgoal):
 1. eqButUID s s'
[PROOF STEP]
using assms eqButUID_sentOuterFriendIDs_cong[of s s]
[PROOF STATE]
proof (prove)
using this:
a = COMact (comSendDeleteOFriend UID p aid uid')
ou \<noteq> outErr
f (Trans s a ou s') = FrVal aid uid' False
uid' \<notin> UIDs aid
step s a = (ou, s')
reach s
uID' \<notin> UIDs aID
a = COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<or> a = COMact (comSendDeleteOFriend UID (pass s UID) aID uID')
\<lbrakk>eqButUID s s; ?uid' \<notin> UIDs ?aid\<rbrakk> \<Longrightarrow> eqButUID (s\<lparr>sentOuterFriendIDs := (sentOuterFriendIDs s)(UID := sentOuterFriendIDs s UID ## (?aid, ?uid'))\<rparr>) s
\<lbrakk>eqButUID s s; ?uid' \<notin> UIDs ?aid\<rbrakk> \<Longrightarrow> eqButUID s (s\<lparr>sentOuterFriendIDs := (sentOuterFriendIDs s)(UID := sentOuterFriendIDs s UID ## (?aid, ?uid'))\<rparr>)
\<lbrakk>eqButUID s s; ?uid' \<notin> UIDs ?aid\<rbrakk> \<Longrightarrow> eqButUID s (s\<lparr>sentOuterFriendIDs := (sentOuterFriendIDs s)(UID := remove1 (?aid, ?uid') (sentOuterFriendIDs s UID))\<rparr>)
\<lbrakk>eqButUID s s; ?uid' \<notin> UIDs ?aid\<rbrakk> \<Longrightarrow> eqButUID (s\<lparr>sentOuterFriendIDs := (sentOuterFriendIDs s)(UID := remove1 (?aid, ?uid') (sentOuterFriendIDs s UID))\<rparr>) s

goal (1 subgoal):
 1. eqButUID s s'
[PROOF STEP]
by (auto split: prod.splits simp: com_defs)
[PROOF STATE]
proof (state)
this:
eqButUID s s'

goal (2 subgoals):
 1. \<And>uid p uid'. \<lbrakk>uID' \<notin> UIDs aID; a = COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<or> a = COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); a = Cact (cFriend uid p uid'); ou = outOK; p = pass s uid; uid \<in> UIDs AID \<and> uid' = UID \<or> uid = UID \<and> uid' \<in> UIDs AID; open s'; \<not> open s; f (Trans s a ou s') = OVal True\<rbrakk> \<Longrightarrow> eqButUID s s'
 2. \<And>uid p uid'. \<lbrakk>uID' \<notin> UIDs aID; a = COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<or> a = COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); a = Dact (dFriend uid p uid'); ou = outOK; p = pass s uid; uid \<in> UIDs AID \<and> uid' = UID \<or> uid = UID \<and> uid' \<in> UIDs AID; open s; \<not> open s'; f (Trans s a ou s') = OVal False\<rbrakk> \<Longrightarrow> eqButUID s s'
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
eqButUID s s'

goal (1 subgoal):
 1. \<lbrakk>step s a = (ou, s'); reach s; uID' \<notin> UIDs aID; a = COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<or> a = COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); \<not> \<phi> (Trans s a ou s')\<rbrakk> \<Longrightarrow> eqButUID s s'
[PROOF STEP]
qed (auto split: prod.splits)


[STATEMENT]
lemma eqButUID_step_\<phi>_imp:
assumes ss1: "eqButUID s s1"
and rs: "reach s" and rs1: "reach s1"
and step: "step s a = (ou,s')" and step1: "step s1 a = (ou1,s1')"
and a: "\<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow>
                   a \<noteq> COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<and>
                   a \<noteq> COMact (comSendDeleteOFriend UID (pass s UID) aID uID')"
and \<phi>: "\<phi> (Trans s a ou s')"
shows "\<phi> (Trans s1 a ou1 s1')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> (Trans s1 a ou1 s1')
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<phi> (Trans s1 a ou1 s1')
[PROOF STEP]
have "eqButUID s' s1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqButUID s' s1'
[PROOF STEP]
using eqButUID_step[OF ss1 step step1 rs rs1]
[PROOF STATE]
proof (prove)
using this:
eqButUID s' s1'

goal (1 subgoal):
 1. eqButUID s' s1'
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
eqButUID s' s1'

goal (1 subgoal):
 1. \<phi> (Trans s1 a ou1 s1')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eqButUID s' s1'
[PROOF STEP]
have "open s = open s1" and "open s' = open s1'"
[PROOF STATE]
proof (prove)
using this:
eqButUID s' s1'

goal (1 subgoal):
 1. open s = open s1 &&& open s' = open s1'
[PROOF STEP]
using ss1
[PROOF STATE]
proof (prove)
using this:
eqButUID s' s1'
eqButUID s s1

goal (1 subgoal):
 1. open s = open s1 &&& open s' = open s1'
[PROOF STEP]
by (auto simp: eqButUID_open_eq)
[PROOF STATE]
proof (state)
this:
open s = open s1
open s' = open s1'

goal (1 subgoal):
 1. \<phi> (Trans s1 a ou1 s1')
[PROOF STEP]
with \<phi> step step1
[PROOF STATE]
proof (chain)
picking this:
\<phi> (Trans s a ou s')
step s a = (ou, s')
step s1 a = (ou1, s1')
open s = open s1
open s' = open s1'
[PROOF STEP]
show "\<phi> (Trans s1 a ou1 s1')"
[PROOF STATE]
proof (prove)
using this:
\<phi> (Trans s a ou s')
step s a = (ou, s')
step s1 a = (ou1, s1')
open s = open s1
open s' = open s1'

goal (1 subgoal):
 1. \<phi> (Trans s1 a ou1 s1')
[PROOF STEP]
using rs ss1 a
[PROOF STATE]
proof (prove)
using this:
\<phi> (Trans s a ou s')
step s a = (ou, s')
step s1 a = (ou1, s1')
open s = open s1
open s' = open s1'
reach s
eqButUID s s1
\<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s UID) aID uID')

goal (1 subgoal):
 1. \<phi> (Trans s1 a ou1 s1')
[PROOF STEP]
by (elim \<phi>E) (auto simp: com_defs)
[PROOF STATE]
proof (state)
this:
\<phi> (Trans s1 a ou1 s1')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eqButUID_step_\<phi>:
assumes ss1: "eqButUID s s1"
and rs: "reach s" and rs1: "reach s1"
and step: "step s a = (ou,s')" and step1: "step s1 a = (ou1,s1')"
and a: "\<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow>
                   a \<noteq> COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<and>
                   a \<noteq> COMact (comSendDeleteOFriend UID (pass s UID) aID uID')"
shows "\<phi> (Trans s a ou s') = \<phi> (Trans s1 a ou1 s1')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> (Trans s a ou s') = \<phi> (Trans s1 a ou1 s1')
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<phi> (Trans s a ou s') \<Longrightarrow> \<phi> (Trans s1 a ou1 s1')
 2. \<phi> (Trans s1 a ou1 s1') \<Longrightarrow> \<phi> (Trans s a ou s')
[PROOF STEP]
assume "\<phi> (Trans s a ou s')"
[PROOF STATE]
proof (state)
this:
\<phi> (Trans s a ou s')

goal (2 subgoals):
 1. \<phi> (Trans s a ou s') \<Longrightarrow> \<phi> (Trans s1 a ou1 s1')
 2. \<phi> (Trans s1 a ou1 s1') \<Longrightarrow> \<phi> (Trans s a ou s')
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
eqButUID s s1
reach s
reach s1
step s a = (ou, s')
step s1 a = (ou1, s1')
\<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s UID) aID uID')
\<phi> (Trans s a ou s')
[PROOF STEP]
show "\<phi> (Trans s1 a ou1 s1')"
[PROOF STATE]
proof (prove)
using this:
eqButUID s s1
reach s
reach s1
step s a = (ou, s')
step s1 a = (ou1, s1')
\<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s UID) aID uID')
\<phi> (Trans s a ou s')

goal (1 subgoal):
 1. \<phi> (Trans s1 a ou1 s1')
[PROOF STEP]
by (rule eqButUID_step_\<phi>_imp)
[PROOF STATE]
proof (state)
this:
\<phi> (Trans s1 a ou1 s1')

goal (1 subgoal):
 1. \<phi> (Trans s1 a ou1 s1') \<Longrightarrow> \<phi> (Trans s a ou s')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<phi> (Trans s1 a ou1 s1') \<Longrightarrow> \<phi> (Trans s a ou s')
[PROOF STEP]
assume "\<phi> (Trans s1 a ou1 s1')"
[PROOF STATE]
proof (state)
this:
\<phi> (Trans s1 a ou1 s1')

goal (1 subgoal):
 1. \<phi> (Trans s1 a ou1 s1') \<Longrightarrow> \<phi> (Trans s a ou s')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<phi> (Trans s1 a ou1 s1')

goal (1 subgoal):
 1. \<phi> (Trans s1 a ou1 s1') \<Longrightarrow> \<phi> (Trans s a ou s')
[PROOF STEP]
have "eqButUID s1 s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqButUID s1 s
[PROOF STEP]
using ss1
[PROOF STATE]
proof (prove)
using this:
eqButUID s s1

goal (1 subgoal):
 1. eqButUID s1 s
[PROOF STEP]
by (rule eqButUID_sym)
[PROOF STATE]
proof (state)
this:
eqButUID s1 s

goal (1 subgoal):
 1. \<phi> (Trans s1 a ou1 s1') \<Longrightarrow> \<phi> (Trans s a ou s')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
eqButUID s1 s

goal (1 subgoal):
 1. \<phi> (Trans s1 a ou1 s1') \<Longrightarrow> \<phi> (Trans s a ou s')
[PROOF STEP]
have "\<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow>
                   a \<noteq> COMact (comSendCreateOFriend UID (pass s1 UID) aID uID') \<and>
                   a \<noteq> COMact (comSendDeleteOFriend UID (pass s1 UID) aID uID')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s1 UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s1 UID) aID uID')
[PROOF STEP]
using a ss1
[PROOF STATE]
proof (prove)
using this:
\<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s UID) aID uID')
eqButUID s s1

goal (1 subgoal):
 1. \<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s1 UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s1 UID) aID uID')
[PROOF STEP]
by (auto simp: eqButUID_stateSelectors)
[PROOF STATE]
proof (state)
this:
\<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s1 UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s1 UID) aID uID')

goal (1 subgoal):
 1. \<phi> (Trans s1 a ou1 s1') \<Longrightarrow> \<phi> (Trans s a ou s')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<phi> (Trans s1 a ou1 s1')
eqButUID s1 s
\<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s1 UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s1 UID) aID uID')
[PROOF STEP]
show "\<phi> (Trans s a ou s')"
[PROOF STATE]
proof (prove)
using this:
\<phi> (Trans s1 a ou1 s1')
eqButUID s1 s
\<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s1 UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s1 UID) aID uID')

goal (1 subgoal):
 1. \<phi> (Trans s a ou s')
[PROOF STEP]
using rs rs1 step step1
[PROOF STATE]
proof (prove)
using this:
\<phi> (Trans s1 a ou1 s1')
eqButUID s1 s
\<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s1 UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s1 UID) aID uID')
reach s
reach s1
step s a = (ou, s')
step s1 a = (ou1, s1')

goal (1 subgoal):
 1. \<phi> (Trans s a ou s')
[PROOF STEP]
by (intro eqButUID_step_\<phi>_imp[of s1 s])
[PROOF STATE]
proof (state)
this:
\<phi> (Trans s a ou s')

goal:
No subgoals!
[PROOF STEP]
qed