[STATEMENT]
lemma eqButUID_step_friendIDs_eq:
assumes ss1: "eqButUID s s1"
and rs: "reach s" and rs1: "reach s1"
and step: "step s a = (ou,s')" and step1: "step s1 a = (ou1,s1')"
and a: "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)"
and "friendIDs s = friendIDs s1"
shows "friendIDs s' = friendIDs s1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. friendIDs s' = friendIDs s1'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
eqButUID s s1
reach s
reach s1
step s a = (ou, s')
step s1 a = (ou1, s1')
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)
friendIDs s = friendIDs s1

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

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

goal (1 subgoal):
 1. friendIDs s' = friendIDs s1'
[PROOF STEP]
by (cases sa) (auto simp: s_defs)
[PROOF STATE]
proof (state)
this:
friendIDs s' = friendIDs s1'

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

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

goal (1 subgoal):
 1. friendIDs s' = friendIDs s1'
[PROOF STEP]
by (cases ua) (auto simp: u_defs)
[PROOF STATE]
proof (state)
this:
friendIDs s' = friendIDs s1'

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

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

goal (1 subgoal):
 1. friendIDs s' = friendIDs s1'
[PROOF STEP]
by (cases ca) (auto simp: com_defs)
[PROOF STATE]
proof (state)
this:
friendIDs s' = friendIDs s1'

goal (4 subgoals):
 1. \<And>x2. \<lbrakk>eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); 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); friendIDs s = friendIDs s1; a = Cact x2\<rbrakk> \<Longrightarrow> friendIDs s' = friendIDs s1'
 2. \<And>x3. \<lbrakk>eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); 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); friendIDs s = friendIDs s1; a = Dact x3\<rbrakk> \<Longrightarrow> friendIDs s' = friendIDs s1'
 3. \<And>x5. \<lbrakk>eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); 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); friendIDs s = friendIDs s1; a = Ract x5\<rbrakk> \<Longrightarrow> friendIDs s' = friendIDs s1'
 4. \<And>x6. \<lbrakk>eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); 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); friendIDs s = friendIDs s1; a = Lact x6\<rbrakk> \<Longrightarrow> friendIDs s' = friendIDs s1'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x2. \<lbrakk>eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); 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); friendIDs s = friendIDs s1; a = Cact x2\<rbrakk> \<Longrightarrow> friendIDs s' = friendIDs s1'
 2. \<And>x3. \<lbrakk>eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); 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); friendIDs s = friendIDs s1; a = Dact x3\<rbrakk> \<Longrightarrow> friendIDs s' = friendIDs s1'
 3. \<And>x5. \<lbrakk>eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); 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); friendIDs s = friendIDs s1; a = Ract x5\<rbrakk> \<Longrightarrow> friendIDs s' = friendIDs s1'
 4. \<And>x6. \<lbrakk>eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); 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); friendIDs s = friendIDs s1; a = Lact x6\<rbrakk> \<Longrightarrow> friendIDs s' = friendIDs s1'
[PROOF STEP]
case (Dact da)
[PROOF STATE]
proof (state)
this:
a = Dact da

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

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

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

goal (1 subgoal):
 1. friendIDs s' = friendIDs s1'
[PROOF STEP]
by (cases "(uid,uid') \<in> {(UID1,UID2), (UID2,UID1)}")
           (auto simp: d_defs eqButUID_stateSelectors eqButUIDf_not_UID')
[PROOF STATE]
proof (state)
this:
friendIDs s' = friendIDs s1'

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

goal (3 subgoals):
 1. \<And>x2. \<lbrakk>eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); 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); friendIDs s = friendIDs s1; a = Cact x2\<rbrakk> \<Longrightarrow> friendIDs s' = friendIDs s1'
 2. \<And>x5. \<lbrakk>eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); 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); friendIDs s = friendIDs s1; a = Ract x5\<rbrakk> \<Longrightarrow> friendIDs s' = friendIDs s1'
 3. \<And>x6. \<lbrakk>eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); 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); friendIDs s = friendIDs s1; a = Lact x6\<rbrakk> \<Longrightarrow> friendIDs s' = friendIDs s1'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x2. \<lbrakk>eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); 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); friendIDs s = friendIDs s1; a = Cact x2\<rbrakk> \<Longrightarrow> friendIDs s' = friendIDs s1'
 2. \<And>x5. \<lbrakk>eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); 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); friendIDs s = friendIDs s1; a = Ract x5\<rbrakk> \<Longrightarrow> friendIDs s' = friendIDs s1'
 3. \<And>x6. \<lbrakk>eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); 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); friendIDs s = friendIDs s1; a = Lact x6\<rbrakk> \<Longrightarrow> friendIDs s' = friendIDs s1'
[PROOF STEP]
case (Cact ca)
[PROOF STATE]
proof (state)
this:
a = Cact ca

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

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

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

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

goal (5 subgoals):
 1. \<And>x11 x12. \<lbrakk>a = Cact ca; eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); 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); friendIDs s = friendIDs s1; ca = cNUReq x11 x12\<rbrakk> \<Longrightarrow> friendIDs s' = friendIDs s1'
 2. \<And>x21 x22 x23 x24. \<lbrakk>a = Cact ca; eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); 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); friendIDs s = friendIDs s1; ca = cUser x21 x22 x23 x24\<rbrakk> \<Longrightarrow> friendIDs s' = friendIDs s1'
 3. \<And>x31 x32 x33. \<lbrakk>a = Cact ca; eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); 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); friendIDs s = friendIDs s1; ca = cPost x31 x32 x33\<rbrakk> \<Longrightarrow> friendIDs s' = friendIDs s1'
 4. \<And>x41 x42 x43 x44. \<lbrakk>a = Cact ca; eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); 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); friendIDs s = friendIDs s1; ca = cFriendReq x41 x42 x43 x44\<rbrakk> \<Longrightarrow> friendIDs s' = friendIDs s1'
 5. \<And>x51 x52 x53. \<lbrakk>a = Cact ca; eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); 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); friendIDs s = friendIDs s1; ca = cFriend x51 x52 x53\<rbrakk> \<Longrightarrow> friendIDs s' = friendIDs s1'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p = pass s uid
