[STATEMENT]
lemma istate_\<Delta>0:
assumes B: "B vl vl1"
shows "\<Delta>0 istate vl istate vl1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Delta>0 istate vl istate vl1
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
B vl vl1

goal (1 subgoal):
 1. \<Delta>0 istate vl istate vl1
[PROOF STEP]
unfolding \<Delta>0_def B_def istate_def
[PROOF STATE]
proof (prove)
using this:
length vl = length vl1

goal (1 subgoal):
 1. AID \<notin> set (serverApiIDs \<lparr>admin = emptyUserID, pendingUReqs = [], userReq = \<lambda>uID. emptyRequestInfo, userIDs = [], user = \<lambda>uID. emptyUser, pass = \<lambda>uID. emptyPass, pendingFReqs = \<lambda>uID. [], friendReq = \<lambda>uID uID'. emptyRequestInfo, friendIDs = \<lambda>uID. [], sentOuterFriendIDs = \<lambda>uID. [], recvOuterFriendIDs = \<lambda>uID. [], postIDs = [], post = \<lambda>papID. emptyPost, owner = \<lambda>pID. emptyUserID, vis = \<lambda>pID. FriendV, pendingSApiReqs = [], sApiReq = \<lambda>aID. emptyRequestInfo, serverApiIDs = [], serverPass = \<lambda>aID. emptyPass, outerPostIDs = \<lambda>aID. [], outerPost = \<lambda>aID papID. emptyPost, outerOwner = \<lambda>aID papID. emptyUserID, outerVis = \<lambda>aID pID. FriendV, pendingCApiReqs = [], cApiReq = \<lambda>aID. emptyRequestInfo, clientApiIDs = [], clientPass = \<lambda>aID. emptyPass, sharedWith = \<lambda>pID. []\<rparr>) \<and> \<lparr>admin = emptyUserID, pendingUReqs = [], userReq = \<lambda>uID. emptyRequestInfo, userIDs = [], user = \<lambda>uID. emptyUser, pass = \<lambda>uID. emptyPass, pendingFReqs = \<lambda>uID. [], friendReq = \<lambda>uID uID'. emptyRequestInfo, friendIDs = \<lambda>uID. [], sentOuterFriendIDs = \<lambda>uID. [], recvOuterFriendIDs = \<lambda>uID. [], postIDs = [], post = \<lambda>papID. emptyPost, owner = \<lambda>pID. emptyUserID, vis = \<lambda>pID. FriendV, pendingSApiReqs = [], sApiReq = \<lambda>aID. emptyRequestInfo, serverApiIDs = [], serverPass = \<lambda>aID. emptyPass, outerPostIDs = \<lambda>aID. [], outerPost = \<lambda>aID papID. emptyPost, outerOwner = \<lambda>aID papID. emptyUserID, outerVis = \<lambda>aID pID. FriendV, pendingCApiReqs = [], cApiReq = \<lambda>aID. emptyRequestInfo, clientApiIDs = [], clientPass = \<lambda>aID. emptyPass, sharedWith = \<lambda>pID. []\<rparr> = \<lparr>admin = emptyUserID, pendingUReqs = [], userReq = \<lambda>uID. emptyRequestInfo, userIDs = [], user = \<lambda>uID. emptyUser, pass = \<lambda>uID. emptyPass, pendingFReqs = \<lambda>uID. [], friendReq = \<lambda>uID uID'. emptyRequestInfo, friendIDs = \<lambda>uID. [], sentOuterFriendIDs = \<lambda>uID. [], recvOuterFriendIDs = \<lambda>uID. [], postIDs = [], post = \<lambda>papID. emptyPost, owner = \<lambda>pID. emptyUserID, vis = \<lambda>pID. FriendV, pendingSApiReqs = [], sApiReq = \<lambda>aID. emptyRequestInfo, serverApiIDs = [], serverPass = \<lambda>aID. emptyPass, outerPostIDs = \<lambda>aID. [], outerPost = \<lambda>aID papID. emptyPost, outerOwner = \<lambda>aID papID. emptyUserID, outerVis = \<lambda>aID pID. FriendV, pendingCApiReqs = [], cApiReq = \<lambda>aID. emptyRequestInfo, clientApiIDs = [], clientPass = \<lambda>aID. emptyPass, sharedWith = \<lambda>pID. []\<rparr> \<and> length vl = length vl1
[PROOF STEP]
by auto


[STATEMENT]
lemma unwind_cont_\<Delta>0: "unwind_cont \<Delta>0 {\<Delta>0,\<Delta>1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unwind_cont \<Delta>0 {\<Delta>0, \<Delta>1}
[PROOF STEP]
proof(rule, simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s vl s1 vl1. \<lbrakk>reachNT s; reach s1; \<Delta>0 s vl s1 vl1\<rbrakk> \<Longrightarrow> iaction (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s vl s1 vl1 \<or> (vl = [] \<longrightarrow> vl1 = []) \<and> reaction (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s vl s1 vl1
[PROOF STEP]
let ?\<Delta> = "\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s vl s1 vl1. \<lbrakk>reachNT s; reach s1; \<Delta>0 s vl s1 vl1\<rbrakk> \<Longrightarrow> iaction (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s vl s1 vl1 \<or> (vl = [] \<longrightarrow> vl1 = []) \<and> reaction (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s vl s1 vl1
[PROOF STEP]
fix s s1 :: state and vl vl1 :: "value list"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s vl s1 vl1. \<lbrakk>reachNT s; reach s1; \<Delta>0 s vl s1 vl1\<rbrakk> \<Longrightarrow> iaction (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s vl s1 vl1 \<or> (vl = [] \<longrightarrow> vl1 = []) \<and> reaction (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s vl s1 vl1
[PROOF STEP]
assume rsT: "reachNT s" and rs1: "reach s1" and "\<Delta>0 s vl s1 vl1"
[PROOF STATE]
proof (state)
this:
reachNT s
reach s1
\<Delta>0 s vl s1 vl1

goal (1 subgoal):
 1. \<And>s vl s1 vl1. \<lbrakk>reachNT s; reach s1; \<Delta>0 s vl s1 vl1\<rbrakk> \<Longrightarrow> iaction (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s vl s1 vl1 \<or> (vl = [] \<longrightarrow> vl1 = []) \<and> reaction (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s vl s1 vl1
[PROOF STEP]
hence rs: "reach s" and ss1: "s1 = s" and l: "length vl = length vl1"
  and AID: "\<not> AID \<in>\<in> serverApiIDs s"
[PROOF STATE]
proof (prove)
using this:
reachNT s
reach s1
\<Delta>0 s vl s1 vl1

goal (1 subgoal):
 1. (reach s &&& s1 = s) &&& length vl = length vl1 &&& AID \<notin> set (serverApiIDs s)
[PROOF STEP]
using reachNT_reach
[PROOF STATE]
proof (prove)
using this:
reachNT s
reach s1
\<Delta>0 s vl s1 vl1
reachNT ?s \<Longrightarrow> reach ?s

goal (1 subgoal):
 1. (reach s &&& s1 = s) &&& length vl = length vl1 &&& AID \<notin> set (serverApiIDs s)
[PROOF STEP]
unfolding \<Delta>0_def
[PROOF STATE]
proof (prove)
using this:
reachNT s
reach s1
AID \<notin> set (serverApiIDs s) \<and> s = s1 \<and> length vl = length vl1
reachNT ?s \<Longrightarrow> reach ?s

goal (1 subgoal):
 1. (reach s &&& s1 = s) &&& length vl = length vl1 &&& AID \<notin> set (serverApiIDs s)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
reach s
s1 = s
length vl = length vl1
AID \<notin> set (serverApiIDs s)

goal (1 subgoal):
 1. \<And>s vl s1 vl1. \<lbrakk>reachNT s; reach s1; \<Delta>0 s vl s1 vl1\<rbrakk> \<Longrightarrow> iaction (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s vl s1 vl1 \<or> (vl = [] \<longrightarrow> vl1 = []) \<and> reaction (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s vl s1 vl1
[PROOF STEP]
show "iaction ?\<Delta> s vl s1 vl1 \<or>
        ((vl = [] \<longrightarrow> vl1 = []) \<and> reaction ?\<Delta> s vl s1 vl1)" (is "?iact \<or> (_ \<and> ?react)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iaction (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s vl s1 vl1 \<or> (vl = [] \<longrightarrow> vl1 = []) \<and> reaction (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s vl s1 vl1
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. iaction (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s vl s1 vl1 \<or> (vl = [] \<longrightarrow> vl1 = []) \<and> reaction (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s vl s1 vl1
[PROOF STEP]
have ?react
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reaction (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s vl s1 vl1
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a ou s' vl'. \<lbrakk>step s a = (ou, s'); \<not> T (Trans s a ou s'); consume (Trans s a ou s') vl vl'\<rbrakk> \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s s1 vl1 a ou s' vl' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s s1 vl1 a ou s' vl'
[PROOF STEP]
fix a :: act and ou :: out and s' :: state and vl'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a ou s' vl'. \<lbrakk>step s a = (ou, s'); \<not> T (Trans s a ou s'); consume (Trans s a ou s') vl vl'\<rbrakk> \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s s1 vl1 a ou s' vl' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s s1 vl1 a ou s' vl'
[PROOF STEP]
let ?trn = "Trans s a ou s'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a ou s' vl'. \<lbrakk>step s a = (ou, s'); \<not> T (Trans s a ou s'); consume (Trans s a ou s') vl vl'\<rbrakk> \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s s1 vl1 a ou s' vl' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s s1 vl1 a ou s' vl'
[PROOF STEP]
let ?trn1 = "Trans s1 a ou s'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a ou s' vl'. \<lbrakk>step s a = (ou, s'); \<not> T (Trans s a ou s'); consume (Trans s a ou s') vl vl'\<rbrakk> \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s s1 vl1 a ou s' vl' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s s1 vl1 a ou s' vl'
[PROOF STEP]
assume step: "step s a = (ou, s')" and T: "\<not> T ?trn" and c: "consume ?trn vl vl'"
[PROOF STATE]
proof (state)
this:
step s a = (ou, s')
\<not> T (Trans s a ou s')
consume (Trans s a ou s') vl vl'

goal (1 subgoal):
 1. \<And>a ou s' vl'. \<lbrakk>step s a = (ou, s'); \<not> T (Trans s a ou s'); consume (Trans s a ou s') vl vl'\<rbrakk> \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s s1 vl1 a ou s' vl' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s s1 vl1 a ou s' vl'
[PROOF STEP]
show "match ?\<Delta> s s1 vl1 a ou s' vl' \<or> ignore ?\<Delta> s s1 vl1 a ou s' vl'" (is "?match \<or> ?ignore")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. match (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s s1 vl1 a ou s' vl' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s s1 vl1 a ou s' vl'
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. match (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s s1 vl1 a ou s' vl' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s s1 vl1 a ou s' vl'
[PROOF STEP]
have \<phi>: "\<not> \<phi> ?trn"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> \<phi> (Trans s a ou s')
[PROOF STEP]
using AID step
[PROOF STATE]
proof (prove)
using this:
AID \<notin> set (serverApiIDs s)
step s a = (ou, s')

goal (1 subgoal):
 1. \<not> \<phi> (Trans s a ou s')
[PROOF STEP]
unfolding \<phi>_def2
[PROOF STATE]
proof (prove)
using this:
AID \<notin> set (serverApiIDs s)
step s a = (ou, s')

goal (1 subgoal):
 1. \<nexists>uid p pst vs. a = COMact (comReceivePost AID p PID pst uid vs) \<and> ou = outOK
[PROOF STEP]
(* [OF step] *)
[PROOF STATE]
proof (prove)
using this:
AID \<notin> set (serverApiIDs s)
step s a = (ou, s')

goal (1 subgoal):
 1. \<nexists>uid p pst vs. a = COMact (comReceivePost AID p PID pst uid vs) \<and> ou = outOK
[PROOF STEP]
by (auto simp: u_defs com_defs)
[PROOF STATE]
proof (state)
this:
\<not> \<phi> (Trans s a ou s')

goal (1 subgoal):
 1. match (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s s1 vl1 a ou s' vl' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s s1 vl1 a ou s' vl'
[PROOF STEP]
hence vl': "vl' = vl"
[PROOF STATE]
proof (prove)
using this:
\<not> \<phi> (Trans s a ou s')

goal (1 subgoal):
 1. vl' = vl
[PROOF STEP]
using c \<phi>
[PROOF STATE]
proof (prove)
using this:
\<not> \<phi> (Trans s a ou s')
consume (Trans s a ou s') vl vl'
\<not> \<phi> (Trans s a ou s')

goal (1 subgoal):
 1. vl' = vl
[PROOF STEP]
unfolding consume_def
[PROOF STATE]
proof (prove)
using this:
\<not> \<phi> (Trans s a ou s')
if \<phi> (Trans s a ou s') then vl \<noteq> [] \<and> f (Trans s a ou s') = hd vl \<and> vl' = tl vl else vl' = vl
\<not> \<phi> (Trans s a ou s')

goal (1 subgoal):
 1. vl' = vl
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vl' = vl

goal (1 subgoal):
 1. match (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s s1 vl1 a ou s' vl' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s s1 vl1 a ou s' vl'
[PROOF STEP]
have ?match
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. match (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s s1 vl1 a ou s' vl'
[PROOF STEP]
proof(cases "\<exists> p. a = COMact (comConnectServer AID p) \<and> ou = outOK")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s s1 vl1 a ou s' vl'
 2. \<nexists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s s1 vl1 a ou s' vl'
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<exists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK

goal (2 subgoals):
 1. \<exists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s s1 vl1 a ou s' vl'
 2. \<nexists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s s1 vl1 a ou s' vl'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK
[PROOF STEP]
obtain p where a: "a = COMact (comConnectServer AID p)" and ou: "ou = outOK"
[PROOF STATE]
proof (prove)
using this:
\<exists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>a = COMact (comConnectServer AID p); ou = outOK\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a = COMact (comConnectServer AID p)
ou = outOK

goal (2 subgoals):
 1. \<exists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s s1 vl1 a ou s' vl'
 2. \<nexists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s s1 vl1 a ou s' vl'
[PROOF STEP]
have AID': "AID \<in>\<in> serverApiIDs s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AID \<in>\<in> serverApiIDs s'
[PROOF STEP]
using step AID
[PROOF STATE]
proof (prove)
using this:
step s a = (ou, s')
AID \<notin> set (serverApiIDs s)

goal (1 subgoal):
 1. AID \<in>\<in> serverApiIDs s'
[PROOF STEP]
unfolding a ou
[PROOF STATE]
proof (prove)
using this:
step s (COMact (comConnectServer AID p)) = (outOK, s')
AID \<notin> set (serverApiIDs s)

goal (1 subgoal):
 1. AID \<in>\<in> serverApiIDs s'
[PROOF STEP]
by (auto simp: com_defs)
[PROOF STATE]
proof (state)
this:
AID \<in>\<in> serverApiIDs s'

goal (2 subgoals):
 1. \<exists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s s1 vl1 a ou s' vl'
 2. \<nexists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s s1 vl1 a ou s' vl'
[PROOF STEP]
note uid = reachNT_state[OF rsT]
[PROOF STATE]
proof (state)
this:
\<not> (\<exists>uid\<in>UIDs. uid \<in>\<in> userIDs s \<and> PID \<in>\<in> outerPostIDs s AID \<and> (uid = admin s \<or> (AID, outerOwner s AID PID) \<in>\<in> recvOuterFriendIDs s uid \<or> outerVis s AID PID = PublicV))

goal (2 subgoals):
 1. \<exists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s s1 vl1 a ou s' vl'
 2. \<nexists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s s1 vl1 a ou s' vl'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. match (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s s1 vl1 a ou s' vl'
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. validTrans (Trans s1 ?a1.0 ?ou1.0 ?s1')
 2. consume (Trans s1 ?a1.0 ?ou1.0 ?s1') vl1 ?vl1'
 3. \<gamma> (Trans s a ou s') = \<gamma> (Trans s1 ?a1.0 ?ou1.0 ?s1')
 4. \<gamma> (Trans s a ou s') \<Longrightarrow> g (Trans s a ou s') = g (Trans s1 ?a1.0 ?ou1.0 ?s1')
 5. \<Delta>0 s' vl' ?s1' ?vl1' \<or> \<Delta>1 s' vl' ?s1' ?vl1'
[PROOF STEP]
show "validTrans ?trn1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. validTrans (Trans s1 a ou s')
[PROOF STEP]
unfolding ss1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. validTrans (Trans s a ou s')
[PROOF STEP]
using step
[PROOF STATE]
proof (prove)
using this:
step s a = (ou, s')

goal (1 subgoal):
 1. validTrans (Trans s a ou s')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
validTrans (Trans s1 a ou s')

goal (4 subgoals):
 1. consume (Trans s1 a ou s') vl1 ?vl1'
 2. \<gamma> (Trans s a ou s') = \<gamma> (Trans s1 a ou s')
 3. \<gamma> (Trans s a ou s') \<Longrightarrow> g (Trans s a ou s') = g (Trans s1 a ou s')
 4. \<Delta>0 s' vl' s' ?vl1' \<or> \<Delta>1 s' vl' s' ?vl1'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. consume (Trans s1 a ou s') vl1 ?vl1'
 2. \<gamma> (Trans s a ou s') = \<gamma> (Trans s1 a ou s')
 3. \<gamma> (Trans s a ou s') \<Longrightarrow> g (Trans s a ou s') = g (Trans s1 a ou s')
 4. \<Delta>0 s' vl' s' ?vl1' \<or> \<Delta>1 s' vl' s' ?vl1'
[PROOF STEP]
show "consume ?trn1 vl1 vl1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. consume (Trans s1 a ou s') vl1 vl1
[PROOF STEP]
using \<phi>
[PROOF STATE]
proof (prove)
using this:
\<not> \<phi> (Trans s a ou s')

goal (1 subgoal):
 1. consume (Trans s1 a ou s') vl1 vl1
[PROOF STEP]
unfolding consume_def ss1
[PROOF STATE]
proof (prove)
using this:
\<not> \<phi> (Trans s a ou s')

goal (1 subgoal):
 1. if \<phi> (Trans s a ou s') then vl1 \<noteq> [] \<and> f (Trans s a ou s') = hd vl1 \<and> vl1 = tl vl1 else vl1 = vl1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
consume (Trans s1 a ou s') vl1 vl1

goal (3 subgoals):
 1. \<gamma> (Trans s a ou s') = \<gamma> (Trans s1 a ou s')
 2. \<gamma> (Trans s a ou s') \<Longrightarrow> g (Trans s a ou s') = g (Trans s1 a ou s')
 3. \<Delta>0 s' vl' s' vl1 \<or> \<Delta>1 s' vl' s' vl1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<gamma> (Trans s a ou s') = \<gamma> (Trans s1 a ou s')
 2. \<gamma> (Trans s a ou s') \<Longrightarrow> g (Trans s a ou s') = g (Trans s1 a ou s')
 3. \<Delta>0 s' vl' s' vl1 \<or> \<Delta>1 s' vl' s' vl1
[PROOF STEP]
show "\<gamma> ?trn = \<gamma> ?trn1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<gamma> (Trans s a ou s') = \<gamma> (Trans s1 a ou s')
[PROOF STEP]
unfolding ss1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<gamma> (Trans s a ou s') = \<gamma> (Trans s a ou s')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<gamma> (Trans s a ou s') = \<gamma> (Trans s1 a ou s')

goal (2 subgoals):
 1. \<gamma> (Trans s a ou s') \<Longrightarrow> g (Trans s a ou s') = g (Trans s1 a ou s')
 2. \<Delta>0 s' vl' s' vl1 \<or> \<Delta>1 s' vl' s' vl1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<gamma> (Trans s a ou s') \<Longrightarrow> g (Trans s a ou s') = g (Trans s1 a ou s')
 2. \<Delta>0 s' vl' s' vl1 \<or> \<Delta>1 s' vl' s' vl1
[PROOF STEP]
assume "\<gamma> ?trn"
[PROOF STATE]
proof (state)
this:
\<gamma> (Trans s a ou s')

goal (2 subgoals):
 1. \<gamma> (Trans s a ou s') \<Longrightarrow> g (Trans s a ou s') = g (Trans s1 a ou s')
 2. \<Delta>0 s' vl' s' vl1 \<or> \<Delta>1 s' vl' s' vl1
[PROOF STEP]
thus "g ?trn = g ?trn1"
[PROOF STATE]
proof (prove)
using this:
\<gamma> (Trans s a ou s')

goal (1 subgoal):
 1. g (Trans s a ou s') = g (Trans s1 a ou s')
[PROOF STEP]
unfolding ss1
[PROOF STATE]
proof (prove)
using this:
\<gamma> (Trans s a ou s')

goal (1 subgoal):
 1. g (Trans s a ou s') = g (Trans s a ou s')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
g (Trans s a ou s') = g (Trans s1 a ou s')

goal (1 subgoal):
 1. \<Delta>0 s' vl' s' vl1 \<or> \<Delta>1 s' vl' s' vl1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Delta>0 s' vl' s' vl1 \<or> \<Delta>1 s' vl' s' vl1
[PROOF STEP]
have "\<Delta>1 s' vl' s' vl1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Delta>1 s' vl' s' vl1
[PROOF STEP]
using l AID' c
[PROOF STATE]
proof (prove)
using this:
length vl = length vl1
AID \<in>\<in> serverApiIDs s'
consume (Trans s a ou s') vl vl'

goal (1 subgoal):
 1. \<Delta>1 s' vl' s' vl1
[PROOF STEP]
unfolding ss1 \<Delta>1_def vl'
[PROOF STATE]
proof (prove)
using this:
length vl = length vl1
AID \<in>\<in> serverApiIDs s'
consume (Trans s a ou s') vl vl

goal (1 subgoal):
 1. AID \<in>\<in> serverApiIDs s' \<and> eqButPID s' s' \<and> length vl = length vl1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Delta>1 s' vl' s' vl1

goal (1 subgoal):
 1. \<Delta>0 s' vl' s' vl1 \<or> \<Delta>1 s' vl' s' vl1
[PROOF STEP]
thus "?\<Delta> s' vl' s' vl1"
[PROOF STATE]
proof (prove)
using this:
\<Delta>1 s' vl' s' vl1

goal (1 subgoal):
 1. \<Delta>0 s' vl' s' vl1 \<or> \<Delta>1 s' vl' s' vl1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Delta>0 s' vl' s' vl1 \<or> \<Delta>1 s' vl' s' vl1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
match (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s s1 vl1 a ou s' vl'

goal (1 subgoal):
 1. \<nexists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s s1 vl1 a ou s' vl'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<nexists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s s1 vl1 a ou s' vl'
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<nexists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK

goal (1 subgoal):
 1. \<nexists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s s1 vl1 a ou s' vl'
[PROOF STEP]
note a = False
[PROOF STATE]
proof (state)
this:
\<nexists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK

goal (1 subgoal):
 1. \<nexists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s s1 vl1 a ou s' vl'
[PROOF STEP]
have AID': "\<not> AID \<in>\<in> serverApiIDs s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AID \<notin> set (serverApiIDs s')
[PROOF STEP]
using step AID a
[PROOF STATE]
proof (prove)
using this:
step s a = (ou, s')
AID \<notin> set (serverApiIDs s)
\<nexists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK

goal (1 subgoal):
 1. AID \<notin> set (serverApiIDs s')
[PROOF STEP]
apply(cases a)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>x1. \<lbrakk>step s a = (ou, s'); AID \<notin> set (serverApiIDs s); \<nexists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK; a = Sact x1\<rbrakk> \<Longrightarrow> AID \<notin> set (serverApiIDs s')
 2. \<And>x2. \<lbrakk>step s a = (ou, s'); AID \<notin> set (serverApiIDs s); \<nexists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK; a = Cact x2\<rbrakk> \<Longrightarrow> AID \<notin> set (serverApiIDs s')
 3. \<And>x3. \<lbrakk>step s a = (ou, s'); AID \<notin> set (serverApiIDs s); \<nexists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK; a = Dact x3\<rbrakk> \<Longrightarrow> AID \<notin> set (serverApiIDs s')
 4. \<And>x4. \<lbrakk>step s a = (ou, s'); AID \<notin> set (serverApiIDs s); \<nexists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK; a = Uact x4\<rbrakk> \<Longrightarrow> AID \<notin> set (serverApiIDs s')
 5. \<And>x5. \<lbrakk>step s a = (ou, s'); AID \<notin> set (serverApiIDs s); \<nexists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK; a = Ract x5\<rbrakk> \<Longrightarrow> AID \<notin> set (serverApiIDs s')
 6. \<And>x6. \<lbrakk>step s a = (ou, s'); AID \<notin> set (serverApiIDs s); \<nexists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK; a = Lact x6\<rbrakk> \<Longrightarrow> AID \<notin> set (serverApiIDs s')
 7. \<And>x7. \<lbrakk>step s a = (ou, s'); AID \<notin> set (serverApiIDs s); \<nexists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK; a = COMact x7\<rbrakk> \<Longrightarrow> AID \<notin> set (serverApiIDs s')
[PROOF STEP]
subgoal for x1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>step s a = (ou, s'); AID \<notin> set (serverApiIDs s); \<nexists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK; a = Sact x1\<rbrakk> \<Longrightarrow> AID \<notin> set (serverApiIDs s')
[PROOF STEP]
apply(cases x1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1a x2. \<lbrakk>step s a = (ou, s'); AID \<notin> set (serverApiIDs s); \<nexists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK; a = Sact x1; x1 = sSys x1a x2\<rbrakk> \<Longrightarrow> AID \<notin> set (serverApiIDs s')
[PROOF STEP]
apply(fastforce simp: s_defs)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>x2. \<lbrakk>step s a = (ou, s'); AID \<notin> set (serverApiIDs s); \<nexists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK; a = Cact x2\<rbrakk> \<Longrightarrow> AID \<notin> set (serverApiIDs s')
 2. \<And>x3. \<lbrakk>step s a = (ou, s'); AID \<notin> set (serverApiIDs s); \<nexists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK; a = Dact x3\<rbrakk> \<Longrightarrow> AID \<notin> set (serverApiIDs s')
 3. \<And>x4. \<lbrakk>step s a = (ou, s'); AID \<notin> set (serverApiIDs s); \<nexists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK; a = Uact x4\<rbrakk> \<Longrightarrow> AID \<notin> set (serverApiIDs s')
 4. \<And>x5. \<lbrakk>step s a = (ou, s'); AID \<notin> set (serverApiIDs s); \<nexists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK; a = Ract x5\<rbrakk> \<Longrightarrow> AID \<notin> set (serverApiIDs s')
 5. \<And>x6. \<lbrakk>step s a = (ou, s'); AID \<notin> set (serverApiIDs s); \<nexists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK; a = Lact x6\<rbrakk> \<Longrightarrow> AID \<notin> set (serverApiIDs s')
 6. \<And>x7. \<lbrakk>step s a = (ou, s'); AID \<notin> set (serverApiIDs s); \<nexists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK; a = COMact x7\<rbrakk> \<Longrightarrow> AID \<notin> set (serverApiIDs s')
[PROOF STEP]
subgoal for x2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>step s a = (ou, s'); AID \<notin> set (serverApiIDs s); \<nexists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK; a = Cact x2\<rbrakk> \<Longrightarrow> AID \<notin> set (serverApiIDs s')
[PROOF STEP]
apply(cases x2)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x11 x12. \<lbrakk>step s a = (ou, s'); AID \<notin> set (serverApiIDs s); \<nexists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK; a = Cact x2; x2 = cNUReq x11 x12\<rbrakk> \<Longrightarrow> AID \<notin> set (serverApiIDs s')
 2. \<And>x21 x22 x23 x24. \<lbrakk>step s a = (ou, s'); AID \<notin> set (serverApiIDs s); \<nexists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK; a = Cact x2; x2 = cUser x21 x22 x23 x24\<rbrakk> \<Longrightarrow> AID \<notin> set (serverApiIDs s')
 3. \<And>x31 x32 x33. \<lbrakk>step s a = (ou, s'); AID \<notin> set (serverApiIDs s); \<nexists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK; a = Cact x2; x2 = cPost x31 x32 x33\<rbrakk> \<Longrightarrow> AID \<notin> set (serverApiIDs s')
 4. \<And>x41 x42 x43 x44. \<lbrakk>step s a = (ou, s'); AID \<notin> set (serverApiIDs s); \<nexists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK; a = Cact x2; x2 = cFriendReq x41 x42 x43 x44\<rbrakk> \<Longrightarrow> AID \<notin> set (serverApiIDs s')
 5. \<And>x51 x52 x53. \<lbrakk>step s a = (ou, s'); AID \<notin> set (serverApiIDs s); \<nexists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK; a = Cact x2; x2 = cFriend x51 x52 x53\<rbrakk> \<Longrightarrow> AID \<notin> set (serverApiIDs s')
[PROOF STEP]
apply(fastforce simp: c_defs)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x3. \<lbrakk>step s a = (ou, s'); AID \<notin> set (serverApiIDs s); \<nexists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK; a = Dact x3\<rbrakk> \<Longrightarrow> AID \<notin> set (serverApiIDs s')
 2. \<And>x4. \<lbrakk>step s a = (ou, s'); AID \<notin> set (serverApiIDs s); \<nexists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK; a = Uact x4\<rbrakk> \<Longrightarrow> AID \<notin> set (serverApiIDs s')
 3. \<And>x5. \<lbrakk>step s a = (ou, s'); AID \<notin> set (serverApiIDs s); \<nexists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK; a = Ract x5\<rbrakk> \<Longrightarrow> AID \<notin> set (serverApiIDs s')
 4. \<And>x6. \<lbrakk>step s a = (ou, s'); AID \<notin> set (serverApiIDs s); \<nexists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK; a = Lact x6\<rbrakk> \<Longrightarrow> AID \<notin> set (serverApiIDs s')
 5. \<And>x7. \<lbrakk>step s a = (ou, s'); AID \<notin> set (serverApiIDs s); \<nexists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK; a = COMact x7\<rbrakk> \<Longrightarrow> AID \<notin> set (serverApiIDs s')
[PROOF STEP]
subgoal for x3
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>step s a = (ou, s'); AID \<notin> set (serverApiIDs s); \<nexists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK; a = Dact x3\<rbrakk> \<Longrightarrow> AID \<notin> set (serverApiIDs s')
[PROOF STEP]
apply(cases x3)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3a. \<lbrakk>step s a = (ou, s'); AID \<notin> set (serverApiIDs s); \<nexists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK; a = Dact x3; x3 = dFriend x1 x2 x3a\<rbrakk> \<Longrightarrow> AID \<notin> set (serverApiIDs s')
[PROOF STEP]
apply(fastforce simp: d_defs)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x4. \<lbrakk>step s a = (ou, s'); AID \<notin> set (serverApiIDs s); \<nexists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK; a = Uact x4\<rbrakk> \<Longrightarrow> AID \<notin> set (serverApiIDs s')
 2. \<And>x5. \<lbrakk>step s a = (ou, s'); AID \<notin> set (serverApiIDs s); \<nexists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK; a = Ract x5\<rbrakk> \<Longrightarrow> AID \<notin> set (serverApiIDs s')
 3. \<And>x6. \<lbrakk>step s a = (ou, s'); AID \<notin> set (serverApiIDs s); \<nexists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK; a = Lact x6\<rbrakk> \<Longrightarrow> AID \<notin> set (serverApiIDs s')
 4. \<And>x7. \<lbrakk>step s a = (ou, s'); AID \<notin> set (serverApiIDs s); \<nexists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK; a = COMact x7\<rbrakk> \<Longrightarrow> AID \<notin> set (serverApiIDs s')
[PROOF STEP]
subgoal for x4
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>step s a = (ou, s'); AID \<notin> set (serverApiIDs s); \<nexists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK; a = Uact x4\<rbrakk> \<Longrightarrow> AID \<notin> set (serverApiIDs s')
[PROOF STEP]
apply(cases x4)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x11 x12 x13 x14 x15. \<lbrakk>step s a = (ou, s'); AID \<notin> set (serverApiIDs s); \<nexists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK; a = Uact x4; x4 = uUser x11 x12 x13 x14 x15\<rbrakk> \<Longrightarrow> AID \<notin> set (serverApiIDs s')
 2. \<And>x21 x22 x23 x24. \<lbrakk>step s a = (ou, s'); AID \<notin> set (serverApiIDs s); \<nexists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK; a = Uact x4; x4 = uPost x21 x22 x23 x24\<rbrakk> \<Longrightarrow> AID \<notin> set (serverApiIDs s')
 3. \<And>x31 x32 x33 x34. \<lbrakk>step s a = (ou, s'); AID \<notin> set (serverApiIDs s); \<nexists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK; a = Uact x4; x4 = uVisPost x31 x32 x33 x34\<rbrakk> \<Longrightarrow> AID \<notin> set (serverApiIDs s')
[PROOF STEP]
apply(fastforce simp: u_defs)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x5. \<lbrakk>step s a = (ou, s'); AID \<notin> set (serverApiIDs s); \<nexists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK; a = Ract x5\<rbrakk> \<Longrightarrow> AID \<notin> set (serverApiIDs s')
 2. \<And>x6. \<lbrakk>step s a = (ou, s'); AID \<notin> set (serverApiIDs s); \<nexists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK; a = Lact x6\<rbrakk> \<Longrightarrow> AID \<notin> set (serverApiIDs s')
 3. \<And>x7. \<lbrakk>step s a = (ou, s'); AID \<notin> set (serverApiIDs s); \<nexists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK; a = COMact x7\<rbrakk> \<Longrightarrow> AID \<notin> set (serverApiIDs s')
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>step s a = (ou, s'); AID \<notin> set (serverApiIDs s); \<nexists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK; a = Ract x5_\<rbrakk> \<Longrightarrow> AID \<notin> set (serverApiIDs s')
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x6. \<lbrakk>step s a = (ou, s'); AID \<notin> set (serverApiIDs s); \<nexists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK; a = Lact x6\<rbrakk> \<Longrightarrow> AID \<notin> set (serverApiIDs s')
 2. \<And>x7. \<lbrakk>step s a = (ou, s'); AID \<notin> set (serverApiIDs s); \<nexists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK; a = COMact x7\<rbrakk> \<Longrightarrow> AID \<notin> set (serverApiIDs s')
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>step s a = (ou, s'); AID \<notin> set (serverApiIDs s); \<nexists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK; a = Lact x6_\<rbrakk> \<Longrightarrow> AID \<notin> set (serverApiIDs s')
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x7. \<lbrakk>step s a = (ou, s'); AID \<notin> set (serverApiIDs s); \<nexists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK; a = COMact x7\<rbrakk> \<Longrightarrow> AID \<notin> set (serverApiIDs s')
[PROOF STEP]
subgoal for x7
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>step s a = (ou, s'); AID \<notin> set (serverApiIDs s); \<nexists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK; a = COMact x7\<rbrakk> \<Longrightarrow> AID \<notin> set (serverApiIDs s')
[PROOF STEP]
apply(cases x7)
[PROOF STATE]
proof (prove)
goal (10 subgoals):
 1. \<And>x11 x12 x13 x14. \<lbrakk>step s a = (ou, s'); AID \<notin> set (serverApiIDs s); \<nexists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK; a = COMact x7; x7 = comSendServerReq x11 x12 x13 x14\<rbrakk> \<Longrightarrow> AID \<notin> set (serverApiIDs s')
 2. \<And>x21 x22. \<lbrakk>step s a = (ou, s'); AID \<notin> set (serverApiIDs s); \<nexists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK; a = COMact x7; x7 = comReceiveClientReq x21 x22\<rbrakk> \<Longrightarrow> AID \<notin> set (serverApiIDs s')
 3. \<And>x31 x32 x33 x34. \<lbrakk>step s a = (ou, s'); AID \<notin> set (serverApiIDs s); \<nexists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK; a = COMact x7; x7 = comConnectClient x31 x32 x33 x34\<rbrakk> \<Longrightarrow> AID \<notin> set (serverApiIDs s')
 4. \<And>x41 x42. \<lbrakk>step s a = (ou, s'); AID \<notin> set (serverApiIDs s); \<nexists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK; a = COMact x7; x7 = comConnectServer x41 x42\<rbrakk> \<Longrightarrow> AID \<notin> set (serverApiIDs s')
 5. \<And>x51 x52 x53 x54 x55 x56. \<lbrakk>step s a = (ou, s'); AID \<notin> set (serverApiIDs s); \<nexists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK; a = COMact x7; x7 = comReceivePost x51 x52 x53 x54 x55 x56\<rbrakk> \<Longrightarrow> AID \<notin> set (serverApiIDs s')
 6. \<And>x61 x62 x63 x64. \<lbrakk>step s a = (ou, s'); AID \<notin> set (serverApiIDs s); \<nexists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK; a = COMact x7; x7 = comSendPost x61 x62 x63 x64\<rbrakk> \<Longrightarrow> AID \<notin> set (serverApiIDs s')
 7. \<And>x71 x72 x73 x74. \<lbrakk>step s a = (ou, s'); AID \<notin> set (serverApiIDs s); \<nexists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK; a = COMact x7; x7 = comReceiveCreateOFriend x71 x72 x73 x74\<rbrakk> \<Longrightarrow> AID \<notin> set (serverApiIDs s')
 8. \<And>x81 x82 x83 x84. \<lbrakk>step s a = (ou, s'); AID \<notin> set (serverApiIDs s); \<nexists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK; a = COMact x7; x7 = comSendCreateOFriend x81 x82 x83 x84\<rbrakk> \<Longrightarrow> AID \<notin> set (serverApiIDs s')
 9. \<And>x91 x92 x93 x94. \<lbrakk>step s a = (ou, s'); AID \<notin> set (serverApiIDs s); \<nexists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK; a = COMact x7; x7 = comReceiveDeleteOFriend x91 x92 x93 x94\<rbrakk> \<Longrightarrow> AID \<notin> set (serverApiIDs s')
 10. \<And>x101 x102 x103 x104. \<lbrakk>step s a = (ou, s'); AID \<notin> set (serverApiIDs s); \<nexists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK; a = COMact x7; x7 = comSendDeleteOFriend x101 x102 x103 x104\<rbrakk> \<Longrightarrow> AID \<notin> set (serverApiIDs s')
[PROOF STEP]
apply(fastforce simp: com_defs)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
AID \<notin> set (serverApiIDs s')

goal (1 subgoal):
 1. \<nexists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s s1 vl1 a ou s' vl'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. match (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s s1 vl1 a ou s' vl'
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. validTrans (Trans s1 ?a1.0 ?ou1.0 ?s1')
 2. consume (Trans s1 ?a1.0 ?ou1.0 ?s1') vl1 ?vl1'
 3. \<gamma> (Trans s a ou s') = \<gamma> (Trans s1 ?a1.0 ?ou1.0 ?s1')
 4. \<gamma> (Trans s a ou s') \<Longrightarrow> g (Trans s a ou s') = g (Trans s1 ?a1.0 ?ou1.0 ?s1')
 5. \<Delta>0 s' vl' ?s1' ?vl1' \<or> \<Delta>1 s' vl' ?s1' ?vl1'
[PROOF STEP]
show "validTrans ?trn1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. validTrans (Trans s1 a ou s')
[PROOF STEP]
unfolding ss1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. validTrans (Trans s a ou s')
[PROOF STEP]
using step
[PROOF STATE]
proof (prove)
using this:
step s a = (ou, s')

goal (1 subgoal):
 1. validTrans (Trans s a ou s')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
validTrans (Trans s1 a ou s')

goal (4 subgoals):
 1. consume (Trans s1 a ou s') vl1 ?vl1'
 2. \<gamma> (Trans s a ou s') = \<gamma> (Trans s1 a ou s')
 3. \<gamma> (Trans s a ou s') \<Longrightarrow> g (Trans s a ou s') = g (Trans s1 a ou s')
 4. \<Delta>0 s' vl' s' ?vl1' \<or> \<Delta>1 s' vl' s' ?vl1'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. consume (Trans s1 a ou s') vl1 ?vl1'
 2. \<gamma> (Trans s a ou s') = \<gamma> (Trans s1 a ou s')
 3. \<gamma> (Trans s a ou s') \<Longrightarrow> g (Trans s a ou s') = g (Trans s1 a ou s')
 4. \<Delta>0 s' vl' s' ?vl1' \<or> \<Delta>1 s' vl' s' ?vl1'
[PROOF STEP]
show "consume ?trn1 vl1 vl1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. consume (Trans s1 a ou s') vl1 vl1
[PROOF STEP]
using \<phi>
[PROOF STATE]
proof (prove)
using this:
\<not> \<phi> (Trans s a ou s')

goal (1 subgoal):
 1. consume (Trans s1 a ou s') vl1 vl1
[PROOF STEP]
unfolding consume_def ss1
[PROOF STATE]
proof (prove)
using this:
\<not> \<phi> (Trans s a ou s')

goal (1 subgoal):
 1. if \<phi> (Trans s a ou s') then vl1 \<noteq> [] \<and> f (Trans s a ou s') = hd vl1 \<and> vl1 = tl vl1 else vl1 = vl1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
consume (Trans s1 a ou s') vl1 vl1

goal (3 subgoals):
 1. \<gamma> (Trans s a ou s') = \<gamma> (Trans s1 a ou s')
 2. \<gamma> (Trans s a ou s') \<Longrightarrow> g (Trans s a ou s') = g (Trans s1 a ou s')
 3. \<Delta>0 s' vl' s' vl1 \<or> \<Delta>1 s' vl' s' vl1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<gamma> (Trans s a ou s') = \<gamma> (Trans s1 a ou s')
 2. \<gamma> (Trans s a ou s') \<Longrightarrow> g (Trans s a ou s') = g (Trans s1 a ou s')
 3. \<Delta>0 s' vl' s' vl1 \<or> \<Delta>1 s' vl' s' vl1
[PROOF STEP]
show "\<gamma> ?trn = \<gamma> ?trn1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<gamma> (Trans s a ou s') = \<gamma> (Trans s1 a ou s')
[PROOF STEP]
unfolding ss1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<gamma> (Trans s a ou s') = \<gamma> (Trans s a ou s')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<gamma> (Trans s a ou s') = \<gamma> (Trans s1 a ou s')

goal (2 subgoals):
 1. \<gamma> (Trans s a ou s') \<Longrightarrow> g (Trans s a ou s') = g (Trans s1 a ou s')
 2. \<Delta>0 s' vl' s' vl1 \<or> \<Delta>1 s' vl' s' vl1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<gamma> (Trans s a ou s') \<Longrightarrow> g (Trans s a ou s') = g (Trans s1 a ou s')
 2. \<Delta>0 s' vl' s' vl1 \<or> \<Delta>1 s' vl' s' vl1
[PROOF STEP]
assume "\<gamma> ?trn"
[PROOF STATE]
proof (state)
this:
\<gamma> (Trans s a ou s')

goal (2 subgoals):
 1. \<gamma> (Trans s a ou s') \<Longrightarrow> g (Trans s a ou s') = g (Trans s1 a ou s')
 2. \<Delta>0 s' vl' s' vl1 \<or> \<Delta>1 s' vl' s' vl1
[PROOF STEP]
thus "g ?trn = g ?trn1"
[PROOF STATE]
proof (prove)
using this:
\<gamma> (Trans s a ou s')

goal (1 subgoal):
 1. g (Trans s a ou s') = g (Trans s1 a ou s')
[PROOF STEP]
unfolding ss1
[PROOF STATE]
proof (prove)
using this:
\<gamma> (Trans s a ou s')

goal (1 subgoal):
 1. g (Trans s a ou s') = g (Trans s a ou s')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
g (Trans s a ou s') = g (Trans s1 a ou s')

goal (1 subgoal):
 1. \<Delta>0 s' vl' s' vl1 \<or> \<Delta>1 s' vl' s' vl1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Delta>0 s' vl' s' vl1 \<or> \<Delta>1 s' vl' s' vl1
[PROOF STEP]
have "\<Delta>0 s' vl' s' vl1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Delta>0 s' vl' s' vl1
[PROOF STEP]
using a AID' l
[PROOF STATE]
proof (prove)
using this:
\<nexists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK
AID \<notin> set (serverApiIDs s')
length vl = length vl1

goal (1 subgoal):
 1. \<Delta>0 s' vl' s' vl1
[PROOF STEP]
unfolding \<Delta>0_def vl' ss1
[PROOF STATE]
proof (prove)
using this:
\<nexists>p. a = COMact (comConnectServer AID p) \<and> ou = outOK
AID \<notin> set (serverApiIDs s')
length vl = length vl1

goal (1 subgoal):
 1. AID \<notin> set (serverApiIDs s') \<and> s' = s' \<and> length vl = length vl1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Delta>0 s' vl' s' vl1

goal (1 subgoal):
 1. \<Delta>0 s' vl' s' vl1 \<or> \<Delta>1 s' vl' s' vl1
[PROOF STEP]
thus "?\<Delta> s' vl' s' vl1"
[PROOF STATE]
proof (prove)
using this:
\<Delta>0 s' vl' s' vl1

goal (1 subgoal):
 1. \<Delta>0 s' vl' s' vl1 \<or> \<Delta>1 s' vl' s' vl1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Delta>0 s' vl' s' vl1 \<or> \<Delta>1 s' vl' s' vl1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
match (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s s1 vl1 a ou s' vl'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
match (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s s1 vl1 a ou s' vl'

goal (1 subgoal):
 1. match (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s s1 vl1 a ou s' vl' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s s1 vl1 a ou s' vl'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
match (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s s1 vl1 a ou s' vl'

goal (1 subgoal):
 1. match (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s s1 vl1 a ou s' vl' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s s1 vl1 a ou s' vl'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
match (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s s1 vl1 a ou s' vl' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s s1 vl1 a ou s' vl'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
match (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s s1 vl1 a ou s' vl' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s s1 vl1 a ou s' vl'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
reaction (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s vl s1 vl1

goal (1 subgoal):
 1. iaction (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s vl s1 vl1 \<or> (vl = [] \<longrightarrow> vl1 = []) \<and> reaction (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s vl s1 vl1
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
reaction (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s vl s1 vl1

goal (1 subgoal):
 1. iaction (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s vl s1 vl1 \<or> (vl = [] \<longrightarrow> vl1 = []) \<and> reaction (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s vl s1 vl1
[PROOF STEP]
using l
[PROOF STATE]
proof (prove)
using this:
reaction (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s vl s1 vl1
length vl = length vl1

goal (1 subgoal):
 1. iaction (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s vl s1 vl1 \<or> (vl = [] \<longrightarrow> vl1 = []) \<and> reaction (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s vl s1 vl1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
iaction (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s vl s1 vl1 \<or> (vl = [] \<longrightarrow> vl1 = []) \<and> reaction (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s vl s1 vl1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
iaction (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s vl s1 vl1 \<or> (vl = [] \<longrightarrow> vl1 = []) \<and> reaction (\<lambda>s vl s1 vl1. \<Delta>0 s vl s1 vl1 \<or> \<Delta>1 s vl s1 vl1) s vl s1 vl1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma unwind_cont_\<Delta>1: "unwind_cont \<Delta>1 {\<Delta>1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unwind_cont \<Delta>1 {\<Delta>1}
[PROOF STEP]
proof(rule, simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s vl s1 vl1. \<lbrakk>reachNT s; reach s1; \<Delta>1 s vl s1 vl1\<rbrakk> \<Longrightarrow> iaction \<Delta>1 s vl s1 vl1 \<or> (vl = [] \<longrightarrow> vl1 = []) \<and> reaction \<Delta>1 s vl s1 vl1
[PROOF STEP]
let ?\<Delta> = "\<lambda>s vl s1 vl1. \<Delta>1 s vl s1 vl1"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s vl s1 vl1. \<lbrakk>reachNT s; reach s1; \<Delta>1 s vl s1 vl1\<rbrakk> \<Longrightarrow> iaction \<Delta>1 s vl s1 vl1 \<or> (vl = [] \<longrightarrow> vl1 = []) \<and> reaction \<Delta>1 s vl s1 vl1
[PROOF STEP]
fix s s1 :: state and vl vl1 :: "value list"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s vl s1 vl1. \<lbrakk>reachNT s; reach s1; \<Delta>1 s vl s1 vl1\<rbrakk> \<Longrightarrow> iaction \<Delta>1 s vl s1 vl1 \<or> (vl = [] \<longrightarrow> vl1 = []) \<and> reaction \<Delta>1 s vl s1 vl1
[PROOF STEP]
assume rsT: "reachNT s" and rs1: "reach s1" and "\<Delta>1 s vl s1 vl1"
[PROOF STATE]
proof (state)
this:
reachNT s
reach s1
\<Delta>1 s vl s1 vl1

goal (1 subgoal):
 1. \<And>s vl s1 vl1. \<lbrakk>reachNT s; reach s1; \<Delta>1 s vl s1 vl1\<rbrakk> \<Longrightarrow> iaction \<Delta>1 s vl s1 vl1 \<or> (vl = [] \<longrightarrow> vl1 = []) \<and> reaction \<Delta>1 s vl s1 vl1
[PROOF STEP]
hence rs: "reach s" and ss1: "eqButPID s s1"
  and l: "length vl = length vl1" and AID: "AID \<in>\<in> serverApiIDs s"
[PROOF STATE]
proof (prove)
using this:
reachNT s
reach s1
\<Delta>1 s vl s1 vl1

goal (1 subgoal):
 1. (reach s &&& eqButPID s s1) &&& length vl = length vl1 &&& AID \<in>\<in> serverApiIDs s
[PROOF STEP]
using reachNT_reach
[PROOF STATE]
proof (prove)
using this:
reachNT s
reach s1
\<Delta>1 s vl s1 vl1
reachNT ?s \<Longrightarrow> reach ?s

goal (1 subgoal):
 1. (reach s &&& eqButPID s s1) &&& length vl = length vl1 &&& AID \<in>\<in> serverApiIDs s
[PROOF STEP]
unfolding \<Delta>1_def
[PROOF STATE]
proof (prove)
using this:
reachNT s
reach s1
AID \<in>\<in> serverApiIDs s \<and> eqButPID s s1 \<and> length vl = length vl1
reachNT ?s \<Longrightarrow> reach ?s

goal (1 subgoal):
 1. (reach s &&& eqButPID s s1) &&& length vl = length vl1 &&& AID \<in>\<in> serverApiIDs s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
reach s
eqButPID s s1
length vl = length vl1
AID \<in>\<in> serverApiIDs s

goal (1 subgoal):
 1. \<And>s vl s1 vl1. \<lbrakk>reachNT s; reach s1; \<Delta>1 s vl s1 vl1\<rbrakk> \<Longrightarrow> iaction \<Delta>1 s vl s1 vl1 \<or> (vl = [] \<longrightarrow> vl1 = []) \<and> reaction \<Delta>1 s vl s1 vl1
[PROOF STEP]
have AID1: "AID \<in>\<in> serverApiIDs s1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AID \<in>\<in> serverApiIDs s1
[PROOF STEP]
using eqButPID_stateSelectors[OF ss1] AID
[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> pendingFReqs s = pendingFReqs s1 \<and> friendReq s = friendReq s1 \<and> friendIDs s = friendIDs s1 \<and> sentOuterFriendIDs s = sentOuterFriendIDs s1 \<and> recvOuterFriendIDs s = recvOuterFriendIDs s1 \<and> postIDs s = postIDs s1 \<and> admin s = admin s1 \<and> post s = post s1 \<and> owner s = owner s1 \<and> vis s = vis 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> eeqButPID (outerPost s) (outerPost s1) \<and> outerOwner s = outerOwner s1 \<and> outerVis s = outerVis 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 \<and> IDsOK s = IDsOK s1
AID \<in>\<in> serverApiIDs s

goal (1 subgoal):
 1. AID \<in>\<in> serverApiIDs s1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
AID \<in>\<in> serverApiIDs s1

goal (1 subgoal):
 1. \<And>s vl s1 vl1. \<lbrakk>reachNT s; reach s1; \<Delta>1 s vl s1 vl1\<rbrakk> \<Longrightarrow> iaction \<Delta>1 s vl s1 vl1 \<or> (vl = [] \<longrightarrow> vl1 = []) \<and> reaction \<Delta>1 s vl s1 vl1
[PROOF STEP]
(* have own: "owner s PID \<in> set (userIDs s)" using reach_owner_userIDs[OF rs PID] .
  hence own1: "owner s1 PID \<in> set (userIDs s1)" using eqButPID_stateSelectors[OF ss1] by auto *)
[PROOF STATE]
proof (state)
this:
AID \<in>\<in> serverApiIDs s1

goal (1 subgoal):
 1. \<And>s vl s1 vl1. \<lbrakk>reachNT s; reach s1; \<Delta>1 s vl s1 vl1\<rbrakk> \<Longrightarrow> iaction \<Delta>1 s vl s1 vl1 \<or> (vl = [] \<longrightarrow> vl1 = []) \<and> reaction \<Delta>1 s vl s1 vl1
[PROOF STEP]
show "iaction ?\<Delta> s vl s1 vl1 \<or>
        ((vl = [] \<longrightarrow> vl1 = []) \<and> reaction ?\<Delta> s vl s1 vl1)" (is "?iact \<or> (_ \<and> ?react)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iaction \<Delta>1 s vl s1 vl1 \<or> (vl = [] \<longrightarrow> vl1 = []) \<and> reaction \<Delta>1 s vl s1 vl1
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. iaction \<Delta>1 s vl s1 vl1 \<or> (vl = [] \<longrightarrow> vl1 = []) \<and> reaction \<Delta>1 s vl s1 vl1
[PROOF STEP]
have ?react
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reaction \<Delta>1 s vl s1 vl1
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a ou s' vl'. \<lbrakk>step s a = (ou, s'); \<not> T (Trans s a ou s'); consume (Trans s a ou s') vl vl'\<rbrakk> \<Longrightarrow> match \<Delta>1 s s1 vl1 a ou s' vl' \<or> ignore \<Delta>1 s s1 vl1 a ou s' vl'
[PROOF STEP]
fix a :: act and ou :: out and s' :: state and vl'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a ou s' vl'. \<lbrakk>step s a = (ou, s'); \<not> T (Trans s a ou s'); consume (Trans s a ou s') vl vl'\<rbrakk> \<Longrightarrow> match \<Delta>1 s s1 vl1 a ou s' vl' \<or> ignore \<Delta>1 s s1 vl1 a ou s' vl'
[PROOF STEP]
let ?trn = "Trans s a ou s'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a ou s' vl'. \<lbrakk>step s a = (ou, s'); \<not> T (Trans s a ou s'); consume (Trans s a ou s') vl vl'\<rbrakk> \<Longrightarrow> match \<Delta>1 s s1 vl1 a ou s' vl' \<or> ignore \<Delta>1 s s1 vl1 a ou s' vl'
[PROOF STEP]
assume step: "step s a = (ou, s')" and T: "\<not> T ?trn" and c: "consume ?trn vl vl'"
[PROOF STATE]
proof (state)
this:
step s a = (ou, s')
\<not> T (Trans s a ou s')
consume (Trans s a ou s') vl vl'

goal (1 subgoal):
 1. \<And>a ou s' vl'. \<lbrakk>step s a = (ou, s'); \<not> T (Trans s a ou s'); consume (Trans s a ou s') vl vl'\<rbrakk> \<Longrightarrow> match \<Delta>1 s s1 vl1 a ou s' vl' \<or> ignore \<Delta>1 s s1 vl1 a ou s' vl'
[PROOF STEP]
show "match ?\<Delta> s s1 vl1 a ou s' vl' \<or> ignore ?\<Delta> s s1 vl1 a ou s' vl'" (is "?match \<or> ?ignore")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. match \<Delta>1 s s1 vl1 a ou s' vl' \<or> ignore \<Delta>1 s s1 vl1 a ou s' vl'
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. match \<Delta>1 s s1 vl1 a ou s' vl' \<or> ignore \<Delta>1 s s1 vl1 a ou s' vl'
[PROOF STEP]
have ?match
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. match \<Delta>1 s s1 vl1 a ou s' vl'
[PROOF STEP]
proof(cases "\<exists> p pst uid vs. a = COMact (comReceivePost AID p PID pst uid vs) \<and> ou = outOK")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>p pst uid vs. a = COMact (comReceivePost AID p PID pst uid vs) \<and> ou = outOK \<Longrightarrow> match \<Delta>1 s s1 vl1 a ou s' vl'
 2. \<nexists>p pst uid vs. a = COMact (comReceivePost AID p PID pst uid vs) \<and> ou = outOK \<Longrightarrow> match \<Delta>1 s s1 vl1 a ou s' vl'
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<exists>p pst uid vs. a = COMact (comReceivePost AID p PID pst uid vs) \<and> ou = outOK

goal (2 subgoals):
 1. \<exists>p pst uid vs. a = COMact (comReceivePost AID p PID pst uid vs) \<and> ou = outOK \<Longrightarrow> match \<Delta>1 s s1 vl1 a ou s' vl'
 2. \<nexists>p pst uid vs. a = COMact (comReceivePost AID p PID pst uid vs) \<and> ou = outOK \<Longrightarrow> match \<Delta>1 s s1 vl1 a ou s' vl'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>p pst uid vs. a = COMact (comReceivePost AID p PID pst uid vs) \<and> ou = outOK
[PROOF STEP]
obtain p pst uid vs where
          a: "a = COMact (comReceivePost AID p PID pst uid vs)" and ou: "ou = outOK"
[PROOF STATE]
proof (prove)
using this:
\<exists>p pst uid vs. a = COMact (comReceivePost AID p PID pst uid vs) \<and> ou = outOK

goal (1 subgoal):
 1. (\<And>p pst uid vs. \<lbrakk>a = COMact (comReceivePost AID p PID pst uid vs); ou = outOK\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a = COMact (comReceivePost AID p PID pst uid vs)
ou = outOK

goal (2 subgoals):
 1. \<exists>p pst uid vs. a = COMact (comReceivePost AID p PID pst uid vs) \<and> ou = outOK \<Longrightarrow> match \<Delta>1 s s1 vl1 a ou s' vl'
 2. \<nexists>p pst uid vs. a = COMact (comReceivePost AID p PID pst uid vs) \<and> ou = outOK \<Longrightarrow> match \<Delta>1 s s1 vl1 a ou s' vl'
[PROOF STEP]
have p: "p = serverPass s AID"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p = serverPass s AID
[PROOF STEP]
using comReceivePost_out[OF step a ou]
[PROOF STATE]
proof (prove)
using this:
p = serverPass s AID

goal (1 subgoal):
 1. p = serverPass s AID
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
p = serverPass s AID

goal (2 subgoals):
 1. \<exists>p pst uid vs. a = COMact (comReceivePost AID p PID pst uid vs) \<and> ou = outOK \<Longrightarrow> match \<Delta>1 s s1 vl1 a ou s' vl'
 2. \<nexists>p pst uid vs. a = COMact (comReceivePost AID p PID pst uid vs) \<and> ou = outOK \<Longrightarrow> match \<Delta>1 s s1 vl1 a ou s' vl'
[PROOF STEP]
have p1: "p = serverPass s1 AID"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p = serverPass s1 AID
[PROOF STEP]
using p ss1 eqButPID_stateSelectors
[PROOF STATE]
proof (prove)
using this:
p = serverPass s AID
eqButPID s s1
eqButPID ?s ?s1.0 \<Longrightarrow> admin ?s = admin ?s1.0 \<and> pendingUReqs ?s = pendingUReqs ?s1.0 \<and> userReq ?s = userReq ?s1.0 \<and> userIDs ?s = userIDs ?s1.0 \<and> user ?s = user ?s1.0 \<and> pass ?s = pass ?s1.0 \<and> pendingFReqs ?s = pendingFReqs ?s1.0 \<and> friendReq ?s = friendReq ?s1.0 \<and> friendIDs ?s = friendIDs ?s1.0 \<and> sentOuterFriendIDs ?s = sentOuterFriendIDs ?s1.0 \<and> recvOuterFriendIDs ?s = recvOuterFriendIDs ?s1.0 \<and> postIDs ?s = postIDs ?s1.0 \<and> admin ?s = admin ?s1.0 \<and> post ?s = post ?s1.0 \<and> owner ?s = owner ?s1.0 \<and> vis ?s = vis ?s1.0 \<and> pendingSApiReqs ?s = pendingSApiReqs ?s1.0 \<and> sApiReq ?s = sApiReq ?s1.0 \<and> serverApiIDs ?s = serverApiIDs ?s1.0 \<and> serverPass ?s = serverPass ?s1.0 \<and> outerPostIDs ?s = outerPostIDs ?s1.0 \<and> eeqButPID (outerPost ?s) (outerPost ?s1.0) \<and> outerOwner ?s = outerOwner ?s1.0 \<and> outerVis ?s = outerVis ?s1.0 \<and> pendingCApiReqs ?s = pendingCApiReqs ?s1.0 \<and> cApiReq ?s = cApiReq ?s1.0 \<and> clientApiIDs ?s = clientApiIDs ?s1.0 \<and> clientPass ?s = clientPass ?s1.0 \<and> sharedWith ?s = sharedWith ?s1.0 \<and> IDsOK ?s = IDsOK ?s1.0

goal (1 subgoal):
 1. p = serverPass s1 AID
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p = serverPass s1 AID

goal (2 subgoals):
 1. \<exists>p pst uid vs. a = COMact (comReceivePost AID p PID pst uid vs) \<and> ou = outOK \<Longrightarrow> match \<Delta>1 s s1 vl1 a ou s' vl'
 2. \<nexists>p pst uid vs. a = COMact (comReceivePost AID p PID pst uid vs) \<and> ou = outOK \<Longrightarrow> match \<Delta>1 s s1 vl1 a ou s' vl'
[PROOF STEP]
have \<phi>: "\<phi> ?trn"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> (Trans s a ou s')
[PROOF STEP]
using a ou step \<phi>_def2
[PROOF STATE]
proof (prove)
using this:
a = COMact (comReceivePost AID p PID pst uid vs)
ou = outOK
step s a = (ou, s')
\<phi> (Trans ?s ?a ?ou ?s') = (\<exists>uid p pst vs. ?a = COMact (comReceivePost AID p PID pst uid vs) \<and> ?ou = outOK)

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

goal (2 subgoals):
 1. \<exists>p pst uid vs. a = COMact (comReceivePost AID p PID pst uid vs) \<and> ou = outOK \<Longrightarrow> match \<Delta>1 s s1 vl1 a ou s' vl'
 2. \<nexists>p pst uid vs. a = COMact (comReceivePost AID p PID pst uid vs) \<and> ou = outOK \<Longrightarrow> match \<Delta>1 s s1 vl1 a ou s' vl'
[PROOF STEP]
obtain v where vl: "vl = v # vl'" and f: "f ?trn = v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>v. \<lbrakk>vl = v # vl'; f (Trans s a ou s') = v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using c \<phi>
[PROOF STATE]
proof (prove)
using this:
consume (Trans s a ou s') vl vl'
\<phi> (Trans s a ou s')

goal (1 subgoal):
 1. (\<And>v. \<lbrakk>vl = v # vl'; f (Trans s a ou s') = v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding consume_def
[PROOF STATE]
proof (prove)
using this:
if \<phi> (Trans s a ou s') then vl \<noteq> [] \<and> f (Trans s a ou s') = hd vl \<and> vl' = tl vl else vl' = vl
\<phi> (Trans s a ou s')

goal (1 subgoal):
 1. (\<And>v. \<lbrakk>vl = v # vl'; f (Trans s a ou s') = v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases vl) auto
[PROOF STATE]
proof (state)
this:
vl = v # vl'
f (Trans s a ou s') = v

goal (2 subgoals):
 1. \<exists>p pst uid vs. a = COMact (comReceivePost AID p PID pst uid vs) \<and> ou = outOK \<Longrightarrow> match \<Delta>1 s s1 vl1 a ou s' vl'
 2. \<nexists>p pst uid vs. a = COMact (comReceivePost AID p PID pst uid vs) \<and> ou = outOK \<Longrightarrow> match \<Delta>1 s s1 vl1 a ou s' vl'
[PROOF STEP]
have AID': "AID \<in>\<in> serverApiIDs s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AID \<in>\<in> serverApiIDs s'
[PROOF STEP]
using step AID
[PROOF STATE]
proof (prove)
using this:
step s a = (ou, s')
AID \<in>\<in> serverApiIDs s

goal (1 subgoal):
 1. AID \<in>\<in> serverApiIDs s'
[PROOF STEP]
unfolding a ou
[PROOF STATE]
proof (prove)
using this:
step s (COMact (comReceivePost AID p PID pst uid vs)) = (outOK, s')
AID \<in>\<in> serverApiIDs s

goal (1 subgoal):
 1. AID \<in>\<in> serverApiIDs s'
[PROOF STEP]
by (auto simp: com_defs)
[PROOF STATE]
proof (state)
this:
AID \<in>\<in> serverApiIDs s'

goal (2 subgoals):
 1. \<exists>p pst uid vs. a = COMact (comReceivePost AID p PID pst uid vs) \<and> ou = outOK \<Longrightarrow> match \<Delta>1 s s1 vl1 a ou s' vl'
 2. \<nexists>p pst uid vs. a = COMact (comReceivePost AID p PID pst uid vs) \<and> ou = outOK \<Longrightarrow> match \<Delta>1 s s1 vl1 a ou s' vl'
[PROOF STEP]
note uid = reachNT_state[OF rsT]
[PROOF STATE]
proof (state)
this:
\<not> (\<exists>uid\<in>UIDs. uid \<in>\<in> userIDs s \<and> PID \<in>\<in> outerPostIDs s AID \<and> (uid = admin s \<or> (AID, outerOwner s AID PID) \<in>\<in> recvOuterFriendIDs s uid \<or> outerVis s AID PID = PublicV))

goal (2 subgoals):
 1. \<exists>p pst uid vs. a = COMact (comReceivePost AID p PID pst uid vs) \<and> ou = outOK \<Longrightarrow> match \<Delta>1 s s1 vl1 a ou s' vl'
 2. \<nexists>p pst uid vs. a = COMact (comReceivePost AID p PID pst uid vs) \<and> ou = outOK \<Longrightarrow> match \<Delta>1 s s1 vl1 a ou s' vl'
[PROOF STEP]
obtain v1 vl1' where vl1: "vl1 = v1 # vl1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>v1 vl1'. vl1 = v1 # vl1' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using l
[PROOF STATE]
proof (prove)
using this:
length vl = length vl1

goal (1 subgoal):
 1. (\<And>v1 vl1'. vl1 = v1 # vl1' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding vl
[PROOF STATE]
proof (prove)
using this:
length (v # vl') = length vl1

goal (1 subgoal):
 1. (\<And>v1 vl1'. vl1 = v1 # vl1' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases vl1) auto
[PROOF STATE]
proof (state)
this:
vl1 = v1 # vl1'

goal (2 subgoals):
 1. \<exists>p pst uid vs. a = COMact (comReceivePost AID p PID pst uid vs) \<and> ou = outOK \<Longrightarrow> match \<Delta>1 s s1 vl1 a ou s' vl'
 2. \<nexists>p pst uid vs. a = COMact (comReceivePost AID p PID pst uid vs) \<and> ou = outOK \<Longrightarrow> match \<Delta>1 s s1 vl1 a ou s' vl'
[PROOF STEP]
obtain pst1 where v1: "v1 = PValR pst1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>pst1. v1 = PValR pst1 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases v1) auto
[PROOF STATE]
proof (state)
this:
v1 = PValR pst1

goal (2 subgoals):
 1. \<exists>p pst uid vs. a = COMact (comReceivePost AID p PID pst uid vs) \<and> ou = outOK \<Longrightarrow> match \<Delta>1 s s1 vl1 a ou s' vl'
 2. \<nexists>p pst uid vs. a = COMact (comReceivePost AID p PID pst uid vs) \<and> ou = outOK \<Longrightarrow> match \<Delta>1 s s1 vl1 a ou s' vl'
[PROOF STEP]
define a1 where "a1 \<equiv> COMact (comReceivePost AID p PID pst1 uid vs)"
[PROOF STATE]
proof (state)
this:
a1 \<equiv> COMact (comReceivePost AID p PID pst1 uid vs)

goal (2 subgoals):
 1. \<exists>p pst uid vs. a = COMact (comReceivePost AID p PID pst uid vs) \<and> ou = outOK \<Longrightarrow> match \<Delta>1 s s1 vl1 a ou s' vl'
 2. \<nexists>p pst uid vs. a = COMact (comReceivePost AID p PID pst uid vs) \<and> ou = outOK \<Longrightarrow> match \<Delta>1 s s1 vl1 a ou s' vl'
[PROOF STEP]
note a1 = this
[PROOF STATE]
proof (state)
this:
a1 \<equiv> COMact (comReceivePost AID p PID pst1 uid vs)

goal (2 subgoals):
 1. \<exists>p pst uid vs. a = COMact (comReceivePost AID p PID pst uid vs) \<and> ou = outOK \<Longrightarrow> match \<Delta>1 s s1 vl1 a ou s' vl'
 2. \<nexists>p pst uid vs. a = COMact (comReceivePost AID p PID pst uid vs) \<and> ou = outOK \<Longrightarrow> match \<Delta>1 s s1 vl1 a ou s' vl'
[PROOF STEP]
obtain s1' where step1: "step s1 a1 = (outOK, s1')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s1'. step s1 a1 = (outOK, s1') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using AID1
[PROOF STATE]
proof (prove)
using this:
AID \<in>\<in> serverApiIDs s1

goal (1 subgoal):
 1. (\<And>s1'. step s1 a1 = (outOK, s1') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding a1_def p1
[PROOF STATE]
proof (prove)
using this:
AID \<in>\<in> serverApiIDs s1

goal (1 subgoal):
 1. (\<And>s1'. step s1 (COMact (comReceivePost AID (serverPass s1 AID) PID pst1 uid vs)) = (outOK, s1') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (simp add: com_defs)
[PROOF STATE]
proof (state)
this:
step s1 a1 = (outOK, s1')

goal (2 subgoals):
 1. \<exists>p pst uid vs. a = COMact (comReceivePost AID p PID pst uid vs) \<and> ou = outOK \<Longrightarrow> match \<Delta>1 s s1 vl1 a ou s' vl'
 2. \<nexists>p pst uid vs. a = COMact (comReceivePost AID p PID pst uid vs) \<and> ou = outOK \<Longrightarrow> match \<Delta>1 s s1 vl1 a ou s' vl'
[PROOF STEP]
have s's1': "eqButPID s' s1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqButPID s' s1'
[PROOF STEP]
using comReceivePost_step_eqButPID[OF a _ step step1 ss1] a1
[PROOF STATE]
proof (prove)
using this:
a1 = COMact (comReceivePost AID p PID ?pst1.0 uid vs) \<Longrightarrow> eqButPID s' s1'
a1 \<equiv> COMact (comReceivePost AID p PID pst1 uid vs)

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

goal (2 subgoals):
 1. \<exists>p pst uid vs. a = COMact (comReceivePost AID p PID pst uid vs) \<and> ou = outOK \<Longrightarrow> match \<Delta>1 s s1 vl1 a ou s' vl'
 2. \<nexists>p pst uid vs. a = COMact (comReceivePost AID p PID pst uid vs) \<and> ou = outOK \<Longrightarrow> match \<Delta>1 s s1 vl1 a ou s' vl'
[PROOF STEP]
let ?trn1 = "Trans s1 a1 outOK s1'"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>p pst uid vs. a = COMact (comReceivePost AID p PID pst uid vs) \<and> ou = outOK \<Longrightarrow> match \<Delta>1 s s1 vl1 a ou s' vl'
 2. \<nexists>p pst uid vs. a = COMact (comReceivePost AID p PID pst uid vs) \<and> ou = outOK \<Longrightarrow> match \<Delta>1 s s1 vl1 a ou s' vl'
[PROOF STEP]
have \<phi>1: "\<phi> ?trn1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> (Trans s1 a1 outOK s1')
[PROOF STEP]
unfolding \<phi>_def2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>uid p pst vs. a1 = COMact (comReceivePost AID p PID pst uid vs) \<and> outOK = outOK
[PROOF STEP]
(* [OF step1] *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>uid p pst vs. a1 = COMact (comReceivePost AID p PID pst uid vs) \<and> outOK = outOK
[PROOF STEP]
unfolding a1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>uida pa pst vsa. COMact (comReceivePost AID p PID pst1 uid vs) = COMact (comReceivePost AID pa PID pst uida vsa) \<and> outOK = outOK
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<phi> (Trans s1 a1 outOK s1')

goal (2 subgoals):
 1. \<exists>p pst uid vs. a = COMact (comReceivePost AID p PID pst uid vs) \<and> ou = outOK \<Longrightarrow> match \<Delta>1 s s1 vl1 a ou s' vl'
 2. \<nexists>p pst uid vs. a = COMact (comReceivePost AID p PID pst uid vs) \<and> ou = outOK \<Longrightarrow> match \<Delta>1 s s1 vl1 a ou s' vl'
[PROOF STEP]
have f1: "f ?trn1 = v1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (Trans s1 a1 outOK s1') = v1
[PROOF STEP]
unfolding a1 v1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (Trans s1 (COMact (comReceivePost AID p PID pst1 uid vs)) outOK s1') = PValR pst1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f (Trans s1 a1 outOK s1') = v1

goal (2 subgoals):
 1. \<exists>p pst uid vs. a = COMact (comReceivePost AID p PID pst uid vs) \<and> ou = outOK \<Longrightarrow> match \<Delta>1 s s1 vl1 a ou s' vl'
 2. \<nexists>p pst uid vs. a = COMact (comReceivePost AID p PID pst uid vs) \<and> ou = outOK \<Longrightarrow> match \<Delta>1 s s1 vl1 a ou s' vl'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. match \<Delta>1 s s1 vl1 a ou s' vl'
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. validTrans (Trans s1 ?a1.0 ?ou1.0 ?s1')
 2. consume (Trans s1 ?a1.0 ?ou1.0 ?s1') vl1 ?vl1'
 3. \<gamma> (Trans s a ou s') = \<gamma> (Trans s1 ?a1.0 ?ou1.0 ?s1')
 4. \<gamma> (Trans s a ou s') \<Longrightarrow> g (Trans s a ou s') = g (Trans s1 ?a1.0 ?ou1.0 ?s1')
 5. \<Delta>1 s' vl' ?s1' ?vl1'
[PROOF STEP]
show "validTrans ?trn1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. validTrans (Trans s1 a1 outOK s1')
[PROOF STEP]
using step1
[PROOF STATE]
proof (prove)
using this:
step s1 a1 = (outOK, s1')

goal (1 subgoal):
 1. validTrans (Trans s1 a1 outOK s1')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
validTrans (Trans s1 a1 outOK s1')

goal (4 subgoals):
 1. consume (Trans s1 a1 outOK s1') vl1 ?vl1'
 2. \<gamma> (Trans s a ou s') = \<gamma> (Trans s1 a1 outOK s1')
 3. \<gamma> (Trans s a ou s') \<Longrightarrow> g (Trans s a ou s') = g (Trans s1 a1 outOK s1')
 4. \<Delta>1 s' vl' s1' ?vl1'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. consume (Trans s1 a1 outOK s1') vl1 ?vl1'
 2. \<gamma> (Trans s a ou s') = \<gamma> (Trans s1 a1 outOK s1')
 3. \<gamma> (Trans s a ou s') \<Longrightarrow> g (Trans s a ou s') = g (Trans s1 a1 outOK s1')
 4. \<Delta>1 s' vl' s1' ?vl1'
[PROOF STEP]
show "consume ?trn1 vl1 vl1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. consume (Trans s1 a1 outOK s1') vl1 vl1'
[PROOF STEP]
using \<phi>1 f1
[PROOF STATE]
proof (prove)
using this:
\<phi> (Trans s1 a1 outOK s1')
f (Trans s1 a1 outOK s1') = v1

goal (1 subgoal):
 1. consume (Trans s1 a1 outOK s1') vl1 vl1'
[PROOF STEP]
unfolding consume_def ss1 vl1
[PROOF STATE]
proof (prove)
using this:
\<phi> (Trans s1 a1 outOK s1')
f (Trans s1 a1 outOK s1') = v1

goal (1 subgoal):
 1. if \<phi> (Trans s1 a1 outOK s1') then v1 # vl1' \<noteq> [] \<and> f (Trans s1 a1 outOK s1') = hd (v1 # vl1') \<and> vl1' = tl (v1 # vl1') else vl1' = v1 # vl1'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
consume (Trans s1 a1 outOK s1') vl1 vl1'

goal (3 subgoals):
 1. \<gamma> (Trans s a ou s') = \<gamma> (Trans s1 a1 outOK s1')
 2. \<gamma> (Trans s a ou s') \<Longrightarrow> g (Trans s a ou s') = g (Trans s1 a1 outOK s1')
 3. \<Delta>1 s' vl' s1' vl1'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<gamma> (Trans s a ou s') = \<gamma> (Trans s1 a1 outOK s1')
 2. \<gamma> (Trans s a ou s') \<Longrightarrow> g (Trans s a ou s') = g (Trans s1 a1 outOK s1')
 3. \<Delta>1 s' vl' s1' vl1'
[PROOF STEP]
show "\<gamma> ?trn = \<gamma> ?trn1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<gamma> (Trans s a ou s') = \<gamma> (Trans s1 a1 outOK s1')
[PROOF STEP]
unfolding a a1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<gamma> (Trans s (COMact (comReceivePost AID p PID pst uid vs)) ou s') = \<gamma> (Trans s1 (COMact (comReceivePost AID p PID pst1 uid vs)) outOK s1')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<gamma> (Trans s a ou s') = \<gamma> (Trans s1 a1 outOK s1')

goal (2 subgoals):
 1. \<gamma> (Trans s a ou s') \<Longrightarrow> g (Trans s a ou s') = g (Trans s1 a1 outOK s1')
 2. \<Delta>1 s' vl' s1' vl1'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<gamma> (Trans s a ou s') \<Longrightarrow> g (Trans s a ou s') = g (Trans s1 a1 outOK s1')
 2. \<Delta>1 s' vl' s1' vl1'
[PROOF STEP]
assume "\<gamma> ?trn"
[PROOF STATE]
proof (state)
this:
\<gamma> (Trans s a ou s')

goal (2 subgoals):
 1. \<gamma> (Trans s a ou s') \<Longrightarrow> g (Trans s a ou s') = g (Trans s1 a1 outOK s1')
 2. \<Delta>1 s' vl' s1' vl1'
[PROOF STEP]
thus "g ?trn = g ?trn1"
[PROOF STATE]
proof (prove)
using this:
\<gamma> (Trans s a ou s')

goal (1 subgoal):
 1. g (Trans s a ou s') = g (Trans s1 a1 outOK s1')
[PROOF STEP]
unfolding a a1 ou
[PROOF STATE]
proof (prove)
using this:
\<gamma> (Trans s (COMact (comReceivePost AID p PID pst uid vs)) outOK s')

goal (1 subgoal):
 1. g (Trans s (COMact (comReceivePost AID p PID pst uid vs)) outOK s') = g (Trans s1 (COMact (comReceivePost AID p PID pst1 uid vs)) outOK s1')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
g (Trans s a ou s') = g (Trans s1 a1 outOK s1')

goal (1 subgoal):
 1. \<Delta>1 s' vl' s1' vl1'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Delta>1 s' vl' s1' vl1'
[PROOF STEP]
show "\<Delta>1 s' vl' s1' vl1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Delta>1 s' vl' s1' vl1'
[PROOF STEP]
using l AID' c s's1'
[PROOF STATE]
proof (prove)
using this:
length vl = length vl1
AID \<in>\<in> serverApiIDs s'
consume (Trans s a ou s') vl vl'
eqButPID s' s1'

goal (1 subgoal):
 1. \<Delta>1 s' vl' s1' vl1'
[PROOF STEP]
unfolding \<Delta>1_def vl vl1
[PROOF STATE]
proof (prove)
using this:
length (v # vl') = length (v1 # vl1')
AID \<in>\<in> serverApiIDs s'
consume (Trans s a ou s') (v # vl') vl'
eqButPID s' s1'

goal (1 subgoal):
 1. AID \<in>\<in> serverApiIDs s' \<and> eqButPID s' s1' \<and> length vl' = length vl1'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Delta>1 s' vl' s1' vl1'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
match \<Delta>1 s s1 vl1 a ou s' vl'

goal (1 subgoal):
 1. \<nexists>p pst uid vs. a = COMact (comReceivePost AID p PID pst uid vs) \<and> ou = outOK \<Longrightarrow> match \<Delta>1 s s1 vl1 a ou s' vl'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<nexists>p pst uid vs. a = COMact (comReceivePost AID p PID pst uid vs) \<and> ou = outOK \<Longrightarrow> match \<Delta>1 s s1 vl1 a ou s' vl'
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<nexists>p pst uid vs. a = COMact (comReceivePost AID p PID pst uid vs) \<and> ou = outOK

goal (1 subgoal):
 1. \<nexists>p pst uid vs. a = COMact (comReceivePost AID p PID pst uid vs) \<and> ou = outOK \<Longrightarrow> match \<Delta>1 s s1 vl1 a ou s' vl'
[PROOF STEP]
note a = False
[PROOF STATE]
proof (state)
this:
\<nexists>p pst uid vs. a = COMact (comReceivePost AID p PID pst uid vs) \<and> ou = outOK

goal (1 subgoal):
 1. \<nexists>p pst uid vs. a = COMact (comReceivePost AID p PID pst uid vs) \<and> ou = outOK \<Longrightarrow> match \<Delta>1 s s1 vl1 a ou s' vl'
[PROOF STEP]
obtain s1' ou1 where step1: "step s1 a = (ou1, s1')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ou1 s1'. step s1 a = (ou1, s1') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
step s1 a = (ou1, s1')

goal (1 subgoal):
 1. \<nexists>p pst uid vs. a = COMact (comReceivePost AID p PID pst uid vs) \<and> ou = outOK \<Longrightarrow> match \<Delta>1 s s1 vl1 a ou s' vl'
[PROOF STEP]
let ?trn1 = "Trans s1 a ou1 s1'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<nexists>p pst uid vs. a = COMact (comReceivePost AID p PID pst uid vs) \<and> ou = outOK \<Longrightarrow> match \<Delta>1 s s1 vl1 a ou s' vl'
[PROOF STEP]
have \<phi>: "\<not> \<phi> ?trn"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> \<phi> (Trans s a ou s')
[PROOF STEP]
using a step \<phi>_def2
[PROOF STATE]
proof (prove)
using this:
\<nexists>p pst uid vs. a = COMact (comReceivePost AID p PID pst uid vs) \<and> ou = outOK
step s a = (ou, s')
\<phi> (Trans ?s ?a ?ou ?s') = (\<exists>uid p pst vs. ?a = COMact (comReceivePost AID p PID pst uid vs) \<and> ?ou = outOK)

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

goal (1 subgoal):
 1. \<nexists>p pst uid vs. a = COMact (comReceivePost AID p PID pst uid vs) \<and> ou = outOK \<Longrightarrow> match \<Delta>1 s s1 vl1 a ou s' vl'
[PROOF STEP]
have \<phi>1: "\<not> \<phi> ?trn1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> \<phi> (Trans s1 a ou1 s1')
[PROOF STEP]
using \<phi> ss1 step step1 eqButPID_step_\<phi>
[PROOF STATE]
proof (prove)
using this:
\<not> \<phi> (Trans s a ou s')
eqButPID s s1
step s a = (ou, s')
step s1 a = (ou1, s1')
\<lbrakk>eqButPID ?s ?s1.0; step ?s ?a = (?ou, ?s'); step ?s1.0 ?a = (?ou1.0, ?s1')\<rbrakk> \<Longrightarrow> \<phi> (Trans ?s ?a ?ou ?s') = \<phi> (Trans ?s1.0 ?a ?ou1.0 ?s1')

goal (1 subgoal):
 1. \<not> \<phi> (Trans s1 a ou1 s1')
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> \<phi> (Trans s1 a ou1 s1')

goal (1 subgoal):
 1. \<nexists>p pst uid vs. a = COMact (comReceivePost AID p PID pst uid vs) \<and> ou = outOK \<Longrightarrow> match \<Delta>1 s s1 vl1 a ou s' vl'
[PROOF STEP]
have s's1': "eqButPID s' s1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqButPID s' s1'
[PROOF STEP]
using ss1 step step1 eqButPID_step
[PROOF STATE]
proof (prove)
using this:
eqButPID s s1
step s a = (ou, s')
step s1 a = (ou1, s1')
\<lbrakk>eqButPID ?s ?s1.0; step ?s ?a = (?ou, ?s'); step ?s1.0 ?a = (?ou1.0, ?s1')\<rbrakk> \<Longrightarrow> eqButPID ?s' ?s1'

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

goal (1 subgoal):
 1. \<nexists>p pst uid vs. a = COMact (comReceivePost AID p PID pst uid vs) \<and> ou = outOK \<Longrightarrow> match \<Delta>1 s s1 vl1 a ou s' vl'
[PROOF STEP]
have ouou1: "\<gamma> ?trn \<Longrightarrow> ou = ou1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<gamma> (Trans s a ou s') \<Longrightarrow> ou = ou1
[PROOF STEP]
using eqButPID_step_\<gamma>_out ss1 step step1 T rs1 rsT
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>eqButPID ?s ?s1.0; step ?s ?a = (?ou, ?s'); step ?s1.0 ?a = (?ou1.0, ?s1'); reachNT ?s; \<not> T (Trans ?s ?a ?ou ?s'); reach ?s1.0; \<gamma> (Trans ?s ?a ?ou ?s')\<rbrakk> \<Longrightarrow> ?ou = ?ou1.0
eqButPID s s1
step s a = (ou, s')
step s1 a = (ou1, s1')
\<not> T (Trans s a ou s')
reach s1
reachNT s

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

goal (1 subgoal):
 1. \<nexists>p pst uid vs. a = COMact (comReceivePost AID p PID pst uid vs) \<and> ou = outOK \<Longrightarrow> match \<Delta>1 s s1 vl1 a ou s' vl'
[PROOF STEP]
have AID': "AID \<in>\<in> serverApiIDs s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AID \<in>\<in> serverApiIDs s'
[PROOF STEP]
using AID step rs
[PROOF STATE]
proof (prove)
using this:
AID \<in>\<in> serverApiIDs s
step s a = (ou, s')
reach s

goal (1 subgoal):
 1. AID \<in>\<in> serverApiIDs s'
[PROOF STEP]
using IDs_mono
[PROOF STATE]
proof (prove)
using this:
AID \<in>\<in> serverApiIDs s
step s a = (ou, s')
reach s
\<lbrakk>step ?s ?a = (?ou, ?s'); ?uid \<in>\<in> userIDs ?s\<rbrakk> \<Longrightarrow> ?uid \<in>\<in> userIDs ?s'
\<lbrakk>step ?s ?a = (?ou, ?s'); ?nid \<in>\<in> postIDs ?s\<rbrakk> \<Longrightarrow> ?nid \<in>\<in> postIDs ?s'
\<lbrakk>step ?s ?a = (?ou, ?s'); ?aid \<in>\<in> clientApiIDs ?s\<rbrakk> \<Longrightarrow> ?aid \<in>\<in> clientApiIDs ?s'
\<lbrakk>step ?s ?a = (?ou, ?s'); ?sid \<in>\<in> serverApiIDs ?s\<rbrakk> \<Longrightarrow> ?sid \<in>\<in> serverApiIDs ?s'
\<lbrakk>step ?s ?a = (?ou, ?s'); ?nid \<in>\<in> outerPostIDs ?s ?aid\<rbrakk> \<Longrightarrow> ?nid \<in>\<in> outerPostIDs ?s' ?aid

goal (1 subgoal):
 1. AID \<in>\<in> serverApiIDs s'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
AID \<in>\<in> serverApiIDs s'

goal (1 subgoal):
 1. \<nexists>p pst uid vs. a = COMact (comReceivePost AID p PID pst uid vs) \<and> ou = outOK \<Longrightarrow> match \<Delta>1 s s1 vl1 a ou s' vl'
[PROOF STEP]
have vl': "vl' = vl"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vl' = vl
[PROOF STEP]
using c \<phi>
[PROOF STATE]
proof (prove)
using this:
consume (Trans s a ou s') vl vl'
\<not> \<phi> (Trans s a ou s')

goal (1 subgoal):
 1. vl' = vl
[PROOF STEP]
unfolding consume_def
[PROOF STATE]
proof (prove)
using this:
if \<phi> (Trans s a ou s') then vl \<noteq> [] \<and> f (Trans s a ou s') = hd vl \<and> vl' = tl vl else vl' = vl
\<not> \<phi> (Trans s a ou s')

goal (1 subgoal):
 1. vl' = vl
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vl' = vl

goal (1 subgoal):
 1. \<nexists>p pst uid vs. a = COMact (comReceivePost AID p PID pst uid vs) \<and> ou = outOK \<Longrightarrow> match \<Delta>1 s s1 vl1 a ou s' vl'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. match \<Delta>1 s s1 vl1 a ou s' vl'
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. validTrans (Trans s1 ?a1.0 ?ou1.0 ?s1')
 2. consume (Trans s1 ?a1.0 ?ou1.0 ?s1') vl1 ?vl1'
 3. \<gamma> (Trans s a ou s') = \<gamma> (Trans s1 ?a1.0 ?ou1.0 ?s1')
 4. \<gamma> (Trans s a ou s') \<Longrightarrow> g (Trans s a ou s') = g (Trans s1 ?a1.0 ?ou1.0 ?s1')
 5. \<Delta>1 s' vl' ?s1' ?vl1'
[PROOF STEP]
show "validTrans ?trn1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. validTrans (Trans s1 a ou1 s1')
[PROOF STEP]
using step1
[PROOF STATE]
proof (prove)
using this:
step s1 a = (ou1, s1')

goal (1 subgoal):
 1. validTrans (Trans s1 a ou1 s1')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
validTrans (Trans s1 a ou1 s1')

goal (4 subgoals):
 1. consume (Trans s1 a ou1 s1') vl1 ?vl1'
 2. \<gamma> (Trans s a ou s') = \<gamma> (Trans s1 a ou1 s1')
 3. \<gamma> (Trans s a ou s') \<Longrightarrow> g (Trans s a ou s') = g (Trans s1 a ou1 s1')
 4. \<Delta>1 s' vl' s1' ?vl1'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. consume (Trans s1 a ou1 s1') vl1 ?vl1'
 2. \<gamma> (Trans s a ou s') = \<gamma> (Trans s1 a ou1 s1')
 3. \<gamma> (Trans s a ou s') \<Longrightarrow> g (Trans s a ou s') = g (Trans s1 a ou1 s1')
 4. \<Delta>1 s' vl' s1' ?vl1'
[PROOF STEP]
show "consume ?trn1 vl1 vl1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. consume (Trans s1 a ou1 s1') vl1 vl1
[PROOF STEP]
using \<phi>1
[PROOF STATE]
proof (prove)
using this:
\<not> \<phi> (Trans s1 a ou1 s1')

goal (1 subgoal):
 1. consume (Trans s1 a ou1 s1') vl1 vl1
[PROOF STEP]
unfolding consume_def ss1
[PROOF STATE]
proof (prove)
using this:
\<not> \<phi> (Trans s1 a ou1 s1')

goal (1 subgoal):
 1. if \<phi> (Trans s1 a ou1 s1') then vl1 \<noteq> [] \<and> f (Trans s1 a ou1 s1') = hd vl1 \<and> vl1 = tl vl1 else vl1 = vl1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
consume (Trans s1 a ou1 s1') vl1 vl1

goal (3 subgoals):
 1. \<gamma> (Trans s a ou s') = \<gamma> (Trans s1 a ou1 s1')
 2. \<gamma> (Trans s a ou s') \<Longrightarrow> g (Trans s a ou s') = g (Trans s1 a ou1 s1')
 3. \<Delta>1 s' vl' s1' vl1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<gamma> (Trans s a ou s') = \<gamma> (Trans s1 a ou1 s1')
 2. \<gamma> (Trans s a ou s') \<Longrightarrow> g (Trans s a ou s') = g (Trans s1 a ou1 s1')
 3. \<Delta>1 s' vl' s1' vl1
[PROOF STEP]
show 1: "\<gamma> ?trn = \<gamma> ?trn1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<gamma> (Trans s a ou s') = \<gamma> (Trans s1 a ou1 s1')
[PROOF STEP]
unfolding ss1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<gamma> (Trans s a ou s') = \<gamma> (Trans s1 a ou1 s1')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<gamma> (Trans s a ou s') = \<gamma> (Trans s1 a ou1 s1')

goal (2 subgoals):
 1. \<gamma> (Trans s a ou s') \<Longrightarrow> g (Trans s a ou s') = g (Trans s1 a ou1 s1')
 2. \<Delta>1 s' vl' s1' vl1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<gamma> (Trans s a ou s') \<Longrightarrow> g (Trans s a ou s') = g (Trans s1 a ou1 s1')
 2. \<Delta>1 s' vl' s1' vl1
[PROOF STEP]
assume "\<gamma> ?trn"
[PROOF STATE]
proof (state)
this:
\<gamma> (Trans s a ou s')

goal (2 subgoals):
 1. \<gamma> (Trans s a ou s') \<Longrightarrow> g (Trans s a ou s') = g (Trans s1 a ou1 s1')
 2. \<Delta>1 s' vl' s1' vl1
[PROOF STEP]
hence "ou = ou1"
[PROOF STATE]
proof (prove)
using this:
\<gamma> (Trans s a ou s')

goal (1 subgoal):
 1. ou = ou1
[PROOF STEP]
using ouou1
[PROOF STATE]
proof (prove)
using this:
\<gamma> (Trans s a ou s')
\<gamma> (Trans s a ou s') \<Longrightarrow> ou = ou1

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

goal (2 subgoals):
 1. \<gamma> (Trans s a ou s') \<Longrightarrow> g (Trans s a ou s') = g (Trans s1 a ou1 s1')
 2. \<Delta>1 s' vl' s1' vl1
[PROOF STEP]
thus "g ?trn = g ?trn1"
[PROOF STATE]
proof (prove)
using this:
ou = ou1

goal (1 subgoal):
 1. g (Trans s a ou s') = g (Trans s1 a ou1 s1')
[PROOF STEP]
using ouou1
[PROOF STATE]
proof (prove)
using this:
ou = ou1
\<gamma> (Trans s a ou s') \<Longrightarrow> ou = ou1

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

goal (1 subgoal):
 1. \<Delta>1 s' vl' s1' vl1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Delta>1 s' vl' s1' vl1
[PROOF STEP]
show "\<Delta>1 s' vl' s1' vl1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Delta>1 s' vl' s1' vl1
[PROOF STEP]
using a l s's1' AID'
[PROOF STATE]
proof (prove)
using this:
\<nexists>p pst uid vs. a = COMact (comReceivePost AID p PID pst uid vs) \<and> ou = outOK
length vl = length vl1
eqButPID s' s1'
AID \<in>\<in> serverApiIDs s'

goal (1 subgoal):
 1. \<Delta>1 s' vl' s1' vl1
[PROOF STEP]
unfolding \<Delta>1_def vl'
[PROOF STATE]
proof (prove)
using this:
\<nexists>p pst uid vs. a = COMact (comReceivePost AID p PID pst uid vs) \<and> ou = outOK
length vl = length vl1
eqButPID s' s1'
AID \<in>\<in> serverApiIDs s'

goal (1 subgoal):
 1. AID \<in>\<in> serverApiIDs s' \<and> eqButPID s' s1' \<and> length vl = length vl1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Delta>1 s' vl' s1' vl1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
match \<Delta>1 s s1 vl1 a ou s' vl'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
match \<Delta>1 s s1 vl1 a ou s' vl'

goal (1 subgoal):
 1. match \<Delta>1 s s1 vl1 a ou s' vl' \<or> ignore \<Delta>1 s s1 vl1 a ou s' vl'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
match \<Delta>1 s s1 vl1 a ou s' vl'

goal (1 subgoal):
 1. match \<Delta>1 s s1 vl1 a ou s' vl' \<or> ignore \<Delta>1 s s1 vl1 a ou s' vl'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
match \<Delta>1 s s1 vl1 a ou s' vl' \<or> ignore \<Delta>1 s s1 vl1 a ou s' vl'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
match \<Delta>1 s s1 vl1 a ou s' vl' \<or> ignore \<Delta>1 s s1 vl1 a ou s' vl'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
reaction \<Delta>1 s vl s1 vl1

goal (1 subgoal):
 1. iaction \<Delta>1 s vl s1 vl1 \<or> (vl = [] \<longrightarrow> vl1 = []) \<and> reaction \<Delta>1 s vl s1 vl1
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
reaction \<Delta>1 s vl s1 vl1

goal (1 subgoal):
 1. iaction \<Delta>1 s vl s1 vl1 \<or> (vl = [] \<longrightarrow> vl1 = []) \<and> reaction \<Delta>1 s vl s1 vl1
[PROOF STEP]
using l
[PROOF STATE]
proof (prove)
using this:
reaction \<Delta>1 s vl s1 vl1
length vl = length vl1

goal (1 subgoal):
 1. iaction \<Delta>1 s vl s1 vl1 \<or> (vl = [] \<longrightarrow> vl1 = []) \<and> reaction \<Delta>1 s vl s1 vl1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
iaction \<Delta>1 s vl s1 vl1 \<or> (vl = [] \<longrightarrow> vl1 = []) \<and> reaction \<Delta>1 s vl s1 vl1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
iaction \<Delta>1 s vl s1 vl1 \<or> (vl = [] \<longrightarrow> vl1 = []) \<and> reaction \<Delta>1 s vl s1 vl1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem Post_secure: secure
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. secure
[PROOF STEP]
apply (rule unwind_decomp_secure_graph[of Gr \<Delta>0])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<forall>\<Delta>\<in>Domain Gr. \<exists>\<Delta>s\<subseteq>Domain Gr. (\<Delta>, \<Delta>s) \<in> Gr
 2. \<Delta>0 \<in> Domain Gr
 3. \<And>vl vl1. B vl vl1 \<Longrightarrow> \<Delta>0 istate vl istate vl1
 4. \<And>\<Delta>. unwind_exit \<Delta> \<or> (\<forall>\<Delta>s. (\<Delta>, \<Delta>s) \<in> Gr \<longrightarrow> unwind_cont \<Delta> \<Delta>s)
[PROOF STEP]
unfolding Gr_def
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<forall>\<Delta>\<in>Domain {(\<Delta>0, {\<Delta>0, \<Delta>1}), (\<Delta>1, {\<Delta>1})}. \<exists>\<Delta>s\<subseteq>Domain {(\<Delta>0, {\<Delta>0, \<Delta>1}), (\<Delta>1, {\<Delta>1})}. (\<Delta>, \<Delta>s) \<in> {(\<Delta>0, {\<Delta>0, \<Delta>1}), (\<Delta>1, {\<Delta>1})}
 2. \<Delta>0 \<in> Domain {(\<Delta>0, {\<Delta>0, \<Delta>1}), (\<Delta>1, {\<Delta>1})}
 3. \<And>vl vl1. B vl vl1 \<Longrightarrow> \<Delta>0 istate vl istate vl1
 4. \<And>\<Delta>. unwind_exit \<Delta> \<or> (\<forall>\<Delta>s. (\<Delta>, \<Delta>s) \<in> {(\<Delta>0, {\<Delta>0, \<Delta>1}), (\<Delta>1, {\<Delta>1})} \<longrightarrow> unwind_cont \<Delta> \<Delta>s)
[PROOF STEP]
apply (simp, smt insert_subset order_refl)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<Delta>0 \<in> Domain {(\<Delta>0, {\<Delta>0, \<Delta>1}), (\<Delta>1, {\<Delta>1})}
 2. \<And>vl vl1. B vl vl1 \<Longrightarrow> \<Delta>0 istate vl istate vl1
 3. \<And>\<Delta>. unwind_exit \<Delta> \<or> (\<forall>\<Delta>s. (\<Delta>, \<Delta>s) \<in> {(\<Delta>0, {\<Delta>0, \<Delta>1}), (\<Delta>1, {\<Delta>1})} \<longrightarrow> unwind_cont \<Delta> \<Delta>s)
[PROOF STEP]
using istate_\<Delta>0 unwind_cont_\<Delta>0 unwind_cont_\<Delta>1
[PROOF STATE]
proof (prove)
using this:
B ?vl ?vl1.0 \<Longrightarrow> \<Delta>0 istate ?vl istate ?vl1.0
unwind_cont \<Delta>0 {\<Delta>0, \<Delta>1}
unwind_cont \<Delta>1 {\<Delta>1}

goal (3 subgoals):
 1. \<Delta>0 \<in> Domain {(\<Delta>0, {\<Delta>0, \<Delta>1}), (\<Delta>1, {\<Delta>1})}
 2. \<And>vl vl1. B vl vl1 \<Longrightarrow> \<Delta>0 istate vl istate vl1
 3. \<And>\<Delta>. unwind_exit \<Delta> \<or> (\<forall>\<Delta>s. (\<Delta>, \<Delta>s) \<in> {(\<Delta>0, {\<Delta>0, \<Delta>1}), (\<Delta>1, {\<Delta>1})} \<longrightarrow> unwind_cont \<Delta> \<Delta>s)
[PROOF STEP]
unfolding Gr_def
[PROOF STATE]
proof (prove)
using this:
B ?vl ?vl1.0 \<Longrightarrow> \<Delta>0 istate ?vl istate ?vl1.0
unwind_cont \<Delta>0 {\<Delta>0, \<Delta>1}
unwind_cont \<Delta>1 {\<Delta>1}

goal (3 subgoals):
 1. \<Delta>0 \<in> Domain {(\<Delta>0, {\<Delta>0, \<Delta>1}), (\<Delta>1, {\<Delta>1})}
 2. \<And>vl vl1. B vl vl1 \<Longrightarrow> \<Delta>0 istate vl istate vl1
 3. \<And>\<Delta>. unwind_exit \<Delta> \<or> (\<forall>\<Delta>s. (\<Delta>, \<Delta>s) \<in> {(\<Delta>0, {\<Delta>0, \<Delta>1}), (\<Delta>1, {\<Delta>1})} \<longrightarrow> unwind_cont \<Delta> \<Delta>s)
[PROOF STEP]
by auto


[STATEMENT]
lemma apx_transitive_2:
  assumes "x \<sqsubseteq> y"
      and "y \<sqsubseteq> z"
    shows "x \<sqsubseteq> z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<sqsubseteq> z
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<sqsubseteq> z
[PROOF STEP]
have "C z \<le> C (y \<squnion> n(y) * top)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C z \<le> C (y \<squnion> n y * top)
[PROOF STEP]
using assms(2) apx_def le_inf_iff
[PROOF STATE]
proof (prove)
using this:
y \<sqsubseteq> z
(?x \<sqsubseteq> ?y) = (?x \<le> ?y \<squnion> L \<and> C ?y \<le> ?x \<squnion> n ?x * top)
(?x \<le> ?y \<sqinter> ?z) = (?x \<le> ?y \<and> ?x \<le> ?z)

goal (1 subgoal):
 1. C z \<le> C (y \<squnion> n y * top)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
C z \<le> C (y \<squnion> n y * top)

goal (1 subgoal):
 1. x \<sqsubseteq> z
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
C z \<le> C (y \<squnion> n y * top)

goal (1 subgoal):
 1. x \<sqsubseteq> z
[PROOF STEP]
have "... = C y \<squnion> n(y) * top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C (y \<squnion> n y * top) = C y \<squnion> n y * top
[PROOF STEP]
by (simp add: C_n_mult_closed inf_sup_distrib1)
[PROOF STATE]
proof (state)
this:
C (y \<squnion> n y * top) = C y \<squnion> n y * top

goal (1 subgoal):
 1. x \<sqsubseteq> z
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
C (y \<squnion> n y * top) = C y \<squnion> n y * top

goal (1 subgoal):
 1. x \<sqsubseteq> z
[PROOF STEP]
have "... \<le> x \<squnion> n(x) * top \<squnion> n(y) * top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C y \<squnion> n y * top \<le> x \<squnion> n x * top \<squnion> n y * top
[PROOF STEP]
using assms(1) apx_def sup_left_isotone
[PROOF STATE]
proof (prove)
using this:
x \<sqsubseteq> y
(?x \<sqsubseteq> ?y) = (?x \<le> ?y \<squnion> L \<and> C ?y \<le> ?x \<squnion> n ?x * top)
?x \<le> ?y \<Longrightarrow> ?x \<squnion> ?z \<le> ?y \<squnion> ?z

goal (1 subgoal):
 1. C y \<squnion> n y * top \<le> x \<squnion> n x * top \<squnion> n y * top
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
C y \<squnion> n y * top \<le> x \<squnion> n x * top \<squnion> n y * top

goal (1 subgoal):
 1. x \<sqsubseteq> z
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
C y \<squnion> n y * top \<le> x \<squnion> n x * top \<squnion> n y * top

goal (1 subgoal):
 1. x \<sqsubseteq> z
[PROOF STEP]
have "... = x \<squnion> n(x) * top \<squnion> n(C y) * top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<squnion> n x * top \<squnion> n y * top = x \<squnion> n x * top \<squnion> n (C y) * top
[PROOF STEP]
by (simp add: n_C)
[PROOF STATE]
proof (state)
this:
x \<squnion> n x * top \<squnion> n y * top = x \<squnion> n x * top \<squnion> n (C y) * top

goal (1 subgoal):
 1. x \<sqsubseteq> z
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x \<squnion> n x * top \<squnion> n y * top = x \<squnion> n x * top \<squnion> n (C y) * top

goal (1 subgoal):
 1. x \<sqsubseteq> z
[PROOF STEP]
have "... \<le> x \<squnion> n(x) * top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<squnion> n x * top \<squnion> n (C y) * top \<le> x \<squnion> n x * top
[PROOF STEP]
by (metis assms(1) sup_assoc sup_idem sup_right_isotone apx_def mult_left_isotone n_add_n_top n_isotone)
[PROOF STATE]
proof (state)
this:
x \<squnion> n x * top \<squnion> n (C y) * top \<le> x \<squnion> n x * top

goal (1 subgoal):
 1. x \<sqsubseteq> z
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
C z \<le> x \<squnion> n x * top
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
C z \<le> x \<squnion> n x * top

goal (1 subgoal):
 1. x \<sqsubseteq> z
[PROOF STEP]
by (smt assms sup_assoc sup_commute apx_def le_iff_sup)
[PROOF STATE]
proof (state)
this:
x \<sqsubseteq> z

goal:
No subgoals!
[PROOF STEP]
qed