[STATEMENT]
lemma step_pendingFReqs:
assumes step: "step s a = (ou, s')"
and "\<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and>
           a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and>
           a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and>
           a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req)"
shows "uid \<in>\<in> pendingFReqs s' uid' \<longleftrightarrow> uid \<in>\<in> pendingFReqs s uid'" (is ?uid)
  and "uid' \<in>\<in> pendingFReqs s' uid \<longleftrightarrow> uid' \<in>\<in> pendingFReqs s uid" (is ?uid')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') &&& (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid')
 2. (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
step s a = (ou, s')
\<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req)
[PROOF STEP]
have "?uid \<and> ?uid'"
[PROOF STATE]
proof (prove)
using this:
step s a = (ou, s')
\<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req)

goal (1 subgoal):
 1. (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
[PROOF STEP]
proof (cases a)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>x1. \<lbrakk>step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); a = Sact x1\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
 2. \<And>x2. \<lbrakk>step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); a = Cact x2\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
 3. \<And>x3. \<lbrakk>step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); a = Dact x3\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
 4. \<And>x4. \<lbrakk>step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); a = Uact x4\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
 5. \<And>x5. \<lbrakk>step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); a = Ract x5\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
 6. \<And>x6. \<lbrakk>step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); a = Lact x6\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
 7. \<And>x7. \<lbrakk>step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); a = COMact x7\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
[PROOF STEP]
case (Sact sa)
[PROOF STATE]
proof (state)
this:
a = Sact sa

goal (7 subgoals):
 1. \<And>x1. \<lbrakk>step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); a = Sact x1\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
 2. \<And>x2. \<lbrakk>step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); a = Cact x2\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
 3. \<And>x3. \<lbrakk>step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); a = Dact x3\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
 4. \<And>x4. \<lbrakk>step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); a = Uact x4\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
 5. \<And>x5. \<lbrakk>step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); a = Ract x5\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
 6. \<And>x6. \<lbrakk>step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); a = Lact x6\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
 7. \<And>x7. \<lbrakk>step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); a = COMact x7\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a = Sact sa
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a = Sact sa

goal (1 subgoal):
 1. (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a = Sact sa
step s a = (ou, s')
\<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req)

goal (1 subgoal):
 1. (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
[PROOF STEP]
by (cases sa) (auto simp: s_defs)
[PROOF STATE]
proof (state)
this:
(uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)

goal (6 subgoals):
 1. \<And>x2. \<lbrakk>step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); a = Cact x2\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
 2. \<And>x3. \<lbrakk>step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); a = Dact x3\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
 3. \<And>x4. \<lbrakk>step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); a = Uact x4\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
 4. \<And>x5. \<lbrakk>step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); a = Ract x5\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
 5. \<And>x6. \<lbrakk>step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); a = Lact x6\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
 6. \<And>x7. \<lbrakk>step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); a = COMact x7\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>x2. \<lbrakk>step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); a = Cact x2\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
 2. \<And>x3. \<lbrakk>step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); a = Dact x3\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
 3. \<And>x4. \<lbrakk>step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); a = Uact x4\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
 4. \<And>x5. \<lbrakk>step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); a = Ract x5\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
 5. \<And>x6. \<lbrakk>step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); a = Lact x6\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
 6. \<And>x7. \<lbrakk>step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); a = COMact x7\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
[PROOF STEP]
case (Uact ua)
[PROOF STATE]
proof (state)
this:
a = Uact ua

goal (6 subgoals):
 1. \<And>x2. \<lbrakk>step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); a = Cact x2\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
 2. \<And>x3. \<lbrakk>step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); a = Dact x3\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
 3. \<And>x4. \<lbrakk>step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); a = Uact x4\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
 4. \<And>x5. \<lbrakk>step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); a = Ract x5\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
 5. \<And>x6. \<lbrakk>step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); a = Lact x6\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
 6. \<And>x7. \<lbrakk>step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); a = COMact x7\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a = Uact ua
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a = Uact ua

goal (1 subgoal):
 1. (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a = Uact ua
step s a = (ou, s')
\<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req)

goal (1 subgoal):
 1. (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
[PROOF STEP]
by (cases ua) (auto simp: u_defs)
[PROOF STATE]
proof (state)
this:
(uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)

goal (5 subgoals):
 1. \<And>x2. \<lbrakk>step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); a = Cact x2\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
 2. \<And>x3. \<lbrakk>step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); a = Dact x3\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
 3. \<And>x5. \<lbrakk>step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); a = Ract x5\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
 4. \<And>x6. \<lbrakk>step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); a = Lact x6\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
 5. \<And>x7. \<lbrakk>step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); a = COMact x7\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>x2. \<lbrakk>step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); a = Cact x2\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
 2. \<And>x3. \<lbrakk>step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); a = Dact x3\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
 3. \<And>x5. \<lbrakk>step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); a = Ract x5\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
 4. \<And>x6. \<lbrakk>step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); a = Lact x6\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
 5. \<And>x7. \<lbrakk>step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); a = COMact x7\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
