[STATEMENT]
lemma eqButUID_step_\<gamma>:
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: "\<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow>
                   a \<noteq> COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<and>
                   a \<noteq> COMact (comSendDeleteOFriend UID (pass s UID) aID uID')"
shows "\<gamma> (Trans s a ou s') = \<gamma> (Trans s1 a ou1 s1')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<gamma> (Trans s a ou s') = \<gamma> (Trans s1 a ou1 s1')
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<gamma> (Trans s a ou s') = \<gamma> (Trans s1 a ou1 s1')
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<gamma> (Trans s a ou s') = \<gamma> (Trans s1 a ou1 s1')
[PROOF STEP]
fix ca
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<gamma> (Trans s a ou s') = \<gamma> (Trans s1 a ou1 s1')
[PROOF STEP]
assume a: "a = COMact ca"
[PROOF STATE]
proof (state)
this:
a = COMact ca

goal (1 subgoal):
 1. \<gamma> (Trans s a ou s') = \<gamma> (Trans s1 a ou1 s1')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a = COMact ca
[PROOF STEP]
have "ou = ou1"
[PROOF STATE]
proof (prove)
using this:
a = COMact ca

goal (1 subgoal):
 1. ou = ou1
[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')
\<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s UID) aID uID')

goal (1 subgoal):
 1. ou = ou1
[PROOF STEP]
proof (cases ca)
[PROOF STATE]
proof (state)
goal (10 subgoals):
 1. \<And>x11 x12 x13 x14. \<lbrakk>a = COMact ca; eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); \<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); ca = comSendServerReq x11 x12 x13 x14\<rbrakk> \<Longrightarrow> ou = ou1
 2. \<And>x21 x22. \<lbrakk>a = COMact ca; eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); \<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); ca = comReceiveClientReq x21 x22\<rbrakk> \<Longrightarrow> ou = ou1
 3. \<And>x31 x32 x33 x34. \<lbrakk>a = COMact ca; eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); \<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); ca = comConnectClient x31 x32 x33 x34\<rbrakk> \<Longrightarrow> ou = ou1
 4. \<And>x41 x42. \<lbrakk>a = COMact ca; eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); \<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); ca = comConnectServer x41 x42\<rbrakk> \<Longrightarrow> ou = ou1
 5. \<And>x51 x52 x53 x54 x55 x56. \<lbrakk>a = COMact ca; eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); \<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); ca = comReceivePost x51 x52 x53 x54 x55 x56\<rbrakk> \<Longrightarrow> ou = ou1
 6. \<And>x61 x62 x63 x64. \<lbrakk>a = COMact ca; eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); \<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); ca = comSendPost x61 x62 x63 x64\<rbrakk> \<Longrightarrow> ou = ou1
 7. \<And>x71 x72 x73 x74. \<lbrakk>a = COMact ca; eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); \<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); ca = comReceiveCreateOFriend x71 x72 x73 x74\<rbrakk> \<Longrightarrow> ou = ou1
 8. \<And>x81 x82 x83 x84. \<lbrakk>a = COMact ca; eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); \<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); ca = comSendCreateOFriend x81 x82 x83 x84\<rbrakk> \<Longrightarrow> ou = ou1
 9. \<And>x91 x92 x93 x94. \<lbrakk>a = COMact ca; eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); \<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); ca = comReceiveDeleteOFriend x91 x92 x93 x94\<rbrakk> \<Longrightarrow> ou = ou1
 10. \<And>x101 x102 x103 x104. \<lbrakk>a = COMact ca; eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); \<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); ca = comSendDeleteOFriend x101 x102 x103 x104\<rbrakk> \<Longrightarrow> ou = ou1
[PROOF STEP]
case (comSendCreateOFriend uid p aid uid')
[PROOF STATE]
proof (state)
this:
ca = comSendCreateOFriend uid p aid uid'

goal (10 subgoals):
 1. \<And>x11 x12 x13 x14. \<lbrakk>a = COMact ca; eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); \<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); ca = comSendServerReq x11 x12 x13 x14\<rbrakk> \<Longrightarrow> ou = ou1
 2. \<And>x21 x22. \<lbrakk>a = COMact ca; eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); \<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); ca = comReceiveClientReq x21 x22\<rbrakk> \<Longrightarrow> ou = ou1
 3. \<And>x31 x32 x33 x34. \<lbrakk>a = COMact ca; eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); \<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); ca = comConnectClient x31 x32 x33 x34\<rbrakk> \<Longrightarrow> ou = ou1
 4. \<And>x41 x42. \<lbrakk>a = COMact ca; eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); \<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); ca = comConnectServer x41 x42\<rbrakk> \<Longrightarrow> ou = ou1
 5. \<And>x51 x52 x53 x54 x55 x56. \<lbrakk>a = COMact ca; eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); \<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); ca = comReceivePost x51 x52 x53 x54 x55 x56\<rbrakk> \<Longrightarrow> ou = ou1
 6. \<And>x61 x62 x63 x64. \<lbrakk>a = COMact ca; eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); \<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); ca = comSendPost x61 x62 x63 x64\<rbrakk> \<Longrightarrow> ou = ou1
 7. \<And>x71 x72 x73 x74. \<lbrakk>a = COMact ca; eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); \<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); ca = comReceiveCreateOFriend x71 x72 x73 x74\<rbrakk> \<Longrightarrow> ou = ou1
 8. \<And>x81 x82 x83 x84. \<lbrakk>a = COMact ca; eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); \<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); ca = comSendCreateOFriend x81 x82 x83 x84\<rbrakk> \<Longrightarrow> ou = ou1
 9. \<And>x91 x92 x93 x94. \<lbrakk>a = COMact ca; eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); \<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); ca = comReceiveDeleteOFriend x91 x92 x93 x94\<rbrakk> \<Longrightarrow> ou = ou1
 10. \<And>x101 x102 x103 x104. \<lbrakk>a = COMact ca; eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); \<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); ca = comSendDeleteOFriend x101 x102 x103 x104\<rbrakk> \<Longrightarrow> ou = ou1