[PROOF STEP]
have "uid' \<in>\<in> pendingFReqs s uid \<longleftrightarrow> uid' \<in>\<in> pendingFReqs s1 uid"
[PROOF STATE]
proof (prove)
using this:
p = pass s uid

goal (1 subgoal):
 1. (uid' \<in>\<in> pendingFReqs s uid) = (uid' \<in>\<in> pendingFReqs s1 uid)
[PROOF STEP]
using Cact cFriend ss1 a
[PROOF STATE]
proof (prove)
using this:
p = pass s uid
a = Cact ca
ca = cFriend uid p uid'
eqButUID s s1
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)

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

goal (5 subgoals):
 1. \<And>x11 x12. \<lbrakk>a = Cact ca; eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); 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); friendIDs s = friendIDs s1; ca = cNUReq x11 x12\<rbrakk> \<Longrightarrow> friendIDs s' = friendIDs s1'
 2. \<And>x21 x22 x23 x24. \<lbrakk>a = Cact ca; eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); 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); friendIDs s = friendIDs s1; ca = cUser x21 x22 x23 x24\<rbrakk> \<Longrightarrow> friendIDs s' = friendIDs s1'
 3. \<And>x31 x32 x33. \<lbrakk>a = Cact ca; eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); 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); friendIDs s = friendIDs s1; ca = cPost x31 x32 x33\<rbrakk> \<Longrightarrow> friendIDs s' = friendIDs s1'
 4. \<And>x41 x42 x43 x44. \<lbrakk>a = Cact ca; eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); 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); friendIDs s = friendIDs s1; ca = cFriendReq x41 x42 x43 x44\<rbrakk> \<Longrightarrow> friendIDs s' = friendIDs s1'
 5. \<And>x51 x52 x53. \<lbrakk>a = Cact ca; eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); 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); friendIDs s = friendIDs s1; ca = cFriend x51 x52 x53\<rbrakk> \<Longrightarrow> friendIDs s' = friendIDs s1'
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
p = pass s uid \<Longrightarrow> (uid' \<in>\<in> pendingFReqs s uid) = (uid' \<in>\<in> pendingFReqs s1 uid)

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

goal (1 subgoal):
 1. friendIDs s' = friendIDs s1'
[PROOF STEP]
by (auto simp: c_defs eqButUID_stateSelectors)
[PROOF STATE]
proof (state)
this:
friendIDs s' = friendIDs s1'

goal (4 subgoals):
 1. \<And>x11 x12. \<lbrakk>a = Cact ca; eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); 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); friendIDs s = friendIDs s1; ca = cNUReq x11 x12\<rbrakk> \<Longrightarrow> friendIDs s' = friendIDs s1'
 2. \<And>x21 x22 x23 x24. \<lbrakk>a = Cact ca; eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); 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); friendIDs s = friendIDs s1; ca = cUser x21 x22 x23 x24\<rbrakk> \<Longrightarrow> friendIDs s' = friendIDs s1'
 3. \<And>x31 x32 x33. \<lbrakk>a = Cact ca; eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); 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); friendIDs s = friendIDs s1; ca = cPost x31 x32 x33\<rbrakk> \<Longrightarrow> friendIDs s' = friendIDs s1'
 4. \<And>x41 x42 x43 x44. \<lbrakk>a = Cact ca; eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); 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); friendIDs s = friendIDs s1; ca = cFriendReq x41 x42 x43 x44\<rbrakk> \<Longrightarrow> friendIDs s' = friendIDs s1'
[PROOF STEP]
qed (auto simp: c_defs)
[PROOF STATE]
proof (state)
this:
friendIDs s' = friendIDs s1'

goal (2 subgoals):
 1. \<And>x5. \<lbrakk>eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); 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); friendIDs s = friendIDs s1; a = Ract x5\<rbrakk> \<Longrightarrow> friendIDs s' = friendIDs s1'
 2. \<And>x6. \<lbrakk>eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); 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); friendIDs s = friendIDs s1; a = Lact x6\<rbrakk> \<Longrightarrow> friendIDs s' = friendIDs s1'
[PROOF STEP]
qed auto