[PROOF STEP]
case (COMact ca)
[PROOF STATE]
proof (state)
this:
a = COMact ca

goal (5 subgoals):
 1. \<And>x2. \<lbrakk>step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); a = Cact x2\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
 2. \<And>x3. \<lbrakk>step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); a = Dact x3\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
 3. \<And>x5. \<lbrakk>step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); a = Ract x5\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
 4. \<And>x6. \<lbrakk>step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); a = Lact x6\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
 5. \<And>x7. \<lbrakk>step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); a = COMact x7\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a = COMact ca
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a = COMact ca

goal (1 subgoal):
 1. (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a = COMact ca
step s a = (ou, s')
\<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req)

goal (1 subgoal):
 1. (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
[PROOF STEP]
by (cases ca) (auto simp: com_defs)
[PROOF STATE]
proof (state)
this:
(uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)

goal (4 subgoals):
 1. \<And>x2. \<lbrakk>step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); a = Cact x2\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
 2. \<And>x3. \<lbrakk>step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); a = Dact x3\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
 3. \<And>x5. \<lbrakk>step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); a = Ract x5\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
 4. \<And>x6. \<lbrakk>step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); a = Lact x6\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x2. \<lbrakk>step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); a = Cact x2\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
 2. \<And>x3. \<lbrakk>step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); a = Dact x3\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
 3. \<And>x5. \<lbrakk>step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); a = Ract x5\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
 4. \<And>x6. \<lbrakk>step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); a = Lact x6\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
[PROOF STEP]
case (Cact ca)
[PROOF STATE]
proof (state)
this:
a = Cact ca

goal (4 subgoals):
 1. \<And>x2. \<lbrakk>step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); a = Cact x2\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
 2. \<And>x3. \<lbrakk>step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); a = Dact x3\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
 3. \<And>x5. \<lbrakk>step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); a = Ract x5\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
 4. \<And>x6. \<lbrakk>step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); a = Lact x6\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a = Cact ca
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a = Cact ca

goal (1 subgoal):
 1. (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a = Cact ca
step s a = (ou, s')
\<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req)

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

goal (5 subgoals):
 1. \<And>x11 x12. \<lbrakk>a = Cact ca; step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); ca = cNUReq x11 x12\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
 2. \<And>x21 x22 x23 x24. \<lbrakk>a = Cact ca; step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); ca = cUser x21 x22 x23 x24\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
 3. \<And>x31 x32 x33. \<lbrakk>a = Cact ca; step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); ca = cPost x31 x32 x33\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
 4. \<And>x41 x42 x43 x44. \<lbrakk>a = Cact ca; step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); ca = cFriendReq x41 x42 x43 x44\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
 5. \<And>x51 x52 x53. \<lbrakk>a = Cact ca; step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); ca = cFriend x51 x52 x53\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ca = cFriend uid1 p uid1'
[PROOF STEP]
have "((uid1 = uid \<longrightarrow> uid1' \<noteq> uid') \<and> (uid1 = uid' \<longrightarrow> uid1' \<noteq> uid)) \<or> ou = outErr"
[PROOF STATE]
proof (prove)
using this:
ca = cFriend uid1 p uid1'

goal (1 subgoal):
 1. (uid1 = uid \<longrightarrow> uid1' \<noteq> uid') \<and> (uid1 = uid' \<longrightarrow> uid1' \<noteq> uid) \<or> ou = outErr
[PROOF STEP]
using Cact assms
[PROOF STATE]
proof (prove)
using this:
ca = cFriend uid1 p uid1'
a = Cact ca
step s a = (ou, s')
\<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req)

goal (1 subgoal):
 1. (uid1 = uid \<longrightarrow> uid1' \<noteq> uid') \<and> (uid1 = uid' \<longrightarrow> uid1' \<noteq> uid) \<or> ou = outErr
[PROOF STEP]
by (auto simp: c_defs)
[PROOF STATE]
proof (state)
this:
(uid1 = uid \<longrightarrow> uid1' \<noteq> uid') \<and> (uid1 = uid' \<longrightarrow> uid1' \<noteq> uid) \<or> ou = outErr

goal (5 subgoals):
 1. \<And>x11 x12. \<lbrakk>a = Cact ca; step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); ca = cNUReq x11 x12\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
 2. \<And>x21 x22 x23 x24. \<lbrakk>a = Cact ca; step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); ca = cUser x21 x22 x23 x24\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
 3. \<And>x31 x32 x33. \<lbrakk>a = Cact ca; step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); ca = cPost x31 x32 x33\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
 4. \<And>x41 x42 x43 x44. \<lbrakk>a = Cact ca; step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); ca = cFriendReq x41 x42 x43 x44\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
 5. \<And>x51 x52 x53. \<lbrakk>a = Cact ca; step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); ca = cFriend x51 x52 x53\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(uid1 = uid \<longrightarrow> uid1' \<noteq> uid') \<and> (uid1 = uid' \<longrightarrow> uid1' \<noteq> uid) \<or> ou = outErr
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(uid1 = uid \<longrightarrow> uid1' \<noteq> uid') \<and> (uid1 = uid' \<longrightarrow> uid1' \<noteq> uid) \<or> ou = outErr