[PROOF STEP]
with assms a
[PROOF STATE]
proof (chain)
picking this:
eqButUID s s1
reach s
reach s1
step s a = (ou, s')
step s1 a = (ou1, s1')
\<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s UID) aID uID')
a = COMact ca
ca = comSendCreateOFriend uid p aid uid'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eqButUID s s1
reach s
reach s1
step s a = (ou, s')
step s1 a = (ou1, s1')
\<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s UID) aID uID')
a = COMact ca
ca = comSendCreateOFriend uid p aid uid'

goal (1 subgoal):
 1. ou = ou1
[PROOF STEP]
by (cases "uid = UID"; cases "uid' \<in> UIDs aid")
             (auto simp: com_defs eqButUID_def eqButUID_sentOuterFriends_UIDs eqButUID_not_UID)
[PROOF STATE]
proof (state)
this:
ou = ou1

goal (9 subgoals):
 1. \<And>x11 x12 x13 x14. \<lbrakk>a = COMact ca; eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); \<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); ca = comSendServerReq x11 x12 x13 x14\<rbrakk> \<Longrightarrow> ou = ou1
 2. \<And>x21 x22. \<lbrakk>a = COMact ca; eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); \<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); ca = comReceiveClientReq x21 x22\<rbrakk> \<Longrightarrow> ou = ou1
 3. \<And>x31 x32 x33 x34. \<lbrakk>a = COMact ca; eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); \<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); ca = comConnectClient x31 x32 x33 x34\<rbrakk> \<Longrightarrow> ou = ou1
 4. \<And>x41 x42. \<lbrakk>a = COMact ca; eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); \<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); ca = comConnectServer x41 x42\<rbrakk> \<Longrightarrow> ou = ou1
 5. \<And>x51 x52 x53 x54 x55 x56. \<lbrakk>a = COMact ca; eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); \<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); ca = comReceivePost x51 x52 x53 x54 x55 x56\<rbrakk> \<Longrightarrow> ou = ou1
 6. \<And>x61 x62 x63 x64. \<lbrakk>a = COMact ca; eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); \<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); ca = comSendPost x61 x62 x63 x64\<rbrakk> \<Longrightarrow> ou = ou1
 7. \<And>x71 x72 x73 x74. \<lbrakk>a = COMact ca; eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); \<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); ca = comReceiveCreateOFriend x71 x72 x73 x74\<rbrakk> \<Longrightarrow> ou = ou1
 8. \<And>x91 x92 x93 x94. \<lbrakk>a = COMact ca; eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); \<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); ca = comReceiveDeleteOFriend x91 x92 x93 x94\<rbrakk> \<Longrightarrow> ou = ou1
 9. \<And>x101 x102 x103 x104. \<lbrakk>a = COMact ca; eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); \<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); ca = comSendDeleteOFriend x101 x102 x103 x104\<rbrakk> \<Longrightarrow> ou = ou1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. \<And>x11 x12 x13 x14. \<lbrakk>a = COMact ca; eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); \<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); ca = comSendServerReq x11 x12 x13 x14\<rbrakk> \<Longrightarrow> ou = ou1
 2. \<And>x21 x22. \<lbrakk>a = COMact ca; eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); \<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); ca = comReceiveClientReq x21 x22\<rbrakk> \<Longrightarrow> ou = ou1
 3. \<And>x31 x32 x33 x34. \<lbrakk>a = COMact ca; eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); \<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); ca = comConnectClient x31 x32 x33 x34\<rbrakk> \<Longrightarrow> ou = ou1
 4. \<And>x41 x42. \<lbrakk>a = COMact ca; eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); \<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); ca = comConnectServer x41 x42\<rbrakk> \<Longrightarrow> ou = ou1
 5. \<And>x51 x52 x53 x54 x55 x56. \<lbrakk>a = COMact ca; eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); \<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); ca = comReceivePost x51 x52 x53 x54 x55 x56\<rbrakk> \<Longrightarrow> ou = ou1
 6. \<And>x61 x62 x63 x64. \<lbrakk>a = COMact ca; eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); \<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); ca = comSendPost x61 x62 x63 x64\<rbrakk> \<Longrightarrow> ou = ou1
 7. \<And>x71 x72 x73 x74. \<lbrakk>a = COMact ca; eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); \<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); ca = comReceiveCreateOFriend x71 x72 x73 x74\<rbrakk> \<Longrightarrow> ou = ou1
 8. \<And>x91 x92 x93 x94. \<lbrakk>a = COMact ca; eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); \<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); ca = comReceiveDeleteOFriend x91 x92 x93 x94\<rbrakk> \<Longrightarrow> ou = ou1
 9. \<And>x101 x102 x103 x104. \<lbrakk>a = COMact ca; eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); \<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); ca = comSendDeleteOFriend x101 x102 x103 x104\<rbrakk> \<Longrightarrow> ou = ou1
[PROOF STEP]
case (comSendDeleteOFriend uid p aid uid')
[PROOF STATE]
proof (state)
this:
ca = comSendDeleteOFriend uid p aid uid'

goal (9 subgoals):
 1. \<And>x11 x12 x13 x14. \<lbrakk>a = COMact ca; eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); \<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); ca = comSendServerReq x11 x12 x13 x14\<rbrakk> \<Longrightarrow> ou = ou1
 2. \<And>x21 x22. \<lbrakk>a = COMact ca; eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); \<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); ca = comReceiveClientReq x21 x22\<rbrakk> \<Longrightarrow> ou = ou1
 3. \<And>x31 x32 x33 x34. \<lbrakk>a = COMact ca; eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); \<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); ca = comConnectClient x31 x32 x33 x34\<rbrakk> \<Longrightarrow> ou = ou1
 4. \<And>x41 x42. \<lbrakk>a = COMact ca; eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); \<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); ca = comConnectServer x41 x42\<rbrakk> \<Longrightarrow> ou = ou1
 5. \<And>x51 x52 x53 x54 x55 x56. \<lbrakk>a = COMact ca; eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); \<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); ca = comReceivePost x51 x52 x53 x54 x55 x56\<rbrakk> \<Longrightarrow> ou = ou1
 6. \<And>x61 x62 x63 x64. \<lbrakk>a = COMact ca; eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); \<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); ca = comSendPost x61 x62 x63 x64\<rbrakk> \<Longrightarrow> ou = ou1
 7. \<And>x71 x72 x73 x74. \<lbrakk>a = COMact ca; eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); \<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); ca = comReceiveCreateOFriend x71 x72 x73 x74\<rbrakk> \<Longrightarrow> ou = ou1
 8. \<And>x91 x92 x93 x94. \<lbrakk>a = COMact ca; eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); \<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); ca = comReceiveDeleteOFriend x91 x92 x93 x94\<rbrakk> \<Longrightarrow> ou = ou1
 9. \<And>x101 x102 x103 x104. \<lbrakk>a = COMact ca; eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); \<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); ca = comSendDeleteOFriend x101 x102 x103 x104\<rbrakk> \<Longrightarrow> ou = ou1
