[STATEMENT]
lemma eqButUID_step_\<phi>_imp:
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 \<phi>: "\<phi> (Trans s a ou s')"
shows "\<phi> (Trans s1 a ou1 s1')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> (Trans s1 a ou1 s1')
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<phi> (Trans s1 a ou1 s1')
[PROOF STEP]
have "eqButUID s' s1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqButUID s' s1'
[PROOF STEP]
using eqButUID_step[OF ss1 step step1 rs rs1]
[PROOF STATE]
proof (prove)
using this:
eqButUID s' s1'

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

goal (1 subgoal):
 1. \<phi> (Trans s1 a ou1 s1')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eqButUID s' s1'
[PROOF STEP]
have "open s = open s1" and "open s' = open s1'"
        and "openByA s = openByA s1" and "openByA s' = openByA s1'"
        and "openByF s = openByF s1" and "openByF s' = openByF s1'"
[PROOF STATE]
proof (prove)
using this:
eqButUID s' s1'

goal (1 subgoal):
 1. (open s = open s1 &&& open s' = open s1' &&& openByA s = openByA s1) &&& openByA s' = openByA s1' &&& openByF s = openByF s1 &&& openByF s' = openByF s1'
[PROOF STEP]
using ss1
[PROOF STATE]
proof (prove)
using this:
eqButUID s' s1'
eqButUID s s1

goal (1 subgoal):
 1. (open s = open s1 &&& open s' = open s1' &&& openByA s = openByA s1) &&& openByA s' = openByA s1' &&& openByF s = openByF s1 &&& openByF s' = openByF s1'
[PROOF STEP]
by (auto simp: eqButUID_open_eq eqButUID_openByA_eq eqButUID_openByF_eq)
[PROOF STATE]
proof (state)
this:
open s = open s1
open s' = open s1'
openByA s = openByA s1
openByA s' = openByA s1'
openByF s = openByF s1
openByF s' = openByF s1'

goal (1 subgoal):
 1. \<phi> (Trans s1 a ou1 s1')
[PROOF STEP]
with \<phi> a step step1
[PROOF STATE]
proof (chain)
picking this:
\<phi> (Trans s a ou s')
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)
step s a = (ou, s')
step s1 a = (ou1, s1')
open s = open s1
open s' = open s1'
openByA s = openByA s1
openByA s' = openByA s1'
openByF s = openByF s1
openByF s' = openByF s1'
[PROOF STEP]
show "\<phi> (Trans s1 a ou1 s1')"
[PROOF STATE]
proof (prove)
using this:
\<phi> (Trans s a ou s')
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)
step s a = (ou, s')
step s1 a = (ou1, s1')
open s = open s1
open s' = open s1'
openByA s = openByA s1
openByA s' = openByA s1'
openByF s = openByF s1
openByF s' = openByF s1'

goal (1 subgoal):
 1. \<phi> (Trans s1 a ou1 s1')
[PROOF STEP]
using UID1_UID2_UIDs
[PROOF STATE]
proof (prove)
using this:
\<phi> (Trans s a ou s')
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)
step s a = (ou, s')
step s1 a = (ou1, s1')
open s = open s1
open s' = open s1'
openByA s = openByA s1
openByA s' = openByA s1'
openByF s = openByF s1
openByF s' = openByF s1'
{UID1, UID2} \<inter> UIDs = {}

goal (1 subgoal):
 1. \<phi> (Trans s1 a ou1 s1')
[PROOF STEP]
by (elim \<phi>.elims) (auto simp: c_defs d_defs)
[PROOF STATE]
proof (state)
this:
\<phi> (Trans s1 a ou1 s1')

goal:
No subgoals!
[PROOF STEP]
qed