[STATEMENT]
lemma spmf_samp_uni_eq_return_bool_mod:
  shows "spmf (do {
          x1 \<leftarrow> sample_uniform q;
          return_spmf (int x1 = y mod q)}) True = 1/q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spmf (sample_uniform q \<bind> (\<lambda>x1. return_spmf (int x1 = int (y mod q)))) True = 1 / real q
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. spmf (sample_uniform q \<bind> (\<lambda>x1. return_spmf (int x1 = int (y mod q)))) True = 1 / real q
[PROOF STEP]
have "spmf (do {
          x1 \<leftarrow> sample_uniform q;
          return_spmf (x1 = y mod q)}) True = spmf (sample_uniform q \<bind> (\<lambda> x1. return_spmf x1)) (y mod q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spmf (sample_uniform q \<bind> (\<lambda>x1. return_spmf (x1 = y mod q))) True = spmf (sample_uniform q \<bind> return_spmf) (y mod q)
[PROOF STEP]
apply(simp only: spmf_bind)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LINT x|measure_spmf (sample_uniform q). spmf (return_spmf (x = y mod q)) True = LINT x|measure_spmf (sample_uniform q). spmf (return_spmf x) (y mod q)
[PROOF STEP]
apply(rule Bochner_Integration.integral_cong[OF refl])+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> space (measure_spmf (sample_uniform q)) \<Longrightarrow> spmf (return_spmf (x = y mod q)) True = spmf (return_spmf x) (y mod q)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> space (measure_spmf (sample_uniform q)) \<Longrightarrow> spmf (return_spmf (x = y mod q)) True = spmf (return_spmf x) (y mod q)
[PROOF STEP]
fix x :: nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> space (measure_spmf (sample_uniform q)) \<Longrightarrow> spmf (return_spmf (x = y mod q)) True = spmf (return_spmf x) (y mod q)
[PROOF STEP]
have "y mod q = x \<longrightarrow> indicator {True} (x = (y mod q)) = (indicator {(y mod q)} x::real)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y mod q = x \<longrightarrow> indicat_real {True} (x = y mod q) = indicat_real {y mod q} x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
y mod q = x \<longrightarrow> indicat_real {True} (x = y mod q) = indicat_real {y mod q} x

goal (1 subgoal):
 1. \<And>x. x \<in> space (measure_spmf (sample_uniform q)) \<Longrightarrow> spmf (return_spmf (x = y mod q)) True = spmf (return_spmf x) (y mod q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y mod q = x \<longrightarrow> indicat_real {True} (x = y mod q) = indicat_real {y mod q} x
[PROOF STEP]
have "indicator {True} (x = y mod q) = (indicator {y mod q} x::real)"
[PROOF STATE]
proof (prove)
using this:
y mod q = x \<longrightarrow> indicat_real {True} (x = y mod q) = indicat_real {y mod q} x

goal (1 subgoal):
 1. indicat_real {True} (x = y mod q) = indicat_real {y mod q} x
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
indicat_real {True} (x = y mod q) = indicat_real {y mod q} x

goal (1 subgoal):
 1. \<And>x. x \<in> space (measure_spmf (sample_uniform q)) \<Longrightarrow> spmf (return_spmf (x = y mod q)) True = spmf (return_spmf x) (y mod q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
indicat_real {True} (x = y mod q) = indicat_real {y mod q} x
[PROOF STEP]
show "spmf (return_spmf (x = y mod q)) True = spmf (return_spmf x) (y mod q)"
[PROOF STATE]
proof (prove)
using this:
indicat_real {True} (x = y mod q) = indicat_real {y mod q} x

goal (1 subgoal):
 1. spmf (return_spmf (x = y mod q)) True = spmf (return_spmf x) (y mod q)
[PROOF STEP]
by (metis pmf_return spmf_of_pmf_return_pmf spmf_spmf_of_pmf)
[PROOF STATE]
proof (state)
this:
spmf (return_spmf (x = y mod q)) True = spmf (return_spmf x) (y mod q)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
spmf (sample_uniform q \<bind> (\<lambda>x1. return_spmf (x1 = y mod q))) True = spmf (sample_uniform q \<bind> return_spmf) (y mod q)

goal (1 subgoal):
 1. spmf (sample_uniform q \<bind> (\<lambda>x1. return_spmf (int x1 = int (y mod q)))) True = 1 / real q
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
spmf (sample_uniform q \<bind> (\<lambda>x1. return_spmf (x1 = y mod q))) True = spmf (sample_uniform q \<bind> return_spmf) (y mod q)

goal (1 subgoal):
 1. spmf (sample_uniform q \<bind> (\<lambda>x1. return_spmf (int x1 = int (y mod q)))) True = 1 / real q
[PROOF STEP]
using samp_uni_spmf_mod_q
[PROOF STATE]
proof (prove)
using this:
spmf (sample_uniform q \<bind> (\<lambda>x1. return_spmf (x1 = y mod q))) True = spmf (sample_uniform q \<bind> return_spmf) (y mod q)
spmf (sample_uniform q) (?x mod q) = 1 / real q

goal (1 subgoal):
 1. spmf (sample_uniform q \<bind> (\<lambda>x1. return_spmf (int x1 = int (y mod q)))) True = 1 / real q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
spmf (sample_uniform q \<bind> (\<lambda>x1. return_spmf (int x1 = int (y mod q)))) True = 1 / real q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma int_or_zero [simp]: "0 OR x = x"
  for x :: int
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 OR x = x
[PROOF STEP]
by (fact or.left_neutral)


[STATEMENT]
lemma (in category) id_dom_cod:
  assumes "A \<in> Ob"
  shows "Dom (Id A) = A" and "Cod (Id A) = A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Dom (Id A) = A &&& Cod (Id A) = A
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Dom (Id A) = A
 2. Cod (Id A) = A
[PROOF STEP]
from \<open>A \<in> Ob\<close>
[PROOF STATE]
proof (chain)
picking this:
A \<in> Ob
[PROOF STEP]
have 1: "Id A \<in> Hom A A"
[PROOF STATE]
proof (prove)
using this:
A \<in> Ob

goal (1 subgoal):
 1. Id A \<in> Hom A A
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
Id A \<in> Hom A A

goal (2 subgoals):
 1. Dom (Id A) = A
 2. Cod (Id A) = A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Id A \<in> Hom A A
[PROOF STEP]
show "Dom (Id A) = A" and "Cod (Id A) = A"
[PROOF STATE]
proof (prove)
using this:
Id A \<in> Hom A A

goal (1 subgoal):
 1. Dom (Id A) = A &&& Cod (Id A) = A
[PROOF STEP]
by (simp_all add: hom_def)
[PROOF STATE]
proof (state)
this:
Dom (Id A) = A
Cod (Id A) = A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma one_less_inverse:
  "0 < a \<Longrightarrow> a < 1 \<Longrightarrow> 1 < inverse a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(0::'a) < a; a < (1::'a)\<rbrakk> \<Longrightarrow> (1::'a) < inverse a
[PROOF STEP]
using less_imp_inverse_less [of a 1, unfolded inverse_1]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>a < (1::'a); (0::'a) < a\<rbrakk> \<Longrightarrow> (1::'a) < inverse a

goal (1 subgoal):
 1. \<lbrakk>(0::'a) < a; a < (1::'a)\<rbrakk> \<Longrightarrow> (1::'a) < inverse a
[PROOF STEP]
.


[STATEMENT]
lemma le_divide_eq_1_neg [simp]:
  "a < 0 \<Longrightarrow> (1 \<le> b/a) = (b \<le> a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a < (0::'a) \<Longrightarrow> ((1::'a) \<le> b / a) = (b \<le> a)
[PROOF STEP]
by (metis local.le_divide_eq_1_pos local.minus_divide_divide local.neg_0_less_iff_less local.neg_le_iff_le)


[STATEMENT]
lemma eqButUID12_cong:
assumes "eqButUID12 freq freq1"
(*and "uid = UID1 \<Longrightarrow> eqButUID2 uu uu1"*)
and "\<not> (uid,uid') \<in> {(UID1,UID2), (UID2,UID1)} \<Longrightarrow> uu = uu1"
shows "eqButUID12 (fun_upd2 freq uid uid' uu) (fun_upd2 freq1 uid uid' uu1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqButUID12 (fun_upd2 freq uid uid' uu) (fun_upd2 freq1 uid uid' uu1)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
eqButUID12 freq freq1
(uid, uid') \<notin> {(UID1, UID2), (UID2, UID1)} \<Longrightarrow> uu = uu1

goal (1 subgoal):
 1. eqButUID12 (fun_upd2 freq uid uid' uu) (fun_upd2 freq1 uid uid' uu1)
[PROOF STEP]
unfolding eqButUID12_def fun_upd2_def
[PROOF STATE]
proof (prove)
using this:
\<forall>uid uid'. if (uid, uid') \<in> {(UID1, UID2), (UID2, UID1)} then True else freq uid uid' = freq1 uid uid'
(uid, uid') \<notin> {(UID1, UID2), (UID2, UID1)} \<Longrightarrow> uu = uu1

goal (1 subgoal):
 1. \<forall>uida uid'a. if (uida, uid'a) \<in> {(UID1, UID2), (UID2, UID1)} then True else (if uid = uida \<and> uid' = uid'a then uu else freq uida uid'a) = (if uid = uida \<and> uid' = uid'a then uu1 else freq1 uida uid'a)
[PROOF STEP]
by (auto split: if_splits)


[STATEMENT]
lemma eqButUID_step:
assumes ss1: "eqButUID s s1"
and step: "step s a = (ou,s')"
and step1: "step s1 a = (ou1,s1')"
and rs: "reach s"
and rs1: "reach s1"
shows "eqButUID s' s1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqButUID s' s1'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eqButUID s' s1'
[PROOF STEP]
note simps = eqButUID_def s_defs c_defs u_defs r_defs l_defs
[PROOF STATE]
proof (state)
this:
eqButUID ?s ?s1.0 \<equiv> admin ?s = admin ?s1.0 \<and> pendingUReqs ?s = pendingUReqs ?s1.0 \<and> userReq ?s = userReq ?s1.0 \<and> userIDs ?s = userIDs ?s1.0 \<and> user ?s = user ?s1.0 \<and> pass ?s = pass ?s1.0 \<and> eqButUIDf (pendingFReqs ?s) (pendingFReqs ?s1.0) \<and> eqButUID12 (friendReq ?s) (friendReq ?s1.0) \<and> eqButUIDf (friendIDs ?s) (friendIDs ?s1.0) \<and> postIDs ?s = postIDs ?s1.0 \<and> admin ?s = admin ?s1.0 \<and> post ?s = post ?s1.0 \<and> owner ?s = owner ?s1.0 \<and> vis ?s = vis ?s1.0
e_startSys ?s ?uID ?p \<equiv> userIDs ?s = []
startSys ?s ?uID ?p \<equiv> ?s\<lparr>admin := ?uID, userIDs := [?uID], user := (user ?s)(?uID := emptyUser), pass := (pass ?s)(?uID := ?p)\<rparr>
e_createNUReq ?s ?uID ?req \<equiv> admin ?s \<in>\<in> userIDs ?s \<and> ?uID \<notin> set (userIDs ?s) \<and> ?uID \<notin> set (pendingUReqs ?s)
createNUReq ?s ?uID ?reqInfo \<equiv> ?s\<lparr>pendingUReqs := pendingUReqs ?s ## ?uID, userReq := (userReq ?s)(?uID := ?reqInfo)\<rparr>
e_createUser ?s ?uID ?p ?uID' ?p' \<equiv> IDsOK ?s [?uID] [] \<and> pass ?s ?uID = ?p \<and> ?uID = admin ?s \<and> ?uID' \<in>\<in> pendingUReqs ?s
createUser ?s ?uID ?p ?uID' ?p' \<equiv> ?s\<lparr>userIDs := ?uID' # userIDs ?s, user := (user ?s)(?uID' := emptyUser), pass := (pass ?s)(?uID' := ?p'), pendingUReqs := remove1 ?uID' (pendingUReqs ?s), userReq := (userReq ?s)(?uID := emptyReq)\<rparr>
e_createFriendReq ?s ?uID ?p ?uID' ?req \<equiv> IDsOK ?s [?uID, ?uID'] [] \<and> pass ?s ?uID = ?p \<and> ?uID \<notin> set (pendingFReqs ?s ?uID') \<and> ?uID \<notin> set (friendIDs ?s ?uID')
createFriendReq ?s ?uID ?p ?uID' ?req \<equiv> let pfr = pendingFReqs ?s in ?s\<lparr>pendingFReqs := pfr(?uID' := pfr ?uID' ## ?uID), friendReq := fun_upd2 (friendReq ?s) ?uID ?uID' ?req\<rparr>
e_createFriend ?s ?uID ?p ?uID' \<equiv> IDsOK ?s [?uID, ?uID'] [] \<and> pass ?s ?uID = ?p \<and> ?uID' \<in>\<in> pendingFReqs ?s ?uID
createFriend ?s ?uID ?p ?uID' \<equiv> let fr = friendIDs ?s; pfr = pendingFReqs ?s in ?s\<lparr>friendIDs := fr(?uID := fr ?uID ## ?uID', ?uID' := fr ?uID' ## ?uID), pendingFReqs := pfr(?uID := remove1 ?uID' (pfr ?uID), ?uID' := remove1 ?uID (pfr ?uID')), friendReq := fun_upd2 (fun_upd2 (friendReq ?s) ?uID' ?uID emptyReq) ?uID ?uID' emptyReq\<rparr>
e_createPost ?s ?uID ?p ?pID ?title \<equiv> IDsOK ?s [?uID] [] \<and> pass ?s ?uID = ?p \<and> ?pID \<notin> set (postIDs ?s)
createPost ?s ?uID ?p ?pID ?title \<equiv> ?s\<lparr>postIDs := ?pID # postIDs ?s, post := (post ?s)(?pID := Ntc ?title emptyText emptyImg), owner := (owner ?s)(?pID := ?uID)\<rparr>
e_updateUser ?s ?uID ?p ?p' ?name ?info \<equiv> IDsOK ?s [?uID] [] \<and> pass ?s ?uID = ?p
updateUser ?s ?uID ?p ?p' ?name ?info \<equiv> ?s\<lparr>user := (user ?s)(?uID := Usr ?name ?info), pass := (pass ?s)(?uID := ?p')\<rparr>
e_updatePost ?s ?uID ?p ?pID ?pst \<equiv> IDsOK ?s [?uID] [?pID] \<and> pass ?s ?uID = ?p \<and> owner ?s ?pID = ?uID
updatePost ?s ?uID ?p ?pID ?pst \<equiv> ?s\<lparr>post := (post ?s)(?pID := ?pst)\<rparr>
e_updateVisPost ?s ?uID ?p ?pID ?vs \<equiv> IDsOK ?s [?uID] [?pID] \<and> pass ?s ?uID = ?p \<and> owner ?s ?pID = ?uID \<and> ?vs \<in> {FriendV, PublicV}
updateVisPost ?s ?uID ?p ?pID ?vs \<equiv> ?s\<lparr>vis := (vis ?s)(?pID := ?vs)\<rparr>
readNUReq ?s ?uID ?p ?uID' \<equiv> userReq ?s ?uID'
e_readNUReq ?s ?uID ?p ?uID' \<equiv> IDsOK ?s [?uID] [] \<and> pass ?s ?uID = ?p \<and> ?uID = admin ?s \<and> ?uID' \<in>\<in> pendingUReqs ?s
readUser ?s ?uID ?p ?uID' \<equiv> niUser (user ?s ?uID')
e_readUser ?s ?uID ?p ?uID' \<equiv> IDsOK ?s [?uID, ?uID'] [] \<and> pass ?s ?uID = ?p
readAmIAdmin ?s ?uID ?p \<equiv> ?uID = admin ?s
e_readAmIAdmin ?s ?uID ?p \<equiv> IDsOK ?s [?uID] [] \<and> pass ?s ?uID = ?p
readPost ?s ?uID ?p ?pID \<equiv> post ?s ?pID
e_readPost ?s ?uID ?p ?pID \<equiv> let post = post ?s ?pID in IDsOK ?s [?uID] [?pID] \<and> pass ?s ?uID = ?p \<and> (owner ?s ?pID = ?uID \<or> ?uID \<in>\<in> friendIDs ?s (owner ?s ?pID) \<or> vis ?s ?pID = PublicV)
readVisPost ?s ?uID ?p ?pID \<equiv> vis ?s ?pID
e_readVisPost ?s ?uID ?p ?pID \<equiv> let post = post ?s ?pID in IDsOK ?s [?uID] [?pID] \<and> pass ?s ?uID = ?p \<and> (owner ?s ?pID = ?uID \<or> ?uID \<in>\<in> friendIDs ?s (owner ?s ?pID) \<or> vis ?s ?pID = PublicV)
readOwnerPost ?s ?uID ?p ?pID \<equiv> owner ?s ?pID
e_readOwnerPost ?s ?uID ?p ?pID \<equiv> let post = post ?s ?pID in IDsOK ?s [?uID] [?pID] \<and> pass ?s ?uID = ?p \<and> (owner ?s ?pID = ?uID \<or> ?uID \<in>\<in> friendIDs ?s (owner ?s ?pID) \<or> vis ?s ?pID = PublicV)
readFriendReqToMe ?s ?uID ?p ?uID' \<equiv> friendReq ?s ?uID' ?uID
e_readFriendReqToMe ?s ?uID ?p ?uID' \<equiv> IDsOK ?s [?uID, ?uID'] [] \<and> pass ?s ?uID = ?p \<and> ?uID' \<in>\<in> pendingFReqs ?s ?uID
readFriendReqFromMe ?s ?uID ?p ?uID' \<equiv> friendReq ?s ?uID ?uID'
e_readFriendReqFromMe ?s ?uID ?p ?uID' \<equiv> IDsOK ?s [?uID, ?uID'] [] \<and> pass ?s ?uID = ?p \<and> ?uID \<in>\<in> pendingFReqs ?s ?uID'
listPendingUReqs ?s ?uID ?p \<equiv> pendingUReqs ?s
e_listPendingUReqs ?s ?uID ?p \<equiv> IDsOK ?s [?uID] [] \<and> pass ?s ?uID = ?p \<and> ?uID = admin ?s
listAllUsers ?s ?uID ?p \<equiv> userIDs ?s
e_listAllUsers ?s ?uID ?p \<equiv> IDsOK ?s [?uID] [] \<and> pass ?s ?uID = ?p
listFriends ?s ?uID ?p ?uID' \<equiv> friendIDs ?s ?uID'
e_listFriends ?s ?uID ?p ?uID' \<equiv> IDsOK ?s [?uID, ?uID'] [] \<and> pass ?s ?uID = ?p \<and> (?uID = ?uID' \<or> ?uID \<in>\<in> friendIDs ?s ?uID')
listPosts ?s ?uID ?p \<equiv> cmap (\<lambda>pID. if vis ?s pID = PublicV \<or> ?uID \<in>\<in> friendIDs ?s (owner ?s pID) \<or> ?uID = owner ?s pID then [(owner ?s pID, pID)] else []) (postIDs ?s)
e_listPosts ?s ?uID ?p \<equiv> IDsOK ?s [?uID] [] \<and> pass ?s ?uID = ?p

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fetch_bef_erase_b_b:
  assumes "n < length lm" "0 < s" "s \<le> 2 * n" "s mod 2 = 0"
  shows "(fetch (mopup_a n @ shift mopup_b (2 * n)) s Bk) = (R, s - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fetch (mopup_a n @ shift mopup_b (2 * n)) s Bk = (R, s - 1)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fetch (mopup_a n @ shift mopup_b (2 * n)) s Bk = (R, s - 1)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