[PROOF STEP]
with assms a
[PROOF STATE]
proof (chain)
picking this:
eqButUID s s1
reach s
reach s1
step s a = (ou, s')
step s1 a = (ou1, s1')
\<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s UID) aID uID')
a = COMact ca
ca = comSendDeleteOFriend uid p aid uid'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eqButUID s s1
reach s
reach s1
step s a = (ou, s')
step s1 a = (ou1, s1')
\<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s UID) aID uID')
a = COMact ca
ca = comSendDeleteOFriend uid p aid uid'

goal (1 subgoal):
 1. ou = ou1
[PROOF STEP]
by (cases "uid = UID"; cases "uid' \<in> UIDs aid")
             (auto simp: com_defs eqButUID_def eqButUID_sentOuterFriends_UIDs eqButUID_not_UID)
[PROOF STATE]
proof (state)
this:
ou = ou1

goal (8 subgoals):
 1. \<And>x11 x12 x13 x14. \<lbrakk>a = COMact ca; eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); \<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); ca = comSendServerReq x11 x12 x13 x14\<rbrakk> \<Longrightarrow> ou = ou1
 2. \<And>x21 x22. \<lbrakk>a = COMact ca; eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); \<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); ca = comReceiveClientReq x21 x22\<rbrakk> \<Longrightarrow> ou = ou1
 3. \<And>x31 x32 x33 x34. \<lbrakk>a = COMact ca; eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); \<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); ca = comConnectClient x31 x32 x33 x34\<rbrakk> \<Longrightarrow> ou = ou1
 4. \<And>x41 x42. \<lbrakk>a = COMact ca; eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); \<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); ca = comConnectServer x41 x42\<rbrakk> \<Longrightarrow> ou = ou1
 5. \<And>x51 x52 x53 x54 x55 x56. \<lbrakk>a = COMact ca; eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); \<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); ca = comReceivePost x51 x52 x53 x54 x55 x56\<rbrakk> \<Longrightarrow> ou = ou1
 6. \<And>x61 x62 x63 x64. \<lbrakk>a = COMact ca; eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); \<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); ca = comSendPost x61 x62 x63 x64\<rbrakk> \<Longrightarrow> ou = ou1
 7. \<And>x71 x72 x73 x74. \<lbrakk>a = COMact ca; eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); \<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); ca = comReceiveCreateOFriend x71 x72 x73 x74\<rbrakk> \<Longrightarrow> ou = ou1
 8. \<And>x91 x92 x93 x94. \<lbrakk>a = COMact ca; eqButUID s s1; reach s; reach s1; step s a = (ou, s'); step s1 a = (ou1, s1'); \<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s UID) aID uID'); ca = comReceiveDeleteOFriend x91 x92 x93 x94\<rbrakk> \<Longrightarrow> ou = ou1
[PROOF STEP]
qed (auto simp: com_defs eqButUID_def)
[PROOF STATE]
proof (state)
this:
ou = ou1

goal (1 subgoal):
 1. \<gamma> (Trans s a ou s') = \<gamma> (Trans s1 a ou1 s1')
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
a = COMact ?ca2 \<Longrightarrow> ou = ou1