goal (1 subgoal):
 1. (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
[PROOF STEP]
using step Cact cFriend
[PROOF STATE]
proof (prove)
using this:
(uid1 = uid \<longrightarrow> uid1' \<noteq> uid') \<and> (uid1 = uid' \<longrightarrow> uid1' \<noteq> uid) \<or> ou = outErr
step s a = (ou, s')
a = Cact ca
ca = cFriend uid1 p uid1'

goal (1 subgoal):
 1. (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
[PROOF STEP]
by (auto simp: c_defs)
[PROOF STATE]
proof (state)
this:
(uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)

goal (4 subgoals):
 1. \<And>x11 x12. \<lbrakk>a = Cact ca; step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); ca = cNUReq x11 x12\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
 2. \<And>x21 x22 x23 x24. \<lbrakk>a = Cact ca; step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); ca = cUser x21 x22 x23 x24\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
 3. \<And>x31 x32 x33. \<lbrakk>a = Cact ca; step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); ca = cPost x31 x32 x33\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
 4. \<And>x41 x42 x43 x44. \<lbrakk>a = Cact ca; step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); ca = cFriendReq x41 x42 x43 x44\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
[PROOF STEP]
qed (auto simp: c_defs)
[PROOF STATE]
proof (state)
this:
(uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)

goal (3 subgoals):
 1. \<And>x3. \<lbrakk>step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); a = Dact x3\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
 2. \<And>x5. \<lbrakk>step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); a = Ract x5\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
 3. \<And>x6. \<lbrakk>step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); a = Lact x6\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x3. \<lbrakk>step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); a = Dact x3\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
 2. \<And>x5. \<lbrakk>step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); a = Ract x5\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
 3. \<And>x6. \<lbrakk>step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); a = Lact x6\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
[PROOF STEP]
case (Dact da)
[PROOF STATE]
proof (state)
this:
a = Dact da

goal (3 subgoals):
 1. \<And>x3. \<lbrakk>step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); a = Dact x3\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
 2. \<And>x5. \<lbrakk>step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); a = Ract x5\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
 3. \<And>x6. \<lbrakk>step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); a = Lact x6\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a = Dact da
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a = Dact da

goal (1 subgoal):
 1. (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a = Dact da
step s a = (ou, s')
\<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req)

goal (1 subgoal):
 1. (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
[PROOF STEP]
by (cases da) (auto simp: d_defs)
[PROOF STATE]
proof (state)
this:
(uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)

goal (2 subgoals):
 1. \<And>x5. \<lbrakk>step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); a = Ract x5\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
 2. \<And>x6. \<lbrakk>step s a = (ou, s'); \<forall>req. a \<noteq> Cact (cFriend uid (pass s uid) uid') \<and> a \<noteq> Cact (cFriend uid' (pass s uid') uid) \<and> a \<noteq> Dact (dFriend uid (pass s uid) uid') \<and> a \<noteq> Dact (dFriend uid' (pass s uid') uid) \<and> a \<noteq> Cact (cFriendReq uid (pass s uid) uid' req) \<and> a \<noteq> Cact (cFriendReq uid' (pass s uid') uid req); a = Lact x6\<rbrakk> \<Longrightarrow> (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
(uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)

goal (2 subgoals):
 1. (uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid')
 2. (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)
[PROOF STEP]
show ?uid and ?uid'
[PROOF STATE]
proof (prove)
using this:
(uid \<in>\<in> pendingFReqs s' uid') = (uid \<in>\<in> pendingFReqs s uid') \<and> (uid' \<in>\<in> pendingFReqs s' uid) = (uid' \<in>\<in> pendingFReqs s uid)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eqButUID_friends12_set_friendIDs_eq:
assumes ss1: "eqButUID s s1"
and f12: "friends12 s = friends12 s1"
and rs: "reach s" and rs1: "reach s1"
shows "set (friendIDs s uid) = set (friendIDs s1 uid)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (friendIDs s uid) = set (friendIDs s1 uid)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. set (friendIDs s uid) = set (friendIDs s1 uid)
[PROOF STEP]
have dfIDs: "distinct (friendIDs s uid)" "distinct (friendIDs s1 uid)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (friendIDs s uid) &&& distinct (friendIDs s1 uid)
[PROOF STEP]
using reach_distinct_friends_reqs[OF rs] reach_distinct_friends_reqs[OF rs1]
[PROOF STATE]
proof (prove)
using this:
distinct (friendIDs s ?uid)
distinct (pendingFReqs s ?uid)
distinct (sentOuterFriendIDs s ?uid)
distinct (recvOuterFriendIDs s ?uid)
?uid' \<in>\<in> pendingFReqs s ?uid \<Longrightarrow> ?uid' \<notin> set (friendIDs s ?uid)
?uid' \<in>\<in> pendingFReqs s ?uid \<Longrightarrow> ?uid \<notin> set (friendIDs s ?uid')
distinct (friendIDs s1 ?uid)
distinct (pendingFReqs s1 ?uid)
distinct (sentOuterFriendIDs s1 ?uid)
distinct (recvOuterFriendIDs s1 ?uid)
?uid' \<in>\<in> pendingFReqs s1 ?uid \<Longrightarrow> ?uid' \<notin> set (friendIDs s1 ?uid)
?uid' \<in>\<in> pendingFReqs s1 ?uid \<Longrightarrow> ?uid \<notin> set (friendIDs s1 ?uid')

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

