[STATEMENT]
lemma eqButPID_step_eq:
assumes ss1: "eqButPID s s1"
and a: "a = Uact (uPost uid p PID pst)" "ou = outOK"
and step: "step s a = (ou, s')" and step1: "step s1 a = (ou', s1')"
shows "s' = s1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s' = s1'
[PROOF STEP]
using ss1 step step1
[PROOF STATE]
proof (prove)
using this:
eqButPID s s1
step s a = (ou, s')
step s1 a = (ou', s1')

goal (1 subgoal):
 1. s' = s1'
[PROOF STEP]
using eqButPID_stateSelectors[OF ss1]
eqButPID_update[OF ss1] (* eqButPID_setTextPost[OF ss1] *) eqButPID_setShared[OF ss1]
[PROOF STATE]
proof (prove)
using this:
eqButPID s s1
step s a = (ou, s')
step s1 a = (ou', s1')
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> eeqButPID (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> 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> eeqButPID_F (sharedWith s) (sharedWith s1) \<and> IDsOK s = IDsOK s1
(post s)(PID := ?txt) = (post s1)(PID := ?txt)
(sharedWith s)(PID := map (\<lambda>(aID, uu_). (aID, ?b)) (sharedWith s PID)) = (sharedWith s1)(PID := map (\<lambda>(aID, uu_). (aID, ?b)) (sharedWith s1 PID))

goal (1 subgoal):
 1. s' = s1'
[PROOF STEP]
unfolding a
[PROOF STATE]
proof (prove)
using this:
eqButPID s s1
step s (Uact (uPost uid p PID pst)) = (outOK, s')
step s1 (Uact (uPost uid p PID pst)) = (ou', s1')
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> eeqButPID (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> 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> eeqButPID_F (sharedWith s) (sharedWith s1) \<and> IDsOK s = IDsOK s1
(post s)(PID := ?txt) = (post s1)(PID := ?txt)
(sharedWith s)(PID := map (\<lambda>(aID, uu_). (aID, ?b)) (sharedWith s PID)) = (sharedWith s1)(PID := map (\<lambda>(aID, uu_). (aID, ?b)) (sharedWith s1 PID))

goal (1 subgoal):
 1. s' = s1'
[PROOF STEP]
by (auto simp: u_defs)


[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:
corrFrom emptyPost vl1 \<and> (vl = [] \<longrightarrow> vl1 = []) \<and> map PValS_tgtAPI (filter isPValS vl) = map PValS_tgtAPI (filter isPValS vl1)

goal (1 subgoal):
 1. PID \<notin> set (postIDs \<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> post \<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> PID = emptyPost \<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> corrFrom (post \<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> PID) vl1 \<and> (vl = [] \<longrightarrow> vl1 = []) \<and> map PValS_tgtAPI (filter isPValS vl) = map PValS_tgtAPI (filter isPValS 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 pPID: "post s PID = emptyPost"
  and ch: "corrFrom (post s1 PID) vl1"
  and l: "map PValS_tgtAPI (filter isPValS vl) = map PValS_tgtAPI (filter isPValS vl1)"
  and PID: "\<not> PID \<in>\<in> postIDs s" and vlvl1: "vl = [] \<Longrightarrow> vl1 = []"
[PROOF STATE]
proof (prove)
using this:
reachNT s
reach s1
\<Delta>0 s vl s1 vl1

goal (1 subgoal):
 1. (reach s &&& s1 = s &&& post s PID = emptyPost) &&& (corrFrom (post s1 PID) vl1 &&& map PValS_tgtAPI (filter isPValS vl) = map PValS_tgtAPI (filter isPValS vl1)) &&& PID \<notin> set (postIDs s) &&& (vl = [] \<Longrightarrow> vl1 = [])
[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 &&& post s PID = emptyPost) &&& (corrFrom (post s1 PID) vl1 &&& map PValS_tgtAPI (filter isPValS vl) = map PValS_tgtAPI (filter isPValS vl1)) &&& PID \<notin> set (postIDs s) &&& (vl = [] \<Longrightarrow> vl1 = [])
[PROOF STEP]
unfolding \<Delta>0_def
[PROOF STATE]
proof (prove)
using this:
reachNT s
reach s1
PID \<notin> set (postIDs s) \<and> post s PID = emptyPost \<and> s = s1 \<and> corrFrom (post s1 PID) vl1 \<and> (vl = [] \<longrightarrow> vl1 = []) \<and> map PValS_tgtAPI (filter isPValS vl) = map PValS_tgtAPI (filter isPValS vl1)
reachNT ?s \<Longrightarrow> reach ?s

goal (1 subgoal):
 1. (reach s &&& s1 = s &&& post s PID = emptyPost) &&& (corrFrom (post s1 PID) vl1 &&& map PValS_tgtAPI (filter isPValS vl) = map PValS_tgtAPI (filter isPValS vl1)) &&& PID \<notin> set (postIDs s) &&& (vl = [] \<Longrightarrow> vl1 = [])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
reach s
s1 = s
post s PID = emptyPost
corrFrom (post s1 PID) vl1
map PValS_tgtAPI (filter isPValS vl) = map PValS_tgtAPI (filter isPValS vl1)
PID \<notin> set (postIDs s)
vl = [] \<Longrightarrow> 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]
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 PID step
[PROOF STATE]
proof (prove)
using this:
PID \<notin> set (postIDs 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:
PID \<notin> set (postIDs s)
step s a = (ou, s')

goal (1 subgoal):
 1. \<not> ((\<exists>uid p pst. a = Uact (uPost uid p PID pst) \<and> ou = outOK) \<or> (\<exists>uid p aid. a = COMact (comSendPost uid p aid PID) \<and> ou \<noteq> outErr))
[PROOF STEP]
(* [OF step] *)
[PROOF STATE]
proof (prove)
using this:
PID \<notin> set (postIDs s)
step s a = (ou, s')

goal (1 subgoal):
 1. \<not> ((\<exists>uid p pst. a = Uact (uPost uid p PID pst) \<and> ou = outOK) \<or> (\<exists>uid p aid. a = COMact (comSendPost uid p aid PID) \<and> ou \<noteq> outErr))
[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 pPID': "post s' PID = emptyPost"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. post s' PID = emptyPost
[PROOF STEP]
using pPID PID step
[PROOF STATE]
proof (prove)
using this:
post s PID = emptyPost
PID \<notin> set (postIDs s)
step s a = (ou, s')

goal (1 subgoal):
 1. post s' PID = emptyPost
[PROOF STEP]
apply(cases a)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>x1. \<lbrakk>post s PID = emptyPost; PID \<notin> set (postIDs s); step s a = (ou, s'); a = Sact x1\<rbrakk> \<Longrightarrow> post s' PID = emptyPost
 2. \<And>x2. \<lbrakk>post s PID = emptyPost; PID \<notin> set (postIDs s); step s a = (ou, s'); a = Cact x2\<rbrakk> \<Longrightarrow> post s' PID = emptyPost
 3. \<And>x3. \<lbrakk>post s PID = emptyPost; PID \<notin> set (postIDs s); step s a = (ou, s'); a = Dact x3\<rbrakk> \<Longrightarrow> post s' PID = emptyPost
 4. \<And>x4. \<lbrakk>post s PID = emptyPost; PID \<notin> set (postIDs s); step s a = (ou, s'); a = Uact x4\<rbrakk> \<Longrightarrow> post s' PID = emptyPost
 5. \<And>x5. \<lbrakk>post s PID = emptyPost; PID \<notin> set (postIDs s); step s a = (ou, s'); a = Ract x5\<rbrakk> \<Longrightarrow> post s' PID = emptyPost
 6. \<And>x6. \<lbrakk>post s PID = emptyPost; PID \<notin> set (postIDs s); step s a = (ou, s'); a = Lact x6\<rbrakk> \<Longrightarrow> post s' PID = emptyPost
 7. \<And>x7. \<lbrakk>post s PID = emptyPost; PID \<notin> set (postIDs s); step s a = (ou, s'); a = COMact x7\<rbrakk> \<Longrightarrow> post s' PID = emptyPost
[PROOF STEP]
subgoal for x1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>post s PID = emptyPost; PID \<notin> set (postIDs s); step s a = (ou, s'); a = Sact x1\<rbrakk> \<Longrightarrow> post s' PID = emptyPost
[PROOF STEP]
apply(cases x1, auto simp: all_defs)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>x2. \<lbrakk>post s PID = emptyPost; PID \<notin> set (postIDs s); step s a = (ou, s'); a = Cact x2\<rbrakk> \<Longrightarrow> post s' PID = emptyPost
 2. \<And>x3. \<lbrakk>post s PID = emptyPost; PID \<notin> set (postIDs s); step s a = (ou, s'); a = Dact x3\<rbrakk> \<Longrightarrow> post s' PID = emptyPost
 3. \<And>x4. \<lbrakk>post s PID = emptyPost; PID \<notin> set (postIDs s); step s a = (ou, s'); a = Uact x4\<rbrakk> \<Longrightarrow> post s' PID = emptyPost
 4. \<And>x5. \<lbrakk>post s PID = emptyPost; PID \<notin> set (postIDs s); step s a = (ou, s'); a = Ract x5\<rbrakk> \<Longrightarrow> post s' PID = emptyPost
 5. \<And>x6. \<lbrakk>post s PID = emptyPost; PID \<notin> set (postIDs s); step s a = (ou, s'); a = Lact x6\<rbrakk> \<Longrightarrow> post s' PID = emptyPost
 6. \<And>x7. \<lbrakk>post s PID = emptyPost; PID \<notin> set (postIDs s); step s a = (ou, s'); a = COMact x7\<rbrakk> \<Longrightarrow> post s' PID = emptyPost
[PROOF STEP]
subgoal for x2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>post s PID = emptyPost; PID \<notin> set (postIDs s); step s a = (ou, s'); a = Cact x2\<rbrakk> \<Longrightarrow> post s' PID = emptyPost
[PROOF STEP]
apply(cases x2, auto simp: all_defs)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x3. \<lbrakk>post s PID = emptyPost; PID \<notin> set (postIDs s); step s a = (ou, s'); a = Dact x3\<rbrakk> \<Longrightarrow> post s' PID = emptyPost
 2. \<And>x4. \<lbrakk>post s PID = emptyPost; PID \<notin> set (postIDs s); step s a = (ou, s'); a = Uact x4\<rbrakk> \<Longrightarrow> post s' PID = emptyPost
 3. \<And>x5. \<lbrakk>post s PID = emptyPost; PID \<notin> set (postIDs s); step s a = (ou, s'); a = Ract x5\<rbrakk> \<Longrightarrow> post s' PID = emptyPost
 4. \<And>x6. \<lbrakk>post s PID = emptyPost; PID \<notin> set (postIDs s); step s a = (ou, s'); a = Lact x6\<rbrakk> \<Longrightarrow> post s' PID = emptyPost
 5. \<And>x7. \<lbrakk>post s PID = emptyPost; PID \<notin> set (postIDs s); step s a = (ou, s'); a = COMact x7\<rbrakk> \<Longrightarrow> post s' PID = emptyPost
[PROOF STEP]
subgoal for x3
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>post s PID = emptyPost; PID \<notin> set (postIDs s); step s a = (ou, s'); a = Dact x3\<rbrakk> \<Longrightarrow> post s' PID = emptyPost
[PROOF STEP]
apply(cases x3, auto simp: all_defs)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x4. \<lbrakk>post s PID = emptyPost; PID \<notin> set (postIDs s); step s a = (ou, s'); a = Uact x4\<rbrakk> \<Longrightarrow> post s' PID = emptyPost
 2. \<And>x5. \<lbrakk>post s PID = emptyPost; PID \<notin> set (postIDs s); step s a = (ou, s'); a = Ract x5\<rbrakk> \<Longrightarrow> post s' PID = emptyPost
 3. \<And>x6. \<lbrakk>post s PID = emptyPost; PID \<notin> set (postIDs s); step s a = (ou, s'); a = Lact x6\<rbrakk> \<Longrightarrow> post s' PID = emptyPost
 4. \<And>x7. \<lbrakk>post s PID = emptyPost; PID \<notin> set (postIDs s); step s a = (ou, s'); a = COMact x7\<rbrakk> \<Longrightarrow> post s' PID = emptyPost
[PROOF STEP]
subgoal for x4
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>post s PID = emptyPost; PID \<notin> set (postIDs s); step s a = (ou, s'); a = Uact x4\<rbrakk> \<Longrightarrow> post s' PID = emptyPost
[PROOF STEP]
apply(cases x4, auto simp: all_defs)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x5. \<lbrakk>post s PID = emptyPost; PID \<notin> set (postIDs s); step s a = (ou, s'); a = Ract x5\<rbrakk> \<Longrightarrow> post s' PID = emptyPost
 2. \<And>x6. \<lbrakk>post s PID = emptyPost; PID \<notin> set (postIDs s); step s a = (ou, s'); a = Lact x6\<rbrakk> \<Longrightarrow> post s' PID = emptyPost
 3. \<And>x7. \<lbrakk>post s PID = emptyPost; PID \<notin> set (postIDs s); step s a = (ou, s'); a = COMact x7\<rbrakk> \<Longrightarrow> post s' PID = emptyPost
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>post s PID = emptyPost; PID \<notin> set (postIDs s); step s a = (ou, s'); a = Ract x5_\<rbrakk> \<Longrightarrow> post s' PID = emptyPost
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x6. \<lbrakk>post s PID = emptyPost; PID \<notin> set (postIDs s); step s a = (ou, s'); a = Lact x6\<rbrakk> \<Longrightarrow> post s' PID = emptyPost
 2. \<And>x7. \<lbrakk>post s PID = emptyPost; PID \<notin> set (postIDs s); step s a = (ou, s'); a = COMact x7\<rbrakk> \<Longrightarrow> post s' PID = emptyPost
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>post s PID = emptyPost; PID \<notin> set (postIDs s); step s a = (ou, s'); a = Lact x6_\<rbrakk> \<Longrightarrow> post s' PID = emptyPost
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x7. \<lbrakk>post s PID = emptyPost; PID \<notin> set (postIDs s); step s a = (ou, s'); a = COMact x7\<rbrakk> \<Longrightarrow> post s' PID = emptyPost
[PROOF STEP]
subgoal for x7
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>post s PID = emptyPost; PID \<notin> set (postIDs s); step s a = (ou, s'); a = COMact x7\<rbrakk> \<Longrightarrow> post s' PID = emptyPost
[PROOF STEP]
apply(cases x7, auto simp: all_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:
post s' PID = emptyPost

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> uid p. a = Cact (cPost uid p PID) \<and> ou = outOK")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>uid p. a = Cact (cPost uid p PID) \<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>uid p. a = Cact (cPost uid p PID) \<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>uid p. a = Cact (cPost uid p PID) \<and> ou = outOK

goal (2 subgoals):
 1. \<exists>uid p. a = Cact (cPost uid p PID) \<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>uid p. a = Cact (cPost uid p PID) \<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>uid p. a = Cact (cPost uid p PID) \<and> ou = outOK
[PROOF STEP]
obtain uid p where a: "a = Cact (cPost uid p PID)" and ou: "ou = outOK"
[PROOF STATE]
proof (prove)
using this:
\<exists>uid p. a = Cact (cPost uid p PID) \<and> ou = outOK

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

goal (2 subgoals):
 1. \<exists>uid p. a = Cact (cPost uid p PID) \<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>uid p. a = Cact (cPost uid p PID) \<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 PID': "PID \<in>\<in> postIDs s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. PID \<in>\<in> postIDs s'
[PROOF STEP]
using step PID
[PROOF STATE]
proof (prove)
using this:
step s a = (ou, s')
PID \<notin> set (postIDs s)

goal (1 subgoal):
 1. PID \<in>\<in> postIDs s'
[PROOF STEP]
unfolding a ou
[PROOF STATE]
proof (prove)
using this:
step s (Cact (cPost uid p PID)) = (outOK, s')
PID \<notin> set (postIDs s)

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

goal (2 subgoals):
 1. \<exists>uid p. a = Cact (cPost uid p PID) \<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>uid p. a = Cact (cPost uid p PID) \<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> postIDs s \<and> (uid = admin s \<or> uid = owner s PID \<or> uid \<in>\<in> friendIDs s (owner s PID) \<or> vis s PID = PublicV))

goal (2 subgoals):
 1. \<exists>uid p. a = Cact (cPost uid p PID) \<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>uid p. a = Cact (cPost uid p PID) \<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 PID' c ch vlvl1 pPID' pPID
[PROOF STATE]
proof (prove)
using this:
map PValS_tgtAPI (filter isPValS vl) = map PValS_tgtAPI (filter isPValS vl1)
PID \<in>\<in> postIDs s'
consume (Trans s a ou s') vl vl'
corrFrom (post s1 PID) vl1
vl = [] \<Longrightarrow> vl1 = []
post s' PID = emptyPost
post s PID = emptyPost

goal (1 subgoal):
 1. \<Delta>1 s' vl' s' vl1
[PROOF STEP]
unfolding ss1 \<Delta>1_def vl'
[PROOF STATE]
proof (prove)
using this:
map PValS_tgtAPI (filter isPValS vl) = map PValS_tgtAPI (filter isPValS vl1)
PID \<in>\<in> postIDs s'
consume (Trans s a ou s') vl vl
corrFrom (post s PID) vl1
vl = [] \<Longrightarrow> vl1 = []
post s' PID = emptyPost
post s PID = emptyPost

goal (1 subgoal):
 1. PID \<in>\<in> postIDs s' \<and> eqButPID s' s' \<and> corrFrom (post s' PID) vl1 \<and> (vl = [] \<longrightarrow> vl1 = []) \<and> map PValS_tgtAPI (filter isPValS vl) = map PValS_tgtAPI (filter isPValS 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>uid p. a = Cact (cPost uid p PID) \<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>uid p. a = Cact (cPost uid p PID) \<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>uid p. a = Cact (cPost uid p PID) \<and> ou = outOK

goal (1 subgoal):
 1. \<nexists>uid p. a = Cact (cPost uid p PID) \<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>uid p. a = Cact (cPost uid p PID) \<and> ou = outOK

goal (1 subgoal):
 1. \<nexists>uid p. a = Cact (cPost uid p PID) \<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 PID': "\<not> PID \<in>\<in> postIDs s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. PID \<notin> set (postIDs s')
[PROOF STEP]
using step PID a
[PROOF STATE]
proof (prove)
using this:
step s a = (ou, s')
PID \<notin> set (postIDs s)
\<nexists>uid p. a = Cact (cPost uid p PID) \<and> ou = outOK

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

goal (1 subgoal):
 1. \<nexists>uid p. a = Cact (cPost uid p PID) \<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 PID' pPID pPID' ch vlvl1 l
[PROOF STATE]
proof (prove)
using this:
\<nexists>uid p. a = Cact (cPost uid p PID) \<and> ou = outOK
PID \<notin> set (postIDs s')
post s PID = emptyPost
post s' PID = emptyPost
corrFrom (post s1 PID) vl1
vl = [] \<Longrightarrow> vl1 = []
map PValS_tgtAPI (filter isPValS vl) = map PValS_tgtAPI (filter isPValS 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>uid p. a = Cact (cPost uid p PID) \<and> ou = outOK
PID \<notin> set (postIDs s')
post s PID = emptyPost
post s' PID = emptyPost
corrFrom (post s PID) vl1
vl = [] \<Longrightarrow> vl1 = []
map PValS_tgtAPI (filter isPValS vl) = map PValS_tgtAPI (filter isPValS vl1)

goal (1 subgoal):
 1. PID \<notin> set (postIDs s') \<and> post s' PID = emptyPost \<and> s' = s' \<and> corrFrom (post s' PID) vl1 \<and> (vl = [] \<longrightarrow> vl1 = []) \<and> map PValS_tgtAPI (filter isPValS vl) = map PValS_tgtAPI (filter isPValS 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 vlvl1
[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
vl = [] \<Longrightarrow> 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 simp
[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