goal (1 subgoal):
 1. \<gamma> (Trans s a ou s') = \<gamma> (Trans s1 a ou1 s1')
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
eqButUID s s1
reach s
reach s1
step s a = (ou, s')
step s1 a = (ou1, s1')
\<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s UID) aID uID')
a = COMact ?ca2 \<Longrightarrow> ou = ou1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eqButUID s s1
reach s
reach s1
step s a = (ou, s')
step s1 a = (ou1, s1')
\<forall>aID uID'. uID' \<notin> UIDs aID \<longrightarrow> a \<noteq> COMact (comSendCreateOFriend UID (pass s UID) aID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend UID (pass s UID) aID uID')
a = COMact ?ca2 \<Longrightarrow> ou = ou1

goal (1 subgoal):
 1. \<gamma> (Trans s a ou s') = \<gamma> (Trans s1 a ou1 s1')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<gamma> (Trans s a ou s') = \<gamma> (Trans s1 a ou1 s1')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma weakCongruenceE:
  fixes P  :: "ccs"
  and   Q  :: "ccs"

  assumes "P \<cong> Q"

  shows "P \<leadsto><weakBisimulation> Q"
  and   "Q \<leadsto><weakBisimulation> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<leadsto><weakBisimulation> Q &&& Q \<leadsto><weakBisimulation> P
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P \<cong> Q

goal (1 subgoal):
 1. P \<leadsto><weakBisimulation> Q &&& Q \<leadsto><weakBisimulation> P
[PROOF STEP]
by(auto simp add: weakCongruence_def)


[STATEMENT]
lemma weakCongruenceI:
  fixes P :: "ccs"
  and   Q :: "ccs"

  assumes "P \<leadsto><weakBisimulation> Q"
  and     "Q \<leadsto><weakBisimulation> P"

  shows "P \<cong> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<cong> Q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P \<leadsto><weakBisimulation> Q
Q \<leadsto><weakBisimulation> P

goal (1 subgoal):
 1. P \<cong> Q
[PROOF STEP]
by(auto simp add: weakCongruence_def)


[STATEMENT]
lemma weakCongISym[consumes 1, case_names cSym cSim]:
  fixes P :: ccs
  and   Q :: ccs

  assumes "Prop P Q"
  and     "\<And>P Q. Prop P Q \<Longrightarrow> Prop Q P"
  and     "\<And>P Q. Prop P Q \<Longrightarrow> (F P) \<leadsto><weakBisimulation> (F Q)"

  shows "F P \<cong> F Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F P \<cong> F Q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Prop P Q
Prop ?P ?Q \<Longrightarrow> Prop ?Q ?P
Prop ?P ?Q \<Longrightarrow> F ?P \<leadsto><weakBisimulation> F ?Q

goal (1 subgoal):
 1. F P \<cong> F Q
[PROOF STEP]
by(auto simp add: weakCongruence_def)


[STATEMENT]
lemma weakCongISym2[consumes 1, case_names cSim]:
  fixes P :: ccs
  and   Q :: ccs

  assumes "P \<cong> Q"
  and     "\<And>P Q. P \<cong> Q \<Longrightarrow> (F P) \<leadsto><weakBisimulation> (F Q)"

  shows "F P \<cong> F Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F P \<cong> F Q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P \<cong> Q
?P \<cong> ?Q \<Longrightarrow> F ?P \<leadsto><weakBisimulation> F ?Q

goal (1 subgoal):
 1. F P \<cong> F Q
[PROOF STEP]
by(auto simp add: weakCongruence_def)


[STATEMENT]
lemma reflexive:
  fixes P :: ccs

  shows "P \<cong> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<cong> P
[PROOF STEP]
by(auto intro: weakCongruenceI Weak_Bisim.reflexive Weak_Cong_Sim.reflexive)


[STATEMENT]
lemma symmetric:
  fixes P :: ccs
  and   Q :: ccs

  assumes "P \<cong> Q"

  shows "Q \<cong> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q \<cong> P
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P \<cong> Q

goal (1 subgoal):
 1. Q \<cong> P
[PROOF STEP]
by(auto simp add: weakCongruence_def)


[STATEMENT]
lemma transitive:
  fixes P :: ccs
  and   Q :: ccs
  and   R :: ccs

  assumes "P \<cong> Q"
  and     "Q \<cong> R"

  shows "P \<cong> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<cong> R
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P \<cong> R
[PROOF STEP]
let ?Prop = "\<lambda>P R. \<exists>Q. P \<cong> Q \<and> Q \<cong> R"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P \<cong> R
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
P \<cong> Q
Q \<cong> R
[PROOF STEP]
have "?Prop P R"
[PROOF STATE]
proof (prove)
using this:
P \<cong> Q
Q \<cong> R

goal (1 subgoal):
 1. \<exists>Q. P \<cong> Q \<and> Q \<cong> R
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>Q. P \<cong> Q \<and> Q \<cong> R

goal (1 subgoal):
 1. P \<cong> R
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>Q. P \<cong> Q \<and> Q \<cong> R

goal (1 subgoal):
 1. P \<cong> R
[PROOF STEP]
proof(induct rule: weakCongISym)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>P Q. \<exists>Qa. P \<cong> Qa \<and> Qa \<cong> Q \<Longrightarrow> \<exists>Qa. Q \<cong> Qa \<and> Qa \<cong> P
 2. \<And>P Q. \<exists>Qa. P \<cong> Qa \<and> Qa \<cong> Q \<Longrightarrow> P \<leadsto><weakBisimulation> Q
[PROOF STEP]
case(cSym P R)
[PROOF STATE]
proof (state)
this:
\<exists>Q. P \<cong> Q \<and> Q \<cong> R

goal (2 subgoals):
 1. \<And>P Q. \<exists>Qa. P \<cong> Qa \<and> Qa \<cong> Q \<Longrightarrow> \<exists>Qa. Q \<cong> Qa \<and> Qa \<cong> P
 2. \<And>P Q. \<exists>Qa. P \<cong> Qa \<and> Qa \<cong> Q \<Longrightarrow> P \<leadsto><weakBisimulation> Q
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<exists>Q. P \<cong> Q \<and> Q \<cong> R

goal (1 subgoal):
 1. \<exists>Q. R \<cong> Q \<and> Q \<cong> P
[PROOF STEP]
by(auto dest: symmetric)
[PROOF STATE]
proof (state)
this:
\<exists>Q. R \<cong> Q \<and> Q \<cong> P

goal (1 subgoal):
 1. \<And>P Q. \<exists>Qa. P \<cong> Qa \<and> Qa \<cong> Q \<Longrightarrow> P \<leadsto><weakBisimulation> Q
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P Q. \<exists>Qa. P \<cong> Qa \<and> Qa \<cong> Q \<Longrightarrow> P \<leadsto><weakBisimulation> Q
[PROOF STEP]
case(cSim P R)
[PROOF STATE]
proof (state)
this:
\<exists>Q. P \<cong> Q \<and> Q \<cong> R

goal (1 subgoal):
 1. \<And>P Q. \<exists>Qa. P \<cong> Qa \<and> Qa \<cong> Q \<Longrightarrow> P \<leadsto><weakBisimulation> Q
[PROOF STEP]
from \<open>?Prop P R\<close>
[PROOF STATE]
proof (chain)
picking this:
\<exists>Q. P \<cong> Q \<and> Q \<cong> R
[PROOF STEP]
obtain Q where "P \<cong> Q" and "Q \<cong> R"
[PROOF STATE]
proof (prove)
using this:
\<exists>Q. P \<cong> Q \<and> Q \<cong> R

goal (1 subgoal):
 1. (\<And>Q. \<lbrakk>P \<cong> Q; Q \<cong> R\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P \<cong> Q
Q \<cong> R

goal (1 subgoal):
 1. \<And>P Q. \<exists>Qa. P \<cong> Qa \<and> Qa \<cong> Q \<Longrightarrow> P \<leadsto><weakBisimulation> Q
[PROOF STEP]
from \<open>P \<cong> Q\<close>
[PROOF STATE]
proof (chain)
picking this:
P \<cong> Q
[PROOF STEP]
have "P \<leadsto><weakBisimulation> Q"
[PROOF STATE]
proof (prove)
using this:
P \<cong> Q

goal (1 subgoal):
 1. P \<leadsto><weakBisimulation> Q
[PROOF STEP]
by(rule weakCongruenceE)
[PROOF STATE]
proof (state)
this:
P \<leadsto><weakBisimulation> Q

goal (1 subgoal):
 1. \<And>P Q. \<exists>Qa. P \<cong> Qa \<and> Qa \<cong> Q \<Longrightarrow> P \<leadsto><weakBisimulation> Q
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
P \<leadsto><weakBisimulation> Q

goal (1 subgoal):
 1. \<And>P Q. \<exists>Qa. P \<cong> Qa \<and> Qa \<cong> Q \<Longrightarrow> P \<leadsto><weakBisimulation> Q
[PROOF STEP]
from \<open>Q \<cong> R\<close>
[PROOF STATE]
proof (chain)
picking this:
Q \<cong> R
[PROOF STEP]
have "Q \<leadsto><weakBisimulation> R"
[PROOF STATE]
proof (prove)
using this:
Q \<cong> R

goal (1 subgoal):
 1. Q \<leadsto><weakBisimulation> R
[PROOF STEP]
by(rule weakCongruenceE)
[PROOF STATE]
proof (state)
this:
Q \<leadsto><weakBisimulation> R

goal (1 subgoal):
 1. \<And>P Q. \<exists>Qa. P \<cong> Qa \<and> Qa \<cong> Q \<Longrightarrow> P \<leadsto><weakBisimulation> Q
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Q \<leadsto><weakBisimulation> R

goal (1 subgoal):
 1. \<And>P Q. \<exists>Qa. P \<cong> Qa \<and> Qa \<cong> Q \<Longrightarrow> P \<leadsto><weakBisimulation> Q
[PROOF STEP]
from Weak_Bisim.transitive
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?P \<approx> ?Q; ?Q \<approx> ?R\<rbrakk> \<Longrightarrow> ?P \<approx> ?R
[PROOF STEP]
have "weakBisimulation O weakBisimulation \<subseteq> weakBisimulation"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?P \<approx> ?Q; ?Q \<approx> ?R\<rbrakk> \<Longrightarrow> ?P \<approx> ?R

goal (1 subgoal):
 1. weakBisimulation O weakBisimulation \<subseteq> weakBisimulation
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
weakBisimulation O weakBisimulation \<subseteq> weakBisimulation

goal (1 subgoal):
 1. \<And>P Q. \<exists>Qa. P \<cong> Qa \<and> Qa \<cong> Q \<Longrightarrow> P \<leadsto><weakBisimulation> Q
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
P \<leadsto><weakBisimulation> Q
Q \<leadsto><weakBisimulation> R
weakBisimulation O weakBisimulation \<subseteq> weakBisimulation
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
P \<leadsto><weakBisimulation> Q
Q \<leadsto><weakBisimulation> R
weakBisimulation O weakBisimulation \<subseteq> weakBisimulation

goal (1 subgoal):
 1. P \<leadsto><weakBisimulation> R
[PROOF STEP]
using weakBisimulationE(1)
[PROOF STATE]
proof (prove)
using this:
P \<leadsto><weakBisimulation> Q
Q \<leadsto><weakBisimulation> R
weakBisimulation O weakBisimulation \<subseteq> weakBisimulation
?P \<approx> ?Q \<Longrightarrow> ?P \<leadsto>\<^sup>^<weakBisimulation> ?Q

goal (1 subgoal):
 1. P \<leadsto><weakBisimulation> R
[PROOF STEP]
by(rule Weak_Cong_Sim.transitive)
[PROOF STATE]
proof (state)
this:
P \<leadsto><weakBisimulation> R

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P \<cong> R

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bisimWeakCongruence:
  fixes P :: ccs
  and   Q :: ccs

  assumes "P \<sim> Q"

  shows "P \<cong> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<cong> Q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P \<sim> Q

goal (1 subgoal):
 1. P \<cong> Q
[PROOF STEP]
proof(induct rule: weakCongISym)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>P Q. P \<sim> Q \<Longrightarrow> Q \<sim> P
 2. \<And>P Q. P \<sim> Q \<Longrightarrow> P \<leadsto><weakBisimulation> Q
[PROOF STEP]
case(cSym P Q)
[PROOF STATE]
proof (state)
this:
P \<sim> Q

goal (2 subgoals):
 1. \<And>P Q. P \<sim> Q \<Longrightarrow> Q \<sim> P
 2. \<And>P Q. P \<sim> Q \<Longrightarrow> P \<leadsto><weakBisimulation> Q
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
P \<sim> Q

goal (1 subgoal):
 1. Q \<sim> P
[PROOF STEP]
by(rule bisimE)
[PROOF STATE]
proof (state)
this:
Q \<sim> P

goal (1 subgoal):
 1. \<And>P Q. P \<sim> Q \<Longrightarrow> P \<leadsto><weakBisimulation> Q
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P Q. P \<sim> Q \<Longrightarrow> P \<leadsto><weakBisimulation> Q
[PROOF STEP]
case(cSim P Q)
[PROOF STATE]
proof (state)
this:
P \<sim> Q

goal (1 subgoal):
 1. \<And>P Q. P \<sim> Q \<Longrightarrow> P \<leadsto><weakBisimulation> Q
[PROOF STEP]
from \<open>P \<sim> Q\<close>
[PROOF STATE]
proof (chain)
picking this:
P \<sim> Q
[PROOF STEP]
have "P \<leadsto>[bisim] Q"
[PROOF STATE]
proof (prove)
using this:
P \<sim> Q

goal (1 subgoal):
 1. P \<leadsto>[bisim] Q
[PROOF STEP]
by(rule bisimE)
[PROOF STATE]
proof (state)
this:
P \<leadsto>[bisim] Q

goal (1 subgoal):
 1. \<And>P Q. P \<sim> Q \<Longrightarrow> P \<leadsto><weakBisimulation> Q
[PROOF STEP]
hence "P \<leadsto>[weakBisimulation] Q"
[PROOF STATE]
proof (prove)
using this:
P \<leadsto>[bisim] Q

goal (1 subgoal):
 1. P \<leadsto>[weakBisimulation] Q
[PROOF STEP]
using bisimWeakBisimulation
[PROOF STATE]
proof (prove)
using this:
P \<leadsto>[bisim] Q
?P \<sim> ?Q \<Longrightarrow> ?P \<approx> ?Q

goal (1 subgoal):
 1. P \<leadsto>[weakBisimulation] Q
[PROOF STEP]
by(rule_tac monotonic) auto
[PROOF STATE]
proof (state)
this:
P \<leadsto>[weakBisimulation] Q

goal (1 subgoal):
 1. \<And>P Q. P \<sim> Q \<Longrightarrow> P \<leadsto><weakBisimulation> Q
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
P \<leadsto>[weakBisimulation] Q

goal (1 subgoal):
 1. P \<leadsto><weakBisimulation> Q
[PROOF STEP]
by(rule simWeakSim)
[PROOF STATE]
proof (state)
this:
P \<leadsto><weakBisimulation> Q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma structCongWeakCongruence:
  fixes P :: ccs
  and   Q :: ccs

  assumes "P \<equiv>\<^sub>s Q"

  shows "P \<cong> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<cong> Q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P \<equiv>\<^sub>s Q

goal (1 subgoal):
 1. P \<cong> Q
[PROOF STEP]
by(auto intro: bisimWeakCongruence bisimStructCong)


[STATEMENT]
lemma weakCongruenceWeakBisimulation:
  fixes P :: ccs
  and   Q :: ccs

  assumes "P \<cong> Q"

  shows "P \<approx> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<approx> Q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P \<approx> Q
[PROOF STEP]
let ?X = "{(P, Q) | P Q. P \<cong> Q}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P \<approx> Q
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
P \<cong> Q
[PROOF STEP]
have "(P, Q) \<in> ?X"
[PROOF STATE]
proof (prove)
using this:
P \<cong> Q

goal (1 subgoal):
 1. (P, Q) \<in> {(P, Q) |P Q. P \<cong> Q}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(P, Q) \<in> {(P, Q) |P Q. P \<cong> Q}

goal (1 subgoal):
 1. P \<approx> Q
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(P, Q) \<in> {(P, Q) |P Q. P \<cong> Q}

goal (1 subgoal):
 1. P \<approx> Q
[PROOF STEP]
proof(coinduct rule: weakBisimulationCoinduct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {(P, Q) |P Q. P \<cong> Q} \<Longrightarrow> R \<leadsto>\<^sup>^<({(P, Q) |P Q. P \<cong> Q} \<union> weakBisimulation)> S
 2. \<And>R S. (R, S) \<in> {(P, Q) |P Q. P \<cong> Q} \<Longrightarrow> (S, R) \<in> {(P, Q) |P Q. P \<cong> Q}
[PROOF STEP]
case(cSim P Q)
[PROOF STATE]
proof (state)
this:
(P, Q) \<in> {(P, Q) |P Q. P \<cong> Q}

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {(P, Q) |P Q. P \<cong> Q} \<Longrightarrow> R \<leadsto>\<^sup>^<({(P, Q) |P Q. P \<cong> Q} \<union> weakBisimulation)> S
 2. \<And>R S. (R, S) \<in> {(P, Q) |P Q. P \<cong> Q} \<Longrightarrow> (S, R) \<in> {(P, Q) |P Q. P \<cong> Q}
[PROOF STEP]
from \<open>(P, Q) \<in> ?X\<close>
[PROOF STATE]
proof (chain)
picking this:
(P, Q) \<in> {(P, Q) |P Q. P \<cong> Q}
[PROOF STEP]
have "P \<cong> Q"
[PROOF STATE]
proof (prove)
using this:
(P, Q) \<in> {(P, Q) |P Q. P \<cong> Q}

goal (1 subgoal):
 1. P \<cong> Q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P \<cong> Q

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {(P, Q) |P Q. P \<cong> Q} \<Longrightarrow> R \<leadsto>\<^sup>^<({(P, Q) |P Q. P \<cong> Q} \<union> weakBisimulation)> S
 2. \<And>R S. (R, S) \<in> {(P, Q) |P Q. P \<cong> Q} \<Longrightarrow> (S, R) \<in> {(P, Q) |P Q. P \<cong> Q}
[PROOF STEP]
hence "P \<leadsto><weakBisimulation> Q"
[PROOF STATE]
proof (prove)
using this:
P \<cong> Q

goal (1 subgoal):
 1. P \<leadsto><weakBisimulation> Q
[PROOF STEP]
by(rule Weak_Cong.weakCongruenceE)
[PROOF STATE]
proof (state)
this:
P \<leadsto><weakBisimulation> Q

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {(P, Q) |P Q. P \<cong> Q} \<Longrightarrow> R \<leadsto>\<^sup>^<({(P, Q) |P Q. P \<cong> Q} \<union> weakBisimulation)> S
 2. \<And>R S. (R, S) \<in> {(P, Q) |P Q. P \<cong> Q} \<Longrightarrow> (S, R) \<in> {(P, Q) |P Q. P \<cong> Q}
[PROOF STEP]
hence "P \<leadsto><(?X \<union> weakBisimulation)> Q"
[PROOF STATE]
proof (prove)
using this:
P \<leadsto><weakBisimulation> Q

goal (1 subgoal):
 1. P \<leadsto><({(P, Q) |P Q. P \<cong> Q} \<union> weakBisimulation)> Q
[PROOF STEP]
by(force intro: Weak_Cong_Sim.weakMonotonic)
[PROOF STATE]
proof (state)
this:
P \<leadsto><({(P, Q) |P Q. P \<cong> Q} \<union> weakBisimulation)> Q

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {(P, Q) |P Q. P \<cong> Q} \<Longrightarrow> R \<leadsto>\<^sup>^<({(P, Q) |P Q. P \<cong> Q} \<union> weakBisimulation)> S
 2. \<And>R S. (R, S) \<in> {(P, Q) |P Q. P \<cong> Q} \<Longrightarrow> (S, R) \<in> {(P, Q) |P Q. P \<cong> Q}
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
P \<leadsto><({(P, Q) |P Q. P \<cong> Q} \<union> weakBisimulation)> Q

goal (1 subgoal):
 1. P \<leadsto>\<^sup>^<({(P, Q) |P Q. P \<cong> Q} \<union> weakBisimulation)> Q
[PROOF STEP]
by(rule weakCongSimWeakSim)
[PROOF STATE]
proof (state)
this:
P \<leadsto>\<^sup>^<({(P, Q) |P Q. P \<cong> Q} \<union> weakBisimulation)> Q

goal (1 subgoal):
 1. \<And>R S. (R, S) \<in> {(P, Q) |P Q. P \<cong> Q} \<Longrightarrow> (S, R) \<in> {(P, Q) |P Q. P \<cong> Q}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>R S. (R, S) \<in> {(P, Q) |P Q. P \<cong> Q} \<Longrightarrow> (S, R) \<in> {(P, Q) |P Q. P \<cong> Q}
[PROOF STEP]
case(cSym P Q)
[PROOF STATE]
proof (state)
this:
(P, Q) \<in> {(P, Q) |P Q. P \<cong> Q}

goal (1 subgoal):
 1. \<And>R S. (R, S) \<in> {(P, Q) |P Q. P \<cong> Q} \<Longrightarrow> (S, R) \<in> {(P, Q) |P Q. P \<cong> Q}
[PROOF STEP]
from \<open>(P, Q) \<in> ?X\<close>
[PROOF STATE]
proof (chain)
picking this:
(P, Q) \<in> {(P, Q) |P Q. P \<cong> Q}
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(P, Q) \<in> {(P, Q) |P Q. P \<cong> Q}

goal (1 subgoal):
 1. (Q, P) \<in> {(P, Q) |P Q. P \<cong> Q}
[PROOF STEP]
by(blast dest: symmetric)
[PROOF STATE]
proof (state)
this:
(Q, P) \<in> {(P, Q) |P Q. P \<cong> Q}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P \<approx> Q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma LeftDerivationLadder_length_1:
  assumes ladder: "LeftDerivationLadder \<alpha> D L \<gamma>"
  assumes singleton_L: "length L = 1"
  shows "LeftDerivationFix \<alpha> (ladder_i L 0) D (ladder_last_j L) \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LeftDerivationFix \<alpha> (ladder_i L 0) D (ladder_last_j L) \<gamma>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. LeftDerivationFix \<alpha> (ladder_i L 0) D (ladder_last_j L) \<gamma>
[PROOF STEP]
have ldfix: "LeftDerivationFix \<alpha> (ladder_i L 0) (take (ladder_n L 0) D) (ladder_j L 0)
    (ladder_\<gamma> \<alpha> D L 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LeftDerivationFix \<alpha> (ladder_i L 0) (take (ladder_n L 0) D) (ladder_j L 0) (ladder_\<gamma> \<alpha> D L 0)
[PROOF STEP]
using ladder LeftDerivationLadder_def
[PROOF STATE]
proof (prove)
using this:
LeftDerivationLadder \<alpha> D L \<gamma>
LeftDerivationLadder ?a ?D ?L ?b = (LeftDerivation ?a ?D ?b \<and> is_ladder ?D ?L \<and> LeftDerivationFix ?a (ladder_i ?L 0) (take (ladder_n ?L 0) ?D) (ladder_j ?L 0) (ladder_\<gamma> ?a ?D ?L 0) \<and> LeftDerivationIntros ?a ?D ?L)

goal (1 subgoal):
 1. LeftDerivationFix \<alpha> (ladder_i L 0) (take (ladder_n L 0) D) (ladder_j L 0) (ladder_\<gamma> \<alpha> D L 0)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
LeftDerivationFix \<alpha> (ladder_i L 0) (take (ladder_n L 0) D) (ladder_j L 0) (ladder_\<gamma> \<alpha> D L 0)

goal (1 subgoal):
 1. LeftDerivationFix \<alpha> (ladder_i L 0) D (ladder_last_j L) \<gamma>
[PROOF STEP]
have ladder_n_0: "ladder_n L 0 = length D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ladder_n L 0 = length D
[PROOF STEP]
using ladder singleton_L
[PROOF STATE]
proof (prove)
using this:
LeftDerivationLadder \<alpha> D L \<gamma>
length L = 1

goal (1 subgoal):
 1. ladder_n L 0 = length D
[PROOF STEP]
by (metis LeftDerivationLadder_def One_nat_def diff_Suc_1 is_ladder_def ladder_last_n_intro)
[PROOF STATE]
proof (state)
this:
ladder_n L 0 = length D

goal (1 subgoal):
 1. LeftDerivationFix \<alpha> (ladder_i L 0) D (ladder_last_j L) \<gamma>
[PROOF STEP]
from ldfix ladder_n_0 ladder singleton_L
[PROOF STATE]
proof (chain)
picking this:
LeftDerivationFix \<alpha> (ladder_i L 0) (take (ladder_n L 0) D) (ladder_j L 0) (ladder_\<gamma> \<alpha> D L 0)
ladder_n L 0 = length D
LeftDerivationLadder \<alpha> D L \<gamma>
length L = 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
LeftDerivationFix \<alpha> (ladder_i L 0) (take (ladder_n L 0) D) (ladder_j L 0) (ladder_\<gamma> \<alpha> D L 0)
ladder_n L 0 = length D
LeftDerivationLadder \<alpha> D L \<gamma>
length L = 1

goal (1 subgoal):
 1. LeftDerivationFix \<alpha> (ladder_i L 0) D (ladder_last_j L) \<gamma>
[PROOF STEP]
by (metis Derivation_unique_dest LeftDerivationLadder_def
      LeftDerivationLadder_implies_LeftDerivation_at_index LeftDerivationLadder_ladder_n_bound
      LeftDerivation_implies_Derivation One_nat_def diff_Suc_1 ladder_last_j_def take_all
      zero_less_one)
[PROOF STATE]
proof (state)
this:
LeftDerivationFix \<alpha> (ladder_i L 0) D (ladder_last_j L) \<gamma>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma LeftDerivationFix_from_singleton_helper:
  assumes "LeftDerivationFix [A] 0 D (length u) (u @ [B] @ v)"
  shows "D = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. D = []
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. D = []
[PROOF STEP]
from iffD1[OF LeftDerivationFix_def assms]
[PROOF STATE]
proof (chain)
picking this:
is_sentence [A] \<and> is_sentence (u @ [B] @ v) \<and> LeftDerivation [A] D (u @ [B] @ v) \<and> 0 < length [A] \<and> length u < length (u @ [B] @ v) \<and> [A] ! 0 = (u @ [B] @ v) ! length u \<and> (\<exists>E F. D = E @ derivation_shift F 0 (Suc (length u)) \<and> LeftDerivation (take 0 [A]) E (take (length u) (u @ [B] @ v)) \<and> LeftDerivation (drop (Suc 0) [A]) F (drop (Suc (length u)) (u @ [B] @ v)))
[PROOF STEP]
obtain E F where EF:
    "is_sentence [A] \<and>
     is_sentence (u @ [B] @ v) \<and>
     LeftDerivation [A] D (u @ [B] @ v) \<and>
     0 < length [A] \<and>
     length u < length (u @ [B] @ v) \<and>
     [A] ! 0 = (u @ [B] @ v) ! length u \<and>
     D = E @ derivation_shift F 0 (Suc (length u)) \<and>
     LeftDerivation (take 0 [A]) E (take (length u) (u @ [B] @ v)) \<and>
     LeftDerivation (drop (Suc 0) [A]) F (drop (Suc (length u)) (u @ [B] @ v))"
[PROOF STATE]
proof (prove)
using this:
is_sentence [A] \<and> is_sentence (u @ [B] @ v) \<and> LeftDerivation [A] D (u @ [B] @ v) \<and> 0 < length [A] \<and> length u < length (u @ [B] @ v) \<and> [A] ! 0 = (u @ [B] @ v) ! length u \<and> (\<exists>E F. D = E @ derivation_shift F 0 (Suc (length u)) \<and> LeftDerivation (take 0 [A]) E (take (length u) (u @ [B] @ v)) \<and> LeftDerivation (drop (Suc 0) [A]) F (drop (Suc (length u)) (u @ [B] @ v)))

goal (1 subgoal):
 1. (\<And>E F. is_sentence [A] \<and> is_sentence (u @ [B] @ v) \<and> LeftDerivation [A] D (u @ [B] @ v) \<and> 0 < length [A] \<and> length u < length (u @ [B] @ v) \<and> [A] ! 0 = (u @ [B] @ v) ! length u \<and> D = E @ derivation_shift F 0 (Suc (length u)) \<and> LeftDerivation (take 0 [A]) E (take (length u) (u @ [B] @ v)) \<and> LeftDerivation (drop (Suc 0) [A]) F (drop (Suc (length u)) (u @ [B] @ v)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
is_sentence [A] \<and> is_sentence (u @ [B] @ v) \<and> LeftDerivation [A] D (u @ [B] @ v) \<and> 0 < length [A] \<and> length u < length (u @ [B] @ v) \<and> [A] ! 0 = (u @ [B] @ v) ! length u \<and> D = E @ derivation_shift F 0 (Suc (length u)) \<and> LeftDerivation (take 0 [A]) E (take (length u) (u @ [B] @ v)) \<and> LeftDerivation (drop (Suc 0) [A]) F (drop (Suc (length u)) (u @ [B] @ v))

goal (1 subgoal):
 1. D = []
[PROOF STEP]
from EF
[PROOF STATE]
proof (chain)
picking this:
is_sentence [A] \<and> is_sentence (u @ [B] @ v) \<and> LeftDerivation [A] D (u @ [B] @ v) \<and> 0 < length [A] \<and> length u < length (u @ [B] @ v) \<and> [A] ! 0 = (u @ [B] @ v) ! length u \<and> D = E @ derivation_shift F 0 (Suc (length u)) \<and> LeftDerivation (take 0 [A]) E (take (length u) (u @ [B] @ v)) \<and> LeftDerivation (drop (Suc 0) [A]) F (drop (Suc (length u)) (u @ [B] @ v))
[PROOF STEP]
have E: "E = []"
[PROOF STATE]
proof (prove)
using this:
is_sentence [A] \<and> is_sentence (u @ [B] @ v) \<and> LeftDerivation [A] D (u @ [B] @ v) \<and> 0 < length [A] \<and> length u < length (u @ [B] @ v) \<and> [A] ! 0 = (u @ [B] @ v) ! length u \<and> D = E @ derivation_shift F 0 (Suc (length u)) \<and> LeftDerivation (take 0 [A]) E (take (length u) (u @ [B] @ v)) \<and> LeftDerivation (drop (Suc 0) [A]) F (drop (Suc (length u)) (u @ [B] @ v))

goal (1 subgoal):
 1. E = []
[PROOF STEP]
by (metis Derivation.elims(2) Derives1_split LeftDerivation_implies_Derivation
      Nil_is_append_conv list.distinct(1) take_0)
[PROOF STATE]
proof (state)
this:
E = []

goal (1 subgoal):
 1. D = []
[PROOF STEP]
from EF
[PROOF STATE]
proof (chain)
picking this:
is_sentence [A] \<and> is_sentence (u @ [B] @ v) \<and> LeftDerivation [A] D (u @ [B] @ v) \<and> 0 < length [A] \<and> length u < length (u @ [B] @ v) \<and> [A] ! 0 = (u @ [B] @ v) ! length u \<and> D = E @ derivation_shift F 0 (Suc (length u)) \<and> LeftDerivation (take 0 [A]) E (take (length u) (u @ [B] @ v)) \<and> LeftDerivation (drop (Suc 0) [A]) F (drop (Suc (length u)) (u @ [B] @ v))
[PROOF STEP]
have F: "F = []"
[PROOF STATE]
proof (prove)
using this:
is_sentence [A] \<and> is_sentence (u @ [B] @ v) \<and> LeftDerivation [A] D (u @ [B] @ v) \<and> 0 < length [A] \<and> length u < length (u @ [B] @ v) \<and> [A] ! 0 = (u @ [B] @ v) ! length u \<and> D = E @ derivation_shift F 0 (Suc (length u)) \<and> LeftDerivation (take 0 [A]) E (take (length u) (u @ [B] @ v)) \<and> LeftDerivation (drop (Suc 0) [A]) F (drop (Suc (length u)) (u @ [B] @ v))

goal (1 subgoal):
 1. F = []
[PROOF STEP]
by (metis E LeftDerivation.simps(1) LeftDerivation_ge_take LeftDerivation_implies_Derivation
      append_eq_conv_conj derivation_ge_shift is_word_Derivation length_Cons length_derivation_shift
      list.size(3) nth_Cons_0 nth_append self_append_conv2 take_0)
[PROOF STATE]
proof (state)
this:
F = []

goal (1 subgoal):
 1. D = []
[PROOF STEP]
from EF E F
[PROOF STATE]
proof (chain)
picking this:
is_sentence [A] \<and> is_sentence (u @ [B] @ v) \<and> LeftDerivation [A] D (u @ [B] @ v) \<and> 0 < length [A] \<and> length u < length (u @ [B] @ v) \<and> [A] ! 0 = (u @ [B] @ v) ! length u \<and> D = E @ derivation_shift F 0 (Suc (length u)) \<and> LeftDerivation (take 0 [A]) E (take (length u) (u @ [B] @ v)) \<and> LeftDerivation (drop (Suc 0) [A]) F (drop (Suc (length u)) (u @ [B] @ v))
E = []
F = []
[PROOF STEP]
show "D = []"
[PROOF STATE]
proof (prove)
using this:
is_sentence [A] \<and> is_sentence (u @ [B] @ v) \<and> LeftDerivation [A] D (u @ [B] @ v) \<and> 0 < length [A] \<and> length u < length (u @ [B] @ v) \<and> [A] ! 0 = (u @ [B] @ v) ! length u \<and> D = E @ derivation_shift F 0 (Suc (length u)) \<and> LeftDerivation (take 0 [A]) E (take (length u) (u @ [B] @ v)) \<and> LeftDerivation (drop (Suc 0) [A]) F (drop (Suc (length u)) (u @ [B] @ v))
E = []
F = []

goal (1 subgoal):
 1. D = []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
D = []

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma LeftDerivationFix_from_singleton:
  assumes "LeftDerivationFix [A] i D j \<gamma>"
  shows "D = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. D = []
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. D = []
[PROOF STEP]
have "\<exists> u B v. splits_at \<gamma> j u B v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>u B v. splits_at \<gamma> j u B v
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
LeftDerivationFix [A] i D j \<gamma>

goal (1 subgoal):
 1. \<exists>u B v. splits_at \<gamma> j u B v
[PROOF STEP]
using LeftDerivationFix_splits_at_derives
[PROOF STATE]
proof (prove)
using this:
LeftDerivationFix [A] i D j \<gamma>
LeftDerivationFix ?a ?i ?D ?j ?b \<Longrightarrow> \<exists>U a1 a2 b1 b2. splits_at ?a ?i a1 U a2 \<and> splits_at ?b ?j b1 U b2 \<and> derives a1 b1 \<and> derives a2 b2

goal (1 subgoal):
 1. \<exists>u B v. splits_at \<gamma> j u B v
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>u B v. splits_at \<gamma> j u B v

goal (1 subgoal):
 1. D = []
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>u B v. splits_at \<gamma> j u B v
[PROOF STEP]
obtain u B v where s: "splits_at \<gamma> j u B v"
[PROOF STATE]
proof (prove)
using this:
\<exists>u B v. splits_at \<gamma> j u B v

goal (1 subgoal):
 1. (\<And>u B v. splits_at \<gamma> j u B v \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
splits_at \<gamma> j u B v

goal (1 subgoal):
 1. D = []
[PROOF STEP]
from s
[PROOF STATE]
proof (chain)
picking this:
splits_at \<gamma> j u B v
[PROOF STEP]
have s1: "\<gamma> = u @ [B] @ v"
[PROOF STATE]
proof (prove)
using this:
splits_at \<gamma> j u B v

goal (1 subgoal):
 1. \<gamma> = u @ [B] @ v
[PROOF STEP]
using splits_at_combine
[PROOF STATE]
proof (prove)
using this:
splits_at \<gamma> j u B v
splits_at ?\<delta> ?i ?\<alpha> ?N ?\<beta> \<Longrightarrow> ?\<delta> = ?\<alpha> @ [?N] @ ?\<beta>

goal (1 subgoal):
 1. \<gamma> = u @ [B] @ v
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<gamma> = u @ [B] @ v

goal (1 subgoal):
 1. D = []
[PROOF STEP]
from s
[PROOF STATE]
proof (chain)
picking this:
splits_at \<gamma> j u B v
[PROOF STEP]
have s2: "j = length u"
[PROOF STATE]
proof (prove)
using this:
splits_at \<gamma> j u B v

goal (1 subgoal):
 1. j = length u
[PROOF STEP]
using splits_at_def
[PROOF STATE]
proof (prove)
using this:
splits_at \<gamma> j u B v
splits_at ?\<delta> ?i ?\<alpha> ?N ?\<beta> = (?i < length ?\<delta> \<and> ?\<alpha> = take ?i ?\<delta> \<and> ?N = ?\<delta> ! ?i \<and> ?\<beta> = drop (Suc ?i) ?\<delta>)

goal (1 subgoal):
 1. j = length u
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
j = length u

goal (1 subgoal):
 1. D = []
[PROOF STEP]
from assms s1 s2 LeftDerivationFix_from_singleton_helper
[PROOF STATE]
proof (chain)
picking this:
LeftDerivationFix [A] i D j \<gamma>
\<gamma> = u @ [B] @ v
j = length u
LeftDerivationFix [?A] 0 ?D (length ?u) (?u @ [?B] @ ?v) \<Longrightarrow> ?D = []
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
LeftDerivationFix [A] i D j \<gamma>
\<gamma> = u @ [B] @ v
j = length u
LeftDerivationFix [?A] 0 ?D (length ?u) (?u @ [?B] @ ?v) \<Longrightarrow> ?D = []

goal (1 subgoal):
 1. D = []
[PROOF STEP]
by (metis LeftDerivationFix_def length_Cons less_Suc0 list.size(3))
[PROOF STATE]
proof (state)
this:
D = []

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma LeftDerivationLadder_ladder_\<gamma>_last:
  assumes "LeftDerivationLadder \<alpha> D L \<gamma>"
  shows "\<gamma> = ladder_\<gamma> \<alpha> D L (length L - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<gamma> = ladder_\<gamma> \<alpha> D L (length L - 1)
[PROOF STEP]
by (metis Derive LeftDerivationLadder_def LeftDerivation_implies_Derivation One_nat_def assms
  is_ladder_def last_ladder_\<gamma>)