[STATEMENT]
lemma eqButUID_cong[simp, intro]:
"\<And> uu1 uu2. eqButUID s s1 \<Longrightarrow> uu1 = uu2 \<Longrightarrow> eqButUID (s \<lparr>admin := uu1\<rparr>) (s1 \<lparr>admin := uu2\<rparr>)"

"\<And> uu1 uu2. eqButUID s s1 \<Longrightarrow> uu1 = uu2 \<Longrightarrow> eqButUID (s \<lparr>pendingUReqs := uu1\<rparr>) (s1 \<lparr>pendingUReqs := uu2\<rparr>)"
"\<And> uu1 uu2. eqButUID s s1 \<Longrightarrow> uu1 = uu2 \<Longrightarrow> eqButUID (s \<lparr>userReq := uu1\<rparr>) (s1 \<lparr>userReq := uu2\<rparr>)"
"\<And> uu1 uu2. eqButUID s s1 \<Longrightarrow> uu1 = uu2 \<Longrightarrow> eqButUID (s \<lparr>userIDs := uu1\<rparr>) (s1 \<lparr>userIDs := uu2\<rparr>)"
"\<And> uu1 uu2. eqButUID s s1 \<Longrightarrow> uu1 = uu2 \<Longrightarrow> eqButUID (s \<lparr>user := uu1\<rparr>) (s1 \<lparr>user := uu2\<rparr>)"
"\<And> uu1 uu2. eqButUID s s1 \<Longrightarrow> uu1 = uu2 \<Longrightarrow> eqButUID (s \<lparr>pass := uu1\<rparr>) (s1 \<lparr>pass := uu2\<rparr>)"

"\<And> uu1 uu2. eqButUID s s1 \<Longrightarrow> uu1 = uu2 \<Longrightarrow> eqButUID (s \<lparr>postIDs := uu1\<rparr>) (s1 \<lparr>postIDs := uu2\<rparr>)"
"\<And> uu1 uu2. eqButUID s s1 \<Longrightarrow> uu1 = uu2 \<Longrightarrow> eqButUID (s \<lparr>owner := uu1\<rparr>) (s1 \<lparr>owner := uu2\<rparr>)"
"\<And> uu1 uu2. eqButUID s s1 \<Longrightarrow> uu1 = uu2 \<Longrightarrow> eqButUID (s \<lparr>post := uu1\<rparr>) (s1 \<lparr>post := uu2\<rparr>)"
"\<And> uu1 uu2. eqButUID s s1 \<Longrightarrow> uu1 = uu2 \<Longrightarrow> eqButUID (s \<lparr>vis := uu1\<rparr>) (s1 \<lparr>vis := uu2\<rparr>)"

"\<And> uu1 uu2. eqButUID s s1 \<Longrightarrow> eqButUIDf uu1 uu2 \<Longrightarrow> eqButUID (s \<lparr>pendingFReqs := uu1\<rparr>) (s1 \<lparr>pendingFReqs := uu2\<rparr>)"
"\<And> uu1 uu2. eqButUID s s1 \<Longrightarrow> eqButUID12 uu1 uu2 \<Longrightarrow> eqButUID (s \<lparr>friendReq := uu1\<rparr>) (s1 \<lparr>friendReq := uu2\<rparr>)"
"\<And> uu1 uu2. eqButUID s s1 \<Longrightarrow> eqButUIDf uu1 uu2 \<Longrightarrow> eqButUID (s \<lparr>friendIDs := uu1\<rparr>) (s1 \<lparr>friendIDs := uu2\<rparr>)"

"\<And> uu1 uu2. eqButUID s s1 \<Longrightarrow> uu1 = uu2 \<Longrightarrow> eqButUID (s \<lparr>pendingSApiReqs := uu1\<rparr>) (s1 \<lparr>pendingSApiReqs := uu2\<rparr>)"
"\<And> uu1 uu2. eqButUID s s1 \<Longrightarrow> uu1 = uu2 \<Longrightarrow> eqButUID (s \<lparr>sApiReq := uu1\<rparr>) (s1 \<lparr>sApiReq := uu2\<rparr>)"
"\<And> uu1 uu2. eqButUID s s1 \<Longrightarrow> uu1 = uu2 \<Longrightarrow> eqButUID (s \<lparr>serverApiIDs := uu1\<rparr>) (s1 \<lparr>serverApiIDs := uu2\<rparr>)"
"\<And> uu1 uu2. eqButUID s s1 \<Longrightarrow> uu1 = uu2 \<Longrightarrow> eqButUID (s \<lparr>serverPass := uu1\<rparr>) (s1 \<lparr>serverPass := uu2\<rparr>)"
"\<And> uu1 uu2. eqButUID s s1 \<Longrightarrow> uu1 = uu2 \<Longrightarrow> eqButUID (s \<lparr>outerPostIDs := uu1\<rparr>) (s1 \<lparr>outerPostIDs := uu2\<rparr>)"
"\<And> uu1 uu2. eqButUID s s1 \<Longrightarrow> uu1 = uu2 \<Longrightarrow> eqButUID (s \<lparr>outerPost := uu1\<rparr>) (s1 \<lparr>outerPost := uu2\<rparr>)"
"\<And> uu1 uu2. eqButUID s s1 \<Longrightarrow> uu1 = uu2 \<Longrightarrow> eqButUID (s \<lparr>outerVis := uu1\<rparr>) (s1 \<lparr>outerVis := uu2\<rparr>)"
"\<And> uu1 uu2. eqButUID s s1 \<Longrightarrow> uu1 = uu2 \<Longrightarrow> eqButUID (s \<lparr>outerOwner := uu1\<rparr>) (s1 \<lparr>outerOwner := uu2\<rparr>)"
"\<And> uu1 uu2. eqButUID s s1 \<Longrightarrow> uu1 = uu2 \<Longrightarrow> eqButUID (s \<lparr>sentOuterFriendIDs := uu1\<rparr>) (s1 \<lparr>sentOuterFriendIDs := uu2\<rparr>)"
"\<And> uu1 uu2. eqButUID s s1 \<Longrightarrow> uu1 = uu2 \<Longrightarrow> eqButUID (s \<lparr>recvOuterFriendIDs := uu1\<rparr>) (s1 \<lparr>recvOuterFriendIDs := uu2\<rparr>)"