n < length lm
0 < s
s \<le> 2 * n
is_even s
[PROOF STEP]
obtain q where q:"s = 2 * q"
[PROOF STATE]
proof (prove)
using this:
n < length lm
0 < s
s \<le> 2 * n
is_even s

goal (1 subgoal):
 1. (\<And>q. s = 2 * q \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s = 2 * q

goal (1 subgoal):
 1. fetch (mopup_a n @ shift mopup_b (2 * n)) s Bk = (R, s - 1)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s = 2 * q
[PROOF STEP]
obtain nat where nat:"q = Suc nat"
[PROOF STATE]
proof (prove)
using this:
s = 2 * q

goal (1 subgoal):
 1. (\<And>nat. q = Suc nat \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
s = 2 * q
0 < s

goal (1 subgoal):
 1. (\<And>nat. q = Suc nat \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases q, auto)
[PROOF STATE]
proof (state)
this:
q = Suc nat

goal (1 subgoal):
 1. fetch (mopup_a n @ shift mopup_b (2 * n)) s Bk = (R, s - 1)
[PROOF STEP]
from assms(3) mopup_a_nth[of nat n 2]
[PROOF STATE]
proof (chain)
picking this:
s \<le> 2 * n
\<lbrakk>nat < n; 2 < 4\<rbrakk> \<Longrightarrow> mopup_a n ! (4 * nat + 2) = mopup_a (Suc nat) ! (4 * nat + 2)
[PROOF STEP]
have "mopup_a n ! (4 * nat + 2) = mopup_a (Suc nat) ! ((4 * nat) + 2)"
[PROOF STATE]
proof (prove)
using this:
s \<le> 2 * n
\<lbrakk>nat < n; 2 < 4\<rbrakk> \<Longrightarrow> mopup_a n ! (4 * nat + 2) = mopup_a (Suc nat) ! (4 * nat + 2)

goal (1 subgoal):
 1. mopup_a n ! (4 * nat + 2) = mopup_a (Suc nat) ! (4 * nat + 2)
[PROOF STEP]
unfolding nat q
[PROOF STATE]
proof (prove)
using this:
2 * Suc nat \<le> 2 * n
\<lbrakk>nat < n; 2 < 4\<rbrakk> \<Longrightarrow> mopup_a n ! (4 * nat + 2) = mopup_a (Suc nat) ! (4 * nat + 2)

goal (1 subgoal):
 1. mopup_a n ! (4 * nat + 2) = mopup_a (Suc nat) ! (4 * nat + 2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mopup_a n ! (4 * nat + 2) = mopup_a (Suc nat) ! (4 * nat + 2)

goal (1 subgoal):
 1. fetch (mopup_a n @ shift mopup_b (2 * n)) s Bk = (R, s - 1)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
mopup_a n ! (4 * nat + 2) = mopup_a (Suc nat) ! (4 * nat + 2)

goal (1 subgoal):
 1. fetch (mopup_a n @ shift mopup_b (2 * n)) s Bk = (R, s - 1)
[PROOF STEP]
using assms nat q
[PROOF STATE]
proof (prove)
using this:
mopup_a n ! (4 * nat + 2) = mopup_a (Suc nat) ! (4 * nat + 2)
n < length lm
0 < s
s \<le> 2 * n
is_even s
q = Suc nat
s = 2 * q

goal (1 subgoal):
 1. fetch (mopup_a n @ shift mopup_b (2 * n)) s Bk = (R, s - 1)
[PROOF STEP]
by (auto simp: nth_append)
[PROOF STATE]
proof (state)
this:
fetch (mopup_a n @ shift mopup_b (2 * n)) s Bk = (R, s - 1)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma butlast_split: "n < length q \<Longrightarrow> butlast q = (take n q)@(drop n (butlast q))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < length q \<Longrightarrow> butlast q = take n q @ drop n (butlast q)
[PROOF STEP]
by (metis append_take_drop_id take_butlast)