[STATEMENT]
lemma step_friendIDs:
assumes "step s a = (ou, s')"
and "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)"
shows "uid \<in>\<in> friendIDs s' uid' \<longleftrightarrow> uid \<in>\<in> friendIDs s uid'" (is ?uid)
  and "uid' \<in>\<in> friendIDs s' uid \<longleftrightarrow> uid' \<in>\<in> friendIDs s uid" (is ?uid')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') &&& (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs s uid)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid')
 2. (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs s uid)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
step s a = (ou, s')
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)
[PROOF STEP]
have "?uid \<and> ?uid'"
[PROOF STATE]
proof (prove)
using this:
step s a = (ou, s')
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)

goal (1 subgoal):
 1. (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs s uid)
[PROOF STEP]
proof (cases a)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>x1. \<lbrakk>step s a = (ou, s'); 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); a = Sact x1\<rbrakk> \<Longrightarrow> (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs s uid)
 2. \<And>x2. \<lbrakk>step s a = (ou, s'); 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); a = Cact x2\<rbrakk> \<Longrightarrow> (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs s uid)
 3. \<And>x3. \<lbrakk>step s a = (ou, s'); 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); a = Dact x3\<rbrakk> \<Longrightarrow> (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs s uid)
 4. \<And>x4. \<lbrakk>step s a = (ou, s'); 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); a = Uact x4\<rbrakk> \<Longrightarrow> (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs s uid)
 5. \<And>x5. \<lbrakk>step s a = (ou, s'); 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); a = Ract x5\<rbrakk> \<Longrightarrow> (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs s uid)
 6. \<And>x6. \<lbrakk>step s a = (ou, s'); 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); a = Lact x6\<rbrakk> \<Longrightarrow> (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs s uid)
 7. \<And>x7. \<lbrakk>step s a = (ou, s'); 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); a = COMact x7\<rbrakk> \<Longrightarrow> (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs 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'); 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); a = Sact x1\<rbrakk> \<Longrightarrow> (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs s uid)
 2. \<And>x2. \<lbrakk>step s a = (ou, s'); 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); a = Cact x2\<rbrakk> \<Longrightarrow> (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs s uid)
 3. \<And>x3. \<lbrakk>step s a = (ou, s'); 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); a = Dact x3\<rbrakk> \<Longrightarrow> (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs s uid)
 4. \<And>x4. \<lbrakk>step s a = (ou, s'); 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); a = Uact x4\<rbrakk> \<Longrightarrow> (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs s uid)
 5. \<And>x5. \<lbrakk>step s a = (ou, s'); 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); a = Ract x5\<rbrakk> \<Longrightarrow> (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs s uid)
 6. \<And>x6. \<lbrakk>step s a = (ou, s'); 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); a = Lact x6\<rbrakk> \<Longrightarrow> (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs s uid)
 7. \<And>x7. \<lbrakk>step s a = (ou, s'); 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); a = COMact x7\<rbrakk> \<Longrightarrow> (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs 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> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs s uid)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a = Sact sa
step s a = (ou, s')
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)

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

goal (6 subgoals):
 1. \<And>x2. \<lbrakk>step s a = (ou, s'); 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); a = Cact x2\<rbrakk> \<Longrightarrow> (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs s uid)
 2. \<And>x3. \<lbrakk>step s a = (ou, s'); 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); a = Dact x3\<rbrakk> \<Longrightarrow> (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs s uid)
 3. \<And>x4. \<lbrakk>step s a = (ou, s'); 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); a = Uact x4\<rbrakk> \<Longrightarrow> (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs s uid)
 4. \<And>x5. \<lbrakk>step s a = (ou, s'); 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); a = Ract x5\<rbrakk> \<Longrightarrow> (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs s uid)
 5. \<And>x6. \<lbrakk>step s a = (ou, s'); 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); a = Lact x6\<rbrakk> \<Longrightarrow> (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs s uid)
 6. \<And>x7. \<lbrakk>step s a = (ou, s'); 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); a = COMact x7\<rbrakk> \<Longrightarrow> (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs s uid)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>x2. \<lbrakk>step s a = (ou, s'); 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); a = Cact x2\<rbrakk> \<Longrightarrow> (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs s uid)
 2. \<And>x3. \<lbrakk>step s a = (ou, s'); 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); a = Dact x3\<rbrakk> \<Longrightarrow> (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs s uid)
 3. \<And>x4. \<lbrakk>step s a = (ou, s'); 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); a = Uact x4\<rbrakk> \<Longrightarrow> (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs s uid)
 4. \<And>x5. \<lbrakk>step s a = (ou, s'); 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); a = Ract x5\<rbrakk> \<Longrightarrow> (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs s uid)
 5. \<And>x6. \<lbrakk>step s a = (ou, s'); 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); a = Lact x6\<rbrakk> \<Longrightarrow> (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs s uid)
 6. \<And>x7. \<lbrakk>step s a = (ou, s'); 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); a = COMact x7\<rbrakk> \<Longrightarrow> (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs 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'); 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); a = Cact x2\<rbrakk> \<Longrightarrow> (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs s uid)
 2. \<And>x3. \<lbrakk>step s a = (ou, s'); 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); a = Dact x3\<rbrakk> \<Longrightarrow> (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs s uid)
 3. \<And>x4. \<lbrakk>step s a = (ou, s'); 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); a = Uact x4\<rbrakk> \<Longrightarrow> (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs s uid)
 4. \<And>x5. \<lbrakk>step s a = (ou, s'); 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); a = Ract x5\<rbrakk> \<Longrightarrow> (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs s uid)
 5. \<And>x6. \<lbrakk>step s a = (ou, s'); 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); a = Lact x6\<rbrakk> \<Longrightarrow> (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs s uid)
 6. \<And>x7. \<lbrakk>step s a = (ou, s'); 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); a = COMact x7\<rbrakk> \<Longrightarrow> (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs 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> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs s uid)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a = Uact ua
step s a = (ou, s')
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)

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

goal (5 subgoals):
 1. \<And>x2. \<lbrakk>step s a = (ou, s'); 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); a = Cact x2\<rbrakk> \<Longrightarrow> (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs s uid)
 2. \<And>x3. \<lbrakk>step s a = (ou, s'); 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); a = Dact x3\<rbrakk> \<Longrightarrow> (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs s uid)
 3. \<And>x5. \<lbrakk>step s a = (ou, s'); 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); a = Ract x5\<rbrakk> \<Longrightarrow> (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs s uid)
 4. \<And>x6. \<lbrakk>step s a = (ou, s'); 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); a = Lact x6\<rbrakk> \<Longrightarrow> (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs s uid)
 5. \<And>x7. \<lbrakk>step s a = (ou, s'); 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); a = COMact x7\<rbrakk> \<Longrightarrow> (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs s uid)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>x2. \<lbrakk>step s a = (ou, s'); 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); a = Cact x2\<rbrakk> \<Longrightarrow> (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs s uid)
 2. \<And>x3. \<lbrakk>step s a = (ou, s'); 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); a = Dact x3\<rbrakk> \<Longrightarrow> (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs s uid)
 3. \<And>x5. \<lbrakk>step s a = (ou, s'); 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); a = Ract x5\<rbrakk> \<Longrightarrow> (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs s uid)
 4. \<And>x6. \<lbrakk>step s a = (ou, s'); 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); a = Lact x6\<rbrakk> \<Longrightarrow> (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs s uid)
 5. \<And>x7. \<lbrakk>step s a = (ou, s'); 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); a = COMact x7\<rbrakk> \<Longrightarrow> (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs 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'); 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); a = Cact x2\<rbrakk> \<Longrightarrow> (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs s uid)
 2. \<And>x3. \<lbrakk>step s a = (ou, s'); 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); a = Dact x3\<rbrakk> \<Longrightarrow> (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs s uid)
 3. \<And>x5. \<lbrakk>step s a = (ou, s'); 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); a = Ract x5\<rbrakk> \<Longrightarrow> (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs s uid)
 4. \<And>x6. \<lbrakk>step s a = (ou, s'); 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); a = Lact x6\<rbrakk> \<Longrightarrow> (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs s uid)
 5. \<And>x7. \<lbrakk>step s a = (ou, s'); 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); a = COMact x7\<rbrakk> \<Longrightarrow> (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs 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> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs s uid)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a = COMact ca
step s a = (ou, s')
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)

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

goal (4 subgoals):
 1. \<And>x2. \<lbrakk>step s a = (ou, s'); 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); a = Cact x2\<rbrakk> \<Longrightarrow> (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs s uid)
 2. \<And>x3. \<lbrakk>step s a = (ou, s'); 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); a = Dact x3\<rbrakk> \<Longrightarrow> (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs s uid)
 3. \<And>x5. \<lbrakk>step s a = (ou, s'); 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); a = Ract x5\<rbrakk> \<Longrightarrow> (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs s uid)
 4. \<And>x6. \<lbrakk>step s a = (ou, s'); 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); a = Lact x6\<rbrakk> \<Longrightarrow> (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs s uid)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x2. \<lbrakk>step s a = (ou, s'); 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); a = Cact x2\<rbrakk> \<Longrightarrow> (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs s uid)
 2. \<And>x3. \<lbrakk>step s a = (ou, s'); 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); a = Dact x3\<rbrakk> \<Longrightarrow> (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs s uid)
 3. \<And>x5. \<lbrakk>step s a = (ou, s'); 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); a = Ract x5\<rbrakk> \<Longrightarrow> (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs s uid)
 4. \<And>x6. \<lbrakk>step s a = (ou, s'); 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); a = Lact x6\<rbrakk> \<Longrightarrow> (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs 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'); 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); a = Cact x2\<rbrakk> \<Longrightarrow> (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs s uid)
 2. \<And>x3. \<lbrakk>step s a = (ou, s'); 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); a = Dact x3\<rbrakk> \<Longrightarrow> (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs s uid)
 3. \<And>x5. \<lbrakk>step s a = (ou, s'); 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); a = Ract x5\<rbrakk> \<Longrightarrow> (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs s uid)
 4. \<And>x6. \<lbrakk>step s a = (ou, s'); 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); a = Lact x6\<rbrakk> \<Longrightarrow> (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs 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> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs s uid)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a = Cact ca
step s a = (ou, s')
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)

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

goal (3 subgoals):
 1. \<And>x3. \<lbrakk>step s a = (ou, s'); 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); a = Dact x3\<rbrakk> \<Longrightarrow> (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs s uid)
 2. \<And>x5. \<lbrakk>step s a = (ou, s'); 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); a = Ract x5\<rbrakk> \<Longrightarrow> (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs s uid)
 3. \<And>x6. \<lbrakk>step s a = (ou, s'); 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); a = Lact x6\<rbrakk> \<Longrightarrow> (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs s uid)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x3. \<lbrakk>step s a = (ou, s'); 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); a = Dact x3\<rbrakk> \<Longrightarrow> (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs s uid)
 2. \<And>x5. \<lbrakk>step s a = (ou, s'); 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); a = Ract x5\<rbrakk> \<Longrightarrow> (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs s uid)
 3. \<And>x6. \<lbrakk>step s a = (ou, s'); 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); a = Lact x6\<rbrakk> \<Longrightarrow> (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs 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'); 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); a = Dact x3\<rbrakk> \<Longrightarrow> (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs s uid)
 2. \<And>x5. \<lbrakk>step s a = (ou, s'); 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); a = Ract x5\<rbrakk> \<Longrightarrow> (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs s uid)
 3. \<And>x6. \<lbrakk>step s a = (ou, s'); 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); a = Lact x6\<rbrakk> \<Longrightarrow> (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs 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> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs s uid)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a = Dact da
step s a = (ou, s')
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)

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

goal (2 subgoals):
 1. \<And>x5. \<lbrakk>step s a = (ou, s'); 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); a = Ract x5\<rbrakk> \<Longrightarrow> (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs s uid)
 2. \<And>x6. \<lbrakk>step s a = (ou, s'); 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); a = Lact x6\<rbrakk> \<Longrightarrow> (uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs s uid)
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
(uid \<in>\<in> friendIDs s' uid') = (uid \<in>\<in> friendIDs s uid') \<and> (uid' \<in>\<in> friendIDs s' uid) = (uid' \<in>\<in> friendIDs s uid)

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma step_friends12:
assumes "step s a = (ou, s')"
and "a \<noteq> Cact (cFriend UID1 (pass s UID1) UID2) \<and> a \<noteq> Cact (cFriend UID2 (pass s UID2) UID1) \<and>
     a \<noteq> Dact (dFriend UID1 (pass s UID1) UID2) \<and> a \<noteq> Dact (dFriend UID2 (pass s UID2) UID1)"
shows "friends12 s' \<longleftrightarrow> friends12 s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. friends12 s' = friends12 s
[PROOF STEP]
using step_friendIDs[OF assms]
[PROOF STATE]
proof (prove)
using this:
(UID1 \<in>\<in> friendIDs s' UID2) = (UID1 \<in>\<in> friendIDs s UID2)
(UID2 \<in>\<in> friendIDs s' UID1) = (UID2 \<in>\<in> friendIDs s UID1)

goal (1 subgoal):
 1. friends12 s' = friends12 s
[PROOF STEP]
unfolding friends12_def
[PROOF STATE]
proof (prove)
using this:
(UID1 \<in>\<in> friendIDs s' UID2) = (UID1 \<in>\<in> friendIDs s UID2)
(UID2 \<in>\<in> friendIDs s' UID1) = (UID2 \<in>\<in> friendIDs s UID1)

goal (1 subgoal):
 1. (UID1 \<in>\<in> friendIDs s' UID2 \<and> UID2 \<in>\<in> friendIDs s' UID1) = (UID1 \<in>\<in> friendIDs s UID2 \<and> UID2 \<in>\<in> friendIDs s UID1)
[PROOF STEP]
by auto