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

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

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

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

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

goal (1 subgoal):
 1. \<And>s vl s1 vl1. \<lbrakk>reachNT s; reach s1; \<Delta>2 s vl s1 vl1\<rbrakk> \<Longrightarrow> iaction \<Delta>2 s vl s1 vl1 \<or> (vl = [] \<longrightarrow> vl1 = []) \<and> reaction \<Delta>2 s vl s1 vl1
[PROOF STEP]
have PID1: "PID \<in>\<in> postIDs s1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. PID \<in>\<in> postIDs s1
[PROOF STEP]
using eqButPID_stateSelectors[OF ss1] PID
[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> 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
PID \<in>\<in> postIDs s

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

goal (1 subgoal):
 1. \<And>s vl s1 vl1. \<lbrakk>reachNT s; reach s1; \<Delta>2 s vl s1 vl1\<rbrakk> \<Longrightarrow> iaction \<Delta>2 s vl s1 vl1 \<or> (vl = [] \<longrightarrow> vl1 = []) \<and> reaction \<Delta>2 s vl s1 vl1
[PROOF STEP]
have own: "owner s PID \<in> set (userIDs s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. owner s PID \<in>\<in> userIDs s
[PROOF STEP]
using reach_owner_userIDs[OF rs PID]
[PROOF STATE]
proof (prove)
using this:
owner s PID \<in>\<in> userIDs s

goal (1 subgoal):
 1. owner s PID \<in>\<in> userIDs s
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
owner s PID \<in>\<in> userIDs s

goal (1 subgoal):
 1. \<And>s vl s1 vl1. \<lbrakk>reachNT s; reach s1; \<Delta>2 s vl s1 vl1\<rbrakk> \<Longrightarrow> iaction \<Delta>2 s vl s1 vl1 \<or> (vl = [] \<longrightarrow> vl1 = []) \<and> reaction \<Delta>2 s vl s1 vl1
[PROOF STEP]
hence own1: "owner s1 PID \<in> set (userIDs s1)"
[PROOF STATE]
proof (prove)
using this:
owner s PID \<in>\<in> userIDs s

goal (1 subgoal):
 1. owner s1 PID \<in>\<in> userIDs s1
[PROOF STEP]
using eqButPID_stateSelectors[OF ss1]
[PROOF STATE]
proof (prove)
using this:
owner s PID \<in>\<in> userIDs s
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

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

goal (1 subgoal):
 1. \<And>s vl s1 vl1. \<lbrakk>reachNT s; reach s1; \<Delta>2 s vl s1 vl1\<rbrakk> \<Longrightarrow> iaction \<Delta>2 s vl s1 vl1 \<or> (vl = [] \<longrightarrow> vl1 = []) \<and> reaction \<Delta>2 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>2 s vl s1 vl1 \<or> (vl = [] \<longrightarrow> vl1 = []) \<and> reaction \<Delta>2 s vl s1 vl1
[PROOF STEP]
proof(cases vl1)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. vl1 = [] \<Longrightarrow> iaction \<Delta>2 s vl s1 vl1 \<or> (vl = [] \<longrightarrow> vl1 = []) \<and> reaction \<Delta>2 s vl s1 vl1
 2. \<And>a list. vl1 = a # list \<Longrightarrow> iaction \<Delta>2 s vl s1 vl1 \<or> (vl = [] \<longrightarrow> vl1 = []) \<and> reaction \<Delta>2 s vl s1 vl1
[PROOF STEP]
case (Cons v1 vll1)
[PROOF STATE]
proof (state)
this:
vl1 = v1 # vll1

goal (2 subgoals):
 1. vl1 = [] \<Longrightarrow> iaction \<Delta>2 s vl s1 vl1 \<or> (vl = [] \<longrightarrow> vl1 = []) \<and> reaction \<Delta>2 s vl s1 vl1
 2. \<And>a list. vl1 = a # list \<Longrightarrow> iaction \<Delta>2 s vl s1 vl1 \<or> (vl = [] \<longrightarrow> vl1 = []) \<and> reaction \<Delta>2 s vl s1 vl1
[PROOF STEP]
note vl1 = Cons
[PROOF STATE]
proof (state)
this:
vl1 = v1 # vll1

goal (2 subgoals):
 1. vl1 = [] \<Longrightarrow> iaction \<Delta>2 s vl s1 vl1 \<or> (vl = [] \<longrightarrow> vl1 = []) \<and> reaction \<Delta>2 s vl s1 vl1
 2. \<And>a list. vl1 = a # list \<Longrightarrow> iaction \<Delta>2 s vl s1 vl1 \<or> (vl = [] \<longrightarrow> vl1 = []) \<and> reaction \<Delta>2 s vl s1 vl1
[PROOF STEP]
obtain pst1 where v1: "v1 = PVal pst1" and lvll1: "list_all isPVal vll1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>pst1. \<lbrakk>v1 = PVal pst1; list_all isPVal vll1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using lvl1
[PROOF STATE]
proof (prove)
using this:
list_all isPVal vl1

goal (1 subgoal):
 1. (\<And>pst1. \<lbrakk>v1 = PVal pst1; list_all isPVal vll1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding vl1
[PROOF STATE]
proof (prove)
using this:
list_all isPVal (v1 # vll1)

goal (1 subgoal):
 1. (\<And>pst1. \<lbrakk>v1 = PVal pst1; list_all isPVal vll1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases v1) auto
[PROOF STATE]
proof (state)
this:
v1 = PVal pst1
list_all isPVal vll1

goal (2 subgoals):
 1. vl1 = [] \<Longrightarrow> iaction \<Delta>2 s vl s1 vl1 \<or> (vl = [] \<longrightarrow> vl1 = []) \<and> reaction \<Delta>2 s vl s1 vl1
 2. \<And>a list. vl1 = a # list \<Longrightarrow> iaction \<Delta>2 s vl s1 vl1 \<or> (vl = [] \<longrightarrow> vl1 = []) \<and> reaction \<Delta>2 s vl s1 vl1
[PROOF STEP]
define uid where "uid \<equiv> owner s PID"
[PROOF STATE]
proof (state)
this:
uid \<equiv> owner s PID

goal (2 subgoals):
 1. vl1 = [] \<Longrightarrow> iaction \<Delta>2 s vl s1 vl1 \<or> (vl = [] \<longrightarrow> vl1 = []) \<and> reaction \<Delta>2 s vl s1 vl1
 2. \<And>a list. vl1 = a # list \<Longrightarrow> iaction \<Delta>2 s vl s1 vl1 \<or> (vl = [] \<longrightarrow> vl1 = []) \<and> reaction \<Delta>2 s vl s1 vl1
[PROOF STEP]
define p where "p \<equiv> pass s uid"
[PROOF STATE]
proof (state)
this:
p \<equiv> pass s uid

goal (2 subgoals):
 1. vl1 = [] \<Longrightarrow> iaction \<Delta>2 s vl s1 vl1 \<or> (vl = [] \<longrightarrow> vl1 = []) \<and> reaction \<Delta>2 s vl s1 vl1
 2. \<And>a list. vl1 = a # list \<Longrightarrow> iaction \<Delta>2 s vl s1 vl1 \<or> (vl = [] \<longrightarrow> vl1 = []) \<and> reaction \<Delta>2 s vl s1 vl1
[PROOF STEP]
define a1 where "a1 \<equiv> Uact (uPost uid p PID pst1)"
[PROOF STATE]
proof (state)
this:
a1 \<equiv> Uact (uPost uid p PID pst1)

goal (2 subgoals):
 1. vl1 = [] \<Longrightarrow> iaction \<Delta>2 s vl s1 vl1 \<or> (vl = [] \<longrightarrow> vl1 = []) \<and> reaction \<Delta>2 s vl s1 vl1
 2. \<And>a list. vl1 = a # list \<Longrightarrow> iaction \<Delta>2 s vl s1 vl1 \<or> (vl = [] \<longrightarrow> vl1 = []) \<and> reaction \<Delta>2 s vl s1 vl1
[PROOF STEP]
have uid1: "uid = owner s1 PID" and p1: "p = pass s1 uid"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. uid = owner s1 PID &&& p = pass s1 uid
[PROOF STEP]
unfolding uid_def p_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. owner s PID = owner s1 PID &&& pass s (owner s PID) = pass s1 (owner s PID)
[PROOF STEP]
using eqButPID_stateSelectors[OF ss1]
[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> 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

goal (1 subgoal):
 1. owner s PID = owner s1 PID &&& pass s (owner s PID) = pass s1 (owner s PID)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
uid = owner s1 PID
p = pass s1 uid

goal (2 subgoals):
 1. vl1 = [] \<Longrightarrow> iaction \<Delta>2 s vl s1 vl1 \<or> (vl = [] \<longrightarrow> vl1 = []) \<and> reaction \<Delta>2 s vl s1 vl1
 2. \<And>a list. vl1 = a # list \<Longrightarrow> iaction \<Delta>2 s vl s1 vl1 \<or> (vl = [] \<longrightarrow> vl1 = []) \<and> reaction \<Delta>2 s vl s1 vl1
[PROOF STEP]
obtain ou1 s1' where step1: "step s1 a1 = (ou1, s1')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ou1 s1'. step s1 a1 = (ou1, s1') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases "step s1 a1") auto
[PROOF STATE]
proof (state)
this:
step s1 a1 = (ou1, s1')

goal (2 subgoals):
 1. vl1 = [] \<Longrightarrow> iaction \<Delta>2 s vl s1 vl1 \<or> (vl = [] \<longrightarrow> vl1 = []) \<and> reaction \<Delta>2 s vl s1 vl1
 2. \<And>a list. vl1 = a # list \<Longrightarrow> iaction \<Delta>2 s vl s1 vl1 \<or> (vl = [] \<longrightarrow> vl1 = []) \<and> reaction \<Delta>2 s vl s1 vl1
[PROOF STEP]
have ou1: "ou1 = outOK"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ou1 = outOK
[PROOF STEP]
using step1 PID1 own1
[PROOF STATE]
proof (prove)
using this:
step s1 a1 = (ou1, s1')
PID \<in>\<in> postIDs s1
owner s1 PID \<in>\<in> userIDs s1

goal (1 subgoal):
 1. ou1 = outOK
[PROOF STEP]
unfolding a1_def uid1 p1
[PROOF STATE]
proof (prove)
using this:
step s1 (Uact (uPost (owner s1 PID) (pass s1 (owner s1 PID)) PID pst1)) = (ou1, s1')
PID \<in>\<in> postIDs s1
owner s1 PID \<in>\<in> userIDs s1

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

goal (2 subgoals):
 1. vl1 = [] \<Longrightarrow> iaction \<Delta>2 s vl s1 vl1 \<or> (vl = [] \<longrightarrow> vl1 = []) \<and> reaction \<Delta>2 s vl s1 vl1
 2. \<And>a list. vl1 = a # list \<Longrightarrow> iaction \<Delta>2 s vl s1 vl1 \<or> (vl = [] \<longrightarrow> vl1 = []) \<and> reaction \<Delta>2 s vl s1 vl1
[PROOF STEP]
have uid: "uid \<notin> UIDs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. uid \<notin> UIDs
[PROOF STEP]
unfolding uid_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. owner s PID \<notin> UIDs
[PROOF STEP]
using rsT reachNT_state own PID
[PROOF STATE]
proof (prove)
using this:
reachNT s
reachNT ?s \<Longrightarrow> \<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))
owner s PID \<in>\<in> userIDs s
PID \<in>\<in> postIDs s

goal (1 subgoal):
 1. owner s PID \<notin> UIDs
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
uid \<notin> UIDs

goal (2 subgoals):
 1. vl1 = [] \<Longrightarrow> iaction \<Delta>2 s vl s1 vl1 \<or> (vl = [] \<longrightarrow> vl1 = []) \<and> reaction \<Delta>2 s vl s1 vl1
 2. \<And>a list. vl1 = a # list \<Longrightarrow> iaction \<Delta>2 s vl s1 vl1 \<or> (vl = [] \<longrightarrow> vl1 = []) \<and> reaction \<Delta>2 s vl s1 vl1
[PROOF STEP]
let ?trn1 = "Trans s1 a1 ou1 s1'"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. vl1 = [] \<Longrightarrow> iaction \<Delta>2 s vl s1 vl1 \<or> (vl = [] \<longrightarrow> vl1 = []) \<and> reaction \<Delta>2 s vl s1 vl1
 2. \<And>a list. vl1 = a # list \<Longrightarrow> iaction \<Delta>2 s vl s1 vl1 \<or> (vl = [] \<longrightarrow> vl1 = []) \<and> reaction \<Delta>2 s vl s1 vl1
[PROOF STEP]
have ?iact
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iaction \<Delta>2 s vl s1 vl1
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. step s1 ?a1.0 = (?ou1.0, ?s1')
 2. \<phi> (Trans s1 ?a1.0 ?ou1.0 ?s1')
 3. consume (Trans s1 ?a1.0 ?ou1.0 ?s1') vl1 ?vl1'
 4. \<not> \<gamma> (Trans s1 ?a1.0 ?ou1.0 ?s1')
 5. \<Delta>2 s vl ?s1' ?vl1'
[PROOF STEP]
show "step s1 a1 = (ou1, s1')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. step s1 a1 = (ou1, s1')
[PROOF STEP]
using step1
[PROOF STATE]
proof (prove)
using this:
step s1 a1 = (ou1, s1')

goal (1 subgoal):
 1. step s1 a1 = (ou1, s1')
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
step s1 a1 = (ou1, s1')

goal (4 subgoals):
 1. \<phi> (Trans s1 a1 ou1 s1')
 2. consume (Trans s1 a1 ou1 s1') vl1 ?vl1'
 3. \<not> \<gamma> (Trans s1 a1 ou1 s1')
 4. \<Delta>2 s vl s1' ?vl1'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<phi> (Trans s1 a1 ou1 s1')
 2. consume (Trans s1 a1 ou1 s1') vl1 ?vl1'
 3. \<not> \<gamma> (Trans s1 a1 ou1 s1')
 4. \<Delta>2 s vl s1' ?vl1'
[PROOF STEP]
show \<phi>1: "\<phi> ?trn1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> (Trans s1 a1 ou1 s1')
[PROOF STEP]
unfolding \<phi>_def2(* [OF step1] *) a1_def ou1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>uida pa pst. Uact (uPost uid p PID pst1) = Uact (uPost uida pa PID pst) \<and> outOK = outOK) \<or> (\<exists>uida pa aid. Uact (uPost uid p PID pst1) = COMact (comSendPost uida pa aid PID) \<and> outOK \<noteq> outErr)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<phi> (Trans s1 a1 ou1 s1')

goal (3 subgoals):
 1. consume (Trans s1 a1 ou1 s1') vl1 ?vl1'
 2. \<not> \<gamma> (Trans s1 a1 ou1 s1')
 3. \<Delta>2 s vl s1' ?vl1'
[PROOF STEP]
show "consume ?trn1 vl1 vll1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. consume (Trans s1 a1 ou1 s1') vl1 vll1
[PROOF STEP]
using \<phi>1
[PROOF STATE]
proof (prove)
using this:
\<phi> (Trans s1 a1 ou1 s1')

goal (1 subgoal):
 1. consume (Trans s1 a1 ou1 s1') vl1 vll1
[PROOF STEP]
unfolding vl1 consume_def a1_def v1
[PROOF STATE]
proof (prove)
using this:
\<phi> (Trans s1 (Uact (uPost uid p PID pst1)) ou1 s1')

goal (1 subgoal):
 1. if \<phi> (Trans s1 (Uact (uPost uid p PID pst1)) ou1 s1') then PVal pst1 # vll1 \<noteq> [] \<and> f (Trans s1 (Uact (uPost uid p PID pst1)) ou1 s1') = hd (PVal pst1 # vll1) \<and> vll1 = tl (PVal pst1 # vll1) else vll1 = PVal pst1 # vll1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
consume (Trans s1 a1 ou1 s1') vl1 vll1

goal (2 subgoals):
 1. \<not> \<gamma> (Trans s1 a1 ou1 s1')
 2. \<Delta>2 s vl s1' vll1
[PROOF STEP]
show "\<not> \<gamma> ?trn1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> \<gamma> (Trans s1 a1 ou1 s1')
[PROOF STEP]
using uid
[PROOF STATE]
proof (prove)
using this:
uid \<notin> UIDs

goal (1 subgoal):
 1. \<not> \<gamma> (Trans s1 a1 ou1 s1')
[PROOF STEP]
unfolding a1_def
[PROOF STATE]
proof (prove)
using this:
uid \<notin> UIDs

goal (1 subgoal):
 1. \<not> \<gamma> (Trans s1 (Uact (uPost uid p PID pst1)) ou1 s1')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> \<gamma> (Trans s1 a1 ou1 s1')

goal (1 subgoal):
 1. \<Delta>2 s vl s1' vll1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Delta>2 s vl s1' vll1
[PROOF STEP]
have "eqButPID s1 s1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqButPID s1 s1'
[PROOF STEP]
using Uact_uPaperC_step_eqButPID[OF _ step1] a1_def
[PROOF STATE]
proof (prove)
using this:
a1 = Uact (uPost ?uid ?p PID ?pst) \<Longrightarrow> eqButPID s1 s1'
a1 \<equiv> Uact (uPost uid p PID pst1)

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

goal (1 subgoal):
 1. \<Delta>2 s vl s1' vll1
[PROOF STEP]
hence ss1': "eqButPID s s1'"
[PROOF STATE]
proof (prove)
using this:
eqButPID s1 s1'

goal (1 subgoal):
 1. eqButPID s s1'
[PROOF STEP]
using eqButPID_trans ss1
[PROOF STATE]
proof (prove)
using this:
eqButPID s1 s1'
\<lbrakk>eqButPID ?s ?s1.0; eqButPID ?s1.0 ?s2.0\<rbrakk> \<Longrightarrow> eqButPID ?s ?s2.0
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. \<Delta>2 s vl s1' vll1
[PROOF STEP]
show "\<Delta>2 s vl s1' vll1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Delta>2 s vl s1' vll1
[PROOF STEP]
using PID ss1' lvll1
[PROOF STATE]
proof (prove)
using this:
PID \<in>\<in> postIDs s
eqButPID s s1'
list_all isPVal vll1

goal (1 subgoal):
 1. \<Delta>2 s vl s1' vll1
[PROOF STEP]
unfolding \<Delta>2_def vl
[PROOF STATE]
proof (prove)
using this:
PID \<in>\<in> postIDs s
eqButPID s s1'
list_all isPVal vll1

goal (1 subgoal):
 1. PID \<in>\<in> postIDs s \<and> eqButPID s s1' \<and> [] = [] \<and> list_all isPVal vll1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Delta>2 s vl s1' vll1

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

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

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

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

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

goal (1 subgoal):
 1. vl1 = [] \<Longrightarrow> iaction \<Delta>2 s vl s1 vl1 \<or> (vl = [] \<longrightarrow> vl1 = []) \<and> reaction \<Delta>2 s vl s1 vl1
[PROOF STEP]
have ?react
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reaction \<Delta>2 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>2 s s1 vl1 a ou s' vl' \<or> ignore \<Delta>2 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>2 s s1 vl1 a ou s' vl' \<or> ignore \<Delta>2 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>2 s s1 vl1 a ou s' vl' \<or> ignore \<Delta>2 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>2 s s1 vl1 a ou s' vl' \<or> ignore \<Delta>2 s s1 vl1 a ou s' vl'
[PROOF STEP]
obtain ou1 s1' 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. \<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>2 s s1 vl1 a ou s' vl' \<or> ignore \<Delta>2 s s1 vl1 a ou s' vl'
[PROOF STEP]
let ?trn1 = "Trans s1 a ou1 s1'"
[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>2 s s1 vl1 a ou s' vl' \<or> ignore \<Delta>2 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 eqButPID_step ss1 step step1
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>eqButPID ?s ?s1.0; step ?s ?a = (?ou, ?s'); step ?s1.0 ?a = (?ou1.0, ?s1')\<rbrakk> \<Longrightarrow> eqButPID ?s' ?s1'
eqButPID s s1
step s a = (ou, s')
step s1 a = (ou1, s1')

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

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>2 s s1 vl1 a ou s' vl' \<or> ignore \<Delta>2 s s1 vl1 a ou s' vl'
[PROOF STEP]
have \<gamma>\<gamma>1: "\<gamma> ?trn \<longleftrightarrow> \<gamma> ?trn1"
[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 (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>2 s s1 vl1 a ou s' vl' \<or> ignore \<Delta>2 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 rs PID
[PROOF STATE]
proof (prove)
using this:
step s a = (ou, s')
reach s
PID \<in>\<in> postIDs s

goal (1 subgoal):
 1. PID \<in>\<in> postIDs s'
[PROOF STEP]
using reach_postIDs_persist
[PROOF STATE]
proof (prove)
using this:
step s a = (ou, s')
reach s
PID \<in>\<in> postIDs s
\<lbrakk>?pID \<in>\<in> postIDs ?s; step ?s ?a = (?ou, ?s')\<rbrakk> \<Longrightarrow> ?pID \<in>\<in> postIDs ?s'

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

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>2 s s1 vl1 a ou s' vl' \<or> ignore \<Delta>2 s s1 vl1 a ou s' vl'
[PROOF STEP]
have \<phi>: "\<not> \<phi> ?trn" and vl': "vl' = vl"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> \<phi> (Trans s a ou s') &&& vl' = vl
[PROOF STEP]
using c
[PROOF STATE]
proof (prove)
using this:
consume (Trans s a ou s') vl vl'

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

goal (1 subgoal):
 1. \<not> \<phi> (Trans s a ou s') &&& vl' = []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> \<phi> (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>2 s s1 vl1 a ou s' vl' \<or> ignore \<Delta>2 s s1 vl1 a ou s' vl'
[PROOF STEP]
hence \<phi>1: "\<not> \<phi> ?trn1"
[PROOF STATE]
proof (prove)
using this:
\<not> \<phi> (Trans s a ou s')
vl' = vl

goal (1 subgoal):
 1. \<not> \<phi> (Trans s1 a ou1 s1')
[PROOF STEP]
using eqButPID_step_\<phi> step ss1 step1
[PROOF STATE]
proof (prove)
using this:
\<not> \<phi> (Trans s a ou s')
vl' = vl
\<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')
step s a = (ou, s')
eqButPID s s1
step s1 a = (ou1, s1')

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

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>2 s s1 vl1 a ou s' vl' \<or> ignore \<Delta>2 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>2 s s1 vl1 a ou s' vl' \<or> ignore \<Delta>2 s s1 vl1 a ou s' vl'
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. match \<Delta>2 s s1 vl1 a ou s' vl' \<or> ignore \<Delta>2 s s1 vl1 a ou s' vl'
[PROOF STEP]
have ?match
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. match \<Delta>2 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>2 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 auto
[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>2 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
[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 simp
[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>2 s' vl' s1' vl1
[PROOF STEP]
show "\<gamma> ?trn \<longleftrightarrow> \<gamma> ?trn1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<gamma> (Trans s a ou s') = \<gamma> (Trans s1 a ou1 s1')
[PROOF STEP]
by fact
[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>2 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>2 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>2 s' vl' s1' vl1
[PROOF STEP]
note \<gamma> = this
[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>2 s' vl' s1' vl1
[PROOF STEP]
have ou: "(\<exists> uid p aid pid. a = COMact (comSendPost uid p aid pid) \<and> outPurge ou = outPurge ou1) \<or>
                                        ou = ou1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>uid p aid pid. a = COMact (comSendPost uid p aid pid) \<and> outPurge ou = outPurge ou1) \<or> ou = ou1
[PROOF STEP]
using eqButPID_step_\<gamma>_out[OF ss1 step step1 rsT T rs1 \<gamma>]
[PROOF STATE]
proof (prove)
using this:
(\<exists>uid p aid pid. a = COMact (comSendPost uid p aid pid) \<and> outPurge ou = outPurge ou1) \<or> ou = ou1

goal (1 subgoal):
 1. (\<exists>uid p aid pid. a = COMact (comSendPost uid p aid pid) \<and> outPurge ou = outPurge ou1) \<or> ou = ou1
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<exists>uid p aid pid. a = COMact (comSendPost uid p aid pid) \<and> outPurge ou = outPurge ou1) \<or> 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>2 s' vl' s1' vl1
[PROOF STEP]
thus "g ?trn = g ?trn1"
[PROOF STATE]
proof (prove)
using this:
(\<exists>uid p aid pid. a = COMact (comSendPost uid p aid pid) \<and> outPurge ou = outPurge ou1) \<or> 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>2 s' vl' s1' vl1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Delta>2 s' vl' s1' vl1
[PROOF STEP]
have 2[simp]: "textPost (post s1' PID)  = textPost (post s1 PID)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. textPost (post s1' PID) = textPost (post s1 PID)
[PROOF STEP]
using step1 PID1 \<phi>1
[PROOF STATE]
proof (prove)
using this:
step s1 a = (ou1, s1')
PID \<in>\<in> postIDs s1
\<not> \<phi> (Trans s1 a ou1 s1')

goal (1 subgoal):
 1. textPost (post s1' PID) = textPost (post s1 PID)
[PROOF STEP]
unfolding \<phi>_def2
[PROOF STATE]
proof (prove)
using this:
step s1 a = (ou1, s1')
PID \<in>\<in> postIDs s1
\<not> ((\<exists>uid p pst. a = Uact (uPost uid p PID pst) \<and> ou1 = outOK) \<or> (\<exists>uid p aid. a = COMact (comSendPost uid p aid PID) \<and> ou1 \<noteq> outErr))

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

goal (1 subgoal):
 1. textPost (post s1' PID) = textPost (post s1 PID)
[PROOF STEP]
apply(cases a)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>x1. \<lbrakk>step s1 a = (ou1, s1'); PID \<in>\<in> postIDs s1; \<not> ((\<exists>uid p pst. a = Uact (uPost uid p PID pst) \<and> ou1 = outOK) \<or> (\<exists>uid p aid. a = COMact (comSendPost uid p aid PID) \<and> ou1 \<noteq> outErr)); a = Sact x1\<rbrakk> \<Longrightarrow> textPost (post s1' PID) = textPost (post s1 PID)
 2. \<And>x2. \<lbrakk>step s1 a = (ou1, s1'); PID \<in>\<in> postIDs s1; \<not> ((\<exists>uid p pst. a = Uact (uPost uid p PID pst) \<and> ou1 = outOK) \<or> (\<exists>uid p aid. a = COMact (comSendPost uid p aid PID) \<and> ou1 \<noteq> outErr)); a = Cact x2\<rbrakk> \<Longrightarrow> textPost (post s1' PID) = textPost (post s1 PID)
 3. \<And>x3. \<lbrakk>step s1 a = (ou1, s1'); PID \<in>\<in> postIDs s1; \<not> ((\<exists>uid p pst. a = Uact (uPost uid p PID pst) \<and> ou1 = outOK) \<or> (\<exists>uid p aid. a = COMact (comSendPost uid p aid PID) \<and> ou1 \<noteq> outErr)); a = Dact x3\<rbrakk> \<Longrightarrow> textPost (post s1' PID) = textPost (post s1 PID)
 4. \<And>x4. \<lbrakk>step s1 a = (ou1, s1'); PID \<in>\<in> postIDs s1; \<not> ((\<exists>uid p pst. a = Uact (uPost uid p PID pst) \<and> ou1 = outOK) \<or> (\<exists>uid p aid. a = COMact (comSendPost uid p aid PID) \<and> ou1 \<noteq> outErr)); a = Uact x4\<rbrakk> \<Longrightarrow> textPost (post s1' PID) = textPost (post s1 PID)
 5. \<And>x5. \<lbrakk>step s1 a = (ou1, s1'); PID \<in>\<in> postIDs s1; \<not> ((\<exists>uid p pst. a = Uact (uPost uid p PID pst) \<and> ou1 = outOK) \<or> (\<exists>uid p aid. a = COMact (comSendPost uid p aid PID) \<and> ou1 \<noteq> outErr)); a = Ract x5\<rbrakk> \<Longrightarrow> textPost (post s1' PID) = textPost (post s1 PID)
 6. \<And>x6. \<lbrakk>step s1 a = (ou1, s1'); PID \<in>\<in> postIDs s1; \<not> ((\<exists>uid p pst. a = Uact (uPost uid p PID pst) \<and> ou1 = outOK) \<or> (\<exists>uid p aid. a = COMact (comSendPost uid p aid PID) \<and> ou1 \<noteq> outErr)); a = Lact x6\<rbrakk> \<Longrightarrow> textPost (post s1' PID) = textPost (post s1 PID)
 7. \<And>x7. \<lbrakk>step s1 a = (ou1, s1'); PID \<in>\<in> postIDs s1; \<not> ((\<exists>uid p pst. a = Uact (uPost uid p PID pst) \<and> ou1 = outOK) \<or> (\<exists>uid p aid. a = COMact (comSendPost uid p aid PID) \<and> ou1 \<noteq> outErr)); a = COMact x7\<rbrakk> \<Longrightarrow> textPost (post s1' PID) = textPost (post s1 PID)
[PROOF STEP]
subgoal for x1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>step s1 a = (ou1, s1'); PID \<in>\<in> postIDs s1; \<not> ((\<exists>uid p pst. a = Uact (uPost uid p PID pst) \<and> ou1 = outOK) \<or> (\<exists>uid p aid. a = COMact (comSendPost uid p aid PID) \<and> ou1 \<noteq> outErr)); a = Sact x1\<rbrakk> \<Longrightarrow> textPost (post s1' PID) = textPost (post s1 PID)
[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>step s1 a = (ou1, s1'); PID \<in>\<in> postIDs s1; \<not> ((\<exists>uid p pst. a = Uact (uPost uid p PID pst) \<and> ou1 = outOK) \<or> (\<exists>uid p aid. a = COMact (comSendPost uid p aid PID) \<and> ou1 \<noteq> outErr)); a = Cact x2\<rbrakk> \<Longrightarrow> textPost (post s1' PID) = textPost (post s1 PID)
 2. \<And>x3. \<lbrakk>step s1 a = (ou1, s1'); PID \<in>\<in> postIDs s1; \<not> ((\<exists>uid p pst. a = Uact (uPost uid p PID pst) \<and> ou1 = outOK) \<or> (\<exists>uid p aid. a = COMact (comSendPost uid p aid PID) \<and> ou1 \<noteq> outErr)); a = Dact x3\<rbrakk> \<Longrightarrow> textPost (post s1' PID) = textPost (post s1 PID)
 3. \<And>x4. \<lbrakk>step s1 a = (ou1, s1'); PID \<in>\<in> postIDs s1; \<not> ((\<exists>uid p pst. a = Uact (uPost uid p PID pst) \<and> ou1 = outOK) \<or> (\<exists>uid p aid. a = COMact (comSendPost uid p aid PID) \<and> ou1 \<noteq> outErr)); a = Uact x4\<rbrakk> \<Longrightarrow> textPost (post s1' PID) = textPost (post s1 PID)
 4. \<And>x5. \<lbrakk>step s1 a = (ou1, s1'); PID \<in>\<in> postIDs s1; \<not> ((\<exists>uid p pst. a = Uact (uPost uid p PID pst) \<and> ou1 = outOK) \<or> (\<exists>uid p aid. a = COMact (comSendPost uid p aid PID) \<and> ou1 \<noteq> outErr)); a = Ract x5\<rbrakk> \<Longrightarrow> textPost (post s1' PID) = textPost (post s1 PID)
 5. \<And>x6. \<lbrakk>step s1 a = (ou1, s1'); PID \<in>\<in> postIDs s1; \<not> ((\<exists>uid p pst. a = Uact (uPost uid p PID pst) \<and> ou1 = outOK) \<or> (\<exists>uid p aid. a = COMact (comSendPost uid p aid PID) \<and> ou1 \<noteq> outErr)); a = Lact x6\<rbrakk> \<Longrightarrow> textPost (post s1' PID) = textPost (post s1 PID)
 6. \<And>x7. \<lbrakk>step s1 a = (ou1, s1'); PID \<in>\<in> postIDs s1; \<not> ((\<exists>uid p pst. a = Uact (uPost uid p PID pst) \<and> ou1 = outOK) \<or> (\<exists>uid p aid. a = COMact (comSendPost uid p aid PID) \<and> ou1 \<noteq> outErr)); a = COMact x7\<rbrakk> \<Longrightarrow> textPost (post s1' PID) = textPost (post s1 PID)
[PROOF STEP]
subgoal for x2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>step s1 a = (ou1, s1'); PID \<in>\<in> postIDs s1; \<not> ((\<exists>uid p pst. a = Uact (uPost uid p PID pst) \<and> ou1 = outOK) \<or> (\<exists>uid p aid. a = COMact (comSendPost uid p aid PID) \<and> ou1 \<noteq> outErr)); a = Cact x2\<rbrakk> \<Longrightarrow> textPost (post s1' PID) = textPost (post s1 PID)
[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>step s1 a = (ou1, s1'); PID \<in>\<in> postIDs s1; \<not> ((\<exists>uid p pst. a = Uact (uPost uid p PID pst) \<and> ou1 = outOK) \<or> (\<exists>uid p aid. a = COMact (comSendPost uid p aid PID) \<and> ou1 \<noteq> outErr)); a = Dact x3\<rbrakk> \<Longrightarrow> textPost (post s1' PID) = textPost (post s1 PID)
 2. \<And>x4. \<lbrakk>step s1 a = (ou1, s1'); PID \<in>\<in> postIDs s1; \<not> ((\<exists>uid p pst. a = Uact (uPost uid p PID pst) \<and> ou1 = outOK) \<or> (\<exists>uid p aid. a = COMact (comSendPost uid p aid PID) \<and> ou1 \<noteq> outErr)); a = Uact x4\<rbrakk> \<Longrightarrow> textPost (post s1' PID) = textPost (post s1 PID)
 3. \<And>x5. \<lbrakk>step s1 a = (ou1, s1'); PID \<in>\<in> postIDs s1; \<not> ((\<exists>uid p pst. a = Uact (uPost uid p PID pst) \<and> ou1 = outOK) \<or> (\<exists>uid p aid. a = COMact (comSendPost uid p aid PID) \<and> ou1 \<noteq> outErr)); a = Ract x5\<rbrakk> \<Longrightarrow> textPost (post s1' PID) = textPost (post s1 PID)
 4. \<And>x6. \<lbrakk>step s1 a = (ou1, s1'); PID \<in>\<in> postIDs s1; \<not> ((\<exists>uid p pst. a = Uact (uPost uid p PID pst) \<and> ou1 = outOK) \<or> (\<exists>uid p aid. a = COMact (comSendPost uid p aid PID) \<and> ou1 \<noteq> outErr)); a = Lact x6\<rbrakk> \<Longrightarrow> textPost (post s1' PID) = textPost (post s1 PID)
 5. \<And>x7. \<lbrakk>step s1 a = (ou1, s1'); PID \<in>\<in> postIDs s1; \<not> ((\<exists>uid p pst. a = Uact (uPost uid p PID pst) \<and> ou1 = outOK) \<or> (\<exists>uid p aid. a = COMact (comSendPost uid p aid PID) \<and> ou1 \<noteq> outErr)); a = COMact x7\<rbrakk> \<Longrightarrow> textPost (post s1' PID) = textPost (post s1 PID)
[PROOF STEP]
subgoal for x3
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>step s1 a = (ou1, s1'); PID \<in>\<in> postIDs s1; \<not> ((\<exists>uid p pst. a = Uact (uPost uid p PID pst) \<and> ou1 = outOK) \<or> (\<exists>uid p aid. a = COMact (comSendPost uid p aid PID) \<and> ou1 \<noteq> outErr)); a = Dact x3\<rbrakk> \<Longrightarrow> textPost (post s1' PID) = textPost (post s1 PID)
[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>step s1 a = (ou1, s1'); PID \<in>\<in> postIDs s1; \<not> ((\<exists>uid p pst. a = Uact (uPost uid p PID pst) \<and> ou1 = outOK) \<or> (\<exists>uid p aid. a = COMact (comSendPost uid p aid PID) \<and> ou1 \<noteq> outErr)); a = Uact x4\<rbrakk> \<Longrightarrow> textPost (post s1' PID) = textPost (post s1 PID)
 2. \<And>x5. \<lbrakk>step s1 a = (ou1, s1'); PID \<in>\<in> postIDs s1; \<not> ((\<exists>uid p pst. a = Uact (uPost uid p PID pst) \<and> ou1 = outOK) \<or> (\<exists>uid p aid. a = COMact (comSendPost uid p aid PID) \<and> ou1 \<noteq> outErr)); a = Ract x5\<rbrakk> \<Longrightarrow> textPost (post s1' PID) = textPost (post s1 PID)
 3. \<And>x6. \<lbrakk>step s1 a = (ou1, s1'); PID \<in>\<in> postIDs s1; \<not> ((\<exists>uid p pst. a = Uact (uPost uid p PID pst) \<and> ou1 = outOK) \<or> (\<exists>uid p aid. a = COMact (comSendPost uid p aid PID) \<and> ou1 \<noteq> outErr)); a = Lact x6\<rbrakk> \<Longrightarrow> textPost (post s1' PID) = textPost (post s1 PID)
 4. \<And>x7. \<lbrakk>step s1 a = (ou1, s1'); PID \<in>\<in> postIDs s1; \<not> ((\<exists>uid p pst. a = Uact (uPost uid p PID pst) \<and> ou1 = outOK) \<or> (\<exists>uid p aid. a = COMact (comSendPost uid p aid PID) \<and> ou1 \<noteq> outErr)); a = COMact x7\<rbrakk> \<Longrightarrow> textPost (post s1' PID) = textPost (post s1 PID)
[PROOF STEP]
subgoal for x4
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>step s1 a = (ou1, s1'); PID \<in>\<in> postIDs s1; \<not> ((\<exists>uid p pst. a = Uact (uPost uid p PID pst) \<and> ou1 = outOK) \<or> (\<exists>uid p aid. a = COMact (comSendPost uid p aid PID) \<and> ou1 \<noteq> outErr)); a = Uact x4\<rbrakk> \<Longrightarrow> textPost (post s1' PID) = textPost (post s1 PID)
[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>step s1 a = (ou1, s1'); PID \<in>\<in> postIDs s1; \<not> ((\<exists>uid p pst. a = Uact (uPost uid p PID pst) \<and> ou1 = outOK) \<or> (\<exists>uid p aid. a = COMact (comSendPost uid p aid PID) \<and> ou1 \<noteq> outErr)); a = Ract x5\<rbrakk> \<Longrightarrow> textPost (post s1' PID) = textPost (post s1 PID)
 2. \<And>x6. \<lbrakk>step s1 a = (ou1, s1'); PID \<in>\<in> postIDs s1; \<not> ((\<exists>uid p pst. a = Uact (uPost uid p PID pst) \<and> ou1 = outOK) \<or> (\<exists>uid p aid. a = COMact (comSendPost uid p aid PID) \<and> ou1 \<noteq> outErr)); a = Lact x6\<rbrakk> \<Longrightarrow> textPost (post s1' PID) = textPost (post s1 PID)
 3. \<And>x7. \<lbrakk>step s1 a = (ou1, s1'); PID \<in>\<in> postIDs s1; \<not> ((\<exists>uid p pst. a = Uact (uPost uid p PID pst) \<and> ou1 = outOK) \<or> (\<exists>uid p aid. a = COMact (comSendPost uid p aid PID) \<and> ou1 \<noteq> outErr)); a = COMact x7\<rbrakk> \<Longrightarrow> textPost (post s1' PID) = textPost (post s1 PID)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>step s1 a = (ou1, s1'); PID \<in>\<in> postIDs s1; \<not> ((\<exists>uid p pst. a = Uact (uPost uid p PID pst) \<and> ou1 = outOK) \<or> (\<exists>uid p aid. a = COMact (comSendPost uid p aid PID) \<and> ou1 \<noteq> outErr)); a = Ract x5_\<rbrakk> \<Longrightarrow> textPost (post s1' PID) = textPost (post s1 PID)
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x6. \<lbrakk>step s1 a = (ou1, s1'); PID \<in>\<in> postIDs s1; \<not> ((\<exists>uid p pst. a = Uact (uPost uid p PID pst) \<and> ou1 = outOK) \<or> (\<exists>uid p aid. a = COMact (comSendPost uid p aid PID) \<and> ou1 \<noteq> outErr)); a = Lact x6\<rbrakk> \<Longrightarrow> textPost (post s1' PID) = textPost (post s1 PID)
 2. \<And>x7. \<lbrakk>step s1 a = (ou1, s1'); PID \<in>\<in> postIDs s1; \<not> ((\<exists>uid p pst. a = Uact (uPost uid p PID pst) \<and> ou1 = outOK) \<or> (\<exists>uid p aid. a = COMact (comSendPost uid p aid PID) \<and> ou1 \<noteq> outErr)); a = COMact x7\<rbrakk> \<Longrightarrow> textPost (post s1' PID) = textPost (post s1 PID)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>step s1 a = (ou1, s1'); PID \<in>\<in> postIDs s1; \<not> ((\<exists>uid p pst. a = Uact (uPost uid p PID pst) \<and> ou1 = outOK) \<or> (\<exists>uid p aid. a = COMact (comSendPost uid p aid PID) \<and> ou1 \<noteq> outErr)); a = Lact x6_\<rbrakk> \<Longrightarrow> textPost (post s1' PID) = textPost (post s1 PID)
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x7. \<lbrakk>step s1 a = (ou1, s1'); PID \<in>\<in> postIDs s1; \<not> ((\<exists>uid p pst. a = Uact (uPost uid p PID pst) \<and> ou1 = outOK) \<or> (\<exists>uid p aid. a = COMact (comSendPost uid p aid PID) \<and> ou1 \<noteq> outErr)); a = COMact x7\<rbrakk> \<Longrightarrow> textPost (post s1' PID) = textPost (post s1 PID)
[PROOF STEP]
subgoal for x7
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>step s1 a = (ou1, s1'); PID \<in>\<in> postIDs s1; \<not> ((\<exists>uid p pst. a = Uact (uPost uid p PID pst) \<and> ou1 = outOK) \<or> (\<exists>uid p aid. a = COMact (comSendPost uid p aid PID) \<and> ou1 \<noteq> outErr)); a = COMact x7\<rbrakk> \<Longrightarrow> textPost (post s1' PID) = textPost (post s1 PID)
[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:
textPost (post s1' PID) = textPost (post s1 PID)

goal (1 subgoal):
 1. \<Delta>2 s' vl' s1' vl1
[PROOF STEP]
show "\<Delta>2 s' vl' s1' vl1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Delta>2 s' vl' s1' vl1
[PROOF STEP]
using PID' s's1' vl
[PROOF STATE]
proof (prove)
using this:
PID \<in>\<in> postIDs s'
eqButPID s' s1'
vl = []

goal (1 subgoal):
 1. \<Delta>2 s' vl' s1' vl1
[PROOF STEP]
unfolding \<Delta>2_def vl1 vl'
[PROOF STATE]
proof (prove)
using this:
PID \<in>\<in> postIDs s'
eqButPID s' s1'
vl = []

goal (1 subgoal):
 1. PID \<in>\<in> postIDs s' \<and> eqButPID s' s1' \<and> vl = [] \<and> list_all isPVal []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Delta>2 s' vl' s1' vl1

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

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

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

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

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
iaction \<Delta>2 s vl s1 vl1 \<or> (vl = [] \<longrightarrow> vl1 = []) \<and> reaction \<Delta>2 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, \<Delta>2}), (\<Delta>2, {\<Delta>2})}. \<exists>\<Delta>s\<subseteq>Domain {(\<Delta>0, {\<Delta>0, \<Delta>1}), (\<Delta>1, {\<Delta>1, \<Delta>2}), (\<Delta>2, {\<Delta>2})}. (\<Delta>, \<Delta>s) \<in> {(\<Delta>0, {\<Delta>0, \<Delta>1}), (\<Delta>1, {\<Delta>1, \<Delta>2}), (\<Delta>2, {\<Delta>2})}
 2. \<Delta>0 \<in> Domain {(\<Delta>0, {\<Delta>0, \<Delta>1}), (\<Delta>1, {\<Delta>1, \<Delta>2}), (\<Delta>2, {\<Delta>2})}
 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, \<Delta>2}), (\<Delta>2, {\<Delta>2})} \<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, \<Delta>2}), (\<Delta>2, {\<Delta>2})}
 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, \<Delta>2}), (\<Delta>2, {\<Delta>2})} \<longrightarrow> unwind_cont \<Delta> \<Delta>s)
[PROOF STEP]
using istate_\<Delta>0 unwind_cont_\<Delta>0 unwind_cont_\<Delta>1 unwind_cont_\<Delta>2
[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, \<Delta>2}
unwind_cont \<Delta>2 {\<Delta>2}

goal (3 subgoals):
 1. \<Delta>0 \<in> Domain {(\<Delta>0, {\<Delta>0, \<Delta>1}), (\<Delta>1, {\<Delta>1, \<Delta>2}), (\<Delta>2, {\<Delta>2})}
 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, \<Delta>2}), (\<Delta>2, {\<Delta>2})} \<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, \<Delta>2}
unwind_cont \<Delta>2 {\<Delta>2}

goal (3 subgoals):
 1. \<Delta>0 \<in> Domain {(\<Delta>0, {\<Delta>0, \<Delta>1}), (\<Delta>1, {\<Delta>1, \<Delta>2}), (\<Delta>2, {\<Delta>2})}
 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, \<Delta>2}), (\<Delta>2, {\<Delta>2})} \<longrightarrow> unwind_cont \<Delta> \<Delta>s)
[PROOF STEP]
by auto


[STATEMENT]
lemma "fetch [(R, 3),(WB,2), (R,1),(R,1), (WO,0),(WB,2), (L,8)] 0 Bk = (Nop , 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fetch [(R, 3), (WB, 2), (R, 1), (R, 1), (WO, 0), (WB, 2), (L, 8)] 0 Bk = (Nop, 0)
[PROOF STEP]
by auto


[STATEMENT]
lemma "fetch [(R, 3),(WB,2), (R,1),(R,1), (WO,0),(WB,2), (L,8)] 0 Oc = (Nop , 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fetch [(R, 3), (WB, 2), (R, 1), (R, 1), (WO, 0), (WB, 2), (L, 8)] 0 Oc = (Nop, 0)
[PROOF STEP]
by auto


[STATEMENT]
lemma "fetch [(R, 3),(WB,2), (R,1),(R,1), (WO,0),(WB,2), (L,8)] 1 Bk = (R , 3)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fetch [(R, 3), (WB, 2), (R, 1), (R, 1), (WO, 0), (WB, 2), (L, 8)] 1 Bk = (R, 3)
[PROOF STEP]
by auto


[STATEMENT]
lemma "fetch [(R, 3),(WB,2), (R,1),(R,1), (WO,0),(WB,2), (L,8)] 1 Oc = (WB, 2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fetch [(R, 3), (WB, 2), (R, 1), (R, 1), (WO, 0), (WB, 2), (L, 8)] 1 Oc = (WB, 2)
[PROOF STEP]
by auto


[STATEMENT]
lemma "fetch [(R, 3),(WB,2), (R,1),(R,1), (WO,0),(WB,2), (L,8)] 3 Bk = (WO, 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fetch [(R, 3), (WB, 2), (R, 1), (R, 1), (WO, 0), (WB, 2), (L, 8)] 3 Bk = (WO, 0)
[PROOF STEP]
by (simp add: numeral_eqs_upto_12)


[STATEMENT]
lemma "fetch [(R, 3),(WB,2), (R,1),(R,1), (WO,0),(WB,2), (L,8)] 3 Oc = (WB, 2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fetch [(R, 3), (WB, 2), (R, 1), (R, 1), (WO, 0), (WB, 2), (L, 8)] 3 Oc = (WB, 2)
[PROOF STEP]
by (simp add: numeral_eqs_upto_12)


[STATEMENT]
lemma "fetch [(R, 3),(WB,2), (R,1),(R,1), (WO,0),(WB,2), (L,8)] 4 Bk = (L, 8)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fetch [(R, 3), (WB, 2), (R, 1), (R, 1), (WO, 0), (WB, 2), (L, 8)] 4 Bk = (L, 8)
[PROOF STEP]
by (simp add: numeral_eqs_upto_12)


[STATEMENT]
lemma "fetch [(R, 3),(WB,2), (R,1),(R,1), (WO,0),(WB,2), (L,8)] 4 Oc = (Nop, 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fetch [(R, 3), (WB, 2), (R, 1), (R, 1), (WO, 0), (WB, 2), (L, 8)] 4 Oc = (Nop, 0)
[PROOF STEP]
by (simp add: numeral_eqs_upto_12)


[STATEMENT]
lemma "fetch [(R, 3),(WB,2), (R,1),(R,1), (WO,0),(WB,2), (L,8)] 10 Bk = (Nop, 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fetch [(R, 3), (WB, 2), (R, 1), (R, 1), (WO, 0), (WB, 2), (L, 8)] 10 Bk = (Nop, 0)
[PROOF STEP]
by (simp add: numeral_eqs_upto_12)


[STATEMENT]
lemma "fetch [(R, 3),(WB,2), (R,1),(R,1), (WO,0),(WB,2), (L,8)] 10 Oc = (Nop, 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fetch [(R, 3), (WB, 2), (R, 1), (R, 1), (WO, 0), (WB, 2), (L, 8)] 10 Oc = (Nop, 0)
[PROOF STEP]
by (simp add: numeral_eqs_upto_12)


[STATEMENT]
lemma
  "\<lbrace>\<lambda>(l1, r1). (l1,r1) = ([], [Oc,Oc] )\<rbrace> tm_weak_copy \<lbrace>\<lambda>(l0,r0). \<exists>k l. (l0,r0) = (Bk \<up> k, [Oc,Oc,Bk,Oc,Oc] @ Bk \<up> l)\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>(l1, r1). (l1, r1) = ([], [Oc, Oc])\<rbrace> tm_weak_copy \<lbrace>\<lambda>(l0, r0). \<exists>k l. (l0, r0) = (Bk \<up> k, [Oc, Oc, Bk, Oc, Oc] @ Bk \<up> l)\<rbrace>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrace>\<lambda>(l1, r1). (l1, r1) = ([], [Oc, Oc])\<rbrace> tm_weak_copy \<lbrace>\<lambda>(l0, r0). \<exists>k l. (l0, r0) = (Bk \<up> k, [Oc, Oc, Bk, Oc, Oc] @ Bk \<up> l)\<rbrace>
[PROOF STEP]
have "\<lbrace>\<lambda>tap. tap = ([], <[1::nat]>) \<rbrace> tm_weak_copy \<lbrace> \<lambda>tap. \<exists>k l. tap = (Bk \<up> k, <[hd [1::nat], hd [1::nat]]> @ Bk \<up> l) \<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>tap. tap = ([], <[1]>)\<rbrace> tm_weak_copy \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, <[hd [1], hd [1]]> @ Bk \<up> l)\<rbrace>
[PROOF STEP]
by (simp add: tm_weak_copy_correct5)
[PROOF STATE]
proof (state)
this:
\<lbrace>\<lambda>tap. tap = ([], <[1]>)\<rbrace> tm_weak_copy \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, <[hd [1], hd [1]]> @ Bk \<up> l)\<rbrace>

goal (1 subgoal):
 1. \<lbrace>\<lambda>(l1, r1). (l1, r1) = ([], [Oc, Oc])\<rbrace> tm_weak_copy \<lbrace>\<lambda>(l0, r0). \<exists>k l. (l0, r0) = (Bk \<up> k, [Oc, Oc, Bk, Oc, Oc] @ Bk \<up> l)\<rbrace>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrace>\<lambda>tap. tap = ([], <[1]>)\<rbrace> tm_weak_copy \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, <[hd [1], hd [1]]> @ Bk \<up> l)\<rbrace>
[PROOF STEP]
have "\<lbrace>\<lambda>tap. tap = ([], <[1::nat]>) \<rbrace> tm_weak_copy \<lbrace> \<lambda>tap. \<exists>k l. tap = (Bk \<up> k, <[1::nat, 1::nat]> @ Bk \<up> l) \<rbrace>"
[PROOF STATE]
proof (prove)
using this:
\<lbrace>\<lambda>tap. tap = ([], <[1]>)\<rbrace> tm_weak_copy \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, <[hd [1], hd [1]]> @ Bk \<up> l)\<rbrace>

goal (1 subgoal):
 1. \<lbrace>\<lambda>tap. tap = ([], <[1]>)\<rbrace> tm_weak_copy \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, <[1, 1]> @ Bk \<up> l)\<rbrace>
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<lbrace>\<lambda>tap. tap = ([], <[1]>)\<rbrace> tm_weak_copy \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, <[1, 1]> @ Bk \<up> l)\<rbrace>

goal (1 subgoal):
 1. \<lbrace>\<lambda>(l1, r1). (l1, r1) = ([], [Oc, Oc])\<rbrace> tm_weak_copy \<lbrace>\<lambda>(l0, r0). \<exists>k l. (l0, r0) = (Bk \<up> k, [Oc, Oc, Bk, Oc, Oc] @ Bk \<up> l)\<rbrace>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrace>\<lambda>tap. tap = ([], <[1]>)\<rbrace> tm_weak_copy \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, <[1, 1]> @ Bk \<up> l)\<rbrace>

goal (1 subgoal):
 1. \<lbrace>\<lambda>(l1, r1). (l1, r1) = ([], [Oc, Oc])\<rbrace> tm_weak_copy \<lbrace>\<lambda>(l0, r0). \<exists>k l. (l0, r0) = (Bk \<up> k, [Oc, Oc, Bk, Oc, Oc] @ Bk \<up> l)\<rbrace>
[PROOF STEP]
have "<[1::nat]> = [Oc,Oc]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <[1]> = [Oc, Oc]
[PROOF STEP]
by (simp add: tape_of_list_def tape_of_nat_def)
[PROOF STATE]
proof (state)
this:
<[1]> = [Oc, Oc]

goal (1 subgoal):
 1. \<lbrace>\<lambda>(l1, r1). (l1, r1) = ([], [Oc, Oc])\<rbrace> tm_weak_copy \<lbrace>\<lambda>(l0, r0). \<exists>k l. (l0, r0) = (Bk \<up> k, [Oc, Oc, Bk, Oc, Oc] @ Bk \<up> l)\<rbrace>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
<[1]> = [Oc, Oc]

goal (1 subgoal):
 1. \<lbrace>\<lambda>(l1, r1). (l1, r1) = ([], [Oc, Oc])\<rbrace> tm_weak_copy \<lbrace>\<lambda>(l0, r0). \<exists>k l. (l0, r0) = (Bk \<up> k, [Oc, Oc, Bk, Oc, Oc] @ Bk \<up> l)\<rbrace>
[PROOF STEP]
have "<[1::nat, 1::nat]> = [Oc,Oc,Bk,Oc,Oc]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <[1, 1]> = [Oc, Oc, Bk, Oc, Oc]
[PROOF STEP]
by (simp add: tape_of_list_def tape_of_nat_def)
[PROOF STATE]
proof (state)
this:
<[1, 1]> = [Oc, Oc, Bk, Oc, Oc]

goal (1 subgoal):
 1. \<lbrace>\<lambda>(l1, r1). (l1, r1) = ([], [Oc, Oc])\<rbrace> tm_weak_copy \<lbrace>\<lambda>(l0, r0). \<exists>k l. (l0, r0) = (Bk \<up> k, [Oc, Oc, Bk, Oc, Oc] @ Bk \<up> l)\<rbrace>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<lbrace>\<lambda>tap. tap = ([], <[1]>)\<rbrace> tm_weak_copy \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, <[1, 1]> @ Bk \<up> l)\<rbrace>
<[1]> = [Oc, Oc]
<[1, 1]> = [Oc, Oc, Bk, Oc, Oc]
[PROOF STEP]
have "\<lbrace>\<lambda>tap. tap = ([], <[1::nat]>) \<rbrace> tm_weak_copy \<lbrace> \<lambda>tap. \<exists>k l. tap = (Bk \<up> k, <[hd [1::nat], hd [1::nat]]> @ Bk \<up> l) \<rbrace>"
[PROOF STATE]
proof (prove)
using this:
\<lbrace>\<lambda>tap. tap = ([], <[1]>)\<rbrace> tm_weak_copy \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, <[1, 1]> @ Bk \<up> l)\<rbrace>
<[1]> = [Oc, Oc]
<[1, 1]> = [Oc, Oc, Bk, Oc, Oc]

goal (1 subgoal):
 1. \<lbrace>\<lambda>tap. tap = ([], <[1]>)\<rbrace> tm_weak_copy \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, <[hd [1], hd [1]]> @ Bk \<up> l)\<rbrace>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<lbrace>\<lambda>tap. tap = ([], <[1]>)\<rbrace> tm_weak_copy \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, <[hd [1], hd [1]]> @ Bk \<up> l)\<rbrace>

goal (1 subgoal):
 1. \<lbrace>\<lambda>(l1, r1). (l1, r1) = ([], [Oc, Oc])\<rbrace> tm_weak_copy \<lbrace>\<lambda>(l0, r0). \<exists>k l. (l0, r0) = (Bk \<up> k, [Oc, Oc, Bk, Oc, Oc] @ Bk \<up> l)\<rbrace>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrace>\<lambda>tap. tap = ([], <[1]>)\<rbrace> tm_weak_copy \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, <[hd [1], hd [1]]> @ Bk \<up> l)\<rbrace>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrace>\<lambda>tap. tap = ([], <[1]>)\<rbrace> tm_weak_copy \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, <[hd [1], hd [1]]> @ Bk \<up> l)\<rbrace>

goal (1 subgoal):
 1. \<lbrace>\<lambda>(l1, r1). (l1, r1) = ([], [Oc, Oc])\<rbrace> tm_weak_copy \<lbrace>\<lambda>(l0, r0). \<exists>k l. (l0, r0) = (Bk \<up> k, [Oc, Oc, Bk, Oc, Oc] @ Bk \<up> l)\<rbrace>
[PROOF STEP]
by (smt Hoare_haltI Hoare_halt_E0 \<open><[1, 1]> = [Oc, Oc, Bk, Oc, Oc]\<close> \<open><[1]> = [Oc, Oc]\<close>
        case_prodD case_prodI holds_for.simps is_final_eq list.discI list.inject list.sel(1)
        not_Cons_self2 tape_of_list_def tape_of_nat_def tape_of_nat_list.elims tape_of_nat_list.simps(3))
[PROOF STATE]
proof (state)
this:
\<lbrace>\<lambda>(l1, r1). (l1, r1) = ([], [Oc, Oc])\<rbrace> tm_weak_copy \<lbrace>\<lambda>(l0, r0). \<exists>k l. (l0, r0) = (Bk \<up> k, [Oc, Oc, Bk, Oc, Oc] @ Bk \<up> l)\<rbrace>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma
  "\<forall>n. \<lbrace>\<lambda>tap. tap = ([], Oc\<up>(n+1))\<rbrace> tm_weak_copy \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k,  Oc\<up>(n+1) @ [Bk] @ Oc\<up>(n+1) @ Bk \<up> l) \<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n. \<lbrace>\<lambda>tap. tap = ([], Oc \<up> (n + 1))\<rbrace> tm_weak_copy \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, Oc \<up> (n + 1) @ [Bk] @ Oc \<up> (n + 1) @ Bk \<up> l)\<rbrace>
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. \<lbrace>\<lambda>tap. tap = ([], Oc \<up> (n + 1))\<rbrace> tm_weak_copy \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, Oc \<up> (n + 1) @ [Bk] @ Oc \<up> (n + 1) @ Bk \<up> l)\<rbrace>
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. \<lbrace>\<lambda>tap. tap = ([], Oc \<up> (n + 1))\<rbrace> tm_weak_copy \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, Oc \<up> (n + 1) @ [Bk] @ Oc \<up> (n + 1) @ Bk \<up> l)\<rbrace>
[PROOF STEP]
have "\<lbrace>\<lambda>tap. tap = ([], <[n::nat]>)\<rbrace> tm_weak_copy \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, <[n, n]> @ Bk \<up> l) \<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>tap. tap = ([], <[n]>)\<rbrace> tm_weak_copy \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, <[n, n]> @ Bk \<up> l)\<rbrace>
[PROOF STEP]
by (rule tm_weak_copy_correct5)
[PROOF STATE]
proof (state)
this:
\<lbrace>\<lambda>tap. tap = ([], <[n]>)\<rbrace> tm_weak_copy \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, <[n, n]> @ Bk \<up> l)\<rbrace>

goal (1 subgoal):
 1. \<And>n. \<lbrace>\<lambda>tap. tap = ([], Oc \<up> (n + 1))\<rbrace> tm_weak_copy \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, Oc \<up> (n + 1) @ [Bk] @ Oc \<up> (n + 1) @ Bk \<up> l)\<rbrace>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrace>\<lambda>tap. tap = ([], <[n]>)\<rbrace> tm_weak_copy \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, <[n, n]> @ Bk \<up> l)\<rbrace>

goal (1 subgoal):
 1. \<And>n. \<lbrace>\<lambda>tap. tap = ([], Oc \<up> (n + 1))\<rbrace> tm_weak_copy \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, Oc \<up> (n + 1) @ [Bk] @ Oc \<up> (n + 1) @ Bk \<up> l)\<rbrace>
[PROOF STEP]
have "<[n::nat]> =  Oc\<up>(Suc n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <[n]> = Oc \<up> Suc n
[PROOF STEP]
by (simp add: tape_of_list_def tape_of_nat_def)
[PROOF STATE]
proof (state)
this:
<[n]> = Oc \<up> Suc n

goal (1 subgoal):
 1. \<And>n. \<lbrace>\<lambda>tap. tap = ([], Oc \<up> (n + 1))\<rbrace> tm_weak_copy \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, Oc \<up> (n + 1) @ [Bk] @ Oc \<up> (n + 1) @ Bk \<up> l)\<rbrace>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
<[n]> = Oc \<up> Suc n

goal (1 subgoal):
 1. \<And>n. \<lbrace>\<lambda>tap. tap = ([], Oc \<up> (n + 1))\<rbrace> tm_weak_copy \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, Oc \<up> (n + 1) @ [Bk] @ Oc \<up> (n + 1) @ Bk \<up> l)\<rbrace>
[PROOF STEP]
have "<[n, n]> =  Oc\<up>(Suc n) @ [Bk] @ Oc\<up>(Suc n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <[n, n]> = Oc \<up> Suc n @ [Bk] @ Oc \<up> Suc n
[PROOF STEP]
by (simp add: tape_of_list_def tape_of_nat_def)
[PROOF STATE]
proof (state)
this:
<[n, n]> = Oc \<up> Suc n @ [Bk] @ Oc \<up> Suc n

goal (1 subgoal):
 1. \<And>n. \<lbrace>\<lambda>tap. tap = ([], Oc \<up> (n + 1))\<rbrace> tm_weak_copy \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, Oc \<up> (n + 1) @ [Bk] @ Oc \<up> (n + 1) @ Bk \<up> l)\<rbrace>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<lbrace>\<lambda>tap. tap = ([], <[n]>)\<rbrace> tm_weak_copy \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, <[n, n]> @ Bk \<up> l)\<rbrace>
<[n]> = Oc \<up> Suc n
<[n, n]> = Oc \<up> Suc n @ [Bk] @ Oc \<up> Suc n
[PROOF STEP]
have X: "\<lbrace>\<lambda>tap. tap = ([], Oc\<up>(Suc n))\<rbrace> tm_weak_copy \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k,  Oc\<up>(Suc n) @ [Bk] @ Oc\<up>(Suc n) @ Bk \<up> l) \<rbrace>"
[PROOF STATE]
proof (prove)
using this:
\<lbrace>\<lambda>tap. tap = ([], <[n]>)\<rbrace> tm_weak_copy \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, <[n, n]> @ Bk \<up> l)\<rbrace>
<[n]> = Oc \<up> Suc n
<[n, n]> = Oc \<up> Suc n @ [Bk] @ Oc \<up> Suc n

goal (1 subgoal):
 1. \<lbrace>\<lambda>tap. tap = ([], Oc \<up> Suc n)\<rbrace> tm_weak_copy \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, Oc \<up> Suc n @ [Bk] @ Oc \<up> Suc n @ Bk \<up> l)\<rbrace>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<lbrace>\<lambda>tap. tap = ([], Oc \<up> Suc n)\<rbrace> tm_weak_copy \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, Oc \<up> Suc n @ [Bk] @ Oc \<up> Suc n @ Bk \<up> l)\<rbrace>

goal (1 subgoal):
 1. \<And>n. \<lbrace>\<lambda>tap. tap = ([], Oc \<up> (n + 1))\<rbrace> tm_weak_copy \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, Oc \<up> (n + 1) @ [Bk] @ Oc \<up> (n + 1) @ Bk \<up> l)\<rbrace>
[PROOF STEP]
show "\<lbrace>\<lambda>tap. tap = ([], Oc\<up>(n+1))\<rbrace> tm_weak_copy \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k,  Oc\<up>(n+1) @ [Bk] @ Oc\<up>(n+1) @ Bk \<up> l) \<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>tap. tap = ([], Oc \<up> (n + 1))\<rbrace> tm_weak_copy \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, Oc \<up> (n + 1) @ [Bk] @ Oc \<up> (n + 1) @ Bk \<up> l)\<rbrace>
[PROOF STEP]
using X
[PROOF STATE]
proof (prove)
using this:
\<lbrace>\<lambda>tap. tap = ([], Oc \<up> Suc n)\<rbrace> tm_weak_copy \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, Oc \<up> Suc n @ [Bk] @ Oc \<up> Suc n @ Bk \<up> l)\<rbrace>

goal (1 subgoal):
 1. \<lbrace>\<lambda>tap. tap = ([], Oc \<up> (n + 1))\<rbrace> tm_weak_copy \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, Oc \<up> (n + 1) @ [Bk] @ Oc \<up> (n + 1) @ Bk \<up> l)\<rbrace>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrace>\<lambda>tap. tap = ([], Oc \<up> (n + 1))\<rbrace> tm_weak_copy \<lbrace>\<lambda>tap. \<exists>k l. tap = (Bk \<up> k, Oc \<up> (n + 1) @ [Bk] @ Oc \<up> (n + 1) @ Bk \<up> l)\<rbrace>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma leftmost_element_property:
  assumes "\<exists>x \<in> set xs. P x"
  obtains zs x' ys where "xs = zs@x'#ys" and "P x'" and "\<forall>z \<in> set zs. \<not> P z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>zs x' ys. \<lbrakk>xs = zs @ x' # ys; P x'; \<forall>z\<in>set zs. \<not> P z\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof(atomize_elim)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>zs x' ys. xs = zs @ x' # ys \<and> P x' \<and> (\<forall>z\<in>set zs. \<not> P z)
[PROOF STEP]
from \<open>\<exists>x \<in> set xs. P x\<close>
[PROOF STATE]
proof (chain)
picking this:
\<exists>x\<in>set xs. P x
[PROOF STEP]
show "\<exists>zs x' ys. xs = zs @ x' # ys \<and> P x' \<and> (\<forall>z\<in>set zs. \<not> P z)"
[PROOF STATE]
proof (prove)
using this:
\<exists>x\<in>set xs. P x

goal (1 subgoal):
 1. \<exists>zs x' ys. xs = zs @ x' # ys \<and> P x' \<and> (\<forall>z\<in>set zs. \<not> P z)
[PROOF STEP]
proof(induct xs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Bex (set []) P \<Longrightarrow> \<exists>zs x' ys. [] = zs @ x' # ys \<and> P x' \<and> (\<forall>z\<in>set zs. \<not> P z)
 2. \<And>a xs. \<lbrakk>Bex (set xs) P \<Longrightarrow> \<exists>zs x' ys. xs = zs @ x' # ys \<and> P x' \<and> (\<forall>z\<in>set zs. \<not> P z); Bex (set (a # xs)) P\<rbrakk> \<Longrightarrow> \<exists>zs x' ys. a # xs = zs @ x' # ys \<and> P x' \<and> (\<forall>z\<in>set zs. \<not> P z)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
\<exists>a\<in>set []. P a

goal (2 subgoals):
 1. Bex (set []) P \<Longrightarrow> \<exists>zs x' ys. [] = zs @ x' # ys \<and> P x' \<and> (\<forall>z\<in>set zs. \<not> P z)
 2. \<And>a xs. \<lbrakk>Bex (set xs) P \<Longrightarrow> \<exists>zs x' ys. xs = zs @ x' # ys \<and> P x' \<and> (\<forall>z\<in>set zs. \<not> P z); Bex (set (a # xs)) P\<rbrakk> \<Longrightarrow> \<exists>zs x' ys. a # xs = zs @ x' # ys \<and> P x' \<and> (\<forall>z\<in>set zs. \<not> P z)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<exists>a\<in>set []. P a

goal (1 subgoal):
 1. \<exists>zs x' ys. [] = zs @ x' # ys \<and> P x' \<and> (\<forall>z\<in>set zs. \<not> P z)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>zs x' ys. [] = zs @ x' # ys \<and> P x' \<and> (\<forall>z\<in>set zs. \<not> P z)

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>Bex (set xs) P \<Longrightarrow> \<exists>zs x' ys. xs = zs @ x' # ys \<and> P x' \<and> (\<forall>z\<in>set zs. \<not> P z); Bex (set (a # xs)) P\<rbrakk> \<Longrightarrow> \<exists>zs x' ys. a # xs = zs @ x' # ys \<and> P x' \<and> (\<forall>z\<in>set zs. \<not> P z)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>Bex (set xs) P \<Longrightarrow> \<exists>zs x' ys. xs = zs @ x' # ys \<and> P x' \<and> (\<forall>z\<in>set zs. \<not> P z); Bex (set (a # xs)) P\<rbrakk> \<Longrightarrow> \<exists>zs x' ys. a # xs = zs @ x' # ys \<and> P x' \<and> (\<forall>z\<in>set zs. \<not> P z)
[PROOF STEP]
case (Cons x' xs')
[PROOF STATE]
proof (state)
this:
\<exists>a\<in>set xs'. P a \<Longrightarrow> \<exists>zs x' ys. xs' = zs @ x' # ys \<and> P x' \<and> (\<forall>z\<in>set zs. \<not> P z)
\<exists>a\<in>set (x' # xs'). P a

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>Bex (set xs) P \<Longrightarrow> \<exists>zs x' ys. xs = zs @ x' # ys \<and> P x' \<and> (\<forall>z\<in>set zs. \<not> P z); Bex (set (a # xs)) P\<rbrakk> \<Longrightarrow> \<exists>zs x' ys. a # xs = zs @ x' # ys \<and> P x' \<and> (\<forall>z\<in>set zs. \<not> P z)
[PROOF STEP]
note IH = \<open>\<exists>a\<in>set xs'. P a
      \<Longrightarrow> \<exists>zs x' ys. xs' = zs@x'#ys \<and> P x' \<and> (\<forall>z\<in>set zs. \<not> P z)\<close>
[PROOF STATE]
proof (state)
this:
\<exists>a\<in>set xs'. P a \<Longrightarrow> \<exists>zs x' ys. xs' = zs @ x' # ys \<and> P x' \<and> (\<forall>z\<in>set zs. \<not> P z)

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>Bex (set xs) P \<Longrightarrow> \<exists>zs x' ys. xs = zs @ x' # ys \<and> P x' \<and> (\<forall>z\<in>set zs. \<not> P z); Bex (set (a # xs)) P\<rbrakk> \<Longrightarrow> \<exists>zs x' ys. a # xs = zs @ x' # ys \<and> P x' \<and> (\<forall>z\<in>set zs. \<not> P z)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>zs x'a ys. x' # xs' = zs @ x'a # ys \<and> P x'a \<and> (\<forall>z\<in>set zs. \<not> P z)
[PROOF STEP]
proof (cases "P x'")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. P x' \<Longrightarrow> \<exists>zs x'a ys. x' # xs' = zs @ x'a # ys \<and> P x'a \<and> (\<forall>z\<in>set zs. \<not> P z)
 2. \<not> P x' \<Longrightarrow> \<exists>zs x'a ys. x' # xs' = zs @ x'a # ys \<and> P x'a \<and> (\<forall>z\<in>set zs. \<not> P z)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
P x'

goal (2 subgoals):
 1. P x' \<Longrightarrow> \<exists>zs x'a ys. x' # xs' = zs @ x'a # ys \<and> P x'a \<and> (\<forall>z\<in>set zs. \<not> P z)
 2. \<not> P x' \<Longrightarrow> \<exists>zs x'a ys. x' # xs' = zs @ x'a # ys \<and> P x'a \<and> (\<forall>z\<in>set zs. \<not> P z)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
P x'
[PROOF STEP]
have "(\<exists>ys. x' # xs' = [] @ x' # ys) \<and> P x' \<and> (\<forall>x\<in>set []. \<not> P x)"
[PROOF STATE]
proof (prove)
using this:
P x'

goal (1 subgoal):
 1. (\<exists>ys. x' # xs' = [] @ x' # ys) \<and> P x' \<and> (\<forall>x\<in>set []. \<not> P x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<exists>ys. x' # xs' = [] @ x' # ys) \<and> P x' \<and> (\<forall>x\<in>set []. \<not> P x)

goal (2 subgoals):
 1. P x' \<Longrightarrow> \<exists>zs x'a ys. x' # xs' = zs @ x'a # ys \<and> P x'a \<and> (\<forall>z\<in>set zs. \<not> P z)
 2. \<not> P x' \<Longrightarrow> \<exists>zs x'a ys. x' # xs' = zs @ x'a # ys \<and> P x'a \<and> (\<forall>z\<in>set zs. \<not> P z)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<exists>ys. x' # xs' = [] @ x' # ys) \<and> P x' \<and> (\<forall>x\<in>set []. \<not> P x)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<exists>ys. x' # xs' = [] @ x' # ys) \<and> P x' \<and> (\<forall>x\<in>set []. \<not> P x)

goal (1 subgoal):
 1. \<exists>zs x'a ys. x' # xs' = zs @ x'a # ys \<and> P x'a \<and> (\<forall>z\<in>set zs. \<not> P z)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>zs x'a ys. x' # xs' = zs @ x'a # ys \<and> P x'a \<and> (\<forall>z\<in>set zs. \<not> P z)

goal (1 subgoal):
 1. \<not> P x' \<Longrightarrow> \<exists>zs x'a ys. x' # xs' = zs @ x'a # ys \<and> P x'a \<and> (\<forall>z\<in>set zs. \<not> P z)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> P x' \<Longrightarrow> \<exists>zs x'a ys. x' # xs' = zs @ x'a # ys \<and> P x'a \<and> (\<forall>z\<in>set zs. \<not> P z)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> P x'

goal (1 subgoal):
 1. \<not> P x' \<Longrightarrow> \<exists>zs x'a ys. x' # xs' = zs @ x'a # ys \<and> P x'a \<and> (\<forall>z\<in>set zs. \<not> P z)
[PROOF STEP]
with \<open>\<exists>y\<in>set (x'#xs'). P y\<close>
[PROOF STATE]
proof (chain)
picking this:
\<exists>y\<in>set (x' # xs'). P y
\<not> P x'
[PROOF STEP]
have "\<exists>y\<in>set xs'. P y"
[PROOF STATE]
proof (prove)
using this:
\<exists>y\<in>set (x' # xs'). P y
\<not> P x'

goal (1 subgoal):
 1. \<exists>y\<in>set xs'. P y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>y\<in>set xs'. P y

goal (1 subgoal):
 1. \<not> P x' \<Longrightarrow> \<exists>zs x'a ys. x' # xs' = zs @ x'a # ys \<and> P x'a \<and> (\<forall>z\<in>set zs. \<not> P z)
[PROOF STEP]
from IH[OF this]
[PROOF STATE]
proof (chain)
picking this:
\<exists>zs x' ys. xs' = zs @ x' # ys \<and> P x' \<and> (\<forall>z\<in>set zs. \<not> P z)
[PROOF STEP]
obtain y ys zs where "xs' = zs@y#ys"
        and "P y" and "\<forall>z\<in>set zs. \<not> P z"
[PROOF STATE]
proof (prove)
using this:
\<exists>zs x' ys. xs' = zs @ x' # ys \<and> P x' \<and> (\<forall>z\<in>set zs. \<not> P z)

goal (1 subgoal):
 1. (\<And>zs y ys. \<lbrakk>xs' = zs @ y # ys; P y; \<forall>z\<in>set zs. \<not> P z\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
xs' = zs @ y # ys
P y
\<forall>z\<in>set zs. \<not> P z

goal (1 subgoal):
 1. \<not> P x' \<Longrightarrow> \<exists>zs x'a ys. x' # xs' = zs @ x'a # ys \<and> P x'a \<and> (\<forall>z\<in>set zs. \<not> P z)
[PROOF STEP]
from \<open>\<forall>z\<in>set zs. \<not> P z\<close> False
[PROOF STATE]
proof (chain)
picking this:
\<forall>z\<in>set zs. \<not> P z
\<not> P x'
[PROOF STEP]
have "\<forall>z\<in>set (x'#zs). \<not> P z"
[PROOF STATE]
proof (prove)
using this:
\<forall>z\<in>set zs. \<not> P z
\<not> P x'

goal (1 subgoal):
 1. \<forall>z\<in>set (x' # zs). \<not> P z
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>z\<in>set (x' # zs). \<not> P z

goal (1 subgoal):
 1. \<not> P x' \<Longrightarrow> \<exists>zs x'a ys. x' # xs' = zs @ x'a # ys \<and> P x'a \<and> (\<forall>z\<in>set zs. \<not> P z)
[PROOF STEP]
with \<open>xs' = zs@y#ys\<close> \<open>P y\<close>
[PROOF STATE]
proof (chain)
picking this:
xs' = zs @ y # ys
P y
\<forall>z\<in>set (x' # zs). \<not> P z
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
xs' = zs @ y # ys
P y
\<forall>z\<in>set (x' # zs). \<not> P z

goal (1 subgoal):
 1. \<exists>zs x'a ys. x' # xs' = zs @ x'a # ys \<and> P x'a \<and> (\<forall>z\<in>set zs. \<not> P z)
[PROOF STEP]
by (metis Cons_eq_append_conv)
[PROOF STATE]
proof (state)
this:
\<exists>zs x'a ys. x' # xs' = zs @ x'a # ys \<and> P x'a \<and> (\<forall>z\<in>set zs. \<not> P z)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>zs x'a ys. x' # xs' = zs @ x'a # ys \<and> P x'a \<and> (\<forall>z\<in>set zs. \<not> P z)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>zs x' ys. xs = zs @ x' # ys \<and> P x' \<and> (\<forall>z\<in>set zs. \<not> P z)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rightmost_element_property:
  assumes "\<exists>x \<in> set xs. P x"
  obtains ys x' zs where "xs = ys@x'#zs" and "P x'" and "\<forall>z \<in> set zs. \<not> P z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ys x' zs. \<lbrakk>xs = ys @ x' # zs; P x'; \<forall>z\<in>set zs. \<not> P z\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof(atomize_elim)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>ys x' zs. xs = ys @ x' # zs \<and> P x' \<and> (\<forall>z\<in>set zs. \<not> P z)
[PROOF STEP]
from \<open>\<exists>x \<in> set xs. P x\<close>
[PROOF STATE]
proof (chain)
picking this:
\<exists>x\<in>set xs. P x
[PROOF STEP]
show "\<exists>ys x' zs. xs = ys @ x' # zs \<and> P x' \<and> (\<forall>z\<in>set zs. \<not> P z)"
[PROOF STATE]
proof (prove)
using this:
\<exists>x\<in>set xs. P x

goal (1 subgoal):
 1. \<exists>ys x' zs. xs = ys @ x' # zs \<and> P x' \<and> (\<forall>z\<in>set zs. \<not> P z)
[PROOF STEP]
proof(induct xs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Bex (set []) P \<Longrightarrow> \<exists>ys x' zs. [] = ys @ x' # zs \<and> P x' \<and> (\<forall>z\<in>set zs. \<not> P z)
 2. \<And>a xs. \<lbrakk>Bex (set xs) P \<Longrightarrow> \<exists>ys x' zs. xs = ys @ x' # zs \<and> P x' \<and> (\<forall>z\<in>set zs. \<not> P z); Bex (set (a # xs)) P\<rbrakk> \<Longrightarrow> \<exists>ys x' zs. a # xs = ys @ x' # zs \<and> P x' \<and> (\<forall>z\<in>set zs. \<not> P z)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
\<exists>a\<in>set []. P a

goal (2 subgoals):
 1. Bex (set []) P \<Longrightarrow> \<exists>ys x' zs. [] = ys @ x' # zs \<and> P x' \<and> (\<forall>z\<in>set zs. \<not> P z)
 2. \<And>a xs. \<lbrakk>Bex (set xs) P \<Longrightarrow> \<exists>ys x' zs. xs = ys @ x' # zs \<and> P x' \<and> (\<forall>z\<in>set zs. \<not> P z); Bex (set (a # xs)) P\<rbrakk> \<Longrightarrow> \<exists>ys x' zs. a # xs = ys @ x' # zs \<and> P x' \<and> (\<forall>z\<in>set zs. \<not> P z)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<exists>a\<in>set []. P a

goal (1 subgoal):
 1. \<exists>ys x' zs. [] = ys @ x' # zs \<and> P x' \<and> (\<forall>z\<in>set zs. \<not> P z)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>ys x' zs. [] = ys @ x' # zs \<and> P x' \<and> (\<forall>z\<in>set zs. \<not> P z)

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>Bex (set xs) P \<Longrightarrow> \<exists>ys x' zs. xs = ys @ x' # zs \<and> P x' \<and> (\<forall>z\<in>set zs. \<not> P z); Bex (set (a # xs)) P\<rbrakk> \<Longrightarrow> \<exists>ys x' zs. a # xs = ys @ x' # zs \<and> P x' \<and> (\<forall>z\<in>set zs. \<not> P z)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>Bex (set xs) P \<Longrightarrow> \<exists>ys x' zs. xs = ys @ x' # zs \<and> P x' \<and> (\<forall>z\<in>set zs. \<not> P z); Bex (set (a # xs)) P\<rbrakk> \<Longrightarrow> \<exists>ys x' zs. a # xs = ys @ x' # zs \<and> P x' \<and> (\<forall>z\<in>set zs. \<not> P z)
[PROOF STEP]
case (Cons x' xs')
[PROOF STATE]
proof (state)
this:
\<exists>a\<in>set xs'. P a \<Longrightarrow> \<exists>ys x' zs. xs' = ys @ x' # zs \<and> P x' \<and> (\<forall>z\<in>set zs. \<not> P z)
\<exists>a\<in>set (x' # xs'). P a

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>Bex (set xs) P \<Longrightarrow> \<exists>ys x' zs. xs = ys @ x' # zs \<and> P x' \<and> (\<forall>z\<in>set zs. \<not> P z); Bex (set (a # xs)) P\<rbrakk> \<Longrightarrow> \<exists>ys x' zs. a # xs = ys @ x' # zs \<and> P x' \<and> (\<forall>z\<in>set zs. \<not> P z)
[PROOF STEP]
note IH = \<open>\<exists>a\<in>set xs'. P a
      \<Longrightarrow> \<exists>ys x' zs. xs' = ys @ x' # zs \<and> P x' \<and> (\<forall>z\<in>set zs. \<not> P z)\<close>
[PROOF STATE]
proof (state)
this:
\<exists>a\<in>set xs'. P a \<Longrightarrow> \<exists>ys x' zs. xs' = ys @ x' # zs \<and> P x' \<and> (\<forall>z\<in>set zs. \<not> P z)

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>Bex (set xs) P \<Longrightarrow> \<exists>ys x' zs. xs = ys @ x' # zs \<and> P x' \<and> (\<forall>z\<in>set zs. \<not> P z); Bex (set (a # xs)) P\<rbrakk> \<Longrightarrow> \<exists>ys x' zs. a # xs = ys @ x' # zs \<and> P x' \<and> (\<forall>z\<in>set zs. \<not> P z)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>ys x'a zs. x' # xs' = ys @ x'a # zs \<and> P x'a \<and> (\<forall>z\<in>set zs. \<not> P z)
[PROOF STEP]
proof(cases "\<exists>y\<in>set xs'. P y")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>y\<in>set xs'. P y \<Longrightarrow> \<exists>ys x'a zs. x' # xs' = ys @ x'a # zs \<and> P x'a \<and> (\<forall>z\<in>set zs. \<not> P z)
 2. \<not> (\<exists>y\<in>set xs'. P y) \<Longrightarrow> \<exists>ys x'a zs. x' # xs' = ys @ x'a # zs \<and> P x'a \<and> (\<forall>z\<in>set zs. \<not> P z)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<exists>y\<in>set xs'. P y

goal (2 subgoals):
 1. \<exists>y\<in>set xs'. P y \<Longrightarrow> \<exists>ys x'a zs. x' # xs' = ys @ x'a # zs \<and> P x'a \<and> (\<forall>z\<in>set zs. \<not> P z)
 2. \<not> (\<exists>y\<in>set xs'. P y) \<Longrightarrow> \<exists>ys x'a zs. x' # xs' = ys @ x'a # zs \<and> P x'a \<and> (\<forall>z\<in>set zs. \<not> P z)
[PROOF STEP]
from IH[OF this]
[PROOF STATE]
proof (chain)
picking this:
\<exists>ys x' zs. xs' = ys @ x' # zs \<and> P x' \<and> (\<forall>z\<in>set zs. \<not> P z)
[PROOF STEP]
obtain y ys zs where "xs' = ys @ y # zs"
        and "P y" and "\<forall>z\<in>set zs. \<not> P z"
[PROOF STATE]
proof (prove)
using this:
\<exists>ys x' zs. xs' = ys @ x' # zs \<and> P x' \<and> (\<forall>z\<in>set zs. \<not> P z)

goal (1 subgoal):
 1. (\<And>ys y zs. \<lbrakk>xs' = ys @ y # zs; P y; \<forall>z\<in>set zs. \<not> P z\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
xs' = ys @ y # zs
P y
\<forall>z\<in>set zs. \<not> P z

goal (2 subgoals):
 1. \<exists>y\<in>set xs'. P y \<Longrightarrow> \<exists>ys x'a zs. x' # xs' = ys @ x'a # zs \<and> P x'a \<and> (\<forall>z\<in>set zs. \<not> P z)
 2. \<not> (\<exists>y\<in>set xs'. P y) \<Longrightarrow> \<exists>ys x'a zs. x' # xs' = ys @ x'a # zs \<and> P x'a \<and> (\<forall>z\<in>set zs. \<not> P z)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
xs' = ys @ y # zs
P y
\<forall>z\<in>set zs. \<not> P z

goal (1 subgoal):
 1. \<exists>ys x'a zs. x' # xs' = ys @ x'a # zs \<and> P x'a \<and> (\<forall>z\<in>set zs. \<not> P z)
[PROOF STEP]
by (metis Cons_eq_append_conv)
[PROOF STATE]
proof (state)
this:
\<exists>ys x'a zs. x' # xs' = ys @ x'a # zs \<and> P x'a \<and> (\<forall>z\<in>set zs. \<not> P z)

goal (1 subgoal):
 1. \<not> (\<exists>y\<in>set xs'. P y) \<Longrightarrow> \<exists>ys x'a zs. x' # xs' = ys @ x'a # zs \<and> P x'a \<and> (\<forall>z\<in>set zs. \<not> P z)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<exists>y\<in>set xs'. P y) \<Longrightarrow> \<exists>ys x'a zs. x' # xs' = ys @ x'a # zs \<and> P x'a \<and> (\<forall>z\<in>set zs. \<not> P z)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (\<exists>y\<in>set xs'. P y)

goal (1 subgoal):
 1. \<not> (\<exists>y\<in>set xs'. P y) \<Longrightarrow> \<exists>ys x'a zs. x' # xs' = ys @ x'a # zs \<and> P x'a \<and> (\<forall>z\<in>set zs. \<not> P z)
[PROOF STEP]
with \<open>\<exists>y\<in>set (x'#xs'). P y\<close>
[PROOF STATE]
proof (chain)
picking this:
\<exists>y\<in>set (x' # xs'). P y
\<not> (\<exists>y\<in>set xs'. P y)
[PROOF STEP]
have "P x'"
[PROOF STATE]
proof (prove)
using this:
\<exists>y\<in>set (x' # xs'). P y
\<not> (\<exists>y\<in>set xs'. P y)

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

goal (1 subgoal):
 1. \<not> (\<exists>y\<in>set xs'. P y) \<Longrightarrow> \<exists>ys x'a zs. x' # xs' = ys @ x'a # zs \<and> P x'a \<and> (\<forall>z\<in>set zs. \<not> P z)
[PROOF STEP]
with False
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<exists>y\<in>set xs'. P y)
P x'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>y\<in>set xs'. P y)
P x'

goal (1 subgoal):
 1. \<exists>ys x'a zs. x' # xs' = ys @ x'a # zs \<and> P x'a \<and> (\<forall>z\<in>set zs. \<not> P z)
[PROOF STEP]
by (metis eq_Nil_appendI)
[PROOF STATE]
proof (state)
this:
\<exists>ys x'a zs. x' # xs' = ys @ x'a # zs \<and> P x'a \<and> (\<forall>z\<in>set zs. \<not> P z)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>ys x'a zs. x' # xs' = ys @ x'a # zs \<and> P x'a \<and> (\<forall>z\<in>set zs. \<not> P z)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>ys x' zs. xs = ys @ x' # zs \<and> P x' \<and> (\<forall>z\<in>set zs. \<not> P z)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma map_append_append_maps:
  assumes map:"map f xs = ys@zs"
  obtains xs' xs'' where "map f xs' = ys" and "map f xs'' = zs" and "xs=xs'@xs''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>xs' xs''. \<lbrakk>map f xs' = ys; map f xs'' = zs; xs = xs' @ xs''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis append_eq_conv_conj append_take_drop_id assms drop_map take_map that)