[STATEMENT]
lemma Dact_dFriend_step_eqButUID:
assumes step: "step s (Dact (dFriend uid p uid')) = (ou,s')"
and s: "reach s"
and uids: "(uid = UID1 \<and> uid' = UID2) \<or> (uid = UID2 \<and> uid' = UID1)" (is "?u12 \<or> ?u21")
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 (Dact (dFriend uid p uid')) = (ou, s')
reach s
uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1

goal (1 subgoal):
 1. eqButUID s s'
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>step s (Dact (dFriend uid p uid')) = (ou, s'); reach s; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; ?P3\<rbrakk> \<Longrightarrow> eqButUID s s'
 2. \<lbrakk>step s (Dact (dFriend uid p uid')) = (ou, s'); reach s; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; \<not> ?P3\<rbrakk> \<Longrightarrow> eqButUID s s'
[PROOF STEP]
assume ou: "ou = outOK"
[PROOF STATE]
proof (state)
this:
ou = outOK

goal (2 subgoals):
 1. \<lbrakk>step s (Dact (dFriend uid p uid')) = (ou, s'); reach s; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; ?P3\<rbrakk> \<Longrightarrow> eqButUID s s'
 2. \<lbrakk>step s (Dact (dFriend uid p uid')) = (ou, s'); reach s; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; \<not> ?P3\<rbrakk> \<Longrightarrow> eqButUID s s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ou = outOK
[PROOF STEP]
have "uid' \<in>\<in> friendIDs s uid"
[PROOF STATE]
proof (prove)
using this:
ou = outOK

goal (1 subgoal):
 1. uid' \<in>\<in> friendIDs s uid
[PROOF STEP]
using step
[PROOF STATE]
proof (prove)
using this:
ou = outOK
step s (Dact (dFriend uid p uid')) = (ou, s')

goal (1 subgoal):
 1. uid' \<in>\<in> friendIDs s uid
[PROOF STEP]
by (auto simp add: d_defs)
[PROOF STATE]
proof (state)
this:
uid' \<in>\<in> friendIDs s uid

goal (2 subgoals):
 1. \<lbrakk>step s (Dact (dFriend uid p uid')) = (ou, s'); reach s; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; ?P3\<rbrakk> \<Longrightarrow> eqButUID s s'
 2. \<lbrakk>step s (Dact (dFriend uid p uid')) = (ou, s'); reach s; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; \<not> ?P3\<rbrakk> \<Longrightarrow> eqButUID s s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
uid' \<in>\<in> friendIDs s uid
[PROOF STEP]
have fRs: "distinct (friendIDs s uid)" "distinct (friendIDs s uid')"
[PROOF STATE]
proof (prove)
using this:
uid' \<in>\<in> friendIDs s uid

goal (1 subgoal):
 1. distinct (friendIDs s uid) &&& distinct (friendIDs s uid')
[PROOF STEP]
using reach_distinct_friends_reqs[OF s]
[PROOF STATE]
proof (prove)
using this:
uid' \<in>\<in> friendIDs s uid
distinct (friendIDs s ?uid)
distinct (pendingFReqs s ?uid)
distinct (sentOuterFriendIDs s ?uid)
distinct (recvOuterFriendIDs s ?uid)
?uid' \<in>\<in> pendingFReqs s ?uid \<Longrightarrow> ?uid' \<notin> set (friendIDs s ?uid)
?uid' \<in>\<in> pendingFReqs s ?uid \<Longrightarrow> ?uid \<notin> set (friendIDs s ?uid')

goal (1 subgoal):
 1. distinct (friendIDs s uid) &&& distinct (friendIDs s uid')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
distinct (friendIDs s uid)
distinct (friendIDs s uid')

goal (2 subgoals):
 1. \<lbrakk>step s (Dact (dFriend uid p uid')) = (ou, s'); reach s; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; ?P3\<rbrakk> \<Longrightarrow> eqButUID s s'
 2. \<lbrakk>step s (Dact (dFriend uid p uid')) = (ou, s'); reach s; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; \<not> ?P3\<rbrakk> \<Longrightarrow> eqButUID s s'
[PROOF STEP]
have "eqButUIDf (friendIDs s) (friendIDs (deleteFriend s uid p uid'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqButUIDf (friendIDs s) (friendIDs (deleteFriend s uid p uid'))
[PROOF STEP]
using fRs uids UID1_UID2
[PROOF STATE]
proof (prove)
using this:
distinct (friendIDs s uid)
distinct (friendIDs s uid')
uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1
UID1 \<noteq> UID2

goal (1 subgoal):
 1. eqButUIDf (friendIDs s) (friendIDs (deleteFriend s uid p uid'))
[PROOF STEP]
unfolding eqButUIDf_def
[PROOF STATE]
proof (prove)
using this:
distinct (friendIDs s uid)
distinct (friendIDs s uid')
uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1
UID1 \<noteq> UID2

goal (1 subgoal):
 1. eqButUIDl UID2 (friendIDs s UID1) (friendIDs (deleteFriend s uid p uid') UID1) \<and> eqButUIDl UID1 (friendIDs s UID2) (friendIDs (deleteFriend s uid p uid') UID2) \<and> (\<forall>uida. uida \<noteq> UID1 \<and> uida \<noteq> UID2 \<longrightarrow> friendIDs s uida = friendIDs (deleteFriend s uid p uid') uida)
[PROOF STEP]
by (cases "?u12") (auto simp add: d_defs remove1_idem distinct_remove1_removeAll)
[PROOF STATE]
proof (state)
this:
eqButUIDf (friendIDs s) (friendIDs (deleteFriend s uid p uid'))

goal (2 subgoals):
 1. \<lbrakk>step s (Dact (dFriend uid p uid')) = (ou, s'); reach s; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; ?P3\<rbrakk> \<Longrightarrow> eqButUID s s'
 2. \<lbrakk>step s (Dact (dFriend uid p uid')) = (ou, s'); reach s; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; \<not> ?P3\<rbrakk> \<Longrightarrow> eqButUID s s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eqButUIDf (friendIDs s) (friendIDs (deleteFriend s uid p uid'))
[PROOF STEP]
show "eqButUID s s'"
[PROOF STATE]
proof (prove)
using this:
eqButUIDf (friendIDs s) (friendIDs (deleteFriend s uid p uid'))

goal (1 subgoal):
 1. eqButUID s s'
[PROOF STEP]
using step ou
[PROOF STATE]
proof (prove)
using this:
eqButUIDf (friendIDs s) (friendIDs (deleteFriend s uid p uid'))
step s (Dact (dFriend uid p uid')) = (ou, s')
ou = outOK

goal (1 subgoal):
 1. eqButUID s s'
[PROOF STEP]
unfolding eqButUID_def
[PROOF STATE]
proof (prove)
using this:
eqButUIDf (friendIDs s) (friendIDs (deleteFriend s uid p uid'))
step s (Dact (dFriend uid p uid')) = (ou, s')
ou = outOK

goal (1 subgoal):
 1. admin s = admin s' \<and> pendingUReqs s = pendingUReqs s' \<and> userReq s = userReq s' \<and> userIDs s = userIDs s' \<and> user s = user s' \<and> pass s = pass s' \<and> eqButUIDf (pendingFReqs s) (pendingFReqs s') \<and> eqButUID12 (friendReq s) (friendReq s') \<and> eqButUIDf (friendIDs s) (friendIDs s') \<and> postIDs s = postIDs s' \<and> admin s = admin s' \<and> post s = post s' \<and> vis s = vis s' \<and> owner s = owner s' \<and> pendingSApiReqs s = pendingSApiReqs s' \<and> sApiReq s = sApiReq s' \<and> serverApiIDs s = serverApiIDs s' \<and> serverPass s = serverPass s' \<and> outerPostIDs s = outerPostIDs s' \<and> outerPost s = outerPost s' \<and> outerVis s = outerVis s' \<and> outerOwner s = outerOwner s' \<and> sentOuterFriendIDs s = sentOuterFriendIDs s' \<and> recvOuterFriendIDs s = recvOuterFriendIDs s' \<and> pendingCApiReqs s = pendingCApiReqs s' \<and> cApiReq s = cApiReq s' \<and> clientApiIDs s = clientApiIDs s' \<and> clientPass s = clientPass s' \<and> sharedWith s = sharedWith s'
[PROOF STEP]
by (auto simp add: d_defs)
[PROOF STATE]
proof (state)
this:
eqButUID s s'

goal (1 subgoal):
 1. \<lbrakk>step s (Dact (dFriend uid p uid')) = (ou, s'); reach s; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; ou \<noteq> outOK\<rbrakk> \<Longrightarrow> eqButUID s s'
[PROOF STEP]
qed (auto)


[STATEMENT]
lemma eqButUID_step:
assumes ss1: "eqButUID s s1"
and step: "step s a = (ou,s')"
and step1: "step s1 a = (ou1,s1')"
and rs: "reach s"
and rs1: "reach s1"
shows "eqButUID s' s1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqButUID s' s1'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eqButUID s' s1'
[PROOF STEP]
note simps = eqButUID_stateSelectors s_defs c_defs u_defs r_defs l_defs com_defs
[PROOF STATE]
proof (state)
this:
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> eqButUIDf (pendingFReqs ?s) (pendingFReqs ?s1.0)
eqButUID ?s ?s1.0 \<Longrightarrow> eqButUID12 (friendReq ?s) (friendReq ?s1.0)
eqButUID ?s ?s1.0 \<Longrightarrow> eqButUIDf (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> 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
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>
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>
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
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
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

goal (1 subgoal):
 1. eqButUID s' s1'
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
eqButUID s s1
step s a = (ou, s')
step s1 a = (ou1, s1')
reach s
reach s1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eqButUID s s1
step s a = (ou, s')
step s1 a = (ou1, s1')
reach s
reach s1

goal (1 subgoal):
 1. eqButUID s' s1'
[PROOF STEP]
proof (cases a)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>x1. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Sact x1\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 2. \<And>x2. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Cact x2\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 3. \<And>x3. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Dact x3\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 4. \<And>x4. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Uact x4\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 5. \<And>x5. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Ract x5\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 6. \<And>x6. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Lact x6\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 7. \<And>x7. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = COMact x7\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
case (Sact sa)
[PROOF STATE]
proof (state)
this:
a = Sact sa

goal (7 subgoals):
 1. \<And>x1. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Sact x1\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 2. \<And>x2. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Cact x2\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 3. \<And>x3. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Dact x3\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 4. \<And>x4. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Uact x4\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 5. \<And>x5. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Ract x5\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 6. \<And>x6. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Lact x6\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 7. \<And>x7. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = COMact x7\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
eqButUID s s1
step s a = (ou, s')
step s1 a = (ou1, s1')
reach s
reach s1
a = Sact sa
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eqButUID s s1
step s a = (ou, s')
step s1 a = (ou1, s1')
reach s
reach s1
a = Sact sa

goal (1 subgoal):
 1. eqButUID s' s1'
[PROOF STEP]
by (cases sa) (auto simp add: simps)
[PROOF STATE]
proof (state)
this:
eqButUID s' s1'

goal (6 subgoals):
 1. \<And>x2. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Cact x2\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 2. \<And>x3. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Dact x3\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 3. \<And>x4. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Uact x4\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 4. \<And>x5. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Ract x5\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 5. \<And>x6. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Lact x6\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 6. \<And>x7. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = COMact x7\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>x2. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Cact x2\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 2. \<And>x3. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Dact x3\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 3. \<And>x4. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Uact x4\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 4. \<And>x5. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Ract x5\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 5. \<And>x6. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Lact x6\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 6. \<And>x7. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = COMact x7\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
case (Cact ca)
[PROOF STATE]
proof (state)
this:
a = Cact ca

goal (6 subgoals):
 1. \<And>x2. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Cact x2\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 2. \<And>x3. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Dact x3\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 3. \<And>x4. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Uact x4\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 4. \<And>x5. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Ract x5\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 5. \<And>x6. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Lact x6\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 6. \<And>x7. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = COMact x7\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
note a = this
[PROOF STATE]
proof (state)
this:
a = Cact ca

goal (6 subgoals):
 1. \<And>x2. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Cact x2\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 2. \<And>x3. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Dact x3\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 3. \<And>x4. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Uact x4\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 4. \<And>x5. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Ract x5\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 5. \<And>x6. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Lact x6\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 6. \<And>x7. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = COMact x7\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
eqButUID s s1
step s a = (ou, s')
step s1 a = (ou1, s1')
reach s
reach s1
a = Cact ca
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eqButUID s s1
step s a = (ou, s')
step s1 a = (ou1, s1')
reach s
reach s1
a = Cact ca

goal (1 subgoal):
 1. eqButUID s' s1'
[PROOF STEP]
proof (cases ca)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>x11 x12. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Cact ca; ca = cNUReq x11 x12\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 2. \<And>x21 x22 x23 x24. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Cact ca; ca = cUser x21 x22 x23 x24\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 3. \<And>x31 x32 x33. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Cact ca; ca = cPost x31 x32 x33\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 4. \<And>x41 x42 x43 x44. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Cact ca; ca = cFriendReq x41 x42 x43 x44\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 5. \<And>x51 x52 x53. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Cact ca; ca = cFriend x51 x52 x53\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
case (cFriendReq uid p uid' req)
[PROOF STATE]
proof (state)
this:
ca = cFriendReq uid p uid' req

goal (5 subgoals):
 1. \<And>x11 x12. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Cact ca; ca = cNUReq x11 x12\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 2. \<And>x21 x22 x23 x24. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Cact ca; ca = cUser x21 x22 x23 x24\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 3. \<And>x31 x32 x33. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Cact ca; ca = cPost x31 x32 x33\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 4. \<And>x41 x42 x43 x44. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Cact ca; ca = cFriendReq x41 x42 x43 x44\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 5. \<And>x51 x52 x53. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Cact ca; ca = cFriend x51 x52 x53\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
note ca = this
[PROOF STATE]
proof (state)
this:
ca = cFriendReq uid p uid' req

goal (5 subgoals):
 1. \<And>x11 x12. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Cact ca; ca = cNUReq x11 x12\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 2. \<And>x21 x22 x23 x24. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Cact ca; ca = cUser x21 x22 x23 x24\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 3. \<And>x31 x32 x33. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Cact ca; ca = cPost x31 x32 x33\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 4. \<And>x41 x42 x43 x44. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Cact ca; ca = cFriendReq x41 x42 x43 x44\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 5. \<And>x51 x52 x53. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Cact ca; ca = cFriend x51 x52 x53\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ca = cFriendReq uid p uid' req
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ca = cFriendReq uid p uid' req

goal (1 subgoal):
 1. eqButUID s' s1'
[PROOF STEP]
proof (cases "(uid = UID1 \<and> uid' = UID2) \<or> (uid = UID2 \<and> uid' = UID1)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>ca = cFriendReq uid p uid' req; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 2. \<lbrakk>ca = cFriendReq uid p uid' req; \<not> (uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1)\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1

goal (2 subgoals):
 1. \<lbrakk>ca = cFriendReq uid p uid' req; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 2. \<lbrakk>ca = cFriendReq uid p uid' req; \<not> (uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1)\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1
[PROOF STEP]
have "eqButUID s s'" and "eqButUID s1 s1'"
[PROOF STATE]
proof (prove)
using this:
uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1

goal (1 subgoal):
 1. eqButUID s s' &&& eqButUID s1 s1'
[PROOF STEP]
using step step1
[PROOF STATE]
proof (prove)
using this:
uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1
step s a = (ou, s')
step s1 a = (ou1, s1')

goal (1 subgoal):
 1. eqButUID s s' &&& eqButUID s1 s1'
[PROOF STEP]
unfolding a ca
[PROOF STATE]
proof (prove)
using this:
uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1
step s (Cact (cFriendReq uid p uid' req)) = (ou, s')
step s1 (Cact (cFriendReq uid p uid' req)) = (ou1, s1')

goal (1 subgoal):
 1. eqButUID s s' &&& eqButUID s1 s1'
[PROOF STEP]
by (auto intro: Cact_cFriendReq_step_eqButUID)
[PROOF STATE]
proof (state)
this:
eqButUID s s'
eqButUID s1 s1'

goal (2 subgoals):
 1. \<lbrakk>ca = cFriendReq uid p uid' req; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 2. \<lbrakk>ca = cFriendReq uid p uid' req; \<not> (uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1)\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
with ss1
[PROOF STATE]
proof (chain)
picking this:
eqButUID s s1
eqButUID s s'
eqButUID s1 s1'
[PROOF STEP]
show "eqButUID s' s1'"
[PROOF STATE]
proof (prove)
using this:
eqButUID s s1
eqButUID s s'
eqButUID s1 s1'

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

goal (1 subgoal):
 1. \<lbrakk>ca = cFriendReq uid p uid' req; \<not> (uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1)\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>ca = cFriendReq uid p uid' req; \<not> (uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1)\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1)

goal (1 subgoal):
 1. \<lbrakk>ca = cFriendReq uid p uid' req; \<not> (uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1)\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
have fRs: "eqButUIDf (pendingFReqs s) (pendingFReqs s1)"
               and fIDs: "eqButUIDf (friendIDs s) (friendIDs s1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqButUIDf (pendingFReqs s) (pendingFReqs s1) &&& eqButUIDf (friendIDs s) (friendIDs s1)
[PROOF STEP]
using ss1
[PROOF STATE]
proof (prove)
using this:
eqButUID s s1

goal (1 subgoal):
 1. eqButUIDf (pendingFReqs s) (pendingFReqs s1) &&& eqButUIDf (friendIDs s) (friendIDs s1)
[PROOF STEP]
by (auto simp: simps)
[PROOF STATE]
proof (state)
this:
eqButUIDf (pendingFReqs s) (pendingFReqs s1)
eqButUIDf (friendIDs s) (friendIDs s1)

goal (1 subgoal):
 1. \<lbrakk>ca = cFriendReq uid p uid' req; \<not> (uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1)\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eqButUIDf (pendingFReqs s) (pendingFReqs s1)
eqButUIDf (friendIDs s) (friendIDs s1)
[PROOF STEP]
have uid_uid': "uid \<in>\<in> pendingFReqs s uid' \<longleftrightarrow> uid \<in>\<in> pendingFReqs s1 uid'"
                                  "uid \<in>\<in> friendIDs s uid' \<longleftrightarrow> uid \<in>\<in> friendIDs s1 uid'"
[PROOF STATE]
proof (prove)
using this:
eqButUIDf (pendingFReqs s) (pendingFReqs s1)
eqButUIDf (friendIDs s) (friendIDs s1)

goal (1 subgoal):
 1. (uid \<in>\<in> pendingFReqs s uid') = (uid \<in>\<in> pendingFReqs s1 uid') &&& (uid \<in>\<in> friendIDs s uid') = (uid \<in>\<in> friendIDs s1 uid')
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
eqButUIDf (pendingFReqs s) (pendingFReqs s1)
eqButUIDf (friendIDs s) (friendIDs s1)
\<not> (uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1)

goal (1 subgoal):
 1. (uid \<in>\<in> pendingFReqs s uid') = (uid \<in>\<in> pendingFReqs s1 uid') &&& (uid \<in>\<in> friendIDs s uid') = (uid \<in>\<in> friendIDs s1 uid')
[PROOF STEP]
by (auto intro!: eqButUIDf_not_UID')
[PROOF STATE]
proof (state)
this:
(uid \<in>\<in> pendingFReqs s uid') = (uid \<in>\<in> pendingFReqs s1 uid')
(uid \<in>\<in> friendIDs s uid') = (uid \<in>\<in> friendIDs s1 uid')

goal (1 subgoal):
 1. \<lbrakk>ca = cFriendReq uid p uid' req; \<not> (uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1)\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
have "eqButUIDf ((pendingFReqs s)(uid' := pendingFReqs s uid' ## uid))
                              ((pendingFReqs s1)(uid' := pendingFReqs s1 uid' ## uid))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqButUIDf ((pendingFReqs s)(uid' := pendingFReqs s uid' ## uid)) ((pendingFReqs s1)(uid' := pendingFReqs s1 uid' ## uid))
[PROOF STEP]
using fRs False
[PROOF STATE]
proof (prove)
using this:
eqButUIDf (pendingFReqs s) (pendingFReqs s1)
\<not> (uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1)

goal (1 subgoal):
 1. eqButUIDf ((pendingFReqs s)(uid' := pendingFReqs s uid' ## uid)) ((pendingFReqs s1)(uid' := pendingFReqs s1 uid' ## uid))
[PROOF STEP]
by (intro eqButUIDf_cong) (auto simp add: remove1_append remove1_idem eqButUIDf_def)
[PROOF STATE]
proof (state)
this:
eqButUIDf ((pendingFReqs s)(uid' := pendingFReqs s uid' ## uid)) ((pendingFReqs s1)(uid' := pendingFReqs s1 uid' ## uid))

goal (1 subgoal):
 1. \<lbrakk>ca = cFriendReq uid p uid' req; \<not> (uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1)\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
eqButUIDf ((pendingFReqs s)(uid' := pendingFReqs s uid' ## uid)) ((pendingFReqs s1)(uid' := pendingFReqs s1 uid' ## uid))

goal (1 subgoal):
 1. \<lbrakk>ca = cFriendReq uid p uid' req; \<not> (uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1)\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
have "eqButUID12 (fun_upd2 (friendReq s) uid uid' req)
                                        (fun_upd2 (friendReq s1) uid uid' req)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqButUID12 (fun_upd2 (friendReq s) uid uid' req) (fun_upd2 (friendReq s1) uid uid' req)
[PROOF STEP]
using ss1
[PROOF STATE]
proof (prove)
using this:
eqButUID s s1

goal (1 subgoal):
 1. eqButUID12 (fun_upd2 (friendReq s) uid uid' req) (fun_upd2 (friendReq s1) uid uid' req)
[PROOF STEP]
by (intro eqButUID12_cong) (auto simp: simps)
[PROOF STATE]
proof (state)
this:
eqButUID12 (fun_upd2 (friendReq s) uid uid' req) (fun_upd2 (friendReq s1) uid uid' req)

goal (1 subgoal):
 1. \<lbrakk>ca = cFriendReq uid p uid' req; \<not> (uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1)\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
eqButUID12 (fun_upd2 (friendReq s) uid uid' req) (fun_upd2 (friendReq s1) uid uid' req)

goal (1 subgoal):
 1. \<lbrakk>ca = cFriendReq uid p uid' req; \<not> (uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1)\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
have "e_createFriendReq s uid p uid' req
                         \<longleftrightarrow> e_createFriendReq s1 uid p uid' req"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e_createFriendReq s uid p uid' req = e_createFriendReq s1 uid p uid' req
[PROOF STEP]
using uid_uid' ss1
[PROOF STATE]
proof (prove)
using this:
(uid \<in>\<in> pendingFReqs s uid') = (uid \<in>\<in> pendingFReqs s1 uid')
(uid \<in>\<in> friendIDs s uid') = (uid \<in>\<in> friendIDs s1 uid')
eqButUID s s1

goal (1 subgoal):
 1. e_createFriendReq s uid p uid' req = e_createFriendReq s1 uid p uid' req
[PROOF STEP]
by (auto simp: simps)
[PROOF STATE]
proof (state)
this:
e_createFriendReq s uid p uid' req = e_createFriendReq s1 uid p uid' req

goal (1 subgoal):
 1. \<lbrakk>ca = cFriendReq uid p uid' req; \<not> (uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1)\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
eqButUIDf ((pendingFReqs s)(uid' := pendingFReqs s uid' ## uid)) ((pendingFReqs s1)(uid' := pendingFReqs s1 uid' ## uid))
eqButUID12 (fun_upd2 (friendReq s) uid uid' req) (fun_upd2 (friendReq s1) uid uid' req)
e_createFriendReq s uid p uid' req = e_createFriendReq s1 uid p uid' req
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eqButUIDf ((pendingFReqs s)(uid' := pendingFReqs s uid' ## uid)) ((pendingFReqs s1)(uid' := pendingFReqs s1 uid' ## uid))
eqButUID12 (fun_upd2 (friendReq s) uid uid' req) (fun_upd2 (friendReq s1) uid uid' req)
e_createFriendReq s uid p uid' req = e_createFriendReq s1 uid p uid' req

goal (1 subgoal):
 1. eqButUID s' s1'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
eqButUIDf ((pendingFReqs s)(uid' := pendingFReqs s uid' ## uid)) ((pendingFReqs s1)(uid' := pendingFReqs s1 uid' ## uid))
eqButUID12 (fun_upd2 (friendReq s) uid uid' req) (fun_upd2 (friendReq s1) uid uid' req)
e_createFriendReq s uid p uid' req = e_createFriendReq s1 uid p uid' req
eqButUID s s1
step s a = (ou, s')
step s1 a = (ou1, s1')
reach s
reach s1

goal (1 subgoal):
 1. eqButUID s' s1'
[PROOF STEP]
unfolding a ca
[PROOF STATE]
proof (prove)
using this:
eqButUIDf ((pendingFReqs s)(uid' := pendingFReqs s uid' ## uid)) ((pendingFReqs s1)(uid' := pendingFReqs s1 uid' ## uid))
eqButUID12 (fun_upd2 (friendReq s) uid uid' req) (fun_upd2 (friendReq s1) uid uid' req)
e_createFriendReq s uid p uid' req = e_createFriendReq s1 uid p uid' req
eqButUID s s1
step s (Cact (cFriendReq uid p uid' req)) = (ou, s')
step s1 (Cact (cFriendReq uid p uid' req)) = (ou1, s1')
reach s
reach s1

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
eqButUID s' s1'

goal (4 subgoals):
 1. \<And>x11 x12. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Cact ca; ca = cNUReq x11 x12\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 2. \<And>x21 x22 x23 x24. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Cact ca; ca = cUser x21 x22 x23 x24\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 3. \<And>x31 x32 x33. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Cact ca; ca = cPost x31 x32 x33\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 4. \<And>x51 x52 x53. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Cact ca; ca = cFriend x51 x52 x53\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x11 x12. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Cact ca; ca = cNUReq x11 x12\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 2. \<And>x21 x22 x23 x24. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Cact ca; ca = cUser x21 x22 x23 x24\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 3. \<And>x31 x32 x33. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Cact ca; ca = cPost x31 x32 x33\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 4. \<And>x51 x52 x53. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Cact ca; ca = cFriend x51 x52 x53\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
case (cFriend uid p uid')
[PROOF STATE]
proof (state)
this:
ca = cFriend uid p uid'

goal (4 subgoals):
 1. \<And>x11 x12. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Cact ca; ca = cNUReq x11 x12\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 2. \<And>x21 x22 x23 x24. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Cact ca; ca = cUser x21 x22 x23 x24\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 3. \<And>x31 x32 x33. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Cact ca; ca = cPost x31 x32 x33\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 4. \<And>x51 x52 x53. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Cact ca; ca = cFriend x51 x52 x53\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
note ca = this
[PROOF STATE]
proof (state)
this:
ca = cFriend uid p uid'

goal (4 subgoals):
 1. \<And>x11 x12. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Cact ca; ca = cNUReq x11 x12\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 2. \<And>x21 x22 x23 x24. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Cact ca; ca = cUser x21 x22 x23 x24\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 3. \<And>x31 x32 x33. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Cact ca; ca = cPost x31 x32 x33\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 4. \<And>x51 x52 x53. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Cact ca; ca = cFriend x51 x52 x53\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ca = cFriend uid p uid'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ca = cFriend uid p uid'

goal (1 subgoal):
 1. eqButUID s' s1'
[PROOF STEP]
proof (cases "(uid = UID1 \<and> uid' = UID2) \<or> (uid = UID2 \<and> uid' = UID1)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>ca = cFriend uid p uid'; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 2. \<lbrakk>ca = cFriend uid p uid'; \<not> (uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1)\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1

goal (2 subgoals):
 1. \<lbrakk>ca = cFriend uid p uid'; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 2. \<lbrakk>ca = cFriend uid p uid'; \<not> (uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1)\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1
[PROOF STEP]
have "eqButUID s s'" and "eqButUID s1 s1'"
[PROOF STATE]
proof (prove)
using this:
uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1

goal (1 subgoal):
 1. eqButUID s s' &&& eqButUID s1 s1'
[PROOF STEP]
using step step1 rs rs1
[PROOF STATE]
proof (prove)
using this:
uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1
step s a = (ou, s')
step s1 a = (ou1, s1')
reach s
reach s1

goal (1 subgoal):
 1. eqButUID s s' &&& eqButUID s1 s1'
[PROOF STEP]
unfolding a ca
[PROOF STATE]
proof (prove)
using this:
uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1
step s (Cact (cFriend uid p uid')) = (ou, s')
step s1 (Cact (cFriend uid p uid')) = (ou1, s1')
reach s
reach s1

goal (1 subgoal):
 1. eqButUID s s' &&& eqButUID s1 s1'
[PROOF STEP]
by (auto intro!: Cact_cFriend_step_eqButUID)+
[PROOF STATE]
proof (state)
this:
eqButUID s s'
eqButUID s1 s1'

goal (2 subgoals):
 1. \<lbrakk>ca = cFriend uid p uid'; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 2. \<lbrakk>ca = cFriend uid p uid'; \<not> (uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1)\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
with ss1
[PROOF STATE]
proof (chain)
picking this:
eqButUID s s1
eqButUID s s'
eqButUID s1 s1'
[PROOF STEP]
show "eqButUID s' s1'"
[PROOF STATE]
proof (prove)
using this:
eqButUID s s1
eqButUID s s'
eqButUID s1 s1'

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

goal (1 subgoal):
 1. \<lbrakk>ca = cFriend uid p uid'; \<not> (uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1)\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>ca = cFriend uid p uid'; \<not> (uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1)\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1)

goal (1 subgoal):
 1. \<lbrakk>ca = cFriend uid p uid'; \<not> (uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1)\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
have fRs: "eqButUIDf (pendingFReqs s) (pendingFReqs s1)"
                    (is "eqButUIDf (?pfr s) (?pfr s1)")
               and fIDs: "eqButUIDf (friendIDs s) (friendIDs s1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqButUIDf (pendingFReqs s) (pendingFReqs s1) &&& eqButUIDf (friendIDs s) (friendIDs s1)
[PROOF STEP]
using ss1
[PROOF STATE]
proof (prove)
using this:
eqButUID s s1

goal (1 subgoal):
 1. eqButUIDf (pendingFReqs s) (pendingFReqs s1) &&& eqButUIDf (friendIDs s) (friendIDs s1)
[PROOF STEP]
by (auto simp: simps)
[PROOF STATE]
proof (state)
this:
eqButUIDf (pendingFReqs s) (pendingFReqs s1)
eqButUIDf (friendIDs s) (friendIDs s1)

goal (1 subgoal):
 1. \<lbrakk>ca = cFriend uid p uid'; \<not> (uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1)\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eqButUIDf (pendingFReqs s) (pendingFReqs s1)
eqButUIDf (friendIDs s) (friendIDs s1)
[PROOF STEP]
have uid_uid': "uid \<in>\<in> pendingFReqs s uid' \<longleftrightarrow> uid \<in>\<in> pendingFReqs s1 uid'"
                                  "uid' \<in>\<in> pendingFReqs s uid \<longleftrightarrow> uid' \<in>\<in> pendingFReqs s1 uid"
                                  "uid \<in>\<in> friendIDs s uid' \<longleftrightarrow> uid \<in>\<in> friendIDs s1 uid'"
                                  "uid' \<in>\<in> friendIDs s uid \<longleftrightarrow> uid' \<in>\<in> friendIDs s1 uid"
[PROOF STATE]
proof (prove)
using this:
eqButUIDf (pendingFReqs s) (pendingFReqs s1)
eqButUIDf (friendIDs s) (friendIDs s1)

goal (1 subgoal):
 1. ((uid \<in>\<in> pendingFReqs s uid') = (uid \<in>\<in> pendingFReqs s1 uid') &&& (uid' \<in>\<in> pendingFReqs s uid) = (uid' \<in>\<in> pendingFReqs s1 uid)) &&& (uid \<in>\<in> friendIDs s uid') = (uid \<in>\<in> friendIDs s1 uid') &&& (uid' \<in>\<in> friendIDs s uid) = (uid' \<in>\<in> friendIDs s1 uid)
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
eqButUIDf (pendingFReqs s) (pendingFReqs s1)
eqButUIDf (friendIDs s) (friendIDs s1)
\<not> (uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1)

goal (1 subgoal):
 1. ((uid \<in>\<in> pendingFReqs s uid') = (uid \<in>\<in> pendingFReqs s1 uid') &&& (uid' \<in>\<in> pendingFReqs s uid) = (uid' \<in>\<in> pendingFReqs s1 uid)) &&& (uid \<in>\<in> friendIDs s uid') = (uid \<in>\<in> friendIDs s1 uid') &&& (uid' \<in>\<in> friendIDs s uid) = (uid' \<in>\<in> friendIDs s1 uid)
[PROOF STEP]
by (auto intro!: eqButUIDf_not_UID')
[PROOF STATE]
proof (state)
this:
(uid \<in>\<in> pendingFReqs s uid') = (uid \<in>\<in> pendingFReqs s1 uid')
(uid' \<in>\<in> pendingFReqs s uid) = (uid' \<in>\<in> pendingFReqs s1 uid)
(uid \<in>\<in> friendIDs s uid') = (uid \<in>\<in> friendIDs s1 uid')
(uid' \<in>\<in> friendIDs s uid) = (uid' \<in>\<in> friendIDs s1 uid)

goal (1 subgoal):
 1. \<lbrakk>ca = cFriend uid p uid'; \<not> (uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1)\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
have "eqButUIDl UID1 (remove1 uid' (?pfr s UID2)) (remove1 uid' (?pfr s1 UID2))"
               and "eqButUIDl UID2 (remove1 uid' (?pfr s UID1)) (remove1 uid' (?pfr s1 UID1))"
               and "eqButUIDl UID1 (remove1 uid (?pfr s UID2)) (remove1 uid (?pfr s1 UID2))"
               and "eqButUIDl UID2 (remove1 uid (?pfr s UID1)) (remove1 uid (?pfr s1 UID1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (eqButUIDl UID1 (remove1 uid' (pendingFReqs s UID2)) (remove1 uid' (pendingFReqs s1 UID2)) &&& eqButUIDl UID2 (remove1 uid' (pendingFReqs s UID1)) (remove1 uid' (pendingFReqs s1 UID1))) &&& eqButUIDl UID1 (remove1 uid (pendingFReqs s UID2)) (remove1 uid (pendingFReqs s1 UID2)) &&& eqButUIDl UID2 (remove1 uid (pendingFReqs s UID1)) (remove1 uid (pendingFReqs s1 UID1))
[PROOF STEP]
using fRs
[PROOF STATE]
proof (prove)
using this:
eqButUIDf (pendingFReqs s) (pendingFReqs s1)

goal (1 subgoal):
 1. (eqButUIDl UID1 (remove1 uid' (pendingFReqs s UID2)) (remove1 uid' (pendingFReqs s1 UID2)) &&& eqButUIDl UID2 (remove1 uid' (pendingFReqs s UID1)) (remove1 uid' (pendingFReqs s1 UID1))) &&& eqButUIDl UID1 (remove1 uid (pendingFReqs s UID2)) (remove1 uid (pendingFReqs s1 UID2)) &&& eqButUIDl UID2 (remove1 uid (pendingFReqs s UID1)) (remove1 uid (pendingFReqs s1 UID1))
[PROOF STEP]
unfolding eqButUIDf_def
[PROOF STATE]
proof (prove)
using this:
eqButUIDl UID2 (pendingFReqs s UID1) (pendingFReqs s1 UID1) \<and> eqButUIDl UID1 (pendingFReqs s UID2) (pendingFReqs s1 UID2) \<and> (\<forall>uid. uid \<noteq> UID1 \<and> uid \<noteq> UID2 \<longrightarrow> pendingFReqs s uid = pendingFReqs s1 uid)

goal (1 subgoal):
 1. (eqButUIDl UID1 (remove1 uid' (pendingFReqs s UID2)) (remove1 uid' (pendingFReqs s1 UID2)) &&& eqButUIDl UID2 (remove1 uid' (pendingFReqs s UID1)) (remove1 uid' (pendingFReqs s1 UID1))) &&& eqButUIDl UID1 (remove1 uid (pendingFReqs s UID2)) (remove1 uid (pendingFReqs s1 UID2)) &&& eqButUIDl UID2 (remove1 uid (pendingFReqs s UID1)) (remove1 uid (pendingFReqs s1 UID1))
[PROOF STEP]
by (auto intro!: eqButUIDl_remove1_cong simp del: eqButUIDl.simps)
[PROOF STATE]
proof (state)
this:
eqButUIDl UID1 (remove1 uid' (pendingFReqs s UID2)) (remove1 uid' (pendingFReqs s1 UID2))
eqButUIDl UID2 (remove1 uid' (pendingFReqs s UID1)) (remove1 uid' (pendingFReqs s1 UID1))
eqButUIDl UID1 (remove1 uid (pendingFReqs s UID2)) (remove1 uid (pendingFReqs s1 UID2))
eqButUIDl UID2 (remove1 uid (pendingFReqs s UID1)) (remove1 uid (pendingFReqs s1 UID1))

goal (1 subgoal):
 1. \<lbrakk>ca = cFriend uid p uid'; \<not> (uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1)\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eqButUIDl UID1 (remove1 uid' (pendingFReqs s UID2)) (remove1 uid' (pendingFReqs s1 UID2))
eqButUIDl UID2 (remove1 uid' (pendingFReqs s UID1)) (remove1 uid' (pendingFReqs s1 UID1))
eqButUIDl UID1 (remove1 uid (pendingFReqs s UID2)) (remove1 uid (pendingFReqs s1 UID2))
eqButUIDl UID2 (remove1 uid (pendingFReqs s UID1)) (remove1 uid (pendingFReqs s1 UID1))
[PROOF STEP]
have 1: "eqButUIDf ((?pfr s)(uid := remove1 uid' (?pfr s uid),
                                                uid' := remove1 uid (?pfr s uid')))
                                     ((?pfr s1)(uid := remove1 uid' (?pfr s1 uid),
                                                uid' := remove1 uid (?pfr s1 uid')))"
[PROOF STATE]
proof (prove)
using this:
eqButUIDl UID1 (remove1 uid' (pendingFReqs s UID2)) (remove1 uid' (pendingFReqs s1 UID2))
eqButUIDl UID2 (remove1 uid' (pendingFReqs s UID1)) (remove1 uid' (pendingFReqs s1 UID1))
eqButUIDl UID1 (remove1 uid (pendingFReqs s UID2)) (remove1 uid (pendingFReqs s1 UID2))
eqButUIDl UID2 (remove1 uid (pendingFReqs s UID1)) (remove1 uid (pendingFReqs s1 UID1))

goal (1 subgoal):
 1. eqButUIDf ((pendingFReqs s)(uid := remove1 uid' (pendingFReqs s uid), uid' := remove1 uid (pendingFReqs s uid'))) ((pendingFReqs s1)(uid := remove1 uid' (pendingFReqs s1 uid), uid' := remove1 uid (pendingFReqs s1 uid')))
[PROOF STEP]
using fRs False
[PROOF STATE]
proof (prove)
using this:
eqButUIDl UID1 (remove1 uid' (pendingFReqs s UID2)) (remove1 uid' (pendingFReqs s1 UID2))
eqButUIDl UID2 (remove1 uid' (pendingFReqs s UID1)) (remove1 uid' (pendingFReqs s1 UID1))
eqButUIDl UID1 (remove1 uid (pendingFReqs s UID2)) (remove1 uid (pendingFReqs s1 UID2))
eqButUIDl UID2 (remove1 uid (pendingFReqs s UID1)) (remove1 uid (pendingFReqs s1 UID1))
eqButUIDf (pendingFReqs s) (pendingFReqs s1)
\<not> (uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1)

goal (1 subgoal):
 1. eqButUIDf ((pendingFReqs s)(uid := remove1 uid' (pendingFReqs s uid), uid' := remove1 uid (pendingFReqs s uid'))) ((pendingFReqs s1)(uid := remove1 uid' (pendingFReqs s1 uid), uid' := remove1 uid (pendingFReqs s1 uid')))
[PROOF STEP]
by (intro eqButUIDf_cong) (auto simp add: eqButUIDf_def)
[PROOF STATE]
proof (state)
this:
eqButUIDf ((pendingFReqs s)(uid := remove1 uid' (pendingFReqs s uid), uid' := remove1 uid (pendingFReqs s uid'))) ((pendingFReqs s1)(uid := remove1 uid' (pendingFReqs s1 uid), uid' := remove1 uid (pendingFReqs s1 uid')))

goal (1 subgoal):
 1. \<lbrakk>ca = cFriend uid p uid'; \<not> (uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1)\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
have "uid = UID1 \<Longrightarrow> eqButUIDl UID2 (friendIDs s UID1 ## uid') (friendIDs s1 UID1 ## uid')"
               and "uid = UID2 \<Longrightarrow> eqButUIDl UID1 (friendIDs s UID2 ## uid') (friendIDs s1 UID2 ## uid')"
               and "uid' = UID1 \<Longrightarrow> eqButUIDl UID2 (friendIDs s UID1 ## uid) (friendIDs s1 UID1 ## uid)"
               and "uid' = UID2 \<Longrightarrow> eqButUIDl UID1 (friendIDs s UID2 ## uid) (friendIDs s1 UID2 ## uid)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((uid = UID1 \<Longrightarrow> eqButUIDl UID2 (friendIDs s UID1 ## uid') (friendIDs s1 UID1 ## uid')) &&& (uid = UID2 \<Longrightarrow> eqButUIDl UID1 (friendIDs s UID2 ## uid') (friendIDs s1 UID2 ## uid'))) &&& (uid' = UID1 \<Longrightarrow> eqButUIDl UID2 (friendIDs s UID1 ## uid) (friendIDs s1 UID1 ## uid)) &&& (uid' = UID2 \<Longrightarrow> eqButUIDl UID1 (friendIDs s UID2 ## uid) (friendIDs s1 UID2 ## uid))
[PROOF STEP]
using fIDs uid_uid'
[PROOF STATE]
proof (prove)
using this:
eqButUIDf (friendIDs s) (friendIDs s1)
(uid \<in>\<in> pendingFReqs s uid') = (uid \<in>\<in> pendingFReqs s1 uid')
(uid' \<in>\<in> pendingFReqs s uid) = (uid' \<in>\<in> pendingFReqs s1 uid)
(uid \<in>\<in> friendIDs s uid') = (uid \<in>\<in> friendIDs s1 uid')
(uid' \<in>\<in> friendIDs s uid) = (uid' \<in>\<in> friendIDs s1 uid)

goal (1 subgoal):
 1. ((uid = UID1 \<Longrightarrow> eqButUIDl UID2 (friendIDs s UID1 ## uid') (friendIDs s1 UID1 ## uid')) &&& (uid = UID2 \<Longrightarrow> eqButUIDl UID1 (friendIDs s UID2 ## uid') (friendIDs s1 UID2 ## uid'))) &&& (uid' = UID1 \<Longrightarrow> eqButUIDl UID2 (friendIDs s UID1 ## uid) (friendIDs s1 UID1 ## uid)) &&& (uid' = UID2 \<Longrightarrow> eqButUIDl UID1 (friendIDs s UID2 ## uid) (friendIDs s1 UID2 ## uid))
[PROOF STEP]
by - (intro eqButUIDl_snoc_cong; simp add: eqButUIDf_def)+
[PROOF STATE]
proof (state)
this:
uid = UID1 \<Longrightarrow> eqButUIDl UID2 (friendIDs s UID1 ## uid') (friendIDs s1 UID1 ## uid')
uid = UID2 \<Longrightarrow> eqButUIDl UID1 (friendIDs s UID2 ## uid') (friendIDs s1 UID2 ## uid')
uid' = UID1 \<Longrightarrow> eqButUIDl UID2 (friendIDs s UID1 ## uid) (friendIDs s1 UID1 ## uid)
uid' = UID2 \<Longrightarrow> eqButUIDl UID1 (friendIDs s UID2 ## uid) (friendIDs s1 UID2 ## uid)

goal (1 subgoal):
 1. \<lbrakk>ca = cFriend uid p uid'; \<not> (uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1)\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
uid = UID1 \<Longrightarrow> eqButUIDl UID2 (friendIDs s UID1 ## uid') (friendIDs s1 UID1 ## uid')
uid = UID2 \<Longrightarrow> eqButUIDl UID1 (friendIDs s UID2 ## uid') (friendIDs s1 UID2 ## uid')
uid' = UID1 \<Longrightarrow> eqButUIDl UID2 (friendIDs s UID1 ## uid) (friendIDs s1 UID1 ## uid)
uid' = UID2 \<Longrightarrow> eqButUIDl UID1 (friendIDs s UID2 ## uid) (friendIDs s1 UID2 ## uid)
[PROOF STEP]
have 2: "eqButUIDf ((friendIDs s)(uid := friendIDs s uid ## uid',
                                                      uid' := friendIDs s uid' ## uid))
                                       ((friendIDs s1)(uid := friendIDs s1 uid ## uid',
                                                       uid' := friendIDs s1 uid' ## uid))"
[PROOF STATE]
proof (prove)
using this:
uid = UID1 \<Longrightarrow> eqButUIDl UID2 (friendIDs s UID1 ## uid') (friendIDs s1 UID1 ## uid')
uid = UID2 \<Longrightarrow> eqButUIDl UID1 (friendIDs s UID2 ## uid') (friendIDs s1 UID2 ## uid')
uid' = UID1 \<Longrightarrow> eqButUIDl UID2 (friendIDs s UID1 ## uid) (friendIDs s1 UID1 ## uid)
uid' = UID2 \<Longrightarrow> eqButUIDl UID1 (friendIDs s UID2 ## uid) (friendIDs s1 UID2 ## uid)

goal (1 subgoal):
 1. eqButUIDf ((friendIDs s)(uid := friendIDs s uid ## uid', uid' := friendIDs s uid' ## uid)) ((friendIDs s1)(uid := friendIDs s1 uid ## uid', uid' := friendIDs s1 uid' ## uid))
[PROOF STEP]
using fIDs
[PROOF STATE]
proof (prove)
using this:
uid = UID1 \<Longrightarrow> eqButUIDl UID2 (friendIDs s UID1 ## uid') (friendIDs s1 UID1 ## uid')
uid = UID2 \<Longrightarrow> eqButUIDl UID1 (friendIDs s UID2 ## uid') (friendIDs s1 UID2 ## uid')
uid' = UID1 \<Longrightarrow> eqButUIDl UID2 (friendIDs s UID1 ## uid) (friendIDs s1 UID1 ## uid)
uid' = UID2 \<Longrightarrow> eqButUIDl UID1 (friendIDs s UID2 ## uid) (friendIDs s1 UID2 ## uid)
eqButUIDf (friendIDs s) (friendIDs s1)

goal (1 subgoal):
 1. eqButUIDf ((friendIDs s)(uid := friendIDs s uid ## uid', uid' := friendIDs s uid' ## uid)) ((friendIDs s1)(uid := friendIDs s1 uid ## uid', uid' := friendIDs s1 uid' ## uid))
[PROOF STEP]
by (intro eqButUIDf_cong) (auto simp add: eqButUIDf_def)
[PROOF STATE]
proof (state)
this:
eqButUIDf ((friendIDs s)(uid := friendIDs s uid ## uid', uid' := friendIDs s uid' ## uid)) ((friendIDs s1)(uid := friendIDs s1 uid ## uid', uid' := friendIDs s1 uid' ## uid))

goal (1 subgoal):
 1. \<lbrakk>ca = cFriend uid p uid'; \<not> (uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1)\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
have 3: "eqButUID12 (fun_upd2 (fun_upd2 (friendReq s) uid' uid emptyRequestInfo)
                                                                    uid uid' emptyRequestInfo)
                                  (fun_upd2 (fun_upd2 (friendReq s1) uid' uid emptyRequestInfo)
                                                                     uid uid' emptyRequestInfo)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqButUID12 (fun_upd2 (fun_upd2 (friendReq s) uid' uid emptyRequestInfo) uid uid' emptyRequestInfo) (fun_upd2 (fun_upd2 (friendReq s1) uid' uid emptyRequestInfo) uid uid' emptyRequestInfo)
[PROOF STEP]
using ss1
[PROOF STATE]
proof (prove)
using this:
eqButUID s s1

goal (1 subgoal):
 1. eqButUID12 (fun_upd2 (fun_upd2 (friendReq s) uid' uid emptyRequestInfo) uid uid' emptyRequestInfo) (fun_upd2 (fun_upd2 (friendReq s1) uid' uid emptyRequestInfo) uid uid' emptyRequestInfo)
[PROOF STEP]
by (intro eqButUID12_cong) (auto simp: simps)
[PROOF STATE]
proof (state)
this:
eqButUID12 (fun_upd2 (fun_upd2 (friendReq s) uid' uid emptyRequestInfo) uid uid' emptyRequestInfo) (fun_upd2 (fun_upd2 (friendReq s1) uid' uid emptyRequestInfo) uid uid' emptyRequestInfo)

goal (1 subgoal):
 1. \<lbrakk>ca = cFriend uid p uid'; \<not> (uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1)\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
have "e_createFriend s uid p uid'
                \<longleftrightarrow> e_createFriend s1 uid p uid'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e_createFriend s uid p uid' = e_createFriend s1 uid p uid'
[PROOF STEP]
using uid_uid' ss1
[PROOF STATE]
proof (prove)
using this:
(uid \<in>\<in> pendingFReqs s uid') = (uid \<in>\<in> pendingFReqs s1 uid')
(uid' \<in>\<in> pendingFReqs s uid) = (uid' \<in>\<in> pendingFReqs s1 uid)
(uid \<in>\<in> friendIDs s uid') = (uid \<in>\<in> friendIDs s1 uid')
(uid' \<in>\<in> friendIDs s uid) = (uid' \<in>\<in> friendIDs s1 uid)
eqButUID s s1

goal (1 subgoal):
 1. e_createFriend s uid p uid' = e_createFriend s1 uid p uid'
[PROOF STEP]
by (auto simp: simps)
[PROOF STATE]
proof (state)
this:
e_createFriend s uid p uid' = e_createFriend s1 uid p uid'

goal (1 subgoal):
 1. \<lbrakk>ca = cFriend uid p uid'; \<not> (uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1)\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
with 1 2 3
[PROOF STATE]
proof (chain)
picking this:
eqButUIDf ((pendingFReqs s)(uid := remove1 uid' (pendingFReqs s uid), uid' := remove1 uid (pendingFReqs s uid'))) ((pendingFReqs s1)(uid := remove1 uid' (pendingFReqs s1 uid), uid' := remove1 uid (pendingFReqs s1 uid')))
eqButUIDf ((friendIDs s)(uid := friendIDs s uid ## uid', uid' := friendIDs s uid' ## uid)) ((friendIDs s1)(uid := friendIDs s1 uid ## uid', uid' := friendIDs s1 uid' ## uid))
eqButUID12 (fun_upd2 (fun_upd2 (friendReq s) uid' uid emptyRequestInfo) uid uid' emptyRequestInfo) (fun_upd2 (fun_upd2 (friendReq s1) uid' uid emptyRequestInfo) uid uid' emptyRequestInfo)
e_createFriend s uid p uid' = e_createFriend s1 uid p uid'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eqButUIDf ((pendingFReqs s)(uid := remove1 uid' (pendingFReqs s uid), uid' := remove1 uid (pendingFReqs s uid'))) ((pendingFReqs s1)(uid := remove1 uid' (pendingFReqs s1 uid), uid' := remove1 uid (pendingFReqs s1 uid')))
eqButUIDf ((friendIDs s)(uid := friendIDs s uid ## uid', uid' := friendIDs s uid' ## uid)) ((friendIDs s1)(uid := friendIDs s1 uid ## uid', uid' := friendIDs s1 uid' ## uid))
eqButUID12 (fun_upd2 (fun_upd2 (friendReq s) uid' uid emptyRequestInfo) uid uid' emptyRequestInfo) (fun_upd2 (fun_upd2 (friendReq s1) uid' uid emptyRequestInfo) uid uid' emptyRequestInfo)
e_createFriend s uid p uid' = e_createFriend s1 uid p uid'

goal (1 subgoal):
 1. eqButUID s' s1'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
eqButUIDf ((pendingFReqs s)(uid := remove1 uid' (pendingFReqs s uid), uid' := remove1 uid (pendingFReqs s uid'))) ((pendingFReqs s1)(uid := remove1 uid' (pendingFReqs s1 uid), uid' := remove1 uid (pendingFReqs s1 uid')))
eqButUIDf ((friendIDs s)(uid := friendIDs s uid ## uid', uid' := friendIDs s uid' ## uid)) ((friendIDs s1)(uid := friendIDs s1 uid ## uid', uid' := friendIDs s1 uid' ## uid))
eqButUID12 (fun_upd2 (fun_upd2 (friendReq s) uid' uid emptyRequestInfo) uid uid' emptyRequestInfo) (fun_upd2 (fun_upd2 (friendReq s1) uid' uid emptyRequestInfo) uid uid' emptyRequestInfo)
e_createFriend s uid p uid' = e_createFriend s1 uid p uid'
eqButUID s s1
step s a = (ou, s')
step s1 a = (ou1, s1')
reach s
reach s1

goal (1 subgoal):
 1. eqButUID s' s1'
[PROOF STEP]
unfolding a ca
[PROOF STATE]
proof (prove)
using this:
eqButUIDf ((pendingFReqs s)(uid := remove1 uid' (pendingFReqs s uid), uid' := remove1 uid (pendingFReqs s uid'))) ((pendingFReqs s1)(uid := remove1 uid' (pendingFReqs s1 uid), uid' := remove1 uid (pendingFReqs s1 uid')))
eqButUIDf ((friendIDs s)(uid := friendIDs s uid ## uid', uid' := friendIDs s uid' ## uid)) ((friendIDs s1)(uid := friendIDs s1 uid ## uid', uid' := friendIDs s1 uid' ## uid))
eqButUID12 (fun_upd2 (fun_upd2 (friendReq s) uid' uid emptyRequestInfo) uid uid' emptyRequestInfo) (fun_upd2 (fun_upd2 (friendReq s1) uid' uid emptyRequestInfo) uid uid' emptyRequestInfo)
e_createFriend s uid p uid' = e_createFriend s1 uid p uid'
eqButUID s s1
step s (Cact (cFriend uid p uid')) = (ou, s')
step s1 (Cact (cFriend uid p uid')) = (ou1, s1')
reach s
reach s1

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
eqButUID s' s1'

goal (3 subgoals):
 1. \<And>x11 x12. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Cact ca; ca = cNUReq x11 x12\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 2. \<And>x21 x22 x23 x24. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Cact ca; ca = cUser x21 x22 x23 x24\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 3. \<And>x31 x32 x33. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Cact ca; ca = cPost x31 x32 x33\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
qed (auto simp: simps)
[PROOF STATE]
proof (state)
this:
eqButUID s' s1'

goal (5 subgoals):
 1. \<And>x3. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Dact x3\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 2. \<And>x4. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Uact x4\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 3. \<And>x5. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Ract x5\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 4. \<And>x6. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Lact x6\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 5. \<And>x7. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = COMact x7\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>x3. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Dact x3\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 2. \<And>x4. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Uact x4\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 3. \<And>x5. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Ract x5\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 4. \<And>x6. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Lact x6\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 5. \<And>x7. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = COMact x7\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
case (Uact ua)
[PROOF STATE]
proof (state)
this:
a = Uact ua

goal (5 subgoals):
 1. \<And>x3. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Dact x3\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 2. \<And>x4. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Uact x4\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 3. \<And>x5. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Ract x5\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 4. \<And>x6. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Lact x6\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 5. \<And>x7. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = COMact x7\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
eqButUID s s1
step s a = (ou, s')
step s1 a = (ou1, s1')
reach s
reach s1
a = Uact ua
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eqButUID s s1
step s a = (ou, s')
step s1 a = (ou1, s1')
reach s
reach s1
a = Uact ua

goal (1 subgoal):
 1. eqButUID s' s1'
[PROOF STEP]
by (cases ua) (auto simp add: simps)
[PROOF STATE]
proof (state)
this:
eqButUID s' s1'

goal (4 subgoals):
 1. \<And>x3. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Dact x3\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 2. \<And>x5. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Ract x5\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 3. \<And>x6. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Lact x6\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 4. \<And>x7. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = COMact x7\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x3. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Dact x3\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 2. \<And>x5. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Ract x5\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 3. \<And>x6. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Lact x6\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 4. \<And>x7. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = COMact x7\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
case (Ract ra)
[PROOF STATE]
proof (state)
this:
a = Ract ra

goal (4 subgoals):
 1. \<And>x3. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Dact x3\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 2. \<And>x5. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Ract x5\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 3. \<And>x6. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Lact x6\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 4. \<And>x7. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = COMact x7\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
eqButUID s s1
step s a = (ou, s')
step s1 a = (ou1, s1')
reach s
reach s1
a = Ract ra
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eqButUID s s1
step s a = (ou, s')
step s1 a = (ou1, s1')
reach s
reach s1
a = Ract ra

goal (1 subgoal):
 1. eqButUID s' s1'
[PROOF STEP]
by (cases ra) (auto simp add: simps)
[PROOF STATE]
proof (state)
this:
eqButUID s' s1'

goal (3 subgoals):
 1. \<And>x3. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Dact x3\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 2. \<And>x6. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Lact x6\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 3. \<And>x7. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = COMact x7\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x3. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Dact x3\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 2. \<And>x6. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Lact x6\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 3. \<And>x7. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = COMact x7\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
case (Lact la)
[PROOF STATE]
proof (state)
this:
a = Lact la

goal (3 subgoals):
 1. \<And>x3. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Dact x3\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 2. \<And>x6. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Lact x6\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 3. \<And>x7. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = COMact x7\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
eqButUID s s1
step s a = (ou, s')
step s1 a = (ou1, s1')
reach s
reach s1
a = Lact la
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eqButUID s s1
step s a = (ou, s')
step s1 a = (ou1, s1')
reach s
reach s1
a = Lact la

goal (1 subgoal):
 1. eqButUID s' s1'
[PROOF STEP]
by (cases la) (auto simp add: simps)
[PROOF STATE]
proof (state)
this:
eqButUID s' s1'

goal (2 subgoals):
 1. \<And>x3. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Dact x3\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 2. \<And>x7. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = COMact x7\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x3. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Dact x3\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 2. \<And>x7. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = COMact x7\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
case (COMact ca)
[PROOF STATE]
proof (state)
this:
a = COMact ca

goal (2 subgoals):
 1. \<And>x3. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Dact x3\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 2. \<And>x7. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = COMact x7\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
eqButUID s s1
step s a = (ou, s')
step s1 a = (ou1, s1')
reach s
reach s1
a = COMact ca
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eqButUID s s1
step s a = (ou, s')
step s1 a = (ou1, s1')
reach s
reach s1
a = COMact ca

goal (1 subgoal):
 1. eqButUID s' s1'
[PROOF STEP]
by (cases ca) (auto simp add: simps)
[PROOF STATE]
proof (state)
this:
eqButUID s' s1'

goal (1 subgoal):
 1. \<And>x3. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Dact x3\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x3. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Dact x3\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
case (Dact da)
[PROOF STATE]
proof (state)
this:
a = Dact da

goal (1 subgoal):
 1. \<And>x3. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Dact x3\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
note a = this
[PROOF STATE]
proof (state)
this:
a = Dact da

goal (1 subgoal):
 1. \<And>x3. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Dact x3\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
eqButUID s s1
step s a = (ou, s')
step s1 a = (ou1, s1')
reach s
reach s1
a = Dact da
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eqButUID s s1
step s a = (ou, s')
step s1 a = (ou1, s1')
reach s
reach s1
a = Dact da

goal (1 subgoal):
 1. eqButUID s' s1'
[PROOF STEP]
proof (cases da)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1 x2 x3. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Dact da; da = dFriend x1 x2 x3\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
case (dFriend uid p uid')
[PROOF STATE]
proof (state)
this:
da = dFriend uid p uid'

goal (1 subgoal):
 1. \<And>x1 x2 x3. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Dact da; da = dFriend x1 x2 x3\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
note ca = this
[PROOF STATE]
proof (state)
this:
da = dFriend uid p uid'

goal (1 subgoal):
 1. \<And>x1 x2 x3. \<lbrakk>eqButUID s s1; step s a = (ou, s'); step s1 a = (ou1, s1'); reach s; reach s1; a = Dact da; da = dFriend x1 x2 x3\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
da = dFriend uid p uid'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
da = dFriend uid p uid'

goal (1 subgoal):
 1. eqButUID s' s1'
[PROOF STEP]
proof (cases "(uid = UID1 \<and> uid' = UID2) \<or> (uid = UID2 \<and> uid' = UID1)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>da = dFriend uid p uid'; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 2. \<lbrakk>da = dFriend uid p uid'; \<not> (uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1)\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1

goal (2 subgoals):
 1. \<lbrakk>da = dFriend uid p uid'; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 2. \<lbrakk>da = dFriend uid p uid'; \<not> (uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1)\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1
[PROOF STEP]
have "eqButUID s s'" and "eqButUID s1 s1'"
[PROOF STATE]
proof (prove)
using this:
uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1

goal (1 subgoal):
 1. eqButUID s s' &&& eqButUID s1 s1'
[PROOF STEP]
using step step1 rs rs1
[PROOF STATE]
proof (prove)
using this:
uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1
step s a = (ou, s')
step s1 a = (ou1, s1')
reach s
reach s1

goal (1 subgoal):
 1. eqButUID s s' &&& eqButUID s1 s1'
[PROOF STEP]
unfolding a ca
[PROOF STATE]
proof (prove)
using this:
uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1
step s (Dact (dFriend uid p uid')) = (ou, s')
step s1 (Dact (dFriend uid p uid')) = (ou1, s1')
reach s
reach s1

goal (1 subgoal):
 1. eqButUID s s' &&& eqButUID s1 s1'
[PROOF STEP]
by (auto intro!: Dact_dFriend_step_eqButUID)+
[PROOF STATE]
proof (state)
this:
eqButUID s s'
eqButUID s1 s1'

goal (2 subgoals):
 1. \<lbrakk>da = dFriend uid p uid'; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1\<rbrakk> \<Longrightarrow> eqButUID s' s1'
 2. \<lbrakk>da = dFriend uid p uid'; \<not> (uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1)\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
with ss1
[PROOF STATE]
proof (chain)
picking this:
eqButUID s s1
eqButUID s s'
eqButUID s1 s1'
[PROOF STEP]
show "eqButUID s' s1'"
[PROOF STATE]
proof (prove)
using this:
eqButUID s s1
eqButUID s s'
eqButUID s1 s1'

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

goal (1 subgoal):
 1. \<lbrakk>da = dFriend uid p uid'; \<not> (uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1)\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>da = dFriend uid p uid'; \<not> (uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1)\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1)

goal (1 subgoal):
 1. \<lbrakk>da = dFriend uid p uid'; \<not> (uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1)\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
have fIDs: "eqButUIDf (friendIDs s) (friendIDs s1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqButUIDf (friendIDs s) (friendIDs s1)
[PROOF STEP]
using ss1
[PROOF STATE]
proof (prove)
using this:
eqButUID s s1

goal (1 subgoal):
 1. eqButUIDf (friendIDs s) (friendIDs s1)
[PROOF STEP]
by (auto simp: simps)
[PROOF STATE]
proof (state)
this:
eqButUIDf (friendIDs s) (friendIDs s1)

goal (1 subgoal):
 1. \<lbrakk>da = dFriend uid p uid'; \<not> (uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1)\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eqButUIDf (friendIDs s) (friendIDs s1)
[PROOF STEP]
have uid_uid': "uid \<in>\<in> friendIDs s uid' \<longleftrightarrow> uid \<in>\<in> friendIDs s1 uid'"
                                  "uid' \<in>\<in> friendIDs s uid \<longleftrightarrow> uid' \<in>\<in> friendIDs s1 uid"
[PROOF STATE]
proof (prove)
using this:
eqButUIDf (friendIDs s) (friendIDs s1)

goal (1 subgoal):
 1. (uid \<in>\<in> friendIDs s uid') = (uid \<in>\<in> friendIDs s1 uid') &&& (uid' \<in>\<in> friendIDs s uid) = (uid' \<in>\<in> friendIDs s1 uid)
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
eqButUIDf (friendIDs s) (friendIDs s1)
\<not> (uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1)

goal (1 subgoal):
 1. (uid \<in>\<in> friendIDs s uid') = (uid \<in>\<in> friendIDs s1 uid') &&& (uid' \<in>\<in> friendIDs s uid) = (uid' \<in>\<in> friendIDs s1 uid)
[PROOF STEP]
by (auto intro!: eqButUIDf_not_UID')
[PROOF STATE]
proof (state)
this:
(uid \<in>\<in> friendIDs s uid') = (uid \<in>\<in> friendIDs s1 uid')
(uid' \<in>\<in> friendIDs s uid) = (uid' \<in>\<in> friendIDs s1 uid)

goal (1 subgoal):
 1. \<lbrakk>da = dFriend uid p uid'; \<not> (uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1)\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
have dfIDs: "distinct (friendIDs s uid)" "distinct (friendIDs s uid')"
                          "distinct (friendIDs s1 uid)" "distinct (friendIDs s1 uid')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (distinct (friendIDs s uid) &&& distinct (friendIDs s uid')) &&& distinct (friendIDs s1 uid) &&& distinct (friendIDs s1 uid')
[PROOF STEP]
using reach_distinct_friends_reqs[OF rs] reach_distinct_friends_reqs[OF rs1]
[PROOF STATE]
proof (prove)
using this:
distinct (friendIDs s ?uid)
distinct (pendingFReqs s ?uid)
distinct (sentOuterFriendIDs s ?uid)
distinct (recvOuterFriendIDs s ?uid)
?uid' \<in>\<in> pendingFReqs s ?uid \<Longrightarrow> ?uid' \<notin> set (friendIDs s ?uid)
?uid' \<in>\<in> pendingFReqs s ?uid \<Longrightarrow> ?uid \<notin> set (friendIDs s ?uid')
distinct (friendIDs s1 ?uid)
distinct (pendingFReqs s1 ?uid)
distinct (sentOuterFriendIDs s1 ?uid)
distinct (recvOuterFriendIDs s1 ?uid)
?uid' \<in>\<in> pendingFReqs s1 ?uid \<Longrightarrow> ?uid' \<notin> set (friendIDs s1 ?uid)
?uid' \<in>\<in> pendingFReqs s1 ?uid \<Longrightarrow> ?uid \<notin> set (friendIDs s1 ?uid')

goal (1 subgoal):
 1. (distinct (friendIDs s uid) &&& distinct (friendIDs s uid')) &&& distinct (friendIDs s1 uid) &&& distinct (friendIDs s1 uid')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
distinct (friendIDs s uid)
distinct (friendIDs s uid')
distinct (friendIDs s1 uid)
distinct (friendIDs s1 uid')

goal (1 subgoal):
 1. \<lbrakk>da = dFriend uid p uid'; \<not> (uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1)\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
have "uid = UID1 \<Longrightarrow> eqButUIDl UID2 (remove1 uid' (friendIDs s UID1)) (remove1 uid' (friendIDs s1 UID1))"
               and "uid = UID2 \<Longrightarrow> eqButUIDl UID1 (remove1 uid' (friendIDs s UID2)) (remove1 uid' (friendIDs s1 UID2))"
               and "uid' = UID1 \<Longrightarrow> eqButUIDl UID2 (remove1 uid (friendIDs s UID1)) (remove1 uid (friendIDs s1 UID1))"
               and "uid' = UID2 \<Longrightarrow> eqButUIDl UID1 (remove1 uid (friendIDs s UID2)) (remove1 uid (friendIDs s1 UID2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((uid = UID1 \<Longrightarrow> eqButUIDl UID2 (remove1 uid' (friendIDs s UID1)) (remove1 uid' (friendIDs s1 UID1))) &&& (uid = UID2 \<Longrightarrow> eqButUIDl UID1 (remove1 uid' (friendIDs s UID2)) (remove1 uid' (friendIDs s1 UID2)))) &&& (uid' = UID1 \<Longrightarrow> eqButUIDl UID2 (remove1 uid (friendIDs s UID1)) (remove1 uid (friendIDs s1 UID1))) &&& (uid' = UID2 \<Longrightarrow> eqButUIDl UID1 (remove1 uid (friendIDs s UID2)) (remove1 uid (friendIDs s1 UID2)))
[PROOF STEP]
using fIDs uid_uid'
[PROOF STATE]
proof (prove)
using this:
eqButUIDf (friendIDs s) (friendIDs s1)
(uid \<in>\<in> friendIDs s uid') = (uid \<in>\<in> friendIDs s1 uid')
(uid' \<in>\<in> friendIDs s uid) = (uid' \<in>\<in> friendIDs s1 uid)

goal (1 subgoal):
 1. ((uid = UID1 \<Longrightarrow> eqButUIDl UID2 (remove1 uid' (friendIDs s UID1)) (remove1 uid' (friendIDs s1 UID1))) &&& (uid = UID2 \<Longrightarrow> eqButUIDl UID1 (remove1 uid' (friendIDs s UID2)) (remove1 uid' (friendIDs s1 UID2)))) &&& (uid' = UID1 \<Longrightarrow> eqButUIDl UID2 (remove1 uid (friendIDs s UID1)) (remove1 uid (friendIDs s1 UID1))) &&& (uid' = UID2 \<Longrightarrow> eqButUIDl UID1 (remove1 uid (friendIDs s UID2)) (remove1 uid (friendIDs s1 UID2)))
[PROOF STEP]
by - (intro eqButUIDl_remove1_cong; simp add: eqButUIDf_def)+
[PROOF STATE]
proof (state)
this:
uid = UID1 \<Longrightarrow> eqButUIDl UID2 (remove1 uid' (friendIDs s UID1)) (remove1 uid' (friendIDs s1 UID1))
uid = UID2 \<Longrightarrow> eqButUIDl UID1 (remove1 uid' (friendIDs s UID2)) (remove1 uid' (friendIDs s1 UID2))
uid' = UID1 \<Longrightarrow> eqButUIDl UID2 (remove1 uid (friendIDs s UID1)) (remove1 uid (friendIDs s1 UID1))
uid' = UID2 \<Longrightarrow> eqButUIDl UID1 (remove1 uid (friendIDs s UID2)) (remove1 uid (friendIDs s1 UID2))

goal (1 subgoal):
 1. \<lbrakk>da = dFriend uid p uid'; \<not> (uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1)\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
uid = UID1 \<Longrightarrow> eqButUIDl UID2 (remove1 uid' (friendIDs s UID1)) (remove1 uid' (friendIDs s1 UID1))
uid = UID2 \<Longrightarrow> eqButUIDl UID1 (remove1 uid' (friendIDs s UID2)) (remove1 uid' (friendIDs s1 UID2))
uid' = UID1 \<Longrightarrow> eqButUIDl UID2 (remove1 uid (friendIDs s UID1)) (remove1 uid (friendIDs s1 UID1))
uid' = UID2 \<Longrightarrow> eqButUIDl UID1 (remove1 uid (friendIDs s UID2)) (remove1 uid (friendIDs s1 UID2))
[PROOF STEP]
have 1: "eqButUIDf ((friendIDs s)(uid := remove1 uid' (friendIDs s uid),
                                                      uid' := remove1 uid (friendIDs s uid')))
                                       ((friendIDs s1)(uid := remove1 uid' (friendIDs s1 uid),
                                                       uid' := remove1 uid (friendIDs s1 uid')))"
[PROOF STATE]
proof (prove)
using this:
uid = UID1 \<Longrightarrow> eqButUIDl UID2 (remove1 uid' (friendIDs s UID1)) (remove1 uid' (friendIDs s1 UID1))
uid = UID2 \<Longrightarrow> eqButUIDl UID1 (remove1 uid' (friendIDs s UID2)) (remove1 uid' (friendIDs s1 UID2))
uid' = UID1 \<Longrightarrow> eqButUIDl UID2 (remove1 uid (friendIDs s UID1)) (remove1 uid (friendIDs s1 UID1))
uid' = UID2 \<Longrightarrow> eqButUIDl UID1 (remove1 uid (friendIDs s UID2)) (remove1 uid (friendIDs s1 UID2))

goal (1 subgoal):
 1. eqButUIDf ((friendIDs s)(uid := remove1 uid' (friendIDs s uid), uid' := remove1 uid (friendIDs s uid'))) ((friendIDs s1)(uid := remove1 uid' (friendIDs s1 uid), uid' := remove1 uid (friendIDs s1 uid')))
[PROOF STEP]
using fIDs
[PROOF STATE]
proof (prove)
using this:
uid = UID1 \<Longrightarrow> eqButUIDl UID2 (remove1 uid' (friendIDs s UID1)) (remove1 uid' (friendIDs s1 UID1))
uid = UID2 \<Longrightarrow> eqButUIDl UID1 (remove1 uid' (friendIDs s UID2)) (remove1 uid' (friendIDs s1 UID2))
uid' = UID1 \<Longrightarrow> eqButUIDl UID2 (remove1 uid (friendIDs s UID1)) (remove1 uid (friendIDs s1 UID1))
uid' = UID2 \<Longrightarrow> eqButUIDl UID1 (remove1 uid (friendIDs s UID2)) (remove1 uid (friendIDs s1 UID2))
eqButUIDf (friendIDs s) (friendIDs s1)

goal (1 subgoal):
 1. eqButUIDf ((friendIDs s)(uid := remove1 uid' (friendIDs s uid), uid' := remove1 uid (friendIDs s uid'))) ((friendIDs s1)(uid := remove1 uid' (friendIDs s1 uid), uid' := remove1 uid (friendIDs s1 uid')))
[PROOF STEP]
by (intro eqButUIDf_cong) (auto simp add: eqButUIDf_def)
[PROOF STATE]
proof (state)
this:
eqButUIDf ((friendIDs s)(uid := remove1 uid' (friendIDs s uid), uid' := remove1 uid (friendIDs s uid'))) ((friendIDs s1)(uid := remove1 uid' (friendIDs s1 uid), uid' := remove1 uid (friendIDs s1 uid')))

goal (1 subgoal):
 1. \<lbrakk>da = dFriend uid p uid'; \<not> (uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1)\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
have "e_deleteFriend s uid p uid'
                \<longleftrightarrow> e_deleteFriend s1 uid p uid'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e_deleteFriend s uid p uid' = e_deleteFriend s1 uid p uid'
[PROOF STEP]
using uid_uid' ss1
[PROOF STATE]
proof (prove)
using this:
(uid \<in>\<in> friendIDs s uid') = (uid \<in>\<in> friendIDs s1 uid')
(uid' \<in>\<in> friendIDs s uid) = (uid' \<in>\<in> friendIDs s1 uid)
eqButUID s s1

goal (1 subgoal):
 1. e_deleteFriend s uid p uid' = e_deleteFriend s1 uid p uid'
[PROOF STEP]
by (auto simp: simps d_defs)
[PROOF STATE]
proof (state)
this:
e_deleteFriend s uid p uid' = e_deleteFriend s1 uid p uid'

goal (1 subgoal):
 1. \<lbrakk>da = dFriend uid p uid'; \<not> (uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1)\<rbrakk> \<Longrightarrow> eqButUID s' s1'
[PROOF STEP]
with 1
[PROOF STATE]
proof (chain)
picking this:
eqButUIDf ((friendIDs s)(uid := remove1 uid' (friendIDs s uid), uid' := remove1 uid (friendIDs s uid'))) ((friendIDs s1)(uid := remove1 uid' (friendIDs s1 uid), uid' := remove1 uid (friendIDs s1 uid')))
e_deleteFriend s uid p uid' = e_deleteFriend s1 uid p uid'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eqButUIDf ((friendIDs s)(uid := remove1 uid' (friendIDs s uid), uid' := remove1 uid (friendIDs s uid'))) ((friendIDs s1)(uid := remove1 uid' (friendIDs s1 uid), uid' := remove1 uid (friendIDs s1 uid')))
e_deleteFriend s uid p uid' = e_deleteFriend s1 uid p uid'

goal (1 subgoal):
 1. eqButUID s' s1'
[PROOF STEP]
using assms dfIDs
[PROOF STATE]
proof (prove)
using this:
eqButUIDf ((friendIDs s)(uid := remove1 uid' (friendIDs s uid), uid' := remove1 uid (friendIDs s uid'))) ((friendIDs s1)(uid := remove1 uid' (friendIDs s1 uid), uid' := remove1 uid (friendIDs s1 uid')))
e_deleteFriend s uid p uid' = e_deleteFriend s1 uid p uid'
eqButUID s s1
step s a = (ou, s')
step s1 a = (ou1, s1')
reach s
reach s1
distinct (friendIDs s uid)
distinct (friendIDs s uid')
distinct (friendIDs s1 uid)
distinct (friendIDs s1 uid')

goal (1 subgoal):
 1. eqButUID s' s1'
[PROOF STEP]
unfolding a ca
[PROOF STATE]
proof (prove)
using this:
eqButUIDf ((friendIDs s)(uid := remove1 uid' (friendIDs s uid), uid' := remove1 uid (friendIDs s uid'))) ((friendIDs s1)(uid := remove1 uid' (friendIDs s1 uid), uid' := remove1 uid (friendIDs s1 uid')))
e_deleteFriend s uid p uid' = e_deleteFriend s1 uid p uid'
eqButUID s s1
step s (Dact (dFriend uid p uid')) = (ou, s')
step s1 (Dact (dFriend uid p uid')) = (ou1, s1')
reach s
reach s1
distinct (friendIDs s uid)
distinct (friendIDs s uid')
distinct (friendIDs s1 uid)
distinct (friendIDs s1 uid')

goal (1 subgoal):
 1. eqButUID s' s1'
[PROOF STEP]
by (auto simp: simps d_defs distinct_remove1_removeAll)
[PROOF STATE]
proof (state)
this:
eqButUID s' s1'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
eqButUID s' s1'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
eqButUID s' s1'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
eqButUID s' s1'

goal:
No subgoals!
[PROOF STEP]
qed