[STATEMENT]
lemma createFriend_sym: "createFriend s uid p uid' = createFriend s uid' p' uid"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. createFriend s uid p uid' = createFriend s uid' p' uid
[PROOF STEP]
unfolding c_defs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (let fr = friendIDs s; pfr = pendingFReqs s in s\<lparr>friendIDs := fr(uid := fr uid ## uid', uid' := fr uid' ## uid), pendingFReqs := pfr(uid := remove1 uid' (pfr uid), uid' := remove1 uid (pfr uid')), friendReq := fun_upd2 (fun_upd2 (friendReq s) uid' uid emptyRequestInfo) uid uid' emptyRequestInfo\<rparr>) = (let fr = friendIDs s; pfr = pendingFReqs s in s\<lparr>friendIDs := fr(uid' := fr uid' ## uid, uid := fr uid ## uid'), pendingFReqs := pfr(uid' := remove1 uid (pfr uid'), uid := remove1 uid' (pfr uid)), friendReq := fun_upd2 (fun_upd2 (friendReq s) uid uid' emptyRequestInfo) uid' uid emptyRequestInfo\<rparr>)
[PROOF STEP]
by (cases "uid = uid'") (auto simp: fun_upd2_comm fun_upd_twist)


[STATEMENT]
lemma deleteFriend_sym: "deleteFriend s uid p uid' = deleteFriend s uid' p' uid"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deleteFriend s uid p uid' = deleteFriend s uid' p' uid
[PROOF STEP]
unfolding d_defs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (let fr = friendIDs s in s\<lparr>friendIDs := fr(uid := removeAll uid' (fr uid), uid' := removeAll uid (fr uid'))\<rparr>) = (let fr = friendIDs s in s\<lparr>friendIDs := fr(uid' := removeAll uid (fr uid'), uid := removeAll uid' (fr uid))\<rparr>)
[PROOF STEP]
by (cases "uid = uid'") (auto simp: fun_upd_twist)


[STATEMENT]
lemma createFriendReq_createFriend_absorb:
assumes "e_createFriendReq s uid' p uid req"
shows "createFriend (createFriendReq s uid' p1 uid req) uid p2 uid' = createFriend s uid p3 uid'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. createFriend (createFriendReq s uid' p1 uid req) uid p2 uid' = createFriend s uid p3 uid'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
e_createFriendReq s uid' p uid req

goal (1 subgoal):
 1. createFriend (createFriendReq s uid' p1 uid req) uid p2 uid' = createFriend s uid p3 uid'
[PROOF STEP]
unfolding c_defs
[PROOF STATE]
proof (prove)
using this:
IDsOK s [uid', uid] [] [] [] \<and> pass s uid' = p \<and> uid' \<notin> set (pendingFReqs s uid) \<and> uid' \<notin> set (friendIDs s uid)

goal (1 subgoal):
 1. (let fr = friendIDs (let pfr = pendingFReqs s in s\<lparr>pendingFReqs := pfr(uid := pfr uid ## uid'), friendReq := fun_upd2 (friendReq s) uid' uid req\<rparr>); pfr = pendingFReqs (let pfr = pendingFReqs s in s\<lparr>pendingFReqs := pfr(uid := pfr uid ## uid'), friendReq := fun_upd2 (friendReq s) uid' uid req\<rparr>) in (let pfr = pendingFReqs s in s\<lparr>pendingFReqs := pfr(uid := pfr uid ## uid'), friendReq := fun_upd2 (friendReq s) uid' uid req\<rparr>)\<lparr>friendIDs := fr(uid := fr uid ## uid', uid' := fr uid' ## uid), pendingFReqs := pfr(uid := remove1 uid' (pfr uid), uid' := remove1 uid (pfr uid')), friendReq := fun_upd2 (fun_upd2 (friendReq (let pfr = pendingFReqs s in s\<lparr>pendingFReqs := pfr(uid := pfr uid ## uid'), friendReq := fun_upd2 (friendReq s) uid' uid req\<rparr>)) uid' uid emptyRequestInfo) uid uid' emptyRequestInfo\<rparr>) = (let fr = friendIDs s; pfr = pendingFReqs s in s\<lparr>friendIDs := fr(uid := fr uid ## uid', uid' := fr uid' ## uid), pendingFReqs := pfr(uid := remove1 uid' (pfr uid), uid' := remove1 uid (pfr uid')), friendReq := fun_upd2 (fun_upd2 (friendReq s) uid' uid emptyRequestInfo) uid uid' emptyRequestInfo\<rparr>)
[PROOF STEP]
by (auto simp: remove1_idem remove1_append fun_upd2_absorb)


[STATEMENT]
lemma eqButUID_deleteFriend12_friendIDs_eq:
assumes ss1: "eqButUID s s1"
and rs: "reach s" and rs1: "reach s1"
shows "friendIDs (deleteFriend s UID1 p UID2) = friendIDs (deleteFriend s1 UID1 p' UID2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. friendIDs (deleteFriend s UID1 p UID2) = friendIDs (deleteFriend s1 UID1 p' UID2)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. friendIDs (deleteFriend s UID1 p UID2) = friendIDs (deleteFriend s1 UID1 p' UID2)
[PROOF STEP]
have "distinct (friendIDs s UID1)" "distinct (friendIDs s UID2)"
       "distinct (friendIDs s1 UID1)" "distinct (friendIDs s1 UID2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (distinct (friendIDs s UID1) &&& distinct (friendIDs s UID2)) &&& distinct (friendIDs s1 UID1) &&& distinct (friendIDs s1 UID2)
[PROOF STEP]
using rs rs1
[PROOF STATE]
proof (prove)
using this:
reach s
reach s1

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

goal (1 subgoal):
 1. friendIDs (deleteFriend s UID1 p UID2) = friendIDs (deleteFriend s1 UID1 p' UID2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
distinct (friendIDs s UID1)
distinct (friendIDs s UID2)
distinct (friendIDs s1 UID1)
distinct (friendIDs s1 UID2)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
distinct (friendIDs s UID1)
distinct (friendIDs s UID2)
distinct (friendIDs s1 UID1)
distinct (friendIDs s1 UID2)

goal (1 subgoal):
 1. friendIDs (deleteFriend s UID1 p UID2) = friendIDs (deleteFriend s1 UID1 p' UID2)
[PROOF STEP]
using ss1
[PROOF STATE]
proof (prove)
using this:
distinct (friendIDs s UID1)
distinct (friendIDs s UID2)
distinct (friendIDs s1 UID1)
distinct (friendIDs s1 UID2)
eqButUID s s1

goal (1 subgoal):
 1. friendIDs (deleteFriend s UID1 p UID2) = friendIDs (deleteFriend s1 UID1 p' UID2)
[PROOF STEP]
unfolding eqButUID_def eqButUIDf_def
[PROOF STATE]
proof (prove)
using this:
distinct (friendIDs s UID1)
distinct (friendIDs s UID2)
distinct (friendIDs s1 UID1)
distinct (friendIDs s1 UID2)
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> (eqButUIDl UID2 (pendingFReqs s UID1) (pendingFReqs s1 UID1) \<and> eqButUIDl UID1 (pendingFReqs s UID2) (pendingFReqs s1 UID2) \<and> (\<forall>uid. uid \<noteq> UID1 \<and> uid \<noteq> UID2 \<longrightarrow> pendingFReqs s uid = pendingFReqs s1 uid)) \<and> eqButUID12 (friendReq s) (friendReq s1) \<and> (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)) \<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. friendIDs (deleteFriend s UID1 p UID2) = friendIDs (deleteFriend s1 UID1 p' UID2)
[PROOF STEP]
unfolding d_defs
[PROOF STATE]
proof (prove)
using this:
distinct (friendIDs s UID1)
distinct (friendIDs s UID2)
distinct (friendIDs s1 UID1)
distinct (friendIDs s1 UID2)
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> (eqButUIDl UID2 (pendingFReqs s UID1) (pendingFReqs s1 UID1) \<and> eqButUIDl UID1 (pendingFReqs s UID2) (pendingFReqs s1 UID2) \<and> (\<forall>uid. uid \<noteq> UID1 \<and> uid \<noteq> UID2 \<longrightarrow> pendingFReqs s uid = pendingFReqs s1 uid)) \<and> eqButUID12 (friendReq s) (friendReq s1) \<and> (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)) \<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. friendIDs (let fr = friendIDs s in s\<lparr>friendIDs := fr(UID1 := removeAll UID2 (fr UID1), UID2 := removeAll UID1 (fr UID2))\<rparr>) = friendIDs (let fr = friendIDs s1 in s1\<lparr>friendIDs := fr(UID1 := removeAll UID2 (fr UID1), UID2 := removeAll UID1 (fr UID2))\<rparr>)
[PROOF STEP]
by (auto simp: distinct_remove1_removeAll)
[PROOF STATE]
proof (state)
this:
friendIDs (deleteFriend s UID1 p UID2) = friendIDs (deleteFriend s1 UID1 p' UID2)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eqButUID_createFriend12_friendIDs_eq:
assumes ss1: "eqButUID s s1"
and rs: "reach s" and rs1: "reach s1"
and f12: "\<not>friends12 s" "\<not>friends12 s1"
shows "friendIDs (createFriend s UID1 p UID2) = friendIDs (createFriend s1 UID1 p' UID2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. friendIDs (createFriend s UID1 p UID2) = friendIDs (createFriend s1 UID1 p' UID2)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. friendIDs (createFriend s UID1 p UID2) = friendIDs (createFriend s1 UID1 p' UID2)
[PROOF STEP]
have f12': "UID1 \<notin> set (friendIDs s UID2)" "UID2 \<notin> set (friendIDs s UID1)"
             "UID1 \<notin> set (friendIDs s1 UID2)" "UID2 \<notin> set (friendIDs s1 UID1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (UID1 \<notin> set (friendIDs s UID2) &&& UID2 \<notin> set (friendIDs s UID1)) &&& UID1 \<notin> set (friendIDs s1 UID2) &&& UID2 \<notin> set (friendIDs s1 UID1)
[PROOF STEP]
using f12 rs rs1 reach_friendIDs_symmetric
[PROOF STATE]
proof (prove)
using this:
\<not> friends12 s
\<not> friends12 s1
reach s
reach s1
reach ?s \<Longrightarrow> (?uID1.0 \<in>\<in> friendIDs ?s ?uID2.0) = (?uID2.0 \<in>\<in> friendIDs ?s ?uID1.0)

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

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

goal (1 subgoal):
 1. friendIDs (createFriend s UID1 p UID2) = friendIDs (createFriend s1 UID1 p' UID2)
[PROOF STEP]
have "friendIDs s = friendIDs s1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. friendIDs s = friendIDs s1
[PROOF STEP]
proof (intro ext)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. friendIDs s x = friendIDs s1 x
[PROOF STEP]
fix uid
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. friendIDs s x = friendIDs s1 x
[PROOF STEP]
show "friendIDs s uid = friendIDs s1 uid"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. friendIDs s uid = friendIDs s1 uid
[PROOF STEP]
using ss1 f12'
[PROOF STATE]
proof (prove)
using this:
eqButUID s s1
UID1 \<notin> set (friendIDs s UID2)
UID2 \<notin> set (friendIDs s UID1)
UID1 \<notin> set (friendIDs s1 UID2)
UID2 \<notin> set (friendIDs s1 UID1)

goal (1 subgoal):
 1. friendIDs s uid = friendIDs s1 uid
[PROOF STEP]
unfolding eqButUID_def eqButUIDf_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> (eqButUIDl UID2 (pendingFReqs s UID1) (pendingFReqs s1 UID1) \<and> eqButUIDl UID1 (pendingFReqs s UID2) (pendingFReqs s1 UID2) \<and> (\<forall>uid. uid \<noteq> UID1 \<and> uid \<noteq> UID2 \<longrightarrow> pendingFReqs s uid = pendingFReqs s1 uid)) \<and> eqButUID12 (friendReq s) (friendReq s1) \<and> (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)) \<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
UID1 \<notin> set (friendIDs s UID2)
UID2 \<notin> set (friendIDs s UID1)
UID1 \<notin> set (friendIDs s1 UID2)
UID2 \<notin> set (friendIDs s1 UID1)

goal (1 subgoal):
 1. friendIDs s uid = friendIDs s1 uid
[PROOF STEP]
by (cases "uid = UID1 \<or> uid = UID2") (auto simp: remove1_idem)
[PROOF STATE]
proof (state)
this:
friendIDs s uid = friendIDs s1 uid

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

goal (1 subgoal):
 1. friendIDs (createFriend s UID1 p UID2) = friendIDs (createFriend s1 UID1 p' UID2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
friendIDs s = friendIDs s1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
friendIDs s = friendIDs s1

goal (1 subgoal):
 1. friendIDs (createFriend s UID1 p UID2) = friendIDs (createFriend s1 UID1 p' UID2)
[PROOF STEP]
by (auto simp: c_defs)
[PROOF STATE]
proof (state)
this:
friendIDs (createFriend s UID1 p UID2) = friendIDs (createFriend s1 UID1 p' UID2)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma multi_to_arith_prog:
  "multi_arith_prog 1 start steps c =
    arith_prog start (steps 0) (c 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multi_arith_prog 1 start steps c = arith_prog start (steps 0) (c 0)
[PROOF STEP]
unfolding multi_arith_prog_def arith_prog_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. start + int (\<Sum>i<1. c i * steps i) = start + int (c 0 * steps 0)
[PROOF STEP]
by auto


[STATEMENT]
lemma arith_prog_to_multi:
  "arith_prog start step c =
    multi_arith_prog 1 start (\<lambda>_. step) (\<lambda>_. c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arith_prog start step c = multi_arith_prog 1 start (\<lambda>_. step) (\<lambda>_. c)
[PROOF STEP]
unfolding multi_arith_prog_def arith_prog_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. start + int (c * step) = start + int (\<Sum>i<1. c * step)
[PROOF STEP]
by auto


[STATEMENT]
lemma arith_prog_mono:
  assumes "c \<le> c'"
  shows   "arith_prog start step c \<le> arith_prog start step c'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arith_prog start step c \<le> arith_prog start step c'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
c \<le> c'

goal (1 subgoal):
 1. arith_prog start step c \<le> arith_prog start step c'
[PROOF STEP]
unfolding arith_prog_def
[PROOF STATE]
proof (prove)
using this:
c \<le> c'

goal (1 subgoal):
 1. start + int (c * step) \<le> start + int (c' * step)
[PROOF STEP]
by (auto intro: mult_mono)


[STATEMENT]
lemma is_arith_prog_onD:
  assumes "is_arith_prog_on l start step a b"
  assumes "c \<in> {0..<l}"
  shows   "arith_prog start step c \<in> {a..b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arith_prog start step c \<in> {a..b}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. arith_prog start step c \<in> {a..b}
[PROOF STEP]
have "arith_prog start step 0 \<le> arith_prog start step c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arith_prog start step 0 \<le> arith_prog start step c
[PROOF STEP]
by (rule arith_prog_mono) auto
[PROOF STATE]
proof (state)
this:
arith_prog start step 0 \<le> arith_prog start step c

goal (1 subgoal):
 1. arith_prog start step c \<in> {a..b}
[PROOF STEP]
hence "arith_prog start step c \<ge> a"
[PROOF STATE]
proof (prove)
using this:
arith_prog start step 0 \<le> arith_prog start step c

goal (1 subgoal):
 1. a \<le> arith_prog start step c
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
arith_prog start step 0 \<le> arith_prog start step c
is_arith_prog_on l start step a b
c \<in> {0..<l}

goal (1 subgoal):
 1. a \<le> arith_prog start step c
[PROOF STEP]
by (simp add: arith_prog_def is_arith_prog_on_def
                      add_increasing2)
[PROOF STATE]
proof (state)
this:
a \<le> arith_prog start step c

goal (1 subgoal):
 1. arith_prog start step c \<in> {a..b}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
a \<le> arith_prog start step c

goal (1 subgoal):
 1. arith_prog start step c \<in> {a..b}
[PROOF STEP]
have "arith_prog start step (l-1) \<ge>
                   arith_prog start step c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arith_prog start step c \<le> arith_prog start step (l - 1)
[PROOF STEP]
by (rule arith_prog_mono) (use assms(2) in auto)
[PROOF STATE]
proof (state)
this:
arith_prog start step c \<le> arith_prog start step (l - 1)

goal (1 subgoal):
 1. arith_prog start step c \<in> {a..b}
[PROOF STEP]
hence "arith_prog start step c \<le> b"
[PROOF STATE]
proof (prove)
using this:
arith_prog start step c \<le> arith_prog start step (l - 1)

goal (1 subgoal):
 1. arith_prog start step c \<le> b
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
arith_prog start step c \<le> arith_prog start step (l - 1)
is_arith_prog_on l start step a b
c \<in> {0..<l}

goal (1 subgoal):
 1. arith_prog start step c \<le> b
[PROOF STEP]
unfolding arith_prog_def is_arith_prog_on_def
[PROOF STATE]
proof (prove)
using this:
start + int (c * step) \<le> start + int ((l - 1) * step)
a \<le> start \<and> start + int ((l - 1) * step) \<le> b
c \<in> {0..<l}

goal (1 subgoal):
 1. start + int (c * step) \<le> b
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
arith_prog start step c \<le> b

goal (1 subgoal):
 1. arith_prog start step c \<in> {a..b}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
a \<le> arith_prog start step c
arith_prog start step c \<le> b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a \<le> arith_prog start step c
arith_prog start step c \<le> b

goal (1 subgoal):
 1. arith_prog start step c \<in> {a..b}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
arith_prog start step c \<in> {a..b}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma multi_arith_prog_mono:
  assumes "\<And>i. i < m \<Longrightarrow> c i \<le> c' i"
  shows   "multi_arith_prog m start steps c \<le>
            multi_arith_prog m start steps c'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multi_arith_prog m start steps c \<le> multi_arith_prog m start steps c'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?i < m \<Longrightarrow> c ?i \<le> c' ?i

goal (1 subgoal):
 1. multi_arith_prog m start steps c \<le> multi_arith_prog m start steps c'
[PROOF STEP]
unfolding multi_arith_prog_def
[PROOF STATE]
proof (prove)
using this:
?i < m \<Longrightarrow> c ?i \<le> c' ?i

goal (1 subgoal):
 1. start + int (\<Sum>i<m. c i * steps i) \<le> start + int (\<Sum>i<m. c' i * steps i)
[PROOF STEP]
by (auto intro!: sum_mono intro: mult_right_mono)


[STATEMENT]
lemma is_multi_arith_prog_onD:
  assumes "is_multi_arith_prog_on l m start steps a b"
  assumes "c \<in> {0..<m} \<rightarrow> {0..<l}"
  shows   "multi_arith_prog m start steps c \<in> {a..b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multi_arith_prog m start steps c \<in> {a..b}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. multi_arith_prog m start steps c \<in> {a..b}
[PROOF STEP]
have "multi_arith_prog m start steps (\<lambda>_. 0) \<le>
          multi_arith_prog m start steps c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multi_arith_prog m start steps (\<lambda>_. 0) \<le> multi_arith_prog m start steps c
[PROOF STEP]
by (rule multi_arith_prog_mono) auto
[PROOF STATE]
proof (state)
this:
multi_arith_prog m start steps (\<lambda>_. 0) \<le> multi_arith_prog m start steps c

goal (1 subgoal):
 1. multi_arith_prog m start steps c \<in> {a..b}
[PROOF STEP]
hence "multi_arith_prog m start steps c \<ge> a"
[PROOF STATE]
proof (prove)
using this:
multi_arith_prog m start steps (\<lambda>_. 0) \<le> multi_arith_prog m start steps c

goal (1 subgoal):
 1. a \<le> multi_arith_prog m start steps c
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
multi_arith_prog m start steps (\<lambda>_. 0) \<le> multi_arith_prog m start steps c
is_multi_arith_prog_on l m start steps a b
c \<in> {0..<m} \<rightarrow> {0..<l}

goal (1 subgoal):
 1. a \<le> multi_arith_prog m start steps c
[PROOF STEP]
by (simp add: multi_arith_prog_def
       is_multi_arith_prog_on_def)
[PROOF STATE]
proof (state)
this:
a \<le> multi_arith_prog m start steps c

goal (1 subgoal):
 1. multi_arith_prog m start steps c \<in> {a..b}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
a \<le> multi_arith_prog m start steps c

goal (1 subgoal):
 1. multi_arith_prog m start steps c \<in> {a..b}
[PROOF STEP]
have "multi_arith_prog m start steps (\<lambda>_. l-1) \<ge>
                   multi_arith_prog m start steps c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multi_arith_prog m start steps c \<le> multi_arith_prog m start steps (\<lambda>_. l - 1)
[PROOF STEP]
by (rule multi_arith_prog_mono) (use assms in force)
[PROOF STATE]
proof (state)
this:
multi_arith_prog m start steps c \<le> multi_arith_prog m start steps (\<lambda>_. l - 1)

goal (1 subgoal):
 1. multi_arith_prog m start steps c \<in> {a..b}
[PROOF STEP]
hence "multi_arith_prog m start steps c \<le> b"
[PROOF STATE]
proof (prove)
using this:
multi_arith_prog m start steps c \<le> multi_arith_prog m start steps (\<lambda>_. l - 1)

goal (1 subgoal):
 1. multi_arith_prog m start steps c \<le> b
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
multi_arith_prog m start steps c \<le> multi_arith_prog m start steps (\<lambda>_. l - 1)
is_multi_arith_prog_on l m start steps a b
c \<in> {0..<m} \<rightarrow> {0..<l}

goal (1 subgoal):
 1. multi_arith_prog m start steps c \<le> b
[PROOF STEP]
by (simp add: multi_arith_prog_def
        is_multi_arith_prog_on_def)
[PROOF STATE]
proof (state)
this:
multi_arith_prog m start steps c \<le> b

goal (1 subgoal):
 1. multi_arith_prog m start steps c \<in> {a..b}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
a \<le> multi_arith_prog m start steps c
multi_arith_prog m start steps c \<le> b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a \<le> multi_arith_prog m start steps c
multi_arith_prog m start steps c \<le> b

goal (1 subgoal):
 1. multi_arith_prog m start steps c \<in> {a..b}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
multi_arith_prog m start steps c \<in> {a..b}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vdwE:
  assumes "vdw k l n"
          "b + 1 \<ge> a + int n"
          "col \<in> {a..b} \<rightarrow> {..<k}"
  obtains j start step where
    "j < k" "step > 0"
    "is_arith_prog_on l start step a b"
    "arith_prog start step ` {..<l} \<subseteq> col -` {j} \<inter> {a..b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>j step start. \<lbrakk>j < k; 0 < step; is_arith_prog_on l start step a b; arith_prog start step ` {..<l} \<subseteq> col -` {j} \<inter> {a..b}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms that
[PROOF STATE]
proof (prove)
using this:
vdw k l n
a + int n \<le> b + 1
col \<in> {a..b} \<rightarrow> {..<k}
\<lbrakk>?j < k; 0 < ?step; is_arith_prog_on l ?start ?step a b; arith_prog ?start ?step ` {..<l} \<subseteq> col -` {?j} \<inter> {a..b}\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. (\<And>j step start. \<lbrakk>j < k; 0 < step; is_arith_prog_on l start step a b; arith_prog start step ` {..<l} \<subseteq> col -` {j} \<inter> {a..b}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding vdw_def
[PROOF STATE]
proof (prove)
using this:
\<forall>a b col. a + int n \<le> b + 1 \<and> col \<in> {a..b} \<rightarrow> {..<k} \<longrightarrow> (\<exists>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on l start step a b \<and> arith_prog start step ` {..<l} \<subseteq> col -` {j} \<inter> {a..b})
a + int n \<le> b + 1
col \<in> {a..b} \<rightarrow> {..<k}
\<lbrakk>?j < k; 0 < ?step; is_arith_prog_on l ?start ?step a b; arith_prog ?start ?step ` {..<l} \<subseteq> col -` {?j} \<inter> {a..b}\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. (\<And>j step start. \<lbrakk>j < k; 0 < step; is_arith_prog_on l start step a b; arith_prog start step ` {..<l} \<subseteq> col -` {j} \<inter> {a..b}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis


[STATEMENT]
lemma vdw_imp_pos:
  assumes "vdw k l n"
          "l > 0"
  shows "n > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < n
[PROOF STEP]
proof (rule Nat.gr0I)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n = 0 \<Longrightarrow> False
[PROOF STEP]
assume [simp]: "n = 0"
[PROOF STATE]
proof (state)
this:
n = 0

goal (1 subgoal):
 1. n = 0 \<Longrightarrow> False
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
vdw k l n
0 < l

goal (1 subgoal):
 1. False
[PROOF STEP]
by (elim vdwE[where a = 1 and b = 0 and col = "\<lambda>_. 0"])
       (auto simp: lessThan_empty_iff)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vdw_0_left [simp, intro]: "n>0 \<Longrightarrow> vdw 0 l n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> vdw 0 l n
[PROOF STEP]
by (auto simp: vdw_def)


[STATEMENT]
lemma vdw_1_left:
  assumes "l>0"
  shows "vdw 1 l l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vdw 1 l l
[PROOF STEP]
unfolding vdw_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a b col. a + int l \<le> b + 1 \<and> col \<in> {a..b} \<rightarrow> {..<1} \<longrightarrow> (\<exists>j start step. j < 1 \<and> 0 < step \<and> is_arith_prog_on l start step a b \<and> arith_prog start step ` {..<l} \<subseteq> col -` {j} \<inter> {a..b})
[PROOF STEP]
proof (safe, goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int l \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<1}\<rbrakk> \<Longrightarrow> \<exists>j start step. j < 1 \<and> 0 < step \<and> is_arith_prog_on l start step a b \<and> arith_prog start step ` {..<l} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
case (1 a b col)
[PROOF STATE]
proof (state)
this:
a + int l \<le> b + 1
col \<in> {a..b} \<rightarrow> {..<1}

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int l \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<1}\<rbrakk> \<Longrightarrow> \<exists>j start step. j < 1 \<and> 0 < step \<and> is_arith_prog_on l start step a b \<and> arith_prog start step ` {..<l} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
have "arith_prog a 1 ` {..<l} \<subseteq> {a..b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arith_prog a 1 ` {..<l} \<subseteq> {a..b}
[PROOF STEP]
using 1(1)
[PROOF STATE]
proof (prove)
using this:
a + int l \<le> b + 1

goal (1 subgoal):
 1. arith_prog a 1 ` {..<l} \<subseteq> {a..b}
[PROOF STEP]
by (auto simp: arith_prog_def)
[PROOF STATE]
proof (state)
this:
arith_prog a 1 ` {..<l} \<subseteq> {a..b}

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int l \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<1}\<rbrakk> \<Longrightarrow> \<exists>j start step. j < 1 \<and> 0 < step \<and> is_arith_prog_on l start step a b \<and> arith_prog start step ` {..<l} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
arith_prog a 1 ` {..<l} \<subseteq> {a..b}

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int l \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<1}\<rbrakk> \<Longrightarrow> \<exists>j start step. j < 1 \<and> 0 < step \<and> is_arith_prog_on l start step a b \<and> arith_prog start step ` {..<l} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
have "{a..b} = col -` {0} \<inter> {a..b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {a..b} = col -` {0} \<inter> {a..b}
[PROOF STEP]
using 1(2)
[PROOF STATE]
proof (prove)
using this:
col \<in> {a..b} \<rightarrow> {..<1}

goal (1 subgoal):
 1. {a..b} = col -` {0} \<inter> {a..b}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{a..b} = col -` {0} \<inter> {a..b}

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int l \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<1}\<rbrakk> \<Longrightarrow> \<exists>j start step. j < 1 \<and> 0 < step \<and> is_arith_prog_on l start step a b \<and> arith_prog start step ` {..<l} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
arith_prog a 1 ` {..<l} \<subseteq> col -` {0} \<inter> {a..b}
[PROOF STEP]
have "arith_prog a 1 ` {..<l} \<subseteq> col -` {0} \<inter> {a..b}"
[PROOF STATE]
proof (prove)
using this:
arith_prog a 1 ` {..<l} \<subseteq> col -` {0} \<inter> {a..b}

goal (1 subgoal):
 1. arith_prog a 1 ` {..<l} \<subseteq> col -` {0} \<inter> {a..b}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
arith_prog a 1 ` {..<l} \<subseteq> col -` {0} \<inter> {a..b}

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int l \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<1}\<rbrakk> \<Longrightarrow> \<exists>j start step. j < 1 \<and> 0 < step \<and> is_arith_prog_on l start step a b \<and> arith_prog start step ` {..<l} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
arith_prog a 1 ` {..<l} \<subseteq> col -` {0} \<inter> {a..b}

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int l \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<1}\<rbrakk> \<Longrightarrow> \<exists>j start step. j < 1 \<and> 0 < step \<and> is_arith_prog_on l start step a b \<and> arith_prog start step ` {..<l} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
have "is_arith_prog_on l a 1 a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_arith_prog_on l a 1 a b
[PROOF STEP]
unfolding is_arith_prog_on_def arith_prog_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<le> a \<and> a + int ((l - 1) * 1) \<le> b
[PROOF STEP]
using 1 assms
[PROOF STATE]
proof (prove)
using this:
a + int l \<le> b + 1
col \<in> {a..b} \<rightarrow> {..<1}
0 < l

goal (1 subgoal):
 1. a \<le> a \<and> a + int ((l - 1) * 1) \<le> b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_arith_prog_on l a 1 a b

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int l \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<1}\<rbrakk> \<Longrightarrow> \<exists>j start step. j < 1 \<and> 0 < step \<and> is_arith_prog_on l start step a b \<and> arith_prog start step ` {..<l} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
arith_prog a 1 ` {..<l} \<subseteq> col -` {0} \<inter> {a..b}
is_arith_prog_on l a 1 a b
[PROOF STEP]
show "\<exists>j start step. j < 1 \<and> 0 < step \<and>
        is_arith_prog_on l start step a b \<and>
        arith_prog start step ` {..<l} \<subseteq> col -` {j} \<inter> {a..b}"
[PROOF STATE]
proof (prove)
using this:
arith_prog a 1 ` {..<l} \<subseteq> col -` {0} \<inter> {a..b}
is_arith_prog_on l a 1 a b

goal (1 subgoal):
 1. \<exists>j start step. j < 1 \<and> 0 < step \<and> is_arith_prog_on l start step a b \<and> arith_prog start step ` {..<l} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>j start step. j < 1 \<and> 0 < step \<and> is_arith_prog_on l start step a b \<and> arith_prog start step ` {..<l} \<subseteq> col -` {j} \<inter> {a..b}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vdw_1_right: "vdw k 1 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vdw k 1 1
[PROOF STEP]
unfolding vdw_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a b col. a + int 1 \<le> b + 1 \<and> col \<in> {a..b} \<rightarrow> {..<k} \<longrightarrow> (\<exists>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on 1 start step a b \<and> arith_prog start step ` {..<1} \<subseteq> col -` {j} \<inter> {a..b})
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int 1 \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on 1 start step a b \<and> arith_prog start step ` {..<1} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
fix a b :: int and col :: "int \<Rightarrow> nat"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int 1 \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on 1 start step a b \<and> arith_prog start step ` {..<1} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
assume *: "a + int 1 \<le> b + 1" "col \<in> {a..b} \<rightarrow> {..<k}"
[PROOF STATE]
proof (state)
this:
a + int 1 \<le> b + 1
col \<in> {a..b} \<rightarrow> {..<k}

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int 1 \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on 1 start step a b \<and> arith_prog start step ` {..<1} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
have "col a < k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. col a < k
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
a + int 1 \<le> b + 1
col \<in> {a..b} \<rightarrow> {..<k}

goal (1 subgoal):
 1. col a < k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
col a < k

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int 1 \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on 1 start step a b \<and> arith_prog start step ` {..<1} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
have "arith_prog a 1 ` {..<1} = {a}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arith_prog a 1 ` {..<1} = {a}
[PROOF STEP]
using *(1)
[PROOF STATE]
proof (prove)
using this:
a + int 1 \<le> b + 1

goal (1 subgoal):
 1. arith_prog a 1 ` {..<1} = {a}
[PROOF STEP]
by (auto simp: arith_prog_def)
[PROOF STATE]
proof (state)
this:
arith_prog a 1 ` {..<1} = {a}

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int 1 \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on 1 start step a b \<and> arith_prog start step ` {..<1} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
arith_prog a 1 ` {..<1} = {a}

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int 1 \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on 1 start step a b \<and> arith_prog start step ` {..<1} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
have "{a} \<subseteq> col -` {col a} \<inter> {a..b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {a} \<subseteq> col -` {col a} \<inter> {a..b}
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
a + int 1 \<le> b + 1
col \<in> {a..b} \<rightarrow> {..<k}

goal (1 subgoal):
 1. {a} \<subseteq> col -` {col a} \<inter> {a..b}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{a} \<subseteq> col -` {col a} \<inter> {a..b}

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int 1 \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on 1 start step a b \<and> arith_prog start step ` {..<1} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
arith_prog a 1 ` {..<1} \<subseteq> col -` {col a} \<inter> {a..b}
[PROOF STEP]
have "arith_prog a 1 ` {..<1} \<subseteq> col -` {col a} \<inter> {a..b}"
[PROOF STATE]
proof (prove)
using this:
arith_prog a 1 ` {..<1} \<subseteq> col -` {col a} \<inter> {a..b}

goal (1 subgoal):
 1. arith_prog a 1 ` {..<1} \<subseteq> col -` {col a} \<inter> {a..b}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
arith_prog a 1 ` {..<1} \<subseteq> col -` {col a} \<inter> {a..b}

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int 1 \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on 1 start step a b \<and> arith_prog start step ` {..<1} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
arith_prog a 1 ` {..<1} \<subseteq> col -` {col a} \<inter> {a..b}

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int 1 \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on 1 start step a b \<and> arith_prog start step ` {..<1} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
have "is_arith_prog_on 1 a 1 a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_arith_prog_on 1 a 1 a b
[PROOF STEP]
unfolding is_arith_prog_on_def arith_prog_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<le> a \<and> a + int ((1 - 1) * 1) \<le> b
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
a + int 1 \<le> b + 1
col \<in> {a..b} \<rightarrow> {..<k}

goal (1 subgoal):
 1. a \<le> a \<and> a + int ((1 - 1) * 1) \<le> b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_arith_prog_on 1 a 1 a b

goal (1 subgoal):
 1. \<And>a b col. \<lbrakk>a + int 1 \<le> b + 1; col \<in> {a..b} \<rightarrow> {..<k}\<rbrakk> \<Longrightarrow> \<exists>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on 1 start step a b \<and> arith_prog start step ` {..<1} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
arith_prog a 1 ` {..<1} \<subseteq> col -` {col a} \<inter> {a..b}
is_arith_prog_on 1 a 1 a b
[PROOF STEP]
show  "\<exists>j start step.
          j < k \<and> 0 < step \<and> is_arith_prog_on 1 start step a b \<and>
          arith_prog start step ` {..<1} \<subseteq> col -` {j} \<inter> {a..b}"
[PROOF STATE]
proof (prove)
using this:
arith_prog a 1 ` {..<1} \<subseteq> col -` {col a} \<inter> {a..b}
is_arith_prog_on 1 a 1 a b

goal (1 subgoal):
 1. \<exists>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on 1 start step a b \<and> arith_prog start step ` {..<1} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
using \<open>col a <k\<close>
[PROOF STATE]
proof (prove)
using this:
arith_prog a 1 ` {..<1} \<subseteq> col -` {col a} \<inter> {a..b}
is_arith_prog_on 1 a 1 a b
col a < k

goal (1 subgoal):
 1. \<exists>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on 1 start step a b \<and> arith_prog start step ` {..<1} \<subseteq> col -` {j} \<inter> {a..b}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>j start step. j < k \<and> 0 < step \<and> is_arith_prog_on 1 start step a b \<and> arith_prog start step ` {..<1} \<subseteq> col -` {j} \<inter> {a..b}

goal:
No subgoals!
[PROOF STEP]
qed