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

goal (1 subgoal):
 1. \<And>s vl s1 vl1. \<lbrakk>reachNT s; reach s1; \<Delta>4 s vl s1 vl1\<rbrakk> \<Longrightarrow> iaction (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s vl s1 vl1 \<or> (vl = [] \<longrightarrow> vl1 = []) \<and> reaction (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s vl s1 vl1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
reachNT s
reach s1
\<Delta>4 s vl s1 vl1
[PROOF STEP]
obtain uid CID  wl where uuid: "isREVNth s uid PID N"
  and rs: "reach s" and ph: "phase s CID \<ge> revPH" (is "?ph \<ge> revPH") and ss1: "s1 = s"
  and PID: "PID \<in>\<in> paperIDs s CID" and vl: "vl = map (Pair disPH) wl"
  and vl1: "vl1 = map (Pair disPH) wl"
[PROOF STATE]
proof (prove)
using this:
reachNT s
reach s1
\<Delta>4 s vl s1 vl1

goal (1 subgoal):
 1. (\<And>uid CID wl. \<lbrakk>isREVNth s uid PID N; reach s; revPH \<le> phase s CID; s1 = s; PID \<in>\<in> paperIDs s CID; vl = map (Pair disPH) wl; vl1 = map (Pair disPH) wl\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using reachNT_reach
[PROOF STATE]
proof (prove)
using this:
reachNT s
reach s1
\<Delta>4 s vl s1 vl1
reachNT ?s \<Longrightarrow> reach ?s

goal (1 subgoal):
 1. (\<And>uid CID wl. \<lbrakk>isREVNth s uid PID N; reach s; revPH \<le> phase s CID; s1 = s; PID \<in>\<in> paperIDs s CID; vl = map (Pair disPH) wl; vl1 = map (Pair disPH) wl\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding \<Delta>4_def
[PROOF STATE]
proof (prove)
using this:
reachNT s
reach s1
\<exists>cid uid. PID \<in>\<in> paperIDs s cid \<and> revPH \<le> phase s cid \<and> isREVNth s uid PID N \<and> s = s1 \<and> (\<exists>wl. vl = map (Pair disPH) wl \<and> vl1 = map (Pair disPH) wl)
reachNT ?s \<Longrightarrow> reach ?s

goal (1 subgoal):
 1. (\<And>uid CID wl. \<lbrakk>isREVNth s uid PID N; reach s; revPH \<le> phase s CID; s1 = s; PID \<in>\<in> paperIDs s CID; vl = map (Pair disPH) wl; vl1 = map (Pair disPH) wl\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
isREVNth s uid PID N
reach s
revPH \<le> phase s CID
s1 = s
PID \<in>\<in> paperIDs s CID
vl = map (Pair disPH) wl
vl1 = map (Pair disPH) wl

goal (1 subgoal):
 1. \<And>s vl s1 vl1. \<lbrakk>reachNT s; reach s1; \<Delta>4 s vl s1 vl1\<rbrakk> \<Longrightarrow> iaction (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s vl s1 vl1 \<or> (vl = [] \<longrightarrow> vl1 = []) \<and> reaction (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s vl s1 vl1
[PROOF STEP]
hence uid: "isRevNth s CID uid PID N"
[PROOF STATE]
proof (prove)
using this:
isREVNth s uid PID N
reach s
revPH \<le> phase s CID
s1 = s
PID \<in>\<in> paperIDs s CID
vl = map (Pair disPH) wl
vl1 = map (Pair disPH) wl

goal (1 subgoal):
 1. isRevNth s CID uid PID N
[PROOF STEP]
by (metis isREVNth_imp_isRevNth)
[PROOF STATE]
proof (state)
this:
isRevNth s CID uid PID N

goal (1 subgoal):
 1. \<And>s vl s1 vl1. \<lbrakk>reachNT s; reach s1; \<Delta>4 s vl s1 vl1\<rbrakk> \<Longrightarrow> iaction (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s vl s1 vl1 \<or> (vl = [] \<longrightarrow> vl1 = []) \<and> reaction (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e 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>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s vl s1 vl1 \<or> (vl = [] \<longrightarrow> vl1 = []) \<and> reaction (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e 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>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s vl s1 vl1 \<or> (vl = [] \<longrightarrow> vl1 = []) \<and> reaction (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e 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>4 s vl s1 vl1 \<or> \<Delta>e 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>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e 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>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e 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>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl'
[PROOF STEP]
let ?ph' = "phase s' CID"
[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>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e 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>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl'
[PROOF STEP]
have uid': "isRevNth s' CID uid PID N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isRevNth s' CID uid PID N
[PROOF STEP]
by (metis isRevNth_persistent rs step uid)
[PROOF STATE]
proof (state)
this:
isRevNth s' CID uid PID N

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>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl'
[PROOF STEP]
hence uuid': "isREVNth s' uid PID N"
[PROOF STATE]
proof (prove)
using this:
isRevNth s' CID uid PID N

goal (1 subgoal):
 1. isREVNth s' uid PID N
[PROOF STEP]
by (metis isREVNth_def)
[PROOF STATE]
proof (state)
this:
isREVNth s' uid PID N

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>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl'
[PROOF STEP]
have PID': "PID \<in>\<in> paperIDs s' CID"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. PID \<in>\<in> paperIDs s' CID
[PROOF STEP]
using PID rs
[PROOF STATE]
proof (prove)
using this:
PID \<in>\<in> paperIDs s CID
reach s

goal (1 subgoal):
 1. PID \<in>\<in> paperIDs s' CID
[PROOF STEP]
by (metis paperIDs_mono step)
[PROOF STATE]
proof (state)
this:
PID \<in>\<in> paperIDs s' CID

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>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl'
[PROOF STEP]
have ph': "phase s' CID \<ge> revPH"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. revPH \<le> phase s' CID
[PROOF STEP]
using rs isRevNth_geq_revPH local.step reach_PairI uid'
[PROOF STATE]
proof (prove)
using this:
reach s
\<lbrakk>reach ?s; isRevNth ?s ?confID ?uID ?papID ?n\<rbrakk> \<Longrightarrow> revPH \<le> phase ?s ?confID
step s a = (ou, s')
\<lbrakk>reach ?s; step ?s ?a = (?ou, ?s')\<rbrakk> \<Longrightarrow> reach ?s'
isRevNth s' CID uid PID N

goal (1 subgoal):
 1. revPH \<le> phase s' CID
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
revPH \<le> phase s' CID

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>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e 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>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e 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>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl'
[PROOF STEP]
proof(cases "\<phi> ?trn")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<phi> (Trans s a ou s') \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl'
 2. \<not> \<phi> (Trans s a ou s') \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl'
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<phi> (Trans s a ou s')

goal (2 subgoals):
 1. \<phi> (Trans s a ou s') \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl'
 2. \<not> \<phi> (Trans s a ou s') \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl'
[PROOF STEP]
note \<phi> = True
[PROOF STATE]
proof (state)
this:
\<phi> (Trans s a ou s')

goal (2 subgoals):
 1. \<phi> (Trans s a ou s') \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl'
 2. \<not> \<phi> (Trans s a ou s') \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl'
[PROOF STEP]
hence \<phi>1: "\<phi> ?trn1"
[PROOF STATE]
proof (prove)
using this:
\<phi> (Trans s a ou s')

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

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

goal (2 subgoals):
 1. \<phi> (Trans s a ou s') \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl'
 2. \<not> \<phi> (Trans s a ou s') \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl'
[PROOF STEP]
obtain w wl' where wl: "wl = w # wl'" and vl: "vl = (disPH,w) # map (Pair disPH) wl'"
        and vl1: "vl1 = (disPH,w) # map (Pair disPH) wl'" and vl': "vl' = map (Pair disPH) wl'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>w wl'. \<lbrakk>wl = w # wl'; vl = (disPH, w) # map (Pair disPH) wl'; vl1 = (disPH, w) # map (Pair disPH) wl'; vl' = map (Pair disPH) wl'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<phi> \<phi>1 c
[PROOF STATE]
proof (prove)
using this:
\<phi> (Trans s a ou s')
\<phi> (Trans s1 a ou s')
consume (Trans s a ou s') vl vl'

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

goal (1 subgoal):
 1. (\<And>w wl'. \<lbrakk>wl = w # wl'; map (Pair disPH) wl = (disPH, w) # map (Pair disPH) wl'; map (Pair disPH) wl = (disPH, w) # map (Pair disPH) wl'; vl' = map (Pair disPH) wl'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases wl) auto
[PROOF STATE]
proof (state)
this:
wl = w # wl'
vl = (disPH, w) # map (Pair disPH) wl'
vl1 = (disPH, w) # map (Pair disPH) wl'
vl' = map (Pair disPH) wl'

goal (2 subgoals):
 1. \<phi> (Trans s a ou s') \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl'
 2. \<not> \<phi> (Trans s a ou s') \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl'
[PROOF STEP]
have f: "f ?trn = (disPH, w)" "f ?trn1 = (disPH, w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (Trans s a ou s') = (disPH, w) &&& f (Trans s1 a ou s') = (disPH, w)
[PROOF STEP]
using \<phi> \<phi>1 c
[PROOF STATE]
proof (prove)
using this:
\<phi> (Trans s a ou s')
\<phi> (Trans s1 a ou s')
consume (Trans s a ou s') vl vl'

goal (1 subgoal):
 1. f (Trans s a ou s') = (disPH, w) &&& f (Trans s1 a ou s') = (disPH, w)
[PROOF STEP]
unfolding consume_def vl vl1 ss1
[PROOF STATE]
proof (prove)
using this:
\<phi> (Trans s a ou s')
\<phi> (Trans s a ou s')
if \<phi> (Trans s a ou s') then (disPH, w) # map (Pair disPH) wl' \<noteq> [] \<and> f (Trans s a ou s') = hd ((disPH, w) # map (Pair disPH) wl') \<and> vl' = tl ((disPH, w) # map (Pair disPH) wl') else vl' = (disPH, w) # map (Pair disPH) wl'

goal (1 subgoal):
 1. f (Trans s a ou s') = (disPH, w) &&& f (Trans s a ou s') = (disPH, w)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f (Trans s a ou s') = (disPH, w)
f (Trans s1 a ou s') = (disPH, w)

goal (2 subgoals):
 1. \<phi> (Trans s a ou s') \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl'
 2. \<not> \<phi> (Trans s a ou s') \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e 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>4 s vl s1 vl1 \<or> \<Delta>e 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>4 s' vl' ?s1' ?vl1' \<or> \<Delta>e 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]
using step
[PROOF STATE]
proof (prove)
using this:
step s a = (ou, s')

goal (1 subgoal):
 1. validTrans (Trans s1 a ou s')
[PROOF STEP]
unfolding ss1
[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>4 s' vl' s' ?vl1' \<or> \<Delta>e 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>4 s' vl' s' ?vl1' \<or> \<Delta>e s' vl' s' ?vl1'
[PROOF STEP]
show "consume ?trn1 vl1 vl'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. consume (Trans s1 a ou s') vl1 vl'
[PROOF STEP]
unfolding consume_def vl1 vl'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. if \<phi> (Trans s1 a ou s') then (disPH, w) # map (Pair disPH) wl' \<noteq> [] \<and> f (Trans s1 a ou s') = hd ((disPH, w) # map (Pair disPH) wl') \<and> map (Pair disPH) wl' = tl ((disPH, w) # map (Pair disPH) wl') else map (Pair disPH) wl' = (disPH, w) # map (Pair disPH) wl'
[PROOF STEP]
using \<phi>1 f
[PROOF STATE]
proof (prove)
using this:
\<phi> (Trans s1 a ou s')
f (Trans s a ou s') = (disPH, w)
f (Trans s1 a ou s') = (disPH, w)

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

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>4 s' vl' s' vl' \<or> \<Delta>e s' vl' s' vl'
[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>4 s' vl' s' vl' \<or> \<Delta>e s' vl' s' vl'
[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>4 s' vl' s' vl' \<or> \<Delta>e s' vl' s' vl'
[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>4 s' vl' s' vl' \<or> \<Delta>e s' vl' s' vl'
[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>4 s' vl' s' vl' \<or> \<Delta>e s' vl' s' vl'
[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]
by simp
[PROOF STATE]
proof (state)
this:
g (Trans s a ou s') = g (Trans s1 a ou s')

goal (1 subgoal):
 1. \<Delta>4 s' vl' s' vl' \<or> \<Delta>e s' vl' s' vl'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Delta>4 s' vl' s' vl' \<or> \<Delta>e s' vl' s' vl'
[PROOF STEP]
have "\<Delta>4 s' vl' s' vl'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Delta>4 s' vl' s' vl'
[PROOF STEP]
using ph' PID' uuid'
[PROOF STATE]
proof (prove)
using this:
revPH \<le> phase s' CID
PID \<in>\<in> paperIDs s' CID
isREVNth s' uid PID N

goal (1 subgoal):
 1. \<Delta>4 s' vl' s' vl'
[PROOF STEP]
unfolding \<Delta>4_def vl'
[PROOF STATE]
proof (prove)
using this:
revPH \<le> phase s' CID
PID \<in>\<in> paperIDs s' CID
isREVNth s' uid PID N

goal (1 subgoal):
 1. \<exists>cid uid. PID \<in>\<in> paperIDs s' cid \<and> revPH \<le> phase s' cid \<and> isREVNth s' uid PID N \<and> s' = s' \<and> (\<exists>wl. map (Pair disPH) wl' = map (Pair disPH) wl \<and> map (Pair disPH) wl' = map (Pair disPH) wl)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Delta>4 s' vl' s' vl'

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

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

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

goal (2 subgoals):
 1. \<phi> (Trans s a ou s') \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl'
 2. \<not> \<phi> (Trans s a ou s') \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e 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>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl'

goal (1 subgoal):
 1. match (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e 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>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl'

goal (1 subgoal):
 1. \<not> \<phi> (Trans s a ou s') \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> \<phi> (Trans s a ou s') \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl'
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> \<phi> (Trans s a ou s')

goal (1 subgoal):
 1. \<not> \<phi> (Trans s a ou s') \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl'
[PROOF STEP]
note \<phi> = False
[PROOF STATE]
proof (state)
this:
\<not> \<phi> (Trans s a ou s')

goal (1 subgoal):
 1. \<not> \<phi> (Trans s a ou s') \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) 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')

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

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

goal (1 subgoal):
 1. \<not> \<phi> (Trans s a ou s') \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e 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 s1 a ou s')

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

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

goal (1 subgoal):
 1. vl' = map (Pair disPH) wl
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vl' = vl

goal (1 subgoal):
 1. \<not> \<phi> (Trans s a ou s') \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e 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>4 s vl s1 vl1 \<or> \<Delta>e 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>4 s' vl' ?s1' ?vl1' \<or> \<Delta>e 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]
using step
[PROOF STATE]
proof (prove)
using this:
step s a = (ou, s')

goal (1 subgoal):
 1. validTrans (Trans s1 a ou s')
[PROOF STEP]
unfolding ss1
[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>4 s' vl' s' ?vl1' \<or> \<Delta>e 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>4 s' vl' s' ?vl1' \<or> \<Delta>e s' vl' s' ?vl1'
[PROOF STEP]
show "consume ?trn1 vl1 vl"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. consume (Trans s1 a ou s') vl1 vl
[PROOF STEP]
unfolding consume_def vl1 vl
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. if \<phi> (Trans s1 a ou s') then map (Pair disPH) wl \<noteq> [] \<and> f (Trans s1 a ou s') = hd (map (Pair disPH) wl) \<and> map (Pair disPH) wl = tl (map (Pair disPH) wl) else map (Pair disPH) wl = map (Pair disPH) wl
[PROOF STEP]
using \<phi>1
[PROOF STATE]
proof (prove)
using this:
\<not> \<phi> (Trans s1 a ou s')

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

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>4 s' vl' s' vl \<or> \<Delta>e s' vl' s' vl
[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>4 s' vl' s' vl \<or> \<Delta>e s' vl' s' vl
[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>4 s' vl' s' vl \<or> \<Delta>e s' vl' s' vl
[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>4 s' vl' s' vl \<or> \<Delta>e s' vl' s' vl
[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>4 s' vl' s' vl \<or> \<Delta>e s' vl' s' vl
[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]
by simp
[PROOF STATE]
proof (state)
this:
g (Trans s a ou s') = g (Trans s1 a ou s')

goal (1 subgoal):
 1. \<Delta>4 s' vl' s' vl \<or> \<Delta>e s' vl' s' vl
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Delta>4 s' vl' s' vl \<or> \<Delta>e s' vl' s' vl
[PROOF STEP]
have "\<Delta>4 s' vl' s' vl"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Delta>4 s' vl' s' vl
[PROOF STEP]
using ph' PID' uuid'
[PROOF STATE]
proof (prove)
using this:
revPH \<le> phase s' CID
PID \<in>\<in> paperIDs s' CID
isREVNth s' uid PID N

goal (1 subgoal):
 1. \<Delta>4 s' vl' s' vl
[PROOF STEP]
unfolding \<Delta>4_def vl' vl
[PROOF STATE]
proof (prove)
using this:
revPH \<le> phase s' CID
PID \<in>\<in> paperIDs s' CID
isREVNth s' uid PID N

goal (1 subgoal):
 1. \<exists>cid uid. PID \<in>\<in> paperIDs s' cid \<and> revPH \<le> phase s' cid \<and> isREVNth s' uid PID N \<and> s' = s' \<and> (\<exists>wla. map (Pair disPH) wl = map (Pair disPH) wla \<and> map (Pair disPH) wl = map (Pair disPH) wla)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Delta>4 s' vl' s' vl

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

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

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

goal (1 subgoal):
 1. \<not> \<phi> (Trans s a ou s') \<Longrightarrow> match (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e 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>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl'

goal (1 subgoal):
 1. match (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e 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>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e 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>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s s1 vl1 a ou s' vl' \<or> ignore (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e 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>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s vl s1 vl1

goal (1 subgoal):
 1. iaction (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s vl s1 vl1 \<or> (vl = [] \<longrightarrow> vl1 = []) \<and> reaction (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e 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>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s vl s1 vl1

goal (1 subgoal):
 1. iaction (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s vl s1 vl1 \<or> (vl = [] \<longrightarrow> vl1 = []) \<and> reaction (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s vl s1 vl1
[PROOF STEP]
using vl vl1
[PROOF STATE]
proof (prove)
using this:
reaction (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s vl s1 vl1
vl = map (Pair disPH) wl
vl1 = map (Pair disPH) wl

goal (1 subgoal):
 1. iaction (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s vl s1 vl1 \<or> (vl = [] \<longrightarrow> vl1 = []) \<and> reaction (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s vl s1 vl1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
iaction (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s vl s1 vl1 \<or> (vl = [] \<longrightarrow> vl1 = []) \<and> reaction (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e 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>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s vl s1 vl1 \<or> (vl = [] \<longrightarrow> vl1 = []) \<and> reaction (\<lambda>s vl s1 vl1. \<Delta>4 s vl s1 vl1 \<or> \<Delta>e s vl s1 vl1) s vl s1 vl1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma invarNT_K2exit: "invarNT (K2exit cid)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invarNT (K2exit cid)
[PROOF STEP]
unfolding invarNT_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s a ou s'. reachNT s \<and> K2exit cid s \<and> \<not> T (Trans s a ou s') \<and> step s a = (ou, s') \<longrightarrow> K2exit cid s'
[PROOF STEP]
apply (safe dest!: reachNT_reach)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s a ou s'. \<lbrakk>reach s; K2exit cid s; \<not> T (Trans s a ou s'); step s a = (ou, s')\<rbrakk> \<Longrightarrow> K2exit cid s'
[PROOF STEP]
subgoal for _ a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reach s_; K2exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_)\<rbrakk> \<Longrightarrow> K2exit cid s'_
[PROOF STEP]
apply(cases a)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x1. \<lbrakk>reach s_; K2exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Cact x1\<rbrakk> \<Longrightarrow> K2exit cid s'_
 2. \<And>x2. \<lbrakk>reach s_; K2exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2\<rbrakk> \<Longrightarrow> K2exit cid s'_
 3. \<And>x3. \<lbrakk>reach s_; K2exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = UUact x3\<rbrakk> \<Longrightarrow> K2exit cid s'_
 4. \<And>x4. \<lbrakk>reach s_; K2exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Ract x4\<rbrakk> \<Longrightarrow> K2exit cid s'_
 5. \<And>x5. \<lbrakk>reach s_; K2exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Lact x5\<rbrakk> \<Longrightarrow> K2exit cid s'_
[PROOF STEP]
subgoal for x1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reach s_; K2exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Cact x1\<rbrakk> \<Longrightarrow> K2exit cid s'_
[PROOF STEP]
apply(cases x1)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>x11 x12 x13 x14 x15. \<lbrakk>reach s_; K2exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Cact x1; x1 = cUser x11 x12 x13 x14 x15\<rbrakk> \<Longrightarrow> K2exit cid s'_
 2. \<And>x21 x22 x23 x24 x25. \<lbrakk>reach s_; K2exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Cact x1; x1 = cConf x21 x22 x23 x24 x25\<rbrakk> \<Longrightarrow> K2exit cid s'_
 3. \<And>x31 x32 x33 x34. \<lbrakk>reach s_; K2exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Cact x1; x1 = cPC x31 x32 x33 x34\<rbrakk> \<Longrightarrow> K2exit cid s'_
 4. \<And>x41 x42 x43 x44. \<lbrakk>reach s_; K2exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Cact x1; x1 = cChair x41 x42 x43 x44\<rbrakk> \<Longrightarrow> K2exit cid s'_
 5. \<And>x51 x52 x53 x54 x55 x56. \<lbrakk>reach s_; K2exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Cact x1; x1 = cPaper x51 x52 x53 x54 x55 x56\<rbrakk> \<Longrightarrow> K2exit cid s'_
 6. \<And>x61 x62 x63 x64 x65. \<lbrakk>reach s_; K2exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Cact x1; x1 = cAuthor x61 x62 x63 x64 x65\<rbrakk> \<Longrightarrow> K2exit cid s'_
 7. \<And>x71 x72 x73 x74 x75. \<lbrakk>reach s_; K2exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Cact x1; x1 = cConflict x71 x72 x73 x74 x75\<rbrakk> \<Longrightarrow> K2exit cid s'_
 8. \<And>x81 x82 x83 x84 x85. \<lbrakk>reach s_; K2exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Cact x1; x1 = cReview x81 x82 x83 x84 x85\<rbrakk> \<Longrightarrow> K2exit cid s'_
[PROOF STEP]
apply (fastforce simp add: c_defs K2exit_def geq_noPH_confIDs)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x2. \<lbrakk>reach s_; K2exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2\<rbrakk> \<Longrightarrow> K2exit cid s'_
 2. \<And>x3. \<lbrakk>reach s_; K2exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = UUact x3\<rbrakk> \<Longrightarrow> K2exit cid s'_
 3. \<And>x4. \<lbrakk>reach s_; K2exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Ract x4\<rbrakk> \<Longrightarrow> K2exit cid s'_
 4. \<And>x5. \<lbrakk>reach s_; K2exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Lact x5\<rbrakk> \<Longrightarrow> K2exit cid s'_
[PROOF STEP]
subgoal for x2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reach s_; K2exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2\<rbrakk> \<Longrightarrow> K2exit cid s'_
[PROOF STEP]
apply(cases x2)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>x11 x12 x13 x14 x15 x16. \<lbrakk>reach s_; K2exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uUser x11 x12 x13 x14 x15 x16\<rbrakk> \<Longrightarrow> K2exit cid s'_
 2. \<And>x21 x22 x23. \<lbrakk>reach s_; K2exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uConfA x21 x22 x23\<rbrakk> \<Longrightarrow> K2exit cid s'_
 3. \<And>x31 x32 x33 x34. \<lbrakk>reach s_; K2exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uPhase x31 x32 x33 x34\<rbrakk> \<Longrightarrow> K2exit cid s'_
 4. \<And>x41 x42 x43 x44 x45 x46. \<lbrakk>reach s_; K2exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uPaperTA x41 x42 x43 x44 x45 x46\<rbrakk> \<Longrightarrow> K2exit cid s'_
 5. \<And>x51 x52 x53 x54 x55. \<lbrakk>reach s_; K2exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uPaperC x51 x52 x53 x54 x55\<rbrakk> \<Longrightarrow> K2exit cid s'_
 6. \<And>x61 x62 x63 x64 x65. \<lbrakk>reach s_; K2exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uPref x61 x62 x63 x64 x65\<rbrakk> \<Longrightarrow> K2exit cid s'_
 7. \<And>x71 x72 x73 x74 x75 x76. \<lbrakk>reach s_; K2exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uReview x71 x72 x73 x74 x75 x76\<rbrakk> \<Longrightarrow> K2exit cid s'_
[PROOF STEP]
apply (fastforce simp add: u_defs K2exit_def paperIDs_equals)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x3. \<lbrakk>reach s_; K2exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = UUact x3\<rbrakk> \<Longrightarrow> K2exit cid s'_
 2. \<And>x4. \<lbrakk>reach s_; K2exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Ract x4\<rbrakk> \<Longrightarrow> K2exit cid s'_
 3. \<And>x5. \<lbrakk>reach s_; K2exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Lact x5\<rbrakk> \<Longrightarrow> K2exit cid s'_
[PROOF STEP]
subgoal for x3
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reach s_; K2exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = UUact x3\<rbrakk> \<Longrightarrow> K2exit cid s'_
[PROOF STEP]
apply(cases x3)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x11 x12 x13 x14. \<lbrakk>reach s_; K2exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = UUact x3; x3 = uuNews x11 x12 x13 x14\<rbrakk> \<Longrightarrow> K2exit cid s'_
 2. \<And>x21 x22 x23 x24 x25. \<lbrakk>reach s_; K2exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = UUact x3; x3 = uuDis x21 x22 x23 x24 x25\<rbrakk> \<Longrightarrow> K2exit cid s'_
 3. \<And>x31 x32 x33 x34 x35 x36. \<lbrakk>reach s_; K2exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = UUact x3; x3 = uuReview x31 x32 x33 x34 x35 x36\<rbrakk> \<Longrightarrow> K2exit cid s'_
 4. \<And>x41 x42 x43 x44 x45. \<lbrakk>reach s_; K2exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = UUact x3; x3 = uuDec x41 x42 x43 x44 x45\<rbrakk> \<Longrightarrow> K2exit cid s'_
[PROOF STEP]
apply (fastforce simp add: uu_defs K2exit_def)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x4. \<lbrakk>reach s_; K2exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Ract x4\<rbrakk> \<Longrightarrow> K2exit cid s'_
 2. \<And>x5. \<lbrakk>reach s_; K2exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Lact x5\<rbrakk> \<Longrightarrow> K2exit cid s'_
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma noVal_K2exit: "noVal (K2exit cid) v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. noVal (K2exit cid) v
[PROOF STEP]
apply(rule no\<phi>_noVal)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. no\<phi> (K2exit cid)
[PROOF STEP]
unfolding no\<phi>_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s a ou s'. reachNT s \<and> K2exit cid s \<and> step s a = (ou, s') \<longrightarrow> \<not> \<phi> (Trans s a ou s')
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s a ou s'. \<lbrakk>reachNT s; K2exit cid s; step s a = (ou, s'); \<phi> (Trans s a ou s')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
subgoal for _ a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reachNT s_; K2exit cid s_; step s_ a = (ou_, s'_); \<phi> (Trans s_ a ou_ s'_)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(cases a)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x1. \<lbrakk>reachNT s_; K2exit cid s_; step s_ a = (ou_, s'_); \<phi> (Trans s_ a ou_ s'_); a = Cact x1\<rbrakk> \<Longrightarrow> False
 2. \<And>x2. \<lbrakk>reachNT s_; K2exit cid s_; step s_ a = (ou_, s'_); \<phi> (Trans s_ a ou_ s'_); a = Uact x2\<rbrakk> \<Longrightarrow> False
 3. \<And>x3. \<lbrakk>reachNT s_; K2exit cid s_; step s_ a = (ou_, s'_); \<phi> (Trans s_ a ou_ s'_); a = UUact x3\<rbrakk> \<Longrightarrow> False
 4. \<And>x4. \<lbrakk>reachNT s_; K2exit cid s_; step s_ a = (ou_, s'_); \<phi> (Trans s_ a ou_ s'_); a = Ract x4\<rbrakk> \<Longrightarrow> False
 5. \<And>x5. \<lbrakk>reachNT s_; K2exit cid s_; step s_ a = (ou_, s'_); \<phi> (Trans s_ a ou_ s'_); a = Lact x5\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reachNT s_; K2exit cid s_; step s_ a = (ou_, s'_); \<phi> (Trans s_ a ou_ s'_); a = Cact x1_\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by (fastforce simp add: c_defs K2exit_def)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x2. \<lbrakk>reachNT s_; K2exit cid s_; step s_ a = (ou_, s'_); \<phi> (Trans s_ a ou_ s'_); a = Uact x2\<rbrakk> \<Longrightarrow> False
 2. \<And>x3. \<lbrakk>reachNT s_; K2exit cid s_; step s_ a = (ou_, s'_); \<phi> (Trans s_ a ou_ s'_); a = UUact x3\<rbrakk> \<Longrightarrow> False
 3. \<And>x4. \<lbrakk>reachNT s_; K2exit cid s_; step s_ a = (ou_, s'_); \<phi> (Trans s_ a ou_ s'_); a = Ract x4\<rbrakk> \<Longrightarrow> False
 4. \<And>x5. \<lbrakk>reachNT s_; K2exit cid s_; step s_ a = (ou_, s'_); \<phi> (Trans s_ a ou_ s'_); a = Lact x5\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
subgoal for x2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reachNT s_; K2exit cid s_; step s_ a = (ou_, s'_); \<phi> (Trans s_ a ou_ s'_); a = Uact x2\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(cases x2)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>x11 x12 x13 x14 x15 x16. \<lbrakk>reachNT s_; K2exit cid s_; step s_ a = (ou_, s'_); \<phi> (Trans s_ a ou_ s'_); a = Uact x2; x2 = uUser x11 x12 x13 x14 x15 x16\<rbrakk> \<Longrightarrow> False
 2. \<And>x21 x22 x23. \<lbrakk>reachNT s_; K2exit cid s_; step s_ a = (ou_, s'_); \<phi> (Trans s_ a ou_ s'_); a = Uact x2; x2 = uConfA x21 x22 x23\<rbrakk> \<Longrightarrow> False
 3. \<And>x31 x32 x33 x34. \<lbrakk>reachNT s_; K2exit cid s_; step s_ a = (ou_, s'_); \<phi> (Trans s_ a ou_ s'_); a = Uact x2; x2 = uPhase x31 x32 x33 x34\<rbrakk> \<Longrightarrow> False
 4. \<And>x41 x42 x43 x44 x45 x46. \<lbrakk>reachNT s_; K2exit cid s_; step s_ a = (ou_, s'_); \<phi> (Trans s_ a ou_ s'_); a = Uact x2; x2 = uPaperTA x41 x42 x43 x44 x45 x46\<rbrakk> \<Longrightarrow> False
 5. \<And>x51 x52 x53 x54 x55. \<lbrakk>reachNT s_; K2exit cid s_; step s_ a = (ou_, s'_); \<phi> (Trans s_ a ou_ s'_); a = Uact x2; x2 = uPaperC x51 x52 x53 x54 x55\<rbrakk> \<Longrightarrow> False
 6. \<And>x61 x62 x63 x64 x65. \<lbrakk>reachNT s_; K2exit cid s_; step s_ a = (ou_, s'_); \<phi> (Trans s_ a ou_ s'_); a = Uact x2; x2 = uPref x61 x62 x63 x64 x65\<rbrakk> \<Longrightarrow> False
 7. \<And>x71 x72 x73 x74 x75 x76. \<lbrakk>reachNT s_; K2exit cid s_; step s_ a = (ou_, s'_); \<phi> (Trans s_ a ou_ s'_); a = Uact x2; x2 = uReview x71 x72 x73 x74 x75 x76\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (auto simp add: u_defs K2exit_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x71 x72 aa aaa b x1 x2a x3 x4 x5 x6. \<lbrakk>ou_ = outOK; a = Uact (uReview x71 x72 (pass s_ x72) PID N (aa, aaa, b)); x2 = uReview x71 x72 (pass s_ x72) PID N (aa, aaa, b); reachNT s_; PID \<in>\<in> paperIDs s_ cid; x71 \<in>\<in> confIDs s_; revPH < phase s_ cid; \<forall>uid. Rev PID N \<notin> set (roles s_ cid uid); x72 \<in>\<in> userIDs s_; PID \<in>\<in> paperIDs s_ x71; phase s_ x71 = revPH; isRev s_ x71 x72 PID; getReviewIndex s_ x71 x72 PID = N; paper s_ PID = Paper x1 x2a x3 x4 x5 x6; s'_ = s_\<lparr>paper := (paper s_)(PID := Paper x1 x2a x3 (x4[N := (aa, aaa, b) # emptyReview]) x5 x6)\<rparr>\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (metis less_not_refl paperIDs_equals reachNT_reach)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x3. \<lbrakk>reachNT s_; K2exit cid s_; step s_ a = (ou_, s'_); \<phi> (Trans s_ a ou_ s'_); a = UUact x3\<rbrakk> \<Longrightarrow> False
 2. \<And>x4. \<lbrakk>reachNT s_; K2exit cid s_; step s_ a = (ou_, s'_); \<phi> (Trans s_ a ou_ s'_); a = Ract x4\<rbrakk> \<Longrightarrow> False
 3. \<And>x5. \<lbrakk>reachNT s_; K2exit cid s_; step s_ a = (ou_, s'_); \<phi> (Trans s_ a ou_ s'_); a = Lact x5\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
subgoal for x3
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reachNT s_; K2exit cid s_; step s_ a = (ou_, s'_); \<phi> (Trans s_ a ou_ s'_); a = UUact x3\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(cases x3)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x11 x12 x13 x14. \<lbrakk>reachNT s_; K2exit cid s_; step s_ a = (ou_, s'_); \<phi> (Trans s_ a ou_ s'_); a = UUact x3; x3 = uuNews x11 x12 x13 x14\<rbrakk> \<Longrightarrow> False
 2. \<And>x21 x22 x23 x24 x25. \<lbrakk>reachNT s_; K2exit cid s_; step s_ a = (ou_, s'_); \<phi> (Trans s_ a ou_ s'_); a = UUact x3; x3 = uuDis x21 x22 x23 x24 x25\<rbrakk> \<Longrightarrow> False
 3. \<And>x31 x32 x33 x34 x35 x36. \<lbrakk>reachNT s_; K2exit cid s_; step s_ a = (ou_, s'_); \<phi> (Trans s_ a ou_ s'_); a = UUact x3; x3 = uuReview x31 x32 x33 x34 x35 x36\<rbrakk> \<Longrightarrow> False
 4. \<And>x41 x42 x43 x44 x45. \<lbrakk>reachNT s_; K2exit cid s_; step s_ a = (ou_, s'_); \<phi> (Trans s_ a ou_ s'_); a = UUact x3; x3 = uuDec x41 x42 x43 x44 x45\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (auto simp add: uu_defs K2exit_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x31 x32 aa aaa b x1 x2 x3a x4 x5 x6. \<lbrakk>ou_ = outOK; a = UUact (uuReview x31 x32 (pass s_ x32) PID N (aa, aaa, b)); x3 = uuReview x31 x32 (pass s_ x32) PID N (aa, aaa, b); reachNT s_; PID \<in>\<in> paperIDs s_ cid; x31 \<in>\<in> confIDs s_; revPH < phase s_ cid; \<forall>uid. Rev PID N \<notin> set (roles s_ cid uid); x32 \<in>\<in> userIDs s_; PID \<in>\<in> paperIDs s_ x31; phase s_ x31 = disPH; isRev s_ x31 x32 PID; getReviewIndex s_ x31 x32 PID = N; paper s_ PID = Paper x1 x2 x3a x4 x5 x6; s'_ = s_\<lparr>paper := (paper s_)(PID := Paper x1 x2 x3a (x4[N := (aa, aaa, b) # x4 ! N]) x5 x6)\<rparr>\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (metis isRev_def3 paperIDs_equals reachNT_reach)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x4. \<lbrakk>reachNT s_; K2exit cid s_; step s_ a = (ou_, s'_); \<phi> (Trans s_ a ou_ s'_); a = Ract x4\<rbrakk> \<Longrightarrow> False
 2. \<And>x5. \<lbrakk>reachNT s_; K2exit cid s_; step s_ a = (ou_, s'_); \<phi> (Trans s_ a ou_ s'_); a = Lact x5\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma invarNT_K3exit: "invarNT (K3exit cid)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invarNT (K3exit cid)
[PROOF STEP]
unfolding invarNT_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s a ou s'. reachNT s \<and> K3exit cid s \<and> \<not> T (Trans s a ou s') \<and> step s a = (ou, s') \<longrightarrow> K3exit cid s'
[PROOF STEP]
apply (safe dest!: reachNT_reach)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s a ou s'. \<lbrakk>reach s; K3exit cid s; \<not> T (Trans s a ou s'); step s a = (ou, s')\<rbrakk> \<Longrightarrow> K3exit cid s'
[PROOF STEP]
subgoal for _ a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reach s_; K3exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_)\<rbrakk> \<Longrightarrow> K3exit cid s'_
[PROOF STEP]
apply(cases a)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x1. \<lbrakk>reach s_; K3exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Cact x1\<rbrakk> \<Longrightarrow> K3exit cid s'_
 2. \<And>x2. \<lbrakk>reach s_; K3exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2\<rbrakk> \<Longrightarrow> K3exit cid s'_
 3. \<And>x3. \<lbrakk>reach s_; K3exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = UUact x3\<rbrakk> \<Longrightarrow> K3exit cid s'_
 4. \<And>x4. \<lbrakk>reach s_; K3exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Ract x4\<rbrakk> \<Longrightarrow> K3exit cid s'_
 5. \<And>x5. \<lbrakk>reach s_; K3exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Lact x5\<rbrakk> \<Longrightarrow> K3exit cid s'_
[PROOF STEP]
subgoal for x1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reach s_; K3exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Cact x1\<rbrakk> \<Longrightarrow> K3exit cid s'_
[PROOF STEP]
apply(cases x1)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>x11 x12 x13 x14 x15. \<lbrakk>reach s_; K3exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Cact x1; x1 = cUser x11 x12 x13 x14 x15\<rbrakk> \<Longrightarrow> K3exit cid s'_
 2. \<And>x21 x22 x23 x24 x25. \<lbrakk>reach s_; K3exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Cact x1; x1 = cConf x21 x22 x23 x24 x25\<rbrakk> \<Longrightarrow> K3exit cid s'_
 3. \<And>x31 x32 x33 x34. \<lbrakk>reach s_; K3exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Cact x1; x1 = cPC x31 x32 x33 x34\<rbrakk> \<Longrightarrow> K3exit cid s'_
 4. \<And>x41 x42 x43 x44. \<lbrakk>reach s_; K3exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Cact x1; x1 = cChair x41 x42 x43 x44\<rbrakk> \<Longrightarrow> K3exit cid s'_
 5. \<And>x51 x52 x53 x54 x55 x56. \<lbrakk>reach s_; K3exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Cact x1; x1 = cPaper x51 x52 x53 x54 x55 x56\<rbrakk> \<Longrightarrow> K3exit cid s'_
 6. \<And>x61 x62 x63 x64 x65. \<lbrakk>reach s_; K3exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Cact x1; x1 = cAuthor x61 x62 x63 x64 x65\<rbrakk> \<Longrightarrow> K3exit cid s'_
 7. \<And>x71 x72 x73 x74 x75. \<lbrakk>reach s_; K3exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Cact x1; x1 = cConflict x71 x72 x73 x74 x75\<rbrakk> \<Longrightarrow> K3exit cid s'_
 8. \<And>x81 x82 x83 x84 x85. \<lbrakk>reach s_; K3exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Cact x1; x1 = cReview x81 x82 x83 x84 x85\<rbrakk> \<Longrightarrow> K3exit cid s'_
[PROOF STEP]
apply (fastforce simp add: c_defs K3exit_def geq_noPH_confIDs)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x2. \<lbrakk>reach s_; K3exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2\<rbrakk> \<Longrightarrow> K3exit cid s'_
 2. \<And>x3. \<lbrakk>reach s_; K3exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = UUact x3\<rbrakk> \<Longrightarrow> K3exit cid s'_
 3. \<And>x4. \<lbrakk>reach s_; K3exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Ract x4\<rbrakk> \<Longrightarrow> K3exit cid s'_
 4. \<And>x5. \<lbrakk>reach s_; K3exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Lact x5\<rbrakk> \<Longrightarrow> K3exit cid s'_
[PROOF STEP]
subgoal for x2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reach s_; K3exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2\<rbrakk> \<Longrightarrow> K3exit cid s'_
[PROOF STEP]
apply(cases x2)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>x11 x12 x13 x14 x15 x16. \<lbrakk>reach s_; K3exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uUser x11 x12 x13 x14 x15 x16\<rbrakk> \<Longrightarrow> K3exit cid s'_
 2. \<And>x21 x22 x23. \<lbrakk>reach s_; K3exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uConfA x21 x22 x23\<rbrakk> \<Longrightarrow> K3exit cid s'_
 3. \<And>x31 x32 x33 x34. \<lbrakk>reach s_; K3exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uPhase x31 x32 x33 x34\<rbrakk> \<Longrightarrow> K3exit cid s'_
 4. \<And>x41 x42 x43 x44 x45 x46. \<lbrakk>reach s_; K3exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uPaperTA x41 x42 x43 x44 x45 x46\<rbrakk> \<Longrightarrow> K3exit cid s'_
 5. \<And>x51 x52 x53 x54 x55. \<lbrakk>reach s_; K3exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uPaperC x51 x52 x53 x54 x55\<rbrakk> \<Longrightarrow> K3exit cid s'_
 6. \<And>x61 x62 x63 x64 x65. \<lbrakk>reach s_; K3exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uPref x61 x62 x63 x64 x65\<rbrakk> \<Longrightarrow> K3exit cid s'_
 7. \<And>x71 x72 x73 x74 x75 x76. \<lbrakk>reach s_; K3exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Uact x2; x2 = uReview x71 x72 x73 x74 x75 x76\<rbrakk> \<Longrightarrow> K3exit cid s'_
[PROOF STEP]
apply (fastforce simp add: u_defs K3exit_def paperIDs_equals)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x3. \<lbrakk>reach s_; K3exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = UUact x3\<rbrakk> \<Longrightarrow> K3exit cid s'_
 2. \<And>x4. \<lbrakk>reach s_; K3exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Ract x4\<rbrakk> \<Longrightarrow> K3exit cid s'_
 3. \<And>x5. \<lbrakk>reach s_; K3exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Lact x5\<rbrakk> \<Longrightarrow> K3exit cid s'_
[PROOF STEP]
subgoal for x3
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reach s_; K3exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = UUact x3\<rbrakk> \<Longrightarrow> K3exit cid s'_
[PROOF STEP]
apply(cases x3)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x11 x12 x13 x14. \<lbrakk>reach s_; K3exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = UUact x3; x3 = uuNews x11 x12 x13 x14\<rbrakk> \<Longrightarrow> K3exit cid s'_
 2. \<And>x21 x22 x23 x24 x25. \<lbrakk>reach s_; K3exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = UUact x3; x3 = uuDis x21 x22 x23 x24 x25\<rbrakk> \<Longrightarrow> K3exit cid s'_
 3. \<And>x31 x32 x33 x34 x35 x36. \<lbrakk>reach s_; K3exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = UUact x3; x3 = uuReview x31 x32 x33 x34 x35 x36\<rbrakk> \<Longrightarrow> K3exit cid s'_
 4. \<And>x41 x42 x43 x44 x45. \<lbrakk>reach s_; K3exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = UUact x3; x3 = uuDec x41 x42 x43 x44 x45\<rbrakk> \<Longrightarrow> K3exit cid s'_
[PROOF STEP]
apply (fastforce simp add: uu_defs K3exit_def)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x4. \<lbrakk>reach s_; K3exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Ract x4\<rbrakk> \<Longrightarrow> K3exit cid s'_
 2. \<And>x5. \<lbrakk>reach s_; K3exit cid s_; \<not> T (Trans s_ a ou_ s'_); step s_ a = (ou_, s'_); a = Lact x5\<rbrakk> \<Longrightarrow> K3exit cid s'_
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma noVal_K3exit: "noVal (K3exit cid) (revPH,u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. noVal (K3exit cid) (revPH, u)
[PROOF STEP]
unfolding noVal_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s a ou s'. reachNT s \<and> K3exit cid s \<and> step s a = (ou, s') \<and> \<phi> (Trans s a ou s') \<longrightarrow> f (Trans s a ou s') \<noteq> (revPH, u)
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s a ou s'. \<lbrakk>reachNT s; K3exit cid s; step s a = (ou, s'); \<phi> (Trans s a ou s'); f (Trans s a ou s') = (revPH, u)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
subgoal for _ a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reachNT s_; K3exit cid s_; step s_ a = (ou_, s'_); \<phi> (Trans s_ a ou_ s'_); f (Trans s_ a ou_ s'_) = (revPH, u)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(cases a)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x1. \<lbrakk>reachNT s_; K3exit cid s_; step s_ a = (ou_, s'_); \<phi> (Trans s_ a ou_ s'_); f (Trans s_ a ou_ s'_) = (revPH, u); a = Cact x1\<rbrakk> \<Longrightarrow> False
 2. \<And>x2. \<lbrakk>reachNT s_; K3exit cid s_; step s_ a = (ou_, s'_); \<phi> (Trans s_ a ou_ s'_); f (Trans s_ a ou_ s'_) = (revPH, u); a = Uact x2\<rbrakk> \<Longrightarrow> False
 3. \<And>x3. \<lbrakk>reachNT s_; K3exit cid s_; step s_ a = (ou_, s'_); \<phi> (Trans s_ a ou_ s'_); f (Trans s_ a ou_ s'_) = (revPH, u); a = UUact x3\<rbrakk> \<Longrightarrow> False
 4. \<And>x4. \<lbrakk>reachNT s_; K3exit cid s_; step s_ a = (ou_, s'_); \<phi> (Trans s_ a ou_ s'_); f (Trans s_ a ou_ s'_) = (revPH, u); a = Ract x4\<rbrakk> \<Longrightarrow> False
 5. \<And>x5. \<lbrakk>reachNT s_; K3exit cid s_; step s_ a = (ou_, s'_); \<phi> (Trans s_ a ou_ s'_); f (Trans s_ a ou_ s'_) = (revPH, u); a = Lact x5\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reachNT s_; K3exit cid s_; step s_ a = (ou_, s'_); \<phi> (Trans s_ a ou_ s'_); f (Trans s_ a ou_ s'_) = (revPH, u); a = Cact x1_\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by (fastforce simp add: c_defs K3exit_def)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x2. \<lbrakk>reachNT s_; K3exit cid s_; step s_ a = (ou_, s'_); \<phi> (Trans s_ a ou_ s'_); f (Trans s_ a ou_ s'_) = (revPH, u); a = Uact x2\<rbrakk> \<Longrightarrow> False
 2. \<And>x3. \<lbrakk>reachNT s_; K3exit cid s_; step s_ a = (ou_, s'_); \<phi> (Trans s_ a ou_ s'_); f (Trans s_ a ou_ s'_) = (revPH, u); a = UUact x3\<rbrakk> \<Longrightarrow> False
 3. \<And>x4. \<lbrakk>reachNT s_; K3exit cid s_; step s_ a = (ou_, s'_); \<phi> (Trans s_ a ou_ s'_); f (Trans s_ a ou_ s'_) = (revPH, u); a = Ract x4\<rbrakk> \<Longrightarrow> False
 4. \<And>x5. \<lbrakk>reachNT s_; K3exit cid s_; step s_ a = (ou_, s'_); \<phi> (Trans s_ a ou_ s'_); f (Trans s_ a ou_ s'_) = (revPH, u); a = Lact x5\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
subgoal for x2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reachNT s_; K3exit cid s_; step s_ a = (ou_, s'_); \<phi> (Trans s_ a ou_ s'_); f (Trans s_ a ou_ s'_) = (revPH, u); a = Uact x2\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(cases x2)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>x11 x12 x13 x14 x15 x16. \<lbrakk>reachNT s_; K3exit cid s_; step s_ a = (ou_, s'_); \<phi> (Trans s_ a ou_ s'_); f (Trans s_ a ou_ s'_) = (revPH, u); a = Uact x2; x2 = uUser x11 x12 x13 x14 x15 x16\<rbrakk> \<Longrightarrow> False
 2. \<And>x21 x22 x23. \<lbrakk>reachNT s_; K3exit cid s_; step s_ a = (ou_, s'_); \<phi> (Trans s_ a ou_ s'_); f (Trans s_ a ou_ s'_) = (revPH, u); a = Uact x2; x2 = uConfA x21 x22 x23\<rbrakk> \<Longrightarrow> False
 3. \<And>x31 x32 x33 x34. \<lbrakk>reachNT s_; K3exit cid s_; step s_ a = (ou_, s'_); \<phi> (Trans s_ a ou_ s'_); f (Trans s_ a ou_ s'_) = (revPH, u); a = Uact x2; x2 = uPhase x31 x32 x33 x34\<rbrakk> \<Longrightarrow> False
 4. \<And>x41 x42 x43 x44 x45 x46. \<lbrakk>reachNT s_; K3exit cid s_; step s_ a = (ou_, s'_); \<phi> (Trans s_ a ou_ s'_); f (Trans s_ a ou_ s'_) = (revPH, u); a = Uact x2; x2 = uPaperTA x41 x42 x43 x44 x45 x46\<rbrakk> \<Longrightarrow> False
 5. \<And>x51 x52 x53 x54 x55. \<lbrakk>reachNT s_; K3exit cid s_; step s_ a = (ou_, s'_); \<phi> (Trans s_ a ou_ s'_); f (Trans s_ a ou_ s'_) = (revPH, u); a = Uact x2; x2 = uPaperC x51 x52 x53 x54 x55\<rbrakk> \<Longrightarrow> False
 6. \<And>x61 x62 x63 x64 x65. \<lbrakk>reachNT s_; K3exit cid s_; step s_ a = (ou_, s'_); \<phi> (Trans s_ a ou_ s'_); f (Trans s_ a ou_ s'_) = (revPH, u); a = Uact x2; x2 = uPref x61 x62 x63 x64 x65\<rbrakk> \<Longrightarrow> False
 7. \<And>x71 x72 x73 x74 x75 x76. \<lbrakk>reachNT s_; K3exit cid s_; step s_ a = (ou_, s'_); \<phi> (Trans s_ a ou_ s'_); f (Trans s_ a ou_ s'_) = (revPH, u); a = Uact x2; x2 = uReview x71 x72 x73 x74 x75 x76\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (auto simp add: u_defs K3exit_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x71 x72 x1 x2a x3 x4 x5 x6. \<lbrakk>ou_ = outOK; phase s_ x71 = revPH; a = Uact (uReview x71 x72 (pass s_ x72) PID N u); x2 = uReview x71 x72 (pass s_ x72) PID N u; reachNT s_; PID \<in>\<in> paperIDs s_ cid; revPH < phase s_ cid; x71 \<in>\<in> confIDs s_; x72 \<in>\<in> userIDs s_; PID \<in>\<in> paperIDs s_ x71; isRev s_ x71 x72 PID; getReviewIndex s_ x71 x72 PID = N; paper s_ PID = Paper x1 x2a x3 x4 x5 x6; s'_ = s_\<lparr>paper := (paper s_)(PID := Paper x1 x2a x3 (x4[N := u # emptyReview]) x5 x6)\<rparr>\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (metis less_not_refl paperIDs_equals reachNT_reach)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x3. \<lbrakk>reachNT s_; K3exit cid s_; step s_ a = (ou_, s'_); \<phi> (Trans s_ a ou_ s'_); f (Trans s_ a ou_ s'_) = (revPH, u); a = UUact x3\<rbrakk> \<Longrightarrow> False
 2. \<And>x4. \<lbrakk>reachNT s_; K3exit cid s_; step s_ a = (ou_, s'_); \<phi> (Trans s_ a ou_ s'_); f (Trans s_ a ou_ s'_) = (revPH, u); a = Ract x4\<rbrakk> \<Longrightarrow> False
 3. \<And>x5. \<lbrakk>reachNT s_; K3exit cid s_; step s_ a = (ou_, s'_); \<phi> (Trans s_ a ou_ s'_); f (Trans s_ a ou_ s'_) = (revPH, u); a = Lact x5\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
subgoal for x3
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reachNT s_; K3exit cid s_; step s_ a = (ou_, s'_); \<phi> (Trans s_ a ou_ s'_); f (Trans s_ a ou_ s'_) = (revPH, u); a = UUact x3\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(cases x3)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x11 x12 x13 x14. \<lbrakk>reachNT s_; K3exit cid s_; step s_ a = (ou_, s'_); \<phi> (Trans s_ a ou_ s'_); f (Trans s_ a ou_ s'_) = (revPH, u); a = UUact x3; x3 = uuNews x11 x12 x13 x14\<rbrakk> \<Longrightarrow> False
 2. \<And>x21 x22 x23 x24 x25. \<lbrakk>reachNT s_; K3exit cid s_; step s_ a = (ou_, s'_); \<phi> (Trans s_ a ou_ s'_); f (Trans s_ a ou_ s'_) = (revPH, u); a = UUact x3; x3 = uuDis x21 x22 x23 x24 x25\<rbrakk> \<Longrightarrow> False
 3. \<And>x31 x32 x33 x34 x35 x36. \<lbrakk>reachNT s_; K3exit cid s_; step s_ a = (ou_, s'_); \<phi> (Trans s_ a ou_ s'_); f (Trans s_ a ou_ s'_) = (revPH, u); a = UUact x3; x3 = uuReview x31 x32 x33 x34 x35 x36\<rbrakk> \<Longrightarrow> False
 4. \<And>x41 x42 x43 x44 x45. \<lbrakk>reachNT s_; K3exit cid s_; step s_ a = (ou_, s'_); \<phi> (Trans s_ a ou_ s'_); f (Trans s_ a ou_ s'_) = (revPH, u); a = UUact x3; x3 = uuDec x41 x42 x43 x44 x45\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (auto simp add: uu_defs K3exit_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x4. \<lbrakk>reachNT s_; K3exit cid s_; step s_ a = (ou_, s'_); \<phi> (Trans s_ a ou_ s'_); f (Trans s_ a ou_ s'_) = (revPH, u); a = Ract x4\<rbrakk> \<Longrightarrow> False
 2. \<And>x5. \<lbrakk>reachNT s_; K3exit cid s_; step s_ a = (ou_, s'_); \<phi> (Trans s_ a ou_ s'_); f (Trans s_ a ou_ s'_) = (revPH, u); a = Lact x5\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma unwind_exit_\<Delta>e: "unwind_exit \<Delta>e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unwind_exit \<Delta>e
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s vl s1 vl1. \<lbrakk>reachNT s; reach s1; \<Delta>e s vl s1 vl1\<rbrakk> \<Longrightarrow> vl \<noteq> [] \<and> exit s (hd vl)
[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>e s vl s1 vl1\<rbrakk> \<Longrightarrow> vl \<noteq> [] \<and> exit s (hd vl)
[PROOF STEP]
assume rsT: "reachNT s" and rs1: "reach s1" and \<Delta>e: "\<Delta>e s vl s1 vl1"
[PROOF STATE]
proof (state)
this:
reachNT s
reach s1
\<Delta>e s vl s1 vl1

goal (1 subgoal):
 1. \<And>s vl s1 vl1. \<lbrakk>reachNT s; reach s1; \<Delta>e s vl s1 vl1\<rbrakk> \<Longrightarrow> vl \<noteq> [] \<and> exit s (hd vl)
[PROOF STEP]
hence rs:  "reach s" and vl: "vl \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
reachNT s
reach s1
\<Delta>e s vl s1 vl1

goal (1 subgoal):
 1. reach s &&& vl \<noteq> []
[PROOF STEP]
using reachNT_reach
[PROOF STATE]
proof (prove)
using this:
reachNT s
reach s1
\<Delta>e s vl s1 vl1
reachNT ?s \<Longrightarrow> reach ?s

goal (1 subgoal):
 1. reach s &&& vl \<noteq> []
[PROOF STEP]
unfolding \<Delta>e_def
[PROOF STATE]
proof (prove)
using this:
reachNT s
reach s1
vl \<noteq> [] \<and> ((\<exists>cid. PID \<in>\<in> paperIDs s cid \<and> revPH < phase s cid \<and> (\<nexists>uid. isREVNth s uid PID N)) \<or> (\<exists>cid. PID \<in>\<in> paperIDs s cid \<and> revPH < phase s cid \<and> fst (hd vl) = revPH))
reachNT ?s \<Longrightarrow> reach ?s

goal (1 subgoal):
 1. reach s &&& vl \<noteq> []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
reach s
vl \<noteq> []

goal (1 subgoal):
 1. \<And>s vl s1 vl1. \<lbrakk>reachNT s; reach s1; \<Delta>e s vl s1 vl1\<rbrakk> \<Longrightarrow> vl \<noteq> [] \<and> exit s (hd vl)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
reach s
vl \<noteq> []
[PROOF STEP]
obtain CID where K: "K2exit CID s \<or> K3exit CID s" and PID: "PID \<in>\<in> paperIDs s CID"
[PROOF STATE]
proof (prove)
using this:
reach s
vl \<noteq> []

goal (1 subgoal):
 1. (\<And>CID. \<lbrakk>K2exit CID s \<or> K3exit CID s; PID \<in>\<in> paperIDs s CID\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<Delta>e
[PROOF STATE]
proof (prove)
using this:
reach s
vl \<noteq> []
\<Delta>e s vl s1 vl1

goal (1 subgoal):
 1. (\<And>CID. \<lbrakk>K2exit CID s \<or> K3exit CID s; PID \<in>\<in> paperIDs s CID\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding K2exit_def K3exit_def \<Delta>e_def
[PROOF STATE]
proof (prove)
using this:
reach s
vl \<noteq> []
vl \<noteq> [] \<and> ((\<exists>cid. PID \<in>\<in> paperIDs s cid \<and> revPH < phase s cid \<and> (\<nexists>uid. isREVNth s uid PID N)) \<or> (\<exists>cid. PID \<in>\<in> paperIDs s cid \<and> revPH < phase s cid \<and> fst (hd vl) = revPH))

goal (1 subgoal):
 1. (\<And>CID. \<lbrakk>PID \<in>\<in> paperIDs s CID \<and> revPH < phase s CID \<and> (\<nexists>uid. isRevNth s CID uid PID N) \<or> PID \<in>\<in> paperIDs s CID \<and> revPH < phase s CID; PID \<in>\<in> paperIDs s CID\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
K2exit CID s \<or> K3exit CID s
PID \<in>\<in> paperIDs s CID

goal (1 subgoal):
 1. \<And>s vl s1 vl1. \<lbrakk>reachNT s; reach s1; \<Delta>e s vl s1 vl1\<rbrakk> \<Longrightarrow> vl \<noteq> [] \<and> exit s (hd vl)
[PROOF STEP]
show "vl \<noteq> [] \<and> exit s (hd vl)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vl \<noteq> [] \<and> exit s (hd vl)
[PROOF STEP]
proof(simp add: vl, cases "K2exit CID s")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. K2exit CID s \<Longrightarrow> exit s (hd vl)
 2. \<not> K2exit CID s \<Longrightarrow> exit s (hd vl)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
K2exit CID s

goal (2 subgoals):
 1. K2exit CID s \<Longrightarrow> exit s (hd vl)
 2. \<not> K2exit CID s \<Longrightarrow> exit s (hd vl)
[PROOF STEP]
thus "exit s (hd vl)"
[PROOF STATE]
proof (prove)
using this:
K2exit CID s

goal (1 subgoal):
 1. exit s (hd vl)
[PROOF STEP]
by (metis rsT exitI2 invarNT_K2exit noVal_K2exit)
[PROOF STATE]
proof (state)
this:
exit s (hd vl)

goal (1 subgoal):
 1. \<not> K2exit CID s \<Longrightarrow> exit s (hd vl)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> K2exit CID s \<Longrightarrow> exit s (hd vl)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> K2exit CID s

goal (1 subgoal):
 1. \<not> K2exit CID s \<Longrightarrow> exit s (hd vl)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> K2exit CID s
[PROOF STEP]
obtain u where h: "hd vl = (revPH,u)" and K3: "K3exit CID s"
[PROOF STATE]
proof (prove)
using this:
\<not> K2exit CID s

goal (1 subgoal):
 1. (\<And>u. \<lbrakk>hd vl = (revPH, u); K3exit CID s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<Delta>e K PID rs
[PROOF STATE]
proof (prove)
using this:
\<not> K2exit CID s
\<Delta>e s vl s1 vl1
K2exit CID s \<or> K3exit CID s
PID \<in>\<in> paperIDs s CID
reach s

goal (1 subgoal):
 1. (\<And>u. \<lbrakk>hd vl = (revPH, u); K3exit CID s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding \<Delta>e_def K2exit_def K3exit_def
[PROOF STATE]
proof (prove)
using this:
\<not> (PID \<in>\<in> paperIDs s CID \<and> revPH < phase s CID \<and> (\<nexists>uid. isRevNth s CID uid PID N))
vl \<noteq> [] \<and> ((\<exists>cid. PID \<in>\<in> paperIDs s cid \<and> revPH < phase s cid \<and> (\<nexists>uid. isREVNth s uid PID N)) \<or> (\<exists>cid. PID \<in>\<in> paperIDs s cid \<and> revPH < phase s cid \<and> fst (hd vl) = revPH))
PID \<in>\<in> paperIDs s CID \<and> revPH < phase s CID \<and> (\<nexists>uid. isRevNth s CID uid PID N) \<or> PID \<in>\<in> paperIDs s CID \<and> revPH < phase s CID
PID \<in>\<in> paperIDs s CID
reach s

goal (1 subgoal):
 1. (\<And>u. \<lbrakk>hd vl = (revPH, u); PID \<in>\<in> paperIDs s CID \<and> revPH < phase s CID\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases vl) (auto simp: isREVNth_def)
[PROOF STATE]
proof (state)
this:
hd vl = (revPH, u)
K3exit CID s

goal (1 subgoal):
 1. \<not> K2exit CID s \<Longrightarrow> exit s (hd vl)
[PROOF STEP]
show "exit s (hd vl)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exit s (hd vl)
[PROOF STEP]
unfolding h
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exit s (revPH, u)
[PROOF STEP]
using K3
[PROOF STATE]
proof (prove)
using this:
K3exit CID s

goal (1 subgoal):
 1. exit s (revPH, u)
[PROOF STEP]
by (metis rsT exitI2 invarNT_K3exit noVal_K3exit)
[PROOF STATE]
proof (state)
this:
exit s (hd vl)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
vl \<noteq> [] \<and> exit s (hd vl)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem secure: secure
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. secure
[PROOF STEP]
apply(rule unwind_decomp4_secure[of \<Delta>1 \<Delta>2 \<Delta>e \<Delta>3 \<Delta>4])
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>vl vl1. B vl vl1 \<Longrightarrow> \<Delta>1 istate vl istate vl1
 2. unwind_cont \<Delta>1 {\<Delta>1, \<Delta>2, \<Delta>e}
 3. unwind_cont \<Delta>2 {\<Delta>2, \<Delta>3, \<Delta>e}
 4. unwind_cont \<Delta>3 {\<Delta>3, \<Delta>4, \<Delta>e}
 5. unwind_cont \<Delta>4 {\<Delta>4, \<Delta>e}
 6. unwind_exit \<Delta>e
[PROOF STEP]
using
istate_\<Delta>1
unwind_cont_\<Delta>1 unwind_cont_\<Delta>2 unwind_cont_\<Delta>2 unwind_cont_\<Delta>3 unwind_cont_\<Delta>4
unwind_exit_\<Delta>e
[PROOF STATE]
proof (prove)
using this:
B ?vl ?vl1.0 \<Longrightarrow> \<Delta>1 istate ?vl istate ?vl1.0
unwind_cont \<Delta>1 {\<Delta>1, \<Delta>2, \<Delta>e}
unwind_cont \<Delta>2 {\<Delta>2, \<Delta>3, \<Delta>e}
unwind_cont \<Delta>2 {\<Delta>2, \<Delta>3, \<Delta>e}
unwind_cont \<Delta>3 {\<Delta>3, \<Delta>4, \<Delta>e}
unwind_cont \<Delta>4 {\<Delta>4, \<Delta>e}
unwind_exit \<Delta>e

goal (6 subgoals):
 1. \<And>vl vl1. B vl vl1 \<Longrightarrow> \<Delta>1 istate vl istate vl1
 2. unwind_cont \<Delta>1 {\<Delta>1, \<Delta>2, \<Delta>e}
 3. unwind_cont \<Delta>2 {\<Delta>2, \<Delta>3, \<Delta>e}
 4. unwind_cont \<Delta>3 {\<Delta>3, \<Delta>4, \<Delta>e}
 5. unwind_cont \<Delta>4 {\<Delta>4, \<Delta>e}
 6. unwind_exit \<Delta>e
[PROOF STEP]
by auto


[STATEMENT]
lemma isCom1_isComV1:
assumes "validTrans trn1" and "reach (srcOf trn1)" and "\<phi>1 trn1"
shows "isCom1 trn1 \<longleftrightarrow> isComV1 (f1 trn1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isCom1 trn1 = isComV1 (f1 trn1)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Iss.validTrans trn1
Iss.reach (srcOf trn1)
\<phi>1 trn1

goal (1 subgoal):
 1. isCom1 trn1 = isComV1 (f1 trn1)
[PROOF STEP]
apply(cases trn1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4. \<lbrakk>Iss.validTrans trn1; Iss.reach (srcOf trn1); \<phi>1 trn1; trn1 = Trans x1 x2 x3 x4\<rbrakk> \<Longrightarrow> isCom1 trn1 = isComV1 (f1 trn1)
[PROOF STEP]
by (auto simp: Iss.\<phi>_def2 split: prod.splits)


[STATEMENT]
lemma isCom1_isComO1:
assumes "validTrans trn1" and "reach (srcOf trn1)" and "\<gamma>1 trn1"
shows "isCom1 trn1 \<longleftrightarrow> isComO1 (g1 trn1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isCom1 trn1 = isComO1 (g1 trn1)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Iss.validTrans trn1
Iss.reach (srcOf trn1)
\<gamma>1 trn1

goal (1 subgoal):
 1. isCom1 trn1 = isComO1 (g1 trn1)
[PROOF STEP]
by (cases trn1 rule: isCom1.cases) auto


[STATEMENT]
lemma isCom2_isComV2:
assumes "validTrans trn2" and "reach (srcOf trn2)" and "\<phi>2 trn2"
shows "isCom2 trn2 \<longleftrightarrow> isComV2 (f2 trn2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isCom2 trn2 = isComV2 (f2 trn2)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Iss.validTrans trn2
Iss.reach (srcOf trn2)
\<phi>2 trn2

goal (1 subgoal):
 1. isCom2 trn2 = isComV2 (f2 trn2)
[PROOF STEP]
apply(cases trn2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4. \<lbrakk>Iss.validTrans trn2; Iss.reach (srcOf trn2); \<phi>2 trn2; trn2 = Trans x1 x2 x3 x4\<rbrakk> \<Longrightarrow> isCom2 trn2 = isComV2 (f2 trn2)
[PROOF STEP]
by (auto simp: Rcv.\<phi>_def2 split: prod.splits)


[STATEMENT]
lemma isCom2_isComO2:
assumes "validTrans trn2" and "reach (srcOf trn2)" and "\<gamma>2 trn2"
shows "isCom2 trn2 \<longleftrightarrow> isComO2 (g2 trn2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isCom2 trn2 = isComO2 (g2 trn2)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Iss.validTrans trn2
Iss.reach (srcOf trn2)
\<gamma>2 trn2

goal (1 subgoal):
 1. isCom2 trn2 = isComO2 (g2 trn2)
[PROOF STEP]
by (cases trn2 rule: isCom2.cases) auto


[STATEMENT]
lemma sync_syncV:
assumes "validTrans trn1" and "reach (srcOf trn1)"
and "validTrans trn2" and "reach (srcOf trn2)"
and "isCom1 trn1" and "isCom2 trn2" and "\<phi>1 trn1" and "\<phi>2 trn2"
and "sync trn1 trn2"
shows "syncV (f1 trn1) (f2 trn2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. syncV (f1 trn1) (f2 trn2)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Iss.validTrans trn1
Iss.reach (srcOf trn1)
Iss.validTrans trn2
Iss.reach (srcOf trn2)
isCom1 trn1
isCom2 trn2
\<phi>1 trn1
\<phi>2 trn2
sync trn1 trn2

goal (1 subgoal):
 1. syncV (f1 trn1) (f2 trn2)
[PROOF STEP]
apply(cases trn1, cases trn2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4 x1a x2a x3a x4a. \<lbrakk>Iss.validTrans trn1; Iss.reach (srcOf trn1); Iss.validTrans trn2; Iss.reach (srcOf trn2); isCom1 trn1; isCom2 trn2; \<phi>1 trn1; \<phi>2 trn2; sync trn1 trn2; trn1 = Trans x1 x2 x3 x4; Iss.validTrans trn1; Iss.reach (srcOf trn1); Iss.validTrans trn2; Iss.reach (srcOf trn2); isCom1 trn1; isCom2 trn2; \<phi>1 trn1; \<phi>2 trn2; sync trn1 trn2; trn2 = Trans x1a x2a x3a x4a\<rbrakk> \<Longrightarrow> syncV (f1 trn1) (f2 trn2)
[PROOF STEP]
by (auto simp: Iss.\<phi>_def2 Rcv.\<phi>_def2 split: prod.splits)


[STATEMENT]
lemma sync_syncO:
assumes "validTrans trn1" and "reach (srcOf trn1)"
and "validTrans trn2" and "reach (srcOf trn2)"
and "isCom1 trn1" and "isCom2 trn2" and "\<gamma>1 trn1" and "\<gamma>2 trn2"
and "sync trn1 trn2"
shows "syncO (g1 trn1) (g2 trn2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. syncO (g1 trn1) (g2 trn2)
[PROOF STEP]
proof(cases trn1)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4. trn1 = Trans x1 x2 x3 x4 \<Longrightarrow> syncO (g1 trn1) (g2 trn2)
[PROOF STEP]
case (Trans s1 a1 ou1 s1')
[PROOF STATE]
proof (state)
this:
trn1 = Trans s1 a1 ou1 s1'

goal (1 subgoal):
 1. \<And>x1 x2 x3 x4. trn1 = Trans x1 x2 x3 x4 \<Longrightarrow> syncO (g1 trn1) (g2 trn2)
[PROOF STEP]
note trn1 = Trans
[PROOF STATE]
proof (state)
this:
trn1 = Trans s1 a1 ou1 s1'

goal (1 subgoal):
 1. \<And>x1 x2 x3 x4. trn1 = Trans x1 x2 x3 x4 \<Longrightarrow> syncO (g1 trn1) (g2 trn2)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. syncO (g1 trn1) (g2 trn2)
[PROOF STEP]
proof(cases trn2)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4. trn2 = Trans x1 x2 x3 x4 \<Longrightarrow> syncO (g1 trn1) (g2 trn2)
[PROOF STEP]
case (Trans s2 a2 ou2 s2')
[PROOF STATE]
proof (state)
this:
trn2 = Trans s2 a2 ou2 s2'

goal (1 subgoal):
 1. \<And>x1 x2 x3 x4. trn2 = Trans x1 x2 x3 x4 \<Longrightarrow> syncO (g1 trn1) (g2 trn2)
[PROOF STEP]
note trn2 = Trans
[PROOF STATE]
proof (state)
this:
trn2 = Trans s2 a2 ou2 s2'

goal (1 subgoal):
 1. \<And>x1 x2 x3 x4. trn2 = Trans x1 x2 x3 x4 \<Longrightarrow> syncO (g1 trn1) (g2 trn2)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. syncO (g1 trn1) (g2 trn2)
[PROOF STEP]
proof(cases a1)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>x1. a1 = Sact x1 \<Longrightarrow> syncO (g1 trn1) (g2 trn2)
 2. \<And>x2. a1 = Cact x2 \<Longrightarrow> syncO (g1 trn1) (g2 trn2)
 3. \<And>x3. a1 = Dact x3 \<Longrightarrow> syncO (g1 trn1) (g2 trn2)
 4. \<And>x4. a1 = Uact x4 \<Longrightarrow> syncO (g1 trn1) (g2 trn2)
 5. \<And>x5. a1 = Ract x5 \<Longrightarrow> syncO (g1 trn1) (g2 trn2)
 6. \<And>x6. a1 = Lact x6 \<Longrightarrow> syncO (g1 trn1) (g2 trn2)
 7. \<And>x7. a1 = COMact x7 \<Longrightarrow> syncO (g1 trn1) (g2 trn2)
[PROOF STEP]
case (COMact ca1)
[PROOF STATE]
proof (state)
this:
a1 = COMact ca1

goal (7 subgoals):
 1. \<And>x1. a1 = Sact x1 \<Longrightarrow> syncO (g1 trn1) (g2 trn2)
 2. \<And>x2. a1 = Cact x2 \<Longrightarrow> syncO (g1 trn1) (g2 trn2)
 3. \<And>x3. a1 = Dact x3 \<Longrightarrow> syncO (g1 trn1) (g2 trn2)
 4. \<And>x4. a1 = Uact x4 \<Longrightarrow> syncO (g1 trn1) (g2 trn2)
 5. \<And>x5. a1 = Ract x5 \<Longrightarrow> syncO (g1 trn1) (g2 trn2)
 6. \<And>x6. a1 = Lact x6 \<Longrightarrow> syncO (g1 trn1) (g2 trn2)
 7. \<And>x7. a1 = COMact x7 \<Longrightarrow> syncO (g1 trn1) (g2 trn2)
[PROOF STEP]
note a1 = COMact
[PROOF STATE]
proof (state)
this:
a1 = COMact ca1

goal (7 subgoals):
 1. \<And>x1. a1 = Sact x1 \<Longrightarrow> syncO (g1 trn1) (g2 trn2)
 2. \<And>x2. a1 = Cact x2 \<Longrightarrow> syncO (g1 trn1) (g2 trn2)
 3. \<And>x3. a1 = Dact x3 \<Longrightarrow> syncO (g1 trn1) (g2 trn2)
 4. \<And>x4. a1 = Uact x4 \<Longrightarrow> syncO (g1 trn1) (g2 trn2)
 5. \<And>x5. a1 = Ract x5 \<Longrightarrow> syncO (g1 trn1) (g2 trn2)
 6. \<And>x6. a1 = Lact x6 \<Longrightarrow> syncO (g1 trn1) (g2 trn2)
 7. \<And>x7. a1 = COMact x7 \<Longrightarrow> syncO (g1 trn1) (g2 trn2)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. syncO (g1 trn1) (g2 trn2)
[PROOF STEP]
proof(cases a2)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>x1. a2 = Sact x1 \<Longrightarrow> syncO (g1 trn1) (g2 trn2)
 2. \<And>x2. a2 = Cact x2 \<Longrightarrow> syncO (g1 trn1) (g2 trn2)
 3. \<And>x3. a2 = Dact x3 \<Longrightarrow> syncO (g1 trn1) (g2 trn2)
 4. \<And>x4. a2 = Uact x4 \<Longrightarrow> syncO (g1 trn1) (g2 trn2)
 5. \<And>x5. a2 = Ract x5 \<Longrightarrow> syncO (g1 trn1) (g2 trn2)
 6. \<And>x6. a2 = Lact x6 \<Longrightarrow> syncO (g1 trn1) (g2 trn2)
 7. \<And>x7. a2 = COMact x7 \<Longrightarrow> syncO (g1 trn1) (g2 trn2)
[PROOF STEP]
case (COMact ca2)
[PROOF STATE]
proof (state)
this:
a2 = COMact ca2

goal (7 subgoals):
 1. \<And>x1. a2 = Sact x1 \<Longrightarrow> syncO (g1 trn1) (g2 trn2)
 2. \<And>x2. a2 = Cact x2 \<Longrightarrow> syncO (g1 trn1) (g2 trn2)
 3. \<And>x3. a2 = Dact x3 \<Longrightarrow> syncO (g1 trn1) (g2 trn2)
 4. \<And>x4. a2 = Uact x4 \<Longrightarrow> syncO (g1 trn1) (g2 trn2)
 5. \<And>x5. a2 = Ract x5 \<Longrightarrow> syncO (g1 trn1) (g2 trn2)
 6. \<And>x6. a2 = Lact x6 \<Longrightarrow> syncO (g1 trn1) (g2 trn2)
 7. \<And>x7. a2 = COMact x7 \<Longrightarrow> syncO (g1 trn1) (g2 trn2)
[PROOF STEP]
note a2 = COMact
[PROOF STATE]
proof (state)
this:
a2 = COMact ca2

goal (7 subgoals):
 1. \<And>x1. a2 = Sact x1 \<Longrightarrow> syncO (g1 trn1) (g2 trn2)
 2. \<And>x2. a2 = Cact x2 \<Longrightarrow> syncO (g1 trn1) (g2 trn2)
 3. \<And>x3. a2 = Dact x3 \<Longrightarrow> syncO (g1 trn1) (g2 trn2)
 4. \<And>x4. a2 = Uact x4 \<Longrightarrow> syncO (g1 trn1) (g2 trn2)
 5. \<And>x5. a2 = Ract x5 \<Longrightarrow> syncO (g1 trn1) (g2 trn2)
 6. \<And>x6. a2 = Lact x6 \<Longrightarrow> syncO (g1 trn1) (g2 trn2)
 7. \<And>x7. a2 = COMact x7 \<Longrightarrow> syncO (g1 trn1) (g2 trn2)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. syncO (g1 trn1) (g2 trn2)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Iss.validTrans trn1
Iss.reach (srcOf trn1)
Iss.validTrans trn2
Iss.reach (srcOf trn2)
isCom1 trn1
isCom2 trn2
\<gamma>1 trn1
\<gamma>2 trn2
sync trn1 trn2

goal (1 subgoal):
 1. syncO (g1 trn1) (g2 trn2)
[PROOF STEP]
unfolding trn1 trn2 a1 a2
[PROOF STATE]
proof (prove)
using this:
Iss.validTrans (Trans s1 (COMact ca1) ou1 s1')
Iss.reach (srcOf (Trans s1 (COMact ca1) ou1 s1'))
Iss.validTrans (Trans s2 (COMact ca2) ou2 s2')
Iss.reach (srcOf (Trans s2 (COMact ca2) ou2 s2'))
isCom1 (Trans s1 (COMact ca1) ou1 s1')
isCom2 (Trans s2 (COMact ca2) ou2 s2')
\<gamma>1 (Trans s1 (COMact ca1) ou1 s1')
\<gamma>2 (Trans s2 (COMact ca2) ou2 s2')
sync (Trans s1 (COMact ca1) ou1 s1') (Trans s2 (COMact ca2) ou2 s2')

goal (1 subgoal):
 1. syncO (g1 (Trans s1 (COMact ca1) ou1 s1')) (g2 (Trans s2 (COMact ca2) ou2 s2'))
[PROOF STEP]
apply(cases ca1)
[PROOF STATE]
proof (prove)
goal (10 subgoals):
 1. \<And>x11 x12 x13 x14. \<lbrakk>Iss.validTrans (Trans s1 (COMact ca1) ou1 s1'); Iss.reach (srcOf (Trans s1 (COMact ca1) ou1 s1')); Iss.validTrans (Trans s2 (COMact ca2) ou2 s2'); Iss.reach (srcOf (Trans s2 (COMact ca2) ou2 s2')); isCom1 (Trans s1 (COMact ca1) ou1 s1'); isCom2 (Trans s2 (COMact ca2) ou2 s2'); \<gamma>1 (Trans s1 (COMact ca1) ou1 s1'); \<gamma>2 (Trans s2 (COMact ca2) ou2 s2'); sync (Trans s1 (COMact ca1) ou1 s1') (Trans s2 (COMact ca2) ou2 s2'); ca1 = comSendServerReq x11 x12 x13 x14\<rbrakk> \<Longrightarrow> syncO (g1 (Trans s1 (COMact ca1) ou1 s1')) (g2 (Trans s2 (COMact ca2) ou2 s2'))
 2. \<And>x21 x22. \<lbrakk>Iss.validTrans (Trans s1 (COMact ca1) ou1 s1'); Iss.reach (srcOf (Trans s1 (COMact ca1) ou1 s1')); Iss.validTrans (Trans s2 (COMact ca2) ou2 s2'); Iss.reach (srcOf (Trans s2 (COMact ca2) ou2 s2')); isCom1 (Trans s1 (COMact ca1) ou1 s1'); isCom2 (Trans s2 (COMact ca2) ou2 s2'); \<gamma>1 (Trans s1 (COMact ca1) ou1 s1'); \<gamma>2 (Trans s2 (COMact ca2) ou2 s2'); sync (Trans s1 (COMact ca1) ou1 s1') (Trans s2 (COMact ca2) ou2 s2'); ca1 = comReceiveClientReq x21 x22\<rbrakk> \<Longrightarrow> syncO (g1 (Trans s1 (COMact ca1) ou1 s1')) (g2 (Trans s2 (COMact ca2) ou2 s2'))
 3. \<And>x31 x32 x33 x34. \<lbrakk>Iss.validTrans (Trans s1 (COMact ca1) ou1 s1'); Iss.reach (srcOf (Trans s1 (COMact ca1) ou1 s1')); Iss.validTrans (Trans s2 (COMact ca2) ou2 s2'); Iss.reach (srcOf (Trans s2 (COMact ca2) ou2 s2')); isCom1 (Trans s1 (COMact ca1) ou1 s1'); isCom2 (Trans s2 (COMact ca2) ou2 s2'); \<gamma>1 (Trans s1 (COMact ca1) ou1 s1'); \<gamma>2 (Trans s2 (COMact ca2) ou2 s2'); sync (Trans s1 (COMact ca1) ou1 s1') (Trans s2 (COMact ca2) ou2 s2'); ca1 = comConnectClient x31 x32 x33 x34\<rbrakk> \<Longrightarrow> syncO (g1 (Trans s1 (COMact ca1) ou1 s1')) (g2 (Trans s2 (COMact ca2) ou2 s2'))
 4. \<And>x41 x42. \<lbrakk>Iss.validTrans (Trans s1 (COMact ca1) ou1 s1'); Iss.reach (srcOf (Trans s1 (COMact ca1) ou1 s1')); Iss.validTrans (Trans s2 (COMact ca2) ou2 s2'); Iss.reach (srcOf (Trans s2 (COMact ca2) ou2 s2')); isCom1 (Trans s1 (COMact ca1) ou1 s1'); isCom2 (Trans s2 (COMact ca2) ou2 s2'); \<gamma>1 (Trans s1 (COMact ca1) ou1 s1'); \<gamma>2 (Trans s2 (COMact ca2) ou2 s2'); sync (Trans s1 (COMact ca1) ou1 s1') (Trans s2 (COMact ca2) ou2 s2'); ca1 = comConnectServer x41 x42\<rbrakk> \<Longrightarrow> syncO (g1 (Trans s1 (COMact ca1) ou1 s1')) (g2 (Trans s2 (COMact ca2) ou2 s2'))
 5. \<And>x51 x52 x53 x54 x55 x56. \<lbrakk>Iss.validTrans (Trans s1 (COMact ca1) ou1 s1'); Iss.reach (srcOf (Trans s1 (COMact ca1) ou1 s1')); Iss.validTrans (Trans s2 (COMact ca2) ou2 s2'); Iss.reach (srcOf (Trans s2 (COMact ca2) ou2 s2')); isCom1 (Trans s1 (COMact ca1) ou1 s1'); isCom2 (Trans s2 (COMact ca2) ou2 s2'); \<gamma>1 (Trans s1 (COMact ca1) ou1 s1'); \<gamma>2 (Trans s2 (COMact ca2) ou2 s2'); sync (Trans s1 (COMact ca1) ou1 s1') (Trans s2 (COMact ca2) ou2 s2'); ca1 = comReceivePost x51 x52 x53 x54 x55 x56\<rbrakk> \<Longrightarrow> syncO (g1 (Trans s1 (COMact ca1) ou1 s1')) (g2 (Trans s2 (COMact ca2) ou2 s2'))
 6. \<And>x61 x62 x63 x64. \<lbrakk>Iss.validTrans (Trans s1 (COMact ca1) ou1 s1'); Iss.reach (srcOf (Trans s1 (COMact ca1) ou1 s1')); Iss.validTrans (Trans s2 (COMact ca2) ou2 s2'); Iss.reach (srcOf (Trans s2 (COMact ca2) ou2 s2')); isCom1 (Trans s1 (COMact ca1) ou1 s1'); isCom2 (Trans s2 (COMact ca2) ou2 s2'); \<gamma>1 (Trans s1 (COMact ca1) ou1 s1'); \<gamma>2 (Trans s2 (COMact ca2) ou2 s2'); sync (Trans s1 (COMact ca1) ou1 s1') (Trans s2 (COMact ca2) ou2 s2'); ca1 = comSendPost x61 x62 x63 x64\<rbrakk> \<Longrightarrow> syncO (g1 (Trans s1 (COMact ca1) ou1 s1')) (g2 (Trans s2 (COMact ca2) ou2 s2'))
 7. \<And>x71 x72 x73 x74. \<lbrakk>Iss.validTrans (Trans s1 (COMact ca1) ou1 s1'); Iss.reach (srcOf (Trans s1 (COMact ca1) ou1 s1')); Iss.validTrans (Trans s2 (COMact ca2) ou2 s2'); Iss.reach (srcOf (Trans s2 (COMact ca2) ou2 s2')); isCom1 (Trans s1 (COMact ca1) ou1 s1'); isCom2 (Trans s2 (COMact ca2) ou2 s2'); \<gamma>1 (Trans s1 (COMact ca1) ou1 s1'); \<gamma>2 (Trans s2 (COMact ca2) ou2 s2'); sync (Trans s1 (COMact ca1) ou1 s1') (Trans s2 (COMact ca2) ou2 s2'); ca1 = comReceiveCreateOFriend x71 x72 x73 x74\<rbrakk> \<Longrightarrow> syncO (g1 (Trans s1 (COMact ca1) ou1 s1')) (g2 (Trans s2 (COMact ca2) ou2 s2'))
 8. \<And>x81 x82 x83 x84. \<lbrakk>Iss.validTrans (Trans s1 (COMact ca1) ou1 s1'); Iss.reach (srcOf (Trans s1 (COMact ca1) ou1 s1')); Iss.validTrans (Trans s2 (COMact ca2) ou2 s2'); Iss.reach (srcOf (Trans s2 (COMact ca2) ou2 s2')); isCom1 (Trans s1 (COMact ca1) ou1 s1'); isCom2 (Trans s2 (COMact ca2) ou2 s2'); \<gamma>1 (Trans s1 (COMact ca1) ou1 s1'); \<gamma>2 (Trans s2 (COMact ca2) ou2 s2'); sync (Trans s1 (COMact ca1) ou1 s1') (Trans s2 (COMact ca2) ou2 s2'); ca1 = comSendCreateOFriend x81 x82 x83 x84\<rbrakk> \<Longrightarrow> syncO (g1 (Trans s1 (COMact ca1) ou1 s1')) (g2 (Trans s2 (COMact ca2) ou2 s2'))
 9. \<And>x91 x92 x93 x94. \<lbrakk>Iss.validTrans (Trans s1 (COMact ca1) ou1 s1'); Iss.reach (srcOf (Trans s1 (COMact ca1) ou1 s1')); Iss.validTrans (Trans s2 (COMact ca2) ou2 s2'); Iss.reach (srcOf (Trans s2 (COMact ca2) ou2 s2')); isCom1 (Trans s1 (COMact ca1) ou1 s1'); isCom2 (Trans s2 (COMact ca2) ou2 s2'); \<gamma>1 (Trans s1 (COMact ca1) ou1 s1'); \<gamma>2 (Trans s2 (COMact ca2) ou2 s2'); sync (Trans s1 (COMact ca1) ou1 s1') (Trans s2 (COMact ca2) ou2 s2'); ca1 = comReceiveDeleteOFriend x91 x92 x93 x94\<rbrakk> \<Longrightarrow> syncO (g1 (Trans s1 (COMact ca1) ou1 s1')) (g2 (Trans s2 (COMact ca2) ou2 s2'))
 10. \<And>x101 x102 x103 x104. \<lbrakk>Iss.validTrans (Trans s1 (COMact ca1) ou1 s1'); Iss.reach (srcOf (Trans s1 (COMact ca1) ou1 s1')); Iss.validTrans (Trans s2 (COMact ca2) ou2 s2'); Iss.reach (srcOf (Trans s2 (COMact ca2) ou2 s2')); isCom1 (Trans s1 (COMact ca1) ou1 s1'); isCom2 (Trans s2 (COMact ca2) ou2 s2'); \<gamma>1 (Trans s1 (COMact ca1) ou1 s1'); \<gamma>2 (Trans s2 (COMact ca2) ou2 s2'); sync (Trans s1 (COMact ca1) ou1 s1') (Trans s2 (COMact ca2) ou2 s2'); ca1 = comSendDeleteOFriend x101 x102 x103 x104\<rbrakk> \<Longrightarrow> syncO (g1 (Trans s1 (COMact ca1) ou1 s1')) (g2 (Trans s2 (COMact ca2) ou2 s2'))
[PROOF STEP]
by (cases ca2, auto split: prod.splits)+
[PROOF STATE]
proof (state)
this:
syncO (g1 trn1) (g2 trn2)

goal (6 subgoals):
 1. \<And>x1. a2 = Sact x1 \<Longrightarrow> syncO (g1 trn1) (g2 trn2)
 2. \<And>x2. a2 = Cact x2 \<Longrightarrow> syncO (g1 trn1) (g2 trn2)
 3. \<And>x3. a2 = Dact x3 \<Longrightarrow> syncO (g1 trn1) (g2 trn2)
 4. \<And>x4. a2 = Uact x4 \<Longrightarrow> syncO (g1 trn1) (g2 trn2)
 5. \<And>x5. a2 = Ract x5 \<Longrightarrow> syncO (g1 trn1) (g2 trn2)
 6. \<And>x6. a2 = Lact x6 \<Longrightarrow> syncO (g1 trn1) (g2 trn2)
[PROOF STEP]
qed(insert assms, unfold trn1 trn2, auto)
[PROOF STATE]
proof (state)
this:
syncO (g1 trn1) (g2 trn2)

goal (6 subgoals):
 1. \<And>x1. a1 = Sact x1 \<Longrightarrow> syncO (g1 trn1) (g2 trn2)
 2. \<And>x2. a1 = Cact x2 \<Longrightarrow> syncO (g1 trn1) (g2 trn2)
 3. \<And>x3. a1 = Dact x3 \<Longrightarrow> syncO (g1 trn1) (g2 trn2)
 4. \<And>x4. a1 = Uact x4 \<Longrightarrow> syncO (g1 trn1) (g2 trn2)
 5. \<And>x5. a1 = Ract x5 \<Longrightarrow> syncO (g1 trn1) (g2 trn2)
 6. \<And>x6. a1 = Lact x6 \<Longrightarrow> syncO (g1 trn1) (g2 trn2)
[PROOF STEP]
qed(insert assms, unfold trn1 trn2, auto)
[PROOF STATE]
proof (state)
this:
syncO (g1 trn1) (g2 trn2)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
syncO (g1 trn1) (g2 trn2)

goal:
No subgoals!
[PROOF STEP]
qed