"\<And> uu1 uu2. eqButUID s s1 \<Longrightarrow> uu1 = uu2 \<Longrightarrow> eqButUID (s \<lparr>pendingCApiReqs := uu1\<rparr>) (s1 \<lparr>pendingCApiReqs := uu2\<rparr>)"
"\<And> uu1 uu2. eqButUID s s1 \<Longrightarrow> uu1 = uu2 \<Longrightarrow> eqButUID (s \<lparr>cApiReq := uu1\<rparr>) (s1 \<lparr>cApiReq := uu2\<rparr>)"
"\<And> uu1 uu2. eqButUID s s1 \<Longrightarrow> uu1 = uu2 \<Longrightarrow> eqButUID (s \<lparr>clientApiIDs := uu1\<rparr>) (s1 \<lparr>clientApiIDs := uu2\<rparr>)"
"\<And> uu1 uu2. eqButUID s s1 \<Longrightarrow> uu1 = uu2 \<Longrightarrow> eqButUID (s \<lparr>clientPass := uu1\<rparr>) (s1 \<lparr>clientPass := uu2\<rparr>)"
"\<And> uu1 uu2. eqButUID s s1 \<Longrightarrow> uu1 = uu2 \<Longrightarrow> eqButUID (s \<lparr>sharedWith := uu1\<rparr>) (s1 \<lparr>sharedWith:= uu2\<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((((\<And>uu1 uu2. \<lbrakk>eqButUID s s1; uu1 = uu2\<rbrakk> \<Longrightarrow> eqButUID (s\<lparr>admin := uu1\<rparr>) (s1\<lparr>admin := uu2\<rparr>)) &&& (\<And>uu1 uu2. \<lbrakk>eqButUID s s1; uu1 = uu2\<rbrakk> \<Longrightarrow> eqButUID (s\<lparr>pendingUReqs := uu1\<rparr>) (s1\<lparr>pendingUReqs := uu2\<rparr>)) &&& (\<And>uu1 uu2. \<lbrakk>eqButUID s s1; uu1 = uu2\<rbrakk> \<Longrightarrow> eqButUID (s\<lparr>userReq := uu1\<rparr>) (s1\<lparr>userReq := uu2\<rparr>))) &&& ((\<And>uu1 uu2. \<lbrakk>eqButUID s s1; uu1 = uu2\<rbrakk> \<Longrightarrow> eqButUID (s\<lparr>userIDs := uu1\<rparr>) (s1\<lparr>userIDs := uu2\<rparr>)) &&& (\<And>uu1 uu2. \<lbrakk>eqButUID s s1; uu1 = uu2\<rbrakk> \<Longrightarrow> eqButUID (s\<lparr>user := uu1\<rparr>) (s1\<lparr>user := uu2\<rparr>))) &&& (\<And>uu1 uu2. \<lbrakk>eqButUID s s1; uu1 = uu2\<rbrakk> \<Longrightarrow> eqButUID (s\<lparr>pass := uu1\<rparr>) (s1\<lparr>pass := uu2\<rparr>)) &&& (\<And>uu1 uu2. \<lbrakk>eqButUID s s1; uu1 = uu2\<rbrakk> \<Longrightarrow> eqButUID (s\<lparr>postIDs := uu1\<rparr>) (s1\<lparr>postIDs := uu2\<rparr>))) &&& ((\<And>uu1 uu2. \<lbrakk>eqButUID s s1; uu1 = uu2\<rbrakk> \<Longrightarrow> eqButUID (s\<lparr>owner := uu1\<rparr>) (s1\<lparr>owner := uu2\<rparr>)) &&& (\<And>uu1 uu2. \<lbrakk>eqButUID s s1; uu1 = uu2\<rbrakk> \<Longrightarrow> eqButUID (s\<lparr>post := uu1\<rparr>) (s1\<lparr>post := uu2\<rparr>)) &&& (\<And>uu1 uu2. \<lbrakk>eqButUID s s1; uu1 = uu2\<rbrakk> \<Longrightarrow> eqButUID (s\<lparr>vis := uu1\<rparr>) (s1\<lparr>vis := uu2\<rparr>))) &&& ((\<And>uu1 uu2. \<lbrakk>eqButUID s s1; eqButUIDf uu1 uu2\<rbrakk> \<Longrightarrow> eqButUID (s\<lparr>pendingFReqs := uu1\<rparr>) (s1\<lparr>pendingFReqs := uu2\<rparr>)) &&& (\<And>uu1 uu2. \<lbrakk>eqButUID s s1; eqButUID12 uu1 uu2\<rbrakk> \<Longrightarrow> eqButUID (s\<lparr>friendReq := uu1\<rparr>) (s1\<lparr>friendReq := uu2\<rparr>))) &&& (\<And>uu1 uu2. \<lbrakk>eqButUID s s1; eqButUIDf uu1 uu2\<rbrakk> \<Longrightarrow> eqButUID (s\<lparr>friendIDs := uu1\<rparr>) (s1\<lparr>friendIDs := uu2\<rparr>)) &&& (\<And>uu1 uu2. \<lbrakk>eqButUID s s1; uu1 = uu2\<rbrakk> \<Longrightarrow> eqButUID (s\<lparr>pendingSApiReqs := uu1\<rparr>) (s1\<lparr>pendingSApiReqs := uu2\<rparr>))) &&& (((\<And>uu1 uu2. \<lbrakk>eqButUID s s1; uu1 = uu2\<rbrakk> \<Longrightarrow> eqButUID (s\<lparr>sApiReq := uu1\<rparr>) (s1\<lparr>sApiReq := uu2\<rparr>)) &&& (\<And>uu1 uu2. \<lbrakk>eqButUID s s1; uu1 = uu2\<rbrakk> \<Longrightarrow> eqButUID (s\<lparr>serverApiIDs := uu1\<rparr>) (s1\<lparr>serverApiIDs := uu2\<rparr>)) &&& (\<And>uu1 uu2. \<lbrakk>eqButUID s s1; uu1 = uu2\<rbrakk> \<Longrightarrow> eqButUID (s\<lparr>serverPass := uu1\<rparr>) (s1\<lparr>serverPass := uu2\<rparr>))) &&& ((\<And>uu1 uu2. \<lbrakk>eqButUID s s1; uu1 = uu2\<rbrakk> \<Longrightarrow> eqButUID (s\<lparr>outerPostIDs := uu1\<rparr>) (s1\<lparr>outerPostIDs := uu2\<rparr>)) &&& (\<And>uu1 uu2. \<lbrakk>eqButUID s s1; uu1 = uu2\<rbrakk> \<Longrightarrow> eqButUID (s\<lparr>outerPost := uu1\<rparr>) (s1\<lparr>outerPost := uu2\<rparr>))) &&& (\<And>uu1 uu2. \<lbrakk>eqButUID s s1; uu1 = uu2\<rbrakk> \<Longrightarrow> eqButUID (s\<lparr>outerVis := uu1\<rparr>) (s1\<lparr>outerVis := uu2\<rparr>)) &&& (\<And>uu1 uu2. \<lbrakk>eqButUID s s1; uu1 = uu2\<rbrakk> \<Longrightarrow> eqButUID (s\<lparr>outerOwner := uu1\<rparr>) (s1\<lparr>outerOwner := uu2\<rparr>))) &&& ((\<And>uu1 uu2. \<lbrakk>eqButUID s s1; uu1 = uu2\<rbrakk> \<Longrightarrow> eqButUID (s\<lparr>sentOuterFriendIDs := uu1\<rparr>) (s1\<lparr>sentOuterFriendIDs := uu2\<rparr>)) &&& (\<And>uu1 uu2. \<lbrakk>eqButUID s s1; uu1 = uu2\<rbrakk> \<Longrightarrow> eqButUID (s\<lparr>recvOuterFriendIDs := uu1\<rparr>) (s1\<lparr>recvOuterFriendIDs := uu2\<rparr>)) &&& (\<And>uu1 uu2. \<lbrakk>eqButUID s s1; uu1 = uu2\<rbrakk> \<Longrightarrow> eqButUID (s\<lparr>pendingCApiReqs := uu1\<rparr>) (s1\<lparr>pendingCApiReqs := uu2\<rparr>))) &&& ((\<And>uu1 uu2. \<lbrakk>eqButUID s s1; uu1 = uu2\<rbrakk> \<Longrightarrow> eqButUID (s\<lparr>cApiReq := uu1\<rparr>) (s1\<lparr>cApiReq := uu2\<rparr>)) &&& (\<And>uu1 uu2. \<lbrakk>eqButUID s s1; uu1 = uu2\<rbrakk> \<Longrightarrow> eqButUID (s\<lparr>clientApiIDs := uu1\<rparr>) (s1\<lparr>clientApiIDs := uu2\<rparr>))) &&& (\<And>uu1 uu2. \<lbrakk>eqButUID s s1; uu1 = uu2\<rbrakk> \<Longrightarrow> eqButUID (s\<lparr>clientPass := uu1\<rparr>) (s1\<lparr>clientPass := uu2\<rparr>)) &&& (\<And>uu1 uu2. \<lbrakk>eqButUID s s1; uu1 = uu2\<rbrakk> \<Longrightarrow> eqButUID (s\<lparr>sharedWith := uu1\<rparr>) (s1\<lparr>sharedWith := uu2\<rparr>))
[PROOF STEP]
unfolding eqButUID_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((((\<And>uu1 uu2. \<lbrakk>admin s = admin s1 \<and> pendingUReqs s = pendingUReqs s1 \<and> userReq s = userReq s1 \<and> userIDs s = userIDs s1 \<and> user s = user s1 \<and> pass s = pass s1 \<and> eqButUIDf (pendingFReqs s) (pendingFReqs s1) \<and> eqButUID12 (friendReq s) (friendReq s1) \<and> eqButUIDf (friendIDs s) (friendIDs s1) \<and> postIDs s = postIDs s1 \<and> admin s = admin s1 \<and> post s = post s1 \<and> vis s = vis s1 \<and> owner s = owner s1 \<and> pendingSApiReqs s = pendingSApiReqs s1 \<and> sApiReq s = sApiReq s1 \<and> serverApiIDs s = serverApiIDs s1 \<and> serverPass s = serverPass s1 \<and> outerPostIDs s = outerPostIDs s1 \<and> outerPost s = outerPost s1 \<and> outerVis s = outerVis s1 \<and> outerOwner s = outerOwner s1 \<and> sentOuterFriendIDs s = sentOuterFriendIDs s1 \<and> recvOuterFriendIDs s = recvOuterFriendIDs s1 \<and> pendingCApiReqs s = pendingCApiReqs s1 \<and> cApiReq s = cApiReq s1 \<and> clientApiIDs s = clientApiIDs s1 \<and> clientPass s = clientPass s1 \<and> sharedWith s = sharedWith s1; uu1 = uu2\<rbrakk> \<Longrightarrow> admin (s\<lparr>admin := uu1\<rparr>) = admin (s1\<lparr>admin := uu2\<rparr>) \<and> pendingUReqs (s\<lparr>admin := uu1\<rparr>) = pendingUReqs (s1\<lparr>admin := uu2\<rparr>) \<and> userReq (s\<lparr>admin := uu1\<rparr>) = userReq (s1\<lparr>admin := uu2\<rparr>) \<and> userIDs (s\<lparr>admin := uu1\<rparr>) = userIDs (s1\<lparr>admin := uu2\<rparr>) \<and> user (s\<lparr>admin := uu1\<rparr>) = user (s1\<lparr>admin := uu2\<rparr>) \<and> pass (s\<lparr>admin := uu1\<rparr>) = pass (s1\<lparr>admin := uu2\<rparr>) \<and> eqButUIDf (pendingFReqs (s\<lparr>admin := uu1\<rparr>)) (pendingFReqs (s1\<lparr>admin := uu2\<rparr>)) \<and> eqButUID12 (friendReq (s\<lparr>admin := uu1\<rparr>)) (friendReq (s1\<lparr>admin := uu2\<rparr>)) \<and> eqButUIDf (friendIDs (s\<lparr>admin := uu1\<rparr>)) (friendIDs (s1\<lparr>admin := uu2\<rparr>)) \<and> postIDs (s\<lparr>admin := uu1\<rparr>) = postIDs (s1\<lparr>admin := uu2\<rparr>) \<and> admin (s\<lparr>admin := uu1\<rparr>) = admin (s1\<lparr>admin := uu2\<rparr>) \<and> post (s\<lparr>admin := uu1\<rparr>) = post (s1\<lparr>admin := uu2\<rparr>) \<and> vis (s\<lparr>admin := uu1\<rparr>) = vis (s1\<lparr>admin := uu2\<rparr>) \<and> owner (s\<lparr>admin := uu1\<rparr>) = owner (s1\<lparr>admin := uu2\<rparr>) \<and> pendingSApiReqs (s\<lparr>admin := uu1\<rparr>) = pendingSApiReqs (s1\<lparr>admin := uu2\<rparr>) \<and> sApiReq (s\<lparr>admin := uu1\<rparr>) = sApiReq (s1\<lparr>admin := uu2\<rparr>) \<and> serverApiIDs (s\<lparr>admin := uu1\<rparr>) = serverApiIDs (s1\<lparr>admin := uu2\<rparr>) \<and> serverPass (s\<lparr>admin := uu1\<rparr>) = serverPass (s1\<lparr>admin := uu2\<rparr>) \<and> outerPostIDs (s\<lparr>admin := uu1\<rparr>) = outerPostIDs (s1\<lparr>admin := uu2\<rparr>) \<and> outerPost (s\<lparr>admin := uu1\<rparr>) = outerPost (s1\<lparr>admin := uu2\<rparr>) \<and> outerVis (s\<lparr>admin := uu1\<rparr>) = outerVis (s1\<lparr>admin := uu2\<rparr>) \<and> outerOwner (s\<lparr>admin := uu1\<rparr>) = outerOwner (s1\<lparr>admin := uu2\<rparr>) \<and> sentOuterFriendIDs (s\<lparr>admin := uu1\<rparr>) = sentOuterFriendIDs (s1\<lparr>admin := uu2\<rparr>) \<and> recvOuterFriendIDs (s\<lparr>admin := uu1\<rparr>) = recvOuterFriendIDs (s1\<lparr>admin := uu2\<rparr>) \<and> pendingCApiReqs (s\<lparr>admin := uu1\<rparr>) = pendingCApiReqs (s1\<lparr>admin := uu2\<rparr>) \<and> cApiReq (s\<lparr>admin := uu1\<rparr>) = cApiReq (s1\<lparr>admin := uu2\<rparr>) \<and> clientApiIDs (s\<lparr>admin := uu1\<rparr>) = clientApiIDs (s1\<lparr>admin := uu2\<rparr>) \<and> clientPass (s\<lparr>admin := uu1\<rparr>) = clientPass (s1\<lparr>admin := uu2\<rparr>) \<and> sharedWith (s\<lparr>admin := uu1\<rparr>) = sharedWith (s1\<lparr>admin := uu2\<rparr>)) &&& (\<And>uu1 uu2. \<lbrakk>admin s = admin s1 \<and> pendingUReqs s = pendingUReqs s1 \<and> userReq s = userReq s1 \<and> userIDs s = userIDs s1 \<and> user s = user s1 \<and> pass s = pass s1 \<and> eqButUIDf (pendingFReqs s) (pendingFReqs s1) \<and> eqButUID12 (friendReq s) (friendReq s1) \<and> eqButUIDf (friendIDs s) (friendIDs s1) \<and> postIDs s = postIDs s1 \<and> admin s = admin s1 \<and> post s = post s1 \<and> vis s = vis s1 \<and> owner s = owner s1 \<and> pendingSApiReqs s = pendingSApiReqs s1 \<and> sApiReq s = sApiReq s1 \<and> serverApiIDs s = serverApiIDs s1 \<and> serverPass s = serverPass s1 \<and> outerPostIDs s = outerPostIDs s1 \<and> outerPost s = outerPost s1 \<and> outerVis s = outerVis s1 \<and> outerOwner s = outerOwner s1 \<and> sentOuterFriendIDs s = sentOuterFriendIDs s1 \<and> recvOuterFriendIDs s = recvOuterFriendIDs s1 \<and> pendingCApiReqs s = pendingCApiReqs s1 \<and> cApiReq s = cApiReq s1 \<and> clientApiIDs s = clientApiIDs s1 \<and> clientPass s = clientPass s1 \<and> sharedWith s = sharedWith s1; uu1 = uu2\<rbrakk> \<Longrightarrow> admin (s\<lparr>pendingUReqs := uu1\<rparr>) = admin (s1\<lparr>pendingUReqs := uu2\<rparr>) \<and> pendingUReqs (s\<lparr>pendingUReqs := uu1\<rparr>) = pendingUReqs (s1\<lparr>pendingUReqs := uu2\<rparr>) \<and> userReq (s\<lparr>pendingUReqs := uu1\<rparr>) = userReq (s1\<lparr>pendingUReqs := uu2\<rparr>) \<and> userIDs (s\<lparr>pendingUReqs := uu1\<rparr>) = userIDs (s1\<lparr>pendingUReqs := uu2\<rparr>) \<and> user (s\<lparr>pendingUReqs := uu1\<rparr>) = user (s1\<lparr>pendingUReqs := uu2\<rparr>) \<and> pass (s\<lparr>pendingUReqs := uu1\<rparr>) = pass (s1\<lparr>pendingUReqs := uu2\<rparr>) \<and> eqButUIDf (pendingFReqs (s\<lparr>pendingUReqs := uu1\<rparr>)) (pendingFReqs (s1\<lparr>pendingUReqs := uu2\<rparr>)) \<and> eqButUID12 (friendReq (s\<lparr>pendingUReqs := uu1\<rparr>)) (friendReq (s1\<lparr>pendingUReqs := uu2\<rparr>)) \<and> eqButUIDf (friendIDs (s\<lparr>pendingUReqs := uu1\<rparr>)) (friendIDs (s1\<lparr>pendingUReqs := uu2\<rparr>)) \<and> postIDs (s\<lparr>pendingUReqs := uu1\<rparr>) = postIDs (s1\<lparr>pendingUReqs := uu2\<rparr>) \<and> admin (s\<lparr>pendingUReqs := uu1\<rparr>) = admin (s1\<lparr>pendingUReqs := uu2\<rparr>) \<and> post (s\<lparr>pendingUReqs := uu1\<rparr>) = post (s1\<lparr>pendingUReqs := uu2\<rparr>) \<and> vis (s\<lparr>pendingUReqs := uu1\<rparr>) = vis (s1\<lparr>pendingUReqs := uu2\<rparr>) \<and> owner (s\<lparr>pendingUReqs := uu1\<rparr>) = owner (s1\<lparr>pendingUReqs := uu2\<rparr>) \<and> pendingSApiReqs (s\<lparr>pendingUReqs := uu1\<rparr>) = pendingSApiReqs (s1\<lparr>pendingUReqs := uu2\<rparr>) \<and> sApiReq (s\<lparr>pendingUReqs := uu1\<rparr>) = sApiReq (s1\<lparr>pendingUReqs := uu2\<rparr>) \<and> serverApiIDs (s\<lparr>pendingUReqs := uu1\<rparr>) = serverApiIDs (s1\<lparr>pendingUReqs := uu2\<rparr>) \<and> serverPass (s\<lparr>pendingUReqs := uu1\<rparr>) = serverPass (s1\<lparr>pendingUReqs := uu2\<rparr>) \<and> outerPostIDs (s\<lparr>pendingUReqs := uu1\<rparr>) = outerPostIDs (s1\<lparr>pendingUReqs := uu2\<rparr>) \<and> outerPost (s\<lparr>pendingUReqs := uu1\<rparr>) = outerPost (s1\<lparr>pendingUReqs := uu2\<rparr>) \<and> outerVis (s\<lparr>pendingUReqs := uu1\<rparr>) = outerVis (s1\<lparr>pendingUReqs := uu2\<rparr>) \<and> outerOwner (s\<lparr>pendingUReqs := uu1\<rparr>) = outerOwner (s1\<lparr>pendingUReqs := uu2\<rparr>) \<and> sentOuterFriendIDs (s\<lparr>pendingUReqs := uu1\<rparr>) = sentOuterFriendIDs (s1\<lparr>pendingUReqs := uu2\<rparr>) \<and> recvOuterFriendIDs (s\<lparr>pendingUReqs := uu1\<rparr>) = recvOuterFriendIDs (s1\<lparr>pendingUReqs := uu2\<rparr>) \<and> pendingCApiReqs (s\<lparr>pendingUReqs := uu1\<rparr>) = pendingCApiReqs (s1\<lparr>pendingUReqs := uu2\<rparr>) \<and> cApiReq (s\<lparr>pendingUReqs := uu1\<rparr>) = cApiReq (s1\<lparr>pendingUReqs := uu2\<rparr>) \<and> clientApiIDs (s\<lparr>pendingUReqs := uu1\<rparr>) = clientApiIDs (s1\<lparr>pendingUReqs := uu2\<rparr>) \<and> clientPass (s\<lparr>pendingUReqs := uu1\<rparr>) = clientPass (s1\<lparr>pendingUReqs := uu2\<rparr>) \<and> sharedWith (s\<lparr>pendingUReqs := uu1\<rparr>) = sharedWith (s1\<lparr>pendingUReqs := uu2\<rparr>)) &&& (\<And>uu1 uu2. \<lbrakk>admin s = admin s1 \<and> pendingUReqs s = pendingUReqs s1 \<and> userReq s = userReq s1 \<and> userIDs s = userIDs s1 \<and> user s = user s1 \<and> pass s = pass s1 \<and> eqButUIDf (pendingFReqs s) (pendingFReqs s1) \<and> eqButUID12 (friendReq s) (friendReq s1) \<and> eqButUIDf (friendIDs s) (friendIDs s1) \<and> postIDs s = postIDs s1 \<and> admin s = admin s1 \<and> post s = post s1 \<and> vis s = vis s1 \<and> owner s = owner s1 \<and> pendingSApiReqs s = pendingSApiReqs s1 \<and> sApiReq s = sApiReq s1 \<and> serverApiIDs s = serverApiIDs s1 \<and> serverPass s = serverPass s1 \<and> outerPostIDs s = outerPostIDs s1 \<and> outerPost s = outerPost s1 \<and> outerVis s = outerVis s1 \<and> outerOwner s = outerOwner s1 \<and> sentOuterFriendIDs s = sentOuterFriendIDs s1 \<and> recvOuterFriendIDs s = recvOuterFriendIDs s1 \<and> pendingCApiReqs s = pendingCApiReqs s1 \<and> cApiReq s = cApiReq s1 \<and> clientApiIDs s = clientApiIDs s1 \<and> clientPass s = clientPass s1 \<and> sharedWith s = sharedWith s1; uu1 = uu2\<rbrakk> \<Longrightarrow> admin (s\<lparr>userReq := uu1\<rparr>) = admin (s1\<lparr>userReq := uu2\<rparr>) \<and> pendingUReqs (s\<lparr>userReq := uu1\<rparr>) = pendingUReqs (s1\<lparr>userReq := uu2\<rparr>) \<and> userReq (s\<lparr>userReq := uu1\<rparr>) = userReq (s1\<lparr>userReq := uu2\<rparr>) \<and> userIDs (s\<lparr>userReq := uu1\<rparr>) = userIDs (s1\<lparr>userReq := uu2\<rparr>) \<and> user (s\<lparr>userReq := uu1\<rparr>) = user (s1\<lparr>userReq := uu2\<rparr>) \<and> pass (s\<lparr>userReq := uu1\<rparr>) = pass (s1\<lparr>userReq := uu2\<rparr>) \<and> eqButUIDf (pendingFReqs (s\<lparr>userReq := uu1\<rparr>)) (pendingFReqs (s1\<lparr>userReq := uu2\<rparr>)) \<and> eqButUID12 (friendReq (s\<lparr>userReq := uu1\<rparr>)) (friendReq (s1\<lparr>userReq := uu2\<rparr>)) \<and> eqButUIDf (friendIDs (s\<lparr>userReq := uu1\<rparr>)) (friendIDs (s1\<lparr>userReq := uu2\<rparr>)) \<and> postIDs (s\<lparr>userReq := uu1\<rparr>) = postIDs (s1\<lparr>userReq := uu2\<rparr>) \<and> admin (s\<lparr>userReq := uu1\<rparr>) = admin (s1\<lparr>userReq := uu2\<rparr>) \<and> post (s\<lparr>userReq := uu1\<rparr>) = post (s1\<lparr>userReq := uu2\<rparr>) \<and> vis (s\<lparr>userReq := uu1\<rparr>) = vis (s1\<lparr>userReq := uu2\<rparr>) \<and> owner (s\<lparr>userReq := uu1\<rparr>) = owner (s1\<lparr>userReq := uu2\<rparr>) \<and> pendingSApiReqs (s\<lparr>userReq := uu1\<rparr>) = pendingSApiReqs (s1\<lparr>userReq := uu2\<rparr>) \<and> sApiReq (s\<lparr>userReq := uu1\<rparr>) = sApiReq (s1\<lparr>userReq := uu2\<rparr>) \<and> serverApiIDs (s\<lparr>userReq := uu1\<rparr>) = serverApiIDs (s1\<lparr>userReq := uu2\<rparr>) \<and> serverPass (s\<lparr>userReq := uu1\<rparr>) = serverPass (s1\<lparr>userReq := uu2\<rparr>) \<and> outerPostIDs (s\<lparr>userReq := uu1\<rparr>) = outerPostIDs (s1\<lparr>userReq := uu2\<rparr>) \<and> outerPost (s\<lparr>userReq := uu1\<rparr>) = outerPost (s1\<lparr>userReq := uu2\<rparr>) \<and> outerVis (s\<lparr>userReq := uu1\<rparr>) = outerVis (s1\<lparr>userReq := uu2\<rparr>) \<and> outerOwner (s\<lparr>userReq := uu1\<rparr>) = outerOwner (s1\<lparr>userReq := uu2\<rparr>) \<and> sentOuterFriendIDs (s\<lparr>userReq := uu1\<rparr>) = sentOuterFriendIDs (s1\<lparr>userReq := uu2\<rparr>) \<and> recvOuterFriendIDs (s\<lparr>userReq := uu1\<rparr>) = recvOuterFriendIDs (s1\<lparr>userReq := uu2\<rparr>) \<and> pendingCApiReqs (s\<lparr>userReq := uu1\<rparr>) = pendingCApiReqs (s1\<lparr>userReq := uu2\<rparr>) \<and> cApiReq (s\<lparr>userReq := uu1\<rparr>) = cApiReq (s1\<lparr>userReq := uu2\<rparr>) \<and> clientApiIDs (s\<lparr>userReq := uu1\<rparr>) = clientApiIDs (s1\<lparr>userReq := uu2\<rparr>) \<and> clientPass (s\<lparr>userReq := uu1\<rparr>) = clientPass (s1\<lparr>userReq := uu2\<rparr>) \<and> sharedWith (s\<lparr>userReq := uu1\<rparr>) = sharedWith (s1\<lparr>userReq := uu2\<rparr>))) &&& ((\<And>uu1 uu2. \<lbrakk>admin s = admin s1 \<and> pendingUReqs s = pendingUReqs s1 \<and> userReq s = userReq s1 \<and> userIDs s = userIDs s1 \<and> user s = user s1 \<and> pass s = pass s1 \<and> eqButUIDf (pendingFReqs s) (pendingFReqs s1) \<and> eqButUID12 (friendReq s) (friendReq s1) \<and> eqButUIDf (friendIDs s) (friendIDs s1) \<and> postIDs s = postIDs s1 \<and> admin s = admin s1 \<and> post s = post s1 \<and> vis s = vis s1 \<and> owner s = owner s1 \<and> pendingSApiReqs s = pendingSApiReqs s1 \<and> sApiReq s = sApiReq s1 \<and> serverApiIDs s = serverApiIDs s1 \<and> serverPass s = serverPass s1 \<and> outerPostIDs s = outerPostIDs s1 \<and> outerPost s = outerPost s1 \<and> outerVis s = outerVis s1 \<and> outerOwner s = outerOwner s1 \<and> sentOuterFriendIDs s = sentOuterFriendIDs s1 \<and> recvOuterFriendIDs s = recvOuterFriendIDs s1 \<and> pendingCApiReqs s = pendingCApiReqs s1 \<and> cApiReq s = cApiReq s1 \<and> clientApiIDs s = clientApiIDs s1 \<and> clientPass s = clientPass s1 \<and> sharedWith s = sharedWith s1; uu1 = uu2\<rbrakk> \<Longrightarrow> admin (s\<lparr>userIDs := uu1\<rparr>) = admin (s1\<lparr>userIDs := uu2\<rparr>) \<and> pendingUReqs (s\<lparr>userIDs := uu1\<rparr>) = pendingUReqs (s1\<lparr>userIDs := uu2\<rparr>) \<and> userReq (s\<lparr>userIDs := uu1\<rparr>) = userReq (s1\<lparr>userIDs := uu2\<rparr>) \<and> userIDs (s\<lparr>userIDs := uu1\<rparr>) = userIDs (s1\<lparr>userIDs := uu2\<rparr>) \<and> user (s\<lparr>userIDs := uu1\<rparr>) = user (s1\<lparr>userIDs := uu2\<rparr>) \<and> pass (s\<lparr>userIDs := uu1\<rparr>) = pass (s1\<lparr>userIDs := uu2\<rparr>) \<and> eqButUIDf (pendingFReqs (s\<lparr>userIDs := uu1\<rparr>)) (pendingFReqs (s1\<lparr>userIDs := uu2\<rparr>)) \<and> eqButUID12 (friendReq (s\<lparr>userIDs := uu1\<rparr>)) (friendReq (s1\<lparr>userIDs := uu2\<rparr>)) \<and> eqButUIDf (friendIDs (s\<lparr>userIDs := uu1\<rparr>)) (friendIDs (s1\<lparr>userIDs := uu2\<rparr>)) \<and> postIDs (s\<lparr>userIDs := uu1\<rparr>) = postIDs (s1\<lparr>userIDs := uu2\<rparr>) \<and> admin (s\<lparr>userIDs := uu1\<rparr>) = admin (s1\<lparr>userIDs := uu2\<rparr>) \<and> post (s\<lparr>userIDs := uu1\<rparr>) = post (s1\<lparr>userIDs := uu2\<rparr>) \<and> vis (s\<lparr>userIDs := uu1\<rparr>) = vis (s1\<lparr>userIDs := uu2\<rparr>) \<and> owner (s\<lparr>userIDs := uu1\<rparr>) = owner (s1\<lparr>userIDs := uu2\<rparr>) \<and> pendingSApiReqs (s\<lparr>userIDs := uu1\<rparr>) = pendingSApiReqs (s1\<lparr>userIDs := uu2\<rparr>) \<and> sApiReq (s\<lparr>userIDs := uu1\<rparr>) = sApiReq (s1\<lparr>userIDs := uu2\<rparr>) \<and> serverApiIDs (s\<lparr>userIDs := uu1\<rparr>) = serverApiIDs (s1\<lparr>userIDs := uu2\<rparr>) \<and> serverPass (s\<lparr>userIDs := uu1\<rparr>) = serverPass (s1\<lparr>userIDs := uu2\<rparr>) \<and> outerPostIDs (s\<lparr>userIDs := uu1\<rparr>) = outerPostIDs (s1\<lparr>userIDs := uu2\<rparr>) \<and> outerPost (s\<lparr>userIDs := uu1\<rparr>) = outerPost (s1\<lparr>userIDs := uu2\<rparr>) \<and> outerVis (s\<lparr>userIDs := uu1\<rparr>) = outerVis (s1\<lparr>userIDs := uu2\<rparr>) \<and> outerOwner (s\<lparr>userIDs := uu1\<rparr>) = outerOwner (s1\<lparr>userIDs := uu2\<rparr>) \<and> sentOuterFriendIDs (s\<lparr>userIDs := uu1\<rparr>) = sentOuterFriendIDs (s1\<lparr>userIDs := uu2\<rparr>) \<and> recvOuterFriendIDs (s\<lparr>userIDs := uu1\<rparr>) = recvOuterFriendIDs (s1\<lparr>userIDs := uu2\<rparr>) \<and> pendingCApiReqs (s\<lparr>userIDs := uu1\<rparr>) = pendingCApiReqs (s1\<lparr>userIDs := uu2\<rparr>) \<and> cApiReq (s\<lparr>userIDs := uu1\<rparr>) = cApiReq (s1\<lparr>userIDs := uu2\<rparr>) \<and> clientApiIDs (s\<lparr>userIDs := uu1\<rparr>) = clientApiIDs (s1\<lparr>userIDs := uu2\<rparr>) \<and> clientPass (s\<lparr>userIDs := uu1\<rparr>) = clientPass (s1\<lparr>userIDs := uu2\<rparr>) \<and> sharedWith (s\<lparr>userIDs := uu1\<rparr>) = sharedWith (s1\<lparr>userIDs := uu2\<rparr>)) &&& (\<And>uu1 uu2. \<lbrakk>admin s = admin s1 \<and> pendingUReqs s = pendingUReqs s1 \<and> userReq s = userReq s1 \<and> userIDs s = userIDs s1 \<and> user s = user s1 \<and> pass s = pass s1 \<and> eqButUIDf (pendingFReqs s) (pendingFReqs s1) \<and> eqButUID12 (friendReq s) (friendReq s1) \<and> eqButUIDf (friendIDs s) (friendIDs s1) \<and> postIDs s = postIDs s1 \<and> admin s = admin s1 \<and> post s = post s1 \<and> vis s = vis s1 \<and> owner s = owner s1 \<and> pendingSApiReqs s = pendingSApiReqs s1 \<and> sApiReq s = sApiReq s1 \<and> serverApiIDs s = serverApiIDs s1 \<and> serverPass s = serverPass s1 \<and> outerPostIDs s = outerPostIDs s1 \<and> outerPost s = outerPost s1 \<and> outerVis s = outerVis s1 \<and> outerOwner s = outerOwner s1 \<and> sentOuterFriendIDs s = sentOuterFriendIDs s1 \<and> recvOuterFriendIDs s = recvOuterFriendIDs s1 \<and> pendingCApiReqs s = pendingCApiReqs s1 \<and> cApiReq s = cApiReq s1 \<and> clientApiIDs s = clientApiIDs s1 \<and> clientPass s = clientPass s1 \<and> sharedWith s = sharedWith s1; uu1 = uu2\<rbrakk> \<Longrightarrow> admin (s\<lparr>user := uu1\<rparr>) = admin (s1\<lparr>user := uu2\<rparr>) \<and> pendingUReqs (s\<lparr>user := uu1\<rparr>) = pendingUReqs (s1\<lparr>user := uu2\<rparr>) \<and> userReq (s\<lparr>user := uu1\<rparr>) = userReq (s1\<lparr>user := uu2\<rparr>) \<and> userIDs (s\<lparr>user := uu1\<rparr>) = userIDs (s1\<lparr>user := uu2\<rparr>) \<and> user (s\<lparr>user := uu1\<rparr>) = user (s1\<lparr>user := uu2\<rparr>) \<and> pass (s\<lparr>user := uu1\<rparr>) = pass (s1\<lparr>user := uu2\<rparr>) \<and> eqButUIDf (pendingFReqs (s\<lparr>user := uu1\<rparr>)) (pendingFReqs (s1\<lparr>user := uu2\<rparr>)) \<and> eqButUID12 (friendReq (s\<lparr>user := uu1\<rparr>)) (friendReq (s1\<lparr>user := uu2\<rparr>)) \<and> eqButUIDf (friendIDs (s\<lparr>user := uu1\<rparr>)) (friendIDs (s1\<lparr>user := uu2\<rparr>)) \<and> postIDs (s\<lparr>user := uu1\<rparr>) = postIDs (s1\<lparr>user := uu2\<rparr>) \<and> admin (s\<lparr>user := uu1\<rparr>) = admin (s1\<lparr>user := uu2\<rparr>) \<and> post (s\<lparr>user := uu1\<rparr>) = post (s1\<lparr>user := uu2\<rparr>) \<and> vis (s\<lparr>user := uu1\<rparr>) = vis (s1\<lparr>user := uu2\<rparr>) \<and> owner (s\<lparr>user := uu1\<rparr>) = owner (s1\<lparr>user := uu2\<rparr>) \<and> pendingSApiReqs (s\<lparr>user := uu1\<rparr>) = pendingSApiReqs (s1\<lparr>user := uu2\<rparr>) \<and> sApiReq (s\<lparr>user := uu1\<rparr>) = sApiReq (s1\<lparr>user := uu2\<rparr>) \<and> serverApiIDs (s\<lparr>user := uu1\<rparr>) = serverApiIDs (s1\<lparr>user := uu2\<rparr>) \<and> serverPass (s\<lparr>user := uu1\<rparr>) = serverPass (s1\<lparr>user := uu2\<rparr>) \<and> outerPostIDs (s\<lparr>user := uu1\<rparr>) = outerPostIDs (s1\<lparr>user := uu2\<rparr>) \<and> outerPost (s\<lparr>user := uu1\<rparr>) = outerPost (s1\<lparr>user := uu2\<rparr>) \<and> outerVis (s\<lparr>user := uu1\<rparr>) = outerVis (s1\<lparr>user := uu2\<rparr>) \<and> outerOwner (s\<lparr>user := uu1\<rparr>) = outerOwner (s1\<lparr>user := uu2\<rparr>) \<and> sentOuterFriendIDs (s\<lparr>user := uu1\<rparr>) = sentOuterFriendIDs (s1\<lparr>user := uu2\<rparr>) \<and> recvOuterFriendIDs (s\<lparr>user := uu1\<rparr>) = recvOuterFriendIDs (s1\<lparr>user := uu2\<rparr>) \<and> pendingCApiReqs (s\<lparr>user := uu1\<rparr>) = pendingCApiReqs (s1\<lparr>user := uu2\<rparr>) \<and> cApiReq (s\<lparr>user := uu1\<rparr>) = cApiReq (s1\<lparr>user := uu2\<rparr>) \<and> clientApiIDs (s\<lparr>user := uu1\<rparr>) = clientApiIDs (s1\<lparr>user := uu2\<rparr>) \<and> clientPass (s\<lparr>user := uu1\<rparr>) = clientPass (s1\<lparr>user := uu2\<rparr>) \<and> sharedWith (s\<lparr>user := uu1\<rparr>) = sharedWith (s1\<lparr>user := uu2\<rparr>))) &&& (\<And>uu1 uu2. \<lbrakk>admin s = admin s1 \<and> pendingUReqs s = pendingUReqs s1 \<and> userReq s = userReq s1 \<and> userIDs s = userIDs s1 \<and> user s = user s1 \<and> pass s = pass s1 \<and> eqButUIDf (pendingFReqs s) (pendingFReqs s1) \<and> eqButUID12 (friendReq s) (friendReq s1) \<and> eqButUIDf (friendIDs s) (friendIDs s1) \<and> postIDs s = postIDs s1 \<and> admin s = admin s1 \<and> post s = post s1 \<and> vis s = vis s1 \<and> owner s = owner s1 \<and> pendingSApiReqs s = pendingSApiReqs s1 \<and> sApiReq s = sApiReq s1 \<and> serverApiIDs s = serverApiIDs s1 \<and> serverPass s = serverPass s1 \<and> outerPostIDs s = outerPostIDs s1 \<and> outerPost s = outerPost s1 \<and> outerVis s = outerVis s1 \<and> outerOwner s = outerOwner s1 \<and> sentOuterFriendIDs s = sentOuterFriendIDs s1 \<and> recvOuterFriendIDs s = recvOuterFriendIDs s1 \<and> pendingCApiReqs s = pendingCApiReqs s1 \<and> cApiReq s = cApiReq s1 \<and> clientApiIDs s = clientApiIDs s1 \<and> clientPass s = clientPass s1 \<and> sharedWith s = sharedWith s1; uu1 = uu2\<rbrakk> \<Longrightarrow> admin (s\<lparr>pass := uu1\<rparr>) = admin (s1\<lparr>pass := uu2\<rparr>) \<and> pendingUReqs (s\<lparr>pass := uu1\<rparr>) = pendingUReqs (s1\<lparr>pass := uu2\<rparr>) \<and> userReq (s\<lparr>pass := uu1\<rparr>) = userReq (s1\<lparr>pass := uu2\<rparr>) \<and> userIDs (s\<lparr>pass := uu1\<rparr>) = userIDs (s1\<lparr>pass := uu2\<rparr>) \<and> user (s\<lparr>pass := uu1\<rparr>) = user (s1\<lparr>pass := uu2\<rparr>) \<and> pass (s\<lparr>pass := uu1\<rparr>) = pass (s1\<lparr>pass := uu2\<rparr>) \<and> eqButUIDf (pendingFReqs (s\<lparr>pass := uu1\<rparr>)) (pendingFReqs (s1\<lparr>pass := uu2\<rparr>)) \<and> eqButUID12 (friendReq (s\<lparr>pass := uu1\<rparr>)) (friendReq (s1\<lparr>pass := uu2\<rparr>)) \<and> eqButUIDf (friendIDs (s\<lparr>pass := uu1\<rparr>)) (friendIDs (s1\<lparr>pass := uu2\<rparr>)) \<and> postIDs (s\<lparr>pass := uu1\<rparr>) = postIDs (s1\<lparr>pass := uu2\<rparr>) \<and> admin (s\<lparr>pass := uu1\<rparr>) = admin (s1\<lparr>pass := uu2\<rparr>) \<and> post (s\<lparr>pass := uu1\<rparr>) = post (s1\<lparr>pass := uu2\<rparr>) \<and> vis (s\<lparr>pass := uu1\<rparr>) = vis (s1\<lparr>pass := uu2\<rparr>) \<and> owner (s\<lparr>pass := uu1\<rparr>) = owner (s1\<lparr>pass := uu2\<rparr>) \<and> pendingSApiReqs (s\<lparr>pass := uu1\<rparr>) = pendingSApiReqs (s1\<lparr>pass := uu2\<rparr>) \<and> sApiReq (s\<lparr>pass := uu1\<rparr>) = sApiReq (s1\<lparr>pass := uu2\<rparr>) \<and> serverApiIDs (s\<lparr>pass := uu1\<rparr>) = serverApiIDs (s1\<lparr>pass := uu2\<rparr>) \<and> serverPass (s\<lparr>pass := uu1\<rparr>) = serverPass (s1\<lparr>pass := uu2\<rparr>) \<and> outerPostIDs (s\<lparr>pass := uu1\<rparr>) = outerPostIDs (s1\<lparr>pass := uu2\<rparr>) \<and> outerPost (s\<lparr>pass := uu1\<rparr>) = outerPost (s1\<lparr>pass := uu2\<rparr>) \<and> outerVis (s\<lparr>pass := uu1\<rparr>) = outerVis (s1\<lparr>pass := uu2\<rparr>) \<and> outerOwner (s\<lparr>pass := uu1\<rparr>) = outerOwner (s1\<lparr>pass := uu2\<rparr>) \<and> sentOuterFriendIDs (s\<lparr>pass := uu1\<rparr>) = sentOuterFriendIDs (s1\<lparr>pass := uu2\<rparr>) \<and> recvOuterFriendIDs (s\<lparr>pass := uu1\<rparr>) = recvOuterFriendIDs (s1\<lparr>pass := uu2\<rparr>) \<and> pendingCApiReqs (s\<lparr>pass := uu1\<rparr>) = pendingCApiReqs (s1\<lparr>pass := uu2\<rparr>) \<and> cApiReq (s\<lparr>pass := uu1\<rparr>) = cApiReq (s1\<lparr>pass := uu2\<rparr>) \<and> clientApiIDs (s\<lparr>pass := uu1\<rparr>) = clientApiIDs (s1\<lparr>pass := uu2\<rparr>) \<and> clientPass (s\<lparr>pass := uu1\<rparr>) = clientPass (s1\<lparr>pass := uu2\<rparr>) \<and> sharedWith (s\<lparr>pass := uu1\<rparr>) = sharedWith (s1\<lparr>pass := uu2\<rparr>)) &&& (\<And>uu1 uu2. \<lbrakk>admin s = admin s1 \<and> pendingUReqs s = pendingUReqs s1 \<and> userReq s = userReq s1 \<and> userIDs s = userIDs s1 \<and> user s = user s1 \<and> pass s = pass s1 \<and> eqButUIDf (pendingFReqs s) (pendingFReqs s1) \<and> eqButUID12 (friendReq s) (friendReq s1) \<and> eqButUIDf (friendIDs s) (friendIDs s1) \<and> postIDs s = postIDs s1 \<and> admin s = admin s1 \<and> post s = post s1 \<and> vis s = vis s1 \<and> owner s = owner s1 \<and> pendingSApiReqs s = pendingSApiReqs s1 \<and> sApiReq s = sApiReq s1 \<and> serverApiIDs s = serverApiIDs s1 \<and> serverPass s = serverPass s1 \<and> outerPostIDs s = outerPostIDs s1 \<and> outerPost s = outerPost s1 \<and> outerVis s = outerVis s1 \<and> outerOwner s = outerOwner s1 \<and> sentOuterFriendIDs s = sentOuterFriendIDs s1 \<and> recvOuterFriendIDs s = recvOuterFriendIDs s1 \<and> pendingCApiReqs s = pendingCApiReqs s1 \<and> cApiReq s = cApiReq s1 \<and> clientApiIDs s = clientApiIDs s1 \<and> clientPass s = clientPass s1 \<and> sharedWith s = sharedWith s1; uu1 = uu2\<rbrakk> \<Longrightarrow> admin (s\<lparr>postIDs := uu1\<rparr>) = admin (s1\<lparr>postIDs := uu2\<rparr>) \<and> pendingUReqs (s\<lparr>postIDs := uu1\<rparr>) = pendingUReqs (s1\<lparr>postIDs := uu2\<rparr>) \<and> userReq (s\<lparr>postIDs := uu1\<rparr>) = userReq (s1\<lparr>postIDs := uu2\<rparr>) \<and> userIDs (s\<lparr>postIDs := uu1\<rparr>) = userIDs (s1\<lparr>postIDs := uu2\<rparr>) \<and> user (s\<lparr>postIDs := uu1\<rparr>) = user (s1\<lparr>postIDs := uu2\<rparr>) \<and> pass (s\<lparr>postIDs := uu1\<rparr>) = pass (s1\<lparr>postIDs := uu2\<rparr>) \<and> eqButUIDf (pendingFReqs (s\<lparr>postIDs := uu1\<rparr>)) (pendingFReqs (s1\<lparr>postIDs := uu2\<rparr>)) \<and> eqButUID12 (friendReq (s\<lparr>postIDs := uu1\<rparr>)) (friendReq (s1\<lparr>postIDs := uu2\<rparr>)) \<and> eqButUIDf (friendIDs (s\<lparr>postIDs := uu1\<rparr>)) (friendIDs (s1\<lparr>postIDs := uu2\<rparr>)) \<and> postIDs (s\<lparr>postIDs := uu1\<rparr>) = postIDs (s1\<lparr>postIDs := uu2\<rparr>) \<and> admin (s\<lparr>postIDs := uu1\<rparr>) = admin (s1\<lparr>postIDs := uu2\<rparr>) \<and> post (s\<lparr>postIDs := uu1\<rparr>) = post (s1\<lparr>postIDs := uu2\<rparr>) \<and> vis (s\<lparr>postIDs := uu1\<rparr>) = vis (s1\<lparr>postIDs := uu2\<rparr>) \<and> owner (s\<lparr>postIDs := uu1\<rparr>) = owner (s1\<lparr>postIDs := uu2\<rparr>) \<and> pendingSApiReqs (s\<lparr>postIDs := uu1\<rparr>) = pendingSApiReqs (s1\<lparr>postIDs := uu2\<rparr>) \<and> sApiReq (s\<lparr>postIDs := uu1\<rparr>) = sApiReq (s1\<lparr>postIDs := uu2\<rparr>) \<and> serverApiIDs (s\<lparr>postIDs := uu1\<rparr>) = serverApiIDs (s1\<lparr>postIDs := uu2\<rparr>) \<and> serverPass (s\<lparr>postIDs := uu1\<rparr>) = serverPass (s1\<lparr>postIDs := uu2\<rparr>) \<and> outerPostIDs (s\<lparr>postIDs := uu1\<rparr>) = outerPostIDs (s1\<lparr>postIDs := uu2\<rparr>) \<and> outerPost (s\<lparr>postIDs := uu1\<rparr>) = outerPost (s1\<lparr>postIDs := uu2\<rparr>) \<and> outerVis (s\<lparr>postIDs := uu1\<rparr>) = outerVis (s1\<lparr>postIDs := uu2\<rparr>) \<and> outerOwner (s\<lparr>postIDs := uu1\<rparr>) = outerOwner (s1\<lparr>postIDs := uu2\<rparr>) \<and> sentOuterFriendIDs (s\<lparr>postIDs := uu1\<rparr>) = sentOuterFriendIDs (s1\<lparr>postIDs := uu2\<rparr>) \<and> recvOuterFriendIDs (s\<lparr>postIDs := uu1\<rparr>) = recvOuterFriendIDs (s1\<lparr>postIDs := uu2\<rparr>) \<and> pendingCApiReqs (s\<lparr>postIDs := uu1\<rparr>) = pendingCApiReqs (s1\<lparr>postIDs := uu2\<rparr>) \<and> cApiReq (s\<lparr>postIDs := uu1\<rparr>) = cApiReq (s1\<lparr>postIDs := uu2\<rparr>) \<and> clientApiIDs (s\<lparr>postIDs := uu1\<rparr>) = clientApiIDs (s1\<lparr>postIDs := uu2\<rparr>) \<and> clientPass (s\<lparr>postIDs := uu1\<rparr>) = clientPass (s1\<lparr>postIDs := uu2\<rparr>) \<and> sharedWith (s\<lparr>postIDs := uu1\<rparr>) = sharedWith (s1\<lparr>postIDs := uu2\<rparr>))) &&& ((\<And>uu1 uu2. \<lbrakk>admin s = admin s1 \<and> pendingUReqs s = pendingUReqs s1 \<and> userReq s = userReq s1 \<and> userIDs s = userIDs s1 \<and> user s = user s1 \<and> pass s = pass s1 \<and> eqButUIDf (pendingFReqs s) (pendingFReqs s1) \<and> eqButUID12 (friendReq s) (friendReq s1) \<and> eqButUIDf (friendIDs s) (friendIDs s1) \<and> postIDs s = postIDs s1 \<and> admin s = admin s1 \<and> post s = post s1 \<and> vis s = vis s1 \<and> owner s = owner s1 \<and> pendingSApiReqs s = pendingSApiReqs s1 \<and> sApiReq s = sApiReq s1 \<and> serverApiIDs s = serverApiIDs s1 \<and> serverPass s = serverPass s1 \<and> outerPostIDs s = outerPostIDs s1 \<and> outerPost s = outerPost s1 \<and> outerVis s = outerVis s1 \<and> outerOwner s = outerOwner s1 \<and> sentOuterFriendIDs s = sentOuterFriendIDs s1 \<and> recvOuterFriendIDs s = recvOuterFriendIDs s1 \<and> pendingCApiReqs s = pendingCApiReqs s1 \<and> cApiReq s = cApiReq s1 \<and> clientApiIDs s = clientApiIDs s1 \<and> clientPass s = clientPass s1 \<and> sharedWith s = sharedWith s1; uu1 = uu2\<rbrakk> \<Longrightarrow> admin (s\<lparr>owner := uu1\<rparr>) = admin (s1\<lparr>owner := uu2\<rparr>) \<and> pendingUReqs (s\<lparr>owner := uu1\<rparr>) = pendingUReqs (s1\<lparr>owner := uu2\<rparr>) \<and> userReq (s\<lparr>owner := uu1\<rparr>) = userReq (s1\<lparr>owner := uu2\<rparr>) \<and> userIDs (s\<lparr>owner := uu1\<rparr>) = userIDs (s1\<lparr>owner := uu2\<rparr>) \<and> user (s\<lparr>owner := uu1\<rparr>) = user (s1\<lparr>owner := uu2\<rparr>) \<and> pass (s\<lparr>owner := uu1\<rparr>) = pass (s1\<lparr>owner := uu2\<rparr>) \<and> eqButUIDf (pendingFReqs (s\<lparr>owner := uu1\<rparr>)) (pendingFReqs (s1\<lparr>owner := uu2\<rparr>)) \<and> eqButUID12 (friendReq (s\<lparr>owner := uu1\<rparr>)) (friendReq (s1\<lparr>owner := uu2\<rparr>)) \<and> eqButUIDf (friendIDs (s\<lparr>owner := uu1\<rparr>)) (friendIDs (s1\<lparr>owner := uu2\<rparr>)) \<and> postIDs (s\<lparr>owner := uu1\<rparr>) = postIDs (s1\<lparr>owner := uu2\<rparr>) \<and> admin (s\<lparr>owner := uu1\<rparr>) = admin (s1\<lparr>owner := uu2\<rparr>) \<and> post (s\<lparr>owner := uu1\<rparr>) = post (s1\<lparr>owner := uu2\<rparr>) \<and> vis (s\<lparr>owner := uu1\<rparr>) = vis (s1\<lparr>owner := uu2\<rparr>) \<and> owner (s\<lparr>owner := uu1\<rparr>) = owner (s1\<lparr>owner := uu2\<rparr>) \<and> pendingSApiReqs (s\<lparr>owner := uu1\<rparr>) = pendingSApiReqs (s1\<lparr>owner := uu2\<rparr>) \<and> sApiReq (s\<lparr>owner := uu1\<rparr>) = sApiReq (s1\<lparr>owner := uu2\<rparr>) \<and> serverApiIDs (s\<lparr>owner := uu1\<rparr>) = serverApiIDs (s1\<lparr>owner := uu2\<rparr>) \<and> serverPass (s\<lparr>owner := uu1\<rparr>) = serverPass (s1\<lparr>owner := uu2\<rparr>) \<and> outerPostIDs (s\<lparr>owner := uu1\<rparr>) = outerPostIDs (s1\<lparr>owner := uu2\<rparr>) \<and> outerPost (s\<lparr>owner := uu1\<rparr>) = outerPost (s1\<lparr>owner := uu2\<rparr>) \<and> outerVis (s\<lparr>owner := uu1\<rparr>) = outerVis (s1\<lparr>owner := uu2\<rparr>) \<and> outerOwner (s\<lparr>owner := uu1\<rparr>) = outerOwner (s1\<lparr>owner := uu2\<rparr>) \<and> sentOuterFriendIDs (s\<lparr>owner := uu1\<rparr>) = sentOuterFriendIDs (s1\<lparr>owner := uu2\<rparr>) \<and> recvOuterFriendIDs (s\<lparr>owner := uu1\<rparr>) = recvOuterFriendIDs (s1\<lparr>owner := uu2\<rparr>) \<and> pendingCApiReqs (s\<lparr>owner := uu1\<rparr>) = pendingCApiReqs (s1\<lparr>owner := uu2\<rparr>) \<and> cApiReq (s\<lparr>owner := uu1\<rparr>) = cApiReq (s1\<lparr>owner := uu2\<rparr>) \<and> clientApiIDs (s\<lparr>owner := uu1\<rparr>) = clientApiIDs (s1\<lparr>owner := uu2\<rparr>) \<and> clientPass (s\<lparr>owner := uu1\<rparr>) = clientPass (s1\<lparr>owner := uu2\<rparr>) \<and> sharedWith (s\<lparr>owner := uu1\<rparr>) = sharedWith (s1\<lparr>owner := uu2\<rparr>)) &&& (\<And>uu1 uu2. \<lbrakk>admin s = admin s1 \<and> pendingUReqs s = pendingUReqs s1 \<and> userReq s = userReq s1 \<and> userIDs s = userIDs s1 \<and> user s = user s1 \<and> pass s = pass s1 \<and> eqButUIDf (pendingFReqs s) (pendingFReqs s1) \<and> eqButUID12 (friendReq s) (friendReq s1) \<and> eqButUIDf (friendIDs s) (friendIDs s1) \<and> postIDs s = postIDs s1 \<and> admin s = admin s1 \<and> post s = post s1 \<and> vis s = vis s1 \<and> owner s = owner s1 \<and> pendingSApiReqs s = pendingSApiReqs s1 \<and> sApiReq s = sApiReq s1 \<and> serverApiIDs s = serverApiIDs s1 \<and> serverPass s = serverPass s1 \<and> outerPostIDs s = outerPostIDs s1 \<and> outerPost s = outerPost s1 \<and> outerVis s = outerVis s1 \<and> outerOwner s = outerOwner s1 \<and> sentOuterFriendIDs s = sentOuterFriendIDs s1 \<and> recvOuterFriendIDs s = recvOuterFriendIDs s1 \<and> pendingCApiReqs s = pendingCApiReqs s1 \<and> cApiReq s = cApiReq s1 \<and> clientApiIDs s = clientApiIDs s1 \<and> clientPass s = clientPass s1 \<and> sharedWith s = sharedWith s1; uu1 = uu2\<rbrakk> \<Longrightarrow> admin (s\<lparr>post := uu1\<rparr>) = admin (s1\<lparr>post := uu2\<rparr>) \<and> pendingUReqs (s\<lparr>post := uu1\<rparr>) = pendingUReqs (s1\<lparr>post := uu2\<rparr>) \<and> userReq (s\<lparr>post := uu1\<rparr>) = userReq (s1\<lparr>post := uu2\<rparr>) \<and> userIDs (s\<lparr>post := uu1\<rparr>) = userIDs (s1\<lparr>post := uu2\<rparr>) \<and> user (s\<lparr>post := uu1\<rparr>) = user (s1\<lparr>post := uu2\<rparr>) \<and> pass (s\<lparr>post := uu1\<rparr>) = pass (s1\<lparr>post := uu2\<rparr>) \<and> eqButUIDf (pendingFReqs (s\<lparr>post := uu1\<rparr>)) (pendingFReqs (s1\<lparr>post := uu2\<rparr>)) \<and> eqButUID12 (friendReq (s\<lparr>post := uu1\<rparr>)) (friendReq (s1\<lparr>post := uu2\<rparr>)) \<and> eqButUIDf (friendIDs (s\<lparr>post := uu1\<rparr>)) (friendIDs (s1\<lparr>post := uu2\<rparr>)) \<and> postIDs (s\<lparr>post := uu1\<rparr>) = postIDs (s1\<lparr>post := uu2\<rparr>) \<and> admin (s\<lparr>post := uu1\<rparr>) = admin (s1\<lparr>post := uu2\<rparr>) \<and> post (s\<lparr>post := uu1\<rparr>) = post (s1\<lparr>post := uu2\<rparr>) \<and> vis (s\<lparr>post := uu1\<rparr>) = vis (s1\<lparr>post := uu2\<rparr>) \<and> owner (s\<lparr>post := uu1\<rparr>) = owner (s1\<lparr>post := uu2\<rparr>) \<and> pendingSApiReqs (s\<lparr>post := uu1\<rparr>) = pendingSApiReqs (s1\<lparr>post := uu2\<rparr>) \<and> sApiReq (s\<lparr>post := uu1\<rparr>) = sApiReq (s1\<lparr>post := uu2\<rparr>) \<and> serverApiIDs (s\<lparr>post := uu1\<rparr>) = serverApiIDs (s1\<lparr>post := uu2\<rparr>) \<and> serverPass (s\<lparr>post := uu1\<rparr>) = serverPass (s1\<lparr>post := uu2\<rparr>) \<and> outerPostIDs (s\<lparr>post := uu1\<rparr>) = outerPostIDs (s1\<lparr>post := uu2\<rparr>) \<and> outerPost (s\<lparr>post := uu1\<rparr>) = outerPost (s1\<lparr>post := uu2\<rparr>) \<and> outerVis (s\<lparr>post := uu1\<rparr>) = outerVis (s1\<lparr>post := uu2\<rparr>) \<and> outerOwner (s\<lparr>post := uu1\<rparr>) = outerOwner (s1\<lparr>post := uu2\<rparr>) \<and> sentOuterFriendIDs (s\<lparr>post := uu1\<rparr>) = sentOuterFriendIDs (s1\<lparr>post := uu2\<rparr>) \<and> recvOuterFriendIDs (s\<lparr>post := uu1\<rparr>) = recvOuterFriendIDs (s1\<lparr>post := uu2\<rparr>) \<and> pendingCApiReqs (s\<lparr>post := uu1\<rparr>) = pendingCApiReqs (s1\<lparr>post := uu2\<rparr>) \<and> cApiReq (s\<lparr>post := uu1\<rparr>) = cApiReq (s1\<lparr>post := uu2\<rparr>) \<and> clientApiIDs (s\<lparr>post := uu1\<rparr>) = clientApiIDs (s1\<lparr>post := uu2\<rparr>) \<and> clientPass (s\<lparr>post := uu1\<rparr>) = clientPass (s1\<lparr>post := uu2\<rparr>) \<and> sharedWith (s\<lparr>post := uu1\<rparr>) = sharedWith (s1\<lparr>post := uu2\<rparr>)) &&& (\<And>uu1 uu2. \<lbrakk>admin s = admin s1 \<and> pendingUReqs s = pendingUReqs s1 \<and> userReq s = userReq s1 \<and> userIDs s = userIDs s1 \<and> user s = user s1 \<and> pass s = pass s1 \<and> eqButUIDf (pendingFReqs s) (pendingFReqs s1) \<and> eqButUID12 (friendReq s) (friendReq s1) \<and> eqButUIDf (friendIDs s) (friendIDs s1) \<and> postIDs s = postIDs s1 \<and> admin s = admin s1 \<and> post s = post s1 \<and> vis s = vis s1 \<and> owner s = owner s1 \<and> pendingSApiReqs s = pendingSApiReqs s1 \<and> sApiReq s = sApiReq s1 \<and> serverApiIDs s = serverApiIDs s1 \<and> serverPass s = serverPass s1 \<and> outerPostIDs s = outerPostIDs s1 \<and> outerPost s = outerPost s1 \<and> outerVis s = outerVis s1 \<and> outerOwner s = outerOwner s1 \<and> sentOuterFriendIDs s = sentOuterFriendIDs s1 \<and> recvOuterFriendIDs s = recvOuterFriendIDs s1 \<and> pendingCApiReqs s = pendingCApiReqs s1 \<and> cApiReq s = cApiReq s1 \<and> clientApiIDs s = clientApiIDs s1 \<and> clientPass s = clientPass s1 \<and> sharedWith s = sharedWith s1; uu1 = uu2\<rbrakk> \<Longrightarrow> admin (s\<lparr>vis := uu1\<rparr>) = admin (s1\<lparr>vis := uu2\<rparr>) \<and> pendingUReqs (s\<lparr>vis := uu1\<rparr>) = pendingUReqs (s1\<lparr>vis := uu2\<rparr>) \<and> userReq (s\<lparr>vis := uu1\<rparr>) = userReq (s1\<lparr>vis := uu2\<rparr>) \<and> userIDs (s\<lparr>vis := uu1\<rparr>) = userIDs (s1\<lparr>vis := uu2\<rparr>) \<and> user (s\<lparr>vis := uu1\<rparr>) = user (s1\<lparr>vis := uu2\<rparr>) \<and> pass (s\<lparr>vis := uu1\<rparr>) = pass (s1\<lparr>vis := uu2\<rparr>) \<and> eqButUIDf (pendingFReqs (s\<lparr>vis := uu1\<rparr>)) (pendingFReqs (s1\<lparr>vis := uu2\<rparr>)) \<and> eqButUID12 (friendReq (s\<lparr>vis := uu1\<rparr>)) (friendReq (s1\<lparr>vis := uu2\<rparr>)) \<and> eqButUIDf (friendIDs (s\<lparr>vis := uu1\<rparr>)) (friendIDs (s1\<lparr>vis := uu2\<rparr>)) \<and> postIDs (s\<lparr>vis := uu1\<rparr>) = postIDs (s1\<lparr>vis := uu2\<rparr>) \<and> admin (s\<lparr>vis := uu1\<rparr>) = admin (s1\<lparr>vis := uu2\<rparr>) \<and> post (s\<lparr>vis := uu1\<rparr>) = post (s1\<lparr>vis := uu2\<rparr>) \<and> vis (s\<lparr>vis := uu1\<rparr>) = vis (s1\<lparr>vis := uu2\<rparr>) \<and> owner (s\<lparr>vis := uu1\<rparr>) = owner (s1\<lparr>vis := uu2\<rparr>) \<and> pendingSApiReqs (s\<lparr>vis := uu1\<rparr>) = pendingSApiReqs (s1\<lparr>vis := uu2\<rparr>) \<and> sApiReq (s\<lparr>vis := uu1\<rparr>) = sApiReq (s1\<lparr>vis := uu2\<rparr>) \<and> serverApiIDs (s\<lparr>vis := uu1\<rparr>) = serverApiIDs (s1\<lparr>vis := uu2\<rparr>) \<and> serverPass (s\<lparr>vis := uu1\<rparr>) = serverPass (s1\<lparr>vis := uu2\<rparr>) \<and> outerPostIDs (s\<lparr>vis := uu1\<rparr>) = outerPostIDs (s1\<lparr>vis := uu2\<rparr>) \<and> outerPost (s\<lparr>vis := uu1\<rparr>) = outerPost (s1\<lparr>vis := uu2\<rparr>) \<and> outerVis (s\<lparr>vis := uu1\<rparr>) = outerVis (s1\<lparr>vis := uu2\<rparr>) \<and> outerOwner (s\<lparr>vis := uu1\<rparr>) = outerOwner (s1\<lparr>vis := uu2\<rparr>) \<and> sentOuterFriendIDs (s\<lparr>vis := uu1\<rparr>) = sentOuterFriendIDs (s1\<lparr>vis := uu2\<rparr>) \<and> recvOuterFriendIDs (s\<lparr>vis := uu1\<rparr>) = recvOuterFriendIDs (s1\<lparr>vis := uu2\<rparr>) \<and> pendingCApiReqs (s\<lparr>vis := uu1\<rparr>) = pendingCApiReqs (s1\<lparr>vis := uu2\<rparr>) \<and> cApiReq (s\<lparr>vis := uu1\<rparr>) = cApiReq (s1\<lparr>vis := uu2\<rparr>) \<and> clientApiIDs (s\<lparr>vis := uu1\<rparr>) = clientApiIDs (s1\<lparr>vis := uu2\<rparr>) \<and> clientPass (s\<lparr>vis := uu1\<rparr>) = clientPass (s1\<lparr>vis := uu2\<rparr>) \<and> sharedWith (s\<lparr>vis := uu1\<rparr>) = sharedWith (s1\<lparr>vis := uu2\<rparr>))) &&& ((\<And>uu1 uu2. \<lbrakk>admin s = admin s1 \<and> pendingUReqs s = pendingUReqs s1 \<and> userReq s = userReq s1 \<and> userIDs s = userIDs s1 \<and> user s = user s1 \<and> pass s = pass s1 \<and> eqButUIDf (pendingFReqs s) (pendingFReqs s1) \<and> eqButUID12 (friendReq s) (friendReq s1) \<and> eqButUIDf (friendIDs s) (friendIDs s1) \<and> postIDs s = postIDs s1 \<and> admin s = admin s1 \<and> post s = post s1 \<and> vis s = vis s1 \<and> owner s = owner s1 \<and> pendingSApiReqs s = pendingSApiReqs s1 \<and> sApiReq s = sApiReq s1 \<and> serverApiIDs s = serverApiIDs s1 \<and> serverPass s = serverPass s1 \<and> outerPostIDs s = outerPostIDs s1 \<and> outerPost s = outerPost s1 \<and> outerVis s = outerVis s1 \<and> outerOwner s = outerOwner s1 \<and> sentOuterFriendIDs s = sentOuterFriendIDs s1 \<and> recvOuterFriendIDs s = recvOuterFriendIDs s1 \<and> pendingCApiReqs s = pendingCApiReqs s1 \<and> cApiReq s = cApiReq s1 \<and> clientApiIDs s = clientApiIDs s1 \<and> clientPass s = clientPass s1 \<and> sharedWith s = sharedWith s1; eqButUIDf uu1 uu2\<rbrakk> \<Longrightarrow> admin (s\<lparr>pendingFReqs := uu1\<rparr>) = admin (s1\<lparr>pendingFReqs := uu2\<rparr>) \<and> pendingUReqs (s\<lparr>pendingFReqs := uu1\<rparr>) = pendingUReqs (s1\<lparr>pendingFReqs := uu2\<rparr>) \<and> userReq (s\<lparr>pendingFReqs := uu1\<rparr>) = userReq (s1\<lparr>pendingFReqs := uu2\<rparr>) \<and> userIDs (s\<lparr>pendingFReqs := uu1\<rparr>) = userIDs (s1\<lparr>pendingFReqs := uu2\<rparr>) \<and> user (s\<lparr>pendingFReqs := uu1\<rparr>) = user (s1\<lparr>pendingFReqs := uu2\<rparr>) \<and> pass (s\<lparr>pendingFReqs := uu1\<rparr>) = pass (s1\<lparr>pendingFReqs := uu2\<rparr>) \<and> eqButUIDf (pendingFReqs (s\<lparr>pendingFReqs := uu1\<rparr>)) (pendingFReqs (s1\<lparr>pendingFReqs := uu2\<rparr>)) \<and> eqButUID12 (friendReq (s\<lparr>pendingFReqs := uu1\<rparr>)) (friendReq (s1\<lparr>pendingFReqs := uu2\<rparr>)) \<and> eqButUIDf (friendIDs (s\<lparr>pendingFReqs := uu1\<rparr>)) (friendIDs (s1\<lparr>pendingFReqs := uu2\<rparr>)) \<and> postIDs (s\<lparr>pendingFReqs := uu1\<rparr>) = postIDs (s1\<lparr>pendingFReqs := uu2\<rparr>) \<and> admin (s\<lparr>pendingFReqs := uu1\<rparr>) = admin (s1\<lparr>pendingFReqs := uu2\<rparr>) \<and> post (s\<lparr>pendingFReqs := uu1\<rparr>) = post (s1\<lparr>pendingFReqs := uu2\<rparr>) \<and> vis (s\<lparr>pendingFReqs := uu1\<rparr>) = vis (s1\<lparr>pendingFReqs := uu2\<rparr>) \<and> owner (s\<lparr>pendingFReqs := uu1\<rparr>) = owner (s1\<lparr>pendingFReqs := uu2\<rparr>) \<and> pendingSApiReqs (s\<lparr>pendingFReqs := uu1\<rparr>) = pendingSApiReqs (s1\<lparr>pendingFReqs := uu2\<rparr>) \<and> sApiReq (s\<lparr>pendingFReqs := uu1\<rparr>) = sApiReq (s1\<lparr>pendingFReqs := uu2\<rparr>) \<and> serverApiIDs (s\<lparr>pendingFReqs := uu1\<rparr>) = serverApiIDs (s1\<lparr>pendingFReqs := uu2\<rparr>) \<and> serverPass (s\<lparr>pendingFReqs := uu1\<rparr>) = serverPass (s1\<lparr>pendingFReqs := uu2\<rparr>) \<and> outerPostIDs (s\<lparr>pendingFReqs := uu1\<rparr>) = outerPostIDs (s1\<lparr>pendingFReqs := uu2\<rparr>) \<and> outerPost (s\<lparr>pendingFReqs := uu1\<rparr>) = outerPost (s1\<lparr>pendingFReqs := uu2\<rparr>) \<and> outerVis (s\<lparr>pendingFReqs := uu1\<rparr>) = outerVis (s1\<lparr>pendingFReqs := uu2\<rparr>) \<and> outerOwner (s\<lparr>pendingFReqs := uu1\<rparr>) = outerOwner (s1\<lparr>pendingFReqs := uu2\<rparr>) \<and> sentOuterFriendIDs (s\<lparr>pendingFReqs := uu1\<rparr>) = sentOuterFriendIDs (s1\<lparr>pendingFReqs := uu2\<rparr>) \<and> recvOuterFriendIDs (s\<lparr>pendingFReqs := uu1\<rparr>) = recvOuterFriendIDs (s1\<lparr>pendingFReqs := uu2\<rparr>) \<and> pendingCApiReqs (s\<lparr>pendingFReqs := uu1\<rparr>) = pendingCApiReqs (s1\<lparr>pendingFReqs := uu2\<rparr>) \<and> cApiReq (s\<lparr>pendingFReqs := uu1\<rparr>) = cApiReq (s1\<lparr>pendingFReqs := uu2\<rparr>) \<and> clientApiIDs (s\<lparr>pendingFReqs := uu1\<rparr>) = clientApiIDs (s1\<lparr>pendingFReqs := uu2\<rparr>) \<and> clientPass (s\<lparr>pendingFReqs := uu1\<rparr>) = clientPass (s1\<lparr>pendingFReqs := uu2\<rparr>) \<and> sharedWith (s\<lparr>pendingFReqs := uu1\<rparr>) = sharedWith (s1\<lparr>pendingFReqs := uu2\<rparr>)) &&& (\<And>uu1 uu2. \<lbrakk>admin s = admin s1 \<and> pendingUReqs s = pendingUReqs s1 \<and> userReq s = userReq s1 \<and> userIDs s = userIDs s1 \<and> user s = user s1 \<and> pass s = pass s1 \<and> eqButUIDf (pendingFReqs s) (pendingFReqs s1) \<and> eqButUID12 (friendReq s) (friendReq s1) \<and> eqButUIDf (friendIDs s) (friendIDs s1) \<and> postIDs s = postIDs s1 \<and> admin s = admin s1 \<and> post s = post s1 \<and> vis s = vis s1 \<and> owner s = owner s1 \<and> pendingSApiReqs s = pendingSApiReqs s1 \<and> sApiReq s = sApiReq s1 \<and> serverApiIDs s = serverApiIDs s1 \<and> serverPass s = serverPass s1 \<and> outerPostIDs s = outerPostIDs s1 \<and> outerPost s = outerPost s1 \<and> outerVis s = outerVis s1 \<and> outerOwner s = outerOwner s1 \<and> sentOuterFriendIDs s = sentOuterFriendIDs s1 \<and> recvOuterFriendIDs s = recvOuterFriendIDs s1 \<and> pendingCApiReqs s = pendingCApiReqs s1 \<and> cApiReq s = cApiReq s1 \<and> clientApiIDs s = clientApiIDs s1 \<and> clientPass s = clientPass s1 \<and> sharedWith s = sharedWith s1; eqButUID12 uu1 uu2\<rbrakk> \<Longrightarrow> admin (s\<lparr>friendReq := uu1\<rparr>) = admin (s1\<lparr>friendReq := uu2\<rparr>) \<and> pendingUReqs (s\<lparr>friendReq := uu1\<rparr>) = pendingUReqs (s1\<lparr>friendReq := uu2\<rparr>) \<and> userReq (s\<lparr>friendReq := uu1\<rparr>) = userReq (s1\<lparr>friendReq := uu2\<rparr>) \<and> userIDs (s\<lparr>friendReq := uu1\<rparr>) = userIDs (s1\<lparr>friendReq := uu2\<rparr>) \<and> user (s\<lparr>friendReq := uu1\<rparr>) = user (s1\<lparr>friendReq := uu2\<rparr>) \<and> pass (s\<lparr>friendReq := uu1\<rparr>) = pass (s1\<lparr>friendReq := uu2\<rparr>) \<and> eqButUIDf (pendingFReqs (s\<lparr>friendReq := uu1\<rparr>)) (pendingFReqs (s1\<lparr>friendReq := uu2\<rparr>)) \<and> eqButUID12 (friendReq (s\<lparr>friendReq := uu1\<rparr>)) (friendReq (s1\<lparr>friendReq := uu2\<rparr>)) \<and> eqButUIDf (friendIDs (s\<lparr>friendReq := uu1\<rparr>)) (friendIDs (s1\<lparr>friendReq := uu2\<rparr>)) \<and> postIDs (s\<lparr>friendReq := uu1\<rparr>) = postIDs (s1\<lparr>friendReq := uu2\<rparr>) \<and> admin (s\<lparr>friendReq := uu1\<rparr>) = admin (s1\<lparr>friendReq := uu2\<rparr>) \<and> post (s\<lparr>friendReq := uu1\<rparr>) = post (s1\<lparr>friendReq := uu2\<rparr>) \<and> vis (s\<lparr>friendReq := uu1\<rparr>) = vis (s1\<lparr>friendReq := uu2\<rparr>) \<and> owner (s\<lparr>friendReq := uu1\<rparr>) = owner (s1\<lparr>friendReq := uu2\<rparr>) \<and> pendingSApiReqs (s\<lparr>friendReq := uu1\<rparr>) = pendingSApiReqs (s1\<lparr>friendReq := uu2\<rparr>) \<and> sApiReq (s\<lparr>friendReq := uu1\<rparr>) = sApiReq (s1\<lparr>friendReq := uu2\<rparr>) \<and> serverApiIDs (s\<lparr>friendReq := uu1\<rparr>) = serverApiIDs (s1\<lparr>friendReq := uu2\<rparr>) \<and> serverPass (s\<lparr>friendReq := uu1\<rparr>) = serverPass (s1\<lparr>friendReq := uu2\<rparr>) \<and> outerPostIDs (s\<lparr>friendReq := uu1\<rparr>) = outerPostIDs (s1\<lparr>friendReq := uu2\<rparr>) \<and> outerPost (s\<lparr>friendReq := uu1\<rparr>) = outerPost (s1\<lparr>friendReq := uu2\<rparr>) \<and> outerVis (s\<lparr>friendReq := uu1\<rparr>) = outerVis (s1\<lparr>friendReq := uu2\<rparr>) \<and> outerOwner (s\<lparr>friendReq := uu1\<rparr>) = outerOwner (s1\<lparr>friendReq := uu2\<rparr>) \<and> sentOuterFriendIDs (s\<lparr>friendReq := uu1\<rparr>) = sentOuterFriendIDs (s1\<lparr>friendReq := uu2\<rparr>) \<and> recvOuterFriendIDs (s\<lparr>friendReq := uu1\<rparr>) = recvOuterFriendIDs (s1\<lparr>friendReq := uu2\<rparr>) \<and> pendingCApiReqs (s\<lparr>friendReq := uu1\<rparr>) = pendingCApiReqs (s1\<lparr>friendReq := uu2\<rparr>) \<and> cApiReq (s\<lparr>friendReq := uu1\<rparr>) = cApiReq (s1\<lparr>friendReq := uu2\<rparr>) \<and> clientApiIDs (s\<lparr>friendReq := uu1\<rparr>) = clientApiIDs (s1\<lparr>friendReq := uu2\<rparr>) \<and> clientPass (s\<lparr>friendReq := uu1\<rparr>) = clientPass (s1\<lparr>friendReq := uu2\<rparr>) \<and> sharedWith (s\<lparr>friendReq := uu1\<rparr>) = sharedWith (s1\<lparr>friendReq := uu2\<rparr>))) &&& (\<And>uu1 uu2. \<lbrakk>admin s = admin s1 \<and> pendingUReqs s = pendingUReqs s1 \<and> userReq s = userReq s1 \<and> userIDs s = userIDs s1 \<and> user s = user s1 \<and> pass s = pass s1 \<and> eqButUIDf (pendingFReqs s) (pendingFReqs s1) \<and> eqButUID12 (friendReq s) (friendReq s1) \<and> eqButUIDf (friendIDs s) (friendIDs s1) \<and> postIDs s = postIDs s1 \<and> admin s = admin s1 \<and> post s = post s1 \<and> vis s = vis s1 \<and> owner s = owner s1 \<and> pendingSApiReqs s = pendingSApiReqs s1 \<and> sApiReq s = sApiReq s1 \<and> serverApiIDs s = serverApiIDs s1 \<and> serverPass s = serverPass s1 \<and> outerPostIDs s = outerPostIDs s1 \<and> outerPost s = outerPost s1 \<and> outerVis s = outerVis s1 \<and> outerOwner s = outerOwner s1 \<and> sentOuterFriendIDs s = sentOuterFriendIDs s1 \<and> recvOuterFriendIDs s = recvOuterFriendIDs s1 \<and> pendingCApiReqs s = pendingCApiReqs s1 \<and> cApiReq s = cApiReq s1 \<and> clientApiIDs s = clientApiIDs s1 \<and> clientPass s = clientPass s1 \<and> sharedWith s = sharedWith s1; eqButUIDf uu1 uu2\<rbrakk> \<Longrightarrow> admin (s\<lparr>friendIDs := uu1\<rparr>) = admin (s1\<lparr>friendIDs := uu2\<rparr>) \<and> pendingUReqs (s\<lparr>friendIDs := uu1\<rparr>) = pendingUReqs (s1\<lparr>friendIDs := uu2\<rparr>) \<and> userReq (s\<lparr>friendIDs := uu1\<rparr>) = userReq (s1\<lparr>friendIDs := uu2\<rparr>) \<and> userIDs (s\<lparr>friendIDs := uu1\<rparr>) = userIDs (s1\<lparr>friendIDs := uu2\<rparr>) \<and> user (s\<lparr>friendIDs := uu1\<rparr>) = user (s1\<lparr>friendIDs := uu2\<rparr>) \<and> pass (s\<lparr>friendIDs := uu1\<rparr>) = pass (s1\<lparr>friendIDs := uu2\<rparr>) \<and> eqButUIDf (pendingFReqs (s\<lparr>friendIDs := uu1\<rparr>)) (pendingFReqs (s1\<lparr>friendIDs := uu2\<rparr>)) \<and> eqButUID12 (friendReq (s\<lparr>friendIDs := uu1\<rparr>)) (friendReq (s1\<lparr>friendIDs := uu2\<rparr>)) \<and> eqButUIDf (friendIDs (s\<lparr>friendIDs := uu1\<rparr>)) (friendIDs (s1\<lparr>friendIDs := uu2\<rparr>)) \<and> postIDs (s\<lparr>friendIDs := uu1\<rparr>) = postIDs (s1\<lparr>friendIDs := uu2\<rparr>) \<and> admin (s\<lparr>friendIDs := uu1\<rparr>) = admin (s1\<lparr>friendIDs := uu2\<rparr>) \<and> post (s\<lparr>friendIDs := uu1\<rparr>) = post (s1\<lparr>friendIDs := uu2\<rparr>) \<and> vis (s\<lparr>friendIDs := uu1\<rparr>) = vis (s1\<lparr>friendIDs := uu2\<rparr>) \<and> owner (s\<lparr>friendIDs := uu1\<rparr>) = owner (s1\<lparr>friendIDs := uu2\<rparr>) \<and> pendingSApiReqs (s\<lparr>friendIDs := uu1\<rparr>) = pendingSApiReqs (s1\<lparr>friendIDs := uu2\<rparr>) \<and> sApiReq (s\<lparr>friendIDs := uu1\<rparr>) = sApiReq (s1\<lparr>friendIDs := uu2\<rparr>) \<and> serverApiIDs (s\<lparr>friendIDs := uu1\<rparr>) = serverApiIDs (s1\<lparr>friendIDs := uu2\<rparr>) \<and> serverPass (s\<lparr>friendIDs := uu1\<rparr>) = serverPass (s1\<lparr>friendIDs := uu2\<rparr>) \<and> outerPostIDs (s\<lparr>friendIDs := uu1\<rparr>) = outerPostIDs (s1\<lparr>friendIDs := uu2\<rparr>) \<and> outerPost (s\<lparr>friendIDs := uu1\<rparr>) = outerPost (s1\<lparr>friendIDs := uu2\<rparr>) \<and> outerVis (s\<lparr>friendIDs := uu1\<rparr>) = outerVis (s1\<lparr>friendIDs := uu2\<rparr>) \<and> outerOwner (s\<lparr>friendIDs := uu1\<rparr>) = outerOwner (s1\<lparr>friendIDs := uu2\<rparr>) \<and> sentOuterFriendIDs (s\<lparr>friendIDs := uu1\<rparr>) = sentOuterFriendIDs (s1\<lparr>friendIDs := uu2\<rparr>) \<and> recvOuterFriendIDs (s\<lparr>friendIDs := uu1\<rparr>) = recvOuterFriendIDs (s1\<lparr>friendIDs := uu2\<rparr>) \<and> pendingCApiReqs (s\<lparr>friendIDs := uu1\<rparr>) = pendingCApiReqs (s1\<lparr>friendIDs := uu2\<rparr>) \<and> cApiReq (s\<lparr>friendIDs := uu1\<rparr>) = cApiReq (s1\<lparr>friendIDs := uu2\<rparr>) \<and> clientApiIDs (s\<lparr>friendIDs := uu1\<rparr>) = clientApiIDs (s1\<lparr>friendIDs := uu2\<rparr>) \<and> clientPass (s\<lparr>friendIDs := uu1\<rparr>) = clientPass (s1\<lparr>friendIDs := uu2\<rparr>) \<and> sharedWith (s\<lparr>friendIDs := uu1\<rparr>) = sharedWith (s1\<lparr>friendIDs := uu2\<rparr>)) &&& (\<And>uu1 uu2. \<lbrakk>admin s = admin s1 \<and> pendingUReqs s = pendingUReqs s1 \<and> userReq s = userReq s1 \<and> userIDs s = userIDs s1 \<and> user s = user s1 \<and> pass s = pass s1 \<and> eqButUIDf (pendingFReqs s) (pendingFReqs s1) \<and> eqButUID12 (friendReq s) (friendReq s1) \<and> eqButUIDf (friendIDs s) (friendIDs s1) \<and> postIDs s = postIDs s1 \<and> admin s = admin s1 \<and> post s = post s1 \<and> vis s = vis s1 \<and> owner s = owner s1 \<and> pendingSApiReqs s = pendingSApiReqs s1 \<and> sApiReq s = sApiReq s1 \<and> serverApiIDs s = serverApiIDs s1 \<and> serverPass s = serverPass s1 \<and> outerPostIDs s = outerPostIDs s1 \<and> outerPost s = outerPost s1 \<and> outerVis s = outerVis s1 \<and> outerOwner s = outerOwner s1 \<and> sentOuterFriendIDs s = sentOuterFriendIDs s1 \<and> recvOuterFriendIDs s = recvOuterFriendIDs s1 \<and> pendingCApiReqs s = pendingCApiReqs s1 \<and> cApiReq s = cApiReq s1 \<and> clientApiIDs s = clientApiIDs s1 \<and> clientPass s = clientPass s1 \<and> sharedWith s = sharedWith s1; uu1 = uu2\<rbrakk> \<Longrightarrow> admin (s\<lparr>pendingSApiReqs := uu1\<rparr>) = admin (s1\<lparr>pendingSApiReqs := uu2\<rparr>) \<and> pendingUReqs (s\<lparr>pendingSApiReqs := uu1\<rparr>) = pendingUReqs (s1\<lparr>pendingSApiReqs := uu2\<rparr>) \<and> userReq (s\<lparr>pendingSApiReqs := uu1\<rparr>) = userReq (s1\<lparr>pendingSApiReqs := uu2\<rparr>) \<and> userIDs (s\<lparr>pendingSApiReqs := uu1\<rparr>) = userIDs (s1\<lparr>pendingSApiReqs := uu2\<rparr>) \<and> user (s\<lparr>pendingSApiReqs := uu1\<rparr>) = user (s1\<lparr>pendingSApiReqs := uu2\<rparr>) \<and> pass (s\<lparr>pendingSApiReqs := uu1\<rparr>) = pass (s1\<lparr>pendingSApiReqs := uu2\<rparr>) \<and> eqButUIDf (pendingFReqs (s\<lparr>pendingSApiReqs := uu1\<rparr>)) (pendingFReqs (s1\<lparr>pendingSApiReqs := uu2\<rparr>)) \<and> eqButUID12 (friendReq (s\<lparr>pendingSApiReqs := uu1\<rparr>)) (friendReq (s1\<lparr>pendingSApiReqs := uu2\<rparr>)) \<and> eqButUIDf (friendIDs (s\<lparr>pendingSApiReqs := uu1\<rparr>)) (friendIDs (s1\<lparr>pendingSApiReqs := uu2\<rparr>)) \<and> postIDs (s\<lparr>pendingSApiReqs := uu1\<rparr>) = postIDs (s1\<lparr>pendingSApiReqs := uu2\<rparr>) \<and> admin (s\<lparr>pendingSApiReqs := uu1\<rparr>) = admin (s1\<lparr>pendingSApiReqs := uu2\<rparr>) \<and> post (s\<lparr>pendingSApiReqs := uu1\<rparr>) = post (s1\<lparr>pendingSApiReqs := uu2\<rparr>) \<and> vis (s\<lparr>pendingSApiReqs := uu1\<rparr>) = vis (s1\<lparr>pendingSApiReqs := uu2\<rparr>) \<and> owner (s\<lparr>pendingSApiReqs := uu1\<rparr>) = owner (s1\<lparr>pendingSApiReqs := uu2\<rparr>) \<and> pendingSApiReqs (s\<lparr>pendingSApiReqs := uu1\<rparr>) = pendingSApiReqs (s1\<lparr>pendingSApiReqs := uu2\<rparr>) \<and> sApiReq (s\<lparr>pendingSApiReqs := uu1\<rparr>) = sApiReq (s1\<lparr>pendingSApiReqs := uu2\<rparr>) \<and> serverApiIDs (s\<lparr>pendingSApiReqs := uu1\<rparr>) = serverApiIDs (s1\<lparr>pendingSApiReqs := uu2\<rparr>) \<and> serverPass (s\<lparr>pendingSApiReqs := uu1\<rparr>) = serverPass (s1\<lparr>pendingSApiReqs := uu2\<rparr>) \<and> outerPostIDs (s\<lparr>pendingSApiReqs := uu1\<rparr>) = outerPostIDs (s1\<lparr>pendingSApiReqs := uu2\<rparr>) \<and> outerPost (s\<lparr>pendingSApiReqs := uu1\<rparr>) = outerPost (s1\<lparr>pendingSApiReqs := uu2\<rparr>) \<and> outerVis (s\<lparr>pendingSApiReqs := uu1\<rparr>) = outerVis (s1\<lparr>pendingSApiReqs := uu2\<rparr>) \<and> outerOwner (s\<lparr>pendingSApiReqs := uu1\<rparr>) = outerOwner (s1\<lparr>pendingSApiReqs := uu2\<rparr>) \<and> sentOuterFriendIDs (s\<lparr>pendingSApiReqs := uu1\<rparr>) = sentOuterFriendIDs (s1\<lparr>pendingSApiReqs := uu2\<rparr>) \<and> recvOuterFriendIDs (s\<lparr>pendingSApiReqs := uu1\<rparr>) = recvOuterFriendIDs (s1\<lparr>pendingSApiReqs := uu2\<rparr>) \<and> pendingCApiReqs (s\<lparr>pendingSApiReqs := uu1\<rparr>) = pendingCApiReqs (s1\<lparr>pendingSApiReqs := uu2\<rparr>) \<and> cApiReq (s\<lparr>pendingSApiReqs := uu1\<rparr>) = cApiReq (s1\<lparr>pendingSApiReqs := uu2\<rparr>) \<and> clientApiIDs (s\<lparr>pendingSApiReqs := uu1\<rparr>) = clientApiIDs (s1\<lparr>pendingSApiReqs := uu2\<rparr>) \<and> clientPass (s\<lparr>pendingSApiReqs := uu1\<rparr>) = clientPass (s1\<lparr>pendingSApiReqs := uu2\<rparr>) \<and> sharedWith (s\<lparr>pendingSApiReqs := uu1\<rparr>) = sharedWith (s1\<lparr>pendingSApiReqs := uu2\<rparr>))) &&& (((\<And>uu1 uu2. \<lbrakk>admin s = admin s1 \<and> pendingUReqs s = pendingUReqs s1 \<and> userReq s = userReq s1 \<and> userIDs s = userIDs s1 \<and> user s = user s1 \<and> pass s = pass s1 \<and> eqButUIDf (pendingFReqs s) (pendingFReqs s1) \<and> eqButUID12 (friendReq s) (friendReq s1) \<and> eqButUIDf (friendIDs s) (friendIDs s1) \<and> postIDs s = postIDs s1 \<and> admin s = admin s1 \<and> post s = post s1 \<and> vis s = vis s1 \<and> owner s = owner s1 \<and> pendingSApiReqs s = pendingSApiReqs s1 \<and> sApiReq s = sApiReq s1 \<and> serverApiIDs s = serverApiIDs s1 \<and> serverPass s = serverPass s1 \<and> outerPostIDs s = outerPostIDs s1 \<and> outerPost s = outerPost s1 \<and> outerVis s = outerVis s1 \<and> outerOwner s = outerOwner s1 \<and> sentOuterFriendIDs s = sentOuterFriendIDs s1 \<and> recvOuterFriendIDs s = recvOuterFriendIDs s1 \<and> pendingCApiReqs s = pendingCApiReqs s1 \<and> cApiReq s = cApiReq s1 \<and> clientApiIDs s = clientApiIDs s1 \<and> clientPass s = clientPass s1 \<and> sharedWith s = sharedWith s1; uu1 = uu2\<rbrakk> \<Longrightarrow> admin (s\<lparr>sApiReq := uu1\<rparr>) = admin (s1\<lparr>sApiReq := uu2\<rparr>) \<and> pendingUReqs (s\<lparr>sApiReq := uu1\<rparr>) = pendingUReqs (s1\<lparr>sApiReq := uu2\<rparr>) \<and> userReq (s\<lparr>sApiReq := uu1\<rparr>) = userReq (s1\<lparr>sApiReq := uu2\<rparr>) \<and> userIDs (s\<lparr>sApiReq := uu1\<rparr>) = userIDs (s1\<lparr>sApiReq := uu2\<rparr>) \<and> user (s\<lparr>sApiReq := uu1\<rparr>) = user (s1\<lparr>sApiReq := uu2\<rparr>) \<and> pass (s\<lparr>sApiReq := uu1\<rparr>) = pass (s1\<lparr>sApiReq := uu2\<rparr>) \<and> eqButUIDf (pendingFReqs (s\<lparr>sApiReq := uu1\<rparr>)) (pendingFReqs (s1\<lparr>sApiReq := uu2\<rparr>)) \<and> eqButUID12 (friendReq (s\<lparr>sApiReq := uu1\<rparr>)) (friendReq (s1\<lparr>sApiReq := uu2\<rparr>)) \<and> eqButUIDf (friendIDs (s\<lparr>sApiReq := uu1\<rparr>)) (friendIDs (s1\<lparr>sApiReq := uu2\<rparr>)) \<and> postIDs (s\<lparr>sApiReq := uu1\<rparr>) = postIDs (s1\<lparr>sApiReq := uu2\<rparr>) \<and> admin (s\<lparr>sApiReq := uu1\<rparr>) = admin (s1\<lparr>sApiReq := uu2\<rparr>) \<and> post (s\<lparr>sApiReq := uu1\<rparr>) = post (s1\<lparr>sApiReq := uu2\<rparr>) \<and> vis (s\<lparr>sApiReq := uu1\<rparr>) = vis (s1\<lparr>sApiReq := uu2\<rparr>) \<and> owner (s\<lparr>sApiReq := uu1\<rparr>) = owner (s1\<lparr>sApiReq := uu2\<rparr>) \<and> pendingSApiReqs (s\<lparr>sApiReq := uu1\<rparr>) = pendingSApiReqs (s1\<lparr>sApiReq := uu2\<rparr>) \<and> sApiReq (s\<lparr>sApiReq := uu1\<rparr>) = sApiReq (s1\<lparr>sApiReq := uu2\<rparr>) \<and> serverApiIDs (s\<lparr>sApiReq := uu1\<rparr>) = serverApiIDs (s1\<lparr>sApiReq := uu2\<rparr>) \<and> serverPass (s\<lparr>sApiReq := uu1\<rparr>) = serverPass (s1\<lparr>sApiReq := uu2\<rparr>) \<and> outerPostIDs (s\<lparr>sApiReq := uu1\<rparr>) = outerPostIDs (s1\<lparr>sApiReq := uu2\<rparr>) \<and> outerPost (s\<lparr>sApiReq := uu1\<rparr>) = outerPost (s1\<lparr>sApiReq := uu2\<rparr>) \<and> outerVis (s\<lparr>sApiReq := uu1\<rparr>) = outerVis (s1\<lparr>sApiReq := uu2\<rparr>) \<and> outerOwner (s\<lparr>sApiReq := uu1\<rparr>) = outerOwner (s1\<lparr>sApiReq := uu2\<rparr>) \<and> sentOuterFriendIDs (s\<lparr>sApiReq := uu1\<rparr>) = sentOuterFriendIDs (s1\<lparr>sApiReq := uu2\<rparr>) \<and> recvOuterFriendIDs (s\<lparr>sApiReq := uu1\<rparr>) = recvOuterFriendIDs (s1\<lparr>sApiReq := uu2\<rparr>) \<and> pendingCApiReqs (s\<lparr>sApiReq := uu1\<rparr>) = pendingCApiReqs (s1\<lparr>sApiReq := uu2\<rparr>) \<and> cApiReq (s\<lparr>sApiReq := uu1\<rparr>) = cApiReq (s1\<lparr>sApiReq := uu2\<rparr>) \<and> clientApiIDs (s\<lparr>sApiReq := uu1\<rparr>) = clientApiIDs (s1\<lparr>sApiReq := uu2\<rparr>) \<and> clientPass (s\<lparr>sApiReq := uu1\<rparr>) = clientPass (s1\<lparr>sApiReq := uu2\<rparr>) \<and> sharedWith (s\<lparr>sApiReq := uu1\<rparr>) = sharedWith (s1\<lparr>sApiReq := uu2\<rparr>)) &&& (\<And>uu1 uu2. \<lbrakk>admin s = admin s1 \<and> pendingUReqs s = pendingUReqs s1 \<and> userReq s = userReq s1 \<and> userIDs s = userIDs s1 \<and> user s = user s1 \<and> pass s = pass s1 \<and> eqButUIDf (pendingFReqs s) (pendingFReqs s1) \<and> eqButUID12 (friendReq s) (friendReq s1) \<and> eqButUIDf (friendIDs s) (friendIDs s1) \<and> postIDs s = postIDs s1 \<and> admin s = admin s1 \<and> post s = post s1 \<and> vis s = vis s1 \<and> owner s = owner s1 \<and> pendingSApiReqs s = pendingSApiReqs s1 \<and> sApiReq s = sApiReq s1 \<and> serverApiIDs s = serverApiIDs s1 \<and> serverPass s = serverPass s1 \<and> outerPostIDs s = outerPostIDs s1 \<and> outerPost s = outerPost s1 \<and> outerVis s = outerVis s1 \<and> outerOwner s = outerOwner s1 \<and> sentOuterFriendIDs s = sentOuterFriendIDs s1 \<and> recvOuterFriendIDs s = recvOuterFriendIDs s1 \<and> pendingCApiReqs s = pendingCApiReqs s1 \<and> cApiReq s = cApiReq s1 \<and> clientApiIDs s = clientApiIDs s1 \<and> clientPass s = clientPass s1 \<and> sharedWith s = sharedWith s1; uu1 = uu2\<rbrakk> \<Longrightarrow> admin (s\<lparr>serverApiIDs := uu1\<rparr>) = admin (s1\<lparr>serverApiIDs := uu2\<rparr>) \<and> pendingUReqs (s\<lparr>serverApiIDs := uu1\<rparr>) = pendingUReqs (s1\<lparr>serverApiIDs := uu2\<rparr>) \<and> userReq (s\<lparr>serverApiIDs := uu1\<rparr>) = userReq (s1\<lparr>serverApiIDs := uu2\<rparr>) \<and> userIDs (s\<lparr>serverApiIDs := uu1\<rparr>) = userIDs (s1\<lparr>serverApiIDs := uu2\<rparr>) \<and> user (s\<lparr>serverApiIDs := uu1\<rparr>) = user (s1\<lparr>serverApiIDs := uu2\<rparr>) \<and> pass (s\<lparr>serverApiIDs := uu1\<rparr>) = pass (s1\<lparr>serverApiIDs := uu2\<rparr>) \<and> eqButUIDf (pendingFReqs (s\<lparr>serverApiIDs := uu1\<rparr>)) (pendingFReqs (s1\<lparr>serverApiIDs := uu2\<rparr>)) \<and> eqButUID12 (friendReq (s\<lparr>serverApiIDs := uu1\<rparr>)) (friendReq (s1\<lparr>serverApiIDs := uu2\<rparr>)) \<and> eqButUIDf (friendIDs (s\<lparr>serverApiIDs := uu1\<rparr>)) (friendIDs (s1\<lparr>serverApiIDs := uu2\<rparr>)) \<and> postIDs (s\<lparr>serverApiIDs := uu1\<rparr>) = postIDs (s1\<lparr>serverApiIDs := uu2\<rparr>) \<and> admin (s\<lparr>serverApiIDs := uu1\<rparr>) = admin (s1\<lparr>serverApiIDs := uu2\<rparr>) \<and> post (s\<lparr>serverApiIDs := uu1\<rparr>) = post (s1\<lparr>serverApiIDs := uu2\<rparr>) \<and> vis (s\<lparr>serverApiIDs := uu1\<rparr>) = vis (s1\<lparr>serverApiIDs := uu2\<rparr>) \<and> owner (s\<lparr>serverApiIDs := uu1\<rparr>) = owner (s1\<lparr>serverApiIDs := uu2\<rparr>) \<and> pendingSApiReqs (s\<lparr>serverApiIDs := uu1\<rparr>) = pendingSApiReqs (s1\<lparr>serverApiIDs := uu2\<rparr>) \<and> sApiReq (s\<lparr>serverApiIDs := uu1\<rparr>) = sApiReq (s1\<lparr>serverApiIDs := uu2\<rparr>) \<and> serverApiIDs (s\<lparr>serverApiIDs := uu1\<rparr>) = serverApiIDs (s1\<lparr>serverApiIDs := uu2\<rparr>) \<and> serverPass (s\<lparr>serverApiIDs := uu1\<rparr>) = serverPass (s1\<lparr>serverApiIDs := uu2\<rparr>) \<and> outerPostIDs (s\<lparr>serverApiIDs := uu1\<rparr>) = outerPostIDs (s1\<lparr>serverApiIDs := uu2\<rparr>) \<and> outerPost (s\<lparr>serverApiIDs := uu1\<rparr>) = outerPost (s1\<lparr>serverApiIDs := uu2\<rparr>) \<and> outerVis (s\<lparr>serverApiIDs := uu1\<rparr>) = outerVis (s1\<lparr>serverApiIDs := uu2\<rparr>) \<and> outerOwner (s\<lparr>serverApiIDs := uu1\<rparr>) = outerOwner (s1\<lparr>serverApiIDs := uu2\<rparr>) \<and> sentOuterFriendIDs (s\<lparr>serverApiIDs := uu1\<rparr>) = sentOuterFriendIDs (s1\<lparr>serverApiIDs := uu2\<rparr>) \<and> recvOuterFriendIDs (s\<lparr>serverApiIDs := uu1\<rparr>) = recvOuterFriendIDs (s1\<lparr>serverApiIDs := uu2\<rparr>) \<and> pendingCApiReqs (s\<lparr>serverApiIDs := uu1\<rparr>) = pendingCApiReqs (s1\<lparr>serverApiIDs := uu2\<rparr>) \<and> cApiReq (s\<lparr>serverApiIDs := uu1\<rparr>) = cApiReq (s1\<lparr>serverApiIDs := uu2\<rparr>) \<and> clientApiIDs (s\<lparr>serverApiIDs := uu1\<rparr>) = clientApiIDs (s1\<lparr>serverApiIDs := uu2\<rparr>) \<and> clientPass (s\<lparr>serverApiIDs := uu1\<rparr>) = clientPass (s1\<lparr>serverApiIDs := uu2\<rparr>) \<and> sharedWith (s\<lparr>serverApiIDs := uu1\<rparr>) = sharedWith (s1\<lparr>serverApiIDs := uu2\<rparr>)) &&& (\<And>uu1 uu2. \<lbrakk>admin s = admin s1 \<and> pendingUReqs s = pendingUReqs s1 \<and> userReq s = userReq s1 \<and> userIDs s = userIDs s1 \<and> user s = user s1 \<and> pass s = pass s1 \<and> eqButUIDf (pendingFReqs s) (pendingFReqs s1) \<and> eqButUID12 (friendReq s) (friendReq s1) \<and> eqButUIDf (friendIDs s) (friendIDs s1) \<and> postIDs s = postIDs s1 \<and> admin s = admin s1 \<and> post s = post s1 \<and> vis s = vis s1 \<and> owner s = owner s1 \<and> pendingSApiReqs s = pendingSApiReqs s1 \<and> sApiReq s = sApiReq s1 \<and> serverApiIDs s = serverApiIDs s1 \<and> serverPass s = serverPass s1 \<and> outerPostIDs s = outerPostIDs s1 \<and> outerPost s = outerPost s1 \<and> outerVis s = outerVis s1 \<and> outerOwner s = outerOwner s1 \<and> sentOuterFriendIDs s = sentOuterFriendIDs s1 \<and> recvOuterFriendIDs s = recvOuterFriendIDs s1 \<and> pendingCApiReqs s = pendingCApiReqs s1 \<and> cApiReq s = cApiReq s1 \<and> clientApiIDs s = clientApiIDs s1 \<and> clientPass s = clientPass s1 \<and> sharedWith s = sharedWith s1; uu1 = uu2\<rbrakk> \<Longrightarrow> admin (s\<lparr>serverPass := uu1\<rparr>) = admin (s1\<lparr>serverPass := uu2\<rparr>) \<and> pendingUReqs (s\<lparr>serverPass := uu1\<rparr>) = pendingUReqs (s1\<lparr>serverPass := uu2\<rparr>) \<and> userReq (s\<lparr>serverPass := uu1\<rparr>) = userReq (s1\<lparr>serverPass := uu2\<rparr>) \<and> userIDs (s\<lparr>serverPass := uu1\<rparr>) = userIDs (s1\<lparr>serverPass := uu2\<rparr>) \<and> user (s\<lparr>serverPass := uu1\<rparr>) = user (s1\<lparr>serverPass := uu2\<rparr>) \<and> pass (s\<lparr>serverPass := uu1\<rparr>) = pass (s1\<lparr>serverPass := uu2\<rparr>) \<and> eqButUIDf (pendingFReqs (s\<lparr>serverPass := uu1\<rparr>)) (pendingFReqs (s1\<lparr>serverPass := uu2\<rparr>)) \<and> eqButUID12 (friendReq (s\<lparr>serverPass := uu1\<rparr>)) (friendReq (s1\<lparr>serverPass := uu2\<rparr>)) \<and> eqButUIDf (friendIDs (s\<lparr>serverPass := uu1\<rparr>)) (friendIDs (s1\<lparr>serverPass := uu2\<rparr>)) \<and> postIDs (s\<lparr>serverPass := uu1\<rparr>) = postIDs (s1\<lparr>serverPass := uu2\<rparr>) \<and> admin (s\<lparr>serverPass := uu1\<rparr>) = admin (s1\<lparr>serverPass := uu2\<rparr>) \<and> post (s\<lparr>serverPass := uu1\<rparr>) = post (s1\<lparr>serverPass := uu2\<rparr>) \<and> vis (s\<lparr>serverPass := uu1\<rparr>) = vis (s1\<lparr>serverPass := uu2\<rparr>) \<and> owner (s\<lparr>serverPass := uu1\<rparr>) = owner (s1\<lparr>serverPass := uu2\<rparr>) \<and> pendingSApiReqs (s\<lparr>serverPass := uu1\<rparr>) = pendingSApiReqs (s1\<lparr>serverPass := uu2\<rparr>) \<and> sApiReq (s\<lparr>serverPass := uu1\<rparr>) = sApiReq (s1\<lparr>serverPass := uu2\<rparr>) \<and> serverApiIDs (s\<lparr>serverPass := uu1\<rparr>) = serverApiIDs (s1\<lparr>serverPass := uu2\<rparr>) \<and> serverPass (s\<lparr>serverPass := uu1\<rparr>) = serverPass (s1\<lparr>serverPass := uu2\<rparr>) \<and> outerPostIDs (s\<lparr>serverPass := uu1\<rparr>) = outerPostIDs (s1\<lparr>serverPass := uu2\<rparr>) \<and> outerPost (s\<lparr>serverPass := uu1\<rparr>) = outerPost (s1\<lparr>serverPass := uu2\<rparr>) \<and> outerVis (s\<lparr>serverPass := uu1\<rparr>) = outerVis (s1\<lparr>serverPass := uu2\<rparr>) \<and> outerOwner (s\<lparr>serverPass := uu1\<rparr>) = outerOwner (s1\<lparr>serverPass := uu2\<rparr>) \<and> sentOuterFriendIDs (s\<lparr>serverPass := uu1\<rparr>) = sentOuterFriendIDs (s1\<lparr>serverPass := uu2\<rparr>) \<and> recvOuterFriendIDs (s\<lparr>serverPass := uu1\<rparr>) = recvOuterFriendIDs (s1\<lparr>serverPass := uu2\<rparr>) \<and> pendingCApiReqs (s\<lparr>serverPass := uu1\<rparr>) = pendingCApiReqs (s1\<lparr>serverPass := uu2\<rparr>) \<and> cApiReq (s\<lparr>serverPass := uu1\<rparr>) = cApiReq (s1\<lparr>serverPass := uu2\<rparr>) \<and> clientApiIDs (s\<lparr>serverPass := uu1\<rparr>) = clientApiIDs (s1\<lparr>serverPass := uu2\<rparr>) \<and> clientPass (s\<lparr>serverPass := uu1\<rparr>) = clientPass (s1\<lparr>serverPass := uu2\<rparr>) \<and> sharedWith (s\<lparr>serverPass := uu1\<rparr>) = sharedWith (s1\<lparr>serverPass := uu2\<rparr>))) &&& ((\<And>uu1 uu2. \<lbrakk>admin s = admin s1 \<and> pendingUReqs s = pendingUReqs s1 \<and> userReq s = userReq s1 \<and> userIDs s = userIDs s1 \<and> user s = user s1 \<and> pass s = pass s1 \<and> eqButUIDf (pendingFReqs s) (pendingFReqs s1) \<and> eqButUID12 (friendReq s) (friendReq s1) \<and> eqButUIDf (friendIDs s) (friendIDs s1) \<and> postIDs s = postIDs s1 \<and> admin s = admin s1 \<and> post s = post s1 \<and> vis s = vis s1 \<and> owner s = owner s1 \<and> pendingSApiReqs s = pendingSApiReqs s1 \<and> sApiReq s = sApiReq s1 \<and> serverApiIDs s = serverApiIDs s1 \<and> serverPass s = serverPass s1 \<and> outerPostIDs s = outerPostIDs s1 \<and> outerPost s = outerPost s1 \<and> outerVis s = outerVis s1 \<and> outerOwner s = outerOwner s1 \<and> sentOuterFriendIDs s = sentOuterFriendIDs s1 \<and> recvOuterFriendIDs s = recvOuterFriendIDs s1 \<and> pendingCApiReqs s = pendingCApiReqs s1 \<and> cApiReq s = cApiReq s1 \<and> clientApiIDs s = clientApiIDs s1 \<and> clientPass s = clientPass s1 \<and> sharedWith s = sharedWith s1; uu1 = uu2\<rbrakk> \<Longrightarrow> admin (s\<lparr>outerPostIDs := uu1\<rparr>) = admin (s1\<lparr>outerPostIDs := uu2\<rparr>) \<and> pendingUReqs (s\<lparr>outerPostIDs := uu1\<rparr>) = pendingUReqs (s1\<lparr>outerPostIDs := uu2\<rparr>) \<and> userReq (s\<lparr>outerPostIDs := uu1\<rparr>) = userReq (s1\<lparr>outerPostIDs := uu2\<rparr>) \<and> userIDs (s\<lparr>outerPostIDs := uu1\<rparr>) = userIDs (s1\<lparr>outerPostIDs := uu2\<rparr>) \<and> user (s\<lparr>outerPostIDs := uu1\<rparr>) = user (s1\<lparr>outerPostIDs := uu2\<rparr>) \<and> pass (s\<lparr>outerPostIDs := uu1\<rparr>) = pass (s1\<lparr>outerPostIDs := uu2\<rparr>) \<and> eqButUIDf (pendingFReqs (s\<lparr>outerPostIDs := uu1\<rparr>)) (pendingFReqs (s1\<lparr>outerPostIDs := uu2\<rparr>)) \<and> eqButUID12 (friendReq (s\<lparr>outerPostIDs := uu1\<rparr>)) (friendReq (s1\<lparr>outerPostIDs := uu2\<rparr>)) \<and> eqButUIDf (friendIDs (s\<lparr>outerPostIDs := uu1\<rparr>)) (friendIDs (s1\<lparr>outerPostIDs := uu2\<rparr>)) \<and> postIDs (s\<lparr>outerPostIDs := uu1\<rparr>) = postIDs (s1\<lparr>outerPostIDs := uu2\<rparr>) \<and> admin (s\<lparr>outerPostIDs := uu1\<rparr>) = admin (s1\<lparr>outerPostIDs := uu2\<rparr>) \<and> post (s\<lparr>outerPostIDs := uu1\<rparr>) = post (s1\<lparr>outerPostIDs := uu2\<rparr>) \<and> vis (s\<lparr>outerPostIDs := uu1\<rparr>) = vis (s1\<lparr>outerPostIDs := uu2\<rparr>) \<and> owner (s\<lparr>outerPostIDs := uu1\<rparr>) = owner (s1\<lparr>outerPostIDs := uu2\<rparr>) \<and> pendingSApiReqs (s\<lparr>outerPostIDs := uu1\<rparr>) = pendingSApiReqs (s1\<lparr>outerPostIDs := uu2\<rparr>) \<and> sApiReq (s\<lparr>outerPostIDs := uu1\<rparr>) = sApiReq (s1\<lparr>outerPostIDs := uu2\<rparr>) \<and> serverApiIDs (s\<lparr>outerPostIDs := uu1\<rparr>) = serverApiIDs (s1\<lparr>outerPostIDs := uu2\<rparr>) \<and> serverPass (s\<lparr>outerPostIDs := uu1\<rparr>) = serverPass (s1\<lparr>outerPostIDs := uu2\<rparr>) \<and> outerPostIDs (s\<lparr>outerPostIDs := uu1\<rparr>) = outerPostIDs (s1\<lparr>outerPostIDs := uu2\<rparr>) \<and> outerPost (s\<lparr>outerPostIDs := uu1\<rparr>) = outerPost (s1\<lparr>outerPostIDs := uu2\<rparr>) \<and> outerVis (s\<lparr>outerPostIDs := uu1\<rparr>) = outerVis (s1\<lparr>outerPostIDs := uu2\<rparr>) \<and> outerOwner (s\<lparr>outerPostIDs := uu1\<rparr>) = outerOwner (s1\<lparr>outerPostIDs := uu2\<rparr>) \<and> sentOuterFriendIDs (s\<lparr>outerPostIDs := uu1\<rparr>) = sentOuterFriendIDs (s1\<lparr>outerPostIDs := uu2\<rparr>) \<and> recvOuterFriendIDs (s\<lparr>outerPostIDs := uu1\<rparr>) = recvOuterFriendIDs (s1\<lparr>outerPostIDs := uu2\<rparr>) \<and> pendingCApiReqs (s\<lparr>outerPostIDs := uu1\<rparr>) = pendingCApiReqs (s1\<lparr>outerPostIDs := uu2\<rparr>) \<and> cApiReq (s\<lparr>outerPostIDs := uu1\<rparr>) = cApiReq (s1\<lparr>outerPostIDs := uu2\<rparr>) \<and> clientApiIDs (s\<lparr>outerPostIDs := uu1\<rparr>) = clientApiIDs (s1\<lparr>outerPostIDs := uu2\<rparr>) \<and> clientPass (s\<lparr>outerPostIDs := uu1\<rparr>) = clientPass (s1\<lparr>outerPostIDs := uu2\<rparr>) \<and> sharedWith (s\<lparr>outerPostIDs := uu1\<rparr>) = sharedWith (s1\<lparr>outerPostIDs := uu2\<rparr>)) &&& (\<And>uu1 uu2. \<lbrakk>admin s = admin s1 \<and> pendingUReqs s = pendingUReqs s1 \<and> userReq s = userReq s1 \<and> userIDs s = userIDs s1 \<and> user s = user s1 \<and> pass s = pass s1 \<and> eqButUIDf (pendingFReqs s) (pendingFReqs s1) \<and> eqButUID12 (friendReq s) (friendReq s1) \<and> eqButUIDf (friendIDs s) (friendIDs s1) \<and> postIDs s = postIDs s1 \<and> admin s = admin s1 \<and> post s = post s1 \<and> vis s = vis s1 \<and> owner s = owner s1 \<and> pendingSApiReqs s = pendingSApiReqs s1 \<and> sApiReq s = sApiReq s1 \<and> serverApiIDs s = serverApiIDs s1 \<and> serverPass s = serverPass s1 \<and> outerPostIDs s = outerPostIDs s1 \<and> outerPost s = outerPost s1 \<and> outerVis s = outerVis s1 \<and> outerOwner s = outerOwner s1 \<and> sentOuterFriendIDs s = sentOuterFriendIDs s1 \<and> recvOuterFriendIDs s = recvOuterFriendIDs s1 \<and> pendingCApiReqs s = pendingCApiReqs s1 \<and> cApiReq s = cApiReq s1 \<and> clientApiIDs s = clientApiIDs s1 \<and> clientPass s = clientPass s1 \<and> sharedWith s = sharedWith s1; uu1 = uu2\<rbrakk> \<Longrightarrow> admin (s\<lparr>outerPost := uu1\<rparr>) = admin (s1\<lparr>outerPost := uu2\<rparr>) \<and> pendingUReqs (s\<lparr>outerPost := uu1\<rparr>) = pendingUReqs (s1\<lparr>outerPost := uu2\<rparr>) \<and> userReq (s\<lparr>outerPost := uu1\<rparr>) = userReq (s1\<lparr>outerPost := uu2\<rparr>) \<and> userIDs (s\<lparr>outerPost := uu1\<rparr>) = userIDs (s1\<lparr>outerPost := uu2\<rparr>) \<and> user (s\<lparr>outerPost := uu1\<rparr>) = user (s1\<lparr>outerPost := uu2\<rparr>) \<and> pass (s\<lparr>outerPost := uu1\<rparr>) = pass (s1\<lparr>outerPost := uu2\<rparr>) \<and> eqButUIDf (pendingFReqs (s\<lparr>outerPost := uu1\<rparr>)) (pendingFReqs (s1\<lparr>outerPost := uu2\<rparr>)) \<and> eqButUID12 (friendReq (s\<lparr>outerPost := uu1\<rparr>)) (friendReq (s1\<lparr>outerPost := uu2\<rparr>)) \<and> eqButUIDf (friendIDs (s\<lparr>outerPost := uu1\<rparr>)) (friendIDs (s1\<lparr>outerPost := uu2\<rparr>)) \<and> postIDs (s\<lparr>outerPost := uu1\<rparr>) = postIDs (s1\<lparr>outerPost := uu2\<rparr>) \<and> admin (s\<lparr>outerPost := uu1\<rparr>) = admin (s1\<lparr>outerPost := uu2\<rparr>) \<and> post (s\<lparr>outerPost := uu1\<rparr>) = post (s1\<lparr>outerPost := uu2\<rparr>) \<and> vis (s\<lparr>outerPost := uu1\<rparr>) = vis (s1\<lparr>outerPost := uu2\<rparr>) \<and> owner (s\<lparr>outerPost := uu1\<rparr>) = owner (s1\<lparr>outerPost := uu2\<rparr>) \<and> pendingSApiReqs (s\<lparr>outerPost := uu1\<rparr>) = pendingSApiReqs (s1\<lparr>outerPost := uu2\<rparr>) \<and> sApiReq (s\<lparr>outerPost := uu1\<rparr>) = sApiReq (s1\<lparr>outerPost := uu2\<rparr>) \<and> serverApiIDs (s\<lparr>outerPost := uu1\<rparr>) = serverApiIDs (s1\<lparr>outerPost := uu2\<rparr>) \<and> serverPass (s\<lparr>outerPost := uu1\<rparr>) = serverPass (s1\<lparr>outerPost := uu2\<rparr>) \<and> outerPostIDs (s\<lparr>outerPost := uu1\<rparr>) = outerPostIDs (s1\<lparr>outerPost := uu2\<rparr>) \<and> outerPost (s\<lparr>outerPost := uu1\<rparr>) = outerPost (s1\<lparr>outerPost := uu2\<rparr>) \<and> outerVis (s\<lparr>outerPost := uu1\<rparr>) = outerVis (s1\<lparr>outerPost := uu2\<rparr>) \<and> outerOwner (s\<lparr>outerPost := uu1\<rparr>) = outerOwner (s1\<lparr>outerPost := uu2\<rparr>) \<and> sentOuterFriendIDs (s\<lparr>outerPost := uu1\<rparr>) = sentOuterFriendIDs (s1\<lparr>outerPost := uu2\<rparr>) \<and> recvOuterFriendIDs (s\<lparr>outerPost := uu1\<rparr>) = recvOuterFriendIDs (s1\<lparr>outerPost := uu2\<rparr>) \<and> pendingCApiReqs (s\<lparr>outerPost := uu1\<rparr>) = pendingCApiReqs (s1\<lparr>outerPost := uu2\<rparr>) \<and> cApiReq (s\<lparr>outerPost := uu1\<rparr>) = cApiReq (s1\<lparr>outerPost := uu2\<rparr>) \<and> clientApiIDs (s\<lparr>outerPost := uu1\<rparr>) = clientApiIDs (s1\<lparr>outerPost := uu2\<rparr>) \<and> clientPass (s\<lparr>outerPost := uu1\<rparr>) = clientPass (s1\<lparr>outerPost := uu2\<rparr>) \<and> sharedWith (s\<lparr>outerPost := uu1\<rparr>) = sharedWith (s1\<lparr>outerPost := uu2\<rparr>))) &&& (\<And>uu1 uu2. \<lbrakk>admin s = admin s1 \<and> pendingUReqs s = pendingUReqs s1 \<and> userReq s = userReq s1 \<and> userIDs s = userIDs s1 \<and> user s = user s1 \<and> pass s = pass s1 \<and> eqButUIDf (pendingFReqs s) (pendingFReqs s1) \<and> eqButUID12 (friendReq s) (friendReq s1) \<and> eqButUIDf (friendIDs s) (friendIDs s1) \<and> postIDs s = postIDs s1 \<and> admin s = admin s1 \<and> post s = post s1 \<and> vis s = vis s1 \<and> owner s = owner s1 \<and> pendingSApiReqs s = pendingSApiReqs s1 \<and> sApiReq s = sApiReq s1 \<and> serverApiIDs s = serverApiIDs s1 \<and> serverPass s = serverPass s1 \<and> outerPostIDs s = outerPostIDs s1 \<and> outerPost s = outerPost s1 \<and> outerVis s = outerVis s1 \<and> outerOwner s = outerOwner s1 \<and> sentOuterFriendIDs s = sentOuterFriendIDs s1 \<and> recvOuterFriendIDs s = recvOuterFriendIDs s1 \<and> pendingCApiReqs s = pendingCApiReqs s1 \<and> cApiReq s = cApiReq s1 \<and> clientApiIDs s = clientApiIDs s1 \<and> clientPass s = clientPass s1 \<and> sharedWith s = sharedWith s1; uu1 = uu2\<rbrakk> \<Longrightarrow> admin (s\<lparr>outerVis := uu1\<rparr>) = admin (s1\<lparr>outerVis := uu2\<rparr>) \<and> pendingUReqs (s\<lparr>outerVis := uu1\<rparr>) = pendingUReqs (s1\<lparr>outerVis := uu2\<rparr>) \<and> userReq (s\<lparr>outerVis := uu1\<rparr>) = userReq (s1\<lparr>outerVis := uu2\<rparr>) \<and> userIDs (s\<lparr>outerVis := uu1\<rparr>) = userIDs (s1\<lparr>outerVis := uu2\<rparr>) \<and> user (s\<lparr>outerVis := uu1\<rparr>) = user (s1\<lparr>outerVis := uu2\<rparr>) \<and> pass (s\<lparr>outerVis := uu1\<rparr>) = pass (s1\<lparr>outerVis := uu2\<rparr>) \<and> eqButUIDf (pendingFReqs (s\<lparr>outerVis := uu1\<rparr>)) (pendingFReqs (s1\<lparr>outerVis := uu2\<rparr>)) \<and> eqButUID12 (friendReq (s\<lparr>outerVis := uu1\<rparr>)) (friendReq (s1\<lparr>outerVis := uu2\<rparr>)) \<and> eqButUIDf (friendIDs (s\<lparr>outerVis := uu1\<rparr>)) (friendIDs (s1\<lparr>outerVis := uu2\<rparr>)) \<and> postIDs (s\<lparr>outerVis := uu1\<rparr>) = postIDs (s1\<lparr>outerVis := uu2\<rparr>) \<and> admin (s\<lparr>outerVis := uu1\<rparr>) = admin (s1\<lparr>outerVis := uu2\<rparr>) \<and> post (s\<lparr>outerVis := uu1\<rparr>) = post (s1\<lparr>outerVis := uu2\<rparr>) \<and> vis (s\<lparr>outerVis := uu1\<rparr>) = vis (s1\<lparr>outerVis := uu2\<rparr>) \<and> owner (s\<lparr>outerVis := uu1\<rparr>) = owner (s1\<lparr>outerVis := uu2\<rparr>) \<and> pendingSApiReqs (s\<lparr>outerVis := uu1\<rparr>) = pendingSApiReqs (s1\<lparr>outerVis := uu2\<rparr>) \<and> sApiReq (s\<lparr>outerVis := uu1\<rparr>) = sApiReq (s1\<lparr>outerVis := uu2\<rparr>) \<and> serverApiIDs (s\<lparr>outerVis := uu1\<rparr>) = serverApiIDs (s1\<lparr>outerVis := uu2\<rparr>) \<and> serverPass (s\<lparr>outerVis := uu1\<rparr>) = serverPass (s1\<lparr>outerVis := uu2\<rparr>) \<and> outerPostIDs (s\<lparr>outerVis := uu1\<rparr>) = outerPostIDs (s1\<lparr>outerVis := uu2\<rparr>) \<and> outerPost (s\<lparr>outerVis := uu1\<rparr>) = outerPost (s1\<lparr>outerVis := uu2\<rparr>) \<and> outerVis (s\<lparr>outerVis := uu1\<rparr>) = outerVis (s1\<lparr>outerVis := uu2\<rparr>) \<and> outerOwner (s\<lparr>outerVis := uu1\<rparr>) = outerOwner (s1\<lparr>outerVis := uu2\<rparr>) \<and> sentOuterFriendIDs (s\<lparr>outerVis := uu1\<rparr>) = sentOuterFriendIDs (s1\<lparr>outerVis := uu2\<rparr>) \<and> recvOuterFriendIDs (s\<lparr>outerVis := uu1\<rparr>) = recvOuterFriendIDs (s1\<lparr>outerVis := uu2\<rparr>) \<and> pendingCApiReqs (s\<lparr>outerVis := uu1\<rparr>) = pendingCApiReqs (s1\<lparr>outerVis := uu2\<rparr>) \<and> cApiReq (s\<lparr>outerVis := uu1\<rparr>) = cApiReq (s1\<lparr>outerVis := uu2\<rparr>) \<and> clientApiIDs (s\<lparr>outerVis := uu1\<rparr>) = clientApiIDs (s1\<lparr>outerVis := uu2\<rparr>) \<and> clientPass (s\<lparr>outerVis := uu1\<rparr>) = clientPass (s1\<lparr>outerVis := uu2\<rparr>) \<and> sharedWith (s\<lparr>outerVis := uu1\<rparr>) = sharedWith (s1\<lparr>outerVis := uu2\<rparr>)) &&& (\<And>uu1 uu2. \<lbrakk>admin s = admin s1 \<and> pendingUReqs s = pendingUReqs s1 \<and> userReq s = userReq s1 \<and> userIDs s = userIDs s1 \<and> user s = user s1 \<and> pass s = pass s1 \<and> eqButUIDf (pendingFReqs s) (pendingFReqs s1) \<and> eqButUID12 (friendReq s) (friendReq s1) \<and> eqButUIDf (friendIDs s) (friendIDs s1) \<and> postIDs s = postIDs s1 \<and> admin s = admin s1 \<and> post s = post s1 \<and> vis s = vis s1 \<and> owner s = owner s1 \<and> pendingSApiReqs s = pendingSApiReqs s1 \<and> sApiReq s = sApiReq s1 \<and> serverApiIDs s = serverApiIDs s1 \<and> serverPass s = serverPass s1 \<and> outerPostIDs s = outerPostIDs s1 \<and> outerPost s = outerPost s1 \<and> outerVis s = outerVis s1 \<and> outerOwner s = outerOwner s1 \<and> sentOuterFriendIDs s = sentOuterFriendIDs s1 \<and> recvOuterFriendIDs s = recvOuterFriendIDs s1 \<and> pendingCApiReqs s = pendingCApiReqs s1 \<and> cApiReq s = cApiReq s1 \<and> clientApiIDs s = clientApiIDs s1 \<and> clientPass s = clientPass s1 \<and> sharedWith s = sharedWith s1; uu1 = uu2\<rbrakk> \<Longrightarrow> admin (s\<lparr>outerOwner := uu1\<rparr>) = admin (s1\<lparr>outerOwner := uu2\<rparr>) \<and> pendingUReqs (s\<lparr>outerOwner := uu1\<rparr>) = pendingUReqs (s1\<lparr>outerOwner := uu2\<rparr>) \<and> userReq (s\<lparr>outerOwner := uu1\<rparr>) = userReq (s1\<lparr>outerOwner := uu2\<rparr>) \<and> userIDs (s\<lparr>outerOwner := uu1\<rparr>) = userIDs (s1\<lparr>outerOwner := uu2\<rparr>) \<and> user (s\<lparr>outerOwner := uu1\<rparr>) = user (s1\<lparr>outerOwner := uu2\<rparr>) \<and> pass (s\<lparr>outerOwner := uu1\<rparr>) = pass (s1\<lparr>outerOwner := uu2\<rparr>) \<and> eqButUIDf (pendingFReqs (s\<lparr>outerOwner := uu1\<rparr>)) (pendingFReqs (s1\<lparr>outerOwner := uu2\<rparr>)) \<and> eqButUID12 (friendReq (s\<lparr>outerOwner := uu1\<rparr>)) (friendReq (s1\<lparr>outerOwner := uu2\<rparr>)) \<and> eqButUIDf (friendIDs (s\<lparr>outerOwner := uu1\<rparr>)) (friendIDs (s1\<lparr>outerOwner := uu2\<rparr>)) \<and> postIDs (s\<lparr>outerOwner := uu1\<rparr>) = postIDs (s1\<lparr>outerOwner := uu2\<rparr>) \<and> admin (s\<lparr>outerOwner := uu1\<rparr>) = admin (s1\<lparr>outerOwner := uu2\<rparr>) \<and> post (s\<lparr>outerOwner := uu1\<rparr>) = post (s1\<lparr>outerOwner := uu2\<rparr>) \<and> vis (s\<lparr>outerOwner := uu1\<rparr>) = vis (s1\<lparr>outerOwner := uu2\<rparr>) \<and> owner (s\<lparr>outerOwner := uu1\<rparr>) = owner (s1\<lparr>outerOwner := uu2\<rparr>) \<and> pendingSApiReqs (s\<lparr>outerOwner := uu1\<rparr>) = pendingSApiReqs (s1\<lparr>outerOwner := uu2\<rparr>) \<and> sApiReq (s\<lparr>outerOwner := uu1\<rparr>) = sApiReq (s1\<lparr>outerOwner := uu2\<rparr>) \<and> serverApiIDs (s\<lparr>outerOwner := uu1\<rparr>) = serverApiIDs (s1\<lparr>outerOwner := uu2\<rparr>) \<and> serverPass (s\<lparr>outerOwner := uu1\<rparr>) = serverPass (s1\<lparr>outerOwner := uu2\<rparr>) \<and> outerPostIDs (s\<lparr>outerOwner := uu1\<rparr>) = outerPostIDs (s1\<lparr>outerOwner := uu2\<rparr>) \<and> outerPost (s\<lparr>outerOwner := uu1\<rparr>) = outerPost (s1\<lparr>outerOwner := uu2\<rparr>) \<and> outerVis (s\<lparr>outerOwner := uu1\<rparr>) = outerVis (s1\<lparr>outerOwner := uu2\<rparr>) \<and> outerOwner (s\<lparr>outerOwner := uu1\<rparr>) = outerOwner (s1\<lparr>outerOwner := uu2\<rparr>) \<and> sentOuterFriendIDs (s\<lparr>outerOwner := uu1\<rparr>) = sentOuterFriendIDs (s1\<lparr>outerOwner := uu2\<rparr>) \<and> recvOuterFriendIDs (s\<lparr>outerOwner := uu1\<rparr>) = recvOuterFriendIDs (s1\<lparr>outerOwner := uu2\<rparr>) \<and> pendingCApiReqs (s\<lparr>outerOwner := uu1\<rparr>) = pendingCApiReqs (s1\<lparr>outerOwner := uu2\<rparr>) \<and> cApiReq (s\<lparr>outerOwner := uu1\<rparr>) = cApiReq (s1\<lparr>outerOwner := uu2\<rparr>) \<and> clientApiIDs (s\<lparr>outerOwner := uu1\<rparr>) = clientApiIDs (s1\<lparr>outerOwner := uu2\<rparr>) \<and> clientPass (s\<lparr>outerOwner := uu1\<rparr>) = clientPass (s1\<lparr>outerOwner := uu2\<rparr>) \<and> sharedWith (s\<lparr>outerOwner := uu1\<rparr>) = sharedWith (s1\<lparr>outerOwner := uu2\<rparr>))) &&& ((\<And>uu1 uu2. \<lbrakk>admin s = admin s1 \<and> pendingUReqs s = pendingUReqs s1 \<and> userReq s = userReq s1 \<and> userIDs s = userIDs s1 \<and> user s = user s1 \<and> pass s = pass s1 \<and> eqButUIDf (pendingFReqs s) (pendingFReqs s1) \<and> eqButUID12 (friendReq s) (friendReq s1) \<and> eqButUIDf (friendIDs s) (friendIDs s1) \<and> postIDs s = postIDs s1 \<and> admin s = admin s1 \<and> post s = post s1 \<and> vis s = vis s1 \<and> owner s = owner s1 \<and> pendingSApiReqs s = pendingSApiReqs s1 \<and> sApiReq s = sApiReq s1 \<and> serverApiIDs s = serverApiIDs s1 \<and> serverPass s = serverPass s1 \<and> outerPostIDs s = outerPostIDs s1 \<and> outerPost s = outerPost s1 \<and> outerVis s = outerVis s1 \<and> outerOwner s = outerOwner s1 \<and> sentOuterFriendIDs s = sentOuterFriendIDs s1 \<and> recvOuterFriendIDs s = recvOuterFriendIDs s1 \<and> pendingCApiReqs s = pendingCApiReqs s1 \<and> cApiReq s = cApiReq s1 \<and> clientApiIDs s = clientApiIDs s1 \<and> clientPass s = clientPass s1 \<and> sharedWith s = sharedWith s1; uu1 = uu2\<rbrakk> \<Longrightarrow> admin (s\<lparr>sentOuterFriendIDs := uu1\<rparr>) = admin (s1\<lparr>sentOuterFriendIDs := uu2\<rparr>) \<and> pendingUReqs (s\<lparr>sentOuterFriendIDs := uu1\<rparr>) = pendingUReqs (s1\<lparr>sentOuterFriendIDs := uu2\<rparr>) \<and> userReq (s\<lparr>sentOuterFriendIDs := uu1\<rparr>) = userReq (s1\<lparr>sentOuterFriendIDs := uu2\<rparr>) \<and> userIDs (s\<lparr>sentOuterFriendIDs := uu1\<rparr>) = userIDs (s1\<lparr>sentOuterFriendIDs := uu2\<rparr>) \<and> user (s\<lparr>sentOuterFriendIDs := uu1\<rparr>) = user (s1\<lparr>sentOuterFriendIDs := uu2\<rparr>) \<and> pass (s\<lparr>sentOuterFriendIDs := uu1\<rparr>) = pass (s1\<lparr>sentOuterFriendIDs := uu2\<rparr>) \<and> eqButUIDf (pendingFReqs (s\<lparr>sentOuterFriendIDs := uu1\<rparr>)) (pendingFReqs (s1\<lparr>sentOuterFriendIDs := uu2\<rparr>)) \<and> eqButUID12 (friendReq (s\<lparr>sentOuterFriendIDs := uu1\<rparr>)) (friendReq (s1\<lparr>sentOuterFriendIDs := uu2\<rparr>)) \<and> eqButUIDf (friendIDs (s\<lparr>sentOuterFriendIDs := uu1\<rparr>)) (friendIDs (s1\<lparr>sentOuterFriendIDs := uu2\<rparr>)) \<and> postIDs (s\<lparr>sentOuterFriendIDs := uu1\<rparr>) = postIDs (s1\<lparr>sentOuterFriendIDs := uu2\<rparr>) \<and> admin (s\<lparr>sentOuterFriendIDs := uu1\<rparr>) = admin (s1\<lparr>sentOuterFriendIDs := uu2\<rparr>) \<and> post (s\<lparr>sentOuterFriendIDs := uu1\<rparr>) = post (s1\<lparr>sentOuterFriendIDs := uu2\<rparr>) \<and> vis (s\<lparr>sentOuterFriendIDs := uu1\<rparr>) = vis (s1\<lparr>sentOuterFriendIDs := uu2\<rparr>) \<and> owner (s\<lparr>sentOuterFriendIDs := uu1\<rparr>) = owner (s1\<lparr>sentOuterFriendIDs := uu2\<rparr>) \<and> pendingSApiReqs (s\<lparr>sentOuterFriendIDs := uu1\<rparr>) = pendingSApiReqs (s1\<lparr>sentOuterFriendIDs := uu2\<rparr>) \<and> sApiReq (s\<lparr>sentOuterFriendIDs := uu1\<rparr>) = sApiReq (s1\<lparr>sentOuterFriendIDs := uu2\<rparr>) \<and> serverApiIDs (s\<lparr>sentOuterFriendIDs := uu1\<rparr>) = serverApiIDs (s1\<lparr>sentOuterFriendIDs := uu2\<rparr>) \<and> serverPass (s\<lparr>sentOuterFriendIDs := uu1\<rparr>) = serverPass (s1\<lparr>sentOuterFriendIDs := uu2\<rparr>) \<and> outerPostIDs (s\<lparr>sentOuterFriendIDs := uu1\<rparr>) = outerPostIDs (s1\<lparr>sentOuterFriendIDs := uu2\<rparr>) \<and> outerPost (s\<lparr>sentOuterFriendIDs := uu1\<rparr>) = outerPost (s1\<lparr>sentOuterFriendIDs := uu2\<rparr>) \<and> outerVis (s\<lparr>sentOuterFriendIDs := uu1\<rparr>) = outerVis (s1\<lparr>sentOuterFriendIDs := uu2\<rparr>) \<and> outerOwner (s\<lparr>sentOuterFriendIDs := uu1\<rparr>) = outerOwner (s1\<lparr>sentOuterFriendIDs := uu2\<rparr>) \<and> sentOuterFriendIDs (s\<lparr>sentOuterFriendIDs := uu1\<rparr>) = sentOuterFriendIDs (s1\<lparr>sentOuterFriendIDs := uu2\<rparr>) \<and> recvOuterFriendIDs (s\<lparr>sentOuterFriendIDs := uu1\<rparr>) = recvOuterFriendIDs (s1\<lparr>sentOuterFriendIDs := uu2\<rparr>) \<and> pendingCApiReqs (s\<lparr>sentOuterFriendIDs := uu1\<rparr>) = pendingCApiReqs (s1\<lparr>sentOuterFriendIDs := uu2\<rparr>) \<and> cApiReq (s\<lparr>sentOuterFriendIDs := uu1\<rparr>) = cApiReq (s1\<lparr>sentOuterFriendIDs := uu2\<rparr>) \<and> clientApiIDs (s\<lparr>sentOuterFriendIDs := uu1\<rparr>) = clientApiIDs (s1\<lparr>sentOuterFriendIDs := uu2\<rparr>) \<and> clientPass (s\<lparr>sentOuterFriendIDs := uu1\<rparr>) = clientPass (s1\<lparr>sentOuterFriendIDs := uu2\<rparr>) \<and> sharedWith (s\<lparr>sentOuterFriendIDs := uu1\<rparr>) = sharedWith (s1\<lparr>sentOuterFriendIDs := uu2\<rparr>)) &&& (\<And>uu1 uu2. \<lbrakk>admin s = admin s1 \<and> pendingUReqs s = pendingUReqs s1 \<and> userReq s = userReq s1 \<and> userIDs s = userIDs s1 \<and> user s = user s1 \<and> pass s = pass s1 \<and> eqButUIDf (pendingFReqs s) (pendingFReqs s1) \<and> eqButUID12 (friendReq s) (friendReq s1) \<and> eqButUIDf (friendIDs s) (friendIDs s1) \<and> postIDs s = postIDs s1 \<and> admin s = admin s1 \<and> post s = post s1 \<and> vis s = vis s1 \<and> owner s = owner s1 \<and> pendingSApiReqs s = pendingSApiReqs s1 \<and> sApiReq s = sApiReq s1 \<and> serverApiIDs s = serverApiIDs s1 \<and> serverPass s = serverPass s1 \<and> outerPostIDs s = outerPostIDs s1 \<and> outerPost s = outerPost s1 \<and> outerVis s = outerVis s1 \<and> outerOwner s = outerOwner s1 \<and> sentOuterFriendIDs s = sentOuterFriendIDs s1 \<and> recvOuterFriendIDs s = recvOuterFriendIDs s1 \<and> pendingCApiReqs s = pendingCApiReqs s1 \<and> cApiReq s = cApiReq s1 \<and> clientApiIDs s = clientApiIDs s1 \<and> clientPass s = clientPass s1 \<and> sharedWith s = sharedWith s1; uu1 = uu2\<rbrakk> \<Longrightarrow> admin (s\<lparr>recvOuterFriendIDs := uu1\<rparr>) = admin (s1\<lparr>recvOuterFriendIDs := uu2\<rparr>) \<and> pendingUReqs (s\<lparr>recvOuterFriendIDs := uu1\<rparr>) = pendingUReqs (s1\<lparr>recvOuterFriendIDs := uu2\<rparr>) \<and> userReq (s\<lparr>recvOuterFriendIDs := uu1\<rparr>) = userReq (s1\<lparr>recvOuterFriendIDs := uu2\<rparr>) \<and> userIDs (s\<lparr>recvOuterFriendIDs := uu1\<rparr>) = userIDs (s1\<lparr>recvOuterFriendIDs := uu2\<rparr>) \<and> user (s\<lparr>recvOuterFriendIDs := uu1\<rparr>) = user (s1\<lparr>recvOuterFriendIDs := uu2\<rparr>) \<and> pass (s\<lparr>recvOuterFriendIDs := uu1\<rparr>) = pass (s1\<lparr>recvOuterFriendIDs := uu2\<rparr>) \<and> eqButUIDf (pendingFReqs (s\<lparr>recvOuterFriendIDs := uu1\<rparr>)) (pendingFReqs (s1\<lparr>recvOuterFriendIDs := uu2\<rparr>)) \<and> eqButUID12 (friendReq (s\<lparr>recvOuterFriendIDs := uu1\<rparr>)) (friendReq (s1\<lparr>recvOuterFriendIDs := uu2\<rparr>)) \<and> eqButUIDf (friendIDs (s\<lparr>recvOuterFriendIDs := uu1\<rparr>)) (friendIDs (s1\<lparr>recvOuterFriendIDs := uu2\<rparr>)) \<and> postIDs (s\<lparr>recvOuterFriendIDs := uu1\<rparr>) = postIDs (s1\<lparr>recvOuterFriendIDs := uu2\<rparr>) \<and> admin (s\<lparr>recvOuterFriendIDs := uu1\<rparr>) = admin (s1\<lparr>recvOuterFriendIDs := uu2\<rparr>) \<and> post (s\<lparr>recvOuterFriendIDs := uu1\<rparr>) = post (s1\<lparr>recvOuterFriendIDs := uu2\<rparr>) \<and> vis (s\<lparr>recvOuterFriendIDs := uu1\<rparr>) = vis (s1\<lparr>recvOuterFriendIDs := uu2\<rparr>) \<and> owner (s\<lparr>recvOuterFriendIDs := uu1\<rparr>) = owner (s1\<lparr>recvOuterFriendIDs := uu2\<rparr>) \<and> pendingSApiReqs (s\<lparr>recvOuterFriendIDs := uu1\<rparr>) = pendingSApiReqs (s1\<lparr>recvOuterFriendIDs := uu2\<rparr>) \<and> sApiReq (s\<lparr>recvOuterFriendIDs := uu1\<rparr>) = sApiReq (s1\<lparr>recvOuterFriendIDs := uu2\<rparr>) \<and> serverApiIDs (s\<lparr>recvOuterFriendIDs := uu1\<rparr>) = serverApiIDs (s1\<lparr>recvOuterFriendIDs := uu2\<rparr>) \<and> serverPass (s\<lparr>recvOuterFriendIDs := uu1\<rparr>) = serverPass (s1\<lparr>recvOuterFriendIDs := uu2\<rparr>) \<and> outerPostIDs (s\<lparr>recvOuterFriendIDs := uu1\<rparr>) = outerPostIDs (s1\<lparr>recvOuterFriendIDs := uu2\<rparr>) \<and> outerPost (s\<lparr>recvOuterFriendIDs := uu1\<rparr>) = outerPost (s1\<lparr>recvOuterFriendIDs := uu2\<rparr>) \<and> outerVis (s\<lparr>recvOuterFriendIDs := uu1\<rparr>) = outerVis (s1\<lparr>recvOuterFriendIDs := uu2\<rparr>) \<and> outerOwner (s\<lparr>recvOuterFriendIDs := uu1\<rparr>) = outerOwner (s1\<lparr>recvOuterFriendIDs := uu2\<rparr>) \<and> sentOuterFriendIDs (s\<lparr>recvOuterFriendIDs := uu1\<rparr>) = sentOuterFriendIDs (s1\<lparr>recvOuterFriendIDs := uu2\<rparr>) \<and> recvOuterFriendIDs (s\<lparr>recvOuterFriendIDs := uu1\<rparr>) = recvOuterFriendIDs (s1\<lparr>recvOuterFriendIDs := uu2\<rparr>) \<and> pendingCApiReqs (s\<lparr>recvOuterFriendIDs := uu1\<rparr>) = pendingCApiReqs (s1\<lparr>recvOuterFriendIDs := uu2\<rparr>) \<and> cApiReq (s\<lparr>recvOuterFriendIDs := uu1\<rparr>) = cApiReq (s1\<lparr>recvOuterFriendIDs := uu2\<rparr>) \<and> clientApiIDs (s\<lparr>recvOuterFriendIDs := uu1\<rparr>) = clientApiIDs (s1\<lparr>recvOuterFriendIDs := uu2\<rparr>) \<and> clientPass (s\<lparr>recvOuterFriendIDs := uu1\<rparr>) = clientPass (s1\<lparr>recvOuterFriendIDs := uu2\<rparr>) \<and> sharedWith (s\<lparr>recvOuterFriendIDs := uu1\<rparr>) = sharedWith (s1\<lparr>recvOuterFriendIDs := uu2\<rparr>)) &&& (\<And>uu1 uu2. \<lbrakk>admin s = admin s1 \<and> pendingUReqs s = pendingUReqs s1 \<and> userReq s = userReq s1 \<and> userIDs s = userIDs s1 \<and> user s = user s1 \<and> pass s = pass s1 \<and> eqButUIDf (pendingFReqs s) (pendingFReqs s1) \<and> eqButUID12 (friendReq s) (friendReq s1) \<and> eqButUIDf (friendIDs s) (friendIDs s1) \<and> postIDs s = postIDs s1 \<and> admin s = admin s1 \<and> post s = post s1 \<and> vis s = vis s1 \<and> owner s = owner s1 \<and> pendingSApiReqs s = pendingSApiReqs s1 \<and> sApiReq s = sApiReq s1 \<and> serverApiIDs s = serverApiIDs s1 \<and> serverPass s = serverPass s1 \<and> outerPostIDs s = outerPostIDs s1 \<and> outerPost s = outerPost s1 \<and> outerVis s = outerVis s1 \<and> outerOwner s = outerOwner s1 \<and> sentOuterFriendIDs s = sentOuterFriendIDs s1 \<and> recvOuterFriendIDs s = recvOuterFriendIDs s1 \<and> pendingCApiReqs s = pendingCApiReqs s1 \<and> cApiReq s = cApiReq s1 \<and> clientApiIDs s = clientApiIDs s1 \<and> clientPass s = clientPass s1 \<and> sharedWith s = sharedWith s1; uu1 = uu2\<rbrakk> \<Longrightarrow> admin (s\<lparr>pendingCApiReqs := uu1\<rparr>) = admin (s1\<lparr>pendingCApiReqs := uu2\<rparr>) \<and> pendingUReqs (s\<lparr>pendingCApiReqs := uu1\<rparr>) = pendingUReqs (s1\<lparr>pendingCApiReqs := uu2\<rparr>) \<and> userReq (s\<lparr>pendingCApiReqs := uu1\<rparr>) = userReq (s1\<lparr>pendingCApiReqs := uu2\<rparr>) \<and> userIDs (s\<lparr>pendingCApiReqs := uu1\<rparr>) = userIDs (s1\<lparr>pendingCApiReqs := uu2\<rparr>) \<and> user (s\<lparr>pendingCApiReqs := uu1\<rparr>) = user (s1\<lparr>pendingCApiReqs := uu2\<rparr>) \<and> pass (s\<lparr>pendingCApiReqs := uu1\<rparr>) = pass (s1\<lparr>pendingCApiReqs := uu2\<rparr>) \<and> eqButUIDf (pendingFReqs (s\<lparr>pendingCApiReqs := uu1\<rparr>)) (pendingFReqs (s1\<lparr>pendingCApiReqs := uu2\<rparr>)) \<and> eqButUID12 (friendReq (s\<lparr>pendingCApiReqs := uu1\<rparr>)) (friendReq (s1\<lparr>pendingCApiReqs := uu2\<rparr>)) \<and> eqButUIDf (friendIDs (s\<lparr>pendingCApiReqs := uu1\<rparr>)) (friendIDs (s1\<lparr>pendingCApiReqs := uu2\<rparr>)) \<and> postIDs (s\<lparr>pendingCApiReqs := uu1\<rparr>) = postIDs (s1\<lparr>pendingCApiReqs := uu2\<rparr>) \<and> admin (s\<lparr>pendingCApiReqs := uu1\<rparr>) = admin (s1\<lparr>pendingCApiReqs := uu2\<rparr>) \<and> post (s\<lparr>pendingCApiReqs := uu1\<rparr>) = post (s1\<lparr>pendingCApiReqs := uu2\<rparr>) \<and> vis (s\<lparr>pendingCApiReqs := uu1\<rparr>) = vis (s1\<lparr>pendingCApiReqs := uu2\<rparr>) \<and> owner (s\<lparr>pendingCApiReqs := uu1\<rparr>) = owner (s1\<lparr>pendingCApiReqs := uu2\<rparr>) \<and> pendingSApiReqs (s\<lparr>pendingCApiReqs := uu1\<rparr>) = pendingSApiReqs (s1\<lparr>pendingCApiReqs := uu2\<rparr>) \<and> sApiReq (s\<lparr>pendingCApiReqs := uu1\<rparr>) = sApiReq (s1\<lparr>pendingCApiReqs := uu2\<rparr>) \<and> serverApiIDs (s\<lparr>pendingCApiReqs := uu1\<rparr>) = serverApiIDs (s1\<lparr>pendingCApiReqs := uu2\<rparr>) \<and> serverPass (s\<lparr>pendingCApiReqs := uu1\<rparr>) = serverPass (s1\<lparr>pendingCApiReqs := uu2\<rparr>) \<and> outerPostIDs (s\<lparr>pendingCApiReqs := uu1\<rparr>) = outerPostIDs (s1\<lparr>pendingCApiReqs := uu2\<rparr>) \<and> outerPost (s\<lparr>pendingCApiReqs := uu1\<rparr>) = outerPost (s1\<lparr>pendingCApiReqs := uu2\<rparr>) \<and> outerVis (s\<lparr>pendingCApiReqs := uu1\<rparr>) = outerVis (s1\<lparr>pendingCApiReqs := uu2\<rparr>) \<and> outerOwner (s\<lparr>pendingCApiReqs := uu1\<rparr>) = outerOwner (s1\<lparr>pendingCApiReqs := uu2\<rparr>) \<and> sentOuterFriendIDs (s\<lparr>pendingCApiReqs := uu1\<rparr>) = sentOuterFriendIDs (s1\<lparr>pendingCApiReqs := uu2\<rparr>) \<and> recvOuterFriendIDs (s\<lparr>pendingCApiReqs := uu1\<rparr>) = recvOuterFriendIDs (s1\<lparr>pendingCApiReqs := uu2\<rparr>) \<and> pendingCApiReqs (s\<lparr>pendingCApiReqs := uu1\<rparr>) = pendingCApiReqs (s1\<lparr>pendingCApiReqs := uu2\<rparr>) \<and> cApiReq (s\<lparr>pendingCApiReqs := uu1\<rparr>) = cApiReq (s1\<lparr>pendingCApiReqs := uu2\<rparr>) \<and> clientApiIDs (s\<lparr>pendingCApiReqs := uu1\<rparr>) = clientApiIDs (s1\<lparr>pendingCApiReqs := uu2\<rparr>) \<and> clientPass (s\<lparr>pendingCApiReqs := uu1\<rparr>) = clientPass (s1\<lparr>pendingCApiReqs := uu2\<rparr>) \<and> sharedWith (s\<lparr>pendingCApiReqs := uu1\<rparr>) = sharedWith (s1\<lparr>pendingCApiReqs := uu2\<rparr>))) &&& ((\<And>uu1 uu2. \<lbrakk>admin s = admin s1 \<and> pendingUReqs s = pendingUReqs s1 \<and> userReq s = userReq s1 \<and> userIDs s = userIDs s1 \<and> user s = user s1 \<and> pass s = pass s1 \<and> eqButUIDf (pendingFReqs s) (pendingFReqs s1) \<and> eqButUID12 (friendReq s) (friendReq s1) \<and> eqButUIDf (friendIDs s) (friendIDs s1) \<and> postIDs s = postIDs s1 \<and> admin s = admin s1 \<and> post s = post s1 \<and> vis s = vis s1 \<and> owner s = owner s1 \<and> pendingSApiReqs s = pendingSApiReqs s1 \<and> sApiReq s = sApiReq s1 \<and> serverApiIDs s = serverApiIDs s1 \<and> serverPass s = serverPass s1 \<and> outerPostIDs s = outerPostIDs s1 \<and> outerPost s = outerPost s1 \<and> outerVis s = outerVis s1 \<and> outerOwner s = outerOwner s1 \<and> sentOuterFriendIDs s = sentOuterFriendIDs s1 \<and> recvOuterFriendIDs s = recvOuterFriendIDs s1 \<and> pendingCApiReqs s = pendingCApiReqs s1 \<and> cApiReq s = cApiReq s1 \<and> clientApiIDs s = clientApiIDs s1 \<and> clientPass s = clientPass s1 \<and> sharedWith s = sharedWith s1; uu1 = uu2\<rbrakk> \<Longrightarrow> admin (s\<lparr>cApiReq := uu1\<rparr>) = admin (s1\<lparr>cApiReq := uu2\<rparr>) \<and> pendingUReqs (s\<lparr>cApiReq := uu1\<rparr>) = pendingUReqs (s1\<lparr>cApiReq := uu2\<rparr>) \<and> userReq (s\<lparr>cApiReq := uu1\<rparr>) = userReq (s1\<lparr>cApiReq := uu2\<rparr>) \<and> userIDs (s\<lparr>cApiReq := uu1\<rparr>) = userIDs (s1\<lparr>cApiReq := uu2\<rparr>) \<and> user (s\<lparr>cApiReq := uu1\<rparr>) = user (s1\<lparr>cApiReq := uu2\<rparr>) \<and> pass (s\<lparr>cApiReq := uu1\<rparr>) = pass (s1\<lparr>cApiReq := uu2\<rparr>) \<and> eqButUIDf (pendingFReqs (s\<lparr>cApiReq := uu1\<rparr>)) (pendingFReqs (s1\<lparr>cApiReq := uu2\<rparr>)) \<and> eqButUID12 (friendReq (s\<lparr>cApiReq := uu1\<rparr>)) (friendReq (s1\<lparr>cApiReq := uu2\<rparr>)) \<and> eqButUIDf (friendIDs (s\<lparr>cApiReq := uu1\<rparr>)) (friendIDs (s1\<lparr>cApiReq := uu2\<rparr>)) \<and> postIDs (s\<lparr>cApiReq := uu1\<rparr>) = postIDs (s1\<lparr>cApiReq := uu2\<rparr>) \<and> admin (s\<lparr>cApiReq := uu1\<rparr>) = admin (s1\<lparr>cApiReq := uu2\<rparr>) \<and> post (s\<lparr>cApiReq := uu1\<rparr>) = post (s1\<lparr>cApiReq := uu2\<rparr>) \<and> vis (s\<lparr>cApiReq := uu1\<rparr>) = vis (s1\<lparr>cApiReq := uu2\<rparr>) \<and> owner (s\<lparr>cApiReq := uu1\<rparr>) = owner (s1\<lparr>cApiReq := uu2\<rparr>) \<and> pendingSApiReqs (s\<lparr>cApiReq := uu1\<rparr>) = pendingSApiReqs (s1\<lparr>cApiReq := uu2\<rparr>) \<and> sApiReq (s\<lparr>cApiReq := uu1\<rparr>) = sApiReq (s1\<lparr>cApiReq := uu2\<rparr>) \<and> serverApiIDs (s\<lparr>cApiReq := uu1\<rparr>) = serverApiIDs (s1\<lparr>cApiReq := uu2\<rparr>) \<and> serverPass (s\<lparr>cApiReq := uu1\<rparr>) = serverPass (s1\<lparr>cApiReq := uu2\<rparr>) \<and> outerPostIDs (s\<lparr>cApiReq := uu1\<rparr>) = outerPostIDs (s1\<lparr>cApiReq := uu2\<rparr>) \<and> outerPost (s\<lparr>cApiReq := uu1\<rparr>) = outerPost (s1\<lparr>cApiReq := uu2\<rparr>) \<and> outerVis (s\<lparr>cApiReq := uu1\<rparr>) = outerVis (s1\<lparr>cApiReq := uu2\<rparr>) \<and> outerOwner (s\<lparr>cApiReq := uu1\<rparr>) = outerOwner (s1\<lparr>cApiReq := uu2\<rparr>) \<and> sentOuterFriendIDs (s\<lparr>cApiReq := uu1\<rparr>) = sentOuterFriendIDs (s1\<lparr>cApiReq := uu2\<rparr>) \<and> recvOuterFriendIDs (s\<lparr>cApiReq := uu1\<rparr>) = recvOuterFriendIDs (s1\<lparr>cApiReq := uu2\<rparr>) \<and> pendingCApiReqs (s\<lparr>cApiReq := uu1\<rparr>) = pendingCApiReqs (s1\<lparr>cApiReq := uu2\<rparr>) \<and> cApiReq (s\<lparr>cApiReq := uu1\<rparr>) = cApiReq (s1\<lparr>cApiReq := uu2\<rparr>) \<and> clientApiIDs (s\<lparr>cApiReq := uu1\<rparr>) = clientApiIDs (s1\<lparr>cApiReq := uu2\<rparr>) \<and> clientPass (s\<lparr>cApiReq := uu1\<rparr>) = clientPass (s1\<lparr>cApiReq := uu2\<rparr>) \<and> sharedWith (s\<lparr>cApiReq := uu1\<rparr>) = sharedWith (s1\<lparr>cApiReq := uu2\<rparr>)) &&& (\<And>uu1 uu2. \<lbrakk>admin s = admin s1 \<and> pendingUReqs s = pendingUReqs s1 \<and> userReq s = userReq s1 \<and> userIDs s = userIDs s1 \<and> user s = user s1 \<and> pass s = pass s1 \<and> eqButUIDf (pendingFReqs s) (pendingFReqs s1) \<and> eqButUID12 (friendReq s) (friendReq s1) \<and> eqButUIDf (friendIDs s) (friendIDs s1) \<and> postIDs s = postIDs s1 \<and> admin s = admin s1 \<and> post s = post s1 \<and> vis s = vis s1 \<and> owner s = owner s1 \<and> pendingSApiReqs s = pendingSApiReqs s1 \<and> sApiReq s = sApiReq s1 \<and> serverApiIDs s = serverApiIDs s1 \<and> serverPass s = serverPass s1 \<and> outerPostIDs s = outerPostIDs s1 \<and> outerPost s = outerPost s1 \<and> outerVis s = outerVis s1 \<and> outerOwner s = outerOwner s1 \<and> sentOuterFriendIDs s = sentOuterFriendIDs s1 \<and> recvOuterFriendIDs s = recvOuterFriendIDs s1 \<and> pendingCApiReqs s = pendingCApiReqs s1 \<and> cApiReq s = cApiReq s1 \<and> clientApiIDs s = clientApiIDs s1 \<and> clientPass s = clientPass s1 \<and> sharedWith s = sharedWith s1; uu1 = uu2\<rbrakk> \<Longrightarrow> admin (s\<lparr>clientApiIDs := uu1\<rparr>) = admin (s1\<lparr>clientApiIDs := uu2\<rparr>) \<and> pendingUReqs (s\<lparr>clientApiIDs := uu1\<rparr>) = pendingUReqs (s1\<lparr>clientApiIDs := uu2\<rparr>) \<and> userReq (s\<lparr>clientApiIDs := uu1\<rparr>) = userReq (s1\<lparr>clientApiIDs := uu2\<rparr>) \<and> userIDs (s\<lparr>clientApiIDs := uu1\<rparr>) = userIDs (s1\<lparr>clientApiIDs := uu2\<rparr>) \<and> user (s\<lparr>clientApiIDs := uu1\<rparr>) = user (s1\<lparr>clientApiIDs := uu2\<rparr>) \<and> pass (s\<lparr>clientApiIDs := uu1\<rparr>) = pass (s1\<lparr>clientApiIDs := uu2\<rparr>) \<and> eqButUIDf (pendingFReqs (s\<lparr>clientApiIDs := uu1\<rparr>)) (pendingFReqs (s1\<lparr>clientApiIDs := uu2\<rparr>)) \<and> eqButUID12 (friendReq (s\<lparr>clientApiIDs := uu1\<rparr>)) (friendReq (s1\<lparr>clientApiIDs := uu2\<rparr>)) \<and> eqButUIDf (friendIDs (s\<lparr>clientApiIDs := uu1\<rparr>)) (friendIDs (s1\<lparr>clientApiIDs := uu2\<rparr>)) \<and> postIDs (s\<lparr>clientApiIDs := uu1\<rparr>) = postIDs (s1\<lparr>clientApiIDs := uu2\<rparr>) \<and> admin (s\<lparr>clientApiIDs := uu1\<rparr>) = admin (s1\<lparr>clientApiIDs := uu2\<rparr>) \<and> post (s\<lparr>clientApiIDs := uu1\<rparr>) = post (s1\<lparr>clientApiIDs := uu2\<rparr>) \<and> vis (s\<lparr>clientApiIDs := uu1\<rparr>) = vis (s1\<lparr>clientApiIDs := uu2\<rparr>) \<and> owner (s\<lparr>clientApiIDs := uu1\<rparr>) = owner (s1\<lparr>clientApiIDs := uu2\<rparr>) \<and> pendingSApiReqs (s\<lparr>clientApiIDs := uu1\<rparr>) = pendingSApiReqs (s1\<lparr>clientApiIDs := uu2\<rparr>) \<and> sApiReq (s\<lparr>clientApiIDs := uu1\<rparr>) = sApiReq (s1\<lparr>clientApiIDs := uu2\<rparr>) \<and> serverApiIDs (s\<lparr>clientApiIDs := uu1\<rparr>) = serverApiIDs (s1\<lparr>clientApiIDs := uu2\<rparr>) \<and> serverPass (s\<lparr>clientApiIDs := uu1\<rparr>) = serverPass (s1\<lparr>clientApiIDs := uu2\<rparr>) \<and> outerPostIDs (s\<lparr>clientApiIDs := uu1\<rparr>) = outerPostIDs (s1\<lparr>clientApiIDs := uu2\<rparr>) \<and> outerPost (s\<lparr>clientApiIDs := uu1\<rparr>) = outerPost (s1\<lparr>clientApiIDs := uu2\<rparr>) \<and> outerVis (s\<lparr>clientApiIDs := uu1\<rparr>) = outerVis (s1\<lparr>clientApiIDs := uu2\<rparr>) \<and> outerOwner (s\<lparr>clientApiIDs := uu1\<rparr>) = outerOwner (s1\<lparr>clientApiIDs := uu2\<rparr>) \<and> sentOuterFriendIDs (s\<lparr>clientApiIDs := uu1\<rparr>) = sentOuterFriendIDs (s1\<lparr>clientApiIDs := uu2\<rparr>) \<and> recvOuterFriendIDs (s\<lparr>clientApiIDs := uu1\<rparr>) = recvOuterFriendIDs (s1\<lparr>clientApiIDs := uu2\<rparr>) \<and> pendingCApiReqs (s\<lparr>clientApiIDs := uu1\<rparr>) = pendingCApiReqs (s1\<lparr>clientApiIDs := uu2\<rparr>) \<and> cApiReq (s\<lparr>clientApiIDs := uu1\<rparr>) = cApiReq (s1\<lparr>clientApiIDs := uu2\<rparr>) \<and> clientApiIDs (s\<lparr>clientApiIDs := uu1\<rparr>) = clientApiIDs (s1\<lparr>clientApiIDs := uu2\<rparr>) \<and> clientPass (s\<lparr>clientApiIDs := uu1\<rparr>) = clientPass (s1\<lparr>clientApiIDs := uu2\<rparr>) \<and> sharedWith (s\<lparr>clientApiIDs := uu1\<rparr>) = sharedWith (s1\<lparr>clientApiIDs := uu2\<rparr>))) &&& (\<And>uu1 uu2. \<lbrakk>admin s = admin s1 \<and> pendingUReqs s = pendingUReqs s1 \<and> userReq s = userReq s1 \<and> userIDs s = userIDs s1 \<and> user s = user s1 \<and> pass s = pass s1 \<and> eqButUIDf (pendingFReqs s) (pendingFReqs s1) \<and> eqButUID12 (friendReq s) (friendReq s1) \<and> eqButUIDf (friendIDs s) (friendIDs s1) \<and> postIDs s = postIDs s1 \<and> admin s = admin s1 \<and> post s = post s1 \<and> vis s = vis s1 \<and> owner s = owner s1 \<and> pendingSApiReqs s = pendingSApiReqs s1 \<and> sApiReq s = sApiReq s1 \<and> serverApiIDs s = serverApiIDs s1 \<and> serverPass s = serverPass s1 \<and> outerPostIDs s = outerPostIDs s1 \<and> outerPost s = outerPost s1 \<and> outerVis s = outerVis s1 \<and> outerOwner s = outerOwner s1 \<and> sentOuterFriendIDs s = sentOuterFriendIDs s1 \<and> recvOuterFriendIDs s = recvOuterFriendIDs s1 \<and> pendingCApiReqs s = pendingCApiReqs s1 \<and> cApiReq s = cApiReq s1 \<and> clientApiIDs s = clientApiIDs s1 \<and> clientPass s = clientPass s1 \<and> sharedWith s = sharedWith s1; uu1 = uu2\<rbrakk> \<Longrightarrow> admin (s\<lparr>clientPass := uu1\<rparr>) = admin (s1\<lparr>clientPass := uu2\<rparr>) \<and> pendingUReqs (s\<lparr>clientPass := uu1\<rparr>) = pendingUReqs (s1\<lparr>clientPass := uu2\<rparr>) \<and> userReq (s\<lparr>clientPass := uu1\<rparr>) = userReq (s1\<lparr>clientPass := uu2\<rparr>) \<and> userIDs (s\<lparr>clientPass := uu1\<rparr>) = userIDs (s1\<lparr>clientPass := uu2\<rparr>) \<and> user (s\<lparr>clientPass := uu1\<rparr>) = user (s1\<lparr>clientPass := uu2\<rparr>) \<and> pass (s\<lparr>clientPass := uu1\<rparr>) = pass (s1\<lparr>clientPass := uu2\<rparr>) \<and> eqButUIDf (pendingFReqs (s\<lparr>clientPass := uu1\<rparr>)) (pendingFReqs (s1\<lparr>clientPass := uu2\<rparr>)) \<and> eqButUID12 (friendReq (s\<lparr>clientPass := uu1\<rparr>)) (friendReq (s1\<lparr>clientPass := uu2\<rparr>)) \<and> eqButUIDf (friendIDs (s\<lparr>clientPass := uu1\<rparr>)) (friendIDs (s1\<lparr>clientPass := uu2\<rparr>)) \<and> postIDs (s\<lparr>clientPass := uu1\<rparr>) = postIDs (s1\<lparr>clientPass := uu2\<rparr>) \<and> admin (s\<lparr>clientPass := uu1\<rparr>) = admin (s1\<lparr>clientPass := uu2\<rparr>) \<and> post (s\<lparr>clientPass := uu1\<rparr>) = post (s1\<lparr>clientPass := uu2\<rparr>) \<and> vis (s\<lparr>clientPass := uu1\<rparr>) = vis (s1\<lparr>clientPass := uu2\<rparr>) \<and> owner (s\<lparr>clientPass := uu1\<rparr>) = owner (s1\<lparr>clientPass := uu2\<rparr>) \<and> pendingSApiReqs (s\<lparr>clientPass := uu1\<rparr>) = pendingSApiReqs (s1\<lparr>clientPass := uu2\<rparr>) \<and> sApiReq (s\<lparr>clientPass := uu1\<rparr>) = sApiReq (s1\<lparr>clientPass := uu2\<rparr>) \<and> serverApiIDs (s\<lparr>clientPass := uu1\<rparr>) = serverApiIDs (s1\<lparr>clientPass := uu2\<rparr>) \<and> serverPass (s\<lparr>clientPass := uu1\<rparr>) = serverPass (s1\<lparr>clientPass := uu2\<rparr>) \<and> outerPostIDs (s\<lparr>clientPass := uu1\<rparr>) = outerPostIDs (s1\<lparr>clientPass := uu2\<rparr>) \<and> outerPost (s\<lparr>clientPass := uu1\<rparr>) = outerPost (s1\<lparr>clientPass := uu2\<rparr>) \<and> outerVis (s\<lparr>clientPass := uu1\<rparr>) = outerVis (s1\<lparr>clientPass := uu2\<rparr>) \<and> outerOwner (s\<lparr>clientPass := uu1\<rparr>) = outerOwner (s1\<lparr>clientPass := uu2\<rparr>) \<and> sentOuterFriendIDs (s\<lparr>clientPass := uu1\<rparr>) = sentOuterFriendIDs (s1\<lparr>clientPass := uu2\<rparr>) \<and> recvOuterFriendIDs (s\<lparr>clientPass := uu1\<rparr>) = recvOuterFriendIDs (s1\<lparr>clientPass := uu2\<rparr>) \<and> pendingCApiReqs (s\<lparr>clientPass := uu1\<rparr>) = pendingCApiReqs (s1\<lparr>clientPass := uu2\<rparr>) \<and> cApiReq (s\<lparr>clientPass := uu1\<rparr>) = cApiReq (s1\<lparr>clientPass := uu2\<rparr>) \<and> clientApiIDs (s\<lparr>clientPass := uu1\<rparr>) = clientApiIDs (s1\<lparr>clientPass := uu2\<rparr>) \<and> clientPass (s\<lparr>clientPass := uu1\<rparr>) = clientPass (s1\<lparr>clientPass := uu2\<rparr>) \<and> sharedWith (s\<lparr>clientPass := uu1\<rparr>) = sharedWith (s1\<lparr>clientPass := uu2\<rparr>)) &&& (\<And>uu1 uu2. \<lbrakk>admin s = admin s1 \<and> pendingUReqs s = pendingUReqs s1 \<and> userReq s = userReq s1 \<and> userIDs s = userIDs s1 \<and> user s = user s1 \<and> pass s = pass s1 \<and> eqButUIDf (pendingFReqs s) (pendingFReqs s1) \<and> eqButUID12 (friendReq s) (friendReq s1) \<and> eqButUIDf (friendIDs s) (friendIDs s1) \<and> postIDs s = postIDs s1 \<and> admin s = admin s1 \<and> post s = post s1 \<and> vis s = vis s1 \<and> owner s = owner s1 \<and> pendingSApiReqs s = pendingSApiReqs s1 \<and> sApiReq s = sApiReq s1 \<and> serverApiIDs s = serverApiIDs s1 \<and> serverPass s = serverPass s1 \<and> outerPostIDs s = outerPostIDs s1 \<and> outerPost s = outerPost s1 \<and> outerVis s = outerVis s1 \<and> outerOwner s = outerOwner s1 \<and> sentOuterFriendIDs s = sentOuterFriendIDs s1 \<and> recvOuterFriendIDs s = recvOuterFriendIDs s1 \<and> pendingCApiReqs s = pendingCApiReqs s1 \<and> cApiReq s = cApiReq s1 \<and> clientApiIDs s = clientApiIDs s1 \<and> clientPass s = clientPass s1 \<and> sharedWith s = sharedWith s1; uu1 = uu2\<rbrakk> \<Longrightarrow> admin (s\<lparr>sharedWith := uu1\<rparr>) = admin (s1\<lparr>sharedWith := uu2\<rparr>) \<and> pendingUReqs (s\<lparr>sharedWith := uu1\<rparr>) = pendingUReqs (s1\<lparr>sharedWith := uu2\<rparr>) \<and> userReq (s\<lparr>sharedWith := uu1\<rparr>) = userReq (s1\<lparr>sharedWith := uu2\<rparr>) \<and> userIDs (s\<lparr>sharedWith := uu1\<rparr>) = userIDs (s1\<lparr>sharedWith := uu2\<rparr>) \<and> user (s\<lparr>sharedWith := uu1\<rparr>) = user (s1\<lparr>sharedWith := uu2\<rparr>) \<and> pass (s\<lparr>sharedWith := uu1\<rparr>) = pass (s1\<lparr>sharedWith := uu2\<rparr>) \<and> eqButUIDf (pendingFReqs (s\<lparr>sharedWith := uu1\<rparr>)) (pendingFReqs (s1\<lparr>sharedWith := uu2\<rparr>)) \<and> eqButUID12 (friendReq (s\<lparr>sharedWith := uu1\<rparr>)) (friendReq (s1\<lparr>sharedWith := uu2\<rparr>)) \<and> eqButUIDf (friendIDs (s\<lparr>sharedWith := uu1\<rparr>)) (friendIDs (s1\<lparr>sharedWith := uu2\<rparr>)) \<and> postIDs (s\<lparr>sharedWith := uu1\<rparr>) = postIDs (s1\<lparr>sharedWith := uu2\<rparr>) \<and> admin (s\<lparr>sharedWith := uu1\<rparr>) = admin (s1\<lparr>sharedWith := uu2\<rparr>) \<and> post (s\<lparr>sharedWith := uu1\<rparr>) = post (s1\<lparr>sharedWith := uu2\<rparr>) \<and> vis (s\<lparr>sharedWith := uu1\<rparr>) = vis (s1\<lparr>sharedWith := uu2\<rparr>) \<and> owner (s\<lparr>sharedWith := uu1\<rparr>) = owner (s1\<lparr>sharedWith := uu2\<rparr>) \<and> pendingSApiReqs (s\<lparr>sharedWith := uu1\<rparr>) = pendingSApiReqs (s1\<lparr>sharedWith := uu2\<rparr>) \<and> sApiReq (s\<lparr>sharedWith := uu1\<rparr>) = sApiReq (s1\<lparr>sharedWith := uu2\<rparr>) \<and> serverApiIDs (s\<lparr>sharedWith := uu1\<rparr>) = serverApiIDs (s1\<lparr>sharedWith := uu2\<rparr>) \<and> serverPass (s\<lparr>sharedWith := uu1\<rparr>) = serverPass (s1\<lparr>sharedWith := uu2\<rparr>) \<and> outerPostIDs (s\<lparr>sharedWith := uu1\<rparr>) = outerPostIDs (s1\<lparr>sharedWith := uu2\<rparr>) \<and> outerPost (s\<lparr>sharedWith := uu1\<rparr>) = outerPost (s1\<lparr>sharedWith := uu2\<rparr>) \<and> outerVis (s\<lparr>sharedWith := uu1\<rparr>) = outerVis (s1\<lparr>sharedWith := uu2\<rparr>) \<and> outerOwner (s\<lparr>sharedWith := uu1\<rparr>) = outerOwner (s1\<lparr>sharedWith := uu2\<rparr>) \<and> sentOuterFriendIDs (s\<lparr>sharedWith := uu1\<rparr>) = sentOuterFriendIDs (s1\<lparr>sharedWith := uu2\<rparr>) \<and> recvOuterFriendIDs (s\<lparr>sharedWith := uu1\<rparr>) = recvOuterFriendIDs (s1\<lparr>sharedWith := uu2\<rparr>) \<and> pendingCApiReqs (s\<lparr>sharedWith := uu1\<rparr>) = pendingCApiReqs (s1\<lparr>sharedWith := uu2\<rparr>) \<and> cApiReq (s\<lparr>sharedWith := uu1\<rparr>) = cApiReq (s1\<lparr>sharedWith := uu2\<rparr>) \<and> clientApiIDs (s\<lparr>sharedWith := uu1\<rparr>) = clientApiIDs (s1\<lparr>sharedWith := uu2\<rparr>) \<and> clientPass (s\<lparr>sharedWith := uu1\<rparr>) = clientPass (s1\<lparr>sharedWith := uu2\<rparr>) \<and> sharedWith (s\<lparr>sharedWith := uu1\<rparr>) = sharedWith (s1\<lparr>sharedWith := uu2\<rparr>))
[PROOF STEP]
by auto