[STATEMENT]
lemma eqButUID_stateSelectors:
"eqButUID s s1 \<Longrightarrow>
 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>
 owner s = owner s1 \<and>
 vis s = vis s1 \<and>

 IDsOK s = IDsOK s1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqButUID s s1 \<Longrightarrow> 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> owner s = owner s1 \<and> vis s = vis s1 \<and> IDsOK s = IDsOK s1
[PROOF STEP]
unfolding eqButUID_def IDsOK_def[abs_def]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 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> owner s = owner s1 \<and> vis s = vis s1 \<Longrightarrow> 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> owner s = owner s1 \<and> vis s = vis s1 \<and> (\<lambda>uIDs pIDs. list_all (\<lambda>uID. uID \<in>\<in> userIDs s) uIDs \<and> list_all (\<lambda>pID. pID \<in>\<in> postIDs s) pIDs) = (\<lambda>uIDs pIDs. list_all (\<lambda>uID. uID \<in>\<in> userIDs s1) uIDs \<and> list_all (\<lambda>pID. pID \<in>\<in> postIDs s1) pIDs)
[PROOF STEP]
by auto


[STATEMENT]
lemma eqButUID_eqButUID2:
"eqButUID s s1 \<Longrightarrow> eqButUIDl UID2 (friendIDs s UID1) (friendIDs s1 UID1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqButUID s s1 \<Longrightarrow> eqButUIDl UID2 (friendIDs s UID1) (friendIDs s1 UID1)
[PROOF STEP]
unfolding eqButUID_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 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> owner s = owner s1 \<and> vis s = vis s1 \<Longrightarrow> eqButUIDl UID2 (friendIDs s UID1) (friendIDs s1 UID1)
[PROOF STEP]
using eqButUIDf_eqButUIDl
[PROOF STATE]
proof (prove)
using this:
eqButUIDf ?frds ?frds1.0 \<Longrightarrow> eqButUIDl UID2 (?frds UID1) (?frds1.0 UID1)
eqButUIDf ?frds ?frds1.0 \<Longrightarrow> eqButUIDl UID1 (?frds UID2) (?frds1.0 UID2)

goal (1 subgoal):
 1. 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> owner s = owner s1 \<and> vis s = vis s1 \<Longrightarrow> eqButUIDl UID2 (friendIDs s UID1) (friendIDs s1 UID1)
[PROOF STEP]
by (smt eqButUIDf_eqButUIDl eqButUIDl.simps)


[STATEMENT]
lemma eqButUID_not_UID:
"eqButUID s s1 \<Longrightarrow> uid \<noteq> UID \<Longrightarrow> post s uid = post s1 uid"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>eqButUID s s1; uid \<noteq> UID\<rbrakk> \<Longrightarrow> post s uid = post s1 uid
[PROOF STEP]
unfolding eqButUID_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<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> owner s = owner s1 \<and> vis s = vis s1; uid \<noteq> UID\<rbrakk> \<Longrightarrow> post s uid = post s1 uid
[PROOF STEP]
by auto


[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>)"
[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>))
[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> owner s = owner s1 \<and> vis s = vis 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> owner (s\<lparr>admin := uu1\<rparr>) = owner (s1\<lparr>admin := uu2\<rparr>) \<and> vis (s\<lparr>admin := uu1\<rparr>) = vis (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> owner s = owner s1 \<and> vis s = vis 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> owner (s\<lparr>pendingUReqs := uu1\<rparr>) = owner (s1\<lparr>pendingUReqs := uu2\<rparr>) \<and> vis (s\<lparr>pendingUReqs := uu1\<rparr>) = vis (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> owner s = owner s1 \<and> vis s = vis 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> owner (s\<lparr>userReq := uu1\<rparr>) = owner (s1\<lparr>userReq := uu2\<rparr>) \<and> vis (s\<lparr>userReq := uu1\<rparr>) = vis (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> owner s = owner s1 \<and> vis s = vis 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> owner (s\<lparr>userIDs := uu1\<rparr>) = owner (s1\<lparr>userIDs := uu2\<rparr>) \<and> vis (s\<lparr>userIDs := uu1\<rparr>) = vis (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> owner s = owner s1 \<and> vis s = vis 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> owner (s\<lparr>user := uu1\<rparr>) = owner (s1\<lparr>user := uu2\<rparr>) \<and> vis (s\<lparr>user := uu1\<rparr>) = vis (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> owner s = owner s1 \<and> vis s = vis 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> owner (s\<lparr>pass := uu1\<rparr>) = owner (s1\<lparr>pass := uu2\<rparr>) \<and> vis (s\<lparr>pass := uu1\<rparr>) = vis (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> owner s = owner s1 \<and> vis s = vis 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> owner (s\<lparr>postIDs := uu1\<rparr>) = owner (s1\<lparr>postIDs := uu2\<rparr>) \<and> vis (s\<lparr>postIDs := uu1\<rparr>) = vis (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> owner s = owner s1 \<and> vis s = vis 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> owner (s\<lparr>owner := uu1\<rparr>) = owner (s1\<lparr>owner := uu2\<rparr>) \<and> vis (s\<lparr>owner := uu1\<rparr>) = vis (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> owner s = owner s1 \<and> vis s = vis 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> owner (s\<lparr>post := uu1\<rparr>) = owner (s1\<lparr>post := uu2\<rparr>) \<and> vis (s\<lparr>post := uu1\<rparr>) = vis (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> owner s = owner s1 \<and> vis s = vis 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> owner (s\<lparr>vis := uu1\<rparr>) = owner (s1\<lparr>vis := uu2\<rparr>) \<and> vis (s\<lparr>vis := uu1\<rparr>) = vis (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> owner s = owner s1 \<and> vis s = vis 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> owner (s\<lparr>pendingFReqs := uu1\<rparr>) = owner (s1\<lparr>pendingFReqs := uu2\<rparr>) \<and> vis (s\<lparr>pendingFReqs := uu1\<rparr>) = vis (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> owner s = owner s1 \<and> vis s = vis 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> owner (s\<lparr>friendReq := uu1\<rparr>) = owner (s1\<lparr>friendReq := uu2\<rparr>) \<and> vis (s\<lparr>friendReq := uu1\<rparr>) = vis (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> owner s = owner s1 \<and> vis s = vis 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> owner (s\<lparr>friendIDs := uu1\<rparr>) = owner (s1\<lparr>friendIDs := uu2\<rparr>) \<and> vis (s\<lparr>friendIDs := uu1\<rparr>) = vis (s1\<lparr>friendIDs := uu2\<rparr>))
[PROOF STEP]
by auto