goal (1 subgoal):
 1. set (friendIDs s uid) = set (friendIDs s1 uid)
[PROOF STEP]
from f12
[PROOF STATE]
proof (chain)
picking this:
friends12 s = friends12 s1
[PROOF STEP]
have uid12: "UID1 \<in>\<in> friendIDs s UID2 \<longleftrightarrow> UID1 \<in>\<in> friendIDs s1 UID2"
                       "UID2 \<in>\<in> friendIDs s UID1 \<longleftrightarrow> UID2 \<in>\<in> friendIDs s1 UID1"
[PROOF STATE]
proof (prove)
using this:
friends12 s = friends12 s1

goal (1 subgoal):
 1. (UID1 \<in>\<in> friendIDs s UID2) = (UID1 \<in>\<in> friendIDs s1 UID2) &&& (UID2 \<in>\<in> friendIDs s UID1) = (UID2 \<in>\<in> friendIDs s1 UID1)
[PROOF STEP]
using reach_friendIDs_symmetric[OF rs] reach_friendIDs_symmetric[OF rs1]
[PROOF STATE]
proof (prove)
using this:
friends12 s = friends12 s1
(?uID1.0 \<in>\<in> friendIDs s ?uID2.0) = (?uID2.0 \<in>\<in> friendIDs s ?uID1.0)
(?uID1.0 \<in>\<in> friendIDs s1 ?uID2.0) = (?uID2.0 \<in>\<in> friendIDs s1 ?uID1.0)

goal (1 subgoal):
 1. (UID1 \<in>\<in> friendIDs s UID2) = (UID1 \<in>\<in> friendIDs s1 UID2) &&& (UID2 \<in>\<in> friendIDs s UID1) = (UID2 \<in>\<in> friendIDs s1 UID1)
[PROOF STEP]
unfolding friends12_def
[PROOF STATE]
proof (prove)
using this:
(UID1 \<in>\<in> friendIDs s UID2 \<and> UID2 \<in>\<in> friendIDs s UID1) = (UID1 \<in>\<in> friendIDs s1 UID2 \<and> UID2 \<in>\<in> friendIDs s1 UID1)
(?uID1.0 \<in>\<in> friendIDs s ?uID2.0) = (?uID2.0 \<in>\<in> friendIDs s ?uID1.0)
(?uID1.0 \<in>\<in> friendIDs s1 ?uID2.0) = (?uID2.0 \<in>\<in> friendIDs s1 ?uID1.0)

goal (1 subgoal):
 1. (UID1 \<in>\<in> friendIDs s UID2) = (UID1 \<in>\<in> friendIDs s1 UID2) &&& (UID2 \<in>\<in> friendIDs s UID1) = (UID2 \<in>\<in> friendIDs s1 UID1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(UID1 \<in>\<in> friendIDs s UID2) = (UID1 \<in>\<in> friendIDs s1 UID2)
(UID2 \<in>\<in> friendIDs s UID1) = (UID2 \<in>\<in> friendIDs s1 UID1)

goal (1 subgoal):
 1. set (friendIDs s uid) = set (friendIDs s1 uid)
[PROOF STEP]
from ss1
[PROOF STATE]
proof (chain)
picking this:
eqButUID s s1
[PROOF STEP]
have fIDs: "eqButUIDf (friendIDs s) (friendIDs s1)"
[PROOF STATE]
proof (prove)
using this:
eqButUID s s1

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

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

goal (1 subgoal):
 1. set (friendIDs s uid) = set (friendIDs s1 uid)
[PROOF STEP]
show "set (friendIDs s uid) = set (friendIDs s1 uid)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (friendIDs s uid) = set (friendIDs s1 uid)
[PROOF STEP]
proof (intro equalityI subsetI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in>\<in> friendIDs s uid \<Longrightarrow> x \<in>\<in> friendIDs s1 uid
 2. \<And>x. x \<in>\<in> friendIDs s1 uid \<Longrightarrow> x \<in>\<in> friendIDs s uid
[PROOF STEP]
fix uid'
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in>\<in> friendIDs s uid \<Longrightarrow> x \<in>\<in> friendIDs s1 uid
 2. \<And>x. x \<in>\<in> friendIDs s1 uid \<Longrightarrow> x \<in>\<in> friendIDs s uid
[PROOF STEP]
assume "uid' \<in>\<in> friendIDs s uid"
[PROOF STATE]
proof (state)
this:
uid' \<in>\<in> friendIDs s uid

goal (2 subgoals):
 1. \<And>x. x \<in>\<in> friendIDs s uid \<Longrightarrow> x \<in>\<in> friendIDs s1 uid
 2. \<And>x. x \<in>\<in> friendIDs s1 uid \<Longrightarrow> x \<in>\<in> friendIDs s uid
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
uid' \<in>\<in> friendIDs s uid
[PROOF STEP]
show "uid' \<in>\<in> friendIDs s1 uid"
[PROOF STATE]
proof (prove)
using this:
uid' \<in>\<in> friendIDs s uid

goal (1 subgoal):
 1. uid' \<in>\<in> friendIDs s1 uid
[PROOF STEP]
using fIDs dfIDs uid12 eqButUIDf_not_UID'
[PROOF STATE]
proof (prove)
using this:
uid' \<in>\<in> friendIDs s uid
eqButUIDf (friendIDs s) (friendIDs s1)
distinct (friendIDs s uid)
distinct (friendIDs s1 uid)
(UID1 \<in>\<in> friendIDs s UID2) = (UID1 \<in>\<in> friendIDs s1 UID2)
(UID2 \<in>\<in> friendIDs s UID1) = (UID2 \<in>\<in> friendIDs s1 UID1)
\<lbrakk>eqButUIDf ?frds ?frds1.0; (?uid, ?uid') \<notin> {(UID1, UID2), (UID2, UID1)}\<rbrakk> \<Longrightarrow> (?uid \<in>\<in> ?frds ?uid') = (?uid \<in>\<in> ?frds1.0 ?uid')

goal (1 subgoal):
 1. uid' \<in>\<in> friendIDs s1 uid
[PROOF STEP]
unfolding eqButUIDf_def
[PROOF STATE]
proof (prove)
using this:
uid' \<in>\<in> friendIDs s uid
eqButUIDl UID2 (friendIDs s UID1) (friendIDs s1 UID1) \<and> eqButUIDl UID1 (friendIDs s UID2) (friendIDs s1 UID2) \<and> (\<forall>uid. uid \<noteq> UID1 \<and> uid \<noteq> UID2 \<longrightarrow> friendIDs s uid = friendIDs s1 uid)
distinct (friendIDs s uid)
distinct (friendIDs s1 uid)
(UID1 \<in>\<in> friendIDs s UID2) = (UID1 \<in>\<in> friendIDs s1 UID2)
(UID2 \<in>\<in> friendIDs s UID1) = (UID2 \<in>\<in> friendIDs s1 UID1)
\<lbrakk>eqButUIDl UID2 (?frds UID1) (?frds1.0 UID1) \<and> eqButUIDl UID1 (?frds UID2) (?frds1.0 UID2) \<and> (\<forall>uid. uid \<noteq> UID1 \<and> uid \<noteq> UID2 \<longrightarrow> ?frds uid = ?frds1.0 uid); (?uid, ?uid') \<notin> {(UID1, UID2), (UID2, UID1)}\<rbrakk> \<Longrightarrow> (?uid \<in>\<in> ?frds ?uid') = (?uid \<in>\<in> ?frds1.0 ?uid')

goal (1 subgoal):
 1. uid' \<in>\<in> friendIDs s1 uid
[PROOF STEP]
by (metis (no_types, lifting) insert_iff prod.inject singletonD)
[PROOF STATE]
proof (state)
this:
uid' \<in>\<in> friendIDs s1 uid

goal (1 subgoal):
 1. \<And>x. x \<in>\<in> friendIDs s1 uid \<Longrightarrow> x \<in>\<in> friendIDs s uid
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<in> friendIDs s1 uid \<Longrightarrow> x \<in>\<in> friendIDs s uid
[PROOF STEP]
fix uid'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<in> friendIDs s1 uid \<Longrightarrow> x \<in>\<in> friendIDs s uid
[PROOF STEP]
assume "uid' \<in>\<in> friendIDs s1 uid"
[PROOF STATE]
proof (state)
this:
uid' \<in>\<in> friendIDs s1 uid

goal (1 subgoal):
 1. \<And>x. x \<in>\<in> friendIDs s1 uid \<Longrightarrow> x \<in>\<in> friendIDs s uid
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
uid' \<in>\<in> friendIDs s1 uid
[PROOF STEP]
show "uid' \<in>\<in> friendIDs s uid"
[PROOF STATE]
proof (prove)
using this:
uid' \<in>\<in> friendIDs s1 uid

goal (1 subgoal):
 1. uid' \<in>\<in> friendIDs s uid
[PROOF STEP]
using fIDs dfIDs uid12 eqButUIDf_not_UID'
[PROOF STATE]
proof (prove)
using this:
uid' \<in>\<in> friendIDs s1 uid
eqButUIDf (friendIDs s) (friendIDs s1)
distinct (friendIDs s uid)
distinct (friendIDs s1 uid)
(UID1 \<in>\<in> friendIDs s UID2) = (UID1 \<in>\<in> friendIDs s1 UID2)
(UID2 \<in>\<in> friendIDs s UID1) = (UID2 \<in>\<in> friendIDs s1 UID1)
\<lbrakk>eqButUIDf ?frds ?frds1.0; (?uid, ?uid') \<notin> {(UID1, UID2), (UID2, UID1)}\<rbrakk> \<Longrightarrow> (?uid \<in>\<in> ?frds ?uid') = (?uid \<in>\<in> ?frds1.0 ?uid')

goal (1 subgoal):
 1. uid' \<in>\<in> friendIDs s uid
[PROOF STEP]
unfolding eqButUIDf_def
[PROOF STATE]
proof (prove)
using this:
uid' \<in>\<in> friendIDs s1 uid
eqButUIDl UID2 (friendIDs s UID1) (friendIDs s1 UID1) \<and> eqButUIDl UID1 (friendIDs s UID2) (friendIDs s1 UID2) \<and> (\<forall>uid. uid \<noteq> UID1 \<and> uid \<noteq> UID2 \<longrightarrow> friendIDs s uid = friendIDs s1 uid)
distinct (friendIDs s uid)
distinct (friendIDs s1 uid)
(UID1 \<in>\<in> friendIDs s UID2) = (UID1 \<in>\<in> friendIDs s1 UID2)
(UID2 \<in>\<in> friendIDs s UID1) = (UID2 \<in>\<in> friendIDs s1 UID1)
\<lbrakk>eqButUIDl UID2 (?frds UID1) (?frds1.0 UID1) \<and> eqButUIDl UID1 (?frds UID2) (?frds1.0 UID2) \<and> (\<forall>uid. uid \<noteq> UID1 \<and> uid \<noteq> UID2 \<longrightarrow> ?frds uid = ?frds1.0 uid); (?uid, ?uid') \<notin> {(UID1, UID2), (UID2, UID1)}\<rbrakk> \<Longrightarrow> (?uid \<in>\<in> ?frds ?uid') = (?uid \<in>\<in> ?frds1.0 ?uid')

goal (1 subgoal):
 1. uid' \<in>\<in> friendIDs s uid
[PROOF STEP]
by (metis (no_types, lifting) insert_iff prod.inject singletonD)
[PROOF STATE]
proof (state)
this:
uid' \<in>\<in> friendIDs s uid

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
set (friendIDs s uid) = set (friendIDs s1 uid)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma distinct_remove1_idem: "distinct xs \<Longrightarrow> remove1 y (remove1 y xs) = remove1 y xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct xs \<Longrightarrow> remove1 y (remove1 y xs) = remove1 y xs
[PROOF STEP]
by (induction xs) (auto simp add: remove1_idem)


[STATEMENT]
lemma Cact_cFriend_step_eqButUID:
assumes step: "step s (Cact (cFriend uid p uid')) = (ou,s')"
and s: "reach s"
and uids: "(uid = UID1 \<and> uid' = UID2) \<or> (uid = UID2 \<and> uid' = UID1)" (is "?u12 \<or> ?u21")
shows "eqButUID s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqButUID s s'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
step s (Cact (cFriend uid p uid')) = (ou, s')
reach s
uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1

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

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

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

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

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

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

goal (1 subgoal):
 1. (uid' \<notin> set (friendIDs s uid) &&& uid \<notin> set (friendIDs s uid')) &&& distinct (pendingFReqs s uid) &&& distinct (pendingFReqs s uid')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
uid' \<notin> set (friendIDs s uid)
uid \<notin> set (friendIDs s uid')
distinct (pendingFReqs s uid)
distinct (pendingFReqs s uid')

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

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

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

goal (2 subgoals):
 1. \<lbrakk>step s (Cact (cFriend uid p uid')) = (ou, s'); reach s; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; ?P3\<rbrakk> \<Longrightarrow> eqButUID s s'
 2. \<lbrakk>step s (Cact (cFriend uid p uid')) = (ou, s'); reach s; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; \<not> ?P3\<rbrakk> \<Longrightarrow> eqButUID s s'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
eqButUIDf (friendIDs s) (friendIDs (createFriend s uid p uid'))

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

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

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

goal (2 subgoals):
 1. \<lbrakk>step s (Cact (cFriend uid p uid')) = (ou, s'); reach s; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; ?P3\<rbrakk> \<Longrightarrow> eqButUID s s'
 2. \<lbrakk>step s (Cact (cFriend uid p uid')) = (ou, s'); reach s; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; \<not> ?P3\<rbrakk> \<Longrightarrow> eqButUID s s'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
eqButUIDf (pendingFReqs s) (pendingFReqs (createFriend s uid p uid'))

goal (2 subgoals):
 1. \<lbrakk>step s (Cact (cFriend uid p uid')) = (ou, s'); reach s; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; ?P3\<rbrakk> \<Longrightarrow> eqButUID s s'
 2. \<lbrakk>step s (Cact (cFriend uid p uid')) = (ou, s'); reach s; uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; \<not> ?P3\<rbrakk> \<Longrightarrow> eqButUID s s'
[PROOF STEP]
have "eqButUID12 (friendReq s) (friendReq (createFriend s uid p uid'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqButUID12 (friendReq s) (friendReq (createFriend s uid p uid'))
[PROOF STEP]
using uids
[PROOF STATE]
proof (prove)
using this:
uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1

goal (1 subgoal):
 1. eqButUID12 (friendReq s) (friendReq (createFriend s uid p uid'))
[PROOF STEP]
unfolding eqButUID12_def
[PROOF STATE]
proof (prove)
using this:
uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1

goal (1 subgoal):
 1. \<forall>uida uid'a. if (uida, uid'a) \<in> {(UID1, UID2), (UID2, UID1)} then True else friendReq s uida uid'a = friendReq (createFriend s uid p uid') uida uid'a
[PROOF STEP]
by (auto simp add: c_defs fun_upd2_eq_but_a_b)
[PROOF STATE]
proof (state)
this:
eqButUID12 (friendReq s) (friendReq (createFriend s uid p uid'))

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

goal (1 subgoal):
 1. eqButUID s s'
[PROOF STEP]
using step ou
[PROOF STATE]
proof (prove)
using this:
eqButUIDf (friendIDs s) (friendIDs (createFriend s uid p uid'))
eqButUIDf (pendingFReqs s) (pendingFReqs (createFriend s uid p uid'))
eqButUID12 (friendReq s) (friendReq (createFriend s uid p uid'))
step s (Cact (cFriend uid p uid')) = (ou, s')
ou = outOK

goal (1 subgoal):
 1. eqButUID s s'
[PROOF STEP]
unfolding eqButUID_def
[PROOF STATE]
proof (prove)
using this:
eqButUIDf (friendIDs s) (friendIDs (createFriend s uid p uid'))
eqButUIDf (pendingFReqs s) (pendingFReqs (createFriend s uid p uid'))
eqButUID12 (friendReq s) (friendReq (createFriend s uid p uid'))
step s (Cact (cFriend uid p uid')) = (ou, s')
ou = outOK

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

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


[STATEMENT]
lemma Cact_cFriendReq_step_eqButUID:
assumes step: "step s (Cact (cFriendReq uid p uid' req)) = (ou,s')"
and uids: "(uid = UID1 \<and> uid' = UID2) \<or> (uid = UID2 \<and> uid' = UID1)" (is "?u12 \<or> ?u21")
shows "eqButUID s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqButUID s s'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
step s (Cact (cFriendReq uid p uid' req)) = (ou, s')
uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1

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

goal (2 subgoals):
 1. \<lbrakk>step s (Cact (cFriendReq uid p uid' req)) = (ou, s'); uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; ?P2\<rbrakk> \<Longrightarrow> eqButUID s s'
 2. \<lbrakk>step s (Cact (cFriendReq uid p uid' req)) = (ou, s'); uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; \<not> ?P2\<rbrakk> \<Longrightarrow> eqButUID s s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ou = outOK
[PROOF STEP]
have "uid \<notin> set (pendingFReqs s uid')" "uid \<notin> set (friendIDs s uid')"
[PROOF STATE]
proof (prove)
using this:
ou = outOK

goal (1 subgoal):
 1. uid \<notin> set (pendingFReqs s uid') &&& uid \<notin> set (friendIDs s uid')
[PROOF STEP]
using step
[PROOF STATE]
proof (prove)
using this:
ou = outOK
step s (Cact (cFriendReq uid p uid' req)) = (ou, s')

goal (1 subgoal):
 1. uid \<notin> set (pendingFReqs s uid') &&& uid \<notin> set (friendIDs s uid')
[PROOF STEP]
by (auto simp add: c_defs)
[PROOF STATE]
proof (state)
this:
uid \<notin> set (pendingFReqs s uid')
uid \<notin> set (friendIDs s uid')

goal (2 subgoals):
 1. \<lbrakk>step s (Cact (cFriendReq uid p uid' req)) = (ou, s'); uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; ?P2\<rbrakk> \<Longrightarrow> eqButUID s s'
 2. \<lbrakk>step s (Cact (cFriendReq uid p uid' req)) = (ou, s'); uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; \<not> ?P2\<rbrakk> \<Longrightarrow> eqButUID s s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
uid \<notin> set (pendingFReqs s uid')
uid \<notin> set (friendIDs s uid')
[PROOF STEP]
have "eqButUIDf (pendingFReqs s) (pendingFReqs (createFriendReq s uid p uid' req))"
[PROOF STATE]
proof (prove)
using this:
uid \<notin> set (pendingFReqs s uid')
uid \<notin> set (friendIDs s uid')

goal (1 subgoal):
 1. eqButUIDf (pendingFReqs s) (pendingFReqs (createFriendReq s uid p uid' req))
[PROOF STEP]
using uids UID1_UID2
[PROOF STATE]
proof (prove)
using this:
uid \<notin> set (pendingFReqs s uid')
uid \<notin> set (friendIDs s uid')
uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1
UID1 \<noteq> UID2

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

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

goal (2 subgoals):
 1. \<lbrakk>step s (Cact (cFriendReq uid p uid' req)) = (ou, s'); uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; ?P2\<rbrakk> \<Longrightarrow> eqButUID s s'
 2. \<lbrakk>step s (Cact (cFriendReq uid p uid' req)) = (ou, s'); uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; \<not> ?P2\<rbrakk> \<Longrightarrow> eqButUID s s'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
eqButUIDf (pendingFReqs s) (pendingFReqs (createFriendReq s uid p uid' req))

goal (2 subgoals):
 1. \<lbrakk>step s (Cact (cFriendReq uid p uid' req)) = (ou, s'); uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; ?P2\<rbrakk> \<Longrightarrow> eqButUID s s'
 2. \<lbrakk>step s (Cact (cFriendReq uid p uid' req)) = (ou, s'); uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; \<not> ?P2\<rbrakk> \<Longrightarrow> eqButUID s s'
[PROOF STEP]
have "eqButUID12 (friendReq s) (friendReq (createFriendReq s uid p uid' req))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqButUID12 (friendReq s) (friendReq (createFriendReq s uid p uid' req))
[PROOF STEP]
using uids
[PROOF STATE]
proof (prove)
using this:
uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1

goal (1 subgoal):
 1. eqButUID12 (friendReq s) (friendReq (createFriendReq s uid p uid' req))
[PROOF STEP]
unfolding eqButUID12_def
[PROOF STATE]
proof (prove)
using this:
uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1

goal (1 subgoal):
 1. \<forall>uida uid'a. if (uida, uid'a) \<in> {(UID1, UID2), (UID2, UID1)} then True else friendReq s uida uid'a = friendReq (createFriendReq s uid p uid' req) uida uid'a
[PROOF STEP]
by (auto simp add: c_defs fun_upd2_eq_but_a_b)
[PROOF STATE]
proof (state)
this:
eqButUID12 (friendReq s) (friendReq (createFriendReq s uid p uid' req))

goal (2 subgoals):
 1. \<lbrakk>step s (Cact (cFriendReq uid p uid' req)) = (ou, s'); uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; ?P2\<rbrakk> \<Longrightarrow> eqButUID s s'
 2. \<lbrakk>step s (Cact (cFriendReq uid p uid' req)) = (ou, s'); uid = UID1 \<and> uid' = UID2 \<or> uid = UID2 \<and> uid' = UID1; \<not> ?P2\<rbrakk> \<Longrightarrow> eqButUID s s'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
eqButUIDf (pendingFReqs s) (pendingFReqs (createFriendReq s uid p uid' req))
eqButUID12 (friendReq s) (friendReq (createFriendReq s uid p uid' req))
[PROOF STEP]
show "eqButUID s s'"
[PROOF STATE]
proof (prove)
using this:
eqButUIDf (pendingFReqs s) (pendingFReqs (createFriendReq s uid p uid' req))
eqButUID12 (friendReq s) (friendReq (createFriendReq s uid p uid' req))

goal (1 subgoal):
 1. eqButUID s s'
[PROOF STEP]
using step ou
[PROOF STATE]
proof (prove)
using this:
eqButUIDf (pendingFReqs s) (pendingFReqs (createFriendReq s uid p uid' req))
eqButUID12 (friendReq s) (friendReq (createFriendReq s uid p uid' req))
step s (Cact (cFriendReq uid p uid' req)) = (ou, s')
ou = outOK

goal (1 subgoal):
 1. eqButUID s s'
[PROOF STEP]
unfolding eqButUID_def
[PROOF STATE]
proof (prove)
using this:
eqButUIDf (pendingFReqs s) (pendingFReqs (createFriendReq s uid p uid' req))
eqButUID12 (friendReq s) (friendReq (createFriendReq s uid p uid' req))
step s (Cact (cFriendReq uid p uid' req)) = (ou, s')
ou = outOK

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

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